module Core.Context import        Core.CaseTreeimport        Core.CompileExprimport public Core.Coreimport        Core.Envimport        Core.Hashimport public Core.Nameimport        Core.Optionsimport public Core.TT import Utils.Binary import Data.IOArrayimport Data.NameMapimport Data.StringMapimport Data.IntMap import System %default covering public exportdata HoleInfo        = NotHole        | SolvedHole Nat public exportrecord PMDefInfo where  constructor MkPMDefInfo  holeInfo : HoleInfo -- data if it comes from a solved hole  alwaysReduce : Bool -- always reduce, even when quoting etc                 -- typically for inlinable metavariable solutions exportdefaultPI : PMDefInfodefaultPI = MkPMDefInfo NotHole False public exportrecord TypeFlags where  constructor MkTypeFlags  uniqueAuto : Bool  -- should 'auto' implicits check for uniqueness  external : Bool -- defined externally (e.g. in a C or Scheme library) exportdefaultFlags : TypeFlagsdefaultFlags = MkTypeFlags False False public exportdata Def : Type where    None : Def -- Not yet defined    PMDef : (pminfo : PMDefInfo) ->            (args : List Name) ->            (treeCT : CaseTree args) ->            (treeRT : CaseTree args) ->            (pats : List (vs ** (Env Term vs, Term vs, Term vs))) ->                -- original checked patterns (LHS/RHS) with the names in                -- the environment. Used for display purposes, for helping                -- find size changes in termination checking, and for                -- generating specialised definitions (so needs to be the                -- full, non-erased, term)            Def -- Ordinary function definition    ExternDef : (arity : Nat) -> Def    ForeignDef : (arity : Nat) ->                 List String -> -- supported calling conventions,                                -- e.g "C:printf,libc,stdlib.h", "scheme:display", ...                 Def    Builtin : {arity : Nat} -> PrimFn arity -> Def    DCon : (tag : Int) -> (arity : Nat) ->           (newtypeArg : Maybe (Bool, Nat)) ->               -- if only constructor, and only one argument is non-Rig0,               -- flag it here. The Nat is the unerased argument position.               -- The Bool is 'True' if there is no %World token in the               -- structure, which means it is safe to completely erase               -- when pattern matching (otherwise we still have to ensure               -- that the value is inspected, to make sure external effects               -- happen)           Def -- data constructor    TCon : (tag : Int) -> (arity : Nat) ->           (parampos : List Nat) -> -- parameters           (detpos : List Nat) -> -- determining arguments           (flags : TypeFlags) -> -- should 'auto' implicits check           (mutwith : List Name) ->           (datacons : List Name) ->           (detagabbleBy : Maybe (List Nat)) ->                    -- argument positions which can be used for                    -- detagging, if it's possible (to check if it's                    -- safe to erase)           Def    Hole : (numlocs : Nat) -> -- Number of locals in scope at binding point                              -- (mostly to help display)           (implbind : Bool) -> -- Does this stand for an implicitly bound name           Def    BySearch : RigCount -> (maxdepth : Nat) -> (defining : Name) -> Def    -- Constraints are integer references into the current map of    -- constraints in the UnifyState (see Core.UnifyState)    Guess : (guess : ClosedTerm) ->            (envbind : Nat) -> -- Number of things in the environment when                               -- we guessed the term            (constraints : List Int) -> Def    ImpBind : Def -- global name temporarily standing for an implicitly bound name    -- A delayed elaboration. The elaborators themselves are stored in the    -- unifiation state    Delayed : Def exportShow Def where  show None = "undefined"  show (PMDef _ args ct rt pats)      = show args ++ ";\nCompile time tree: " ++ show ct ++        "\nRun time tree: " ++ show rt  show (DCon t a nt)      = "DataCon " ++ show t ++ " " ++ show a           ++ maybe "" (\n => " (newtype by " ++ show n ++ ")") nt  show (TCon t a ps ds u ms cons det)      = "TyCon " ++ show t ++ " " ++ show a ++ " params: " ++ show ps ++        " constructors: " ++ show cons ++        " mutual with: " ++ show ms ++        " detaggable by: " ++ show det  show (ExternDef arity) = "<external def with arity " ++ show arity ++ ">"  show (ForeignDef a cs) = "<foreign def with arity " ++ show a ++                           " " ++ show cs ++">"  show (Builtin {arity} _) = "<builtin with arith " ++ show arity ++ ">"  show (Hole _ p) = "Hole" ++ if p then " [impl]" else ""  show (BySearch c depth def) = "Search in " ++ show def  show (Guess tm _ cs) = "Guess " ++ show tm ++ " when " ++ show cs  show ImpBind = "Bound name"  show Delayed = "Delayed" public exportrecord Constructor where  constructor MkCon  loc : FC  name : Name  arity : Nat  type : ClosedTerm public exportdata DataDef : Type where     MkData : (tycon : Constructor) -> (datacons : List Constructor) ->              DataDef public exportdata Clause : Type where     MkClause : (env : Env Term vars) ->                (lhs : Term vars) -> (rhs : Term vars) -> Clause public exportdata DefFlag    = Inline    | Invertible -- assume safe to cancel arguments in unification    | Overloadable -- allow ad-hoc overloads    | TCInline -- always inline before totality checking         -- (in practice, this means it's reduced in 'normaliseHoles')         -- This means the function gets inlined when calculating the size         -- change graph, but otherwise not. It's only safe if the function         -- being inlined is terminating no matter what, and is really a bit         -- of a hack to make sure interface dictionaries are properly inlined         -- (otherwise they look potentially non terminating) so use with         -- care!    | SetTotal TotalReq    | BlockedHint -- a hint, but blocked for the moment (so don't use)    | Macro    | PartialEval (List (Name, Nat)) -- Partially evaluate on completing defintion.         -- This means the definition is standing for a specialisation so we         -- should evaluate the RHS, with reduction limits on the given names,         -- and ensure the name has made progress in doing so (i.e. has reduced         -- at least once) exportEq DefFlag where    (==) Inline Inline = True    (==) Invertible Invertible = True    (==) Overloadable Overloadable = True    (==) TCInline TCInline = True    (==) (SetTotal x) (SetTotal y) = x == y    (==) BlockedHint BlockedHint = True    (==) Macro Macro = True    (==) (PartialEval x) (PartialEval y) = x == y    (==) _ _ = False public exportdata SizeChange = Smaller | Same | Unknown exportShow SizeChange where  show Smaller = "Smaller"  show Same = "Same"  show Unknown = "Unknown" public exportrecord SCCall where     constructor MkSCCall     fnCall : Name -- Function called     fnArgs : List (Maybe (Nat, SizeChange))        -- relationship to arguments of calling function; argument position        -- (in the calling function), and how its size changed in the call.        -- 'Nothing' if it's not related to any of the calling function's        -- arguments exportShow SCCall where  show c = show (fnCall c) ++ ": " ++ show (fnArgs c) public exportrecord GlobalDef where  constructor MkGlobalDef  location : FC  fullname : Name -- original unresolved name  type : ClosedTerm  eraseArgs : List Nat -- which argument positions to erase at runtime  safeErase : List Nat -- which argument positions are safe to assume                       -- erasable without 'dotting', because their types                       -- are collapsible relative to non-erased arguments  specArgs : List Nat -- arguments to specialise by  inferrable : List Nat -- arguments which can be inferred from elsewhere in the type  multiplicity : RigCount  vars : List Name -- environment name is defined in  visibility : Visibility  totality : Totality  flags : List DefFlag  refersToM : Maybe (NameMap Bool)  refersToRuntimeM : Maybe (NameMap Bool)  invertible : Bool -- for an ordinary definition, is it invertible in unification  noCycles : Bool -- for metavariables, whether they can be cyclic (this                  -- would only be allowed when using a metavariable as a                  -- placeholder for a yet to be elaborated arguments, but                  -- not for implicits because that'd indicate failing the                  -- occurs check)  linearChecked : Bool -- Flag whether we've already checked its linearity  definition : Def  compexpr : Maybe CDef  namedcompexpr : Maybe NamedDef  sizeChange : List SCCall exportrefersTo : GlobalDef -> NameMap BoolrefersTo def = maybe empty id (refersToM def) exportrefersToRuntime : GlobalDef -> NameMap BoolrefersToRuntime def = maybe empty id (refersToRuntimeM def) -- Label for array referencesexportdata Arr : Type where -- A context entry. If it's never been looked up, we haven't decoded the-- binary blob yet, so decode it first timepublic exportdata ContextEntry : Type where     Coded : Binary -> ContextEntry     Decoded : GlobalDef -> ContextEntry -- All the GlobalDefs. We can only have one context, because name references-- point at locations in here, and if we have more than one the indices won't-- match up. So, this isn't polymorphic.exportrecord Context where    constructor MkContext    firstEntry : Int -- First entry in the current source file    nextEntry : Int    -- Map from full name to its position in the context    resolvedAs : NameMap Int    -- Map from strings to all the possible names in all namespaces    possibles : StringMap (List (Name, Int))    -- Reference to the actual content, indexed by Int    content : Ref Arr (IOArray ContextEntry)    -- Branching depth, in a backtracking elaborator. 0 is top level; at lower    -- levels we need to stage updates rather than add directly to the    -- 'content' store    branchDepth : Nat    -- Things which we're going to add, if this branch succeeds    staging : IntMap ContextEntry     -- Namespaces which are visible (i.e. have been imported)    -- This only matters during evaluation and type checking, to control    -- access in a program - in all other cases, we'll assume everything is    -- visible    visibleNS : List (List String)    allPublic : Bool -- treat everything as public. This is only intended                     -- for checking partially evaluated definitions    inlineOnly : Bool -- only return things with the 'alwaysReduce' flag exportgetContent : Context -> Ref Arr (IOArray ContextEntry)getContent = content -- Implemented later, once we can convert to and from full names-- Defined in Core.TTCexportdecode : Context -> Int -> (update : Bool) -> ContextEntry -> Core GlobalDef initSize : IntinitSize = 10000 Grow : IntGrow = initSize exportinitCtxtS : Int -> Core ContextinitCtxtS s    = do arr <- coreLift $ newArray s         aref <- newRef Arr arr         pure (MkContext 0 0 empty empty aref 0 empty [["_PE"]] False False) exportinitCtxt : Core ContextinitCtxt = initCtxtS initSize addPossible : Name -> Int ->              StringMap (List (Name, Int)) -> StringMap (List (Name, Int))addPossible n i ps    = case userNameRoot n of           Nothing => ps           Just nr =>              case lookup nr ps of                   Nothing => insert nr [(n, i)] ps                   Just nis => insert nr ((n, i) :: nis) ps exportnewEntry : Name -> Context -> Core (Int, Context)newEntry n ctxt    = do let idx = nextEntry ctxt         let a = content ctxt         arr <- get Arr         when (idx >= max arr) $                 do arr' <- coreLift $ newArrayCopy (max arr + Grow) arr                    put Arr arr'         pure (idx, record { nextEntry = idx + 1,                             resolvedAs $= insert n idx,                             possibles $= addPossible n idx                           } ctxt) -- Get the position of the next entry in the context array, growing the-- array if it's out of bounds.-- Updates the context with the mapping from name to indexexportgetPosition : Name -> Context -> Core (Int, Context)getPosition (Resolved idx) ctxt = pure (idx, ctxt)getPosition n ctxt    = case lookup n (resolvedAs ctxt) of           Just idx =>              do pure (idx, ctxt)           Nothing => newEntry n ctxt exportgetNameID : Name -> Context -> Maybe IntgetNameID (Resolved idx) ctxt = Just idxgetNameID n ctxt = lookup n (resolvedAs ctxt) -- Add the name to the context, or update the existing entry if it's already-- there.-- If we're not at the top level, add it to the staging areaexportaddCtxt : Name -> GlobalDef -> Context -> Core (Int, Context)addCtxt n val ctxt_in    = if branchDepth ctxt_in == 0         then do (idx, ctxt) <- getPosition n ctxt_in                 let a = content ctxt                 arr <- get Arr                 coreLift $ writeArray arr idx (Decoded val)                 pure (idx, ctxt)         else do (idx, ctxt) <- getPosition n ctxt_in                 pure (idx, record { staging $= insert idx (Decoded val) } ctxt) exportaddEntry : Name -> ContextEntry -> Context -> Core (Int, Context)addEntry n entry ctxt_in    = if branchDepth ctxt_in == 0         then do (idx, ctxt) <- getPosition n ctxt_in                 let a = content ctxt                 arr <- get Arr                 coreLift $ writeArray arr idx entry                 pure (idx, ctxt)         else do (idx, ctxt) <- getPosition n ctxt_in                 pure (idx, record { staging $= insert idx entry } ctxt) returnDef : Bool -> Int -> GlobalDef -> Maybe (Int, GlobalDef)returnDef False idx def = Just (idx, def)returnDef True idx def    = case definition def of           PMDef pi _ _ _ _ =>                 if alwaysReduce pi                    then Just (idx, def)                    else Nothing           _ => Nothing exportlookupCtxtExactI : Name -> Context -> Core (Maybe (Int, GlobalDef))lookupCtxtExactI (Resolved idx) ctxt    = case lookup idx (staging ctxt) of           Just val =>                 pure $ returnDef (inlineOnly ctxt) idx !(decode ctxt idx True val)           Nothing =>              do let a = content ctxt                 arr <- get Arr                 Just def <- coreLift (readArray arr idx)                      | Nothing => pure Nothing                 pure $ returnDef (inlineOnly ctxt) idx !(decode ctxt idx True def)lookupCtxtExactI n ctxt    = do let Just idx = lookup n (resolvedAs ctxt)                  | Nothing => pure Nothing         lookupCtxtExactI (Resolved idx) ctxt exportlookupCtxtExact : Name -> Context -> Core (Maybe GlobalDef)lookupCtxtExact (Resolved idx) ctxt    = case lookup idx (staging ctxt) of           Just res =>                do def <- decode ctxt idx True res                   case returnDef (inlineOnly ctxt) idx def of                        Nothing => pure Nothing                        Just (_, def) => pure (Just def)           Nothing =>              do let a = content ctxt                 arr <- get Arr                 Just res <- coreLift (readArray arr idx)                      | Nothing => pure Nothing                 def <- decode ctxt idx True res                 case returnDef (inlineOnly ctxt) idx def of                      Nothing => pure Nothing                      Just (_, def) => pure (Just def)lookupCtxtExact n ctxt    = do Just (i, def) <- lookupCtxtExactI n ctxt              | Nothing => pure Nothing         pure (Just def) exportlookupContextEntry : Name -> Context -> Core (Maybe (Int, ContextEntry))lookupContextEntry (Resolved idx) ctxt    = case lookup idx (staging ctxt) of           Just res => pure (Just (idx, res))           Nothing =>              do let a = content ctxt                 arr <- get Arr                 Just res <- coreLift (readArray arr idx)                      | Nothing => pure Nothing                 pure (Just (idx, res))lookupContextEntry n ctxt    = do let Just idx = lookup n (resolvedAs ctxt)                  | Nothing => pure Nothing         lookupContextEntry (Resolved idx) ctxt exportlookupCtxtName : Name -> Context -> Core (List (Name, Int, GlobalDef))lookupCtxtName n ctxt    = case userNameRoot n of           Nothing => do Just (i, res) <- lookupCtxtExactI n ctxt                              | Nothing => pure []                         pure [(n, i, res)]           Just r =>              do let Just ps = lookup r (possibles ctxt)                      | Nothing => pure []                 ps' <- the (Core (List (Maybe (Name, Int, GlobalDef)))) $                           traverse (\ (n, i) =>                                    do Just res <- lookupCtxtExact (Resolved i) ctxt                                            | pure Nothing                                       pure (Just (n, i, res))) ps                 getMatches ps'  where    matches : Name -> (Name, Int, a) -> Bool    matches (NS ns _) (NS cns _, _, _) = ns `isPrefixOf` cns    matches (NS _ _) _ = True -- no in library name, so root doesn't match    matches _ _ = True -- no prefix, so root must match, so good     getMatches : List (Maybe (Name, Int, GlobalDef)) ->                 Core (List (Name, Int, GlobalDef))    getMatches [] = pure []    getMatches (Nothing :: rs) = getMatches rs    getMatches (Just r :: rs)        = if matches n r             then do rs' <- getMatches rs                     pure (r :: rs')             else getMatches rs branchCtxt : Context -> Core ContextbranchCtxt ctxt = pure (record { branchDepth $= S } ctxt) commitCtxt : Context -> Core ContextcommitCtxt ctxt    = case branchDepth ctxt of           Z => pure ctxt           S Z => -- add all the things from 'staging' to the real array                  do let a = content ctxt                     arr <- get Arr                     coreLift $ commitStaged (toList (staging ctxt)) arr                     pure (record { staging = empty,                                    branchDepth = Z } ctxt)           S k => pure (record { branchDepth = k } ctxt)  where    -- We know the array must be big enough, because it will have been resized    -- if necessary in the branch to fit the index we've been given here    commitStaged : List (Int, ContextEntry) -> IOArray ContextEntry -> IO ()    commitStaged [] arr = pure ()    commitStaged ((idx, val) :: rest) arr        = do writeArray arr idx val             commitStaged rest arr export

Lines 1–500 of 2281. Load more