Agda-2.8.0: A dependently typed functional programming language and proof assistant

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 `String` rather than `Expr` because the give action expects a string.
MimerClauses QName [Clause] |
MimerList [(Int, String)] |
MimerNoResult |

#### Instances

Instances details

PrettyTCM MimerResult Source # |
Instance details Defined in Agda.Mimer.Mimer Methods prettyTCM :: MonadPretty m => MimerResult -> m Doc Source #
NFData MimerResult Source # |
Instance details Defined in Agda.Mimer.Mimer Methods rnf :: MimerResult -> () Source #
Generic MimerResult Source # |

Instance details

Defined in Agda.Mimer.Mimer

Associated Types

type Rep MimerResult |

Instance details

Defined in Agda.Mimer.Mimer

type Rep MimerResult = D1 ('MetaData "MimerResult" "Agda.Mimer.Mimer" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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)))

Methods

from :: MimerResult -> Rep MimerResult x Source #

to :: Rep MimerResult x -> MimerResult Source #

type Rep MimerResult Source # |

Instance details

Defined in Agda.Mimer.Mimer

type Rep MimerResult = D1 ('MetaData "MimerResult" "Agda.Mimer.Mimer" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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)))

mimer Source #

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.