Skip to content

Instantly share code, notes, and snippets.

@joseanpg
Last active September 8, 2015 13:36
Show Gist options
  • Save joseanpg/ba0d860353e6323970f0 to your computer and use it in GitHub Desktop.
Save joseanpg/ba0d860353e6323970f0 to your computer and use it in GitHub Desktop.
Basic Polymorphic Typechecking ~ Luca Cardelli 1987
(** http://lucacardelli.name/Papers/BasicTypechecking.pdf **)
(** Modula 2 **)
(***************************************************************************)
(**************************** DEFINITION MODULES ***************************)
(***************************************************************************)
(***************************************************************************)
DEFINITION MODULE ErrorMod;
PROCEDURE Msg(msg: ARRAY OF CHAR);
(* Print an error message *)
END ErrorMod.
(***************************************************************************)
DEFINITION MODULE SymbolMod;
TYPE
Ide;
PROCEDURE New(string: ARRAY OF CHAR): Ide;
(* Create a new identifier from a string *)
PROCEDURE Equal(ide1, ide2: Ide): BOOLEAN;
(* Compare two identifiers *)
END SymbolMod.
(***************************************************************************)
DEFINITION MODULE ParseTreeMod;
IMPORT SymbolMod;
FROM SymbolMod IMPORT Ide;
TYPE
Exp = POINTER TO ExpBase;
(* Parse tree for expressions *)
ExpClass = (IdeClass, CondClass, LambClass, ApplClass, BlockClass);
ExpBase = RECORD
CASE class: ExpClass OF
| IdeClass: ide: Ide;
| CondClass: test, ifTrue, ifFalse: Exp;
| LambClass: binder: Ide; body: Exp;
| ApplClass: fun, arg: Exp;
| BlockClass: decl: Decl; scope: Exp;
END;
END;
(* Parse tree for declarations *)
Decl = POINTER TO DeclBase;
DeclClass = (DefClass, SeqClass, RecClass);
DeclBase = RECORD
CASE class: DeclClass OF
| DefClass: binder: Ide; def: Exp;
| SeqClass: first, second: Decl;
| RecClass: rec: Decl;
END;
END;
(* Allocation routines for Exp and Decl *)
PROCEDURE NewIdeExp(ide: Ide): Exp;
PROCEDURE NewCondExp(test, ifTrue, ifFalse: Exp): Exp;
PROCEDURE NewLambExp(binder: Ide; body: Exp): Exp;
PROCEDURE NewApplExp(fun, arg: Exp): Exp;
PROCEDURE NewBlockExp(decl: Decl; scope: Exp): Exp;
PROCEDURE NewDefDecl(binder: Ide; def: Exp): Decl;
PROCEDURE NewSeqDecl(first, second: Decl): Decl;
PROCEDURE NewRecDecl(rec: Decl): Decl;
END ParseTreeMod.
(***************************************************************************)
DEFINITION MODULE TypeMod;
IMPORT SymbolMod;
FROM SymbolMod IMPORT Ide;
TYPE
(* The internal representation of type expressions *)
TypeExp = POINTER TO TypeExpBase;
TypeClass = (VarType, OperType);
TypeExpBase = RECORD
CASE class: TypeClass OF
| VarType: instance: TypeExp;
| OperType: ide: Ide; args: TypeList;
END;
END;
TypeList = POINTER TO TypeListBase;
TypeListBase = RECORD head: TypeExp; tail: TypeList; END;
(* Allocate a new type variable *)
PROCEDURE NewTypeVar(): TypeExp;
(* Allocate a new type operator *)
PROCEDURE NewTypeOper(ide: Ide; args: TypeList): TypeExp;
(* The empty type list *)
VAR
Empty: TypeList;
(* Allocate a new type list *)
PROCEDURE Extend(head: TypeExp; tail: TypeList): TypeList;
(* Compare two types for identity (pointer equality) *)
PROCEDURE SameType(typeExp1, typeExp2: TypeExp): BOOLEAN;
(* Eliminate redundant instantiated variables at the top of "typeExp";
The result of Prune is always a non-instantiated type variable or a
type operator *)
PROCEDURE Prune(typeExp: TypeExp): TypeExp;
(* Whether an uninstantiated type variable occurs in a type expression *)
PROCEDURE OccursInType(typeVar: TypeExp; typeExp: TypeExp): BOOLEAN;
(* Whether an uninstantiated type variable occurs in a list *)
PROCEDURE OccursInTypeList(typeVar: TypeExp; list: TypeList): BOOLEAN;
(* Unify two type expressions *)
PROCEDURE UnifyType(typeExp1, typeExp2: TypeExp);
(* Unify two lists of type expressions *)
PROCEDURE UnifyArgs(list1, list2: TypeList);
END TypeMod.
(***************************************************************************)
DEFINITION MODULE GenericVarMod;
IMPORT TypeMod;
FROM TypeMod IMPORT TypeExp;
TYPE
(* Lists of non-generic type variables and their instantiations *)
NonGenericVars;
VAR
(* The empty list *)
Empty: NonGenericVars;
(* Extend a list *)
PROCEDURE Extend(head: TypeExp; tail: NonGenericVars): NonGenericVars;
(* Whether an uninstantiated type variable is generic w.r.t. a list of
non-generic type variables *)
PROCEDURE IsGeneric(typeVar: TypeExp; list: NonGenericVars): BOOLEAN;
(* Make a copy of a type expression; the generic varibles are copied, while
the non-generic variables are shared *)
PROCEDURE FreshType(typeExp: TypeExp; list: NonGenericVars): TypeExp;
END GenericVarMod.
(***************************************************************************)
DEFINITION MODULE EnvMod;
IMPORT SymbolMod, TypeMod, GenericVarMod;
FROM SymbolMod IMPORT Ide;
FROM TypeMod IMPORT TypeExp;
FROM GenericVarMod IMPORT NonGenericVars;
TYPE
(* Environments associating type expressions to identifiers *)
Env;
VAR
(* The empty environment *)
Empty: Env;
(* Extend an environment with an identifier-type pair *)
PROCEDURE Extend(ide: Ide; typeExp: TypeExp; tail: Env): Env;
(* Search for an identifier in an environment and return a "fresh" copy of
the associated type (using GenericVar.FreshType). The identifier must be
bound in the environment *)
PROCEDURE Retrieve(ide: Ide; env: Env; list: NonGenericVars): TypeExp;
END EnvMod.
(***************************************************************************)
DEFINITION MODULE TypecheckMod;
IMPORT ParseTreeMod, TypeMod, EnvMod, GenericVarMod;
FROM ParseTreeMod IMPORT Exp, Decl;
FROM TypeMod IMPORT TypeExp;
FROM EnvMod IMPORT Env;
FROM GenericVarMod IMPORT NonGenericVars;
(* Typecheck an expression w.r.t. an environment, and return its type *)
PROCEDURE AnalyzeExp(exp: Exp; env: Env; list: NonGenericVars): TypeExp;
(* Typecheck a declaration w.r.t an environment, and return an extended
environment containing the types of the identifiers introduced by the
declaration *)
PROCEDURE AnalyzeDecl(decl: Decl; env: Env; list: NonGenericVars): Env;
END TypecheckMod.
(***************************************************************************)
(************************* IMPLEMENTATION MODULES **************************)
(***************************************************************************)
(***************************************************************************)
IMPLEMENTATION MODULE TypeMod;
IMPORT ErrorMod;
PROCEDURE NewTypeVar(): TypeExp;
VAR r: TypeExp;
BEGIN
NEW(r, VarType); r^.class := VarType; r^.instance := NIL; RETURN r;
END NewTypeVar;
PROCEDURE NewTypeOper(ide: Ide; args: TypeList): TypeExp;
VAR r: TypeExp;
BEGIN
NEW(r, OperType); r^.class := OperType; r^.ide := ide; r^.args := args; RETURN r;
END NewTypeOper;
PROCEDURE Extend(head: TypeExp; tail: TypeList): TypeList;
VAR r: TypeList;
BEGIN
NEW(r); r^.head := head; r^.tail := tail; RETURN r;
END Extend;
PROCEDURE SameType(typeExp1, typeExp2: TypeExp): BOOLEAN;
BEGIN RETURN typeExp1 = typeExp2; END SameType;
PROCEDURE Prune(typeExp: TypeExp): TypeExp;
BEGIN
CASE typeExp^.class OF
| VarType:
IF typeExp^.instance = NIL THEN
RETURN typeExp;
ELSE
typeExp^.instance := Prune(typeExp^.instance);
RETURN typeExp^.instance;
END;
| OperType:
RETURN typeExp;
END;
END Prune;
PROCEDURE OccursInType(typeVar: TypeExp; typeExp: TypeExp): BOOLEAN;
BEGIN
typeExp := Prune(typeExp);
CASE typeExp^.class OF
| VarType: RETURN SameType(typeVar, typeExp);
| OperType: RETURN OccursInTypeList(typeVar, typeExp^.args);
END;
END OccursInType;
PROCEDURE OccursInTypeList(typeVar: TypeExp; list: TypeList): BOOLEAN;
BEGIN
IF list = NIL THEN RETURN FALSE END;
IF OccursInType(typeVar, list^.head) THEN RETURN TRUE END;
RETURN OccursInTypeList(typeVar, list^.tail);
END OccursInTypeList;
PROCEDURE UnifyType(typeExp1, typeExp2: TypeExp);
BEGIN
typeExp1 := Prune(typeExp1);
typeExp2 := Prune(typeExp2);
CASE typeExp1^.class OF
| VarType:
IF OccursInType(typeExp1, typeExp2) THEN
IF NOT SameType(typeExp1, typeExp2) THEN
ErrorMod.Msg("Type clash");
END;
ELSE
typeExp1^.instance := typeExp2;
END;
| OperType:
CASE typeExp2^.class OF
| VarType: UnifyType(typeExp2, typeExp1);
| OperType:
IF SymbolMod.Equal(typeExp1^.ide, typeExp2^.ide) THEN
UnifyArgs(typeExp1^.args, typeExp2^.args);
ELSE
ErrorMod.Msg("Type clash");
END;
END;
END;
END UnifyType;
PROCEDURE UnifyArgs(list1, list2: TypeList);
BEGIN
IF (list1 = Empty) AND (list2 = Empty) THEN RETURN; END;
IF (list1 = Empty) OR (list2 = Empty) THEN
ErrorMod.Msg("Type clash");
ELSE
UnifyType(list1^.head, list2^.head);
UnifyArgs(list1^.tail, list2^.tail);
END;
END UnifyArgs;
BEGIN
Empty := NIL;
END TypeMod.
(***************************************************************************)
IMPLEMENTATION MODULE GenericVarMod;
FROM TypeMod IMPORT TypeClass, TypeList;
TYPE
NonGenericVars = TypeList;
PROCEDURE Extend(head: TypeExp; tail: NonGenericVars): NonGenericVars;
BEGIN RETURN TypeMod.Extend(head, tail); END Extend;
PROCEDURE IsGeneric(typeVar: TypeExp; list: NonGenericVars): BOOLEAN;
BEGIN RETURN NOT TypeMod.OccursInTypeList(typeVar, list); END IsGeneric;
TYPE
CopyEnv = POINTER TO CopyEnvBase;
CopyEnvBase = RECORD old, new: TypeExp; tail: CopyEnv; END;
PROCEDURE ExtendCopyEnv(old, new: TypeExp; tail: CopyEnv): CopyEnv;
VAR r: CopyEnv;
BEGIN
NEW(r); r^.old := old; r^.new := new; r^.tail := tail; RETURN r;
END ExtendCopyEnv;
PROCEDURE FreshVar(typeVar: TypeExp; scan: CopyEnv; VAR env: CopyEnv): TypeExp;
VAR newTypeVar: TypeExp;
BEGIN
IF scan = NIL THEN
newTypeVar := TypeMod.NewTypeVar();
env := ExtendCopyEnv(typeVar, newTypeVar, env);
RETURN newTypeVar;
ELSIF TypeMod.SameType(typeVar, scan^.old) THEN
RETURN scan^.new
ELSE
RETURN FreshVar(typeVar, scan^.tail, (*VAR*) env);
END;
END FreshVar;
PROCEDURE Fresh(typeExp: TypeExp; list: NonGenericVars; VAR env: CopyEnv): TypeExp;
BEGIN
typeExp := TypeMod.Prune(typeExp);
CASE typeExp^.class OF
| VarType:
IF IsGeneric(typeExp, list) THEN
RETURN FreshVar(typeExp, env, (*VAR*) env)
ELSE
RETURN typeExp
END;
| OperType:
RETURN TypeMod.NewTypeOper(typeExp^.ide, FreshList(typeExp^.args, list, (*VAR*) env));
END;
END Fresh;
PROCEDURE FreshList(args: TypeList; list: NonGenericVars; VAR env: CopyEnv): TypeList;
BEGIN
IF args = TypeMod.Empty THEN RETURN TypeMod.Empty END;
RETURN TypeMod.Extend(Fresh(args^.head, list, (*VAR*) env),FreshList(args^.tail, list, (*VAR*) env));
END FreshList;
PROCEDURE FreshType(typeExp: TypeExp; list: NonGenericVars): TypeExp;
VAR env: CopyEnv;
BEGIN env := NIL; RETURN Fresh(typeExp, list, (*VAR*) env); END FreshType;
BEGIN
Empty := TypeMod.Empty;
END GenericVarMod.
(***************************************************************************)
IMPLEMENTATION MODULE EnvMod;
IMPORT ErrorMod;
TYPE
Env = POINTER TO EnvBase;
EnvBase = RECORD ide: Ide; typeExp: TypeExp; tail: Env; END;
PROCEDURE Extend(ide: Ide; typeExp: TypeExp; tail: Env): Env;
VAR r: Env;
BEGIN
NEW(r); r^.ide := ide; r^.typeExp := typeExp; r^.tail := tail; RETURN r;
END Extend;
PROCEDURE Retrieve(ide: Ide; env: Env; list: NonGenericVars): TypeExp;
BEGIN
IF env = EnvMod.Empty THEN
ErrorMod.Msg("Unbound ide");
RETURN NIL;
ELSIF SymbolMod.Equal(ide, env^.ide) THEN
RETURN GenericVarMod.FreshType(env^.typeExp, list);
ELSE
RETURN Retrieve(ide, env^.tail, list);
END;
END Retrieve;
BEGIN
Empty := NIL;
END EnvMod.
(***************************************************************************)
IMPLEMENTATION MODULE TypecheckMod;
IMPORT SymbolMod;
FROM ParseTreeMod IMPORT ExpClass, DeclClass;
FROM TypeMod IMPORT NewTypeVar, NewTypeOper, UnifyType, UnifyArgs;
VAR
BoolType: TypeExp;
PROCEDURE FunType(dom, cod: TypeExp): TypeExp;
BEGIN
RETURN
NewTypeOper(SymbolMod.New("->"),TypeMod.Extend(dom, TypeMod.Extend(cod, TypeMod.Empty)))
END FunType;
PROCEDURE AnalyzeExp(exp: Exp; env: Env; list: NonGenericVars): TypeExp;
VAR
typeOfThen, typeOfElse, typeOfBinder, typeOfBody, typeOfFun, typeOfArg, typeOfRes: TypeExp;
bodyEnv, declEnv: Env;
bodyList: NonGenericVars;
BEGIN
CASE exp^.class OF
| IdeClass: RETURN EnvMod.Retrieve(exp^.ide, env, list);
| CondClass:
UnifyType(AnalyzeExp(exp^.test, env, list), BoolType);
typeOfThen := AnalyzeExp(exp^.ifTrue, env, list);
typeOfElse := AnalyzeExp(exp^.ifFalse, env, list);
UnifyType(typeOfThen, typeOfElse);
RETURN typeOfThen;
| LambClass:
typeOfBinder := NewTypeVar();
bodyEnv := EnvMod.Extend(exp^.binder, typeOfBinder, env);
bodyList := GenericVarMod.Extend(typeOfBinder, list);
typeOfBody := AnalyzeExp(exp^.body, bodyEnv, bodyList);
RETURN FunType(typeOfBinder, typeOfBody);
| ApplClass:
typeOfFun := AnalyzeExp(exp^.fun, env, list);
typeOfArg := AnalyzeExp(exp^.arg, env, list);
typeOfRes := NewTypeVar();
UnifyType(typeOfFun, FunType(typeOfArg, typeOfRes));
RETURN typeOfRes;
| BlockClass:
declEnv := AnalyzeDecl(exp^.decl, env, list);
RETURN AnalyzeExp(exp^.scope, declEnv, list);
END;
END AnalyzeExp;
PROCEDURE AnalyzeDecl(decl: Decl; env: Env; list: NonGenericVars): Env;
BEGIN
CASE decl^.class OF
| DefClass:
RETURN EnvMod.Extend(decl^.binder, AnalyzeExp(decl^.def, env, list), env);
| SeqClass:
RETURN AnalyzeDecl(decl^.second, AnalyzeDecl(decl^.first, env, list), list);
| RecClass:
AnalyzeRecDeclBind(decl^.rec, (*VAR*) env, (*VAR*) list);
AnalyzeRecDecl(decl^.rec, env, list);
RETURN env;
END;
END AnalyzeDecl;
PROCEDURE AnalyzeRecDeclBind(decl: Decl; VAR env: Env; VAR list: NonGenericVars);
VAR newTypeVar: TypeExp;
BEGIN
CASE decl^.class OF
| DefClass:
newTypeVar := NewTypeVar();
env := EnvMod.Extend(decl^.binder, newTypeVar, env);
list := GenericVarMod.Extend(newTypeVar, list);
| SeqClass:
AnalyzeRecDeclBind(decl^.first, (*VAR) env, (*VAR*) list);
AnalyzeRecDeclBind(decl^.second, (*VAR) env, (*VAR*) list);
| RecClass: AnalyzeRecDeclBind(decl^.rec, (*VAR) env, (*VAR*) list);
END;
END AnalyzeRecDeclBind;
PROCEDURE AnalyzeRecDecl(decl: Decl; env: Env; list: NonGenericVars);
BEGIN
CASE decl^.class OF
| DefClass:
UnifyType(EnvMod.Retrieve(decl^.binder, env, list),
AnalyzeExp(decl^.def, env, list));
| SeqClass:
AnalyzeRecDecl(decl^.first, env, list);
AnalyzeRecDecl(decl^.second, env, list);
| RecClass: AnalyzeRecDecl(decl^.rec, env, list);
END;
END AnalyzeRecDecl;
BEGIN
BoolType := NewTypeOper(SymbolMod.New("bool"), TypeMod.Empty);
END TypecheckMod.
-- http://lucacardelli.name/Papers/BasicTypechecking.pdf
msg :: String -> IO ()
newtype Ide = Ide String
equal :: Ide -> Ide -> Bool
data Exp = ExpIde { ide :: Ide }
| ExpCond { test :: Exp, ifTrue :: Exp, ifFalse :: Exp }
| ExpLamb { binder :: Ide, body :: Exp }
| ExpAppl { fun :: Exp, arg :: Exp }
data Decl = DeclDef { binder :: Ide, def :: Exp }
| DeclSeq { firt :: Decl, second :: Decl }
| DeclRec { rec :: Decl }
data TypeExp = VarType { instance :: Ref (Maybe TypeExp) }
| OperType { ide :: Ide, args :: [TypeExp] }
sameType :: TypeExp -> TypeExp -> BOOLEAN
sameType typeExp1 typeExp2 = typeExp1 == typeExp2
-- Eliminate redundant instantiated variables at the top of "typeExp"
-- The result of Prune is always a non-instantiated type variable or a type operator
-- !!!!!!!!!!!!!!!!!!!!!!!
prune :: TypeExp -> TypeExp
prune typeExp = case typeExp of
OperType _ _ -> typeExp
VarType instance -> case ^instance of
Nothing -> typeExp
Just typeExp' -> do typeExp.instance := prune typeExp'
typeExp
-- Whether an uninstantiated type variable occurs in a type expression
occursInType :: TypeExp -> TypeExp -> BOOLEAN
-- TypeVar
occursInType typeVar typeExp =
-- warning: prune mutator
case prune typeExp of
VarType _ -> sameType typeVar typeExp
OperType _ args -> occursInTypeList typeVar args
-- Whether an uninstantiated type variable occurs in a list
occursInTypeList :: TypeExp -> [TypeExp] -> BOOLEAN;
-- TypeVar
occursInTypeList typeVar typeList = case typeList of
[] -> False
t:ts | occursInType typeVar t -> True
| otherwise -> occursInTypeList typeVar ts
-- Unify two type expressions
unifyType :: TypeExp -> TypeExp -> ()
unifyType typeExp1 typeExp2 =
typeExp1 := prune typeExp1 !!!!!!!!!!!!!!
typeExp2 := prune typeExp2 !!!!!!!!!!!!!!
case typeExp1 of
VarType _ -> if occursInType typeExp1 typeExp2
then if not (sameType typeExp1 typeExp2)
then msg "Type clash"
else !!!!!!!!!!!!!!!
else typeExp1.instance := typeExp2
OperType ide1 args1 -> case typeExp2 of
VarType _ -> unifyType typeExp2 typeExp1
OperType ide2 args2 -> if ide1 == ide2
then unifyArgs args1 args2
else msg "Type clash"
-- Unify two lists of type expressions
unifyArgs :: [TypeExp] -> [TypeExp] -> IO ();
unifyArgs [] [] = return ()
unifyArgs [] _ = msg "Type clash"
unifyArgs _ [] = msg "Type clash"
unifyArgs (x:xs) (y:ys) = do unifyType x y
unifyArgs xs ys
-- Lists of non-generic type variables and their instantiations
newtype NonGenericVars = NonGenericVars [TypeExp]
-- [TypeVar]
-- Whether an uninstantiated type variable is generic w.r.t. a list of non-generic type variables
isGeneric :: TypeExp -> NonGenericVars -> BOOLEAN
-- TypeVar
isGeneric typeVar nonGenericVars = not (occursInTypeList typeVar list)
-- Environments associating type expressions to identifiers *)
newtype Env = Env [(Ide, TypeExp)]
-- The empty environment
empty = Env []
-- Extend an environment with an identifier-type pair
extend :: Ide -> TypeExp -> Env -> Env
-- Search for an identifier in an environment and
-- return a "fresh" copy of the associated type (using GenericVar.FreshType).
-- The identifier must be bound in the environment
retrieve :: Ide -> Env -> NonGenericVars -> Maybe TypeExp
retrieve ide env nonGenericVars = case env of
[] -> msg "Unbound ide"
return Nothing
(i,typeExp):env' | equal ide i -> freshType typeExp nonGenericVars
| otherwise -> retrieve ide env' nonGenericVars
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
newtype CopyEnv = CopyEnv [(TypeExp, TypeExp)]
-- old new
extendCopyEnv old new (CopyEnv list) = CopyEnv ((old,new):list)
freshVar :: TypeExp -> CopyEnv -> Ref CopyEnv -> TypeExp
-- TypeVar
freshVar typeVar scan env =
let newTypeVar :: Ref TypeExp
case scan of
CopyEnv [] -> newTypeVar := TypeVar ?
env := extendCopyEnv typeVar newTypeVar env
return newTypeVar
CopyEnv ((old:new):xs) | sameType typeVar, scan^.old) -> new
| otherwise -> freshVar typeVar (CopyEnv xs) {-VAR-} env
fresh :: TypeExp -> NonGenericVars -> Ref CopyEnv -> TypeExp
fresh typeExp nonGenericVars env =
typeExp := prune typeExp !!!!!!!!
case typeExp of
OperType ide args -> TypeOper ide ( FreshList args list {-VAR-} env )
VarType | isGeneric(typeExp, list) -> freshVar typeExp env {-VAR-} env
| otherwise -> typeExp
freshList :: TypeList -> NonGenericVars -> Ref CopyEnv -> TypeList
freshList args nonGenericVars envCopyEnv
case args of
[] -> []
(a:as) -> ( fresh a nonGenericVars {-VAR-} env ) : (freshList as nonGenericVars {-VAR-} env));
-- Make a copy of a type expression; the generic varibles are copied, while the non-generic variables are shared
freshType :: TypeExp -> NonGenericVars -> TypeExp
freshType typeExp nonGenericVars =
let env:: CopyEnv
env = NIL
in fresh typeExp nonGenericVars (*VAR*) env
Empty := TypeMod.Empty;
----------------------------------------------------------
BoolType :: TypeExp;
BoolType = TypeOper (Ide "bool") []
funType :: TypeExp -> TypeExp -> TypeExp
funType dom cod = TypeOper (Ide "->") [dom, cod]
-- Typecheck an expression w.r.t. an environment, and return its type
analyzeExp :: Exp -> Env -> NonGenericVars -> TypeExp
analyzeExp exp env nonGenericVars =
case exp of
ExpIde Ide -> retrieve ide env nonGenericVars
ExpCond test ifTrue ifFalse -> do unifyType (AnalyzeExp test env nonGenericVars) BoolType
let typeOfThen = analyzeExp ifTrue env nonGenericVars
typeOfElse = analyzeExp ifFalse env nonGenericVars
unifyType typeOfThen typeOfElse
return typeOfThen
ExpLamb binder body -> let typeOfBinder := NewTypeVar ?
bodyEnv := (binder:typeOfBinder):env
bodyNonGenericVars := typeOfBinder: nonGenericVars
typeOfBody := snalyzeExp body bodyEnv bodyNonGenericVars
return funType typeOfBinder typeOfBody
ExpAppl fun arg -> let typeOfFun := analyzeExp fun env nonGenericVars
typeOfArg := analyzeExp arg env nonGenericVars
typeOfRes := TypeVar ?
unifyType typeOfFun (funType typeOfArg typeOfRes)
return typeOfRes;
ExpBlock declEnv := analyzeDecl decl env nonGenericVars
RETURN analyzeExp scope declEnv nonGenericVars
-- Typecheck a declaration w.r.t an environment, and return an extended
-- environment containing the types of the identifiers introduced by the declaration
analyzeDecl :: Decl -> Env -> NonGenericVars -> Env
analyzeDecl decl env nonGenericVars =
case decl of
DefClass binder def -> (binder, analyzeExp def env nonGenericVars): env
SeqClass first second -> analyzeDecl second (analyzeDecl first env nonGenericVars) nonGenericVars
RecClass rec -> analyzeRecDeclBind rec {-VAR-} env {-VAR-} nonGenericVars
analyzeRecDecl rec env nonGenericVars
return env
analyzeRecDeclBind :: Decl -> Ref Env -> Ref NonGenericVars
analyzeRecDeclBind decl env nonGenericVars
case decl of
| DefClass binder def -> let newTypeVar := TypeVar ?
env := (binder, newTypeVar): env
nonGenericVars := newTypeVar : nonGenericVars
| SeqClass first second -> analyzeRecDeclBind first {-VAR-} env {-VAR-} nonGenericVars
analyzeRecDeclBind second {-VAR-} env {-VAR-} nonGenericVars
| RecClass rec -> analyzeRecDeclBind rec {-VAR-} env {-VAR-} nonGenericVars
analyzeRecDecl :: Decl -> Env -> NonGenericVars
analyzeRecDecl decl env nonGenericVars =
case decl of
DefClass binder def -> unifyType (retrieve binder env nonGenericVars) (analyzeExp def env nonGenericVars)
SeqClass first second -> analyzeRecDecl first env, nonGenericVars
analyzeRecDecl second env nonGenericVars
RecClass rec -> analyzeRecDecl rec env nonGenericVars
-- 1
TYPE
Env = POINTER TO EnvBase;
EnvBase = RECORD ide: Ide; typeExp: TypeExp; tail: Env; END;
-- 2
TYPE
Env = POINTER TO RECORD ide: Ide; typeExp: TypeExp; tail: Env; END;
-- 3
data Env = Env { ide :: Ide, typeExp :: TypeExp,tail :: Env }
-----------------------------
-- 1
TypeExp = POINTER TO TypeExpBase;
TypeClass = (VarType, OperType);
TypeExpBase = RECORD
CASE class: TypeClass OF
| VarType: instance: TypeExp;
| OperType: ide: Ide; args: TypeList;
END;
END;
-- 2
TypeExp = POINTER TO TypeExpBase;
TypeExpBase = RECORD
CASE class: (VarType, OperType) OF
| VarType: instance: TypeExp;
| OperType: ide: Ide; args: TypeList;
END;
END;
-- 3
TypeExp = POINTER TO RECORD
CASE class: (VarType, OperType) OF
| VarType: instance: TypeExp;
| OperType: ide: Ide; args: TypeList;
END;
END;
-- 4
data TypeExp = VarType { instance :: TypeExp }
| OperType { ide :: Ide, args :: TypeList }
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment