From d60bd86842b33fe1fa95b54e7afc229f84f0ef8b Mon Sep 17 00:00:00 2001
From: crumbtoo <crumb@disroot.org>
Date: Mon, 26 Feb 2024 18:18:02 -0700
Subject: [PATCH] it may not be perfection but it is progress

---
 rlp.cabal               |  1 +
 src/Core/Parse.y        | 20 +++++++++++++++++++-
 src/Core/Parse/Types.hs | 10 +++++++---
 src/Core/Syntax.hs      |  9 +++++++++
 4 files changed, 36 insertions(+), 4 deletions(-)

diff --git a/rlp.cabal b/rlp.cabal
index 3c66a85..bedfc4a 100644
--- a/rlp.cabal
+++ b/rlp.cabal
@@ -44,6 +44,7 @@ library
                     , Data.Heap
                     , Data.Pretty
                     , Core.Parse
+                    , Core.Parse.Types
                     , Core.Lex
                     , Core2Core
                     , Rlp2Core
diff --git a/src/Core/Parse.y b/src/Core/Parse.y
index f20690d..f42e6b5 100644
--- a/src/Core/Parse.y
+++ b/src/Core/Parse.y
@@ -76,7 +76,8 @@ Eof             : eof           { () }
                 | error         { () }
 
 StandaloneProgram :: { Program Var }
-StandaloneProgram : Program eof                 {% finishTyping $1 }
+-- StandaloneProgram : Program eof                 { undefined }
+StandaloneProgram : ProgramUgh eof                 { $1 }
 
 Program         :: { Program PsName }
 Program         : ScTypeSig ';' Program         { insTypeSig ($1 & _1 %~ Left) $3 }
@@ -86,6 +87,12 @@ Program         : ScTypeSig ';' Program         { insTypeSig ($1 & _1 %~ Left) $
                 | TLPragma  Program             {% doTLPragma $1 $2 }
                 | TLPragma                      {% doTLPragma $1 mempty }
 
+ProgramUgh      :: { Program Var }
+                : TypedScDef ';' ProgramUgh
+                            { $3 & insTypeSigUgh (fst $1)
+                                 & insScDef (snd $1) }
+                | OptSemi { mempty }
+
 TLPragma        :: { Pragma }
                 : '{-#' Words '#-}'             { Pragma $2 }
 
@@ -100,6 +107,10 @@ OptSemi         : ';'                           { () }
 ScTypeSig       :: { (Name, Type) }
 ScTypeSig       : Id ':' Type                   { ($1, $3) }
 
+TypedScDef      :: { (Var, ScDef Var) }
+                : Id ':' Type ';' Id ParListUgh '=' Expr
+                            { (MkVar $1 $3, mkTypedScDef $1 $3 $5 $6 $8) }
+
 ScDefs          :: { [ScDef PsName] }
 ScDefs          : ScDef ';' ScDefs              { $1 : $3 }
                 | ScDef ';'                     { [$1] }
@@ -120,6 +131,10 @@ Type1           : '(' Type ')'                  { $2 }
                 | varname                       { TyVar $1 }
                 | conname                       { TyCon $1 }
 
+ParListUgh      :: { [Name] }
+ParListUgh      : varname ParListUgh            { $1 : $2 }
+                | {- epsilon -}                 { [] }
+
 ParList         :: { [PsName] }
 ParList         : varname ParList               { Left $1 : $2 }
                 | {- epsilon -}                 { [] }
@@ -207,6 +222,9 @@ astPragma _ = undefined
 insTypeSig :: (Hashable b) => (b, Type) -> Program b -> Program b
 insTypeSig ts = programTypeSigs %~ uncurry H.insert ts
 
+insTypeSigUgh :: Var -> Program Var -> Program Var
+insTypeSigUgh w@(MkVar _ t) = programTypeSigs %~ H.insert w t
+
 singletonTypeSig :: (Hashable b) => (b, Type) -> Program b
 singletonTypeSig ts = insTypeSig ts mempty
 
diff --git a/src/Core/Parse/Types.hs b/src/Core/Parse/Types.hs
index 5456b4f..448bae0 100644
--- a/src/Core/Parse/Types.hs
+++ b/src/Core/Parse/Types.hs
@@ -4,7 +4,7 @@ module Core.Parse.Types
     , psTyVars
     , def
     , PsName
-    , finishTyping
+    , mkTypedScDef
     )
     where
 --------------------------------------------------------------------------------
@@ -12,6 +12,7 @@ import Control.Applicative
 import Control.Monad
 import Control.Monad.State
 import Data.Default
+import Data.Maybe
 import Data.Tuple               (swap)
 
 import Control.Lens
@@ -53,6 +54,9 @@ type PsName = Either Name Var
 
 --------------------------------------------------------------------------------
 
-finishTyping :: Program PsName -> P (Program Var)
-finishTyping = traverseOf binders undefined
+mkTypedScDef :: Name -> Type -> Name -> [Name] -> Expr Var -> ScDef Var
+mkTypedScDef nt tt n as e | nt == n = ScDef n' as' e
+    where
+        n' = MkVar n tt
+        as' = zipWith MkVar as (tt ^.. arrowStops)
 
diff --git a/src/Core/Syntax.hs b/src/Core/Syntax.hs
index 03a2292..cece62e 100644
--- a/src/Core/Syntax.hs
+++ b/src/Core/Syntax.hs
@@ -37,6 +37,7 @@ module Core.Syntax
     , formalising
     , HasRHS(_rhs), HasLHS(_lhs)
     , HasBinders(binders)
+    , HasArrowStops(arrowStops)
     )
     where
 ----------------------------------------------------------------------------------
@@ -543,6 +544,14 @@ instance (HasBinders (f b (Fix (f b))) (f b' (Fix (f b'))) b b')
       => HasBinders (Fix (f b)) (Fix (f b')) b b' where
     binders k (Fix f) = Fix <$> binders k f
 
+class HasArrowStops s t a b | s -> a, t -> b, s b -> t, t a -> s where
+    arrowStops :: Traversal s t a b
+
+instance HasArrowStops Type Type Type Type where
+    arrowStops k (s :-> t) = (:->) <$> k s <*> arrowStops k t
+
+--------------------------------------------------------------------------------
+
 liftEqExpr :: (Eq b)
            => (a -> a' -> Bool)
            -> ExprF b a -> ExprF b a' -> Bool