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

minimal bound context

parent fa096ac0
......@@ -12,4 +12,5 @@ let () =
try str_to_term (Sys.argv.(1) ^ "\n") with _ -> failwith "Syntax error"
in
let lterm = Core.term_to_l_term term in
Core.print_simulation lterm
Printf.printf "%s\n%s" (Core.trs_term_to_string (Core.l_term_to_trsterm lterm))
(Core.rules_to_string (Core.rules lterm))
......@@ -50,10 +50,17 @@ let vname = function Var n -> n | _ -> ""
let remove l1 f x =
L.fold_left (fun acc hd -> if f hd = x then acc else hd :: acc) [] l1
let rec fvars = function
let rec _fvars = function
| Var x -> [ Var x ]
| Lam (x, e) -> remove (fvars e) vname x
| App (e1, e2) -> fvars e1 @ fvars e2
| Lam (x, e) -> remove (_fvars e) vname x
| App (e1, e2) -> _fvars e1 @ _fvars e2
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)
(* lift : term -> TRS *)
let rec term_to_l_term term =
......@@ -183,11 +190,25 @@ let rec trs_term_to_string term =
let term_print term = Printf.printf "%s" (trs_term_to_string term)
let rec fvars_trsterm x trsterm =
match trsterm with
| TVar _ ->
if trsterm = TVar x then [] else [trsterm]
| TDes (e1, e2) ->
fvars_trsterm x e1 @ fvars_trsterm x e2
| TCon (_, fvs) ->
if fvs = [] then [trsterm] else
L.flatten (L.map (fvars_trsterm x) fvs)
let rec l_term_to_trsterm lterm =
match lterm with
| LVar x -> TVar x
| LLam (l, fvs, _, _) -> TCon (l, L.map l_term_to_trsterm fvs)
| 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
TCon (l, fvs_t)
type trs_rule = RR of trs_term * trs_term
......@@ -195,13 +216,30 @@ let trs_rule_to_string 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)
| TCon (l, fvs) ->
if fvs = [] then TVar (String.lowercase_ascii l) else
TCon (l, L.map tcon_tovar fvs)
let rec rules lterm =
match lterm with
| LVar _ -> []
| LApp (e1, e2) -> rules e1 @ rules e2
| LLam (_, _, x, e) ->
RR (TDes (l_term_to_trsterm lterm, TVar x), l_term_to_trsterm 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
| LApp (e1, e2) -> rules e1 @ rules e2
let rules_to_string xs = String.concat ".\n" (L.map trs_rule_to_string xs)
......
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