record types in the logic (only type declaration so far, as syntactic sugar for an algebraic)

CHANGES

 
+  o record types in the logic
+    - introduced with syntax "type t = {| a:int; b:bool |}"
+    - actually syntactic sugar for "type t = T (a:int) (b:bool)"
+      i.e. an algebraic with one constructor and projection functions
+
 version 0.64, Feb 16, 2011
 ==========================
 

src/parser/lexer.mll

@@ -213,6 +213,10 @@ rule token = parse
       { LEFTBRC }
   | "}"
       { RIGHTBRC }
+  | "{|"
+      { LEFTREC }
+  | "|}"
+      { RIGHTREC }
   | ":"
       { COLON }
   | ";"

src/parser/parser.pre.mly

@@ -177,10 +177,10 @@
 %token BACKQUOTE BAR
 %token COLON COMMA
 %token DOT EQUAL FUNC LAMBDA LTGT
-%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
+%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTREC LEFTSQ
 %token LRARROW
 %token PRED QUOTE
-%token RIGHTPAR RIGHTSQ
+%token RIGHTPAR RIGHTREC RIGHTSQ
 %token UNDERSCORE
 
 %token EOF
@@ -393,6 +393,21 @@ typedefn:
 | EQUAL primitive_type    { TDalias $2 }
 | EQUAL typecases         { TDalgebraic $2 }
 | EQUAL BAR typecases     { TDalgebraic $3 }
+| EQUAL record_type       { TDrecord $2 }
+;
+
+record_type:
+| LEFTREC list1_record_field RIGHTREC { $2 }
+;
+
+list1_record_field:
+| record_field                              { [$1] }
+| record_field SEMICOLON list1_record_field { $1 :: $3 }
+;
+
+record_field:
+| opt_mutable lident COLON primitive_type 
+   { loc (), $1, $2, $4 }
 ;
 
 typecases:

src/parser/ptree.ml

@@ -103,10 +103,13 @@ type clone_subst =
   | CSlemma of qualid
   | CSgoal  of qualid
 
+type is_mutable = bool
+
 type type_def =
   | TDabstract
   | TDalias     of pty
   | TDalgebraic of (loc * ident * param list) list
+  | TDrecord    of (loc * is_mutable * ident * pty) list
 
 type type_decl = {
   td_loc    : loc;
@@ -221,8 +224,6 @@ and expr_desc =
 
 and triple = pre * expr * post
 
-type is_mutable = bool
-
 type program_decl =
   | Dlet    of ident * expr
   | Dletrec of (ident * binder list * variant option * triple) list

src/parser/typing.ml

@@ -645,6 +645,7 @@ let add_projection cl p (fs,tyarg,tyval) th =
 
 let add_projections th d = match d.td_def with
   | TDabstract | TDalias _ -> th
+  | TDrecord _ -> assert false
   | TDalgebraic cl ->
       let per_cs acc (_,id,pl) =
         let cs = find_lsymbol (Qident id) th in
@@ -726,6 +727,8 @@ let add_types dl th =
 	    create_tysymbol id vl (Some (apply ty))
 	| TDabstract | TDalgebraic _ ->
 	    create_tysymbol id vl None
+	| TDrecord _ ->
+	    assert false
       in
       Hashtbl.add tysymbols x (Some ts);
       ts
@@ -761,6 +764,8 @@ let add_types dl th =
 	    create_fsymbol (id_user ~labels id loc) tyl ty
 	  in
 	  Talgebraic (List.map constructor cl)
+      | TDrecord _ ->
+	  assert false
     in
     ts, d
   in
@@ -769,6 +774,20 @@ let add_types dl th =
   in
   List.fold_left add_projections th dl
 
+let record_typedef td = match td.td_def with
+  | TDabstract | TDalgebraic _ | TDalias _ ->
+      td
+  | TDrecord fl ->
+      let field (loc, mut, id, ty) = 
+	if mut then errorm ~loc "a logic record field cannot be mutable";
+	Some id, ty 
+      in
+      let id = { td.td_ident with id = String.capitalize td.td_ident.id } in
+      { td with td_def = TDalgebraic [td.td_loc, id, List.map field fl] }
+
+let add_types dl th =
+  add_types (List.map record_typedef dl) th
+
 let env_of_vsymbol_list vl =
   List.fold_left (fun env v -> Mstr.add v.vs_name.id_string v env) Mstr.empty vl
 

tests/test-jcf.why

 
 
-theory List
 
-  type list 'a = Nil | Cons 'a (list 'a)
+theory Records
 
-end
-
-theory Length
-  use import int.Int
-  use import List
-
-  logic length (l : list 'a) : int = 
-    match l with
-    | Nil      -> 0
-    | Cons _ r -> 1 + length r
-    end
-
-  lemma Length_nonnegative : forall l:list 'a. length(l) >= 0
-
-end
-
-theory Sorted
-
-  use import List
+  use import bool.Bool
   use import int.Int
- 
-  inductive sorted (list int) =
-    | Sorted_Nil : 
-        sorted Nil
-    | Sorted_One : 
-        forall x:int. sorted (Cons x Nil)
-    | Sorted_Two : 
-        forall x y : int, l : list int. 
-        x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l))
- 
-end
 
-theory Order
+  type t = {| a:int; b:bool |}
 
-  type t
-  logic (<=) t t
+  logic inv (t:t) = a t = 0 <-> b t = True
 
-  axiom Le_refl : forall x : t. x <= x
-  axiom Le_asym : forall x y : t. x <= y -> y <= x -> x = y
-  axiom Le_trans: forall x y z : t. x <= y -> y <= z -> x <= z
-
-end
-
-theory SortedGen
-
-  use import List
-
-  clone import Order as O
- 
-  inductive sorted (l : list t) =
-    | Sorted_Nil : 
-        sorted Nil
-    | Sorted_One : 
-        forall x:t. sorted (Cons x Nil)
-    | Sorted_Two : 
-        forall x y : t, l : list t. 
-        x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l))
- 
-end
-
-theory SortedIntList
-
-  use import int.Int
-  clone SortedGen with type O.t = int, logic O.(<=) = (<=)
+  goal g1 : forall t:t. inv t -> a t = 0 -> b t = True
 
 end