Commit 0e6b3e63 authored by MARCHE Claude's avatar MARCHE Claude

transf compute: analysis the typing bug

parent e29e3119
......@@ -99,6 +99,11 @@ val ty_s_any : (tysymbol -> bool) -> ty -> bool
exception TypeMismatch of ty * ty
val ty_match : ty Mtv.t -> ty -> ty -> ty Mtv.t
(** [ty_match sigma0 pat sub] returns a type substitution [sigma] such
that [sigma pat = sub]. Raises TypeMismatch if no substitution
exists.
*)
val ty_inst : ty Mtv.t -> ty -> ty
val ty_freevars : Stv.t -> ty -> Stv.t
val ty_closed : ty -> bool
......
......@@ -9,17 +9,8 @@
(* *)
(********************************************************************)
open Term
(* {2 builtin symbols} *)
let builtins = Hls.create 17
......@@ -409,7 +400,9 @@ and reduce_eval st t sigma rem =
{ value_stack = Term t :: st ;
cont_stack = rem;
}
with Not_found -> assert false
with Not_found ->
Format.eprintf "Tvar not found: %a@." Pretty.print_vs v;
assert false
end
| Tif(t1,t2,t3) ->
{ value_stack = st;
......@@ -475,7 +468,7 @@ and reduce_app engine st ls ty rem_cont =
(* regular definition *)
let d = List.assq ls dl in
let l,t = Decl.open_ls_defn d in
let type_subst = Ty.oty_match Ty.Mtv.empty ty t.t_ty in
let type_subst = Ty.oty_match Ty.Mtv.empty t.t_ty ty in
let t = t_ty_subst type_subst Mvs.empty t in
let sigma =
try
......@@ -489,8 +482,19 @@ and reduce_app engine st ls ty rem_cont =
(* try a rewrite rule *)
begin
try
Format.eprintf "try a rewrite rule on %a@." Pretty.print_ls ls;
let sigma,rhs = one_step_reduce engine ls args in
let type_subst = Ty.oty_match Ty.Mtv.empty ty rhs.t_ty in
Format.eprintf "rhs = %a@." Pretty.print_term rhs;
Format.eprintf "sigma = ";
Mvs.iter
(fun v t -> Format.eprintf "%a -> %a,"
Pretty.print_vs v Pretty.print_term t)
sigma;
Format.eprintf "@.";
Format.eprintf "try a type match: %a and %a@."
(Pp.print_option Pretty.print_ty) ty
(Pp.print_option Pretty.print_ty) rhs.t_ty;
let type_subst = Ty.oty_match Ty.Mtv.empty rhs.t_ty ty in
Format.eprintf "subst of rhs: ";
Ty.Mtv.iter
(fun tv ty -> Format.eprintf "%a -> %a,"
......@@ -501,6 +505,13 @@ and reduce_app engine st ls ty rem_cont =
let sigma =
Mvs.map (t_ty_subst type_subst Mvs.empty) sigma
in
Format.eprintf "rhs = %a@." Pretty.print_term rhs;
Format.eprintf "sigma = ";
Mvs.iter
(fun v t -> Format.eprintf "%a -> %a,"
Pretty.print_vs v Pretty.print_term t)
sigma;
Format.eprintf "@.";
{ value_stack = rem_st;
cont_stack = Keval(rhs,sigma) :: rem_cont;
}
......@@ -598,8 +609,6 @@ let extract_rule t =
end
| _ -> raise
(NotARewriteRule "rule should be of the form forall ... t1 = t2 or f1 <-> f2")
in
aux Svs.empty t
......
......@@ -44,7 +44,7 @@
</goal>
</theory>
<theory name="TestList" expanded="true">
<goal name="g1" sum="f55bdd48b7c84d63db3d500485f0d1f5" expanded="true">
<goal name="g1" sum="0ddd0eeb3a391ca74d03f68832a092a6" expanded="true">
<transf name="compute_in_goal" expanded="true">
</transf>
</goal>
......@@ -54,6 +54,10 @@
</goal>
<goal name="g3" sum="f1e9a9ae39f7d5c63ce17202d5b6a04f" expanded="true">
</goal>
<goal name="h1" sum="e2022f7025813c0922b8d8d9143180b9" expanded="true">
</goal>
<goal name="h2" sum="23bc457ed3671d19bf68aacaceb560ac" expanded="true">
</goal>
</theory>
<theory name="Rstandard" expanded="true">
</theory>
......@@ -105,28 +109,12 @@
</theory>
<theory name="Rgroup" expanded="true">
<goal name="g0" sum="1e4b57ee823bf83fde917bdd0b03d14a" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g0.1" expl="1." sum="143d0d6addcac455f08acfb659827668">
</goal>
</transf>
</goal>
<goal name="g01" sum="0a7faedd8825702fce72f3e84ec82571" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g01.1" expl="1." sum="a66352ac30125db23e59fdc4823816b6">
</goal>
</transf>
</goal>
<goal name="g1" sum="825053ebfb5449346b8ed12490cc9354" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g1.1" expl="1." sum="992aa1eb1a8bf3883d4100848222a45e">
</goal>
</transf>
</goal>
<goal name="g2" sum="76634810995226e5b7def51a0259205b" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g2.1" expl="1." sum="061d6069cfc72329b2dacb4392f050c9">
</goal>
</transf>
</goal>
</theory>
<theory name="Rinteger" expanded="true">
......@@ -135,18 +123,10 @@
</theory>
<theory name="TestInteger" expanded="true">
<goal name="g1" sum="dab58bcd2a433e50f94afd9cd1659810" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g1.1" expl="1." sum="4c4937d701abd0d106d51fa154f0e03c">
</goal>
</transf>
</goal>
<goal name="g2" sum="58217b4a5d78d925ea3cf1a798093f35" expanded="true">
<transf name="compute_in_goal" expanded="true">
</transf>
</goal>
<goal name="g3" sum="3dcaf92c24507ef6b9d45c146cfeffa1" expanded="true">
<transf name="compute_in_goal" expanded="true">
</transf>
</goal>
</theory>
<theory name="MoreSets" expanded="true">
......
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