diff options
| -rw-r--r-- | language/l2.ott | 17 | ||||
| -rw-r--r-- | src/ast_util.ml | 1 | ||||
| -rw-r--r-- | src/constraint.ml | 40 | ||||
| -rw-r--r-- | src/constraint.mli | 1 | ||||
| -rw-r--r-- | src/initial_check.ml | 3 | ||||
| -rw-r--r-- | src/type_check.ml | 185 | ||||
| -rw-r--r-- | test/typecheck/pass/ex_cast.sail | 2 | ||||
| -rw-r--r-- | test/typecheck/pass/exint.sail | 4 | ||||
| -rw-r--r-- | test/typecheck/pass/lexp_memory.sail | 2 | ||||
| -rw-r--r-- | test/typecheck/pass/mips_CP0Cause_BD_assign1.sail | 2 | ||||
| -rw-r--r-- | test/typecheck/pass/mips_CP0Cause_BD_assign2.sail | 2 |
11 files changed, 149 insertions, 110 deletions
diff --git a/language/l2.ott b/language/l2.ott index d27648e9..d010bc67 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -198,14 +198,15 @@ kind :: 'K_' ::= nexp :: 'Nexp_' ::= {{ com numeric expression, of kind $[[Nat]]$ }} {{ aux _ l }} - | id :: :: id {{ com abbreviation identifier }} - | kid :: :: var {{ com variable }} - | num :: :: constant {{ com constant }} - | nexp1 * nexp2 :: :: times {{ com product }} - | nexp1 + nexp2 :: :: sum {{ com sum }} - | nexp1 - nexp2 :: :: minus {{ com subtraction }} - | 2** nexp :: :: exp {{ com exponential }} - | neg nexp :: I :: neg {{ com for internal use only}} + | id :: :: id {{ com abbreviation identifier }} + | kid :: :: var {{ com variable }} + | num :: :: constant {{ com constant }} + | id ( nexp1 , ... , nexpn ) :: :: app {{ com app }} + | nexp1 * nexp2 :: :: times {{ com product }} + | nexp1 + nexp2 :: :: sum {{ com sum }} + | nexp1 - nexp2 :: :: minus {{ com subtraction }} + | 2** nexp :: :: exp {{ com exponential }} + | neg nexp :: I :: neg {{ com for internal use only}} | ( nexp ) :: S :: paren {{ ichlo [[nexp]] }} order :: 'Ord_' ::= diff --git a/src/ast_util.ml b/src/ast_util.ml index 5393bb81..aa3efc40 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -458,6 +458,7 @@ and string_of_nexp_aux = function | Nexp_times (n1, n2) -> "(" ^ string_of_nexp n1 ^ " * " ^ string_of_nexp n2 ^ ")" | Nexp_sum (n1, n2) -> "(" ^ string_of_nexp n1 ^ " + " ^ string_of_nexp n2 ^ ")" | Nexp_minus (n1, n2) -> "(" ^ string_of_nexp n1 ^ " - " ^ string_of_nexp n2 ^ ")" + | Nexp_app (id, nexps) -> string_of_id id ^ "(" ^ string_of_list ", " string_of_nexp nexps ^ ")" | Nexp_exp n -> "2 ^ " ^ string_of_nexp n | Nexp_neg n -> "- " ^ string_of_nexp n diff --git a/src/constraint.ml b/src/constraint.ml index 5dcc10f0..37073ff2 100644 --- a/src/constraint.ml +++ b/src/constraint.ml @@ -3,27 +3,33 @@ open Util (* ===== Integer Constraints ===== *) -type nexp_op = Plus | Minus | Mult +type nexp_op = string type nexp = - | NFun of (nexp_op * nexp * nexp) + | NFun of (nexp_op * nexp list) | N2n of nexp | NConstant of big_int | NVar of int -let big_int_op : nexp_op -> big_int -> big_int -> big_int = function - | Plus -> add_big_int - | Minus -> sub_big_int - | Mult -> mult_big_int +let big_int_op : nexp_op -> (big_int -> big_int -> big_int) option = function + | "+" -> Some add_big_int + | "-" -> Some sub_big_int + | "*" -> Some mult_big_int + | _ -> None let rec arith constr = let constr' = match constr with - | NFun (op, x, y) -> NFun (op, arith x, arith y) + | NFun (op, [x; y]) -> NFun (op, [arith x; arith y]) | N2n c -> N2n (arith c) | c -> c in match constr' with - | NFun (op, NConstant x, NConstant y) -> NConstant (big_int_op op x y) + | NFun (op, [NConstant x; NConstant y]) as c -> + begin + match big_int_op op with + | Some op -> NConstant (op x y) + | None -> c + end | N2n (NConstant x) -> NConstant (power_int_positive_big_int 2 x) | c -> c @@ -63,7 +69,7 @@ module IntSet = Set.Make( let rec nexp_vars : nexp -> IntSet.t = function | NConstant _ -> IntSet.empty | NVar v -> IntSet.singleton v - | NFun (_, x, y) -> IntSet.union (nexp_vars x) (nexp_vars y) + | NFun (_, xs) -> List.fold_left IntSet.union IntSet.empty (List.map nexp_vars xs) | N2n x -> nexp_vars x let rec constraint_vars : nexp constraint_bool -> IntSet.t = function @@ -98,14 +104,8 @@ let cop_sexpr op x y = | Eq -> sfun "=" [x; y] | NEq -> sfun "not" [sfun "=" [x; y]] -let iop_sexpr op x y = - match op with - | Plus -> sfun "+" [x; y] - | Minus -> sfun "-" [x; y] - | Mult -> sfun "*" [x; y] - let rec sexpr_of_nexp = function - | NFun (op, x, y) -> iop_sexpr op (sexpr_of_nexp x) (sexpr_of_nexp y) + | NFun (op, xs) -> sfun op (List.map sexpr_of_nexp xs) | N2n x -> sfun "^" [Atom "2"; sexpr_of_nexp x] | NConstant c -> Atom (string_of_big_int c) (* CHECK: do we do negative constants right? *) | NVar var -> Atom ("v" ^ string_of_int var) @@ -245,11 +245,13 @@ let neq x y : t = CFun (NEq, x, y) let pow2 x : nexp = N2n x -let add x y : nexp = NFun (Plus, x, y) +let add x y : nexp = NFun ("+", [x; y]) + +let sub x y : nexp = NFun ("-", [x; y]) -let sub x y : nexp = NFun (Minus, x, y) +let mult x y : nexp = NFun ("*", [x; y]) -let mult x y : nexp = NFun (Mult, x, y) +let app f xs : nexp = NFun (f, xs) let constant (x : big_int) : nexp = NConstant x diff --git a/src/constraint.mli b/src/constraint.mli index 4f69d51f..33881fcf 100644 --- a/src/constraint.mli +++ b/src/constraint.mli @@ -28,6 +28,7 @@ val pow2 : nexp -> nexp val add : nexp -> nexp -> nexp val sub : nexp -> nexp -> nexp val mult : nexp -> nexp -> nexp +val app : string -> nexp list -> nexp val constant : Big_int.big_int -> nexp val variable : int -> nexp diff --git a/src/initial_check.ml b/src/initial_check.ml index df715e17..e80ff9a4 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -238,6 +238,9 @@ 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) + | Parse_ast.ATyp_app (id, ts) -> + let nexps = List.map (to_ast_nexp k_env) ts in + Nexp_aux (Nexp_app (to_ast_id id, nexps), l) | _ -> 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 = diff --git a/src/type_check.ml b/src/type_check.ml index 8a56d9b2..f71e52c1 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -225,6 +225,7 @@ and nexp_subst_aux sv subst = function | Nexp_times (nexp1, nexp2) -> Nexp_times (nexp_subst sv subst nexp1, nexp_subst sv subst nexp2) | Nexp_sum (nexp1, nexp2) -> Nexp_sum (nexp_subst sv subst nexp1, nexp_subst sv subst nexp2) | Nexp_minus (nexp1, nexp2) -> Nexp_minus (nexp_subst sv subst nexp1, nexp_subst sv subst nexp2) + | Nexp_app (id, nexps) -> Nexp_app (id, List.map (nexp_subst sv subst) nexps) | Nexp_exp nexp -> Nexp_exp (nexp_subst sv subst nexp) | Nexp_neg nexp -> Nexp_neg (nexp_subst sv subst nexp) @@ -238,6 +239,7 @@ and nc_subst_nexp_aux l sv subst = function | NC_equal (n1, n2) -> NC_equal (nexp_subst sv subst n1, nexp_subst sv subst n2) | NC_bounded_ge (n1, n2) -> NC_bounded_ge (nexp_subst sv subst n1, nexp_subst sv subst n2) | NC_bounded_le (n1, n2) -> NC_bounded_le (nexp_subst sv subst n1, nexp_subst sv subst n2) + | NC_not_equal (n1, n2) -> NC_not_equal (nexp_subst sv subst n1, nexp_subst sv subst n2) | NC_set (kid, ints) as set_nc -> if Kid.compare kid sv = 0 then nexp_set_to_or l (mk_nexp subst) ints @@ -393,6 +395,11 @@ module Env : sig val fresh_kid : ?kid:kid -> t -> kid val expand_synonyms : t -> typ -> typ val base_typ_of : t -> typ -> typ + val add_smt_op : id -> string -> t -> t + val get_smt_op : id -> t -> string + (* Well formedness-checks *) + val wf_typ : ?exs:KidSet.t -> t -> typ -> unit + val wf_constraint : ?exs:KidSet.t -> t -> n_constraint -> unit val empty : t end = struct type t = @@ -411,6 +418,7 @@ end = struct records : (typquant * (typ * id) list) Bindings.t; accessors : (typquant * typ) Bindings.t; externs : (string -> string option) Bindings.t; + smt_ops : string Bindings.t; casts : id list; allow_casts : bool; constraints : n_constraint list; @@ -435,6 +443,7 @@ end = struct records = Bindings.empty; accessors = Bindings.empty; externs = Bindings.empty; + smt_ops = Bindings.empty; casts = []; allow_casts = true; constraints = []; @@ -443,56 +452,16 @@ end = struct poly_undefineds = false; } - let counter = ref 0 - - let fresh_kid ?kid:(kid=mk_kid "") env = - let suffix = if Kid.compare kid (mk_kid "") = 0 then "#" else "#" ^ string_of_id (id_of_kid kid) in - let fresh = Kid_aux (Var ("'fv" ^ string_of_int !counter ^ suffix), Parse_ast.Unknown) in - incr counter; fresh - - let freshen_kid env kid (typq, typ) = - let fresh = fresh_kid ~kid:kid env in - (typquant_subst_kid kid fresh typq, typ_subst_kid kid fresh typ) - - let freshen_bind env bind = - List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars) - - let get_val_spec id env = - try - let bind = Bindings.find id env.top_val_specs in - typ_debug ("get_val_spec: Env has " ^ string_of_list ", " (fun (kid, bk) -> string_of_kid kid ^ " => " ^ string_of_base_kind_aux bk) (KBindings.bindings env.typ_vars)); - let bind' = List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars) in - typ_debug ("get_val_spec: freshened to " ^ string_of_bind bind'); - bind' - with - | Not_found -> typ_error (id_loc id) ("No val spec found for " ^ string_of_id id) - - let update_val_spec id bind env = - begin - typ_print ("Adding val spec binding " ^ string_of_id id ^ " :: " ^ string_of_bind bind); - { env with top_val_specs = Bindings.add id bind env.top_val_specs } - end - - let add_val_spec id bind env = - if Bindings.mem id env.top_val_specs - then typ_error (id_loc id) ("Identifier " ^ string_of_id id ^ " is already bound") - else update_val_spec id bind env - - let is_union_constructor id env = - let is_ctor id (Tu_aux (tu, _)) = match tu with - | Tu_id ctor_id when Id.compare id ctor_id = 0 -> true - | Tu_ty_id (_, ctor_id) when Id.compare id ctor_id = 0 -> true - | _ -> false - in - let type_unions = List.concat (List.map (fun (_, (_, tus)) -> tus) (Bindings.bindings env.variants)) in - List.exists (is_ctor id) type_unions - let get_typ_var kid env = try KBindings.find kid env.typ_vars with | Not_found -> typ_error (kid_loc kid) ("No kind identifier " ^ string_of_kid kid) let get_typ_vars env = env.typ_vars + let builtin_typs = + IdSet.of_list (List.map mk_id + [ "range"; "atom"; "vector"; "register"; "bit"; "unit"; "int"; "nat"; "bool"; "real"; "list"; "string"; "itself"]) + (* FIXME: Add an IdSet for builtin types *) let bound_typ_id env id = Bindings.mem id env.typ_synonyms @@ -500,18 +469,27 @@ end = struct || Bindings.mem id env.records || Bindings.mem id env.regtyps || Bindings.mem id env.enums - || Id.compare id (mk_id "range") = 0 - || Id.compare id (mk_id "vector") = 0 - || Id.compare id (mk_id "register") = 0 - || Id.compare id (mk_id "bit") = 0 - || Id.compare id (mk_id "unit") = 0 - || Id.compare id (mk_id "int") = 0 - || Id.compare id (mk_id "nat") = 0 - || Id.compare id (mk_id "bool") = 0 - || Id.compare id (mk_id "real") = 0 - || Id.compare id (mk_id "list") = 0 - || Id.compare id (mk_id "string") = 0 - || Id.compare id (mk_id "itself") = 0 + || IdSet.mem id builtin_typs + + let get_overloads id env = + try Bindings.find id env.overloads with + | Not_found -> [] + + let add_overloads id ids env = + typ_print ("Adding overloads for " ^ string_of_id id ^ " [" ^ string_of_list ", " string_of_id ids ^ "]"); + { env with overloads = Bindings.add id ids env.overloads } + + let add_smt_op id str env = + typ_print ("Adding smt binding " ^ string_of_id id ^ " to " ^ str); + { env with smt_ops = Bindings.add id str env.smt_ops } + + let get_smt_op (Id_aux (_, l) as id) env = + let rec first_smt_op = function + | id :: ids -> (try Bindings.find id env.smt_ops with Not_found -> first_smt_op ids) + | [] -> typ_error l ("No SMT op for " ^ string_of_id id) + in + try Bindings.find id env.smt_ops with + | Not_found -> first_smt_op (get_overloads id env) (* Check if a type, order, or n-expression is well-formed. Throws a type error if the type is badly formed. FIXME: Add arity to type @@ -529,7 +507,8 @@ end = struct | Typ_app (id, args) when bound_typ_id env id -> List.iter (wf_typ_arg ~exs:exs env) args | Typ_app (id, _) -> typ_error l ("Undefined type " ^ string_of_id id) | Typ_exist ([], _, _) -> typ_error l ("Existential must have some type variables") - | Typ_exist (kids, nc, typ) when KidSet.is_empty exs -> wf_typ ~exs:(KidSet.of_list kids) env typ + | Typ_exist (kids, nc, typ) when KidSet.is_empty exs -> + wf_constraint ~exs:(KidSet.of_list kids) env nc; wf_typ ~exs:(KidSet.of_list kids) env typ | Typ_exist (_, _, _) -> typ_error l ("Nested existentials are not allowed") and wf_typ_arg ?exs:(exs=KidSet.empty) env (Typ_arg_aux (typ_arg_aux, _)) = match typ_arg_aux with @@ -549,6 +528,9 @@ end = struct ^ string_of_base_kind_aux kind ^ " but should have kind Nat") end | Nexp_constant _ -> () + | Nexp_app (id, nexps) -> + let _ = get_smt_op id env in + List.iter (fun n -> wf_nexp ~exs:exs env n) nexps | Nexp_times (nexp1, nexp2) -> wf_nexp ~exs:exs env nexp1; wf_nexp ~exs:exs env nexp2 | Nexp_sum (nexp1, nexp2) -> wf_nexp ~exs:exs env nexp1; wf_nexp ~exs:exs env nexp2 | Nexp_minus (nexp1, nexp2) -> wf_nexp ~exs:exs env nexp1; wf_nexp ~exs:exs env nexp2 @@ -565,6 +547,60 @@ end = struct ^ string_of_base_kind_aux kind ^ " but should have kind Order") end | Ord_inc | Ord_dec -> () + and wf_constraint ?exs:(exs=KidSet.empty) env (NC_aux (nc, _)) = + match nc with + | NC_equal (n1, n2) -> wf_nexp ~exs:exs env n1; wf_nexp ~exs:exs env n2 + | NC_not_equal (n1, n2) -> wf_nexp ~exs:exs env n1; wf_nexp ~exs:exs env n2 + | NC_bounded_ge (n1, n2) -> wf_nexp ~exs:exs env n1; wf_nexp ~exs:exs env n2 + | NC_bounded_le (n1, n2) -> wf_nexp ~exs:exs env n1; wf_nexp ~exs:exs env n2 + | NC_set (kid, ints) -> () (* MAYBE: We could demand that ints are all unique here *) + | NC_or (nc1, nc2) -> wf_constraint ~exs:exs env nc1; wf_constraint ~exs:exs env nc2 + | NC_and (nc1, nc2) -> wf_constraint ~exs:exs env nc1; wf_constraint ~exs:exs env nc2 + | NC_true | NC_false -> () + + let counter = ref 0 + + let fresh_kid ?kid:(kid=mk_kid "") env = + let suffix = if Kid.compare kid (mk_kid "") = 0 then "#" else "#" ^ string_of_id (id_of_kid kid) in + let fresh = Kid_aux (Var ("'fv" ^ string_of_int !counter ^ suffix), Parse_ast.Unknown) in + incr counter; fresh + + let freshen_kid env kid (typq, typ) = + let fresh = fresh_kid ~kid:kid env in + (typquant_subst_kid kid fresh typq, typ_subst_kid kid fresh typ) + + let freshen_bind env bind = + List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars) + + let get_val_spec id env = + try + let bind = Bindings.find id env.top_val_specs in + typ_debug ("get_val_spec: Env has " ^ string_of_list ", " (fun (kid, bk) -> string_of_kid kid ^ " => " ^ string_of_base_kind_aux bk) (KBindings.bindings env.typ_vars)); + let bind' = List.fold_left (fun bind (kid, _) -> freshen_kid env kid bind) bind (KBindings.bindings env.typ_vars) in + typ_debug ("get_val_spec: freshened to " ^ string_of_bind bind'); + bind' + with + | Not_found -> typ_error (id_loc id) ("No val spec found for " ^ string_of_id id) + + let update_val_spec id bind env = + begin + typ_print ("Adding val spec binding " ^ string_of_id id ^ " :: " ^ string_of_bind bind); + { env with top_val_specs = Bindings.add id bind env.top_val_specs } + end + + let add_val_spec id bind env = + if Bindings.mem id env.top_val_specs + then typ_error (id_loc id) ("Identifier " ^ string_of_id id ^ " is already bound") + else update_val_spec id bind env + + let is_union_constructor id env = + let is_ctor id (Tu_aux (tu, _)) = match tu with + | Tu_id ctor_id when Id.compare id ctor_id = 0 -> true + | Tu_ty_id (_, ctor_id) when Id.compare id ctor_id = 0 -> true + | _ -> false + in + let type_unions = List.concat (List.map (fun (_, (_, tus)) -> tus) (Bindings.bindings env.variants)) in + List.exists (is_ctor id) type_unions let add_enum id ids env = if bound_typ_id env id @@ -666,14 +702,6 @@ end = struct try Bindings.find id env.registers with | Not_found -> typ_error (id_loc id) ("No register binding found for " ^ string_of_id id) - let get_overloads id env = - try Bindings.find id env.overloads with - | Not_found -> [] - - let add_overloads id ids env = - typ_print ("Adding overloads for " ^ string_of_id id ^ " [" ^ string_of_list ", " string_of_id ids ^ "]"); - { env with overloads = Bindings.add id ids env.overloads } - let is_extern id env backend = try not (Bindings.find id env.externs backend = None) with | Not_found -> false @@ -793,17 +821,6 @@ end = struct try Bindings.find id env.num_defs with | Not_found -> typ_raise (id_loc id) (Err_no_num_ident id) - let rec wf_constraint env (NC_aux (nc, _)) = - match nc with - | NC_equal (n1, n2) -> wf_nexp env n1; wf_nexp env n2 - | NC_not_equal (n1, n2) -> wf_nexp env n1; wf_nexp env n2 - | NC_bounded_ge (n1, n2) -> wf_nexp env n1; wf_nexp env n2 - | NC_bounded_le (n1, n2) -> wf_nexp env n1; wf_nexp env n2 - | NC_set (kid, ints) -> () (* MAYBE: We could demand that ints are all unique here *) - | NC_or (nc1, nc2) -> wf_constraint env nc1; wf_constraint env nc2 - | NC_and (nc1, nc2) -> wf_constraint env nc1; wf_constraint env nc2 - | NC_true | NC_false -> () - let get_constraints env = env.constraints let add_constraint (NC_aux (_, l) as constr) env = @@ -936,7 +953,7 @@ let lvector_typ env l typ = let initial_env = Env.empty - |> Env.add_typ_synonym (mk_id "atom") (fun _ args -> mk_typ (Typ_app (mk_id "range", args @ args))) + (* |> Env.add_typ_synonym (mk_id "atom") (fun _ args -> mk_typ (Typ_app (mk_id "range", args @ args))) *) (* Internal functions for Monomorphise.AtomToItself *) @@ -1066,6 +1083,9 @@ let rec normalize_typ env (Typ_aux (typ, l)) = | Typ_var kid -> Tnf_var kid | Typ_tup typs -> Tnf_tup (List.map (normalize_typ env) typs) | Typ_app (f, []) -> normalize_typ env (Typ_aux (Typ_id f, l)) + | Typ_app (Id_aux (Id "atom", _), [Typ_arg_aux (Typ_arg_nexp n, _)]) -> + let kid = Env.fresh_kid env in + Tnf_index_sort (IS_prop (kid, [(n, nvar kid); (nvar kid, n)])) | Typ_app (Id_aux (Id "range", _), [Typ_arg_aux (Typ_arg_nexp n1, _); Typ_arg_aux (Typ_arg_nexp n2, _)]) -> let kid = Env.fresh_kid env in Tnf_index_sort (IS_prop (kid, [(n1, nvar kid); (nvar kid, n2)])) @@ -1115,6 +1135,7 @@ let rec nexp_constraint env var_of (Nexp_aux (nexp, l)) = | Nexp_minus (nexp1, nexp2) -> Constraint.sub (nexp_constraint env var_of nexp1) (nexp_constraint env var_of nexp2) | Nexp_exp nexp -> Constraint.pow2 (nexp_constraint env var_of nexp) | Nexp_neg nexp -> Constraint.sub (Constraint.constant (big_int_of_int 0)) (nexp_constraint env var_of nexp) + | Nexp_app (id, nexps) -> Constraint.app (Env.get_smt_op id env) (List.map (nexp_constraint env var_of) nexps) let rec nc_constraint env var_of (NC_aux (nc, l)) = match nc with @@ -1248,6 +1269,7 @@ let rec nexp_frees ?exs:(exs=KidSet.empty) (Nexp_aux (nexp, l)) = | Nexp_times (n1, n2) -> KidSet.union (nexp_frees ~exs:exs n1) (nexp_frees ~exs:exs n2) | Nexp_sum (n1, n2) -> KidSet.union (nexp_frees ~exs:exs n1) (nexp_frees ~exs:exs n2) | Nexp_minus (n1, n2) -> KidSet.union (nexp_frees ~exs:exs n1) (nexp_frees ~exs:exs n2) + | Nexp_app (id, ns) -> List.fold_left KidSet.union KidSet.empty (List.map (fun n -> nexp_frees ~exs:exs n) ns) | Nexp_exp n -> nexp_frees ~exs:exs n | Nexp_neg n -> nexp_frees ~exs:exs n @@ -1474,6 +1496,9 @@ let rec unify l env typ1 typ2 = | Invalid_argument _ -> unify_error l (string_of_typ typ1 ^ " cannot be unified with " ^ string_of_typ typ2 ^ " tuple type is of different length") end + | Typ_app (f1, [arg1a; arg1b]), Typ_app (f2, [arg2]) + when Id.compare (mk_id "range") f1 = 0 && Id.compare (mk_id "atom") f2 = 0 -> + unify_typ_arg_list 0 KBindings.empty [] [] [arg1a; arg1b] [arg2; arg2] | Typ_app (f1, args1), Typ_app (f2, args2) when Id.compare f1 f2 = 0 -> unify_typ_arg_list 0 KBindings.empty [] [] args1 args2 | _, _ -> unify_error l (string_of_typ typ1 ^ " cannot be unified with " ^ string_of_typ typ2) @@ -2115,6 +2140,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ begin match letbind with | LB_val (P_aux (P_typ (ptyp, _), _) as pat, bind) -> + Env.wf_typ env ptyp; let checked_bind = crule check_exp env bind ptyp in let tpat, env = bind_pat env pat ptyp in annot_exp (E_let (LB_aux (LB_val (tpat, checked_bind), (let_loc, None)), crule check_exp env exp typ)) typ @@ -2126,6 +2152,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ | E_app_infix (x, op, y), _ -> check_exp env (E_aux (E_app (deinfix op, [x; y]), (l, ()))) typ | E_app (f, [E_aux (E_constraint nc, _)]), _ when Id.compare f (mk_id "_prove") = 0 -> + Env.wf_constraint env nc; if prove env nc then annot_exp (E_lit (L_aux (L_unit, Parse_ast.Unknown))) unit_typ else typ_error l ("Cannot prove " ^ string_of_n_constraint nc) @@ -2405,6 +2432,7 @@ and infer_pat env (P_aux (pat_aux, (l, ())) as pat) = | Enum enum -> annot_pat (P_id v) enum, env end | P_typ (typ_annot, pat) -> + Env.wf_typ env typ_annot; let (typed_pat, env) = bind_pat env pat typ_annot in annot_pat (P_typ (typ_annot, typed_pat)) typ_annot, env | P_lit lit -> @@ -2695,6 +2723,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) = | E_lit lit -> annot_exp (E_lit lit) (infer_lit env lit) | E_sizeof nexp -> annot_exp (E_sizeof nexp) (mk_typ (Typ_app (mk_id "atom", [mk_typ_arg (Typ_arg_nexp nexp)]))) | E_constraint nc -> + Env.wf_constraint env nc; annot_exp (E_constraint nc) bool_typ | E_field (exp, field) -> begin @@ -3392,6 +3421,8 @@ let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls) let check_val_spec env (VS_aux (vs, (l, _))) = let (id, quants, typ, env) = match vs with | VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id, ext_opt, is_cast) -> + let env = match ext_opt "smt" with Some op -> Env.add_smt_op id op env | None -> env in + Env.wf_typ (add_typquant quants env) typ; let env = (* match ext_opt with | None -> env diff --git a/test/typecheck/pass/ex_cast.sail b/test/typecheck/pass/ex_cast.sail index 5ea22d14..964bfa72 100644 --- a/test/typecheck/pass/ex_cast.sail +++ b/test/typecheck/pass/ex_cast.sail @@ -3,7 +3,7 @@ default Order dec val cast int -> exist 'n. [:'n:] effect pure ex_int -val [:'n:] -> bit['n] effect pure zeros +val forall 'n. [:'n:] -> bit['n] effect pure zeros val int -> unit effect pure test diff --git a/test/typecheck/pass/exint.sail b/test/typecheck/pass/exint.sail index dfe51eb9..1239fa44 100644 --- a/test/typecheck/pass/exint.sail +++ b/test/typecheck/pass/exint.sail @@ -1,9 +1,9 @@ typedef Int = exist 'n. [:'n:] -val ([:'n:], [:'m:]) -> exist 'o, 'o = 'n + 'm. [:'o:] effect pure add +val forall 'n, 'm. ([:'n:], [:'m:]) -> exist 'o, 'o = 'n + 'm. [:'o:] effect pure add -val ([:'n:], [:'m:]) -> exist 'o, 'o = 'n * 'm. [:'o:] effect pure mult +val forall 'n, 'm. ([:'n:], [:'m:]) -> exist 'o, 'o = 'n * 'm. [:'o:] effect pure mult overload (deinfix +) [add] diff --git a/test/typecheck/pass/lexp_memory.sail b/test/typecheck/pass/lexp_memory.sail index cc84130f..321fb315 100644 --- a/test/typecheck/pass/lexp_memory.sail +++ b/test/typecheck/pass/lexp_memory.sail @@ -48,7 +48,7 @@ val forall Num 'n, Num 'm, Order 'ord. (vector<'n,'m,'ord,bit>, vector<'n,'m,'or overload (deinfix ==) [eq_vec] -val extern forall Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec +val extern forall Num 'l, Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec val cast forall Nat 'n, Nat 'l. [|0:1|] -> vector<'n,'l,dec,bit> effect pure cast_01_vec function forall Num 'n, Num 'l. (vector<'n,'l,dec,bit>) cast_01_vec i = to_vec_dec (sizeof 'n, sizeof 'l, i) diff --git a/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail b/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail index 0160dd8a..54ae354f 100644 --- a/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail +++ b/test/typecheck/pass/mips_CP0Cause_BD_assign1.sail @@ -1,7 +1,7 @@ val cast forall Num 'n. [:1:] -> vector<'n,1,dec,bit> effect pure cast_1_vec val cast forall Num 'n. [:0:] -> vector<'n,1,dec,bit> effect pure cast_0_vec -val extern forall Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec +val extern forall Num 'l, Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec function forall Num 'n. (vector<'n,1,dec,bit>) cast_1_vec i = to_vec_dec (sizeof 'n, 1, i) function forall Num 'n. (vector<'n,1,dec,bit>) cast_0_vec i = to_vec_dec (sizeof 'n, 1, i) diff --git a/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail b/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail index 847bca60..2e80f538 100644 --- a/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail +++ b/test/typecheck/pass/mips_CP0Cause_BD_assign2.sail @@ -1,7 +1,7 @@ val cast forall Num 'n. [:1:] -> vector<'n,1,dec,bit> effect pure cast_1_vec val cast forall Num 'n. [:0:] -> vector<'n,1,dec,bit> effect pure cast_0_vec -val extern forall Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec +val extern forall Num 'l, Num 'm. ([:'l:], [:'m:], int) -> vector<'l,'m,dec,bit> effect pure to_vec_dec function forall Num 'n. (vector<'n,1,dec,bit>) cast_1_vec i = to_vec_dec (sizeof 'n, 1, i) function forall Num 'n. (vector<'n,1,dec,bit>) cast_0_vec i = to_vec_dec (sizeof 'n, 1, i) |