edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2025-01-03 10:14:53 +03:00
Code Issues Projects Releases Wiki Activity

Add syntax for 'using' blocks

Browse Source
This commit is contained in:
Edwin Brady 2020-01-24 15:21:16 +00:00
parent c84e2b5cb7
commit 118ea787c3
10 changed files with 76 additions and 24 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
src/Idris/Desugar.idr
View File

@ -409,7 +409,9 @@ mutual
{auto m : Ref MD Metadata} ->
List Name -> PTypeDecl -> Core ImpTy
desugarType ps (MkPTy fc n ty)
= pure $ MkImpTy fc n !(bindTypeNames ps !(desugar AnyExpr ps ty))
= do syn <- get Syn
pure $ MkImpTy fc n !(bindTypeNames (usingImpl syn)
ps !(desugar AnyExpr ps ty))
desugarClause : {auto s : Ref Syn SyntaxInfo} ->
{auto c : Ref Ctxt Defs} ->
@ -439,11 +441,16 @@ mutual
{auto m : Ref MD Metadata} ->
List Name -> PDataDecl -> Core ImpData
desugarData ps (MkPData fc n tycon opts datacons)
= pure $ MkImpData fc n !(bindTypeNames ps !(desugar AnyExpr ps tycon))
= do syn <- get Syn
pure $ MkImpData fc n
!(bindTypeNames (usingImpl syn)
ps !(desugar AnyExpr ps tycon))
opts
!(traverse (desugarType ps) datacons)
desugarData ps (MkPLater fc n tycon)
= pure $ MkImpLater fc n !(bindTypeNames ps !(desugar AnyExpr ps tycon))
= do syn <- get Syn
pure $ MkImpLater fc n !(bindTypeNames (usingImpl syn)
ps !(desugar AnyExpr ps tycon))
desugarField : {auto s : Ref Syn SyntaxInfo} ->
{auto c : Ref Ctxt Defs} ->
@ -452,7 +459,9 @@ mutual
List Name -> PField ->
Core IField
desugarField ps (MkField fc rig p n ty)
= pure (MkIField fc rig p n !(bindTypeNames ps !(desugar AnyExpr ps ty)))
= do syn <- get Syn
pure (MkIField fc rig p n !(bindTypeNames (usingImpl syn)
ps !(desugar AnyExpr ps ty)))
-- Get the declaration to process on each pass of a mutual block
-- Essentially: types on the first pass
@ -488,6 +497,8 @@ mutual
getDecl p (PParameters fc ps pds)
= Just (PParameters fc ps (mapMaybe (getDecl p) pds))
getDecl p (PUsing fc ps pds)
= Just (PUsing fc ps (mapMaybe (getDecl p) pds))
getDecl Single d = Just d
@ -546,6 +557,16 @@ mutual
(map snd params')
let paramsb = map (\ (n, tm) => (n, doBind pnames tm)) params'
pure [IParameters fc paramsb (concat pds')]
desugarDecl ps (PUsing fc uimpls uds)
= do syn <- get Syn
let oldu = usingImpl syn
uimpls' <- traverse (\ ntm => do tm' <- desugar AnyExpr ps (snd ntm)
pure (fst ntm, tm')) uimpls
put Syn (record { usingImpl = uimpls' ++ oldu } syn)
uds' <- traverse (desugarDecl ps) uds
syn <- get Syn
put Syn (record { usingImpl = oldu } syn)
pure (concat uds')
desugarDecl ps (PReflect fc tm)
= throw (GenericMsg fc "Reflection not implemented yet")
-- pure [IReflect fc !(desugar AnyExpr ps tm)]

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

@ -41,9 +41,9 @@ mkIfaceData {vars} fc vis env constraints n conName ps dets meths
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
con = MkImpTy fc conName !(bindTypeNames (map fst ps ++ map fst meths ++ vars) conty) in
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)
!(bindTypeNames [] (map fst ps ++ map fst meths ++ vars)
(mkDataTy fc ps))
opts [con])
where
@ -83,7 +83,7 @@ getMethDecl : {auto c : Ref Ctxt Defs} ->
(FC, RigCount, List FnOpt, n, (Bool, RawImp)) ->
Core (n, RigCount, RawImp)
getMethDecl {vars} env nest params mnames (fc, c, opts, n, (d, ty))
= do ty_imp <- bindTypeNames (map fst params ++ mnames ++ vars) ty
= do ty_imp <- bindTypeNames [] (map fst params ++ mnames ++ vars) ty
pure (n, c, stripParams (map fst params) ty_imp)
where
-- We don't want the parameters to explicitly appear in the method
@ -120,7 +120,7 @@ getMethToplevel {vars} env vis iname cname constraints allmeths params
-- Make the constraint application explicit for any method names
-- which appear in other method types
let ty_constr = substNames vars (map applyCon allmeths) ty
ty_imp <- bindTypeNames vars (bindIFace fc ity ty_constr)
ty_imp <- bindTypeNames [] vars (bindIFace fc ity ty_constr)
cn <- inCurrentNS n
let tydecl = IClaim fc c vis (if d then [Inline, Invertible]
else [Inline])
@ -174,7 +174,7 @@ getConstraintHint : {auto c : Ref Ctxt Defs} ->
getConstraintHint {vars} fc env vis iname cname constraints meths params (cn, con)
= do let ity = apply (IVar fc iname) (map (IVar fc) params)
let fty = IPi fc RigW Explicit Nothing ity con
ty_imp <- bindTypeNames (meths ++ vars) fty
ty_imp <- bindTypeNames [] (meths ++ vars) fty
let hintname = DN ("Constraint " ++ show con)
(UN ("__" ++ show iname ++ "_" ++ show con))
let tydecl = IClaim fc RigW vis [Inline, Hint False]
@ -331,7 +331,7 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
(map fst tydecls)
let dty = substNames vars methNameMap dty
dty_imp <- bindTypeNames (map fst tydecls ++ vars)
dty_imp <- bindTypeNames [] (map fst tydecls ++ vars)
(bindIFace fc ity dty)
log 5 $ "Default method " ++ show dn ++ " : " ++ show dty_imp
let dtydecl = IClaim fc rig vis [] (MkImpTy fc dn dty_imp)

20
src/Idris/Parser.idr
View File

@ -1011,6 +1011,24 @@ paramDecls fname indents
end <- location
pure (PParameters (MkFC fname start end) ps (collectDefs (concat ds)))
usingDecls : FileName -> IndentInfo -> Rule PDecl
usingDecls fname indents
= do start <- location
keyword "using"
commit
symbol "("
us <- sepBy (symbol ",")
(do n <- option Nothing
(do x <- unqualifiedName
symbol ":"
pure (Just (UN x)))
ty <- typeExpr pdef fname indents
pure (n, ty))
symbol ")"
ds <- assert_total (nonEmptyBlock (topDecl fname))
end <- location
pure (PUsing (MkFC fname start end) us (collectDefs (concat ds)))
fnOpt : Rule PFnOpt
fnOpt
= do keyword "partial"
@ -1260,6 +1278,8 @@ topDecl fname indents
pure [d]
<|> do d <- paramDecls fname indents
pure [d]
<|> do d <- usingDecls fname indents
pure [d]
<|> do d <- directiveDecl fname indents
pure [d]
<|> do start <- location

6
src/Idris/Syntax.idr
View File

@ -195,6 +195,7 @@ mutual
PDef : FC -> List PClause -> PDecl
PData : FC -> Visibility -> PDataDecl -> PDecl
PParameters : FC -> List (Name, PTerm) -> List PDecl -> PDecl
PUsing : FC -> List (Maybe Name, PTerm) -> List PDecl -> PDecl
PReflect : FC -> PTerm -> PDecl
PInterface : FC ->
Visibility ->
@ -243,6 +244,7 @@ definedIn [] = []
definedIn (PClaim _ _ _ _ (MkPTy _ n _) :: ds) = n :: definedIn ds
definedIn (PData _ _ d :: ds) = definedInData d ++ definedIn ds
definedIn (PParameters _ _ pds :: ds) = definedIn pds ++ definedIn ds
definedIn (PUsing _ _ pds :: ds) = definedIn pds ++ definedIn ds
definedIn (PNamespace _ _ ns :: ds) = definedIn ns ++ definedIn ds
definedIn (_ :: ds) = definedIn ds
@ -512,6 +514,7 @@ record SyntaxInfo where
ifaces : ANameMap IFaceInfo
bracketholes : List Name -- hole names in argument position (so need
-- to be bracketed when solved)
usingImpl : List (Maybe Name, RawImp)
startExpr : RawImp
export
@ -545,7 +548,7 @@ TTC SyntaxInfo where
bhs <- fromBuf b
start <- fromBuf b
pure (MkSyntax (fromList inf) (fromList pre) (fromList ifs)
bhs start)
bhs [] start)
HasNames IFaceInfo where
full gam iface
@ -590,6 +593,7 @@ initSyntax
(insert "-" 10 empty)
empty
[]
[]
(IVar (MkFC "(default)" (0, 0) (0, 0)) (UN "main"))
-- A label for Syntax info in the global state

16
src/TTImp/BindImplicits.idr
View File

@ -115,14 +115,20 @@ bindNames arg tm
pure (map UN (map snd ns), doBind ns tm)
else pure ([], tm)
addUsing : List (Maybe Name, RawImp) ->
RawImp -> RawImp
addUsing uimpls tm = tm
export
bindTypeNames : {auto c : Ref Ctxt Defs} ->
List (Maybe Name, RawImp) ->
List Name -> RawImp-> Core RawImp
bindTypeNames env tm
= if !isAutoImplicits
then do let ns = nub (findBindableNames True env [] tm)
pure (doBind ns tm)
else pure tm
bindTypeNames uimpls env tm_in
= let tm = addUsing uimpls tm_in in
if !isAutoImplicits
then do let ns = nub (findBindableNames True env [] tm)
pure (doBind ns tm)
else pure tm
export
bindTypeNamesUsed : {auto c : Ref Ctxt Defs} ->

6
src/TTImp/ProcessData.idr
View File

@ -65,7 +65,7 @@ checkCon : {vars : _} ->
ImpTy -> Core Constructor
checkCon {vars} opts nest env vis tn (MkImpTy fc cn_in ty_raw)
= do cn <- inCurrentNS cn_in
ty_raw <- bindTypeNames vars ty_raw
ty_raw <- bindTypeNames [] vars ty_raw
defs <- get Ctxt
-- Check 'cn' is undefined
@ -187,7 +187,7 @@ processData : {vars : _} ->
ImpData -> Core ()
processData {vars} eopts nest env fc vis (MkImpLater dfc n_in ty_raw)
= do n <- inCurrentNS n_in
ty_raw <- bindTypeNames vars ty_raw
ty_raw <- bindTypeNames [] vars ty_raw
defs <- get Ctxt
-- Check 'n' is undefined
@ -224,7 +224,7 @@ processData {vars} eopts nest env fc vis (MkImpLater dfc n_in ty_raw)
processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_raw)
= do n <- inCurrentNS n_in
ty_raw <- bindTypeNames vars ty_raw
ty_raw <- bindTypeNames [] vars ty_raw
log 1 $ "Processing " ++ show n
defs <- get Ctxt

2
src/TTImp/ProcessParams.idr
View File

@ -36,7 +36,7 @@ processParams {vars} {c} {m} {u} nest env fc ps ds
-- then read off the environment from the elaborated type. This way
-- we'll get all the implicit names we need
let pty_raw = mkParamTy ps
pty_imp <- bindTypeNames vars (IBindHere fc (PI Rig0) pty_raw)
pty_imp <- bindTypeNames [] vars (IBindHere fc (PI Rig0) pty_raw)
log 10 $ "Checking " ++ show pty_imp
pty <- checkTerm (-1) InType []
nest env pty_imp (gType fc)

6
src/TTImp/ProcessRecord.idr
View File

@ -65,9 +65,9 @@ elabRecord {vars} eopts fc env nest vis tn params rcon fields
= do let retty = apply (IVar fc tn) (map (IVar fc) (map fst params))
let conty = mkTy (map jname params) $
mkTy (map farg fields) retty
let con = MkImpTy fc cname !(bindTypeNames (map fst params ++
let con = MkImpTy fc cname !(bindTypeNames [] (map fst params ++
map fname fields ++ vars) conty)
let dt = MkImpData fc tn !(bindTypeNames (map fst params ++
let dt = MkImpData fc tn !(bindTypeNames [] (map fst params ++
map fname fields ++ vars)
(mkDataTy fc params)) [] [con]
log 5 $ "Record data type " ++ show dt
@ -98,7 +98,7 @@ elabRecord {vars} eopts fc env nest vis tn params rcon fields
ty <- unelab tyenv ty_chk
let ty' = substNames vars upds ty
let rname = MN "rec" 0
gty <- bindTypeNames
gty <- bindTypeNames []
(map fst params ++ map fname fields ++ vars) $
mkTy (map jname params) $
IPi fc RigW Explicit (Just rname) recTy ty'

2
src/TTImp/ProcessType.idr
View File

@ -103,7 +103,7 @@ processType : {vars : _} ->
List FnOpt -> ImpTy -> Core ()
processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw)
= do n <- inCurrentNS n_in
ty_raw <- bindTypeNames vars ty_raw
ty_raw <- bindTypeNames [] vars ty_raw
log 1 $ "Processing " ++ show n
log 5 $ "Checking type decl " ++ show n ++ " : " ++ show ty_raw

1
src/TTImp/TTImp.idr
View File

@ -552,6 +552,7 @@ getFn : RawImp -> RawImp
getFn (IApp _ f arg) = getFn f
getFn (IWithApp _ f arg) = getFn f
getFn (IImplicitApp _ f _ _) = getFn f
getFn (IAs _ _ _ f) = getFn f
getFn f = f
-- Everything below is TTC instances