Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Case study examples #12

Open
wants to merge 7 commits into
base: master
Choose a base branch
from
Open

Case study examples #12

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
6142a4f
Added step 1
Nov 11, 2019
f119db5
Fixed names in case-study-1.ub
Nov 11, 2019
c5ddcad
Added case-study-2.ub
Nov 11, 2019
a776de6
Added case-study-3.ub
Nov 11, 2019
afe2d07
Added case-study-4.ub
Nov 11, 2019
8be326b
Added case-study-5.ub
Nov 11, 2019
5881ef9
Deleted old examples
Nov 11, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
25 changes: 20 additions & 5 deletions Repl/examples/extended-example-1.ub → Repl/examples/case-study-1.ub
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
/* General: */

data Identifier where
Tik()
Tok(Identifier)
Expand All @@ -19,6 +21,19 @@ data Redex where
RedAnd(Expr, Expr)
RedOr(Expr, Expr)

cfun Value:asExpr() : Expr :=
case ValPosVar(id) => EVar(id)
case ValNegVar(id) => ENot(EVar(id))
case ValAnd(e1,e2) => EAnd(e1.asExpr(), e2.asExpr())
case ValOr(e1,e2) => EOr(e1.asExpr(), e2.asExpr())

cfun Redex:eval() : Expr :=
case RedNot(e) => e
case RedAnd(e1,e2) => EOr(ENot(e1), ENot(e2))
case RedOr(e1,e2) => EAnd(ENot(e1), ENot(e2))

/* Specific to this step: */

data Found where
FoundValue(Value)
FoundRedex(Redex)
Expand All @@ -35,19 +50,19 @@ cfun Expr:searchNeg(ctx : Value2Found) : Found :=
cfun Expr:searchPos(ctx : Value2Found) : Found :=
case EVar(n) => ctx.apply(ValPosVar(n))
case ENot(e) => e.searchNeg(ctx)
case EAnd(e1,e2) => e1.searchPos( comatch Value2Found:AndCtx1 using e2 := e2 : Expr, ctx := ctx : Value2Found with
cocase apply(val1) => e2.searchPos( comatch Value2Found:AndCtx2 using val1 := val1 : Value , ctx := ctx : Value2Found with
case EAnd(e1,e2) => e1.searchPos( comatch Value2Found:AndCnt1 using e2 := e2 : Expr, ctx := ctx : Value2Found with
cocase apply(val1) => e2.searchPos( comatch Value2Found:AndCnt2 using val1 := val1 : Value , ctx := ctx : Value2Found with
cocase apply(val2) => ctx.apply(ValAnd(val1, val2))
)
)
case EOr(e1,e2) => e1.searchPos( comatch Value2Found:OrCtx1 using e2 := e2 : Expr, ctx := ctx : Value2Found with
cocase apply(val1) => e2.searchPos( comatch Value2Found:OrCtx4 using val1 := val1 : Value , ctx := ctx : Value2Found with
case EOr(e1,e2) => e1.searchPos( comatch Value2Found:OrCnt1 using e2 := e2 : Expr, ctx := ctx : Value2Found with
cocase apply(val1) => e2.searchPos( comatch Value2Found:OrCnt2 using val1 := val1 : Value , ctx := ctx : Value2Found with
cocase apply(val2) => ctx.apply(ValOr(val1, val2))
)
)

fun search(e : Expr) : Found :=
e.searchPos(comatch Value2Found:EmptyCtx with
e.searchPos(comatch Value2Found:BaseCnt with
cocase apply(val) => FoundValue(val)
)

70 changes: 70 additions & 0 deletions Repl/examples/case-study-2.ub
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,70 @@
/* General: */

data Identifier where
Tik()
Tok(Identifier)

data Expr where
EVar(Identifier)
ENot(Expr)
EAnd(Expr, Expr)
EOr(Expr, Expr)

data Value where
ValPosVar(Identifier)
ValNegVar(Identifier)
ValAnd(Value, Value)
ValOr(Value, Value)

data Redex where
RedNot(Expr)
RedAnd(Expr, Expr)
RedOr(Expr, Expr)

cfun Value:asExpr() : Expr :=
case ValPosVar(id) => EVar(id)
case ValNegVar(id) => ENot(EVar(id))
case ValAnd(e1,e2) => EAnd(e1.asExpr(), e2.asExpr())
case ValOr(e1,e2) => EOr(e1.asExpr(), e2.asExpr())

cfun Redex:eval() : Expr :=
case RedNot(e) => e
case RedAnd(e1,e2) => EOr(ENot(e1), ENot(e2))
case RedOr(e1,e2) => EAnd(ENot(e1), ENot(e2))

/* Specific to this step: */
/* After constructorizing "Value2Found" from case-study-1.ub */

data Found where
FoundValue(Value)
FoundRedex(Redex)

data Value2Found where
_BaseCnt()
_AndCnt1(Expr , Value2Found)
_AndCnt2(Value , Value2Found)
_OrCnt1(Expr , Value2Found)
_OrCnt2(Value , Value2Found)

cfun Expr:searchNeg(ctx : Value2Found) : Found :=
case EVar(n) => ctx.apply(ValNegVar(n))
case ENot(e) => FoundRedex(RedNot(e))
case EAnd(e1,e2) => FoundRedex(RedAnd(e1,e2))
case EOr(e1,e2) => FoundRedex(RedOr(e1,e2))

cfun Expr:searchPos(ctx : Value2Found) : Found :=
case EVar(id) => ctx.apply(ValPosVar(id))
case ENot(e) => e.searchNeg(ctx)
case EAnd(e1, e2) => e1.searchPos(_AndCnt1(e2 , ctx))
case EOr(e1 , e2) => e1.searchPos(_OrCnt1(e2 , ctx))


fun search(e : Expr) : Found :=
e.searchPos(_BaseCnt())

cfun Value2Found:apply(v : Value) : Found :=
case _BaseCnt() => FoundValue(v)
case _AndCnt1(e, cnt) => e.searchPos(_AndCnt2(v, cnt))
case _AndCnt2(v2, cnt) => cnt.apply(ValAnd(v2, v))
case _OrCnt1(e, cnt) => e.searchPos(_OrCnt2(v, cnt))
case _OrCnt2(v2, cnt) => cnt.apply(ValOr(v2, v))
82 changes: 82 additions & 0 deletions Repl/examples/case-study-3.ub
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,82 @@
/* General: */

data Identifier where
Tik()
Tok(Identifier)

data Expr where
EVar(Identifier)
ENot(Expr)
EAnd(Expr, Expr)
EOr(Expr, Expr)

data Value where
ValPosVar(Identifier)
ValNegVar(Identifier)
ValAnd(Value, Value)
ValOr(Value, Value)

data Redex where
RedNot(Expr)
RedAnd(Expr, Expr)
RedOr(Expr, Expr)

cfun Value:asExpr() : Expr :=
case ValPosVar(id) => EVar(id)
case ValNegVar(id) => ENot(EVar(id))
case ValAnd(e1,e2) => EAnd(e1.asExpr(), e2.asExpr())
case ValOr(e1,e2) => EOr(e1.asExpr(), e2.asExpr())

cfun Redex:eval() : Expr :=
case RedNot(e) => e
case RedAnd(e1,e2) => EOr(ENot(e1), ENot(e2))
case RedOr(e1,e2) => EAnd(ENot(e1), ENot(e2))

/* Specific to this step: */
/* */
/* Renaming: */
/* apply --> findNext */
/* Value2Found --> Context */
/* _BaseCnt() --> EmptyCtx() */
/* _AndCnt1(...) --> _AndCtx1() */
/* _AndCnt2(...) --> _AndCtx2() */
/* _OrCnt1(...) --> _OrCtx1() */
/* _OrCnt1(...) --> _OrCtx1() */
/* */
/* Adding argument to FoundRedex */
/* */
/* Modifying searchNeg */

data Found where
FoundValue(Value)
FoundRedex(Redex, Context)

data Context where
_EmptyCtx()
_AndCtx1(Expr , Context)
_AndCtx2(Value , Context)
_OrCtx1(Expr , Context)
_OrCtx2(Value , Context)

cfun Expr:searchNeg(ctx : Context) : Found :=
case EVar(n) => ctx.findNext(ValNegVar(n))
case ENot(e) => FoundRedex(RedNot(e), ctx)
case EAnd(e1,e2) => FoundRedex(RedAnd(e1,e2), ctx)
case EOr(e1,e2) => FoundRedex(RedOr(e1,e2), ctx)

cfun Expr:searchPos(ctx : Context) : Found :=
case EVar(id) => ctx.findNext(ValPosVar(id))
case ENot(e) => e.searchNeg(ctx)
case EAnd(e1, e2) => e1.searchPos(_AndCtx1(e2 , ctx))
case EOr(e1 , e2) => e1.searchPos(_OrCtx1(e2 , ctx))


fun search(e : Expr) : Found :=
e.searchPos(EmptyCtx())

cfun Context:findNext(v : Value) : Found :=
case _EmptyCtx() => FoundValue(v)
case _AndCtx1(e, cnt) => e.searchPos(_AndCtx2(v, cnt))
case _AndCtx2(v2, cnt) => cnt.findNext(ValAnd(v2, v))
case _OrCtx1(e, cnt) => e.searchPos(_OrCtx2(v, cnt))
case _OrCtx2(v2, cnt) => cnt.findNext(ValOr(v2, v))
78 changes: 78 additions & 0 deletions Repl/examples/case-study-4.ub
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,78 @@
/* General: */

data Identifier where
Tik()
Tok(Identifier)

data Expr where
EVar(Identifier)
ENot(Expr)
EAnd(Expr, Expr)
EOr(Expr, Expr)

data Value where
ValPosVar(Identifier)
ValNegVar(Identifier)
ValAnd(Value, Value)
ValOr(Value, Value)

data Redex where
RedNot(Expr)
RedAnd(Expr, Expr)
RedOr(Expr, Expr)

cfun Value:asExpr() : Expr :=
case ValPosVar(id) => EVar(id)
case ValNegVar(id) => ENot(EVar(id))
case ValAnd(e1,e2) => EAnd(e1.asExpr(), e2.asExpr())
case ValOr(e1,e2) => EOr(e1.asExpr(), e2.asExpr())

cfun Redex:eval() : Expr :=
case RedNot(e) => e
case RedAnd(e1,e2) => EOr(ENot(e1), ENot(e2))
case RedOr(e1,e2) => EAnd(ENot(e1), ENot(e2))

/* Specific to this step: */
/* */
/* Adding the substitute function */

data Found where
FoundValue(Value)
FoundRedex(Redex, Context)

data Context where
_EmptyCtx()
_AndCtx1(Expr , Context)
_AndCtx2(Value , Context)
_OrCtx1(Expr , Context)
_OrCtx2(Value , Context)

cfun Expr:searchNeg(ctx : Context) : Found :=
case EVar(n) => ctx.findNext(ValNegVar(n))
case ENot(e) => FoundRedex(RedNot(e), ctx)
case EAnd(e1,e2) => FoundRedex(RedAnd(e1,e2), ctx)
case EOr(e1,e2) => FoundRedex(RedOr(e1,e2), ctx)

cfun Expr:searchPos(ctx : Context) : Found :=
case EVar(id) => ctx.findNext(ValPosVar(id))
case ENot(e) => e.searchNeg(ctx)
case EAnd(e1, e2) => e1.searchPos(_AndCtx1(e2 , ctx))
case EOr(e1 , e2) => e1.searchPos(_OrCtx1(e2 , ctx))


fun search(e : Expr) : Found :=
e.searchPos(EmptyCtx())

cfun Context:findNext(v : Value) : Found :=
case _EmptyCtx() => FoundValue(v)
case _AndCtx1(e, cnt) => e.searchPos(_AndCtx2(v, cnt))
case _AndCtx2(v2, cnt) => cnt.findNext(ValAnd(v2, v))
case _OrCtx1(e, cnt) => e.searchPos(_OrCtx2(v, cnt))
case _OrCtx2(v2, cnt) => cnt.findNext(ValOr(v2, v))

cfun Context:substitute(e : Expr) : Expr :=
case _EmptyCtx() => e
case _AndCtx1(e2, ctx) => ctx.substitute(EAnd(e,e2))
case _AndCtx2(v, ctx) => ctx.substitute(EAnd(v.asExpr(), e))
case _OrCtx1(e2, ctx) => ctx.substitute(EOr(e, e2))
case _OrCtx2(v, ctx) => ctx.substitute(EOr(v.asExpr(), e))
76 changes: 76 additions & 0 deletions Repl/examples/case-study-5.ub
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,76 @@
/* General: */

data Identifier where
Tik()
Tok(Identifier)

data Expr where
EVar(Identifier)
ENot(Expr)
EAnd(Expr, Expr)
EOr(Expr, Expr)

data Value where
ValPosVar(Identifier)
ValNegVar(Identifier)
ValAnd(Value, Value)
ValOr(Value, Value)

data Redex where
RedNot(Expr)
RedAnd(Expr, Expr)
RedOr(Expr, Expr)

cfun Value:asExpr() : Expr :=
case ValPosVar(id) => EVar(id)
case ValNegVar(id) => ENot(EVar(id))
case ValAnd(e1,e2) => EAnd(e1.asExpr(), e2.asExpr())
case ValOr(e1,e2) => EOr(e1.asExpr(), e2.asExpr())

cfun Redex:eval() : Expr :=
case RedNot(e) => e
case RedAnd(e1,e2) => EOr(ENot(e1), ENot(e2))
case RedOr(e1,e2) => EAnd(ENot(e1), ENot(e2))

/* Specific to this step: */
/* */
/* Destructorizing Context */

data Found where
FoundValue(Value)
FoundRedex(Redex, Context)

codata Context where
findNext(Value) : Found
substitute(Expr) : Expr

fun search(e : Expr) : Found :=
e.searchPos( comatch Context:EmptyCtx with
cocase findNext(z0) => FoundValue(z0)
cocase substitute(z0) => z0
)

cfun Expr:searchNeg(ctx : Context) : Found :=
case EVar(n) => ctx.findNext(ValNegVar(n))
case ENot(e) => FoundRedex(RedNot(e), ctx)
case EAnd(e1,e2) => FoundRedex(RedAnd(e1,e2), ctx)
case EOr(e1,e2) => FoundRedex(RedOr(e1,e2), ctx)


cfun Expr:searchPos(x0 : Context) : Found :=
case EVar(x1) => x0.findNext(ValPosVar(x1))
case ENot(x1) => x1.searchNeg(x0)
case EAnd(x1 , x2) => x1.searchPos( comatch Context:AndCtx1 using y0 := x2 : Expr , y1 := x0 : Context with
cocase findNext(z2) => y0.searchPos( comatch Context:AndCtx2 using z0 := z2 : Value , z1 := y1 : Context with
cocase findNext(a2) => z1.findNext(ValAnd(z0 , a2))
cocase substitute(a2) => z1.substitute(EAnd(z0.asExpr() , a2))
)
cocase substitute(z2) => y1.substitute(EAnd(z2 , y0))
)
case EOr(x1 , x2) => x1.searchPos( comatch Context:OrCtx1 using y0 := x2 : Expr , y1 := x0 : Context with
cocase findNext(z2) => y0.searchPos( comatch Context:OrCtx2 using z0 := z2 : Value , z1 := y1 : Context with
cocase findNext(a2) => z1.findNext(ValOr(z0 , a2))
cocase substitute(a2) => z1.substitute(EOr(z0.asExpr() , a2))
)
cocase substitute(z2) => y1.substitute(EOr(z2 , y0))
)
Loading