diff options
| -rw-r--r-- | src/type_check_new.ml | 4 | ||||
| -rw-r--r-- | src/type_check_new.mli | 81 | ||||
| -rwxr-xr-x | test/typecheck/run_tests.sh | 18 |
3 files changed, 78 insertions, 25 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 diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh index a3829970..8926a397 100755 --- a/test/typecheck/run_tests.sh +++ b/test/typecheck/run_tests.sh @@ -21,16 +21,19 @@ fail=0 XML="" function green { + (( pass += 1 )) printf "$1: ${GREEN}$2${NC}\n" XML+=" <testcase name=\"$1\"/>\n" } function yellow { + (( fail += 1 )) printf "$1: ${YELLOW}$2${NC}\n" XML+=" <testcase name=\"$1\">\n <error message=\"$2\">$2</error>\n </testcase>\n" } function red { + (( fail += 1 )) printf "$1: ${RED}$2${NC}\n" XML+=" <testcase name=\"$1\">\n <error message=\"$2\">$2</error>\n </testcase>\n" } @@ -52,15 +55,11 @@ do then if $SAILDIR/sail -dno_cast -just_check $DIR/rtpass/$i 2> /dev/null; then - (( pass += 2)) green "tested $i expecting pass" "pass" else - (( fail += 1 )) - (( pass += 1 )) - yellow "tested $i expecting pass" "pass but failed re-check" + yellow "tested $i expecting pass" "failed re-check" fi else - (( fail += 2 )) red "tested $i expecting pass" "fail" fi done @@ -71,16 +70,12 @@ for i in `ls $DIR/fail/`; do if $SAILDIR/sail -ddump_tc_ast -just_check $DIR/fail/$i 2> /dev/null 1> $DIR/rtfail/$i; then - (( fail += 2 )) red "tested $i expecting fail" "pass" else if $SAILDIR/sail -dno_cast -just_check $DIR/rtfail/$i 2> /dev/null; then - (( fail += 1 )) - (( pass += 1 )) - yellow "tested $i expecting fail" "failed but passed re-check" + yellow "tested $i expecting fail" "passed re-check" else - (( pass += 2 )) green "tested $i expecting fail" "fail" fi fi @@ -98,14 +93,11 @@ function test_lem { mv $SAILDIR/${i%%.*}_embed_sequential.lem $DIR/lem/ if lem -lib $SAILDIR/src/lem_interp -lib $SAILDIR/src/gen_lib/ $DIR/lem/${i%%.*}_embed_types.lem $DIR/lem/${i%%.*}_embed.lem 2> /dev/null then - (( pass += 1 )) green "generated lem for $1/$i" "pass" else - (( fail += 1 )) red "generated lem for $1/$i" "failed to typecheck lem" fi else - (( fail += 1 )) red "generated lem for $1/$i" "failed to generate lem" fi done |