Commit 048f4034 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

fix the inlining transformations

parent a7720a18
......@@ -13,9 +13,7 @@ fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
(* À discuter *)
transformation "simplify_recursive_definition"
(*
transformation "inline_trivial"
*)
transformation "eliminate_builtin"
transformation "eliminate_mutual_recursion"
......
......@@ -10,9 +10,7 @@ valid 0
unknown "no contradiction was found" "some enclosures were not satisfied"
transformation "simplify_recursive_definition"
(*
transformation "inline_trivial"
*)
transformation "eliminate_builtin"
transformation "eliminate_inductive"
......
......@@ -43,9 +43,11 @@ let rec replacet env t =
| Tapp (fs,tl) ->
begin try
let (vs,t) = Mls.find fs env.fs in
let m = List.fold_left2 (fun acc x y -> Mvs.add x y acc)
Mvs.empty vs tl in
t_subst m t
let add (mt,mv) x y =
(Ty.ty_match mt x.vs_ty y.t_ty, Mvs.add x y mv)
in
let (mt,mv) = List.fold_left2 add (Ty.Mtv.empty, Mvs.empty) vs tl in
t_ty_subst mt mv t
with Not_found -> t end
| _ -> t
......@@ -55,9 +57,11 @@ and replacep env f =
| Fapp (ps,tl) ->
begin try
let (vs,f) = Mls.find ps env.ps in
let m = List.fold_left2 (fun acc x y -> Mvs.add x y acc)
Mvs.empty vs tl in
f_subst m f
let add (mt,mv) x y =
(Ty.ty_match mt x.vs_ty y.t_ty, Mvs.add x y mv)
in
let (mt,mv) = List.fold_left2 add (Ty.Mtv.empty, Mvs.empty) vs tl in
f_ty_subst mt mv f
with Not_found -> f end
| _ -> f
......
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