Did most of the boring stuff. Now, work on the abstract domain.

11 files changed, 209 insertions, 109 deletions

diff --git a/abstract/abs_domain.ml b/abstract/abs_domain.ml
index ddc34ab..a7f5455 100644
--- a/abstract/abs_domain.ml
+++ b/abstract/abs_domain.ml
@@ -2,6 +2,7 @@ open Ast
 open Formula
 open Num_domain
 open Typing
+open Util
 
 module type ENVIRONMENT_DOMAIN = sig
     type t
@@ -43,6 +44,14 @@ end
 
 module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct
 
+    type enum_valuation = (string * string) list
+
+    module VMapKey = struct
+      type t = enum_valuation VarMap.t
+      let compare = VarMap.compare (fun a b -> Pervasives.compare (List.sort Pervasives.compare a) (List.sort Pervasives.compare b))
+    end
+    module VMap = Mapext.Make(VMapKey)
+
     type t = ND.t
     type itv = ND.itv
 
@@ -65,16 +74,16 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct
     let subset = ND.subset
     let eq = ND.eq
 
-    let rec apply_cl x (cons, rest) = match rest with
+    let rec apply_cl x (econs, cons, rest) = match rest with
         | CLTrue ->
           ND.apply_ncl x cons
         | CLFalse -> vbottom x
         | CLAnd(a, b) ->
-          let y = apply_cl x (cons, a) in
-          apply_cl y (cons, b)
-        | CLOr((ca, ra), (cb, rb)) ->
-          let y = apply_cl x (cons@ca, ra) in
-          let z = apply_cl x (cons@cb, rb) in
+          let y = apply_cl x (econs, cons, a) in
+          apply_cl y (econs, cons, b)
+        | CLOr((eca, ca, ra), (ecb, cb, rb)) ->
+          let y = apply_cl x (econs@eca, cons@ca, ra) in
+          let z = apply_cl x (econs@ecb, cons@cb, rb) in
           join y z
 
     let apply_f x f = apply_cl x (conslist_of_f f)
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index 1d3e20a..7950144 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -27,14 +27,10 @@ end = struct
     }
 
 
-
-
     (* init state *)
     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 rp true) in
-      let cl_g = Formula.conslist_of_f f_g in
 
       let env = List.fold_left
         (fun env (_, id, ty) -> E.addvar env id ty)
@@ -58,6 +54,9 @@ end = struct
 
       let env = E.apply_f env init_f in
 
+      let cl = Formula.conslist_of_f f in
+      let cl_g = Formula.conslist_of_f f_g in
+
       { rp; widen_delay;
         f; cl; f_g; cl_g;
         guarantees; env }
diff --git a/abstract/formula.ml b/abstract/formula.ml
index a598750..ce83935 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -1,4 +1,6 @@
 open Ast
+open Util
+open Ast_util
 
 (* AST for logical formulas *)
 
@@ -23,12 +25,24 @@ type num_cons = num_expr * num_cons_op  (* always imply right member = 0 *)
 
 (* Logical part *)
 
+
+(* Enumerated types *)
+type enum_expr =
+  | EIdent of id
+  | EItem of string
+
+type enum_op =
+  | E_EQ | E_NE
+
+type enum_cons = enum_op * enum_expr * enum_expr
+
 type bool_expr =
   (* constants *)
   | BConst of bool
   (* operators from numeric values to boolean values *)
   | BRel of binary_rel_op * num_expr * num_expr
-  | BBoolEq of id * bool
+  (* operators on enumerated types *)
+  | BEnumCons of enum_cons
   (* boolean operators *)
   | BAnd of bool_expr * bool_expr
   | BOr of bool_expr * bool_expr
@@ -46,6 +60,10 @@ let f_or a b = match a, b with
   | a, BConst false -> a
   | a, b -> BOr(a, b)
 
+let f_e_eq a b = match a, b with
+  | EItem u, EItem v -> BConst (u = v)
+  | _ -> BEnumCons(E_EQ, a, b)
+
 
 (* Write all formula without using the NOT operator *)
 
@@ -56,7 +74,7 @@ let rec eliminate_not = function
   | x -> x
 and eliminate_not_negate = function
   | BConst x -> BConst(not x)
-  | BBoolEq(id, v) -> BBoolEq(id, not v)
+  | BEnumCons(op, a, b) -> BEnumCons((if op = E_EQ then E_NE else E_EQ), a, b)
   | BNot e -> eliminate_not e
   | BRel(r, a, b) ->
     if r = AST_EQ then
@@ -83,7 +101,7 @@ and eliminate_not_negate = function
   We also use this step to simplify trues and falses that may be present.
 *)
 
-type conslist = num_cons list * conslist_bool_expr
+type conslist = enum_cons list * num_cons list * conslist_bool_expr
 and conslist_bool_expr =
   | CLTrue
   | CLFalse
@@ -104,32 +122,30 @@ let rec conslist_of_f = function
     let cons = if y = NIntConst 0
       then (x, op)
       else (NBinary(AST_MINUS, x, y), op)
-    in [cons], CLTrue
+    in [], [cons], CLTrue
   | BConst x ->
-    [], if x then CLTrue else CLFalse
-  | BBoolEq(id, v) ->
-    if v then
-      [NBinary(AST_MINUS, NIdent id, NIntConst 1), CONS_EQ], CLTrue
-    else
-      [NIdent id, CONS_EQ], CLTrue
+    [], [], if x then CLTrue else CLFalse
+  | BEnumCons e ->
+    [e], [], CLTrue
   | BOr(a, b) ->
-    let ca, ra = conslist_of_f a in
-    let cb, rb = conslist_of_f b in
-    begin match ca, ra, cb, rb with
-      | _, CLFalse, _, _ -> cb, rb
-      | _, _, _, CLFalse -> ca, ra
-      | [], CLTrue, _, _ -> [], CLTrue
-      | _, _, [], CLTrue -> [], CLTrue
-      | _ -> [], CLOr((ca, ra), (cb, rb))
+    let eca, ca, ra = conslist_of_f a in
+    let ecb, cb, rb = conslist_of_f b in
+    begin match eca, ca, ra, ecb, cb, rb with
+      | _, _, CLFalse, _, _, _ -> ecb, cb, rb
+      | _, _, _, _, _, CLFalse -> eca, ca, ra
+      | [], [], CLTrue, _, _, _ -> [], [], CLTrue
+      | _, _, _, [], [], CLTrue -> [], [], CLTrue
+      | _ -> [], [], CLOr((eca, ca, ra), (ecb, cb, rb))
     end
   | BAnd(a, b) ->
-    let ca, ra = conslist_of_f a in
-    let cb, rb = conslist_of_f b in
+    let eca, ca, ra = conslist_of_f a in
+    let ecb, cb, rb = conslist_of_f b in
     let cons = ca @ cb in
+    let econs = eca @ ecb in
     begin match ra, rb with
-      | CLFalse, _ | _, CLFalse -> [], CLFalse
-      | CLTrue, _ -> cons, rb
-      | ra, CLTrue -> cons, ra
-      | _, _ -> cons, CLAnd(ra, rb)
+      | CLFalse, _ | _, CLFalse -> [], [], CLFalse
+      | CLTrue, _ -> econs, cons, rb
+      | _, CLTrue -> econs, cons, ra
+      | _, _ -> econs, cons, CLAnd(ra, rb)
     end
 
diff --git a/abstract/formula_printer.ml b/abstract/formula_printer.ml
index 1b31ba1..44f2d39 100644
--- a/abstract/formula_printer.ml
+++ b/abstract/formula_printer.ml
@@ -1,3 +1,4 @@
+open Util
 open Ast
 open Formula
 open Ast_printer
@@ -56,15 +57,24 @@ let rec print_num_expr fmt e = match e with
     Format.fprintf fmt "%s " (string_of_unary_op op);
     print_ah fmt print_num_expr ne_prec a ne_prec e
 
+(* Enumeated expressions *)
+let print_enum_expr fmt = function
+  | EIdent id -> Format.fprintf fmt "%s" id
+  | EItem x -> Format.fprintf fmt "%s" x
+
+let str_of_enum_op = function
+  | E_EQ -> "≡"
+  | E_NE -> "≢"
+
+let print_econs fmt (op, a, b) =
+    Format.fprintf fmt "%a %s %a"
+      print_enum_expr a (str_of_enum_op op) print_enum_expr b
+
 (* Print boolean form of formula *)
 
 let rec print_bool_expr fmt e = match e with
   | BConst b -> Format.fprintf fmt "%s" (if b then "true" else "false")
-  | BBoolEq(id, v) ->
-    if v then
-      Format.fprintf fmt "%a" print_id id
-    else
-      Format.fprintf fmt "¬%a" print_id id
+  | BEnumCons c -> print_econs fmt c
   | BRel(op, a, b) ->
     print_ch fmt print_num_expr ne_prec a be_prec e;
     Format.fprintf fmt "@ %s " (string_of_binary_rel op);
@@ -112,26 +122,33 @@ let print_cons fmt (eq, sg) =
   Format.fprintf fmt "@[<hv 2>%a %a 0@]"
     print_num_expr eq print_cons_sg sg
 
-let rec print_conslist fmt (cons, e) =
+let rec print_conslist fmt (econs, cons, e) =
+  let c = 
+    (List.map (fun x -> Left x) econs) @ (List.map (fun y -> Right y) cons)
+  in
+  let f fmt = function
+    | Left x -> Format.fprintf fmt "@[<hv 2>%a@]" print_econs x
+    | Right x -> Format.fprintf fmt "@[<hv 2>%a@]" print_cons x
+  in
   let rec aux = function
     | [] -> false
     | [a] ->
-      Format.fprintf fmt "@[<hv 2>%a@]" print_cons a; true
+      f fmt a; true
     | p::q ->
-      Format.fprintf fmt "@[<hv 2>%a@]" print_cons p;
+      f fmt p;
       Format.fprintf fmt "@ ∧ ";
       aux q
   in
   match e with
   | CLTrue ->
     Format.fprintf fmt "@[<hv 2>(";
-    ignore (aux cons);
+    ignore (aux c);
     Format.fprintf fmt ")@]"
   | CLFalse -> 
     Format.fprintf fmt "false"
   | _ ->
     Format.fprintf fmt "@[<hv 2>(";
-    if aux cons then Format.fprintf fmt "@ ∧ ";
+    if aux c then Format.fprintf fmt "@ ∧ ";
     print_conslist_expr fmt e;
     Format.fprintf fmt ")@]"
 
@@ -140,7 +157,7 @@ and print_conslist_expr fmt = function
   | CLFalse -> Format.fprintf fmt "false"
   | CLOr(a, b) ->
     Format.fprintf fmt "@[<hv 2>(%a@ ∨ %a)@]"
-        print_conslist a
+       print_conslist a
         print_conslist b
   | CLAnd(a, b) ->
     Format.fprintf fmt "%a@ ∧ %a"
diff --git a/abstract/transform.ml b/abstract/transform.ml
index 890f598..708456e 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -18,38 +18,57 @@ type transform_data = {
     (* future : the automata state *)
 }
 
-(* f_of_nexpr :
-    transform_data -> (string, string) -> (num_expr list -> 'a) -> expr -> 'a
+(* Numerical types / Enumerated types *)
+type ne_expr =
+  | EE of enum_expr
+  | NE of num_expr
+
+(* f_of_neexpr :
+    transform_data -> (string, string) -> (ne_expr list -> bool_expr) -> expr -> bool_expr
 *)
-let rec f_of_nexpr td (node, prefix) where expr =
-  let sub = f_of_nexpr td (node, prefix) in
+let rec f_of_neexpr td (node, prefix) where expr =
+  let sub = f_of_neexpr td (node, prefix) in
+  let le = loc_error (snd expr) in
   match fst expr with
   (* ident *)
-  | AST_identifier(id, _) -> where [NIdent (node^"/"^id)]
+  | AST_identifier(id, _) ->
+    let qid = node^"/"^id in
+    begin match type_var td.rp node id with
+    | TInt | TReal -> where [NE (NIdent qid)]
+    | TEnum _ -> where [EE (EIdent qid)]
+    end
   | AST_idconst(id, _) ->
     begin let x = VarMap.find ("cst/"^id) td.consts in
-      try where [NIntConst (I.as_int x)]
-      with _ -> try where [NRealConst (I.as_real x)]
-      with _ -> error "Invalid data for supposedly numerical constant."
+      try where [NE (NIntConst (I.as_int x))]
+      with _ -> try where [NE (NRealConst (I.as_real x))]
+      with _ -> try where [EE (EItem (if I.as_bool x then bool_true else bool_false))]
+      with _ -> le error "Invalid data for supposedly numerical/boolean constant."
     end
   (* numerical *)
-  | AST_int_const(i, _) -> where [NIntConst(int_of_string i)]
-  | AST_real_const(r, _) -> where [NRealConst(float_of_string r)]
+  | AST_int_const(i, _) -> where [NE(NIntConst(int_of_string i))]
+  | AST_real_const(r, _) -> where [NE(NRealConst(float_of_string r))]
+  | AST_bool_const b -> where [EE(EItem (if b then bool_true else bool_false))]
   | AST_unary(op, e) ->
     sub (function
-      | [x] -> where [NUnary(op, x)]
-      | _ -> invalid_arity "Unary operator") e
+      | [NE x] -> where [NE(NUnary(op, x))]
+      | _ -> le invalid_arity "Unary operator") e
   | AST_binary(op, a, b) ->
     sub (function
-      | [x] ->
+      | [NE x] ->
         sub (function
-          | [y] -> where [NBinary(op, x, y)]
-          | _ -> invalid_arity "binary_operator") b
-      | _ -> invalid_arity "binary operator") a
+          | [NE y] -> where [NE(NBinary(op, x, y))]
+          | _ -> le invalid_arity "binary operator") b
+      | _ -> le invalid_arity "binary operator") a
   (* temporal *)
   | 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)
+      where
+        (List.mapi
+          (fun i t -> let x = id^"."^(string_of_int i) in
+              match t with
+              | TInt | TReal -> NE(NIdent x)
+              | TEnum _ -> EE(EIdent x))
+          typ)
   | AST_arrow(a, b) ->
     f_or
       (f_and (BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0))
@@ -63,20 +82,34 @@ let rec f_of_nexpr td (node, prefix) where expr =
       (f_and (BNot(f_of_expr td (node, prefix) c)) (sub where b))
   | AST_instance ((f, _), args, nid) ->
     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 *)
-  | _ ->
+    where
+      (List.map
+        (fun (_, id, t) -> let x = node^"/"^nid^"/"^id in
+            match t with
+            | AST_TINT | AST_TREAL -> NE(NIdent x)
+            | _ -> EE(EIdent x))
+        n.ret)
+  | AST_tuple l ->
+    let rec rl l x = match l with
+      | [] -> where x
+      | p::q -> 
+        sub (fun y -> rl q (x@y)) p
+    in rl l []
+  (* boolean values treated as enumerated types *)
+  | _ when type_expr td.rp node expr = [bool_type] ->
     f_or
-      (f_and ((f_of_expr td (node, prefix) expr)) (where [NIntConst 1]))
-      (f_and (BNot(f_of_expr td (node, prefix) expr)) (where [NIntConst 0]))
+      (f_and (f_of_expr td (node, prefix) expr) (where [EE (EItem bool_true)]))
+      (f_and (f_of_expr td (node, prefix) (AST_not(expr), snd expr))
+        (where [EE (EItem bool_false)]))
+  | _ -> le type_error "Expected numerical/enumerated value"
+
 
 
 (* 
   f_of_expr :
     transform_data -> (string, string) -> expr -> bool_expr
   f_of_bexpr :
-    transform_data -> (string, string) -> (bool_expr -> 'a) -> expr -> 'a
+    transform_data -> (string, string) -> (bool_expr -> bool_expr) -> expr -> bool_expr
 *)
 and f_of_bexpr td (node, prefix) where expr =
   let sub = f_of_bexpr td (node, prefix) in
@@ -87,37 +120,35 @@ and f_of_bexpr td (node, prefix) where expr =
   | AST_not(a) -> BNot(sub where a)
   | AST_binary_rel(rel, a, b) ->
     where
-      (f_of_nexpr td (node, prefix)
+      (f_of_neexpr td (node, prefix)
         (function
-          | [x] -> f_of_nexpr td (node, prefix)
-            (function
-              | [y] -> BRel(rel, x, y)
-              | _ -> invalid_arity "boolean relation") b
-          | _ -> invalid_arity "boolean relation")
-        a)
-  | AST_identifier (id, _) ->
-    let id = node^"/"^id in
-    f_or
-      (f_and (BBoolEq(id, true)) (where (BConst true)))
-      (f_and (BBoolEq(id, false)) (where (BConst false)))
-  (* temporal *)
-  | AST_pre(_, id) ->
-    f_or
-      (f_and (BBoolEq(id, true)) (where (BConst true)))
-      (f_and (BBoolEq(id, false)) (where (BConst false)))
+          | [NE x; NE y] -> BRel(rel, x, y)
+          | [EE x; EE y] ->
+            let eop = match rel with
+              | AST_EQ -> E_EQ
+              | AST_NE -> E_NE
+              | _ -> type_error "Invalid operator on enumerated values."
+            in BEnumCons(eop, x, y)
+          | _ -> invalid_arity "Binary operator")
+        (AST_tuple [a; b], snd expr))
+  (* Temporal *)
   | AST_arrow(a, b) ->
       f_or
         (f_and (BRel(AST_EQ, NIdent(node^"/"^prefix^"time"), NIntConst 0))
           (sub where a))
         (f_and (BRel(AST_GE, NIdent(node^"/"^prefix^"time"), NIntConst 1))
           (sub where b))
-  (* other *)
-  | AST_if(c, a, b) ->
-    f_or
-      (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))
-
-  | _ -> loc_error (snd expr) error "Expected boolean value."
+  (* Enumerations... *)
+  | _ when type_expr td.rp node expr = [bool_type] ->
+    let ff = function
+      | [EE x] -> 
+        f_or
+          (f_and (f_e_eq x (EItem bool_true)) (where (BConst true)))
+          (f_and (f_e_eq x (EItem bool_false)) (where (BConst false)))
+      | _ -> assert false
+    in
+    f_of_neexpr td (node, prefix) ff expr
+  | _ -> type_error "Expected boolean value."
 
 and f_of_expr td (node, prefix) expr =
     f_of_bexpr td (node, prefix) (fun x -> x) expr
@@ -132,8 +163,9 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
       let eq = f_of_scope active td (node^"/"^id, "", eqs) assume_guarantees in
       if active then
         List.fold_left (fun eq ((_,argname,_), expr) ->
-            let eq_arg = f_of_nexpr td (node, prefix) (function
-                  | [v] -> BRel(AST_EQ, NIdent(node^"/"^id^"/"^argname), v)
+            let eq_arg = f_of_neexpr td (node, prefix) (function
+                  | [NE v] -> BRel(AST_EQ, NIdent(node^"/"^id^"/"^argname), v)
+                  | [EE v] -> f_e_eq (EIdent(node^"/"^id^"/"^argname)) v
                   | _ -> invalid_arity "in argument")
                 expr
             in f_and eq eq_arg)
@@ -146,17 +178,23 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
     in
     let pre_expr (id, expr) =
       if active then
-        f_of_nexpr td (node, prefix) (fun elist ->
+        f_of_neexpr 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))
+                (fun i v -> let x = ("N"^id^"."^(string_of_int i)) in
+                  match v with
+                  | NE v -> BRel(AST_EQ, NIdent x, v)
+                  | EE v -> f_e_eq (EIdent x) v)
                 elist))
           expr
       else
         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)))
+            (fun i t -> let x = string_of_int i in
+              match t with
+              | TInt | TReal -> BRel(AST_EQ, NIdent("N"^id^"."^x), NIdent (id^"."^x))
+              | TEnum _ -> f_e_eq (EIdent("N"^id^"."^x)) (EIdent (id^"."^x)))
             typ)
     in
     List.fold_left (fun x i -> f_and (pre_expr i) x)
@@ -166,14 +204,16 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
     | AST_assign(ids, e) ->
       let assign_eq = 
         if active then
-          f_of_nexpr td (node, prefix)
-            (fun vs ->
-              let rels = 
-                List.map2 (fun (id, _) v -> BRel(AST_EQ, NIdent (node^"/"^id), v))
-                ids vs
-              in
-                list_fold_op f_and rels)
-            e
+            f_of_neexpr td (node, prefix)
+              (fun vs ->
+                let rels = 
+                  List.map2 (fun (id, _) -> function
+                    | NE v -> BRel(AST_EQ, NIdent (node^"/"^id), v)
+                    | EE v -> f_e_eq (EIdent (node^"/"^id)) v)
+                  ids vs
+                in
+                  list_fold_op f_and rels)
+              e
         else
           BConst true
       in
diff --git a/frontend/ast.ml b/frontend/ast.ml
index 4f8c860..ae11064 100644
--- a/frontend/ast.ml
+++ b/frontend/ast.ml
@@ -57,6 +57,7 @@ type expr =
     (* other *)
     | AST_if          of (expr ext) * (expr ext) * (expr ext)
     | AST_instance    of (id ext) * (expr ext list) * id
+    | AST_tuple       of expr ext list
 
 type var_def = bool * id * typ
 
diff --git a/frontend/ast_printer.ml b/frontend/ast_printer.ml
index 7ddcb67..ac30fe9 100644
--- a/frontend/ast_printer.ml
+++ b/frontend/ast_printer.ml
@@ -160,6 +160,10 @@ let rec print_expr fmt e =
         Format.fprintf fmt "%a(%a)"
           print_id i (print_list print_expr ", ") (List.map fst l)
 
+  | AST_tuple x ->
+      Format.fprintf fmt "(%a)"
+        (print_list print_expr ", ") (List.map fst x)
+
 
 (* equations *)
 
diff --git a/frontend/ast_util.ml b/frontend/ast_util.ml
index a7953ad..b3393a7 100644
--- a/frontend/ast_util.ml
+++ b/frontend/ast_util.ml
@@ -55,6 +55,7 @@ let rec extract_instances p e = match fst e with
     let (node, _) = find_node_decl p f in
     let args_x = List.map2 (fun id arg -> id, arg) node.args args in
     (f, id, node.body, args_x)::more
+  | AST_tuple x -> List.flatten (List.map (extract_instances p) x)
 
 (* Utility : find pre declarations in an expression *)
 
@@ -70,6 +71,7 @@ let rec extract_pre e = match fst e with
     extract_pre e1 @ extract_pre e2 @ extract_pre e3
   | AST_instance((f, _), args, id) ->
     List.flatten (List.map extract_pre args)
+  | AST_tuple x -> List.flatten (List.map extract_pre x)
   | AST_pre(e', n) ->
     (n, e')::(extract_pre e')
 
diff --git a/frontend/typing.ml b/frontend/typing.ml
index 07b3bcd..1545a38 100644
--- a/frontend/typing.ml
+++ b/frontend/typing.ml
@@ -13,8 +13,8 @@ type typ =
     | TReal
     | TEnum of string list
 
-let bool_true = "T"
-let bool_false = "F"
+let bool_true = "tt"
+let bool_false = "ff"
 let bool_type = TEnum [bool_true; bool_false]
 
 let t_of_ast_t = function
@@ -87,11 +87,15 @@ let rec type_expr_vl p vl cvl node expr =
       (* 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
+    | AST_tuple x -> List.flatten (List.map sub x)
 
 
-(* type_expr : tp -> string -> typ list *)
+(* type_expr : tp -> string -> expr -> typ list *)
 let type_expr tp = type_expr_vl tp.p tp.all_vars tp.const_vars
 
+let type_var tp node id =
+    let _, _, t = List.find (fun (_, x, _) -> x = (node^"/"^id)) tp.all_vars in t
+
 
 (* Program rooting *)
 
diff --git a/interpret/interpret.ml b/interpret/interpret.ml
index b9a5576..27cecdb 100644
--- a/interpret/interpret.ml
+++ b/interpret/interpret.ml
@@ -210,6 +210,7 @@ end = struct
       | [VBool false] -> sub_eval b
       | _ -> type_error "Invalid condition in if."
       end
+    | AST_tuple x -> List.flatten (List.map sub_eval x)
     | AST_instance((f, _), args, nid) ->
       let (n, _) = find_node_decl env.st.p f in
       List.map
diff --git a/libs/util.ml b/libs/util.ml
index 97aa480..6931ed9 100644
--- a/libs/util.ml
+++ b/libs/util.ml
@@ -1,3 +1,10 @@
+(* Either type *)
+
+type ('a, 'b) either =
+  | Left of 'a
+  | Right of 'b
+
+
 (* Locations *)
 
 type position = Lexing.position