Commit 461c6fdf authored by Samuel Frontull's avatar Samuel Frontull
Browse files

Merge branch 'master' into 'main'

Master

See merge request !5
parents 3878d8e5 e450b42b
......@@ -12,4 +12,4 @@ 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
Io.print_simulation lterm
module L = List
let _ROOT = "e"
let _APP_L = "1"
let _APP_R = "2"
let _LAM = "1"
type term = Var of string | Lam of string * term | App of term * term
let rec _term_to_string term =
match term with
| Var v -> v
| Lam (v, t) -> "λ" ^ v ^ "." ^ _term_to_string t
| App (e1, e2) -> (
match (e1, e2) with
| Var _, Var _ -> _term_to_string e1 ^ " " ^ _term_to_string e2
| Var _, _ -> _term_to_string e1 ^ " (" ^ _term_to_string e2 ^ ")"
| _, Var _ -> "(" ^ _term_to_string e1 ^ ") " ^ _term_to_string e2
| _, _ -> "(" ^ _term_to_string e1 ^ ") (" ^ _term_to_string e2 ^ ")" )
let remove l1 f x =
L.fold_left (fun acc hd -> if f hd = x then acc else hd :: acc) [] l1
let label = ref 0
......@@ -21,39 +21,12 @@ let next_label () =
type l_term =
| LVar of string
| LLam of string * l_term list * string * l_term
| LLam of string * string * l_term
| LApp of l_term * l_term
let rec _l_term_to_string term c =
match term with
| LVar v -> v
| LLam (l, fvs, v, t) ->
"λ" ^ v ^ "_" ^ l ^ "["
^ String.concat " " (L.map (fun k -> _l_term_to_string k 0) fvs)
^ "]."
^ _l_term_to_string t (c + 1)
| LApp (e1, e2) -> (
match (e1, e2) with
| LVar _, LVar _ -> _l_term_to_string e1 c ^ " " ^ _l_term_to_string e2 c
| LVar _, _ ->
_l_term_to_string e1 c ^ " (" ^ _l_term_to_string e2 c ^ ")"
| _, LVar _ ->
"(" ^ _l_term_to_string e1 c ^ ") " ^ _l_term_to_string e2 c
| _, _ ->
"(" ^ _l_term_to_string e1 c ^ ") (" ^ _l_term_to_string e2 c ^ ")" )
let l_term_to_string term = _l_term_to_string term 0
let uniq_cons x xs = if L.mem x xs then xs else x :: xs
(** Extract the name of a variable from a {e a_term} *)
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
| Var x -> [ Var x ]
| Lam (x, e) -> remove (fvars e) vname x
| App (e1, e2) -> fvars e1 @ fvars e2
let linear_list xs = L.fold_right uniq_cons xs []
(* lift : term -> TRS *)
let rec term_to_l_term term =
......@@ -61,33 +34,30 @@ let rec term_to_l_term term =
| Var x -> LVar x
| Lam (x, e) ->
let l = next_label () in
let fvs = L.map term_to_l_term (fvars term) in
LLam (l, fvs, x, term_to_l_term e)
LLam (l, x, term_to_l_term e)
| App (e1, e2) -> LApp (term_to_l_term e1, term_to_l_term e2)
let rec l_term_to_term = function
| LVar v -> Var v
| LLam (_, _, v, t) -> Lam (v, l_term_to_term t)
| LLam (_, v, t) -> Lam (v, l_term_to_term t)
| LApp (e1, e2) -> App (l_term_to_term e1, l_term_to_term e2)
let rec rename_fv term x y =
match term with
| LVar s -> if s = x then LVar y else term
| LLam (l, fvs, s, t) ->
let fvs' = L.map (fun t -> rename_fv t x y) fvs in
if s = x then term else LLam (l, fvs', s, rename_fv t x y)
| LLam (l, s, t) -> if s = x then term else LLam (l, s, rename_fv t x y)
| LApp (e1, e2) -> LApp (rename_fv e1 x y, rename_fv e2 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 ^ _LAM))
| LApp (e1, e2) ->
LApp (default_names_r e1 (pos ^ "0"), default_names_r e2 (pos ^ "1"))
LApp (default_names_r e1 (pos ^ _APP_L), default_names_r e2 (pos ^ _APP_R))
let default_names term = default_names_r term "e"
let default_names term = default_names_r term _ROOT
(** Extract the name of a variable from a {e a_term} *)
let lvname = function LVar n -> n | _ -> ""
......@@ -95,7 +65,7 @@ let lvname = function LVar n -> n | _ -> ""
(** Extract the free variables in a {e a_term} *)
let rec free_variables = function
| LVar x -> [ LVar x ]
| LLam (_, _, x, e) -> remove (free_variables e) lvname x
| LLam (_, x, e) -> remove (free_variables e) lvname x
| LApp (e1, e2) -> free_variables e1 @ free_variables e2
let counter = ref 0
......@@ -104,105 +74,154 @@ let next_fresh () =
counter := !counter + 1;
"p_" ^ string_of_int !counter
(** replace every var occurrence by fresh var *)
(** replace every var x occurrence by var y *)
let rec subst m x y =
match m with
| LVar z -> if z = x then LVar y else m
| LLam (l, fvs, z, e) ->
| LLam (l, z, e) ->
let z' = if z = x then y else z in
let fvs' = L.map (fun t -> subst t x y) fvs in
LLam (l, fvs', z', subst e x y)
LLam (l, z', subst e x y)
| LApp (e1, e2) -> LApp (subst e1 x y, subst e2 x y)
(** capture-avoiding substitution *)
let rec _casubst m x n fvn =
match m with
| LVar y -> if x = y then n else m
| LLam (l, fvs, y, e) -> (
| LApp (e1, e2) -> LApp (_casubst e1 x n fvn, _casubst e2 x n fvn)
| LLam (l, y, e) -> (
if y = x then m
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 -> x = y) fvn in
match inters with
| [] ->
LLam
(l, L.map (fun z -> _casubst z x n fvn) fvs, y, _casubst e x n fvn)
| [] -> LLam (l, y, _casubst e x n fvn)
| hd :: _ ->
let f = next_fresh () in
let m' = subst m hd f in
_casubst m' x n fvn )
| LApp (e1, e2) -> LApp (_casubst e1 x n fvn, _casubst e2 x n fvn)
let casubst m x n = _casubst m x n (L.map lvname (free_variables n))
let beta term =
match term with
| LApp (LLam (_, _, x, m), n) ->
let res = casubst m x n in
res
| LApp (LLam (_, x, m), n) -> casubst m x n
| _ -> failwith "beta: Not a redex."
let rec _weak_redexpos term pos =
let rec _weak_redexpos term pos bvs =
match term with
| LApp (LLam (_, _, _, _), _) -> pos
| LApp (LLam (l, v, b), arg) -> (
(* Printf.printf "%s\n" (l_term_to_string term); *)
let fvs = free_variables term in
let f_bvs = L.filter (fun x -> L.mem x bvs) fvs in
match f_bvs with
| [] -> 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 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")
let posl = _weak_redexpos e1 (pos ^ _APP_L) bvs in
if posl <> "" then posl else _weak_redexpos e2 (pos ^ _APP_R) bvs
| LLam (_, x, e) -> _weak_redexpos e (pos ^ _LAM) (LVar x :: bvs)
| _ -> ""
let weak_redexpos term = _weak_redexpos term ""
let weak_redexpos term = _weak_redexpos term _ROOT []
let starts_with p s =
if String.length p <= String.length s then
String.sub s 0 (String.length p) = p
else false
let rec _weak_step term pos p =
match term with
| LApp (LLam (_, _, _, _), _) -> if p = pos then beta term else term
| LApp (LLam (l, v, b), arg) ->
if p = pos then beta term
else if starts_with (p ^ _APP_L) pos then
LApp (_weak_step (LLam (l, v, b)) pos (p ^ _APP_L), arg)
else LApp (LLam (l, v, b), _weak_step arg pos (p ^ _APP_R))
| LApp (e1, e2) ->
LApp (_weak_step e1 pos (p ^ "1"), _weak_step e2 pos (p ^ "2"))
LApp (_weak_step e1 pos (p ^ _APP_L), _weak_step e2 pos (p ^ _APP_R))
| LLam (l, x, e) -> LLam (l, x, _weak_step e pos (p ^ _LAM))
| _ -> term
let weak_step term = _weak_step term (weak_redexpos term) ""
let weak_step term = _weak_step term (weak_redexpos term) _ROOT
let weak_step_pos term pos = _weak_step term pos ""
let weak_step_pos term pos = _weak_step term pos _ROOT
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} *)
let vtname = function TVar n -> n | _ -> ""
let rec trs_term_to_string term =
match term with
| TVar v -> v
| 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 ^ ")"
let isvar = function TVar _ -> true | _ -> false
let term_print term = Printf.printf "%s" (trs_term_to_string term)
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 rec _components_lterm xs pos lterm =
if free_variables lterm = [] then [ (lterm, pos) ]
else
match lterm with
| LVar _ -> if L.mem lterm xs then [] else [ (lterm, pos) ]
| LApp (e1, e2) -> (
(* check if abstracted variables occur in left argument *)
let e1_fvs = L.filter (fun z -> L.mem z (free_variables e1)) xs in
(* check if abstracted variables occur in right argument *)
let e2_fvs = L.filter (fun z -> L.mem z (free_variables e2)) xs in
match (e1_fvs, e2_fvs) with
| [], [] -> [ (lterm, pos) ]
| [], _ ->
[ (e1, pos ^ _APP_L) ] @ _components_lterm xs (pos ^ _APP_R) e2
| _, [] ->
_components_lterm xs (pos ^ _APP_L) e1 @ [ (e2, pos ^ _APP_R) ]
| _, _ ->
_components_lterm xs (pos ^ _APP_L) e1
@ _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
| 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)
| LLam (l, x, e) ->
let cmps = _components_lterm [ LVar x ] _LAM e in
TCon (l, L.map (fun c -> (l_term_to_trsterm (fst c), snd c)) cmps)
type trs_rule = RR of trs_term * trs_term
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)
| LApp (e1, e2) -> (
let e1' = _fvar_components_lterm xs (pos ^ _APP_L) e1 in
let e2' = _fvar_components_lterm xs (pos ^ _APP_R) e2 in
match (e1', e2') with
| LVar x, LVar y ->
if L.mem x xs || L.mem y xs then LApp (e1', e2')
else LVar ("v_" ^ pos)
| _ -> LApp (e1', e2') )
| LLam (l, y, e) ->
let e' = _fvar_components_lterm (y :: xs) (pos ^ _LAM) e in
LLam (l, y, e')
let fvar_components_lterm x lterm = _fvar_components_lterm [ x ] _ROOT lterm
let trs_rule_to_string term =
match term with
| RR (l, r) -> trs_term_to_string l ^ " -> " ^ trs_term_to_string r
type trs_rule = RR of trs_term * trs_term
let rec rules lterm =
match lterm with
| LVar _ -> []
| LLam (_, _, x, e) ->
RR (TDes (l_term_to_trsterm lterm, TVar x), l_term_to_trsterm e)
:: rules e
| LApp (e1, e2) -> rules e1 @ rules e2
let rules_to_string xs = String.concat ".\n" (L.map trs_rule_to_string xs)
| LLam (l, x, e) ->
let e' = fvar_components_lterm 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
type trs = TRS of trs_rule list * trs_term
......@@ -210,37 +229,59 @@ let trs_rules = function TRS (xs, _) -> xs
let trs_term = function TRS (_, t) -> t
let term_to_trs x =
let lx = term_to_l_term x in
TRS (rules lx, l_term_to_trsterm lx)
let l_term_to_trs x = TRS (rules x, l_term_to_trsterm x)
let rec _redexpos trsterm pos =
match trsterm with
| TDes (TCon (_, _), _) -> pos
| TDes (e1, e2) ->
let posl = _redexpos e1 (pos ^ "1") in
if posl != "" then posl else _redexpos e2 (pos ^ "2")
let posl = _redexpos e1 (pos ^ _APP_L) in
if posl != "" then posl else _redexpos e2 (pos ^ _APP_R)
| 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 _ROOT
let rec combine a b =
match (a, b) with
| TVar _, _ -> [ (a, b) ]
| TDes (a1, a2), TDes (b1, b2) -> combine a1 b1 @ combine a2 b2
| TCon (_, a1), TCon (_, b1) ->
L.flatten
(L.map
(fun x -> combine (fst x) (snd x))
(L.combine (L.map fst a1) (L.map fst b1)))
| _, _ -> failwith "combine not same structure."
let rec combine_fvs fvs_r fvs =
match (fvs_r, fvs) with
| t :: ts, f :: fs -> combine t f @ combine_fvs ts fs
| [], [] -> []
| _, _ -> failwith "combine_fvs not same length."
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 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 =
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) :: combine_fvs (L.map fst fvs) (L.map fst fvs2))
else rewrite xs trsterm
| [], _ -> trsterm
| _, _ -> failwith "Not a rule or not a trsterm."
......@@ -250,23 +291,27 @@ let rec _rstep trsterm trsrules pos p =
| 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"))
TDes
( _rstep e1 trsrules pos (p ^ _APP_L),
_rstep e2 trsrules pos (p ^ _APP_R) )
| 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) _ROOT)
let rstep_pos trs pos =
match trs with TRS (xs, t) -> TRS (xs, _rstep t xs pos "")
let rec all_vars vs =
match vs with TVar _ :: xs -> all_vars xs | _ :: _ -> false | [] -> true
match trs with TRS (xs, t) -> TRS (xs, _rstep t xs pos _ROOT)
(* 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 then L.hd trsrules else trs_rule xs label
| _ :: xs -> trs_rule xs label
| [] -> failwith "No rule with such label."
......@@ -277,93 +322,40 @@ let next_fresh_2 () =
"v" ^ string_of_int !counter_projection
let rec trs_to_term trs =
(* Printf.printf "trstoterm: %s\n\n" (trs_to_string trs); *)
match trs with
| TRS (xs, t) -> (
match t with
| TVar x -> LVar x
| TDes (e1, e2) ->
LApp (trs_to_term (TRS (xs, e1)), trs_to_term (TRS (xs, e2)))
| TCon (label, fvs) -> (
let rr = trs_rule xs label in
| TCon (l, fvs) -> (
let rr = trs_rule xs l in
match rr with
| RR (TDes (TCon (_, fvs_r), var), r) ->
if L.mem var fvs then
let fresh = next_fresh_2 () in
let rfresh = subst r [ (var, TVar fresh) ] in
if
L.mem var
(L.flatten (L.map (fun f -> fvar_trsterm (fst f)) fvs))
then
let f = next_fresh_2 () in
let rfresh = subst r [ (var, TVar f) ] in
LLam
( label,
L.map trs_to_term (L.map (fun st -> TRS (xs, st)) fvs),
fresh,
trs_to_term (TRS (xs, subst rfresh (L.combine fvs_r fvs)))
( l,
f,
trs_to_term
(TRS
( xs,
subst rfresh
(combine_fvs (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,
vtname var,
trs_to_term (TRS (xs, subst r (L.combine fvs_r fvs))) )
trs_to_term
(TRS
( xs,
subst r
(combine_fvs (L.map fst fvs_r) (L.map fst fvs)) ))
)
| _ -> failwith "Not a RR found." ) )
let trs_to_string trs =
match trs with
| TRS (xs, t) ->
"TRS:\n" ^ rules_to_string xs ^ ".\n----\n" ^ trs_term_to_string t
let rec _weak_reduction term =
let wt = weak_step term in
if wt = term then [] else wt :: _weak_reduction wt
let weak_reduction term = term :: _weak_reduction term
let rec _trs_reduction trs =
let rt = rstep trs in
if rt = trs then [] else rt :: _trs_reduction rt
let trs_reduction trs = trs :: _trs_reduction trs
let rec simulate_trs_in_lterm trs =
match trs with
| 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'
(*
trs ....... -> ...... trs'
^ |
| v
lterm ...... -> ...... lterm'
*)
let rec simulate_lterm_in_trs lterm =
let pos = weak_redexpos 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 print_simulation lterm =
let sim = simulate_lterm_in_trs lterm in
let sim2 = simulate_trs_in_lterm (l_term_to_trs lterm) in
Printf.printf
"%s\n\n++++++++++++++++\n++++++++++++++++\n++++++++++++++++\n\n%s\n"
(String.concat "\n\n========================\n\n" sim)
(String.concat "\n\n========================\n\n" sim2)
open Core
let rec _l_term_to_string term c label =
match term with
| LVar v -> v
| LLam (l, v, t) ->
if label then "λ" ^ v ^ "_" ^ l ^ "." ^ _l_term_to_string t (c + 1) label
else "λ" ^ v ^ "." ^ _l_term_to_string t (c + 1) label
| LApp (e1, e2) -> (
match (e1, e2) with
| LVar _, LVar _ ->
_l_term_to_string e1 c label ^ " " ^ _l_term_to_string e2 c label
| LVar _, _ ->
_l_term_to_string e1 c label
^ " ("
^ _l_term_to_string e2 c label
^ ")"
| _, LVar _ ->
"("
^ _l_term_to_string e1 c label
^ ") "
^ _l_term_to_string e2 c label
| _, _ ->
"("
^ _l_term_to_string e1 c label
^ ") ("
^ _l_term_to_string e2 c label
^ ")" )
let l_term_to_string term = _l_term_to_string term 0 false
let l_term_with_label_to_string term = _l_term_to_string term 0 true
let rec _trs_term_to_string term pp =
match term with
| TVar v -> v
| TDes (e1, e2) -> (
match (e1, e2) with
| TDes _, TDes _ ->
"(" ^ _trs_term_to_string e1 pp ^ ") (" ^ _trs_term_to_string e2 pp
^ ")"
| TDes _, _ ->
"(" ^ _trs_term_to_string e1 pp ^ ") " ^ _trs_term_to_string e2 pp
| _, TDes _ ->
_trs_term_to_string e1 pp ^ " (" ^ _trs_term_to_string e2 pp ^ ")"
| _, _ -> _trs_term_to_string e1 pp ^ " " ^ _trs_term_to_string e2 pp )
| TCon (l, fvs) ->
let fun_lp x = "(" ^ _trs_term_to_string (fst x) pp ^ ")@" ^ snd x in
let fun_l x = _trs_term_to_string (fst x) pp in
if fvs = [] then l
else if pp then l ^ "[" ^ String.concat "," (L.map fun_lp fvs) ^ "]"