programs: solved conflicts in grammar

drivers/tptp.drv

@@ -37,7 +37,6 @@ theory BuiltIn
   syntax logic (_<>_) "(%1 != %2)"
 end
 
-
 (*
 Local Variables:
 mode: why

src/parser/typing.mli

@@ -80,4 +80,11 @@ val pattern : vsymbol Mstr.t -> dpattern -> vsymbol Mstr.t * pattern
 
 val qloc : Ptree.qualid -> Loc.position
 
+val ts_tuple : int -> Ty.tysymbol
+val fs_tuple : int -> Term.lsymbol
+
+val with_tuples : 
+  ?reset:bool -> (theory_uc -> 'a -> 'b) -> theory_uc -> 'a -> 'b
+
+
 

src/programs/pgm_lexer.mll

@@ -171,7 +171,9 @@ rule token = parse
       { OP0 "ge" }
   | "+" | "-" as c
       { OP2 (String.make 1 c) }
-  | "*" | "/" | "%" as c
+  | "*"
+      { STAR }
+  | "/" | "%" as c
       { OP3 (String.make 1 c) }
   | "@"
       { AT }
@@ -198,8 +200,6 @@ rule token = parse
       { BARBAR }
   | "&&" 
       { AMPAMP }
-  | "=>"
-      { BIGARROW }
   | "\""
       { STRING (string lexbuf) }
   | eof 

src/programs/pgm_parser.mly

@@ -115,7 +115,7 @@
 
 %token UNDERSCORE QUOTE COMMA LEFTPAR RIGHTPAR COLON SEMICOLON
 %token COLONEQUAL ARROW EQUAL AT DOT LEFTSQ RIGHTSQ BANG
-%token LEFTBLEFTB RIGHTBRIGHTB BAR BARBAR AMPAMP BIGARROW 
+%token LEFTBLEFTB RIGHTBRIGHTB BAR BARBAR AMPAMP STAR
 %token EOF
 
 /* Precedences */
@@ -146,7 +146,7 @@
 %left EQUAL OP0
 %left OP1
 %left OP2
-%left OP3
+%left OP3 STAR
 %nonassoc prefix_op
 %right unary_op
 %left prec_app
@@ -225,6 +225,7 @@ any_op:
 | OP0   { $1 }
 | OP2   { $1 }
 | OP3   { $1 }
+| STAR  { "*" }
 ;
 
 qualid:
@@ -255,6 +256,8 @@ expr:
    { mk_infix $1 $2 $3 }
 | expr OP3 expr 
    { mk_infix $1 $2 $3 }
+| expr STAR expr 
+   { mk_infix $1 "*" $3 }
 | NOT expr %prec prefix_op
    { mk_expr (mk_apply_id { id = "notb"; id_loc = loc () } [$2]) }
 | any_op expr %prec prefix_op
@@ -293,7 +296,7 @@ expr:
    { mk_expr (Ewhile ($2, $4, $5)) }
 | ABSURD
    { mk_expr Eabsurd }
-| expr COLON pure_type
+| expr COLON simple_pure_type
    { mk_expr (Ecast ($1, $3)) }
 | RAISE uident
    { mk_expr (Eraise ($2, None)) }
@@ -303,6 +306,8 @@ expr:
    { mk_expr (Etry ($2, $5)) }
 | ANY simple_type_c
    { mk_expr (Eany $2) }
+| LEFTPAR expr COMMA list1_expr_sep_comma RIGHTPAR
+   { mk_expr (Etuple ($2 :: $4)) }
 ;
 
 triple:
@@ -373,6 +378,8 @@ pattern:
 | lident                                        { mk_pat (PPpvar $1) }
 | uqualid                                       { mk_pat (PPpapp ($1, [])) }
 | uqualid LEFTPAR list1_pat_sep_comma RIGHTPAR  { mk_pat (PPpapp ($1, $3)) }
+| LEFTPAR pattern COMMA list1_pat_sep_comma RIGHTPAR          
+                                                { mk_pat (PPptuple ($2 :: $4)) }
 | pattern AS lident                             { mk_pat (PPpas ($1,$3)) }
 | LEFTPAR pattern RIGHTPAR                      { $2 }
 ;
@@ -403,17 +410,29 @@ type_var:
 | QUOTE ident { $2 }
 ;
 
-pure_type:
+simple_pure_type:
 | type_var 
    { PPTtyvar $1 }
 | lqualid
    { PPTtyapp ([], $1) }
-| pure_type lqualid
+| simple_pure_type lqualid
    { PPTtyapp ([$1], $2) }
 | LEFTPAR pure_type COMMA list1_pure_type_sep_comma RIGHTPAR lqualid
    { PPTtyapp ($2 :: $4, $6) }
 ;
 
+pure_type:
+| simple_pure_type 
+    { $1 }
+| simple_pure_type STAR list1_simple_pure_type_sep_star
+    { PPTtuple ($1 :: $3) }
+;
+
+list1_simple_pure_type_sep_star:
+| simple_pure_type                                      { [$1] }
+| simple_pure_type STAR list1_simple_pure_type_sep_star { $1 :: $3 }
+;
+
 list1_pure_type_sep_comma:
 | pure_type                                      { [$1] }
 | pure_type COMMA list1_pure_type_sep_comma { $1 :: $3 }
@@ -453,9 +472,12 @@ type_c:
     { type_c $1 $2 $3 $4 }
 ;
 
+/* for ANY */
 simple_type_c:
-| simple_type_v 
-    { type_c (lexpr_true ()) $1 empty_effect (lexpr_true (), []) }
+| simple_pure_type
+    { type_c (lexpr_true ()) (Tpure $1) empty_effect (lexpr_true (), []) }
+| LEFTPAR type_v RIGHTPAR
+    { type_c (lexpr_true ()) $2 empty_effect (lexpr_true (), []) }
 | pre type_v effects post
     { type_c $1 $2 $3 $4 }
 ;

src/programs/pgm_ptree.ml

@@ -78,6 +78,7 @@ and expr_desc =
   | Efun of binder list * triple
   | Elet of ident * expr * expr
   | Eletrec of (ident * binder list * variant option * triple) list * expr
+  | Etuple of expr list
   (* control *)
   | Esequence of expr * expr
   | Eif of expr * expr * expr

src/programs/pgm_typing.ml

@@ -258,6 +258,25 @@ and dexpr_desc env loc = function
       let env, dl = dletrec env dl in
       let e1 = dexpr env e1 in
       DEletrec (dl, e1), e1.dexpr_type
+  | Pgm_ptree.Etuple el ->
+      let n = List.length el in
+      let s = Typing.fs_tuple n in
+      let tyl = List.map (fun _ -> create_type_var loc) el in
+      let ty = Tyapp (Typing.ts_tuple n, tyl) in
+      let create d ty = 
+	{ dexpr_desc = d; dexpr_denv = env.denv;
+	  dexpr_type = ty; dexpr_loc = loc }
+      in
+      let apply e1 e2 ty2 = 
+	let e2 = dexpr env e2 in
+	assert (Denv.unify e2.dexpr_type ty2);
+	let ty = create_type_var loc in
+	assert (Denv.unify e1.dexpr_type (Tyapp (ts_arrow env.uc, [ty2; ty])));
+	create (DEapply (e1, e2)) ty
+      in
+      let e = create (DEglobal s) (dcurrying env.uc tyl ty) in
+      let e = List.fold_left2 apply e el tyl in
+      e.dexpr_desc, ty
 
   | Pgm_ptree.Esequence (e1, e2) ->
       let e1 = dexpr env e1 in
@@ -614,6 +633,8 @@ let add_decl uc ls =
     in
     errorm ?loc "clash with previous symbol %s" ls.ls_name.id_string
     
+let add_decl = Typing.with_tuples add_decl
+
 let file env uc dl =
   let uc, dl =
     List.fold_left
@@ -669,11 +690,12 @@ End:
 
 (* 
 TODO:
-- tuples
 
 - mutually recursive functions: allow only one order relation specified
 
 - program symbol table outside of the theory
 
+- exhaustivity of pattern-matching
+
 - ghost / effects
 *)

tests/test-pgm-jcf.mlw

@@ -2,8 +2,11 @@
 { 
 use import list.List
 logic c : int
+
 }
 
+let ff () = (1, 2)
+
 let p42 () = { wf_lt_int(4,3) } 1 { true }
 
 exception Not_found