module TTImp.ProcessDef import Core.CaseBuilderimport Core.CaseTreeimport Core.Contextimport Core.Coreimport Core.Coverageimport Core.Envimport Core.Hashimport Core.LinearCheckimport Core.Metadataimport Core.Normaliseimport Core.Terminationimport Core.Valueimport Core.UnifyState import TTImp.BindImplicitsimport TTImp.Elabimport TTImp.Elab.Checkimport TTImp.Impossibleimport TTImp.PartialEvalimport TTImp.TTImpimport TTImp.Unelabimport TTImp.Utilsimport TTImp.WithClause import Data.NameMap mutual  mismatchNF : Defs -> NF vars -> NF vars -> Core Bool  mismatchNF defs (NTCon _ xn xt _ xargs) (NTCon _ yn yt _ yargs)      = if xn /= yn           then pure True           else anyM (mismatch defs) (zip xargs yargs)  mismatchNF defs (NDCon _ _ xt _ xargs) (NDCon _ _ yt _ yargs)      = if xt /= yt           then pure True           else anyM (mismatch defs) (zip xargs yargs)  mismatchNF defs (NPrimVal _ xc) (NPrimVal _ yc) = pure (xc /= yc)  mismatchNF defs (NDelayed _ _ x) (NDelayed _ _ y) = mismatchNF defs x y  mismatchNF defs (NDelay _ _ _ x) (NDelay _ _ _ y)      = mismatchNF defs !(evalClosure defs x) !(evalClosure defs y)  mismatchNF _ _ _ = pure False   mismatch : Defs -> (Closure vars, Closure vars) -> Core Bool  mismatch defs (x, y)      = mismatchNF defs !(evalClosure defs x) !(evalClosure defs y) -- If the terms have the same type constructor at the head, and one of-- the argument positions has different constructors at its head, then this-- is an impossible case, so return TrueexportimpossibleOK : Defs -> NF vars -> NF vars -> Core BoolimpossibleOK defs (NTCon _ xn xt xa xargs) (NTCon _ yn yt ya yargs)    = if xn == yn         then anyM (mismatch defs) (zip xargs yargs)         else pure False-- If it's a data constructor, any mismatch will doimpossibleOK defs (NDCon _ _ xt _ xargs) (NDCon _ _ yt _ yargs)    = if xt /= yt         then pure True         else anyM (mismatch defs) (zip xargs yargs)impossibleOK defs (NPrimVal _ x) (NPrimVal _ y) = pure (x /= y)impossibleOK defs (NDCon _ _ _ _ _) (NPrimVal _ _) = pure TrueimpossibleOK defs (NPrimVal _ _) (NDCon _ _ _ _ _) = pure TrueimpossibleOK defs x y = pure False exportimpossibleErrOK : {auto c : Ref Ctxt Defs} ->                  Defs -> Error -> Core BoolimpossibleErrOK defs (CantConvert fc env l r)    = do logTerm 10 "Impossible" !(normalise defs env l)         logTerm 10 "    ...and" !(normalise defs env r)         impossibleOK defs !(nf defs env l)                           !(nf defs env r)impossibleErrOK defs (CantSolveEq fc env l r)    = do logTerm 10 "Impossible" !(normalise defs env l)         logTerm 10 "    ...and" !(normalise defs env r)         impossibleOK defs !(nf defs env l)                           !(nf defs env r)impossibleErrOK defs (BadDotPattern _ _ ErasedArg _ _) = pure TrueimpossibleErrOK defs (CyclicMeta _ _) = pure TrueimpossibleErrOK defs (AllFailed errs)    = anyM (impossibleErrOK defs) (map snd errs)impossibleErrOK defs (WhenUnifying _ _ _ _ err)    = impossibleErrOK defs errimpossibleErrOK defs _ = pure False -- Given a type checked LHS and its type, return the environment in which we-- should check the RHS, the LHS and its type in that environment,-- and a function which turns a checked RHS into a-- pattern clause-- The 'SubVars' proof contains a proof that refers to the *inner* environment,-- so all the outer things are marked as 'DropCons'extendEnv : Env Term vars -> SubVars inner vars ->            NestedNames vars ->            Term vars -> Term vars ->            Core (vars' **                    (SubVars inner vars',                     Env Term vars', NestedNames vars',                     Term vars', Term vars'))extendEnv env p nest (Bind _ n (PVar c pi tmty) sc) (Bind _ n' (PVTy _ _) tysc) with (nameEq n n')  extendEnv env p nest (Bind _ n (PVar c pi tmty) sc) (Bind _ n' (PVTy _ _) tysc) | Nothing      = throw (InternalError "Can't happen: names don't match in pattern type")  extendEnv env p nest (Bind _ n (PVar c pi tmty) sc) (Bind _ n (PVTy _ _) tysc) | (Just Refl)      = extendEnv (PVar c pi tmty :: env) (DropCons p) (weaken nest) sc tyscextendEnv env p nest (Bind _ n (PLet c tmval tmty) sc) (Bind _ n' (PLet _ _ _) tysc) with (nameEq n n')  extendEnv env p nest (Bind _ n (PLet c tmval tmty) sc) (Bind _ n' (PLet _ _ _) tysc) | Nothing      = throw (InternalError "Can't happen: names don't match in pattern type")  -- PLet on the left becomes Let on the right, to give it computational force  extendEnv env p nest (Bind _ n (PLet c tmval tmty) sc) (Bind _ n (PLet _ _ _) tysc) | (Just Refl)      = extendEnv (Let c tmval tmty :: env) (DropCons p) (weaken nest) sc tyscextendEnv env p nest tm ty      = pure (_ ** (p, env, nest, tm, ty)) -- Find names which are applied to a function in a Rig1/Rig0 position,-- so that we know how they should be bound on the right hand side of the-- pattern.-- 'bound' counts the number of variables locally bound; these are the-- only ones we're checking linearity of (we may be shadowing names if this-- is a local definition, so we need to leave the earlier ones alone)findLinear : {auto c : Ref Ctxt Defs} ->             Bool -> Nat -> RigCount -> Term vars ->             Core (List (Name, RigCount))findLinear top bound rig (Bind fc n b sc)    = findLinear top (S bound) rig scfindLinear top bound rig (As fc _ _ p)    = findLinear top bound rig pfindLinear top bound rig tm    = case getFnArgs tm of           (Ref _ _ n, []) => pure []           (Ref _ nt n, args)              => do defs <- get Ctxt                    Just nty <- lookupTyExact n (gamma defs)                         | Nothing => pure []                    findLinArg (accessible nt rig) !(nf defs [] nty) args           _ => pure []    where      accessible : NameType -> RigCount -> RigCount      accessible Func r = if top then r else Rig0      accessible _ r = r       findLinArg : RigCount -> NF [] -> List (Term vars) ->                   Core (List (Name, RigCount))      findLinArg rig ty (As fc UseLeft _ p :: as)          = findLinArg rig ty (p :: as)      findLinArg rig ty (As fc UseRight p _ :: as)          = findLinArg rig ty (p :: as)      findLinArg rig (NBind _ x (Pi c _ _) sc) (Local {name=a} fc _ idx prf :: as)          = do defs <- get Ctxt               if idx < bound                 then do sc' <- sc defs (toClosure defaultOpts [] (Ref fc Bound x))                         pure $ (a, rigMult c rig) ::                                    !(findLinArg rig sc' as)                 else do sc' <- sc defs (toClosure defaultOpts [] (Ref fc Bound x))                         findLinArg rig sc' as      findLinArg rig (NBind fc x (Pi c _ _) sc) (a :: as)          = do defs <- get Ctxt               pure $ !(findLinear False bound (rigMult c rig) a) ++                      !(findLinArg rig !(sc defs (toClosure defaultOpts [] (Ref fc Bound x))) as)      findLinArg rig ty (a :: as)          = pure $ !(findLinear False bound rig a) ++ !(findLinArg rig ty as)      findLinArg _ _ [] = pure [] setLinear : List (Name, RigCount) -> Term vars -> Term varssetLinear vs (Bind fc x (PVar c p ty) sc)    = case lookup x vs of           Just c' => Bind fc x (PVar c' p ty) (setLinear vs sc)           _ => Bind fc x (PVar c p ty) (setLinear vs sc)setLinear vs (Bind fc x (PVTy c ty) sc)    = case lookup x vs of           Just c' => Bind fc x (PVTy c' ty) (setLinear vs sc)           _ => Bind fc x (PVTy c ty) (setLinear vs sc)setLinear vs tm = tm -- Combining multiplicities on LHS:-- Rig1 + Rig1/W not valid, since it means we have repeated use of name-- Rig0 + RigW = RigW-- Rig0 + Rig1 = Rig1combineLinear : FC -> List (Name, RigCount) ->                Core (List (Name, RigCount))combineLinear loc [] = pure []combineLinear loc ((n, count) :: cs)    = case lookupAll n cs of           [] => pure $ (n, count) :: !(combineLinear loc cs)           counts => do count' <- combineAll count counts                        pure $ (n, count') ::                               !(combineLinear loc (filter notN cs))  where    notN : (Name, RigCount) -> Bool    notN (n', _) = n /= n'     lookupAll : Name -> List (Name, RigCount) -> List RigCount    lookupAll n [] = []    lookupAll n ((n', c) :: cs)       = if n == n' then c :: lookupAll n cs else lookupAll n cs     combine : RigCount -> RigCount -> Core RigCount    combine Rig1 Rig1 = throw (LinearUsed loc 2 n)    combine Rig1 RigW = throw (LinearUsed loc 2 n)    combine RigW Rig1 = throw (LinearUsed loc 2 n)    combine RigW RigW = pure RigW    combine Rig0 c = pure c    combine c Rig0 = pure c     combineAll : RigCount -> List RigCount -> Core RigCount    combineAll c [] = pure c    combineAll c (c' :: cs)        = do newc <- combine c c'             combineAll newc cs 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 ->           FC -> RawImp ->           Core (RawImp, -- checked LHS with implicits added                 (vars' ** (SubVars vars vars',                           Env Term vars', NestedNames vars',                           Term vars', Term vars')))checkLHS {vars} mult hashit n opts nest env fc lhs_in    = do defs <- get Ctxt         lhs_raw <- lhsInCurrentNS nest lhs_in         autoimp <- isUnboundImplicits         setUnboundImplicits True         (_, lhs_bound) <- bindNames False lhs_raw         setUnboundImplicits autoimp         lhs <- implicitsAs defs vars lhs_bound          log 5 $ "Checking LHS of " ++ show !(getFullName (Resolved n)) ++                 " " ++ show lhs         logEnv 5 "In env" env         (lhstm, lhstyg) <-             wrapError (InLHS fc !(getFullName (Resolved n))) $                     elabTerm n (InLHS mult) opts nest env                                (IBindHere fc PATTERN lhs) Nothing         logTerm 5 "Checked LHS term" lhstm         lhsty <- getTerm lhstyg          defs <- get Ctxt         let lhsenv = letToLam env         -- we used to fully normalise the LHS, to make sure fromInteger         -- patterns were allowed, but now they're fully normalised anyway         -- so we only need to do the holes. If there's a lot of type level         -- computation, this is a huge saving!         lhstm <- normaliseHoles defs lhsenv lhstm         lhsty <- normaliseHoles defs env lhsty         linvars_in <- findLinear True 0 Rig1 lhstm         logTerm 10 "Checked LHS term after normalise" lhstm         log 5 $ "Linearity of names in " ++ show n ++ ": " ++                 show linvars_in          linvars <- combineLinear fc linvars_in         let lhstm_lin = setLinear linvars lhstm         let lhsty_lin = setLinear linvars lhsty          logTerm 3 "LHS term" lhstm_lin         logTerm 5 "LHS type" lhsty_lin         setHoleLHS (bindEnv fc env lhstm_lin)          ext <- extendEnv env SubRefl nest lhstm_lin lhsty_lin         pure (lhs, ext) plicit : Binder (Term vars) -> PiInfo RawImpplicit (Pi _ p _) = forgetDef pplicit (PVar _ p _) = forgetDef pplicit _ = Explicit bindNotReq : {vs : _} ->             FC -> Int -> Env Term vs -> (sub : SubVars pre vs) ->             List (PiInfo RawImp, Name) ->             Term vs -> (List (PiInfo RawImp, Name), Term pre)bindNotReq fc i [] SubRefl ns tm = (ns, embed tm)bindNotReq fc i (b :: env) SubRefl ns tm   = let tmptm = subst (Ref fc Bound (MN "arg" i)) tm         (ns', btm) = bindNotReq fc (1 + i) env SubRefl ns tmptm in         (ns', refToLocal (MN "arg" i) _ btm)bindNotReq fc i (b :: env) (KeepCons p) ns tm   = let tmptm = subst (Ref fc Bound (MN "arg" i)) tm         (ns', btm) = bindNotReq fc (1 + i) env p ns tmptm in         (ns', refToLocal (MN "arg" i) _ btm)bindNotReq {vs = n :: _} fc i (b :: env) (DropCons p) ns tm   = bindNotReq fc i env p ((plicit b, n) :: ns)       (Bind fc _ (Pi (multiplicity b) Explicit (binderType b)) tm) bindReq : {vs : _} ->          FC -> Env Term vs -> (sub : SubVars pre vs) ->          List (PiInfo RawImp, Name) ->          Term pre -> Maybe (List (PiInfo RawImp, Name), List Name, ClosedTerm)bindReq {vs} fc env SubRefl ns tm    = pure (ns, notLets [] _ env, abstractEnvType fc env tm)  where    notLets : List Name -> (vars : List Name) -> Env Term vars -> List Name    notLets acc [] _ = acc    notLets acc (v :: vs) (Let _ _ _ :: env) = notLets acc vs env    notLets acc (v :: vs) (_ :: env) = notLets (v :: acc) vs envbindReq {vs = n :: _} fc (b :: env) (KeepCons p) ns tm    = do b' <- shrinkBinder b p         bindReq fc env p ((plicit b, n) :: ns)            (Bind fc _ (Pi (multiplicity b) Explicit (binderType b')) tm)bindReq fc (b :: env) (DropCons p) ns tm    = bindReq fc env p ns tm -- Return whether any of the pattern variables are in a trivially empty-- type, where trivally empty means one of:--  * No constructors--  * Every constructor of the family has a return type which conflicts with--    the given constructor's typehasEmptyPat : Defs -> Env Term vars -> Term vars -> Core BoolhasEmptyPat defs env (Bind fc x (PVar c p ty) sc)   = pure $ !(isEmpty defs !(nf defs env ty))            || !(hasEmptyPat defs (PVar c p ty :: env) sc)hasEmptyPat defs env _ = pure False -- For checking with blocks as nested namesapplyEnv : {auto c : Ref Ctxt Defs} ->           Env Term vars -> Name ->           Core (Name, (Maybe Name, List Name, FC -> NameType -> Term vars))applyEnv env withname    = do n' <- resolveName withname         pure (withname, (Just withname, namesNoLet env,                  \fc, nt => applyTo fc                         (Ref fc nt (Resolved n')) env)) -- Check a pattern clause, returning the component of the 'Case' expression it-- represents, or Nothing if it's an impossible clauseexportcheckClause : {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 ->              ImpClause -> Core (Either RawImp Clause)checkClause mult hashit n opts nest env (ImpossibleClause fc lhs)    = do lhs_raw <- lhsInCurrentNS nest lhs         handleUnify           (do autoimp <- isUnboundImplicits               setUnboundImplicits True               (_, lhs) <- bindNames False lhs_raw               setUnboundImplicits autoimp                log 5 $ "Checking " ++ show lhs               logEnv 5 "In env" env               (lhstm, lhstyg) <-                           elabTerm n (InLHS mult) opts nest env                                      (IBindHere fc PATTERN lhs) Nothing               defs <- get Ctxt               lhs <- normaliseHoles defs env lhstm               if !(hasEmptyPat defs env lhs)                  then pure (Left lhs_raw)                  else throw (ValidCase fc env (Left lhs)))           (\err =>              case err of                   ValidCase _ _ _ => throw err                   _ => do defs <- get Ctxt                           if !(impossibleErrOK defs err)                              then pure (Left lhs_raw)                              else throw (ValidCase fc env (Right err)))checkClause {vars} mult hashit n opts nest env (PatClause fc lhs_in rhs)    = do (_, (vars'  ** (sub', env', nest', lhstm', lhsty'))) <-             checkLHS mult hashit n opts nest env fc lhs_in         let rhsMode = case mult of                            Rig0 => InType                            _ => InExpr         log 5 $ "Checking RHS " ++ show rhs         logEnv 5 "In env" env'          rhstm <- wrapError (InRHS fc !(getFullName (Resolved n))) $                       checkTermSub n rhsMode opts nest' env' env sub' rhs (gnf env' lhsty')         clearHoleLHS          logTerm 3 "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 (Right (MkClause env' lhstm' rhstm))-- TODO: (to decide) With is complicated. Move this into its own module?checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw cs)    = do (lhs, (vars'  ** (sub', env', nest', lhspat, reqty))) <-             checkLHS mult hashit n opts nest env fc lhs_in         let wmode               = case mult of                      Rig0 => InType -- treat as used in type only                      _ => InExpr          (wval, gwvalTy) <- wrapError (InRHS fc !(getFullName (Resolved n))) $                elabTermSub n wmode opts nest' env' env sub' wval_raw Nothing         clearHoleLHS          logTerm 5 "With value" wval         logTerm 3 "Required type" reqty         wvalTy <- getTerm gwvalTy         defs <- get Ctxt         wval <- normaliseHoles defs env' wval         wvalTy <- normaliseHoles defs env' wvalTy          let (wevars ** withSub) = keepOldEnv sub' (snd (findSubEnv env' wval))         logTerm 5 "With value type" wvalTy         log 5 $ "Using vars " ++ show wevars          let Just wval = shrinkTerm wval withSub             | 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")          -- Abstracting over 'wval' in the scope of bNotReq in order         -- to get the 'magic with' behaviour         let wargn = MN "warg" 0         let scenv = Pi RigW Explicit wvalTy :: wvalEnv          let bnr = bindNotReq fc 0 env' withSub [] reqty         let notreqns = fst bnr         let notreqty = snd bnr          wtyScope <- replace defs scenv !(nf defs scenv (weaken wval))                            (Local fc (Just False) _ First)                            !(nf defs scenv                                 (weaken {n=wargn} notreqty))         let bNotReq = Bind fc wargn (Pi RigW Explicit wvalTy) wtyScope          let Just (reqns, envns, wtype) = bindReq fc env' withSub [] bNotReq             | Nothing => throw (InternalError "Impossible happened: With abstraction failure #4")          -- list of argument names - 'Just' means we need to match the name         -- in the with clauses to find out what the pattern should be.         -- 'Nothing' means it's the with pattern (so wargn)         let wargNames                 = map Just reqns ++                   Nothing :: map Just notreqns          logTerm 3 "With function type" wtype         log 5 $ "Argument names " ++ show wargNames          wname <- genWithName n         widx <- addDef wname (newDef fc wname (if mult == Rig0 then Rig0 else RigW)                                      vars wtype Private None)         let rhs_in = apply (IVar fc wname)                        (map (IVar fc) envns ++                         map (maybe wval_raw (\pn => IVar fc (snd pn))) wargNames)          log 3 $ "Applying to with argument " ++ show rhs_in         rhs <- wrapError (InRHS fc !(getFullName (Resolved n))) $             checkTermSub n wmode opts nest' env' env sub' rhs_in                          (gnf env' reqty)          -- Generate new clauses by rewriting the matched arguments         cs' <- traverse (mkClauseWith 1 wname wargNames lhs) cs         log 3 $ "With clauses: " ++ show cs'          -- Elaborate the new definition here         nestname <- applyEnv env wname         let nest'' = record { names $= (nestname ::) } nest          let wdef = IDef fc wname cs'         processDecl [] nest'' env wdef          pure (Right (MkClause env' lhspat rhs))  where    -- If it's 'KeepCons/SubRefl' in 'outprf', that means it was in the outer    -- environment so we need to keep it in the same place in the 'with'    -- function. Hence, turn it to KeepCons whatever    keepOldEnv : (outprf : SubVars outer vs) -> SubVars vs' vs ->                 (vs'' : List Name ** SubVars vs'' vs)    keepOldEnv {vs} SubRefl p = (vs ** SubRefl)    keepOldEnv {vs} p SubRefl = (vs ** SubRefl)    keepOldEnv (DropCons p) (DropCons p')        = let (_ ** rest) = keepOldEnv p p' in              (_ ** DropCons rest)    keepOldEnv (DropCons p) (KeepCons p')        = let (_ ** rest) = keepOldEnv p p' in              (_ ** KeepCons rest)    keepOldEnv (KeepCons p) (DropCons p')        = let (_ ** rest) = keepOldEnv p p' in              (_ ** KeepCons rest)    keepOldEnv (KeepCons p) (KeepCons p')        = let (_ ** rest) = keepOldEnv p p' in              (_ ** KeepCons rest)     -- Rewrite the clauses in the block to use an updated LHS.    -- 'drop' is the number of additional with arguments we expect (i.e.    -- the things to drop from the end before matching LHSs)    mkClauseWith : (drop : Nat) -> Name -> List (Maybe (PiInfo RawImp, Name)) ->                   RawImp -> ImpClause ->                   Core ImpClause    mkClauseWith drop wname wargnames lhs (PatClause ploc patlhs rhs)

Lines 1–500 of 737. Load more