Skip to content

GitLab

Commit 7e671c1a authored by Frontull Samuel's avatar Frontull Samuel
Browse files

code cleanup

parent 0f922eb8
Hide whitespace changes
Inline Side-by-side
Showing with 56 additions and 138 deletions
lib/core.ml
View file @ 7e671c1a
module L = List
open Set
open Util
open Log
......@@ -54,11 +53,11 @@ let rec ctx_to_string = function
let rec _a_term_to_string term =
match term with
| AVar (s, _) -> s
| ALam (((s, vt), t), tp) -> (
| ALam (((s, vt), t), _) -> (
match vt with
| UnT -> "λ" ^ s ^ "." ^ _a_term_to_string t
| _ -> "λ" ^ s ^ "^" ^ typ_to_string vt ^ "." ^ _a_term_to_string t )
| AApp (x, y, tp) -> (
| AApp (x, y, _) -> (
match (x, y) with
| AVar _, AVar _ -> _a_term_to_string x ^ " " ^ _a_term_to_string y
| AVar _, _ -> _a_term_to_string x ^ " (" ^ _a_term_to_string y ^ ")"
......@@ -68,21 +67,6 @@ let rec _a_term_to_string term =
(** Convert a {e a_term} to string *)
let a_term_to_string term = _a_term_to_string term
(* let rec _a_term_to_string2 term =
match term with
| AVar (s, _) -> s
| ALam (((s, vt), t), tp) ->
(String.make 1 '\\') ^ s ^ " -> " ^ _a_term_to_string2 t
| AApp (x, y, tp) -> (
match (x, y) with
| AVar _, AVar _ -> _a_term_to_string2 x ^ " " ^ _a_term_to_string2 y
| AVar _, _ -> _a_term_to_string2 x ^ " (" ^ _a_term_to_string2 y ^ ")"
| _, AVar _ -> "(" ^ _a_term_to_string2 x ^ ") " ^ _a_term_to_string2 y
| _, _ -> "(" ^ _a_term_to_string2 x ^ ") (" ^ _a_term_to_string2 y ^ ")" )
(** Convert a {e a_term} to string *)
let a_term_to_string2 term = _a_term_to_string2 term *)
(** Extract the name of a variable from a {e a_term} *)
let vname = function AVar (n, _) -> n | _ -> ""
......@@ -96,7 +80,7 @@ let rec _assignments tterm =
match tterm with
| AVar (v, t) -> [ (v, t) ]
| ALam ((xs, t), _) -> xs :: _assignments t
| AApp (x, y, t) -> _assignments x @ _assignments y
| AApp (x, y, _) -> _assignments x @ _assignments y
(** Extract all the type assignments in a term attached to a given context *)
let assignments ctx tterm = ctx @ _assignments tterm
......@@ -118,8 +102,8 @@ let order_consistent tterm = _order_consistent (_assignments tterm)
(** Extract the free variables in a {e a_term} *)
let rec free_variables = function
| AVar (x, t) -> [ AVar (x, t) ]
| ALam ((x, e), t) -> remove (free_variables e) vname (fst x)
| AApp (x, y, t) -> free_variables x @ free_variables y
| ALam ((x, e), _) -> remove (free_variables e) vname (fst x)
| AApp (x, y, _) -> free_variables x @ free_variables y
(** Extract the free variables in a list of {e a_term}s *)
let rec free_variables_list = function
......@@ -127,9 +111,9 @@ let rec free_variables_list = function
| x :: xs -> free_variables x @ free_variables_list xs
let rec binders = function
| AVar (x, t) -> []
| ALam ((x, e), t) -> x :: binders e
| AApp (x, y, t) -> binders x @ binders y
| AVar _ -> []
| ALam ((x, e), _) -> x :: binders e
| AApp (x, y, _) -> binders x @ binders y
let rec _safe_naming = function
| [] -> true
......@@ -163,8 +147,8 @@ let rec issafe tterm =
(* Printf.printf "%d %s:%d\n" minord (a_term_to_string tterm) (ord (ttyp tterm)); *)
match tterm with
| AVar _ -> true
| AApp (x, y, typ) -> issafe x && issafe y
| ALam ((vs, st), typ) -> (
| AApp (x, y, _) -> issafe x && issafe y
| ALam ((_, st), typ) -> (
minord >= ord typ
&& match st with AApp (x, y, _) -> issafe x && issafe y | _ -> issafe st )
......@@ -184,9 +168,9 @@ let term_nodes tterm = term_nodes_r tterm "e"
(** Extract the free variables in a {e a_term} *)
let rec _free_variables_pos tterm pos =
match tterm with
| AVar (x, t) -> [ (pos, x) ]
| ALam ((x, y), t) -> remove (_free_variables_pos y (pos ^ "0")) snd (fst x)
| AApp (x, y, t) ->
| AVar (x, _) -> [ (pos, x) ]
| ALam ((x, y), _) -> remove (_free_variables_pos y (pos ^ "0")) snd (fst x)
| AApp (x, y, _) ->
_free_variables_pos x (pos ^ "0") @ _free_variables_pos y (pos ^ "1")
let free_variables_pos tterm = _free_variables_pos tterm "e"
......@@ -201,11 +185,11 @@ let rec b_edges_r tterm pos =
let fvs = _free_variables_pos t (pos ^ "0") in
let vs = fst xs in
let bfvs =
L.map fst (L.filter (fun (p, x) -> if x = vs then true else false) fvs)
L.map fst (L.filter (fun (_, x) -> if x = vs then true else false) fvs)
in
let bpairs = gentuples pos bfvs in
bpairs @ b_edges_r t (pos ^ "0")
| AApp (x, y, typ) -> b_edges_r x (pos ^ "0") @ b_edges_r y (pos ^ "1")
| AApp (x, y, _) -> b_edges_r x (pos ^ "0") @ b_edges_r y (pos ^ "1")
let b_edges tterm = b_edges_r tterm "e"
......@@ -216,19 +200,19 @@ let rec c_edges_r tterm pos =
let fvs = _free_variables_pos t (pos ^ "0") in
let vs = fst xs in
let cfvs =
L.map fst (L.filter (fun (p, x) -> if x = vs then false else true) fvs)
L.map fst (L.filter (fun (_, x) -> if x = vs then false else true) fvs)
in
let cpairs = gentuples pos cfvs in
cpairs @ c_edges_r t (pos ^ "0")
| AApp (x, y, typ) -> c_edges_r x (pos ^ "0") @ c_edges_r y (pos ^ "1")
| AApp (x, y, _) -> c_edges_r x (pos ^ "0") @ c_edges_r y (pos ^ "1")
let c_edges tterm = c_edges_r tterm "e"
let rec a_edges_r tterm pos =
match tterm with
| AVar _ -> []
| ALam ((xs, t), _) -> a_edges_r t (pos ^ "0")
| AApp (x, y, typ) ->
| ALam ((_, t), _) -> a_edges_r t (pos ^ "0")
| AApp (x, y, _) ->
let fvs = L.map fst (_free_variables_pos y (pos ^ "1")) in
let pairs = gentuples pos fvs in
pairs @ a_edges_r x (pos ^ "0") @ a_edges_r y (pos ^ "1")
......@@ -245,7 +229,7 @@ let rec cutlist l n =
| x :: xs, _ -> x :: cutlist xs (n - 1)
let node_tostring = function
| p, AS s, _ -> p ^ "-@"
| p, AS _, _ -> p ^ "-@"
| p, LS vs, _ -> p ^ "-λ" ^ fst vs
| p, VS s, _ -> p ^ "-" ^ s
......@@ -261,17 +245,15 @@ let append_wbp p n =
| Node _ -> Comp [ p; n ]
| Comp xs -> Comp (xs @ [ n ])
(* | Comp xs -> Comp ([p; n]) *)
let rec wbp_tolist = function
| Empty -> []
| Node (pos, sym, typ) -> [ pos ]
| Node (pos, _, _) -> [ pos ]
| Comp [] -> []
| Comp (x :: xs) -> wbp_tolist x @ wbp_tolist (Comp xs)
let rec wbp_tosymlevellist level = function
| Empty -> []
| Node (pos, sym, typ) -> [ (pos, sym, level) ]
| Node (pos, sym, _) -> [ (pos, sym, level) ]
| Comp [] -> []
| Comp (x :: xs) ->
wbp_tosymlevellist (level + 1) x @ wbp_tosymlevellist level (Comp xs)
......@@ -280,18 +262,18 @@ let wbp_tosymlevellist wbp = wbp_tosymlevellist 0 wbp
let rec wbp_tosymlist = function
| Empty -> []
| Node (pos, sym, typ) -> [ (pos, sym) ]
| Node (pos, sym, _) -> [ (pos, sym) ]
| Comp [] -> []
| Comp (x :: xs) -> wbp_tosymlist x @ wbp_tosymlist (Comp xs)
let sym_tostring = function AS s -> "@" | LS vs -> "λ" ^ fst vs | VS s -> s
let sym_tostring = function AS _ -> "@" | LS vs -> "λ" ^ fst vs | VS s -> s
let isapp = function AS _ -> true | _ -> false
let rec _wbp_tostring path flag =
match (path, flag) with
| Empty, _ -> ""
| Node (pos, sym, typ), _ -> sym_tostring sym ^ "-" ^ pos
| Node (pos, sym, _), _ -> sym_tostring sym ^ "-" ^ pos
| Comp _, false -> "[" ^ _wbp_tostring path true ^ "]"
| Comp [], _ -> ""
| Comp [ x ], _ -> _wbp_tostring x false
......@@ -312,7 +294,7 @@ let reverse_wbp p = _reverse_wbp p false
let rec wbp_tail p =
match p with
| Empty -> Empty
| Node (pos, sym, typ) -> Empty
| Node _ -> Empty
| Comp (Node _ :: xs) -> Comp xs
| Comp (x :: xs) -> append_wbp (wbp_tail x) (Comp xs)
| Comp [] -> Empty
......@@ -321,7 +303,7 @@ let rec last_wbp = function
| Empty -> Empty
| Node (pos, sym, typ) -> Node (pos, sym, typ)
| Comp [ x ] -> last_wbp x
| Comp (x :: xs) -> last_wbp (Comp xs)
| Comp (_ :: xs) -> last_wbp (Comp xs)
| _ -> failwith "Wbp wrong."
let rec first_wbp = function
......@@ -333,7 +315,7 @@ let rec first_wbp = function
let rec wbp_length = function
| Empty -> 0
| Node (pos, sym, typ) -> 1
| Node _ -> 1
| Comp [] -> 0
| Comp (x :: xs) -> wbp_length x + wbp_length (Comp xs)
......@@ -372,17 +354,6 @@ let decompose path s e =
let legal = l1 = l2 && w1_l = L.rev w2_l in
legal
(* if not legal then (
Printf.printf "\nl1 (%d): %s\n" l1_idx l1;
Printf.printf "w1 (%d): %s\n" s (wbp_tostring w1);
Printf.printf "cycle: %s\n" (list_tostring (sublist path_l s e) (fun x -> x));
Printf.printf "w2 (%d): %s\n" e (wbp_tostring w2);
Printf.printf "l2 (%d): %s\n\n" l2_idx l2;
legal
)
else
legal *)
let rec find_cycle path pa pb level s e idx =
match path with
| (px, _, lx) :: (py, sy, ly) :: xs ->
......@@ -413,11 +384,8 @@ let check_cycle path = function s, e -> decompose path s e
let is_legal = function
| Empty -> false
| path ->
(* Printf.printf "Checking: %s\n" (wbp_tostring path); *)
let cs = detect_cycles (wbp_tosymlevellist path) 0 in
(* Printf.printf "Cycles found: %d\n" (L.length cs); *)
let legal = L.fold_left ( && ) true (L.map (check_cycle path) cs) in
(* Printf.printf "------------------------------------------------------------------------------------\n\n"; *)
legal
let isvar_node = function Node (_, VS _, _) -> true | _ -> false
......@@ -439,42 +407,33 @@ 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 rec lambda_composition_1 nodes varpath p_list =
(* Printf.printf "\nlambda_composition_1: (%s)\n\n" ((wbp_tostring) varpath); *)
match p_list with
| w :: ws ->
let arg =
posymtyp_to_node (L.hd (get_node (node_pos (first_wbp w) ^ "1") nodes))
in
(* Printf.printf "arg: (%s)\n" (wbp_tostring arg);
Printf.printf "append result: (%s)\n" ((wbp_tostring) (append_wbp (append_wbp varpath (reverse_wbp w)) arg)); *)
append_wbp (append_wbp varpath (reverse_wbp w)) arg
:: lambda_composition_1 nodes varpath ws
| [] -> [ Empty ]
let rec lambda_composition_2 nodes lampath p_list =
(* Printf.printf "\nlambda_composition_2: (%s)\n\n" ((wbp_tostring) lampath); *)
match p_list with
| w :: ws ->
let arg =
posymtyp_to_node
(L.hd (get_node (node_pos (first_wbp lampath) ^ "1") nodes))
in
(* Printf.printf "arg: (%s)\n" (wbp_tostring arg);
Printf.printf "append result: (%s)\n" ((wbp_tostring) (append_wbp (append_wbp w (reverse_wbp lampath)) arg)); *)
append_wbp (append_wbp w (reverse_wbp lampath)) arg
:: lambda_composition_2 nodes lampath ws
| [] -> [ Empty ]
let rec app_composition nodes appapp applam_list =
(* Printf.printf "\app_composition: (%s)\n\n" ((wbp_tostring) p1); *)
match applam_list with
| y :: ys ->
let body =
posymtyp_to_node (L.hd (get_node (node_pos (last_wbp y) ^ "0") nodes))
in
let newpath = append_wbp (append_wbp appapp (wbp_tail y)) body in
(* let newpath = append_wbp (append_wbp (reverse_wbp (wbp_tail (reverse_wbp appapp))) y) body in *)
(* Printf.printf "APP_COMPOSITION\nAA: %s\nAL: %s\nRS: %s\n\n" (wbp_tostring appapp) (wbp_tostring y) (wbp_tostring newpath); *)
newpath :: app_composition nodes appapp ys
| [] -> [ Empty ]
......@@ -672,14 +631,6 @@ let rec subst var fresh term =
ALam ((xsn, subst var fresh e), t)
| AApp (e1, e2, t) -> AApp (subst var fresh e1, subst var fresh e2, t)
(** capture-permitting substitution *)
let rec cpsubst var ex term =
match term with
| AVar (x, t) -> if x = var then ex else term
| ALam ((xs, e), t) ->
if var = fst xs then term else ALam ((xs, cpsubst var ex e), t)
| AApp (e1, e2, t) -> AApp (cpsubst var ex e1, cpsubst var ex e2, t)
let beta_counter = ref 0
let counter = ref 0
......@@ -690,9 +641,8 @@ let next_fresh () =
(** capture-avoiding substitution *)
let rec _casubst var ex term fvex =
(* Printf.printf "_casubst: %s[%s:=%s]\n" (a_term_to_string term) var (a_term_to_string ex); *)
match term with
| AVar (x, t) -> if x = var then ex else term
| AVar (x, _) -> if x = var then ex else term
| ALam ((xs, e), t) ->
if fst xs = var then term
else if L.mem (fst xs) fvex && L.mem var (L.map vname (free_variables e))
......@@ -706,13 +656,12 @@ let rec _casubst var ex term fvex =
AApp (_casubst var ex e1 fvex, _casubst var ex e2 fvex, t)
let casubst var ex term =
(* Printf.printf "casubst: %s[%s:=%s]\n" (a_term_to_string term) var (a_term_to_string ex); *)
_casubst var ex term (L.map vname (free_variables ex))
(** capture-permitting substitution *)
let rec cpsubst var ex term =
match term with
| AVar (x, t) -> if x = var then ex else term
| AVar (x, _) -> if x = var then ex else term
| ALam ((xs, e), t) ->
if fst xs = var then term else ALam ((xs, cpsubst var ex e), t)
| AApp (e1, e2, t) -> AApp (cpsubst var ex e1, cpsubst var ex e2, t)
......@@ -743,10 +692,10 @@ let default_names term = default_names_r term "e"
let rec _subterm_at term pos current =
match term with
| AVar (s, t) -> term
| ALam ((xs, e), t) ->
| AVar _ -> term
| ALam ((_, e), _) ->
if pos = current then term else _subterm_at e pos (current ^ "0")
| AApp (e1, e2, t) ->
| AApp (e1, e2, _) ->
if pos = current then term
else if is_prefix (current ^ "0") pos then
_subterm_at e1 pos (current ^ "0")
......@@ -755,20 +704,16 @@ let rec _subterm_at term pos current =
let subterm_at term pos = _subterm_at term pos "e"
let beta subst term =
(* Printf.printf "beta: %s\n" (a_term_to_string term); *)
beta_counter := !beta_counter + 1;
match term with
| AApp (ALam (((var, _), e1), _), e2, _) ->
(* Printf.printf "subst: %s by %s in %s\n" var (a_term_to_string e2) (a_term_to_string e1); *)
let res = subst var e2 e1 in
(* Printf.printf "res: %s\n" (a_term_to_string res); *)
res
| _ -> failwith "beta: Not a redex."
let rec _reduce_at_pos subst term pos current =
(* Printf.printf "reduce at pos %s, current %s\n" pos current; *)
match term with
| AVar (s, t) -> term
| AVar _ -> term
| ALam ((xs, e), t) ->
ALam ((xs, _reduce_at_pos subst e pos (current ^ "0")), t)
| AApp (e1, e2, t) ->
......@@ -781,7 +726,7 @@ let reduce_at_pos subst term pos = _reduce_at_pos subst term pos "e"
let rec _reduce_lo subst term =
match term with
| AVar (s, t) -> term
| AVar _ -> term
| ALam ((xs, e), t) -> ALam ((xs, _reduce_lo subst e), t)
| AApp (e1, e2, t) -> (
match e1 with
......@@ -793,24 +738,23 @@ let rec _reduce_lo subst term =
let reduce_lo subst term = _reduce_lo subst term
let rec _reduce_lazy subst term =
let _reduce_weak subst term =
match term with
| AVar (s, t) -> term
| ALam ((xs, e), t) -> term
| AVar _ -> term
| ALam _ -> term
| AApp (e1, e2, t) -> (
match e1 with
| ALam _ -> beta subst term
| _ ->
let left = _reduce_lo subst e1 in
if left = e1 then AApp (e1, e2, t)
(* if left = e1 then AApp (e1, _reduce_lo subst e2, t) *)
else AApp (left, e2, t) )
let reduce_lazy subst term = _reduce_lazy subst term
let reduce_weak subst term = _reduce_weak subst term
let rec _reduce_ne subst term =
match term with
| AVar (s, t) -> term
| AVar _ -> term
| ALam ((xs, e), t) -> ALam ((xs, _reduce_ne subst e), t)
| AApp (e1, e2, t) -> (
let right = _reduce_ne subst e2 in
......@@ -829,20 +773,17 @@ let rec _extract_first_redex_pos path =
if pa ^ "0" = pl then [ pa ] else _extract_first_redex_pos xs
| (pl, LS _, _) :: (pa, AS _, _) :: xs ->
if pa ^ "0" = pl then [ pa ] else _extract_first_redex_pos xs
| x :: xs -> _extract_first_redex_pos xs
| _ :: xs -> _extract_first_redex_pos xs
let extract_first_redex_pos path = _extract_first_redex_pos path
let reduce_scc term scc_path =
(* Printf.printf "reduce_scc %s \n" (a_term_to_string term); *)
let rpos = extract_first_redex_pos scc_path in
let subst = casubst in
match rpos with
| [] -> term
| x :: _ ->
(* Printf.printf "Reduce at %s \n" x; *)
let red = reduce_at_pos subst term x in
(* Printf.printf "reduce_scc: %s\n" (a_term_to_string red) ; *)
red
let rec _sn_reduce_to_nf subst term =
......@@ -862,7 +803,6 @@ let reduce_to_nf term max_depth = term :: _reduce_to_nf term max_depth 0
let rec reduce_with_paths term max_depth sim =
let nodes = term_nodes term in
let paths = scc term max_depth sim in
(* Printf.printf "reduce_with_paths: %s %d\n" (a_term_to_string term) (L.length (snd paths)); *)
match paths with
| _, [] -> [ term ]
| _, x :: _ ->
......@@ -885,25 +825,22 @@ let rec sn_reduce_with_paths_to_nf term max_depth sim =
let rec size term =
match term with
| AVar (s, t) -> 0
| ALam ((xs, e), t) -> 1 + size e
| AApp (e1, e2, t) -> 1 + size e1 + size e2
| AVar _ -> 0
| ALam ((_, e), _) -> 1 + size e
| AApp (e1, e2, _) -> 1 + size e1 + size e2
let rec nf subst term =
(* Printf.printf "%d %s\n" (size term) (a_term_to_string term); *)
let new_term = reduce_lo subst term in
if new_term = term then term else nf subst new_term
let rec _nf_arr acc subst term =
(* Printf.printf "%d %s\n" (size term) (a_term_to_string term); *)
let new_term = reduce_lo subst term in
if new_term = term then acc else _nf_arr (acc @ [ new_term ]) subst new_term
let rec nf_arr subst term = _nf_arr [] subst term
let nf_arr subst term = _nf_arr [] subst term
let rec whnf subst term =
(* Printf.printf "%d %s\n" (size term) (a_term_to_string term); *)
let new_term = reduce_lazy subst term in
let new_term = reduce_weak subst term in
if new_term = term then term else whnf subst new_term
let rec _reduce_lo_memo subst term cache =
......@@ -914,7 +851,7 @@ let rec _reduce_lo_memo subst term cache =
| false -> (
Printf.printf "NO Cache hit %s.\n\n" (a_term_to_string term);
match term with
| AVar (s, t) -> term
| AVar _ -> term
| ALam ((xs, e), t) -> ALam ((xs, _reduce_lo_memo subst e cache), t)
| AApp (e1, e2, t) -> (
match e1 with
......@@ -922,10 +859,8 @@ let rec _reduce_lo_memo subst term cache =
| _ ->
let left = _reduce_lo_memo subst e1 cache in
Hashtbl.add cache e1 left;
(* Printf.printf "Cache add %s.\n" (a_term_to_string e1); *)
if left = e1 then (
let arg = _reduce_lo_memo subst e2 cache in
(* Printf.printf "Cache add %s.\n" (a_term_to_string e2); *)
Hashtbl.add cache e2 arg;
AApp (e1, arg, t) )
else AApp (left, e2, t) ) )
......
lib/dot.ml
View file @ 7e671c1a
open Core
module L = List
open Printf
open Util
let node_to_dot pre pos ord s fontcolor =
if ord = "" then
......@@ -20,7 +19,7 @@ let typtofont t =
| _ ->
"<font point-size=\"10\" color=\"gray11\">" ^ typ_to_string t ^ "</font>"
let rec ass_to_string = function v, t -> v ^ typtofont t
let ass_to_string = function v, t -> v ^ typtofont t
(** Transform positive integer to string else empty string *)
let ordtostr o = if o < 0 then "" else string_of_int o
......@@ -70,7 +69,7 @@ let rec term_edges_r tterm pos =
match tterm with
| AVar _ -> []
| ALam ((_, t), _) -> (pos, pos ^ "0") :: term_edges_r t (pos ^ "0")
| AApp (x, y, typ) ->
| AApp (x, y, _) ->
((pos, pos ^ "0") :: (pos, pos ^ "1") :: term_edges_r x (pos ^ "0"))
@ term_edges_r y (pos ^ "1")
......@@ -115,8 +114,6 @@ let _tofont s size color =
let tofont s = _tofont s 12 "gray40"
let itofont i = if i < 0 then "" else " : " ^ tofont (string_of_int i)
let tosup s = tofont ("<sup>" ^ s ^ "</sup>")
let itosup i = if i < 0 then "" else tosup (string_of_int i)
......@@ -170,10 +167,9 @@ let rec _reduction_to_dot pre l i =
let reduction_to_dot pre l = _reduction_to_dot pre l 0
let scc_path_to_dot i path term nodes =
let scc_path_to_dot i path nodes =
let ua = unavoidable_scc path in
if ua then
(* Printf.printf "\n\tUnavoidable chain\n"; *)
"subgraph cluster_paths" ^ string_of_int i
^ " {label=\"Unavoidable\"; color=gray;"
^ _scc_path_to_dot ("p_" ^ string_of_int i) nodes path
......@@ -184,17 +180,17 @@ let scc_path_to_dot i path term nodes =
^ _scc_path_to_dot ("p_" ^ string_of_int i) nodes path
^ "} "
let rec _scc_paths_to_dot i sccpaths term nodes =
let rec _scc_paths_to_dot i sccpaths nodes =
match sccpaths with
| [ [] ] -> ""
| [] -> ""
| x :: xs ->
scc_path_to_dot i x term nodes ^ _scc_paths_to_dot (i + 1) xs term nodes
scc_path_to_dot i x nodes ^ _scc_paths_to_dot (i + 1) xs nodes
let scc_paths_to_dot sccpaths term nodes =
let scc_paths_to_dot sccpaths nodes =
let legend = "" in
"subgraph cluster_allpaths {"
^ _scc_paths_to_dot 0 sccpaths term nodes
^ _scc_paths_to_dot 0 sccpaths nodes
^ legend ^ "} "
(** Generate dot-code *)
......@@ -226,7 +222,7 @@ let term_ctx_to_dot ctx tterm reduction scc_paths name =
^ r_paths_to_dot name (snd (legal_paths tterm 12 true))
^ nodes_order name nodes ^ ctx_str ^ "} " ^ reduction_dot
^ "subgraph cluster_paths { color=invis "
^ scc_paths_to_dot scc_paths tterm nodes
^ scc_paths_to_dot scc_paths nodes
^ " } " ^ "HEADER [shape=\"none\" label=\"\"];}"
let export_term_ctx_dot ctx tterm dir name =
......
lib/dune
View file @ 7e671c1a
(library
(flags (-w))
(name alpha)
(public_name alpha))
......
lib/grammar.mly
View file @ 7e671c1a
%{
open Printf
open Core
open Safe
%}
......
lib/lexer.mll
View file @ 7e671c1a
(* File lexer.mll *)
{
open Grammar (* The type token is defined in parser.mli *)
open Lexing
exception Eof
}
......
lib/util.ml
View file @ 7e671c1a
......@@ -38,7 +38,7 @@ let llast l = L.hd (L.rev l)
let lfst = L.hd
let lsnd = function x :: y :: _ -> y | _ -> failwith "No second element"
let lsnd = function _ :: y :: _ -> y | _ -> failwith "No second element"
let is_prefix pre str =
let len_pre = String.length pre in
......@@ -75,13 +75,6 @@ let rec sublist l s e =
let tail = if e = 0 then [] else sublist xs (s - 1) (e - 1) in
if s > 0 then tail else x :: tail
let is_prefix str1 str2 =
let str1_len = String.length str1 in
if String.length str2 < str1_len then false
else
let pre = String.sub str2 0 str1_len in
pre = str1
let rec duplicates = function
| [] -> false
| hd :: tl -> List.exists (( = ) hd) tl || duplicates tl
lib/util.mli
View file @ 7e671c1a
......@@ -31,9 +31,6 @@ val lfst : 'a list -> 'a
val lsnd : 'a list -> 'a
(** get second element of a list *)
val is_prefix : string -> string -> bool
(** check if first argument is prefix of second *)
val melt_ll : 'a list list -> 'a list list -> 'a list list
val melt_ll_neq : 'a list list -> 'a list list -> 'a list list
......
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