From c951318b083bb7835a734b587cd4147a94c76d4d Mon Sep 17 00:00:00 2001
From: Victor Taelin <victor.taelin@gmail.com>
Date: Sun, 29 Sep 2024 15:35:41 -0300
Subject: [PATCH] allow labelled fields on ctors

---
 src/Kind/API.hs     |  2 +-
 src/Kind/Check.hs   | 24 +++++++++++-------------
 src/Kind/Compile.hs |  2 +-
 src/Kind/Equal.hs   | 16 +++-------------
 src/Kind/Parse.hs   | 26 ++++++++++++++++++++++++--
 src/Kind/Reduce.hs  | 16 ++++++----------
 src/Kind/Show.hs    |  6 +++++-
 src/Kind/Type.hs    |  2 +-
 8 files changed, 52 insertions(+), 42 deletions(-)

diff --git a/src/Kind/API.hs b/src/Kind/API.hs
index 5db895fe2..59074136e 100644
--- a/src/Kind/API.hs
+++ b/src/Kind/API.hs
@@ -116,7 +116,7 @@ getDeps term = case term of
   Slf _ typ bod -> getDeps typ ++ getDeps (bod Set)
   Ins val       -> getDeps val
   Dat scp cts   -> concatMap getDeps scp ++ concatMap getDepsCtr cts
-  Con _ arg     -> concatMap getDeps arg
+  Con _ arg     -> concatMap (getDeps . snd) arg
   Mat cse       -> concatMap (getDeps . snd) cse
   Let _ val bod -> getDeps val ++ getDeps (bod Set)
   Use _ val bod -> getDeps val ++ getDeps (bod Set)
diff --git a/src/Kind/Check.hs b/src/Kind/Check.hs
index df931da71..e3275ae69 100644
--- a/src/Kind/Check.hs
+++ b/src/Kind/Check.hs
@@ -56,7 +56,6 @@ infer term dep = debug ("infer: " ++ termShower False term dep) $ go term dep wh
         envLog (Error Nothing (Hol "self-type" []) vtyp (Ins val) dep)
         envFail
 
-  -- CHANGED: Updated Dat case to handle new Ctr structure with Tele
   go (Dat scp cts) dep = do
     forM_ cts $ \ (Ctr _ tele) -> do
       checkTele Nothing tele Set dep
@@ -151,7 +150,6 @@ check src val typ dep = debug ("check: " ++ termShower True val dep ++ "\n    ::
         infer (Ins val) dep
         return ()
 
-  -- CHANGED: Updated Con case to handle new Ctr structure with Tele
   go src val@(Con nam arg) typx dep = do
     book <- envGetBook
     fill <- envGetFill
@@ -168,7 +166,6 @@ check src val typ dep = debug ("check: " ++ termShower True val dep ++ "\n    ::
         infer (Con nam arg) dep
         return ()
 
-  -- CHANGED: Updated Mat case to handle new Ctr structure with Tele
   go src (Mat cse) typx dep = do
     book <- envGetBook
     fill <- envGetFill
@@ -256,7 +253,6 @@ check src val typ dep = debug ("check: " ++ termShower True val dep ++ "\n    ::
       envLog (Error src expected detected term dep)
       envFail
 
--- CHANGED: Added checkTele function
 checkTele :: Maybe Cod -> Tele -> Term -> Int -> Env ()
 checkTele src tele typ dep = case tele of
   TRet term -> check src term typ dep
@@ -264,28 +260,30 @@ checkTele src tele typ dep = case tele of
     check src inp Set dep
     checkTele src (bod (Ann False (Var nam dep) inp)) typ (dep + 1)
 
--- CHANGED: Added checkConAgainstTele function
-checkConAgainstTele :: Maybe Cod -> [Term] -> Tele -> Int -> Env ()
+checkConAgainstTele :: Maybe Cod -> [(Maybe String, Term)] -> Tele -> Int -> Env ()
 checkConAgainstTele src [] (TRet _) _ = return ()
-checkConAgainstTele src (arg:args) (TExt nam inp bod) dep = do
-  check src arg inp dep
+checkConAgainstTele src ((maybeField, arg):args) (TExt nam inp bod) dep = do
+  case maybeField of
+    Just field -> if field /= nam
+      then do
+        envLog (Error src (Hol ("expected:" ++ nam) []) (Hol ("detected:" ++ field) []) (Hol "field_mismatch" []) dep)
+        envFail
+      else check src arg inp dep
+    Nothing -> check src arg inp dep
   checkConAgainstTele src args (bod arg) dep
 checkConAgainstTele src _ _ dep = do
   envLog (Error src (Hol "constructor_arity_mismatch" []) (Hol "unknown_type" []) (Hol "constructor" []) dep)
   envFail
 
--- CHANGED: ....
 teleToType :: Tele -> Term -> Int -> Term
 teleToType (TRet _)           ret _   = ret
 teleToType (TExt nam inp bod) ret dep = All nam inp (\x -> teleToType (bod x) ret (dep + 1))
 
--- CHANGED: Helper function to extract both arguments and return type from a telescope
-teleToTerm :: Tele -> Int -> ([Term], Term)
+teleToTerm :: Tele -> Int -> ([(Maybe String, Term)], Term)
 teleToTerm tele dep = go tele [] dep where
   go (TRet ret)         args _   = (reverse args, ret)
-  go (TExt nam inp bod) args dep = go (bod (Var nam dep)) ((Var nam dep) : args) (dep + 1)
+  go (TExt nam inp bod) args dep = go (bod (Var nam dep)) ((Just nam, Var nam dep) : args) (dep + 1)
 
--- CHANGED: ...
 extractEqualities :: Term -> Term -> Int -> [(Int, Term)]
 extractEqualities (Dat as _) (Dat bs _) dep = zipWith go as bs where
   go (Var _ i) v = (i, v)
diff --git a/src/Kind/Compile.hs b/src/Kind/Compile.hs
index 79dd3027d..8a50fde8e 100644
--- a/src/Kind/Compile.hs
+++ b/src/Kind/Compile.hs
@@ -32,7 +32,7 @@ termToJS term dep = case term of
   Dat _ _ ->
     "null"
   Con nam arg ->
-    let arg' = map (\x -> termToJS x dep) arg
+    let arg' = map (\(f, x) -> termToJS x dep) arg
         fds' = concat (zipWith (\i x -> concat [", x", show i, ": ", x]) [0..] arg')
     in concat ["{$: \"", nameToJS nam, "\", length: ", show (length arg), fds', "}"]
   Mat cse ->
diff --git a/src/Kind/Equal.hs b/src/Kind/Equal.hs
index e5876d4d2..897ccf64c 100644
--- a/src/Kind/Equal.hs
+++ b/src/Kind/Equal.hs
@@ -1,5 +1,3 @@
--- //./Type.hs//
-
 module Kind.Equal where
 
 import Control.Monad (zipWithM)
@@ -55,7 +53,6 @@ identical a b dep = do
     identical aVal b dep
   go a (Ins bVal) dep =
     identical a bVal dep
-  -- CHANGED: Updated Dat case to handle new Ctr structure with Tele
   go (Dat aScp aCts) (Dat bScp bCts) dep = do
     iSlf <- zipWithM (\ax bx -> identical ax bx dep) aScp bScp
     if and iSlf && length aCts == length bCts
@@ -63,7 +60,7 @@ identical a b dep = do
       else return False
   go (Con aNam aArg) (Con bNam bArg) dep = do
     if aNam == bNam && length aArg == length bArg
-      then and <$> zipWithM (\aArg bArg -> identical aArg bArg dep) aArg bArg
+      then and <$> zipWithM (\(_, aVal) (_, bVal) -> identical aVal bVal dep) aArg bArg
       else return False
   go (Mat aCse) (Mat bCse) dep = do
     if length aCse == length bCse
@@ -124,7 +121,6 @@ identical a b dep = do
   go a b dep =
     return False
 
-  -- CHANGED: Updated goCtr to handle new Ctr structure with Tele
   goCtr (Ctr aCNm aTele) (Ctr bCNm bTele) = do
     if aCNm == bCNm
       then goTele aTele bTele dep
@@ -135,7 +131,6 @@ identical a b dep = do
       then identical aCBod bCBod dep
       else return False
 
-  -- CHANGED: Added goTele function to handle Tele equality
   goTele :: Tele -> Tele -> Int -> Env Bool
   goTele (TRet aTerm) (TRet bTerm) dep = identical aTerm bTerm dep
   goTele (TExt aNam aTyp aBod) (TExt bNam bTyp bBod) dep = do
@@ -160,7 +155,6 @@ similar a b dep = go a b dep where
   go (Slf aNam aTyp aBod) (Slf bNam bTyp bBod) dep = do
     book <- envGetBook
     similar (reduce book IM.empty 0 aTyp) (reduce book IM.empty 0 bTyp) dep
-  -- CHANGED: Updated Dat case to handle new Ctr structure with Tele
   go (Dat aScp aCts) (Dat bScp bCts) dep = do
     eSlf <- zipWithM (\ax bx -> equal ax bx dep) aScp bScp
     if and eSlf && length aCts == length bCts
@@ -168,7 +162,7 @@ similar a b dep = go a b dep where
       else return False
   go (Con aNam aArg) (Con bNam bArg) dep = do
     if aNam == bNam && length aArg == length bArg
-      then and <$> zipWithM (\a b -> equal a b dep) aArg bArg
+      then and <$> zipWithM (\(_, aVal) (_, bVal) -> equal aVal bVal dep) aArg bArg
       else return False
   go (Mat aCse) (Mat bCse) dep = do
     if length aCse == length bCse
@@ -184,7 +178,6 @@ similar a b dep = go a b dep where
     return (eZer && eSuc)
   go a b dep = identical a b dep
 
-  -- CHANGED: Updated goCtr to handle new Ctr structure with Tele
   goCtr (Ctr aCNm aTele) (Ctr bCNm bTele) = do
     if aCNm == bCNm
       then goTele aTele bTele dep
@@ -195,7 +188,6 @@ similar a b dep = go a b dep where
       then equal aCBod bCBod dep
       else return False
 
-  -- CHANGED: Added goTele function to handle Tele similarity
   goTele :: Tele -> Tele -> Int -> Env Bool
   goTele (TRet aTerm) (TRet bTerm) dep = equal aTerm bTerm dep
   goTele (TExt aNam aTyp aBod) (TExt bNam bTyp bBod) dep = do
@@ -273,13 +265,12 @@ occur book fill uid term dep = go term dep where
   go (Ins val) dep =
     let o_val = go val dep
     in o_val
-  -- CHANGED: Updated Dat case to handle new Ctr structure with Tele
   go (Dat scp cts) dep =
     let o_scp = any (\x -> go x dep) scp
         o_cts = any (\(Ctr _ tele) -> goTele tele dep) cts
     in o_scp || o_cts
   go (Con nam arg) dep =
-    any (\x -> go x dep) arg
+    any (\(_, x) -> go x dep) arg
   go (Mat cse) dep =
     any (\ (_, cbod) -> go cbod dep) cse
   go (Let nam val bod) dep =
@@ -310,7 +301,6 @@ occur book fill uid term dep = go term dep where
   go _ dep =
     False
 
-  -- CHANGED: Added goTele function to handle Tele occurrence check
   goTele :: Tele -> Int -> Bool
   goTele (TRet term) dep = go term dep
   goTele (TExt nam typ bod) dep =
diff --git a/src/Kind/Parse.hs b/src/Kind/Parse.hs
index 2e8cd86af..fb2078a7d 100644
--- a/src/Kind/Parse.hs
+++ b/src/Kind/Parse.hs
@@ -208,15 +208,37 @@ parseTele = do
   ret <- parseTerm
   return $ foldr (\(nam, typ) acc -> TExt nam typ (\x -> acc)) (TRet ret) fields
 
+-- parseCon = withSrc $ do
+  -- P.char '#'
+  -- nam <- parseName
+  -- parseTrivia
+  -- P.char '{'
+  -- arg <- P.many $ P.try $ parseTerm
+  -- parseTrivia
+  -- P.char '}'
+  -- return $ Con nam arg
+   
 parseCon = withSrc $ do
   P.char '#'
   nam <- parseName
   parseTrivia
   P.char '{'
-  arg <- P.many $ P.try $ parseTerm
+  parseTrivia
+  args <- P.sepBy parseConArg (P.char ',' >> parseTrivia)
   parseTrivia
   P.char '}'
-  return $ Con nam arg
+  return $ Con nam args
+
+parseConArg :: Parser (Maybe String, Term)
+parseConArg = do
+  maybeField <- P.optionMaybe $ do
+    field <- parseName
+    parseTrivia
+    P.char ':'
+    parseTrivia
+    return field
+  term <- parseTerm
+  return (maybeField, term)
 
 parseSwi = withSrc $ do
   P.try $ do
diff --git a/src/Kind/Reduce.hs b/src/Kind/Reduce.hs
index 5215bcf75..cf3a0fb6d 100644
--- a/src/Kind/Reduce.hs
+++ b/src/Kind/Reduce.hs
@@ -16,7 +16,7 @@ import qualified Data.IntMap.Strict as IM
 -- Evaluates a term to weak normal form
 -- 'lv' defines when to expand refs: 0 = never, 1 = on redexes
 reduce :: Book -> Fill -> Int -> Term -> Term
-reduce book fill lv term = {-trace (termShower False term 0) $-} red term where
+reduce book fill lv term = red term where
 
   red (App fun arg)     = app (red fun) arg
   red (Ann chk val typ) = red val
@@ -39,7 +39,7 @@ reduce book fill lv term = {-trace (termShower False term 0) $-} red term where
   app fun           arg = App fun arg
 
   mat cse (Con cnam carg) = case lookup cnam cse of
-    Just cx -> red (foldl App cx carg)
+    Just cx -> red (foldl App cx (map snd carg))
     Nothing -> error $ "Constructor " ++ cnam ++ " not found in pattern match."
   mat cse arg = App (Mat cse) arg
 
@@ -107,7 +107,6 @@ normal book fill lv term dep = go (reduce book fill lv term) dep where
   go (Ins val) dep =
     let nf_val = normal book fill lv val dep in
     Ins nf_val
-  -- CHANGED: Updated Dat case to handle new Ctr structure with Tele
   go (Dat scp cts) dep =
     let go_ctr = (\ (Ctr nm tele) ->
           let nf_tele = normalTele book fill lv tele dep in
@@ -116,7 +115,7 @@ normal book fill lv term dep = go (reduce book fill lv term) dep where
     let nf_cts = map go_ctr cts in
     Dat nf_scp nf_cts
   go (Con nam arg) dep =
-    let nf_arg = map (\a -> normal book fill lv a dep) arg in
+    let nf_arg = map (\(f, t) -> (f, normal book fill lv t dep)) arg in
     Con nam nf_arg
   go (Mat cse) dep =
     let nf_cse = map (\(cnam, cbod) -> (cnam, normal book fill lv cbod dep)) cse in
@@ -150,7 +149,6 @@ normal book fill lv term dep = go (reduce book fill lv term) dep where
     Src src nf_val
   go (Met uid spn) dep = Met uid spn -- TODO: normalize spine
 
--- CHANGED: Added normalTele function
 normalTele :: Book -> Fill -> Int -> Tele -> Int -> Tele
 normalTele book fill lv tele dep = case tele of
   TRet term ->
@@ -188,7 +186,6 @@ bind (Slf nam typ bod) ctx =
 bind (Ins val) ctx =
   let val' = bind val ctx in
   Ins val'
--- CHANGED: Updated Dat case to handle new Ctr structure with Tele
 bind (Dat scp cts) ctx =
   let scp' = map (\x -> bind x ctx) scp in
   let cts' = map (\x -> bindCtr x ctx) cts in
@@ -198,7 +195,7 @@ bind (Dat scp cts) ctx =
     bindTele (TRet term)        ctx = TRet (bind term ctx)
     bindTele (TExt nam typ bod) ctx = TExt nam (bind typ ctx) $ \x -> bindTele (bod x) ((nam, x) : ctx)
 bind (Con nam arg) ctx =
-  let arg' = map (\x -> bind x ctx) arg in
+  let arg' = map (\(f, x) -> (f, bind x ctx)) arg in
   Con nam arg'
 bind (Mat cse) ctx =
   let cse' = map (\(cn,cb) -> (cn, bind cb ctx)) cse in
@@ -268,7 +265,7 @@ genMetas term = fst (go term 0) where
         (cts', c2) = foldr (\(Ctr nm tele) (acc, c') -> let (tele', c'') = goTele tele c' in (Ctr nm tele' : acc, c'')) ([], c1) cts
     in (Dat scp' cts', c2)
   go (Con nam arg) c = 
-    let (arg', c1) = foldr (\t (acc, c') -> let (t', c'') = go t c' in (t':acc, c'')) ([], c) arg
+    let (arg', c1) = foldr (\(f, t) (acc, c') -> let (t', c'') = go t c' in ((f, t'):acc, c'')) ([], c) arg
     in (Con nam arg', c1)
   go (Mat cse) c = 
     let (cse', c1) = foldr (\(cn, cb) (acc, c') -> let (cb', c'') = go cb c' in ((cn, cb'):acc, c'')) ([], c) cse
@@ -318,9 +315,8 @@ subst lvl neo term = go term where
   go (Ann chk val typ) = Ann chk (go val) (go typ)
   go (Slf nam typ bod) = Slf nam (go typ) (\x -> go (bod x))
   go (Ins val)         = Ins (go val)
-  -- CHANGED: Updated Dat case to handle new Ctr structure with Tele
   go (Dat scp cts)     = Dat (map go scp) (map goCtr cts)
-  go (Con nam arg)     = Con nam (map go arg)
+  go (Con nam arg)     = Con nam (map (\(f, t) -> (f, go t)) arg)
   go (Mat cse)         = Mat (map goCse cse)
   go (Swi zer suc)     = Swi (go zer) (go suc)
   go (Ref nam)         = Ref nam
diff --git a/src/Kind/Show.hs b/src/Kind/Show.hs
index df03a2cea..8a0e98426 100644
--- a/src/Kind/Show.hs
+++ b/src/Kind/Show.hs
@@ -53,8 +53,12 @@ termShower small term dep = case term of
           "#" ++ nm ++ " " ++ teleShower small tele dep) cts)
     in concat ["#[", scp', "]{ ", cts', " }"]
   Con nam arg ->
-    let arg' = unwords (map (\x -> termShower small x dep) arg)
+    let arg' = unwords (map showArg arg)
     in concat ["#", nam, "{", arg', "}"]
+    where
+      showArg (maybeField, term) = case maybeField of
+        Just field -> field ++ ": " ++ termShower small term dep
+        Nothing -> termShower small term dep
   Mat cse ->
     let cse' = unwords (map (\(cnm, cbod) -> "#" ++ cnm ++ ": " ++ termShower small cbod dep) cse)
     in concat ["λ{ ", cse', " }"]
diff --git a/src/Kind/Type.hs b/src/Kind/Type.hs
index e00aad638..d408fddb6 100644
--- a/src/Kind/Type.hs
+++ b/src/Kind/Type.hs
@@ -29,7 +29,7 @@ data Term
   | Dat [Term] [Ctr]
 
   -- Constructor: #CN { x0 x1 ... }
-  | Con String [Term]
+  | Con String [(Maybe String, Term)]
 
   -- Match: λ{ #C0:B0 #C1:B1 ... }
   | Mat [(String, Term)]