Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Contribute to GitLab
Sign in
Toggle navigation
C
cpdt
Project
Project
Details
Activity
Cycle Analytics
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Charts
Issues
0
Issues
0
List
Board
Labels
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Charts
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Charts
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
research
cpdt
Commits
28f1bb13
Commit
28f1bb13
authored
Oct 03, 2008
by
Adam Chlipala
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
maybe and sumor
parent
5eac1280
Changes
1
Show whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
120 additions
and
2 deletions
+120
-2
Subset.v
src/Subset.v
+120
-2
No files found.
src/Subset.v
View file @
28f1bb13
...
@@ -421,22 +421,95 @@ let rec in_dec a_eq_dec x = function
...
@@ -421,22 +421,95 @@ let rec in_dec a_eq_dec x = function
(
**
*
Partial
Subset
Types
*
)
(
**
*
Partial
Subset
Types
*
)
(
**
Our
final
implementation
of
dependent
predecessor
used
a
very
specific
argument
type
to
ensure
that
execution
could
always
complete
normally
.
Sometimes
we
want
to
allow
execution
to
fail
,
and
we
want
a
more
principled
way
of
signaling
that
than
returning
a
default
value
,
as
[
pred
]
does
for
[
0
]
.
One
approach
is
to
define
this
type
family
[
maybe
]
,
which
is
a
version
of
[
sig
]
that
allows
obligation
-
free
failure
.
*
)
Inductive
maybe
(
A
:
Type
)
(
P
:
A
->
Prop
)
:
Set
:=
Inductive
maybe
(
A
:
Type
)
(
P
:
A
->
Prop
)
:
Set
:=
|
Unknown
:
maybe
P
|
Unknown
:
maybe
P
|
Found
:
forall
x
:
A
,
P
x
->
maybe
P
.
|
Found
:
forall
x
:
A
,
P
x
->
maybe
P
.
(
**
We
can
define
some
new
notations
,
analogous
to
those
we
defined
for
subset
types
.
*
)
Notation
"{{ x | P }}"
:=
(
maybe
(
fun
x
=>
P
))
.
Notation
"{{ x | P }}"
:=
(
maybe
(
fun
x
=>
P
))
.
Notation
"??"
:=
(
Unknown
_
)
.
Notation
"??"
:=
(
Unknown
_
)
.
Notation
"[[ x ]]"
:=
(
Found
_
x
_
)
.
Notation
"[[ x ]]"
:=
(
Found
_
x
_
)
.
(
**
Now
our
next
version
of
[
pred
]
is
trivial
to
write
.
*
)
Definition
pred_strong6
(
n
:
nat
)
:
{{
m
|
n
=
S
m
}}.
refine
(
fun
n
=>
match
n
return
{{
m
|
n
=
S
m
}}
with
|
O
=>
??
|
S
n
'
=>
[[
n
'
]]
end
)
;
trivial
.
Defined
.
(
**
Because
we
used
[
maybe
]
,
one
valid
implementation
of
the
type
we
gave
[
pred_strong6
]
would
return
[
??
]
in
every
case
.
We
can
strengthen
the
type
to
rule
out
such
vacuous
implementations
,
and
the
type
family
[
sumor
]
from
the
standard
library
provides
the
easiest
starting
point
.
For
type
[
A
]
and
proposition
[
B
]
,
[
A
+
{
B
}
]
desugars
to
[
sumor
A
B
]
,
whose
values
are
either
values
of
[
A
]
or
proofs
of
[
B
]
.
*
)
Print
sumor
.
(
**
[[
Inductive
sumor
(
A
:
Type
)
(
B
:
Prop
)
:
Type
:=
inleft
:
A
->
A
+
{
B
}
|
inright
:
B
->
A
+
{
B
}
For
inleft
:
Argument
A
is
implicit
For
inright
:
Argument
B
is
implicit
]]
*
)
(
**
We
add
notations
for
easy
use
of
the
[
sumor
]
constructors
.
The
second
notation
is
specialized
to
[
sumor
]
s
whose
[
A
]
parameters
are
instantiated
with
regular
subset
types
,
since
this
is
how
we
will
use
[
sumor
]
below
.
*
)
Notation
"!!"
:=
(
inright
_
_
)
.
Notation
"[[[ x ]]]"
:=
(
inleft
_
[
x
])
.
(
**
Now
we
are
ready
to
give
the
final
version
of
possibly
-
failing
predecessor
.
The
[
sumor
]
-
based
type
that
we
use
is
maximally
expressive
;
any
implementation
of
the
type
has
the
same
input
-
output
behavior
.
*
)
Definition
pred_strong7
(
n
:
nat
)
:
{
m
:
nat
|
n
=
S
m
}
+
{
n
=
0
}.
refine
(
fun
n
=>
match
n
return
{
m
:
nat
|
n
=
S
m
}
+
{
n
=
0
}
with
|
O
=>
!!
|
S
n
'
=>
[[[
n
'
]]]
end
)
;
trivial
.
Defined
.
(
**
*
Monadic
Notations
*
)
(
**
We
can
treat
[
maybe
]
like
a
monad
,
in
the
same
way
that
the
Haskell
[
Maybe
]
type
is
interpreted
as
a
failure
monad
.
Our
[
maybe
]
has
the
wrong
type
to
be
a
literal
monad
,
but
a
"bind"
-
like
notation
will
still
be
helpful
.
*
)
Notation
"x <- e1 ; e2"
:=
(
match
e1
with
Notation
"x <- e1 ; e2"
:=
(
match
e1
with
|
Unknown
=>
??
|
Unknown
=>
??
|
Found
x
_
=>
e2
|
Found
x
_
=>
e2
end
)
end
)
(
right
associativity
,
at
level
60
)
.
(
right
associativity
,
at
level
60
)
.
Notation
"e1 ;; e2"
:=
(
if
e1
then
e2
else
??
)
(
**
The
meaning
of
[
x
<-
e1
;
e2
]
is
:
First
run
[
e1
]
.
If
it
fails
to
find
an
answer
,
then
announce
failure
for
our
derived
computation
,
too
.
If
[
e1
]
%
\
textit
{%
#
<
i
>
#
does
#
</
i
>
#
%}%
find
an
answer
,
pass
that
answer
on
to
[
e2
]
to
find
the
final
result
.
The
variable
[
x
]
can
be
considered
bound
in
[
e2
]
.
(
right
associativity
,
at
level
60
)
.
This
notation
is
very
helpful
for
composing
richly
-
typed
procedures
.
For
instance
,
here
is
a
very
simple
implementation
of
a
function
to
take
the
predecessors
of
two
naturals
at
once
.
*
)
Definition
doublePred
(
n1
n2
:
nat
)
:
{{
p
|
n1
=
S
(
fst
p
)
/
\
n2
=
S
(
snd
p
)
}}.
refine
(
fun
n1
n2
=>
m1
<-
pred_strong6
n1
;
m2
<-
pred_strong6
n2
;
[[(
m1
,
m2
)]])
;
tauto
.
Defined
.
(
**
We
can
build
a
[
sumor
]
version
of
the
"bind"
notation
and
use
it
to
write
a
similarly
straightforward
version
of
this
function
.
*
)
(
**
printing
<--
$
\
longleftarrow
$
*
)
Notation
"x <-- e1 ; e2"
:=
(
match
e1
with
|
inright
_
=>
!!
|
inleft
(
exist
x
_
)
=>
e2
end
)
(
right
associativity
,
at
level
60
)
.
(
**
printing
*
$
\
times
$
*
)
Definition
doublePred
'
(
n1
n2
:
nat
)
:
{
p
:
nat
*
nat
|
n1
=
S
(
fst
p
)
/
\
n2
=
S
(
snd
p
)
}
+
{
n1
=
0
\
/
n2
=
0
}.
refine
(
fun
n1
n2
=>
m1
<--
pred_strong7
n1
;
m2
<--
pred_strong7
n2
;
[[[(
m1
,
m2
)]]])
;
tauto
.
Defined
.
(
**
*
A
Type
-
Checking
Example
*
)
(
**
*
A
Type
-
Checking
Example
*
)
...
@@ -467,6 +540,9 @@ Definition eq_type_dec : forall (t1 t2 : type), {t1 = t2} + {t1 <> t2}.
...
@@ -467,6 +540,9 @@ Definition eq_type_dec : forall (t1 t2 : type), {t1 = t2} + {t1 <> t2}.
decide
equality
.
decide
equality
.
Defined
.
Defined
.
Notation
"e1 ;; e2"
:=
(
if
e1
then
e2
else
??
)
(
right
associativity
,
at
level
60
)
.
Definition
typeCheck
(
e
:
exp
)
:
{{
t
|
hasType
e
t
}}.
Definition
typeCheck
(
e
:
exp
)
:
{{
t
|
hasType
e
t
}}.
Hint
Constructors
hasType
.
Hint
Constructors
hasType
.
...
@@ -492,3 +568,45 @@ Defined.
...
@@ -492,3 +568,45 @@ Defined.
Eval
simpl
in
typeCheck
(
Nat
0
)
.
Eval
simpl
in
typeCheck
(
Nat
0
)
.
Eval
simpl
in
typeCheck
(
Plus
(
Nat
1
)
(
Nat
2
))
.
Eval
simpl
in
typeCheck
(
Plus
(
Nat
1
)
(
Nat
2
))
.
Eval
simpl
in
typeCheck
(
Plus
(
Nat
1
)
(
Bool
false
))
.
Eval
simpl
in
typeCheck
(
Plus
(
Nat
1
)
(
Bool
false
))
.
Print
sumor
.
Notation
"e1 ;;; e2"
:=
(
if
e1
then
e2
else
!!
)
(
right
associativity
,
at
level
60
)
.
Theorem
hasType_det
:
forall
e
t1
,
hasType
e
t1
->
forall
t2
,
hasType
e
t2
->
t1
=
t2
.
induction
1
;
inversion
1
;
crush
.
Qed
.
Definition
typeCheck
'
(
e
:
exp
)
:
{
t
:
type
|
hasType
e
t
}
+
{
forall
t
,
~
hasType
e
t
}.
Hint
Constructors
hasType
.
Hint
Resolve
hasType_det
.
refine
(
fix
F
(
e
:
exp
)
:
{
t
:
type
|
hasType
e
t
}
+
{
forall
t
,
~
hasType
e
t
}
:=
match
e
return
{
t
:
type
|
hasType
e
t
}
+
{
forall
t
,
~
hasType
e
t
}
with
|
Nat
_
=>
[[[
TNat
]]]
|
Plus
e1
e2
=>
t1
<--
F
e1
;
t2
<--
F
e2
;
eq_type_dec
t1
TNat
;;;
eq_type_dec
t2
TNat
;;;
[[[
TNat
]]]
|
Bool
_
=>
[[[
TBool
]]]
|
And
e1
e2
=>
t1
<--
F
e1
;
t2
<--
F
e2
;
eq_type_dec
t1
TBool
;;;
eq_type_dec
t2
TBool
;;;
[[[
TBool
]]]
end
)
;
clear
F
;
crush
'
tt
hasType
;
eauto
.
Defined
.
Eval
simpl
in
typeCheck
'
(
Nat
0
)
.
Eval
simpl
in
typeCheck
'
(
Plus
(
Nat
1
)
(
Nat
2
))
.
Eval
simpl
in
typeCheck
'
(
Plus
(
Nat
1
)
(
Bool
false
))
.
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