Skip to content
GitLab
Explore
Sign in
Register
Primary navigation
Search or go to…
Project
H
haskell challenges
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Deploy
Releases
Package registry
Model registry
Operate
Terraform modules
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
kwsa1g20
haskell challenges
Commits
2360d703
Commit
2360d703
authored
1 year ago
by
kwsa1g20
Browse files
Options
Downloads
Patches
Plain Diff
Upload New File
parent
adfec137
No related branches found
No related tags found
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
Challenges.hs
+404
-0
404 additions, 0 deletions
Challenges.hs
with
404 additions
and
0 deletions
Challenges.hs
0 → 100644
+
404
−
0
View file @
2360d703
{-# LANGUAGE DeriveGeneric #-}
-- comp2209 Functional Programming Challenges
-- (c) University of Southampton 2022
-- Skeleton code to be updated with your solutions
-- The dummy functions here simply return an arbitrary value that is usually wrong
-- DO NOT MODIFY THE FOLLOWING LINES OF CODE
module
Challenges
(
Atoms
,
Interactions
,
Pos
,
EdgePos
,
Side
(
..
),
Marking
(
..
),
LamExpr
(
..
),
ArithExpr
(
..
),
calcBBInteractions
,
solveBB
,
prettyPrint
,
parseArith
,
churchEnc
,
innerRedn1
,
innerArithRedn1
,
compareArithLam
)
where
-- Import standard library and parsing definitions from Hutton 2016, Chapter 13
import
Data.Char
import
Parsing
import
Control.Monad
import
Data.List
import
GHC.Generics
(
Generic
,
Generic1
)
import
Control.DeepSeq
import
Data.Maybe
import
Data.Ord
import
Data.Function
-- Challenge 1
-- Calculate Interactions in the Black Box
type
Atoms
=
[
Pos
]
type
Interactions
=
[
(
EdgePos
,
Marking
)
]
type
Pos
=
(
Int
,
Int
)
-- top left is (1,1) , bottom right is (N,N) where N is size of grid
type
EdgePos
=
(
Side
,
Int
)
-- int range is 1 to N where N is size of grid
type
Corners
=
[(
Angel
,
Pos
)]
type
RayPath
=
(
Side
,
Atoms
)
data
Side
=
North
|
East
|
South
|
West
deriving
(
Show
,
Eq
,
Ord
,
Generic
)
data
Marking
=
Absorb
|
Reflect
|
Path
EdgePos
deriving
(
Show
,
Eq
)
data
Angel
=
Lt
|
Rt
|
Lb
|
Rb
deriving
(
Show
,
Eq
)
calcBBInteractions
::
Int
->
Atoms
->
[
EdgePos
]
->
Interactions
calcBBInteractions
limit
atoms
positions
|
limit
<
1
=
error
"grid must be larger than 0*0"
calcBBInteractions
limit
atoms
[]
=
[]
calcBBInteractions
limit
atoms
(
x
:
xs
)
|
checkEdgeReflection
(
head
(
snd
coordinates
))
atoms
(
fst
x
)
=
(
x
,
Reflect
)
:
calcBBInteractions
limit
atoms
xs
|
otherwise
=
traverseGraph
coordinates
atoms
corners
(
x
,
limit
)
:
calcBBInteractions
limit
atoms
xs
where
coordinates
=
pathCreator
x
limit
corners
=
cornerCreator
atoms
createGrid
n
=
[(
y
,
x
)
|
x
<-
[
1
..
n
],
y
<-
[
1
..
n
]]
cornerCreator
::
Atoms
->
Corners
cornerCreator
[]
=
[]
cornerCreator
((
y
,
z
)
:
xs
)
=
(
Rb
,(
y
+
1
,
z
+
1
))
:
(
Rt
,(
y
+
1
,
z
-
1
))
:
(
Lb
,(
y
-
1
,
z
+
1
))
:
(
Lt
,(
y
-
1
,
z
-
1
))
:
cornerCreator
xs
pathCreator
::
EdgePos
->
Int
->
RayPath
pathCreator
(
North
,
n
)
t
=
(
South
,[(
n
,
x
)
|
x
<-
[
1
..
t
+
1
]])
pathCreator
(
East
,
n
)
t
=
(
West
,[(
x
,
n
)
|
x
<-
[
t
,
t
-
1
..
0
]])
pathCreator
(
South
,
n
)
t
=
(
North
,[(
n
,
x
)
|
x
<-
[
t
,
t
-
1
..
0
]])
pathCreator
(
West
,
n
)
t
=
(
East
,[(
x
,
n
)
|
x
<-
[
1
..
t
+
1
]])
checkEdgeReflection
::
(
Int
,
Int
)
->
Atoms
->
Side
->
Bool
checkEdgeReflection
x
[]
side
=
False
checkEdgeReflection
x
((
z
,
w
)
:
ys
)
side
|
x
`
elem
`
((
z
,
w
)
:
ys
)
=
False
|
(
side
==
North
||
side
==
South
)
&&
(
x
==
(
z
+
1
,
w
))
=
True
|
(
side
==
North
||
side
==
South
)
&&
(
x
==
(
z
-
1
,
w
))
=
True
|
(
side
==
West
||
side
==
East
)
&&
(
x
==
(
z
,
w
+
1
))
=
True
|
(
side
==
West
||
side
==
East
)
&&
x
==
((
z
,
w
-
1
))
=
True
|
otherwise
=
checkEdgeReflection
x
ys
side
traverseGraph
::
RayPath
->
Atoms
->
Corners
->
(
EdgePos
,
Int
)
->
(
EdgePos
,
Marking
)
traverseGraph
(
North
,(
x
:
xs
))
atoms
corners
start
|
(
snd
x
)
==
0
=
((
fst
start
),
Path
(
North
,(
fst
x
)))
|
x
`
elem
`
atoms
=
((
fst
start
),
Absorb
)
|
length
(
y
)
==
2
&&
((
fst
x
),(
snd
x
)
-
1
)
`
notElem
`
atoms
=
((
fst
start
),
Reflect
)
|
length
(
y
)
>
0
&&
((
fst
x
),(
snd
x
)
-
1
)
`
notElem
`
atoms
=
traverseGraph
(
deflect
North
y
(
snd
start
))
atoms
corners
start
|
otherwise
=
traverseGraph
(
North
,(
xs
))
atoms
corners
start
where
y
=
find'
x
corners
traverseGraph
(
East
,(
x
:
xs
))
atoms
corners
start
|
(
fst
x
)
>
(
snd
start
)
=
((
fst
start
),
Path
(
East
,(
snd
x
)))
|
x
`
elem
`
atoms
=
((
fst
start
),
Absorb
)
|
length
(
y
)
==
2
&&
((
fst
x
)
+
1
,(
snd
x
))
`
notElem
`
atoms
=
((
fst
start
),
Reflect
)
|
length
(
y
)
>
0
&&
((
fst
x
)
+
1
,(
snd
x
))
`
notElem
`
atoms
=
traverseGraph
(
deflect
East
y
(
snd
start
))
atoms
corners
start
|
otherwise
=
traverseGraph
(
East
,(
xs
))
atoms
corners
start
where
y
=
find'
x
corners
traverseGraph
(
South
,(
x
:
xs
))
atoms
corners
start
|
(
snd
x
)
>
(
snd
start
)
=
((
fst
start
),
Path
(
South
,(
fst
x
)))
|
x
`
elem
`
atoms
=
((
fst
start
),
Absorb
)
|
length
(
y
)
==
2
&&
((
fst
x
),(
snd
x
)
+
1
)
`
notElem
`
atoms
=
((
fst
start
),
Reflect
)
|
length
(
y
)
>
0
&&
((
fst
x
),(
snd
x
)
+
1
)
`
notElem
`
atoms
=
traverseGraph
(
deflect
South
y
(
snd
start
))
atoms
corners
start
|
otherwise
=
traverseGraph
(
South
,(
xs
))
atoms
corners
start
where
y
=
find'
x
corners
traverseGraph
(
West
,(
x
:
xs
))
atoms
corners
start
|
(
fst
x
)
==
0
=
((
fst
start
),
Path
(
West
,(
snd
x
)))
|
x
`
elem
`
atoms
=
((
fst
start
),
Absorb
)
|
length
(
y
)
==
2
&&
((
fst
x
)
-
1
,(
snd
x
))
`
notElem
`
atoms
=
((
fst
start
),
Reflect
)
|
length
(
y
)
==
1
&&
((
fst
x
)
-
1
,(
snd
x
))
`
notElem
`
atoms
=
traverseGraph
(
deflect
West
y
(
snd
start
))
atoms
corners
start
|
otherwise
=
traverseGraph
(
West
,(
xs
))
atoms
corners
start
where
y
=
find'
x
corners
deflect
::
Side
->
Corners
->
Int
->
RayPath
deflect
North
corners
limit
|
(
fst
(
head
corners
))
==
Rb
=
(
East
,[(
z
,
y
)
|
z
<-
[
x
+
1
..
limit
+
1
]
])
|
(
fst
(
head
corners
))
==
Lb
=
(
West
,[(
z
,
y
)
|
z
<-
[
x
-
1
,
x
-
2
..
0
]])
|
(
fst
(
head
corners
))
==
Lt
=
(
West
,[(
z
,
y
)
|
z
<-
[
x
-
1
,
x
-
2
..
0
]])
|
(
fst
(
head
corners
))
==
Rt
=
(
East
,[(
z
,
y
)
|
z
<-
[
x
+
1
..
limit
+
1
]
])
|
otherwise
=
(
North
,
[]
)
where
x
=
fst
.
snd
.
head
$
corners
y
=
snd
.
snd
.
head
$
corners
deflect
East
corners
limit
|
(
fst
(
head
corners
))
==
Lb
=
(
South
,[(
x
,
z
)
|
z
<-
[
y
+
1
..
limit
+
1
]
])
|
(
fst
(
head
corners
))
==
Lt
=
(
North
,[(
x
,
z
)
|
z
<-
[
y
-
1
,
y
-
2
..
0
]])
|
(
fst
(
head
corners
))
==
Rt
=
(
North
,[(
x
,
z
)
|
z
<-
[
y
-
1
,
y
-
2
..
0
]])
|
(
fst
(
head
corners
))
==
Lb
=
(
South
,[(
x
,
z
)
|
z
<-
[
y
+
1
..
limit
+
1
]
])
|
otherwise
=
(
East
,
[]
)
where
x
=
fst
.
snd
.
head
$
corners
y
=
snd
.
snd
.
head
$
corners
deflect
South
corners
limit
|
(
fst
(
head
corners
))
==
Rt
||
(
fst
(
head
corners
))
==
Rb
=
(
East
,[(
z
,
y
)
|
z
<-
[
x
+
1
..
limit
+
1
]
])
|
(
fst
(
head
corners
))
==
Lt
||
(
fst
(
head
corners
))
==
Lb
=
(
West
,[(
z
,
y
)
|
z
<-
[
x
-
1
,
x
-
2
..
0
]])
|
otherwise
=
(
South
,
[]
)
where
x
=
fst
.
snd
.
head
$
corners
y
=
snd
.
snd
.
head
$
corners
deflect
West
corners
limit
|
(
fst
(
head
corners
))
==
Rb
||
(
fst
(
head
corners
))
==
Lb
=
(
South
,[(
x
,
z
)
|
z
<-
[
y
+
1
..
limit
+
1
]])
|
(
fst
(
head
corners
))
==
Rt
||
(
fst
(
head
corners
))
==
Lt
=
(
North
,[(
x
,
z
)
|
z
<-
[
y
-
1
,
y
-
2
..
0
]])
|
otherwise
=
(
West
,
[]
)
where
x
=
fst
.
snd
.
head
$
corners
y
=
snd
.
snd
.
head
$
corners
find'
k
t
=
[(
z
,
v
)
|
(
z
,
v
)
<-
t
,
k
==
v
]
-- Challenge 2
-- Find atoms in a Black Box
data
Deflections
=
Up
|
Down
|
DRight
|
DLeft
solveBB
::
Int
->
Interactions
->
Atoms
solveBB
limit
xs
=
smallestList
(
filter
(
not
.
null
)(
filterAtums
limit
xs
(
powerset
(
possibleAtoms
limit
xs
[]
))))
-- this give a possible set of atoms
possibleAtoms
limit
[]
ys
=
ys
possibleAtoms
limit
(
x
:
xs
)
ys
|
calcBBInteractions
limit
ys
[
fst
x
]
==
[
x
]
=
possibleAtoms
limit
xs
ys
|
checkNormal
x
=
possibleAtoms
limit
xs
(
subsetNormal
ys
x
limit
(
automSetNormal
limit
x
))
|
otherwise
=
possibleAtoms
limit
xs
(
subsetAbnormal
ys
x
limit
(
automSetAbnormal
limit
x
))
subsetNormal
ys
interaction
limit
[]
=
ys
subsetNormal
ys
interaction
limit
(
x
:
xs
)
|
calcBBInteractions
limit
(
ys
++
[
x
])
[(
fst
interaction
)]
==
[
interaction
]
=
subsetNormal
(
ys
++
[
x
])
interaction
limit
xs
|
otherwise
=
subsetNormal
ys
interaction
limit
xs
subsetAbnormal
ys
interaction
limit
[]
=
ys
subsetAbnormal
ys
interaction
limit
(
x
:
xs
)
|
calcBBInteractions
limit
(
ys
++
x
)
[(
fst
interaction
)]
==
[
interaction
]
=
subsetAbnormal
(
ys
++
x
)
interaction
limit
xs
|
otherwise
=
subsetAbnormal
ys
interaction
limit
xs
checkNormal
((
North
,
n
),
Path
(
z
,
x
))
|
(
z
==
South
||
z
==
North
)
&&
n
/=
x
=
False
|
otherwise
=
True
checkNormal
((
South
,
n
),
Path
(
z
,
x
))
|
(
z
==
South
||
z
==
North
)
&&
n
/=
x
=
False
|
otherwise
=
True
checkNormal
((
West
,
n
),
Path
(
z
,
x
))
|
(
z
==
West
||
z
==
East
)
&&
n
/=
x
=
False
|
otherwise
=
True
checkNormal
((
East
,
n
),
Path
(
z
,
x
))
|
(
z
==
East
||
z
==
West
)
&&
n
/=
x
=
False
|
otherwise
=
True
checkNormal
(
x
,
Reflect
)
=
True
checkNormal
(
x
,
Absorb
)
=
True
automSetNormal
limit
(
z
,
y
)
=
filter
(
\
x
->
helper1
limit
[
x
]
z
(
z
,
y
))
(
coordinates
limit
)
automSetAbnormal
limit
(
z
,
y
)
=
concat
(
filter
(
not
.
null
)(
map
(
filter
(
\
x
->
helper1
limit
x
z
(
z
,
y
)))(
atomsSubs
(
coordinates
limit
))))
coordinates
limit
=
[(
x
,
y
)
|
x
<-
[
1
..
limit
],
y
<-
[
1
..
limit
]]
helper1
limit
xs
y
interaction
|
calcBBInteractions
limit
xs
[
y
]
==
[
interaction
]
=
True
|
otherwise
=
False
atomsSubs
[]
=
[]
atomsSubs
(
x
:
xs
)
=
helpme
x
xs
:
atomsSubs
xs
helpme
z
xs
=
map
(
\
x
->
[
z
,
x
])
xs
filterAtums
::
Int
->
Interactions
->
[
Atoms
]
->
[
Atoms
]
filterAtums
limit
zs
(
ys
)
=
filter
(
\
x
->
(
calcBBInteractions
limit
x
(
map
fst
zs
)
==
zs
))
ys
smallestList
::
[[
a
]]
->
[
a
]
smallestList
=
minimumBy
(
compare
`
on
`
length
)
powerset
::
[
a
]
->
[[
a
]]
powerset
[]
=
[
[]
]
powerset
(
x
:
xs
)
=
let
ps
=
powerset
xs
in
ps
++
[
x
:
s
|
s
<-
ps
]
-- Challenge 3
-- Pretty Printing Lambda with Alpha-Normalisation
data
LamExpr
=
LamApp
LamExpr
LamExpr
|
LamAbs
Int
LamExpr
|
LamVar
Int
deriving
(
Eq
,
Show
,
Read
)
prettyPrint
::
LamExpr
->
String
prettyPrint
x
=
printExp
(
fixingLambdas
x
0
)
{- turning the lambda expressions into alpha normal form-}
fixingLambdas
::
LamExpr
->
Int
->
LamExpr
fixingLambdas
(
LamVar
x
)
y
|
x
<
0
=
error
" no negative variables"
|
otherwise
=
LamVar
x
fixingLambdas
(
LamAbs
x
e1
)
y
|
y
==
x
=
LamAbs
x
(
fixingLambdas
e1
0
)
|
free
y
e1
=
fixingLambdas
(
LamAbs
x
e1
)
(
y
+
1
)
|
not
(
free
x
e1
)
=
LamAbs
y
(
fixingLambdas
e1
0
)
|
otherwise
=
LamAbs
y
(
fixingLambdas
(
renameFree
x
e1
y
)
0
)
fixingLambdas
(
LamApp
e1
e2
)
y
=
LamApp
(
fixingLambdas
e1
y
)
(
fixingLambdas
e2
y
)
{- renames free variables of x in e1 to y -}
renameFree
::
Int
->
LamExpr
->
Int
->
LamExpr
renameFree
old
(
LamVar
x
)
new
|
x
==
old
=
LamVar
new
|
otherwise
=
LamVar
x
renameFree
old
(
LamAbs
x
e1
)
new
=
LamAbs
x
(
renameFree
old
e1
new
)
renameFree
old
(
LamApp
e1
e2
)
new
|
(
free
old
e1
)
&&
(
free
old
e2
)
=
LamApp
(
renameFree
old
e1
new
)
(
renameFree
old
e2
new
)
|
(
free
old
e1
)
=
LamApp
(
renameFree
old
e1
new
)
e2
|
otherwise
=
LamApp
e1
(
renameFree
old
e2
new
)
{- used it from lecture notes with a little bit adjustment -}
free
::
Int
->
LamExpr
->
Bool
free
x
(
LamVar
y
)
=
x
==
y
free
x
(
LamAbs
y
e
)
|
x
==
y
=
False
free
x
(
LamAbs
y
e
)
|
x
/=
y
=
free
x
e
free
x
(
LamApp
e1
e2
)
=
(
free
x
e1
)
||
(
free
x
e2
)
{- printing the expression -}
printExp
::
LamExpr
->
String
printExp
(
LamVar
n
)
=
"x"
++
show
n
printExp
(
LamApp
(
LamAbs
x
y
)
z
)
=
"("
++
printExp
(
LamAbs
x
y
)
++
")"
++
printExp
z
printExp
(
LamApp
x
(
LamApp
e1
e2
))
=
printExp
x
++
"("
++
printExp
e1
++
printExp
e2
++
")"
printExp
(
LamApp
(
LamVar
n
)
x
)
=
"x"
++
show
n
++
printExp
x
printExp
(
LamApp
x
(
LamVar
n
)
)
=
printExp
x
++
"x"
++
show
n
printExp
(
LamAbs
n
x
)
=
"
\\
x"
++
show
n
++
"->"
++
printExp
x
-- Challenge 4
-- Parsing Arithmetic Expressions
data
ArithExpr
=
Add
ArithExpr
ArithExpr
|
Mul
ArithExpr
ArithExpr
|
Section
ArithExpr
|
SecApp
ArithExpr
ArithExpr
|
ArithNum
Int
deriving
(
Show
,
Eq
,
Read
)
parseArith
::
String
->
Maybe
ArithExpr
parseArith
x
=
maybeArith
(
parse
expr
x
)
maybeArith
[(
x
,
[]
)]
=
Just
x
maybeArith
[]
=
Nothing
maybeArith
[(
x
,
xs
)]
=
Nothing
--code taken from lectures and changed a little
expr
::
Parser
ArithExpr
expr
=
do
space
t
<-
term
space
char
'*'
space
e
<-
expr
space
return
(
Mul
t
e
)
<|>
term
term
::
Parser
ArithExpr
term
=
do
space
f
<-
factor
space
char
'+'
space
t
<-
term
space
return
(
Add
f
t
)
<|>
factor
factor
::
Parser
ArithExpr
factor
=
nat'
<|>
do
space
char
'('
space
char
'+'
space
x
<-
expr
space
char
')'
space
e
<-
factor
space
return
(
SecApp
(
Section
x
)
e
)
<|>
do
space
char
'('
space
e
<-
expr
space
char
')'
space
return
(
e
)
nat'
::
Parser
ArithExpr
nat'
=
do
ds
<-
some
digit
return
(
ArithNum
(
read
ds
))
-- Challenge 5
-- Church Encoding of arithmetic
churchEnc
::
ArithExpr
->
LamExpr
churchEnc
(
ArithNum
n
)
|
n
<
0
=
error
" no negative numbers "
|
otherwise
=
LamAbs
0
(
LamAbs
1
(
createNum
n
))
churchEnc
(
Add
x
y
)
=
LamApp
(
LamApp
plus
(
churchEnc
x
))
(
churchEnc
y
)
churchEnc
(
Mul
x
y
)
=
LamApp
(
LamApp
mult
(
churchEnc
x
))
(
churchEnc
y
)
churchEnc
(
SecApp
(
Section
x
)
y
)
=
LamApp
(
LamApp
plus
(
churchEnc
x
))
(
churchEnc
y
)
createNum
::
Int
->
LamExpr
createNum
0
=
LamVar
1
createNum
n
=
LamApp
(
LamVar
0
)
(
createNum
(
n
-
1
))
mult
=
LamAbs
0
(
LamAbs
1
(
LamAbs
2
(
LamAbs
3
(
LamApp
(
LamApp
(
LamVar
0
)
(
LamApp
(
LamVar
1
)
(
LamVar
2
)))
(
LamVar
3
)))))
plus
=
LamAbs
0
(
LamAbs
1
(
LamAbs
2
(
LamAbs
3
(
LamApp
(
LamApp
(
LamVar
0
)
(
LamVar
2
)
)
(
LamApp
(
LamApp
(
LamVar
1
)
(
LamVar
2
))
(
LamVar
3
))))))
-- Challenge 6
-- Compare Innermost Reduction for Arithmetic and its Church Encoding
innerRedn1
::
LamExpr
->
Maybe
LamExpr
innerRedn1
(
LamVar
n
)
=
Nothing
innerRedn1
e1
|
e1
==
(
eval1cbv
e1
)
=
Nothing
|
otherwise
=
Just
(
eval1cbv
e1
)
-- code taken from lectures 38 and 39 adn changed a bit
eval1cbv
(
LamVar
x
)
=
(
LamVar
x
)
eval1cbv
(
LamAbs
x
e
)
|
(
checkinnerReduction
e
)
==
True
=
LamAbs
x
(
eval1cbv
e
)
|
otherwise
=
(
LamAbs
x
e
)
eval1cbv
(
LamApp
(
LamAbs
x
e1
)
e
)
|
(
checkinnerReduction
e1
)
==
False
=
subst
e1
x
e
|
otherwise
=
LamApp
(
LamAbs
x
(
eval1cbv
e1
))
e
eval1cbv
(
LamApp
e1
@
(
LamVar
x
)
e2
)
=
LamApp
e1
(
eval1cbv
e2
)
eval1cbv
(
LamApp
e1
e2
)
=
LamApp
(
eval1cbv
e1
)
e2
checkinnerReduction
::
LamExpr
->
Bool
checkinnerReduction
(
LamVar
x
)
=
False
checkinnerReduction
(
LamAbs
x
e1
)
=
checkinnerReduction
e1
checkinnerReduction
(
LamApp
(
LamAbs
x
e
)
e1
)
=
True
checkinnerReduction
(
LamApp
e1
e2
)
=
checkinnerReduction
e1
||
checkinnerReduction
e2
subst
::
LamExpr
->
Int
->
LamExpr
->
LamExpr
subst
(
LamVar
x
)
y
e
|
x
==
y
=
e
|
x
/=
y
=
LamVar
x
subst
(
LamAbs
x
e1
)
y
e
|
x
/=
y
&&
not
(
free
x
e
)
=
LamAbs
x
(
subst
e1
y
e
)
|
x
/=
y
&&
(
free
x
e
)
=
let
x'
=
(
rename
x
e1
)
in
subst
(
LamAbs
x'
(
subst
e1
x
(
LamVar
x'
)))
y
e
|
x
==
y
=
LamAbs
x
e1
subst
(
LamApp
e1
e2
)
y
e
=
LamApp
(
subst
e1
y
e
)
(
subst
e2
y
e
)
rename
x
e
|
free
(
x
+
1
)
e
=
rename
(
x
+
1
)
e
|
otherwise
=
(
x
+
1
)
innerArithRedn1
::
ArithExpr
->
Maybe
ArithExpr
innerArithRedn1
(
ArithNum
x
)
=
Nothing
innerArithRedn1
e1
|
e1
==
reductionArith
e1
=
Nothing
|
otherwise
=
Just
(
reductionArith
e1
)
reductionArith
(
Mul
(
ArithNum
n
)
(
ArithNum
m
))
=
ArithNum
(
n
*
m
)
reductionArith
(
Add
(
ArithNum
n
)
(
ArithNum
m
))
=
ArithNum
(
n
+
m
)
reductionArith
(
SecApp
(
Section
(
ArithNum
n
))
(
ArithNum
m
))
=
ArithNum
(
n
+
m
)
reductionArith
(
Mul
x
@
(
ArithNum
y
)
e1
)
=
(
Mul
x
(
reductionArith
e1
))
reductionArith
(
Add
x
@
(
ArithNum
y
)
e1
)
=
(
Add
x
(
reductionArith
e1
))
reductionArith
(
SecApp
(
Section
(
ArithNum
n
))
e2
)
=
(
SecApp
(
Section
(
ArithNum
n
))
(
reductionArith
e2
))
reductionArith
(
SecApp
(
Section
e1
)
e2
)
=
(
SecApp
(
Section
(
reductionArith
e1
))
e2
)
reductionArith
(
Mul
e1
e2
)
=
(
Mul
(
reductionArith
e1
)
e2
)
reductionArith
(
Add
e1
e2
)
=
(
Add
(
reductionArith
e1
)
e2
)
compareArithLam
::
ArithExpr
->
(
Int
,
Int
)
compareArithLam
e1
=
(
evalArithm
e1
0
,
evalLambda
(
churchEnc
e1
)
0
)
evalArithm
e1
z
|
(
innerArithRedn1
e1
)
==
Nothing
=
z
|
otherwise
=
evalArithm
(
fromJust
(
innerArithRedn1
e1
))
(
z
+
1
)
evalLambda
e1
z
|
(
innerRedn1
e1
)
==
Nothing
=
z
|
otherwise
=
evalLambda
(
fromJust
(
innerRedn1
e1
))
(
z
+
1
)
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment