accept type expressions as arguments for metas

src/driver/driver.ml

@@ -150,8 +150,19 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
         let td = remove_prop (find_pr th q) in
         add_meta th td (if c then meta_cl else meta)
     | Rmeta (c,s,al) ->
+        let rec ty_of_pty = function
+          | PTyvar x ->
+              Ty.ty_var (Typing.create_user_tv x)
+          | PTyapp ((loc,_) as q,tyl) ->
+              let ts = find_ts th q in
+              let tyl = List.map ty_of_pty tyl in
+              Loc.try2 loc Ty.ty_app ts tyl
+          | PTuple tyl ->
+              let ts = Ty.ts_tuple (List.length tyl) in
+              Ty.ty_app ts (List.map ty_of_pty tyl)
+        in
         let convert = function
-          | PMAts q  -> MAts (find_ts th q)
+          | PMAty ty -> MAty (ty_of_pty ty)
           | PMAfs q  -> MAls (find_fs th q)
           | PMAps q  -> MAls (find_ps th q)
           | PMApr q  -> MApr (find_pr th q)

src/driver/driver_ast.ml

@@ -15,8 +15,13 @@ type qualid = loc * string list
 
 type cloned = bool
 
+type pty =
+  | PTyvar of string
+  | PTyapp of qualid * pty list
+  | PTuple of pty list
+
 type metarg =
-  | PMAts  of qualid
+  | PMAty  of pty
   | PMAfs  of qualid
   | PMAps  of qualid
   | PMApr  of qualid

src/driver/driver_lexer.mll

@@ -40,6 +40,7 @@
         "time",    TIME;
         "unknown", UNKNOWN;
         "fail", FAIL;
+        "constant", CONSTANT;
         "function", FUNCTION;
         "predicate", PREDICATE;
         "type", TYPE;
@@ -93,6 +94,8 @@ rule token = parse
       { DOT }
   | ","
       { COMMA }
+  | "'"
+      { QUOTE }
   | op_char+ as op
       { OPERATOR op }
   | "\""

src/driver/driver_parser.mly

@@ -27,13 +27,16 @@
 %token <string> OPERATOR
 %token THEORY END SYNTAX REMOVE META PRELUDE PRINTER
 %token VALID INVALID TIMEOUT OUTOFMEMORY UNKNOWN FAIL TIME
-%token UNDERSCORE LEFTPAR RIGHTPAR CLONED DOT EOF
+%token UNDERSCORE LEFTPAR RIGHTPAR CLONED DOT QUOTE EOF
 %token BLACKLIST
 %token MODULE EXCEPTION VAL
 %token FUNCTION PREDICATE TYPE PROP FILENAME TRANSFORM PLUGIN
-%token LEFTPAR_STAR_RIGHTPAR COMMA
+%token LEFTPAR_STAR_RIGHTPAR COMMA CONSTANT
 %token LEFTSQ RIGHTSQ LARROW
 
+%nonassoc SYNTAX REMOVE PRELUDE
+%nonassoc prec_pty
+
 %type <Driver_ast.file> file
 %start file
 %type <Driver_ast.file_extract> file_extract
@@ -88,6 +91,7 @@ list0_trule:
 trule:
 | PRELUDE STRING                          { Rprelude  ($2) }
 | SYNTAX cloned TYPE      qualid STRING   { Rsyntaxts ($2, $4, $5) }
+| SYNTAX cloned CONSTANT  qualid STRING   { Rsyntaxfs ($2, $4, $5) }
 | SYNTAX cloned FUNCTION  qualid STRING   { Rsyntaxfs ($2, $4, $5) }
 | SYNTAX cloned PREDICATE qualid STRING   { Rsyntaxps ($2, $4, $5) }
 | REMOVE cloned PROP qualid               { Rremovepr ($2, $4) }
@@ -101,7 +105,7 @@ meta_args:
 ;
 
 meta_arg:
-| TYPE      qualid { PMAts  $2 }
+| TYPE primitive_type_top { PMAty $2 }
 | FUNCTION  qualid { PMAfs  $2 }
 | PREDICATE qualid { PMAps  $2 }
 | PROP      qualid { PMApr  $2 }
@@ -163,6 +167,49 @@ list1_string_list:
 | list1_string_list STRING { $2 :: $1 }
 ;
 
+/* Types */
+
+primitive_type_top:
+| qualid primitive_type_args_top  { PTyapp ($1, $2) }
+| primitive_type_arg_common       { $1 }
+;
+
+primitive_type_args_top:
+| /* epsilon */ %prec prec_pty                { [] }
+| primitive_type_arg primitive_type_args_top  { $1 :: $2 }
+;
+
+primitive_type:
+| qualid primitive_type_args  { PTyapp ($1, $2) }
+| primitive_type_arg          { $1 }
+;
+
+primitive_type_args:
+| primitive_type_arg                      { [$1] }
+| primitive_type_arg primitive_type_args  { $1 :: $2 }
+;
+
+primitive_type_arg:
+| qualid                    { PTyapp ($1, []) }
+| primitive_type_arg_common { $1 }
+;
+
+primitive_type_arg_common:
+| type_var                          { PTyvar $1 }
+| LEFTPAR primitive_types RIGHTPAR  { PTuple $2 }
+| LEFTPAR RIGHTPAR                  { PTuple [] }
+| LEFTPAR primitive_type RIGHTPAR   { $2 }
+;
+
+primitive_types:
+| primitive_type COMMA primitive_type  { [$1; $3] }
+| primitive_type COMMA primitive_types { $1 :: $3 }
+;
+
+type_var:
+| QUOTE ident { $2 }
+;
+
 /* WhyML */
 
 file_extract:

src/parser/parser.mly

@@ -379,7 +379,8 @@ list1_meta_arg_sep_comma:
 ;
 
 meta_arg:
-| TYPE      qualid { PMAts  $2 }
+| TYPE primitive_type { PMAty $2 }
+| CONSTANT  qualid { PMAfs  $2 }
 | FUNCTION  qualid { PMAfs  $2 }
 | PREDICATE qualid { PMAps  $2 }
 | PROP      qualid { PMApr  $2 }

src/parser/ptree.ml

@@ -148,7 +148,7 @@ type prop_kind =
   | Kaxiom | Klemma | Kgoal
 
 type metarg =
-  | PMAts  of qualid
+  | PMAty  of pty
   | PMAfs  of qualid
   | PMAps  of qualid
   | PMApr  of qualid

src/parser/typing.ml

@@ -1115,7 +1115,7 @@ let add_decl loc th = function
       add_prop (prop_kind k) loc s f th
   | Meta (id, al) ->
       let convert = function
-        | PMAts q  -> MAts (find_tysymbol q th)
+        | PMAty ty -> MAty (ty_of_pty th ty)
         | PMAfs q  -> MAls (find_fsymbol q th)
         | PMAps q  -> MAls (find_psymbol q th)
         | PMApr q  -> MApr (find_prop q th)

src/whyml/mlw_driver.ml

@@ -115,8 +115,19 @@ let load_driver lib file extra_files =
     | Rremovepr (_,q) ->
         ignore (find_pr th q)
     | Rmeta (_,s,al) ->
+        let rec ty_of_pty = function
+          | PTyvar x ->
+              Ty.ty_var (Typing.create_user_tv x)
+          | PTyapp ((loc,_) as q,tyl) ->
+              let ts = find_ts th q in
+              let tyl = List.map ty_of_pty tyl in
+              Loc.try2 loc Ty.ty_app ts tyl
+          | PTuple tyl ->
+              let ts = Ty.ts_tuple (List.length tyl) in
+              Ty.ty_app ts (List.map ty_of_pty tyl)
+        in
         let convert = function
-          | PMAts q  -> MAts (find_ts th q)
+          | PMAty ty -> MAty (ty_of_pty ty)
           | PMAfs q  -> MAls (find_fs th q)
           | PMAps q  -> MAls (find_ps th q)
           | PMApr q  -> MApr (find_pr th q)