edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-12-01 06:12:57 +03:00
Code Issues Projects Releases Wiki Activity

Record editing metadata and interface hashes

Browse Source
This commit is contained in:
Edwin Brady 2019-05-31 11:42:11 +01:00
parent 2b38ce0188
commit a05c656d76
8 changed files with 82 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
src/Core/Context.idr
View File

@ -1,12 +1,13 @@
module Core.Context
import Core.CaseTree
import Core.CaseTree
import public Core.Core
import Core.Env
import Core.Env
import Core.Hash
import public Core.Name
import Core.Options
import Core.Options
import public Core.TT
import Core.TTC
import Core.TTC
import Utils.Binary
@ -500,6 +501,20 @@ initDefs
export
data Ctxt : Type where
export
addHash : {auto c : Ref Ctxt Defs} ->
Hashable a => a -> Core ()
addHash x
= do defs <- get Ctxt
put Ctxt (record { ifaceHash = hashWithSalt (ifaceHash defs) x } defs)
export
initHash : {auto c : Ref Ctxt Defs} ->
Core ()
initHash
= do defs <- get Ctxt
put Ctxt (record { ifaceHash = 5381 } defs)
export
addDef : {auto c : Ref Ctxt Defs} ->
Name -> GlobalDef -> Core Int

14
src/Core/FC.idr
View File

@ -18,6 +18,20 @@ record FC where
startPos : FilePos
endPos : FilePos
-- Return whether a given file position is within the file context (assuming we're
-- in the right file)
export
within : FilePos -> FC -> Bool
within (x, y) (MkFC _ start end)
= (x, y) >= start && (x, y) <= end
-- Return whether a given line is on the same line as the file context (assuming
-- we're in the right file)
export
onLine : Int -> FC -> Bool
onLine x (MkFC _ start end)
= x >= fst start && x <= fst end
export
emptyFC : FC
emptyFC = MkFC "(no file)" (0, 0) (0, 0)

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

@ -19,6 +19,7 @@ import TTImp.TTImp
-- names. Look in the Env first, then the global context.
getNameType : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto m : Ref MD Metadata} ->
{auto e : Ref EST (EState vars)} ->
RigCount -> Env Term vars ->
FC -> Name ->
@ -28,6 +29,7 @@ getNameType rigc env fc x
Just (MkIsDefined rigb lv) =>
do rigSafe rigb rigc
let bty = binderType (getBinder lv env)
addNameType fc x env bty
pure (Local fc (Just rigb) _ lv, gnf env bty)
Nothing =>
do defs <- get Ctxt
@ -39,6 +41,7 @@ getNameType rigc env fc x
DCon t a => DataCon t a
TCon t a _ _ _ _ => TyCon t a
_ => Func
addNameType fc x env (embed (type def))
pure (Ref fc nt (Resolved i), gnf env (embed (type def)))
where
rigSafe : RigCount -> RigCount -> Core ()
@ -50,6 +53,7 @@ getNameType rigc env fc x
-- Get the type of a variable, looking it up in the nested names first.
getVarType : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto m : Ref MD Metadata} ->
{auto e : Ref EST (EState vars)} ->
RigCount -> NestedNames vars -> Env Term vars ->
FC -> Name ->

4
src/TTImp/Elab/Hole.idr
View File

@ -3,6 +3,7 @@ module TTImp.Elab.Hole
import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.Normalise
import Core.Unify
import Core.TT
@ -16,6 +17,7 @@ import TTImp.TTImp
export
checkHole : {vars : _} ->
{auto c : Ref Ctxt Defs} ->
{auto m : Ref MD Metadata} ->
{auto u : Ref UST UState} ->
{auto e : Ref EST (EState vars)} ->
RigCount -> ElabInfo ->
@ -26,10 +28,12 @@ checkHole rig elabinfo nest env fc n_in (Just gexpty)
= do nm <- inCurrentNS (UN n_in)
expty <- getTerm gexpty
metaval <- metaVar fc rig env nm expty
withCurrentLHS nm
pure (metaval, gexpty)
checkHole rig elabinfo nest env fc n_in exp
= do nmty <- genName "holeTy"
ty <- metaVar fc Rig0 env nmty (TType fc)
nm <- inCurrentNS (UN n_in)
metaval <- metaVar fc rig env nm ty
withCurrentLHS nm
pure (metaval, gnf env ty)

3
src/TTImp/Elab/ImplicitBind.idr
View File

@ -435,7 +435,7 @@ checkBindVar rig elabinfo nest env fc str topexp
est <- get EST
put EST (record { boundNames $= ((n, NameBinding rig tm exp) ::),
toBind $= ((n, NameBinding rig tm bty) :: ) } est)
-- addNameType loc (UN str) env exp
addNameType fc (UN str) env exp
checkExp rig elabinfo env fc tm (gnf env exp) topexp
Just bty =>
do -- TODO: for metadata addNameType loc (UN str) env ty
@ -445,6 +445,7 @@ checkBindVar rig elabinfo nest env fc str topexp
let tm = bindingTerm bty
let ty = bindingType bty
defs <- get Ctxt
addNameType fc (UN str) env ty
checkExp rig elabinfo env fc tm (gnf env ty) topexp
where
updateRig : Name -> RigCount -> List (Name, ImplBinding vars) ->

17
src/TTImp/ProcessData.idr
View File

@ -3,6 +3,7 @@ module TTImp.ProcessData
import Core.Context
import Core.Core
import Core.Env
import Core.Hash
import Core.Metadata
import Core.Normalise
import Core.UnifyState
@ -73,8 +74,11 @@ checkCon {vars} opts nest env vis tn (MkImpTy fc cn_in ty_raw)
checkFamily fc cn tn env !(nf defs env ty)
let fullty = abstractEnvType fc env ty
logTermNF 5 (show cn) [] fullty
-- TODO: Interface hash
case vis of
Public => do addHash cn
addHash fullty
_ => pure ()
pure (MkCon fc cn !(getArity defs [] fullty) fullty)
conName : Constructor -> Name
@ -108,10 +112,13 @@ processData {vars} eopts nest env fc vis (MkImpLater dfc n_in ty_raw)
checkIsType fc n env !(nf defs env ty)
arity <- getArity defs [] fullty
-- Add the type constructor as a placeholder while checking
-- data constructors
-- Add the type constructor as a placeholder
tidx <- addDef n (newDef fc n Rig1 fullty vis
(TCon 0 arity [] [] [] []))
case vis of
Private => pure ()
_ => do addHash n
addHash fullty
pure ()
processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_raw)
= do n <- inCurrentNS n_in
@ -148,6 +155,10 @@ processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_ra
-- data constructors
tidx <- addDef n (newDef fc n Rig1 fullty vis
(TCon 0 arity [] [] [] []))
case vis of
Private => pure ()
_ => do addHash n
addHash fullty
-- Constructors are private if the data type as a whole is
-- export

17
src/TTImp/ProcessDef.idr
View File

@ -5,6 +5,7 @@ import Core.CaseTree
import Core.Context
import Core.Core
import Core.Env
import Core.Hash
import Core.Metadata
import Core.Normalise
import Core.Value
@ -177,6 +178,7 @@ checkLHS mult hashit n opts nest env fc lhs_in
logTerm 5 "LHS term" lhstm_lin
logTerm 5 "LHS type" lhsty_lin
setHoleLHS (bindEnv fc env lhstm_lin)
extendEnv env SubRefl nest lhstm_lin lhsty_lin
@ -233,8 +235,21 @@ checkClause {vars} mult hashit n opts nest env (PatClause fc lhs_in rhs)
Rig0 => InType
_ => InExpr
(rhstm, rhserased) <- checkTermSub n rhsMode opts nest' env' env sub' rhs (gnf env' lhsty')
clearHoleLHS
logTerm 5 "RHS term" rhstm
when hashit $
do addHash lhstm'
addHash rhstm
-- If the rhs is a hole, record the lhs in the metadata because we
-- might want to split it interactively
case rhstm of
Meta _ _ _ _ =>
addLHS (getFC lhs_in) (length env) env' lhstm'
_ => pure ()
pure (Just (MkClause env' lhstm' rhstm,
MkClause env' lhstm' rhserased))
checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw cs)
@ -247,6 +262,8 @@ checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw cs
(wval, wval_erased, gwvalTy) <- wrapError (InRHS fc (Resolved n)) $
elabTermSub n wmode opts nest' env' env sub' wval_raw Nothing
clearHoleLHS
logTerm 5 "With value" wval
logTerm 5 "Required type" reqty
wvalTy <- getTerm gwvalTy

10
src/TTImp/ProcessType.idr
View File

@ -3,6 +3,7 @@ module TTImp.ProcessType
import Core.Context
import Core.Core
import Core.Env
import Core.Hash
import Core.Metadata
import Core.Normalise
import Core.TT
@ -80,5 +81,10 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw)
log 1 $ "Setting options for " ++ show n ++ ": " ++ show opts
traverse (processFnOpt fc (Resolved idx)) opts
-- TODO: Interface hash and saving
pure ()
-- Add to the interactive editing metadata
addTyDecl fc (Resolved idx) env ty -- for definition generation
addNameType fc (Resolved idx) env ty -- for looking up types
when (vis /= Private) $
do addHash n
addHash ty