Commit a3724954 authored by Frontull Samuel's avatar Frontull Samuel
Browse files

fixed combine for nested lambdas

parent 8b5b34b0
......@@ -220,9 +220,9 @@ let rec _trs_term_to_string term pp =
else if pp then l ^ "[" ^ String.concat "," (L.map fun_lp fvs) ^ "]"
else l ^ "[" ^ String.concat "," (L.map fun_l fvs) ^ "]"
let trs_term_to_string term = _trs_term_to_string term false
let trs_term_to_string term = _trs_term_to_string term true
let trs_term_to_string_nopos term = _trs_term_to_string term true
let trs_term_to_string_nopos term = _trs_term_to_string term false
let term_print term = Printf.printf "%s" (trs_term_to_string term)
......@@ -308,7 +308,7 @@ type trs = TRS of trs_rule list * trs_term
let trs_to_string trs =
match trs with
| TRS (xs, t) ->
"TRS:\n" ^ rules_to_string xs ^ ".\n----\n" ^ trs_term_to_string t
"TRS:\n" ^ rules_to_string xs ^ ".\n----\n" ^ trs_term_to_string_nopos t
let trs_rules = function TRS (xs, _) -> xs
......@@ -339,6 +339,21 @@ let rec _redexpos trsterm pos =
let redexpos trsterm = _redexpos trsterm _ROOT
let rec combine a b =
match a,b with
| TVar _, _ -> [(a,b)]
| TDes (a1, a2), TDes (b1, b2) ->
combine a1 b1 @ combine a2 b2
| TCon (_, a1), TCon (_, b1) ->
L.flatten (L.map (fun x -> combine (fst x) (snd x)) (L.combine (L.map fst a1) (L.map fst b1)))
| _, _ -> failwith("combine not same structure.")
let rec combine_fvs fvs_r fvs =
match fvs_r, fvs with
| t :: ts, f :: fs -> combine t f @ combine_fvs ts fs
| [], [] -> []
| _, _ -> failwith("combine_fvs not same length.")
let rec search_pairs v f = function
| (x, n) :: xs -> if f v = f x then n else search_pairs v f xs
| [] -> v
......@@ -353,7 +368,8 @@ let rec rewrite trsrules trsterm =
match (trsrules, trsterm) with
| RR (TDes (TCon (l, fvs), TVar x), r) :: xs, TDes (TCon (l2, fvs2), arg) ->
if l = l2 then
subst r ((TVar x, arg) :: L.combine (L.map fst fvs) (L.map fst fvs2))
(* subst r ((TVar x, arg) :: L.combine (L.map fst fvs) (L.map fst fvs2)) *)
subst r ((TVar x, arg) :: combine_fvs (L.map fst fvs) (L.map fst fvs2))
else rewrite xs trsterm
| [], _ -> trsterm
| _, _ -> failwith "Not a rule or not a trsterm."
......@@ -405,7 +421,7 @@ let rec trs_to_term trs =
let rr = trs_rule xs l in
match rr with
| RR (TDes (TCon (_, fvs_r), var), r) ->
if L.mem var (L.map fst fvs) then
(* if L.mem var (L.map fst fvs) then
let f = next_fresh_2 () in
let rfresh = subst r [ (var, TVar f) ] in
LLam
......@@ -416,14 +432,15 @@ let rec trs_to_term trs =
( xs,
subst rfresh
(L.combine (L.map fst fvs_r) (L.map fst fvs)) )) )
else
else *)
LLam
( l,
vtname var,
trs_to_term
(TRS
( xs,
subst r (L.combine (L.map fst fvs_r) (L.map fst fvs))
(* subst r (L.combine (L.map fst fvs_r) (L.map fst fvs)) *)
subst r (combine_fvs (L.map fst fvs_r) (L.map fst fvs))
)) )
| _ -> failwith "Not a RR found." ) )
......
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