Skip to content
Permalink
Browse files

[issue 938] implement recursive instance search (without termination …

…check)
  • Loading branch information...
guillaumebrunerie committed Jul 11, 2014
1 parent 2730b7b commit 7ca60fd60aec1b73d9f14aaa6e1aeef184bcca79
Showing with 711 additions and 236 deletions.
  1. +94 −0 CHANGELOG
  2. +2 −1 src/full/Agda/Interaction/BasicOps.hs
  3. +11 −5 src/full/Agda/Interaction/Imports.hs
  4. +4 −0 src/full/Agda/Syntax/Common.hs
  5. +8 −1 src/full/Agda/Syntax/Concrete.hs
  6. +69 −22 src/full/Agda/Syntax/Concrete/Definitions.hs
  7. +1 −0 src/full/Agda/Syntax/Concrete/Generic.hs
  8. +1 −0 src/full/Agda/Syntax/Concrete/Pretty.hs
  9. +6 −1 src/full/Agda/Syntax/Info.hs
  10. +1 −0 src/full/Agda/Syntax/Parser/Lexer.x
  11. +10 −16 src/full/Agda/Syntax/Parser/Parser.y
  12. +2 −2 src/full/Agda/Syntax/Parser/Tokens.hs
  13. +11 −9 src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
  14. +39 −42 src/full/Agda/TypeChecking/InstanceArguments.hs
  15. +11 −7 src/full/Agda/TypeChecking/MetaVars.hs
  16. +4 −3 src/full/Agda/TypeChecking/MetaVars.hs-boot
  17. +22 −1 src/full/Agda/TypeChecking/Monad/Base.hs
  18. +23 −0 src/full/Agda/TypeChecking/Monad/State.hs
  19. +5 −1 src/full/Agda/TypeChecking/Pretty.hs
  20. +2 −1 src/full/Agda/TypeChecking/Reduce.hs
  21. +3 −0 src/full/Agda/TypeChecking/Rules/Data.hs
  22. +3 −5 src/full/Agda/TypeChecking/Rules/Decl.hs
  23. +3 −0 src/full/Agda/TypeChecking/Rules/Record.hs
  24. +4 −4 src/full/Agda/TypeChecking/Serialise.hs
  25. +42 −0 src/full/Agda/TypeChecking/Telescope.hs
  26. +2 −2 test/Common/Reflect.agda
  27. +1 −1 test/fail/InstanceArgumentsAmbiguous.agda
  28. +35 −0 test/fail/InstanceMeta.agda
  29. +5 −0 test/fail/InstanceMeta.err
  30. +2 −1 test/{succeed → fail}/Issue1003.agda
  31. +4 −0 test/fail/Issue1003.err
  32. 0 test/{succeed → fail}/Issue351-5.agda
  33. +3 −0 test/fail/Issue351-5.err
  34. +1 −1 test/fail/Issue551a.agda
  35. +13 −12 test/fail/Issue723.agda
  36. +4 −6 test/fail/Issue723.err
  37. +12 −0 test/fail/UnknownImplicitInstance.agda
  38. +3 −0 test/fail/UnknownImplicitInstance.err
  39. +23 −0 test/succeed/ConstructorsInstance.agda
  40. +9 −7 test/succeed/InstanceArguments.agda
  41. +5 −4 test/succeed/InstanceArgumentsConstraints.agda
  42. +2 −2 test/succeed/InstanceArgumentsHidden.agda
  43. +1 −1 test/succeed/InstanceGuessesMeta.agda
  44. +1 −1 test/succeed/InstanceGuessesMeta2.agda
  45. +26 −0 test/succeed/InstanceMetaType.agda
  46. +3 −2 test/succeed/Issue1184.agda
  47. +2 −2 test/succeed/Issue435.agda
  48. +5 −4 test/succeed/Issue509.agda
  49. +4 −4 test/succeed/Issue551b.agda
  50. +6 −4 test/succeed/Issue558.agda
  51. +9 −6 test/succeed/Issue558b.agda
  52. +3 −2 test/succeed/Issue558c.agda
  53. +0 −28 test/succeed/Issue670b.agda
  54. +1 −1 test/succeed/Issue747.agda
  55. +8 −7 test/succeed/Issue814.agda
  56. +4 −3 test/succeed/Issue899.agda
  57. +1 −1 test/succeed/NoPatternMatching.agda
  58. +3 −2 test/succeed/RecordUpdateSyntax.agda
  59. +69 −0 test/succeed/RecursiveInstanceSearch.agda
  60. +48 −0 test/succeed/RecursiveInstanceSearchLevel.agda
  61. +12 −11 test/succeed/UnquoteInstance.agda
@@ -31,6 +31,100 @@ Important changes since 2.4.0.1:
Note: Unsafe use of ETA can make Agda loop, e.g. by triggering
infinite eta expansion!

* Instance search is now more efficient and recursive (see issue 938)
(but without termination check yet)

A new keyword `instance' has been introduced (in the style of
`abstract' and `private') which must now be used for every
definition/postulate that has to be taken into account during instance
resolution. For example:

{-# OPTIONS --copatterns #-}

record RawMonoid (A : Set) : Set where
field
nil : A
_++_ : A -> A -> A
open RawMonoid

instance
rawMonoidList : {A : Set} -> RawMonoid (List A)
rawMonoidList = record { nil = []; _++_ = List._++_ }

-- using copatterns to define this recursive instance:

rawMonoidMaybe : {A : Set} {{m : RawMonoid A}} -> RawMonoid (Maybe A)
nil rawMonoidMaybe = nothing
_++_ rawMonoidMaybe nothing mb = mb
_++_ rawMonoidMaybe ma nothing = ma
_++_ (rawMonoidMaybe {{m}}) (just a) (just b) = just (_++_ m a b)

Moreover, each type of an instance must end in (something that reduces
to) a named type (e.g. a record, a datatype or a postulate). This
allows us to build a simple index structure

data/record name --> possible instances

that speeds up instance search.

Instance search takes into account all local bindings and all global
'instance' bindings and the search is recursive. For instance,
searching for

? : RawMonoid (Maybe (List A))

will consider the candidates {rawMonoidList, rawMonoidMaybe}, fail to
unify the first one, succeeding with the second one

? = rawMonoidMaybe {A = List A} {{m = ?m}} : RawMonoid (Maybe (List A))

and continue with goal

?m : RawMonoid (List A)

This will then find

?m = rawMonoidList {A = A}

and putting together we have the solution.

Be careful that there is no termination check for now, you can easily
make Agda loop by declaring the identity function as an instance. But
it shouldn’t be possible to make Agda loop by only declaring
structurally recursive instances (whatever that means).

Additionally:

* Uniqueness of instances is up to definitional equality (see issue 899)

* Instance search will not be attempted if there are unsolved metas in
the goal. The issue is that trying to typecheck [? ++ ?] would
generate a constraint of type `RawMonoid ?' to be solved by instance
search, but unification with `rawMonoidMaybe' will succeed and
generate a new constraint of type `RawMonoid ?2' to be solved by
instance search, and so on, so Agda would loop.

As a special case, if none of the instances declared for that type
is recursive, then instance search is attempted as usual even if
there are unsolved metas (no risk of looping here).

* Instances of the following form are allowed:

Π-level : {n : ℕ} {A : Set} {B : A → Set}
{{_ : (a : A) → has-level n (B a)}}
→ has-level n ((a : A) → B a)

When searching recursively for an instance of type `(a : A) →
has-level n (B a)', a lambda will automatically be introduced and
instance search will search for something of type `has-level n (B
a)' in the context extended by `a : A'.

* There is no longer any attempt to solve irrelevant metas by instance
search

* Constructors of records and datatypes are automatically added to the
instance table

* Bugs fixed (see https://code.google.com/p/agda/issues):
1203
1205
@@ -276,7 +276,8 @@ instance Reify Constraint (OutputConstraint Expr Expr) where
OpenIFS{} -> __IMPOSSIBLE__
InstS{} -> __IMPOSSIBLE__
InstV{} -> __IMPOSSIBLE__
reify (FindInScope m cands) = do
reify (FindInScope m mcands) = do
let cands = caseMaybe mcands [] (\ x -> x)
m' <- reify (MetaV m [])
ctxArgs <- getContextArgs
t <- getMetaType m
@@ -42,6 +42,7 @@ import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Monad
-- import Agda.TypeChecking.Monad.Base.KillRange -- killRange for Signature
import Agda.TypeChecking.Serialise
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.Monad.Benchmark (billTop, reimburseTop)
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
@@ -88,7 +89,7 @@ mergeInterface i = do
Just b1 = Map.lookup b bs
Just b2 = Map.lookup b bi
mapM_ check (map fst $ Map.toList $ Map.intersection bs bi)
addImportedThings sig bi (iHaskellImports i) (iPatternSyns i)
addImportedThings sig bi (iHaskellImports i) (iPatternSyns i) (iInstanceDefs i)
reportSLn "import.iface.merge" 20 $
" Rebinding primitives " ++ show prim
prim <- Map.fromList <$> mapM rebind prim
@@ -100,13 +101,14 @@ mergeInterface i = do
return (x, Prim $ pf { primFunName = q })

addImportedThings ::
Signature -> BuiltinThings PrimFun -> Set String -> A.PatternSynDefns -> TCM ()
addImportedThings isig ibuiltin hsImports patsyns =
Signature -> BuiltinThings PrimFun -> Set String -> A.PatternSynDefns -> InstanceTable -> TCM ()
addImportedThings isig ibuiltin hsImports patsyns instdefs =
modify $ \st -> st
{ stImports = unionSignatures [stImports st, isig]
, stImportedBuiltins = Map.union (stImportedBuiltins st) ibuiltin
, stHaskellImports = Set.union (stHaskellImports st) hsImports
, stPatternSynImports = Map.union (stPatternSynImports st) patsyns
, stInstanceDefs = (Map.unionWith List.union (fst (stInstanceDefs st)) instdefs, snd (stInstanceDefs st))
}

-- | Scope checks the given module. A proper version of the module
@@ -361,7 +363,8 @@ getInterface' x includeStateChanges =
-- things.
sig <- getSignature
patsyns <- getPatternSyns
addImportedThings sig Map.empty Set.empty patsyns
instdefs <- getInstanceDefs
addImportedThings sig Map.empty Set.empty patsyns instdefs
setSignature emptySignature
setPatternSyns Map.empty

@@ -376,6 +379,7 @@ getInterface' x includeStateChanges =
isig <- getImportedSignature
ibuiltin <- gets stImportedBuiltins
ipatsyns <- getPatternSynImports
instdefs <- getInstanceDefs
ho <- getInteractionOutputCallback
-- Every interface is treated in isolation. Note: Changes
-- to stDecodedModules are not preserved if an error is
@@ -393,7 +397,7 @@ getInterface' x includeStateChanges =
modify $ \s -> s { stModuleToSource = mf
}
setVisitedModules vs
addImportedThings isig ibuiltin Set.empty ipatsyns
addImportedThings isig ibuiltin Set.empty ipatsyns instdefs

r <- withMsgs $ createInterface file x
mf <- stModuleToSource <$> get
@@ -630,6 +634,7 @@ buildInterface file topLevel syntaxInfo previousHsImports pragmas = do
mhs <- mapM (\ m -> (m,) <$> moduleHash m) $ Set.toList ms
hsImps <- getHaskellImports
patsyns <- getPatternSyns
instdefs<- getInstanceDefs
h <- liftIO $ hashFile file
let builtin' = Map.mapWithKey (\ x b -> (x,) . primFunName <$> b) builtin
reportSLn "import.iface" 7 " instantiating all meta variables"
@@ -645,6 +650,7 @@ buildInterface file topLevel syntaxInfo previousHsImports pragmas = do
, iHighlighting = syntaxInfo
, iPragmaOptions = pragmas
, iPatternSyns = patsyns
, iInstanceDefs = instdefs
}
reportSLn "import.iface" 7 " interface complete"
return i
@@ -500,6 +500,10 @@ data IsAbstract = AbstractDef | ConcreteDef
instance KillRange IsAbstract where
killRange = id

-- | Is this definition eligible for instance search?
data IsInstance = InstanceDef | NotInstanceDef
deriving (Typeable, Show, Eq, Ord)

type Nat = Int
type Arity = Nat

@@ -31,6 +31,7 @@ module Agda.Syntax.Concrete
, Declaration(..)
, ModuleApplication(..)
, TypeSignature
, TypeSignatureOrInstanceBlock
, Constructor
, ImportDirective(..), UsingOrHiding(..), ImportedName(..)
, Renaming(..), AsName(..)
@@ -297,6 +298,9 @@ data AsName = AsName { asName :: Name
-- | Just type signatures.
type TypeSignature = Declaration

-- | Just type signatures or instance blocks.
type TypeSignatureOrInstanceBlock = Declaration

-- | A data constructor declaration is just a type signature.
type Constructor = TypeSignature

@@ -320,7 +324,8 @@ data Declaration
| Mutual !Range [Declaration]
| Abstract !Range [Declaration]
| Private !Range [Declaration]
| Postulate !Range [TypeSignature]
| InstanceB !Range [Declaration]
| Postulate !Range [TypeSignatureOrInstanceBlock]
| Primitive !Range [TypeSignature]
| Open !Range QName ImportDirective
| Import !Range QName (Maybe AsName) OpenShortHand ImportDirective
@@ -524,6 +529,7 @@ instance HasRange Declaration where
getRange (Open r _ _) = r
getRange (ModuleMacro r _ _ _ _) = r
getRange (Import r _ _ _ _) = r
getRange (InstanceB r _) = r
getRange (Private r _) = r
getRange (Postulate r _) = r
getRange (Primitive r _) = r
@@ -614,6 +620,7 @@ instance KillRange Declaration where
killRange (Mutual _ d) = killRange1 (Mutual noRange) d
killRange (Abstract _ d) = killRange1 (Abstract noRange) d
killRange (Private _ d) = killRange1 (Private noRange) d
killRange (InstanceB _ d) = killRange1 (InstanceB noRange) d
killRange (Postulate _ t) = killRange1 (Postulate noRange) t
killRange (Primitive _ t) = killRange1 (Primitive noRange) t
killRange (Open _ q i) = killRange2 (Open noRange) q i

0 comments on commit 7ca60fd

Please sign in to comment.
You can’t perform that action at this time.