diff --git a/.gitignore b/.gitignore index bc89608..2a37f27 100644 --- a/.gitignore +++ b/.gitignore @@ -23,3 +23,8 @@ plugin/Makefile plugin/.merlin *.out _opam +_build +/Makefile +/Makefile.conf +.merlin +/src/plibrary.ml diff --git a/README.md b/README.md index ebb8db3..00d47dc 100644 --- a/README.md +++ b/README.md @@ -3,7 +3,7 @@ This is a library of useful utility functions for Coq plugins. These functions o To build this library with a test plugin, run: ``` -./build.sh +dune build ``` See [PUMPKIN PATCH](https://github.com/uwplse/PUMPKIN-PATCH) and [DEVOID](https://github.com/uwplse/ornamental-search) for examples of loading it as a submodule. diff --git a/_CoqProject b/_CoqProject deleted file mode 100644 index 339b268..0000000 --- a/_CoqProject +++ /dev/null @@ -1,97 +0,0 @@ --I src/utilities --I src/coq --I src/coq/termutils --I src/coq/constants --I src/coq/logicutils --I src/coq/logicutils/contexts --I src/coq/logicutils/typesandequality --I src/coq/logicutils/hofs --I src/coq/logicutils/inductive --I src/coq/logicutils/transformation --I src/coq/devutils --I src/coq/representationutils --I src/coq/decompiler --I src --R src Plibrary --Q theories Plibrary - -src/utilities/utilities.mli -src/utilities/utilities.ml - -src/coq/termutils/apputils.mli -src/coq/termutils/apputils.ml -src/coq/termutils/constutils.mli -src/coq/termutils/constutils.ml -src/coq/termutils/funutils.mli -src/coq/termutils/funutils.ml - -src/coq/representationutils/defutils.mli -src/coq/representationutils/defutils.ml -src/coq/representationutils/nameutils.mli -src/coq/representationutils/nameutils.ml - -src/coq/logicutils/typesandequality/inference.mli -src/coq/logicutils/typesandequality/inference.ml -src/coq/logicutils/typesandequality/convertibility.mli -src/coq/logicutils/typesandequality/convertibility.ml -src/coq/logicutils/typesandequality/checking.mli -src/coq/logicutils/typesandequality/checking.ml - -src/coq/constants/equtils.mli -src/coq/constants/equtils.ml -src/coq/constants/sigmautils.mli -src/coq/constants/sigmautils.ml -src/coq/constants/produtils.mli -src/coq/constants/produtils.ml -src/coq/constants/idutils.mli -src/coq/constants/idutils.ml -src/coq/constants/proputils.ml -src/coq/constants/proputils.mli - -src/coq/logicutils/contexts/stateutils.mli -src/coq/logicutils/contexts/stateutils.ml -src/coq/logicutils/contexts/envutils.mli -src/coq/logicutils/contexts/envutils.ml -src/coq/logicutils/contexts/contextutils.mli -src/coq/logicutils/contexts/contextutils.ml - -src/coq/logicutils/hofs/hofs.mli -src/coq/logicutils/hofs/hofs.ml -src/coq/logicutils/hofs/hofimpls.mli -src/coq/logicutils/hofs/hofimpls.ml -src/coq/logicutils/hofs/debruijn.mli -src/coq/logicutils/hofs/debruijn.ml -src/coq/logicutils/hofs/substitution.mli -src/coq/logicutils/hofs/substitution.ml -src/coq/logicutils/hofs/reducers.mli -src/coq/logicutils/hofs/reducers.ml -src/coq/logicutils/hofs/typehofs.mli -src/coq/logicutils/hofs/typehofs.ml -src/coq/logicutils/hofs/zooming.mli -src/coq/logicutils/hofs/zooming.ml -src/coq/logicutils/hofs/hypotheses.mli -src/coq/logicutils/hofs/hypotheses.ml -src/coq/logicutils/hofs/filters.mli -src/coq/logicutils/hofs/filters.ml - -src/coq/logicutils/inductive/indexing.mli -src/coq/logicutils/inductive/indexing.ml -src/coq/logicutils/inductive/indutils.mli -src/coq/logicutils/inductive/indutils.ml - -src/coq/logicutils/contexts/modutils.mli -src/coq/logicutils/contexts/modutils.ml - -src/coq/logicutils/transformation/transform.mli -src/coq/logicutils/transformation/transform.ml - -src/coq/devutils/printing.mli -src/coq/devutils/printing.ml - -src/coq/decompiler/decompiler.mli -src/coq/decompiler/decompiler.ml - -src/plibrary.ml4 -src/plib.mlpack - -theories/Plib.v diff --git a/build.sh b/build.sh deleted file mode 100755 index 99853cb..0000000 --- a/build.sh +++ /dev/null @@ -1,2 +0,0 @@ -coq_makefile -f _CoqProject -o Makefile -make clean && make && make install diff --git a/dune-project b/dune-project new file mode 100644 index 0000000..54d8b99 --- /dev/null +++ b/dune-project @@ -0,0 +1,3 @@ +(lang dune 3.6) +(using coq 0.6) +(name my-plugin) \ No newline at end of file diff --git a/my-plugin.opam b/my-plugin.opam new file mode 100644 index 0000000..e69de29 diff --git a/src/coq/constants/equtils.ml b/src/coq/constants/equtils.ml index a1ed2a8..3867fc1 100644 --- a/src/coq/constants/equtils.ml +++ b/src/coq/constants/equtils.ml @@ -14,7 +14,7 @@ let coq_init_logic = (* equality *) let eq : types = - mkInd (MutInd.make1 (KerName.make2 coq_init_logic (Label.make "eq")), 0) + mkInd (MutInd.make1 (KerName.make coq_init_logic (Label.make "eq")), 0) (* Constructor for quality *) let eq_refl : types = @@ -70,8 +70,9 @@ let apply_eq (app : eq_app) : types = * Deconstruct an eq type *) let dest_eq (trm : types) : eq_app = - let [at_type; trm1; trm2] = unfold_args trm in - { at_type; trm1; trm2 } + match unfold_args trm with + | [at_type; trm1; trm2] -> { at_type; trm1; trm2 } + | _ -> assert false (* * An application of eq_sym @@ -93,10 +94,12 @@ let apply_eq_sym (app : eq_sym_app) : types = * Deconstruct an eq type *) let dest_eq_sym (trm : types) : eq_sym_app = - let [at_type; trm1; trm2; eq_proof] = unfold_args trm in - let eq_typ = { at_type; trm1; trm2 } in - { eq_typ; eq_proof } - + match unfold_args trm with + | [at_type; trm1; trm2; eq_proof] -> + let eq_typ = { at_type; trm1; trm2 } in + { eq_typ; eq_proof } + | _ -> assert false + (* * An application of eq_ind *) @@ -120,8 +123,10 @@ let apply_eq_ind (app : eq_ind_app) : types = * Deconstruct an eq_ind *) let dest_eq_ind (trm : types) : eq_ind_app = - let [at_type; trm1; p; b; trm2; h] = unfold_args trm in - { at_type; trm1; p; b; trm2; h } + match unfold_args trm with + | [at_type; trm1; p; b; trm2; h] -> + { at_type; trm1; p; b; trm2; h } + | _ -> assert false (* * An application of eq_refl @@ -142,8 +147,10 @@ let apply_eq_refl (app : eq_refl_app) : types = * Deconstruct an eq_refl *) let dest_eq_refl (trm : types) : eq_refl_app = - let [typ; trm] = unfold_args trm in - { typ; trm } + match unfold_args trm with + | [typ; trm] -> + { typ; trm } + | _ -> assert false (* * Deconstruct an eq_refl. diff --git a/src/coq/constants/idutils.ml b/src/coq/constants/idutils.ml index 8bf2da7..7ce27c5 100644 --- a/src/coq/constants/idutils.ml +++ b/src/coq/constants/idutils.ml @@ -4,7 +4,6 @@ open Constr open Names -open Environ open Evd let coq_init_datatypes = @@ -27,7 +26,7 @@ let id_typ : types = let identity_term env sigma typ : evar_map * types = let sigma, sort_family = Inference.infer_sort env sigma typ in match sort_family with - | InProp -> + | Sorts.InProp -> (sigma, mkApp (id_prop, Array.make 1 typ)) | _ -> (sigma, mkApp (id_typ, Array.make 1 typ)) diff --git a/src/coq/constants/produtils.ml b/src/coq/constants/produtils.ml index a07adbe..a37069f 100644 --- a/src/coq/constants/produtils.ml +++ b/src/coq/constants/produtils.ml @@ -14,7 +14,7 @@ let coq_init_data = (* prod types *) let prod : types = - mkInd (MutInd.make1 (KerName.make2 coq_init_data (Label.make "prod")), 0) + mkInd (MutInd.make1 (KerName.make coq_init_data (Label.make "prod")), 0) (* Introduction for sigma types *) let pair : constr = @@ -55,9 +55,11 @@ let apply_pair (app : pair_app) = * Deconsruct a sigT type from a type *) let dest_pair (trm : constr) = - let [typ1; typ2; trm1; trm2] = unfold_args trm in - { typ1; typ2; trm1; trm2 } - + match unfold_args trm with + | [typ1; typ2; trm1; trm2] -> + { typ1; typ2; trm1; trm2 } + | _ -> assert false + (* * An application of prod *) @@ -77,8 +79,10 @@ let apply_prod (app : prod_app) : types = * Deconstruct a prod *) let dest_prod (trm : types) : prod_app = - let [typ1; typ2] = unfold_args trm in - { typ1; typ2 } + match unfold_args trm with + | [typ1; typ2] -> + { typ1; typ2 } + | _ -> assert false (* * An application of prod_rect @@ -106,9 +110,11 @@ let elim_prod (app : prod_elim) = * Deconstruct an application of prod *) let dest_prod_elim (trm : constr) = - let [typ1; typ2; p; proof; arg] = unfold_args trm in - let to_elim = { typ1; typ2 } in - { to_elim; p; proof; arg } + match unfold_args trm with + | [typ1; typ2; p; proof; arg] -> + let to_elim = { typ1; typ2 } in + { to_elim; p; proof; arg } + | _ -> assert false (* * First projection of a prod diff --git a/src/coq/constants/proputils.ml b/src/coq/constants/proputils.ml index ecc32b1..82c5967 100644 --- a/src/coq/constants/proputils.ml +++ b/src/coq/constants/proputils.ml @@ -4,7 +4,6 @@ open Constr open Names -open Apputils let coq_init_logic = ModPath.MPfile @@ -14,7 +13,7 @@ let coq_init_logic = (* Logical or *) let logical_or : types = - mkInd (MutInd.make1 (KerName.make2 coq_init_logic (Label.make "or")), 0) + mkInd (MutInd.make1 (KerName.make coq_init_logic (Label.make "or")), 0) (* left constructor of \/ *) let or_introl : types = @@ -27,7 +26,7 @@ let or_intror : types = (* Logical and *) let logical_and : types = - mkInd (MutInd.make1 (KerName.make2 coq_init_logic (Label.make "and")), 0) + mkInd (MutInd.make1 (KerName.make coq_init_logic (Label.make "and")), 0) (* constructor of /\ *) let conj : types = diff --git a/src/coq/constants/sigmautils.ml b/src/coq/constants/sigmautils.ml index a7ed555..66b1382 100644 --- a/src/coq/constants/sigmautils.ml +++ b/src/coq/constants/sigmautils.ml @@ -14,7 +14,7 @@ let coq_init_specif = (* sigma types *) let sigT : types = - mkInd (MutInd.make1 (KerName.make2 coq_init_specif (Label.make "sigT")), 0) + mkInd (MutInd.make1 (KerName.make coq_init_specif (Label.make "sigT")), 0) (* Introduction for sigma types *) let existT : types = @@ -55,8 +55,10 @@ let pack_existT (app : existT_app) : types = * Deconstruct an existT term *) let dest_existT (trm : types) : existT_app = - let [index_type; packer; index; unpacked] = unfold_args trm in - { index_type; packer; index; unpacked } + match unfold_args trm with + | [index_type; packer; index; unpacked] -> + { index_type; packer; index; unpacked } + | _ -> assert false (* * An application of sigT @@ -77,8 +79,10 @@ let pack_sigT (app : sigT_app) = * Deconsruct a sigT type from a type *) let dest_sigT (typ : types) = - let [index_type; packer] = unfold_args typ in - { index_type; packer } + match unfold_args typ with + | [index_type; packer] -> + { index_type; packer } + | _ -> assert false (* * Build the eta-expansion of a term known to have a sigma type. @@ -116,9 +120,11 @@ let elim_sigT (app : sigT_elim) = * Deconstruct an application of sigT_rect *) let dest_sigT_elim (trm : types) = - let [index_type; packer; packed_type; unpacked; arg] = unfold_args trm in - let to_elim = { index_type ; packer } in - { to_elim; packed_type; unpacked; arg } + match unfold_args trm with + | [index_type; packer; packed_type; unpacked; arg] -> + let to_elim = { index_type ; packer } in + { to_elim; packed_type; unpacked; arg } + | _ -> assert false (* * Left projection of a sigma type diff --git a/src/coq/decompiler/decompiler.ml b/src/coq/decompiler/decompiler.ml index a7c24bd..5af055c 100644 --- a/src/coq/decompiler/decompiler.ml +++ b/src/coq/decompiler/decompiler.ml @@ -36,11 +36,11 @@ let parse_tac_str (s : string) : unit Proofview.tactic = (* Run a coq tactic against a given goal, returning generated subgoals *) let run_tac env sigma (tac : unit Proofview.tactic) (goal : constr) : Goal.goal list * Evd.evar_map = - let p = Proof.start sigma [(env, EConstr.of_constr goal)] in - let (p', _) = Proof.run_tactic env tac p in - let (subgoals, _, _, _, sigma) = Proof.proof p' in - subgoals, sigma - + let p = Proof.start ~name:(destVar goal) ~poly:true sigma [(env, EConstr.of_constr goal)] in + let (p', _, _) = Proof.run_tactic env tac p in + let d = Proof.data p' in + d.goals, d.sigma + (* Returns true if the given tactic solves the goal. *) let solves env sigma (tac : unit Proofview.tactic) (goal : constr) : bool state = try @@ -217,7 +217,9 @@ let rec intros_revert (t : tactical) : tactical = (* Combine common subgoal tactics into semicolons. *) let rec semicolons sigma (t : tactical) : tactical = let first t = match t with - | Compose ( [ tac ], _) -> tac in + | Compose ( [ tac ], _) -> tac + | Compose _ -> assert false + in let subgoals t = match t with | Compose ( _, goals) -> goals in match t with @@ -330,7 +332,7 @@ and try_custom_tacs env sigma get_hints all_opts trm = try let goal = (Typeops.infer env trm).uj_type in let goal_env env sigma g = - let typ = EConstr.to_constr sigma (Goal.V82.abstract_type sigma g) in + let typ = EConstr.to_constr ~abort_on_undefined_evars:false sigma (Goal.V82.abstract_type sigma g) in Zooming.zoom_product_type (Environ.reset_context env) typ in let rec aux opts = match opts with @@ -437,7 +439,7 @@ and exists (f, args) (env, sigma, opts) : tactical option = dot (Exists (env, exT.index)) (first_pass env sigma opts exT.unpacked) (* Value must be a rewrite on a hypothesis in context. *) -and rewrite_in (_, valu, _, body) (env, sigma, opts) : tactical option = +and rewrite_in (name, valu, _, body) (env, sigma, opts) : tactical option = let valu = Reduction.whd_betaiota env valu in try_app valu >>= fun (f, args) -> dest_rewrite (mkApp (f, args)) >>= fun rewr -> @@ -449,7 +451,7 @@ and rewrite_in (_, valu, _, body) (env, sigma, opts) : tactical option = (first_pass env' sigma opts body) (* Value must be an application with last argument in context. *) -and apply_in (n, valu, typ, body) (env, sigma, opts) : tactical option = +and apply_in (name, valu, typ, body) (env, sigma, opts) : tactical option = let valu = Reduction.whd_betaiota env valu in try_app valu >>= fun (f, args) -> let len = Array.length args in @@ -476,13 +478,13 @@ and apply_in (n, valu, typ, body) (env, sigma, opts) : tactical option = (* Last resort decompile let-in as a pose. *) and pose (n, valu, t, body) (env, sigma, opts) : tactical option = - let n' = fresh_name env n in + let n' = fresh_name env (Context.binder_name n) in let env' = push_let_in (Name n', valu, t) env in let decomp_body = first_pass env' sigma opts body in (* If the binding is NEVER used, just skip this. *) if noccurn 1 body then Some decomp_body else dot (Pose (env, valu, n')) (decomp_body) - + (* Decompile a term into its equivalent tactic list. *) let tac_from_term env sigma get_hints trm : tactical = (* Perform second pass to revise greedy tactic list. *) @@ -502,7 +504,9 @@ let bullet level = let blt = match level mod 3 with | 0 -> '*' | 1 -> '-' - | 2 -> '+' in + | 2 -> '+' + | _ -> assert false + in str (String.make num blt) ++ str " " (* Concatenate list of pp.t with separator *) diff --git a/src/coq/devutils/printing.ml b/src/coq/devutils/printing.ml index 51787a2..c0a9663 100644 --- a/src/coq/devutils/printing.ml +++ b/src/coq/devutils/printing.ml @@ -21,10 +21,7 @@ open Contextutils module CRD = Context.Rel.Declaration (* Pretty-print a `global_reference` with fancy `constr` coloring. *) -let pr_global_as_constr gref = - let env = Global.env () in - let sigma = Evd.from_env env in - pr_constr_env env sigma (Universes.constr_of_global gref) +let pr_global_as_constr gref = Printer.pr_global gref (* Using pp, prints directly to a string *) let print_to_string (pp : formatter -> 'a -> unit) (trm : 'a) : string = @@ -61,8 +58,10 @@ let universe_as_string u = (* Gets a sort as a string *) let sort_as_string s = match s with - | Term.Prop _ -> if s = Sorts.prop then "Prop" else "Set" - | Term.Type u -> Printf.sprintf "Type %s" (universe_as_string u) + | Sorts.Prop -> "Prop" + | Sorts.Set -> "Set" + | Sorts.SProp -> "SProp" + | Sorts.Type u -> Printf.sprintf "Type %s" (universe_as_string u) (* Prints a term *) let rec term_as_string (env : env) (trm : types) = @@ -70,7 +69,7 @@ let rec term_as_string (env : env) (trm : types) = | Rel i -> (try let (n, _, _) = CRD.to_tuple @@ lookup_rel i env in - Printf.sprintf "(%s [Rel %d])" (name_as_string n) i + Printf.sprintf "(%s [Rel %d])" (name_as_string (Context.binder_name n)) i with Not_found -> Printf.sprintf "(Unbound_Rel %d)" i) | Var v -> @@ -84,22 +83,22 @@ let rec term_as_string (env : env) (trm : types) = | Prod (n, t, b) -> Printf.sprintf "(Π (%s : %s) . %s)" - (name_as_string n) + (name_as_string (Context.binder_name n)) (term_as_string env t) - (term_as_string (push_local (n, t) env) b) + (term_as_string (push_local (Context.binder_name n, t) env) b) | Lambda (n, t, b) -> Printf.sprintf "(λ (%s : %s) . %s)" - (name_as_string n) + (name_as_string (Context.binder_name n)) (term_as_string env t) - (term_as_string (push_local (n, t) env) b) + (term_as_string (push_local (Context.binder_name n, t) env) b) | LetIn (n, trm, typ, e) -> Printf.sprintf "(let (%s : %s) := %s in %s)" - (name_as_string n) + (name_as_string (Context.binder_name n)) (term_as_string env typ) (term_as_string env trm) - (term_as_string (push_let_in (n, trm, typ) env) e) + (term_as_string (push_let_in (Context.binder_name n, trm, typ) env) e) | App (f, xs) -> Printf.sprintf "(%s %s)" @@ -129,10 +128,10 @@ let rec term_as_string (env : env) (trm : types) = (name_as_string n) (term_as_string env t) (term_as_string env_fix d)) - (Array.to_list ns) + (Array.to_list (Array.map Context.binder_name ns)) (Array.to_list ts) (Array.to_list ds)) - | Case (ci, ct, m, bs) -> + | Case (ci, ct, _, m, bs) -> let (i, i_index) = ci.ci_ind in let mutind_body = lookup_mind i env in let ind_body = mutind_body.mind_packets.(i_index) in @@ -156,6 +155,7 @@ let rec term_as_string (env : env) (trm : types) = Printf.sprintf "(%s)" (print_to_string print_constr trm) | Proj (p, c) -> (* TODO *) Printf.sprintf "(%s)" (print_to_string print_constr trm) + | Int i -> Uint63.to_string i (* Debug a term *) let debug_term (env : env) (trm : types) (descriptor : string) : unit = @@ -180,7 +180,7 @@ let env_as_string (env : env) : string = let (n, b, t) = CRD.to_tuple @@ lookup_rel i env in Printf.sprintf "%s (Rel %d): %s" - (name_as_string n) + (name_as_string (Context.binder_name n)) i (term_as_string (pop_rel_context i env) t)) all_relis) diff --git a/src/coq/devutils/printing.mli b/src/coq/devutils/printing.mli index d4dc67d..fa62803 100644 --- a/src/coq/devutils/printing.mli +++ b/src/coq/devutils/printing.mli @@ -8,7 +8,7 @@ open Evd (* --- Coq terms --- *) (* Pretty-print a `global_reference` with fancy `constr` coloring. *) -val pr_global_as_constr : global_reference -> Pp.t +val pr_global_as_constr : GlobRef.t -> Pp.t (* Gets a name as a string *) val name_as_string : Name.t -> string diff --git a/src/coq/logicutils/contexts/contextutils.ml b/src/coq/logicutils/contexts/contextutils.ml index d44c7cc..4f8f60f 100644 --- a/src/coq/logicutils/contexts/contextutils.ml +++ b/src/coq/logicutils/contexts/contextutils.ml @@ -50,11 +50,19 @@ let named_type decl = CND.get_type decl (* --- Constructing declarations --- *) +(* Get relative context for a name *) +let get_rel_ctx_name name = + match name with (* handle if anon or not *) + | Anonymous -> Context.anonR + | Name idt -> Context.nameR idt + +let get_rel_ctx decl = get_rel_ctx_name (rel_name decl) + (* Make the rel declaration for a local assumption *) -let rel_assum (name, typ) = CRD.LocalAssum (name, typ) +let rel_assum (name, typ) = CRD.LocalAssum (get_rel_ctx_name name, typ) (* Make the rel declaration for a local definition *) -let rel_defin (name, def, typ) = CRD.LocalDef (name, def, typ) +let rel_defin (name, def, typ) = CRD.LocalDef (get_rel_ctx_name name, def, typ) (* Make the named declaration for a local assumption *) let named_assum (id, typ) = CND.LocalAssum (id, typ) @@ -104,7 +112,9 @@ let smash_prod_assum ctxt body = (fun body decl -> match rel_value decl with | Some defn -> Vars.subst1 defn body - | None -> mkProd (rel_name decl, rel_type decl, body)) + | None -> match decl with + | CRD.LocalAssum (a, _) -> mkProd (a, rel_type decl, body) + | CRD.LocalDef (a, _, _) -> mkProd (a, rel_type decl, body)) ~init:body ctxt @@ -117,7 +127,9 @@ let smash_lam_assum ctxt body = (fun body decl -> match rel_value decl with | Some defn -> Vars.subst1 defn body - | None -> mkLambda (rel_name decl, rel_type decl, body)) + | None -> match decl with + | CRD.LocalAssum (a, _) -> mkLambda (a, rel_type decl, body) + | CRD.LocalDef (a, _, _) -> mkLambda (a, rel_type decl, body)) ~init:body ctxt @@ -131,7 +143,7 @@ let decompose_prod_n_zeta n term = if n > 0 then match Constr.kind body with | Prod (name, param, body) -> - aux (n - 1) (Context.Rel.add (rel_assum (name, param)) ctxt) body + aux (n - 1) (Context.Rel.add (rel_assum (Context.binder_name name, param)) ctxt) body | LetIn (name, def_term, def_type, body) -> aux n ctxt (Vars.subst1 def_term body) | _ -> @@ -151,7 +163,7 @@ let decompose_lam_n_zeta n term = if n > 0 then match Constr.kind body with | Lambda (name, param, body) -> - aux (n - 1) (Context.Rel.add (rel_assum (name, param)) ctxt) body + aux (n - 1) (Context.Rel.add (rel_assum (Context.binder_name name, param)) ctxt) body | LetIn (name, def_term, def_type, body) -> Vars.subst1 def_term body |> aux n ctxt | _ -> @@ -200,13 +212,13 @@ let bindings_for_inductive env mutind_body ind_bodies : rel_declaration list = (fun i ind_body -> let name_id = ind_body.mind_typename in let typ = type_of_inductive env i mutind_body in - CRD.LocalAssum (Name name_id, typ)) + CRD.LocalAssum (Context.nameR name_id, typ)) ind_bodies) (* * Fixpoints *) -let bindings_for_fix (names : name array) (typs : types array) : rel_declaration list = +let bindings_for_fix (names : Name.t Context.binder_annot array) (typs : types array) : rel_declaration list = Array.to_list (CArray.map2_i (fun i name typ -> CRD.LocalAssum (name, Vars.lift i typ)) diff --git a/src/coq/logicutils/contexts/contextutils.mli b/src/coq/logicutils/contexts/contextutils.mli index f227051..ba06def 100644 --- a/src/coq/logicutils/contexts/contextutils.mli +++ b/src/coq/logicutils/contexts/contextutils.mli @@ -35,11 +35,15 @@ val define_rel_decl : (* * Construct a named assumption/definition *) -val named_assum : Id.t * 'types -> ('constr, 'types) CND.pt -val named_defin : Id.t * 'constr * 'types -> ('constr, 'types) CND.pt +val named_assum : Id.t Context.binder_annot * 'types -> ('constr, 'types) CND.pt +val named_defin : Id.t Context.binder_annot * 'constr * 'types -> ('constr, 'types) CND.pt (* --- Questions about declarations --- *) +val get_rel_ctx_name : Names.name -> Names.Name.t Context.binder_annot + +val get_rel_ctx : ('constr, 'types) CRD.pt -> Names.Name.t Context.binder_annot + (* * Is the rel declaration a local assumption/definition? *) @@ -133,7 +137,7 @@ val bindings_for_inductive : env -> mutual_inductive_body -> one_inductive_body array -> rel_declaration list val bindings_for_fix : - name array -> types array -> rel_declaration list + Name.t Context.binder_annot array -> types array -> rel_declaration list (* --- Combining contexts --- *) diff --git a/src/coq/logicutils/contexts/envutils.ml b/src/coq/logicutils/contexts/envutils.ml index 3b4ebb5..ff9abe3 100644 --- a/src/coq/logicutils/contexts/envutils.ml +++ b/src/coq/logicutils/contexts/envutils.ml @@ -6,8 +6,6 @@ open Utilities open Environ open Constr open Declarations -open Decl_kinds -open Constrextern open Contextutils open Evd open Names @@ -33,15 +31,15 @@ let lookup_all_rels (env : env) : rel_declaration list = (* Return a name-type pair from the given rel_declaration. *) let rel_name_type rel : Name.t * types = match rel with - | CRD.LocalAssum (n, t) -> (n, t) - | CRD.LocalDef (n, _, t) -> (n, t) + | CRD.LocalAssum (n, t) -> (Context.binder_name n, t) + | CRD.LocalDef (n, _, t) -> (Context.binder_name n, t) (* Push a local binding to an environment *) -let push_local (n, t) = push_rel CRD.(LocalAssum (n, t)) +let push_local (n, t) = push_rel CRD.(LocalAssum (get_rel_ctx_name n, t)) (* Push a let-in definition to an environment *) -let push_let_in (n, e, t) = push_rel CRD.(LocalDef(n, e, t)) +let push_let_in (n, e, t) = push_rel CRD.(LocalDef(get_rel_ctx_name n, e, t)) (* Lookup n rels and remove then *) let lookup_pop (n : int) (env : env) = @@ -53,7 +51,7 @@ let force_constant_body const_body = | Def const_def -> Mod_subst.force_constr const_def | OpaqueDef opaq -> - Opaqueproof.force_proof (Global.opaque_tables ()) opaq + fst (Opaqueproof.force_proof Library.indirect_accessor (Global.opaque_tables ()) opaq) | _ -> CErrors.user_err ~hdr:"force_constant_body" (Pp.str "An axiom has no defining term") diff --git a/src/coq/logicutils/contexts/envutils.mli b/src/coq/logicutils/contexts/envutils.mli index 62cc865..f9817b2 100644 --- a/src/coq/logicutils/contexts/envutils.mli +++ b/src/coq/logicutils/contexts/envutils.mli @@ -27,8 +27,8 @@ val rel_name_type : rel_declaration -> Name.t * types (* * Push to an environment *) -val push_local : (name * types) -> env -> env -val push_let_in : (name * types * types) -> env -> env +val push_local : (Name.t * types) -> env -> env +val push_let_in : (Name.t * types * types) -> env -> env (* * Lookup from an environment diff --git a/src/coq/logicutils/contexts/modutils.ml b/src/coq/logicutils/contexts/modutils.ml index 709ab84..ed179a7 100644 --- a/src/coq/logicutils/contexts/modutils.ml +++ b/src/coq/logicutils/contexts/modutils.ml @@ -25,9 +25,9 @@ let decompose_module_signature mod_sign = * The optional argument specifies functor parameters. *) let declare_module_structure ?(params=[]) ident declare_elements = - let mod_sign = Vernacexpr.Check [] in + let mod_sign = Declaremods.Check [] in let mod_path = - Declaremods.start_module Modintern.interp_module_ast None ident params mod_sign + Declaremods.start_module None ident params mod_sign in Dumpglob.dump_moddef mod_path "mod"; declare_elements mod_path; @@ -55,7 +55,7 @@ let fold_module_structure_by_decl init fold_const fold_ind mod_body = match mod_elem with | SFBconst const_body -> let const = Constant.make2 mod_path label in - if Refset.mem (ConstRef const) globset then + if GlobRef.Set.mem (ConstRef const) globset then (globset, acc) else (globset, fold_const acc const const_body) @@ -63,9 +63,10 @@ let fold_module_structure_by_decl init fold_const fold_ind mod_body = check_inductive_supported mind_body; let ind_body = mind_body.mind_packets.(0) in let ind = (MutInd.make2 mod_path label, 0) in + let env = Global.env () in let globset' = - List.map (Indrec.lookup_eliminator ind) ind_body.mind_kelim |> - List.fold_left (fun gset gref -> Refset.add gref gset) globset + List.map (Indrec.lookup_eliminator env ind) [ind_body.mind_kelim] |> + List.fold_left (fun gset gref -> GlobRef.Set.add gref gset) globset in (globset', fold_ind acc ind (mind_body, ind_body)) | SFBmodule mod_body -> @@ -77,7 +78,7 @@ let fold_module_structure_by_decl init fold_const fold_ind mod_body = Pp.(str "Skipping nested module signature " ++ Label.print label); (globset, acc) in - fold_module_structure_by_elem (Refset.empty, init) fold_mod_elem mod_body |> snd + fold_module_structure_by_elem (GlobRef.Set.empty, init) fold_mod_elem mod_body |> snd (* * Same as `fold_module_structure_by_decl` except a single step function diff --git a/src/coq/logicutils/contexts/modutils.mli b/src/coq/logicutils/contexts/modutils.mli index b1becf4..0ab376e 100644 --- a/src/coq/logicutils/contexts/modutils.mli +++ b/src/coq/logicutils/contexts/modutils.mli @@ -15,7 +15,7 @@ val decompose_module_signature : module_signature -> (Names.MBId.t * module_type * * The optional argument specifies functor parameters. *) -val declare_module_structure : ?params:(Constrexpr.module_ast Declaremods.module_params) -> Id.t -> (ModPath.t -> unit) -> ModPath.t +val declare_module_structure : ?params:(Declaremods.module_params) -> Id.t -> (ModPath.t -> unit) -> ModPath.t (* * Fold over the constant/inductive definitions within a module structure, @@ -24,15 +24,14 @@ val declare_module_structure : ?params:(Constrexpr.module_ast Declaremods.module * * Elimination schemes (e.g., `Ind_rect`) are filtered out from the definitions. *) -val fold_module_structure_by_decl : 'a -> ('a -> Constant.t -> constant_body -> 'a) -> ('a -> inductive -> Inductive.mind_specif -> 'a) -> module_body -> 'a +val fold_module_structure_by_decl : 'a -> ('a -> Names.Constant.t -> Opaqueproof.opaque Declarations.constant_body -> 'a) -> ('a -> Names.MutInd.t * int -> Declarations.mutual_inductive_body * Declarations.one_inductive_body -> 'a) -> 'b Declarations.generic_module_body -> 'a (* * Same as `fold_module_structure_by_decl` except a single step function * accepting a global reference. *) -val fold_module_structure_by_glob : 'a -> ('a -> global_reference -> 'a) -> module_body -> 'a - +val fold_module_structure_by_glob : 'a -> ('a -> Globnames.global_reference -> 'a) -> 'b Declarations.generic_module_body -> 'a (* * Same as `fold_module_structure_by_glob` except an implicit unit accumulator. *) -val iter_module_structure_by_glob : (global_reference -> unit) -> module_body -> unit +val iter_module_structure_by_glob : (Globnames.global_reference -> unit) -> 'a Declarations.generic_module_body -> unit \ No newline at end of file diff --git a/src/coq/logicutils/hofs/debruijn.ml b/src/coq/logicutils/hofs/debruijn.ml index 5820e90..3204cf5 100644 --- a/src/coq/logicutils/hofs/debruijn.ml +++ b/src/coq/logicutils/hofs/debruijn.ml @@ -80,33 +80,6 @@ let shift_by_unconditional (n : int) (trm : types) : types = () trm -(* - * Function from: - * https://github.com/coq/coq/commit/7ada864b7728c9c94b7ca9856b6b2c89feb0214e - * Inlined here to make this compatible with Coq 8.8.0 - * TODO remove with update - *) -let fold_constr_with_binders g f n acc c = - match kind c with - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> acc - | Cast (c,_, t) -> f n (f n acc c) t - | Prod (na,t,c) -> f (g n) (f n acc t) c - | Lambda (na,t,c) -> f (g n) (f n acc t) c - | LetIn (na,b,t,c) -> f (g n) (f n (f n acc b) t) c - | App (c,l) -> Array.fold_left (f n) (f n acc c) l - | Proj (p,c) -> f n acc c - | Evar (_,l) -> Array.fold_left (f n) acc l - | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl - | Fix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g c) n lna tl in - let fd = Array.map2 (fun t b -> (t,b)) tl bl in - Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd - | CoFix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g c) n lna tl in - let fd = Array.map2 (fun t b -> (t,b)) tl bl in - Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd - (* * Gather the set of relative (de Bruijn) variables occurring in the term that * are free (i.e., not bound) under nb levels of external relative binding. diff --git a/src/coq/logicutils/hofs/filters.ml b/src/coq/logicutils/hofs/filters.ml index 585bae3..96d872b 100644 --- a/src/coq/logicutils/hofs/filters.ml +++ b/src/coq/logicutils/hofs/filters.ml @@ -4,7 +4,6 @@ open Constr open Environ open Debruijn open Evd -open Utilities open Checking open Inference open Stateutils diff --git a/src/coq/logicutils/hofs/hofs.ml b/src/coq/logicutils/hofs/hofs.ml index 29bd75a..87ef031 100644 --- a/src/coq/logicutils/hofs/hofs.ml +++ b/src/coq/logicutils/hofs/hofs.ml @@ -5,7 +5,6 @@ open Constr open Contextutils open Envutils open Utilities -open Names open Evd open Stateutils @@ -132,17 +131,6 @@ let map_rec_env_fix map_rec d env (sigma : evar_map) a ns ts (trm : types) = let d_n = List.fold_left (fun a' _ -> d a') a (range 0 n) in map_rec env_fix sigma d_n trm -(* - * Recurse on a mapping function with an environment for a fixpoint - * TODO do we need both of these, or is type system too weak? - *) -let map_rec_env_fix_cartesian (map_rec : ('a, 'b) list_transformer_with_env) d env sigma a ns ts = - let fix_bindings = bindings_for_fix ns ts in - let env_fix = push_rel_context fix_bindings env in - let n = List.length fix_bindings in - let d_n = List.fold_left (fun a' _ -> d a') a (range 0 n) in - map_rec env_fix sigma d_n - (* * TODO explain *) @@ -154,26 +142,26 @@ let map_term_env_rec map_rec f d env sigma a trm = sigma, mkCast (c', k, t') | Prod (n, t, b) -> let sigma, t' = map_rec env sigma a t in - let sigma, b' = map_rec (push_local (n, t) env) sigma (d a) b in + let sigma, b' = map_rec (push_local (Context.binder_name n, t) env) sigma (d a) b in sigma, mkProd (n, t', b') | Lambda (n, t, b) -> let sigma, t' = map_rec env sigma a t in - let sigma, b' = map_rec (push_local (n, t) env) sigma (d a) b in + let sigma, b' = map_rec (push_local (Context.binder_name n, t) env) sigma (d a) b in sigma, mkLambda (n, t', b') | LetIn (n, trm, typ, e) -> let sigma, trm' = map_rec env sigma a trm in let sigma, typ' = map_rec env sigma a typ in - let sigma, e' = map_rec (push_let_in (n, e, typ) env) sigma (d a) e in + let sigma, e' = map_rec (push_let_in (Context.binder_name n, e, typ) env) sigma (d a) e in sigma, mkLetIn (n, trm', typ', e') | App (fu, args) -> let sigma, fu' = map_rec env sigma a fu in let sigma, args' = map_rec_args map_rec env sigma a args in sigma, mkApp (fu', args') - | Case (ci, ct, m, bs) -> + | Case (ci, ct, iv, m, bs) -> let sigma, ct' = map_rec env sigma a ct in let sigma, m' = map_rec env sigma a m in let sigma, bs' = map_rec_args map_rec env sigma a bs in - sigma, mkCase (ci, ct', m', bs') + sigma, mkCase (ci, ct',iv, m', bs') | Fix ((is, i), (ns, ts, ds)) -> let sigma, ts' = map_rec_args map_rec env sigma a ts in let sigma, ds' = map_rec_args (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a ns ts trm) env sigma a ds in (* TODO refactor *) @@ -223,26 +211,26 @@ let map_subterms_env_rec map_rec f d env sigma a trm = sigma, combine_cartesian (fun c' t' -> mkCast (c', k, t')) cs' ts' | Prod (n, t, b) -> let sigma, ts' = map_rec env sigma a t in - let sigma, bs' = map_rec (push_local (n, t) env) sigma (d a) b in + let sigma, bs' = map_rec (push_local (Context.binder_name n, t) env) sigma (d a) b in sigma, combine_cartesian (fun t' b' -> mkProd (n, t', b')) ts' bs' | Lambda (n, t, b) -> let sigma, ts' = map_rec env sigma a t in - let sigma, bs' = map_rec (push_local (n, t) env) sigma (d a) b in + let sigma, bs' = map_rec (push_local (Context.binder_name n, t) env) sigma (d a) b in sigma, combine_cartesian (fun t' b' -> mkLambda (n, t', b')) ts' bs' | LetIn (n, trm, typ, e) -> let sigma, trms' = map_rec env sigma a trm in let sigma, typs' = map_rec env sigma a typ in - let sigma, es' = map_rec (push_let_in (n, e, typ) env) sigma (d a) e in + let sigma, es' = map_rec (push_let_in (Context.binder_name n, e, typ) env) sigma (d a) e in sigma, combine_cartesian (fun trm' (typ', e') -> mkLetIn (n, trm', typ', e')) trms' (cartesian typs' es') | App (fu, args) -> let sigma, fus' = map_rec env sigma a fu in let sigma, argss' = map_rec_args_cartesian map_rec env sigma a args in sigma, combine_cartesian (fun fu' args' -> mkApp (fu', args')) fus' argss' - | Case (ci, ct, m, bs) -> + | Case (ci, ct, iv, m, bs) -> let sigma, cts' = map_rec env sigma a ct in let sigma, ms' = map_rec env sigma a m in let sigma, bss' = map_rec_args_cartesian map_rec env sigma a bs in - sigma, combine_cartesian (fun ct' (m', bs') -> mkCase (ci, ct', m', bs')) cts' (cartesian ms' bss') + sigma, combine_cartesian (fun ct' (m', bs') -> mkCase (ci, ct', iv, m', bs')) cts' (cartesian ms' bss') | Fix ((is, i), (ns, ts, ds)) -> let sigma, tss' = map_rec_args_cartesian map_rec env sigma a ts in let sigma, dss' = map_rec_args_cartesian (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a ns ts trm) env sigma a ds in (* TODO refactor *) @@ -316,16 +304,16 @@ let map_term_env_rec_shallow map_rec f d env sigma a trm = sigma, mkCast (c', k, t') | Prod (n, t, b) -> let sigma, t' = map_rec env sigma a t in - let sigma, b' = map_rec (push_local (n, t) env) sigma (d a) b in + let sigma, b' = map_rec (push_local (Context.binder_name n, t) env) sigma (d a) b in sigma, mkProd (n, t', b') | Lambda (n, t, b) -> let sigma, t' = map_rec env sigma a t in - let sigma, b' = map_rec (push_local (n, t) env) sigma (d a) b in + let sigma, b' = map_rec (push_local (Context.binder_name n, t) env) sigma (d a) b in sigma, mkLambda (n, t', b') | LetIn (n, trm, typ, e) -> let sigma, trm' = map_rec env sigma a trm in let sigma, typ' = map_rec env sigma a typ in - let sigma, e' = map_rec (push_let_in (n, e, typ) env) sigma (d a) e in + let sigma, e' = map_rec (push_let_in (Context.binder_name n, e, typ) env) sigma (d a) e in sigma, mkLetIn (n, trm', typ', e') | App (fu, args) -> let sigma, fu' = map_rec env sigma a fu in @@ -334,11 +322,11 @@ let map_term_env_rec_shallow map_rec f d env sigma a trm = if isLambda t then sigma, t else map_rec env sigma a t in map_rec_args map_rec_shallow env sigma a args in sigma, mkApp (fu', args') - | Case (ci, ct, m, bs) -> + | Case (ci, ct, iv, m, bs) -> let sigma, ct' = map_rec env sigma a ct in let sigma, m' = map_rec env sigma a m in let sigma, bs' = map_rec_args map_rec env sigma a bs in - sigma, mkCase (ci, ct', m', bs') + sigma, mkCase (ci, ct', iv, m', bs') | Fix ((is, i), (ns, ts, ds)) -> let sigma, ts' = map_rec_args map_rec env sigma a ts in let sigma, ds' = map_rec_args (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a ns ts trm) env sigma a ds in (* TODO refactor *) @@ -495,22 +483,22 @@ let rec map_term_env_if_list p f d env sigma a trm = List.append c' t' | Prod (n, t, b) -> let t' = map_rec env sigma a t in - let b' = map_rec (push_local (n, t) env) sigma (d a) b in + let b' = map_rec (push_local (Context.binder_name n, t) env) sigma (d a) b in List.append t' b' | Lambda (n, t, b) -> let t' = map_rec env sigma a t in - let b' = map_rec (push_local (n, t) env) sigma (d a) b in + let b' = map_rec (push_local (Context.binder_name n, t) env) sigma (d a) b in List.append t' b' | LetIn (n, trm, typ, e) -> let trm' = map_rec env sigma a trm in let typ' = map_rec env sigma a typ in - let e' = map_rec (push_let_in (n, e, typ) env) sigma (d a) e in + let e' = map_rec (push_let_in (Context.binder_name n, e, typ) env) sigma (d a) e in List.append trm' (List.append typ' e') | App (fu, args) -> let fu' = map_rec env sigma a fu in let args' = Array.map (map_rec env sigma a) args in List.append fu' (List.flatten (Array.to_list args')) - | Case (ci, ct, m, bs) -> + | Case (ci, ct, iv, m, bs) -> let ct' = map_rec env sigma a ct in let m' = map_rec env sigma a m in let bs' = Array.map (map_rec env sigma a) bs in @@ -580,22 +568,22 @@ let rec exists_subterm_env p d env sigma (a : 'a) (trm : types) : evar_map * boo sigma, c' || t' | Prod (n, t, b) -> let sigma, t' = map_rec env sigma a t in - let sigma, b' = map_rec (push_local (n, t) env) sigma (d a) b in + let sigma, b' = map_rec (push_local (Context.binder_name n, t) env) sigma (d a) b in sigma, t' || b' | Lambda (n, t, b) -> let sigma, t' = map_rec env sigma a t in - let sigma, b' = map_rec (push_local (n, t) env) sigma (d a) b in + let sigma, b' = map_rec (push_local (Context.binder_name n, t) env) sigma (d a) b in sigma, t' || b' | LetIn (n, trm, typ, e) -> let sigma, trm' = map_rec env sigma a trm in let sigma, typ' = map_rec env sigma a typ in - let sigma, e' = map_rec (push_let_in (n, e, typ) env) sigma (d a) e in + let sigma, e' = map_rec (push_let_in (Context.binder_name n, e, typ) env) sigma (d a) e in sigma, trm' || typ' || e' | App (fu, args) -> let sigma, fu' = map_rec env sigma a fu in let sigma, args' = exists_args map_rec env sigma a args in sigma, fu' || args' - | Case (ci, ct, m, bs) -> + | Case (ci, ct, iv, m, bs) -> let sigma, ct' = map_rec env sigma a ct in let sigma, m' = map_rec env sigma a m in let sigma, bs' = exists_args map_rec env sigma a bs in diff --git a/src/coq/logicutils/hofs/hofs.mli b/src/coq/logicutils/hofs/hofs.mli index 5269b52..6fedd07 100644 --- a/src/coq/logicutils/hofs/hofs.mli +++ b/src/coq/logicutils/hofs/hofs.mli @@ -98,7 +98,7 @@ type ('a, 'b) proposition_list_mapper = val map_rec_env_fix : (env -> evar_map -> 'a -> types -> 'b state) -> ('a -> 'a) -> - (env -> evar_map -> 'a -> Names.name array -> types array -> types -> 'b state) + (env -> evar_map -> 'a -> Names.Name.t Context.binder_annot array -> types array -> types -> 'b state) val map_rec_args : ('a, 'b) transformer_with_env -> diff --git a/src/coq/logicutils/hofs/reducers.ml b/src/coq/logicutils/hofs/reducers.ml index 1b0b3ca..4e0e644 100644 --- a/src/coq/logicutils/hofs/reducers.ml +++ b/src/coq/logicutils/hofs/reducers.ml @@ -18,25 +18,25 @@ type stateless_reducer = env -> evar_map -> types -> types (* Default reducer *) let reduce_term (env : env) (sigma : evar_map) (trm : types) = - sigma, EConstr.to_constr + sigma, EConstr.to_constr ~abort_on_undefined_evars:false sigma (Reductionops.nf_betaiotazeta env sigma (EConstr.of_constr trm)) (* Delta reduction *) let delta (env : env) (sigma : evar_map) (trm : types) = - sigma, EConstr.to_constr + sigma, EConstr.to_constr ~abort_on_undefined_evars:false sigma (Reductionops.whd_delta env sigma (EConstr.of_constr trm)) (* Weak head reduction *) let whd (env : env) (sigma : evar_map) (trm : types) = - sigma, EConstr.to_constr + sigma, EConstr.to_constr ~abort_on_undefined_evars:false sigma (Reductionops.whd_all env sigma (EConstr.of_constr trm)) (* nf_all *) let reduce_nf (env : env) (sigma : evar_map) (trm : types) = - sigma, EConstr.to_constr + sigma, EConstr.to_constr ~abort_on_undefined_evars:false sigma (Reductionops.nf_all env sigma (EConstr.of_constr trm)) @@ -105,22 +105,22 @@ let reduce_remove_identities : reducer = (* Reduce and also unfold definitions *) let reduce_unfold (env : env) sigma (trm : types) = - sigma, EConstr.to_constr + sigma, EConstr.to_constr ~abort_on_undefined_evars:false sigma (Reductionops.nf_all env sigma (EConstr.of_constr trm)) (* Reduce and also unfold definitions, but weak head *) let reduce_unfold_whd (env : env) sigma (trm : types) = - sigma, EConstr.to_constr + sigma, EConstr.to_constr ~abort_on_undefined_evars:false sigma (Reductionops.whd_all env sigma (EConstr.of_constr trm)) (* Weak-head reduce a term if it is a let-in *) let reduce_whd_if_let_in (env : env) sigma (trm : types) = if isLetIn trm then - sigma, EConstr.to_constr + sigma, EConstr.to_constr ~abort_on_undefined_evars:false sigma - (Reductionops.whd_betaiotazeta sigma (EConstr.of_constr trm)) + (Reductionops.whd_betaiotazeta env sigma (EConstr.of_constr trm)) else sigma, trm diff --git a/src/coq/logicutils/hofs/substitution.ml b/src/coq/logicutils/hofs/substitution.ml index f4f0e2e..f72c5bb 100644 --- a/src/coq/logicutils/hofs/substitution.ml +++ b/src/coq/logicutils/hofs/substitution.ml @@ -117,7 +117,7 @@ let all_typ_substs_combs : (types * types) comb_substitution = (* --- Substituting global references --- *) -type global_substitution = global_reference Globnames.Refmap.t +type global_substitution = GlobRef.t Names.GlobRef.Map.t (* Substitute global references throughout a term *) let rec subst_globals subst (term : constr) = @@ -126,17 +126,17 @@ let rec subst_globals subst (term : constr) = (fun _ t -> try pglobal_of_constr t |> - map_puniverses (flip Globnames.Refmap.find subst) |> + map_puniverses (flip Names.GlobRef.Map.find subst) |> constr_of_pglobal with _ -> match kind t with - | Case (ci, p, b, bl) -> + | Case (ci, p, iv, b, bl) -> let ci_ind' = destInd (subst_globals subst (mkInd ci.ci_ind)) in let ci' = { ci with ci_ind = fst ci_ind' } in let b' = subst_globals subst b in let p' = subst_globals subst p in let bl' = Array.map (subst_globals subst) bl in - mkCase (ci', p', b', bl') + mkCase (ci', p', iv, b', bl') | _ -> t) (fun _ -> ()) () diff --git a/src/coq/logicutils/hofs/substitution.mli b/src/coq/logicutils/hofs/substitution.mli index 205bcf4..f80e284 100644 --- a/src/coq/logicutils/hofs/substitution.mli +++ b/src/coq/logicutils/hofs/substitution.mli @@ -76,7 +76,7 @@ val all_typ_substs_combs : (types * types) comb_substitution (* --- Substituting global references (TODO unify w/ above after cleaning types) --- *) -type global_substitution = global_reference Globnames.Refmap.t +type global_substitution = GlobRef.t Names.GlobRef.Map.t (* Substitute global references throughout a term *) val subst_globals : global_substitution -> constr -> constr diff --git a/src/coq/logicutils/hofs/zooming.ml b/src/coq/logicutils/hofs/zooming.ml index 722b554..c1e49a9 100644 --- a/src/coq/logicutils/hofs/zooming.ml +++ b/src/coq/logicutils/hofs/zooming.ml @@ -10,7 +10,6 @@ open Envutils open Contextutils open Debruijn open Sigmautils -open Evd open Names (* --- Zooming --- *) @@ -22,7 +21,7 @@ let rec zoom_n_prod env npm typ : env * types = else match kind typ with | Prod (n1, t1, b1) -> - zoom_n_prod (push_local (n1, t1) env) (npm - 1) b1 + zoom_n_prod (push_local (Context.binder_name n1, t1) env) (npm - 1) b1 | _ -> failwith "more parameters expected" @@ -35,7 +34,7 @@ let zoom_n_lambda env npm trm : env * types = let rec zoom_lambda_term (env : env) (trm : types) : env * types = match kind trm with | Lambda (n, t, b) -> - zoom_lambda_term (push_local (n, t) env) b + zoom_lambda_term (push_local (Context.binder_name n, t) env) b | _ -> (env, trm) @@ -43,7 +42,7 @@ let rec zoom_lambda_term (env : env) (trm : types) : env * types = let rec zoom_product_type (env : env) (typ : types) : env * types = match kind typ with | Prod (n, t, b) -> - zoom_product_type (push_local (n, t) env) b + zoom_product_type (push_local (Context.binder_name n, t) env) b | _ -> (env, typ) @@ -56,7 +55,7 @@ let zoom_lambda_names env except trm : env * types * Id.t list = | limit -> match kind trm with | Lambda (n, t, b) -> - let name = fresh_name env n in + let name = fresh_name env (Context.binder_name n) in let env' = push_local (Name name, t) env in let env, trm, names = aux env' (limit - 1) b in diff --git a/src/coq/logicutils/inductive/indexing.ml b/src/coq/logicutils/inductive/indexing.ml index b01d640..9746731 100644 --- a/src/coq/logicutils/inductive/indexing.ml +++ b/src/coq/logicutils/inductive/indexing.ml @@ -10,7 +10,6 @@ open Hofimpls open Reducers open Sigmautils open Apputils -open Evd (* --- Generic functions --- *) diff --git a/src/coq/logicutils/inductive/indutils.ml b/src/coq/logicutils/inductive/indutils.ml index c8c1b5b..585da88 100644 --- a/src/coq/logicutils/inductive/indutils.ml +++ b/src/coq/logicutils/inductive/indutils.ml @@ -31,7 +31,7 @@ let check_inductive_supported mutind_body : unit = let inductive_of_elim (env : env) (pc : pconstant) : MutInd.t option = let (c, u) = pc in let kn = Constant.canonical c in - let (modpath, dirpath, label) = KerName.repr kn in + let (modpath, label) = KerName.repr kn in let rec try_find_ind is_rev = try let label_string = Label.to_string label in @@ -42,7 +42,7 @@ let inductive_of_elim (env : env) (pc : pconstant) : MutInd.t option = if (suffix = "_ind" || suffix = "_rect" || suffix = "_rec" || suffix = "_ind_r") then let ind_label_string = String.sub label_string 0 split_index in let ind_label = Label.of_id (Id.of_string_soft ind_label_string) in - let ind_name = MutInd.make1 (KerName.make modpath dirpath ind_label) in + let ind_name = MutInd.make1 (KerName.make modpath ind_label) in let _ = lookup_mind ind_name env in Some ind_name else @@ -56,7 +56,7 @@ let inductive_of_elim (env : env) (pc : pconstant) : MutInd.t option = else None in try_find_ind false - + (* * Get the number of constructors for an inductive type * @@ -78,7 +78,8 @@ let is_elim (env : env) (trm : types) = (* Lookup the eliminator over the type sort *) let type_eliminator (env : env) (ind : inductive) = - Universes.constr_of_global (Indrec.lookup_eliminator ind InType) + UnivGen.constr_of_monomorphic_global (Indrec.lookup_eliminator env ind Sorts.InType) +[@@ocaml.warning "-3"] (* TODO handle univ poly eliminator *) (* Applications of eliminators *) type elim_app = @@ -125,9 +126,9 @@ let rec num_ihs env sigma rec_typ typ = let t_red = reduce_stateless reduce_term env sigma t in if is_or_applies rec_typ t_red then let (n_b_t, b_t, b_b) = destProd b in - 1 + num_ihs (push_local (n, t) (push_local (n_b_t, b_t) env)) sigma rec_typ b_b + 1 + num_ihs (push_local (Context.binder_name n, t) (push_local (Context.binder_name n_b_t, b_t) env)) sigma rec_typ b_b else - num_ihs (push_local (n, t) env) sigma rec_typ b + num_ihs (push_local (Context.binder_name n, t) env) sigma rec_typ b | _ -> 0 @@ -142,49 +143,34 @@ let arity_of_ind_body ind_body = match ind_body.mind_arity with | RegularArity { mind_user_arity; mind_sort } -> mind_user_arity - | TemplateArity { template_param_levels; template_level } -> + | TemplateArity { template_level } -> let sort = Constr.mkType template_level in recompose_prod_assum ind_body.mind_arity_ctxt sort -(* Create an Entries.local_entry from a Rel.Declaration.t *) -let make_ind_local_entry decl = - let entry = - match decl with - | CRD.LocalAssum (_, typ) -> Entries.LocalAssumEntry typ - | CRD.LocalDef (_, term, _) -> Entries.LocalDefEntry term - in - match CRD.get_name decl with - | Name.Name id -> (id, entry) - | Name.Anonymous -> failwith "Parameters to an inductive type may not be anonymous" (* Instantiate an abstract universe context *) let inst_abs_univ_ctx abs_univ_ctx = (* Note that we're creating *globally* fresh universe levels. *) - Universes.fresh_instance_from_context abs_univ_ctx |> Univ.UContext.make + let instance, (_, constr) = UnivGen.fresh_instance abs_univ_ctx in + Univ.UContext.make (instance, constr) (* Instantiate an abstract_inductive_universes into an Entries.inductive_universes with Univ.UContext.t (TODO do we do something with evar_map here?) *) let make_ind_univs_entry = function - | Monomorphic_ind univ_ctx_set -> + | Declarations.Monomorphic uctx_set -> let univ_ctx = Univ.UContext.empty in - (Entries.Monomorphic_ind_entry univ_ctx_set, univ_ctx) - | Polymorphic_ind abs_univ_ctx -> - let univ_ctx = inst_abs_univ_ctx abs_univ_ctx in - (Entries.Polymorphic_ind_entry univ_ctx, univ_ctx) - | Cumulative_ind abs_univ_cumul -> - let abs_univ_ctx = Univ.ACumulativityInfo.univ_context abs_univ_cumul in - let univ_ctx = inst_abs_univ_ctx abs_univ_ctx in - let univ_var = Univ.ACumulativityInfo.variance abs_univ_cumul in - let univ_cumul = Univ.CumulativityInfo.make (univ_ctx, univ_var) in - (Entries.Cumulative_ind_entry univ_cumul, univ_ctx) + (Entries.Monomorphic_entry uctx_set, univ_ctx) + | Declarations.Polymorphic auctx -> + let univ_ctx = inst_abs_univ_ctx auctx in + (Entries.Polymorphic_entry (Univ.AUContext.names auctx, univ_ctx), univ_ctx) let open_inductive ?(global=false) env (mind_body, ind_body) = let univs, univ_ctx = make_ind_univs_entry mind_body.mind_universes in let subst_univs = Vars.subst_instance_constr (Univ.UContext.instance univ_ctx) in let env = Environ.push_context univ_ctx env in if global then - Global.push_context false univ_ctx; + Global.push_context_set ~strict:false (Univ.ContextSet.of_context univ_ctx); let arity = arity_of_ind_body ind_body in - let arity_ctx = [CRD.LocalAssum (Name.Anonymous, arity)] in + let arity_ctx = [CRD.LocalAssum (get_rel_ctx_name Name.Anonymous, arity)] in let ctors_typ = Array.map (recompose_prod_assum arity_ctx) ind_body.mind_user_lc in env, univs, subst_univs arity, Array.map_to_list subst_univs ctors_typ @@ -195,20 +181,19 @@ let declare_inductive typename consnames template univs nparam arity constypes = let ind_entry = { mind_entry_typename = typename; mind_entry_arity = arity; - mind_entry_template = template; mind_entry_consnames = consnames; mind_entry_lc = List.map snd constypes } in let mind_entry = { mind_entry_record = None; + mind_entry_variance = None; mind_entry_finite = Declarations.Finite; - mind_entry_params = List.map make_ind_local_entry params; + mind_entry_params = params; mind_entry_inds = [ind_entry]; mind_entry_universes = univs; - mind_entry_private = None } + mind_entry_private = None; + mind_entry_template = template; + } in - let ((_, ker_name), _) = Declare.declare_mind mind_entry in - let mind = MutInd.make1 ker_name in - let ind = (mind, 0) in - Indschemes.declare_default_schemes mind; - ind + let mind = DeclareInd.declare_mutual_inductive_with_eliminations mind_entry UnivNames.empty_binders [] in + (mind, 0) diff --git a/src/coq/logicutils/inductive/indutils.mli b/src/coq/logicutils/inductive/indutils.mli index 502e99b..b4ae13d 100644 --- a/src/coq/logicutils/inductive/indutils.mli +++ b/src/coq/logicutils/inductive/indutils.mli @@ -71,7 +71,7 @@ val arity_of_ind_body : one_inductive_body -> types * levels and constraints. A descriptor for the inductive type's universe * properties is also returned. *) -val open_inductive : ?global:bool -> env -> Inductive.mind_specif -> env * Entries.inductive_universes * types * types list +val open_inductive : ?global:bool -> env -> Inductive.mind_specif -> env * Entries.universes_entry * types * types list (* * Declare a new inductive type in the global environment. Note that the arity @@ -79,5 +79,4 @@ val open_inductive : ?global:bool -> env -> Inductive.mind_specif -> env * Entri * a recursive reference and then all parameters (i.e., * forall (I : arity) (P : params), ...). *) -val declare_inductive : Id.t -> Id.t list -> bool -> Entries.inductive_universes -> int -> types -> types list -> inductive - +val declare_inductive : Id.t -> Id.t list -> bool -> Entries.universes_entry -> int -> types -> types list -> inductive diff --git a/src/coq/logicutils/transformation/transform.ml b/src/coq/logicutils/transformation/transform.ml index 1a786ad..bdccdf3 100644 --- a/src/coq/logicutils/transformation/transform.ml +++ b/src/coq/logicutils/transformation/transform.ml @@ -15,6 +15,7 @@ open Indutils open Substitution open Stateutils open Recordops +open Record (* Type-sensitive transformation of terms *) type constr_transformer = env -> evar_map -> constr -> evar_map * constr @@ -28,7 +29,7 @@ let force_constant_body const_body = | Def const_def -> Mod_subst.force_constr const_def | OpaqueDef opaq -> - Opaqueproof.force_proof (Global.opaque_tables ()) opaq + fst (Opaqueproof.force_proof Library.indirect_accessor (Global.opaque_tables ()) opaq) | _ -> CErrors.user_err ~hdr:"force_constant_body" (Pp.str "An axiom has no defining term") @@ -43,9 +44,9 @@ let force_constant_body const_body = let transform_constant ident tr_constr const_body = let env = match const_body.const_universes with - | Monomorphic_const univs -> + | Monomorphic univs -> Global.env () |> Environ.push_context_set univs - | Polymorphic_const univs -> + | Polymorphic univs -> CErrors.user_err ~hdr:"transform_constant" Pp.(str "Universe polymorphism is not supported") in @@ -53,7 +54,7 @@ let transform_constant ident tr_constr const_body = let sigma = Evd.from_env env in let sigma, term' = tr_constr env sigma term in let sigma, type' = tr_constr env sigma const_body.const_type in - sigma, Globnames.destConstRef (define_term ~typ:type' ident sigma term' true) + sigma, Globnames.destConstRef (define_term ~typ:type' ident sigma term') (* * Declare a new inductive family under the given name with the transformed type @@ -96,13 +97,25 @@ let try_register_record mod_path (ind, ind') = r.s_PROJ in (try - declare_structure (ind', (ind', 1), pks, ps) + Record.Internal.declare_structure_entry {s_CONST = (ind',1); s_EXPECTEDPARAM = r.s_EXPECTEDPARAM; s_PROJKIND = pks; s_PROJ = ps} with _ -> Feedback.msg_warning (Pp.str "Failed to register projections for transformed record")) with Not_found -> () +let lookup_eliminator_error_handling ind sorts = + (* Feedback.msg_warning (Pp.(str "start ")); *) + let env = Global.env () in + List.filter_map (fun x -> x) + (List.map + (fun x -> + try Some (x, Indrec.lookup_eliminator env ind x) + with + | _ -> None + ) + sorts) + (* * Declare a new module structure under the given name with the compositionally * transformed (i.e., forward-substituted) components from the given module @@ -117,7 +130,7 @@ let try_register_record mod_path (ind, ind') = * * TODO sigma handling, not sure how to do it here/if we need it *) -let transform_module_structure ?(init=const Globnames.Refmap.empty) ?(opaques=Globnames.Refset.empty) ident tr_constr mod_body = +let transform_module_structure ?(init=const GlobRef.Map.empty) ?(opaques=GlobRef.Set.empty) ident tr_constr mod_body = let open Modutils in let mod_path = mod_body.mod_mp in let mod_arity, mod_elems = decompose_module_signature mod_body.mod_type in @@ -127,7 +140,7 @@ let transform_module_structure ?(init=const Globnames.Refmap.empty) ?(opaques=Gl match b with | SFBconst const_body -> let const = Constant.make2 mod_path l in - not (Globnames.Refset.mem (ConstRef const) opaques) + not (GlobRef.Set.mem (GlobRef.ConstRef const) opaques) | _ -> true) mod_elems @@ -141,24 +154,32 @@ let transform_module_structure ?(init=const Globnames.Refmap.empty) ?(opaques=Gl match body with | SFBconst const_body -> let const = Constant.make2 mod_path label in - if Globnames.Refmap.mem (ConstRef const) subst then + if GlobRef.Map.mem (ConstRef const) subst then subst (* Do not transform schematic definitions. *) else let sigma, const' = transform_constant ident tr_constr const_body in - Globnames.Refmap.add (ConstRef const) (ConstRef const') subst + GlobRef.Map.add (ConstRef const) (ConstRef const') subst | SFBmind mind_body -> check_inductive_supported mind_body; let ind = (MutInd.make2 mod_path label, 0) in let ind_body = mind_body.mind_packets.(0) in let sigma, ind' = transform_inductive ident tr_constr (mind_body, ind_body) in try_register_record mod_path' (ind, ind'); + let subst = GlobRef.Map.add (IndRef ind) (IndRef ind') subst in let ncons = Array.length ind_body.mind_consnames in let list_cons ind = List.init ncons (fun i -> ConstructRef (ind, i + 1)) in - let sorts = ind_body.mind_kelim in - let list_elim ind = List.map (Indrec.lookup_eliminator ind) sorts in - Globnames.Refmap.add (IndRef ind) (IndRef ind') subst |> - List.fold_right2 Globnames.Refmap.add (list_cons ind) (list_cons ind') |> - List.fold_right2 Globnames.Refmap.add (list_elim ind) (list_elim ind') + let sorts = List.map Sorts.family [Sorts.sprop; Sorts.prop; Sorts.set; Sorts.type1] in + let list_elim ind = lookup_eliminator_error_handling ind sorts in + let list_elim_ind = list_elim ind in + let list_elim_ind' = list_elim ind' in + let list_elim_ind_sorts = List.map fst list_elim_ind in + let list_elim_ind'_sorts = List.map fst list_elim_ind' in + let common_sorts = List.filter (fun x -> List.exists (fun y -> Sorts.family_equal x y) list_elim_ind_sorts) list_elim_ind'_sorts in + let list_elim_ind_winnowed = List.map snd (List.filter (fun (x, y) -> List.exists (fun z -> Sorts.family_equal x z) common_sorts) list_elim_ind) in + let list_elim_ind'_winnowed = List.map snd (List.filter (fun (x, y) -> List.exists (fun z -> Sorts.family_equal x z) common_sorts) list_elim_ind') in + GlobRef.Map.add (IndRef ind) (IndRef ind') subst |> + List.fold_right2 GlobRef.Map.add (list_cons ind) (list_cons ind') |> + List.fold_right2 GlobRef.Map.add (list_elim_ind_winnowed) (list_elim_ind'_winnowed) | SFBmodule mod_body -> Feedback.msg_warning (Pp.str "Skipping nested module structure"); subst diff --git a/src/coq/logicutils/transformation/transform.mli b/src/coq/logicutils/transformation/transform.mli index 68c42f1..79b32ab 100644 --- a/src/coq/logicutils/transformation/transform.mli +++ b/src/coq/logicutils/transformation/transform.mli @@ -20,7 +20,7 @@ type constr_transformer = env -> evar_map -> constr -> evar_map * constr * NOTE: Global side effects. *) val transform_constant : - Id.t -> constr_transformer -> constant_body -> evar_map * Constant.t + Id.t -> constr_transformer -> Opaqueproof.opaque constant_body -> evar_map * Constant.t (* * Declare a new inductive family under the given name with the transformed type @@ -45,4 +45,4 @@ val transform_inductive : * NOTE: Global side effects. *) val transform_module_structure : - ?init:(unit -> global_substitution) -> ?opaques:(Globnames.Refset.t) -> Id.t -> constr_transformer -> module_body -> ModPath.t + ?init:(unit -> global_substitution) -> ?opaques:(Names.GlobRef.Set.t) -> Id.t -> constr_transformer -> module_body -> ModPath.t diff --git a/src/coq/logicutils/typesandequality/convertibility.ml b/src/coq/logicutils/typesandequality/convertibility.ml index 8b1a854..c50b46e 100644 --- a/src/coq/logicutils/typesandequality/convertibility.ml +++ b/src/coq/logicutils/typesandequality/convertibility.ml @@ -4,7 +4,6 @@ open Constr open Contextutils -open Utilities open Environ open Evd open Inference diff --git a/src/coq/logicutils/typesandequality/inference.ml b/src/coq/logicutils/typesandequality/inference.ml index 31af8fe..91a1b02 100644 --- a/src/coq/logicutils/typesandequality/inference.ml +++ b/src/coq/logicutils/typesandequality/inference.ml @@ -2,25 +2,19 @@ * Type inference *) -open Environ -open Evd open Constr open Declarations (* Safely infer the WHNF type of a term, updating the evar map *) let infer_type env sigma term = - let sigma_ref = ref sigma in let eterm = EConstr.of_constr term in - let typ = Typing.e_type_of ~refresh:true env sigma_ref eterm in - let sigma = ! sigma_ref in - sigma, EConstr.to_constr sigma typ + let sigma, typ = Typing.type_of ~refresh:true env sigma eterm in + sigma, EConstr.to_constr ~abort_on_undefined_evars:false sigma typ (* Safely infer the sort of a type, updating the evar map *) let infer_sort env sigma term = - let sigma_ref = ref sigma in let eterm = EConstr.of_constr term in - let sort = Typing.e_sort_of env sigma_ref eterm in - let sigma = ! sigma_ref in + let sigma, sort = Typing.sort_of env sigma eterm in sigma, Sorts.family sort (* Get the type of an inductive type (TODO do we need evar_map here?) *) @@ -30,4 +24,4 @@ let type_of_inductive env index mutind_body : types = let univs = Declareops.inductive_polymorphic_context mutind_body in let univ_instance = Univ.make_abstract_instance univs in let mutind_spec = (mutind_body, ind_body) in - Inductive.type_of_inductive env (mutind_spec, univ_instance) + Inductive.type_of_inductive (mutind_spec, univ_instance) diff --git a/src/coq/representationutils/defutils.ml b/src/coq/representationutils/defutils.ml index a18b343..b369d42 100644 --- a/src/coq/representationutils/defutils.ml +++ b/src/coq/representationutils/defutils.ml @@ -5,8 +5,6 @@ open Constr open Names open Evd -open Decl_kinds -open Recordops open Constrexpr open Constrextern @@ -15,7 +13,7 @@ open Constrextern (* https://github.com/ybertot/plugin_tutorials/blob/master/tuto1/src/simple_declare.ml TODO do we need to return the updated evar_map? *) -let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook refresh = +let edeclare ident poly ~opaque sigma udecl body tyopt imps hook = let open EConstr in (* XXX: "Standard" term construction combinators such as `mkApp` don't add any universe constraints that may be needed later for @@ -33,48 +31,39 @@ let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook re canonical structure resolution and what not. *) let env = Global.env () in - let sigma = - if refresh then - fst (Typing.type_of ~refresh:false env sigma body) - else - sigma + let sigma = fst (Typing.type_of env sigma body) in let sigma = - if Option.has_some tyopt && refresh then - fst (Typing.type_of ~refresh:false env sigma (Option.get tyopt)) + if Option.has_some tyopt then + fst (Typing.type_of env sigma (Option.get tyopt)) else sigma - in - let sigma = Evd.minimize_universes sigma in - let body = to_constr sigma body in - let tyopt = Option.map (to_constr sigma) tyopt in - let uvars_fold uvars c = - Univ.LSet.union uvars (Univops.universes_of_constr c) in - let uvars = List.fold_left uvars_fold Univ.LSet.empty - (Option.List.cons tyopt [body]) in - let sigma = Evd.restrict_universe_context sigma uvars in - let univs = Evd.check_univ_decl ~poly sigma udecl in - let ubinders = Evd.universe_binders sigma in - let ce = Declare.definition_entry ?types:tyopt ~univs body in - DeclareDef.declare_definition ident k ce ubinders imps hook + in + let sigma = Evd.minimize_universes sigma in (* todo: is this necessary/bad? *) + let udecl = UState.default_univ_decl in + let sigma = (Evd.fold_undefined (fun x _ sigma -> Evd.remove sigma x) sigma) sigma in + let scope = Locality.Global Locality.ImportDefaultBehavior in + let kind = Decls.(IsDefinition Definition) in + let info = Declare.Info.make ~scope ~kind ~udecl ~poly () in + let cinfo = Declare.CInfo.make ~name:ident ~typ:tyopt () in + Declare.declare_definition ~info:info ~cinfo:cinfo ~opaque:opaque ~body:body sigma (* Define a new Coq term *) -let define_term ?typ (n : Id.t) (evm : evar_map) (trm : types) (refresh : bool) = - let k = (Global, Flags.is_universe_polymorphism(), Definition) in +let define_term ?typ (n : Id.t) (evm : evar_map) (trm : types) = + let poly = Attributes.is_universe_polymorphism() in let udecl = UState.default_univ_decl in - let nohook = Lemmas.mk_hook (fun _ x -> x) in let etrm = EConstr.of_constr trm in let etyp = Option.map EConstr.of_constr typ in - edeclare n k ~opaque:false evm udecl etrm etyp [] nohook refresh + edeclare n poly ~opaque:false evm udecl etrm etyp [] None (* Define a Canonical Structure *) -let define_canonical ?typ (n : Id.t) (evm : evar_map) (trm : types) (refresh : bool) = - let k = (Global, Flags.is_universe_polymorphism (), CanonicalStructure) in +let define_canonical ?typ (n : Id.t) (evm : evar_map) (trm : types) = + let poly = Attributes.is_universe_polymorphism() in let udecl = UState.default_univ_decl in - let hook = Lemmas.mk_hook (fun _ x -> declare_canonical_structure x; x) in + let hook = Declare.Hook.make (fun x -> let open Declare.Hook.S in Canonical.declare_canonical_structure x.dref) in let etrm = EConstr.of_constr trm in let etyp = Option.map EConstr.of_constr typ in - edeclare n k ~opaque:false evm udecl etrm etyp [] hook refresh + edeclare n poly ~opaque:false evm udecl etrm etyp [] (Some hook) (* --- Converting between representations --- *) @@ -85,21 +74,22 @@ let define_canonical ?typ (n : Id.t) (evm : evar_map) (trm : types) (refresh : b (* Intern a term (for now, ignore the resulting evar_map) *) let intern env sigma t : evar_map * types = let (sigma, trm) = Constrintern.interp_constr_evars env sigma t in - sigma, EConstr.to_constr sigma trm + sigma, EConstr.to_constr ~abort_on_undefined_evars:false sigma trm (* Extern a term *) let extern env sigma t : constr_expr = - Constrextern.extern_constr true env sigma (EConstr.of_constr t) + Constrextern.extern_constr ~lax:true env sigma (EConstr.of_constr t) (* Construct the external expression for a definition *) -let expr_of_global (g : global_reference) : constr_expr = +let expr_of_global (g : GlobRef.t) : constr_expr = let r = extern_reference Id.Set.empty g in CAst.make @@ (CAppExpl ((None, r, None), [])) (* Convert a term into a global reference with universes (or raise Not_found) *) let pglobal_of_constr term = + let open GlobRef in match Constr.kind term with - | Const (const, univs) -> Globnames.ConstRef const, univs + | Const (const, univs) -> ConstRef const, univs | Ind (ind, univs) -> IndRef ind, univs | Construct (cons, univs) -> ConstructRef cons, univs | Var id -> VarRef id, Univ.Instance.empty @@ -107,15 +97,14 @@ let pglobal_of_constr term = (* Convert a global reference with universes into a term *) let constr_of_pglobal (glob, univs) = + let open GlobRef in match glob with - | Globnames.ConstRef const -> mkConstU (const, univs) + | ConstRef const -> mkConstU (const, univs) | IndRef ind -> mkIndU (ind, univs) | ConstructRef cons -> mkConstructU (cons, univs) | VarRef id -> mkVar id (* Safely instantiate a global reference, with proper universe handling *) let new_global sigma gref = - let sigma_ref = ref sigma in - let glob = Evarutil.e_new_global sigma_ref gref in - let sigma = ! sigma_ref in - sigma, EConstr.to_constr sigma glob + let sigma, typ = Evarutil.new_global sigma gref in + sigma, EConstr.to_constr ~abort_on_undefined_evars:false sigma typ diff --git a/src/coq/representationutils/defutils.mli b/src/coq/representationutils/defutils.mli index 84cfc2e..509802f 100644 --- a/src/coq/representationutils/defutils.mli +++ b/src/coq/representationutils/defutils.mli @@ -16,13 +16,12 @@ open Constrexpr * (Refreshing universes is REALLY costly) *) val define_term : - ?typ:types -> Id.t -> evar_map -> types -> bool -> global_reference - + ?typ:types -> Id.t -> evar_map -> types -> GlobRef.t (* * Like define_term, but for a canonical structure *) val define_canonical : - ?typ:types -> Id.t -> evar_map -> types -> bool -> global_reference + ?typ:types -> Id.t -> evar_map -> types -> GlobRef.t (* --- Converting between representations --- *) @@ -55,19 +54,19 @@ val extern : env -> evar_map -> types -> constr_expr (* * Construct the external expression for a definition. *) -val expr_of_global : global_reference -> constr_expr +val expr_of_global : GlobRef.t -> constr_expr (* * Convert a term into a global reference with universes (or raise Not_found) *) -val pglobal_of_constr : constr -> global_reference Univ.puniverses +val pglobal_of_constr : constr -> GlobRef.t Univ.puniverses (* * Convert a global reference with universes into a term *) -val constr_of_pglobal : global_reference Univ.puniverses -> constr +val constr_of_pglobal : GlobRef.t Univ.puniverses -> constr (* * Safely instantiate a global reference, updating the evar map *) -val new_global : evar_map -> global_reference -> evar_map * constr +val new_global : evar_map -> GlobRef.t -> evar_map * constr diff --git a/src/coq/representationutils/nameutils.ml b/src/coq/representationutils/nameutils.ml index 9432148..cf72370 100644 --- a/src/coq/representationutils/nameutils.ml +++ b/src/coq/representationutils/nameutils.ml @@ -2,7 +2,6 @@ * Utilities for names, references, and identifiers *) -open Constr open Names open Util diff --git a/src/coq/termutils/constutils.ml b/src/coq/termutils/constutils.ml index 4a8e384..69f1e2b 100644 --- a/src/coq/termutils/constutils.ml +++ b/src/coq/termutils/constutils.ml @@ -3,7 +3,6 @@ *) open Constr -open Environ open Names (* --- Constructing constants --- *) @@ -18,8 +17,10 @@ let make_constant id = * Safely extract the body of a constant, instantiating any universe variables *) let open_constant env const = - let (Some (term, auctx)) = Global.body_of_constant const in - let uctx = Universes.fresh_instance_from_context auctx |> Univ.UContext.make in - let term = Vars.subst_instance_constr (Univ.UContext.instance uctx) term in - let env = Environ.push_context uctx env in - env, term + match Global.body_of_constant Library.indirect_accessor const with + | (Some (term, _, auctx)) -> + let (uinst, uctxset) = UnivGen.fresh_instance auctx in + let uctx = Univ.UContext.make (uinst, (Univ.ContextSet.constraints uctxset)) in + let term = Vars.subst_instance_constr (Univ.UContext.instance uctx) term in + let env = Environ.push_context uctx env in env, term + | None -> failwith "Constant extraction failed" diff --git a/src/dune b/src/dune new file mode 100644 index 0000000..abd1224 --- /dev/null +++ b/src/dune @@ -0,0 +1,10 @@ +(library + (name example_plugin) + (wrapped false) + (public_name my-plugin.plugin) + (synopsis "Coq Plugin library") + (flags :standard -rectypes -w -3-8-27-28-33) + (libraries coq.plugins.ltac)) + +(include_subdirs unqualified) +(coq.pp (modules plib)) \ No newline at end of file diff --git a/src/plib.mlg b/src/plib.mlg new file mode 100644 index 0000000..355877c --- /dev/null +++ b/src/plib.mlg @@ -0,0 +1 @@ +DECLARE PLUGIN "example_plugin" diff --git a/src/plib.mlpack b/src/plib.mlpack deleted file mode 100644 index 2d376a0..0000000 --- a/src/plib.mlpack +++ /dev/null @@ -1,47 +0,0 @@ -Utilities - -Apputils -Constutils -Funutils - -Defutils -Nameutils - -Inference -Convertibility -Checking - -Equtils -Sigmautils -Produtils -Idutils -Proputils - -Stateutils -Envutils -Contextutils - -Hofs -Debruijn -Hofimpls -Substitution -Reducers -Typehofs -Filters -Zooming -Hypotheses -Filters - -Indexing -Indutils - -Modutils - -Transform - -Printing - -Decompiler - -Plibrary - diff --git a/src/plibrary.ml4 b/src/plibrary.ml4 deleted file mode 100644 index 197773c..0000000 --- a/src/plibrary.ml4 +++ /dev/null @@ -1 +0,0 @@ -DECLARE PLUGIN "plib" diff --git a/src/utilities/utilities.ml b/src/utilities/utilities.ml index 2d54096..425565e 100644 --- a/src/utilities/utilities.ml +++ b/src/utilities/utilities.ml @@ -136,13 +136,7 @@ let combine_cartesian_append (al : 'a list array) : 'a array list = (* Map3 *) -let rec map3 (f : 'a -> 'b -> 'c -> 'd) l1 l2 l3 : 'd list = - match (l1, l2, l3) with - | ([], [], []) -> - [] - | (h1 :: t1, h2 :: t2, h3 :: t3) -> - let r = f h1 h2 h3 in r :: map3 f t1 t2 t3 - +let map3 = CList.map3 (* * Creates a list of the range of min to max, excluding max * This is an auxiliary function renamed from seq in template-coq diff --git a/synth.opam b/synth.opam new file mode 100644 index 0000000..e69de29 diff --git a/theories/Plib.v b/theories/Plib.v deleted file mode 100644 index 87e32df..0000000 --- a/theories/Plib.v +++ /dev/null @@ -1 +0,0 @@ -Declare ML Module "plib". diff --git a/theories/Test.v b/theories/Test.v new file mode 100644 index 0000000..4f750b2 --- /dev/null +++ b/theories/Test.v @@ -0,0 +1 @@ +Declare ML Module "example_plugin". diff --git a/theories/dune b/theories/dune new file mode 100644 index 0000000..8dbda55 --- /dev/null +++ b/theories/dune @@ -0,0 +1,4 @@ +(coq.theory + (name MyPlugin) + (package my-plugin) + (plugins my-plugin.plugin)) \ No newline at end of file