record expressions

.gitignore

@@ -154,6 +154,7 @@ why.conf
 /examples/programs/mergesort_list/
 /examples/programs/binary_search/
 /examples/programs/same_fringe/
+/examples/programs/quicksort/
 
 # modules
 /modules/string/

CHANGES

@@ -12,8 +12,9 @@
     "wait_on_call (prove_task t ()) ()".
   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)"
+      actually syntactic sugar for "type t = `mk t' (a:int) (b:bool)"
       i.e. an algebraic with one constructor and projection functions
+    - a record expression is written {| a = 1; b = True |}
 
 version 0.64, Feb 16, 2011
 ==========================

bench/typing/bad/record1.why

+
+theory T
+  type t = {| mutable a:int |}
+end

bench/typing/bad/record2.why

+theory T
+  logic f int : int
+  goal g1 : let t = {| f = 1 |} in true
+end

bench/typing/bad/record3.why

+theory T
+  type t = {| a:int; b:int; |}
+  type u = {| c:int; d:int; |}
+  goal g1 : let t = {| a = 1;  c = 2 |} in true
+end

bench/typing/bad/record4.why

+theory Records
+  use import bool.Bool
+  type t = {| a:int; b:bool; |}
+  goal g1 : let t = {| a = 1;  b = 2 |} in true
+end

bench/typing/bad/record5.why

+theory T
+  use import list.List
+  use import bool.Bool
+  type t 'a = {| a : list 'a; b : list 'a; |}
+  goal g1 : let t = {| a = Cons 1 Nil; b = Cons True Nil |} in true
+end

bench/typing/bad/record6.why

+theory Records
+  type t = {| a:int |}
+  goal g1 : let t = {| a = 1; a = 2 |} in true
+end

bench/typing/bad/record7.why

+theory Records
+  type t = {| a:int; b:int |}
+  goal g1 : let t = {| a = 1 |} in true
+end

src/parser/denv.ml

@@ -67,7 +67,7 @@ let rec print_dty fmt = function
   | Tyapp (s, [t]) ->
       fprintf fmt "%s %a" s.ts_name.id_string print_dty t
   | Tyapp (s, l) ->
-      fprintf fmt "%s %a" s.ts_name.id_string (print_list comma print_dty) l
+      fprintf fmt "%s %a" s.ts_name.id_string (print_list space print_dty) l
 
 let rec view_dty = function
   | Tyvar { type_val = Some dty } -> view_dty dty

src/parser/parser.pre.mly

@@ -397,12 +397,12 @@ typedefn:
 ;
 
 record_type:
-| LEFTREC list1_record_field RIGHTREC { $2 }
+| LEFTREC list1_record_field opt_semicolon RIGHTREC { $2 }
 ;
 
 list1_record_field:
 | record_field                              { [$1] }
-| record_field SEMICOLON list1_record_field { $1 :: $3 }
+| list1_record_field SEMICOLON record_field { $3 :: $1 }
 ;
 
 record_field:
@@ -568,6 +568,15 @@ lexpr:
    { $1 }
 ;
 
+list1_field_value:
+| field_value                             { [$1] }
+| list1_field_value SEMICOLON field_value { $3 :: $1 }
+;
+
+field_value:
+| lqualid EQUAL lexpr { $1, $3 }
+;
+
 list1_lexpr_arg:
 | lexpr_arg                 { [$1] }
 | lexpr_arg list1_lexpr_arg { $1::$2 }
@@ -595,6 +604,8 @@ lexpr_arg:
    { mk_pp (PPtuple []) }
 | LEFTPAR lexpr COMMA list1_lexpr_sep_comma RIGHTPAR
    { mk_pp (PPtuple ($2 :: $4)) }
+| LEFTREC list1_field_value opt_semicolon RIGHTREC
+   { mk_pp (PPrecord (List.rev $2)) }
 | OPPREF lexpr_arg
    { mk_pp (PPapp (Qident (mk_id (prefix $1) (loc_i 2)), [$2])) }
 | lexpr_arg LEFTSQ lexpr RIGHTSQ

src/parser/ptree.ml

@@ -80,6 +80,7 @@ and pp_desc =
   | PPmatch of lexpr * (pattern * lexpr) list
   | PPcast of lexpr * pty
   | PPtuple of lexpr list
+  | PPrecord of (qualid * lexpr) list
 
 (*s Declarations. *)
 

src/parser/typing.ml

@@ -366,6 +366,54 @@ let apply_highord loc x tl = match List.rev tl with
   | a::tl -> [{pp_loc = loc; pp_desc = PPapp (x, List.rev tl)}; a]
   | [] -> assert false
 
+(* [is_projection uc ls] returns
+   - [Some (ts, lsc, i)] if [ls] is the i-th projection of an
+     algebraic datatype [ts] with only one constructor [lcs]
+   - [None] otherwise 
+ *)
+let is_projection uc ls = 
+  try
+    let ts = match ls.ls_args, ls.ls_value with
+      | [{ty_node = Ty.Tyapp (ts, _)}], Some _ -> ts
+      | _ -> (* not a function with 1 argument *) raise Exit
+    in
+    let kn = get_known uc in
+    let lsc = match Decl.find_constructors kn ts with
+      | [lsc] -> lsc
+      | _ -> (* 0 or several constructors *) raise Exit
+    in
+    let def = match Decl.find_logic_definition kn ls with
+      | Some def -> def
+      | None -> (* no definition *) raise Exit
+    in
+    let v, t = match Decl.open_fs_defn def with
+      | [v], t -> v, t
+      | _ -> assert false
+    in
+    let b = match t.t_node with
+      | Tcase ({t_node=Term.Tvar v'}, [b]) when vs_equal v' v -> b
+      | _ -> raise Exit
+    in
+    let p, t = t_open_branch b in
+    let pl = match p with
+      | { pat_node = Term.Papp (lsc', pl) } when ls_equal lsc lsc' -> pl
+      | _ -> raise Exit
+    in
+    let i = match t.t_node with 
+      | Term.Tvar xi -> 
+	  let rec index i = function 
+	    | [] -> raise Exit
+	    | { pat_node = Term.Pvar v} :: _ when vs_equal v xi -> i
+	    | _ :: l -> index (i+1) l
+	  in
+	  index 0 pl
+      | _ -> 
+	  raise Exit
+    in
+    Some (ts, lsc, i)
+  with Exit ->
+    None
+
 let rec dterm ?(localize=false) env { pp_loc = loc; pp_desc = t } =
   let n, ty = dterm_node ~localize loc env t in
   let t = { dt_node = n; dt_ty = ty } in
@@ -509,6 +557,45 @@ and dterm_node ~localize loc env = function
             id, ty, Fbinop (Fiff, Fapp (ps_pred_app, [h;u]), f)
       in
       Teps (id, ty, Fquant (Fforall, uqu, trl, f)), ty
+  | PPrecord fl ->
+      let type_field (q, e) = 
+	let loc = qloc q in
+	let ls, tyl, ty = specialize_fsymbol q env.uc in
+	match is_projection env.uc ls, tyl with
+	  | None, _ -> 
+	      errorm ~loc "this is not a record field"
+	  | Some (ts, ls, i), [tya] -> 
+	      let loce = e.pp_loc in
+	      let e = dterm ~localize env e in
+	      if not (unify e.dt_ty ty) then 
+		term_expected_type ~loc:loce e.dt_ty ty;
+	      ts, (loc, ls, i, tya), e
+	  | _ -> 
+	      assert false
+      in
+      let fl = List.map type_field fl in
+      let ts,(_,ls,_,ty),_ = match fl with [] -> assert false | x :: _ -> x in
+      let args = Array.create (List.length ls.ls_args) None in
+      let check_field (ts', (loc, _, i, tye), e) = 
+	if not (ts_equal ts' ts) then 
+	  errorm ~loc "this should be a field for type %a" Pretty.print_ts ts;
+	assert (0 <= i && i < Array.length args);
+	if args.(i) <> None then
+	  errorm ~loc "this record field is defined several times";
+	args.(i) <- Some e;
+	if not (unify tye ty) then 
+	  errorm ~loc 
+	    "@[this is a field for type %a,@ \
+               but a field for type %a is expected@]"
+	    print_dty tye print_dty ty
+      in
+      List.iter check_field fl;
+      let add_arg e acc = match e with
+	| None -> errorm ~loc "some record fields are missing"
+	| Some e -> e :: acc
+      in
+      let fl = Array.fold_right add_arg args [] in
+      Tapp (ls, fl), ty
   | PPquant _ | PPbinop _ | PPunop _ | PPfalse | PPtrue ->
       error ~loc TermExpected
 
@@ -593,7 +680,7 @@ and dfmla_node ~localize loc env = function
       let s, tyl = specialize_psymbol x env.uc in
       let tl = dtype_args s.ls_name loc env tyl [] in
       Fapp (s, tl)
-  | PPeps _ | PPconst _ | PPcast _ | PPtuple _ ->
+  | PPeps _ | PPconst _ | PPcast _ | PPtuple _ | PPrecord _ ->
       error ~loc PredicateExpected
 
 and dpat_list env ty p =
@@ -782,7 +869,8 @@ let record_typedef td = match td.td_def with
 	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
+      (* constructor for type t is "mk t" (and not String.capitalize t) *)
+      let id = { td.td_ident with id = "mk " ^ td.td_ident.id } in
       { td with td_def = TDalgebraic [td.td_loc, id, List.map field fl] }
 
 let add_types dl th =

tests/test-jcf.why

@@ -3,14 +3,13 @@
 
 theory Records
 
+  use import list.List
   use import bool.Bool
   use import int.Int
 
-  type t = {| a:int; b:bool |}
+  type t 'a 'b = {| a : 'a; b : list 'b; |}
 
-  logic inv (t:t) = a t = 0 <-> b t = True
-
-  goal g1 : forall t:t. inv t -> a t = 0 -> b t = True
+  goal g1 : let t = {| b = Cons True Nil; a = 1;  |} in a t = 1
 
 end