Commit 2fba6975 authored by MARCHE Claude's avatar MARCHE Claude

extended the use_api example and fixed the bench

parent 70badf6c
...@@ -1141,13 +1141,14 @@ testl-type: bin/why3.byte ...@@ -1141,13 +1141,14 @@ testl-type: bin/why3.byte
test-api.byte: examples/use_api/use_api.ml lib/why3/why3.cma test-api.byte: examples/use_api/use_api.ml lib/why3/why3.cma
$(if $(QUIET),@echo 'Ocaml $<' &&) \ $(if $(QUIET),@echo 'Ocaml $<' &&) \
ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< \ ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< \
|| (printf "Test of Why API calls failed. Please fix it"; exit 2) || (rm -f test-api.byte; printf "Test of Why API calls failed. Please fix it"; exit 2)
@rm -f test-api.byte;
test-api.opt: examples/use_api/use_api.ml lib/why3/why3.cmxa test-api.opt: examples/use_api/use_api.ml lib/why3/why3.cmxa
$(if $(QUIET),@echo 'Ocamlopt $<' &&) \ $(if $(QUIET),@echo 'Ocamlopt $<' &&) \
($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa $< \ ($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa $< \
&& ./test-api.opt) \ && ./test-api.opt) \
|| (printf "Test of Why API calls failed. Please fix it"; exit 2) || (rm -f test-api.opt; printf "Test of Why API calls failed. Please fix it"; exit 2)
@rm -f test-api.opt @rm -f test-api.opt
#test-shape: lib/why3/why3.cma #test-shape: lib/why3/why3.cma
...@@ -1156,14 +1157,16 @@ test-api.opt: examples/use_api/use_api.ml lib/why3/why3.cmxa ...@@ -1156,14 +1157,16 @@ test-api.opt: examples/use_api/use_api.ml lib/why3/why3.cmxa
test-session.byte: examples/use_api/create_session.ml lib/why3/why3.cma test-session.byte: examples/use_api/create_session.ml lib/why3/why3.cma
$(if $(QUIET),@echo 'Ocaml $<' &&) \ $(if $(QUIET),@echo 'Ocaml $<' &&) \
ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< \ ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< \
|| (printf "Test of Why API calls for Session module failed. Please fix it"; exit 2) || (rm -f why3session.xml; \
printf "Test of Why API calls for Session module failed. Please fix it"; exit 2)
@rm -f why3session.xml @rm -f why3session.xml
test-session.opt: examples/use_api/create_session.ml lib/why3/why3.cmxa test-session.opt: examples/use_api/create_session.ml lib/why3/why3.cmxa
$(if $(QUIET),@echo 'Ocamlopt $<' &&) \ $(if $(QUIET),@echo 'Ocamlopt $<' &&) \
($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa $< \ ($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa $< \
&& ./test-session.opt) \ && ./test-session.opt) \
|| (printf "Test of Why API calls for Session module failed. Please fix it"; exit 2) || (rm -f test-session.opt why3session.xml; \
printf "Test of Why API calls for Session module failed. Please fix it"; exit 2)
@rm -f test-session.opt why3session.xml @rm -f test-session.opt why3session.xml
......
...@@ -351,40 +351,42 @@ let d2 = ...@@ -351,40 +351,42 @@ let d2 =
} }
in in
let body = let body =
(* ref 0 *) (* building expression "ref 0" *)
let e = let e =
(* recall that "ref" has type forall 'a, 'a -> ref 'a *) (* recall that "ref" has type "(v:'a) -> ref 'a". We need to build an
(* (???) we built the instance of 'a by int *) instance of it *)
(* (???) or we built a dummy effective parameter of type int ? *) (* we first built a dummy effective parameter v of type int *)
let pv = let pv =
Mlw_ty.create_pvsymbol Mlw_ty.create_pvsymbol
(Ident.id_fresh "a") (Mlw_ty.vty_value Mlw_ty.ity_int) (Ident.id_fresh "v") (Mlw_ty.vty_value Mlw_ty.ity_int)
in in
(* ity is (ref int) with a *fresh* region *) (* we build "ref int" with a *fresh* region *)
let ity = Mlw_ty.ity_app_fresh ref_type [Mlw_ty.ity_int] in let ity = Mlw_ty.ity_app_fresh ref_type [Mlw_ty.ity_int] in
(* ??? the type (int -> ref <fresh region> int) ? *) (* we build the type "(v:int) -> ref <fresh region> int)" *)
let vta = Mlw_ty.vty_arrow [pv] (Mlw_ty.VTvalue (Mlw_ty.vty_value ity)) in let vta = Mlw_ty.vty_arrow [pv] (Mlw_ty.VTvalue (Mlw_ty.vty_value ity)) in
(* e1 : the appropriate instance of "ref" *)
let e1 = Mlw_expr.e_arrow ref_fun vta in let e1 = Mlw_expr.e_arrow ref_fun vta in
(* we apply it to 0 *)
let c0 = Mlw_expr.e_const (Number.ConstInt (Number.int_const_dec "0")) in let c0 = Mlw_expr.e_const (Number.ConstInt (Number.int_const_dec "0")) in
Mlw_expr.e_app e1 [c0] Mlw_expr.e_app e1 [c0]
in in
(* let x = ref 0 *) (* building the first part of the let x = ref 0 *)
let letdef = Mlw_expr.create_let_defn (Ident.id_fresh "x") e in let letdef = Mlw_expr.create_let_defn (Ident.id_fresh "x") e in
(* get back the variable x *)
let var_x = match letdef.Mlw_expr.let_sym with let var_x = match letdef.Mlw_expr.let_sym with
| Mlw_expr.LetV vs -> vs | Mlw_expr.LetV vs -> vs
| Mlw_expr.LetA _ -> assert false | Mlw_expr.LetA _ -> assert false
in in
(* !x *) (* building expression "!x" *)
let bang_x = let bang_x =
(* recall that "!" as type forall 'a. ref 'a -> 'a *) (* recall that "!" as type "ref 'a -> 'a" *)
let pv = (* we build a dummy parameter r of the same type as x *)
Mlw_ty.create_pvsymbol (Ident.id_fresh "r") var_x.Mlw_ty.pv_vtv
in
let vta = let vta =
Mlw_ty.vty_arrow [pv] Mlw_ty.vty_arrow [var_x]
(Mlw_ty.VTvalue (Mlw_ty.vty_value Mlw_ty.ity_int)) (Mlw_ty.VTvalue (Mlw_ty.vty_value Mlw_ty.ity_int))
in in
Mlw_expr.e_arrow get_fun vta let e1 = Mlw_expr.e_arrow get_fun vta in
Mlw_expr.e_app e1 [Mlw_expr.e_value var_x]
in in
(* the complete body *) (* the complete body *)
Mlw_expr.e_let letdef bang_x Mlw_expr.e_let letdef bang_x
...@@ -420,5 +422,5 @@ let () = ...@@ -420,5 +422,5 @@ let () =
(* (*
ocamlc -I ../../lib/why3 -c use_api.ml ocaml -I ../../lib/why3 unix.cma nums.cma str.cma dynlink.cma ../../lib/why3/why3.cma use_api.ml
*) *)
...@@ -34,6 +34,7 @@ module rec T : sig ...@@ -34,6 +34,7 @@ module rec T : sig
its_priv : bool; its_priv : bool;
} }
(** ity = individual type in programs, first-order, i.e. no functions *)
and ity = private { and ity = private {
ity_node : ity_node; ity_node : ity_node;
ity_vars : varset; ity_vars : varset;
...@@ -85,6 +86,8 @@ exception UnboundRegion of region ...@@ -85,6 +86,8 @@ exception UnboundRegion of region
val create_region : preid -> ity -> region val create_region : preid -> ity -> region
(** creation of a symbol for type in programs *)
val create_itysymbol : val create_itysymbol :
preid -> ?abst:bool -> ?priv:bool -> ?inv:bool -> preid -> ?abst:bool -> ?priv:bool -> ?inv:bool ->
tvsymbol list -> region list -> ity option -> itysymbol tvsymbol list -> region list -> ity option -> itysymbol
......
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