summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/initial_check.ml8
-rw-r--r--src/initial_check.mli4
-rw-r--r--src/main.ml5
-rw-r--r--src/process_file.ml9
-rw-r--r--src/process_file.mli3
-rw-r--r--src/test/test1.sail2
-rw-r--r--src/type_check.ml304
-rw-r--r--src/type_check.mli14
-rw-r--r--src/type_internal.ml30
-rw-r--r--src/type_internal.mli9
10 files changed, 367 insertions, 21 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml
index b84cfdcc..7a4cc413 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -4,7 +4,7 @@ open Ast
type kind = Type_internal.kind
type typ = Type_internal.t
-type envs = Nameset.t * kind Envmap.t * t Envmap.t
+type envs = Nameset.t * kind Envmap.t * tannot Envmap.t
type 'a envs_out = 'a * envs
let id_to_string (Id_aux(id,l)) =
@@ -666,12 +666,12 @@ let rec to_ast_defs_helper envs partial_defs = function
then (fst !d) :: defs, envs, partial_defs
else typ_error l "Scattered type definition never ended" (Some id) None None))
-let to_ast (default_names : Nameset.t) (kind_env : kind Envmap.t) (typ_env : t Envmap.t) (Parse_ast.Defs(defs)) =
- let defs,_,partial_defs = to_ast_defs_helper (default_names,kind_env,typ_env) [] defs in
+let to_ast (default_names : Nameset.t) (kind_env : kind Envmap.t) (typ_env : tannot Envmap.t) (Parse_ast.Defs(defs)) =
+ let defs,(_,k_env,_),partial_defs = to_ast_defs_helper (default_names,kind_env,typ_env) [] defs in
List.iter
(fun (id,(d,k)) ->
(match !d with
| (DEF_aux(_,(l,_)),false) -> typ_error l "Scattered definition never ended" (Some id) None None
| (_, true) -> ()))
partial_defs;
- (Defs defs)
+ (Defs defs),k_env
diff --git a/src/initial_check.mli b/src/initial_check.mli
index 03b34e78..fd9444da 100644
--- a/src/initial_check.mli
+++ b/src/initial_check.mli
@@ -4,7 +4,7 @@ open Type_internal
type kind = Type_internal.kind
type typ = Type_internal.t
-type envs = Nameset.t * kind Envmap.t * typ Envmap.t
+type envs = Nameset.t * kind Envmap.t * tannot Envmap.t
type 'a envs_out = 'a * envs
-val to_ast : Nameset.t -> kind Envmap.t -> typ Envmap.t -> Parse_ast.defs -> tannot defs
+val to_ast : Nameset.t -> kind Envmap.t -> tannot Envmap.t -> Parse_ast.defs -> tannot defs * kind Envmap.t
diff --git a/src/main.ml b/src/main.ml
index 5698b81a..639da7d7 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -393,12 +393,13 @@ let main() =
then Printf.printf "L2 pre alpha \n"
else let parsed = (List.map (fun f -> (f,(parse_file f))) !opt_file_arguments) in
let asts = (List.map (fun (f,past) -> (f,convert_ast past)) parsed) in
+ let chkedasts = (List.map (fun (f,(ast,kenv)) -> (f,check_ast ast kenv)) asts) in
begin
(if !(opt_print_verbose)
- then ((Pretty_print.pp_defs Format.std_formatter) (snd (List.hd asts)))
+ then ((Pretty_print.pp_defs Format.std_formatter) (snd (List.hd chkedasts)))
else ());
(if !(opt_print_lem)
- then output "" Lem_ast_out asts
+ then output "" Lem_ast_out chkedasts
else ());
end
diff --git a/src/process_file.ml b/src/process_file.ml
index b07caca4..29635f91 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -87,9 +87,16 @@ let parse_file (f : string) : Parse_ast.defs =
| Lexer.LexError(s,p) ->
raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s)))
-let convert_ast (defs : Parse_ast.defs) : Type_internal.tannot Ast.defs =
+let convert_ast (defs : Parse_ast.defs) : (Type_internal.tannot Ast.defs * kind Envmap.t)=
Initial_check.to_ast Nameset.empty Type_internal.initial_kind_env Envmap.empty defs
+
+let check_ast (defs : Type_internal.tannot Ast.defs) (k : kind Envmap.t) : Type_internal.tannot Ast.defs =
+ let d_env = { Type_check.k_env = k; Type_check.abbrevs = Envmap.empty;
+ Type_check.namesch = Envmap.empty; Type_check.enum_env = Envmap.empty;
+ Type_check.rec_env = []; } in
+ Type_check.check (Type_check.Env (d_env, Type_internal.initial_typ_env)) defs
+
let open_output_with_check file_name =
let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in
let o' = Format.formatter_of_out_channel o in
diff --git a/src/process_file.mli b/src/process_file.mli
index 8dde8e02..49fe8254 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -45,7 +45,8 @@
(**************************************************************************)
val parse_file : string -> Parse_ast.defs
-val convert_ast : Parse_ast.defs -> Type_internal.tannot Ast.defs
+val convert_ast : Parse_ast.defs -> Type_internal.tannot Ast.defs * Type_internal.kind Type_internal.Envmap.t
+val check_ast: Type_internal.tannot Ast.defs -> Type_internal.kind Type_internal.Envmap.t -> Type_internal.tannot Ast.defs
type out_type =
| Lem_ast_out
diff --git a/src/test/test1.sail b/src/test/test1.sail
index 3580f3e6..78258929 100644
--- a/src/test/test1.sail
+++ b/src/test/test1.sail
@@ -8,7 +8,7 @@ typedef int_list [name = "il"] = list<nat>
typedef reco = const struct forall 'i, 'a, 'b. { 'a['i] v; 'b w; }
typedef maybe = const union forall 'a. { Nne; 'a Sme; }
typedef colors = enumerate { red; green; blue }
-typedef creg = register bits [5:'i] { 5 : h ; 6..7 : j}
+typedef creg = register bits [5:10] { 5 : h ; 6..7 : j}
let bool e = true
let bit v = bitzero
let ( bit [ 32 ] ) v1 = 0b101
diff --git a/src/type_check.ml b/src/type_check.ml
new file mode 100644
index 00000000..17def702
--- /dev/null
+++ b/src/type_check.ml
@@ -0,0 +1,304 @@
+open Ast
+open Type_internal
+type kind = Type_internal.kind
+type typ = Type_internal.t
+type 'a emap = 'a Envmap.t
+
+type rec_kind = Record | Register
+type def_envs = {
+ k_env: kind emap;
+ abbrevs: tannot emap;
+ namesch : tannot emap;
+ enum_env : (string list) emap;
+ rec_env : (string * rec_kind * ((string * tannot) list)) list;
+ }
+type envs = Env of def_envs * tannot emap
+type 'a envs_out = 'a * envs
+
+let id_to_string (Id_aux(id,l)) =
+ match id with
+ | Id(s) -> s
+ | DeIid(s) -> s
+
+let typ_error l msg =
+ raise (Reporting_basic.err_typ
+ l
+ (msg ))
+
+
+(*No checks necessary, unlike conversion in initial_check*)
+let kind_to_k (K_aux((K_kind baseks),l)) =
+ let bk_to_k (BK_aux(bk,l')) =
+ match bk with
+ | BK_type -> { k = K_Typ}
+ | BK_nat -> { k = K_Nat}
+ | BK_order -> { k = K_Ord}
+ | BK_effect -> { k = K_Efct}
+ in
+ match baseks with
+ | [] -> raise (Reporting_basic.err_unreachable l "Empty kind")
+ | [bk] -> bk_to_k bk
+ | bks -> (match List.rev bks with
+ | [] -> raise (Reporting_basic.err_unreachable l "Empty after reverse")
+ | out::args -> {k = K_Lam( List.map bk_to_k (List.rev args), bk_to_k out) })
+
+let rec typ_to_t (Typ_aux(typ,l)) =
+ match typ with
+ | Typ_id i -> {t = Tid (id_to_string i)}
+ | Typ_var (Kid_aux((Var i),l')) -> {t = Tvar i}
+ | Typ_fn (ty1,ty2,e) -> {t = Tfn (typ_to_t ty1,typ_to_t ty2,aeffect_to_effect e)}
+ | Typ_tup(tys) -> {t = Ttup (List.map typ_to_t tys) }
+ | Typ_app(i,args) -> {t = Tapp (id_to_string i,List.map typ_arg_to_targ args) }
+and typ_arg_to_targ (Typ_arg_aux(ta,l)) =
+ match ta with
+ | Typ_arg_nexp n -> TA_nexp (anexp_to_nexp n)
+ | Typ_arg_typ t -> TA_typ (typ_to_t t)
+ | Typ_arg_order o -> TA_ord (aorder_to_ord o)
+ | Typ_arg_effect e -> TA_eft (aeffect_to_effect e)
+and anexp_to_nexp ((Nexp_aux(n,l)) : Ast.nexp) : nexp =
+ match n with
+ | Nexp_var (Kid_aux((Var i),l')) -> {nexp = Nvar i}
+ | Nexp_constant i -> {nexp=Nconst i}
+ | Nexp_times(n1,n2) -> {nexp=Nmult(anexp_to_nexp n1,anexp_to_nexp n2)}
+ | Nexp_sum(n1,n2) -> {nexp=Nadd(anexp_to_nexp n1,anexp_to_nexp n2)}
+ | Nexp_exp n -> {nexp=N2n(anexp_to_nexp n)}
+and aeffect_to_effect ((Effect_aux(e,l)) : Ast.effect) : effect =
+ match e with
+ | Effect_var (Kid_aux((Var i),l')) -> {effect = Evar i}
+ | Effect_set effects -> {effect = Eset effects}
+and aorder_to_ord (Ord_aux(o,l) : Ast.order) =
+ match o with
+ | Ord_var (Kid_aux((Var i),l')) -> {order = Ovar i}
+ | Ord_inc -> {order = Oinc}
+ | Ord_dec -> {order = Odec}
+
+let rec eval_to_nexp_const n =
+ match n.nexp with
+ | Nconst i -> n
+ | Nmult(n1,n2) ->
+ (match (eval_to_nexp_const n1).nexp,(eval_to_nexp_const n2).nexp with
+ | Nconst i1, Nconst i2 -> {nexp=Nconst (i1*i2)}
+ | _,_ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Var found in eval_to_nexp_const"))
+ | Nadd(n1,n2) ->
+ (match (eval_to_nexp_const n1).nexp,(eval_to_nexp_const n2).nexp with
+ | Nconst i1, Nconst i2 -> {nexp=Nconst (i1+i2)}
+ | _,_ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Var found in eval_to_nexp_const"))
+ | Nneg n1 ->
+ (match (eval_to_nexp_const n1).nexp with
+ | Nconst i -> {nexp = Nconst(- i)}
+ | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Var found in eval_to_nexp_const"))
+ | N2n n1 ->
+ (match (eval_to_nexp_const n1).nexp with
+ | Nconst i ->
+ let rec two_pow = function
+ | 0 -> 1;
+ | n -> 2* (two_pow n-1) in
+ {nexp = Nconst(two_pow i)}
+ | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Var found in eval_to_nexp_const"))
+ | Nvar _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Var found in eval_to_nexp_const")
+
+
+let rec quants_to_consts (Env (d_env,t_env)) qis : (t_params * nexp_range list) =
+ match qis with
+ | [] -> [],[]
+ | (QI_aux(qi,l))::qis ->
+ let (ids,cs) = quants_to_consts (Env (d_env,t_env)) qis in
+ (match qi with
+ | QI_id(KOpt_aux(ki,l')) ->
+ (match ki with
+ | KOpt_none (Kid_aux((Var i),l'')) ->
+ (match Envmap.apply d_env.k_env i with
+ | Some k -> ((i,k)::ids,cs)
+ | None -> raise (Reporting_basic.err_unreachable l'' "Unkinded id without default after initial check"))
+ | KOpt_kind(kind,Kid_aux((Var i),l'')) -> ((i,kind_to_k kind)::ids,cs))
+ | QI_const(NC_aux(nconst,l')) ->
+ (match nconst with
+ | NC_fixed(n1,n2) -> (ids,Eq(l',anexp_to_nexp n1,anexp_to_nexp n2)::cs)
+ | NC_bounded_ge(n1,n2) -> (ids,GtEq(l',anexp_to_nexp n1,anexp_to_nexp n2)::cs)
+ | NC_bounded_le(n1,n2) -> (ids,LtEq(l',anexp_to_nexp n1,anexp_to_nexp n2)::cs)
+ | NC_nat_set_bounded(Kid_aux((Var i),l''), bounds) -> (ids,In(l',i,bounds)::cs)))
+
+
+let typq_to_params envs (TypQ_aux(tq,l)) =
+ match tq with
+ | TypQ_tq(qis) -> quants_to_consts envs qis
+ | TypQ_no_forall -> [],[]
+
+let typschm_to_tannot envs ((TypSchm_aux(typschm,l)):typschm) (tag : tag) : tannot =
+ match typschm with
+ | TypSchm_ts(tq,typ) ->
+ let t = typ_to_t typ in
+ let (ids,constraints) = typq_to_params envs tq in
+ Some((ids,t),tag,constraints)
+
+let into_register (t : tannot) : tannot =
+ match t with
+ | Some((ids,ty),tag,constraints) -> Some((ids, {t= Tapp("register",[TA_typ ty])}),tag,constraints)
+ | None -> None
+
+let rec check_exp envs expect_t (E_aux(e,annot)) =
+ match e with
+ | E_block(exps) ->
+ let (exps',annot',envs,sc) = check_block envs envs expect_t exps in
+ (E_aux(E_block(exps'),annot'), envs,sc)
+ | E_id(id) -> let (names,kinds,typs) = envs in
+ (match Envmap.apply typs (id_to_string id) with
+ | Some(typ) -> (E_aux(e,annot),envs,[])
+ | None -> (E_aux(e,annot),envs,[]))
+
+and check_block orig_envs envs expect_t exps =
+ match exps with
+ | [] -> ([],(Parse_ast.Unknown,None),orig_envs,[])
+ | [e] -> let (E_aux(e',annot),envs,sc) = check_exp envs expect_t e in
+ ([E_aux(e',annot)],annot,orig_envs,sc)
+ | e::exps -> let (e',envs,sc) = check_exp envs expect_t (*wrong*) e in
+ let (exps',annot',orig_envs,sc') = check_block orig_envs envs expect_t exps in
+ ((e'::exps'),annot',orig_envs,sc@sc')
+
+(*val check_type_def : envs -> (tannot type_def) -> (tannot type_def) envs_out*)
+let check_type_def envs (TD_aux(td,(l,annot))) =
+ let (Env(d_env,t_env)) = envs in
+ match td with
+ | TD_abbrev(id,nmscm,typschm) ->
+ let tan = typschm_to_tannot envs typschm Emp in
+ (TD_aux(td,(l,tan)),
+ Env( { d_env with abbrevs = Envmap.insert d_env.abbrevs ((id_to_string id),tan)},t_env))
+ | TD_record(id,nmscm,typq,fields,_) ->
+ let id' = id_to_string id in
+ let (params,constraints) = typq_to_params envs typq in
+ let tyannot = Some((params,{t=Tid id'}),Emp,constraints) in
+ let fields' = List.map
+ (fun (ty,i)->(id_to_string i),Some((params,(typ_to_t ty)),Emp,constraints)) fields in
+ (TD_aux(td,(l,tyannot)),Env({d_env with rec_env = (id',Record,fields')::d_env.rec_env},t_env))
+ | TD_variant(id,nmscm,typq,arms,_) ->
+ let id' = id_to_string id in
+ let (params,constraints) = typq_to_params envs typq in
+ let ty = {t=Tid id'} in
+ let tyannot = Some((params,ty),Constructor,constraints) in
+ let arm_t input = Some((params,{t=Tfn(input,ty,{effect=Eset []})}),Constructor,constraints) in
+ let arms' = List.map
+ (fun (Tu_aux(tu,l')) ->
+ match tu with
+ | Tu_id i -> ((id_to_string i),(arm_t {t=Tid "unit"}))
+ | Tu_ty_id(typ,i)-> ((id_to_string i),(arm_t (typ_to_t typ))))
+ arms in
+ let t_env = List.fold_right (fun (id,tann) t_env -> Envmap.insert t_env (id,tann)) arms' t_env in
+ (TD_aux(td,(l,tyannot)),(Env (d_env,t_env)))
+ | TD_enum(id,nmscm,ids,_) ->
+ let id' = id_to_string id in
+ let ids' = List.map id_to_string ids in
+ let ty = Some (([],{t = Tid id' }),Enum,[]) in
+ let t_env = List.fold_right (fun id t_env -> Envmap.insert t_env (id,ty)) ids' t_env in
+ let enum_env = Envmap.insert d_env.enum_env (id',ids') in
+ (TD_aux(td,(l,ty)),Env({d_env with enum_env = enum_env;},t_env))
+ | TD_register(id,base,top,ranges) ->
+ let id' = id_to_string id in
+ let basei = eval_to_nexp_const(anexp_to_nexp base) in
+ let topi = eval_to_nexp_const(anexp_to_nexp top) in
+ match basei.nexp,topi.nexp with
+ | Nconst b, Nconst t ->
+ if b <= t then (
+ let ty = {t = Tapp("vector",[TA_nexp basei; TA_nexp{nexp=Nconst(t-b)};
+ TA_ord({order = Oinc}); TA_typ({t = Tid "bit"});])} in
+ let franges =
+ List.map
+ (fun ((BF_aux(idx,l)),id) ->
+ let (base,climb) =
+ match idx with
+ | BF_single i ->
+ if b <= i && i <= t
+ then {nexp=Nconst i},{nexp=Nconst 0}
+ else typ_error l ("register type declaration " ^ id' ^ " contains a field specification outside of the declared register size")
+ | BF_range(i1,i2) ->
+ if i1<i2
+ then if b<=i1 && i2<=t
+ then {nexp=Nconst i1},{nexp=Nconst (i2 - i1)}
+ else typ_error l ("register type declaration " ^ id' ^ " contains a field specification outside of the declared register size")
+ else typ_error l ("register type declaration " ^ id' ^ " is not consistently increasing")
+ | BF_concat _ -> assert false (* What is this supposed to imply again?*) in
+ ((id_to_string id),
+ Some(([],{t=Tapp("vector",[TA_nexp base;TA_nexp climb;TA_ord({order=Oinc});TA_typ({t= Tid "bit"})])}),Emp,[])))
+ ranges
+ in
+ let tannot = into_register (Some(([],ty),Emp,[])) in
+ (TD_aux(td,(l,tannot)),
+ Env({d_env with rec_env = ((id',Register,franges)::d_env.rec_env);
+ abbrevs = Envmap.insert d_env.abbrevs (id',tannot)},t_env)))
+ else (
+ let ty = {t = Tapp("vector",[TA_nexp basei; TA_nexp{nexp=Nconst(b-t)};
+ TA_ord({order = Odec}); TA_typ({t = Tid "bit"});])} in
+ let franges =
+ List.map
+ (fun ((BF_aux(idx,l)),id) ->
+ let (base,climb) =
+ match idx with
+ | BF_single i ->
+ if b >= i && i >= t
+ then {nexp=Nconst i},{nexp=Nconst 0}
+ else typ_error l ("register type declaration " ^ id' ^ " contains a field specification outside of the declared register size")
+ | BF_range(i1,i2) ->
+ if i1>i2
+ then if b>=i1 && i2>=t
+ then {nexp=Nconst i1},{nexp=Nconst (i1 - i2)}
+ else typ_error l ("register type declaration " ^ id' ^ " contains a field specification outside of the declared register size")
+ else typ_error l ("register type declaration " ^ id' ^ " is not consistently decreasing")
+ | BF_concat _ -> assert false (* What is this supposed to imply again?*) in
+ ((id_to_string id),
+ Some(([],{t=Tapp("vector",[TA_nexp base;TA_nexp climb;TA_ord({order=Odec});TA_typ({t= Tid "bit"})])}),Emp,[])))
+ ranges
+ in
+ let tannot = into_register (Some(([],ty),Emp,[])) in
+ (TD_aux(td,(l,tannot)),
+ Env({d_env with rec_env = (id',Register,franges)::d_env.rec_env;
+ abbrevs = Envmap.insert d_env.abbrevs (id',tannot)},t_env)))
+
+let check_val_spec envs (VS_aux(vs,(l,annot))) =
+ let (Env(d_env,t_env)) = envs in
+ match vs with
+ | VS_val_spec(typs,id) ->
+ let tannot = typschm_to_tannot envs typs Emp in
+ (VS_aux(vs,(l,tannot)),
+ Env(d_env,(Envmap.insert t_env (id_to_string id,tannot))))
+ | VS_extern_no_rename(typs,id) ->
+ let tannot = typschm_to_tannot envs typs External in
+ (VS_aux(vs,(l,tannot)),
+ Env(d_env,(Envmap.insert t_env (id_to_string id,tannot))))
+ | VS_extern_spec(typs,id,s) ->
+ let tannot = typschm_to_tannot envs typs External in
+ (VS_aux(vs,(l,tannot)),
+ Env(d_env,(Envmap.insert t_env (id_to_string id,tannot))))
+
+let check_default envs (DT_aux(ds,(l,annot))) =
+ let (Env(d_env,t_env)) = envs in
+ match ds with
+ | DT_kind _ -> ((DT_aux(ds,(l,annot))),envs)
+ | DT_typ(typs,id) ->
+ let tannot = typschm_to_tannot envs typs Default in
+ (DT_aux(ds,(l,tannot)),
+ Env(d_env,(Envmap.insert t_env (id_to_string id,tannot))))
+
+(*val check_def : envs -> tannot def -> (tannot def) envs_out*)
+let check_def envs (DEF_aux(def,(l,annot))) =
+ match def with
+ | DEF_type tdef -> let td,envs = check_type_def envs tdef in
+ (DEF_aux((DEF_type td),(l,annot)),envs)
+ | DEF_fundef fdef -> (DEF_aux(def,(l,annot)),envs)
+ | DEF_val letdef -> (DEF_aux(def,(l,annot)),envs)
+ | DEF_spec spec -> let vs,envs = check_val_spec envs spec in
+ (DEF_aux(DEF_spec(vs),(l,annot)),envs)
+ | DEF_default default -> let ds,envs = check_default envs default in
+ (DEF_aux((DEF_default(ds)),(l,annot)),envs)
+ | DEF_reg_dec(typ,id) ->
+ let t = (typ_to_t typ) in
+ let (Env(d_env,t_env)) = envs in
+ let tannot = into_register (Some(([],t),External,[])) in
+ (DEF_aux(def,(l,tannot)),(Env(d_env,Envmap.insert t_env ((id_to_string id),tannot))))
+
+
+(*val check : envs -> tannot defs -> tannot defs*)
+let rec check envs (Defs defs) =
+ match defs with
+ | [] -> (Defs [])
+ | def::defs -> let (def, envs) = check_def envs def in
+ let (Defs defs) = check envs (Defs defs) in
+ (Defs (def::defs))
diff --git a/src/type_check.mli b/src/type_check.mli
index 25992725..9f8b6b33 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -2,8 +2,18 @@ open Ast
open Type_internal
type kind = Type_internal.kind
type typ = Type_internal.t
+type 'a emap = 'a Envmap.t
-type envs = Nameset.t * kind Envmap.t * typ Envmap.t
+type rec_kind = Record | Register
+type def_envs = {
+ k_env: kind emap;
+ abbrevs: tannot emap;
+ namesch : tannot emap;
+ enum_env : (string list) emap;
+ rec_env : (string * rec_kind * ((string * tannot) list)) list;
+ }
+type envs = Env of def_envs * tannot emap
type 'a envs_out = 'a * envs
-val check : Nameset.t -> kind Envmap.t -> typ Envmap.t -> tannot defs -> tannot defs
+
+val check : envs -> tannot defs -> tannot defs
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 445fac7b..2964b8f0 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -62,15 +62,17 @@ type tag =
| External
| Default
| Constructor
+ | Enum
(* Constraints for nexps, plus the location which added the constraint *)
type nexp_range =
| LtEq of Parse_ast.l * nexp * nexp
| Eq of Parse_ast.l * nexp * nexp
| GtEq of Parse_ast.l * nexp * nexp
- | In of Parse_ast.l * nexp * nexp list
+ | In of Parse_ast.l * string * int list
-type tannot = (t * tag * nexp_range list) option
+type t_params = (string * kind) list
+type tannot = ((t_params * t) * tag * nexp_range list) option
let initial_kind_env =
Envmap.from_list [
@@ -84,6 +86,14 @@ let initial_kind_env =
("vector", {k = K_Lam( [ {k = K_Nat}; {k = K_Nat}; {k= K_Ord} ; {k=K_Typ}], {k=K_Typ}) } )
]
+let nat_typ = {t=Tid "nat"}
+let pure = {effect=Eset []}
+let initial_typ_env =
+ Envmap.from_list [
+ ("+",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure)}),External,[]));
+ ]
+
+
let eq_error l msg = raise (Reporting_basic.err_typ l msg)
let compare_effect (BE_aux(e1,_)) (BE_aux(e2,_)) =
@@ -168,9 +178,19 @@ and type_arg_eq l ta1 ta2 =
match ta1,ta2 with
| TA_typ t1,TA_typ t2 -> snd (type_eq l t1 t2)
| TA_nexp n1,TA_nexp n2 -> if nexp_eq n1 n2 then [] else [Eq(l,n1,n2)]
- | TA_eft e1,TA_eft e2 -> (effects_eq l e1 e2;[])
- | TA_ord o1,TA_ord o2 -> (order_eq l o1 o2;[])
+ | TA_eft e1,TA_eft e2 -> (ignore(effects_eq l e1 e2);[])
+ | TA_ord o1,TA_ord o2 -> (ignore(order_eq l o1 o2);[])
| _,_ -> eq_error l "Type arguments must be of the same kind"
-let rec type_coerce l t1 t2 = (t2,[])
+let rec type_coerce l t1 t2 =
+ match t1.t,t2.t with
+ | Tid v1,Tid v2 -> if v1 = v2 then (None,[]) else eq_error l ("Type variables " ^ v1 ^ " and " ^ v2 ^ " do not match and cannot be unified") (*lookup for abbrev*)
+ | Ttup t1s, Ttup t2s ->
+ (None,(List.flatten (List.map snd (List.map2 (type_eq l) t1s t2s))))
+ | Tapp(id1,args1), Tapp(id2,args2) ->
+ if id1=id2 && (List.length args2 = List.length args2) then
+ (None,(List.flatten (List.map2 (type_arg_eq l) args1 args2)))
+ else eq_error l ("Type application of " ^ id1 ^ " and " ^ id2 ^ " must match")
+ | _,_ -> let (t2,consts) = type_eq l t1 t2 in
+ (None,consts)
diff --git a/src/type_internal.mli b/src/type_internal.mli
index dadd4002..e3b9a526 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -58,20 +58,23 @@ type tag =
| External
| Default
| Constructor
+ | Enum
(* Constraints for nexps, plus the location which added the constraint, each nexp is either <= 0 = 0 or >= 0 *)
type nexp_range =
| LtEq of Parse_ast.l * nexp * nexp
| Eq of Parse_ast.l * nexp * nexp
| GtEq of Parse_ast.l * nexp * nexp
- | In of Parse_ast.l * nexp * nexp list
+ | In of Parse_ast.l * string * int list
-type tannot = (t * tag * nexp_range list) option
+type t_params = (string * kind) list
+type tannot = ((t_params * t) * tag * nexp_range list) option
val initial_kind_env : kind Envmap.t
+val initial_typ_env : tannot Envmap.t
(* type_eq mutates to unify variables, and will raise an exception if two types cannot be equal *)
val type_eq : Parse_ast.l -> t -> t -> t * nexp_range list
(* type_eq mutates to unify variables, and will raise an exception if the first type cannot be coerced into the second *)
-val type_coerce : Parse_ast.l -> t -> t -> t * nexp_range list
+val type_coerce : Parse_ast.l -> t -> t -> t option * nexp_range list
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:56:02 +0000