diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_internal.ml | 52 | ||||
| -rw-r--r-- | src/type_internal.mli | 7 |
2 files changed, 51 insertions, 8 deletions
diff --git a/src/type_internal.ml b/src/type_internal.ml index 2bd0f659..445fac7b 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -22,6 +22,7 @@ and k_aux = type t = { mutable t : t_aux } and t_aux = | Tvar of string + | Tid of string | Tfn of t * t * effect | Ttup of t list | Tapp of string * t_arg list @@ -62,11 +63,11 @@ type tag = | Default | Constructor -(* Constraints for nexps, plus the location which added the constraint, each nexp is either <= 0 = 0 or >= 0 *) +(* Constraints for nexps, plus the location which added the constraint *) type nexp_range = - | LtEq of Parse_ast.l * nexp - | Eq of Parse_ast.l * nexp - | GtEq of Parse_ast.l * nexp + | 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 type tannot = (t * tag * nexp_range list) option @@ -130,5 +131,46 @@ let effects_eq l e1 e2 = | Evar v1, Evar v2 -> if v1 = v2 then e2 else eq_error l ("Effect variables " ^ v1 ^ " and " ^ v2 ^ " do not match and cannot be unified") | Evar v1, Eset _ -> eq_error l ("Effect variable " ^ v1 ^ " cannot be used where a concrete set of effects is specified") -let rec type_eq l t1 t2 = (t2,[]) +(* Is checking for structural equality only, other forms of equality will be handeled by constraints *) +let rec nexp_eq n1 n2 = + match n1.nexp,n2.nexp with + | Nvar v1,Nvar v2 -> v1=v2 + | Nconst n1,Nconst n2 -> n1=n2 + | Nadd(nl1,nl2), Nadd(nr1,nr2) -> nexp_eq nl1 nr1 && nexp_eq nl2 nr2 + | Nmult(nl1,nl2), Nmult(nr1,nr2) -> nexp_eq nl1 nr1 && nexp_eq nl2 nr2 + | N2n n,N2n n2 -> nexp_eq n n2 + | Nneg n,Nneg n2 -> nexp_eq n n2 + | Nuvar _, n -> n1.nexp <- n2.nexp; true + | n,Nuvar _ -> n2.nexp <- n1.nexp; true + | _,_ -> false + +(*Is checking for structural equality amongst the types, building constraints for kind Nat. Note: needs an environment to handle type abbreviations*) +let rec type_eq l t1 t2 = + match t1.t,t2.t with + | Tvar v1,Tvar v2 -> if v1 = v2 then (t2,[]) else eq_error l ("Type variables " ^ v1 ^ " and " ^ v2 ^ " do not match and cannot be unified") + | Tid v1,Tid v2 -> if v1 = v2 then (t2,[]) else eq_error l ("Type variables " ^ v1 ^ " and " ^ v2 ^ " do not match and cannot be unified") (*lookup for abbrev*) + | Tfn(tin1,tout1,effect1),Tfn(tin2,tout2,effect2) -> + let (tin,cin) = type_eq l tin1 tin2 in + let (tout,cout) = type_eq l tout1 tout2 in + let effect = effects_eq l effect1 effect2 in + (t2,cin@cout) + | Ttup t1s, Ttup t2s -> + (t2,(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 + (t2,(List.flatten (List.map2 (type_arg_eq l) args1 args2))) + else eq_error l ("Type application of " ^ id1 ^ " and " ^ id2 ^ " must match") + | Tuvar _, t -> t1.t <- t2.t; (t2,[]) + | t,Tuvar _ -> t2.t <- t1.t; (t2,[]) + | _,_ -> eq_error l ("Type mismatch") + +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;[]) + | _,_ -> eq_error l "Type arguments must be of the same kind" + + let rec type_coerce l t1 t2 = (t2,[]) diff --git a/src/type_internal.mli b/src/type_internal.mli index 2e8c3418..dadd4002 100644 --- a/src/type_internal.mli +++ b/src/type_internal.mli @@ -22,6 +22,7 @@ type o_uvar type t = { mutable t : t_aux } and t_aux = | Tvar of string + | Tid of string | Tfn of t * t * effect | Ttup of t list | Tapp of string * t_arg list @@ -60,9 +61,9 @@ type tag = (* 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 - | Eq of Parse_ast.l * nexp - | GtEq of Parse_ast.l * nexp + | 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 type tannot = (t * tag * nexp_range list) option |