Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
ed7582c5
Commit
ed7582c5
authored
Mar 18, 2010
by
Andrei Paskevich
Browse files
a bit of renaming around prsymbols and props
parent
259be340
Changes
10
Hide whitespace changes
Inline
Side-by-side
src/core/decl.ml
View file @
ed7582c5
...
...
@@ -82,12 +82,12 @@ let ls_defn_axiom (_,_,_,f) = f
(** Inductive predicate declaration *)
type
pr
op
=
{
type
pr
symbol
=
{
pr_name
:
ident
;
}
module
Prop
=
struct
type
t
=
pr
op
type
t
=
pr
symbol
let
equal
=
(
==
)
let
hash
pr
=
pr
.
pr_name
.
id_tag
let
compare
pr1
pr2
=
...
...
@@ -97,11 +97,11 @@ module Spr = Set.Make(Prop)
module
Mpr
=
Map
.
Make
(
Prop
)
module
Hpr
=
Hashtbl
.
Make
(
Prop
)
let
create_pr
op
n
=
{
pr_name
=
id_register
n
}
let
create_pr
symbol
n
=
{
pr_name
=
id_register
n
}
type
prop
_fmla
=
prop
*
fmla
type
prop
=
prsymbol
*
fmla
type
ind_decl
=
lsymbol
*
prop
_fmla
list
type
ind_decl
=
lsymbol
*
prop
list
(** Proposition declaration *)
...
...
@@ -110,7 +110,7 @@ type prop_kind =
|
Plemma
|
Pgoal
type
prop_decl
=
prop_kind
*
pr
op
*
fmla
type
prop_decl
=
prop_kind
*
pr
symbol
*
fmla
(** Declaration type *)
...
...
@@ -246,9 +246,9 @@ let create_logic_decl ldl =
ignore
(
List
.
fold_left
check_decl
Sid
.
empty
ldl
);
create_logic_decl
ldl
exception
InvalidIndDecl
of
lsymbol
*
pr
op
exception
TooSpecificIndDecl
of
lsymbol
*
pr
op
*
term
exception
NonPositiveIndDecl
of
lsymbol
*
pr
op
*
lsymbol
exception
InvalidIndDecl
of
lsymbol
*
pr
symbol
exception
TooSpecificIndDecl
of
lsymbol
*
pr
symbol
*
term
exception
NonPositiveIndDecl
of
lsymbol
*
pr
symbol
*
lsymbol
exception
Found
of
lsymbol
let
ls_mem
s
sps
=
if
Sls
.
mem
s
sps
then
raise
(
Found
s
)
else
false
...
...
src/core/decl.mli
View file @
ed7582c5
...
...
@@ -47,19 +47,19 @@ val ls_defn_axiom : ls_defn -> fmla
(** Inductive predicate declaration *)
type
pr
op
=
private
{
type
pr
symbol
=
private
{
pr_name
:
ident
;
}
module
Spr
:
Set
.
S
with
type
elt
=
pr
op
module
Mpr
:
Map
.
S
with
type
key
=
pr
op
module
Hpr
:
Hashtbl
.
S
with
type
key
=
pr
op
module
Spr
:
Set
.
S
with
type
elt
=
pr
symbol
module
Mpr
:
Map
.
S
with
type
key
=
pr
symbol
module
Hpr
:
Hashtbl
.
S
with
type
key
=
pr
symbol
val
create_pr
op
:
preid
->
pr
op
val
create_pr
symbol
:
preid
->
pr
symbol
type
prop
_fmla
=
prop
*
fmla
type
prop
=
prsymbol
*
fmla
type
ind_decl
=
lsymbol
*
prop
_fmla
list
type
ind_decl
=
lsymbol
*
prop
list
(* Proposition declaration *)
...
...
@@ -68,7 +68,7 @@ type prop_kind =
|
Plemma
|
Pgoal
type
prop_decl
=
prop_kind
*
pr
op
*
fmla
type
prop_decl
=
prop_kind
*
pr
symbol
*
fmla
(** Declaration type *)
...
...
@@ -88,7 +88,7 @@ and decl_node =
val
create_ty_decl
:
ty_decl
list
->
decl
val
create_logic_decl
:
logic_decl
list
->
decl
val
create_ind_decl
:
ind_decl
list
->
decl
val
create_prop_decl
:
prop_kind
->
pr
op
->
fmla
->
decl
val
create_prop_decl
:
prop_kind
->
pr
symbol
->
fmla
->
decl
(* separate independent groups of declarations *)
...
...
@@ -102,9 +102,9 @@ exception ConstructorExpected of lsymbol
exception
IllegalTypeAlias
of
tysymbol
exception
UnboundTypeVar
of
tvsymbol
exception
InvalidIndDecl
of
lsymbol
*
pr
op
exception
TooSpecificIndDecl
of
lsymbol
*
pr
op
*
term
exception
NonPositiveIndDecl
of
lsymbol
*
pr
op
*
lsymbol
exception
InvalidIndDecl
of
lsymbol
*
pr
symbol
exception
TooSpecificIndDecl
of
lsymbol
*
pr
symbol
*
term
exception
NonPositiveIndDecl
of
lsymbol
*
pr
symbol
*
lsymbol
exception
IllegalConstructor
of
lsymbol
exception
BadLogicDecl
of
ident
...
...
src/core/pretty.mli
View file @
ed7582c5
...
...
@@ -34,7 +34,7 @@ val print_vs : formatter -> vsymbol -> unit (* variable *)
val
print_ts
:
formatter
->
tysymbol
->
unit
(* type symbol *)
val
print_ls
:
formatter
->
lsymbol
->
unit
(* logic symbol *)
val
print_pr
:
formatter
->
pr
op
->
unit
(* proposition name *)
val
print_pr
:
formatter
->
pr
symbol
->
unit
(* proposition name *)
val
print_ty
:
formatter
->
ty
->
unit
(* type *)
val
print_vsty
:
formatter
->
vsymbol
->
unit
(* variable : type *)
...
...
src/core/task.mli
View file @
ed7582c5
...
...
@@ -57,7 +57,7 @@ val task_iter : (decl -> unit) -> task -> unit
val
task_decls
:
task
->
decl
list
val
task_goal
:
task
->
pr
op
val
task_goal
:
task
->
pr
symbol
(* exceptions *)
...
...
src/core/theory.ml
View file @
ed7582c5
...
...
@@ -32,7 +32,7 @@ module Mnm = Mstr
type
namespace
=
{
ns_ts
:
tysymbol
Mnm
.
t
;
(* type symbols *)
ns_ls
:
lsymbol
Mnm
.
t
;
(* logic symbols *)
ns_pr
:
prop
_fmla
Mnm
.
t
;
(* propositions *)
ns_pr
:
prop
Mnm
.
t
;
(* propositions *)
ns_ns
:
namespace
Mnm
.
t
;
(* inner namespaces *)
}
...
...
@@ -70,10 +70,10 @@ let rec ns_find get_map ns = function
let
ns_find_ts
=
ns_find
(
fun
ns
->
ns
.
ns_ts
)
let
ns_find_ls
=
ns_find
(
fun
ns
->
ns
.
ns_ls
)
let
ns_find_pr
=
ns_find
(
fun
ns
->
ns
.
ns_pr
)
let
ns_find_prop
ns
sl
=
fst
(
ns_find_pr
ns
sl
)
let
ns_find_fmla
ns
sl
=
snd
(
ns_find_pr
ns
sl
)
let
ns_find_prop
=
ns_find
(
fun
ns
->
ns
.
ns_pr
)
let
ns_find_pr
ns
sl
=
fst
(
ns_find_prop
ns
sl
)
let
ns_find_fmla
ns
sl
=
snd
(
ns_find_prop
ns
sl
)
(** Theory *)
...
...
@@ -249,7 +249,7 @@ exception CannotInstantiate of ident
type
clones
=
{
ts_table
:
tysymbol
Hts
.
t
;
ls_table
:
lsymbol
Hls
.
t
;
pr_table
:
prop
_fmla
Hpr
.
t
;
pr_table
:
prop
Hpr
.
t
;
id_table
:
ident
Hid
.
t
;
nw_local
:
unit
Hid
.
t
;
id_local
:
Sid
.
t
;
...
...
@@ -298,7 +298,7 @@ let cl_find_ls cl ls =
let
cl_trans_fmla
cl
f
=
f_s_map
(
cl_find_ts
cl
)
(
cl_find_ls
cl
)
f
let
cl_trans_prop
cl
(
pr
,
f
)
=
let
pr'
=
create_pr
op
(
id_dup
pr
.
pr_name
)
in
let
pr'
=
create_pr
symbol
(
id_dup
pr
.
pr_name
)
in
let
f'
=
cl_trans_fmla
cl
f
in
Hid
.
add
cl
.
id_table
pr
.
pr_name
pr'
.
pr_name
;
Hpr
.
add
cl
.
pr_table
pr
(
pr'
,
f'
);
...
...
src/core/theory.mli
View file @
ed7582c5
...
...
@@ -30,13 +30,13 @@ module Mnm : Map.S with type key = string
type
namespace
=
private
{
ns_ts
:
tysymbol
Mnm
.
t
;
(* type symbols *)
ns_ls
:
lsymbol
Mnm
.
t
;
(* logic symbols *)
ns_pr
:
prop
_fmla
Mnm
.
t
;
(* propositions *)
ns_pr
:
prop
Mnm
.
t
;
(* propositions *)
ns_ns
:
namespace
Mnm
.
t
;
(* inner namespaces *)
}
val
ns_find_ts
:
namespace
->
string
list
->
tysymbol
val
ns_find_ls
:
namespace
->
string
list
->
lsymbol
val
ns_find_pr
:
namespace
->
string
list
->
pr
op_fmla
val
ns_find_pr
:
namespace
->
string
list
->
pr
symbol
val
ns_find_prop
:
namespace
->
string
list
->
prop
val
ns_find_fmla
:
namespace
->
string
list
->
fmla
...
...
src/driver/driver.ml
View file @
ed7582c5
...
...
@@ -231,7 +231,7 @@ let load_rules env clone driver {thr_name = loc,qualid; thr_rules = trl} =
begin
try
add_htheory
c
(
ns_find_pr
op
th
.
th_export
q
)
.
pr_name
Remove
(
ns_find_pr
th
.
th_export
q
)
.
pr_name
Remove
with
Not_found
->
errorm
~
loc
"Unknown axioms %s"
(
string_of_qualid
qualid
q
)
end
...
...
@@ -272,7 +272,7 @@ let load_rules env clone driver {thr_name = loc,qualid; thr_rules = trl} =
|
Rtagpr
(
c
,
(
loc
,
q
)
,
s
)
->
begin
try
add_htheory
c
(
ns_find_pr
op
th
.
th_export
q
)
.
pr_name
add_htheory
c
(
ns_find_pr
th
.
th_export
q
)
.
pr_name
(
Tag
(
Sstr
.
singleton
s
))
with
Not_found
->
errorm
~
loc
"Unknown proposition %s"
(
string_of_qualid
qualid
q
)
...
...
src/main.ml
View file @
ed7582c5
...
...
@@ -201,7 +201,7 @@ let do_file env drv filename_printer file =
|
Some
s
->
Some
(
Hashtbl
.
fold
(
fun
s
l
acc
->
let
pr
=
try
fst
(
ns_find_pr
th
.
th_export
l
)
with
Not_found
->
let
pr
=
try
ns_find_pr
th
.
th_export
l
with
Not_found
->
eprintf
"File %s : --goal : Unknown goal %s@."
file
s
;
exit
1
in
Decl
.
Spr
.
add
pr
acc
)
s
Decl
.
Spr
.
empty
)
in
...
...
src/parser/typing.ml
View file @
ed7582c5
...
...
@@ -911,7 +911,7 @@ let fmla env f =
let
add_prop
k
loc
s
f
th
=
let
f
=
fmla
th
f
in
try
add_decl
th
(
create_prop_decl
k
(
create_pr
op
(
id_user
s
.
id
loc
))
f
)
add_decl
th
(
create_prop_decl
k
(
create_pr
symbol
(
id_user
s
.
id
loc
))
f
)
with
ClashSymbol
_
->
error
~
loc
(
Clash
s
.
id
)
...
...
@@ -1010,7 +1010,7 @@ let add_inductives dl th =
let
id
=
d
.
in_ident
.
id
in
let
ps
=
Hashtbl
.
find
psymbols
id
in
let
clause
(
loc
,
id
,
f
)
=
create_pr
op
(
id_user
id
.
id
loc
)
,
fmla
th'
f
create_pr
symbol
(
id_user
id
.
id
loc
)
,
fmla
th'
f
in
ps
,
List
.
map
clause
d
.
in_def
in
...
...
src/transform/split_conjunction.ml
View file @
ed7582c5
...
...
@@ -85,7 +85,7 @@ let elt split_pos d =
|
Dprop
(
Pgoal
,
pr
,
f
)
->
let
l
=
split_pos
[]
f
in
List
.
map
(
fun
p
->
[
create_prop_decl
Pgoal
(
create_pr
op
(
id_clone
pr
.
pr_name
))
p
])
l
(
create_pr
symbol
(
id_clone
pr
.
pr_name
))
p
])
l
|
_
->
[[
d
]]
let
t
fsp
=
Register
.
store
(
fun
()
->
Trans
.
decl_l
(
elt
fsp
)
None
)
...
...
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