Commit 18d4c8a2 authored by charguer's avatar charguer
Browse files

add support for 'ignore CFML' directive at beginning of toplevel definitions to be ignored by cfml

parent eadc1a98
open Pervasives
(**
(**
*
* This file contains unit tests for testing the generation of
* characteristic formulae, their display, and their associated
......@@ -8,13 +8,35 @@ open Pervasives
*)
(********************************************************************)
(* ** Ignored definitions *)
let ignored_def =
ignore "CFML";
3
let ignored_fun x =
ignore "CFML";
2 * x
let not_ignored_fun x =
ignore x;
2 * x
let rec ignored_fun2a x =
ignore "CFML";
ignored_fun2b x
and ignored_fun2b x =
ignored_fun2a x
(********************************************************************)
(* ** Notation for PRE/INV/POST *)
let notation_inv_post r =
let notation_inv_post r =
!r
let notation_pre_inv_post r s =
let notation_pre_inv_post r s =
incr r; !s
......@@ -27,8 +49,8 @@ let notation_pre_inv_post r s =
type renaming_t' = int
type renaming_t2 = C'
type 'a renaming_t3 = int
type 'a_ renaming_t4 = int
type 'a renaming_t3 = int
type 'a_ renaming_t4 = int
let renaming_demo () =
(* let x_ = 3 in --rejected *)
......@@ -54,7 +76,7 @@ let let_poly_p1 () =
let let_poly_p2 () =
let f x = x in
let _r =
let _r =
let _s = f None in ()
in
()
......@@ -134,13 +156,13 @@ let let_poly_r2 () =
y
let let_poly_r3 () =
let r =
let r =
let x = ref [] in
[] in
r
(* ---Code not allowed because produces a ['_a list ref] at top level;
i.e. rejected when using OCaml "-strict_value_restriction" flag
i.e. rejected when using OCaml "-strict_value_restriction" flag
let h1 =
let f () : 'a list ref = ref [] in
f
......@@ -149,7 +171,7 @@ let h1 =
(********************************************************************)
(* ** Return *)
(* ** Return *)
let ret_unit x =
()
......@@ -163,7 +185,7 @@ let ret_int_pair () =
let ret_poly () =
[]
(* --Not yet supported:
(* --Not yet supported:
Error is: Cannot infer this placeholder of type Type
let ret_poly_internal () =
let x = ignore None in
......@@ -173,7 +195,7 @@ let ret_poly_internal () =
(* --TODO: BUG
The reference A_ was not found in the current environment.*)
(*
(*
let ret_poly_internal () =
let x = ignore (None : 'a option) in
()
......@@ -184,8 +206,8 @@ let ret_poly_internal () =
(* ** Sequence *)
let seq_ret_unit () =
ret_unit 1;
ret_unit 2;
ret_unit 1;
ret_unit 2;
ret_unit 3
......@@ -247,7 +269,7 @@ let let_fun_poly_pair_homogeneous () =
f 3 3
let let_fun_on_the_fly () =
(fun x f -> f x) 3 (fun x -> x+1)
(fun x f -> f x) 3 (fun x -> x+1)
let let_fun_in_let () =
let f = (assert (true); fun x -> x) in
......@@ -268,7 +290,7 @@ let app_partial_3_2 () =
let app_partial_add () =
let add x y = x + y in
let g = add 1 in g 2
let app_partial_appto () =
let appto x f = f x in
let _r = appto 3 ((+) 1) in
......@@ -301,7 +323,7 @@ let app_over_id () =
(********************************************************************)
(* ** Infix functions *)
let (+++) x y = x + y
let (+++) x y = x + y
let infix_aux x y = x +++ y
......@@ -336,7 +358,7 @@ let compare_min () =
let compare_float () =
(1. <> 0. && 1. <= 2.) || (0. = 1. && 1. >= 2. && 1. < 2. && 2. > 1.)
*)
let compare_poly () =
let _r1 = (None = None) in
let _r2 = (Some 3 = None) in
......@@ -347,8 +369,8 @@ let compare_poly () =
let f () = 4 in
let _r5 = ((Some f, None) = (None, Some f)) in *)
type 'a compare_poly_type =
| CompCst
type 'a compare_poly_type =
| CompCst
| CompPoly of 'a
| CompTuple of 'a * bool
| CompFunc of ('a -> 'a)
......@@ -369,18 +391,18 @@ let compare_physical_loc_func () =
let _r3 = if (f == f) then f() else 1 in
()
let compare_physical_algebraic () =
let rec replace (k:int) (v:int) (l:(int*int) list) =
let compare_physical_algebraic () =
let rec replace (k:int) (v:int) (l:(int*int) list) =
match l with
| [] -> l
| (k2,v2)::t2 ->
| (k2,v2)::t2 ->
let t = replace k v t2 in
if k = k2 then (k,v)::t
else if t != t2 then (k2,v2)::t
else l (* no change *)
in
replace 1 9 [(1,3); (4,2); (2,5)]
replace 1 9 [(1,3); (4,2); (2,5)]
(********************************************************************)
(* ** List operators *)
......@@ -443,15 +465,15 @@ let (top_val_pair_fun_1,top_val_pair_fun_2) =
(********************************************************************)
(* ** Polymorphic let bindings *)
let let_poly_nil () =
let let_poly_nil () =
let x = [] in x
let let_poly_nil_pair () =
let let_poly_nil_pair () =
let x = ([], []) in x
let let_poly_nil_pair_homogeneous () =
let x : ('a list * 'a list) = ([], []) in x
let let_poly_nil_pair_heterogeneous () =
let x : ('a list * int list) = ([], []) in x
......@@ -488,7 +510,7 @@ let match_nested () =
(* TODO
let match_term_when () =
let f x = x + 1 in
match f 3 with
match f 3 with
| 0 -> 1
| n when n > 0 -> 2
| _ -> 3
......@@ -512,7 +534,7 @@ let exn_assert_false () =
let exn_failwith () =
failwith "ok"
exception My_exn
exception My_exn
let exn_raise () =
raise My_exn
......@@ -522,7 +544,7 @@ let exn_raise () =
(* ** Assertions *)
let assert_true () =
assert true;
assert true;
3
let assert_pos x =
......@@ -530,16 +552,16 @@ let assert_pos x =
3
let assert_same (x:int) (y:int) =
assert (x = y);
assert (x = y);
3
let assert_let () =
assert (let _x = true in true);
assert (let _x = true in true);
3
let assert_seq () =
let r = ref 0 in
assert (incr r; true);
assert (incr r; true);
!r
let assert_in_seq () =
......@@ -558,14 +580,14 @@ let if_term () =
let if_else_if () =
let f x = false in
if f 0 then 1
if f 0 then 1
else if f 1 then 2
else 0
let if_then_no_else b =
let r = ref 0 in
if b
then incr r;
then incr r;
!r
......@@ -584,10 +606,10 @@ let sitems_get_nb r =
let sitems_incr_nb_let r =
let x = r.nb in
r.nb <- x + 1
r.nb <- x + 1
let sitems_incr_nb r =
r.nb <- r.nb + 1
r.nb <- r.nb + 1
let sitems_length_items_let r =
let x = r.items in
......@@ -663,9 +685,9 @@ let ref_gc () =
let _r2 = ref 1 in
let _r3 = ref 1 in
let _r4 = ref 1 in
let x =
let x =
let r5 = ref 2 in
!r5
!r5
in
x + !r1
......@@ -694,7 +716,7 @@ let array_ops () =
let while_decr () =
let n = ref 3 in
let c = ref 0 in
while !n > 0 do
while !n > 0 do
incr c;
decr n;
done;
......@@ -766,14 +788,14 @@ type type_clashing_with_var = int
(********************************************************************)
(* ** Type algebraic *)
type 'a alga_three =
| Alga_A
| Alga_B of int * int
type 'a alga_three =
| Alga_A
| Alga_B of int * int
| Alga_C of (int * int)
| Alga_D of 'a
| Alga_D of 'a
| Alga_E of 'a * ('a -> 'a)
type ('a,'b) algb_erase =
type ('a,'b) algb_erase =
| Algb_A of 'a
| Algb_B of (int -> 'b)
......@@ -781,17 +803,17 @@ type ('a,'b) algb_erase =
(********************************************************************)
(* ** Type record *)
type recorda = {
mutable recorda1 : int;
type recorda = {
mutable recorda1 : int;
mutable recorda2 : int }
(*----*)
type ('a,'b) recordb =
{ mutable recordb1 : 'a ;
type ('a,'b) recordb =
{ mutable recordb1 : 'a ;
mutable recordb2 : 'b -> 'b }
(* not supported: record overloading of fields
(* not supported: record overloading of fields
-- else would need to prefix all fields with the type... *)
......@@ -845,14 +867,14 @@ type typerecb1 = | Typerecb_1 of typerecb1 typerecb2
(*----*)
(* Circularity between mutable records and inductive is broken
(* Circularity between mutable records and inductive is broken
through the indirection at type loc *)
type 'a typerecd1 = { mutable typerecd1_f : 'a typerecd2 }
and 'a typerecd2 =
| Typerecd_2a
| Typerecd_2b of 'a typerecd1
| Typerecd_2c of 'a typerecd3
and 'a typerecd2 =
| Typerecd_2a
| Typerecd_2b of 'a typerecd1
| Typerecd_2c of 'a typerecd3
and 'a typerecd3 = { mutable typerecd3_f : 'a typerecd2 }
......@@ -861,7 +883,7 @@ and 'a typerecd3 = { mutable typerecd3_f : 'a typerecd2 }
(* ** Local module *)
module ModFoo = struct
type t = int
let x : t = 3
......@@ -879,7 +901,7 @@ module type ModBarType = sig
end
module ModBar : ModBarType = struct
type t = int
let x : t = 3
......@@ -890,14 +912,14 @@ end
(* ** Functor *)
module ModFunctor (Bar : ModBarType) = struct
type u = Bar.t
let x : u = Bar.x
end
module ModFunctorTyped (Bar : ModBarType) : ModBarType = struct
type t = Bar.t
let x : t = Bar.x
......@@ -949,7 +971,7 @@ let list_ops () =
(* TODO
let match_term_when () =
let f x = x + 1 in
match f 3 with
match f 3 with
| 0 -> 1
| n when n > 0 -> 2
| _ -> 3
......
......@@ -379,7 +379,7 @@ Proof using.
xapp2.
dup 5.
{ apply Spec. xrets. auto. }
{ xapp3_no_apply. Focus 2. apply S. xrets. auto. }
{ xapp3_no_apply. 2:{ apply S. } xrets. auto. }
{ xapp3_no_simpl. xrets~. skip. skip. }
{ xapp3. xrets~. }
{ xapp. xret. xsimpl~. } }
......
......@@ -427,6 +427,7 @@ let exp_find_inlined_primitive e oargs =
(* _debug(); *)
begin match args with
| [n; {exp_desc = Texp_constant (Const_int m)}]
when m <> 0
&& List.mem name ["Pervasives.mod"; "Pervasives./"] ->
......@@ -985,8 +986,28 @@ let is_type_abbrev (name,dec) =
let is_type_record (name,dec) =
match dec.typ_type.type_kind with Type_record _ -> true | _ -> false
let rec is_ignored_str_value (pat,exp) =
is_ignored_exp exp
and is_ignored_exp exp =
match exp.exp_desc with
| Texp_constraint (e, _, _) ->
is_ignored_exp e
| Texp_sequence(expr1, expr2) ->
is_ignored_exp expr1
| Texp_function (_, pat_expr_list, _) ->
List.exists is_ignored_str_value pat_expr_list
| Texp_apply ({exp_desc = Texp_ident (f,_d)},
[_, Some {exp_desc = Texp_constant (Const_string "CFML")}, _])
when get_qualified_pervasives_name f = "Pervasives.ignore"
-> true
| _ -> false
(** Generate the top-level Coq declarations associated with
a top-level declaration from a module. *)
a top-level declaration from a module.
If a toplevel definition begins with [ignore "CFML"] in its body,
then the toplevel definition is ignored by CFML altogether. *)
let rec cfg_structure_item s : cftops =
let loc = s.str_loc in
......@@ -994,98 +1015,101 @@ let rec cfg_structure_item s : cftops =
| Tstr_value(rf, fvs, pat_expr_list) ->
reset_local_labels();
(* --todo: improve code sharing between local bindings and top-level bindings *)
let is_let_fun (pat,exp) =
match exp.exp_desc with
| Texp_function (_,_,_) -> true
| Texp_constraint({exp_desc = Texp_function (_,_,_)},_,_) -> true
| _ -> false in
if List.for_all is_let_fun pat_expr_list then begin
let env' = match rf with
| Nonrecursive -> Ident.empty
| Recursive -> Ident.empty
(* --todo: better support for polymorphic recursion
List.fold_left (fun (pat,bod) acc -> Ident.add (pattern_ident pat) 0 acc) env pat_expr_list *)
| Default -> unsupported loc "Default recursion mode"
in
let ncs = List.map (fun (pat,bod) -> (pattern_name_protect_infix pat, cfg_func env' fvs pat bod)) pat_expr_list in
(List.map (fun (name,_) -> Cftop_val (name, func_type)) ncs)
@ (List.map (fun (name,cf_body) -> Cftop_fun_cf (name, cf_body)) ncs)
@ [Cftop_coqs (List.map (fun (name,_) -> register_cf name) ncs)]
(* let-binding of a single value *)
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
(* DEPRECATED if (hack_recognize_okasaki_lazy x) then [] else *)
begin
(* deprecated: pure-mode let-binding
if !pure_mode then begin
let cf_body = cfg_exp (Ident.empty) bod in
let implicits =
match fvs_strict with
| [] -> []
| _ -> [ Coqtop_implicit (x, List.map (fun t -> (t,Coqi_maximal)) fvs_strict) ]
in
[ Cftop_val (x, coq_forall_types fvs_strict typ);
Cftop_coqs implicits;
Cftop_pure_cf (x, fvs_strict, fvs_others, cf_body);
Cftop_coqs [register_cf x]; ]
end else*)
(* value let-binding *)
if Typecore.is_nonexpansive bod then begin
let v =
try lift_val (Ident.empty) bod
with Not_in_normal_form (loc2, s) ->
(* TODO: here and elsewhere, use a wrapper for extending the errors *)
raise (Not_in_normal_form (loc2, s ^ " (only value can satisfy the value restriction)"))
in
let fvs_typ, typ = lift_typ_sch loc pat.pat_type in
let fvs = List.map name_of_type_var (List.filter typvar_is_used fvs) in
if not (list_is_included fvs_typ fvs)
then failwith "fvs_typ not included in fvs for let binding";
let fvs_strict = fvs_typ in
let fvs_others = list_minus fvs fvs_strict in
let v_typed = coq_annot v typ in
let implicits =
match fvs_strict with
| [] -> []
| _ -> [ Coqtop_implicit (x, List.map (fun t -> (t,Coqi_maximal)) fvs_strict) ]
if List.exists is_ignored_str_value pat_expr_list then [] (* ignore *) else begin
(* --todo: improve code sharing between local bindings and top-level bindings *)
let is_let_fun (pat,exp) =
match exp.exp_desc with
| Texp_function (_,_,_) -> true
| Texp_constraint({exp_desc = Texp_function (_,_,_)},_,_) -> true
| _ -> false in
if List.for_all is_let_fun pat_expr_list then begin
let env' = match rf with
| Nonrecursive -> Ident.empty
| Recursive -> Ident.empty
(* --todo: better support for polymorphic recursion
List.fold_left (fun (pat,bod) acc -> Ident.add (pattern_ident pat) 0 acc) env pat_expr_list *)
| Default -> unsupported loc "Default recursion mode"
in
let ncs = List.map (fun (pat,bod) -> (pattern_name_protect_infix pat, cfg_func env' fvs pat bod)) pat_expr_list in
(List.map (fun (name,_) -> Cftop_val (name, func_type)) ncs)
@ (List.map (fun (name,cf_body) -> Cftop_fun_cf (name, cf_body)) ncs)
@ [Cftop_coqs (List.map (fun (name,_) -> register_cf name) ncs)]
(* let-binding of a single value *)
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
(* DEPRECATED if (hack_recognize_okasaki_lazy x) then [] else *)
begin
(* deprecated: pure-mode let-binding
if !pure_mode then begin
let cf_body = cfg_exp (Ident.empty) bod in
let implicits =
match fvs_strict with
| [] -> []
| _ -> [ Coqtop_implicit (x, List.map (fun t -> (t,Coqi_maximal)) fvs_strict) ]
in
[ Cftop_val (x, coq_forall_types fvs_strict typ);
Cftop_coqs implicits;
Cftop_pure_cf (x, fvs_strict, fvs_others, cf_body);
Cftop_coqs [register_cf x]; ]
end else*)
(* value let-binding *)
if Typecore.is_nonexpansive bod then begin
let v =
try lift_val (Ident.empty) bod
with Not_in_normal_form (loc2, s) ->
(* TODO: here and elsewhere, use a wrapper for extending the errors *)
raise (Not_in_normal_form (loc2, s ^ " (only value can satisfy the value restriction)"))
in
[ Cftop_val (x, coq_forall_types fvs_strict typ);
Cftop_coqs implicits;
Cftop_val_cf (x, fvs_strict, fvs_others, v_typed);
Cftop_coqs [register_cf x]; ]
(* term let-binding -- later *)
end else begin
let fvs_typ, typ = lift_typ_sch loc pat.pat_type in
let fvs = List.map name_of_type_var (List.filter typvar_is_used fvs) in
if not (list_is_included fvs_typ fvs)
then failwith "fvs_typ not included in fvs for let binding";
let fvs_strict = fvs_typ in
let fvs_others = list_minus fvs fvs_strict in
let v_typed = coq_annot v typ in
let implicits =
match fvs_strict with
| [] -> []
| _ -> [ Coqtop_implicit (x, List.map (fun t -> (t,Coqi_maximal)) fvs_strict) ]
in
[ Cftop_val (x, coq_forall_types fvs_strict typ);
Cftop_coqs implicits;
Cftop_val_cf (x, fvs_strict, fvs_others, v_typed);
Cftop_coqs [register_cf x]; ]
(* term let-binding -- later *)
end else begin
unsupported loc "top-level binding of terms that are not values";
(* let (fvs_strict, fvs_others, typ) = get_fvs_typ loc fvs pat.pat_type in*)
(* if fvs_strict <> [] || fvs_others <> []
then not_in_normal_form loc ("(unsatisfied value restriction) "
^ (Print_tast.string_of_expression false e));
let cf1 = cfg_exp env bod in
let env' = Ident.add (pattern_ident pat) (List.length fvs_strict) env in
let cf2 = cfg_exp env' body in
add_used_label x;
Cf_let ((x,typ), cf1, cf2) *)
unsupported loc "top-level binding of terms that are not values";
(* let (fvs_strict, fvs_others, typ) = get_fvs_typ loc fvs pat.pat_type in*)
(* if fvs_strict <> [] || fvs_others <> []
then not_in_normal_form loc ("(unsatisfied value restriction) "
^ (Print_tast.string_of_expression false e));
let cf1 = cfg_exp env bod in
let env' = Ident.add (pattern_ident pat) (List.length fvs_strict) env in
let cf2 = cfg_exp env' body in
add_used_label x;
Cf_let ((x,typ), cf1, cf2) *)
end
end