diff options
Diffstat (limited to 'src/initial_check.ml')
| -rw-r--r-- | src/initial_check.ml | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml index 4d6db996..1db9d80b 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -73,7 +73,7 @@ let rec kind_to_string kind = match kind.k with | K_Lam (kinds,kind) -> "Lam [" ^ string_of_list ", " kind_to_string kinds ^ "] -> " ^ (kind_to_string kind) (*Envs is a tuple of used names (currently unused), map from id to kind, default order for vector types and literal vectors *) -type envs = Nameset.t * kind Envmap.t * order +type envs = Nameset.t * kind Envmap.t * order type 'a envs_out = 'a * envs let id_to_string (Id_aux(id,l)) = @@ -207,6 +207,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) @@ -231,7 +236,7 @@ and to_ast_nexp (k_env : kind Envmap.t) (n: Parse_ast.atyp) : Ast.nexp = let n1 = to_ast_nexp k_env t1 in let n2 = to_ast_nexp k_env t2 in Nexp_aux (Nexp_minus (n1, n2), l) - | _ -> typ_error l "Requred an item of kind Nat, encountered an illegal form for this kind" None None None) + | _ -> typ_error l "Required an item of kind Nat, encountered an illegal form for this kind" None None None) and to_ast_order (k_env : kind Envmap.t) (def_ord : order) (o: Parse_ast.atyp) : Ast.order = match o with @@ -297,10 +302,10 @@ and to_ast_typ_arg (k_env : kind Envmap.t) (def_ord : order) (kind : kind) (arg | K_Nat -> Typ_arg_nexp (to_ast_nexp k_env arg) | K_Ord -> Typ_arg_order (to_ast_order k_env def_ord arg) | K_Efct -> Typ_arg_effect (to_ast_effects k_env arg) - | _ -> raise (Reporting_basic.err_unreachable l "To_ast_typ_arg received Lam kind or infer kind")), + | _ -> raise (Reporting_basic.err_unreachable l ("To_ast_typ_arg received Lam kind or infer kind: " ^ kind_to_string 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 @@ -326,6 +331,8 @@ let rec to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.n_constrai NC_or (to_ast_nexp_constraint k_env nc1, to_ast_nexp_constraint k_env nc2) | Parse_ast.NC_and (nc1, nc2) -> NC_and (to_ast_nexp_constraint k_env nc1, to_ast_nexp_constraint k_env nc2) + | Parse_ast.NC_true -> NC_true + | Parse_ast.NC_false -> NC_false ), l) (* Transforms a typquant while building first the kind environment of declared variables, and also the kind environment in context *) |