remove deprecated code and various other warnings

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

plugin/src/core/components/abstraction/abstracters.mli

@@ -1,6 +1,6 @@
 (* --- Abstraction Strategies --- *)
 
-open Term
+open Constr
 open Environ
 open Candidates
 

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

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

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,27 +94,29 @@ 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) ->
      let p = mkRel pi in
      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
  *
  * 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"

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
 

plugin/src/core/components/differencing/appdifferencers.ml

@@ -1,20 +1,18 @@
 (* --- 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
 open Assumptions
 open Cutlemma
 open Specialization
 open Zooming
-open Printing
 open Debruijn
 open Filters
 
@@ -65,17 +63,17 @@ 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
            fs
          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,29 +82,31 @@ 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
          if non_empty fs then
            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
 	   let fs = diff_rec diff_f opts d_f in
 	   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) ->

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

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

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

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 --- *)