diff options
| author | peb <unknown> | 2005-08-08 08:01:10 +0000 |
|---|---|---|
| committer | peb <unknown> | 2005-08-08 08:01:10 +0000 |
| commit | 1351c101337e46a89c066f0830ed6f06fc96cf7a (patch) | |
| tree | c2a07b6182345a72cf8cea2125972630044fdf46 /grammars | |
| parent | b03a738c4433f40c1eca2691fe09ea31d71475fe (diff) | |
"Committed_by_peb"
Diffstat (limited to 'grammars')
| -rw-r--r-- | grammars/ljung/thesis/CopyMorphism.gf | 22 | ||||
| -rw-r--r-- | grammars/ljung/thesis/CopyMorphismAbs.gf | 15 | ||||
| -rw-r--r-- | grammars/ljung/thesis/Erasing.gf | 26 | ||||
| -rw-r--r-- | grammars/ljung/thesis/ErasingAbs.gf | 21 |
4 files changed, 84 insertions, 0 deletions
diff --git a/grammars/ljung/thesis/CopyMorphism.gf b/grammars/ljung/thesis/CopyMorphism.gf new file mode 100644 index 000000000..71faf1d99 --- /dev/null +++ b/grammars/ljung/thesis/CopyMorphism.gf @@ -0,0 +1,22 @@ + +-- the example 4.1 from Ljunglöf (2004, page 82) + +concrete CopyMorphism of CopyMorphismAbs = { + +lincat +S = { s : Str }; +A = { s1 : Str; s2 : Str }; + +lin + +f x = { s = x.s1 ++ x.s2 }; + +g x y = { s1 = x.s1 ++ y.s1; + s2 = x.s2 ++ y.s2 }; + +ac = { s1 = "a"; s2 = "c" }; + +bd = { s1 = "b"; s2 = "d" }; + + +} diff --git a/grammars/ljung/thesis/CopyMorphismAbs.gf b/grammars/ljung/thesis/CopyMorphismAbs.gf new file mode 100644 index 000000000..02929f699 --- /dev/null +++ b/grammars/ljung/thesis/CopyMorphismAbs.gf @@ -0,0 +1,15 @@ + +-- the example 4.1 from Ljunglöf (2004, page 82) + +abstract CopyMorphismAbs = { + +cat S; A; + +fun + +f : A -> S; +g : A -> A -> A; +ac : A; +bd : A; + +} diff --git a/grammars/ljung/thesis/Erasing.gf b/grammars/ljung/thesis/Erasing.gf new file mode 100644 index 000000000..8b393eec8 --- /dev/null +++ b/grammars/ljung/thesis/Erasing.gf @@ -0,0 +1,26 @@ + +-- the example 4.1 from Ljunglöf (2004, page 82) + +concrete Erasing of ErasingAbs = { + +lincat +S = { s : Str }; +A = { s1 : Str; s2 : Str }; +B = { s : Str }; +C = { s : Str }; + +lin + +f x = { s = x.s1 }; + +g x y z = { s1 = x.s2 ++ y.s; + s2 = x.s1 ++ z.s }; + +a = { s1 = "a1"; s2 = "a2" }; + +b = { s = "b" }; + +c = { s = "c" }; + + +} diff --git a/grammars/ljung/thesis/ErasingAbs.gf b/grammars/ljung/thesis/ErasingAbs.gf new file mode 100644 index 000000000..7b42b8863 --- /dev/null +++ b/grammars/ljung/thesis/ErasingAbs.gf @@ -0,0 +1,21 @@ + +-- the example 4.1 from Ljunglöf (2004, page 82) + +abstract ErasingAbs = { + +cat S; A; B; C; + +fun + +f : A -> S; + +g : A -> B -> C -> A; + +a : A; + +b : B; + +c : C; + + +} |
