Commit 70badf6c authored by MARCHE Claude's avatar MARCHE Claude

Jessie3: new attempt to use ref.(!)

parent 038febb8
......@@ -181,7 +181,7 @@ let () = printf "@[On task 4, alt-ergo answers %a@."
(* create a theory *)
let () = printf "@[creating theory 'My_theory'@]@."
let my_theory : Theory.theory_uc =
let my_theory : Theory.theory_uc =
Theory.create_theory (Ident.id_fresh "My_theory")
(* add declarations of goals *)
......@@ -193,7 +193,7 @@ let my_theory : Theory.theory_uc = Theory.add_decl my_theory decl_goal1
let () = printf "@[adding goal 2@]@."
let my_theory : Theory.theory_uc = Theory.add_param_decl my_theory prop_var_A
let my_theory : Theory.theory_uc = Theory.add_param_decl my_theory prop_var_B
let decl_goal2 : Decl.decl =
let decl_goal2 : Decl.decl =
Decl.create_prop_decl Decl.Pgoal goal_id2 fmla2
let my_theory : Theory.theory_uc = Theory.add_decl my_theory decl_goal2
......@@ -224,11 +224,11 @@ let () = printf "@[theory is:@\n%a@]@." Pretty.print_theory my_theory
(* getting set of task from a theory *)
let my_tasks : Task.task list =
let my_tasks : Task.task list =
List.rev (Task.split_theory my_theory None None)
let () =
let () =
printf "Tasks are:@.";
let _ =
List.fold_left
......@@ -251,10 +251,10 @@ let mul_int : Term.lsymbol =
let unit_type = Ty.ty_tuple []
(* declaration of
let f (_dummy:unit) : unit
let f (_dummy:unit) : unit
requires { true }
ensures { true }
=
=
assert { 6*7 = 42 }
*)
let d =
......@@ -290,13 +290,13 @@ let d =
let def = Mlw_expr.create_fun_defn (Ident.id_fresh "f") lambda in
Mlw_decl.create_rec_decl [def]
(*
(*
declaration of
let f (_dummy:unit) : unit
let f (_dummy:unit) : unit
requires { true }
ensures { result = 0 }
=
=
let x = ref 0 in
!x
......@@ -305,12 +305,12 @@ declaration of
(* import the ref.Ref module *)
let ref_modules, ref_theories =
let ref_modules, ref_theories =
Env.read_lib_file (Mlw_main.library_of_env env) ["ref"]
let ref_module : Mlw_module.modul = Stdlib.Mstr.find "Ref" ref_modules
let ref_type : Mlw_ty.T.itysymbol =
let ref_type : Mlw_ty.T.itysymbol =
match
Mlw_module.ns_find_ts ref_module.Mlw_module.mod_export ["ref"]
with
......@@ -318,7 +318,7 @@ let ref_type : Mlw_ty.T.itysymbol =
| Mlw_module.TS _ -> assert false
(* the "ref" function *)
let ref_fun : Mlw_expr.psymbol =
let ref_fun : Mlw_expr.psymbol =
match
Mlw_module.ns_find_ps ref_module.Mlw_module.mod_export ["ref"]
with
......@@ -326,6 +326,15 @@ let ref_fun : Mlw_expr.psymbol =
| _ -> assert false
(* the "!" function *)
let get_fun : Mlw_expr.psymbol =
match
Mlw_module.ns_find_ps ref_module.Mlw_module.mod_export ["prefix !"]
with
| Mlw_module.PS p -> p
| _ -> assert false
let d2 =
let args =
[Mlw_ty.create_pvsymbol
......@@ -342,14 +351,43 @@ let d2 =
}
in
let body =
let pv = Mlw_ty.create_pvsymbol (Ident.id_fresh "a") (Mlw_ty.vty_value Mlw_ty.ity_int) in
let ity = Mlw_ty.ity_app_fresh ref_type [Mlw_ty.ity_int] in
let vta = Mlw_ty.vty_arrow [pv] (Mlw_ty.VTvalue (Mlw_ty.vty_value ity)) in
let e1 = Mlw_expr.e_arrow ref_fun vta in
let c0 = Mlw_expr.e_const (Number.ConstInt (Number.int_const_dec "0")) in
let e = Mlw_expr.e_app e1 [c0] in
(* ref 0 *)
let e =
(* recall that "ref" has type forall 'a, 'a -> ref 'a *)
(* (???) we built the instance of 'a by int *)
(* (???) or we built a dummy effective parameter of type int ? *)
let pv =
Mlw_ty.create_pvsymbol
(Ident.id_fresh "a") (Mlw_ty.vty_value Mlw_ty.ity_int)
in
(* ity is (ref int) with a *fresh* region *)
let ity = Mlw_ty.ity_app_fresh ref_type [Mlw_ty.ity_int] in
(* ??? the type (int -> ref <fresh region> int) ? *)
let vta = Mlw_ty.vty_arrow [pv] (Mlw_ty.VTvalue (Mlw_ty.vty_value ity)) in
let e1 = Mlw_expr.e_arrow ref_fun vta in
let c0 = Mlw_expr.e_const (Number.ConstInt (Number.int_const_dec "0")) in
Mlw_expr.e_app e1 [c0]
in
(* let x = ref 0 *)
let letdef = Mlw_expr.create_let_defn (Ident.id_fresh "x") e in
Mlw_expr.e_let letdef c0
let var_x = match letdef.Mlw_expr.let_sym with
| Mlw_expr.LetV vs -> vs
| Mlw_expr.LetA _ -> assert false
in
(* !x *)
let bang_x =
(* recall that "!" as type forall 'a. ref 'a -> 'a *)
let pv =
Mlw_ty.create_pvsymbol (Ident.id_fresh "r") var_x.Mlw_ty.pv_vtv
in
let vta =
Mlw_ty.vty_arrow [pv]
(Mlw_ty.VTvalue (Mlw_ty.vty_value Mlw_ty.ity_int))
in
Mlw_expr.e_arrow get_fun vta
in
(* the complete body *)
Mlw_expr.e_let letdef bang_x
in
let lambda = {
Mlw_expr.l_args = args;
......@@ -378,3 +416,9 @@ let () =
Printexc.print_backtrace stderr;
flush stderr
*)
(*
ocamlc -I ../../lib/why3 -c use_api.ml
*)
......@@ -508,17 +508,9 @@ let mk_ref ty =
let vta = Mlw_ty.vty_arrow [pv] (Mlw_ty.VTvalue (Mlw_ty.vty_value ity)) in
Mlw_expr.e_arrow ref_fun vta
let mk_get ty =
let mk_get ref_ty ty =
try
let vty = Mlw_ty.vty_value ty in
let r = match vty.Mlw_ty.vtv_mut with
| Some r -> r
| None -> assert false
in
let ity = Mlw_ty.ity_app ref_type [ty] [r] in
let pv =
Mlw_ty.create_pvsymbol (Ident.id_fresh "a") vty
in
let pv = Mlw_ty.create_pvsymbol (Ident.id_fresh "r") ref_ty in
let vta = Mlw_ty.vty_arrow [pv] (Mlw_ty.VTvalue (Mlw_ty.vty_value ty)) in
Mlw_expr.e_arrow get_fun vta
with e ->
......@@ -557,11 +549,11 @@ let get_var v =
let lval (host,offset) =
match host,offset with
| Var v, NoOffset ->
| Var v, NoOffset ->
let v,ty = get_var v in
begin try
Mlw_expr.e_app
(mk_get ty)
Mlw_expr.e_app
(mk_get v.Mlw_ty.pv_vty ty)
[Mlw_expr.e_value v]
with e ->
Self.fatal "Exception raised during application of !@ %a@."
......@@ -607,11 +599,11 @@ let binop op e1 e2 =
| Ge|Eq|Ne|BAnd|BXor|BOr|LAnd|LOr ->
Self.not_yet_implemented "binop"
let constant c =
let constant c =
match c with
| CInt64(_t,_ikind, Some s) ->
| CInt64(_t,_ikind, Some s) ->
Number.ConstInt (Literals.integer s)
| CInt64(_t,_ikind, None) ->
| CInt64(_t,_ikind, None) ->
Self.not_yet_implemented "constant CInt64/None"
| CStr _
| CWStr _
......@@ -619,13 +611,13 @@ let constant c =
| CReal (_, _, _)
| CEnum _ ->
Self.not_yet_implemented "constant"
let rec expr e =
match e.enode with
| Const c -> Mlw_expr.e_const (constant c)
| Lval lv -> lval lv
| BinOp (op, e1, e2, _loc) ->
binop op (expr e1) (expr e2)
binop op (expr e1) (expr e2)
| SizeOf _
| SizeOfE _
| SizeOfStr _
......@@ -643,8 +635,8 @@ let assignment (lhost,offset) e _loc =
| Var v , NoOffset ->
let v,ty = get_var v in
begin try
Mlw_expr.e_app
(mk_set ty)
Mlw_expr.e_app
(mk_set ty)
[Mlw_expr.e_value v; expr e]
with e ->
Self.fatal "Exception raised during application of :=@ %a@."
......
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