Commit 4c24b678 authored by Frontull Samuel's avatar Frontull Samuel
Browse files

minimal bound contexts replaced by fresh variables for rule creation

parent bb71d96a
......@@ -12,5 +12,18 @@ let () =
try str_to_term (Sys.argv.(1) ^ "\n") with _ -> failwith "Syntax error"
in
let lterm = Core.term_to_l_term term in
Printf.printf "%s\n%s" (Core.trs_term_to_string (Core.l_term_to_trsterm lterm))
(Core.rules_to_string (Core.rules lterm))
(* let tterm = Core.l_term_to_trsterm lterm in
let trs = Core.l_term_to_trs lterm in
let trs' = Core.rstep trs in
Printf.printf "%s\n" (Core._term_to_string term);
(* Printf.printf "redex @ %s\n" (Core.weak_redexpos lterm); *)
Printf.printf "===================\n\n";
Printf.printf "%s\n" (Core.trs_term_to_string tterm);
(* Printf.printf "redex @ %s\n" (Core.redexpos tterm); *)
Printf.printf "---------------------------------\n%s\n\n"
(Core.rules_to_string (Core.rules lterm));
Printf.printf "%s\n" (Core.trs_term_to_string (Core.trs_term trs'));
Printf.printf "%s\n"
(Core._term_to_string (Core.l_term_to_term (Core.trs_to_term trs'))); *)
Core.print_simulation lterm
......@@ -59,8 +59,7 @@ let uniq_cons x xs = if L.mem x xs then xs else x :: xs
let linear_list xs = L.fold_right uniq_cons xs []
let fvars term =
linear_list (_fvars term)
let fvars term = linear_list (_fvars term)
(* lift : term -> TRS *)
let rec term_to_l_term term =
......@@ -88,9 +87,9 @@ let rec rename_fv term x y =
let rec default_names_r term pos =
match term with
| LVar v -> LVar v
| LLam (l, fvs, v, t) ->
| LLam (l, _, v, t) ->
let vf = "x_" ^ pos in
LLam (l, fvs, vf, default_names_r (rename_fv t v vf) (pos ^ "0"))
LLam (l, [], vf, default_names_r (rename_fv t v vf) (pos ^ "0"))
| LApp (e1, e2) ->
LApp (default_names_r e1 (pos ^ "0"), default_names_r e2 (pos ^ "1"))
......@@ -130,7 +129,7 @@ let rec _casubst m x n fvn =
else
(* get intersection of fvn and fvs variable names *)
(* let fvs_vars = L.map lvname (L.flatten (L.map free_variables fvs)) in
let inters = List.filter (fun x -> List.mem x (y :: fvs_vars)) fvn in *)
let inters = List.filter (fun x -> List.mem x (y :: fvs_vars)) fvn in *)
let inters = List.filter (fun x -> x = y) fvn in
match inters with
| [] ->
......@@ -153,28 +152,30 @@ let beta term =
let rec _weak_redexpos term pos =
match term with
| LApp (LLam (_, _, _, _), _) -> pos
| LApp (LLam (_, _, _, _), _) -> if free_variables term = [] then pos else ""
| LApp (e1, e2) ->
let posl = _weak_redexpos e1 (pos ^ "1") in
if posl != "" then posl else _weak_redexpos e2 (pos ^ "2")
if posl <> "" then posl else _weak_redexpos e2 (pos ^ "2")
| LLam (_, _, _, e) -> _weak_redexpos e (pos ^ "1")
| _ -> ""
let weak_redexpos term = _weak_redexpos term ""
let weak_redexpos term = _weak_redexpos term "e"
let rec _weak_step term pos p =
match term with
| LApp (LLam (_, _, _, _), _) -> if p = pos then beta term else term
| LApp (e1, e2) ->
LApp (_weak_step e1 pos (p ^ "1"), _weak_step e2 pos (p ^ "2"))
| LLam (l, f, x, e) -> LLam (l, f, x, _weak_step e pos (p ^ "1"))
| _ -> term
let weak_step term = _weak_step term (weak_redexpos term) ""
let weak_step term = _weak_step term (weak_redexpos term) "e"
let weak_step_pos term pos = _weak_step term pos ""
let weak_step_pos term pos = _weak_step term pos "e"
type trs_term =
| TVar of string
| TCon of string * trs_term list
| TCon of string * (trs_term * string) list
| TDes of trs_term * trs_term
(** Extract the name of a variable from a {e a_term} *)
......@@ -183,63 +184,120 @@ let vtname = function TVar n -> n | _ -> ""
let rec trs_term_to_string term =
match term with
| TVar v -> v
| TDes (e1, e2) -> (
match (e1, e2) with
| TDes _, TDes _ ->
"(" ^ trs_term_to_string e1 ^ ") (" ^ trs_term_to_string e2 ^ ")"
| TDes _, _ -> " (" ^ trs_term_to_string e1 ^ ") " ^ trs_term_to_string e2
| _, TDes _ -> trs_term_to_string e1 ^ " (" ^ trs_term_to_string e2 ^ ")"
| _, _ -> trs_term_to_string e1 ^ " " ^ trs_term_to_string e2 )
| TCon (l, fvs) ->
l ^ "(" ^ String.concat "," (L.map trs_term_to_string fvs) ^ ")"
| TDes (e1, e2) ->
"@(" ^ trs_term_to_string e1 ^ ", " ^ trs_term_to_string e2 ^ ")"
if fvs = [] then l
else
l ^ "["
^ String.concat ","
(L.map
(fun x -> "(" ^ trs_term_to_string (fst x) ^ ")@" ^ snd x)
fvs)
^ "]"
let term_print term = Printf.printf "%s" (trs_term_to_string term)
let rec fvars_trsterm x trsterm =
let rec fvar_trsterm t =
match t with
| TVar _ -> [ t ]
| TDes (e1, e2) -> fvar_trsterm e1 @ fvar_trsterm e2
| TCon (_, fvs) -> L.flatten (L.map (fun x -> fvar_trsterm (fst x)) fvs)
let components_counter = ref 0
let next_fresh_component () =
components_counter := !components_counter + 1;
"v_" ^ string_of_int !components_counter
let rec _components_trsterm x pos trsterm =
match trsterm with
| TVar _ ->
if trsterm = TVar x then [] else [trsterm]
| TVar _ -> if trsterm = TVar x then [] else [ (trsterm, pos) ]
| TDes (e1, e2) ->
fvars_trsterm x e1 @ fvars_trsterm x e2
if fvar_trsterm trsterm = [] then [ (trsterm, pos) ]
else
_components_trsterm x (pos ^ "1") e1
@ _components_trsterm x (pos ^ "2") e2
| TCon (_, fvs) ->
if fvs = [] then [trsterm] else
L.flatten (L.map (fvars_trsterm x) fvs)
if fvs = [] then [ (trsterm, pos) ]
else
L.flatten
(L.map (fun y -> _components_trsterm x ("1" ^ snd y) (fst y)) fvs)
let components_trsterm x trsterm = _components_trsterm x "e" trsterm
let rec l_term_to_trsterm lterm =
match lterm with
| LVar x -> TVar x
| LApp (e1, e2) ->
TDes (l_term_to_trsterm e1, l_term_to_trsterm e2)
| LApp (e1, e2) -> TDes (l_term_to_trsterm e1, l_term_to_trsterm e2)
| LLam (l, _, x, e) ->
let e_t = l_term_to_trsterm e in
let fvs_t = fvars_trsterm x e_t in
let fvs_t = _components_trsterm x "1" e_t in
TCon (l, fvs_t)
let rec _components_lterm x pos lterm =
if free_variables lterm = [] then LVar ("v_" ^ pos)
else
match lterm with
| LVar y -> if y = x then lterm else LVar ("v_" ^ pos)
| LApp (e1, e2) ->
let e1' = _components_lterm x (pos ^ "1") e1 in
let e2' = _components_lterm x (pos ^ "2") e2 in
LApp (e1', e2')
| LLam (l, fvs, y, e) ->
let e' = _components_lterm x (pos ^ "1") e in
LLam (l, fvs, y, e')
let components_lterm x lterm = _components_lterm x "e" lterm
type trs_rule = RR of trs_term * trs_term
let trs_rule_to_string term =
let rec trs_term_to_string_nopos term =
match term with
| RR (l, r) -> trs_term_to_string l ^ " -> " ^ trs_term_to_string r
let rec tcon_tovar trsterm =
match trsterm with
| TVar _ -> trsterm
| TDes (e1, e2) ->
TDes (tcon_tovar e1, tcon_tovar e2)
| TVar v -> v
| TDes (e1, e2) -> (
match (e1, e2) with
| TDes _, TDes _ ->
"("
^ trs_term_to_string_nopos e1
^ ") ("
^ trs_term_to_string_nopos e2
^ ")"
| TDes _, _ ->
" ("
^ trs_term_to_string_nopos e1
^ ") "
^ trs_term_to_string_nopos e2
| _, TDes _ ->
trs_term_to_string_nopos e1 ^ " (" ^ trs_term_to_string_nopos e2 ^ ")"
| _, _ -> trs_term_to_string_nopos e1 ^ " " ^ trs_term_to_string_nopos e2
)
| TCon (l, fvs) ->
if fvs = [] then TVar (String.lowercase_ascii l) else
TCon (l, L.map tcon_tovar fvs)
if fvs = [] then l
else
l ^ "["
^ String.concat "," (L.map (fun x -> trs_term_to_string (fst x)) fvs)
^ "]"
let trs_rule_to_string term =
match term with
| RR (l, r) ->
trs_term_to_string_nopos l ^ " -> " ^ trs_term_to_string_nopos r
let rec rules lterm =
match lterm with
| LVar _ -> []
| LApp (e1, e2) -> rules e1 @ rules e2
| LLam (_, _, x, e) ->
let e_t = tcon_tovar (l_term_to_trsterm e) in
let trsterm = l_term_to_trsterm lterm in
let trsterm_t = (
match trsterm with
| TCon (l, fvs) ->
TCon (l, L.map tcon_tovar fvs)
| _ -> trsterm
) in
RR (TDes (trsterm_t, TVar x), e_t)
:: rules e
| LLam (l, f, x, e) ->
let e' = components_lterm x e in
let e_t = l_term_to_trsterm e' in
let trsterm_t = l_term_to_trsterm (LLam (l, f, x, e')) in
RR (TDes (trsterm_t, TVar x), e_t) :: rules e
let rules_to_string xs = String.concat ".\n" (L.map trs_rule_to_string xs)
......@@ -261,9 +319,18 @@ let rec _redexpos trsterm pos =
| TDes (e1, e2) ->
let posl = _redexpos e1 (pos ^ "1") in
if posl != "" then posl else _redexpos e2 (pos ^ "2")
| TCon (_, fvs) ->
if fvs = [] then ""
else
let xs =
L.filter
(fun y -> y != "")
(L.map (fun x -> _redexpos (fst x) (pos ^ snd x)) fvs)
in
if L.length xs > 0 then L.hd xs else ""
| _ -> ""
let redexpos trsterm = _redexpos trsterm ""
let redexpos trsterm = _redexpos trsterm "e"
let rec search_pairs v f = function
| (x, n) :: xs -> if f v = f x then n else search_pairs v f xs
......@@ -273,30 +340,38 @@ let rec subst m pairs =
(* Printf.printf "subst\n"; *)
match m with
| 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)
| TCon (l, fvs) -> TCon (l, L.map (fun z -> (subst (fst z) pairs, snd z)) fvs)
let rec rewrite trsrules trsterm =
(* Printf.printf "Rewrite: %s\n" (trs_term_to_string 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 fvs fvs2)
if l = l2 then
subst r ((TVar x, arg) :: L.combine (L.map fst fvs) (L.map fst fvs2))
else rewrite xs trsterm
| [], _ -> trsterm
| _, _ -> failwith "Not a rule or not a trsterm."
let rec _rstep trsterm trsrules pos p =
(* Printf.printf "%s # %s # %s\n" (trs_term_to_string trsterm) pos p; *)
match trsterm with
| TDes (TCon (_, _), _) ->
if p = pos then rewrite trsrules trsterm else trsterm
| TDes (e1, e2) ->
TDes (_rstep e1 trsrules pos (p ^ "1"), _rstep e2 trsrules pos (p ^ "2"))
| TCon (l, fvs) ->
TCon
( l,
L.map (fun z -> (_rstep (fst z) trsrules pos (p ^ snd z), snd z)) fvs
)
| _ -> trsterm
let rstep trs =
match trs with TRS (xs, t) -> TRS (xs, _rstep t xs (redexpos t) "")
match trs with TRS (xs, t) -> TRS (xs, _rstep t xs (redexpos t) "e")
let rstep_pos trs pos =
match trs with TRS (xs, t) -> TRS (xs, _rstep t xs pos "")
match trs with TRS (xs, t) -> TRS (xs, _rstep t xs pos "e")
let rec all_vars vs =
match vs with TVar _ :: xs -> all_vars xs | _ :: _ -> false | [] -> true
......@@ -304,8 +379,9 @@ let rec all_vars vs =
(* project : TRS -> term *)
let rec trs_rule trsrules label =
match trsrules with
| RR (TDes (TCon (l, fvs), _), _) :: xs ->
if l = label && all_vars fvs then L.hd trsrules else trs_rule xs label
| RR (TDes (TCon (l, _), _), _) :: xs ->
(* if l = label && all_vars (L.map fst fvs) then L.hd trsrules else trs_rule xs label *)
if l = label then L.hd trsrules else trs_rule xs label
| _ :: xs -> trs_rule xs label
| [] -> failwith "No rule with such label."
......@@ -326,21 +402,30 @@ let rec trs_to_term trs =
let rr = trs_rule xs label in
match rr with
| RR (TDes (TCon (_, fvs_r), var), r) ->
if L.mem var fvs then
if L.mem var (L.map fst fvs) then
let fresh = next_fresh_2 () in
let rfresh = subst r [ (var, TVar fresh) ] in
LLam
( label,
L.map trs_to_term (L.map (fun st -> TRS (xs, st)) fvs),
L.map trs_to_term
(L.map (fun st -> TRS (xs, st)) (L.map fst fvs)),
fresh,
trs_to_term (TRS (xs, subst rfresh (L.combine fvs_r fvs)))
)
trs_to_term
(TRS
( xs,
subst rfresh
(L.combine (L.map fst fvs_r) (L.map fst fvs)) )) )
else
LLam
( label,
L.map trs_to_term (L.map (fun st -> TRS (xs, st)) fvs),
L.map trs_to_term
(L.map (fun st -> TRS (xs, st)) (L.map fst fvs)),
vtname var,
trs_to_term (TRS (xs, subst r (L.combine fvs_r fvs))) )
trs_to_term
(TRS
( xs,
subst r (L.combine (L.map fst fvs_r) (L.map fst fvs))
)) )
| _ -> failwith "Not a RR found." ) )
let trs_to_string trs =
......@@ -365,15 +450,15 @@ let rec simulate_trs_in_lterm trs =
| TRS (_, t) ->
let pos = redexpos t in
let trs' = rstep_pos trs pos in
if t = trs_term trs' then []
else
let lterm = trs_to_term trs in
let lterm' = weak_step_pos lterm pos in
let lterm'_trs = l_term_to_trs lterm' in
( trs_to_string trs ^ "\n\n" ^ l_term_to_string lterm ^ "\n->" ^ pos
^ "\n" ^ l_term_to_string lterm' ^ "\n\n" ^ trs_to_string trs' ^ "\n\n"
^ trs_to_string lterm'_trs )
:: simulate_trs_in_lterm trs'
let lterm = trs_to_term trs in
let lterm' = weak_step_pos lterm pos in
let lterm'_trs = l_term_to_trs lterm' in
( trs_to_string trs ^ "\n\n"
^ _term_to_string (l_term_to_term lterm)
^ "\n->" ^ pos ^ "\n"
^ _term_to_string (l_term_to_term lterm')
^ "\n\n" ^ trs_to_string trs' ^ "\n\n" ^ trs_to_string lterm'_trs )
:: (if t = trs_term trs' then [] else simulate_trs_in_lterm trs')
(*
trs ....... -> ...... trs'
......@@ -383,21 +468,21 @@ lterm ...... -> ...... lterm'
*)
let rec simulate_lterm_in_trs lterm =
let pos = weak_redexpos lterm in
let trs = l_term_to_trs lterm in
let lterm' = weak_step_pos lterm pos in
if lterm = lterm' then []
else
let trs = l_term_to_trs lterm in
let trs' = rstep_pos trs pos in
let trs'_lterm = trs_to_term trs' in
let alpha_eq = default_names trs'_lterm = default_names lterm' in
( "lterm: " ^ l_term_to_string lterm ^ "\n\n" ^ trs_to_string trs ^ "\n->"
^ pos ^ "\n"
^ trs_term_to_string (trs_term trs')
^ "\n\ntrs'_lterm: "
^ l_term_to_string trs'_lterm
^ "\nlterm' : " ^ l_term_to_string lterm' ^ "\n\nalpha_eq: "
^ Bool.to_string alpha_eq )
:: simulate_lterm_in_trs lterm'
let trs' = rstep_pos trs pos in
let trs'_lterm = trs_to_term trs' in
let alpha_eq = default_names trs'_lterm = default_names lterm' in
( "lterm: "
^ _term_to_string (l_term_to_term lterm)
^ "\nredex@" ^ pos ^ "\n" ^ trs_to_string trs ^ "\n->" ^ pos ^ "\n"
^ trs_term_to_string (trs_term trs')
^ "\n\ntrs'_lterm: "
^ _term_to_string (l_term_to_term trs'_lterm)
^ "\nlterm' : "
^ _term_to_string (l_term_to_term lterm')
^ "\n\nalpha_eq: " ^ Bool.to_string alpha_eq )
:: (if lterm = lterm' then [] else simulate_lterm_in_trs lterm')
let print_simulation lterm =
let sim = simulate_lterm_in_trs lterm 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