summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Makefile5
-rw-r--r--abstract/abs_interp.ml85
-rw-r--r--abstract/transform.ml58
-rw-r--r--frontend/ast_printer.ml12
-rw-r--r--frontend/ast_util.ml (renamed from interpret/ast_util.ml)25
-rw-r--r--frontend/rename.ml (renamed from interpret/rename.ml)3
-rw-r--r--frontend/typing.ml178
-rw-r--r--interpret/interpret.ml24
-rw-r--r--main.ml6
9 files changed, 270 insertions, 126 deletions
diff --git a/Makefile b/Makefile
index 7645849..6386a97 100644
--- a/Makefile
+++ b/Makefile
@@ -8,6 +8,9 @@ SRC= main.ml \
frontend/parser.mly \
frontend/lexer.mll \
frontend/ast_printer.ml \
+ frontend/typing.ml \
+ frontend/ast_util.ml \
+ frontend/rename.ml \
abstract/formula.ml \
abstract/formula_printer.ml \
abstract/transform.ml \
@@ -17,8 +20,6 @@ SRC= main.ml \
abstract/nonrelational.ml \
abstract/intervals_domain.ml \
interpret/interpret.ml \
- interpret/ast_util.ml \
- interpret/rename.ml
all: $(BIN)
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index 00f7fad..c621734 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -1,6 +1,7 @@
open Ast
open Ast_util
open Formula
+open Typing
open Util
open Environment_domain
@@ -9,15 +10,13 @@ module I (E : ENVIRONMENT_DOMAIN) : sig
type st
- val do_prog : int -> prog -> id -> unit
+ val do_prog : int -> rooted_prog -> unit
end = struct
type st = {
- p : prog;
+ rp : rooted_prog;
widen_delay : int;
- root_scope : scope;
- all_vars : var_def list;
env : E.t;
f : bool_expr;
cl : conslist;
@@ -27,75 +26,29 @@ end = struct
}
- let node_vars p f nid =
- let (n, _) = find_node_decl p f in
- List.map (fun (p, id, t) -> p, nid^"/"^id, t)
- (n.args @ n.ret @ n.var)
- (*
- extract_all_vars : prog -> scope -> var_decl list
-
- Extracts all variables with names given according to
- naming convention used here and in transform.ml :
- - pre variables are not prefixed by scope
- - next values for variables are prefixed by capital N
- *)
- let rec extract_all_vars p (node, prefix, eqs) =
- let vars_of_expr e =
- List.flatten
- (List.map
- (fun (f, id, eqs, args) ->
- node_vars p f (node^"/"^id) @
- extract_all_vars p (node^"/"^id, "", eqs))
- (extract_instances p e))
- @
- List.flatten
- (List.map
- (fun (id, _) -> [false, id, AST_TINT; false, "N"^id, AST_TINT])
- (* TODO : type of pre value ? *)
- (extract_pre e))
- in
- let vars_of_eq e = match fst e with
- | AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) -> vars_of_expr e
- | AST_activate (b, _) ->
- let rec do_branch = function
- | AST_activate_body b ->
- List.map (fun (p, id, t) -> p, node^"/"^id, t) b.act_locals
- @
- extract_all_vars p (node, b.act_id^".", b.body)
- | AST_activate_if(c, a, b) ->
- vars_of_expr c @ do_branch a @ do_branch b
- in do_branch b
- | AST_automaton _ -> not_implemented "extract_all vars automaton"
- in
- (false, node^"/"^prefix^"time", AST_TINT)::
- (false, "N"^node^"/"^prefix^"time", AST_TINT)::
- (List.flatten (List.map vars_of_eq eqs))
(* init state *)
- let init_state widen_delay p root =
- let root_scope = get_root_scope p root in
-
- let f = Formula.eliminate_not (Transform.f_of_prog p root false) in
+ let init_state widen_delay rp =
+ let f = Formula.eliminate_not (Transform.f_of_prog rp false) in
let cl = Formula.conslist_of_f f in
- let f_g = Formula.eliminate_not (Transform.f_of_prog p root true) in
+ let f_g = Formula.eliminate_not (Transform.f_of_prog rp true) in
let cl_g = Formula.conslist_of_f f_g in
- let all_vars = node_vars p root "" @ extract_all_vars p root_scope in
let env = List.fold_left
(fun env (_, id, ty) ->
- E.addvar env id (ty = AST_TREAL))
+ E.addvar env id (ty = TReal))
E.init
- all_vars
+ rp.all_vars
in
- let init_f = Transform.init_f_of_prog p root in
- let guarantees = Transform.guarantees_of_prog p root in
+ let init_f = Transform.init_f_of_prog rp in
+ let guarantees = Transform.guarantees_of_prog rp in
Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f;
Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f;
Format.printf "Cycle formula with guarantees:@.%a@.@." Formula_printer.print_expr f_g;
- Format.printf "Vars: @[<hov>%a@]@.@." (Ast_printer.print_list Ast_printer.print_var_decl ", ") all_vars;
+ Format.printf "Vars: @[<hov>%a@]@.@." (Ast_printer.print_list Ast_printer.print_typed_var ", ") rp.all_vars;
Format.printf "Guarantees:@.";
List.iter (fun (id, f) ->
@@ -105,9 +58,9 @@ end = struct
let env = E.apply_f env init_f in
- { p; root_scope; widen_delay;
+ { rp; widen_delay;
f; cl; f_g; cl_g;
- guarantees; all_vars; env }
+ guarantees; env }
(*
pass_cycle : var_def list -> E.t -> E.t
@@ -138,7 +91,7 @@ end = struct
(* cycle : st -> cl -> env -> env *)
let cycle st cl i =
- (pass_cycle st.all_vars (E.apply_cl i cl))
+ (pass_cycle st.rp.all_vars (E.apply_cl i cl))
(*
loop : st -> env -> env -> env
@@ -173,10 +126,10 @@ end = struct
y, z
(*
- do_prog : prog -> id -> unit
+ do_prog : rooted_prog -> unit
*)
- let do_prog widen_delay p root =
- let st = init_state widen_delay p root in
+ let do_prog widen_delay rp =
+ let st = init_state widen_delay rp in
let pnew = st.env in
let pnew_c = E.apply_cl pnew st.cl in
@@ -209,13 +162,13 @@ end = struct
Format.printf "@]@."
end;
- if List.exists (fun (p, _, _) -> p) st.all_vars then begin
+ if List.exists (fun (p, _, _) -> p) st.rp.all_vars then begin
Format.printf "Probes:@[<v>";
List.iter (fun (p, id, _) ->
if p then Format.printf " %a ∊ %a@ "
Formula_printer.print_id id
E.print_itv (E.var_itv final id))
- st.all_vars;
+ st.rp.all_vars;
Format.printf "@]@."
end
diff --git a/abstract/transform.ml b/abstract/transform.ml
index 25e4b43..890f598 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -2,6 +2,7 @@ open Ast
open Util
open Ast_util
open Formula
+open Typing
open Interpret (* used for constant evaluation ! *)
@@ -12,9 +13,8 @@ open Interpret (* used for constant evaluation ! *)
type scope = id * id * eqn ext list
type transform_data = {
- p : Ast.prog;
+ rp : rooted_prog;
consts : I.value VarMap.t;
- root_scope : scope;
(* future : the automata state *)
}
@@ -47,7 +47,9 @@ let rec f_of_nexpr td (node, prefix) where expr =
| _ -> invalid_arity "binary_operator") b
| _ -> invalid_arity "binary operator") a
(* temporal *)
- | AST_pre(_, id) -> where [NIdent id]
+ | AST_pre(expr, id) ->
+ let typ = type_expr td.rp node expr in
+ where (List.mapi (fun i _ -> NIdent (id^"."^(string_of_int i))) typ)
| AST_arrow(a, b) ->
f_or
(f_and (BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0))
@@ -60,7 +62,7 @@ let rec f_of_nexpr td (node, prefix) where expr =
(f_and (f_of_expr td (node, prefix) c) (sub where a))
(f_and (BNot(f_of_expr td (node, prefix) c)) (sub where b))
| AST_instance ((f, _), args, nid) ->
- let (n, _) = find_node_decl td.p f in
+ let (n, _) = find_node_decl td.rp.p f in
where (List.map (fun (_, id, _) -> NIdent (node^"/"^nid^"/"^id)) n.ret)
(* boolean values treated as integers *)
@@ -140,16 +142,22 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
eq
in
let eq = List.fold_left (fun x i -> f_and (instance_eq i) x)
- eq (extract_instances td.p e)
+ eq (extract_instances td.rp.p e)
in
let pre_expr (id, expr) =
if active then
- f_of_nexpr td (node, prefix) (function
- | [v] -> BRel(AST_EQ, NIdent("N"^id), v)
- | _ -> invalid_arity "pre on complex data not supported")
+ f_of_nexpr td (node, prefix) (fun elist ->
+ list_fold_op f_and
+ (List.mapi
+ (fun i v -> BRel(AST_EQ, NIdent("N"^id^"."^(string_of_int i)), v))
+ elist))
expr
else
- BRel(AST_EQ, NIdent("N"^id), NIdent id)
+ let typ = type_expr td.rp node expr in
+ list_fold_op f_and
+ (List.mapi
+ (fun i _ -> let x = string_of_int i in BRel(AST_EQ, NIdent("N"^id^"."^x), NIdent (id^"."^x)))
+ typ)
in
List.fold_left (fun x i -> f_and (pre_expr i) x)
eq (extract_pre e)
@@ -224,25 +232,24 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
time_incr_eq
(List.map do_eq eqs)
-and f_of_prog p root assume_guarantees =
+and f_of_prog rp assume_guarantees =
let td = {
- root_scope = get_root_scope p root;
- p = p;
- consts = I.consts p root;
+ rp = rp;
+ consts = I.consts rp;
} in
- f_of_scope true td td.root_scope assume_guarantees
+ f_of_scope true td td.rp.root_scope assume_guarantees
(*
Translate init state into a formula
*)
-let rec init_f_of_scope p (node, prefix, eqs) =
+let rec init_f_of_scope rp (node, prefix, eqs) =
let expr_eq e =
let instance_eq (_, id, eqs, args) =
- init_f_of_scope p (node^"/"^id, "", eqs)
+ init_f_of_scope rp (node^"/"^id, "", eqs)
in
List.fold_left (fun x i -> f_and (instance_eq i) x)
- (BConst true) (extract_instances p e)
+ (BConst true) (extract_instances rp.p e)
in
let do_eq eq = match fst eq with
| AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) ->
@@ -250,7 +257,7 @@ let rec init_f_of_scope p (node, prefix, eqs) =
| AST_activate (b, _) ->
let rec cond_eq = function
| AST_activate_body b ->
- init_f_of_scope p (node, b.act_id^".", b.body)
+ init_f_of_scope rp (node, b.act_id^".", b.body)
| AST_activate_if(c, a, b) ->
f_and (expr_eq c)
(f_and (cond_eq a) (cond_eq b))
@@ -265,8 +272,8 @@ let rec init_f_of_scope p (node, prefix, eqs) =
in
List.fold_left f_and time_eq (List.map do_eq eqs)
-and init_f_of_prog p root =
- init_f_of_scope p (get_root_scope p root)
+and init_f_of_prog rp =
+ init_f_of_scope rp rp.root_scope
(*
Get expressions for guarantee violation
@@ -277,7 +284,7 @@ let rec g_of_scope td (node, prefix, eqs) cond =
g_of_scope td (node^"/"^id, "", eqs) cond
in
List.fold_left (fun x i -> (instance_g i) @ x)
- [] (extract_instances td.p e)
+ [] (extract_instances td.rp.p e)
in
let do_eq eq = match fst eq with
| AST_assign(_, e) | AST_assume(_, e) ->
@@ -299,11 +306,10 @@ let rec g_of_scope td (node, prefix, eqs) cond =
in
List.fold_left (@) [] (List.map do_eq eqs)
-and guarantees_of_prog p root =
+and guarantees_of_prog rp =
let td = {
- root_scope = get_root_scope p root;
- p = p;
- consts = I.consts p root;
+ rp = rp;
+ consts = I.consts rp;
} in
- g_of_scope td (get_root_scope p root) (BConst true)
+ g_of_scope td rp.root_scope (BConst true)
diff --git a/frontend/ast_printer.ml b/frontend/ast_printer.ml
index 3ac881e..7ddcb67 100644
--- a/frontend/ast_printer.ml
+++ b/frontend/ast_printer.ml
@@ -1,5 +1,6 @@
open Ast
open Lexing
+open Typing
(* Locations *)
@@ -252,3 +253,14 @@ let print_toplevel fmt = function
let print_prog fmt p =
List.iter (print_toplevel fmt) p
+
+
+(* Typed variable *)
+
+let print_type fmt = function
+ | TInt -> Format.fprintf fmt "int"
+ | TReal -> Format.fprintf fmt "real"
+ | TEnum e -> Format.fprintf fmt "enum { %a }" (print_list print_id ", ") e
+
+let print_typed_var fmt (p, id, t) =
+ Format.fprintf fmt "%s%s: %a" (if p then "probe " else "") id print_type t
diff --git a/interpret/ast_util.ml b/frontend/ast_util.ml
index 9cfe995..a7953ad 100644
--- a/interpret/ast_util.ml
+++ b/frontend/ast_util.ml
@@ -1,6 +1,14 @@
open Ast
open Util
+(* Some errors *)
+
+let combinatorial_cycle v = error ("Combinatorial cycle with variable: " ^ v)
+let no_variable e = error ("No such variable: " ^ e)
+let type_error e = error ("Type error: " ^ e)
+let not_implemented e = error ("Not implemented: " ^ e)
+let invalid_arity e = error ("Invalid arity (" ^ e ^ ")")
+
(* Utility : find declaration of a const / a node *)
let find_const_decl p id =
@@ -27,16 +35,6 @@ let extract_const_decls =
[]
-(* Utility : scopes *)
-
-
-(* path to node * subscope prefix in node * equations in scope *)
-type scope = id * id * eqn ext list
-
-let get_root_scope p root =
- let (n, _) = find_node_decl p root in
- ("", "", n.body)
-
(* Utility : find instances declared in an expression *)
@@ -75,10 +73,3 @@ let rec extract_pre e = match fst e with
| AST_pre(e', n) ->
(n, e')::(extract_pre e')
-(* Some errors *)
-
-let combinatorial_cycle v = error ("Combinatorial cycle with variable: " ^ v)
-let no_variable e = error ("No such variable: " ^ e)
-let type_error e = error ("Type error: " ^ e)
-let not_implemented e = error ("Not implemented: " ^ e)
-let invalid_arity e = error ("Invalid arity (" ^ e ^ ")")
diff --git a/interpret/rename.ml b/frontend/rename.ml
index 654b101..9c4cc31 100644
--- a/interpret/rename.ml
+++ b/frontend/rename.ml
@@ -3,8 +3,9 @@
open Ast
open Util
open Ast_util
+open Typing
-type renaming = (id * bool) VarMap.t
+type renaming = (id * bool) VarMap.t (* bool: is const ? *)
(* consts_renaming : prog -> renaming *)
let consts_renaming p =
diff --git a/frontend/typing.ml b/frontend/typing.ml
new file mode 100644
index 0000000..07b3bcd
--- /dev/null
+++ b/frontend/typing.ml
@@ -0,0 +1,178 @@
+(*
+ - Instanciate a program with a root node
+ - Enumerate all the variables, give them a type
+ - Give a type to expressions
+*)
+
+open Ast
+open Ast_util
+open Util
+
+type typ =
+ | TInt
+ | TReal
+ | TEnum of string list
+
+let bool_true = "T"
+let bool_false = "F"
+let bool_type = TEnum [bool_true; bool_false]
+
+let t_of_ast_t = function
+ | AST_TINT -> TInt
+ | AST_TREAL -> TReal
+ | AST_TBOOL -> bool_type
+
+
+(* probe? * variable full name * variable type *)
+type var = bool * id * typ
+
+(* path to node * subscope prefix in node * equations in scope *)
+type scope = id * id * eqn ext list
+
+type rooted_prog = {
+ p : prog;
+ root_node : node_decl;
+ root_scope : scope;
+ all_vars : var list;
+ const_vars : var list;
+}
+
+(* Typing *)
+
+(*
+ type_expr_vl : prog -> var list -> string -> typ list
+*)
+let rec type_expr_vl p vl cvl node expr =
+ let sub = type_expr_vl p vl cvl node in
+ let err = loc_error (snd expr) type_error in
+ match fst expr with
+ (* Identifiers *)
+ | AST_identifier(id, _) ->
+ let _, _, t = List.find (fun (_, x, _) -> x = (node^"/"^id)) vl in [t]
+ | AST_idconst(id, _) ->
+ let _, _, t = List.find (fun (_, x, _) -> x = id) cvl in [t]
+ (* On numerical values *)
+ | AST_int_const _ -> [TInt]
+ | AST_real_const _ -> [TReal]
+ | AST_unary (_, se) ->
+ begin match sub se with
+ | [TInt] -> [TInt]
+ | [TReal] -> [TReal]
+ | _ -> err "Invalid argument for unary."
+ end
+ | AST_binary(_, a, b) ->
+ begin match sub a, sub b with
+ | [TInt], [TInt] -> [TInt]
+ | [TReal], [TReal] -> [TReal]
+ | [TInt], [TReal] | [TReal], [TInt] -> [TReal]
+ | _ -> err "Invalid argument for binary."
+ end
+ (* On boolean values *)
+ | AST_bool_const _ -> [bool_type]
+ | AST_binary_rel _ -> [bool_type] (* do not check subtypes... TODO? *)
+ | AST_binary_bool _ -> [bool_type] (* the same *)
+ | AST_not _ -> [bool_type] (* the same *)
+ (* Temporal primitives *)
+ | AST_pre(e, _) -> sub e
+ | AST_arrow(a, b) ->
+ let ta, tb = sub a, sub b in
+ if ta = tb then ta
+ else err "Arrow does not have same type on both sides."
+ (* other *)
+ | AST_if(c, a, b) ->
+ let ta, tb = sub a, sub b in
+ if ta = tb then ta
+ else err "If does not have same type on both branches."
+ | AST_instance((f, _), _, _) ->
+ (* do not check types of arguments... TODO? *)
+ let (n, _) = find_node_decl p f in
+ List.map (fun (_, _, t) -> t_of_ast_t t) n.ret
+
+
+(* type_expr : tp -> string -> typ list *)
+let type_expr tp = type_expr_vl tp.p tp.all_vars tp.const_vars
+
+
+(* Program rooting *)
+
+
+(* decls_of_node : node_decl -> var_decl list *)
+let decls_of_node n = n.args @ n.ret @ n.var
+
+(* vars_in_node string -> var_decl list -> var list *)
+let vars_in_node nid =
+ List.map (fun (p, id, t) -> p, nid^"/"^id, t_of_ast_t t)
+
+(* node_vars : prog -> id -> string -> var list *)
+let node_vars p f nid =
+ let (n, _) = find_node_decl p f in
+ vars_in_node nid (decls_of_node n)
+
+(*
+ extract_all_vars : prog -> scope -> var list
+
+ Extracts all variables with names given according to
+ naming convention used here and in transform.ml :
+ - pre variables are not prefixed by scope
+ - next values for variables are prefixed by capital N
+*)
+let rec extract_all_vars p (node, prefix, eqs) n_vars const_vars =
+ let vars_of_expr e =
+ List.flatten
+ (List.map
+ (fun (f, id, eqs, args) ->
+ let nv = node_vars p f (node^"/"^id) in
+ nv @ extract_all_vars p (node^"/"^id, "", eqs) nv const_vars)
+ (extract_instances p e))
+ @
+ List.flatten
+ (List.map
+ (fun (id, expr) ->
+ let vd =
+ List.mapi
+ (fun i t -> false, id^"."^(string_of_int i), t)
+ (type_expr_vl p n_vars const_vars node expr)
+ in
+ vd @ (List.map (fun (a, x, c) -> (a, "N"^x, c)) vd))
+ (extract_pre e))
+ in
+ let vars_of_eq e = match fst e with
+ | AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) -> vars_of_expr e
+ | AST_activate (b, _) ->
+ let rec do_branch = function
+ | AST_activate_body b ->
+ let bvars = vars_in_node node b.act_locals in
+ bvars @
+ extract_all_vars p
+ (node, b.act_id^".", b.body)
+ (bvars@n_vars)
+ const_vars
+ | AST_activate_if(c, a, b) ->
+ vars_of_expr c @ do_branch a @ do_branch b
+ in do_branch b
+ | AST_automaton _ -> not_implemented "extract_all vars automaton"
+ in
+ (false, node^"/"^prefix^"time", TInt)::
+ (false, "N"^node^"/"^prefix^"time", TInt)::
+ (List.flatten (List.map vars_of_eq eqs))
+
+
+(*
+ root_prog : prog -> id -> rooted_prog
+*)
+let root_prog p root =
+ let (n, _) = find_node_decl p root in
+ let root_scope = ("", "", n.body) in
+
+ let const_vars = List.map
+ (fun (cd, _) -> (false, cd.c_name, t_of_ast_t cd.typ))
+ (extract_const_decls p)
+ in
+
+ let root_vars = vars_in_node "" (decls_of_node n) in
+
+ { p; root_scope; root_node = n;
+ const_vars = const_vars;
+ all_vars = root_vars @ extract_all_vars p root_scope root_vars const_vars }
+
+
diff --git a/interpret/interpret.ml b/interpret/interpret.ml
index 6f7c90e..b9a5576 100644
--- a/interpret/interpret.ml
+++ b/interpret/interpret.ml
@@ -1,6 +1,7 @@
open Ast
open Util
open Ast_util
+open Typing
module I : sig
@@ -26,13 +27,13 @@ module I : sig
(*
Get the constants only
*)
- val consts : prog -> id -> value VarMap.t
+ val consts : rooted_prog -> value VarMap.t
(*
Construct initial state for a program.
The id is the root node of the program evaluation.
*)
- val init_state : prog -> id -> state
+ val init_state : rooted_prog -> state
(*
Run a step of the program (not necessary to specify the program,
@@ -88,6 +89,7 @@ end = struct
type state = {
+ rp : rooted_prog;
p : prog;
root_scope : scope;
outputs : id list;
@@ -441,13 +443,13 @@ end = struct
(*
init_state : prog -> id -> state
*)
- let init_state p root =
- let (n, _) = find_node_decl p root in
+ let init_state rp =
let st = {
- p = p;
- root_scope = get_root_scope p root;
+ rp = rp;
+ p = rp.p;
+ root_scope = rp.root_scope;
save = VarMap.empty;
- outputs = (List.map (fun (_,n,_) -> n) n.ret);
+ outputs = (List.map (fun (_,n,_) -> n) rp.root_node.ret);
} in
let env = { st = st; vars = Hashtbl.create 42 } in
@@ -461,11 +463,11 @@ end = struct
| [v] -> Hashtbl.replace env.vars cpath v
| _ -> loc_error l error "Arity error in constant expression."))
| _ -> ())
- p;
+ rp.p;
List.iter (function
| AST_const_decl(d, l) -> ignore (get_var env "cst" d.c_name)
| _ -> ())
- p;
+ rp.p;
reset_scope env st.root_scope;
{ st with save = Hashtbl.fold VarMap.add env.vars VarMap.empty }
@@ -485,7 +487,7 @@ end = struct
do_weak_transitions env st.root_scope;
extract_st env, out
- let consts p root =
- (init_state p root).save
+ let consts rp =
+ (init_state rp).save
end
diff --git a/main.ml b/main.ml
index e98dd5f..b63b35f 100644
--- a/main.ml
+++ b/main.ml
@@ -31,7 +31,7 @@ let options = [
]
let do_test_interpret prog verbose =
- let s0 = Interpret.init_state prog "test" in
+ let s0 = Interpret.init_state (Typing.root_prog prog "test") in
if verbose then begin
Format.printf "Init state:@.";
Interpret.print_state Format.std_formatter s0;
@@ -75,8 +75,8 @@ let () =
let prog = Rename.rename_prog prog in
if !dumprn then Ast_printer.print_prog Format.std_formatter prog;
- if !ai_itv then AI_Itv.do_prog !ai_widen_delay prog !ai_root;
- if !ai_rel then AI_Rel.do_prog !ai_widen_delay prog !ai_root;
+ if !ai_itv then AI_Itv.do_prog !ai_widen_delay (Typing.root_prog prog !ai_root);
+ if !ai_rel then AI_Rel.do_prog !ai_widen_delay (Typing.root_prog prog !ai_root);
if !vtest then do_test_interpret prog true
else if !test then do_test_interpret prog false;