Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
CHARGUERAUD Arthur
cfml
Commits
51dd8f50
Commit
51dd8f50
authored
Mar 31, 2016
by
charguer
Browse files
progress_generator
parent
9a77f4db
Changes
9
Hide whitespace changes
Inline
Side-by-side
Makefile
View file @
51dd8f50
...
...
@@ -31,6 +31,11 @@ coqlib:
coqlib_quick
:
$(MAKE)
-C
lib/coq quick
coqlib_quick_cf
:
$(MAKE)
-C
lib/coq quick_cf
#------ TODO: ocamllib is deprecated
ocamllib
:
tools
$(MAKE)
-C
lib/ocaml
...
...
examples/BasicDemos/Demo.ml
View file @
51dd8f50
...
...
@@ -69,7 +69,7 @@ let let_val_pair_int () =
x
let
let_val_poly
()
=
let
x
=
[]
in
let
_
x
=
[]
in
3
...
...
@@ -135,7 +135,7 @@ let app_partial_add () =
let
app_partial_appto
()
=
let
appto
x
f
=
f
x
in
let
r
=
appto
3
((
+
)
1
)
in
let
_
r
=
appto
3
((
+
)
1
)
in
appto
3
(
fun
x
->
x
+
1
)
let
test_partial_app_arities
()
=
...
...
@@ -271,10 +271,10 @@ let sitems_push x r =
let
array_ops
()
=
let
t
=
Array
.
make
3
0
in
let
x
=
t
.
(
1
)
in
let
_
x
=
t
.
(
1
)
in
t
.
(
2
)
<-
4
;
let
y
=
t
.
(
2
)
in
let
z
=
t
.
(
1
)
in
let
_
y
=
t
.
(
2
)
in
let
_
z
=
t
.
(
1
)
in
Array
.
length
t
...
...
@@ -316,10 +316,6 @@ let rec rec_partial_half x =
(********************************************************************)
(* ** External *)
external
external_mono
:
int
=
"%external_mono"
external
external_poly
:
'
a
=
"%external_poly"
external
external_func
:
int
->
'
a
->
'
a
array
=
"%external_func"
...
...
@@ -333,6 +329,9 @@ type 'a type_homo_pair = ('a * 'a)
type
(
'
a
,
'
b
)
type_poly_pair
=
((
'
a
*
'
b
)
*
(
'
a
*
'
b
))
let
type_clashing_with_var
=
3
type
type_clashing_with_var
=
int
(********************************************************************)
(* ** Type algebraic *)
...
...
@@ -346,7 +345,7 @@ type 'a alga_three =
type
(
'
a
,
'
b
)
algb_erase
=
|
Algb_A
of
'
a
|
Algb_B
of
int
->
'
b
|
Algb_B
of
(
int
->
'
b
)
(********************************************************************)
...
...
@@ -374,8 +373,8 @@ type typerecb1 = | Typerecb_1 of typerecb2
work around by inlining, e.g.:
*)
type
typerec
b
1
=
|
Typerec
b
_1
of
typerec
b
1
list
type
typerec
b
2
=
typerec
b
1
list
type
typerec
c
1
=
|
Typerec
c
_1
of
typerec
c
1
list
type
typerec
c
2
=
typerec
c
1
list
...
...
@@ -385,7 +384,7 @@ type typerecb2 = typerecb1 list
module
ModFoo
=
struct
type
t
=
int
val
x
:
t
=
3
let
x
:
t
=
3
end
...
...
@@ -402,7 +401,7 @@ end
module
ModBar
:
ModBarType
=
struct
type
t
=
int
val
x
:
t
=
3
let
x
:
t
=
3
end
...
...
@@ -413,14 +412,14 @@ end
module
ModFunctor
(
Bar
:
ModBarType
)
=
struct
type
u
=
Bar
.
t
val
x
:
u
=
Bar
.
x
let
x
:
u
=
Bar
.
x
end
module
ModFunctorTyped
(
Bar
:
ModBarType
)
:
ModBarType
=
struct
type
t
=
Bar
.
t
val
x
:
t
=
Bar
.
x
let
x
:
t
=
Bar
.
x
end
...
...
examples/Makefile.example
View file @
51dd8f50
...
...
@@ -94,7 +94,7 @@ cf: $(ML)
# Make sure TLC and CFML itself are up-to-date.
# Needed only when developing TLC and CFML. Ideally, should be removed.
@$(MAKE)
-C
$(CFML)/lib/tlc
--no-print-directory
quick
@$(MAKE)
-C
$(CFML)
--no-print-directory
quick
@$(MAKE)
-C
$(CFML)
--no-print-directory
tools
coqlib_
quick
_cf
@$(MAKE)
CFML
=
$(CFML)
OCAML_FLAGS
=
$(OCAML_FLAGS)
COQINCLUDE
=
"
$(COQINCLUDE)
"
ML
=
"
$(ML)
"
--no-print-directory
-f
$(CFML)
/lib/make/Makefile.cf all
proof
:
cf
...
...
generator/characteristic.ml
View file @
51dd8f50
...
...
@@ -47,10 +47,15 @@ let external_modules_reset () =
let
lift_ident_name
id
=
let
name
=
Ident
.
name
id
in
if
name
=
"OkaStream"
then
"CFPrim"
else
(* TODO : improve *)
let
coqname
=
name
^
"_"
in
if
Ident
.
persistent
id
then
external_modules_add
coqname
;
coqname
(* -- old:
if Ident.persistent id
then (let result = name ^ "_ml" in external_modules_add result; result)
else "ML" ^ name
*)
(* -- old: if name = "OkaStream" then "CFPrim" else *)
let
rec
lift_full_path
=
function
|
Pident
id
->
Pident
(
Ident
.
create
(
lift_ident_name
id
))
...
...
generator/normalize.ml
View file @
51dd8f50
...
...
@@ -24,9 +24,13 @@ let fullname_of_lident idt =
String
.
concat
"."
words
let
check_var
loc
x
=
if
loc
.
loc_ghost
then
()
else
(* todo: avoid this hack *)
if
String
.
length
x
>
1
&&
x
.
[
0
]
=
'
_'
then
unsupported
(
"variables cannot be prefixed with underscore: "
^
x
)
(* Reject program containing variables with a trailing underscore,
as we use such an underscore to disambiguate with type variables *)
let
n
=
String
.
length
x
in
if
n
>
0
&&
x
.
[
n
-
1
]
=
'
_'
then
unsupported
(
"variables names should not end with an underscore: "
^
x
)
(* --is this line needed? if loc.loc_ghost then () else *)
let
check_lident
loc
idt
=
check_var
loc
(
name_of_lident
idt
)
...
...
generator/print_coq.ml
View file @
51dd8f50
...
...
@@ -105,7 +105,8 @@ let tuple expr es =
(* -------------------------------------------------------------------------- *)
(* Labels (part of [Coq_tag]). *)
(* FOR FUTURE USE
Labels (part of [Coq_tag]). *)
let
label
=
function
|
None
->
...
...
@@ -161,7 +162,7 @@ and expr1 = function
apps
[
string
"@CFPrint.tag"
;
string
tag
;
label
l
;
(* FUTURE USE:
label l;
*)
string
"_"
;
expr0
e
]
...
...
generator/print_type.ml
View file @
51dd8f50
...
...
@@ -61,7 +61,7 @@ let mark_loops = mark_loops
let
name_of_type
ty
=
let
ty
=
proxy
ty
in
let
x
=
name_of_type
ty
in
"_"
^
(
String
.
uppercase
x
)
(
String
.
uppercase
x
)
^
"_"
let
reset_names
=
reset_names
...
...
lib/coq/CFPrint.v
View file @
51dd8f50
...
...
@@ -213,7 +213,7 @@ Notation "'LetApp' x ':=' f xs 'in' F2" :=
-
(
at
level
69
,
x
ident
,
f
at
level
0
,
x1
at
level
0
,
x2
at
level
0
,
*
)
Notation
"'SeqApp' f xs ;;
Q
2"
:=
Notation
"'SeqApp' f xs ;;
F
2"
:=
(
!
Seq
(
fun
H
Q
=>
exists
Q
'
,
(
App
f
xs
;)
H
Q
'
/
\
F2
(
Q
'
tt
)
Q
))
(
at
level
68
,
f
at
level
0
,
xs
at
level
0
,
right
associativity
,
format
"'[v' 'SeqApp' '[' f xs ']' ;; '/' '[' F2 ']' ']'"
)
:
charac
.
...
...
@@ -371,7 +371,7 @@ Notation "F1 ;; F2" :=
(
********************************************************************
)
(
**
Assert
*
)
Notation
"'Assert
_' ;;
F1"
:=
Notation
"'Assert
'
F1"
:=
(
!
Assert
(
fun
H
Q
=>
F1
H
(
fun
(
b
:
bool
)
=>
\
[
b
=
true
]
\
*
H
)
/
\
H
==>
Q
tt
))
(
at
level
68
,
right
associativity
,
format
"'[v' 'Assert' F1 ']'"
)
:
charac
.
...
...
@@ -405,45 +405,45 @@ Notation "'IfProp' P 'Then' F1 'Else' F2" :=
(
********************************************************************
)
(
**
Case
*
)
Notation
"'Case' x '=' p 'Then' F1 'Else'
Q
2"
:=
Notation
"'Case' x '=' p 'Then' F1 'Else'
F
2"
:=
(
!
Case
(
fun
H
Q
=>
(
x
=
p
->
F1
H
Q
)
/
\
(
x
<>
p
->
F2
H
Q
)))
(
at
level
69
,
x
at
level
0
)
:
charac
.
Notation
"'Case' x '=' p [ x1 ] 'Then' F1 'Else'
Q
2"
:=
Notation
"'Case' x '=' p [ x1 ] 'Then' F1 'Else'
F
2"
:=
(
!
Case
(
fun
H
Q
=>
(
forall
x1
,
x
=
p
->
F1
H
Q
)
/
\
((
forall
x1
,
x
<>
p
)
->
F2
H
Q
)))
(
at
level
69
,
x
at
level
0
,
x1
ident
)
:
charac
.
Notation
"'Case' x '=' p [ x1 x2 ] 'Then' F1 'Else'
Q
2"
:=
Notation
"'Case' x '=' p [ x1 x2 ] 'Then' F1 'Else'
F
2"
:=
(
!
Case
(
fun
H
Q
=>
(
forall
x1
x2
,
x
=
p
->
F1
H
Q
)
/
\
((
forall
x1
x2
,
x
<>
p
)
->
F2
H
Q
)))
(
at
level
69
,
x
at
level
0
,
x1
ident
,
x2
ident
)
:
charac
.
Notation
"'Case' x '=' p [ x1 x2 x3 ] 'Then' F1 'Else'
Q
2"
:=
Notation
"'Case' x '=' p [ x1 x2 x3 ] 'Then' F1 'Else'
F
2"
:=
(
!
Case
(
fun
H
Q
=>
(
forall
x1
x2
x3
,
x
=
p
->
F1
H
Q
)
/
\
((
forall
x1
x2
x3
,
x
<>
p
)
->
F2
H
Q
)))
(
at
level
69
,
x
at
level
0
,
x1
ident
,
x2
ident
,
x3
ident
)
:
charac
.
Notation
"'Case' x '=' p [ x1 x2 x3 x4 ] 'Then' F1 'Else'
Q
2"
:=
Notation
"'Case' x '=' p [ x1 x2 x3 x4 ] 'Then' F1 'Else'
F
2"
:=
(
!
Case
(
fun
H
Q
=>
(
forall
x1
x2
x3
x4
,
x
=
p
->
F1
H
Q
)
/
\
((
forall
x1
x2
x3
x4
,
x
<>
p
)
->
F2
H
Q
)))
(
at
level
69
,
x
at
level
0
,
x1
ident
,
x2
ident
,
x3
ident
,
x4
ident
)
:
charac
.
Notation
"'Case' x '=' p [ x1 x2 x3 x4 x5 ] 'Then' F1 'Else'
Q
2"
:=
Notation
"'Case' x '=' p [ x1 x2 x3 x4 x5 ] 'Then' F1 'Else'
F
2"
:=
(
!
Case
(
fun
H
Q
=>
(
forall
x1
x2
x3
x4
x5
,
x
=
p
->
F1
H
Q
)
/
\
((
forall
x1
x2
x3
x4
x5
,
x
<>
p
)
->
F2
H
Q
)))
(
at
level
69
,
x
at
level
0
,
x1
ident
,
x2
ident
,
x3
ident
,
x4
ident
,
x5
ident
)
:
charac
.
Notation
"'Case' x '=' p [ x1 x2 x3 x4 x5 x6 ] 'Then' F1 'Else'
Q
2"
:=
Notation
"'Case' x '=' p [ x1 x2 x3 x4 x5 x6 ] 'Then' F1 'Else'
F
2"
:=
(
!
Case
(
fun
H
Q
=>
(
forall
x1
x2
x3
x4
x5
x6
,
x
=
p
->
F1
H
Q
)
/
\
((
forall
x1
x2
x3
x4
x5
x6
,
x
<>
p
)
->
F2
H
Q
)))
(
at
level
69
,
x
at
level
0
,
x1
ident
,
x2
ident
,
x3
ident
,
x4
ident
,
x5
ident
,
x6
ident
)
:
charac
.
Notation
"'Case' x '=' p [ x1 x2 x3 x4 x5 x6 x7 ] 'Then' F1 'Else'
Q
2"
:=
Notation
"'Case' x '=' p [ x1 x2 x3 x4 x5 x6 x7 ] 'Then' F1 'Else'
F
2"
:=
(
!
Case
(
fun
H
Q
=>
(
forall
x1
x2
x3
x4
x5
x6
x7
,
x
=
p
->
F1
H
Q
)
/
\
((
forall
x1
x2
x3
x4
x5
x6
x7
,
x
<>
p
)
->
F2
H
Q
)))
(
at
level
69
,
x
at
level
0
,
x1
ident
,
x2
ident
,
...
...
@@ -453,46 +453,46 @@ Notation "'Case' x '=' p [ x1 x2 x3 x4 x5 x6 x7 ] 'Then' F1 'Else' Q2" :=
(
********************************************************************
)
(
**
CaseWhen
*
)
Notation
"'Case' x '=' p 'When' w 'Then' F1 'Else'
Q
2"
:=
Notation
"'Case' x '=' p 'When' w 'Then' F1 'Else'
F
2"
:=
(
!
CaseWhen
(
fun
H
Q
=>
(
x
=
p
->
istrue
(
w
)
%
bool
->
F1
H
Q
)
/
\
(
x
<>
p
\
/
istrue
(
!
w
)
->
F2
H
Q
)))
(
at
level
69
,
x
at
level
0
)
:
charac
.
Notation
"'Case' x '=' p [ x1 ] 'When' w 'Then' F1 'Else'
Q
2"
:=
Notation
"'Case' x '=' p [ x1 ] 'When' w 'Then' F1 'Else'
F
2"
:=
(
!
CaseWhen
(
fun
H
Q
=>
(
forall
x1
,
x
=
p
->
istrue
w
%
bool
->
F1
H
Q
)
/
\
((
forall
x1
,
x
<>
p
\
/
istrue
(
!
w
))
->
F2
H
Q
)))
(
at
level
69
,
x
at
level
0
,
x1
ident
)
:
charac
.
Notation
"'Case' x '=' p [ x1 x2 ] 'When' w 'Then' F1 'Else'
Q
2"
:=
Notation
"'Case' x '=' p [ x1 x2 ] 'When' w 'Then' F1 'Else'
F
2"
:=
(
!
CaseWhen
(
fun
H
Q
=>
(
forall
x1
x2
,
x
=
p
->
istrue
w
%
bool
->
F1
H
Q
)
/
\
((
forall
x1
x2
,
x
<>
p
\
/
istrue
(
!
w
))
->
F2
H
Q
)))
(
at
level
69
,
x
at
level
0
,
x1
ident
,
x2
ident
)
:
charac
.
Notation
"'Case' x '=' p [ x1 x2 x3 ] 'When' w 'Then' F1 'Else'
Q
2"
:=
Notation
"'Case' x '=' p [ x1 x2 x3 ] 'When' w 'Then' F1 'Else'
F
2"
:=
(
!
CaseWhen
(
fun
H
Q
=>
(
forall
x1
x2
x3
,
x
=
p
->
istrue
w
%
bool
->
F1
H
Q
)
/
\
((
forall
x1
x2
x3
,
x
<>
p
\
/
istrue
(
!
w
))
->
F2
H
Q
)))
(
at
level
69
,
x
at
level
0
,
x1
ident
,
x2
ident
,
x3
ident
)
:
charac
.
Notation
"'Case' x '=' p [ x1 x2 x3 x4 ] 'When' w 'Then' F1 'Else'
Q
2"
:=
Notation
"'Case' x '=' p [ x1 x2 x3 x4 ] 'When' w 'Then' F1 'Else'
F
2"
:=
(
!
CaseWhen
(
fun
H
Q
=>
(
forall
x1
x2
x3
x4
,
x
=
p
->
istrue
w
%
bool
->
F1
H
Q
)
/
\
((
forall
x1
x2
x3
x4
,
x
<>
p
\
/
istrue
(
!
w
))
->
F2
H
Q
)))
(
at
level
69
,
x
at
level
0
,
x1
ident
,
x2
ident
,
x3
ident
,
x4
ident
)
:
charac
.
Notation
"'Case' x '=' p [ x1 x2 x3 x4 x5 ] 'When' w 'Then' F1 'Else'
Q
2"
:=
Notation
"'Case' x '=' p [ x1 x2 x3 x4 x5 ] 'When' w 'Then' F1 'Else'
F
2"
:=
(
!
CaseWhen
(
fun
H
Q
=>
(
forall
x1
x2
x3
x4
x5
,
x
=
p
->
istrue
w
%
bool
->
F1
H
Q
)
/
\
((
forall
x1
x2
x3
x4
x5
,
x
<>
p
\
/
istrue
(
!
w
))
->
F2
H
Q
)))
(
at
level
69
,
x
at
level
0
,
x1
ident
,
x2
ident
,
x3
ident
,
x4
ident
,
x5
ident
)
:
charac
.
Notation
"'Case' x '=' p [ x1 x2 x3 x4 x5 x6 ] 'When' w 'Then' F1 'Else'
Q
2"
:=
Notation
"'Case' x '=' p [ x1 x2 x3 x4 x5 x6 ] 'When' w 'Then' F1 'Else'
F
2"
:=
(
!
CaseWhen
(
fun
H
Q
=>
(
forall
x1
x2
x3
x4
x5
x6
,
x
=
p
->
istrue
w
%
bool
->
F1
H
Q
)
/
\
((
forall
x1
x2
x3
x4
x5
x6
,
x
<>
p
\
/
istrue
(
!
w
))
->
F2
H
Q
)))
(
at
level
69
,
x
at
level
0
,
x1
ident
,
x2
ident
,
x3
ident
,
x4
ident
,
x5
ident
,
x6
ident
)
:
charac
.
Notation
"'Case' x '=' p [ x1 x2 x3 x4 x5 x6 x7 ] 'When' w 'Then' F1 'Else'
Q
2"
:=
Notation
"'Case' x '=' p [ x1 x2 x3 x4 x5 x6 x7 ] 'When' w 'Then' F1 'Else'
F
2"
:=
(
!
CaseWhen
(
fun
H
Q
=>
(
forall
x1
x2
x3
x4
x5
x6
x7
,
x
=
p
->
istrue
w
%
bool
->
F1
H
Q
)
/
\
((
forall
x1
x2
x3
x4
x5
x6
x7
,
x
<>
p
\
/
istrue
(
!
w
))
->
F2
H
Q
)))
(
at
level
69
,
x
at
level
0
,
x1
ident
,
x2
ident
,
...
...
@@ -606,8 +606,12 @@ Notation "'TopFun' f ':=' K" :=
(
*
**
Database
of
characteristic
formulae
*
)
Definition
database_cf
:=
True
.
Notation
"'RegisterCf' T"
:=
(
Register
database_cf
T
)
(
at
level
69
).
(
*
re
-
export
this
notation
in
the
charac
scope
*
)
Notation
"'Register' D T"
:=
(
ltac_database
(
boxer
D
)
(
boxer
T
)
_
)
(
at
level
69
,
D
at
level
0
,
T
at
level
0
)
:
charac
.
Ltac
CFPrint_Provide
T
:=
Provide
T
.
(
********************************************************************
)
...
...
@@ -619,13 +623,14 @@ Notation "'RegisterCf' T" := (Register database_cf T)
or
,
if
it
involves
time
credits
,
use
:
Hint
Extern
1
(
RegisterSpecCredits
f
)
=>
Provide
f_spec
.
*
)
Definition
database_spec
:=
True
.
Notation
"'RegisterSpec' T"
:=
(
Register
database_spec
T
)
(
at
level
69
).
(
at
level
69
)
:
charac
.
Definition
database_spec_credits
:=
True
.
Notation
"'RegisterSpecCredits' T"
:=
(
Register
database_spec_credits
T
)
(
at
level
69
).
(
at
level
69
)
:
charac
.
(
**
The
focus
and
unfocus
databases
are
used
to
register
specifications
for
accessors
to
record
fields
,
combined
with
focus
/
unfocus
operations
*
)
...
...
lib/coq/Makefile
View file @
51dd8f50
...
...
@@ -36,3 +36,5 @@ all: proof
COQINCLUDE
:=
-R
$(CFML)
/lib/tlc TLC
-R
.
CFML
include
$(CFML)/lib/make/Makefile.coq
quick_cf
:
CFHeader.vio
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