edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-12-28 23:33:27 +03:00
Code Issues Projects Releases Wiki Activity

Add ! notation

Browse Source 
In a small change from Idris 1, this lifts to the nearest binder or
block, so doesn't lift past an explicit "do" in particular. Blocks are:
- case branches
- if branches
- scope of local function definitions, or any binder
- do blocks
This commit is contained in:
Edwin Brady 2020-01-26 16:52:25 +00:00
parent 9cd040fcb4
commit 1da3af5b2a
9 changed files with 208 additions and 104 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

240
src/Idris/Desugar.idr
View File

@ -99,90 +99,107 @@ toTokList (PPrefixOp fc opn arg)
pure (Op fc opn (Prefix prec) :: rtoks) pure (Op fc opn (Prefix prec) :: rtoks)
toTokList t = pure [Expr t] toTokList t = pure [Expr t]
record BangData where
constructor MkBangData
nextName : Int
bangNames : List (Name, FC, RawImp)
initBangs : BangData
initBangs = MkBangData 0 []
bindBangs : List (Name, FC, RawImp) -> RawImp -> RawImp
bindBangs [] tm = tm
bindBangs ((n, fc, btm) :: bs) tm
= bindBangs bs $ IApp fc (IApp fc (IVar fc (UN ">>=")) btm)
(ILam fc RigW Explicit (Just n)
(Implicit fc False) tm)
data Bang : Type where
mutual mutual
export desugarB : {auto s : Ref Syn SyntaxInfo} ->
desugar : {auto s : Ref Syn SyntaxInfo} -> {auto b : Ref Bang BangData} ->
{auto c : Ref Ctxt Defs} -> {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} -> {auto m : Ref MD Metadata} ->
{auto m : Ref MD Metadata} -> {auto u : Ref UST UState} ->
Side -> List Name -> PTerm -> Core RawImp Side -> List Name -> PTerm -> Core RawImp
desugar side ps (PRef fc x) = pure $ IVar fc x desugarB side ps (PRef fc x) = pure $ IVar fc x
desugar side ps (PPi fc rig p mn argTy retTy) desugarB side ps (PPi fc rig p mn argTy retTy)
= let ps' = maybe ps (:: ps) mn in = let ps' = maybe ps (:: ps) mn in
pure $ IPi fc rig p mn !(desugar side ps argTy) pure $ IPi fc rig p mn !(desugarB side ps argTy)
!(desugar side ps' retTy) !(desugarB side ps' retTy)
desugar side ps (PLam fc rig p (PRef _ n@(UN _)) argTy scope) desugarB side ps (PLam fc rig p (PRef _ n@(UN _)) argTy scope)
= pure $ ILam fc rig p (Just n) !(desugar side ps argTy) = pure $ ILam fc rig p (Just n) !(desugarB side ps argTy)
!(desugar side (n :: ps) scope) !(desugar side (n :: ps) scope)
desugar side ps (PLam fc rig p (PRef _ n@(MN _ _)) argTy scope) desugarB side ps (PLam fc rig p (PRef _ n@(MN _ _)) argTy scope)
= pure $ ILam fc rig p (Just n) !(desugar side ps argTy) = pure $ ILam fc rig p (Just n) !(desugarB side ps argTy)
!(desugar side (n :: ps) scope) !(desugar side (n :: ps) scope)
desugar side ps (PLam fc rig p (PImplicit _) argTy scope) desugarB side ps (PLam fc rig p (PImplicit _) argTy scope)
= pure $ ILam fc rig p Nothing !(desugar side ps argTy) = pure $ ILam fc rig p Nothing !(desugarB side ps argTy)
!(desugar side ps scope) !(desugar side ps scope)
desugar side ps (PLam fc rig p pat argTy scope) desugarB side ps (PLam fc rig p pat argTy scope)
= pure $ ILam fc rig p (Just (MN "lamc" 0)) !(desugar side ps argTy) $ = pure $ ILam fc rig p (Just (MN "lamc" 0)) !(desugarB side ps argTy) $
ICase fc (IVar fc (MN "lamc" 0)) (Implicit fc False) ICase fc (IVar fc (MN "lamc" 0)) (Implicit fc False)
[!(desugarClause ps True (MkPatClause fc pat scope []))] [!(desugarClause ps True (MkPatClause fc pat scope []))]
desugar side ps (PLet fc rig (PRef _ n) nTy nVal scope []) desugarB side ps (PLet fc rig (PRef _ n) nTy nVal scope [])
= pure $ ILet fc rig n !(desugar side ps nTy) !(desugar side ps nVal) = pure $ ILet fc rig n !(desugarB side ps nTy) !(desugarB side ps nVal)
!(desugar side (n :: ps) scope) !(desugar side (n :: ps) scope)
desugar side ps (PLet fc rig pat nTy nVal scope alts) desugarB side ps (PLet fc rig pat nTy nVal scope alts)
= pure $ ICase fc !(desugar side ps nVal) !(desugar side ps nTy) = pure $ ICase fc !(desugarB side ps nVal) !(desugarB side ps nTy)
!(traverse (desugarClause ps True) !(traverse (desugarClause ps True)
(MkPatClause fc pat scope [] :: alts)) (MkPatClause fc pat scope [] :: alts))
desugar side ps (PCase fc x xs) desugarB side ps (PCase fc x xs)
= pure $ ICase fc !(desugar side ps x) = pure $ ICase fc !(desugarB side ps x)
(Implicit fc False) (Implicit fc False)
!(traverse (desugarClause ps True) xs) !(traverse (desugarClause ps True) xs)
desugar side ps (PLocal fc xs scope) desugarB side ps (PLocal fc xs scope)
= pure $ ILocal fc (concat !(traverse (desugarDecl ps) xs)) = pure $ ILocal fc (concat !(traverse (desugarDecl ps) xs))
!(desugar side (definedIn xs ++ ps) scope) !(desugar side (definedIn xs ++ ps) scope)
desugar side ps (PApp pfc (PUpdate fc fs) rec) desugarB side ps (PApp pfc (PUpdate fc fs) rec)
= pure $ IUpdate pfc !(traverse (desugarUpdate side ps) fs) = pure $ IUpdate pfc !(traverse (desugarUpdate side ps) fs)
!(desugar side ps rec) !(desugarB side ps rec)
desugar side ps (PUpdate fc fs) desugarB side ps (PUpdate fc fs)
= desugar side ps (PLam fc RigW Explicit (PRef fc (MN "rec" 0)) (PImplicit fc) = desugarB side ps (PLam fc RigW Explicit (PRef fc (MN "rec" 0)) (PImplicit fc)
(PApp fc (PUpdate fc fs) (PRef fc (MN "rec" 0)))) (PApp fc (PUpdate fc fs) (PRef fc (MN "rec" 0))))
desugar side ps (PApp fc x y) desugarB side ps (PApp fc x y)
= pure $ IApp fc !(desugar side ps x) !(desugar side ps y) = pure $ IApp fc !(desugarB side ps x) !(desugarB side ps y)
desugar side ps (PWithApp fc x y) desugarB side ps (PWithApp fc x y)
= pure $ IWithApp fc !(desugar side ps x) !(desugar side ps y) = pure $ IWithApp fc !(desugarB side ps x) !(desugarB side ps y)
desugar side ps (PImplicitApp fc x argn y) desugarB side ps (PImplicitApp fc x argn y)
= pure $ IImplicitApp fc !(desugar side ps x) argn !(desugar side ps y) = pure $ IImplicitApp fc !(desugarB side ps x) argn !(desugarB side ps y)
desugar side ps (PDelayed fc r ty) desugarB side ps (PDelayed fc r ty)
= pure $ IDelayed fc r !(desugar side ps ty) = pure $ IDelayed fc r !(desugarB side ps ty)
desugar side ps (PDelay fc tm) desugarB side ps (PDelay fc tm)
= pure $ IDelay fc !(desugar side ps tm) = pure $ IDelay fc !(desugarB side ps tm)
desugar side ps (PForce fc tm) desugarB side ps (PForce fc tm)
= pure $ IForce fc !(desugar side ps tm) = pure $ IForce fc !(desugarB side ps tm)
desugar side ps (PEq fc l r) desugarB side ps (PEq fc l r)
= do l' <- desugar side ps l = do l' <- desugarB side ps l
r' <- desugar side ps r r' <- desugarB side ps r
pure $ IAlternative fc FirstSuccess pure $ IAlternative fc FirstSuccess
[apply (IVar fc (UN "===")) [l', r'], [apply (IVar fc (UN "===")) [l', r'],
apply (IVar fc (UN "~=~")) [l', r']] apply (IVar fc (UN "~=~")) [l', r']]
desugar side ps (PBracketed fc e) = desugar side ps e desugarB side ps (PBracketed fc e) = desugarB side ps e
desugar side ps (POp fc op l r) desugarB side ps (POp fc op l r)
= do ts <- toTokList (POp fc op l r) = do ts <- toTokList (POp fc op l r)
desugarTree side ps !(parseOps ts) desugarTree side ps !(parseOps ts)
desugar side ps (PPrefixOp fc op arg) desugarB side ps (PPrefixOp fc op arg)
= do ts <- toTokList (PPrefixOp fc op arg) = do ts <- toTokList (PPrefixOp fc op arg)
desugarTree side ps !(parseOps ts) desugarTree side ps !(parseOps ts)
desugar side ps (PSectionL fc op arg) desugarB side ps (PSectionL fc op arg)
= do syn <- get Syn = do syn <- get Syn
-- It might actually be a prefix argument rather than a section -- It might actually be a prefix argument rather than a section
-- so check that first, otherwise desugar as a lambda -- so check that first, otherwise desugar as a lambda
case lookup (nameRoot op) (prefixes syn) of case lookup (nameRoot op) (prefixes syn) of
Nothing => Nothing =>
desugar side ps (PLam fc RigW Explicit (PRef fc (MN "arg" 0)) (PImplicit fc) desugarB side ps (PLam fc RigW Explicit (PRef fc (MN "arg" 0)) (PImplicit fc)
(POp fc op (PRef fc (MN "arg" 0)) arg)) (POp fc op (PRef fc (MN "arg" 0)) arg))
Just prec => desugar side ps (PPrefixOp fc op arg) Just prec => desugarB side ps (PPrefixOp fc op arg)
desugar side ps (PSectionR fc arg op) desugarB side ps (PSectionR fc arg op)
= desugar side ps (PLam fc RigW Explicit (PRef fc (MN "arg" 0)) (PImplicit fc) = desugarB side ps (PLam fc RigW Explicit (PRef fc (MN "arg" 0)) (PImplicit fc)
(POp fc op arg (PRef fc (MN "arg" 0)))) (POp fc op arg (PRef fc (MN "arg" 0))))
desugar side ps (PSearch fc depth) = pure $ ISearch fc depth desugarB side ps (PSearch fc depth) = pure $ ISearch fc depth
desugar side ps (PPrimVal fc (BI x)) desugarB side ps (PPrimVal fc (BI x))
= case !fromIntegerName of = case !fromIntegerName of
Nothing => Nothing =>
pure $ IAlternative fc (UniqueDefault (IPrimVal fc (BI x))) pure $ IAlternative fc (UniqueDefault (IPrimVal fc (BI x)))
@ -190,81 +207,89 @@ mutual
IPrimVal fc (I (fromInteger x))] IPrimVal fc (I (fromInteger x))]
Just fi => pure $ IApp fc (IVar fc fi) Just fi => pure $ IApp fc (IVar fc fi)
(IPrimVal fc (BI x)) (IPrimVal fc (BI x))
desugar side ps (PPrimVal fc (Str x)) desugarB side ps (PPrimVal fc (Str x))
= case !fromStringName of = case !fromStringName of
Nothing => Nothing =>
pure $ IPrimVal fc (Str x) pure $ IPrimVal fc (Str x)
Just f => pure $ IApp fc (IVar fc f) Just f => pure $ IApp fc (IVar fc f)
(IPrimVal fc (Str x)) (IPrimVal fc (Str x))
desugar side ps (PPrimVal fc (Ch x)) desugarB side ps (PPrimVal fc (Ch x))
= case !fromCharName of = case !fromCharName of
Nothing => Nothing =>
pure $ IPrimVal fc (Ch x) pure $ IPrimVal fc (Ch x)
Just f => pure $ IApp fc (IVar fc f) Just f => pure $ IApp fc (IVar fc f)
(IPrimVal fc (Ch x)) (IPrimVal fc (Ch x))
desugar side ps (PPrimVal fc x) = pure $ IPrimVal fc x desugarB side ps (PPrimVal fc x) = pure $ IPrimVal fc x
desugar side ps (PQuote fc tm) desugarB side ps (PQuote fc tm)
= pure $ IQuote fc !(desugar side ps tm) = pure $ IQuote fc !(desugarB side ps tm)
desugar side ps (PQuoteDecl fc x) desugarB side ps (PQuoteDecl fc x)
= do [x'] <- desugarDecl ps x = do [x'] <- desugarDecl ps x
| _ => throw (GenericMsg fc "Can't quote this declaration") | _ => throw (GenericMsg fc "Can't quote this declaration")
pure $ IQuoteDecl fc x' pure $ IQuoteDecl fc x'
desugar side ps (PUnquote fc tm) desugarB side ps (PUnquote fc tm)
= pure $ IUnquote fc !(desugar side ps tm) = pure $ IUnquote fc !(desugarB side ps tm)
desugar side ps (PRunElab fc tm) desugarB side ps (PRunElab fc tm)
= pure $ IRunElab fc !(desugar side ps tm) = pure $ IRunElab fc !(desugarB side ps tm)
desugar side ps (PHole fc br holename) desugarB side ps (PHole fc br holename)
= do when br $ = do when br $
do syn <- get Syn do syn <- get Syn
put Syn (record { bracketholes $= ((UN holename) ::) } syn) put Syn (record { bracketholes $= ((UN holename) ::) } syn)
pure $ IHole fc holename pure $ IHole fc holename
desugar side ps (PType fc) = pure $ IType fc desugarB side ps (PType fc) = pure $ IType fc
desugar side ps (PAs fc vname pattern) desugarB side ps (PAs fc vname pattern)
= pure $ IAs fc UseRight vname !(desugar side ps pattern) = pure $ IAs fc UseRight vname !(desugarB side ps pattern)
desugar side ps (PDotted fc x) desugarB side ps (PDotted fc x)
= pure $ IMustUnify fc UserDotted !(desugar side ps x) = pure $ IMustUnify fc UserDotted !(desugarB side ps x)
desugar side ps (PImplicit fc) = pure $ Implicit fc True desugarB side ps (PImplicit fc) = pure $ Implicit fc True
desugar side ps (PInfer fc) = pure $ Implicit fc False desugarB side ps (PInfer fc) = pure $ Implicit fc False
desugar side ps (PDoBlock fc block) desugarB side ps (PDoBlock fc block)
= expandDo side ps fc block = expandDo side ps fc block
desugar side ps (PList fc args) desugarB side ps (PBang fc term)
= do itm <- desugarB side ps term
bs <- get Bang
let bn = MN "bind" (nextName bs)
put Bang (record { nextName $= (+1),
bangNames $= ((bn, fc, itm) ::)
} bs)
pure (IVar fc bn)
desugarB side ps (PList fc args)
= expandList side ps fc args = expandList side ps fc args
desugar side ps (PPair fc l r) desugarB side ps (PPair fc l r)
= do l' <- desugar side ps l = do l' <- desugarB side ps l
r' <- desugar side ps r r' <- desugarB side ps r
let pval = apply (IVar fc (UN "MkPair")) [l', r'] let pval = apply (IVar fc (UN "MkPair")) [l', r']
pure $ IAlternative fc (UniqueDefault pval) pure $ IAlternative fc (UniqueDefault pval)
[apply (IVar fc (UN "Pair")) [l', r'], pval] [apply (IVar fc (UN "Pair")) [l', r'], pval]
desugar side ps (PDPair fc (PRef nfc (UN n)) (PImplicit _) r) desugarB side ps (PDPair fc (PRef nfc (UN n)) (PImplicit _) r)
= do r' <- desugar side ps r = do r' <- desugarB side ps r
let pval = apply (IVar fc (UN "MkDPair")) [IVar nfc (UN n), r'] let pval = apply (IVar fc (UN "MkDPair")) [IVar nfc (UN n), r']
pure $ IAlternative fc (UniqueDefault pval) pure $ IAlternative fc (UniqueDefault pval)
[apply (IVar fc (UN "DPair")) [apply (IVar fc (UN "DPair"))
[Implicit nfc False, [Implicit nfc False,
ILam nfc RigW Explicit (Just (UN n)) (Implicit nfc False) r'], ILam nfc RigW Explicit (Just (UN n)) (Implicit nfc False) r'],
pval] pval]
desugar side ps (PDPair fc (PRef nfc (UN n)) ty r) desugarB side ps (PDPair fc (PRef nfc (UN n)) ty r)
= do ty' <- desugar side ps ty = do ty' <- desugarB side ps ty
r' <- desugar side ps r r' <- desugarB side ps r
pure $ apply (IVar fc (UN "DPair")) pure $ apply (IVar fc (UN "DPair"))
[ty', [ty',
ILam nfc RigW Explicit (Just (UN n)) ty' r'] ILam nfc RigW Explicit (Just (UN n)) ty' r']
desugar side ps (PDPair fc l (PImplicit _) r) desugarB side ps (PDPair fc l (PImplicit _) r)
= do l' <- desugar side ps l = do l' <- desugarB side ps l
r' <- desugar side ps r r' <- desugarB side ps r
pure $ apply (IVar fc (UN "MkDPair")) [l', r'] pure $ apply (IVar fc (UN "MkDPair")) [l', r']
desugar side ps (PDPair fc l ty r) desugarB side ps (PDPair fc l ty r)
= throw (GenericMsg fc "Invalid dependent pair type") = throw (GenericMsg fc "Invalid dependent pair type")
desugar side ps (PUnit fc) desugarB side ps (PUnit fc)
= pure $ IAlternative fc (UniqueDefault (IVar fc (UN "MkUnit"))) = pure $ IAlternative fc (UniqueDefault (IVar fc (UN "MkUnit")))
[IVar fc (UN "Unit"), [IVar fc (UN "Unit"),
IVar fc (UN "MkUnit")] IVar fc (UN "MkUnit")]
desugar side ps (PIfThenElse fc x t e) desugarB side ps (PIfThenElse fc x t e)
= pure $ ICase fc !(desugar side ps x) (Implicit fc False) = pure $ ICase fc !(desugar side ps x) (Implicit fc False)
[PatClause fc (IVar fc (UN "True")) !(desugar side ps t), [PatClause fc (IVar fc (UN "True")) !(desugar side ps t),
PatClause fc (IVar fc (UN "False")) !(desugar side ps e)] PatClause fc (IVar fc (UN "False")) !(desugar side ps e)]
desugar side ps (PComprehension fc ret conds) desugarB side ps (PComprehension fc ret conds)
= desugar side ps (PDoBlock fc (map guard conds ++ [toPure ret])) = desugarB side ps (PDoBlock fc (map guard conds ++ [toPure ret]))
where where
guard : PDo -> PDo guard : PDo -> PDo
guard (DoExp fc tm) = DoExp fc (PApp fc (PRef fc (UN "guard")) tm) guard (DoExp fc tm) = DoExp fc (PApp fc (PRef fc (UN "guard")) tm)
@ -272,27 +297,27 @@ mutual
toPure : PTerm -> PDo toPure : PTerm -> PDo
toPure tm = DoExp fc (PApp fc (PRef fc (UN "pure")) tm) toPure tm = DoExp fc (PApp fc (PRef fc (UN "pure")) tm)
desugar side ps (PRewrite fc rule tm) desugarB side ps (PRewrite fc rule tm)
= pure $ IRewrite fc !(desugar side ps rule) !(desugar side ps tm) = pure $ IRewrite fc !(desugarB side ps rule) !(desugarB side ps tm)
desugar side ps (PRange fc start next end) desugarB side ps (PRange fc start next end)
= case next of = case next of
Nothing => Nothing =>
desugar side ps (PApp fc desugarB side ps (PApp fc
(PApp fc (PRef fc (UN "rangeFromTo")) (PApp fc (PRef fc (UN "rangeFromTo"))
start) end) start) end)
Just n => Just n =>
desugar side ps (PApp fc desugarB side ps (PApp fc
(PApp fc (PApp fc
(PApp fc (PRef fc (UN "rangeFromThenTo")) (PApp fc (PRef fc (UN "rangeFromThenTo"))
start) n) end) start) n) end)
desugar side ps (PRangeStream fc start next) desugarB side ps (PRangeStream fc start next)
= case next of = case next of
Nothing => Nothing =>
desugar side ps (PApp fc (PRef fc (UN "rangeFrom")) start) desugarB side ps (PApp fc (PRef fc (UN "rangeFrom")) start)
Just n => Just n =>
desugar side ps (PApp fc (PApp fc (PRef fc (UN "rangeFromThen")) start) n) desugarB side ps (PApp fc (PApp fc (PRef fc (UN "rangeFromThen")) start) n)
desugar side ps (PUnifyLog fc tm) desugarB side ps (PUnifyLog fc tm)
= pure $ IUnifyLog fc !(desugar side ps tm) = pure $ IUnifyLog fc !(desugarB side ps tm)
desugarUpdate : {auto s : Ref Syn SyntaxInfo} -> desugarUpdate : {auto s : Ref Syn SyntaxInfo} ->
{auto c : Ref Ctxt Defs} -> {auto c : Ref Ctxt Defs} ->
@ -375,6 +400,7 @@ mutual
pure $ IRewrite fc rule' rest' pure $ IRewrite fc rule' rest'
desugarTree : {auto s : Ref Syn SyntaxInfo} -> desugarTree : {auto s : Ref Syn SyntaxInfo} ->
{auto b : Ref Bang BangData} ->
{auto c : Ref Ctxt Defs} -> {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} -> {auto u : Ref UST UState} ->
{auto m : Ref MD Metadata} -> {auto m : Ref MD Metadata} ->
@ -401,7 +427,7 @@ mutual
desugarTree side ps (Pre loc op arg) desugarTree side ps (Pre loc op arg)
= do arg' <- desugarTree side ps arg = do arg' <- desugarTree side ps arg
pure (IApp loc (IVar loc op) arg') pure (IApp loc (IVar loc op) arg')
desugarTree side ps (Leaf t) = desugar side ps t desugarTree side ps (Leaf t) = desugarB side ps t
desugarType : {auto s : Ref Syn SyntaxInfo} -> desugarType : {auto s : Ref Syn SyntaxInfo} ->
{auto c : Ref Ctxt Defs} -> {auto c : Ref Ctxt Defs} ->
@ -683,3 +709,15 @@ mutual
Overloadable n => pure [IPragma (\c, nest, env => setNameFlag fc n Overloadable)] Overloadable n => pure [IPragma (\c, nest, env => setNameFlag fc n Overloadable)]
Extension e => pure [IPragma (\c, nest, env => setExtension e)] Extension e => pure [IPragma (\c, nest, env => setExtension e)]
export
desugar : {auto s : Ref Syn SyntaxInfo} ->
{auto c : Ref Ctxt Defs} ->
{auto m : Ref MD Metadata} ->
{auto u : Ref UST UState} ->
Side -> List Name -> PTerm -> Core RawImp
desugar s ps tm
= do b <- newRef Bang initBangs
tm' <- desugarB s ps tm
bd <- get Bang
pure $ bindBangs (bangNames bd) tm'

5
src/Idris/Parser.idr
View File

@ -345,6 +345,11 @@ mutual
<|> do start <- location <|> do start <- location
symbol "[" symbol "["
listExpr fname start indents listExpr fname start indents
<|> do start <- location
symbol "!"
e <- simpleExpr fname indents
end <- location
pure (PBang (MkFC fname start end) e)
<|> do start <- location <|> do start <- location
symbol "%"; exactIdent "unifyLog" symbol "%"; exactIdent "unifyLog"
e <- expr pdef fname indents e <- expr pdef fname indents

4
src/Idris/Syntax.idr
View File

@ -77,6 +77,7 @@ mutual
-- Syntactic sugar -- Syntactic sugar
PDoBlock : FC -> List PDo -> PTerm PDoBlock : FC -> List PDo -> PTerm
PBang : FC -> PTerm -> PTerm
PList : FC -> List PTerm -> PTerm PList : FC -> List PTerm -> PTerm
PPair : FC -> PTerm -> PTerm -> PTerm PPair : FC -> PTerm -> PTerm -> PTerm
PDPair : FC -> PTerm -> PTerm -> PTerm -> PTerm PDPair : FC -> PTerm -> PTerm -> PTerm -> PTerm
@ -92,7 +93,7 @@ mutual
-- Debugging -- Debugging
PUnifyLog : FC -> PTerm -> PTerm PUnifyLog : FC -> PTerm -> PTerm
-- TODO: Ranges, idiom brackets (?), -- TODO: Idiom brackets (?),
-- 'with' disambiguation -- 'with' disambiguation
public export public export
@ -441,6 +442,7 @@ mutual
showPrec d (PBracketed _ tm) = "(" ++ showPrec d tm ++ ")" showPrec d (PBracketed _ tm) = "(" ++ showPrec d tm ++ ")"
showPrec d (PDoBlock _ ds) showPrec d (PDoBlock _ ds)
= "do " ++ showSep " ; " (map showDo ds) = "do " ++ showSep " ; " (map showDo ds)
showPrec d (PBang _ tm) = "!" ++ showPrec d tm
showPrec d (PList _ xs) showPrec d (PList _ xs)
= "[" ++ showSep ", " (map (showPrec d) xs) ++ "]" = "[" ++ showSep ", " (map (showPrec d) xs) ++ "]"
showPrec d (PPair _ l r) = "(" ++ showPrec d l ++ ", " ++ showPrec d r ++ ")" showPrec d (PPair _ l r) = "(" ++ showPrec d l ++ ", " ++ showPrec d r ++ ")"

3
src/Parser/Lexer.idr
View File

@ -131,7 +131,8 @@ export
reservedSymbols : List String reservedSymbols : List String
reservedSymbols reservedSymbols
= symbols ++ = symbols ++
["%", "\\", ":", "=", "|", "|||", "<-", "->", "=>", "?", "&", "**", ".."] ["%", "\\", ":", "=", "|", "|||", "<-", "->", "=>", "?", "!",
"&", "**", ".."]
symbolChar : Char -> Bool symbolChar : Char -> Bool
symbolChar c = c `elem` unpack opChars symbolChar c = c `elem` unpack opChars

2
tests/Main.idr
View File

@ -65,7 +65,7 @@ typeddTests
chezTests : List String chezTests : List String
chezTests chezTests
= ["chez001", "chez002", "chez003", "chez004", "chez005", "chez006", = ["chez001", "chez002", "chez003", "chez004", "chez005", "chez006",
"chez007", "chez008", "chez009", "chez010"] "chez007", "chez008", "chez009", "chez010", "chez011"]
ideModeTests : List String ideModeTests : List String
ideModeTests ideModeTests

33
tests/chez/chez011/bangs.idr Normal file
View File

@ -0,0 +1,33 @@
add : Int -> Int -> Int
add = (+)
-- lift to nearest binder
addm1 : Maybe Int -> Maybe Int -> Maybe Int
addm1 x y = let z = x in pure (add !z !y)
-- lift to nearest binder
addm2 : Maybe Int -> Maybe Int -> Maybe Int
addm2 = \x, y => pure (!x + !y)
getLen : String -> IO Nat
getLen str = pure (length str)
fakeGetLine : String -> IO String
fakeGetLine str = pure str
-- lift out innermost first
printThing1 : IO ()
printThing1 = printLn !(getLen !(fakeGetLine "line1"))
-- lift out leftmost first
printThing2 : IO ()
printThing2 = printLn (!(fakeGetLine "1") ++ !(fakeGetLine "2"))
-- don't lift out of if
printBool : Bool -> IO ()
printBool x
= if x
then putStrLn !(fakeGetLine "True")
else putStrLn !(fakeGetLine "False")

15
tests/chez/chez011/expected Normal file
View File

@ -0,0 +1,15 @@
5
"12"
True
False
____ __ _ ___
/ _/___/ /____(_)____ |__ \
/ // __ / ___/ / ___/ __/ / Version 0.0.0-9cd040fcb
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
/___/\__,_/_/ /_/____/ /____/
Welcome to Idris 2. Enjoy yourself!
1/1: Building bangs (bangs.idr)
Main> Just 7
Main> Just 7
Main> Main> Main> Main> Main> Bye for now!

7
tests/chez/chez011/input Normal file
View File

@ -0,0 +1,7 @@
addm1 (Just 3) (Just 4)
addm2 (Just 3) (Just 4)
:exec printThing1
:exec printThing2
:exec printBool True
:exec printBool False
:q

3
tests/chez/chez011/run Normal file
View File

@ -0,0 +1,3 @@
$1 bangs.idr < input
rm -rf build