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

syntactic sugar

parent a6120ed8
......@@ -31,8 +31,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 []
(* lift : term -> TRS *)
let rec term_to_l_term term =
match term with
let rec term_to_l_term = function
| Var x -> LVar x
| Lam (x, e) ->
let l = next_label () in
......@@ -50,16 +49,15 @@ let rec rename term x y =
| LLam (l, s, t) -> if s = x then term else LLam (l, s, rename t x y)
| LApp (e1, e2) -> LApp (rename e1 x y, rename e2 x y)
let rec default_names_r term pos =
match term with
let rec default_names_r pos = function
| LVar v -> LVar v
| LLam (l, v, t) ->
let vf = "x_" ^ pos in
LLam (l, vf, default_names_r (rename t v vf) (pos ^ _LAM))
LLam (l, vf, default_names_r (pos ^ _LAM) (rename t v vf) )
| LApp (e1, e2) ->
LApp (default_names_r e1 (pos ^ _APP_L), default_names_r e2 (pos ^ _APP_R))
LApp (default_names_r (pos ^ _APP_L) e1, default_names_r (pos ^ _APP_R) e2)
let default_names term = default_names_r term _ROOT
let default_names term = default_names_r _ROOT term
(** Extract the name of a variable from a {e a_term} *)
let lvname = function LVar n -> n | _ -> ""
......@@ -103,8 +101,7 @@ let rec _casubst m x n fvn =
let casubst m x n = _casubst m x n (L.map lvname (free_variables n))
let beta term =
match term with
let beta = function
| LApp (LLam (_, x, m), n) -> casubst m x n
| _ -> failwith "beta: Not a redex."
......@@ -158,9 +155,8 @@ type trs_term =
(** Extract the name of a variable from a {e a_term} *)
let vtname = function TVar n -> n | _ -> ""
let rec fvar_trsterm t =
match t with
| TVar _ -> [ t ]
let rec fvar_trsterm = function
| TVar v -> [ TVar v ]
| TDes (e1, e2) -> fvar_trsterm e1 @ fvar_trsterm e2
| TCon (_, fvs) -> L.flatten (L.map (fun x -> fvar_trsterm (fst x)) fvs)
......@@ -184,8 +180,7 @@ let rec _components_lterm xs pos lterm =
@ _components_lterm xs (pos ^ _APP_R) e2 )
| LLam (_, y, e) -> _components_lterm (LVar y :: xs) (pos ^ _LAM) e
let rec l_term_to_trsterm lterm =
match lterm with
let rec l_term_to_trsterm = function
| LVar x -> TVar x
| LApp (e1, e2) -> TDes (l_term_to_trsterm e1, l_term_to_trsterm e2)
| LLam (l, x, e) ->
......@@ -196,10 +191,10 @@ let rec _fvar_components_lterm xs pos lterm =
if free_variables lterm = [] then LVar ("v_" ^ pos)
else
match lterm with
| LVar y -> if L.mem y xs then lterm else LVar ("v_" ^ pos)
| LVar _ -> if L.mem lterm xs then lterm else LVar ("v_" ^ pos)
| LApp (e1, e2) -> (
let e1_fvs = intersect xs (L.map lvname (free_variables e1)) in
let e2_fvs = intersect xs (L.map lvname (free_variables e2)) in
let e1_fvs = intersect xs (free_variables e1) in
let e2_fvs = intersect xs (free_variables e2) in
match (e1_fvs, e2_fvs) with
| [], [] -> LVar ("v_" ^ pos)
| _, _ ->
......@@ -208,20 +203,19 @@ let rec _fvar_components_lterm xs pos lterm =
LApp (e1', e2')
)
| LLam (l, y, e) ->
let e' = _fvar_components_lterm (y :: xs) (pos ^ _LAM) e in
let e' = _fvar_components_lterm (LVar y :: xs) (pos ^ _LAM) e in
LLam (l, y, e')
let fvar_components_lterm x lterm =
_fvar_components_lterm [ x ] _ROOT lterm
let fvar_components_lterm xs lterm =
_fvar_components_lterm xs _ROOT lterm
type trs_rule = RR of trs_term * trs_term
let rec rules lterm =
match lterm with
let rec rules = function
| LVar _ -> []
| LApp (e1, e2) -> rules e1 @ rules e2
| LLam (l, x, e) ->
let e' = fvar_components_lterm x e in
let e' = fvar_components_lterm [ LVar x ] e in
let e_t = l_term_to_trsterm e' in
let trsterm_t = l_term_to_trsterm (LLam (l, x, e')) in
RR (TDes (trsterm_t, TVar x), e_t) :: rules e
......@@ -234,29 +228,29 @@ let trs_term = function TRS (_, t) -> t
let l_term_to_trs x = TRS (rules x, l_term_to_trsterm x)
let rec _redexpos trsterm pos =
match trsterm with
let rec _redexpos pos = function
| TDes (TCon (_, _), _) -> pos
| TDes (e1, e2) ->
let posl = _redexpos e1 (pos ^ _APP_L) in
if posl != "" then posl else _redexpos e2 (pos ^ _APP_R)
let posl = _redexpos (pos ^ _APP_L) e1 in
if posl != "" then posl else _redexpos (pos ^ _APP_R) e2
| TCon (_, fvs) ->
if fvs = [] then ""
else
let xs =
L.filter
(fun y -> y != "")
(L.map (fun x -> _redexpos (fst x) (pos ^ snd x)) fvs)
(L.map (fun x -> _redexpos (pos ^ snd x) (fst x)) fvs)
in
if L.length xs > 0 then L.hd xs else ""
| _ -> ""
let redexpos trsterm = _redexpos trsterm _ROOT
let redexpos trsterm = _redexpos _ROOT trsterm
let rec combine a b =
match (a, b) with
| TVar _, _ -> [ (a, b) ]
| TDes (a1, a2), TDes (b1, b2) -> combine a1 b1 @ combine a2 b2
| TDes (a1, a2), TDes (b1, b2) ->
combine a1 b1 @ combine a2 b2
| TCon (_, a1), TCon (_, b1) ->
L.flatten
(L.map
......@@ -304,11 +298,11 @@ let rec _rstep trsterm trsrules pos p =
)
| _ -> trsterm
let rstep trs =
match trs with TRS (xs, t) -> TRS (xs, _rstep t xs (redexpos t) _ROOT)
let rstep = function
| TRS (xs, t) -> TRS (xs, _rstep t xs (redexpos t) _ROOT)
let rstep_pos trs pos =
match trs with TRS (xs, t) -> TRS (xs, _rstep t xs pos _ROOT)
let rstep_pos pos = function
| TRS (xs, t) -> TRS (xs, _rstep t xs pos _ROOT)
(* project : TRS -> term *)
let rec trs_rule trsrules label =
......@@ -324,10 +318,9 @@ let next_fresh_2 () =
counter_projection := !counter_projection + 1;
"v" ^ string_of_int !counter_projection
let rec trs_to_term trs =
let rec trs_to_term = function
(* Printf.printf "trstoterm: %s\n\n" (trs_to_string trs); *)
match trs with
| TRS (xs, t) -> (
| TRS (xs, t) ->
match t with
| TVar x -> LVar x
| TDes (e1, e2) ->
......@@ -361,4 +354,4 @@ let rec trs_to_term trs =
subst r
(combine_fvs (L.map fst fvs_r) (L.map fst fvs)) ))
)
| _ -> failwith "Not a RR found." ) )
| _ -> failwith "Not a RR found." )
......@@ -71,7 +71,7 @@ let rec _simulate_lterm_in_trs lterm trs alltrue =
let pos = weak_redexpos lterm in
if pos <> "" then
let lterm' = weak_step_pos lterm pos in
let trs' = rstep_pos trs pos in
let trs' = rstep_pos pos trs in
let trs'_lterm = trs_to_term trs' in
let alpha_eq = default_names trs'_lterm = default_names lterm' in
let alltrue = alltrue && alpha_eq 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