Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.Mimer.Mimer
Description
This module contains the implementation of Mimer, the current implementation of the auto interactive command (C-c C-a) and the successor of Agsy.
The overall idea is that Mimer gathers a collection of "components" that it could use for building a solution and tries to refine the goal iteratively using these components. Components include global definitions, local variables, let-bound variables, and recursive calls to the function being defined.
Mimer manages multiple branches of the search at the same time and assigns a cost to each branch, which is the sum of the costs of all its components. The cost of a component in turn is determined by its type and the number of new metas it introduces.
A branch can be refined by picking one of its unsolved metavariables and refining it with all available components, resulting in a number of new branches (each one with a higher cost than the original).
Mimer iteratively refines the branch with the lowest cost until it finds a solution or runs out of time.
Synopsis
- data MimerResult
- = MimerExpr String
- | MimerClauses QName [Clause]
- | MimerList [(Int, String)]
- | MimerNoResult
- mimer :: MonadTCM tcm => Rewrite -> InteractionId -> Range -> String -> tcm MimerResult
Documentation
data MimerResult Source #
Constructors
MimerExpr String | Returns |
MimerClauses QName [Clause] | |
MimerList [(Int, String)] | |
MimerNoResult |
Instances
PrettyTCM MimerResult Source # | |||||
Defined in Agda.Mimer.Mimer Methods prettyTCM :: MonadPretty m => MimerResult -> m Doc Source # | |||||
Generic MimerResult Source # | |||||
Defined in Agda.Mimer.Mimer Associated Types
| |||||
NFData MimerResult Source # | |||||
Defined in Agda.Mimer.Mimer Methods rnf :: MimerResult -> () | |||||
type Rep MimerResult Source # | |||||
Defined in Agda.Mimer.Mimer type Rep MimerResult = D1 ('MetaData "MimerResult" "Agda.Mimer.Mimer" "Agda-2.8.0-ES80446w7YfI1YRCZGcXTm" 'False) ((C1 ('MetaCons "MimerExpr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "MimerClauses" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Clause]))) :+: (C1 ('MetaCons "MimerList" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Int, String)])) :+: C1 ('MetaCons "MimerNoResult" 'PrefixI 'False) (U1 :: Type -> Type))) |
Arguments
:: MonadTCM tcm | |
=> Rewrite | Degree of normalization of solution terms. |
-> InteractionId | Hole to run on. |
-> Range | Range of hole (for parse errors). |
-> String | Content of hole (to parametrize Mimer). |
-> tcm MimerResult |
Entry point. Run Mimer on the given interaction point, returning the desired solution(s). Also debug prints timing statistics.