transf compute: use a more general reduction engine

Makefile.in

@@ -135,7 +135,7 @@ LIB_TRANSFORM = simplify_formula inlining split_goal induction \
 		introduction abstraction close_epsilon lift_epsilon \
 		eliminate_epsilon \
 		eval_match instantiate_predicate smoke_detector \
-		compute
+		reduction_engine compute
 
 LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq pvs isabelle \
 	      simplify gappa cvc3 yices mathematica

src/core/decl.mli

@@ -51,7 +51,7 @@ val ls_defn_decrease : ls_defn -> int list
     from a declaration; on the result of [make_ls_defn],
     [ls_defn_decrease] will always return an empty list. *)
 
-(** {2 Inductive predicate declaration} *)
+(** {2 Proposition names} *)
 
 type prsymbol = private {
   pr_name : ident;
@@ -68,6 +68,8 @@ val pr_equal : prsymbol -> prsymbol -> bool
 
 val pr_hash : prsymbol -> int
 
+(** {2 Inductive predicate declaration} *)
+
 type ind_decl = lsymbol * (prsymbol * term) list
 
 type ind_sign = Ind | Coind

src/transform/compute.ml

@@ -64,7 +64,7 @@ let ls_minus = ref ps_equ (* temporary *)
 
 let const_equality c1 c2 =
   match c1,c2 with
-  | Number.ConstInt i1, Number.ConstInt i2 -> 
+  | Number.ConstInt i1, Number.ConstInt i2 ->
     BigInt.eq (Number.compute_int i1) (Number.compute_int i2)
   | _ -> raise Undetermined
 
@@ -168,6 +168,7 @@ let add_builtin_th env (l,n,t,d) =
     Format.eprintf "[Compute] theory %s not found@." n
 
 let get_builtins env =
+  Hls.clear builtins;
   Hls.add builtins ps_equ eval_equ;
   List.iter (add_builtin_th env) built_in_theories
 
@@ -255,6 +256,7 @@ and compute_app env ls tl ty =
         match tl with
         | [ { t_node = Tapp(ls1,tl1) } ] ->
           (* if ls is a projection and ls1 is a constructor,
+
              we should compute that projection *)
           let rec iter dl =
             match dl with
@@ -322,6 +324,59 @@ let compute env task =
   | _ -> assert false
 
 let () =
-  Trans.register_env_transform_l "compute" 
+  Trans.register_env_transform_l "compute"
     (fun env -> Trans.store (compute env))
     ~desc:"Compute@ as@ much@ as@ possible"
+
+
+
+
+(* compute with rewrite rules *)
+
+
+
+let collect_rule_decl prs e d =
+  match d.Decl.d_node with
+    | Decl.Dtype _ | Decl.Ddata _ | Decl.Dparam _ | Decl.Dind  _
+    | Decl.Dlogic _ -> e
+    | Decl.Dprop(_, pr, t) ->
+      if Decl.Spr.mem pr prs then
+        Reduction_engine.add_rule t e
+      else e
+
+let collect_rules prs t =
+  Task.task_fold
+    (fun e td -> match td.Theory.td_node with
+      | Theory.Decl d -> collect_rule_decl prs e d
+      | _ -> e)
+    (Reduction_engine.create ()) t
+
+let normalize_goal (prs : Decl.Spr.t) task =
+  let engine = collect_rules prs task in
+  match task with
+  | Some
+      { task_decl =
+          { td_node = Decl { d_node = Dprop (Pgoal, pr, f) } };
+        task_prev = prev;
+      } ->
+(*
+    get_builtins env;
+*)
+    let f = Reduction_engine.normalize engine f in
+    begin match f.t_node with
+    | Ttrue -> []
+    | _ ->
+      let d = Decl.create_prop_decl Pgoal pr f in
+      [Task.add_decl prev d]
+    end
+  | _ -> assert false
+
+
+let meta = Theory.register_meta "rewrite" [Theory.MTprsymbol]
+  ~desc:"Declares@ the@ given@ prop@ as@ a@ rewrite@ rule."
+
+let normalize_transf =
+  Trans.on_tagged_pr meta (fun prs -> Trans.store (normalize_goal prs))
+
+let () = Trans.register_transform_l "compute_in_goal" normalize_transf
+  ~desc:"Normalize@ terms@ with@ respect@ to@ rewrite@ rules@ declared as metas"

src/transform/reduction_engine.ml

+
+open Term
+
+type rule = vsymbol list * term list * term
+type engine = rule list Mls.t
+
+
+(*
+
+  A configuration is a pair (t,s) where t is a stack of terms and s is a
+  stack of function symbols.
+
+  A configuration ([t1;..;tn],[f1;..;fk]) represents a whole term, its
+  model, as defined recursively by
+
+    model([t],[]) = t
+
+    model(t1::..::tn::t,f::s) = model(f(t1,..,tn)::t,s)
+      where f as arity n
+
+  A given term can be "exploded" into a configuration by reversing the
+  rules above
+
+  During reduction, the terms in the first stack are kept in normal
+  form. The normalization process can be defined as the repeated
+  application of the following rules.
+
+  ([t],[]) --> t  // t is in normal form
+
+  if f(t1,..,tn) is not a redex then
+  (t1::..::tn::t,f::s) --> (f(t1,..,tn)::t,s)
+
+  if f(t1,..,tn) is a redex l sigma for a rule l -> r then
+  (t1::..::tn::t,f::s) --> (subst(sigma) @ t,explode(r) @ s)
+
+
+
+
+*)
+
+type value =
+| Term of term    (* invariant: is in normal form *)
+(* TODO, for optimization
+| Int of BigInt.t
+*)
+
+type substitution = term Mvs.t
+
+type cont =
+| Kapp of lsymbol * Ty.ty option
+| Kif of term * term * substitution
+| Klet of vsymbol * term * substitution
+| Kcase of term_branch list * substitution
+| Keps of vsymbol
+| Kquant of quant * vsymbol list * trigger
+| Kbinop of binop
+| Knot
+| Keval of term * substitution
+
+type config = {
+  value_stack : value list;
+  cont_stack : cont list;
+}
+
+
+exception NoMatch
+
+let first_order_matching (vars : Svs.t) (largs : term list)
+    (args : term list) : substitution =
+  let rec loop sigma largs args =
+    match largs,args with
+      | [],[] -> sigma
+      | t1::r1, t2::r2 ->
+        begin
+(*
+          Format.eprintf "matching terms %a and %a...@."
+            Pretty.print_term t1 Pretty.print_term t2;
+*)
+          match t1.t_node with
+            | Tvar vs when Svs.mem vs vars ->
+              begin
+                try let t = Mvs.find vs sigma in
+                    if t_equal t t2 then
+                      loop sigma r1 r2
+                    else
+                      raise NoMatch
+                with Not_found ->
+                  loop (Mvs.add vs t2 sigma) r1 r2
+              end
+            | Tapp(ls1,args1) ->
+              begin
+                match t2.t_node with
+                  | Tapp(ls2,args2) when ls_equal ls1 ls2 ->
+                    loop sigma (List.rev_append args1 r1)
+                      (List.rev_append args2 r2)
+                  | _ -> raise NoMatch
+              end
+            | _ ->
+(*
+              Format.eprintf "are these terms equal ?...";
+*)
+              if t_equal t1 t2 then
+                begin
+(*
+                  Format.eprintf " yes!@.";
+*)
+                  loop sigma r1 r2
+                end
+              else
+                begin
+(*
+                  Format.eprintf " no@.";
+*)
+                  raise NoMatch
+                end
+        end
+      | _ -> raise NoMatch
+  in
+  loop Mvs.empty largs args
+
+
+
+exception Undetermined
+
+let rec matching sigma t p =
+  match p.pat_node with
+  | Pwild -> sigma
+  | Pvar v -> Mvs.add v t sigma
+  | Por(p1,p2) ->
+    begin
+      try matching sigma t p1
+      with NoMatch -> matching sigma t p2
+    end
+  | Pas(p,v) -> matching (Mvs.add v t sigma) t p
+  | Papp(ls1,pl) ->
+    match t.t_node with
+      | Tapp(ls2,tl) ->
+        if ls_equal ls1 ls2 then
+          List.fold_left2 matching sigma tl pl
+        else
+          if ls2.ls_constr > 0 then raise NoMatch
+          else raise Undetermined
+      | _ -> raise Undetermined
+
+
+
+
+let rec reduce engine c =
+  match c.value_stack, c.cont_stack with
+  | _, [] -> assert false
+  | st, Keval (t,sigma) :: rem -> reduce_eval st t sigma rem
+  | [], Kif _ :: _ -> assert false
+  | v :: st, Kif(t2,t3,sigma) :: rem ->
+    begin
+      match v with
+      | Term { t_node = Ttrue } ->
+        { value_stack = st ;
+          cont_stack = Keval(t2,sigma) :: rem }
+      | Term { t_node = Tfalse } ->
+        { value_stack = st ;
+          cont_stack = Keval(t3,sigma) :: rem }
+      | Term t1 ->
+        { value_stack =
+            Term (t_if t1 (t_subst sigma t2) (t_subst sigma t3)) :: st;
+          cont_stack = rem ;
+        }
+(* TODO
+      | Int _ -> assert false (* would be ill-typed *)
+*)
+    end
+  | [], Klet _ :: _ -> assert false
+  | (Term t1) :: st, Klet(v,t2,sigma) :: rem ->
+    { value_stack = st;
+      cont_stack = Keval(t2, Mvs.add v t1 sigma) :: rem;
+    }
+  | [], Kcase _ :: _ -> assert false
+  | (Term t1) :: st, Kcase(tbl,sigma) :: rem ->
+    reduce_match st t1 tbl sigma rem
+  | ([] | [_]), Kbinop _ :: _ -> assert false
+  | (Term t1) :: (Term t2) :: st, Kbinop op :: rem ->
+    { value_stack = Term (t_binary_simp op t1 t2) :: st;
+      cont_stack = rem;
+    }
+  | [], Knot :: _ -> assert false
+  | (Term t) :: st, Knot :: rem ->
+    { value_stack = Term (t_not t) :: st;
+      cont_stack = rem;
+    }
+  | st, Kapp(ls,ty) :: rem ->
+    reduce_app st ls ty rem
+  | [], Keps _ :: _ -> assert false
+  | Term t :: st, Keps v :: rem ->
+    { value_stack = Term (t_eps_close v t) :: st;
+      cont_stack = rem;
+    }
+  | [], Kquant _ :: _ -> assert false
+  | Term t :: st, Kquant(q,vl,tr) :: rem ->
+    { value_stack = Term (t_quant_close q vl tr t) :: st;
+      cont_stack = rem;
+    }
+
+and reduce_match st u tbl sigma cont =
+  let rec iter tbl =
+    match tbl with
+    | [] -> assert false (* pattern matching not exhaustive *)
+    | b::rem ->
+      let p,t = t_open_branch b in
+      try
+        let sigma' = matching sigma u p in
+        { value_stack = st;
+          cont_stack = Keval(t,sigma') :: cont;
+        }
+      with NoMatch -> iter rem
+  in
+  try iter tbl with Undetermined ->
+    { value_stack = Term (t_case u tbl) :: st;
+      cont_stack = cont;
+    }
+
+
+and reduce_eval st t sigma rem =
+  match t.t_node with
+  | Tvar v ->
+    begin
+      try
+        let t = Mvs.find v sigma in
+        { value_stack = Term t :: st ;
+          cont_stack = rem;
+        }
+      with Not_found -> assert false
+    end
+  | Tif(t1,t2,t3) ->
+    { value_stack = st;
+      cont_stack = Keval(t1,sigma) :: Kif(t2,t3,sigma) :: rem;
+    }
+  | Tlet(t1,tb) ->
+    let v,t2 = t_open_bound tb in
+    { value_stack = st ;
+      cont_stack = Keval(t1,sigma) :: Klet(v,t2,sigma) :: rem }
+  | Tcase(t1,tbl) ->
+    { value_stack = st;
+      cont_stack = Keval(t1,sigma) :: Kcase(tbl,sigma) :: rem }
+  | Tbinop(op,t1,t2) ->
+    { value_stack = st;
+      cont_stack = Keval(t1,sigma) :: Keval(t2,sigma) :: Kbinop op :: rem;
+    }
+  | Tnot t1 ->
+    { value_stack = st;
+      cont_stack = Keval(t1,sigma) :: Knot :: rem;
+    }
+  | Teps tb ->
+    let v,t1 = t_open_bound tb in
+    { value_stack = st ;
+      cont_stack = Keval(t1,sigma) :: Keps v :: rem;
+    }
+  | Tquant(q,tq) ->
+    let vl,tr,t1 = t_open_quant tq in
+    { value_stack = st;
+      cont_stack = Keval(t1,sigma) :: Kquant(q,vl,tr) :: rem;
+    }
+  | Tapp(ls,tl) ->
+    let args = List.rev_map (fun t -> Keval(t,sigma)) tl in
+    { value_stack = st;
+      cont_stack = List.rev_append args (Kapp(ls,t.t_ty) :: rem);
+    }
+  | Ttrue | Tfalse | Tconst _ ->
+    { value_stack = Term t :: st;
+      cont_stack = rem;
+    }
+
+and reduce_app st ls ty rem =
+  let rec extract_first n acc l =
+    if n = 0 then acc,l else
+      match l with
+      | Term x :: r ->
+        extract_first (n-1) (x::acc) r
+      | [] -> assert false
+  in
+  let arity = List.length ls.ls_args in
+  let args,rem_st = extract_first arity [] st in
+(*
+  try
+    let f = Hls.find builtins ls in
+    f ls tl ty
+  with Not_found ->
+*)
+(*
+    try
+      let d = Ident.Mid.find ls.ls_name env.tknown in
+      match d.Decl.d_node with
+      | Decl.Dtype _ | Decl.Dprop _ -> assert false
+      | Decl.Dlogic dl ->
+        (* regular definition *)
+        let d = List.assq ls dl in
+        let l,t = Decl.open_ls_defn d in
+        let env' = multibind_vs l tl env in
+        compute_in_term env' t
+      | Decl.Dparam _ | Decl.Dind _ ->
+        t_app ls tl ty
+      | Decl.Ddata dl ->
+        (* constructor or projection *)
+        match tl with
+        | [ { t_node = Tapp(ls1,tl1) } ] ->
+          (* if ls is a projection and ls1 is a constructor,
+
+             we should compute that projection *)
+          let rec iter dl =
+            match dl with
+            | [] -> t_app ls tl ty
+            | (_,csl) :: rem ->
+              let rec iter2 csl =
+                match csl with
+                | [] -> iter rem
+                | (cs,prs) :: rem2 ->
+                  if ls_equal cs ls1
+                  then
+                    (* we found the right constructor *)
+                    let rec iter3 prs tl1 =
+                      match prs,tl1 with
+                      | (Some pr)::prs, t::tl1 ->
+                        if ls_equal ls pr
+                        then (* projection found! *) t
+                        else
+                          iter3 prs tl1
+                      | None::prs, _::tl1 ->
+                        iter3 prs tl1
+                      | _ -> t_app ls tl ty
+                    in iter3 prs tl1
+                  else iter2 rem2
+              in iter2 csl
+          in iter dl
+        | _ -> t_app ls tl ty
+    with Not_found ->
+*)
+(*
+      Format.eprintf "[Compute] definition of logic symbol %s not found@."
+        ls.ls_name.Ident.id_string;
+*)
+      { value_stack = Term (t_app ls args ty) :: rem_st;
+        cont_stack = rem;
+      }
+
+
+
+(* TODO *)
+
+let rec many_steps engine c n =
+  match c.value_stack, c.cont_stack with
+  | [Term t], [] -> t
+  | _, [] -> assert false
+  | _ -> if n = 0 then assert false else
+      let c = reduce engine c in
+      many_steps engine c (n-1)
+
+let normalize engine t = 
+  let c = { value_stack = []; cont_stack = [Keval(t,Mvs.empty)] } in
+  many_steps engine c 1000
+
+let create () = Mls.empty
+
+exception NotARewriteRule of string
+
+let add_rule _t _e = assert false

src/transform/reduction_engine.mli

+
+
+(*********************
+
+{1 A reduction engine for Why3 terms}
+
+*************************)
+
+(*
+terms are normalized with respect to
+
+1) built-in computation rules
+
+ a) on propositional connectives, e.g.
+
+   f /\ true -> f
+
+ b) on integers, e.g.
+
+   35 + 7 -> 42
+
+ c) on projections of pairs and of other ADTs, e.g
+
+  fst (x,y) -> x
+
+  cdr (Cons x y) -> y
+
+ d) on defined function symbols, e.g.
+
+  function sqr (x:int) = x * x
+
+  sqr 4 -> 4 * 4 -> 16
+
+  sqr x -> x * x
+
+ e) (TODO?) on booleans, e.g.
+
+  True xor False -> True
+
+ f) (TODO?) on reals, e.g.
+
+  1.0 + 2.5 -> 3.5
+
+2) axioms declared as rewrite rules, thanks to the "rewrite" metas, e.g. if
+
+    function dot : t -> t -> t
+    axiom assoc: forall x y z, dot (dot x y) z = dot x (dot y z)
+    meta "rewrite" assoc
+
+  then
+
+  dot (dot a b) (dot c d) -> dot a (dot b (dot c d))
+
+  axioms used as rewrite rules must be either of the form
+
+    forall ... t1 = t2
+
+  or
+
+    forall ... f1 <-> f2
+
+   where the root symbol of t1 (resp. f1) is a non-interpreted function
+   symbol (resp. non-interpreted predicate symbol)
+
+  rewriting is done from left to right
+
+
+*)
+
+type engine
+
+val normalize : engine -> Term.term -> Term.term
+
+val create : unit -> engine
+
+exception NotARewriteRule of string
+
+val add_rule : Term.term -> engine -> engine
+

tests/test_compute.why

@@ -15,4 +15,11 @@ theory T
 
   goal h1: 2+2=4
 
+  type t = { f : int }
+
+  goal i1: let x = { f = 4 } in x.f < 5
+
+  goal i2: let  x = { f = 4 } in
+    match x with { f = y } -> y + 1 > 3 end
+
 end

tests/test_compute/why3session.xml

@@ -5,33 +5,47 @@
 <file name="../test_compute.why" expanded="true">
 <theory name="T" expanded="true">
  <goal name="g1" sum="1ad4ea691c2d3b0a420f5b0819ebc531" expanded="true">
- <transf name="compute" expanded="true">
+ <transf name="compute_in_goal" expanded="true">
  </transf>
  </goal>
  <goal name="g2" sum="ff207d8c26146a3871613afb3a9ac891" expanded="true">
- <transf name="compute" expanded="true">
+ <transf name="compute_in_goal" expanded="true">
   <goal name="g2.1" expl="1." sum="c42af3c02ebf5e859a4dcf65db69d973">
   </goal>
  </transf>
  </goal>
  <goal name="g3" sum="059bfb681820ff98c7d4f1682433c247" expanded="true">
- <transf name="compute" expanded="true">
+ <transf name="compute_in_goal" expanded="true">
  </transf>
  </goal>
  <goal name="g10" sum="de9cadc887ffe8cc81f58a6d7c218b44" expanded="true">
- <transf name="compute" expanded="true">
-  <goal name="g10.1" expl="1." sum="c42af3c02ebf5e859a4dcf65db69d973">
+ <transf name="compute_in_goal" expanded="true">
+  <goal name="g10.1" expl="1." sum="f00e1dfbb01a6a6b20dbaf11948dcbc0">
   </goal>
  </transf>
  </goal>
  <goal name="g11" sum="8e9637aa282b824dc1ef410b939e7235" expanded="true">
- <transf name="compute" expanded="true">
-  <goal name="g11.1" expl="1." sum="c42af3c02ebf5e859a4dcf65db69d973">
+ <transf name="compute_in_goal" expanded="true">
+  <goal name="g11.1" expl="1." sum="f00e1dfbb01a6a6b20dbaf11948dcbc0">
   </goal>
  </transf>
  </goal>
  <goal name="h1" sum="5d9ea52d9f6b9033794f44b5aa590306" expanded="true">
- <transf name="compute" expanded="true">
+ <transf name="compute_in_goal" expanded="true">
+  <goal name="h1.1" expl="1." sum="3ec24f1a92fb220b819dc1ee528ae1b6">
+  </goal>
+ </transf>
+ </goal>
+ <goal name="i1" sum="dfe815a019525fce8a2b755ff30f708a" expanded="true">
+ <transf name="compute_in_goal" expanded="true">
+  <goal name="i1.1" expl="1." sum="c11f16854e4ae49e1988dc7055044e7d">
+  </goal>
+ </transf>
+ </goal>
+ <goal name="i2" sum="28f0e4a6c637d7af3829655f5173f1e7" expanded="true">
+ <transf name="compute_in_goal" expanded="true">
+  <goal name="i2.1" expl="1." sum="2311d64bc0d33b2e7a1b0a9f813c6a83">
+  </goal>
  </transf>
  </goal>
 </theory>