diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_check_new.ml | 4 | ||||
| -rw-r--r-- | src/type_check_new.mli | 81 |
2 files changed, 73 insertions, 12 deletions
diff --git a/src/type_check_new.ml b/src/type_check_new.ml index 6230f289..8a0a0533 100644 --- a/src/type_check_new.ml +++ b/src/type_check_new.ml @@ -45,7 +45,7 @@ open Ast open Util open Big_int -let debug = ref 1 +let debug = ref 0 let depth = ref 0 let rec indent n = match n with @@ -802,7 +802,7 @@ end = struct let add_regtyp id base top ranges env = if Bindings.mem id env.regtyps - then typ_error (id_loc id) ("Register typ " ^ string_of_id id ^ " is already bound") + then typ_error (id_loc id) ("Register type " ^ string_of_id id ^ " is already bound") else begin typ_print ("Adding register type " ^ string_of_id id); diff --git a/src/type_check_new.mli b/src/type_check_new.mli index 2ae7e65b..028732f9 100644 --- a/src/type_check_new.mli +++ b/src/type_check_new.mli @@ -43,40 +43,101 @@ open Ast -type mut = Immutable | Mutable +exception Type_error of l * string;; -type flow_typ +type mut = Immutable | Mutable type lvar = Register of typ | Enum of typ | Local of mut * typ | Unbound module Env : sig + (* Env.t is the type of environments *) type t + + (* Note: Most get_ functions assume the identifiers exist, and throw type + errors if it doesn't. *) + val get_val_spec : id -> t -> typquant * typ - val add_val_spec : id -> typquant * typ -> t -> t - (* val get_local : id -> t -> mut * typ *) - val add_local : id -> mut * typ -> t -> t + val get_register : id -> t -> typ - val add_register : id -> typ -> t -> t + + val get_regtyp : id -> t -> int * int * (index_range * id) list + + (* Returns true if id is a register type, false otherwise *) + val is_regtyp : id -> t -> bool + + (* Check if a local variable is mutable. Throws Type_error if it + isn't a mutable variable. Probably best to use Env.lookup_id + instead *) val is_mutable : id -> t -> bool + + (* Get the current set of constraints. *) val get_constraints : t -> n_constraint list - val add_constraint : n_constraint -> t -> t + val get_typ_var : kid -> t -> base_kind_aux - val add_typ_var : kid -> base_kind_aux -> t -> t + + (* If the environment is checking a function, then this will get the + expected return type of the function. It's useful for checking or + inserting early returns. *) val get_ret_typ : t -> typ option - val add_ret_typ : typ -> t -> t - val add_typ_synonym : id -> (typ_arg list -> typ) -> t -> t + val get_typ_synonym : id -> t -> typ_arg list -> typ + + val get_overloads : id -> t -> id list + + (* Lookup id searchs for a specified id in the environment, and + returns it's type and what kind of identifier it is, using the + lvar type. Returns Unbound if the identifier is unbound, and + won't throw any exceptions. *) val lookup_id : id -> t -> lvar + + (* Return a fresh kind identifier that doesn't exist in the environment *) val fresh_kid : t -> kid + val expand_synonyms : t -> typ -> typ + + (* no_casts removes all the implicit type casts/coercions from the + environment, so checking a term with such an environment will + guarantee not to insert any casts. Not that this is only about + the implicit casting and has nothing to do with the E_cast AST + node. *) val no_casts : t -> t + + (* Is casting allowed by the environment *) + val allow_casts : t -> bool + val empty : t end type tannot = (Env.t * typ) option +(* Strip the type annotations from an expression. *) +val strip_exp : 'a exp -> unit exp + +(* Check an expression has some type. Returns a fully annotated + version of the expression, where each subexpression is annotated + with it's type and the Environment used while checking it. The can + be used to re-start the typechecking process on any + sub-expression. so local modifications to the AST can be + re-checked. *) val check_exp : Env.t -> unit exp -> typ -> tannot exp +(* Fully type-check an AST + +Some invariants that will hold of a fully checked AST are: + + * No internal nodes, such as E_internal_exp, or E_comment nodes. + + * E_vector_access nodes and similar will be replaced by function + calls E_app to vector access functions. This is different to the + old type checker. + + * Every expressions type annotation (tanot) will be Some (typ, env). + + * Also every pattern will be annotated with the type it matches. + + * Toplevel expressions such as typedefs and some subexpressions such + as letbinds may have None as their tannots if it doesn't make sense + for them to have type annotations. *) val check : Env.t -> 'a defs -> tannot defs * Env.t val initial_env : Env.t |