diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/type_internal.ml | 3 | ||||
| -rw-r--r-- | src/type_internal.mli | 6 |
2 files changed, 9 insertions, 0 deletions
diff --git a/src/type_internal.ml b/src/type_internal.ml index b019624d..bfed90ee 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -81,3 +81,6 @@ let initial_kind_env = ("enum", {k = K_Lam( [ {k = K_Nat}; {k= K_Nat}; {k=K_Ord} ], {k = K_Typ}) }); ("vector", {k = K_Lam( [ {k = K_Nat}; {k = K_Nat}; {k= K_Ord} ; {k=K_Typ}], {k=K_Typ}) } ) ] + +let rec type_eq l t1 t2 = (t2,[]) +let rec type_coerce l t1 t2 = (t2,[]) diff --git a/src/type_internal.mli b/src/type_internal.mli index fedc5cc4..2e8c3418 100644 --- a/src/type_internal.mli +++ b/src/type_internal.mli @@ -68,3 +68,9 @@ type nexp_range = type tannot = (t * tag * nexp_range list) option val initial_kind_env : kind 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 |