st/lama_byterun
1
0
Fork 0
mirror of https://github.com/ProgramSnail/Lama.git synced 2025-12-05 22:38:44 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Merge remote-tracking branch 'origin/hw2'

Browse source 
* origin/hw2:
  Fixed common.ml/Syntax.ml
  Fixed common.mlyet again
  Fixed SM.run
  Added SM.run
  Fixed common.ml
  Sync
  Added CONST instruction
This commit is contained in:
Podkopaev Anton 2018-03-06 17:58:54 +03:00
commit 29cd925266
4 changed files with 281 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

16
regression/common.ml Normal file
View file

@ -0,0 +1,16 @@
open GT
open Syntax
let conj = (&&)
open Embedding
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