From 6eafc6f330cefe3b63c3e6a81c80a8dbafd483e4 Mon Sep 17 00:00:00 2001 From: Talia Ringer Date: Thu, 9 Aug 2018 18:46:50 -0700 Subject: [PATCH] remove deprecated code and various other warnings --- .../components/abstraction/abstracters.ml | 14 ++++------ .../components/abstraction/abstracters.mli | 2 +- .../components/abstraction/abstraction.ml | 22 ++++++--------- .../components/abstraction/abstraction.mli | 5 +--- .../abstraction/abstractionconfig.ml | 21 +++++++------- .../abstraction/abstractionconfig.mli | 3 +- .../differencing/appdifferencers.ml | 28 +++++++++---------- .../differencing/changedetectors.ml | 3 +- .../components/differencing/differencers.ml | 2 +- .../components/differencing/differencers.mli | 2 +- .../components/differencing/differencing.ml | 5 ---- .../differencing/fixdifferencers.ml | 15 +++++----- .../differencing/higherdifferencers.ml | 4 +-- .../differencing/inddifferencers.ml | 2 -- .../differencing/proofdifferencers.ml | 14 ++++------ .../core/components/factoring/factoring.ml | 7 ++--- .../core/components/factoring/factoring.mli | 2 +- .../core/components/inversion/inverting.ml | 11 ++++---- .../core/components/inversion/inverting.mli | 2 +- .../specialization/specialization.ml | 4 +-- .../specialization/specialization.mli | 2 +- plugin/src/core/configuration/searchopts.ml | 10 +++---- plugin/src/core/configuration/searchopts.mli | 3 +- plugin/src/core/procedures/search.ml | 3 +- plugin/src/core/procedures/search.mli | 2 +- plugin/src/core/procedures/theorem.ml | 9 +++--- plugin/src/core/procedures/theorem.mli | 2 +- plugin/src/library/coq/coqenvs.ml | 4 +-- plugin/src/library/coq/coqenvs.mli | 4 +-- plugin/src/library/coq/coqterms.ml | 16 +++++------ plugin/src/library/coq/coqterms.mli | 6 ++-- plugin/src/library/coq/debruijn.ml | 7 ++--- plugin/src/library/coq/debruijn.mli | 2 +- plugin/src/library/coq/filters.ml | 6 ++-- plugin/src/library/coq/filters.mli | 3 +- plugin/src/library/coq/hofs.ml | 27 ++++++++---------- plugin/src/library/coq/hofs.mli | 2 +- plugin/src/library/coq/printing.ml | 27 ++++++++---------- plugin/src/library/coq/printing.mli | 4 +-- plugin/src/library/coq/reducers.ml | 8 +++--- plugin/src/library/coq/reducers.mli | 2 +- plugin/src/library/coq/substitution.ml | 5 +--- plugin/src/library/coq/substitution.mli | 6 +--- .../proofsearch/compilation/evaluation.ml | 7 ++--- .../proofsearch/compilation/evaluation.mli | 2 +- .../proofsearch/compilation/expansion.ml | 12 ++++---- .../proofsearch/compilation/expansion.mli | 8 +----- .../proofsearch/compilation/proofdiff.ml | 22 ++++++--------- .../proofsearch/compilation/proofdiff.mli | 4 +-- .../proofsearch/compilation/zooming.ml | 9 +----- .../proofsearch/compilation/zooming.mli | 6 ++-- .../proofsearch/representation/assumptions.ml | 16 +++++------ .../representation/assumptions.mli | 3 +- .../proofsearch/representation/candidates.ml | 2 +- .../proofsearch/representation/candidates.mli | 2 +- .../proofsearch/representation/cutlemma.ml | 6 ++-- .../proofsearch/representation/cutlemma.mli | 2 +- .../representation/kindofchange.ml | 2 +- .../representation/kindofchange.mli | 2 +- .../proofsearch/representation/merging.ml | 3 +- .../proofsearch/representation/merging.mli | 2 +- .../proofsearch/representation/proofcat.ml | 4 +-- .../proofsearch/representation/proofcat.mli | 3 +- .../representation/proofcatterms.ml | 22 ++------------- .../representation/proofcatterms.mli | 3 +- plugin/src/library/utilities/collections.ml | 8 ++++-- plugin/src/patcher.ml4 | 18 ++++++------ 67 files changed, 203 insertions(+), 293 deletions(-) diff --git a/plugin/src/core/components/abstraction/abstracters.ml b/plugin/src/core/components/abstraction/abstracters.ml index 9c0253f..47448cd 100644 --- a/plugin/src/core/components/abstraction/abstracters.ml +++ b/plugin/src/core/components/abstraction/abstracters.ml @@ -1,12 +1,10 @@ (* --- Abstraction Strategies --- *) -open Term +open Constr open Environ open Coqterms open Collections open Substitution -open Debruijn -open Printing open Reducers open Filters open Candidates @@ -29,7 +27,7 @@ type abstraction_strategy = * Do not consider lambdas. *) let rec num_apps (trm : types) : int = - match kind_of_term trm with + match kind trm with | App (f, args) -> Array.fold_left (fun n a -> n + num_apps a) (1 + num_apps f) args | _ -> @@ -91,7 +89,7 @@ let kind_of_abstraction strategy = strategy.to_abstract (* Fully abstract each term, substituting every convertible subterm *) let syntactic_full (env : env) (arg_actual : types) (arg_abstract : types) (trms : candidates) : candidates = - if eq_constr arg_actual arg_abstract then + if equal arg_actual arg_abstract then trms else List.map (all_conv_substs env (arg_actual, arg_abstract)) trms @@ -101,7 +99,7 @@ let syntactic_full_strategy : abstracter = (* Fully abstract each term, substituting every subterm w/ convertible types *) let types_full (env : env) (arg_actual : types) (arg_abstract : types) (trms : candidates) : candidates = - if eq_constr arg_actual arg_abstract then + if equal arg_actual arg_abstract then trms else List.map (all_typ_substs env (arg_actual, arg_abstract)) trms @@ -113,7 +111,7 @@ let types_full_strategy : abstracter = let pattern_full (env : env) (arg_actual : types) (arg_abstract : types) (trms : types list) : types list = let types_conv = types_convertible env arg_abstract in let exists_types_conv = List.exists types_conv in - match map_tuple kind_of_term (arg_actual, arg_abstract) with + match map_tuple kind (arg_actual, arg_abstract) with | (App (f, args), _) when exists_types_conv (Array.to_list args) -> let arg = List.find types_conv (Array.to_list args) in let sub = all_constr_substs env f in @@ -126,7 +124,7 @@ let pattern_full_strategy : abstracter = (* All combinations of abstractions of convertible subterms *) let syntactic_all_combinations (env : env) (arg_actual : types) (arg_abstract : types) (trms : candidates) : candidates = - if eq_constr arg_actual arg_abstract then + if equal arg_actual arg_abstract then trms else flat_map (all_conv_substs_combs env (arg_actual, arg_abstract)) trms diff --git a/plugin/src/core/components/abstraction/abstracters.mli b/plugin/src/core/components/abstraction/abstracters.mli index 263e64f..6628247 100644 --- a/plugin/src/core/components/abstraction/abstracters.mli +++ b/plugin/src/core/components/abstraction/abstracters.mli @@ -1,6 +1,6 @@ (* --- Abstraction Strategies --- *) -open Term +open Constr open Environ open Candidates diff --git a/plugin/src/core/components/abstraction/abstraction.ml b/plugin/src/core/components/abstraction/abstraction.ml index 4e2b7f0..dee56a5 100644 --- a/plugin/src/core/components/abstraction/abstraction.ml +++ b/plugin/src/core/components/abstraction/abstraction.ml @@ -4,17 +4,13 @@ open Proofcatterms open Abstracters open Abstractionconfig open Environ -open Term +open Constr open Debruijn open Coqterms -open Printing open Collections open Reducers open Specialization -open Coqenvs -open Utilities open Candidates -open Coqenvs open Proofdiff open Searchopts open Cutlemma @@ -43,7 +39,7 @@ let generalize (env : env) (num_to_abstract : int) (cs : candidates) : candidate (fun _ (en, l) -> let typ = unshift (infer_type en (mkRel 1)) in let env_pop = Environ.pop_rel_context 1 en in - (env_pop, List.map (fun b -> mkLambda (Anonymous, typ, b)) l)) + (env_pop, List.map (fun b -> mkLambda (Names.Name.Anonymous, typ, b)) l)) (range 1 (num_to_abstract + 1)) (env, cs)) @@ -56,7 +52,7 @@ let get_prop_abstract_goal_type (config : abstraction_config) = let prop = mkRel (nb_rel env) in let base = mkApp (prop, Array.of_list config.args_base) in let goal = mkApp (prop, Array.of_list config.args_goal) in - let goal_type_env = mkProd (Anonymous, base, shift goal) in + let goal_type_env = mkProd (Names.Name.Anonymous, base, shift goal) in reconstruct_prod env goal_type_env (* @@ -78,7 +74,7 @@ let get_arg_abstract_goal_type (config : abstraction_config) : types = | (Prod (n_b, t_b, b_b), Prod (_, _, b_g)) -> mkProd (n_b, t_b, infer_goal b_b b_g) | _ -> - mkProd (Anonymous, b, shift g) + mkProd (Names.Name.Anonymous, b, shift g) in infer_goal config.f_base config.f_goal (* @@ -109,7 +105,7 @@ let get_abstraction_args config : closure = if i = 0 then (en, []) else - match kind_of_term g with + match kind g with | Lambda (n, t, b) -> let en' = push_rel CRD.(LocalAssum(n, t)) en in let (en'', b') = infer_args (i - 1) en' b in @@ -228,12 +224,12 @@ let abstract_case (opts : options) (d : goal_case_diff) cs : candidates = let old_goal = old_proof d_goal in let env = context_env old_goal in match get_change opts with - | Hypothesis (_, _) -> + | Kindofchange.Hypothesis (_, _) -> let (g_o, g_n) = map_tuple context_term (old_goal, new_proof d_goal) in - filter_by_type env (mkProd (Anonymous, g_n, shift g_o)) cs - | InductiveType (_, _) -> + filter_by_type env (mkProd (Names.Name.Anonymous, g_n, shift g_o)) cs + | Kindofchange.InductiveType (_, _) -> cs - | FixpointCase ((_, _), cut) when are_cut env cut cs -> + | Kindofchange.FixpointCase ((_, _), cut) when are_cut env cut cs -> cs | _ -> try_abstract_inductive d_goal cs diff --git a/plugin/src/core/components/abstraction/abstraction.mli b/plugin/src/core/components/abstraction/abstraction.mli index 4a41131..45aa7e1 100644 --- a/plugin/src/core/components/abstraction/abstraction.mli +++ b/plugin/src/core/components/abstraction/abstraction.mli @@ -1,9 +1,6 @@ (* --- Abstraction Component --- *) -open Abstracters -open Environ -open Term -open Coqterms +open Constr open Candidates open Abstractionconfig open Proofdiff diff --git a/plugin/src/core/components/abstraction/abstractionconfig.ml b/plugin/src/core/components/abstraction/abstractionconfig.ml index 9995b36..3337b1b 100644 --- a/plugin/src/core/components/abstraction/abstractionconfig.ml +++ b/plugin/src/core/components/abstraction/abstractionconfig.ml @@ -1,13 +1,10 @@ open Environ -open Term +open Constr open Abstracters open Candidates open Coqterms open Debruijn open Collections -open Searchopts -open Reducers -open Printing open Proofdiff open Cutlemma @@ -53,7 +50,7 @@ let rec configure_goal_body env goal c : abstraction_config = let cs = [c] in let args_base = Array.to_list (snd (destApp gt)) in let args_goal = List.map unshift (Array.to_list (snd (destApp gb))) in - if List.for_all2 eq_constr args_base args_goal then (* argument *) + if List.for_all2 equal args_base args_goal then (* argument *) if isApp ctt then let f_goal = unshift (unwrap_definition env (fst (destApp gb))) in let f_base = unwrap_definition env (fst (destApp gt)) in @@ -97,7 +94,7 @@ let configure_args env (d_type : types proof_diff) cs = * top-level *) let rec apply_prop pi goal = - match kind_of_term goal with + match kind goal with | Prod (n, t, b) when isProd b -> mkProd (n, t, apply_prop (shift_i pi) b) | Prod (n, t, b) -> @@ -105,6 +102,8 @@ let rec apply_prop pi goal = let t_args = singleton_array t in let b_args = singleton_array b in mkProd (n, mkApp (p, t_args), mkApp (shift p, b_args)) + | _ -> + failwith "called apply_prop on a non-product" (* * Push the function to abstract into the environment @@ -112,12 +111,12 @@ let rec apply_prop pi goal = * We should check this is actually well-typed *) let rec push_prop env typ : env = - match kind_of_term typ with + match kind typ with | Prod (n, t, b) -> push_prop (push_rel CRD.(LocalAssum(n, t)) env) b | App (f, _) -> push_rel - CRD.(LocalAssum(Anonymous, infer_type env f)) + CRD.(LocalAssum(Names.Name.Anonymous, infer_type env f)) (pop_rel_context (nb_rel env) env) | _ -> failwith "Could not find function to abstract" @@ -141,12 +140,12 @@ let configure_fixpoint_cases env (diffs : types list) (cs : candidates) = (* Given some cut lemma application, configure arguments to abstract *) let rec configure_args_cut_app env (app : types) cs : abstraction_config = - match kind_of_term app with + match kind app with | Lambda (n, t, b) -> configure_args_cut_app (push_rel CRD.(LocalAssum(n, t)) env) b cs | App (f, args) -> let rec get_lemma_functions typ = - match kind_of_term typ with + match kind typ with | Prod (n, t, b) when isProd b -> let (f_base, f_goal) = get_lemma_functions b in (mkLambda (n, t, f_base), mkLambda (n, t, f_goal)) @@ -168,7 +167,7 @@ let configure_cut_args env (cut : cut_lemma) (cs : candidates) = let cs = filter_consistent_cut env cut cs in if List.length cs > 0 then let (_, _, b) = destLambda (get_app cut) in - let env_cut = push_rel CRD.(LocalAssum(Anonymous, get_lemma cut)) env in + let env_cut = push_rel CRD.(LocalAssum(Names.Name.Anonymous, get_lemma cut)) env in configure_args_cut_app env_cut b cs else failwith "No candidates are consistent with the cut lemma type" diff --git a/plugin/src/core/components/abstraction/abstractionconfig.mli b/plugin/src/core/components/abstraction/abstractionconfig.mli index bec5142..f11dd38 100644 --- a/plugin/src/core/components/abstraction/abstractionconfig.mli +++ b/plugin/src/core/components/abstraction/abstractionconfig.mli @@ -1,8 +1,7 @@ open Environ -open Term +open Constr open Abstracters open Candidates -open Searchopts open Proofdiff open Cutlemma diff --git a/plugin/src/core/components/differencing/appdifferencers.ml b/plugin/src/core/components/differencing/appdifferencers.ml index 902e47f..79f13e0 100644 --- a/plugin/src/core/components/differencing/appdifferencers.ml +++ b/plugin/src/core/components/differencing/appdifferencers.ml @@ -1,12 +1,11 @@ (* --- Recursive Differencers for Application --- *) -open Term +open Constr open Proofcatterms open Proofdiff open Candidates open Searchopts open Coqterms -open Differencers open Collections open Proofdifferencers open Higherdifferencers @@ -14,7 +13,6 @@ open Assumptions open Cutlemma open Specialization open Zooming -open Printing open Debruijn open Filters @@ -65,9 +63,9 @@ let diff_app diff_f diff_arg opts (d : goal_proof_diff) : candidates = let d_f = difference f_o f_n no_assumptions in let d_args = difference args_o args_n no_assumptions in (match get_change opts with - | InductiveType (_, _) -> + | Kindofchange.InductiveType (_, _) -> diff_rec diff_f opts d_f - | FixpointCase ((_, _), cut) -> + | Kindofchange.FixpointCase ((_, _), cut) -> let filter_diff_cut diff = filter_diff (filter_cut env cut) diff in let fs = filter_diff_cut (diff_rec diff_f opts) d_f in if non_empty fs then @@ -75,7 +73,7 @@ let diff_app diff_f diff_arg opts (d : goal_proof_diff) : candidates = else let d_args_rev = reverse d_args in filter_diff_cut (diff_map_flat (diff_rec diff_arg opts)) d_args_rev - | ConclusionCase cut when isConstruct f_o && isConstruct f_n -> + | Kindofchange.ConclusionCase cut when isConstruct f_o && isConstruct f_n -> let diff_arg o d = if no_diff o d then give_up else diff_arg o d in filter_diff (fun args -> @@ -84,13 +82,13 @@ let diff_app diff_f diff_arg opts (d : goal_proof_diff) : candidates = filter_applies_cut env (Option.get cut) args_lambdas else args) - (diff_map_flat (diff_rec diff_arg (set_change opts Conclusion))) + (diff_map_flat (diff_rec diff_arg (set_change opts Kindofchange.Conclusion))) d_args - | Hypothesis (_, _) -> + | Kindofchange.Hypothesis (_, _) -> let old_goal = fst (old_proof d) in let new_goal = fst (new_proof d) in let (g_o, g_n) = map_tuple context_term (old_goal, new_goal) in - let goal_type = mkProd (Anonymous, g_n, shift g_o) in + let goal_type = mkProd (Names.Name.Anonymous, g_n, shift g_o) in let filter_goal = filter_by_type env goal_type in let filter_diff_h diff = filter_diff filter_goal diff in let fs = filter_diff_h (diff_rec diff_f opts) d_f in @@ -98,7 +96,7 @@ let diff_app diff_f diff_arg opts (d : goal_proof_diff) : candidates = fs else filter_diff_h (diff_map_flat (diff_rec diff_arg opts)) d_args - | Conclusion -> + | Kindofchange.Conclusion -> if args_convertible env args_o args_n then let specialize = specialize_using specialize_no_reduce env in let combine_app = combine_cartesian specialize in @@ -106,7 +104,9 @@ let diff_app diff_f diff_arg opts (d : goal_proof_diff) : candidates = let args = Array.map (fun a_o -> [a_o]) args_o in combine_app fs (combine_cartesian_append args) else - give_up) + give_up + | _ -> + give_up) | _ -> give_up @@ -130,9 +130,9 @@ let diff_app_ind diff_ind diff_arg opts (d : goal_proof_diff) : candidates = let (n, npms_new, args_n) = new_proof d_zoom in let f = diff_ind opts (difference (o, npms_old) (n, npms_new) assums) in match get_change opts with - | (InductiveType (_, _)) | (Hypothesis (_, _)) -> + | (Kindofchange.InductiveType (_, _)) | (Kindofchange.Hypothesis (_, _)) -> f - | FixpointCase ((_, _), cut) -> + | Kindofchange.FixpointCase ((_, _), cut) -> let env = context_env (fst (old_proof d)) in let filter_diff_cut diff = filter_diff (filter_cut env cut) diff in if non_empty f then @@ -148,7 +148,7 @@ let diff_app_ind diff_ind diff_arg opts (d : goal_proof_diff) : candidates = let (_, prop_trm_ext, _) = prop o npms_old in let prop_trm = ext_term prop_trm_ext in let rec prop_arity p = - match kind_of_term p with + match kind p with | Lambda (_, _, b) -> 1 + prop_arity b | Prod (_, _, b) -> diff --git a/plugin/src/core/components/differencing/changedetectors.ml b/plugin/src/core/components/differencing/changedetectors.ml index 85eb802..d69e6bf 100644 --- a/plugin/src/core/components/differencing/changedetectors.ml +++ b/plugin/src/core/components/differencing/changedetectors.ml @@ -1,12 +1,11 @@ (* --- Change detectors --- *) -open Term +open Constr open Environ open Coqterms open Proofdiff open Proofcatterms open Cutlemma -open Differencers open Kindofchange open Reducers open Assumptions diff --git a/plugin/src/core/components/differencing/differencers.ml b/plugin/src/core/components/differencing/differencers.ml index c76e396..c73501d 100644 --- a/plugin/src/core/components/differencing/differencers.ml +++ b/plugin/src/core/components/differencing/differencers.ml @@ -1,6 +1,6 @@ (* --- Type definitions for differencers --- *) -open Term +open Constr open Proofdiff open Candidates open Proofcat diff --git a/plugin/src/core/components/differencing/differencers.mli b/plugin/src/core/components/differencing/differencers.mli index 84d32c3..807fcf5 100644 --- a/plugin/src/core/components/differencing/differencers.mli +++ b/plugin/src/core/components/differencing/differencers.mli @@ -1,6 +1,6 @@ (* --- Type definitions for differencers --- *) -open Term +open Constr open Proofdiff open Candidates open Proofcat diff --git a/plugin/src/core/components/differencing/differencing.ml b/plugin/src/core/components/differencing/differencing.ml index d2f1ec8..bee8c52 100644 --- a/plugin/src/core/components/differencing/differencing.ml +++ b/plugin/src/core/components/differencing/differencing.ml @@ -12,12 +12,7 @@ open Proofdifferencers open Higherdifferencers open Appdifferencers open Inddifferencers -open Proofcatterms -open Debruijn -open Expansion -open Utilities open Term -open Collections (* --- Debugging --- *) diff --git a/plugin/src/core/components/differencing/fixdifferencers.ml b/plugin/src/core/components/differencing/fixdifferencers.ml index 9201b41..853243d 100644 --- a/plugin/src/core/components/differencing/fixdifferencers.ml +++ b/plugin/src/core/components/differencing/fixdifferencers.ml @@ -1,7 +1,7 @@ (* --- Differencing of Fixpoints --- *) open Collections -open Term +open Constr open Environ open Coqterms open Coqenvs @@ -10,7 +10,6 @@ open Candidates open Reducers open Assumptions open Debruijn -open Differencers open Higherdifferencers module CRD = Context.Rel.Declaration @@ -33,7 +32,7 @@ let rec get_goal_fix env (d : types proof_diff) : candidates = let old_term = old_proof d in let new_term = new_proof d in let assums = assumptions d in - if eq_constr old_term new_term then + if equal old_term new_term then give_up else match kinds_of_terms (old_term, new_term) with @@ -47,11 +46,11 @@ let rec get_goal_fix env (d : types proof_diff) : candidates = let red_old = reduce_hd (old_proof d) in let red_new = reduce_hd (new_proof d) in match kinds_of_terms (red_old, red_new) with - | (App (f1, args1), App (f2, args2)) when eq_constr f1 f2 -> + | (App (f1, args1), App (f2, args2)) when equal f1 f2 -> let d_args = difference args1 args2 no_assumptions in diff_map_flat get_goal_reduced d_args - | _ when not (eq_constr red_old red_new) -> - [reduce_unfold env (mkProd (Anonymous, red_old, shift red_new))] + | _ when not (equal red_old red_new) -> + [reduce_unfold env (mkProd (Names.Name.Anonymous, red_old, shift red_new))] | _ -> give_up in get_goal_reduced (difference old_term new_term no_assumptions) @@ -67,7 +66,7 @@ let rec diff_fix_case env (d : types proof_diff) : candidates = diff_fix_case (push_rel CRD.(LocalAssum(n1, t1)) env) (difference b1 b2 assums) | (Case (_, ct1, m1, bs1), Case (_, ct2, m2, bs2)) when conv m1 m2 -> if same_length bs1 bs2 then - let env_m = push_rel CRD.(LocalAssum(Anonymous, m1)) env in + let env_m = push_rel CRD.(LocalAssum(Names.Name.Anonymous, m1)) env in let diff_bs = diff_map_flat (get_goal_fix env_m) in List.map unshift @@ -102,7 +101,7 @@ let diff_fix_cases env (d : types proof_diff) : candidates = List.map (fun t -> mkApp (t, singleton_array new_term)) lambdas - in unique eq_constr (reduce_all reduce_term env apps) + in unique equal (reduce_all reduce_term env apps) else failwith "Cannot infer goals for generalizing change in definition" | _ -> diff --git a/plugin/src/core/components/differencing/higherdifferencers.ml b/plugin/src/core/components/differencing/higherdifferencers.ml index 8a8af7d..5c6ca92 100644 --- a/plugin/src/core/components/differencing/higherdifferencers.ml +++ b/plugin/src/core/components/differencing/higherdifferencers.ml @@ -1,4 +1,4 @@ -open Term +open Constr open Proofdiff open Collections open Candidates @@ -32,7 +32,7 @@ let diff_reduced diff d = let (o, n) = proof_terms d in let d_red = reduce_diff reduce_term d in let (o_red, n_red) = proof_terms d_red in - if not ((eq_constr o o_red) && (eq_constr n n_red)) then + if not ((equal o o_red) && (equal n n_red)) then diff d_red else give_up diff --git a/plugin/src/core/components/differencing/inddifferencers.ml b/plugin/src/core/components/differencing/inddifferencers.ml index 8356081..06c838b 100644 --- a/plugin/src/core/components/differencing/inddifferencers.ml +++ b/plugin/src/core/components/differencing/inddifferencers.ml @@ -12,9 +12,7 @@ open Debruijn open Kindofchange open Searchopts open Abstraction -open Differencers open Expansion -open Printing open Environ (* --- Cases --- *) diff --git a/plugin/src/core/components/differencing/proofdifferencers.ml b/plugin/src/core/components/differencing/proofdifferencers.ml index 7898ca2..a6b4c21 100644 --- a/plugin/src/core/components/differencing/proofdifferencers.ml +++ b/plugin/src/core/components/differencing/proofdifferencers.ml @@ -1,18 +1,16 @@ (* --- Differencing of Proofs --- *) open Proofcatterms -open Term +open Constr open Coqterms open Environ open Searchopts -open Differencers open Substitution open Proofdiff open Debruijn open Filters open Candidates open Reducers -open Printing open Kindofchange module CRD = Context.Rel.Declaration @@ -77,13 +75,13 @@ let merge_diff_envs is_ind num_new_rels (d : goal_type_term_diff) = *) let build_app_candidates (env : env) (from_type : types) (old_term : types) (new_term : types) = try - let env_shift = push_rel CRD.(LocalAssum(Anonymous, from_type)) env in + let env_shift = push_rel CRD.(LocalAssum(Names.Name.Anonymous, from_type)) env in let old_term_shift = shift old_term in let new_term_shift = shift new_term in let sub = all_conv_substs_combs env_shift (new_term_shift, (mkRel 1)) in let bodies = sub old_term_shift in List.map - (fun b -> mkLambda (Anonymous, from_type, b)) + (fun b -> mkLambda (Names.Name.Anonymous, from_type, b)) (filter_not_same env_shift old_term_shift bodies) with _ -> give_up @@ -129,7 +127,7 @@ let find_difference (opts : options) (d : goal_proof_diff) : candidates = infer_type env_merge new_term in let candidates = build_app_candidates env_merge from_type old_term new_term in - let goal_type = mkProd (Anonymous, new_goal_type, shift old_goal_type) in + let goal_type = mkProd (Names.Name.Anonymous, new_goal_type, shift old_goal_type) in let reduced = reduce_all reduce_remove_identities env_merge candidates in let filter = filter_by_type env_merge goal_type in List.map @@ -148,8 +146,8 @@ let no_diff opts (d : goal_proof_diff) : bool = match get_change opts with | FixpointCase ((d_old, d_new), _) -> conv - || (eq_constr d_old old_term && eq_constr d_new new_term) - || (eq_constr d_old new_term && eq_constr d_new old_term) + || (equal d_old old_term && equal d_new new_term) + || (equal d_old new_term && equal d_new old_term) | _ -> conv diff --git a/plugin/src/core/components/factoring/factoring.ml b/plugin/src/core/components/factoring/factoring.ml index fa70391..e59039f 100644 --- a/plugin/src/core/components/factoring/factoring.ml +++ b/plugin/src/core/components/factoring/factoring.ml @@ -1,6 +1,6 @@ (* --- The Factoring Component --- *) -open Term +open Constr open Environ open Coqterms open Reducers @@ -8,7 +8,6 @@ open Specialization open Names open Collections open Debruijn -open Printing module CRD = Context.Rel.Declaration @@ -36,7 +35,7 @@ let is_assumption (env : env) (trm : types) : bool = (* * Assume a term of type typ in an environment *) -let assume (env : env) (n : name) (typ : types) : env = +let assume (env : env) (n : Name.t) (typ : types) : env = let env_pop = pop_rel_context 1 env in push_rel CRD.(LocalAssum(n, typ)) env_pop @@ -78,7 +77,7 @@ let rec find_path (env : env) (trm : types) : factors = if is_assumption env trm then [(env, trm)] else - match kind_of_term trm with + match kind trm with | App (f, args) -> let paths = Array.map (find_path env) args in let nonempty_paths = filter_non_empty (Array.to_list paths) in diff --git a/plugin/src/core/components/factoring/factoring.mli b/plugin/src/core/components/factoring/factoring.mli index 1ed7a68..497fedd 100644 --- a/plugin/src/core/components/factoring/factoring.mli +++ b/plugin/src/core/components/factoring/factoring.mli @@ -1,6 +1,6 @@ (* --- The Factoring Component --- *) -open Term +open Constr open Environ (* diff --git a/plugin/src/core/components/inversion/inverting.ml b/plugin/src/core/components/inversion/inverting.ml index 4a128e1..4aff6af 100644 --- a/plugin/src/core/components/inversion/inverting.ml +++ b/plugin/src/core/components/inversion/inverting.ml @@ -1,10 +1,9 @@ (* --- Inversion Component --- *) -open Term +open Constr open Environ open Coqterms open Collections -open Printing open Utilities open Debruijn open Reducers @@ -51,9 +50,9 @@ let invert_factors (invert : inverter) (fs : factors) : factors = *) let build_swap_map (env : env) (o : types) (n : types) : swap_map = let rec build_swaps i swap = - match map_tuple kind_of_term swap with + match map_tuple kind swap with | (App (f_s, args_s), App (f_n, args_n)) -> - let is_swap s = not (fold_tuple eq_constr s) in + let is_swap s = not (fold_tuple equal s) in let arg_swaps = filter_swaps is_swap (of_arguments args_s args_n) in let swaps = unshift_swaps_by i arg_swaps in merge_swaps (swaps :: (map_swaps (build_swaps i) swaps)) @@ -76,7 +75,7 @@ let build_swap_map (env : env) (o : types) (n : types) : swap_map = * Generalizing how to swap arguments is hard and will still probably involve * swaps above. *) -let rec exploit_type_symmetry (env : env) (trm : types) : types list = +let exploit_type_symmetry (env : env) (trm : types) : types list = map_subterms_env_if_lazy (fun _ _ t -> isApp t && is_rewrite (fst (destApp t))) (fun en _ t -> @@ -135,7 +134,7 @@ let rec exploit_type_symmetry (env : env) (trm : types) : types list = *) let invert_factor (env, rp) : (env * types) option = let rp = reduce_term env rp in - match kind_of_term rp with + match kind rp with | Lambda (n, old_goal_type, body) -> let env_body = push_rel CRD.(LocalAssum(n, old_goal_type)) env in let new_goal_type = unshift (reduce_term env_body (infer_type env_body body)) in diff --git a/plugin/src/core/components/inversion/inverting.mli b/plugin/src/core/components/inversion/inverting.mli index eadf1b6..76990bb 100644 --- a/plugin/src/core/components/inversion/inverting.mli +++ b/plugin/src/core/components/inversion/inverting.mli @@ -1,6 +1,6 @@ (* --- Inversion Component --- *) -open Term +open Constr open Environ type inverter diff --git a/plugin/src/core/components/specialization/specialization.ml b/plugin/src/core/components/specialization/specialization.ml index 597e4f7..e337e38 100644 --- a/plugin/src/core/components/specialization/specialization.ml +++ b/plugin/src/core/components/specialization/specialization.ml @@ -10,7 +10,7 @@ *) open Environ -open Term +open Constr open Coqterms open Reducers open Collections @@ -38,7 +38,7 @@ let specialize_using (s : specializer) env f args = * At the bottom level, it returns betaiota reduction. *) let rec specialize_body (s : specializer) (env : env) (t : types) : types = - match kind_of_term t with + match kind t with | Lambda (n, t, b) -> mkLambda (n, t, specialize_body s (push_rel CRD.(LocalAssum(n, t)) env) b) | App (f, args) -> diff --git a/plugin/src/core/components/specialization/specialization.mli b/plugin/src/core/components/specialization/specialization.mli index 489445d..ba1ce71 100644 --- a/plugin/src/core/components/specialization/specialization.mli +++ b/plugin/src/core/components/specialization/specialization.mli @@ -9,7 +9,7 @@ * for future extension to the tool. *) -open Term +open Constr open Environ open Reducers diff --git a/plugin/src/core/configuration/searchopts.ml b/plugin/src/core/configuration/searchopts.ml index b84f3f0..8ef4486 100644 --- a/plugin/src/core/configuration/searchopts.ml +++ b/plugin/src/core/configuration/searchopts.ml @@ -1,6 +1,6 @@ (* Search configuration *) -open Term +open Constr open Environ open Coqterms open Proofcat @@ -9,9 +9,7 @@ open Collections open Debruijn open Utilities open Proofdiff -open Reducers open Assumptions -open Printing open Kindofchange open Cutlemma open Zooming @@ -79,9 +77,9 @@ let configure_same_h change (d : lift_goal_diff) : types -> types -> bool = let k_n = destConst f_n in let ind_o = mkInd (Option.get (inductive_of_elim env_o k_o), 0) in let ind_n = mkInd (Option.get (inductive_of_elim env_n k_n), 0) in - (eq_constr f_o f_n) || (eq_constr ind_o o && eq_constr ind_n n)) + (equal f_o f_n) || (equal ind_o o && equal ind_n n)) | _ -> - eq_constr + equal (* * Given a set of goals, update the goal terms for a change in types. @@ -161,7 +159,7 @@ let configure_update_goals change d_old d = let default_goals = map_tuple fst (old_proof d_def, new_proof d_def) in let (g_o, g_n) = context_terms old_goals in let (g_o', g_n') = context_terms default_goals in - if eq_constr g_o g_o' && eq_constr g_n g_n' then (* set initial goals *) + if equal g_o g_o' && equal g_n g_n' then (* set initial goals *) set_hypothesis_goals t_old t_new d_def else (* update goals *) update_goals_types d_old d diff --git a/plugin/src/core/configuration/searchopts.mli b/plugin/src/core/configuration/searchopts.mli index 93020f6..1998e51 100644 --- a/plugin/src/core/configuration/searchopts.mli +++ b/plugin/src/core/configuration/searchopts.mli @@ -1,7 +1,6 @@ (* Search configuration *) -open Term -open Environ +open Constr open Proofdiff open Cutlemma open Kindofchange diff --git a/plugin/src/core/procedures/search.ml b/plugin/src/core/procedures/search.ml index 364d5aa..441ee41 100644 --- a/plugin/src/core/procedures/search.ml +++ b/plugin/src/core/procedures/search.ml @@ -1,14 +1,13 @@ (* Search procedures *) open Environ -open Term +open Constr open Assumptions open Abstraction open Abstractionconfig open Proofdiff open Reducers open Specialization -open Printing open Collections open Inverting open Searchopts diff --git a/plugin/src/core/procedures/search.mli b/plugin/src/core/procedures/search.mli index 735c959..a445477 100644 --- a/plugin/src/core/procedures/search.mli +++ b/plugin/src/core/procedures/search.mli @@ -1,6 +1,6 @@ (* Search procedures *) -open Term +open Constr open Proofdiff open Searchopts diff --git a/plugin/src/core/procedures/theorem.ml b/plugin/src/core/procedures/theorem.ml index e978b88..34379d8 100644 --- a/plugin/src/core/procedures/theorem.ml +++ b/plugin/src/core/procedures/theorem.ml @@ -1,9 +1,8 @@ (* Updating theorems instead of proofs *) -open Term +open Constr open Environ open Coqterms -open Printing open Substitution open Debruijn open Reducers @@ -17,7 +16,7 @@ module CRD = Context.Rel.Declaration * TODO common with reversal, factor that out *) let rec zoom_lambda_term (env : env) (trm : types) : env * types = - match kind_of_term trm with + match kind trm with | Lambda (n, t, b) -> zoom_lambda_term (push_rel CRD.(LocalAssum(n, t)) env) b | _ -> @@ -27,7 +26,7 @@ let rec zoom_lambda_term (env : env) (trm : types) : env * types = * Zoom all the way into a product type *) let rec zoom_product_type (env : env) (typ : types) : env * types = - match kind_of_term typ with + match kind typ with | Prod (n, t, b) -> zoom_product_type (push_rel CRD.(LocalAssum(n, t)) env) b | _ -> @@ -41,7 +40,7 @@ let rec zoom_product_type (env : env) (typ : types) : env * types = *) let rec args_to (env : env) (f : types) (trm : types) : env * (types array) = let nonempty (_, a) = Array.length a > 0 in - match kind_of_term trm with + match kind trm with | Lambda (n, t, b) -> args_to (push_rel CRD.(LocalAssum(n,t)) env) f b | App (g, args) -> diff --git a/plugin/src/core/procedures/theorem.mli b/plugin/src/core/procedures/theorem.mli index fb77b7a..156fd82 100644 --- a/plugin/src/core/procedures/theorem.mli +++ b/plugin/src/core/procedures/theorem.mli @@ -1,6 +1,6 @@ (* Updating theorems instead of proofs *) -open Term +open Constr open Environ (* diff --git a/plugin/src/library/coq/coqenvs.ml b/plugin/src/library/coq/coqenvs.ml index b7a8601..9912701 100644 --- a/plugin/src/library/coq/coqenvs.ml +++ b/plugin/src/library/coq/coqenvs.ml @@ -1,7 +1,7 @@ open Environ open Collections open Declarations -open Term +open Constr open Coqterms open Names @@ -53,7 +53,7 @@ let bindings_for_inductive (env : env) (mutind_body : mutual_inductive_body) (in * A fixpoint creates bindings that we need to push to the environment * This function gets all of those bindings *) -let bindings_for_fix (names : name array) (typs : types array) : CRD.t list = +let bindings_for_fix (names : Name.t array) (typs : types array) : CRD.t list = Array.to_list (CArray.map2_i (fun i name typ -> CRD.LocalAssum (name, Vars.lift i typ)) diff --git a/plugin/src/library/coq/coqenvs.mli b/plugin/src/library/coq/coqenvs.mli index 9f3560b..545cbbc 100644 --- a/plugin/src/library/coq/coqenvs.mli +++ b/plugin/src/library/coq/coqenvs.mli @@ -1,7 +1,7 @@ open Environ open Context open Declarations -open Term +open Constr open Names type 'a contextual = env -> 'a @@ -32,4 +32,4 @@ val bindings_for_inductive : env -> mutual_inductive_body -> one_inductive_body * A fixpoint also creates bindings that we need to push to the environment * This function gets all of those bindings *) -val bindings_for_fix : name array -> types array -> Rel.Declaration.t list +val bindings_for_fix : Name.t array -> types array -> Rel.Declaration.t list diff --git a/plugin/src/library/coq/coqterms.ml b/plugin/src/library/coq/coqterms.ml index 751f475..d38252d 100644 --- a/plugin/src/library/coq/coqterms.ml +++ b/plugin/src/library/coq/coqterms.ml @@ -3,12 +3,10 @@ open Environ open Evd open Constr -open Constrexpr -open Declarations open Decl_kinds open Names -open Univ open Collections +open Declarations module CRD = Context.Rel.Declaration @@ -147,7 +145,7 @@ let eq_sym : types = let is_prop (trm : types) : bool = match kind trm with | Sort s -> - s = Term.prop_sort + s = Sorts.prop | _ -> false @@ -214,7 +212,7 @@ let rec reconstruct_prod (env : env) (b : types) : types = (* --- Inductive types --- *) (* Get the body of a mutually inductive type *) -let lookup_mutind_body (i : mutual_inductive) (env : env) : mutual_inductive_body = +let lookup_mutind_body i (env : env) : mutual_inductive_body = lookup_mind i env (* Get the type of a mutually inductive type *) @@ -230,7 +228,7 @@ let check_inductive_supported (mutind_body : mutual_inductive_body) : unit = if not (Array.length ind_bodies = 1) then failwith "mutually inductive types not yet supported" else - if (mutind_body.mind_finite = Decl_kinds.CoFinite) then + if (mutind_body.mind_finite = CoFinite) then failwith "coinductive types not yet supported" else () @@ -243,7 +241,7 @@ let check_inductive_supported (mutind_body : mutual_inductive_body) : unit = * * TODO clean me after changes *) -let inductive_of_elim (env : env) (pc : pconstant) : mutual_inductive option = +let inductive_of_elim (env : env) (pc : pconstant) = let (c, u) = pc in let kn = Constant.canonical c in let (modpath, dirpath, label) = KerName.repr kn in @@ -258,7 +256,7 @@ let inductive_of_elim (env : env) (pc : pconstant) : mutual_inductive option = 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 - lookup_mutind_body ind_name env; + ignore (lookup_mutind_body ind_name env); Some ind_name else if not is_rev then @@ -299,7 +297,7 @@ let conv_ignoring_univ_inconsistency env evm (trm1 : types) (trm2 : types) : boo Reductionops.is_conv env evm etrm1 etrm2 with _ -> match map_tuple kind (trm1, trm2) with - | (Sort (Type u1), Sort (Type u2)) -> true + | (Sort (Sorts.Type u1), Sort (Sorts.Type u2)) -> true | _ -> false (* Checks whether two terms are convertible in env with the empty evar environment *) diff --git a/plugin/src/library/coq/coqterms.mli b/plugin/src/library/coq/coqterms.mli index 76153a9..5f2bb9f 100644 --- a/plugin/src/library/coq/coqterms.mli +++ b/plugin/src/library/coq/coqterms.mli @@ -2,7 +2,7 @@ open Environ open Evd -open Term +open Constr open Declarations open Names @@ -78,7 +78,7 @@ val reconstruct_prod : env -> types -> types (* --- Inductive types --- *) (* (To avoid confusing Coq naming) get the body of a mutually inductive type *) -val lookup_mutind_body : mutual_inductive -> env -> mutual_inductive_body +val lookup_mutind_body : MutInd.t -> env -> mutual_inductive_body (* Get the type of a mutually inductive type *) val type_of_inductive : env -> mutual_inductive_body -> one_inductive_body -> types @@ -94,7 +94,7 @@ val check_inductive_supported : mutual_inductive_body -> unit * If so, return Some with the inductive type * Otherwise, return None *) -val inductive_of_elim : env -> pconstant -> mutual_inductive option +val inductive_of_elim : env -> pconstant -> MutInd.t option (* * Get the number of constructors for an inductive type diff --git a/plugin/src/library/coq/debruijn.ml b/plugin/src/library/coq/debruijn.ml index 14d426b..defce0e 100644 --- a/plugin/src/library/coq/debruijn.ml +++ b/plugin/src/library/coq/debruijn.ml @@ -1,11 +1,10 @@ (* --- DeBruijn management --- *) open Environ -open Term +open Constr open Hofs open Collections open Coqenvs -open Printing (* TODO move shiftability into a module/functor *) @@ -36,7 +35,7 @@ let shift_i (i : int) : int = let unshift_local (max : int) (n : int) (trm : types) : types = map_term (fun (m, adj) t -> - match kind_of_term t with + match kind t with | Rel i -> let i' = if i > m then unshift_i_by adj i else i in mkRel i' @@ -73,7 +72,7 @@ let unshift (t : types) : types = let shift_by_unconditional (n : int) (trm : types) : types = map_term (fun _ t -> - match kind_of_term t with + match kind t with | Rel i -> let i' = shift_i_by n i in mkRel i' diff --git a/plugin/src/library/coq/debruijn.mli b/plugin/src/library/coq/debruijn.mli index 52a368e..9b339d9 100644 --- a/plugin/src/library/coq/debruijn.mli +++ b/plugin/src/library/coq/debruijn.mli @@ -1,7 +1,7 @@ (* DeBruijn management *) open Environ -open Term +open Constr (* --- Indexes --- *) diff --git a/plugin/src/library/coq/filters.ml b/plugin/src/library/coq/filters.ml index 5fccc8b..5ccb530 100644 --- a/plugin/src/library/coq/filters.ml +++ b/plugin/src/library/coq/filters.ml @@ -1,6 +1,6 @@ (* Filters *) -open Term +open Constr open Environ open Coqterms open Debruijn @@ -23,7 +23,7 @@ let find_by_type (env : env) (typ : types) (trms : types list) : types list = (* Filter a list of terms to those not exactly the same as the supplied term *) let filter_not_same (_ : env) (trm : types) (trms : types list) : types list = - let same = eq_constr trm in (* exact equality for constructors *) + let same = equal trm in (* exact equality for constructors *) List.filter (fun t -> not (same t)) trms (* @@ -44,7 +44,7 @@ let filter_ihs (env : env) (cs : types list) : types list = (fun c -> let c_no_ih = unshift c in try - let c_type = infer_type env_no_ih c_no_ih in + ignore (infer_type env_no_ih c_no_ih); true with _ -> false) cs diff --git a/plugin/src/library/coq/filters.mli b/plugin/src/library/coq/filters.mli index 84919cf..9b0334b 100644 --- a/plugin/src/library/coq/filters.mli +++ b/plugin/src/library/coq/filters.mli @@ -1,8 +1,7 @@ (* Filters for terms and eterms *) -open Term +open Constr open Environ -open Coqterms type 'a filter_strategy = env -> types -> 'a list -> 'a list diff --git a/plugin/src/library/coq/hofs.ml b/plugin/src/library/coq/hofs.ml index 56d45e7..57e02f7 100644 --- a/plugin/src/library/coq/hofs.ml +++ b/plugin/src/library/coq/hofs.ml @@ -4,13 +4,11 @@ (* TODO can still generalize these to make them easier to extend further *) open Environ -open Term +open Constr open Coqterms open Coqenvs open Collections open Names -open Utilities -open Printing module CRD = Context.Rel.Declaration @@ -68,7 +66,6 @@ type ('a, 'b) conditional_cartesian_mapper_with_env = (* Specific predicates and functions for implementation *) type 'a p_no_env = ('a, types) pred -type 'a pe_no_env = ('a, eterm) pred type 'a p_with_env = ('a, types) pred_with_env type 'a pe_with_env = ('a, eterm) pred_with_env type 'a f_no_env = ('a, types) transformer @@ -83,7 +80,7 @@ type 'a f_cart_no_env = ('a, types) cartesian_transformer (* * Recurse on a mapping function with an environment for a fixpoint *) -let map_rec_env_fix (map_rec : ('a, 'b) transformer_with_env) (d : 'a updater) (env : env) (a : 'a) (ns : name array) (ts : types array) = +let map_rec_env_fix (map_rec : ('a, 'b) transformer_with_env) (d : 'a updater) (env : env) (a : 'a) (ns : Name.t array) (ts : types array) = 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 @@ -93,7 +90,7 @@ let map_rec_env_fix (map_rec : ('a, 'b) transformer_with_env) (d : 'a updater) ( (* * Recurse on a mapping function with an environment for a fixpoint *) -let map_rec_env_fix_cartesian (map_rec : ('a, 'b) cartesian_transformer_with_env) (d : 'a updater) (env : env) (a : 'a) (ns : name array) (ts : types array) = +let map_rec_env_fix_cartesian (map_rec : ('a, 'b) cartesian_transformer_with_env) (d : 'a updater) (env : env) (a : 'a) (ns : Name.t array) (ts : types array) = 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 @@ -108,7 +105,7 @@ let map_rec_env_fix_cartesian (map_rec : ('a, 'b) cartesian_transformer_with_env *) let rec map_term_env (f : 'a f_with_env) (d : 'a updater) (env : env) (a : 'a) (trm : types) : types = let map_rec = map_term_env f d in - match kind_of_term trm with + match kind trm with | Cast (c, k, t) -> let c' = map_rec env a c in let t' = map_rec env a t in @@ -165,7 +162,7 @@ let map_term (f : 'a f_no_env) (d : 'a updater) (a : 'a) (trm : types) : types = *) let rec map_subterms_env (f : 'a f_cart_with_env) (d : 'a updater) (env : env) (a : 'a) (trm : types) : types list = let map_rec = map_subterms_env f d in - match kind_of_term trm with + match kind trm with | Cast (c, k, t) -> let cs' = map_rec env a c in let ts' = map_rec env a t in @@ -227,7 +224,7 @@ let rec map_term_env_if (p : 'a p_with_env) (f : 'a f_with_env) (d : 'a updater) if p env a trm then f env a trm else - match kind_of_term trm with + match kind trm with | Cast (c, k, t) -> let c' = map_rec env a c in let t' = map_rec env a t in @@ -282,7 +279,7 @@ let rec map_term_env_if_shallow (p : 'a p_with_env) (f : 'a f_with_env) (d : 'a if p env a trm then f env a trm else - match kind_of_term trm with + match kind trm with | Cast (c, k, t) -> let c' = map_rec env a c in let t' = map_rec env a t in @@ -350,7 +347,7 @@ let rec map_subterms_env_if (p : 'a p_with_env) (f : 'a f_cart_with_env) (d : 'a if p env a trm then f env a trm else - match kind_of_term trm with + match kind trm with | Cast (c, k, t) -> let cs' = map_rec env a c in let ts' = map_rec env a t in @@ -404,7 +401,7 @@ let rec map_subterms_env_if_combs (p : 'a p_with_env) (f : 'a f_cart_with_env) ( let trms = if p env a trm then f env a trm else [trm] in flat_map (fun trm' -> - match kind_of_term trm' with + match kind trm' with | Cast (c, k, t) -> let cs' = map_rec env a c in let ts' = map_rec env a t in @@ -459,7 +456,7 @@ let rec map_subterms_env_if_combs (p : 'a p_with_env) (f : 'a f_cart_with_env) ( let rec map_subterms_env_if_lazy (p : 'a p_with_env) (f : 'a f_cart_with_env) (d : 'a updater) (env : env) (a : 'a) (trm : types) : types list = let map_rec = map_subterms_env_if_lazy p f d in let trms' = - match kind_of_term trm with + match kind trm with | Cast (c, k, t) -> let cs' = map_rec env a c in let ts' = map_rec env a t in @@ -522,7 +519,7 @@ let map_eterms (f : eterm -> eterm) ((evm, ts) : eterms) : eterms = *) let rec map_eterm_env (f : 'a fe_with_env) (d : 'a updater) (env : env) (a : 'a) ((evm, trm) : eterm) : eterm = let map_rec = map_eterm_env f d in - match kind_of_term trm with + match kind trm with | Cast (c, k, t) -> let (evm', c') = map_rec env a (evm, c) in let (evm'', t') = map_rec env a (evm', t) in @@ -582,7 +579,7 @@ let map_eterm (f : 'a fe_no_env) (d : 'a updater) (a : 'a) (etrm : eterm) : eter let rec map_eterm_env_if_lazy (p : 'a pe_with_env) (f : 'a fe_with_env) (d : 'a updater) (env : env) (a : 'a) ((evm, trm) : eterm) : eterm = let map_rec = map_eterm_env_if_lazy p f d in let (evm', trm') = - match kind_of_term trm with + match kind trm with | Cast (c, k, t) -> let (evm', c') = map_rec env a (evm, c) in let (evm'', t') = map_rec env a (evm', t) in diff --git a/plugin/src/library/coq/hofs.mli b/plugin/src/library/coq/hofs.mli index 1cbde09..5fbaca0 100644 --- a/plugin/src/library/coq/hofs.mli +++ b/plugin/src/library/coq/hofs.mli @@ -1,7 +1,7 @@ (* Higher-order functions on terms *) open Environ -open Term +open Constr open Coqterms (* Predicates to determine whether to apply a mapped function *) diff --git a/plugin/src/library/coq/printing.ml b/plugin/src/library/coq/printing.ml index be264d5..acfa97a 100644 --- a/plugin/src/library/coq/printing.ml +++ b/plugin/src/library/coq/printing.ml @@ -9,13 +9,14 @@ open Format open Names open Univ -open Term +open Constr open Environ open Coqenvs open Printer open Utilities open Goptions open Collections +open Declarations module CRD = Context.Rel.Declaration @@ -31,15 +32,11 @@ let print_to_string (pp : formatter -> 'a -> unit) (trm : 'a) : string = (* --- Coq terms --- *) (* Gets n as a string *) -let name_as_string (n : name) : string = +let name_as_string (n : Name.t) : string = match n with - | Name id -> string_of_id id + | Name id -> Id.to_string id | Anonymous -> "_" -(* Pretty prints a term using Coq's pretty printer *) -let print_constr (fmt : formatter) (c : constr) : unit = - Pp.pp_with fmt (Printer.pr_constr c) - (* Pretty prints a universe level *) let print_univ_level (fmt : formatter) (l : Level.t) = Pp.pp_with fmt (Level.pr l) @@ -53,12 +50,12 @@ let universe_as_string u = (* Gets a sort as a string *) let sort_as_string s = match s with - | Prop _ -> if s = prop_sort then "Prop" else "Set" - | Type u -> Printf.sprintf "Type %s" (universe_as_string u) + | Term.Prop _ -> if s = Sorts.prop then "Prop" else "Set" + | Term.Type u -> Printf.sprintf "Type %s" (universe_as_string u) (* Prints a term *) let rec term_as_string (env : env) (trm : types) = - match kind_of_term trm with + match kind trm with | Rel i -> (try let (n, _, _) = CRD.to_tuple @@ lookup_rel i env in @@ -66,7 +63,7 @@ let rec term_as_string (env : env) (trm : types) = with Not_found -> Printf.sprintf "(Unbound_Rel %d)" i) | Var v -> - string_of_id v + Id.to_string v | Meta mv -> failwith "Metavariables are not yet supported" | Evar (k, cs) -> @@ -85,17 +82,17 @@ let rec term_as_string (env : env) (trm : types) = Printf.sprintf "(%s %s)" (term_as_string env f) (String.concat " " (List.map (term_as_string env) (Array.to_list xs))) | Const (c, u) -> let ker_name = Constant.canonical c in - string_of_kn ker_name + KerName.to_string ker_name | Construct (((i, i_index), c_index), u) -> let mutind_body = lookup_mind i env in let ind_body = mutind_body.mind_packets.(i_index) in let constr_name_id = ind_body.mind_consnames.(c_index - 1) in - string_of_id constr_name_id + Id.to_string constr_name_id | Ind ((i, i_index), u) -> let mutind_body = lookup_mind i env in let ind_bodies = mutind_body.mind_packets in let name_id = (ind_bodies.(i_index)).mind_typename in - string_of_id name_id + Id.to_string name_id | Case (ci, ct, m, bs) -> let (i, i_index) = ci.ci_ind in let mutind_body = lookup_mind i env in @@ -111,7 +108,7 @@ let rec term_as_string (env : env) (trm : types) = (fun c_i b -> Printf.sprintf "(case %s => %s)" - (string_of_id (ind_body.mind_consnames.(c_i))) + (Id.to_string (ind_body.mind_consnames.(c_i))) (term_as_string env b)) bs))) | Fix ((is, i), (ns, ts, ds)) -> diff --git a/plugin/src/library/coq/printing.mli b/plugin/src/library/coq/printing.mli index 86cbfe2..c63e375 100644 --- a/plugin/src/library/coq/printing.mli +++ b/plugin/src/library/coq/printing.mli @@ -2,7 +2,7 @@ open Format open Names -open Term +open Constr open Environ open Evd @@ -14,7 +14,7 @@ val print_to_string : (formatter -> 'a -> unit) -> 'a -> string (* --- Coq terms --- *) (* Gets a name as a string *) -val name_as_string : name -> string +val name_as_string : Name.t -> string (* Gets a term as a string in an environment *) val term_as_string : env -> types -> string diff --git a/plugin/src/library/coq/reducers.ml b/plugin/src/library/coq/reducers.ml index b539dbe..29a6533 100644 --- a/plugin/src/library/coq/reducers.ml +++ b/plugin/src/library/coq/reducers.ml @@ -1,7 +1,7 @@ (* Strategies for reducing terms *) open Environ -open Term +open Constr open Hofs open Coqterms open Utilities @@ -34,7 +34,7 @@ let rec reduce_body_if p (r : reducer) env trm = if p env trm then r env trm else - match kind_of_term trm with + match kind trm with | Lambda (n, t, b) -> reduce_body_if p r (push_rel CRD.(LocalAssum(n, t)) env) b | _ -> @@ -59,7 +59,7 @@ let remove_identities (env : env) (trm : types) : types = map_term_if (fun _ t -> applies_identity t) (fun _ t -> - match kind_of_term t with + match kind t with | App (_, args) -> Array.get args 1 | _ -> @@ -99,7 +99,7 @@ let reduce_whd_if_let_in (env : env) (trm : types) : types = * has only hypotheses that are referenced. *) let rec remove_unused_hypos (env : env) (trm : types) : types = - match kind_of_term trm with + match kind trm with | Lambda (n, t, b) -> let env_b = push_rel CRD.(LocalAssum(n, t)) env in let b' = remove_unused_hypos env_b b in diff --git a/plugin/src/library/coq/reducers.mli b/plugin/src/library/coq/reducers.mli index fedc673..0498db0 100644 --- a/plugin/src/library/coq/reducers.mli +++ b/plugin/src/library/coq/reducers.mli @@ -1,7 +1,7 @@ (* Strategies for reducing terms *) open Environ -open Term +open Constr type reducer = env -> types -> types diff --git a/plugin/src/library/coq/substitution.ml b/plugin/src/library/coq/substitution.ml index 436ec00..697efd0 100644 --- a/plugin/src/library/coq/substitution.ml +++ b/plugin/src/library/coq/substitution.ml @@ -1,13 +1,10 @@ (* Substitution auxiliary functions *) open Environ -open Term +open Constr open Coqterms open Hofs open Debruijn -open Coqenvs -open Collections -open Printing (* TODO clean up so retrieval is easier *) type ('a, 'b) substitution = env -> 'a -> types -> 'b diff --git a/plugin/src/library/coq/substitution.mli b/plugin/src/library/coq/substitution.mli index e8e463c..e5cb113 100644 --- a/plugin/src/library/coq/substitution.mli +++ b/plugin/src/library/coq/substitution.mli @@ -1,11 +1,7 @@ (* Substitution auxiliary functions *) open Environ -open Term -open Coqterms -open Assumptions -open Coqenvs -open Debruijn +open Constr (* TODO clean up so retrieval is easier *) type ('a, 'b) substitution = env -> 'a -> types -> 'b diff --git a/plugin/src/library/proofsearch/compilation/evaluation.ml b/plugin/src/library/proofsearch/compilation/evaluation.ml index aa58008..16cce02 100644 --- a/plugin/src/library/proofsearch/compilation/evaluation.ml +++ b/plugin/src/library/proofsearch/compilation/evaluation.ml @@ -1,6 +1,6 @@ (* --- Evaluation, which is lazy (takes one step) --- *) -open Term +open Constr open Environ open Proofcat open Proofcatterms @@ -9,9 +9,7 @@ open Utilities open Names open Debruijn open Collections -open Substitution open Declarations -open Printing module CRD = Context.Rel.Declaration @@ -53,7 +51,7 @@ let rec induction_constrs (nc : int) (env : env) ((n, t, b) : Name.t * types * t else let e = LazyBinding (mkRel 1, push_rel CRD.(LocalAssum(n, t)) env) in let c = eval_theorem_bind e env t in - match kind_of_term b with + match kind b with | Prod (n', t', b') -> let d = List.length (morphisms c) in let prod' = (n', unshift_by d t', unshift_by d b') in @@ -134,7 +132,6 @@ let eval_induction (mutind_body : mutual_inductive_body) (fc : proof_cat) (args let c = combine_constrs fc cs_bound in let property = arg_partition.property in let params = arg_partition.params in - let env = context_env t in let c_bound = bind_property_and_params property params npms c in (c_bound, npms, arg_partition.final_args) else diff --git a/plugin/src/library/proofsearch/compilation/evaluation.mli b/plugin/src/library/proofsearch/compilation/evaluation.mli index f733ec3..c42a41c 100644 --- a/plugin/src/library/proofsearch/compilation/evaluation.mli +++ b/plugin/src/library/proofsearch/compilation/evaluation.mli @@ -1,6 +1,6 @@ (* --- Evaluation, which is lazy (takes one step) --- *) -open Term +open Constr open Environ open Proofcat open Declarations diff --git a/plugin/src/library/proofsearch/compilation/expansion.ml b/plugin/src/library/proofsearch/compilation/expansion.ml index 4605993..34e3d88 100644 --- a/plugin/src/library/proofsearch/compilation/expansion.ml +++ b/plugin/src/library/proofsearch/compilation/expansion.ml @@ -2,7 +2,7 @@ open Names open Environ -open Term +open Constr open Coqterms open Coqenvs open Proofcat @@ -11,7 +11,7 @@ open Evaluation open Collections open Utilities open Debruijn -open Printing +open Declarations module CRD = Context.Rel.Declaration @@ -77,7 +77,7 @@ let expand_app (env : env) ((f, args) : types * types array) = *) let expand_term (default : env -> types -> proof_cat) (o : context_object) : proof_cat = let (trm, env) = dest_context_term o in - match kind_of_term trm with + match kind trm with | Prod (n, t, b) -> expand_product env (n, t, b) | Lambda (n, t, b) -> @@ -85,7 +85,7 @@ let expand_term (default : env -> types -> proof_cat) (o : context_object) : pro | Ind ((i, ii), u) -> expand_inductive env ((i, ii), u) | App (f, args) -> - (match kind_of_term f with + (match kind f with | Lambda (n, t, b) -> (* Does not yet delta-reduce *) if Array.length args > 0 then @@ -100,7 +100,7 @@ let expand_term (default : env -> types -> proof_cat) (o : context_object) : pro (* Expand a product type as far as its conclusion goes *) let expand_product_fully (o : context_object) : proof_cat = let rec expand_fully env (n, t, b) = - match kind_of_term b with + match kind b with | Prod (n', t', b') -> let t'' = eval_theorem env t in let env' = push_rel CRD.(LocalAssum(n, t)) env in @@ -260,7 +260,7 @@ let expand_application (c, n, l) : proof_cat * int * (types list) = match e with | LazyBinding (trm, env) -> let (f, args) = destApp trm in - (match kind_of_term f with + (match kind f with | Const (c, u) -> expand_const_app env (c, u) (f, args) l | _ -> diff --git a/plugin/src/library/proofsearch/compilation/expansion.mli b/plugin/src/library/proofsearch/compilation/expansion.mli index bd699c2..b1eb3fe 100644 --- a/plugin/src/library/proofsearch/compilation/expansion.mli +++ b/plugin/src/library/proofsearch/compilation/expansion.mli @@ -1,19 +1,13 @@ (* Expanding proof categories *) -open Names open Environ -open Term +open Constr open Proofcat (* --- Type definitions --- *) type 'a expansion_strategy = 'a -> 'a -(* --- Terms and types ---*) - -(* TODO hide me when refactoring is done *) -val expand_product : env -> (Name.t * types * types) -> proof_cat - (* --- Contexts --- *) (* diff --git a/plugin/src/library/proofsearch/compilation/proofdiff.ml b/plugin/src/library/proofsearch/compilation/proofdiff.ml index cc9e8ba..82e0e62 100644 --- a/plugin/src/library/proofsearch/compilation/proofdiff.ml +++ b/plugin/src/library/proofsearch/compilation/proofdiff.ml @@ -1,19 +1,16 @@ (* Difference between old and new proofs *) -open Term +open Constr open Environ open Proofcat open Assumptions open Expansion open Coqterms open Evaluation -open Utilities open Proofcatterms -open Substitution open Reducers open Declarations open Collections -open Printing open Merging (* --- Types --- *) @@ -318,20 +315,20 @@ let changed_constrs env ind_o ind_n = let cs_o = constructor_types env ind_o in let cs_n = constructor_types env ind_n in let cs = List.map2 (fun o n -> (o, n)) cs_o cs_n in - List.filter (fun (o, n) -> not (eq_constr o n)) cs + List.filter (fun (o, n) -> not (equal o n)) cs (* * Check if two types are inductive types with the same shape * * Fail if there are any assumptions in d * For now, only allow one constructor to change - * The rest must be eq_constr + * The rest must be equal *) let same_shape (env : env) (d : types proof_diff) : bool = assert (num_assumptions (assumptions d) = 0); let o = old_proof d in let n = new_proof d in - match map_tuple kind_of_term (o, n) with + match map_tuple kind (o, n) with | (Ind ((i_o, ii_o), u_o), Ind ((i_n, ii_n), u_n)) -> let ind_o = lookup_mutind_body i_o env in let ind_n = lookup_mutind_body i_n env in @@ -356,12 +353,12 @@ let ind_type_diff (env : env) (d : types proof_diff) : types proof_diff = assert (same_shape env d); let o = old_proof d in let n = new_proof d in - let (Ind ((i_o, _), _), Ind ((i_n, _), _)) = map_tuple kind_of_term (o, n) in + let (Ind ((i_o, _), _), Ind ((i_n, _), _)) = map_tuple kind (o, n) in let ind_o = lookup_mutind_body i_o env in let ind_n = lookup_mutind_body i_n env in let neqs = changed_constrs env ind_o ind_n in let rec remove_conclusion c = - match kind_of_term c with + match kind c with | Prod (n, t, b) -> if isProd b then mkProd (n, t, remove_conclusion b) @@ -391,14 +388,13 @@ let induct_over_same_h eq (d : goal_proof_diff) : bool = if (isApp trm1) && (isApp trm2) then let (f1, _) = destApp trm1 in let (f2, _) = destApp trm2 in - match (kind_of_term f1, kind_of_term f2) with + match (kind f1, kind f2) with | (Const k1, Const k2) -> let ind1_opt = inductive_of_elim (context_env (terminal o)) k1 in let ind2_opt = inductive_of_elim (context_env (terminal n)) k2 in if Option.has_some ind1_opt && Option.has_some ind2_opt then - let ind1 = Option.get ind1_opt in - let ind2 = Option.get ind2_opt in - eq f1 f2 + (* should be checking that the types are the same, too *) + eq f1 f2 else false | _ -> diff --git a/plugin/src/library/proofsearch/compilation/proofdiff.mli b/plugin/src/library/proofsearch/compilation/proofdiff.mli index 9912457..5900e27 100644 --- a/plugin/src/library/proofsearch/compilation/proofdiff.mli +++ b/plugin/src/library/proofsearch/compilation/proofdiff.mli @@ -1,11 +1,9 @@ (* Differences between old and new proofs *) -open Term +open Constr open Environ open Proofcat open Assumptions -open Expansion -open Substitution open Reducers open Merging diff --git a/plugin/src/library/proofsearch/compilation/zooming.ml b/plugin/src/library/proofsearch/compilation/zooming.ml index 1efb7d0..f68db13 100644 --- a/plugin/src/library/proofsearch/compilation/zooming.ml +++ b/plugin/src/library/proofsearch/compilation/zooming.ml @@ -3,15 +3,9 @@ open Proofdiff open Proofcatterms open Expansion open Assumptions -open Coqterms -open Evaluation -open Term -open Utilities open Candidates -open Term +open Constr open Debruijn -open Expansion -open Printing (* --- Zooming --- *) @@ -29,7 +23,6 @@ type 'a zoomer = (* Remove the initial object of c *) let remove_initial (c : proof_cat) : proof_cat = let i = initial c in - let os = objects c in let ms = morphisms c in let os' = all_objects_except i (objects c) in let (ms', ims) = List.partition (map_source (objects_not_equal i)) ms in diff --git a/plugin/src/library/proofsearch/compilation/zooming.mli b/plugin/src/library/proofsearch/compilation/zooming.mli index da06477..dfc720a 100644 --- a/plugin/src/library/proofsearch/compilation/zooming.mli +++ b/plugin/src/library/proofsearch/compilation/zooming.mli @@ -3,7 +3,7 @@ open Expansion open Proofcat open Candidates open Names -open Term +open Constr (* --- Zooming --- *) @@ -113,13 +113,13 @@ val zoom_search : search_function -> goal_proof_diff -> candidates * Zoom in, search, and wrap the result in a lambda *) val zoom_wrap_lambda : - search_function -> name -> types -> goal_proof_diff -> candidates + search_function -> Name.t -> types -> goal_proof_diff -> candidates (* * Zoom in, search, and wrap the result in a product *) val zoom_wrap_prod : - search_function -> name -> types -> goal_proof_diff -> candidates + search_function -> Name.t -> types -> goal_proof_diff -> candidates (* * Zoom in, search, and unshift the result diff --git a/plugin/src/library/proofsearch/representation/assumptions.ml b/plugin/src/library/proofsearch/representation/assumptions.ml index 9070d58..dc92153 100644 --- a/plugin/src/library/proofsearch/representation/assumptions.ml +++ b/plugin/src/library/proofsearch/representation/assumptions.ml @@ -1,13 +1,13 @@ (* Equality assumptions for substitutions in proof search *) -open Term +open Constr open Environ open Collections open Coqenvs open Debruijn -open Printing open Coqterms open Hofs +open Printing module CRD = Context.Rel.Declaration @@ -36,7 +36,7 @@ let substitutions_as_string (env : env) (subs : param_substitutions) : string = (* Is there an assumption or substitution about the term? *) let has_assumption_or_substitution (l : (int * 'a) list) (trm : types) : bool = - match kind_of_term trm with + match kind trm with | Rel i -> List.mem_assoc i l | _ -> false @@ -226,7 +226,7 @@ let substitute_env_params (subs : param_substitutions) (env : env) : env = * Given a swap map, make a unique swap map (no repeats and only one direction) *) let unique_swaps (swaps : swap_map) : swap_map = - let same = eq_constr in + let same = equal in let are_unique (s1, d1) (s2, d2) = (same s1 s2 && same d1 d2) || (same s1 d2 && same d1 s2) in unique are_unique swaps @@ -289,7 +289,7 @@ let shift_swaps = shift_swaps_by 1 * Get a swap map for all combinations of a function application *) let build_swap_map (en : env) (t : types) : swap_map = - match kind_of_term t with + match kind t with | App (_, args) -> filter_swaps (fun (a1, a2) -> @@ -336,7 +336,7 @@ let apply_swaps_combine c a env args swaps : 'a list = *) let all_typ_swaps_combs (env : env) (trm : types) : types list = unique - eq_constr + equal (map_subterms_env_if_lazy (fun en _ t -> isApp t) @@ -358,14 +358,14 @@ let all_typ_swaps_combs (env : env) (trm : types) : types list = *) let all_conv_swaps_combs (env : env) (swaps : swap_map) (trm : types) = unique - eq_constr + equal (map_subterms_env_if_lazy (fun _ _ t -> isApp t) (fun en depth t -> let swaps = shift_swaps_by depth swaps in let (f, args) = destApp t in unique - eq_constr + equal (apply_swaps_combine (fun s -> mkApp (f, s)) t env args swaps)) (fun depth -> depth + 1) env diff --git a/plugin/src/library/proofsearch/representation/assumptions.mli b/plugin/src/library/proofsearch/representation/assumptions.mli index 7cb3959..98d25af 100644 --- a/plugin/src/library/proofsearch/representation/assumptions.mli +++ b/plugin/src/library/proofsearch/representation/assumptions.mli @@ -1,8 +1,7 @@ (* Equality assumptions for substitutions in proof search *) -open Term +open Constr open Environ -open Coqterms type equal_assumptions type param_substitutions diff --git a/plugin/src/library/proofsearch/representation/candidates.ml b/plugin/src/library/proofsearch/representation/candidates.ml index 430ae4f..ea12afd 100644 --- a/plugin/src/library/proofsearch/representation/candidates.ml +++ b/plugin/src/library/proofsearch/representation/candidates.ml @@ -1,6 +1,6 @@ (* Basic types for proof search *) -open Term +open Constr type candidates = types list diff --git a/plugin/src/library/proofsearch/representation/candidates.mli b/plugin/src/library/proofsearch/representation/candidates.mli index a0f5101..19d818f 100644 --- a/plugin/src/library/proofsearch/representation/candidates.mli +++ b/plugin/src/library/proofsearch/representation/candidates.mli @@ -1,6 +1,6 @@ (* Basic types for proof search *) -open Term +open Constr type candidates = types list diff --git a/plugin/src/library/proofsearch/representation/cutlemma.ml b/plugin/src/library/proofsearch/representation/cutlemma.ml index d60d8dc..f934458 100644 --- a/plugin/src/library/proofsearch/representation/cutlemma.ml +++ b/plugin/src/library/proofsearch/representation/cutlemma.ml @@ -1,6 +1,6 @@ (* --- Cutting by intermediate lemmas/guiding search --- *) -open Term +open Constr open Environ open Reducers open Coqterms @@ -43,7 +43,7 @@ let has_cut_type_strict env cut trm = (* Flip the conclusions of a cut lemma *) let rec flip_concls lemma = - match kind_of_term lemma with + match kind lemma with | Prod (n, t, b) when isProd b -> mkProd (n, t, flip_concls b) | Prod (n, t, b) -> @@ -97,7 +97,7 @@ let has_cut_type env cut trm = let has_cut_type_app env cut trm = try let typ = shift (reduce_term env (infer_type env trm)) in - let env_cut = push_rel CRD.(LocalAssum(Anonymous, get_lemma cut)) env in + let env_cut = push_rel CRD.(LocalAssum(Names.Name.Anonymous, get_lemma cut)) env in let app = get_app cut in let app_app = reduce_term env_cut (mkApp (app, singleton_array (mkRel 1))) in let app_app_typ = infer_type env_cut app_app in diff --git a/plugin/src/library/proofsearch/representation/cutlemma.mli b/plugin/src/library/proofsearch/representation/cutlemma.mli index 9610309..5231c39 100644 --- a/plugin/src/library/proofsearch/representation/cutlemma.mli +++ b/plugin/src/library/proofsearch/representation/cutlemma.mli @@ -1,6 +1,6 @@ (* --- Cutting by intermediate lemmas/guiding search --- *) -open Term +open Constr open Environ (* diff --git a/plugin/src/library/proofsearch/representation/kindofchange.ml b/plugin/src/library/proofsearch/representation/kindofchange.ml index 818a730..85ce05f 100644 --- a/plugin/src/library/proofsearch/representation/kindofchange.ml +++ b/plugin/src/library/proofsearch/representation/kindofchange.ml @@ -1,6 +1,6 @@ (* --- Kinds of changes --- *) -open Term +open Constr open Cutlemma (* diff --git a/plugin/src/library/proofsearch/representation/kindofchange.mli b/plugin/src/library/proofsearch/representation/kindofchange.mli index 24dfbb1..a4ba525 100644 --- a/plugin/src/library/proofsearch/representation/kindofchange.mli +++ b/plugin/src/library/proofsearch/representation/kindofchange.mli @@ -1,6 +1,6 @@ (* --- Kinds of changes --- *) -open Term +open Constr open Cutlemma (* diff --git a/plugin/src/library/proofsearch/representation/merging.ml b/plugin/src/library/proofsearch/representation/merging.ml index 728778e..18cbfc3 100644 --- a/plugin/src/library/proofsearch/representation/merging.ml +++ b/plugin/src/library/proofsearch/representation/merging.ml @@ -1,13 +1,12 @@ (* --- Merging environments --- *) -open Term +open Constr open Environ open Debruijn open Assumptions open Collections open Coqterms open Coqenvs -open Printing module CRD = Context.Rel.Declaration diff --git a/plugin/src/library/proofsearch/representation/merging.mli b/plugin/src/library/proofsearch/representation/merging.mli index 4c9f98a..9058739 100644 --- a/plugin/src/library/proofsearch/representation/merging.mli +++ b/plugin/src/library/proofsearch/representation/merging.mli @@ -1,6 +1,6 @@ (* --- Merging environments --- *) -open Term +open Constr open Environ open Assumptions open Coqterms diff --git a/plugin/src/library/proofsearch/representation/proofcat.ml b/plugin/src/library/proofsearch/representation/proofcat.ml index 496c852..8c35cf5 100644 --- a/plugin/src/library/proofsearch/representation/proofcat.ml +++ b/plugin/src/library/proofsearch/representation/proofcat.ml @@ -1,11 +1,10 @@ (* Proof categories, core logic *) open Category -open Term +open Constr open Environ open Printing open Coqterms -open Substitution open Assumptions open Utilities open Collections @@ -530,7 +529,6 @@ let shortest_path_length (c : proof_cat) (o : context_object) : int = (* --- Functors --- *) module ProofFunctor = Functor (ProofCat) (ProofCat) -type proof_functor = ProofFunctor.t (* * Apply a functor over proof categories diff --git a/plugin/src/library/proofsearch/representation/proofcat.mli b/plugin/src/library/proofsearch/representation/proofcat.mli index 40b9cc6..c4052bf 100644 --- a/plugin/src/library/proofsearch/representation/proofcat.mli +++ b/plugin/src/library/proofsearch/representation/proofcat.mli @@ -1,6 +1,5 @@ -open Term +open Constr open Environ -open Category open Assumptions (* Proof categories, core logic *) diff --git a/plugin/src/library/proofsearch/representation/proofcatterms.ml b/plugin/src/library/proofsearch/representation/proofcatterms.ml index 2e20ccd..4f8c477 100644 --- a/plugin/src/library/proofsearch/representation/proofcatterms.ml +++ b/plugin/src/library/proofsearch/representation/proofcatterms.ml @@ -1,23 +1,20 @@ (* Logic for proof categories that is specific to terms and types *) -open Term +open Constr open Environ open Proofcat open Names open Debruijn open Assumptions -open Substitution open Utilities open Collections -open Coqterms -open Printing module CRD = Context.Rel.Declaration (* --- Construction --- *) (* Get the extension for a trm in env *) -let rec ext_of_term (env : env) (trm : types) : extension = +let ext_of_term (env : env) (trm : types) : extension = LazyBinding (trm, env) (* Get a fresh inductive hypothesis *) @@ -610,21 +607,6 @@ let sub_obj_property_params pi pb subs ds o = let subs_shift = shift_substitutions_by d subs in substitute_ext_params subs_shift e -(* - * Auxiliary function for binding properties and parameters - * Substitute a property into an extension e at distance d from initial - * Get d from a map of context indexes to distances for efficiency - * - * Can still make this more efficient, but not sure if it's worth it - *) - let sub_ext_property ds pi pb env i e = - let d = List.assoc i ds in - let d_to_p = d - pi in - let p_shift = shift_ext_by d_to_p pb in - let subs = build_substitution (ext_term p_shift) no_substitutions in - let subs_shift = shift_from_substitutions_by d_to_p subs in - substitute_ext_params subs_shift e - (* * Auxiliary function for binding properties and parameters * Substitute a property and parameters into an arrow m at distance d diff --git a/plugin/src/library/proofsearch/representation/proofcatterms.mli b/plugin/src/library/proofsearch/representation/proofcatterms.mli index d36ba79..6767023 100644 --- a/plugin/src/library/proofsearch/representation/proofcatterms.mli +++ b/plugin/src/library/proofsearch/representation/proofcatterms.mli @@ -1,10 +1,9 @@ (* Logic for proof categories that is specific to terms and types *) -open Term +open Constr open Environ open Proofcat open Names -open Assumptions (* --- Construction --- *) diff --git a/plugin/src/library/utilities/collections.ml b/plugin/src/library/utilities/collections.ml index 60c8ddf..60259f4 100644 --- a/plugin/src/library/utilities/collections.ml +++ b/plugin/src/library/utilities/collections.ml @@ -60,19 +60,19 @@ let rec combinations (l : 'a list) = * Cartesian product of two lists * From http://stackoverflow.com/questions/1507496/ocaml-permutation-of-every-value-in-two-sets-how-to-translate-this-from-java *) -let rec cartesian (l1 : 'a list) (l2 : 'b list) : ('a * 'b) list = +let cartesian (l1 : 'a list) (l2 : 'b list) : ('a * 'b) list = List.concat (List.map (fun a -> List.map (fun b -> (a, b)) l2) l1) (* * Combine all permutations of pairs of elements in lists l1 and l2 via f *) -let rec combine_cartesian (f : 'a -> 'b -> 'c) (l1 : 'a list) (l2 : 'b list) : 'c list = +let combine_cartesian (f : 'a -> 'b -> 'c) (l1 : 'a list) (l2 : 'b list) : 'c list = List.map (fun (a, b) -> f a b) (cartesian l1 l2) (* * Turns an array of lists into a list of arrays *) -let rec combine_cartesian_append (al : 'a list array) : 'a array list = +let combine_cartesian_append (al : 'a list array) : 'a array list = let al' = Array.to_list (Array.map (List.map (fun a -> [a])) al) in if (Array.length al) <= 1 then List.map Array.of_list (List.concat al') @@ -128,6 +128,8 @@ let rec map3 (f : 'a -> 'b -> 'c -> 'd) l1 l2 l3 : 'd list = [] | (h1 :: t1, h2 :: t2, h3 :: t3) -> let r = f h1 h2 h3 in r :: map3 f t1 t2 t3 + | _ -> + failwith "illegal call to map3" (* * Get the head of a transformation on a list, diff --git a/plugin/src/patcher.ml4 b/plugin/src/patcher.ml4 index cccf486..b322e89 100644 --- a/plugin/src/patcher.ml4 +++ b/plugin/src/patcher.ml4 @@ -1,6 +1,6 @@ DECLARE PLUGIN "patch" -open Term +open Constr open Names open Environ open Coqterms @@ -53,14 +53,14 @@ let _ = Goptions.declare_bool_option { (* Intern terms corresponding to two definitions *) let intern_defs d1 d2 : types * types = - let (evm, env) = Lemmas.get_current_context() in + let (evm, env) = Pfedit.get_current_context() in let d1 = intern env evm d1 in let d2 = intern env evm d2 in (unwrap_definition env d1, unwrap_definition env d2) (* Initialize diff & search configuration *) let configure trm1 trm2 cut : goal_proof_diff * options = - let (evm, env) = Lemmas.get_current_context() in + let (evm, env) = Pfedit.get_current_context() in let cut_term = Option.map (intern env evm) cut in let lemma = Option.map (build_cut_lemma env) cut_term in let c1 = eval_proof env trm1 in @@ -86,7 +86,7 @@ let invert_patch n env evm patch = (* Common patch command functionality *) let patch n old_term new_term try_invert a search = - let (evm, env) = Lemmas.get_current_context() in + let (evm, env) = Pfedit.get_current_context () in let reduce = try_reduce reduce_remove_identities in let patch = reduce env (search env evm a) in let prefix = Id.to_string n in @@ -129,7 +129,7 @@ let patch_proof n d_old d_new cut = * It just might be useful in the future, so feel free to play with it *) let patch_theorem n d_old d_new t = - let (evm, env) = Lemmas.get_current_context() in + let (evm, env) = Pfedit.get_current_context() in let (old_term, new_term) = (intern env evm d_old, intern env evm d_new) in patch n old_term new_term false t (fun env evm t -> @@ -139,20 +139,20 @@ let patch_theorem n d_old d_new t = (* Invert a term *) let invert n trm : unit = - let (evm, env) = Lemmas.get_current_context() in + let (evm, env) = Pfedit.get_current_context() in let body = lookup_definition env (intern env evm trm) in invert_patch n env evm body (* Specialize a term *) let specialize n trm : unit = - let (evm, env) = Lemmas.get_current_context() in + let (evm, env) = Pfedit.get_current_context() in let reducer = specialize_body specialize_term in let specialized = reducer env (intern env evm trm) in ignore (define_term n evm specialized false) (* Abstract a term by a function or arguments *) let abstract n trm goal : unit = - let (evm, env) = Lemmas.get_current_context() in + let (evm, env) = Pfedit.get_current_context() in let c = lookup_definition env (intern env evm trm) in let goal_type = unwrap_definition env (intern env evm goal) in let config = configure_from_goal env goal_type c in @@ -174,7 +174,7 @@ let abstract n trm goal : unit = (* Factor a term into a sequence of lemmas *) let factor n trm : unit = - let (evm, env) = Lemmas.get_current_context() in + let (evm, env) = Pfedit.get_current_context() in let body = lookup_definition env (intern env evm trm) in let fs = reconstruct_factors (factor_term env body) in let prefix = Id.to_string n in