wip

- `@[fail] def foo = ...` succeeds if `foo` has some error.
- `@[fail "scope"] def foo = ...` succeeds if `foo` has some error
  containing the word "scope" somewhere
- `@[fail] namespace foo { }` works too and the error must be anywhere
  in the namespace

examples/fail.quox

@@ -0,0 +1,10 @@
+#[fail "but cases for"]
+def missing-b : {a, b} → {a} =
+  λ x ⇒ case x return {a} of { 'a ⇒ 'a }
+
+#[fail "duplicate arms"]
+def repeat-enum-case : {a} → {a} =
+  λ x ⇒ case x return {a} of { 'a ⇒ 'a; 'a ⇒ 'a }
+
+#[fail "duplicate tags"]
+def repeat-enum-type : {a, a} = 'a

lib/Quox/Equal.idr

@@ -424,7 +424,7 @@ namespace Elim
                      Eff EqualElim (Term 0 n)
   computeElimTypeE defs ectx sg e =
     let Val n = ectx.termLen in
-    lift $ computeElimType defs (toWhnfContext ectx) sg e
+    lift $ computeElimType defs (toWhnfContext ectx) e {ne}
 
   private
   putError : Has InnerErrEff fs => Error -> Eff fs ()

lib/Quox/Parser/FromParser.idr

@@ -3,6 +3,7 @@ module Quox.Parser.FromParser
 
 import public Quox.Parser.FromParser.Error as Quox.Parser.FromParser
 
+import Quox.Pretty
 import Quox.Parser.Syntax
 import Quox.Parser.Parser
 import public Quox.Parser.LoadFile
@@ -42,6 +43,35 @@ FromParserIO : List (Type -> Type)
 FromParserIO = LoadFile :: FromParserPure
 
 
+export
+fromParserPure : NameSuf -> Definitions ->
+                 Eff FromParserPure a ->
+                 Either Error (a, NameSuf, Definitions)
+fromParserPure suf defs act = runSTErr $ do
+  suf  <- liftST $ newSTRef suf
+  defs <- liftST $ newSTRef defs
+  res  <- runEff act $ with Union.(::)
+    [handleExcept (\e => stLeft e),
+     handleStateSTRef defs,
+     handleStateSTRef !(liftST $ newSTRef [<]),
+     handleStateSTRef suf]
+  pure (res, !(liftST $ readSTRef suf), !(liftST $ readSTRef defs))
+
+
+export covering
+fromParserIO : (MonadRec io, HasIO io) =>
+               IncludePath -> IORef SeenSet ->
+               IORef NameSuf -> IORef Definitions ->
+               Eff FromParserIO a -> io (Either Error a)
+fromParserIO inc seen suf defs act = liftIO $ fromIOErr $ do
+  runEff act $ with Union.(::)
+    [handleLoadFileIOE LoadError seen inc,
+     handleExcept (\e => ioLeft e),
+     handleStateIORef defs,
+     handleStateIORef !(newIORef [<]),
+     handleStateIORef suf]
+
+
 parameters {auto _ : Functor m} (b : Var n -> m a) (f : PName -> m a)
            (xs : Context' PatVar n)
   private
@@ -151,7 +181,7 @@ mutual
       map E $ CaseEnum (fromPQty pi)
         <$> fromPTermElim ds ns tag
         <*> fromPTermTScope ds ns [< r] ret
-        <*> assert_total fromPTermEnumArms ds ns arms
+        <*> assert_total fromPTermEnumArms loc ds ns arms
         <*> pure loc
 
     Nat loc => pure $ Nat loc
@@ -166,12 +196,11 @@ mutual
         <*> fromPTermTScope ds ns [< s, ih] suc
         <*> pure loc
 
-    Enum strs loc =>
-      let set = SortedSet.fromList strs in
-      if length strs == length (SortedSet.toList set) then
-        pure $ Enum set loc
-      else
-        throw $ DuplicatesInEnum loc strs
+    Enum strs loc => do
+      let set = SortedSet.fromList strs
+      unless (length strs == length (SortedSet.toList set)) $
+        throw $ DuplicatesInEnumType loc strs
+      pure $ Enum set loc
 
     Tag str loc => pure $ Tag str loc
 
@@ -229,12 +258,15 @@ mutual
         <*> pure loc
 
   private
-  fromPTermEnumArms : Context' PatVar d -> Context' PatVar n ->
+  fromPTermEnumArms : Loc -> Context' PatVar d -> Context' PatVar n ->
                       List (PTagVal, PTerm) ->
                       Eff FromParserPure (CaseEnumArms d n)
-  fromPTermEnumArms ds ns =
-    map SortedMap.fromList .
-    traverse (bitraverse (pure . fromPTagVal) (fromPTermWith ds ns))
+  fromPTermEnumArms loc ds ns arms = do
+    res <- SortedMap.fromList <$>
+           traverse (bitraverse (pure . fromPTagVal) (fromPTermWith ds ns)) arms
+    unless (length (keys res) == length arms) $
+      throw $ DuplicatesInEnumCase loc (map (fromPTagVal . fst) arms)
+    pure res
 
   private
   fromPTermElim : Context' PatVar d -> Context' PatVar n ->
@@ -318,12 +350,43 @@ fromPDef (MkPDef qty pname ptype pterm defLoc) = do
       res <- liftTC $ inferC empty sqty elim
       addDef name gqty res.type term defLoc
 
+
+public export
+data HasFail = NoFail | AnyFail | FailWith String
+
+export
+hasFail : List PDeclMod -> HasFail
+hasFail []                  = NoFail
+hasFail (PFail str _ :: _)  = maybe AnyFail FailWith str
+
 export covering
 fromPDecl : PDecl -> Eff FromParserPure (List NDefinition)
-fromPDecl (PDef def) = singleton <$> fromPDef def
-fromPDecl (PNs  ns)  =
+
+export covering
+fromPDeclBody : PDeclBody -> Eff FromParserPure (List NDefinition)
+fromPDeclBody (PDef def) = singleton <$> fromPDef def
+fromPDeclBody (PNs  ns)  =
   localAt NS (<+> ns.name) $ concat <$> traverse fromPDecl ns.decls
 
+export covering
+expectFail : PDeclBody -> Eff FromParserPure Error
+expectFail body =
+  case fromParserPure !(getAt GEN) !(getAt DEFS) $ fromPDeclBody body of
+    Left  err => pure err
+    Right _   => throw $ ExpectedFail body.loc
+
+
+fromPDecl (MkPDecl mods decl loc) = case hasFail mods of
+  NoFail       => fromPDeclBody decl
+  AnyFail      => expectFail decl $> []
+  FailWith str => do
+    err <- expectFail decl
+    let msg = runPretty $ prettyError False err {opts = Opts 10_000} -- w/e
+    if str `isInfixOf` renderInfinite msg
+       then pure []
+       else throw $ WrongFail str err loc
+
+
 mutual
   export covering
   loadProcessFile : Loc -> String -> Eff FromParserIO (List NDefinition)
@@ -339,32 +402,3 @@ mutual
   fromPTopLevel : PTopLevel -> Eff FromParserIO (List NDefinition)
   fromPTopLevel (PD    decl)     = lift $ fromPDecl decl
   fromPTopLevel (PLoad file loc) = loadProcessFile loc file
-
-
-export
-fromParserPure : NameSuf -> Definitions ->
-                 Eff FromParserPure a ->
-                 Either Error (a, NameSuf, Definitions)
-fromParserPure suf defs act = runSTErr $ do
-  suf  <- liftST $ newSTRef suf
-  defs <- liftST $ newSTRef defs
-  res  <- runEff act $ with Union.(::)
-    [handleExcept (\e => stLeft e),
-     handleStateSTRef defs,
-     handleStateSTRef !(liftST $ newSTRef [<]),
-     handleStateSTRef suf]
-  pure (res, !(liftST $ readSTRef suf), !(liftST $ readSTRef defs))
-
-
-export covering
-fromParserIO : (MonadRec io, HasIO io) =>
-               IncludePath -> IORef SeenSet ->
-               IORef NameSuf -> IORef Definitions ->
-               Eff FromParserIO a -> io (Either Error a)
-fromParserIO inc seen suf defs act = liftIO $ fromIOErr $ do
-  runEff act $ with Union.(::)
-    [handleLoadFileIOE LoadError seen inc,
-     handleExcept (\e => ioLeft e),
-     handleStateIORef defs,
-     handleStateIORef !(newIORef [<]),
-     handleStateIORef suf]

lib/Quox/Parser/FromParser/Error.idr

@@ -22,7 +22,8 @@ ParseError = Parser.Error
 public export
 data Error =
     AnnotationNeeded Loc (NameContexts d n) (Term d n)
-  | DuplicatesInEnum Loc (List TagVal)
+  | DuplicatesInEnumType Loc (List TagVal)
+  | DuplicatesInEnumCase Loc (List TagVal)
   | TermNotInScope Loc Name
   | DimNotInScope Loc PBaseName
   | QtyNotGlobal Loc Qty
@@ -30,18 +31,22 @@ data Error =
   | DisplacedBoundVar Loc PName
   | WrapTypeError TypeError
   | LoadError Loc FilePath FileError
+  | ExpectedFail Loc
+  | WrongFail String Error Loc
   | WrapParseError String ParseError
 
 
 export
 prettyLexError : {opts : _} -> String -> LexError -> Eff Pretty (Doc opts)
 prettyLexError file (Err reason line col char) = do
-  let loc = makeLoc file (MkBounds line col line col)
   reason <- case reason of
-    EndInput    => pure "unexpected end of input"
-    NoRuleApply => pure $ text "unrecognised character: \{show char}"
+    Other msg => pure $ text msg
+    NoRuleApply => case char of
+      Just char => pure $ text "unrecognised character: \{show char}"
+      Nothing   => pure $ text "unexpected end of input"
     ComposeNotClosing (sl, sc) (el, ec) => pure $
       hsep ["unterminated token at", !(prettyBounds (MkBounds sl sc el ec))]
+  let loc = makeLoc file (MkBounds line col line col)
   pure $ vappend !(prettyLoc loc) reason
 
 export
@@ -62,19 +67,23 @@ prettyParseError file (ParseError errs) =
     traverse (map ("-" <++>) . prettyParseError1 file) (toList errs)
 
 
-parameters (showContext : Bool)
+parameters {opts : LayoutOpts} (showContext : Bool)
   export
-  prettyError : {opts : _} -> Error -> Eff Pretty (Doc opts)
+  prettyError : Error -> Eff Pretty (Doc opts)
   prettyError (AnnotationNeeded loc ctx tm) =
     [|vappend (prettyLoc loc)
         (hangD "type annotation needed on"
                !(prettyTerm ctx.dnames ctx.tnames tm))|]
     -- [todo] print the original PTerm instead
 
-  prettyError (DuplicatesInEnum loc tags) =
+  prettyError (DuplicatesInEnumType loc tags) =
     [|vappend (prettyLoc loc)
         (hangD "duplicate tags in enum type" !(prettyEnum tags))|]
 
+  prettyError (DuplicatesInEnumCase loc tags) =
+    [|vappend (prettyLoc loc)
+        (hangD "duplicate arms in enum case" !(prettyEnum tags))|]
+
   prettyError (DimNotInScope loc i) =
     [|vappend (prettyLoc loc)
         (pure $ hsep ["dimension", !(hl DVar $ text i), "not in scope"])|]
@@ -106,5 +115,13 @@ parameters (showContext : Bool)
           "couldn't load file" <++> text file,
           text $ show err]
 
+  prettyError (ExpectedFail loc) = pure $
+    sep [!(prettyLoc loc), "expected error"]
+
+  prettyError (WrongFail str err loc) = pure $
+    sep [!(prettyLoc loc),
+         "wrong error, expected to match", !(hl Tag $ text "\"\{str}\""),
+         "but got", !(prettyError err)]
+
   prettyError (WrapParseError file err) =
     prettyParseError file err

lib/Quox/Parser/Lexer.idr

@@ -34,16 +34,27 @@ data Token =
   | Sup Nat
 %runElab derive "Token" [Eq, Ord, Show]
 
--- token or whitespace
+||| token or whitespace
+||| @ Skip whitespace, comments, etc
+||| @ Invalid a token which failed a post-lexer check
+|||           (e.g. a qualified name containing a keyword)
+||| @ T a well formed token
 public export
-0 TokenW : Type
-TokenW = Maybe Token
+data ExtToken = Skip | Invalid String String | T Token
+%runElab derive "ExtToken" [Eq, Ord, Show]
 
 
+public export
+data ErrorReason =
+    NoRuleApply
+  | ComposeNotClosing (Int, Int) (Int, Int)
+  | Other String
+%runElab derive "ErrorReason" [Eq, Ord, Show]
+
 public export
 record Error where
   constructor Err
-  reason    : StopReason
+  reason    : ErrorReason
   line, col : Int
   ||| `Nothing` if the error is at the end of the input
   char      : Maybe Char
@@ -52,19 +63,14 @@ record Error where
 
 
 private
-skip : Lexer -> Tokenizer TokenW
-skip t = match t $ const Nothing
+skip : Lexer -> Tokenizer ExtToken
+skip t = match t $ const Skip
 
 private
-match : Lexer -> (String -> Token) -> Tokenizer TokenW
-match t f = Tokenizer.match t (Just . f)
-%hide Tokenizer.match
+tmatch : Lexer -> (String -> Token) -> Tokenizer ExtToken
+tmatch t f = match t (T . f)
 
 
-private
-name : Tokenizer TokenW
-name = match name $ Name . fromListP . split (== '.') . normalizeNfc
-
 ||| [todo] escapes other than `\"` and (accidentally) `\\`
 export
 fromStringLit : String -> String
@@ -76,17 +82,17 @@ fromStringLit = pack . go . unpack . drop 1 . dropLast 1 where
   go (c :: cs)         = c :: go cs
 
 private
-string : Tokenizer TokenW
-string = match stringLit (Str . fromStringLit)
+string : Tokenizer ExtToken
+string = tmatch stringLit (Str . fromStringLit)
 
 private
-nat : Tokenizer TokenW
-nat = match (some (range '0' '9')) (Nat . cast)
+nat : Tokenizer ExtToken
+nat = tmatch (some (range '0' '9')) (Nat . cast)
 
 private
-tag : Tokenizer TokenW
-tag = match (is '\'' <+> name)      (Tag . drop 1)
-  <|> match (is '\'' <+> stringLit) (Tag . fromStringLit . drop 1)
+tag : Tokenizer ExtToken
+tag = tmatch (is '\'' <+> name)      (Tag . drop 1)
+  <|> tmatch (is '\'' <+> stringLit) (Tag . fromStringLit . drop 1)
 
 
 
@@ -112,17 +118,17 @@ supToNat = cast . pack . map fromSup . unpack
 
 -- ★0, Type0. base ★/Type is a Reserved
 private
-universe : Tokenizer TokenW
+universe : Tokenizer ExtToken
 universe = universeWith "★" <|> universeWith "Type" where
-  universeWith : String -> Tokenizer TokenW
+  universeWith : String -> Tokenizer ExtToken
   universeWith pfx =
     let len = length pfx in
-    match (exact pfx <+> digits) (TYPE . cast . drop len)
+    tmatch (exact pfx <+> digits) (TYPE . cast . drop len)
 
 private
-sup : Tokenizer TokenW
-sup = match (some $ pred isSupDigit) (Sup . supToNat)
-  <|> match (is '^' <+> digits)      (Sup . cast . drop 1)
+sup : Tokenizer ExtToken
+sup = tmatch (some $ pred isSupDigit) (Sup . supToNat)
+  <|> tmatch (is '^' <+> digits)      (Sup . cast . drop 1)
 
 
 private %inline
@@ -134,9 +140,11 @@ namespace Reserved
   ||| description of a reserved symbol
   ||| @ Word a reserved word (must not be followed by letters, digits, etc)
   ||| @ Sym a reserved symbol (must not be followed by symbolic chars)
-  ||| @ Punc a character that doesn't show up in names (brackets, etc)
+  ||| @ Punc a character that doesn't show up in names (brackets, etc);
+  |||        also a sequence ending in one of those, like `#[`, since the
+  |||        difference relates to lookahead
   public export
-  data Reserved1 = Word String | Sym String | Punc Char
+  data Reserved1 = Word String | Sym String | Punc String
   %runElab derive "Reserved1" [Eq, Ord, Show]
 
   ||| description of a token that might have unicode & ascii-only aliases
@@ -145,17 +153,14 @@ namespace Reserved
   %runElab derive "Reserved" [Eq, Ord, Show]
 
   public export
-  Sym1, Word1 : String -> Reserved
-  Sym1 = Only . Sym
+  Sym1, Word1, Punc1 : String -> Reserved
+  Sym1  = Only . Sym
   Word1 = Only . Word
-
-  public export
-  Punc1 : Char -> Reserved
   Punc1 = Only . Punc
 
 public export
 resString1 : Reserved1 -> String
-resString1 (Punc x) = singleton x
+resString1 (Punc x) = x
 resString1 (Word w) = w
 resString1 (Sym  s) = s
 
@@ -166,17 +171,23 @@ resString : Reserved -> String
 resString (Only r)   = resString1 r
 resString (r `Or` _) = resString1 r
 
+||| return both representative strings for a token description
+public export
+resString2 : Reserved -> List String
+resString2 (Only r)   = [resString1 r]
+resString2 (r `Or` s) = [resString1 r, resString1 s]
+
 private
-resTokenizer1 : Reserved1 -> String -> Tokenizer TokenW
+resTokenizer1 : Reserved1 -> String -> Tokenizer ExtToken
 resTokenizer1 r str =
   let res : String -> Token := const $ Reserved str in
-  case r of Word w => match (exact w <+> reject idContEnd) res
-            Sym s  => match (exact s <+> reject symCont)   res
-            Punc x => match (is x)                         res
+  case r of Word w => tmatch (exact w <+> reject idContEnd) res
+            Sym  s => tmatch (exact s <+> reject symCont)   res
+            Punc x => tmatch (exact x)                      res
 
 ||| match a reserved token
 export
-resTokenizer : Reserved -> Tokenizer TokenW
+resTokenizer : Reserved -> Tokenizer ExtToken
 resTokenizer (Only r)   = resTokenizer1 r (resString1 r)
 resTokenizer (r `Or` s) =
   resTokenizer1 r (resString1 r) <|> resTokenizer1 s (resString1 r)
@@ -188,8 +199,8 @@ resTokenizer (r `Or` s) =
 public export
 reserved : List Reserved
 reserved =
-  [Punc1 '(', Punc1 ')', Punc1 '[', Punc1 ']', Punc1 '{', Punc1 '}',
-   Punc1 ',', Punc1 ';',
+  [Punc1 "(", Punc1 ")", Punc1 "[", Punc1 "]", Punc1 "{", Punc1 "}",
+   Punc1 ",", Punc1 ";", Punc1 "#[",
    Sym1 "@",
    Sym1 ":",
    Sym "⇒" `Or` Sym "=>",
@@ -197,7 +208,7 @@ reserved =
    Sym "×" `Or` Sym "**",
    Sym "≡" `Or` Sym "==",
    Sym "∷" `Or` Sym "::",
-   Punc1 '.',
+   Punc1 ".",
    Word1 "case",
    Word1 "case0", Word1 "case1",
    Word "caseω" `Or` Word "case#",
@@ -220,14 +231,31 @@ reserved =
    Word1 "load",
    Word1 "namespace"]
 
+public export
+reservedStrings : List String
+reservedStrings = map resString reserved
+
+public export
+allReservedStrings : List String
+allReservedStrings = foldMap resString2 reserved
+
 ||| `IsReserved str` is true if `Reserved str` might actually show up in
 ||| the token stream
 public export
 IsReserved : String -> Type
-IsReserved str = str `Elem` map resString reserved
+IsReserved str = So (str `elem` allReservedStrings)
+
+private
+name : Tokenizer ExtToken
+name =
+  match name $ \str =>
+    let parts = split (== '.') $ normalizeNfc str in
+    case find (`elem` allReservedStrings) (toList parts) of
+      Nothing => T $ Name $ fromListP parts
+      Just w  => Invalid "reserved word '\{w}' inside name \{str}" str
 
 export
-tokens : Tokenizer TokenW
+tokens : Tokenizer ExtToken
 tokens = choice $
   map skip [pred isWhitespace,
             lineComment (exact "--" <+> reject symCont),
@@ -236,10 +264,24 @@ tokens = choice $
   map resTokenizer reserved <+>
   [sup, nat, string, tag, name]
 
+export
+check : Alternative f =>
+        WithBounds ExtToken -> Either Error (f (WithBounds Token))
+check (MkBounded val irr bounds@(MkBounds line col _ _)) = case val of
+  Skip            => Right empty
+  T tok           => Right $ pure $ MkBounded tok irr bounds
+  Invalid msg tok => Left  $ Err (Other msg) line col (index 0 tok)
+
+export
+toErrorReason : StopReason -> Maybe ErrorReason
+toErrorReason EndInput                = Nothing
+toErrorReason NoRuleApply             = Just NoRuleApply
+toErrorReason (ComposeNotClosing s e) = Just $ ComposeNotClosing s e
+
 export
 lex : String -> Either Error (List (WithBounds Token))
 lex str =
   let (res, reason, line, col, str) = lex tokens str in
-  case reason of
-    EndInput => Right $ mapMaybe sequence res
-    _        => Left  $ Err {reason, line, col, char = index 0 str}
+  case toErrorReason reason of
+    Nothing => concatMap check res @{MonoidApplicative}
+    Just e  => Left $ Err {reason = e, line, col, char = index 0 str}

lib/Quox/Parser/Parser.idr

@@ -149,6 +149,12 @@ export
 qty : FileName -> Grammar True PQty
 qty fname = withLoc fname [|PQ qtyVal|]
 
+export
+exactName : String -> Grammar True ()
+exactName name = terminal "expected '\{name}'" $ \case
+  Name (MakePName [<] x) => guard $ x == name
+  _                      => Nothing
+
 
 ||| pattern var (unqualified name or _)
 export
@@ -576,6 +582,15 @@ term fname = lamTerm fname
          <|> sigmaTerm fname
 
 
+export
+pragma : Grammar True a -> Grammar True a
+pragma p = resC "#[" *> p <* mustWork (resC "]")
+
+export
+declMod : FileName -> Grammar True PDeclMod
+declMod fname = withLoc fname $ pragma $
+  exactName "fail" *> [|PFail $ optional strLit|]
+
 export
 decl : FileName -> Grammar True PDecl
 
@@ -610,7 +625,11 @@ where
   nsInner = [] <$ resC "}"
         <|> [|(assert_total decl fname <* commit) :: assert_total nsInner|]
 
-decl fname = [|PDef $ definition fname|] <|> [|PNs $ namespace_ fname|]
+export
+declBody : FileName -> Grammar True PDeclBody
+declBody fname = [|PDef $ definition fname|] <|> [|PNs $ namespace_ fname|]
+
+decl fname = withLoc fname [|MkPDecl (many $ declMod fname) (declBody fname)|]
 
 export
 load : FileName -> Grammar True PTopLevel

lib/Quox/Parser/Syntax.idr

@@ -153,6 +153,12 @@ record PDefinition where
 
 export Located PDefinition where def.loc = def.loc_
 
+public export
+data PDeclMod =
+    PFail (Maybe String) Loc
+%name PDeclMod mod
+%runElab derive "PDeclMod" [Eq, Ord, Show]
+
 mutual
   public export
   record PNamespace where
@@ -163,18 +169,27 @@ mutual
   %name PNamespace ns
 
   public export
-  data PDecl =
-      PDef PDefinition
-    | PNs  PNamespace
-  %name PDecl decl
-%runElab deriveMutual ["PNamespace", "PDecl"] [Eq, Ord, Show]
+  record PDecl where
+    constructor MkPDecl
+    mods : List PDeclMod
+    decl : PDeclBody
+    loc_ : Loc
+
+  public export
+  data PDeclBody =
+      PDef  PDefinition
+    | PNs   PNamespace
+  %name PDeclBody decl
+%runElab deriveMutual ["PNamespace", "PDecl", "PDeclBody"] [Eq, Ord, Show]
 
 export Located PNamespace where ns.loc = ns.loc_
 
+export Located PDecl where decl.loc = decl.loc_
+
 export
-Located PDecl where
-  (PDef def).loc = def.loc
-  (PNs  ns).loc  = ns.loc
+Located PDeclBody where
+  (PDef  def).loc  = def.loc
+  (PNs   ns).loc   = ns.loc
 
 public export
 data PTopLevel = PD PDecl | PLoad String Loc

lib/Quox/Typing/Context.idr

@@ -73,7 +73,7 @@ namespace TContext
   zeroFor : Context tm n -> QOutput n
   zeroFor ctx = Zero <$ ctx
 
-private
+public export
 extendLen : Telescope a n1 n2 -> Singleton n1 -> Singleton n2
 extendLen [<]        x = x
 extendLen (tel :< _) x = [|S $ extendLen tel x|]

lib/Quox/Untyped/Erase.idr

@@ -4,10 +4,18 @@ import Quox.Definition
 import Quox.Syntax.Term.Base as Q
 import Quox.Syntax.Term.Subst
 import Quox.Untyped.Syntax as U
+import Quox.Typing.Context
+import Quox.Whnf
 
-import Control.Eff
+import Quox.EffExtra
+import Data.Singleton
+import Data.SnocVect
+import Language.Reflection
 
 %default total
+%language ElabReflection
+
+%hide TT.Name
 
 
 public export
@@ -27,38 +35,131 @@ EContext = Context' IsErased
 public export
 record ErasureContext d n where
   constructor MkEContexts
-  dnames : Context' Binder d
-  tnames : Context' Binder n
+  {auto dimLen : Singleton d}
+  {auto termLen : Singleton n}
+  dnames : BContext d
+  tnames : BContext n
+  tctx   : TContext d n
   erased : EContext n
 %name ErasureContext ctx
 
 
+public export
+TypeError : Type
+TypeError = Typing.Error.Error
+%hide Typing.Error.Error
+
 public export
 data Error =
   CompileTimeOnly (ErasureContext d n) (Q.Term d n)
-| Expected String (ErasureContext d n) (Q.Term d n)
 | ErasedVar       (ErasureContext d n) (Var n)
 | NotInScope      Name
+| WrapTypeError   TypeError
 
 public export
 Erase : List (Type -> Type)
-Erase = [Except Error, Reader Definitions]
+Erase = [Except Error, DefsReader, NameGen]
 
 
 export
-extendTy : Binder -> Qty -> ErasureContext d n -> ErasureContext d (S n)
-extendTy x pi (MkEContexts dnames tnames erased) =
-  MkEContexts dnames (tnames :< x) (erased :< isErased pi)
+toWhnfContext : ErasureContext d n -> WhnfContext d n
+toWhnfContext (MkEContexts {dnames, tnames, tctx, _}) =
+  MkWhnfContext {dnames, tnames, tctx}
 
 export
-extendDim : Binder -> ErasureContext d n -> ErasureContext (S d) n
-extendDim i (MkEContexts dnames tnames erased) =
-  MkEContexts (dnames :< i) tnames erased
+(.names) : ErasureContext d n -> NameContexts d n
+ctx.names = MkNameContexts ctx.dnames ctx.tnames
 
 
-private %inline
-(.bname) : Scoped 1 _ _ -> Binder
-t.bname = Bind t.name.val
+export
+liftWhnf : Eff Whnf a -> Eff Erase a
+liftWhnf act = runEff act
+  [\x => send x, \case (Err e) => throw $ WrapTypeError e]
+
+export covering
+whnf0 : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
+        ErasureContext d n -> SQty ->
+        tm d n -> Eff Erase (tm d n)
+whnf0 ctx sg tm = do
+  let Val n = ctx.termLen; Val d = ctx.dimLen
+  liftWhnf $ whnf0 !(askAt DEFS) (toWhnfContext ctx) sg tm
+
+export covering
+computeElimType : ErasureContext d n -> SQty -> Elim d n -> Eff Erase (Term d n)
+computeElimType ctx sg e = do
+  let Val n = ctx.termLen; Val d = ctx.dimLen
+      ctx   = toWhnfContext ctx
+  defs          <- askAt DEFS
+  Element e enf <- liftWhnf $ whnf defs ctx sg e
+  liftWhnf $ computeElimType defs ctx e {ne = enf}
+
+
+parameters (ctx : ErasureContext d n) (loc : Loc)
+  private covering %macro
+  expect : (forall d, n. Loc -> NameContexts d n -> Term d n -> TypeError) ->
+           TTImp -> TTImp -> Elab (Term d n -> Eff Erase a)
+  expect k l r = do
+    f <- check `(\case ~(l) => Just ~(r); _ => Nothing)
+    pure $ \t =>
+      let err = throw $ WrapTypeError $ k loc ctx.names t in
+      maybe err pure . f =<< whnf0 ctx SZero t
+
+  export covering %inline
+  expectTYPE : Term d n -> Eff Erase Universe
+  expectTYPE = expect ExpectedTYPE `(TYPE {l, _}) `(l)
+
+  export covering %inline
+  expectPi : Term d n -> Eff Erase (Qty, Term d n, ScopeTerm d n)
+  expectPi = expect ExpectedPi `(Pi {qty, arg, res, _}) `((qty, arg, res))
+
+  export covering %inline
+  expectSig : Term d n -> Eff Erase (Term d n, ScopeTerm d n)
+  expectSig = expect ExpectedSig `(Sig {fst, snd, _}) `((fst, snd))
+
+  export covering %inline
+  expectEnum : Term d n -> Eff Erase (SortedSet TagVal)
+  expectEnum = expect ExpectedEnum `(Enum {cases, _}) `(cases)
+
+  export covering %inline
+  expectEq : Term d n -> Eff Erase (DScopeTerm d n, Term d n, Term d n)
+  expectEq = expect ExpectedEq `(Eq {ty, l, r, _}) `((ty, l, r))
+
+  export covering %inline
+  expectNat : Term d n -> Eff Erase ()
+  expectNat = expect ExpectedNat `(Nat {}) `(())
+
+  export covering %inline
+  expectBOX : Term d n -> Eff Erase (Qty, Term d n)
+  expectBOX = expect ExpectedBOX `(BOX {qty, ty, _}) `((qty, ty))
+
+
+export
+extendTyN : CtxExtension d n1 n2 ->
+            ErasureContext d n1 -> ErasureContext d n2
+extendTyN tel (MkEContexts {termLen, dnames, tnames, tctx, erased}) =
+  let (qs, xs, ss) = unzip3 tel in
+  MkEContexts {
+    dnames,
+    tnames  = tnames . xs,
+    tctx    = tctx . ss,
+    erased  = erased . map isErased qs,
+    termLen = extendLen tel termLen
+  }
+
+export
+extendTy : Qty -> BindName -> Term d n ->
+           ErasureContext d n -> ErasureContext d (S n)
+extendTy pi x ty = extendTyN [< (pi, x, ty)]
+
+export
+extendDim : BindName -> ErasureContext d n -> ErasureContext (S d) n
+extendDim i (MkEContexts {dimLen, dnames, tnames, tctx, erased}) =
+  MkEContexts {
+    tnames, erased,
+    dimLen = [|S dimLen|],
+    dnames = dnames :< i,
+    tctx   = map (dweakT 1) tctx
+  }
 
 
 export covering
@@ -66,7 +167,8 @@ eraseTerm : ErasureContext d n ->
             (ty, tm : Q.Term d n) -> Eff Erase (U.Term n)
 
 export covering
-eraseElim : ErasureContext d n -> (tm : Q.Elim d n) -> Eff Erase (U.Term n)
+eraseElim : ErasureContext d n -> (tm : Q.Elim d n) ->
+            Eff Erase (Q.Term d n, U.Term n)
 
 eraseTerm ctx _ s@(TYPE {}) =
   throw $ CompileTimeOnly ctx s
@@ -75,8 +177,7 @@ eraseTerm ctx _ s@(Pi {}) =
   throw $ CompileTimeOnly ctx s
 
 eraseTerm ctx ty (Lam body loc) = do
-  let Pi {qty, arg, res, _} = ty
-    | _ => throw $ Expected "function type" ctx ty
+  (qty, arg, res) <- expectPi ctx loc ty
   case isErased qty of
     Erased => do
       -- replace with a fake name like "<erased x>"
@@ -85,53 +186,54 @@ eraseTerm ctx ty (Lam body loc) = do
           dummy = F (unq $ UN "<erased \{name}>") 0 noLoc
       eraseTerm ctx (sub1 res dummy) (sub1 body dummy)
     Kept => do
-      let x = body.bname
-      U.Lam x <$> eraseTerm (extendTy x qty ctx) res.term body.term
+      let x = body.name
+      body <- eraseTerm (extendTy qty x arg ctx) res.term body.term
+      pure $ U.Lam x body loc
 
 eraseTerm ctx _ s@(Sig {}) =
   throw $ CompileTimeOnly ctx s
 
 eraseTerm ctx ty (Pair fst snd loc) = do
-  let Sig {fst = a, snd = b, _} = ty
-    | _ => throw $ Expected "pair type" ctx ty
+  (a, b) <- expectSig ctx loc ty
   let b = sub1 b (Ann fst a a.loc)
-  [|eraseTerm ctx a fst `Pair` eraseTerm ctx b snd|]
+  fst <- eraseTerm ctx a fst
+  snd <- eraseTerm ctx b snd
+  pure $ Pair fst snd loc
 
 eraseTerm ctx _ s@(Enum {}) =
   throw $ CompileTimeOnly ctx s
 
 eraseTerm ctx _ (Tag tag loc) =
-  pure $ Tag tag
+  pure $ Tag tag loc
 
 eraseTerm ctx ty s@(Eq {}) =
   throw $ CompileTimeOnly ctx s
 
 eraseTerm ctx ty (DLam body loc) = do
-  let Eq {ty = a, _} = ty
-    | _ => throw $ Expected "equality type" ctx ty
-  eraseTerm (extendDim body.bname ctx) a.term body.term
+  (a, _, _) <- expectEq ctx loc ty
+  eraseTerm (extendDim body.name ctx) a.term body.term
 
 eraseTerm ctx _ s@(Nat {}) =
   throw $ CompileTimeOnly ctx s
 
 eraseTerm _ _ (Zero loc) =
-  pure Zero
+  pure $ Zero loc
 
-eraseTerm ctx ty (Succ p loc) =
-  [|Succ $ eraseTerm ctx ty p|]
+eraseTerm ctx ty (Succ p loc) = do
+  p <- eraseTerm ctx ty p
+  pure $ Succ p loc
 
 eraseTerm ctx ty s@(BOX {}) =
   throw $ CompileTimeOnly ctx s
 
 eraseTerm ctx ty (Box val loc) = do
-  let BOX {qty, ty = a, _} = ty
-    | _ => throw $ Expected "box type" ctx ty
+  (qty, a) <- expectBOX ctx loc ty
   case isErased qty of
-    Erased => pure ErasedBox -- lmao
+    Erased => pure $ ErasedBox loc -- lmao
     Kept   => eraseTerm ctx a val
 
 eraseTerm ctx ty (E e) =
-  eraseElim ctx e
+  snd <$> eraseElim ctx e
 
 eraseTerm ctx ty (CloT  (Sub term th)) =
   eraseTerm ctx ty $ pushSubstsWith' id th term
@@ -140,41 +242,91 @@ eraseTerm ctx ty (DCloT (Sub term th)) =
   eraseTerm ctx ty $ pushSubstsWith' th id term
 
 eraseElim ctx e@(F x u loc) = do
-  Just def <- asks $ lookup x
+  Just def <- asksAt DEFS $ lookup x
     | Nothing => throw $ NotInScope x
   case isErased def.qty.qty of
     Erased => throw $ CompileTimeOnly ctx $ E e
-    Kept   => pure  $ F x
+    Kept =>
+      let Val d = ctx.dimLen; Val n = ctx.termLen in
+      pure (def.type, F x loc)
 
 eraseElim ctx e@(B i loc) = do
   case ctx.erased !!! i of
     Erased => throw $ CompileTimeOnly ctx $ E e
-    Kept   => pure  $ B i
+    Kept   => pure (ctx.tctx !! i, B i loc)
 
-eraseElim ctx (App fun arg loc) = ?eraseElim_rhs_2
+eraseElim ctx (App fun arg loc) = do
+  (tfun, fun)       <- eraseElim ctx fun
+  (qty, targ, tres) <- expectPi ctx loc tfun
+  let ty = sub1 tres (Ann arg targ arg.loc)
+  case isErased qty of
+    Erased => pure (ty, fun)
+    Kept   => do arg <- eraseTerm ctx targ arg
+                 pure (ty, App fun arg loc)
 
-eraseElim ctx (CasePair qty pair ret body loc) = ?eraseElim_rhs_3
+eraseElim ctx (CasePair qty pair ret body loc) = do
+  ty <- computeElimType ctx SOne pair
+  eraseElim ctx $
+    Ann (subN body [< Fst pair pair.loc, Snd pair pair.loc])
+        (sub1 ret pair) loc
 
-eraseElim ctx (Fst pair loc) = ?eraseElim_rhs_4
+eraseElim ctx (Fst pair loc) = do
+  (ty, pair) <- eraseElim ctx pair
+  (a,  _)    <- expectSig ctx loc ty
+  pure (a, Fst pair loc)
 
-eraseElim ctx (Snd pair loc) = ?eraseElim_rhs_5
+eraseElim ctx (Snd pair0 loc) = do
+  (ty, pair) <- eraseElim ctx pair0
+  (_,  b)    <- expectSig ctx loc ty
+  pure (sub1 b (Fst pair0 loc), Snd pair loc)
 
-eraseElim ctx (CaseEnum qty tag ret arms loc) = ?eraseElim_rhs_6
+eraseElim ctx e@(CaseEnum qty tag ret arms loc) =
+  case isErased qty of
+    Erased => case SortedMap.toList arms of
+      []         => pure (sub1 ret tag, Absurd loc)
+      [(_, arm)] => let ty = sub1 ret tag in (ty,) <$> eraseTerm ctx ty arm
+      _          => throw $ CompileTimeOnly ctx $ E e
+    Kept => do
+      let ty = sub1 ret tag
+      (tagTy, tag) <- eraseElim ctx tag
+      arms <- for (SortedMap.toList arms) $ \(t, rhs) =>
+        (t,) <$> eraseTerm ctx (sub1 ret $ Ann (Tag t loc) tagTy loc) rhs
+      pure (ty, CaseEnum tag arms loc)
 
-eraseElim ctx (CaseNat qty qtyIH nat ret zero succ loc) = ?eraseElim_rhs_7
+eraseElim ctx (CaseNat qty qtyIH nat ret zero succ loc) = do
+  let ty = sub1 ret nat
+  (_, nat) <- eraseElim ctx nat
+  zero <- eraseTerm ctx (sub1 ret (Ann (Zero loc) (Nat loc) loc)) zero
+  let [< p, ih] = succ.names
+  succ <- eraseTerm
+    (extendTyN [< (qty, p, Nat loc),
+                  (qtyIH, ih, sub1 (ret // shift 1) (BV 0 loc))] ctx)
+    (sub1 (ret // shift 2) (Ann (Succ (BVT 1 loc) loc) (Nat loc) loc))
+    succ.term
+  pure (ty, CaseNat nat zero p ih succ loc)
 
-eraseElim ctx (CaseBox qty box ret body loc) = ?eraseElim_rhs_8
+eraseElim ctx (CaseBox qty box ret body loc) = do
+  let ty = sub1 ret box
+  body <- eraseTerm ctx ty $ sub1 body box
+  pure (ty, body)
 
-eraseElim ctx (DApp fun arg loc) = ?eraseElim_rhs_9
+eraseElim ctx (DApp fun arg loc) = do
+  (tfun, fun) <- eraseElim ctx fun
+  (a, _, _)   <- expectEq ctx loc tfun
+  pure (dsub1 a arg, fun)
 
 eraseElim ctx (Ann tm ty loc) =
-  eraseTerm ctx ty tm
+  (ty,) <$> eraseTerm ctx ty tm
 
-eraseElim ctx (Coe ty p q val loc) = ?eraseElim_rhs_11
+eraseElim ctx (Coe ty p q val loc) = do
+  val <- eraseTerm ctx (dsub1 ty q) val
+  pure (dsub1 ty p, val)
 
-eraseElim ctx (Comp ty p q val r zero one loc) = ?eraseElim_rhs_12
+eraseElim ctx (Comp ty p q val r zero one loc) =
+  (ty,) <$> eraseTerm ctx ty val
 
-eraseElim ctx (TypeCase ty ret arms def loc) = ?eraseElim_rhs_13
+eraseElim ctx t@(TypeCase ty ret arms def loc) =
+  throw $ CompileTimeOnly ctx $ E t
 
 eraseElim ctx (CloE (Sub term th)) =
   eraseElim ctx $ pushSubstsWith' id th term

lib/Quox/Untyped/Syntax.idr

@@ -4,10 +4,12 @@ import Quox.Var
 import Quox.Context
 import Quox.Name
 import Quox.Pretty
+import Quox.Syntax.Subst
 
 import Data.Vect
 import Data.DPair
 import Data.SortedMap
+import Data.SnocVect
 import Derive.Prelude
 %hide TT.Name
 
@@ -15,40 +17,54 @@ import Derive.Prelude
 %language ElabReflection
 
 
-public export
-data Binder = Bind BaseName
-Eq Binder where _ == _ = True
-Ord Binder where compare _ _ = EQ
-%runElab derive "Binder" [Show]
-
 public export
 data Term : Nat -> Type where
-  F : (x : Name) -> Term n
-  B : (i : Var n) -> Term n
+  F : (x : Name) -> Loc -> Term n
+  B : (i : Var n) -> Loc -> Term n
 
-  Lam : (x : Binder) -> (body : Term (S n)) -> Term n
-  App : (fun, arg : Term n) -> Term n
+  Lam : (x : BindName) -> (body : Term (S n)) -> Loc -> Term n
+  App : (fun, arg : Term n) -> Loc -> Term n
 
-  Pair : (fst, snd : Term n) -> Term n
-  Fst : (pair : Term n) -> Term n
-  Snd : (pair : Term n) -> Term n
+  Pair : (fst, snd : Term n) -> Loc -> Term n
+  Fst : (pair : Term n) -> Loc -> Term n
+  Snd : (pair : Term n) -> Loc -> Term n
 
-  Tag : (tag : String) -> Term n
-  CaseEnum : (tag : Term n) -> (cases : List (String, Term n)) -> Term n
+  Tag : (tag : String) -> Loc -> Term n
+  CaseEnum : (tag : Term n) -> (cases : List (String, Term n)) -> Loc -> Term n
+  ||| empty match with an erased head
+  Absurd : Loc -> Term n
 
-  Zero : Term n
-  Succ : (nat : Term n) -> Term n
+  Zero : Loc -> Term n
+  Succ : (nat : Term n) -> Loc -> Term n
   CaseNat : (nat : Term n) ->
             (zer : Term n) ->
-            (x, ih : Binder) -> (suc : Term (2 + n)) ->
+            (x, ih : BindName) -> (suc : Term (2 + n)) ->
+            Loc ->
             Term n
 
-  ||| replacement for terms of type [0.A], for now
-  ErasedBox : Term n
+  Erased : Loc -> Term n
 %name Term s, t, u
 %runElab deriveIndexed "Term" [Eq, Ord, Show]
 
 
+export
+Located (Term n) where
+  (F x loc).loc                      = loc
+  (B i loc).loc                      = loc
+  (Lam x body loc).loc               = loc
+  (App fun arg loc).loc              = loc
+  (Pair fst snd loc).loc             = loc
+  (Fst pair loc).loc                 = loc
+  (Snd pair loc).loc                 = loc
+  (Tag tag loc).loc                  = loc
+  (CaseEnum tag cases loc).loc       = loc
+  (Absurd loc).loc                   = loc
+  (Zero loc).loc                     = loc
+  (Succ nat loc).loc                 = loc
+  (CaseNat nat zer x ih suc loc).loc = loc
+  (Erased loc).loc                   = loc
+
+
 public export
 0 Definitions : Type
 Definitions = SortedMap Name $ Term 0
@@ -56,37 +72,33 @@ Definitions = SortedMap Name $ Term 0
 
 parameters {opts : LayoutOpts}
   export
-  prettyBind : Binder -> Eff Pretty (Doc opts)
-  prettyBind (Bind x) = hl TVar $ text $ baseStr x
+  prettyTerm : BContext n -> Term n -> Eff Pretty (Doc opts)
 
   export
-  prettyTerm : Context' Binder n -> Term n -> Eff Pretty (Doc opts)
-
-  export
-  prettyArg : Context' Binder n -> Term n -> Eff Pretty (Doc opts)
+  prettyArg : BContext n -> Term n -> Eff Pretty (Doc opts)
   prettyArg xs arg = withPrec Arg $ prettyTerm xs arg
 
   export
-  prettyApp' : Context' Binder n -> Doc opts -> Term n -> Eff Pretty (Doc opts)
+  prettyApp' : Context' BindName n -> Doc opts -> Term n -> Eff Pretty (Doc opts)
   prettyApp' xs fun arg =
     parensIfM App =<< do
       arg <- prettyArg xs arg
       pure $ sep [fun, arg]
 
   export
-  prettyApp : Context' Binder n -> Term n -> Term n -> Eff Pretty (Doc opts)
+  prettyApp : Context' BindName n -> Term n -> Term n -> Eff Pretty (Doc opts)
   prettyApp xs fun arg = prettyApp' xs !(prettyArg xs fun) arg
 
   public export
   PrettyCaseArm : Nat -> Type
-  PrettyCaseArm n = Exists $ \s => (Vect s Binder, Term (s + n))
+  PrettyCaseArm n = Exists $ \s => (Vect s BindName, Term (s + n))
 
   export %inline
-  caseArm : Vect s Binder -> Term (s + n) -> PrettyCaseArm n
+  caseArm : Vect s BindName -> Term (s + n) -> PrettyCaseArm n
   caseArm xs t = Evidence _ (xs, t)
 
   export
-  prettyCase : Context' Binder n ->
+  prettyCase : Context' BindName n ->
                (a -> Eff Pretty (Doc opts)) ->
                Term n -> List (a, PrettyCaseArm n) ->
                Eff Pretty (Doc opts)
@@ -100,30 +112,81 @@ parameters {opts : LayoutOpts}
       body <- braces $ separateLoose !semiD cases
       pure $ sep [header, body]
 
-  prettyTerm _  (F x) = prettyFree x
-  prettyTerm xs (B i) = prettyBind $ xs !!! i
-  prettyTerm xs (Lam x body) =
+  prettyTerm _  (F x _) = prettyFree x
+  prettyTerm xs (B i _) = prettyTBind $ xs !!! i
+  prettyTerm xs (Lam x body _) =
     parensIfM Outer =<< do
-      header <- hsep <$> sequence [lamD, prettyBind x, darrowD]
+      header <- hsep <$> sequence [lamD, prettyTBind x, darrowD]
       body   <- withPrec Outer $ prettyTerm (xs :< x) body
       hangDSingle header body
-  prettyTerm xs (App fun arg) = prettyApp xs fun arg
-  prettyTerm xs (Pair fst snd) =
+  prettyTerm xs (App fun arg _) = prettyApp xs fun arg
+  prettyTerm xs (Pair fst snd _) =
     parens =<< separateTight !commaD <$>
       sequence {t = List} [prettyTerm xs fst, prettyTerm xs snd]
-  prettyTerm xs (Fst pair) = prettyApp' xs !fstD pair
-  prettyTerm xs (Snd pair) = prettyApp' xs !sndD pair
-  prettyTerm xs (Tag tag) = prettyTag tag
-  prettyTerm xs (CaseEnum tag cases) = assert_total
+  prettyTerm xs (Fst pair _) = prettyApp' xs !fstD pair
+  prettyTerm xs (Snd pair _) = prettyApp' xs !sndD pair
+  prettyTerm xs (Tag tag _) = prettyTag tag
+  prettyTerm xs (CaseEnum tag cases _) = assert_total
     prettyCase xs prettyTag tag $ map (mapSnd $ caseArm []) cases
-  prettyTerm xs Zero = zeroD
-  prettyTerm xs (Succ nat) = prettyApp' xs !succD nat
-  prettyTerm xs (CaseNat nat zer x ih suc) = assert_total
+  prettyTerm xs (Absurd _) = hl Syntax "absurd"
+  prettyTerm xs (Zero _) = zeroD
+  prettyTerm xs (Succ nat _) = prettyApp' xs !succD nat
+  prettyTerm xs (CaseNat nat zer x ih suc _) = assert_total
     prettyCase xs pure nat
       [(!zeroD,  caseArm []      zer),
        (!sucPat, caseArm [x, ih] suc)]
     where
       sucPat = separateTight {t = List} !commaD <$>
-               sequence [[|succD <++> prettyBind x|], prettyBind ih]
-  prettyTerm _ ErasedBox =
+               sequence [[|succD <++> prettyTBind x|], prettyTBind ih]
+  prettyTerm _ (Erased _) =
     hl Syntax =<< ifUnicode "⌷" "[]"
+
+
+public export
+USubst : Nat -> Nat -> Type
+USubst = Subst Term
+
+
+public export FromVar Term where fromVarLoc = B
+
+
+public export
+CanSubstSelf Term where
+  s // th = case s of
+    F x loc =>
+      F x loc
+    B i loc =>
+      getLoc th i loc
+    Lam x body loc =>
+      Lam x (assert_total $ body // push th) loc
+    App fun arg loc =>
+      App (fun // th) (arg // th) loc
+    Pair fst snd loc =>
+      Pair (fst // th) (snd // th) loc
+    Fst pair loc =>
+      Fst (pair // th) loc
+    Snd pair loc =>
+      Snd (pair // th) loc
+    Tag tag loc =>
+      Tag tag loc
+    CaseEnum tag cases loc =>
+      CaseEnum (tag // th) (map (assert_total mapSnd (// th)) cases) loc
+    Absurd loc =>
+      Absurd loc
+    Zero loc =>
+      Zero loc
+    Succ nat loc =>
+      Succ (nat // th) loc
+    CaseNat nat zer x ih suc loc =>
+      CaseNat (nat // th) (zer // th)
+              x ih (assert_total $ suc // pushN 2 th) loc
+    Erased loc =>
+      Erased loc
+
+public export
+subN : SnocVect s (Term n) -> Term (s + n) -> Term n
+subN th t = t // fromSnocVect th
+
+public export
+sub1 : Term n -> Term (S n) -> Term n
+sub1 e = subN [< e]

lib/Quox/Whnf/ComputeElimType.idr

@@ -14,8 +14,8 @@ export covering
 computeElimType : CanWhnf Term Interface.isRedexT =>
                   CanWhnf Elim Interface.isRedexE =>
                   {d, n : Nat} ->
-                  (defs : Definitions) -> WhnfContext d n -> (pi : SQty) ->
-                  (e : Elim d n) -> (0 ne : No (isRedexE defs pi e)) =>
+                  (defs : Definitions) -> WhnfContext d n ->
+                  (e : Elim d n) -> (0 ne : No (isRedexE defs sg e)) =>
                   Eff Whnf (Term d n)
 
 
@@ -24,11 +24,11 @@ export covering
 computeWhnfElimType0 : CanWhnf Term Interface.isRedexT =>
                        CanWhnf Elim Interface.isRedexE =>
                        {d, n : Nat} ->
-                       (defs : Definitions) -> WhnfContext d n -> (pi : SQty) ->
-                       (e : Elim d n) -> (0 ne : No (isRedexE defs pi e)) =>
+                       (defs : Definitions) -> WhnfContext d n ->
+                       (e : Elim d n) -> (0 ne : No (isRedexE defs sg e)) =>
                        Eff Whnf (Term d n)
 
-computeElimType defs ctx pi e {ne} =
+computeElimType defs ctx e {ne} =
   case e of
     F x u loc => do
       let Just def = lookup x defs
@@ -39,7 +39,7 @@ computeElimType defs ctx pi e {ne} =
       pure $ ctx.tctx !! i
 
     App f s loc =>
-      case !(computeWhnfElimType0 defs ctx pi f {ne = noOr1 ne}) of
+      case !(computeWhnfElimType0 defs ctx f {ne = noOr1 ne}) of
         Pi {arg, res, _} => pure $ sub1 res $ Ann s arg loc
         ty               => throw $ ExpectedPi loc ctx.names ty
 
@@ -47,12 +47,12 @@ computeElimType defs ctx pi e {ne} =
       pure $ sub1 ret pair
 
     Fst pair loc =>
-      case !(computeWhnfElimType0 defs ctx pi pair {ne = noOr1 ne}) of
+      case !(computeWhnfElimType0 defs ctx pair {ne = noOr1 ne}) of
         Sig {fst, _} => pure fst
         ty           => throw $ ExpectedSig loc ctx.names ty
 
     Snd pair loc =>
-      case !(computeWhnfElimType0 defs ctx pi pair {ne = noOr1 ne}) of
+      case !(computeWhnfElimType0 defs ctx pair {ne = noOr1 ne}) of
         Sig {snd, _} => pure $ sub1 snd $ Fst pair loc
         ty           => throw $ ExpectedSig loc ctx.names ty
 
@@ -66,7 +66,7 @@ computeElimType defs ctx pi e {ne} =
       pure $ sub1 ret box
 
     DApp {fun = f, arg = p, loc} =>
-      case !(computeWhnfElimType0 defs ctx pi f {ne = noOr1 ne}) of
+      case !(computeWhnfElimType0 defs ctx f {ne = noOr1 ne}) of
         Eq {ty, _} => pure $ dsub1 ty p
         t          => throw $ ExpectedEq loc ctx.names t
 
@@ -82,5 +82,5 @@ computeElimType defs ctx pi e {ne} =
     TypeCase {ret, _} =>
       pure ret
 
-computeWhnfElimType0 defs ctx pi e =
-  computeElimType defs ctx pi e >>= whnf0 defs ctx pi
+computeWhnfElimType0 defs ctx e =
+  computeElimType defs ctx e {sg} >>= whnf0 defs ctx SZero

lib/Quox/Whnf/Main.idr

@@ -157,7 +157,7 @@ CanWhnf Elim Interface.isRedexE where
           eqCoe defs ctx sg ty p' q' val p appLoc
       Right ndlh => case p of
         K e _ => do
-          Eq {l, r, ty, _} <- computeWhnfElimType0 defs ctx sg f
+          Eq {l, r, ty, _} <- computeWhnfElimType0 defs ctx f {ne = fnf}
             | ty => throw $ ExpectedEq ty.loc ctx.names ty
           whnf defs ctx sg $
             ends (Ann (setLoc appLoc l) ty.zero appLoc)

lib/Quox/Whnf/TypeCase.idr

@@ -39,7 +39,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
              Eff Whnf (Term d n, ScopeTerm d n)
   tycasePi (Pi {arg, res, _}) = pure (arg, res)
   tycasePi (E e) {tnf} = do
-    ty <- computeElimType defs ctx SZero e {ne = noOr2 tnf}
+    ty <- computeElimType defs ctx e {ne = noOr2 tnf}
     let loc  = e.loc
         narg = mnb "Arg" loc; nret = mnb "Ret" loc
         arg  = E $ typeCase1Y e ty KPi [< !narg, !nret] (BVT 1 loc) loc
@@ -57,7 +57,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
               Eff Whnf (Term d n, ScopeTerm d n)
   tycaseSig (Sig {fst, snd, _}) = pure (fst, snd)
   tycaseSig (E e) {tnf} = do
-    ty <- computeElimType defs ctx SZero e {ne = noOr2 tnf}
+    ty <- computeElimType defs ctx e {ne = noOr2 tnf}
     let loc  = e.loc
         nfst = mnb "Fst" loc; nsnd = mnb "Snd" loc
         fst  = E $ typeCase1Y e ty KSig [< !nfst, !nsnd] (BVT 1 loc) loc
@@ -75,7 +75,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
               Eff Whnf (Term d n)
   tycaseBOX (BOX {ty, _}) = pure ty
   tycaseBOX (E e) {tnf} = do
-    ty <- computeElimType defs ctx SZero e {ne = noOr2 tnf}
+    ty <- computeElimType defs ctx e {ne = noOr2 tnf}
     pure $ E $ typeCase1Y e ty KBOX [< !(mnb "Ty" e.loc)] (BVT 0 e.loc) e.loc
   tycaseBOX t = throw $ ExpectedBOX t.loc ctx.names t
 
@@ -87,7 +87,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
              Eff Whnf (Term d n, Term d n, DScopeTerm d n, Term d n, Term d n)
   tycaseEq (Eq {ty, l, r, _}) = pure (ty.zero, ty.one, ty, l, r)
   tycaseEq (E e) {tnf} = do
-    ty <- computeElimType defs ctx SZero e {ne = noOr2 tnf}
+    ty <- computeElimType defs ctx e {ne = noOr2 tnf}
     let loc   = e.loc
         names = traverse' (\x => mnb x loc) [< "A0", "A1", "A", "L", "R"]
         a0    = E $ typeCase1Y e ty KEq !names (BVT 4 loc) loc

lib/Text/PrettyPrint/Bernardy/Core/Decorate.idr

@@ -5,6 +5,7 @@ module Text.PrettyPrint.Bernardy.Core.Decorate
 
 import public Text.PrettyPrint.Bernardy.Core
 import Data.DPair
+import Data.String
 
 
 public export
@@ -43,3 +44,12 @@ decorateLayout h l@(MkLayout content stats) =
 export
 decorate : {opts : _} -> Highlight -> Doc opts -> Doc opts
 decorate h doc = doc >>= \l => pure (decorateLayout h l)
+
+
+||| render a doc with no line breaks at all
+export
+renderInfinite : Doc opts -> String
+renderInfinite (MkDoc (MkLayout content _) _) = unwords content where
+  unwords : SnocList String -> String
+  unwords [<]       = ""
+  unwords (xs :< x) = foldMap (++ " ") xs ++ x

tests/Tests/Lexer.idr

@@ -47,7 +47,12 @@ tests = "lexer" :- [
     lexes "    " [],
     lexes "-- line comment" [],
     lexes "name -- line comment" [Name "name"],
-    lexes "-- line comment\nnameBetween -- and another" [Name "nameBetween"],
+    lexes
+      """
+      -- line comment
+      nameBetween -- and another
+      """
+      [Name "nameBetween"],
     lexes "{- block comment -}" [],
     lexes "{- {- nested -} block comment -}" []
   ],
@@ -70,13 +75,14 @@ tests = "lexer" :- [
     lexes "normalïse" [Name "normalïse"],
       -- ↑ replace i + combining ¨ with precomposed ï
     lexes "map#" [Name "map#"],
+    lexes "map#[" [Name "map#", Reserved "["], -- don't actually do this
+    lexes "map #[" [Name "map", Reserved "#["],
     lexes "write!" [Name "write!"],
     lexes "uhh??!?!?!?" [Name "uhh??!?!?!?"],
 
-    todo "check for reserved words in a qname",
-    skip $
-    lexes "abc.fun.def"
-      [Name "abc", Reserved ".", Reserved "λ", Reserved ".", Name "def"],
+    lexFail "abc.fun.ghi",
+    lexFail "abc.λ.ghi",
+    lexFail "abc.ω.ghi",
 
     lexes "+" [Name "+"],
     lexes "*" [Name "*"],

tests/Tests/Parser.idr

@@ -424,33 +424,46 @@ tests = "parser" :- [
 
   "top level" :- [
     parseMatch input "def0 A : ★⁰ = {}; def0 B : ★¹ = A;"
-      `([PD $ PDef $ MkPDef (PQ Zero _) "A" (Just $ TYPE 0 _) (Enum [] _) _,
-         PD $ PDef $ MkPDef (PQ Zero _) "B" (Just $ TYPE 1 _) (V "A" {}) _]),
+      `([PD $ MkPDecl []
+          (PDef $ MkPDef (PQ Zero _) "A" (Just $ TYPE 0 _) (Enum [] _) _) _,
+         PD $ MkPDecl []
+          (PDef $ MkPDef (PQ Zero _) "B" (Just $ TYPE 1 _) (V "A" {}) _) _]),
     parseMatch input "def0 A : ★⁰ = {} def0 B : ★¹ = A" $
-      `([PD $ PDef $ MkPDef (PQ Zero _) "A" (Just $ TYPE 0 _) (Enum [] _) _,
-         PD $ PDef $ MkPDef (PQ Zero _) "B" (Just $ TYPE 1 _) (V "A" {}) _]),
+      `([PD $ MkPDecl []
+          (PDef $ MkPDef (PQ Zero _) "A" (Just $ TYPE 0 _) (Enum [] _) _) _,
+         PD $ MkPDecl []
+          (PDef $ MkPDef (PQ Zero _) "B" (Just $ TYPE 1 _) (V "A" {}) _) _]),
     note "empty input",
     parsesAs input "" [],
     parseFails input ";;;;;;;;;;;;;;;;;;;;;;;;;;",
     parseMatch input "namespace a {}"
-      `([PD $ PNs $ MkPNamespace [< "a"] [] _]),
+      `([PD $ MkPDecl [] (PNs $ MkPNamespace [< "a"] [] _) _]),
     parseMatch input "namespace a.b.c {}"
-      `([PD $ PNs $ MkPNamespace [< "a", "b", "c"] [] _]),
+      `([PD $ MkPDecl []
+          (PNs $ MkPNamespace [< "a", "b", "c"] [] _) _]),
     parseMatch input "namespace a {namespace b {}}"
-      `([PD $ PNs $ MkPNamespace [< "a"] [PNs $ MkPNamespace [< "b"] [] _] _]),
+      `([PD (MkPDecl []
+          (PNs $ MkPNamespace [< "a"]
+            [MkPDecl [] (PNs $ MkPNamespace [< "b"] [] _) _] _) _)]),
     parseMatch input "namespace a {def x = 't ∷ {t}}"
-      `([PD $ PNs $ MkPNamespace [< "a"]
-          [PDef $ MkPDef (PQ Any _) "x" Nothing
-              (Ann (Tag "t" _) (Enum ["t"] _) _) _] _]),
+      `([PD (MkPDecl []
+          (PNs $ MkPNamespace [< "a"]
+            [MkPDecl []
+              (PDef $ MkPDef (PQ Any _) "x" Nothing
+                (Ann (Tag "t" _) (Enum ["t"] _) _) _) _] _) _)]),
     parseMatch input "namespace a {def x = 't ∷ {t}} def y = a.x"
-      `([PD $ PNs $ MkPNamespace [< "a"]
-          [PDef $ MkPDef (PQ Any _) "x" Nothing
-              (Ann (Tag "t" _) (Enum ["t"] _) _) _] _,
-         PD $ PDef $ MkPDef (PQ Any _) "y" Nothing
-            (V (MakePName [< "a"] "x") {}) _]),
+      `([PD (MkPDecl []
+          (PNs $ MkPNamespace [< "a"]
+            [MkPDecl []
+              (PDef $ MkPDef (PQ Any _) "x" Nothing
+                             (Ann (Tag "t" _) (Enum ["t"] _) _) _) _] _) _),
+         PD (MkPDecl []
+          (PDef $ MkPDef (PQ Any _) "y" Nothing
+                         (V (MakePName [< "a"] "x") Nothing _) _) _)]),
     parseMatch input #" load "a.quox"; def b = a.b "#
       `([PLoad "a.quox" _,
-         PD $ PDef $ MkPDef (PQ Any _) "b" Nothing
-            (V (MakePName [< "a"] "b") {}) _])
+         PD (MkPDecl []
+           (PDef $ MkPDef (PQ Any _) "b" Nothing
+                          (V (MakePName [< "a"] "b") Nothing _) _) _)])
   ]
 ]