merge the types [term] and [fmla]

Rename as little as possible and keep the API.
Make all the necessary checks in Term and Decl.
Remove the duplicate code in Term but keep it elsewhere.
We will factorize the code as we go, without rush.

src/core/decl.ml

@@ -40,7 +40,7 @@ type logic_decl = lsymbol * ls_defn option
 exception UnboundVar of vsymbol
 
 let check_fvs f =
-  let fvs = f_freevars Svs.empty f in
+  let fvs = f_freevars Svs.empty (t_prop f) in
   Svs.iter (fun vs -> raise (UnboundVar vs)) fvs;
   f
 
@@ -52,7 +52,7 @@ let check_tl ty t = check_ty ty (t_type t)
 let make_fs_defn fs vl t =
   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_oty_equal fs.ls_value t.t_ty;
+  check_t_ty fs.ls_value t;
   List.iter2 check_vl fs.ls_args vl;
   fs, Some (fs, check_fvs fd)
 
@@ -66,8 +66,8 @@ let make_ls_defn ls vl = e_apply (make_fs_defn ls vl) (make_ps_defn ls vl)
 
 let open_ls_defn (_,f) =
   let vl, ef = f_open_forall f in
-  match ef.f_node with
-    | Fapp (_, [_; t2]) -> vl, Term t2
+  match ef.t_node with
+    | Tapp (_, [_; t2]) -> vl, Term t2
     | Fbinop (_, _, f2) -> vl, Fmla f2
     | _ -> assert false
 
@@ -138,13 +138,13 @@ let build_call_graph cgr syms ls =
           let vml = match_term vm e [vm] p in
           List.iter (fun vm -> term vm () t) vml) bl
     | _ -> t_fold (term vm) (fmla vm) () t
-  and fmla vm () f = match f.f_node with
-    | Fapp (s,tl) when Mls.mem s syms ->
+  and fmla vm () f = match f.t_node with
+    | Tapp (s,tl) when Mls.mem s syms ->
         f_fold (term vm) (fmla vm) () f; call vm s tl
-    | Flet ({t_node = Tvar v}, b) when Mvs.mem v vm ->
+    | Tlet ({t_node = Tvar v}, b) when Mvs.mem v vm ->
         let u,e = f_open_bound b in
         fmla (Mvs.add u (Mvs.find v vm) vm) () e
-    | Fcase (e,bl) ->
+    | Tcase (e,bl) ->
         term vm () e; List.iter (fun b ->
           let p,f = f_open_branch b in
           let vml = match_term vm e [vm] p in
@@ -454,16 +454,16 @@ exception Found of lsymbol
 let ls_mem s sps = if Sls.mem s sps then raise (Found s) else false
 let t_pos_ps sps = t_s_all (fun _ -> true) (fun s -> not (ls_mem s sps))
 
-let rec f_pos_ps sps pol f = match f.f_node, pol with
-  | Fapp (s, _), Some false when ls_mem s sps -> false
-  | Fapp (s, _), None when ls_mem s sps -> false
+let rec f_pos_ps sps pol f = match f.t_node, pol with
+  | Tapp (s, _), Some false when ls_mem s sps -> false
+  | Tapp (s, _), None when ls_mem s sps -> false
   | Fbinop (Fiff, f, g), _ ->
       f_pos_ps sps None f && f_pos_ps sps None g
   | Fbinop (Fimplies, f, g), _ ->
       f_pos_ps sps (option_map not pol) f && f_pos_ps sps pol g
   | Fnot f, _ ->
       f_pos_ps sps (option_map not pol) f
-  | Fif (f,g,h), _ ->
+  | Tif (f,g,h), _ ->
       f_pos_ps sps None f && f_pos_ps sps pol g && f_pos_ps sps pol h
   | _ -> f_all (t_pos_ps sps) (f_pos_ps sps pol) f
 
@@ -472,15 +472,15 @@ let create_ind_decl idl =
   let add acc (ps,_) = Sls.add ps acc in
   let sps = List.fold_left add Sls.empty idl in
   let check_ax ps (syms,news) (pr,f) =
-    let rec clause acc f = match f.f_node with
+    let rec clause acc f = match f.t_node with
       | Fquant (Fforall, f) ->
           let _,_,f = f_open_quant f in clause acc f
       | Fbinop (Fimplies, g, f) -> clause (g::acc) f
       | _ -> (acc, f)
     in
     let cls, f = clause [] (check_fvs f) in
-    match f.f_node with
-      | Fapp (s, tl) when ls_equal s ps ->
+    match f.t_node with
+      | Tapp (s, tl) when ls_equal s ps ->
           List.iter2 check_tl ps.ls_args tl;
           (try ignore (List.for_all (f_pos_ps sps (Some true)) cls)
           with Found ls -> raise (NonPositiveIndDecl (ps, pr, ls)));
@@ -640,8 +640,8 @@ let rec check_matchT kn () t = match t.t_node with
       t_fold (check_matchT kn) (check_matchF kn) () t
   | _ -> t_fold (check_matchT kn) (check_matchF kn) () t
 
-and check_matchF kn () f = match f.f_node with
-  | Fcase (t1,bl) ->
+and check_matchF kn () f = match f.t_node with
+  | Tcase (t1,bl) ->
       let bl = List.map (fun b -> let p,f = f_open_branch b in [p],f) bl in
       ignore (try Pattern.CompileFmla.compile (find_constructors kn) [t1] bl
       with Pattern.NonExhaustive p -> raise (NonExhaustiveExpr (p,Fmla f)));

src/core/env.mli

@@ -28,7 +28,7 @@ val env_tag : env -> Hashweak.tag
 module Wenv : Hashweak.S with type key = env
 
 type retrieve_channel = string list -> string * in_channel
-  (** retrieves a channel from a given path; a filename is also returned, 
+  (** retrieves a channel from a given path; a filename is also returned,
       for printing purposes only *)
 
 type retrieve_theory  = env -> string list -> theory Mnm.t

src/core/pretty.ml

@@ -199,7 +199,7 @@ and print_lterm pri fmt t = match t.t_label with
   | ll -> fprintf fmt (protect_on (pri > 0) "%a %a")
       (print_list space print_label) ll (print_tnode 0) t
 
-and print_lfmla pri fmt f = match f.f_label with
+and print_lfmla pri fmt f = match f.t_label with
   | _ when Debug.nottest_flag debug_print_labels
        -> print_fnode pri fmt f
   | [] -> print_fnode pri fmt f
@@ -250,9 +250,10 @@ and print_tnode pri fmt t = match t.t_node with
       fprintf fmt (protect_on (pri > 0) "epsilon %a.@ %a")
         print_vsty v print_fmla f;
       forget_var v
+  | Fquant _ | Fbinop _ | Fnot _ | Ftrue | Ffalse -> raise (TermExpected t)
 
-and print_fnode pri fmt f = match f.f_node with
-  | Fapp (ps,tl) ->
+and print_fnode pri fmt f = match f.t_node with
+  | Tapp (ps,tl) ->
       print_app pri ps fmt tl
   | Fquant (q,fq) ->
       let vl,tl,f = f_open_quant fq in
@@ -269,17 +270,18 @@ and print_fnode pri fmt f = match f.f_node with
         (print_lfmla (p + 1)) f1 print_binop b (print_lfmla p) f2
   | Fnot f ->
       fprintf fmt (protect_on (pri > 4) "not %a") (print_lfmla 4) f
-  | Fif (f1,f2,f3) ->
+  | Tif (f1,f2,f3) ->
       fprintf fmt (protect_on (pri > 0) "if @[%a@] then %a@ else %a")
         print_fmla f1 print_fmla f2 print_fmla f3
-  | Flet (t,f) ->
+  | Tlet (t,f) ->
       let v,f = f_open_bound f in
       fprintf fmt (protect_on (pri > 0) "let %a = @[%a@] in@ %a")
         print_vs v (print_lterm 4) t print_fmla f;
       forget_var v
-  | Fcase (t,bl) ->
+  | Tcase (t,bl) ->
       fprintf fmt "match @[%a@] with@\n@[<hov>%a@]@\nend"
         print_term t (print_list newline print_fbranch) bl
+  | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
 
 and print_tbranch fmt br =
   let p,t = t_open_branch br in
@@ -511,7 +513,7 @@ let () = Exn_printer.register
   | 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
+      fprintf fmt "Not a term: %a" print_fmla t
   | Term.FmlaExpected t ->
       fprintf fmt "Not a formula: %a" print_term t
   | Term.NoMatch ->

src/core/term.mli

@@ -135,14 +135,6 @@ type term = private {
   t_tag   : int;
 }
 
-and fmla = private {
-  f_node  : fmla_node;
-  f_label : label list;
-  f_loc   : Loc.position option;
-  f_vars  : Svs.t;
-  f_tag   : int;
-}
-
 and term_node = private
   | Tvar of vsymbol
   | Tconst of constant
@@ -151,27 +143,22 @@ and term_node = private
   | Tlet of term * term_bound
   | Tcase of term * term_branch list
   | Teps of fmla_bound
-
-and fmla_node = private
-  | Fapp of lsymbol * term list
   | Fquant of quant * fmla_quant
   | Fbinop of binop * fmla * fmla
   | Fnot of fmla
   | Ftrue
   | Ffalse
-  | Fif of fmla * fmla * fmla
-  | Flet of term * fmla_bound
-  | Fcase of term * fmla_branch list
 
-and term_bound
-
-and fmla_bound
+and fmla = term
 
-and fmla_quant
+and term_bound
+and fmla_bound = term_bound
 
 and term_branch
+and fmla_branch = term_branch
 
-and fmla_branch
+and term_quant
+and fmla_quant = term_quant
 
 and expr =
   | Term of term
@@ -239,6 +226,7 @@ val f_open_quant_cb :
 
 (** compute type instance *)
 
+val ls_arg_inst : lsymbol -> term list -> 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
@@ -250,6 +238,8 @@ exception FmlaExpected of term
 
 val e_app : lsymbol -> term list -> oty -> term
 val t_type : term -> ty
+val t_prop : term -> term
+val check_t_ty : oty -> term -> unit
 
 (** Smart constructors for term *)
 

src/core/theory.ml

@@ -533,15 +533,15 @@ let cl_type cl inst tdl =
 
 let extract_ls_defn f =
   let vl, ef = f_open_forall f in
-  match ef.f_node with
-    | Fapp (s, [t1; t2]) when ls_equal s ps_equ ->
+  match ef.t_node with
+    | Tapp (s, [t1; t2]) when ls_equal s ps_equ ->
         begin match t1.t_node with
           | Tapp (fs, _) -> make_fs_defn fs vl t2
           | _ -> assert false
         end
     | Fbinop (Fiff, f1, f2) ->
-        begin match f1.f_node with
-          | Fapp (ps, _) -> make_ps_defn ps vl f2
+        begin match f1.t_node with
+          | Tapp (ps, _) -> make_ps_defn ps vl f2
           | _ -> assert false
         end
     | _ -> assert false

src/core/ty.ml

@@ -268,8 +268,3 @@ 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

@@ -100,6 +100,8 @@ val ty_inst  : ty Mtv.t -> ty -> ty
 
 val ty_freevars : Stv.t -> ty -> Stv.t
 
+val check_ty_equal : ty -> ty -> unit
+
 (* built-in symbols *)
 
 val ts_int  : tysymbol
@@ -142,6 +144,3 @@ 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/ide/gmain.ml

@@ -728,16 +728,16 @@ let info_window ?(callback=(fun () -> ())) mt s =
   let expl_regexp = Str.regexp "expl:\\(.*\\)"
 
   let rec get_labels f =
-    (match f.Term.f_node with
+    (match f.Term.t_node with
       | Term.Fbinop(Term.Fimplies,_,f) -> get_labels f
       | Term.Fquant(Term.Fforall,fq) ->
 	  let (_,_,f) = Term.f_open_quant fq in get_labels f
-      | Term.Flet(_,fb) ->
-	  let (_,f) = Term.f_open_bound fb in get_labels f
-      | Term.Fcase(_,[fb]) ->
-	  let (_,f) = Term.f_open_branch fb in get_labels f
+      | Term.Tlet(_,fb) ->
+	  let (_,f) = Term.t_open_bound fb in get_labels f
+      | Term.Tcase(_,[fb]) ->
+	  let (_,f) = Term.t_open_branch fb in get_labels f
       | _ -> [])
-    @ f.Term.f_label
+    @ f.Term.t_label
 
   let get_explanation id fmla =
     let r = ref None in
@@ -2070,8 +2070,8 @@ let color_loc loc =
   if f = !current_file then color_loc source_view l b e
 
 let rec color_f_locs () f =
-  Util.option_iter color_loc f.Term.f_loc;
-  Term.f_fold color_t_locs color_f_locs () f
+  Util.option_iter color_loc f.Term.t_loc;
+  Term.t_fold color_t_locs color_f_locs () f
 
 and color_t_locs () t =
   Util.option_iter color_loc t.Term.t_loc;

src/ide/newmain.ml

@@ -1093,8 +1093,8 @@ let color_loc ~color loc =
   if f = !current_file then color_loc ~color source_view l b e
 
 let rec color_f_locs () f =
-  Util.option_iter (color_loc ~color:location_tag) f.Term.f_loc;
-  Term.f_fold color_t_locs color_f_locs () f
+  Util.option_iter (color_loc ~color:location_tag) f.Term.t_loc;
+  Term.t_fold color_t_locs color_f_locs () f
 
 and color_t_locs () t =
   Util.option_iter (color_loc ~color:location_tag) t.Term.t_loc;

src/ide/session.ml

@@ -528,16 +528,16 @@ let schedule_edit_proof ~debug:_ ~editor ~file ~driver ~callback goal =
   let expl_regexp = Str.regexp "expl:\\(.*\\)"
 
   let rec get_labels f =
-    (match f.Term.f_node with
+    (match f.Term.t_node with
       | Term.Fbinop(Term.Fimplies,_,f) -> get_labels f
       | Term.Fquant(Term.Fforall,fq) ->
 	  let (_,_,f) = Term.f_open_quant fq in get_labels f
-      | Term.Flet(_,fb) ->
-	  let (_,f) = Term.f_open_bound fb in get_labels f
-      | Term.Fcase(_,[fb]) ->
-	  let (_,f) = Term.f_open_branch fb in get_labels f
+      | Term.Tlet(_,fb) ->
+	  let (_,f) = Term.t_open_bound fb in get_labels f
+      | Term.Tcase(_,[fb]) ->
+	  let (_,f) = Term.t_open_branch fb in get_labels f
       | _ -> [])
-    @ f.Term.f_label
+    @ f.Term.t_label
 
   let get_explanation id fmla =
     let r = ref None in

src/parser/denv.ml

@@ -348,14 +348,16 @@ and specialize_term_node ~loc htv = function
       let v, f = f_open_bound fb in
       Teps (ident_of_vs ~loc v, specialize_ty ~loc htv v.vs_ty,
 	    specialize_fmla ~loc htv f)
+  | Term.Fquant _ | Term.Fbinop _ | Term.Fnot _
+  | Term.Ftrue | Term.Ffalse -> assert false
 
 and specialize_fmla ~loc htv f =
-  let df = specialize_fmla_node ~loc htv f.f_node in
-  let df = option_apply df (fun p -> Fnamed (Lpos p,df)) f.f_loc in
-  List.fold_left (fun f l -> Fnamed (Lstr l, f)) df f.f_label
+  let df = specialize_fmla_node ~loc htv f.t_node in
+  let df = option_apply df (fun p -> Fnamed (Lpos p,df)) f.t_loc in
+  List.fold_left (fun f l -> Fnamed (Lstr l, f)) df f.t_label
 
 and specialize_fmla_node ~loc htv = function
-  | Term.Fapp (ls, tl) ->
+  | Term.Tapp (ls, tl) ->
       Fapp (ls, List.map (specialize_term ~loc htv) tl)
   | Term.Fquant (q, fq) ->
       let vl, tl, f = f_open_quant fq in
@@ -370,18 +372,19 @@ and specialize_fmla_node ~loc htv = function
       Ftrue
   | Term.Ffalse ->
       Ffalse
-  | Term.Fif (f1, f2, f3) ->
+  | Term.Tif (f1, f2, f3) ->
       Fif (specialize_fmla ~loc htv f1,
 	   specialize_fmla ~loc htv f2, specialize_fmla ~loc htv f3)
-  | Term.Flet (t1, f2b) ->
+  | Term.Tlet (t1, f2b) ->
       let v, f2 = f_open_bound f2b in
       Flet (specialize_term ~loc htv t1,
 	    ident_of_vs ~loc v, specialize_fmla ~loc htv f2)
-  | Term.Fcase (t, fbl) ->
+  | Term.Tcase (t, fbl) ->
       let branch b = let p, f = f_open_branch b in
 	specialize_pattern ~loc htv p, specialize_fmla ~loc htv f
       in
       Fmatch (specialize_term ~loc htv t, List.map branch fbl)
+  | Term.Tvar _ | Term.Tconst _ | Term.Teps _ -> assert false
 
 and specialize_trigger ~loc htv = function
   | Term.Term t -> TRterm (specialize_term ~loc htv t)

src/printer/alt_ergo.ml

@@ -88,15 +88,16 @@ let rec print_term info fmt t = match t.t_node with
       "alt-ergo : you must eliminate match"
   | Teps _ -> unsupportedTerm t
       "alt-ergo : you must eliminate epsilon"
+  | Fquant _ | Fbinop _ | Fnot _ | Ftrue | Ffalse -> raise (TermExpected t)
 
 and print_tapp info fmt = function
   | [] -> ()
   | tl -> fprintf fmt "(%a)" (print_list comma (print_term info)) tl
 
-let rec print_fmla info fmt f = match f.f_node with
-  | Fapp ({ ls_name = id }, []) ->
+let rec print_fmla info fmt f = match f.t_node with
+  | Tapp ({ ls_name = id }, []) ->
       print_ident fmt id
-  | Fapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
+  | Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
       | Some s -> syntax_arguments s (print_term info) fmt tl
       | None -> fprintf fmt "%a(%a)" print_ident ls.ls_name
                     (print_list comma (print_term info)) tl
@@ -127,14 +128,15 @@ let rec print_fmla info fmt f = match f.f_node with
       fprintf fmt "true"
   | Ffalse ->
       fprintf fmt "false"
-  | Fif (f1, f2, f3) ->
+  | Tif (f1, f2, f3) ->
       fprintf fmt "((%a and %a) or (not %a and %a))"
 	(print_fmla info) f1 (print_fmla info) f2 (print_fmla info)
         f1 (print_fmla info) f3
-  | Flet _ -> unsupportedFmla f
+  | Tlet _ -> unsupportedFmla f
       "alt-ergo : you must eliminate let in formula"
-  | Fcase _ -> unsupportedFmla f
+  | Tcase _ -> unsupportedFmla f
       "alt-ergo : you must eliminate match"
+  | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
 
 
 and print_expr info fmt = e_apply (print_term info fmt) (print_fmla info fmt)
@@ -142,7 +144,7 @@ and print_expr info fmt = e_apply (print_term info fmt) (print_fmla info fmt)
 and print_triggers info fmt tl =
   let filter = function
     | Term _ -> true
-    | Fmla {f_node = Fapp (ps,_)} -> not (ls_equal ps ps_equ)
+    | Fmla {t_node = Tapp (ps,_)} -> not (ls_equal ps ps_equ)
     | _ -> false in
   let tl = List.map (List.filter filter) tl in
   let tl = List.filter (function [] -> false | _::_ -> true) tl in

src/printer/coq.ml

@@ -199,7 +199,7 @@ and print_lrterm opl opr info fmt t = match t.t_label with
       (print_list space print_label) ll (print_tnode false false info) t
 *)
 
-and print_lrfmla opl opr info fmt f = match f.f_label with
+and print_lrfmla opl opr info fmt f = match f.t_label with
   | _ -> print_fnode opl opr info fmt f
 (*
   | [] -> print_fnode opl opr info fmt f
@@ -243,8 +243,9 @@ and print_tnode opl opr info fmt t = match t.t_node with
           else fprintf fmt (protect_on opl "(%a%a:%a)") print_ls fs
             (print_paren_r (print_term info)) tl (print_ty info) (t_type t)
     end
+  | Fquant _ | Fbinop _ | Fnot _ | Ftrue | Ffalse -> raise (TermExpected t)
 
-and print_fnode opl opr info fmt f = match f.f_node with
+and print_fnode opl opr info fmt f = match f.t_node with
   | Fquant (Fforall,fq) ->
       let vl,_tl,f = f_open_quant fq in
       fprintf fmt (protect_on opr "forall %a,@ %a")
@@ -272,24 +273,25 @@ and print_fnode opl opr info fmt f = match f.f_node with
         (print_opr_fmla info) f1 print_binop b (print_opl_fmla info) f2
   | Fnot f ->
       fprintf fmt (protect_on opr "~ %a") (print_opl_fmla info) f
-  | Flet (t,f) ->
+  | Tlet (t,f) ->
       let v,f = f_open_bound f in
       fprintf fmt (protect_on opr "let %a :=@ %a in@ %a")
         print_vs v (print_opl_term info) t (print_opl_fmla info) f;
       forget_var v
-  | Fcase (t,bl) ->
+  | Tcase (t,bl) ->
       fprintf fmt "match %a with@\n@[<hov>%a@]@\nend"
         (print_term info) t
         (print_list newline (print_fbranch info)) bl
-  | Fif (f1,f2,f3) ->
+  | Tif (f1,f2,f3) ->
       fprintf fmt (protect_on opr "if %a@ then %a@ else %a")
         (print_fmla info) f1 (print_fmla info) f2 (print_opl_fmla info) f3
-  | Fapp (ps, tl) ->
+  | Tapp (ps, tl) ->
     begin match query_syntax info.info_syn ps.ls_name with
       | Some s -> syntax_arguments s (print_term info) fmt tl
       | _ -> fprintf fmt "(%a %a)" print_ls ps
           (print_space_list (print_term info)) tl
     end
+  | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
 
 and print_tbranch info fmt br =
   let p,t = t_open_branch br in

src/printer/cvc3.ml

@@ -158,11 +158,12 @@ let rec print_term info fmt t = match t.t_node with
       "cvc3 : you must eliminate match"
   | Teps _ -> unsupportedTerm t
       "cvc3 : you must eliminate epsilon"
+  | Fquant _ | Fbinop _ | Fnot _ | Ftrue | Ffalse -> raise (TermExpected t)
 
-and print_fmla info fmt f = match f.f_node with
-  | Fapp ({ ls_name = id }, []) ->
+and print_fmla info fmt f = match f.t_node with
+  | Tapp ({ ls_name = id }, []) ->
       print_ident fmt id
-  | Fapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
+  | Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
       | Some s -> syntax_arguments_typed s (print_term info)
         (print_type info) None fmt tl
       | None -> begin match tl with
@@ -202,16 +203,17 @@ and print_fmla info fmt f = match f.f_node with
       fprintf fmt "TRUE"
   | Ffalse ->
       fprintf fmt "FALSE"
-  | Fif (f1, f2, f3) ->
+  | Tif (f1, f2, f3) ->
       fprintf fmt "@[(IF %a@ THEN %a@ ELSE %a ENDIF)@]"
 	(print_fmla info) f1 (print_fmla info) f2 (print_fmla info) f3
-  | Flet (t1, tb) ->
+  | Tlet (t1, tb) ->
       let v, f2 = f_open_bound tb in
       fprintf fmt "@[(LET %a =@ %a IN@ %a)@]" print_var v
         (print_term info) t1 (print_fmla info) f2;
       forget_var v
-  | Fcase _ -> unsupportedFmla f
+  | Tcase _ -> unsupportedFmla f
       "cvc3 : you must eliminate match"
+  | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
 
 and print_expr info fmt = e_apply (print_term info fmt) (print_fmla info fmt)
 

src/printer/gappa.ml

@@ -152,6 +152,7 @@ let rec print_term info fmt t =
       "gappa: you must eliminate match"
   | Teps _ -> unsupportedTerm t
       "gappa : you must eliminate epsilon"
+  | Fquant _ | Fbinop _ | Fnot _ | Ftrue | Ffalse -> raise (TermExpected t)
 
 
 (* predicates *)
@@ -159,13 +160,13 @@ let rec print_term info fmt t =
 let rec print_fmla info fmt f =
   let term = print_term info in
   let fmla = print_fmla info in
-  match f.f_node with
-  | Fapp ({ ls_name = id }, []) ->
+  match f.t_node with
+  | Tapp ({ ls_name = id }, []) ->
     begin match query_syntax info.info_syn id with
       | Some s -> syntax_arguments s term fmt []
       | None -> print_ident fmt id
     end
-  | Fapp (ls, [t1;t2]) when ls_equal ls ps_equ ->
+  | Tapp (ls, [t1;t2]) when ls_equal ls ps_equ ->
       (* TODO: distinguish between type of t1 and t2 
          the following is OK only for real of integer
       *)
@@ -179,7 +180,7 @@ let rec print_fmla info fmt f =
         with Not_found ->
           fprintf fmt "%a - %a in [0,0]" term t1 term t2
       end
-  | Fapp (ls, [t1;t2]) when Mls.mem ls info.info_ops_of_rel ->
+  | Tapp (ls, [t1;t2]) when Mls.mem ls info.info_ops_of_rel ->
       let s,op,rev_op = try Mls.find ls info.info_ops_of_rel
 	with Not_found -> assert false
       in
@@ -193,7 +194,7 @@ let rec print_fmla info fmt f =
         with Not_found ->
           fprintf fmt "%s%a - %a %s 0" s term t1 term t2 op
       end
-  | Fapp (ls, tl) ->
+  | Tapp (ls, tl) ->
       begin match query_syntax info.info_syn ls.ls_name with
 	| Some s -> syntax_arguments s term fmt tl
 	| None ->
@@ -228,13 +229,14 @@ let rec print_fmla info fmt f =
       fprintf fmt "(0 in [0,0])"
   | Ffalse ->
       fprintf fmt "(1 in [0,0])"
-  | Fif (_f1, _f2, _f3) ->
+  | Tif (_f1, _f2, _f3) ->
       unsupportedFmla f
         "gappa: you must eliminate if in formula"
-  | Flet _ -> unsupportedFmla f
+  | Tlet _ -> unsupportedFmla f
       "gappa: you must eliminate let in formula"
-  | Fcase _ -> unsupportedFmla f
+  | Tcase _ -> unsupportedFmla f
       "gappa: you must eliminate match"
+  | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
 
 (*
 let print_decl (* ?old *) info fmt d =
@@ -276,8 +278,8 @@ let print_decls ?old info fmt dl =
 exception AlreadyDefined
 
 let filter_hyp info defs eqs hyps pr f =
-  match f.f_node with
-  | Fapp(ls,[t1;t2]) when ls == ps_equ ->
+  match f.t_node with
+  | Tapp(ls,[t1;t2]) when ls == ps_equ ->
       let try_equality t1 t2 =
         match t1.t_node with
           | Tapp(l,[]) ->
@@ -294,7 +296,7 @@ let filter_hyp info defs eqs hyps pr f =
         (eqs, (pr,f)::hyps)
       end
   (* todo: support more kinds of hypotheses *)
-  | Fapp(ls,_) when Sid.mem ls.ls_name info.info_symbols ->