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
Raphaël Cauderlier
Sigmaid
Commits
bedb2e0d
Commit
bedb2e0d
authored
Jun 27, 2014
by
Raphaël Cauderlier
Browse files
Test file
parent
5695ed9d
Changes
7
Hide whitespace changes
Inline
Side-by-side
.gitignore
View file @
bedb2e0d
...
...
@@ -4,3 +4,4 @@
tmp.dk
_build/
sigmaid.native
test.dk
Makefile
View file @
bedb2e0d
...
...
@@ -14,9 +14,15 @@ depend: .depend
dkdep
*
.dk
>
.depend
clean
:
rm
-f
*
.dko .depend tmp.dk
rm
-f
*
.dko .depend tmp.dk
test.dk sigmaid.native
sigmaid.native
:
ocamlbuild
-use-menhir
sigmaid.native
test.dk
:
sigmaid.native
./sigmaid.native test.sigma
>
test.dk
test
:
test.dk dk_obj_examples.dko
dkcheck
-nc
-r
test.dk
-include
.depend
lexer.mll
View file @
bedb2e0d
...
...
@@ -4,8 +4,7 @@
}
rule
token
=
parse
|
[
'
'
'\t'
]
as
c
{
Format
.
eprintf
"ignore '%c'@
\n
"
c
;
token
lexbuf
}
|
[
'
'
'\t'
]
{
token
lexbuf
}
|
'\n'
{
token
lexbuf
}
|
'.'
([
'
a'
-
'
z'
]
[
'
a'
-
'
z'
'
A'
-
'
Z'
'
_'
'
0
'
-
'
9
'
]
*
as
s
)
"<="
{
UPDATE
(
s
)
}
|
'.'
([
'
a'
-
'
z'
]
[
'
a'
-
'
z'
'
A'
-
'
Z'
'
_'
'
0
'
-
'
9
'
]
*
as
s
)
{
SELECT
(
s
)
}
...
...
parsetree.mli
View file @
bedb2e0d
...
...
@@ -22,7 +22,7 @@ type term =
and
meth
=
Method
of
id
*
stype
*
term
;;
type
line
=
|
Typedef
of
cid
*
stype
|
Typedef
of
cid
*
cid
list
*
stype
|
Vardef
of
id
*
stype
*
term
|
Check
of
term
*
stype
|
Norm
of
term
...
...
printer.ml
View file @
bedb2e0d
...
...
@@ -9,14 +9,14 @@ let print_label out_fmter (Label l) = Format.fprintf out_fmter "%s" l
let
rec
print_ty
out_fmter
=
function
|
Stcid
(
c
,
_
)
->
print_cid
out_fmter
c
|
Stlist
[]
->
Format
.
fprintf
out_fmter
"@[type
_
nil@]"
Format
.
fprintf
out_fmter
"@[
dk_
type
.
nil@]"
|
Stlist
((
l
,
ty
)
::
ll
)
->
Format
.
fprintf
out_fmter
"@[type
_
cons@ (%a)@ (%a)@ (%a)@]"
Format
.
fprintf
out_fmter
"@[
dk_
type
.
cons@ (%a)@ (%a)@ (%a)@]"
print_label
l
print_ty
ty
print_ty
(
Stlist
ll
)
|
Starr
(
ty1
,
ty2
)
->
Format
.
fprintf
out_fmter
"@[
A
rrow@ (%a)@ (%a)@]"
Format
.
fprintf
out_fmter
"@[
dk_obj_examples.a
rrow@ (%a)@ (%a)@]"
print_ty
ty1
print_ty
ty2
...
...
@@ -27,13 +27,13 @@ let rec print_term out_fmter : tterm -> unit = function
Format
.
fprintf
out_fmter
"(%a)"
print_term
t
|
Tapp
(
t1
,
t2
,
ty2
,
ty
)
->
Format
.
fprintf
out_fmter
"@[App@ (%a)@ (%a)@ (%a)@ (%a)@]"
Format
.
fprintf
out_fmter
"@[
dk_obj_examples.
App@ (%a)@ (%a)@ (%a)@ (%a)@]"
print_ty
ty
print_ty
ty2
print_term
t1
print_term
t2
|
Tabst
(
x
,
ty
,
body
,
rty
)
->
Format
.
fprintf
out_fmter
"@[Lambda@ (%a)@ (%a)@ (%a :@ %a =>@ %a)@]"
Format
.
fprintf
out_fmter
"@[
dk_obj_examples.
Lambda@ (%a)@ (%a)@ (%a :@ %a =>@ %a)@]"
print_ty
ty
print_ty
rty
print_id
x
...
...
@@ -42,28 +42,28 @@ let rec print_term out_fmter : tterm -> unit = function
|
Tobj
(
ll
,
ty
)
->
print_object
ty
out_fmter
ll
|
Tsel
(
t
,
l
,
ty
)
->
Format
.
fprintf
out_fmter
"@[select@ (%a)@ (%a)@ (%a)@]"
Format
.
fprintf
out_fmter
"@[
dk_obj.
select@ (%a)@ (%a)@ (%a)@]"
print_ty
ty
print_term
t
print_label
l
|
Tupd
(
t
,
l
,
m
,
ty
)
->
Format
.
fprintf
out_fmter
"@[update@ (%a)@ (%a)@ (%a)@ (%a)@]"
Format
.
fprintf
out_fmter
"@[
dk_obj.
update@ (%a)@ (%a)@ (%a)@ (%a)@]"
print_ty
ty
print_term
t
print_label
l
print_meth
m
|
Tcast
(
t
,
ty1
,
ty2
)
->
Format
.
fprintf
out_fmter
"@[coerce@
I@
(%a)@ (%a)@ (%a)@]"
Format
.
fprintf
out_fmter
"@[
dk_obj.
coerce@ (%a)@ (%a)@
dk_logic.I@
(%a)@]"
print_ty
ty1
print_ty
ty2
print_term
t
and
print_object
ty
out_fmter
=
function
|
[]
->
Format
.
fprintf
out_fmter
"@[
pre
nil@ (%a)@ (assoc@ (%a))@]"
Format
.
fprintf
out_fmter
"@[
dk_obj.Po_
nil@ (%a)@ (
dk_type.
assoc@ (%a))@]"
print_ty
ty
print_ty
ty
|
(
l
,
m
)
::
ll
->
Format
.
fprintf
out_fmter
"@[
pre
cons@ (%a)@ (assoc@ (%a))@ (%a)@ (%a)@ (%a)@ (%a)@]"
Format
.
fprintf
out_fmter
"@[
dk_obj.Po_
cons@ (%a)@ (
dk_type.
assoc@ (%a))@ (%a)@ (%a)@ (%a)@ (%a)@]"
print_ty
ty
print_ty
ty
print_domain
ll
...
...
@@ -71,9 +71,9 @@ and print_object ty out_fmter = function
print_meth
m
(
print_object
ty
)
ll
and
print_domain
out_fmter
=
function
|
[]
->
Format
.
fprintf
out_fmter
"domain
_
nil"
|
[]
->
Format
.
fprintf
out_fmter
"
dk_
domain
.
nil"
|
(
l
,
_
)
::
ll
->
Format
.
fprintf
out_fmter
"@[domain
_
cons@ (%a)@ (%a)"
Format
.
fprintf
out_fmter
"@[
dk_
domain
.
cons@ (%a)@ (%a)"
print_label
l
print_domain
ll
and
print_meth
out_fmter
(
Tmeth
(
x
,
ty
,
body
,
rty
))
=
...
...
@@ -84,16 +84,16 @@ and print_meth out_fmter (Tmeth (x, ty, body, rty)) =
let
print_line
out_fmter
=
function
|
Ttypedef
(
cid
,
ty
)
->
Format
.
fprintf
out_fmter
"@[%a :@ type :=@ %a.@]@
\n
"
Format
.
fprintf
out_fmter
"@[%a :@
dk_type.
type :=@ %a.@]@
\n
"
print_cid
cid
print_ty
ty
|
Tvardef
(
id
,
ty
,
def
)
->
Format
.
fprintf
out_fmter
"@[%a :@
Object
(%a) :=@ %a.@]@
\n
"
Format
.
fprintf
out_fmter
"@[%a :@
dk_obj.Expr
(%a) :=@ %a.@]@
\n
"
print_id
id
print_ty
ty
print_term
def
|
Tcheck
(
t
,
ty
)
->
Format
.
fprintf
out_fmter
"@[#CHECK %a
:
@ %a.@]@
\n
"
Format
.
fprintf
out_fmter
"@[#CHECK %a
,@ dk_obj.Expr
@
(
%a
)
.@]@
\n
"
print_term
(
Tcast
(
t
,
infer
t
,
ty
))
print_ty
ty
|
Tnorm
t
->
...
...
sigmaid.ml
View file @
bedb2e0d
...
...
@@ -13,31 +13,20 @@ let rec lex_prog lb =
let
lines
=
lex_prog
lb
in
(
pos
,
line
)
::
lines
with
End_of_file
->
[]
|
e
->
let
start
=
lb
.
Lexing
.
lex_start_p
in
let
file
=
start
.
Lexing
.
pos_fname
in
let
line
=
start
.
Lexing
.
pos_lnum
in
let
cnum
=
start
.
Lexing
.
pos_cnum
-
start
.
Lexing
.
pos_bol
in
let
tok
=
Lexing
.
lexeme
lb
in
Format
.
eprintf
"File: %s, line: %d, column: %d, Parse error: unexpected token %s@
\n
@."
file
line
cnum
tok
;
raise
e
|
Parsing
.
Parse_error
->
print_pos
lb
;
[]
let
main
()
=
Arg
.
parse
[]
(
fun
file
->
let
err
=
Format
.
err_formatter
in
Format
.
fprintf
err
"Sigmaid@
\n
@."
;
let
input
=
open_in
file
in
let
lexbuf
=
Lexing
.
from_channel
input
in
let
out_fmter
=
Format
.
std_formatter
in
let
prog
=
lex_prog
lexbuf
in
Format
.
fprintf
err
"Programm lexed@
\n
."
;
let
scoped_prog
=
Scoper
.
scope
prog
in
Format
.
fprintf
err
"Programm scoped@
\n
."
;
let
typed_prog
=
Typer
.
type_check
scoped_prog
in
Format
.
fprintf
err
"Programm typed@
\n
."
;
Format
.
fprintf
out_fmter
"#NAME %s.@
\n
"
(
Filename
.
chop_extension
file
)
;
Printer
.
print
out_fmter
typed_prog
;
Format
.
fprintf
err
"Programm printed@
\n
@."
;
)
"Please provide a file name."
Format
.
fprintf
out_fmter
"
@."
)
"Please provide a file name."
let
_
=
main
()
test.sigma
0 → 100644
View file @
bedb2e0d
type A := [].
var a : A := [].
check a : [].
norm a.
type
\ No newline at end of file
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