0 | module Idrall.Derive.Common
  1 |
  2 | import Language.Reflection
  3 | import Data.List1
  4 | import public Data.String
  5 |
  6 | %language ElabReflection
  7 |
  8 | %hide Data.List.lookup
  9 |
 10 | ---------------------------------------------------
 11 | -- from idris2-elab-util Language.Reflection.Syntax
 12 | ---------------------------------------------------
 13 |
 14 | ||| Named type.
 15 | |||
 16 | ||| This is an alias for `MkTyp EmptyFC`.
 17 | export
 18 | mkTy : (n : Name) -> (ty : TTImp) -> ITy
 19 | mkTy = MkTy EmptyFC . MkFCVal EmptyFC
 20 |
 21 | ||| Creates a variable from the given name
 22 | |||
 23 | ||| Names are best created using quotes: `{ AName },
 24 | ||| `{ In.Namespacs.Name }.
 25 | |||
 26 | ||| Likewise, if the name is already known at the time of
 27 | ||| writing, use quotes for defining variables directly: `(AName)
 28 | export
 29 | var : Name -> TTImp
 30 | var = IVar EmptyFC
 31 |
 32 | public export
 33 | FromString Name where
 34 |   fromString s = run (split ('.' ==) s) []
 35 |     where run : List1 String -> List String -> Name
 36 |           run (h ::: []) []        = UN $ Basic h
 37 |           run (h ::: []) ns        = NS (MkNS ns) (UN $ Basic h)
 38 |           run (h ::: (y :: ys)) xs = run (y ::: ys) (h :: xs)
 39 |
 40 | ||| Alias for `var . fromString`
 41 | export
 42 | varStr : String -> TTImp
 43 | varStr = var . fromString
 44 |
 45 | ||| A pattern clause consisting of the left-hand and
 46 | ||| right-hand side of the pattern arrow "=>".
 47 | |||
 48 | ||| This is an alias for `PatClause EmptyFC`.
 49 | export
 50 | patClause : (lhs : TTImp) -> (rhs : TTImp) -> Clause
 51 | patClause = PatClause EmptyFC
 52 | ------
 53 |
 54 | ||| from idris2-lsp
 55 | export
 56 | stripNs : Name -> Name
 57 | stripNs (NS _ x) = x
 58 | stripNs x = x
 59 |
 60 | ||| from idris2-lsp
 61 | covering
 62 | export
 63 | genReadableSym : String -> Elab Name
 64 | genReadableSym hint = do
 65 |   MN v i <- genSym hint
 66 |     | _ => fail "cannot generate readable argument name"
 67 |   pure $ UN $ Basic (v ++ show i)
 68 |
 69 | ||| from idris2-lsp
 70 | export
 71 | primStr : String -> TTImp
 72 | primStr = IPrimVal EmptyFC . Str
 73 |
 74 | ||| from idris2-lsp
 75 | export
 76 | bindvar : Name -> TTImp
 77 | bindvar = IBindVar EmptyFC
 78 |
 79 | ||| from idris2-lsp
 80 | export
 81 | implicit' : TTImp
 82 | implicit' = Implicit EmptyFC True
 83 |
 84 | ||| moved from where clause
 85 | export
 86 | getArgs : TTImp -> Elab (List (Name, TTImp))
 87 | getArgs (IPi _ _ _ (Just n) argTy retTy) = ((n, argTy) ::) <$> getArgs retTy
 88 | getArgs (IPi _ _ _ Nothing _ _) = fail $ "All arguments must be explicitly named"
 89 | getArgs _ = pure []
 90 |
 91 | public export
 92 | Cons : Type
 93 | Cons = (List (Name, List (Name, TTImp)))
 94 |
 95 | export
 96 | logCons : Cons -> Elab ()
 97 | logCons [] = do
 98 |   pure ()
 99 | logCons (x :: xs) = do
100 |   more x
101 |   logCons xs
102 | where
103 |   go : List (Name, TTImp) -> Elab ()
104 |   go [] =  pure ()
105 |   go ((n, t) :: ys) = do
106 |     logMsg "" 7 ("ArgName: " ++ show n)
107 |     logTerm "" 7 "ArgType" t
108 |     go ys
109 |   more : (Name, List (Name, TTImp)) -> Elab ()
110 |   more (constructor', args) = do
111 |     logMsg "" 7 ("Constructor: " ++ show constructor')
112 |     go args
113 |
114 | ||| Used with FromDhall interface, to dervice implementations
115 | ||| for ADTs or Records
116 | public export
117 | data IdrisType
118 |   = ADT
119 |   | Record
120 |
121 | public export
122 | record Options where
123 |   constructor MkOptions
124 |   ||| This function is used to adjust constructor argument names
125 |   ||| during encoding and decoding
126 |   fieldNameModifier          : String -> String
127 |
128 | export
129 | defaultOptions : Options
130 | defaultOptions = MkOptions id
131 |
132 |