diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast.ml | 1 | ||||
| -rw-r--r-- | src/ast_util.ml | 5 | ||||
| -rw-r--r-- | src/initial_check.ml | 7 | ||||
| -rw-r--r-- | src/lexer.mll | 1 | ||||
| -rw-r--r-- | src/parse_ast.ml | 5 | ||||
| -rw-r--r-- | src/parser.mly | 18 |
6 files changed, 29 insertions, 8 deletions
@@ -227,6 +227,7 @@ typ_aux = (* Type expressions, of kind $_$ *) | Typ_fn of typ * typ * effect (* Function type (first-order only in user code) *) | Typ_tup of (typ) list (* Tuple type *) | Typ_app of id * (typ_arg) list (* type constructor application *) + | Typ_exist of kid list * n_constraint * typ and typ = Typ_aux of typ_aux * l diff --git a/src/ast_util.ml b/src/ast_util.ml index 5bb4e0a6..2d714158 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -212,6 +212,8 @@ and string_of_typ_aux = function | Typ_app (id, args) -> string_of_id id ^ "<" ^ string_of_list ", " string_of_typ_arg args ^ ">" | Typ_fn (typ_arg, typ_ret, eff) -> string_of_typ typ_arg ^ " -> " ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff + | Typ_exist (kids, nc, typ) -> + "exist " ^ string_of_list " " string_of_kid kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ and string_of_typ_arg = function | Typ_arg_aux (typ_arg, l) -> string_of_typ_arg_aux typ_arg and string_of_typ_arg_aux = function @@ -219,8 +221,7 @@ and string_of_typ_arg_aux = function | Typ_arg_typ typ -> string_of_typ typ | Typ_arg_order o -> string_of_order o | Typ_arg_effect eff -> string_of_effect eff - -let rec string_of_n_constraint = function +and string_of_n_constraint = function | NC_aux (NC_fixed (n1, n2), _) -> string_of_nexp n1 ^ " = " ^ string_of_nexp n2 | NC_aux (NC_not_equal (n1, n2), _) -> string_of_nexp n1 ^ " != " ^ string_of_nexp n2 | NC_aux (NC_bounded_ge (n1, n2), _) -> string_of_nexp n1 ^ " >= " ^ string_of_nexp n2 diff --git a/src/initial_check.ml b/src/initial_check.ml index 7be3a940..0e68ad81 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -215,6 +215,11 @@ let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp) else typ_error l "Type constructor given incorrect number of arguments" (Some id) None None | None -> typ_error l "Required a type constructor, encountered an unbound identifier" (Some id) None None | _ -> typ_error l "Required a type constructor, encountered a base kind variable" (Some id) None None) + | Parse_ast.ATyp_exist (kids, nc, atyp) -> + let kids = List.map to_ast_var kids in + let k_env = List.fold_left Envmap.insert k_env (List.map (fun kid -> (var_to_string kid, {k=K_Nat})) kids) in + let exist_typ = to_ast_typ k_env def_ord atyp in + Typ_exist (kids, to_ast_nexp_constraint k_env nc, exist_typ) | _ -> typ_error l "Required an item of kind Type, encountered an illegal form for this kind" None None None ), l) @@ -308,7 +313,7 @@ and to_ast_typ_arg (k_env : kind Envmap.t) (def_ord : order) (kind : kind) (arg | _ -> raise (Reporting_basic.err_unreachable l "To_ast_typ_arg received Lam kind or infer kind")), l) -let rec to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.n_constraint) : n_constraint = +and to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.n_constraint) : n_constraint = match c with | Parse_ast.NC_aux(nc,l) -> NC_aux( (match nc with diff --git a/src/lexer.mll b/src/lexer.mll index 45d8b3c2..228ca38f 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -79,6 +79,7 @@ let kw_table = ("cast", (fun _ -> Cast)); ("false", (fun _ -> False)); ("forall", (fun _ -> Forall)); + ("exist", (fun _ -> Exist)); ("foreach", (fun _ -> Foreach)); ("function", (fun x -> Function_)); ("overload", (fun _ -> Overload)); diff --git a/src/parse_ast.ml b/src/parse_ast.ml index 526dffa8..c2e550f4 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -144,18 +144,19 @@ atyp_aux = (* expressions of all kinds, to be translated to types, nats, orders | ATyp_fn of atyp * atyp * atyp (* Function type (first-order only in user code), last atyp is an effect *) | ATyp_tup of (atyp) list (* Tuple type *) | ATyp_app of id * (atyp) list (* type constructor application *) + | ATyp_exist of kid list * n_constraint * atyp and atyp = ATyp_aux of atyp_aux * l -type +and kinded_id_aux = (* optionally kind-annotated identifier *) KOpt_none of kid (* identifier *) | KOpt_kind of kind * kid (* kind-annotated variable *) -type +and n_constraint_aux = (* constraint over kind $_$ *) NC_fixed of atyp * atyp | NC_bounded_ge of atyp * atyp diff --git a/src/parser.mly b/src/parser.mly index 62a2c9f4..685422e0 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -129,7 +129,7 @@ let make_vector_sugar order_set is_inc typ typ1 = /*Terminals with no content*/ %token And Alias As Assert Bitzero Bitone Bits By Case Clause Const Dec Def Default Deinfix Effect EFFECT End -%token Enumerate Else Exit Extern False Forall Foreach Overload Function_ If_ In IN Inc Let_ Member Nat NatNum Order Cast +%token Enumerate Else Exit Extern False Forall Exist Foreach Overload Function_ If_ In IN Inc Let_ Member Nat NatNum Order Cast %token Pure Rec Register Return Scattered Sizeof Struct Switch Then True TwoStarStar Type TYPE Typedef %token Undefined Union With When Val Constraint %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape @@ -286,6 +286,12 @@ tyvar: | TyVar { (Kid_aux((Var($1)),loc ())) } +tyvars: + | tyvar + { [$1] } + | tyvar tyvars + { $1 :: $2 } + atomic_kind: | TYPE { bkloc BK_type } @@ -446,10 +452,16 @@ tup_typ: | Lparen tup_typ_list Rparen { tloc (ATyp_tup $2) } -typ: +exist_typ: | tup_typ { $1 } - | tup_typ MinusGt tup_typ Effect effect_typ + | Exist tyvars Comma nexp_constraint Dot tup_typ + { tloc (ATyp_exist ($2, $4, $6)) } + +typ: + | exist_typ + { $1 } + | tup_typ MinusGt exist_typ Effect effect_typ { tloc (ATyp_fn($1,$3,$5)) } lit: |