fix the other similar loops

closes #38, again

exe/Main.idr

@@ -1,22 +1,21 @@
 module Main
 
 import Quox.Syntax as Q
-import Quox.Parser
 import Quox.Definition as Q
-import Quox.Pretty
 import Quox.Untyped.Syntax as U
+import Quox.Parser
 import Quox.Untyped.Erase
 import Quox.Untyped.Scheme
+import Quox.Pretty
 import Options
 
-import Data.IORef
-import Data.SortedSet
-import Text.Show.PrettyVal
-import Text.Show.Pretty
 import System
 import System.File
+import Data.IORef
 import Control.Eff
 
+%default total
+
 %hide Doc.(>>=)
 %hide Core.(>>=)
 
@@ -36,13 +35,9 @@ hlFor Term  _       = highlightSGR
 hlFor Html  _       = highlightHtml
 
 private
-runPretty : Options -> Eff Pretty a -> a
-runPretty opts act =
-  runPrettyWith Outer opts.flavor (hlFor opts.hlType opts.outFile) 2 act
-
-private
-putErrLn : HasIO io => String -> io ()
-putErrLn = ignore . fPutStrLn stderr
+runPretty : Options -> OutFile -> Eff Pretty a -> a
+runPretty opts file act =
+  runPrettyWith Outer opts.flavor (hlFor opts.hlType file) 2 act
 
 private
 record State where
@@ -92,6 +87,13 @@ prettyError (MultipleMains xs)  =
 prettyError (WriteError file e) = pure $
   hangSingle 2 (text "couldn't write file \{file}:") (pshow e)
 
+private
+dieError : Options -> Error -> IO a
+dieError opts e =
+  die (Opts opts.width) $
+  runPretty ({outFile := Console} opts) Console $
+  prettyError e
+
 private
 data CompileTag = OPTS | STATE
 
@@ -102,7 +104,7 @@ Compile =
    ReaderL STATE State, ReaderL OPTS Options,
    LoadFile, IO]
 
-private
+private covering
 runCompile : Options -> State -> Eff Compile a -> IO (Either Error a)
 runCompile opts state act =
   fromIOErr $ runEff act $ with Union.(::)
@@ -130,38 +132,57 @@ stopHere = failAt STOP
 
 
 private
-FlexDoc : Type
-FlexDoc = {opts : LayoutOpts} -> Doc opts
-
+data ConsoleChannel = COut | CErr
 
 private
-outputStr : Lazy String -> Eff Compile ()
-outputStr str =
-  case !(asksAt OPTS outFile) of
-    NoOut   => pure ()
-    Console => putStr str
-    File f  => do
-      res <- withFile f WriteTruncate pure $ \h => fPutStr h str
-      rethrow $ mapFst (WriteError f) res
+data OpenFile = OConsole ConsoleChannel | OFile String File | ONone
 
 private
-outputDocs : (opts : Options) ->
-             ({opts : LayoutOpts} -> List (Doc opts)) -> Eff Compile ()
-outputDocs opts doc =
-  outputStr $ concat $ map (render (Opts opts.width)) doc
+rethrowFile : String -> Either FileError a -> Eff Compile a
+rethrowFile f = rethrow . mapFst (WriteError f)
 
 private
-outputDocStopIf : Phase ->
-                  ({opts : LayoutOpts} -> Eff Pretty (List (Doc opts))) ->
-                  Eff CompileStop ()
-outputDocStopIf p docs = do
+toOutFile : OpenFile -> OutFile
+toOutFile (OConsole _) = Console
+toOutFile (OFile f _)  = File f
+toOutFile ONone        = NoOut
+
+private
+withFileC : String -> (OpenFile -> Eff Compile a) -> Eff Compile a
+withFileC f act =
+  withFile f WriteTruncate pure (Prelude.map Right . act . OFile f) >>=
+  rethrowFile f
+
+private
+withOutFile : ConsoleChannel -> OutFile ->
+              (OpenFile -> Eff Compile a) -> Eff Compile a
+withOutFile _  (File f) act = withFileC f act
+withOutFile ch Console  act = act $ OConsole ch
+withOutFile _  NoOut    act = act ONone
+
+private
+outputStr : OpenFile -> Lazy String -> Eff Compile ()
+outputStr ONone           _   = pure ()
+outputStr (OConsole COut) str = putStr str
+outputStr (OConsole CErr) str = fPutStr stderr str >>= rethrowFile "<stderr>"
+outputStr (OFile f h)     str = fPutStr h str >>= rethrowFile f
+
+private
+outputDocs : OpenFile ->
+             ({opts : LayoutOpts} -> Eff Pretty (List (Doc opts))) ->
+             Eff Compile ()
+outputDocs file docs = do
   opts <- askAt OPTS
-  when (opts.until == Just p) $ Prelude.do
-    lift $ outputDocs !(askAt OPTS) (runPretty opts docs)
-    stopHere
+  for_ (runPretty opts (toOutFile file) docs) $ \x =>
+    outputStr file $ render (Opts opts.width) x
 
 private
-liftFromParser : Eff FromParserIO a -> Eff CompileStop a
+outputDoc : OpenFile ->
+            ({opts : LayoutOpts} -> Eff Pretty (Doc opts)) -> Eff Compile ()
+outputDoc file doc = outputDocs file $ singleton <$> doc
+
+private
+liftFromParser : Eff FromParserIO a -> Eff Compile a
 liftFromParser act =
   runEff act $ with Union.(::)
     [handleExcept $ \err => throw $ FromParserError err,
@@ -171,14 +192,14 @@ liftFromParser act =
      \g => send g]
 
 private
-liftErase : Q.Definitions -> Eff Erase a -> Eff CompileStop a
+liftErase : Q.Definitions -> Eff Erase a -> Eff Compile a
 liftErase defs act =
   runEff act
     [handleExcept $ \err => throw $ EraseError err,
      handleStateIORef !(asksAt STATE suf)]
 
 private
-liftScheme : Eff Scheme a -> Eff CompileStop (a, List Id)
+liftScheme : Eff Scheme a -> Eff Compile (a, List Id)
 liftScheme act = do
   runEff [|MkPair act (getAt MAIN)|]
     [handleStateIORef !(newIORef empty),
@@ -186,49 +207,110 @@ liftScheme act = do
 
 
 private
-oneMain : Has (Except Error) fs => List Id -> Eff fs Id
-oneMain []    = throw NoMain
-oneMain [x]   = pure x
-oneMain mains = throw $ MultipleMains mains
+Step : Type -> Type -> Type
+Step i o = OpenFile -> i -> Eff Compile o
 
+-- private
+-- processFile : String -> Eff Compile ()
+-- processFile file = withEarlyStop $ do
+--   Just ast <- loadFile noLoc file
+--     | Nothing => pure ()
+--   -- putErrLn "checking \{file}"
+--   when (!(asksAt OPTS until) == Just Parse) $ do
+--     lift $ outputStr $ show ast
+--     stopHere
+--   defList <- liftFromParser $ concat <$> traverse fromPTopLevel ast
+--   outputDocStopIf Check $
+--     traverse (uncurry Q.prettyDef) defList
+--   let defs = SortedMap.fromList defList
+--   erased <- liftErase defs $
+--     traverse (\(x, d) => (x,) <$> eraseDef defs x d) defList
+--   outputDocStopIf Erase $
+--     traverse (uncurry U.prettyDef) erased
+--   (scheme, mains) <- liftScheme $ map catMaybes $
+--     traverse (uncurry defToScheme) erased
+--   outputDocStopIf Scheme $
+--     intersperse empty <$> traverse prettySexp scheme
 
 private
-processFile : String -> Eff Compile ()
-processFile file = withEarlyStop $ do
-  Just ast <- loadFile noLoc file
-    | Nothing => pure ()
-  -- putErrLn "checking \{file}"
-  when (!(asksAt OPTS until) == Just Parse) $ do
-    lift $ outputStr $ show ast
-    stopHere
-  defList <- liftFromParser $ concat <$> traverse fromPTopLevel ast
-  outputDocStopIf Check $
-    traverse (uncurry Q.prettyDef) defList
-  let defs = SortedMap.fromList defList
-  erased <- liftErase defs $
-    traverse (\(x, d) => (x,) <$> eraseDef defs x d) defList
-  outputDocStopIf Erase $
-    traverse (uncurry U.prettyDef) erased
-  (scheme, mains) <- liftScheme $ map catMaybes $
-    traverse (uncurry defToScheme) erased
-  outputDocStopIf Scheme $
-    intersperse empty <$> traverse prettySexp scheme
+step : {default CErr console : ConsoleChannel} ->
+       Phase -> OutFile -> Step i o -> i -> Eff CompileStop o
+step phase file act x = do
   opts <- askAt OPTS
-  main <- oneMain mains
-  lift $ outputDocs opts $ intersperse empty $ runPretty opts $ do
-    res    <- traverse prettySexp scheme
+  res <- lift $ withOutFile console file $ \h => act h x
+  when (opts.until == Just phase) stopHere
+  pure res
+
+
+private covering
+parse : Step String PFile
+parse h file = do
+  Just ast <- loadFile noLoc file
+    | Nothing => pure []
+  outputStr h $ show ast
+  pure ast
+
+private covering
+check : Step PFile (List Q.NDefinition)
+check h decls =
+  map concat $ for decls $ \decl => do
+    defs <- liftFromParser $ fromPTopLevel decl
+    outputDocs h $ traverse (\(x, d) => prettyDef x d) defs
+    pure defs
+
+private covering
+erase : Step (List Q.NDefinition) (List U.NDefinition)
+erase h defList =
+  for defList $ \(x, def) => do
+    def <- liftErase defs $ eraseDef defs x def
+    outputDoc h $ U.prettyDef x def
+    pure (x, def)
+where defs = SortedMap.fromList defList
+
+private covering
+scheme : Step (List U.NDefinition) (List Sexp, Id)
+scheme h defs = do
+  sexps' <- for defs $ \(x, d) => do
+    (msexp, mains) <- liftScheme $ defToScheme x d
+    outputDoc h $ maybe (sayErased x) prettySexp msexp
+    pure (msexp, mains)
+  bitraverse (pure . catMaybes) (oneMain . concat) $ unzip sexps'
+where
+  sayErased : {opts : LayoutOpts} -> Name -> Eff Pretty (Doc opts)
+  sayErased x = pure $ hsep [";;", prettyName x, "erased"]
+
+  oneMain : List Id -> Eff Compile Id
+  oneMain [m] = pure m
+  oneMain []  = throw NoMain
+  oneMain ms  = throw $ MultipleMains ms
+
+private covering
+output : Step (List Sexp, Id) ()
+output h (sexps, main) =
+  lift $ outputDocs h $ do
+    res    <- traverse prettySexp sexps
     runner <- makeRunMain main
     pure $ text Scheme.prelude :: res ++ [runner]
 
-export
+private covering
+processFile : String -> Eff Compile ()
+processFile file = withEarlyStop $ pipeline !(askAt OPTS) file where
+  pipeline : Options -> String -> Eff CompileStop ()
+  pipeline opts =
+    step Parse  opts.dump.parse  Main.parse  >=>
+    step Check  opts.dump.check  Main.check  >=>
+    step Erase  opts.dump.erase  Main.erase  >=>
+    step Scheme opts.dump.scheme Main.scheme >=>
+    step End    opts.outFile     Main.output {console = COut}
+
+
+export covering
 main : IO ()
 main = do
   (_, opts, files) <- options
   case !(runCompile opts !newState $ traverse_ processFile files) of
     Right () => pure ()
-    Left  e  => die (Opts opts.width) $
-                runPretty ({outFile := Console} opts) $
-                prettyError e
+    Left  e  => dieError opts e
 
 
 -----------------------------------
@@ -244,6 +326,13 @@ text _ =
    #" /_/"#,
    ""]
 
+--   ["",
+--    #" __ _ _  _ _____ __"#,
+--    #"/ _` | || / _ \ \ /"#,
+--    #"\__, |\_,_\___/_\_\"#,
+--    #"   |_|"#,
+--    ""]
+
 private
 qtuwu : PrettyOpts -> List String
 qtuwu opts =

exe/Options.idr

@@ -13,30 +13,37 @@ import Derive.Prelude
 public export
 data OutFile = File String | Console | NoOut
 %name OutFile f
-%runElab derive "OutFile" [Eq, Ord, Show]
+%runElab derive "OutFile" [Eq, Show]
 
 public export
-data Phase = Parse | Check | Erase | Scheme
+data Phase = Parse | Check | Erase | Scheme | End
 %name Phase p
-%runElab derive "Phase" [Eq, Ord, Show]
+%runElab derive "Phase" [Eq, Show]
 
-||| a list of all `Phase`s
+||| a list of all intermediate `Phase`s (excluding `End`)
 public export %inline
 allPhases : List Phase
 allPhases = %runElab do
-  -- as a script so it stays up to date
   cs <- getCons $ fst !(lookupName "Phase")
-  traverse (check . var) cs
+  traverse (check . var) $ fromMaybe [] $ init' cs
 
-||| "guess" is Term for a terminal and NoHL for a file
+||| `Guess` is `Term` for a terminal and `NoHL` for a file
 public export
 data HLType = Guess | NoHL | Term | Html
-%runElab derive "HLType" [Eq, Ord, Show]
+%runElab derive "HLType" [Eq, Show]
+
+public export
+record Dump where
+  constructor MkDump
+  parse, check, erase, scheme : OutFile
+%name Dump dump
+%runElab derive "Dump" [Show]
 
 public export
 record Options where
   constructor MkOpts
   hlType  : HLType
+  dump    : Dump
   outFile : OutFile
   until   : Maybe Phase
   flavor  : Pretty.Flavor
@@ -55,6 +62,7 @@ export
 defaultOpts : IO Options
 defaultOpts = pure $ MkOpts {
   hlType  = Guess,
+  dump    = MkDump NoOut NoOut NoOut NoOut,
   outFile = Console,
   until   = Nothing,
   flavor  = Unicode,
@@ -70,19 +78,31 @@ data OptAction = ShowHelp HelpType | Err String | Ok (Options -> Options)
 %name OptAction act
 
 private
-toOutFile : String -> OptAction
-toOutFile ""  = Ok {outFile := NoOut}
-toOutFile "-" = Ok {outFile := Console}
-toOutFile f   = Ok {outFile := File f}
+toOutFile : String -> OutFile
+toOutFile ""  = NoOut
+toOutFile "-" = Console
+toOutFile f   = File f
 
 private
 toPhase : String -> OptAction
 toPhase str =
   let lstr = toLower str in
   case find (\p => toLower (show p) == lstr) allPhases of
-    Just p  => Ok {until := Just p}
+    Just p  => Ok $ setPhase p
     Nothing => Err "unknown phase name \{show str}\nphases: \{phaseNames}"
-where phaseNames = joinBy ", " $ map (toLower . show) allPhases
+where
+  phaseNames = joinBy ", " $ map (toLower . show) allPhases
+
+  defConsole : OutFile -> OutFile
+  defConsole NoOut = Console
+  defConsole f     = f
+
+  setPhase : Phase -> Options -> Options
+  setPhase Parse  = {until := Just Parse,  dump.parse  $= defConsole}
+  setPhase Check  = {until := Just Check,  dump.check  $= defConsole}
+  setPhase Erase  = {until := Just Erase,  dump.erase  $= defConsole}
+  setPhase Scheme = {until := Just Scheme, dump.scheme $= defConsole}
+  setPhase End    = id
 
 private
 toWidth : String -> OptAction
@@ -96,17 +116,24 @@ toHLType str = case toLower str of
   "none" => Ok {hlType := NoHL}
   "term" => Ok {hlType := Term}
   "html" => Ok {hlType := Html}
-  _      => Err "unknown highlighting type \{str}\ntypes: term, html, none"
+  _      => Err "unknown highlighting type \{show str}\ntypes: term, html, none"
+
+||| like ghc, -i '' clears the search path; -i a:b:c adds a,b,c to the end
+private
+dirListFlag : String -> List String -> List String
+dirListFlag arg val =
+  if null arg then [] else val ++ toList (split (== ':') arg)
 
 private
 commonOptDescrs' : List (OptDescr OptAction)
 commonOptDescrs' = [
-  MkOpt ['i'] ["include"] (ReqArg (\i => Ok {include $= (i ::)}) "<dir>")
-    "add a directory to look for source files",
-  MkOpt ['o'] ["output"] (ReqArg toOutFile "<file>")
+  MkOpt ['i'] ["include"]
+    (ReqArg (\is => Ok {include $= dirListFlag is}) "<dir>:<dir>...")
+    "add directories to look for source files",
+  MkOpt ['o'] ["output"] (ReqArg (\s => Ok {outFile := toOutFile s}) "<file>")
     "output file (\"-\" for stdout, \"\" for no output)",
   MkOpt ['P'] ["phase"] (ReqArg toPhase "<phase>")
-    "phase to stop at (by default go as far as exists)"
+    "stop after the given phase"
 ]
 
 private
@@ -119,7 +146,16 @@ extraOptDescrs = [
   MkOpt [] ["width"] (ReqArg toWidth "<width>")
     "max output width (defaults to terminal width)",
   MkOpt [] ["color", "colour"] (ReqArg toHLType "<type>")
-    "select highlighting type"
+    "select highlighting type",
+
+  MkOpt [] ["dparse"] (ReqArg (\s => Ok {dump.parse := toOutFile s}) "<file>")
+    "dump AST",
+  MkOpt [] ["dcheck"] (ReqArg (\s => Ok {dump.check := toOutFile s}) "<file>")
+    "dump typechecker output",
+  MkOpt [] ["derase"] (ReqArg (\s => Ok {dump.erase := toOutFile s}) "<file>")
+    "dump erasure output",
+  MkOpt [] ["dscheme"] (ReqArg (\s => Ok {dump.scheme := toOutFile s}) "<file>")
+    "dump scheme output (without prelude)"
 ]
 
 private
@@ -152,10 +188,6 @@ applyAction opts (ShowHelp All)    = usage allOptDescrs
 applyAction opts (Err err)         = die err
 applyAction opts (Ok f)            = pure $ f opts
 
-private
-finalise : Options -> Options
-finalise = {include $= reverse}
-
 export
 options : IO (String, Options, List String)
 options = do
@@ -167,4 +199,4 @@ options = do
   unless (null res.unrecognized) $
     die "unrecognised options: \{joinBy ", " res.unrecognized}"
   opts <- foldlM applyAction !defaultOpts res.options
-  pure (app, finalise opts, res.nonOptions)
+  pure (app, opts, res.nonOptions)

lib/Quox/Definition.idr

@@ -89,12 +89,16 @@ isZero g = g.qty == GZero
 
 
 public export
-data DefEnvTag = DEFS
+NDefinition : Type
+NDefinition = (Name, Definition)
 
 public export
 Definitions : Type
 Definitions = SortedMap Name Definition
 
+public export
+data DefEnvTag = DEFS
+
 public export
 DefsReader : Type -> Type
 DefsReader = ReaderL DEFS Definitions

lib/Quox/Equal.idr

@@ -259,15 +259,16 @@ namespace Term
           compare0 defs ctx sg (sub1 snd (Ann s fst s.loc)) (E $ Snd e e.loc) t
         SOne => clashT loc ctx ty s t
 
-  compare0' defs ctx sg ty@(Enum {}) s t = local_ Equal $
+  compare0' defs ctx sg ty@(Enum cases _) s t = local_ Equal $
+    -- η for empty & singleton enums
+    if length (SortedSet.toList cases) <= 1 then pure () else
     case (s, t) of
       -- --------------------
-      --  Γ ⊢ `t = `t ⇐ {ts}
+      --  Γ ⊢ 't = 't ⇐ {ts}
       --
       -- t ∈ ts is in the typechecker, not here, ofc
-      (Tag t1 {}, Tag t2 {}) =>
-        unless (t1 == t2) $ clashT s.loc ctx ty s t
-      (E e, E f) => ignore $ Elim.compare0 defs ctx sg e f
+      (Tag t1 {}, Tag t2 {}) => unless (t1 == t2) $ clashT s.loc ctx ty s t
+      (E e,       E f)       => ignore $ Elim.compare0 defs ctx sg e f
 
       (Tag {}, E _)    => clashT s.loc ctx ty s t
       (E _,    Tag {}) => clashT s.loc ctx ty s t

lib/Quox/FreeVars.idr

@@ -229,27 +229,27 @@ HasFreeVars (Elim d) where
 
 
 private
-expandDShift : {d1 : Nat} -> Shift d1 d2 -> Context' (Dim d2) d1
-expandDShift by = tabulateLT d1 (\i => BV i noLoc // by)
+expandDShift : {d1 : Nat} -> Shift d1 d2 -> Loc -> Context' (Dim d2) d1
+expandDShift by loc = tabulateLT d1 (\i => BV i loc // by)
 
 private
-expandDSubst : {d1 : Nat} -> DSubst d1 d2 -> Context' (Dim d2) d1
-expandDSubst (Shift by) = expandDShift by
-expandDSubst (t ::: th) = expandDSubst th :< t
+expandDSubst : {d1 : Nat} -> DSubst d1 d2 -> Loc -> Context' (Dim d2) d1
+expandDSubst (Shift by) loc = expandDShift by loc
+expandDSubst (t ::: th) loc = expandDSubst th loc :< t
 
 
 private
-fdvSubst' : {d1, d2, n : Nat} -> HasFreeDVars tm =>
+fdvSubst' : {d1, d2, n : Nat} -> (Located2 tm, HasFreeDVars tm) =>
             tm d1 n -> DSubst d1 d2 -> FreeVars d2
 fdvSubst' t th =
-  fold $ zipWith maybeOnly (fdv t).vars (expandDSubst th)
+  fold $ zipWith maybeOnly (fdv t).vars (expandDSubst th t.loc)
 where
   maybeOnly : {d : Nat} -> Bool -> Dim d -> FreeVars d
   maybeOnly True (B i _) = only i
   maybeOnly _    _       = none
 
 private
-fdvSubst : {d, n : Nat} -> HasFreeDVars tm =>
+fdvSubst : {d, n : Nat} -> (Located2 tm, HasFreeDVars tm) =>
            WithSubst (\d => tm d n) Dim d -> FreeVars d
 fdvSubst (Sub t th) = let Val from = getFrom th in fdvSubst' t th
 

lib/Quox/Loc.idr

@@ -118,6 +118,11 @@ export %inline
 or : Loc -> Loc -> Loc
 or (L l1) (L l2) = L $ l1 `or_` l2
 
+export %inline
+extendOr : Loc -> Loc -> Loc
+extendOr l1 l2 = (l1 `extendL` l2) `or` l2
+
+
 
 public export
 interface Located a where (.loc) : a -> Loc
@@ -126,9 +131,22 @@ public export
 0 Located1 : (a -> Type) -> Type
 Located1 f = forall x. Located (f x)
 
+public export
+0 Located2 : (a -> b -> Type) -> Type
+Located2 f = forall x, y. Located (f x y)
+
 public export
 interface Located a => Relocatable a where setLoc : Loc -> a -> a
 
 public export
 0 Relocatable1 : (a -> Type) -> Type
 Relocatable1 f = forall x. Relocatable (f x)
+
+public export
+0 Relocatable2 : (a -> b -> Type) -> Type
+Relocatable2 f = forall x, y. Relocatable (f x y)
+
+
+export
+locs : Located a => Foldable t => t a -> Loc
+locs = foldl (\loc, y => loc `extendOr` y.loc) noLoc

lib/Quox/NatExtra.idr

@@ -82,7 +82,7 @@ namespace Int
 
   export %inline
   fromHex : String -> Maybe Int
-  fromHex = fromHex' 0
+  fromHex str = do guard $ str /= ""; fromHex' 0 str
 
 namespace Nat
   export

lib/Quox/Parser/FromParser.idr

@@ -27,11 +27,6 @@ import Data.IORef
 %default total
 
 
-public export
-NDefinition : Type
-NDefinition = (Name, Definition)
-
-
 public export
 data StateTag = NS | SEEN
 
@@ -307,7 +302,7 @@ mutual
                     Eff FromParserPure (DScopeTermN s d n)
   fromPTermDScope ds ns xs t =
     if all isUnused xs then
-      SN <$> fromPTermWith ds ns t
+      SN {f = \d => Term d n} <$> fromPTermWith ds ns t
     else
       DST (fromSnocVect $ map fromPatVar xs) <$> fromPTermWith (ds ++ xs) ns t
 

lib/Quox/Scoped.idr

@@ -38,3 +38,22 @@ export %inline
 export %inline %hint
 ShowScoped : (forall n. Show (f n)) => Show (Scoped s f n)
 ShowScoped = deriveShow
+
+
+||| scope which ignores all its binders
+public export %inline
+SN : Located1 f => {s : Nat} -> f n -> Scoped s f n
+SN body = S (replicate s $ BN Unused body.loc) $ N body
+
+||| scope which uses its binders
+public export %inline
+SY : BContext s -> f (s + n) -> Scoped s f n
+SY ns = S ns . Y
+
+public export %inline
+name : Scoped 1 f n -> BindName
+name (S [< x] _) = x
+
+public export %inline
+(.name) : Scoped 1 f n -> BindName
+s.name = name s

lib/Quox/Syntax/DimEq.idr

@@ -71,13 +71,13 @@ toMaybe (Just x) = Just x
 
 
 export
-fromGround' : Context' DimConst d -> DimEq' d
-fromGround' [<]        = [<]
-fromGround' (ctx :< e) = fromGround' ctx :< Just (K e noLoc)
+fromGround' : BContext d -> Context' DimConst d -> DimEq' d
+fromGround' [<]       [<]        = [<]
+fromGround' (xs :< x) (ctx :< e) = fromGround' xs ctx :< Just (K e x.loc)
 
 export
-fromGround : Context' DimConst d -> DimEq d
-fromGround = C . fromGround'
+fromGround : BContext d -> Context' DimConst d -> DimEq d
+fromGround = C .: fromGround'
 
 
 public export %inline

lib/Quox/Syntax/Subst.idr

@@ -96,18 +96,18 @@ map f (t ::: th) = f t ::: map f th
 
 
 public export %inline
-push : CanSubstSelf f => Subst f from to -> Subst f (S from) (S to)
-push th = fromVar VZ ::: (th . shift 1)
+push : CanSubstSelf f => Loc -> Subst f from to -> Subst f (S from) (S to)
+push loc th = fromVarLoc VZ loc ::: (th . shift 1)
 
 -- [fixme] a better way to do this?
 public export
-pushN : CanSubstSelf f => (s : Nat) ->
+pushN : CanSubstSelf f => (s : Nat) -> Loc ->
         Subst f from to -> Subst f (s + from) (s + to)
-pushN 0     th = th
-pushN (S s) th =
+pushN 0     _   th = th
+pushN (S s) loc th =
   rewrite plusSuccRightSucc s from in
   rewrite plusSuccRightSucc s to in
-  pushN s $ fromVar VZ ::: (th . shift 1)
+  pushN s loc $ fromVarLoc VZ loc ::: (th . shift 1)
 
 public export
 drop1 : Subst f (S from) to -> Subst f from to

lib/Quox/Syntax/Term/Base.idr

@@ -236,117 +236,6 @@ mutual
   ShowElim : Show (Elim d n)
   ShowElim = assert_total {a = Show (Elim d n)} deriveShow
 
-||| scope which ignores all its binders
-public export %inline
-SN : {s : Nat} -> f n -> Scoped s f n
-SN = S (replicate s $ BN Unused noLoc) . N
-
-||| scope which uses its binders
-public export %inline
-SY : BContext s -> f (s + n) -> Scoped s f n
-SY ns = S ns . Y
-
-public export %inline
-name : Scoped 1 f n -> BindName
-name (S [< x] _) = x
-
-public export %inline
-(.name) : Scoped 1 f n -> BindName
-s.name = name s
-
-||| more convenient Pi
-public export %inline
-PiY : (qty : Qty) -> (x : BindName) ->
-      (arg : Term d n) -> (res : Term d (S n)) -> (loc : Loc) -> Term d n
-PiY {qty, x, arg, res, loc} = Pi {qty, arg, res = SY [< x] res, loc}
-
-||| more convenient Lam
-public export %inline
-LamY : (x : BindName) -> (body : Term d (S n)) -> (loc : Loc) -> Term d n
-LamY {x, body, loc} = Lam {body = SY [< x] body, loc}
-
-public export %inline
-LamN : (body : Term d n) -> (loc : Loc) -> Term d n
-LamN {body, loc} = Lam {body = SN body, loc}
-
-||| non dependent function type
-public export %inline
-Arr : (qty : Qty) -> (arg, res : Term d n) -> (loc : Loc) -> Term d n
-Arr {qty, arg, res, loc} = Pi {qty, arg, res = SN res, loc}
-
-||| more convenient Sig
-public export %inline
-SigY : (x : BindName) -> (fst : Term d n) ->
-       (snd : Term d (S n)) -> (loc : Loc) -> Term d n
-SigY {x, fst, snd, loc} = Sig {fst, snd = SY [< x] snd, loc}
-
-||| non dependent pair type
-public export %inline
-And : (fst, snd : Term d n) -> (loc : Loc) -> Term d n
-And {fst, snd, loc} = Sig {fst, snd = SN snd, loc}
-
-||| more convenient Eq
-public export %inline
-EqY : (i : BindName) -> (ty : Term (S d) n) ->
-      (l, r : Term d n) -> (loc : Loc) -> Term d n
-EqY {i, ty, l, r, loc} = Eq {ty = SY [< i] ty, l, r, loc}
-
-||| more convenient DLam
-public export %inline
-DLamY : (i : BindName) -> (body : Term (S d) n) -> (loc : Loc) -> Term d n
-DLamY {i, body, loc} = DLam {body = SY [< i] body, loc}
-
-public export %inline
-DLamN : (body : Term d n) -> (loc : Loc) -> Term d n
-DLamN {body, loc} = DLam {body = SN body, loc}
-
-||| non dependent equality type
-public export %inline
-Eq0 : (ty, l, r : Term d n) -> (loc : Loc) -> Term d n
-Eq0 {ty, l, r, loc} = Eq {ty = SN ty, l, r, loc}
-
-||| same as `F` but as a term
-public export %inline
-FT : Name -> Universe -> Loc -> Term d n
-FT x u loc = E $ F x u loc
-
-||| same as `B` but as a term
-public export %inline
-BT : Var n -> (loc : Loc) -> Term d n
-BT i loc = E $ B i loc
-
-||| abbreviation for a bound variable like `BV 4` instead of
-||| `B (VS (VS (VS (VS VZ))))`
-public export %inline
-BV : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Elim d n
-BV i loc = B (V i) loc
-
-||| same as `BV` but as a term
-public export %inline
-BVT : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Term d n
-BVT i loc = E $ BV i loc
-
-public export %inline
-Zero : Loc -> Term d n
-Zero = Nat 0
-
-public export %inline
-enum : List TagVal -> Loc -> Term d n
-enum ts loc = Enum (SortedSet.fromList ts) loc
-
-public export %inline
-typeCase : Elim d n -> Term d n ->
-           List (TypeCaseArm d n) -> Term d n -> Loc -> Elim d n
-typeCase ty ret arms def loc = TypeCase ty ret (fromList arms) def loc
-
-public export %inline
-typeCase1Y : Elim d n -> Term d n ->
-             (k : TyConKind) -> BContext (arity k) -> Term d (arity k + n) ->
-             (loc : Loc) ->
-             {default (NAT loc) def : Term d n} ->
-             Elim d n
-typeCase1Y ty ret k ns body loc = typeCase ty ret [(k ** SY ns body)] def loc
-
 
 export
 Located (Elim d n) where
@@ -463,3 +352,97 @@ Relocatable1 f => Relocatable (ScopedBody s f n) where
 export
 Relocatable1 f => Relocatable (Scoped s f n) where
   setLoc loc (S names body) = S (setLoc loc <$> names) (setLoc loc body)
+
+
+||| more convenient Pi
+public export %inline
+PiY : (qty : Qty) -> (x : BindName) ->
+      (arg : Term d n) -> (res : Term d (S n)) -> (loc : Loc) -> Term d n
+PiY {qty, x, arg, res, loc} = Pi {qty, arg, res = SY [< x] res, loc}
+
+||| more convenient Lam
+public export %inline
+LamY : (x : BindName) -> (body : Term d (S n)) -> (loc : Loc) -> Term d n
+LamY {x, body, loc} = Lam {body = SY [< x] body, loc}
+
+public export %inline
+LamN : (body : Term d n) -> (loc : Loc) -> Term d n
+LamN {body, loc} = Lam {body = SN body, loc}
+
+||| non dependent function type
+public export %inline
+Arr : (qty : Qty) -> (arg, res : Term d n) -> (loc : Loc) -> Term d n
+Arr {qty, arg, res, loc} = Pi {qty, arg, res = SN res, loc}
+
+||| more convenient Sig
+public export %inline
+SigY : (x : BindName) -> (fst : Term d n) ->
+       (snd : Term d (S n)) -> (loc : Loc) -> Term d n
+SigY {x, fst, snd, loc} = Sig {fst, snd = SY [< x] snd, loc}
+
+||| non dependent pair type
+public export %inline
+And : (fst, snd : Term d n) -> (loc : Loc) -> Term d n
+And {fst, snd, loc} = Sig {fst, snd = SN snd, loc}
+
+||| more convenient Eq
+public export %inline
+EqY : (i : BindName) -> (ty : Term (S d) n) ->
+      (l, r : Term d n) -> (loc : Loc) -> Term d n
+EqY {i, ty, l, r, loc} = Eq {ty = SY [< i] ty, l, r, loc}
+
+||| more convenient DLam
+public export %inline
+DLamY : (i : BindName) -> (body : Term (S d) n) -> (loc : Loc) -> Term d n
+DLamY {i, body, loc} = DLam {body = SY [< i] body, loc}
+
+public export %inline
+DLamN : (body : Term d n) -> (loc : Loc) -> Term d n
+DLamN {body, loc} = DLam {body = SN body, loc}
+
+||| non dependent equality type
+public export %inline
+Eq0 : (ty, l, r : Term d n) -> (loc : Loc) -> Term d n
+Eq0 {ty, l, r, loc} = Eq {ty = SN ty, l, r, loc}
+
+||| same as `F` but as a term
+public export %inline
+FT : Name -> Universe -> Loc -> Term d n
+FT x u loc = E $ F x u loc
+
+||| same as `B` but as a term
+public export %inline
+BT : Var n -> (loc : Loc) -> Term d n
+BT i loc = E $ B i loc
+
+||| abbreviation for a bound variable like `BV 4` instead of
+||| `B (VS (VS (VS (VS VZ))))`
+public export %inline
+BV : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Elim d n
+BV i loc = B (V i) loc
+
+||| same as `BV` but as a term
+public export %inline
+BVT : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Term d n
+BVT i loc = E $ BV i loc
+
+public export %inline
+Zero : Loc -> Term d n
+Zero = Nat 0
+
+public export %inline
+enum : List TagVal -> Loc -> Term d n
+enum ts loc = Enum (SortedSet.fromList ts) loc
+
+public export %inline
+typeCase : Elim d n -> Term d n ->
+           List (TypeCaseArm d n) -> Term d n -> Loc -> Elim d n
+typeCase ty ret arms def loc = TypeCase ty ret (fromList arms) def loc
+
+public export %inline
+typeCase1Y : Elim d n -> Term d n ->
+             (k : TyConKind) -> BContext (arity k) -> Term d (arity k + n) ->
+             (loc : Loc) ->
+             {default (NAT loc) def : Term d n} ->
+             Elim d n
+typeCase1Y ty ret k ns body loc = typeCase ty ret [(k ** SY ns body)] def loc

lib/Quox/Syntax/Term/Pretty.idr

@@ -608,7 +608,7 @@ prettyElim dnames tnames (Coe ty p q val _) =
 
 prettyElim dnames tnames e@(Comp ty p q val r zero one _) =
   parensIfM App =<< do
-    ty   <- prettyTypeLine dnames tnames $ assert_smaller e $ SN ty
+    ty   <- assert_total $ prettyTypeLine dnames tnames $ SN ty
     pq   <- sep <$> sequence [prettyDArg dnames p, prettyDArg dnames q]
     val  <- prettyTArg dnames tnames val
     r    <- prettyDArg dnames r

lib/Quox/Syntax/Term/Subst.idr

@@ -56,12 +56,12 @@ namespace DSubst.DScopeTermN
   (//) : {s : Nat} ->
          DScopeTermN s d1 n -> Lazy (DSubst d1 d2) ->
          DScopeTermN s d2 n
-  S ns (Y body) // th = S ns $ Y $ body // pushN s th
+  S ns (Y body) // th = S ns $ Y $ body // pushN s (locs $ toList' ns) th
   S ns (N body) // th = S ns $ N $ body // th
 
 
 export %inline FromVar (Elim d) where fromVarLoc = B
-export %inline FromVar (Term d) where fromVarLoc = E .: fromVar
+export %inline FromVar (Term d) where fromVarLoc = E .: fromVarLoc
 
 
 ||| does the minimal reasonable work:
@@ -104,7 +104,7 @@ namespace ScopeTermN
   (//) : {s : Nat} ->
          ScopeTermN s d n1 -> Lazy (TSubst d n1 n2) ->
          ScopeTermN s d n2
-  S ns (Y body) // th = S ns $ Y $ body // pushN s th
+  S ns (Y body) // th = S ns $ Y $ body // pushN s (locs $ toList' ns) th
   S ns (N body) // th = S ns $ N $ body // th
 
 namespace DScopeTermN
@@ -134,6 +134,15 @@ public export %inline
 dweakT : (by : Nat) -> Term d n -> Term (by + d) n
 dweakT by t = t // shift by
 
+public export %inline
+dweakS : (by : Nat) -> ScopeTermN s d n -> ScopeTermN s (by + d) n
+dweakS by t = t // shift by
+
+public export %inline
+dweakDS : {s : Nat} -> (by : Nat) ->
+          DScopeTermN s d n -> DScopeTermN s (by + d) n
+dweakDS by t = t // shift by
+
 public export %inline
 dweakE : (by : Nat) -> Elim d n -> Elim (by + d) n
 dweakE by t = t // shift by
@@ -143,6 +152,15 @@ public export %inline
 weakT : (by : Nat) -> Term d n -> Term d (by + n)
 weakT by t = t // shift by
 
+public export %inline
+weakS : {s : Nat} -> (by : Nat) -> ScopeTermN s d n -> ScopeTermN s d (by + n)
+weakS by t = t // shift by
+
+public export %inline
+weakDS : {s : Nat} -> (by : Nat) ->
+         DScopeTermN s d n -> DScopeTermN s d (by + n)
+weakDS by t = t // shift by
+
 public export %inline
 weakE : (by : Nat) -> Elim d n -> Elim d (by + n)
 weakE by t = t // shift by
@@ -189,11 +207,11 @@ dsub1 t p = dsubN t [< p]
 
 
 public export %inline
-(.zero) : DScopeTerm d n -> {default noLoc loc : Loc} -> Term d n
+(.zero) : (body : DScopeTerm d n) -> {default body.loc loc : Loc} -> Term d n
 body.zero = dsub1 body $ K Zero loc
 
 public export %inline
-(.one) : DScopeTerm d n -> {default noLoc loc : Loc} -> Term d n
+(.one) : (body : DScopeTerm d n) -> {default body.loc loc : Loc} -> Term d n
 body.one = dsub1 body $ K One loc
 
 

lib/Quox/Typechecker.idr

@@ -304,7 +304,7 @@ mutual
     infres <- inferC ctx SZero e
     -- if Ψ | Γ ⊢ Type ℓ <: Type 𝓀
     case u of
-      Just u  => lift $ subtype e.loc ctx infres.type (TYPE u noLoc)
+      Just u  => lift $ subtype e.loc ctx infres.type (TYPE u e.loc)
       Nothing => ignore $ expectTYPE !(askAt DEFS) ctx SZero e.loc infres.type
     -- then Ψ | Γ ⊢₀ E ⇐ Type 𝓀
 

lib/Quox/Typing.idr

@@ -54,7 +54,7 @@ substCasePairRet [< x, y] dty retty =
 public export
 substCaseSuccRet : BContext 2 -> ScopeTerm d n -> Term d (2 + n)
 substCaseSuccRet [< p, ih] retty =
-  let arg = Ann (Succ (BVT 1 p.loc) p.loc) (NAT noLoc) $ p.loc `extendL` ih.loc
+  let arg = Ann (Succ (BVT 1 p.loc) p.loc) (NAT p.loc) $ p.loc `extendL` ih.loc
   in
   retty.term // (arg ::: shift 2)
 

lib/Quox/Typing/Context.idr

@@ -26,6 +26,14 @@ CanShift (LocalVar d) where
   l // by = {type $= (// by), term $= map (// by)} l
 
 namespace LocalVar
+  export %inline
+  letVar : (type, term : Term d n) -> LocalVar d n
+  letVar type term = MkLocal {type, term = Just term}
+
+  export %inline
+  lamVar : (type : Term d n) -> LocalVar d n
+  lamVar type = MkLocal {type, term = Nothing}
+
   subD : DSubst d1 d2 -> LocalVar d1 n -> LocalVar d2 n
   subD th = {type $= (// th), term $= map (// th)}
 
@@ -135,7 +143,7 @@ namespace TyContext
 
   export %inline
   extendTyN : CtxExtension d n1 n2 -> TyContext d n1 -> TyContext d n2
-  extendTyN = extendTyLetN . map (\(q, x, s) => (q, x, MkLocal s Nothing))
+  extendTyN = extendTyLetN . map (\(q, x, s) => (q, x, lamVar s))
 
   export %inline
   extendTyLetN0 : CtxExtensionLet0 d n1 n2 -> TyContext d n1 -> TyContext d n2
@@ -148,7 +156,7 @@ namespace TyContext
   export %inline
   extendTyLet : Qty -> BindName -> Term d n -> Term d n ->
                 TyContext d n -> TyContext d (S n)
-  extendTyLet q x s e = extendTyLetN [< (q, x, MkLocal s (Just e))]
+  extendTyLet q x s e = extendTyLetN [< (q, x, letVar s e)]
 
   export %inline
   extendTy : Qty -> BindName -> Term d n -> TyContext d n -> TyContext d (S n)
@@ -239,7 +247,7 @@ namespace EqContext
 
   export %inline
   extendTyN : CtxExtension 0 n1 n2 -> EqContext n1 -> EqContext n2
-  extendTyN = extendTyLetN . map (\(q, x, s) => (q, x, MkLocal s Nothing))
+  extendTyN = extendTyLetN . map (\(q, x, s) => (q, x, lamVar s))
 
   export %inline
   extendTyLetN0 : CtxExtensionLet0 0 n1 n2 -> EqContext n1 -> EqContext n2
@@ -252,7 +260,7 @@ namespace EqContext
   export %inline
   extendTyLet : Qty -> BindName -> Term 0 n -> Term 0 n ->
                 EqContext n -> EqContext (S n)
-  extendTyLet q x s e = extendTyLetN [< (q, x, MkLocal s (Just e))]
+  extendTyLet q x s e = extendTyLetN [< (q, x, letVar s e)]
 
   export %inline
   extendTy : Qty -> BindName -> Term 0 n -> EqContext n -> EqContext (S n)
@@ -272,7 +280,7 @@ namespace EqContext
   toTyContext : (e : EqContext n) -> TyContext e.dimLen n
   toTyContext (MkEqContext {dimLen, dassign, dnames, tctx, tnames, qtys}) =
     MkTyContext {
-      dctx = fromGround dassign,
+      dctx = fromGround dnames dassign,
       tctx = map (subD $ shift0 dimLen) tctx,
       dnames, tnames, qtys
     }
@@ -293,6 +301,25 @@ namespace WhnfContext
   empty : WhnfContext 0 0
   empty = MkWhnfContext [<] [<] [<]
 
+  export
+  extendTy' : BindName -> LocalVar d n -> WhnfContext d n -> WhnfContext d (S n)
+  extendTy' x var (MkWhnfContext {termLen, dnames, tnames, tctx}) =
+    MkWhnfContext {
+      dnames,
+      termLen = [|S termLen|],
+      tnames  = tnames :< x,
+      tctx    = tctx   :< var
+    }
+
+  export %inline
+  extendTy : BindName -> Term d n -> WhnfContext d n -> WhnfContext d (S n)
+  extendTy x ty ctx = extendTy' x (lamVar ty) ctx
+
+  export %inline
+  extendTyLet : BindName -> (type, term : Term d n) ->
+                WhnfContext d n -> WhnfContext d (S n)
+  extendTyLet x type term ctx = extendTy' x (letVar {type, term}) ctx
+
   export
   extendDimN : {s : Nat} -> BContext s -> WhnfContext d n ->
                WhnfContext (s + d) n

lib/Quox/Untyped/Scheme.idr

@@ -70,7 +70,7 @@ public export
 data Id = I String Nat
 %runElab derive "Id" [Eq, Ord]
 
-private
+export
 prettyId' : {opts : LayoutOpts} -> Id -> Doc opts
 prettyId' (I str 0) = text $ escId str
 prettyId' (I str k) = text $ escId "\{str}:\{show k}"

lib/Quox/Untyped/Syntax.idr

@@ -93,6 +93,10 @@ public export
 0 Definitions : Type
 Definitions = SortedMap Name Definition
 
+public export
+0 NDefinition : Type
+NDefinition = (Name, Definition)
+
 
 export covering
 prettyTerm : {opts : LayoutOpts} -> BContext n ->
@@ -262,7 +266,7 @@ CanSubstSelf Term where
     B i loc =>
       getLoc th i loc
     Lam x body loc =>
-      Lam x (assert_total $ body // push th) loc
+      Lam x (assert_total $ body // push x.loc th) loc
     App fun arg loc =>
       App (fun // th) (arg // th) loc
     Pair fst snd loc =>
@@ -282,19 +286,18 @@ CanSubstSelf Term where
     Succ nat loc =>
       Succ (nat // th) loc
     CaseNat nat zer suc loc =>
-      CaseNat (nat // th) (zer // th)
-              (assert_total substSuc suc th) loc
+      CaseNat (nat // th) (zer // th) (assert_total substSuc suc th) loc
     Str s loc =>
       Str s loc
     Let u x rhs body loc =>
-      Let u x (rhs // th) (assert_total $ body // push th) loc
+      Let u x (rhs // th) (assert_total $ body // push x.loc th) loc
     Erased loc =>
       Erased loc
   where
     substSuc : forall from, to.
                CaseNatSuc from -> USubst from to -> CaseNatSuc to
-    substSuc (NSRec    x ih t) th = NSRec    x ih $ t // pushN 2 th
-    substSuc (NSNonrec x    t) th = NSNonrec x    $ t // push    th
+    substSuc (NSRec    x ih t) th = NSRec    x ih $ t // pushN 2 x.loc th
+    substSuc (NSNonrec x    t) th = NSNonrec x    $ t // push    x.loc th
 
 public export
 subN : SnocVect s (Term n) -> Term (s + n) -> Term n

lib/Quox/Var.idr

@@ -141,9 +141,6 @@ weakIsSpec p i = toNatInj $ trans (weakCorrect p i) (sym $ weakSpecCorrect p i)
 public export
 interface FromVar f where %inline fromVarLoc : Var n -> Loc -> f n
 
-public export %inline
-fromVar : FromVar f => Var n -> {default noLoc loc : Loc} -> f n
-fromVar x = fromVarLoc x loc
 
 public export FromVar Var where fromVarLoc x _ = x
 

lib/Quox/Whnf/Coercion.idr

@@ -63,11 +63,11 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
     Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
     (tfst, tsnd) <- tycaseSig defs ctx1 ty
     let [< x, y] = body.names
-        a' = CoeT i (weakT 2 tfst) p q (BVT 1 noLoc) x.loc
+        a' = CoeT i (weakT 2 tfst) p q (BVT 1 x.loc) x.loc
         tsnd' = tsnd.term //
-          (CoeT i (weakT 2 $ tfst // (B VZ noLoc ::: shift 2))
-            (weakD 1 p) (B VZ noLoc) (BVT 1 noLoc) y.loc ::: shift 2)
-        b' = CoeT i tsnd' p q (BVT 0 noLoc) y.loc
+          (CoeT i (weakT 2 $ tfst // (B VZ tsnd.loc ::: shift 2))
+            (weakD 1 p) (B VZ i.loc) (BVT 1 tsnd.loc) y.loc ::: shift 2)
+        b' = CoeT i tsnd' p q (BVT 0 y.loc) y.loc
     whnf defs ctx sg $ CasePair qty (Ann val (ty // one p) val.loc) ret
       (ST body.names $ body.term // (a' ::: b' ::: shift 2)) loc
 
@@ -119,7 +119,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
   eqCoe sty@(S [< j] ty) p q val r loc = do
     -- (coe [j ⇒ Eq [i ⇒ A] L R] @p @q eq) @r
     --   ⇝
-    -- comp [j ⇒ A‹r/i›] @p @q (eq ∷ (Eq [i ⇒ A] L R)‹p/j›)
+    -- comp [j ⇒ A‹r/i›] @p @q ((eq ∷ (Eq [i ⇒ A] L R)‹p/j›) @r)
     --   @r { 0 j ⇒ L; 1 j ⇒ R }
     let ctx1 = extendDim j ctx
     Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
@@ -141,11 +141,16 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
     let ctx1 = extendDim i ctx
     Element ty tynf <- whnf defs ctx1 SZero $ getTerm ty
     ta <- tycaseBOX defs ctx1 ty
-    let a' = CoeT i (weakT 1 ta) p q (BVT 0 noLoc) body.name.loc
+    let xloc = body.name.loc
+    let a' = CoeT i (weakT 1 ta) p q (BVT 0 xloc) xloc
     whnf defs ctx sg $ CaseBox qty (Ann val (ty // one p) val.loc) ret
       (ST body.names $ body.term // (a' ::: shift 1)) loc
 
 
+-- new params block to call the above functions at different `n`
+parameters {auto _ : CanWhnf Term Interface.isRedexT}
+           {auto _ : CanWhnf Elim Interface.isRedexE}
+           (defs : Definitions) (ctx : WhnfContext d n) (sg : SQty)
   ||| pushes a coercion inside a whnf-ed term
   export covering
   pushCoe : BindName ->
@@ -162,17 +167,22 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
       IOState tyLoc =>
         whnf defs ctx sg $ Ann s (IOState tyLoc) loc
 
-      -- η expand it so that whnf for App can deal with it
+      -- η expand, then simplify the Coe/App in the body
       --
       -- (coe (𝑖 ⇒ π.(x : A) → B) @p @q s)
       --   ⇝
       -- (λ y ⇒ (coe (𝑖 ⇒ π.(x : A) → B) @p @q s) y) ∷ (π.(x : A) → B)‹q/𝑖›
-      Pi {} =>
-        let inner = Coe (SY [< i] ty) p q s loc in
+      --   ⇝     ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
+      -- (λ y ⇒ ⋯) ∷ (π.(x : A) → B)‹q/𝑖›   -- see `piCoe`
+      --
+      -- do the piCoe step here because otherwise equality checking keeps
+      -- doing the η forever
+      Pi {arg, res = S [< x] _, _} => do
+        let ctx' = extendTy x (arg // one p) ctx
+        body <- piCoe defs ctx' sg
+          (weakDS 1 $ SY [< i] ty) p q (weakT 1 s) (BVT 0 loc) loc
         whnf defs ctx sg $
-          Ann (LamY !(mnb "y" loc)
-                  (E $ App (weakE 1 inner) (BVT 0 loc) loc) loc)
-              (ty // one q) loc
+          Ann (LamY x (E body.fst) loc) (ty // one q) loc
 
       -- no η!!!
       -- push into a pair constructor, otherwise still stuck
@@ -198,17 +208,23 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
       Enum cases tyLoc =>
         whnf defs ctx sg $ Ann s (Enum cases tyLoc) loc
 
-      -- η expand, same as for Π
+      -- η expand/simplify, same as for Π
       --
       -- (coe (𝑖 ⇒ Eq (𝑗 ⇒ A) l r) @p @q s)
       --   ⇝
       -- (δ 𝑘 ⇒ (coe (𝑖 ⇒ Eq (𝑗 ⇒ A) l r) @p @q s) @𝑘) ∷ (Eq (𝑗 ⇒ A) l r)‹q/𝑖›
-      Eq {} =>
-        let inner = Coe (SY [< i] ty) p q s loc in
+      --   ⇝     ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
+      -- (δ 𝑘 ⇒ ⋯) ∷ (Eq (𝑗 ⇒ A) l r)‹q/𝑖›   -- see `eqCoe`
+      --
+      -- do the eqCoe step here because otherwise equality checking keeps
+      -- doing the η forever
+      Eq {ty = S [< j] _, _} => do
+        let ctx' = extendDim j ctx
+        body <- eqCoe defs ctx' sg
+          (dweakDS 1 $ S [< i] $ Y ty) (weakD 1 p) (weakD 1 q)
+          (dweakT 1 s) (BV 0 loc) loc
         whnf defs ctx sg $
-          Ann (DLamY !(mnb "k" loc)
-                  (E $ DApp (dweakE 1 inner) (BV 0 loc) loc) loc)
-              (ty // one q) loc
+          Ann (DLamY i (E body.fst) loc) (ty // one q) loc
 
       -- (coe ℕ @_ @_ s) ⇝ (s ∷ ℕ)
       NAT tyLoc =>
@@ -218,22 +234,19 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
       STRING tyLoc =>
         whnf defs ctx sg $ Ann s (STRING tyLoc) loc
 
-      -- η expand.... kinda
+      -- η expand/simplify
       --
-      -- (coe (𝑖 ⇒ [π. A]) @p @q s)
+      -- (coe (𝑖 ⇒ [π.A]) @p @q s)
       --   ⇝
-      -- [case1 s ∷ [π.A]‹p/𝑖› return A‹q/𝑖›
-      --  of {[x] ⇒ coe (𝑖 ⇒ A) @p @q x}] ∷ [π.A]‹q/𝑖›
+      -- [case coe (𝑖 ⇒ [π.A]) @p @q s return A‹q/𝑖› of {[x] ⇒ x}]
+      --   ⇝
+      -- [case1 s ∷ [π.A]‹p/𝑖› ⋯] ∷ [π.A]‹q/𝑖›   -- see `boxCoe`
       --
-      -- a literal η expansion of `e ⇝ [case e of {[x] ⇒ x}]` causes a loop in
-      -- the equality checker because whnf of `case e ⋯` requires whnf of `e`
+      -- do the eqCoe step here because otherwise equality checking keeps
+      -- doing the η forever
       BOX qty inner tyLoc => do
-        let inner = CaseBox {
-              qty  = One,
-              box  = Ann s (ty // one p) s.loc,
-              ret  = SN $ inner // one q,
-              body = SY [< !(mnb "x" loc)] $ E $
-                     Coe (ST [< i] $ weakT 1 inner) p q (BVT 0 s.loc) s.loc,
-              loc
-            }
-        whnf defs ctx sg $ Ann (Box (E inner) loc) (ty // one q) loc
+        body <- boxCoe defs ctx sg qty
+          (SY [< i] ty) p q s
+          (SN $ inner // one q)
+          (SY [< !(mnb "inner" loc)] (BVT 0 loc)) loc
+        whnf defs ctx sg $ Ann (Box (E body.fst) loc) (ty // one q) loc

lib/Quox/Whnf/Interface.idr

@@ -83,7 +83,7 @@ isTagHead (Ann (Tag {}) (Enum {}) _) = True
 isTagHead (Coe {})                   = True
 isTagHead _                          = False
 
-||| an expression like `0 ∷ ℕ` or `suc n ∷ ℕ`
+||| an expression like `𝑘 ∷ ℕ` for a natural constant 𝑘, or `suc n ∷ ℕ`
 public export %inline
 isNatHead : Elim {} -> Bool
 isNatHead (Ann (Nat  {}) (NAT {}) _) = True
@@ -160,11 +160,13 @@ isK (K {}) = True
 isK _      = False
 
 
-||| if `ty` is a type constructor, and `val` is a value of that type where a
-||| coercion can be reduced. which is the case if any of:
-||| - `ty` is an atomic type
-||| - `ty` has η
-||| - `val` is a constructor form
+||| true if `ty` is a type constructor, and `val` is a value of that type where
+||| a coercion can be reduced
+|||
+||| 1. `ty` is an atomic type
+||| 2. `ty` has an η law that is usable in this context
+|||    (e.g. η for pairs only exists when σ=0, not when σ=1)
+||| 3. `val` is a constructor form
 public export %inline
 canPushCoe : SQty -> (ty, val : Term {}) -> Bool
 canPushCoe sg (TYPE    {}) _         = True

lib/Quox/Whnf/Main.idr

@@ -255,7 +255,7 @@ CanWhnf Term Interface.isRedexT where
       Left _ => case p of
         Nat p _               => pure $ nred $ Nat (S p) loc
         E (Ann (Nat p _) _ _) => pure $ nred $ Nat (S p) loc
-      Right nc => pure $ Element (Succ p loc) nc
+      Right nc => pure $ nred $ Succ p loc
 
   whnf defs ctx sg (Let _ rhs body _) =
     whnf defs ctx sg $ sub1 body rhs

lib/Quox/Whnf/TypeCase.idr

@@ -120,9 +120,9 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
     -- (type-case π.(x : A) → B ∷ ★ᵢ return Q of { (a → b) ⇒ s; ⋯ }) ⇝
     -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ Q
     Pi {arg, res, loc = piLoc, _} =>
-      let arg' = Ann arg (TYPE u noLoc) arg.loc
+      let arg' = Ann arg (TYPE u arg.loc) arg.loc
           res' = Ann (Lam res res.loc)
-                     (Arr Zero arg (TYPE u noLoc) arg.loc) res.loc
+                     (Arr Zero arg (TYPE u arg.loc) arg.loc) res.loc
       in
       whnf defs ctx SZero $
         Ann (subN (tycaseRhsDef def KPi arms) [< arg', res']) ret loc
@@ -130,9 +130,9 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
     -- (type-case (x : A) × B ∷ ★ᵢ return Q of { (a × b) ⇒ s; ⋯ }) ⇝
     -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ Q
     Sig {fst, snd, loc = sigLoc, _} =>
-      let fst' = Ann fst (TYPE u noLoc) fst.loc
+      let fst' = Ann fst (TYPE u fst.loc) fst.loc
           snd' = Ann (Lam snd snd.loc)
-                     (Arr Zero fst (TYPE u noLoc) fst.loc) snd.loc
+                     (Arr Zero fst (TYPE u fst.loc) fst.loc) snd.loc
       in
       whnf defs ctx SZero $
         Ann (subN (tycaseRhsDef def KSig arms) [< fst', snd']) ret loc
@@ -150,8 +150,8 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
       let a0 = a.zero; a1 = a.one in
       whnf defs ctx SZero $ Ann
         (subN (tycaseRhsDef def KEq arms)
-           [< Ann a0 (TYPE u noLoc) a.loc, Ann a1 (TYPE u noLoc) a.loc,
-              Ann (DLam a a.loc) (Eq0 (TYPE u noLoc) a0 a1 a.loc) a.loc,
+           [< Ann a0 (TYPE u a.loc) a.loc, Ann a1 (TYPE u a.loc) a.loc,
+              Ann (DLam a a.loc) (Eq0 (TYPE u a.loc) a0 a1 a.loc) a.loc,
               Ann l a0 l.loc, Ann r a1 r.loc])
         ret loc
 
@@ -166,5 +166,5 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
     -- (type-case [π.A] ∷ ★ᵢ return Q of { [a] ⇒ s; ⋯ }) ⇝ s[(A ∷ ★ᵢ)/a] ∷ Q
     BOX {ty = a, loc = boxLoc, _} =>
       whnf defs ctx SZero $ Ann
-        (sub1 (tycaseRhsDef def KBOX arms) (Ann a (TYPE u noLoc) a.loc))
+        (sub1 (tycaseRhsDef def KBOX arms) (Ann a (TYPE u a.loc) a.loc))
         ret loc

pack.toml

@@ -1,4 +1,4 @@
-collection = "nightly-231020"
+collection = "nightly-240101"
 
 [custom.all.tap]
 type = "git"

quox.bib

@@ -329,6 +329,13 @@
   doi          = {10.1109/LICS.2000.855774},
 }
 
+@misc{ornaments,
+  author = {Conor {McBride}},
+  title  = {Ornamental Algebras, Algebraic Ornaments},
+  year   = {2011},
+  url    = {https://personal.cis.strath.ac.uk/conor.mcbride/pub/OAAO/LitOrn.pdf},
+}
+
 
 % Misc implementation
 

tests/Tests/DimEq.idr

@@ -97,7 +97,7 @@ tests = "dimension constraints" :- [
     testPrettyD iijj ZeroIsOne "𝑖, 𝑗, 0 = 1",
     testPrettyD [<] new "" {label = "[empty output from empty context]"},
     testPrettyD ii new "𝑖",
-    testPrettyD iijj (fromGround [< Zero, One])
+    testPrettyD iijj (fromGround [< "𝑖", "𝑗"] [< Zero, One])
       "𝑖, 𝑗, 𝑖 = 0, 𝑗 = 1",
     testPrettyD iijj (C [< Just (^K Zero), Nothing])
       "𝑖, 𝑗, 𝑖 = 0",