Rolling up our own representation of clauses.

4 files changed, 98 insertions, 37 deletions

diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 13f150381a..4bcbe69b07 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Locus
 open Globnames
 open Genredexpr
 open Tac2expr
@@ -47,13 +46,11 @@ let to_constr_with_bindings v = match Value.to_tuple v with
 | [| c; bnd |] -> (Value.to_constr c, to_bindings bnd)
 | _ -> assert false
 
-let to_int_or_var i = Misctypes.ArgArg (Value.to_int i)
-
-let to_occurrences f = function
+let to_occurrences = function
 | ValInt 0 -> AllOccurrences
-| ValBlk (0, [| vl |]) -> AllOccurrencesBut (Value.to_list f vl)
+| ValBlk (0, [| vl |]) -> AllOccurrencesBut (Value.to_list Value.to_int vl)
 | ValInt 1 -> NoOccurrences
-| ValBlk (1, [| vl |]) -> OnlyOccurrences (Value.to_list f vl)
+| ValBlk (1, [| vl |]) -> OnlyOccurrences (Value.to_list Value.to_int vl)
 | _ -> assert false
 
 let to_hyp_location_flag v = match Value.to_int v with
@@ -66,11 +63,11 @@ let to_clause v = match Value.to_tuple v with
 | [| hyps; concl |] ->
   let cast v = match Value.to_tuple v with
   | [| hyp; occ; flag |] ->
-    ((to_occurrences to_int_or_var occ, Value.to_ident hyp), to_hyp_location_flag flag)
+    (Value.to_ident hyp, to_occurrences occ, to_hyp_location_flag flag)
   | _ -> assert false
   in
   let hyps = Value.to_option (fun h -> Value.to_list cast h) hyps in
-  { onhyps = hyps; concl_occs = to_occurrences to_int_or_var concl; }
+  { onhyps = hyps; concl_occs = to_occurrences concl; }
 | _ -> assert false
 
 let to_red_flag v = match Value.to_tuple v with
@@ -87,10 +84,10 @@ let to_red_flag v = match Value.to_tuple v with
 | _ -> assert false
 
 let to_pattern_with_occs pat =
-  to_pair Value.to_pattern (fun occ -> to_occurrences to_int_or_var occ) pat
+  to_pair Value.to_pattern to_occurrences pat
 
 let to_constr_with_occs c =
-  to_pair Value.to_constr (fun occ -> to_occurrences to_int_or_var occ) c
+  to_pair Value.to_constr to_occurrences c
 
 let rec to_intro_pattern v = match Value.to_block v with
 | (0, [| b |]) -> IntroForthcoming (Value.to_bool b)
@@ -259,11 +256,11 @@ end
 let () = define_prim1 "tac_generalize" begin fun cl ->
   let cast v = match Value.to_tuple v with
   | [| c; occs; na |] ->
-    ((to_occurrences Value.to_int occs, Value.to_constr c), to_name na)
+    (Value.to_constr c, to_occurrences occs, to_name na)
   | _ -> assert false
   in
   let cl = Value.to_list cast cl in
-  Tactics.new_generalize_gen cl
+  Tac2tactics.generalize cl
 end
 
 let () = define_prim1 "tac_assert" begin fun ast ->
@@ -291,7 +288,7 @@ let () = define_prim3 "tac_set" begin fun ev p cl ->
   Proofview.tclEVARMAP >>= fun sigma ->
   thaw p >>= fun p ->
   let (na, c) = to_pair to_name Value.to_constr p in
-  Tactics.letin_pat_tac ev None na (sigma, c) cl
+  Tac2tactics.letin_pat_tac ev None na (sigma, c) cl
 end
 
 let () = define_prim5 "tac_remember" begin fun ev na c eqpat cl ->
@@ -326,12 +323,12 @@ end
 
 let () = define_prim1 "tac_red" begin fun cl ->
   let cl = to_clause cl in
-  Tactics.reduce (Red false) cl
+  Tac2tactics.reduce (Red false) cl
 end
 
 let () = define_prim1 "tac_hnf" begin fun cl ->
   let cl = to_clause cl in
-  Tactics.reduce Hnf cl
+  Tac2tactics.reduce Hnf cl
 end
 
 let () = define_prim3 "tac_simpl" begin fun flags where cl ->
@@ -360,7 +357,7 @@ let () = define_prim2 "tac_lazy" begin fun flags cl ->
 end
 
 let () = define_prim2 "tac_unfold" begin fun refs cl ->
-  let map v = to_pair Value.to_reference (fun occ -> to_occurrences to_int_or_var occ) v in
+  let map v = to_pair Value.to_reference to_occurrences v in
   let refs = Value.to_list map refs in
   let cl = to_clause cl in
   Tac2tactics.unfold refs cl
@@ -369,7 +366,7 @@ end
 let () = define_prim2 "tac_fold" begin fun args cl ->
   let args = Value.to_list Value.to_constr args in
   let cl = to_clause cl in
-  Tactics.reduce (Fold args) cl
+  Tac2tactics.reduce (Fold args) cl
 end
 
 let () = define_prim2 "tac_pattern" begin fun where cl ->
@@ -442,7 +439,7 @@ let () = define_red2 "eval_lazy" begin fun flags c ->
 end
 
 let () = define_red2 "eval_unfold" begin fun refs c ->
-  let map v = to_pair Value.to_reference (fun occ -> to_occurrences to_int_or_var occ) v in
+  let map v = to_pair Value.to_reference to_occurrences v in
   let refs = Value.to_list map refs in
   let c = Value.to_constr c in
   Tac2tactics.eval_unfold refs c
@@ -455,7 +452,7 @@ let () = define_red2 "eval_fold" begin fun args c ->
 end
 
 let () = define_red2 "eval_pattern" begin fun where c ->
-  let where = Value.to_list (fun p -> to_pair Value.to_constr (fun occ -> to_occurrences to_int_or_var occ) p) where in
+  let where = Value.to_list (fun p -> to_pair Value.to_constr to_occurrences p) where in
   let c = Value.to_constr c in
   Tac2tactics.eval_pattern where c
 end
@@ -569,7 +566,7 @@ end
 
 let () = define_prim1 "tac_symmetry" begin fun cl ->
   let cl = to_clause cl in
-  Tactics.intros_symmetry cl
+  Tac2tactics.symmetry cl
 end
 
 let () = define_prim2 "tac_split" begin fun ev bnd ->
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index 42916a9578..b55bd5c1b8 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -67,6 +67,23 @@ and mk_or_and_intro_pattern = function
 
 let mk_intro_patterns ipat = List.map mk_intro_pattern ipat
 
+let mk_occurrences f = function
+| AllOccurrences -> Locus.AllOccurrences
+| AllOccurrencesBut l -> Locus.AllOccurrencesBut (List.map f l)
+| NoOccurrences -> Locus.NoOccurrences
+| OnlyOccurrences l -> Locus.OnlyOccurrences (List.map f l)
+
+let mk_occurrences_expr occ =
+  mk_occurrences (fun i -> Misctypes.ArgArg i) occ
+
+let mk_hyp_location (id, occs, h) =
+  ((mk_occurrences_expr occs, id), h)
+
+let mk_clause cl = {
+  Locus.onhyps = Option.map (fun l -> List.map mk_hyp_location l) cl.onhyps;
+  Locus.concl_occs = mk_occurrences_expr cl.concl_occs;
+}
+
 let intros_patterns ev ipat =
   let ipat = mk_intro_patterns ipat in
   Tactics.intro_patterns ev ipat
@@ -93,6 +110,7 @@ let mk_destruction_arg = function
 let mk_induction_clause (arg, eqn, as_, occ) =
   let eqn = Option.map (fun ipat -> Loc.tag @@ mk_intro_pattern_naming ipat) eqn in
   let as_ = Option.map (fun ipat -> Loc.tag @@ mk_or_and_intro_pattern ipat) as_ in
+  let occ = Option.map mk_clause occ in
   ((None, mk_destruction_arg arg), (eqn, as_), occ)
 
 let induction_destruct isrec ev (ic : induction_clause list) using =
@@ -105,6 +123,11 @@ let elim ev c copt =
   let copt = Option.map mk_with_bindings copt in
   Tactics.elim ev None c copt
 
+let generalize pl =
+  let mk_occ occs = mk_occurrences (fun i -> i) occs in
+  let pl = List.map (fun (c, occs, na) -> (mk_occ occs, c), na) pl in
+  Tactics.new_generalize_gen pl
+
 let general_case_analysis ev c =
   let c = mk_with_bindings c in
   Tactics.general_case_analysis ev None c
@@ -131,9 +154,14 @@ let rewrite ev rw cl by =
     (Option.default true orient, repeat, None, delayed_of_tactic c)
   in
   let rw = List.map map_rw rw in
+  let cl = mk_clause cl in
   let by = Option.map (fun tac -> Tacticals.New.tclCOMPLETE tac, Equality.Naive) by in
   Equality.general_multi_rewrite ev rw cl by
 
+let symmetry cl =
+  let cl = mk_clause cl in
+  Tactics.intros_symmetry cl
+
 let forward fst tac ipat c =
   let ipat = Option.map mk_intro_pattern ipat in
   Tactics.forward fst tac ipat c
@@ -148,6 +176,7 @@ let assert_ = function
 
 let letin_pat_tac ev ipat na c cl =
   let ipat = Option.map (fun (b, ipat) -> (b, Loc.tag @@ mk_intro_pattern_naming ipat)) ipat in
+  let cl = mk_clause cl in
   Tactics.letin_pat_tac ev ipat na c cl
 
 (** Ltac interface treats differently global references than other term
@@ -155,9 +184,9 @@ let letin_pat_tac ev ipat na c cl =
     Instead, we parse indifferently any pattern and dispatch when the tactic is
     called. *)
 let map_pattern_with_occs (pat, occ) = match pat with
-| Pattern.PRef (ConstRef cst) -> (occ, Inl (EvalConstRef cst))
-| Pattern.PRef (VarRef id) -> (occ, Inl (EvalVarRef id))
-| _ -> (occ, Inr pat)
+| Pattern.PRef (ConstRef cst) -> (mk_occurrences_expr occ, Inl (EvalConstRef cst))
+| Pattern.PRef (VarRef id) -> (mk_occurrences_expr occ, Inl (EvalVarRef id))
+| _ -> (mk_occurrences_expr occ, Inr pat)
 
 let get_evaluable_reference = function
 | VarRef id -> Proofview.tclUNIT (EvalVarRef id)
@@ -167,44 +196,57 @@ let get_evaluable_reference = function
     Nametab.pr_global_env Id.Set.empty r ++ spc () ++
     str "to an evaluable reference.")
 
+let reduce r cl =
+  let cl = mk_clause cl in
+  Tactics.reduce r cl
+
 let simpl flags where cl =
   let where = Option.map map_pattern_with_occs where in
+  let cl = mk_clause cl in
   Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
   let flags = { flags with rConst } in
   Tactics.reduce (Simpl (flags, where)) cl
 
 let cbv flags cl =
+  let cl = mk_clause cl in
   Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
   let flags = { flags with rConst } in
   Tactics.reduce (Cbv flags) cl
 
 let cbn flags cl =
+  let cl = mk_clause cl in
   Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
   let flags = { flags with rConst } in
   Tactics.reduce (Cbn flags) cl
 
 let lazy_ flags cl =
+  let cl = mk_clause cl in
   Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
   let flags = { flags with rConst } in
   Tactics.reduce (Lazy flags) cl
 
 let unfold occs cl =
+  let cl = mk_clause cl in
   let map (gr, occ) =
+    let occ = mk_occurrences_expr occ in
     get_evaluable_reference gr >>= fun gr -> Proofview.tclUNIT (occ, gr)
   in
   Proofview.Monad.List.map map occs >>= fun occs ->
   Tactics.reduce (Unfold occs) cl
 
 let pattern where cl =
-  let where = List.map (fun (c, occ) -> (occ, c)) where in
+  let where = List.map (fun (c, occ) -> (mk_occurrences_expr occ, c)) where in
+  let cl = mk_clause cl in
   Tactics.reduce (Pattern where) cl
 
 let vm where cl =
   let where = Option.map map_pattern_with_occs where in
+  let cl = mk_clause cl in
   Tactics.reduce (CbvVm where) cl
 
 let native where cl =
   let where = Option.map map_pattern_with_occs where in
+  let cl = mk_clause cl in
   Tactics.reduce (CbvNative where) cl
 
 let eval_fun red c =
@@ -244,6 +286,7 @@ let eval_lazy flags c =
 
 let eval_unfold occs c =
   let map (gr, occ) =
+    let occ = mk_occurrences_expr occ in
     get_evaluable_reference gr >>= fun gr -> Proofview.tclUNIT (occ, gr)
   in
   Proofview.Monad.List.map map occs >>= fun occs ->
@@ -253,7 +296,7 @@ let eval_fold cl c =
   eval_fun (Fold cl) c
 
 let eval_pattern where c =
-  let where = List.map (fun (pat, occ) -> (occ, pat)) where in
+  let where = List.map (fun (pat, occ) -> (mk_occurrences_expr occ, pat)) where in
   eval_fun (Pattern where) c
 
 let eval_vm where c =
@@ -303,6 +346,7 @@ let injection ev ipat arg =
 let autorewrite ~all by ids cl =
   let conds = if all then Some Equality.AllMatches else None in
   let ids = List.map Id.to_string ids in
+  let cl = mk_clause cl in
   match by with
   | None -> Autorewrite.auto_multi_rewrite ?conds ids cl
   | Some by -> Autorewrite.auto_multi_rewrite_with ?conds by ids cl
diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli
index 842b09c22f..3d64e7ec8c 100644
--- a/src/tac2tactics.mli
+++ b/src/tac2tactics.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Locus
 open Globnames
 open Tac2expr
 open EConstr
@@ -31,6 +30,8 @@ val elim : evars_flag -> constr_with_bindings -> constr_with_bindings option ->
 
 val general_case_analysis : evars_flag -> constr_with_bindings ->  unit tactic
 
+val generalize : (constr * occurrences * Name.t) list -> unit tactic
+
 val constructor_tac : evars_flag -> int option -> int -> bindings -> unit tactic
 
 val left_with_bindings  : evars_flag -> bindings -> unit tactic
@@ -40,6 +41,8 @@ val split_with_bindings : evars_flag -> bindings -> unit tactic
 val rewrite :
   evars_flag -> rewriting list -> clause -> unit tactic option -> unit tactic
 
+val symmetry : clause -> unit tactic
+
 val forward : bool -> unit tactic option option ->
   intro_pattern option -> constr -> unit tactic
 
@@ -48,8 +51,10 @@ val assert_ : assertion -> unit tactic
 val letin_pat_tac : evars_flag -> (bool * intro_pattern_naming) option ->
   Name.t -> (Evd.evar_map * constr) -> clause -> unit tactic
 
+val reduce : Redexpr.red_expr -> clause -> unit tactic
+
 val simpl : global_reference glob_red_flag ->
-  (Pattern.constr_pattern * occurrences_expr) option -> clause -> unit tactic
+  (Pattern.constr_pattern * occurrences) option -> clause -> unit tactic
 
 val cbv : global_reference glob_red_flag -> clause -> unit tactic
 
@@ -57,20 +62,20 @@ val cbn : global_reference glob_red_flag -> clause -> unit tactic
 
 val lazy_ : global_reference glob_red_flag -> clause -> unit tactic
 
-val unfold : (global_reference * occurrences_expr) list -> clause -> unit tactic
+val unfold : (global_reference * occurrences) list -> clause -> unit tactic
 
-val pattern : (constr * occurrences_expr) list -> clause -> unit tactic
+val pattern : (constr * occurrences) list -> clause -> unit tactic
 
-val vm : (Pattern.constr_pattern * occurrences_expr) option -> clause -> unit tactic
+val vm : (Pattern.constr_pattern * occurrences) option -> clause -> unit tactic
 
-val native : (Pattern.constr_pattern * occurrences_expr) option -> clause -> unit tactic
+val native : (Pattern.constr_pattern * occurrences) option -> clause -> unit tactic
 
 val eval_red : constr -> constr tactic
 
 val eval_hnf : constr -> constr tactic
 
 val eval_simpl : global_reference glob_red_flag ->
-  (Pattern.constr_pattern * occurrences_expr) option -> constr -> constr tactic
+  (Pattern.constr_pattern * occurrences) option -> constr -> constr tactic
 
 val eval_cbv : global_reference glob_red_flag -> constr -> constr tactic
 
@@ -78,15 +83,15 @@ val eval_cbn : global_reference glob_red_flag -> constr -> constr tactic
 
 val eval_lazy : global_reference glob_red_flag -> constr -> constr tactic
 
-val eval_unfold : (global_reference * occurrences_expr) list -> constr -> constr tactic
+val eval_unfold : (global_reference * occurrences) list -> constr -> constr tactic
 
 val eval_fold : constr list -> constr -> constr tactic
 
-val eval_pattern : (EConstr.t * occurrences_expr) list -> constr -> constr tactic
+val eval_pattern : (EConstr.t * occurrences) list -> constr -> constr tactic
 
-val eval_vm : (Pattern.constr_pattern * occurrences_expr) option -> constr -> constr tactic
+val eval_vm : (Pattern.constr_pattern * occurrences) option -> constr -> constr tactic
 
-val eval_native : (Pattern.constr_pattern * occurrences_expr) option -> constr -> constr tactic
+val eval_native : (Pattern.constr_pattern * occurrences) option -> constr -> constr tactic
 
 val discriminate : evars_flag -> destruction_arg option -> unit tactic
 
diff --git a/src/tac2types.mli b/src/tac2types.mli
index 6845de8c7c..1cacbefc88 100644
--- a/src/tac2types.mli
+++ b/src/tac2types.mli
@@ -53,11 +53,26 @@ and or_and_intro_pattern =
 | IntroOrPattern of intro_pattern list list
 | IntroAndPattern of intro_pattern list
 
+type occurrences =
+| AllOccurrences
+| AllOccurrencesBut of int list
+| NoOccurrences
+| OnlyOccurrences of int list
+
+type hyp_location_flag = Locus.hyp_location_flag =
+| InHyp | InHypTypeOnly | InHypValueOnly
+
+type hyp_location = Id.t * occurrences * hyp_location_flag
+
+type clause =
+  { onhyps : hyp_location list option;
+    concl_occs : occurrences }
+
 type induction_clause =
   destruction_arg *
   intro_pattern_naming option *
   or_and_intro_pattern option *
-  Locus.clause option
+  clause option
 
 type multi = Misctypes.multi =
 | Precisely of int