diff options
Diffstat (limited to 'doc/tutorial/gf-tutorial.t2t')
| -rw-r--r-- | doc/tutorial/gf-tutorial.t2t | 49 |
1 files changed, 10 insertions, 39 deletions
diff --git a/doc/tutorial/gf-tutorial.t2t b/doc/tutorial/gf-tutorial.t2t index 469166090..7467e107e 100644 --- a/doc/tutorial/gf-tutorial.t2t +++ b/doc/tutorial/gf-tutorial.t2t @@ -3718,49 +3718,25 @@ Concrete syntax does not know if a category is a dependent type. ``` Notice that the ``Kind`` argument is suppressed in linearization. -Parsing with dependent types is performed in two phases: +Parsing with dependent types consists of two phases: + context-free parsing + filtering through type checker +Parsing a type-correct command works as expected: -By just doing the first phase, the ``kind`` argument is not found: ``` > parse "dim the light" - CAction ? dim (DKindOne light) -``` -Moreover, type-incorrect commands are not rejected: -``` - > parse "dim the fan" - CAction ? dim (DKindOne fan) -``` -The term ``?`` is a **metavariable**, returned by the parser -for any subtree that is suppressed by a linearization rule. -These are the same kind of metavariables as were used #Rsecediting -to mark incomplete parts of trees in the syntax editor. - - - -#NEW - -===Solving metavariables=== - -Use the command ``put_tree = pt`` with the option ``-typecheck``: -``` - > parse "dim the light" | put_tree -typecheck CAction light dim (DKindOne light) ``` -The ``typecheck`` process may fail, in which case an error message -is shown and no tree is returned: +However, type-incorrect commands are rejected by the typecheck: ``` - > parse "dim the fan" | put_tree -typecheck - - Error in tree UCommand (CAction ? 0 dim (DKindOne fan)) : - (? 0 <> fan) (? 0 <> light) + > parse "dim the fan" + The parsing is successful but the type checking failed with error(s): + Couldn't match expected type Device light + against the interred type Device fan + In the expression: DKindOne fan ``` - - - #NEW ==Polymorphism== @@ -3786,23 +3762,19 @@ to express Haskell-type library functions: \_,_,_,f,x,y -> f y x ; ``` - #NEW ===Dependent types: exercises=== 1. Write an abstract syntax module with above contents and an appropriate English concrete syntax. Try to parse the commands -//dim the light// and //dim the fan//, with and without ``solve`` filtering. - +//dim the light// and //dim the fan//. -2. Perform random and exhaustive generation, with and without -``solve`` filtering. +2. Perform random and exhaustive generation. 3. Add some device kinds and actions to the grammar. - #NEW ==Proof objects== @@ -3912,7 +3884,6 @@ fun Classes for new actions can be added incrementally. - #NEW ==Variable bindings== |