From f3bc389b62c34c8d6a80fb4525b3a8a146c8f22a Mon Sep 17 00:00:00 2001 From: Dmitry Boulytchev Date: Sun, 25 Feb 2018 20:35:54 +0300 Subject: [PATCH] Fixed common.ml --- regression/common.ml | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/regression/common.ml b/regression/common.ml index b44940b1d..fa06cbe4e 100644 --- a/regression/common.ml +++ b/regression/common.ml @@ -1,6 +1,16 @@ open GT -open Syntax.Expr +open Syntax + +let conj = (&&) + open Embedding -let state ps = List.fold_right (fun (x, v) s -> update x v s) ps empty -let eval s e = Printf.printf "%d\n" (eval s e) +let state ps = List.fold_right (fun (x, v) (s, p) -> Expr.update x v s, (x =:= !? v) :: p) ps (Expr.empty, []) +let eval (s, p) e = + let orig = Expr.eval s e in + let stmt = List.fold_right (fun p s -> p |> s) p (Stmt.Write e) in + let [s_orig] = eval [] stmt in + let [sm_orig] = SM.run [] (SM.compile stmt) in + if conj (orig = s_orig) (orig = sm_orig) + then Printf.printf "%d\n" orig + else Printf.printf "*** divergence: %d %d %d\n" orig s_orig sm_orig