tons of stuff

.gitignore

@@ -19,3 +19,5 @@ cabal.project.local*
 .DS_Store
 .holefill
 .tmp
+.backup/
+*.koder

book/Bool.kind

@@ -0,0 +1,4 @@
+Bool : * = #[]{
+  #false{} : Bool
+  #true{} : Bool
+}

book/Equal.kind

@@ -0,0 +1,14 @@
+// Defines propositional equality between two values of the same type.
+// - A: The type of the values being compared.
+// - a: The first value.
+// - b: The second value.
+// Constructor:
+// - refl: Represents reflexivity, i.e., that `a` equals itself.
+Equal
+: ∀(A: *)
+  ∀(a: A)
+  ∀(b: A)
+  *
+= λA λa λb #[]{
+  #refl{} : (Equal A a a)
+}

book/Equal/apply.kind

@@ -0,0 +1,19 @@
+// Applies a function to both sides of an equality proof.
+// - A: The type of the compared values.
+// - B: The type of the compared values after applying the function.
+// - a: The first compared value.
+// - b: The second compared value.
+// - f: The function to apply to both sides of the equality.
+// - e: The proof of equality between `a` and `b`.
+// = A proof that `(f a)` is equal to `(f b)`.
+Equal/apply
+: ∀(A: *)
+  ∀(B: *)
+  ∀(a: A)
+  ∀(b: A)
+  ∀(f: ∀(x: A) B)
+  ∀(e: (Equal A a b))
+  (Equal B (f a) (f b))
+= λA λB λa λb λf λ{
+  #refl: #refl{}
+}

book/Equal/refl.kind

@@ -0,0 +1,10 @@
+// Constructs a proof of reflexivity for propositional equality.
+// - A: The type of the value.
+// - x: The value for which to construct the reflexivity proof.
+// = A proof that `x` is equal to itself.
+Equal/refl
+: ∀(A: *)
+  ∀(x: A)
+  (Equal A x x)
+= λA λx
+  #refl{}

book/Equal/rewrite.kind

@@ -0,0 +1,13 @@
+Equal/rewrite
+
+: ∀(T: *)
+  ∀(a: T)
+  ∀(b: T)
+  ∀(e: (Equal T a b))
+  ∀(P: ∀(x: A) *)
+  ∀(x: (P a))
+  (P b)
+  
+= λT λa λb λ{
+  #refl: λP λx x
+}

book/List.kind

@@ -0,0 +1,12 @@
+// Defines a generic list datatype.
+// - A: The type of elements in the list.
+// Constructors:
+// - nil: Represents an empty list.
+// - cons: Adds an element to the front of a list.
+List
+: ∀(A: *)
+  *
+= λA #[]{
+  #nil{} : (List A)
+  #cons{ head:A tail:(List A) } : (List A)
+}

book/List/cons.kind

@@ -0,0 +1,12 @@
+// Constructs a new list by adding an element to the front of an existing list.
+// - A: The type of elements in the list.
+// - head: The element to add to the front of the list.
+// - tail: The current list.
+// = A new list with `head` as its 1st element, followed by the elements of `tail`.
+List/cons
+: ∀(A: *)
+  ∀(head: A)
+  ∀(tail: (List A))
+  (List A)
+= λA λhead λtail
+  #cons{head tail}

book/List/map.kind

@@ -0,0 +1,20 @@
+// Applies a function to each element of a list.
+// - A: The type of elements in the input list.
+// - B: The type of elements in the output list.
+// - xs: The input list.
+// - fn: The function to apply to each element.
+// = A new list with the function applied to each element of the input list.
+List/map
+: ∀(A: *)
+  ∀(B: *)
+  ∀(xs: (List A))
+  ∀(fn: ∀(x: A) B)
+  (List B)
+= λA λB λ{
+  #nil: λfn
+    #nil{}
+  #cons: λxs.head λxs.tail λfn
+    let head = (fn xs.head)
+    let tail = (List/map A B xs.tail fn)
+    #cons{head tail}
+}

book/List/nil.kind

@@ -0,0 +1,8 @@
+// Constructs an empty list.
+// - A: The type of elements in the list.
+// = An empty list of type `(List A)`.
+List/nil
+: ∀(A: *)
+  (List A)
+= λA
+  #nil{}

book/Nat.kind

@@ -1,4 +1,9 @@
-Nat : * = #[]{
+// Defines the natural numbers (nat) as an inductive datatype.
+// - succ: Represents the successor of a nat (x+1).
+// - zero: Represents the natural nat (0).
+Nat
+: *
+= #[]{
   #zero{} : Nat
-  #succ{ pred: Nat } : Nat
+  #succ{ pred:Nat } : Nat
 }

book/Nat/add.kind

@@ -0,0 +1,12 @@
+// Adds two natural numbers
+// - a: The 1st nat.
+// - b: The 2nd nat.
+// = The sum of `a` and `b`
+Nat/add
+: ∀(a: Nat)
+  ∀(b: Nat)
+  Nat
+= λ{
+  #zero: λb b
+  #succ: λa.pred λb #succ{(Nat/add a.pred b)}
+}

book/Nat/equal.kind

@@ -0,0 +1,18 @@
+// Checks if two natural numbers are equal.
+// - a: The 1st nat.
+// - b: The 2nt nat.
+// = True if `a` and `b` are equal.
+Nat/equal
+: ∀(a: Nat)
+  ∀(b: Nat)
+  Bool
+= λ{
+  #zero: λ{
+    #zero: #true{}
+    #succ: λb.pred #false{}
+  }
+  #succ: λa.pred λ{
+    #zero: #false{}
+    #succ: λb.pred (Nat/equal a.pred b.pred)
+  }
+}

book/Nat/id.kind

@@ -0,0 +1,7 @@
+Nat/id
+: ∀(a: Nat)
+  Nat
+= λ{
+  #zero: #zero{}
+  #succ: λa.pred (Nat/id a.pred)
+}

book/Nat/mul.kind

@@ -0,0 +1,13 @@
+// Multiplies two natural numbers
+// - a: The 1st nat.
+// - b: The 2nd nat.
+// = The product of `a` and `b`
+Nat/mul
+: ∀(a: Nat)
+  ∀(b: Nat)
+  Nat
+= λ{
+  #zero: λb #zero{}
+  #succ: λa.pred λb
+    (Nat/add b (Nat/mul a.pred b))
+}

book/Nat/succ.kind

@@ -0,0 +1,8 @@
+// Constructs the successor of a natural number.
+// - n: The natural number to which we add 1.
+// = The successor of the nat `n`.
+Nat/succ
+: ∀(n: Nat)
+  Nat
+= λn
+  #succ{n}

book/Nat/zero.kind

@@ -0,0 +1,5 @@
+// Represents the zero natural number.
+// = The nat 0.
+Nat/zero
+: Nat
+= #zero{}

book/U32/sum.kind

@@ -0,0 +1,10 @@
+U32/sum
+
+: ∀(x: U32)
+  U32
+
+= λ{
+  0: 0
+  _: λx.pred (+ x.pred (U32/sum x.pred))
+}
+

book/main.kind

@@ -1,3 +1,3 @@
 main
-: U32
-= (U32/sum 10)
+: Nat
+= (Nat/mul #succ{#succ{#succ{#zero{}}}} #succ{#succ{#zero{}}})

src/Kind/API.hs

@@ -36,12 +36,8 @@ extractName :: FilePath -> String -> String
 extractName basePath = dropBasePath . dropExtension where
   dropExtension path
     | "kind" `isExtensionOf` path = System.FilePath.dropExtension path
-    | otherwise = path
-  dropBasePath path = maybe path id (stripPrefix basePath path)
-
--- Resolves an input to a definition name
-resolveName :: FilePath -> String -> String
-resolveName = extractName
+    | otherwise                   = path
+  dropBasePath path = maybe path id (stripPrefix (basePath++"/") path)
 
 -- Loads a file and its dependencies into the book
 apiLoad :: FilePath -> Book -> String -> IO Book
@@ -152,13 +148,13 @@ main = do
 
 runCommand :: FilePath -> (Book -> String -> IO ()) -> String -> IO ()
 runCommand basePath cmd input = do
-  let name = resolveName basePath input
+  let name = extractName basePath input
   book <- apiLoad basePath M.empty name
   cmd book name
 
 runDeps :: FilePath -> String -> IO ()
 runDeps basePath input = do
-  let name = resolveName basePath input
+  let name = extractName basePath input
   book <- apiLoad basePath M.empty name
   let deps = S.toList $ getAllDeps book name
   forM_ deps $ \dep -> putStrLn dep

src/Kind/Check.hs

@@ -16,7 +16,7 @@ import Debug.Trace
 -- -------------
 
 infer :: Term -> Int -> Env Term
-infer term dep = go term dep where
+infer term dep = debug ("infer: " ++ termShower False term dep) $ go term dep where
   go (All nam inp bod) dep = do
     envSusp (Check Nothing inp Set dep)
     envSusp (Check Nothing (bod (Ann False (Var nam dep) inp)) Set (dep + 1))
@@ -130,7 +130,7 @@ infer term dep = go term dep where
     infer val dep
 
 check :: Maybe Cod -> Term -> Term -> Int -> Env ()
-check src val typ dep = go src val typ dep where
+check src val typ dep = debug ("check: " ++ termShower True val dep ++ "\n    :: " ++ termShower True typ dep) $ go src val typ dep where
   go src (Lam nam bod) typx dep = do
     book <- envGetBook
     fill <- envGetFill

src/Kind/Equal.hs

@@ -5,17 +5,17 @@ import Control.Monad (zipWithM)
 import Kind.Type
 import Kind.Env
 import Kind.Reduce
+import Kind.Show
 
 import qualified Data.Map.Strict as M
 import qualified Data.IntMap.Strict as IM
-import Debug.Trace
 
 -- Equality
 -- --------
 
 -- Checks if two terms are equal, after reduction steps
 equal :: Term -> Term -> Int -> Env Bool
-equal a b dep = do
+equal a b dep = debug ("== " ++ termShower False a dep ++ "\n.. " ++ termShower False b dep) $ do
   -- Reduces both sides to wnf
   book <- envGetBook
   fill <- envGetFill
@@ -24,7 +24,7 @@ equal a b dep = do
   state <- envSnapshot
   -- If both sides are identical, return true
   is_id <- identical a' b' dep
-  if is_id then
+  if is_id then do
     envPure True
   -- Otherwise, check if they're component-wise equal
   else do
@@ -33,7 +33,7 @@ equal a b dep = do
 
 -- Checks if two terms are already syntactically identical
 identical :: Term -> Term -> Int -> Env Bool
-identical a b dep = go a b dep where
+identical a b dep = debug ("ID " ++ termShower False a dep ++ "\n.. " ++ termShower False b dep) $ go a b dep where
   go (All aNam aInp aBod) (All bNam bInp bBod) dep = do
     iInp <- identical aInp bInp dep
     iBod <- identical (aBod (Var aNam dep)) (bBod (Var bNam dep)) (dep + 1)
@@ -77,10 +77,16 @@ identical a b dep = go a b dep where
     identical aVal b dep
   go a (Ann chk bVal bTyp) dep =
     identical a bVal dep
-  go a (Met bUid bSpn) dep =
-    unify bUid bSpn a dep
-  go (Met aUid aSpn) b dep =
-    unify aUid aSpn b dep
+  go (Met aUid aSpn) b dep = do
+    fill <- envGetFill
+    case IM.lookup aUid fill of
+      Just sol -> identical sol b dep
+      Nothing  -> unify aUid aSpn b dep
+  go a (Met bUid bSpn) dep = do
+    fill <- envGetFill
+    case IM.lookup bUid fill of
+      Just sol -> identical a sol dep
+      Nothing  -> unify bUid bSpn a dep
   go (Hol aNam aCtx) b dep =
     return True
   go a (Hol bNam bCtx) dep =
@@ -187,7 +193,7 @@ unify uid spn b dep = do
   fill <- envGetFill
 
   -- is this hole not already solved?
-  let unsolved = not (IM.member uid fill)
+  let solved = IM.member uid fill
 
   -- does the spine satisfies conditions?
   let solvable = valid fill spn []
@@ -195,11 +201,11 @@ unify uid spn b dep = do
   -- is the solution not recursive?
   let no_loops = not $ occur book fill uid b dep
 
-  do
+  debug ("unify: " ++ show uid ++ " " ++ termShower False b dep ++ " | " ++ show solved ++ " " ++ show solvable ++ " " ++ show no_loops) $ do
     -- If all is ok, generate the solution and return true
-    if unsolved && solvable && no_loops then do
+    if not solved && solvable && no_loops then do
       let solution = solve book fill uid spn b
-      envFill uid solution
+      debug ("solve: " ++ show uid ++ " " ++ termShower False solution dep) $ envFill uid solution
       return True
 
     -- Otherwise, return true iff both are identical metavars

src/Kind/Reduce.hs

@@ -2,8 +2,10 @@ module Kind.Reduce where
 
 import Prelude hiding (EQ, LT, GT)
 import Data.Char (ord)
+import Debug.Trace
 
 import Kind.Type
+import Kind.Show
 
 import qualified Data.Map.Strict as M
 import qualified Data.IntMap.Strict as IM
@@ -12,8 +14,9 @@ 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 = red term where
+reduce book fill lv term = {-trace (termShower False term 0) $-} red term where
 
   red (App fun arg)     = app (red fun) arg
   red (Ann chk val typ) = red val
@@ -28,7 +31,7 @@ reduce book fill lv term = red term where
   red (Met uid spn)     = met uid spn
   red val               = val
 
-  app (Ref nam)     arg = app (ref nam) arg
+  app (Ref nam)     arg | lv > 0 = app (ref nam) arg
   app (Met uid spn) arg = red (Met uid (spn ++ [arg]))
   app (Lam nam bod) arg = red (bod (reduce book fill 0 arg))
   app (Mat cse)     arg = mat cse (red arg)
@@ -45,7 +48,6 @@ reduce book fill lv term = red term where
   swi zer suc (Op2 ADD (Num 1) k) = red (App suc k)
   swi zer suc val                 = App (Swi zer suc) val
 
-
   met uid spn = case IM.lookup uid fill of
     Just val -> red (case spn of
       []       -> val
@@ -67,7 +69,7 @@ reduce book fill lv term = red term where
   op2 GTE (Num fst) (Num snd) = Num (if fst >= snd then 1 else 0)
   op2 opr fst       snd       = Op2 opr fst snd
 
-  ref nam | lv == 2 = case M.lookup nam book of
+  ref nam | lv > 0 = case M.lookup nam book of
     Just val -> red val
     Nothing  -> error $ "Undefined reference: " ++ nam
   ref nam = Ref nam

src/Kind/Show.hs

@@ -3,8 +3,8 @@ module Kind.Show where
 import Prelude hiding (EQ, LT, GT)
 
 import Kind.Type
-import Kind.Reduce
 
+import Debug.Trace
 import System.IO (readFile)
 import System.Directory (canonicalizePath)
 import Control.Exception (try)
@@ -59,7 +59,7 @@ termShower small term dep = case term of
   Mat cse ->
     let cse' = unwords (map (\(cnm, cbod) -> "#" ++ cnm ++ ": " ++ termShower small cbod dep) cse)
     in concat ["λ{ ", cse', " }"]
-  Ref nam -> nam
+  Ref nam -> concat ["@", nam]
   Let nam val bod ->
     let nam' = nam
         val' = termShower small val dep

src/Kind/Type.hs

@@ -3,6 +3,8 @@ module Kind.Type where
 import qualified Data.IntMap.Strict as IM
 import qualified Data.Map.Strict as M
 
+import Debug.Trace
+
 -- Kind's AST
 data Term
   -- Product: `∀(x: A) B`
@@ -107,3 +109,6 @@ data Check = Check (Maybe Cod) Term Term Int -- postponed check
 data State = State Book Fill [Check] [Info] -- state type
 data Res a = Done State a | Fail State -- result type
 data Env a = Env (State -> Res a) -- monadic checker
+
+--debug a b = trace a b
+debug a b = b