Commit 3c0924af authored by MARCHE Claude's avatar MARCHE Claude
Browse files

More tests on term evaluation

parent a516b45e
......@@ -527,7 +527,7 @@ let do_theory env drv fname tname th glist elist =
match l with
| [] ->
let t = Mlw_interp.eval_term Term.Mvs.empty Term.Mvs.empty t in
printf "Evaluation of %s: %a@." x Pretty.print_term t
printf "@[<hov 2>Evaluation of %s:@ %a@]@." x Pretty.print_term t
| _ ->
eprintf "Symbol '%s' is not a constant in theory '%s'.@." x tname;
exit 1
......
open Term
let eval_app ls tl =
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_infer ls tl
t_app ls tl ty
(* TODO later
begin match t1.t_node,t2.t_node with
| Ttrue, Tfalse | Tfalse, Ttrue -> t_false
......@@ -15,7 +15,13 @@ let eval_app ls tl =
| _ -> assert false
else
(* TODO : if has_definition ls then ... *)
t_app_infer ls tl
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
let rec eval_term menv env t =
match t.t_node with
......@@ -33,7 +39,7 @@ let rec eval_term menv env t =
t_iff_simp (eval_term menv env t1) (eval_term menv env t2)
| Tnot t1 -> t_not_simp (eval_term menv env t1)
| Tapp(ls,tl) ->
eval_app ls (List.map (eval_term menv env) tl)
eval_app ls (List.map (eval_term menv env) tl) t.t_ty
| Tif(t1,t2,t3) ->
let u = eval_term menv env t1 in
begin match u.t_node with
......
......@@ -10,4 +10,16 @@ theory T
constant c3 : int = if true /\ false then 1 else 2
constant c4 : int = if 2 = 2 then 1 else 2
constant c5 : int = if 2 = 3 then 1 else 2
constant c6 : int = 2+2
use import list.List
constant l1 : list int = Cons 5 Nil
constant l2 : int = match Cons 5 Nil with Nil -> 1 | Cons _ _ -> 2 end
end
\ No newline at end of file
Supports Markdown
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