rhi/quox
rhi
/
quox
1
0
Fork 0
Code Issues 16 Pull Requests 1 Releases Wiki Activity

erasure and also baby's first scheme backend #29

Merged
rhi merged 33 commits from 🧼 into 🐉 2023-11-03 13:06:42 -04:00
Conversation 0 Commits 33 Files Changed 58 +2914 -855
58 changed files with 2914 additions and 855 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
examples/all.quox
View File

@ -6,3 +6,5 @@ load "nat.quox"
load "pair.quox"
load "list.quox"
load "eta.quox"
load "fail.quox"
load "qty.quox"

9
examples/bool.quox
View File

@ -18,8 +18,13 @@ def if2 : 0.(A B : ★) → (b : Bool) → ω.A → ω.B → if¹ ★ b A B =
def0 T : Bool → ★ = λ b ⇒ if¹ ★ b True False;
def boolω : Bool → [ω.Bool] =
λ b ⇒ if [ω.Bool] b ['true] ['false];
def dup! : (b : Bool) → [ω. Sing Bool b] =
λ b ⇒ if-dep (λ b ⇒ [ω. Sing Bool b]) b
[('true, [δ _ ⇒ 'true])]
[('false, [δ _ ⇒ 'false])];
def dup : Bool → [ω. Bool] =
λ b ⇒ appω (Sing Bool b) Bool (sing.val Bool b) (dup! b);
def true-not-false : Not ('true ≡ 'false : Bool) =
λ eq ⇒ coe (𝑖 ⇒ T (eq @𝑖)) 'true;

4
examples/eta.quox
View File

@ -18,8 +18,8 @@ def0 pair : (A : ★) → (B : A → ★) → (P : Σ A B → ★) → (e : Σ A
λ A B P e p ⇒ p
-- not exactly η, but kinda related
def0 from-false : (A : ★) → (P : (False → A) → ★) → (f : False → A) →
P (λ x ⇒ void A x) → P f =
def0 from-false : (A : ★) → (P : (0.False → A) → ★) → (f : 0.False → A) →
P (void A) → P f =
λ A P f p ⇒ p
}

6
examples/fail.quox
View File

@ -8,3 +8,9 @@ def repeat-enum-case : {a} → {a} =
#[fail "duplicate tags"]
def repeat-enum-type : {a, a} = 'a
#[fail "double-def.X has already been defined"]
namespace double-def {
def0 X : ★ = {a}
def0 X : ★ = {a}
}

26
examples/hello.quox Normal file
View File

@ -0,0 +1,26 @@
def0 Unit : ★ = {tt}
def drop-unit : 0.(A : ★) → Unit → A → A =
λ A u x ⇒ case u return A of {'tt ⇒ x}
-- postulate0 IOState : ★
def0 IO : ★ → ★ = λ A ⇒ IOState → A × IOState
def bind : 0.(A B : ★) → IO A → (A → IO B) → IO B =
λ A B m k s0 ⇒
case m s0 return B × IOState of { (x, s1) ⇒ k x s1 }
def seq : IO Unit → IO Unit → IO Unit =
λ a b ⇒ bind Unit Unit a (λ u ⇒ drop-unit (IO Unit) u b)
#[compile-scheme "(lambda (n) (builtin-io (display n) (newline) 'tt))"]
postulate print-ℕ : ℕ → IO Unit
#[compile-scheme "(lambda (str) (builtin-io (display str) (newline) 'tt))"]
postulate print : String → IO Unit
load "nat.quox"
#[main]
def main = seq (print-ℕ (nat.plus 1000000000 1)) (print "(nice)")

2
examples/list.quox
View File

@ -24,6 +24,7 @@ def elim : 0.(A : ★) → 0.(P : (n : ℕ) → Vec n A → ★) →
}
};
#[compile-scheme "(lambda% (n xs) xs)"]
def up : 0.(A : ★) → (n : ℕ) → Vec n A → Vec¹ n A =
λ A n ⇒
case n return n' ⇒ Vec n' A → Vec¹ n' A of {
@ -63,6 +64,7 @@ def elim : 0.(A : ★) → 0.(P : List A → ★) →
};
-- [fixme] List A <: List¹ A should be automatic, imo
#[compile-scheme "(lambda (xs) xs)"]
def up : 0.(A : ★) → List A → List¹ A =
λ A xs ⇒
case xs return List¹ A of { (len, elems) ⇒

2
examples/misc.quox
View File

@ -6,7 +6,7 @@ def0 Not : ★ → ★ = λ A ⇒ ω.A → False
def void : 0.(A : ★) → 0.False → A =
λ A v ⇒ case0 v return A of { }
def0 All : (A : ★) → (0.A → ★) → ★¹ =
def0 All : (A : ★) → (0.A → ★) → ★ =
λ A P ⇒ (x : A) → P x
def0 cong :

4
examples/nat.quox
View File

@ -4,6 +4,7 @@ load "either.quox";
namespace nat {
#[compile-scheme "(lambda (n) (cons n 'erased))"]
def dup! : (n : ℕ) → [ω. Sing ℕ n] =
λ n ⇒
case n return n' ⇒ [ω. Sing ℕ n'] of {
@ -16,6 +17,7 @@ def dup! : (n : ℕ) → [ω. Sing ℕ n] =
def dup : ℕ → [ω.ℕ] =
λ n ⇒ appω (Sing ℕ n) ℕ (sing.val ℕ n) (dup! n);
#[compile-scheme "(lambda% (m n) (+ m n))"]
def plus : ℕ → ℕ → ℕ =
λ m n ⇒
case m return ℕ of {
@ -23,6 +25,7 @@ def plus : ℕ → ℕ → ℕ =
succ _, 1.p ⇒ succ p
};
#[compile-scheme "(lambda% (m n) (* m n))"]
def timesω : ℕ → ω.ℕ → ℕ =
λ m n ⇒
case m return ℕ of {
@ -67,6 +70,7 @@ def0 not-succ-self : (m : ℕ) → Not (m ≡ succ m : ℕ) =
}
#[compile-scheme "(lambda% (m n) (if (= m n) Yes No))"]
def eq? : DecEq ℕ =
λ m ⇒
caseω m

10
examples/pair.quox
View File

@ -28,7 +28,7 @@ def curry :
λ A B C f x y ⇒ f (x, y);
def curry' :
0.(A B C : ★) → ((A × B) → C) → A → B → C =
0.(A B C : ★) → (A × B → C) → A → B → C =
λ A B C ⇒ curry A (λ _ ⇒ B) (λ _ ⇒ C);
def0 fst-snd :
@ -54,13 +54,19 @@ def map :
0.(A A' : ★) →
0.(B : A → ★) → 0.(B' : A' → ★) →
(f : A → A') → (g : 0.(x : A) → (B x) → B' (f x)) →
(Σ A B) → Σ A' B' =
Σ A B → Σ A' B' =
λ A A' B B' f g p ⇒
case p return Σ A' B' of { (x, y) ⇒ (f x, g x y) };
def map' : 0.(A A' B B' : ★) → (A → A') → (B → B') → (A × B) → A' × B' =
λ A A' B B' f g ⇒ map A A' (λ _ ⇒ B) (λ _ ⇒ B') f (λ _ ⇒ g);
def map-fst : 0.(A A' B : ★) → (A → A') → A × B → A' × B =
λ A A' B f ⇒ map' A A' B B f (λ x ⇒ x);
def map-snd : 0.(A B B' : ★) → (B → B') → A × B → A × B' =
λ A B B' f ⇒ map' A A B B' (λ x ⇒ x) f;
}
def0 Σ = pair.Σ;

73
examples/qty.quox Normal file
View File

@ -0,0 +1,73 @@
def0 Qty : ★ = {"zero", one, any}
def dup : Qty → [ω.Qty] =
λ π ⇒ case π return [ω.Qty] of {
'zero ⇒ ['zero];
'one ⇒ ['one];
'any ⇒ ['any];
}
def drop : 0.(A : ★) → Qty → A → A =
λ A π x ⇒ case π return A of {
'zero ⇒ x;
'one ⇒ x;
'any ⇒ x;
}
def if-zero : 0.(A : ★) → Qty → ω.A → ω.A → A =
λ A π z nz ⇒
case π return A of { 'zero ⇒ z; 'one ⇒ nz; 'any ⇒ nz }
def plus : Qty → Qty → Qty =
λ π ρ ⇒
case π return Qty of {
'zero ⇒ ρ;
'one ⇒ if-zero Qty ρ 'one 'any;
'any ⇒ drop Qty ρ 'any;
}
def times : Qty → Qty → Qty =
λ π ρ ⇒
case π return Qty of {
'zero ⇒ drop Qty ρ 'zero;
'one ⇒ ρ;
'any ⇒ if-zero Qty ρ 'zero 'any;
}
def0 FUN : Qty → (A : ★) → (A → ★) → ★ =
λ π A B ⇒
case π return ★ of {
'zero ⇒ 0.(x : A) → B x;
'one ⇒ 1.(x : A) → B x;
'any ⇒ ω.(x : A) → B x;
}
def0 Fun : Qty → ★ → ★ → ★ =
λ π A B ⇒ FUN π A (λ _ ⇒ B)
def0 Box : Qty → ★ → ★ =
λ π A ⇒
case π return ★ of {
'zero ⇒ [0.A];
'one ⇒ [1.A];
'any ⇒ [ω.A];
}
def0 unbox : (π : Qty) → (A : ★) → Box π A → A =
λ π A ⇒
case π return π' ⇒ Box π' A → A of {
'zero ⇒ λ x ⇒ case x return A of { [x] ⇒ x };
'one ⇒ λ x ⇒ case x return A of { [x] ⇒ x };
'any ⇒ λ x ⇒ case x return A of { [x] ⇒ x };
}
def apply : (π : Qty) → 0.(A : ★) → 0.(B : A → ★) →
FUN π A B → (x : Box π A) → B (unbox π A x) =
λ π A B ⇒
case π
return π' ⇒ FUN π' A B → (x : Box π' A) → B (unbox π' A x)
of {
'zero ⇒ λ f x ⇒ case x return x' ⇒ B (unbox 'zero A x') of { [x] ⇒ f x };
'one ⇒ λ f x ⇒ case x return x' ⇒ B (unbox 'one A x') of { [x] ⇒ f x };
'any ⇒ λ f x ⇒ case x return x' ⇒ B (unbox 'any A x') of { [x] ⇒ f x };
}

232
exe/Main.idr
View File

@ -1,46 +1,230 @@
module Main
import Quox.Syntax
import Quox.Syntax as Q
import Quox.Parser
import Quox.Definition
import Quox.Definition as Q
import Quox.Pretty
import Quox.Untyped.Syntax as U
import Quox.Untyped.Erase
import Quox.Untyped.Scheme
import Options
import System
import Data.IORef
import Data.SortedSet
import Text.Show.PrettyVal
import Text.Show.Pretty
import System
import System.File
import Control.Eff
private
Opts : LayoutOpts
Opts = Opts 80
%hide Doc.(>>=)
%hide Core.(>>=)
private
putDoc : Doc Opts -> IO ()
putDoc = putStr . render Opts
die : HasIO io => (opts : LayoutOpts) -> Doc opts -> io a
die opts err = do
ignore $ fPutStr stderr $ render opts err
exitFailure
private
die : Doc Opts -> IO a
die err = do putDoc err; exitFailure
runPretty : Options -> Eff Pretty a -> a
runPretty opts act =
let doColor = opts.color && opts.outFile == Console
hl = if doColor then highlightSGR else noHighlight
in
runPrettyWith Outer opts.flavor hl 2 act
private
prettySig : Name -> Definition -> Eff Pretty (Doc Opts)
prettySig name def = do
qty <- prettyQty def.qty.qty
name <- prettyFree name
type <- prettyTerm [<] [<] def.type
hangDSingle (hsep [hcat [qty, !dotD, name], !colonD]) type
putErrLn : HasIO io => String -> io ()
putErrLn = ignore . fPutStrLn stderr
private
record State where
constructor MkState
seen : IORef SeenSet
defs : IORef Q.Definitions
ns : IORef Mods
suf : IORef NameSuf
%name Main.State state
private
newState : HasIO io => io State
newState = pure $ MkState {
seen = !(newIORef empty),
defs = !(newIORef empty),
ns = !(newIORef [<]),
suf = !(newIORef 0)
}
private
data Error =
ParseError String Parser.Error
| FromParserError FromParser.Error
| EraseError Erase.Error
| WriteError FilePath FileError
| NoMain
| MultipleMains (List Id)
%hide FromParser.Error
%hide Erase.Error
%hide Lexer.Error
%hide Parser.Error
private
loadError : Loc -> FilePath -> FileError -> Error
loadError loc file err = FromParserError $ LoadError loc file err
private
prettyError : {opts : LayoutOpts} -> Error -> Eff Pretty (Doc opts)
prettyError (ParseError file e) = prettyParseError file e
prettyError (FromParserError e) = FromParser.prettyError True e
prettyError (EraseError e) = Erase.prettyError True e
prettyError NoMain = pure "no #[main] function given"
prettyError (MultipleMains xs) =
pure $ sep ["multiple #[main] functions given:",
separateLoose "," !(traverse prettyId xs)]
prettyError (WriteError file e) = pure $
hangSingle 2 (text "couldn't write file \{file}:") (pshow e)
private
data CompileTag = OPTS | STATE
private
Compile : List (Type -> Type)
Compile =
[Except Error,
ReaderL STATE State, ReaderL OPTS Options,
LoadFile, IO]
private
runCompile : Options -> State -> Eff Compile a -> IO (Either Error a)
runCompile opts state act =
fromIOErr $ runEff act $ with Union.(::)
[handleExcept (\e => ioLeft e),
handleReaderConst state,
handleReaderConst opts,
handleLoadFileIOE loadError ParseError state.seen opts.include,
liftIO]
private
data StopTag = STOP
private
CompileStop : List (Type -> Type)
CompileStop = FailL STOP :: Compile
private
withEarlyStop : Has (FailL STOP) fs => Eff fs () -> Eff (fs - FailL STOP) ()
withEarlyStop = ignore . runFailAt STOP
private
stopHere : Has (FailL STOP) fs => Eff fs ()
stopHere = failAt STOP
private
FlexDoc : Type
FlexDoc = {opts : LayoutOpts} -> Doc opts
private
outputStr : Lazy String -> Eff Compile ()
outputStr str =
case !(asksAt OPTS outFile) of
None => pure ()
Console => putStr str
File f => do
res <- withFile f WriteTruncate pure $ \h => fPutStr h str
rethrow $ mapFst (WriteError f) res
private
outputDocs : (opts : Options) ->
({opts : LayoutOpts} -> List (Doc opts)) -> Eff Compile ()
outputDocs opts doc =
outputStr $ concat $ map (render (Opts opts.width)) doc
private
outputDocStopIf : Phase ->
({opts : LayoutOpts} -> Eff Pretty (List (Doc opts))) ->
Eff CompileStop ()
outputDocStopIf p docs = do
opts <- askAt OPTS
when (opts.until == Just p) $ Prelude.do
lift $ outputDocs !(askAt OPTS) (runPretty opts docs)
stopHere
private
liftFromParser : Eff FromParserIO a -> Eff CompileStop a
liftFromParser act =
runEff act $ with Union.(::)
[handleExcept (\err => throw $ FromParserError err),
handleStateIORef !(asksAt STATE defs),
handleStateIORef !(asksAt STATE ns),
handleStateIORef !(asksAt STATE suf),
\g => send g]
private
liftErase : Q.Definitions -> Eff Erase a -> Eff CompileStop a
liftErase defs act =
runEff act
[\case Err e => throw $ EraseError e,
\case Ask => pure defs,
handleStateIORef !(asksAt STATE suf)]
private
liftScheme : Eff Scheme a -> Eff CompileStop (a, List Id)
liftScheme act = do
runEff [|MkPair act (getAt MAIN)|]
[handleStateIORef !(newIORef empty),
handleStateIORef !(newIORef [])]
private
oneMain : Has (Except Error) fs => List Id -> Eff fs Id
oneMain [] = throw NoMain
oneMain [x] = pure x
oneMain mains = throw $ MultipleMains mains
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 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
opts <- askAt OPTS
main <- oneMain mains
lift $ outputDocs opts $ intersperse empty $ runPretty opts $ do
res <- traverse prettySexp scheme
runner <- makeRunMain main
pure $ text Scheme.prelude :: res ++ [runner]
export
main : IO ()
main = do
seen <- newIORef SortedSet.empty
defs <- newIORef SortedMap.empty
suf <- newIORef 0
for_ (drop 1 !getArgs) $ \file => do
putStrLn "checking \{file}"
Right res <- fromParserIO ["."] seen suf defs $ loadProcessFile noLoc file
| Left err => die $ runPrettyColor $ prettyError True err
for_ res $ \(name, def) => putDoc $ runPrettyColor $ prettySig name def
(_, 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
-----------------------------------
{-

153
exe/Options.idr Normal file
View File

@ -0,0 +1,153 @@
module Options
import Quox.Pretty
import System
import System.Console.GetOpt
import System.File
import System.Term
import Derive.Prelude
%default total
%language ElabReflection
public export
data OutFile = File String | Console | None
%name OutFile f
%runElab derive "OutFile" [Eq, Ord, Show]
public export
data Phase = Parse | Check | Erase | Scheme
%name Phase p
%runElab derive "Phase" [Eq, Ord, Show]
||| a list of all `Phase`s
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
public export
record Options where
constructor MkOpts
color : Bool
outFile : OutFile
until : Maybe Phase
flavor : Pretty.Flavor
width : Nat
include : List String
%name Options opts
%runElab derive "Options" [Show]
export
defaultOpts : IO Options
defaultOpts = pure $ MkOpts {
color = True,
outFile = Console,
until = Nothing,
flavor = Unicode,
width = cast !getTermCols,
include = ["."]
}
private
data HelpType = Common | All
private
data OptAction = ShowHelp HelpType | Err String | Ok (Options -> Options)
%name OptAction act
private
toOutFile : String -> OptAction
toOutFile "" = Ok {outFile := None}
toOutFile "-" = Ok {outFile := Console}
toOutFile f = Ok {outFile := 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}
Nothing => Err "unknown phase name \{show str}\nphases: \{phaseNames}"
where phaseNames = joinBy ", " $ map (toLower . show) allPhases
private
toWidth : String -> OptAction
toWidth s = case parsePositive s of
Just n => Ok {width := n}
Nothing => Err "invalid width: \{show s}"
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>")
"output file (\"-\" for stdout, \"\" for no output)",
MkOpt ['P'] ["phase"] (ReqArg toPhase "<phase>")
"phase to stop at (by default go as far as exists)"
]
private
extraOptDescrs : List (OptDescr OptAction)
extraOptDescrs = [
MkOpt [] ["unicode"] (NoArg $ Ok {flavor := Unicode})
"use unicode syntax when printing (default)",
MkOpt [] ["ascii"] (NoArg $ Ok {flavor := Ascii})
"use ascii syntax when printing",
MkOpt [] ["width"] (ReqArg toWidth "<width>")
"max output width (defaults to terminal width)",
MkOpt [] ["color", "colour"] (NoArg $ Ok {color := True})
"use colour output (default)",
MkOpt [] ["no-color", "no-colour"] (NoArg $ Ok {color := False})
"don't use colour output"
]
private
helpOptDescrs : List (OptDescr OptAction)
helpOptDescrs = [
MkOpt ['h'] ["help"] (NoArg $ ShowHelp Common) "show common options",
MkOpt [] ["help-all"] (NoArg $ ShowHelp All) "show all options"
]
commonOptDescrs = commonOptDescrs' ++ helpOptDescrs
allOptDescrs = commonOptDescrs' ++ extraOptDescrs ++ helpOptDescrs
export
usageHeader : String
usageHeader = joinBy "\n" [
"quox [options] [file.quox ...]",
"rawr"
]
export
usage : List (OptDescr _) -> IO a
usage ds = do
ignore $ fPutStr stderr $ usageInfo usageHeader ds
exitSuccess
private
applyAction : Options -> OptAction -> IO Options
applyAction opts (ShowHelp Common) = usage commonOptDescrs
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
app :: args <- getArgs
| [] => die "couldn't get command line arguments"
let res = getOpt Permute allOptDescrs args
unless (null res.errors) $
die $ trim $ concat res.errors
unless (null res.unrecognized) $
die "unrecognised options: \{joinBy ", " res.unrecognized}"
opts <- foldlM applyAction !defaultOpts res.options
pure (app, finalise opts, res.nonOptions)

2
exe/quox.ipkg
View File

@ -1,7 +1,7 @@
package quox
version = 0
depends = base, contrib, elab-util, sop, quox-lib
depends = base, contrib, elab-util, pretty-show, quox-lib
executable = quox
main = Main

52
lib/Quox/Definition.idr
View File

@ -5,7 +5,9 @@ import public Quox.Syntax
import Quox.Displace
import public Data.SortedMap
import public Quox.Loc
import Quox.Pretty
import Control.Eff
import Data.Singleton
import Decidable.Decidable
@ -24,18 +26,24 @@ namespace DefBody
public export
record Definition where
constructor MkDef
qty : GQty
type0 : Term 0 0
body0 : DefBody
loc_ : Loc
qty : GQty
type0 : Term 0 0
body0 : DefBody
scheme : Maybe String
isMain : Bool
loc_ : Loc
public export %inline
mkPostulate : GQty -> (type0 : Term 0 0) -> Loc -> Definition
mkPostulate qty type0 loc_ = MkDef {qty, type0, body0 = Postulate, loc_}
mkPostulate : GQty -> (type0 : Term 0 0) -> Maybe String -> Bool -> Loc ->
Definition
mkPostulate qty type0 scheme isMain loc_ =
MkDef {qty, type0, body0 = Postulate, scheme, isMain, loc_}
public export %inline
mkDef : GQty -> (type0, term0 : Term 0 0) -> Loc -> Definition
mkDef qty type0 term0 loc_ = MkDef {qty, type0, body0 = Concrete term0, loc_}
mkDef : GQty -> (type0, term0 : Term 0 0) -> Maybe String -> Bool -> Loc ->
Definition
mkDef qty type0 term0 scheme isMain loc_ =
MkDef {qty, type0, body0 = Concrete term0, scheme, isMain, loc_}
export Located Definition where def.loc = def.loc_
export Relocatable Definition where setLoc loc = {loc_ := loc}
@ -62,6 +70,18 @@ parameters {d, n : Nat}
toElim : Definition -> Universe -> Maybe $ Elim d n
toElim def u = pure $ Ann !(def.termAt u) (def.typeAt u) def.loc
public export
(.typeWith) : Definition -> Singleton d -> Singleton n -> Term d n
g.typeWith (Val d) (Val n) = g.type
public export
(.typeWithAt) : Definition -> Singleton d -> Singleton n -> Universe -> Term d n
g.typeWithAt d n u = displace u $ g.typeWith d n
public export
(.termWith) : Definition -> Singleton d -> Singleton n -> Maybe (Term d n)
g.termWith (Val d) (Val n) = g.term
public export %inline
isZero : Definition -> Bool
@ -83,7 +103,21 @@ public export
DefsState : Type -> Type
DefsState = StateL DEFS Definitions
public export %inline
lookupElim : {d, n : Nat} -> Name -> Universe -> Definitions -> Maybe (Elim d n)
lookupElim x u defs = toElim !(lookup x defs) u
public export %inline
lookupElim0 : Name -> Universe -> Definitions -> Maybe (Elim 0 0)
lookupElim0 = lookupElim
export
prettyDef : {opts : LayoutOpts} -> Name -> Definition -> Eff Pretty (Doc opts)
prettyDef name def = withPrec Outer $ do
qty <- prettyQty def.qty.qty
dot <- dotD
name <- prettyFree name
colon <- colonD
type <- prettyTerm [<] [<] def.type
hangDSingle (hsep [hcat [qty, dot, name], colon]) type

7
lib/Quox/Displace.idr
View File

@ -16,6 +16,7 @@ parameters (k : Universe)
namespace Term
doDisplace (TYPE l loc) = TYPE (k + l) loc
doDisplace (IOState loc) = IOState loc
doDisplace (Pi qty arg res loc) =
Pi qty (doDisplace arg) (doDisplaceS res) loc
doDisplace (Lam body loc) = Lam (doDisplaceS body) loc
@ -26,9 +27,11 @@ parameters (k : Universe)
doDisplace (Eq ty l r loc) =
Eq (doDisplaceDS ty) (doDisplace l) (doDisplace r) loc
doDisplace (DLam body loc) = DLam (doDisplaceDS body) loc
doDisplace (Nat loc) = Nat loc
doDisplace (Zero loc) = Zero loc
doDisplace (NAT loc) = NAT loc
doDisplace (Nat n loc) = Nat n loc
doDisplace (Succ p loc) = Succ (doDisplace p) loc
doDisplace (STRING loc) = STRING loc
doDisplace (Str s loc) = Str s loc
doDisplace (BOX qty ty loc) = BOX qty (doDisplace ty) loc
doDisplace (Box val loc) = Box (doDisplace val) loc
doDisplace (E e) = E (doDisplace e)

30
lib/Quox/EffExtra.idr
View File

@ -69,25 +69,23 @@ subsetTail : Length xs => (0 x : a) -> Subset xs (x :: xs)
subsetTail _ = subsetWith S
export
catchMaybeAt : (0 lbl : tag) -> (Has (ExceptL lbl e) fs, Length fs) =>
(e -> Eff fs a) -> Eff fs a -> Eff fs a
catchMaybeAt lbl hnd act =
catchAt lbl hnd $ lift @{subsetTail $ ExceptL lbl e} act
export %inline
catchMaybe : (Has (Except e) fs, Length fs) =>
(e -> Eff fs a) -> Eff fs a -> Eff fs a
catchMaybe = catchMaybeAt ()
export
wrapErrAt : (0 lbl : tag) -> (Has (ExceptL lbl e) fs, Length fs) =>
(e -> e) -> Eff fs a -> Eff fs a
wrapErrAt lbl wrap = catchMaybeAt lbl (\ex => throwAt lbl $ wrap ex)
rethrowAtWith : (0 lbl : tag) -> Has (ExceptL lbl e') fs =>
(e -> e') -> Either e a -> Eff fs a
rethrowAtWith lbl f = rethrowAt lbl . mapFst f
export %inline
wrapErr : (Has (Except e) fs, Length fs) => (e -> e) -> Eff fs a -> Eff fs a
wrapErr = wrapErrAt ()
export
rethrowWith : Has (Except e') fs => (e -> e') -> Either e a -> Eff fs a
rethrowWith = rethrowAtWith ()
export
wrapErr : Length fs => (e -> e') ->
Eff (ExceptL lbl e :: fs) a ->
Eff (ExceptL lbl e' :: fs) a
wrapErr f act =
catchAt lbl (throwAt lbl . f) @{S Z} $
lift @{subsetTail _} act
export

267
lib/Quox/Equal.idr
View File

@ -45,22 +45,26 @@ public export %inline
sameTyCon : (s, t : Term d n) ->
(0 ts : So (isTyConE s)) => (0 tt : So (isTyConE t)) =>
Bool
sameTyCon (TYPE {}) (TYPE {}) = True
sameTyCon (TYPE {}) _ = False
sameTyCon (Pi {}) (Pi {}) = True
sameTyCon (Pi {}) _ = False
sameTyCon (Sig {}) (Sig {}) = True
sameTyCon (Sig {}) _ = False
sameTyCon (Enum {}) (Enum {}) = True
sameTyCon (Enum {}) _ = False
sameTyCon (Eq {}) (Eq {}) = True
sameTyCon (Eq {}) _ = False
sameTyCon (Nat {}) (Nat {}) = True
sameTyCon (Nat {}) _ = False
sameTyCon (BOX {}) (BOX {}) = True
sameTyCon (BOX {}) _ = False
sameTyCon (E {}) (E {}) = True
sameTyCon (E {}) _ = False
sameTyCon (TYPE {}) (TYPE {}) = True
sameTyCon (TYPE {}) _ = False
sameTyCon (IOState {}) (IOState {}) = True
sameTyCon (IOState {}) _ = False
sameTyCon (Pi {}) (Pi {}) = True
sameTyCon (Pi {}) _ = False
sameTyCon (Sig {}) (Sig {}) = True
sameTyCon (Sig {}) _ = False
sameTyCon (Enum {}) (Enum {}) = True
sameTyCon (Enum {}) _ = False
sameTyCon (Eq {}) (Eq {}) = True
sameTyCon (Eq {}) _ = False
sameTyCon (NAT {}) (NAT {}) = True
sameTyCon (NAT {}) _ = False
sameTyCon (STRING {}) (STRING {}) = True
sameTyCon (STRING {}) _ = False
sameTyCon (BOX {}) (BOX {}) = True
sameTyCon (BOX {}) _ = False
sameTyCon (E {}) (E {}) = True
sameTyCon (E {}) _ = False
||| true if a type is known to be empty.
@ -70,12 +74,15 @@ sameTyCon (E {}) _ = False
||| * `[π.A]` is empty if `A` is.
||| * that's it.
public export covering
isEmpty : {n : Nat} -> Definitions -> EqContext n -> SQty -> Term 0 n ->
isEmpty : Definitions -> EqContext n -> SQty -> Term 0 n ->
Eff EqualInner Bool
isEmpty defs ctx sg ty0 = do
Element ty0 nc <- whnf defs ctx sg ty0.loc ty0
let Left y = choose $ isTyConE ty0
| Right n => pure False
case ty0 of
TYPE {} => pure False
IOState {} => pure False
Pi {arg, res, _} => pure False
Sig {fst, snd, _} =>
isEmpty defs ctx sg fst `orM`
@ -83,17 +90,10 @@ isEmpty defs ctx sg ty0 = do
Enum {cases, _} =>
pure $ null cases
Eq {} => pure False
Nat {} => pure False
NAT {} => pure False
STRING {} => pure False
BOX {ty, _} => isEmpty defs ctx sg ty
E (Ann {tm, _}) => isEmpty defs ctx sg tm
E _ => pure False
Lam {} => pure False
Pair {} => pure False
Tag {} => pure False
DLam {} => pure False
Zero {} => pure False
Succ {} => pure False
Box {} => pure False
||| true if a type is known to be a subsingleton purely by its form.
||| a subsingleton is a type with only zero or one possible values.
@ -106,12 +106,15 @@ isEmpty defs ctx sg ty0 = do
||| * an enum type is a subsingleton if it has zero or one tags.
||| * a box type is a subsingleton if its content is
public export covering
isSubSing : {n : Nat} -> Definitions -> EqContext n -> SQty -> Term 0 n ->
isSubSing : Definitions -> EqContext n -> SQty -> Term 0 n ->
Eff EqualInner Bool
isSubSing defs ctx sg ty0 = do
Element ty0 nc <- whnf defs ctx sg ty0.loc ty0
let Left y = choose $ isTyConE ty0
| Right n => pure False
case ty0 of
TYPE {} => pure False
IOState {} => pure False
Pi {arg, res, _} =>
isEmpty defs ctx sg arg `orM`
isSubSing defs (extendTy0 res.name arg ctx) sg res.term
@ -121,17 +124,10 @@ isSubSing defs ctx sg ty0 = do
Enum {cases, _} =>
pure $ length (SortedSet.toList cases) <= 1
Eq {} => pure True
Nat {} => pure False
NAT {} => pure False
STRING {} => pure False
BOX {ty, _} => isSubSing defs ctx sg ty
E (Ann {tm, _}) => isSubSing defs ctx sg tm
E _ => pure False
Lam {} => pure False
Pair {} => pure False
Tag {} => pure False
DLam {} => pure False
Zero {} => pure False
Succ {} => pure False
Box {} => pure False
||| the left argument if the current mode is `Super`; otherwise the right one.
@ -183,21 +179,32 @@ namespace Term
Eff EqualInner ()
compare0' defs ctx sg (TYPE {}) s t = compareType defs ctx s t
compare0' defs ctx sg ty@(IOState {}) s t =
-- Γ ⊢ e = f ⇒ IOState
-- ----------------------
-- Γ ⊢ e = f ⇐ IOState
--
-- (no canonical values, ofc)
case (s, t) of
(E e, E f) => ignore $ Elim.compare0 defs ctx sg e f
(E _, _) => wrongType t.loc ctx ty t
_ => wrongType s.loc ctx ty s
compare0' defs ctx sg ty@(Pi {qty, arg, res, _}) s t = local_ Equal $
-- Γ ⊢ A empty
-- -------------------------------------------
-- Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) : (π·x : A) → B
if !(isEmpty' arg) then pure () else
-- Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) ⇐ (π·x : A) → B
if !(isEmpty defs ctx sg arg) then pure () else
case (s, t) of
-- Γ, x : A ⊢ s = t : B
-- Γ, x : A ⊢ s = t ⇐ B
-- -------------------------------------------
-- Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) : (π·x : A) → B
-- Γ ⊢ (λ x ⇒ s) = (λ x ⇒ t) ⇐ (π·x : A) → B
(Lam b1 {}, Lam b2 {}) =>
compare0 defs ctx' sg res.term b1.term b2.term
-- Γ, x : A ⊢ s = e x : B
-- Γ, x : A ⊢ s = e x ⇐ B
-- -----------------------------------
-- Γ ⊢ (λ x ⇒ s) = e : (π·x : A) → B
-- Γ ⊢ (λ x ⇒ s) = e ⇐ (π·x : A) → B
(E e, Lam b {}) => eta s.loc e b
(Lam b {}, E e) => eta s.loc e b
@ -207,9 +214,6 @@ namespace Term
(E _, t) => wrongType t.loc ctx ty t
(s, _) => wrongType s.loc ctx ty s
where
isEmpty' : Term 0 n -> Eff EqualInner Bool
isEmpty' t = let Val n = ctx.termLen in isEmpty defs ctx sg arg
ctx' : EqContext (S n)
ctx' = extendTy qty res.name arg ctx
@ -222,9 +226,9 @@ namespace Term
compare0' defs ctx sg ty@(Sig {fst, snd, _}) s t = local_ Equal $
case (s, t) of
-- Γ ⊢ s₁ = t₁ : A Γ ⊢ s₂ = t₂ : B{s₁/x}
-- Γ ⊢ s₁ = t₁ ⇐ A Γ ⊢ s₂ = t₂ ⇐ B{s₁/x}
-- --------------------------------------------
-- Γ ⊢ (s₁, t₁) = (s₂,t₂) : (x : A) × B
-- Γ ⊢ (s₁, t₁) = (s₂,t₂) ⇐ (x : A) × B
--
-- [todo] η for π ≥ 0 maybe
(Pair sFst sSnd {}, Pair tFst tSnd {}) => do
@ -251,7 +255,7 @@ namespace Term
compare0' defs ctx sg ty@(Enum {}) s t = local_ Equal $
case (s, t) of
-- --------------------
-- Γ ⊢ `t = `t : {ts}
-- Γ ⊢ `t = `t ⇐ {ts}
--
-- t ∈ ts is in the typechecker, not here, ofc
(Tag t1 {}, Tag t2 {}) =>
@ -269,39 +273,54 @@ namespace Term
-- ✨ uip ✨
--
-- ----------------------------
-- Γ ⊢ e = f : Eq [i ⇒ A] s t
-- Γ ⊢ e = f ⇐ Eq [i ⇒ A] s t
pure ()
compare0' defs ctx sg nat@(Nat {}) s t = local_ Equal $
compare0' defs ctx sg nat@(NAT {}) s t = local_ Equal $
case (s, t) of
-- ---------------
-- Γ ⊢ 0 = 0 : ℕ
(Zero {}, Zero {}) => pure ()
-- Γ ⊢ n = n ⇐ ℕ
(Nat x {}, Nat y {}) => unless (x == y) $ clashT s.loc ctx nat s t
-- Γ ⊢ s = t : ℕ
-- Γ ⊢ s = t ⇐ ℕ
-- -------------------------
-- Γ ⊢ succ s = succ t : ℕ
(Succ s' {}, Succ t' {}) => compare0 defs ctx sg nat s' t'
-- Γ ⊢ succ s = succ t ⇐ ℕ
(Succ s' {}, Succ t' {}) => compare0 defs ctx sg nat s' t'
(Nat (S x) {}, Succ t' {}) => compare0 defs ctx sg nat (Nat x s.loc) t'
(Succ s' {}, Nat (S y) {}) => compare0 defs ctx sg nat s' (Nat y t.loc)
(E e, E f) => ignore $ Elim.compare0 defs ctx sg e f
(Zero {}, Succ {}) => clashT s.loc ctx nat s t
(Zero {}, E _) => clashT s.loc ctx nat s t
(Succ {}, Zero {}) => clashT s.loc ctx nat s t
(Succ {}, E _) => clashT s.loc ctx nat s t
(E _, Zero {}) => clashT s.loc ctx nat s t
(E _, Succ {}) => clashT s.loc ctx nat s t
(Nat 0 {}, Succ {}) => clashT s.loc ctx nat s t
(Nat 0 {}, E _) => clashT s.loc ctx nat s t
(Succ {}, Nat 0 {}) => clashT s.loc ctx nat s t
(Succ {}, E _) => clashT s.loc ctx nat s t
(E _, Nat 0 {}) => clashT s.loc ctx nat s t
(E _, Succ {}) => clashT s.loc ctx nat s t
(Zero {}, t) => wrongType t.loc ctx nat t
(Succ {}, t) => wrongType t.loc ctx nat t
(E _, t) => wrongType t.loc ctx nat t
(s, _) => wrongType s.loc ctx nat s
(Nat 0 {}, t) => wrongType t.loc ctx nat t
(Succ {}, t) => wrongType t.loc ctx nat t
(E _, t) => wrongType t.loc ctx nat t
(s, _) => wrongType s.loc ctx nat s
compare0' defs ctx sg str@(STRING {}) s t = local_ Equal $
case (s, t) of
(Str x _, Str y _) => unless (x == y) $ clashT s.loc ctx str s t
(E e, E f) => ignore $ Elim.compare0 defs ctx sg e f
(Str {}, E _) => clashT s.loc ctx str s t
(E _, Str {}) => clashT s.loc ctx str s t
(Str {}, _) => wrongType t.loc ctx str t
(E _, _) => wrongType t.loc ctx str t
_ => wrongType s.loc ctx str s
compare0' defs ctx sg bty@(BOX q ty {}) s t = local_ Equal $
case (s, t) of
-- Γ ⊢ s = t : A
-- Γ ⊢ s = t ⇐ A
-- -----------------------
-- Γ ⊢ [s] = [t] : [π.A]
-- Γ ⊢ [s] = [t] ⇐ [π.A]
(Box s _, Box t _) => compare0 defs ctx sg ty s t
-- Γ ⊢ s = (case1 e return A of {[x] ⇒ x}) ⇐ A
@ -344,6 +363,10 @@ compareType' defs ctx a@(TYPE k {}) (TYPE l {}) =
-- Γ ⊢ Type 𝓀 <: Type ℓ
expectModeU a.loc !mode k l
compareType' defs ctx a@(IOState {}) (IOState {}) =
-- Γ ⊢ IOState <: IOState
pure ()
compareType' defs ctx (Pi {qty = sQty, arg = sArg, res = sRes, loc})
(Pi {qty = tQty, arg = tArg, res = tRes, _}) = do
-- Γ ⊢ A₁ :> A₂ Γ, x : A₁ ⊢ B₁ <: B₂
@ -382,11 +405,16 @@ compareType' defs ctx s@(Enum tags1 {}) t@(Enum tags2 {}) = do
-- a runtime coercion
unless (tags1 == tags2) $ clashTy s.loc ctx s t
compareType' defs ctx (Nat {}) (Nat {}) =
compareType' defs ctx (NAT {}) (NAT {}) =
-- ------------
-- Γ ⊢ ℕ <: ℕ
pure ()
compareType' defs ctx (STRING {}) (STRING {}) =
-- ------------
-- Γ ⊢ String <: String
pure ()
compareType' defs ctx (BOX pi a loc) (BOX rh b {}) = do
expectEqualQ loc pi rh
compareType defs ctx a b
@ -402,9 +430,39 @@ lookupFree : Has ErrorEff fs =>
Definitions -> EqContext n -> Name -> Universe -> Loc ->
Eff fs (Term 0 n)
lookupFree defs ctx x u loc =
let Val n = ctx.termLen in
maybe (throw $ NotInScope loc x) (\d => pure $ d.typeAt u) $
lookup x defs
case lookup x defs of
Nothing => throw $ NotInScope loc x
Just d => pure $ d.typeWithAt [|Z|] ctx.termLen u
export
typecaseTel : (k : TyConKind) -> BContext (arity k) -> Universe ->
CtxExtension d n (arity k + n)
typecaseTel k xs u = case k of
KTYPE => [<]
KIOState => [<]
-- A : ★ᵤ, B : 0.A → ★ᵤ
KPi =>
let [< a, b] = xs in
[< (Zero, a, TYPE u a.loc),
(Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)]
KSig =>
let [< a, b] = xs in
[< (Zero, a, TYPE u a.loc),
(Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)]
KEnum => [<]
-- A₀ : ★ᵤ, A₁ : ★ᵤ, A : (A₀ ≡ A₁ : ★ᵤ), L : A₀, R : A₀
KEq =>
let [< a0, a1, a, l, r] = xs in
[< (Zero, a0, TYPE u a0.loc),
(Zero, a1, TYPE u a1.loc),
(Zero, a, Eq0 (TYPE u a.loc) (BVT 1 a.loc) (BVT 0 a.loc) a.loc),
(Zero, l, BVT 2 l.loc),
(Zero, r, BVT 2 r.loc)]
KNat => [<]
KString => [<]
-- A : ★ᵤ
KBOX => let [< a] = xs in [< (Zero, a, TYPE u a.loc)]
namespace Elim
@ -422,9 +480,8 @@ namespace Elim
computeElimTypeE : (defs : Definitions) -> EqContext n -> (sg : SQty) ->
(e : Elim 0 n) -> (0 ne : NotRedex defs sg e) =>
Eff EqualElim (Term 0 n)
computeElimTypeE defs ectx sg e =
let Val n = ectx.termLen in
lift $ computeElimType defs (toWhnfContext ectx) sg e
computeElimTypeE defs ectx sg e = lift $
computeElimType defs (toWhnfContext ectx) sg e
private
putError : Has InnerErrEff fs => Error -> Eff fs ()
@ -453,51 +510,12 @@ namespace Elim
(def : Term 0 n) ->
Eff EqualElim ()
compareArm {b1 = Nothing, b2 = Nothing, _} = pure ()
compareArm defs ctx k ret u b1 b2 def =
let def = SN def in
compareArm_ defs ctx k ret u (fromMaybe def b1) (fromMaybe def b2)
where
compareArm_ : Definitions -> EqContext n -> (k : TyConKind) ->
(ret : Term 0 n) -> (u : Universe) ->
(b1, b2 : TypeCaseArmBody k 0 n) ->
Eff EqualElim ()
compareArm_ defs ctx KTYPE ret u b1 b2 =
try $ Term.compare0 defs ctx SZero ret b1.term b2.term
compareArm_ defs ctx KPi ret u b1 b2 = do
let [< a, b] = b1.names
ctx = extendTyN0
[< (a, TYPE u a.loc),
(b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx
try $ Term.compare0 defs ctx SZero (weakT 2 ret) b1.term b2.term
compareArm_ defs ctx KSig ret u b1 b2 = do
let [< a, b] = b1.names
ctx = extendTyN0
[< (a, TYPE u a.loc),
(b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx
try $ Term.compare0 defs ctx SZero (weakT 2 ret) b1.term b2.term
compareArm_ defs ctx KEnum ret u b1 b2 =
try $ Term.compare0 defs ctx SZero ret b1.term b2.term
compareArm_ defs ctx KEq ret u b1 b2 = do
let [< a0, a1, a, l, r] = b1.names
ctx = extendTyN0
[< (a0, TYPE u a0.loc),
(a1, TYPE u a1.loc),
(a, Eq0 (TYPE u a.loc) (BVT 1 a0.loc) (BVT 0 a1.loc) a.loc),
(l, BVT 2 a0.loc),
(r, BVT 2 a1.loc)] ctx
try $ Term.compare0 defs ctx SZero (weakT 5 ret) b1.term b2.term
compareArm_ defs ctx KNat ret u b1 b2 =
try $ Term.compare0 defs ctx SZero ret b1.term b2.term
compareArm_ defs ctx KBOX ret u b1 b2 = do
let ctx = extendTy0 b1.name (TYPE u b1.name.loc) ctx
try $ Term.compare0 defs ctx SZero (weakT 1 ret) b1.term b1.term
compareArm defs ctx k ret u b1 b2 def = do
let def = SN def
left = fromMaybe def b1; right = fromMaybe def b2
names = (fromMaybe def $ b1 <|> b2).names
try $ compare0 defs (extendTyN (typecaseTel k names u) ctx)
SZero (weakT (arity k) ret) left.term right.term
private covering
compare0Inner : Definitions -> EqContext n -> (sg : SQty) ->
@ -610,10 +628,10 @@ namespace Elim
try $ do
compareType defs (extendTy0 eret.name ety ctx) eret.term fret.term
Term.compare0 defs ctx sg
(sub1 eret (Ann (Zero ezer.loc) (Nat ezer.loc) ezer.loc))
(sub1 eret (Ann (Zero ezer.loc) (NAT ezer.loc) ezer.loc))
ezer fzer
Term.compare0 defs
(extendTyN [< (epi, p, Nat p.loc), (epi', ih, eret.term)] ctx) sg
(extendTyN [< (epi, p, NAT p.loc), (epi', ih, eret.term)] ctx) sg
(substCaseSuccRet esuc.names eret) esuc.term fsuc.term
expectEqualQ e.loc epi fpi
expectEqualQ e.loc epi' fpi'
@ -713,7 +731,6 @@ namespace Elim
clashE defs ctx sg e f
compare0Inner defs ctx sg e f = do
let Val n = ctx.termLen
Element e ne <- whnf defs ctx sg e.loc e
Element f nf <- whnf defs ctx sg f.loc f
ty <- compare0Inner' defs ctx sg e f ne nf
@ -726,7 +743,6 @@ namespace Elim
namespace Term
compare0 defs ctx sg ty s t =
wrapErr (WhileComparingT ctx !mode sg ty s t) $ do
let Val n = ctx.termLen
Element ty' _ <- whnf defs ctx SZero ty.loc ty
Element s' _ <- whnf defs ctx sg s.loc s
Element t' _ <- whnf defs ctx sg t.loc t
@ -739,7 +755,6 @@ namespace Elim
maybe (pure ty) throw err
compareType defs ctx s t = do
let Val n = ctx.termLen
Element s' _ <- whnf defs ctx SZero s.loc s
Element t' _ <- whnf defs ctx SZero t.loc t
ts <- ensureTyCon s.loc ctx s'
@ -759,7 +774,6 @@ parameters (loc : Loc) (ctx : TyContext d n)
eachFace : Applicative f => FreeVars d ->
(EqContext n -> DSubst d 0 -> f ()) -> f ()
eachFace fvs act =
let Val d = ctx.dimLen in
for_ (splits loc ctx.dctx fvs) $ \th =>
act (makeEqContext ctx th) th
@ -774,8 +788,7 @@ parameters (loc : Loc) (ctx : TyContext d n)
private
fdvAll : HasFreeDVars t => List (t d n) -> FreeVars d
fdvAll ts =
let Val d = ctx.dimLen; Val n = ctx.termLen in foldMap fdv ts
fdvAll = let Val d = ctx.dimLen in foldMap (fdvWith [|d|] ctx.termLen)
namespace Term
export covering

82
lib/Quox/FreeVars.idr
View File

@ -93,6 +93,14 @@ interface HasFreeDVars (0 tm : TermLike) where
constructor HFDV
fdv : {d, n : Nat} -> tm d n -> FreeVars d
public export %inline
fvWith : HasFreeVars tm => Singleton n -> tm n -> FreeVars n
fvWith (Val n) = fv
public export %inline
fdvWith : HasFreeDVars tm => Singleton d -> Singleton n -> tm d n -> FreeVars d
fdvWith (Val d) (Val n) = fdv
export
Fdv : (0 tm : TermLike) -> {n : Nat} ->
HasFreeDVars tm => HasFreeVars (\d => tm d n)
@ -172,23 +180,26 @@ export HasFreeVars (Elim d)
export
HasFreeVars (Term d) where
fv (TYPE {}) = none
fv (Pi {arg, res, _}) = fv arg <+> fv res
fv (Lam {body, _}) = fv body
fv (Sig {fst, snd, _}) = fv fst <+> fv snd
fv (Pair {fst, snd, _}) = fv fst <+> fv snd
fv (Enum {}) = none
fv (Tag {}) = none
fv (Eq {ty, l, r, _}) = fvD ty <+> fv l <+> fv r
fv (DLam {body, _}) = fvD body
fv (Nat {}) = none
fv (Zero {}) = none
fv (Succ {p, _}) = fv p
fv (BOX {ty, _}) = fv ty
fv (Box {val, _}) = fv val
fv (E e) = fv e
fv (CloT s) = fv s
fv (DCloT s) = fv s.term
fv (TYPE {}) = none
fv (IOState {}) = none
fv (Pi {arg, res, _}) = fv arg <+> fv res
fv (Lam {body, _}) = fv body
fv (Sig {fst, snd, _}) = fv fst <+> fv snd
fv (Pair {fst, snd, _}) = fv fst <+> fv snd
fv (Enum {}) = none
fv (Tag {}) = none
fv (Eq {ty, l, r, _}) = fvD ty <+> fv l <+> fv r
fv (DLam {body, _}) = fvD body
fv (NAT {}) = none
fv (Nat {}) = none
fv (Succ {p, _}) = fv p
fv (STRING {}) = none
fv (Str {}) = none
fv (BOX {ty, _}) = fv ty
fv (Box {val, _}) = fv val
fv (E e) = fv e
fv (CloT s) = fv s
fv (DCloT s) = fv s.term
export
HasFreeVars (Elim d) where
@ -247,23 +258,26 @@ export HasFreeDVars Elim
export
HasFreeDVars Term where
fdv (TYPE {}) = none
fdv (Pi {arg, res, _}) = fdv arg <+> fdvT res
fdv (Lam {body, _}) = fdvT body
fdv (Sig {fst, snd, _}) = fdv fst <+> fdvT snd
fdv (Pair {fst, snd, _}) = fdv fst <+> fdv snd
fdv (Enum {}) = none
fdv (Tag {}) = none
fdv (Eq {ty, l, r, _}) = fdv @{DScope} ty <+> fdv l <+> fdv r
fdv (DLam {body, _}) = fdv @{DScope} body
fdv (Nat {}) = none
fdv (Zero {}) = none
fdv (Succ {p, _}) = fdv p
fdv (BOX {ty, _}) = fdv ty
fdv (Box {val, _}) = fdv val
fdv (E e) = fdv e
fdv (CloT s) = fdv s @{WithSubst}
fdv (DCloT s) = fdvSubst s
fdv (TYPE {}) = none
fdv (IOState {}) = none
fdv (Pi {arg, res, _}) = fdv arg <+> fdvT res
fdv (Lam {body, _}) = fdvT body
fdv (Sig {fst, snd, _}) = fdv fst <+> fdvT snd
fdv (Pair {fst, snd, _}) = fdv fst <+> fdv snd
fdv (Enum {}) = none
fdv (Tag {}) = none
fdv (Eq {ty, l, r, _}) = fdv @{DScope} ty <+> fdv l <+> fdv r
fdv (DLam {body, _}) = fdv @{DScope} body
fdv (NAT {}) = none
fdv (Nat {}) = none
fdv (Succ {p, _}) = fdv p
fdv (STRING {}) = none
fdv (Str {}) = none
fdv (BOX {ty, _}) = fdv ty
fdv (Box {val, _}) = fdv val
fdv (E e) = fdv e
fdv (CloT s) = fdv s @{WithSubst}
fdv (DCloT s) = fdvSubst s
export
HasFreeDVars Elim where

17
lib/Quox/Loc.idr
View File

@ -1,6 +1,7 @@
||| file locations
module Quox.Loc
import Quox.PrettyValExtra
import public Text.Bounded
import Data.SortedMap
import Derive.Prelude
@ -12,12 +13,12 @@ public export
FileName : Type
FileName = String
%runElab derive "Bounds" [Ord]
%runElab derive "Bounds" [Ord, PrettyVal]
public export
data Loc_ = NoLoc | YesLoc FileName Bounds
%name Loc_ loc
%runElab derive "Loc_" [Eq, Ord, Show]
%runElab derive "Loc_" [Eq, Ord, Show, PrettyVal]
||| a wrapper for locations which are always considered equal
@ -39,6 +40,18 @@ public export %inline
makeLoc : FileName -> Bounds -> Loc
makeLoc = L .: YesLoc
public export %inline
loc : FileName -> (sl, sc, el, ec : Int) -> Loc
loc file sl sc el ec = makeLoc file $ MkBounds sl sc el ec
export
PrettyVal Loc where
prettyVal (L NoLoc) = Con "noLoc" []
prettyVal (L (YesLoc file (MkBounds sl sc el ec))) =
Con "loc" [prettyVal file,
prettyVal sl, prettyVal sc,
prettyVal el, prettyVal ec]
export
onlyStart_ : Loc_ -> Loc_

7
lib/Quox/Name.idr
View File

@ -2,6 +2,7 @@ module Quox.Name
import Quox.Loc
import Quox.CharExtra
import Quox.PrettyValExtra
import public Data.SnocList
import Data.List
import Control.Eff
@ -23,7 +24,7 @@ data BaseName
= UN String -- user-given name
| MN String NameSuf -- machine-generated name
| Unused -- "_"
%runElab derive "BaseName" [Eq, Ord]
%runElab derive "BaseName" [Eq, Ord, PrettyVal]
export
baseStr : BaseName -> String
@ -66,7 +67,7 @@ record PName where
constructor MakePName
mods : Mods
base : PBaseName
%runElab derive "PName" [Eq, Ord]
%runElab derive "PName" [Eq, Ord, PrettyVal]
export %inline
fromPName : PName -> Name
@ -97,7 +98,7 @@ record BindName where
constructor BN
val : BaseName
loc_ : Loc
%runElab derive "BindName" [Eq, Ord, Show]
%runElab derive "BindName" [Eq, Ord, Show, PrettyVal]
export Located BindName where n.loc = n.loc_
export Relocatable BindName where setLoc loc (BN x _) = BN x loc

112
lib/Quox/Parser/FromParser.idr
View File

@ -19,6 +19,7 @@ import System.File
import System.Path
import Data.IORef
%hide Typing.Error
%hide Lexer.Error
%hide Parser.Error
@ -40,7 +41,7 @@ FromParserPure = [Except Error, DefsState, StateL NS Mods, NameGen]
public export
FromParserIO : List (Type -> Type)
FromParserIO = LoadFile :: FromParserPure
FromParserIO = FromParserPure ++ [LoadFile]
export
@ -63,13 +64,13 @@ 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),
fromParserIO inc seen suf defs act =
liftIO $ fromIOErr $ runEff act $ with Union.(::)
[handleExcept (\e => ioLeft e),
handleStateIORef defs,
handleStateIORef !(newIORef [<]),
handleStateIORef suf]
handleStateIORef suf,
handleLoadFileIOE LoadError WrapParseError seen inc]
parameters {auto _ : Functor m} (b : Var n -> m a) (f : PName -> m a)
@ -141,6 +142,9 @@ mutual
TYPE k loc =>
pure $ TYPE k loc
IOState loc =>
pure $ IOState loc
Pi pi x s t loc =>
Pi (fromPQty pi)
<$> fromPTermWith ds ns s
@ -184,10 +188,13 @@ mutual
<*> assert_total fromPTermEnumArms loc ds ns arms
<*> pure loc
Nat loc => pure $ Nat loc
Zero loc => pure $ Zero loc
NAT loc => pure $ NAT loc
Nat n loc => pure $ Nat n loc
Succ n loc => [|Succ (fromPTermWith ds ns n) (pure loc)|]
STRING loc => pure $ STRING loc
Str str loc => pure $ Str str loc
Case pi nat (r, ret) (CaseNat zer (s, pi', ih, suc) _) loc =>
map E $ CaseNat (fromPQty pi) (fromPQty pi')
<$> fromPTermElim ds ns nat
@ -322,33 +329,39 @@ liftTC tc = runEff tc $ with Union.(::)
\g => send g]
private
addDef : Has DefsState fs => Name -> GQty -> Term 0 0 -> Term 0 0 -> Loc ->
Eff fs NDefinition
addDef name gqty type term loc = do
let def = mkDef gqty type term loc
addDef : Has DefsState fs => Name -> Definition -> Eff fs NDefinition
addDef name def = do
modifyAt DEFS $ insert name def
pure (name, def)
export covering
fromPDef : PDefinition -> Eff FromParserPure NDefinition
fromPDef (MkPDef qty pname ptype pterm defLoc) = do
fromPDef : PDefinition -> Maybe String -> Bool ->
Eff FromParserPure NDefinition
fromPDef (MkPDef qty pname pbody defLoc) scheme isMain = do
name <- fromPBaseNameNS pname
when !(getsAt DEFS $ isJust . lookup name) $ do
throw $ AlreadyExists defLoc name
gqty <- globalPQty qty.val qty.loc
let sqty = globalToSubj gqty
type <- traverse fromPTerm ptype
term <- fromPTerm pterm
case type of
Just type => do
ignore $ liftTC $ do
checkTypeC empty type Nothing
checkC empty sqty term type
addDef name gqty type term defLoc
Nothing => do
let E elim = term
| _ => throw $ AnnotationNeeded term.loc empty term
res <- liftTC $ inferC empty sqty elim
addDef name gqty res.type term defLoc
case pbody of
PConcrete ptype pterm => do
type <- traverse fromPTerm ptype
term <- fromPTerm pterm
case type of
Just type => do
ignore $ liftTC $ do
checkTypeC empty type Nothing
checkC empty sqty term type
addDef name $ mkDef gqty type term scheme isMain defLoc
Nothing => do
let E elim = term
| _ => throw $ AnnotationNeeded term.loc empty term
res <- liftTC $ inferC empty sqty elim
addDef name $ mkDef gqty res.type term scheme isMain defLoc
PPostulate ptype => do
type <- fromPTerm ptype
addDef name $ mkPostulate gqty type scheme isMain defLoc
public export
@ -356,31 +369,50 @@ data HasFail = NoFail | AnyFail | FailWith String
export
hasFail : List PDeclMod -> HasFail
hasFail [] = NoFail
hasFail (PFail str _ :: _) = maybe AnyFail FailWith str
hasFail [] = NoFail
hasFail (PFail str :: _) = maybe AnyFail FailWith str
hasFail (_ :: rest) = hasFail rest
export
getScheme : List PDeclMod -> Maybe String
getScheme [] = Nothing
getScheme (PCompileScheme str :: _) = Just str
getScheme (_ :: rest) = getScheme rest
export
isMain : List PDeclMod -> Bool
isMain [] = False
isMain (PMain :: _) = True
isMain (_ :: rest) = isMain rest
export covering
fromPDecl : PDecl -> Eff FromParserPure (List NDefinition)
export covering
fromPDeclBody : PDeclBody -> Eff FromParserPure (List NDefinition)
fromPDeclBody (PDef def) = singleton <$> fromPDef def
fromPDeclBody (PNs ns) =
fromPDeclBody : PDeclBody -> Maybe String -> Bool -> Loc ->
Eff FromParserPure (List NDefinition)
fromPDeclBody (PDef def) scheme isMain loc =
singleton <$> fromPDef def scheme isMain
fromPDeclBody (PNs ns) scheme isMain loc = do
when (isJust scheme) $ throw $ SchemeOnNamespace loc ns.name
when isMain $ throw $ MainOnNamespace loc ns.name
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
expectFail : PDeclBody -> Loc -> Eff FromParserPure Error
expectFail body loc =
let res = fromParserPure !(getAt GEN) !(getAt DEFS) $
fromPDeclBody body Nothing False loc in
case res 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 $> []
NoFail => fromPDeclBody decl (getScheme mods) (isMain mods) loc
AnyFail => expectFail decl loc $> []
FailWith str => do
err <- expectFail decl
err <- expectFail decl loc
let msg = runPretty $ prettyError False err {opts = Opts 10_000} -- w/e
if str `isInfixOf` renderInfinite msg
then pure []
@ -392,9 +424,7 @@ mutual
loadProcessFile : Loc -> String -> Eff FromParserIO (List NDefinition)
loadProcessFile loc file =
case !(loadFile loc file) of
Just inp => do
tl <- either (throw . WrapParseError file) pure $ lexParseInput file inp
concat <$> traverse fromPTopLevel tl
Just tl => concat <$> traverse fromPTopLevel tl
Nothing => pure []
||| populates the `defs` field of the state

27
lib/Quox/Parser/FromParser/Error.idr
View File

@ -7,6 +7,8 @@ import System.File
import Quox.Pretty
%default total
%hide Text.PrettyPrint.Prettyprinter.Doc.infixr.(<++>)
@ -30,8 +32,11 @@ data Error =
| DimNameInTerm Loc PBaseName
| DisplacedBoundVar Loc PName
| WrapTypeError TypeError
| AlreadyExists Loc Name
| LoadError Loc FilePath FileError
| ExpectedFail Loc
| SchemeOnNamespace Loc Mods
| MainOnNamespace Loc Mods
| WrongFail String Error Loc
| WrapParseError String ParseError
@ -110,18 +115,32 @@ parameters {opts : LayoutOpts} (showContext : Bool)
prettyError (WrapTypeError err) =
Typing.prettyError showContext $ trimContext 2 err
prettyError (AlreadyExists loc name) = pure $
vsep [!(prettyLoc loc),
sep [!(prettyFree name), "has already been defined"]]
prettyError (LoadError loc file err) = pure $
vsep [!(prettyLoc loc),
"couldn't load file" <++> text file,
text $ show err]
prettyError (ExpectedFail loc) = pure $
sep [!(prettyLoc loc), "expected error"]
vsep [!(prettyLoc loc), "expected error"]
prettyError (SchemeOnNamespace loc ns) = pure $
vsep [!(prettyLoc loc),
hsep ["namespace", !(hl Free $ text $ joinBy "." $ toList ns),
"cannot have #[compile-scheme] attached"]]
prettyError (MainOnNamespace loc ns) = pure $
vsep [!(prettyLoc loc),
hsep ["namespace", !(hl Free $ text $ joinBy "." $ toList ns),
"cannot have #[main] attached"]]
prettyError (WrongFail str err loc) = pure $
sep [!(prettyLoc loc),
"wrong error, expected to match", !(hl Tag $ text "\"\{str}\""),
"but got", !(prettyError err)]
vsep [!(prettyLoc loc),
"wrong error, expected to match", !(hl Tag $ text "\"\{str}\""),
"but got", !(prettyError err)]
prettyError (WrapParseError file err) =
prettyParseError file err

7
lib/Quox/Parser/Lexer.idr
View File

@ -19,7 +19,7 @@ import Derive.Prelude
||| @ Reserved reserved token
||| @ Name name, possibly qualified
||| @ Nat nat literal
||| @ String string literal
||| @ Str string literal
||| @ Tag tag literal
||| @ TYPE "Type" or "★" with ascii nat directly after
||| @ Sup superscript or ^ number (displacement, or universe for ★)
@ -222,11 +222,16 @@ reserved =
Word "ω" `Or` Sym "#",
Sym "★" `Or` Word "Type",
Word "ℕ" `Or` Word "Nat",
Word1 "IOState",
Word1 "String",
Word1 "zero", Word1 "succ",
Word1 "coe", Word1 "comp",
Word1 "def",
Word1 "def0",
Word "defω" `Or` Word "def#",
Word1 "postulate",
Word1 "postulate0",
Word "postulateω" `Or` Word "postulate#",
Sym1 "=",
Word1 "load",
Word1 "namespace"]

26
lib/Quox/Parser/LoadFile.idr
View File

@ -1,5 +1,7 @@
module Quox.Parser.LoadFile
import public Quox.Parser.Syntax
import Quox.Parser.Parser
import Quox.Loc
import Quox.EffExtra
import Data.IORef
@ -20,7 +22,7 @@ data LoadFileL : (lbl : k) -> Type -> Type where
[search lbl]
Seen : FilePath -> LoadFileL lbl Bool
SetSeen : FilePath -> LoadFileL lbl ()
DoLoad : Loc -> FilePath -> LoadFileL lbl String
DoLoad : Loc -> FilePath -> LoadFileL lbl PFile
public export
LoadFile : Type -> Type
@ -47,11 +49,11 @@ setSeen = setSeenAt ()
export
doLoadAt : (0 lbl : k) -> Has (LoadFileL lbl) fs =>
Loc -> FilePath -> Eff fs String
Loc -> FilePath -> Eff fs PFile
doLoadAt lbl loc file = send $ DoLoad {lbl} loc file
export %inline
doLoad : Has LoadFile fs => Loc -> FilePath -> Eff fs String
doLoad : Has LoadFile fs => Loc -> FilePath -> Eff fs PFile
doLoad = doLoadAt ()
@ -63,10 +65,6 @@ public export
IncludePath : Type
IncludePath = List String
public export
ErrorWrapper : Type -> Type
ErrorWrapper e = Loc -> FilePath -> FileError -> e
export covering
readFileFrom : HasIO io => IncludePath -> FilePath ->
io (Either FileError String)
@ -76,23 +74,27 @@ readFileFrom inc f =
Nothing => pure $ Left $ FileNotFound
export covering
handleLoadFileIOE : ErrorWrapper e ->
handleLoadFileIOE : (Loc -> FilePath -> FileError -> e) ->
(FilePath -> Parser.Error -> e) ->
IORef SeenSet -> IncludePath ->
LoadFileL lbl a -> IOErr e a
handleLoadFileIOE inj seen inc = \case
handleLoadFileIOE injf injp seen inc = \case
Seen f => contains f <$> readIORef seen
SetSeen f => modifyIORef seen $ insert f
DoLoad l f => readFileFrom inc f >>= either (ioLeft . inj l f) pure
DoLoad l f =>
case !(readFileFrom inc f) of
Left err => ioLeft $ injf l f err
Right str => either (ioLeft . injp f) pure $ lexParseInput f str
export
loadFileAt : (0 lbl : k) -> Has (LoadFileL lbl) fs =>
Loc -> FilePath -> Eff fs (Maybe String)
Loc -> FilePath -> Eff fs (Maybe PFile)
loadFileAt lbl loc file =
if !(seenAt lbl file)
then pure Nothing
else Just <$> doLoadAt lbl loc file <* setSeenAt lbl file
export
loadFile : Has LoadFile fs => Loc -> FilePath -> Eff fs (Maybe String)
loadFile : Has LoadFile fs => Loc -> FilePath -> Eff fs (Maybe PFile)
loadFile = loadFileAt ()

67
lib/Quox/Parser/Parser.idr
View File

@ -292,12 +292,15 @@ export
termArg : FileName -> Grammar True PTerm
termArg fname = withLoc fname $
[|TYPE universe1|]
<|> IOState <$ res "IOState"
<|> [|Enum enumType|]
<|> [|Tag tag|]
<|> const <$> boxTerm fname
<|> Nat <$ res "ℕ"
<|> Zero <$ res "zero"
<|> [|fromNat nat|]
<|> NAT <$ res "ℕ"
<|> Nat 0 <$ res "zero"
<|> [|Nat nat|]
<|> STRING <$ res "String"
<|> [|Str strLit|]
<|> [|V qname displacement|]
<|> const <$> tupleTerm fname
@ -587,32 +590,60 @@ 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|]
declMod : Grammar True PDeclMod
declMod = pragma $
exactName "fail" *> [|PFail $ optional strLit|]
<|> exactName "compile-scheme" *> [|PCompileScheme strLit|]
<|> exactName "main" $> PMain
<|> do other <- qname
fatalError "unknown declaration flag \{show other}" {c = False}
export
decl : FileName -> Grammar True PDecl
||| `def` alone means `defω`
||| `def` alone means `defω`; same for `postulate`
export
defIntro : FileName -> Grammar True PQty
defIntro fname =
withLoc fname (PQ Zero <$ resC "def0")
<|> withLoc fname (PQ Any <$ resC "defω")
<|> do pos <- bounds $ resC "def"
defIntro' : (bare, zero, omega : String) ->
(0 _ : IsReserved bare) =>
(0 _ : IsReserved zero) =>
(0 _ : IsReserved omega) =>
FileName -> Grammar True PQty
defIntro' bare zero omega fname =
withLoc fname (PQ Zero <$ resC zero)
<|> withLoc fname (PQ Any <$ resC omega)
<|> do pos <- bounds $ resC bare
let any = PQ Any $ makeLoc fname pos.bounds
option any $ qty fname <* needRes "."
export
definition : FileName -> Grammar True PDefinition
definition fname = withLoc fname $ do
defIntro : FileName -> Grammar True PQty
defIntro = defIntro' "def" "def0" "defω"
export
postulateIntro : FileName -> Grammar True PQty
postulateIntro = defIntro' "postulate" "postulate0" "postulateω"
export
postulate : FileName -> Grammar True PDefinition
postulate fname = withLoc fname $ Core.do
qty <- postulateIntro fname
name <- baseName
type <- resC ":" *> mustWork (term fname)
pure $ MkPDef qty name $ PPostulate type
export
concrete : FileName -> Grammar True PDefinition
concrete fname = withLoc fname $ do
qty <- defIntro fname
name <- baseName
type <- optional $ resC ":" *> mustWork (term fname)
term <- needRes "=" *> mustWork (term fname)
optRes ";"
pure $ MkPDef qty name type term
pure $ MkPDef qty name $ PConcrete type term
export
definition : FileName -> Grammar True PDefinition
definition fname = try (postulate fname) <|> concrete fname
export
namespace_ : FileName -> Grammar True PNamespace
@ -629,7 +660,7 @@ export
declBody : FileName -> Grammar True PDeclBody
declBody fname = [|PDef $ definition fname|] <|> [|PNs $ namespace_ fname|]
decl fname = withLoc fname [|MkPDecl (many $ declMod fname) (declBody fname)|]
decl fname = withLoc fname [|MkPDecl (many declMod) (declBody fname)|]
export
load : FileName -> Grammar True PTopLevel
@ -641,7 +672,7 @@ topLevel : FileName -> Grammar True PTopLevel
topLevel fname = load fname <|> [|PD $ decl fname|]
export
input : FileName -> Grammar False (List PTopLevel)
input : FileName -> Grammar False PFile
input fname = [] <$ eof
<|> [|(topLevel fname <* commit) :: assert_total input fname|]
@ -650,5 +681,5 @@ lexParseTerm : FileName -> String -> Either Error PTerm
lexParseTerm = lexParseWith . term
export
lexParseInput : FileName -> String -> Either Error (List PTopLevel)
lexParseInput : FileName -> String -> Either Error PFile
lexParseInput = lexParseWith . input

100
lib/Quox/Parser/Syntax.idr
View File

@ -3,6 +3,7 @@ module Quox.Parser.Syntax
import public Quox.Loc
import public Quox.Syntax
import public Quox.Definition
import Quox.PrettyValExtra
import Derive.Prelude
%hide TT.Name
@ -14,7 +15,7 @@ import Derive.Prelude
public export
data PatVar = Unused Loc | PV PBaseName Loc
%name PatVar v
%runElab derive "PatVar" [Eq, Ord, Show]
%runElab derive "PatVar" [Eq, Ord, Show, PrettyVal]
export
Located PatVar where
@ -38,7 +39,7 @@ record PQty where
val : Qty
loc_ : Loc
%name PQty qty
%runElab derive "PQty" [Eq, Ord, Show]
%runElab derive "PQty" [Eq, Ord, Show, PrettyVal]
export Located PQty where q.loc = q.loc_
@ -46,7 +47,7 @@ namespace PDim
public export
data PDim = K DimConst Loc | V PBaseName Loc
%name PDim p, q
%runElab derive "PDim" [Eq, Ord, Show]
%runElab derive "PDim" [Eq, Ord, Show, PrettyVal]
export
Located PDim where
@ -56,7 +57,7 @@ Located PDim where
public export
data PTagVal = PT TagVal Loc
%name PTagVal tag
%runElab derive "PTagVal" [Eq, Ord, Show]
%runElab derive "PTagVal" [Eq, Ord, Show, PrettyVal]
namespace PTerm
@ -66,6 +67,8 @@ namespace PTerm
data PTerm =
TYPE Universe Loc
| IOState Loc
| Pi PQty PatVar PTerm PTerm Loc
| Lam PatVar PTerm Loc
| App PTerm PTerm Loc
@ -82,8 +85,11 @@ namespace PTerm
| DLam PatVar PTerm Loc
| DApp PTerm PDim Loc
| Nat Loc
| Zero Loc | Succ PTerm Loc
| NAT Loc
| Nat Nat Loc | Succ PTerm Loc
| STRING Loc -- "String" is a reserved word in idris
| Str String Loc
| BOX PQty PTerm Loc
| Box PTerm Loc
@ -104,33 +110,40 @@ namespace PTerm
| CaseBox PatVar PTerm Loc
%name PCaseBody body
%runElab deriveMutual ["PTerm", "PCaseBody"] [Eq, Ord, Show]
public export %inline
Zero : Loc -> PTerm
Zero = Nat 0
%runElab deriveMutual ["PTerm", "PCaseBody"] [Eq, Ord, Show, PrettyVal]
export
Located PTerm where
(TYPE _ loc).loc = loc
(Pi _ _ _ _ loc).loc = loc
(Lam _ _ loc).loc = loc
(App _ _ loc).loc = loc
(Sig _ _ _ loc).loc = loc
(Pair _ _ loc).loc = loc
(Fst _ loc).loc = loc
(Snd _ loc).loc = loc
(Case _ _ _ _ loc).loc = loc
(Enum _ loc).loc = loc
(Tag _ loc).loc = loc
(Eq _ _ _ loc).loc = loc
(DLam _ _ loc).loc = loc
(DApp _ _ loc).loc = loc
(Nat loc).loc = loc
(Zero loc).loc = loc
(Succ _ loc).loc = loc
(BOX _ _ loc).loc = loc
(Box _ loc).loc = loc
(V _ _ loc).loc = loc
(Ann _ _ loc).loc = loc
(Coe _ _ _ _ loc).loc = loc
(Comp _ _ _ _ _ _ _ loc).loc = loc
(TYPE _ loc).loc = loc
(IOState loc).loc = loc
(Pi _ _ _ _ loc).loc = loc
(Lam _ _ loc).loc = loc
(App _ _ loc).loc = loc
(Sig _ _ _ loc).loc = loc
(Pair _ _ loc).loc = loc
(Fst _ loc).loc = loc
(Snd _ loc).loc = loc
(Case _ _ _ _ loc).loc = loc
(Enum _ loc).loc = loc
(Tag _ loc).loc = loc
(Eq _ _ _ loc).loc = loc
(DLam _ _ loc).loc = loc
(DApp _ _ loc).loc = loc
(NAT loc).loc = loc
(Nat _ loc).loc = loc
(Succ _ loc).loc = loc
(STRING loc).loc = loc
(Str _ loc).loc = loc
(BOX _ _ loc).loc = loc
(Box _ loc).loc = loc
(V _ _ loc).loc = loc
(Ann _ _ loc).loc = loc
(Coe _ _ _ _ loc).loc = loc
(Comp _ _ _ _ _ _ _ loc).loc = loc
export
Located PCaseBody where
@ -140,24 +153,31 @@ Located PCaseBody where
(CaseBox _ _ loc).loc = loc
public export
data PBody = PConcrete (Maybe PTerm) PTerm | PPostulate PTerm
%name PBody body
%runElab derive "PBody" [Eq, Ord, Show, PrettyVal]
public export
record PDefinition where
constructor MkPDef
qty : PQty
name : PBaseName
type : Maybe PTerm
term : PTerm
body : PBody
loc_ : Loc
%name PDefinition def
%runElab derive "PDefinition" [Eq, Ord, Show]
%runElab derive "PDefinition" [Eq, Ord, Show, PrettyVal]
export Located PDefinition where def.loc = def.loc_
public export
data PDeclMod =
PFail (Maybe String) Loc
PFail (Maybe String)
| PCompileScheme String
| PMain
%name PDeclMod mod
%runElab derive "PDeclMod" [Eq, Ord, Show]
%runElab derive "PDeclMod" [Eq, Ord, Show, PrettyVal]
mutual
public export
@ -180,7 +200,8 @@ mutual
PDef PDefinition
| PNs PNamespace
%name PDeclBody decl
%runElab deriveMutual ["PNamespace", "PDecl", "PDeclBody"] [Eq, Ord, Show]
%runElab deriveMutual ["PNamespace", "PDecl", "PDeclBody"]
[Eq, Ord, Show, PrettyVal]
export Located PNamespace where ns.loc = ns.loc_
@ -194,7 +215,7 @@ Located PDeclBody where
public export
data PTopLevel = PD PDecl | PLoad String Loc
%name PTopLevel t
%runElab derive "PTopLevel" [Eq, Ord, Show]
%runElab derive "PTopLevel" [Eq, Ord, Show, PrettyVal]
export
Located PTopLevel where
@ -203,6 +224,5 @@ Located PTopLevel where
public export
fromNat : Nat -> Loc -> PTerm
fromNat 0 loc = Zero loc
fromNat (S k) loc = Succ (fromNat k loc) loc
PFile : Type
PFile = List PTopLevel

36
lib/Quox/Pretty.idr
View File

@ -115,11 +115,14 @@ export %inline
hangD : {opts : LayoutOpts} -> Doc opts -> Doc opts -> Eff Pretty (Doc opts)
hangD d1 d2 = pure $ hangSep !(askAt INDENT) d1 d2
export %inline
hangSingle : {opts : LayoutOpts} -> Nat -> Doc opts -> Doc opts -> Doc opts
hangSingle n d1 d2 = ifMultiline (d1 <++> d2) (vappend d1 (indent n d2))
export %inline
hangDSingle : {opts : LayoutOpts} -> Doc opts -> Doc opts ->
Eff Pretty (Doc opts)
hangDSingle d1 d2 =
pure $ ifMultiline (d1 <++> d2) (vappend d1 !(indentD d2))
hangDSingle d1 d2 = pure $ hangSingle !(askAt INDENT) d1 d2
export
@ -188,11 +191,24 @@ parameters {opts : LayoutOpts} {auto _ : Foldable t}
separateTight : Doc opts -> t (Doc opts) -> Doc opts
separateTight d = sep . exceptLast (<+> d) . toList
export
hseparateTight : Doc opts -> t (Doc opts) -> Doc opts
hseparateTight d = hsep . exceptLast (<+> d) . toList
export
vseparateTight : Doc opts -> t (Doc opts) -> Doc opts
vseparateTight d = vsep . exceptLast (<+> d) . toList
export
fillSeparateTight : Doc opts -> t (Doc opts) -> Doc opts
fillSeparateTight d = fillSep . exceptLast (<+> d) . toList
export %inline
pshow : {opts : LayoutOpts} -> Show a => a -> Doc opts
pshow = text . show
export %inline
ifUnicode : (uni, asc : Lazy a) -> Eff Pretty a
ifUnicode uni asc =
@ -232,11 +248,12 @@ prettyDBind = hl DVar . prettyBind'
export %inline
typeD, arrowD, darrowD, timesD, lamD, eqndD, dlamD, annD, natD,
eqD, colonD, commaD, semiD, caseD, typecaseD, returnD,
typeD, ioStateD, arrowD, darrowD, timesD, lamD, eqndD, dlamD, annD, natD,
stringD, eqD, colonD, commaD, semiD, caseD, typecaseD, returnD,
ofD, dotD, zeroD, succD, coeD, compD, undD, cstD, pipeD, fstD, sndD :
{opts : LayoutOpts} -> Eff Pretty (Doc opts)
typeD = hl Syntax . text =<< ifUnicode "★" "Type"
ioStateD = hl Syntax $ text "IOState"
arrowD = hl Delim . text =<< ifUnicode "→" "->"
darrowD = hl Delim . text =<< ifUnicode "⇒" "=>"
timesD = hl Delim . text =<< ifUnicode "×" "**"
@ -245,6 +262,7 @@ eqndD = hl Delim . text =<< ifUnicode "≡" "=="
dlamD = hl Syntax . text =<< ifUnicode "δ" "dfun"
annD = hl Delim . text =<< ifUnicode "∷" "::"
natD = hl Syntax . text =<< ifUnicode "ℕ" "Nat"
stringD = hl Syntax $ text "String"
eqD = hl Syntax $ text "Eq"
colonD = hl Delim $ text ":"
commaD = hl Delim $ text ","
@ -313,3 +331,13 @@ prettyLoc (L (YesLoc file b)) =
export
prettyTag : {opts : _} -> String -> Eff Pretty (Doc opts)
prettyTag tag = hl Tag $ text $ "'" ++ quoteTag tag
export
prettyStrLit : {opts : _} -> String -> Eff Pretty (Doc opts)
prettyStrLit s =
let s = concatMap esc1 $ unpack s in
hl Syntax $ hcat ["\"", text s, "\""]
where
esc1 : Char -> String
esc1 '"' = "\""; esc1 '\\' = "\\"
esc1 c = singleton c

10
lib/Quox/PrettyValExtra.idr Normal file
View File

@ -0,0 +1,10 @@
module Quox.PrettyValExtra
import Derive.Prelude
import public Text.Show.Value
import public Text.Show.PrettyVal
import public Text.Show.PrettyVal.Derive
%language ElabReflection
%runElab derive "SnocList" [PrettyVal]

3
lib/Quox/Syntax/Dim.idr
View File

@ -6,6 +6,7 @@ import Quox.Var
import Quox.Syntax.Subst
import Quox.Pretty
import Quox.Context
import Quox.PrettyValExtra
import Decidable.Equality
import Control.Function
@ -18,7 +19,7 @@ import Derive.Prelude
public export
data DimConst = Zero | One
%name DimConst e
%runElab derive "DimConst" [Eq, Ord, Show]
%runElab derive "DimConst" [Eq, Ord, Show, PrettyVal]
||| `ends l r e` returns `l` if `e` is `Zero`, or `r` if it is `One`.
public export

27
lib/Quox/Syntax/DimEq.idr
View File

@ -237,9 +237,20 @@ setSelf (B i _) (C eqs) with (compareP i i) | (compare i.nat i.nat)
_ | IsGT gt | GT = absurd gt
private %inline
dimEqPrec : BContext d -> Maybe (DimEq' d) -> PPrec
dimEqPrec vars eqs =
if length vars <= 1 && maybe True null eqs then Arg else Outer
private
prettyDVars : {opts : _} -> BContext d -> Eff Pretty (SnocList (Doc opts))
prettyDVars = traverse prettyDBind . toSnocList'
prettyDVars' : {opts : _} -> BContext d -> Eff Pretty (SnocList (Doc opts))
prettyDVars' = traverse prettyDBind . toSnocList'
export
prettyDVars : {opts : _} -> BContext d -> Eff Pretty (Doc opts)
prettyDVars vars =
parensIfM (dimEqPrec vars Nothing) $
fillSeparateTight !commaD $ !(prettyDVars' vars)
private
prettyCst : {opts : _} -> BContext d -> Dim d -> Dim d -> Eff Pretty (Doc opts)
@ -256,16 +267,16 @@ prettyCsts dnames (eqs :< Just q) =
export
prettyDimEq' : {opts : _} -> BContext d -> DimEq' d -> Eff Pretty (Doc opts)
prettyDimEq' dnames eqs = do
vars <- prettyDVars dnames
eqs <- prettyCsts dnames eqs
let prec = if length vars <= 1 && null eqs then Arg else Outer
parensIfM prec $ fillSeparateTight !commaD $ toList vars ++ toList eqs
prettyDimEq' vars eqs = do
vars' <- prettyDVars' vars
eqs' <- prettyCsts vars eqs
parensIfM (dimEqPrec vars (Just eqs)) $
fillSeparateTight !commaD $ vars' ++ eqs'
export
prettyDimEq : {opts : _} -> BContext d -> DimEq d -> Eff Pretty (Doc opts)
prettyDimEq dnames ZeroIsOne = do
vars <- prettyDVars dnames
vars <- prettyDVars' dnames
cst <- prettyCst [<] (K Zero noLoc) (K One noLoc)
pure $ separateTight !commaD $ vars :< cst
prettyDimEq dnames (C eqs) = prettyDimEq' dnames eqs

7
lib/Quox/Syntax/Qty.idr
View File

@ -6,6 +6,7 @@ module Quox.Syntax.Qty
import Quox.Pretty
import Quox.Decidable
import Quox.PrettyValExtra
import Data.DPair
import Derive.Prelude
@ -20,7 +21,7 @@ import Derive.Prelude
||| - ω (or #): don't care. an ω variable *can* also be used 0/1 time
public export
data Qty = Zero | One | Any
%runElab derive "Qty" [Eq, Ord, Show]
%runElab derive "Qty" [Eq, Ord, Show, PrettyVal]
%name Qty.Qty pi, rh
@ -79,7 +80,7 @@ lub p q = if p == q then p else Any
||| for the subject of a typing judgment. see @qtt, §2.3 for more detail
public export
data SQty = SZero | SOne
%runElab derive "SQty" [Eq, Ord, Show]
%runElab derive "SQty" [Eq, Ord, Show, PrettyVal]
%name Qty.SQty sg
||| "σ ⨴ π"
@ -96,7 +97,7 @@ subjMult sg _ = sg
||| at runtime at all or not
public export
data GQty = GZero | GAny
%runElab derive "GQty" [Eq, Ord, Show]
%runElab derive "GQty" [Eq, Ord, Show, PrettyVal]
%name GQty rh
public export

36
lib/Quox/Syntax/Term/Base.idr
View File

@ -61,6 +61,10 @@ mutual
||| type of types
TYPE : (l : Universe) -> (loc : Loc) -> Term d n
||| IO state token. this is a builtin because otherwise #[main] being a
||| builtin makes no sense
IOState : (loc : Loc) -> Term d n
||| function type
Pi : (qty : Qty) -> (arg : Term d n) ->
(res : ScopeTerm d n) -> (loc : Loc) -> Term d n
@ -83,11 +87,14 @@ mutual
DLam : (body : DScopeTerm d n) -> (loc : Loc) -> Term d n
||| natural numbers (temporary until 𝐖 gets added)
Nat : (loc : Loc) -> Term d n
-- [todo] can these be elims?
Zero : (loc : Loc) -> Term d n
NAT : (loc : Loc) -> Term d n
Nat : (val : Nat) -> (loc : Loc) -> Term d n
Succ : (p : Term d n) -> (loc : Loc) -> Term d n
||| strings
STRING : (loc : Loc) -> Term d n
Str : (str : String) -> (loc : Loc) -> Term d n
||| "box" (package a value up with a certain quantity)
BOX : (qty : Qty) -> (ty : Term d n) -> (loc : Loc) -> Term d n
Box : (val : Term d n) -> (loc : Loc) -> Term d n
@ -316,10 +323,9 @@ public export %inline
BVT : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Term d n
BVT i loc = E $ BV i loc
public export
makeNat : Nat -> Loc -> Term d n
makeNat 0 loc = Zero loc
makeNat (S k) loc = Succ (makeNat k loc) loc
public export %inline
Zero : Loc -> Term d n
Zero = Nat 0
public export %inline
enum : List TagVal -> Loc -> Term d n
@ -334,7 +340,7 @@ 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} ->
{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
@ -361,6 +367,7 @@ Located (Elim d n) where
export
Located (Term d n) where
(TYPE _ loc).loc = loc
(IOState loc).loc = loc
(Pi _ _ _ loc).loc = loc
(Lam _ loc).loc = loc
(Sig _ _ loc).loc = loc
@ -369,8 +376,10 @@ Located (Term d n) where
(Tag _ loc).loc = loc
(Eq _ _ _ loc).loc = loc
(DLam _ loc).loc = loc
(Nat loc).loc = loc
(Zero loc).loc = loc
(NAT loc).loc = loc
(Nat _ loc).loc = loc
(STRING loc).loc = loc
(Str _ loc).loc = loc
(Succ _ loc).loc = loc
(BOX _ _ loc).loc = loc
(Box _ loc).loc = loc
@ -421,6 +430,7 @@ Relocatable (Elim d n) where
export
Relocatable (Term d n) where
setLoc loc (TYPE l _) = TYPE l loc
setLoc loc (IOState _) = IOState loc
setLoc loc (Pi qty arg res _) = Pi qty arg res loc
setLoc loc (Lam body _) = Lam body loc
setLoc loc (Sig fst snd _) = Sig fst snd loc
@ -429,9 +439,11 @@ Relocatable (Term d n) where
setLoc loc (Tag tag _) = Tag tag loc
setLoc loc (Eq ty l r _) = Eq ty l r loc
setLoc loc (DLam body _) = DLam body loc
setLoc loc (Nat _) = Nat loc
setLoc loc (Zero _) = Zero loc
setLoc loc (NAT _) = NAT loc
setLoc loc (Nat n _) = Nat n loc
setLoc loc (Succ p _) = Succ p loc
setLoc loc (STRING _) = STRING loc
setLoc loc (Str s _) = Str s loc
setLoc loc (BOX qty ty _) = BOX qty ty loc
setLoc loc (Box val _) = Box val loc
setLoc loc (E e) = E $ setLoc loc e

49
lib/Quox/Syntax/Term/Pretty.idr
View File

@ -251,12 +251,11 @@ parameters {opts : LayoutOpts} (dnames : BContext d) (tnames : BContext n)
body <- withPrec Outer $ assert_total
prettyTerm (dnames . dbinds) (tnames . tbinds) body
header <- (pat <++>) <$> darrowD
pure $ hsep [header, body] <|> vsep [header, !(indentD body)]
pure $ ifMultiline (header <++> body) (vsep [header, !(indentD body)])
private
prettyCaseBody : List (CaseArm opts d n) -> Eff Pretty (Doc opts)
prettyCaseBody xs =
braces . separateTight !semiD =<< traverse prettyCaseArm xs
prettyCaseBody : List (CaseArm opts d n) -> Eff Pretty (List (Doc opts))
prettyCaseBody xs = traverse prettyCaseArm xs
private
prettyCompPat : {opts : _} -> DimConst -> BindName -> Eff Pretty (Doc opts)
@ -299,7 +298,7 @@ prettyCaseRet dnames tnames body = withPrec Outer $ case body of
S [< x] (Y tm) => do
header <- [|prettyTBind x <++> darrowD|]
body <- assert_total prettyTerm dnames (tnames :< x) tm
pure $ hsep [header, body] <|> vsep [header, !(indentD body)]
hangDSingle header body
private
prettyCase_ : {opts : _} ->
@ -307,10 +306,16 @@ prettyCase_ : {opts : _} ->
Doc opts -> Elim d n -> ScopeTerm d n -> List (CaseArm opts d n) ->
Eff Pretty (Doc opts)
prettyCase_ dnames tnames intro head ret body = do
head <- assert_total prettyElim dnames tnames head
ret <- prettyCaseRet dnames tnames ret
body <- prettyCaseBody dnames tnames body
parensIfM Outer $ sep [intro <++> head, !returnD <++> ret, !ofD <++> body]
head <- assert_total prettyElim dnames tnames head
ret <- prettyCaseRet dnames tnames ret
bodys <- prettyCaseBody dnames tnames body
return <- returnD; of_ <- ofD
lb <- hl Delim "{"; rb <- hl Delim "}"; semi <- semiD
ind <- askAt INDENT
parensIfM Outer $ ifMultiline
(hsep [intro, head, return, ret, of_, lb, hseparateTight semi bodys, rb])
(vsep [intro <++> head, return <++> ret, of_ <++> lb,
indent ind $ vseparateTight semi bodys, rb])
private
prettyCase : {opts : _} ->
@ -338,6 +343,7 @@ prettyTyCasePat : {opts : _} ->
(k : TyConKind) -> BContext (arity k) ->
Eff Pretty (Doc opts)
prettyTyCasePat KTYPE [<] = typeD
prettyTyCasePat KIOState [<] = ioStateD
prettyTyCasePat KPi [< a, b] =
parens . hsep =<< sequence [prettyTBind a, arrowD, prettyTBind b]
prettyTyCasePat KSig [< a, b] =
@ -346,6 +352,7 @@ prettyTyCasePat KEnum [<] = hl Syntax $ text "{}"
prettyTyCasePat KEq [< a0, a1, a, l, r] =
hsep <$> sequence (eqD :: map prettyTBind [a0, a1, a, l, r])
prettyTyCasePat KNat [<] = natD
prettyTyCasePat KString [<] = stringD
prettyTyCasePat KBOX [< a] = bracks =<< prettyTBind a
@ -387,6 +394,9 @@ prettyTerm dnames tnames (TYPE l _) =
pure $ hcat [star, level]
Ascii => [|hl Syntax "Type" <++> hl Universe (text $ show l)|]
prettyTerm dnames tnames (IOState _) =
ioStateD
prettyTerm dnames tnames (Pi qty arg res _) =
parensIfM Outer =<< do
let MkSplitPi {binds, cod} = splitPi [< (qty, res.name, arg)] res.term
@ -439,20 +449,13 @@ prettyTerm dnames tnames (Eq ty l r _) =
prettyTerm dnames tnames s@(DLam {}) =
prettyLambda dnames tnames s
prettyTerm dnames tnames (Nat _) = natD
prettyTerm dnames tnames (Zero _) = hl Syntax "0"
prettyTerm dnames tnames (Succ p _) = do
succD <- succD
let succ : Doc opts -> Eff Pretty (Doc opts)
succ t = prettyAppD succD [t]
toNat : Term d n -> Eff Pretty (Either (Doc opts) Nat)
toNat s with (pushSubsts' s)
_ | Zero _ = pure $ Right 0
_ | Succ d _ = bitraverse succ (pure . S) =<<
toNat (assert_smaller s d)
_ | s' = map Left . withPrec Arg $
prettyTerm dnames tnames $ assert_smaller s s'
either succ (hl Syntax . text . show . S) =<< toNat p
prettyTerm dnames tnames (NAT _) = natD
prettyTerm dnames tnames (Nat n _) = hl Syntax $ pshow n
prettyTerm dnames tnames (Succ p _) =
prettyAppD !succD [!(withPrec Arg $ prettyTerm dnames tnames p)]
prettyTerm dnames tnames (STRING _) = stringD
prettyTerm dnames tnames (Str s _) = prettyStrLit s
prettyTerm dnames tnames (BOX qty ty _) =
bracks . hcat =<<

14
lib/Quox/Syntax/Term/Subst.idr
View File

@ -254,6 +254,8 @@ mutual
PushSubsts Term Subst.isCloT where
pushSubstsWith th ph (TYPE l loc) =
nclo $ TYPE l loc
pushSubstsWith th ph (IOState loc) =
nclo $ IOState loc
pushSubstsWith th ph (Pi qty a body loc) =
nclo $ Pi qty (a // th // ph) (body // th // ph) loc
pushSubstsWith th ph (Lam body loc) =
@ -270,12 +272,16 @@ mutual
nclo $ Eq (ty // th // ph) (l // th // ph) (r // th // ph) loc
pushSubstsWith th ph (DLam body loc) =
nclo $ DLam (body // th // ph) loc
pushSubstsWith _ _ (Nat loc) =
nclo $ Nat loc
pushSubstsWith _ _ (Zero loc) =
nclo $ Zero loc
pushSubstsWith _ _ (NAT loc) =
nclo $ NAT loc
pushSubstsWith _ _ (Nat n loc) =
nclo $ Nat n loc
pushSubstsWith th ph (Succ n loc) =
nclo $ Succ (n // th // ph) loc
pushSubstsWith _ _ (STRING loc) =
nclo $ STRING loc
pushSubstsWith _ _ (Str s loc) =
nclo $ Str s loc
pushSubstsWith th ph (BOX pi ty loc) =
nclo $ BOX pi (ty // th // ph) loc
pushSubstsWith th ph (Box val loc) =

29
lib/Quox/Syntax/Term/Tighten.idr
View File

@ -44,6 +44,7 @@ mutual
tightenT' : OPE n1 n2 -> (t : Term d n2) -> (0 nt : NotClo t) =>
Maybe (Term d n1)
tightenT' p (TYPE l loc) = pure $ TYPE l loc
tightenT' p (IOState loc) = pure $ IOState loc
tightenT' p (Pi qty arg res loc) =
Pi qty <$> tightenT p arg <*> tightenS p res <*> pure loc
tightenT' p (Lam body loc) =
@ -60,12 +61,16 @@ mutual
Eq <$> tightenDS p ty <*> tightenT p l <*> tightenT p r <*> pure loc
tightenT' p (DLam body loc) =
DLam <$> tightenDS p body <*> pure loc
tightenT' p (Nat loc) =
pure $ Nat loc
tightenT' p (Zero loc) =
pure $ Zero loc
tightenT' p (NAT loc) =
pure $ NAT loc
tightenT' p (Nat n loc) =
pure $ Nat n loc
tightenT' p (Succ s loc) =
Succ <$> tightenT p s <*> pure loc
tightenT' p (STRING loc) =
pure $ STRING loc
tightenT' p (Str s loc) =
pure $ Str s loc
tightenT' p (BOX qty ty loc) =
BOX qty <$> tightenT p ty <*> pure loc
tightenT' p (Box val loc) =
@ -163,6 +168,8 @@ mutual
Maybe (Term d1 n)
dtightenT' p (TYPE l loc) =
pure $ TYPE l loc
dtightenT' p (IOState loc) =
pure $ IOState loc
dtightenT' p (Pi qty arg res loc) =
Pi qty <$> dtightenT p arg <*> dtightenS p res <*> pure loc
dtightenT' p (Lam body loc) =
@ -179,12 +186,16 @@ mutual
Eq <$> dtightenDS p ty <*> dtightenT p l <*> dtightenT p r <*> pure loc
dtightenT' p (DLam body loc) =
DLam <$> dtightenDS p body <*> pure loc
dtightenT' p (Nat loc) =
pure $ Nat loc
dtightenT' p (Zero loc) =
pure $ Zero loc
dtightenT' p (NAT loc) =
pure $ NAT loc
dtightenT' p (Nat n loc) =
pure $ Nat n loc
dtightenT' p (Succ s loc) =
Succ <$> dtightenT p s <*> pure loc
dtightenT' p (STRING loc) =
pure $ STRING loc
dtightenT' p (Str s loc) =
pure $ Str s loc
dtightenT' p (BOX qty ty loc) =
BOX qty <$> dtightenT p ty <*> pure loc
dtightenT' p (Box val loc) =
@ -320,7 +331,7 @@ public export %inline
typeCase1T : 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} ->
{default (NAT loc) def : Term d n} ->
Elim d n
typeCase1T ty ret k ns body loc {def} =
typeCase ty ret [(k ** ST ns body)] def loc

19
lib/Quox/Syntax/Term/TyConKind.idr
View File

@ -9,7 +9,8 @@ import Generics.Derive
public export
data TyConKind = KTYPE | KPi | KSig | KEnum | KEq | KNat | KBOX
data TyConKind =
KTYPE | KIOState | KPi | KSig | KEnum | KEq | KNat | KString | KBOX
%name TyConKind k
%runElab derive "TyConKind" [Eq.Eq, Ord.Ord, Show.Show, Generic, Meta, DecEq]
@ -25,10 +26,12 @@ allKinds = %runElab do
||| in `type-case`, how many variables are bound in this branch
public export %inline
arity : TyConKind -> Nat
arity KTYPE = 0
arity KPi = 2
arity KSig = 2
arity KEnum = 0
arity KEq = 5
arity KNat = 0
arity KBOX = 1
arity KTYPE = 0
arity KIOState = 0
arity KPi = 2
arity KSig = 2
arity KEnum = 0
arity KEq = 5
arity KNat = 0
arity KString = 0
arity KBOX = 1

65
lib/Quox/Typechecker.idr
View File

@ -41,34 +41,6 @@ lubs ctx [] = zeroFor ctx
lubs ctx (x :: xs) = lubs1 $ x ::: xs
export
typecaseTel : (k : TyConKind) -> BContext (arity k) -> Universe ->
CtxExtension d n (arity k + n)
typecaseTel k xs u = case k of
KTYPE => [<]
-- A : ★ᵤ, B : 0.A → ★ᵤ
KPi =>
let [< a, b] = xs in
[< (Zero, a, TYPE u a.loc),
(Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)]
KSig =>
let [< a, b] = xs in
[< (Zero, a, TYPE u a.loc),
(Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)]
KEnum => [<]
-- A₀ : ★ᵤ, A₁ : ★ᵤ, A : (A₀ ≡ A₁ : ★ᵤ), L : A₀, R : A₀
KEq =>
let [< a0, a1, a, l, r] = xs in
[< (Zero, a0, TYPE u a0.loc),
(Zero, a1, TYPE u a1.loc),
(Zero, a, Eq0 (TYPE u a.loc) (BVT 1 a.loc) (BVT 0 a.loc) a.loc),
(Zero, l, BVT 2 l.loc),
(Zero, r, BVT 2 r.loc)]
KNat => [<]
-- A : ★ᵤ
KBOX => let [< a] = xs in [< (Zero, a, TYPE u a.loc)]
mutual
||| "Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ"
|||
@ -164,6 +136,8 @@ mutual
check' ctx sg t@(TYPE {}) ty = toCheckType ctx sg t ty
check' ctx sg t@(IOState {}) ty = toCheckType ctx sg t ty
check' ctx sg t@(Pi {}) ty = toCheckType ctx sg t ty
check' ctx sg (Lam body loc) ty = do
@ -214,16 +188,22 @@ mutual
-- then Ψ | Γ ⊢ σ · (δ i ⇒ t) ⇐ Eq [i ⇒ A] l r ⊳ Σ
pure qout
check' ctx sg t@(Nat {}) ty = toCheckType ctx sg t ty
check' ctx sg t@(NAT {}) ty = toCheckType ctx sg t ty
check' ctx sg (Zero {}) ty = do
expectNat !(askAt DEFS) ctx SZero ty.loc ty
check' ctx sg (Nat {}) ty = do
expectNAT !(askAt DEFS) ctx SZero ty.loc ty
pure $ zeroFor ctx
check' ctx sg (Succ n {}) ty = do
expectNat !(askAt DEFS) ctx SZero ty.loc ty
expectNAT !(askAt DEFS) ctx SZero ty.loc ty
checkC ctx sg n ty
check' ctx sg t@(STRING {}) ty = toCheckType ctx sg t ty
check' ctx sg t@(Str s {}) ty = do
expectSTRING !(askAt DEFS) ctx SZero ty.loc ty
pure $ zeroFor ctx
check' ctx sg t@(BOX {}) ty = toCheckType ctx sg t ty
check' ctx sg (Box val loc) ty = do
@ -252,6 +232,9 @@ mutual
Just l => unless (k < l) $ throw $ BadUniverse loc k l
Nothing => pure ()
checkType' ctx (IOState loc) u = pure ()
-- Ψ | Γ ⊢₀ IOState ⇒ Type ℓ
checkType' ctx (Pi qty arg res _) u = do
-- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
checkTypeC ctx arg u
@ -292,10 +275,14 @@ mutual
checkType' ctx t@(DLam {}) u =
throw $ NotType t.loc ctx t
checkType' ctx (Nat {}) u = pure ()
checkType' ctx t@(Zero {}) u = throw $ NotType t.loc ctx t
checkType' ctx (NAT {}) u = pure ()
checkType' ctx t@(Nat {}) u = throw $ NotType t.loc ctx t
checkType' ctx t@(Succ {}) u = throw $ NotType t.loc ctx t
checkType' ctx (STRING loc) u = pure ()
-- Ψ | Γ ⊢₀ STRING ⇒ Type ℓ
checkType' ctx t@(Str {}) u = throw $ NotType t.loc ctx t
checkType' ctx (BOX q ty _) u = checkType ctx ty u
checkType' ctx t@(Box {}) u = throw $ NotType t.loc ctx t
@ -328,8 +315,10 @@ mutual
-- if σ ≤ π
expectCompatQ loc sg.qty g.qty.qty
-- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ 𝟎
let Val d = ctx.dimLen; Val n = ctx.termLen
pure $ InfRes {type = g.typeAt u, qout = zeroFor ctx}
pure $ InfRes {
type = g.typeWithAt ctx.dimLen ctx.termLen u,
qout = zeroFor ctx
}
infer' ctx sg (B i _) =
-- if x : A ∈ Γ
@ -426,7 +415,7 @@ mutual
-- if Ψ | Γ ⊢ σ · n ⇒ ℕ ⊳ Σn
nres <- inferC ctx sg n
let nat = nres.type
expectNat !(askAt DEFS) ctx SZero n.loc nat
expectNAT !(askAt DEFS) ctx SZero n.loc nat
-- if Ψ | Γ, n : ℕ ⊢₀ A ⇐ Type
checkTypeC (extendTy Zero ret.name nat ctx) ret.term Nothing
-- if Ψ | Γ ⊢ σ · zer ⇐ A[0 ∷ ℕ/n] ⊳ Σz
@ -435,7 +424,7 @@ mutual
-- with ρ₂ ≤ π'σ, (ρ₁ + ρ₂) ≤ πσ
let [< p, ih] = suc.names
pisg = pi * sg.qty
sucCtx = extendTyN [< (pisg, p, Nat p.loc), (pi', ih, ret.term)] ctx
sucCtx = extendTyN [< (pisg, p, NAT p.loc), (pi', ih, ret.term)] ctx
sucType = substCaseSuccRet suc.names ret
sucout :< qp :< qih <- checkC sucCtx sg suc.term sucType
expectCompatQ loc qih (pi' * sg.qty)

19
lib/Quox/Typing.idr
View File

@ -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 noLoc) $ p.loc `extendL` ih.loc
in
retty.term // (arg ::: shift 2)
@ -104,8 +104,12 @@ parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)}
expectEq = expect ExpectedEq `(Eq {ty, l, r, _}) `((ty, l, r))
export covering %inline
expectNat : Term d n -> Eff fs ()
expectNat = expect ExpectedNat `(Nat {}) `(())
expectNAT : Term d n -> Eff fs ()
expectNAT = expect ExpectedNAT `(NAT {}) `(())
export covering %inline
expectSTRING : Term d n -> Eff fs ()
expectSTRING = expect ExpectedSTRING `(STRING {}) `(())
export covering %inline
expectBOX : Term d n -> Eff fs (Qty, Term d n)
@ -118,7 +122,6 @@ parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)}
whnf : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
tm 0 n -> Eff fs (NonRedex tm 0 n defs sg)
whnf tm = do
let Val n = ctx.termLen
res <- lift $ runExcept $ whnf defs (toWhnfContext ctx) sg tm
rethrow res
@ -152,8 +155,12 @@ parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)}
expectEq = expect ExpectedEq `(Eq {ty, l, r, _}) `((ty, l, r))
export covering %inline
expectNat : Term 0 n -> Eff fs ()
expectNat = expect ExpectedNat `(Nat {}) `(())
expectNAT : Term 0 n -> Eff fs ()
expectNAT = expect ExpectedNAT `(NAT {}) `(())
export covering %inline
expectSTRING : Term 0 n -> Eff fs ()
expectSTRING = expect ExpectedSTRING `(STRING {}) `(())
export covering %inline
expectBOX : Term 0 n -> Eff fs (Qty, Term 0 n)

13
lib/Quox/Typing/Context.idr
View File

@ -58,6 +58,8 @@ record EqContext n where
public export
record WhnfContext d n where
constructor MkWhnfContext
{auto dimLen : Singleton d}
{auto termLen : Singleton n}
dnames : BContext d
tnames : BContext n
tctx : TContext d n
@ -73,7 +75,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|]
@ -232,6 +234,12 @@ namespace EqContext
toWhnfContext (MkEqContext {tnames, tctx, _}) =
MkWhnfContext {dnames = [<], tnames, tctx}
export
injElim : WhnfContext d n -> Elim 0 0 -> Elim d n
injElim ctx e =
let Val d = ctx.dimLen; Val n = ctx.termLen in
e // shift0 d // shift0 n
namespace WhnfContext
public export %inline
empty : WhnfContext 0 0
@ -240,8 +248,9 @@ namespace WhnfContext
export
extendDimN : {s : Nat} -> BContext s -> WhnfContext d n ->
WhnfContext (s + d) n
extendDimN ns (MkWhnfContext {dnames, tnames, tctx}) =
extendDimN ns (MkWhnfContext {dnames, tnames, tctx, dimLen}) =
MkWhnfContext {
dimLen = [|Val s + dimLen|],
dnames = dnames ++ toSnocVect' ns,
tctx = dweakT s <$> tctx,
tnames

345
lib/Quox/Typing/Error.idr
View File

@ -13,6 +13,8 @@ import Derive.Prelude
%language ElabReflection
%hide TT.Name
%default total
public export
record NameContexts d n where
@ -60,17 +62,18 @@ namespace WhnfContext
public export
data Error
= ExpectedTYPE Loc (NameContexts d n) (Term d n)
| ExpectedPi Loc (NameContexts d n) (Term d n)
| ExpectedSig Loc (NameContexts d n) (Term d n)
| ExpectedEnum Loc (NameContexts d n) (Term d n)
| ExpectedEq Loc (NameContexts d n) (Term d n)
| ExpectedNat Loc (NameContexts d n) (Term d n)
| ExpectedBOX Loc (NameContexts d n) (Term d n)
| BadUniverse Loc Universe Universe
| TagNotIn Loc TagVal (SortedSet TagVal)
| BadCaseEnum Loc (SortedSet TagVal) (SortedSet TagVal)
| BadQtys Loc String (TyContext d n) (List (QOutput n, Term d n))
= ExpectedTYPE Loc (NameContexts d n) (Term d n)
| ExpectedPi Loc (NameContexts d n) (Term d n)
| ExpectedSig Loc (NameContexts d n) (Term d n)
| ExpectedEnum Loc (NameContexts d n) (Term d n)
| ExpectedEq Loc (NameContexts d n) (Term d n)
| ExpectedNAT Loc (NameContexts d n) (Term d n)
| ExpectedSTRING Loc (NameContexts d n) (Term d n)
| ExpectedBOX Loc (NameContexts d n) (Term d n)
| BadUniverse Loc Universe Universe
| TagNotIn Loc TagVal (SortedSet TagVal)
| BadCaseEnum Loc (SortedSet TagVal) (SortedSet TagVal)
| BadQtys Loc String (TyContext d n) (List (QOutput n, Term d n))
-- first term arg of ClashT is the type
| ClashT Loc (EqContext n) EqMode (Term 0 n) (Term 0 n) (Term 0 n)
@ -124,7 +127,8 @@ Located Error where
(ExpectedSig loc _ _).loc = loc
(ExpectedEnum loc _ _).loc = loc
(ExpectedEq loc _ _).loc = loc
(ExpectedNat loc _ _).loc = loc
(ExpectedNAT loc _ _).loc = loc
(ExpectedSTRING loc _ _).loc = loc
(ExpectedBOX loc _ _).loc = loc
(BadUniverse loc _ _).loc = loc
(TagNotIn loc _ _).loc = loc
@ -246,162 +250,171 @@ where
hangDSingle "with quantities" $
separateTight !commaD $ toSnocList' !(traverse prettyQty qs)]
export
prettyErrorNoLoc : {opts : _} -> (showContext : Bool) -> Error ->
Eff Pretty (Doc opts)
prettyErrorNoLoc showContext = \case
ExpectedTYPE _ ctx s =>
hangDSingle "expected a type universe, but got"
!(prettyTerm ctx.dnames ctx.tnames s)
ExpectedPi _ ctx s =>
hangDSingle "expected a function type, but got"
!(prettyTerm ctx.dnames ctx.tnames s)
ExpectedSig _ ctx s =>
hangDSingle "expected a pair type, but got"
!(prettyTerm ctx.dnames ctx.tnames s)
ExpectedEnum _ ctx s =>
hangDSingle "expected an enumeration type, but got"
!(prettyTerm ctx.dnames ctx.tnames s)
ExpectedEq _ ctx s =>
hangDSingle "expected an enumeration type, but got"
!(prettyTerm ctx.dnames ctx.tnames s)
ExpectedNat _ ctx s =>
hangDSingle
("expected the type" <++>
!(prettyTerm [<] [<] $ Nat noLoc) <+> ", but got")
!(prettyTerm ctx.dnames ctx.tnames s)
ExpectedBOX _ ctx s =>
hangDSingle "expected a box type, but got"
!(prettyTerm ctx.dnames ctx.tnames s)
BadUniverse _ k l => pure $
sep ["the universe level" <++> !(prettyUniverse k),
"is not strictly less than" <++> !(prettyUniverse l)]
TagNotIn _ tag set =>
hangDSingle (hsep ["the tag", !(prettyTag tag), "is not contained in"])
!(prettyTerm [<] [<] $ Enum set noLoc)
BadCaseEnum _ head body => sep <$> sequence
[hangDSingle "case expression has head of type"
!(prettyTerm [<] [<] $ Enum head noLoc),
hangDSingle "but cases for"
!(prettyTerm [<] [<] $ Enum body noLoc)]
BadQtys _ what ctx arms =>
hangDSingle (text "inconsistent variable usage in \{what}") $
sep !(printCaseQtys ctx ctx.tnames arms)
ClashT _ ctx mode ty s t =>
inEContext ctx . sep =<< sequence
[hangDSingle "the term" !(prettyTerm [<] ctx.tnames s),
hangDSingle (text "is not \{prettyMode mode}")
!(prettyTerm [<] ctx.tnames t),
hangDSingle "at type" !(prettyTerm [<] ctx.tnames ty)]
ClashTy _ ctx mode a b =>
inEContext ctx . sep =<< sequence
[hangDSingle "the type" !(prettyTerm [<] ctx.tnames a),
hangDSingle (text "is not \{prettyMode mode}")
!(prettyTerm [<] ctx.tnames b)]
ClashE _ ctx mode e f =>
inEContext ctx . sep =<< sequence
[hangDSingle "the term" !(prettyElim [<] ctx.tnames e),
hangDSingle (text "is not \{prettyMode mode}")
!(prettyElim [<] ctx.tnames f)]
ClashU _ mode k l => pure $
sep ["the universe level" <++> !(prettyUniverse k),
text "is not \{prettyModeU mode}" <++> !(prettyUniverse l)]
ClashQ _ pi rh => pure $
sep ["the quantity" <++> !(prettyQty pi),
"is not equal to" <++> !(prettyQty rh)]
NotInScope _ x => pure $
hsep [!(prettyFree x), "is not in scope"]
NotType _ ctx s =>
inTContext ctx . sep =<< sequence
[hangDSingle "the term" !(prettyTerm ctx.dnames ctx.tnames s),
pure "is not a type"]
WrongType _ ctx ty s =>
inEContext ctx . sep =<< sequence
[hangDSingle "the term" !(prettyTerm [<] ctx.tnames s),
hangDSingle "cannot have type" !(prettyTerm [<] ctx.tnames ty)]
MissingEnumArm _ tag tags => pure $
sep [hsep ["the tag", !(prettyTag tag), "is not contained in"],
!(prettyTerm [<] [<] $ Enum (fromList tags) noLoc)]
WhileChecking ctx sg s a err =>
[|vappendBlank
(inTContext ctx . sep =<< sequence
[hangDSingle "while checking" !(prettyTerm ctx.dnames ctx.tnames s),
hangDSingle "has type" !(prettyTerm ctx.dnames ctx.tnames a),
hangDSingle "with quantity" !(prettyQty sg.qty)])
(prettyErrorNoLoc showContext err)|]
WhileCheckingTy ctx a k err =>
[|vappendBlank
(inTContext ctx . sep =<< sequence
[hangDSingle "while checking" !(prettyTerm ctx.dnames ctx.tnames a),
pure $ text $ isTypeInUniverse k])
(prettyErrorNoLoc showContext err)|]
WhileInferring ctx sg e err =>
[|vappendBlank
(inTContext ctx . sep =<< sequence
[hangDSingle "while inferring the type of"
!(prettyElim ctx.dnames ctx.tnames e),
hangDSingle "with quantity" !(prettyQty sg.qty)])
(prettyErrorNoLoc showContext err)|]
WhileComparingT ctx mode sg a s t err =>
[|vappendBlank
(inEContext ctx . sep =<< sequence
[hangDSingle "while checking that" !(prettyTerm [<] ctx.tnames s),
hangDSingle (text "is \{prettyMode mode}")
!(prettyTerm [<] ctx.tnames t),
hangDSingle "at type" !(prettyTerm [<] ctx.tnames a),
hangDSingle "with quantity" !(prettyQty sg.qty)])
(prettyErrorNoLoc showContext err)|]
WhileComparingE ctx mode sg e f err =>
[|vappendBlank
(inEContext ctx . sep =<< sequence
[hangDSingle "while checking that" !(prettyElim [<] ctx.tnames e),
hangDSingle (text "is \{prettyMode mode}")
!(prettyElim [<] ctx.tnames f),
hangDSingle "with quantity" !(prettyQty sg.qty)])
(prettyErrorNoLoc showContext err)|]
where
vappendBlank : Doc opts -> Doc opts -> Doc opts
vappendBlank a b = flush a `vappend` b
parameters {opts : LayoutOpts} (showContext : Bool)
export
inContext' : Bool -> a -> (a -> Eff Pretty (Doc opts)) ->
Doc opts -> Eff Pretty (Doc opts)
inContext' null ctx f doc =
if showContext && not null then
pure $ vappend doc (sep ["in context", !(f ctx)])
else pure doc
export %inline
inTContext : TyContext d n -> Doc opts -> Eff Pretty (Doc opts)
inTContext ctx doc =
if showContext && not (null ctx) then
pure $ vappend doc (sep ["in context", !(prettyTyContext ctx)])
else pure doc
inTContext ctx = inContext' (null ctx) ctx prettyTyContext
export %inline
inEContext : EqContext n -> Doc opts -> Eff Pretty (Doc opts)
inEContext ctx doc =
if showContext && not (null ctx) then
pure $ vappend doc (sep ["in context", !(prettyEqContext ctx)])
else pure doc
inEContext ctx = inContext' (null ctx) ctx prettyEqContext
export
prettyError : {opts : _} -> (showContext : Bool) ->
Error -> Eff Pretty (Doc opts)
prettyError showContext err = sep <$> sequence
[prettyLoc err.loc, indentD =<< prettyErrorNoLoc showContext err]
export
prettyErrorNoLoc : Error -> Eff Pretty (Doc opts)
prettyErrorNoLoc err0 = case err0 of
ExpectedTYPE _ ctx s =>
hangDSingle "expected a type universe, but got"
!(prettyTerm ctx.dnames ctx.tnames s)
ExpectedPi _ ctx s =>
hangDSingle "expected a function type, but got"
!(prettyTerm ctx.dnames ctx.tnames s)
ExpectedSig _ ctx s =>
hangDSingle "expected a pair type, but got"
!(prettyTerm ctx.dnames ctx.tnames s)
ExpectedEnum _ ctx s =>
hangDSingle "expected an enumeration type, but got"
!(prettyTerm ctx.dnames ctx.tnames s)
ExpectedEq _ ctx s =>
hangDSingle "expected an enumeration type, but got"
!(prettyTerm ctx.dnames ctx.tnames s)
ExpectedNAT _ ctx s =>
hangDSingle
("expected the type" <++>
!(prettyTerm [<] [<] $ NAT noLoc) <+> ", but got")
!(prettyTerm ctx.dnames ctx.tnames s)
ExpectedSTRING _ ctx s =>
hangDSingle
("expected the type" <++>
!(prettyTerm [<] [<] $ STRING noLoc) <+> ", but got")
!(prettyTerm ctx.dnames ctx.tnames s)
ExpectedBOX _ ctx s =>
hangDSingle "expected a box type, but got"
!(prettyTerm ctx.dnames ctx.tnames s)
BadUniverse _ k l => pure $
sep ["the universe level" <++> !(prettyUniverse k),
"is not strictly less than" <++> !(prettyUniverse l)]
TagNotIn _ tag set =>
hangDSingle (hsep ["the tag", !(prettyTag tag), "is not contained in"])
!(prettyTerm [<] [<] $ Enum set noLoc)
BadCaseEnum _ head body => sep <$> sequence
[hangDSingle "case expression has head of type"
!(prettyTerm [<] [<] $ Enum head noLoc),
hangDSingle "but cases for"
!(prettyTerm [<] [<] $ Enum body noLoc)]
BadQtys _ what ctx arms =>
hangDSingle (text "inconsistent variable usage in \{what}") $
sep !(printCaseQtys ctx ctx.tnames arms)
ClashT _ ctx mode ty s t =>
inEContext ctx . sep =<< sequence
[hangDSingle "the term" !(prettyTerm [<] ctx.tnames s),
hangDSingle (text "is not \{prettyMode mode}")
!(prettyTerm [<] ctx.tnames t),
hangDSingle "at type" !(prettyTerm [<] ctx.tnames ty)]
ClashTy _ ctx mode a b =>
inEContext ctx . sep =<< sequence
[hangDSingle "the type" !(prettyTerm [<] ctx.tnames a),
hangDSingle (text "is not \{prettyMode mode}")
!(prettyTerm [<] ctx.tnames b)]
ClashE _ ctx mode e f =>
inEContext ctx . sep =<< sequence
[hangDSingle "the term" !(prettyElim [<] ctx.tnames e),
hangDSingle (text "is not \{prettyMode mode}")
!(prettyElim [<] ctx.tnames f)]
ClashU _ mode k l => pure $
sep ["the universe level" <++> !(prettyUniverse k),
text "is not \{prettyModeU mode}" <++> !(prettyUniverse l)]
ClashQ _ pi rh => pure $
sep ["the quantity" <++> !(prettyQty pi),
"is not equal to" <++> !(prettyQty rh)]
NotInScope _ x => pure $
hsep [!(prettyFree x), "is not in scope"]
NotType _ ctx s =>
inTContext ctx . sep =<< sequence
[hangDSingle "the term" !(prettyTerm ctx.dnames ctx.tnames s),
pure "is not a type"]
WrongType _ ctx ty s =>
inEContext ctx . sep =<< sequence
[hangDSingle "the term" !(prettyTerm [<] ctx.tnames s),
hangDSingle "cannot have type" !(prettyTerm [<] ctx.tnames ty)]
MissingEnumArm _ tag tags => pure $
sep [hsep ["the tag", !(prettyTag tag), "is not contained in"],
!(prettyTerm [<] [<] $ Enum (fromList tags) noLoc)]
WhileChecking ctx sg s a err =>
[|vappendBlank
(inTContext ctx . sep =<< sequence
[hangDSingle "while checking" !(prettyTerm ctx.dnames ctx.tnames s),
hangDSingle "has type" !(prettyTerm ctx.dnames ctx.tnames a),
hangDSingle "with quantity" !(prettyQty sg.qty)])
(prettyErrorNoLoc err)|]
WhileCheckingTy ctx a k err =>
[|vappendBlank
(inTContext ctx . sep =<< sequence
[hangDSingle "while checking" !(prettyTerm ctx.dnames ctx.tnames a),
pure $ text $ isTypeInUniverse k])
(prettyErrorNoLoc err)|]
WhileInferring ctx sg e err =>
[|vappendBlank
(inTContext ctx . sep =<< sequence
[hangDSingle "while inferring the type of"
!(prettyElim ctx.dnames ctx.tnames e),
hangDSingle "with quantity" !(prettyQty sg.qty)])
(prettyErrorNoLoc err)|]
WhileComparingT ctx mode sg a s t err =>
[|vappendBlank
(inEContext ctx . sep =<< sequence
[hangDSingle "while checking that" !(prettyTerm [<] ctx.tnames s),
hangDSingle (text "is \{prettyMode mode}")
!(prettyTerm [<] ctx.tnames t),
hangDSingle "at type" !(prettyTerm [<] ctx.tnames a),
hangDSingle "with quantity" !(prettyQty sg.qty)])
(prettyErrorNoLoc err)|]
WhileComparingE ctx mode sg e f err =>
[|vappendBlank
(inEContext ctx . sep =<< sequence
[hangDSingle "while checking that" !(prettyElim [<] ctx.tnames e),
hangDSingle (text "is \{prettyMode mode}")
!(prettyElim [<] ctx.tnames f),
hangDSingle "with quantity" !(prettyQty sg.qty)])
(prettyErrorNoLoc err)|]
where
vappendBlank : Doc opts -> Doc opts -> Doc opts
vappendBlank a b = flush a `vappend` b
export
prettyError : Error -> Eff Pretty (Doc opts)
prettyError err = sep <$> sequence
[prettyLoc err.loc, indentD =<< prettyErrorNoLoc err]

536
lib/Quox/Untyped/Erase.idr Normal file
View File

@ -0,0 +1,536 @@
module Quox.Untyped.Erase
import Quox.Definition as Q
import Quox.Pretty
import Quox.Syntax.Term.Base as Q
import Quox.Syntax.Term.Subst
import Quox.Typing
import Quox.Untyped.Syntax as U
import Quox.Whnf
import Quox.EffExtra
import Data.List1
import Data.Singleton
import Data.SnocVect
import Language.Reflection
%default total
%language ElabReflection
%hide TT.Name
%hide AppView.(.head)
public export
data IsErased = Erased | Kept
public export
isErased : Qty -> IsErased
isErased Zero = Erased
isErased One = Kept
isErased Any = Kept
public export
ErasureContext : Nat -> Nat -> Type
ErasureContext = TyContext
public export
TypeError : Type
TypeError = Typing.Error.Error
%hide Typing.Error.Error
public export
data Error =
CompileTimeOnly (ErasureContext d n) (Q.Term d n)
| WrapTypeError TypeError
| Postulate Loc Name
| WhileErasing Name Q.Definition Error
| MainIsErased Loc Name
%name Error err
private %inline
notInScope : Loc -> Name -> Error
notInScope = WrapTypeError .: NotInScope
export
Located Error where
(CompileTimeOnly _ s).loc = s.loc
(WrapTypeError err).loc = err.loc
(Postulate loc _).loc = loc
(WhileErasing _ def e).loc = e.loc `or` def.loc
(MainIsErased loc _).loc = loc
parameters {opts : LayoutOpts} (showContext : Bool)
export
prettyErrorNoLoc : Error -> Eff Pretty (Doc opts)
prettyErrorNoLoc (CompileTimeOnly ctx s) =
inTContext showContext ctx $
sep ["the term", !(prettyTerm ctx.dnames ctx.tnames s),
"only exists at compile time"]
prettyErrorNoLoc (WrapTypeError err) =
prettyErrorNoLoc showContext err
prettyErrorNoLoc (Postulate _ x) =
pure $ sep [!(prettyFree x), "is a postulate with no definition"]
prettyErrorNoLoc (WhileErasing x def err) = pure $
vsep [hsep ["while erasing the definition", !(prettyFree x)],
!(prettyErrorNoLoc err)]
prettyErrorNoLoc (MainIsErased _ x) =
pure $ hsep [!(prettyFree x), "is marked #[main] but is erased"]
export
prettyError : Error -> Eff Pretty (Doc opts)
prettyError err = sep <$> sequence
[prettyLoc err.loc, indentD =<< prettyErrorNoLoc err]
public export
Erase : List (Type -> Type)
Erase = [Except Error, DefsReader, NameGen]
export
liftWhnf : Eff Whnf a -> Eff Erase a
liftWhnf act = lift $ wrapErr WrapTypeError act
export covering
computeElimType : ErasureContext d n -> SQty -> Elim d n -> Eff Erase (Term d n)
computeElimType ctx sg e = do
defs <- askAt DEFS
let ctx = toWhnfContext ctx
liftWhnf $ do
Element e _ <- whnf defs ctx sg e
computeElimType defs ctx sg e
private %macro
wrapExpect : TTImp ->
Elab (TyContext d n -> Loc -> Term d n -> Eff Erase a)
wrapExpect f_ = do
f <- check `(\x => ~(f_) x)
pure $ \ctx, loc, s => liftWhnf $ f !(askAt DEFS) ctx SZero loc s
public export
record EraseElimResult d n where
constructor EraRes
type : Lazy (Q.Term d n)
term : U.Term n
-- "Ψ | Γ | Σ ⊢ s ⤋ s' ⇐ A" for `s' <- eraseTerm (Ψ,Γ,Σ) A s`
--
-- in the below comments, Ψ, Γ, Σ are implicit and
-- only their extensions are written
export covering
eraseTerm : ErasureContext d n ->
(ty, tm : Q.Term d n) -> Eff Erase (U.Term n)
-- "Ψ | Γ | Σ ⊢ e ⤋ e' ⇒ A" for `EraRes A e' <- eraseElim (Ψ,Γ,Σ) e`
export covering
eraseElim : ErasureContext d n -> (tm : Q.Elim d n) ->
Eff Erase (EraseElimResult d n)
eraseTerm ctx _ s@(TYPE {}) =
throw $ CompileTimeOnly ctx s
eraseTerm ctx _ s@(IOState {}) =
throw $ CompileTimeOnly ctx s
eraseTerm ctx _ s@(Pi {}) =
throw $ CompileTimeOnly ctx s
-- x : A | 0.x ⊢ s ⤋ s' ⇐ B
-- -------------------------------------
-- (λ x ⇒ s) ⤋ s'[⌷/x] ⇐ 0.(x : A) → B
--
-- x : A | π.x ⊢ s ⤋ s' ⇐ B π ≠ 0
-- ----------------------------------------
-- (λ x ⇒ s) ⤋ (λ x ⇒ s') ⇐ π.(x : A) → B
eraseTerm ctx ty (Lam body loc) = do
let x = body.name
(qty, arg, res) <- wrapExpect `(expectPi) ctx loc ty
body <- eraseTerm (extendTy qty x arg ctx) res.term body.term
pure $ case isErased qty of
Kept => U.Lam x body loc
Erased => sub1 (Erased loc) body
eraseTerm ctx _ s@(Sig {}) =
throw $ CompileTimeOnly ctx s
-- s ⤋ s' ⇐ A t ⤋ t' ⇐ B[s/x]
-- ---------------------------------
-- (s, t) ⤋ (s', t') ⇐ (x : A) × B
eraseTerm ctx ty (Pair fst snd loc) = do
(a, b) <- wrapExpect `(expectSig) ctx loc ty
let b = sub1 b (Ann fst a a.loc)
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 loc
eraseTerm ctx ty s@(Eq {}) =
throw $ CompileTimeOnly ctx s
-- 𝑖 ⊢ s ⤋ s' ⇐ A
-- ---------------------------------
-- (δ 𝑖 ⇒ s) ⤋ s' ⇐ Eq (𝑖 ⇒ A) l r
eraseTerm ctx ty (DLam body loc) = do
a <- fst <$> wrapExpect `(expectEq) ctx loc ty
eraseTerm (extendDim body.name ctx) a.term body.term
eraseTerm ctx _ s@(NAT {}) =
throw $ CompileTimeOnly ctx s
-- n ⤋ n ⇐ ℕ
eraseTerm _ _ (Nat n loc) =
pure $ Nat n loc
-- s ⤋ s' ⇐ ℕ
-- -----------------------
-- succ s ⤋ succ s' ⇐ ℕ
eraseTerm ctx ty (Succ p loc) = do
p <- eraseTerm ctx ty p
pure $ Succ p loc
eraseTerm ctx ty s@(STRING {}) =
throw $ CompileTimeOnly ctx s
-- s ⤋ s ⇐ String
eraseTerm _ _ (Str s loc) =
pure $ Str s loc
eraseTerm ctx ty s@(BOX {}) =
throw $ CompileTimeOnly ctx s
-- [s] ⤋ ⌷ ⇐ [0.A]
--
-- π ≠ 0 s ⤋ s' ⇐ A
-- --------------------
-- [s] ⤋ s' ⇐ [π.A]
eraseTerm ctx ty (Box val loc) = do
(qty, a) <- wrapExpect `(expectBOX) ctx loc ty
case isErased qty of
Erased => pure $ Erased loc
Kept => eraseTerm ctx a val
-- e ⤋ e' ⇒ B
-- ------------
-- e ⤋ e' ⇐ A
eraseTerm ctx ty (E e) =
term <$> eraseElim ctx e
eraseTerm ctx ty (CloT (Sub term th)) =
eraseTerm ctx ty $ pushSubstsWith' id th term
eraseTerm ctx ty (DCloT (Sub term th)) =
eraseTerm ctx ty $ pushSubstsWith' th id term
-- defω x : A = s
-- ----------------
-- x ⤋ x ⇒ A
eraseElim ctx e@(F x u loc) = do
Just def <- asksAt DEFS $ lookup x
| Nothing => throw $ notInScope loc x
case isErased def.qty.qty of
Erased => throw $ CompileTimeOnly ctx $ E e
Kept => pure $ EraRes (def.typeWith ctx.dimLen ctx.termLen) $ F x loc
-- π.x ∈ Σ π ≠ 0
-- -----------------
-- x ⤋ x ⇒ A
eraseElim ctx e@(B i loc) = do
case isErased $ ctx.qtys !!! i of
Erased => throw $ CompileTimeOnly ctx $ E e
Kept => pure $ EraRes (ctx.tctx !! i) $ B i loc
-- f ⤋ f' ⇒ π.(x : A) → B s ⤋ s' ⇒ A π ≠ 0
-- ---------------------------------------------
-- f s ⤋ f' s' ⇒ B[s/x]
--
-- f ⤋ f' ⇒ 0.(x : A) → B
-- -------------------------
-- f s ⤋ f' ⇒ B[s/x]
eraseElim ctx (App fun arg loc) = do
efun <- eraseElim ctx fun
(qty, targ, tres) <- wrapExpect `(expectPi) ctx loc efun.type
let ty = sub1 tres (Ann arg targ arg.loc)
case isErased qty of
Erased => pure $ EraRes ty efun.term
Kept => do arg <- eraseTerm ctx targ arg
pure $ EraRes ty $ App efun.term arg loc
-- e ⇒ (x : A) × B
-- x : A, y : B | ρ.x, ρ.y ⊢ s ⤋ s' ⇐ R[((x,y) ∷ (x : A) × B)/z]
-- -------------------------------------------------------------------
-- (case0 e return z ⇒ R of {(x, y) ⇒ s}) ⤋ s'[⌷/x, ⌷/y] ⇒ R[e/z]
--
-- e ⤋ e' ⇒ (x : A) × B ρ ≠ 0
-- x : A, y : B | ρ.x, ρ.y ⊢ s ⤋ s' ⇐ R[((x,y) ∷ (x : A) × B)/z]
-- ----------------------------------------------------------------------------
-- (caseρ e return z ⇒ R of {(x, y) ⇒ s}) ⤋
-- ⤋
-- let xy = e' in let x = fst xy in let y = snd xy in s' ⇒ R[e/z]
eraseElim ctx (CasePair qty pair ret body loc) = do
let [< x, y] = body.names
case isErased qty of
Kept => do
EraRes ety eterm <- eraseElim ctx pair
let ty = sub1 (ret // shift 2) $
Ann (Pair (BVT 0 loc) (BVT 1 loc) loc) (weakT 2 ety) loc
(tfst, tsnd) <- wrapExpect `(expectSig) ctx loc ety
let ctx' = extendTyN [< (qty, x, tfst), (qty, y, tsnd.term)] ctx
body' <- eraseTerm ctx' ty body.term
p <- mnb "p" loc
pure $ EraRes (sub1 ret pair) $
Let p eterm
(Let x (Fst (B VZ loc) loc)
(Let y (Snd (B (VS VZ) loc) loc)
(body' // (B VZ loc ::: B (VS VZ) loc ::: shift 3))
loc) loc) loc
Erased => do
ety <- computeElimType ctx SOne pair
let ty = sub1 (ret // shift 2) $
Ann (Pair (BVT 0 loc) (BVT 1 loc) loc) (weakT 2 ety) loc
(tfst, tsnd) <- wrapExpect `(expectSig) ctx loc ety
let ctx' = extendTyN0 [< (x, tfst), (y, tsnd.term)] ctx
body' <- eraseTerm ctx' ty body.term
pure $ EraRes (sub1 ret pair) $ subN [< Erased loc, Erased loc] body'
-- e ⤋ e' ⇒ (x : A) × B
-- ----------------------
-- fst e ⤋ fst e' ⇒ A
eraseElim ctx (Fst pair loc) = do
epair <- eraseElim ctx pair
a <- fst <$> wrapExpect `(expectSig) ctx loc epair.type
pure $ EraRes a $ Fst epair.term loc
-- e ⤋ e' ⇒ (x : A) × B
-- -----------------------------
-- snd e ⤋ snd e' ⇒ B[fst e/x]
eraseElim ctx (Snd pair loc) = do
epair <- eraseElim ctx pair
b <- snd <$> wrapExpect `(expectSig) ctx loc epair.type
pure $ EraRes (sub1 b (Fst pair loc)) $ Snd epair.term loc
-- caseρ e return z ⇒ R of {} ⤋ absurd ⇒ R[e/z]
--
-- s ⤋ s' ⇐ R[𝐚∷{𝐚}/z]
-- -----------------------------------------------
-- case0 e return z ⇒ R of {𝐚 ⇒ s} ⤋ s' ⇒ R[e/z]
--
-- e ⤋ e' ⇒ A sᵢ ⤋ s'ᵢ ⇐ R[𝐚ᵢ/z] ρ ≠ 0 i ≠ 0
-- -------------------------------------------------------------------
-- caseρ e return z ⇒ R of {𝐚ᵢ ⇒ sᵢ} ⤋ case e of {𝐚ᵢ ⇒ s'ᵢ} ⇒ R[e/z]
eraseElim ctx e@(CaseEnum qty tag ret arms loc) = do
let ty = sub1 ret tag
case isErased qty of
Erased => case SortedMap.toList arms of
[] => pure $ EraRes ty $ Absurd loc
[(t, rhs)] => do
let ty' = sub1 ret (Ann (Tag t loc) (enum [t] loc) loc)
rhs' <- eraseTerm ctx ty' rhs
pure $ EraRes ty rhs'
_ => throw $ CompileTimeOnly ctx $ E e
Kept => case List1.fromList $ SortedMap.toList arms of
Nothing => pure $ EraRes ty $ Absurd loc
Just arms => do
etag <- eraseElim ctx tag
arms <- for arms $ \(t, rhs) => do
let ty' = sub1 ret (Ann (Tag t loc) etag.type loc)
rhs' <- eraseTerm ctx ty' rhs
pure (t, rhs')
pure $ EraRes ty $ CaseEnum etag.term arms loc
-- n ⤋ n' ⇒ ℕ z ⤋ z' ⇐ R[zero∷ℕ/z] ς ≠ 0
-- m : ℕ, ih : R[m/z] | ρ.m, ς.ih ⊢ s ⤋ s' ⇐ R[(succ m)∷ℕ/z]
-- -----------------------------------------------------------
-- caseρ n return z ⇒ R of {0 ⇒ z; succ m, ς.ih ⇒ s}
-- ⤋
-- case n' of {0 ⇒ z'; succ m, ih ⇒ s'} ⇒ R[n/z]
--
-- n ⤋ n' ⇒ ℕ z ⤋ z' ⇐ R[zero∷ℕ/z]
-- m : ℕ, ih : R[m/z] | ρ.m, 0.ih ⊢ s ⤋ s' ⇐ R[(succ m)∷ℕ/z]
-- -----------------------------------------------------------
-- caseρ n return z ⇒ R of {0 ⇒ z; succ m, 0.ih ⇒ s}
-- ⤋
-- case n' of {0 ⇒ z'; succ m ⇒ s'[⌷/ih]} ⇒ R[n/z]
eraseElim ctx (CaseNat qty qtyIH nat ret zero succ loc) = do
let ty = sub1 ret nat
enat <- 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
let succ = case isErased qtyIH of
Kept => NSRec p ih succ'
Erased => NSNonrec p (sub1 (Erased loc) succ')
pure $ EraRes ty $ CaseNat enat.term zero succ loc
-- b ⤋ b' ⇒ [π.A] πρ ≠ 0 x : A | πρ.x ⊢ s ⤋ s' ⇐ R[[x]∷[π.A]/z]
-- ------------------------------------------------------------------
-- caseρ b return z ⇒ R of {[x] ⇒ s} ⤋ let x = b' in s' ⇒ R[b/z]
--
-- b ⇒ [π.A] x : A | 0.x ⊢ s ⤋ s' ⇐ R[[x]∷[0.A]/z] πρ = 0
-- -------------------------------------------------------------
-- caseρ b return z ⇒ R of {[x] ⇒ s} ⤋ s'[⌷/x] ⇒ R[b/z]
eraseElim ctx (CaseBox qty box ret body loc) = do
tbox <- computeElimType ctx SOne box -- [fixme] is there any way to avoid this?
(pi, tinner) <- wrapExpect `(expectBOX) ctx loc tbox
let ctx' = extendTy (pi * qty) body.name tinner ctx
bty = sub1 (ret // shift 1) $
Ann (Box (BVT 0 loc) loc) (weakT 1 tbox) loc
case isErased $ qty * pi of
Kept => do
ebox <- eraseElim ctx box
ebody <- eraseTerm ctx' bty body.term
pure $ EraRes (sub1 ret box) $ Let body.name ebox.term ebody loc
Erased => do
body' <- eraseTerm ctx' bty body.term
pure $ EraRes (sub1 ret box) $ body' // one (Erased loc)
-- f ⤋ f' ⇒ Eq (𝑖 ⇒ A) l r
-- ------------------------------
-- f @r ⤋ f' ⇒ A‹r/𝑖›
eraseElim ctx (DApp fun arg loc) = do
efun <- eraseElim ctx fun
a <- fst <$> wrapExpect `(expectEq) ctx loc efun.type
pure $ EraRes (dsub1 a arg) efun.term
-- s ⤋ s' ⇐ A
-- ----------------
-- s ∷ A ⤋ s' ⇒ A
eraseElim ctx (Ann tm ty loc) =
EraRes ty <$> eraseTerm ctx ty tm
-- s ⤋ s' ⇐ A‹p/𝑖›
-- -----------------------------------
-- coe (𝑖 ⇒ A) @p @q s ⤋ s' ⇒ A‹q/𝑖›
eraseElim ctx (Coe ty p q val loc) = do
val <- eraseTerm ctx (dsub1 ty p) val
pure $ EraRes (dsub1 ty q) val
-- s ⤋ s' ⇐ A
-- --------------------------------
-- comp A @p @q s @r {⋯} ⤋ s' ⇒ A
eraseElim ctx (Comp ty p q val r zero one loc) =
EraRes ty <$> eraseTerm ctx ty val
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
eraseElim ctx (DCloE (Sub term th)) =
eraseElim ctx $ pushSubstsWith' th id term
export
uses : Var n -> Term n -> Nat
uses i (F {}) = 0
uses i (B j _) = if i == j then 1 else 0
uses i (Lam x body _) = uses (VS i) body
uses i (App fun arg _) = uses i fun + uses i arg
uses i (Pair fst snd _) = uses i fst + uses i snd
uses i (Fst pair _) = uses i pair
uses i (Snd pair _) = uses i pair
uses i (Tag tag _) = 0
uses i (CaseEnum tag cases _) =
uses i tag + foldl max 0 (map (assert_total uses i . snd) cases)
uses i (Absurd {}) = 0
uses i (Nat {}) = 0
uses i (Succ nat _) = uses i nat
uses i (CaseNat nat zer suc _) = uses i nat + max (uses i zer) (uses' suc)
where uses' : CaseNatSuc n -> Nat
uses' (NSRec _ _ s) = uses (VS (VS i)) s
uses' (NSNonrec _ s) = uses (VS i) s
uses i (Str {}) = 0
uses i (Let x rhs body _) = uses i rhs + uses (VS i) body
uses i (Erased {}) = 0
export
inlineable : U.Term n -> Bool
inlineable (F {}) = True
inlineable (B {}) = True
inlineable (Tag {}) = True
inlineable (Nat {}) = True
inlineable (Str {}) = True
inlineable (Absurd {}) = True
inlineable (Erased {}) = True
inlineable _ = False
export
droppable : U.Term n -> Bool
droppable (F {}) = True
droppable (B {}) = True
droppable (Fst e _) = droppable e
droppable (Snd e _) = droppable e
droppable (Tag {}) = True
droppable (Nat {}) = True
droppable (Str {}) = True
droppable (Absurd {}) = True
droppable (Erased {}) = True
droppable _ = False
export
trimLets : U.Term n -> U.Term n
trimLets (F x loc) = F x loc
trimLets (B i loc) = B i loc
trimLets (Lam x body loc) = Lam x (trimLets body) loc
trimLets (App fun arg loc) = App (trimLets fun) (trimLets arg) loc
trimLets (Pair fst snd loc) = Pair (trimLets fst) (trimLets snd) loc
trimLets (Fst pair loc) = Fst (trimLets pair) loc
trimLets (Snd pair loc) = Snd (trimLets pair) loc
trimLets (Tag tag loc) = Tag tag loc
trimLets (CaseEnum tag cases loc) =
let tag = trimLets tag
cases = map (map $ \c => trimLets $ assert_smaller cases c) cases in
if droppable tag && length cases == 1
then snd cases.head
else CaseEnum tag cases loc
trimLets (Absurd loc) = Absurd loc
trimLets (Nat n loc) = Nat n loc
trimLets (Succ nat loc) = Succ (trimLets nat) loc
trimLets (CaseNat nat zer suc loc) =
CaseNat (trimLets nat) (trimLets zer) (trimLets' suc) loc
where trimLets' : CaseNatSuc n -> CaseNatSuc n
trimLets' (NSRec x ih s) = NSRec x ih $ trimLets s
trimLets' (NSNonrec x s) = NSNonrec x $ trimLets s
trimLets (Str s loc) = Str s loc
trimLets (Let x rhs body loc) =
let rhs' = trimLets rhs
body' = trimLets body
uses = uses VZ body in
if inlineable rhs' || uses == 1 || (droppable rhs' && uses == 0)
then sub1 rhs' body'
else Let x rhs' body' loc
trimLets (Erased loc) = Erased loc
export covering
eraseDef : Name -> Q.Definition -> Eff Erase U.Definition
eraseDef name def@(MkDef qty type body scheme isMain loc) =
wrapErr (WhileErasing name def) $
case isErased qty.qty of
Erased => do
when isMain $ throw $ MainIsErased loc name
pure ErasedDef
Kept =>
case scheme of
Just str => pure $ SchemeDef isMain str
Nothing => case body of
Postulate => throw $ Postulate loc name
Concrete body => KeptDef isMain . trimLets <$>
eraseTerm empty type body

374
lib/Quox/Untyped/Scheme.idr Normal file
View File

@ -0,0 +1,374 @@
module Quox.Untyped.Scheme
import Quox.Name
import Quox.Context
import Quox.Untyped.Syntax
import Quox.Pretty
import Quox.EffExtra
import Quox.CharExtra
import Data.DPair
import Data.List1
import Data.String
import Data.SortedSet
import Data.Vect
import Derive.Prelude
%default total
%language ElabReflection
%hide TT.Name
export
isSchemeInitial : Char -> Bool
isSchemeInitial c =
let gc = genCat c in
isLetter gc || isSymbol gc && c /= '|' ||
gc == Number Letter ||
gc == Number Other ||
gc == Mark NonSpacing ||
gc == Punctuation Dash ||
gc == Punctuation Connector ||
gc == Punctuation Other && c /= '\'' && c /= '\\' ||
gc == Other PrivateUse ||
(c `elem` unpack "!$%&*/:<=>?~_^")
export
isSchemeSubsequent : Char -> Bool
isSchemeSubsequent c =
let gc = genCat c in
isSchemeInitial c ||
isNumber gc ||
isMark gc ||
(c `elem` unpack ".+-@")
export
isSchemeId : String -> Bool
isSchemeId str =
str == "1+" || str == "1-" ||
case unpack str of
[] => False
c :: cs => isSchemeInitial c && all isSchemeSubsequent cs
export
escId : String -> String
escId str =
let str' = concatMap doEsc $ unpack str in
if isSchemeId str' then str' else "|\{str}|"
where
doEsc : Char -> String
doEsc '\\' = "\\\\"
doEsc '|' = "\\|"
doEsc '\'' = "^"
doEsc c = singleton c
public export
data Id = I String Nat
%runElab derive "Id" [Eq, Ord]
private
prettyId' : {opts : LayoutOpts} -> Id -> Doc opts
prettyId' (I str 0) = text $ escId str
prettyId' (I str k) = text $ escId "\{str}:\{show k}"
export
prettyId : {opts : LayoutOpts} -> Id -> Eff Pretty (Doc opts)
prettyId x = hl TVar $ prettyId' x
public export
data StateTag = AVOID | MAIN
public export
Scheme : List (Type -> Type)
Scheme = [StateL AVOID (SortedSet Id), StateL MAIN (List Id)]
-- names to avoid, and functions with #[main] (should only be one)
public export
data Sexp =
V Id
| L (List Sexp)
| Q Sexp
| N Nat
| S String
| Lambda (List Id) Sexp
| LambdaC (List Id) Sexp -- curried lambda
| Let Id Sexp Sexp
| Case Sexp (List1 (List Sexp, Sexp))
| Define Id Sexp
| Literal String
export
FromString Sexp where fromString s = V $ I s 0
private
makeIdBase : Mods -> String -> String
makeIdBase mods str = joinBy "." $ toList $ mods :< str
export
makeId : Name -> Id
makeId (MakeName mods (UN str)) = I (makeIdBase mods str) 0
makeId (MakeName mods (MN str k)) = I (makeIdBase mods str) 0
makeId (MakeName mods Unused) = I (makeIdBase mods "_") 0
export
makeIdB : BindName -> Id
makeIdB (BN name _) = makeId $ MakeName [<] name
private
bump : Id -> Id
bump (I x i) = I x (S i)
export covering
getFresh : SortedSet Id -> Id -> Id
getFresh used x =
if contains x used then getFresh used (bump x) else x
export covering
freshIn : Id -> (Id -> Eff Scheme a) -> Eff Scheme a
freshIn x k =
let x = getFresh !(getAt AVOID) x in
localAt AVOID (insert x) $ k x
export covering
freshInB : BindName -> (Id -> Eff Scheme a) -> Eff Scheme a
freshInB x = freshIn (makeIdB x)
export covering
freshInBT : Telescope' BindName m n ->
(Telescope' Id m n -> Eff Scheme a) ->
Eff Scheme a
freshInBT xs act = do
let (xs', used') = go (map makeIdB xs) !(getAt AVOID)
localAt_ AVOID used' $ act xs'
where
go : forall n. Telescope' Id m n ->
SortedSet Id -> (Telescope' Id m n, SortedSet Id)
go [<] used = ([<], used)
go (xs :< x) used =
let x = getFresh used x
(xs, used) = go xs (insert x used)
in
(xs :< x, used)
export covering
freshInBC : Context' BindName n -> (Context' Id n -> Eff Scheme a) ->
Eff Scheme a
freshInBC = freshInBT
export covering
toScheme : Context' Id n -> Term n -> Eff Scheme Sexp
toScheme xs (F x _) = pure $ V $ makeId x
toScheme xs (B i _) = pure $ V $ xs !!! i
toScheme xs (Lam x body _) =
let Evidence n' (ys, body) = splitLam [< x] body in
freshInBT ys $ \ys => do
pure $ LambdaC (toList' ys) !(toScheme (xs . ys) body)
toScheme xs (App fun arg _) = do
let (fun, args) = splitApp fun
fun <- toScheme xs fun
args <- traverse (toScheme xs) args
arg <- toScheme xs arg
pure $ if null args
then L [fun, arg]
else L $ "%" :: fun :: toList (args :< arg)
toScheme xs (Pair fst snd _) =
pure $ L ["cons", !(toScheme xs fst), !(toScheme xs snd)]
toScheme xs (Fst pair _) =
pure $ L ["car", !(toScheme xs pair)]
toScheme xs (Snd pair _) =
pure $ L ["cdr", !(toScheme xs pair)]
toScheme xs (Tag tag _) =
pure $ Q $ fromString tag
toScheme xs (CaseEnum tag cases _) =
Case <$> toScheme xs tag
<*> for cases (\(t, rhs) => ([fromString t],) <$> toScheme xs rhs)
toScheme xs (Absurd _) =
pure $ Q "absurd"
toScheme xs (Nat n _) =
pure $ N n
toScheme xs (Succ nat _) =
pure $ L ["+", !(toScheme xs nat), N 1]
toScheme xs (CaseNat nat zer (NSRec p ih suc) _) =
freshInBC [< p, ih] $ \[< p, ih] =>
pure $
L ["case-nat-rec",
Lambda [] !(toScheme xs zer),
Lambda [p, ih] !(toScheme (xs :< p :< ih) suc),
!(toScheme xs nat)]
toScheme xs (Str s _) = pure $ S s
toScheme xs (CaseNat nat zer (NSNonrec p suc) _) =
freshInB p $ \p =>
pure $
L ["case-nat-nonrec",
Lambda [] !(toScheme xs zer),
Lambda [p] !(toScheme (xs :< p) suc),
!(toScheme xs nat)]
toScheme xs (Let x rhs body _) =
freshInB x $ \x =>
pure $ Let x !(toScheme xs rhs) !(toScheme (xs :< x) body)
toScheme xs (Erased _) =
pure $ Q "erased"
export
prelude : String
prelude = """
#!r6rs
; curried lambda
(define-syntax lambda%
(syntax-rules ()
[(_ (x0 x1 ...) body ...)
(lambda (x0) (lambda% (x1 ...) body ...))]
[(_ () body ...)
(begin body ...)]))
; curried application
(define-syntax %
(syntax-rules ()
[(_ e0 e1 e2 ...)
(% (e0 e1) e2 ...)]
[(_ e) e]))
; curried function definition
(define-syntax define%
(syntax-rules ()
[(_ (f x ...) body ...)
(define f (lambda% (x ...) body ...))]
[(_ x body ...)
(define x body ...)]))
(define-syntax builtin-io
(syntax-rules ()
[(_ body ...)
(lambda (s)
(let [(res (begin body ...))]
(cons res s)))]))
(define (case-nat-rec z s n)
(let go [(acc (z)) (i 0)]
(if (= i n) acc (go (s i acc) (+ i 1)))))
(define (case-nat-nonrec z s n)
(if (= n 0) (z) (s (- n 1))))
(define (run-main f) (f 'io-state) (void))
;;;;;;
"""
export covering
defToScheme : Name -> Definition -> Eff Scheme (Maybe Sexp)
defToScheme x ErasedDef = pure Nothing
defToScheme x (KeptDef isMain def) = do
let x = makeId x
when isMain $ modifyAt MAIN (x ::)
modifyAt AVOID $ insert x
pure $ Just $ Define x !(toScheme [<] def)
defToScheme x (SchemeDef isMain str) = do
let x = makeId x
when isMain $ modifyAt MAIN (x ::)
modifyAt AVOID $ insert x
pure $ Just $ Define x $ Literal str
orIndent : {opts : LayoutOpts} -> Doc opts -> Doc opts -> Eff Pretty (Doc opts)
orIndent a b = do
one <- parens $ a <++> b
two <- parens $ a `vappend` indent 2 b
pure $ ifMultiline one two
export covering
prettySexp : {opts : LayoutOpts} -> Sexp -> Eff Pretty (Doc opts)
private covering
prettyLambda : {opts : LayoutOpts} ->
String -> List Id -> Sexp -> Eff Pretty (Doc opts)
prettyLambda lam xs e =
orIndent
(hsep [!(hl Syntax $ text lam), !(prettySexp $ L $ map V xs)])
!(prettySexp e)
private covering
prettyBind : {opts : LayoutOpts} -> (Id, Sexp) -> Eff Pretty (Doc opts)
prettyBind (x, e) = parens $ sep [!(prettyId x), !(prettySexp e)]
private covering
prettyLet : {opts : LayoutOpts} ->
SnocList (Id, Sexp) -> Sexp -> Eff Pretty (Doc opts)
prettyLet ps (Let x rhs body) = prettyLet (ps :< (x, rhs)) body
prettyLet ps e =
orIndent
(hsep [!(hl Syntax "let*"),
!(bracks . vsep . toList =<< traverse prettyBind ps)])
!(prettySexp e)
private covering
prettyDefine : {opts : LayoutOpts} ->
String -> Either Id (List Id) -> Sexp -> Eff Pretty (Doc opts)
prettyDefine def xs body =
parens $ vappend
(hsep [!(hl Syntax $ text def),
!(either prettyId (prettySexp . L . map V) xs)])
(indent 2 !(prettySexp body))
prettySexp (V x) = prettyId x
prettySexp (L []) = hl Delim "()"
prettySexp (L (x :: xs)) = do
d <- prettySexp x
ds <- traverse prettySexp xs
parens $ ifMultiline
(hsep $ d :: ds)
(hsep [d, vsep ds] <|> vsep (d :: map (indent 2) ds))
prettySexp (Q (V x)) = hl Tag $ "'" <+> prettyId' x
prettySexp (Q x) = pure $ hcat [!(hl Tag "'"), !(prettySexp x)]
prettySexp (N n) = hl Tag $ pshow n
prettySexp (S s) = prettyStrLit s
prettySexp (Lambda xs e) = prettyLambda "lambda" xs e
prettySexp (LambdaC xs e) = prettyLambda "lambda%" xs e
prettySexp (Let x rhs e) = prettyLet [< (x, rhs)] e
prettySexp (Case h as) = do
header' <- prettySexp h
case_ <- caseD
let header = ifMultiline (case_ <++> header')
(case_ `vappend` indent 2 header')
arms <- traverse prettyCase $ toList as
pure $ ifMultiline
(parens $ header <++> hsep arms)
(parens $ vsep $ header :: map (indent 2) arms)
where
prettyCase : (List Sexp, Sexp) -> Eff Pretty (Doc opts)
prettyCase (ps, e) = bracks $
ifMultiline
(hsep [!(parens . hsep =<< traverse prettySexp ps), !(prettySexp e)])
(vsep [!(parens . sep =<< traverse prettySexp ps), !(prettySexp e)])
prettySexp (Define x e) = case e of
LambdaC xs e => prettyDefine "define%" (Right $ x :: xs) e
Lambda xs e => prettyDefine "define" (Right $ x :: xs) e
_ => prettyDefine "define" (Left x) e
prettySexp (Literal sexp) =
pure $ text sexp
export covering
makeRunMain : {opts : LayoutOpts} -> Id -> Eff Pretty (Doc opts)
makeRunMain x = prettySexp $ L ["run-main", V x]

320
lib/Quox/Untyped/Syntax.idr Normal file
View File

@ -0,0 +1,320 @@
module Quox.Untyped.Syntax
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
%default total
%language ElabReflection
public export
data Term : Nat -> Type
public export
data CaseNatSuc : Nat -> Type
data Term where
F : (x : Name) -> Loc -> Term n
B : (i : Var n) -> Loc -> 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) -> Loc -> Term n
Fst : (pair : Term n) -> Loc -> Term n
Snd : (pair : Term n) -> Loc -> Term n
Tag : (tag : String) -> Loc -> Term n
CaseEnum : (tag : Term n) -> (cases : List1 (String, Term n)) -> Loc -> Term n
||| empty match
Absurd : Loc -> Term n
Nat : (val : Nat) -> Loc -> Term n
Succ : (nat : Term n) -> Loc -> Term n
CaseNat : (nat : Term n) ->
(zer : Term n) ->
(suc : CaseNatSuc n) ->
Loc ->
Term n
Str : (str : String) -> Loc -> Term n
Let : (x : BindName) -> (rhs : Term n) -> (body : Term (S n)) -> Loc ->
Term n
Erased : Loc -> Term n
%name Term s, t, u
data CaseNatSuc where
NSRec : (x, ih : BindName) -> Term (2 + n) -> CaseNatSuc n
NSNonrec : (x : BindName) -> Term (S n) -> CaseNatSuc n
%name CaseNatSuc suc
%runElab deriveParam $
map (\ty => PI ty allIndices [Eq, Ord, Show]) ["Term", "CaseNatSuc"]
export
Located (Term n) where
(F _ loc).loc = loc
(B _ loc).loc = loc
(Lam _ _ loc).loc = loc
(App _ _ loc).loc = loc
(Pair _ _ loc).loc = loc
(Fst _ loc).loc = loc
(Snd _ loc).loc = loc
(Tag _ loc).loc = loc
(CaseEnum _ _ loc).loc = loc
(Absurd loc).loc = loc
(Nat _ loc).loc = loc
(Succ _ loc).loc = loc
(CaseNat _ _ _ loc).loc = loc
(Str _ loc).loc = loc
(Let _ _ _ loc).loc = loc
(Erased loc).loc = loc
public export
data Definition =
ErasedDef
| KeptDef Bool (Term 0)
| SchemeDef Bool String
-- bools are presence of #[main] flag
public export
0 Definitions : Type
Definitions = SortedMap Name Definition
export
letD, inD : {opts : LayoutOpts} -> Eff Pretty (Doc opts)
letD = hl Syntax "let"
inD = hl Syntax "in"
export covering
prettyTerm : {opts : LayoutOpts} -> BContext n ->
Term n -> Eff Pretty (Doc opts)
export covering
prettyArg : {opts : LayoutOpts} -> BContext n -> Term n -> Eff Pretty (Doc opts)
prettyArg xs arg = withPrec Arg $ prettyTerm xs arg
export covering
prettyAppHead : {opts : LayoutOpts} -> BContext n ->
Term n -> Eff Pretty (Doc opts)
prettyAppHead xs fun = withPrec App $ prettyTerm xs fun
export
prettyApp' : {opts : LayoutOpts} ->
Doc opts -> SnocList (Doc opts) -> Eff Pretty (Doc opts)
prettyApp' fun args = do
d <- askAt INDENT
let args = toList args
parensIfM App $
hsep (fun :: args)
<|> hsep [fun, vsep args]
<|> vsep (fun :: map (indent d) args)
export covering
prettyApp : {opts : LayoutOpts} -> BContext n ->
Doc opts -> SnocList (Term n) -> Eff Pretty (Doc opts)
prettyApp xs fun args = prettyApp' fun =<< traverse (prettyArg xs) args
public export
record PrettyCaseArm a n where
constructor MkPrettyCaseArm
lhs : a
{len : Nat}
vars : Vect len BindName
rhs : Term (len + n)
export covering
prettyCase : {opts : LayoutOpts} -> BContext n ->
(a -> Eff Pretty (Doc opts)) ->
Term n -> List (PrettyCaseArm a n) ->
Eff Pretty (Doc opts)
prettyCase xs f head arms =
parensIfM Outer =<< do
header <- hsep <$> sequence [caseD, prettyTerm xs head, ofD]
cases <- for arms $ \(MkPrettyCaseArm lhs ys rhs) => do
lhs <- hsep <$> sequence [f lhs, darrowD]
rhs <- withPrec Outer $ prettyTerm (xs <>< ys) rhs
hangDSingle lhs rhs
lb <- hl Delim "{"; sc <- semiD; rb <- hl Delim "}"; d <- askAt INDENT
pure $ ifMultiline
(hsep [header, lb, separateTight sc cases, rb])
(vsep [hsep [header, lb], indent d $ vsep (map (<+> sc) cases), rb])
private
sucPat : {opts : LayoutOpts} -> BindName -> Eff Pretty (Doc opts)
sucPat x = pure $ !succD <++> !(prettyTBind x)
export
splitApp : Term n -> (Term n, SnocList (Term n))
splitApp (App f x _) = mapSnd (:< x) $ splitApp f
splitApp f = (f, [<])
export
splitPair : Term n -> List (Term n)
splitPair (Pair s t _) = s :: splitPair t
splitPair t = [t]
export
splitLam : Telescope' BindName a b -> Term b ->
Exists $ \c => (Telescope' BindName a c, Term c)
splitLam ys (Lam x body _) = splitLam (ys :< x) body
splitLam ys t = Evidence _ (ys, t)
export
splitLet : Telescope (\i => (BindName, Term i)) a b -> Term b ->
Exists $ \c => (Telescope (\i => (BindName, Term i)) a c, Term c)
splitLet ys (Let x rhs body _) = splitLet (ys :< (x, rhs)) body
splitLet ys t = Evidence _ (ys, t)
private covering
prettyLets : {opts : LayoutOpts} ->
BContext a -> Telescope (\i => (BindName, Term i)) a b ->
Eff Pretty (SnocList (Doc opts))
prettyLets xs lets = sequence $ snd $ go lets where
go : forall b. Telescope (\i => (BindName, Term i)) a b ->
(BContext b, SnocList (Eff Pretty (Doc opts)))
go [<] = (xs, [<])
go (lets :< (x, rhs)) =
let (ys, docs) = go lets
doc = do
x <- prettyTBind x
rhs <- withPrec Outer $ prettyTerm ys rhs
hangDSingle (hsep [!letD, x, !cstD]) (hsep [rhs, !inD]) in
(ys :< x, docs :< doc)
private
sucCaseArm : {opts : LayoutOpts} ->
CaseNatSuc n -> Eff Pretty (PrettyCaseArm (Doc opts) n)
sucCaseArm (NSRec x ih s) = pure $
MkPrettyCaseArm (!(sucPat x) <+> !commaD <++> !(prettyTBind ih)) [x, ih] s
sucCaseArm (NSNonrec x s) = pure $
MkPrettyCaseArm !(sucPat x) [x] s
prettyTerm _ (F x _) = prettyFree x
prettyTerm xs (B i _) = prettyTBind $ xs !!! i
prettyTerm xs (Lam x body _) =
parensIfM Outer =<< do
let Evidence n' (ys, body) = splitLam [< x] body
vars <- hsep . toList' <$> traverse prettyTBind ys
body <- withPrec Outer $ prettyTerm (xs . ys) body
hangDSingle (hsep [!lamD, vars, !darrowD]) body
prettyTerm xs (App fun arg _) =
let (fun, args) = splitApp fun in
prettyApp xs !(prettyAppHead xs fun) (args :< arg)
prettyTerm xs (Pair fst snd _) =
parens . separateTight !commaD =<<
traverse (withPrec Outer . prettyTerm xs) (fst :: splitPair 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 _) =
prettyCase xs prettyTag tag $
map (\(t, rhs) => MkPrettyCaseArm t [] rhs) $ toList cases
prettyTerm xs (Absurd _) = hl Syntax "absurd"
prettyTerm xs (Nat n _) = hl Tag $ pshow n
prettyTerm xs (Succ nat _) = prettyApp xs !succD [< nat]
prettyTerm xs (CaseNat nat zer suc _) =
prettyCase xs pure nat [MkPrettyCaseArm !zeroD [] zer, !(sucCaseArm suc)]
prettyTerm xs (Str s _) =
prettyStrLit s
prettyTerm xs (Let x rhs body _) =
parensIfM Outer =<< do
let Evidence n' (lets, body) = splitLet [< (x, rhs)] body
heads <- prettyLets xs lets
body <- withPrec Outer $ prettyTerm (xs . map fst lets) body
let lines = toList $ heads :< body
pure $ ifMultiline (hsep lines) (vsep lines)
prettyTerm _ (Erased _) =
hl Syntax =<< ifUnicode "⌷" "[]"
export covering
prettyDef : {opts : LayoutOpts} -> Name ->
Definition -> Eff Pretty (Doc opts)
prettyDef name ErasedDef =
pure $ hsep [!(prettyFree name), !cstD, !(prettyTerm [<] $ Erased noLoc)]
prettyDef name (KeptDef isMain rhs) = do
name <- prettyFree name {opts}
eq <- cstD
rhs <- withPrec Outer $ prettyTerm [<] rhs
let header = if isMain then text "#[main]" <++> name else name
hangDSingle (header <++> eq) rhs
prettyDef name (SchemeDef isMain str) = do
name <- prettyFree name {opts}
eq <- cstD
let rhs = text $ "scheme:" ++ str
let header = if isMain then text "#[main]" <++> name else name
hangDSingle (header <++> eq) rhs
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
Nat n loc =>
Nat n loc
Succ nat loc =>
Succ (nat // th) loc
CaseNat nat zer suc loc =>
CaseNat (nat // th) (zer // th)
(assert_total substSuc suc th) loc
Str s loc =>
Str s loc
Let x rhs body loc =>
Let x (rhs // th) (assert_total $ body // push 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
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]

14
lib/Quox/Whnf/Coercion.idr
View File

@ -23,7 +23,7 @@ where
parameters {auto _ : CanWhnf Term Interface.isRedexT}
{auto _ : CanWhnf Elim Interface.isRedexE}
{d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n) (sg : SQty)
(defs : Definitions) (ctx : WhnfContext d n) (sg : SQty)
||| reduce a function application `App (Coe ty p q val) s loc`
export covering
piCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) ->
@ -158,6 +158,10 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
TYPE l tyLoc =>
whnf defs ctx sg $ Ann s (TYPE l tyLoc) loc
-- (coe IOState @_ @_ s) ⇝ (s ∷ IOState)
IOState tyLoc =>
whnf defs ctx sg $ Ann s (IOState tyLoc) loc
-- η expand it so that whnf for App can deal with it
--
-- (coe (𝑖 ⇒ π.(x : A) → B) @p @q s)
@ -207,8 +211,12 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
(ty // one q) loc
-- (coe ℕ @_ @_ s) ⇝ (s ∷ ℕ)
Nat tyLoc =>
whnf defs ctx sg $ Ann s (Nat tyLoc) loc
NAT tyLoc =>
whnf defs ctx sg $ Ann s (NAT tyLoc) loc
-- (coe String @_ @_ s) ⇝ (s ∷ String)
STRING tyLoc =>
whnf defs ctx sg $ Ann s (STRING tyLoc) loc
-- η expand
--

40
lib/Quox/Whnf/ComputeElimType.idr
View File

@ -11,35 +11,35 @@ import Quox.Displace
||| - assumes the elim is already typechecked
||| - the return value is not reduced
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)) =>
Eff Whnf (Term d n)
computeElimType :
CanWhnf Term Interface.isRedexT =>
CanWhnf Elim Interface.isRedexE =>
(defs : Definitions) -> WhnfContext d n -> (0 sg : SQty) ->
(e : Elim d n) -> (0 ne : No (isRedexE defs sg e)) =>
Eff Whnf (Term d n)
||| computes a type and then reduces it to whnf
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)) =>
Eff Whnf (Term d n)
computeWhnfElimType0 :
CanWhnf Term Interface.isRedexT =>
CanWhnf Elim Interface.isRedexE =>
(defs : Definitions) -> WhnfContext d n -> (0 sg : SQty) ->
(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 sg e =
case e of
F x u loc => do
let Just def = lookup x defs
| Nothing => throw $ NotInScope loc x
pure $ def.typeAt u
pure $ def.typeWithAt ctx.dimLen ctx.termLen u
B i _ =>
pure $ ctx.tctx !! i
App f s loc =>
case !(computeWhnfElimType0 defs ctx pi f {ne = noOr1 ne}) of
case !(computeWhnfElimType0 defs ctx sg 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 sg 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 sg 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 sg 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 sg e =
computeElimType defs ctx sg e >>= whnf0 defs ctx SZero

109
lib/Quox/Whnf/Interface.idr
View File

@ -13,18 +13,17 @@ import public Control.Eff
public export
Whnf : List (Type -> Type)
Whnf = [NameGen, Except Error]
Whnf = [Except Error, NameGen]
public export
0 RedexTest : TermLike -> Type
RedexTest tm = {d, n : Nat} -> Definitions -> SQty -> tm d n -> Bool
RedexTest tm = {0 d, n : Nat} -> Definitions -> SQty -> tm d n -> Bool
public export
interface CanWhnf (0 tm : TermLike) (0 isRedex : RedexTest tm) | tm
where
whnf : {d, n : Nat} -> (defs : Definitions) ->
(ctx : WhnfContext d n) -> (q : SQty) ->
whnf : (defs : Definitions) -> (ctx : WhnfContext d n) -> (q : SQty) ->
tm d n -> Eff Whnf (Subset (tm d n) (No . isRedex defs q))
-- having isRedex be part of the class header, and needing to be explicitly
-- quantified on every use since idris can't infer its type, is a little ugly.
@ -32,7 +31,7 @@ where
-- cases idris can't tell that `isRedex` and `isRedexT` are the same thing
public export %inline
whnf0 : {d, n : Nat} -> {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
whnf0 : {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex =>
Definitions -> WhnfContext d n -> SQty -> tm d n -> Eff Whnf (tm d n)
whnf0 defs ctx q t = fst <$> whnf defs ctx q t
@ -85,11 +84,18 @@ isTagHead _ = False
||| an expression like `0 ∷ ℕ` or `suc n ∷ ℕ`
public export %inline
isNatHead : Elim {} -> Bool
isNatHead (Ann (Zero {}) (Nat {}) _) = True
isNatHead (Ann (Succ {}) (Nat {}) _) = True
isNatHead (Ann (Nat {}) (NAT {}) _) = True
isNatHead (Ann (Succ {}) (NAT {}) _) = True
isNatHead (Coe {}) = True
isNatHead _ = False
||| a natural constant, with or without an annotation
public export %inline
isNatConst : Term d n -> Bool
isNatConst (Nat {}) = True
isNatConst (E (Ann (Nat {}) _ _)) = True
isNatConst _ = False
||| an expression like `[s] ∷ [π. A]`
public export %inline
isBoxHead : Elim {} -> Bool
@ -112,23 +118,26 @@ isAnn _ = False
||| a syntactic type
public export %inline
isTyCon : Term {} -> Bool
isTyCon (TYPE {}) = True
isTyCon (Pi {}) = True
isTyCon (Lam {}) = False
isTyCon (Sig {}) = True
isTyCon (Pair {}) = False
isTyCon (Enum {}) = True
isTyCon (Tag {}) = False
isTyCon (Eq {}) = True
isTyCon (DLam {}) = False
isTyCon (Nat {}) = True
isTyCon (Zero {}) = False
isTyCon (Succ {}) = False
isTyCon (BOX {}) = True
isTyCon (Box {}) = False
isTyCon (E {}) = False
isTyCon (CloT {}) = False
isTyCon (DCloT {}) = False
isTyCon (TYPE {}) = True
isTyCon (IOState {}) = True
isTyCon (Pi {}) = True
isTyCon (Lam {}) = False
isTyCon (Sig {}) = True
isTyCon (Pair {}) = False
isTyCon (Enum {}) = True
isTyCon (Tag {}) = False
isTyCon (Eq {}) = True
isTyCon (DLam {}) = False
isTyCon (NAT {}) = True
isTyCon (Nat {}) = False
isTyCon (Succ {}) = False
isTyCon (STRING {}) = True
isTyCon (Str {}) = False
isTyCon (BOX {}) = True
isTyCon (Box {}) = False
isTyCon (E {}) = False
isTyCon (CloT {}) = False
isTyCon (DCloT {}) = False
||| a syntactic type, or a neutral
public export %inline
@ -155,24 +164,27 @@ isK _ = False
||| - `val` is a constructor form
public export %inline
canPushCoe : SQty -> (ty, val : Term {}) -> Bool
canPushCoe sg (TYPE {}) _ = True
canPushCoe sg (Pi {}) _ = True
canPushCoe sg (Lam {}) _ = False
canPushCoe sg (Sig {}) (Pair {}) = True
canPushCoe sg (Sig {}) _ = False
canPushCoe sg (Pair {}) _ = False
canPushCoe sg (Enum {}) _ = True
canPushCoe sg (Tag {}) _ = False
canPushCoe sg (Eq {}) _ = True
canPushCoe sg (DLam {}) _ = False
canPushCoe sg (Nat {}) _ = True
canPushCoe sg (Zero {}) _ = False
canPushCoe sg (Succ {}) _ = False
canPushCoe sg (BOX {}) _ = True
canPushCoe sg (Box {}) _ = False
canPushCoe sg (E {}) _ = False
canPushCoe sg (CloT {}) _ = False
canPushCoe sg (DCloT {}) _ = False
canPushCoe sg (TYPE {}) _ = True
canPushCoe sg (IOState {}) _ = True
canPushCoe sg (Pi {}) _ = True
canPushCoe sg (Lam {}) _ = False
canPushCoe sg (Sig {}) (Pair {}) = True
canPushCoe sg (Sig {}) _ = False
canPushCoe sg (Pair {}) _ = False
canPushCoe sg (Enum {}) _ = True
canPushCoe sg (Tag {}) _ = False
canPushCoe sg (Eq {}) _ = True
canPushCoe sg (DLam {}) _ = False
canPushCoe sg (NAT {}) _ = True
canPushCoe sg (Nat {}) _ = False
canPushCoe sg (Succ {}) _ = False
canPushCoe sg (STRING {}) _ = True
canPushCoe sg (Str {}) _ = False
canPushCoe sg (BOX {}) _ = True
canPushCoe sg (Box {}) _ = False
canPushCoe sg (E {}) _ = False
canPushCoe sg (CloT {}) _ = False
canPushCoe sg (DCloT {}) _ = False
mutual
@ -194,8 +206,7 @@ mutual
||| 7. a closure
public export
isRedexE : RedexTest Elim
isRedexE defs sg (F {x, u, _}) {d, n} =
isJust $ lookupElim x u defs {d, n}
isRedexE defs sg (F {x, u, _}) = isJust $ lookupElim0 x u defs
isRedexE _ sg (B {}) = False
isRedexE defs sg (App {fun, _}) =
isRedexE defs sg fun || isLamHead fun
@ -231,9 +242,11 @@ mutual
||| 2. an annotated elimination
||| (the annotation is redundant in a checkable context)
||| 3. a closure
||| 4. `succ` applied to a natural constant
public export
isRedexT : RedexTest Term
isRedexT _ _ (CloT {}) = True
isRedexT _ _ (DCloT {}) = True
isRedexT defs sg (E {e, _}) = isAnn e || isRedexE defs sg e
isRedexT _ _ _ = False
isRedexT _ _ (CloT {}) = True
isRedexT _ _ (DCloT {}) = True
isRedexT defs sg (E {e, _}) = isAnn e || isRedexE defs sg e
isRedexT _ _ (Succ p {}) = isNatConst p
isRedexT _ _ _ = False

52
lib/Quox/Whnf/Main.idr
View File

@ -16,8 +16,8 @@ export covering CanWhnf Elim Interface.isRedexE
covering
CanWhnf Elim Interface.isRedexE where
whnf defs ctx sg (F x u loc) with (lookupElim x u defs) proof eq
_ | Just y = whnf defs ctx sg $ setLoc loc y
whnf defs ctx sg (F x u loc) with (lookupElim0 x u defs) proof eq
_ | Just y = whnf defs ctx sg $ setLoc loc $ injElim ctx y
_ | Nothing = pure $ Element (F x u loc) $ rewrite eq in Ah
whnf _ _ _ (B i loc) = pure $ nred $ B i loc
@ -113,10 +113,15 @@ CanWhnf Elim Interface.isRedexE where
Left _ =>
let ty = sub1 ret nat in
case nat of
Ann (Zero _) (Nat _) _ =>
Ann (Nat 0 _) (NAT _) _ =>
whnf defs ctx sg $ Ann zer ty zer.loc
Ann (Succ n succLoc) (Nat natLoc) _ =>
let nn = Ann n (Nat natLoc) succLoc
Ann (Nat (S n) succLoc) (NAT natLoc) _ =>
let nn = Ann (Nat n succLoc) (NAT natLoc) succLoc
tm = subN suc [< nn, CaseNat pi piIH nn ret zer suc caseLoc]
in
whnf defs ctx sg $ Ann tm ty caseLoc
Ann (Succ n succLoc) (NAT natLoc) _ =>
let nn = Ann n (NAT natLoc) succLoc
tm = subN suc [< nn, CaseNat pi piIH nn ret zer suc caseLoc]
in
whnf defs ctx sg $ Ann tm ty caseLoc
@ -225,20 +230,29 @@ CanWhnf Elim Interface.isRedexE where
covering
CanWhnf Term Interface.isRedexT where
whnf _ _ _ t@(TYPE {}) = pure $ nred t
whnf _ _ _ t@(Pi {}) = pure $ nred t
whnf _ _ _ t@(Lam {}) = pure $ nred t
whnf _ _ _ t@(Sig {}) = pure $ nred t
whnf _ _ _ t@(Pair {}) = pure $ nred t
whnf _ _ _ t@(Enum {}) = pure $ nred t
whnf _ _ _ t@(Tag {}) = pure $ nred t
whnf _ _ _ t@(Eq {}) = pure $ nred t
whnf _ _ _ t@(DLam {}) = pure $ nred t
whnf _ _ _ t@(Nat {}) = pure $ nred t
whnf _ _ _ t@(Zero {}) = pure $ nred t
whnf _ _ _ t@(Succ {}) = pure $ nred t
whnf _ _ _ t@(BOX {}) = pure $ nred t
whnf _ _ _ t@(Box {}) = pure $ nred t
whnf _ _ _ t@(TYPE {}) = pure $ nred t
whnf _ _ _ t@(IOState {}) = pure $ nred t
whnf _ _ _ t@(Pi {}) = pure $ nred t
whnf _ _ _ t@(Lam {}) = pure $ nred t
whnf _ _ _ t@(Sig {}) = pure $ nred t
whnf _ _ _ t@(Pair {}) = pure $ nred t
whnf _ _ _ t@(Enum {}) = pure $ nred t
whnf _ _ _ t@(Tag {}) = pure $ nred t
whnf _ _ _ t@(Eq {}) = pure $ nred t
whnf _ _ _ t@(DLam {}) = pure $ nred t
whnf _ _ _ t@(NAT {}) = pure $ nred t
whnf _ _ _ t@(Nat {}) = pure $ nred t
whnf _ _ _ t@(STRING {}) = pure $ nred t
whnf _ _ _ t@(Str {}) = pure $ nred t
whnf _ _ _ t@(BOX {}) = pure $ nred t
whnf _ _ _ t@(Box {}) = pure $ nred t
whnf _ _ _ (Succ p loc) =
case nchoose $ isNatConst p of
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) $ ?cc
-- s ∷ A ⇝ s (in term context)
whnf defs ctx sg (E e) = do

13
lib/Quox/Whnf/TypeCase.idr
View File

@ -30,7 +30,7 @@ tycaseRhsDef0 def k arms = fromMaybe def $ tycaseRhs0 k arms
parameters {auto _ : CanWhnf Term Interface.isRedexT}
{auto _ : CanWhnf Elim Interface.isRedexE}
{d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
(defs : Definitions) (ctx : WhnfContext d n)
||| for π.(x : A) → B, returns (A, B);
||| for an elim returns a pair of type-cases that will reduce to that;
||| for other intro forms error
@ -99,7 +99,6 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
pure (a0, a1, a, l, r)
tycaseEq t = throw $ ExpectedEq t.loc ctx.names t
||| reduce a type-case applied to a type constructor
|||
||| `reduceTypeCase A i Q arms def _` reduces an expression
@ -114,6 +113,10 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
TYPE {} =>
whnf defs ctx SZero $ Ann (tycaseRhsDef0 def KTYPE arms) ret loc
-- (type-case IOState ∷ _ return Q of { IOState ⇒ s; ⋯ }) ⇝ s ∷ Q
IOState {} =>
whnf defs ctx SZero $ Ann (tycaseRhsDef0 def KIOState arms) ret loc
-- (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, _} =>
@ -153,9 +156,13 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
ret loc
-- (type-case ℕ ∷ _ return Q of { ℕ ⇒ s; ⋯ }) ⇝ s ∷ Q
Nat {} =>
NAT {} =>
whnf defs ctx SZero $ Ann (tycaseRhsDef0 def KNat arms) ret loc
-- (type-case String ∷ _ return Q of { String ⇒ s; ⋯ }) ⇝ s ∷ Q
STRING {} =>
whnf defs ctx SZero $ Ann (tycaseRhsDef0 def KString arms) ret loc
-- (type-case [π.A] ∷ ★ᵢ return Q of { [a] ⇒ s; ⋯ }) ⇝ s[(A ∷ ★ᵢ)/a] ∷ Q
BOX {ty = a, loc = boxLoc, _} =>
whnf defs ctx SZero $ Ann

26
lib/Text/PrettyPrint/Bernardy/Core/Decorate.idr
View File

@ -1,29 +1,37 @@
-- this module has to be called this because a module A.B's private elements are
-- still visible to A.B.C, even if they're in different packages. which i don't
-- think is a good idea but i also don't want to fork prettier over it
--
-- also i adapted this code from stefan höck's prettier-ansi package
-- (https://github.com/idris-community/idris2-ansi)
module Text.PrettyPrint.Bernardy.Core.Decorate
import public Text.PrettyPrint.Bernardy.Core
import Data.DPair
import Data.String
import Derive.Prelude
%language ElabReflection
public export
record Highlight where
constructor MkHighlight
before, after : String
%name Highlight h
%runElab derive "Highlight" [Eq]
export
emptyHL : Highlight -> Bool
emptyHL (MkHighlight before after) = before == "" && after == ""
emptyHL : Highlight
emptyHL = MkHighlight "" ""
-- taken from prettier-ansi
-- lifted from prettier-ansi
private
decorateImpl : Highlight ->
(ss : SnocList String) -> (0 _ : NonEmptySnoc ss) =>
Subset (SnocList String) NonEmptySnoc
decorateImpl h [<x] = Element [< h.before ++ x ++ h.after] %search
decorateImpl h [< x] = Element [< h.before ++ x ++ h.after] %search
decorateImpl h (sx :< x) = Element (go [] sx :< (x ++ h.after)) %search
where
go : List String -> SnocList String -> SnocList String
@ -35,17 +43,19 @@ decorateImpl h (sx :< x) = Element (go [] sx :< (x ++ h.after)) %search
||| changing its stats like width or height.
export
decorateLayout : Highlight -> Layout -> Layout
decorateLayout h l@(MkLayout content stats) =
if emptyHL h then l else
decorateLayout h (MkLayout content stats) =
layout (decorateImpl h content) stats
||| Decorate a `Doc` with the given highlighting *without*
||| changing its stats like width or height.
export
decorate : {opts : _} -> Highlight -> Doc opts -> Doc opts
decorate h doc = doc >>= \l => pure (decorateLayout h l)
decorate : {opts : LayoutOpts} -> Highlight -> Doc opts -> Doc opts
decorate h doc =
if h == emptyHL then doc else doc >>= pure . decorateLayout h
-- this function has nothing to do with highlighting but it's here because it
-- _also_ needs access to the private stuff
||| render a doc with no line breaks at all
export
renderInfinite : Doc opts -> String

10
lib/quox-lib.ipkg
View File

@ -5,7 +5,9 @@ authors = "rhiannon morris"
sourceloc = "https://git.rhiannon.website/rhi/quox"
license = "acsl"
depends = base, contrib, elab-util, sop, snocvect, eff, prettier
depends =
base, contrib, elab-util, sop, snocvect, eff, prettier,
pretty-show, parser-show
modules =
Text.PrettyPrint.Bernardy.Core.Decorate,
@ -14,6 +16,7 @@ modules =
Quox.CharExtra,
Quox.NatExtra,
Quox.EffExtra,
Quox.PrettyValExtra,
Quox.Decidable,
Quox.No,
Quox.Loc,
@ -56,4 +59,7 @@ modules =
Quox.Parser.LoadFile,
Quox.Parser.FromParser,
Quox.Parser.FromParser.Error,
Quox.Parser
Quox.Parser,
Quox.Untyped.Syntax,
Quox.Untyped.Erase,
Quox.Untyped.Scheme

2
pack.toml
View File

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

10
tests/AstExtra.idr
View File

@ -31,3 +31,13 @@ ctx tel = let (ns, ts) = unzip tel in
MkTyContext new [<] ts ns anys
ctx01 tel = let (ns, ts) = unzip tel in
MkTyContext ZeroIsOne [<] ts ns anys
export
mkDef : GQty -> Term 0 0 -> Term 0 0 -> Definition
mkDef q ty tm = Definition.mkDef q ty tm Nothing False noLoc
%hide Definition.mkDef
export
mkPostulate : GQty -> Term 0 0 -> Definition
mkPostulate q ty = Definition.mkPostulate q ty Nothing False noLoc
%hide Definition.mkPostulate

91
tests/Tests/Equal.idr
View File

@ -2,25 +2,24 @@ module Tests.Equal
import Quox.Equal
import Quox.Typechecker
import Quox.ST
import Control.Monad.ST
import public TypingImpls
import TAP
import Quox.EffExtra
import AstExtra
defGlobals : Definitions
defGlobals = fromList
[("A", ^mkPostulate GZero (^TYPE 0)),
("B", ^mkPostulate GZero (^TYPE 0)),
("a", ^mkPostulate GAny (^FT "A" 0)),
("a'", ^mkPostulate GAny (^FT "A" 0)),
("b", ^mkPostulate GAny (^FT "B" 0)),
("f", ^mkPostulate GAny (^Arr One (^FT "A" 0) (^FT "A" 0))),
("id", ^mkDef GAny (^Arr One (^FT "A" 0) (^FT "A" 0)) (^LamY "x" (^BVT 0))),
("eq-AB", ^mkPostulate GZero (^Eq0 (^TYPE 0) (^FT "A" 0) (^FT "B" 0))),
("two", ^mkDef GAny (^Nat) (^Succ (^Succ (^Zero))))]
[("A", mkPostulate GZero (^TYPE 0)),
("B", mkPostulate GZero (^TYPE 0)),
("a", mkPostulate GAny (^FT "A" 0)),
("a'", mkPostulate GAny (^FT "A" 0)),
("b", mkPostulate GAny (^FT "B" 0)),
("f", mkPostulate GAny (^Arr One (^FT "A" 0) (^FT "A" 0))),
("id", mkDef GAny (^Arr One (^FT "A" 0) (^FT "A" 0)) (^LamY "x" (^BVT 0))),
("eq-AB", mkPostulate GZero (^Eq0 (^TYPE 0) (^FT "A" 0) (^FT "B" 0))),
("two", mkDef GAny (^NAT) (^Succ (^Succ (^Zero))))]
parameters (label : String) (act : Eff Equal ())
{default defGlobals globals : Definitions}
@ -156,7 +155,7 @@ tests = "equality & subtyping" :- [
let tm = ^Eq0 (^TYPE 1) (^TYPE 0) (^TYPE 0) in
equalT empty (^TYPE 2) tm tm,
testEq "A ≔ ★₁ ⊢ (★₀ ≡ ★₀ : ★₁) = (★₀ ≡ ★₀ : A)"
{globals = fromList [("A", ^mkDef GZero (^TYPE 2) (^TYPE 1))]} $
{globals = fromList [("A", mkDef GZero (^TYPE 2) (^TYPE 1))]} $
equalT empty (^TYPE 2)
(^Eq0 (^TYPE 1) (^TYPE 0) (^TYPE 0))
(^Eq0 (^FT "A" 0) (^TYPE 0) (^TYPE 0)),
@ -176,7 +175,7 @@ tests = "equality & subtyping" :- [
testEq "p : (a ≡ a' : A), q : (a ≡ a' : A) ∥ ⊢ p = q (free)"
{globals =
let def = ^mkPostulate GZero
let def = mkPostulate GZero
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0))
in defGlobals `mergeLeft` fromList [("p", def), ("q", def)]} $
equalE empty (^F "p" 0) (^F "q" 0),
@ -195,32 +194,32 @@ tests = "equality & subtyping" :- [
testEq "E ≔ a ≡ a' : A, EE ≔ E ∥ x : EE, y : EE ⊢ x = y"
{globals = defGlobals `mergeLeft` fromList
[("E", ^mkDef GZero (^TYPE 0)
[("E", mkDef GZero (^TYPE 0)
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0))),
("EE", ^mkDef GZero (^TYPE 0) (^FT "E" 0))]} $
("EE", mkDef GZero (^TYPE 0) (^FT "E" 0))]} $
equalE
(extendTyN [< (Any, "x", ^FT "EE" 0), (Any, "y", ^FT "EE" 0)] empty)
(^BV 0) (^BV 1),
testEq "E ≔ a ≡ a' : A, EE ≔ E ∥ x : EE, y : E ⊢ x = y"
{globals = defGlobals `mergeLeft` fromList
[("E", ^mkDef GZero (^TYPE 0)
[("E", mkDef GZero (^TYPE 0)
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0))),
("EE", ^mkDef GZero (^TYPE 0) (^FT "E" 0))]} $
("EE", mkDef GZero (^TYPE 0) (^FT "E" 0))]} $
equalE
(extendTyN [< (Any, "x", ^FT "EE" 0), (Any, "y", ^FT "E" 0)] empty)
(^BV 0) (^BV 1),
testEq "E ≔ a ≡ a' : A ∥ x : E, y : E ⊢ x = y"
{globals = defGlobals `mergeLeft` fromList
[("E", ^mkDef GZero (^TYPE 0)
[("E", mkDef GZero (^TYPE 0)
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0)))]} $
equalE (extendTyN [< (Any, "x", ^FT "E" 0), (Any, "y", ^FT "E" 0)] empty)
(^BV 0) (^BV 1),
testEq "E ≔ a ≡ a' : A ∥ x : (E×E), y : (E×E) ⊢ x = y"
{globals = defGlobals `mergeLeft` fromList
[("E", ^mkDef GZero (^TYPE 0)
[("E", mkDef GZero (^TYPE 0)
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0)))]} $
let ty : forall n. Term 0 n := ^Sig (^FT "E" 0) (SN $ ^FT "E" 0) in
equalE (extendTyN [< (Any, "x", ty), (Any, "y", ty)] empty)
@ -228,9 +227,9 @@ tests = "equality & subtyping" :- [
testEq "E ≔ a ≡ a' : A, W ≔ E × E ∥ x : W, y : E×E ⊢ x = y"
{globals = defGlobals `mergeLeft` fromList
[("E", ^mkDef GZero (^TYPE 0)
[("E", mkDef GZero (^TYPE 0)
(^Eq0 (^FT "A" 0) (^FT "a" 0) (^FT "a'" 0))),
("W", ^mkDef GZero (^TYPE 0) (^And (^FT "E" 0) (^FT "E" 0)))]} $
("W", mkDef GZero (^TYPE 0) (^And (^FT "E" 0) (^FT "E" 0)))]} $
equalE
(extendTyN [< (Any, "x", ^FT "W" 0),
(Any, "y", ^And (^FT "E" 0) (^FT "E" 0))] empty)
@ -280,11 +279,11 @@ tests = "equality & subtyping" :- [
"free var" :-
let au_bu = fromList
[("A", ^mkDef GAny (^TYPE 1) (^TYPE 0)),
("B", ^mkDef GAny (^TYPE 1) (^TYPE 0))]
[("A", mkDef GAny (^TYPE 1) (^TYPE 0)),
("B", mkDef GAny (^TYPE 1) (^TYPE 0))]
au_ba = fromList
[("A", ^mkDef GAny (^TYPE 1) (^TYPE 0)),
("B", ^mkDef GAny (^TYPE 1) (^FT "A" 0))]
[("A", mkDef GAny (^TYPE 1) (^TYPE 0)),
("B", mkDef GAny (^TYPE 1) (^FT "A" 0))]
in [
testEq "A = A" $
equalE empty (^F "A" 0) (^F "A" 0),
@ -305,13 +304,13 @@ tests = "equality & subtyping" :- [
testNeq "A ≮: B" $
subE empty (^F "A" 0) (^F "B" 0),
testEq "A : ★₃ ≔ ★₀, B : ★₃ ≔ ★₂ ⊢ A <: B"
{globals = fromList [("A", ^mkDef GAny (^TYPE 3) (^TYPE 0)),
("B", ^mkDef GAny (^TYPE 3) (^TYPE 2))]} $
{globals = fromList [("A", mkDef GAny (^TYPE 3) (^TYPE 0)),
("B", mkDef GAny (^TYPE 3) (^TYPE 2))]} $
subE empty (^F "A" 0) (^F "B" 0),
note "(A and B in different universes)",
testEq "A : ★₁ ≔ ★₀, B : ★₃ ≔ ★₂ ⊢ A <: B"
{globals = fromList [("A", ^mkDef GAny (^TYPE 1) (^TYPE 0)),
("B", ^mkDef GAny (^TYPE 3) (^TYPE 2))]} $
{globals = fromList [("A", mkDef GAny (^TYPE 1) (^TYPE 0)),
("B", mkDef GAny (^TYPE 3) (^TYPE 2))]} $
subE empty (^F "A" 0) (^F "B" 0),
testEq "0=1 ⊢ A <: B" $
subE empty01 (^F "A" 0) (^F "B" 0)
@ -448,30 +447,30 @@ tests = "equality & subtyping" :- [
],
"natural type" :- [
testEq "ℕ = ℕ" $ equalTy empty (^Nat) (^Nat),
testEq "ℕ = ℕ : ★₀" $ equalT empty (^TYPE 0) (^Nat) (^Nat),
testEq "ℕ = ℕ : ★₆₉" $ equalT empty (^TYPE 69) (^Nat) (^Nat),
testNeq "ℕ ≠ {}" $ equalTy empty (^Nat) (^enum []),
testEq "0=1 ⊢ ℕ = {}" $ equalTy empty01 (^Nat) (^enum [])
testEq "ℕ = ℕ" $ equalTy empty (^NAT) (^NAT),
testEq "ℕ = ℕ : ★₀" $ equalT empty (^TYPE 0) (^NAT) (^NAT),
testEq "ℕ = ℕ : ★₆₉" $ equalT empty (^TYPE 69) (^NAT) (^NAT),
testNeq "ℕ ≠ {}" $ equalTy empty (^NAT) (^enum []),
testEq "0=1 ⊢ ℕ = {}" $ equalTy empty01 (^NAT) (^enum [])
],
"natural numbers" :- [
testEq "0 = 0" $ equalT empty (^Nat) (^Zero) (^Zero),
testEq "0 = 0" $ equalT empty (^NAT) (^Zero) (^Zero),
testEq "succ two = succ two" $
equalT empty (^Nat) (^Succ (^FT "two" 0)) (^Succ (^FT "two" 0)),
equalT empty (^NAT) (^Succ (^FT "two" 0)) (^Succ (^FT "two" 0)),
testNeq "succ two ≠ two" $
equalT empty (^Nat) (^Succ (^FT "two" 0)) (^FT "two" 0),
equalT empty (^NAT) (^Succ (^FT "two" 0)) (^FT "two" 0),
testNeq "0 ≠ 1" $
equalT empty (^Nat) (^Zero) (^Succ (^Zero)),
equalT empty (^NAT) (^Zero) (^Succ (^Zero)),
testEq "0=1 ⊢ 0 = 1" $
equalT empty01 (^Nat) (^Zero) (^Succ (^Zero))
equalT empty01 (^NAT) (^Zero) (^Succ (^Zero))
],
"natural elim" :- [
testEq "caseω 0 return {a,b} of {zero ⇒ 'a; succ _ ⇒ 'b} = 'a" $
equalT empty
(^enum ["a", "b"])
(E $ ^CaseNat Any Zero (^Ann (^Zero) (^Nat))
(E $ ^CaseNat Any Zero (^Ann (^Zero) (^NAT))
(SN $ ^enum ["a", "b"])
(^Tag "a")
(SN $ ^Tag "b"))
@ -479,19 +478,19 @@ tests = "equality & subtyping" :- [
testEq "caseω 1 return {a,b} of {zero ⇒ 'a; succ _ ⇒ 'b} = 'b" $
equalT empty
(^enum ["a", "b"])
(E $ ^CaseNat Any Zero (^Ann (^Succ (^Zero)) (^Nat))
(E $ ^CaseNat Any Zero (^Ann (^Succ (^Zero)) (^NAT))
(SN $ ^enum ["a", "b"])
(^Tag "a")
(SN $ ^Tag "b"))
(^Tag "b"),
testEq "caseω 4 return ℕ of {0 ⇒ 0; succ n ⇒ n} = 3" $
equalT empty
(^Nat)
(E $ ^CaseNat Any Zero (^Ann (^makeNat 4) (^Nat))
(SN $ ^Nat)
(^NAT)
(E $ ^CaseNat Any Zero (^Ann (^Nat 4) (^NAT))
(SN $ ^NAT)
(^Zero)
(SY [< "n", ^BN Unused] $ ^BVT 1))
(^makeNat 3)
(^Nat 3)
],
todo "pair types",
@ -514,7 +513,7 @@ tests = "equality & subtyping" :- [
(^Pair (^Tag "b") (^Tag "a")),
testEq "0=1 ⊢ ('a, 'b) = ('b, 'a) : ℕ" $
equalT empty01
(^Nat)
(^NAT)
(^Pair (^Tag "a") (^Tag "b"))
(^Pair (^Tag "b") (^Tag "a"))
],

2
tests/Tests/FromPTerm.idr
View File

@ -85,7 +85,7 @@ tests = "PTerm → Term" :- [
],
"terms" :-
let defs = fromList [("f", mkDef GAny (Nat noLoc) (Zero noLoc) noLoc)]
let defs = fromList [("f", mkDef GAny (^NAT) (^Zero))]
-- doesn't have to be well typed yet, just well scoped
fromPTerm = runFromParser {defs} .
fromPTermWith [< "𝑖", "𝑗"] [< "A", "x", "y", "z"]

106
tests/Tests/Parser.idr
View File

@ -64,8 +64,8 @@ tests = "parser" :- [
"names" :- [
parsesAs (const qname) "x"
(MakePName [<] "x"),
parsesAs (const qname) "Data.String.length"
(MakePName [< "Data", "String"] "length"),
parsesAs (const qname) "Data.List.length"
(MakePName [< "Data", "List"] "length"),
parseFails (const qname) "_"
],
@ -282,29 +282,24 @@ tests = "parser" :- [
],
"naturals" :- [
parseMatch term "ℕ" `(Nat _),
parseMatch term "Nat" `(Nat _),
parseMatch term "zero" `(Zero _),
parseMatch term "ℕ" `(NAT _),
parseMatch term "Nat" `(NAT _),
parseMatch term "zero" `(Nat 0 _),
parseMatch term "succ n" `(Succ (V "n" {}) _),
parseMatch term "3"
`(Succ (Succ (Succ (Zero _) _) _) _),
parseMatch term "succ (succ 1)"
`(Succ (Succ (Succ (Zero _) _) _) _),
parseMatch term "3" `(Nat 3 _),
parseMatch term "succ (succ 1)" `(Succ (Succ (Nat 1 _) _) _),
parseFails term "succ succ 5",
parseFails term "succ"
],
"box" :- [
parseMatch term "[1.ℕ]"
`(BOX (PQ One _) (Nat _) _),
`(BOX (PQ One _) (NAT _) _),
parseMatch term "[ω. ℕ × ℕ]"
`(BOX (PQ Any _) (Sig (Unused _) (Nat _) (Nat _) _) _),
parseMatch term "[a]"
`(Box (V "a" {}) _),
parseMatch term "[0]"
`(Box (Zero _) _),
parseMatch term "[1]"
`(Box (Succ (Zero _) _) _)
`(BOX (PQ Any _) (Sig (Unused _) (NAT _) (NAT _) _) _),
parseMatch term "[a]" `(Box (V "a" {}) _),
parseMatch term "[0]" `(Box (Nat 0 _) _),
parseMatch term "[1]" `(Box (Nat 1 _) _)
],
"coe" :- [
@ -388,14 +383,14 @@ tests = "parser" :- [
`(Case (PQ Any _) (V "n" {}) (Unused _, V "A" {})
(CaseNat (V "a" {}) (PV "n'" _, PQ Zero _, Unused _, V "b" {}) _) _),
parseMatch term "caseω n return ℕ of { succ _, 1.ih ⇒ ih; zero ⇒ 0; }"
`(Case (PQ Any _) (V "n" {}) (Unused _, Nat _)
(CaseNat (Zero _) (Unused _, PQ One _, PV "ih" _, V "ih" {}) _) _),
`(Case (PQ Any _) (V "n" {}) (Unused _, NAT _)
(CaseNat (Nat 0 _) (Unused _, PQ One _, PV "ih" _, V "ih" {}) _) _),
parseMatch term "caseω n return ℕ of { succ _, ω.ih ⇒ ih; zero ⇒ 0; }"
`(Case (PQ Any _) (V "n" {}) (Unused _, Nat _)
(CaseNat (Zero _) (Unused _, PQ Any _, PV "ih" _, V "ih" {}) _) _),
`(Case (PQ Any _) (V "n" {}) (Unused _, NAT _)
(CaseNat (Nat 0 _) (Unused _, PQ Any _, PV "ih" _, V "ih" {}) _) _),
parseMatch term "caseω n return ℕ of { succ _, ih ⇒ ih; zero ⇒ 0; }"
`(Case (PQ Any _) (V "n" {}) (Unused _, Nat _)
(CaseNat (Zero _) (Unused _, PQ One _, PV "ih" _, V "ih" {}) _) _),
`(Case (PQ Any _) (V "n" {}) (Unused _, NAT _)
(CaseNat (Nat 0 _) (Unused _, PQ One _, PV "ih" _, V "ih" {}) _) _),
parseFails term "caseω n return A of { zero ⇒ a }",
parseFails term "caseω n return ℕ of { succ ⇒ 5 }"
],
@ -403,36 +398,53 @@ tests = "parser" :- [
"definitions" :- [
parseMatch definition "defω x : {a} × {b} = ('a, 'b);"
`(MkPDef (PQ Any _) "x"
(Just (Sig (Unused _) (Enum ["a"] _) (Enum ["b"] _) _))
(Pair (Tag "a" _) (Tag "b" _) _) _),
(PConcrete
(Just (Sig (Unused _) (Enum ["a"] _) (Enum ["b"] _) _))
(Pair (Tag "a" _) (Tag "b" _) _)) _),
parseMatch definition "def# x : {a} ** {b} = ('a, 'b)"
`(MkPDef (PQ Any _) "x"
(Just (Sig (Unused _) (Enum ["a"] _) (Enum ["b"] _) _))
(Pair (Tag "a" _) (Tag "b" _) _) _),
(PConcrete
(Just (Sig (Unused _) (Enum ["a"] _) (Enum ["b"] _) _))
(Pair (Tag "a" _) (Tag "b" _) _)) _),
parseMatch definition "def ω.x : {a} × {b} = ('a, 'b)"
`(MkPDef (PQ Any _) "x"
(Just (Sig (Unused _) (Enum ["a"] _) (Enum ["b"] _) _))
(Pair (Tag "a" _) (Tag "b" _) _) _),
(PConcrete
(Just (Sig (Unused _) (Enum ["a"] _) (Enum ["b"] _) _))
(Pair (Tag "a" _) (Tag "b" _) _)) _),
parseMatch definition "def x : {a} × {b} = ('a, 'b)"
`(MkPDef (PQ Any _) "x"
(Just (Sig (Unused _) (Enum ["a"] _) (Enum ["b"] _) _))
(Pair (Tag "a" _) (Tag "b" _) _) _),
(PConcrete
(Just (Sig (Unused _) (Enum ["a"] _) (Enum ["b"] _) _))
(Pair (Tag "a" _) (Tag "b" _) _)) _),
parseMatch definition "def0 A : ★⁰ = {a, b, c}"
`(MkPDef (PQ Zero _) "A" (Just $ TYPE 0 _)
(Enum ["a", "b", "c"] _) _)
`(MkPDef (PQ Zero _) "A"
(PConcrete (Just $ TYPE 0 _) (Enum ["a", "b", "c"] _)) _),
parseMatch definition "postulate yeah : ℕ"
`(MkPDef (PQ Any _) "yeah" (PPostulate (NAT _)) _),
parseMatch definition "postulateω yeah : ℕ"
`(MkPDef (PQ Any _) "yeah" (PPostulate (NAT _)) _),
parseMatch definition "postulate0 FileHandle : ★"
`(MkPDef (PQ Zero _) "FileHandle" (PPostulate (TYPE 0 _)) _),
parseFails definition "postulate not-a-postulate : ℕ = 69",
parseFails definition "postulate not-a-postulate = 69",
parseFails definition "def not-a-def : ℕ"
],
"top level" :- [
parseMatch input "def0 A : ★⁰ = {}; def0 B : ★¹ = A;"
`([PD $ MkPDecl []
(PDef $ MkPDef (PQ Zero _) "A" (Just $ TYPE 0 _) (Enum [] _) _) _,
(PDef $ MkPDef (PQ Zero _) "A"
(PConcrete (Just $ TYPE 0 _) (Enum [] _)) _) _,
PD $ MkPDecl []
(PDef $ MkPDef (PQ Zero _) "B" (Just $ TYPE 1 _) (V "A" {}) _) _]),
(PDef $ MkPDef (PQ Zero _) "B"
(PConcrete (Just $ TYPE 1 _) (V "A" {})) _) _]),
parseMatch input "def0 A : ★⁰ = {} def0 B : ★¹ = A" $
`([PD $ MkPDecl []
(PDef $ MkPDef (PQ Zero _) "A" (Just $ TYPE 0 _) (Enum [] _) _) _,
(PDef $ MkPDef (PQ Zero _) "A"
(PConcrete (Just $ TYPE 0 _) (Enum [] _)) _) _,
PD $ MkPDecl []
(PDef $ MkPDef (PQ Zero _) "B" (Just $ TYPE 1 _) (V "A" {}) _) _]),
(PDef $ MkPDef (PQ Zero _) "B"
(PConcrete (Just $ TYPE 1 _) (V "A" {})) _) _]),
note "empty input",
parsesAs input "" [],
parseFails input ";;;;;;;;;;;;;;;;;;;;;;;;;;",
@ -449,21 +461,23 @@ tests = "parser" :- [
`([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"
(PDef $ MkPDef (PQ Any _) "x"
(PConcrete Nothing
(Ann (Tag "t" _) (Enum ["t"] _) _)) _) _] _) _)]),
parseMatch input "namespace a {def x : {t} = 't} def y = a.x"
`([PD (MkPDecl []
(PNs $ MkPNamespace [< "a"]
[MkPDecl []
(PDef $ MkPDef (PQ Any _) "x" Nothing
(Ann (Tag "t" _) (Enum ["t"] _) _) _) _] _) _),
(PDef $ MkPDef (PQ Any _) "x"
(PConcrete (Just (Enum ["t"] _))
(Tag "t" _)) _) _] _) _),
PD (MkPDecl []
(PDef $ MkPDef (PQ Any _) "y" Nothing
(V (MakePName [< "a"] "x") Nothing _) _) _)]),
(PDef $ MkPDef (PQ Any _) "y"
(PConcrete Nothing (V (MakePName [< "a"] "x") Nothing _)) _) _)]),
parseMatch input #" load "a.quox"; def b = a.b "#
`([PLoad "a.quox" _,
PD (MkPDecl []
(PDef $ MkPDef (PQ Any _) "b" Nothing
(V (MakePName [< "a"] "b") Nothing _) _) _)])
(PDef $ MkPDef (PQ Any _) "b"
(PConcrete Nothing (V (MakePName [< "a"] "b") Nothing _)) _) _)])
]
]

2
tests/Tests/PrettyTerm.idr
View File

@ -210,7 +210,7 @@ tests = "pretty printing terms" :- [
"type-case" :- [
testPrettyE [<] [<]
{label = "type-case ℕ ∷ ★⁰ return ★⁰ of { ⋯ }"}
(^TypeCase (^Ann (^Nat) (^TYPE 0)) (^TYPE 0) empty (^Nat))
(^TypeCase (^Ann (^NAT) (^TYPE 0)) (^TYPE 0) empty (^NAT))
"type-case ℕ ∷ ★⁰ return ★⁰ of { _ ⇒ ℕ }"
"type-case Nat :: Type 0 return Type 0 of { _ => Nat }"
],

22
tests/Tests/Reduce.idr
View File

@ -14,8 +14,8 @@ import Control.Eff
runWhnf : Eff Whnf a -> Either Error a
runWhnf act = runSTErr $ do
runEff act [handleStateSTRef !(liftST $ newSTRef 0),
handleExcept (\e => stLeft e)]
runEff act [handleExcept (\e => stLeft e),
handleStateSTRef !(liftST $ newSTRef 0)]
parameters {0 isRedex : RedexTest tm} {auto _ : CanWhnf tm isRedex} {d, n : Nat}
{auto _ : (Eq (tm d n), Show (tm d n))}
@ -32,7 +32,7 @@ parameters {0 isRedex : RedexTest tm} {auto _ : CanWhnf tm isRedex} {d, n : Nat}
testNoStep label ctx e = testWhnf label ctx e e
private
ctx : Context (\n => (BindName, Term 0 n)) n -> WhnfContext 0 n
ctx : {n : Nat} -> Context (\n => (BindName, Term 0 n)) n -> WhnfContext 0 n
ctx xs = let (ns, ts) = unzip xs in MkWhnfContext [<] ns ts
@ -52,7 +52,7 @@ tests = "whnf" :- [
],
"neutrals" :- [
testNoStep "x" (ctx [< ("A", ^Nat)]) $ ^BV 0,
testNoStep "x" (ctx [< ("A", ^NAT)]) $ ^BV 0,
testNoStep "a" empty $ ^F "a" 0,
testNoStep "f a" empty $ ^App (^F "f" 0) (^FT "a" 0),
testNoStep "★₀ ∷ ★₁" empty $ ^Ann (^TYPE 0) (^TYPE 1)
@ -73,21 +73,21 @@ tests = "whnf" :- [
"definitions" :- [
testWhnf "a (transparent)" empty
{defs = fromList [("a", ^mkDef GZero (^TYPE 1) (^TYPE 0))]}
{defs = fromList [("a", ^mkDef GZero (^TYPE 1) (^TYPE 0) Nothing False)]}
(^F "a" 0) (^Ann (^TYPE 0) (^TYPE 1)),
testNoStep "a (opaque)" empty
{defs = fromList [("a", ^mkPostulate GZero (^TYPE 1))]}
{defs = fromList [("a", ^mkPostulate GZero (^TYPE 1) Nothing False)]}
(^F "a" 0)
],
"elim closure" :- [
testWhnf "x{}" (ctx [< ("x", ^Nat)])
testWhnf "x{}" (ctx [< ("x", ^NAT)])
(CloE (Sub (^BV 0) id))
(^BV 0),
testWhnf "x{a/x}" empty
(CloE (Sub (^BV 0) (^F "a" 0 ::: id)))
(^F "a" 0),
testWhnf "x{a/y}" (ctx [< ("x", ^Nat)])
testWhnf "x{a/y}" (ctx [< ("x", ^NAT)])
(CloE (Sub (^BV 0) (^BV 0 ::: ^F "a" 0 ::: id)))
(^BV 0),
testWhnf "x{(y{a/y})/x}" empty
@ -96,7 +96,7 @@ tests = "whnf" :- [
testWhnf "(x y){f/x,a/y}" empty
(CloE (Sub (^App (^BV 0) (^BVT 1)) (^F "f" 0 ::: ^F "a" 0 ::: id)))
(^App (^F "f" 0) (^FT "a" 0)),
testWhnf "(y ∷ x){A/x}" (ctx [< ("x", ^Nat)])
testWhnf "(y ∷ x){A/x}" (ctx [< ("x", ^NAT)])
(CloE (Sub (^Ann (^BVT 1) (^BVT 0)) (^F "A" 0 ::: id)))
(^BV 0),
testWhnf "(y ∷ x){A/x,a/y}" empty
@ -129,10 +129,10 @@ tests = "whnf" :- [
^App (^F "f" 0)
(E $ ^App (^Ann (^LamY "x" (^BVT 0)) (^Arr One (^FT "A" 0) (^FT "A" 0)))
(^FT "a" 0)),
testNoStep "λx. (y x){x/x,a/y}" (ctx [< ("y", ^Nat)]) $
testNoStep "λx. (y x){x/x,a/y}" (ctx [< ("y", ^NAT)]) $
^LamY "x" (CloT $ Sub (E $ ^App (^BV 1) (^BVT 0))
(^BV 0 ::: ^F "a" 0 ::: id)),
testNoStep "f (y x){x/x,a/y}" (ctx [< ("y", ^Nat)]) $
testNoStep "f (y x){x/x,a/y}" (ctx [< ("y", ^NAT)]) $
^App (^F "f" 0)
(CloT (Sub (E $ ^App (^BV 1) (^BVT 0))
(^BV 0 ::: ^F "a" 0 ::: id)))

42
tests/Tests/Typechecker.idr
View File

@ -2,7 +2,7 @@ module Tests.Typechecker
import Quox.Syntax
import Quox.Typechecker as Lib
import Quox.ST
import Control.Monad.ST
import public TypingImpls
import TAP
import Quox.EffExtra
@ -79,7 +79,7 @@ sndDef =
(SY [< "x", "y"] $ ^BVT 0))))
nat : Term d n
nat = ^Nat
nat = ^NAT
apps : Elim d n -> List (Term d n) -> Elim d n
apps = foldl (\f, s => ^App f s)
@ -87,28 +87,28 @@ apps = foldl (\f, s => ^App f s)
defGlobals : Definitions
defGlobals = fromList
[("A", ^mkPostulate GZero (^TYPE 0)),
("B", ^mkPostulate GZero (^TYPE 0)),
("C", ^mkPostulate GZero (^TYPE 1)),
("D", ^mkPostulate GZero (^TYPE 1)),
("P", ^mkPostulate GZero (^Arr Any (^FT "A" 0) (^TYPE 0))),
("a", ^mkPostulate GAny (^FT "A" 0)),
("a'", ^mkPostulate GAny (^FT "A" 0)),
("b", ^mkPostulate GAny (^FT "B" 0)),
("c", ^mkPostulate GAny (^FT "C" 0)),
("d", ^mkPostulate GAny (^FT "D" 0)),
("f", ^mkPostulate GAny (^Arr One (^FT "A" 0) (^FT "A" 0))),
("fω", ^mkPostulate GAny (^Arr Any (^FT "A" 0) (^FT "A" 0))),
("g", ^mkPostulate GAny (^Arr One (^FT "A" 0) (^FT "B" 0))),
("f2", ^mkPostulate GAny
[("A", mkPostulate GZero (^TYPE 0)),
("B", mkPostulate GZero (^TYPE 0)),
("C", mkPostulate GZero (^TYPE 1)),
("D", mkPostulate GZero (^TYPE 1)),
("P", mkPostulate GZero (^Arr Any (^FT "A" 0) (^TYPE 0))),
("a", mkPostulate GAny (^FT "A" 0)),
("a'", mkPostulate GAny (^FT "A" 0)),
("b", mkPostulate GAny (^FT "B" 0)),
("c", mkPostulate GAny (^FT "C" 0)),
("d", mkPostulate GAny (^FT "D" 0)),
("f", mkPostulate GAny (^Arr One (^FT "A" 0) (^FT "A" 0))),
("fω", mkPostulate GAny (^Arr Any (^FT "A" 0) (^FT "A" 0))),
("g", mkPostulate GAny (^Arr One (^FT "A" 0) (^FT "B" 0))),
("f2", mkPostulate GAny
(^Arr One (^FT "A" 0) (^Arr One (^FT "A" 0) (^FT "B" 0)))),
("p", ^mkPostulate GAny
("p", mkPostulate GAny
(^PiY One "x" (^FT "A" 0) (E $ ^App (^F "P" 0) (^BVT 0)))),
("q", ^mkPostulate GAny
("q", mkPostulate GAny
(^PiY One "x" (^FT "A" 0) (E $ ^App (^F "P" 0) (^BVT 0)))),
("refl", ^mkDef GAny reflTy reflDef),
("fst", ^mkDef GAny fstTy fstDef),
("snd", ^mkDef GAny sndTy sndDef)]
("refl", mkDef GAny reflTy reflDef),
("fst", mkDef GAny fstTy fstDef),
("snd", mkDef GAny sndTy sndDef)]
parameters (label : String) (act : Lazy (Eff Test ()))
{default defGlobals globals : Definitions}