Added context to bdep solve

Author: Gustavo2622

examples/mapreduce_paper.ec

@@ -107,7 +107,7 @@ admit.
 admit.
 qed.
 
-lemma xor_left_eq_xor_right : forall (w: W8.t),  xor_left w = xor_right w.
+lemma xor_left_eq_xor_right (w: W8.t) : xor_left w = xor_right w.
     proof.
       bdep solve.
     qed.

src/ecCircuits.ml

@@ -134,6 +134,7 @@ module type CircuitInterface = sig
     type cache
     val update_cache : cache -> lpattern -> circuit -> cache
     val cache_get : cache -> ident -> circuit
+    val cache_add : cache -> ident -> circuit -> cache
     val empty_cache : cache
     val cache_map : (ident -> circuit -> circuit) -> cache -> cache
   end
@@ -809,6 +810,9 @@ module MakeCircuitInterfaceFromCBackend(Backend: CBackend) : CircuitInterface =
       with Not_found -> 
         assert false (* FIXME: Error handling *)
 
+    let cache_add (cache: cache) (idn: ident) (c: circuit) : cache = 
+      Map.add idn c cache 
+
     let empty_cache : cache = 
       Map.empty
 
@@ -1706,10 +1710,10 @@ let (op_cache : circuit Mp.t ref) = ref Mp.empty
 
 let circuit_of_form 
   ?(pstate  : pstate = empty_pstate) (* Program variable values *)
+  ?(cache   : cache  = empty_cache)
    (hyps    : hyps) 
    (f_      : EcAst.form) 
   : circuit =
-  let cache = empty_cache in
 
   let rec doit (cache: cache) (hyps: hyps) (f_: form) : hyps * circuit = 
     let env = toenv hyps in
@@ -2131,6 +2135,10 @@ let circuit_mapreduce ?(perm : (int -> int) option) (c: circuit) (w_in: width) (
 
 type circuit = ExampleInterface.circuit
 type pstate = ExampleInterface.PState.pstate
+type cache = ExampleInterface.LocalCache.cache
+let cache_get = cache_get
+let cache_add = cache_add
+let empty_cache = empty_cache 
 let circuit_to_string (c: circuit) : string = assert false
 let pstate_get = pstate_get 
 let pstate_get_opt = pstate_get_opt

src/ecCircuits.mli

@@ -11,6 +11,7 @@ module Map = Batteries.Map
 (* -------------------------------------------------------------------- *)
 type circuit 
 type pstate
+type cache
 
 (* -------------------------------------------------------------------- *)
 exception CircError of string
@@ -27,6 +28,11 @@ val pstate_get : pstate -> symbol -> circuit
 val pstate_get_opt : pstate -> symbol -> circuit option
 val pstate_get_all : pstate -> circuit list 
 
+(* Cache utilities *)
+val cache_get : cache -> ident -> circuit
+val cache_add : cache -> ident -> circuit -> cache
+val empty_cache : cache
+
 (* Transform circuits *)
 val circuit_ueq : circuit -> circuit -> circuit
 val circuit_aggregate : circuit list -> circuit
@@ -43,7 +49,7 @@ val circ_taut  : circuit -> bool
 
 (* Generate circuits *)
 (* Form processors *)
-val circuit_of_form : ?pstate:pstate -> hyps -> form -> circuit
+val circuit_of_form : ?pstate:pstate -> ?cache:cache -> hyps -> form -> circuit
 val circ_simplify_form_bitstring_equality :
   ?mem:EcMemory.memory ->
   ?pstate:pstate ->

src/phl/ecPhlBDep.ml

@@ -1000,10 +1000,36 @@ let process_bdep_eval (bdeinfo: bdep_eval_info) (tc: tcenv1) =
   let tc = EcPhlConseq.t_hoareS_conseq_nm pre post tc in
   FApi.t_last (t_bdep_eval n m inpvs outvs lane frange sign) tc 
 
+(* TODO: Figure out how to not repeat computations here? *) 
 let t_bdep_solve
   (tc : tcenv1) =
-  if circ_taut (circuit_of_form (FApi.tc1_hyps tc) (FApi.tc1_goal tc)) then
-  FApi.close (!@ tc) VBdep
-  else 
-  tc_error (FApi.tc1_penv tc) "Failed to solve goal through circuit reasoning@\n"  
-
+  begin 
+    let hyps = (FApi.tc1_hyps tc) in
+    let goal = (FApi.tc1_goal tc) in
+    let ctxt = tohyps hyps in
+    assert (ctxt.h_tvar = []);
+    let ctxt = ctxt.h_local in
+    let goal = List.fold_left (fun goal (id, lk) ->
+      match lk with
+      | EcBaseLogic.LD_var (t, Some f) -> 
+          begin try 
+            ignore (circuit_of_form hyps (f_forall [(id, GTty t)] f));
+            f_forall [(id, GTty t)] (f_and goal (f_eq (f_local id t) f))
+          with _ -> f_forall [(id, GTty t)] goal
+          end
+      | EcBaseLogic.LD_var (t, None) -> f_forall [(id, GTty t)] goal 
+      | EcBaseLogic.LD_hyp f -> 
+          begin try
+            ignore (circuit_of_form hyps f);
+            f_and f goal 
+          with _ -> goal 
+          end
+      | EcBaseLogic.LD_mem _ 
+      | EcBaseLogic.LD_modty _
+      | EcBaseLogic.LD_abs_st _ -> assert false
+    ) goal ctxt in
+    if circ_taut (circuit_of_form hyps goal) then
+    FApi.close (!@ tc) VBdep
+    else 
+    tc_error (FApi.tc1_penv tc) "Failed to solve goal through circuit reasoning@\n"  
+  end