msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

(Tutorial) Remove mentions to pt -typecheck

Browse Source 
The GF shell no longer has `put_tree -typecheck` option, and typechecking is done automatically when parsing.

The metavariable thing is a bit unclear: you don't get it when parsing "dim the light", or "switch on the fan, but you do get it when you `gt` after adding `switchOn` and `switchOff`.

```
> p "switch on the fan"
CAction fan (switchOff fan) (DKindOne fan)
> gt
CAction light dim (DKindOne light)
CAction ?3 (switchOff ?3) (DKindOne ?3)
CAction ?3 (switchOn ?3) (DKindOne ?3)
```

My hypothesis is that you don't get metavariable when parsing e.g. "dim the light", because even though `light` is suppressed in `CAction`, it still appears in `DKindOne`, so it gets to contribute to the whole tree with its string.
This commit is contained in:
Inari Listenmaa
2020-09-29 09:23:36 +02:00
committed by GitHub
parent 2c2bd158a6
commit f56fbcf86e
1 changed files with 10 additions and 39 deletions
Download Patch File Download Diff File Expand all files Collapse all files

49
doc/tutorial/gf-tutorial.t2t
View File

@@ -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==