st/lama_byterun
1
0
Fork 0
mirror of https://github.com/ProgramSnail/Lama.git synced 2025-12-24 15:48:47 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

SM/Stmt

Browse source
This commit is contained in:
Dmitry Boulytchev 2018-02-20 02:53:58 +03:00
commit 84bea2d60b
7 changed files with 200 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

4
regression/Makefile
View file

@ -15,10 +15,10 @@ all: .depend $(TOPFILE).opt
$(OCAMLDEP) $(PXFLAGS) *.ml > .depend
$(TOPFILE).opt: $(SOURCES:.ml=.cmx)
$(OCAMLOPT) -o $(TOPFILE).opt $(OFLAGS) $(LIBS:.cma=.cmxa) ostap.cmx Expr.cmx Embedding.cmx $(SOURCES:.ml=.cmx)
$(OCAMLOPT) -o $(TOPFILE).opt $(OFLAGS) $(LIBS:.cma=.cmxa) ostap.cmx Syntax.cmx Embedding.cmx SM.cmx $(SOURCES:.ml=.cmx)
$(TOPFILE).byte: $(SOURCES:.ml=.cmo)
$(OCAMLC) -o $(TOPFILE).byte $(BFLAGS) $(LIBS) ostap.cmo Expr.cmo Embedding.cmo $(SOURCES:.ml=.cmo)
$(OCAMLC) -o $(TOPFILE).byte $(BFLAGS) $(LIBS) ostap.cmo Syntax.cmo Embedding.cmo SM.cmo $(SOURCES:.ml=.cmo)
clean:
rm -Rf *.cmi *.cmo *.cmx *.annot *.o *.opt *.byte *~

16
regression/common.ml
View file

@ -1,6 +1,16 @@
open GT
open 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

1
regression/test.sh
View file

@ -1 +1,2 @@
make clean
make TOPFILE=test000