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.Alternative -- From Data.List.Ex, needed for LogPosition Con to work
  8 | import public Data.List.Quantifiers
  9 | import public Data.List1
 10 | import public Data.String
 11 | import public Data.Vect
 12 |
 13 | import public Deriving.Show
 14 |
 15 | import public Language.Reflection
 16 | import Language.Reflection.Expr
 17 | import Language.Reflection.Logging
 18 | import public Language.Reflection.Syntax
 19 | import public Language.Reflection.Syntax.Ops
 20 |
 21 | %default total
 22 |
 23 | %language ElabReflection
 24 |
 25 | --------------------------------------------------------------------------------
 26 | --          General Types
 27 | --------------------------------------------------------------------------------
 28 |
 29 | ||| Constructor of a data type
 30 | public export
 31 | record Con where
 32 |   constructor MkCon
 33 |   name : Name
 34 |   args : List Arg
 35 |   type : TTImp
 36 |
 37 | export %hint
 38 | countShow : Show Count
 39 | countShow = %runElab derive
 40 |
 41 | export %hint
 42 | piInfoShow : Show a => Show (PiInfo a)
 43 | piInfoShow = %runElab derive
 44 |
 45 | export %hint
 46 | argShow : Show Arg
 47 | argShow = %runElab derive
 48 |
 49 | export %hint
 50 | conShow : Show Con
 51 | conShow = %runElab derive
 52 |
 53 | ||| Tries to lookup a constructor by name.
 54 | export
 55 | getCon : Elaboration m => Name -> m Con
 56 | getCon n = do (n', tt) <- lookupName n
 57 |               let (args, tpe) = unPi $ cleanupNamedHoles tt
 58 |               pure $ MkCon n' args tpe
 59 |
 60 | export
 61 | LogPosition Con where
 62 |   logPosition con = do
 63 |     let fullName = show con.name
 64 |     let fullName' = unpack fullName
 65 |     maybe fullName (pack . flip drop fullName' . S . finToNat) $ findLastIndex (== '.') fullName'
 66 |
 67 | ||| Information about a data type
 68 | |||
 69 | ||| @name : Name of the data type
 70 | |||         Note: There is no guarantee that the name will be fully
 71 | |||         qualified
 72 | ||| @args : Type arguments of the data type
 73 | ||| @cons : List of data constructors
 74 | public export
 75 | record TypeInfo where
 76 |   constructor MkTypeInfo
 77 |   name : Name
 78 |   args : List Arg
 79 |   cons : List Con
 80 |
 81 | export
 82 | LogPosition TypeInfo where
 83 |   logPosition = show . name
 84 |
 85 | export %hint
 86 | tiShow : Show TypeInfo
 87 | tiShow = %runElab derive
 88 |
 89 | ||| Tries to get information about the data type specified
 90 | ||| by name. The name need not be fully qualified, but
 91 | ||| needs to be unambiguous.
 92 | export
 93 | getInfo' : Elaboration m => Name -> m TypeInfo
 94 | getInfo' n = do
 95 |   (n',tt)        <- lookupName n
 96 |   let (args,IType _) = unPi $ cleanupNamedHoles tt
 97 |     | (_,_) => fail "Type declaration does not end in IType"
 98 |   conNames       <- getCons n'
 99 |   cons           <- traverse getCon conNames
100 |   pure (MkTypeInfo n' args cons)
101 |
102 | ||| macro version of `getInfo'`
103 | export %macro
104 | getInfo : Name -> Elab TypeInfo
105 | getInfo = getInfo'
106 |
107 | --- Namedness property ---
108 |
109 | public export
110 | data ConArgsNamed : Con -> Type where
111 |   TheyAreNamed : All IsNamedArg ars -> ConArgsNamed $ MkCon nm ars ty
112 |
113 | public export
114 | areConArgsNamed : (con : Con) -> Dec $ ConArgsNamed con
115 | areConArgsNamed $ MkCon _ ars _ with (all isNamedArg ars)
116 |   _ | Yes ars' = Yes $ TheyAreNamed ars'
117 |   _ | No nars  = No $ \(TheyAreNamed ars') => nars ars'
118 |
119 | public export
120 | 0 conArgsNamed : (0 _ : ConArgsNamed c) => All IsNamedArg c.args
121 | conArgsNamed @{TheyAreNamed p} = p
122 |
123 | public export
124 | data AllTyArgsNamed : TypeInfo -> Type where
125 |   TheyAllAreNamed : All IsNamedArg ars -> All ConArgsNamed cns -> AllTyArgsNamed $ MkTypeInfo nm ars cns
126 |
127 | public export
128 | areAllTyArgsNamed : (ty : TypeInfo) -> Dec $ AllTyArgsNamed ty
129 | areAllTyArgsNamed $ MkTypeInfo _ ars cns with (all isNamedArg ars, all areConArgsNamed cns)
130 |   _ | (Yes ars', Yes cns') = Yes $ TheyAllAreNamed ars' cns'
131 |   _ | (No nars, _) = No $ \(TheyAllAreNamed ars' _) => nars ars'
132 |   _ | (_, No ncns) = No $ \(TheyAllAreNamed _ cns') => ncns cns'
133 |
134 | public export
135 | 0 (.tyArgsNamed) : (0 _ : AllTyArgsNamed t) -> All IsNamedArg t.args
136 | (.tyArgsNamed) (TheyAllAreNamed at ct) = at
137 |
138 | public export
139 | 0 (.tyConArgsNamed) : (0 _ : AllTyArgsNamed t) -> All ConArgsNamed t.cons
140 | (.tyConArgsNamed) (TheyAllAreNamed at ct) = ct
141 |
142 | -------------------------------------
143 | --- Working around type inference ---
144 | -------------------------------------
145 |
146 | public export %inline
147 | (.tyName) : TypeInfo -> Name
148 | (.tyName) = name
149 |
150 | public export %inline
151 | (.tyArgs) : TypeInfo -> List Arg
152 | (.tyArgs) = args
153 |
154 | public export %inline
155 | (.tyCons) : TypeInfo -> List Con
156 | (.tyCons) = cons
157 |
158 | public export %inline
159 | (.conArgs) : Con -> List Arg
160 | (.conArgs) = args
161 |
162 | export
163 | [ConEqByName] Eq Con where
164 |   (==) = (==) `on` name
165 |
166 | export
167 | [ConOrdByName] Ord Con using ConEqByName where
168 |   compare = comparing name
169 |