Commit 3968cb1b authored by Frontull Samuel's avatar Frontull Samuel
Browse files

formatting

parent 91696637
......@@ -53,7 +53,7 @@ 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 (pos ^ _LAM) (rename t v vf) )
LLam (l, vf, default_names_r (pos ^ _LAM) (rename t v vf))
| LApp (e1, e2) ->
LApp (default_names_r (pos ^ _APP_L) e1, default_names_r (pos ^ _APP_R) e2)
......@@ -116,8 +116,7 @@ let rec _weak_redexpos term pos bvs =
| [] -> pos
| _ ->
let posl = _weak_redexpos (LLam (l, v, b)) (pos ^ _APP_L) bvs in
if posl <> "" then posl else _weak_redexpos arg (pos ^ _APP_R) bvs
)
if posl <> "" then posl else _weak_redexpos arg (pos ^ _APP_R) bvs )
| LApp (e1, e2) ->
let posl = _weak_redexpos e1 (pos ^ _APP_L) bvs in
if posl <> "" then posl else _weak_redexpos e2 (pos ^ _APP_R) bvs
......@@ -185,7 +184,7 @@ let rec l_term_to_trsterm = function
| LApp (e1, e2) -> TDes (l_term_to_trsterm e1, l_term_to_trsterm e2)
| LLam (l, x, e) ->
let cmps = _components_lterm [ LVar x ] _LAM e in
TCon (l, L.map (fun (t,p) -> (l_term_to_trsterm t, p)) cmps)
TCon (l, L.map (fun (t, p) -> (l_term_to_trsterm t, p)) cmps)
let rec _fvar_components_lterm xs pos lterm =
if free_variables lterm = [] then LVar ("v_" ^ pos)
......@@ -200,14 +199,12 @@ let rec _fvar_components_lterm xs pos lterm =
| _, _ ->
let e1' = _fvar_components_lterm xs (pos ^ _APP_L) e1 in
let e2' = _fvar_components_lterm xs (pos ^ _APP_R) e2 in
LApp (e1', e2')
)
LApp (e1', e2') )
| LLam (l, y, e) ->
let e' = _fvar_components_lterm (LVar y :: xs) (pos ^ _LAM) e in
LLam (l, y, e')
let fvar_components_lterm xs lterm =
_fvar_components_lterm xs _ROOT lterm
let fvar_components_lterm xs lterm = _fvar_components_lterm xs _ROOT lterm
type trs_rule = RR of trs_term * trs_term
......@@ -249,8 +246,7 @@ 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
......@@ -298,11 +294,9 @@ let rec _rstep trsterm trsrules pos p =
)
| _ -> trsterm
let rstep = function
| 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 pos = function
| 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 =
......@@ -320,7 +314,7 @@ let next_fresh_2 () =
let rec trs_to_term = function
(* Printf.printf "trstoterm: %s\n\n" (trs_to_string trs); *)
| TRS (xs, t) ->
| TRS (xs, t) -> (
match t with
| TVar x -> LVar x
| TDes (e1, e2) ->
......@@ -354,4 +348,4 @@ let rec trs_to_term = function
subst r
(combine_fvs (L.map fst fvs_r) (L.map fst fvs)) ))
)
| _ -> failwith "Not a RR found." )
| _ -> 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