diff options
| author | Kathy Gray | 2014-01-07 15:35:41 +0000 |
|---|---|---|
| committer | Kathy Gray | 2014-01-07 15:35:41 +0000 |
| commit | aedfbef5ccfe39e661cc309d2ee1c96a5f70dc5a (patch) | |
| tree | 0802f8fa5420f2d4f1930cd18e392212b4f22a80 /src | |
| parent | 093550b39e7331179cbdae913021be27f11e4153 (diff) | |
lem homs and type headers
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 |