From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 vernac/comFixpoint.ml | 353 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 353 insertions(+)
 create mode 100644 vernac/comFixpoint.ml

(limited to 'vernac/comFixpoint.ml')

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
new file mode 100644
index 00000000..1c141c01
--- /dev/null
+++ b/vernac/comFixpoint.ml
@@ -0,0 +1,353 @@
+open Pp
+open CErrors
+open Util
+open Constr
+open Vars
+open Termops
+open Declare
+open Names
+open Constrexpr
+open Constrexpr_ops
+open Constrintern
+open Decl_kinds
+open Pretyping
+open Evarutil
+open Evarconv
+open Misctypes
+
+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' (EConstr.of_constr 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 ~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 env sigma before in
+  let sigma, (impl_env', ((env'', ctx'), imps')) = interp_context_evars ~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 sigma impls (env,_) fix =
+  interp_type_evars_impls ~impls env sigma fix.fix_type
+
+let interp_fix_body 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 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 fixtypes fixdefs =
+  let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
+  let names = List.map (fun id -> Name id) fixnames 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 * constr option list * types list
+
+(* Wellfounded definition *)
+
+let contrib_name = "Program"
+let subtac_dir = [contrib_name]
+let tactics_module = subtac_dir @ ["Tactics"]
+
+let init_constant dir s sigma =
+  Evarutil.new_global sigma (Coqlib.coq_reference "Command" dir s)
+
+let fix_proto = init_constant tactics_module "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 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 = Univdecls.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 env sigma ~cofix) sigma fixl in
+  let fixctximpenvs, fixctximps = List.split fiximppairs in
+  let sigma, (fixccls,fixcclimps) =
+    on_snd List.split @@
+      List.fold_left3_map interp_fix_ccl 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
+               let _evd = ref sigma in
+               let res = Typing.e_solve_evars env _evd app in
+               !_evd, res
+             with e when CErrors.noncritical e -> sigma, t
+           in
+           sigma, LocalAssum (id,fixprot) :: env'
+         else sigma, LocalAssum (id,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 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, _ = nf_evars_and_universes sigma in
+  let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr sigma) c) fixdefs in
+  let fixtypes = List.map EConstr.(to_constr sigma) fixtypes in
+  let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in
+
+  (* Build the fix declaration block *)
+  (env,rec_sign,decl,sigma), (fixnames,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots
+
+let check_recursive isfix env evd (fixnames,fixdefs,_) =
+  check_evars_are_solved env evd Evd.empty;
+  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 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;
+  (fix,pl,Evd.evar_universe_context evd,info)
+
+let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
+  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
+    Lemmas.start_proof_with_initialization (local,poly,DefinitionBody Fixpoint)
+      evd pl (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
+  else begin
+    (* We shortcut the proof process *)
+    let fixdefs = List.map Option.get fixdefs in
+    let fixdecls = prepare_recursive_declaration fixnames 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 = Univops.universes_of_constr env (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 (local, poly, Fixpoint) pl ctx)
+              fixnames fixdecls fixtypes fiximps);
+    (* Declare the recursive definitions *)
+    fixpoint_message (Some indexes) fixnames;
+  end;
+  (* Declare notations *)
+  List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns
+
+let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
+  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
+      Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint)
+      evd pl (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
+  else begin
+    (* We shortcut the proof process *)
+    let fixdefs = List.map Option.get fixdefs in
+    let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
+    let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
+    let env = Global.env () in
+    let vars = Univops.universes_of_constr env (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 (local, poly, CoFixpoint) pl ctx)
+              fixnames fixdecls fixtypes fiximps);
+    (* Declare the recursive definitions *)
+    cofixpoint_message fixnames
+  end;
+  (* Declare notations *)
+  List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns
+
+let extract_decreasing_argument limit = function
+  | (na,CStructRec) -> na
+  | (na,_) when not limit -> na
+  | _ -> user_err Pp.(str
+      "Only structural decreasing is supported for a non-Program Fixpoint")
+
+let extract_fixpoint_components limit l =
+  let fixl, ntnl = List.split l in
+  let fixl = List.map (fun (({CAst.v=id},pl),ann,bl,typ,def) ->
+    let ann = extract_decreasing_argument limit 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 local poly l =
+  let fixl, ntns = extract_fixpoint_components 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
+  declare_fixpoint local poly fix possible_indexes ntns;
+  if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
+
+let do_cofixpoint local poly l =
+  let fixl,ntns = extract_cofixpoint_components l in
+  let cofix = interp_fixpoint ~cofix:true fixl ntns in
+  declare_cofixpoint local poly cofix ntns;
+  if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
-- 
cgit v1.2.3