Commit 781293a9 authored by Frontull Samuel's avatar Frontull Samuel
Browse files

no fresh labels and all_var contraint when search for rule

parent 6149907e
......@@ -90,12 +90,6 @@ let rec default_names_r term pos =
let default_names term = default_names_r term "e"
let rec default_labels term =
match term with
| LVar v -> LVar v
| LLam (_, fvs, v, t) -> LLam (next_label (), fvs, v, default_labels t)
| LApp (e1, e2) -> LApp (default_labels e1, default_labels e2)
(** Extract the name of a variable from a {e a_term} *)
let lvname = function LVar n -> n | _ -> ""
......@@ -111,6 +105,51 @@ let next_fresh () =
counter := !counter + 1;
"p_" ^ string_of_int !counter
let rec replace_label lterm l n =
match lterm with
| LVar _ -> lterm
| LLam (lo, fvs, v, t) ->
let rt = replace_label t l n in
let fvst = L.map (fun fvt -> replace_label fvt l n) fvs in
if lo = l then LLam (n, fvst, v, replace_label rt l n)
else LLam (lo, fvst, v, replace_label rt l n)
| LApp (e1, e2) -> LApp (replace_label e1 l n, replace_label e2 l n)
let uniq_cons x xs = if List.mem x xs then xs else x :: xs
let remove_from_right xs = List.fold_right uniq_cons xs []
let rec _l_term_labels lterm =
match lterm with
| LVar _ -> []
| LLam (l, fvs, _, t) ->
(l :: L.flatten (L.map _l_term_labels fvs)) @ _l_term_labels t
| LApp (e1, e2) -> _l_term_labels e1 @ _l_term_labels e2
let l_term_labels term = remove_from_right (_l_term_labels term)
let new_label_pairs labels = L.map (fun x -> (x, next_label ())) labels
let id x = x
let rec search_pairs v f = function
| (x, n) :: xs -> if f v = f x then n else search_pairs v f xs
| [] -> v
let rec _assign_labels term pairs =
match term with
| LVar v -> LVar v
| LLam (l, fvs, v, t) ->
(* let lf = search_pairs l id pairs in *)
let lf = next_label () in
let rt = replace_label t l lf in
let fvst = L.map (fun x -> _assign_labels x pairs) fvs in
LLam (lf, fvst, v, _assign_labels rt pairs)
| LApp (e1, e2) -> LApp (_assign_labels e1 pairs, _assign_labels e2 pairs)
let fresh_labels term =
_assign_labels term (new_label_pairs (l_term_labels term))
(** replace every var occurrence by fresh var *)
let rec subst m x y =
match m with
......@@ -234,14 +273,10 @@ let rec _redexpos trsterm pos =
let redexpos trsterm = _redexpos trsterm ""
let rec search_pairs v = function
| (x, n) :: xs -> if vtname v = vtname x then n else search_pairs v xs
| [] -> v
let rec subst m pairs =
(* Printf.printf "subst\n"; *)
match m with
| TVar _ -> search_pairs m pairs
| TVar _ -> search_pairs m vtname pairs
| TCon (l, fvs) -> TCon (l, L.map (fun z -> subst z pairs) fvs)
| TDes (e1, e2) -> TDes (subst e1 pairs, subst e2 pairs)
......@@ -269,12 +304,12 @@ let rec all_vars vs =
(* project : TRS -> term *)
let rec trs_rule trsrules label =
(* Printf.printf "trs_rule %s\n" label;
Printf.printf "trs_rules %s\n"
(* Printf.printf "---\ntrs_rule %s\n" label;
Printf.printf "trs_rules:\n %s\n---\n"
(String.concat "\n" (L.map trs_rule_to_string trsrules)); *)
match trsrules with
| RR (TDes (TCon (l, _), _), _) :: xs ->
if l = label then L.hd trsrules else trs_rule xs label
| RR (TDes (TCon (l, fvs), _), _) :: xs ->
if l = label && all_vars fvs then L.hd trsrules else trs_rule xs label
| _ :: xs -> trs_rule xs label
| [] -> failwith "No rule with such label."
......@@ -369,7 +404,8 @@ let reduction_print term =
(String.concat "\n"
(L.mapi
(fun i (a_term, b_trs) ->
let a_term_default = default_labels a_term in
(* let a_term_default = fresh_labels a_term in *)
let a_term_default = a_term in
let a_term_trs = l_term_to_trs a_term_default in
let b_trs_term = trs_to_term b_trs in
(* let b_term_trs = l_term_to_trs b_trs_term in *)
......
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