Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: comFixpoint.ml Sprache: SML

Original von: Coq^©

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Pp
open CErrors
open Util
open Constr
open Context
open Vars
open Termops
open Declare
open Names
open Constrexpr
open Constrexpr_ops
open Constrintern
open Decl_kinds
open Pretyping
open Evarutil
open Evarconv

module RelDecl = Context.Rel.Declaration

(* 3c| Fixpoints and co-fixpoints *)

(* An (unoptimized) function that maps preorders to partial orders...

   Input:  a list of associations (x,[y1;...;yn]), all yi distincts
           and different of x, meaning x<=y1, ..., x<=yn

   Output: a list of associations (x,Inr [y1;...;yn]), collecting all
           distincts yi greater than x, _or_, (x, Inl y) meaning that
           x is in the same class as y (in which case, x occurs
           nowhere else in the association map)

   partial_order : ('a * 'a list) list -> ('a * ('a,'a list) union) list
*)

let rec partial_order cmp = function
  | [] -> []
  | (x,xge)::rest ->
    let rec browse res xge' = function
    | [] ->
        let res = List.map (function
          | (z, Inr zge) when List.mem_f cmp x zge ->
            (z, Inr (List.union cmp zge xge'))
          | r -> r) res in
        (x,Inr xge')::res
    | y::xge ->
      let rec link y =
        try match List.assoc_f cmp y res with
        | Inl z -> link z
        | Inr yge ->
          if List.mem_f cmp x yge then
            let res = List.remove_assoc_f cmp y res in
            let res = List.map (function
              | (z, Inl t) ->
                  if cmp t y then (z, Inl x) else (z, Inl t)
              | (z, Inr zge) ->
                  if List.mem_f cmp y zge then
                    (z, Inr (List.add_set cmp x (List.remove cmp y zge)))
                  else
                    (z, Inr zge)) res in
            browse ((y,Inl x)::res) xge' (List.union cmp xge (List.remove cmp x yge))
          else
            browse res (List.add_set cmp y (List.union cmp xge' yge)) xge
        with Not_found -> browse res (List.add_set cmp y xge') xge
      in link y
    in browse (partial_order cmp rest) [] xge

let non_full_mutual_message x xge y yge isfix rest =
  let reason =
    if Id.List.mem x yge then
      Id.print y ++ str " depends on " ++ Id.print x ++ strbrk " but not conversely"
    else if Id.List.mem y xge then
      Id.print x ++ str " depends on " ++ Id.print y ++ strbrk " but not conversely"
    else
      Id.print y ++ str " and " ++ Id.print x ++ strbrk " are not mutually dependent" in
  let e = if List.is_empty rest then reason else strbrk "e.g., " ++ reason in
  let k = if isfix then "fixpoint" else "cofixpoint" in
  let w =
    if isfix
    then strbrk "Well-foundedness check may fail unexpectedly." ++ fnl()
    else mt () in
  strbrk "Not a fully mutually defined " ++ str k ++ fnl () ++
  str "(" ++ e ++ str ")." ++ fnl () ++ w

let warn_non_full_mutual =
  CWarnings.create ~name:"non-full-mutual" ~category:"fixpoints"
         (fun (x,xge,y,yge,isfix,rest) ->
          non_full_mutual_message x xge y yge isfix rest)

let check_mutuality env evd isfix fixl =
  let names = List.map fst fixl in
  let preorder =
    List.map (fun (id,def) ->
      (id, List.filter (fun id' -> not (Id.equal id id') && occur_var env evd id' def) names))
      fixl in
  let po = partial_order Id.equal preorder in
  match List.filter (function (_,Inr _) -> true | _ -> false) po with
    | (x,Inr xge)::(y,Inr yge)::rest ->
       warn_non_full_mutual (x,xge,y,yge,isfix,rest)
    | _ -> ()

type structured_fixpoint_expr = {
  fix_name : Id.t;
  fix_univs : universe_decl_expr option;
  fix_annot : lident option;
  fix_binders : local_binder_expr list;
  fix_body : constr_expr option;
  fix_type : constr_expr
}

let interp_fix_context ~program_mode ~cofix env sigma fix =
  let before, after = if not cofix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in
  let sigma, (impl_env, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma before in
  let sigma, (impl_env', ((env'', ctx'), imps')) =
    interp_context_evars ~program_mode ~impl_env ~shift:(Context.Rel.nhyps ctx) env' sigma after
  in
  let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in
  sigma, ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot)

let interp_fix_ccl ~program_mode sigma impls (env,_) fix =
  let sigma, (c, impl) = interp_type_evars_impls ~program_mode ~impls env sigma fix.fix_type in
  let r = Retyping.relevance_of_type env sigma c in
  sigma, (c, r, impl)

let interp_fix_body ~program_mode env_rec sigma impls (_,ctx) fix ccl =
  let open EConstr in
  Option.cata (fun body ->
    let env = push_rel_context ctx env_rec in
    let sigma, body = interp_casted_constr_evars ~program_mode env sigma ~impls body ccl in
    sigma, Some (it_mkLambda_or_LetIn body ctx)) (sigma, None) fix.fix_body

let build_fix_type (_,ctx) ccl = EConstr.it_mkProd_or_LetIn ccl ctx

let prepare_recursive_declaration fixnames fixrs fixtypes fixdefs =
  let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
  let names = List.map2 (fun id r -> make_annot (Name id) r) fixnames fixrs in
  (Array.of_list names, Array.of_list fixtypes, Array.of_list defs)

(* Jump over let-bindings. *)

let compute_possible_guardness_evidences (ctx,_,recindex) =
  (* A recursive index is characterized by the number of lambdas to
     skip before finding the relevant inductive argument *)
  match recindex with
  | Some i -> [i]
  | None ->
      (* If recursive argument was not given by user, we try all args.
         An earlier approach was to look only for inductive arguments,
         but doing it properly involves delta-reduction, and it finally
         doesn't seem to worth the effort (except for huge mutual
         fixpoints ?) *)
      List.interval 0 (Context.Rel.nhyps ctx - 1)

type recursive_preentry =
  Id.t list * Sorts.relevance list * constr option list * types list

(* Wellfounded definition *)

let fix_proto sigma =
  Evarutil.new_global sigma (Coqlib.lib_ref "program.tactic.fix_proto")

let interp_recursive ~program_mode ~cofix fixl notations =
  let open Context.Named.Declaration in
  let open EConstr in
  let env = Global.env() in
  let fixnames = List.map (fun fix -> fix.fix_name) fixl in

  (* Interp arities allowing for unresolved types *)
  let all_universes =
    List.fold_right (fun sfe acc ->
        match sfe.fix_univs , acc with
        | None , acc -> acc
        | x , None -> x
        | Some ls , Some us ->
          let open UState in
          let lsu = ls.univdecl_instance and usu = us.univdecl_instance in
           if not (CList.for_all2eq (fun x y -> Id.equal x.CAst.v y.CAst.v) lsu usu) then
             user_err Pp.(str "(co)-recursive definitions should all have the same universe binders");
           Some us) fixl None in
  let sigma, decl = interp_univ_decl_opt env all_universes in
  let sigma, (fixctxs, fiximppairs, fixannots) =
    on_snd List.split3 @@
      List.fold_left_map (fun sigma -> interp_fix_context ~program_mode env sigma ~cofix) sigma fixl in
  let fixctximpenvs, fixctximps = List.split fiximppairs in
  let sigma, (fixccls,fixrs,fixcclimps) =
    on_snd List.split3 @@
      List.fold_left3_map (interp_fix_ccl ~program_mode) sigma fixctximpenvs fixctxs fixl in
  let fixtypes = List.map2 build_fix_type fixctxs fixccls in
  let fixtypes = List.map (fun c -> nf_evar sigma c) fixtypes in
  let fiximps = List.map3
    (fun ctximps cclimps (_,ctx) -> ctximps@(Impargs.lift_implicits (Context.Rel.nhyps ctx) cclimps))
    fixctximps fixcclimps fixctxs in
  let sigma, rec_sign =
    List.fold_left2
      (fun (sigma, env') id t ->
         if program_mode then
           let sigma, sort = Typing.type_of ~refresh:true env sigma t in
           let sigma, fixprot =
             try
               let sigma, h_term = fix_proto sigma in
               let app = mkApp (h_term, [|sort; t|]) in
               Typing.solve_evars env sigma app
             with e when CErrors.noncritical e -> sigma, t
           in
           sigma, LocalAssum (make_annot id Sorts.Relevant,fixprot) :: env'
         else sigma, LocalAssum (make_annot id Sorts.Relevant,t) :: env')
      (sigma,[]) fixnames fixtypes
  in
  let env_rec = push_named_context rec_sign env in

  (* Get interpretation metadatas *)
  let impls = compute_internalization_env env sigma Recursive fixnames fixtypes fiximps in

  (* Interp bodies with rollback because temp use of notations/implicit *)
  let sigma, fixdefs =
    Metasyntax.with_syntax_protection (fun () ->
      List.iter (Metasyntax.set_notation_for_interpretation env_rec impls) notations;
      List.fold_left4_map
        (fun sigma fixctximpenv -> interp_fix_body ~program_mode env_rec sigma (Id.Map.fold Id.Map.add fixctximpenv impls))
        sigma fixctximpenvs fixctxs fixl fixccls)
      () in

  (* Instantiate evars and check all are resolved *)
  let sigma = solve_unif_constraints_with_heuristics env_rec sigma in
  let sigma = Evd.minimize_universes sigma in
  let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in

  (* Build the fix declaration block *)
  (env,rec_sign,decl,sigma), (fixnames,fixrs,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots

let check_recursive isfix env evd (fixnames,_,fixdefs,_) =
  if List.for_all Option.has_some fixdefs then begin
    let fixdefs = List.map Option.get fixdefs in
    check_mutuality env evd isfix (List.combine fixnames fixdefs)
  end

let ground_fixpoint env evd (fixnames,fixrs,fixdefs,fixtypes) =
  check_evars_are_solved ~program_mode:false env evd;
  let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr evd) c) fixdefs in
  let fixtypes = List.map EConstr.(to_constr evd) fixtypes in
  Evd.evar_universe_context evd, (fixnames,fixrs,fixdefs,fixtypes)

let interp_fixpoint ~cofix l ntns =
  let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l ntns in
  check_recursive true env evd fix;
  let uctx,fix = ground_fixpoint env evd fix in
  (fix,pl,uctx,info)

let declare_fixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
  let pstate =
  if List.exists Option.is_empty fixdefs then
    (* Some bodies to define by proof *)
    let thms =
      List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps))))
                fixnames fixtypes fiximps in
    let init_tac =
      Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
        fixdefs) in
    let evd = Evd.from_ctx ctx in
    Some
    (Lemmas.start_proof_with_initialization ~ontop (local,poly,DefinitionBody Fixpoint)
      evd pl (Some(false,indexes,init_tac)) thms None)
  else begin
    (* We shortcut the proof process *)
    let fixdefs = List.map Option.get fixdefs in
    let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
    let env = Global.env() in
    let indexes = search_guard env indexes fixdecls in
    let fiximps = List.map (fun (n,r,p) -> r) fiximps in
    let vars = Vars.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
    let fixdecls =
      List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
    let evd = Evd.from_ctx ctx in
    let evd = Evd.restrict_universe_context evd vars in
    let ctx = Evd.check_univ_decl ~poly evd pl in
    let pl = Evd.universe_binders evd in
    let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
    ignore (List.map4 (DeclareDef.declare_fix ~ontop (local, poly, Fixpoint) pl ctx)
              fixnames fixdecls fixtypes fiximps);
    (* Declare the recursive definitions *)
    fixpoint_message (Some indexes) fixnames;
    None
  end in
  (* Declare notations *)
  List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
  pstate

let declare_cofixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
  let pstate =
  if List.exists Option.is_empty fixdefs then
    (* Some bodies to define by proof *)
    let thms =
      List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps))))
                fixnames fixtypes fiximps in
    let init_tac =
      Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
        fixdefs) in
    let evd = Evd.from_ctx ctx in
    Some (Lemmas.start_proof_with_initialization ~ontop (Global,poly, DefinitionBody CoFixpoint)
            evd pl (Some(true,[],init_tac)) thms None)
  else begin
    (* We shortcut the proof process *)
    let fixdefs = List.map Option.get fixdefs in
    let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
    let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
    let vars = Vars.universes_of_constr (List.hd fixdecls) in
    let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
    let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
    let evd = Evd.from_ctx ctx in
    let evd = Evd.restrict_universe_context evd vars in
    let ctx = Evd.check_univ_decl ~poly evd pl in
    let pl = Evd.universe_binders evd in
    ignore (List.map4 (DeclareDef.declare_fix ~ontop (local, poly, CoFixpoint) pl ctx)
              fixnames fixdecls fixtypes fiximps);
    (* Declare the recursive definitions *)
    cofixpoint_message fixnames;
    None
  end in
  (* Declare notations *)
  List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
  pstate

let extract_decreasing_argument ~structonly = function { CAst.v = v } -> match v with
  | CStructRec na -> na
  | (CWfRec (na,_) | CMeasureRec (Some na,_,_)) when not structonly -> na
  | CMeasureRec (None,_,_) when not structonly ->
    user_err Pp.(str "Decreasing argument must be specified in measure clause.")
  | _ -> user_err Pp.(str
           "Well-founded induction requires Program Fixpoint or Function.")

let extract_fixpoint_components ~structonly l =
  let fixl, ntnl = List.split l in
  let fixl = List.map (fun (({CAst.v=id},pl),ann,bl,typ,def) ->
      (* This is a special case: if there's only one binder, we pick it as the
      recursive argument if none is provided. *)
      let ann = Option.map (fun ann -> match bl, ann with
        | [CLocalAssum([{ CAst.v = Name x }],_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } ->
          CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel)
        | [CLocalDef({ CAst.v = Name x },_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } ->
          CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel)
        | _, x -> x) ann
      in
      let ann = Option.map (extract_decreasing_argument ~structonly) ann in
      {fix_name = id; fix_annot = ann; fix_univs = pl;
       fix_binders = bl; fix_body = def; fix_type = typ}) fixl in
  fixl, List.flatten ntnl

let extract_cofixpoint_components l =
  let fixl, ntnl = List.split l in
  List.map (fun (({CAst.v=id},pl),bl,typ,def) ->
            {fix_name = id; fix_annot = None; fix_univs = pl;
             fix_binders = bl; fix_body = def; fix_type = typ}) fixl,
  List.flatten ntnl

let check_safe () =
  let open Declarations in
  let flags = Environ.typing_flags (Global.env ()) in
  flags.check_universes && flags.check_guarded

let do_fixpoint ~ontop local poly l =
  let fixl, ntns = extract_fixpoint_components ~structonly:true l in
  let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl ntns in
  let possible_indexes =
    List.map compute_possible_guardness_evidences info in
  let pstate = declare_fixpoint ~ontop local poly fix possible_indexes ntns in
  if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ();
  pstate

let do_cofixpoint ~ontop local poly l =
  let fixl,ntns = extract_cofixpoint_components l in
  let cofix = interp_fixpoint ~cofix:true fixl ntns in
  let pstate = declare_cofixpoint ~ontop local poly cofix ntns in
  if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ();
  pstate

¤ Dauer der Verarbeitung: 0.31 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.