Commit d86015af authored by POTTIER Francois's avatar POTTIER Francois

Removed recursive types [TyMu].

parent 848abd59
......@@ -18,7 +18,6 @@ type TYP =
| TyArrow of TYP * TYP
| TyProduct of TYP * TYP
| TyForall of ('bn, TYP) abs
| TyMu of ('bn, TYP) abs
(* Term variables. *)
......
......@@ -47,52 +47,30 @@ let extend_with_tyvar (env : env) (a : tyvar) : env =
(* Destructors. *)
let unfold ty =
assert (guq_typ ty);
match ty with
| TyMu (a, body) ->
(* No shadowing within [ty] implies [a # ba(body)]. *)
assert (not (Atom.Set.mem a (ba_typ body)));
(* The free names of [ty] are free in [body] too.
Global uniqueness for [body] yields [fa(body) # ba(body)].
Therefore, we have [fa(ty) # ba(body)]. *)
assert (Atom.Set.disjoint (fa_typ ty) (ba_typ body));
(* By the above, the bound names of [body] are disjoint with the
domain and codomain of the substitution [ty/a]. *)
subst_TyVar_typ1 copy_typ ty a body
| _ ->
assert false
exception NotAnArrow of nominal_typ
let rec as_arrow ty : nominal_typ * nominal_typ =
let as_arrow ty : nominal_typ * nominal_typ =
match ty with
| TyArrow (ty1, ty2) ->
ty1, ty2
| TyMu _ ->
as_arrow (unfold ty)
| _ ->
raise (NotAnArrow ty)
exception NotAProduct of nominal_typ
let rec as_product ty : nominal_typ * nominal_typ =
let as_product ty : nominal_typ * nominal_typ =
match ty with
| TyProduct (ty1, ty2) ->
ty1, ty2
| TyMu _ ->
as_product (unfold ty)
| _ ->
raise (NotAProduct ty)
exception NotAForall of nominal_typ
let rec as_forall ty : tyvar * nominal_typ =
let as_forall ty : tyvar * nominal_typ =
match ty with
| TyForall (a, ty) ->
a, ty
| TyMu _ ->
as_forall (unfold ty)
| _ ->
raise (NotAForall ty)
......@@ -100,8 +78,6 @@ let rec as_forall ty : tyvar * nominal_typ =
(* An equality test. *)
(* TEMPORARY should unfold recursive types on the fly *)
exception TypeMismatch of nominal_typ * nominal_typ
let (--) ty1 ty2 =
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment