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
b615b5df
Commit
b615b5df
authored
Feb 10, 2010
by
Jean-Christophe Filliâtre
Browse files
un debut de module Typing
parent
1512d6a0
Changes
9
Hide whitespace changes
Inline
Side-by-side
Makefile.in
View file @
b615b5df
...
...
@@ -91,7 +91,7 @@ check: $(BINARY) $(PRELUDE)
LIBCMO
=
lib/pp.cmo lib/loc.cmo
CMO
=
$(LIBCMO)
src/name.cmo src/hashcons.cmo src/term.cmo src/pretty.cmo
\
src/parser.cmo src/lexer.cmo src/main.cmo
src/parser.cmo src/lexer.cmo
src/typing.cmo
src/main.cmo
CMX
=
$(CMO:.cmo=.cmx)
bin/why.opt
:
$(CMX)
...
...
@@ -109,7 +109,7 @@ bin/top: $(CMO)
ocamlmktop
$(BFLAGS)
-o
$@
str.cma
$^
test
:
bin/why.byte
bin/why.byte src/test.why
ocamlrun
-bt
bin/why.byte src/test.why
# graphical interface
#####################
...
...
lib/loc.ml
View file @
b615b5df
...
...
@@ -35,6 +35,10 @@ type position = Lexing.position * Lexing.position
exception
Located
of
position
*
exn
let
set_file
file
lb
=
lb
.
Lexing
.
lex_curr_p
<-
{
lb
.
Lexing
.
lex_curr_p
with
Lexing
.
pos_fname
=
file
}
let
dummy_position
=
Lexing
.
dummy_pos
,
Lexing
.
dummy_pos
let
gen_report_line
fmt
(
f
,
l
,
b
,
e
)
=
...
...
lib/loc.mli
View file @
b615b5df
...
...
@@ -11,6 +11,8 @@ type position = Lexing.position * Lexing.position
exception
Located
of
position
*
exn
val
set_file
:
string
->
Lexing
.
lexbuf
->
unit
val
string
:
position
->
string
val
parse
:
string
->
position
...
...
src/lexer.mli
0 → 100644
View file @
b615b5df
type
error
exception
Lexical_error
of
error
val
report
:
Format
.
formatter
->
error
->
unit
val
parse_logic_file
:
Lexing
.
lexbuf
->
Ptree
.
logic_file
src/lexer.mll
View file @
b615b5df
{
open
Format
open
Lexing
open
Ptree
open
Parser
(* lexical errors *)
type
error
=
|
IllegalCharacter
of
char
|
UnterminatedComment
|
UnterminatedString
exception
Lexical_error
of
error
let
report
fmt
=
function
|
IllegalCharacter
c
->
fprintf
fmt
"illegal character %c"
c
|
UnterminatedComment
->
fprintf
fmt
"unterminated comment"
|
UnterminatedString
->
fprintf
fmt
"unterminated string"
let
keywords
=
Hashtbl
.
create
97
let
()
=
List
.
iter
...
...
@@ -70,8 +85,6 @@
let
string_buf
=
Buffer
.
create
1024
exception
Lexical_error
of
string
let
char_for_backslash
=
function
|
'
n'
->
'\n'
|
'
t'
->
'\t'
...
...
@@ -200,7 +213,7 @@ rule token = parse
|
eof
{
EOF
}
|
_
as
c
{
raise
(
Lexical_error
(
"i
llegal
c
haracter
: "
^
String
.
make
1
c
))
}
{
raise
(
Lexical_error
(
I
llegal
C
haracter
c
))
}
and
comment
=
parse
|
"*)"
...
...
@@ -210,7 +223,7 @@ and comment = parse
|
newline
{
newline
lexbuf
;
comment
lexbuf
}
|
eof
{
raise
(
Lexical_error
"u
nterminated
c
omment
"
)
}
{
raise
(
Lexical_error
U
nterminated
C
omment
)
}
|
_
{
comment
lexbuf
}
...
...
@@ -222,7 +235,7 @@ and string = parse
|
newline
{
newline
lexbuf
;
Buffer
.
add_char
string_buf
'\n'
;
string
lexbuf
}
|
eof
{
raise
(
Lexical_error
"u
nterminated
s
tring
"
)
}
{
raise
(
Lexical_error
U
nterminated
S
tring
)
}
|
_
as
c
{
Buffer
.
add_char
string_buf
c
;
string
lexbuf
}
...
...
src/main.ml
View file @
b615b5df
...
...
@@ -18,19 +18,26 @@ open Format
let
file
=
Sys
.
argv
.
(
1
)
let
rec
report
fmt
=
function
|
Lexer
.
Lexical_error
e
->
fprintf
fmt
"lexical error: %a"
Lexer
.
report
e
;
|
Loc
.
Located
(
loc
,
e
)
->
fprintf
fmt
"%a%a"
Loc
.
report_position
loc
report
e
|
Parsing
.
Parse_error
->
fprintf
fmt
"syntax error"
|
e
->
fprintf
fmt
"anomaly: %s"
(
Printexc
.
to_string
e
)
let
()
=
try
let
c
=
open_in
file
in
let
lb
=
Lexing
.
from_channel
c
in
lb
.
Lexing
.
lex_curr_p
<-
{
lb
.
Lexing
.
lex_curr_p
with
Lexing
.
pos_fname
=
file
};
Loc
.
set_file
file
lb
;
let
_f
=
Lexer
.
parse_logic_file
lb
in
close_in
c
with
|
Lexer
.
Lexical_error
s
->
eprintf
"lexical error: %s@."
s
;
exit
1
|
Loc
.
Located
(
loc
,
Parsing
.
Parse_error
)
->
eprintf
"%asyntax error@."
Loc
.
report_position
loc
;
exit
1
with
e
->
eprintf
"%a@."
report
e
;
exit
1
(****
...
...
src/test.why
View file @
b615b5df
(* test file *)
type 'a list
type 'a list
logic nil : 'a list
logic cons : 'a, 'a list -> 'a list
...
...
src/typing.ml
0 → 100644
View file @
b615b5df
open
Term
module
M
=
Map
.
Make
(
String
)
type
env
=
{
tysymbols
:
tysymbol
M
.
t
;
fsymbols
:
fsymbol
M
.
t
;
psymbols
:
psymbol
M
.
t
;
tyvars
:
vsymbol
M
.
t
;
vars
:
vsymbol
M
.
t
;
}
let
empty
=
{
tysymbols
=
M
.
empty
;
fsymbols
=
M
.
empty
;
psymbols
=
M
.
empty
;
tyvars
=
M
.
empty
;
vars
=
M
.
empty
;
}
src/typing.mli
0 → 100644
View file @
b615b5df
open
Term
(** typing environments *)
type
env
val
empty
:
env
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