Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
CHARGUERAUD Arthur
cfml
Commits
755a3f1c
Commit
755a3f1c
authored
Jan 07, 2016
by
POTTIER Francois
Browse files
Cleanup.
parent
6af442ec
Changes
1
Hide whitespace changes
Inline
Side-by-side
generator/print_coq.ml
View file @
755a3f1c
...
...
@@ -21,25 +21,16 @@ let width =
(* Various fixed elements. *)
let
arrow
=
string
"
->"
string
"->"
let
doublearrow
=
string
"=>"
let
colon
=
string
" :"
let
colonequals
=
string
" :="
let
within
=
string
"in"
string
":="
let
quote
=
string
"'"
let
dot
=
string
"."
let
spacecolon
=
string
" :"
(* -------------------------------------------------------------------------- *)
...
...
@@ -116,7 +107,7 @@ let label = function
string
"_"
|
Some
l
->
parens
(
string
"Label_create"
^/^
quote
^^
string
l
string
"Label_create"
^/^
s
quote
^^
string
l
)
(* -------------------------------------------------------------------------- *)
...
...
@@ -141,7 +132,7 @@ let rec expr0 = function
|
Coq_record
_les
->
assert
false
(* TODO *)
|
Coq_annot
(
e1
,
e2
)
->
parens
(
expr
e1
^^
colon
^/^
expr
e2
)
parens
(
expr
e1
^^
space
colon
^/^
expr
e2
)
|
Coq_app
_
|
Coq_tag
_
|
Coq_impl
_
...
...
@@ -167,28 +158,28 @@ and expr1 = function
and
expr2
=
function
|
Coq_impl
(
e1
,
e2
)
->
group
(
expr1
e1
^^
arrow
^/^
expr2
e2
)
group
(
expr1
e1
^^
space
^^
arrow
^/^
expr2
e2
)
|
e
->
expr1
e
and
expr3
=
function
|
Coq_lettuple
(
es
,
e1
,
e2
)
->
block
(
string
"let '"
^^
tuple
expr
es
^^
colonequals
)
(
string
"let '"
^^
tuple
expr
es
^^
space
^^
colonequals
)
(
break
1
^^
expr
e1
)
(
break
1
^^
with
in
)
(
break
1
^^
string
"
in
"
)
^/^
expr3
e2
|
Coq_forall
((
x
,
e1
)
,
e2
)
->
block
(
string
"forall "
^^
string
x
^^
colon
)
(
string
"forall "
^^
string
x
^^
space
colon
)
(
break
1
^^
expr
e1
^^
comma
)
empty
^/^
expr3
e2
|
Coq_fun
((
x
,
e1
)
,
e2
)
->
block
(
string
"fun "
^^
string
x
^^
colon
)
(
string
"fun "
^^
string
x
^^
space
colon
)
(
break
1
^^
expr
e1
)
(
break
1
^^
doublearrow
)
^/^
...
...
@@ -206,7 +197,7 @@ and expr e =
(* Raw. *)
let
var
(
x
,
t
)
=
block
(
string
x
^^
colon
)
(
space
^^
expr
t
)
empty
block
(
string
x
^^
space
colon
)
(
space
^^
expr
t
)
empty
(* With parentheses and with a leading space. *)
...
...
@@ -230,16 +221,16 @@ let fields xts =
let
definition
x
d1
=
block
(
space
^^
x
^^
colon
)
(
space
^^
x
^^
space
colon
)
(
break
1
^^
d1
)
(
break
1
^^
string
":="
)
(
break
1
^^
colonequals
)
(* A parameter, without a leading keyword, but with a leading space.
[ x : d1.]. *)
let
parameter
x
d1
=
block
(
space
^^
x
^^
colon
)
(
space
^^
x
^^
space
colon
)
(
break
1
^^
d1
)
dot
...
...
@@ -318,13 +309,13 @@ let top = function
|
Coqtop_hint_constructors
(
xs
,
base
)
->
string
"Hint Constructors "
^^
separate_map
space
string
xs
^^
colon
^/^
space
colon
^/^
string
base
^^
dot
|
Coqtop_hint_unfold
(
xs
,
base
)
->
string
"Hint Unfold "
^^
separate_map
space
string
xs
^^
colon
^/^
space
colon
^/^
string
base
^^
dot
|
Coqtop_require
x
->
...
...
Write
Preview
Supports
Markdown
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