0 | -- This module should've be called `*.Con`, since it serves the `Con` data type,
  1 | -- but due to a need of compatibility with some lame OSes, we named it like this
  2 | module Language.Reflection.Compat.Constr
  3 |
  4 | import public Data.List.Elem
  5 | import public Data.So
  6 |
  7 | import public Language.Reflection.Compat
  8 | import Language.Reflection.Expr
  9 |
 10 | import public Syntax.IHateParens.List
 11 |
 12 | %default total
 13 |
 14 | --------------------------------------------
 15 | --- Compiler-based `Con` transformations ---
 16 | --------------------------------------------
 17 |
 18 | export
 19 | normaliseCon : Elaboration m => Con -> m Con
 20 | normaliseCon orig@(MkCon n args ty) = uncurry (MkCon n) . unPi <$> normaliseAsType (piAll ty args) `try` pure orig
 21 |
 22 | ------------------------------------
 23 | --- Syntactic analysis of `Con`s ---
 24 | ------------------------------------
 25 |
 26 | export
 27 | conSubexprs : Con -> List TTImp
 28 | conSubexprs con = map type con.args ++ map getExpr (snd $ unAppAny con.type)
 29 |
 30 | ||| Calculate constructor signature
 31 | export
 32 | (.sig) : Con -> TTImp
 33 | con.sig = piAll con.type con.args
 34 |
 35 | ||| Calculate constructor ITy
 36 | export
 37 | (.iTy) : Con -> ITy
 38 | con.iTy = mkTy .| dropNS con.name .| con.sig
 39 |
 40 | --------------------------------------
 41 | --- Compile-time constructors info ---
 42 | --------------------------------------
 43 |
 44 | --- Constructor argument with nice literals ---
 45 |
 46 | public export
 47 | record ConArg (0 con : Con) where
 48 |   constructor MkConArg
 49 |   conArgIdx : Fin con.args.length
 50 |
 51 | namespace ConArg
 52 |
 53 |   public export
 54 |   fromInteger : (x : Integer) -> (0 _ : So $ integerLessThanNat x con.args.length) => ConArg con
 55 |   fromInteger x = MkConArg $ fromInteger x
 56 |
 57 |   elemToFin : Elem e xs -> Fin xs.length
 58 |   elemToFin Here      = FZ
 59 |   elemToFin (There x) = FS $ elemToFin x
 60 |
 61 |   public export
 62 |   fromName : (n : Name) -> Elem (Just n) (map Arg.name con.args) => ConArg con
 63 |   fromName _ @{e} = MkConArg $ rewrite sym $ lengthMap con.args in elemToFin e
 64 |
 65 |   -- this function is not exported because it breaks type inference in polymorphic higher-kinded case,
 66 |   -- but we still leave this a) in a hope that type inference would be improved; b) to make sure we still can implement it.
 67 |   --public export
 68 |   fromString : (n : String) -> Elem (Just $ fromString n) (map Arg.name con.args) => ConArg con
 69 |   fromString n = fromName $ fromString n
 70 |
 71 | --- Getting full names of a data constructor ---
 72 |
 73 | dataCon : Name -> Elab Name
 74 | dataCon n = do
 75 |   [n] <- mapMaybe id <$> (traverse isAccessibleDataCon =<< getInfo n)
 76 |     | [] => fail "Not found data constructor `\{n}`"
 77 |     | ns => fail "Ambiguous data constructors: \{joinBy ", " $ show <$> ns}"
 78 |   pure n
 79 |
 80 |   where
 81 |     isAccessibleDataCon : (Name, NameInfo) -> Elab $ Maybe Name
 82 |     isAccessibleDataCon (n, MkNameInfo $ DataCon {}) = (catch (check {expected=()} `(let x = ~(var n) in ())) $> n) @{Compose}
 83 |     isAccessibleDataCon _                            = pure Nothing
 84 |
 85 | export %macro (.dataCon) : Name -> Elab Name; (.dataCon) = dataCon
 86 |
 87 | --- Information about constructors ---
 88 |
 89 | public export
 90 | record IsConstructor (0 n : Name) where
 91 |   constructor ItIsCon
 92 |   typeInfo : TypeInfo
 93 |   conInfo  : Con
 94 |
 95 | namespace IsConstructor
 96 |   export
 97 |   data GenuineProof : IsConstructor n -> Type where
 98 |     ItIsGenuine : GenuineProof iscn
 99 |
100 | export %macro
101 | itIsConstructor : {n : Name} -> Elab (con : IsConstructor n ** GenuineProof con)
102 | itIsConstructor = do
103 |   cn <- dataCon n
104 |   let True = n == cn
105 |     | False => fail "Name `\{show n}` is not a full name, use either `\{show cn}` or macro `.dataCon`"
106 |   con <- getCon cn
107 |   let (IVar _ ty, _) = unAppAny con.type
108 |     | (lhs, _) => fail "Can't get type name: \{show lhs}"
109 |   ty <- getInfo' ty
110 |   pure (ItIsCon ty con ** ItIsGenuine)
111 |