0 | module Core.Case.Util
 1 |
 2 | import Core.Case.CaseTree
 3 | import Core.Context
 4 | import Core.Value
 5 |
 6 | import Libraries.Data.List.SizeOf
 7 |
 8 | public export
 9 | record DataCon where
10 |   constructor MkDataCon
11 |   name  : Name
12 |   tag   : Int
13 |   arity : Nat
14 |
15 | ||| Given a normalised type, get all the possible constructors for that
16 | ||| type family, with their type, name, tag, and arity.
17 | export
18 | getCons : Defs -> NF vars -> Core (List DataCon)
19 | getCons defs (NTCon _ tn _ _)
20 |     = case !(lookupDefExact tn (gamma defs)) of
21 |            Just (TCon _ _ _ _ _ cons _) =>
22 |                 do cs' <- traverse addTy (fromMaybe [] cons)
23 |                    pure (catMaybes cs')
24 |            _ => throw (InternalError "Called `getCons` on something that is not a Type constructor")
25 |   where
26 |     addTy : Name -> Core (Maybe DataCon)
27 |     addTy cn
28 |         = do Just gdef <- lookupCtxtExact cn (gamma defs)
29 |                   | _ => pure Nothing
30 |              case (gdef.definition, gdef.type) of
31 |                   (DCon t arity _, ty) =>
32 |                         pure . Just $ MkDataCon cn t arity
33 |                   _ => pure Nothing
34 | getCons defs _ = pure []
35 |
36 | emptyRHS : FC -> CaseTree vars -> CaseTree vars
37 | emptyRHS fc (Case idx el sc alts) = Case idx el sc (map emptyRHSalt alts)
38 |   where
39 |     emptyRHSalt : CaseAlt vars -> CaseAlt vars
40 |     emptyRHSalt (ConCase n t args sc) = ConCase n t args (emptyRHS fc sc)
41 |     emptyRHSalt (DelayCase c arg sc) = DelayCase c arg (emptyRHS fc sc)
42 |     emptyRHSalt (ConstCase c sc) = ConstCase c (emptyRHS fc sc)
43 |     emptyRHSalt (DefaultCase sc) = DefaultCase (emptyRHS fc sc)
44 | emptyRHS fc (STerm i s) = STerm i (Erased fc Placeholder)
45 | emptyRHS fc sc = sc
46 |
47 | export
48 | mkAlt : FC -> CaseTree vars -> DataCon -> CaseAlt vars
49 | mkAlt fc sc (MkDataCon cn t ar)
50 |     = ConCase cn t (map (MN "m") (take ar [0..]))
51 |               (weakenNs (map take) (emptyRHS fc sc))
52 |
53 | export
54 | tagIs : Int -> CaseAlt vars -> Bool
55 | tagIs t (ConCase _ t' _ _) = t == t'
56 | tagIs t (ConstCase {}) = False
57 | tagIs t (DelayCase {}) = False
58 | tagIs t (DefaultCase _) = True
59 |