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
121
Issues
121
List
Boards
Labels
Service Desk
Milestones
Merge Requests
15
Merge Requests
15
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
18aca836
Commit
18aca836
authored
Mar 18, 2019
by
François Bobot
Browse files
Options
Browse Files
Download
Plain Diff
Merge branch 'bobot/tagset' into 'master'
Imperative TagSet with iterators See merge request
!82
parents
21500d33
4f7af118
Changes
5
Hide whitespace changes
Inline
Side-by-side
Showing
5 changed files
with
717 additions
and
4 deletions
+717
-4
drivers/ocaml64.drv
drivers/ocaml64.drv
+6
-0
examples/stdlib/tagset/why3session.xml
examples/stdlib/tagset/why3session.xml
+359
-0
src/mlw/ocaml_printer.ml
src/mlw/ocaml_printer.ml
+6
-4
stdlib/mach/peano.mlw
stdlib/mach/peano.mlw
+9
-0
stdlib/mach/tagset.mlw
stdlib/mach/tagset.mlw
+337
-0
No files found.
drivers/ocaml64.drv
View file @
18aca836
...
...
@@ -302,6 +302,12 @@ module mach.peano.MinMax
syntax val min "min %1 %2" prec 4 3 3
end
module mach.peano.Int63
syntax val defensive_to_int63 "%1"
syntax val to_int63 "%1"
syntax val of_int63 "%1"
end
module mach.onetime.OneTime
syntax type t "int"
syntax val to_int "Z.of_int %1" prec 4 3
...
...
examples/stdlib/tagset/why3session.xml
0 → 100644
View file @
18aca836
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session
shape_version=
"6"
>
<prover
id=
"0"
name=
"Alt-Ergo"
version=
"2.2.0"
timelimit=
"1"
steplimit=
"0"
memlimit=
"1000"
/>
<prover
id=
"1"
name=
"CVC4"
version=
"1.6"
timelimit=
"1"
steplimit=
"0"
memlimit=
"1000"
/>
<prover
id=
"2"
name=
"Z3"
version=
"4.4.1"
timelimit=
"1"
steplimit=
"0"
memlimit=
"1000"
/>
<file
proved=
"true"
>
<path
name=
".."
/>
<path
name=
".."
/>
<path
name=
".."
/>
<path
name=
"stdlib"
/>
<path
name=
"mach"
/>
<path
name=
"tagset.mlw"
/>
<theory
name=
"TagSetIntf"
proved=
"true"
>
<goal
name=
"VC t"
expl=
"VC for t"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"VC iterator"
expl=
"VC for iterator"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.05"
/></proof>
</goal>
</theory>
<theory
name=
"TagSet"
proved=
"true"
>
<goal
name=
"VC iteration_state"
expl=
"VC for iteration_state"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.07"
/></proof>
</goal>
<goal
name=
"VC t"
expl=
"VC for t"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.03"
/></proof>
</goal>
<goal
name=
"VC create"
expl=
"VC for create"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.09"
/></proof>
</goal>
<goal
name=
"VC mem"
expl=
"VC for mem"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.11"
/></proof>
</goal>
<goal
name=
"VC max_tags"
expl=
"VC for max_tags"
proved=
"true"
>
<proof
prover=
"0"
obsolete=
"true"
><result
status=
"timeout"
time=
"1.00"
/></proof>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.09"
/></proof>
<proof
prover=
"2"
obsolete=
"true"
><result
status=
"timeout"
time=
"1.00"
/></proof>
</goal>
<goal
name=
"VC resize"
expl=
"VC for resize"
proved=
"true"
>
<transf
name=
"split_vc"
proved=
"true"
>
<goal
name=
"VC resize.0"
expl=
"integer overflow"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.06"
/></proof>
</goal>
<goal
name=
"VC resize.1"
expl=
"division by zero"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"VC resize.2"
expl=
"integer overflow"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.07"
/></proof>
</goal>
<goal
name=
"VC resize.3"
expl=
"integer overflow"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.07"
/></proof>
</goal>
<goal
name=
"VC resize.4"
expl=
"array creation size"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.05"
/></proof>
</goal>
<goal
name=
"VC resize.5"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.06"
/></proof>
</goal>
<goal
name=
"VC resize.6"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.03"
/></proof>
</goal>
<goal
name=
"VC resize.7"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.05"
/></proof>
</goal>
<goal
name=
"VC resize.8"
expl=
"type invariant"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.08"
/></proof>
</goal>
<goal
name=
"VC resize.9"
expl=
"type invariant"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.10"
/></proof>
</goal>
<goal
name=
"VC resize.10"
expl=
"type invariant"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.10"
/></proof>
</goal>
<goal
name=
"VC resize.11"
expl=
"type invariant"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.09"
/></proof>
</goal>
<goal
name=
"VC resize.12"
expl=
"type invariant"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.11"
/></proof>
</goal>
<goal
name=
"VC resize.13"
expl=
"type invariant"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.05"
/></proof>
</goal>
<goal
name=
"VC resize.14"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.06"
/></proof>
</goal>
<goal
name=
"VC resize.15"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.06"
/></proof>
</goal>
</transf>
</goal>
<goal
name=
"VC add"
expl=
"VC for add"
proved=
"true"
>
<transf
name=
"split_vc"
proved=
"true"
>
<goal
name=
"VC add.0"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.03"
/></proof>
</goal>
<goal
name=
"VC add.1"
expl=
"index in array bounds"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"VC add.2"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.03"
/></proof>
</goal>
<goal
name=
"VC add.3"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.03"
/></proof>
</goal>
<goal
name=
"VC add.4"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"VC add.5"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"VC add.6"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"VC add.7"
expl=
"type invariant"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"VC add.8"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"VC add.9"
expl=
"type invariant"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.08"
/></proof>
</goal>
<goal
name=
"VC add.10"
expl=
"type invariant"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.10"
/></proof>
</goal>
<goal
name=
"VC add.11"
expl=
"type invariant"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.10"
/></proof>
</goal>
<goal
name=
"VC add.12"
expl=
"type invariant"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.11"
/></proof>
</goal>
<goal
name=
"VC add.13"
expl=
"type invariant"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.15"
/></proof>
</goal>
<goal
name=
"VC add.14"
expl=
"type invariant"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.06"
/></proof>
</goal>
<goal
name=
"VC add.15"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.05"
/></proof>
</goal>
</transf>
</goal>
<goal
name=
"VC remove"
expl=
"VC for remove"
proved=
"true"
>
<transf
name=
"split_vc"
proved=
"true"
>
<goal
name=
"VC remove.0"
expl=
"index in array bounds"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.03"
/></proof>
</goal>
<goal
name=
"VC remove.1"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"VC remove.2"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.05"
/></proof>
</goal>
<goal
name=
"VC remove.3"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"VC remove.4"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"VC remove.5"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"VC remove.6"
expl=
"type invariant"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.03"
/></proof>
</goal>
<goal
name=
"VC remove.7"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"VC remove.8"
expl=
"type invariant"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.07"
/></proof>
</goal>
<goal
name=
"VC remove.9"
expl=
"type invariant"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.08"
/></proof>
</goal>
<goal
name=
"VC remove.10"
expl=
"type invariant"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.10"
/></proof>
</goal>
<goal
name=
"VC remove.11"
expl=
"type invariant"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.10"
/></proof>
</goal>
<goal
name=
"VC remove.12"
expl=
"type invariant"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.13"
/></proof>
</goal>
<goal
name=
"VC remove.13"
expl=
"type invariant"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.05"
/></proof>
</goal>
<goal
name=
"VC remove.14"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.08"
/></proof>
</goal>
<goal
name=
"VC remove.15"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.05"
/></proof>
</goal>
<goal
name=
"VC remove.16"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"VC remove.17"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"VC remove.18"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"VC remove.19"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"VC remove.20"
expl=
"type invariant"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"VC remove.21"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"VC remove.22"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.05"
steps=
"73"
/></proof>
</goal>
</transf>
</goal>
<goal
name=
"VC iterator"
expl=
"VC for iterator"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.11"
/></proof>
</goal>
<goal
name=
"Iterator.VC create"
expl=
"VC for create"
proved=
"true"
>
<transf
name=
"split_vc"
proved=
"true"
>
<goal
name=
"VC create.0"
expl=
"loop invariant init"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.05"
/></proof>
</goal>
<goal
name=
"VC create.1"
expl=
"loop invariant init"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"VC create.2"
expl=
"index in array bounds"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"VC create.3"
expl=
"integer overflow"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.06"
/></proof>
</goal>
<goal
name=
"VC create.4"
expl=
"loop variant decrease"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.05"
/></proof>
</goal>
<goal
name=
"VC create.5"
expl=
"loop invariant preservation"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.06"
/></proof>
</goal>
<goal
name=
"VC create.6"
expl=
"loop invariant preservation"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.08"
/></proof>
</goal>
<goal
name=
"VC create.7"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.07"
/></proof>
</goal>
<goal
name=
"VC create.8"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"VC create.9"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.08"
/></proof>
</goal>
<goal
name=
"VC create.10"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.08"
/></proof>
</goal>
<goal
name=
"VC create.11"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.13"
/></proof>
</goal>
<goal
name=
"VC create.12"
expl=
"precondition"
proved=
"true"
>
<transf
name=
"split_vc"
proved=
"true"
>
<goal
name=
"VC create.12.0"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"VC create.12.1"
expl=
"precondition"
proved=
"true"
>
<transf
name=
"split_vc"
proved=
"true"
>
<goal
name=
"VC create.12.1.0"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.07"
/></proof>
</goal>
<goal
name=
"VC create.12.1.1"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.06"
/></proof>
</goal>
</transf>
</goal>
<goal
name=
"VC create.12.2"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.12"
/></proof>
</goal>
</transf>
</goal>
<goal
name=
"VC create.13"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"VC create.14"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.03"
/></proof>
</goal>
<goal
name=
"VC create.15"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.03"
/></proof>
</goal>
</transf>
</goal>
<goal
name=
"Iterator.VC is_empty"
expl=
"VC for is_empty"
proved=
"true"
>
<proof
prover=
"2"
><result
status=
"valid"
time=
"0.17"
/></proof>
</goal>
<goal
name=
"Iterator.VC next"
expl=
"VC for next"
proved=
"true"
>
<transf
name=
"split_vc"
proved=
"true"
>
<goal
name=
"VC next.0"
expl=
"assertion"
proved=
"true"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.02"
steps=
"109"
/></proof>
</goal>
<goal
name=
"VC next.1"
expl=
"index in array bounds"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.06"
/></proof>
</goal>
<goal
name=
"VC next.2"
expl=
"integer overflow"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.06"
/></proof>
</goal>
<goal
name=
"VC next.3"
expl=
"loop invariant init"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.05"
/></proof>
</goal>
<goal
name=
"VC next.4"
expl=
"loop invariant init"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.06"
/></proof>
</goal>
<goal
name=
"VC next.5"
expl=
"index in array bounds"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.08"
/></proof>
</goal>
<goal
name=
"VC next.6"
expl=
"integer overflow"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.06"
/></proof>
</goal>
<goal
name=
"VC next.7"
expl=
"loop variant decrease"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.05"
/></proof>
</goal>
<goal
name=
"VC next.8"
expl=
"loop invariant preservation"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.05"
/></proof>
</goal>
<goal
name=
"VC next.9"
expl=
"loop invariant preservation"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.08"
/></proof>
</goal>
<goal
name=
"VC next.10"
expl=
"assertion"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.08"
/></proof>
</goal>
<goal
name=
"VC next.11"
expl=
"type invariant"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.12"
/></proof>
</goal>
<goal
name=
"VC next.12"
expl=
"type invariant"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.07"
/></proof>
</goal>
<goal
name=
"VC next.13"
expl=
"type invariant"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.08"
/></proof>
</goal>
<goal
name=
"VC next.14"
expl=
"type invariant"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.09"
/></proof>
</goal>
<goal
name=
"VC next.15"
expl=
"type invariant"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.58"
/></proof>
</goal>
<goal
name=
"VC next.16"
expl=
"type invariant"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.13"
/></proof>
</goal>
<goal
name=
"VC next.17"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.12"
/></proof>
</goal>
<goal
name=
"VC next.18"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"VC next.19"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
src/mlw/ocaml_printer.ml
View file @
18aca836
...
...
@@ -92,12 +92,15 @@ module Print = struct
List
.
iter
(
fun
s
->
Hstr
.
add
h
s
()
)
ocaml_keywords
;
Hstr
.
mem
h
let
char_to_alnumusquote
c
=
match
c
with
'\''
->
"
\'
"
|
_
->
char_to_alnumus
c
(* iprinter: local names
aprinter: type variables
tprinter: toplevel definitions *)
let
iprinter
,
aprinter
,
tprinter
=
let
isanitize
=
sanitizer
char_to_alnumus
char_to_alnumus
in
let
lsanitize
=
sanitizer
char_to_lalnumus
char_to_alnumus
in
let
isanitize
=
sanitizer
char_to_alnumus
char_to_alnumus
quote
in
let
lsanitize
=
sanitizer
char_to_lalnumus
char_to_alnumus
quote
in
create_ident_printer
ocaml_keywords
~
sanitizer
:
isanitize
,
create_ident_printer
ocaml_keywords
~
sanitizer
:
lsanitize
,
create_ident_printer
ocaml_keywords
~
sanitizer
:
lsanitize
...
...
@@ -719,8 +722,7 @@ module Print = struct
let
extract_functor_args
info
dl
=
let
rec
extract
args
=
function
(* FIXME remove empty args? *)
(* | Dmodule (_, []) :: dl -> extract args dl *)
|
Dmodule
(
_
,
[]
)
::
dl
->
extract
args
dl
|
Dmodule
(
x
,
dlx
)
::
dl
when
is_signature
info
dlx
->
extract
((
x
,
dlx
)
::
args
)
dl
|
dl
->
List
.
rev
args
,
dl
in
...
...
stdlib/mach/peano.mlw
View file @
18aca836
...
...
@@ -102,10 +102,19 @@ module MinMax
end
module Int63
use int.Int
use mach.int.Int63
use Peano
val defensive_to_int63 (x:t) : int63
requires { Int63.in_bounds x.v }
ensures { result = x.v }
val partial to_int63 (x:t) : int63
ensures { result = x.v }
val of_int63 (x:int63) (low high: t) : t
requires { low.v <= x <= high.v }
ensures { result.v = x }
end
stdlib/mach/tagset.mlw
0 → 100644
View file @
18aca836
module S
use int.Int
use mach.int.Int63 as Int63
type key
val constant dummy: key
val function tag (k:key): Int63.int63
ensures { k<>dummy -> 0 <= result < Int63.max_int63 }
axiom tag_correct: forall x y. tag x = tag y -> x = y
end
module TagSetIntf
use int.Int
use import mach.int.Int63 as Int63
use map.Map
use map.Const
use set.Fset as S
use list.List
use list.Mem as LMem
use import mach.array.Array63 as Array
use seq.Seq as Seq
use bool.Bool
use mach.peano.Peano as Peano
use mach.peano.Int63 as PeanoInt63
use ref.Ref
clone import S as S with axiom tag_correct
type iteration_state = mutable { }
type t = abstract {
mutable elts: S.fset key;
mutable iterated: iteration_state;
}
invariant { not (S.mem S.dummy elts) }
by {
elts = S.empty;
iterated = any iteration_state;
}
val create () : t
ensures { result.elts = S.empty }
val function mem (k: key) (h: t) : bool
requires { k <> S.dummy }
ensures { result = S.mem k h.elts }
val function max_tags (h: t) : Int63.int63
ensures { forall v. S.mem v h.elts -> tag v <= result }
ensures { -1 <= result < Int63.max_int63 }
val add (h: t) (k: key): unit
requires { k <> S.dummy }
ensures { h.elts = S.add k (old h.elts) }
writes { h.elts, h.iterated }
val remove (h: t) (k: key): unit
requires { k <> S.dummy }
ensures { h.elts = S.remove k (old h.elts) }
writes { h.elts, h.iterated }
type iterator = abstract {
iterating: iteration_state;
mutable seen: S.fset key;
mutable todo: S.fset key;
all: S.fset key;
}
invariant { S.(union seen todo == all) }
invariant { S.(inter seen todo == S.empty) }
by {
iterating = any iteration_state;
seen = S.empty;
todo = S.empty;
all = S.empty
}
scope Iterator
val create (h:t) : iterator
ensures { result.seen = S.empty }
ensures { result.todo = h.elts }
ensures { result.all = h.elts }
alias { result.iterating with h.iterated }
predicate is_empty (i:iterator) = S.is_empty i.todo
val is_empty (i:iterator) : bool
ensures { result = (S.is_empty i.todo) }
val next (i:iterator) : key
requires { not (S.is_empty i.todo) }
writes { i.seen, i.todo }
ensures { S.mem result (old i.todo) }
ensures { i.todo = S.remove result (old i.todo) }
ensures { i.seen = S.add result (old i.seen) }
end
end
module TagSet
use int.Int
use mach.int.MinMax63
use import mach.int.Int63 as Int63
use set.Fset as S
use import mach.array.Array63 as Array
use seq.Seq
use bool.Bool
use mach.peano.Peano as Peano
use mach.peano.Int63 as PeanoInt63
use ref.Ref
clone import S as S with axiom tag_correct
type iteration_state = mutable {
ghost mutable elts': S.fset key;
mutable value: array key;
}
invariant { not (S.mem S.dummy elts') }
invariant { forall v. S.mem v elts' -> tag v < value.length }
invariant { forall v. S.mem v elts' -> value[tag v] <> S.dummy }
invariant { forall i. 0 <= i < value.length -> value[i] <> S.dummy -> tag (value[i]) = i }
invariant { forall i. 0 <= i < value.length -> value[i] <> S.dummy -> S.mem (value[i]) elts' }
by {
elts' = S.empty;
value = Array.make 0 (any key);
}
type t = {
ghost mutable elts: S.fset key;
mutable iterated: iteration_state;
}
invariant { elts = iterated.elts' }
let create () : t
ensures { result.elts = S.empty }
=
let iterated = {
elts' = S.empty;
value = Array.make 8 S.dummy;
}
in
{
elts = S.empty;
iterated = iterated;
}
let function mem (k: key) (h: t) : bool
requires { k <> S.dummy }
ensures { result = S.mem k h.elts } =
tag k < Array.length h.iterated.value && Array.(S.tag h.iterated.value[tag k] <> S.tag S.dummy)
let function max_tags (h: t) : Int63.int63
ensures { forall v. S.mem v h.elts -> tag v <= result }
ensures { -1 <= result < Int63.max_int63 } =
Array.(length h.iterated.value) - 1
let resize (h:t) (k:key) : unit
requires { k <> S.dummy }
ensures { tag k < Array.(length h.iterated.value) }
=
let len = tag k + 1 in
let n = Array.length h.iterated.value in
if len > n then begin
let nlen = (max len (2 * (min n (Int63.max_int / 2)))) in
let a = Array.(make nlen S.dummy) in
Array.blit h.iterated.value 0 a 0 n;
h.iterated.value <- a;
end
let add (h: t) (k: key): unit
requires { k <> S.dummy }
ensures { h.elts = S.add k (old h.elts) }
writes { h.elts , h.iterated } =
resize h k;
h.elts <- S.add k h.elts;
h.iterated.elts' <- S.add k h.iterated.elts';
h.iterated.value[tag k] <- k;
if false then
h.iterated <- {
elts' = h.iterated.elts';
value = h.iterated.value;
}
let remove (k: key) (h: t) : unit
requires { k <> S.dummy }
ensures { h.elts = S.remove k h.elts } =
if tag k < Array.length h.iterated.value then begin
h.elts <- S.remove k h.elts;
h.iterated.elts' <- S.remove k h.iterated.elts';
Array.(h.iterated.value[tag k] <- S.dummy);
end;
if false then
h.iterated <- {
elts' = h.iterated.elts';
value = h.iterated.value;
}
type iterator = {
iterating: iteration_state;
ghost mutable seen: S.fset key;
ghost mutable todo: S.fset key;
ghost all: S.fset key;
mutable offset: int63;
}