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
CHARGUERAUD Arthur
cfml
Commits
a6263aae
Commit
a6263aae
authored
Apr 01, 2016
by
charguer
Browse files
inprogress
parent
f37ac489
Changes
24
Expand all
Hide whitespace changes
Inline
Side-by-side
Makefile
View file @
a6263aae
...
...
@@ -31,10 +31,11 @@ coqlib:
coqlib_quick
:
$(MAKE)
-C
lib/coq quick
# quick_cf builds what is needed for compiling characteristic formulae files (CFHeader)
coqlib_quick_cf
:
$(MAKE)
-C
lib/coq quick_cf
#------ TODO: ocamllib is deprecated
#------ TODO: ocamllib is deprecated
ocamllib
:
tools
$(MAKE)
-C
lib/ocaml
...
...
bin/Old_CFTactics.v
0 → 100644
View file @
a6263aae
This diff is collapsed.
Click to expand it.
bin/primitives.ml
0 → 100644
View file @
a6263aae
open
Mytools
(*#########################################################################*)
(* ** Helper function to decompose Coq paths *)
(*#########################################################################*)
(* TEMPORARILY DEPRECATED
(** List of special modules whose [open] should not lead to the
generation of an [Require Import] statement. *)
let is_primitive_module n =
List.mem n [ "NullPointers"; "StrongPointers" ]
(* ; "Okasaki"; "OkaStream" *)
(** [is_primitive_module] Recognizes builtin modules that have a special treatment,
namely "NullPointers" and "StrongPointers" *)
val is_primitive_module : string -> bool
*)
(* TEMPORARILY DEPRECATED
(** List of special top-level definitions that should not lead
to the generation of a characteristic formula. The definition
of [!$] as a keyword for forcing lazy expressions is one such
exception. *)
let hack_recognize_okasaki_lazy = function
| "!$" -> true
| _ -> false
(** Below is a HACK for the [!$] symbol used in Okasaki's code to mean "lazy" *)
val hack_recognize_okasaki_lazy : string -> bool
*)
(** DEPRECATED test only base on the last part of the name
let rec split_at_dots s pos =
try
let dot = String.index_from s pos '.' in
String.sub s pos (dot - pos) :: split_at_dots s (dot + 1)
with Not_found ->
[String.sub s pos (String.length s - pos)]
let name_of_mlpath s =
List.hd (List.rev (split_at_dots s 0))
(* HACK! Same as above, but only checks base on the tail of the name,
e.g. considering only "+" instead of "Pervasives.+"
This hack is only correct if we forbit the rebinding of
these special primitive names, however this check is not
yet implemented. *)
val is_inlined_primitive_hack : string -> int -> bool
let is_inlined_primitive_hack p arity =
let p = add_pervasives_prefix_if_needed p in
match list_assoc_option p Renaming.inlined_primitives_table with
| None -> false
| Some (n,y) -> (arity = n)
(* old: let inlined_primitives_table = List.map (fun (x,(n,y)) -> name_of_mlpath x, (n,y)) inlined_primitives_table in *)
*)
\ No newline at end of file
bin/primitives.mli
0 → 100644
View file @
a6263aae
(** This module contains information for properly handling
OCaml builtin functions and Coq builtin functions and
data types. *)
bin/test.v
0 → 100644
View file @
a6263aae
Require
Import
List
.
Lemma
test
:
True
.
let
x
:=
eval
compute
in
(
List
.
length
(
3
::
4
::
nil
))
in
pose
x
.
admit
.
examples/BasicDemos/Demo.ml
View file @
a6263aae
...
...
@@ -164,6 +164,11 @@ let test_partial_app_arities () =
let
f3
=
func4
1
2
3
in
f1
2
3
4
+
f2
3
4
+
f3
4
let
app_partial_builtin
()
=
let
f
=
(
+
)
1
in
f
2
(********************************************************************)
(* ** Over applications *)
...
...
examples/Makefile.example
View file @
a6263aae
...
...
@@ -64,7 +64,8 @@ OCAMLBUILD := \
##############################################################
# Targets
all
:
code cf proof
all
:
cf proof
# code => excluded cause does not work yet
nocode
:
cf proof
...
...
generator/Makefile
View file @
a6263aae
...
...
@@ -18,3 +18,7 @@ clean:
# Note: to generate mli files, run the following command from ./_build:
# ocamlc -I typing -I utils -I tools -I parsing -I lex -I /usr/local/lib/ocaml/4.01.0/pprint/ -i normalize.ml > ../normalize.mli
# TODO
:
understand if myocamldeb is needed or not.
\ No newline at end of file
generator/characteristic.ml
View file @
a6263aae
...
...
@@ -8,7 +8,6 @@ open Print_tast
open
Print_type
open
Formula
open
Coq
open
Primitives
open
Path
open
Renaming
open
Printf
...
...
@@ -122,19 +121,9 @@ let rec lift_btyp t =
val_type
|
Btyp_arrow
(
t1
,
t2
)
->
val_type
|
Btyp_constr
(
id
,
[
t
])
when
Path
.
name
id
=
"
ref"
||
Path
.
name
id
=
"Pervasives.ref"
||
Path
.
name
id
=
"
mlist"
->
(* --todo: not needed anymore
*)
|
Btyp_constr
(
id
,
[
t
])
when
Path
.
name
id
=
"
array"
->
(*
|| Path.name id = "
Pervasives.array"
*)
loc_type
|
Btyp_constr
(
id
,
[
t
])
when
Path
.
name
id
=
"array"
||
Path
.
name
id
=
"Pervasives.array"
->
loc_type
|
Btyp_constr
(
id
,
[
t
])
when
Path
.
name
id
=
"heap"
||
Path
.
name
id
=
"Heap.heap"
->
(* todo generalize *)
loc_type
|
Btyp_constr
(
id
,
[
t
])
when
Path
.
same
id
Predef
.
path_lazy_t
||
Path
.
name
id
=
"Lazy.t"
->
aux
t
(* todo: les Lazy provenant des patterns ne sont pas identique Predef.path_lazy_t *)
|
Btyp_constr
(
id
,
[
t
])
when
Path
.
name
id
=
"Stream.stream"
||
Path
.
name
id
=
"stream"
->
Coq_app
(
Coq_var
"list"
,
aux
t
)
|
Btyp_constr
(
id
,
[
t
])
when
Path
.
name
id
=
"Stream.stream_cell"
||
Path
.
name
id
=
"stream_cell"
->
Coq_app
(
Coq_var
"list"
,
aux
t
)
|
Btyp_constr
(
id
,
ts
)
->
coq_apps
(
Coq_var
(
type_constr_name
(
lift_path_name
id
)))
(
List
.
map
aux
ts
)
|
Btyp_tuple
ts
->
...
...
@@ -150,6 +139,24 @@ let rec lift_btyp t =
then
unsupported
(
"found a recursive type that is not erased by an arrow:"
^
(
print_out_type
t
));
aux
t1
(* TEMPORARILY DEPRECATED
| Btyp_constr (id,[t]) when Path.name id = "ref" || Path.name id = "Pervasives.ref" ->
loc_type
| Btyp_constr (id,[t]) when Path.name id = "heap" || Path.name id = "Heap.heap" ->
loc_type
| Btyp_constr (id,[t]) when Path.same id Predef.path_lazy_t || Path.name id = "Lazy.t" ->
aux t
| Btyp_constr (id,[t]) when Path.name id = "Stream.stream" || Path.name id = "stream" ->
Coq_app (Coq_var "list", aux t)
| Btyp_constr (id,[t]) when Path.name id = "Stream.stream_cell" || Path.name id = "stream_cell" ->
Coq_app (Coq_var "list", aux t)
*)
(* REMARK: les Lazy provenant des patterns ne sont pas identique Predef.path_lazy_t *)
(** Translates a Caml type into a Coq type *)
let
lift_typ_exp
ty
=
...
...
@@ -783,7 +790,8 @@ let rec cfg_structure_item s : cftops =
end
else
if
(
List
.
length
pat_expr_list
=
1
)
then
begin
(* later: check it is not a function *)
let
(
pat
,
bod
)
=
List
.
hd
pat_expr_list
in
let
x
=
pattern_name_protect_infix
pat
in
if
(
hack_recognize_okasaki_lazy
x
)
then
[]
else
begin
(* DEPRECATED if (hack_recognize_okasaki_lazy x) then [] else *)
begin
let
fvs_typ
,
typ
=
lift_typ_sch
pat
.
pat_type
in
let
fvs
=
List
.
map
name_of_type
fvs
in
let
fvs_strict
=
list_intersect
fvs
fvs_typ
in
...
...
@@ -852,7 +860,7 @@ let rec cfg_structure_item s : cftops =
|
Tstr_modtype
(
id
,
decl
)
->
cfg_modtype
id
decl
|
Tstr_open
path
->
if
is_primitive_module
(
Path
.
name
path
)
then
[]
else
(* TEMPORARILY DEPRECATED
if is_primitive_module (Path.name path) then [] else
*)
[
Cftop_coqs
[
Coqtop_require_import
[
lift_full_path_name
path
]
]
]
|
Tstr_primitive
(
id
,
descr
)
->
...
...
@@ -1372,6 +1380,7 @@ let cfg_file str =
Coqtop_set_implicit_args
;
Coqtop_require
[
"Coq.ZArith.BinInt"
;
"LibLogic"
;
"LibRelation"
;
"LibInt"
;
"Shared"
;
"CFHeaps"
;
"CFApp"
];
Coqtop_require_import
[
"CFHeader"
];
Coqtop_require
[
"CFPrint"
];
Coqtop_custom
"Open Scope list_scope."
;
Coqtop_custom
"Local Notation
\"
'int'
\"
:= (Coq.ZArith.BinInt.Z)."
;
Coqtop_custom
"Delimit Scope Z_scope with Z."
...
...
generator/coq.ml
View file @
a6263aae
...
...
@@ -36,7 +36,7 @@ and coq =
|
Coq_type
|
Coq_tuple
of
coqs
|
Coq_record
of
(
var
*
coq
)
list
|
Coq_tag
of
string
*
string
option
*
coq
|
Coq_tag
of
string
*
coq
list
*
string
option
*
coq
|
Coq_annot
of
coq
*
coq
and
coqs
=
coq
list
...
...
@@ -116,31 +116,31 @@ and implicit =
(** Several Coq constants *)
let
coq_false
=
Coq_var
"False"
Coq_var
"
Coq.Init.Logic.
False"
let
coq_true
=
Coq_var
"True"
Coq_var
"
Coq.Init.Logic.
True"
let
coq_bool_false
=
Coq_var
"false"
Coq_var
"
Coq.Init.Datatypes.
false"
let
coq_bool_true
=
Coq_var
"true"
Coq_var
"
Coq.Init.Datatypes.
true"
let
coq_tt
=
Coq_var
"tt"
Coq_var
"
Coq.Init.Datatypes.
tt"
let
coq_unit
=
Coq_var
"unit"
Coq_var
"
Coq.Init.Datatypes.
unit"
let
coq_int
=
Coq_var
"
int
"
Coq_var
"
Coq.ZArith.BinInt.Z
"
let
coq_list
xs
=
Coq_list
xs
let
coq_bool
=
Coq_var
"bool"
Coq_var
"
Coq.Init.Datatypes.
bool"
(** Identifier [x] *)
...
...
@@ -228,27 +228,27 @@ let coq_prod cs =
match
cs
with
|
[]
->
coq_unit
|
[
c
]
->
c
|
c0
::
cs'
->
List
.
fold_left
(
fun
acc
c
->
coq_apps
(
Coq_var
"prod"
)
[
acc
;
c
])
c0
cs'
|
c0
::
cs'
->
List
.
fold_left
(
fun
acc
c
->
coq_apps
(
Coq_var
"
Coq.Init.Datatypes.
prod"
)
[
acc
;
c
])
c0
cs'
(** Logic combinators *)
let
coq_eq
c1
c2
=
coq_apps
(
Coq_var
"Logic.eq"
)
[
c1
;
c2
]
coq_apps
(
Coq_var
"
Coq.Init.
Logic.eq"
)
[
c1
;
c2
]
let
coq_neq
c1
c2
=
coq_apps
(
Coq_var
"Logic.not"
)
[
coq_eq
c1
c2
]
coq_apps
(
Coq_var
"
Coq.Init.
Logic.not"
)
[
coq_eq
c1
c2
]
let
coq_disj
c1
c2
=
coq_apps
(
Coq_var
"Logic.or"
)
[
c1
;
c2
]
coq_apps
(
Coq_var
"
Coq.Init.
Logic.or"
)
[
c1
;
c2
]
let
coq_conj
c1
c2
=
coq_apps
(
Coq_var
"Logic.and"
)
[
c1
;
c2
]
coq_apps
(
Coq_var
"
Coq.Init.
Logic.and"
)
[
c1
;
c2
]
let
coq_neg
c
=
Coq_app
(
Coq_var
"LibBool.neg"
,
c
)
Coq_app
(
Coq_var
"
TLC.
LibBool.neg"
,
c
)
let
coq_exist
x
c1
c2
=
coq_apps
(
Coq_var
"Logic.ex"
)
[
Coq_fun
((
x
,
c1
)
,
c2
)]
coq_apps
(
Coq_var
"
Coq.Init.
Logic.ex"
)
[
Coq_fun
((
x
,
c1
)
,
c2
)]
(** Iterated logic combinators *)
...
...
@@ -263,10 +263,10 @@ let coq_exists xcs c2 =
(** Arithmetic operations *)
let
coq_le
c1
c2
=
coq_apps
(
Coq_var
"LibOrder.le"
)
[
c1
;
c2
]
coq_apps
(
Coq_var
"
TLC.
LibOrder.le"
)
[
c1
;
c2
]
let
coq_gt
c1
c2
=
coq_apps
(
Coq_var
"LibOrder.gt"
)
[
c1
;
c2
]
coq_apps
(
Coq_var
"
TLC.
LibOrder.gt"
)
[
c1
;
c2
]
let
coq_plus
c1
c2
=
coq_apps
(
Coq_var
"Coq.ZArith.BinInt.Zplus"
)
[
c1
;
c2
]
...
...
@@ -302,8 +302,9 @@ let string_of_var_bits vb =
let
value_variable
n
=
string_of_var_bits
(
var_bits_of_int
n
)
let
coq_tag
(
tag
:
string
)
?
label
(
term
:
coq
)
=
Coq_tag
(
tag
,
label
,
term
)
let
coq_tag
(
tag
:
string
)
?
args
?
label
(
term
:
coq
)
=
let
args
=
match
args
with
|
None
->
[]
|
Some
args
->
args
in
Coq_tag
(
"CFML.CFPrint."
^
tag
,
args
,
label
,
term
)
let
coq_annot
(
term
:
coq
)
(
term_type
:
coq
)
=
Coq_annot
(
term
,
term_type
)
...
...
generator/formula.ml
View file @
a6263aae
...
...
@@ -45,41 +45,41 @@ and cftops = cftop list
(** Abstract datatype for dynamic values *)
let
coq_dyn_at
=
coq_var_at
"CFHeaps.dyn"
let
coq_dyn_at
=
coq_var_at
"
CFML.
CFHeaps.dyn"
(** Abstract datatype for functions *)
let
val_type
=
Coq_var
"CFApp.func"
let
val_type
=
Coq_var
"
CFML.
CFApp.func"
(** Abstract data type for locations *)
let
loc_type
=
Coq_var
"CFHeaps.loc"
Coq_var
"
CFML.
CFHeaps.loc"
(** Abstract data type for heaps *)
let
heap
=
Coq_var
"CFHeaps.heap"
Coq_var
"
CFML.
CFHeaps.heap"
(** Type of proposition on heaps, [hprop], a shorthand for [heap->Prop] *)
let
hprop
=
Coq_var
"CFHeaps.hprop"
Coq_var
"
CFML.
CFHeaps.hprop"
(** Type of representation predicates *)
let
htype
c_abstract
c_concrete
=
coq_apps
(
Coq_var
"CFHeaps.htype"
)
[
c_abstract
;
c_concrete
]
coq_apps
(
Coq_var
"
CFML.
CFHeaps.htype"
)
[
c_abstract
;
c_concrete
]
(** The identity representation predicate *)
let
id_repr
=
Coq_var
"CFHeaps.Id"
Coq_var
"
CFML.
CFHeaps.Id"
(** Representation predicate tag *)
let
hdata
c_concrete
c_abstract
=
coq_apps
(
Coq_var
"CFHeaps.hdata"
)
[
c_abstract
;
c_concrete
]
coq_apps
(
Coq_var
"
CFML.
CFHeaps.hdata"
)
[
c_abstract
;
c_concrete
]
(** Type of pure post-conditions [_ -> Prop] *)
...
...
@@ -104,7 +104,7 @@ let formula_type =
(** Hprop entailment [H1 ==> H2] *)
let
heap_impl
h1
h2
=
coq_apps
(
Coq_var
"LibLogic.pred_le"
)
[
h1
;
h2
]
coq_apps
(
Coq_var
"
TLC.
LibLogic.pred_le"
)
[
h1
;
h2
]
(** Specialized Hprop entailment [H1 ==> Q2 tt] *)
...
...
@@ -114,7 +114,7 @@ let heap_impl_unit h1 q2 =
(** Postcondition entailment [Q1 ===> Q2] *)
let
post_impl
q1
q2
=
coq_apps
(
Coq_var
"LibRelation.rel_le"
)
[
q1
;
q2
]
coq_apps
(
Coq_var
"
TLC.
LibRelation.rel_le"
)
[
q1
;
q2
]
(** Specialized post-conditions [fun (_:unit) => H], i.e. [# H] *)
...
...
@@ -124,17 +124,17 @@ let post_unit h =
(** Separating conjunction [H1 * H2] *)
let
heap_star
h1
h2
=
coq_apps
(
Coq_var
"CFHeaps.heap_is_star"
)
[
h1
;
h2
]
coq_apps
(
Coq_var
"
CFML.
CFHeaps.heap_is_star"
)
[
h1
;
h2
]
(** Base data [heap_is_single c1 c2] *)
let
heap_is_single
c1
c2
=
coq_apps
(
coq_var_at
"CFHeaps.heap_is_single"
)
[
c1
;
Coq_wild
;
c2
]
coq_apps
(
coq_var_at
"
CFML.
CFHeaps.heap_is_single"
)
[
c1
;
Coq_wild
;
c2
]
(** Empty heap predicate [[]] *)
let
heap_empty
=
Coq_var
"CFHeaps.heap_is_empty"
Coq_var
"
CFML.
CFHeaps.heap_is_empty"
(** Iterated separating conjunction [H1 * .. * HN] *)
...
...
@@ -146,7 +146,7 @@ let heap_stars hs =
(** Lifted existentials [Hexists x, H] *)
let
heap_exists
xname
xtype
h
=
Coq_app
(
Coq_var
"CFHeaps.heap_is_pack"
,
Coq_fun
((
xname
,
xtype
)
,
h
))
Coq_app
(
Coq_var
"
CFML.
CFHeaps.heap_is_pack"
,
Coq_fun
((
xname
,
xtype
)
,
h
))
(** Lifted existentials [Hexists x, H], alternative *)
...
...
@@ -161,4 +161,4 @@ let heap_existss x_names_types h =
(** Lifted propositions [ [P] ] *)
let
heap_pred
c
=
Coq_app
(
Coq_var
"CFHeaps.heap_is_empty_st"
,
c
)
Coq_app
(
Coq_var
"
CFML.
CFHeaps.heap_is_empty_st"
,
c
)
generator/formula_to_coq.ml
View file @
a6263aae
...
...
@@ -7,6 +7,7 @@ open Renaming
(*#########################################################################*)
(* ** Conversion of IMPERATIVE characteristic formulae to Coq *)
(* TODO: extract hard coded constants*)
let
rec
coqtops_of_imp_cf
cf
=
let
coq_of_cf
=
coqtops_of_imp_cf
in
...
...
@@ -18,7 +19,7 @@ let rec coqtops_of_imp_cf cf =
|
Some
t
->
t
in
let
f_core
=
coq_funs
[(
"H"
,
hprop
);(
"Q"
,
Coq_impl
(
typ
,
hprop
))]
c
in
let
f
=
Coq_app
(
Coq_var
"CFHeaps.local"
,
f_core
)
in
let
f
=
Coq_app
(
Coq_var
"
CFML.
CFHeaps.local"
,
f_core
)
in
match
label
with
|
None
->
coq_tag
tag
f
|
Some
x
->
(*todo:remove this hack*)
if
x
=
"_c"
then
coq_tag
tag
f
else
...
...
@@ -50,7 +51,7 @@ let rec coqtops_of_imp_cf cf =
assert
(
List
.
length
ts
=
List
.
length
vs
);
let
tvs
=
List
.
combine
ts
vs
in
let
args
=
List
.
map
(
fun
(
t
,
v
)
->
coq_apps
coq_dyn_at
[
t
;
v
])
tvs
in
coq_tag
"tag_apply"
(
coq_apps
(
coq_var_at
"app_def"
)
[
f
;
coq_list
args
;
tret
])
coq_tag
"tag_apply"
(
coq_apps
(
coq_var_at
"
CFML.CFApp.
app_def"
)
[
f
;
coq_list
args
;
tret
])
(* (!Apply: (app_def f [(@dyn t1 v1) (@dyn t2 v2)])) *)
(* DEPRECATED
...
...
@@ -124,8 +125,8 @@ let rec coqtops_of_imp_cf cf =
*)
|
Cf_caseif
(
v
,
cf1
,
cf2
)
->
let
c1
=
Coq_impl
(
coq_eq
v
(
C
oq_
var
"
true
"
)
,
coq_apps
(
coq_of_cf
cf1
)
[
h
;
q
])
in
let
c2
=
Coq_impl
(
coq_eq
v
(
C
oq_
var
"
false
"
)
,
coq_apps
(
coq_of_cf
cf2
)
[
h
;
q
])
in
let
c1
=
Coq_impl
(
coq_eq
v
c
oq_
bool_
true
,
coq_apps
(
coq_of_cf
cf1
)
[
h
;
q
])
in
let
c2
=
Coq_impl
(
coq_eq
v
c
oq_
bool_
false
,
coq_apps
(
coq_of_cf
cf2
)
[
h
;
q
])
in
funhq
"tag_if"
(
coq_conj
c1
c2
)
(* (!I a: (fun H Q => (x = true -> Q1 H Q) /\ (x = false -> Q2 H Q))) *)
...
...
@@ -148,7 +149,7 @@ let rec coqtops_of_imp_cf cf =
where trueb are implicit by coercions *)
|
Cf_match
(
label
,
n
,
cf1
)
->
coq_tag
(
Printf
.
sprintf
"(tag_match %d%snat)
"
n
"%"
)
(*~label:label*)
(
coq_of_cf
cf1
)
coq_tag
"tag_match"
~
args
:
[
Coq_var
(
Printf
.
sprintf
"%d%s
"
n
"%
nat
"
)
]
(*~label:label*)
(
coq_of_cf
cf1
)
|
Cf_seq
(
cf1
,
cf2
)
->
let
q'
=
Coq_var
"Q'"
in
...
...
@@ -168,7 +169,7 @@ let rec coqtops_of_imp_cf cf =
let
ple
=
Coq_impl
(
coq_le
i
v2
,
coq_apps
body_le
[
h
;
q
])
in
let
body_gt
=
funhq
"tag_ret"
~
rettype
:
coq_unit
(
heap_impl_unit
h
q
)
in
let
pgt
=
Coq_impl
(
coq_gt
i
v2
,
coq_apps
body_gt
[
h
;
q
])
in
let
locals
=
Coq_app
(
Coq_var
"CFHeaps.is_local_pred"
,
s
)
in
let
locals
=
Coq_app
(
Coq_var
"
CFML.
CFHeaps.is_local_pred"
,
s
)
in
let
bodys
=
coq_conj
ple
pgt
in
let
hypr
=
coq_foralls
[(
i_name
,
coq_int
);
(
"H"
,
hprop
);
(
"Q"
,
Coq_impl
(
coq_unit
,
hprop
))]
(
Coq_impl
(
bodys
,
(
coq_apps
s
[
i
;
h
;
q
])))
in
funhq
"tag_for"
(
Coq_forall
((
"S"
,
typs
)
,
coq_impls
[
locals
;
hypr
]
(
coq_apps
s
[
v1
;
h
;
q
])))
...
...
@@ -188,7 +189,7 @@ let rec coqtops_of_imp_cf cf =
let
cfif
=
Cf_caseif
(
Coq_var
"_c"
,
cfseq
,
cfret
)
in
let
bodyr
=
coq_of_cf
(
Cf_let
((
"_c"
,
coq_bool
)
,
cf1
,
cfif
))
in
let
hypr
=
coq_foralls
[(
"H"
,
hprop
);
(
"Q"
,
Coq_impl
(
coq_unit
,
hprop
))]
(
Coq_impl
(
coq_apps
bodyr
[
h
;
q
]
,
(
coq_apps
r
[
h
;
q
])))
in
let
localr
=
Coq_app
(
Coq_var
"CFHeaps.is_local"
,
r
)
in
let
localr
=
Coq_app
(
Coq_var
"
CFML.
CFHeaps.is_local"
,
r
)
in
funhq
"tag_while"
(
Coq_forall
((
"R"
,
typr
)
,
coq_impls
[
localr
;
hypr
]
(
coq_apps
r
[
h
;
q
])))
(* (!While: (fun H Q => forall R:~~unit, is_local R ->
(forall H Q,
...
...
@@ -198,7 +199,7 @@ let rec coqtops_of_imp_cf cf =
|
Cf_pay
(
cf1
)
->
let
h'
=
Coq_var
"H'"
in
let
c1
=
coq_apps
(
Coq_var
"pay_one"
)
[
h
;
h'
]
in
let
c1
=
coq_apps
(
Coq_var
"
CFML.CFHeaps.
pay_one"
)
[
h
;
h'
]
in
let
c2
=
coq_apps
(
coq_of_cf
cf1
)
[
h'
;
Coq_var
"Q"
]
in
funhq
"tag_pay"
(
coq_exist
"H'"
hprop
(
coq_conj
c1
c2
))
(* (!Pay: fun H Q => exists H', pay_one H H' /\ F1 H' Q *)
...
...
generator/normalize.ml
View file @
a6263aae
...
...
@@ -5,7 +5,6 @@ open Parsetree
open
Mytools
open
Longident
open
Location
open
Primitives
open
Renaming
(** This file takes as input an abstract syntax tree and produces
...
...
@@ -37,9 +36,9 @@ let is_inlined_primitive e largs =
|
Pexp_ident
f
,
[
n
;
{
pexp_desc
=
Pexp_constant
(
Const_int
m
)}]
(* TODO: check that mod and "/" are actually coming from pervasives *)
when
m
>
0
&&
let
x
=
name_of_lident
f
in
x
=
"mod"
||
x
=
"/"
->
is_inlined_primitive
_hack
(
fullname_of_lident
f
)
primitive_special
is_inlined_primitive
(
fullname_of_lident
f
)
primitive_special
|
Pexp_ident
f
,_
->
is_inlined_primitive
_hack
(
fullname_of_lident
f
)
(
List
.
length
args
)
is_inlined_primitive
(
fullname_of_lident
f
)
(
List
.
length
args
)
|
_
->
false
let
is_failwith_function
e
=
...
...
generator/primitives.ml
deleted
100644 → 0
View file @
f37ac489
open
Mytools
(*#########################################################################*)
(* ** Helper function to decompose Coq paths *)
let
rec
split_at_dots
s
pos
=
try
let
dot
=
String
.
index_from
s
pos
'.'
in
String
.
sub
s
pos
(
dot
-
pos
)
::
split_at_dots
s
(
dot
+
1
)
with
Not_found
->
[
String
.
sub
s
pos
(
String
.
length
s
-
pos
)]
let
name_of_mlpath
s
=
List
.
hd
(
List
.
rev
(
split_at_dots
s
0
))
(*#########################################################################*)
(* ** List of inlined primitives *)
(** Fully-applied "inlined primitive" are translated directly as a
Coq application, and does not involve the "AppReturns" predicate. *)
let
primitive_special
=
-
1
let
inlined_primitives_table
=
[
"Pervasives.+"
,
(
2
,
"Coq.ZArith.BinInt.Zplus"
);
"Pervasives.-"
,
(
2
,
"Coq.ZArith.BinInt.Zminus"
);
"Pervasives.*"
,
(
2
,
"Coq.ZArith.BinInt.Zmult"
);
"Pervasives.~-"
,
(
1
,
"Coq.ZArith.BinInt.Zopp"
);
"Pervasives.&&"
,
(
2
,
"LibBool.and"
);
"Pervasives.||"
,
(
2
,
"LibBool.or"
);
(*
"Pervasives./", (primitive_special, "Coq.ZArith.Zdiv.Zdiv");
"Pervasives.mod", (primitive_special, "Coq.ZArith.Zdiv.Zmod");
*)
(*
"Pervasives.=", (2, "(fun _y _z => isTrue (_y = _z))");
"Pervasives.<>", (2, "(fun _y _z => isTrue (_y <> _z))");
"Pervasives.<", (2, "(fun _y _z => isTrue (_y < _z))");
"Pervasives.<=", (2, "(fun _y _z => isTrue (_y <= _z))");
"Pervasives.>", (2, "(fun _y _z => isTrue (_y > _z))");
"Pervasives.>=", (2, "(fun _y _z => isTrue (_y >= _z))");
"Pervasives.max", (2, "(fun _y _z => Zmin (_y >= _z))");
"Pervasives.min", (2, "(fun _y _z => isTrue (_y >= _z))");
"Pervasives.not", (1, "LibBool.neg");
"Pervasives.fst", (1, "(@fst _ _)");
"Pervasives.snd", (1, "(@snd _ _)");
"Pervasives.@", (2, "LibList.append");
"List.rev", (1, "LibList.rev");
"List.length", (1, "LibList.length");
"List.append", (2, "LibList.append");
"OkaStream.++", (2, "LibList.append");
"OkaStream.reverse", (1, "LibList.rev");
"StrongPointers.cast", (1, "")
"Lazy.force", (1, "");
"Okasaki.!$", (1, ""); (* i.e., @LibLogic.id _*)
*)
]
(*#########################################################################*)
(* ** List of all primitives *)
(** Primitive functions from the following list are mapped to special
Coq constants whose specification is axiomatized. *)
let
all_primitives_table
=
[
(* "Pervasives.=", "ml_eqb";
"Pervasives.<>", "ml_neq";
"Pervasives.==", "ml_phy_eq";
"Pervasives.!=", "ml_phy_neq";
"Pervasives.+", "ml_plus";
"Pervasives.-", "ml_minus";
"Pervasives.~-", "ml_opp";
"Pervasives.*", "ml_mul";
"Pervasives./", "ml_div";
"Pervasives.mod", "ml_mod";
"Pervasives.<=", "ml_leq";
"Pervasives.<", "ml_lt";
"Pervasives.>", "ml_gt";
"Pervasives.>=", "ml_geq";
"Pervasives.&&", "ml_and";
"Pervasives.||", "ml_or";
"Pervasives.@", "ml_append";
"Pervasives.raise", "ml_raise";
"Pervasives.asr", "ml_asr";
"Pervasives.ref", "ml_ref";
"Pervasives.!", "ml_get";
"Pervasives.:=", "ml_set";
"Pervasives.incr", "ml_incr";
"Pervasives.decr", "ml_decr";
"Pervasives.fst", "ml_fst";
"Pervasives.snd", "ml_snd";
"Pervasives.max_int", "ml_max_int";
"Pervasives.min_int", "ml_min_int";
"Pervasives.read_int", "ml_read_int";
"Pervasives.print_int", "ml_print_int";