mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-09-11 16:05:51 +03:00
Add Metadata type
Metadata is now propagated through the elaborator, although we're not using it yet
This commit is contained in:
parent
6c88bfec7a
commit
2b38ce0188
@ -236,7 +236,9 @@ readFromTTC : TTC extra =>
|
||||
(fname : String) -> -- file containing the module
|
||||
(modNS : List String) -> -- module namespace
|
||||
(importAs : List String) -> -- namespace to import as
|
||||
Core (Maybe (extra, Int, List (List String, Bool, List String)))
|
||||
Core (Maybe (extra, Int,
|
||||
List (List String, Bool, List String),
|
||||
NameRefs))
|
||||
readFromTTC loc reexp fname modNS importAs
|
||||
= logTime "Reading TTC" $
|
||||
do defs <- get Ctxt
|
||||
@ -269,7 +271,7 @@ readFromTTC loc reexp fname modNS importAs
|
||||
put UST (record { holes = fromList (holes ttc),
|
||||
constraints = fromList (constraints ttc),
|
||||
nextName = nextVar ttc } ust)
|
||||
pure (Just (extraData ttc, ifaceHash ttc, imported ttc))
|
||||
pure (Just (extraData ttc, ifaceHash ttc, imported ttc, r))
|
||||
|
||||
getImportHashes : NameRefs -> Ref Bin Binary ->
|
||||
Core (List (List String, Int))
|
||||
|
214
src/Core/Metadata.idr
Normal file
214
src/Core/Metadata.idr
Normal file
@ -0,0 +1,214 @@
|
||||
module Core.Metadata
|
||||
|
||||
import Core.Binary
|
||||
import Core.Context
|
||||
import Core.Core
|
||||
import Core.Env
|
||||
import Core.FC
|
||||
import Core.Normalise
|
||||
import Core.TT
|
||||
import Core.TTC
|
||||
|
||||
-- Additional data we keep about the context to support interactive editing
|
||||
|
||||
public export
|
||||
record Metadata where
|
||||
constructor MkMetadata
|
||||
-- Mapping from source annotation (location, typically) to
|
||||
-- the LHS defined at that location. Also record the outer environment
|
||||
-- length, since we don't want to case split on these.
|
||||
lhsApps : List (FC, (Nat, ClosedTerm))
|
||||
-- Mapping from annotation the the name defined with that annotation,
|
||||
-- and its type (so, giving the ability to get the types of locally
|
||||
-- defined names)
|
||||
-- The type is abstracted over the whole environment; the Nat gives
|
||||
-- the number of names which were in the environment at the time
|
||||
names : List (FC, (Name, Nat, ClosedTerm))
|
||||
-- Mapping from annotation to the name that's declared there and
|
||||
-- its type; the Nat is as above
|
||||
tydecls : List (FC, (Name, Nat, ClosedTerm))
|
||||
-- Current lhs, if applicable, and a mapping from hole names to the
|
||||
-- lhs they're under. This is for expression search, to ensure that
|
||||
-- recursive calls have a smaller value as an argument.
|
||||
-- Also use this to get the name of the function being defined (i.e.
|
||||
-- to know what the recursive call is, if applicable)
|
||||
currentLHS : Maybe ClosedTerm
|
||||
holeLHS : List (Name, ClosedTerm)
|
||||
|
||||
export
|
||||
initMetadata : Metadata
|
||||
initMetadata = MkMetadata [] [] [] Nothing []
|
||||
|
||||
-- A label for metadata in the global state
|
||||
export
|
||||
data MD : Type where
|
||||
|
||||
TTC Metadata where
|
||||
toBuf b m
|
||||
= do toBuf b (lhsApps m)
|
||||
toBuf b (names m)
|
||||
toBuf b (tydecls m)
|
||||
toBuf b (holeLHS m)
|
||||
|
||||
fromBuf s b
|
||||
= do apps <- fromBuf s b
|
||||
ns <- fromBuf s b
|
||||
tys <- fromBuf s b
|
||||
hlhs <- fromBuf s b
|
||||
pure (MkMetadata apps ns tys Nothing hlhs)
|
||||
|
||||
export
|
||||
addLHS : {auto m : Ref MD Metadata} ->
|
||||
FC -> Nat -> Env Term vars -> Term vars -> Core ()
|
||||
addLHS loc outerenvlen env tm
|
||||
= do meta <- get MD
|
||||
put MD (record {
|
||||
lhsApps $= ((loc, outerenvlen, bindEnv loc (toPat env) tm) ::)
|
||||
} meta)
|
||||
where
|
||||
toPat : Env Term vs -> Env Term vs
|
||||
toPat (Lam c p ty :: bs) = PVar c ty :: toPat bs
|
||||
toPat (b :: bs) = b :: toPat bs
|
||||
toPat [] = []
|
||||
|
||||
export
|
||||
addNameType : {auto m : Ref MD Metadata} ->
|
||||
FC -> Name -> Env Term vars -> Term vars -> Core ()
|
||||
addNameType loc n env tm
|
||||
= do meta <- get MD
|
||||
put MD (record {
|
||||
names $= ((loc, (n, length env, bindEnv loc env tm)) ::)
|
||||
} meta)
|
||||
|
||||
export
|
||||
addTyDecl : {auto m : Ref MD Metadata} ->
|
||||
FC -> Name -> Env Term vars -> Term vars -> Core ()
|
||||
addTyDecl loc n env tm
|
||||
= do meta <- get MD
|
||||
put MD (record {
|
||||
tydecls $= ((loc, (n, length env, bindEnv loc env tm)) ::)
|
||||
} meta)
|
||||
|
||||
export
|
||||
setHoleLHS : {auto m : Ref MD Metadata} ->
|
||||
ClosedTerm -> Core ()
|
||||
setHoleLHS tm
|
||||
= do meta <- get MD
|
||||
put MD (record { currentLHS = Just tm } meta)
|
||||
|
||||
export
|
||||
clearHoleLHS : {auto m : Ref MD Metadata} ->
|
||||
Core ()
|
||||
clearHoleLHS
|
||||
= do meta <- get MD
|
||||
put MD (record { currentLHS = Nothing } meta)
|
||||
|
||||
export
|
||||
withCurrentLHS : {auto m : Ref MD Metadata} ->
|
||||
Name -> Core ()
|
||||
withCurrentLHS n
|
||||
= do meta <- get MD
|
||||
maybe (pure ())
|
||||
(\lhs => put MD (record { holeLHS $= ((n, lhs) ::) } meta))
|
||||
(currentLHS meta)
|
||||
|
||||
findEntryWith : (FC -> a -> Bool) -> List (FC, a) -> Maybe (FC, a)
|
||||
findEntryWith p [] = Nothing
|
||||
findEntryWith p ((l, x) :: xs)
|
||||
= if p l x
|
||||
then Just (l, x)
|
||||
else findEntryWith p xs
|
||||
|
||||
export
|
||||
findLHSAt : {auto m : Ref MD Metadata} ->
|
||||
(FC -> ClosedTerm -> Bool) ->
|
||||
Core (Maybe (FC, Nat, ClosedTerm))
|
||||
findLHSAt p
|
||||
= do meta <- get MD
|
||||
pure (findEntryWith (\ loc, tm => p loc (snd tm)) (lhsApps meta))
|
||||
|
||||
export
|
||||
findTypeAt : {auto m : Ref MD Metadata} ->
|
||||
(FC -> (Name, Nat, ClosedTerm) -> Bool) ->
|
||||
Core (Maybe (Name, Nat, ClosedTerm))
|
||||
findTypeAt p
|
||||
= do meta <- get MD
|
||||
pure (map snd (findEntryWith p (names meta)))
|
||||
|
||||
export
|
||||
findTyDeclAt : {auto m : Ref MD Metadata} ->
|
||||
(FC -> (Name, Nat, ClosedTerm) -> Bool) ->
|
||||
Core (Maybe (FC, Name, Nat, ClosedTerm))
|
||||
findTyDeclAt p
|
||||
= do meta <- get MD
|
||||
pure (findEntryWith p (tydecls meta))
|
||||
|
||||
export
|
||||
findHoleLHS : {auto m : Ref MD Metadata} ->
|
||||
Name -> Core (Maybe ClosedTerm)
|
||||
findHoleLHS hn
|
||||
= do meta <- get MD
|
||||
pure (lookupBy (\x, y => dropNS x == dropNS y) hn (holeLHS meta))
|
||||
|
||||
-- Normalise all the types of the names, since they might have had holes
|
||||
-- when added and the holes won't necessarily get saved
|
||||
normaliseTypes : {auto m : Ref MD Metadata} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
Core ()
|
||||
normaliseTypes
|
||||
= do meta <- get MD
|
||||
defs <- get Ctxt
|
||||
ns' <- traverse (nfType defs) (names meta)
|
||||
put MD (record { names = ns' } meta)
|
||||
where
|
||||
nfType : Defs -> (FC, (Name, Nat, ClosedTerm)) ->
|
||||
Core (FC, (Name, Nat, ClosedTerm))
|
||||
nfType defs (loc, (n, len, ty))
|
||||
= pure (loc, (n, len, !(normaliseHoles defs [] ty)))
|
||||
|
||||
record TTMFile where
|
||||
constructor MkTTMFile
|
||||
version : Int
|
||||
metadata : Metadata
|
||||
|
||||
TTC TTMFile where
|
||||
toBuf b file
|
||||
= do toBuf b "TTM"
|
||||
toBuf b (version file)
|
||||
toBuf b (metadata file)
|
||||
|
||||
fromBuf s b
|
||||
= do hdr <- fromBuf s b
|
||||
when (hdr /= "TTM") $ corrupt "TTM header"
|
||||
ver <- fromBuf s b
|
||||
checkTTCVersion ver ttcVersion
|
||||
md <- fromBuf s b
|
||||
pure (MkTTMFile ver md)
|
||||
|
||||
export
|
||||
writeToTTM : {auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
(fname : String) ->
|
||||
Core ()
|
||||
writeToTTM fname
|
||||
= do normaliseTypes
|
||||
buf <- initBinary
|
||||
meta <- get MD
|
||||
toBuf buf (MkTTMFile ttcVersion meta)
|
||||
Right ok <- coreLift $ writeToFile fname !(get Bin)
|
||||
| Left err => throw (InternalError (fname ++ ": " ++ show err))
|
||||
pure ()
|
||||
|
||||
-- The 'NameRefs' comes from the corresponding TTC file (so the assumption
|
||||
-- is that the TTM and TTC are in sync!)
|
||||
export
|
||||
readFromTTM : {auto m : Ref MD Metadata} ->
|
||||
NameRefs -> (fname : String) ->
|
||||
Core ()
|
||||
readFromTTM r fname
|
||||
= do Right buf <- coreLift $ readFromFile fname
|
||||
| Left err => throw (InternalError (fname ++ ": " ++ show err))
|
||||
bin <- newRef Bin buf
|
||||
ttm <- fromBuf r bin
|
||||
put MD (metadata ttm)
|
||||
|
@ -4,6 +4,7 @@ import Core.Context
|
||||
import Core.Core
|
||||
import Core.Env
|
||||
import Core.LinearCheck
|
||||
import Core.Metadata
|
||||
import Core.Normalise
|
||||
import Core.UnifyState
|
||||
import Core.Unify
|
||||
@ -23,6 +24,7 @@ getRigNeeded _ = Rig1
|
||||
export
|
||||
elabTermSub : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
Int -> ElabMode -> List ElabOpt ->
|
||||
NestedNames vars -> Env Term vars ->
|
||||
@ -112,6 +114,7 @@ elabTermSub defining mode opts nest env env' sub tm ty
|
||||
export
|
||||
elabTerm : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
Int -> ElabMode -> List ElabOpt ->
|
||||
NestedNames vars -> Env Term vars ->
|
||||
@ -123,6 +126,7 @@ elabTerm defining mode opts nest env tm ty
|
||||
export
|
||||
checkTermSub : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
Int -> ElabMode -> List ElabOpt ->
|
||||
NestedNames vars -> Env Term vars ->
|
||||
@ -138,6 +142,7 @@ checkTermSub defining mode opts nest env env' sub tm ty
|
||||
export
|
||||
checkTerm : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
Int -> ElabMode -> List ElabOpt ->
|
||||
NestedNames vars -> Env Term vars ->
|
||||
|
@ -3,6 +3,7 @@ module TTImp.Elab.Ambiguity
|
||||
import Core.Context
|
||||
import Core.Core
|
||||
import Core.Env
|
||||
import Core.Metadata
|
||||
import Core.Normalise
|
||||
import Core.Unify
|
||||
import Core.TT
|
||||
@ -238,6 +239,7 @@ getName _ = Nothing
|
||||
export
|
||||
checkAlternative : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
RigCount -> ElabInfo ->
|
||||
|
@ -4,6 +4,7 @@ import Core.CaseTree
|
||||
import Core.Context
|
||||
import Core.Core
|
||||
import Core.Env
|
||||
import Core.Metadata
|
||||
import Core.Normalise
|
||||
import Core.Unify
|
||||
import Core.TT
|
||||
@ -99,6 +100,7 @@ concrete defs env _ = pure False
|
||||
mutual
|
||||
makeImplicit : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
RigCount -> RigCount -> ElabInfo ->
|
||||
@ -126,6 +128,7 @@ mutual
|
||||
|
||||
makeAutoImplicit : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
RigCount -> RigCount -> ElabInfo ->
|
||||
@ -195,6 +198,7 @@ mutual
|
||||
-- disambiguation when elaborating the argument.
|
||||
checkRestApp : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
RigCount -> RigCount -> ElabInfo ->
|
||||
@ -272,6 +276,7 @@ mutual
|
||||
-- Returns the checked term and its (weakly) normalised type
|
||||
checkAppWith : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
RigCount -> ElabInfo ->
|
||||
@ -392,6 +397,7 @@ mutual
|
||||
export
|
||||
checkApp : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
RigCount -> ElabInfo ->
|
||||
|
@ -3,6 +3,7 @@ module TTImp.Elab.As
|
||||
import Core.Context
|
||||
import Core.Core
|
||||
import Core.Env
|
||||
import Core.Metadata
|
||||
import Core.Normalise
|
||||
import Core.Unify
|
||||
import Core.TT
|
||||
@ -19,6 +20,7 @@ import Data.NameMap
|
||||
export
|
||||
checkAs : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
RigCount -> ElabInfo ->
|
||||
|
@ -3,6 +3,7 @@ module TTImp.Elab.Binders
|
||||
import Core.Context
|
||||
import Core.Core
|
||||
import Core.Env
|
||||
import Core.Metadata
|
||||
import Core.Normalise
|
||||
import Core.Unify
|
||||
import Core.TT
|
||||
@ -29,6 +30,7 @@ dropName n nest = record { names $= drop } nest
|
||||
export
|
||||
checkPi : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
RigCount -> ElabInfo ->
|
||||
@ -59,6 +61,7 @@ findLamRig (Just expty)
|
||||
|
||||
inferLambda : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
RigCount -> ElabInfo ->
|
||||
@ -95,6 +98,7 @@ getTyNF env x
|
||||
export
|
||||
checkLambda : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
RigCount -> ElabInfo ->
|
||||
@ -140,16 +144,17 @@ weakenExp env (Just gtm)
|
||||
|
||||
export
|
||||
checkLet : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
RigCount -> ElabInfo ->
|
||||
NestedNames vars -> Env Term vars ->
|
||||
FC ->
|
||||
RigCount -> (n : Name) ->
|
||||
(nTy : RawImp) -> (nVal : RawImp) -> (scope : RawImp) ->
|
||||
(expTy : Maybe (Glued vars)) ->
|
||||
Core (Term vars, Glued 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 ->
|
||||
RigCount -> (n : Name) ->
|
||||
(nTy : RawImp) -> (nVal : RawImp) -> (scope : RawImp) ->
|
||||
(expTy : Maybe (Glued vars)) ->
|
||||
Core (Term vars, Glued vars)
|
||||
checkLet rigc_in elabinfo nest env fc rigl n nTy nVal scope expty
|
||||
= do let rigc = if rigc_in == Rig0 then Rig0 else Rig1
|
||||
(tyv, tyt) <- check Rig0 (nextLevel elabinfo) nest env nTy (Just (gType fc))
|
||||
|
@ -3,6 +3,7 @@ module TTImp.Elab.Case
|
||||
import Core.Context
|
||||
import Core.Core
|
||||
import Core.Env
|
||||
import Core.Metadata
|
||||
import Core.Normalise
|
||||
import Core.Unify
|
||||
import Core.TT
|
||||
@ -228,6 +229,7 @@ findScrutinee _ _ _ = Nothing
|
||||
export
|
||||
caseBlock : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
RigCount ->
|
||||
@ -402,6 +404,7 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
|
||||
export
|
||||
checkCase : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
RigCount -> ElabInfo ->
|
||||
|
@ -6,6 +6,7 @@ module TTImp.Elab.Check
|
||||
import Core.Context
|
||||
import Core.Core
|
||||
import Core.Env
|
||||
import Core.Metadata
|
||||
import Core.Normalise
|
||||
import Core.Unify
|
||||
import Core.UnifyState
|
||||
@ -305,24 +306,28 @@ bindingVars e
|
||||
export
|
||||
tryError : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
Core a -> Core (Either Error a)
|
||||
tryError elab
|
||||
= do ust <- get UST
|
||||
est <- get EST
|
||||
md <- get MD
|
||||
defs <- branch
|
||||
catch (do res <- elab
|
||||
commit
|
||||
pure (Right res))
|
||||
(\err => do put UST ust
|
||||
put EST est
|
||||
put MD md
|
||||
put Ctxt defs
|
||||
pure (Left err))
|
||||
|
||||
export
|
||||
try : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
Core a -> Core a -> Core a
|
||||
@ -334,6 +339,7 @@ try elab1 elab2
|
||||
export
|
||||
handle : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
Core a -> (Error -> Core a) -> Core a
|
||||
@ -344,6 +350,7 @@ handle elab1 elab2
|
||||
|
||||
successful : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
List (Maybe Name, Core a) ->
|
||||
@ -353,21 +360,26 @@ successful [] = pure []
|
||||
successful ((tm, elab) :: elabs)
|
||||
= do ust <- get UST
|
||||
est <- get EST
|
||||
md <- get MD
|
||||
defs <- branch
|
||||
catch (do -- Run the elaborator
|
||||
res <- elab
|
||||
-- Record post-elaborator state
|
||||
ust' <- get UST
|
||||
est' <- get EST
|
||||
md' <- get MD
|
||||
defs' <- get Ctxt
|
||||
-- Reset to previous state and try the rest
|
||||
put UST ust
|
||||
put EST est
|
||||
put MD md
|
||||
put Ctxt defs
|
||||
elabs' <- successful elabs
|
||||
-- Record success, and the state we ended at
|
||||
pure (Right (res, defs', ust', est') :: elabs'))
|
||||
(\err => do put UST ust
|
||||
put EST est
|
||||
put MD md
|
||||
put Ctxt defs
|
||||
elabs' <- successful elabs
|
||||
pure (Left (tm, err) :: elabs'))
|
||||
@ -375,6 +387,7 @@ successful ((tm, elab) :: elabs)
|
||||
export
|
||||
exactlyOne : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
FC -> Env Term vars ->
|
||||
@ -406,6 +419,7 @@ exactlyOne {vars} fc env all
|
||||
export
|
||||
anyOne : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
FC -> List (Maybe Name, Core (Term vars, Glued vars)) ->
|
||||
@ -419,6 +433,7 @@ anyOne fc ((tm, elab) :: es) = try elab (anyOne fc es)
|
||||
export
|
||||
check : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
RigCount -> ElabInfo ->
|
||||
@ -430,6 +445,7 @@ check : {vars : _} ->
|
||||
export
|
||||
checkImp : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
RigCount -> ElabInfo ->
|
||||
@ -440,6 +456,7 @@ checkImp : {vars : _} ->
|
||||
export
|
||||
processDecl : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
List ElabOpt -> NestedNames vars ->
|
||||
Env Term vars -> ImpDecl -> Core ()
|
||||
|
@ -4,6 +4,7 @@ import Core.CaseTree
|
||||
import Core.Context
|
||||
import Core.Core
|
||||
import Core.Env
|
||||
import Core.Metadata
|
||||
import Core.Normalise
|
||||
import Core.Unify
|
||||
import Core.TT
|
||||
@ -43,6 +44,7 @@ mkClosedElab {vars = x :: vars} fc (b :: env) elab
|
||||
-- have been resolved
|
||||
export
|
||||
delayOnFailure : {auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
FC -> RigCount -> Env Term vars ->
|
||||
|
@ -3,6 +3,7 @@ module TTImp.Elab.Dot
|
||||
import Core.Context
|
||||
import Core.Core
|
||||
import Core.Env
|
||||
import Core.Metadata
|
||||
import Core.Normalise
|
||||
import Core.Unify
|
||||
import Core.TT
|
||||
@ -19,6 +20,7 @@ import Data.NameMap
|
||||
export
|
||||
checkDot : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
RigCount -> ElabInfo ->
|
||||
|
@ -5,6 +5,7 @@ module TTImp.Elab.ImplicitBind
|
||||
import Core.Context
|
||||
import Core.Core
|
||||
import Core.Env
|
||||
import Core.Metadata
|
||||
import Core.Normalise
|
||||
import Core.Unify
|
||||
import Core.TT
|
||||
@ -54,7 +55,7 @@ mutual
|
||||
export
|
||||
mkOuterHole : {auto e : Ref EST (EState vars)} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto e : Ref UST UState} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
FC -> RigCount ->
|
||||
Name -> Env Term vars -> Maybe (Glued vars) ->
|
||||
Core (Term vars, Term vars)
|
||||
@ -88,7 +89,7 @@ mkOuterHole loc rig n topenv Nothing
|
||||
export
|
||||
mkPatternHole : {auto e : Ref EST (EState vars)} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto e : Ref UST UState} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
FC -> RigCount -> Name -> Env Term vars -> BindMode ->
|
||||
Maybe (Glued vars) ->
|
||||
Core (Term vars, Term vars, Term vars)
|
||||
@ -403,6 +404,7 @@ getToBind {vars} fc elabmode impmode env excepts toptm
|
||||
export
|
||||
checkBindVar : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
RigCount -> ElabInfo ->
|
||||
@ -470,6 +472,7 @@ checkBindVar rig elabinfo nest env fc str topexp
|
||||
export
|
||||
checkBindHere : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
RigCount -> ElabInfo ->
|
||||
|
@ -3,6 +3,7 @@ module TTImp.Elab.Lazy
|
||||
import Core.Context
|
||||
import Core.Core
|
||||
import Core.Env
|
||||
import Core.Metadata
|
||||
import Core.Normalise
|
||||
import Core.Unify
|
||||
import Core.TT
|
||||
@ -17,6 +18,7 @@ import TTImp.TTImp
|
||||
export
|
||||
checkDelayed : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
RigCount -> ElabInfo ->
|
||||
@ -30,6 +32,7 @@ checkDelayed rig elabinfo nest env fc r tm exp
|
||||
export
|
||||
checkDelay : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
RigCount -> ElabInfo ->
|
||||
@ -67,6 +70,7 @@ checkDelay rig elabinfo nest env fc tm mexpected
|
||||
export
|
||||
checkForce : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
RigCount -> ElabInfo ->
|
||||
|
@ -3,6 +3,7 @@ module TTImp.Elab.Local
|
||||
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
|
||||
checkLocal : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
RigCount -> ElabInfo ->
|
||||
|
@ -3,6 +3,7 @@ module TTImp.Elab.Record
|
||||
import Core.Context
|
||||
import Core.Core
|
||||
import Core.Env
|
||||
import Core.Metadata
|
||||
import Core.Normalise
|
||||
import Core.Unify
|
||||
import Core.TT
|
||||
@ -160,6 +161,7 @@ recUpdate rigc elabinfo loc nest env flds rec grecty
|
||||
export
|
||||
checkUpdate : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
RigCount -> ElabInfo ->
|
||||
|
@ -4,6 +4,7 @@ import Core.Context
|
||||
import Core.Core
|
||||
import Core.Env
|
||||
import Core.GetType
|
||||
import Core.Metadata
|
||||
import Core.Normalise
|
||||
import Core.Unify
|
||||
import Core.TT
|
||||
@ -86,6 +87,7 @@ elabRewrite loc env expected rulety
|
||||
export
|
||||
checkRewrite : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
RigCount -> ElabInfo ->
|
||||
|
@ -3,6 +3,7 @@ module TTImp.Elab.Term
|
||||
import Core.Context
|
||||
import Core.Core
|
||||
import Core.Env
|
||||
import Core.Metadata
|
||||
import Core.Normalise
|
||||
import Core.Unify
|
||||
import Core.TT
|
||||
@ -77,6 +78,7 @@ insertImpLam env tm _ = pure tm
|
||||
-- Implements 'checkImp' in TTImp.Elab.Check
|
||||
checkTerm : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
{auto e : Ref EST (EState vars)} ->
|
||||
RigCount -> ElabInfo ->
|
||||
@ -177,6 +179,7 @@ checkTerm rig elabinfo nest env (Implicit fc b) Nothing
|
||||
-- Declared in TTImp.Elab.Check
|
||||
-- check : {vars : _} ->
|
||||
-- {auto c : Ref Ctxt Defs} ->
|
||||
-- {auto m : Ref MD Metadata} ->
|
||||
-- {auto u : Ref UST UState} ->
|
||||
-- {auto e : Ref EST (EState vars)} ->
|
||||
-- RigCount -> ElabInfo -> Env Term vars -> RawImp ->
|
||||
@ -207,6 +210,7 @@ TTImp.Elab.Check.check rigc elabinfo nest env tm_in exp
|
||||
-- As above, but doesn't add any implicit lambdas, forces, delays, etc
|
||||
-- checkImp : {vars : _} ->
|
||||
-- {auto c : Ref Ctxt Defs} ->
|
||||
-- {auto m : Ref MD Metadata} ->
|
||||
-- {auto u : Ref UST UState} ->
|
||||
-- {auto e : Ref EST (EState vars)} ->
|
||||
-- RigCount -> ElabInfo -> Env Term vars -> RawImp -> Maybe (Glued vars) ->
|
||||
|
@ -3,6 +3,7 @@ module TTImp.ProcessData
|
||||
import Core.Context
|
||||
import Core.Core
|
||||
import Core.Env
|
||||
import Core.Metadata
|
||||
import Core.Normalise
|
||||
import Core.UnifyState
|
||||
import Core.Value
|
||||
@ -49,6 +50,7 @@ checkFamily loc cn tn env nf
|
||||
|
||||
checkCon : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
List ElabOpt -> NestedNames vars ->
|
||||
Env Term vars -> Visibility -> Name ->
|
||||
@ -81,6 +83,7 @@ conName (MkCon _ cn _ _) = cn
|
||||
export
|
||||
processData : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
List ElabOpt -> NestedNames vars ->
|
||||
Env Term vars -> FC -> Visibility ->
|
||||
|
@ -3,6 +3,7 @@ module TTImp.ProcessDecls
|
||||
import Core.Context
|
||||
import Core.Core
|
||||
import Core.Env
|
||||
import Core.Metadata
|
||||
import Core.UnifyState
|
||||
|
||||
import Parser.Support
|
||||
@ -18,6 +19,7 @@ import TTImp.TTImp
|
||||
-- Implements processDecl, declared in TTImp.Elab.Check
|
||||
process : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
List ElabOpt ->
|
||||
NestedNames vars -> Env Term vars -> ImpDecl -> Core ()
|
||||
@ -46,6 +48,7 @@ TTImp.Elab.Check.processDecl = process
|
||||
export
|
||||
processDecls : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
NestedNames vars -> Env Term vars -> List ImpDecl -> Core Bool
|
||||
processDecls nest env decls
|
||||
@ -54,6 +57,7 @@ processDecls nest env decls
|
||||
|
||||
export
|
||||
processTTImpFile : {auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
String -> Core Bool
|
||||
processTTImpFile fname
|
||||
|
@ -5,6 +5,7 @@ import Core.CaseTree
|
||||
import Core.Context
|
||||
import Core.Core
|
||||
import Core.Env
|
||||
import Core.Metadata
|
||||
import Core.Normalise
|
||||
import Core.Value
|
||||
import Core.UnifyState
|
||||
@ -137,6 +138,7 @@ combineLinear loc ((n, count) :: cs)
|
||||
export
|
||||
checkLHS : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
(mult : RigCount) -> (hashit : Bool) ->
|
||||
Int -> List ElabOpt -> NestedNames vars -> Env Term vars ->
|
||||
@ -217,6 +219,7 @@ getNotReq _ (KeepCons p) = getNotReq _ p
|
||||
export
|
||||
checkClause : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
(mult : RigCount) -> (hashit : Bool) ->
|
||||
Int -> List ElabOpt -> NestedNames vars -> Env Term vars ->
|
||||
@ -259,6 +262,8 @@ checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw cs
|
||||
| Nothing => throw (InternalError "Impossible happened: With abstraction failure #1")
|
||||
let Just wvalTy = shrinkTerm wvalTy withSub
|
||||
| Nothing => throw (InternalError "Impossible happened: With abstraction failure #2")
|
||||
-- Should the env be normalised too? If the following 'impossible'
|
||||
-- error is ever thrown, that might be the cause!
|
||||
let Just wvalEnv = shrinkEnv env' withSub
|
||||
| Nothing => throw (InternalError "Impossible happened: With abstraction failure #3")
|
||||
|
||||
@ -400,6 +405,7 @@ toPats (MkClause {vars} env lhs rhs)
|
||||
|
||||
export
|
||||
processDef : {auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
List ElabOpt -> NestedNames vars -> Env Term vars -> FC ->
|
||||
Name -> List ImpClause -> Core ()
|
||||
|
@ -3,6 +3,7 @@ module TTImp.ProcessType
|
||||
import Core.Context
|
||||
import Core.Core
|
||||
import Core.Env
|
||||
import Core.Metadata
|
||||
import Core.Normalise
|
||||
import Core.TT
|
||||
import Core.UnifyState
|
||||
@ -47,6 +48,7 @@ processFnOpt fc ndef PartialOK
|
||||
export
|
||||
processType : {vars : _} ->
|
||||
{auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
List ElabOpt -> NestedNames vars -> Env Term vars ->
|
||||
FC -> RigCount -> Visibility ->
|
||||
|
@ -8,6 +8,7 @@ import Core.Directory
|
||||
import Core.Env
|
||||
import Core.FC
|
||||
import Core.InitPrimitives
|
||||
import Core.Metadata
|
||||
import Core.Normalise
|
||||
import Core.Options
|
||||
import Core.TT
|
||||
@ -35,6 +36,7 @@ coreMain : String -> List String -> Core ()
|
||||
coreMain fname args
|
||||
= do defs <- initDefs
|
||||
c <- newRef Ctxt defs
|
||||
m <- newRef MD initMetadata
|
||||
u <- newRef UST initUState
|
||||
d <- getDirs
|
||||
t <- processArgs args
|
||||
|
@ -5,6 +5,7 @@ import Core.Context
|
||||
import Core.Core
|
||||
import Core.Env
|
||||
import Core.FC
|
||||
import Core.Metadata
|
||||
import Core.Normalise
|
||||
import Core.TT
|
||||
import Core.Unify
|
||||
@ -28,6 +29,7 @@ showInfo (n, d) = coreLift $ putStrLn (show n ++ " ==> " ++ show d)
|
||||
|
||||
-- Returns 'True' if the REPL should continue
|
||||
process : {auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
ImpREPL -> Core Bool
|
||||
process (Eval ttimp)
|
||||
@ -74,6 +76,7 @@ process Quit
|
||||
pure False
|
||||
|
||||
processCatch : {auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
ImpREPL -> Core Bool
|
||||
processCatch cmd
|
||||
@ -83,6 +86,7 @@ processCatch cmd
|
||||
|
||||
export
|
||||
repl : {auto c : Ref Ctxt Defs} ->
|
||||
{auto m : Ref MD Metadata} ->
|
||||
{auto u : Ref UST UState} ->
|
||||
Core ()
|
||||
repl
|
||||
|
@ -15,6 +15,7 @@ modules =
|
||||
Core.GetType,
|
||||
Core.Hash,
|
||||
Core.LinearCheck,
|
||||
Core.Metadata,
|
||||
Core.Name,
|
||||
Core.Normalise,
|
||||
Core.Options,
|
||||
|
Loading…
Reference in New Issue
Block a user