edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-09-11 16:05:51 +03:00
Code Issues Projects Releases Wiki Activity

Check and add transform rules

Browse Source 
They don't do anything yet though
This commit is contained in:
Edwin Brady 2020-05-09 18:55:56 +01:00
parent 15c6a0d137
commit 449f29b723
14 changed files with 104 additions and 37 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
idris2.ipkg
View File

@ -118,6 +118,7 @@ modules =
TTImp.ProcessDef,
TTImp.ProcessParams,
TTImp.ProcessRecord,
TTImp.ProcessTransform,
TTImp.ProcessType,
-- TTImp.Reflect,
TTImp.TTImp,

1
idris2api.ipkg
View File

@ -112,6 +112,7 @@ modules =
TTImp.ProcessDef,
TTImp.ProcessParams,
TTImp.ProcessRecord,
TTImp.ProcessTransform,
TTImp.ProcessType,
TTImp.TTImp,
TTImp.Unelab,

2
libs/base/Data/IORef.idr
View File

@ -1,7 +1,5 @@
module Data.IORef
%cg chicken (use box)
-- Implemented externally
-- e.g., in Scheme, passed around as a box
data Mut : Type -> Type where [external]

28
src/Core/Binary.idr
View File

@ -27,7 +27,7 @@ import Data.Buffer
-- TTC files can only be compatible if the version number is the same
export
ttcVersion : Int
ttcVersion = 23
ttcVersion = 24
export
checkTTCVersion : String -> Int -> Int -> Core ()
@ -52,6 +52,7 @@ record TTCFile extra where
primnames : PrimNames
namedirectives : List (Name, List String)
cgdirectives : List (CG, String)
transforms : List (Name, Transform)
extraData : extra
HasNames a => HasNames (List a) where
@ -77,6 +78,10 @@ HasNames (Name, List String) where
full c (n, b) = pure (!(full c n), b)
resolved c (n, b) = pure (!(resolved c n), b)
HasNames (Name, Transform) where
full c (n, b) = pure (!(full c n), !(full c b))
resolved c (n, b) = pure (!(resolved c n), !(resolved c b))
HasNames (Name, Name, Bool) where
full c (n1, n2, b) = pure (!(full c n1), !(full c n2), b)
resolved c (n1, n2, b) = pure (!(resolved c n1), !(resolved c n2), b)
@ -87,7 +92,7 @@ HasNames e => HasNames (TTCFile e) where
autoHints typeHints
imported nextVar currentNS nestedNS
pairnames rewritenames primnames
namedirectives cgdirectives
namedirectives cgdirectives trans
extra)
= pure $ MkTTCFile version ifaceHash iHashes
context userHoles
@ -99,6 +104,7 @@ HasNames e => HasNames (TTCFile e) where
!(fullPrim gam primnames)
!(full gam namedirectives)
cgdirectives
!(full gam trans)
!(full gam extra)
where
fullPair : Context -> Maybe PairNames -> Core (Maybe PairNames)
@ -124,7 +130,7 @@ HasNames e => HasNames (TTCFile e) where
autoHints typeHints
imported nextVar currentNS nestedNS
pairnames rewritenames primnames
namedirectives cgdirectives
namedirectives cgdirectives trans
extra)
= pure $ MkTTCFile version ifaceHash iHashes
context userHoles
@ -136,6 +142,7 @@ HasNames e => HasNames (TTCFile e) where
!(resolvedPrim gam primnames)
!(resolved gam namedirectives)
cgdirectives
!(resolved gam trans)
!(resolved gam extra)
where
resolvedPair : Context -> Maybe PairNames -> Core (Maybe PairNames)
@ -184,6 +191,7 @@ writeTTCFile b file_in
toBuf b (primnames file)
toBuf b (namedirectives file)
toBuf b (cgdirectives file)
toBuf b (transforms file)
toBuf b (extraData file)
readTTCFile : TTC extra =>
@ -212,11 +220,12 @@ readTTCFile modns as b
prims <- fromBuf b
nds <- fromBuf b
cgds <- fromBuf b
trans <- fromBuf b
ex <- fromBuf b
pure (MkTTCFile ver ifaceHash importHashes
defs uholes
autohs typehs imp nextv cns nns
pns rws prims nds cgds ex)
pns rws prims nds cgds trans ex)
-- Pull out the list of GlobalDefs that we want to save
getSaveDefs : List Name -> List (Name, Binary) -> Defs ->
@ -261,6 +270,7 @@ writeToTTC extradata fname
(primnames (options defs))
(NameMap.toList (namedirectives defs))
(cgdirectives defs)
(saveTransforms defs)
extradata)
Right ok <- coreLift $ writeToFile fname !(get Bin)
| Left err => throw (InternalError (fname ++ ": " ++ show err))
@ -350,6 +360,15 @@ updateCGDirectives cgs
let cgs' = nub (cgs ++ cgdirectives defs)
put Ctxt (record { cgdirectives = cgs' } defs)
export
updateTransforms : {auto c : Ref Ctxt Defs} ->
List (Name, Transform) -> Core ()
updateTransforms [] = pure ()
updateTransforms ((n, t) :: ts)
= do defs <- get Ctxt
put Ctxt (record { transforms $= insert n t } defs)
updateTransforms ts
getNSas : (String, (List String, Bool, List String)) ->
(List String, List String)
getNSas (a, (b, c, d)) = (b, d)
@ -407,6 +426,7 @@ readFromTTC loc reexp fname modNS importAs
updatePrims (primnames ttc)
updateNameDirectives (reverse (namedirectives ttc))
updateCGDirectives (cgdirectives ttc)
updateTransforms (transforms ttc)
when (not reexp) clearSavedHints
resetFirstEntry

14
src/Core/Context.idr
View File

@ -513,11 +513,12 @@ newDef fc n rig vars ty vis def
-- 'NF but we're working with terms rather than values...)
public export
data Transform : Type where
MkTransform : Env Term vars -> Term vars -> Term vars -> Transform
MkTransform : Name -> -- name for identifying the rule
Env Term vars -> Term vars -> Term vars -> Transform
export
getFnName : Transform -> Maybe Name
getFnName (MkTransform _ app _)
getFnName (MkTransform _ _ app _)
= case getFn app of
Ref _ _ fn => Just fn
_ => Nothing
@ -771,11 +772,12 @@ HasNames GlobalDef where
export
HasNames Transform where
full gam (MkTransform env lhs rhs)
= pure $ MkTransform !(full gam env) !(full gam lhs) !(full gam rhs)
full gam (MkTransform n env lhs rhs)
= pure $ MkTransform !(full gam n) !(full gam env)
!(full gam lhs) !(full gam rhs)
resolved gam (MkTransform env lhs rhs)
= pure $ MkTransform !(resolved gam env)
resolved gam (MkTransform n env lhs rhs)
= pure $ MkTransform !(resolved gam n) !(resolved gam env)
!(resolved gam lhs) !(resolved gam rhs)
public export

7
src/Core/TTC.idr
View File

@ -961,19 +961,22 @@ TTC GlobalDef where
top [] Public unchecked [] refs refsR
False False True def cdef Nothing [])
export
TTC Transform where
toBuf b (MkTransform {vars} env lhs rhs)
toBuf b (MkTransform {vars} n env lhs rhs)
= do toBuf b vars
toBuf b n
toBuf b env
toBuf b lhs
toBuf b rhs
fromBuf b
= do vars <- fromBuf b
n <- fromBuf b
env <- fromBuf b
lhs <- fromBuf b
rhs <- fromBuf b
pure (MkTransform {vars} env lhs rhs)
pure (MkTransform {vars} n env lhs rhs)
-- decode : Context -> Int -> (update : Bool) -> ContextEntry -> Core GlobalDef
Core.Context.decode gam idx update (Coded bin)

4
src/Idris/Desugar.idr
View File

@ -790,10 +790,10 @@ mutual
desugarDecl ps (PNamespace fc ns decls)
= do ds <- traverse (desugarDecl ps) decls
pure [INamespace fc ns (concat ds)]
desugarDecl ps (PTransform fc lhs rhs)
desugarDecl ps (PTransform fc n lhs rhs)
= do (bound, blhs) <- bindNames False !(desugar LHS ps lhs)
rhs' <- desugar AnyExpr (bound ++ ps) rhs
pure [ITransform fc blhs rhs']
pure [ITransform fc (UN n) blhs rhs']
desugarDecl ps (PDirective fc d)
= case d of
Hide n => pure [IPragma (\c, nest, env => hide fc n)]

7
src/Idris/Parser.idr
View File

@ -1093,13 +1093,14 @@ namespaceDecl fname indents
transformDecl : FileName -> IndentInfo -> Rule PDecl
transformDecl fname indents
= do pragma "transform"
start <- location
= do start <- location
pragma "transform"
n <- strLit
lhs <- expr plhs fname indents
symbol "="
rhs <- expr pnowith fname indents
end <- location
pure (PTransform (MkFC fname start end) lhs rhs)
pure (PTransform (MkFC fname start end) n lhs rhs)
mutualDecls : FileName -> IndentInfo -> Rule PDecl
mutualDecls fname indents

5
src/Idris/Resugar.idr
View File

@ -387,8 +387,9 @@ mutual
toPDecl (INamespace fc ns ds)
= do ds' <- traverse toPDecl ds
pure (Just (PNamespace fc ns (mapMaybe id ds')))
toPDecl (ITransform fc lhs rhs)
= pure (Just (PTransform fc !(toPTerm startPrec lhs)
toPDecl (ITransform fc n lhs rhs)
= pure (Just (PTransform fc (show n)
!(toPTerm startPrec lhs)
!(toPTerm startPrec rhs)))
toPDecl (IPragma _) = pure Nothing
toPDecl (ILog _) = pure Nothing

4
src/Idris/Syntax.idr
View File

@ -238,7 +238,7 @@ mutual
PMutual : FC -> List PDecl -> PDecl
PFixity : FC -> Fixity -> Nat -> OpStr -> PDecl
PNamespace : FC -> List String -> List PDecl -> PDecl
PTransform : FC -> PTerm -> PTerm -> PDecl
PTransform : FC -> String -> PTerm -> PTerm -> PDecl
PDirective : FC -> Directive -> PDecl
definedInData : PDataDecl -> List Name
@ -847,7 +847,7 @@ mapPTermM f = goPTerm where
goPDecl (PMutual fc ps) = PMutual fc <$> goPDecls ps
goPDecl p@(PFixity _ _ _ _) = pure p
goPDecl (PNamespace fc strs ps) = PNamespace fc strs <$> goPDecls ps
goPDecl (PTransform fc a b) = PTransform fc <$> goPTerm a <*> goPTerm b
goPDecl (PTransform fc n a b) = PTransform fc n <$> goPTerm a <*> goPTerm b
goPDecl p@(PDirective _ _) = pure p

5
src/TTImp/ProcessDecls.idr
View File

@ -15,6 +15,7 @@ import TTImp.ProcessData
import TTImp.ProcessDef
import TTImp.ProcessParams
import TTImp.ProcessRecord
import TTImp.ProcessTransform
import TTImp.ProcessType
import TTImp.TTImp
@ -42,8 +43,8 @@ process eopts nest env (INamespace fc ns decls)
traverse_ (processDecl eopts nest env) decls
defs <- get Ctxt
put Ctxt (record { currentNS = cns } defs)
process eopts nest env (ITransform fc lhs rhs)
= throw (GenericMsg fc "%transform not yet implemented")
process eopts nest env (ITransform fc n lhs rhs)
= processTransform eopts nest env fc n lhs rhs
process {c} eopts nest env (IPragma act)
= act c nest env
process eopts nest env (ILog n)

17
src/TTImp/ProcessDef.idr
View File

@ -209,10 +209,12 @@ combineLinear loc ((n, count) :: cs)
= do newc <- combine c c'
combineAll newc cs
export -- also used by Transforms
checkLHS : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto m : Ref MD Metadata} ->
{auto u : Ref UST UState} ->
Bool -> -- in transform
(mult : RigCount) -> (hashit : Bool) ->
Int -> List ElabOpt -> NestedNames vars -> Env Term vars ->
FC -> RawImp ->
@ -220,9 +222,11 @@ checkLHS : {vars : _} ->
(vars' ** (SubVars vars vars',
Env Term vars', NestedNames vars',
Term vars', Term vars')))
checkLHS {vars} mult hashit n opts nest env fc lhs_in
checkLHS {vars} trans mult hashit n opts nest env fc lhs_in
= do defs <- get Ctxt
lhs_raw <- lhsInCurrentNS nest lhs_in
lhs_raw <- if trans
then pure lhs_in
else lhsInCurrentNS nest lhs_in
autoimp <- isUnboundImplicits
setUnboundImplicits True
(_, lhs_bound) <- bindNames False lhs_raw
@ -232,9 +236,12 @@ checkLHS {vars} mult hashit n opts nest env fc lhs_in
log 5 $ "Checking LHS of " ++ show !(getFullName (Resolved n)) ++
" " ++ show lhs
logEnv 5 "In env" env
let lhsMode = if trans
then InExpr
else InLHS mult
(lhstm, lhstyg) <-
wrapError (InLHS fc !(getFullName (Resolved n))) $
elabTerm n (InLHS mult) opts nest env
elabTerm n lhsMode opts nest env
(IBindHere fc PATTERN lhs) Nothing
logTerm 5 "Checked LHS term" lhstm
lhsty <- getTerm lhstyg
@ -361,7 +368,7 @@ checkClause mult hashit n opts nest env (ImpossibleClause fc lhs)
else throw (ValidCase fc env (Right err)))
checkClause {vars} mult hashit n opts nest env (PatClause fc lhs_in rhs)
= do (_, (vars' ** (sub', env', nest', lhstm', lhsty'))) <-
checkLHS mult hashit n opts nest env fc lhs_in
checkLHS False mult hashit n opts nest env fc lhs_in
let rhsMode = if isErased mult then InType else InExpr
log 5 $ "Checking RHS " ++ show rhs
logEnv 5 "In env" env'
@ -386,7 +393,7 @@ checkClause {vars} mult hashit n opts nest env (PatClause fc lhs_in rhs)
-- TODO: (to decide) With is complicated. Move this into its own module?
checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw cs)
= do (lhs, (vars' ** (sub', env', nest', lhspat, reqty))) <-
checkLHS mult hashit n opts nest env fc lhs_in
checkLHS False mult hashit n opts nest env fc lhs_in
let wmode
= if isErased mult then InType else InExpr

31
src/TTImp/ProcessTransform.idr Normal file
View File

@ -0,0 +1,31 @@
module TTImp.ProcessTransform
import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.Normalise
import Core.UnifyState
import TTImp.Elab
import TTImp.Elab.Check
import TTImp.ProcessDef -- for checking LHS
import TTImp.TTImp
export
processTransform : {auto c : Ref Ctxt Defs} ->
{auto m : Ref MD Metadata} ->
{auto u : Ref UST UState} ->
List ElabOpt -> NestedNames vars -> Env Term vars -> FC ->
Name -> RawImp -> RawImp -> Core ()
processTransform eopts nest env fc tn_in lhs rhs
= do tn <- inCurrentNS tn_in
tidx <- resolveName tn
(_, (vars' ** (sub', env', nest', lhstm, lhsty))) <-
checkLHS True top True tidx eopts nest env fc lhs
logTerm 3 "Transform LHS" lhstm
rhstm <- wrapError (InRHS fc tn_in) $
checkTermSub tidx InExpr eopts nest' env' env sub' rhs (gnf env' lhsty)
clearHoleLHS
logTerm 3 "Transform RHS" rhstm
addTransform fc (MkTransform tn env' lhstm rhstm)

15
src/TTImp/TTImp.idr
View File

@ -311,7 +311,7 @@ mutual
Maybe String -> -- nested namespace
Visibility -> ImpRecord -> ImpDecl
INamespace : FC -> List String -> List ImpDecl -> ImpDecl
ITransform : FC -> RawImp -> RawImp -> ImpDecl
ITransform : FC -> Name -> RawImp -> RawImp -> ImpDecl
IPragma : ({vars : _} -> Ref Ctxt Defs ->
NestedNames vars -> Env Term vars -> Core ()) ->
ImpDecl
@ -329,8 +329,8 @@ mutual
show (INamespace _ ns decls)
= "namespace " ++ show ns ++
showSep "\n" (assert_total $ map show decls)
show (ITransform _ lhs rhs)
= "%transform " ++ show lhs ++ " ==> " ++ show rhs
show (ITransform _ n lhs rhs)
= "%transform " ++ show n ++ " " ++ show lhs ++ " ==> " ++ show rhs
show (IPragma _) = "[externally defined pragma]"
show (ILog lvl) = "%logging " ++ show lvl
@ -933,8 +933,8 @@ mutual
= do tag 4; toBuf b fc; toBuf b ns; toBuf b vis; toBuf b r
toBuf b (INamespace fc xs ds)
= do tag 5; toBuf b fc; toBuf b xs; toBuf b ds
toBuf b (ITransform fc lhs rhs)
= do tag 6; toBuf b fc; toBuf b lhs; toBuf b rhs
toBuf b (ITransform fc n lhs rhs)
= do tag 6; toBuf b fc; toBuf b n; toBuf b lhs; toBuf b rhs
toBuf b (IPragma f) = throw (InternalError "Can't write Pragma")
toBuf b (ILog n)
= do tag 7; toBuf b n
@ -960,8 +960,9 @@ mutual
5 => do fc <- fromBuf b; xs <- fromBuf b
ds <- fromBuf b
pure (INamespace fc xs ds)
6 => do fc <- fromBuf b; lhs <- fromBuf b; rhs <- fromBuf b
pure (ITransform fc lhs rhs)
6 => do fc <- fromBuf b; n <- fromBuf b
lhs <- fromBuf b; rhs <- fromBuf b
pure (ITransform fc n lhs rhs)
7 => do n <- fromBuf b
pure (ILog n)
_ => corrupt "ImpDecl"