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

Term evaluation: defined symbols, and first builtin symbols

parent 4d798089
......@@ -526,7 +526,7 @@ let do_theory env drv fname tname th glist elist =
let l,t = Decl.open_ls_defn d in
match l with
| [] ->
let t = Mlw_interp.eval_term Term.Mvs.empty Term.Mvs.empty t in
let t = Mlw_interp.eval_term env th.th_known t in
printf "@[<hov 2>Evaluation of %s:@ %a@]@." x Pretty.print_term t
| _ ->
eprintf "Symbol '%s' is not a constant in theory '%s'.@." x tname;
......
......@@ -77,7 +77,7 @@ let real_const_hex i f e =
(** Printing *)
let any_to_dec radix s =
let compute_any radix s =
let n = String.length s in
let rec compute acc i =
if i = n then
......@@ -91,7 +91,17 @@ let any_to_dec radix s =
assert (v < radix);
compute (add_int_big_int v (mult_int_big_int radix acc)) (i + 1)
end in
string_of_big_int (compute zero_big_int 0)
(compute zero_big_int 0)
let compute_int c =
match c with
| IConstDec s -> compute_any 10 s
| IConstHex s -> compute_any 16 s
| IConstOct s -> compute_any 8 s
| IConstBin s -> compute_any 2 s
let any_to_dec radix s =
string_of_big_int (compute_any radix s)
let power2 n =
string_of_big_int (power_int_positive_int 2 n)
......
......@@ -38,6 +38,8 @@ val int_const_bin : string -> integer_constant
InvalidConstantLiteral(base,s) is raised if [s] contains invalid
characters for the given base. *)
val compute_int : integer_constant -> Big_int.big_int
val real_const_dec : string -> string -> string option -> real_constant
val real_const_hex : string -> string -> string option -> real_constant
......
open Term
let eval_app ls tl ty =
if ls_equal ls ps_equ then
match tl with
| [t1;t2] ->
if t_equal_alpha t1 t2 then t_true else
t_app ls tl ty
(* TODO later
begin match t1.t_node,t2.t_node with
| Ttrue, Tfalse | Tfalse, Ttrue -> t_false
| Const c1, Const c2 -> eval_const ...
*)
| _ -> assert false
else
(* TODO : if has_definition ls then ... *)
try
t_app ls tl ty
with e ->
Format.eprintf "Exception during term evaluation (t_app_infer %s): %a@."
ls.ls_name.Ident.id_string
Exn_printer.exn_printer e;
exit 2
exception NoMatch
exception Undetermined
let builtins = Hls.create 17
let eval_equ _ls l =
match l with
| [t1;t2] ->
if t_equal_alpha t1 t2 then t_true else
t_equ t1 t2
(* TODO later
begin match t1.t_node,t2.t_node with
| Ttrue, Tfalse | Tfalse, Ttrue -> t_false
| Const c1, Const c2 -> eval_const ...
*)
| _ -> assert false
let add_const c1 c2 =
match c1,c2 with
| Number.ConstInt i1, Number.ConstInt i2 ->
let i1 = Number.compute_int i1 in
let i2 = Number.compute_int i2 in
let a = Big_int.add_big_int i1 i2 in
let s = Big_int.string_of_big_int a in
Number.ConstInt (Number.int_const_dec s)
| _ -> assert false
let eval_add ls l =
match l with
| [t1;t2] ->
begin
match t1.t_node, t2.t_node with
| Tconst c1, Tconst c2 -> t_const (add_const c1 c2)
| _ -> t_app_infer ls [t1;t2]
end
| _ -> assert false
let built_in_theories =
[ ["int"],"Int",
["infix +", eval_add]
]
let add_builtin_th env (l,n,d) =
try
let th = Env.find_theory env l n in
List.iter
(fun (id,f) ->
let ls = Theory.ns_find_ls th.Theory.th_export [id] in
Hls.add builtins ls f)
d
with Not_found -> ()
let get_builtins env =
Hls.add builtins ps_equ eval_equ;
List.iter (add_builtin_th env) built_in_theories
let rec matching env t p =
match p.pat_node,t.t_node with
| Pwild, _ -> env
......@@ -41,44 +74,44 @@ let rec matching env t p =
| Pas _, _ -> raise Undetermined
let rec eval_term menv env t =
let rec eval_term km menv env t =
match t.t_node with
| Tvar x ->
begin try Mvs.find x env
with Not_found -> t
end
| Tbinop(Tand,t1,t2) ->
t_and_simp (eval_term menv env t1) (eval_term menv env t2)
t_and_simp (eval_term km menv env t1) (eval_term km menv env t2)
| Tbinop(Tor,t1,t2) ->
t_or_simp (eval_term menv env t1) (eval_term menv env t2)
t_or_simp (eval_term km menv env t1) (eval_term km menv env t2)
| Tbinop(Timplies,t1,t2) ->
t_implies_simp (eval_term menv env t1) (eval_term menv env t2)
t_implies_simp (eval_term km menv env t1) (eval_term km menv env t2)
| Tbinop(Tiff,t1,t2) ->
t_iff_simp (eval_term menv env t1) (eval_term menv env t2)
| Tnot t1 -> t_not_simp (eval_term menv env t1)
t_iff_simp (eval_term km menv env t1) (eval_term km menv env t2)
| Tnot t1 -> t_not_simp (eval_term km menv env t1)
| Tapp(ls,tl) ->
eval_app ls (List.map (eval_term menv env) tl) t.t_ty
eval_app km menv env ls (List.map (eval_term km menv env) tl) t.t_ty
| Tif(t1,t2,t3) ->
let u = eval_term menv env t1 in
let u = eval_term km menv env t1 in
begin match u.t_node with
| Ttrue -> eval_term menv env t2
| Tfalse -> eval_term menv env t3
| Ttrue -> eval_term km menv env t2
| Tfalse -> eval_term km menv env t3
| _ -> t_if u t2 t3
end
| Tlet(t1,tb) ->
let u = eval_term menv env t1 in
let u = eval_term km menv env t1 in
let v,t2 = t_open_bound tb in
eval_term menv (Mvs.add v u env) t2
eval_term km menv (Mvs.add v u env) t2
| Tcase(t1,tbl) ->
let u = eval_term menv env t1 in
eval_match menv env u tbl
let u = eval_term km menv env t1 in
eval_match km menv env u tbl
| Tquant _
| Teps _
| Tconst _
| Ttrue
| Tfalse -> t
and eval_match menv env u tbl =
and eval_match km menv env u tbl =
let rec iter tbl =
match tbl with
| [] ->
......@@ -88,7 +121,40 @@ and eval_match menv env u tbl =
let p,t = t_open_branch b in
try
let env' = matching env u p in
eval_term menv env' t
eval_term km menv env' t
with NoMatch -> iter rem
in
try iter tbl with Undetermined -> t_case u tbl
and eval_app km menv env ls tl ty =
try
let f = Hls.find builtins ls in
f ls tl
with Not_found ->
match
try
Decl.find_logic_definition km ls
with Not_found ->
Format.eprintf "lsymbol %s not found in term evaluation@."
ls.ls_name.Ident.id_string;
exit 2
with
| None ->
begin try
t_app ls tl ty
with e ->
Format.eprintf "@[<hov 2>Exception during term evaluation (t_app %s):@ %a@]@."
ls.ls_name.Ident.id_string
Exn_printer.exn_printer e;
exit 2
end
| Some d ->
let l,t = Decl.open_ls_defn d in
let env' = List.fold_right2 Mvs.add l tl env in
eval_term km menv env' t
let eval_term env km t =
get_builtins env;
eval_term km Mvs.empty Mvs.empty t
......@@ -41,7 +41,17 @@ theory T
use import list.Append
constant l5 : int = match (Cons 5 Nil) ++ Nil with Nil -> 1 | Cons _ _ -> 2 end
constant l5 : list 'a = Nil ++ Nil
constant l5a : list int = (Nil : list int) ++ Nil
constant l5b : list int = Nil ++ (Nil : list int)
constant l5c : list int = (Cons 5 Nil) ++ Nil (* plante ! *)
constant l6a : int = match (Nil : list int) ++ Nil with Nil -> 1 | Cons _ _ -> 2 end
constant l6b : int = match (Cons 5 Nil) ++ Nil with Nil -> 1 | Cons _ _ -> 2 end (* plante ! *)
end
\ No newline at end of file
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