constantes

src/core/term.ml

@@ -244,6 +244,14 @@ type binop =
   | Fimplies
   | Fiff
 
+type real_constant = 
+  | RConstDecimal of string * string * string option (* int / frac / exp *)
+  | RConstHexa of string * string * string
+
+type constant =
+  | ConstInt of string
+  | ConstReal of real_constant
+
 type term = {
   t_node : term_node;
   t_label : label list;
@@ -260,7 +268,7 @@ and fmla = {
 and term_node =
   | Tbvar of int
   | Tvar of vsymbol
-  | Tconst of unit
+  | Tconst of constant
   | Tapp of fsymbol * term list
   | Tlet of term * term_bound
   | Tcase of term * term_branch list
@@ -302,6 +310,7 @@ module T = struct
   let t_equal_node t1 t2 = match t1, t2 with
     | Tbvar x1, Tbvar x2 -> x1 == x2
     | Tvar v1, Tvar v2 -> v1 == v2
+    | Tconst c1, Tconst c2 -> c1 = c2
     | Tapp (s1, l1), Tapp (s2, l2) -> s1 == s2 && List.for_all2 (==) l1 l2
     | Tlet (t1, b1), Tlet (t2, b2) -> t1 == t2 && t_eq_bound b1 b2
     | Tcase (t1, l1), Tcase (t2, l2) ->
@@ -328,7 +337,7 @@ module T = struct
   let t_hash_node = function
     | Tbvar n -> n
     | Tvar v -> v.vs_name.id_tag
-    | Tconst () -> 0
+    | Tconst c -> Hashtbl.hash c
     | Tapp (f, tl) -> Hashcons.combine_list t_hash (f.fs_name.id_tag) tl
     | Tlet (t, bt) -> Hashcons.combine t.t_tag (t_hash_bound bt)
     | Tcase (t, bl) -> Hashcons.combine_list t_hash_branch t.t_tag bl
@@ -431,6 +440,7 @@ module Sfmla = Set.Make(F)
 let mk_term n ty = { t_node = n; t_label = []; t_ty = ty; t_tag = -1 }
 let t_bvar n ty = Hterm.hashcons (mk_term (Tbvar n) ty)
 let t_var v = Hterm.hashcons (mk_term (Tvar v) v.vs_ty)
+let t_const c ty = Hterm.hashcons (mk_term (Tconst c) ty)
 let t_app f tl ty = Hterm.hashcons (mk_term (Tapp (f, tl)) ty)
 let t_let v t1 t2 = Hterm.hashcons (mk_term (Tlet (t1, (v, t2))) t2.t_ty)
 let t_case t bl ty = Hterm.hashcons (mk_term (Tcase (t, bl)) ty)

src/core/term.mli

@@ -121,6 +121,14 @@ type binop =
   | Fimplies
   | Fiff
 
+type real_constant = 
+  | RConstDecimal of string * string * string option (* int / frac / exp *)
+  | RConstHexa of string * string * string
+
+type constant =
+  | ConstInt of string
+  | ConstReal of real_constant
+
 type term = private {
   t_node : term_node;
   t_label : label list;
@@ -137,7 +145,7 @@ and fmla = private {
 and term_node = private
   | Tbvar of int
   | Tvar of vsymbol
-  | Tconst of unit
+  | Tconst of constant
   | Tapp of fsymbol * term list
   | Tlet of term * term_bound
   | Tcase of term * term_branch list
@@ -174,6 +182,7 @@ module Sfmla : Set.S with type elt = fmla
 (* smart constructors for term *)
 
 val t_var : vsymbol -> term
+val t_const : constant -> ty -> term
 val t_app : fsymbol -> term list -> ty -> term
 val t_let : vsymbol -> term -> term -> term
 val t_case : term -> (pattern * term) list -> ty -> term

src/core/theory.mli

@@ -124,9 +124,10 @@ val clone_export : theory_uc -> theory -> th_inst -> theory_uc
 
 val get_namespace : theory_uc -> namespace
 
-(* equality *)
+(* builtin *)
 
-val eq : psymbol
+val t_int  : tysymbol
+val t_real : tysymbol
 
 (* exceptions *)
 

src/parser/lexer.mll

@@ -20,6 +20,7 @@
 {
   open Format
   open Lexing
+  open Term
   open Ptree
   open Parser
 

src/parser/parser.mly

@@ -407,9 +407,9 @@ lexpr:
 | EXISTS lident COLON primitive_type DOT lexpr %prec prec_exists
    { mk_pp (PPexists ($2, $4, $6)) }
 | INTEGER
-   { mk_pp (PPconst (ConstInt $1)) }
+   { mk_pp (PPconst (Term.ConstInt $1)) }
 | FLOAT
-   { mk_pp (PPconst (ConstFloat $1)) }
+   { mk_pp (PPconst (Term.ConstReal $1)) }
 | TRUE
    { mk_pp PPtrue }
 | FALSE

src/parser/ptree.mli

@@ -23,13 +23,8 @@ type loc = Loc.position
 
 (*s Logical expressions (for both terms and predicates) *)
 
-type real_constant = 
-  | RConstDecimal of string * string * string option (* int / frac / exp *)
-  | RConstHexa of string * string * string
-
-type constant =
-  | ConstInt of string
-  | ConstFloat of real_constant
+type real_constant = Term.real_constant
+type constant = Term.constant
 
 type pp_infix = 
   | PPand | PPor | PPimplies | PPiff 

src/parser/typing.ml

@@ -326,6 +326,7 @@ type dterm = { dt_node : dterm_node; dt_ty : dty }
 
 and dterm_node =
   | Tvar of string
+  | Tconst of constant
   | Tapp of fsymbol * dterm list
   | Tlet of dterm * string * dterm
 (*   | Tcase of dterm * tbranch list *)
@@ -369,6 +370,10 @@ and dterm_node loc env = function
       let s, tyl, ty = specialize_fsymbol s in
       let tl = dtype_args s.fs_name loc env tyl tl in
       Tapp (s, tl), ty
+  | PPconst (ConstInt _ as c) ->
+      Tconst c, Tyapp (Theory.t_int, [])
+  | PPconst (ConstReal _ as c) ->
+      Tconst c, Tyapp (Theory.t_real, [])
   | _ ->
       assert false (*TODO*)
 
@@ -425,6 +430,8 @@ let rec term env t = match t.dt_node with
   | Tvar x ->
       assert (M.mem x env);
       t_var (M.find x env)
+  | Tconst c ->
+      t_const c (ty t.dt_ty)
   | Tapp (s, tl) ->
       t_app s (List.map (term env) tl) (ty t.dt_ty)
   | _ ->

src/test.why

@@ -12,7 +12,8 @@ theory A
   type t
   logic p(t)
   logic q(x: t) = p(x)
-  logic c : real
+  logic c : int = 42
+  logic c' : real = 42.5
 end
 
 theory B