module Core.CaseBuilder import Core.CaseTreeimport Core.Contextimport Core.Coreimport Core.Envimport Core.Normaliseimport Core.TTimport Core.Value import Data.LengthMatch %default covering public exportdata Phase = CompileTime | RunTime data ArgType : List Name -> Type where     Known : RigCount -> (ty : Term vars) -> ArgType vars -- arg has type 'ty'     Stuck : (fty : Term vars) -> ArgType vars         -- ^ arg will have argument type of 'fty' when we know enough to         -- calculate it     Unknown : ArgType vars         -- arg's type is not yet known due to a previously stuck argument Show (ArgType ns) where  show (Known c t) = "Known " ++ show c ++ " " ++ show t  show (Stuck t) = "Stuck " ++ show t  show Unknown = "Unknown" record PatInfo (pvar : Name) (vars : List Name) where  constructor MkInfo  pat : Pat  loc : IsVar name idx vars  argType : ArgType vars -- Type of the argument being inspected (i.e.                         -- *not* refined by this particular pattern) Show (PatInfo n vars) where  show pi = show (pat pi) ++ " : " ++ show (argType pi) {-NamedPats is a list of patterns on the LHS of a clause. Each entry inthe list gives a pattern, and a proof that there is a variable we caninspect to see if it matches the pattern. A definition consists of a list of clauses, which are a 'NamedPats' anda term on the RHS. There is an assumption that corresponding positions inNamedPats always have the same 'Elem' proof, though this isn't expressed ina type anywhere.-} data NamedPats : List Name -> -- pattern variables still to process                 List Name -> -- the pattern variables still to process,                              -- in order                 Type where     Nil : NamedPats vars []     (::) : PatInfo pvar vars ->            -- ^ a pattern, where its variable appears in the vars list,            -- and its type. The type has no variable names; any names it            -- refers to are explicit            NamedPats vars ns -> NamedPats vars (pvar :: ns) getPatInfo : NamedPats vars todo -> List PatgetPatInfo [] = []getPatInfo (x :: xs) = pat x :: getPatInfo xs updatePats : {auto c : Ref Ctxt Defs} ->             Env Term vars ->             NF vars -> NamedPats vars todo -> Core (NamedPats vars todo)updatePats env nf [] = pure []updatePats {todo = pvar :: ns} env (NBind fc _ (Pi c _ farg) fsc) (p :: ps)  = case argType p of         Unknown =>            do defs <- get Ctxt               empty <- clearDefs defs               pure (record { argType = Known c !(quote empty env farg) } p                          :: !(updatePats env !(fsc defs (toClosure defaultOpts env (Ref fc Bound pvar))) ps))         _ => pure (p :: ps)updatePats env nf (p :: ps)  = case argType p of         Unknown =>            do defs <- get Ctxt               empty <- clearDefs defs               pure (record { argType = Stuck !(quote empty env nf) } p :: ps)         _ => pure (p :: ps) mkEnv : FC -> (vs : List Name) -> Env Term vsmkEnv fc [] = []mkEnv fc (n :: ns) = PVar RigW Explicit (Erased fc False) :: mkEnv fc ns substInPatInfo : {auto c : Ref Ctxt Defs} ->                 FC -> Name -> Term vars -> PatInfo pvar vars ->                 NamedPats vars todo ->                 Core (PatInfo pvar vars, NamedPats vars todo)substInPatInfo {pvar} {vars} fc n tm p ps    = case argType p of           Known c ty => pure (record { argType = Known c (substName n tm ty) } p, ps)           Stuck fty =>             do defs <- get Ctxt                empty <- clearDefs defs                let env = mkEnv fc vars                case !(nf defs env (substName n tm fty)) of                     NBind pfc _ (Pi c _ farg) fsc =>                       pure (record { argType = Known c !(quote empty env farg) } p,                                 !(updatePats env                                       !(fsc defs (toClosure defaultOpts env                                             (Ref pfc Bound pvar))) ps))                     _ => pure (p, ps)           Unknown => pure (p, ps) -- Substitute the name with a term in the pattern types, and reduce further-- (this aims to resolve any 'Stuck' pattern types)substInPats : {auto c : Ref Ctxt Defs} ->              FC -> Name -> Term vars -> NamedPats vars todo ->              Core (NamedPats vars todo)substInPats fc n tm [] = pure []substInPats fc n tm (p :: ps)    = do (p', ps') <- substInPatInfo fc n tm p ps         pure (p' :: !(substInPats fc n tm ps')) getPat : {idx : Nat} ->         .(IsVar name idx ps) -> NamedPats ns ps -> PatInfo name nsgetPat First (x :: xs) = xgetPat (Later p) (x :: xs) = getPat p xs dropPat : {idx : Nat} ->          .(el : IsVar name idx ps) ->          NamedPats ns ps -> NamedPats ns (dropVar ps el)dropPat First (x :: xs) = xsdropPat (Later p) (x :: xs) = x :: dropPat p xs Show (NamedPats vars todo) where  show xs = "[" ++ showAll xs ++ "]"    where      showAll : NamedPats vs ts -> String      showAll [] = ""      showAll {ts = t :: _ } [x]          = show t ++ " " ++ show (pat x) ++ " [" ++ show (argType x) ++ "]"      showAll {ts = t :: _ } (x :: xs)          = show t ++ " " ++ show (pat x) ++ " [" ++ show (argType x) ++ "]"                     ++ ", " ++ showAll xs Weaken ArgType where  weaken (Known c ty) = Known c (weaken ty)  weaken (Stuck fty) = Stuck (weaken fty)  weaken Unknown = Unknown Weaken (PatInfo p) where  weaken (MkInfo p el fty) = MkInfo p (Later el) (weaken fty) -- FIXME: perhaps 'vars' should be second argument so we can use Weaken interfaceweaken : NamedPats vars todo -> NamedPats (x :: vars) todoweaken [] = []weaken (p :: ps) = weaken p :: weaken ps weakenNs : (ns : List Name) ->           NamedPats vars todo -> NamedPats (ns ++ vars) todoweakenNs ns [] = []weakenNs ns (p :: ps)    = weakenNs ns p :: weakenNs ns ps (++) : NamedPats vars ms -> NamedPats vars ns -> NamedPats vars (ms ++ ns)(++) [] ys = ys(++) (x :: xs) ys = x :: xs ++ ys tail : NamedPats vars (p :: ps) -> NamedPats vars pstail (x :: xs) = xs take : (as : List Name) -> NamedPats vars (as ++ bs) -> NamedPats vars astake [] ps = []take (x :: xs) (p :: ps) = p :: take xs ps data PatClause : (vars : List Name) -> (todo : List Name) -> Type where     MkPatClause : List Name -> -- names matched so far (from original lhs)                   NamedPats vars todo ->                   (rhs : Term vars) -> PatClause vars todo getNPs : PatClause vars todo -> NamedPats vars todogetNPs (MkPatClause _ lhs rhs) = lhs Show (PatClause vars todo) where  show (MkPatClause _ ps rhs)     = show ps ++ " => " ++ show rhs substInClause : {auto c : Ref Ctxt Defs} ->                FC -> PatClause vars (a :: todo) ->                Core (PatClause vars (a :: todo))substInClause {vars} {a} fc (MkPatClause pvars (MkInfo pat pprf fty :: pats) rhs)    = do pats' <- substInPats fc a (mkTerm vars pat) pats         pure (MkPatClause pvars (MkInfo pat pprf fty :: pats') rhs) data Partitions : List (PatClause vars todo) -> Type where     ConClauses : (cs : List (PatClause vars todo)) ->                  Partitions ps -> Partitions (cs ++ ps)     VarClauses : (vs : List (PatClause vars todo)) ->                  Partitions ps -> Partitions (vs ++ ps)     NoClauses : Partitions [] Show (Partitions ps) where  show (ConClauses cs rest) = "CON " ++ show cs ++ ", " ++ show rest  show (VarClauses vs rest) = "VAR " ++ show vs ++ ", " ++ show rest  show NoClauses = "NONE" data ClauseType = ConClause | VarClause namesIn : List Name -> Pat -> BoolnamesIn pvars (PAs _ n p) = (n `elem` pvars) && namesIn pvars pnamesIn pvars (PCon _ _ _ _ ps) = all (namesIn pvars) psnamesIn pvars (PTyCon _ _ _ ps) = all (namesIn pvars) psnamesIn pvars (PArrow _ _ s t) = namesIn pvars s && namesIn pvars tnamesIn pvars (PDelay _ _ t p) = namesIn pvars t && namesIn pvars pnamesIn pvars (PLoc _ n) = n `elem` pvarsnamesIn pvars _ = True namesFrom : Pat -> List NamenamesFrom (PAs _ n p) = n :: namesFrom pnamesFrom (PCon _ _ _ _ ps) = concatMap namesFrom psnamesFrom (PTyCon _ _ _ ps) = concatMap namesFrom psnamesFrom (PArrow _ _ s t) = namesFrom s ++ namesFrom tnamesFrom (PDelay _ _ t p) = namesFrom t ++ namesFrom pnamesFrom (PLoc _ n) = [n]namesFrom _ = [] clauseType : Phase -> PatClause vars (a :: as) -> ClauseType-- If it's irrelevant, a constructor, and there's no names we haven't seen yet-- and don't see later, treat it as a variable-- Or, if we're compiling for runtime we won't be able to split on it, so-- also treat it as a variableclauseType phase (MkPatClause pvars (MkInfo arg _ ty :: rest) rhs)    = getClauseType phase arg ty  where    getClauseType : Phase -> Pat -> ArgType vars -> ClauseType    getClauseType CompileTime (PCon _ _ _ _ xs) (Known Rig0 t)        = if all (namesIn (pvars ++ concatMap namesFrom (getPatInfo rest))) xs             then VarClause             else ConClause    getClauseType phase (PAs _ _ p) t = getClauseType phase p t    getClauseType phase _ (Known Rig0 t) = VarClause    getClauseType phase (PCon _ _ _ _ xs) _ = ConClause    getClauseType phase (PTyCon _ _ _ xs) _ = ConClause    getClauseType phase (PConst _ x) _ = ConClause    getClauseType phase (PArrow _ _ s t) _ = ConClause    getClauseType phase (PDelay _ _ _ _) t = ConClause    getClauseType phase _ _ = VarClause partition : Phase -> (ps : List (PatClause vars (a :: as))) -> Partitions pspartition phase [] = NoClausespartition phase (x :: xs) with (partition phase xs)  partition phase (x :: (cs ++ ps)) | (ConClauses cs rest)        = case clauseType phase x of               ConClause => ConClauses (x :: cs) rest               VarClause => VarClauses [x] (ConClauses cs rest)  partition phase (x :: (vs ++ ps)) | (VarClauses vs rest)        = case clauseType phase x of               ConClause => ConClauses [x] (VarClauses vs rest)               VarClause => VarClauses (x :: vs) rest  partition phase (x :: []) | NoClauses        = case clauseType phase x of               ConClause => ConClauses [x] NoClauses               VarClause => VarClauses [x] NoClauses data ConType : Type where     CName : Name -> (tag : Int) -> ConType     CDelay : ConType     CConst : Constant -> ConType conTypeEq : (x, y : ConType) -> Maybe (x = y)conTypeEq (CName x tag) (CName x' tag')   = do Refl <- nameEq x x'        case decEq tag tag' of             Yes Refl => Just Refl             No contra => NothingconTypeEq CDelay CDelay = Just ReflconTypeEq (CConst x) (CConst y)   = case constantEq x y of          Nothing => Nothing          Just Refl => Just ReflconTypeEq _ _ = Nothing data Group : List Name -> -- variables in scope             List Name -> -- pattern variables still to process             Type where     ConGroup : Name -> (tag : Int) ->                List (PatClause (newargs ++ vars) (newargs ++ todo)) ->                Group vars todo     DelayGroup : List (PatClause (tyarg :: valarg :: vars)                                  (tyarg :: valarg :: todo)) ->                  Group vars todo     ConstGroup : Constant -> List (PatClause vars todo) ->                  Group vars todo Show (Group vars todo) where  show (ConGroup c t cs) = "Con " ++ show c ++ ": " ++ show cs  show (DelayGroup cs) = "Delay: " ++ show cs  show (ConstGroup c cs) = "Const " ++ show c ++ ": " ++ show cs data GroupMatch : ConType -> List Pat -> Group vars todo -> Type where  ConMatch : LengthMatch ps newargs ->             GroupMatch (CName n tag) ps               (ConGroup {newargs} n tag (MkPatClause pvs pats rhs :: rest))  DelayMatch : GroupMatch CDelay []               (DelayGroup {tyarg} {valarg} (MkPatClause pvs pats rhs :: rest))  ConstMatch : GroupMatch (CConst c) []                  (ConstGroup c (MkPatClause pvs pats rhs :: rest))  NoMatch : GroupMatch ct ps g checkGroupMatch : (c : ConType) -> (ps : List Pat) -> (g : Group vars todo) ->                  GroupMatch c ps gcheckGroupMatch (CName x tag) ps (ConGroup {newargs} x' tag' (MkPatClause pvs pats rhs :: rest))    = case checkLengthMatch ps newargs of           Nothing => NoMatch           Just prf => case (nameEq x x', decEq tag tag') of                            (Just Refl, Yes Refl) => ConMatch prf                            _ => NoMatchcheckGroupMatch (CName x tag) ps _ = NoMatchcheckGroupMatch CDelay [] (DelayGroup (MkPatClause pvs pats rhs :: rest))    = DelayMatchcheckGroupMatch (CConst c) [] (ConstGroup c' (MkPatClause pvs pats rhs :: rest))    = case constantEq c c' of           Nothing => NoMatch           Just Refl => ConstMatchcheckGroupMatch _ _ _ = NoMatch data PName : Type where nextName : {auto i : Ref PName Int} ->           String -> Core NamenextName root    = do x <- get PName         put PName (x + 1)         pure (MN root x) nextNames : {auto i : Ref PName Int} ->            {auto c : Ref Ctxt Defs} ->            FC -> String -> List Pat -> Maybe (NF vars) ->            Core (args ** NamedPats (args ++ vars) args)nextNames fc root [] fty = pure ([] ** [])nextNames {vars} fc root (p :: pats) fty     = do defs <- get Ctxt          empty <- clearDefs defs          n <- nextName root          let env = mkEnv fc vars          fa_tys <- the (Core (Maybe (NF vars), ArgType vars)) $              case fty of                   Nothing => pure (Nothing, Unknown)                   Just (NBind pfc _ (Pi c _ (NErased _ _)) fsc) =>                      pure (Just !(fsc defs (toClosure defaultOpts env (Ref pfc Bound n))),                        Unknown)                   Just (NBind pfc _ (Pi c _ farg) fsc) =>                      pure (Just !(fsc defs (toClosure defaultOpts env (Ref pfc Bound n))),                        Known c !(quote empty env farg))                   Just t =>                      pure (Nothing, Stuck !(quote empty env t))          (args ** ps) <- nextNames {vars} fc root pats (fst fa_tys)          let argTy = case snd fa_tys of                           Unknown => Unknown                           Known rig t => Known rig (weakenNs (n :: args) t)                           Stuck t => Stuck (weakenNs (n :: args) t)          pure (n :: args ** MkInfo p First argTy :: weaken ps) -- replace the prefix of patterns with 'pargs'newPats : (pargs : List Pat) -> LengthMatch pargs ns ->          NamedPats vars (ns ++ todo) ->          NamedPats vars nsnewPats [] NilMatch rest = []newPats (newpat :: xs) (ConsMatch w) (pi :: rest)  = record { pat = newpat} pi :: newPats xs w rest updateNames : List (Name, Pat) -> List (Name, Name)updateNames = mapMaybe update  where    update : (Name, Pat) -> Maybe (Name, Name)    update (n, PLoc fc p) = Just (p, n)    update _ = Nothing updatePatNames : List (Name, Name) -> NamedPats vars todo -> NamedPats vars todoupdatePatNames _ [] = []updatePatNames ns (pi :: ps)    = record { pat $= update } pi :: updatePatNames ns ps  where    update : Pat -> Pat    update (PAs fc n p)        = case lookup n ns of               Nothing => PAs fc n (update p)               Just n' => PAs fc n' (update p)    update (PCon fc n i a ps) = PCon fc n i a (map update ps)    update (PTyCon fc n a ps) = PTyCon fc n a (map update ps)    update (PArrow fc x s t) = PArrow fc x (update s) (update t)    update (PDelay fc r t p) = PDelay fc r (update t) (update p)    update (PLoc fc n)        = case lookup n ns of               Nothing => PLoc fc n               Just n' => PLoc fc n'    update p = p groupCons : {auto i : Ref PName Int} ->            {auto c : Ref Ctxt Defs} ->            FC -> Name ->            List Name ->            List (PatClause vars (a :: todo)) ->            Core (List (Group vars todo))groupCons fc fn pvars cs     = gc [] cs  where    addConG : Name -> (tag : Int) ->              List Pat -> NamedPats vars todo ->              (rhs : Term vars) ->              (acc : List (Group vars todo)) ->              Core (List (Group vars todo))    -- Group all the clauses that begin with the same constructor, and    -- add new pattern arguments for each of that constructor's arguments.    -- The type of 'ConGroup' ensures that we refer to the arguments by    -- the same name in each of the clauses    addConG {todo} n tag pargs pats rhs []        = do cty <- the (Core (NF vars)) $ if n == UN "->"                      then pure $ NBind fc (MN "_" 0) (Pi RigW Explicit (NType fc)) $                              (\d, a => pure $ NBind fc (MN "_" 1) (Pi RigW Explicit (NErased fc False))                                (\d, a => pure $ NType fc))                      else do defs <- get Ctxt                              Just t <- lookupTyExact n (gamma defs)                                   | Nothing => pure (NErased fc False)                              nf defs (mkEnv fc vars) (embed t)             (patnames ** newargs) <- nextNames {vars} fc "e" pargs (Just cty)             -- Update non-linear names in remaining patterns (to keep             -- explicit dependencies in types accurate)             let pats' = updatePatNames (updateNames (zip patnames pargs))                                        (weakenNs patnames pats)             let clause = MkPatClause {todo = patnames ++ todo}                              pvars                              (newargs ++ pats')                              (weakenNs patnames rhs)             pure [ConGroup n tag [clause]]    addConG {todo} n tag pargs pats rhs (g :: gs) with (checkGroupMatch (CName n tag) pargs g)      addConG {todo} n tag pargs pats rhs              ((ConGroup {newargs} n tag ((MkPatClause pvars ps tm) :: rest)) :: gs)                   | (ConMatch {newargs} lprf)        = do let newps = newPats pargs lprf ps             let pats' = updatePatNames (updateNames (zip newargs pargs))                                        (weakenNs newargs pats)             let newclause : PatClause (newargs ++ vars) (newargs ++ todo)                   = MkPatClause pvars                                 (newps ++ pats')                                 (weakenNs newargs rhs)             -- put the new clause at the end of the group, since we             -- match the clauses top to bottom.             pure ((ConGroup n tag (MkPatClause pvars ps tm :: rest ++ [newclause]))                         :: gs)      addConG n tag pargs pats rhs (g :: gs) | NoMatch        = do gs' <- addConG n tag pargs pats rhs gs             pure (g :: gs')     -- This rather ugly special case is to deal with laziness, where Delay    -- is like a constructor, but with a special meaning that it forces    -- evaluation when case analysis reaches it (dealt with in the evaluator    -- and compiler)    addDelayG : Pat -> Pat -> NamedPats vars todo ->                (rhs : Term vars) ->                (acc : List (Group vars todo)) ->                Core (List (Group vars todo))    addDelayG {todo} pty parg pats rhs []        = do let dty = NBind fc (MN "a" 0) (Pi Rig0 Explicit (NType fc)) $                        (\d, a =>                            do a' <- evalClosure d a                               pure (NBind fc (MN "x" 0) (Pi RigW Explicit a')                                       (\dv, av => pure (NDelayed fc LUnknown a'))))             ([tyname, argname] ** newargs) <- nextNames {vars} fc "e" [pty, parg]                                                  (Just dty)                | _ => throw (InternalError "Error compiling Delay pattern match")             let pats' = updatePatNames (updateNames [(tyname, pty),                                                      (argname, parg)])                                        (weakenNs [tyname, argname] pats)             let clause = MkPatClause {todo = tyname :: argname :: todo}                             pvars (newargs ++  pats')                                   (weakenNs [tyname, argname] rhs)             pure [DelayGroup [clause]]    addDelayG {todo} pty parg pats rhs (g :: gs) with (checkGroupMatch CDelay [] g)      addDelayG {todo} pty parg pats rhs          ((DelayGroup {tyarg} {valarg} ((MkPatClause pvars ps tm) :: rest)) :: gs)                 | (DelayMatch {tyarg} {valarg})         = do let newps = newPats [pty, parg] (ConsMatch (ConsMatch NilMatch)) ps              let pats' = updatePatNames (updateNames [(tyarg, pty),                                                       (valarg, parg)])                                         (weakenNs [tyarg, valarg] pats)              let newclause : PatClause (tyarg :: valarg :: vars)                                        (tyarg :: valarg :: todo)                    = MkPatClause pvars (newps ++ pats')                                        (weakenNs [tyarg, valarg] rhs)              pure ((DelayGroup (MkPatClause pvars ps tm :: rest ++ [newclause]))                         :: gs)      addDelayG pty parg pats rhs (g :: gs) | NoMatch         = do gs' <- addDelayG pty parg pats rhs gs              pure (g :: gs')     addConstG : Constant -> NamedPats vars todo ->                (rhs : Term vars) ->                (acc : List (Group vars todo)) ->                Core (List (Group vars todo))    addConstG c pats rhs []        = pure [ConstGroup c [MkPatClause pvars pats rhs]]    addConstG {todo} c pats rhs (g :: gs) with (checkGroupMatch (CConst c) [] g)

Lines 1–500 of 949. Load more