Skip to content
GitLab
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
e4e484d3
Commit
e4e484d3
authored
Apr 19, 2010
by
Andrei Paskevich
Browse files
remove src/orm and move the test files to tests/
parent
d1a5ec78
Changes
8
Expand all
Hide whitespace changes
Inline
Side-by-side
src/orm/convert.ml
deleted
100644 → 0
View file @
d1a5ec78
open
Printf
let
_
=
let
fin
=
open_in
Sys
.
argv
.
(
1
)
in
let
fout
=
open_out
Sys
.
argv
.
(
2
)
in
fprintf
fout
"(* autogenerated from convert.ml and sql_access.ml *)
\n
"
;
fprintf
fout
"open Printer_utils
\n
"
;
fprintf
fout
"let print_header e =
\n
"
;
(
try
while
true
do
let
l
=
input_line
fin
in
fprintf
fout
" e.p
\"
%s
\"
;
\n
"
(
String
.
escaped
l
);
done
with
End_of_file
->
()
);
fprintf
fout
" ()"
;
close_out
fout
;
close_in
fin
src/orm/printer_utils.ml
deleted
100644 → 0
View file @
d1a5ec78
(*
* Copyright (c) 2009 Anil Madhavapeddy <anil@recoil.org>
*
* Permission to use, copy, modify, and distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
* copyright notice and this permission notice appear in all copies.
*
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
* ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
* WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
* ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
* OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
*)
open
Printf
type
env
=
{
fn
:
int
->
string
->
unit
;
p
:
string
->
unit
;
(* printer function *)
i
:
int
;
(* indent level *)
nl
:
unit
->
unit
;
(* new line *)
dbg
:
bool
;
}
let
indent
e
=
{
e
with
i
=
succ
e
.
i
;
p
=
e
.
fn
(
succ
e
.
i
)
}
let
indent_fn
e
fn
=
let
e
=
indent
e
in
fn
e
let
list_iter_indent
e
fn
l
=
List
.
iter
(
indent_fn
e
fn
)
l
let
hashtbl_iter_indent
e
fn
h
=
Hashtbl
.
iter
(
indent_fn
e
fn
)
h
let
may
fn
=
function
|
None
->
()
|
Some
x
->
fn
x
let
must
fn
=
function
|
None
->
failwith
"must"
|
Some
x
->
fn
x
let
init_printer
?
(
msg
=
None
)
?
(
debug
=
false
)
fout
=
let
ind
i
s
=
String
.
make
(
i
*
2
)
'
'
^
s
in
let
out
i
s
=
output_string
fout
((
ind
i
s
)
^
"
\n
"
)
in
may
(
out
0
)
msg
;
{
fn
=
out
;
i
=
0
;
p
=
(
out
0
);
nl
=
(
fun
(
x
:
unit
)
->
out
0
""
);
dbg
=
debug
;
}
let
print_module
e
n
fn
=
e
.
p
(
sprintf
"module %s = struct"
(
String
.
capitalize
n
));
indent_fn
e
fn
;
e
.
p
"end"
;
e
.
nl
()
let
print_module_sig
e
n
fn
=
e
.
p
(
sprintf
"module %s : sig"
(
String
.
capitalize
n
));
indent_fn
e
fn
;
e
.
p
"end"
let
print_record
e
nm
fn
=
e
.
p
(
sprintf
"type %s = {"
nm
);
indent_fn
e
fn
;
e
.
p
"}"
;
e
.
nl
()
let
print_object
e
nm
fn
=
e
.
p
(
sprintf
"type %s = <"
nm
);
indent_fn
e
fn
;
e
.
p
">"
;
e
.
nl
()
let
print_comment
e
fmt
=
let
xfn
s
=
e
.
p
(
"(* "
^
s
^
" *)"
)
in
kprintf
xfn
fmt
let
print_ocamldoc
e
?
(
raises
=
""
)
?
(
args
=
""
)
body
=
e
.
p
(
sprintf
"(** %s%s"
(
match
args
with
""
->
""
|
x
->
sprintf
"[%s] "
x
)
body
);
(
match
raises
with
""
->
()
|
r
->
e
.
p
(
" @raise "
^
r
));
e
.
p
" *)"
let
pfn
e
fmt
=
let
xfn
s
=
e
.
p
s
in
kprintf
xfn
fmt
let
dbg
e
fmt
=
let
xfn
s
=
if
e
.
dbg
then
pfn
e
"print_endline (%s);"
s
in
kprintf
xfn
fmt
let
(
--*
)
=
print_comment
let
(
-->
)
e
fn
=
indent_fn
e
fn
let
(
+=
)
=
pfn
let
(
-=
)
=
dbg
let
(
$
)
f
x
=
f
x
src/orm/sql_access.ml
deleted
100644 → 0
View file @
d1a5ec78
(*
* Copyright (c) 2009 Anil Madhavapeddy <anil@recoil.org>
*
* Permission to use, copy, modify, and distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
* copyright notice and this permission notice appear in all copies.
*
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
* ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
* WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
* ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
* OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
*)
open
Sqlite3
open
Printf
type
transaction_mode
=
[
|
`Deferred
|
`Immediate
|
`Exclusive
]
type
state
=
{
db
:
db
;
mutable
in_transaction
:
int
;
busyfn
:
db
->
unit
;
mode
:
transaction_mode
;
}
let
default_busyfn
(
db
:
Sqlite3
.
db
)
=
print_endline
"WARNING: busy"
;
Thread
.
delay
(
Random
.
float
1
.
)
let
raise_sql_error
x
=
raise
(
Sqlite3
.
Error
(
Rc
.
to_string
x
))
let
try_finally
fn
finalfn
=
try
let
r
=
fn
()
in
finalfn
()
;
r
with
e
->
begin
print_endline
(
sprintf
"WARNING: exception: %s"
(
Printexc
.
to_string
e
));
finalfn
()
;
raise
e
end
(* retry until a non-BUSY error code is returned *)
let
rec
db_busy_retry
db
fn
=
match
fn
()
with
|
Rc
.
BUSY
->
db
.
busyfn
db
.
db
;
db_busy_retry
db
fn
;
|
x
->
x
(* make sure an OK is returned from the database *)
let
db_must_ok
db
fn
=
match
db_busy_retry
db
fn
with
|
Rc
.
OK
->
()
|
x
->
raise_sql_error
x
(* make sure a DONE is returned from the database *)
let
db_must_done
db
fn
=
match
db_busy_retry
db
fn
with
|
Rc
.
DONE
->
()
|
x
->
raise_sql_error
x
(* request a transaction *)
let
transaction
db
fn
=
let
m
=
match
db
.
mode
with
|
`Deferred
->
"DEFERRED"
|
`Immediate
->
"IMMEDIATE"
|
`Exclusive
->
"EXCLUSIVE"
in
try_finally
(
fun
()
->
if
db
.
in_transaction
=
0
then
(
db_must_ok
db
(
fun
()
->
exec
db
.
db
(
sprintf
"BEGIN %s TRANSACTION"
m
));
);
db
.
in_transaction
<-
db
.
in_transaction
+
1
;
fn
()
;
)
(
fun
()
->
if
db
.
in_transaction
=
1
then
(
db_must_ok
db
(
fun
()
->
exec
db
.
db
"END TRANSACTION"
);
);
db
.
in_transaction
<-
db
.
in_transaction
-
1
)
(* iterate over a result set *)
let
step_fold
db
stmt
iterfn
=
let
stepfn
()
=
Sqlite3
.
step
stmt
in
let
rec
fn
a
=
match
db_busy_retry
db
stepfn
with
|
Sqlite3
.
Rc
.
ROW
->
fn
(
iterfn
stmt
::
a
)
|
Sqlite3
.
Rc
.
DONE
->
a
|
x
->
raise_sql_error
x
in
fn
[]
src/orm/sql_orm.ml
deleted
100644 → 0
View file @
d1a5ec78
This diff is collapsed.
Click to expand it.
src/orm/sql_orm_header.ml
deleted
100644 → 0
View file @
d1a5ec78
(* autogenerated from convert.ml and sql_access.ml *)
open
Printer_utils
let
print_header
e
=
e
.
p
"(*"
;
e
.
p
" * Copyright (c) 2009 Anil Madhavapeddy <anil@recoil.org>"
;
e
.
p
" *"
;
e
.
p
" * Permission to use, copy, modify, and distribute this software for any"
;
e
.
p
" * purpose with or without fee is hereby granted, provided that the above"
;
e
.
p
" * copyright notice and this permission notice appear in all copies."
;
e
.
p
" *"
;
e
.
p
" * THE SOFTWARE IS PROVIDED
\"
AS IS
\"
AND THE AUTHOR DISCLAIMS ALL WARRANTIES"
;
e
.
p
" * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF"
;
e
.
p
" * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR"
;
e
.
p
" * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES"
;
e
.
p
" * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN"
;
e
.
p
" * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF"
;
e
.
p
" * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE."
;
e
.
p
" *)"
;
e
.
p
""
;
e
.
p
"open Sqlite3"
;
e
.
p
"open Printf"
;
e
.
p
""
;
e
.
p
"type transaction_mode = ["
;
e
.
p
" |`Deferred"
;
e
.
p
" |`Immediate"
;
e
.
p
" |`Exclusive"
;
e
.
p
"]"
;
e
.
p
""
;
e
.
p
"type state = {"
;
e
.
p
" db : db;"
;
e
.
p
" mutable in_transaction: int;"
;
e
.
p
" busyfn: db -> unit;"
;
e
.
p
" mode: transaction_mode;"
;
e
.
p
"}"
;
e
.
p
""
;
e
.
p
"let default_busyfn (db:Sqlite3.db) ="
;
e
.
p
" print_endline
\"
WARNING: busy
\"
;"
;
e
.
p
" Thread.delay (Random.float 1.)"
;
e
.
p
""
;
e
.
p
"let raise_sql_error x ="
;
e
.
p
" raise (Sqlite3.Error (Rc.to_string x))"
;
e
.
p
""
;
e
.
p
"let try_finally fn finalfn ="
;
e
.
p
" try"
;
e
.
p
" let r = fn () in"
;
e
.
p
" finalfn ();"
;
e
.
p
" r"
;
e
.
p
" with e -> begin"
;
e
.
p
" print_endline (sprintf
\"
WARNING: exception: %s
\"
(Printexc.to_string e));"
;
e
.
p
" finalfn ();"
;
e
.
p
" raise e"
;
e
.
p
" end"
;
e
.
p
""
;
e
.
p
"(* retry until a non-BUSY error code is returned *)"
;
e
.
p
"let rec db_busy_retry db fn ="
;
e
.
p
" match fn () with"
;
e
.
p
" |Rc.BUSY -> "
;
e
.
p
" db.busyfn db.db;"
;
e
.
p
" db_busy_retry db fn;"
;
e
.
p
" |x -> x"
;
e
.
p
""
;
e
.
p
"(* make sure an OK is returned from the database *)"
;
e
.
p
"let db_must_ok db fn ="
;
e
.
p
" match db_busy_retry db fn with"
;
e
.
p
" |Rc.OK -> ()"
;
e
.
p
" |x -> raise_sql_error x"
;
e
.
p
""
;
e
.
p
"(* make sure a DONE is returned from the database *)"
;
e
.
p
"let db_must_done db fn = "
;
e
.
p
" match db_busy_retry db fn with"
;
e
.
p
" |Rc.DONE -> ()"
;
e
.
p
" |x -> raise_sql_error x"
;
e
.
p
""
;
e
.
p
"(* request a transaction *)"
;
e
.
p
"let transaction db fn ="
;
e
.
p
" let m = match db.mode with"
;
e
.
p
" |`Deferred ->
\"
DEFERRED
\"
|`Immediate ->
\"
IMMEDIATE
\"
|`Exclusive ->
\"
EXCLUSIVE
\"
in"
;
e
.
p
" try_finally (fun () ->"
;
e
.
p
" if db.in_transaction = 0 then ("
;
e
.
p
" db_must_ok db (fun () -> exec db.db (sprintf
\"
BEGIN %s TRANSACTION
\"
m));"
;
e
.
p
" );"
;
e
.
p
" db.in_transaction <- db.in_transaction + 1;"
;
e
.
p
" fn ();"
;
e
.
p
" ) (fun () ->"
;
e
.
p
" if db.in_transaction = 1 then ("
;
e
.
p
" db_must_ok db (fun () -> exec db.db
\"
END TRANSACTION
\"
);"
;
e
.
p
" );"
;
e
.
p
" db.in_transaction <- db.in_transaction - 1"
;
e
.
p
" )"
;
e
.
p
""
;
e
.
p
"(* iterate over a result set *)"
;
e
.
p
"let step_fold db stmt iterfn ="
;
e
.
p
" let stepfn () = Sqlite3.step stmt in"
;
e
.
p
" let rec fn a = match db_busy_retry db stepfn with"
;
e
.
p
" |Sqlite3.Rc.ROW -> fn (iterfn stmt :: a)"
;
e
.
p
" |Sqlite3.Rc.DONE -> a"
;
e
.
p
" |x -> raise_sql_error x"
;
e
.
p
" in"
;
e
.
p
" fn []"
;
()
\ No newline at end of file
test.why
→
test
s/test-claude
.why
View file @
e4e484d3
File moved
src
/test.why
→
tests
/test
-jcf
.why
View file @
e4e484d3
File moved
src/programs/test
.mlw
→
tests/test-pgm-jcf
.mlw
View file @
e4e484d3
File moved
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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