Implicit arguments in GF. Works only in PGF for now.

This commit is contained in:
krasimir
2009-10-02 13:25:12 +00:00
parent 40373704ff
commit 2732a7a22e
9 changed files with 168 additions and 44 deletions

View File

@@ -122,6 +122,7 @@ data Term =
| App Term Term -- ^ application: @f a@
| Abs BindType Ident Term -- ^ abstraction: @\x -> b@
| Meta {-# UNPACK #-} !MetaId -- ^ metavariable: @?i@ (only parsable: ? = ?0)
| ImplArg Term -- ^ placeholder for implicit argument @{t}@
| Prod BindType Ident Term Term -- ^ function type: @(x : A) -> B@, @A -> B@, @({x} : A) -> B@
| Typed Term Term -- ^ type-annotated term
--
@@ -177,6 +178,8 @@ data Patt =
| PVal Patt Type Int -- ^ parameter value number: @T # i#
| PAs Ident Patt -- ^ as-pattern: x@p
| PImplArg Patt -- ^ placeholder for pattern for implicit argument @{p}@
-- regular expression patterns
| PNeg Patt -- ^ negated pattern: -p