Prep to switch from Def to CExp for backend passes.

.gitignore

@@ -1,5 +1,4 @@
 build/
-*.*~ATTIC
 \#*
 *~
 *.swp

serializer.ts

@@ -10,7 +10,6 @@ const NUMBER = 5;
 const NULL = 6;
 const te = new TextEncoder();
 
-// TODO - next two functions are machine generated and need to be fixed
 class DeserializationStream {
   pos = 0;
   buf: Uint8Array;

src/Data/Graph.newt

@@ -0,0 +1,87 @@
+module Data.Graph
+
+import Prelude
+import Data.SortedMap
+import Data.SnocList
+
+-- https://en.wikipedia.org/wiki/Tarjan%27s_strongly_connected_components_algorithm#The_algorithm_in_pseudocode
+
+-- Based on the wikipedia article, probably could use cleanup. Maybe switch to state monad.
+
+record TVertex k where
+  constructor MkTV
+  name : k
+  out : List k
+  index : Int
+  lowLink : Int
+  onStack : Bool
+
+record TState k where
+  constructor MkTState
+  lastIndex : Int
+  stack : List k
+  result : List (List k)
+  graph : SortedMap k (TVertex k)
+
+strongConnect : ∀ k. {{Ord k}} → TState k → TVertex k → TState k
+strongConnect {k} st vtx =
+  let index' = st.lastIndex + 1
+      vtx' = MkTV vtx.name vtx.out index' index' True
+      stack' = vtx.name :: st.stack
+      graph' = updateMap vtx'.name vtx' st.graph
+      st' = MkTState index' stack' st.result graph'
+  in checkRoot $ foldl doEdge st' vtx.out
+  where
+    -- There is a lot in here because everything is public at the moment
+    -- Although we do reach for `k` and `vtx.name` a few times
+    min : Int → Int → Int
+    min a b = if a < b then a else b
+
+    splitComp : List k → List k → (List k × List k)
+    splitComp acc Nil = (acc, Nil)
+    splitComp acc (x :: xs) = if compare x vtx.name == EQ
+      then (x :: acc, xs)
+      else splitComp (x :: acc) xs
+
+    updateNode : TState k → k → (TVertex k → TVertex k) → TState k
+    updateNode st@(MkTState lastIndex stack result graph) name f =
+      case lookupMap' name graph of
+        Just v => MkTState lastIndex stack result (updateMap name (f v) graph)
+        Nothing => st
+
+    updateLowLink : TState k → k → Int → TState k
+    updateLowLink st nm v = updateNode st nm $ \ vt => MkTV vt.name vt.out vt.index (min vt.lowLink v) vt.onStack
+
+    offStack : TState k → k → TState k
+    offStack st name = updateNode st name $ \ vt => MkTV vt.name vt.out vt.index vt.lowLink False
+
+    doEdge : TState k → k → TState k
+    doEdge st k =
+      let (Just w) = lookupMap' k st.graph | _ => st in
+      if w.onStack then updateLowLink st vtx.name w.index
+      else if w.index == 0 then
+        let st' = strongConnect st w in
+        let (Just w) = lookupMap' k st'.graph | _ => st' in
+        updateLowLink st' vtx.name w.lowLink
+      else st
+
+    checkRoot : TState k → TState k
+    checkRoot st =
+      let (Just v) = lookupMap' vtx.name st.graph | _ => st in
+      if v.lowLink == v.index
+      then let (comp,stack) = splitComp Nil st.stack in
+           let st = foldl offStack st comp in
+           MkTState st.lastIndex stack (comp :: st.result) st.graph
+      else st -- leave on stack
+
+tarjan : ∀ k. {{Ord k}} → List (k × List k) → List (List k)
+tarjan {k} nodes =
+  let g = foldMap const EmptyMap $ map mkVertex nodes in
+  .result $ foldl checkVertex (MkTState 0 Nil Nil g) $ map fst nodes
+  where
+    mkVertex : k × List k → k × TVertex k
+    mkVertex (n,out) = (n, MkTV n out 0 0 False)
+
+    checkVertex : TState k → k → TState k
+    checkVertex st k = let (Just vtx) = lookupMap' k st.graph | _ => st in
+      if vtx.index > 0 then st else strongConnect st vtx

src/Data/TestGraph.newt

@@ -0,0 +1,20 @@
+module Data.TestGraph
+
+import Prelude
+import Data.Graph
+import Node
+
+main : IO Unit
+main = do
+  let (_ :: fn :: Nil) = getArgs | args => putStrLn "bad args \{show args}"
+  (Right text) <- readFile fn | Left err => putStrLn "Can't read \{fn}: \{show err}"
+  let graph = mapMaybe readLine $ split text "\n"
+  debugLog graph
+  let result = tarjan graph
+  debugLog result
+  where
+    readLine : String → Maybe (String × List String)
+    readLine line = case split line " " of
+      ("" :: _) => Nothing
+      (x :: rest) => Just (x, rest)
+      _ => Nothing

src/Lib/Common.newt

@@ -7,6 +7,9 @@ import Data.SortedMap
 
 -- l is environment size, this works for both lvl2ix and ix2lvl
 
+range : Int → Int → List Int
+range n m = if n < m then n :: range (n + 1) m else Nil
+
 lvl2ix : Int -> Int -> Int
 lvl2ix l k = l - k - 1
 

src/Lib/Compile.newt

@@ -8,6 +8,7 @@ import Lib.Prettier
 import Lib.CompileExp
 import Lib.TopContext
 import Lib.LiftWhere
+import Lib.TCO
 import Lib.Ref2
 import Lib.Erasure
 import Data.String
@@ -36,6 +37,7 @@ data JSExp : U where
   JUndefined : JSExp
   Index : JSExp -> JSExp -> JSExp
   Dot : JSExp -> String -> JSExp
+  Raw : String -> JSExp
 
 data JSStmt : StKind -> U where
   -- Maybe make this a snoc...
@@ -108,6 +110,9 @@ freshNames nms env = go nms env Lin
       let (n', env') = freshName' n env
       in go ns env' (acc :< n')
 
+
+
+
 -- This is inspired by A-normalization, look into the continuation monad
 -- There is an index on JSStmt, adopted from Stefan Hoeck's code.
 --
@@ -119,6 +124,7 @@ termToJS env (CBnd k) f = case getAt (cast k) env.jsenv of
   (Just e) => f e
   Nothing => fatalError "Bad bounds"
 termToJS env CErased f = f JUndefined
+termToJS env (CRaw str) f = f (Raw str)
 termToJS env (CLam nm t) f =
   let (nm',env') = freshName' nm env -- "\{nm}$\{show $ length env}"
   in f $ JLam (nm' :: Nil) (termToJS env' t JReturn)
@@ -146,7 +152,11 @@ termToJS env (CLetRec nm t u) f =
   in case termToJS env' t (JAssign nm') of
     (JAssign _ exp) => JSnoc (JConst nm' exp) (termToJS env' u f)
     t' => JSnoc (JLet nm' t') (termToJS env' u f)
-
+termToJS env (CConstr nm args) f = go args 0 (\ args => f $ LitObject (("tag", LitString nm) :: args))
+  where
+    go : ∀ e. List CExp -> Int -> (List (String × JSExp) -> JSStmt e) -> JSStmt e
+    go Nil ix k = k Nil
+    go (t :: ts) ix k = termToJS env t $ \ t' => go ts (ix + 1) $ \ args => k $ ("h\{show ix}", t') :: args
 termToJS env (CApp t args etas) f = termToJS env t (\ t' => (argsToJS t' args Lin f)) --  (f (Apply t' args'))))
   where
     etaExpand : JSEnv -> Nat -> SnocList JSExp -> JSExp -> JSExp
@@ -234,6 +244,7 @@ expToDoc (LitObject xs) = text "{" <+> folddoc (\ a e => a ++ text ", " <+/> e)
 
 expToDoc (LitString str) = text $ quoteString str
 expToDoc (LitInt i) = text $ show i
+expToDoc (Raw str) = text str
 -- TODO add precedence
 expToDoc (Apply x@(JLam _ _) xs) = text "(" ++ expToDoc x ++ text ")" ++ text "(" ++ nest 2 (commaSep (map expToDoc xs)) ++ text ")"
 expToDoc (Apply x xs) = expToDoc x ++ text "(" ++ nest 2 (commaSep (map expToDoc xs)) ++ text ")"
@@ -270,18 +281,17 @@ mkArgs : Nat -> List String -> List String
 mkArgs Z acc = acc
 mkArgs (S k) acc = mkArgs k ("h\{show k}" :: acc)
 
-dcon : QName -> Nat -> Doc
-dcon qn@(QN ns nm) Z = stmtToDoc $ JConst (show qn) $ LitObject (("tag", LitString nm) :: Nil)
-dcon qn@(QN ns nm) arity =
-  let args = mkArgs arity Nil
-      obj = ("tag", LitString nm) :: map (\x => (x, Var x)) args
-  in stmtToDoc $ JConst (show qn) (JLam args (JReturn (LitObject obj)))
-
 -- use iife to turn stmts into expr
 maybeWrap : JSStmt Return -> JSExp
 maybeWrap (JReturn exp) = exp
 maybeWrap stmt = Apply (JLam Nil stmt) Nil
 
+dcon : QName -> Int -> Doc
+dcon qn arity =
+  let ct = compileDCon qn arity
+      exp = maybeWrap $ termToJS emptyJSEnv ct JReturn
+  in stmtToDoc $ JConst (show qn) exp
+
 -- convert a Def to a Doc (compile to javascript)
 defToDoc : {{Ref2 Defs St}} → QName → Def → M Doc
 defToDoc name (Fn tm) = do
@@ -290,10 +300,10 @@ defToDoc name (Fn tm) = do
   let exp = maybeWrap $ termToJS emptyJSEnv ct JReturn
   pure $ text "const" <+> jsIdent (show name) <+> text "=" <+/> expToDoc exp ++ text ";"
 defToDoc name Axiom = pure $ text ""
-defToDoc name (DCon arity str) = pure $ dcon name (cast arity)
+defToDoc name (DCon arity _) = pure $ dcon name arity
-defToDoc name (TCon arity strs) = pure $ dcon name (cast arity)
+defToDoc name (TCon arity strs) = pure $ dcon name arity
-defToDoc name (PrimTCon arity) = pure $ dcon name (cast arity)
+defToDoc name (PrimTCon arity) = pure $ dcon name arity
-defToDoc name (PrimFn src _ _) = pure $ text "const" <+> jsIdent (show name) <+> text "=" <+> text src
+defToDoc name (PrimFn src _ _) = pure $ stmtToDoc $ JConst (show name) $ Raw src
 
 -- Collect the QNames used in a term
 getNames : Tm -> List QName -> List QName
@@ -368,6 +378,7 @@ process name = do
   let foo = MkRef ref -- for the autos below
   eraseEntries
   liftWhere
+  tailCallOpt
   entries <- readIORef ref
   let names = sortedNames entries name
   for names $ \ nm => case lookupMap nm entries of

src/Lib/CompileExp.newt

@@ -27,6 +27,7 @@ data CAlt : U where
 
 data CExp : U where
   CBnd : Int -> CExp
+  -- How is CLam different from CFun with one arg?
   CLam : Name -> CExp -> CExp
   CFun : List Name -> CExp -> CExp
   CApp : CExp -> List CExp -> Int -> CExp
@@ -37,6 +38,10 @@ data CExp : U where
   CLet : Name -> CExp -> CExp -> CExp
   CLetRec : Name -> CExp -> CExp -> CExp
   CErased : CExp
+  -- Data / type constructor
+  CConstr : Name -> List CExp -> CExp
+  -- Raw javascript for `pfunc`
+  CRaw : String -> CExp
 
 -- I'm counting Lam in the term for arity.  This matches what I need in
 -- code gen.
@@ -66,9 +71,14 @@ arityForName fc nm = do
 compileTerm : {{Ref2 Defs St}} → Tm -> M CExp
 
 -- need to eta out extra args, fill in the rest of the apps
+-- NOW - maybe eta here instead of Compile.newt, drop number on CApp
+-- The problem would be deBruijn. We have to put the app under CLam
+-- which would mess up all of the deBruijn (unless we push it out)
+
 apply : CExp -> List CExp -> SnocList CExp -> Nat -> M CExp
 -- out of args, make one up (fix that last arg)
-apply t Nil acc (S k) = pure $ CApp t (acc <>> Nil) (1 + cast k)
+apply t Nil acc (S k) =
+  pure $ CApp t (acc <>> Nil) (1 + cast k)
 apply t (x :: xs) acc (S k)  =  apply t xs (acc :< x) k
 -- once we hit zero, we fold the rest
 apply t ts acc Z = go (CApp t (acc <>> Nil) 0) ts
@@ -137,4 +147,9 @@ compileFun tm = go tm Lin
     go tm Lin = compileTerm tm
     go tm args = CFun (args <>> Nil) <$> compileTerm tm
 
-
+-- What are the Defs used for above? (Arity for name)
+compileDCon : QName → Int → CExp
+compileDCon (QN _ nm) 0 = CConstr nm Nil
+compileDCon (QN _ nm) arity =
+  let args = map (\k => "h\{show k}") (range 0 arity) in
+  CFun args $ CConstr nm $ map (\k => CBnd $ arity - k - 1) (range 0 arity)

src/Lib/Elab.newt

@@ -1144,9 +1144,6 @@ buildLitCases : Context -> Problem -> FC -> String -> Val -> M (List CaseAlt)
 buildLitCases ctx prob fc scnm scty = do
   let lits = nub $ getLits scnm prob.clauses
   alts <- traverse (buildLitCase ctx prob fc scnm scty) lits
-  -- TODO build default case
-  -- run getLits
-  -- buildLitCase for each
 
   let defclauses = filter isDefault prob.clauses
   when (length' defclauses == 0) $ \ _ => error fc "no default for literal slot on \{show scnm}"

src/Lib/ProcessDecl.newt

@@ -45,7 +45,7 @@ logMetas (Unsolved fc k ctx ty User cons :: rest) = do
       ty' <- quote ctx.lvl ty
       let names = map fst ctx.types
       env <- dumpEnv ctx
-      let msg = "\{env}  -----------\n  \{render 90 $ pprint names ty'}"
+      let msg = "\{env}\n  -----------\n  \{render 90 $ pprint names ty'}"
       info fc "User Hole\n\{msg}"
       logMetas rest
 logMetas (Unsolved fc k ctx ty kind cons :: rest) = do

src/Lib/TCO.newt

@@ -0,0 +1,44 @@
+module Lib.TCO
+
+import Prelude
+import Data.Graph
+import Lib.Ref2
+import Lib.Common
+import Lib.Types
+import Lib.CompileExp
+
+-- We need CompileExp here, so we know if it's
+-- fully applied, needs eta, etc.
+-- Maybe we should move Ref2 Defs over to CExp?
+-- But we'll need CExp for constructors, etc.
+-- I _could_ collect a stack and look up arity, but
+-- at the next stage, we'd need to fake up constructor
+-- records
+
+tailNames : CExp → List Name
+-- This is tricky, we need to skip the first CLam, but
+-- a deeper one is a return value
+tailNames (CApp (CRef name) args 0) = name :: Nil
+tailNames (CCase _ alts) = join $ map altTailNames alts
+  where
+    altTailNames : CAlt → List Name
+    altTailNames (CConAlt _ _ exp) = tailNames exp
+    altTailNames (CDefAlt exp) = tailNames exp
+    altTailNames (CLitAlt _ exp) = tailNames exp
+tailNames (CLet _ _ t) = tailNames t
+tailNames (CLetRec _ _ t) = tailNames t
+tailNames (CConstr _ args) = join $ map tailNames args
+tailNames (CBnd _) = Nil
+tailNames (CFun _ _) = Nil
+tailNames (CLam _ _) = Nil
+tailNames (CApp t args n) = Nil
+tailNames (CRef _) = Nil
+tailNames CErased = Nil
+tailNames (CLit _) = Nil
+tailNames (CMeta _) = Nil
+tailNames (CRaw _) = Nil
+
+tailCallOpt : {{Ref2 Defs St}} → M Unit
+tailCallOpt = do
+  defs <- getRef Defs
+  putStrLn "TODO TCO"

src/Monad/State.newt

@@ -0,0 +1,33 @@
+module Monad.State
+
+import Prelude
+
+record State s a where
+  constructor MkState
+  runState : s -> (a × s)
+
+get : ∀ s. State s s
+get = MkState (\s => (s, s))
+
+put : ∀ s. s -> State s Unit
+put s = MkState (\_ => (MkUnit, s))
+
+modify : ∀ s. (s → s) → State s Unit
+modify f = do
+  v <- get
+  put $ f v
+
+instance ∀ s. Functor (State s) where
+  map f (MkState run) = MkState (\s => let (a, s') = run s in (f a, s'))
+
+instance ∀ s. Applicative (State s) where
+  return x = MkState (\s => (x, s))
+  (MkState f) <*> (MkState x) = MkState (\s => let (g, s') = f s in
+                                               let (a, s'') = x s'
+                                               in (g a, s''))
+
+instance ∀ s. Monad (State s) where
+  pure x = MkState (\s => (x, s))
+  bind (MkState x) f = MkState (\s => let (a, s') = x s in
+                                     let (MkState y) = f a in
+                                     y s')

tests/Neighbors.newt

@@ -0,0 +1,51 @@
+-- https://www.youtube.com/watch?v=pNBPCnZEdSs
+module Neighbors
+
+-- Prf ?
+import Prelude
+
+data Void : U where
+
+data Prf : U → U where
+  Pf : ∀ a. {{_ : a}} → Prf a
+
+tryThis : ∀ A B. Prf A → Prf B → Prf A
+-- this needs help in newt
+tryThis (Pf {{x}}) b = Pf {_} {{x}}
+
+P : U
+
+data Bnd : U where
+  bot : Bnd
+  val : P → Bnd
+  top : Bnd
+
+Rel : U → U
+Rel a = a × a → U
+
+L : P × P → U
+
+-- FIXME Rel Bnd needs to be expanded
+-- LH LB : Rel Bnd → U
+LH LB : Bnd × Bnd → U
+LH (bot, _) = Unit
+LH (val x, val y) = L (x, y)
+LH _ = Void
+LB xy = Prf (LH xy)
+data Set : U where
+  SR SP : Set -- recursive / param
+  S0 S1 : Set -- empty, unit
+  _:+_ _:*_ : (S T : Set) → Set
+
+infixl 5 _:+_ _:*_
+SetF : Set → U → U
+SetF sr r = r
+SetF sr p = p
+SetF (s :+ t) r = SetF s r + SetF t r
+SetF (s :* t) r = SetF s r * SetF t r
+
+infixl 5 <_>
+data MuSet : Set → U where
+  <_> : ∀ t. SetF t (MuSet t) → MuSet t
+
+-- 9:30