From 889eafdee3c08e658193f704015455056bce8e6c Mon Sep 17 00:00:00 2001
From: Victor Taelin <victor.taelin@gmail.com>
Date: Thu, 17 Oct 2024 22:24:44 -0300
Subject: [PATCH] Nat, List, String syntax sugars

- #1 desugars to #Succ{#Zero{}}

- "abc" desugars to #Cons{'a' #Cons{'b' #Cons{'c' #Nil{}}}}

- [1 2 3] desugars to #Cons{1 #Cons{2 #Cons{3 #Nil{}}}}

note that this is type agnostic, so, one could use these sugars for
different types (ex: Fin, Vector, Text, etc.)
---
 src/Kind/Check.hs   | 21 +++++++++++++++------
 src/Kind/Compile.hs |  4 ++++
 src/Kind/Equal.hs   |  6 ++++++
 src/Kind/Parse.hs   | 31 +++++++++++++++++++++++++++++--
 src/Kind/Reduce.hs  | 25 ++++++++++++++++++++-----
 src/Kind/Show.hs    |  3 ++-
 src/Kind/Type.hs    |  3 +++
 7 files changed, 79 insertions(+), 14 deletions(-)

diff --git a/src/Kind/Check.hs b/src/Kind/Check.hs
index 10972632a..e926ded29 100644
--- a/src/Kind/Check.hs
+++ b/src/Kind/Check.hs
@@ -78,12 +78,6 @@ infer term dep = debug ("infer: " ++ termShower False term dep) $ go term dep wh
   go (Num num) dep = do
     return U32
 
-  go (Txt txt) dep = do
-    return (Ref "Base/String/String")
-
-  go (Nat val) dep = do
-    return (Ref "Base/Nat/Nat")
-
   go (Op2 opr fst snd) dep = do
     envSusp (Check Nothing fst U32 dep)
     envSusp (Check Nothing snd U32 dep)
@@ -236,6 +230,21 @@ check src val typ dep = debug ("check: " ++ termShower True val dep ++ "\n    ::
   go src (Met uid spn) typx dep = do
     return ()
 
+  go src tm@(Txt txt) typx dep = do
+    book <- envGetBook
+    fill <- envGetFill
+    go src (reduce book fill 2 tm) typx dep
+
+  go src tm@(Nat val) typx dep = do
+    book <- envGetBook
+    fill <- envGetFill
+    go src (reduce book fill 2 tm) typx dep
+
+  go src tm@(Lst lst) typx dep = do
+    book <- envGetBook
+    fill <- envGetFill
+    go src (reduce book fill 2 tm) typx dep
+
   go src (Ann chk val typ) typx dep = do
     cmp src val typ typx dep
     if chk then do
diff --git a/src/Kind/Compile.hs b/src/Kind/Compile.hs
index 8a50fde8e..4027c360c 100644
--- a/src/Kind/Compile.hs
+++ b/src/Kind/Compile.hs
@@ -5,6 +5,8 @@ import Kind.Reduce
 
 import qualified Data.Map.Strict as M
 import qualified Data.IntMap.Strict as IM
+import Data.List (intercalate)
+
 
 import Prelude hiding (EQ, LT, GT)
 
@@ -66,6 +68,8 @@ termToJS term dep = case term of
     in concat ["((x => x === 0 ? ", zer', " : ", suc', "(x - 1)))"]
   Txt txt ->
     show txt
+  Lst lst ->
+    "[" ++ intercalate " " (map (\x -> termToJS x dep) lst) ++ "]"
   Nat val ->
     show val
   Hol _ _ ->
diff --git a/src/Kind/Equal.hs b/src/Kind/Equal.hs
index f319db4e2..338707c28 100644
--- a/src/Kind/Equal.hs
+++ b/src/Kind/Equal.hs
@@ -110,6 +110,8 @@ identical a b dep = do
     return (iZer && iSuc)
   go (Txt aTxt) (Txt bTxt) dep =
     return (aTxt == bTxt)
+  go (Lst aLst) (Lst bLst) dep =
+    and <$> zipWithM (\a b -> identical a b dep) aLst bLst
   go (Nat aVal) (Nat bVal) dep =
     return (aVal == bVal)
   go (Src aSrc aVal) b dep =
@@ -379,6 +381,8 @@ same (Swi aZer aSuc) (Swi bZer bSuc) dep =
   same aZer bZer dep && same aSuc bSuc dep
 same (Txt aTxt) (Txt bTxt) dep =
   aTxt == bTxt
+same (Lst aLst) (Lst bLst) dep =
+  length aLst == length bLst && and (zipWith (\a b -> same a b dep) aLst bLst)
 same (Nat aVal) (Nat bVal) dep =
   aVal == bVal
 same (Src aSrc aVal) b dep =
@@ -435,6 +439,7 @@ subst lvl neo term = go term where
   go (Num n)           = Num n
   go (Op2 opr fst snd) = Op2 opr (go fst) (go snd)
   go (Txt txt)         = Txt txt
+  go (Lst lst)         = Lst (map go lst)
   go (Nat val)         = Nat val
   go (Var nam idx)     = if lvl == idx then neo else Var nam idx
   go (Src src val)     = Src src (go val)
@@ -466,6 +471,7 @@ replace old neo term dep = if same old term dep then neo else go term where
   go (Num n)            = Num n
   go (Op2 opr fst snd)  = Op2 opr (replace old neo fst dep) (replace old neo snd dep)
   go (Txt txt)          = Txt txt
+  go (Lst lst)          = Lst (map (\x -> replace old neo x dep) lst)
   go (Nat val)          = Nat val
   go (Var nam idx)      = Var nam idx
   go (Src src val)      = Src src (replace old neo val dep)
diff --git a/src/Kind/Parse.hs b/src/Kind/Parse.hs
index 3d51d5444..4d52875b3 100644
--- a/src/Kind/Parse.hs
+++ b/src/Kind/Parse.hs
@@ -1,3 +1,5 @@
+-- //./Type.hs//
+
 module Kind.Parse where
 
 import Debug.Trace
@@ -131,6 +133,7 @@ parseTerm = (do
     , parseSlf
     , parseIns
     , parseDat
+    , parseNat -- sugar
     , parseCon
     , parseUse
     , parseLet
@@ -138,8 +141,9 @@ parseTerm = (do
     , parseMatch -- sugar
     , parseSet
     , parseNum
-    , parseTxt
-    , parseChr
+    , parseTxt -- sugar
+    , parseLst -- sugar
+    , parseChr -- sugar
     , parseHol
     , parseMet
     , parseRef
@@ -308,6 +312,12 @@ parseTxt = withSrc $ do
   char '"'
   return $ Txt txt
 
+parseLst = withSrc $ do
+  char '['
+  elems <- P.many parseTerm
+  char ']'
+  return $ Lst elems
+
 parseChr = withSrc $ do
   char '\''  
   chr <- parseEscaped <|> noneOf "'\\"
@@ -431,6 +441,9 @@ expandUses uses name =
 
 -- TODO: rewrite the code above to apply the expand-uses functionality to the generated refs. also, append just "bind" and "pure" (instad of "/Monad/bind" etc.)
 
+-- Do-Notation:
+-- ------------
+
 data DoBlck = DoBlck String [DoStmt] Bool Term -- bool used for wrap
 data DoStmt = DoBind String Term | DoSeq Term
 
@@ -483,6 +496,9 @@ desugarDo (DoBlck name stmts wrap ret) = do
 parseDo :: Parser Term
 parseDo = parseDoSugar >>= desugarDo
 
+-- Match
+-- -----
+
 -- Let's now implement the 'parseMatch' sugar. The following syntax:
 -- 'match x { #Foo: foo #Bar: bar ... }'
 -- desugars to:
@@ -502,3 +518,14 @@ parseMatch = withSrc $ do
     return (cnam, cbod)
   char '}'
   return $ App (Mat cse) x
+
+-- Match
+-- -----
+
+-- Nat: the '#123' expression is parsed into (Nat 123)
+
+parseNat :: Parser Term
+parseNat = withSrc $ P.try $ do
+  char '#'
+  num <- P.many1 digit
+  return $ Nat (read num)
diff --git a/src/Kind/Reduce.hs b/src/Kind/Reduce.hs
index 685b98da8..4e25db901 100644
--- a/src/Kind/Reduce.hs
+++ b/src/Kind/Reduce.hs
@@ -10,6 +10,10 @@ import Kind.Show
 import qualified Data.Map.Strict as M
 import qualified Data.IntMap.Strict as IM
 
+-- for exitting on undefined ref (should be handled better)
+import System.Exit (exitWith, ExitCode(ExitFailure))
+import System.IO.Unsafe (unsafePerformIO)
+
 -- Evaluation
 -- ----------
 
@@ -26,6 +30,7 @@ reduce book fill lv term = red term where
   red (Use nam val bod) = red (bod (red val))
   red (Op2 opr fst snd) = op2 opr (red fst) (red snd)
   red (Txt val)         = txt val
+  red (Lst val)         = lst val
   red (Nat val)         = nat val
   red (Src src val)     = red val
   red (Met uid spn)     = met uid spn
@@ -76,14 +81,18 @@ reduce book fill lv term = red term where
 
   ref nam | lv > 0 = case M.lookup nam book of
     Just val -> red val
-    Nothing  -> error $ "Undefined reference: " ++ nam
+    Nothing  -> trace ("Undefined reference: " ++ nam) (unsafePerformIO $ exitWith $ ExitFailure 1)
   ref nam = Ref nam
 
-  txt []     = red (Ref "Base/String/cons")
-  txt (x:xs) = red (App (App (Ref "Base/String/nil") (Num (toEnum (ord x)))) (Txt xs))
+  txt []     = red (Con "Nil" [])
+  txt (x:xs) = red (Con "Cons" [(Nothing, Num (toEnum (ord x))), (Nothing, Txt xs)])
+
+  lst []     = red (Con "Nil" [])
+  lst (x:xs) = red (Con "Cons" [(Nothing, x), (Nothing, Lst xs)])
+  
+  nat 0 = Con "Zero" []
+  nat n = Con "Succ" [(Nothing, Nat (n - 1))]
 
-  nat 0 = Ref "Base/Nat/zero"
-  nat n = App (Ref "Base/Nat/succ") (nat (n - 1))
 
 -- Normalization
 -- -------------
@@ -147,6 +156,9 @@ normal book fill lv term dep = go (reduce book fill lv term) dep where
     let nf_snd = normal book fill lv snd dep in
     Op2 opr nf_fst nf_snd
   go (Txt val) dep = Txt val
+  go (Lst val) dep =
+    let nf_val = map (\x -> normal book fill lv x dep) val in
+    Lst nf_val
   go (Nat val) dep = Nat val
   go (Var nam idx) dep = Var nam idx
   go (Src src val) dep =
@@ -229,6 +241,9 @@ bind (Op2 opr fst snd) ctx =
   let snd' = bind snd ctx in
   Op2 opr fst' snd'
 bind (Txt txt) ctx = Txt txt
+bind (Lst lst) ctx =
+  let lst' = map (\x -> bind x ctx) lst in
+  Lst lst'
 bind (Nat val) ctx = Nat val
 bind (Hol nam ctxs) ctx = Hol nam (reverse (map snd ctx))
 bind (Met uid spn) ctx = Met uid []
diff --git a/src/Kind/Show.hs b/src/Kind/Show.hs
index 8a0e98426..ea46ae0d3 100644
--- a/src/Kind/Show.hs
+++ b/src/Kind/Show.hs
@@ -88,7 +88,8 @@ termShower small term dep = case term of
         succ' = termShower small succ dep
     in concat ["λ{ 0: ", zero', " _: ", succ', " }"]
   Txt txt -> concat ["\"" , txt , "\""]
-  Nat val -> show val
+  Lst lst -> concat ["[", unwords (map (\x -> termShower small x dep) lst), "]"]
+  Nat val -> concat ["#", (show val)]
   Hol nam ctx -> concat ["?" , nam]
   Met uid spn -> concat ["_", show uid, "[", strSpn spn dep, " ]"]
   Var nam idx -> nam
diff --git a/src/Kind/Type.hs b/src/Kind/Type.hs
index 81bc80594..0845e7b94 100644
--- a/src/Kind/Type.hs
+++ b/src/Kind/Type.hs
@@ -74,6 +74,9 @@ data Term
   -- Text Literal (sugar)
   | Txt String
 
+  -- List Literal (sugar)
+  | Lst [Term]
+
   -- Nat Literal (sugar)
   | Nat Integer