From: Mart Lubbers <mart@martlubbers.net>
Date: Mon, 4 Mar 2019 12:06:45 +0000 (+0100)
Subject: try letrec
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=fd1b446f346e18dbdeec2eb868c26764fddd84ca;p=minfp.git

try letrec
---

diff --git a/ast.dcl b/ast.dcl
index eecc8b6..9e733b2 100644
--- a/ast.dcl
+++ b/ast.dcl
@@ -3,17 +3,14 @@ definition module ast
 from Data.Either import :: Either
 from StdOverloaded import class toString
 
-:: AST = AST [Function]
-
 :: Function = Function [Char] [[Char]] Expression
-
 :: Expression
 	= Lit Value
 	| Var [Char]
 	| App Expression Expression
 	| Lambda [Char] Expression
 	| Builtin [Char] [Expression]
-	| Let [Char] Expression
+	| Let [Char] [[Char]] Expression Expression
 
 :: Value
 	= Int Int
@@ -26,4 +23,4 @@ from StdOverloaded import class toString
 	| TBool
 	| TFun Type Type
 
-instance toString AST, Function, Expression, Value, Type
+instance toString Expression, Value, Type
diff --git a/ast.icl b/ast.icl
index d934dd2..2714a0c 100644
--- a/ast.icl
+++ b/ast.icl
@@ -3,9 +3,6 @@ implementation module ast
 import StdEnv
 import Text
 
-instance toString AST where
-	toString (AST f) = join "\n" (map toString f)
-
 instance toString Function where
 	toString (Function i a e) = concat [toString i, " ", join " " (map toString a), " = ", toString e]
 
diff --git a/check.dcl b/check.dcl
index 015d891..b35ad70 100644
--- a/check.dcl
+++ b/check.dcl
@@ -1,7 +1,6 @@
 definition module check
 
 from Data.Either import :: Either
-from ast import :: AST, :: Type
+from ast import :: Function, :: Expression, :: Type
 
-:: Scheme     =   Forall [[Char]] Type
-check :: AST -> Either [String] (AST, [([Char], Scheme)])
+check :: [Function] -> Either [String] Expression
diff --git a/check.icl b/check.icl
index 5cac054..93f579d 100644
--- a/check.icl
+++ b/check.icl
@@ -2,189 +2,206 @@ implementation module check
 
 import StdEnv
 
-import qualified Data.Map as DM
-from Data.Map import instance Functor (Map k)
-import qualified Data.Set as DS
-import Data.Functor
-import Data.Func
 import Data.Either
 import Data.List
-import Data.Maybe
-import Control.Applicative
 import Control.Monad
-import Control.Monad.Trans
-import qualified Control.Monad.State as MS
-import Control.Monad.State => qualified gets, put, modify
-import Control.Monad.RWST => qualified put
 
 import ast
 
-check :: AST -> Either [String] (AST, [([Char], Scheme)])
-check (AST fs) = pure (AST fs, [])/*case inferAST preamble fs of
-	Left e = Left e
-	Right s = Right (AST fs, 'DM'.toList s)
+check :: [Function] -> Either [String] Expression
+check fs
+	# dups = filter (\x->length x > 1) (groupBy (\(Function i _ _) (Function j _ _)->i == j) fs)
+	| length dups > 0 = Left ["Duplicate functions: ":[toString n\\[(Function n _ _):_]<-dups]]
+	= case partition (\a->a=:(Function ['start'] _ _)) fs of
+		([], _) = Left ["No start function defined"]
+		([Function _ [] e], fs) = Right (foldr (\(Function i a e)->Let i a e) e fs)
+		([Function _ _ _], _) = Left ["Start cannot have arguments"]
 where
-	preamble = 'DM'.fromList
-		[(['if'], Forall [['a']] $ TFun TBool $ TFun (TVar ['a']) $ TFun (TVar ['a']) $ TVar ['a'])
-		,(['eq'], Forall [] $ TFun TInt $ TFun TInt TBool)
-		,(['mul'], Forall [] $ TFun TInt $ TFun TInt TInt)
-		,(['div'], Forall [] $ TFun TInt $ TFun TInt TInt)
-		,(['add'], Forall [] $ TFun TInt $ TFun TInt TInt)
-		,(['sub'], Forall [] $ TFun TInt $ TFun TInt TInt)
-		]
-*/
-
-:: TypeEnv    :== 'DM'.Map [Char] Scheme
-:: Constraint :== (Type, Type)
-:: Subst      :== 'DM'.Map [Char] Type
-:: Unifier    :== (Subst, [Constraint])
-:: Infer a    :== RWST TypeEnv [Constraint] InferState (Either [String]) a
-:: InferState =   { count :: Int }
-:: Scheme     =   Forall [[Char]] Type
-:: Solve a    :== StateT Unifier (Either [String]) a
-
-nullSubst :: Subst
-nullSubst = 'DM'.newMap
-
-uni :: Type Type -> Infer ()
-uni t1 t2 = tell [(t1, t2)]
-
-inEnv :: ([Char], Scheme) (Infer a) -> Infer a
-inEnv (x, sc) m = local (\e->'DM'.put x sc $ 'DM'.del x e) m
-
-letters :: [[Char]]
-letters = [1..] >>= flip replicateM ['a'..'z']
-
-fresh :: Infer Type
-fresh = get >>= \s=:{count}->'Control.Monad.RWST'.put {s & count=count + 1} >>| pure (TVar $ letters !! count)
-
-class Substitutable a
-where
-	apply :: Subst a -> a
-	ftv   :: a -> [[Char]]
-
-instance Substitutable Type
-where
-	apply s t=:(TVar a) = maybe t id $ 'DM'.get a s
-	apply s (TFun t1 t2)  = TFun (apply s t1) (apply s t2)
-	apply _ t = t
-
-	ftv (TVar a)     = [a]
-	ftv (TFun t1 t2) = union (ftv t1) (ftv t2)
-	ftv t            = []
-
-instance Substitutable Scheme
-where
-	apply s (Forall as t)   = Forall as $ apply (foldr 'DM'.del s as) t
-	ftv (Forall as t) = difference (ftv t) as
-
-instance Substitutable [a] | Substitutable a
-where
-	apply s ls = map (apply s) ls
-	ftv t = foldr (union o ftv) [] t
-
-instance Substitutable TypeEnv where
-	apply s env = fmap (apply s) env
-	ftv env = ftv $ 'DM'.elems env
-
-instance Substitutable Constraint where
-	apply s (t1, t2) = (apply s t1, apply s t2)
-	ftv (t1, t2) = union (ftv t1) (ftv t2)
-
-instantiate ::  Scheme -> Infer Type
-instantiate (Forall as t) = mapM (const fresh) as
-	>>= \as`->let s = 'DM'.fromList $ zip2 as as` in pure $ apply s t
-
-generalize :: TypeEnv Type -> Scheme
-generalize env t = Forall (difference (ftv t) (ftv env)) t
-
-//:: Expression
-//	= Lit Value
-//	| Var [Char]
-//	| App Expression Expression
-//	| Lambda [Char] Expression
-//	| Builtin [Char] [Expression]
-inferExpr :: TypeEnv Expression -> Either [String] Scheme
-inferExpr env ex = case runRWST (infer ex) env {count=0} of
-	Left e = Left e
-	Right (ty, st, cs) = case runStateT solver ('DM'.newMap, cs) of
-		Left e = Left e
-		Right (s, _) = Right (closeOver (apply s ty))
-
-closeOver :: Type -> Scheme
-closeOver t = normalize (generalize 'DM'.newMap t)
-
-normalize :: Scheme -> Scheme
-normalize t = t 
-
-inferAST :: TypeEnv [Function] -> Either [String] TypeEnv
-inferAST env [] = Right env
-inferAST env [Function name args body:rest] = case inferExpr env (foldr Lambda body args) of
-	Left e = Left e
-	Right ty = inferAST ('DM'.put name ty env) rest
-
-inferFunc :: [Function] -> Infer ()
-inferFunc [] = pure () 
-inferFunc [Function name args body:rest]
-	=      ask
-	>>= \en->infer (foldr Lambda body args)
-	>>= \t1->inEnv (name, generalize en t1) (inferFunc rest)
-	>>= \_->pure ()
-
-infer :: Expression -> Infer Type
-infer (Lit v) = case v of
-	Int  _ = pure TInt
-	Bool _ = pure TBool
-infer (Var s) = asks ('DM'.get s)
-	>>= maybe (liftT $ Left ["Unbound variable " +++ toString s]) instantiate
-infer (App e1 e2)
-	=        infer e1
-	>>= \t1->infer e2
-	>>= \t2->fresh
-	>>= \tv->uni t1 (TFun t2 tv)
-	>>|      pure tv
-infer (Lambda s e)
-	=        fresh
-	>>= \tv->inEnv (s, Forall [] tv) (infer e)
-	>>= \t-> pure (TFun tv t)
-//infer (Let x e1 e2)
-//	=        ask
-//	>>= \en->infer e1
-//	>>= \t1->inEnv (x, generalize en t1) (infer e2)
-
-unifies :: Type Type -> Solve Unifier
-unifies TInt TInt = pure ('DM'.newMap, [])
-unifies TBool TBool = pure ('DM'.newMap, [])
-unifies (TVar a) (TVar b) 
-	| a == b = pure ('DM'.newMap, [])
-unifies (TVar v) t = tbind v t
-unifies t (TVar v) = tbind v t
-unifies (TFun t1 t2) (TFun t3 t4) = unifyMany [t1, t2] [t3, t4]
-unifies t1 t2 = liftT $ Left ["Cannot unify " +++ toString t1 +++ " with " +++ toString t2]
-
-unifyMany :: [Type] [Type] -> Solve Unifier
-unifyMany [] [] = pure ('DM'.newMap, [])
-unifyMany [t1:ts1] [t2:ts2] = unifies t1 t2
-	>>= \(su1, cs1)->unifyMany (apply su1 ts1) (apply su1 ts2)
-	>>= \(su2, cs2)->pure (su2 `compose` su1, cs1 ++ cs2)
-unifyMany t1 t2 = liftT $ Left ["Length difference in unifyMany"]
-
-(`compose`) infix 1 :: Subst Subst -> Subst
-(`compose`) s1 s2 = 'DM'.union (apply s1 <$> s2) s1
-
-tbind ::  [Char] Type -> Solve Unifier
-tbind a (TVar b)
-	| a == b = pure ('DM'.newMap, [])
-tbind a t
-	| occursCheck a t = liftT $ Left ["Infinite type " +++ toString a +++ toString t]
-	= pure $ ('DM'.singleton a t, [])
-
-occursCheck ::  [Char] a -> Bool | Substitutable a
-occursCheck a t = isMember a $ ftv t
-
-solver :: Solve Subst
-solver = getState >>= \(su, cs)->case cs of
-	[] = pure su
-	[(t1, t2):cs0] = unifies t1 t2
-		>>= \(su1, cs1)->'MS'.put (su1 `compose` su, cs1 ++ (apply su1 cs0))
-		>>| solver
+	funs = [i\\(Function i _ _)<-fs]
+
+//import qualified Data.Map as DM
+//from Data.Map import instance Functor (Map k)
+//import qualified Data.Set as DS
+//import Data.Functor
+//import Data.Func
+//import Data.Either
+//import Data.List
+//import Data.Maybe
+//import Control.Applicative
+//import Control.Monad
+//import Control.Monad.Trans
+//import qualified Control.Monad.State as MS
+//import Control.Monad.State => qualified gets, put, modify
+//import Control.Monad.RWST => qualified put
+//
+//import ast
+//
+//check :: AST -> Either [String] (AST, [([Char], Scheme)])
+//check (AST fs) = pure (AST fs, [])/*case inferAST preamble fs of
+//	Left e = Left e
+//	Right s = Right (AST fs, 'DM'.toList s)
+//where
+//	preamble = 'DM'.fromList
+//		[(['if'], Forall [['a']] $ TFun TBool $ TFun (TVar ['a']) $ TFun (TVar ['a']) $ TVar ['a'])
+//		,(['eq'], Forall [] $ TFun TInt $ TFun TInt TBool)
+//		,(['mul'], Forall [] $ TFun TInt $ TFun TInt TInt)
+//		,(['div'], Forall [] $ TFun TInt $ TFun TInt TInt)
+//		,(['add'], Forall [] $ TFun TInt $ TFun TInt TInt)
+//		,(['sub'], Forall [] $ TFun TInt $ TFun TInt TInt)
+//		]
+//*/
+//
+//:: TypeEnv    :== 'DM'.Map [Char] Scheme
+//:: Constraint :== (Type, Type)
+//:: Subst      :== 'DM'.Map [Char] Type
+//:: Unifier    :== (Subst, [Constraint])
+//:: Infer a    :== RWST TypeEnv [Constraint] InferState (Either [String]) a
+//:: InferState =   { count :: Int }
+//:: Scheme     =   Forall [[Char]] Type
+//:: Solve a    :== StateT Unifier (Either [String]) a
+//
+//nullSubst :: Subst
+//nullSubst = 'DM'.newMap
+//
+//uni :: Type Type -> Infer ()
+//uni t1 t2 = tell [(t1, t2)]
+//
+//inEnv :: ([Char], Scheme) (Infer a) -> Infer a
+//inEnv (x, sc) m = local (\e->'DM'.put x sc $ 'DM'.del x e) m
+//
+//letters :: [[Char]]
+//letters = [1..] >>= flip replicateM ['a'..'z']
+//
+//fresh :: Infer Type
+//fresh = get >>= \s=:{count}->'Control.Monad.RWST'.put {s & count=count + 1} >>| pure (TVar $ letters !! count)
+//
+//class Substitutable a
+//where
+//	apply :: Subst a -> a
+//	ftv   :: a -> [[Char]]
+//
+//instance Substitutable Type
+//where
+//	apply s t=:(TVar a) = maybe t id $ 'DM'.get a s
+//	apply s (TFun t1 t2)  = TFun (apply s t1) (apply s t2)
+//	apply _ t = t
+//
+//	ftv (TVar a)     = [a]
+//	ftv (TFun t1 t2) = union (ftv t1) (ftv t2)
+//	ftv t            = []
+//
+//instance Substitutable Scheme
+//where
+//	apply s (Forall as t)   = Forall as $ apply (foldr 'DM'.del s as) t
+//	ftv (Forall as t) = difference (ftv t) as
+//
+//instance Substitutable [a] | Substitutable a
+//where
+//	apply s ls = map (apply s) ls
+//	ftv t = foldr (union o ftv) [] t
+//
+//instance Substitutable TypeEnv where
+//	apply s env = fmap (apply s) env
+//	ftv env = ftv $ 'DM'.elems env
+//
+//instance Substitutable Constraint where
+//	apply s (t1, t2) = (apply s t1, apply s t2)
+//	ftv (t1, t2) = union (ftv t1) (ftv t2)
+//
+//instantiate ::  Scheme -> Infer Type
+//instantiate (Forall as t) = mapM (const fresh) as
+//	>>= \as`->let s = 'DM'.fromList $ zip2 as as` in pure $ apply s t
+//
+//generalize :: TypeEnv Type -> Scheme
+//generalize env t = Forall (difference (ftv t) (ftv env)) t
+//
+////:: Expression
+////	= Lit Value
+////	| Var [Char]
+////	| App Expression Expression
+////	| Lambda [Char] Expression
+////	| Builtin [Char] [Expression]
+//inferExpr :: TypeEnv Expression -> Either [String] Scheme
+//inferExpr env ex = case runRWST (infer ex) env {count=0} of
+//	Left e = Left e
+//	Right (ty, st, cs) = case runStateT solver ('DM'.newMap, cs) of
+//		Left e = Left e
+//		Right (s, _) = Right (closeOver (apply s ty))
+//
+//closeOver :: Type -> Scheme
+//closeOver t = normalize (generalize 'DM'.newMap t)
+//
+//normalize :: Scheme -> Scheme
+//normalize t = t 
+//
+//inferAST :: TypeEnv [Function] -> Either [String] TypeEnv
+//inferAST env [] = Right env
+//inferAST env [Function name args body:rest] = case inferExpr env (foldr Lambda body args) of
+//	Left e = Left e
+//	Right ty = inferAST ('DM'.put name ty env) rest
+//
+//inferFunc :: [Function] -> Infer ()
+//inferFunc [] = pure () 
+//inferFunc [Function name args body:rest]
+//	=      ask
+//	>>= \en->infer (foldr Lambda body args)
+//	>>= \t1->inEnv (name, generalize en t1) (inferFunc rest)
+//	>>= \_->pure ()
+//
+//infer :: Expression -> Infer Type
+//infer (Lit v) = case v of
+//	Int  _ = pure TInt
+//	Bool _ = pure TBool
+//infer (Var s) = asks ('DM'.get s)
+//	>>= maybe (liftT $ Left ["Unbound variable " +++ toString s]) instantiate
+//infer (App e1 e2)
+//	=        infer e1
+//	>>= \t1->infer e2
+//	>>= \t2->fresh
+//	>>= \tv->uni t1 (TFun t2 tv)
+//	>>|      pure tv
+//infer (Lambda s e)
+//	=        fresh
+//	>>= \tv->inEnv (s, Forall [] tv) (infer e)
+//	>>= \t-> pure (TFun tv t)
+////infer (Let x e1 e2)
+////	=        ask
+////	>>= \en->infer e1
+////	>>= \t1->inEnv (x, generalize en t1) (infer e2)
+//
+//unifies :: Type Type -> Solve Unifier
+//unifies TInt TInt = pure ('DM'.newMap, [])
+//unifies TBool TBool = pure ('DM'.newMap, [])
+//unifies (TVar a) (TVar b) 
+//	| a == b = pure ('DM'.newMap, [])
+//unifies (TVar v) t = tbind v t
+//unifies t (TVar v) = tbind v t
+//unifies (TFun t1 t2) (TFun t3 t4) = unifyMany [t1, t2] [t3, t4]
+//unifies t1 t2 = liftT $ Left ["Cannot unify " +++ toString t1 +++ " with " +++ toString t2]
+//
+//unifyMany :: [Type] [Type] -> Solve Unifier
+//unifyMany [] [] = pure ('DM'.newMap, [])
+//unifyMany [t1:ts1] [t2:ts2] = unifies t1 t2
+//	>>= \(su1, cs1)->unifyMany (apply su1 ts1) (apply su1 ts2)
+//	>>= \(su2, cs2)->pure (su2 `compose` su1, cs1 ++ cs2)
+//unifyMany t1 t2 = liftT $ Left ["Length difference in unifyMany"]
+//
+//(`compose`) infix 1 :: Subst Subst -> Subst
+//(`compose`) s1 s2 = 'DM'.union (apply s1 <$> s2) s1
+//
+//tbind ::  [Char] Type -> Solve Unifier
+//tbind a (TVar b)
+//	| a == b = pure ('DM'.newMap, [])
+//tbind a t
+//	| occursCheck a t = liftT $ Left ["Infinite type " +++ toString a +++ toString t]
+//	= pure $ ('DM'.singleton a t, [])
+//
+//occursCheck ::  [Char] a -> Bool | Substitutable a
+//occursCheck a t = isMember a $ ftv t
+//
+//solver :: Solve Subst
+//solver = getState >>= \(su, cs)->case cs of
+//	[] = pure su
+//	[(t1, t2):cs0] = unifies t1 t2
+//		>>= \(su1, cs1)->'MS'.put (su1 `compose` su, cs1 ++ (apply su1 cs0))
+//		>>| solver
diff --git a/gen.dcl b/gen.dcl
index e9e876d..ab44a57 100644
--- a/gen.dcl
+++ b/gen.dcl
@@ -1,6 +1,6 @@
 definition module gen
 
 from Data.Either import :: Either
-from ast import :: AST
+from ast import :: Expression
 
-gen :: AST -> Either [String] [String]
+gen :: Expression -> Either [String] [String]
diff --git a/gen.icl b/gen.icl
index 01fa272..6c7b5ee 100644
--- a/gen.icl
+++ b/gen.icl
@@ -8,7 +8,9 @@ import Text
 
 import ast
 
-gen :: AST -> Either [String] [String]
+gen :: Expression -> Either [String] [String]
+gen _ = Left ["genbork"]
+/*
 gen (AST fs) = Right
 	["#include \"rts.h\"\n"
 	:genCode fs []
@@ -34,3 +36,4 @@ instance genCode Expression where
 	genCode (App a b) c = ["ap(":genCode a [", ":genCode b [")":c]]]
 	genCode (Lambda a b) c = abort "help"
 	genCode (Builtin b args) c = genCode b ["(":genCode args [")":c]]
+*/
diff --git a/int.dcl b/int.dcl
index 1b8d96f..b36e59a 100644
--- a/int.dcl
+++ b/int.dcl
@@ -1,6 +1,6 @@
 definition module int
 
 from Data.Either import :: Either
-from ast import :: AST, :: Value
+from ast import :: Expression, :: Value
 
-int :: AST -> Either [String] Value
+int :: Expression -> Either [String] Value
diff --git a/int.icl b/int.icl
index 4d2087a..be7e595 100644
--- a/int.icl
+++ b/int.icl
@@ -13,8 +13,9 @@ import Control.Monad.Trans
 
 import ast
 
-int :: AST -> Either [String] Value
-int (AST fs) = evalStateT (mapM evalFun fs >>| getStart fs >>= eval >>= printer) preamble
+int :: Expression -> Either [String] Value
+int _ = Left ["intbork"]
+/*int (AST fs) = evalStateT (mapM evalFun fs >>| getStart fs >>= eval >>= printer) preamble
 
 err :: String -> Eval a
 err e = liftT (Left [e])
@@ -87,3 +88,4 @@ eval (Builtin i as) = case (i, as) of
 	(['eq'], [l,r]) = eval l >>= printer >>= \l->eval r >>= printer >>= \r->case (l,r) of
 		(Int a, Int b) = pure (Bool (a == b))
 //		_ = err "eq only defined for integers"
+*/
diff --git a/main.icl b/main.icl
index d2b5114..910de46 100644
--- a/main.icl
+++ b/main.icl
@@ -24,8 +24,8 @@ chars f
 :: Mode = MHelp | MLex | MParse | MType | MInterpret | MGen
 :: Result
 	= Lex [Token]
-	| Parse AST
-	| Type [([Char], Scheme)]
+	| Parse [Function]
+	| Type Expression
 	| Interpret Value
 	| Gen [String]
 
@@ -52,6 +52,6 @@ Start w
 		MHelp = Left [usageInfo ("Usage: " +++ argv0 +++ " [options]\n") options]
 		MLex = Lex <$> lex cs
 		MParse = Parse <$> (lex cs >>= parse)
-		MType = Type <$> snd <$> (lex cs >>= parse >>= check)
-		MInterpret = Interpret <$> (lex cs >>= parse >>= check >>= int o fst)
-		MGen = Gen <$> (lex cs >>= parse >>= check >>= gen o fst)
+		MType = Type <$> (lex cs >>= parse >>= check)
+		MInterpret = Interpret <$> (lex cs >>= parse >>= check >>= int)
+		MGen = Gen <$> (lex cs >>= parse >>= check >>= gen)
diff --git a/parse.dcl b/parse.dcl
index 84718fe..07121fd 100644
--- a/parse.dcl
+++ b/parse.dcl
@@ -1,8 +1,8 @@
 definition module parse
 
 from Data.Either import :: Either
-from ast import :: AST
+from ast import :: Function
 
 :: Token
 lex :: [Char] -> Either [String] [Token]
-parse :: [Token] -> Either [String] AST
+parse :: [Token] -> Either [String] [Function]
diff --git a/parse.icl b/parse.icl
index e17ad02..c35f78a 100644
--- a/parse.icl
+++ b/parse.icl
@@ -74,8 +74,8 @@ pChainl op p = foldl (flip ($)) <$> p <*> many (flip <$> op <*> p)
 pChainr :: (Parser (a a -> a)) (Parser a) -> Parser a
 pChainr op p = flip ($) <$> p <*> (flip <$> op <*> pChainr op p) <|> p
 
-parse :: [Token] -> Either [String] AST
-parse ts = case runStateT (AST <$> pAST <* pEof) {zero & tokens=ts} of
+parse :: [Token] -> Either [String] [Function]
+parse ts = case runStateT (pAST <* pEof) {zero & tokens=ts} of
 	Right (a, _) = Right a
 	Left e = Left e
 where