diff --git a/.gitignore b/.gitignore index a9d45b3..6869629 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,10 @@ _build tags +beamer.aux +beamer.log +beamer.nav +beamer.out +beamer.pdf +beamer.snm +beamer.toc +texput.log diff --git a/beamer/beamer.tex b/beamer/beamer.tex index 4cb9ae5..445a780 100644 --- a/beamer/beamer.tex +++ b/beamer/beamer.tex @@ -1,6 +1,5 @@ \documentclass{beamer} \usepackage{tikz} -%\usepackage{minted} \usetikzlibrary{positioning} \usetheme{Darmstadt} @@ -43,42 +42,6 @@ \centering \includegraphics[width=.75\textwidth]{imgs/gadt.png} \end{figure} -%type _ t_var = -% | BVar: ident -> bool t_var -% | IVar: ident -> int t_var -% | RVar: ident -> real t_var -% -%type _ t_expression = -% | EVar: 'a t_var -> 'a t_expression -% | EMonOp: monop * 'a t_expression -> 'a t_expression -% | EBinOp: binop * 'a t_expression * 'a t_expression -> 'a t_expression -% | ETriOp: triop * bool t_expression * 'a t_expression * 'a t_expression -> 'a t_expression -% | EComp: compop * 'a t_expression * 'a t_expression -> bool t_expression -% | EConst: 'a const -> 'a t_expression -% | ETuple: 'a t_expression * 'b t_expression -> ('a * 'b) t_expression -% | EApp: (('a -> 'b) t_node) * 'a t_expression -> 'b t_expression -% -%and _ t_varlist = -% | NVar: 'a t_varlist -% | CVar: 'a t_var * 'b t_varlist -> ('a * 'b) t_varlist -% -%and 'a t_equation = 'a t_varlist * 'a t_expression -% -%and _ t_eqlist = -% | NEql: unit t_eqlist -% | CEql: 'a t_equation * 'b t_eqlist -> ('a * 'b) t_eqlist -% -%and _ t_node = -% | MakeNode: -% ident -% * 'i t_varlist * 'o t_varlist -% * 'l t_varlist * 'e t_eqlist -% -> ('i -> 'o) t_node -% -%type _ t_nodelist = -% | NNode: unit t_nodelist -% | CNode: ('a -> 'b) t_node * 'c t_nodelist -> (('a -> 'b) * 'c) t_nodelist -% \end{minted} \end{frame} \begin{frame} \begin{block}{Pros of using GADTs} @@ -134,7 +97,7 @@ \section{Passes} \begin{frame}{Passes} - \begin{block} + \begin{block}{Classification} The passes of our compiler are functions of taking a program and either: \begin{itemize} \item returning a program if the pass succeeded diff --git a/src/ast.ml b/src/ast.ml index ffa3ef1..fe087cf 100644 --- a/src/ast.ml +++ b/src/ast.ml @@ -69,8 +69,6 @@ and t_node = n_local_vars: t_varlist; n_equations: t_eqlist; n_automata: t_autolist; - n_inputs_type : full_ty; - n_outputs_type : full_ty; } type t_nodelist = t_node list diff --git a/src/main.ml b/src/main.ml index 6edbada..c1334ea 100644 --- a/src/main.ml +++ b/src/main.ml @@ -25,7 +25,8 @@ let exec_passes ast main_fn verbose debug passes f = let _ = (** Usage and argument parsing. *) - let default_passes = ["chkvar_init_unicity"; "pre2vars"; "linearization"] in + let default_passes = ["pre2vars"; "linearization"; "equations_ordering"] in + let sanity_passes = ["chkvar_init_unicity"; "check_typing"] in let usage_msg = "Usage: main [-passes p1,...,pn] [-ast] [-verbose] [-debug] \ [-o output_file] [-m main_function] source_file\n" in @@ -37,10 +38,14 @@ let _ = let passes = ref [] in let main_fn = ref "main" in let source_file = ref "" in + let testopt = ref false in let output_file = ref "out.c" in let anon_fun filename = source_file := filename in let speclist = [ + ("-test", Arg.Set testopt, "Runs the sanity passes not only at the \ + begining of the compilation, but also after \ + each pass altering the AST."); ("-ast", Arg.Set ppast, "Only print the AST of the input file"); ("-nop", Arg.Set nopopt, "Only computes the AST and execute the passes"); ("-verbose", Arg.Set verbose, "Output some debug information"); @@ -66,6 +71,8 @@ let _ = ("pre2vars", Passes.pre2vars); ("chkvar_init_unicity", Passes.chkvar_init_unicity); ("linearization", Passes.pass_linearization); + ("equations_ordering", Passes.pass_eq_reordering); + ("check_typing", Passes.pass_typing); ]; (** Main functionality below *) @@ -99,12 +106,19 @@ let _ = end in - let passes = List.map (fun (pass: string) -> (pass, - match Hashtbl.find_opt passes_table pass with - | None -> - (exit_error (Format.sprintf "The pass %s does not exist.\n" pass); exit 0) - | Some f -> - (print_debug ("The pass "^pass^" has been selected.\n"); f))) !passes in + let passes = + List.map + (fun (pass: string) -> (pass, + match Hashtbl.find_opt passes_table pass with + | None -> + (exit_error (Format.sprintf "The pass %s does not exist.\n" pass); exit 0) + | Some f -> + (print_debug ("The pass "^pass^" has been selected.\n"); f))) + (sanity_passes @ + if !testopt + then List.flatten (List.map (fun p -> p :: sanity_passes) !passes) + else !passes) + in print_debug (Format.asprintf "Initial AST (before executing any passes):\n%a" Pp.pp_ast ast) ; diff --git a/src/parser.mly b/src/parser.mly index 3d39a12..4722140 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -198,9 +198,7 @@ node_content: n_outputs = (t_out, e_out); n_local_vars = $10; n_equations = eqs; - n_automata = aut; - n_inputs_type = t_in; - n_outputs_type = t_out; } in + n_automata = aut; } in if Hashtbl.find_opt defined_nodes node_name <> None then raise (MyParsingError (Format.asprintf "The node %s is already defined." @@ -386,8 +384,8 @@ expr: { let name = $1 in let node = fetch_node name in let args = $3 in - if type_exp args = node.n_inputs_type - then EApp (node.n_outputs_type, fetch_node name, args) + if type_exp args = fst node.n_inputs + then EApp (fst node.n_outputs, fetch_node name, args) else raise (MyParsingError ("The application does not type check!", current_location())) } diff --git a/src/passes.ml b/src/passes.ml index bbb7b19..52f3bbf 100644 --- a/src/passes.ml +++ b/src/passes.ml @@ -2,6 +2,7 @@ open Ast open Passes_utils +open Utils let pre2vars verbose debug main_fn = let rec all_pre expr = @@ -13,181 +14,285 @@ let pre2vars verbose debug main_fn = in let rec pre_push expr : t_expression = match expr with - | EVar _ -> EMonOp (Utils.type_exp expr, MOp_pre, expr) + | EVar _ -> EMonOp (type_exp expr, MOp_pre, expr) | EConst _ -> expr (** pre(c) = c for any constant c *) | EMonOp (ty, mop, expr) -> begin match mop with - | MOp_pre -> - if all_pre expr - then EMonOp (ty, mop, EMonOp (ty, mop, expr)) - else pre_push (pre_push expr) - | _ -> EMonOp (ty, mop, pre_push expr) - end - | EBinOp (ty, bop, expr, expr') -> - let expr = pre_push expr in let expr' = pre_push expr' in - EBinOp (ty, bop, expr, expr') - | ETriOp (ty, top, expr, expr', expr'') -> - let expr = pre_push expr in let expr' = pre_push expr' in - let expr'' = pre_push expr'' in - ETriOp (ty, top, expr, expr', expr'') - | EComp (ty, cop, expr, expr') -> - let expr = pre_push expr in let expr' = pre_push expr' in - EComp (ty, cop, expr, expr') - | EWhen (ty, expr, expr') -> - let expr = pre_push expr in let expr' = pre_push expr' in - EWhen (ty, expr, expr') - | EReset (ty, expr, expr') -> - let expr = pre_push expr in let expr' = pre_push expr' in - EReset (ty, expr, expr') - | ETuple (ty, elist) -> - let elist = - List.fold_right (fun expr acc -> (pre_push expr) :: acc) elist [] in - ETuple (ty, elist) - | EApp (ty, node, arg) -> - let arg = pre_push arg in - EApp (ty, node, arg) - in - let rec aux (expr: t_expression) = - match expr with - | EVar _ -> expr - | EMonOp (ty, mop, expr) -> - begin - match mop with - | MOp_pre -> pre_push expr - | _ -> let expr = aux expr in EMonOp (ty, mop, expr) - end - | EBinOp (ty, bop, expr, expr') -> - let expr = aux expr in let expr' = aux expr' in - EBinOp (ty, bop, expr, expr') - | ETriOp (ty, top, expr, expr', expr'') -> - let expr = aux expr in let expr' = aux expr' in - let expr'' = aux expr'' in - ETriOp (ty, top, expr, expr', expr'') - | EComp (ty, cop, expr, expr') -> - let expr = aux expr in let expr' = aux expr' in - EComp (ty, cop, expr, expr') - | EWhen (ty, expr, expr') -> - let expr = aux expr in let expr' = aux expr' in - EWhen (ty, expr, expr') - | EReset (ty, expr, expr') -> - let expr = aux expr in let expr' = aux expr' in - EReset (ty, expr, expr') - | EConst (ty, c) -> EConst (ty, c) - | ETuple (ty, elist) -> - let elist = - List.fold_right (fun expr acc -> (aux expr) :: acc) elist [] in - ETuple (ty, elist) - | EApp (ty, node, arg) -> - let arg = aux arg in - EApp (ty, node, arg) - in - expression_pass (Utils.somify aux) + | MOp_pre -> + if all_pre expr + then EMonOp (ty, mop, EMonOp (ty, mop, expr)) + else pre_push (pre_push expr) + | _ -> EMonOp (ty, mop, pre_push expr) + end + | EBinOp (ty, bop, expr, expr') -> + let expr = pre_push expr in let expr' = pre_push expr' in + EBinOp (ty, bop, expr, expr') + | ETriOp (ty, top, expr, expr', expr'') -> + let expr = pre_push expr in let expr' = pre_push expr' in + let expr'' = pre_push expr'' in + ETriOp (ty, top, expr, expr', expr'') + | EComp (ty, cop, expr, expr') -> + let expr = pre_push expr in let expr' = pre_push expr' in + EComp (ty, cop, expr, expr') + | EWhen (ty, expr, expr') -> + let expr = pre_push expr in let expr' = pre_push expr' in + EWhen (ty, expr, expr') + | EReset (ty, expr, expr') -> + let expr = pre_push expr in let expr' = pre_push expr' in + EReset (ty, expr, expr') + | ETuple (ty, elist) -> + let elist = + List.fold_right (fun expr acc -> (pre_push expr) :: acc) elist [] in + ETuple (ty, elist) + | EApp (ty, node, arg) -> + let arg = pre_push arg in + EApp (ty, node, arg) +in +let rec aux (expr: t_expression) = + match expr with + | EVar _ -> expr + | EMonOp (ty, mop, expr) -> + begin + match mop with + | MOp_pre -> pre_push expr + | _ -> let expr = aux expr in EMonOp (ty, mop, expr) + end + | EBinOp (ty, bop, expr, expr') -> + let expr = aux expr in let expr' = aux expr' in + EBinOp (ty, bop, expr, expr') + | ETriOp (ty, top, expr, expr', expr'') -> + let expr = aux expr in let expr' = aux expr' in + let expr'' = aux expr'' in + ETriOp (ty, top, expr, expr', expr'') + | EComp (ty, cop, expr, expr') -> + let expr = aux expr in let expr' = aux expr' in + EComp (ty, cop, expr, expr') + | EWhen (ty, expr, expr') -> + let expr = aux expr in let expr' = aux expr' in + EWhen (ty, expr, expr') + | EReset (ty, expr, expr') -> + let expr = aux expr in let expr' = aux expr' in + EReset (ty, expr, expr') + | EConst (ty, c) -> EConst (ty, c) + | ETuple (ty, elist) -> + let elist = + List.fold_right (fun expr acc -> (aux expr) :: acc) elist [] in + ETuple (ty, elist) + | EApp (ty, node, arg) -> + let arg = aux arg in + EApp (ty, node, arg) +in +expression_pass (somify aux) let chkvar_init_unicity verbose debug main_fn : t_nodelist -> t_nodelist option = - let aux (node: t_node) : t_node option = - let incr_aux h n = - match Hashtbl.find_opt h n with - | None -> failwith "todo, should not happend." - | Some num -> Hashtbl.replace h n (num + 1) - in - let incr_eq h (((_, patt), _): t_equation) = - List.iter (fun v -> incr_aux h (Utils.name_of_var v)) patt - in - let rec incr_eqlist h = function - | [] -> () - | eq :: eqs -> (incr_eq h eq; incr_eqlist h eqs) - in - let incr_branch h (State (_, eqs, _, _): t_state) = incr_eqlist h eqs in - let incr_automata h ((_, states): t_automaton) = - let acc = Hashtbl.copy h in - List.iter - (fun st -> - let h_st = Hashtbl.copy h in - incr_branch h_st st; - Hashtbl.iter - (fun varname num' -> - match Hashtbl.find_opt acc varname with - | None -> failwith "non!" - | Some num -> Hashtbl.replace acc varname (Int.max num num') - ) h_st) states; - Hashtbl.iter (fun v n -> Hashtbl.replace h v n) acc - in - let check_now h : bool= - Hashtbl.fold - (fun varname num old_res -> - if num > 1 - then (verbose (Format.asprintf "%s initialized twice!" varname); false) - else old_res) h true - in - (*let purge_initialized h = - Hashtbl.iter - (fun varname num -> - if num > 0 - then (verbose (Format.asprintf "Purging %s" varname); Hashtbl.remove h varname) - else ()) h - in*) - let h = Hashtbl.create Config.maxvar in - let add_var n v = - match v with - | IVar s -> Hashtbl.add h s n - | BVar s -> Hashtbl.add h s n - | RVar s -> Hashtbl.add h s n +let aux (node: t_node) : t_node option = + let incr_aux h n = + match Hashtbl.find_opt h n with + | None -> failwith "todo, should not happend." + | Some num -> Hashtbl.replace h n (num + 1) in - let add_var_in = add_var 1 in - let add_var_loc = add_var 0 in - List.iter add_var_in (snd node.n_inputs); - List.iter add_var_loc (snd node.n_outputs); - List.iter add_var_loc (snd node.n_local_vars); - (** Usual Equations *) - incr_eqlist h node.n_equations; - if check_now h = false - then None - else - begin - List.iter (* 0. *) (incr_automata h) node.n_automata; - if check_now h - then Some node - else None - end - (** never purge -> failwith never executed! purge_initialized h; *) + let incr_eq h (((_, patt), _): t_equation) = + List.iter (fun v -> incr_aux h (name_of_var v)) patt + in + let rec incr_eqlist h = function + | [] -> () + | eq :: eqs -> (incr_eq h eq; incr_eqlist h eqs) + in + let incr_branch h (State (_, eqs, _, _): t_state) = incr_eqlist h eqs in + let incr_automata h ((_, states): t_automaton) = + let acc = Hashtbl.copy h in + List.iter + (fun st -> + let h_st = Hashtbl.copy h in + incr_branch h_st st; + Hashtbl.iter + (fun varname num' -> + match Hashtbl.find_opt acc varname with + | None -> failwith "non!" + | Some num -> Hashtbl.replace acc varname (Int.max num num') + ) h_st) states; + Hashtbl.iter (fun v n -> Hashtbl.replace h v n) acc + in + let check_now h : bool= + Hashtbl.fold + (fun varname num old_res -> + if num > 1 + then (verbose (Format.asprintf "%s initialized twice!" varname); false) + else old_res) h true + in + (*let purge_initialized h = + Hashtbl.iter + (fun varname num -> + if num > 0 + then (verbose (Format.asprintf "Purging %s" varname); Hashtbl.remove h varname) + else ()) h + in*) + let h = Hashtbl.create Config.maxvar in + let add_var n v = + match v with + | IVar s -> Hashtbl.add h s n + | BVar s -> Hashtbl.add h s n + | RVar s -> Hashtbl.add h s n in - node_pass aux + let add_var_in = add_var 1 in + let add_var_loc = add_var 0 in + List.iter add_var_in (snd node.n_inputs); + List.iter add_var_loc (snd node.n_outputs); + List.iter add_var_loc (snd node.n_local_vars); + (** Usual Equations *) + incr_eqlist h node.n_equations; + if check_now h = false + then None + else + begin + List.iter (* 0. *) (incr_automata h) node.n_automata; + if check_now h + then Some node + else None + end + (** never purge -> failwith never executed! purge_initialized h; *) +in +node_pass aux let pass_linearization verbose debug main_fn = - let node_lin (node: t_node): t_node option = - let rec tpl ((pat, exp): t_equation) = - match exp with - | ETuple (_, hexps :: texps) -> - let p1, p2 = - Utils.list_select - (List.length (Utils.type_exp hexps)) - (snd pat) in - let t1 = List.flatten (List.map Utils.type_var p1) in - let t2 = List.flatten (List.map Utils.type_var p2) in - ((t1, p1), hexps) - :: (tpl ((t2, p2), - ETuple (List.flatten (List.map Utils.type_exp texps), texps))) - | ETuple (_, []) -> [] - | _ -> [(pat, exp)] - in - let new_locvars = node.n_local_vars in - let new_equations = List.flatten - begin - List.map - tpl - node.n_equations - end in - Some - { - n_name = node.n_name; - n_inputs = node.n_inputs; - n_outputs = node.n_outputs; - n_local_vars = new_locvars; - n_equations = new_equations; - n_automata = node.n_automata; - n_inputs_type = node.n_inputs_type; - n_outputs_type = node.n_outputs_type; - } +let node_lin (node: t_node): t_node option = + let rec tpl ((pat, exp): t_equation) = + match exp with + | ETuple (_, hexps :: texps) -> + debug "An ETuple has been recognized, inlining..."; + let p1, p2 = + list_select + (List.length (type_exp hexps)) + (snd pat) in + let t1 = List.flatten (List.map type_var p1) in + let t2 = List.flatten (List.map type_var p2) in + ((t1, p1), hexps) + :: (tpl ((t2, p2), + ETuple (List.flatten (List.map type_exp texps), texps))) + | ETuple (_, []) -> [] + | _ -> [(pat, exp)] in - node_pass node_lin + let new_locvars = node.n_local_vars in + let new_equations = List.flatten + begin + List.map + tpl + node.n_equations + end in + Some + { + n_name = node.n_name; + n_inputs = node.n_inputs; + n_outputs = node.n_outputs; + n_local_vars = new_locvars; + n_equations = new_equations; + n_automata = node.n_automata; + } +in +node_pass node_lin + +let pass_eq_reordering verbose debug main_fn ast = +let rec pick_equations init_vars eqs remaining_equations = + match remaining_equations with + | [] -> Some eqs + | _ -> + begin + match List.filter + (fun (patt, expr) -> + List.for_all + (fun v -> List.mem v init_vars) + (vars_of_expr expr)) + remaining_equations with + | [] -> raise (PassExn "[equation ordering] The equations cannot be ordered.") + | h :: t -> + let init_vars = + List.fold_left + (fun acc vs -> + acc @ (vars_of_patt (fst vs))) init_vars (h :: t) in + pick_equations init_vars (eqs@(h :: t)) + (List.filter (fun eq -> List.for_all (fun e -> eq <> e) (h :: t)) remaining_equations) + end + in +let node_eq_reorganising (node: t_node): t_node option = + let init_vars = List.map name_of_var (snd node.n_inputs) in + try + begin + match pick_equations init_vars [] node.n_equations with + | None -> None + | Some eqs -> Some { node with n_equations = eqs } + end + with PassExn err -> (verbose err; None) +in +node_pass node_eq_reorganising ast + +let pass_typing verbose debug main_fn ast = + let htbl = Hashtbl.create (List.length ast) in + let () = debug "[typing verification]" in + let () = List.iter + (fun n -> Hashtbl.add htbl n.n_name (fst n.n_inputs, fst n.n_outputs)) + ast in + let rec check_varlist vl = + let t = fst vl in + let l = snd vl in + match t, l with + | [], [] -> true + | TInt :: t, IVar _ :: l -> check_varlist (t, l) + | TBool :: t, BVar _ :: l -> check_varlist (t, l) + | TReal :: t, RVar _ :: l -> check_varlist (t, l) + | _, _ -> false + in + let rec check_expr vl = function + | EVar (t, v) -> t = type_var v + | EMonOp (t, _, e) -> check_expr vl e && type_exp e = t + | EBinOp (t, _, e, e') -> check_expr vl e && check_expr vl e' + && t = type_exp e && t = type_exp e' + | ETriOp (t, _, c, e, e') -> + check_expr vl e && check_expr vl e' && check_expr vl c + && type_exp c = [TBool] && type_exp e = t && type_exp e' = t + | EComp (t, _, e, e') -> + check_expr vl e && check_expr vl e' && t = [TBool] + | EWhen (t, e, e') -> + check_expr vl e && check_expr vl e' + && t = type_exp e && [TBool] = type_exp e' + | EReset (t, e, e') -> + check_expr vl e && check_expr vl e' && t = type_exp e && type_exp e' = [TBool] + | EConst (t, c) -> type_const c = t + | ETuple (t, l) -> + List.for_all (check_expr vl) l + && t = List.flatten (List.map type_exp l) + | EApp (t, n, e) -> + check_expr vl e && t = (fst n.n_outputs) && type_exp e = (fst n.n_inputs) + in + let check_equation vl ((peq, eeq): t_equation) = + if check_varlist peq + then + if check_expr vl eeq + then fst peq = type_exp eeq + else false + else false + in + let rec check_equations vl = function + | [] -> true + | eq :: eqs -> + if check_equation vl eq + then check_equations vl eqs + else false + in + let check_one_node node = + check_varlist (node.n_inputs) + && check_varlist (node.n_outputs) + && check_varlist (node.n_local_vars) + && check_equations + (varlist_concat node.n_inputs + (varlist_concat node.n_outputs node.n_local_vars)) + node.n_equations + in + let rec aux = function + | [] -> Some ast + | n :: nodes -> + if check_one_node n + then aux nodes + else None + in aux ast + diff --git a/src/passes_utils.ml b/src/passes_utils.ml index 5848189..0e159d9 100644 --- a/src/passes_utils.ml +++ b/src/passes_utils.ml @@ -18,8 +18,6 @@ let equation_pass (f: t_equation -> t_equation option) ast: t_nodelist option = n_local_vars = node.n_local_vars; n_equations = eqs; n_automata = node.n_automata; - n_inputs_type = node.n_inputs_type; - n_outputs_type = node.n_outputs_type; } in node_pass aux ast @@ -31,3 +29,5 @@ let expression_pass f: t_nodelist -> t_nodelist option = | Some expr -> Some (patt, expr) in equation_pass aux + +exception PassExn of string diff --git a/src/pp.ml b/src/pp.ml index 378cd65..11aa484 100644 --- a/src/pp.ml +++ b/src/pp.ml @@ -136,7 +136,8 @@ let pp_expression = let rec pp_equations fmt: t_eqlist -> unit = function | [] -> () | (patt, expr) :: eqs -> - Format.fprintf fmt "\t\t∗ Equation of type : %a\n\t\t left side: %a\n\t\t right side:\n%a\n%a" + Format.fprintf fmt "\t\t∗ Equation of type : %a\n\t\t left side: %a\n\ + \t\t right side:\n%a\n\n%a" debug_type_pp (Utils.type_exp expr) pp_varlist patt pp_expression expr diff --git a/src/test.node b/src/test.node index 5b65c18..9200b38 100644 --- a/src/test.node +++ b/src/test.node @@ -1,4 +1,5 @@ node diagonal_int (i: int) returns (o1, o2 : int); +let i: int; let (o1, o2) = (i, i); tel diff --git a/src/test2.node b/src/test2.node index 58ac619..36209a1 100644 --- a/src/test2.node +++ b/src/test2.node @@ -1,4 +1,7 @@ node diagonal_int (i: int) returns (o1, o2 : int); +var y: int; let - (o1, o2) = (i, i); + o2 = y; + y = i; + o1 = i; tel diff --git a/src/utils.ml b/src/utils.ml index afadb9f..fa769a1 100644 --- a/src/utils.ml +++ b/src/utils.ml @@ -22,7 +22,12 @@ let rec list_chk v = function | [] -> false | h :: t -> if h = v then true else list_chk v t -exception MyParsingError of (string * Ast.location) +exception MyParsingError of (string * location) + +let type_const = function + | CReal _ -> [TReal] + | CInt _ -> [TInt ] + | CBool _ -> [TBool] let type_var (v: t_var) = match v with @@ -60,3 +65,23 @@ let rec fresh_var_name (l: t_varlist) n : ident = if List.filter (fun v -> name_of_var v = name) (snd l) = [] then name else fresh_var_name l n + +let vars_of_patt patt = List.map name_of_var (snd patt) + +let rec vars_of_expr (expr: t_expression) : ident list = + match expr with + | EConst _ -> [] + | EVar (_, v) -> [name_of_var v] + (** pre (e) does not rely on anything in this round *) + | EMonOp (_, MOp_pre, _) -> [] + | EApp (_, _, e) | EMonOp (_, _, e) -> vars_of_expr e + | EComp (_, _, e, e') | EReset (_, e, e') | EBinOp (_, _, e, e') + | EWhen (_, e, e') -> + (vars_of_expr e) @ (vars_of_expr e') + | ETriOp (_, _, e, e', e'') -> + (vars_of_expr e) @ (vars_of_expr e') @ (vars_of_expr e'') + | ETuple (_, l) -> List.flatten (List.map vars_of_expr l) + +let rec varlist_concat (l1: t_varlist) (l2: t_varlist): t_varlist = + (fst l1 @ fst l2, snd l1 @ snd l2) +