From 89aa60da21e471a0c0c9d836f88aa260679b3ae6 Mon Sep 17 00:00:00 2001 From: MarcoTz Date: Thu, 11 Apr 2024 16:27:10 +0200 Subject: [PATCH] fixed web app --- web-app/StringFormat.hs | 4 +-- web-app/index.html | 68 ++++++++++++++++++++--------------------- 2 files changed, 36 insertions(+), 36 deletions(-) diff --git a/web-app/StringFormat.hs b/web-app/StringFormat.hs index 76da0f8..8d2b8a0 100644 --- a/web-app/StringFormat.hs +++ b/web-app/StringFormat.hs @@ -2,8 +2,8 @@ module StringFormat where import Environment import Common -import Syntax.Typed.Terms -import Pretty.Typed () +import Syntax.Kinded.Terms +import Pretty.Kinded () import Data.List (intercalate) diff --git a/web-app/index.html b/web-app/index.html index 650f748..be9551f 100644 --- a/web-app/index.html +++ b/web-app/index.html @@ -49,101 +49,101 @@

Results

- data Pair(a:+,b:+):+{ + data Pair(a:+,b:+){ Tup(a,b) } - data Nat :+ { + data Nat { Z, S(Nat) } - data Fun(a:+,b:-):- { + data Fun(a:+,b:-) { Ap(a,b) } - printCons :: forall X.X:-; + printCons :: forall X.X; printCons := mu x.Print x; - swap :: forall X Y. Fun(Pair(X,Y),Pair(Y,X)):+; + swap :: forall X Y. Fun(Pair(X,Y),Pair(Y,X)); swap := case { Ap(p,a) => < case { - Tup(b,c) => < Tup(c,b) | Pair(Y,X):+ | + | a> - } | + | p> + Tup(b,c) => < Tup(c,b) | Pair(Y,X): CBV | a> + } | CBV | p> }; - pair1 :: Pair(Nat,Nat):+; + pair1 :: Pair(Nat,Nat); pair1 := Tup(Z,S(Z)); - main := < swap | + | Ap(pair1,printCons)>; + main := < swap | CBV | Ap(pair1,printCons)>;
- data List(a:+):+{ + data List(a:+){ Nil, Cons(a,List(a)) } - data Fun(a:+,b:-):- { + data Fun(a:+,b:-) { Ap(a,b) } - data Unit : + { MkUnit } + data Unit { MkUnit } - printCons :: forall X. X:-; + printCons :: forall X. X; printCons := mu x.Print x; - tail :: forall X. Fun(List(X),List(X)) : +; + tail :: forall X. Fun(List(X),List(X)); tail := case { Ap(ls,a) => < case { - Nil => <Nil | + | a>, - Cons(hd,rs) => <rs | + | a> - } | + | ls> + Nil => <Nil | CBV | a>, + Cons(hd,rs) => <rs | CBV | a> + } | CBV | ls> }; - list1 :: List(Unit):+; + list1 :: List(Unit); list1 := Cons(MkUnit,Cons(MkUnit,Nil)); - main := < tail | + | Ap(list1,printCons)>; + main := < tail | CBV | Ap(list1,printCons)>;
- data Nat : + { + data Nat { Z, S(Nat) } - data Fun(a:+,b:-):- { + data Fun(a:+,b:-) { Ap(a,b) } - printCons :: Forall X.X:-; + printCons :: Forall X.X; printCons := mu x. Print x; - pred :: Fun(Nat,Nat):+; + pred :: Fun(Nat,Nat); pred := case { Ap(n,a) => < case { - Z => < Z | + | a>, - S(m) => < m | + | a > - } | + | n> + Z => < Z | CBV | a>, + S(m) => < m | CBV | a > + } | CBV | n> }; - nat1 :: Nat:+; + nat1 :: Nat; nat1 := S(S(Z)); - main := < pred | + | Ap(nat1,printCons)>; + main := < pred | CBV | Ap(nat1,printCons)>;
- data Fun(a:+,b:-):- { + data Fun(a:+,b:-){ Ap(a,b) } - data Unit:+ {MkUnit} + data Unit {MkUnit} - printCons :: Forall X.X:-; + printCons :: Forall X.X; printCons := mu x. Print x; - id :: forall X. Fun(X,X) : +; - id := case { Ap(x,a) => <x | + | a> }; + id :: forall X. Fun(X,X); + id := case { Ap(x,a) => <x | CBV | a> }; - main := < id | + | Ap(MkUnit,printCons)>; + main := < id | CBV | Ap(MkUnit,printCons)>;