idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-01 09:49:24 +03:00
Code Issues Projects Releases Wiki Activity

Implement #553 V2

Browse Source
This commit is contained in:
russoul 2020-08-31 14:04:57 +03:00
parent 406f9f5099
commit cb1a5f663c
9 changed files with 214 additions and 76 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -211,9 +211,8 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
defs <- get Ctxt
let fldTys = getFieldArgs !(normaliseHoles defs [] conty)
log "elab.implementation" 5 $ "Field types " ++ show fldTys
let irhs = apply (IVar fc con)
(map (const (ISearch fc 500)) (parents cdata)
++ map (mkMethField methImps fldTys) fns)
let irhs = apply (autoImpsApply (IVar fc con) $ map (const (ISearch fc 500)) (parents cdata))
(map (mkMethField methImps fldTys) fns)
let impFn = IDef fc impName [PatClause fc ilhs irhs]
log "elab.implementation" 5 $ "Implementation record: " ++ show impFn
@ -268,6 +267,10 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
impsApply fn ((n, arg) :: ns)
= impsApply (IImplicitApp fc fn (Just n) arg) ns
autoImpsApply : RawImp -> List RawImp -> RawImp
autoImpsApply f [] = f
autoImpsApply f (x :: xs) = autoImpsApply (IImplicitApp (getFC f) f Nothing x) xs
mkLam : List (Name, RigCount, PiInfo RawImp) -> RawImp -> RawImp
mkLam [] tm = tm
mkLam ((x, c, p) :: xs) tm

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

@ -46,7 +46,7 @@ mkIfaceData {vars} fc vis env constraints n conName ps dets meths
else [NoHints, UniqueSearch, SearchBy dets]
retty = apply (IVar fc n) (map (IVar fc) (map fst ps))
conty = mkTy Implicit (map jname ps) $
mkTy Explicit (map bhere constraints ++ map bname meths) retty
mkTy AutoImplicit (map bhere constraints) (mkTy Explicit (map bname meths) retty)
con = MkImpTy fc conName !(bindTypeNames [] (map fst ps ++ map fst meths ++ vars) conty) in
pure $ IData fc vis (MkImpData fc n
!(bindTypeNames [] (map fst ps ++ map fst meths ++ vars)
@ -135,8 +135,7 @@ getMethToplevel {vars} env vis iname cname constraints allmeths params
else [Inline])
(MkImpTy fc cn ty_imp)
let conapp = apply (IVar fc cname)
(map (const (Implicit fc True)) constraints ++
map (IBindVar fc) (map bindName allmeths))
(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)
@ -178,6 +177,11 @@ getMethToplevel {vars} env vis iname cname constraints allmeths params
methName : Name -> Name
methName n = UN (bindName n)
impsBind : RawImp -> Nat -> RawImp
impsBind fn Z = fn
impsBind fn (S k)
= impsBind (IImplicitApp fc fn Nothing (Implicit fc True)) k
-- Get the function for chasing a constraint. This is one of the
-- arguments to the record, appearing before the method arguments.
getConstraintHint : {vars : _} ->
@ -196,9 +200,8 @@ getConstraintHint {vars} fc env vis iname cname constraints meths params (cn, co
(UN ("__" ++ show iname ++ "_" ++ show con))
let tydecl = IClaim fc top vis [Inline, Hint False]
(MkImpTy fc hintname ty_imp)
let conapp = apply (IVar fc cname)
(map (IBindVar fc) (map bindName constraints) ++
map (const (Implicit fc True)) meths)
let conapp = apply (impsBind (IVar fc cname) (map bindName constraints))
(map (const (Implicit fc True)) meths)
let fnclause = PatClause fc (IApp fc (IVar fc hintname) conapp)
(IVar fc (constName cn))
let fndef = IDef fc hintname [fnclause]
@ -212,6 +215,12 @@ getConstraintHint {vars} fc env vis iname cname constraints meths params (cn, co
constName : Name -> Name
constName n = UN (bindName n)
impsBind : RawImp -> List String -> RawImp
impsBind fn [] = fn
impsBind fn (n :: ns)
= impsBind (IImplicitApp fc fn Nothing (IBindVar fc n)) ns
getSig : ImpDecl -> Maybe (FC, RigCount, List FnOpt, Name, (Bool, RawImp))
getSig (IClaim _ c _ opts (MkImpTy fc n ty))
= Just (fc, c, opts, n, (False, namePis 0 ty))

8
src/Idris/Parser.idr
View File

@ -650,14 +650,14 @@ mutual
recordInstance : FileName -> IndentInfo -> Rule PTerm
recordInstance fname indents
= do b <- bounds (do keyword "record"
n <- name
mbname <- (Just <$> name) <|> (const Nothing <$> symbol "_")
symbol "{"
commit
fs <- sepBy (symbol ",") (field fname indents False)
symbol "}"
pure (n, fs))
(name, fs) <- pure b.val
pure (PInstance (boundToFC fname b) name fs)
pure (mbname, fs))
(mbname, fs) <- pure b.val
pure (PInstance (boundToFC fname b) mbname fs)
rewrite_ : FileName -> IndentInfo -> Rule PTerm
rewrite_ fname indents

5
src/Idris/Syntax.idr
View File

@ -13,6 +13,7 @@ import TTImp.TTImp
import Data.ANameMap
import Data.List
import Data.Maybe
import Data.NameMap
import Data.StringMap
import Text.PrettyPrint.Prettyprinter
@ -46,7 +47,7 @@ mutual
PCase : FC -> PTerm -> List PClause -> PTerm
PLocal : FC -> List PDecl -> (scope : PTerm) -> PTerm
PUpdate : FC -> List PFieldUpdate -> PTerm
PInstance : FC -> Name -> 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
@ -537,7 +538,7 @@ mutual
showPrec d (PUpdate _ fs)
= "record { " ++ showSep ", " (map showUpdate fs) ++ " }"
showPrec d (PInstance _ n fs)
= "record " ++ showPrec d n ++ " { " ++ showSep ", " (map showUpdate 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)

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

@ -631,20 +631,23 @@ checkApp : {vars : _} ->
FC -> (fn : RawImp) ->
(expargs : List RawImp) ->
(impargs : List (Maybe Name, RawImp)) ->
(mkFullyApplied : RawImp -> RawImp) ->
Maybe (Glued vars) ->
Core (Term vars, Glued vars)
checkApp rig elabinfo nest env fc (IApp fc' fn arg) expargs impargs exp
= checkApp rig elabinfo nest env fc' fn (arg :: expargs) impargs exp
checkApp rig elabinfo nest env fc (IImplicitApp fc' fn nm arg) expargs impargs exp
= checkApp rig elabinfo nest env fc' fn expargs ((nm, arg) :: impargs) exp
checkApp rig elabinfo nest env fc (IInstance fc' name fs) expargs impargs exp
= do elabs <- elabInstance env fc' name fs
let namedElabs = map (\(name, args) =>
( Just name
, checkApp rig elabinfo nest env fc (apply (IVar fc name) args) expargs impargs exp))
elabs
exactlyOne fc env namedElabs
checkApp rig elabinfo nest env fc (IVar fc' n) expargs impargs exp
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
= do (ntm, arglen, nty_in) <- getVarType rig nest env fc n
nty <- getNF nty_in
let prims = mapMaybe id
@ -711,7 +714,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 impargs _ 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

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

@ -236,32 +236,58 @@ checkUpdate rig elabinfo nest env fc upds rec expected
check rig elabinfo nest env rcase expected
export
elabInstance : {vars : _} ->
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 -> Name -> List IFieldUpdate ->
Core (List (Name, List RawImp)) -- one or more possible elaborations
elabInstance env fc providedName fs
= 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
for fullnames \(fullname, allfields) => do
seqexp <- flip traverse allfields \x => lookupOrElse x fs' (throw (NotCoveredField fc x))
pure $ (fullname, seqexp)
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 notInfered 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)
notInferedMsg : String
notInferedMsg = "Can't infer the type of the record." --TODO make a proper error
notInfered : Error -> Bool
notInfered (GenericMsg _ msg) = msg == notInferedMsg
notInfered _ = False
errorConstructorNotFound : Error
errorConstructorNotFound = GenericMsg fc "No constructor satisfies provided fields."
@ -319,8 +345,17 @@ elabInstance env fc providedName fs
[] => Left errorConstructorNotFound
oneOrMoreNames => Right (map snd oneOrMoreNames)
isConName : Defs -> Name -> Core Bool
isConName defs name
= case !(lookupDefExact name (gamma defs)) of
Just (DCon _ _ _) => pure True
_ => pure False
-- taken from Desugar.idr, better find one common place for this def ?
mkConName : (tConName : Name) -> Name
mkConName (NS ns (UN n)) = NS ns (DN n (MN ("__mk" ++ n) 0))
mkConName n = DN (show n) (MN ("__mk" ++ show n) 0)
elabCon : (ty : Glued vars) -> FC -> Core (Term vars, Glued vars) -- TODO seek for constructor if there is one
elabCon gty fullLoc
= do defs <- get Ctxt
tynf <- getNF gty
let (Just tconName) = getRecordType env tynf
| _ => throw (GenericMsg fullLoc notInferedMsg)
(Just [conName]) <- findConNames defs tconName
| mbnames => throw (InternalError (show mbnames))
check rig elabinfo nest env (mkFull (IInstance fc (Just conName) fs)) expected

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

@ -121,11 +121,11 @@ checkTerm : {vars : _} ->
RigCount -> ElabInfo ->
NestedNames vars -> Env Term vars -> RawImp -> Maybe (Glued vars) ->
Core (Term vars, Glued vars)
checkTerm rig elabinfo nest env (IVar fc n) exp
checkTerm rig elabinfo nest env full@(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) [] [] exp
checkApp rig elabinfo nest env fc full [] [] id 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) [] [] exp
checkTerm rig elabinfo nest env (IApp fc fn arg) exp
= checkApp rig elabinfo nest env fc fn [arg] [] exp
checkTerm rig elabinfo nest env full@(IInstance fc n fs) exp
= checkApp rig elabinfo nest env fc full [] [] id exp
checkTerm rig elabinfo nest env full@(IApp fc fn arg) exp
= checkApp rig elabinfo nest env fc fn [arg] [] (\fn => IApp 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)] exp
checkTerm rig elabinfo nest env full@(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 (ISearch fc depth) (Just gexpty)
= do est <- get EST
nm <- genName "search"

7
src/TTImp/TTImp.idr
View File

@ -10,6 +10,7 @@ import Core.TTC
import Core.Value
import Data.List
import Data.Maybe
%default covering
@ -65,7 +66,7 @@ mutual
(args : List Name) -> RawImp -> RawImp
IUpdate : FC -> List IFieldUpdate -> RawImp -> RawImp
IInstance : FC -> Name -> List IFieldUpdate -> RawImp
IInstance : FC -> Maybe Name -> List IFieldUpdate -> RawImp
IApp : FC -> RawImp -> RawImp -> RawImp
IImplicitApp : FC -> RawImp -> Maybe Name -> RawImp -> RawImp
@ -144,8 +145,8 @@ mutual
++ " " ++ show args ++ ") " ++ show sc ++ ")"
show (IUpdate _ flds rec)
= "(%record " ++ showSep ", " (map show flds) ++ " " ++ show rec ++ ")"
show (IInstance _ n flds)
= "(%recordinst " ++ show n ++ " " ++ showSep ", " (map show flds) ++ ")"
show (IInstance _ mbname flds)
= "(%recordinst " ++ fromMaybe "_" (show <$> mbname) ++ " " ++ showSep ", " (map show flds) ++ ")"
show (IApp fc f a)
= "(" ++ show f ++ " " ++ show a ++ ")"

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

@ -1,5 +1,16 @@
module Fld
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 specifing type constructors instead of data constructors
-- does not simplify or provide any other benifit in internal implementation.
namespace SuperDog
public export
record SuperDog where
@ -22,15 +33,15 @@ record Other a where
fieldA : a
fieldB : b
myDog_notWorking0 : record MkDog {name = "Sam"} -- Not all fields are covered
myDog_shouldNotTypecheck0 : record MkDog {name = "Sam"} -- Not all fields are covered
myDog_notWorking1 : record MkDog {age = 3, name1 = "Sam"} -- No constructor with name `MkDog`
-- has field `name1`
myDog_notWorking2 : record MkDog
{ age = 4
, age = 2
, weight = 12
, name = "Sam" } -- Duplicate names
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
@ -52,7 +63,7 @@ record Unit where
constructor MkUnit
unit : Fld.Unit
unit = record MkUnit {}
unit = record _ {} -- infer the constructor
namespace R1
@ -69,7 +80,82 @@ namespace R2
field : a
r1 : R1
r1 = record MkR {field = "string"} -- type-driven disambiguation
r1 = record _ {field = "string"} -- type-driven disambiguation
r2 : ?
r2 = record MkR {field = the Nat 22} -- fail, impossible to disambiguate
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