diff --git a/demos/system-F-type/F.cppo.ml b/demos/system-F-type/F.cppo.ml
index 14a7da43ac5dae13e895874c795f7dd4dbc6b1ed..62f269d8aa3f42fc92ba901b7dad700406adb1f1 100644
--- a/demos/system-F-type/F.cppo.ml
+++ b/demos/system-F-type/F.cppo.ml
@@ -1,10 +1,14 @@
open AlphaLib
open Abstraction
-#include "AlphaLibMacros.cppo.ml"
(* In this demo, only type variables are handled via AlphaLib. Term variables
are represented as strings. *)
+(* Type variables. *)
+
+type tyvar =
+ Atom.t
+
(* Types. *)
type ('fn, 'bn) typ =
@@ -16,19 +20,19 @@ type ('fn, 'bn) typ =
(* Term variables. *)
-and var = (string[@opaque])
+and tevar = (string[@opaque])
(* Terms. *)
and ('fn, 'bn) term =
- | TeVar of var
- | TeAbs of var * ('fn, 'bn) typ * ('fn, 'bn) term
+ | TeVar of tevar
+ | TeAbs of tevar * ('fn, 'bn) typ * ('fn, 'bn) term
| TeApp of ('fn, 'bn) term * ('fn, 'bn) term
- | TeLet of var * ('fn, 'bn) term * ('fn, 'bn) term
+ | TeLet of tevar * ('fn, 'bn) term * ('fn, 'bn) term
| TeTyAbs of ('bn, ('fn, 'bn) term) abstraction
| TeTyApp of ('fn, 'bn) term * ('fn, 'bn) typ
| TePair of ('fn, 'bn) term * ('fn, 'bn) term
- | Teroj of int * ('fn, 'bn) term
+ | TeProj of int * ('fn, 'bn) term
(* Visitor generation. *)
@@ -51,7 +55,7 @@ and ('fn, 'bn) term =
]
-(* Operations based on visitors. *)
+(* Type abbreviations. *)
type raw_typ =
(string, string) typ
@@ -63,6 +67,10 @@ type raw_term =
type nominal_term =
(Atom.t, Atom.t) term
+(* Operations based on visitors. *)
+
+#include "AlphaLibMacros.cppo.ml"
+
__FA
FA(typ)
FA(term)
diff --git a/demos/system-F-type/FTypeChecker.ml b/demos/system-F-type/FTypeChecker.ml
new file mode 100644
index 0000000000000000000000000000000000000000..1ec0f903e2fe36650f2fa9e1cd6c6791370d13e1
--- /dev/null
+++ b/demos/system-F-type/FTypeChecker.ml
@@ -0,0 +1,148 @@
+open AlphaLib
+open F
+
+(* -------------------------------------------------------------------------- *)
+
+(* Type environments. *)
+
+module TermVar =
+ String
+
+module TermVarMap =
+ Map.Make(TermVar)
+
+type env = {
+ tevars: nominal_typ TermVarMap.t;
+ tyvars: Atom.Set.t
+}
+
+let empty : env =
+ { tevars = TermVarMap.empty; tyvars = Atom.Set.empty }
+
+exception UnboundTermVariable of tevar
+
+let lookup (env : env) (x : tevar) : nominal_typ =
+ try
+ (* The free type variables of this type cannot be captured; see below. *)
+ TermVarMap.find x env.tevars
+ with Not_found ->
+ raise (UnboundTermVariable x)
+
+let extend_with_tevar (env : env) (x : tevar) (ty : nominal_typ) : env =
+ (* We maintain the invariant that the free type variables in the codomain
+ of [env.tevars] form a subset of [env.tyvars]. *)
+ assert (Atom.Set.subset (fa_typ ty) env.tyvars);
+ { env with tevars = TermVarMap.add x ty env.tevars }
+
+let extend_with_tyvar (env : env) (a : tyvar) : env =
+ (* We assume that type variables are globally unique in the term that we are
+ type-checking. Thus, the \Lambda-bound name [a] cannot be in the domain
+ of the environment (i.e., it cannot have been previously bound). Therefore,
+ by the above invariant, it cannot be in the codomain of the environment
+ either. This implies that it is safe to look up a type in the environment. *)
+ assert (not (Atom.Set.mem a env.tyvars));
+ { env with tyvars = Atom.Set.add a env.tyvars }
+
+(* -------------------------------------------------------------------------- *)
+
+(* Destructors. *)
+
+let unfold ty =
+ assert (wf_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.
+ Strong well-formedness 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_typ_typ1 ty a body
+ | _ ->
+ assert false
+
+exception NotAnArrow of nominal_typ
+
+let rec 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 =
+ 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 =
+ match ty with
+ | TyForall (a, ty) ->
+ a, ty
+ | TyMu _ ->
+ as_forall (unfold ty)
+ | _ ->
+ raise (NotAForall ty)
+
+(* -------------------------------------------------------------------------- *)
+
+(* An equality test. *)
+
+(* TEMPORARY should unfold recursive types on the fly *)
+
+exception TypeMismatch of nominal_typ * nominal_typ
+
+let (--) ty1 ty2 =
+ if not (equiv_typ ty1 ty2) then
+ raise (TypeMismatch (ty1, ty2))
+
+(* -------------------------------------------------------------------------- *)
+
+(* The type-checker. *)
+
+let rec typeof env (t : nominal_term) : nominal_typ =
+ match t with
+ | TeVar x ->
+ lookup env x
+ | TeAbs (x, ty1, t) ->
+ let ty2 = typeof (extend_with_tevar env x ty1) t in
+ TyArrow (ty1, ty2)
+ | TeApp (t, u) ->
+ let ty1, ty2 = as_arrow (typeof env t) in
+ typeof env u -- ty1;
+ ty2
+ | TeLet (x, t, u) ->
+ let env = extend_with_tevar env x (typeof env t) in
+ typeof env u
+ | TeTyAbs (a, t) ->
+ TyForall (a, typeof (extend_with_tyvar env a) t)
+ | TeTyApp (t, ty2) ->
+ let a, ty1 = as_forall (typeof env t) in
+ (* We need ba(ty1) # [ty2/a] for this substitution to be safe. *)
+ (* We have ba(ty1) # a because the type a.ty1 is well-formed. Weak uniqueness,
+ also known as no-shadowing, suffices. *)
+ assert (not (Atom.Set.mem a (ba_typ ty1))); (* TEMPORARY problem: ba is too strong *)
+ (* We have ba(ty1) # fa(ty2) because fa(ty2) is a subset of dom(env), that is,
+ env.tyvars, and typeof has the postcondition ba(\result) # env.tyvars. *)
+ subst_typ_typ1 ty2 a ty1
+ | TePair (t1, t2) ->
+ TyProduct (typeof env t1, typeof env t2)
+ | TeProj (i, t) ->
+ assert (i = 1 || i = 2);
+ let ty1, ty2 = as_product (typeof env t) in
+ if i = 1 then ty1 else ty2
+
+let typeof =
+ typeof empty
diff --git a/demos/system-F-type/Main.ml b/demos/system-F-type/Main.ml
index 32bddb0e870fc12c19d14ed419a4abbd793fc25a..5ae0e6dc6304a9a23f45cb00b6b0a836ec1469a8 100644
--- a/demos/system-F-type/Main.ml
+++ b/demos/system-F-type/Main.ml
@@ -1 +1 @@
-module T = F
+module T = FTypeChecker