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