From 25b372fbacf43bf65d7956e59b1a239fe7deadd7 Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Thu, 20 Jul 2023 16:55:44 -0500 Subject: [PATCH 01/44] Move build to dune. --- _CoqProject | 97 ------------------------------------------------ build.sh | 2 - dune-project | 1 + src/dune | 9 +++++ src/plib.mlpack | 47 ----------------------- src/plibrary.ml4 | 1 - synth.opam | 0 7 files changed, 10 insertions(+), 147 deletions(-) delete mode 100644 _CoqProject delete mode 100755 build.sh create mode 100644 dune-project create mode 100644 src/dune delete mode 100644 src/plib.mlpack delete mode 100644 src/plibrary.ml4 create mode 100644 synth.opam 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..0a32580 --- /dev/null +++ b/dune-project @@ -0,0 +1 @@ +(lang dune 3.6) diff --git a/src/dune b/src/dune new file mode 100644 index 0000000..422abf1 --- /dev/null +++ b/src/dune @@ -0,0 +1,9 @@ +(library + (name termutils) + (wrapped false) + (public_name synth.termutils) + (synopsis "Termutils library") + (flags :standard -rectypes -w -3-8-27-28-33) + (libraries coq.plugins.ltac)) + +(include_subdirs unqualified) 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/synth.opam b/synth.opam new file mode 100644 index 0000000..e69de29 From 60c6de8788cbb78939db940bcf131fd0aa889293 Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Thu, 20 Jul 2023 17:31:05 -0500 Subject: [PATCH 02/44] Fixed type errors, still some remaining. --- .gitignore | 1 + src/coq/devutils/printing.ml | 25 +++++----- src/coq/devutils/printing.mli | 2 +- src/coq/logicutils/contexts/modutils.mli | 4 +- src/coq/logicutils/hofs/hofs.ml | 46 +++++++++---------- src/coq/logicutils/hofs/substitution.ml | 2 +- src/coq/logicutils/hofs/substitution.mli | 2 +- src/coq/logicutils/hofs/zooming.ml | 8 ++-- .../logicutils/typesandequality/inference.ml | 10 +--- src/coq/representationutils/defutils.mli | 12 ++--- 10 files changed, 52 insertions(+), 60 deletions(-) diff --git a/.gitignore b/.gitignore index bc89608..3cdf6d4 100644 --- a/.gitignore +++ b/.gitignore @@ -23,3 +23,4 @@ plugin/Makefile plugin/.merlin *.out _opam +_build/ diff --git a/src/coq/devutils/printing.ml b/src/coq/devutils/printing.ml index 51787a2..99cac13 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 = @@ -70,7 +67,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 +81,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)" @@ -119,7 +116,7 @@ let rec term_as_string (env : env) (trm : types) = let name_id = (ind_bodies.(i_index)).mind_typename in Id.to_string name_id | Fix ((is, i), (ns, ts, ds)) -> - let env_fix = push_rel_context (bindings_for_fix ns ds) env in + let env_fix = push_rel_context (bindings_for_fix (Array.map Context.binder_name ns) ds) env in String.concat " with " (map3 @@ -129,7 +126,7 @@ 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) -> @@ -180,7 +177,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..e90a439 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 : Globnames.global_reference -> Pp.t (* Gets a name as a string *) val name_as_string : Name.t -> string diff --git a/src/coq/logicutils/contexts/modutils.mli b/src/coq/logicutils/contexts/modutils.mli index b1becf4..fdb1aaa 100644 --- a/src/coq/logicutils/contexts/modutils.mli +++ b/src/coq/logicutils/contexts/modutils.mli @@ -30,9 +30,9 @@ val fold_module_structure_by_decl : 'a -> ('a -> Constant.t -> constant_body -> * 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) -> 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) -> module_body -> unit diff --git a/src/coq/logicutils/hofs/hofs.ml b/src/coq/logicutils/hofs/hofs.ml index 29bd75a..fb6227f 100644 --- a/src/coq/logicutils/hofs/hofs.ml +++ b/src/coq/logicutils/hofs/hofs.ml @@ -154,16 +154,16 @@ 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 @@ -176,11 +176,11 @@ let map_term_env_rec map_rec f d env sigma a trm = sigma, mkCase (ci, ct', 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 *) + let sigma, ds' = map_rec_args (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a (Array.map Context.binder_name ns) ts trm) env sigma a ds in (* TODO refactor *) sigma, mkFix ((is, i), (ns, ts', ds')) | CoFix (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 *) + let sigma, ds' = map_rec_args (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a (Array.map Context.binder_name ns) ts trm) env sigma a ds in (* TODO refactor *) sigma, mkCoFix (i, (ns, ts', ds')) | Proj (p, c) -> let sigma, c' = map_rec env sigma a c in @@ -223,16 +223,16 @@ 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 @@ -245,11 +245,11 @@ let map_subterms_env_rec map_rec f d env sigma a trm = sigma, combine_cartesian (fun ct' (m', bs') -> mkCase (ci, ct', 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 *) + let sigma, dss' = map_rec_args_cartesian (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a (Array.map Context.binder_name ns) ts trm) env sigma a ds in (* TODO refactor *) sigma, combine_cartesian (fun ts' ds' -> mkFix ((is, i), (ns, ts', ds'))) tss' dss' | CoFix (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 *) + let sigma, dss' = map_rec_args_cartesian (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a (Array.map Context.binder_name ns) ts trm) env sigma a ds in (* TODO refactor *) sigma, combine_cartesian (fun ts' ds' -> mkCoFix (i, (ns, ts', ds'))) tss' dss' | Proj (p, c) -> let sigma, cs' = map_rec env sigma a c in @@ -316,16 +316,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 @@ -341,11 +341,11 @@ let map_term_env_rec_shallow map_rec f d env sigma a trm = sigma, mkCase (ci, ct', 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 *) + let sigma, ds' = map_rec_args (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a (Array.map Context.binder_name ns) ts trm) env sigma a ds in (* TODO refactor *) sigma, mkFix ((is, i), (ns, ts', ds')) | CoFix (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 *) + let sigma, ds' = map_rec_args (fun env sigma a trm -> map_rec_env_fix map_rec d env sigma a (Array.map Context.binder_name ns) ts trm) env sigma a ds in (* TODO refactor *) sigma, mkCoFix (i, (ns, ts', ds')) | Proj (p, c) -> let sigma, c' = map_rec env sigma a c in @@ -495,16 +495,16 @@ 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 @@ -517,11 +517,11 @@ let rec map_term_env_if_list p f d env sigma a trm = List.append ct' (List.append m' (List.flatten (Array.to_list bs'))) | Fix ((is, i), (ns, ts, ds)) -> let ts' = Array.map (map_rec env sigma a) ts in - let ds' = Array.map (map_rec_env_fix map_rec d env sigma a ns ts) ds in + let ds' = Array.map (map_rec_env_fix map_rec d env sigma a (Array.map Context.binder_name ns) ts) ds in List.append (List.flatten (Array.to_list ts')) (List.flatten (Array.to_list ds')) | CoFix (i, (ns, ts, ds)) -> let ts' = Array.map (map_rec env sigma a) ts in - let ds' = Array.map (map_rec_env_fix map_rec d env sigma a ns ts) ds in + let ds' = Array.map (map_rec_env_fix map_rec d env sigma a (Array.map Context.binder_name ns) ts) ds in List.append (List.flatten (Array.to_list ts')) (List.flatten (Array.to_list ds')) | Proj (pr, c) -> map_rec env sigma a c @@ -580,16 +580,16 @@ 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 diff --git a/src/coq/logicutils/hofs/substitution.ml b/src/coq/logicutils/hofs/substitution.ml index f4f0e2e..52683fe 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 = Globnames.global_reference Globnames.Refmap.t (* Substitute global references throughout a term *) let rec subst_globals subst (term : constr) = diff --git a/src/coq/logicutils/hofs/substitution.mli b/src/coq/logicutils/hofs/substitution.mli index 205bcf4..e921f38 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 = Globnames.global_reference Globnames.Refmap.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..72624d1 100644 --- a/src/coq/logicutils/hofs/zooming.ml +++ b/src/coq/logicutils/hofs/zooming.ml @@ -22,7 +22,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 +35,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 +43,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 +56,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/typesandequality/inference.ml b/src/coq/logicutils/typesandequality/inference.ml index 31af8fe..477154e 100644 --- a/src/coq/logicutils/typesandequality/inference.ml +++ b/src/coq/logicutils/typesandequality/inference.ml @@ -9,19 +9,13 @@ 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 + Typing.type_of ~refresh:true env sigma eterm (* 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 - sigma, Sorts.family sort + Typing.sort_of env sigma eterm (* Get the type of an inductive type (TODO do we need evar_map here?) *) let type_of_inductive env index mutind_body : types = diff --git a/src/coq/representationutils/defutils.mli b/src/coq/representationutils/defutils.mli index 84cfc2e..7d485db 100644 --- a/src/coq/representationutils/defutils.mli +++ b/src/coq/representationutils/defutils.mli @@ -16,13 +16,13 @@ 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 -> bool -> Globnames.global_reference (* * 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 -> bool -> Globnames.global_reference (* --- Converting between representations --- *) @@ -55,19 +55,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 : Globnames.global_reference -> 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 -> Globnames.global_reference Univ.puniverses (* * Convert a global reference with universes into a term *) -val constr_of_pglobal : global_reference Univ.puniverses -> constr +val constr_of_pglobal : Globnames.global_reference 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 -> Globnames.global_reference -> evar_map * constr From 6e33a0a1ddafa0576880c888c3b9f390f44cae6f Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Fri, 21 Jul 2023 14:08:52 -0500 Subject: [PATCH 03/44] Fixed type errors, still some remaining. --- src/coq/logicutils/contexts/envutils.ml | 4 +-- src/coq/logicutils/hofs/hofs.ml | 4 +-- src/coq/logicutils/inductive/indutils.ml | 31 +++++++++--------------- src/coq/representationutils/defutils.ml | 14 ++++------- 4 files changed, 20 insertions(+), 33 deletions(-) diff --git a/src/coq/logicutils/contexts/envutils.ml b/src/coq/logicutils/contexts/envutils.ml index 3b4ebb5..5be88cc 100644 --- a/src/coq/logicutils/contexts/envutils.ml +++ b/src/coq/logicutils/contexts/envutils.ml @@ -33,8 +33,8 @@ 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 *) diff --git a/src/coq/logicutils/hofs/hofs.ml b/src/coq/logicutils/hofs/hofs.ml index fb6227f..1044294 100644 --- a/src/coq/logicutils/hofs/hofs.ml +++ b/src/coq/logicutils/hofs/hofs.ml @@ -136,12 +136,12 @@ let map_rec_env_fix map_rec d env (sigma : evar_map) a ns ts (trm : types) = * 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 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 + map_rec env_fix sigma d_n *) (* * TODO explain diff --git a/src/coq/logicutils/inductive/indutils.ml b/src/coq/logicutils/inductive/indutils.ml index c8c1b5b..040e640 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,7 @@ 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_global (Indrec.lookup_eliminator ind InType) (* Applications of eliminators *) type elim_app = @@ -146,16 +146,6 @@ let arity_of_ind_body ind_body = 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 = @@ -164,13 +154,13 @@ let inst_abs_univ_ctx abs_univ_ctx = (* 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 -> + | Entries.Monomorphic_entry univ_ctx_set -> let univ_ctx = Univ.UContext.empty in (Entries.Monomorphic_ind_entry univ_ctx_set, univ_ctx) - | Polymorphic_ind abs_univ_ctx -> + | Entries.Polymorphic_entry 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 -> + | Entries.Cumulative_ind_entry 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 @@ -182,7 +172,7 @@ let open_inductive ?(global=false) env (mind_body, ind_body) = 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 false univ_ctx; let arity = arity_of_ind_body ind_body in let arity_ctx = [CRD.LocalAssum (Name.Anonymous, arity)] in let ctors_typ = Array.map (recompose_prod_assum arity_ctx) ind_body.mind_user_lc in @@ -202,10 +192,11 @@ let declare_inductive typename consnames template univs nparam arity constypes = let mind_entry = { mind_entry_record = 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_variance = None } in let ((_, ker_name), _) = Declare.declare_mind mind_entry in let mind = MutInd.make1 ker_name in diff --git a/src/coq/representationutils/defutils.ml b/src/coq/representationutils/defutils.ml index a18b343..ce1d0ae 100644 --- a/src/coq/representationutils/defutils.ml +++ b/src/coq/representationutils/defutils.ml @@ -56,11 +56,11 @@ let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook re 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 + DeclareDef.declare_definition ~ontop:None ~hook_data:hook ident k ce ubinders imps (* 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 k = (Global, Attributes.is_universe_polymorphism(), Definition) in let udecl = UState.default_univ_decl in let nohook = Lemmas.mk_hook (fun _ x -> x) in let etrm = EConstr.of_constr trm in @@ -69,7 +69,7 @@ let define_term ?typ (n : Id.t) (evm : evar_map) (trm : types) (refresh : bool) (* 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 k = (Global, Attributes.is_universe_polymorphism (), CanonicalStructure) in let udecl = UState.default_univ_decl in let hook = Lemmas.mk_hook (fun _ x -> declare_canonical_structure x; x) in let etrm = EConstr.of_constr trm in @@ -92,7 +92,7 @@ let extern env sigma t : constr_expr = Constrextern.extern_constr 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 : Globnames.global_reference) : constr_expr = let r = extern_reference Id.Set.empty g in CAst.make @@ (CAppExpl ((None, r, None), [])) @@ -114,8 +114,4 @@ let constr_of_pglobal (glob, 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 new_global sigma gref = Evarutil.new_global sigma gref From 1ac206115ab4c921bec6c15eb247eec8f0f1a19e Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Mon, 24 Jul 2023 11:49:22 -0500 Subject: [PATCH 04/44] Fixed type errors, still some remaining. --- src/coq/logicutils/inductive/indutils.ml | 14 ++++---------- src/coq/logicutils/inductive/indutils.mli | 5 ++--- src/coq/logicutils/transformation/transform.ml | 13 +++++-------- 3 files changed, 11 insertions(+), 21 deletions(-) diff --git a/src/coq/logicutils/inductive/indutils.ml b/src/coq/logicutils/inductive/indutils.ml index 040e640..e675334 100644 --- a/src/coq/logicutils/inductive/indutils.ml +++ b/src/coq/logicutils/inductive/indutils.ml @@ -156,19 +156,13 @@ let inst_abs_univ_ctx abs_univ_ctx = let make_ind_univs_entry = function | Entries.Monomorphic_entry univ_ctx_set -> let univ_ctx = Univ.UContext.empty in - (Entries.Monomorphic_ind_entry univ_ctx_set, univ_ctx) - | Entries.Polymorphic_entry abs_univ_ctx -> + (Entries.Monomorphic_entry univ_ctx_set, univ_ctx) + | Entries.Polymorphic_entry (name_array, abs_univ_ctx) -> let univ_ctx = inst_abs_univ_ctx abs_univ_ctx in - (Entries.Polymorphic_ind_entry univ_ctx, univ_ctx) - | Entries.Cumulative_ind_entry 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.Polymorphic_entry (name_array, 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 univs, univ_ctx = make_ind_univs_entry mind_body 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 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..ae5971b 100644 --- a/src/coq/logicutils/transformation/transform.ml +++ b/src/coq/logicutils/transformation/transform.ml @@ -43,9 +43,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 @@ -89,14 +89,11 @@ let try_register_record mod_path (ind, ind') = try let r = lookup_structure ind in Feedback.msg_info (Pp.str "Transformed a record"); + let con = r.s_CONST in let pks = r.s_PROJKIND in - let ps = - List.map - (Option.map (fun p -> Constant.make2 mod_path (Constant.label p))) - r.s_PROJ - in + let ps = r.s_PROJ in (try - declare_structure (ind', (ind', 1), pks, ps) + declare_structure (con, pks, ps) with _ -> Feedback.msg_warning (Pp.str "Failed to register projections for transformed record")) From 816cdee75dd1d967a0109a7996c3d00de0606a03 Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Mon, 24 Jul 2023 14:34:47 -0500 Subject: [PATCH 05/44] Fixed type errors, still some remaining. --- src/coq/decompiler/decompiler.ml | 4 ++-- src/coq/logicutils/contexts/modutils.ml | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/coq/decompiler/decompiler.ml b/src/coq/decompiler/decompiler.ml index a7c24bd..e57324d 100644 --- a/src/coq/decompiler/decompiler.ml +++ b/src/coq/decompiler/decompiler.ml @@ -36,7 +36,7 @@ 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.start ~name:(Names.Id.of_string "placeholder") ~poly:true 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 @@ -476,7 +476,7 @@ 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. *) diff --git a/src/coq/logicutils/contexts/modutils.ml b/src/coq/logicutils/contexts/modutils.ml index 709ab84..dbc68ca 100644 --- a/src/coq/logicutils/contexts/modutils.ml +++ b/src/coq/logicutils/contexts/modutils.ml @@ -25,7 +25,7 @@ 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 in From 858443e74db00acef0467e870c4880b0cc5760cd Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Tue, 25 Jul 2023 12:57:58 -0500 Subject: [PATCH 06/44] Fixed type errors, still some remaining. --- src/coq/decompiler/decompiler.ml | 10 ++++---- src/coq/devutils/printing.ml | 6 ++--- src/coq/logicutils/contexts/envutils.mli | 4 ++-- src/coq/logicutils/hofs/hofs.ml | 30 ++++++++++++------------ src/coq/logicutils/hofs/zooming.ml | 8 +++---- 5 files changed, 29 insertions(+), 29 deletions(-) diff --git a/src/coq/decompiler/decompiler.ml b/src/coq/decompiler/decompiler.ml index e57324d..b9da7ed 100644 --- a/src/coq/decompiler/decompiler.ml +++ b/src/coq/decompiler/decompiler.ml @@ -437,19 +437,19 @@ 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 -> try_rel rewr.px >>= fun idx -> guard (noccurn (idx + 1) body) >>= fun _ -> let n, t = rel_name_type (lookup_rel idx env) in - let env' = push_local (n, t) env in + let env' = push_local (Context.make_annot n (Context.binder_relevance name), t) env in dot (RewriteIn (env, rewr.eq, rewr.px, rewr.left)) (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 @@ -458,7 +458,7 @@ and apply_in (n, valu, typ, body) (env, sigma, opts) : tactical option = guard (noccurn (idx + 1) body) >>= fun _ -> (* H does not occur in body *) guard (not (noccurn 1 body)) >>= fun _ -> (* new binding DOES occur *) let n, t = rel_name_type (lookup_rel idx env) in (* "H" *) - let env' = push_local (n, t) env in (* change type of "H" *) + let env' = push_local (Context.make_annot n (Context.binder_relevance name), t) env in (* change type of "H" *) let prf = mkApp (f, Array.sub args 0 (len - 1)) in (* let H2 := f H1 := H2 ... *) let apply_binding app_in (_, sigma) = @@ -477,7 +477,7 @@ 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 (Context.binder_name n) in - let env' = push_let_in (Name n', valu, t) env in + let env' = push_let_in (Context.make_annot (Name n') (Context.binder_relevance 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 diff --git a/src/coq/devutils/printing.ml b/src/coq/devutils/printing.ml index 99cac13..f9ee7e9 100644 --- a/src/coq/devutils/printing.ml +++ b/src/coq/devutils/printing.ml @@ -83,20 +83,20 @@ let rec term_as_string (env : env) (trm : types) = "(Π (%s : %s) . %s)" (name_as_string (Context.binder_name n)) (term_as_string env t) - (term_as_string (push_local (Context.binder_name n, t) env) b) + (term_as_string (push_local (n, t) env) b) | Lambda (n, t, b) -> Printf.sprintf "(λ (%s : %s) . %s)" (name_as_string (Context.binder_name n)) (term_as_string env t) - (term_as_string (push_local (Context.binder_name n, t) env) b) + (term_as_string (push_local (n, t) env) b) | LetIn (n, trm, typ, e) -> Printf.sprintf "(let (%s : %s) := %s in %s)" (name_as_string (Context.binder_name n)) (term_as_string env typ) (term_as_string env trm) - (term_as_string (push_let_in (Context.binder_name n, trm, typ) env) e) + (term_as_string (push_let_in (n, trm, typ) env) e) | App (f, xs) -> Printf.sprintf "(%s %s)" diff --git a/src/coq/logicutils/contexts/envutils.mli b/src/coq/logicutils/contexts/envutils.mli index 62cc865..cd9b871 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 Context.binder_annot * types) -> env -> env +val push_let_in : (name Context.binder_annot * types * types) -> env -> env (* * Lookup from an environment diff --git a/src/coq/logicutils/hofs/hofs.ml b/src/coq/logicutils/hofs/hofs.ml index 1044294..4ff5058 100644 --- a/src/coq/logicutils/hofs/hofs.ml +++ b/src/coq/logicutils/hofs/hofs.ml @@ -154,16 +154,16 @@ 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 (Context.binder_name n, t) env) sigma (d a) b in + let sigma, b' = map_rec (push_local (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 (Context.binder_name n, t) env) sigma (d a) b in + let sigma, b' = map_rec (push_local (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 (Context.binder_name n, e, typ) env) sigma (d a) e in + let sigma, e' = map_rec (push_let_in (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 @@ -223,16 +223,16 @@ 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 (Context.binder_name n, t) env) sigma (d a) b in + let sigma, bs' = map_rec (push_local (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 (Context.binder_name n, t) env) sigma (d a) b in + let sigma, bs' = map_rec (push_local (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 (Context.binder_name n, e, typ) env) sigma (d a) e in + let sigma, es' = map_rec (push_let_in (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 @@ -316,16 +316,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 (Context.binder_name n, t) env) sigma (d a) b in + let sigma, b' = map_rec (push_local (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 (Context.binder_name n, t) env) sigma (d a) b in + let sigma, b' = map_rec (push_local (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 (Context.binder_name n, e, typ) env) sigma (d a) e in + let sigma, e' = map_rec (push_let_in (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 @@ -495,16 +495,16 @@ 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 (Context.binder_name n, t) env) sigma (d a) b in + let b' = map_rec (push_local (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 (Context.binder_name n, t) env) sigma (d a) b in + let b' = map_rec (push_local (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 (Context.binder_name n, e, typ) env) sigma (d a) e in + let e' = map_rec (push_let_in (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 @@ -580,16 +580,16 @@ 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 (Context.binder_name n, t) env) sigma (d a) b in + let sigma, b' = map_rec (push_local (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 (Context.binder_name n, t) env) sigma (d a) b in + let sigma, b' = map_rec (push_local (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 (Context.binder_name n, e, typ) env) sigma (d a) e in + let sigma, e' = map_rec (push_let_in (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 diff --git a/src/coq/logicutils/hofs/zooming.ml b/src/coq/logicutils/hofs/zooming.ml index 72624d1..67ce5d3 100644 --- a/src/coq/logicutils/hofs/zooming.ml +++ b/src/coq/logicutils/hofs/zooming.ml @@ -22,7 +22,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 (Context.binder_name n1, t1) env) (npm - 1) b1 + zoom_n_prod (push_local (n1, t1) env) (npm - 1) b1 | _ -> failwith "more parameters expected" @@ -35,7 +35,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 (Context.binder_name n, t) env) b + zoom_lambda_term (push_local (n, t) env) b | _ -> (env, trm) @@ -43,7 +43,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 (Context.binder_name n, t) env) b + zoom_product_type (push_local (n, t) env) b | _ -> (env, typ) @@ -57,7 +57,7 @@ let zoom_lambda_names env except trm : env * types * Id.t list = match kind trm with | Lambda (n, t, b) -> let name = fresh_name env (Context.binder_name n) in - let env' = push_local (Name name, t) env in + let env' = push_local (Context.make_annot (Name name) (Context.binder_relevance n), t) env in let env, trm, names = aux env' (limit - 1) b in (env, trm, name :: names) From 19e5b26957c3962e37cedc369355f48d7a382cf0 Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Tue, 25 Jul 2023 14:45:54 -0500 Subject: [PATCH 07/44] Fixed type errors, still some remaining. --- src/coq/devutils/printing.ml | 2 +- src/coq/logicutils/contexts/contextutils.ml | 19 ++++++++++++------- src/coq/logicutils/contexts/contextutils.mli | 6 +++--- src/coq/logicutils/hofs/hofs.ml | 16 ++++++++-------- src/coq/logicutils/hofs/hofs.mli | 2 +- 5 files changed, 25 insertions(+), 20 deletions(-) diff --git a/src/coq/devutils/printing.ml b/src/coq/devutils/printing.ml index f9ee7e9..cd86380 100644 --- a/src/coq/devutils/printing.ml +++ b/src/coq/devutils/printing.ml @@ -116,7 +116,7 @@ let rec term_as_string (env : env) (trm : types) = let name_id = (ind_bodies.(i_index)).mind_typename in Id.to_string name_id | Fix ((is, i), (ns, ts, ds)) -> - let env_fix = push_rel_context (bindings_for_fix (Array.map Context.binder_name ns) ds) env in + let env_fix = push_rel_context (bindings_for_fix ns ds) env in String.concat " with " (map3 diff --git a/src/coq/logicutils/contexts/contextutils.ml b/src/coq/logicutils/contexts/contextutils.ml index d44c7cc..2daeabd 100644 --- a/src/coq/logicutils/contexts/contextutils.ml +++ b/src/coq/logicutils/contexts/contextutils.ml @@ -57,10 +57,10 @@ let rel_assum (name, typ) = CRD.LocalAssum (name, typ) let rel_defin (name, def, typ) = CRD.LocalDef (name, def, typ) (* Make the named declaration for a local assumption *) -let named_assum (id, typ) = CND.LocalAssum (id, typ) +let named_assum (id, typ) = CND.LocalAssum (Context.annotR id, typ) (* Make the named declaration for a local definition *) -let named_defin (id, def, typ) = CND.LocalDef (id, def, typ) +let named_defin (id, def, typ) = CND.LocalDef (Context.annotR id, def, typ) (* * Instantiate a local assumption as a local definition, using the provided term @@ -71,7 +71,8 @@ let named_defin (id, def, typ) = CND.LocalDef (id, def, typ) *) let define_rel_decl body decl = assert (is_rel_assum decl); - rel_defin (rel_name decl, body, rel_type decl) + match decl with + | CRD.LocalAssum (a, _) -> rel_defin (a, body, rel_type decl) (* --- Mapping over contexts --- *) @@ -104,7 +105,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 +120,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 @@ -200,13 +205,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 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..59dd6e0 100644 --- a/src/coq/logicutils/contexts/contextutils.mli +++ b/src/coq/logicutils/contexts/contextutils.mli @@ -20,8 +20,8 @@ module CND = Context.Named.Declaration (* * Construct a local assumption/definition *) -val rel_assum : Name.t * 'types -> ('constr, 'types) CRD.pt -val rel_defin : Name.t * 'constr * 'types -> ('constr, 'types) CRD.pt +val rel_assum : Name.t Context.binder_annot * 'types -> ('constr, 'types) CRD.pt +val rel_defin : Name.t Context.binder_annot * 'constr * 'types -> ('constr, 'types) CRD.pt (* * Instantiate a local assumption as a local definition, using the provided term @@ -133,7 +133,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 Context.binder_annot array -> types array -> rel_declaration list (* --- Combining contexts --- *) diff --git a/src/coq/logicutils/hofs/hofs.ml b/src/coq/logicutils/hofs/hofs.ml index 4ff5058..ffcb4b2 100644 --- a/src/coq/logicutils/hofs/hofs.ml +++ b/src/coq/logicutils/hofs/hofs.ml @@ -176,11 +176,11 @@ let map_term_env_rec map_rec f d env sigma a trm = sigma, mkCase (ci, ct', 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 (Array.map Context.binder_name ns) ts trm) env sigma a ds in (* TODO refactor *) + 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 *) sigma, mkFix ((is, i), (ns, ts', ds')) | CoFix (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 (Array.map Context.binder_name ns) ts trm) env sigma a ds in (* TODO refactor *) + 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 *) sigma, mkCoFix (i, (ns, ts', ds')) | Proj (p, c) -> let sigma, c' = map_rec env sigma a c in @@ -245,11 +245,11 @@ let map_subterms_env_rec map_rec f d env sigma a trm = sigma, combine_cartesian (fun ct' (m', bs') -> mkCase (ci, ct', 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 (Array.map Context.binder_name ns) ts trm) env sigma a ds in (* TODO refactor *) + 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 *) sigma, combine_cartesian (fun ts' ds' -> mkFix ((is, i), (ns, ts', ds'))) tss' dss' | CoFix (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 (Array.map Context.binder_name ns) ts trm) env sigma a ds in (* TODO refactor *) + 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 *) sigma, combine_cartesian (fun ts' ds' -> mkCoFix (i, (ns, ts', ds'))) tss' dss' | Proj (p, c) -> let sigma, cs' = map_rec env sigma a c in @@ -341,11 +341,11 @@ let map_term_env_rec_shallow map_rec f d env sigma a trm = sigma, mkCase (ci, ct', 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 (Array.map Context.binder_name ns) ts trm) env sigma a ds in (* TODO refactor *) + 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 *) sigma, mkFix ((is, i), (ns, ts', ds')) | CoFix (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 (Array.map Context.binder_name ns) ts trm) env sigma a ds in (* TODO refactor *) + 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 *) sigma, mkCoFix (i, (ns, ts', ds')) | Proj (p, c) -> let sigma, c' = map_rec env sigma a c in @@ -517,11 +517,11 @@ let rec map_term_env_if_list p f d env sigma a trm = List.append ct' (List.append m' (List.flatten (Array.to_list bs'))) | Fix ((is, i), (ns, ts, ds)) -> let ts' = Array.map (map_rec env sigma a) ts in - let ds' = Array.map (map_rec_env_fix map_rec d env sigma a (Array.map Context.binder_name ns) ts) ds in + let ds' = Array.map (map_rec_env_fix map_rec d env sigma a ns ts) ds in List.append (List.flatten (Array.to_list ts')) (List.flatten (Array.to_list ds')) | CoFix (i, (ns, ts, ds)) -> let ts' = Array.map (map_rec env sigma a) ts in - let ds' = Array.map (map_rec_env_fix map_rec d env sigma a (Array.map Context.binder_name ns) ts) ds in + let ds' = Array.map (map_rec_env_fix map_rec d env sigma a ns ts) ds in List.append (List.flatten (Array.to_list ts')) (List.flatten (Array.to_list ds')) | Proj (pr, c) -> map_rec env sigma a c diff --git a/src/coq/logicutils/hofs/hofs.mli b/src/coq/logicutils/hofs/hofs.mli index 5269b52..db9cd98 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 Context.binder_annot array -> types array -> types -> 'b state) val map_rec_args : ('a, 'b) transformer_with_env -> From 7f0c7ec741beb1463f78150039b35516df00ce08 Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Tue, 25 Jul 2023 18:10:39 -0500 Subject: [PATCH 08/44] Undoing some changes from previous commit, using annotR uniformly now. --- src/coq/logicutils/contexts/contextutils.ml | 11 +++++------ src/coq/logicutils/contexts/contextutils.mli | 4 ++-- 2 files changed, 7 insertions(+), 8 deletions(-) diff --git a/src/coq/logicutils/contexts/contextutils.ml b/src/coq/logicutils/contexts/contextutils.ml index 2daeabd..e48b5db 100644 --- a/src/coq/logicutils/contexts/contextutils.ml +++ b/src/coq/logicutils/contexts/contextutils.ml @@ -51,10 +51,10 @@ let named_type decl = CND.get_type decl (* --- Constructing declarations --- *) (* Make the rel declaration for a local assumption *) -let rel_assum (name, typ) = CRD.LocalAssum (name, typ) +let rel_assum (name, typ) = CRD.LocalAssum (Context.annotR 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 (Context.annotR name, def, typ) (* Make the named declaration for a local assumption *) let named_assum (id, typ) = CND.LocalAssum (Context.annotR id, typ) @@ -71,8 +71,7 @@ let named_defin (id, def, typ) = CND.LocalDef (Context.annotR id, def, typ) *) let define_rel_decl body decl = assert (is_rel_assum decl); - match decl with - | CRD.LocalAssum (a, _) -> rel_defin (a, body, rel_type decl) + rel_defin (rel_name decl, body, rel_type decl) (* --- Mapping over contexts --- *) @@ -136,7 +135,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) | _ -> @@ -156,7 +155,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 | _ -> diff --git a/src/coq/logicutils/contexts/contextutils.mli b/src/coq/logicutils/contexts/contextutils.mli index 59dd6e0..5bf55ff 100644 --- a/src/coq/logicutils/contexts/contextutils.mli +++ b/src/coq/logicutils/contexts/contextutils.mli @@ -20,8 +20,8 @@ module CND = Context.Named.Declaration (* * Construct a local assumption/definition *) -val rel_assum : Name.t Context.binder_annot * 'types -> ('constr, 'types) CRD.pt -val rel_defin : Name.t Context.binder_annot * 'constr * 'types -> ('constr, 'types) CRD.pt +val rel_assum : Name.t * 'types -> ('constr, 'types) CRD.pt +val rel_defin : Name.t * 'constr * 'types -> ('constr, 'types) CRD.pt (* * Instantiate a local assumption as a local definition, using the provided term From 12f3ee59948e1f30eecf763a81570dbeadf25c56 Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Thu, 27 Jul 2023 12:51:29 -0500 Subject: [PATCH 09/44] Change typo in .gitignore --- .gitignore | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.gitignore b/.gitignore index 3cdf6d4..86105e6 100644 --- a/.gitignore +++ b/.gitignore @@ -23,4 +23,4 @@ plugin/Makefile plugin/.merlin *.out _opam -_build/ +_build From 1612ebccefc38a8358a43a883aa32301a40461e5 Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Thu, 27 Jul 2023 12:55:40 -0500 Subject: [PATCH 10/44] Remove unsused function. --- src/coq/logicutils/hofs/hofs.ml | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/src/coq/logicutils/hofs/hofs.ml b/src/coq/logicutils/hofs/hofs.ml index ffcb4b2..0bc6f9f 100644 --- a/src/coq/logicutils/hofs/hofs.ml +++ b/src/coq/logicutils/hofs/hofs.ml @@ -132,17 +132,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 *) From d8a0d14528964fb689bfe776b6260e692876f62d Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Thu, 27 Jul 2023 14:21:11 -0500 Subject: [PATCH 11/44] Renaming Globnames.global_reference to GlobRef.t --- src/coq/devutils/printing.mli | 2 +- src/coq/logicutils/contexts/modutils.mli | 4 ++-- src/coq/logicutils/hofs/substitution.ml | 2 +- src/coq/logicutils/hofs/substitution.mli | 2 +- src/coq/representationutils/defutils.ml | 2 +- src/coq/representationutils/defutils.mli | 13 ++++++------- 6 files changed, 12 insertions(+), 13 deletions(-) diff --git a/src/coq/devutils/printing.mli b/src/coq/devutils/printing.mli index e90a439..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 : Globnames.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/modutils.mli b/src/coq/logicutils/contexts/modutils.mli index fdb1aaa..4b531f1 100644 --- a/src/coq/logicutils/contexts/modutils.mli +++ b/src/coq/logicutils/contexts/modutils.mli @@ -30,9 +30,9 @@ val fold_module_structure_by_decl : 'a -> ('a -> Constant.t -> constant_body -> * Same as `fold_module_structure_by_decl` except a single step function * accepting a global reference. *) -val fold_module_structure_by_glob : 'a -> ('a -> Globnames.global_reference -> 'a) -> module_body -> 'a +val fold_module_structure_by_glob : 'a -> ('a -> GlobRef.t -> 'a) -> module_body -> 'a (* * Same as `fold_module_structure_by_glob` except an implicit unit accumulator. *) -val iter_module_structure_by_glob : (Globnames.global_reference -> unit) -> module_body -> unit +val iter_module_structure_by_glob : (GlobRef.t -> unit) -> module_body -> unit diff --git a/src/coq/logicutils/hofs/substitution.ml b/src/coq/logicutils/hofs/substitution.ml index 52683fe..7b05c9c 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 = Globnames.global_reference Globnames.Refmap.t +type global_substitution = GlobRef.t Globnames.Refmap.t (* Substitute global references throughout a term *) let rec subst_globals subst (term : constr) = diff --git a/src/coq/logicutils/hofs/substitution.mli b/src/coq/logicutils/hofs/substitution.mli index e921f38..374de2f 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 = Globnames.global_reference Globnames.Refmap.t +type global_substitution = GlobRef.t Globnames.Refmap.t (* Substitute global references throughout a term *) val subst_globals : global_substitution -> constr -> constr diff --git a/src/coq/representationutils/defutils.ml b/src/coq/representationutils/defutils.ml index ce1d0ae..28de476 100644 --- a/src/coq/representationutils/defutils.ml +++ b/src/coq/representationutils/defutils.ml @@ -92,7 +92,7 @@ let extern env sigma t : constr_expr = Constrextern.extern_constr true env sigma (EConstr.of_constr t) (* Construct the external expression for a definition *) -let expr_of_global (g : Globnames.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), [])) diff --git a/src/coq/representationutils/defutils.mli b/src/coq/representationutils/defutils.mli index 7d485db..1ff75a6 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 -> Globnames.global_reference - + ?typ:types -> Id.t -> evar_map -> types -> bool -> GlobRef.t (* * Like define_term, but for a canonical structure *) val define_canonical : - ?typ:types -> Id.t -> evar_map -> types -> bool -> Globnames.global_reference + ?typ:types -> Id.t -> evar_map -> types -> bool -> 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 : Globnames.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 -> Globnames.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 : Globnames.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 -> Globnames.global_reference -> evar_map * constr +val new_global : evar_map -> GlobRef.t -> evar_map * constr From e3076e5497cc014793941fddcb080fd534e4105d Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Fri, 28 Jul 2023 14:16:36 -0500 Subject: [PATCH 12/44] Fixed the type in indutils --- src/coq/logicutils/inductive/indutils.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/coq/logicutils/inductive/indutils.ml b/src/coq/logicutils/inductive/indutils.ml index e675334..c34bf8e 100644 --- a/src/coq/logicutils/inductive/indutils.ml +++ b/src/coq/logicutils/inductive/indutils.ml @@ -154,10 +154,10 @@ let inst_abs_univ_ctx abs_univ_ctx = (* 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 - | Entries.Monomorphic_entry univ_ctx_set -> + | Declarations.Monomorphic uctx_set -> let univ_ctx = Univ.UContext.empty in - (Entries.Monomorphic_entry univ_ctx_set, univ_ctx) - | Entries.Polymorphic_entry (name_array, abs_univ_ctx) -> + (Entries.Monomorphic_entry uctx_set, univ_ctx) + | Declarations.Polymorphic auctx -> let univ_ctx = inst_abs_univ_ctx abs_univ_ctx in (Entries.Polymorphic_entry (name_array, univ_ctx), univ_ctx) From 0ebe46b560e21caed4222aed10804ee3368c26ba Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Mon, 31 Jul 2023 12:28:09 -0500 Subject: [PATCH 13/44] Fixed the type incompatibility in inference.ml --- src/coq/logicutils/typesandequality/inference.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/coq/logicutils/typesandequality/inference.ml b/src/coq/logicutils/typesandequality/inference.ml index 477154e..042bff1 100644 --- a/src/coq/logicutils/typesandequality/inference.ml +++ b/src/coq/logicutils/typesandequality/inference.ml @@ -10,12 +10,14 @@ open Declarations (* Safely infer the WHNF type of a term, updating the evar map *) let infer_type env sigma term = let eterm = EConstr.of_constr term in - Typing.type_of ~refresh:true env sigma eterm + let sigma, typ = Typing.type_of ~refresh:true env sigma eterm in + sigma, EConstr.to_constr sigma typ (* Safely infer the sort of a type, updating the evar map *) let infer_sort env sigma term = let eterm = EConstr.of_constr term in - Typing.sort_of env sigma eterm + 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?) *) let type_of_inductive env index mutind_body : types = From fe4467516339f963dbd4770ef378c1f04ec87674 Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Fri, 4 Aug 2023 16:56:56 -0500 Subject: [PATCH 14/44] Refactored to maintain the original semantics. --- src/coq/logicutils/transformation/transform.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/coq/logicutils/transformation/transform.ml b/src/coq/logicutils/transformation/transform.ml index ae5971b..4abe43e 100644 --- a/src/coq/logicutils/transformation/transform.ml +++ b/src/coq/logicutils/transformation/transform.ml @@ -88,12 +88,14 @@ let transform_inductive ident tr_constr (mind_body, ind_body as ind_specif) = let try_register_record mod_path (ind, ind') = try let r = lookup_structure ind in + let r' = lookup_structure ind' in Feedback.msg_info (Pp.str "Transformed a record"); - let con = r.s_CONST in + (* let con = r.s_CONST in *) let pks = r.s_PROJKIND in let ps = r.s_PROJ in + let ps' = List.map (Option.map (fun p -> Constant.make2 mod_path (Constant.label p))) ps in (try - declare_structure (con, pks, ps) + declare_structure (r'.s_CONST, pks, ps') with _ -> Feedback.msg_warning (Pp.str "Failed to register projections for transformed record")) From eadbabf24c75cf382abbb3c0f595d9ab13146d30 Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Mon, 7 Aug 2023 12:48:21 -0500 Subject: [PATCH 15/44] Refactored constutils to handle type change of UnivGen.fresh_instance --- src/coq/termutils/constutils.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/coq/termutils/constutils.ml b/src/coq/termutils/constutils.ml index 4a8e384..07ee80f 100644 --- a/src/coq/termutils/constutils.ml +++ b/src/coq/termutils/constutils.ml @@ -19,7 +19,8 @@ let make_constant id = *) 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 instance, (_, constr) = UnivGen.fresh_instance auctx in + let uctx = Univ.UContext.make (instance, constr) in let term = Vars.subst_instance_constr (Univ.UContext.instance uctx) term in let env = Environ.push_context uctx env in env, term From 0b4e99f141244d57c7b24740460c291a351ab301 Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Mon, 7 Aug 2023 15:40:40 -0500 Subject: [PATCH 16/44] Refactored indutils to handle type changes to Declarations.universes --- src/coq/logicutils/inductive/indutils.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/coq/logicutils/inductive/indutils.ml b/src/coq/logicutils/inductive/indutils.ml index c34bf8e..e95ac64 100644 --- a/src/coq/logicutils/inductive/indutils.ml +++ b/src/coq/logicutils/inductive/indutils.ml @@ -150,7 +150,8 @@ let arity_of_ind_body ind_body = (* 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 @@ -158,17 +159,17 @@ let make_ind_univs_entry = function let univ_ctx = Univ.UContext.empty in (Entries.Monomorphic_entry uctx_set, univ_ctx) | Declarations.Polymorphic auctx -> - let univ_ctx = inst_abs_univ_ctx abs_univ_ctx in - (Entries.Polymorphic_entry (name_array, univ_ctx), univ_ctx) + 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 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_set false univ_ctx; + Global.push_context_set 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 (Context.annotR 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 From b1064b318e87e5523c812b51d57dc861faca44ff Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Mon, 7 Aug 2023 15:42:12 -0500 Subject: [PATCH 17/44] Refactored indutils to handle type changes to Declarations.universes --- src/coq/logicutils/inductive/indutils.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coq/logicutils/inductive/indutils.ml b/src/coq/logicutils/inductive/indutils.ml index e95ac64..a5745b0 100644 --- a/src/coq/logicutils/inductive/indutils.ml +++ b/src/coq/logicutils/inductive/indutils.ml @@ -163,7 +163,7 @@ let make_ind_univs_entry = function (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 in + 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 From 43813afe33bba5c541ab8fe8525ec68f72989633 Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Mon, 7 Aug 2023 17:24:44 -0500 Subject: [PATCH 18/44] Refactored defutils to handle type changes in Lemmas.hook_type --- src/coq/representationutils/defutils.ml | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/src/coq/representationutils/defutils.ml b/src/coq/representationutils/defutils.ml index 28de476..4acfa9d 100644 --- a/src/coq/representationutils/defutils.ml +++ b/src/coq/representationutils/defutils.ml @@ -56,25 +56,26 @@ let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook re 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 ~ontop:None ~hook_data:hook ident k ce ubinders imps + let uctx = Evd.evar_universe_context sigma in + let hook_data = Option.map (fun hook -> hook, uctx, []) hook in + DeclareDef.declare_definition ~ontop:None ?hook_data ident k ce ubinders imps (* Define a new Coq term *) let define_term ?typ (n : Id.t) (evm : evar_map) (trm : types) (refresh : bool) = let k = (Global, Attributes.is_universe_polymorphism(), Definition) 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 k ~opaque:false evm udecl etrm etyp [] None refresh (* Define a Canonical Structure *) let define_canonical ?typ (n : Id.t) (evm : evar_map) (trm : types) (refresh : bool) = let k = (Global, Attributes.is_universe_polymorphism (), CanonicalStructure) in let udecl = UState.default_univ_decl in - let hook = Lemmas.mk_hook (fun _ x -> declare_canonical_structure x; x) in + let hook = Lemmas.mk_hook (fun _ _ _ x -> declare_canonical_structure 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 [] hook refresh + edeclare n k ~opaque:false evm udecl etrm etyp [] (Some hook) refresh (* --- Converting between representations --- *) @@ -114,4 +115,6 @@ let constr_of_pglobal (glob, univs) = | VarRef id -> mkVar id (* Safely instantiate a global reference, with proper universe handling *) -let new_global sigma gref = Evarutil.new_global sigma gref +let new_global sigma gref = + let sigma, typ = Evarutil.new_global sigma gref in + sigma, EConstr.to_constr sigma typ \ No newline at end of file From 892b96c345a26ebd2db08cb65128f1c67043e9ec Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Mon, 7 Aug 2023 17:28:39 -0500 Subject: [PATCH 19/44] Added mlg file --- src/plib.mlg | 1 + 1 file changed, 1 insertion(+) create mode 100644 src/plib.mlg diff --git a/src/plib.mlg b/src/plib.mlg new file mode 100644 index 0000000..197773c --- /dev/null +++ b/src/plib.mlg @@ -0,0 +1 @@ +DECLARE PLUGIN "plib" From 78363677e2cf5b80ddf1507716a304cd12df8734 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 8 Aug 2023 16:29:28 +0200 Subject: [PATCH 20/44] Merged changes from another fork branch to fix errors. --- .gitignore | 4 +++ Makefile.local | 1 + src/coq/constants/equtils.ml | 29 ++++++++++++------- src/coq/constants/idutils.ml | 3 +- src/coq/constants/produtils.ml | 24 +++++++++------ src/coq/constants/proputils.ml | 5 ++-- src/coq/constants/sigmautils.ml | 22 +++++++++----- src/coq/decompiler/decompiler.ml | 12 +++++--- src/coq/devutils/printing.ml | 7 +++-- src/coq/logicutils/contexts/contextutils.ml | 2 +- src/coq/logicutils/contexts/envutils.ml | 2 -- src/coq/logicutils/contexts/modutils.ml | 6 ++-- src/coq/logicutils/hofs/debruijn.ml | 27 ----------------- src/coq/logicutils/hofs/filters.ml | 1 - src/coq/logicutils/hofs/hofs.ml | 1 - src/coq/logicutils/hofs/zooming.ml | 1 - src/coq/logicutils/inductive/indexing.ml | 1 - src/coq/logicutils/inductive/indutils.ml | 3 +- .../logicutils/transformation/transform.ml | 14 ++++----- .../typesandequality/convertibility.ml | 1 - .../logicutils/typesandequality/inference.ml | 2 -- src/coq/representationutils/defutils.ml | 12 +++++--- src/coq/representationutils/nameutils.ml | 1 - src/coq/termutils/constutils.ml | 3 +- src/utilities/utilities.ml | 8 +---- 25 files changed, 91 insertions(+), 101 deletions(-) create mode 100644 Makefile.local diff --git a/.gitignore b/.gitignore index 86105e6..2a37f27 100644 --- a/.gitignore +++ b/.gitignore @@ -24,3 +24,7 @@ plugin/.merlin *.out _opam _build +/Makefile +/Makefile.conf +.merlin +/src/plibrary.ml diff --git a/Makefile.local b/Makefile.local new file mode 100644 index 0000000..636472b --- /dev/null +++ b/Makefile.local @@ -0,0 +1 @@ +CAMLFLAGS+=-w -40 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 b9da7ed..53dbe20 100644 --- a/src/coq/decompiler/decompiler.ml +++ b/src/coq/decompiler/decompiler.ml @@ -38,8 +38,8 @@ let run_tac env sigma (tac : unit Proofview.tactic) (goal : constr) : Goal.goal list * Evd.evar_map = let p = Proof.start ~name:(Names.Id.of_string "placeholder") ~poly:true 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 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 = @@ -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 @@ -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 cd86380..cf5f999 100644 --- a/src/coq/devutils/printing.ml +++ b/src/coq/devutils/printing.ml @@ -58,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) = @@ -153,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 = diff --git a/src/coq/logicutils/contexts/contextutils.ml b/src/coq/logicutils/contexts/contextutils.ml index e48b5db..d33b50d 100644 --- a/src/coq/logicutils/contexts/contextutils.ml +++ b/src/coq/logicutils/contexts/contextutils.ml @@ -210,7 +210,7 @@ let bindings_for_inductive env mutind_body ind_bodies : rel_declaration list = (* * Fixpoints *) -let bindings_for_fix (names : name Context.binder_annot 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/envutils.ml b/src/coq/logicutils/contexts/envutils.ml index 5be88cc..b9d5e0e 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 diff --git a/src/coq/logicutils/contexts/modutils.ml b/src/coq/logicutils/contexts/modutils.ml index dbc68ca..46a8469 100644 --- a/src/coq/logicutils/contexts/modutils.ml +++ b/src/coq/logicutils/contexts/modutils.ml @@ -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) @@ -65,7 +65,7 @@ let fold_module_structure_by_decl init fold_const fold_ind mod_body = let ind = (MutInd.make2 mod_path label, 0) 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.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 +77,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/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 0bc6f9f..7a78833 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 diff --git a/src/coq/logicutils/hofs/zooming.ml b/src/coq/logicutils/hofs/zooming.ml index 67ce5d3..ed3a0ed 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 --- *) 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 a5745b0..da77a5a 100644 --- a/src/coq/logicutils/inductive/indutils.ml +++ b/src/coq/logicutils/inductive/indutils.ml @@ -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) = - UnivGen.constr_of_global (Indrec.lookup_eliminator ind InType) + UnivGen.constr_of_global (Indrec.lookup_eliminator ind Sorts.InType) +[@@ocaml.warning "-3"] (* TODO handle univ poly eliminator *) (* Applications of eliminators *) type elim_app = diff --git a/src/coq/logicutils/transformation/transform.ml b/src/coq/logicutils/transformation/transform.ml index 4abe43e..e326f6c 100644 --- a/src/coq/logicutils/transformation/transform.ml +++ b/src/coq/logicutils/transformation/transform.ml @@ -116,7 +116,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 @@ -126,7 +126,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 @@ -140,11 +140,11 @@ 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 @@ -155,9 +155,9 @@ let transform_module_structure ?(init=const Globnames.Refmap.empty) ?(opaques=Gl 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') + 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) (list_elim ind') | SFBmodule mod_body -> Feedback.msg_warning (Pp.str "Skipping nested module structure"); subst 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 042bff1..135d7aa 100644 --- a/src/coq/logicutils/typesandequality/inference.ml +++ b/src/coq/logicutils/typesandequality/inference.ml @@ -2,8 +2,6 @@ * Type inference *) -open Environ -open Evd open Constr open Declarations diff --git a/src/coq/representationutils/defutils.ml b/src/coq/representationutils/defutils.ml index 4acfa9d..7cd9d1b 100644 --- a/src/coq/representationutils/defutils.ml +++ b/src/coq/representationutils/defutils.ml @@ -2,6 +2,8 @@ * Utilities for defining terms *) +module CVars = Vars + open Constr open Names open Evd @@ -49,7 +51,7 @@ let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook re 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 + Univ.LSet.union uvars (CVars.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 @@ -99,8 +101,9 @@ let expr_of_global (g : GlobRef.t) : constr_expr = (* 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 @@ -108,8 +111,9 @@ 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 @@ -117,4 +121,4 @@ let constr_of_pglobal (glob, univs) = (* Safely instantiate a global reference, with proper universe handling *) let new_global sigma gref = let sigma, typ = Evarutil.new_global sigma gref in - sigma, EConstr.to_constr sigma typ \ No newline at end of file + sigma, EConstr.to_constr sigma typ 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 07ee80f..b7cbfb5 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,7 +17,7 @@ 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 (term, auctx) = Option.get @@ Global.body_of_constant const in let instance, (_, constr) = UnivGen.fresh_instance auctx in let uctx = Univ.UContext.make (instance, constr) in let term = Vars.subst_instance_constr (Univ.UContext.instance uctx) term in 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 From b3cd62cc8ecd3a5eb821bb684e7e4525c81fdd3e Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Tue, 8 Aug 2023 14:09:52 -0500 Subject: [PATCH 21/44] Removed Makefile.local --- Makefile.local | 1 - 1 file changed, 1 deletion(-) delete mode 100644 Makefile.local diff --git a/Makefile.local b/Makefile.local deleted file mode 100644 index 636472b..0000000 --- a/Makefile.local +++ /dev/null @@ -1 +0,0 @@ -CAMLFLAGS+=-w -40 From 55c3363382e790ed004adde829094a54bae15212 Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Wed, 16 Aug 2023 17:07:43 -0500 Subject: [PATCH 22/44] Renamed plugin to match template, builds with dune currently. --- dune-project | 2 ++ my-plugin.opam | 0 src/dune | 7 ++++--- src/plib.mlg | 2 +- theories/Plib.v | 1 - theories/Test.v | 1 + theories/dune | 4 ++++ 7 files changed, 12 insertions(+), 5 deletions(-) create mode 100644 my-plugin.opam delete mode 100644 theories/Plib.v create mode 100644 theories/Test.v create mode 100644 theories/dune diff --git a/dune-project b/dune-project index 0a32580..54d8b99 100644 --- a/dune-project +++ b/dune-project @@ -1 +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/dune b/src/dune index 422abf1..abd1224 100644 --- a/src/dune +++ b/src/dune @@ -1,9 +1,10 @@ (library - (name termutils) + (name example_plugin) (wrapped false) - (public_name synth.termutils) - (synopsis "Termutils library") + (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 index 197773c..355877c 100644 --- a/src/plib.mlg +++ b/src/plib.mlg @@ -1 +1 @@ -DECLARE PLUGIN "plib" +DECLARE PLUGIN "example_plugin" 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 From ffe7e1661f355b9de32bbe5bf1d3d629348afc3e Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Fri, 18 Aug 2023 13:58:07 -0500 Subject: [PATCH 23/44] Fixed warnings. --- src/coq/logicutils/contexts/envutils.mli | 4 ++-- src/coq/logicutils/hofs/hofs.mli | 2 +- src/coq/logicutils/hofs/substitution.ml | 4 ++-- src/coq/logicutils/hofs/substitution.mli | 2 +- src/coq/logicutils/transformation/transform.mli | 2 +- 5 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/coq/logicutils/contexts/envutils.mli b/src/coq/logicutils/contexts/envutils.mli index cd9b871..cf7d758 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 Context.binder_annot * types) -> env -> env -val push_let_in : (name Context.binder_annot * types * types) -> env -> env +val push_local : (Name.t Context.binder_annot * types) -> env -> env +val push_let_in : (Name.t Context.binder_annot * types * types) -> env -> env (* * Lookup from an environment diff --git a/src/coq/logicutils/hofs/hofs.mli b/src/coq/logicutils/hofs/hofs.mli index db9cd98..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 Context.binder_annot 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/substitution.ml b/src/coq/logicutils/hofs/substitution.ml index 7b05c9c..b63e8f8 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 = GlobRef.t 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,7 +126,7 @@ 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 diff --git a/src/coq/logicutils/hofs/substitution.mli b/src/coq/logicutils/hofs/substitution.mli index 374de2f..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 = GlobRef.t 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/transformation/transform.mli b/src/coq/logicutils/transformation/transform.mli index 68c42f1..96ab44a 100644 --- a/src/coq/logicutils/transformation/transform.mli +++ b/src/coq/logicutils/transformation/transform.mli @@ -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 From b8af2c9d5cb5cc07cfc9aed43d7ae7d79d26ead0 Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Fri, 18 Aug 2023 13:59:12 -0500 Subject: [PATCH 24/44] Fixed warnings. --- src/coq/logicutils/contexts/contextutils.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coq/logicutils/contexts/contextutils.mli b/src/coq/logicutils/contexts/contextutils.mli index 5bf55ff..889c13f 100644 --- a/src/coq/logicutils/contexts/contextutils.mli +++ b/src/coq/logicutils/contexts/contextutils.mli @@ -133,7 +133,7 @@ val bindings_for_inductive : env -> mutual_inductive_body -> one_inductive_body array -> rel_declaration list val bindings_for_fix : - name Context.binder_annot array -> types array -> rel_declaration list + Name.t Context.binder_annot array -> types array -> rel_declaration list (* --- Combining contexts --- *) From 925fc080e387095b43d7c5596c2f62d259ef78c8 Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Wed, 30 Aug 2023 14:25:09 -0500 Subject: [PATCH 25/44] Added error handling for SProp. --- .../logicutils/transformation/transform.ml | 23 +++++++++++++++++-- 1 file changed, 21 insertions(+), 2 deletions(-) diff --git a/src/coq/logicutils/transformation/transform.ml b/src/coq/logicutils/transformation/transform.ml index e326f6c..5d759a8 100644 --- a/src/coq/logicutils/transformation/transform.ml +++ b/src/coq/logicutils/transformation/transform.ml @@ -102,6 +102,18 @@ let try_register_record mod_path (ind, ind') = with Not_found -> () +let lookup_eliminator_error_handling ind sorts = + (* Feedback.msg_warning (Pp.(str "start ")); *) + List.filter_map (fun x -> x) + (List.map + (fun x -> + (* try Some (x, Indrec.lookup_eliminator env ind x) *) + try Some (x, Indrec.lookup_eliminator 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 @@ -154,10 +166,17 @@ let transform_module_structure ?(init=const GlobRef.Map.empty) ?(opaques=GlobRef 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 + 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) (list_elim 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 From 9e874d3fa02a0261d544edea5370a11f582873fa Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Thu, 28 Sep 2023 15:56:00 +0530 Subject: [PATCH 26/44] Changed the Context.binder_name usage to remove calls to annotR to handle SProp correctly. --- src/coq/decompiler/decompiler.ml | 8 +++--- src/coq/devutils/printing.ml | 6 ++-- src/coq/logicutils/contexts/contextutils.ml | 16 ++++++++--- src/coq/logicutils/contexts/contextutils.mli | 8 ++++-- src/coq/logicutils/contexts/envutils.ml | 4 +-- src/coq/logicutils/contexts/envutils.mli | 4 +-- src/coq/logicutils/hofs/hofs.ml | 30 ++++++++++---------- src/coq/logicutils/hofs/zooming.ml | 8 +++--- src/coq/logicutils/inductive/indutils.ml | 4 +-- 9 files changed, 50 insertions(+), 38 deletions(-) diff --git a/src/coq/decompiler/decompiler.ml b/src/coq/decompiler/decompiler.ml index 53dbe20..177ea3c 100644 --- a/src/coq/decompiler/decompiler.ml +++ b/src/coq/decompiler/decompiler.ml @@ -446,7 +446,7 @@ and rewrite_in (name, valu, _, body) (env, sigma, opts) : tactical option = try_rel rewr.px >>= fun idx -> guard (noccurn (idx + 1) body) >>= fun _ -> let n, t = rel_name_type (lookup_rel idx env) in - let env' = push_local (Context.make_annot n (Context.binder_relevance name), t) env in + let env' = push_local (n, t) env in dot (RewriteIn (env, rewr.eq, rewr.px, rewr.left)) (first_pass env' sigma opts body) @@ -460,7 +460,7 @@ and apply_in (name, valu, typ, body) (env, sigma, opts) : tactical option = guard (noccurn (idx + 1) body) >>= fun _ -> (* H does not occur in body *) guard (not (noccurn 1 body)) >>= fun _ -> (* new binding DOES occur *) let n, t = rel_name_type (lookup_rel idx env) in (* "H" *) - let env' = push_local (Context.make_annot n (Context.binder_relevance name), t) env in (* change type of "H" *) + let env' = push_local (n, t) env in (* change type of "H" *) let prf = mkApp (f, Array.sub args 0 (len - 1)) in (* let H2 := f H1 := H2 ... *) let apply_binding app_in (_, sigma) = @@ -479,12 +479,12 @@ and apply_in (name, 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 (Context.binder_name n) in - let env' = push_let_in (Context.make_annot (Name n') (Context.binder_relevance n), valu, t) env 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. *) diff --git a/src/coq/devutils/printing.ml b/src/coq/devutils/printing.ml index cf5f999..cd55f74 100644 --- a/src/coq/devutils/printing.ml +++ b/src/coq/devutils/printing.ml @@ -85,20 +85,20 @@ let rec term_as_string (env : env) (trm : types) = "(Π (%s : %s) . %s)" (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 (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 (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)" diff --git a/src/coq/logicutils/contexts/contextutils.ml b/src/coq/logicutils/contexts/contextutils.ml index d33b50d..4f8f60f 100644 --- a/src/coq/logicutils/contexts/contextutils.ml +++ b/src/coq/logicutils/contexts/contextutils.ml @@ -50,17 +50,25 @@ 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 (Context.annotR 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 (Context.annotR 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 (Context.annotR id, typ) +let named_assum (id, typ) = CND.LocalAssum (id, typ) (* Make the named declaration for a local definition *) -let named_defin (id, def, typ) = CND.LocalDef (Context.annotR id, def, typ) +let named_defin (id, def, typ) = CND.LocalDef (id, def, typ) (* * Instantiate a local assumption as a local definition, using the provided term diff --git a/src/coq/logicutils/contexts/contextutils.mli b/src/coq/logicutils/contexts/contextutils.mli index 889c13f..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? *) diff --git a/src/coq/logicutils/contexts/envutils.ml b/src/coq/logicutils/contexts/envutils.ml index b9d5e0e..9aaf2d2 100644 --- a/src/coq/logicutils/contexts/envutils.ml +++ b/src/coq/logicutils/contexts/envutils.ml @@ -36,10 +36,10 @@ let rel_name_type rel : Name.t * types = (* 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) = diff --git a/src/coq/logicutils/contexts/envutils.mli b/src/coq/logicutils/contexts/envutils.mli index cf7d758..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.t Context.binder_annot * types) -> env -> env -val push_let_in : (Name.t Context.binder_annot * 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/hofs/hofs.ml b/src/coq/logicutils/hofs/hofs.ml index 7a78833..1b94a96 100644 --- a/src/coq/logicutils/hofs/hofs.ml +++ b/src/coq/logicutils/hofs/hofs.ml @@ -142,16 +142,16 @@ 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 @@ -211,16 +211,16 @@ 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 @@ -304,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 @@ -483,16 +483,16 @@ 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 @@ -568,16 +568,16 @@ 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 diff --git a/src/coq/logicutils/hofs/zooming.ml b/src/coq/logicutils/hofs/zooming.ml index ed3a0ed..c72611a 100644 --- a/src/coq/logicutils/hofs/zooming.ml +++ b/src/coq/logicutils/hofs/zooming.ml @@ -21,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" @@ -34,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) @@ -42,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 +56,7 @@ let zoom_lambda_names env except trm : env * types * Id.t list = match kind trm with | Lambda (n, t, b) -> let name = fresh_name env (Context.binder_name n) in - let env' = push_local (Context.make_annot (Name name) (Context.binder_relevance n), t) env in + let env' = push_local (Context.binder_name n, t) env in let env, trm, names = aux env' (limit - 1) b in (env, trm, name :: names) diff --git a/src/coq/logicutils/inductive/indutils.ml b/src/coq/logicutils/inductive/indutils.ml index da77a5a..805d8d1 100644 --- a/src/coq/logicutils/inductive/indutils.ml +++ b/src/coq/logicutils/inductive/indutils.ml @@ -126,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 From 233f21d991420952a0e9cd7ec2fde0201872c28a Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Thu, 28 Sep 2023 16:22:35 +0530 Subject: [PATCH 27/44] Changed the Context.binder_name usage to remove calls to annotR to handle SProp correctly. --- src/coq/logicutils/inductive/indutils.ml | 2 +- src/coq/logicutils/transformation/transform.ml | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/coq/logicutils/inductive/indutils.ml b/src/coq/logicutils/inductive/indutils.ml index 805d8d1..4d61200 100644 --- a/src/coq/logicutils/inductive/indutils.ml +++ b/src/coq/logicutils/inductive/indutils.ml @@ -170,7 +170,7 @@ let open_inductive ?(global=false) env (mind_body, ind_body) = if global then Global.push_context_set false (Univ.ContextSet.of_context univ_ctx); let arity = arity_of_ind_body ind_body in - let arity_ctx = [CRD.LocalAssum (Context.annotR 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 diff --git a/src/coq/logicutils/transformation/transform.ml b/src/coq/logicutils/transformation/transform.ml index 5d759a8..600e961 100644 --- a/src/coq/logicutils/transformation/transform.ml +++ b/src/coq/logicutils/transformation/transform.ml @@ -163,9 +163,10 @@ let transform_module_structure ?(init=const GlobRef.Map.empty) ?(opaques=GlobRef 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 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 From 7e47d4d4a06fef45089ab24a90f55e3b3568a6e2 Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Wed, 4 Oct 2023 13:03:24 +0530 Subject: [PATCH 28/44] Filter out SProp eliminators based on string match for sind. --- src/coq/logicutils/transformation/transform.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/coq/logicutils/transformation/transform.ml b/src/coq/logicutils/transformation/transform.ml index 600e961..68d87c0 100644 --- a/src/coq/logicutils/transformation/transform.ml +++ b/src/coq/logicutils/transformation/transform.ml @@ -114,6 +114,13 @@ let lookup_eliminator_error_handling ind sorts = ) sorts) +let contains s1 s2 = + let re = Str.regexp_string s2 in + try + ignore (Str.search_forward re s1 0); + true + with Not_found -> false + (* * Declare a new module structure under the given name with the compositionally * transformed (i.e., forward-substituted) components from the given module @@ -138,7 +145,7 @@ let transform_module_structure ?(init=const GlobRef.Map.empty) ?(opaques=GlobRef match b with | SFBconst const_body -> let const = Constant.make2 mod_path l in - not (GlobRef.Set.mem (GlobRef.ConstRef const) opaques) + not (GlobRef.Set.mem (GlobRef.ConstRef const) opaques) && not (contains (Label.to_string l) ("sind")) | _ -> true) mod_elems From 525f61e3094a4f02016f48f4b97573dc75c0702f Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Mon, 23 Oct 2023 17:40:19 -0500 Subject: [PATCH 29/44] Fixed bug that pushed the wrong name. --- src/coq/logicutils/hofs/zooming.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coq/logicutils/hofs/zooming.ml b/src/coq/logicutils/hofs/zooming.ml index c72611a..c1e49a9 100644 --- a/src/coq/logicutils/hofs/zooming.ml +++ b/src/coq/logicutils/hofs/zooming.ml @@ -56,7 +56,7 @@ let zoom_lambda_names env except trm : env * types * Id.t list = match kind trm with | Lambda (n, t, b) -> let name = fresh_name env (Context.binder_name n) in - let env' = push_local (Context.binder_name n, t) env in + let env' = push_local (Name name, t) env in let env, trm, names = aux env' (limit - 1) b in (env, trm, name :: names) From 66079684fd1df5efd546af980dd7728786dc42df Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Wed, 25 Oct 2023 17:54:02 -0500 Subject: [PATCH 30/44] Changed the arguments to declare_structure to reflect the API change. --- src/coq/logicutils/transformation/transform.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/coq/logicutils/transformation/transform.ml b/src/coq/logicutils/transformation/transform.ml index 68d87c0..b286f3b 100644 --- a/src/coq/logicutils/transformation/transform.ml +++ b/src/coq/logicutils/transformation/transform.ml @@ -88,14 +88,15 @@ let transform_inductive ident tr_constr (mind_body, ind_body as ind_specif) = let try_register_record mod_path (ind, ind') = try let r = lookup_structure ind in - let r' = lookup_structure ind' in Feedback.msg_info (Pp.str "Transformed a record"); - (* let con = r.s_CONST in *) let pks = r.s_PROJKIND in - let ps = r.s_PROJ in - let ps' = List.map (Option.map (fun p -> Constant.make2 mod_path (Constant.label p))) ps in + let ps = + List.map + (Option.map (fun p -> Constant.make2 mod_path (Constant.label p))) + r.s_PROJ + in (try - declare_structure (r'.s_CONST, pks, ps') + declare_structure ((ind', 1), pks, ps) with _ -> Feedback.msg_warning (Pp.str "Failed to register projections for transformed record")) From 0082bd84773b328edbc5ccfa7886d2571eb7527b Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Wed, 25 Oct 2023 18:23:35 -0500 Subject: [PATCH 31/44] Filter out SProp sorts to prevent call to Indrec.lookup_eliminator. --- src/coq/logicutils/contexts/modutils.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coq/logicutils/contexts/modutils.ml b/src/coq/logicutils/contexts/modutils.ml index 46a8469..7076472 100644 --- a/src/coq/logicutils/contexts/modutils.ml +++ b/src/coq/logicutils/contexts/modutils.ml @@ -64,7 +64,7 @@ let fold_module_structure_by_decl init fold_const fold_ind mod_body = let ind_body = mind_body.mind_packets.(0) in let ind = (MutInd.make2 mod_path label, 0) in let globset' = - List.map (Indrec.lookup_eliminator ind) ind_body.mind_kelim |> + List.map (Indrec.lookup_eliminator ind) (List.filter (fun (x) -> not (Sorts.family_equal x InSProp)) 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)) From 3a9de5ddb56f016ff4d5d94cbf3c876f6a1610de Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Wed, 25 Oct 2023 22:23:58 -0500 Subject: [PATCH 32/44] Pulled in Max's changes from 8.11 branch of coq-plugin-lib --- src/coq/decompiler/decompiler.ml | 6 ++-- src/coq/logicutils/contexts/envutils.ml | 2 +- src/coq/logicutils/contexts/modutils.ml | 5 +-- src/coq/logicutils/contexts/modutils.mli | 9 +++--- src/coq/logicutils/inductive/indutils.ml | 9 ++---- .../logicutils/transformation/transform.ml | 9 +++--- .../logicutils/transformation/transform.mli | 2 +- src/coq/representationutils/defutils.ml | 32 +++++++------------ src/coq/termutils/constutils.ml | 13 ++++---- 9 files changed, 39 insertions(+), 48 deletions(-) diff --git a/src/coq/decompiler/decompiler.ml b/src/coq/decompiler/decompiler.ml index 177ea3c..4c47809 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 ~name:(Names.Id.of_string "placeholder") ~poly:true sigma [(env, EConstr.of_constr goal)] in - let (p', _) = Proof.run_tactic env tac p in + 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 diff --git a/src/coq/logicutils/contexts/envutils.ml b/src/coq/logicutils/contexts/envutils.ml index 9aaf2d2..ff9abe3 100644 --- a/src/coq/logicutils/contexts/envutils.ml +++ b/src/coq/logicutils/contexts/envutils.ml @@ -51,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/modutils.ml b/src/coq/logicutils/contexts/modutils.ml index 7076472..ed179a7 100644 --- a/src/coq/logicutils/contexts/modutils.ml +++ b/src/coq/logicutils/contexts/modutils.ml @@ -27,7 +27,7 @@ let decompose_module_signature mod_sign = let declare_module_structure ?(params=[]) ident declare_elements = 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; @@ -63,8 +63,9 @@ 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) (List.filter (fun (x) -> not (Sorts.family_equal x InSProp)) ind_body.mind_kelim) |> + 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)) diff --git a/src/coq/logicutils/contexts/modutils.mli b/src/coq/logicutils/contexts/modutils.mli index 4b531f1..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 -> GlobRef.t -> '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 : (GlobRef.t -> 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/inductive/indutils.ml b/src/coq/logicutils/inductive/indutils.ml index 4d61200..1c78ce3 100644 --- a/src/coq/logicutils/inductive/indutils.ml +++ b/src/coq/logicutils/inductive/indutils.ml @@ -78,7 +78,7 @@ let is_elim (env : env) (trm : types) = (* Lookup the eliminator over the type sort *) let type_eliminator (env : env) (ind : inductive) = - UnivGen.constr_of_global (Indrec.lookup_eliminator ind Sorts.InType) + UnivGen.constr_of_monomorphic_global (Indrec.lookup_eliminator env ind Sorts.InType) [@@ocaml.warning "-3"] (* TODO handle univ poly eliminator *) (* Applications of eliminators *) @@ -194,8 +194,5 @@ let declare_inductive typename consnames template univs nparam arity constypes = mind_entry_private = None; mind_entry_variance = None } 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/transformation/transform.ml b/src/coq/logicutils/transformation/transform.ml index b286f3b..6d2c433 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") @@ -96,7 +97,7 @@ let try_register_record mod_path (ind, ind') = r.s_PROJ in (try - declare_structure ((ind', 1), pks, ps) + declare_structure_entry ((ind', 1), pks, ps) with _ -> Feedback.msg_warning (Pp.str "Failed to register projections for transformed record")) @@ -105,11 +106,11 @@ let try_register_record mod_path (ind, ind') = 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) *) - try Some (x, Indrec.lookup_eliminator ind x) + try Some (x, Indrec.lookup_eliminator env ind x) with | _ -> None ) diff --git a/src/coq/logicutils/transformation/transform.mli b/src/coq/logicutils/transformation/transform.mli index 96ab44a..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 diff --git a/src/coq/representationutils/defutils.ml b/src/coq/representationutils/defutils.ml index 7cd9d1b..b987501 100644 --- a/src/coq/representationutils/defutils.ml +++ b/src/coq/representationutils/defutils.ml @@ -7,7 +7,6 @@ module CVars = Vars open Constr open Names open Evd -open Decl_kinds open Recordops open Constrexpr open Constrextern @@ -17,7 +16,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 refresh = let open EConstr in (* XXX: "Standard" term construction combinators such as `mkApp` don't add any universe constraints that may be needed later for @@ -47,37 +46,30 @@ let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook re 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 (CVars.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 sigma = Evd.minimize_universes sigma in (* todo: is this necessary/bad? *) + let sigma, ce = DeclareDef.prepare_definition ~allow_evars:true ~opaque ~poly sigma udecl ~types:tyopt ~body in let ubinders = Evd.universe_binders sigma in - let ce = Declare.definition_entry ?types:tyopt ~univs body in - let uctx = Evd.evar_universe_context sigma in - let hook_data = Option.map (fun hook -> hook, uctx, []) hook in - DeclareDef.declare_definition ~ontop:None ?hook_data ident k ce ubinders imps + let scope = DeclareDef.Global Declare.ImportDefaultBehavior in + let kind = Decls.(IsDefinition Definition) in + DeclareDef.declare_definition ~name:ident ~scope ~kind ?hook_data:hook ubinders ce imps + (* Define a new Coq term *) let define_term ?typ (n : Id.t) (evm : evar_map) (trm : types) (refresh : bool) = - let k = (Global, Attributes.is_universe_polymorphism(), Definition) in + let poly = Attributes.is_universe_polymorphism() in let udecl = UState.default_univ_decl 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 [] None refresh + edeclare n poly ~opaque:false evm udecl etrm etyp [] None refresh (* Define a Canonical Structure *) let define_canonical ?typ (n : Id.t) (evm : evar_map) (trm : types) (refresh : bool) = - let k = (Global, Attributes.is_universe_polymorphism (), CanonicalStructure) in + 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; ()) in + let hook = DeclareDef.Hook.make (fun x -> let open DeclareDef.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 [] (Some hook) refresh + edeclare n poly ~opaque:false evm udecl etrm etyp [] (Some (hook, Evd.evar_universe_context evm, [])) refresh (* todo: check if last empty list is correct to pass *) (* --- Converting between representations --- *) diff --git a/src/coq/termutils/constutils.ml b/src/coq/termutils/constutils.ml index b7cbfb5..69f1e2b 100644 --- a/src/coq/termutils/constutils.ml +++ b/src/coq/termutils/constutils.ml @@ -17,9 +17,10 @@ let make_constant id = * Safely extract the body of a constant, instantiating any universe variables *) let open_constant env const = - let (term, auctx) = Option.get @@ Global.body_of_constant const in - let instance, (_, constr) = UnivGen.fresh_instance auctx in - let uctx = Univ.UContext.make (instance, constr) 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" From 0921f9004f7c483b880e420ea9583e49749d8ffc Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Mon, 4 Dec 2023 11:33:46 -0700 Subject: [PATCH 33/44] Made changes to the API to match Coq 8.12 --- src/coq/logicutils/hofs/reducers.ml | 2 +- src/coq/logicutils/inductive/indutils.ml | 9 +++++---- src/coq/logicutils/transformation/transform.ml | 2 +- src/coq/logicutils/typesandequality/inference.ml | 2 +- src/coq/representationutils/defutils.ml | 12 ++++-------- 5 files changed, 12 insertions(+), 15 deletions(-) diff --git a/src/coq/logicutils/hofs/reducers.ml b/src/coq/logicutils/hofs/reducers.ml index 1b0b3ca..a92e255 100644 --- a/src/coq/logicutils/hofs/reducers.ml +++ b/src/coq/logicutils/hofs/reducers.ml @@ -120,7 +120,7 @@ let reduce_whd_if_let_in (env : env) sigma (trm : types) = if isLetIn trm then sigma, EConstr.to_constr 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/inductive/indutils.ml b/src/coq/logicutils/inductive/indutils.ml index 1c78ce3..b63383a 100644 --- a/src/coq/logicutils/inductive/indutils.ml +++ b/src/coq/logicutils/inductive/indutils.ml @@ -143,7 +143,7 @@ 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 @@ -168,7 +168,7 @@ let open_inductive ?(global=false) env (mind_body, ind_body) = 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_set false (Univ.ContextSet.of_context 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 (get_rel_ctx_name Name.Anonymous, arity)] in let ctors_typ = Array.map (recompose_prod_assum arity_ctx) ind_body.mind_user_lc in @@ -181,7 +181,6 @@ 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 @@ -192,7 +191,9 @@ let declare_inductive typename consnames template univs nparam arity constypes = mind_entry_inds = [ind_entry]; mind_entry_universes = univs; mind_entry_private = None; - mind_entry_variance = None } + mind_entry_template = template; + mind_entry_cumulative = true (* is this correct? *) + } in let mind = DeclareInd.declare_mutual_inductive_with_eliminations mind_entry UnivNames.empty_binders [] in (mind, 0) diff --git a/src/coq/logicutils/transformation/transform.ml b/src/coq/logicutils/transformation/transform.ml index 6d2c433..0cf6064 100644 --- a/src/coq/logicutils/transformation/transform.ml +++ b/src/coq/logicutils/transformation/transform.ml @@ -97,7 +97,7 @@ let try_register_record mod_path (ind, ind') = r.s_PROJ in (try - declare_structure_entry ((ind', 1), pks, ps) + 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")) diff --git a/src/coq/logicutils/typesandequality/inference.ml b/src/coq/logicutils/typesandequality/inference.ml index 135d7aa..c0512ea 100644 --- a/src/coq/logicutils/typesandequality/inference.ml +++ b/src/coq/logicutils/typesandequality/inference.ml @@ -24,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 b987501..300ddfd 100644 --- a/src/coq/representationutils/defutils.ml +++ b/src/coq/representationutils/defutils.ml @@ -2,8 +2,6 @@ * Utilities for defining terms *) -module CVars = Vars - open Constr open Names open Evd @@ -47,12 +45,10 @@ let edeclare ident poly ~opaque sigma udecl body tyopt imps hook refresh = sigma in let sigma = Evd.minimize_universes sigma in (* todo: is this necessary/bad? *) - let sigma, ce = DeclareDef.prepare_definition ~allow_evars:true ~opaque ~poly sigma udecl ~types:tyopt ~body in - let ubinders = Evd.universe_binders sigma in let scope = DeclareDef.Global Declare.ImportDefaultBehavior in let kind = Decls.(IsDefinition Definition) in - DeclareDef.declare_definition ~name:ident ~scope ~kind ?hook_data:hook ubinders ce imps - + DeclareDef.declare_definition ~name:ident ~scope ~kind ~opaque ~impargs:imps ~udecl:udecl ?hook:hook ~poly:poly ~types:tyopt ~body:body sigma + (* Check this change if something breaks later *) (* Define a new Coq term *) let define_term ?typ (n : Id.t) (evm : evar_map) (trm : types) (refresh : bool) = @@ -69,7 +65,7 @@ let define_canonical ?typ (n : Id.t) (evm : evar_map) (trm : types) (refresh : b let hook = DeclareDef.Hook.make (fun x -> let open DeclareDef.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 poly ~opaque:false evm udecl etrm etyp [] (Some (hook, Evd.evar_universe_context evm, [])) refresh (* todo: check if last empty list is correct to pass *) + edeclare n poly ~opaque:false evm udecl etrm etyp [] (Some hook) refresh (* todo: check if last empty list is correct to pass *) (* --- Converting between representations --- *) @@ -84,7 +80,7 @@ let intern env sigma t : evar_map * types = (* 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 : GlobRef.t) : constr_expr = From 9fd5b6f836d89dca8f86e52149a748de28612a22 Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Mon, 4 Dec 2023 12:46:16 -0700 Subject: [PATCH 34/44] Changed the cumulative flag to false to fix test errors in fix-to-elim --- src/coq/logicutils/inductive/indutils.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coq/logicutils/inductive/indutils.ml b/src/coq/logicutils/inductive/indutils.ml index b63383a..5ceba9c 100644 --- a/src/coq/logicutils/inductive/indutils.ml +++ b/src/coq/logicutils/inductive/indutils.ml @@ -192,7 +192,7 @@ let declare_inductive typename consnames template univs nparam arity constypes = mind_entry_universes = univs; mind_entry_private = None; mind_entry_template = template; - mind_entry_cumulative = true (* is this correct? *) + mind_entry_cumulative = false (* is this correct? *) } in let mind = DeclareInd.declare_mutual_inductive_with_eliminations mind_entry UnivNames.empty_binders [] in From c1e4acd8c4873d79762f38f92ad837c47ff974b5 Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Wed, 27 Mar 2024 12:46:01 -0500 Subject: [PATCH 35/44] First attempt at fixing declare_definition bug. --- src/coq/representationutils/defutils.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/coq/representationutils/defutils.ml b/src/coq/representationutils/defutils.ml index 300ddfd..69cf44b 100644 --- a/src/coq/representationutils/defutils.ml +++ b/src/coq/representationutils/defutils.ml @@ -34,21 +34,21 @@ let edeclare ident poly ~opaque sigma udecl body tyopt imps hook refresh = let env = Global.env () in let sigma = if refresh then - fst (Typing.type_of ~refresh:false env sigma body) + fst (Typing.type_of ~refresh:true env sigma body) else sigma in let sigma = if Option.has_some tyopt && refresh then - fst (Typing.type_of ~refresh:false env sigma (Option.get tyopt)) + fst (Typing.type_of ~refresh:true env sigma (Option.get tyopt)) else sigma in let sigma = Evd.minimize_universes sigma in (* todo: is this necessary/bad? *) - let scope = DeclareDef.Global Declare.ImportDefaultBehavior in + let udecl = UState.default_univ_decl in + let scope = Declare.Global Declare.ImportDefaultBehavior in let kind = Decls.(IsDefinition Definition) in - DeclareDef.declare_definition ~name:ident ~scope ~kind ~opaque ~impargs:imps ~udecl:udecl ?hook:hook ~poly:poly ~types:tyopt ~body:body sigma - (* Check this change if something breaks later *) + Declare.declare_definition ~name:ident ~scope ~kind ~opaque:opaque ~impargs:imps ~udecl ~poly ~types:tyopt ~body:body sigma (* Define a new Coq term *) let define_term ?typ (n : Id.t) (evm : evar_map) (trm : types) (refresh : bool) = From fc5357056477f681cbec73bc6a5d504d79261652 Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Wed, 27 Mar 2024 14:23:24 -0500 Subject: [PATCH 36/44] Passing false flag to EConstr.to_constr everywhere --- src/coq/decompiler/decompiler.ml | 2 +- src/coq/logicutils/hofs/reducers.ml | 14 +++++++------- src/coq/logicutils/typesandequality/inference.ml | 2 +- src/coq/representationutils/defutils.ml | 4 ++-- 4 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/coq/decompiler/decompiler.ml b/src/coq/decompiler/decompiler.ml index 4c47809..5af055c 100644 --- a/src/coq/decompiler/decompiler.ml +++ b/src/coq/decompiler/decompiler.ml @@ -332,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 diff --git a/src/coq/logicutils/hofs/reducers.ml b/src/coq/logicutils/hofs/reducers.ml index a92e255..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,20 +105,20 @@ 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 env sigma (EConstr.of_constr trm)) else diff --git a/src/coq/logicutils/typesandequality/inference.ml b/src/coq/logicutils/typesandequality/inference.ml index c0512ea..91a1b02 100644 --- a/src/coq/logicutils/typesandequality/inference.ml +++ b/src/coq/logicutils/typesandequality/inference.ml @@ -9,7 +9,7 @@ open Declarations let infer_type env sigma term = let eterm = EConstr.of_constr term in let sigma, typ = Typing.type_of ~refresh:true env sigma eterm in - sigma, EConstr.to_constr sigma typ + 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 = diff --git a/src/coq/representationutils/defutils.ml b/src/coq/representationutils/defutils.ml index 69cf44b..bf6c766 100644 --- a/src/coq/representationutils/defutils.ml +++ b/src/coq/representationutils/defutils.ml @@ -76,7 +76,7 @@ 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 = @@ -109,4 +109,4 @@ let constr_of_pglobal (glob, univs) = (* Safely instantiate a global reference, with proper universe handling *) let new_global sigma gref = let sigma, typ = Evarutil.new_global sigma gref in - sigma, EConstr.to_constr sigma typ + sigma, EConstr.to_constr ~abort_on_undefined_evars:false sigma typ From f06318154ed110c1d59c99a4df0e02bdfb1ff9e7 Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Wed, 27 Mar 2024 18:15:10 -0500 Subject: [PATCH 37/44] Using declare_entry instead of declare_definition. --- src/coq/representationutils/defutils.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/coq/representationutils/defutils.ml b/src/coq/representationutils/defutils.ml index bf6c766..652d538 100644 --- a/src/coq/representationutils/defutils.ml +++ b/src/coq/representationutils/defutils.ml @@ -45,10 +45,12 @@ let edeclare ident poly ~opaque sigma udecl body tyopt imps hook refresh = sigma in let sigma = Evd.minimize_universes sigma in (* todo: is this necessary/bad? *) - let udecl = UState.default_univ_decl in + let ubinders = Evd.universe_binders sigma in + let uctx = UState.of_binders ubinders in + let defent = Declare.definition_entry ~opaque:opaque (EConstr.to_constr ~abort_on_undefined_evars:false sigma body) in let scope = Declare.Global Declare.ImportDefaultBehavior in let kind = Decls.(IsDefinition Definition) in - Declare.declare_definition ~name:ident ~scope ~kind ~opaque:opaque ~impargs:imps ~udecl ~poly ~types:tyopt ~body:body sigma + Declare.declare_entry ~name:ident ~scope ~kind ~impargs:imps ~uctx:uctx defent (* Define a new Coq term *) let define_term ?typ (n : Id.t) (evm : evar_map) (trm : types) (refresh : bool) = From 603abccaab350ea5d4553b9c55f73fd9f9132ebe Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Wed, 3 Apr 2024 15:01:31 -0500 Subject: [PATCH 38/44] Remove undefined evars before calling declare_definition. --- src/coq/representationutils/defutils.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/coq/representationutils/defutils.ml b/src/coq/representationutils/defutils.ml index 652d538..d7b3b4d 100644 --- a/src/coq/representationutils/defutils.ml +++ b/src/coq/representationutils/defutils.ml @@ -45,12 +45,11 @@ let edeclare ident poly ~opaque sigma udecl body tyopt imps hook refresh = sigma in let sigma = Evd.minimize_universes sigma in (* todo: is this necessary/bad? *) - let ubinders = Evd.universe_binders sigma in - let uctx = UState.of_binders ubinders in - let defent = Declare.definition_entry ~opaque:opaque (EConstr.to_constr ~abort_on_undefined_evars:false sigma body) in + let udecl = UState.default_univ_decl in + let sigma = (Evd.fold_undefined (fun x _ sigma -> Evd.remove sigma x) sigma) sigma in let scope = Declare.Global Declare.ImportDefaultBehavior in let kind = Decls.(IsDefinition Definition) in - Declare.declare_entry ~name:ident ~scope ~kind ~impargs:imps ~uctx:uctx defent + Declare.declare_definition ~name:ident ~scope ~kind ~opaque:opaque ~impargs:imps ~udecl ~poly ~types:tyopt ~body:body sigma (* Define a new Coq term *) let define_term ?typ (n : Id.t) (evm : evar_map) (trm : types) (refresh : bool) = From 35de5ad423b0ca69894a5e9c5f9d91d226937116 Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Thu, 11 Apr 2024 12:57:39 -0500 Subject: [PATCH 39/44] Removed filter for sind. --- src/coq/logicutils/transformation/transform.ml | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/src/coq/logicutils/transformation/transform.ml b/src/coq/logicutils/transformation/transform.ml index 0cf6064..9a3e74e 100644 --- a/src/coq/logicutils/transformation/transform.ml +++ b/src/coq/logicutils/transformation/transform.ml @@ -116,13 +116,6 @@ let lookup_eliminator_error_handling ind sorts = ) sorts) -let contains s1 s2 = - let re = Str.regexp_string s2 in - try - ignore (Str.search_forward re s1 0); - true - with Not_found -> false - (* * Declare a new module structure under the given name with the compositionally * transformed (i.e., forward-substituted) components from the given module @@ -147,7 +140,7 @@ let transform_module_structure ?(init=const GlobRef.Map.empty) ?(opaques=GlobRef match b with | SFBconst const_body -> let const = Constant.make2 mod_path l in - not (GlobRef.Set.mem (GlobRef.ConstRef const) opaques) && not (contains (Label.to_string l) ("sind")) + not (GlobRef.Set.mem (GlobRef.ConstRef const) opaques) | _ -> true) mod_elems From 3ff1c966893c3a1204393f1bbde25a431f57fb08 Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Mon, 15 Apr 2024 14:16:31 -0500 Subject: [PATCH 40/44] First batch of changes for coq 8.13 --- src/coq/devutils/printing.ml | 2 +- src/coq/logicutils/hofs/hofs.ml | 16 ++++++++-------- src/coq/logicutils/hofs/substitution.ml | 4 ++-- src/coq/logicutils/inductive/indutils.ml | 2 +- src/coq/logicutils/transformation/transform.ml | 2 +- src/coq/representationutils/defutils.ml | 9 +++++---- 6 files changed, 18 insertions(+), 17 deletions(-) diff --git a/src/coq/devutils/printing.ml b/src/coq/devutils/printing.ml index cd55f74..c0a9663 100644 --- a/src/coq/devutils/printing.ml +++ b/src/coq/devutils/printing.ml @@ -131,7 +131,7 @@ let rec term_as_string (env : env) (trm : types) = (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 diff --git a/src/coq/logicutils/hofs/hofs.ml b/src/coq/logicutils/hofs/hofs.ml index 1b94a96..87ef031 100644 --- a/src/coq/logicutils/hofs/hofs.ml +++ b/src/coq/logicutils/hofs/hofs.ml @@ -157,11 +157,11 @@ let map_term_env_rec map_rec f d env sigma a trm = 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 *) @@ -226,11 +226,11 @@ let map_subterms_env_rec map_rec f d env sigma a trm = 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 *) @@ -322,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 *) @@ -498,7 +498,7 @@ let rec map_term_env_if_list p f d env sigma a trm = 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 @@ -583,7 +583,7 @@ let rec exists_subterm_env p d env sigma (a : 'a) (trm : types) : evar_map * boo 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/substitution.ml b/src/coq/logicutils/hofs/substitution.ml index b63e8f8..f72c5bb 100644 --- a/src/coq/logicutils/hofs/substitution.ml +++ b/src/coq/logicutils/hofs/substitution.ml @@ -130,13 +130,13 @@ let rec subst_globals subst (term : constr) = 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/inductive/indutils.ml b/src/coq/logicutils/inductive/indutils.ml index 5ceba9c..585da88 100644 --- a/src/coq/logicutils/inductive/indutils.ml +++ b/src/coq/logicutils/inductive/indutils.ml @@ -186,13 +186,13 @@ let declare_inductive typename consnames template univs nparam arity constypes = in let mind_entry = { mind_entry_record = None; + mind_entry_variance = None; mind_entry_finite = Declarations.Finite; mind_entry_params = params; mind_entry_inds = [ind_entry]; mind_entry_universes = univs; mind_entry_private = None; mind_entry_template = template; - mind_entry_cumulative = false (* is this correct? *) } in let mind = DeclareInd.declare_mutual_inductive_with_eliminations mind_entry UnivNames.empty_binders [] in diff --git a/src/coq/logicutils/transformation/transform.ml b/src/coq/logicutils/transformation/transform.ml index 9a3e74e..eb29769 100644 --- a/src/coq/logicutils/transformation/transform.ml +++ b/src/coq/logicutils/transformation/transform.ml @@ -97,7 +97,7 @@ let try_register_record mod_path (ind, ind') = r.s_PROJ in (try - declare_structure_entry {s_CONST = (ind',1); s_EXPECTEDPARAM = r.s_EXPECTEDPARAM; s_PROJKIND = pks; s_PROJ = 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")) diff --git a/src/coq/representationutils/defutils.ml b/src/coq/representationutils/defutils.ml index d7b3b4d..9251bd7 100644 --- a/src/coq/representationutils/defutils.ml +++ b/src/coq/representationutils/defutils.ml @@ -5,7 +5,6 @@ open Constr open Names open Evd -open Recordops open Constrexpr open Constrextern @@ -47,9 +46,11 @@ let edeclare ident poly ~opaque sigma udecl body tyopt imps hook refresh = 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 = Declare.Global Declare.ImportDefaultBehavior in + let scope = Locality.Global Locality.ImportDefaultBehavior in let kind = Decls.(IsDefinition Definition) in - Declare.declare_definition ~name:ident ~scope ~kind ~opaque:opaque ~impargs:imps ~udecl ~poly ~types:tyopt ~body:body sigma + 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) = @@ -63,7 +64,7 @@ let define_term ?typ (n : Id.t) (evm : evar_map) (trm : types) (refresh : bool) let define_canonical ?typ (n : Id.t) (evm : evar_map) (trm : types) (refresh : bool) = let poly = Attributes.is_universe_polymorphism() in let udecl = UState.default_univ_decl in - let hook = DeclareDef.Hook.make (fun x -> let open DeclareDef.Hook.S in Canonical.declare_canonical_structure x.dref) 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 poly ~opaque:false evm udecl etrm etyp [] (Some hook) refresh (* todo: check if last empty list is correct to pass *) From 25774f7065ba7814f0352bca6dbc1aa611b9ad98 Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Tue, 30 Apr 2024 15:06:30 -0500 Subject: [PATCH 41/44] Removed the refresh flag from the define_term and define_canonical interfaces since we dont use the results anyway. --- .../logicutils/transformation/transform.ml | 2 +- src/coq/representationutils/defutils.ml | 22 +++++-------------- src/coq/representationutils/defutils.mli | 4 ++-- 3 files changed, 9 insertions(+), 19 deletions(-) diff --git a/src/coq/logicutils/transformation/transform.ml b/src/coq/logicutils/transformation/transform.ml index eb29769..bdccdf3 100644 --- a/src/coq/logicutils/transformation/transform.ml +++ b/src/coq/logicutils/transformation/transform.ml @@ -54,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 diff --git a/src/coq/representationutils/defutils.ml b/src/coq/representationutils/defutils.ml index 9251bd7..74194f2 100644 --- a/src/coq/representationutils/defutils.ml +++ b/src/coq/representationutils/defutils.ml @@ -13,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 ~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 @@ -31,17 +31,7 @@ let edeclare ident poly ~opaque sigma udecl body tyopt imps hook refresh = canonical structure resolution and what not. *) let env = Global.env () in - let sigma = - if refresh then - fst (Typing.type_of ~refresh:true env sigma body) - else - sigma - in - let sigma = - if Option.has_some tyopt && refresh then - fst (Typing.type_of ~refresh:true env sigma (Option.get tyopt)) - else - sigma + let sigma = fst (Typing.type_of env sigma body) in let sigma = Evd.minimize_universes sigma in (* todo: is this necessary/bad? *) let udecl = UState.default_univ_decl in @@ -53,21 +43,21 @@ let edeclare ident poly ~opaque sigma udecl body tyopt imps hook refresh = 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 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 etrm = EConstr.of_constr trm in let etyp = Option.map EConstr.of_constr typ in - edeclare n poly ~opaque:false evm udecl etrm etyp [] None 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 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 = 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 poly ~opaque:false evm udecl etrm etyp [] (Some hook) refresh (* todo: check if last empty list is correct to pass *) + edeclare n poly ~opaque:false evm udecl etrm etyp [] (Some hook) (* --- Converting between representations --- *) diff --git a/src/coq/representationutils/defutils.mli b/src/coq/representationutils/defutils.mli index 1ff75a6..509802f 100644 --- a/src/coq/representationutils/defutils.mli +++ b/src/coq/representationutils/defutils.mli @@ -16,12 +16,12 @@ open Constrexpr * (Refreshing universes is REALLY costly) *) val define_term : - ?typ:types -> Id.t -> evar_map -> types -> bool -> GlobRef.t + ?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 -> GlobRef.t + ?typ:types -> Id.t -> evar_map -> types -> GlobRef.t (* --- Converting between representations --- *) From 642f7ba6fbc891204f6ca2f9d97c2c2034751cde Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Tue, 30 Apr 2024 15:34:13 -0500 Subject: [PATCH 42/44] Call Typing.type_of in case tyopt is not None. --- src/coq/representationutils/defutils.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/coq/representationutils/defutils.ml b/src/coq/representationutils/defutils.ml index 74194f2..6c5e67c 100644 --- a/src/coq/representationutils/defutils.ml +++ b/src/coq/representationutils/defutils.ml @@ -31,8 +31,12 @@ let edeclare ident poly ~opaque sigma udecl body tyopt imps hook = canonical structure resolution and what not. *) let env = Global.env () in - let sigma = fst (Typing.type_of env sigma body) - in + let sigma = + 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 (* 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 From 48a735ad820bd2f9e9e78aebf88e052ac646cf39 Mon Sep 17 00:00:00 2001 From: Arpan Agrawal Date: Tue, 30 Apr 2024 15:36:27 -0500 Subject: [PATCH 43/44] Preserve original typing call. --- src/coq/representationutils/defutils.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/coq/representationutils/defutils.ml b/src/coq/representationutils/defutils.ml index 6c5e67c..b369d42 100644 --- a/src/coq/representationutils/defutils.ml +++ b/src/coq/representationutils/defutils.ml @@ -31,6 +31,8 @@ let edeclare ident poly ~opaque sigma udecl body tyopt imps hook = canonical structure resolution and what not. *) let env = Global.env () in + let sigma = fst (Typing.type_of env sigma body) + in let sigma = if Option.has_some tyopt then fst (Typing.type_of env sigma (Option.get tyopt)) From 7c7af85beaf7cb74144db2ce1523fc461b55b15d Mon Sep 17 00:00:00 2001 From: Arpan Agrawal <112970424+agrarpan@users.noreply.github.com> Date: Wed, 17 Jul 2024 04:28:41 -0500 Subject: [PATCH 44/44] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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.