module Core.UnifyState import Core.CaseTreeimport Core.Contextimport Core.Coreimport Core.Envimport Core.FCimport Core.Normaliseimport Core.Optionsimport Core.TTimport Core.TTCimport Utils.Binary import Data.IntMapimport Data.NameMapimport Data.StringMap %default covering public exportdata Constraint : Type where     -- An unsolved constraint, noting two terms which need to be convertible     -- in a particular environment     MkConstraint : {vars : _} ->                    FC ->                    (withLazy : Bool) ->                    (blockedOn : List Name) ->                    (env : Env Term vars) ->                    (x : Term vars) -> (y : Term vars) ->                    Constraint     -- An unsolved sequence of constraints, arising from arguments in an     -- application where solving later constraints relies on solving earlier     -- ones     MkSeqConstraint : {vars : _} ->                       FC ->                       (env : Env Term vars) ->                       (xs : List (Term vars)) ->                       (ys : List (Term vars)) ->                       Constraint     -- A resolved constraint     Resolved : Constraint exportTTC Constraint where  toBuf b (MkConstraint {vars} fc l block env x y)     = do tag 0; toBuf b vars; toBuf b l          toBuf b block          toBuf b fc; toBuf b env; toBuf b x; toBuf b y  toBuf b (MkSeqConstraint {vars} fc env xs ys)     = do tag 1; toBuf b vars; toBuf b fc; toBuf b env; toBuf b xs; toBuf b ys  toBuf b Resolved = tag 2   fromBuf b      = case !getTag of             0 => do vars <- fromBuf b                     fc <- fromBuf b; l <- fromBuf b                     block <- fromBuf b                     env <- fromBuf b                     x <- fromBuf b; y <- fromBuf b                     pure (MkConstraint {vars} fc l block env x y)             1 => do vars <- fromBuf b                     fc <- fromBuf b; env <- fromBuf b                     xs <- fromBuf b; ys <- fromBuf b                     pure (MkSeqConstraint {vars} fc env xs ys)             2 => pure Resolved             _ => corrupt "Constraint" public exportrecord UState where  constructor MkUState  holes : IntMap (FC, Name) -- All metavariables with no definition yet.                            -- 'Int' is the 'Resolved' name  guesses : IntMap (FC, Name) -- Names which will be defined when constraints solved                              -- (also includes auto implicit searches)  currentHoles : IntMap (FC, Name) -- Holes introduced this elaboration session  delayedHoles : IntMap (FC, Name) -- Holes left unsolved after an elaboration,                                   -- so we need to check again at the end whether                                   -- they have been solved later. Doesn't include                                   -- user defined hole names, which don't need                                   -- to have been solved  constraints : IntMap Constraint -- map for finding constraints by ID  dotConstraints : List (Name, DotReason, Constraint) -- dot pattern constraints  nextName : Int  nextConstraint : Int  delayedElab : List (Nat, Int, Core ClosedTerm)                -- Elaborators which we need to try again later, because                -- we didn't have enough type information to elaborate                -- successfully yet.                -- 'Nat' is the priority (lowest first)                -- The 'Int' is the resolved name. Delays can't be nested,                -- so we just process them in order.  logging : Bool exportinitUState : UStateinitUState = MkUState empty empty empty empty empty [] 0 0 [] False exportdata UST : Type where exportresetNextVar : {auto u : Ref UST UState} ->               Core ()resetNextVar    = do ust <- get UST         put UST (record { nextName = 0 } ust) -- Generate a global name based on the given root, in the current namespaceexportgenName : {auto c : Ref Ctxt Defs} ->          {auto u : Ref UST UState} ->          String -> Core NamegenName str    = do ust <- get UST         put UST (record { nextName $= (+1) } ust)         n <- inCurrentNS (MN str (nextName ust))         pure n -- Generate a global name based on the given name, in the current namespaceexportgenMVName : {auto c : Ref Ctxt Defs} ->            {auto u : Ref UST UState} ->            Name -> Core NamegenMVName (UN str) = genName strgenMVName (MN str _) = genName strgenMVName n    = do ust <- get UST         put UST (record { nextName $= (+1) } ust)         mn <- inCurrentNS (MN (show n) (nextName ust))         pure mn -- Generate a unique variable name based on the given rootexportgenVarName : {auto c : Ref Ctxt Defs} ->             {auto u : Ref UST UState} ->             String -> Core NamegenVarName str    = do ust <- get UST         put UST (record { nextName $= (+1) } ust)         pure (MN str (nextName ust)) -- Again, for case namesexportgenCaseName : {auto c : Ref Ctxt Defs} ->              {auto u : Ref UST UState} ->			     		Int -> Core NamegenCaseName root    = do ust <- get UST         put UST (record { nextName $= (+1) } ust)         inCurrentNS (CaseBlock root (nextName ust)) exportgenWithName : {auto c : Ref Ctxt Defs} ->              {auto u : Ref UST UState} ->			     		Int -> Core NamegenWithName root    = do ust <- get UST         put UST (record { nextName $= (+1) } ust)         inCurrentNS (WithBlock root (nextName ust)) addHoleName : {auto u : Ref UST UState} ->              FC -> Name -> Int -> Core ()addHoleName fc n i    = do ust <- get UST         put UST (record { holes $= insert i (fc, n),                           currentHoles $= insert i (fc, n) } ust) addGuessName : {auto u : Ref UST UState} ->               FC -> Name -> Int -> Core ()addGuessName fc n i    = do ust <- get UST         put UST (record { guesses $= insert i (fc, n)  } ust) exportremoveHole : {auto u : Ref UST UState} ->             Int -> Core ()removeHole n    = do ust <- get UST         put UST (record { holes $= delete n,                           currentHoles $= delete n,                           delayedHoles $= delete n } ust) exportremoveHoleName : {auto c : Ref Ctxt Defs} ->                 {auto u : Ref UST UState} ->                 Name -> Core ()removeHoleName n    = do defs <- get Ctxt         let Just i = getNameID n (gamma defs)             | Nothing => pure ()         removeHole i exportsaveHoles : {auto u : Ref UST UState} ->            Core (IntMap (FC, Name))saveHoles    = do ust <- get UST         put UST (record { currentHoles = empty } ust)         pure (currentHoles ust) exportrestoreHoles : {auto u : Ref UST UState} ->               IntMap (FC, Name) -> Core ()restoreHoles hs    = do ust <- get UST         put UST (record { currentHoles = hs } ust) exportremoveGuess : {auto u : Ref UST UState} ->              Int -> Core ()removeGuess n    = do ust <- get UST         put UST (record { guesses $= delete n } ust) -- Get all of the hole dataexportgetHoles : {auto u : Ref UST UState} ->           Core (IntMap (FC, Name))getHoles    = do ust <- get UST         pure (holes ust) -- Get all of the guess dataexportgetGuesses : {auto u : Ref UST UState} ->           Core (IntMap (FC, Name))getGuesses    = do ust <- get UST         pure (guesses ust) -- Get the hole data for holes in the current elaboration session-- (i.e. since the last 'saveHoles')exportgetCurrentHoles : {auto u : Ref UST UState} ->                  Core (IntMap (FC, Name))getCurrentHoles    = do ust <- get UST         pure (currentHoles ust) exportisHole : {auto u : Ref UST UState} ->         Int -> Core BoolisHole i    = do ust <- get UST         pure (maybe False (const True) (lookup i (holes ust))) exportisCurrentHole : {auto u : Ref UST UState} ->                Int -> Core BoolisCurrentHole i    = do ust <- get UST         pure (maybe False (const True) (lookup i (currentHoles ust))) exportsetConstraint : {auto u : Ref UST UState} ->                Int -> Constraint -> Core ()setConstraint cid c    = do ust <- get UST         put UST (record { constraints $= insert cid c } ust) exportdeleteConstraint : {auto u : Ref UST UState} ->                Int -> Core ()deleteConstraint cid    = do ust <- get UST         put UST (record { constraints $= delete cid } ust) exportaddConstraint : {auto u : Ref UST UState} ->                {auto c : Ref Ctxt Defs} ->                Constraint -> Core IntaddConstraint constr    = do ust <- get UST         let cid = nextConstraint ust         put UST (record { constraints $= insert cid constr,                           nextConstraint = cid+1 } ust)         pure cid exportaddDot : {auto u : Ref UST UState} ->         FC -> Env Term vars -> Name -> Term vars -> DotReason -> Term vars ->         Core ()addDot fc env dotarg x reason y    = do ust <- get UST         put UST (record { dotConstraints $=                             ((dotarg, reason, MkConstraint fc False [] env x y) ::)                         } ust) mkConstantAppArgs : Bool -> FC -> Env Term vars ->                    (wkns : List Name) ->                    List (Term (wkns ++ (vars ++ done)))mkConstantAppArgs lets fc [] wkns = []mkConstantAppArgs {done} {vars = x :: xs} lets fc (b :: env) wkns    = let rec = mkConstantAppArgs {done} lets fc env (wkns ++ [x]) in          if lets || not (isLet b)             then Local fc (Just (isLet b)) (length wkns) (mkVar wkns) ::                  rewrite (appendAssociative wkns [x] (xs ++ done)) in rec             else rewrite (appendAssociative wkns [x] (xs ++ done)) in rec  where    isLet : Binder (Term vars) -> Bool    isLet (Let _ _ _) = True    isLet _ = False     mkVar : (wkns : List Name) ->            IsVar name (length wkns) (wkns ++ name :: vars ++ done)    mkVar [] = First    mkVar (w :: ws) = Later (mkVar ws) mkConstantAppArgsOthers : Bool -> FC -> Env Term vars ->                          SubVars smaller vars ->                          (wkns : List Name) ->                          List (Term (wkns ++ (vars ++ done)))mkConstantAppArgsOthers lets fc [] p wkns = []mkConstantAppArgsOthers {done} {vars = x :: xs}                        lets fc (b :: env) SubRefl wkns    = rewrite appendAssociative wkns [x] (xs ++ done) in              mkConstantAppArgsOthers lets fc env SubRefl (wkns ++ [x])mkConstantAppArgsOthers {done} {vars = x :: xs}                        lets fc (b :: env) (KeepCons p) wkns    = rewrite appendAssociative wkns [x] (xs ++ done) in              mkConstantAppArgsOthers lets fc env p (wkns ++ [x])mkConstantAppArgsOthers {done} {vars = x :: xs}                        lets fc (b :: env) (DropCons p) wkns    = let rec = mkConstantAppArgsOthers {done} lets fc env p (wkns ++ [x]) in          if lets || not (isLet b)             then Local fc (Just (isLet b)) (length wkns) (mkVar wkns) ::                  rewrite appendAssociative wkns [x] (xs ++ done) in rec             else rewrite appendAssociative wkns [x] (xs ++ done) in rec  where    isLet : Binder (Term vars) -> Bool    isLet (Let _ _ _) = True    isLet _ = False     mkVar : (wkns : List Name) ->            IsVar name (length wkns) (wkns ++ name :: vars ++ done)    mkVar [] = First    mkVar (w :: ws) = Later (mkVar ws)  exportapplyTo : FC -> Term vars -> Env Term vars -> Term varsapplyTo {vars} fc tm env  = let args = reverse (mkConstantAppArgs {done = []} False fc env []) in        apply fc tm (rewrite sym (appendNilRightNeutral vars) in args) exportapplyToFull : FC -> Term vars -> Env Term vars -> Term varsapplyToFull {vars} fc tm env  = let args = reverse (mkConstantAppArgs {done = []} True fc env []) in        apply fc tm (rewrite sym (appendNilRightNeutral vars) in args) exportapplyToOthers : FC -> Term vars -> Env Term vars ->                SubVars smaller vars -> Term varsapplyToOthers {vars} fc tm env sub  = let args = reverse (mkConstantAppArgsOthers {done = []} True fc env sub []) in        apply fc tm (rewrite sym (appendNilRightNeutral vars) in args) -- Create a new metavariable with the given name and return type,-- and return a term which is the metavariable applied to the environment-- (and which has the given type)-- Flag whether cycles are allowed in the result, and whether to abstract-- over letsexportnewMetaLets : {auto c : Ref Ctxt Defs} ->              {auto u : Ref UST UState} ->              FC -> RigCount ->              Env Term vars -> Name -> Term vars -> Def ->              Bool -> Bool ->              Core (Int, Term vars)newMetaLets {vars} fc rig env n ty def nocyc lets    = do let hty = if lets then abstractFullEnvType fc env ty                           else abstractEnvType fc env ty         let hole = record { noCycles = nocyc }                           (newDef fc n rig [] hty Public def)         log 5 $ "Adding new meta " ++ show (n, fc, rig)         logTerm 10 ("New meta type " ++ show n) hty         defs <- get Ctxt         idx <- addDef n hole         addHoleName fc n idx         pure (idx, Meta fc n idx envArgs)  where    envArgs : List (Term vars)    envArgs = let args = reverse (mkConstantAppArgs {done = []} lets fc env []) in                  rewrite sym (appendNilRightNeutral vars) in args exportnewMeta : {auto c : Ref Ctxt Defs} ->          {auto u : Ref UST UState} ->          FC -> RigCount ->          Env Term vars -> Name -> Term vars -> Def ->          Bool ->          Core (Int, Term vars)newMeta fc r env n ty def cyc = newMetaLets fc r env n ty def cyc False mkConstant : FC -> Env Term vars -> Term vars -> ClosedTermmkConstant fc [] tm = tm-- mkConstant {vars = x :: _} fc (Let c val ty :: env) tm--     = mkConstant fc env (Bind fc x (Let c val ty) tm)mkConstant {vars = x :: _} fc (b :: env) tm    = let ty = binderType b in          mkConstant fc env (Bind fc x (Lam (multiplicity b) Explicit ty) tm) -- Given a term and a type, add a new guarded constant to the global context-- by applying the term to the current environment-- Return the replacement term (the name applied to the environment)exportnewConstant : {auto u : Ref UST UState} ->              {auto c : Ref Ctxt Defs} ->              FC -> RigCount -> Env Term vars ->              (tm : Term vars) -> (ty : Term vars) ->              (constrs : List Int) ->              Core (Term vars)newConstant {vars} fc rig env tm ty constrs    = do let def = mkConstant fc env tm         let defty = abstractFullEnvType fc env ty         cn <- genName "postpone"         let guess = newDef fc cn rig [] defty Public                            (Guess def (length env) constrs)         log 5 $ "Adding new constant " ++ show (cn, fc, rig)         logTerm 10 ("New constant type " ++ show cn) defty         idx <- addDef cn guess         addGuessName fc cn idx         pure (Meta fc cn idx envArgs)  where    envArgs : List (Term vars)    envArgs = let args = reverse (mkConstantAppArgs {done = []} True fc env []) in                  rewrite sym (appendNilRightNeutral vars) in args -- Create a new search with the given name and return type,-- and return a term which is the name applied to the environment-- (and which has the given type)exportnewSearch : {auto c : Ref Ctxt Defs} ->            {auto u : Ref UST UState} ->            FC -> RigCount -> Nat -> Name ->            Env Term vars -> Name -> Term vars -> Core (Int, Term vars)newSearch {vars} fc rig depth def env n ty    = do let hty = abstractEnvType fc env ty         let hole = newDef fc n rig [] hty Public (BySearch rig depth def)         log 10 $ "Adding new search " ++ show fc ++ " " ++ show n         logTermNF 10 "New search type" env ty         idx <- addDef n hole         addGuessName fc n idx         pure (idx, Meta fc n idx envArgs)  where    envArgs : List (Term vars)    envArgs = let args = reverse (mkConstantAppArgs {done = []} False fc env []) in                  rewrite sym (appendNilRightNeutral vars) in args -- Add a hole which stands for a delayed elaboratorexportnewDelayed : {auto u : Ref UST UState} ->             {auto c : Ref Ctxt Defs} ->             FC -> RigCount ->             Env Term vars -> Name ->             (ty : Term vars) -> Core (Int, Term vars)newDelayed {vars} fc rig env n ty    = do let hty = abstractEnvType fc env ty         let hole = newDef fc n rig [] hty Public Delayed         idx <- addDef n hole         log 10 $ "Added delayed elaborator " ++ show (n, idx)         addHoleName fc n idx         pure (idx, Meta fc n idx envArgs)  where    envArgs : List (Term vars)    envArgs = let args = reverse (mkConstantAppArgs {done = []} False fc env []) in                  rewrite sym (appendNilRightNeutral vars) in args exporttryErrorUnify : {auto c : Ref Ctxt Defs} ->                {auto u : Ref UST UState} ->                Core a -> Core (Either Error a)tryErrorUnify elab    = do ust <- get UST         defs <- branch         catch (do res <- elab                   commit                   pure (Right res))               (\err => do put UST ust                           defs' <- get Ctxt                           put Ctxt (record { timings = timings defs' } defs)                           pure (Left err)) exporttryUnify : {auto c : Ref Ctxt Defs} ->           {auto u : Ref UST UState} ->           Core a -> Core a -> Core atryUnify elab1 elab2    = do Right ok <- tryErrorUnify elab1               | Left err => elab2         pure ok exporthandleUnify : {auto c : Ref Ctxt Defs} ->              {auto u : Ref UST UState} ->              Core a -> (Error -> Core a) -> Core ahandleUnify elab1 elab2    = do Right ok <- tryErrorUnify elab1               | Left err => elab2 err

Lines 1–500 of 675. Load more