"Committed_by_peb"

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" };
+
+
+}

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;
+
+}

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" };
+
+
+}

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;
+
+
+}