idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-24 06:52:19 +03:00
Code Issues Projects Releases Wiki Activity

Implement new application syntax

Browse Source 
Add syntax for bind-all-explicits

Add new record update syntax

Remove PInstance
This commit is contained in:
russoul 2020-10-01 12:41:30 +03:00
parent af62955e07
commit b57b28a64e
53 changed files with 731 additions and 788 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
CHANGELOG.md
View File

@ -17,9 +17,15 @@ Command-line options changes:
Compiler changes:
* Added syntax for record instantiation:
* Added new syntax for named applications and bind-all-explicits:
`record < Constructor or _ > {<field1> = <expr1>, <field2> = <expr2>, ..., <fieldN> = <exprN>}`
`f {x [= t], x [= t], ...}`
`f {x [= t], x [= t], ..., _}`
`f {}`
* Added new syntax for record updates:
`{x := t, x $= t, ...}`
* Added primitives to the parsing library used in the compiler to get more precise
boundaries to the AST nodes `FC`.

5
libs/base/Language/Reflection/TTImp.idr
View File

@ -36,7 +36,8 @@ mutual
IUpdate : FC -> List IFieldUpdate -> TTImp -> TTImp
IApp : FC -> TTImp -> TTImp -> TTImp
IImplicitApp : FC -> TTImp -> Maybe Name -> TTImp -> TTImp
INamedApp : FC -> TTImp -> Name -> TTImp -> TTImp
IAutoApp : FC -> TTImp -> TTImp -> TTImp
IWithApp : FC -> TTImp -> TTImp -> TTImp
ISearch : FC -> (depth : Nat) -> TTImp
@ -100,7 +101,7 @@ mutual
ForeignFn : List TTImp -> FnOpt
-- assume safe to cancel arguments in unification
Invertible : FnOpt
Totalty : TotalReq -> FnOpt
Totality : TotalReq -> FnOpt
Macro : FnOpt
SpecArgs : List Name -> FnOpt

12
src/Core/Core.idr
View File

@ -93,10 +93,9 @@ data Error : Type where
RecordTypeNeeded : {vars : _} ->
FC -> Env Term vars -> Error
NotRecordField : FC -> String -> Maybe Name -> Error
NotCoveredField : FC -> String -> Error
NotRecordType : FC -> Name -> Error
IncompatibleFieldUpdate : FC -> List String -> Error
InvalidImplicits : {vars : _} ->
InvalidArgs : {vars : _} ->
FC -> Env Term vars -> List (Maybe Name) -> Term vars -> Error
TryWithImplicits : {vars : _} ->
FC -> Env Term vars -> List (Name, Term vars) -> Error
@ -239,14 +238,12 @@ Show Error where
= show fc ++ ":" ++ fld ++ " is not part of a record type"
show (NotRecordField fc fld (Just ty))
= show fc ++ ":Record type " ++ show ty ++ " has no field " ++ fld
show (NotCoveredField fc fieldname)
= show fc ++ ":Field not covered " ++ fieldname
show (NotRecordType fc ty)
= show fc ++ ":" ++ show ty ++ " is not a record type"
show (IncompatibleFieldUpdate fc flds)
= show fc ++ ":Field update " ++ showSep "->" flds ++ " not compatible with other updates"
show (InvalidImplicits fc env ns tm)
= show fc ++ ":" ++ show ns ++ " are not valid implicit arguments in " ++ show tm
show (InvalidArgs fc env ns tm)
= show fc ++ ":" ++ show ns ++ " are not valid arguments in " ++ show tm
show (TryWithImplicits fc env imps)
= show fc ++ ":Need to bind implicits "
++ showSep "," (map (\x => show (fst x) ++ " : " ++ show (snd x)) imps)
@ -349,10 +346,9 @@ getErrorLoc (AllFailed ((_, x) :: _)) = getErrorLoc x
getErrorLoc (AllFailed []) = Nothing
getErrorLoc (RecordTypeNeeded loc _) = Just loc
getErrorLoc (NotRecordField loc _ _) = Just loc
getErrorLoc (NotCoveredField loc _) = Just loc
getErrorLoc (NotRecordType loc _) = Just loc
getErrorLoc (IncompatibleFieldUpdate loc _) = Just loc
getErrorLoc (InvalidImplicits loc _ _ _) = Just loc
getErrorLoc (InvalidArgs loc _ _ _) = Just loc
getErrorLoc (TryWithImplicits loc _ _) = Just loc
getErrorLoc (BadUnboundImplicit loc _ _ _) = Just loc
getErrorLoc (CantSolveGoal loc _ _) = Just loc

14
src/Core/Normalise.idr
View File

@ -1299,20 +1299,20 @@ normaliseErr : {auto c : Ref Ctxt Defs} ->
Error -> Core Error
normaliseErr (CantConvert fc env l r)
= do defs <- get Ctxt
pure $ CantConvert fc env !(normaliseHoles defs env l)
!(normaliseHoles defs env r)
pure $ CantConvert fc env !(normaliseHoles defs env l >>= toFullNames)
!(normaliseHoles defs env r >>= toFullNames)
normaliseErr (CantSolveEq fc env l r)
= do defs <- get Ctxt
pure $ CantSolveEq fc env !(normaliseHoles defs env l)
!(normaliseHoles defs env r)
pure $ CantSolveEq fc env !(normaliseHoles defs env l >>= toFullNames)
!(normaliseHoles defs env r >>= toFullNames)
normaliseErr (WhenUnifying fc env l r err)
= do defs <- get Ctxt
pure $ WhenUnifying fc env !(normaliseHoles defs env l)
!(normaliseHoles defs env r)
pure $ WhenUnifying fc env !(normaliseHoles defs env l >>= toFullNames)
!(normaliseHoles defs env r >>= toFullNames)
!(normaliseErr err)
normaliseErr (CantSolveGoal fc env g)
= do defs <- get Ctxt
pure $ CantSolveGoal fc env !(normaliseHoles defs env g)
pure $ CantSolveGoal fc env !(normaliseHoles defs env g >>= toFullNames)
normaliseErr (AllFailed errs)
= pure $ AllFailed !(traverse (\x => pure (fst x, !(normaliseErr (snd x)))) errs)
normaliseErr (InType fc n err)

11
src/Idris/Desugar.idr
View File

@ -187,14 +187,14 @@ mutual
desugarB side ps (PUpdate fc fs)
= desugarB side ps (PLam fc top Explicit (PRef fc (MN "rec" 0)) (PImplicit fc)
(PApp fc (PUpdate fc fs) (PRef fc (MN "rec" 0))))
desugarB side ps (PInstance fc n fs)
= pure $ IInstance fc n !(traverse (desugarUpdate side ps) fs)
desugarB side ps (PApp fc x y)
= pure $ IApp fc !(desugarB side ps x) !(desugarB side ps y)
desugarB side ps (PAutoApp fc x y)
= pure $ IAutoApp fc !(desugarB side ps x) !(desugarB side ps y)
desugarB side ps (PWithApp fc x y)
= pure $ IWithApp fc !(desugarB side ps x) !(desugarB side ps y)
desugarB side ps (PImplicitApp fc x argn y)
= pure $ IImplicitApp fc !(desugarB side ps x) argn !(desugarB side ps y)
desugarB side ps (PNamedApp fc x argn y)
= pure $ INamedApp fc !(desugarB side ps x) argn !(desugarB side ps y)
desugarB side ps (PDelayed fc r ty)
= pure $ IDelayed fc r !(desugarB side ps ty)
desugarB side ps (PDelay fc tm)
@ -669,7 +669,8 @@ mutual
getFn : RawImp -> Core Name
getFn (IVar _ n) = pure n
getFn (IApp _ f _) = getFn f
getFn (IImplicitApp _ f _ _) = getFn f
getFn (IAutoApp _ f _) = getFn f
getFn (INamedApp _ f _ _) = getFn f
getFn tm = throw (InternalError (show tm ++ " is not a function application"))
toIDef : ImpClause -> Core ImpDecl

27
src/Idris/Elab/Implementation.idr
View File

@ -74,8 +74,8 @@ addDefaults fc impName allms defs body
-- other methods.
-- (See test idris2/interface014 for an example!)
let mupdates
= map (\n => (n, IImplicitApp fc (IVar fc n)
(Just (UN "__con"))
= map (\n => (n, INamedApp fc (IVar fc n)
(UN "__con")
(IVar fc impName))) allms
cs' = map (substNamesClause [] mupdates) cs in
extendBody ms ns
@ -266,11 +266,11 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
impsApply : RawImp -> List (Name, RawImp) -> RawImp
impsApply fn [] = fn
impsApply fn ((n, arg) :: ns)
= impsApply (IImplicitApp fc fn (Just n) arg) ns
= impsApply (INamedApp fc fn n arg) ns
autoImpsApply : RawImp -> List RawImp -> RawImp
autoImpsApply f [] = f
autoImpsApply f (x :: xs) = autoImpsApply (IImplicitApp (getFC f) f Nothing x) xs
autoImpsApply f (x :: xs) = autoImpsApply (IAutoApp (getFC f) f x) xs
mkLam : List (Name, RigCount, PiInfo RawImp) -> RawImp -> RawImp
mkLam [] tm = tm
@ -282,11 +282,11 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
applyTo fc tm ((x, c, Explicit) :: xs)
= applyTo fc (IApp fc tm (IVar fc x)) xs
applyTo fc tm ((x, c, AutoImplicit) :: xs)
= applyTo fc (IImplicitApp fc tm (Just x) (IVar fc x)) xs
= applyTo fc (INamedApp fc tm x (IVar fc x)) xs
applyTo fc tm ((x, c, Implicit) :: xs)
= applyTo fc (IImplicitApp fc tm (Just x) (IVar fc x)) xs
= applyTo fc (INamedApp fc tm x (IVar fc x)) xs
applyTo fc tm ((x, c, DefImplicit _) :: xs)
= applyTo fc (IImplicitApp fc tm (Just x) (IVar fc x)) xs
= applyTo fc (INamedApp fc tm x (IVar fc x)) xs
-- When applying the method in the field for the record, eta expand
-- the expected arguments based on the field type, so that implicits get
@ -425,9 +425,12 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
updateApp ns (IApp fc f arg)
= do f' <- updateApp ns f
pure (IApp fc f' arg)
updateApp ns (IImplicitApp fc f x arg)
updateApp ns (IAutoApp fc f arg)
= do f' <- updateApp ns f
pure (IImplicitApp fc f' x arg)
pure (IAutoApp fc f' arg)
updateApp ns (INamedApp fc f x arg)
= do f' <- updateApp ns f
pure (INamedApp fc f' x arg)
updateApp ns tm
= throw (GenericMsg (getFC tm) "Invalid method definition")
@ -460,9 +463,9 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
= do log "elab.implementation" 3 $
"Adding transform for " ++ show top ++ " : " ++ show ty ++
"\n\tfor " ++ show iname ++ " in " ++ show ns
let lhs = IImplicitApp fc (IVar fc top)
(Just (UN "__con"))
(IVar fc iname)
let lhs = INamedApp fc (IVar fc top)
(UN "__con")
(IVar fc iname)
let Just mname = lookup (dropNS top) ns
| Nothing => pure ()
let rhs = IVar fc mname

18
src/Idris/Elab/Interface.idr
View File

@ -139,8 +139,8 @@ getMethToplevel {vars} env vis iname cname constraints allmeths params
(map (IBindVar fc) (map bindName allmeths))
let argns = getExplicitArgs 0 ty
-- eta expand the RHS so that we put implicits in the right place
let fnclause = PatClause fc (IImplicitApp fc (IVar fc cn)
(Just (UN "__con"))
let fnclause = PatClause fc (INamedApp fc (IVar fc cn)
(UN "__con")
conapp)
(mkLam argns
(apply (IVar fc (methName n))
@ -156,8 +156,8 @@ getMethToplevel {vars} env vis iname cname constraints allmeths params
= IPi (getFC pty) erased Implicit (Just n) pty (bindPs ps ty)
applyCon : Name -> (Name, RawImp)
applyCon n = (n, IImplicitApp fc (IVar fc n)
(Just (UN "__con")) (IVar fc (UN "__con")))
applyCon n = (n, INamedApp fc (IVar fc n)
(UN "__con") (IVar fc (UN "__con")))
getExplicitArgs : Int -> RawImp -> List Name
getExplicitArgs i (IPi _ _ Explicit n _ sc)
@ -214,7 +214,7 @@ getConstraintHint {vars} fc env vis iname cname constraints meths params (cn, co
impsBind : RawImp -> List String -> RawImp
impsBind fn [] = fn
impsBind fn (n :: ns)
= impsBind (IImplicitApp fc fn Nothing (IBindVar fc n)) ns
= impsBind (IAutoApp fc fn (IBindVar fc n)) ns
getSig : ImpDecl -> Maybe (FC, RigCount, List FnOpt, Name, (Bool, RawImp))
@ -399,7 +399,7 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
applyParams : RawImp -> List Name -> RawImp
applyParams tm [] = tm
applyParams tm (UN n :: ns)
= applyParams (IImplicitApp fc tm (Just (UN n)) (IBindVar fc n)) ns
= applyParams (INamedApp fc tm (UN n) (IBindVar fc n)) ns
applyParams tm (_ :: ns) = applyParams tm ns
changeNameTerm : Name -> RawImp -> RawImp
@ -407,8 +407,10 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
= if n == n' then IVar fc dn else IVar fc n'
changeNameTerm dn (IApp fc f arg)
= IApp fc (changeNameTerm dn f) arg
changeNameTerm dn (IImplicitApp fc f x arg)
= IImplicitApp fc (changeNameTerm dn f) x arg
changeNameTerm dn (IAutoApp fc f arg)
= IAutoApp fc (changeNameTerm dn f) arg
changeNameTerm dn (INamedApp fc f x arg)
= INamedApp fc (changeNameTerm dn f) x arg
changeNameTerm dn tm = tm
changeName : Name -> ImpClause -> ImpClause

10
src/Idris/Error.idr
View File

@ -302,19 +302,17 @@ perror (NotRecordField fc fld Nothing)
perror (NotRecordField fc fld (Just ty))
= pure $ errorDesc (reflow "Record type" <++> code (pretty !(getFullName ty)) <++> reflow "has no field"
<++> code (pretty fld) <+> dot) <+> line <+> !(ploc fc)
perror (NotCoveredField fc fld)
= pure $ errorDesc (reflow "Field not covered" <++> code (pretty fld) <+> dot) <+> line <+> !(ploc fc)
perror (NotRecordType fc ty)
= pure $ errorDesc (code (pretty !(getFullName ty)) <++> reflow "is not a record type.") <+> line <+> !(ploc fc)
perror (IncompatibleFieldUpdate fc flds)
= pure $ reflow "Field update" <++> concatWith (surround (pretty "->")) (pretty <$> flds)
<++> reflow "not compatible with other updates at" <+> colon <+> line <+> !(ploc fc)
perror (InvalidImplicits fc env [Just n] tm)
= pure $ errorDesc (code (pretty n) <++> reflow "is not a valid implicit argument in" <++> !(pshow env tm)
perror (InvalidArgs fc env [Just n] tm)
= pure $ errorDesc (code (pretty n) <++> reflow "is not a valid argument in" <++> !(pshow env tm)
<+> dot) <+> line <+> !(ploc fc)
perror (InvalidImplicits fc env ns tm)
perror (InvalidArgs fc env ns tm)
= pure $ errorDesc (concatWith (surround (comma <+> space)) (code . pretty <$> ns)
<++> reflow "are not valid implicit arguments in" <++> !(pshow env tm) <+> dot)
<++> reflow "are not valid arguments in" <++> !(pshow env tm) <+> dot)
<+> line <+> !(ploc fc)
perror (TryWithImplicits fc env imps)
= pure $ errorDesc (reflow "Need to bind implicits"

120
src/Idris/Parser.idr
View File

@ -100,13 +100,15 @@ iOperator
= operator <|> (symbol "`" *> name <* symbol "`")
data ArgType
= ExpArg PTerm
| ImpArg (Maybe Name) PTerm
= UnnamedExpArg PTerm
| UnnamedAutoArg PTerm
| NamedArg Name PTerm
| WithArg PTerm
argTerm : ArgType -> PTerm
argTerm (ExpArg t) = t
argTerm (ImpArg _ t) = t
argTerm (UnnamedExpArg t) = t
argTerm (UnnamedAutoArg t) = t
argTerm (NamedArg _ t) = t
argTerm (WithArg t) = t
mutual
@ -120,7 +122,7 @@ mutual
<|> with_ fname indents
<|> do b <- bounds (MkPair <$> simpleExpr fname indents <*> many (argExpr q fname indents))
(f, args) <- pure b.val
pure (applyExpImp (start b) (end b) f args)
pure (applyExpImp (start b) (end b) f (concat args))
<|> do b <- bounds (MkPair <$> iOperator <*> expr pdef fname indents)
(op, arg) <- pure b.val
pure (PPrefixOp (boundToFC fname b) op arg)
@ -130,42 +132,55 @@ mutual
List ArgType ->
PTerm
applyExpImp start end f [] = f
applyExpImp start end f (ExpArg exp :: args)
applyExpImp start end f (UnnamedExpArg exp :: args)
= applyExpImp start end (PApp (MkFC fname start end) f exp) args
applyExpImp start end f (ImpArg n imp :: args)
= applyExpImp start end (PImplicitApp (MkFC fname start end) f n imp) args
applyExpImp start end f (UnnamedAutoArg imp :: args)
= applyExpImp start end (PAutoApp (MkFC fname start end) f imp) args
applyExpImp start end f (NamedArg n imp :: args)
= applyExpImp start end (PNamedApp (MkFC fname start end) f n imp) args
applyExpImp start end f (WithArg exp :: args)
= applyExpImp start end (PWithApp (MkFC fname start end) f exp) args
argExpr : ParseOpts -> FileName -> IndentInfo -> Rule ArgType
argExpr : ParseOpts -> FileName -> IndentInfo -> Rule (List ArgType)
argExpr q fname indents
= do continue indents
arg <- simpleExpr fname indents
the (SourceEmptyRule _) $ case arg of
PHole loc _ n => pure (ExpArg (PHole loc True n))
t => pure (ExpArg t)
PHole loc _ n => pure [UnnamedExpArg (PHole loc True n)]
t => pure [UnnamedExpArg t]
<|> do continue indents
arg <- implicitArg fname indents
pure (ImpArg (fst arg) (snd arg))
braceArgs fname indents
<|> if withOK q
then do continue indents
symbol "|"
arg <- expr (record {withOK = False} q) fname indents
pure (WithArg arg)
pure [WithArg arg]
else fail "| not allowed here"
implicitArg : FileName -> IndentInfo -> Rule (Maybe Name, PTerm)
implicitArg fname indents
= do x <- bounds (symbol "{" *> unqualifiedName)
(do tm <- symbol "=" *> commit *> expr pdef fname indents <* symbol "}"
pure (Just (UN x.val), tm))
<|> (do b <- bounds (symbol "}")
pure (Just (UN x.val), PRef (boundToFC fname (mergeBounds x b)) (UN x.val)))
<|> do symbol "@{"
commit
tm <- expr pdef fname indents
symbol "}"
pure (Nothing, tm)
where
braceArgs : FileName -> IndentInfo -> Rule (List ArgType)
braceArgs fname indents
= do start <- bounds (symbol "{")
list <- sepBy (symbol ",")
$ do x <- bounds unqualifiedName
option (NamedArg (UN x.val) $ PRef (boundToFC fname x) (UN x.val))
$ do tm <- symbol "=" *> expr pdef fname indents
pure (NamedArg (UN x.val) tm)
matchAny <- option [] (if isCons list then
do symbol ","
x <- bounds (symbol "_")
pure [NamedArg (UN "_") (PImplicit (boundToFC fname x))]
else fail "non-empty list required")
end <- bounds (symbol "}")
matchAny <- pure $ if list.isNil
then [NamedArg (UN "_") (PImplicit (boundToFC fname (mergeBounds start end)))]
else matchAny
pure $ matchAny ++ list
<|> do symbol "@{"
commit
tm <- expr pdef fname indents
symbol "}"
pure [UnnamedAutoArg tm]
with_ : FileName -> IndentInfo -> Rule PTerm
with_ fname indents
@ -371,7 +386,6 @@ mutual
<|> binder fname indents
<|> rewrite_ fname indents
<|> record_ fname indents
<|> recordInstance fname indents
<|> do b <- bounds (symbol ".(" *> commit *> expr pdef fname indents <* symbol ")")
pure (PDotted (boundToFC fname b) b.val)
<|> do b <- bounds (symbol "`(" *> expr pdef fname indents <* symbol ")")
@ -614,18 +628,18 @@ mutual
record_ : FileName -> IndentInfo -> Rule PTerm
record_ fname indents
= do b <- bounds (do keyword "record"
= do b <- bounds (do kw <- option False (keyword "record" *> pure True) -- TODO deprecated
symbol "{"
commit
fs <- sepBy1 (symbol ",") (field fname indents True)
fs <- sepBy1 (symbol ",") (field kw fname indents True)
symbol "}"
pure fs)
pure (PUpdate (boundToFC fname b) b.val)
field : FileName -> IndentInfo -> Bool -> Rule PFieldUpdate
field fname indents allowNS
field : Bool -> FileName -> IndentInfo -> Bool -> Rule PFieldUpdate
field kw fname indents allowNS
= do path <- parseFieldName allowNS
upd <- (symbol "=" *> pure PSetField)
upd <- (ifThenElse kw (symbol "=") (symbol ":=") *> pure PSetField)
<|>
(symbol "$=" *> pure PSetFieldApp)
val <- opExpr plhs fname indents
@ -644,18 +658,6 @@ mutual
parseFieldName True = map fieldName <$> [| name :: many recFieldCompat |]
parseFieldName False = map fieldName <$> [| name :: pure [] |]
recordInstance : FileName -> IndentInfo -> Rule PTerm
recordInstance fname indents
= do b <- bounds (do keyword "record"
mbname <- (Just <$> name) <|> (const Nothing <$> symbol "_")
symbol "{"
commit
fs <- sepBy (symbol ",") (field fname indents False)
symbol "}"
pure (mbname, fs))
(mbname, fs) <- pure b.val
pure (PInstance (boundToFC fname b) mbname fs)
rewrite_ : FileName -> IndentInfo -> Rule PTerm
rewrite_ fname indents
= do b <- bounds (do keyword "rewrite"
@ -846,21 +848,14 @@ mkTyConType fc [] = PType fc
mkTyConType fc (x :: xs)
= PPi fc linear Explicit Nothing (PType fc) (mkTyConType fc xs)
mkDataConType : FC -> PTerm -> List ArgType -> PTerm
mkDataConType fc ret [] = ret
mkDataConType fc ret (ExpArg x :: xs)
= PPi fc linear Explicit Nothing x (mkDataConType fc ret xs)
mkDataConType fc ret (ImpArg n (PRef fc' x) :: xs)
= if n == Just x
then PPi fc linear Implicit n (PType fc')
(mkDataConType fc ret xs)
else PPi fc linear Implicit n (PRef fc' x)
(mkDataConType fc ret xs)
mkDataConType fc ret (ImpArg n x :: xs)
= PPi fc linear Implicit n x (mkDataConType fc ret xs)
mkDataConType fc ret (WithArg a :: xs)
= PImplicit fc -- This can't happen because we parse constructors without
-- withOK set
mkDataConType : FC -> PTerm -> List ArgType -> Maybe PTerm
mkDataConType fc ret [] = Just ret
mkDataConType fc ret (UnnamedExpArg x :: xs)
= PPi fc linear Explicit Nothing x <$> mkDataConType fc ret xs
mkDataConType fc ret (UnnamedAutoArg x :: xs)
= PPi fc linear AutoImplicit Nothing x <$> mkDataConType fc ret xs
mkDataConType _ _ _ -- with and named applications not allowed in simple ADTs
= Nothing
simpleCon : FileName -> PTerm -> IndentInfo -> Rule PTypeDecl
simpleCon fname ret indents
@ -870,8 +865,9 @@ simpleCon fname ret indents
pure (cdoc, cname, params))
atEnd indents
(cdoc, cname, params) <- pure b.val
pure (let cfc = boundToFC fname b in
MkPTy cfc cname cdoc (mkDataConType cfc ret params))
let cfc = boundToFC fname b
fromMaybe (fatalError "Named arguments not allowed in ADT constructors")
(pure . MkPTy cfc cname cdoc <$> mkDataConType cfc ret (concat params))
simpleData : FileName -> WithBounds t -> Name -> IndentInfo -> Rule PDataDecl
simpleData fname start n indents

8
src/Idris/Pretty.idr
View File

@ -214,22 +214,20 @@ mutual
let_ <++> braces (angles (angles "definitions")) <+> line <+> in_ <++> go startPrec sc
go d (PUpdate _ fs) =
parenthesise (d > appPrec) $ group $ record_ <++> braces (vsep $ punctuate comma (prettyUpdate <$> fs))
go d (PInstance _ n fs) =
parenthesise (d > appPrec) $ group $ record_ <++> pretty n <++> braces (vsep $ punctuate comma (prettyUpdate <$> fs))
go d (PApp _ f a) = parenthesise (d > appPrec) $ group $ go leftAppPrec f <++> go appPrec a
go d (PWithApp _ f a) = go d f <++> pipe <++> go d a
go d (PDelayed _ LInf ty) = parenthesise (d > appPrec) $ "Inf" <++> go appPrec ty
go d (PDelayed _ _ ty) = parenthesise (d > appPrec) $ "Lazy" <++> go appPrec ty
go d (PDelay _ tm) = parenthesise (d > appPrec) $ "Delay" <++> go appPrec tm
go d (PForce _ tm) = parenthesise (d > appPrec) $ "Force" <++> go appPrec tm
go d (PImplicitApp _ f Nothing a) =
go d (PAutoApp _ f a) =
parenthesise (d > appPrec) $ group $ go leftAppPrec f <++> "@" <+> braces (go startPrec a)
go d (PImplicitApp _ f (Just n) (PRef _ a)) =
go d (PNamedApp _ f n (PRef _ a)) =
parenthesise (d > appPrec) $ group $
if n == a
then go leftAppPrec f <++> braces (pretty n)
else go leftAppPrec f <++> braces (pretty n <++> equals <++> pretty a)
go d (PImplicitApp _ f (Just n) a) =
go d (PNamedApp _ f n a) =
parenthesise (d > appPrec) $ group $ go leftAppPrec f <++> braces (pretty n <++> equals <++> go d a)
go d (PSearch _ _) = pragma "%search"
go d (PQuote _ tm) = parenthesise (d > appPrec) $ "`" <+> parens (go startPrec tm)

24
src/Idris/Resugar.idr
View File

@ -234,20 +234,21 @@ mutual
= do ds' <- traverse toPFieldUpdate ds
f' <- toPTerm argPrec f
bracket p startPrec (PApp fc (PUpdate fc ds') f')
toPTerm p (IInstance fc n ds)
= do ds' <- traverse toPFieldUpdate ds
bracket p startPrec (PInstance fc n ds')
toPTerm p (IApp fc fn arg)
= do arg' <- toPTerm argPrec arg
app <- toPTermApp fn [(fc, Nothing, arg')]
bracket p appPrec app
toPTerm p (IAutoApp fc fn arg)
= do arg' <- toPTerm argPrec arg
app <- toPTermApp fn [(fc, Just Nothing, arg')]
bracket p appPrec app
toPTerm p (IWithApp fc fn arg)
= do arg' <- toPTerm startPrec arg
fn' <- toPTerm startPrec fn
bracket p appPrec (PWithApp fc fn' arg')
toPTerm p (IImplicitApp fc fn n arg)
toPTerm p (INamedApp fc fn n arg)
= do arg' <- toPTerm startPrec arg
app <- toPTermApp fn [(fc, Just n, arg')]
app <- toPTermApp fn [(fc, Just (Just n), arg')]
imp <- showImplicits
if imp
then bracket p startPrec app
@ -291,10 +292,13 @@ mutual
mkApp fn ((fc, Nothing, arg) :: rest)
= do let ap = sugarApp (PApp fc fn arg)
mkApp ap rest
mkApp fn ((fc, Just n, arg) :: rest)
= do imp <- showImplicits
mkApp fn ((fc, Just Nothing, arg) :: rest)
= do let ap = sugarApp (PAutoApp fc fn arg)
mkApp ap rest
mkApp fn ((fc, Just (Just n), arg) :: rest)
= do imp <- showImplicits --TODO rename to showNamed
if imp
then do let ap = PImplicitApp fc fn n arg
then do let ap = PNamedApp fc fn n arg
mkApp ap rest
else mkApp fn rest
@ -305,9 +309,9 @@ mutual
toPTermApp (IApp fc f a) args
= do a' <- toPTerm argPrec a
toPTermApp f ((fc, Nothing, a') :: args)
toPTermApp (IImplicitApp fc f n a) args
toPTermApp (INamedApp fc f n a) args
= do a' <- toPTerm startPrec a
toPTermApp f ((fc, Just n, a') :: args)
toPTermApp f ((fc, Just (Just n), a') :: args)
toPTermApp fn@(IVar fc n) args
= do defs <- get Ctxt
case !(lookupCtxtExact n (gamma defs)) of

31
src/Idris/Syntax.idr
View File

@ -47,10 +47,10 @@ mutual
PCase : FC -> PTerm -> List PClause -> PTerm
PLocal : FC -> List PDecl -> (scope : PTerm) -> PTerm
PUpdate : FC -> List PFieldUpdate -> PTerm
PInstance : FC -> Maybe Name -> List PFieldUpdate -> PTerm
PApp : FC -> PTerm -> PTerm -> PTerm
PWithApp : FC -> PTerm -> PTerm -> PTerm
PImplicitApp : FC -> PTerm -> (argn : Maybe Name) -> PTerm -> PTerm
PNamedApp : FC -> PTerm -> Name -> PTerm -> PTerm
PAutoApp : FC -> PTerm -> PTerm -> PTerm
PDelayed : FC -> LazyReason -> PTerm -> PTerm
PDelay : FC -> PTerm -> PTerm
@ -115,10 +115,10 @@ mutual
getPTermLoc (PCase fc _ _) = fc
getPTermLoc (PLocal fc _ _) = fc
getPTermLoc (PUpdate fc _) = fc
getPTermLoc (PInstance fc _ _) = fc
getPTermLoc (PApp fc _ _) = fc
getPTermLoc (PWithApp fc _ _) = fc
getPTermLoc (PImplicitApp fc _ _ _) = fc
getPTermLoc (PAutoApp fc _ _) = fc
getPTermLoc (PNamedApp fc _ _ _) = fc
getPTermLoc (PDelayed fc _ _) = fc
getPTermLoc (PDelay fc _) = fc
getPTermLoc (PForce fc _) = fc
@ -531,11 +531,9 @@ mutual
= "let { << definitions >> } in " ++ showPrec d sc
showPrec d (PUpdate _ fs)
= "record { " ++ showSep ", " (map showUpdate fs) ++ " }"
showPrec d (PInstance _ n fs)
= "record " ++ fromMaybe "_" (showPrec d <$> n) ++ " { " ++ showSep ", " (map showUpdate fs) ++ " }"
showPrec d (PApp _ f a) = showPrec App f ++ " " ++ showPrec App a
showPrec d (PWithApp _ f a) = showPrec d f ++ " | " ++ showPrec d a
showPrec d (PImplicitApp _ f Nothing a)
showPrec d (PAutoApp _ f a)
= showPrec d f ++ " @{" ++ showPrec d a ++ "}"
showPrec d (PDelayed _ LInf ty)
= showCon d "Inf" $ showArg ty
@ -545,11 +543,11 @@ mutual
= showCon d "Delay" $ showArg tm
showPrec d (PForce _ tm)
= showCon d "Force" $ showArg tm
showPrec d (PImplicitApp _ f (Just n) (PRef _ a))
showPrec d (PNamedApp _ f n (PRef _ a))
= if n == a
then showPrec d f ++ " {" ++ showPrec d n ++ "}"
else showPrec d f ++ " {" ++ showPrec d n ++ " = " ++ showPrec d a ++ "}"
showPrec d (PImplicitApp _ f (Just n) a)
showPrec d (PNamedApp _ f n a)
= showPrec d f ++ " {" ++ showPrec d n ++ " = " ++ showPrec d a ++ "}"
showPrec _ (PSearch _ _) = "%search"
showPrec d (PQuote _ tm) = "`(" ++ showPrec d tm ++ ")"
@ -796,9 +794,6 @@ mapPTermM f = goPTerm where
goPTerm (PUpdate fc xs) =
PUpdate fc <$> goPFieldUpdates xs
>>= f
goPTerm (PInstance fc n xs) =
PInstance fc n <$> goPFieldUpdates xs
>>= f
goPTerm (PApp fc x y) =
PApp fc <$> goPTerm x
<*> goPTerm y
@ -807,10 +802,14 @@ mapPTermM f = goPTerm where
PWithApp fc <$> goPTerm x
<*> goPTerm y
>>= f
goPTerm (PImplicitApp fc x argn y) =
PImplicitApp fc <$> goPTerm x
<*> pure argn
<*> goPTerm y
goPTerm (PAutoApp fc x y) =
PAutoApp fc <$> goPTerm x
<*> goPTerm y
>>= f
goPTerm (PNamedApp fc x n y) =
PNamedApp fc <$> goPTerm x
<*> pure n
<*> goPTerm y
>>= f
goPTerm (PDelayed fc x y) =
PDelayed fc x <$> goPTerm y

1
src/Parser/Lexer/Source.idr
View File

@ -186,6 +186,7 @@ symbols : List String
symbols
= [".(", -- for things such as Foo.Bar.(+)
"@{",
"${",
"[|", "|]",
"(", ")", "{", "}}", "}", "[", "]", ",", ";", "_",
"`(", "`{{", "`[", "`"]

12
src/TTImp/BindImplicits.idr
View File

@ -37,8 +37,10 @@ renameIBinds rs us (ILam fc c p n ty sc)
= pure $ ILam fc c p n !(renameIBinds rs us ty) !(renameIBinds rs us sc)
renameIBinds rs us (IApp fc fn arg)
= pure $ IApp fc !(renameIBinds rs us fn) !(renameIBinds rs us arg)
renameIBinds rs us (IImplicitApp fc fn n arg)
= pure $ IImplicitApp fc !(renameIBinds rs us fn) n !(renameIBinds rs us arg)
renameIBinds rs us (IAutoApp fc fn arg)
= pure $ IAutoApp fc !(renameIBinds rs us fn) !(renameIBinds rs us arg)
renameIBinds rs us (INamedApp fc fn n arg)
= pure $ INamedApp fc !(renameIBinds rs us fn) n !(renameIBinds rs us arg)
renameIBinds rs us (IWithApp fc fn arg)
= pure $ IWithApp fc !(renameIBinds rs us fn) !(renameIBinds rs us arg)
renameIBinds rs us (IAs fc s n pat)
@ -86,8 +88,10 @@ doBind ns (ILam fc rig p mn aty sc)
ILam fc rig p mn (doBind ns' aty) (doBind ns' sc)
doBind ns (IApp fc fn av)
= IApp fc (doBind ns fn) (doBind ns av)
doBind ns (IImplicitApp fc fn n av)
= IImplicitApp fc (doBind ns fn) n (doBind ns av)
doBind ns (IAutoApp fc fn av)
= IAutoApp fc (doBind ns fn) (doBind ns av)
doBind ns (INamedApp fc fn n av)
= INamedApp fc (doBind ns fn) n (doBind ns av)
doBind ns (IWithApp fc fn av)
= IWithApp fc (doBind ns fn) (doBind ns av)
doBind ns (IAs fc s n pat)

16
src/TTImp/Elab/Ambiguity.idr
View File

@ -97,8 +97,10 @@ expandAmbigName mode nest env orig args (IVar fc x) exp
buildAlt f [] = f
buildAlt f ((fc', Nothing, a) :: as)
= buildAlt (IApp fc' f a) as
buildAlt f ((fc', Just i, a) :: as)
= buildAlt (IImplicitApp fc' f i a) as
buildAlt f ((fc', Just Nothing, a) :: as)
= buildAlt (IAutoApp fc' f a) as
buildAlt f ((fc', Just (Just i), a) :: as)
= buildAlt (INamedApp fc' f i a) as
isPrimName : List Name -> Name -> Bool
isPrimName [] fn = False
@ -144,9 +146,12 @@ expandAmbigName mode nest env orig args (IVar fc x) exp
expandAmbigName mode nest env orig args (IApp fc f a) exp
= expandAmbigName mode nest env orig
((fc, Nothing, a) :: args) f exp
expandAmbigName mode nest env orig args (IImplicitApp fc f n a) exp
expandAmbigName mode nest env orig args (INamedApp fc f n a) exp
= expandAmbigName mode nest env orig
((fc, Just n, a) :: args) f exp
((fc, Just (Just n), a) :: args) f exp
expandAmbigName mode nest env orig args (IAutoApp fc f a) exp
= expandAmbigName mode nest env orig
((fc, Just Nothing, a) :: args) f exp
expandAmbigName elabmode nest env orig args tm exp
= do log "elab.ambiguous" 10 $ "No ambiguity " ++ show orig
pure orig
@ -315,7 +320,8 @@ checkAmbigDepth fc info
getName : RawImp -> Maybe Name
getName (IVar _ n) = Just n
getName (IApp _ f _) = getName f
getName (IImplicitApp _ f _ _) = getName f
getName (INamedApp _ f _ _) = getName f
getName (IAutoApp _ f _) = getName f
getName _ = Nothing
export

249
src/TTImp/Elab/App.idr
View File

@ -16,6 +16,7 @@ import TTImp.Elab.Record
import TTImp.TTImp
import Data.List
import Data.List1
%default covering
@ -139,11 +140,12 @@ mutual
Name -> NF vars -> (Defs -> Closure vars -> Core (NF vars)) ->
(argdata : (Maybe Name, Nat)) ->
(expargs : List RawImp) ->
(impargs : List (Maybe Name, RawImp)) ->
(autoargs : List RawImp) ->
(namedargs : List (Name, RawImp)) ->
(knownret : Bool) ->
(expected : Maybe (Glued vars)) ->
Core (Term vars, Glued vars)
makeImplicit rig argRig elabinfo nest env fc tm x aty sc (n, argpos) expargs impargs kr expty
makeImplicit rig argRig elabinfo nest env fc tm x aty sc (n, argpos) expargs autoargs namedargs kr expty
= do defs <- get Ctxt
nm <- genMVName x
empty <- clearDefs defs
@ -155,7 +157,7 @@ mutual
do est <- get EST
put EST (addBindIfUnsolved nm argRig Implicit env metaval metaty est)
checkAppWith rig elabinfo nest env fc
fntm fnty (n, 1 + argpos) expargs impargs kr expty
fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty
makeAutoImplicit : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
@ -168,11 +170,12 @@ mutual
Name -> NF vars -> (Defs -> Closure vars -> Core (NF vars)) ->
(argpos : (Maybe Name, Nat)) ->
(expargs : List RawImp) ->
(impargs : List (Maybe Name, RawImp)) ->
(autoargs : List RawImp) ->
(namedargs : List (Name, RawImp)) ->
(knownret : Bool) ->
(expected : Maybe (Glued vars)) ->
Core (Term vars, Glued vars)
makeAutoImplicit rig argRig elabinfo nest env fc tm x aty sc (n, argpos) expargs impargs kr expty
makeAutoImplicit rig argRig elabinfo nest env fc tm x aty sc (n, argpos) expargs autoargs namedargs kr expty
-- on the LHS, just treat it as an implicit pattern variable.
-- on the RHS, add a searchable hole
= if metavarImp (elabMode elabinfo)
@ -186,7 +189,7 @@ mutual
est <- get EST
put EST (addBindIfUnsolved nm argRig AutoImplicit env metaval metaty est)
checkAppWith rig elabinfo nest env fc
fntm fnty (n, 1 + argpos) expargs impargs kr expty
fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty
else do defs <- get Ctxt
nm <- genMVName x
-- We need the full normal form to check determining arguments
@ -199,7 +202,7 @@ mutual
let fntm = App fc tm metaval
fnty <- sc defs (toClosure defaultOpts env metaval)
checkAppWith rig elabinfo nest env fc
fntm fnty (n, 1 + argpos) expargs impargs kr expty
fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty
where
metavarImp : ElabMode -> Bool
metavarImp (InLHS _) = True
@ -218,11 +221,12 @@ mutual
(Defs -> Closure vars -> Core (NF vars)) ->
(argpos : (Maybe Name, Nat)) ->
(expargs : List RawImp) ->
(impargs : List (Maybe Name, RawImp)) ->
(autoargs : List RawImp) ->
(namedargs : List (Name, RawImp)) ->
(knownret : Bool) ->
(expected : Maybe (Glued vars)) ->
Core (Term vars, Glued vars)
makeDefImplicit rig argRig elabinfo nest env fc tm x arg aty sc (n, argpos) expargs impargs kr expty
makeDefImplicit rig argRig elabinfo nest env fc tm x arg aty sc (n, argpos) expargs autoargs namedargs kr expty
-- on the LHS, just treat it as an implicit pattern variable.
-- on the RHS, use the default
= if metavarImp (elabMode elabinfo)
@ -236,14 +240,14 @@ mutual
est <- get EST
put EST (addBindIfUnsolved nm argRig AutoImplicit env metaval metaty est)
checkAppWith rig elabinfo nest env fc
fntm fnty (n, 1 + argpos) expargs impargs kr expty
fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty
else do defs <- get Ctxt
empty <- clearDefs defs
aval <- quote empty env arg
let fntm = App fc tm aval
fnty <- sc defs (toClosure defaultOpts env aval)
checkAppWith rig elabinfo nest env fc
fntm fnty (n, 1 + argpos) expargs impargs kr expty
fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty
where
metavarImp : ElabMode -> Bool
metavarImp (InLHS _) = True
@ -262,7 +266,8 @@ mutual
(_ :: _ :: _) => True
_ => False
needsDelayExpr True (IApp _ f _) = needsDelayExpr True f
needsDelayExpr True (IImplicitApp _ f _ _) = needsDelayExpr True f
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 (ILocal _ _ _) = pure True
@ -279,7 +284,8 @@ mutual
RawImp -> Core Bool
needsDelayLHS (IVar fc n) = pure True
needsDelayLHS (IApp _ f _) = needsDelayLHS f
needsDelayLHS (IImplicitApp _ f _ _) = needsDelayLHS f
needsDelayLHS (IAutoApp _ f _) = needsDelayLHS f
needsDelayLHS (INamedApp _ f _ _) = needsDelayLHS f
needsDelayLHS (IAlternative _ _ _) = pure True
needsDelayLHS (ISearch _ _) = pure True
needsDelayLHS (IPrimVal _ _) = pure True
@ -377,12 +383,13 @@ mutual
(argdata : (Maybe Name, Nat)) ->
(arg : RawImp) ->
(expargs : List RawImp) ->
(impargs : List (Maybe Name, RawImp)) ->
(autoargs : List RawImp) ->
(namedargs : List (Name, RawImp)) ->
(knownret : Bool) ->
(expected : Maybe (Glued vars)) ->
Core (Term vars, Glued vars)
checkRestApp rig argRig elabinfo nest env fc tm x aty sc
(n, argpos) arg_in expargs impargs knownret expty
(n, argpos) arg_in expargs autoargs namedargs knownret expty
= do defs <- get Ctxt
arg <- dotErased aty n argpos (elabMode elabinfo) argRig arg_in
kr <- if knownret
@ -399,7 +406,7 @@ mutual
logTerm "elab" 10 "...as" metaval
fnty <- sc defs (toClosure defaultOpts env metaval)
(tm, gty) <- checkAppWith rig elabinfo nest env fc
fntm fnty (n, 1 + argpos) expargs impargs kr expty
fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty
defs <- get Ctxt
aty' <- nf defs env metaty
logNF "elab" 10 ("Now trying " ++ show nm ++ " " ++ show arg) env aty'
@ -448,7 +455,17 @@ mutual
let fntm = App fc tm argv
fnty <- sc defs (toClosure defaultOpts env argv)
checkAppWith rig elabinfo nest env fc
fntm fnty (n, 1 + argpos) expargs impargs kr expty
fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty
public export
findNamed : Name -> List (Name, RawImp) -> Maybe (List1 (Name, RawImp))
findNamed n l = case partition ((== n) . fst) l of
(x :: xs, ys) => Just (x ::: (xs ++ ys))
_ => Nothing
public export
findInfExpBinder : List (Name, RawImp) -> Maybe RawImp
findInfExpBinder = lookup (UN "_")
-- Check an application of 'fntm', with type 'fnty' to the given list
-- of explicit and implicit arguments.
@ -465,25 +482,64 @@ mutual
-- function we're applying, and argument position, for
-- checking if it's okay to erase against 'safeErase'
(expargs : List RawImp) ->
(impargs : List (Maybe Name, RawImp)) ->
(autoargs : List RawImp) ->
(namedargs : List (Name, RawImp)) ->
(knownret : Bool) -> -- Do we know what the return type is yet?
-- if we do, we might be able to use it to work
-- out the types of arguments before elaborating them
(expected : Maybe (Glued vars)) ->
Core (Term vars, Glued vars)
-- Ordinary explicit argument
checkAppWith rig elabinfo nest env fc tm (NBind tfc x (Pi _ rigb Explicit aty) sc)
argdata (arg :: expargs) impargs kr expty
= do let argRig = rig |*| rigb
checkRestApp rig argRig elabinfo nest env fc
tm x aty sc argdata arg expargs impargs kr expty
-- Explicit Pi, we use provided unnamed explicit argument
checkAppWith rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb Explicit aty) sc)
argdata (arg :: expargs') autoargs namedargs kr expty
= do let argRig = rig |*| rigb
checkRestApp rig argRig elabinfo nest env fc
tm x aty sc argdata arg expargs' autoargs namedargs kr expty
checkAppWith rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb Explicit aty) sc)
argdata [] autoargs namedargs kr expty with (findNamed x namedargs)
-- Explicit Pi, we found a compatible named argument
checkAppWith rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb Explicit aty) sc)
argdata [] autoargs namedargs kr expty | Just ((_, arg) ::: namedargs')
= do let argRig = rig |*| rigb
checkRestApp rig argRig elabinfo nest env fc
tm x aty sc argdata arg [] autoargs namedargs' kr expty
checkAppWith rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb Explicit aty) sc)
argdata [] autoargs namedargs kr expty | Nothing
= case findInfExpBinder namedargs of
Just arg =>
do let argRig = rig |*| rigb
checkRestApp rig argRig elabinfo nest env fc
tm x aty sc argdata arg [] autoargs namedargs kr expty
_ =>
do defs <- get Ctxt
checkExp rig elabinfo env fc tm (glueBack defs env ty) expty
-- checkAppWith rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb Explicit aty) sc)
-- argdata expargs autoargs namedargs kr expty with (findNamed x namedargs)
-- checkAppWith rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb Explicit aty) sc)
-- argdata expargs autoargs namedargs kr expty | Just ((_, arg) ::: namedargs')
-- -- Explicit Pi and we found a compatible named argument
-- = do let argRig = rig |*| rigb
-- checkRestApp rig argRig elabinfo nest env fc
-- tm x aty sc argdata arg expargs autoargs namedargs' kr expty
-- checkAppWith rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb Explicit aty) sc)
-- argdata expargs autoargs namedargs kr expty | Nothing
-- -- Explicit Pi, we try to use provided (unnamed) explicit argument
-- = case expargs of
-- arg :: expargs =>
-- do let argRig = rig |*| rigb
-- checkRestApp rig argRig elabinfo nest env fc
-- tm x aty sc argdata arg expargs autoargs namedargs kr expty
-- -- Explicit Pi, no proper argument found, throw an error
-- _ =>
-- do defs <- get Ctxt
-- checkExp rig elabinfo env fc tm (glueBack defs env ty) expty
-- Function type is delayed, so force the term and continue
checkAppWith rig elabinfo nest env fc tm (NDelayed dfc r ty@(NBind _ _ (Pi _ _ _ _) sc)) argdata expargs impargs kr expty
= checkAppWith rig elabinfo nest env fc (TForce dfc r tm) ty argdata expargs impargs kr expty
checkAppWith rig elabinfo nest env fc tm (NDelayed dfc r ty@(NBind _ _ (Pi _ _ _ _) sc)) argdata expargs autoargs namedargs kr expty
= checkAppWith rig elabinfo nest env fc (TForce dfc r tm) ty argdata expargs autoargs namedargs kr expty
-- If there's no more arguments given, and the plicities of the type and
-- the expected type line up, stop
checkAppWith rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb Implicit aty) sc)
argdata [] [] kr (Just expty_in)
argdata [] [] [] kr (Just expty_in)
= do let argRig = rig |*| rigb
expty <- getNF expty_in
defs <- get Ctxt
@ -491,22 +547,22 @@ mutual
NBind tfc' x' (Pi _ rigb' Implicit aty') sc'
=> checkExp rig elabinfo env fc tm (glueBack defs env ty) (Just expty_in)
_ => if not (preciseInf elabinfo)
then makeImplicit rig argRig elabinfo nest env fc tm x aty sc argdata [] [] kr (Just expty_in)
then makeImplicit rig argRig elabinfo nest env fc tm x aty sc argdata [] [] [] kr (Just expty_in)
-- in 'preciseInf' mode blunder on anyway, and hope
-- that we can resolve the implicits
else handle (checkExp rig elabinfo env fc tm (glueBack defs env ty) (Just expty_in))
(\err => makeImplicit rig argRig elabinfo nest env fc tm x aty sc argdata [] [] kr (Just expty_in))
(\err => makeImplicit rig argRig elabinfo nest env fc tm x aty sc argdata [] [] [] kr (Just expty_in))
checkAppWith rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb AutoImplicit aty) sc)
argdata [] [] kr (Just expty_in)
argdata [] [] [] kr (Just expty_in)
= do let argRig = rig |*| rigb
expty <- getNF expty_in
defs <- get Ctxt
case expty of
NBind tfc' x' (Pi _ rigb' AutoImplicit aty') sc'
=> checkExp rig elabinfo env fc tm (glueBack defs env ty) (Just expty_in)
_ => makeAutoImplicit rig argRig elabinfo nest env fc tm x aty sc argdata [] [] kr (Just expty_in)
_ => makeAutoImplicit rig argRig elabinfo nest env fc tm x aty sc argdata [] [] [] kr (Just expty_in)
checkAppWith rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb (DefImplicit aval) aty) sc)
argdata [] [] kr (Just expty_in)
argdata [] [] [] kr (Just expty_in)
= do let argRig = rigMult rig rigb
expty <- getNF expty_in
defs <- get Ctxt
@ -514,86 +570,58 @@ mutual
NBind tfc' x' (Pi _ rigb' (DefImplicit aval') aty') sc'
=> if !(convert defs env aval aval')
then checkExp rig elabinfo env fc tm (glueBack defs env ty) (Just expty_in)
else makeDefImplicit rig argRig elabinfo nest env fc tm x aval aty sc argdata [] [] kr (Just expty_in)
_ => makeDefImplicit rig argRig elabinfo nest env fc tm x aval aty sc argdata [] [] kr (Just expty_in)
else makeDefImplicit rig argRig elabinfo nest env fc tm x aval aty sc argdata [] [] [] kr (Just expty_in)
_ => makeDefImplicit rig argRig elabinfo nest env fc tm x aval aty sc argdata [] [] [] kr (Just expty_in)
-- Check next auto implicit argument
checkAppWith rig elabinfo nest env fc tm (NBind tfc x (Pi _ rigb AutoImplicit aty) sc)
argdata expargs impargs kr expty
argdata expargs autoargs namedargs kr expty
= let argRig = rig |*| rigb in
case useAutoImp [] impargs of
Nothing => makeAutoImplicit rig argRig elabinfo nest env fc tm
x aty sc argdata expargs impargs kr expty
Just (arg, impargs') =>
checkRestApp rig argRig elabinfo nest env fc
tm x aty sc argdata arg expargs impargs' kr expty
where
useAutoImp : List (Maybe Name, RawImp) -> List (Maybe Name, RawImp) ->
Maybe (RawImp, List (Maybe Name, RawImp))
useAutoImp acc [] = Nothing
useAutoImp acc ((Nothing, xtm) :: rest)
= Just (xtm, reverse acc ++ rest)
useAutoImp acc ((Just x', xtm) :: rest)
= if x == x'
then Just (xtm, reverse acc ++ rest)
else useAutoImp ((Just x', xtm) :: acc) rest
useAutoImp acc (ximp :: rest)
= useAutoImp (ximp :: acc) rest
case findNamed x namedargs of
Just ((_, arg) ::: namedargs) =>
checkRestApp rig argRig elabinfo nest env fc
tm x aty sc argdata arg expargs autoargs namedargs kr expty
Nothing =>
case autoargs of
arg :: autoargs =>
checkRestApp rig argRig elabinfo nest env fc
tm x aty sc argdata arg expargs autoargs namedargs kr expty
[] => makeAutoImplicit rig argRig elabinfo nest env fc tm
x aty sc argdata expargs [] namedargs kr expty
-- Check next implicit argument
checkAppWith rig elabinfo nest env fc tm (NBind tfc x (Pi _ rigb Implicit aty) sc)
argdata expargs impargs kr expty
argdata expargs autoargs namedargs kr expty
= let argRig = rig |*| rigb in
case useImp [] impargs of
case findNamed x namedargs of
Nothing => makeImplicit rig argRig elabinfo nest env fc tm
x aty sc argdata expargs impargs kr expty
Just (arg, impargs') =>
x aty sc argdata expargs autoargs namedargs kr expty
Just ((_, arg) ::: namedargs) =>
checkRestApp rig argRig elabinfo nest env fc
tm x aty sc argdata arg expargs impargs' kr expty
where
useImp : List (Maybe Name, RawImp) -> List (Maybe Name, RawImp) ->
Maybe (RawImp, List (Maybe Name, RawImp))
useImp acc [] = Nothing
useImp acc ((Just x', xtm) :: rest)
= if x == x'
then Just (xtm, reverse acc ++ rest)
else useImp ((Just x', xtm) :: acc) rest
useImp acc (ximp :: rest)
= useImp (ximp :: acc) rest
tm x aty sc argdata arg expargs autoargs namedargs kr expty
-- Check next default argument
checkAppWith rig elabinfo nest env fc tm (NBind tfc x (Pi _ rigb (DefImplicit arg) aty) sc)
argdata expargs impargs kr expty
argdata expargs autoargs namedargs kr expty
= let argRig = rigMult rig rigb in
case useImp [] impargs of
case findNamed x namedargs of
Nothing => makeDefImplicit rig argRig elabinfo nest env fc tm
x arg aty sc argdata expargs impargs kr expty
Just (arg, impargs') =>
x arg aty sc argdata expargs autoargs namedargs kr expty
Just ((_, arg) ::: namedargs) =>
checkRestApp rig argRig elabinfo nest env fc
tm x aty sc argdata arg expargs impargs' kr expty
where
useImp : List (Maybe Name, RawImp) -> List (Maybe Name, RawImp) ->
Maybe (RawImp, List (Maybe Name, RawImp))
useImp acc [] = Nothing
useImp acc ((Just x', xtm) :: rest)
= if x == x'
then Just (xtm, reverse acc ++ rest)
else useImp ((Just x', xtm) :: acc) rest
useImp acc (ximp :: rest)
= useImp (ximp :: acc) rest
tm x aty sc argdata arg expargs autoargs namedargs kr expty
checkAppWith rig elabinfo nest env fc tm ty argdata [] [] kr expty
checkAppWith rig elabinfo nest env fc tm ty argdata [] [] [] kr expty
= do defs <- get Ctxt
checkExp rig elabinfo env fc tm (glueBack defs env ty) expty
checkAppWith rig elabinfo nest env fc tm ty argdata [] impargs kr expty
= case filter notInfer impargs of
[] => checkAppWith rig elabinfo nest env fc tm ty argdata [] [] kr expty
is => throw (InvalidImplicits fc env (map fst is) tm)
checkAppWith rig elabinfo nest env fc tm ty argdata [] autoargs namedargs kr expty
= case filter notInferable (autoargs ++ map snd namedargs) of
[] => checkAppWith rig elabinfo nest env fc tm ty argdata [] [] [] kr expty
is => throw (InvalidArgs fc env (map (const Nothing) autoargs ++ map (Just . fst) namedargs) tm)
where
notInfer : (Maybe Name, RawImp) -> Bool
notInfer (_, Implicit _ _) = False
notInfer (n, IAs _ _ _ i) = notInfer (n, i)
notInfer _ = True
checkAppWith {vars} rig elabinfo nest env fc tm ty (n, argpos) (arg :: expargs) impargs kr expty
notInferable : RawImp -> Bool
notInferable (Implicit _ _) = False
notInferable (IAs _ _ _ i) = notInferable i
notInferable _ = True
checkAppWith {vars} rig elabinfo nest env fc tm ty (n, argpos) (arg :: expargs) autoargs namedargs kr expty
= -- Invent a function type, and hope that we'll know enough to solve it
-- later when we unify with expty
do logNF "elab.with" 10 "Function type" env ty
@ -613,7 +641,7 @@ mutual
let expfnty = gnf env (Bind fc argn (Pi fc top Explicit argTy) (weaken retTy))
logGlue "elab.with" 10 "Expected function type" env expfnty
maybe (pure ()) (logGlue "elab.with" 10 "Expected result type" env) expty
res <- checkAppWith rig elabinfo nest env fc fntm fnty (n, 1 + argpos) expargs impargs kr expty
res <- checkAppWith rig elabinfo nest env fc fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty
cres <- Check.convert fc elabinfo env (glueBack defs env ty) expfnty
let [] = constraints cres
| cs => do cty <- getTerm expfnty
@ -631,24 +659,17 @@ checkApp : {vars : _} ->
NestedNames vars -> Env Term vars ->
FC -> (fn : RawImp) ->
(expargs : List RawImp) ->
(impargs : List (Maybe Name, RawImp)) ->
(mkFullyApplied : RawImp -> RawImp) ->
(autoargs : List RawImp) ->
(namedargs : List (Name, RawImp)) ->
Maybe (Glued vars) ->
Core (Term vars, Glued vars)
checkApp rig elabinfo nest env fc (IApp fc' fn arg) expargs impargs mkFull exp
= checkApp rig elabinfo nest env fc' fn (arg :: expargs) impargs (\fn => mkFull (IApp fc' fn arg)) exp
checkApp rig elabinfo nest env fc (IImplicitApp fc' fn nm arg) expargs impargs mkFull exp
= checkApp rig elabinfo nest env fc' fn expargs ((nm, arg) :: impargs) (\fn => mkFull (IImplicitApp fc' fn nm arg)) exp
checkApp rig elabinfo nest env fc (IInstance fc' name fs) expargs impargs mkFull exp
= do mbelabs <- elabInstance rig elabinfo nest env fc' name fs mkFull exp
case mbelabs of
Right elabs =>
let namedElabs = map (\(name, args) =>
( Just name
, checkApp rig elabinfo nest env fc (apply (IVar fc name) args) expargs impargs mkFull exp)) elabs in
exactlyOne fc env namedElabs
Left (meta, ty) => pure (meta, ty)
checkApp rig elabinfo nest env fc (IVar fc' n) expargs impargs _ exp
checkApp rig elabinfo nest env fc (IApp fc' fn arg) expargs autoargs namedargs exp
= checkApp rig elabinfo nest env fc' fn (arg :: expargs) autoargs namedargs exp
checkApp rig elabinfo nest env fc (IAutoApp fc' fn arg) expargs autoargs namedargs exp
= checkApp rig elabinfo nest env fc' fn expargs (arg :: autoargs) namedargs exp
checkApp rig elabinfo nest env fc (INamedApp fc' fn nm arg) expargs autoargs namedargs exp
= checkApp rig elabinfo nest env fc' fn expargs autoargs ((nm, arg) :: namedargs) exp
checkApp rig elabinfo nest env fc (IVar fc' n) expargs autoargs namedargs exp
= do (ntm, arglen, nty_in) <- getVarType rig nest env fc n
nty <- getNF nty_in
let prims = mapMaybe id
@ -672,7 +693,7 @@ checkApp rig elabinfo nest env fc (IVar fc' n) expargs impargs _ exp
Just (Just n', _) => n'
_ => n
normalisePrims prims env
!(checkAppWith rig elabinfo nest env fc ntm nty (Just fn, arglen) expargs impargs False exp)
!(checkAppWith rig elabinfo nest env fc ntm nty (Just fn, arglen) expargs autoargs namedargs False exp)
where
isPrimName : List Name -> Name -> Bool
isPrimName [] fn = False
@ -715,7 +736,7 @@ checkApp rig elabinfo nest env fc (IVar fc' n) expargs impargs _ exp
else pure elabinfo
updateElabInfo _ _ _ _ info = pure info
checkApp rig elabinfo nest env fc fn expargs impargs _ exp
checkApp rig elabinfo nest env fc fn expargs autoargs namedargs exp
= do (fntm, fnty_in) <- checkImp rig elabinfo nest env fn Nothing
fnty <- getNF fnty_in
checkAppWith rig elabinfo nest env fc fntm fnty (Nothing, 0) expargs impargs False exp
checkAppWith rig elabinfo nest env fc fntm fnty (Nothing, 0) expargs autoargs namedargs False exp

2
src/TTImp/Elab/Case.idr
View File

@ -405,7 +405,7 @@ checkCase rig elabinfo nest env fc scr scrty_in alts exp
= applyTo defs (IApp fc ty (Implicit fc False))
!(sc defs (toClosure defaultOpts [] (Erased fc False)))
applyTo defs ty (NBind _ x (Pi _ _ _ _) sc)
= applyTo defs (IImplicitApp fc ty (Just x) (Implicit fc False))
= applyTo defs (INamedApp fc ty x (Implicit fc False))
!(sc defs (toClosure defaultOpts [] (Erased fc False)))
applyTo defs ty _ = pure ty

9
src/TTImp/Elab/Local.idr
View File

@ -34,9 +34,10 @@ checkLocal {vars} rig elabinfo nest env fc nestdecls_in scope expty
= do est <- get EST
let f = defining est
defs <- get Ctxt
let vis = case !(lookupCtxtExact (Resolved (defining est)) (gamma defs)) of
Just gdef => visibility gdef
Nothing => Public
vis <- case !(lookupCtxtExact (Resolved (defining est)) (gamma defs)) of
Just gdef => do log "elab.local" 8 $ "Defining def: " ++ !(prettyName gdef.fullname)
pure $ visibility gdef
Nothing => pure Public
-- If the parent function is public, the nested definitions need
-- to be public too
let nestdecls =
@ -44,9 +45,11 @@ checkLocal {vars} rig elabinfo nest env fc nestdecls_in scope expty
then map setPublic nestdecls_in
else nestdecls_in
let defNames = definedInBlock emptyNS nestdecls
log "elab.local" 8 $ "Nested names: " ++ show !(traverse prettyName defNames)
names' <- traverse (applyEnv f)
(nub defNames) -- binding names must be unique
-- fixes bug #115
--log "elab.local" 8 $ "Visible applied unique: " ++ show !(traverse prettyName names')
let nest' = record { names $= (names' ++) } nest
let env' = dropLinear env
-- We don't want to keep rechecking delayed elaborators in the

6
src/TTImp/Elab/Quote.idr
View File

@ -42,8 +42,10 @@ mutual
= pure $ IUpdate fc !(traverse getUnquoteUpdate ds) !(getUnquote sc)
getUnquote (IApp fc f a)
= pure $ IApp fc !(getUnquote f) !(getUnquote a)
getUnquote (IImplicitApp fc f n a)
= pure $ IImplicitApp fc !(getUnquote f) n !(getUnquote a)
getUnquote (IAutoApp fc f a)
= pure $ IAutoApp fc !(getUnquote f) !(getUnquote a)
getUnquote (INamedApp fc f n a)
= pure $ INamedApp fc !(getUnquote f) n !(getUnquote a)
getUnquote (IWithApp fc f a)
= pure $ IWithApp fc !(getUnquote f) !(getUnquote a)
getUnquote (IAlternative fc at as)

115
src/TTImp/Elab/Record.idr
View File

@ -40,7 +40,7 @@ applyImp f [] = f
applyImp f ((Nothing, arg) :: xs)
= applyImp (IApp (getFC f) f arg) xs
applyImp f ((Just n, arg) :: xs)
= applyImp (IImplicitApp (getFC f) f (Just n) arg) xs
= applyImp (INamedApp (getFC f) f n arg) xs
toLHS' : FC -> Rec -> (Maybe Name, RawImp)
toLHS' loc (Field mn@(Just _) n _)
@ -235,116 +235,3 @@ checkUpdate rig elabinfo nest env fc upds rec expected
rcase <- recUpdate rig elabinfo fc nest env upds rec recty'
log "elab.record" 5 $ "Record update: " ++ show rcase
check rig elabinfo nest env rcase expected
export
elabInstance : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto m : Ref MD Metadata} ->
{auto u : Ref UST UState} ->
{auto e : Ref EST (EState vars)} ->
RigCount ->
ElabInfo ->
NestedNames vars ->
Env Term vars ->
FC -> Maybe Name -> List IFieldUpdate ->
(RawImp -> RawImp) ->
Maybe (Glued vars) ->
Core (Either (Term vars, Glued vars) (List (Name, List RawImp))) -- a hole or 1+ possible elaborations
elabInstance rig elabinfo nest env fc mbprovidedName fs mkFull expected
= case mbprovidedName of
Just providedName => do
defs <- get Ctxt
names@(_ :: _) <- getConNames defs providedName
| _ => throw (NotRecordType fc providedName)
names@(_ :: _) <- do expFldsForEachCon <- traverse (bitraverse pure (findFieldsExplicit defs) . dup) names
pure $ mapMaybe (sequenceM . mapFst pure) expFldsForEachCon
| _ => throw errorConstructorNotFound
providedfields <- traverse getName fs
let True = length providedfields == length (nub providedfields)
| _ => throw (GenericMsg fc "Duplicate fields.")
let (Right fullnames) = tryDisambigConName fc env names providedfields
| Left err => throw err
fs' <- traverse (bitraverse getName getExp . dup) fs
res <- for fullnames \(fullname, allfields) => do
seqexp <- flip traverse allfields \x => lookupOrElse x fs' (throw (NotCoveredField fc x))
pure (fullname, seqexp)
pure (Right res)
Nothing => do defs <- get Ctxt
let full = mkFull (IInstance fc mbprovidedName fs)
let fullLoc = getFC full
tyormeta <- mkExpected expected fullLoc
pure $ Left !(delayOnFailure fullLoc rig env tyormeta needType 5 (const $ elabCon tyormeta fullLoc))
where
mkExpected : Maybe (Glued vars) -> FC -> Core (Glued vars)
mkExpected (Just ty) _ = pure ty
mkExpected Nothing fc
= do nm <- genName "delayTy"
ty <- metaVar fc erased env nm (TType fc)
pure (gnf env ty)
errorConstructorNotFound : Error
errorConstructorNotFound = GenericMsg fc "No constructor satisfies provided fields."
sequenceCore : (Core a, Core b) -> Core (a, b) -- specialize
sequenceCore (x, y) = do
x' <- x
y' <- y
pure (x', y')
sequenceM : forall a, b, m. Monad m => (m a, m b) -> m (a, b) -- Core is not a monad
sequenceM (mx, my)
= do x <- mx
y <- my
pure (x, y)
bimap : forall a, b, a', b'. (a -> a') -> (b -> b') -> (a, b) -> (a', b')
bimap f g (x, y) = (f x, g y)
bitraverse : (a -> Core a') -> (b -> Core b') -> (a, b) -> Core (a', b')
bitraverse f g p = sequenceCore (bimap f g p)
lookupOrElse : forall a. Eq a => a -> List (a, b) -> Core b -> Core b
lookupOrElse x xs def
= case lookup x xs of
Nothing => def
(Just x) => pure x
subsetOf : forall a. Eq a => List a -> List a -> Bool
subsetOf subset set = length (intersect subset set) == length subset
getName : IFieldUpdate -> Core String
getName (ISetField [name] _) = pure name
getName _ = throw (InternalError "impossible")
getExp : IFieldUpdate -> Core RawImp
getExp (ISetField _ exp) = pure exp
getExp _ = throw (InternalError "impossible")
getConNames : Defs -> Name -> Core (List Name)
getConNames defs name
= do list <- lookupDefName name (gamma defs)
pure $ map fst list
findFieldsExplicit : Defs -> Name -> Core (Maybe (List String))
findFieldsExplicit defs con = pure $ map (map fst) $ map (filter (isNothing . fst . snd)) !(findFields defs con)
tryDisambigConName : {vars : _}
-> FC
-> Env Term vars
-> List (Name, List String)
-> List String
-> Either Error (List (Name, List String))
tryDisambigConName fc env exactNames fields
= case filter fst $ map (mapFst (subsetOf fields . snd) . dup) exactNames of
[] => Left errorConstructorNotFound
oneOrMoreNames => Right (map snd oneOrMoreNames)
elabCon : (ty : Glued vars) -> FC -> Core (Term vars, Glued vars)
elabCon gty fullLoc
= do defs <- get Ctxt
tynf <- getNF gty
let (Just tconName) = getRecordType env tynf
| _ => throw (RecordTypeNeeded fullLoc env)
(Just conName) <- findConName defs tconName
| mbnames => throw (InternalError (show mbnames))
check rig elabinfo nest env (mkFull (IInstance fc (Just conName) fs)) expected

12
src/TTImp/Elab/Term.idr
View File

@ -125,7 +125,7 @@ checkTerm rig elabinfo nest env (IVar fc n) exp
= -- It may actually turn out to be an application, if the expected
-- type is expecting an implicit argument, so check it as an
-- application with no arguments
checkApp rig elabinfo nest env fc (IVar fc n) [] [] id exp
checkApp rig elabinfo nest env fc (IVar fc n) [] [] [] exp
checkTerm rig elabinfo nest env (IPi fc r p Nothing argTy retTy) exp
= do n <- case p of
Explicit => genVarName "arg"
@ -152,14 +152,14 @@ checkTerm rig elabinfo nest env (ICaseLocal fc uname iname args scope) exp
= checkCaseLocal rig elabinfo nest env fc uname iname args scope exp
checkTerm rig elabinfo nest env (IUpdate fc upds rec) exp
= checkUpdate rig elabinfo nest env fc upds rec exp
checkTerm rig elabinfo nest env (IInstance fc n fs) exp
= checkApp rig elabinfo nest env fc (IInstance fc n fs) [] [] id exp
checkTerm rig elabinfo nest env (IApp fc fn arg) exp
= checkApp rig elabinfo nest env fc fn [arg] [] (\fn => IApp fc fn arg) exp
= checkApp rig elabinfo nest env fc fn [arg] [] [] exp
checkTerm rig elabinfo nest env (IAutoApp fc fn arg) exp
= checkApp rig elabinfo nest env fc fn [] [arg] [] exp
checkTerm rig elabinfo nest env (IWithApp fc fn arg) exp
= throw (GenericMsg fc "with application not implemented yet")
checkTerm rig elabinfo nest env (IImplicitApp fc fn nm arg) exp
= checkApp rig elabinfo nest env fc fn [] [(nm, arg)] (\fn => IImplicitApp fc fn nm arg) exp
checkTerm rig elabinfo nest env (INamedApp fc fn nm arg) exp
= checkApp rig elabinfo nest env fc fn [] [] [(nm, arg)] exp
checkTerm rig elabinfo nest env (ISearch fc depth) (Just gexpty)
= do est <- get EST
nm <- genName "search"

113
src/TTImp/Impossible.idr
View File

@ -7,8 +7,10 @@ import Core.TT
import Core.Value
import TTImp.TTImp
import TTImp.Elab.App
import Data.List
import Data.List1
%default covering
@ -61,69 +63,57 @@ mutual
processArgs : {auto c : Ref Ctxt Defs} ->
{auto q : Ref QVar Int} ->
Term [] -> NF [] ->
(expargs : List RawImp) -> (impargs : List (Maybe Name, RawImp)) ->
(expargs : List RawImp) ->
(autoargs : List RawImp) ->
(namedargs : List (Name, RawImp)) ->
Core ClosedTerm
processArgs fn (NBind fc x (Pi _ _ Explicit ty) sc) (e :: exp) imp
= do e' <- mkTerm e (Just ty) [] []
processArgs fn (NBind fc x (Pi _ _ Explicit ty) sc) (e :: exps) autos named
= do e' <- mkTerm e (Just ty) [] [] []
defs <- get Ctxt
processArgs (App fc fn e') !(sc defs (toClosure defaultOpts [] e'))
exp imp
processArgs fn (NBind fc x (Pi _ _ Implicit ty) sc) exp imp
exps autos named
processArgs fn (NBind fc x (Pi _ _ Implicit ty) sc) exps autos named
= do defs <- get Ctxt
case useImp [] imp of
case findNamed x named of
Nothing => do e' <- nextVar fc
processArgs (App fc fn e')
!(sc defs (toClosure defaultOpts [] e'))
exp imp
Just (e, impargs') =>
do e' <- mkTerm e (Just ty) [] []
exps autos named
Just ((_, e) ::: named') =>
do e' <- mkTerm e (Just ty) [] [] []
processArgs (App fc fn e') !(sc defs (toClosure defaultOpts [] e'))
exp impargs'
where
useImp : List (Maybe Name, RawImp) -> List (Maybe Name, RawImp) ->
Maybe (RawImp, List (Maybe Name, RawImp))
useImp acc [] = Nothing
useImp acc ((Just x', xtm) :: rest)
= if x == x'
then Just (xtm, reverse acc ++ rest)
else useImp ((Just x', xtm) :: acc) rest
useImp acc (ximp :: rest)
= useImp (ximp :: acc) rest
processArgs fn (NBind fc x (Pi _ _ AutoImplicit ty) sc) exp imp
exps autos named'
processArgs fn (NBind fc x (Pi _ _ AutoImplicit ty) sc) exps autos named
= do defs <- get Ctxt
case useAutoImp [] imp of
Nothing => do e' <- nextVar fc
processArgs (App fc fn e')
!(sc defs (toClosure defaultOpts [] e'))
exp imp
Just (e, impargs') =>
do e' <- mkTerm e (Just ty) [] []
case findNamed x named of
Nothing => case autos of
(e :: autos') =>
do e' <- mkTerm e (Just ty) [] [] []
processArgs (App fc fn e') !(sc defs (toClosure defaultOpts [] e'))
exps autos' named
_ =>
do e' <- nextVar fc
processArgs (App fc fn e')
!(sc defs (toClosure defaultOpts [] e'))
exps [] named
Just ((_, e) ::: named') =>
do e' <- mkTerm e (Just ty) [] [] []
processArgs (App fc fn e') !(sc defs (toClosure defaultOpts [] e'))
exp impargs'
where
useAutoImp : List (Maybe Name, RawImp) -> List (Maybe Name, RawImp) ->
Maybe (RawImp, List (Maybe Name, RawImp))
useAutoImp acc [] = Nothing
useAutoImp acc ((Nothing, xtm) :: rest)
= Just (xtm, reverse acc ++ rest)
useAutoImp acc ((Just x', xtm) :: rest)
= if x == x'
then Just (xtm, reverse acc ++ rest)
else useAutoImp ((Just x', xtm) :: acc) rest
useAutoImp acc (ximp :: rest)
= useAutoImp (ximp :: acc) rest
processArgs fn ty [] [] = pure fn
processArgs fn ty exp imp
exps autos named'
processArgs fn ty [] [] [] = pure fn
processArgs fn ty exps autos named
= throw (GenericMsg (getLoc fn)
("Badly formed impossible clause "
++ show (fn, exp, imp)))
++ show (fn, exps, autos, named)))
buildApp : {auto c : Ref Ctxt Defs} ->
{auto q : Ref QVar Int} ->
FC -> Name -> Maybe (NF []) ->
(expargs : List RawImp) -> (impargs : List (Maybe Name, RawImp)) ->
(expargs : List RawImp) ->
(autoargs : List RawImp) ->
(namedargs : List (Name, RawImp)) ->
Core ClosedTerm
buildApp fc n mty exp imp
buildApp fc n mty exps autos named
= do defs <- get Ctxt
fi <- fromIntegerName
si <- fromStringName
@ -136,21 +126,25 @@ mutual
| [] => throw (UndefinedName fc n)
| ts => throw (AmbiguousName fc (map fst ts))
tynf <- nf defs [] ty
processArgs (Ref fc Func n') tynf exp imp
processArgs (Ref fc Func n') tynf exps autos named
mkTerm : {auto c : Ref Ctxt Defs} ->
{auto q : Ref QVar Int} ->
RawImp -> Maybe (NF []) ->
(expargs : List RawImp) -> (impargs : List (Maybe Name, RawImp)) ->
(expargs : List RawImp) ->
(autoargs : List RawImp) ->
(namedargs : List (Name, RawImp)) ->
Core ClosedTerm
mkTerm (IVar fc n) mty exp imp
= buildApp fc n mty exp imp
mkTerm (IApp fc fn arg) mty exp imp
= mkTerm fn mty (arg :: exp) imp
mkTerm (IImplicitApp fc fn nm arg) mty exp imp
= mkTerm fn mty exp ((nm, arg) :: imp)
mkTerm (IPrimVal fc c) _ _ _ = pure (PrimVal fc c)
mkTerm tm _ _ _ = nextVar (getFC tm)
mkTerm (IVar fc n) mty exps autos named
= buildApp fc n mty exps autos named
mkTerm (IApp fc fn arg) mty exps autos named
= mkTerm fn mty (arg :: exps) autos named
mkTerm (IAutoApp fc fn arg) mty exps autos named
= mkTerm fn mty exps (arg :: autos) named
mkTerm (INamedApp fc fn nm arg) mty exps autos named
= mkTerm fn mty exps autos ((nm, arg) :: named)
mkTerm (IPrimVal fc c) _ _ _ _ = pure (PrimVal fc c)
mkTerm tm _ _ _ _ = nextVar (getFC tm)
-- Given an LHS that is declared 'impossible', build a term to match from,
-- so that when we build the case tree for checking coverage, we take into
@ -161,7 +155,7 @@ getImpossibleTerm : {vars : _} ->
Env Term vars -> NestedNames vars -> RawImp -> Core ClosedTerm
getImpossibleTerm env nest tm
= do q <- newRef QVar (the Int 0)
mkTerm (applyEnv tm) Nothing [] []
mkTerm (applyEnv tm) Nothing [] [] []
where
addEnv : {vars : _} ->
FC -> Env Term vars -> List RawImp
@ -182,6 +176,7 @@ getImpossibleTerm env nest tm
-- the name to the proper one from the nested names map
applyEnv : RawImp -> RawImp
applyEnv (IApp fc fn arg) = IApp fc (applyEnv fn) arg
applyEnv (IImplicitApp fc fn n arg)
= IImplicitApp fc (applyEnv fn) n arg
applyEnv (IAutoApp fc fn arg) = IAutoApp fc (applyEnv fn) arg
applyEnv (INamedApp fc fn n arg)
= INamedApp fc (applyEnv fn) n arg
applyEnv tm = apply (expandNest tm) (addEnv (getFC tm) env)

40
src/TTImp/Interactive/CaseSplit.idr
View File

@ -218,16 +218,20 @@ updateArg allvars var con (IVar fc n)
updateArg allvars var con (IApp fc f a)
= pure $ IApp fc !(updateArg allvars var con f)
!(updateArg allvars var con a)
updateArg allvars var con (IImplicitApp fc f n a)
= pure $ IImplicitApp fc !(updateArg allvars var con f) n
!(updateArg allvars var con a)
updateArg allvars var con (IAutoApp fc f a)
= pure $ IAutoApp fc !(updateArg allvars var con f)
!(updateArg allvars var con a)
updateArg allvars var con (INamedApp fc f n a)
= pure $ INamedApp fc !(updateArg allvars var con f) n
!(updateArg allvars var con a)
updateArg allvars var con (IAs fc s n p)
= updateArg allvars var con p
updateArg allvars var con tm = pure $ Implicit (getFC tm) True
data ArgType
= Explicit FC RawImp
| Implicit FC (Maybe Name) RawImp
| Auto FC RawImp
| Named FC Name RawImp
update : {auto c : Ref Ctxt Defs} ->
List Name -> -- all the variable names
@ -235,19 +239,24 @@ update : {auto c : Ref Ctxt Defs} ->
ArgType -> Core ArgType
update allvars var con (Explicit fc arg)
= pure $ Explicit fc !(updateArg allvars var con arg)
update allvars var con (Implicit fc n arg)
= pure $ Implicit fc n !(updateArg allvars var con arg)
update allvars var con (Auto fc arg)
= pure $ Auto fc !(updateArg allvars var con arg)
update allvars var con (Named fc n arg)
= pure $ Named fc n !(updateArg allvars var con arg)
getFnArgs : RawImp -> List ArgType -> (RawImp, List ArgType)
getFnArgs (IApp fc tm a) args
= getFnArgs tm (Explicit fc a :: args)
getFnArgs (IImplicitApp fc tm n a) args
= getFnArgs tm (Implicit fc n a :: args)
getFnArgs (IAutoApp fc tm a) args
= getFnArgs tm (Auto fc a :: args)
getFnArgs (INamedApp fc tm n a) args
= getFnArgs tm (Named fc n a :: args)
getFnArgs tm args = (tm, args)
apply : RawImp -> List ArgType -> RawImp
apply f (Explicit fc a :: args) = apply (IApp fc f a) args
apply f (Implicit fc n a :: args) = apply (IImplicitApp fc f n a) args
apply f (Auto fc a :: args) = apply (IAutoApp fc f a) args
apply f (Named fc n a :: args) = apply (INamedApp fc f n a) args
apply f [] = f
-- Return a new LHS to check, replacing 'var' with an application of 'con'
@ -295,11 +304,18 @@ findUpdates defs (IVar fc n) tm = recordUpdate fc n tm
findUpdates defs (IApp _ f a) (IApp _ f' a')
= do findUpdates defs f f'
findUpdates defs a a'
findUpdates defs (IImplicitApp _ f _ a) (IImplicitApp _ f' _ a')
findUpdates defs (IAutoApp _ f a) (IAutoApp _ f' a')
= do findUpdates defs f f'
findUpdates defs a a'
findUpdates defs (IImplicitApp _ f _ a) f' = findUpdates defs f f'
findUpdates defs f (IImplicitApp _ f' _ a) = findUpdates defs f f'
findUpdates defs (IAutoApp _ f a) f'
= findUpdates defs f f'
findUpdates defs f (IAutoApp _ f' a)
= findUpdates defs f f'
findUpdates defs (INamedApp _ f _ a) (INamedApp _ f' _ a')
= do findUpdates defs f f'
findUpdates defs a a'
findUpdates defs (INamedApp _ f _ a) f' = findUpdates defs f f'
findUpdates defs f (INamedApp _ f' _ a) = findUpdates defs f f'
findUpdates defs (IAs _ _ _ f) f' = findUpdates defs f f'
findUpdates defs f (IAs _ _ _ f') = findUpdates defs f f'
findUpdates _ _ _ = pure ()

12
src/TTImp/Interactive/GenerateDef.idr
View File

@ -91,7 +91,9 @@ splittableNames (IApp _ f (IBindVar _ n))
= splittableNames f ++ [UN n]
splittableNames (IApp _ f _)
= splittableNames f
splittableNames (IImplicitApp _ f _ _)
splittableNames (IAutoApp _ f _)
= splittableNames f
splittableNames (INamedApp _ f _ _)
= splittableNames f
splittableNames _ = []
@ -114,7 +116,8 @@ trySplit loc lhsraw lhs rhs n
fixNames (IVar loc' (UN n)) = IBindVar loc' n
fixNames (IVar loc' (MN _ _)) = Implicit loc' True
fixNames (IApp loc' f a) = IApp loc' (fixNames f) (fixNames a)
fixNames (IImplicitApp loc' f t a) = IImplicitApp loc' (fixNames f) t (fixNames a)
fixNames (IAutoApp loc' f a) = IAutoApp loc' (fixNames f) (fixNames a)
fixNames (INamedApp loc' f t a) = INamedApp loc' (fixNames f) t (fixNames a)
fixNames tm = tm
updateLHS : List (Name, RawImp) -> RawImp -> RawImp
@ -127,8 +130,9 @@ trySplit loc lhsraw lhs rhs n
Nothing => IBindVar loc' n
Just tm => fixNames tm
updateLHS ups (IApp loc' f a) = IApp loc' (updateLHS ups f) (updateLHS ups a)
updateLHS ups (IImplicitApp loc' f t a)
= IImplicitApp loc' (updateLHS ups f) t (updateLHS ups a)
updateLHS ups (IAutoApp loc' f a) = IAutoApp loc' (updateLHS ups f) (updateLHS ups a)
updateLHS ups (INamedApp loc' f t a)
= INamedApp loc' (updateLHS ups f) t (updateLHS ups a)
updateLHS ups tm = tm
generateSplits : {auto m : Ref MD Metadata} ->

9
src/TTImp/Parser.idr
View File

@ -155,8 +155,10 @@ mutual
applyExpImp start end f [] = f
applyExpImp start end f (Left exp :: args)
= applyExpImp start end (IApp (MkFC fname start end) f exp) args
applyExpImp start end f (Right (n, imp) :: args)
= applyExpImp start end (IImplicitApp (MkFC fname start end) f n imp) args
applyExpImp start end f (Right (Just n, imp) :: args)
= applyExpImp start end (INamedApp (MkFC fname start end) f n imp) args
applyExpImp start end f (Right (Nothing, imp) :: args)
= applyExpImp start end (IAutoApp (MkFC fname start end) f imp) args
argExpr : FileName -> IndentInfo ->
Rule (Either RawImp (Maybe Name, RawImp))
@ -515,7 +517,8 @@ mutual
getFn : RawImp -> SourceEmptyRule Name
getFn (IVar _ n) = pure n
getFn (IApp _ f a) = getFn f
getFn (IImplicitApp _ f _ a) = getFn f
getFn (IAutoApp _ f a) = getFn f
getFn (INamedApp _ f _ a) = getFn f
getFn _ = fail "Not a function application"
clause : Nat -> FileName -> IndentInfo -> Rule (Name, ImpClause)

11
src/TTImp/PartialEval.idr
View File

@ -149,7 +149,7 @@ getSpecPats fc pename fn stk fnty args sargs pats
mkRHSargs (NBind _ x (Pi _ _ _ _) sc) app (a :: as) ((_, Dynamic) :: ds)
= do defs <- get Ctxt
sc' <- sc defs (toClosure defaultOpts [] (Erased fc False))
mkRHSargs sc' (IImplicitApp fc app (Just x) (IVar fc (UN a))) as ds
mkRHSargs sc' (INamedApp fc app x (IVar fc (UN a))) as ds
mkRHSargs (NBind _ x (Pi _ _ Explicit _) sc) app as ((_, Static tm) :: ds)
= do defs <- get Ctxt
sc' <- sc defs (toClosure defaultOpts [] (Erased fc False))
@ -159,7 +159,7 @@ getSpecPats fc pename fn stk fnty args sargs pats
= do defs <- get Ctxt
sc' <- sc defs (toClosure defaultOpts [] (Erased fc False))
tm' <- unelabNoSugar [] tm
mkRHSargs sc' (IImplicitApp fc app (Just x) tm') as ds
mkRHSargs sc' (INamedApp fc app x tm') as ds
-- Type will depend on the value here (we assume a variadic function) but
-- the argument names are still needed
mkRHSargs ty app (a :: as) ((_, Dynamic) :: ds)
@ -169,7 +169,7 @@ getSpecPats fc pename fn stk fnty args sargs pats
getRawArgs : List (Maybe Name, RawImp) -> RawImp -> List (Maybe Name, RawImp)
getRawArgs args (IApp _ f arg) = getRawArgs ((Nothing, arg) :: args) f
getRawArgs args (IImplicitApp _ f (Just n) arg)
getRawArgs args (INamedApp _ f n arg)
= getRawArgs ((Just n, arg) :: args) f
getRawArgs args tm = args
@ -177,7 +177,7 @@ getSpecPats fc pename fn stk fnty args sargs pats
reapply f [] = f
reapply f ((Nothing, arg) :: args) = reapply (IApp fc f arg) args
reapply f ((Just t, arg) :: args)
= reapply (IImplicitApp fc f (Just t) arg) args
= reapply (INamedApp fc f t arg) args
dropArgs : Name -> RawImp -> RawImp
dropArgs pename tm = reapply (IVar fc pename) (dropSpec 0 sargs (getRawArgs [] tm))
@ -301,7 +301,8 @@ mkSpecDef {vars} fc gdef pename sargs fn stk
updateApp : Name -> RawImp -> RawImp
updateApp n (IApp fc f a) = IApp fc (updateApp n f) a
updateApp n (IImplicitApp fc f m a) = IImplicitApp fc (updateApp n f) m a
updateApp n (IAutoApp fc f a) = IAutoApp fc (updateApp n f) a
updateApp n (INamedApp fc f m a) = INamedApp fc (updateApp n f) m a
updateApp n f = IVar fc n
unelabDef : (vs ** (Env Term vs, Term vs, Term vs)) ->

3
src/TTImp/ProcessData.idr
View File

@ -74,7 +74,8 @@ updateNS orig ns tm = updateNSApp tm
then IVar fc ns
else IVar fc n
updateNSApp (IApp fc f arg) = IApp fc (updateNSApp f) arg
updateNSApp (IImplicitApp fc f n arg) = IImplicitApp fc (updateNSApp f) n arg
updateNSApp (IAutoApp fc f arg) = IAutoApp fc (updateNSApp f) arg
updateNSApp (INamedApp fc f n arg) = INamedApp fc (updateNSApp f) n arg
updateNSApp t = t
checkCon : {vars : _} ->

49
src/TTImp/ProcessDef.idr
View File

@ -126,19 +126,29 @@ recoverable defs x y = pure False
export
recoverableErr : {auto c : Ref Ctxt Defs} ->
Defs -> Error -> Core Bool
recoverableErr defs (CantConvert fc env l r)
= recoverable defs !(nf defs env l)
!(nf defs env r)
recoverableErr defs (CantSolveEq fc env l r)
= recoverable defs !(nf defs env l)
!(nf defs env r)
recoverableErr defs (BadDotPattern _ _ ErasedArg _ _) = pure True
recoverableErr defs (CyclicMeta _ _ _ _) = pure True
recoverableErr defs (AllFailed errs)
= anyM (recoverableErr defs) (map snd errs)
recoverableErr defs (WhenUnifying _ _ _ _ err)
= recoverableErr defs err
recoverableErr defs _ = pure False
recoverableErr defs err@(CantConvert fc env l r)
= do log "declare.def.impossible" 5 $ show !(normaliseErr err)
recoverable defs !(nf defs env l)
!(nf defs env r)
recoverableErr defs err@(CantSolveEq fc env l r)
= do log "declare.def.impossible" 5 $ show !(normaliseErr err)
recoverable defs !(nf defs env l)
!(nf defs env r)
recoverableErr defs err@(BadDotPattern _ _ ErasedArg _ _)
= do log "declare.def.impossible" 5 $ show !(normaliseErr err)
pure True
recoverableErr defs err@(CyclicMeta _ _ _ _)
= do log "declare.def.impossible" 5 $ show !(normaliseErr err)
pure True
recoverableErr defs err@(AllFailed errs)
= do log "declare.def.impossible" 5 $ show !(normaliseErr err)
anyM (recoverableErr defs) (map snd errs)
recoverableErr defs err@(WhenUnifying _ _ _ _ err')
= do log "declare.def.impossible" 5 $ show !(normaliseErr err)
recoverableErr defs err'
recoverableErr defs err
= do log "declare.def.impossible" 5 $ show !(normaliseErr err)
pure False
-- Given a type checked LHS and its type, return the environment in which we
-- should check the RHS, the LHS and its type in that environment,
@ -802,23 +812,32 @@ processDef opts nest env fc n_in cs_in
log "declare.def.impossible" 3 $ "Checking for impossibility: " ++ show itm
autoimp <- isUnboundImplicits
setUnboundImplicits True
log "declare.def.impossible" 3 $ "unelab #1: " ++ show itm
(_, lhstm) <- bindNames False itm
log "declare.def.impossible" 3 $ "unelab #2: " ++ show lhstm
setUnboundImplicits autoimp
(lhstm, _) <- elabTerm n (InLHS mult) [] (MkNested []) []
(IBindHere fc PATTERN lhstm) Nothing
log "declare.def.impossible" 3 $ "unelab #3: " ++ show !(toFullNames lhstm)
defs <- get Ctxt
lhs <- normaliseHoles defs [] lhstm
log "declare.def.impossible" 3 $ "unelab #4: " ++ show !(toFullNames lhs)
if !(hasEmptyPat defs [] lhs)
then do put Ctxt ctxt
log "declare.def.impossible" 5 $ "Impossible due to incompatible patterns"
pure Nothing
else do empty <- clearDefs ctxt
rtm <- closeEnv empty !(nf empty [] lhs)
put Ctxt ctxt
log "declare.def.impossible" 5 $ "Possible case: compatible patterns"
pure (Just rtm))
(\err => do defs <- get Ctxt
if not !(recoverableErr defs err)
then pure Nothing
else pure (Just tm))
then do log "declare.def.impossible" 5 $ "Impossible due to unrecoverable error"
pure Nothing
else do log "declare.def.impossible" 5 $ "Possible case: recoverable error"
pure (Just tm))
where
closeEnv : Defs -> NF [] -> Core ClosedTerm
closeEnv defs (NBind _ x (PVar _ _ _ _) sc)

4
src/TTImp/ProcessRecord.idr
View File

@ -92,7 +92,7 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields
apply : RawImp -> List (Name, RawImp, PiInfo RawImp) -> RawImp
apply f [] = f
apply f ((n, arg, Explicit) :: xs) = apply (IApp (getFC f) f arg) xs
apply f ((n, arg, _ ) :: xs) = apply (IImplicitApp (getFC f) f (Just n) arg) xs
apply f ((n, arg, _ ) :: xs) = apply (INamedApp (getFC f) f n arg) xs
elabAsData : Name -> Core ()
elabAsData cname
@ -161,7 +161,7 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields
let lhs = IApp fc (IVar fc projNameNS)
(if imp == Explicit
then lhs_exp
else IImplicitApp fc lhs_exp (Just (UN fldNameStr))
else INamedApp fc lhs_exp (UN fldNameStr)
(IBindVar fc fldNameStr))
let rhs = IVar fc (UN fldNameStr)
log "declare.record.projection" 5 $ "Projection " ++ show lhs ++ " = " ++ show rhs

23
src/TTImp/Reflect.idr
View File

@ -131,12 +131,17 @@ mutual
f' <- reify defs !(evalClosure defs f)
a' <- reify defs !(evalClosure defs a)
pure (IApp fc' f' a')
(NS _ (UN "IImplicitApp"), [fc, f, m, a])
(NS _ (UN "INamedApp"), [fc, f, m, a])
=> do fc' <- reify defs !(evalClosure defs fc)
f' <- reify defs !(evalClosure defs f)
m' <- reify defs !(evalClosure defs m)
a' <- reify defs !(evalClosure defs a)
pure (IImplicitApp fc' f' m' a')
pure (INamedApp fc' f' m' a')
(NS _ (UN "IAutoApp"), [fc, f, a])
=> do fc' <- reify defs !(evalClosure defs fc)
f' <- reify defs !(evalClosure defs f)
a' <- reify defs !(evalClosure defs a)
pure (IAutoApp fc' f' a')
(NS _ (UN "IWithApp"), [fc, f, a])
=> do fc' <- reify defs !(evalClosure defs fc)
f' <- reify defs !(evalClosure defs f)
@ -476,22 +481,22 @@ mutual
ds' <- reflect fc defs lhs env ds
sc' <- reflect fc defs lhs env sc
appCon fc defs (reflectionttimp "IUpdate") [fc', ds', sc']
reflect fc defs lhs env (IInstance tfc n ds)
= do fc' <- reflect fc defs lhs env tfc
n' <- reflect fc defs lhs env n
ds' <- reflect fc defs lhs env ds
appCon fc defs (reflectionttimp "IInstance") [fc', n', ds']
reflect fc defs lhs env (IApp tfc f a)
= do fc' <- reflect fc defs lhs env tfc
f' <- reflect fc defs lhs env f
a' <- reflect fc defs lhs env a
appCon fc defs (reflectionttimp "IApp") [fc', f', a']
reflect fc defs lhs env (IImplicitApp tfc f m a)
reflect fc defs lhs env (IAutoApp tfc f a)
= do fc' <- reflect fc defs lhs env tfc
f' <- reflect fc defs lhs env f
a' <- reflect fc defs lhs env a
appCon fc defs (reflectionttimp "IAutoApp") [fc', f', a']
reflect fc defs lhs env (INamedApp tfc f m a)
= do fc' <- reflect fc defs lhs env tfc
f' <- reflect fc defs lhs env f
m' <- reflect fc defs lhs env m
a' <- reflect fc defs lhs env a
appCon fc defs (reflectionttimp "IImplicitApp") [fc', f', m', a']
appCon fc defs (reflectionttimp "INamedApp") [fc', f', m', a']
reflect fc defs lhs env (IWithApp tfc f a)
= do fc' <- reflect fc defs lhs env tfc
f' <- reflect fc defs lhs env f

63
src/TTImp/TTImp.idr
View File

@ -67,10 +67,10 @@ mutual
(args : List Name) -> RawImp -> RawImp
IUpdate : FC -> List IFieldUpdate -> RawImp -> RawImp
IInstance : FC -> Maybe Name -> List IFieldUpdate -> RawImp
IApp : FC -> RawImp -> RawImp -> RawImp
IImplicitApp : FC -> RawImp -> Maybe Name -> RawImp -> RawImp
IAutoApp : FC -> RawImp -> RawImp -> RawImp
INamedApp : FC -> RawImp -> Name -> RawImp -> RawImp
IWithApp : FC -> RawImp -> RawImp -> RawImp
ISearch : FC -> (depth : Nat) -> RawImp
@ -146,13 +146,12 @@ mutual
++ " " ++ show args ++ ") " ++ show sc ++ ")"
show (IUpdate _ flds rec)
= "(%record " ++ showSep ", " (map show flds) ++ " " ++ show rec ++ ")"
show (IInstance _ mbname flds)
= "(%recordinst " ++ fromMaybe "_" (show <$> mbname) ++ " " ++ showSep ", " (map show flds) ++ ")"
show (IApp fc f a)
= "(" ++ show f ++ " " ++ show a ++ ")"
show (IImplicitApp fc f n a)
show (INamedApp fc f n a)
= "(" ++ show f ++ " [" ++ show n ++ " = " ++ show a ++ "])"
show (IAutoApp fc f a)
= "(" ++ show f ++ " [" ++ show a ++ "])"
show (IWithApp fc f a)
= "(" ++ show f ++ " | " ++ show a ++ ")"
show (ISearch fc d)
@ -395,9 +394,12 @@ lhsInCurrentNS : {auto c : Ref Ctxt Defs} ->
lhsInCurrentNS nest (IApp loc f a)
= do f' <- lhsInCurrentNS nest f
pure (IApp loc f' a)
lhsInCurrentNS nest (IImplicitApp loc f n a)
lhsInCurrentNS nest (IAutoApp loc f a)
= do f' <- lhsInCurrentNS nest f
pure (IImplicitApp loc f' n a)
pure (IAutoApp loc f' a)
lhsInCurrentNS nest (INamedApp loc f n a)
= do f' <- lhsInCurrentNS nest f
pure (INamedApp loc f' n a)
lhsInCurrentNS nest (IWithApp loc f a)
= do f' <- lhsInCurrentNS nest f
pure (IWithApp loc f' a)
@ -421,7 +423,9 @@ findIBinds (ILam fc rig p n aty sc)
= findIBinds aty ++ findIBinds sc
findIBinds (IApp fc fn av)
= findIBinds fn ++ findIBinds av
findIBinds (IImplicitApp fc fn n av)
findIBinds (IAutoApp fc fn av)
= findIBinds fn ++ findIBinds av
findIBinds (INamedApp _ fn _ av)
= findIBinds fn ++ findIBinds av
findIBinds (IWithApp fc fn av)
= findIBinds fn ++ findIBinds av
@ -455,7 +459,9 @@ findImplicits (ILam fc rig p n aty sc)
= findImplicits aty ++ findImplicits sc
findImplicits (IApp fc fn av)
= findImplicits fn ++ findImplicits av
findImplicits (IImplicitApp fc fn n av)
findImplicits (IAutoApp _ fn av)
= findImplicits fn ++ findImplicits av
findImplicits (INamedApp _ fn _ av)
= findImplicits fn ++ findImplicits av
findImplicits (IWithApp fc fn av)
= findImplicits fn ++ findImplicits av
@ -487,9 +493,12 @@ implicitsAs defs ns tm = setAs (map Just (ns ++ map UN (findIBinds tm))) tm
setAs is (IApp loc f a)
= do f' <- setAs is f
pure $ IApp loc f' a
setAs is (IImplicitApp loc f n a)
= do f' <- setAs (n :: is) f
pure $ IImplicitApp loc f' n a
setAs is (IAutoApp loc f a)
= do f' <- setAs (Nothing :: is) f
pure $ IAutoApp loc f' a
setAs is (INamedApp loc f n a)
= do f' <- setAs (Just n :: is) f
pure $ INamedApp loc f' n a
setAs is (IWithApp loc f a)
= do f' <- setAs is f
pure $ IWithApp loc f' a
@ -530,14 +539,14 @@ implicitsAs defs ns tm = setAs (map Just (ns ++ map UN (findIBinds tm))) tm
impAs loc' [] tm = tm
impAs loc' ((UN n, AutoImplicit) :: ns) tm
= impAs loc' ns $
IImplicitApp loc' tm (Just (UN n)) (IBindVar loc' n)
INamedApp loc' tm (UN n) (IBindVar loc' n)
impAs loc' ((n, Implicit) :: ns) tm
= impAs loc' ns $
IImplicitApp loc' tm (Just n)
INamedApp loc' tm n
(IAs loc' UseLeft n (Implicit loc' True))
impAs loc' ((n, DefImplicit t) :: ns) tm
= impAs loc' ns $
IImplicitApp loc' tm (Just n)
INamedApp loc' tm n
(IAs loc' UseLeft n (Implicit loc' True))
impAs loc' (_ :: ns) tm = impAs loc' ns tm
setAs is tm = pure tm
@ -593,9 +602,9 @@ getFC (ICase x _ _ _) = x
getFC (ILocal x _ _) = x
getFC (ICaseLocal x _ _ _ _) = x
getFC (IUpdate x _ _) = x
getFC (IInstance x _ _) = x
getFC (IApp x _ _) = x
getFC (IImplicitApp x _ _ _) = x
getFC (INamedApp x _ _ _) = x
getFC (IAutoApp x _ _) = x
getFC (IWithApp x _ _) = x
getFC (ISearch x _) = x
getFC (IAlternative x _ _) = x
@ -629,7 +638,8 @@ export
getFn : RawImp -> RawImp
getFn (IApp _ f arg) = getFn f
getFn (IWithApp _ f arg) = getFn f
getFn (IImplicitApp _ f _ _) = getFn f
getFn (INamedApp _ f _ _) = getFn f
getFn (IAutoApp _ f _) = getFn f
getFn (IAs _ _ _ f) = getFn f
getFn (IMustUnify _ _ f) = getFn f
getFn f = f
@ -659,7 +669,7 @@ mutual
= do tag 6; toBuf b fc; toBuf b fs; toBuf b rec
toBuf b (IApp fc fn arg)
= do tag 7; toBuf b fc; toBuf b fn; toBuf b arg
toBuf b (IImplicitApp fc fn y arg)
toBuf b (INamedApp fc fn y arg)
= do tag 8; toBuf b fc; toBuf b fn; toBuf b y; toBuf b arg
toBuf b (IWithApp fc fn arg)
= do tag 9; toBuf b fc; toBuf b fn; toBuf b arg
@ -712,8 +722,8 @@ mutual
= do tag 29; toBuf b fc; toBuf b i
toBuf b (IWithUnambigNames fc ns rhs)
= do tag 30; toBuf b ns; toBuf b rhs
toBuf b (IInstance fc n fs)
= do tag 31; toBuf b fc; toBuf b n; toBuf b fs
toBuf b (IAutoApp fc fn arg)
= do tag 31; toBuf b fc; toBuf b fn; toBuf b arg
fromBuf b
= case !getTag of
@ -747,7 +757,7 @@ mutual
pure (IApp fc fn arg)
8 => do fc <- fromBuf b; fn <- fromBuf b
y <- fromBuf b; arg <- fromBuf b
pure (IImplicitApp fc fn y arg)
pure (INamedApp fc fn y arg)
9 => do fc <- fromBuf b; fn <- fromBuf b
arg <- fromBuf b
pure (IWithApp fc fn arg)
@ -804,10 +814,9 @@ mutual
ns <- fromBuf b
rhs <- fromBuf b
pure (IWithUnambigNames fc ns rhs)
31 => do fc <- fromBuf b
n <- fromBuf b
fs <- fromBuf b
pure (IInstance fc n fs)
31 => do fc <- fromBuf b; fn <- fromBuf b
arg <- fromBuf b
pure (IAutoApp fc fn arg)
_ => corrupt "RawImp"
export

7
src/TTImp/Unelab.idr
View File

@ -32,7 +32,8 @@ used idx _ = False
data IArg
= Exp FC RawImp
| Imp FC (Maybe Name) RawImp
| Auto FC RawImp
| Named FC Name RawImp
data UnelabMode
= Full
@ -113,7 +114,7 @@ mutual
where
getFnArgs : RawImp -> List IArg -> (RawImp, List IArg)
getFnArgs (IApp fc f arg) args = getFnArgs f (Exp fc arg :: args)
getFnArgs (IImplicitApp fc f n arg) args = getFnArgs f (Imp fc n arg :: args)
getFnArgs (INamedApp fc f n arg) args = getFnArgs f (Named fc n arg :: args)
getFnArgs tm args = (tm, args)
-- Turn a term back into an unannotated TTImp. Returns the type of the
@ -187,7 +188,7 @@ mutual
glueBack defs env sc')
NBind _ x (Pi _ rig p ty) sc
=> do sc' <- sc defs (toClosure defaultOpts env arg)
pure (IImplicitApp fc fn' (Just x) arg',
pure (INamedApp fc fn' x arg',
glueBack defs env sc')
_ => pure (IApp fc fn' arg', gErased fc)
unelabTy' umode env (As fc s p tm)

24
src/TTImp/Utils.idr
View File

@ -38,7 +38,9 @@ findBindableNames arg env used (ILam fc rig p mn aty sc)
findBindableNames True env' used sc
findBindableNames arg env used (IApp fc fn av)
= findBindableNames False env used fn ++ findBindableNames True env used av
findBindableNames arg env used (IImplicitApp fc fn n av)
findBindableNames arg env used (INamedApp fc fn n av)
= findBindableNames False env used fn ++ findBindableNames True env used av
findBindableNames arg env used (IAutoApp fc fn av)
= findBindableNames False env used fn ++ findBindableNames True env used av
findBindableNames arg env used (IWithApp fc fn av)
= findBindableNames False env used fn ++ findBindableNames True env used av
@ -80,7 +82,9 @@ findAllNames env (ILam fc rig p mn aty sc)
findAllNames env' aty ++ findAllNames env' sc
findAllNames env (IApp fc fn av)
= findAllNames env fn ++ findAllNames env av
findAllNames env (IImplicitApp fc fn n av)
findAllNames env (INamedApp fc fn n av)
= findAllNames env fn ++ findAllNames env av
findAllNames env (IAutoApp fc fn av)
= findAllNames env fn ++ findAllNames env av
findAllNames env (IWithApp fc fn av)
= findAllNames env fn ++ findAllNames env av
@ -114,7 +118,9 @@ findIBindVars (ILam fc rig p mn aty sc)
= findIBindVars aty ++ findIBindVars sc
findIBindVars (IApp fc fn av)
= findIBindVars fn ++ findIBindVars av
findIBindVars (IImplicitApp fc fn n av)
findIBindVars (INamedApp fc fn n av)
= findIBindVars fn ++ findIBindVars av
findIBindVars (IAutoApp fc fn av)
= findIBindVars fn ++ findIBindVars av
findIBindVars (IWithApp fc fn av)
= findIBindVars fn ++ findIBindVars av
@ -170,8 +176,10 @@ mutual
(substNames' bvar bound' ps y)
substNames' bvar bound ps (IApp fc fn arg)
= IApp fc (substNames' bvar bound ps fn) (substNames' bvar bound ps arg)
substNames' bvar bound ps (IImplicitApp fc fn y arg)
= IImplicitApp fc (substNames' bvar bound ps fn) y (substNames' bvar bound ps arg)
substNames' bvar bound ps (INamedApp fc fn y arg)
= INamedApp fc (substNames' bvar bound ps fn) y (substNames' bvar bound ps arg)
substNames' bvar bound ps (IAutoApp fc fn arg)
= IAutoApp fc (substNames' bvar bound ps fn) (substNames' bvar bound ps arg)
substNames' bvar bound ps (IWithApp fc fn arg)
= IWithApp fc (substNames' bvar bound ps fn) (substNames' bvar bound ps arg)
substNames' bvar bound ps (IAlternative fc y xs)
@ -267,8 +275,10 @@ mutual
(substLoc fc' y)
substLoc fc' (IApp fc fn arg)
= IApp fc' (substLoc fc' fn) (substLoc fc' arg)
substLoc fc' (IImplicitApp fc fn y arg)
= IImplicitApp fc' (substLoc fc' fn) y (substLoc fc' arg)
substLoc fc' (INamedApp fc fn y arg)
= INamedApp fc' (substLoc fc' fn) y (substLoc fc' arg)
substLoc fc' (IAutoApp fc fn arg)
= IAutoApp fc' (substLoc fc' fn) (substLoc fc' arg)
substLoc fc' (IWithApp fc fn arg)
= IWithApp fc' (substLoc fc' fn) (substLoc fc' arg)
substLoc fc' (IAlternative fc y xs)

22
src/TTImp/WithClause.idr
View File

@ -40,7 +40,9 @@ mutual
-- TODO: Lam, Let, Case, Local, Update
getMatch lhs (IApp _ f a) (IApp loc f' a')
= matchAll lhs [(f, f'), (a, a')]
getMatch lhs (IImplicitApp _ f n a) (IImplicitApp loc f' n' a')
getMatch lhs (IAutoApp _ f a) (IAutoApp loc f' a')
= matchAll lhs [(f, f'), (a, a')]
getMatch lhs (INamedApp _ f n a) (INamedApp loc f' n' a')
= if n == n'
then matchAll lhs [(f, f'), (a, a')]
else matchFail loc
@ -49,14 +51,20 @@ mutual
-- On LHS: If there's an implicit in the parent, but not the clause, add the
-- implicit to the clause. This will propagate the implicit through to the
-- body
getMatch True (IImplicitApp fc f n a) f'
getMatch True (INamedApp fc f n a) f'
= matchAll True [(f, f'), (a, a)]
getMatch True (IAutoApp fc f a) f'
= matchAll True [(f, f'), (a, a)]
-- On RHS: Rely on unification to fill in the implicit
getMatch False (IImplicitApp fc f n a) f'
getMatch False (INamedApp fc f n a) f'
= getMatch False f f
getMatch False (IAutoApp fc f a) f'
= getMatch False f f
-- Can't have an implicit in the clause if there wasn't a matching
-- implicit in the parent
getMatch lhs f (IImplicitApp fc f' n a)
getMatch lhs f (INamedApp fc f' n a)
= matchFail fc
getMatch lhs f (IAutoApp fc f' a)
= matchFail fc
-- Alternatives are okay as long as the alternatives correspond, and
-- one of them is okay
@ -197,8 +205,10 @@ withRHS fc drop wname wargnames tm toplhs
= pure $ IUpdate fc upds !(wrhs tm) -- TODO!
wrhs (IApp fc f a)
= pure $ IApp fc !(wrhs f) !(wrhs a)
wrhs (IImplicitApp fc f n a)
= pure $ IImplicitApp fc !(wrhs f) n !(wrhs a)
wrhs (IAutoApp fc f a)
= pure $ IAutoApp fc !(wrhs f) !(wrhs a)
wrhs (INamedApp fc f n a)
= pure $ INamedApp fc !(wrhs f) n !(wrhs a)
wrhs (IWithApp fc f a) = updateWith fc f [a]
wrhs (IRewrite fc rule tm) = pure $ IRewrite fc !(wrhs rule) !(wrhs tm)
wrhs (IDelayed fc r tm) = pure $ IDelayed fc r !(wrhs tm)

4
tests/Main.idr
View File

@ -42,7 +42,7 @@ idrisTests
"basic031", "basic032", "basic033", "basic034", "basic035",
"basic036", "basic037", "basic038", "basic039", "basic040",
"basic041", "basic042", "basic043", "basic044", "basic045",
"basic046", "basic047",
"basic046", "basic047", "basic048",
-- Coverage checking
"coverage001", "coverage002", "coverage003", "coverage004",
"coverage005", "coverage006", "coverage007", "coverage008",
@ -102,7 +102,7 @@ idrisTests
"real001", "real002",
-- Records, access and dependent update
"record001", "record002", "record003", "record004", "record005",
"record006", "record007",
"record006",
-- Quotation and reflection
"reflection001", "reflection002", "reflection003", "reflection004",
"reflection005", "reflection006", "reflection007", "reflection008",

132
tests/idris2/basic048/Fld.idr Normal file
View File

@ -0,0 +1,132 @@
import Data.Maybe
import Data.Nat
namespace SuperDog
public export
record SuperDog where
constructor MkDog
supername : String
age : Int
weight : Int
namespace OrdinaryDog
public export
record OrdinaryDog where
constructor MkDog
name : String
age : Int
weight : Int
record Other a where
constructor MkOther
{imp : String}
fieldA : a
fieldB : b
myDog : OrdinaryDog
myDog = MkDog { age = 4
, weight = 12
, name = "Sam" }
mySuperDog : SuperDog
mySuperDog = MkDog { age = 3
, weight = 10
, supername = "Super-Sam" }
other : ?
other = MkOther {fieldB = the Int 1, fieldA = "hi"} {imp = "Secret string"}
same : MkDog {name = "Rex", age = 2, weight = 10} = (the OrdinaryDog $ MkDog "Rex" 2 10)
same = Refl
namespace R1
public export
record R1 where
constructor MkR
field : a
namespace R2
public export
record R2 where
constructor MkR
{auto field : a}
r1 : R1
r1 = MkR {field = "string"}
r2_shouldNotTypecheck3 : ?
r2_shouldNotTypecheck3 = MkR {field = the Nat 22} -- fail, impossible to disambiguate
interface Show a => (num : Num a) => MyIface a where -- Some interface with
constructor MkIface
-- constraints
data MyData : a -> Type -- and a data declaration.
someFunc : a -> a -- Constraints are now elaborated as auto implicits (as one would expect)
giveBack : {x : a} -> MyData x -> a -- (previously as explicit arguments of the interface
-- constructor)
data MyDataImpl : a -> Type where -- implementation of MyData
MkMyData : (x : a) -> MyDataImpl x
-- implementation MyIface Int where
-- MyData = MyDataImpl
-- someFunc = id
-- giveBack (MkMyData x) = x
test0 : (x : Nat) -> Nat -> Nat -> Nat -> (y : Nat) -> x + y = y + x
test0 {} = plusCommutative {}
-- test0 _ _ _ _ _ = plusCommutative _ _
onlyName : OrdinaryDog -> String
onlyName (MkDog {name, _}) = name
mapName : (String -> String) -> OrdinaryDog -> OrdinaryDog
mapName f = {name $= f}
setName : String -> OrdinaryDog -> OrdinaryDog
setName name' = {name := name'}
setNameOld : String -> OrdinaryDog -> OrdinaryDog
setNameOld name' = record {name = name'}
%hint
instanceMyIfaceInt : MyIface Integer -- this def, roughly speaking, is the 'same thing' as the above implementation
-- Show Int, Num Int are auto implicits vvv
instanceMyIfaceInt = MkIface { MyData = MyDataImpl
, someFunc = id
, giveBack = \(MkMyData x) => x} {num = %search} -- auto implicit names are preserved
instanceOk : giveBack (MkMyData 22) = 22
instanceOk = Refl
interface Show' a where -- can be used in types
constructor MkShow'
show' : a -> String
Show' String where
show' = id
%hint
showMaybe' : Show' a => Show' (Maybe a)
showMaybe' = MkShow' { show' = fromMaybe "Nothing" . (("Just " ++ ) . show' <$>) }
showMaybe'Ok : show' (Just "nice") = "Just nice"
showMaybe'Ok = Refl
record Auto a where
constructor MkAuto
{auto aut : a}
testAuto : Auto String
testAuto = MkAuto @{"works"}
record Implicit a where
constructor MkImplicit
{imp : a}
testImplicit : Implicit String
testImplicit = MkImplicit {imp = "NotOk"}

15
tests/idris2/basic048/expected Normal file
View File

@ -0,0 +1,15 @@
1/1: Building Fld (Fld.idr)
Error: While processing right hand side of r2_shouldNotTypecheck3. Ambiguous elaboration. Possible results:
Main.R2.MkR
Main.R1.MkR Type
Fld.idr:61:26--61:29
|
61 | r2_shouldNotTypecheck3 = MkR {field = the Nat 22} -- fail, impossible to disambiguate
| ^^^
Main> Main.myDog : OrdinaryDog
Main> Main.mySuperDog : SuperDog
Main> Main.other : Other String
Main> 1 hole: Main.r2_shouldNotTypecheck3
Main> Bye for now!

5
tests/idris2/basic048/input Normal file
View File

@ -0,0 +1,5 @@
:t myDog
:t mySuperDog
:t other
:m
:q

0
tests/idris2/record007/run → tests/idris2/basic048/run
View File

165
tests/idris2/record006/Fld.idr
View File

@ -1,161 +1,6 @@
module Fld
record Is3 (n : Nat) where
constructor MkThree
{auto prf : n === 3}
import Data.Maybe
-- For now I kept this syntax:
-- record < (data) Constructor or _ > { <field1> = <expr1>, <field2> = <expr2>, ..., <fieldN> = <exprN> }
-- What would be a reason to have named constructors anyway, if we were to instantiate records by their
-- type constructors ?
-- Also it turned out that specifying type constructors instead of data constructors
-- does not simplify or provide any other benifit in internal implementation.
namespace SuperDog
public export
record SuperDog where
constructor MkDog
supername : String
age : Int
weight : Int
namespace OrdinaryDog
public export
record OrdinaryDog where
constructor MkDog
name : String
age : Int
weight : Int
record Other a where
constructor MkOther
{imp : String}
fieldA : a
fieldB : b
myDog_shouldNotTypecheck0 : record MkDog {name = "Sam"} -- Not all fields are covered
myDog_shouldNotTypecheck1 : record MkDog {age = 3, name1 = "Sam"} -- No constructor with name `MkDog`
-- has field `name1`
myDog_shouldNotTypecheck2 : record MkDog
{ age = 4
, age = 2
, weight = 12
, name = "Sam" } -- Duplicate names
myDog : ?
myDog = record MkDog { age = 4
, weight = 12
, name = "Sam" } --Disambiguation by unique fields
mySuperDog : ?
mySuperDog = record MkDog { age = 3
, weight = 10
, supername = "Super-Sam" } --Disambiguation by unique fields
other : ? -- Elaborates as (MkOther (fromString "hi") (the Int 1) {imp = fromString "Secret string"})
other = record MkOther {fieldB = the Int 1, fieldA = "hi"} {imp = "Secret string"}
same : record MkDog {name = "Rex", age = 2, weight = 10} = MkDog "Rex" 2 10
same = Refl
record Unit where
constructor MkUnit
unit : Fld.Unit
unit = record _ {} -- infer the constructor
namespace R1
public export
record R1 where
constructor MkR
field : a
namespace R2
public export
record R2 where
constructor MkR
field : a
r1 : R1
r1 = record _ {field = "string"} -- type-driven disambiguation
r2_shouldNotTypecheck3 : ?
r2_shouldNotTypecheck3 = record MkR {field = the Nat 22} -- fail, impossible to disambiguate
r3_shouldNotTypecheck4 : ?
r3_shouldNotTypecheck4 = record _ {field = the Nat 22} -- fail, impossible to disambiguate
r4 : ?
r4 = the R2 $ record _ {field = the Nat 22} -- ok
sillyShow : String -> String -- shows string as is, constructs an instance of Show String
sillyShow str = show @{ record _ {show = id, showPrec = const id} } str -- TODO default implementations not yet supported
sillyShowOk : sillyShow "x" = "x"
sillyShowOk = Refl
interface Show a => (num : Num a) => MyIface a where -- Some interface with
--constructor MkMyIface, not needed :) -- constraints
data MyData : a -> Type -- and a data declaration.
someFunc : a -> a -- Constraints are now elaborated as auto implicits (as one would expect)
giveBack : {x : a} -> MyData x -> a -- (previously as explicit arguments of the interface
-- constructor)
data MyDataImpl : a -> Type where -- implementation of MyData
MkMyData : (x : a) -> MyDataImpl x
-- implementation MyIface Int where
-- MyData = MyDataImpl
-- someFunc = id
-- giveBack (MkMyData x) = x
%hint
instanceMyIfaceInt : MyIface Integer -- this def, roughly speaking, is the 'same thing' as the above implementation
-- Show Int, Num Int are auto implicits vvv
instanceMyIfaceInt = record _ {MyData = MyDataImpl, someFunc = id, giveBack = \(MkMyData x) => x} {num = %search} -- auto implicit names are preserved
instanceOk : giveBack (MkMyData 22) = 22
instanceOk = Refl
interface Show' a where -- can be used in types
show' : a -> String
Show' String where
show' = id
%hint
showMaybe' : Show' a => Show' (Maybe a)
showMaybe' = record _ { show' = fromMaybe "Nothing" . (("Just " ++ ) . show' <$>) }
showMaybe'Ok : show' (Just "nice") = "Just nice"
showMaybe'Ok = Refl
record Auto a where
{auto aut : a}
testAuto : Auto String
testAuto = record _ {} @{"works"}
record Implicit a where
{imp : a}
testImplicit : Implicit String
testImplicit = record _ {imp = "NotOk"} --TODO imp is an implicit argument
-- why suddenly does it become explicit ?
-- This is current idris behaviour
-- FIX IT !
-- What about different syntax for this: "new {...} = record _ {...}"
-- "new _ {...} = record _ {...}"
-- "new x {...} = record x {...}" ?
-- Saves a little bit of typing and allows omitting the "_" .
-- Also "new" is quite frequently used in programming languages
-- with the meaning "make an instance of something"
-- We can't have "record {...} = record _ {...}" as it intersects with record update syntax
three : Is3 3
three = MkThree

46
tests/idris2/record006/expected
View File

@ -1,45 +1,3 @@
1/1: Building Fld (Fld.idr)
Error: While processing type of myDog_shouldNotTypecheck0. Field not covered age.
Fld.idr:36:29--36:56
|
36 | myDog_shouldNotTypecheck0 : record MkDog {name = "Sam"} -- Not all fields are covered
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: While processing type of myDog_shouldNotTypecheck1. No constructor satisfies provided fields.
Fld.idr:38:29--38:66
|
38 | myDog_shouldNotTypecheck1 : record MkDog {age = 3, name1 = "Sam"} -- No constructor with name `MkDog`
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: While processing type of myDog_shouldNotTypecheck2. Duplicate fields.
Fld.idr:40:29--44:47
40 | myDog_shouldNotTypecheck2 : record MkDog
41 | { age = 4
42 | , age = 2
43 | , weight = 12
44 | , name = "Sam" } -- Duplicate names
Error: While processing right hand side of r2_shouldNotTypecheck3. Ambiguous elaboration. Possible results:
Fld.R2.MkR ?field
Fld.R1.MkR ?field
Fld.idr:86:26--86:57
|
86 | r2_shouldNotTypecheck3 = record MkR {field = the Nat 22} -- fail, impossible to disambiguate
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: While processing right hand side of r3_shouldNotTypecheck4. Can't infer type for this record.
Fld.idr:89:26--89:55
|
89 | r3_shouldNotTypecheck4 = record _ {field = the Nat 22} -- fail, impossible to disambiguate
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Fld> Fld.myDog : OrdinaryDog
Fld> Fld.mySuperDog : SuperDog
Fld> Fld.other : Other String
Fld> 2 holes: Fld.r2_shouldNotTypecheck3, Fld.r3_shouldNotTypecheck4
Fld> Bye for now!
Main> Main> MkThree {n = 3} {prf = Refl {a = Nat} {x = 3}}
Main> Bye for now!

6
tests/idris2/record006/input
View File

@ -1,5 +1,3 @@
:t myDog
:t mySuperDog
:t other
:m
:set showimplicits
three
:q

6
tests/idris2/record007/Fld.idr
View File

@ -1,6 +0,0 @@
record Is3 (n : Nat) where
constructor MkThree
{auto prf : n === 3}
three : Is3 3
three = MkThree

3
tests/idris2/record007/expected
View File

@ -1,3 +0,0 @@
1/1: Building Fld (Fld.idr)
Main> Main> MkThree {n = 3} {prf = Refl {a = Nat} {x = 3}}
Main> Bye for now!

3
tests/idris2/record007/input
View File

@ -1,3 +0,0 @@
:set showimplicits
three
:q

4
tests/ttimp/basic006/expected
View File

@ -1,6 +1,6 @@
Processing as TTImp
Written TTC
Yaffle> ((Main.Just [Just a = ((Main.Vect.Vect (Main.S Main.Z)) Integer)]) ((((Main.Vect.Cons [Just k = Main.Z]) [Just a = Integer]) 1) (Main.Vect.Nil [Just a = Integer])))
Yaffle> ((Main.MkInfer [Just a = (Main.List.List Integer)]) (((Main.List.Cons [Just a = Integer]) 1) (Main.List.Nil [Just a = Integer])))
Yaffle> ((Main.Just [a = ((Main.Vect.Vect (Main.S Main.Z)) Integer)]) ((((Main.Vect.Cons [k = Main.Z]) [a = Integer]) 1) (Main.Vect.Nil [a = Integer])))
Yaffle> ((Main.MkInfer [a = (Main.List.List Integer)]) (((Main.List.Cons [a = Integer]) 1) (Main.List.Nil [a = Integer])))
Yaffle> (repl):1:9--1:12:Ambiguous elaboration [($resolved207 ?Main.{a:62}_[]), ($resolved187 ?Main.{a:62}_[])]
Yaffle> Bye for now!

4
tests/ttimp/coverage001/expected
View File

@ -6,6 +6,6 @@ Vect2.yaff:25:1--26:1:{pat 0 {b:27} : Type} => {pat 0 {a:26} : Type} => ($resolv
Yaffle> Bye for now!
Processing as TTImp
Vect3.yaff:25:1--26:1:Not a valid impossible pattern:
Vect3.yaff:25:9--25:11:When unifying: $resolved184 and ($resolved192 ?Main.{n:21}_[] ?Main.{b:19}_[])
Vect3.yaff:25:9--25:11:Type mismatch: $resolved184 and ($resolved192 ?Main.{n:21}_[] ?Main.{b:19}_[])
Vect3.yaff:25:9--25:11:When unifying: Main.Nat and (Main.Vect ?Main.{n:21}_[] ?Main.{b:19}_[])
Vect3.yaff:25:9--25:11:Type mismatch: Main.Nat and (Main.Vect ?Main.{n:21}_[] ?Main.{b:19}_[])
Yaffle> Bye for now!

4
tests/ttimp/eta001/expected
View File

@ -1,5 +1,5 @@
Processing as TTImp
Written TTC
Yaffle> ((Main.Refl [Just {b:10} = Main.Nat]) [Just x = (Main.S (Main.S (Main.S (Main.S Main.Z))))])
Yaffle> Main.etaGood1 : ((((Main.Eq [Just b = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) [Just a = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) Main.MkTest) (%lam RigW Explicit (Just x) Integer (%lam RigW Explicit (Just y) Integer ((Main.MkTest x) y))))
Yaffle> ((Main.Refl [{b:10} = Main.Nat]) [x = (Main.S (Main.S (Main.S (Main.S Main.Z))))])
Yaffle> Main.etaGood1 : ((((Main.Eq [b = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) [a = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) Main.MkTest) (%lam RigW Explicit (Just x) Integer (%lam RigW Explicit (Just y) Integer ((Main.MkTest x) y))))
Yaffle> Bye for now!

2
tests/ttimp/eta002/expected
View File

@ -1,5 +1,5 @@
Processing as TTImp
Eta.yaff:16:1--17:1:When elaborating right hand side of Main.etaBad:
Eta.yaff:16:10--17:1:When unifying: ($resolved186 ?Main.{b:18}_[] ?Main.{b:18}_[] \(x : Char) => \(y : ?Main.{_:15}_[x[0]]) => ($resolved196 ?Main.{_:16}_[x[1], y[0]] ?Main.{_:17}_[x[1], y[0]]) \(x : Char) => \(y : ?Main.{_:15}_[x[0]]) => ($resolved196 ?Main.{_:16}_[x[1], y[0]] ?Main.{_:17}_[x[1], y[0]])) and ($resolved186 (x : Char) -> (y : ?Main.{_:15}_[x[0]]) -> $resolved195)) ({arg:11} : Integer) -> ({arg:12} : Integer) -> $resolved195)) $resolved196 \(x : Char) => \(y : ?Main.{_:15}_[x[0]]) => ($resolved196 ?Main.{_:16}_[x[1], y[0]] ?Main.{_:17}_[x[1], y[0]]))
Eta.yaff:16:10--17:1:When unifying: (Main.Eq ?Main.{b:18}_[] ?Main.{b:18}_[] \(x : Char) => \(y : ?Main.{_:15}_[x[0]]) => (Main.MkTest ?Main.{_:16}_[x[1], y[0]] ?Main.{_:17}_[x[1], y[0]]) \(x : Char) => \(y : ?Main.{_:15}_[x[0]]) => (Main.MkTest ?Main.{_:16}_[x[1], y[0]] ?Main.{_:17}_[x[1], y[0]])) and (Main.Eq (x : Char) -> (y : ?Main.{_:15}_[x[0]]) -> Main.Test)) ({arg:11} : Integer) -> ({arg:12} : Integer) -> Main.Test)) Main.MkTest \(x : Char) => \(y : ?Main.{_:15}_[x[0]]) => (Main.MkTest ?Main.{_:16}_[x[1], y[0]] ?Main.{_:17}_[x[1], y[0]]))
Eta.yaff:16:10--17:1:Type mismatch: Char and Integer
Yaffle> Bye for now!

18
tests/ttimp/lazy001/expected
View File

@ -1,18 +1,18 @@
Processing as TTImp
Written TTC
Yaffle> (((Main.Stream.Cons [Just a = Integer]) 1) (%delay Main.ones))
Yaffle> (((Main.Cons [Just a = Integer]) 1) (((Main.Cons [Just a = Integer]) 1) (((Main.Cons [Just a = Integer]) 1) (Main.Nil [Just a = Integer]))))
Yaffle> (((Main.Cons [Just a = Integer]) 2) (((Main.Cons [Just a = Integer]) 4) (((Main.Cons [Just a = Integer]) 6) (Main.Nil [Just a = Integer]))))
Yaffle> (((Main.Stream.Cons [a = Integer]) 1) (%delay Main.ones))
Yaffle> (((Main.Cons [a = Integer]) 1) (((Main.Cons [a = Integer]) 1) (((Main.Cons [a = Integer]) 1) (Main.Nil [a = Integer]))))
Yaffle> (((Main.Cons [a = Integer]) 2) (((Main.Cons [a = Integer]) 4) (((Main.Cons [a = Integer]) 6) (Main.Nil [a = Integer]))))
Yaffle> Bye for now!
Processing as TTImp
Written TTC
Yaffle> (((Main.Stream.Cons [Just a = Integer]) 1) (%delay Main.ones))
Yaffle> (((Main.Cons [Just a = Integer]) 1) (((Main.Cons [Just a = Integer]) 1) (((Main.Cons [Just a = Integer]) 1) (Main.Nil [Just a = Integer]))))
Yaffle> (((Main.Cons [Just a = Integer]) 2) (((Main.Cons [Just a = Integer]) 4) (((Main.Cons [Just a = Integer]) 6) (Main.Nil [Just a = Integer]))))
Yaffle> (((Main.Stream.Cons [a = Integer]) 1) (%delay Main.ones))
Yaffle> (((Main.Cons [a = Integer]) 1) (((Main.Cons [a = Integer]) 1) (((Main.Cons [a = Integer]) 1) (Main.Nil [a = Integer]))))
Yaffle> (((Main.Cons [a = Integer]) 2) (((Main.Cons [a = Integer]) 4) (((Main.Cons [a = Integer]) 6) (Main.Nil [a = Integer]))))
Yaffle> Bye for now!
Processing as TTC
Read TTC
Yaffle> (((Main.Stream.Cons [Just a = Integer]) 1) (%delay Main.ones))
Yaffle> (((Main.Cons [Just a = Integer]) 1) (((Main.Cons [Just a = Integer]) 1) (((Main.Cons [Just a = Integer]) 1) (Main.Nil [Just a = Integer]))))
Yaffle> (((Main.Cons [Just a = Integer]) 2) (((Main.Cons [Just a = Integer]) 4) (((Main.Cons [Just a = Integer]) 6) (Main.Nil [Just a = Integer]))))
Yaffle> (((Main.Stream.Cons [a = Integer]) 1) (%delay Main.ones))
Yaffle> (((Main.Cons [a = Integer]) 1) (((Main.Cons [a = Integer]) 1) (((Main.Cons [a = Integer]) 1) (Main.Nil [a = Integer]))))
Yaffle> (((Main.Cons [a = Integer]) 2) (((Main.Cons [a = Integer]) 4) (((Main.Cons [a = Integer]) 6) (Main.Nil [a = Integer]))))
Yaffle> Bye for now!

2
tests/ttimp/nest002/expected
View File

@ -1,7 +1,7 @@
Processing as TTImp
Written TTC
Yaffle> (Main.S (Main.S (Main.S (Main.S (Main.S Main.Z)))))
Yaffle> ((((Main.Cons [Just k = (Main.S Main.Z)]) [Just a = Integer]) 1) ((((Main.Cons [Just k = Main.Z]) [Just a = Integer]) 2) (Main.Nil [Just a = Integer])))
Yaffle> ((((Main.Cons [k = (Main.S Main.Z)]) [a = Integer]) 1) ((((Main.Cons [k = Main.Z]) [a = Integer]) 2) (Main.Nil [a = Integer])))
Yaffle> (Main.S (Main.S (Main.S Main.Z)))
Yaffle> (Main.S (Main.S (Main.S Main.Z)))
Yaffle> Bye for now!

4
tests/ttimp/record001/expected
View File

@ -1,12 +1,12 @@
Processing as TTImp
Written TTC
Yaffle> (Main.S (Main.S (Main.S Main.Z)))
Yaffle> ((((Main.Cons [Just k = (Main.S (Main.S Main.Z))]) [Just a = Integer]) 1) ((((Main.Cons [Just k = (Main.S Main.Z)]) [Just a = Integer]) 2) ((((Main.Cons [Just k = Main.Z]) [Just a = Integer]) 3) (Main.Nil [Just a = Integer]))))
Yaffle> ((((Main.Cons [k = (Main.S (Main.S Main.Z))]) [a = Integer]) 1) ((((Main.Cons [k = (Main.S Main.Z)]) [a = Integer]) 2) ((((Main.Cons [k = Main.Z]) [a = Integer]) 3) (Main.Nil [a = Integer]))))
Yaffle> (Main.S (Main.S (Main.S Main.Z)))
Yaffle> Bye for now!
Processing as TTC
Read TTC
Yaffle> (Main.S (Main.S (Main.S Main.Z)))
Yaffle> ((((Main.Cons [Just k = (Main.S (Main.S Main.Z))]) [Just a = Integer]) 1) ((((Main.Cons [Just k = (Main.S Main.Z)]) [Just a = Integer]) 2) ((((Main.Cons [Just k = Main.Z]) [Just a = Integer]) 3) (Main.Nil [Just a = Integer]))))
Yaffle> ((((Main.Cons [k = (Main.S (Main.S Main.Z))]) [a = Integer]) 1) ((((Main.Cons [k = (Main.S Main.Z)]) [a = Integer]) 2) ((((Main.Cons [k = Main.Z]) [a = Integer]) 3) (Main.Nil [a = Integer]))))
Yaffle> (Main.S (Main.S (Main.S Main.Z)))
Yaffle> Bye for now!

4
tests/ttimp/record002/expected
View File

@ -1,7 +1,7 @@
Processing as TTImp
Written TTC
Yaffle> ((((Main.MkPerson "Fred") 1337) 10) ((Main.MkStats 11) 10))
Yaffle> ((((Main.MkMyDPair [Just a = Main.Nat]) [Just p = (%lam RigW Explicit (Just n) Main.Nat ((Main.Vect n) Integer))]) (Main.S (Main.S (Main.S (Main.S Main.Z))))) ((((Main.Cons [Just k = (Main.S (Main.S (Main.S Main.Z)))]) [Just a = Integer]) 10) ((((Main.Cons [Just k = (Main.S (Main.S Main.Z))]) [Just a = Integer]) 1) ((((Main.Cons [Just k = (Main.S Main.Z)]) [Just a = Integer]) 2) ((((Main.Cons [Just k = Main.Z]) [Just a = Integer]) 3) (Main.Nil [Just a = Integer]))))))
Yaffle> ((((Main.MkMyDPair [Just a = Main.Nat]) [Just p = (%lam RigW Explicit (Just n) Main.Nat ((Main.Vect n) Integer))]) (Main.S (Main.S (Main.S (Main.S Main.Z))))) ((((Main.Cons [Just k = (Main.S (Main.S (Main.S Main.Z)))]) [Just a = Integer]) 10) ((((Main.Cons [Just k = (Main.S (Main.S Main.Z))]) [Just a = Integer]) 1) ((((Main.Cons [Just k = (Main.S Main.Z)]) [Just a = Integer]) 2) ((((Main.Cons [Just k = Main.Z]) [Just a = Integer]) 3) (Main.Nil [Just a = Integer]))))))
Yaffle> ((((Main.MkMyDPair [a = Main.Nat]) [p = (%lam RigW Explicit (Just n) Main.Nat ((Main.Vect n) Integer))]) (Main.S (Main.S (Main.S (Main.S Main.Z))))) ((((Main.Cons [k = (Main.S (Main.S (Main.S Main.Z)))]) [a = Integer]) 10) ((((Main.Cons [k = (Main.S (Main.S Main.Z))]) [a = Integer]) 1) ((((Main.Cons [k = (Main.S Main.Z)]) [a = Integer]) 2) ((((Main.Cons [k = Main.Z]) [a = Integer]) 3) (Main.Nil [a = Integer]))))))
Yaffle> ((((Main.MkMyDPair [a = Main.Nat]) [p = (%lam RigW Explicit (Just n) Main.Nat ((Main.Vect n) Integer))]) (Main.S (Main.S (Main.S (Main.S Main.Z))))) ((((Main.Cons [k = (Main.S (Main.S (Main.S Main.Z)))]) [a = Integer]) 10) ((((Main.Cons [k = (Main.S (Main.S Main.Z))]) [a = Integer]) 1) ((((Main.Cons [k = (Main.S Main.Z)]) [a = Integer]) 2) ((((Main.Cons [k = Main.Z]) [a = Integer]) 3) (Main.Nil [a = Integer]))))))
Yaffle> ((((Main.MkPerson "Fred") 1337) 10) ((Main.MkStats 10) 94))
Yaffle> Bye for now!