Support for strings literals

parent 188478ad
......@@ -25,6 +25,7 @@ valid "^unsat$"
theory BuiltIn
syntax type int "Int"
syntax type real "Real"
syntax type string "String"
syntax predicate (=) "(= %1 %2)"
meta "encoding:kept" type int
......@@ -196,3 +197,23 @@ theory map.Const
meta "encoding:lskept" function const
(* syntax function const "(const[%t0] %1)" *)
end
theory newstring.String
prelude ";;; SMT-LIB2: string theory"
syntax function concat2 "(str.++ %1 %2)"
syntax function concat3 "(str.++ %1 %2 %3)"
syntax function concat4 "(str.++ %1 %2 %3 %4)"
syntax function concat5 "(str.++ %1 %2 %3 %4 %5)"
syntax function length "(str.len %1)"
syntax function indexof "(str.indexof %1 %2 %3)"
syntax function replace "(str.replace %1 %2 %3)"
syntax function replaceall "(str.replaceall %1 %2 %3)"
syntax function substring "(str.substr %1 %2 %3)"
syntax function ([]) "(str.at %1 %2)"
syntax predicate contains "(str.contains %1 %2)"
syntax predicate prefixof "(str.prefixof %1 %2)"
syntax predicate suffixof "(str.suffixof %1 %2)"
end
......@@ -143,6 +143,8 @@ and print_term info fmt t = match t.t_node with
print_app info fmt ls tl t.t_ty
| Tconst c ->
print_number info fmt c
| Tsconst _ ->
unsupportedTerm t "TPTP does not support strings"
| Tlet (t1,tb) ->
let v,t2 = t_open_bound tb in
fprintf fmt "$let_tt(%a@ =@ %a,@ %a)"
......@@ -189,7 +191,7 @@ and print_fmla info fmt f = match f.t_node with
(print_fmla info) f1 (print_fmla info) t1 (print_fmla info) t2
| Tcase _ -> unsupportedTerm f
"TPTP does not support pattern matching, use eliminate_algebraic"
| Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
| Tvar _ | Tconst _ | Tsconst _ | Teps _ -> raise (FmlaExpected f)
let print_tvarg fmt tv = fprintf fmt "%a : $tType" print_tvar tv
let print_tvargs fmt tvs = print_iter1 Stv.iter comma print_tvarg fmt tvs
......@@ -385,6 +387,8 @@ and print_term info fmt t = match t.t_node with
print_app info fmt ls tl t.t_ty
| Tconst c ->
Number.print number_format fmt c
| Tsconst _ ->
unsupportedTerm t "TPTP does not support strings"
| Tlet _ -> unsupportedTerm t
"DFG does not support let, use eliminate_let"
| Tif _ -> unsupportedTerm t
......@@ -423,7 +427,7 @@ let rec print_fmla info fmt f = match f.t_node with
"DFG does not support if, use eliminate_if"
| Tcase _ -> unsupportedTerm f
"DFG does not support pattern matching, use eliminate_algebraic"
| Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
| Tvar _ | Tconst _ | Tsconst _ | Teps _ -> raise (FmlaExpected f)
let print_axiom info fmt d = match d.d_node with
| Dprop (Paxiom, pr, _) when Mid.mem pr.pr_name info.info_syn -> ()
......
......@@ -106,6 +106,7 @@ let rec dty_unify dty1 dty2 = match dty1,dty2 with
let dty_int = Duty ty_int
let dty_real = Duty ty_real
let dty_bool = Duty ty_bool
let dty_str = Duty ty_str
let protect_on x s = if x then "(" ^^ s ^^ ")" else s
......@@ -207,6 +208,7 @@ and dterm_node =
| DTvar of string * dty
| DTgvar of vsymbol
| DTconst of Number.constant * dty
| DTsconst of string
| DTapp of lsymbol * dterm list
| DTfapp of dterm * dterm
| DTif of dterm * dterm * dterm
......@@ -433,6 +435,8 @@ let dterm crcmap ?loc node =
mk_dty (Some (dty_of_ty vs.vs_ty))
| DTconst (_,dty) ->
mk_dty (Some dty)
| DTsconst _ ->
mk_dty (Some dty_str)
| DTapp (ls, dtl) when ls_equal ls ps_equ ->
let dtyl, dty = specialize_ls ls in
let max = max_dty crcmap dtl in
......@@ -623,6 +627,8 @@ and try_term strict keep_loc uloc env prop dty node =
t_var vs
| DTconst (c,dty) ->
t_const c (term_ty_of_dty ~strict dty)
| DTsconst s ->
t_sconst s
| DTapp (ls,[]) when ls_equal ls fs_bool_true ->
if prop then t_true else t_bool_true
| DTapp (ls,[]) when ls_equal ls fs_bool_false ->
......
......@@ -31,6 +31,7 @@ val dty_unify : dty -> dty -> unit (* raises Exit on failure *)
val dty_int : dty
val dty_real : dty
val dty_bool : dty
val dty_str : dty
val dty_fold : (tysymbol -> 'a list -> 'a) ->
(tvsymbol -> 'a) -> (int -> 'a) -> dty -> 'a
......@@ -70,6 +71,7 @@ and dterm_node =
| DTvar of string * dty
| DTgvar of vsymbol
| DTconst of Number.constant * dty
| DTsconst of string
| DTapp of lsymbol * dterm list
| DTfapp of dterm * dterm
| DTif of dterm * dterm * dterm
......
......@@ -354,6 +354,7 @@ and print_tnode pri fmt t = match t.t_node with
print_ty ty
| None -> assert false
end
| Tsconst s -> fprintf fmt "\"%s\"" s
| Tapp (_, [t1]) when Sattr.mem coercion_attr t.t_attrs &&
Debug.test_noflag debug_print_coercions ->
print_lterm pri fmt (t_attr_set t1.t_attrs t1)
......
......@@ -225,6 +225,7 @@ type term = {
and term_node =
| Tvar of vsymbol
| Tconst of Number.constant
| Tsconst of string
| Tapp of lsymbol * term list
| Tif of term * term * term
| Tlet of term * term_bound
......@@ -332,6 +333,8 @@ let t_compare trigger attr loc t1 t2 =
comp_raise (vs_compare v1 v2)
| Tconst c1, Tconst c2 ->
comp_raise (Number.compare_const c1 c2)
| Tsconst s1, Tsconst s2 ->
comp_raise (Pervasives.compare s1 s2)
| Tapp (s1,l1), Tapp (s2,l2) ->
comp_raise (ls_compare s1 s2);
List.iter2 (t_compare bnd vml1 vml2) l1 l2
......@@ -380,17 +383,18 @@ let t_compare trigger attr loc t1 t2 =
t_compare bnd vml1 vml2 f1 f2
| Ttrue, Ttrue -> ()
| Tfalse, Tfalse -> ()
| Tvar _, _ -> raise CompLT | _, Tvar _ -> raise CompGT
| Tconst _, _ -> raise CompLT | _, Tconst _ -> raise CompGT
| Tapp _, _ -> raise CompLT | _, Tapp _ -> raise CompGT
| Tif _, _ -> raise CompLT | _, Tif _ -> raise CompGT
| Tlet _, _ -> raise CompLT | _, Tlet _ -> raise CompGT
| Tcase _, _ -> raise CompLT | _, Tcase _ -> raise CompGT
| Teps _, _ -> raise CompLT | _, Teps _ -> raise CompGT
| Tquant _, _ -> raise CompLT | _, Tquant _ -> raise CompGT
| Tbinop _, _ -> raise CompLT | _, Tbinop _ -> raise CompGT
| Tnot _, _ -> raise CompLT | _, Tnot _ -> raise CompGT
| Ttrue, _ -> raise CompLT | _, Ttrue -> raise CompGT
| Tvar _, _ -> raise CompLT | _, Tvar _ -> raise CompGT
| Tconst _, _ -> raise CompLT | _, Tconst _ -> raise CompGT
| Tsconst _, _ -> raise CompLT | _, Tsconst _ -> raise CompGT
| Tapp _, _ -> raise CompLT | _, Tapp _ -> raise CompGT
| Tif _, _ -> raise CompLT | _, Tif _ -> raise CompGT
| Tlet _, _ -> raise CompLT | _, Tlet _ -> raise CompGT
| Tcase _, _ -> raise CompLT | _, Tcase _ -> raise CompGT
| Teps _, _ -> raise CompLT | _, Teps _ -> raise CompGT
| Tquant _, _ -> raise CompLT | _, Tquant _ -> raise CompGT
| Tbinop _, _ -> raise CompLT | _, Tbinop _ -> raise CompGT
| Tnot _, _ -> raise CompLT | _, Tnot _ -> raise CompGT
| Ttrue, _ -> raise CompLT | _, Ttrue -> raise CompGT
end
end in
try t_compare 0 [] [] t1 t2; 0
......@@ -450,6 +454,7 @@ let t_hash trigger attr t =
begin match t.t_node with
| Tvar v -> vs_hash v
| Tconst c -> Hashtbl.hash c
| Tsconst s -> Hashtbl.hash s
| Tapp (s,l) ->
Hashcons.combine_list (t_hash bnd vml) (ls_hash s) l
| Tif (f,t,e) ->
......@@ -574,7 +579,7 @@ let add_b_vars s (_,b,_) = vars_union s b.bv_vars
let rec t_vars t = match t.t_node with
| Tvar v -> Mvs.singleton v 1
| Tconst _ -> Mvs.empty
| Tconst _ | Tsconst _ -> Mvs.empty
| Tapp (_,tl) -> List.fold_left add_t_vars Mvs.empty tl
| Tif (f,t,e) -> add_t_vars (add_t_vars (t_vars f) t) e
| Tlet (t,bt) -> add_b_vars (t_vars t) bt
......@@ -601,6 +606,7 @@ let mk_term n ty = {
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_sconst s = mk_term (Tsconst s) (Some ty_str)
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
......@@ -630,7 +636,7 @@ let t_attr_copy s t =
let bound_map fn (u,b,e) = (u, bnd_map fn b, fn e)
let t_map_unsafe fn t = t_attr_copy t (match t.t_node with
| Tvar _ | Tconst _ -> t
| Tvar _ | Tconst _ | Tsconst _ -> t
| Tapp (f,tl) -> t_app f (List.map fn tl) t.t_ty
| Tif (f,t1,t2) -> t_if (fn f) (fn t1) (fn t2)
| Tlet (e,b) -> t_let (fn e) (bound_map fn b) t.t_ty
......@@ -646,7 +652,7 @@ let t_map_unsafe fn t = t_attr_copy t (match t.t_node with
let bound_fold fn acc (_,b,e) = fn (bnd_fold fn acc b) e
let t_fold_unsafe fn acc t = match t.t_node with
| Tvar _ | Tconst _ -> acc
| Tvar _ | Tconst _ | Tsconst _ -> acc
| Tapp (_,tl) -> List.fold_left fn acc tl
| Tif (f,t1,t2) -> fn (fn (fn acc f) t1) t2
| Tlet (e,b) -> fn (bound_fold fn acc b) e
......@@ -665,7 +671,7 @@ let bound_map_fold fn acc (u,b,e) =
acc, (u,b,e)
let t_map_fold_unsafe fn acc t = match t.t_node with
| Tvar _ | Tconst _ ->
| Tvar _ | Tconst _ | Tsconst _ ->
acc, t
| Tapp (f,tl) ->
let acc,sl = Lists.map_fold_left fn acc tl in
......@@ -1045,6 +1051,8 @@ let rec t_gen_map fnT fnL m t =
t_var u
| Tconst _ ->
t
| Tsconst _ ->
t
| Tapp (fs, tl) ->
t_app (fnL fs) (List.map fn tl) (Opt.map fnT t.t_ty)
| Tif (f, t1, t2) ->
......@@ -1104,7 +1112,7 @@ let rec t_gen_fold fnT fnL acc t =
let fn = t_gen_fold fnT fnL in
let acc = Opt.fold fnT acc t.t_ty in
match t.t_node with
| Tconst _ | Tvar _ -> acc
| Tsconst _ | Tconst _ | Tvar _ -> acc
| Tapp (f, tl) -> List.fold_left fn (fnL acc f) tl
| Tif (f, t1, t2) -> fn (fn (fn acc f) t1) t2
| Tlet (t1, (_,b,t2)) -> fn (bnd_fold fn (fn acc t1) b) t2
......@@ -1281,7 +1289,7 @@ let rec list_map_cont fnL contL = function
let t_map_cont fn contT t =
let contT e = contT (t_attr_copy t e) in
match t.t_node with
| Tvar _ | Tconst _ -> contT t
| Tvar _ | Tconst _ | Tsconst _ -> contT t
| Tapp (fs, tl) ->
let cont_app tl = contT (t_app fs tl t.t_ty) in
list_map_cont fn cont_app tl
......
......@@ -126,6 +126,7 @@ type term = private {
and term_node =
| Tvar of vsymbol
| Tconst of Number.constant
| Tsconst of string
| Tapp of lsymbol * term list
| Tif of term * term * term
| Tlet of term * term_bound
......@@ -223,6 +224,7 @@ val check_literal : Number.constant -> ty -> unit
val t_var : vsymbol -> term
val t_const : Number.constant -> ty -> term
val t_sconst : string -> term
val t_if : term -> term -> term -> term
val t_let : term -> term_bound -> term
val t_case : term -> term_branch list -> term
......
......@@ -919,6 +919,7 @@ let builtin_theory =
let uc = empty_theory (id_fresh "BuiltIn") ["why3";"BuiltIn"] in
let uc = add_ty_decl uc ts_int in
let uc = add_ty_decl uc ts_real in
let uc = add_ty_decl uc ts_str in
let uc = add_param_decl uc ps_equ in
close_theory uc
......
......@@ -256,13 +256,15 @@ let ty_match s ty1 ty2 =
(* built-in symbols *)
let ts_int = create_tysymbol (id_fresh "int") [] NoDef
let ts_real = create_tysymbol (id_fresh "real") [] NoDef
let ts_bool = create_tysymbol (id_fresh "bool") [] NoDef
let ts_int = create_tysymbol (id_fresh "int") [] NoDef
let ts_real = create_tysymbol (id_fresh "real") [] NoDef
let ts_bool = create_tysymbol (id_fresh "bool") [] NoDef
let ts_str = create_tysymbol (id_fresh "string" ) [] NoDef
let ty_int = ty_app ts_int []
let ty_real = ty_app ts_real []
let ty_bool = ty_app ts_bool []
let ty_str = ty_app ts_str []
let ts_func =
let tv_a = create_tvsymbol (id_fresh "a") in
......
......@@ -142,10 +142,12 @@ val ty_equal_check : ty -> ty -> unit
val ts_int : tysymbol
val ts_real : tysymbol
val ts_bool : tysymbol
val ts_str : tysymbol
val ty_int : ty
val ty_real : ty
val ty_bool : ty
val ty_str : ty
val ts_func : tysymbol
......
......@@ -765,11 +765,13 @@ let t_freepvs pvs t = pvs_of_vss pvs (t_vars t)
let its_int = its_of_ts ts_int true
let its_real = its_of_ts ts_real true
let its_bool = its_of_ts ts_bool true
let its_str = its_of_ts ts_str true
let its_func = its_of_ts ts_func true
let ity_int = ity_app its_int [] []
let ity_real = ity_app its_real [] []
let ity_bool = ity_app its_bool [] []
let ity_str = ity_app its_str [] []
let ity_func a b = ity_app its_func [a;b] []
let ity_pred a = ity_app its_func [a;ity_bool] []
......
......@@ -240,12 +240,14 @@ val ty_unit : ty
val its_int : itysymbol
val its_real : itysymbol
val its_bool : itysymbol
val its_str : itysymbol
val its_unit : itysymbol
val its_func : itysymbol
val ity_int : ity
val ity_real : ity
val ity_bool : ity
val ity_str : ity
val ity_unit : ity
val ity_func : ity -> ity -> ity
val ity_pred : ity -> ity (* ity_pred 'a == ity_func 'a ity_bool *)
......
......@@ -571,10 +571,12 @@ open Theory
Therefore we match the exact contents of th_decls, and crash if it
is not what we expect. *)
let pd_int, pd_real, pd_equ = match builtin_theory.th_decls with
| [{td_node = Decl di}; {td_node = Decl dr}; {td_node = Decl de}] ->
let pd_int, pd_real, pd_str, pd_equ = match builtin_theory.th_decls with
| [{td_node = Decl di}; {td_node = Decl dr};
{td_node = Decl ds}; {td_node = Decl de}] ->
mk_decl (PDtype [mk_itd its_int [] [] [] []]) [di],
mk_decl (PDtype [mk_itd its_real [] [] [] []]) [dr],
mk_decl (PDtype [mk_itd its_str [] [] [] []]) [ds],
mk_decl PDpure [de]
| _ -> assert false
......
......@@ -113,6 +113,7 @@ val pd_int : pdecl
val pd_real : pdecl
val pd_equ : pdecl
val pd_bool : pdecl
val pd_str : pdecl
val pd_tuple : int -> pdecl
val pd_func : pdecl
val pd_func_app : pdecl
......
......@@ -383,6 +383,7 @@ let builtin_module =
let uc = empty_module dummy_env (id_fresh "BuiltIn") ["why3";"BuiltIn"] in
let uc = add_pdecl_no_logic uc pd_int in
let uc = add_pdecl_no_logic uc pd_real in
let uc = add_pdecl_no_logic uc pd_str in
let uc = add_pdecl_no_logic uc pd_equ in
let m = close_module uc in
{ m with mod_theory = builtin_theory }
......
......@@ -240,6 +240,7 @@ let inspect kn tl =
c in
unwind c pjl
| Tconst _ -> V
| Tsconst _ -> V
| Tapp (ls,[t1;t2]) when ls_equal ls ps_equ ->
let c1 = down caps pjl t1 in
let c2 = down caps pjl t2 in
......@@ -456,6 +457,8 @@ let cap_of_term kn uf pins caps t =
unwind t (Mvs.find_def V v caps) pjl
| Tconst _ -> (* constants are valid *)
unroll t pjl, V
| Tsconst _ -> (* constants are valid *)
unroll t pjl, V
| Tapp (ls,[t1;t2]) when ls_equal ls ps_equ ->
let t1, c1 = down caps pjl t1 in
let t2, c2 = down caps pjl t2 in
......@@ -645,7 +648,7 @@ let uf_inter uf1 uf2 =
Mint.inter inter uf1 uf2
let rec inject kn uf pins caps pos f = match f.t_node with
| Tvar _ | Tconst _ | Teps _ -> assert false (* never *)
| Tvar _ | Tconst _ | Tsconst _ | Teps _ -> assert false (* never *)
| Tapp (ls,[t]) when pos && ls_equal ls ls_valid ->
let _, c = cap_of_term kn uf pins caps t in
let n = match c with
......
......@@ -756,6 +756,7 @@ term_arg_:
| qualid { Tident $1 }
| AMP qualid { Tasref $2 }
| numeral { Tconst $1 }
| STRING { Tsconst $1 }
| TRUE { Ttrue }
| FALSE { Tfalse }
| o = oppref ; a = term_arg { Tidapp (Qident o, [a]) }
......@@ -1120,6 +1121,7 @@ expr_arg_:
| qualid { Eident $1 }
| AMP qualid { Easref $2 }
| numeral { Econst $1 }
(* | string { Esconst $1 } *)
| TRUE { Etrue }
| FALSE { Efalse }
| o = oppref ; a = expr_arg { Eidapp (Qident o, [a]) }
......
......@@ -78,6 +78,7 @@ and term_desc =
| Ttrue
| Tfalse
| Tconst of Number.constant
| Tsconst of string
| Tident of qualid
| Tasref of qualid
| Tidapp of qualid * term list
......@@ -131,6 +132,7 @@ and expr_desc =
| Etrue
| Efalse
| Econst of Number.constant
(* | Esconst of string *)
(** lambda-calculus *)
| Eident of qualid
| Easref of qualid
......
......@@ -388,6 +388,8 @@ let rec dterm ns km crcmap gvars at denv {term_desc = desc; term_loc = loc} =
chain loc (dterm ns km crcmap gvars at denv e1) op1 e23
| Ptree.Tconst (Number.ConstInt _ as c) ->
DTconst (c, dty_int)
| Ptree.Tsconst s ->
DTsconst s
| Ptree.Tconst (Number.ConstReal _ as c) ->
DTconst (c, dty_real)
| Ptree.Tlet (x, e1, e2) ->
......@@ -841,11 +843,11 @@ let rec eff_dterm muc denv {term_desc = desc; term_loc = loc} =
let d1 = eff_dterm muc denv e1 in
DEcast (d1, dity_of_pty muc pty)
| Ptree.Tat _ -> Loc.errorm ~loc "`at' and `old' cannot be used here"
| Ptree.Tidapp _ | Ptree.Tconst _ | Ptree.Tinfix _ | Ptree.Tinnfix _
| Ptree.Ttuple _ | Ptree.Tlet _ | Ptree.Tcase _ | Ptree.Tif _
| Ptree.Ttrue | Ptree.Tfalse | Ptree.Tnot _ | Ptree.Tbinop _ | Ptree.Tbinnop _
| Ptree.Tquant _ | Ptree.Trecord _ | Ptree.Tupdate _ ->
Loc.errorm ~loc "unsupported effect expression")
| Ptree.Tidapp _ | Ptree.Tconst _ | Ptree.Tsconst _ | Ptree.Tinfix _
| Ptree.Tinnfix _ | Ptree.Ttuple _ | Ptree.Tlet _ | Ptree.Tcase _
| Ptree.Tif _ | Ptree.Ttrue | Ptree.Tfalse | Ptree.Tnot _
| Ptree.Tbinop _ | Ptree.Tbinnop _ | Ptree.Tquant _ | Ptree.Trecord _
| Ptree.Tupdate _ -> Loc.errorm ~loc "unsupported effect expression")
let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
let expr_app loc e el =
......
......@@ -173,6 +173,8 @@ let rec print_term info fmt t =
let () = match t.t_node with
| Tconst c ->
Number.print number_format fmt c
| Tsconst _ -> unsupportedTerm t
"alt-ergo: strings not supported"
| Tvar { vs_name = id } ->
print_ident info fmt id
| Tapp (ls, tl) ->
......@@ -308,7 +310,7 @@ and print_fmla_node info fmt f = match f.t_node with
forget_var info v
| Tcase _ -> unsupportedTerm f
"alt-ergo: you must eliminate match"
| Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
| Tvar _ | Tconst _ | Tsconst _ | Teps _ -> raise (FmlaExpected f)
and print_expr info fmt =
TermTF.t_select (print_term info fmt) (print_fmla info fmt)
......
......@@ -282,6 +282,8 @@ let rec print_term ?(boxed=false) ?(opr=true) info ~prec fmt t =
print_vs fmt v
| Tconst c ->
Number.print (number_format info) fmt c
| Tsconst _ -> unsupportedTerm t
"coq: strings not supported"
| Tlet (t1,tb) ->
let v,t2 = t_open_bound tb in
fprintf fmt (protect_on (opr && prec < 200) "let %a :=@ %a in@ %a")
......
......@@ -117,6 +117,8 @@ let number_format = {
let rec print_term info fmt t = match t.t_node with
| Tconst c ->
Number.print number_format fmt c
| Tsconst _ -> unsupportedTerm t
"cvc3: strings not supported"
| Tvar v -> print_var fmt v
| Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
| Some s -> syntax_arguments_typed s (print_term info)
......@@ -193,7 +195,7 @@ and print_fmla info fmt f = match f.t_node with
forget_var v
| Tcase _ -> unsupportedTerm f
"cvc3: you must eliminate match"
| Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
| Tvar _ | Tconst _ | Tsconst _ | Teps _ -> raise (FmlaExpected f)
and print_expr info fmt =
TermTF.t_select (print_term info fmt) (print_fmla info fmt)
......
......@@ -201,6 +201,8 @@ let rec print_term info defs fmt t =
with Not_found ->
match t.t_node with
| Tconst _ -> assert false
| Tsconst _ -> unsupportedTerm t
"gappa: strings not supported"
| Tvar { vs_name = id } ->
print_ident fmt id
| Tapp ( { ls_name = id }, [] ) ->
......@@ -308,7 +310,7 @@ let rec print_fmla info defs fmt f =
"gappa: you must eliminate let in formula"
| Tcase _ -> unsupportedTerm f
"gappa: you must eliminate match"
| Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
| Tvar _ | Tconst _ | Tsconst _ | Teps _ -> raise (FmlaExpected f)
let get_constant defs t =
let rec follow neg_ls t =
......
......@@ -236,6 +236,8 @@ let rec print_term info defs fmt t = match t.t_node with
Number.print number_format fmt c
else raise (UnsupportedTerm (t, "floating-point literal"))
end
| Tsconst _ -> unsupportedTerm t
"isabelle: strings not supported"
| Tif (f, t1, t2) ->
print_app print_const (print_term info defs) fmt ("HOL.If", [f; t1; t2])
| Tlet (t1, tb) ->
......
......@@ -162,6 +162,8 @@ let rec print_term info fmt t =
| Tconst c ->
(*Pretty.print_const fmt c*)
print_const fmt c
| Tsconst _ -> unsupportedTerm t
"yices: strings not supported"
| Tvar { vs_name = id } ->
print_ident fmt id
| Tapp ( { ls_name = id } ,[] ) ->
......@@ -299,7 +301,7 @@ let rec print_term info fmt t =
(*| Tcase (t,bl) ->
print_case print_fmla info fmt t bl*)
| Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
| Tvar _ | Tconst _ | Tsconst _ | Teps _ -> raise (FmlaExpected f)
exception AlreadyDefined
......
......@@ -315,6 +315,8 @@ and print_tnode opl opr info fmt t = match t.t_node with
print_vs fmt v
| Tconst c ->
Number.print number_format fmt c
| Tsconst _ -> unsupportedTerm t
"pcs: strings not supported"
| Tif (f, t1, t2) ->
fprintf fmt "IF %a@ THEN %a@ ELSE %a ENDIF"
(print_fmla info) f (print_term info) t1 (print_opl_term info) t2
......@@ -424,7 +426,7 @@ and print_fnode opl opr info fmt f = match f.t_node with
fprintf fmt "%a(%a)" (print_ls_real info) ps
(print_comma_list (print_term info)) tl
end
| Tvar _ | Tconst _ | Teps _ ->
| Tvar _ | Tconst _ | Tsconst _ | Teps _ ->
raise (FmlaExpected f)
and print_tuple_pat info t fmt p =
......
......@@ -50,6 +50,8 @@ let number_format = {
let rec print_term info fmt t = match t.t_node with
| Tconst c ->
Number.print number_format fmt c
| Tsconst _ -> unsupportedTerm t
"simplify: strings not supported"
| Tvar v ->
print_var fmt v
| Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
......@@ -107,7 +109,7 @@ and print_fmla info fmt f = match f.t_node with
unsupportedTerm f "simplify: you must eliminate let"
| Tcase _ ->
unsupportedTerm f "simplify: you must eliminate match"
| Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
| Tvar _ | Tconst _ | Tsconst _ | Teps _ -> raise (FmlaExpected f)
and print_expr info fmt =
TermTF.t_select (print_term info fmt) (print_fmla info fmt)
......
......@@ -92,6 +92,8 @@ let number_format = {
let rec print_term info fmt t = match t.t_node with
| Tconst c ->
Number.print number_format fmt c
| Tsconst s ->
fprintf fmt "\"%s\"" s
| Tvar v -> print_var fmt v
| Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
| Some s -> syntax_arguments s (print_term info) fmt tl
......@@ -162,7 +164,7 @@ and print_fmla info fmt f = match f.t_node with
forget_var v
| Tcase _ -> unsupportedTerm f
"smtv1: you must eliminate match"
| Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
| Tvar _ | Tconst _ | Tsconst _ | Teps _ -> raise (FmlaExpected f)
(*
and _print_expr info fmt =
......
......@@ -255,6 +255,8 @@ let rec print_term info fmt t =
the literal. Do we ensure that preserved literal types
are exactly those that have a dedicated syntax? *)
end
| Tsconst s ->
fprintf fmt "\"%s\"" s
| Tvar v -> print_var info fmt v
| Tapp (ls, tl) ->
begin match query_syntax info.info_syn ls.ls_name with
......@@ -399,7 +401,7 @@ and print_fmla info fmt f =
(print_branches info subject print_fmla) bl;
forget_var info subject
end
| Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f) in
| Tvar _ | Tconst _ | Tsconst _ | Teps _ -> raise (FmlaExpected f) in