Commit ece63468 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

trans compute: typing bug debugging in progress

parent c686e51b
......@@ -461,6 +461,8 @@ 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 t = t_ty_subst type_subst Mvs.empty t in
let sigma =
try
List.fold_right2 Mvs.add l args Mvs.empty
......@@ -474,6 +476,17 @@ and reduce_app engine st ls ty rem_cont =
begin
try
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 "subst of rhs: ";
Ty.Mtv.iter
(fun tv ty -> Format.eprintf "%a -> %a,"
Pretty.print_tv tv Pretty.print_ty ty)
type_subst;
Format.eprintf "@.";
let rhs = t_ty_subst type_subst Mvs.empty rhs in
let sigma =
Mvs.map (t_ty_subst type_subst Mvs.empty) sigma
in
{ value_stack = rem_st;
cont_stack = Keval(rhs,sigma) :: rem_cont;
}
......@@ -522,8 +535,6 @@ and reduce_app engine st ls ty rem_cont =
(* TODO *)
let rec many_steps engine c n =
match c.value_stack, c.cont_stack with
| [Term t], [] -> t
......@@ -585,5 +596,5 @@ let add_rule t e =
try Mls.find ls e.rules
with Not_found -> []
in
{e with rules =
{e with rules =
Mls.add ls ((vars,args,r)::rules) e.rules}
......@@ -42,7 +42,7 @@ theory TestList
constant l1 : list int = Cons 12 (Cons 34 (Cons 56 Nil))
goal g1: match l1 with Nil -> 0 | Cons x y -> x end = 12
goal g1: match l1 with Nil -> 0 | Cons x _ -> x end = 12
use import list.Length
......@@ -55,8 +55,6 @@ theory TestList
goal g3: hd l1 = 12
(* typing bug
use import list.Append
constant l2 : list int =
......@@ -66,7 +64,6 @@ theory TestList
goal h2: length l2 = 5
*)
end
......
......@@ -3,43 +3,43 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../test_compute.why" expanded="true">
<theory name="T" expanded="true">
<goal name="g1" sum="1ad4ea691c2d3b0a420f5b0819ebc531" expanded="true">
<transf name="compute_in_goal" expanded="true">
<theory name="T">
<goal name="g1" sum="1ad4ea691c2d3b0a420f5b0819ebc531">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="g2" sum="ff207d8c26146a3871613afb3a9ac891" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g2" sum="ff207d8c26146a3871613afb3a9ac891">
<transf name="compute_in_goal">
<goal name="g2.1" expl="1." sum="c42af3c02ebf5e859a4dcf65db69d973">
</goal>
</transf>
</goal>
<goal name="g3" sum="059bfb681820ff98c7d4f1682433c247" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g3" sum="059bfb681820ff98c7d4f1682433c247">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="g10" sum="4c10af77fca7fb45f92d4e4181fcc80a" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g10" sum="4c10af77fca7fb45f92d4e4181fcc80a">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="g11" sum="4d359e703e593ef835a349322d923668" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g11" sum="4d359e703e593ef835a349322d923668">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="h1" sum="5d9ea52d9f6b9033794f44b5aa590306" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="h1" sum="5d9ea52d9f6b9033794f44b5aa590306">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="i1" sum="dfe815a019525fce8a2b755ff30f708a" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="i1" sum="dfe815a019525fce8a2b755ff30f708a">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="i2" sum="28f0e4a6c637d7af3829655f5173f1e7" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="i2" sum="28f0e4a6c637d7af3829655f5173f1e7">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="j1" sum="89e081884a488d0109ef1938861ab614" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="j1" sum="89e081884a488d0109ef1938861ab614">
<transf name="compute_in_goal">
</transf>
</goal>
</theory>
......@@ -53,8 +53,6 @@
</transf>
</goal>
<goal name="g3" sum="f1e9a9ae39f7d5c63ce17202d5b6a04f" expanded="true">
<transf name="compute_in_goal" expanded="true">
</transf>
</goal>
</theory>
<theory name="Rstandard" 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