Commit 7e68d0c3 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

trans compute: typing bug seems to be fixed, as last.

parent 33ececbc
......@@ -1015,12 +1015,16 @@ let t_s_map fnT fnL t = t_gen_map fnT fnL (gen_mapV fnT (t_vars t)) t
(* simultaneous substitution into types and terms *)
let t_ty_subst mapT mapV t =
let t_subst_types mapT mapV t =
let fnT = ty_inst mapT in
let m = gen_mapV fnT (t_vars t) in
let t = t_gen_map fnT (fun ls -> ls) m t in
let add _ v t m = vs_check v t; Mvs.add v t m in
let m = Mvs.fold2_inter add m mapV Mvs.empty in
(m,t)
let t_ty_subst mapT mapV t =
let m,t = t_subst_types mapT mapV t in
t_subst_unsafe m t
(* fold over symbols *)
......
......@@ -396,6 +396,10 @@ val t_ty_subst : ty Mtv.t -> term Mvs.t -> term -> term
(** [t_ty_subst mt mv t] substitutes simultaneously type variables by
mapping [mt] and term variables by mapping [mv] in term [t] *)
val t_subst_types : ty Mtv.t -> term Mvs.t -> term -> term Mvs.t * term
(** [t_subst_types mt mv t] substitutes type variables by
mapping [mt] simultaneously in substitution [mv] and in term [t] *)
(** {2 Find free variables and type variables} *)
val t_closed : term -> bool
......
......@@ -223,8 +223,8 @@ type config = {
exception NoMatch
let first_order_matching (vars : Svs.t) (largs : term list)
(args : term list) : substitution =
let rec loop sigma largs args =
(args : term list) : Ty.ty Ty.Mtv.t * substitution =
let rec loop ((mt,mv) as sigma) largs args =
match largs,args with
| [],[] -> sigma
| t1::r1, t2::r2 ->
......@@ -236,13 +236,14 @@ let first_order_matching (vars : Svs.t) (largs : term list)
match t1.t_node with
| Tvar vs when Svs.mem vs vars ->
begin
try let t = Mvs.find vs sigma in
try let t = Mvs.find vs mv in
if t_equal t t2 then
loop sigma r1 r2
else
raise NoMatch
with Not_found ->
loop (Mvs.add vs t2 sigma) r1 r2
loop (Ty.ty_match mt vs.vs_ty (t_type t2),
Mvs.add vs t2 mv) r1 r2
end
| Tapp(ls1,args1) ->
begin
......@@ -273,7 +274,7 @@ let first_order_matching (vars : Svs.t) (largs : term list)
end
| _ -> raise NoMatch
in
loop Mvs.empty largs args
loop (Ty.Mtv.empty, Mvs.empty) largs args
exception Irreducible
......@@ -295,16 +296,16 @@ let one_step_reduce engine ls args =
with Not_found ->
raise Irreducible
let rec matching sigma t p =
let rec matching ((mt,mv) as sigma) t p =
match p.pat_node with
| Pwild -> sigma
| Pvar v -> Mvs.add v t sigma
| Pvar v -> (mt,Mvs.add v t mv)
| Por(p1,p2) ->
begin
try matching sigma t p1
with NoMatch -> matching sigma t p2
end
| Pas(p,v) -> matching (Mvs.add v t sigma) t p
| Pas(p,v) -> matching (mt,Mvs.add v t mv) t p
| Papp(ls1,pl) ->
match t.t_node with
| Tapp(ls2,tl) ->
......@@ -379,14 +380,38 @@ and reduce_match st u tbl sigma cont =
| b::rem ->
let p,t = t_open_branch b in
try
let sigma' = matching sigma u p in
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,"
Pretty.print_tv tv Pretty.print_ty ty)
mt';
Format.eprintf "@]@\n";
Format.eprintf "mv' = @[";
Mvs.iter
(fun v t -> Format.eprintf "%a -> %a,"
Pretty.print_vs v Pretty.print_term t)
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
(fun v t -> Format.eprintf "%a -> %a,"
Pretty.print_vs v Pretty.print_term t)
mv'';
Format.eprintf "@]@.";
{ value_stack = st;
cont_stack = Keval(t,sigma') :: cont;
cont_stack = Keval(t,mv'') :: cont;
}
with NoMatch -> iter rem
in
try iter tbl with Undetermined ->
{ value_stack = Term (t_case u tbl) :: st;
{ (* value_stack = Term (t_case u tbl) :: st; *)
(* FIXME: apply (t_subst sigma) on each branch of tbl !! *)
value_stack = Term (t_subst sigma (t_case u tbl)) :: st;
(* DONE? *)
cont_stack = cont;
}
......@@ -400,7 +425,7 @@ and reduce_eval st t sigma rem =
{ value_stack = Term t :: st ;
cont_stack = rem;
}
with Not_found ->
with Not_found ->
Format.eprintf "Tvar not found: %a@." Pretty.print_vs v;
assert false
end
......@@ -467,33 +492,37 @@ and reduce_app engine st ls ty rem_cont =
| Decl.Dlogic dl ->
(* 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 t.t_ty 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
with Invalid_argument _ -> assert false
let vl,e = Decl.open_ls_defn d in
let add (mt,mv) x y =
Ty.ty_match mt x.vs_ty (t_type y), Mvs.add x y mv
in
let (mt,mv) = List.fold_left2 add (Ty.Mtv.empty, Mvs.empty) vl args in
let mt = Ty.oty_match mt e.t_ty ty in
let mv,e = t_subst_types mt mv e in
{ value_stack = rem_st;
cont_stack = Keval(t,sigma) :: rem_cont;
cont_stack = Keval(e,mv) :: rem_cont;
}
| Decl.Dparam _ | Decl.Dind _ ->
(* 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 (mt,mv),rhs = one_step_reduce engine ls args 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;
(snd sigma);
Format.eprintf "@.";
Format.eprintf "try a type match: %a and %a@."
(Pp.print_option Pretty.print_ty) ty
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
......@@ -512,8 +541,10 @@ and reduce_app engine st ls ty rem_cont =
Pretty.print_vs v Pretty.print_term t)
sigma;
Format.eprintf "@.";
*)
let mv,rhs = t_subst_types mt mv rhs in
{ value_stack = rem_st;
cont_stack = Keval(rhs,sigma) :: rem_cont;
cont_stack = Keval(rhs,mv) :: rem_cont;
}
with Irreducible ->
raise Not_found
......@@ -569,7 +600,10 @@ let rec many_steps engine c n =
many_steps engine c (n-1)
let normalize engine t =
let c = { value_stack = []; cont_stack = [Keval(t,Mvs.empty)] } in
let c = { value_stack = [];
cont_stack = [Keval(t,Mvs.empty)] ;
}
in
many_steps engine c 1000
......
......@@ -3,13 +3,13 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<file name="../test_compute.why" expanded="true">
<theory name="T">
<theory name="T" expanded="true">
<goal name="g1" sum="1ad4ea691c2d3b0a420f5b0819ebc531">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="g2" sum="ff207d8c26146a3871613afb3a9ac891">
<transf name="compute_in_goal">
<goal name="g2" sum="ff207d8c26146a3871613afb3a9ac891" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g2.1" expl="1." sum="c42af3c02ebf5e859a4dcf65db69d973">
</goal>
</transf>
......@@ -44,89 +44,105 @@
</goal>
</theory>
<theory name="TestList" expanded="true">
<goal name="g1" sum="0ddd0eeb3a391ca74d03f68832a092a6" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g1" sum="0ddd0eeb3a391ca74d03f68832a092a6">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="g2" sum="ea853a23a637408ca6f2a1d4f21d0bf7" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g2" sum="ea853a23a637408ca6f2a1d4f21d0bf7">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="g3" sum="f1e9a9ae39f7d5c63ce17202d5b6a04f" expanded="true">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="h1" sum="e2022f7025813c0922b8d8d9143180b9" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="h1.1" expl="1." sum="b11b276809be46293ea8a713456fef9b">
</goal>
</transf>
</goal>
<goal name="h2" sum="23bc457ed3671d19bf68aacaceb560ac" expanded="true">
<transf name="compute_in_goal" expanded="true">
</transf>
</goal>
</theory>
<theory name="Rstandard" expanded="true">
</theory>
<theory name="TestStandard" expanded="true">
<goal name="g00" sum="0ceddda03e7e96cda00c67eebccb8ce2" expanded="true">
<transf name="compute_in_goal" expanded="true">
<theory name="TestStandard">
<goal name="g00" sum="0ceddda03e7e96cda00c67eebccb8ce2">
<transf name="compute_in_goal">
<goal name="g00.1" expl="1." sum="72e859206601f617bc9e8d202f1736c7">
</goal>
</transf>
</goal>
<goal name="g01" sum="033e36efdc75e7ebee7089bb79aae621" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g01" sum="033e36efdc75e7ebee7089bb79aae621">
<transf name="compute_in_goal">
<goal name="g01.1" expl="1." sum="d6d954e45cea3cfb507006372f300730">
</goal>
</transf>
</goal>
<goal name="g02" sum="e9fe9f1ccbd8b3e9306f10125f9884fe" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g02" sum="e9fe9f1ccbd8b3e9306f10125f9884fe">
<transf name="compute_in_goal">
<goal name="g02.1" expl="1." sum="bf81b44246d2030307c2cbbc6036407a">
</goal>
</transf>
</goal>
<goal name="g03" sum="0d4620924ddd3999e33c97573f5b78e0" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g03" sum="0d4620924ddd3999e33c97573f5b78e0">
<transf name="compute_in_goal">
<goal name="g03.1" expl="1." sum="4f95c487067aa0d0dee0ac82ede93e99">
</goal>
</transf>
</goal>
<goal name="g04" sum="e37cdc4814159dbd3887a5880f33246c" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g04" sum="e37cdc4814159dbd3887a5880f33246c">
<transf name="compute_in_goal">
<goal name="g04.1" expl="1." sum="15d82520ff40518ce3e75cf46bb5c135">
</goal>
</transf>
</goal>
<goal name="g05" sum="4e7c955211deed29770e221db4c89bca" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g05" sum="4e7c955211deed29770e221db4c89bca">
<transf name="compute_in_goal">
<goal name="g05.1" expl="1." sum="6f9cf28d8e4785900d38fff421f2260d">
</goal>
</transf>
</goal>
<goal name="g06" sum="447bada60ec36071cd53b698cbf73823" expanded="true">
<goal name="g06" sum="447bada60ec36071cd53b698cbf73823">
</goal>
<goal name="g07" sum="9f175ea63c4a17c0a01aadffe9cf5e9f" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="g07" sum="9f175ea63c4a17c0a01aadffe9cf5e9f">
<transf name="compute_in_goal">
<goal name="g07.1" expl="1." sum="ffa418ac5ab3f343a3554872c65c8bd9">
</goal>
</transf>
</goal>
</theory>
<theory name="Rgroup" expanded="true">
<goal name="g0" sum="1e4b57ee823bf83fde917bdd0b03d14a" expanded="true">
<theory name="Rgroup">
<goal name="g0" sum="1e4b57ee823bf83fde917bdd0b03d14a">
</goal>
<goal name="g01" sum="0a7faedd8825702fce72f3e84ec82571" expanded="true">
<goal name="g01" sum="0a7faedd8825702fce72f3e84ec82571">
</goal>
<goal name="g1" sum="825053ebfb5449346b8ed12490cc9354" expanded="true">
<goal name="g1" sum="825053ebfb5449346b8ed12490cc9354">
</goal>
<goal name="g2" sum="76634810995226e5b7def51a0259205b" expanded="true">
<goal name="g2" sum="76634810995226e5b7def51a0259205b">
</goal>
</theory>
<theory name="Rinteger" expanded="true">
<goal name="l1" sum="9d62555b2a847e0ba9a9e9199cbf2c38" expanded="true">
</goal>
</theory>
<theory name="TestInteger" expanded="true">
<goal name="g1" sum="dab58bcd2a433e50f94afd9cd1659810" expanded="true">
<theory name="TestInteger">
<goal name="g1" sum="dab58bcd2a433e50f94afd9cd1659810">
<transf name="compute_in_goal">
<goal name="g1.1" expl="1." sum="4c4937d701abd0d106d51fa154f0e03c">
</goal>
</transf>
</goal>
<goal name="g2" sum="58217b4a5d78d925ea3cf1a798093f35" expanded="true">
<goal name="g2" sum="58217b4a5d78d925ea3cf1a798093f35">
<transf name="compute_in_goal">
</transf>
</goal>
<goal name="g3" sum="3dcaf92c24507ef6b9d45c146cfeffa1" expanded="true">
<goal name="g3" sum="3dcaf92c24507ef6b9d45c146cfeffa1">
<transf name="compute_in_goal">
</transf>
</goal>
</theory>
<theory name="MoreSets" expanded="true">
......@@ -145,10 +161,22 @@
</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>
</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>
</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>
</transf>
</goal>
</theory>
</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