diff options
Diffstat (limited to 'src/initial_check.ml')
| -rw-r--r-- | src/initial_check.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml index f98b11d8..4dd72980 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -251,6 +251,11 @@ let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp) 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) + | Parse_ast.ATyp_with (atyp, nc) -> + let exist_typ = to_ast_typ k_env def_ord atyp in + let kids = KidSet.elements (tyvars_of_typ exist_typ) in + let k_env = List.fold_left Envmap.insert k_env (List.map (fun kid -> (var_to_string kid, {k=K_Nat})) kids) 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) @@ -915,8 +920,8 @@ let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out let kids = List.map to_ast_var kids in let nc = to_ast_nexp_constraint k_env nc in ((Finished (DEF_constraint (id, kids, nc))), envs), partial_defs - | Parse_ast.DEF_pragma (_, _, l) -> - typ_error l "Encountered preprocessor directive in initial check" None None None + | Parse_ast.DEF_pragma (pragma, arg, l) -> + ((Finished(DEF_pragma (pragma, arg, l))), envs), partial_defs | Parse_ast.DEF_internal_mutrec _ -> (* Should never occur because of remove_mutrec *) typ_error Parse_ast.Unknown "Internal mutual block found when processing scattered defs" None None None |