Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
119
Issues
119
List
Boards
Labels
Service Desk
Milestones
Merge Requests
16
Merge Requests
16
Operations
Operations
Incidents
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
33e453cd
Commit
33e453cd
authored
Mar 09, 2010
by
Jean-Christophe Filliâtre
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
nettoyagae interface Transform
parent
87a0b0f9
Changes
4
Hide whitespace changes
Inline
Side-by-side
Showing
4 changed files
with
9 additions
and
11 deletions
+9
-11
src/core/transform.ml
src/core/transform.ml
+3
-3
src/core/transform.mli
src/core/transform.mli
+4
-6
src/main.ml
src/main.ml
+1
-1
src/transform/inlining.ml
src/transform/inlining.ml
+1
-1
No files found.
src/core/transform.ml
View file @
33e453cd
...
...
@@ -82,11 +82,11 @@ let fold ?clear f_fold v_empty =
let
fold_map
?
clear
f_fold
v_empty
=
let
v_empty
=
v_empty
,
init_context
in
let
f_fold
ctxt
(
env
,
ctxt2
)
=
f_fold
ctxt
ctxt2
env
in
let
f_fold
ctxt
env_ctxt2
=
f_fold
ctxt
env_ctxt2
in
conv_res
(
fold
?
clear
f_fold
v_empty
)
snd
let
map
?
clear
f_map
=
fold_map
?
clear
(
fun
ctxt1
ctxt2
()
->
()
,
f_map
ctxt1
ctxt2
)
()
fold_map
?
clear
(
fun
ctxt1
ctxt2
->
()
,
f_map
ctxt1
(
snd
ctxt2
)
)
()
let
map_concat
?
clear
f_elt
=
let
f_elt
ctxt0
ctxt
=
...
...
@@ -126,7 +126,7 @@ let fold_context_of_decl f ctxt env ctxt_done d =
let
env
,
decls
=
f
ctxt
env
d
in
env
,
List
.
fold_left
add_decl
ctxt_done
decls
let
split_goals
=
let
split_goals
()
=
let
f
ctxt0
(
ctxt
,
l
)
=
let
decl
=
ctxt0
.
ctxt_decl
in
match
decl
.
d_node
with
...
...
src/core/transform.mli
View file @
33e453cd
...
...
@@ -52,7 +52,7 @@ val fold :
val
fold_map
:
?
clear
:
(
unit
->
unit
)
->
(
context
->
context
->
'
a
->
(
'
a
*
context
)
)
->
'
a
->
(
context
->
'
a
*
context
->
'
a
*
context
)
->
'
a
->
context
t
val
map
:
...
...
@@ -80,6 +80,7 @@ val elt :
| Ouse of theory
| Oclone of (ident * ident) list
*)
(*
val elt_of_oelt :
ty:(ty_decl -> ty_decl) ->
logic:(logic_decl -> logic_decl) ->
...
...
@@ -89,16 +90,13 @@ val elt_of_oelt :
clone:(theory -> (ident * ident) list -> decl list) ->
(decl -> decl list)
val fold_context_of_decl:
(context -> 'a -> decl -> 'a * decl list) ->
context -> 'a -> context -> decl -> ('a * context)
*)
(* Utils *)
val
unit_tag
:
unit
->
int
val
split_goals
:
context
list
t
val
extract_goals
:
(
Ident
.
ident
*
Term
.
fmla
*
context
)
list
t
val
split_goals
:
unit
->
context
list
t
val
identity
:
context
t
src/main.ml
View file @
33e453cd
...
...
@@ -92,7 +92,7 @@ let type_file env file =
Typing
.
add_from_file
env
file
let
extract_goals
ctxt
=
Transform
.
apply
Transform
.
split_goals
ctxt
Transform
.
apply
(
Transform
.
split_goals
()
)
ctxt
let
transform
env
l
=
let
l
=
List
.
map
...
...
src/transform/inlining.ml
View file @
33e453cd
...
...
@@ -66,7 +66,7 @@ and replacep env f =
and
substt
env
d
=
t_map
(
replacet
env
)
(
replacep
env
)
d
and
substp
env
d
=
f_map
(
replacet
env
)
(
replacep
env
)
d
let
fold
isnotinlinedt
isnotinlinedf
ctxt0
ctxt
env
=
let
fold
isnotinlinedt
isnotinlinedf
ctxt0
(
env
,
ctxt
)
=
(* Format.printf "I see : %a@\n%a@\n" Pretty.print_decl d print_env env;*)
let
d
=
ctxt0
.
ctxt_decl
in
match
d
.
d_node
with
...
...
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