summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/ast.ml1
-rw-r--r--src/type_check_new.ml67
-rw-r--r--src/type_check_new.mli7
-rw-r--r--test/typecheck/fail/assignment_simple1.sail1
4 files changed, 54 insertions, 22 deletions
diff --git a/src/ast.ml b/src/ast.ml
index c21bd225..17ec2fe8 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -575,7 +575,6 @@ and 'a def = (* Top-level definition *)
| DEF_reg_dec of 'a dec_spec (* register declaration *)
| DEF_comm of 'a dec_comm (* generated comments *)
-
type
'a defs = (* Definition sequence *)
Defs of ('a def) list
diff --git a/src/type_check_new.ml b/src/type_check_new.ml
index 5dedd777..7bede643 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 2
let depth = ref 0
let typ_debug m = if !debug > 1 then prerr_endline m else ()
@@ -235,13 +235,16 @@ end
module Bindings = Map.Make(Id)
module KBindings = Map.Make(Kid)
module KidSet = Set.Make(Kid)
-
+
+type mut = Immutable | Mutable
+
module Env : sig
type t
val get_val_spec : id -> t -> typquant * typ
val add_val_spec : id -> typquant * typ -> t -> t
- val get_local : id -> t -> typ
- val add_local : id -> typ -> t -> t
+ val get_local : id -> t -> mut * typ
+ val add_local : id -> mut * typ -> t -> t
+ val is_mutable : id -> t -> bool
val get_constraints : t -> n_constraint list
val add_constraint : n_constraint -> t -> t
val get_typ_var : kid -> t -> base_kind_aux
@@ -259,7 +262,7 @@ module Env : sig
end = struct
type t =
{ top_val_specs : (typquant * typ) Bindings.t;
- locals : typ Bindings.t;
+ locals : (mut * typ) Bindings.t;
typ_vars : base_kind_aux KBindings.t;
typ_synonyms : (typ_arg list -> typ) Bindings.t;
constraints : n_constraint list;
@@ -294,12 +297,25 @@ end = struct
let get_local id env =
try Bindings.find id env.locals with
- | Not_found -> typ_error (id_loc id) ("No val spec found for " ^ string_of_id id)
-
- let add_local id typ env =
+ | Not_found -> typ_error (id_loc id) ("No local binding found for " ^ string_of_id id)
+
+ let is_mutable id env =
+ try
+ let (mut, _) = Bindings.find id env.locals in
+ match mut with
+ | Mutable -> true
+ | Immutable -> false
+ with
+ | Not_found -> typ_error (id_loc id) ("No local binding found for " ^ string_of_id id)
+
+ let string_of_mtyp (mut, typ) = match mut with
+ | Immutable -> string_of_typ typ
+ | Mutable -> "ref<" ^ string_of_typ typ ^ ">"
+
+ let add_local id mtyp env =
begin
- typ_print ("Adding local binding " ^ string_of_id id ^ " :: " ^ string_of_typ typ);
- { env with locals = Bindings.add id typ env.locals }
+ typ_print ("Adding local binding " ^ string_of_id id ^ " :: " ^ string_of_mtyp mtyp);
+ { env with locals = Bindings.add id mtyp env.locals }
end
let get_typ_var kid env =
@@ -470,6 +486,8 @@ let rec normalize_typ env (Typ_aux (typ, l)) =
| 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)]))
+ | Typ_app ((Id_aux (Id "vector", _) as vector), args) ->
+ Tnf_app (vector, List.map (normalize_typ_arg env) args)
| Typ_app (id, args) -> normalize_typ env (Env.get_typ_synonym id env args)
| Typ_fn _ -> typ_error l ("Cannot normalize function type " ^ string_of_typ (Typ_aux (typ, l)))
and normalize_typ_arg env (Typ_arg_aux (typ_arg, _)) =
@@ -674,11 +692,17 @@ let rec nexp_identical (Nexp_aux (nexp1, _)) (Nexp_aux (nexp2, _)) =
| Nexp_neg n1, Nexp_neg n2 -> nexp_identical n1 n2
| _, _ -> false
-let rec unify_nexps l (Nexp_aux (nexp_aux1, _) as nexp1) nexp2 =
+let rec unify_nexps l (Nexp_aux (nexp_aux1, _) as nexp1) (Nexp_aux (nexp_aux2, _) as nexp2) =
typ_debug ("UNIFYING NEXPS " ^ string_of_nexp nexp1 ^ " AND " ^ string_of_nexp nexp2);
match nexp_aux1 with
| Nexp_id v -> typ_error l "Unimplemented Nexp_id in unify nexp"
- | Nexp_var kid -> (kid, nexp2)
+ | Nexp_var kid -> Some (kid, nexp2)
+ | Nexp_constant c1 ->
+ begin
+ match nexp_aux2 with
+ | Nexp_constant c2 -> if c1 = c2 then None else typ_error l "Constants are not the same"
+ | _ -> typ_error l "Unification error"
+ end
| Nexp_sum (n1a, n1b) ->
if KidSet.is_empty (nexp_frees n1b)
then unify_nexps l n1a (nminus nexp2 n1b)
@@ -726,7 +750,12 @@ let unify l env typ1 typ2 =
| _, _ -> typ_error l (string_of_typ typ1 ^ " cannot be unified with " ^ string_of_typ typ2)
and unify_typ_args l (Typ_arg_aux (typ_arg_aux1, _) as typ_arg1) (Typ_arg_aux (typ_arg_aux2, _) as typ_arg2) =
match typ_arg_aux1, typ_arg_aux2 with
- | Typ_arg_nexp n1, Typ_arg_nexp n2 -> let (kid, unifier) = unify_nexps l n1 n2 in KBindings.singleton kid unifier
+ | Typ_arg_nexp n1, Typ_arg_nexp n2 ->
+ begin
+ match unify_nexps l n1 n2 with
+ | Some (kid, unifier) -> KBindings.singleton kid unifier
+ | None -> KBindings.empty
+ end
| Typ_arg_typ typ1, Typ_arg_typ typ2 -> unify_typ l typ1 typ2
| Typ_arg_order _, Typ_arg_order _ -> assert false (* FIXME *)
| Typ_arg_effect _, Typ_arg_effect _ -> assert false
@@ -746,7 +775,7 @@ let infer_lit env (L_aux (lit_aux, l) as lit) =
let rec bind_pat env (P_aux (pat_aux, (l, _)) as pat) (Typ_aux (typ_aux, _) as typ) =
let annot_pat pat typ = P_aux (pat, (l, Some (env, typ))) in
match pat_aux with
- | P_id v -> annot_pat (P_id v) typ, Env.add_local v typ env
+ | P_id v -> annot_pat (P_id v) typ, Env.add_local v (Immutable, typ) env
| P_wild -> annot_pat P_wild typ, env
| P_typ (typ_annot, pat) ->
begin
@@ -779,11 +808,11 @@ let rec bind_pat env (P_aux (pat_aux, (l, _)) as pat) (Typ_aux (typ_aux, _) as t
and bind_lexp env (LEXP_aux (lexp_aux, (l, _))) typ =
let annot_lexp lexp typ = LEXP_aux (lexp, (l, Some (env, typ))) in
match lexp_aux with
- | LEXP_id v -> annot_lexp (LEXP_id v) typ, Env.add_local v typ env
+ | LEXP_id v -> annot_lexp (LEXP_id v) typ, Env.add_local v (Mutable, typ) env
| LEXP_cast (typ_annot, v) ->
begin
subtyp l env typ typ_annot;
- annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v typ_annot env
+ annot_lexp (LEXP_cast (typ_annot, v)) typ, Env.add_local v (Mutable, typ_annot) env
end
| LEXP_tup lexps ->
begin
@@ -827,7 +856,7 @@ let irule r env exp =
typ_print ("Infer " ^ string_of_exp exp ^ " => " ^ string_of_typ (typ_of inferred_exp));
decr depth;
inferred_exp
-
+
let rec check_exp env (E_aux (exp_aux, (l, _)) as exp : 'a exp) (Typ_aux (typ_aux, _) as typ) : tannot exp =
let annot_exp exp typ = E_aux (exp, (l, Some (env, typ))) in
match (exp_aux, typ_aux) with
@@ -873,7 +902,7 @@ and bind_assignment env lexp (E_aux (_, (l, _)) as exp) =
and infer_exp env (E_aux (exp_aux, (l, _)) as exp : 'a exp) : tannot exp =
let annot_exp exp typ = E_aux (exp, (l, Some (env, typ))) in
match exp_aux with
- | E_id v -> annot_exp (E_id v) (Env.get_local v env)
+ | E_id v -> annot_exp (E_id v) (snd (Env.get_local v env))
| 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_return exp ->
@@ -986,7 +1015,7 @@ let check_val_spec env (VS_aux (vs, (l, _))) =
let check_default env (DT_aux (ds, l)) =
match ds with
- | DT_kind _ -> DEF_default (DT_aux (ds,l)), env
+ | DT_kind _ -> DEF_default (DT_aux (ds,l)), env (* Check: Is this supposed to do nothing? *)
| DT_order (Ord_aux (Ord_inc, _)) -> DEF_default (DT_aux (ds, l)), Env.set_default_order_inc env
| DT_order (Ord_aux (Ord_dec, _)) -> DEF_default (DT_aux (ds, l)), Env.set_default_order_dec env
| DT_order (Ord_aux (Ord_var _, _)) -> typ_error l "Cannot have variable default order"
diff --git a/src/type_check_new.mli b/src/type_check_new.mli
index 98e1171e..54140267 100644
--- a/src/type_check_new.mli
+++ b/src/type_check_new.mli
@@ -43,12 +43,15 @@
open Ast
+type mut = Immutable | Mutable
+
module Env : sig
type t
val get_val_spec : id -> t -> typquant * typ
val add_val_spec : id -> typquant * typ -> t -> t
- val get_local : id -> t -> typ
- val add_local : id -> typ -> t -> t
+ val get_local : id -> t -> mut * typ
+ val add_local : id -> mut * typ -> t -> t
+ val is_mutable : id -> t -> bool
val get_constraints : t -> n_constraint list
val add_constraint : n_constraint -> t -> t
val get_typ_var : kid -> t -> base_kind_aux
diff --git a/test/typecheck/fail/assignment_simple1.sail b/test/typecheck/fail/assignment_simple1.sail
index 1ad9f8bf..3778d84a 100644
--- a/test/typecheck/fail/assignment_simple1.sail
+++ b/test/typecheck/fail/assignment_simple1.sail
@@ -8,6 +8,7 @@ val unit -> [:10:] effect pure test
function [:10:] test () =
{
z := 9;
+ z := 10;
z
}
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 14:24:45 +0000