Commit 6dae9d0e authored by MARCHE Claude's avatar MARCHE Claude

Defunctionalization: Ocaml extraction and a few tests.

Problem: lambda is not extracted into a fun ... -> ...
parent d530cdcd
......@@ -203,7 +203,10 @@ pvsbin/
/examples/*/*/*/*.tex
/examples/use_api/runstrat/makejob.opt
/examples/use_api/runstrat/runstrat.opt
/examples/euler001/euler001__*.ml
/examples/euler001/Makefile
/examples/sudoku/euler001__*.ml
/examples/in_progress/defunctionalization/defunctionalization__*.ml
# modules
/modules/string/
......
MAIN = main
OBJ = defunctionalization__Expr \
defunctionalization__DirectSem \
defunctionalization__CPS \
defunctionalization__Defunctionalization \
ML = $(addsuffix .ml, $(OBJ))
CMO = $(addsuffix .cmo, $(OBJ))
CMX = $(addsuffix .cmx, $(OBJ))
ZARITH = $(shell ocamlfind query -i-format zarith)
# NUMLIB = zarith
NUMLIB = nums
WHY3 = $(shell ocamlfind query -i-format why3)
OCAMLOPT = ocamlopt -noassert -inline 1000
all: $(MAIN).opt
doc:
why3doc ../defunctionalization.mlw
why3session html ../defunctionalization.mlw
$(MAIN).byte: $(CMO) $(MAIN).cmo
ocamlc -g $(ZARITH) $(WHY3) $(NUMLIB).cma why3extract.cma -o $@ $^
$(MAIN).opt: $(CMX) $(MAIN).cmx
$(OCAMLOPT) $(ZARITH) $(WHY3) $(NUMLIB).cmxa why3extract.cmxa -o $@ $^
$(MAIN).cmx: $(CMX)
$(ML): ../defunctionalization.mlw
why3 -E ocaml ../defunctionalization.mlw -o .
%.cmx: %.ml
$(OCAMLOPT) $(WHY3) -annot -c $<
%.cmo: %.ml
ocamlc $(WHY3) -annot -g -c $<
%.cmi: %.mli
ocamlc $(WHY3) -annot -g -c $<
clean::
rm -f $(ML) *.cm[xio] $(MAIN).opt
open Why3extract
open Format
let usage () =
eprintf "Exercises on CPS and de-functionalization@.";
eprintf "Usage: %s" Sys.argv.(0);
exit 2
let input =
if Array.length Sys.argv <> 1 then usage ()
open Defunctionalization__Expr
let rec p_expr fmt e =
match e with
| Cte n -> fprintf fmt "%s" (Why3__BigInt.to_string n)
| Sub(e1,e2) ->
fprintf fmt "%a - %a" p_expr e1 p_expr e2
let p_prog fmt p = p_expr fmt p
let p_value fmt v =
fprintf fmt "%s" (Why3__BigInt.to_string v)
let run s f p =
let v = f p in
printf "%s (%a): %a@." s p_prog p p_value v
let () =
printf "Exercise 0: direct semantics@.";
let i = Defunctionalization__DirectSem.interpret_0 in
run "interpret_0" i Defunctionalization__Expr.p0;
run "interpret_0" i Defunctionalization__Expr.p1;
run "interpret_0" i Defunctionalization__Expr.p2;
run "interpret_0" i Defunctionalization__Expr.p3;
run "interpret_0" i Defunctionalization__Expr.p4;
printf "Done.@\n@."
(* does not work because lambda is not extracted into OCaml
(fun ... -> ...)
let () =
printf "Exercise 1: CPS@.";
let i = Defunctionalization__CPS.interpret_1 in
run "interpret_1" i Defunctionalization__Expr.p0;
run "interpret_1" i Defunctionalization__Expr.p1;
run "interpret_1" i Defunctionalization__Expr.p2;
run "interpret_1" i Defunctionalization__Expr.p3;
run "interpret_1" i Defunctionalization__Expr.p4;
printf "Done.@\n@."
*)
let () =
printf "Exercise 2: Defunctionalization@.";
let i = Defunctionalization__Defunctionalization.interpret_2 in
run "interpret_2" i Defunctionalization__Expr.p0;
run "interpret_2" i Defunctionalization__Expr.p1;
run "interpret_2" i Defunctionalization__Expr.p2;
run "interpret_2" i Defunctionalization__Expr.p3;
run "interpret_2" i Defunctionalization__Expr.p4;
printf "Done.@\n@."
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment