summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Inky.idr277
-rw-r--r--src/Inky/Term.idr113
-rw-r--r--src/Inky/Term/Checks.idr16
-rw-r--r--src/Inky/Term/Compile.idr12
-rw-r--r--src/Inky/Term/Desugar.idr479
-rw-r--r--src/Inky/Term/Parser.idr537
-rw-r--r--src/Inky/Term/Pretty.idr226
-rw-r--r--src/Inky/Term/Pretty/Error.idr12
-rw-r--r--src/Inky/Term/Recompute.idr4
-rw-r--r--src/Inky/Term/Substitution.idr197
-rw-r--r--src/Inky/Term/Sugar.idr73
-rw-r--r--src/Inky/Type/Pretty.idr46
12 files changed, 1033 insertions, 959 deletions
diff --git a/src/Inky.idr b/src/Inky.idr
index ad3a503..3f6b755 100644
--- a/src/Inky.idr
+++ b/src/Inky.idr
@@ -6,6 +6,8 @@ import Control.App
import Control.App.Console
import Control.App.FileIO
+import Data.String
+
import Flap.Decidable
import Flap.Decidable.Maybe
import Flap.Parser
@@ -35,45 +37,110 @@ record Erased (a : Type) where
constructor Forget
0 value : a
+record SynthFailed where
+ constructor UhOh
+ term : Term NoSugar Bounds [<] [<]
+ err : NotSynths {m = Bounds} [<] [<] term
+
+Err : Type
+Err = List1 (WithBounds String)
+
+Interpolation Bounds where
+ interpolate b =
+ "\{show (1 + b.startLine)}:\{show (1 + b.startCol)}--\{show (1 + b.endLine)}:\{show (1 + b.endCol)}"
+
+Interpolation a => Interpolation (WithBounds a) where
+ interpolate x =
+ if x.isIrrelevant
+ then "?:?--?:?: \{x.val}"
+ else "\{x.bounds}: \{x.val}"
+
-- Actions ---------------------------------------------------------------------
-lexInkyString : HasErr String es => String -> App es (List (WithBounds InkyToken))
+readFile : FileIO es => File -> App es String
+readFile f = do
+ content <- read [<] f
+ pure (fastConcat $ content <>> [])
+ where
+ read : SnocList String -> File -> App es (SnocList String)
+ read acc f = do
+ False <- fEOF f
+ | True => pure acc
+ str <- fGetStr f
+ read (acc :< str) f
+
+readFileOrStdin : FileIO es => HasErr IOError es => Maybe FilePath -> App es String
+readFileOrStdin Nothing = readFile stdin
+readFileOrStdin (Just path) = withFile path Read throw readFile
+
+lexInkyString : HasErr (WithBounds String) es => String -> App es (List (WithBounds InkyToken))
lexInkyString file = do
let (tokens, _, _, "") = lex tokenMap file
- | (_, line, col, rest) => throw "\{show (1 + line)}:\{show col}: unexpected character"
+ | (_, line, col, rest) =>
+ throw (MkBounded "unexpected character" False (MkBounds line col line col))
pure (filter (\x => relevant x.val.kind) tokens)
-parseType : HasErr String es => List (WithBounds InkyToken) -> App es (Ty [<])
-parseType toks = do
- let Ok res [] _ = parse @{EqI} OpenType toks
- | Ok res (x :: _) _ => throw "\{x.bounds}: unexpected token \{x.val.kind}, expected end of input"
- | Err msg => throw msg
- let Right a = res.try [<]
- | Left msg => throw msg
+Interpolation (List InkyKind) where
+ interpolate [t] = interpolate t
+ interpolate ts = "one of " ++ joinBy ", " (map interpolate ts)
+
+doParse :
+ HasErr (WithBounds String) es =>
+ (p : InkyParser False [<] [<] a) ->
+ {auto 0 wf : collectTypeErrs @{ListSet} [<] [<] [<] [<] p = []} ->
+ List (WithBounds InkyToken) ->
+ App es a
+doParse p toks =
+ case parse @{ListSet} p toks of
+ Ok res [] _ => pure res
+ Ok res (x :: _) _ =>
+ throw ("expected end of input; got token \{x.val.kind}" <$ x)
+ Err err => throw (parseErrToString err)
+ where
+ parseErrToString : ParseErr InkyKind -> WithBounds String
+ parseErrToString (BadEOF ts) =
+ irrelevantBounds "expected \{ts}; got end of input"
+ parseErrToString (Unexpected ts got) =
+ "expected \{ts}; got token \{got.val.kind}" <$ got
+
+parseType :
+ Has [HasErr (WithBounds String), HasErr Err, HasErr IOError, FileIO] es =>
+ Maybe FilePath -> App es (Ty [<])
+parseType path = do
+ txt <- readFileOrStdin path
+ toks <- lexInkyString txt
+ res <- doParse OpenType toks
+ let Ok a = res.try [<]
+ | Errs errs => throw errs
pure a
-parseTerm : HasErr String es => List (WithBounds InkyToken) -> App es (Term Sugar Bounds [<] [<])
-parseTerm toks = do
- let Ok res [] _ = parse @{EqI} OpenTerm toks
- | Ok res (x :: _) _ => throw "\{x.bounds}: unexpected token \{x.val.kind}, expected end of input"
- | Err msg => throw msg
- let Right t = res.try [<] [<]
- | Left msg => throw msg
- pure t
+parseTerm :
+ Has [HasErr (WithBounds String), HasErr Err, HasErr IOError, FileIO] es =>
+ (termPath, tyPath : Maybe FilePath) -> App es (Term (Sugar [<]) Bounds [<] [<])
+parseTerm termPath tyPath = do
+ txt <- readFileOrStdin termPath
+ toks <- lexInkyString txt
+ res <- doParse OpenTerm toks
+ let Ok t = res.try (Sugar [<]) [<] [<]
+ | Errs errs => throw errs
+ -- Annotate with type
+ let Just _ = tyPath
+ | Nothing => pure t
+ a <- parseType tyPath
+ pure (Annot (MkBounds 0 0 0 0) t a)
-checkType : HasErr String es => (a : Ty [<]) -> App es (Erased $ WellFormed a)
-checkType a = do
- let True `Because` wf = wellFormed a
- | False `Because` bad => throw "type ill-formed"
- pure (Forget wf)
+checkType : HasErr String es => (a : Ty [<]) -> App es ()
+checkType a =
+ unless (wellFormed a).does $
+ throw "type ill-formed"
synthTerm :
- (t : Term mode m [<] [<]) ->
- HasErr (NotSynths [<] [<] t) es =>
+ (t : Term NoSugar Bounds [<] [<]) ->
+ HasErr SynthFailed es =>
App es (Subset (Ty [<]) (Synths [<] [<] t))
synthTerm t = do
let Just a `Because` prf = synths [<] [<] t
- | Nothing `Because` contra => throw contra
+ | Nothing `Because` contra => throw (UhOh t contra)
pure (Element a prf)
printType :
@@ -84,23 +151,13 @@ printType a = do
printTerm :
PrimIO es => {default defaultLayoutOptions opts : LayoutOptions} ->
- Term mode m [<] [<] -> App es ()
+ {mode : Term.Mode} -> Term mode m [<] [<] -> App es ()
printTerm a = do
primIO $ renderIO $ layoutSmart opts $ prettyTerm a Open
-printSynthError :
- PrimIO es => {default defaultLayoutOptions opts : LayoutOptions} ->
- {t : Term mode Bounds [<] [<]} ->
- NotSynths [<] [<] t -> App es ()
-printSynthError contra =
- primIO $ renderIO $ layoutSmart opts $
- concatWith (surround hardline) $
- map (\(bounds, msg) => group $ align $ hang 2 $ pretty "\{bounds}:" <+> line <+> msg) $
- prettyNotSynths contra
-
compileTerm :
PrimIO es => {default defaultLayoutOptions opts : LayoutOptions} ->
- {t : Term mode m [<] [<]} ->
+ {t : Term NoSugar m [<] [<]} ->
(0 prf : Synths [<] [<] t a) ->
App es ()
compileTerm prf =
@@ -108,22 +165,6 @@ compileTerm prf =
pretty "(use-modules (ice-9 match))" <+> line <+>
parens (hang 1 $ pretty "define main" <+> line <+> group (compileSynths [<] [<] prf))
-readFile : FileIO es => File -> App es String
-readFile f = do
- content <- read [<] f
- pure (fastConcat $ content <>> [])
- where
- read : SnocList String -> File -> App es (SnocList String)
- read acc f = do
- False <- fEOF f
- | True => pure acc
- str <- fGetStr f
- read (acc :< str) f
-
-readFileOrStdin : FileIO es => HasErr IOError es => Maybe FilePath -> App es String
-readFileOrStdin Nothing = readFile stdin
-readFileOrStdin (Just path) = withFile path Read throw readFile
-
-- Arguments -------------------------------------------------------------------
@@ -188,27 +229,25 @@ Inky = MkCommand
-- Driver ----------------------------------------------------------------------
-parseArgs :
- (cmd : Command nm) ->
- App (String :: Init) (ParseTree cmd)
-parseArgs cmd = do
- Right args <- primIO cmd.parseArgs
- | Left msg => throw msg
- let Pure args = ParsedTree.finalising args
- | Fail errs => throw (show $ the (Error ()) $ Fail errs)
- pure args
-
-abortErr : PrimIO es => String -> App es a
-abortErr msg = do
- primIO $ () <$ fPutStrLn stderr msg
- primIO exitFailure
-
showHelp : Console es => App es ()
showHelp = putStrLn "Usage: \{Inky .usage}"
-main : IO ()
-main = run {l = MayThrow} $ do
- args <- handle {err = String} (parseArgs Inky) pure abortErr
+process :
+ Has
+ [ HasErr String
+ , HasErr (WithBounds String)
+ , HasErr (List1 $ WithBounds String)
+ , HasErr (List1 ErrorMsg)
+ , HasErr SynthFailed
+ , FileIO
+ , PrimIO
+ ] es =>
+ App es ()
+process = do
+ Right args <- primIO (Inky).parseArgs
+ | Left msg => throw msg
+ let Pure args = ParsedTree.finalising args
+ | Fail errs => throw errs
Collie.handle {cmd = ("inky" ** Inky)} args
[ const showHelp
, "--help" ::= [ const showHelp ]
@@ -217,24 +256,16 @@ main = run {l = MayThrow} $ do
, "type" ::=
[ \cmd => do
let path = cmd.arguments
- txt <- handle {err = IOError} (readFileOrStdin path) pure (abortErr . show)
- toks <- handle {err = String} (lexInkyString txt) pure abortErr
- a <- handle {err = String} (parseType toks) pure abortErr
+ a <- parseType path
printType a
- pure ()
]
, "term" ::=
[ \cmd => do
let path = cmd.arguments
- txt <- handle {err = IOError} (readFileOrStdin path) pure (abortErr . show)
- toks <- handle {err = String} (lexInkyString txt) pure abortErr
- t <- handle {err = String} (parseTerm toks) pure abortErr
+ t <- parseTerm path Nothing
let [noSugar] = cmd.modifiers.content
case noSugar of
- True => do
- let Just t = maybeDesugar t
- | Nothing => abortErr "failed to desugar term"
- printTerm t
+ True => printTerm (desugar t)
False => printTerm t
]
]
@@ -243,29 +274,18 @@ main = run {l = MayThrow} $ do
, "type" ::=
[ \cmd => do
let path = cmd.arguments
- txt <- handle {err = IOError} (readFileOrStdin path) pure (abortErr . show)
- toks <- handle {err = String} (lexInkyString txt) pure abortErr
- a <- handle {err = String} (parseType toks) pure abortErr
- handle {err = String} (checkType a) (const $ pure ()) abortErr
+ a <- parseType path
+ _ <- checkType a
+ pure ()
]
, "term" ::=
[ \cmd => do
let path = cmd.arguments
- txt <- handle {err = IOError} (readFileOrStdin path) pure (abortErr . show)
- toks <- handle {err = String} (lexInkyString txt) pure abortErr
- t <- handle {err = String} (parseTerm toks) pure abortErr
let [type] = cmd.modifiers.content
- t <-
- maybe (pure t)
- (\path => do
- txt <- handle {err = IOError} (readFileOrStdin $ Just path) pure (abortErr . show)
- toks <- handle {err = String} (lexInkyString txt) pure abortErr
- a <- handle {err = String} (parseType toks) pure abortErr
- handle {err = String} (checkType a) (const $ pure ()) abortErr
- pure (Annot (MkBounds (-1) (-1) (-1) (-1)) t a))
- type
- handle {err = NotSynths [<] [<] t} (synthTerm t) (const $ pure ())
- (\contra => do printSynthError contra; primIO exitFailure)
+ t <- parseTerm path type
+ let t = desugar t
+ _ <- synthTerm t
+ pure ()
]
]
, "compile" ::=
@@ -273,23 +293,50 @@ main = run {l = MayThrow} $ do
, "term" ::=
[ \cmd => do
let path = cmd.arguments
- txt <- handle {err = IOError} (readFileOrStdin path) pure (abortErr . show)
- toks <- handle {err = String} (lexInkyString txt) pure abortErr
- t <- handle {err = String} (parseTerm toks) pure abortErr
let [type] = cmd.modifiers.content
- t <-
- maybe (pure t)
- (\path => do
- txt <- handle {err = IOError} (readFileOrStdin $ Just path) pure (abortErr . show)
- toks <- handle {err = String} (lexInkyString txt) pure abortErr
- a <- handle {err = String} (parseType toks) pure abortErr
- handle {err = String} (checkType a) (const $ pure ()) abortErr
- pure (Annot (MkBounds (-1) (-1) (-1) (-1)) t a))
- type
- Element _ prf <-
- handle {err = NotSynths [<] [<] t} (synthTerm t) pure
- (\contra => do printSynthError contra; primIO exitFailure)
+ t <- parseTerm path type
+ let t = desugar t
+ Element _ prf <- synthTerm t
compileTerm prf
]
]
]
+
+handleErr : (0 e : Type) -> (forall a. e -> App es a) -> App (e :: es) a -> App es a
+handleErr e handler app = handle app pure handler
+
+printSynthFailed :
+ PrimIO es => {default defaultLayoutOptions opts : LayoutOptions} ->
+ SynthFailed -> App es ()
+printSynthFailed (UhOh t err) =
+ primIO $ renderIO $ layoutSmart opts $
+ concatWith (surround hardline) $
+ map (\(bounds, msg) => group $ align $ hang 2 $ pretty "\{bounds}:" <+> line <+> msg) $
+ prettyNotSynths err
+
+main : IO ()
+main =
+ run {l = MayThrow} $
+ handleErr (List String)
+ (\msgs => do
+ foldlM (\_, msg => primIO $ () <$ fPutStrLn stderr msg) () msgs
+ primIO exitFailure) $
+ handleErr String
+ (throw . List.singleton) $
+ handleErr (List1 ErrorMsg)
+ (throw . map show . forget) $
+ handleErr (List1 $ WithBounds String)
+ (throw . map interpolate . forget) $
+ handleErr (WithBounds String)
+ (throw . (::: [])) $
+ handleErr IOError
+ (throw . show) $
+ handleErr SynthFailed
+ (\err => do
+ printSynthFailed err
+ primIO exitFailure) $
+ process
+
+-- main =
+-- run {l = MayThrow} $
+-- handle
diff --git a/src/Inky/Term.idr b/src/Inky/Term.idr
index 8fd15aa..0f05f59 100644
--- a/src/Inky/Term.idr
+++ b/src/Inky/Term.idr
@@ -16,7 +16,23 @@ import Flap.Decidable.Maybe
--------------------------------------------------------------------------------
public export
-data Mode = Sugar | NoSugar
+data Mode : Type where
+ Quote : (tyCtx, tmCtx : SnocList String) -> Mode
+ Sugar : (qtCtx : SnocList String) -> Mode
+ NoSugar : Mode
+
+namespace Mode
+ public export
+ NotQuote : Mode -> Type
+ NotQuote (Quote _ _) = Void
+ NotQuote (Sugar _) = So True
+ NotQuote NoSugar = So True
+
+ public export
+ HasSugar : Mode -> Type
+ HasSugar (Quote _ _) = So True
+ HasSugar (Sugar _) = So True
+ HasSugar NoSugar = Void
public export
record WithDoc (a : Type) where
@@ -25,11 +41,28 @@ record WithDoc (a : Type) where
doc : List String
public export
-data Term : Mode -> (m : Type) -> (tyCtx, tmCtx : SnocList String) -> Type where
- Annot : (meta : m) -> Term mode m tyCtx tmCtx -> Ty tyCtx -> Term mode m tyCtx tmCtx
+data Term : Mode -> (m : Type) -> (tyCtx, tmCtx : SnocList String) -> Type
+
+public export
+Ty' : Mode -> (m : Type) -> (tyCtx, tmCtx : SnocList String) -> Type
+Ty' (Quote tyCtx tmCtx) m _ qtCtx = Term (Sugar qtCtx) m tyCtx tmCtx
+Ty' (Sugar qtCtx) m tyCtx tmCtx = Ty tyCtx
+Ty' NoSugar m tyCtx tmCtx = Ty tyCtx
+
+public export
+BoundTy' : Mode -> (m : Type) -> (tyCtx, tmCtx : SnocList String) -> Type
+BoundTy' (Quote tyCtx tmCtx) m _ qtCtx = Term (Sugar qtCtx) m tyCtx tmCtx
+BoundTy' (Sugar qtCtx) m tyCtx tmCtx = (x ** Ty (tyCtx :< x))
+BoundTy' NoSugar m tyCtx tmCtx = (x ** Ty (tyCtx :< x))
+
+data Term where
+ Annot : (meta : m) -> Term mode m tyCtx tmCtx -> Ty' mode m tyCtx tmCtx -> Term mode m tyCtx tmCtx
Var : (meta : m) -> Var tmCtx -> Term mode m tyCtx tmCtx
Let : (meta : WithDoc m) -> Term mode m tyCtx tmCtx -> (x ** Term mode m tyCtx (tmCtx :< x)) -> Term mode m tyCtx tmCtx
- LetTy : (meta : WithDoc m) -> Ty tyCtx -> (x ** Term mode m (tyCtx :< x) tmCtx) -> Term mode m tyCtx tmCtx
+ LetTy :
+ {auto 0 notQuote : NotQuote mode} ->
+ (meta : WithDoc m) -> Ty tyCtx ->
+ (x ** Term mode m (tyCtx :< x) tmCtx) -> Term mode m tyCtx tmCtx
Abs : (meta : m) -> (bound ** Term mode m tyCtx (tmCtx <>< bound)) -> Term mode m tyCtx tmCtx
App : (meta : m) -> Term mode m tyCtx tmCtx -> List (Term mode m tyCtx tmCtx) -> Term mode m tyCtx tmCtx
Tup : (meta : m) -> Row (Term mode m tyCtx tmCtx) -> Term mode m tyCtx tmCtx
@@ -39,7 +72,29 @@ data Term : Mode -> (m : Type) -> (tyCtx, tmCtx : SnocList String) -> Type where
Roll : (meta : m) -> Term mode m tyCtx tmCtx -> Term mode m tyCtx tmCtx
Unroll : (meta : m) -> Term mode m tyCtx tmCtx -> Term mode m tyCtx tmCtx
Fold : (meta : m) -> Term mode m tyCtx tmCtx -> (x ** Term mode m tyCtx (tmCtx :< x)) -> Term mode m tyCtx tmCtx
- Map : (meta : m) -> (x ** Ty (tyCtx :< x)) -> Ty tyCtx -> Ty tyCtx -> Term Sugar m tyCtx tmCtx
+ Map : (meta : m) -> BoundTy' mode m tyCtx tmCtx -> Ty' mode m tyCtx tmCtx -> Ty' mode m tyCtx tmCtx -> Term mode m tyCtx tmCtx
+ -- Quotation sugar
+ QuasiQuote : (meta : m) -> Term (Quote tyCtx tmCtx) m [<] qtCtx -> Term (Sugar qtCtx) m tyCtx tmCtx
+ Unquote : (meta : m) -> Term (Sugar qtCtx) m tyCtx tmCtx -> Term (Quote tyCtx tmCtx) m [<] qtCtx
+ QAbs : (meta : m) -> (bound ** Term (Sugar (qtCtx <>< bound)) m tyCtx tmCtx) -> Term (Sugar qtCtx) m tyCtx tmCtx
+ -- Other sugar
+ Lit :
+ (meta : m) -> Nat ->
+ Term (Sugar qtCtx) m tyCtx tmCtx
+ Suc :
+ (meta : m) -> Term (Sugar qtCtx) m tyCtx tmCtx ->
+ Term (Sugar qtCtx) m tyCtx tmCtx
+ List :
+ (meta : m) -> List (Term (Sugar qtCtx) m tyCtx tmCtx) ->
+ Term (Sugar qtCtx) m tyCtx tmCtx
+ Cons :
+ (meta : m) ->
+ Term (Sugar qtCtx) m tyCtx tmCtx ->
+ Term (Sugar qtCtx) m tyCtx tmCtx ->
+ Term (Sugar qtCtx) m tyCtx tmCtx
+ Str :
+ (meta : m) -> String ->
+ Term (Sugar qtCtx) m tyCtx tmCtx
%name Term e, f, t, u
@@ -59,6 +114,14 @@ export
(Unroll meta _).meta = meta
(Fold meta _ _).meta = meta
(Map meta _ _ _).meta = meta
+(QuasiQuote meta _).meta = meta
+(Unquote meta _).meta = meta
+(QAbs meta _).meta = meta
+(Lit meta _).meta = meta
+(Suc meta _).meta = meta
+(List meta _).meta = meta
+(Cons meta _ _).meta = meta
+(Str meta _).meta = meta
--------------------------------------------------------------------------------
-- Well Formed -----------------------------------------------------------------
@@ -126,7 +189,7 @@ isFunction (x :: bound) a =
namespace Modes
public export
- data SynthsOnly : Term mode m tyCtx tmCtx -> Type where
+ data SynthsOnly : Term NoSugar m tyCtx tmCtx -> Type where
Annot : SynthsOnly (Annot meta t a)
Var : SynthsOnly (Var meta i)
App : SynthsOnly (App meta f ts)
@@ -135,7 +198,7 @@ namespace Modes
Map : SynthsOnly (Map meta (x ** a) b c)
public export
- data ChecksOnly : Term mode m tyCtx tmCtx -> Type where
+ data ChecksOnly : Term NoSugar m tyCtx tmCtx -> Type where
Abs : ChecksOnly (Abs meta (bounds ** t))
Inj : ChecksOnly (Inj meta l t)
Case : ChecksOnly (Case meta e ts)
@@ -149,19 +212,19 @@ public export
data Synths :
All (Assoc0 $ Ty [<]) tyCtx ->
All (Assoc0 $ Ty [<]) tmCtx ->
- Term mode m tyCtx tmCtx -> Ty [<] -> Type
+ Term NoSugar m tyCtx tmCtx -> Ty [<] -> Type
public export
data Checks :
All (Assoc0 $ Ty [<]) tyCtx ->
All (Assoc0 $ Ty [<]) tmCtx ->
- Ty [<] -> Term mode m tyCtx tmCtx -> Type
+ Ty [<] -> Term NoSugar m tyCtx tmCtx -> Type
namespace Spine
public export
data CheckSpine :
All (Assoc0 $ Ty [<]) tyCtx ->
All (Assoc0 $ Ty [<]) tmCtx ->
- Ty [<] -> List (Term mode m tyCtx tmCtx) -> Ty [<] -> Type
+ Ty [<] -> List (Term NoSugar m tyCtx tmCtx) -> Ty [<] -> Type
where
Nil : CheckSpine tyEnv tmEnv a [] a
(::) :
@@ -176,7 +239,7 @@ namespace Synths
data AllSynths :
All (Assoc0 $ Ty [<]) tyCtx ->
All (Assoc0 $ Ty [<]) tmCtx ->
- Context (Term mode m tyCtx tmCtx) -> Row (Ty [<]) -> Type
+ Context (Term NoSugar m tyCtx tmCtx) -> Row (Ty [<]) -> Type
where
Lin : AllSynths tyEnv tmEnv [<] [<]
(:<) :
@@ -192,7 +255,7 @@ namespace Checks
data AllChecks :
All (Assoc0 $ Ty [<]) tyCtx ->
All (Assoc0 $ Ty [<]) tmCtx ->
- Context (Ty [<]) -> Context (Term mode m tyCtx tmCtx) -> Type
+ Context (Ty [<]) -> Context (Term NoSugar m tyCtx tmCtx) -> Type
where
Base : AllChecks tyEnv tmEnv [<] [<]
Step :
@@ -208,7 +271,7 @@ namespace Branches
data AllBranches :
All (Assoc0 $ Ty [<]) tyCtx ->
All (Assoc0 $ Ty [<]) tmCtx ->
- Context (Ty [<]) -> Ty [<] -> Context (x ** Term mode m tyCtx (tmCtx :< x)) -> Type
+ Context (Ty [<]) -> Ty [<] -> Context (x ** Term NoSugar m tyCtx (tmCtx :< x)) -> Type
where
Base : AllBranches tyEnv tmEnv [<] a [<]
Step :
@@ -233,7 +296,7 @@ data Synths where
LetTyS :
WellFormed a ->
Synths (tyEnv :< (x :- sub tyEnv a)) tmEnv e b ->
- Synths tyEnv tmEnv (LetTy meta a (x ** e)) b
+ Synths tyEnv tmEnv (LetTy {notQuote} meta a (x ** e)) b
AppS :
Synths tyEnv tmEnv f a ->
CheckSpine tyEnv tmEnv a ts b ->
@@ -263,9 +326,9 @@ data Checks where
Alpha b c ->
Checks tyEnv tmEnv c (Annot meta t a)
VarC :
- Synths tyEnv tmEnv (Var {mode} meta i) a ->
+ Synths tyEnv tmEnv (Var meta i) a ->
Alpha a b ->
- Checks tyEnv tmEnv b (Var {mode} meta i)
+ Checks tyEnv tmEnv b (Var meta i)
LetC :
Synths tyEnv tmEnv e a ->
Checks tyEnv (tmEnv :< (x :- a)) b t ->
@@ -273,7 +336,7 @@ data Checks where
LetTyC :
WellFormed a ->
Checks (tyEnv :< (x :- sub tyEnv a)) tmEnv b t ->
- Checks tyEnv tmEnv b (LetTy meta a (x ** t))
+ Checks tyEnv tmEnv b (LetTy {notQuote} meta a (x ** t))
AbsC :
IsFunction bound a dom cod ->
Checks tyEnv (tmEnv <>< dom) cod t ->
@@ -334,19 +397,19 @@ public export
data NotSynths :
All (Assoc0 $ Ty [<]) tyCtx ->
All (Assoc0 $ Ty [<]) tmCtx ->
- Term mode m tyCtx tmCtx -> Type
+ Term NoSugar m tyCtx tmCtx -> Type
public export
data NotChecks :
All (Assoc0 $ Ty [<]) tyCtx ->
All (Assoc0 $ Ty [<]) tmCtx ->
- Ty [<] -> Term mode m tyCtx tmCtx -> Type
+ Ty [<] -> Term NoSugar m tyCtx tmCtx -> Type
namespace Spine
public export
data NotCheckSpine :
All (Assoc0 $ Ty [<]) tyCtx ->
All (Assoc0 $ Ty [<]) tmCtx ->
- Ty [<] -> List (Term mode m tyCtx tmCtx) -> Type
+ Ty [<] -> List (Term NoSugar m tyCtx tmCtx) -> Type
where
Step1 :
((b, c : Ty [<]) -> Not (a = TArrow b c)) ->
@@ -362,7 +425,7 @@ namespace Synths
data AnyNotSynths :
All (Assoc0 $ Ty [<]) tyCtx ->
All (Assoc0 $ Ty [<]) tmCtx ->
- (ts : Context (Term mode m tyCtx tmCtx)) -> Type
+ (ts : Context (Term NoSugar m tyCtx tmCtx)) -> Type
where
Step :
These (NotSynths tyEnv tmEnv t) (AnyNotSynths tyEnv tmEnv ts) ->
@@ -375,7 +438,7 @@ namespace Checks
data AnyNotChecks :
All (Assoc0 $ Ty [<]) tyCtx ->
All (Assoc0 $ Ty [<]) tmCtx ->
- Context (Ty [<]) -> Context (Term mode m tyCtx tmCtx) -> Type
+ Context (Ty [<]) -> Context (Term NoSugar m tyCtx tmCtx) -> Type
where
Base1 : AnyNotChecks tyEnv tmEnv (as :< la) [<]
Step1 :
@@ -393,7 +456,7 @@ namespace Branches
data AnyNotBranches :
All (Assoc0 $ Ty [<]) tyCtx ->
All (Assoc0 $ Ty [<]) tmCtx ->
- Context (Ty [<]) -> Ty [<] -> Context (x ** Term mode m tyCtx (tmCtx :< x)) -> Type
+ Context (Ty [<]) -> Ty [<] -> Context (x ** Term NoSugar m tyCtx (tmCtx :< x)) -> Type
where
Base1 : AnyNotBranches tyEnv tmEnv (as :< a) b [<]
Step1 :
@@ -429,7 +492,7 @@ data NotSynths where
NotSynths tyEnv tmEnv (Let meta e (x ** f))
LetTyNS :
These (IllFormed a) (NotSynths (tyEnv :< (x :- sub tyEnv a)) tmEnv e) ->
- NotSynths tyEnv tmEnv (LetTy meta a (x ** e))
+ NotSynths tyEnv tmEnv (LetTy {notQuote} meta a (x ** e))
AppNS1 :
NotSynths tyEnv tmEnv f ->
NotSynths tyEnv tmEnv (App meta f ts)
@@ -486,7 +549,7 @@ data NotChecks where
NotChecks tyEnv tmEnv b (Let meta e (x ** t))
LetTyNC :
These (IllFormed a) (NotChecks (tyEnv :< (x :- sub tyEnv a)) tmEnv b t) ->
- NotChecks tyEnv tmEnv b (LetTy meta a (x ** t))
+ NotChecks tyEnv tmEnv b (LetTy {notQuote} meta a (x ** t))
AbsNC1 :
NotFunction bound a ->
NotChecks tyEnv tmEnv a (Abs meta (bound ** t))
diff --git a/src/Inky/Term/Checks.idr b/src/Inky/Term/Checks.idr
index 829561a..0824362 100644
--- a/src/Inky/Term/Checks.idr
+++ b/src/Inky/Term/Checks.idr
@@ -1,13 +1,16 @@
module Inky.Term.Checks
import Control.Function
+
import Data.DPair
import Data.List.Quantifiers
import Data.Singleton
import Data.These
+
import Flap.Data.SnocList.Quantifiers
import Flap.Decidable
import Flap.Decidable.Maybe
+
import Inky.Term
import Inky.Term.Recompute
@@ -208,23 +211,23 @@ export
synths :
(tyEnv : All (Assoc0 $ Ty [<]) tyCtx) ->
(tmEnv : All (Assoc0 $ Ty [<]) tmCtx) ->
- (e : Term mode m tyCtx tmCtx) ->
+ (e : Term NoSugar m tyCtx tmCtx) ->
Proof (Ty [<]) (Synths tyEnv tmEnv e) (NotSynths tyEnv tmEnv e)
export
checks :
(tyEnv : All (Assoc0 $ Ty [<]) tyCtx) ->
(tmEnv : All (Assoc0 $ Ty [<]) tmCtx) ->
- (a : Ty [<]) -> (t : Term mode m tyCtx tmCtx) ->
+ (a : Ty [<]) -> (t : Term NoSugar m tyCtx tmCtx) ->
LazyEither (Checks tyEnv tmEnv a t) (NotChecks tyEnv tmEnv a t)
checkSpine :
(tyEnv : All (Assoc0 $ Ty [<]) tyCtx) ->
(tmEnv : All (Assoc0 $ Ty [<]) tmCtx) ->
- (a : Ty [<]) -> (ts : List (Term mode m tyCtx tmCtx)) ->
+ (a : Ty [<]) -> (ts : List (Term NoSugar m tyCtx tmCtx)) ->
Proof (Ty [<]) (CheckSpine tyEnv tmEnv a ts) (NotCheckSpine tyEnv tmEnv a ts)
allSynths :
(tyEnv : All (Assoc0 $ Ty [<]) tyCtx) ->
(tmEnv : All (Assoc0 $ Ty [<]) tmCtx) ->
- (es : Context (Term mode m tyCtx tmCtx)) ->
+ (es : Context (Term NoSugar m tyCtx tmCtx)) ->
(0 fresh : AllFresh es.names) ->
Proof (Subset (Row (Ty [<])) (\as => es.names = as.names))
(AllSynths tyEnv tmEnv es . Subset.fst)
@@ -232,12 +235,13 @@ allSynths :
allChecks :
(tyEnv : All (Assoc0 $ Ty [<]) tyCtx) ->
(tmEnv : All (Assoc0 $ Ty [<]) tmCtx) ->
- (as : Context (Ty [<])) -> (ts : Context (Term mode m tyCtx tmCtx)) ->
+ (as : Context (Ty [<])) -> (ts : Context (Term NoSugar m tyCtx tmCtx)) ->
LazyEither (AllChecks tyEnv tmEnv as ts) (AnyNotChecks tyEnv tmEnv as ts)
allBranches :
(tyEnv : All (Assoc0 $ Ty [<]) tyCtx) ->
(tmEnv : All (Assoc0 $ Ty [<]) tmCtx) ->
- (as : Context (Ty [<])) -> (a : Ty [<]) -> (ts : Context (x ** Term mode m tyCtx (tmCtx :< x))) ->
+ (as : Context (Ty [<])) -> (a : Ty [<]) ->
+ (ts : Context (x ** Term NoSugar m tyCtx (tmCtx :< x))) ->
LazyEither (AllBranches tyEnv tmEnv as a ts) (AnyNotBranches tyEnv tmEnv as a ts)
synths tyEnv tmEnv (Annot _ t a) =
diff --git a/src/Inky/Term/Compile.idr b/src/Inky/Term/Compile.idr
index 0867cd2..0d42660 100644
--- a/src/Inky/Term/Compile.idr
+++ b/src/Inky/Term/Compile.idr
@@ -149,7 +149,7 @@ compileFold {a} wf prf target bind body =
export
compileSynths :
{tmCtx : SnocList String} ->
- {t : Term mode m tyCtx tmCtx} ->
+ {t : Term NoSugar m tyCtx tmCtx} ->
{tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
{tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
(0 tyWf : DAll WellFormed tyEnv) ->
@@ -159,7 +159,7 @@ compileSynths :
export
compileChecks :
{tmCtx : SnocList String} ->
- {t : Term mode m tyCtx tmCtx} ->
+ {t : Term NoSugar m tyCtx tmCtx} ->
{tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
{tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
(0 tyWf : DAll WellFormed tyEnv) ->
@@ -170,7 +170,7 @@ compileChecks :
Doc ann
compileSpine :
{tmCtx : SnocList String} ->
- {ts : List (Term mode m tyCtx tmCtx)} ->
+ {ts : List (Term NoSugar m tyCtx tmCtx)} ->
{tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
{tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
(0 tyWf : DAll WellFormed tyEnv) ->
@@ -182,7 +182,7 @@ compileSpine :
Doc ann
compileAllSynths :
{tmCtx : SnocList String} ->
- {ts : Context (Term mode m tyCtx tmCtx)} ->
+ {ts : Context (Term NoSugar m tyCtx tmCtx)} ->
{tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
{tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
(0 tyWf : DAll WellFormed tyEnv) ->
@@ -191,7 +191,7 @@ compileAllSynths :
All (Assoc0 $ Doc ann) ts.names
compileAllChecks :
{tmCtx : SnocList String} ->
- {ts : Context (Term mode m tyCtx tmCtx)} ->
+ {ts : Context (Term NoSugar m tyCtx tmCtx)} ->
{tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
{tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
(0 tyWf : DAll WellFormed tyEnv) ->
@@ -203,7 +203,7 @@ compileAllChecks :
All (Assoc0 $ Doc ann) ts.names
compileAllBranches :
{tmCtx : SnocList String} ->
- {ts : Context (x ** Term mode m tyCtx (tmCtx :< x))} ->
+ {ts : Context (x ** Term NoSugar m tyCtx (tmCtx :< x))} ->
{tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
{tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
(0 tyWf : DAll WellFormed tyEnv) ->
diff --git a/src/Inky/Term/Desugar.idr b/src/Inky/Term/Desugar.idr
index 4bf8f05..2ad87c9 100644
--- a/src/Inky/Term/Desugar.idr
+++ b/src/Inky/Term/Desugar.idr
@@ -1,269 +1,226 @@
module Inky.Term.Desugar
-import Data.List.Quantifiers
-import Data.Maybe
-import Flap.Data.List
-import Flap.Decidable
+import Control.Monad.State
+import Data.SortedMap
import Inky.Term
-import Inky.Term.Substitution
--- Desugar map -----------------------------------------------------------------
-
-desugarMap :
- (meta : m) =>
- (a : Ty tyCtx) -> (i : Var tyCtx) -> (0 prf : i `StrictlyPositiveIn` a) ->
- (f : Term mode m tyCtx' tmCtx) ->
- (t : Term mode m tyCtx' tmCtx) ->
- Term mode m tyCtx' tmCtx
-desugarMapTuple :
- (meta : m) =>
- (as : Context (Ty tyCtx)) ->
- (0 fresh : AllFresh as.names) ->
- (i : Var tyCtx) -> (0 prfs : i `StrictlyPositiveInAll` as) ->
- (f : Term mode m tyCtx' tmCtx) ->
- (t : Term mode m tyCtx' tmCtx) ->
- Row (Term mode m tyCtx' tmCtx)
-desugarMapTupleNames :
- (0 meta : m) =>
- (as : Context (Ty tyCtx)) ->
- (0 fresh : AllFresh as.names) ->
- (0 i : Var tyCtx) -> (0 prfs : i `StrictlyPositiveInAll` as) ->
- (0 f : Term mode m tyCtx' tmCtx) ->
- (0 t : Term mode m tyCtx' tmCtx) ->
- (desugarMapTuple as fresh i prfs f t).names = as.names
-desugarMapCase :
+-- Other Sugar -----------------------------------------------------------------
+
+suc : m -> Term NoSugar m tyCtx tmCtx -> Term NoSugar m tyCtx tmCtx
+suc meta t = Roll meta $ Inj meta "S" t
+
+lit : m -> Nat -> Term NoSugar m tyCtx tmCtx
+lit meta 0 = Roll meta $ Inj meta "Z" $ Tup meta [<]
+lit meta (S k) = suc meta (lit meta k)
+
+cons : m -> Term NoSugar m tyCtx tmCtx -> Term NoSugar m tyCtx tmCtx -> Term NoSugar m tyCtx tmCtx
+cons meta t u = Roll meta $ Inj meta "C" $ Tup meta [<"H" :- t, "T" :- u]
+
+list : m -> List (Term NoSugar m tyCtx tmCtx) -> Term NoSugar m tyCtx tmCtx
+list meta [] = Roll meta $ Inj meta "N" $ Tup meta [<]
+list meta (t :: ts) = cons meta t (list meta ts)
+
+record Cache (a : Type) where
+ constructor MkCache
+ max : Nat
+ vals : SortedMap a Nat
+
+miss : Ord a => a -> Cache a -> (Cache a, Nat)
+miss x cache =
+ let newVals = insert x cache.max cache.vals in
+ let newMax = S cache.max in
+ (MkCache newMax newVals, cache.max)
+
+lookup : Ord a => MonadState (Cache a) m => a -> m Nat
+lookup x = do
+ cache <- get
+ case lookup x cache.vals of
+ Nothing => state (miss x)
+ Just n => pure n
+
+string : MonadState (Cache String) f => m -> String -> f (Term NoSugar m tyCtx tmCtx)
+string meta str = do
+ n <- lookup str
+ pure $ lit meta n
+
+-- Desugar ---------------------------------------------------------------------
+
+desugar' :
+ MonadState (Cache String) f =>
+ Term (Sugar qtCtx) m tyCtx tmCtx -> f (Term NoSugar m tyCtx tmCtx)
+desugarAll :
+ MonadState (Cache String) f =>
+ List (Term (Sugar qtCtx) m tyCtx tmCtx) ->
+ f (List $ Term NoSugar m tyCtx tmCtx)
+desugarCtx :
+ MonadState (Cache String) f =>
+ (ctx : Context (Term (Sugar qtCtx) m tyCtx tmCtx)) ->
+ f (All (Assoc0 $ Term NoSugar m tyCtx tmCtx) ctx.names)
+desugarBranches :
+ MonadState (Cache String) f =>
+ (ctx : Context (x ** Term (Sugar qtCtx) m tyCtx (tmCtx :< x))) ->
+ f (All (Assoc0 (x ** Term NoSugar m tyCtx (tmCtx :< x))) ctx.names)
+
+quote :
+ MonadState (Cache String) f =>
+ Term (Quote tyCtx tmCtx) m [<] qtCtx ->
+ f (Term NoSugar m tyCtx tmCtx)
+quoteAll :
+ MonadState (Cache String) f =>
+ List (Term (Quote tyCtx tmCtx) m [<] qtCtx) ->
+ f (List $ Term NoSugar m tyCtx tmCtx)
+quoteCtx :
+ MonadState (Cache String) f =>
(meta : m) =>
- (as : Context (Ty tyCtx)) ->
- (0 fresh : AllFresh as.names) ->
- (i : Var tyCtx) -> (0 prfs : i `StrictlyPositiveInAll` as) ->
- (f : Term mode m tyCtx' tmCtx) ->
- Row (x ** Term mode m tyCtx' (tmCtx :< x))
-desugarMapCaseNames :
+ Context (Term (Quote tyCtx tmCtx) m [<] qtCtx) ->
+ f (List $ Term NoSugar m tyCtx tmCtx)
+quoteBranches :
+ MonadState (Cache String) f =>
(meta : m) =>
- (as : Context (Ty tyCtx)) ->
- (0 fresh : AllFresh as.names) ->
- (i : Var tyCtx) -> (0 prfs : i `StrictlyPositiveInAll` as) ->
- (f : Term mode m tyCtx' tmCtx) ->
- (desugarMapCase as fresh i prfs f).names = as.names
-
-desugarMap (TVar j) i TVar f t with (i `decEq` j)
- _ | True `Because` _ = App meta f [t]
- _ | False `Because` _ = t
-desugarMap (TArrow a b) i (TArrow prf) f t = t
-desugarMap (TProd (MkRow as fresh)) i (TProd prfs) f t =
- Tup meta (desugarMapTuple as fresh i prfs f t)
-desugarMap (TSum (MkRow as fresh)) i (TSum prfs) f t =
- Case meta t (desugarMapCase as fresh i prfs f)
-desugarMap (TFix x a) i (TFix prf) f t =
- Fold meta t ("_eta" ** Roll meta
- (desugarMap a (ThereVar i) prf (thin (Drop Id) f) (Var meta (%% "_eta"))))
-
-desugarMapTuple [<] [<] i [<] f t = [<]
-desugarMapTuple (as :< (l :- a)) (fresh :< freshIn) i (prfs :< prf) f t =
- (:<)
- (desugarMapTuple as fresh i prfs f t)
- (l :- desugarMap a i prf f (Prj meta t l))
- @{rewrite desugarMapTupleNames as fresh i prfs f t in freshIn}
-
-desugarMapTupleNames [<] [<] i [<] f t = Refl
-desugarMapTupleNames (as :< (l :- a)) (fresh :< freshIn) i (prfs :< prf) f t =
- cong (:< l) $ desugarMapTupleNames as fresh i prfs f t
-
-desugarMapCase [<] [<] i [<] f = [<]
-desugarMapCase (as :< (l :- a)) (fresh :< freshIn) i (prfs :< prf) f =
- (:<)
- (desugarMapCase as fresh i prfs f)
- (l :- ("_eta" ** Inj meta l (desugarMap a i prf (thin (Drop Id) f) (Var meta (%% "_eta")))))
- @{rewrite desugarMapCaseNames as fresh i prfs f in freshIn}
-
-desugarMapCaseNames [<] [<] i [<] f = Refl
-desugarMapCaseNames (as :< (l :- a)) (fresh :< freshIn) i (prfs :< prf) f =
- cong (:< l) $ desugarMapCaseNames as fresh i prfs f
-
--- Desugar Terms ---------------------------------------------------------------
-
-desugarSynths :
- (len : LengthOf tyCtx) =>
- {t : Term Sugar m tyCtx tmCtx} ->
- (0 _ : Synths tyEnv tmEnv t a) ->
- Term NoSugar m tyCtx tmCtx
-desugarChecks :
- LengthOf tyCtx =>
- {t : Term Sugar m tyCtx tmCtx} ->
- (0 _ : Checks tyEnv tmEnv a t) ->
- Term NoSugar m tyCtx tmCtx
-desugarCheckSpine :
- LengthOf tyCtx =>
- {ts : List (Term Sugar m tyCtx tmCtx)} ->
- (0 _ : CheckSpine tyEnv tmEnv a ts b) ->
- List (Term NoSugar m tyCtx tmCtx)
-desugarAllSynths :
- LengthOf tyCtx =>
- {ts : Context (Term Sugar m tyCtx tmCtx)} ->
- (0 _ : AllSynths tyEnv tmEnv ts as) ->
- Context (Term NoSugar m tyCtx tmCtx)
-desugarAllChecks :
- LengthOf tyCtx =>
- {ts : Context (Term Sugar m tyCtx tmCtx)} ->
- (0 _ : AllChecks tyEnv tmEnv as ts) ->
- Context (Term NoSugar m tyCtx tmCtx)
-desugarAllBranches :
- LengthOf tyCtx =>
- {ts : Context (x ** Term Sugar m tyCtx (tmCtx :< x))} ->
- (0 _ : AllBranches tyEnv tmEnv as a ts) ->
- Context (x ** Term NoSugar m tyCtx (tmCtx :< x))
-desugarAllSynthsNames :
- (0 len : LengthOf tyCtx) =>
- {ts : Context (Term Sugar m tyCtx tmCtx)} ->
- (0 prfs : AllSynths tyEnv tmEnv ts as) ->
- (desugarAllSynths prfs).names = ts.names
-desugarAllChecksNames :
- (0 len : LengthOf tyCtx) =>
- {ts : Context (Term Sugar m tyCtx tmCtx)} ->
- (0 prfs : AllChecks tyEnv tmEnv as ts) ->
- (desugarAllChecks prfs).names = ts.names
-desugarAllBranchesNames :
- (0 len : LengthOf tyCtx) =>
- {ts : Context (x ** Term Sugar m tyCtx (tmCtx :< x))} ->
- (0 prfs : AllBranches tyEnv tmEnv as a ts) ->
- (desugarAllBranches prfs).names = ts.names
-
-desugarSynths (AnnotS {meta, a} wf prf) = Annot meta (desugarChecks prf) a
-desugarSynths (VarS {meta, i}) = Var meta i
-desugarSynths (LetS {meta, x} prf1 prf2) = Let meta (desugarSynths prf1) (x ** desugarSynths prf2)
-desugarSynths (LetTyS {meta, a, x} wf prf) = LetTy meta a (x ** desugarSynths prf)
-desugarSynths (AppS {meta} prf prfs) = App meta (desugarSynths prf) (desugarCheckSpine prfs)
-desugarSynths (TupS {meta, es} prfs) =
- Tup meta (MkRow (desugarAllSynths prfs) (rewrite desugarAllSynthsNames prfs in es.fresh))
-desugarSynths (PrjS {meta, l} prf i) = Prj meta (desugarSynths prf) l
-desugarSynths (UnrollS {meta} prf) = Unroll meta (desugarSynths prf)
-desugarSynths (MapS {meta, x, a, b, c} (TFix prf1 wf1) wf2 wf3) =
- Annot meta
- (Abs meta
- (["_fun", "_arg"] ** desugarMap a (%% x) prf1 (Var meta (%% "_fun")) (Var meta (%% "_arg"))))
- (TArrow (TArrow b c) (TArrow
- (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- b)) a)
- (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- c)) a)))
-
-desugarChecks (AnnotC prf1 prf2) = desugarSynths prf1
-desugarChecks (VarC prf1 prf2) = desugarSynths prf1
-desugarChecks (LetC {meta, x} prf1 prf2) = Let meta (desugarSynths prf1) (x ** desugarChecks prf2)
-desugarChecks (LetTyC {meta, a, x} wf prf) = LetTy meta a (x ** desugarChecks prf)
-desugarChecks (AbsC {meta, bound} prf1 prf2) = Abs meta (bound ** desugarChecks prf2)
-desugarChecks (AppC prf1 prf2) = desugarSynths prf1
-desugarChecks (TupC {meta, ts} prfs) =
- Tup meta (MkRow (desugarAllChecks prfs) (rewrite desugarAllChecksNames prfs in ts.fresh))
-desugarChecks (PrjC prf1 prf2) = desugarSynths prf1
-desugarChecks (InjC {meta, l} i prf) = Inj meta l (desugarChecks prf)
-desugarChecks (CaseC {meta, ts} prf prfs) =
- Case meta (desugarSynths prf)
- (MkRow (desugarAllBranches prfs) (rewrite desugarAllBranchesNames prfs in ts.fresh))
-desugarChecks (RollC {meta} prf) = Roll meta (desugarChecks prf)
-desugarChecks (UnrollC prf1 prf2) = desugarSynths prf1
-desugarChecks (FoldC {meta, y} prf1 prf2) = Fold meta (desugarSynths prf1) (y ** desugarChecks prf2)
-desugarChecks (MapC prf1 prf2) = desugarSynths prf1
-
-desugarCheckSpine [] = []
-desugarCheckSpine (prf :: prfs) = desugarChecks prf :: desugarCheckSpine prfs
-
-desugarAllSynths [<] = [<]
-desugarAllSynths ((:<) {l} prfs prf) = desugarAllSynths prfs :< (l :- desugarSynths prf)
-
-desugarAllChecks Base = [<]
-desugarAllChecks (Step {l} i prf prfs) = desugarAllChecks prfs :< (l :- desugarChecks prf)
-
-desugarAllBranches Base = [<]
-desugarAllBranches (Step {l, x} i prf prfs) = desugarAllBranches prfs :< (l :- (x ** desugarChecks prf))
-
-desugarAllSynthsNames [<] = Refl
-desugarAllSynthsNames ((:<) {l} prfs prf) = cong (:< l) $ desugarAllSynthsNames prfs
-
-desugarAllChecksNames Base = Refl
-desugarAllChecksNames (Step {l} i prf prfs) = cong (:< l) $ desugarAllChecksNames prfs
-
-desugarAllBranchesNames Base = Refl
-desugarAllBranchesNames (Step {l} i prf prfs) = cong (:< l) $ desugarAllBranchesNames prfs
-
--- Fallibly Desugar Terms ------------------------------------------------------
+ Context (x ** Term (Quote tyCtx tmCtx) m [<] (qtCtx :< x)) ->
+ f (List $ Term NoSugar m tyCtx tmCtx)
+
+desugar' (Annot meta t a) =
+ let f = \t => Annot meta t a in
+ [| f (desugar' t) |]
+desugar' (Var meta i) = pure (Var meta i)
+desugar' (Let meta e (x ** t)) =
+ let f = \e, t => Let meta e (x ** t) in
+ [| f (desugar' e) (desugar' t) |]
+desugar' (LetTy meta a (x ** t)) =
+ let f = \t => LetTy meta a (x ** t) in
+ [| f (desugar' t) |]
+desugar' (Abs meta (bound ** t)) =
+ let f = \t => Abs meta (bound ** t) in
+ [| f (desugar' t) |]
+desugar' (App meta e ts) =
+ let f = \e, ts => App meta e ts in
+ [| f (desugar' e) (desugarAll ts) |]
+desugar' (Tup meta (MkRow ts fresh)) =
+ let f = \ts => Tup meta (fromAll ts fresh) in
+ [| f (desugarCtx ts) |]
+desugar' (Prj meta e l) =
+ let f = \e => Prj meta e l in
+ [| f (desugar' e) |]
+desugar' (Inj meta l t) =
+ let f = Inj meta l in
+ [| f (desugar' t) |]
+desugar' (Case meta e (MkRow ts fresh)) =
+ let f = \e, ts => Case meta e (fromAll ts fresh) in
+ [| f (desugar' e) (desugarBranches ts) |]
+desugar' (Roll meta t) =
+ let f = Roll meta in
+ [| f (desugar' t) |]
+desugar' (Unroll meta e) =
+ let f = Unroll meta in
+ [| f (desugar' e) |]
+desugar' (Fold meta e (x ** t)) =
+ let f = \e, t => Fold meta e (x ** t) in
+ [| f (desugar' e) (desugar' t) |]
+desugar' (Map meta (x ** a) b c) = pure $ Map meta (x ** a) b c
+desugar' (QuasiQuote meta t) = quote t
+desugar' (QAbs meta (bound ** t)) = desugar' t
+desugar' (Lit meta k) = pure $ lit meta k
+desugar' (Suc meta t) =
+ let f = suc meta in
+ [| f (desugar' t) |]
+desugar' (List meta ts) =
+ let f = list meta in
+ [| f (desugarAll ts) |]
+desugar' (Cons meta t u) =
+ let f = cons meta in
+ [| f (desugar' t) (desugar' u) |]
+desugar' (Str meta str) = string meta str
+
+desugarAll [] = pure []
+desugarAll (t :: ts) = [| desugar' t :: desugarAll ts |]
+
+desugarCtx [<] = pure [<]
+desugarCtx (ts :< (l :- t)) =
+ let f = \ts, t => ts :< (l :- t) in
+ [| f (desugarCtx ts) (desugar' t) |]
+
+desugarBranches [<] = pure [<]
+desugarBranches (ts :< (l :- (x ** t))) =
+ let f = \ts, t => ts :< (l :- (x ** t)) in
+ [| f (desugarBranches ts) (desugar' t) |]
+
+quote (Annot meta t a) =
+ let f = \t, a => Roll meta $ Inj meta "Annot" $ Tup meta [<"Body" :- t, "Ty" :- a] in
+ [| f (quote t) (desugar' a) |]
+quote (Var meta i) = pure $ Roll meta $ Inj meta "Var" $ lit meta (elemToNat i.pos)
+quote (Let meta e (x ** t)) =
+ let
+ f = \e, t =>
+ Roll meta.value $ Inj meta.value "Let" $
+ Tup meta.value [<"Value" :- e, "Body" :- t]
+ in
+ [| f (quote e) (quote t) |]
+quote (Abs meta (bound ** t)) =
+ let
+ f = \t => Roll meta $ Inj meta "Abs" $
+ Tup meta [<"Bound" :- lit meta (length bound), "Body" :- t]
+ in
+ [| f (quote t) |]
+quote (App meta e ts) =
+ let
+ f = \e, ts =>
+ Roll meta $ Inj meta "App" $
+ Tup meta [<"Fun" :- e, "Args" :- list meta ts]
+ in
+ [| f (quote e) (quoteAll ts) |]
+quote (Tup meta (MkRow ts _)) =
+ let f = Roll meta . Inj meta "Tup" . list meta in
+ [| f (quoteCtx ts) |]
+quote (Prj meta e l) =
+ let f = \e, l => Roll meta $ Inj meta "Prj" $ Tup meta [<"Target" :- e, "Label" :- l] in
+ [| f (quote e) (string meta l) |]
+quote (Inj meta l t) =
+ let f = \t, l => Roll meta $ Inj meta "Inj" $ Tup meta [<"Value" :- t, "Label" :- l] in
+ [| f (quote t) (string meta l) |]
+quote (Case meta e (MkRow ts _)) =
+ let
+ f = \e, ts =>
+ Roll meta $ Inj meta "Case" $
+ Tup meta [<"Target" :- e, "Branches" :- list meta ts]
+ in
+ [| f (quote e) (quoteBranches ts) |]
+quote (Roll meta t) =
+ let f = Roll meta . Inj meta "Roll" in
+ [| f (quote t) |]
+quote (Unroll meta e) =
+ let f = Roll meta . Inj meta "Unroll" in
+ [| f (quote e) |]
+quote (Fold meta e (x ** t)) =
+ let f = \e, t => Roll meta $ Inj meta "Fold" $ Tup meta [<"Target" :- e, "Body" :- t] in
+ [| f (quote e) (quote t) |]
+quote (Map meta a b c) =
+ let
+ f = \a, b, c =>
+ Roll meta $ Inj meta "Map" $
+ Tup meta [<"Functor" :- a, "Source" :- b, "Target" :- c]
+ in
+ [| f (desugar' a) (desugar' b) (desugar' c) |]
+quote (Unquote meta t) = desugar' t
+
+quoteAll [] = pure []
+quoteAll (t :: ts) = [| quote t :: quoteAll ts |]
+
+quoteCtx [<] = pure []
+quoteCtx (ts :< (l :- t)) =
+ let f = \ts, l, t => Tup meta [<"Label" :- l, "Value" :- t] :: ts in
+ [| f (quoteCtx ts) (string meta l) (quote t) |]
+
+quoteBranches [<] = pure []
+quoteBranches (ts :< (l :- (x ** t))) =
+ let f = \ts, l, t => Tup meta [<"Label" :- l, "Body" :- t] :: ts in
+ [| f (quoteBranches ts) (string meta l) (quote t) |]
export
-maybeDesugar : (len : LengthOf tyCtx) => Term Sugar m tyCtx tmCtx -> Maybe (Term NoSugar m tyCtx tmCtx)
-maybeDesugarList :
- (len : LengthOf tyCtx) =>
- List (Term Sugar m tyCtx tmCtx) -> Maybe (List $ Term NoSugar m tyCtx tmCtx)
-maybeDesugarAll :
- (len : LengthOf tyCtx) =>
- (ts : Context (Term Sugar m tyCtx tmCtx)) ->
- Maybe (All (Assoc0 $ Term NoSugar m tyCtx tmCtx) ts.names)
-maybeDesugarBranches :
- (len : LengthOf tyCtx) =>
- (ts : Context (x ** Term Sugar m tyCtx (tmCtx :< x))) ->
- Maybe (All (Assoc0 $ (x ** Term NoSugar m tyCtx (tmCtx :< x))) ts.names)
-
-maybeDesugar (Annot meta t a) = do
- t <- maybeDesugar t
- pure (Annot meta t a)
-maybeDesugar (Var meta i) = pure (Var meta i)
-maybeDesugar (Let meta e (x ** t)) = do
- e <- maybeDesugar e
- t <- maybeDesugar t
- pure (Let meta e (x ** t))
-maybeDesugar (LetTy meta a (x ** t)) = do
- t <- maybeDesugar t
- pure (LetTy meta a (x ** t))
-maybeDesugar (Abs meta (bound ** t)) = do
- t <- maybeDesugar t
- pure (Abs meta (bound ** t))
-maybeDesugar (App meta e ts) = do
- e <- maybeDesugar e
- ts <- maybeDesugarList ts
- pure (App meta e ts)
-maybeDesugar (Tup meta (MkRow ts fresh)) = do
- ts <- maybeDesugarAll ts
- pure (Tup meta (fromAll ts fresh))
-maybeDesugar (Prj meta e l) = do
- e <- maybeDesugar e
- pure (Prj meta e l)
-maybeDesugar (Inj meta l t) = do
- t <- maybeDesugar t
- pure (Inj meta l t)
-maybeDesugar (Case meta e (MkRow ts fresh)) = do
- e <- maybeDesugar e
- ts <- maybeDesugarBranches ts
- pure (Case meta e (fromAll ts fresh))
-maybeDesugar (Roll meta t) = do
- t <- maybeDesugar t
- pure (Roll meta t)
-maybeDesugar (Unroll meta e) = do
- e <- maybeDesugar e
- pure (Unroll meta e)
-maybeDesugar (Fold meta e (x ** t)) = do
- e <- maybeDesugar e
- t <- maybeDesugar t
- pure (Fold meta e (x ** t))
-maybeDesugar (Map meta (x ** a) b c) =
- case (%% x `strictlyPositiveIn` a) of
- False `Because` contra => Nothing
- True `Because` prf =>
- pure $
- Annot meta
- (Abs meta
- (["_fun", "_arg"] ** desugarMap a (%% x) prf (Var meta (%% "_fun")) (Var meta (%% "_arg"))))
- (TArrow (TArrow b c) (TArrow
- (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- b)) a)
- (sub (tabulate len (\i => _ :- TVar (toVar i)) :< (x :- c)) a)))
-
-maybeDesugarList [] = pure []
-maybeDesugarList (t :: ts) = [| maybeDesugar t :: maybeDesugarList ts |]
-
-maybeDesugarAll [<] = pure [<]
-maybeDesugarAll (ts :< (l :- t)) = do
- ts <- maybeDesugarAll ts
- t <- maybeDesugar t
- pure (ts :< (l :- t))
-
-maybeDesugarBranches [<] = pure [<]
-maybeDesugarBranches (ts :< (l :- (x ** t))) = do
- ts <- maybeDesugarBranches ts
- t <- maybeDesugar t
- pure (ts :< (l :- (x ** t)))
+desugar : Term (Sugar qtCtx) m tyCtx tmCtx -> Term NoSugar m tyCtx tmCtx
+desugar t =
+ let
+ cache : Cache String
+ cache = MkCache {max = 0, vals = empty}
+ in
+ evalState cache (desugar' t)
diff --git a/src/Inky/Term/Parser.idr b/src/Inky/Term/Parser.idr
index 1f9d983..e977bc2 100644
--- a/src/Inky/Term/Parser.idr
+++ b/src/Inky/Term/Parser.idr
@@ -18,7 +18,6 @@ import Flap.Parser
import Inky.Data.Row
import Inky.Term
-import Inky.Term.Sugar
import Inky.Type
import Text.Lexer
@@ -29,6 +28,7 @@ export
data InkyKind
= TermIdent
| TypeIdent
+ | StringLit
| Lit
| Let
| In
@@ -52,8 +52,10 @@ data InkyKind
| BraceClose
| Arrow
| DoubleArrow
+ | WaveArrow
| Bang
| Tilde
+ | Backtick
| Dot
| Backslash
| Colon
@@ -64,9 +66,10 @@ data InkyKind
| Comment
export
-[EqI] Eq InkyKind where
+Eq InkyKind where
TermIdent == TermIdent = True
TypeIdent == TypeIdent = True
+ StringLit == StringLit = True
Lit == Lit = True
Let == Let = True
In == In = True
@@ -90,8 +93,10 @@ export
BraceClose == BraceClose = True
Arrow == Arrow = True
DoubleArrow == DoubleArrow = True
+ WaveArrow == WaveArrow = True
Bang == Bang = True
Tilde == Tilde = True
+ Backtick == Backtick = True
Dot == Dot = True
Backslash == Backslash = True
Colon == Colon = True
@@ -106,6 +111,7 @@ export
Interpolation InkyKind where
interpolate TermIdent = "term name"
interpolate TypeIdent = "type name"
+ interpolate StringLit = "string"
interpolate Lit = "number"
interpolate Let = "'let'"
interpolate In = "'in'"
@@ -129,8 +135,10 @@ Interpolation InkyKind where
interpolate BraceClose = "'}'"
interpolate Arrow = "'->'"
interpolate DoubleArrow = "'=>'"
+ interpolate WaveArrow = "'~>'"
interpolate Bang = "'!'"
interpolate Tilde = "'~'"
+ interpolate Backtick = "'`'"
interpolate Dot = "'.'"
interpolate Backslash = "'\\'"
interpolate Colon = "':'"
@@ -143,12 +151,14 @@ Interpolation InkyKind where
TokenKind InkyKind where
TokType TermIdent = String
TokType TypeIdent = String
+ TokType StringLit = String
TokType Lit = Nat
TokType Comment = String
TokType _ = ()
tokValue TermIdent = id
tokValue TypeIdent = id
+ tokValue StringLit = \str => substr 1 (length str `minus` 2) str
tokValue Lit = stringToNatOrZ
tokValue Let = const ()
tokValue In = const ()
@@ -172,8 +182,10 @@ TokenKind InkyKind where
tokValue BraceClose = const ()
tokValue Arrow = const ()
tokValue DoubleArrow = const ()
+ tokValue WaveArrow = const ()
tokValue Bang = const ()
tokValue Tilde = const ()
+ tokValue Backtick = const ()
tokValue Dot = const ()
tokValue Backslash = const ()
tokValue Colon = const ()
@@ -201,7 +213,7 @@ keywords =
export
relevant : InkyKind -> Bool
-relevant = (/=) @{EqI} Ignore
+relevant = (/=) Ignore
public export
InkyToken : Type
@@ -228,7 +240,8 @@ tokenMap =
Just k => Tok k s
Nothing => Tok TypeIdent s)] ++
toTokenMap
- [ (digits, Lit)
+ [ (quote (is '"') alpha, StringLit)
+ , (digits, Lit)
, (exact "(", ParenOpen)
, (exact ")", ParenClose)
, (exact "[", BracketOpen)
@@ -239,8 +252,10 @@ tokenMap =
, (exact "}", BraceClose)
, (exact "->", Arrow)
, (exact "=>", DoubleArrow)
+ , (exact "~>", WaveArrow)
, (exact "!", Bang)
, (exact "~", Tilde)
+ , (exact "`", Backtick)
, (exact ".", Dot)
, (exact "\\", Backslash)
, (exact ":", Colon)
@@ -249,6 +264,43 @@ tokenMap =
, (exact ",", Comma)
]
+-- Error Monad -----------------------------------------------------------------
+
+public export
+data Result : (a : Type) -> Type where
+ Ok : a -> Result a
+ Errs : (msgs : List1 (WithBounds String)) -> Result a
+
+export
+Functor Result where
+ map f (Ok x) = Ok (f x)
+ map f (Errs msgs) = Errs msgs
+
+export
+Applicative Result where
+ pure = Ok
+
+ Ok f <*> Ok x = Ok (f x)
+ Ok f <*> Errs msgs = Errs msgs
+ Errs msgs <*> Ok x = Errs msgs
+ Errs msgs1 <*> Errs msgs2 = Errs (msgs1 ++ msgs2)
+
+export
+Monad Result where
+ Ok x >>= f = f x
+ Errs msgs >>= f = Errs msgs
+
+ join (Ok x) = x
+ join (Errs msgs) = Errs msgs
+
+export
+extendResult : Row a -> WithBounds (Assoc (Result a)) -> Result (Row a)
+extendResult row x =
+ case (isFresh row.names x.val.name) of
+ True `Because` prf => Ok ((:<) row (x.val.name :- !x.val.value) @{prf})
+ False `Because` _ =>
+ [| const (Errs $ singleton $ "duplicate name \"\{x.val.name}\"" <$ x) x.val.value |]
+
-- Parser ----------------------------------------------------------------------
public export
@@ -260,35 +312,41 @@ InkyParser nil locked free a =
a
public export
-record ParseFun (0 n : Nat) (0 p : Fun (replicate n $ SnocList String) Type) where
+record ParseFun (as : SnocList Type) (0 p : Fun as Type) where
constructor MkParseFun
- try :
- DFun (replicate n $ SnocList String)
- (chain (lengthOfReplicate n $ SnocList String) (Either String) p)
+ try : DFun as (chain (lengthOf as) Parser.Result p)
-mkVar : ({ctx : _} -> Var ctx -> p ctx) -> WithBounds String -> ParseFun 1 p
+mkVar : ({ctx : _} -> Var ctx -> p ctx) -> WithBounds String -> ParseFun [<SnocList String] p
mkVar f x =
MkParseFun
(\ctx => case Var.lookup x.val ctx of
- Just i => pure (f i)
- Nothing => Left "\{x.bounds}: unbound name \"\{x.val}\"")
-
-mkVar2 :
- ({tyCtx, tmCtx : _} -> WithBounds (Var tmCtx) -> p tyCtx tmCtx) ->
- WithBounds String -> ParseFun 2 p
-mkVar2 f x =
+ Just i => Ok (f i)
+ Nothing => Errs (singleton $ "unbound name \"\{x.val}\"" <$ x))
+
+mkVar3 :
+ ({ctx1 : a} -> {ctx2 : b} -> {ctx3 : SnocList String} ->
+ WithBounds (Var ctx3) ->
+ p ctx1 ctx2 ctx3) ->
+ WithBounds String -> ParseFun [<a, b, SnocList String] p
+mkVar3 f x =
MkParseFun
- (\tyCtx, tmCtx => case Var.lookup x.val tmCtx of
- Just i => pure (f $ i <$ x)
- Nothing => Left "\{x.bounds}: unbound name \"\{x.val}\"")
+ (\ctx1, ctx2, ctx3 => case Var.lookup x.val ctx3 of
+ Just i => Ok (f $ i <$ x)
+ Nothing => Errs (singleton $ "unbound name \"\{x.val}\"" <$ x))
public export
TypeFun : Type
-TypeFun = ParseFun 1 Ty
+TypeFun = ParseFun [<SnocList String] Ty
+
+Type'Fun : Type
+Type'Fun = ParseFun [<Mode, SnocList String, SnocList String] (\mode => Ty' mode Bounds)
+
+BoundType'Fun : Type
+BoundType'Fun = ParseFun [<Mode, SnocList String, SnocList String] (\mode => BoundTy' mode Bounds)
public export
TermFun : Type
-TermFun = ParseFun 2 (Term Sugar Bounds)
+TermFun = ParseFun [<Mode, SnocList String, SnocList String] (\mode => Term mode Bounds)
public export
TypeParser : SnocList String -> SnocList String -> Type
@@ -299,36 +357,41 @@ RowOf :
(0 free : Context Type) ->
InkyParser False [<] free a ->
InkyParser True [<] free (List $ WithBounds $ Assoc a)
-RowOf free p = sepBy (match Comma) (WithBounds $ mkAssoc <$> Seq [match TypeIdent, match Colon, p])
+RowOf free p =
+ sepBy (match Semicolon) (WithBounds $ mkAssoc <$> Seq [match TypeIdent, match Colon, p])
where
mkAssoc : HList [String, (), a] -> Assoc a
mkAssoc [x, _, v] = x :- v
-tryRow :
- List (WithBounds $ Assoc (ParseFun 1 p)) ->
- (ctx : _) -> Either String (Row $ p ctx)
-tryRow xs ctx =
- foldlM
- (\row, xf => do
- a <- xf.val.value.try ctx
- let Just row' = extend row (xf.val.name :- a)
- | Nothing => Left "\{xf.bounds}: duplicate name \"\{xf.val.name}\""
- pure row')
- [<]
- xs
-
-tryRow2 :
- List (WithBounds $ Assoc (ParseFun 2 p)) ->
- (tyCtx, tmCtx : _) -> Either String (Row $ p tyCtx tmCtx)
-tryRow2 xs tyCtx tmCtx =
- foldlM
- (\row, xf => do
- a <- xf.val.value.try tyCtx tmCtx
- let Just row' = extend row (xf.val.name :- a)
- | Nothing => Left "\{xf.bounds}: duplicate name \"\{xf.val.name}\""
- pure row')
- [<]
- xs
+parseRow :
+ List (WithBounds $ Assoc (ParseFun [<a] p)) ->
+ ParseFun [<a] (Row . p)
+parseRow xs =
+ MkParseFun (\ctx =>
+ foldlM
+ (\row => extendResult row . map (\(n :- x) => n :- x.try ctx))
+ [<]
+ xs)
+
+parseRow3 :
+ List (WithBounds $ Assoc (ParseFun [<a,b,c] p)) ->
+ ParseFun [<a, b, c] (\ctx1, ctx2, ctx3 => Row $ p ctx1 ctx2 ctx3)
+parseRow3 xs =
+ MkParseFun (\ctx1, ctx2, ctx3 =>
+ foldlM
+ (\row => extendResult row . map (\(n :- x) => n :- x.try ctx1 ctx2 ctx3))
+ [<]
+ xs)
+
+parseList3 :
+ List (ParseFun [<a,b,c] p) ->
+ ParseFun [<a, b, c] (\ctx1, ctx2, ctx3 => List $ p ctx1 ctx2 ctx3)
+parseList3 [] = MkParseFun (\ctx1, ctx2, ctx3 => Ok [])
+parseList3 (x :: xs) =
+ MkParseFun (\ctx1, ctx2, ctx3 =>
+ [| x.try ctx1 ctx2 ctx3 :: (parseList3 xs).try ctx1 ctx2 ctx3 |])
+
+-- Types -----------------------------------------------------------------------
OpenOrFixpointType : TypeParser [<] [<"openType"]
OpenOrFixpointType =
@@ -339,13 +402,13 @@ OpenOrFixpointType =
]
where
mkFix : HList [(), String, (), TypeFun] -> TypeFun
- mkFix [_, x, _, a] = MkParseFun (\ctx => pure $ TFix x !(a.try (ctx :< x)))
+ mkFix [_, x, _, a] = MkParseFun (\ctx => TFix x <$> a.try (ctx :< x))
AtomType : TypeParser [<"openType"] [<]
AtomType =
OneOf
[ mkVar TVar <$> WithBounds (match TypeIdent)
- , MkParseFun (\_ => pure TNat) <$ match Nat
+ , MkParseFun (\_ => Ok TNat) <$ match Nat
, mkProd <$> enclose (match AngleOpen) (match AngleClose) row
, mkSum <$> enclose (match BracketOpen) (match BracketClose) row
, enclose (match ParenOpen) (match ParenClose) OpenOrFixpointType
@@ -355,10 +418,10 @@ AtomType =
row = RowOf [<"openType" :- TypeFun] $ Var (%%% "openType")
mkProd : List (WithBounds $ Assoc TypeFun) -> TypeFun
- mkProd xs = MkParseFun (\ctx => TProd <$> tryRow xs ctx)
+ mkProd xs = MkParseFun (\ctx => TProd <$> (parseRow xs).try ctx)
mkSum : List (WithBounds $ Assoc TypeFun) -> TypeFun
- mkSum xs = MkParseFun (\ctx => TSum <$> tryRow xs ctx)
+ mkSum xs = MkParseFun (\ctx => TSum <$> (parseRow xs).try ctx)
AppType : TypeParser [<"openType"] [<]
AppType =
@@ -380,54 +443,116 @@ OpenType =
foldr1 {a = TypeFun}
(\x, y => MkParseFun (\ctx => [| TArrow (x.try ctx) (y.try ctx) |]))
+export
+[ListSet] Eq a => Set a (List a) where
+ singleton x = [x]
+
+ member x xs = elem x xs
+
+ intersect xs = filter (\x => elem x xs)
+
+ toList = id
+
%hint
export
-OpenTypeWf : So (wellTyped EqI [<] [<] [<] [<] OpenType)
-OpenTypeWf = Oh
+OpenTypeWf : collectTypeErrs @{ListSet} [<] [<] [<] [<] OpenType = []
+OpenTypeWf = Refl
-- Terms -----------------------------------------------------------------------
+NoSugarMsg : String
+NoSugarMsg = "sugar is not allowed here"
+
+NoUnquoteMsg : String
+NoUnquoteMsg = "cannot unquote outside of quote"
+
+NoQuoteMsg : String
+NoQuoteMsg = "cannot quote inside of quote"
+
+NoQuoteTypesMsg : String
+NoQuoteTypesMsg = "cannot quote types"
+
+NoLetTyMsg : String
+NoLetTyMsg = "cannot bind type inside of quote"
+
+NoQAbsMsg : String
+NoQAbsMsg = "cannot bind term name inside of quote"
+
AtomTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
AtomTerm =
OneOf
- [ mkVar2 (\x => Var x.bounds x.val) <$> WithBounds (match TermIdent)
+ [ mkVar3 (\x => Var x.bounds x.val) <$> WithBounds (match TermIdent)
+ , mkStrLit <$> WithBounds (match StringLit)
, mkLit <$> WithBounds (match Lit)
, mkList <$> WithBounds (
enclose (match BracketOpen) (match BracketClose) $
- sepBy (match Comma) $
+ sepBy (match Semicolon) $
Var (%%% "openTerm"))
, mkTup <$> WithBounds (enclose (match AngleOpen) (match AngleClose) $
RowOf [<"openTerm" :- TermFun] (Var (%%% "openTerm")))
, enclose (match ParenOpen) (match ParenClose) (Var (%%% "openTerm"))
]
where
+ mkStrLit : WithBounds String -> TermFun
+ mkStrLit k = MkParseFun (\mode, tyCtx, tmCtx =>
+ case mode of
+ NoSugar => Errs (singleton $ NoSugarMsg <$ k)
+ Sugar qtCtx => Ok (Str k.bounds k.val)
+ Quote ctx1 ctx2 => Errs (singleton $ NoSugarMsg <$ k))
+
mkLit : WithBounds Nat -> TermFun
- mkLit k = MkParseFun (\tyCtx, tmCtx => pure (Lit k.bounds k.val))
+ mkLit k = MkParseFun (\mode, tyCtx, tmCtx =>
+ case mode of
+ NoSugar => Errs (singleton $ NoSugarMsg <$ k)
+ Sugar qtCtx => Ok (Lit k.bounds k.val)
+ Quote ctx1 ctx2 => Errs (singleton $ NoSugarMsg <$ k))
mkList : WithBounds (List TermFun) -> TermFun
- mkList xs =
- MkParseFun (\tyCtx, tmCtx =>
- foldr
- (\x, ys => pure $ Cons xs.bounds !(x.try tyCtx tmCtx) !ys)
- (pure $ Nil xs.bounds)
- xs.val)
+ mkList xs = MkParseFun (\mode, tyCtx, tmCtx =>
+ case mode of
+ NoSugar => Errs (singleton $ NoSugarMsg <$ xs)
+ Sugar ctx => List xs.bounds <$> (parseList3 xs.val).try (Sugar ctx) tyCtx tmCtx
+ Quote ctx1 ctx2 => Errs (singleton $ NoSugarMsg <$ xs))
mkTup : WithBounds (List (WithBounds $ Assoc TermFun)) -> TermFun
- mkTup xs = MkParseFun (\tyCtx, tmCtx => Tup xs.bounds <$> tryRow2 xs.val tyCtx tmCtx)
+ mkTup xs =
+ MkParseFun (\mode, tyCtx, tmCtx =>
+ Tup xs.bounds <$> (parseRow3 xs.val).try mode tyCtx tmCtx)
PrefixTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
PrefixTerm =
Fix "prefixTerm" $ OneOf
[ mkRoll <$> WithBounds (match Tilde **> Var (%%% "prefixTerm"))
, mkUnroll <$> WithBounds (match Bang **> Var (%%% "prefixTerm"))
+ , mkQuote <$> WithBounds (match Backtick **> Var (%%% "prefixTerm"))
+ , mkUnquote <$> WithBounds (match Comma **> Var (%%% "prefixTerm"))
, rename (Drop Id) Id AtomTerm
]
where
mkRoll : WithBounds TermFun -> TermFun
- mkRoll x = MkParseFun (\tyCtx, tmCtx => pure $ Roll x.bounds !(x.val.try tyCtx tmCtx))
+ mkRoll x = MkParseFun (\mode, tyCtx, tmCtx => Roll x.bounds <$> x.val.try mode tyCtx tmCtx)
mkUnroll : WithBounds TermFun -> TermFun
- mkUnroll x = MkParseFun (\tyCtx, tmCtx => pure $ Unroll x.bounds !(x.val.try tyCtx tmCtx))
+ mkUnroll x = MkParseFun (\mode, tyCtx, tmCtx => Unroll x.bounds <$> x.val.try mode tyCtx tmCtx)
+
+ mkQuote : WithBounds TermFun -> TermFun
+ mkQuote x =
+ MkParseFun (\mode, tyCtx, tmCtx =>
+ case mode of
+ Quote ctx1 ctx2 => Errs (singleton $ NoQuoteMsg <$ x)
+ Sugar ctx => QuasiQuote x.bounds <$> x.val.try (Quote tyCtx tmCtx) [<] ctx
+ NoSugar => Errs (singleton $ NoSugarMsg <$ x))
+
+ mkUnquote : WithBounds TermFun -> TermFun
+ mkUnquote x =
+ MkParseFun (\mode, tyCtx, tmCtx =>
+ case mode of
+ Quote ctx1 ctx2 =>
+ case tyCtx of
+ [<] => Unquote x.bounds <$> x.val.try (Sugar tmCtx) ctx1 ctx2
+ _ => Errs (singleton $ "internal error 0001" <$ x)
+ Sugar ctx => Errs (singleton $ NoUnquoteMsg <$ x)
+ NoSugar => Errs (singleton $ NoSugarMsg <$ x))
SuffixTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
SuffixTerm = mkSuffix <$> Seq [ PrefixTerm , star (match Dot **> WithBounds (match TypeIdent)) ]
@@ -435,8 +560,59 @@ SuffixTerm = mkSuffix <$> Seq [ PrefixTerm , star (match Dot **> WithBounds (mat
mkSuffix : HList [TermFun, List (WithBounds String)] -> TermFun
mkSuffix [t, []] = t
mkSuffix [t, prjs] =
- MkParseFun (\tyCtx, tmCtx =>
- pure $ foldl (\acc, l => Prj l.bounds acc l.val) !(t.try tyCtx tmCtx) prjs)
+ MkParseFun (\mode, tyCtx, tmCtx =>
+ Ok $ foldl (\acc, l => Prj l.bounds acc l.val) !(t.try mode tyCtx tmCtx) prjs)
+
+SuffixTy' : InkyParser False [<"openTerm" :- TermFun] [<] Type'Fun
+SuffixTy' =
+ OneOf
+ [ mkTy <$> WithBounds (sub [<"openType" :- rename Id (Drop Id) OpenType] [<] AtomType)
+ , mkTm <$> WithBounds (match Comma **> weaken (S Z) PrefixTerm)
+ ]
+ where
+ mkTy : WithBounds TypeFun -> Type'Fun
+ mkTy x =
+ MkParseFun (\mode, tyCtx, tmCtx =>
+ case mode of
+ Quote ctx1 ctx2 => Errs (singleton $ NoQuoteTypesMsg <$ x)
+ Sugar ctx => x.val.try tyCtx
+ NoSugar => x.val.try tyCtx)
+
+ mkTm : WithBounds TermFun -> Type'Fun
+ mkTm x =
+ MkParseFun (\mode, tyCtx, tmCtx =>
+ case mode of
+ Quote ctx1 ctx2 => x.val.try (Sugar tmCtx) ctx1 ctx2
+ Sugar ctx => Errs (singleton $ NoUnquoteMsg <$ x)
+ NoSugar => Errs (singleton $ NoSugarMsg <$ x))
+
+SuffixBoundTy' : InkyParser False [<"openTerm" :- TermFun] [<] BoundType'Fun
+SuffixBoundTy' =
+ OneOf
+ [ mkTy <$> enclose (match ParenOpen) (match ParenClose) (Seq
+ [ WithBounds (match Backslash)
+ , match TypeIdent
+ , match DoubleArrow
+ , rename Id (Drop Id) OpenType
+ ])
+ , mkTm <$> WithBounds (match Comma **> weaken (S Z) PrefixTerm)
+ ]
+ where
+ mkTy : HList [WithBounds _, String, _, TypeFun] -> BoundType'Fun
+ mkTy [x, n, _, a] =
+ MkParseFun (\mode, tyCtx, tmCtx =>
+ case mode of
+ Quote ctx1 ctx2 => Errs (singleton $ NoQuoteTypesMsg <$ x)
+ Sugar ctx => MkDPair n <$> a.try (tyCtx :< n)
+ NoSugar => MkDPair n <$> a.try (tyCtx :< n))
+
+ mkTm : WithBounds TermFun -> BoundType'Fun
+ mkTm x =
+ MkParseFun (\mode, tyCtx, tmCtx =>
+ case mode of
+ Quote ctx1 ctx2 => x.val.try (Sugar tmCtx) ctx1 ctx2
+ Sugar ctx => Errs (singleton $ NoUnquoteMsg <$ x)
+ NoSugar => Errs (singleton $ NoSugarMsg <$ x))
AppTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
AppTerm =
@@ -459,14 +635,9 @@ AppTerm =
[ WithBounds SuffixTerm
, mkMap <$> Seq
[ WithBounds (match Map)
- , enclose (match ParenOpen) (match ParenClose) $ Seq
- [ match Backslash
- , match TypeIdent
- , match DoubleArrow
- , rename Id (Drop Id) OpenType
- ]
- , sub [<"openType" :- rename Id (Drop Id) OpenType] [<] AtomType
- , sub [<"openType" :- rename Id (Drop Id) OpenType] [<] AtomType
+ , weaken (S Z) SuffixBoundTy'
+ , weaken (S Z) SuffixTy'
+ , weaken (S Z) SuffixTy'
]
]
, star (weaken (S Z) SuffixTerm)
@@ -474,44 +645,82 @@ AppTerm =
]
where
mkInj : HList [WithBounds String, TermFun] -> TermFun
- mkInj [tag, t] = MkParseFun (\tyCtx, tmCtx => Inj tag.bounds tag.val <$> t.try tyCtx tmCtx)
+ mkInj [tag, t] =
+ MkParseFun (\mode, tyCtx, tmCtx =>
+ Inj tag.bounds tag.val <$> t.try mode tyCtx tmCtx)
mkSuc : HList [WithBounds _, TermFun] -> TermFun
- mkSuc [x, t] = MkParseFun (\tyCtx, tmCtx => Suc x.bounds <$> t.try tyCtx tmCtx)
+ mkSuc [x, t] =
+ MkParseFun (\mode, tyCtx, tmCtx =>
+ case mode of
+ Quote ctx1 ctx2 => Errs (singleton $ NoSugarMsg <$ x)
+ Sugar ctx => Suc x.bounds <$> t.try (Sugar ctx) tyCtx tmCtx
+ NoSugar => Errs (singleton $ NoSugarMsg <$ x))
mkCons : HList [WithBounds _, TermFun, TermFun] -> TermFun
mkCons [x, t, u] =
- MkParseFun (\tyCtx, tmCtx =>
- pure $ Cons x.bounds !(t.try tyCtx tmCtx) !(u.try tyCtx tmCtx))
-
- mkMap : HList [WithBounds (), HList [_, String, _, TypeFun], TypeFun, TypeFun] -> WithBounds TermFun
- mkMap [m, [_, x, _, a], b, c] =
- MkParseFun (\tyCtx, tmCtx =>
- pure $ Map m.bounds (x ** !(a.try (tyCtx :< x))) !(b.try tyCtx) !(c.try tyCtx))
+ MkParseFun (\mode, tyCtx, tmCtx =>
+ case mode of
+ Quote ctx1 ctx2 => Errs (singleton $ NoSugarMsg <$ x)
+ Sugar ctx =>
+ [| Cons (pure x.bounds)
+ (t.try (Sugar ctx) tyCtx tmCtx)
+ (u.try (Sugar ctx) tyCtx tmCtx)
+ |]
+ NoSugar => Errs (singleton $ NoSugarMsg <$ x))
+
+ mkMap :
+ HList [WithBounds (), BoundType'Fun, Type'Fun, Type'Fun] ->
+ WithBounds TermFun
+ mkMap [m, a, b, c] =
+ MkParseFun (\mode, tyCtx, tmCtx => do
+ (a, b, c) <-
+ [| (a.try mode tyCtx tmCtx, [|(b.try mode tyCtx tmCtx, c.try mode tyCtx tmCtx)|]) |]
+ Ok $ Map m.bounds a b c)
<$ m
mkApp : HList [WithBounds TermFun, List TermFun] -> TermFun
mkApp [t, []] = t.val
- mkApp [fun, (arg :: args)] =
- MkParseFun (\tyCtx, tmCtx =>
- pure $
- App
- fun.bounds
- !(fun.val.try tyCtx tmCtx)
- ( !(arg.try tyCtx tmCtx)
- :: (!(foldlM (\acc, arg => pure $ acc :< !(arg.try tyCtx tmCtx)) [<] args) <>> [])))
+ mkApp [fun, args] =
+ MkParseFun (\mode, tyCtx, tmCtx => do
+ (funVal, args) <-
+ [| (fun.val.try mode tyCtx tmCtx, (parseList3 args).try mode tyCtx tmCtx) |]
+ Ok $ App fun.bounds funVal args)
+
+OpenTy' : InkyParser False [<"openTerm" :- TermFun] [<] Type'Fun
+OpenTy' =
+ OneOf
+ [ mkTy <$> WithBounds (rename (Drop Id) Id OpenType)
+ , mkTm <$> WithBounds (match Comma **> weaken (S Z) PrefixTerm)
+ ]
+ where
+ mkTy : WithBounds TypeFun -> Type'Fun
+ mkTy x =
+ MkParseFun (\mode, tyCtx, tmCtx =>
+ case mode of
+ Quote ctx1 ctx2 => Errs (singleton $ NoQuoteTypesMsg <$ x)
+ Sugar ctx => x.val.try tyCtx
+ NoSugar => x.val.try tyCtx)
+
+ mkTm : WithBounds TermFun -> Type'Fun
+ mkTm x =
+ MkParseFun (\mode, tyCtx, tmCtx =>
+ case mode of
+ Quote ctx1 ctx2 => x.val.try (Sugar tmCtx) ctx1 ctx2
+ Sugar ctx => Errs (singleton $ NoUnquoteMsg <$ x)
+ NoSugar => Errs (singleton $ NoSugarMsg <$ x))
AnnotTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
AnnotTerm =
mkAnnot <$> Seq
[ AppTerm
- , option (match Colon **> WithBounds (rename Id (Drop Id) OpenType))
+ , option (match Colon **> WithBounds (weaken (S Z) OpenTy'))
]
where
- mkAnnot : HList [TermFun, Maybe (WithBounds TypeFun)] -> TermFun
+ mkAnnot : HList [TermFun, Maybe (WithBounds Type'Fun)] -> TermFun
mkAnnot [t, Nothing] = t
- mkAnnot [t, Just a] = MkParseFun (\tyCtx, tmCtx =>
- pure $ Annot a.bounds !(t.try tyCtx tmCtx) !(a.val.try tyCtx))
+ mkAnnot [t, Just a] = MkParseFun (\mode, tyCtx, tmCtx =>
+ [| Annot (pure a.bounds) (t.try mode tyCtx tmCtx) (a.val.try mode tyCtx tmCtx) |])
-- Open Terms
@@ -524,9 +733,9 @@ LetTerm =
, OneOf
[ mkAnnot <$> Seq
[ star (enclose (match ParenOpen) (match ParenClose) $
- Seq [ match TermIdent, match Colon, rename Id (Drop Id) OpenType ])
+ Seq [ match TermIdent, match Colon, weaken (S Z) OpenTy' ])
, WithBounds (match Colon)
- , rename Id (Drop Id) OpenType
+ , weaken (S Z) OpenTy'
, match Equal
, star (match Comment)
, Var (%%% "openTerm")]
@@ -547,38 +756,74 @@ LetTerm =
where
mkLet : HList [WithBounds String, WithDoc TermFun, (), TermFun] -> TermFun
mkLet [x, AddDoc e doc, _, t] =
- MkParseFun (\tyCtx, tmCtx =>
- pure $
- Let (AddDoc x.bounds doc) !(e.try tyCtx tmCtx) (x.val ** !(t.try tyCtx (tmCtx :< x.val))))
+ MkParseFun (\mode, tyCtx, tmCtx =>
+ [| (\e, t => Let (AddDoc x.bounds doc) e (x.val ** t))
+ (e.try mode tyCtx tmCtx)
+ (t.try mode tyCtx (tmCtx :< x.val))
+ |])
mkLetType : HList [WithBounds String, (), List String, TypeFun, (), TermFun] -> TermFun
mkLetType [x, _, doc, a, _, t] =
- MkParseFun (\tyCtx, tmCtx =>
- pure $
- LetTy (AddDoc x.bounds doc) !(a.try tyCtx) (x.val ** !(t.try (tyCtx :< x.val) tmCtx)))
-
- mkArrow : List TypeFun -> TypeFun -> TypeFun
- mkArrow [] cod = cod
- mkArrow (arg :: args) cod =
- MkParseFun (\ctx => [| TArrow (arg.try ctx) ((mkArrow args cod).try ctx) |])
+ MkParseFun (\mode, tyCtx, tmCtx =>
+ case mode of
+ Quote ctx1 ctx2 => Errs (singleton $ NoLetTyMsg <$ x)
+ Sugar ctx =>
+ [| (\a, t => LetTy (AddDoc x.bounds doc) a (x.val ** t))
+ (a.try tyCtx)
+ (t.try (Sugar ctx) (tyCtx :< x.val) tmCtx)
+ |]
+ NoSugar =>
+ [| (\a, t => LetTy (AddDoc x.bounds doc) a (x.val ** t))
+ (a.try tyCtx)
+ (t.try NoSugar (tyCtx :< x.val) tmCtx)
+ |])
+
+ mkArrow : (meta : Bounds) -> List Type'Fun -> Type'Fun -> Type'Fun
+ mkArrow meta [] cod = cod
+ mkArrow meta (arg :: args) cod =
+ let
+ arrowTm :
+ Term mode Bounds tyCtx tmCtx ->
+ Term mode Bounds tyCtx tmCtx ->
+ Term mode Bounds tyCtx tmCtx
+ arrowTm =
+ \t, u => Roll meta $ Inj meta "TArrow" $ Tup meta [<"Dom" :- t, "Cod" :- u]
+ in
+ MkParseFun (\mode, tyCtx, tmCtx =>
+ case mode of
+ Quote ctx1 ctx2 =>
+ [| arrowTm
+ (arg.try (Quote ctx1 ctx2) tyCtx tmCtx)
+ ((mkArrow meta args cod).try (Quote ctx1 ctx2) tyCtx tmCtx)
+ |]
+ Sugar ctx =>
+ [| TArrow
+ (arg.try (Sugar ctx) tyCtx tmCtx)
+ ((mkArrow meta args cod).try (Sugar ctx) tyCtx tmCtx)
+ |]
+ NoSugar =>
+ [| TArrow
+ (arg.try NoSugar tyCtx tmCtx)
+ ((mkArrow meta args cod).try NoSugar tyCtx tmCtx)
+ |])
mkAnnot :
- HList [List (HList [String, (), TypeFun]), WithBounds (), TypeFun, (), List String, TermFun] ->
+ HList [List (HList [String, (), Type'Fun]), WithBounds (), Type'Fun, (), List String, TermFun] ->
WithDoc TermFun
mkAnnot [[], m, cod, _, doc, t] =
AddDoc
- (MkParseFun (\tyCtx, tmCtx =>
- pure $ Annot m.bounds !(t.try tyCtx tmCtx) !(cod.try tyCtx)))
+ (MkParseFun (\mode, tyCtx, tmCtx =>
+ [| Annot (pure m.bounds) (t.try mode tyCtx tmCtx) (cod.try mode tyCtx tmCtx) |]))
doc
mkAnnot [args, m, cod, _, doc, t] =
let bound = map (\[x, _, a] => x) args in
let tys = map (\[x, _, a] => a) args in
AddDoc
- (MkParseFun (\tyCtx, tmCtx =>
- pure $
- Annot m.bounds
- (Abs m.bounds (bound ** !(t.try tyCtx (tmCtx <>< bound))))
- !((mkArrow tys cod).try tyCtx)))
+ (MkParseFun (\mode, tyCtx, tmCtx =>
+ [| (\t, a => Annot m.bounds (Abs m.bounds (bound ** t)) a)
+ (t.try mode tyCtx (tmCtx <>< bound))
+ ((mkArrow m.bounds tys cod).try mode tyCtx tmCtx)
+ |]))
doc
mkUnannot : HList [(), List String, TermFun] -> WithDoc TermFun
@@ -589,14 +834,25 @@ AbsTerm =
mkAbs <$> Seq
[ WithBounds (match Backslash)
, sepBy1 (match Comma) (match TermIdent)
- , match DoubleArrow
+ , (match DoubleArrow <||> match WaveArrow)
, Var (%%% "openTerm")
]
where
- mkAbs : HList [WithBounds (), List1 String, (), TermFun] -> TermFun
- mkAbs [m, args, _, body] =
- MkParseFun (\tyCtx, tmCtx =>
- pure $ Abs m.bounds (forget args ** !(body.try tyCtx (tmCtx <>< forget args))))
+ mkAbs : HList [WithBounds (), List1 String, Either () (), TermFun] -> TermFun
+ mkAbs [m, args, Left _, body] =
+ MkParseFun (\mode, tyCtx, tmCtx =>
+ [| (\t => Abs m.bounds (forget args ** t))
+ (body.try mode tyCtx (tmCtx <>< forget args))
+ |])
+ mkAbs [m, args, Right _, body] =
+ MkParseFun (\mode, tyCtx, tmCtx =>
+ case mode of
+ Quote ctx1 ctx2 => Errs (singleton $ NoQAbsMsg <$ m)
+ Sugar ctx =>
+ [| (\t => QAbs m.bounds (forget args ** t))
+ (body.try (Sugar (ctx <>< forget args)) tyCtx tmCtx)
+ |]
+ NoSugar => Errs (singleton $ NoSugarMsg <$ m))
CaseTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
CaseTerm =
@@ -630,25 +886,31 @@ CaseTerm =
mkBranch :
HList [String, String, (), TermFun] ->
- Assoc (ParseFun 2 $ \tyCtx, tmCtx => (x ** Term Sugar Bounds tyCtx (tmCtx :< x)))
+ Assoc
+ (ParseFun [<Mode, SnocList String, SnocList String] $
+ \mode, tyCtx, tmCtx => (x ** Term mode Bounds tyCtx (tmCtx :< x)))
mkBranch [tag, bound, _, branch] =
- tag :- MkParseFun (\tyCtx, tmCtx => pure (bound ** !(branch.try tyCtx (tmCtx :< bound))))
+ tag :-
+ MkParseFun (\mode, tyCtx, tmCtx =>
+ [| (\t => MkDPair bound t) (branch.try mode tyCtx (tmCtx :< bound)) |])
mkCase : HList [WithBounds (), TermFun, _] -> Cases -> TermFun
mkCase [m, target, _] branches =
let branches = map (map mkBranch) branches in
- MkParseFun (\tyCtx, tmCtx =>
- pure $ Case m.bounds !(target.try tyCtx tmCtx) !(tryRow2 branches tyCtx tmCtx))
+ MkParseFun (\mode, tyCtx, tmCtx =>
+ [| Case (pure m.bounds)
+ (target.try mode tyCtx tmCtx)
+ ((parseRow3 branches).try mode tyCtx tmCtx)
+ |])
mkFoldCase : HList [WithBounds (), TermFun, _] -> Cases -> TermFun
mkFoldCase [m, target, _] branches =
let branches = map (map mkBranch) branches in
- MkParseFun (\tyCtx, tmCtx =>
- pure $
- Fold
- m.bounds
- !(target.try tyCtx tmCtx)
- ("__tmp" ** Case m.bounds (Var m.bounds $ %% "__tmp") !(tryRow2 branches tyCtx (tmCtx :< "__tmp"))))
+ MkParseFun (\mode, tyCtx, tmCtx =>
+ [| (\t, ts => Fold m.bounds t ("__tmp" ** Case m.bounds (Var m.bounds $ %% "__tmp") ts))
+ (target.try mode tyCtx tmCtx)
+ ((parseRow3 branches).try mode tyCtx (tmCtx :< "__tmp"))
+ |])
FoldTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun
FoldTerm =
@@ -667,8 +929,11 @@ FoldTerm =
where
mkFold : HList [WithBounds (), TermFun, (), HList [(), String, (), TermFun]] -> TermFun
mkFold [m, target, _, [_, arg, _, body]] =
- MkParseFun (\tyCtx, tmCtx =>
- pure $ Fold m.bounds !(target.try tyCtx tmCtx) (arg ** !(body.try tyCtx (tmCtx :< arg))))
+ MkParseFun (\mode, tyCtx, tmCtx =>
+ [| (\e, t => Fold m.bounds e (arg ** t))
+ (target.try mode tyCtx tmCtx)
+ (body.try mode tyCtx (tmCtx :< arg))
+ |])
export
OpenTerm : InkyParser False [<] [<] TermFun
@@ -683,5 +948,5 @@ OpenTerm =
%hint
export
-OpenTermWf : So (wellTyped EqI [<] [<] [<] [<] OpenTerm)
-OpenTermWf = Oh
+OpenTermWf : collectTypeErrs @{ListSet} [<] [<] [<] [<] OpenTerm = []
+OpenTermWf = Refl
diff --git a/src/Inky/Term/Pretty.idr b/src/Inky/Term/Pretty.idr
index 0523362..fbedab3 100644
--- a/src/Inky/Term/Pretty.idr
+++ b/src/Inky/Term/Pretty.idr
@@ -5,81 +5,34 @@ import Data.String
import Inky.Term
import Inky.Type.Pretty
-import Inky.Term.Sugar
import Text.Bounded
import Text.PrettyPrint.Prettyprinter
-public export
-data TermPrec = Atom | Prefix | Suffix | App | Annot | Open
-
-%name TermPrec d
-
-Eq TermPrec where
- Atom == Atom = True
- Prefix == Prefix = True
- Suffix == Suffix = True
- App == App = True
- Annot == Annot = True
- Open == Open = True
- _ == _ = False
-
-Ord TermPrec where
- compare Atom Atom = EQ
- compare Atom d2 = LT
- compare Prefix Atom = GT
- compare Prefix Prefix = EQ
- compare Prefix d2 = LT
- compare Suffix Atom = GT
- compare Suffix Prefix = GT
- compare Suffix Suffix = EQ
- compare Suffix d2 = LT
- compare App App = EQ
- compare App Annot = LT
- compare App Open = LT
- compare App d2 = GT
- compare Annot Annot = EQ
- compare Annot Open = LT
- compare Annot d2 = GT
- compare Open Open = EQ
- compare Open d2 = GT
-
export
-prettyTerm : {tyCtx, tmCtx : SnocList String} -> Term mode m tyCtx tmCtx -> TermPrec -> Doc ann
-prettyAllTerm : {tyCtx, tmCtx : SnocList String} -> List (Term mode m tyCtx tmCtx) -> TermPrec -> List (Doc ann)
-prettyTermCtx : {tyCtx, tmCtx : SnocList String} -> Context (Term mode m tyCtx tmCtx) -> SnocList (Doc ann)
-prettyCases : {tyCtx, tmCtx : SnocList String} -> Context (x ** Term mode m tyCtx (tmCtx :< x)) -> SnocList (Doc ann)
+prettyTerm :
+ {mode : Mode} -> {tyCtx, tmCtx : SnocList String} ->
+ Term mode m tyCtx tmCtx -> InkyPrec -> Doc ann
+prettyAllTerm :
+ {mode : Mode} -> {tyCtx, tmCtx : SnocList String} ->
+ List (Term mode m tyCtx tmCtx) -> InkyPrec -> List (Doc ann)
+prettyTermCtx :
+ {mode : Mode} -> {tyCtx, tmCtx : SnocList String} ->
+ Context (Term mode m tyCtx tmCtx) -> SnocList (Doc ann)
+prettyCases :
+ {mode : Mode} -> {tyCtx, tmCtx : SnocList String} ->
+ Context (x ** Term mode m tyCtx (tmCtx :< x)) -> SnocList (Doc ann)
prettyLet :
(eqLine : Doc ann) ->
(doc : List String) ->
(bound, body : Doc ann) ->
Doc ann
-lessPrettyTerm : {tyCtx, tmCtx : SnocList String} -> Term mode m tyCtx tmCtx -> TermPrec -> Doc ann
-
-prettyTerm t d =
- case isLit t of
- Just k => pretty k
- Nothing =>
- case isSuc t of
- Just u =>
- group $ align $ hang 2 $ parenthesise (d < App) $
- concatWith (surround line) [pretty "suc", prettyTerm (assert_smaller t u) Suffix]
- Nothing => case isList t of
- Just ts =>
- let ts = prettyAllTerm (assert_smaller t ts) Open in
- group $ align $ flatAlt
- (enclose ("[" <++> neutral) (line <+> "]") $
- concatWith (surround $ line <+> "," <++> neutral) ts)
- (enclose "[" "]" $ concatWith (surround $ "," <++> neutral) ts)
- Nothing => case isCons t of
- Just (hd, tl) =>
- group $ align $ hang 2 $ parenthesise (d < App) $
- concatWith (surround line)
- [ pretty "cons"
- , prettyTerm (assert_smaller t hd) Suffix
- , prettyTerm (assert_smaller t tl) Suffix
- ]
- Nothing => lessPrettyTerm t d
+prettyType' :
+ (mode : Mode) -> {tyCtx, tmCtx : SnocList String} ->
+ Ty' mode m tyCtx tmCtx -> InkyPrec -> Doc ann
+prettyBoundType' :
+ (mode : Mode) -> {tyCtx, tmCtx : SnocList String} ->
+ BoundTy' mode m tyCtx tmCtx -> InkyPrec -> Doc ann
prettyAllTerm [] d = []
prettyAllTerm (t :: ts) d = prettyTerm t d :: prettyAllTerm ts d
@@ -91,6 +44,12 @@ prettyTermCtx (ts :< (l :- Abs _ (bound ** t))) =
pretty l <+> ":" <++>
"\\" <+> concatWith (surround $ "," <++> neutral) (map pretty bound) <++> "=>" <+> line <+>
prettyTerm t Open)
+prettyTermCtx (ts :< (l :- QAbs _ (bound ** t))) =
+ prettyTermCtx ts :<
+ (group $ align $
+ pretty l <+> ":" <++>
+ "\\" <+> concatWith (surround $ "," <++> neutral) (map pretty bound) <++> "~>" <+> line <+>
+ prettyTerm t Open)
prettyTermCtx (ts :< (l :- t)) =
prettyTermCtx ts :<
(group $ align $ pretty l <+> ":" <+> line <+> prettyTerm t Open)
@@ -109,30 +68,42 @@ prettyCases (ts :< (l :- (x ** t))) =
prettyTerm t Open)
prettyLet eqLine [] bound body =
- group $
- (group $
- hang 2
- (group (pretty "let" <++> eqLine) <+> line <+>
- group bound) <+> line <+>
- "in") <+> line <+>
- group body
+ group $ align $
+ (group $
+ hang 2
+ (group (pretty "let" <++> eqLine) <+> line <+>
+ group bound) <+> line <+>
+ "in") <+> line <+>
+ group body
prettyLet eqLine doc bound body =
- (hang 2 $
- group (pretty "let" <++> eqLine) <+> hardline <+>
- concatMap (enclose "--" hardline . pretty) doc <+>
- group bound) <+> hardline <+>
- "in" <+> line <+>
- group body
+ align $
+ (hang 2 $
+ group (pretty "let" <++> eqLine) <+> hardline <+>
+ concatMap (enclose "--" hardline . pretty) doc <+>
+ group bound) <+> hardline <+>
+ "in" <+> line <+>
+ group body
-lessPrettyTerm (Annot _ t a) d =
+prettyType' (Quote tyCtx tmCtx) a d = parenthesise (d < Prefix) $ align $ "," <+> prettyTerm a Prefix
+prettyType' (Sugar qtCtx) a d = prettyType a d
+prettyType' NoSugar a d = prettyType a d
+
+prettyBoundType' (Quote tyCtx tmCtx) a d = parenthesise (d < Prefix) $ align $ "," <+> prettyTerm a Prefix
+prettyBoundType' (Sugar qtCtx) (x ** a) d =
+ parens $ group $ align $ hang 2 $ "\\" <+> pretty x <++> "=>" <+> line <+> prettyType a Open
+prettyBoundType' NoSugar (x ** a) d =
+ parens $ group $ align $ hang 2 $ "\\" <+> pretty x <++> "=>" <+> line <+> prettyType a Open
+
+prettyTerm (Annot _ t a) d =
group $ align $ parenthesise (d < Annot) $
prettyTerm t App <+> line <+>
- ":" <++> prettyType a Open
-lessPrettyTerm (Var _ i) d = pretty (unVal $ nameOf i)
-lessPrettyTerm (Let meta (Annot _ (Abs _ (bound ** e)) a) (x ** t)) d =
+ ":" <++> prettyType' mode a Open
+prettyTerm (Var _ i) d = pretty (unVal $ nameOf i)
+prettyTerm {mode = Sugar _} (Let meta (Annot _ (Abs _ (bound ** e)) a) (x ** t)) d =
let (binds, cod, rest) = groupBinds bound a in
let binds = map (\x => parens (pretty x.name <++> ":" <++> prettyType x.value Open)) binds in
- group $ align $ parenthesise (d < Open) $
+ -- NOTE: group breaks comments
+ align $ parenthesise (d < Open) $
prettyLet
(group $ hang 2 $ flatAlt
( pretty x <+> line <+>
@@ -155,85 +126,108 @@ lessPrettyTerm (Let meta (Annot _ (Abs _ (bound ** e)) a) (x ** t)) d =
let (binds, cod, rest) = groupBinds xs b in
((x :- a) :: binds, cod, rest)
groupBinds xs a = ([], a, xs)
-lessPrettyTerm (Let meta (Annot _ e a) (x ** t)) d =
- group $ align $ parenthesise (d < Open) $
+prettyTerm (Let meta (Annot _ e a) (x ** t)) d =
+ -- NOTE: group breaks comments
+ align $ parenthesise (d < Open) $
prettyLet
- (pretty x <+> line <+> ":" <++> prettyType a Open <++> "=")
+ (pretty x <+> line <+> ":" <++> prettyType' mode a Open <++> "=")
meta.doc
(prettyTerm e Open)
(prettyTerm t Open)
-lessPrettyTerm (Let meta e (x ** t)) d =
- group $ align $ parenthesise (d < Open) $
+prettyTerm (Let meta e (x ** t)) d =
+ -- NOTE: group breaks comments
+ align $ parenthesise (d < Open) $
prettyLet
(pretty x <++> "=")
meta.doc
(prettyTerm e Open)
(prettyTerm t Open)
-lessPrettyTerm (LetTy meta a (x ** t)) d =
- group $ align $ parenthesise (d < Open) $
+prettyTerm (LetTy meta a (x ** t)) d =
+ -- NOTE: group breaks comments
+ align $ parenthesise (d < Open) $
prettyLet
(pretty x <++> "=")
meta.doc
(prettyType a Open)
(prettyTerm t Open)
-lessPrettyTerm (Abs _ (bound ** t)) d =
+prettyTerm (Abs _ (bound ** t)) d =
group $ hang 2 $ parenthesise (d < Open) $
"\\" <+> concatWith (surround $ "," <++> neutral) (map pretty bound) <++> "=>" <+> line <+>
prettyTerm t Open
-lessPrettyTerm (App _ (Map _ (x ** a) b c) ts) d =
+prettyTerm (App _ (Map _ a b c) ts) d =
group $ align $ hang 2 $ parenthesise (d < App) $
concatWith (surround line)
( pretty "map"
- :: parens (group $ align $ hang 2 $ "\\" <+> pretty x <++> "=>" <+> line <+> prettyType a Open)
- :: prettyType b Atom
- :: prettyType c Atom
+ :: prettyBoundType' mode a Suffix
+ :: prettyType' mode b Suffix
+ :: prettyType' mode c Suffix
:: prettyAllTerm ts Suffix)
-lessPrettyTerm (App _ f ts) d =
+prettyTerm (App _ f ts) d =
group $ align $ hang 2 $ parenthesise (d < App) $
- concatWith (surround line) (prettyTerm f Suffix :: prettyAllTerm ts Suffix)
-lessPrettyTerm (Tup _ (MkRow ts _)) d =
+ concatWith (surround line) (prettyTerm f App :: prettyAllTerm ts Suffix)
+prettyTerm (Tup _ (MkRow ts _)) d =
let parts = prettyTermCtx ts <>> [] in
group $ align $ enclose "<" ">" $
flatAlt
- (neutral <++> concatWith (surround $ line' <+> "," <++> neutral) parts <+> line)
- (concatWith (surround $ "," <++> neutral) parts)
-lessPrettyTerm (Prj _ e l) d =
+ (neutral <++> concatWith (surround $ line' <+> ";" <++> neutral) parts <+> line)
+ (concatWith (surround $ ";" <++> neutral) parts)
+prettyTerm (Prj _ e l) d =
group $ align $ hang 2 $ parenthesise (d < Suffix) $
prettyTerm e Suffix <+> line' <+> "." <+> pretty l
-lessPrettyTerm (Inj _ l t) d =
+prettyTerm (Inj _ l t) d =
group $ align $ hang 2 $ parenthesise (d < App) $
pretty l <+> line <+> prettyTerm t Suffix
-lessPrettyTerm (Case _ e (MkRow ts _)) d =
+prettyTerm (Case _ e (MkRow ts _)) d =
let parts = prettyCases ts <>> [] in
group $ align $ hang 2 $ parenthesise (d < Open) $
(group $ "case" <++> prettyTerm e Open <++> "of") <+> line <+>
(braces $ flatAlt
(neutral <++> concatWith (surround $ line' <+> ";" <++> neutral) parts <+> line)
(concatWith (surround $ ";" <++> neutral) parts))
-lessPrettyTerm (Roll _ t) d =
- pretty "~" <+>
- parenthesise (d < Prefix) (group $ align $ hang 2 $ prettyTerm t Prefix)
-lessPrettyTerm (Unroll _ e) d =
- pretty "!" <+>
- parenthesise (d < Prefix) (group $ align $ hang 2 $ prettyTerm e Prefix)
-lessPrettyTerm (Fold _ e ("__tmp" ** Case _ (Var _ ((%%) "__tmp" {pos = Here})) (MkRow ts _))) d =
+prettyTerm (Roll _ t) d =
+ parenthesise (d < Prefix) $ align $ pretty "~" <+> prettyTerm t Prefix
+prettyTerm (Unroll _ e) d =
+ parenthesise (d < Prefix) $ align $ pretty "!" <+> prettyTerm e Prefix
+prettyTerm (Fold _ e ("__tmp" ** Case _ (Var _ ((%%) "__tmp" {pos = Here})) (MkRow ts _))) d =
let parts = prettyCases ts <>> [] in
-- XXX: should check for usage of "__tmp" in ts
group $ align $ hang 2 $ parenthesise (d < Open) $
- (group $ hang (-2) $ "foldcase" <++> prettyTerm e Open <+> line <+> "by") <+> line <+>
+ (group $ "foldcase" <++> prettyTerm e Open <++> "by") <+> line <+>
(braces $ flatAlt
(neutral <++> concatWith (surround $ line' <+> ";" <++> neutral) parts <+> line)
(concatWith (surround $ ";" <++> neutral) parts))
-lessPrettyTerm (Fold _ e (x ** t)) d =
+prettyTerm (Fold _ e (x ** t)) d =
group $ align $ hang 2 $ parenthesise (d < Open) $
(group $ hang (-2) $ "fold" <++> prettyTerm e Open <++> "by") <+> line <+>
(group $ align $ hang 2 $ parens $
"\\" <+> pretty x <++> "=>" <+> line <+> prettyTerm t Open)
-lessPrettyTerm (Map _ (x ** a) b c) d =
+prettyTerm (Map _ a b c) d =
group $ align $ hang 2 $ parenthesise (d < App) $
concatWith (surround line)
[ pretty "map"
- , group (align $ hang 2 $ parens $ "\\" <+> pretty x <++> "=>" <+> line <+> prettyType a Open)
- , prettyType b Atom
- , prettyType c Atom
+ , prettyBoundType' mode a Suffix
+ , prettyType' mode b Suffix
+ , prettyType' mode c Suffix
]
+prettyTerm (QuasiQuote _ t) d =
+ parenthesise (d < Prefix) $ align $ pretty "`" <+> prettyTerm t Prefix
+prettyTerm (Unquote _ t) d =
+ parenthesise (d < Prefix) $ align $ pretty "," <+> prettyTerm t Prefix
+prettyTerm (QAbs _ (bound ** t)) d =
+ group $ hang 2 $ parenthesise (d < Open) $
+ "\\" <+> concatWith (surround $ "," <++> neutral) (map pretty bound) <++> "~>" <+> line <+>
+ prettyTerm t Open
+prettyTerm (Lit _ k) d = pretty k
+prettyTerm (Suc _ t) d =
+ group $ align $ hang 2 $ parenthesise (d < App) $
+ concatWith (surround line) [pretty "suc", prettyTerm t Suffix]
+prettyTerm (List _ ts) d =
+ let parts = prettyAllTerm ts Open in
+ group $ align $ enclose "[" "]" $
+ flatAlt
+ (neutral <++> concatWith (surround $ line' <+> ";" <++> neutral) parts <+> line)
+ (concatWith (surround $ ";" <++> neutral) parts)
+prettyTerm (Cons _ t u) d =
+ group $ align $ hang 2 $ parenthesise (d < App) $
+ concatWith (surround line) [pretty "cons", prettyTerm t Suffix, prettyTerm u Suffix]
+prettyTerm (Str _ str) d = enclose "\"" "\"" $ pretty str
diff --git a/src/Inky/Term/Pretty/Error.idr b/src/Inky/Term/Pretty/Error.idr
index d87178f..ee0f28a 100644
--- a/src/Inky/Term/Pretty/Error.idr
+++ b/src/Inky/Term/Pretty/Error.idr
@@ -25,7 +25,7 @@ Pretty (ChecksOnly t) where
export
prettyNotSynths :
{tyCtx, tmCtx : SnocList String} ->
- {e : Term mode m tyCtx tmCtx} ->
+ {e : Term NoSugar m tyCtx tmCtx} ->
{tyEnv : _} -> {tmEnv : _} ->
NotSynths tyEnv tmEnv e ->
List (m, Doc ann)
@@ -33,33 +33,33 @@ export
prettyNotChecks :
{tyCtx, tmCtx : SnocList String} ->
{a : Ty [<]} ->
- {t : Term mode m tyCtx tmCtx} ->
+ {t : Term NoSugar m tyCtx tmCtx} ->
{tyEnv : _} -> {tmEnv : _} ->
NotChecks tyEnv tmEnv a t ->
List (m, Doc ann)
prettyNotCheckSpine :
{tyCtx, tmCtx : SnocList String} ->
{a : Ty [<]} ->
- {ts : List (Term mode m tyCtx tmCtx)} ->
+ {ts : List (Term NoSugar m tyCtx tmCtx)} ->
{tyEnv : _} -> {tmEnv : _} ->
NotCheckSpine tyEnv tmEnv a ts ->
List (m, Doc ann)
prettyAnyNotSynths :
{tyCtx, tmCtx : SnocList String} ->
- {es : Context (Term mode m tyCtx tmCtx)} ->
+ {es : Context (Term NoSugar m tyCtx tmCtx)} ->
{tyEnv : _} -> {tmEnv : _} ->
AnyNotSynths tyEnv tmEnv es ->
List (m, Doc ann)
prettyAnyNotChecks :
{tyCtx, tmCtx : SnocList String} ->
- {ts : Context (Term mode m tyCtx tmCtx)} ->
+ {ts : Context (Term NoSugar m tyCtx tmCtx)} ->
{tyEnv : _} -> {tmEnv : _} -> {as : Context _} ->
(meta : m) ->
AnyNotChecks tyEnv tmEnv as ts ->
List (m, Doc ann)
prettyAnyNotBranches :
{tyCtx, tmCtx : SnocList String} ->
- {ts : Context (x ** Term mode m tyCtx (tmCtx :< x))} ->
+ {ts : Context (x ** Term NoSugar m tyCtx (tmCtx :< x))} ->
{tyEnv : _} -> {tmEnv : _} -> {as : Context _} -> {a : _} ->
(meta : m) ->
AnyNotBranches tyEnv tmEnv as a ts ->
diff --git a/src/Inky/Term/Recompute.idr b/src/Inky/Term/Recompute.idr
index dd0e809..71ba6b9 100644
--- a/src/Inky/Term/Recompute.idr
+++ b/src/Inky/Term/Recompute.idr
@@ -76,7 +76,7 @@ dropAllWellFormed (wfs :< wf) (There i) = dropAllWellFormed wfs i :< wf
export
synthsWf :
- {e : Term mode m tyCtx tmCtx} ->
+ {e : Term NoSugar m tyCtx tmCtx} ->
{tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
{tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
DAll WellFormed tyEnv -> DAll WellFormed tmEnv ->
@@ -85,7 +85,7 @@ checkSpineWf :
CheckSpine tyEnv tmEnv a ts b ->
WellFormed a -> WellFormed b
allSynthsWf :
- {es : Context (Term mode m tyCtx tmCtx)} ->
+ {es : Context (Term NoSugar m tyCtx tmCtx)} ->
{tyEnv : All (Assoc0 $ Ty [<]) tyCtx} ->
{tmEnv : All (Assoc0 $ Ty [<]) tmCtx} ->
DAll WellFormed tyEnv -> DAll WellFormed tmEnv ->
diff --git a/src/Inky/Term/Substitution.idr b/src/Inky/Term/Substitution.idr
deleted file mode 100644
index c99f5e6..0000000
--- a/src/Inky/Term/Substitution.idr
+++ /dev/null
@@ -1,197 +0,0 @@
-module Inky.Term.Substitution
-
-import Data.List.Quantifiers
-import Flap.Data.List
-import Inky.Term
-
-public export
-thin : ctx1 `Thins` ctx2 -> Term mode m tyCtx ctx1 -> Term mode m tyCtx ctx2
-public export
-thinList : ctx1 `Thins` ctx2 -> List (Term mode m tyCtx ctx1) -> List (Term mode m tyCtx ctx2)
-public export
-thinAll : ctx1 `Thins` ctx2 -> Context (Term mode m tyCtx ctx1) -> Context (Term mode m tyCtx ctx2)
-public export
-thinAllNames :
- (f : ctx1 `Thins` ctx2) -> (ts : Context (Term mode m tyCtx ctx1)) ->
- (thinAll f ts).names = ts.names
-public export
-thinBranches :
- ctx1 `Thins` ctx2 ->
- Context (x ** Term mode m tyCtx (ctx1 :< x)) ->
- Context (x ** Term mode m tyCtx (ctx2 :< x))
-public export
-thinBranchesNames :
- (f : ctx1 `Thins` ctx2) -> (ts : Context (x ** Term mode m tyCtx (ctx1 :< x))) ->
- (thinBranches f ts).names = ts.names
-
-thin f (Annot meta t a) = Annot meta (thin f t) a
-thin f (Var meta i) = Var meta (index f i)
-thin f (Let meta e (x ** t)) = Let meta (thin f e) (x ** thin (Keep f) t)
-thin f (LetTy meta a (x ** t)) = LetTy meta a (x ** thin f t)
-thin f (Abs meta (bound ** t)) = Abs meta (bound ** thin (f <>< lengthOf bound) t)
-thin f (App meta e ts) = App meta (thin f e) (thinList f ts)
-thin f (Tup meta (MkRow ts fresh)) =
- Tup meta (MkRow (thinAll f ts) (rewrite thinAllNames f ts in fresh))
-thin f (Prj meta e l) = Prj meta (thin f e) l
-thin f (Inj meta l t) = Inj meta l (thin f t)
-thin f (Case meta t (MkRow ts fresh)) =
- Case meta (thin f t) (MkRow (thinBranches f ts) (rewrite thinBranchesNames f ts in fresh))
-thin f (Roll meta t) = Roll meta (thin f t)
-thin f (Unroll meta e) = Unroll meta (thin f e)
-thin f (Fold meta e (x ** t)) = Fold meta (thin f e) (x ** thin (Keep f) t)
-thin f (Map meta (x ** a) b c) = Map meta (x ** a) b c
-
-thinList f [] = []
-thinList f (t :: ts) = thin f t :: thinList f ts
-
-thinAll f [<] = [<]
-thinAll f (ts :< (l :- t)) = thinAll f ts :< (l :- thin f t)
-
-thinAllNames f [<] = Refl
-thinAllNames f (ts :< (l :- t)) = cong (:< l) $ thinAllNames f ts
-
-thinBranches f [<] = [<]
-thinBranches f (ts :< (l :- (x ** t))) = thinBranches f ts :< (l :- (x ** thin (Keep f) t))
-
-thinBranchesNames f [<] = Refl
-thinBranchesNames f (ts :< (l :- (x ** t))) = cong (:< l) $ thinBranchesNames f ts
-
-public export
-thinTy : ctx1 `Thins` ctx2 -> Term mode m ctx1 tmCtx -> Term mode m ctx2 tmCtx
-public export
-thinTyList : ctx1 `Thins` ctx2 -> List (Term mode m ctx1 tmCtx) -> List (Term mode m ctx2 tmCtx)
-public export
-thinTyAll : ctx1 `Thins` ctx2 -> Context (Term mode m ctx1 tmCtx) -> Context (Term mode m ctx2 tmCtx)
-public export
-thinTyAllNames :
- (f : ctx1 `Thins` ctx2) -> (ts : Context (Term mode m ctx1 tmCtx)) ->
- (thinTyAll f ts).names = ts.names
-public export
-thinTyBranches :
- ctx1 `Thins` ctx2 ->
- Context (x ** Term mode m ctx1 (tmCtx :< x)) ->
- Context (x ** Term mode m ctx2 (tmCtx :< x))
-public export
-thinTyBranchesNames :
- (f : ctx1 `Thins` ctx2) -> (ts : Context (x ** Term mode m ctx1 (tmCtx :< x))) ->
- (thinTyBranches f ts).names = ts.names
-
-thinTy f (Annot meta t a) = Annot meta (thinTy f t) (rename f a)
-thinTy f (Var meta i) = Var meta i
-thinTy f (Let meta e (x ** t)) = Let meta (thinTy f e) (x ** thinTy f t)
-thinTy f (LetTy meta a (x ** t)) = LetTy meta (rename f a) (x ** thinTy (Keep f) t)
-thinTy f (Abs meta (bound ** t)) = Abs meta (bound ** thinTy f t)
-thinTy f (App meta e ts) = App meta (thinTy f e) (thinTyList f ts)
-thinTy f (Tup meta (MkRow ts fresh)) =
- Tup meta (MkRow (thinTyAll f ts) (rewrite thinTyAllNames f ts in fresh))
-thinTy f (Prj meta e l) = Prj meta (thinTy f e) l
-thinTy f (Inj meta l t) = Inj meta l (thinTy f t)
-thinTy f (Case meta t (MkRow ts fresh)) =
- Case meta (thinTy f t) (MkRow (thinTyBranches f ts) (rewrite thinTyBranchesNames f ts in fresh))
-thinTy f (Roll meta t) = Roll meta (thinTy f t)
-thinTy f (Unroll meta e) = Unroll meta (thinTy f e)
-thinTy f (Fold meta e (x ** t)) = Fold meta (thinTy f e) (x ** thinTy f t)
-thinTy f (Map meta (x ** a) b c) = Map meta (x ** rename (Keep f) a) (rename f b) (rename f c)
-
-thinTyList f [] = []
-thinTyList f (t :: ts) = thinTy f t :: thinTyList f ts
-
-thinTyAll f [<] = [<]
-thinTyAll f (ts :< (l :- t)) = thinTyAll f ts :< (l :- thinTy f t)
-
-thinTyAllNames f [<] = Refl
-thinTyAllNames f (ts :< (l :- t)) = cong (:< l) $ thinTyAllNames f ts
-
-thinTyBranches f [<] = [<]
-thinTyBranches f (ts :< (l :- (x ** t))) = thinTyBranches f ts :< (l :- (x ** thinTy f t))
-
-thinTyBranchesNames f [<] = Refl
-thinTyBranchesNames f (ts :< (l :- (x ** t))) = cong (:< l) $ thinTyBranchesNames f ts
-
-public export
-Env : Mode -> Type -> SnocList String -> SnocList String -> SnocList String -> Type
-Env mode m tyCtx ctx1 ctx2 = All (Assoc0 $ Either (Var ctx2) (Term mode m tyCtx ctx2)) ctx1
-
-public export
-Env' : Mode -> Type -> SnocList String -> List String -> SnocList String -> Type
-Env' mode m tyCtx ctx1 ctx2 = All (Assoc0 $ Either (Var ctx2) (Term mode m tyCtx ctx2)) ctx1
-
-public export
-thinEnv :
- ctx2 `Thins` ctx3 ->
- Env mode m tyCtx ctx1 ctx2 ->
- Env mode m tyCtx ctx1 ctx3
-thinEnv f = mapProperty (map $ bimap (index f) (thin $ f))
-
-public export
-lift :
- Env mode m tyCtx ctx1 ctx2 ->
- Env mode m tyCtx (ctx1 :< x) (ctx2 :< x)
-lift f = thinEnv (Drop Id) f :< (x :- Left (%% x))
-
-public export
-sub :
- Env mode m tyCtx ctx1 ctx2 ->
- Term mode m tyCtx ctx1 -> Term mode m tyCtx ctx2
-public export
-subList :
- Env mode m tyCtx ctx1 ctx2 ->
- List (Term mode m tyCtx ctx1) -> List (Term mode m tyCtx ctx2)
-public export
-subAll :
- Env mode m tyCtx ctx1 ctx2 ->
- Context (Term mode m tyCtx ctx1) -> Context (Term mode m tyCtx ctx2)
-public export
-subAllNames :
- (f : Env mode m tyCtx ctx1 ctx2) ->
- (ts : Context (Term mode m tyCtx ctx1)) -> (subAll f ts).names = ts.names
-public export
-subBranches :
- Env mode m tyCtx ctx1 ctx2 ->
- Context (x ** Term mode m tyCtx (ctx1 :< x)) ->
- Context (x ** Term mode m tyCtx (ctx2 :< x))
-public export
-subBranchesNames :
- (f : Env mode m tyCtx ctx1 ctx2) ->
- (ts : Context (x ** Term mode m tyCtx (ctx1 :< x))) -> (subBranches f ts).names = ts.names
-
-public export
-keepBound :
- forall ctx. {0 bound : List String} ->
- LengthOf bound -> Env' mode m tyCtx bound (ctx <>< bound)
-keepBound Z = []
-keepBound (S len) = (_ :- Left (index (dropFish Id len) (toVar Here))) :: keepBound len
-
-sub f (Annot meta t a) = Annot meta (sub f t) a
-sub f (Var meta i) = either (Var meta) id (indexAll i.pos f).value
-sub f (Let meta e (x ** t)) = Let meta (sub f e) (x ** sub (lift f) t)
-sub f (LetTy meta a (x ** t)) = LetTy meta a (x ** sub (mapProperty (map $ map $ thinTy (Drop Id)) f) t)
-sub f (Abs meta (bound ** t)) =
- let len = lengthOf bound in
- Abs meta (bound ** sub (thinEnv (dropFish Id len) f <>< keepBound len) t)
-sub f (App meta e ts) = App meta (sub f e) (subList f ts)
-sub f (Tup meta (MkRow ts fresh)) =
- Tup meta (MkRow (subAll f ts) (rewrite subAllNames f ts in fresh))
-sub f (Prj meta e l) = Prj meta (sub f e) l
-sub f (Inj meta l t) = Inj meta l (sub f t)
-sub f (Case meta t (MkRow ts fresh)) =
- Case meta (sub f t) (MkRow (subBranches f ts) (rewrite subBranchesNames f ts in fresh))
-sub f (Roll meta t) = Roll meta (sub f t)
-sub f (Unroll meta e) = Unroll meta (sub f e)
-sub f (Fold meta e (x ** t)) = Fold meta (sub f e) (x ** sub (lift f) t)
-sub f (Map meta (x ** a) b c) = Map meta (x ** a) b c
-
-subList f [] = []
-subList f (t :: ts) = sub f t :: subList f ts
-
-subAll f [<] = [<]
-subAll f (ts :< (l :- t)) = subAll f ts :< (l :- sub f t)
-
-subAllNames f [<] = Refl
-subAllNames f (ts :< (l :- t)) = cong (:< l) $ subAllNames f ts
-
-subBranches f [<] = [<]
-subBranches f (ts :< (l :- (x ** t))) = subBranches f ts :< (l :- (x ** sub (lift f) t))
-
-subBranchesNames f [<] = Refl
-subBranchesNames f (ts :< (l :- (x ** t))) = cong (:< l) $ subBranchesNames f ts
diff --git a/src/Inky/Term/Sugar.idr b/src/Inky/Term/Sugar.idr
deleted file mode 100644
index 477df5e..0000000
--- a/src/Inky/Term/Sugar.idr
+++ /dev/null
@@ -1,73 +0,0 @@
-module Inky.Term.Sugar
-
-import Flap.Decidable
-import Inky.Term
-
--- Naturals --------------------------------------------------------------------
-
-export
-Zero : m -> Term mode m tyCtx tmCtx
-Zero meta = Roll meta (Inj meta "Z" $ Tup meta [<])
-
-export
-Suc : m -> Term mode m tyCtx tmCtx -> Term mode m tyCtx tmCtx
-Suc meta t = Roll meta (Inj meta "S" t)
-
-export
-isZero : Term mode m tyCtx tmCtx -> Bool
-isZero (Roll _ (Inj _ "Z" $ Tup _ $ MkRow [<] _)) = True
-isZero _ = False
-
-export
-isSuc : Term mode m tyCtx tmCtx -> Maybe (Term mode m tyCtx tmCtx)
-isSuc (Roll _ (Inj _ "S" t)) = Just t
-isSuc _ = Nothing
-
-export
-Lit : m -> Nat -> Term mode m tyCtx tmCtx
-Lit meta 0 = Roll meta (Inj meta "Z" $ Tup meta [<])
-Lit meta (S n) = Suc meta (Lit meta n)
-
-export
-isLit : Term mode m tyCtx tmCtx -> Maybe Nat
-isLit t =
- if isZero t then Just 0
- else do
- u <- isSuc t
- k <- isLit (assert_smaller t u)
- pure (S k)
-
--- Lists -----------------------------------------------------------------------
-
-export
-Nil : m -> Term mode m tyCtx tmCtx
-Nil meta = Roll meta (Inj meta "N" $ Tup meta [<])
-
-export
-Cons : m -> Term mode m tyCtx tmCtx -> Term mode m tyCtx tmCtx -> Term mode m tyCtx tmCtx
-Cons meta t ts = Roll meta (Inj meta "C" $ Tup meta [<"H" :- t, "T" :- ts])
-
-export
-fromList : m -> List (Term mode m tyCtx tmCtx) -> Term mode m tyCtx tmCtx
-fromList meta [] = Nil meta
-fromList meta (t :: ts) = Cons meta t (fromList meta ts)
-
-export
-isNil : Term mode m tyCtx tmCtx -> Bool
-isNil (Roll _ (Inj _ "N" $ Tup _ $ MkRow [<] _)) = True
-isNil _ = False
-
-export
-isCons : Term mode m tyCtx tmCtx -> Maybe (Term mode m tyCtx tmCtx, Term mode m tyCtx tmCtx)
-isCons (Roll _ (Inj _ "C" $ Tup meta $ MkRow [<"H" :- t, "T" :- ts] _)) = Just (t, ts)
-isCons (Roll _ (Inj _ "C" $ Tup meta $ MkRow [<"T" :- ts, "H" :- t] _)) = Just (t, ts)
-isCons _ = Nothing
-
-export
-isList : Term mode m tyCtx tmCtx -> Maybe (List $ Term mode m tyCtx tmCtx)
-isList t =
- if isNil t then Just []
- else do
- (hd, tl) <- isCons t
- tl <- isList (assert_smaller t tl)
- pure (hd :: tl)
diff --git a/src/Inky/Type/Pretty.idr b/src/Inky/Type/Pretty.idr
index 91b28ba..03b9964 100644
--- a/src/Inky/Type/Pretty.idr
+++ b/src/Inky/Type/Pretty.idr
@@ -6,31 +6,45 @@ import Inky.Type
import Text.PrettyPrint.Prettyprinter
public export
-data TyPrec = Atom | App | Open
+data InkyPrec = Atom | Prefix | Suffix | App | Annot | Open
-%name TyPrec d
+%name InkyPrec d
-Eq TyPrec where
+export
+Eq InkyPrec where
Atom == Atom = True
+ Prefix == Prefix = True
+ Suffix == Suffix = True
App == App = True
+ Annot == Annot = True
Open == Open = True
_ == _ = False
-Ord TyPrec where
+export
+Ord InkyPrec where
compare Atom Atom = EQ
- compare Atom App = LT
- compare Atom Open = LT
- compare App Atom = GT
+ compare Atom d2 = LT
+ compare Prefix Atom = GT
+ compare Prefix Prefix = EQ
+ compare Prefix d2 = LT
+ compare Suffix Atom = GT
+ compare Suffix Prefix = GT
+ compare Suffix Suffix = EQ
+ compare Suffix d2 = LT
compare App App = EQ
+ compare App Annot = LT
compare App Open = LT
- compare Open Atom = GT
- compare Open App = GT
+ compare App d2 = GT
+ compare Annot Annot = EQ
+ compare Annot Open = LT
+ compare Annot d2 = GT
compare Open Open = EQ
+ compare Open d2 = GT
export
-prettyType : {ctx : SnocList String} -> Ty ctx -> TyPrec -> Doc ann
-lessPrettyType : {ctx : SnocList String} -> Ty ctx -> TyPrec -> Doc ann
-lessPrettyTypeCtx : {ctx : SnocList String} -> Context (Ty ctx) -> TyPrec -> SnocList (Doc ann)
+prettyType : {ctx : SnocList String} -> Ty ctx -> InkyPrec -> Doc ann
+lessPrettyType : {ctx : SnocList String} -> Ty ctx -> InkyPrec -> Doc ann
+lessPrettyTypeCtx : {ctx : SnocList String} -> Context (Ty ctx) -> InkyPrec -> SnocList (Doc ann)
prettyType a d =
if does (alpha {ctx2 = [<]} a TNat)
@@ -55,14 +69,14 @@ lessPrettyType (TProd (MkRow as _)) d =
let parts = lessPrettyTypeCtx as Open <>> [] in
group $ align $ enclose "<" ">" $
flatAlt
- (neutral <++> concatWith (surround $ line <+> "," <++> neutral) parts <+> line)
- (concatWith (surround $ "," <++> neutral) parts)
+ (neutral <++> concatWith (surround $ line <+> ";" <++> neutral) parts <+> line)
+ (concatWith (surround $ ";" <++> neutral) parts)
lessPrettyType (TSum (MkRow as _)) d =
let parts = lessPrettyTypeCtx as Open <>> [] in
group $ align $ enclose "[" "]" $
flatAlt
- (neutral <++> concatWith (surround $ line <+> "," <++> neutral) parts <+> line)
- (concatWith (surround $ "," <++> neutral) parts)
+ (neutral <++> concatWith (surround $ line <+> ";" <++> neutral) parts <+> line)
+ (concatWith (surround $ ";" <++> neutral) parts)
lessPrettyType (TFix x a) d =
group $ align $ hang 2 $ parens $
"\\" <+> pretty x <++> "=>" <+> line <+>
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 07:22:46 +0000