Skip to content

Mark Cohen / thesis

Go to a project
Commit 69fcaaf7 by Mark Cohen
Options

Greatly simplified language to match more closely with Wadler paper

parent 65cafe35
Inline Side-by-side
Showing with 344 additions and 528 deletions
LUCA-2/annotate.sml
structure Annotate: sig
datatype aterm
= AInt of int * Ty.ty
= AUnit of Ty.ty
| AVar of string * Ty.ty
| ATrue of Ty.ty
| AFalse of Ty.ty
| AString of string * Ty.ty
| AUnit of Ty.ty
| AIf of aterm * aterm * aterm * Ty.ty
| AZero of Ty.ty
| ASucc of aterm * Ty.ty
| APred of aterm * Ty.ty
| ANil of Ty.ty
| ACons of aterm * aterm * Ty.ty
| AList of aterm list * Ty.ty
| APair of aterm * aterm * Ty.ty
| ALeft of aterm * Ty.ty * Ty.ty
| ARight of Ty.ty * aterm * Ty.ty
| AIf of aterm * aterm * aterm * Ty.ty
| ACase of aterm * string * Ty.ty * aterm * string * Ty.ty * aterm * Ty.ty
| ANone of Ty.ty
| ASome of aterm * Ty.ty
| ACase of aterm * string * Ty.ty * aterm * aterm * Ty.ty
| AFun of string * aterm * Ty.ty
| AAbs of string * aterm * Ty.ty
| AApp of aterm * aterm * Ty.ty
| AVar of string * Ty.ty
| ALet of (string * Ty.ty * aterm) list * aterm * Ty.ty
| ALet of string * Ty.ty * aterm * aterm * Ty.ty
val getTy: aterm -> Ty.ty Attempt.attempt
val annotate: AST.term -> aterm Attempt.attempt
......@@ -40,120 +45,121 @@ end = struct
infix <+>
datatype aterm
= AInt of int * Ty.ty
= AUnit of Ty.ty
| AVar of string * Ty.ty
| ATrue of Ty.ty
| AFalse of Ty.ty
| AString of string * Ty.ty
| AUnit of Ty.ty
| AIf of aterm * aterm * aterm * Ty.ty
| AZero of Ty.ty
| ASucc of aterm * Ty.ty
| APred of aterm * Ty.ty
| ANil of Ty.ty
| ACons of aterm * aterm * Ty.ty
| AList of aterm list * Ty.ty
| APair of aterm * aterm * Ty.ty
| ALeft of aterm * Ty.ty * Ty.ty
| ARight of Ty.ty * aterm * Ty.ty
| AIf of aterm * aterm * aterm * Ty.ty
| ACase of aterm * string * Ty.ty * aterm * string * Ty.ty * aterm * Ty.ty
| ANone of Ty.ty
| ASome of aterm * Ty.ty
| ACase of aterm * string * Ty.ty * aterm * aterm * Ty.ty
| AFun of string * aterm * Ty.ty
| AAbs of string * aterm * Ty.ty
| AApp of aterm * aterm * Ty.ty
| AVar of string * Ty.ty
| ALet of (string * Ty.ty * aterm) list * aterm * Ty.ty
| ALet of string * Ty.ty * aterm * aterm * Ty.ty
fun getTy (AUnit ty) = pure ty
| getTy (AVar (_, ty)) = pure ty
fun getTy (AInt (_, ty)) = pure ty
| getTy (ATrue ty) = pure ty
| getTy (AFalse ty) = pure ty
| getTy (AString (_, ty)) = pure ty
| getTy (AUnit ty) = pure ty
| getTy (AIf (_, _, _, ty)) = pure ty
| getTy (AZero ty) = pure ty
| getTy (ASucc (_, ty)) = pure ty
| getTy (APred (_, ty)) = pure ty
| getTy (ANil ty) = pure ty
| getTy (ACons (_, _, ty)) = pure ty
| getTy (AList (_, ty)) = pure ty
| getTy (APair (_, _, ty)) = pure ty
| getTy (ALeft (_, _, ty)) = pure ty
| getTy (ARight (_, _, ty)) = pure ty
| getTy (AIf (_, _, _, ty)) = pure ty
| getTy (ACase (_, _, _, _, _, _, _, ty)) = pure ty
| getTy (ANone ty) = pure ty
| getTy (ASome (_, ty)) = pure ty
| getTy (ACase (_, _, _, _, _, ty)) = pure ty
| getTy (AFun (_, _, ty)) = pure ty
| getTy (AAbs (_, _, ty)) = pure ty
| getTy (AApp (_, _, ty)) = pure ty
| getTy (AVar (_, ty)) = pure ty
| getTy (ALet (_, _, ty)) = pure ty
| getTy (ALet (_, _, _, _, ty)) = pure ty
local open Ty in
fun annotate' g (AST.Int x) = pure (AInt (x, Int))
| annotate' g AST.True = pure (ATrue Bool)
| annotate' g AST.False = pure (AFalse Bool)
| annotate' g (AST.String s) = pure (AString (s, String))
| annotate' g AST.Unit = pure (AUnit Unit)
fun annotate' g AST.Unit = pure (AUnit Ty.Unit)
| annotate' g (AST.Var x) =
TyEnv.lookup g x >>= (fn ty =>
pure (AVar (x, ty)))
| annotate' g (AST.List es) =
mapM (annotate' g) es >>= (fn aes =>
pure (AList (aes, List (freshTyVar ()))))
| annotate' g (AST.Pair (e1, e2)) =
| annotate' g AST.True = pure (ATrue Ty.Bool)
| annotate' g AST.False = pure (AFalse Ty.Bool)
| annotate' g (AST.If (e1, e2, e3)) =
annotate' g e1 >>= (fn ae1 =>
annotate' g e2 >>= (fn ae2 =>
pure (APair (ae1, ae2, Pair (freshTyVar (), freshTyVar ())))))
| annotate' g (AST.Left e) =
annotate' g e3 >>= (fn ae3 =>
pure (AIf (ae1, ae2, ae3, Ty.freshTyVar ())))))
| annotate' g AST.Zero = pure (AZero Ty.Int)
| annotate' g (AST.Succ e) =
annotate' g e >>= (fn ae =>
pure (ALeft (ae, freshTyVar (), Ty.Sum (freshTyVar (), freshTyVar ()))))
| annotate' g (AST.Right e) =
pure (ASucc (ae, Ty.Int)))
| annotate' g (AST.Pred e) =
annotate' g e >>= (fn ae =>
pure (ARight (freshTyVar (), ae, Ty.Sum (freshTyVar (), freshTyVar ()))))
pure (APred (ae, Ty.Int)))
| annotate' g (AST.If (e1, e2, e3)) =
| annotate' g AST.Nil = pure (ANil (Ty.List (Ty.freshTyVar ())))
| annotate' g (AST.Cons (e1, e2)) =
annotate' g e1 >>= (fn ae1 =>
annotate' g e2 >>= (fn ae2 =>
annotate' g e3 >>= (fn ae3 =>
pure (AIf (ae1, ae2, ae3, freshTyVar ())))))
| annotate' g (AST.Case (e1, x2, e2, x3, e3)) =
pure (ACons (ae1, ae2, Ty.List (Ty.freshTyVar ())))))
| annotate' g (AST.Pair (e1, e2)) =
annotate' g e1 >>= (fn ae1 =>
annotate' g e2 >>= (fn ae2 =>
pure (APair (ae1, ae2, Ty.Pair (Ty.freshTyVar (), Ty.freshTyVar ())))))
| annotate' g AST.None = pure (ANone (Ty.Option (Ty.freshTyVar ())))
| annotate' g (AST.Some e) =
annotate' g e >>= (fn ae =>
pure (ASome (ae, Ty.Option (Ty.freshTyVar ()))))
| annotate' g (AST.Case (e1, x, e2, e3)) =
let
val ty2 = freshTyVar ()
val ty3 = freshTyVar ()
val xTy = Ty.freshTyVar ()
in
annotate' g e1 >>= (fn ae1 =>
annotate' (g <+> (x2, ty2)) e2 >>= (fn ae2 =>
annotate' (g <+> (x3, ty3)) e3 >>= (fn ae3 =>
pure (ACase (ae1, x2, ty2, ae2, x3, ty3, ae3, freshTyVar ())))))
annotate' g e1 >>= (fn ae1 =>
annotate' (g <+> (x, xTy)) e2 >>= (fn ae2 =>
annotate' g e3 >>= (fn ae3 =>
pure (ACase (ae1, x, xTy, ae2, ae3, Ty.freshTyVar ())))))
end
| annotate' g (AST.Fun (arg, e)) =
| annotate' g (AST.Abs (arg, e)) =
let
val argTy = freshTyVar ()
val argTy = Ty.freshTyVar ()
in
annotate' (g <+> (arg, argTy)) e >>= (fn ae =>
getTy ae >>= (fn retTy =>
pure (AFun (arg, ae, Ty.Fun (argTy, retTy)))))
pure (AAbs (arg, ae, Ty.Fun (argTy, retTy)))))
end
| annotate' g (AST.App (f, arg)) =
annotate' g f >>= (fn af =>
annotate' g arg >>= (fn aarg =>
pure (AApp (af, aarg, freshTyVar ()))))
| annotate' g (AST.Var x) =
TyEnv.lookup g x >>= (fn ty =>
pure (AVar (x, ty)))
| annotate' g (AST.Let (ds, e)) =
(* make a first pass to give everything a type *)
forM ds (fn (x', mTy, e') =>
case mTy
of SOME ty' => pure (x', ty', e')
| NONE => pure (x', freshTyVar (), e')) >>= (fn dsBinds' =>
(* format the first pass as a TyEnv *)
forM dsBinds' (fn (x', ty', _) => pure (x', ty')) >>= (fn dsBinds =>
(* annotate' all the bindings *)
forM dsBinds' (fn (x', ty', e') =>
annotate' (dsBinds @ g) e' >>= (fn ae' =>
pure (x', ty', ae'))) >>= (fn ads =>
(* finally, annotate' the in-expression *)
annotate' (dsBinds @ g) e >>= (fn ae =>
getTy ae >>= (fn aeTy =>
pure (ALet (ads, ae, aeTy)))))))
end
pure (AApp (af, aarg, Ty.freshTyVar ()))))
| annotate' g (AST.Let (x, NONE, e', e)) =
annotate' g (AST.Let (x, SOME (Ty.freshTyVar ()), e', e))
| annotate' g (AST.Let (x, SOME ty, e', e)) =
annotate' (g <+> (x, ty)) e' >>= (fn ae' =>
annotate' (g <+> (x, ty)) e >>= (fn ae =>
pure (ALet (x, ty, ae', ae, Ty.freshTyVar ()))))
val annotate = annotate' []
......
LUCA-2/ast.sml
structure AST: sig
datatype term
= Int of int
= Unit
| Var of string
| True
| False
| String of string
| Unit
| If of term * term * term
| Zero
| Succ of term
| Pred of term
| Nil
| Cons of term * term
| List of term list
| Pair of term * term
| Left of term
| Right of term
| If of term * term * term
| Case of term * string * term * string * term
| None
| Some of term
| Case of term * string * term * term
| Fun of string * term
| Abs of string * term
| App of term * term
| Var of string
| Let of (string * Ty.ty option * term) list * term
| Let of string * Ty.ty option * term * term
val isValue: term -> bool
......@@ -28,73 +33,91 @@ structure AST: sig
end = struct
datatype term
= Int of int
= Unit
| Var of string
| True
| False
| String of string
| Unit
| If of term * term * term
| Zero
| Succ of term
| Pred of term
| Nil
| Cons of term * term
| List of term list
| Pair of term * term
| Left of term
| Right of term
| If of term * term * term
| Case of term * string * term * string * term
| None
| Some of term
| Case of term * string * term * term
| Fun of string * term
| Abs of string * term
| App of term * term
| Var of string
| Let of (string * Ty.ty option * term) list * term
| Let of string * Ty.ty option * term * term
fun isValue (Int _) = true
| isValue True = true
| isValue False = true
| isValue (String _) = true
| isValue Unit = true
fun isValue Unit = true
| isValue (List ts) = Utils.andmap isValue ts
| isValue (Left t) = isValue t
| isValue (Right t) = isValue t
| isValue (True | False) = true
| isValue (Fun _) = true
| isValue Zero = true
| isValue (Succ e) = isValue e
| isValue (Pred _) = false
| isValue Nil = true
| isValue (Cons (e1, e2)) = isValue e1 andalso isValue e2
| isValue (Pair (e1, e2)) = isValue e1 andalso isValue e2
| isValue None = true
| isValue (Some e) = isValue e
| isValue (Abs (_, _)) = true
| isValue _ = false
fun fromPeano Zero = 0
| fromPeano (Succ e) = (fromPeano e) + 1
| fromPeano (Pred e) = (fromPeano e) - 1
| fromPeano _ = raise Fail "cannot convert non-numeric term"
local open Utils in
fun unparse (Int x) = Int.toString x
fun unparse Unit = "()"
| unparse (Var x) = x
| unparse True = "true"
| unparse False = "false"
| unparse (String s) = "\"" ^ s ^ "\""
| unparse Unit = "()"
| unparse (List ts) = (brc (cat (between (map unparse ts) ", ")))
| unparse (Pair (ty1, ty2)) = (paren o cat) [unparse ty1, ", ", unparse ty2]
| unparse (Left e) = spc ["inl", unparse e]
| unparse (Right e) = spc ["inl", unparse e]
| unparse (If (e1, e2, e3)) =
spc ["if", (unparse e1), "then", (unparse e2), "else", (unparse e3)]
| unparse (Case (x, y, z, u, v)) = spc [
"case", unparse x,
"of", spc ["Left", y], "=>", unparse z,
"|", spc ["Right", u], "=>", unparse v
| unparse (e as (Zero | (Succ _) | (Pred _))) = (Int.toString o fromPeano) e
| unparse Nil = "[]"
| unparse (Cons (e1, e2)) = spc [unparse e1, "::", unparse e2]
| unparse (Pair (e1, e2)) = paren ((cat o between [unparse e1, unparse e2]) ", ")
| unparse None = "None"
| unparse (Some e) = spc ["Some", unparse e]
| unparse (Case (e1, x, e2, e3)) = spc [
"case", unparse e1,
"of", spc ["Some", x], "=>", unparse e2,
"|", "None", "=>", unparse e3
]
| unparse (Fun (x, e)) =
spc [cat ["fun", (paren x)], (unparse e)]
| unparse (App (f, arg)) =
(case f
of (Var f') => cat [f', ((paren o unparse) arg)]
| _ => cat [((paren o unparse) f), ((paren o unparse) arg)])
| unparse (Var s) = s
| unparse (Let (decs, e)) =
spc (("let" ::
(map (fn (x, _, e') => spc [x, "=", (unparse e')]) decs)) @
["in", (unparse e)])
end
| unparse (Abs (x, e)) =
spc ["fn", x, "=>", unparse e]
| unparse (App ((Var f), arg)) = spc [f, unparse arg]
| unparse (App (e, arg)) = spc [(paren o unparse) e, unparse arg]
| unparse (Let (x, (SOME ty), e', e)) =
spc ["let", x, ":", Ty.unty ty, "=", unparse e', "in", unparse e]
| unparse (Let (x, NONE, e', e)) =
spc ["let", x, "=", unparse e', "in", unparse e]
end
end
LUCA-2/collect.sml
......@@ -14,61 +14,54 @@ end = struct
infixr 1 =<< >=> <=<
infix 4 <$> <*>
open Ty
val <+> = TyEnv.<+>
infix <+>
local open Ty in local open Annotate in
fun collect' [] cs = pure cs
| collect' (Annotate.AList (axs, List ty) :: aes) cs =
forM axs (fn ax =>
Annotate.getTy ax >>= (fn xTy =>
pure (xTy, ty))) >>= (fn cs' =>
collect' (axs @ aes) (cs' @ cs))
| collect' (Annotate.AList (_, _) :: _) _ =
Failure "received an annotated list that didn't have a list type"
| collect' (Annotate.APair (ae1, ae2, ty) :: aes) cs =
Annotate.getTy ae1 >>= (fn ae1Ty =>
Annotate.getTy ae2 >>= (fn ae2Ty =>
collect' (ae1 :: ae2 :: aes) ((Pair (ae1Ty, ae2Ty), ty) :: cs)))
| collect' (Annotate.ALeft (ae1, ty2, ty) :: aes) cs =
Annotate.getTy ae1 >>= (fn ae1Ty =>
collect' (ae1 :: aes) ((Sum (ae1Ty, ty2), ty) :: cs))
| collect' (Annotate.ARight (ty1, ae2, ty) :: aes) cs =
Annotate.getTy ae2 >>= (fn ae2Ty =>
collect' (ae2 :: aes) ((Sum (ty1, ae2Ty), ty) :: cs))
| collect' (Annotate.AIf (ae1, ae2, ae3, ty) :: aes) cs =
Annotate.getTy ae1 >>= (fn ae1Ty =>
Annotate.getTy ae2 >>= (fn ae2Ty =>
Annotate.getTy ae3 >>= (fn ae3Ty =>
| collect' (AIf (ae1, ae2, ae3, ty) :: aes) cs =
getTy ae1 >>= (fn ae1Ty =>
getTy ae2 >>= (fn ae2Ty =>
getTy ae3 >>= (fn ae3Ty =>
collect' (ae1 :: ae2 :: ae3 :: aes)
((ae1Ty, Bool) :: (ae2Ty, ae3Ty) :: (ae2Ty, ty) :: cs))))
| collect' (Annotate.ACase (ae1, _, ty2, ae2, _, ty3, ae3, ty) :: aes) cs =
Annotate.getTy ae1 >>= (fn ae1Ty =>
Annotate.getTy ae2 >>= (fn ae2Ty =>
Annotate.getTy ae3 >>= (fn ae3Ty =>
collect' (ae1 :: ae2 :: ae3 :: aes)
((ae1Ty, Sum (ty2, ty3)) ::
(ae2Ty, ae3Ty) :: (ae2Ty, ty) :: cs))))
| collect' (Annotate.AFun (_, ae, _) :: aes) cs = collect' (ae :: aes) cs
| collect' (Annotate.AApp (f, arg, ty) :: aes) cs =
Annotate.getTy f >>= (fn fTy =>
Annotate.getTy arg >>= (fn argTy =>
collect' (f :: arg :: aes) ((fTy, Fun (argTy, ty)) :: cs)))
| collect' (ACons (hd, tl, List ty) :: aes) cs =
getTy hd >>= (fn hdTy =>
getTy tl >>= (fn tlTy =>
collect' (hd :: tl :: aes) ((hdTy, ty) :: (tlTy, List ty) :: cs)))
| collect' (ACons (_, _, _) :: _) _ =
Failure "received an annotated cons that didn't have a list type"
| collect' (Annotate.ALet (ads, ae, ty) :: aes) cs =
forM ads (fn (_, _, ae') => pure ae') >>= (fn ae's =>
| collect' (APair (ae1, ae2, ty) :: aes) cs =
getTy ae1 >>= (fn ae1Ty =>
getTy ae2 >>= (fn ae2Ty =>
collect' (ae1 :: ae2 :: aes) ((ty, Pair (ae1Ty, ae2Ty)) :: cs)))
forM ads (fn (_, ty, ae') =>
Annotate.getTy ae' >>= (fn ae'Ty =>
pure (ty, ae'Ty))) >>= (fn dcs =>
| collect' (ASome (ae, ty) :: aes) cs =
getTy ae >>= (fn aeTy =>
collect' (ae :: aes) ((ty, Option aeTy) :: cs))
| collect' (ACase (ae1, _, ty2, ae2, ae3, ty) :: aes) cs =
getTy ae1 >>= (fn ae1Ty =>
getTy ae2 >>= (fn ae2Ty =>
getTy ae3 >>= (fn ae3Ty =>
collect' (ae1 :: ae2 :: ae3 :: aes)
((ae1Ty, Option ty2) :: (ae2Ty, ae3Ty) :: (ae2Ty, ty) :: cs))))
| collect' (AAbs (_, ae, _) :: aes) cs = collect' (ae :: aes) cs
| collect' (AApp (f, arg, ty) :: aes) cs =
getTy f >>= (fn fTy =>
getTy arg >>= (fn argTy =>
collect' (f :: arg :: aes) ((fTy, Fun (argTy, ty)) :: cs)))
Annotate.getTy ae >>= (fn aeTy =>
collect' (ae's @ [ae] @ aes) ((aeTy, ty) :: (dcs @ cs)))))
| collect' (ALet (x, ty', ae', ae, ty) :: aes) cs =
getTy ae' >>= (fn ae'Ty =>
getTy ae >>= (fn aeTy =>
collect' (ae' :: ae :: aes) ((ae'Ty, ty') :: (aeTy, ty) :: cs)))
| collect' (_ :: aes) cs = collect' aes cs
end end
fun collect ae = collect' [ae] []
......
LUCA-2/compile.sml
......@@ -12,9 +12,8 @@ structure Compile : sig
val typeof: string -> Ty.ty Attempt.attempt
val polish: string -> Ty.ty Attempt.attempt
val unty: string -> string Attempt.attempt
val elaborateIntermediate: string -> ElaborateIntermediate.term Attempt.attempt
val eval: string -> AST.term Attempt.attempt
val unval: string -> string Attempt.attempt
(* val eval: string -> AST.term Attempt.attempt *)
(* val unval: string -> string Attempt.attempt *)
val read: string -> string
......@@ -56,16 +55,15 @@ end = struct
Ty.resetTyVars ();
compile typeof (pure o Polish.polish) prog)
val unty = compile polish (pure o Ty.unty)
val elaborateIntermediate = compile parse ElaborateIntermediate.elaborate
fun eval prog =
let
val e = parse prog
in
typeof prog >>
e >>=
Eval.eval
end
val unval = compile eval (pure o AST.unparse)
(* fun eval prog = *)
(* let *)
(* val e = parse prog *)
(* in *)
(* typeof prog >> *)
(* e >>= *)
(* Eval.eval *)
(* end *)
(* val unval = compile eval (pure o AST.unparse) *)
fun read filename =
let
......
LUCA-2/elaborate-intermediate.sml deleted 100644 → 0
structure ElaborateIntermediate: sig
datatype term
= Zero
| Succ of term
| Pred of term
| True
| False
| String of string
| Unit
| Nil
| Cons of term * term
| Pair of term * term
| Left of term
| Right of term
| If of term * term * term
| Case of term * string * term * string * term
| Fun of string * term
| App of term * term
| Var of string
| Let of (string * term) list * term
val elaborate: AST.term -> term Attempt.attempt
end = struct
open Attempt
open AttemptMonad
structure AttemptMonadUtil = MonadUtil(AttemptMonad)
open AttemptMonadUtil
infixr 0 $
infix 1 >>= >>
infixr 1 =<< >=> <=<
infix 4 <$> <*>
datatype term
= Zero
| Succ of term
| Pred of term
| True
| False
| String of string
| Unit
| Nil
| Cons of term * term
| Pair of term * term
| Left of term
| Right of term
| If of term * term * term
| Case of term * string * term * string * term
| Fun of string * term
| App of term * term
| Var of string
| Let of (string * term) list * term
local structure A = AST in
fun elaborate (A.Int 0) = pure Zero
| elaborate (A.Int n) =
if n > 0
then
elaborate (A.Int (n - 1)) >>= (fn n' =>
pure (Succ n'))
else
elaborate (A.Int (n + 1)) >>= (fn n' =>
pure (Pred n'))
| elaborate A.True = pure True
| elaborate A.False = pure False
| elaborate (A.String s) = pure (String s)
| elaborate A.Unit = pure Unit
| elaborate (A.List []) = pure Nil
| elaborate (A.List (t :: ts)) =
elaborate (A.List ts) >>= (fn ts' =>
elaborate t >>= (fn t' =>
pure (Cons (t', ts'))))
| elaborate (A.Pair (t1, t2)) =
elaborate t1 >>= (fn t1' =>
elaborate t2 >>= (fn t2' =>
pure (Pair (t1', t2'))))
| elaborate (A.Left t) =
elaborate t >>= (fn t' =>
pure (Left t'))
| elaborate (A.Right t) =
elaborate t >>= (fn t' =>
pure (Right t'))
| elaborate (A.If (t1, t2, t3)) =
elaborate t1 >>= (fn t1' =>
elaborate t2 >>= (fn t2' =>
elaborate t3 >>= (fn t3' =>
pure (If (t1', t2', t3')))))
| elaborate (A.Case (t1, x2, t2, x3, t3)) =
elaborate t1 >>= (fn t1' =>
elaborate t2 >>= (fn t2' =>
elaborate t3 >>= (fn t3' =>
pure (Case (t1', x2, t2', x3, t3')))))
| elaborate (A.Fun (x, t)) =
elaborate t >>= (fn t' =>
pure (Fun (x, t')))
| elaborate (A.App (t1, t2)) =
elaborate t1 >>= (fn t1' =>
elaborate t2 >>= (fn t2' =>
pure (App (t1', t2'))))
| elaborate (A.Var x) = pure (Var x)
| elaborate (A.Let (ds, t)) =
let
val halfFix = Fun ("x", App (Var "f", App (Var "x", Var "x")))
val fix = Fun ("f", App (halfFix, halfFix))
in
elaborate t >>= (fn t' =>
forM ds (fn (x'', _, t'') =>
elaborate t'' >>= (fn t''' =>
pure (x'', App (fix, Fun ("x", t'''))))) >>= (fn ds' =>
pure (Let (ds', t'))))
end
end
end
LUCA-2/parse.sml
......@@ -19,28 +19,34 @@ end = struct
open ParseUtil
infix 1 \/
(* literal expressions *)
val unitExpr =
lit Scan.LParen >>
lit Scan.RParen >>
pure AST.Unit
val varExpr = AST.Var <$> identifier
val boolExpr =
(litKey "true" >> pure AST.True) \/
(litKey "false" >> pure AST.False)
fun toPeano 0 = AST.Zero
| toPeano n = AST.Succ (toPeano (n - 1))
val intExpr = fn ts =>
case ts
of Scan.Numeric n :: ts' => Success (AST.Int n, ts')
of Scan.Numeric n :: ts' => Success (toPeano n, ts')
| _ => Failure ("expected numeric, got: " ^ (Scan.unscan ts))
val unitExpr =
lit Scan.LParen >>
lit Scan.RParen >>
pure AST.Unit
val nilExpr =
lit Scan.LBracket >>
lit Scan.RBracket >>
pure AST.Nil
val stringExpr =
lit Scan.Quote >>
identifier >>= (fn s =>
lit Scan.Quote >>
pure (AST.String s))
val noneExpr =
litKey "None" >>
pure AST.None
(* recursive expressions *)
......@@ -50,59 +56,66 @@ end = struct
lit Scan.RParen >>
pure e1)) ts
and funExpr ts = (
and absExpr ts = (
litKey "fn" >>
(many1 identifier) >>= (fn args =>
(many1 identifier) >>= (fn xs =>
lit Scan.FatArrow >>
expr >>= (fn e =>
pure (foldr (fn (x, inner) => AST.Fun (x, inner)) e args)))) ts
pure (foldr AST.Abs e xs)))) ts
and appExpr ts = (
(varExpr \/ nestedExpr) >>= (fn f =>
many1 (litExpr \/ nestedExpr) >>= (fn args =>
pure (foldl (fn (x, f) => AST.App (f, x)) f args)))) ts
many1 (litExpr \/ nestedExpr) >>= (fn xs =>
pure (foldl (fn (x, f') => AST.App (f', x)) f xs)))) ts
and letExpr ts =
let
fun bindingExpr ts = (
litKey "val" >>
identifier >>= (fn x =>
((lit Scan.Colon >>
(TyExpr.tyExpr Scan.Equals) >>= (fn ty =>
pure (SOME ty))) \/
(pure NONE)) >>= (fn mTy =>
lit Scan.Equals >>
expr >>= (fn e =>
pure (x, mTy, e))))) ts
fun annotated ts = (
identifier >>= (fn x =>
lit Scan.Colon >>
TyExpr.tyExpr Scan.Equals >>= (fn ty =>
pure (x, SOME ty)))) ts
fun unannotated ts = (
identifier >>= (fn x =>
pure (x, NONE))) ts
val bindingExpr = annotated \/ unannotated
in (
litKey "let" >>
(many1 bindingExpr) >>= (fn ds =>
litKey "in" >>
expr >>= (fn e =>
pure (AST.Let (ds, e))))) ts
litKey "let" >>
bindingExpr >>= (fn (x, mTy) =>
lit Scan.Equals >>
expr >>= (fn e' =>
litKey "in" >>
expr >>= (fn e =>
pure (AST.Let (x, mTy, e', e)))))) ts
end
and commaExpr ts = (
expr >>= (fn e =>
lit Scan.Comma >>
pure e)) ts
and listExpr ts = (
lit Scan.LBracket >> ((
(many commaExpr) >>= (fn terms =>
expr >>= (fn last =>
lit Scan.RBracket >>
pure (AST.List (terms @ [last]))))) \/ (
lit Scan.RBracket >>
pure (AST.List [])))) ts
and listExpr ts =
let
fun commaExpr ts = (
lit Scan.Comma >>
expr >>= (fn e =>
pure e)) ts
in (
lit Scan.LBracket >>
expr >>= (fn hd =>
(many commaExpr) >>= (fn tl =>
lit Scan.RBracket >>
pure (foldr (fn (x, inner) => AST.Cons (x, inner)) AST.Nil (hd :: tl))))) ts
end
and pairExpr ts = (
and pairExpr ts =
let
fun commaExpr ts = (
expr >>= (fn e =>
lit Scan.Comma >>
pure e)) ts
in (
lit Scan.LParen >>
(many1 commaExpr) >>= (fn terms =>
expr >>= (fn last =>
(many1 commaExpr) >>= (fn fsts =>
expr >>= (fn snd =>
lit Scan.RParen >>
pure (foldr (fn (x, inner) => AST.Pair (x, inner)) last terms)))) ts
pure (foldr (fn (x, inner) => AST.Pair (x, inner)) snd fsts)))) ts
end
and ifExpr ts = (
litKey "if" >>
......@@ -113,59 +126,34 @@ end = struct
expr >>= (fn e3 =>
pure (AST.If (e1, e2, e3)))))) ts
and plusExpr ts = (
(litExpr \/ nestedExpr) >>= (fn e1 =>
lit Scan.Plus >>
(litExpr \/ nestedExpr) >>= (fn e2 =>
pure (AST.App (AST.App (AST.Var "plus", e1), e2))))) ts
and minusExpr ts = (
(litExpr \/ nestedExpr) >>= (fn e1 =>
lit Scan.Minus >>
(litExpr \/ nestedExpr) >>= (fn e2 =>
pure (AST.App (AST.App (AST.Var "minus", e1), e2))))) ts
and leftExpr ts = (
litId "Left" >>
expr >>= (fn e =>
pure (AST.Left e))) ts
and rightExpr ts = (
litId "Right" >>
expr >>= (fn e =>
pure (AST.Right e))) ts
and someExpr ts = (
litId "Some" >>
expr >>= (fn e =>
pure (AST.Left e))) ts
pure (AST.Some e))) ts
and noneExpr ts = (
litId "None" >>
pure (AST.Right AST.Unit)) ts
pure (AST.None)) ts
and caseExpr ts = (
(* case x *)
litKey "case" >>
(litExpr \/ nestedExpr) >>= (fn x =>
(* of Left x' => expr *)
litKey "of" >>
(litId "Left" \/ litId "Right") >>
identifier >>= (fn y =>
lit Scan.FatArrow >>
expr >>= (fn z =>
(* | Right x' => expr *)
lit Scan.Pipe >>
((litId "Right" >>
identifier) \/
(litId "None" >>
pure "_")) >>= (fn u =>
lit Scan.FatArrow >>
expr >>= (fn v =>
pure (AST.Case (x, y, z, u, v)))))))) ts
(* case e *)
litKey "case" >>
(litExpr \/ nestedExpr) >>= (fn e1 =>
(* of Some x => e *)
litKey "of" >>
litId "Some" >>
identifier >>= (fn x =>
lit Scan.FatArrow >>
expr >>= (fn e2 =>
(* | None => e *)
lit Scan.Pipe >>
litId "None" >>
lit Scan.FatArrow >>
expr >>= (fn e3 =>
pure (AST.Case (e1, x, e2, e3))))))) ts
and litExpr ts = (
boolExpr \/
......@@ -173,28 +161,22 @@ end = struct
listExpr \/
pairExpr \/
unitExpr \/
stringExpr \/
noneExpr \/
varExpr) ts
and expr ts = (
boolExpr \/
plusExpr \/
minusExpr \/
intExpr \/
listExpr \/
pairExpr \/
unitExpr \/
stringExpr \/
leftExpr \/
rightExpr \/
someExpr \/
noneExpr \/
ifExpr \/
caseExpr \/
funExpr \/
absExpr \/
appExpr \/
letExpr \/
......
LUCA-2/polish.sml
......@@ -12,26 +12,15 @@ end = struct
then (x, tv')
else lookupOrPolish ps x
fun polish' ps (Int | Bool | Unit | String) = ps
fun polish' ps (Unit | Bool | Int) = ps
| polish' ps (List ty) = polish' ps ty
| polish' ps (Option ty) = polish' ps ty
| polish' ps (Pair (ty1, ty2)) =
foldl (fn (ty', ps') => polish' ps' ty') ps [ty1, ty2]
| polish' ps (Fun (arg, ret)) =
let
val argPs = polish' ps arg
val retPs = polish' argPs ret
in
argPs @ retPs
end
foldl (fn (ty', ps') => polish' ps' ty') ps [arg, ret]
| polish' ps (TyVar x) =
ps @ [lookupOrPolish ps x]
| polish' ps (Sum (ty1, ty2)) =
let
val lPs = polish' ps ty1
val rPs = polish' lPs ty2
in
lPs @ rPs
end
fun polish ty = Unify.apply (polish' [] ty) ty
......
LUCA-2/scan.sml
......@@ -8,8 +8,6 @@ structure Scan: sig
| Equals
| Numeric of int
| Plus
| Minus
| LBracket
| RBracket
| Comma
......@@ -34,8 +32,6 @@ end = struct
| Equals
| Numeric of int
| Plus
| Minus
| LBracket
| RBracket
| Comma
......@@ -134,8 +130,6 @@ end = struct
| nextToken (#"(" :: cs) = Success (LParen, cs)
| nextToken (#")" :: cs) = Success (RParen, cs)
| nextToken (#"=" :: cs) = Success (Equals, cs)
| nextToken (#"+" :: cs) = Success (Plus, cs)
| nextToken (#"-" :: cs) = Success (Minus, cs)
| nextToken (#"[" :: cs) = Success (LBracket, cs)
| nextToken (#"]" :: cs) = Success (RBracket, cs)
| nextToken (#"," :: cs) = Success (Comma, cs)
......@@ -168,8 +162,6 @@ end = struct
| unscanT Equals = "="
| unscanT (Numeric n) = Int.toString n
| unscanT Plus = "+"
| unscanT Minus = "-"
| unscanT LBracket = "["
| unscanT RBracket = "]"
| unscanT Comma = ","
......
LUCA-2/sources.cm
......@@ -27,10 +27,6 @@ Group
structure Unify
structure Polish
structure ElaborateIntermediate
structure Eval
structure Compile
structure Tests
......@@ -63,9 +59,5 @@ is
unify.sml
polish.sml
elaborate-intermediate.sml
eval.sml
compile.sml
tests.sml
LUCA-2/ty.sml
structure Ty: sig
datatype ty
= Int
= Unit
| Bool
| String
| Unit
| Int
| List of ty
| Pair of ty * ty
| Sum of ty * ty
| Option of ty
| Fun of ty * ty
| TyVar of string
val unty: ty -> string
......@@ -24,41 +20,31 @@ end = struct
(* type declarations *)
datatype ty
= Int
= Unit
| Bool
| String
| Unit
| Int
| List of ty
| Pair of ty * ty
| Sum of ty * ty
| Option of ty
| Fun of ty * ty
| TyVar of string
local open Utils in
fun nest (ty as (Pair (ty1, ty2) | Sum (ty1, ty2) | Fun (ty1, ty2))) =
fun nest (ty as (Pair (ty1, ty2) | Fun (ty1, ty2))) =
paren (unty ty)
| nest ty = unty ty
and unty Int = "int"
and unty Unit = "unit"
| unty Bool = "bool"
| unty String = "string"
| unty Unit = "unit"
| unty Int = "int"
| unty (List ty) = spc [(nest ty), "list"]
| unty (Pair (ty1, ty2)) = (spc o between (map nest [ty1, ty2])) "*"
| unty (Sum (ty1, ty2)) =
if ty2 = Unit
then spc [(nest ty1), "option"]
else spc [(nest ty1), "|", (nest ty2)]
| unty (Option ty) = spc [(nest ty), "option"]
| unty (Fun (arg, res)) = (spc o between (map nest [arg, res])) "->"
| unty (TyVar v) = v
end
(* type variable utilities *)
val counter = ref 1
val polishedCounter = ref [0]
......
LUCA-2/tyexpr.sml
......@@ -13,11 +13,8 @@ structure TyExpr = struct
datatype opers
= Fun
| Pair
| Sum
| List
| Option
| LParen
datatype associativity = Left | Right
......@@ -28,12 +25,10 @@ structure TyExpr = struct
fun precedence Fun = 2
| precedence Pair = 1
| precedence Sum = 1
| precedence _ = raise Fail "tried to take precedence of non-binary operator"
fun associativity Fun = Right
| associativity Pair = Right
| associativity Sum = Right
| associativity _ = raise Fail "tried to take associativity of non-binary operator"
(* type expressions *)
......@@ -41,26 +36,21 @@ structure TyExpr = struct
shunt input ops ((Ty.Fun (x1, x2)) :: out)
| popFromOpers input (Pair :: ops) (x2 :: x1 :: out) =
shunt input ops ((Ty.Pair (x1, x2)) :: out)
| popFromOpers input (Sum :: ops) (x2 :: x1 :: out) =
shunt input ops ((Ty.Sum (x1, x2)) :: out)
| popFromOpers input (List :: ops) (x :: out) =
shunt input ops ((Ty.List x) :: out)
| popFromOpers input (Option :: ops) (x :: out) =
shunt input ops ((Ty.Sum (x, Ty.Unit)) :: out)
shunt input ops ((Ty.Option x) :: out)
| popFromOpers _ _ _ =
Failure "something wasn't right with the operator stack"
(* "number"s *)
and shunt ((Scan.Identifier "int") :: ts) ops out =
shunt ts ops (Ty.Int :: out)
and shunt ((Scan.Identifier "unit") :: ts) ops out =
shunt ts ops (Ty.Unit :: out)
| shunt ((Scan.Identifier "bool") :: ts) ops out =
shunt ts ops (Ty.Bool :: out)
| shunt ((Scan.Identifier "string") :: ts) ops out =
shunt ts ops (Ty.String :: out)
| shunt ((Scan.Identifier "unit") :: ts) ops out =
shunt ts ops (Ty.Unit :: out)
| shunt ((Scan.Identifier "int") :: ts) ops out =
shunt ts ops (Ty.Int :: out)
(* "function"s *)
| shunt ((Scan.Identifier "list") :: ts) ops out =
......@@ -74,7 +64,6 @@ structure TyExpr = struct
val oper = case operToken
of Scan.ThinArrow => Fun
| Scan.Asterisk => Pair
| Scan.Pipe => Sum
| _ => raise Fail "something really horrible must have happened here"
in
shunt ts [oper] out
......@@ -84,7 +73,6 @@ structure TyExpr = struct
val oper = case operToken
of Scan.ThinArrow => Fun
| Scan.Asterisk => Pair
| Scan.Pipe => Sum
| _ => raise Fail "something really horrible must have happened here"
in
if (
......
LUCA-2/unify.sml
......@@ -23,23 +23,23 @@ end = struct
open Ty
fun occurs _ (Int | Bool | Unit | String) = false
fun occurs _ (Unit | Bool | Int) = false
| occurs x (List ty) = occurs x ty
| occurs x (Pair (ty1, ty2)) = occurs x ty1 orelse occurs x ty2
| occurs x (Option ty) = occurs x ty
| occurs x (Fun (arg, ret)) = occurs x arg orelse occurs x ret
| occurs x (TyVar y) = x = y
| occurs x (Sum (ty1, ty2)) = occurs x ty1 orelse occurs x ty2
(* subst s for x in t *)
fun subst _ _ (x as (Int | Bool | Unit | String)) = x
fun subst _ _ (x as (Unit | Bool | Int)) = x
| subst s x (List ty) = List (subst s x ty)
| subst s x (Pair (ty1, ty2)) = Pair (subst s x ty1, subst s x ty2)
| subst s x (Option ty) = Option (subst s x ty)
| subst s x (Fun (arg, ret)) = Fun (subst s x arg, subst s x ret)
| subst s x (TyVar y) =
if x = y
then s
else TyVar y
| subst s x (Sum (ty1, ty2)) = Sum (subst s x ty1, subst s x ty2)
fun apply s t = foldr (fn ((x, t'), e) => subst t' x e) t s
......@@ -48,45 +48,41 @@ end = struct
then Failure ("Cannot unify " ^ x ^ " with " ^ (unty ty))
else Success [(x, ty)]
fun unifyPair Int Int = pure []
| unifyPair Int (TyVar x) = pure [(x, Int)]
| unifyPair (TyVar x) Int = pure [(x, Int)]
fun unify' Unit Unit = pure []
| unify' Unit (TyVar x) = pure [(x, Unit)]
| unify' (TyVar x) Unit = pure [(x, Unit)]
| unifyPair Bool Bool = pure []
| unifyPair Bool (TyVar x) = pure [(x, Bool)]
| unifyPair (TyVar x) Bool = pure [(x, Bool)]
| unify' Bool Bool = pure []
| unify' Bool (TyVar x) = pure [(x, Bool)]
| unify' (TyVar x) Bool = pure [(x, Bool)]
| unifyPair String String = pure []
| unifyPair String (TyVar x) = pure [(x, String)]
| unifyPair (TyVar x) String = pure [(x, String)]
| unify' Int Int = pure []
| unify' Int (TyVar x) = pure [(x, Int)]
| unify' (TyVar x) Int = pure [(x, Int)]
| unifyPair Unit Unit = pure []
| unifyPair Unit (TyVar x) = pure [(x, Unit)]
| unifyPair (TyVar x) Unit = pure [(x, Unit)]
| unify' (List ty1) (List ty2) = unify' ty1 ty2
| unifyPair (List ty1) (List ty2) = unifyPair ty1 ty2
| unifyPair (Pair (ty1, ty2)) (Pair (ty1', ty2')) =
| unify' (Pair (ty1, ty2)) (Pair (ty1', ty2')) =
unify [(ty1, ty1'), (ty2, ty2')]
| unifyPair (Sum (l1, r1)) (Sum (l2, r2)) = unify [(l1, l2), (r1, r2)]
| unify' (Option ty1) (Option ty2) = unify' ty1 ty2
| unifyPair (Fun (arg1, ret1)) (Fun (arg2, ret2)) =
| unify' (Fun (arg1, ret1)) (Fun (arg2, ret2)) =
unify [(arg1, arg2), (ret1, ret2)]
| unifyPair (TyVar x) (TyVar y) =
| unify' (TyVar x) (TyVar y) =
if x = y
then pure []
else pure [(y, TyVar x)]
| unifyPair ty (TyVar x) = unifyIfNotOccurs x ty
| unifyPair (TyVar x) ty = unifyIfNotOccurs x ty
| unify' ty (TyVar x) = unifyIfNotOccurs x ty
| unify' (TyVar x) ty = unifyIfNotOccurs x ty
| unifyPair x y = Failure ("cannot unify " ^ (unty x) ^ " with " ^ (unty y))
| unify' x y = Failure ("cannot unify " ^ (unty x) ^ " with " ^ (unty y))
and unify [] = pure []
| unify ((x, y) :: t) =
unify t >>= (fn t2 =>
unifyPair (apply t2 x) (apply t2 y) >>= (fn t1 =>
unify t >>= (fn t2 =>
unify' (apply t2 x) (apply t2 y) >>= (fn t1 =>
pure (t1 @ t2)))
end
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 sign in to comment