Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in / Register
Toggle navigation
I
iTypes
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Locked Files
Issues
0
Issues
0
List
Boards
Labels
Service Desk
Milestones
Iterations
Merge Requests
0
Merge Requests
0
Requirements
Requirements
List
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Test Cases
Security & Compliance
Security & Compliance
Dependency List
License Compliance
Operations
Operations
Incidents
Environments
Packages & Registries
Packages & Registries
Package Registry
Container Registry
Analytics
Analytics
CI / CD
Code Review
Insights
Issue
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
PLMZ
iTypes
Commits
c97951ae
Commit
c97951ae
authored
Sep 28, 2019
by
André Pacak
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
fo recursive types remove context argument
parent
f802b67b
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
345 additions
and
0 deletions
+345
-0
haskell/src/FORecursiveTypes/EliminateContextArgument.hs
haskell/src/FORecursiveTypes/EliminateContextArgument.hs
+320
-0
haskell/test/FORecursiveTypes/EliminateContextArgumentSpec.hs
...ell/test/FORecursiveTypes/EliminateContextArgumentSpec.hs
+25
-0
No files found.
haskell/src/FORecursiveTypes/EliminateContextArgument.hs
0 → 100644
View file @
c97951ae
{-# LANGUAGE ConstraintKinds, TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RebindableSyntax #-}
module
FORecursiveTypes.EliminateContextArgument
where
import
Prelude
hiding
(
Monad
(
..
),
(
>=
),
(
<=
),
lookup
)
import
GHC.Exts
(
Constraint
)
import
Data.List
(
find
)
import
Data.Maybe
(
isJust
,
fromJust
)
import
Data.Map
(
Map
)
import
qualified
Data.Map
as
Map
import
FORecursiveTypes.Language
import
Util.ErrorMessages
-- is needed because we use the RebindableSyntax extension
ifThenElse
::
Bool
->
a
->
a
->
a
ifThenElse
True
thn
_
=
thn
ifThenElse
False
_
els
=
els
type
Error
=
[
String
]
data
Infer
a
=
Inferred
a
|
NotInferred
Error
deriving
(
Eq
,
Show
)
type
Check
=
Infer
()
instance
Functor
Infer
where
fmap
_
(
NotInferred
err
)
=
NotInferred
err
fmap
f
(
Inferred
ty
)
=
Inferred
$
f
ty
instance
Applicative
Infer
where
pure
=
Inferred
(
NotInferred
err
)
<*>
_
=
NotInferred
err
(
Inferred
a
)
<*>
something
=
fmap
a
something
class
WithTop
a
where
top
::
a
instance
WithTop
Type
where
top
=
AnyType
instance
WithTop
()
where
top
=
()
instance
(
WithTop
a
,
WithTop
b
)
=>
WithTop
(
a
,
b
)
where
top
=
(
top
,
top
)
instance
WithTop
a
=>
WithTop
[
a
]
where
top
=
[
top
]
instance
WithTop
a
=>
WithTop
(
Map
Name
a
)
where
top
=
Map
.
empty
-- Had to define an own monad type class.
-- It is not possible otherwise to get the type constraint WithTop a.
-- We use the extension ConstraintKinds to support this.
-- Could not find a simpler solution for this problem.
-- The restricted monad problem is common.
class
RMonad
m
where
type
RMonadCtx
m
a
::
Constraint
return
::
RMonadCtx
m
a
=>
a
->
m
a
(
>>=
)
::
(
RMonadCtx
m
a
,
RMonadCtx
m
b
)
=>
m
a
->
(
a
->
m
b
)
->
m
b
(
>>
)
::
(
RMonadCtx
m
a
,
RMonadCtx
m
b
)
=>
m
a
->
m
b
->
m
b
m
>>
k
=
m
>>=
\
_
->
k
fail
::
[
String
]
->
m
a
instance
RMonad
Infer
where
type
RMonadCtx
Infer
a
=
WithTop
a
return
=
Inferred
(
Inferred
ty
)
>>=
f
=
f
ty
NotInferred
err1
>>=
f
=
-- we know that top is Inferred AnyType, (AnyType, AnyType) or () by definition
case
f
top
of
Inferred
_
->
fail
err1
NotInferred
err2
->
fail
$
err1
++
err2
fail
=
NotInferred
-- matching functions that extract the inner types if possible
-- one problem is that we do not get as good error messages, because term is not known in these functions
matchNat
::
Type
->
String
->
Check
matchNat
Nat
_
=
return
()
matchNat
ty
err
=
fail
[
natError
ty
err
]
matchFun
::
Type
->
String
->
Infer
(
Type
,
Type
)
matchFun
(
Fun
ty1
ty2
)
_
=
return
(
ty1
,
ty2
)
matchFun
ty
err
=
fail
[
funError
ty
err
]
matchType
::
Type
->
Type
->
String
->
Check
matchType
ty1
ty2
_
|
ty1
==
ty2
=
return
()
matchType
ty1
ty2
err
=
fail
[
generalError
(
show
ty1
)
ty2
err
]
matchSum
::
Type
->
String
->
Infer
(
Type
,
Type
)
matchSum
(
Sum
ty1
ty2
)
_
=
return
(
ty1
,
ty2
)
matchSum
ty
err
=
fail
[
sumError
ty
err
]
matchVariant
::
Type
->
String
->
Infer
(
Map
.
Map
Name
Type
)
matchVariant
(
Variant
types
)
_
=
return
types
matchVariant
ty
err
=
fail
[
variantError
ty
err
]
lookupTypeVar
::
TypeMap
->
Name
->
Infer
Type
lookupTypeVar
Empty
x
=
fail
[
"Unbound type variable "
++
show
x
]
lookupTypeVar
(
Bind
c
x
t
)
y
|
x
==
y
=
return
t
|
otherwise
=
lookupTypeVar
c
y
matchTypeVar
::
TypeMap
->
Type
->
Infer
Type
matchTypeVar
tymap
(
TypeVar
x
)
=
lookupTypeVar
tymap
x
matchTypeVar
_
ty
=
return
ty
liftMaybe
::
WithTop
a
=>
Maybe
a
->
String
->
Infer
a
liftMaybe
(
Just
a
)
_
=
return
a
liftMaybe
Nothing
err
=
fail
[
err
]
lookup
::
TypeMap
->
Term
->
Name
->
Infer
Type
lookup
tymap
t
x
=
case
parent
t
of
Just
p
@
(
Succ
t
_
)
->
do
lookup
tymap
p
x
Just
p
@
(
Add
t1
t2
_
)
|
t
==
t1
->
do
lookup
tymap
p
x
Just
p
@
(
Add
t1
t2
_
)
|
t
==
t2
->
do
lookup
tymap
p
x
Just
p
@
(
Mult
t1
t2
_
)
|
t
==
t1
->
do
lookup
tymap
p
x
Just
p
@
(
Mult
t1
t2
_
)
|
t
==
t2
->
do
lookup
tymap
p
x
Just
p
@
(
Var
name
_
)
->
do
lookup
tymap
p
x
Just
p
@
(
Let
name
term
body
_
)
|
t
==
term
->
do
lookup
tymap
p
x
Just
p
@
(
Let
name
term
body
_
)
|
t
==
body
->
if
name
==
x
then
do
ty
<-
inferType
tymap
term
return
ty
else
lookup
tymap
p
x
Just
p
@
(
Anno
term
ty
_
)
->
do
lookup
tymap
p
x
Just
p
@
(
App
t1
t2
_
)
|
t
==
t1
->
do
lookup
tymap
p
x
Just
p
@
(
App
t1
t2
_
)
|
t
==
t2
->
do
lookup
tymap
p
x
Just
p
@
(
Lam
name
term
_
)
->
if
name
==
x
then
do
ty
<-
requiredType
tymap
p
(
ty1
,
ty2
)
<-
matchFun
ty
(
show
p
)
return
ty1
else
lookup
tymap
p
x
Just
p
@
(
InL
term
_
)
->
do
lookup
tymap
p
x
Just
p
@
(
InR
term
_
)
->
do
lookup
tymap
p
x
Just
p
@
(
Case
e
n1
t1
n2
t2
_
)
|
t
==
t1
->
if
n1
==
x
then
do
ety
<-
inferType
tymap
e
(
ty1
,
ty2
)
<-
matchSum
ety
(
show
e
)
return
ty1
else
lookup
tymap
p
x
Just
p
@
(
Case
e
n1
t1
n2
t2
_
)
|
t
==
t2
->
if
n2
==
x
then
do
ety
<-
inferType
tymap
e
(
ty1
,
ty2
)
<-
matchSum
ety
(
show
e
)
return
ty2
else
lookup
tymap
p
x
Just
p
@
(
Tag
n
t'
_
)
|
t
==
t'
->
do
lookup
tymap
p
x
Just
p
@
(
Match
m
cases
_
)
|
t
==
m
->
do
lookup
tymap
p
x
Just
p
@
(
Match
m
cases
_
)
|
t
/=
m
->
do
ety
<-
inferType
tymap
m
typeMap
<-
matchVariant
ety
(
show
m
)
let
ml
=
find
(
\
(
_
,
x'
,
t'
)
->
t
==
t'
&&
x
==
x'
)
cases
if
isJust
ml
then
do
let
(
l
,
_
,
_
)
=
fromJust
ml
liftMaybe
(
Map
.
lookup
l
typeMap
)
"Could not find labeled type"
else
lookup
tymap
p
x
Just
p
@
(
LetType
x
ty
term
_
)
|
t
==
term
->
do
lookup
tymap
p
x
Just
p
->
do
lookup
tymap
p
x
Nothing
->
fail
[
"Unbound variable "
++
show
x
]
inferType
::
TypeMap
->
Term
->
Infer
Type
inferType
_
(
Unit
_
)
=
return
UnitT
inferType
_
(
Zero
_
)
=
return
Nat
inferType
tymap
(
Succ
t
_
)
=
do
checkType
tymap
t
return
Nat
inferType
tymap
(
Add
t1
t2
_
)
=
do
checkType
tymap
t1
checkType
tymap
t2
return
Nat
inferType
tymap
(
Mult
t1
t2
_
)
=
do
checkType
tymap
t1
checkType
tymap
t2
return
Nat
inferType
tymap
p
@
(
Var
name
_
)
=
lookup
tymap
p
name
inferType
tymap
(
Let
name
t
body
_
)
=
do
tyt
<-
inferType
tymap
t
inferType
tymap
body
inferType
tymap
(
Anno
term
ty
_
)
=
do
checkType
tymap
term
return
ty
inferType
tymap
(
App
t1
t2
_
)
=
do
ty
<-
inferType
tymap
t1
rty
<-
matchTypeVar
tymap
ty
(
ty1
,
ty2
)
<-
matchFun
rty
(
show
t1
)
checkType
tymap
t2
return
ty2
inferType
tymap
(
LetType
n
ty
t
_
)
=
inferType
(
Bind
tymap
n
ty
)
t
inferType
_
t
=
fail
[
"Cannot infer type of term "
++
show
t
]
checkType
::
TypeMap
->
Term
->
Check
checkType
tymap
p
@
(
Lam
name
t
_
)
=
do
ty
<-
requiredType
tymap
p
rty
<-
matchTypeVar
tymap
ty
(
ty1
,
ty2
)
<-
matchFun
rty
(
show
p
)
checkType
tymap
t
checkType
tymap
p
@
(
InL
t
_
)
=
do
ty
<-
requiredType
tymap
p
rty
<-
matchTypeVar
tymap
ty
(
ty1
,
ty2
)
<-
matchSum
rty
(
show
p
)
checkType
tymap
t
checkType
tymap
p
@
(
InR
t
_
)
=
do
ty
<-
requiredType
tymap
p
rty
<-
matchTypeVar
tymap
ty
(
ty1
,
ty2
)
<-
matchSum
rty
(
show
p
)
checkType
tymap
t
checkType
tymap
p
@
(
Case
e
n1
t1
n2
t2
_
)
=
do
ety
<-
inferType
tymap
e
rty
<-
matchTypeVar
tymap
ety
(
ty1
,
ty2
)
<-
matchSum
rty
(
show
e
)
ty
<-
requiredType
tymap
p
checkType
tymap
t1
checkType
tymap
t2
checkType
tymap
p
@
(
Tag
n
t
_
)
=
do
ty
<-
requiredType
tymap
p
rty
<-
matchTypeVar
tymap
ty
types
<-
matchVariant
rty
(
show
p
)
let
lty
=
Map
.
lookup
n
types
lty
<-
liftMaybe
(
Map
.
lookup
n
types
)
"Label not contained in Variant"
checkType
tymap
t
checkType
tymap
p
@
(
Match
m
cases
_
)
=
do
ety
<-
inferType
tymap
m
rty
<-
matchTypeVar
tymap
ety
types
<-
matchVariant
rty
(
show
m
)
ty
<-
requiredType
tymap
p
let
subchecks
=
map
(
\
(
l
,
x
,
t
)
->
do
lty
<-
liftMaybe
(
Map
.
lookup
l
types
)
"Could not find labeled type"
checkType
tymap
t
)
cases
foldl
(
>>
)
(
return
()
)
subchecks
checkType
tymap
t
=
do
ty
<-
requiredType
tymap
t
ty'
<-
inferType
tymap
t
matchType
ty
ty'
(
show
t
)
requiredType
::
TypeMap
->
Term
->
Infer
Type
requiredType
tymap
t
=
case
parent
t
of
Just
(
Succ
t'
_
)
|
t
==
t'
->
return
Nat
Just
(
Add
t1
t2
_
)
|
t
==
t1
->
return
Nat
Just
(
Add
t1
t2
_
)
|
t
==
t2
->
return
Nat
Just
(
Mult
t1
t2
_
)
|
t
==
t1
->
return
Nat
Just
(
Mult
t1
t2
_
)
|
t
==
t2
->
return
Nat
Just
(
Anno
term
ty
_
)
|
t
==
term
->
return
ty
Just
p
@
(
App
t1
t2
_
)
|
t
==
t2
->
do
ty
<-
inferType
tymap
t1
rty
<-
matchTypeVar
tymap
ty
(
ty1
,
ty2
)
<-
matchFun
rty
(
show
t1
)
return
ty1
Just
p
@
(
Lam
name
term
_
)
|
t
==
term
->
do
ty
<-
requiredType
tymap
p
rty
<-
matchTypeVar
tymap
ty
(
ty1
,
ty2
)
<-
matchFun
rty
(
show
p
)
return
ty2
Just
p
@
(
InL
term
_
)
|
t
==
term
->
do
ty
<-
requiredType
tymap
p
rty
<-
matchTypeVar
tymap
ty
(
ty1
,
ty2
)
<-
matchSum
rty
(
show
p
)
return
ty1
Just
p
@
(
InR
term
_
)
|
t
==
term
->
do
ty
<-
requiredType
tymap
p
rty
<-
matchTypeVar
tymap
ty
(
ty1
,
ty2
)
<-
matchSum
rty
(
show
p
)
return
ty2
Just
p
@
(
Case
e
n1
t1
n2
t2
_
)
|
t
==
t1
->
do
ety
<-
inferType
tymap
e
rty
<-
matchTypeVar
tymap
ety
(
ty1
,
ty2
)
<-
matchSum
rty
(
show
e
)
ty
<-
requiredType
tymap
p
return
ty
Just
p
@
(
Case
e
n1
t1
n2
t2
_
)
|
t
==
t2
->
do
ety
<-
inferType
tymap
e
rty
<-
matchTypeVar
tymap
ety
(
ty1
,
ty2
)
<-
matchSum
rty
(
show
e
)
ty
<-
requiredType
tymap
p
return
ty
Just
p
@
(
Tag
n
term
_
)
|
t
==
term
->
do
ty
<-
requiredType
tymap
p
rty
<-
matchTypeVar
tymap
ty
types
<-
matchVariant
rty
(
show
p
)
let
lty
=
Map
.
lookup
n
types
liftMaybe
(
Map
.
lookup
n
types
)
"Label not contained in Variant"
Just
p
@
(
Match
m
cases
_
)
->
do
ty
<-
requiredType
tymap
p
return
ty
_
->
fail
[
"Could not determine required type"
]
haskell/test/FORecursiveTypes/EliminateContextArgumentSpec.hs
0 → 100644
View file @
c97951ae
{-# LANGUAGE FlexibleInstances #-}
module
FORecursiveTypes.EliminateContextArgumentSpec
where
import
Prelude
hiding
(
lookup
,(
*
),
(
**
))
import
Test.Hspec
import
FORecursiveTypes.Base
as
B
import
FORecursiveTypes.SharedSpecs
import
FORecursiveTypes.EliminateContextArgument
as
E
import
FORecursiveTypes.Language
instance
ConvertToBInfer
E
.
Infer
where
convert
(
E
.
Inferred
ty
)
=
B
.
Inferred
ty
convert
(
E
.
NotInferred
err
)
=
B
.
NotInferred
$
head
err
main
::
IO
()
main
=
hspec
spec
spec
::
Spec
spec
=
sharedSpec
$
E
.
inferType
Empty
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment