Merge branch 'dev'

src/core/Rewrite.ml

@@ -244,12 +244,15 @@ module Term = struct
 
      Use the FOTerm.DB case extensively... *)
 
-  let normalize_term_ (t:term): term * rule_set =
+  let normalize_term_ max_steps (t:term): term * rule_set =
+    assert (max_steps >= 0);
     let set = ref TR_set.empty in
+    let fuel = ref max_steps in
     (* compute normal form of subterm. Tail-recursive.
        @param k the continuation
        @return [t'] where [t'] is the normal form of [t] *)
     let rec reduce t k = match T.view t with
+      | _ when !fuel = 0 -> k t
       | T.Const id ->
         (* pick a constant rule *)
         begin match rules_of_id id |> Sequence.head with
@@ -258,6 +261,7 @@ module Term = struct
             assert (T.equal t r.term_lhs);
             set := TR_set.add r !set;
             Util.incr_stat stat_term_rw;
+            decr fuel;
             Util.debugf ~section 5
               "@[<2>rewrite `@[%a@]`@ using `@[%a@]`@]"
               (fun k->k T.pp t Rule.pp r);
@@ -295,6 +299,7 @@ module Term = struct
                        (fun k->k T.pp t' Rule.pp r Subst.pp subst);
                      set := TR_set.add r !set;
                      Util.incr_stat stat_term_rw;
+                     decr fuel;
                      (* NOTE: not efficient, will traverse [t'] fully *)
                      let t' = Subst.FO.apply_no_renaming subst (r.term_rhs,1) in
                      reduce t' k
@@ -319,10 +324,10 @@ module Term = struct
     in
     reduce t (fun t->t, !set)
 
-  let normalize_term (t:term): term * rule_set =
-    Util.with_prof prof_term_rw normalize_term_ t
+  let normalize_term ?(max_steps=max_int) (t:term): term * rule_set =
+    Util.with_prof prof_term_rw (normalize_term_ max_steps) t
 
-  let normalize_term_fst t = fst (normalize_term t)
+  let normalize_term_fst ?max_steps t = fst (normalize_term ?max_steps t)
 
   let narrow_term ?(subst=Subst.empty) ~scope_rules:sc_r (t,sc_t): _ Sequence.t =
     begin match T.view t with

src/core/Rewrite.mli

@@ -42,12 +42,13 @@ module Term : sig
 
   type rule_set = Set.t
 
-  val normalize_term : term -> term * rule_set
+  val normalize_term : ?max_steps:int -> term -> term * rule_set
   (** [normalize t] computes the normal form of [t] w.r.t the set
       of rewrite rules stored in IDs.
-      Returns the new term and the set of rules that were used *)
+      Returns the new term and the set of rules that were used
+      @param max_steps number of steps after which we stop *)
 
-  val normalize_term_fst : term -> term
+  val normalize_term_fst : ?max_steps:int -> term -> term
   (** Same as {!normalize_term} but ignores the set of rules *)
 
   (* TODO: [app f l] which is the same as [T.app f l], but also reduces

src/core/Test_prop.ml

@@ -71,11 +71,15 @@ let normalize_form (f:form): form =
     end
   in
   (* fixpoint of rewriting *)
-  let rec normalize (c:clause): clause Sequence.t =
+  let rec normalize_up_to fuel (c:clause): clause Sequence.t =
+    assert (fuel>=0);
+    if fuel=0 then Sequence.return c
+    else normalize_step (fuel-1) c
+  and normalize_step fuel c =
     let progress=ref false in
-    (* how to normalize a term/lit *)
+    (* how to normalize a term/lit (with restricted resources) *)
     let rw_term t =
-      let t', rules = RW.Term.normalize_term t in
+      let t', rules = RW.Term.normalize_term ~max_steps:10 t in
       if not (RW.Term.Set.is_empty rules) then progress := true;
       t'
     in
@@ -90,15 +94,15 @@ let normalize_form (f:form): form =
     in
     let cs = c |> rw_terms |> rw_clause |> rm_trivial in
     if !progress
-    then normalize_form cs (* normalize each result recursively *)
+    then normalize_form fuel cs (* normalize each result recursively *)
     else (
       (* done, just simplify *)
       Sequence.of_list cs |> Sequence.map simplify
     )
-  and normalize_form (f:form): clause Sequence.t =
-    Sequence.of_list f |> Sequence.flat_map normalize
+  and normalize_form fuel (f:form): clause Sequence.t =
+    Sequence.of_list f |> Sequence.flat_map (normalize_up_to fuel)
   in
-  normalize_form f |> Sequence.to_rev_list
+  normalize_form 3 f |> Sequence.to_rev_list
 
 module Narrow : sig
   val default_limit: int

src/prover/calculi/induction.ml

@@ -1112,10 +1112,13 @@ module Make
                replaced by variables. But first, simplify these clauses
                because otherwise the inductive subgoals
                (which are simplified) will not match
-               the inductive hypothesis. *)
+               the inductive hypothesis.
+
+               NOTE: do not use {!all_simplify} as it interacts badly
+               with avatar splitting. *)
             let clauses =
               C.of_statement st
-              |> CCList.flat_map (fun c -> fst (E.all_simplify c))
+              |> List.map (fun c -> fst (E.simplify c))
             in
             prove_by_ind clauses ~generalize_on:consts;
             (* "skip" in any case, because the proof is done in a cut anyway *)