0 | ||| This module contains copies of the pre-overhaul definitions of the `elab-util` library and/or code derived from these copies
  1 | ||| (the overhaul is this one: https://github.com/stefan-hoeck/idris2-elab-util/pull/56).
  2 | ||| This is done due to be able to migrate to the newer `elab-util` slowly, using both old and new definitions.
  3 | |||
  4 | ||| This copying is done with the permission of Stefan Höck, the author and copyright holder of the `elab-util` library.
  5 | module Language.Reflection.Compat
  6 |
  7 | import public Data.List.Quantifiers
  8 | import public Data.List1
  9 | import public Data.String
 10 | import public Data.Vect
 11 |
 12 | import public Language.Reflection
 13 | import Language.Reflection.Expr
 14 | import Language.Reflection.Logging
 15 | import public Language.Reflection.Syntax
 16 | import public Language.Reflection.Syntax.Ops
 17 |
 18 | %default total
 19 |
 20 | --------------------------------------------------------------------------------
 21 | --          General Types
 22 | --------------------------------------------------------------------------------
 23 |
 24 | ||| Constructor of a data type
 25 | public export
 26 | record Con where
 27 |   constructor MkCon
 28 |   name : Name
 29 |   args : List Arg
 30 |   type : TTImp
 31 |
 32 | ||| Tries to lookup a constructor by name.
 33 | export
 34 | getCon : Elaboration m => Name -> m Con
 35 | getCon n = do (n', tt) <- lookupName n
 36 |               let (args, tpe) = unPi $ cleanupNamedHoles tt
 37 |               pure $ MkCon n' args tpe
 38 |
 39 | export
 40 | LogPosition Con where
 41 |   logPosition con = do
 42 |     let fullName = show con.name
 43 |     let fullName' = unpack fullName
 44 |     maybe fullName (pack . flip drop fullName' . S . finToNat) $ findLastIndex (== '.') fullName'
 45 |
 46 | ||| Information about a data type
 47 | |||
 48 | ||| @name : Name of the data type
 49 | |||         Note: There is no guarantee that the name will be fully
 50 | |||         qualified
 51 | ||| @args : Type arguments of the data type
 52 | ||| @cons : List of data constructors
 53 | public export
 54 | record TypeInfo where
 55 |   constructor MkTypeInfo
 56 |   name : Name
 57 |   args : List Arg
 58 |   cons : List Con
 59 |
 60 | export
 61 | LogPosition TypeInfo where
 62 |   logPosition = show . name
 63 |
 64 | ||| Tries to get information about the data type specified
 65 | ||| by name. The name need not be fully qualified, but
 66 | ||| needs to be unambiguous.
 67 | export
 68 | getInfo' : Elaboration m => Name -> m TypeInfo
 69 | getInfo' n = do
 70 |   (n',tt)        <- lookupName n
 71 |   let (args,IType _) = unPi $ cleanupNamedHoles tt
 72 |     | (_,_) => fail "Type declaration does not end in IType"
 73 |   conNames       <- getCons n'
 74 |   cons           <- traverse getCon conNames
 75 |   pure (MkTypeInfo n' args cons)
 76 |
 77 | ||| macro version of `getInfo'`
 78 | export %macro
 79 | getInfo : Name -> Elab TypeInfo
 80 | getInfo = getInfo'
 81 |
 82 | --- Namedness property ---
 83 |
 84 | public export
 85 | data ConArgsNamed : Con -> Type where
 86 |   TheyAreNamed : All IsNamedArg ars -> ConArgsNamed $ MkCon nm ars ty
 87 |
 88 | public export
 89 | areConArgsNamed : (con : Con) -> Dec $ ConArgsNamed con
 90 | areConArgsNamed $ MkCon _ ars _ with (all isNamedArg ars)
 91 |   _ | Yes ars' = Yes $ TheyAreNamed ars'
 92 |   _ | No nars  = No $ \(TheyAreNamed ars') => nars ars'
 93 |
 94 | public export
 95 | 0 conArgsNamed : (0 _ : ConArgsNamed c) => All IsNamedArg c.args
 96 | conArgsNamed @{TheyAreNamed p} = p
 97 |
 98 | public export
 99 | data AllTyArgsNamed : TypeInfo -> Type where
100 |   TheyAllAreNamed : All IsNamedArg ars -> All ConArgsNamed cns -> AllTyArgsNamed $ MkTypeInfo nm ars cns
101 |
102 | public export
103 | areAllTyArgsNamed : (ty : TypeInfo) -> Dec $ AllTyArgsNamed ty
104 | areAllTyArgsNamed $ MkTypeInfo _ ars cns with (all isNamedArg ars, all areConArgsNamed cns)
105 |   _ | (Yes ars', Yes cns') = Yes $ TheyAllAreNamed ars' cns'
106 |   _ | (No nars, _) = No $ \(TheyAllAreNamed ars' _) => nars ars'
107 |   _ | (_, No ncns) = No $ \(TheyAllAreNamed _ cns') => ncns cns'
108 |
109 | public export
110 | 0 (.tyArgsNamed) : (0 _ : AllTyArgsNamed t) -> All IsNamedArg t.args
111 | (.tyArgsNamed) (TheyAllAreNamed at ct) = at
112 |
113 | public export
114 | 0 (.tyConArgsNamed) : (0 _ : AllTyArgsNamed t) -> All ConArgsNamed t.cons
115 | (.tyConArgsNamed) (TheyAllAreNamed at ct) = ct
116 |
117 | -------------------------------------
118 | --- Working around type inference ---
119 | -------------------------------------
120 |
121 | public export %inline
122 | (.tyName) : TypeInfo -> Name
123 | (.tyName) = name
124 |
125 | public export %inline
126 | (.tyArgs) : TypeInfo -> List Arg
127 | (.tyArgs) = args
128 |
129 | public export %inline
130 | (.tyCons) : TypeInfo -> List Con
131 | (.tyCons) = cons
132 |
133 | public export %inline
134 | (.conArgs) : Con -> List Arg
135 | (.conArgs) = args
136 |
137 | export
138 | [ConEqByName] Eq Con where
139 |   (==) = (==) `on` name
140 |
141 | export
142 | [ConOrdByName] Ord Con using ConEqByName where
143 |   compare = comparing name
144 |