diff --git a/src/driver/driver.ml b/src/driver/driver.ml index 09f7ebc01042e638aed125ccf9d228da9c2bd6f2..6f9af45321485a26a032b50b863f333385eb410b 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 e89054f758dee879aa8ba9faa491a06d2d70e6fe..9836e64baefeb543af46733011fae2e783c4c9dc 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 5c545eb2b584cb751f5a97c64cb1f4e0b831b368..1bdde1edc3f1f3911b0de25acb938415c08541a1 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 b5dbace47b109a15bffedda44e29a74133c1ae61..2ebcc50be4be6c2fb4abbda01324aefb360729e4 100644 --- a/src/driver/driver_parser.mly +++ b/src/driver/driver_parser.mly @@ -27,13 +27,16 @@ %token 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 file %start file %type 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 ca1b79da9a8d9088e7c366337e475e1e897cd50a..e96c8d484c7284f5861dfd9ad9f292e7a5ab4dc7 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 c0e9986ddc43d1af9e037fbf2fb3911f72794327..be75951dae111dafd60e27bcd82f341676d28844 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 65464ebd2cb5c2cc0ebbb5cdba2407599a479956..9dc1b0c5abc9a02f33b84d9c6a64baaed5b877d5 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 c881d3b0f99cbbacea5e233718745f0bd05dc41d..f35b7044245b5fbce53b1b29bb4b94ab57eb2657 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)