From 4242dd9331f47c8bacc219e66321d27bd5af7164 Mon Sep 17 00:00:00 2001
From: Andrei Paskevich <andrei@lri.fr>
Date: Mon, 24 Dec 2012 19:47:38 +0100
Subject: [PATCH] accept type expressions as arguments for metas

---
 src/driver/driver.ml         | 13 ++++++++-
 src/driver/driver_ast.ml     |  7 ++++-
 src/driver/driver_lexer.mll  |  3 ++
 src/driver/driver_parser.mly | 53 ++++++++++++++++++++++++++++++++++--
 src/parser/parser.mly        |  3 +-
 src/parser/ptree.ml          |  2 +-
 src/parser/typing.ml         |  2 +-
 src/whyml/mlw_driver.ml      | 13 ++++++++-
 8 files changed, 87 insertions(+), 9 deletions(-)

diff --git a/src/driver/driver.ml b/src/driver/driver.ml
index 09f7ebc010..6f9af45321 100644
--- a/src/driver/driver.ml
+++ b/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)
diff --git a/src/driver/driver_ast.ml b/src/driver/driver_ast.ml
index e89054f758..9836e64bae 100644
--- a/src/driver/driver_ast.ml
+++ b/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
diff --git a/src/driver/driver_lexer.mll b/src/driver/driver_lexer.mll
index 5c545eb2b5..1bdde1edc3 100644
--- a/src/driver/driver_lexer.mll
+++ b/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 }
   | "\""
diff --git a/src/driver/driver_parser.mly b/src/driver/driver_parser.mly
index b5dbace47b..2ebcc50be4 100644
--- a/src/driver/driver_parser.mly
+++ b/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:
diff --git a/src/parser/parser.mly b/src/parser/parser.mly
index ca1b79da9a..e96c8d484c 100644
--- a/src/parser/parser.mly
+++ b/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 }
diff --git a/src/parser/ptree.ml b/src/parser/ptree.ml
index c0e9986ddc..be75951dae 100644
--- a/src/parser/ptree.ml
+++ b/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
diff --git a/src/parser/typing.ml b/src/parser/typing.ml
index 65464ebd2c..9dc1b0c5ab 100644
--- a/src/parser/typing.ml
+++ b/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)
diff --git a/src/whyml/mlw_driver.ml b/src/whyml/mlw_driver.ml
index c881d3b0f9..f35b704424 100644
--- a/src/whyml/mlw_driver.ml
+++ b/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)
-- 
GitLab