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
Why3
why3
Commits
f53b752f
Commit
f53b752f
authored
Jun 27, 2015
by
Andrei Paskevich
Browse files
Parser: use "scope" instead of "namespace"
parent
a04cd4da
Changes
5
Hide whitespace changes
Inline
Side-by-side
src/core/pretty.ml
View file @
f53b752f
...
...
@@ -29,7 +29,7 @@ let debug_print_locs = Debug.register_info_flag "print_locs"
let
iprinter
,
aprinter
,
tprinter
,
pprinter
=
let
bl
=
[
"theory"
;
"type"
;
"constant"
;
"function"
;
"predicate"
;
"inductive"
;
"axiom"
;
"lemma"
;
"goal"
;
"use"
;
"clone"
;
"prop"
;
"meta"
;
"
namespac
e"
;
"import"
;
"export"
;
"end"
;
"
scop
e"
;
"import"
;
"export"
;
"end"
;
"forall"
;
"exists"
;
"not"
;
"true"
;
"false"
;
"if"
;
"then"
;
"else"
;
"let"
;
"in"
;
"match"
;
"with"
;
"as"
;
"epsilon"
]
in
let
isanitize
=
sanitizer
char_to_alpha
char_to_alnumus
in
...
...
src/parser/lexer.mll
View file @
f53b752f
...
...
@@ -46,7 +46,7 @@
"let"
,
LET
;
"match"
,
MATCH
;
"meta"
,
META
;
"
namespace"
,
NAMESPAC
E
;
"
scope"
,
SCOP
E
;
"not"
,
NOT
;
"predicate"
,
PREDICATE
;
"prop"
,
PROP
;
...
...
src/parser/parser.mly
View file @
f53b752f
...
...
@@ -103,7 +103,7 @@
%
token
AS
AXIOM
CLONE
COINDUCTIVE
CONSTANT
%
token
ELSE
END
EPSILON
EXISTS
EXPORT
FALSE
FORALL
FUNCTION
%
token
GOAL
IF
IMPORT
IN
INDUCTIVE
LEMMA
%
token
LET
MATCH
META
N
AMESPACE
NOT
PROP
PREDICAT
E
%
token
LET
MATCH
META
N
OT
PREDICATE
PROP
SCOP
E
%
token
THEN
THEORY
TRUE
TYPE
USE
WITH
(* program keywords *)
...
...
@@ -184,7 +184,7 @@ module_decl:
{
Typing
.
close_namespace
(
floc
$
startpos
(
$
1
)
$
endpos
(
$
1
))
~
import
:$
1
}
namespace_head
:
|
NAMESPAC
E
boption
(
IMPORT
)
uident
{
Typing
.
open_namespace
$
3
;
$
2
}
|
SCOP
E
boption
(
IMPORT
)
uident
{
Typing
.
open_namespace
$
3
;
$
2
}
(* Use and clone *)
...
...
@@ -202,7 +202,7 @@ use:
{
{
use_module
=
$
2
;
use_import
=
None
}
}
clone_subst
:
|
NAMESPACE
ns
EQUAL
ns
{
CSns
(
floc
$
startpos
$
endpos
,
$
2
,$
4
)
}
|
SCOPE
ns
EQUAL
ns
{
CSns
(
floc
$
startpos
$
endpos
,
$
2
,$
4
)
}
|
TYPE
qualid
ty_var
*
EQUAL
ty
{
CStsym
(
floc
$
startpos
$
endpos
,
$
2
,$
3
,$
5
)
}
|
CONSTANT
qualid
EQUAL
qualid
{
CSfsym
(
floc
$
startpos
$
endpos
,
$
2
,$
4
)
}
|
FUNCTION
qualid
EQUAL
qualid
{
CSfsym
(
floc
$
startpos
$
endpos
,
$
2
,$
4
)
}
...
...
src/printer/why3printer.ml
View file @
f53b752f
...
...
@@ -23,7 +23,7 @@ open Theory
let
iprinter
,
aprinter
,
tprinter
,
pprinter
=
let
bl
=
[
"theory"
;
"type"
;
"function"
;
"predicate"
;
"inductive"
;
"axiom"
;
"lemma"
;
"goal"
;
"use"
;
"clone"
;
"prop"
;
"meta"
;
"
namespac
e"
;
"import"
;
"export"
;
"end"
;
"
scop
e"
;
"import"
;
"export"
;
"end"
;
"forall"
;
"exists"
;
"not"
;
"true"
;
"false"
;
"if"
;
"then"
;
"else"
;
"let"
;
"in"
;
"match"
;
"with"
;
"as"
;
"epsilon"
]
in
let
isanitize
=
sanitizer
char_to_alpha
char_to_alnumus
in
...
...
src/why3doc/doc_lexer.mll
View file @
f53b752f
...
...
@@ -36,8 +36,8 @@
let
is_keyword1
=
make_table
[
"as"
;
"axiom"
;
"clone"
;
"coinductive"
;
"constant"
;
"else"
;
"end"
;
"epsilon"
;
"exists"
;
"export"
;
"false"
;
"forall"
;
"function"
;
"goal"
;
"if"
;
"import"
;
"in"
;
"inductive"
;
"lemma"
;
"let"
;
"match"
;
"meta"
;
"namespace"
;
"not"
;
"predicate"
;
"
pr
op"
;
"then"
;
"theory"
;
"true"
;
"type"
;
"use"
;
"with"
;
"lemma"
;
"let"
;
"match"
;
"meta"
;
"not"
;
"predicate"
;
"prop"
;
"
sc
op
e
"
;
"then"
;
"theory"
;
"true"
;
"type"
;
"use"
;
"with"
;
(* programs *)
"abstract"
;
"any"
;
"begin"
;
"do"
;
"done"
;
"downto"
;
"exception"
;
"for"
;
"fun"
;
"ghost"
;
"loop"
;
"model"
;
"module"
;
...
...
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