From e41e1d8f6a0b47571edd65525ce777c83d3dcf2c Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Wed, 1 Jan 2025 20:24:53 -0800 Subject: [PATCH] porting WIP --- done/Data/Fin.newt | 1 + done/Data/IORef.newt | 27 ++ done/Data/Int.newt | 12 + done/Data/List.newt | 1 + done/Data/List1.newt | 10 + done/Data/Maybe.newt | 1 + done/Data/Nat.newt | 1 + done/Data/SnocList.newt | 14 ++ done/Data/SortedMap.newt | 202 +++++++++++++++ done/Data/String.newt | 11 + done/Data/Vect.newt | 1 + done/Lib/Common.newt | 154 ++++++++++++ done/Lib/Erasure.newt | 101 ++++++++ done/Lib/Parser/Impl.newt | 218 ++++++++++++++++ done/Lib/Prettier.newt | 148 +++++++++++ done/Lib/Syntax.newt | 297 ++++++++++++++++++++++ done/Lib/Token.newt | 100 ++++++++ done/Lib/Tokenizer.newt | 172 +++++++++++++ done/Lib/TopContext.newt | 62 +++++ done/Lib/Types.newt | 517 ++++++++++++++++++++++++++++++++++++++ done/Lib/Util.newt | 26 ++ done/Prelude.newt | 1 + newt/Prelude.newt | 25 +- src/Lib/Parser.idr | 32 ++- 24 files changed, 2118 insertions(+), 16 deletions(-) create mode 100644 done/Data/Fin.newt create mode 100644 done/Data/IORef.newt create mode 100644 done/Data/Int.newt create mode 100644 done/Data/List.newt create mode 100644 done/Data/List1.newt create mode 100644 done/Data/Maybe.newt create mode 100644 done/Data/Nat.newt create mode 100644 done/Data/SnocList.newt create mode 100644 done/Data/SortedMap.newt create mode 100644 done/Data/String.newt create mode 100644 done/Data/Vect.newt create mode 100644 done/Lib/Common.newt create mode 100644 done/Lib/Erasure.newt create mode 100644 done/Lib/Parser/Impl.newt create mode 100644 done/Lib/Prettier.newt create mode 100644 done/Lib/Syntax.newt create mode 100644 done/Lib/Token.newt create mode 100644 done/Lib/Tokenizer.newt create mode 100644 done/Lib/TopContext.newt create mode 100644 done/Lib/Types.newt create mode 100644 done/Lib/Util.newt create mode 120000 done/Prelude.newt diff --git a/done/Data/Fin.newt b/done/Data/Fin.newt new file mode 100644 index 0000000..88094ba --- /dev/null +++ b/done/Data/Fin.newt @@ -0,0 +1 @@ +module Data.Fin diff --git a/done/Data/IORef.newt b/done/Data/IORef.newt new file mode 100644 index 0000000..c9f2232 --- /dev/null +++ b/done/Data/IORef.newt @@ -0,0 +1,27 @@ +module Data.IORef + +import Prelude + +-- We should test this at some point + +ptype IORef : U → U +pfunc primNewIORef uses (MkIORes MkUnit) : ∀ a. a → IO (IORef a) := `(_, a) => (w) => MkIORes(undefined, [a], w)` +pfunc primReadIORef uses (MkIORes MkUnit) : ∀ a. IORef a → IO a := `(_, ref) => (w) => MkIORes(undefined, ref[0], w)` +pfunc primWriteIORef uses (MkIORes MkUnit) : ∀ a. IORef a → a → IO a := `(_, ref, a) => (w) => { + ref[0] = a + return MkIORes(undefined,MkUnit,w) +}` + +newIORef : ∀ io a. {{HasIO io}} → a → io (IORef a) +newIORef a = liftIO $ primNewIORef a + +readIORef : ∀ io a. {{HasIO io}} → IORef a → io a +readIORef ref = liftIO $ primReadIORef ref + +writeIORef : ∀ io a. {{HasIO io}} → IORef a -> a -> io Unit +writeIORef ref a = liftIO $ writeIORef ref a + +-- Idris HasIO constraints to monad, we don't have those constraints yet +modifyIORef : ∀ io a. {{Monad io}} {{HasIO io}} → IORef a -> (a -> a) -> io Unit +modifyIORef {io} ref f = + bind {io} (readIORef ref) $ \a => writeIORef ref (f a) diff --git a/done/Data/Int.newt b/done/Data/Int.newt new file mode 100644 index 0000000..4beed3f --- /dev/null +++ b/done/Data/Int.newt @@ -0,0 +1,12 @@ +module Data.Int + +import Prelude + +div : Int → Int → Int +div a b = a / b + +instance Cast Char Int where + cast = ord + +instance Cast Int String where + cast = show diff --git a/done/Data/List.newt b/done/Data/List.newt new file mode 100644 index 0000000..ffa4b72 --- /dev/null +++ b/done/Data/List.newt @@ -0,0 +1 @@ +module Data.List diff --git a/done/Data/List1.newt b/done/Data/List1.newt new file mode 100644 index 0000000..1d2c573 --- /dev/null +++ b/done/Data/List1.newt @@ -0,0 +1,10 @@ +module Data.List1 + +import Prelude + +infixr 7 _:::_ + +record List1 a where + constructor _:::_ + head1 : a + tail1 : List a diff --git a/done/Data/Maybe.newt b/done/Data/Maybe.newt new file mode 100644 index 0000000..7f138d4 --- /dev/null +++ b/done/Data/Maybe.newt @@ -0,0 +1 @@ +module Data.Maybe diff --git a/done/Data/Nat.newt b/done/Data/Nat.newt new file mode 100644 index 0000000..30b96f8 --- /dev/null +++ b/done/Data/Nat.newt @@ -0,0 +1 @@ +module Data.Nat diff --git a/done/Data/SnocList.newt b/done/Data/SnocList.newt new file mode 100644 index 0000000..2e9fd6c --- /dev/null +++ b/done/Data/SnocList.newt @@ -0,0 +1,14 @@ +module Data.SnocList + +import Prelude + +snoclen : ∀ a. SnocList a → Nat +snoclen {a} xs = go xs Z + where + go : SnocList a → Nat → Nat + go Lin acc = acc + go (xs :< x) acc = go xs (S acc) + +snocelem : ∀ a. {{Eq a}} → a → SnocList a → Bool +snocelem a Lin = False +snocelem a (xs :< x) = if a == x then True else snocelem a xs diff --git a/done/Data/SortedMap.newt b/done/Data/SortedMap.newt new file mode 100644 index 0000000..ea477b3 --- /dev/null +++ b/done/Data/SortedMap.newt @@ -0,0 +1,202 @@ +module Data.SortedMap + +import Prelude + +-- TODO We'll want to replace Ord/Eq with (a → Ordering) (and rewrite most of our aoc solutions...) + +data T23 : Nat -> U -> U -> U where + Leaf : ∀ k v. k -> v -> T23 Z k v + Node2 : ∀ h k v. T23 h k v -> k -> T23 h k v -> T23 (S h) k v + Node3 : ∀ h k v. T23 h k v -> k -> T23 h k v -> k -> T23 h k v -> T23 (S h) k v + +lookupT23 : ∀ h k v. {{Ord k}} -> k -> T23 h k v -> Maybe (k × v) +lookupT23 key (Leaf k v)= case compare k key of + EQ => Just (k,v) + _ => Nothing +lookupT23 key (Node2 t1 k1 t2) = + if key <= k1 then lookupT23 key t1 else lookupT23 key t2 +lookupT23 key (Node3 t1 k1 t2 k2 t3) = + if key <= k1 then lookupT23 key t1 + else if key <= k2 then lookupT23 key t2 + else lookupT23 key t3 + +insertT23 : ∀ h k v. {{Ord k}} -> k -> v -> T23 h k v -> Either (T23 h k v) (T23 h k v × k × T23 h k v) +insertT23 key value (Leaf k v) = case compare key k of + EQ => Left (Leaf key value) + LT => Right (Leaf key value, key, Leaf k v) + GT => Right (Leaf k v, k, Leaf key value) +insertT23 key value (Node2 t1 k1 t2) = + if key <= k1 then + case insertT23 key value t1 of + Left t1' => Left (Node2 t1' k1 t2) + Right (a,b,c) => Left (Node3 a b c k1 t2) + else case insertT23 key value t2 of + Left t2' => Left (Node2 t1 k1 t2') + Right (a,b,c) => Left (Node3 t1 k1 a b c) +insertT23 key value (Node3 t1 k1 t2 k2 t3) = + if key <= k1 then + case insertT23 key value t1 of + Left t1' => Left (Node3 t1' k1 t2 k2 t3) + Right (a,b,c) => Right (Node2 a b c, k1, Node2 t2 k2 t3) + else if key <= k2 then + case insertT23 key value t2 of + Left t2' => Left (Node3 t1 k1 t2' k2 t3) + Right (a,b,c) => Right (Node2 t1 k1 a, b, Node2 c k2 t3) + else + case insertT23 key value t3 of + Left t3' => Left (Node3 t1 k1 t2 k2 t3') + Right (a,b,c) => Right (Node2 t1 k1 t2, k2, Node2 a b c) + +-- This is cribbed from Idris. Deleting nodes takes a bit of code. +Hole : Nat → U → U → U +Hole Z k v = Unit +Hole (S n) k v = T23 n k v + +Node4 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v +Node4 t1 k1 t2 k2 t3 k3 t4 = Node2 (Node2 t1 k1 t2) k2 (Node2 t3 k3 t4) + +Node5 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v +Node5 a b c d e f g h i = Node2 (Node2 a b c) d (Node3 e f g h i) + +Node6 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v +Node6 a b c d e f g h i j k = Node2 (Node3 a b c d e) f (Node3 g h i j k) + +Node7 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v +Node7 a b c d e f g h i j k l m = Node3 (Node3 a b c d e) f (Node2 g h i) j (Node2 k l m) + +merge1 : ∀ k v h. T23 h k v → k → T23 (S h) k v → k → T23 (S h) k v → T23 (S (S h)) k v +merge1 a b (Node2 c d e) f (Node2 g h i) = Node5 a b c d e f g h i +merge1 a b (Node2 c d e) f (Node3 g h i j k) = Node6 a b c d e f g h i j k +merge1 a b (Node3 c d e f g) h (Node2 i j k) = Node6 a b c d e f g h i j k +merge1 a b (Node3 c d e f g) h (Node3 i j k l m) = Node7 a b c d e f g h i j k l m + +merge2 : ∀ k v h. T23 (S h) k v → k → T23 h k v → k → T23 (S h) k v → T23 (S (S h)) k v +merge2 (Node2 a b c) d e f (Node2 g h i) = Node5 a b c d e f g h i +merge2 (Node2 a b c) d e f (Node3 g h i j k) = Node6 a b c d e f g h i j k +merge2 (Node3 a b c d e) f g h (Node2 i j k) = Node6 a b c d e f g h i j k +merge2 (Node3 a b c d e) f g h (Node3 i j k l m) = Node7 a b c d e f g h i j k l m + +merge3 : ∀ k v h. T23 (S h) k v → k → T23 (S h) k v → k → T23 h k v → T23 (S (S h)) k v +merge3 (Node2 a b c) d (Node2 e f g) h i = Node5 a b c d e f g h i +merge3 (Node2 a b c) d (Node3 e f g h i) j k = Node6 a b c d e f g h i j k +merge3 (Node3 a b c d e) f (Node2 g h i) j k = Node6 a b c d e f g h i j k +merge3 (Node3 a b c d e) f (Node3 g h i j k) l m = Node7 a b c d e f g h i j k l m + +-- height is erased in the data everywhere but the top, but needed for case +-- I wonder if we could use a 1 + 1 + 1 type instead of Either Tree Hole and condense this +deleteT23 : ∀ k v. {{Ord k}} → (h : Nat) -> k -> T23 h k v -> Either (T23 h k v) (Hole h k v) +deleteT23 Z key (Leaf k v) = case compare k key of + EQ => Right MkUnit + _ => Left (Leaf k v) +deleteT23 (S Z) key (Node2 t1 k1 t2) = + if key <= k1 + then case deleteT23 Z key t1 of + Left t1 => Left (Node2 t1 k1 t2) + Right _ => Right t2 + else case deleteT23 Z key t2 of + Left t2 => Left (Node2 t1 k1 t2) + Right MkUnit => Right t1 +deleteT23 (S Z) key (Node3 t1 k1 t2 k2 t3) = + if key <= k1 + then case deleteT23 _ key t1 of + Left t1 => Left (Node3 t1 k1 t2 k2 t3) + Right MkUnit => Left (Node2 t2 k2 t3) + else if key <= k2 then case deleteT23 _ key t2 of + Left t2 => Left (Node3 t1 k1 t2 k2 t3) + Right _ => Left (Node2 t1 k1 t3) + else case deleteT23 _ key t3 of + Left t3 => Left (Node3 t1 k1 t2 k2 t3) + Right _ => Left (Node2 t1 k1 t2) +deleteT23 (S (S h)) key (Node2 t1 k1 t2) = + if key <= k1 + then case deleteT23 (S h) key t1 of + Left t1 => Left (Node2 t1 k1 t2) + Right t1 => case t2 of + Node2 t2' k2' t3' => Right (Node3 t1 k1 t2' k2' t3') + Node3 t2 k2 t3 k3 t4 => Left $ Node4 t1 k1 t2 k2 t3 k3 t4 + else case deleteT23 _ key t2 of + Left t2 => Left (Node2 t1 k1 t2) + Right t2 => case t1 of + Node2 a b c => Right (Node3 a b c k1 t2) + Node3 a b c d e => Left (Node4 a b c d e k1 t2) +deleteT23 (S (S h)) key (Node3 t1 k1 t2 k2 t3) = + if key <= k1 + then case deleteT23 _ key t1 of + Left t1 => Left (Node3 t1 k1 t2 k2 t3) + Right t1 => Left (merge1 t1 k1 t2 k2 t3) + else if key <= k2 then case deleteT23 _ key t2 of + Left t2 => Left (Node3 t1 k1 t2 k2 t3) + Right t2 => Left (merge2 t1 k1 t2 k2 t3) + else case deleteT23 _ key t3 of + Left t3 => Left (Node3 t1 k1 t2 k2 t3) + Right t3 => Left (merge3 t1 k1 t2 k2 t3) + +treeLeft : ∀ h k v. T23 h k v → (k × v) +treeLeft (Leaf k v) = (k, v) +treeLeft (Node2 t1 _ _) = treeLeft t1 +treeLeft (Node3 t1 _ _ _ _) = treeLeft t1 + +treeRight : ∀ h k v. T23 h k v → (k × v) +treeRight (Leaf k v) = (k, v) +treeRight (Node2 _ _ t2) = treeRight t2 +treeRight (Node3 _ _ _ _ t3) = treeRight t3 + + +data SortedMap : U -> U -> U where + EmptyMap : ∀ k v. SortedMap k v + -- not erased so we know what happens in delete + MapOf : ∀ k v. {h : Nat} → T23 h k v -> SortedMap k v + +deleteMap : ∀ k v. {{Ord k}} → k → SortedMap k v → SortedMap k v +deleteMap key EmptyMap = EmptyMap +-- REVIEW if I split h separately in a nested case, it doesn't sort out Hole +deleteMap key (MapOf {k} {v} {Z} tree) = case deleteT23 Z key tree of + Left t => MapOf t + Right t => EmptyMap +deleteMap key (MapOf {k} {v} {S n} tree) = case deleteT23 (S n) key tree of + Left t => MapOf t + Right t => MapOf t + +leftMost : ∀ k v. SortedMap k v → Maybe (k × v) +leftMost EmptyMap = Nothing +leftMost (MapOf m) = Just (treeLeft m) + +rightMost : ∀ k v. SortedMap k v → Maybe (k × v) +rightMost EmptyMap = Nothing +rightMost (MapOf m) = Just (treeRight m) + +-- TODO issue with metas and case if written as `do` block +pop : ∀ k v. {{Ord k}} → SortedMap k v → Maybe ((k × v) × SortedMap k v) +pop m = case leftMost m of + Just (k,v) => Just ((k,v), deleteMap k m) + Nothing => Nothing + +lookupMap : ∀ k v. {{Ord k}} -> k -> SortedMap k v -> Maybe (k × v) +lookupMap k EmptyMap = Nothing +lookupMap k (MapOf map) = lookupT23 k map + +lookupMap' : ∀ k v. {{Ord k}} -> k -> SortedMap k v -> Maybe v +lookupMap' k EmptyMap = Nothing +lookupMap' k (MapOf map) = snd <$> lookupT23 k map + + +updateMap : ∀ k v. {{Ord k}} -> k -> v -> SortedMap k v -> SortedMap k v +updateMap k v EmptyMap = MapOf $ Leaf k v +updateMap k v (MapOf map) = case insertT23 k v map of + Left map' => MapOf map' + Right (a, b, c) => MapOf (Node2 a b c) + +toList : ∀ k v. SortedMap k v → List (k × v) +toList {k} {v} (MapOf smap) = reverse $ go smap Nil + where + go : ∀ h. T23 h k v → List (k × v) → List (k × v) + go (Leaf k v) acc = (k, v) :: acc + go (Node2 t1 k1 t2) acc = go t2 (go t1 acc) + go (Node3 t1 k1 t2 k2 t3) acc = go t3 $ go t2 $ go t1 acc +toList _ = Nil + +foldMap : ∀ a b. {{Ord a}} → (b → b → b) → SortedMap a b → List (a × b) → SortedMap a b +foldMap f m Nil = m +foldMap f m ((a,b) :: xs) = case lookupMap a m of + Nothing => foldMap f (updateMap a b m) xs + Just (_, b') => foldMap f (updateMap a (f b' b) m) xs diff --git a/done/Data/String.newt b/done/Data/String.newt new file mode 100644 index 0000000..25a622c --- /dev/null +++ b/done/Data/String.newt @@ -0,0 +1,11 @@ +module Data.String + + +import Prelude + +class Interpolation a where + interpolate : a → String + +unwords : List String → String +unwords stuff = joinBy " " stuff + diff --git a/done/Data/Vect.newt b/done/Data/Vect.newt new file mode 100644 index 0000000..160a6fe --- /dev/null +++ b/done/Data/Vect.newt @@ -0,0 +1 @@ +module Data.Vect diff --git a/done/Lib/Common.newt b/done/Lib/Common.newt new file mode 100644 index 0000000..2beba96 --- /dev/null +++ b/done/Lib/Common.newt @@ -0,0 +1,154 @@ +module Lib.Common + +import Data.String +import Data.Int +import Data.Maybe +import Data.SortedMap + +-- l is environment size, this works for both lvl2ix and ix2lvl + +lvl2ix : Int -> Int -> Int +lvl2ix l k = l - k - 1 + +hexChars : List Char +hexChars = unpack "0123456789ABCDEF" + +-- export +hexDigit : Int -> Char +hexDigit v = fromMaybe ' ' (getAt (cast $ mod v 16) hexChars) + + +toHex : Int -> List Char +toHex 0 = Nil +toHex v = snoc (toHex (div v 16)) (hexDigit v) + + +quoteString : String -> String +quoteString str = pack $ encode (unpack str) (Lin :< '"') + where + encode : List Char -> SnocList Char -> List Char + encode Nil acc = acc <>> ('"' :: Nil) + encode ('"' :: cs) acc = encode cs (acc :< '\\' :< '"') + encode ('\n' :: cs) acc = encode cs (acc :< '\\' :< 'n') + encode ('\\' :: cs) acc = encode cs (acc :< '\\' :< '\\') + encode (c :: cs) acc = + let v : Int = cast c in + if v < 32 then encode cs (acc :< '\\' :< 'u' :< hexDigit (div v 4096) :< hexDigit (div v 256) :< hexDigit (div v 16) :< hexDigit v ) + else encode cs (acc :< c) + + +data Json : U where + JsonObj : List (String × Json) -> Json + JsonStr : String -> Json + JsonBool : Bool -> Json + JsonInt : Int -> Json + JsonArray : List Json -> Json + + +renderJson : Json -> String +renderJson (JsonObj xs) = "{" ++ joinBy "," (map renderPair xs) ++ "}" + where + renderPair : (String × Json) -> String + renderPair (k,v) = quoteString k ++ ":" ++ renderJson v +renderJson (JsonStr str) = quoteString str +renderJson (JsonBool x) = ite x "true" "false" +renderJson (JsonInt i) = cast i +renderJson (JsonArray xs) = "[" ++ joinBy "," (map renderJson xs) ++ "]" + + +class ToJSON a where + toJson : a -> Json + + +instance ToJSON String where + toJson = JsonStr + + +instance ToJSON Int where + toJson = JsonInt + + +record FC where + constructor MkFC + file : String + start : (Int × Int) + + +instance ToJSON FC where + toJson (MkFC file (line,col)) = JsonObj (("file", toJson file) :: ("line", toJson line) :: ("col", toJson col) :: Nil) + + +fcLine : FC -> Int +fcLine (MkFC file (l, c)) = l + + +fcCol : FC -> Int +fcCol (MkFC file (l, c)) = c + + +class HasFC a where + getFC : a -> FC + + + + +emptyFC : FC +emptyFC = MkFC "" (0,0) + +-- Error of a parse + +data Error + = E FC String + | Postpone FC Int String + + + +instance Show FC where + show fc = "\{fc.file}:\{show fc.start}" + + +showError : String -> Error -> String +showError src (E fc msg) = "ERROR at \{show fc}: \{msg}\n" ++ go 0 (lines src) + where + go : Int -> List String -> String + go l Nil = "" + go l (x :: xs) = + if l == fcLine fc then + " \{x}\n \{replicate (cast $ fcCol fc) ' '}^\n" + else if fcLine fc - 3 < l then " " ++ x ++ "\n" ++ go (l + 1) xs + else go (l + 1) xs +showError src (Postpone fc ix msg) = "ERROR at \{show fc}: Postpone \{show ix} \{msg}\n" ++ go 0 (lines src) + where + go : Int -> List String -> String + go l Nil = "" + go l (x :: xs) = + if l == fcLine fc then + " \{x}\n \{replicate (cast $ fcCol fc) ' '}^\n" + else if fcLine fc - 3 < l then " " ++ x ++ "\n" ++ go (l + 1) xs + else go (l + 1) xs + + +data Fixity = InfixL | InfixR | Infix + + +instance Show Fixity where + show InfixL = "infixl" + show InfixR = "infixr" + show Infix = "infix" + + + +record OpDef where + constructor MkOp + opname : String + prec : Int + fix : Fixity + isPrefix : Bool + -- rule is everything after the first part of the operator, splitting on `_` + -- a normal infix operator will have a trailing `""` which will match to + -- prec / prec - 1 + rule : List String + + +Operators : U +Operators = SortedMap String OpDef diff --git a/done/Lib/Erasure.newt b/done/Lib/Erasure.newt new file mode 100644 index 0000000..3999802 --- /dev/null +++ b/done/Lib/Erasure.newt @@ -0,0 +1,101 @@ +module Lib.Erasure + +import Lib.Types +import Data.Maybe +import Data.SnocList +import Lib.TopContext + +EEnv : U +EEnv = List (String × Quant × Maybe Tm) + +-- TODO look into removing Nothing below, can we recover all of the types? +-- Idris does this in `chk` for linearity checking. + +-- check App at type + +getType : Tm -> M (Maybe Tm) +getType (Ref fc nm x) = do + top <- get + case lookup nm top of + Nothing => error fc "\{show nm} not in scope" + (Just (MkEntry _ name type def)) => pure $ Just type +getType tm = pure Nothing + + +erase : EEnv -> Tm -> List (FC × Tm) -> M Tm + +-- App a spine using type +eraseSpine : EEnv -> Tm -> List (FC × Tm) -> (ty : Maybe Tm) -> M Tm +eraseSpine env tm Nil _ = pure tm +eraseSpine env t ((fc, arg) :: args) (Just (Pi fc1 str icit Zero a b)) = do + let u = Erased (getFC arg) + eraseSpine env (App fc t u) args (Just b) +eraseSpine env t ((fc, arg) :: args) (Just (Pi fc1 str icit Many a b)) = do + u <- erase env arg Nil + -- TODO this seems wrong, we need to subst u into b to get the type + eraseSpine env (App fc t u) args (Just b) +-- eraseSpine env t ((fc, arg) :: args) (Just ty) = do +-- error fc "ceci n'est pas une ∏ \{showTm ty}" -- e.g. Bnd 1 +eraseSpine env t ((fc, arg) :: args) _ = do + u <- erase env arg Nil + eraseSpine env (App fc t u) args Nothing + +doAlt : EEnv -> CaseAlt -> M CaseAlt +-- REVIEW do we extend env? +doAlt env (CaseDefault t) = CaseDefault <$> erase env t Nil +doAlt env (CaseCons name args t) = do + top <- get + let (Just (MkEntry _ str type def)) = lookup name top + | _ => error emptyFC "\{show name} dcon missing from context" + let env' = piEnv env type args + CaseCons name args <$> erase env' t Nil + where + piEnv : EEnv -> Tm -> List String -> EEnv + piEnv env (Pi fc nm icit rig t u) (arg :: args) = piEnv ((arg, rig, Just t) :: env) u args + piEnv env _ _ = env + +doAlt env (CaseLit lit t) = CaseLit lit <$> erase env t Nil + +-- Check erasure and insert "Erased" value +-- We have a solution for Erased values, so important thing here is checking. +-- build stack, see what to do when we hit a non-app +-- This is a little fuzzy because we don't have all of the types. +erase env t sp = case t of + (App fc u v) => erase env u ((fc,v) :: sp) + (Ref fc nm x) => do + top <- get + case lookup nm top of + Nothing => error fc "\{show nm} not in scope" + (Just (MkEntry _ name type def)) => eraseSpine env t sp (Just type) + (Lam fc nm icit rig u) => Lam fc nm icit rig <$> erase ((nm, rig, Nothing) :: env) u Nil + -- If we get here, we're looking at a runtime pi type + (Pi fc nm icit rig u v) => do + u' <- erase env u Nil + v' <- erase ((nm, Many, Just u) :: env) v Nil + eraseSpine env (Pi fc nm icit rig u' v') sp (Just $ UU emptyFC) + -- leaving as-is for now, we don't know the quantity of the apps + (Meta fc k) => pure t + (Case fc u alts) => do + -- REVIEW check if this pushes to env, and write that down or get an index on there + u' <- erase env u Nil + alts' <- traverse (doAlt env) alts + eraseSpine env (Case fc u' alts') sp Nothing + (Let fc nm u v) => do + u' <- erase env u Nil + v' <- erase ((nm, Many, Nothing) :: env) v Nil + eraseSpine env (Let fc nm u' v') sp Nothing + (LetRec fc nm ty u v) => do + u' <- erase ((nm, Many, Just ty) :: env) u Nil + v' <- erase ((nm, Many, Just ty) :: env) v Nil + eraseSpine env (LetRec fc nm ty u' v') sp Nothing + (Bnd fc k) => do + case getAt (cast k) env of + Nothing => error fc "bad index \{show k}" + -- This is working, but empty FC + Just (nm, Zero, ty) => error fc "used erased value \{show nm} (FIXME FC may be wrong here)" + Just (nm, Many, ty) => eraseSpine env t sp ty + (UU fc) => eraseSpine env t sp (Just $ UU fc) + (Lit fc lit) => eraseSpine env t sp Nothing + Erased fc => error fc "erased value in relevant context" -- eraseSpine env t sp Nothing + + diff --git a/done/Lib/Parser/Impl.newt b/done/Lib/Parser/Impl.newt new file mode 100644 index 0000000..433c1a0 --- /dev/null +++ b/done/Lib/Parser/Impl.newt @@ -0,0 +1,218 @@ +module Lib.Parser.Impl + +import Lib.Token +import Lib.Common +import Data.String +import Data.Int +import Data.List1 +import Data.SortedMap + + +TokenList : U +TokenList = List BTok + +-- Result of a parse + +data Result : U -> U where + OK : ∀ a. a -> (toks : TokenList) -> (com : Bool) -> Operators -> Result a + Fail : ∀ a. Bool -> Error -> (toks : TokenList) -> (com : Bool) -> Operators -> Result a + + +instance Functor Result where + map f (OK a toks com ops) = OK (f a) toks com ops + map _ (Fail fatal err toks com ops) = Fail fatal err toks com ops + +-- So sixty just has a newtype function here now (probably for perf). +-- A record might be more ergonomic, but would require a record impl before +-- self hosting. + +-- FC is a line and column for indents. The idea being that we check +-- either the col < tokCol or line == tokLine, enabling sameLevel. + +-- We need State for operators (or postpone that to elaboration) +-- Since I've already built out the pratt stuff, I guess I'll +-- leave it in the parser for now + +-- This is a Reader in FC, a State in Operators, Commit flag, TokenList + + +data Parser a = P (TokenList -> Bool -> Operators -> (lc : FC) -> Result a) + + +runP : ∀ a. Parser a -> TokenList -> Bool -> Operators -> FC -> Result a +runP (P f) = f + +-- FIXME no filename, also half the time it is pointing at the token after the error +perror : String -> TokenList -> String -> Error +perror fn Nil msg = E (MkFC fn (0,0)) msg +perror fn ((MkBounded val (MkBounds line col _ _)) :: _) msg = E (MkFC fn (line,col)) msg + + +parse : ∀ a. String -> Parser a -> TokenList -> Either Error a +parse fn pa toks = case runP pa toks False EmptyMap (MkFC fn (-1,-1)) of + Fail fatal err toks com ops => Left err + OK a Nil _ _ => Right a + OK a ts _ _ => Left (perror fn ts "Extra toks") + +-- Intended for parsing a top level declaration + +partialParse : ∀ a. String -> Parser a -> Operators -> TokenList -> Either (Error × TokenList) (a × Operators × TokenList) +partialParse fn pa ops toks = case runP pa toks False ops (MkFC fn (0,0)) of + Fail fatal err toks com ops => Left (err, toks) + OK a ts _ ops => Right (a,ops,ts) + +-- I think I want to drop the typeclasses for v1 + + +try : ∀ a. Parser a -> Parser a +try (P pa) = P $ \toks com ops col => case pa toks com ops col of + (Fail x err toks com ops) => Fail x err toks False ops + res => res + + +fail : ∀ a. String -> Parser a +fail msg = P $ \toks com ops col => Fail False (perror col.file toks msg) toks com ops + + +fatal : ∀ a. String -> Parser a +fatal msg = P $ \toks com ops col => Fail True (perror col.file toks msg) toks com ops + + +getOps : Parser (Operators) +getOps = P $ \ toks com ops col => OK ops toks com ops + + +addOp : String -> Int -> Fixity -> Parser Unit +addOp nm prec fix = P $ \ toks com ops col => + let parts = split "_" nm in + case parts of + "" :: key :: rule => OK MkUnit toks com (updateMap key (MkOp nm prec fix False rule) ops) + key :: rule => OK MkUnit toks com (updateMap key (MkOp nm prec fix True rule) ops) + Nil => Fail True (perror col.file toks "Internal error parsing mixfix") toks com ops + + + + +instance Functor Parser where + map f (P pa) = P $ \ toks com ops col => map f (pa toks com ops col) + + +instance Applicative Parser where + return pa = P (\ toks com ops col => OK pa toks com ops) + P pab <*> P pa = P $ \toks com ops col => + case pab toks com ops col of + Fail fatal err toks com ops => Fail fatal err toks com ops + OK f toks com ops => + case pa toks com ops col of + (OK x toks com ops) => OK (f x) toks com ops + (Fail fatal err toks com ops) => Fail fatal err toks com ops + +-- Second argument lazy so we don't have circular refs when defining parsers. + +instance Alternative Parser where + (P pa) <|> (P pb) = P $ \toks com ops col => + case pa toks False ops col of + OK a toks' _ ops => OK a toks' com ops + Fail True err toks' com ops => Fail True err toks' com ops + Fail fatal err toks' True ops => Fail fatal err toks' True ops + Fail fatal err toks' False ops => pb toks com ops col + + +instance Monad Parser where + pure = return + bind (P pa) pab = P $ \toks com ops col => + case pa toks com ops col of + (OK a toks com ops) => runP (pab a) toks com ops col + (Fail fatal err xs x ops) => Fail fatal err xs x ops + + +satisfy : (BTok -> Bool) -> String -> Parser String +satisfy f msg = P $ \toks com ops col => + case toks of + (t :: ts) => if f t then OK (value t) ts True ops else Fail False (perror col.file toks "\{msg} at \{show t.val.kind}:\{value t}") toks com ops + Nil => Fail False (perror col.file toks "\{msg} at EOF") toks com ops + + +commit : Parser Unit +commit = P $ \toks com ops col => OK MkUnit toks True ops + + +some : ∀ a. Parser a -> Parser (List a) +many : ∀ a. Parser a -> Parser (List a) +some p = _::_ <$> p <*> many p +many p = some p <|> pure Nil + +-- one or more `a` seperated by `s` + +sepBy : ∀ s a. Parser s -> Parser a -> Parser (List a) +sepBy s a = _::_ <$> a <*> many (s *> a) + + +getPos : Parser FC +getPos = P $ \toks com ops indent => case toks of + Nil => OK emptyFC toks com ops + (t :: ts) => OK (MkFC indent.file (getStart t)) toks com ops + +-- Start an indented block and run parser in it + +startBlock : ∀ a. Parser a -> Parser a +startBlock (P p) = P $ \toks com ops indent => case toks of + Nil => p toks com ops indent + (t :: _) => + -- If next token is at or before the current level, we've got an empty block + let (tl,tc) = getStart t in + let (MkFC file (line,col)) = indent in + p toks com ops (MkFC file (tl, ite (tc <= col) (col + 1) tc)) + +-- Assert that parser starts at our current column by +-- checking column and then updating line to match the current + +sameLevel : ∀ a. Parser a -> Parser a +sameLevel (P p) = P $ \toks com ops indent => case toks of + Nil => p toks com ops indent + (t :: _) => + let (tl,tc) = getStart t in + let (MkFC file (line,col)) = indent in + if tc == col then p toks com ops (MkFC file (tl, col)) + else if col < tc then Fail False (perror file toks "unexpected indent") toks com ops + else Fail False (perror file toks "unexpected indent") toks com ops + + +someSame : ∀ a. Parser a -> Parser (List a) +someSame pa = some $ sameLevel pa + + +manySame : ∀ a. Parser a -> Parser (List a) +manySame pa = many $ sameLevel pa + +-- check indent on next token and run parser + +indented : ∀ a. Parser a -> Parser a +indented (P p) = P $ \toks com ops indent => case toks of + Nil => p toks com ops indent + (t :: _) => + let (tl,tc) = getStart t + in if tc > fcCol indent || tl == fcLine indent then p toks com ops indent + else Fail False (perror indent.file toks "unexpected outdent") toks com ops + +-- expect token of given kind + +token' : Kind -> Parser String +token' k = satisfy (\t => t.val.kind == k) "Expected a \{show k} token" + +keyword' : String -> Parser Unit +-- FIXME make this an appropriate whitelist +keyword' kw = ignore $ satisfy (\t => t.val.text == kw && (t.val.kind == Keyword || t.val.kind == Symbol || t.val.kind == Number)) "Expected \{kw}" + +-- expect indented token of given kind + +token : Kind -> Parser String +token = indented ∘ token' + + +keyword : String -> Parser Unit +keyword kw = indented $ keyword' kw + +symbol : String -> Parser Unit +symbol = keyword + diff --git a/done/Lib/Prettier.newt b/done/Lib/Prettier.newt new file mode 100644 index 0000000..91c980d --- /dev/null +++ b/done/Lib/Prettier.newt @@ -0,0 +1,148 @@ +-- A prettier printer, Philip Wadler +-- https://homepages.inf.ed.ac.uk/wadler/papers/prettier/prettier.pdf +module Lib.Prettier + +import Data.String +import Data.Int +import Data.Maybe + +-- `Doc` is a pretty printing document. Constructors are private, use +-- methods below. `Alt` in particular has some invariants on it, see paper +-- for details. (Something along the lines of "the first line of left is not +-- bigger than the first line of the right".) + +data Doc = Empty | Line | Text String | Nest Int Doc | Seq Doc Doc | Alt Doc Doc + +-- The original paper had a List-like structure Doc (the above was DOC) which +-- had Empty and a tail on Text and Line. +data Item = TEXT String | LINE Int + + +empty : Doc +empty = Empty + +flatten : Doc -> Doc +flatten Empty = Empty +flatten (Seq x y) = Seq (flatten x) (flatten y) +flatten (Nest i x) = flatten x +flatten Line = Text " " +flatten (Text str) = Text str +flatten (Alt x y) = flatten x + +group : Doc -> Doc +group x = Alt (flatten x) x + +-- TODO - we can accumulate snoc and cat all at once +layout : List Item -> SnocList String -> String +layout Nil acc = fastConcat $ acc <>> Nil +layout (LINE k :: x) acc = layout x (acc :< "\n" :< replicate (cast k) ' ') +layout (TEXT str :: x) acc = layout x (acc :< str) + +-- Whether a documents first line fits. +fits : Int -> List Item -> Bool +fits w ((TEXT s) :: xs) = if slen s < w then fits (w - slen s) xs else False +fits w _ = True + +-- vs Wadler, we're collecting the left side as a SnocList to prevent +-- blowing out the stack on the Text case. The original had DOC as +-- a Linked-List like structure (now List Item) + +-- I've now added a `fit` boolean to indicate if we should cut when we hit the line length +-- Wadler was relying on laziness to stop the first branch before LINE if necessary +be : Bool -> SnocList Item -> Int -> Int -> List (Int × Doc) -> Maybe (List Item) +be fit acc w k Nil = Just (acc <>> Nil) +be fit acc w k ((i, Empty) :: xs) = be fit acc w k xs +be fit acc w k ((i, Line) :: xs) = (be False (acc :< LINE i) w i xs) +be fit acc w k ((i, (Text s)) :: xs) = + if not fit || (k + slen s < w) + then (be fit (acc :< TEXT s) w (k + slen s) xs) + else Nothing +be fit acc w k ((i, (Nest j x)) :: xs) = be fit acc w k ((i + j, x) :: xs) +be fit acc w k ((i, (Seq x y)) :: xs) = be fit acc w k ((i,x) :: (i,y) :: xs) +be fit acc w k ((i, (Alt x y)) :: xs) = + (_<>>_ acc) <$> (be True Lin w k ((i,x) :: xs) <|> be fit Lin w k ((i,y) :: xs)) + +best : Int -> Int -> Doc -> List Item +best w k x = fromMaybe Nil $ be False Lin w k ((0,x) :: Nil) + +-- Public class + +class Pretty a where + pretty : a -> Doc + + +render : Int -> Doc -> String +render w x = layout (best w 0 x) Lin + + +instance Semigroup Doc where x <+> y = Seq x (Seq (Text " ") y) + +-- Match System.File so we don't get warnings + +infixl 5 __ + + +line : Doc +line = Line + + +text : String -> Doc +text = Text + + +nest : Int -> Doc -> Doc +nest = Nest + +instance Concat Doc where + x ++ y = Seq x y + + +__ : Doc -> Doc -> Doc +x y = x ++ line ++ y + +-- fold, but doesn't emit extra nil + +folddoc : (Doc -> Doc -> Doc) -> List Doc -> Doc +folddoc f Nil = Empty +folddoc f (x :: Nil) = x +folddoc f (x :: xs) = f x (folddoc f xs) + +-- separate with space + +spread : List Doc -> Doc +spread = folddoc _<+>_ + +-- separate with new lines + +stack : List Doc -> Doc +stack = folddoc __ + +-- bracket x with l and r, indenting contents on new line + +bracket : String -> Doc -> String -> Doc +bracket l x r = group (text l ++ nest 2 (line ++ x) ++ line ++ text r) + + +infixl 5 _<+/>_ + +-- Either space or newline + +_<+/>_ : Doc -> Doc -> Doc +x <+/> y = x ++ Alt (text " ") line ++ y + +-- Reformat some docs to fill. Not sure if I want this precise behavior or not. + +fill : List Doc -> Doc +fill Nil = Empty +fill (x :: Nil) = x +fill (x :: y :: xs) = Alt (flatten x <+> fill (flatten y :: xs)) (x fill (y :: xs)) + +-- separate with comma + +commaSep : List Doc -> Doc +commaSep = folddoc (\a b => a ++ text "," <+/> b) + +-- If we stick Doc into a String, try to avoid line-breaks via `flatten` + +instance Interpolation Doc where + interpolate = render 80 ∘ flatten diff --git a/done/Lib/Syntax.newt b/done/Lib/Syntax.newt new file mode 100644 index 0000000..62d0a37 --- /dev/null +++ b/done/Lib/Syntax.newt @@ -0,0 +1,297 @@ +module Lib.Syntax + +import Data.String +import Data.Maybe +import Lib.Parser.Impl +import Lib.Prettier +import Lib.Types + +Raw : U + + +data Pattern + = PatVar FC Icit Name + | PatCon FC Icit QName (List Pattern) (Maybe Name) + | PatWild FC Icit + -- Not handling this yet, but we need to be able to work with numbers and strings... + | PatLit FC Literal + + +getIcit : Pattern -> Icit +getIcit (PatVar x icit str) = icit +getIcit (PatCon x icit str xs as) = icit +getIcit (PatWild x icit) = icit +getIcit (PatLit fc lit) = Explicit + + + +instance HasFC Pattern where + getFC (PatVar fc _ _) = fc + getFC (PatCon fc _ _ _ _) = fc + getFC (PatWild fc _) = fc + getFC (PatLit fc lit) = fc + +-- %runElab deriveShow `{Pattern} + +Constraint : U +Constraint = (String × Pattern) + + +record Clause where + constructor MkClause + clauseFC : FC + -- I'm including the type of the left, so we can check pats and get the list of possibilities + -- But maybe rethink what happens on the left. + -- It's a VVar k or possibly a pattern. + -- a pattern either is zipped out, dropped (non-match) or is assigned to rhs + -- if we can do all three then we can have a VVar here. + cons : List Constraint + pats : List Pattern + -- We'll need some context to typecheck this + -- it has names from Pats, which will need types in the env + expr : Raw + +-- could be a pair, but I suspect stuff will be added? + +data RCaseAlt = MkAlt Raw Raw + + +data DoStmt : U where + DoExpr : (fc : FC) -> Raw -> DoStmt + DoLet : (fc : FC) -> String -> Raw -> DoStmt + DoArrow : (fc : FC) -> Raw -> Raw -> List RCaseAlt -> DoStmt + +Decl : U +data Raw : U where + RVar : (fc : FC) -> (nm : Name) -> Raw + RLam : (fc : FC) -> BindInfo -> (ty : Raw) -> Raw + RApp : (fc : FC) -> (t : Raw) -> (u : Raw) -> (icit : Icit) -> Raw + RU : (fc : FC) -> Raw + RPi : (fc : FC) -> BindInfo -> (ty : Raw) -> (sc : Raw) -> Raw + RLet : (fc : FC) -> (nm : Name) -> (ty : Raw) -> (v : Raw) -> (sc : Raw) -> Raw + RAnn : (fc : FC) -> (tm : Raw) -> (ty : Raw) -> Raw + RLit : (fc : FC) -> Literal -> Raw + RCase : (fc : FC) -> (scrut : Raw) -> (alts : List RCaseAlt) -> Raw + RImplicit : (fc : FC) -> Raw + RHole : (fc : FC) -> Raw + RDo : (fc : FC) -> List DoStmt -> Raw + RIf : (fc : FC) -> Raw -> Raw -> Raw -> Raw + RWhere : (fc : FC) -> (List Decl) -> Raw -> Raw + RAs : (fc : FC) -> Name -> Raw -> Raw + +instance HasFC Raw where + getFC (RVar fc nm) = fc + getFC (RLam fc _ ty) = fc + getFC (RApp fc t u icit) = fc + getFC (RU fc) = fc + getFC (RPi fc _ ty sc) = fc + getFC (RLet fc nm ty v sc) = fc + getFC (RAnn fc tm ty) = fc + getFC (RLit fc y) = fc + getFC (RCase fc scrut alts) = fc + getFC (RImplicit fc) = fc + getFC (RHole fc) = fc + getFC (RDo fc stmts) = fc + getFC (RIf fc _ _ _) = fc + getFC (RWhere fc _ _) = fc + getFC (RAs fc _ _) = fc + + +data Import = MkImport FC Name + + + +Telescope : U +Telescope = List (BindInfo × Raw) + + +data Decl + = TypeSig FC (List Name) Raw + | Def FC Name (List (Raw × Raw)) -- (List Clause) + | DCheck FC Raw Raw + | Data FC Name Raw (List Decl) + | ShortData FC Raw (List Raw) + | PType FC Name (Maybe Raw) + | PFunc FC Name (List String) Raw String + | PMixFix FC (List Name) Int Fixity + | Class FC Name Telescope (List Decl) + | Instance FC Raw (List Decl) + | Record FC Name Telescope (Maybe Name) (Maybe (List Decl)) + + +instance HasFC Decl where + getFC (TypeSig x strs tm) = x + getFC (Def x str xs) = x + getFC (DCheck x tm tm1) = x + getFC (Data x str tm xs) = x + getFC (ShortData x _ _) = x + getFC (PType x str mtm) = x + getFC (PFunc x str _ tm str1) = x + getFC (PMixFix x strs k y) = x + getFC (Class x str xs ys) = x + getFC (Instance x tm xs) = x + getFC (Record x str tm str1 xs) = x + + +record Module where + constructor MkModule + modname : Name + imports : List Import + decls : List Decl + +foo : List String -> String +foo ts = "(" ++ unwords ts ++ ")" + +instance Show Raw +instance Show Pattern + +instance Show Clause where + show (MkClause fc cons pats expr) = show (fc, cons, pats, expr) + +instance Show Import where + show (MkImport _ str) = foo ("MkImport" :: show str :: Nil) + +instance Show BindInfo where + show (BI _ nm icit quant) = foo ("BI" :: show nm :: show icit :: show quant :: Nil) + +-- this is for debugging, use pretty when possible + +instance Show Decl where + show (TypeSig _ str x) = foo ("TypeSig" :: show str :: show x :: Nil) + show (Def _ str clauses) = foo ("Def" :: show str :: show clauses :: Nil) + show (Data _ str xs ys) = foo ("Data" :: show str :: show xs :: show ys :: Nil) + show (DCheck _ x y) = foo ("DCheck" :: show x :: show y :: Nil) + show (PType _ name ty) = foo ("PType" :: name :: show ty :: Nil) + show (ShortData _ lhs sigs) = foo ("ShortData" :: show lhs :: show sigs :: Nil) + show (PFunc _ nm used ty src) = foo ("PFunc" :: nm :: show used :: show ty :: show src :: Nil) + show (PMixFix _ nms prec fix) = foo ("PMixFix" :: show nms :: show prec :: show fix :: Nil) + show (Class _ nm tele decls) = foo ("Class" :: nm :: "..." :: (show $ map show decls) :: Nil) + show (Instance _ nm decls) = foo ("Instance" :: show nm :: (show $ map show decls) :: Nil) + show (Record _ nm tele nm1 decls) = foo ("Record" :: show nm :: show tele :: show nm1 :: show decls :: Nil) + + +instance Show Module where + show (MkModule name imports decls) = foo ("MkModule" :: show name :: show imports :: show decls :: Nil) + + +instance Show Pattern where + show (PatVar _ icit str) = foo ("PatVar" :: show icit :: show str :: Nil) + show (PatCon _ icit str xs as) = foo ("PatCon" :: show icit :: show str :: show xs :: show as :: Nil) + show (PatWild _ icit) = foo ("PatWild" :: show icit :: Nil) + show (PatLit _ lit) = foo ("PatLit" :: show lit :: Nil) + + +instance Show RCaseAlt where + show (MkAlt x y)= foo ("MkAlt" :: show x :: show y :: Nil) + + +instance Show Raw where + show (RImplicit _) = "_" + show (RHole _) = "?" + show (RVar _ name) = foo ("RVar" :: show name :: Nil) + show (RAnn _ t ty) = foo ( "RAnn" :: show t :: show ty :: Nil) + show (RLit _ x) = foo ( "RLit" :: show x :: Nil) + show (RLet _ x ty v scope) = foo ( "Let" :: show x :: " : " :: show ty :: " = " :: show v :: " in " :: show scope :: Nil) + show (RPi _ bi y z) = foo ( "Pi" :: show bi :: show y :: show z :: Nil) + show (RApp _ x y z) = foo ( "App" :: show x :: show y :: show z :: Nil) + show (RLam _ bi y) = foo ( "Lam" :: show bi :: show y :: Nil) + show (RCase _ x xs) = foo ( "Case" :: show x :: show xs :: Nil) + show (RDo _ stmts) = foo ( "DO" :: "FIXME" :: Nil) + show (RU _) = "U" + show (RIf _ x y z) = foo ( "If" :: show x :: show y :: show z :: Nil) + show (RWhere _ _ _) = foo ( "Where" :: "FIXME" :: Nil) + show (RAs _ nm x) = foo ( "RAs" :: nm :: show x :: Nil) + + +instance Pretty Literal where + pretty (LString t) = text t + pretty (LInt i) = text $ show i + pretty (LChar c) = text $ show c + + +instance Pretty Pattern where + -- FIXME - wrap Implicit with {} + pretty (PatVar _ icit str) = text str + pretty (PatCon _ icit nm args Nothing) = text (show nm) <+> spread (map pretty args) + pretty (PatCon _ icit nm args (Just as)) = text as ++ text "@(" ++ text (show nm) <+> spread (map pretty args) ++ text ")" + pretty (PatWild _ icit) = text "_" + pretty (PatLit _ lit) = pretty lit + +wrap : Icit -> Doc -> Doc +wrap Explicit x = text "(" ++ x ++ text ")" +wrap Implicit x = text "{" ++ x ++ text "}" +wrap Auto x = text "{{" ++ x ++ text "}}" + + +instance Pretty Raw where + pretty = asDoc 0 + where + bindDoc : BindInfo -> Doc + bindDoc (BI _ nm icit quant) = text "BINDDOC" + + par : Int -> Int -> Doc -> Doc + par p p' d = if p' < p then text "(" ++ d ++ text ")" else d + + asDoc : Int -> Raw -> Doc + asDoc p (RVar _ str) = text str + asDoc p (RLam _ (BI _ nm icit q) x) = par p 0 $ text "\\" ++ wrap icit (text nm) <+> text "=>" <+> asDoc 0 x + -- This needs precedence and operators... + asDoc p (RApp _ x y Explicit) = par p 2 $ asDoc 2 x <+> asDoc 3 y + asDoc p (RApp _ x y Implicit) = par p 2 $ asDoc 2 x <+> text "{" ++ asDoc 0 y ++ text "}" + asDoc p (RApp _ x y Auto) = par p 2 $ asDoc 2 x <+> text "{{" ++ asDoc 0 y ++ text "}}" + asDoc p (RU _) = text "U" + asDoc p (RPi _ (BI _ "_" Explicit Many) ty scope) = par p 1 $ asDoc p ty <+> text "->" <+/> asDoc p scope + asDoc p (RPi _ (BI _ nm icit quant) ty scope) = + par p 1 $ wrap icit (text (show quant ++ nm) <+> text ":" <+> asDoc p ty ) <+> text "->" <+/> asDoc 1 scope + asDoc p (RLet _ x v ty scope) = + par p 0 $ text "let" <+> text x <+> text ":" <+> asDoc p ty + <+> text "=" <+> asDoc p v + <+/> text "in" <+> asDoc p scope + -- does this exist? + asDoc p (RAnn _ x y) = text "TODO - RAnn" + asDoc p (RLit _ lit) = pretty lit + asDoc p (RCase _ x xs) = text "TODO - RCase" + asDoc p (RImplicit _) = text "_" + asDoc p (RHole _) = text "?" + asDoc p (RDo _ stmts) = text "TODO - RDo" + asDoc p (RIf _ x y z) = par p 0 $ text "if" <+> asDoc 0 x <+/> text "then" <+> asDoc 0 y <+/> text "else" <+> asDoc 0 z + asDoc p (RWhere _ dd b) = text "TODO pretty where" + asDoc p (RAs _ nm x) = text nm ++ text "@(" ++ asDoc 0 x ++ text ")" + +prettyBind : (BindInfo × Raw) -> Doc +prettyBind (BI _ nm icit quant, ty) = wrap icit (text (show quant ++ nm) <+> text ":" <+> pretty ty) + +pipeSep : List Doc -> Doc +pipeSep = folddoc (\a b => a <+/> text "|" <+> b) + + +instance Pretty Decl where + pretty (TypeSig _ nm ty) = spread (map text nm) <+> text ":" <+> nest 2 (pretty ty) + pretty (Def _ nm clauses) = stack $ map prettyPair clauses + where + prettyPair : Raw × Raw → Doc + prettyPair (a, b) = pretty a <+> text "=" <+> pretty b + pretty (Data _ nm x xs) = text "data" <+> text nm <+> text ":" <+> pretty x <+> (nest 2 $ text "where" stack (map pretty xs)) + pretty (DCheck _ x y) = text "#check" <+> pretty x <+> text ":" <+> pretty y + pretty (PType _ nm ty) = text "ptype" <+> text nm <+> (maybe empty (\ty => text ":" <+> pretty ty) ty) + pretty (PFunc _ nm Nil ty src) = text "pfunc" <+> text nm <+> text ":" <+> nest 2 (pretty ty <+> text ":=" <+/> text (show src)) + pretty (PFunc _ nm used ty src) = text "pfunc" <+> text nm <+> text "uses" <+> spread (map text used) <+> text ":" <+> nest 2 (pretty ty <+> text ":=" <+/> text (show src)) + pretty (PMixFix _ names prec fix) = text (show fix) <+> text (show prec) <+> spread (map text names) + pretty (Record _ nm tele cname Nothing) = text "record" <+> text nm <+> text ":" <+> spread (map prettyBind tele) + pretty (Record _ nm tele cname (Just decls)) = text "record" <+> text nm <+> text ":" <+> spread (map prettyBind tele) + <+> (nest 2 $ text "where" stack (maybe empty (\ nm' => text "constructor" <+> text nm') cname :: map pretty decls)) + pretty (Class _ nm tele decls) = text "class" <+> text nm <+> text ":" <+> spread (map prettyBind tele) + <+> (nest 2 $ text "where" stack (map pretty decls)) + pretty (Instance _ _ _) = text "TODO pretty Instance" + pretty (ShortData _ lhs sigs) = text "data" <+> pretty lhs <+> text "=" <+> pipeSep (map pretty sigs) + + +instance Pretty Module where + pretty (MkModule name imports decls) = + text "module" <+> text name + stack (map doImport imports) + stack (map pretty decls) + where + doImport : Import -> Doc + doImport (MkImport _ nm) = text "import" <+> text nm ++ line + diff --git a/done/Lib/Token.newt b/done/Lib/Token.newt new file mode 100644 index 0000000..8cf6cde --- /dev/null +++ b/done/Lib/Token.newt @@ -0,0 +1,100 @@ +module Lib.Token + +import Prelude + +record Bounds where + constructor MkBounds + startLine : Int + startCol : Int + endLine : Int + endCol : Int + + +instance Eq Bounds where + (MkBounds sl sc el ec) == (MkBounds sl' sc' el' ec') = + sl == sl' + && sc == sc' + && el == el' + && ec == ec' + + +record WithBounds ty where + constructor MkBounded + val : ty + bounds : Bounds + + +data Kind + = Ident + | UIdent + | Keyword + | MixFix + | Number + | Character + | StringKind + | JSLit + | Symbol + | Space + | Comment + | Pragma + | Projection + -- not doing Layout.idr + | LBrace + | Semi + | RBrace + | EOI + | StartQuote + | EndQuote + | StartInterp + | EndInterp + + +instance Show Kind where + show Ident = "Ident" + show UIdent = "UIdent" + show Keyword = "Keyword" + show MixFix = "MixFix" + show Number = "Number" + show Character = "Character" + show Symbol = "Symbol" + show Space = "Space" + show LBrace = "LBrace" + show Semi = "Semi" + show RBrace = "RBrace" + show Comment = "Comment" + show EOI = "EOI" + show Pragma = "Pragma" + show StringKind = "String" + show JSLit = "JSLit" + show Projection = "Projection" + show StartQuote = "StartQuote" + show EndQuote = "EndQuote" + show StartInterp = "StartInterp" + show EndInterp = "EndInterp" + + +instance Eq Kind where + a == b = show a == show b + + +record Token where + constructor Tok + kind : Kind + text : String + + + +instance Show Token where + show (Tok k v) = "<\{show k}:\{show v}>" + + +BTok : U +BTok = WithBounds Token + + +value : BTok -> String +value (MkBounded (Tok _ s) _) = s + + +getStart : BTok -> (Int × Int) +getStart (MkBounded _ (MkBounds l c _ _)) = (l,c) diff --git a/done/Lib/Tokenizer.newt b/done/Lib/Tokenizer.newt new file mode 100644 index 0000000..78fe8d2 --- /dev/null +++ b/done/Lib/Tokenizer.newt @@ -0,0 +1,172 @@ +module Lib.Tokenizer + +-- Working alternate tokenizer, saves about 2k, can be translated to newt + +-- Currently this processes a stream of characters, I may switch it to +-- combinators for readability in the future. + +-- Newt is having a rough time dealing with do blocks for Either in here +-- + +import Lib.Token +import Lib.Common +import Data.String +import Data.SnocList + +standalone : List Char +standalone = unpack "()\\{}[],.@" + +keywords : List String +keywords = ("let" :: "in" :: "where" :: "case" :: "of" :: "data" :: "U" :: "do" :: + "ptype" :: "pfunc" :: "module" :: "infixl" :: "infixr" :: "infix" :: + "∀" :: "forall" :: "import" :: "uses" :: + "class" :: "instance" :: "record" :: "constructor" :: + "if" :: "then" :: "else" :: + -- it would be nice to find a way to unkeyword "." so it could be + -- used as an operator too + "$" :: "λ" :: "?" :: "@" :: "." :: + "->" :: "→" :: ":" :: "=>" :: ":=" :: "=" :: "<-" :: "\\" :: "_" :: "|" :: Nil) + +record TState where + constructor TS + trow : Int + tcol : Int + acc : SnocList BTok + chars : List Char + +singleton : Char → String +singleton c = pack $ c :: Nil + +-- This makes a big case tree... +rawTokenise : TState -> Either Error TState + +quoteTokenise : TState -> Int -> Int -> SnocList Char -> Either Error TState +quoteTokenise ts@(TS el ec toks chars) startl startc acc = case chars of + '"' :: cs => Right (TS el ec (toks :< stok) chars) + '\\' :: '{' :: cs => + let tok = MkBounded (Tok StartInterp "\\{") (MkBounds el ec el (ec + 2)) in + case (rawTokenise $ TS el (ec + 2) (toks :< stok :< tok) cs) of + Left err => Left err + Right (TS el ec toks chars) => case chars of + '}' :: cs => + let tok = MkBounded (Tok EndInterp "}") (MkBounds el ec el (ec + 1)) + in quoteTokenise (TS el (ec + 1) (toks :< tok) cs) el (ec + 1) Lin + cs => Left $ E (MkFC "" (el, ec)) "Expected '{'" + -- TODO newline in string should be an error + '\n' :: cs => Left $ E (MkFC "" (el, ec)) "Newline in string" + '\\' :: 'n' :: cs => quoteTokenise (TS el (ec + 2) toks cs) startl startc (acc :< '\n') + '\\' :: c :: cs => quoteTokenise (TS el (ec + 2) toks cs) startl startc (acc :< c) + c :: cs => quoteTokenise (TS el (ec + 1) toks cs) startl startc (acc :< c) + Nil => Left $ E (MkFC "" (el, ec)) "Expected '\"' at EOF" + + where + stok : BTok + stok = MkBounded (Tok StringKind (pack $ acc <>> Nil)) (MkBounds startl startc el ec) + + + +rawTokenise ts@(TS sl sc toks chars) = case chars of + Nil => Right $ ts + ' ' :: cs => rawTokenise (TS sl (sc + 1) toks cs) + '\n' :: cs => rawTokenise (TS (sl + 1) 0 toks cs) + + '"' :: cs => + let tok = mktok False sl (sc + 1) StartQuote "\"" in + case quoteTokenise (TS sl (sc + 1) (toks :< tok) cs) sl (sc + 1) Lin of + Left err => Left err + Right (TS sl sc toks chars) => case chars of + '"' :: cs => let tok = mktok False sl (sc + 1) EndQuote "\"" in + rawTokenise (TS sl (sc + 1) (toks :< tok) cs) + cs => Left $ E (MkFC "" (sl, sc)) "Expected '\"'" + + '{' :: '{' :: cs => + let tok = mktok False sl (sc + 2) Keyword "{{" in + case rawTokenise (TS sl (sc + 2) (toks :< tok) cs) of + Left err => Left err + Right (TS sl sc toks chars) => case chars of + '}' :: '}' :: cs => let tok = mktok False sl (sc + 2) Keyword "}}" in + rawTokenise (TS sl (sc + 2) (toks :< tok) cs) + cs => Left $ E (MkFC "" (sl, sc)) "Expected '}}'" + + '}' :: cs => Right ts + '{' :: cs => + let tok = mktok False sl (sc + 1) Symbol "{" in + case rawTokenise (TS sl (sc + 1) (toks :< tok) cs) of + Left err => Left err + Right (TS sl sc toks chars) => case chars of + '}' :: cs => let tok = mktok False sl (sc + 1) Symbol "}" in + rawTokenise (TS sl (sc + 1) (toks :< tok) cs) + cs => Left $ E (MkFC "" (sl, sc)) "Expected '}'" + + ',' :: cs => rawTokenise (TS sl (sc + 1) (toks :< mktok False sl (sc + 1) Ident ",") cs) + '_' :: ',' :: '_' :: cs => rawTokenise (TS sl (sc + 3) (toks :< mktok False sl (sc + 3) MixFix "_,_") cs) + '_' :: '.' :: '_' :: cs => rawTokenise (TS sl (sc + 3) (toks :< mktok False sl (sc + 3) MixFix "_._") cs) + '\'' :: '\\' :: c :: '\'' :: cs => + let ch = ite (c == 'n') '\n' c + in rawTokenise (TS sl (sc + 4) (toks :< mktok False sl (sc + 4) Character (singleton ch)) cs) + '\'' :: c :: '\'' :: cs => rawTokenise (TS sl (sc + 3) (toks :< mktok False sl (sc + 3) Character (singleton c)) cs) + '#' :: cs => doRest (TS sl (sc + 1) toks cs) Pragma isIdent (Lin :< '#') + '-' :: '-' :: cs => lineComment (TS sl (sc + 2) toks cs) + '/' :: '-' :: cs => blockComment (TS sl (sc + 2) toks cs) + '`' :: cs => doBacktick (TS sl (sc + 1) toks cs) Lin + '.' :: cs => doRest (TS sl (sc + 1) toks cs) Projection isIdent (Lin :< '.') + '-' :: c :: cs => if isDigit c + then doRest (TS sl (sc + 2) toks cs) Number isDigit (Lin :< '-' :< c) + else doRest (TS sl (sc + 1) toks (c :: cs)) Ident isIdent (Lin :< '-') + + c :: cs => doChar c cs + + where + isIdent : Char -> Bool + isIdent c = not (isSpace c || elem c standalone) + + isUIdent : Char -> Bool + isUIdent c = isIdent c || c == '.' + + doBacktick : TState -> SnocList Char -> Either Error TState + doBacktick (TS l c toks Nil) acc = Left $ E (MkFC "" (l,c)) "EOF in backtick string" + doBacktick (TS el ec toks ('`' :: cs)) acc = + let tok = MkBounded (Tok JSLit (pack $ acc <>> Nil)) (MkBounds sl sc el ec) in + rawTokenise (TS el (ec + 1) (toks :< tok) cs) + doBacktick (TS l c toks ('\n' :: cs)) acc = doBacktick (TS (l + 1) 0 toks cs) (acc :< '\n') + doBacktick (TS l c toks (ch :: cs)) acc = doBacktick (TS l (c + 1) toks cs) (acc :< ch) + + + -- temporary use same token as before + mktok : Bool -> Int -> Int -> Kind -> String -> BTok + mktok checkkw el ec kind text = let kind = if checkkw && elem text keywords then Keyword else kind in + MkBounded (Tok kind text) (MkBounds sl sc el ec) + + lineComment : TState -> Either Error TState + lineComment (TS line col toks Nil) = rawTokenise (TS line col toks Nil) + lineComment (TS line col toks ('\n' :: cs)) = rawTokenise (TS (line + 1) 0 toks cs) + lineComment (TS line col toks (c :: cs)) = lineComment (TS line (col + 1) toks cs) + + blockComment : TState -> Either Error TState + blockComment (TS line col toks Nil) = Left $ E (MkFC "" (line, col)) "EOF in block comment" + blockComment (TS line col toks ('-' :: '/' :: cs)) = rawTokenise (TS line (col + 2) toks cs) + blockComment (TS line col toks ('\n' :: cs)) = blockComment (TS (line + 1) 0 toks cs) + blockComment (TS line col toks (c :: cs)) = blockComment (TS line (col + 1) toks cs) + + doRest : TState -> Kind -> (Char -> Bool) -> SnocList Char -> Either Error TState + doRest (TS l c toks Nil) kind pred acc = rawTokenise (TS l c (toks :< mktok True l c kind (pack $ acc <>> Nil)) Nil) + doRest (TS l c toks (ch :: cs)) kind pred acc = if pred ch + then doRest (TS l (c + 1) toks cs) kind pred (acc :< ch) + else + let kind = if snocelem '_' acc then MixFix else kind in + rawTokenise (TS l c (toks :< mktok True l (c - 1) kind (pack $ acc <>> Nil)) (ch :: cs)) + + doChar : Char -> List Char -> Either Error TState + doChar c cs = if elem c standalone + then rawTokenise (TS sl (sc + 1) (toks :< mktok True sl (sc + 1) Symbol (pack $ c :: Nil)) cs) + else let kind = if isDigit c then Number else if isUpper c then UIdent else Ident in + doRest (TS sl sc toks (c :: cs)) kind isIdent Lin + + +tokenise : String -> String -> Either Error (List BTok) +tokenise fn text = case rawTokenise (TS 0 0 Lin (unpack text)) of + Right (TS trow tcol acc Nil) => Right $ acc <>> Nil + Right (TS trow tcol acc chars) => Left $ E (MkFC fn (trow, tcol)) "Extra toks" + Left (E (MkFC file start) str) => Left $ E (MkFC fn start) str + Left err => Left err + diff --git a/done/Lib/TopContext.newt b/done/Lib/TopContext.newt new file mode 100644 index 0000000..1dec1c7 --- /dev/null +++ b/done/Lib/TopContext.newt @@ -0,0 +1,62 @@ +module Lib.TopContext + +import Data.IORef +import Data.SortedMap +import Data.String +import Lib.Types + +-- I want unique ids, to be able to lookup, update, and a Ref so +-- I don't need good Context discipline. (I seem to have made mistakes already.) + + +lookup : QName -> TopContext -> Maybe TopEntry +lookup nm top = lookupMap' nm top.defs + +-- TODO - look at imported namespaces, and either have a map of imported names or search imported namespaces.. + +lookupRaw : String -> TopContext -> Maybe TopEntry +lookupRaw raw top = go $ toList top.defs + where + go : List (QName × TopEntry) -> Maybe TopEntry + go Nil = Nothing + go (((QN ns nm), entry) :: rest) = if nm == raw then Just entry else go rest + +-- Maybe pretty print? + + +instance Show TopContext where + show (MkTop defs metas _ _ _ _) = "\nContext:\n (\{ joinBy "\n" $ map (show ∘ snd) $ toList defs} :: Nil)" + +-- TODO need to get class dependencies working +emptyTop : ∀ io. {{Monad io}} {{HasIO io}} -> io TopContext +emptyTop = do + mcctx <- newIORef (MC Nil 0) + errs <- newIORef $ the (List Error) Nil + pure $ MkTop EmptyMap mcctx False errs Nil EmptyMap + + +setDef : QName -> FC -> Tm -> Def -> M Unit +setDef name fc ty def = do + top <- get + let (Nothing) = lookupMap' name top.defs + | Just (MkEntry fc' nm' ty' def') => error fc "\{show name} is already defined at \{show fc'}" + modify $ \case + MkTop defs metaCtx verbose errors loaded ops => + let defs = (updateMap name (MkEntry fc name ty def) top.defs) in + MkTop defs metaCtx verbose errors loaded ops + + +updateDef : QName -> FC -> Tm -> Def -> M Unit +updateDef name fc ty def = do + top <- get + let (Just (MkEntry fc' nm' ty' def')) = lookupMap' name top.defs + | Nothing => error fc "\{show name} not declared" + modify $ \case + MkTop defs metaCtx verbose errors loaded ops => + let defs = (updateMap name (MkEntry fc' name ty def) defs) in + MkTop defs metaCtx verbose errors loaded ops + +addError : Error -> M Unit +addError err = do + top <- get + modifyIORef top.errors (_::_ err) diff --git a/done/Lib/Types.newt b/done/Lib/Types.newt new file mode 100644 index 0000000..7ffe588 --- /dev/null +++ b/done/Lib/Types.newt @@ -0,0 +1,517 @@ +module Lib.Types + +-- For FC, Error +import Lib.Common +import Lib.Prettier + +import Data.Fin +import Data.IORef +import Data.List +import Data.SnocList +import Data.SortedMap +import Data.String +import Data.Vect + +data QName : U where + QN : List String -> String -> QName + +instance Eq QName where + QN ns n == QN ns' n' = n == n' && ns == ns' + +instance Show QName where + show (QN Nil n) = n + show (QN ns n) = joinBy "." ns ++ "." ++ n + +instance Interpolation QName where + interpolate = show + +instance Ord QName where + compare (QN ns nm) (QN ns' nm') = if ns == ns' then compare nm nm' else compare ns ns' + +Name : U +Name = String + +data Icit = Implicit | Explicit | Auto + +instance Show Icit where + show Implicit = "Implicit" + show Explicit = "Explicit" + show Auto = "Auto" + +data BD = Bound | Defined + +instance Eq BD where + Bound == Bound = True + Defined == Defined = True + _ == _ = False + +instance Show BD where + show Bound = "bnd" + show Defined = "def" + +data Quant = Zero | Many + +instance Show Quant where + show Zero = "0 " + show Many = "" + +instance Eq Quant where + Zero == Zero = True + Many == Many = True + _ == _ = False + +-- We could make this polymorphic and use for environment... + +data BindInfo : U where + BI : (fc : FC) -> (name : Name) -> (icit : Icit) -> (quant : Quant) -> BindInfo + +instance HasFC BindInfo where + getFC (BI fc _ _ _) = fc + +Tm : U + +data Literal = LString String | LInt Int | LChar Char + +instance Show Literal where + show (LString str) = show str + show (LInt i) = show i + show (LChar c) = show c + +data CaseAlt : U where + CaseDefault : Tm -> CaseAlt + CaseCons : (name : QName) -> (args : List String) -> Tm -> CaseAlt + CaseLit : Literal -> Tm -> CaseAlt + +Def : U + +instance Eq Literal where + LString x == LString y = x == y + LInt x == LInt y = x == y + LChar x == LChar y = x == y + _ == _ = False + +data Tm : U where + Bnd : FC -> Int -> Tm + -- Maybe Def here instead of Maybe Tm, we'll have DCon, TCon, etc. + Ref : FC -> QName -> Def -> Tm + Meta : FC -> Int -> Tm + -- kovacs optimization, I think we can App out meta instead + -- InsMeta : Int -> List BD -> Tm + Lam : FC -> Name -> Icit -> Quant -> Tm -> Tm + App : FC -> Tm -> Tm -> Tm + UU : FC -> Tm + Pi : FC -> Name -> Icit -> Quant -> Tm -> Tm -> Tm + Case : FC -> Tm -> List CaseAlt -> Tm + -- need type? + Let : FC -> Name -> Tm -> Tm -> Tm + -- for desugaring where + LetRec : FC -> Name -> Tm -> Tm -> Tm -> Tm + Lit : FC -> Literal -> Tm + Erased : FC -> Tm + +instance HasFC Tm where + getFC (Bnd fc k) = fc + getFC (Ref fc str x) = fc + getFC (Meta fc k) = fc + getFC (Lam fc str _ _ t) = fc + getFC (App fc t u) = fc + getFC (UU fc) = fc + getFC (Pi fc str icit quant t u) = fc + getFC (Case fc t xs) = fc + getFC (Lit fc _) = fc + getFC (Let fc _ _ _) = fc + getFC (LetRec fc _ _ _ _) = fc + getFC (Erased fc) = fc + +showCaseAlt : CaseAlt → String + +instance Show Tm where + show (Bnd _ k) = "(Bnd \{show k})" + show (Ref _ str _) = "(Ref \{show str})" + show (Lam _ nm icit rig t) = "(\\ \{show rig}\{nm} => \{show t})" + show (App _ t u) = "(\{show t} \{show u})" + show (Meta _ i) = "(Meta \{show i})" + show (Lit _ l) = "(Lit \{show l})" + show (UU _) = "U" + show (Pi _ str Explicit rig t u) = "(Pi (\{show rig}\{str} : \{show t}) => \{show u})" + show (Pi _ str Implicit rig t u) = "(Pi {\{show rig}\{str} : \{show t}} => \{show u})" + show (Pi _ str Auto rig t u) = "(Pi {{\{show rig}\{str} : \{show t}}} => \{show u})" + show (Case _ sc alts) = "(Case \{show sc} \{show $ map showCaseAlt alts})" + show (Let _ nm t u) = "(Let \{nm} \{show t} \{show u})" + show (LetRec _ nm ty t u) = "(LetRec \{nm} : \{show ty} \{show t} \{show u})" + show (Erased _) = "ERASED" + + +showCaseAlt (CaseDefault tm) = "_ => \{show tm}" +showCaseAlt (CaseCons nm args tm) = "\{show nm} \{unwords args} => \{show tm}" +showCaseAlt (CaseLit lit tm) = "\{show lit} => \{show tm}" + + +showTm : Tm -> String +showTm = show + +-- I can't really show val because it's HOAS... + +-- TODO derive + +instance Eq Icit where + Implicit == Implicit = True + Explicit == Explicit = True + Auto == Auto = True + _ == _ = False + +-- Eq on Tm. We've got deBruijn indices, so I'm not comparing names + +instance Eq (Tm) where + -- (Local x) == (Local y) = x == y + (Bnd _ x) == (Bnd _ y) = x == y + (Ref _ x _) == Ref _ y _ = x == y + (Lam _ n _ _ t) == Lam _ n' _ _ t' = t == t' + (App _ t u) == App _ t' u' = t == t' && u == u' + (UU _) == (UU _) = True + (Pi _ n icit rig t u) == (Pi _ n' icit' rig' t' u') = icit == icit' && rig == rig' && t == t' && u == u' + _ == _ = False + +-- TODO App and Lam should have <+/> but we need to fix +-- INFO pprint to `nest 2 ...` +-- maybe return Doc and have an Interpolation.. +-- If we need to flatten, case is going to get in the way. + +pprint' : Int -> List String -> Tm -> Doc +pprintAlt : Int -> List String -> CaseAlt -> Doc +pprintAlt p names (CaseDefault t) = text "_" <+> text "=>" <+> pprint' p ("_" :: names) t +pprintAlt p names (CaseCons name args t) = text (show name) <+> spread (map text args) <+> (nest 2 $ text "=>" <+/> pprint' p (reverse args ++ names) t) +-- `;` is not in surface syntax, but sometimes we print on one line +pprintAlt p names (CaseLit lit t) = text (show lit) <+> (nest 2 $ text "=>" <+/> pprint' p names t ++ text ";") + +parens : Int -> Int -> Doc -> Doc +parens a b doc = if a < b + then text "(" ++ doc ++ text ")" + else doc + +pprint' p names (Bnd _ k) = case getAt (cast k) names of + -- Either a bug or we're printing without names + Nothing => text "BND:\{show k}" + Just nm => text "\{nm}:\{show k}" +pprint' p names (Ref _ str mt) = text (show str) +pprint' p names (Meta _ k) = text "?m:\{show k}" +pprint' p names (Lam _ nm icit quant t) = parens 0 p $ nest 2 $ text "\\ \{show quant}\{nm} =>" <+/> pprint' 0 (nm :: names) t +pprint' p names (App _ t u) = parens 0 p $ pprint' 0 names t <+> pprint' 1 names u +pprint' p names (UU _) = text "U" +pprint' p names (Pi _ nm Auto rig t u) = parens 0 p $ + text "{{" ++ text (show rig) <+> text nm <+> text ":" <+> pprint' 0 names t <+> text "}}" <+> text "->" <+> pprint' 0 (nm :: names) u +pprint' p names (Pi _ nm Implicit rig t u) = parens 0 p $ + text "{" ++ text (show rig) <+> text nm <+> text ":" <+> pprint' 0 names t <+> text "}" <+> text "->" <+> pprint' 0 (nm :: names) u +pprint' p names (Pi _ "_" Explicit Many t u) = + parens 0 p $ pprint' 1 names t <+> text "->" <+> pprint' 0 ("_" :: names) u +pprint' p names (Pi _ nm Explicit rig t u) = parens 0 p $ + text "(" ++ text (show rig) <+> text nm <+> text ":" <+> pprint' 0 names t ++ text ")" <+> text "->" <+> pprint' 0 (nm :: names) u +-- FIXME - probably way wrong on the names here. There is implicit binding going on +pprint' p names (Case _ sc alts) = parens 0 p $ text "case" <+> pprint' 0 names sc <+> text "of" ++ (nest 2 (line ++ stack (map (pprintAlt 0 names) alts))) +pprint' p names (Lit _ lit) = text (show lit) +pprint' p names (Let _ nm t u) = parens 0 p $ text "let" <+> text nm <+> text ":=" <+> pprint' 0 names t <+> text "in" (nest 2 $ pprint' 0 (nm :: names) u) +pprint' p names (LetRec _ nm ty t u) = parens 0 p $ text "letrec" <+> text nm <+> text ":" <+> pprint' 0 names ty <+> text ":=" <+> pprint' 0 names t <+> text "in" (nest 2 $ pprint' 0 (nm :: names) u) +pprint' p names (Erased _) = text "ERASED" + +-- Pretty printer for Tm. + +pprint : List String -> Tm -> Doc +pprint names tm = pprint' 0 names tm + +Val : U + +-- IS/TypeTheory.idr is calling this a Kripke function space +-- Yaffle, IS/TypeTheory use a function here. +-- Kovacs, Idris use Env and Tm + +-- in cctt kovacs refers to this choice as defunctionalization vs HOAS +-- https://github.com/AndrasKovacs/cctt/blob/main/README.md#defunctionalization +-- the tradeoff is access to internals of the function + +-- Yaffle is vars -> vars here + +Closure : U + +data Val : U where + -- This will be local / flex with spine. + VVar : FC -> (k : Int) -> (sp : SnocList Val) -> Val + VRef : FC -> (nm : QName) -> Def -> (sp : SnocList Val) -> Val + -- neutral case + VCase : FC -> (sc : Val) -> List CaseAlt -> Val + -- we'll need to look this up in ctx with IO + VMeta : FC -> (ix : Int) -> (sp : SnocList Val) -> Val + VLam : FC -> Name -> Icit -> Quant -> Closure -> Val + VPi : FC -> Name -> Icit -> Quant -> (a : Val) -> (b : Closure) -> Val + VLet : FC -> Name -> Val -> Val -> Val + VLetRec : FC -> Name -> Val -> Val -> Val -> Val + VU : FC -> Val + VErased : FC -> Val + VLit : FC -> Literal -> Val + +Env : U +Env = List Val + +data Mode = CBN | CBV + +data Closure = MkClosure Env Tm + +getValFC : Val -> FC +getValFC (VVar fc _ _) = fc +getValFC (VRef fc _ _ _) = fc +getValFC (VCase fc _ _) = fc +getValFC (VMeta fc _ _) = fc +getValFC (VLam fc _ _ _ _) = fc +getValFC (VPi fc _ _ _ a b) = fc +getValFC (VU fc) = fc +getValFC (VErased fc) = fc +getValFC (VLit fc _) = fc +getValFC (VLet fc _ _ _) = fc +getValFC (VLetRec fc _ _ _ _) = fc + +instance HasFC Val where getFC = getValFC + +showClosure : Closure → String + +instance Show Val where + show (VVar _ k Lin) = "%var\{show k}" + show (VVar _ k sp) = "(%var\{show k} \{unwords $ map show (sp <>> Nil)})" + show (VRef _ nm _ Lin) = show nm + show (VRef _ nm _ sp) = "(\{show nm} \{unwords $ map show (sp <>> Nil)})" + show (VMeta _ ix sp) = "(%meta \{show ix} (\{show $ snoclen sp} sp :: Nil))" + show (VLam _ str icit quant x) = "(%lam \{show quant}\{str} \{showClosure x})" + show (VPi fc str Implicit rig x y) = "(%pi {\{show rig} \{str} : \{show x}}. \{showClosure y})" + show (VPi fc str Explicit rig x y) = "(%pi (\{show rig} \{str} : \{show x}). \{showClosure y})" + show (VPi fc str Auto rig x y) = "(%pi {{\{show rig} \{str} : \{show x}}}. \{showClosure y})" + show (VCase fc sc alts) = "(%case \{show sc} ...)" + show (VU _) = "U" + show (VLit _ lit) = show lit + show (VLet _ nm a b) = "(%let \{show nm} = \{show a} in \{show b}" + show (VLetRec _ nm ty a b) = "(%letrec \{show nm} : \{show ty} = \{show a} in \{show b}" + show (VErased _) = "ERASED" + + +showClosure (MkClosure xs t) = "(%cl (\{show $ length xs} env :: Nil) \{show t})" + +-- instance Show Closure where +-- show = showClosure + +Context : U + +data MetaKind = Normal | User | AutoSolve + +instance Show MetaKind where + show Normal = "Normal" + show User = "User" + show AutoSolve = "Auto" + +-- constrain meta applied to val to be a val + +data MConstraint = MkMc FC Env (SnocList Val) Val + +data MetaEntry = Unsolved FC Int Context Val MetaKind (List MConstraint) | Solved FC Int Val + +record MetaContext where + constructor MC + metas : List MetaEntry + next : Int + +data Def = Axiom | TCon (List QName) | DCon Int QName | Fn Tm | PrimTCon + | PrimFn String (List String) + +instance Show Def where + show Axiom = "axiom" + show (TCon strs) = "TCon \{show strs}" + show (DCon k tyname) = "DCon \{show k} \{show tyname}" + show (Fn t) = "Fn \{show t}" + show (PrimTCon) = "PrimTCon" + show (PrimFn src used) = "PrimFn \{show src} \{show used}" + +-- entry in the top level context + +record TopEntry where + constructor MkEntry + fc : FC + name : QName + type : Tm + def : Def + +-- FIXME snoc + +instance Show TopEntry where + show (MkEntry fc name type def) = "\{show name} : \{show type} := \{show def}" + +-- Top level context. +-- Most of the reason this is separate is to have a different type +-- `Def` for the entries. +-- +-- The price is that we have names in addition to levels. Do we want to +-- expand these during normalization? + +record TopContext where + constructor MkTop + -- We'll add a map later? + defs : SortedMap QName TopEntry + metaCtx : IORef MetaContext + verbose : Bool -- command line flag + errors : IORef (List Error) + -- loaded modules + loaded : List String + ops : Operators + +-- we'll use this for typechecking, but need to keep a TopContext around too. + +record Context where + constructor MkCtx + lvl : Int + -- shall we use lvl as an index? + env : Env -- Values in scope + types : List (String × Val) -- types and names in scope + -- so we'll try "bds" determines length of local context + bds : List BD -- bound or defined + + -- FC to use if we don't have a better option + ctxFC : FC + +-- add a binding to environment + +extend : Context -> String -> Val -> Context +extend (MkCtx lvl env types bds ctxFC) name ty = + MkCtx (1 + lvl) (VVar emptyFC lvl Lin :: env) ((name,ty) :: types) (Bound :: bds) ctxFC + +-- I guess we define things as values? + +define : Context -> String -> Val -> Val -> Context +define (MkCtx lvl env types bds ctxFC) name val ty = + MkCtx (1 + lvl) (val :: env) ((name,ty) :: types) (Defined :: bds) ctxFC + +instance Show MetaEntry where + show (Unsolved pos k ctx ty kind constraints) = "Unsolved \{show pos} \{show k} \{show kind} : \{show ty} \{show ctx.bds} cs \{show $ length constraints}" + show (Solved _ k x) = "Solved \{show k} \{show x}" + +withPos : Context -> FC -> Context +withPos (MkCtx lvl env types bds ctxFC) fc = (MkCtx lvl env types bds fc) + +names : Context -> List String +names ctx = map fst ctx.types + +-- public export +-- M : U -> U +-- M = (StateT TopContext (EitherT Error IO)) + +record M a where + constructor MkM + runM : TopContext -> IO (Either Error (TopContext × a)) + +instance Functor M where + map f (MkM run) = MkM $ \tc => bind {IO} (run tc) $ \case + Left err => pure $ Left err + Right (tc', a) => pure $ Right (tc', f a) + +instance Applicative M where + return x = MkM $ \tc => pure $ Right (tc, x) + (MkM f) <*> (MkM x) = MkM $ \tc => bind {IO} (f tc) $ \case + Left err => pure $ Left err + Right (tc', f') => bind {IO} (x tc') $ \case + Left err => pure $ Left err + Right (tc'', x') => pure $ Right (tc'', f' x') + +instance Monad M where + pure = return + bind (MkM x) f = MkM $ \tc => bind {IO} (x tc) $ \case + Left err => pure $ Left err + Right (tc', a) => runM (f a) tc' + +instance HasIO M where + liftIO io = MkM $ \tc => do + result <- io + pure $ Right (tc, result) + +throwError : ∀ a. Error -> M a +throwError err = MkM $ \_ => pure $ Left err + +catchError : ∀ a. M a -> (Error -> M a) -> M a +catchError (MkM ma) handler = MkM $ \tc => bind {IO} (ma tc) $ \case + Left err => runM (handler err) tc + Right (tc', a) => pure $ Right (tc', a) + +tryError : ∀ a. M a -> M (Either Error a) +tryError ma = catchError (map Right ma) (pure ∘ Left) + +get : M TopContext +get = MkM $ \ tc => pure $ Right (tc, tc) + +put : TopContext -> M Unit +put tc = MkM $ \_ => pure $ Right (tc, MkUnit) + +modify : (TopContext -> TopContext) -> M Unit +modify f = do + tc <- get + put (f tc) + +-- Force argument and print if verbose is true + +debug : Lazy String -> M Unit +debug x = do + top <- get + when top.verbose $ \ _ => putStrLn $ force x + +info : FC -> String -> M Unit +info fc msg = putStrLn "INFO at \{show fc}: \{msg}" + +-- Version of debug that makes monadic computation lazy + +debugM : M String -> M Unit +debugM x = do + top <- get + when top.verbose $ \ _ => do + msg <- x + putStrLn msg + +instance Show Context where + show ctx = "Context \{show $ map fst $ ctx.types}" + +errorMsg : Error -> String +errorMsg (E x str) = str +errorMsg (Postpone x k str) = str + +instance HasFC Error where + getFC (E x str) = x + getFC (Postpone x k str) = x + +error : ∀ a. FC -> String -> M a +error fc msg = throwError $ E fc msg + +error' : ∀ a. String -> M a +error' msg = throwError $ E emptyFC msg + +freshMeta : Context -> FC -> Val -> MetaKind -> M Tm +freshMeta ctx fc ty kind = do + top <- get + mc <- readIORef top.metaCtx + debug $ \ _ => "fresh meta \{show mc.next} : \{show ty} (\{show kind})" + writeIORef top.metaCtx $ MC (Unsolved fc mc.next ctx ty kind Nil :: mc.metas) (1 + mc.next) + pure $ applyBDs 0 (Meta fc mc.next) ctx.bds + where + -- hope I got the right order here :) + applyBDs : Int -> Tm -> List BD -> Tm + applyBDs k t Nil = t + -- review the order here + applyBDs k t (Bound :: xs) = App emptyFC (applyBDs (1 + k) t xs) (Bnd emptyFC k) + applyBDs k t (Defined :: xs) = applyBDs (1 + k) t xs + +lookupMeta : Int -> M MetaEntry +lookupMeta ix = do + top <- get + mc <- readIORef top.metaCtx + go mc.metas + where + go : List MetaEntry -> M MetaEntry + go Nil = error' "Meta \{show ix} not found" + go (meta@(Unsolved _ k ys _ _ _) :: xs) = if k == ix then pure meta else go xs + go (meta@(Solved _ k x) :: xs) = if k == ix then pure meta else go xs + +-- we need more of topcontext later - Maybe switch it up so we're not passing +-- around top + +mkCtx : FC -> Context +mkCtx fc = MkCtx 0 Nil Nil Nil fc diff --git a/done/Lib/Util.newt b/done/Lib/Util.newt new file mode 100644 index 0000000..e3de96b --- /dev/null +++ b/done/Lib/Util.newt @@ -0,0 +1,26 @@ +module Lib.Util + +import Lib.Types + + +funArgs : Tm -> (Tm × List Tm) +funArgs tm = go tm Nil + where + go : Tm -> List Tm -> (Tm × List Tm) + go (App _ t u) args = go t (u :: args) + go t args = (t, args) + +data Binder : U where + MkBind : FC -> String -> Icit -> Quant -> Tm -> Binder + +-- I don't have a show for terms without a name list + +instance Show Binder where + show (MkBind _ nm icit quant t) = "(\{show quant}\{nm} \{show icit} : ... :: Nil)" + +splitTele : Tm -> (Tm × List Binder) +splitTele = go Nil + where + go : List Binder -> Tm -> (Tm × List Binder) + go ts (Pi fc nm icit quant t u) = go (MkBind fc nm icit quant t :: ts) u + go ts tm = (tm, reverse ts) diff --git a/done/Prelude.newt b/done/Prelude.newt new file mode 120000 index 0000000..74c953c --- /dev/null +++ b/done/Prelude.newt @@ -0,0 +1 @@ +../newt/Prelude.newt \ No newline at end of file diff --git a/newt/Prelude.newt b/newt/Prelude.newt index a1266c2..c817484 100644 --- a/newt/Prelude.newt +++ b/newt/Prelude.newt @@ -6,6 +6,10 @@ id x = x the : (a : U) → a → a the _ a = a +const : ∀ a b. a → b → a +const a b = a + + data Bool = True | False not : Bool → Bool @@ -121,15 +125,20 @@ cong : {A B : U} {a b : A} -> (f : A -> B) -> a ≡ b -> f a ≡ f b sym : {A : U} -> {a b : A} -> a ≡ b -> b ≡ a sym Refl = Refl + + -- Functor class Functor (m : U → U) where map : {0 a b} → (a → b) → m a → m b -infixr 4 _<$>_ +infixr 4 _<$>_ _<$_ _<$>_ : {0 f} {{Functor f}} {0 a b} → (a → b) → f a → f b f <$> ma = map f ma +_<$_ : ∀ f a b. {{Functor f}} → b → f a → f b +a <$ b = const a <$> b + instance Functor Maybe where map f Nothing = Nothing map f (Just a) = Just (f a) @@ -161,8 +170,6 @@ class Applicative (f : U → U) where return : {0 a} → a → f a _<*>_ : {0 a b} -> f (a → b) → f a → f b -const : ∀ a b. a → b → a -const a b = a _<*_ : ∀ f a b. {{Applicative f}} → f a → f b → f a fa <* fb = return const <*> fa <*> fb @@ -448,10 +455,16 @@ pfunc stringToInt : String → Int := `(s) => { return rval }` +-- TODO - add Foldable + foldl : ∀ A B. (B -> A -> B) -> B -> List A -> B foldl f acc Nil = acc foldl f acc (x :: xs) = foldl f (f acc x) xs +foldr : ∀ a b. (a → b → b) → b → List a → b +foldr f b Nil = b +foldr f b (x :: xs) = f x (foldr f b xs) + infixl 9 _∘_ _∘_ : {A B C : U} -> (B -> C) -> (A -> B) -> A -> C (f ∘ g) x = f (g x) @@ -830,3 +843,9 @@ ignore = map (const MkUnit) instance ∀ a. {{Show a}} → Show (Maybe a) where show Nothing = "Nothing" show (Just a) = "Just {show a}" + + +-- TODO + +pfunc isPrefixOf uses (True False): String → String → Bool := `(pfx, s) => s.startsWith(pfx) ? True : False` +pfunc strIndex : String → Int → Char := `(s, ix) => s[ix]` diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index 6fcac14..85e93ef 100644 --- a/src/Lib/Parser.idr +++ b/src/Lib/Parser.idr @@ -46,8 +46,10 @@ stringLit = do -- typeExpr is term with arrows. -export typeExpr : Parser Raw -export term : (Parser Raw) +export +typeExpr : Parser Raw +export +term : (Parser Raw) interp : Parser Raw interp = token StartInterp *> term <* token EndInterp @@ -86,8 +88,8 @@ lit = intLit <|> interpString <|> stringLit <|> charLit -- helpful when we've got some / many and need FC for each -withPos : Parser a -> Parser (FC, a) -withPos pa = (,) <$> getPos <*> pa +addPos : Parser a -> Parser (FC, a) +addPos pa = (,) <$> getPos <*> pa asAtom : Parser Raw asAtom = do @@ -118,6 +120,7 @@ pArg = do <|> (Implicit,fc,) <$> braces typeExpr <|> (Auto,fc,) <$> dbraces typeExpr +AppSpine : Type AppSpine = List (Icit,FC,Raw) pratt : Operators -> Int -> String -> Raw -> AppSpine -> Parser (Raw, AppSpine) @@ -163,7 +166,9 @@ pratt ops prec stop left spine = do runRule : Int -> Fixity -> String -> List String -> Raw -> AppSpine -> Parser (Raw,AppSpine) runRule p fix stop [] left spine = pure (left,spine) runRule p fix stop [""] left spine = do - let pr = case fix of InfixR => p; _ => p + 1 + let pr = case fix of + InfixR => p + _ => p + 1 case spine of ((_, fc, right) :: rest) => do (right, rest) <- pratt ops pr stop right rest @@ -239,7 +244,7 @@ lamExpr : Parser Raw lamExpr = do pos <- getPos keyword "\\" <|> keyword "λ" - args <- some $ withPos pLamArg + args <- some $ addPos pLamArg keyword "=>" scope <- typeExpr pure $ foldr (\(fc, icit, name, ty), sc => RLam pos (BI fc name icit Many) sc) scope args @@ -304,7 +309,7 @@ doArrow : Parser DoStmt doArrow = do fc <- getPos left <- typeExpr - Just _ <- optional $ keyword "<-" + (Just _) <- optional $ keyword "<-" | _ => pure $ DoExpr fc left right <- term alts <- startBlock $ manySame $ sym "|" *> caseAlt @@ -360,7 +365,7 @@ ebind = do -- don't commit until we see the ":" sym "(" quant <- quantity - names <- try (some (withPos varname) <* sym ":") + names <- try (some (addPos varname) <* sym ":") ty <- typeExpr sym ")" pure $ map (\(pos, name) => (BI pos name Explicit quant, ty)) names @@ -370,7 +375,7 @@ ibind = do -- I've gone back and forth on this, but I think {m a b} is more useful than {Nat} sym "{" quant <- quantity - names <- (some (withPos varname)) + names <- (some (addPos varname)) ty <- optional (sym ":" *> typeExpr) sym "}" pure $ map (\(pos,name) => (BI pos name Implicit quant, fromMaybe (RImplicit pos) ty)) names @@ -379,7 +384,7 @@ abind : Parser Telescope abind = do -- for this, however, it would be nice to allow {{Monad A}} sym "{{" - name <- optional $ try (withPos varname <* sym ":") + name <- optional $ try (addPos varname <* sym ":") ty <- typeExpr sym "}}" case name of @@ -394,7 +399,7 @@ arrow = sym "->" <|> sym "→" forAll : Parser Raw forAll = do keyword "forall" <|> keyword "∀" - all <- some (withPos varname) + all <- some (addPos varname) keyword "." scope <- typeExpr pure $ foldr (\ (fc, n), sc => RPi fc (BI fc n Implicit Zero) (RImplicit fc) sc) scope all @@ -517,7 +522,7 @@ parseData = do nakedBind : Parser Telescope nakedBind = do - names <- some (withPos varname) + names <- some (addPos varname) pure $ map (\(pos,name) => (BI pos name Explicit Many, RImplicit pos)) names export @@ -605,6 +610,7 @@ data ReplCmd = -- Eventually I'd like immediate actions in the file, like lean, but I -- also want to REPL to work and we can do that first. -export parseRepl : Parser ReplCmd +export +parseRepl : Parser ReplCmd parseRepl = Def <$> parseDecl <|> Norm <$ keyword "#nf" <*> typeExpr <|> Check <$ keyword "#check" <*> typeExpr