module Core.Unify import Core.CaseTreeimport Core.Contextimport Core.Coreimport Core.Envimport Core.GetTypeimport Core.Normaliseimport Core.TTimport public Core.UnifyStateimport Core.Value import Data.IntMapimport Data.List.Viewsimport Data.NameMap %default covering public exportdata UnifyMode = InLHS               | InTerm               | InMatch               | InSearch -- Need to record if we're at the top level or not, because top level things-- can have Force and Delay inserted, and may have been postponed.public exportrecord UnifyInfo where  constructor MkUnifyInfo  atTop : Bool  precise : Bool -- False == generalise to RigW in Pi  umode : UnifyMode exportinTerm : UnifyInfoinTerm = MkUnifyInfo True True InTerm exportinLHS : UnifyInfoinLHS = MkUnifyInfo True True InLHS exportinTermP : Bool -> UnifyInfoinTermP p = MkUnifyInfo True p InTerm exportinMatch : UnifyInfoinMatch = MkUnifyInfo True True InMatch exportinSearch : UnifyInfoinSearch = MkUnifyInfo True True InSearch lam : UnifyInfo -> UnifyInfolam = record { precise = True } inLam : UnifyInfo -> BoolinLam = precise lower : UnifyInfo -> UnifyInfolower = record { atTop = False } Eq UnifyMode where   InLHS == InLHS = True   InTerm == InTerm = True   InMatch == InMatch = True   InSearch == InSearch = True   _ == _ = False Eq UnifyInfo where  x == y = atTop x == atTop y && precise x == precise y && umode x == umode y Show UnifyMode where  show InLHS = "InLHS"  show InTerm = "InTerm"  show InMatch = "InMatch"  show InSearch = "InSearch" -- If we're unifying a Lazy type with a non-lazy type, we need to add an-- explicit force or delay to the first argument to unification. This says-- which to add, if any. Can only added at the very top level.public exportdata AddLazy = NoLazy | AddForce LazyReason | AddDelay LazyReason exportShow AddLazy where  show NoLazy = "NoLazy"  show (AddForce _) = "AddForce"  show (AddDelay _) = "AddDelay" public exportrecord UnifyResult where  constructor MkUnifyResult  constraints : List Int  holesSolved : Bool -- did we solve any holes  namesSolved : List Int -- which ones did we solve (as name indices)  addLazy : AddLazy union : UnifyResult -> UnifyResult -> UnifyResultunion u1 u2 = MkUnifyResult (union (constraints u1) (constraints u2))                            (holesSolved u1 || holesSolved u2)                            (namesSolved u1 ++ namesSolved u2)                            NoLazy -- only top level, so assume no annotation unionAll : List UnifyResult -> UnifyResultunionAll [] = MkUnifyResult [] False [] NoLazyunionAll [c] = cunionAll (c :: cs) = union c (unionAll cs) constrain : Int -> UnifyResultconstrain c = MkUnifyResult [c] False [] NoLazy success : UnifyResultsuccess = MkUnifyResult [] False [] NoLazy solvedHole : Int -> UnifyResultsolvedHole n = MkUnifyResult [] True [n] NoLazy public exportinterface Unify (tm : List Name -> Type) where  -- Unify returns a list of ids referring to newly added constraints  unifyD : Ref Ctxt Defs ->           Ref UST UState ->           UnifyInfo ->           FC -> Env Term vars ->           tm vars -> tm vars ->           Core UnifyResult  -- As unify but at the top level can allow lazy/non-lazy to be mixed in  -- order to infer annotations  unifyWithLazyD : Ref Ctxt Defs ->                   Ref UST UState ->                   UnifyInfo ->                   FC -> Env Term vars ->                   tm vars -> tm vars ->                   Core UnifyResult  unifyWithLazyD = unifyD -- Workaround for auto implicits not working in interfaces-- In calls to unification, the first argument is the given type, and the second-- argument is the expected type.exportunify : Unify tm =>        {auto c : Ref Ctxt Defs} ->        {auto u : Ref UST UState} ->        UnifyInfo ->        FC -> Env Term vars ->        tm vars -> tm vars ->        Core UnifyResultunify {c} {u} = unifyD c u exportunifyWithLazy : Unify tm =>                {auto c : Ref Ctxt Defs} ->                {auto u : Ref UST UState} ->                UnifyInfo ->                FC -> Env Term vars ->                tm vars -> tm vars ->                Core UnifyResultunifyWithLazy {c} {u} = unifyWithLazyD c u -- Defined in Core.AutoSearchexportsearch : {auto c : Ref Ctxt Defs} ->         {auto u : Ref UST UState} ->         FC -> RigCount ->         (defaults : Bool) -> (depth : Nat) ->         (defining : Name) -> (topTy : Term vars) -> Env Term vars ->         Core (Term vars) ufail : FC -> String -> Core aufail loc msg = throw (GenericMsg loc msg) convertError : {auto c : Ref Ctxt Defs} ->               FC -> Env Term vars -> NF vars -> NF vars -> Core aconvertError loc env x y    = do defs <- get Ctxt         empty <- clearDefs defs         throw (CantConvert loc env !(quote empty env x)                                    !(quote empty env y)) convertErrorS : {auto c : Ref Ctxt Defs} ->                Bool -> FC -> Env Term vars -> NF vars -> NF vars -> Core aconvertErrorS s loc env x y    = if s then convertError loc env y x           else convertError loc env x y -- Find all the metavariables required by each of the given names.-- We'll assume all meta solutions are of the form STerm exp.chaseMetas : {auto c : Ref Ctxt Defs} ->             List Name -> NameMap () -> Core (List Name)chaseMetas [] all = pure (keys all)chaseMetas (n :: ns) all    = case lookup n all of           Just _ => chaseMetas ns all           _ => do defs <- get Ctxt                   Just (PMDef _ _ (STerm soln) _ _) <-                                  lookupDefExact n (gamma defs)                        | _ => chaseMetas ns (insert n () all)                   let sns = keys (getMetas soln)                   chaseMetas (sns ++ ns) (insert n () all) -- Get all the metavariable names used by the term (recursively, so we-- can do the occurs check)getMetaNames : {auto c : Ref Ctxt Defs} ->               Term vars -> Core (List Name)getMetaNames tm    = let metas = getMetas tm in          chaseMetas (keys metas) empty postpone : {auto c : Ref Ctxt Defs} ->           {auto u : Ref UST UState} ->           (blockedMeta : Bool) ->           FC -> UnifyInfo -> String ->           Env Term vars -> NF vars -> NF vars -> Core UnifyResultpostpone blockedMetas loc mode logstr env x y    = do defs <- get Ctxt         empty <- clearDefs defs         logC 10 $              do xq <- quote defs env x                 yq <- quote defs env y                 pure (logstr ++ ": " ++ show !(toFullNames xq) ++                                    " =?= " ++ show !(toFullNames yq))         xtm <- quote empty env x         ytm <- quote empty env y         -- Need to find all the metas in the constraint since solving any one         -- of them might stop the constraint being blocked.         metas <-             if blockedMetas                then let xmetas = getMetas xtm in                         chaseMetas (keys (addMetas xmetas ytm)) NameMap.empty                else pure []         blocked <- filterM undefinedN metas         c <- addConstraint (MkConstraint loc (atTop mode) blocked env                                          xtm                                          ytm)         log 10 $ show c ++ " NEW CONSTRAINT " ++ show loc ++                 " blocked on " ++ show metas         logTerm 10 "X" xtm         logTerm 10 "Y" ytm         pure (constrain c)  where    undefinedN : Name -> Core Bool    undefinedN n        = do defs <- get Ctxt             case !(lookupDefExact n (gamma defs)) of                  Just (Hole _ _) => pure True                  Just (BySearch _ _ _) => pure True                  Just (Guess _ _ _) => pure True                  _ => pure False postponeS : {auto c : Ref Ctxt Defs} ->            {auto u : Ref UST UState} ->            Bool -> Bool -> FC -> UnifyInfo -> String -> Env Term vars ->            NF vars -> NF vars ->            Core UnifyResultpostponeS b s loc mode logstr env x y    = if s then postpone b loc (lower mode) logstr env y x           else postpone b loc mode logstr env x y unifyArgs : (Unify tm, Quote tm) =>            {auto c : Ref Ctxt Defs} ->            {auto u : Ref UST UState} ->            UnifyInfo -> FC -> Env Term vars ->            List (tm vars) -> List (tm vars) ->            Core UnifyResultunifyArgs mode loc env [] [] = pure successunifyArgs mode loc env (cx :: cxs) (cy :: cys)    = do -- Do later arguments first, since they may depend on earlier         -- arguments and use their solutions.         cs <- unifyArgs mode loc env cxs cys         res <- unify (lower mode) loc env cx cy         pure (union res cs)unifyArgs mode loc env _ _ = ufail loc "" -- Get the variables in an application argument list; fail if any arguments-- are not variables, fail if there's any repetition of variables-- We use this to check that the pattern unification rule is applicable-- when solving a metavariable applied to argumentsgetVars : List Nat -> List (NF vars) -> Maybe (List (Var vars))getVars got [] = Just []getVars got (NApp fc (NLocal r idx v) [] :: xs)    = if inArgs idx got then Nothing         else do xs' <- getVars (idx :: got) xs                 pure (MkVar v :: xs')  where    -- Save the overhead of the call to APPLY, and the fact that == on    -- Nat is linear time in Idris 1!    inArgs : Nat -> List Nat -> Bool    inArgs n [] = False    inArgs n (n' :: ns)        = if toIntegerNat n == toIntegerNat n' then True else inArgs n nsgetVars got (NAs _ _ _ p :: xs) = getVars got (p :: xs)getVars _ (_ :: xs) = Nothing -- Make a sublist representing the variables used in the application.-- We'll use this to ensure that local variables which appear in a term-- are all arguments to a metavariable application for pattern unificationtoSubVars : (vars : List Name) -> List (Var vars) ->            (newvars ** SubVars newvars vars)toSubVars [] xs = ([] ** SubRefl)toSubVars (n :: ns) xs     -- If there's a proof 'First' in 'xs', then 'n' should be kept,     -- otherwise dropped     -- (Remember: 'n' might be shadowed; looking for 'First' ensures we     -- get the *right* proof that the name is in scope!)     = let (_ ** svs) = toSubVars ns (dropFirst xs) in           if anyFirst xs              then (_ ** KeepCons svs)              else (_ ** DropCons svs)  where    anyFirst : List (Var (n :: ns)) -> Bool    anyFirst [] = False    anyFirst (MkVar First :: xs) = True    anyFirst (MkVar (Later p) :: xs) = anyFirst xs {- Applying the pattern unification rule is okay if:   * Arguments are all distinct local variables   * The metavariable name doesn't appear in the unifying term   * The local variables which appear in the term are all arguments to     the metavariable application (not checked here, checked with the     result of `patternEnv`)    Return the subset of the environment used in the arguments   to which the metavariable is applied. If this environment is enough   to check the term we're unifying with, and that term doesn't use the   metavariable name, we can safely apply the rule.    Also, return the list of arguments the metavariable was applied to, to   make sure we use them in the right order when we build the solution.-}patternEnv : {auto c : Ref Ctxt Defs} ->             {auto u : Ref UST UState} ->             {vars : _} ->             Env Term vars -> List (Closure vars) ->             Core (Maybe (newvars ** (List (Var newvars),                                     SubVars newvars vars)))patternEnv {vars} env args    = do defs <- get Ctxt         empty <- clearDefs defs         args' <- traverse (evalArg empty) args         case getVars [] args' of              Nothing => pure Nothing              Just vs =>                 let (newvars ** svs) = toSubVars _ vs in                     pure (Just (newvars **                                     (updateVars vs svs, svs)))  where    -- Update the variable list to point into the sub environment    -- (All of these will succeed because the SubVars we have comes from    -- the list of variable uses! It's not stated in the type, though.)    updateVars : List (Var vars) -> SubVars newvars vars -> List (Var newvars)    updateVars [] svs = []    updateVars (MkVar p :: ps) svs        = case subElem p svs of               Nothing => updateVars ps svs               Just p' => p' :: updateVars ps svs getVarsBelowTm : Nat -> List (Term vars) -> Maybe (List (Var vars))getVarsBelowTm max [] = Just []getVarsBelowTm max (Local fc r idx v :: xs)    = if idx >= max then Nothing         else do xs' <- getVarsBelowTm idx xs                 pure (MkVar v :: xs')getVarsBelowTm _ (_ :: xs) = Nothing exportpatternEnvTm : {auto c : Ref Ctxt Defs} ->               {auto u : Ref UST UState} ->               {vars : _} ->               Env Term vars -> List (Term vars) ->               Core (Maybe (newvars ** (List (Var newvars),                                       SubVars newvars vars)))patternEnvTm {vars} env args    = do defs <- get Ctxt         empty <- clearDefs defs         case getVarsBelowTm 1000000 args of              Nothing => pure Nothing              Just vs =>                 let (newvars ** svs) = toSubVars _ vs in                     pure (Just (newvars **                                     (updateVars vs svs, svs)))  where    -- Update the variable list to point into the sub environment    -- (All of these will succeed because the SubVars we have comes from    -- the list of variable uses! It's not stated in the type, though.)    updateVars : List (Var vars) -> SubVars newvars vars -> List (Var newvars)    updateVars [] svs = []    updateVars (MkVar p :: ps) svs        = case subElem p svs of               Nothing => updateVars ps svs               Just p' => p' :: updateVars ps svs -- Check that the metavariable name doesn't occur in the solution.-- If it does, normalising might help. If it still does, that's an error.occursCheck : {auto c : Ref Ctxt Defs} ->              FC -> Env Term vars -> UnifyInfo ->              Name -> Term vars -> Core (Maybe (Term vars))occursCheck fc env mode mname tm    = do solmetas <- getMetaNames tm         let False = mname `elem` solmetas             | _ => do defs <- get Ctxt                       tmnf <- normalise defs env tm                       solmetas <- getMetaNames tmnf                       if mname `elem` solmetas                          then do failOnStrongRigid False                                     (throw (CyclicMeta fc env mname tmnf))                                     tmnf                                  pure Nothing                          else pure $ Just tmnf         pure $ Just tm  where    -- Throw an occurs check failure if the name appears 'strong rigid',    -- that is, under a constructor form rather than a function, in the    -- term    failOnStrongRigid : Bool -> Core () -> Term vars -> Core ()    failOnStrongRigid bad err (Meta _ n _ _)        = if bad && n == mname             then err             else pure ()    failOnStrongRigid bad err tm        = case getFnArgs tm of               (f, []) => pure ()               (Ref _ Func _, _) => pure () -- might reduce away, just block               (Ref _ _ _, args) => traverse_ (failOnStrongRigid True err) args               (f, args) => traverse_ (failOnStrongRigid bad err) args -- Instantiate a metavariable by binding the variables in 'newvars'-- and returning the term-- If the type of the metavariable doesn't have enough arguments, fail, because-- this wasn't valid for pattern unificationinstantiate : {auto c : Ref Ctxt Defs} ->              {auto u : Ref UST UState} ->              {newvars : _} ->              FC -> UnifyInfo -> Env Term vars ->              (metavar : Name) -> (mref : Int) -> (numargs : Nat) ->              (mdef : GlobalDef) ->              List (Var newvars) -> -- Variable each argument maps to              Term vars -> -- original, just for error message              Term newvars -> -- shrunk environment              Core ()instantiate {newvars} loc mode env mname mref num mdef locs otm tm    = do logTerm 5 ("Instantiating in " ++ show newvars) tm--          let Hole _ _ = definition mdef--              | def => ufail {a=()} loc (show mname ++ " already resolved as " ++ show def)         case fullname mdef of              PV pv pi => throw (PatternVariableUnifies loc env (PV pv pi) otm)              _ => pure ()         let ty = type mdef -- assume all pi binders we need are there since                            -- it was built from an environment, so no need                            -- to normalise         defs <- get Ctxt         rhs <- mkDef [] newvars (snocList newvars)                     (rewrite appendNilRightNeutral newvars in locs)                     (rewrite appendNilRightNeutral newvars in tm)                     ty         logTerm 5 ("Instantiated: " ++ show mname) ty         log 5 ("From vars: " ++ show newvars)         logTerm 5 "Definition" rhs         let simpleDef = MkPMDefInfo (SolvedHole num) (isSimple rhs)         let newdef = record { definition =                                 PMDef simpleDef [] (STerm rhs) (STerm rhs) []                             } mdef         addDef (Resolved mref) newdef         removeHole mref  where    isSimple : Term vs -> Bool    isSimple (Local _ _ _ _) = True    isSimple (Ref _ _ _) = True    isSimple (Meta _ _ _ _) = True    isSimple (Bind _ _ (Lam _ _ _) sc) = isSimple sc    isSimple (PrimVal _ _) = True    isSimple (TType _) = True    isSimple _ = False     updateLoc : {v : Nat} -> List (Var vs) -> .(IsVar name v vs') ->                Maybe (Var vs)    updateLoc [] el = Nothing    updateLoc (p :: ps) First = Just p    updateLoc (p :: ps) (Later prf) = updateLoc ps prf     -- Since the order of variables is not necessarily the same in the solution,    -- this is to make sure the variables point to the right argument, given    -- the argument list we got from the application of the hole.    updateLocs : List (Var vs) -> Term vs -> Maybe (Term vs)    updateLocs locs (Local fc r idx p)        = do MkVar p' <- updateLoc locs p             Just (Local fc r _ p')    updateLocs {vs} locs (Bind fc x b sc)        = do b' <- updateLocsB b             sc' <- updateLocs                       (MkVar First :: map (\ (MkVar p) => (MkVar (Later p))) locs)                       sc             Just (Bind fc x b' sc')      where        updateLocsB : Binder (Term vs) -> Maybe (Binder (Term vs))        updateLocsB (Lam c p t) = Just (Lam c p !(updateLocs locs t))        updateLocsB (Let c v t) = Just (Let c !(updateLocs locs v) !(updateLocs locs t))        -- Make 'pi' binders have multiplicity W when we infer a Rig1 metavariable,        -- since this is the most general thing to do if it's unknown.        updateLocsB (Pi rig p t) = if isLinear rig

Lines 1–500 of 1544. Load more