\import Logic.Meta

-- | `later meta args` defers the invocation of `meta args`
\meta later 

{- |
  `fails meta args` succeeds if and only if `meta args` fails
  
  `fails {T} meta args` succeeds if and only if `meta args : T` fails
-}
\meta fails 

-- | `using (e_1, ... e_n) e` adds `e_1`, ... `e_n` to the context before checking `e`
\meta using 

-- | `usingOnly (e_1, ... e_n) e` replaces the context with `e_1`, ... `e_n` before checking `e`
\meta usingOnly 

-- | `hiding (x_1, ... x_n) e` hides local variables `x_1`, ... `x_n` from the context before checking `e`
\meta hiding 

-- | `run { e_1, ... e_n }` is equivalent to `e_1 $ e_2 $ ... $ e_n`
\meta run 

-- | `((f_1, ... f_n) at x) r` replaces variable `x` with `f_1 (... (f_n x) ...)` and runs `r` in the modified context
\meta \infix  at 

-- | `f in x` is equivalent to `\let r => f x \in r`. Also, `(f_1, ... f_n) in x` is equivalent to `f_1 in ... f_n in x`. This meta is usually used with `f` being a meta such as `rewrite`, `simplify`, `simp_coe`, or `unfold`.
\meta \infixr  in 

{- |
  `cases args default` works just like `mcases args default`, but does not search for \case expressions or definition invocations.
  Each argument has a set of parameters that can be configured.
  Parameters are specified after keyword 'arg' which is written after the argument.
  Available parameters are 'addPath', 'name', and 'as'.
  Parameter 'name' can be used to specify the name of the argument which can be used in types of subsequent arguments.
  Parameter 'as' can be used to specify an \as-name that will be added to corresponding patterns in each clause.
  The type of an argument is specified as either `e : E` or `e arg parameters : E`.
  The flag 'addPath' indicates that argument `idp` with type `e = x` should be added after the current one, where `e` is the current argument and `x` is its name.
  That is, `cases (e arg addPath)` is equivalent to `cases (e arg (name = x), idp : e = x)`.
-}
\meta cases => _ constructor

{- |
  `mcases {def} args default \with { ... }` finds all invocations of definition `def` in the expected type and generate a \case expression that matches arguments of those invocations.
  
  It matches only those arguments which are matched in `def`.
  If the explicit argument is omitted, then `mcases` searches for \case expressions instead of definition invocations.
  `default` is an optional argument which is used as a default result for missing clauses.
  The list of clauses after \with can be omitted if the default expression is specified.
  `args` is a comma-separated list of expressions (which can be omitted) that will be additionally matched in the resulting \case expressions.
  These arguments are written in the same syntax as arguments in `cases`.
  `mcases` also searches for occurrences of `def` in the types of these additional expressions.
  Parameters of found arguments can be specified in the second implicit argument.
  The syntax is similar to the syntax for arguments in `cases`, but the expression should be omitted.
  If the first implicit argument is `_`, it will be skipped.
  `mcases {def_1, ... def_n}` searches for occurrences of definitions `def_1`, ... `def_n`.
  `mcases {def, i_1, ... i_n}` matches arguments only of `i_1`-th, ... `i_n`-th occurrences of `def`.
  For example,
  * `mcases {(def1,4),def2,(def3,1,2)}` looks for the 4th occurrence of `def1`, all occurrences of `def2`, and the first and the second occurrence of `def3`.
  * `mcases {(1,2),(def,1)}` looks for the first and the second occurrence of a \case expression and the first occurrence of `def`.
  * `mcases {(def1,2),(),def2}` looks for the second occurrence of `def1`, all occurrences of \case expressions, and all occurrences of `def2`.
  * `mcases {_} {arg addPath, arg (), arg addPath}` looks for case expressions and adds a path argument after the first and the third matched expression.
-}
\meta mcases => _ constructor

{- |
  `unfold (f_1, ... f_n) e` unfolds functions/fields/variables `f_1`, ... `f_n` in the expected type before type-checking of `e` and returns `e` itself.
  If the first argument is omitted, it unfold all fields.
  If the expected type is unknown, it unfolds these function in the result type of `e`.
-}
\meta unfold 

-- | Unfolds \let expressions
\meta unfold_let 

-- | Unfolds recursively top-level functions and fields
\meta unfolds 

{- |
  `x <|> y` invokes `x` and if it fails, invokes `y`
  Also, `(x <|> y) z_1 ... z_n` is equivalent to `x z_1 ... z_n <|> z_1 ... z_n`
-}
\meta \infixr  <|> 

-- | The same as {<|>}
\meta try 

{- |
  Inserts data type arguments in constructor invocation.
  If constructor `con` has 3 data type arguments, then `mkcon con args` is equivalent to `con {_} {_} {_} args`
-}
\meta mkcon 

{- |
  * `assumption` searches for a proof in the context. It tries variables that are declared later first.
  * `assumption` {n} returns the n-th variables from the context counting from the end.
  * `assumption` {n} a1 ... ak applies n-th variable from the context to arguments a1, ... ak.
-}
\meta assumption 

-- | `defaultImpl C F E` returns the default implementation of field `F` in class `C` applied to expression `E`. The third argument can be omitted, in which case either `\this` or `_` will be used instead,
\meta defaultImpl