0 | module Idrall.Derive
  1 |
  2 | import Language.Reflection
  3 | import Data.List1
  4 | import public Data.String
  5 |
  6 | import public Idrall.Derive.Common
  7 | import Idrall.Expr
  8 | import Idrall.Error
  9 | import Idrall.Eval
 10 |
 11 | %language ElabReflection
 12 |
 13 | %hide Idrall.Expr.Name
 14 | %hide Data.List.lookup
 15 |
 16 | public export
 17 | interface FromDhall a where
 18 |   fromDhall : Expr Void -> Either Error a
 19 |
 20 | fromDhallErr : Expr Void -> String -> Either Error a
 21 | fromDhallErr e str = Left $ FromDhallError (getFC e) str
 22 |
 23 | export
 24 | FromDhall Nat where
 25 |   fromDhall (ENaturalLit fc x) = pure x
 26 |   fromDhall e = fromDhallErr e "not a Nat"
 27 |
 28 | export
 29 | FromDhall Bool where
 30 |   fromDhall (EBoolLit fc x) = pure x
 31 |   fromDhall e = fromDhallErr e "not a Bool"
 32 |
 33 | export
 34 | FromDhall Integer where
 35 |   fromDhall (EIntegerLit fc x) = pure x
 36 |   fromDhall e = fromDhallErr e "not an Int"
 37 |
 38 | export
 39 | FromDhall Double where
 40 |   fromDhall (EDoubleLit fc x) = pure x
 41 |   fromDhall e = fromDhallErr e "not a Double"
 42 |
 43 | export
 44 | FromDhall String where
 45 |   fromDhall e =
 46 |     let str = strFromExpr e in
 47 |     case str of
 48 |          Nothing => fromDhallErr e "couldn't normalise string"
 49 |          (Just y) => pure y
 50 |
 51 | export
 52 | FromDhall a => FromDhall (List a) where
 53 |   fromDhall (EListLit fc _ xs) = pure $ !(traverse fromDhall xs)
 54 |   fromDhall e = fromDhallErr e "not a List"
 55 |
 56 | export
 57 | FromDhall a => FromDhall (Maybe a) where
 58 |   fromDhall (ESome fc x) =
 59 |     pure $ Just !(fromDhall x)
 60 |   fromDhall (EApp fc (ENone fc') _) = pure $ neutral
 61 |   fromDhall e = fromDhallErr e "not a Maybe"
 62 |
 63 | public export
 64 | lookupEither : Show k => Idrall.FC.FC -> k -> SortedMap k v -> Either Error v
 65 | lookupEither fc k sm =
 66 |   case lookup k sm of
 67 |        Nothing => Left $ FromDhallError fc $ "key \{show k} not found"
 68 |        (Just x) => pure x
 69 |
 70 | Alternative (Either Error) where
 71 |   empty = Left $ FromDhallError initFC "Alternative failed"
 72 |   (Left x) <|> y = y
 73 |   (Right x) <|> _ = (Right x)
 74 |
 75 | export
 76 | deriveFromDhall : IdrisType -> {default Common.defaultOptions options : Options} -> (name : Name) -> Elab ()
 77 | deriveFromDhall it {options} n =
 78 |   do [(name, _)] <- getType n
 79 |              | _ => fail "Ambiguous name"
 80 |      let funName = UN $ Basic ("fromDhall" ++ show (stripNs name))
 81 |      let objName = UN $ Basic ("__impl_fromDhall" ++ show (stripNs name))
 82 |
 83 |      conNames <- getCons name
 84 |
 85 |      -- get the constructors of the record
 86 |      -- cons : (List (Name, List (Name, TTImp)))
 87 |      cons <- for conNames $ \n => do
 88 |        [(conName, conImpl)] <- getType n
 89 |          | _ => fail $ show n ++ "constructor must be in scope and unique"
 90 |        args <- getArgs conImpl
 91 |        pure (conName, args)
 92 |
 93 |      logCons cons
 94 |
 95 |      argName <- genReadableSym "arg"
 96 |
 97 |      clauses <- genClauses it funName argName cons
 98 |
 99 |      let funClaim = IClaim $ MkFCVal EmptyFC $ MkIClaimData MW Export [Inline] (MkTy EmptyFC (NoFC funName) `(Expr Void -> Either Error ~(var name)))
100 |      -- add a catch all pattern
101 |      let funDecl = IDef EmptyFC funName (clauses ++ [patClause `(~(var funName) ~(varStr "expr")) `(Left $ FromDhallError (getFC ~(varStr "expr")) "\{show expr}")])
102 |
103 |      -- declare the fuction in the env
104 |      declare [funClaim, funDecl]
105 |      [(ifName, _)] <- getType `{FromDhall}
106 |        | _ => fail "FromDhall interface must be in scope and unique"
107 |      [NS _ (DN _ ifCon)] <- getCons ifName
108 |        | _ => fail "Interface constructor error"
109 |
110 |      -- created interface for Example, and use function we already declared
111 |      let retty = `(FromDhall ~(var name))
112 |      let objClaim = IClaim $ MkFCVal EmptyFC $ MkIClaimData MW Export [Hint True, Inline] (MkTy EmptyFC (NoFC objName) retty)
113 |      let objrhs = `(~(var ifCon) ~(var funName))
114 |      let objDecl = IDef EmptyFC objName [(PatClause EmptyFC (var objName) objrhs)]
115 |      declare [objClaim, objDecl]
116 |   where
117 |     ||| moved from where clause, used for record constuctors
118 |     genClauseRecord : Name -> Name -> List (Name, TTImp) -> Elab (TTImp)
119 |     genClauseRecord constructor' arg xs = do
120 |           let rhs = foldr (\(n, type), acc =>
121 |                             let name = primStr $ options.fieldNameModifier (show n) in
122 |                                 case type of
123 |                                      _ => `(~acc <*> (lookupEither ~(varStr "fc") (MkFieldName ~name) ~(var arg) >>= fromDhall)))
124 |                           `(pure ~(var constructor')) xs
125 |           pure (rhs)
126 |     genClauseADT : Name -> Name -> Name -> List (Name, TTImp) -> Elab (TTImp, TTImp)
127 |     genClauseADT funName constructor' arg xs =
128 |       let cn = primStr (show $ stripNs constructor')
129 |           debug = show $ constructor'
130 |           debug2 = show $ map fst xs
131 |           lhs0 = `(~(var funName) (EField _ (EUnion _ xs) (MkFieldName ~cn)))
132 |           lhs1 = `(~(var funName) (EApp fc (EField _ (EUnion _ xs) (MkFieldName ~cn)) ~(bindvar arg)))
133 |           -- TODO lhsN for data constructors with more than 0 or 1 args
134 |           in do
135 |           case xs of
136 |                [] => pure $ (lhs0, `(pure ~(var constructor')))
137 |                ((n, _) :: []) => pure $ (lhs1, `(pure ~(var constructor') <*> fromDhall ~(var arg)))
138 |                (x :: _) => fail $ "too many args for constructor: " ++ show constructor'
139 |     genClauses : IdrisType -> Name -> Name -> Cons -> Elab (List Clause)
140 |     genClauses ADT funName arg cons = do
141 |       -- given constructors, lookup fields in dhall unions for those constructors
142 |       clausesADT <- traverse (\(cn, as) => genClauseADT funName cn arg (reverse as)) cons
143 |       pure $ map (\x => patClause (fst x) (snd x)) clausesADT
144 |     genClauses Record funName arg cons = do
145 |       -- given constructors, lookup names in dhall records for those constructors
146 |       clausesRecord <- traverse (\(cn, as) => genClauseRecord cn arg (reverse as)) cons
147 |       -- create clause from dhall to `Maybe a` using the above clauses as the rhs
148 |       pure $ pure $ patClause `(~(var funName) (ERecordLit fc ~(bindvar arg)))
149 |                               (foldl (\acc, x => `(~x)) `(Left $ FromDhallError ~(varStr "fc") "failed1") (clausesRecord)) -- not a real foldl, basically just passes that clausesRecord though, also doesn't support a record with no args
150 |