relax [term.t_ty] to [ty option] and make it compile

I love static typing!

src/core/decl.ml

@@ -44,16 +44,15 @@ let check_fvs f =
   Svs.iter (fun vs -> raise (UnboundVar vs)) fvs;
   f
 
-let check_ty ty ty' =
-  if not (ty_equal ty ty') then raise (TypeMismatch (ty,ty'))
+let check_ty = Ty.check_ty_equal
 
 let check_vl ty v = check_ty ty v.vs_ty
-let check_tl ty t = check_ty ty t.t_ty
+let check_tl ty t = check_ty ty (t_type t)
 
 let make_fs_defn fs vl t =
-  let hd = t_app fs (List.map t_var vl) t.t_ty in
+  let hd = e_app fs (List.map t_var vl) t.t_ty in
   let fd = f_forall_close vl [] (f_equ hd t) in
-  check_ty (of_option fs.ls_value) t.t_ty;
+  check_oty_equal fs.ls_value t.t_ty;
   List.iter2 check_vl fs.ls_args vl;
   fs, Some (fs, check_fvs fd)
 

src/core/pattern.ml

@@ -38,12 +38,12 @@ module Compile (X : Action) = struct
 
   let rec compile constructors tl rl = match tl,rl with
     | _, [] -> (* no actions *)
-        let pl = List.map (fun t -> pat_wild t.t_ty) tl in
+        let pl = List.map (fun t -> pat_wild (t_type t)) tl in
         raise (NonExhaustive pl)
     | [], (_,a) :: _ -> (* no terms, at least one action *)
         a
     | t :: tl, _ -> (* process the leftmost column *)
-        let ty = t.t_ty in
+        let ty = t_type t in
         (* extract the set of constructors *)
         let css = match ty.ty_node with
           | Tyapp (ts,_) ->

src/core/pretty.ml

@@ -233,7 +233,7 @@ and print_tnode pri fmt t = match t.t_node with
       print_app pri fs fmt tl
   | Tapp (fs, tl) ->
       fprintf fmt (protect_on (pri > 0) "%a:%a")
-        (print_app 5 fs) tl print_ty t.t_ty
+        (print_app 5 fs) tl print_ty (t_type t)
   | Tif (f,t1,t2) ->
       fprintf fmt (protect_on (pri > 0) "if @[%a@] then %a@ else %a")
         print_fmla f print_term t1 print_term t2
@@ -494,6 +494,8 @@ let () = Exn_printer.register
       fprintf fmt "Type variable %a is used twice" print_tv tv
   | Ty.UnboundTypeVar tv ->
       fprintf fmt "Unbound type variable: %a" print_tv tv
+  | Ty.UnexpectedProp ->
+      fprintf fmt "Unexpected propositional type"
   | Term.BadArity (ls, ls_arg, app_arg) ->
       fprintf fmt "Bad arity: symbol %a must be applied \
                    to %i arguments, but is applied to %i"
@@ -508,6 +510,10 @@ let () = Exn_printer.register
       fprintf fmt "Not a function symbol: %a" print_ls ls
   | Term.PredicateSymbolExpected ls ->
       fprintf fmt "Not a predicate symbol: %a" print_ls ls
+  | Term.TermExpected t ->
+      fprintf fmt "Not a term: %a" print_term t
+  | Term.FmlaExpected t ->
+      fprintf fmt "Not a formula: %a" print_term t
   | Term.NoMatch ->
       fprintf fmt "Uncatched Term.NoMatch exception: [tf]_match failed"
   | Pattern.ConstructorExpected ls ->

src/core/printer.ml

@@ -132,8 +132,8 @@ let syntax_arguments_typed s print_arg print_type t fmt l =
       let grp = String.sub grp 1 (String.length grp - 1) in
       let i = int_of_string grp in
       if i = 0
-      then print_type fmt (Util.of_option t).t_ty
-      else print_type fmt args.(i-1).t_ty
+      then print_type fmt (t_type (Util.of_option t))
+      else print_type fmt (t_type args.(i-1))
     else
       let i = int_of_string grp in
       print_arg fmt args.(i-1) in

src/core/term.ml

@@ -178,9 +178,6 @@ let pat_map fn pat = match pat.pat_node with
   | Pas (p, v) -> pat_as (fn p) v
   | Por (p, q) -> pat_or (fn p) (fn q)
 
-let check_ty_equal ty1 ty2 =
-  if not (ty_equal ty1 ty2) then raise (TypeMismatch (ty1, ty2))
-
 let protect fn pat =
   let res = fn pat in
   check_ty_equal pat.pat_ty res.pat_ty;
@@ -271,7 +268,7 @@ type term = {
   t_label : label list;
   t_loc   : Loc.position option;
   t_vars  : Svs.t;
-  t_ty    : ty;
+  t_ty    : oty;
   t_tag   : int;
 }
 
@@ -330,6 +327,15 @@ let f_equal : fmla -> fmla -> bool = (==)
 let t_hash t = t.t_tag
 let f_hash f = f.f_tag
 
+(* extract the type of a term *)
+
+exception TermExpected of term
+exception FmlaExpected of term
+
+let t_type t = match t.t_ty with
+  | Some ty -> ty
+  | None -> raise (TermExpected t)
+
 (* expr and trigger equality *)
 
 let e_equal e1 e2 = match e1, e2 with
@@ -400,7 +406,7 @@ module Hsterm = Hashcons.Make (struct
     | _ -> false
 
   let equal t1 t2 =
-    ty_equal t1.t_ty t2.t_ty &&
+    oty_equal t1.t_ty t2.t_ty &&
     t_equal_node t1.t_node t2.t_node &&
     list_all2 (=) t1.t_label t2.t_label
 
@@ -424,7 +430,7 @@ module Hsterm = Hashcons.Make (struct
 
   let hash t =
     Hashcons.combine (t_hash_node t.t_node)
-      (Hashcons.combine_list Hashtbl.hash (ty_hash t.t_ty) t.t_label)
+      (Hashcons.combine_list Hashtbl.hash (oty_hash t.t_ty) t.t_label)
 
   let add_t_vars s t = Svs.union s t.t_vars
   let add_b_vars s (_,b,_) = Svs.union s b.bv_vars
@@ -552,10 +558,10 @@ let mk_term n ty = Hsterm.hashcons {
   t_tag   = -1
 }
 
-let t_var v         = mk_term (Tvar v) v.vs_ty
-let t_const c ty    = mk_term (Tconst c) ty
-let t_int_const s   = mk_term (Tconst (ConstInt s)) Ty.ty_int
-let t_real_const r  = mk_term (Tconst (ConstReal r)) Ty.ty_real
+let t_var v         = mk_term (Tvar v) (Some v.vs_ty)
+let t_const c ty    = mk_term (Tconst c) (Some ty)
+let t_int_const s   = mk_term (Tconst (ConstInt s)) (Some Ty.ty_int)
+let t_real_const r  = mk_term (Tconst (ConstReal r)) (Some Ty.ty_real)
 let t_app f tl ty   = mk_term (Tapp (f, tl)) ty
 let t_if f t1 t2    = mk_term (Tif (f, t1, t2)) t2.t_ty
 let t_let t1 bt ty  = mk_term (Tlet (t1, bt)) ty
@@ -903,16 +909,14 @@ let f_open_quant_cb fq =
 (* constructors with type checking *)
 
 let ls_arg_inst ls tl =
-  let mtch s ty t = ty_match s ty t.t_ty in
+  let mtch s ty t = ty_match s ty (t_type t) in
   try List.fold_left2 mtch Mtv.empty ls.ls_args tl
   with Invalid_argument _ -> raise (BadArity
     (ls, List.length ls.ls_args, List.length tl))
 
 let t_app_infer ls tl =
   let s = ls_arg_inst ls tl in
-  match ls.ls_value with
-    | Some ty -> t_app ls tl (ty_inst s ty)
-    | None -> raise (FunctionSymbolExpected ls)
+  t_app ls tl (oty_inst s ls.ls_value)
 
 let ls_app_inst ls tl ty =
   let s = ls_arg_inst ls tl in
@@ -925,7 +929,8 @@ let ls_app_inst ls tl ty =
 let fs_app_inst fs tl ty = ls_app_inst fs tl (Some ty)
 let ps_app_inst ps tl    = ls_app_inst ps tl (None)
 
-let t_app fs tl ty = ignore (fs_app_inst fs tl ty); t_app fs tl ty
+let e_app ls tl ty = ignore (ls_app_inst ls tl ty); t_app ls tl ty
+let t_app fs tl ty = ignore (fs_app_inst fs tl ty); t_app fs tl (Some ty)
 let f_app ps tl    = ignore (ps_app_inst ps tl);    f_app ps tl
 
 exception EmptyCase
@@ -936,8 +941,8 @@ let t_case t bl =
     | _ -> raise EmptyCase
   in
   let t_check_branch (p,_,tbr) =
-    check_ty_equal p.pat_ty t.t_ty;
-    check_ty_equal ty tbr.t_ty
+    check_ty_equal p.pat_ty (t_type t);
+    check_oty_equal ty tbr.t_ty
   in
   List.iter t_check_branch bl;
   t_case t bl ty
@@ -945,25 +950,25 @@ let t_case t bl =
 let f_case t bl =
   if bl = [] then raise EmptyCase;
   let f_check_branch (p,_,_) =
-    check_ty_equal p.pat_ty t.t_ty
+    check_ty_equal p.pat_ty (t_type t)
   in
   List.iter f_check_branch bl;
   f_case t bl
 
 let t_if f t1 t2 =
-  check_ty_equal t1.t_ty t2.t_ty;
+  check_oty_equal t1.t_ty t2.t_ty;
   t_if f t1 t2
 
 let t_let t1 ((v,_,t2) as bt) =
-  check_ty_equal v.vs_ty t1.t_ty;
+  check_ty_equal v.vs_ty (t_type t1);
   t_let t1 bt t2.t_ty
 
 let f_let t1 ((v,_,_) as bf) =
-  check_ty_equal v.vs_ty t1.t_ty;
+  check_ty_equal v.vs_ty (t_type t1);
   f_let t1 bf
 
 let t_eps ((v,_,_) as bf) =
-  t_eps bf v.vs_ty
+  t_eps bf (Some v.vs_ty)
 
 let t_const c = match c with
   | ConstInt _ -> t_const c ty_int
@@ -1024,7 +1029,7 @@ let fs_tuple = Util.memo_int 17 (fun n ->
 let is_fs_tuple fs = fs == fs_tuple (List.length fs.ls_args)
 
 let t_tuple tl =
-  let ty = ty_tuple (List.map (fun t -> t.t_ty) tl) in
+  let ty = ty_tuple (List.map t_type tl) in
   t_app (fs_tuple (List.length tl)) tl ty
 
 (** Term library *)
@@ -1040,12 +1045,12 @@ let rec t_gen_map fnT fnL m t =
   t_label_copy t (match t.t_node with
     | Tvar v ->
         let r = Mvs.find_default v t m in
-        check_ty_equal (fnT t.t_ty) r.t_ty;
+        check_ty_equal (fnT (t_type t)) (t_type r);
         r
     | Tconst _ ->
         t
     | Tapp (fs, tl) ->
-        t_app (fnL fs) (List.map fn_t tl) (fnT t.t_ty)
+        t_app (fnL fs) (List.map fn_t tl) (fnT (t_type t))
     | Tif (f, t1, t2) ->
         t_if (fn_f f) (fn_t t1) (fn_t t2)
     | Tlet (t1, (u,b,t2)) ->
@@ -1121,7 +1126,7 @@ let f_ty_subst mapT mapV f = f_gen_map (ty_inst mapT) (fun ls -> ls) mapV f
 let rec t_gen_fold fnT fnL acc t =
   let fn_t = t_gen_fold fnT fnL in
   let fn_f = f_gen_fold fnT fnL in
-  let acc = fnT acc t.t_ty in
+  let acc = fnT acc (t_type t) in
   match t.t_node with
   | Tconst _ | Tvar _ -> acc
   | Tapp (f, tl) -> List.fold_left fn_t (fnL acc f) tl
@@ -1177,13 +1182,13 @@ let f_ty_fold fn acc f = f_gen_fold fn Util.const acc f
 let rec t_app_fold fn acc t =
   let acc = t_fold_unsafe (t_app_fold fn) (f_app_fold fn) acc t in
   match t.t_node with
-    | Tapp (ls,tl) -> fn acc ls (List.map (fun t -> t.t_ty) tl) (Some t.t_ty)
+    | Tapp (ls,tl) -> fn acc ls (List.map t_type tl) t.t_ty
     | _ -> acc
 
 and f_app_fold fn acc f =
   let acc = f_fold_unsafe (t_app_fold fn) (f_app_fold fn) acc f in
   match f.f_node with
-    | Fapp (ls,tl) -> fn acc ls (List.map (fun t -> t.t_ty) tl) None
+    | Fapp (ls,tl) -> fn acc ls (List.map t_type tl) None
     | _ -> acc
 
 (* free type variables *)
@@ -1221,7 +1226,7 @@ let f_map fnT fnF f = match f.f_node with
 
 let protect fn t =
   let res = fn t in
-  check_ty_equal t.t_ty res.t_ty;
+  check_oty_equal t.t_ty res.t_ty;
   res
 
 let t_map fnT = t_map (protect fnT)
@@ -1323,7 +1328,7 @@ let f_map_fold fnT fnF acc f = match f.f_node with
 
 let protect_fold fn acc t =
   let acc,res = fn acc t in
-  check_ty_equal t.t_ty res.t_ty;
+  check_oty_equal t.t_ty res.t_ty;
   acc,res
 
 let t_map_fold fnT = t_map_fold (protect_fold fnT)
@@ -1351,7 +1356,7 @@ let t_map_cont fnT fnF contT t =
   match t.t_node with
   | Tvar _ | Tconst _ -> contT t
   | Tapp (fs, tl) ->
-      let cont_app tl = contT (t_app fs tl t.t_ty) in
+      let cont_app tl = contT (e_app fs tl t.t_ty) in
       list_map_cont fnT cont_app tl
   | Tif (f, t1, t2) ->
       let cont_else f t1 t2 = contT (t_if f t1 t2) in
@@ -1415,7 +1420,7 @@ let f_map_cont fnT fnF contF f =
       fnT cont_case t1
 
 let protect_cont t contT e =
-  check_ty_equal t.t_ty e.t_ty;
+  check_oty_equal t.t_ty e.t_ty;
   contT e
 
 let t_map_cont fnT = t_map_cont (fun c t -> fnT (protect_cont t c) t)
@@ -1425,7 +1430,7 @@ let f_map_cont fnT = f_map_cont (fun c t -> fnT (protect_cont t c) t)
 
 let protect_vs fn v =
   let res = fn v in
-  check_ty_equal v.vs_ty res.t_ty;
+  check_ty_equal v.vs_ty (t_type res);
   res
 
 let t_v_map fn t =
@@ -1455,11 +1460,11 @@ let f_occurs_single v f = Svs.mem v f.f_vars
 (* replaces variables with terms in term [t] using map [m] *)
 
 let t_subst m t =
-  Mvs.iter (fun v t -> check_ty_equal v.vs_ty t.t_ty) m;
+  Mvs.iter (fun v t -> check_ty_equal v.vs_ty (t_type t)) m;
   t_subst_unsafe m t
 
 let f_subst m f =
-  Mvs.iter (fun v t -> check_ty_equal v.vs_ty t.t_ty) m;
+  Mvs.iter (fun v t -> check_ty_equal v.vs_ty (t_type t)) m;
   f_subst_unsafe m f
 
 let t_subst_single v t1 t = t_subst (Mvs.singleton v t1) t
@@ -1495,7 +1500,7 @@ let rec pat_equal_alpha p1 p2 =
   | _ -> false
 
 let rec t_equal_alpha c1 c2 m1 m2 t1 t2 =
-  t_equal t1 t2 || ty_equal t1.t_ty t2.t_ty &&
+  t_equal t1 t2 || oty_equal t1.t_ty t2.t_ty &&
   let t_eq = t_equal_alpha c1 c2 m1 m2 in
   let f_eq = f_equal_alpha c1 c2 m1 m2 in
   match t1.t_node, t2.t_node with
@@ -1682,7 +1687,7 @@ exception NoMatch
 
 let rec t_match s t1 t2 =
   if t_equal t1 t2 then s else
-  if not (ty_equal t1.t_ty t2.t_ty) then raise NoMatch else
+  if not (oty_equal t1.t_ty t2.t_ty) then raise NoMatch else
   match t1.t_node, t2.t_node with
     | Tconst c1, Tconst c2 when c1 = c2 -> s
     | Tvar v1, _ ->
@@ -1749,11 +1754,11 @@ and f_subst_term t1 t2 f =
   f_map (t_subst_term t1 t2) (f_subst_term t1 t2) f
 
 let t_subst_term t1 t2 t =
-  check_ty_equal t1.t_ty t2.t_ty;
+  check_oty_equal t1.t_ty t2.t_ty;
   t_subst_term t1 t2 t
 
 let f_subst_term t1 t2 f =
-  check_ty_equal t1.t_ty t2.t_ty;
+  check_oty_equal t1.t_ty t2.t_ty;
   f_subst_term t1 t2 f
 
 (* substitutes fmla [f2] for fmla [f1] in term [t] *)
@@ -1773,11 +1778,11 @@ and f_subst_term_alpha t1 t2 f =
   f_map (t_subst_term_alpha t1 t2) (f_subst_term_alpha t1 t2) f
 
 let t_subst_term_alpha t1 t2 t =
-  check_ty_equal t1.t_ty t2.t_ty;
+  check_oty_equal t1.t_ty t2.t_ty;
   t_subst_term_alpha t1 t2 t
 
 let f_subst_term_alpha t1 t2 f =
-  check_ty_equal t1.t_ty t2.t_ty;
+  check_oty_equal t1.t_ty t2.t_ty;
   f_subst_term_alpha t1 t2 f
 
 (* substitutes fmla [f2] for fmla [f1] in term [t] modulo alpha *)

src/core/term.mli

@@ -45,7 +45,7 @@ val create_vsymbol : preid -> ty -> vsymbol
 type lsymbol = private {
   ls_name   : ident;
   ls_args   : ty list;
-  ls_value  : ty option;
+  ls_value  : oty;
 }
 
 module Mls : Map.S with type key = lsymbol
@@ -57,7 +57,7 @@ val ls_equal : lsymbol -> lsymbol -> bool
   (** equality of function and predicate symbols *)
 val ls_hash : lsymbol -> int
 
-val create_lsymbol : preid -> ty list -> ty option -> lsymbol
+val create_lsymbol : preid -> ty list -> oty -> lsymbol
 val create_fsymbol : preid -> ty list -> ty -> lsymbol
 val create_psymbol : preid -> ty list -> lsymbol
 
@@ -131,7 +131,7 @@ type term = private {
   t_label : label list;
   t_loc   : Loc.position option;
   t_vars  : Svs.t;
-  t_ty    : ty;
+  t_ty    : oty;
   t_tag   : int;
 }
 
@@ -239,10 +239,18 @@ val f_open_quant_cb :
 
 (** compute type instance *)
 
-val ls_app_inst : lsymbol -> term list -> ty option -> ty Mtv.t
+val ls_app_inst : lsymbol -> term list -> oty -> ty Mtv.t
 val fs_app_inst : lsymbol -> term list -> ty -> ty Mtv.t
 val ps_app_inst : lsymbol -> term list -> ty Mtv.t
 
+(* temporary functions for term+fmla fusion *)
+
+exception TermExpected of term
+exception FmlaExpected of term
+
+val e_app : lsymbol -> term list -> oty -> term
+val t_type : term -> ty
+
 (** Smart constructors for term *)
 
 val t_var : vsymbol -> term
@@ -361,11 +369,8 @@ val f_ty_fold : ('a -> ty -> 'a) -> 'a -> fmla -> 'a
 
 (* fold over applications in terms and formulas (but not in patterns!) *)
 
-val t_app_fold :
-  ('a -> lsymbol -> ty list -> ty option -> 'a) -> 'a -> term -> 'a
-
-val f_app_fold :
-  ('a -> lsymbol -> ty list -> ty option -> 'a) -> 'a -> fmla -> 'a
+val t_app_fold : ('a -> lsymbol -> ty list -> oty -> 'a) -> 'a -> term -> 'a
+val f_app_fold : ('a -> lsymbol -> ty list -> oty -> 'a) -> 'a -> fmla -> 'a
 
 (** built-in symbols *)
 

src/core/ty.ml

@@ -265,3 +265,11 @@ let oty_inst m = Util.option_map (ty_inst m)
 let oty_freevars = Util.option_fold ty_freevars
 let oty_cons = Util.option_fold (fun tl t -> t::tl)
 
+let check_ty_equal ty1 ty2 =
+  if not (ty_equal ty1 ty2) then raise (TypeMismatch (ty1, ty2))
+
+let check_oty_equal o1 o2 = match o1,o2 with
+  | Some ty1, Some ty2 -> check_ty_equal ty1 ty2
+  | None, None -> ()
+  | _ -> raise UnexpectedProp
+

src/core/ty.mli

@@ -142,3 +142,6 @@ val oty_match : ty Mtv.t -> oty -> oty -> ty Mtv.t
 val oty_inst  : ty Mtv.t -> oty -> oty
 val oty_freevars : Stv.t -> oty -> Stv.t
 
+val check_ty_equal : ty -> ty -> unit
+val check_oty_equal : oty -> oty -> unit
+

src/parser/denv.ml

@@ -204,7 +204,7 @@ let rec term env t = match t.dt_node with
       t_if (fmla env f) (term env t1) (term env t2)
   | Tlet (e1, id, e2) ->
       let e1 = term env e1 in
-      let v = create_user_vs id e1.t_ty in
+      let v = create_user_vs id (t_type e1) in
       let env = Mstr.add id.id v env in
       let e2 = term env e2 in
       t_let_close v e1 e2
@@ -253,7 +253,7 @@ and fmla env = function
       f_app s (List.map (term env) tl)
   | Flet (e1, id, f2) ->
       let e1 = term env e1 in
-      let v = create_user_vs id e1.t_ty in
+      let v = create_user_vs id (t_type e1) in
       let env = Mstr.add id.id v env in
       let f2 = fmla env f2 in
       f_let_close v e1 f2
@@ -319,7 +319,7 @@ and specialize_pattern_node ~loc htv = function
 let rec specialize_term ~loc htv t =
   let dt =
     { dt_node = specialize_term_node  ~loc htv t.t_node;
-      dt_ty   = specialize_ty         ~loc htv t.t_ty; }
+      dt_ty   = specialize_ty         ~loc htv (t_type t); }
   in
   let add_label l t = { t with dt_node = Tnamed (l, t) } in
   let dt = option_apply dt (fun p -> add_label (Lpos p) dt) t.t_loc in

src/printer/coq.ml

@@ -241,7 +241,7 @@ and print_tnode opl opr info fmt t = match t.t_node with
           then fprintf fmt "(%a %a)" print_ls fs
             (print_space_list (print_term info)) tl
           else fprintf fmt (protect_on opl "(%a%a:%a)") print_ls fs
-            (print_paren_r (print_term info)) tl (print_ty info) t.t_ty
+            (print_paren_r (print_term info)) tl (print_ty info) (t_type t)
     end
 
 and print_fnode opl opr info fmt f = match f.f_node with

src/printer/why3.ml

@@ -200,7 +200,7 @@ and print_tnode pri fmt t = match t.t_node with
       print_tapp pri fs fmt tl
   | Tapp (fs, tl) ->
       fprintf fmt (protect_on (pri > 0) "%a:%a")
-        (print_tapp 0 fs) tl print_ty t.t_ty
+        (print_tapp 0 fs) tl print_ty (t_type t)
   | Tif (f,t1,t2) ->
       fprintf fmt (protect_on (pri > 0) "if @[%a@] then %a@ else %a")
         print_fmla f print_term t1 print_term t2

src/programs/pgm_pretty.ml

@@ -13,7 +13,7 @@ open Pgm_ttree
 let rec print_expr fmt e = match e.expr_desc with
   | Elogic t ->
       fprintf fmt "@[<hov 2><term %a : %a>@]" Pretty.print_term t
-	Pretty.print_ty t.t_ty
+	Pretty.print_ty (t_type t)
   | Elocal v ->
       fprintf fmt "%a" print_pv v
   | Eglobal { ps_kind = PSvar v } ->

src/programs/pgm_typing.ml

@@ -834,14 +834,14 @@ let ivariant env (t, ps) =
   let t = iterm env t in
   match ps with
     | None ->
-	if not (Ty.ty_equal ty_int t.t_ty) then
+	if not (Ty.ty_equal ty_int (t_type t)) then
 	  errorm ~loc "variant should have type int";
 	t, ps
-    | Some { ls_args = [t1; _] } when Ty.ty_equal t1 t.t_ty ->
+    | Some { ls_args = [t1; _] } when Ty.ty_equal t1 (t_type t) ->
 	t, ps
     | Some { ls_args = [t1; _] } ->
 	errorm ~loc "@[variant has type %a, but is expected to have type %a@]"
-	  Pretty.print_ty t.t_ty Pretty.print_ty t1
+	  Pretty.print_ty (t_type t) Pretty.print_ty t1
     | _ ->
 	assert false
 
@@ -1218,8 +1218,8 @@ and iletrec gl env dl =
 	  None, t
       | Some (phi, r) ->
 	  let p, e, q = t in
-	  let phi0 = create_ivsymbol (id_fresh "variant") phi.t_ty in
-	  let e_phi = { iexpr_desc = IElogic phi; iexpr_type = phi.t_ty;
+	  let phi0 = create_ivsymbol (id_fresh "variant") (t_type phi) in
+	  let e_phi = { iexpr_desc = IElogic phi; iexpr_type = t_type phi;
 			iexpr_loc = e.iexpr_loc } in
 	  let e = { e with iexpr_desc = IElet (phi0, e_phi, e) } in
 	  Some (phi0, phi, r), (p, e, q)

src/programs/pgm_wp.ml

@@ -112,7 +112,7 @@ let rec old_label env lab f =
 and old_label_term env lab t = match t.t_node with
   | Tapp (ls, [t]) when ls_equal ls (find_ls ~pure:true env "old") ->
       let t = old_label_term env lab t in (* NECESSARY? *)
-      t_app (find_ls ~pure:true env "at") [t; t_var lab] t.t_ty
+      e_app (find_ls ~pure:true env "at") [t; t_var lab] t.t_ty
   | _ ->
       t_map (old_label_term env lab) (old_label env lab) t
 
@@ -309,7 +309,7 @@ let default_exns_post ef =
   List.map default_exn_post xs
 
 let term_at env lab t =
-  t_app (find_ls ~pure:true env "at") [t; t_var lab] t.t_ty
+  e_app (find_ls ~pure:true env "at") [t; t_var lab] t.t_ty
 
 let wp_expl l f =
   f_label ?loc:f.f_loc (("expl:"^l)::Split_goal.stop_split::f.f_label) f
@@ -576,7 +576,7 @@ let rec t_btop env t = match t.t_node with
       f_equ t (t_True env)
 
 and f_btop env f = match f.f_node with
-  | Fapp (ls, [{t_ty = {ty_node = Tyapp (ts, [])}} as l; r])
+  | Fapp (ls, [{t_ty = Some {ty_node = Tyapp (ts, [])}} as l; r])
   when ls_equal ls ps_equ && ts_equal ts (find_ts ~pure:true env "bool") ->
       f_label_copy f (f_iff_simp (t_btop env l) (t_btop env r))
   | _ -> f_map (fun t -> t) (f_btop env) f

src/transform/abstraction.ml

@@ -35,8 +35,8 @@ let abstraction (keep : lsymbol -> bool) =
         t_map abstract_term abstract_fmla t
     | _ ->
         let (ls, tabs) = try Hterm_alpha.find term_table t with Not_found ->
-          let ls = create_fsymbol (id_fresh "abstr") [] t.t_ty in
-          let tabs = t_app ls [] t.t_ty in
+          let ls = create_lsymbol (id_fresh "abstr") [] t.t_ty in
+          let tabs = e_app ls [] t.t_ty in
           Hterm_alpha.add term_table t (ls, tabs);
           ls, tabs in
         extra_decls := ls :: !extra_decls;

src/transform/eliminate_algebraic.ml

@@ -93,13 +93,13 @@ let rec rewriteT kn state t = match t.t_node with
       in
       let w,m = List.fold_left mk_br (None,Mls.empty) bl in
       let find cs = try Mls.find cs m with Not_found -> of_option w in
-      let ts = match t1.t_ty.ty_node with
-        | Tyapp (ts,_) -> ts
+      let ts = match t1.t_ty with
+        | Some { ty_node = Tyapp (ts,_) } -> ts
         | _ -> Printer.unsupportedTerm t uncompiled
       in
       begin match List.map find (find_constructors kn ts) with
         | [t] -> t
-        | tl  -> t_app (Mts.find ts state.mt_map) (t1::tl) t.t_ty
+        | tl  -> e_app (Mts.find ts state.mt_map) (t1::tl) t.t_ty
       end
   | _ ->
       t_map (rewriteT kn state) (rewriteF kn state Svs.empty true) t
@@ -126,10 +126,10 @@ and rewriteF kn state av sign f = match f.f_node with
       let find cs =
         let vl,e = try Mls.find cs m with Not_found ->
           let var = create_vsymbol (id_fresh "w") in
-          let get_var pj = var (t_app_infer pj [t1]).t_ty in
+          let get_var pj = var (t_type (t_app_infer pj [t1])) in
           List.map get_var (Mls.find cs state.pj_map), of_option w
         in
-        let hd = t_app cs (List.map t_var vl) t1.t_ty in
+        let hd = e_app cs (List.map t_var vl) t1.t_ty in
         match t1.t_node with
         | Tvar v when Svs.mem v av ->
             let hd = f_let_close_simp v hd e in if sign
@@ -140,8 +140,8 @@ and rewriteF kn state av sign f = match f.f_node with
             then f_forall_close_simp vl [] (f_implies_simp hd e)
             else f_exists_close_simp vl [] (f_and_simp     hd e)
       in
-      let ts = match t1.t_ty.ty_node with
-        | Tyapp (ts,_) -> ts
+      let ts = match t1.t_ty with
+        | Some { ty_node = Tyapp (ts,_) } -> ts
         | _ -> Printer.unsupportedFmla f uncompiled
       in
       let op = if sign then f_and_simp else f_or_simp in
@@ -246,11 +246,11 @@ let add_projections (state,task) _ts _ty csl =
     let c = ref 0 in
     let add (pjl,tsk) t =
       let id = id_derive (id ^ (incr c; string_of_int !c)) cs.ls_name in
-      let ls = create_fsymbol id [of_option cs.ls_value] t.t_ty in
+      let ls = create_lsymbol id [of_option cs.ls_value] t.t_ty in
       let tsk = add_decl tsk (create_logic_decl [ls, None]) in
       let id = id_derive (ls.ls_name.id_string ^ "_def") ls.ls_name in
       let pr = create_prsymbol id in
-      let hh = t_app ls [hd] t.t_ty in
+      let hh = e_app ls [hd] t.t_ty in
       let ax = f_forall_close (List.rev vl) [] (f_equ hh t) in
       ls::pjl, add_decl tsk (create_prop_decl Paxiom pr ax)
     in

src/transform/eliminate_definition.ml

@@ -85,7 +85,7 @@ let add_ld func pred axl d = match d with
       let vl,e = open_ls_defn ld in begin match e with
         | Term t when func ->
             let nm = ls.ls_name.id_string ^ "_def" in
-            let hd = t_app ls (List.map t_var vl) t.t_ty in
+            let hd = e_app ls (List.map t_var vl) t.t_ty in
             let ax = f_forall_close vl [] (t_insert hd t) in
             let pr = create_prsymbol (id_derive nm ls.ls_name) in
             create_prop_decl Paxiom pr ax :: axl, (ls, None)

src/transform/eliminate_if.ml

@@ -76,7 +76,7 @@ let add_ld axl d = match d with
         | Term t when has_if t ->
             let nm = ls.ls_name.id_string ^ "_def" in
             let pr = create_prsymbol (id_derive nm ls.ls_name) in
-            let hd = t_app ls (List.map t_var vl) t.t_ty in
+            let hd = e_app ls (List.map t_var vl) t.t_ty in
             let f = f_forall_close vl [] (elim_f (f_equ hd t)) in
             create_prop_decl Paxiom pr f :: axl, (ls, None)
         | _ ->

src/transform/encoding_bridge.ml

@@ -130,7 +130,7 @@ let conv_ls tenv ls =
 
 (* Convert the argument of a function use the bridge if needed*)
 let conv_arg tenv t aty =
-  let tty = t.t_ty in
+  let tty = t_type t in
   if ty_equal tty aty then t else
     try
       (* polymorph specials t2tb *)
@@ -168,7 +168,7 @@ let rec rewrite_term tenv vsvar t =
         let tl = List.map (fnT vsvar) tl in
         let p = Hls.find tenv.trans_lsymbol p in
         let tl = List.map2 (conv_arg tenv) tl p.ls_args in
-        conv_res_app tenv p tl t.t_ty
+        conv_res_app tenv p tl (t_type t)
     | Tlet (t1, b) ->
         let u,t2,close = t_open_bound_cb b in
         let t1 = fnT vsvar t1 in

src/transform/encoding_decorate.ml

@@ -33,12 +33,12 @@ let ls_poly_deco =
 
 let rec deco_arg kept tvar t =
   let t = deco_term kept tvar t in
-  if Sty.mem t.t_ty kept then t else
-  let tty = term_of_ty tvar t.t_ty in
-  t_app ls_poly_deco [tty;t] t.t_ty
+  if Sty.mem (t_type t) kept then t else
+  let tty = term_of_ty tvar (t_type t) in
+  e_app ls_poly_deco [tty;t] t.t_ty
 
 and deco_term kept tvar t = match t.t_node with
-  | Tapp (fs,tl) -> t_app fs (List.map (deco_arg kept tvar) tl) t.t_ty
+  | Tapp (fs,tl) -> e_app fs (List.map (deco_arg kept tvar) tl) t.t_ty
   | _ -> t_map (deco_term kept tvar) (deco_fmla kept tvar) t
 
 and deco_fmla kept tvar f = match f.f_node with

src/transform/encoding_distinction.ml

@@ -118,9 +118,9 @@ let rec rewrite_term env tvar vsvar t =
     | Tvar x -> Mvs.find x vsvar
     | Tapp(p,tl) ->
       let tl = List.map (fnT vsvar) tl in