Create let-reduction phase; let-bound polymorphism working but hacky

LUCA-2/annotate.sml

@@ -24,8 +24,6 @@ structure Annotate: sig
     | AAbs of string * aterm * Ty.ty
     | AApp of aterm * 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
 
@@ -68,8 +66,6 @@ end = struct
     | AAbs of string * aterm * Ty.ty
     | AApp of aterm * aterm * Ty.ty
 
-    | ALet of string * Ty.ty * aterm * aterm * Ty.ty
-
   fun getTy (AUnit ty) = pure ty
     | getTy (AVar (_, ty)) = pure ty
 
@@ -93,8 +89,6 @@ end = struct
     | getTy (AAbs (_, _, ty)) = pure ty
     | getTy (AApp (_, _, ty)) = pure ty
 
-    | getTy (ALet (_, _, _, _, ty)) = pure ty
-
   fun annotate' g AST.Unit = pure (AUnit Ty.Unit)
     | annotate' g (AST.Var x) =
         TyEnv.lookup g x >>= (fn ty =>
@@ -154,12 +148,16 @@ end = struct
         annotate' g arg >>= (fn aarg =>
         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 ()))))
+    (* | 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 ())))) *)
+
+    (* TODO: what do we do with type annotations? *)
+    | annotate' g (AST.Let (_, _, _, _)) =
+        Failure "annotate: unexpected let (should've been reduced away)"
 
   val annotate = annotate' []
 

LUCA-2/ast.sml

@@ -26,12 +26,25 @@ structure AST: sig
 
     | Let of string * Ty.ty option * term * term
 
+  val subst: term -> string -> term -> term
+
   val isValue: term -> bool
 
   val unparse: term -> string
 
 end = struct
 
+  open Attempt
+
+  open AttemptMonad
+  structure AttemptMonadUtil = MonadUtil(AttemptMonad)
+  open AttemptMonadUtil
+  infixr 0 $
+  infix 1 >>= >>
+  infixr 1 =<< >=> <=<
+  infix 4 <$> <*>
+
+
   datatype term
     = Unit
     | Var of string
@@ -59,6 +72,67 @@ end = struct
     | Let of string * Ty.ty option * term * term
 
 
+  (* substitute s for x in e *)
+  fun subst _ _ Unit = Unit
+    | subst s x (Var y) =
+        if x = y
+        then s
+        else Var y
+    | subst _ _ True = True
+    | subst _ _ False = False
+    | subst s x (If (e1, e2, e3)) = crank3 s x e1 e2 e3 If
+    | subst _ _ Zero = Zero
+    | subst s x (Succ e) = crank1 s x e Succ
+    | subst s x (Pred e) = crank1 s x e Pred
+    | subst _ _ Nil = Nil
+    | subst s x (Cons (e1, e2)) = crank2 s x e1 e2 Cons
+    | subst s x (Pair (e1, e2)) = crank2 s x e1 e2 Pair
+    | subst _ _ None = None
+    | subst s x (Some e) = crank1 s x e Some
+    | subst s x (Case (e1, x2, e2, e3)) =
+      let
+        val (x2', e2Pre) = freshen x x2 e2
+      in
+        crank3 s x e1 e2Pre e3 (fn (e1', e2', e3') => (Case (e1', x2', e2', e3')))
+      end
+    | subst s x (Abs (y, e)) =
+      let
+        val (y', ePre) = freshen x y e
+      in
+        crank1 s x ePre (fn e' => Abs (y', e'))
+      end
+    | subst s x (App (e1, e2)) = crank2 s x e1 e2 App
+    | subst s x (Let (y, ty, e1, e2)) =
+      let
+        val (y', e1Pre) = freshen x y e1
+        val (y', e2Pre) = freshen x y e2
+      in
+        crank2 s x e1Pre e2Pre (fn (e1', e2') => Let (y', ty, e1', e2'))
+      end
+
+  and freshen x1 x2 e =
+    if x1 = x2
+    then ("@" ^ x2, subst (Var ("@" ^ x2)) x2 e)
+    else (x2, e)
+
+  and crank1 s x e con = con (subst s x e)
+  and crank2 s x e1 e2 con =
+    let
+      val e1' = subst s x e1
+      val e2' = subst s x e2
+    in
+      con (e1', e2')
+    end
+  and crank3 s x e1 e2 e3 con =
+    let
+      val e1' = subst s x e1
+      val e2' = subst s x e2
+      val e3' = subst s x e3
+    in
+      con (e1', e2', e3')
+    end
+
+
   fun isValue Unit = true
 
     | isValue (True | False) = true

LUCA-2/collect.sml

@@ -55,10 +55,10 @@ end = struct
         getTy arg >>= (fn argTy =>
         collect' (f :: arg :: aes) ((fTy, Fun (argTy, ty)) :: 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' (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

LUCA-2/compile.sml

@@ -6,6 +6,7 @@ structure Compile : sig
   val unscan: string -> string Attempt.attempt
   val parse: string -> AST.term Attempt.attempt
   val unparse: string -> string Attempt.attempt
+  val letReduce: string -> AST.term Attempt.attempt
   val annotate: string -> Annotate.aterm Attempt.attempt
   val collect: string -> (Ty.ty * Ty.ty) list Attempt.attempt
   val unify: string -> Unify.substitution Attempt.attempt
@@ -40,7 +41,9 @@ end = struct
   val parse = compile scan Parse.parse
   val unparse = compile parse (pure o AST.unparse)
 
-  val annotate = compile parse Annotate.annotate
+  val letReduce = compile parse (pure o LetReduce.reduce)
+
+  val annotate = compile letReduce Annotate.annotate
   val collect = compile annotate Collect.collect
   val unify = compile collect Unify.unify
   fun typeof prog =

LUCA-2/letreduce.sml

+structure LetReduce: sig
+
+  val reduce: AST.term -> AST.term
+
+end = struct
+
+  local open AST in
+  fun reduce Unit = Unit
+    | reduce (Var x) = Var x
+    | reduce True = True
+    | reduce False = False
+    | reduce (If (e1, e2, e3)) = crank3 e1 e2 e3 If
+    | reduce Zero = Zero
+    | reduce (Succ e) = crank1 e Succ
+    | reduce (Pred e) = crank1 e Pred
+    | reduce Nil = Nil
+    | reduce (Cons (e1, e2)) = crank2 e1 e2 Cons
+    | reduce (Pair (e1, e2)) = crank2 e1 e2 Pair
+    | reduce None = None
+    | reduce (Some e) = crank1 e Some
+    | reduce (Case (e1, x2, e2, e3)) = crank3 e1 e2 e3 (fn (e1', e2', e3') => Case (e1', x2, e2', e3'))
+    | reduce (Abs (x, e)) = crank1 e (fn e' => Abs (x, e'))
+    | reduce (App (e1, e2)) = crank2 e1 e2 App
+    | reduce (Let (x, ty, e1, e2)) = reduce (subst e1 x e2)
+
+  and crank1 e con = con (reduce e)
+  and crank2 e1 e2 con =
+    let
+      val e1' = reduce e1
+      val e2' = reduce e2
+    in
+      con (e1, e2)
+    end
+  and crank3 e1 e2 e3 con =
+    let
+      val e1' = reduce e1
+      val e2' = reduce e2
+      val e3' = reduce e3
+    in
+      con (e1, e2, e3)
+    end
+  end
+
+end

LUCA-2/sources.cm

@@ -21,6 +21,8 @@ Group
   structure Impl
   structure Parse
 
+  structure LetReduce
+
   structure TyEnv
   structure Annotate
   structure Collect
@@ -53,6 +55,8 @@ is
   impl.sml
   parse.sml
 
+  letreduce.sml
+
   tyenv.sml
   annotate.sml
   collect.sml

log.txt

@@ -161,3 +161,5 @@ It's ugly, but complete, and it does in fact work in isolated testing.
 Trouble is, it doesn't play nice with the larger parser. I'm going to have to consult some other functional implementations of this algorithm to see how I can simplify this.
 
 Specifically, I don't think I have a reliable way to tell it when it's done with the output. What I could do is find a way to have it ignore tokens that couldn't be part of the type expression. Or, in the let parser, I could gobble the tokens until the Equals, and then pass those tokens into the shunting yard parser. I think that might actually be easier, but I still want to see if I can make the shunting yard nicer.
+
+2019-05-27 21:28 Let polymorphism is working but I don't yet know what to do with ascribed types - do we just drop them?