merge

README.md

@@ -52,7 +52,6 @@ has a bug
 
 
 
-<<<<<<< HEAD
 
 
 # What is inside the `root directory` ?
@@ -82,22 +81,7 @@ opam switch 4.14.0+flambda
 dune exec ./hip.exe ../src/programs.t/parse_test.ml
 
 
-=======
 TODO:
 design the experiments to show that:
 re-reasoning does not cause too much overhead. 
-we can reason about multi-shot efficiently. 
-
-# Build web version
-
-```sh
-npm install z3-solver
-npm install -g browserify
-dune build @web
-```
-
-```sh
-cd _build/default
-python -m http.server 8005
-```
->>>>>>> f109ddd921f33788f54cb5cd9addd7342a165288
+we can reason about multi-shot efficiently. 

parsing/Pretty.ml

@@ -561,7 +561,7 @@ let rec detectfailedAssertions (spec:spec) : spec =
   | Require (pi, heap) :: xs  -> 
     (
       let pi' = Provers.normalPure pi in 
-      match Provers.entailConstrains pi' (False) with 
+      match ProversEx.entailConstrains pi' (False) with 
       | true  -> [Require (False , heap)]
       | _ -> Require (pi' , heap) ::  detectfailedAssertions xs 
     )

parsing/ProversEx.ml

@@ -0,0 +1,9 @@
+open Types
+
+let entailConstrains pi1 pi2 =
+  let sat = not (Provers.askZ3 (Not (Or (Not pi1, pi2)))) in
+  (*
+  print_string (showPure pi1 ^" -> " ^ showPure pi2 ^" == ");
+  print_string (string_of_bool (sat) ^ "\n");
+  *)
+  sat

parsing/dune

@@ -66,7 +66,7 @@
 
 (library
  (name core)
- (modules Rewriting Pretty entail forward_rules incr_rules)
+ (modules ProversEx Rewriting Pretty entail forward_rules incr_rules)
  (libraries types provers)
  (inline_tests)
  (preprocess (pps ppx_expect ppx_deriving.std)))

parsing/hiplib.ml

@@ -897,7 +897,7 @@ let res =
       let rhs = (And(p2,  Atomic(EQ, Var v2, t2) )) in 
       (*print_endline ( "yoyo1\n");
       print_endline (string_of_pi (!unifyGlobal));*)
-      (Provers.entailConstrains (And(lhs, !unifyGlobal)) rhs)
+      (ProversEx.entailConstrains (And(lhs, !unifyGlobal)) rhs)
 
     else 
       (match (t2) with 
@@ -909,11 +909,11 @@ let res =
         else 
           let lhs = (And(p1,  Atomic(EQ, Var v1, t1) )) in 
           let rhs = (And(p2,  Atomic(EQ, Var v2, t2) )) in 
-          (Provers.entailConstrains (And(lhs, !unifyGlobal)) rhs)
+          (ProversEx.entailConstrains (And(lhs, !unifyGlobal)) rhs)
       | _ -> 
       let lhs = (And(p1,  Atomic(EQ, Var v1, t1) )) in 
       let rhs = (And(p2,  Atomic(EQ, Var v2, t2) )) in 
-      (Provers.entailConstrains (And(lhs, !unifyGlobal)) rhs))
+      (ProversEx.entailConstrains (And(lhs, !unifyGlobal)) rhs))
 
   | (SepConj ( sp1, sp2), SepConj ( sp3, sp4)) -> 
     speration_logic_ential (p1, sp1) (p2, sp3) && speration_logic_ential (p1, sp2) (p2, sp4)
@@ -929,15 +929,15 @@ let checkEntialmentForNormalFlow (lhs:normalStage) (rhs:normalStage) : bool =
   let () = exGlobal := !exGlobal @ ex1 @ ex2 in 
   let (contravariant) = speration_logic_ential (pi3, heap3) (pi1, heap1) in 
   let (covariant)     = speration_logic_ential (pi2, heap2) (pi4, heap4) in 
-  let returnValue   = Provers.entailConstrains !unifyGlobal (Atomic(EQ, r1, r2)) in 
+  let returnValue   = ProversEx.entailConstrains !unifyGlobal (Atomic(EQ, r1, r2)) in 
   covariant && contravariant && returnValue
 
 
 let rec compareEffectArgument unification v1 v2 =  
   match (v1, v2) with 
   | ([], []) -> true 
   | (x::xs, y::ys) -> 
-    let r1 = Provers.entailConstrains unification (Atomic(EQ, x, y)) in 
+    let r1 = ProversEx.entailConstrains unification (Atomic(EQ, x, y)) in 
     r1 && (compareEffectArgument unification xs ys)
   | (_, _) -> false 
 
@@ -990,7 +990,7 @@ let rec entailmentchecking (lhs:normalisedStagedSpec list) (rhs:normalisedStaged
     r1 && r2
 
 
-let run_string incremental line =
+let run_string_ incremental line =
   let progs = Parser.implementation Lexer.token (Lexing.from_string line) in
   let _effs, methods = transform_strs progs in
   List.iter (fun (_name, _params, given_spec, body) ->
@@ -1072,6 +1072,9 @@ let run_string incremental line =
     end
   ) methods
 
+let run_string incr s =
+  Provers.handle (fun () -> run_string_ incr s)
+
 let main () =
   let inputfile = (Sys.getcwd () ^ "/" ^ Sys.argv.(1)) in
 (*    let outputfile = (Sys.getcwd ()^ "/" ^ Sys.argv.(2)) in
@@ -1118,4 +1121,3 @@ print_string (inputfile ^ "\n" ^ outputfile^"\n");*)
       raise e                      (* 以出错的形式退出: 文件已关闭,但通道没有写入东西 *)
 
    ;;
-

provers/js/provers.ml

@@ -62,7 +62,6 @@ type _ Effect.t += Ask : pi -> bool t
 
 let askZ3 v = perform (Ask v)
 let entails_exists _ _ _ = true
-let entailConstrains _ _ = true
 let normalPure p = p
 
 let handle f =

provers/native/provers.ml

@@ -132,14 +132,6 @@ let askZ3 pi =
     let () = historyTable := (hash_pi pi, re) :: !historyTable in
     re
 
-let entailConstrains pi1 pi2 =
-  let sat = not (askZ3 (Not (Or (Not pi1, pi2)))) in
-  (*
-  print_string (showPure pi1 ^" -> " ^ showPure pi2 ^" == ");
-  print_string (string_of_bool (sat) ^ "\n");
-  *)
-  sat
-
 let rec normalPure (pi : pi) : pi =
   match pi with
   | And (p1, p2) ->

provers/provers.mli

@@ -2,6 +2,5 @@ open Types
 
 val askZ3 : pi -> bool
 val entails_exists : pi -> string list -> pi -> bool
-val entailConstrains : pi -> pi -> bool
 val handle : (unit -> unit) -> unit
 val normalPure : pi -> pi

src/evaluation/handler_types.ml

@@ -0,0 +1,25 @@
+effect Read : int 
+effect Write : int -> unit 
+
+let read () =
+  let n = perform Read in
+  perform (Write 2)
+  (* perform Read *)
+
+let main ()
+= match read () with
+  | v ->
+    Format.printf "normal %d@." v;
+    v
+  | effect Read k ->
+    Format.printf "read handler@.";
+    let v = continue k 1 in
+    Format.printf "read %d@." v;
+    v + 1
+  | effect (Write n) k ->
+    Format.printf "write handler %d@." n;
+    let v = continue k () in
+    Format.printf "write %d@." v;
+    v
+
+let () = ignore (main ())