mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-24 06:52:19 +03:00
[ new ] function options for case blocks (#3062)
This commit is contained in:
G. Allais
GitHub
parent
af7ba2fa67
commit
c52b029986
@ -257,6 +257,7 @@ modules =
|
||||
TTImp.ProcessDecls,
|
||||
TTImp.ProcessDecls.Totality,
|
||||
TTImp.ProcessDef,
|
||||
TTImp.ProcessFnOpt,
|
||||
TTImp.ProcessParams,
|
||||
TTImp.ProcessRecord,
|
||||
TTImp.ProcessRunElab,
|
||||
|
||||
@ -39,7 +39,7 @@ mutual
|
||||
ILet : FC -> (lhsFC : FC) -> Count -> Name ->
|
||||
(nTy : TTImp) -> (nVal : TTImp) ->
|
||||
(scope : TTImp) -> TTImp
|
||||
ICase : FC -> TTImp -> (ty : TTImp) ->
|
||||
ICase : FC -> List FnOpt -> TTImp -> (ty : TTImp) ->
|
||||
List Clause -> TTImp
|
||||
ILocal : FC -> List Decl -> TTImp -> TTImp
|
||||
IUpdate : FC -> List IFieldUpdate -> TTImp -> TTImp
|
||||
@ -203,7 +203,7 @@ getFC (IVar fc _) = fc
|
||||
getFC (IPi fc _ _ _ _ _) = fc
|
||||
getFC (ILam fc _ _ _ _ _) = fc
|
||||
getFC (ILet fc _ _ _ _ _ _) = fc
|
||||
getFC (ICase fc _ _ _) = fc
|
||||
getFC (ICase fc _ _ _ _) = fc
|
||||
getFC (ILocal fc _ _) = fc
|
||||
getFC (IUpdate fc _ _) = fc
|
||||
getFC (IApp fc _ _) = fc
|
||||
@ -236,7 +236,7 @@ mapTopmostFC fcf $ IVar fc a = IVar (fcf fc) a
|
||||
mapTopmostFC fcf $ IPi fc a b c d e = IPi (fcf fc) a b c d e
|
||||
mapTopmostFC fcf $ ILam fc a b c d e = ILam (fcf fc) a b c d e
|
||||
mapTopmostFC fcf $ ILet fc a b c d e f = ILet (fcf fc) a b c d e f
|
||||
mapTopmostFC fcf $ ICase fc a b c = ICase (fcf fc) a b c
|
||||
mapTopmostFC fcf $ ICase fc opts a b c = ICase (fcf fc) opts a b c
|
||||
mapTopmostFC fcf $ ILocal fc a b = ILocal (fcf fc) a b
|
||||
mapTopmostFC fcf $ IUpdate fc a b = IUpdate (fcf fc) a b
|
||||
mapTopmostFC fcf $ IApp fc a b = IApp (fcf fc) a b
|
||||
@ -403,7 +403,7 @@ Eq TTImp where
|
||||
c == c' && (assert_total $ i == i') && n == n' && a == a' && r == r'
|
||||
ILet _ _ c n ty val s == ILet _ _ c' n' ty' val' s' =
|
||||
c == c' && n == n' && ty == ty' && val == val' && s == s'
|
||||
ICase _ t ty cs == ICase _ t' ty' cs'
|
||||
ICase _ _ t ty cs == ICase _ _ t' ty' cs'
|
||||
= t == t' && ty == ty' && (assert_total $ cs == cs')
|
||||
ILocal _ ds e == ILocal _ ds' e' =
|
||||
(assert_total $ ds == ds') && e == e'
|
||||
@ -573,7 +573,7 @@ mutual
|
||||
showPrec d (ILet fc lhsFC rig nm nTy nVal scope)
|
||||
= showParens (d > Open) $
|
||||
"let \{showCount rig (show nm)} : \{show nTy} = \{show nVal} in \{show scope}"
|
||||
showPrec d (ICase fc s ty xs)
|
||||
showPrec d (ICase fc _ s ty xs)
|
||||
= showParens (d > Open) $
|
||||
unwords $ [ "case", show s ] ++ typeFor ty ++ [ "of", "{"
|
||||
, joinBy "; " (assert_total $ map (showClause InCase) xs)
|
||||
@ -783,8 +783,8 @@ parameters (f : TTImp -> TTImp)
|
||||
= f $ ILam fc rig (mapPiInfo pinfo) x (mapTTImp argTy) (mapTTImp lamTy)
|
||||
mapTTImp (ILet fc lhsFC rig n nTy nVal scope)
|
||||
= f $ ILet fc lhsFC rig n (mapTTImp nTy) (mapTTImp nVal) (mapTTImp scope)
|
||||
mapTTImp (ICase fc t ty cls)
|
||||
= f $ ICase fc (mapTTImp t) (mapTTImp ty) (assert_total $ map mapClause cls)
|
||||
mapTTImp (ICase fc opts t ty cls)
|
||||
= f $ ICase fc opts (mapTTImp t) (mapTTImp ty) (assert_total $ map mapClause cls)
|
||||
mapTTImp (ILocal fc xs t)
|
||||
= f $ ILocal fc (assert_total $ map mapDecl xs) (mapTTImp t)
|
||||
mapTTImp (IUpdate fc upds t) = f $ IUpdate fc (assert_total map mapIFieldUpdate upds) (mapTTImp t)
|
||||
@ -909,8 +909,8 @@ parameters {0 m : Type -> Type} {auto mon : Monad m} (f : TTImp -> m TTImp)
|
||||
= f =<< ILam fc rig <$> mapMPiInfo pinfo <*> pure x <*> mapMTTImp argTy <*> mapMTTImp lamTy
|
||||
mapMTTImp (ILet fc lhsFC rig n nTy nVal scope)
|
||||
= f =<< ILet fc lhsFC rig n <$> mapMTTImp nTy <*> mapMTTImp nVal <*> mapMTTImp scope
|
||||
mapMTTImp (ICase fc t ty cls)
|
||||
= f =<< ICase fc <$> mapMTTImp t <*> mapMTTImp ty <*> assert_total (traverse mapMClause cls)
|
||||
mapMTTImp (ICase fc opts t ty cls)
|
||||
= f =<< ICase fc opts <$> mapMTTImp t <*> mapMTTImp ty <*> assert_total (traverse mapMClause cls)
|
||||
mapMTTImp (ILocal fc xs t)
|
||||
= f =<< ILocal fc <$> assert_total (traverse mapMDecl xs) <*> mapMTTImp t
|
||||
mapMTTImp (IUpdate fc upds t)
|
||||
|
||||
@ -29,7 +29,7 @@ import public Libraries.Utils.Binary
|
||||
||| version number if you're changing the version more than once in the same day.
|
||||
export
|
||||
ttcVersion : Int
|
||||
ttcVersion = 20230414 * 100 + 0
|
||||
ttcVersion = 20230829 * 100 + 0
|
||||
|
||||
export
|
||||
checkTTCVersion : String -> Int -> Int -> Core ()
|
||||
|
||||
@ -245,7 +245,7 @@ mutual
|
||||
!(desugar AnyExpr (n :: ps) scope)
|
||||
else pure $ ILam EmptyFC rig !(traverse (desugar AnyExpr ps) p)
|
||||
(Just (MN "lamc" 0)) !(desugarB AnyExpr ps argTy) $
|
||||
ICase fc (IVar EmptyFC (MN "lamc" 0)) (Implicit fc False)
|
||||
ICase fc [] (IVar EmptyFC (MN "lamc" 0)) (Implicit fc False)
|
||||
[snd !(desugarClause ps True (MkPatClause fc pat scope []))]
|
||||
desugarB side ps (PLam fc rig p (PRef _ n@(MN _ _)) argTy scope)
|
||||
= pure $ ILam fc rig !(traverse (desugar AnyExpr ps) p)
|
||||
@ -258,7 +258,7 @@ mutual
|
||||
desugarB side ps (PLam fc rig p pat argTy scope)
|
||||
= pure $ ILam EmptyFC rig !(traverse (desugar AnyExpr ps) p)
|
||||
(Just (MN "lamc" 0)) !(desugarB AnyExpr ps argTy) $
|
||||
ICase fc (IVar EmptyFC (MN "lamc" 0)) (Implicit fc False)
|
||||
ICase fc [] (IVar EmptyFC (MN "lamc" 0)) (Implicit fc False)
|
||||
[snd !(desugarClause ps True (MkPatClause fc pat scope []))]
|
||||
desugarB side ps (PLet fc rig (PRef prefFC n) nTy nVal scope [])
|
||||
= do whenJust (isConcreteFC prefFC) $ \nfc =>
|
||||
@ -266,13 +266,15 @@ mutual
|
||||
pure $ ILet fc prefFC rig n !(desugarB side ps nTy) !(desugarB side ps nVal)
|
||||
!(desugar side (n :: ps) scope)
|
||||
desugarB side ps (PLet fc rig pat nTy nVal scope alts)
|
||||
= pure $ ICase fc !(desugarB side ps nVal) !(desugarB side ps nTy)
|
||||
= pure $ ICase fc [] !(desugarB side ps nVal) !(desugarB side ps nTy)
|
||||
!(traverse (map snd . desugarClause ps True)
|
||||
(MkPatClause fc pat scope [] :: alts))
|
||||
desugarB side ps (PCase fc x xs)
|
||||
= pure $ ICase fc !(desugarB side ps x)
|
||||
(Implicit (virtualiseFC fc) False)
|
||||
!(traverse (map snd . desugarClause ps True) xs)
|
||||
desugarB side ps (PCase fc opts scr cls)
|
||||
= do opts <- traverse (desugarFnOpt ps) opts
|
||||
scr <- desugarB side ps scr
|
||||
let scrty = Implicit (virtualiseFC fc) False
|
||||
cls <- traverse (map snd . desugarClause ps True) cls
|
||||
pure $ ICase fc opts scr scrty cls
|
||||
desugarB side ps (PLocal fc xs scope)
|
||||
= let ps' = definedIn xs ++ ps in
|
||||
pure $ ILocal fc (concat !(traverse (desugarDecl ps') xs))
|
||||
@ -454,7 +456,7 @@ mutual
|
||||
IVar fc (UN $ Basic "MkUnit")]
|
||||
desugarB side ps (PIfThenElse fc x t e)
|
||||
= let fc = virtualiseFC fc in
|
||||
pure $ ICase fc !(desugarB side ps x) (IVar fc (UN $ Basic "Bool"))
|
||||
pure $ ICase fc [] !(desugarB side ps x) (IVar fc (UN $ Basic "Bool"))
|
||||
[PatClause fc (IVar fc (UN $ Basic "True")) !(desugar side ps t),
|
||||
PatClause fc (IVar fc (UN $ Basic "False")) !(desugar side ps e)]
|
||||
desugarB side ps (PComprehension fc ret conds) = do
|
||||
@ -674,7 +676,7 @@ mutual
|
||||
pure $ bindFun fc ns exp'
|
||||
$ ILam EmptyFC top Explicit (Just (MN "_" 0))
|
||||
(Implicit fc False)
|
||||
(ICase fc (IVar patFC (MN "_" 0))
|
||||
(ICase fc [] (IVar patFC (MN "_" 0))
|
||||
(Implicit fc False)
|
||||
(PatClause fcOriginal bpat rest'
|
||||
:: alts'))
|
||||
@ -700,7 +702,7 @@ mutual
|
||||
bd <- get Bang
|
||||
let fc = virtualiseFC fc
|
||||
pure $ bindBangs (bangNames bd) ns $
|
||||
ICase fc tm' ty'
|
||||
ICase fc [] tm' ty'
|
||||
(PatClause fc bpat rest'
|
||||
:: alts')
|
||||
expandDo side ps topfc ns (DoLetLocal fc decls :: rest)
|
||||
|
||||
@ -211,6 +211,17 @@ debugString fname = do
|
||||
DebugLine => "\{show (startLine di.bounds)}"
|
||||
DebugCol => "\{show (startCol di.bounds)}"
|
||||
|
||||
totalityOpt : OriginDesc -> Rule TotalReq
|
||||
totalityOpt fname
|
||||
= (decoratedKeyword fname "partial" $> PartialOK)
|
||||
<|> (decoratedKeyword fname "total" $> Total)
|
||||
<|> (decoratedKeyword fname "covering" $> CoveringOnly)
|
||||
|
||||
fnOpt : OriginDesc -> Rule PFnOpt
|
||||
fnOpt fname
|
||||
= do x <- totalityOpt fname
|
||||
pure $ IFnOpt (Totality x)
|
||||
|
||||
mutual
|
||||
appExpr : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
|
||||
appExpr q fname indents
|
||||
@ -753,7 +764,7 @@ mutual
|
||||
fcCase = virtualiseFC $ boundToFC fname endCase
|
||||
n = MN "lcase" 0 in
|
||||
PLam fcCase top Explicit (PRef fcCase n) (PInfer fcCase) $
|
||||
PCase (virtualiseFC fc) (PRef fcCase n) b.val)
|
||||
PCase (virtualiseFC fc) [] (PRef fcCase n) b.val)
|
||||
|
||||
letBlock : OriginDesc -> IndentInfo -> Rule (WithBounds (Either LetBinder LetDecl))
|
||||
letBlock fname indents = bounds (letBinder <||> letDecl) where
|
||||
@ -782,13 +793,14 @@ mutual
|
||||
|
||||
case_ : OriginDesc -> IndentInfo -> Rule PTerm
|
||||
case_ fname indents
|
||||
= do b <- bounds (do decoratedKeyword fname "case"
|
||||
= do opts <- many (fnDirectOpt fname)
|
||||
b <- bounds (do decoratedKeyword fname "case"
|
||||
scr <- expr pdef fname indents
|
||||
mustWork (commitKeyword fname indents "of")
|
||||
alts <- block (caseAlt fname)
|
||||
pure (scr, alts))
|
||||
(scr, alts) <- pure b.val
|
||||
pure (PCase (virtualiseFC $ boundToFC fname b) scr alts)
|
||||
pure (PCase (virtualiseFC $ boundToFC fname b) opts scr alts)
|
||||
|
||||
|
||||
caseAlt : OriginDesc -> IndentInfo -> Rule PClause
|
||||
@ -1055,6 +1067,52 @@ mutual
|
||||
$ acc :< (line <>> [StrLiteral fc str])
|
||||
<>< map (\str => [StrLiteral fc str]) (init strs)
|
||||
|
||||
fnDirectOpt : OriginDesc -> Rule PFnOpt
|
||||
fnDirectOpt fname
|
||||
= do decoratedPragma fname "hint"
|
||||
pure $ IFnOpt (Hint True)
|
||||
<|> do decoratedPragma fname "globalhint"
|
||||
pure $ IFnOpt (GlobalHint False)
|
||||
<|> do decoratedPragma fname "defaulthint"
|
||||
pure $ IFnOpt (GlobalHint True)
|
||||
<|> do decoratedPragma fname "inline"
|
||||
commit
|
||||
pure $ IFnOpt Inline
|
||||
<|> do decoratedPragma fname "unsafe"
|
||||
commit
|
||||
pure $ IFnOpt Unsafe
|
||||
<|> do decoratedPragma fname "noinline"
|
||||
commit
|
||||
pure $ IFnOpt NoInline
|
||||
<|> do decoratedPragma fname "deprecate"
|
||||
commit
|
||||
pure $ IFnOpt Deprecate
|
||||
<|> do decoratedPragma fname "tcinline"
|
||||
commit
|
||||
pure $ IFnOpt TCInline
|
||||
<|> do decoratedPragma fname "extern"
|
||||
pure $ IFnOpt ExternFn
|
||||
<|> do decoratedPragma fname "macro"
|
||||
pure $ IFnOpt Macro
|
||||
<|> do decoratedPragma fname "spec"
|
||||
ns <- sepBy (decoratedSymbol fname ",") name
|
||||
pure $ IFnOpt (SpecArgs ns)
|
||||
<|> do decoratedPragma fname "foreign"
|
||||
cs <- block (expr pdef fname)
|
||||
pure $ PForeign cs
|
||||
<|> do (decoratedPragma fname "export"
|
||||
<|> withWarning noMangleWarning
|
||||
(decoratedPragma fname "nomangle"))
|
||||
cs <- block (expr pdef fname)
|
||||
pure $ PForeignExport cs
|
||||
where
|
||||
noMangleWarning : String
|
||||
noMangleWarning = """
|
||||
DEPRECATED: "%nomangle".
|
||||
Use "%export" instead
|
||||
"""
|
||||
|
||||
|
||||
visOption : OriginDesc -> Rule Visibility
|
||||
visOption fname
|
||||
= (decoratedKeyword fname "public" *> decoratedKeyword fname "export" $> Public)
|
||||
@ -1268,12 +1326,6 @@ dataDeclBody fname indents
|
||||
(col, n) <- pure b.val
|
||||
simpleData fname b n indents <|> gadtData fname col b n indents
|
||||
|
||||
totalityOpt : OriginDesc -> Rule TotalReq
|
||||
totalityOpt fname
|
||||
= (decoratedKeyword fname "partial" $> PartialOK)
|
||||
<|> (decoratedKeyword fname "total" $> Total)
|
||||
<|> (decoratedKeyword fname "covering" $> CoveringOnly)
|
||||
|
||||
-- a data declaration can have a visibility and an optional totality (#1404)
|
||||
dataVisOpt : OriginDesc -> EmptyRule (Visibility, Maybe TotalReq)
|
||||
dataVisOpt fname
|
||||
@ -1507,56 +1559,6 @@ usingDecls fname indents
|
||||
(us, ds) <- pure b.val
|
||||
pure (PUsing (boundToFC fname b) us (collectDefs (concat ds)))
|
||||
|
||||
fnOpt : OriginDesc -> Rule PFnOpt
|
||||
fnOpt fname
|
||||
= do x <- totalityOpt fname
|
||||
pure $ IFnOpt (Totality x)
|
||||
|
||||
fnDirectOpt : OriginDesc -> Rule PFnOpt
|
||||
fnDirectOpt fname
|
||||
= do decoratedPragma fname "hint"
|
||||
pure $ IFnOpt (Hint True)
|
||||
<|> do decoratedPragma fname "globalhint"
|
||||
pure $ IFnOpt (GlobalHint False)
|
||||
<|> do decoratedPragma fname "defaulthint"
|
||||
pure $ IFnOpt (GlobalHint True)
|
||||
<|> do decoratedPragma fname "inline"
|
||||
commit
|
||||
pure $ IFnOpt Inline
|
||||
<|> do decoratedPragma fname "unsafe"
|
||||
commit
|
||||
pure $ IFnOpt Unsafe
|
||||
<|> do decoratedPragma fname "noinline"
|
||||
commit
|
||||
pure $ IFnOpt NoInline
|
||||
<|> do decoratedPragma fname "deprecate"
|
||||
commit
|
||||
pure $ IFnOpt Deprecate
|
||||
<|> do decoratedPragma fname "tcinline"
|
||||
commit
|
||||
pure $ IFnOpt TCInline
|
||||
<|> do decoratedPragma fname "extern"
|
||||
pure $ IFnOpt ExternFn
|
||||
<|> do decoratedPragma fname "macro"
|
||||
pure $ IFnOpt Macro
|
||||
<|> do decoratedPragma fname "spec"
|
||||
ns <- sepBy (decoratedSymbol fname ",") name
|
||||
pure $ IFnOpt (SpecArgs ns)
|
||||
<|> do decoratedPragma fname "foreign"
|
||||
cs <- block (expr pdef fname)
|
||||
pure $ PForeign cs
|
||||
<|> do (decoratedPragma fname "export"
|
||||
<|> withWarning noMangleWarning
|
||||
(decoratedPragma fname "nomangle"))
|
||||
cs <- block (expr pdef fname)
|
||||
pure $ PForeignExport cs
|
||||
where
|
||||
noMangleWarning : String
|
||||
noMangleWarning = """
|
||||
DEPRECATED: "%nomangle".
|
||||
Use "%export" instead
|
||||
"""
|
||||
|
||||
builtinDecl : OriginDesc -> IndentInfo -> Rule PDecl
|
||||
builtinDecl fname indents
|
||||
= do b <- bounds (do decoratedPragma fname "builtin"
|
||||
|
||||
@ -281,7 +281,7 @@ mutual
|
||||
; _ => hardline <+> indent 4 (vsep (prettyAlt <$> alts)) <+> hardline <+> in_
|
||||
}
|
||||
<+> group (align $ hang 2 $ pretty sc)
|
||||
prettyPrec d (PCase _ tm cs) =
|
||||
prettyPrec d (PCase _ _ tm cs) =
|
||||
parenthesise (d > startPrec) $
|
||||
case_ <++> pretty tm <++> of_ <+> nest 2 (
|
||||
let punctuation = lcurly :: (semi <$ fromMaybe [] (tail' [1..length cs])) in
|
||||
|
||||
@ -315,20 +315,22 @@ mutual
|
||||
sc' <- toPTerm startPrec sc
|
||||
let var = PRef lhsFC (MkKindedName (Just Bound) n n)
|
||||
bracket p startPrec (PLet fc rig var ty' val' sc' [])
|
||||
toPTerm p (ICase fc sc scty [PatClause _ lhs rhs])
|
||||
toPTerm p (ICase fc _ sc scty [PatClause _ lhs rhs])
|
||||
= do sc' <- toPTerm startPrec sc
|
||||
lhs' <- toPTerm startPrec lhs
|
||||
rhs' <- toPTerm startPrec rhs
|
||||
bracket p startPrec
|
||||
(PLet fc top lhs' (PImplicit fc) sc' rhs' [])
|
||||
toPTerm p (ICase fc sc scty alts)
|
||||
= do sc' <- toPTerm startPrec sc
|
||||
toPTerm p (ICase fc opts sc scty alts)
|
||||
= do opts' <- traverse toPFnOpt opts
|
||||
sc' <- toPTerm startPrec sc
|
||||
alts' <- traverse toPClause alts
|
||||
bracket p startPrec (mkIf (PCase fc sc' alts'))
|
||||
bracket p startPrec (mkIf (PCase fc opts' sc' alts'))
|
||||
where
|
||||
mkIf : IPTerm -> IPTerm
|
||||
mkIf tm@(PCase loc sc [MkPatClause _ (PRef _ tval) t [],
|
||||
MkPatClause _ (PRef _ fval) f []])
|
||||
mkIf tm@(PCase loc opts sc
|
||||
[ MkPatClause _ (PRef _ tval) t []
|
||||
, MkPatClause _ (PRef _ fval) f []])
|
||||
= if dropNS (rawName tval) == UN (Basic "True")
|
||||
&& dropNS (rawName fval) == UN (Basic "False")
|
||||
then PIfThenElse loc sc t f
|
||||
|
||||
@ -107,7 +107,7 @@ mutual
|
||||
PLet : FC -> RigCount -> (pat : PTerm' nm) ->
|
||||
(nTy : PTerm' nm) -> (nVal : PTerm' nm) -> (scope : PTerm' nm) ->
|
||||
(alts : List (PClause' nm)) -> PTerm' nm
|
||||
PCase : FC -> PTerm' nm -> List (PClause' nm) -> PTerm' nm
|
||||
PCase : FC -> List (PFnOpt' nm) -> PTerm' nm -> List (PClause' nm) -> PTerm' nm
|
||||
PLocal : FC -> List (PDecl' nm) -> (scope : PTerm' nm) -> PTerm' nm
|
||||
PUpdate : FC -> List (PFieldUpdate' nm) -> PTerm' nm
|
||||
PApp : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm
|
||||
@ -178,7 +178,7 @@ mutual
|
||||
getPTermLoc (PPi fc _ _ _ _ _) = fc
|
||||
getPTermLoc (PLam fc _ _ _ _ _) = fc
|
||||
getPTermLoc (PLet fc _ _ _ _ _ _) = fc
|
||||
getPTermLoc (PCase fc _ _) = fc
|
||||
getPTermLoc (PCase fc _ _ _) = fc
|
||||
getPTermLoc (PLocal fc _ _) = fc
|
||||
getPTermLoc (PUpdate fc _) = fc
|
||||
getPTermLoc (PApp fc _ _) = fc
|
||||
@ -755,7 +755,7 @@ parameters {0 nm : Type} (toName : nm -> Name)
|
||||
= "let " ++ showCount rig ++ showPTermPrec d n ++ " : " ++ showPTermPrec d ty ++ " = "
|
||||
++ showPTermPrec d val ++ concatMap showAlt alts ++
|
||||
" in " ++ showPTermPrec d sc
|
||||
showPTermPrec _ (PCase _ tm cs)
|
||||
showPTermPrec _ (PCase _ _ tm cs)
|
||||
= "case " ++ showPTerm tm ++ " of { " ++
|
||||
showSep " ; " (map showCase cs) ++ " }"
|
||||
where
|
||||
|
||||
@ -36,8 +36,9 @@ mapPTermM f = goPTerm where
|
||||
<*> goPTerm scope
|
||||
<*> goPClauses alts
|
||||
>>= f
|
||||
goPTerm (PCase fc x xs) =
|
||||
PCase fc <$> goPTerm x
|
||||
goPTerm (PCase fc opts x xs) =
|
||||
PCase fc <$> goPFnOpts opts
|
||||
<*> goPTerm x
|
||||
<*> goPClauses xs
|
||||
>>= f
|
||||
goPTerm (PLocal fc xs scope) =
|
||||
@ -395,8 +396,8 @@ mapPTerm f = goPTerm where
|
||||
= f $ PLam fc x (goPiInfo info) z (goPTerm argTy) (goPTerm scope)
|
||||
goPTerm (PLet fc x pat nTy nVal scope alts)
|
||||
= f $ PLet fc x (goPTerm pat) (goPTerm nTy) (goPTerm nVal) (goPTerm scope) (goPClause <$> alts)
|
||||
goPTerm (PCase fc x xs)
|
||||
= f $ PCase fc (goPTerm x) (goPClause <$> xs)
|
||||
goPTerm (PCase fc opts x xs)
|
||||
= f $ PCase fc (goPFnOpt <$> opts) (goPTerm x) (goPClause <$> xs)
|
||||
goPTerm (PLocal fc xs scope)
|
||||
= f $ PLocal fc (goPDecl <$> xs) (goPTerm scope)
|
||||
goPTerm (PUpdate fc xs)
|
||||
@ -596,7 +597,7 @@ substFC fc = mapPTerm $ \case
|
||||
PPi _ x y z argTy retTy => PPi fc x y z argTy retTy
|
||||
PLam _ x y pat argTy scope => PLam fc x y pat argTy scope
|
||||
PLet _ x pat nTy nVal scope alts => PLet fc x pat nTy nVal scope alts
|
||||
PCase _ x xs => PCase fc x xs
|
||||
PCase _ opts x xs => PCase fc opts x xs
|
||||
PLocal _ xs scope => PLocal fc xs scope
|
||||
PUpdate _ xs => PUpdate fc xs
|
||||
PApp _ x y => PApp fc x y
|
||||
|
||||
@ -306,7 +306,7 @@ mutual
|
||||
needsDelayExpr True (IAutoApp _ f _) = needsDelayExpr True f
|
||||
needsDelayExpr True (INamedApp _ f _ _) = needsDelayExpr True f
|
||||
needsDelayExpr True (ILam _ _ _ _ _ _) = pure True
|
||||
needsDelayExpr True (ICase _ _ _ _) = pure True
|
||||
needsDelayExpr True (ICase _ _ _ _ _) = pure True
|
||||
needsDelayExpr True (ILocal _ _ _) = pure True
|
||||
needsDelayExpr True (IUpdate _ _ _) = pure True
|
||||
needsDelayExpr True (IAlternative _ _ _) = pure True
|
||||
|
||||
@ -17,6 +17,7 @@ import TTImp.Elab.Check
|
||||
import TTImp.Elab.Delayed
|
||||
import TTImp.Elab.ImplicitBind
|
||||
import TTImp.Elab.Utils
|
||||
import TTImp.ProcessFnOpt
|
||||
import TTImp.TTImp
|
||||
import TTImp.Utils
|
||||
|
||||
@ -165,13 +166,14 @@ caseBlock : {vars : _} ->
|
||||
ElabInfo -> FC ->
|
||||
NestedNames vars ->
|
||||
Env Term vars ->
|
||||
List FnOpt ->
|
||||
RawImp -> -- original scrutinee
|
||||
Term vars -> -- checked scrutinee
|
||||
Term vars -> -- its type
|
||||
RigCount -> -- its multiplicity
|
||||
List ImpClause -> Maybe (Glued vars) ->
|
||||
Core (Term vars, Glued vars)
|
||||
caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
|
||||
caseBlock {vars} rigc elabinfo fc nest env opts scr scrtm scrty caseRig alts expected
|
||||
= do -- TODO (or to decide): Blodwen allowed ambiguities in the scrutinee
|
||||
-- to be delayed, but now I think it's better to have simpler
|
||||
-- resolution rules, and not delay
|
||||
@ -235,6 +237,8 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
|
||||
(newDef fc casen (if isErased rigc then erased else top)
|
||||
[] casefnty vis None))
|
||||
|
||||
traverse_ (processFnOpt fc False casen) opts
|
||||
|
||||
-- set the totality of the case block to be the same as that
|
||||
-- of the parent function
|
||||
let tot = fromMaybe PartialOK $ do findSetTotal (flags !parentDef)
|
||||
@ -384,10 +388,10 @@ checkCase : {vars : _} ->
|
||||
{auto o : Ref ROpts REPLOpts} ->
|
||||
RigCount -> ElabInfo ->
|
||||
NestedNames vars -> Env Term vars ->
|
||||
FC -> (scr : RawImp) -> (ty : RawImp) -> List ImpClause ->
|
||||
FC -> List FnOpt -> (scr : RawImp) -> (ty : RawImp) -> List ImpClause ->
|
||||
Maybe (Glued vars) ->
|
||||
Core (Term vars, Glued vars)
|
||||
checkCase rig elabinfo nest env fc scr scrty_in alts exp
|
||||
checkCase rig elabinfo nest env fc opts scr scrty_in alts exp
|
||||
= delayElab fc rig env exp CaseBlock $
|
||||
do scrty_exp <- case scrty_in of
|
||||
Implicit _ _ => guessScrType alts
|
||||
@ -419,7 +423,7 @@ checkCase rig elabinfo nest env fc scr scrty_in alts exp
|
||||
logTermNF "elab.case" 5 "Scrutinee type" env scrty
|
||||
defs <- get Ctxt
|
||||
checkConcrete !(nf defs env scrty)
|
||||
caseBlock rig elabinfo fc nest env scr scrtm_in scrty caseRig alts exp
|
||||
caseBlock rig elabinfo fc nest env opts scr scrtm_in scrty caseRig alts exp
|
||||
where
|
||||
-- For the moment, throw an error if we haven't been able to work out
|
||||
-- the type of the case scrutinee, because we'll need it to build the
|
||||
|
||||
@ -35,9 +35,10 @@ mutual
|
||||
= pure $ ILam fc c p n !(getUnquote arg) !(getUnquote sc)
|
||||
getUnquote (ILet fc lhsFC c n ty val sc)
|
||||
= pure $ ILet fc lhsFC c n !(getUnquote ty) !(getUnquote val) !(getUnquote sc)
|
||||
getUnquote (ICase fc sc ty cs)
|
||||
= pure $ ICase fc !(getUnquote sc) !(getUnquote ty)
|
||||
!(traverse getUnquoteClause cs)
|
||||
getUnquote (ICase fc opts sc ty cs)
|
||||
= pure $ ICase fc opts
|
||||
!(getUnquote sc) !(getUnquote ty)
|
||||
!(traverse getUnquoteClause cs)
|
||||
getUnquote (ILocal fc ds sc)
|
||||
= pure $ ILocal fc !(traverse getUnquoteDecl ds) !(getUnquote sc)
|
||||
getUnquote (IUpdate fc ds sc)
|
||||
|
||||
@ -196,7 +196,7 @@ recUpdate rigc elabinfo iloc nest env flds rec grecty
|
||||
fldn <- genFieldName "__fld"
|
||||
sides <- getAllSides iloc flds rectyn rec
|
||||
(Field Nothing fldn (IVar vloc (UN $ Basic fldn)))
|
||||
pure $ ICase vloc rec (Implicit vloc False) [mkClause sides]
|
||||
pure $ ICase vloc [] rec (Implicit vloc False) [mkClause sides]
|
||||
where
|
||||
vloc : FC
|
||||
vloc = virtualiseFC iloc
|
||||
|
||||
@ -146,8 +146,8 @@ checkTerm rig elabinfo nest env (ILam fc r p Nothing argTy scope) exp
|
||||
checkLambda rig elabinfo nest env fc r p n argTy scope exp
|
||||
checkTerm rig elabinfo nest env (ILet fc lhsFC r n nTy nVal scope) exp
|
||||
= checkLet rig elabinfo nest env fc lhsFC r n nTy nVal scope exp
|
||||
checkTerm rig elabinfo nest env (ICase fc scr scrty alts) exp
|
||||
= checkCase rig elabinfo nest env fc scr scrty alts exp
|
||||
checkTerm rig elabinfo nest env (ICase fc opts scr scrty alts) exp
|
||||
= checkCase rig elabinfo nest env fc opts scr scrty alts exp
|
||||
checkTerm rig elabinfo nest env (ILocal fc nested scope) exp
|
||||
= checkLocal rig elabinfo nest env fc nested scope exp
|
||||
checkTerm rig elabinfo nest env (ICaseLocal fc uname iname args scope) exp
|
||||
|
||||
@ -376,13 +376,14 @@ mutual
|
||||
case_ : OriginDesc -> IndentInfo -> Rule RawImp
|
||||
case_ fname indents
|
||||
= do start <- location
|
||||
opts <- many fnOpt
|
||||
keyword "case"
|
||||
scr <- expr fname indents
|
||||
keyword "of"
|
||||
alts <- block (caseAlt fname)
|
||||
end <- location
|
||||
pure (let fc = MkFC fname start end in
|
||||
ICase fc scr (Implicit fc False) alts)
|
||||
ICase fc opts scr (Implicit fc False) alts)
|
||||
|
||||
caseAlt : OriginDesc -> IndentInfo -> Rule ImpClause
|
||||
caseAlt fname indents
|
||||
|
||||
180
src/TTImp/ProcessFnOpt.idr
Normal file
180
src/TTImp/ProcessFnOpt.idr
Normal file
@ -0,0 +1,180 @@
|
||||
module TTImp.ProcessFnOpt
|
||||
|
||||
import Core.Context
|
||||
import Core.Context.Log
|
||||
import Core.Env
|
||||
import Core.Normalise
|
||||
import Core.Value
|
||||
|
||||
import TTImp.TTImp
|
||||
|
||||
import Libraries.Data.NameMap
|
||||
|
||||
getRetTy : Defs -> NF [] -> Core Name
|
||||
getRetTy defs (NBind fc _ (Pi _ _ _ _) sc)
|
||||
= getRetTy defs !(sc defs (toClosure defaultOpts [] (Erased fc Placeholder)))
|
||||
getRetTy defs (NTCon _ n _ _ _) = pure n
|
||||
getRetTy defs ty
|
||||
= throw (GenericMsg (getLoc ty)
|
||||
"Can only add hints for concrete return types")
|
||||
|
||||
throwIfHasFlag : {auto c : Ref Ctxt Defs} -> FC -> Name -> DefFlag -> String -> Core ()
|
||||
throwIfHasFlag fc ndef fl msg
|
||||
= when !(hasFlag fc ndef fl) $ throw (GenericMsg fc msg)
|
||||
|
||||
export
|
||||
processFnOpt : {auto c : Ref Ctxt Defs} ->
|
||||
FC -> Bool -> -- ^ top level name?
|
||||
Name -> FnOpt -> Core ()
|
||||
processFnOpt fc _ ndef Unsafe
|
||||
= do setIsEscapeHatch fc ndef
|
||||
processFnOpt fc _ ndef Inline
|
||||
= do throwIfHasFlag fc ndef NoInline "%noinline and %inline are mutually exclusive"
|
||||
setFlag fc ndef Inline
|
||||
processFnOpt fc _ ndef NoInline
|
||||
= do throwIfHasFlag fc ndef Inline "%inline and %noinline are mutually exclusive"
|
||||
setFlag fc ndef NoInline
|
||||
processFnOpt fc _ ndef Deprecate
|
||||
= setFlag fc ndef Deprecate
|
||||
processFnOpt fc _ ndef TCInline
|
||||
= setFlag fc ndef TCInline
|
||||
processFnOpt fc True ndef (Hint d)
|
||||
= do defs <- get Ctxt
|
||||
Just ty <- lookupTyExact ndef (gamma defs)
|
||||
| Nothing => undefinedName fc ndef
|
||||
target <- getRetTy defs !(nf defs [] ty)
|
||||
addHintFor fc target ndef d False
|
||||
processFnOpt fc _ ndef (Hint d)
|
||||
= do logC "elab" 5 $ do pure $ "Adding local hint " ++ show !(toFullNames ndef)
|
||||
addLocalHint ndef
|
||||
processFnOpt fc True ndef (GlobalHint a)
|
||||
= addGlobalHint ndef a
|
||||
processFnOpt fc _ ndef (GlobalHint a)
|
||||
= throw (GenericMsg fc "%globalhint is not valid in local definitions")
|
||||
processFnOpt fc _ ndef ExternFn
|
||||
= setFlag fc ndef Inline -- if externally defined, inline when compiling
|
||||
processFnOpt fc _ ndef (ForeignFn _)
|
||||
= setFlag fc ndef Inline -- if externally defined, inline when compiling
|
||||
processFnOpt fc _ ndef (ForeignExport _)
|
||||
= pure ()
|
||||
processFnOpt fc _ ndef Invertible
|
||||
= setFlag fc ndef Invertible
|
||||
processFnOpt fc _ ndef (Totality tot)
|
||||
= setFlag fc ndef (SetTotal tot)
|
||||
processFnOpt fc _ ndef Macro
|
||||
= setFlag fc ndef Macro
|
||||
processFnOpt fc _ ndef (SpecArgs ns)
|
||||
= do defs <- get Ctxt
|
||||
Just gdef <- lookupCtxtExact ndef (gamma defs)
|
||||
| Nothing => undefinedName fc ndef
|
||||
nty <- nf defs [] (type gdef)
|
||||
ps <- getNamePos 0 nty
|
||||
ddeps <- collectDDeps nty
|
||||
specs <- collectSpec [] ddeps ps nty
|
||||
ignore $ addDef ndef ({ specArgs := specs } gdef)
|
||||
where
|
||||
insertDeps : List Nat -> List (Name, Nat) -> List Name -> List Nat
|
||||
insertDeps acc ps [] = acc
|
||||
insertDeps acc ps (n :: ns)
|
||||
= case lookup n ps of
|
||||
Nothing => insertDeps acc ps ns
|
||||
Just pos => if pos `elem` acc
|
||||
then insertDeps acc ps ns
|
||||
else insertDeps (pos :: acc) ps ns
|
||||
|
||||
-- Collect the argument names which the dynamic args depend on
|
||||
collectDDeps : NF [] -> Core (List Name)
|
||||
collectDDeps (NBind tfc x (Pi _ _ _ nty) sc)
|
||||
= do defs <- get Ctxt
|
||||
empty <- clearDefs defs
|
||||
sc' <- sc defs (toClosure defaultOpts [] (Ref tfc Bound x))
|
||||
if x `elem` ns
|
||||
then collectDDeps sc'
|
||||
else do aty <- quote empty [] nty
|
||||
-- Get names depended on by nty
|
||||
let deps = keys (getRefs (UN Underscore) aty)
|
||||
rest <- collectDDeps sc'
|
||||
pure (rest ++ deps)
|
||||
collectDDeps _ = pure []
|
||||
|
||||
-- Return names the type depends on, and whether it's a parameter
|
||||
mutual
|
||||
getDepsArgs : Bool -> List (NF []) -> NameMap Bool ->
|
||||
Core (NameMap Bool)
|
||||
getDepsArgs inparam [] ns = pure ns
|
||||
getDepsArgs inparam (a :: as) ns
|
||||
= do ns' <- getDeps inparam a ns
|
||||
getDepsArgs inparam as ns'
|
||||
|
||||
getDeps : Bool -> NF [] -> NameMap Bool ->
|
||||
Core (NameMap Bool)
|
||||
getDeps inparam (NBind _ x (Pi _ _ _ pty) sc) ns
|
||||
= do defs <- get Ctxt
|
||||
ns' <- getDeps inparam !(evalClosure defs pty) ns
|
||||
sc' <- sc defs (toClosure defaultOpts [] (Erased fc Placeholder))
|
||||
getDeps inparam sc' ns'
|
||||
getDeps inparam (NBind _ x b sc) ns
|
||||
= do defs <- get Ctxt
|
||||
ns' <- getDeps False !(evalClosure defs (binderType b)) ns
|
||||
sc' <- sc defs (toClosure defaultOpts [] (Erased fc Placeholder))
|
||||
getDeps False sc' ns
|
||||
getDeps inparam (NApp _ (NRef Bound n) args) ns
|
||||
= do defs <- get Ctxt
|
||||
ns' <- getDepsArgs False !(traverse (evalClosure defs . snd) args) ns
|
||||
pure (insert n inparam ns')
|
||||
getDeps inparam (NDCon _ n t a args) ns
|
||||
= do defs <- get Ctxt
|
||||
getDepsArgs False !(traverse (evalClosure defs . snd) args) ns
|
||||
getDeps inparam (NTCon _ n t a args) ns
|
||||
= do defs <- get Ctxt
|
||||
params <- case !(lookupDefExact n (gamma defs)) of
|
||||
Just (TCon _ _ ps _ _ _ _ _) => pure ps
|
||||
_ => pure []
|
||||
let (ps, ds) = splitPs 0 params (map snd args)
|
||||
ns' <- getDepsArgs True !(traverse (evalClosure defs) ps) ns
|
||||
getDepsArgs False !(traverse (evalClosure defs) ds) ns'
|
||||
where
|
||||
-- Split into arguments in parameter position, and others
|
||||
splitPs : Nat -> List Nat -> List (Closure []) ->
|
||||
(List (Closure []), List (Closure []))
|
||||
splitPs n params [] = ([], [])
|
||||
splitPs n params (x :: xs)
|
||||
= let (ps', ds') = splitPs (1 + n) params xs in
|
||||
if n `elem` params
|
||||
then (x :: ps', ds')
|
||||
else (ps', x :: ds')
|
||||
getDeps inparam (NDelayed _ _ t) ns = getDeps inparam t ns
|
||||
getDeps inparams nf ns = pure ns
|
||||
|
||||
-- If the name of an argument is in the list of specialisable arguments,
|
||||
-- record the position. Also record the position of anything the argument
|
||||
-- depends on which is only dependend on by declared static arguments.
|
||||
collectSpec : List Nat -> -- specialisable so far
|
||||
List Name -> -- things depended on by dynamic args
|
||||
-- We're assuming it's a short list, so just use
|
||||
-- List and don't worry about duplicates.
|
||||
List (Name, Nat) -> NF [] -> Core (List Nat)
|
||||
collectSpec acc ddeps ps (NBind tfc x (Pi _ _ _ nty) sc)
|
||||
= do defs <- get Ctxt
|
||||
empty <- clearDefs defs
|
||||
sc' <- sc defs (toClosure defaultOpts [] (Ref tfc Bound x))
|
||||
if x `elem` ns
|
||||
then do deps <- getDeps True !(evalClosure defs nty) NameMap.empty
|
||||
-- Get names depended on by nty
|
||||
-- Keep the ones which are either:
|
||||
-- * parameters
|
||||
-- * not depended on by a dynamic argument (the ddeps)
|
||||
let rs = filter (\x => snd x ||
|
||||
not (fst x `elem` ddeps))
|
||||
(toList deps)
|
||||
let acc' = insertDeps acc ps (x :: map fst rs)
|
||||
collectSpec acc' ddeps ps sc'
|
||||
else collectSpec acc ddeps ps sc'
|
||||
collectSpec acc ddeps ps _ = pure acc
|
||||
|
||||
getNamePos : Nat -> NF [] -> Core (List (Name, Nat))
|
||||
getNamePos i (NBind tfc x (Pi _ _ _ _) sc)
|
||||
= do defs <- get Ctxt
|
||||
ns' <- getNamePos (1 + i) !(sc defs (toClosure defaultOpts [] (Erased tfc Placeholder)))
|
||||
pure ((x, i) :: ns')
|
||||
getNamePos _ _ = pure []
|
||||
@ -17,6 +17,7 @@ import Idris.Syntax
|
||||
import TTImp.Elab.Check
|
||||
import TTImp.Elab.Utils
|
||||
import TTImp.Elab
|
||||
import TTImp.ProcessFnOpt
|
||||
import TTImp.TTImp
|
||||
|
||||
import Data.List
|
||||
@ -27,174 +28,6 @@ import Libraries.Data.StringMap
|
||||
|
||||
%default covering
|
||||
|
||||
getRetTy : Defs -> NF [] -> Core Name
|
||||
getRetTy defs (NBind fc _ (Pi _ _ _ _) sc)
|
||||
= getRetTy defs !(sc defs (toClosure defaultOpts [] (Erased fc Placeholder)))
|
||||
getRetTy defs (NTCon _ n _ _ _) = pure n
|
||||
getRetTy defs ty
|
||||
= throw (GenericMsg (getLoc ty)
|
||||
"Can only add hints for concrete return types")
|
||||
|
||||
throwIfHasFlag : {auto c : Ref Ctxt Defs} -> FC -> Name -> DefFlag -> String -> Core ()
|
||||
throwIfHasFlag fc ndef fl msg
|
||||
= when !(hasFlag fc ndef fl) $ throw (GenericMsg fc msg)
|
||||
|
||||
processFnOpt : {auto c : Ref Ctxt Defs} ->
|
||||
FC -> Bool -> -- ^ top level name?
|
||||
Name -> FnOpt -> Core ()
|
||||
processFnOpt fc _ ndef Unsafe
|
||||
= do setIsEscapeHatch fc ndef
|
||||
processFnOpt fc _ ndef Inline
|
||||
= do throwIfHasFlag fc ndef NoInline "%noinline and %inline are mutually exclusive"
|
||||
setFlag fc ndef Inline
|
||||
processFnOpt fc _ ndef NoInline
|
||||
= do throwIfHasFlag fc ndef Inline "%inline and %noinline are mutually exclusive"
|
||||
setFlag fc ndef NoInline
|
||||
processFnOpt fc _ ndef Deprecate
|
||||
= setFlag fc ndef Deprecate
|
||||
processFnOpt fc _ ndef TCInline
|
||||
= setFlag fc ndef TCInline
|
||||
processFnOpt fc True ndef (Hint d)
|
||||
= do defs <- get Ctxt
|
||||
Just ty <- lookupTyExact ndef (gamma defs)
|
||||
| Nothing => undefinedName fc ndef
|
||||
target <- getRetTy defs !(nf defs [] ty)
|
||||
addHintFor fc target ndef d False
|
||||
processFnOpt fc _ ndef (Hint d)
|
||||
= do logC "elab" 5 $ do pure $ "Adding local hint " ++ show !(toFullNames ndef)
|
||||
addLocalHint ndef
|
||||
processFnOpt fc True ndef (GlobalHint a)
|
||||
= addGlobalHint ndef a
|
||||
processFnOpt fc _ ndef (GlobalHint a)
|
||||
= throw (GenericMsg fc "%globalhint is not valid in local definitions")
|
||||
processFnOpt fc _ ndef ExternFn
|
||||
= setFlag fc ndef Inline -- if externally defined, inline when compiling
|
||||
processFnOpt fc _ ndef (ForeignFn _)
|
||||
= setFlag fc ndef Inline -- if externally defined, inline when compiling
|
||||
processFnOpt fc _ ndef (ForeignExport _)
|
||||
= pure ()
|
||||
processFnOpt fc _ ndef Invertible
|
||||
= setFlag fc ndef Invertible
|
||||
processFnOpt fc _ ndef (Totality tot)
|
||||
= setFlag fc ndef (SetTotal tot)
|
||||
processFnOpt fc _ ndef Macro
|
||||
= setFlag fc ndef Macro
|
||||
processFnOpt fc _ ndef (SpecArgs ns)
|
||||
= do defs <- get Ctxt
|
||||
Just gdef <- lookupCtxtExact ndef (gamma defs)
|
||||
| Nothing => undefinedName fc ndef
|
||||
nty <- nf defs [] (type gdef)
|
||||
ps <- getNamePos 0 nty
|
||||
ddeps <- collectDDeps nty
|
||||
specs <- collectSpec [] ddeps ps nty
|
||||
ignore $ addDef ndef ({ specArgs := specs } gdef)
|
||||
where
|
||||
insertDeps : List Nat -> List (Name, Nat) -> List Name -> List Nat
|
||||
insertDeps acc ps [] = acc
|
||||
insertDeps acc ps (n :: ns)
|
||||
= case lookup n ps of
|
||||
Nothing => insertDeps acc ps ns
|
||||
Just pos => if pos `elem` acc
|
||||
then insertDeps acc ps ns
|
||||
else insertDeps (pos :: acc) ps ns
|
||||
|
||||
-- Collect the argument names which the dynamic args depend on
|
||||
collectDDeps : NF [] -> Core (List Name)
|
||||
collectDDeps (NBind tfc x (Pi _ _ _ nty) sc)
|
||||
= do defs <- get Ctxt
|
||||
empty <- clearDefs defs
|
||||
sc' <- sc defs (toClosure defaultOpts [] (Ref tfc Bound x))
|
||||
if x `elem` ns
|
||||
then collectDDeps sc'
|
||||
else do aty <- quote empty [] nty
|
||||
-- Get names depended on by nty
|
||||
let deps = keys (getRefs (UN Underscore) aty)
|
||||
rest <- collectDDeps sc'
|
||||
pure (rest ++ deps)
|
||||
collectDDeps _ = pure []
|
||||
|
||||
-- Return names the type depends on, and whether it's a parameter
|
||||
mutual
|
||||
getDepsArgs : Bool -> List (NF []) -> NameMap Bool ->
|
||||
Core (NameMap Bool)
|
||||
getDepsArgs inparam [] ns = pure ns
|
||||
getDepsArgs inparam (a :: as) ns
|
||||
= do ns' <- getDeps inparam a ns
|
||||
getDepsArgs inparam as ns'
|
||||
|
||||
getDeps : Bool -> NF [] -> NameMap Bool ->
|
||||
Core (NameMap Bool)
|
||||
getDeps inparam (NBind _ x (Pi _ _ _ pty) sc) ns
|
||||
= do defs <- get Ctxt
|
||||
ns' <- getDeps inparam !(evalClosure defs pty) ns
|
||||
sc' <- sc defs (toClosure defaultOpts [] (Erased fc Placeholder))
|
||||
getDeps inparam sc' ns'
|
||||
getDeps inparam (NBind _ x b sc) ns
|
||||
= do defs <- get Ctxt
|
||||
ns' <- getDeps False !(evalClosure defs (binderType b)) ns
|
||||
sc' <- sc defs (toClosure defaultOpts [] (Erased fc Placeholder))
|
||||
getDeps False sc' ns
|
||||
getDeps inparam (NApp _ (NRef Bound n) args) ns
|
||||
= do defs <- get Ctxt
|
||||
ns' <- getDepsArgs False !(traverse (evalClosure defs . snd) args) ns
|
||||
pure (insert n inparam ns')
|
||||
getDeps inparam (NDCon _ n t a args) ns
|
||||
= do defs <- get Ctxt
|
||||
getDepsArgs False !(traverse (evalClosure defs . snd) args) ns
|
||||
getDeps inparam (NTCon _ n t a args) ns
|
||||
= do defs <- get Ctxt
|
||||
params <- case !(lookupDefExact n (gamma defs)) of
|
||||
Just (TCon _ _ ps _ _ _ _ _) => pure ps
|
||||
_ => pure []
|
||||
let (ps, ds) = splitPs 0 params (map snd args)
|
||||
ns' <- getDepsArgs True !(traverse (evalClosure defs) ps) ns
|
||||
getDepsArgs False !(traverse (evalClosure defs) ds) ns'
|
||||
where
|
||||
-- Split into arguments in parameter position, and others
|
||||
splitPs : Nat -> List Nat -> List (Closure []) ->
|
||||
(List (Closure []), List (Closure []))
|
||||
splitPs n params [] = ([], [])
|
||||
splitPs n params (x :: xs)
|
||||
= let (ps', ds') = splitPs (1 + n) params xs in
|
||||
if n `elem` params
|
||||
then (x :: ps', ds')
|
||||
else (ps', x :: ds')
|
||||
getDeps inparam (NDelayed _ _ t) ns = getDeps inparam t ns
|
||||
getDeps inparams nf ns = pure ns
|
||||
|
||||
-- If the name of an argument is in the list of specialisable arguments,
|
||||
-- record the position. Also record the position of anything the argument
|
||||
-- depends on which is only dependend on by declared static arguments.
|
||||
collectSpec : List Nat -> -- specialisable so far
|
||||
List Name -> -- things depended on by dynamic args
|
||||
-- We're assuming it's a short list, so just use
|
||||
-- List and don't worry about duplicates.
|
||||
List (Name, Nat) -> NF [] -> Core (List Nat)
|
||||
collectSpec acc ddeps ps (NBind tfc x (Pi _ _ _ nty) sc)
|
||||
= do defs <- get Ctxt
|
||||
empty <- clearDefs defs
|
||||
sc' <- sc defs (toClosure defaultOpts [] (Ref tfc Bound x))
|
||||
if x `elem` ns
|
||||
then do deps <- getDeps True !(evalClosure defs nty) NameMap.empty
|
||||
-- Get names depended on by nty
|
||||
-- Keep the ones which are either:
|
||||
-- * parameters
|
||||
-- * not depended on by a dynamic argument (the ddeps)
|
||||
let rs = filter (\x => snd x ||
|
||||
not (fst x `elem` ddeps))
|
||||
(toList deps)
|
||||
let acc' = insertDeps acc ps (x :: map fst rs)
|
||||
collectSpec acc' ddeps ps sc'
|
||||
else collectSpec acc ddeps ps sc'
|
||||
collectSpec acc ddeps ps _ = pure acc
|
||||
|
||||
getNamePos : Nat -> NF [] -> Core (List (Name, Nat))
|
||||
getNamePos i (NBind tfc x (Pi _ _ _ _) sc)
|
||||
= do defs <- get Ctxt
|
||||
ns' <- getNamePos (1 + i) !(sc defs (toClosure defaultOpts [] (Erased tfc Placeholder)))
|
||||
pure ((x, i) :: ns')
|
||||
getNamePos _ _ = pure []
|
||||
|
||||
getFnString : {auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
|
||||
@ -118,12 +118,13 @@ mutual
|
||||
val' <- reify defs !(evalClosure defs val)
|
||||
sc' <- reify defs !(evalClosure defs sc)
|
||||
pure (ILet fc' lhsFC' c' n' ty' val' sc')
|
||||
(UN (Basic "ICase"), [fc, sc, ty, cs])
|
||||
(UN (Basic "ICase"), [fc, opts, sc, ty, cs])
|
||||
=> do fc' <- reify defs !(evalClosure defs fc)
|
||||
opts' <- reify defs !(evalClosure defs opts)
|
||||
sc' <- reify defs !(evalClosure defs sc)
|
||||
ty' <- reify defs !(evalClosure defs ty)
|
||||
cs' <- reify defs !(evalClosure defs cs)
|
||||
pure (ICase fc' sc' ty' cs')
|
||||
pure (ICase fc' opts' sc' ty' cs')
|
||||
(UN (Basic "ILocal"), [fc, ds, sc])
|
||||
=> do fc' <- reify defs !(evalClosure defs fc)
|
||||
ds' <- reify defs !(evalClosure defs ds)
|
||||
@ -501,12 +502,13 @@ mutual
|
||||
aval' <- reflect fc defs lhs env aval
|
||||
sc' <- reflect fc defs lhs env sc
|
||||
appCon fc defs (reflectionttimp "ILet") [fc', lhsFC', c', n', aty', aval', sc']
|
||||
reflect fc defs lhs env (ICase tfc sc ty cs)
|
||||
reflect fc defs lhs env (ICase tfc opts sc ty cs)
|
||||
= do fc' <- reflect fc defs lhs env tfc
|
||||
opts' <- reflect fc defs lhs env opts
|
||||
sc' <- reflect fc defs lhs env sc
|
||||
ty' <- reflect fc defs lhs env ty
|
||||
cs' <- reflect fc defs lhs env cs
|
||||
appCon fc defs (reflectionttimp "ICase") [fc', sc', ty', cs']
|
||||
appCon fc defs (reflectionttimp "ICase") [fc', opts', sc', ty', cs']
|
||||
reflect fc defs lhs env (ILocal tfc ds sc)
|
||||
= do fc' <- reflect fc defs lhs env tfc
|
||||
ds' <- reflect fc defs lhs env ds
|
||||
|
||||
@ -68,7 +68,7 @@ mutual
|
||||
ILet : FC -> (lhsFC : FC) -> RigCount -> Name ->
|
||||
(nTy : RawImp' nm) -> (nVal : RawImp' nm) ->
|
||||
(scope : RawImp' nm) -> RawImp' nm
|
||||
ICase : FC -> RawImp' nm -> (ty : RawImp' nm) ->
|
||||
ICase : FC -> List (FnOpt' nm) -> RawImp' nm -> (ty : RawImp' nm) ->
|
||||
List (ImpClause' nm) -> RawImp' nm
|
||||
ILocal : FC -> List (ImpDecl' nm) -> RawImp' nm -> RawImp' nm
|
||||
-- Local definitions made elsewhere, but that we're pushing
|
||||
@ -163,7 +163,7 @@ mutual
|
||||
show (ILet fc lhsFC c n ty val sc)
|
||||
= "(%let " ++ show c ++ " " ++ " " ++ show n ++ " " ++ show ty ++
|
||||
" " ++ show val ++ " " ++ show sc ++ ")"
|
||||
show (ICase _ scr scrty alts)
|
||||
show (ICase _ _ scr scrty alts)
|
||||
= "(%case (" ++ show scr ++ " : " ++ show scrty ++ ") " ++ show alts ++ ")"
|
||||
show (ILocal _ def scope)
|
||||
= "(%local (" ++ show def ++ ") " ++ show scope ++ ")"
|
||||
@ -844,7 +844,7 @@ getFC (IVar x _) = x
|
||||
getFC (IPi x _ _ _ _ _) = x
|
||||
getFC (ILam x _ _ _ _ _) = x
|
||||
getFC (ILet x _ _ _ _ _ _) = x
|
||||
getFC (ICase x _ _ _) = x
|
||||
getFC (ICase x _ _ _ _) = x
|
||||
getFC (ILocal x _ _) = x
|
||||
getFC (ICaseLocal x _ _ _ _) = x
|
||||
getFC (IUpdate x _ _) = x
|
||||
|
||||
@ -16,8 +16,8 @@ mutual
|
||||
= ILam fc rig (map (map f) info) nm (map f a) (map f sc)
|
||||
map f (ILet fc lhsFC rig nm ty val sc)
|
||||
= ILet fc lhsFC rig nm (map f ty) (map f val) (map f sc)
|
||||
map f (ICase fc sc ty cls)
|
||||
= ICase fc (map f sc) (map f ty) (map (map f) cls)
|
||||
map f (ICase fc opts sc ty cls)
|
||||
= ICase fc (map (map f) opts) (map f sc) (map f ty) (map (map f) cls)
|
||||
map f (ILocal fc ds sc)
|
||||
= ILocal fc (map (map f) ds) (map f sc)
|
||||
map f (ICaseLocal fc userN intN args sc)
|
||||
|
||||
@ -23,8 +23,8 @@ mutual
|
||||
toBuf b (ILet fc lhsFC r n nTy nVal scope)
|
||||
= do tag 3; toBuf b fc; toBuf b lhsFC; toBuf b r; toBuf b n;
|
||||
toBuf b nTy; toBuf b nVal; toBuf b scope
|
||||
toBuf b (ICase fc y ty xs)
|
||||
= do tag 4; toBuf b fc; toBuf b y; toBuf b ty; toBuf b xs
|
||||
toBuf b (ICase fc opts y ty xs)
|
||||
= do tag 4; toBuf b fc; toBuf b opts; toBuf b y; toBuf b ty; toBuf b xs
|
||||
toBuf b (ILocal fc xs sc)
|
||||
= do tag 5; toBuf b fc; toBuf b xs; toBuf b sc
|
||||
toBuf b (ICaseLocal fc _ _ _ sc)
|
||||
@ -109,9 +109,9 @@ mutual
|
||||
nTy <- fromBuf b; nVal <- fromBuf b
|
||||
scope <- fromBuf b
|
||||
pure (ILet fc lhsFC r n nTy nVal scope)
|
||||
4 => do fc <- fromBuf b; y <- fromBuf b;
|
||||
4 => do fc <- fromBuf b; opts <- fromBuf b; y <- fromBuf b;
|
||||
ty <- fromBuf b; xs <- fromBuf b
|
||||
pure (ICase fc y ty xs)
|
||||
pure (ICase fc opts y ty xs)
|
||||
5 => do fc <- fromBuf b;
|
||||
xs <- fromBuf b; sc <- fromBuf b
|
||||
pure (ILocal fc xs sc)
|
||||
|
||||
@ -94,8 +94,8 @@ parameters (f : RawImp' nm -> RawImp' nm)
|
||||
= f $ ILam fc rig (mapPiInfo pinfo) x (mapTTImp argTy) (mapTTImp lamTy)
|
||||
mapTTImp (ILet fc lhsFC rig n nTy nVal scope)
|
||||
= f $ ILet fc lhsFC rig n (mapTTImp nTy) (mapTTImp nVal) (mapTTImp scope)
|
||||
mapTTImp (ICase fc t ty cls)
|
||||
= f $ ICase fc (mapTTImp t) (mapTTImp ty) (assert_total $ map mapImpClause cls)
|
||||
mapTTImp (ICase fc opts t ty cls)
|
||||
= f $ ICase fc opts (mapTTImp t) (mapTTImp ty) (assert_total $ map mapImpClause cls)
|
||||
mapTTImp (ILocal fc xs t)
|
||||
= f $ ILocal fc (assert_total $ map mapImpDecl xs) (mapTTImp t)
|
||||
mapTTImp (ICaseLocal fc unm inm args t) = f $ ICaseLocal fc unm inm args (mapTTImp t)
|
||||
|
||||
@ -165,7 +165,8 @@ mutual
|
||||
(tm, _) <- unelabTy Full nest env scrutinee
|
||||
Just pats' <- map sequence $ traverse (mkClause fc argpos args) pats
|
||||
| _ => pure Nothing
|
||||
pure $ Just $ ICase fc tm (Implicit fc False) pats'
|
||||
-- TODO: actually grab the fnopts?
|
||||
pure $ Just $ ICase fc [] tm (Implicit fc False) pats'
|
||||
|
||||
dropParams : {auto c : Ref Ctxt Defs} ->
|
||||
List (Name, Nat) -> (IRawImp, Glued vars) ->
|
||||
|
||||
@ -131,7 +131,7 @@ findBindableNamesQuot env used (ILam fc x y z argTy lamTy)
|
||||
= findBindableNamesQuot env used ![argTy, lamTy]
|
||||
findBindableNamesQuot env used (ILet fc lhsfc x y nTy nVal scope)
|
||||
= findBindableNamesQuot env used ![nTy, nVal, scope]
|
||||
findBindableNamesQuot env used (ICase fc x ty xs)
|
||||
findBindableNamesQuot env used (ICase fc _ x ty xs)
|
||||
= findBindableNamesQuot env used !([x, ty] ++ getRawImp !xs)
|
||||
where getRawImp : ImpClause -> List RawImp
|
||||
getRawImp (PatClause fc1 lhs rhs) = [lhs, rhs]
|
||||
@ -319,9 +319,10 @@ mutual
|
||||
ILet fc lhsFC r n (substNames' bvar bound ps nTy)
|
||||
(substNames' bvar bound ps nVal)
|
||||
(substNames' bvar bound' ps scope)
|
||||
substNames' bvar bound ps (ICase fc y ty xs)
|
||||
= ICase fc (substNames' bvar bound ps y) (substNames' bvar bound ps ty)
|
||||
(map (substNamesClause' bvar bound ps) xs)
|
||||
substNames' bvar bound ps (ICase fc opts y ty xs)
|
||||
= ICase fc opts
|
||||
(substNames' bvar bound ps y) (substNames' bvar bound ps ty)
|
||||
(map (substNamesClause' bvar bound ps) xs)
|
||||
substNames' bvar bound ps (ILocal fc xs y)
|
||||
= let bound' = definedInBlock emptyNS xs ++ bound in
|
||||
ILocal fc (map (substNamesDecl' bvar bound ps) xs)
|
||||
@ -426,8 +427,8 @@ mutual
|
||||
= ILet fc' fc' r n (substLoc fc' nTy)
|
||||
(substLoc fc' nVal)
|
||||
(substLoc fc' scope)
|
||||
substLoc fc' (ICase fc y ty xs)
|
||||
= ICase fc' (substLoc fc' y) (substLoc fc' ty)
|
||||
substLoc fc' (ICase fc opts y ty xs)
|
||||
= ICase fc' opts (substLoc fc' y) (substLoc fc' ty)
|
||||
(map (substLocClause fc') xs)
|
||||
substLoc fc' (ILocal fc xs y)
|
||||
= ILocal fc' (map (substLocDecl fc') xs)
|
||||
|
||||
@ -251,8 +251,8 @@ withRHS fc drop wname wargnames tm toplhs
|
||||
= pure $ ILam fc c p n !(wrhs ty) !(wrhs sc)
|
||||
wrhs (ILet fc lhsFC c n ty val sc)
|
||||
= pure $ ILet fc lhsFC c n !(wrhs ty) !(wrhs val) !(wrhs sc)
|
||||
wrhs (ICase fc sc ty clauses)
|
||||
= pure $ ICase fc !(wrhs sc) !(wrhs ty) !(traverse wrhsC clauses)
|
||||
wrhs (ICase fc opts sc ty clauses)
|
||||
= pure $ ICase fc opts !(wrhs sc) !(wrhs ty) !(traverse wrhsC clauses)
|
||||
wrhs (ILocal fc decls sc)
|
||||
= pure $ ILocal fc decls !(wrhs sc) -- TODO!
|
||||
wrhs (IUpdate fc upds tm)
|
||||
|
||||
@ -47,6 +47,7 @@ idrisTestsBasic = MkTestPool "Fundamental language features" [] Nothing
|
||||
"idiom001",
|
||||
"literals001",
|
||||
"dotted001",
|
||||
"case001",
|
||||
"rewrite001",
|
||||
"interpolation001", "interpolation002", "interpolation003",
|
||||
"interpolation004"]
|
||||
|
||||
27
tests/idris2/case001/InlineCase.idr
Normal file
27
tests/idris2/case001/InlineCase.idr
Normal file
@ -0,0 +1,27 @@
|
||||
module InlineCase
|
||||
|
||||
data BTree : Type where
|
||||
Leaf : BTree
|
||||
Node : BTree -> Nat -> BTree -> BTree
|
||||
|
||||
product : BTree -> Nat
|
||||
product Leaf = 1
|
||||
product (Node l n r)
|
||||
= %inline case n of
|
||||
Z => Z
|
||||
_ => %inline case product l of
|
||||
Z => Z
|
||||
pl => %inline case product r of
|
||||
Z => Z
|
||||
pr => pl * n * pr
|
||||
|
||||
myfun : Nat -> Nat
|
||||
myfun Z = Z
|
||||
myfun n = S $ case n of
|
||||
Z => Z
|
||||
S n => myfun n
|
||||
|
||||
main : IO ()
|
||||
main = do
|
||||
l <- getLine
|
||||
print (product $ Node Leaf (length l) Leaf)
|
||||
1
tests/idris2/case001/expected
Normal file
1
tests/idris2/case001/expected
Normal file
@ -0,0 +1 @@
|
||||
(define InlineCase-product (lambda (arg-0) (case (vector-ref arg-0 0) ((0) 1) (else (let ((e-0 (vector-ref arg-0 1))) (let ((e-1 (vector-ref arg-0 2))) (let ((e-2 (vector-ref arg-0 3))) (cond ((equal? e-1 0) 0)(else (let ((sc1 (InlineCase-product e-0))) (cond ((equal? sc1 0) 0)(else (let ((sc1 (InlineCase-product e-2))) (cond ((equal? sc1 0) 0)(else (* (* (InlineCase-product e-0) e-1) (InlineCase-product e-2)))))))))))))))))
|
||||
4
tests/idris2/case001/run
Executable file
4
tests/idris2/case001/run
Executable file
@ -0,0 +1,4 @@
|
||||
rm -rf build
|
||||
|
||||
$1 --no-color --console-width 0 --no-banner --codegen chez InlineCase.idr -o inline-case
|
||||
grep "define InlineCase-product" build/exec/inline-case_app/inline-case.ss
|
||||
@ -37,7 +37,7 @@ genEq typeName = do
|
||||
finalClause = PatClause pos `(_) `(False)
|
||||
clauses <- traverse makeClause constrs
|
||||
let allClauses = clauses ++ [finalClause]
|
||||
caseExpr = ICase pos `(MkPair x y) (Implicit pos True) allClauses
|
||||
caseExpr = ICase pos [] `(MkPair x y) (Implicit pos True) allClauses
|
||||
result = `(\x, y => ~(caseExpr))
|
||||
check result
|
||||
%logging 0
|
||||
|
||||
Loading…
Reference in New Issue
Block a user