Commit 5bce105a authored by MARCHE Claude's avatar MARCHE Claude

trans compute: decide constructor equality

parent 7e68d0c3
......@@ -27,9 +27,15 @@ let const_equality c1 c2 =
BigInt.eq (Number.compute_int i1) (Number.compute_int i2)
| _ -> raise Undetermined
let value_equality t1 t2 =
let rec value_equality t1 t2 =
match (t1.t_node,t2.t_node) with
| Tconst c1, Tconst c2 -> const_equality c1 c2
| Tapp(ls1,_), Tapp(ls2,_) when not (ls_equal ls1 ls2) ->
if ls1.ls_constr > 0 && ls2.ls_constr > 0 then false else
raise Undetermined
| Tapp(ls1,tl1), Tapp(ls2,tl2) when ls_equal ls1 ls2 ->
if List.for_all2 value_equality tl1 tl2 then true else
raise Undetermined
| _ -> raise Undetermined
let to_bool b = if b then t_true else t_false
......@@ -381,6 +387,7 @@ and reduce_match st u tbl sigma cont =
let p,t = t_open_branch b in
try
let (mt',mv') = matching (Ty.Mtv.empty,sigma) u p in
(*
Format.eprintf "Pattern-matching succeeded:@\nmt' = @[";
Ty.Mtv.iter
(fun tv ty -> Format.eprintf "%a -> %a,"
......@@ -394,7 +401,9 @@ and reduce_match st u tbl sigma cont =
mv';
Format.eprintf "@]@.";
Format.eprintf "branch before inst: %a@." Pretty.print_term t;
*)
let mv'',t = t_subst_types mt' mv' t in
(*
Format.eprintf "branch after types inst: %a@." Pretty.print_term t;
Format.eprintf "mv'' = @[";
Mvs.iter
......@@ -402,6 +411,7 @@ and reduce_match st u tbl sigma cont =
Pretty.print_vs v Pretty.print_term t)
mv'';
Format.eprintf "@]@.";
*)
{ value_stack = st;
cont_stack = Keval(t,mv'') :: cont;
}
......
......@@ -52,7 +52,7 @@
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="g3" sum="f1e9a9ae39f7d5c63ce17202d5b6a04f" expanded="true">
<goal name="g3" sum="f1e9a9ae39f7d5c63ce17202d5b6a04f">
<transf name="compute_in_goal">
</transf>
</goal>
......@@ -62,8 +62,8 @@
</goal>
</transf>
</goal>
<goal name="h2" sum="23bc457ed3671d19bf68aacaceb560ac" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="h2" sum="23bc457ed3671d19bf68aacaceb560ac">
<transf name="compute_in_goal">
</transf>
</goal>
</theory>
......@@ -115,23 +115,35 @@
</transf>
</goal>
</theory>
<theory name="Rgroup">
<goal name="g0" sum="1e4b57ee823bf83fde917bdd0b03d14a">
<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">
<goal name="g01" sum="0a7faedd8825702fce72f3e84ec82571" expanded="true">
<transf name="compute_in_goal" expanded="true">
</transf>
</goal>
<goal name="g1" sum="825053ebfb5449346b8ed12490cc9354">
<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">
<goal name="g2" sum="76634810995226e5b7def51a0259205b" expanded="true">
<transf name="compute_in_goal" expanded="true">
</transf>
</goal>
</theory>
<theory name="Rinteger" expanded="true">
<goal name="l1" sum="9d62555b2a847e0ba9a9e9199cbf2c38" expanded="true">
</goal>
</theory>
<theory name="TestInteger">
<goal name="g1" sum="dab58bcd2a433e50f94afd9cd1659810">
<transf name="compute_in_goal">
<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>
......@@ -148,33 +160,33 @@
<theory name="MoreSets" expanded="true">
</theory>
<theory name="TestSets" expanded="true">
<goal name="g00" sum="f038e056e11482d4fcfb897f4952d3e4" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g00" sum="f038e056e11482d4fcfb897f4952d3e4">
<transf name="compute_in_goal">
<goal name="g00.1" expl="1." sum="d41e69e131353b6c9f0b213b7cea5c12">
</goal>
</transf>
</goal>
<goal name="g01" sum="7177ee4dcc6665dea602aced3271f562" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g01.1" expl="1." sum="70eeef8e11e94a8fc0fcf899903c1a7c">
<goal name="g01" sum="7177ee4dcc6665dea602aced3271f562">
<transf name="compute_in_goal">
<goal name="g01.1" expl="1." sum="d41e69e131353b6c9f0b213b7cea5c12">
</goal>
</transf>
</goal>
<goal name="g015" sum="bb4d9978c3fa326961606408c9cc9cd5" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g015.1" expl="1." sum="70eeef8e11e94a8fc0fcf899903c1a7c">
<goal name="g015" sum="bb4d9978c3fa326961606408c9cc9cd5">
<transf name="compute_in_goal">
<goal name="g015.1" expl="1." sum="d41e69e131353b6c9f0b213b7cea5c12">
</goal>
</transf>
</goal>
<goal name="g02" sum="bf942bd01c45cd6931b03788e6d9065e" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g02.1" expl="1." sum="18a068220afd8e096c3bd95010d499ad">
<goal name="g02" sum="bf942bd01c45cd6931b03788e6d9065e">
<transf name="compute_in_goal">
<goal name="g02.1" expl="1." sum="d41e69e131353b6c9f0b213b7cea5c12">
</goal>
</transf>
</goal>
<goal name="g025" sum="396190e131bb8f99956a2f2a7d61e075" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g025.1" expl="1." sum="18a068220afd8e096c3bd95010d499ad">
<goal name="g025" sum="396190e131bb8f99956a2f2a7d61e075">
<transf name="compute_in_goal">
<goal name="g025.1" expl="1." sum="d41e69e131353b6c9f0b213b7cea5c12">
</goal>
</transf>
</goal>
......
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