From ed97d6c0af543f371822ebe0c5bbcb6a5f4f4874 Mon Sep 17 00:00:00 2001 From: Victor Taelin Date: Wed, 28 Aug 2024 20:26:43 -0300 Subject: [PATCH] tons of stuff --- .gitignore | 2 ++ book/Bool.kind | 4 ++++ book/Equal.kind | 14 ++++++++++++++ book/Equal/apply.kind | 19 +++++++++++++++++++ book/Equal/refl.kind | 10 ++++++++++ book/Equal/rewrite.kind | 13 +++++++++++++ book/List.kind | 12 ++++++++++++ book/List/cons.kind | 12 ++++++++++++ book/List/map.kind | 20 ++++++++++++++++++++ book/List/nil.kind | 8 ++++++++ book/Nat.kind | 9 +++++++-- book/Nat/add.kind | 12 ++++++++++++ book/Nat/equal.kind | 18 ++++++++++++++++++ book/Nat/id.kind | 7 +++++++ book/Nat/mul.kind | 13 +++++++++++++ book/Nat/succ.kind | 8 ++++++++ book/Nat/zero.kind | 5 +++++ book/U32/sum.kind | 10 ++++++++++ book/main.kind | 4 ++-- src/Kind/API.hs | 12 ++++-------- src/Kind/Check.hs | 4 ++-- src/Kind/Equal.hs | 30 ++++++++++++++++++------------ src/Kind/Reduce.hs | 10 ++++++---- src/Kind/Show.hs | 4 ++-- src/Kind/Type.hs | 5 +++++ 25 files changed, 233 insertions(+), 32 deletions(-) create mode 100644 book/Bool.kind create mode 100644 book/Equal.kind create mode 100644 book/Equal/apply.kind create mode 100644 book/Equal/refl.kind create mode 100644 book/Equal/rewrite.kind create mode 100644 book/List.kind create mode 100644 book/List/cons.kind create mode 100644 book/List/map.kind create mode 100644 book/List/nil.kind create mode 100644 book/Nat/add.kind create mode 100644 book/Nat/equal.kind create mode 100644 book/Nat/id.kind create mode 100644 book/Nat/mul.kind create mode 100644 book/Nat/succ.kind create mode 100644 book/Nat/zero.kind create mode 100644 book/U32/sum.kind diff --git a/.gitignore b/.gitignore index a69f07a3..f646031a 100644 --- a/.gitignore +++ b/.gitignore @@ -19,3 +19,5 @@ cabal.project.local* .DS_Store .holefill .tmp +.backup/ +*.koder diff --git a/book/Bool.kind b/book/Bool.kind new file mode 100644 index 00000000..0f69c31b --- /dev/null +++ b/book/Bool.kind @@ -0,0 +1,4 @@ +Bool : * = #[]{ + #false{} : Bool + #true{} : Bool +} diff --git a/book/Equal.kind b/book/Equal.kind new file mode 100644 index 00000000..d8346ac7 --- /dev/null +++ b/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) +} diff --git a/book/Equal/apply.kind b/book/Equal/apply.kind new file mode 100644 index 00000000..99ddbef3 --- /dev/null +++ b/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{} +} diff --git a/book/Equal/refl.kind b/book/Equal/refl.kind new file mode 100644 index 00000000..d62c19db --- /dev/null +++ b/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{} diff --git a/book/Equal/rewrite.kind b/book/Equal/rewrite.kind new file mode 100644 index 00000000..e6d98da6 --- /dev/null +++ b/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 +} diff --git a/book/List.kind b/book/List.kind new file mode 100644 index 00000000..747ad0a1 --- /dev/null +++ b/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) +} diff --git a/book/List/cons.kind b/book/List/cons.kind new file mode 100644 index 00000000..3029a445 --- /dev/null +++ b/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} diff --git a/book/List/map.kind b/book/List/map.kind new file mode 100644 index 00000000..4f1e123e --- /dev/null +++ b/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} +} diff --git a/book/List/nil.kind b/book/List/nil.kind new file mode 100644 index 00000000..f2680120 --- /dev/null +++ b/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{} diff --git a/book/Nat.kind b/book/Nat.kind index 734ab289..85d1d6de 100644 --- a/book/Nat.kind +++ b/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 } diff --git a/book/Nat/add.kind b/book/Nat/add.kind new file mode 100644 index 00000000..de73bc81 --- /dev/null +++ b/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)} +} diff --git a/book/Nat/equal.kind b/book/Nat/equal.kind new file mode 100644 index 00000000..67e3cbe0 --- /dev/null +++ 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) + } +} diff --git a/book/Nat/id.kind b/book/Nat/id.kind new file mode 100644 index 00000000..130c66b8 --- /dev/null +++ b/book/Nat/id.kind @@ -0,0 +1,7 @@ +Nat/id +: ∀(a: Nat) + Nat += λ{ + #zero: #zero{} + #succ: λa.pred (Nat/id a.pred) +} diff --git a/book/Nat/mul.kind b/book/Nat/mul.kind new file mode 100644 index 00000000..20c3e04a --- /dev/null +++ b/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)) +} diff --git a/book/Nat/succ.kind b/book/Nat/succ.kind new file mode 100644 index 00000000..ba4171be --- /dev/null +++ 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} diff --git a/book/Nat/zero.kind b/book/Nat/zero.kind new file mode 100644 index 00000000..722e0f7f --- /dev/null +++ b/book/Nat/zero.kind @@ -0,0 +1,5 @@ +// Represents the zero natural number. +// = The nat 0. +Nat/zero +: Nat += #zero{} diff --git a/book/U32/sum.kind b/book/U32/sum.kind new file mode 100644 index 00000000..ce743c00 --- /dev/null +++ b/book/U32/sum.kind @@ -0,0 +1,10 @@ +U32/sum + +: ∀(x: U32) + U32 + += λ{ + 0: 0 + _: λx.pred (+ x.pred (U32/sum x.pred)) +} + diff --git a/book/main.kind b/book/main.kind index 3930453a..64297b11 100644 --- a/book/main.kind +++ b/book/main.kind @@ -1,3 +1,3 @@ main -: U32 -= (U32/sum 10) +: Nat += (Nat/mul #succ{#succ{#succ{#zero{}}}} #succ{#succ{#zero{}}}) diff --git a/src/Kind/API.hs b/src/Kind/API.hs index 52e8d666..e6c1b60c 100644 --- a/src/Kind/API.hs +++ b/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 diff --git a/src/Kind/Check.hs b/src/Kind/Check.hs index a62e6400..78dad071 100644 --- a/src/Kind/Check.hs +++ b/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 diff --git a/src/Kind/Equal.hs b/src/Kind/Equal.hs index 7db50336..a39a03db 100644 --- a/src/Kind/Equal.hs +++ b/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 diff --git a/src/Kind/Reduce.hs b/src/Kind/Reduce.hs index b012b1e9..4db06eb1 100644 --- a/src/Kind/Reduce.hs +++ b/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 diff --git a/src/Kind/Show.hs b/src/Kind/Show.hs index 260b662b..fa14c1a4 100644 --- a/src/Kind/Show.hs +++ b/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 diff --git a/src/Kind/Type.hs b/src/Kind/Type.hs index 36fcdcbe..914d20a4 100644 --- a/src/Kind/Type.hs +++ b/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