Commit 8c59b322 authored by charguer's avatar charguer

xapp_skip

parent 4e4d805f
(************************************************************)
(** Exception *)
external raise : exn -> 'a = "%raise"
external failwith : string -> 'a = "%failwith"
(************************************************************)
(** Type conversion *)
external magic : 'a -> 'b = "%magic"
(************************************************************)
(** Boolean *)
let not x =
if x then false else true
(************************************************************)
(** Physical equality *)
external physical_eq : 'a -> 'a -> bool = "%physical_eq"
let ( == ) = physical_eq
let physical_neq x y =
not (x == y)
let ( !== ) = physical_neq
(************************************************************)
(** Comparison *)
external compare_eq : 'a -> 'a -> bool = "%compare_eq"
external compare_neq : 'a -> 'a -> bool = "%compare_neq"
external compare_lt : 'a -> 'a -> bool = "%compare_lt"
external compare_gt : 'a -> 'a -> bool = "%compare_gt"
external compare_le : 'a -> 'a -> bool = "%compare_le"
external compare_ge : 'a -> 'a -> bool = "%compare_ge"
let ( = ) = compare_eq
let ( <> ) = compare_neq
let ( < ) = compare_lt
let ( > ) = compare_gt
let ( <= ) = compare_le
let ( >= ) = compare_ge
let min x y =
if x <= y then x else y
let max x y =
if x >= y then x else y
(************************************************************)
(** Boolean *)
external bool_and : bool -> bool -> bool = "%bool_and"
external bool_or : bool -> bool -> bool = "%bool_or"
let ( && ) = bool_and
let ( || ) = bool_or
(************************************************************)
(** Integer *)
external int_neg : int -> int = "%int_neg"
external int_add : int -> int -> int = "%int_add"
external int_sub : int -> int -> int = "%int_sub"
external int_mul : int -> int -> int = "%int_mul"
external int_div : int -> int -> int = "%int_div"
external int_mod : int -> int -> int = "%int_mod"
let ( ~- ) = int_neg
let ( + ) = int_add
let ( - ) = int_sub
let ( * ) = int_mul
let ( / ) = int_div
let ( mod ) = int_mod
let succ n =
n + 1
let pred n =
n - 1
let abs x =
if x >= 0 then x else -x
(************************************************************)
(** References *)
type 'a ref = { mutable contents : 'a }
let ref x =
{ contents = x }
let get r =
r.contents
let (!) = get
let set r x =
r.contents <- x
let (:=) = set
let incr r =
r := !r + 1
let decr r =
r := !r - 1
(** [ref_free r] is a logical free operation, useful for translating
to languages without garbage collection *)
let ref_free r =
()
(** [ref_unsafe_set r x] allows to modifies the contents of a reference *)
(* unsupported currently, needs explicit types
let ref_unsafe_set r x =
r.contents <- (magic x)
*)
(************************************************************)
(** Pairs *)
let fst (x,y) =
x
let snd (x,y) =
y
(************************************************************)
(** Unit *)
let ignore x =
()
......@@ -140,7 +140,7 @@ let app_over_id () =
let (+++) x y = x + y
let infix_aux x y = x + y
let infix_aux x y = x +++ y
let (---) = infix_aux
......@@ -148,8 +148,14 @@ let (---) = infix_aux
(********************************************************************)
(* ** Inlined total functions *)
let f () =
1 - 1/(-1) + (2 / 2) mod 3
let inlined_fun_arith () =
let n = 2 in
1 - (1 / n) + ((2 * 2) / 2) mod (- 3)
let inlined_fun_others n =
fst (succ n, ignore (pred n))
(********************************************************************)
......
Set Implicit Arguments.
Require Import LibTactics CFHeaps (* LibInt LibWf *).
Require Import Demo_ml.
(* LibInt LibWf *).
Require Import CFLib.
Require Import Demo_ml.
(*Open Scope tag_scope.*)
Open Scope tag_scope.
(********************************************************************)
(* ** Inlined total functions *)
Lemma inlined_fun_arith_spec :
app inlined_fun_arith [tt] \[] \[= 3].
Proof using.
xcf.
xval.
xlet.
(* note: division by a possibly-null constant is not inlined *)
xapp_skip.
xrets.
skip.
Qed.
Lemma if_true () =
if true then 1 else 0
Proof using.
xcf.
Qed.
Lemma if_term () =
let f x = true in
if f 0 then 1 else 0
Proof using.
xcf.
Qed.
Lemma if_else_if () =
let f x = false in
if f 0 then 1
else if f 1 then 2
else 0
Proof using.
xcf.
Qed.
Lemma if_then_no_else b =
let r = ref 0 in
if b
then incr r;
!r
Proof using.
xcf.
Qed.
(********************************************************************)
(********************************************************************)
(********************************************************************)
......@@ -239,7 +288,10 @@ Proof using.
{ xmatch. xrets*. }
{ xmatch_subst_alias. xrets*. }
{ xmatch_no_alias. xalias. xalias as L. skip. }
{ xmatch_no_cases. dup 5.
{ xmatch_no_cases. dup 6.
{ xmatch_case.
{ xrets~. }
{ xmatch_case. } }
{ xcase_no_simpl.
{ dup 3.
{ xalias. xalias. xret. xsimpl. xauto*. }
......@@ -255,11 +307,10 @@ Proof using.
} }
{ xmatch_no_simpl_no_alias. skip. }
{ xmatch_no_simpl_subst_alias. skip. }
{ xmatch_no_intros. skip. skip. }
{ xmatch_no_intros. skip. }
{ xmatch_no_simpl. inverts C. skip. }
Qed.
Lemma match_nested_spec :
app match_nested [tt] \[] \[= (2,2)::nil].
Proof using.
......@@ -287,6 +338,30 @@ Lemma let_pattern_pair_int_wildcard_spec :
Proof using. xcf. xmatch. xrets~. Qed.
(********************************************************************)
(* ** Infix functions *)
Lemma infix_plus_plus_plus__spec : forall x y,
app infix_plus_plus_plus_ [x y] \[] \[= x + y].
Proof using.
xcf. xrets~.
Qed.
Hint Extern 1 (RegisterSpec infix_plus_plus_plus_) => Provide infix_plus_plus_plus__spec.
Lemma infix_aux_spec : forall x y,
app infix_aux [x y] \[] \[= x + y].
Proof using.
xcf. xapps~.
Qed.
Hint Extern 1 (RegisterSpec infix_aux) => Provide infix_aux_spec.
Lemma infix_minus_minus_minus__spec : forall x y,
app infix_minus_minus_minus_ [x y] \[] \[= x + y].
Proof using.
intros. xcf_show as S. rewrite S. xapps~.
Qed.
......@@ -297,9 +372,6 @@ Proof using. xcf. xmatch. xrets~. Qed.
(*
(********************************************************************)
(* ** Partial applications *)
......@@ -350,7 +422,6 @@ Proof using.
Qed.
(********************************************************************)
(* ** Over applications *)
......@@ -361,34 +432,6 @@ Proof using.
xcf.
Qed.
(********************************************************************)
(* ** Infix functions *)
Lemma (+++) x y = x + y
Proof using.
xcf.
Qed.
Lemma infix_aux x y = x + y
Proof using.
xcf.
Qed.
Lemma (---) = infix_aux
Proof using.
xcf.
Qed.
(********************************************************************)
(* ** Inlined total functions *)
Lemma f () =
1 - 1/(-1) + (2 / 2) mod 3
Proof using.
xcf.
Qed.
......@@ -515,36 +558,6 @@ Qed.
(********************************************************************)
(* ** Conditionals *)
Lemma if_true () =
if true then 1 else 0
Proof using.
xcf.
Qed.
Lemma if_term () =
let f x = true in
if f 0 then 1 else 0
Proof using.
xcf.
Qed.
Lemma if_else_if () =
let f x = false in
if f 0 then 1
else if f 1 then 2
else 0
Proof using.
xcf.
Qed.
Lemma if_then_no_else b =
let r = ref 0 in
if b
then incr r;
!r
Proof using.
xcf.
Qed.
(********************************************************************)
......@@ -657,7 +670,7 @@ Qed.
(* TODO: include demo of xpost (fun r =>\[r = 3]). *)
......
......@@ -350,7 +350,7 @@ let exp_find_inlined_primitive e oargs =
let args = simplify_apply_args oargs in
match e.exp_desc, args with
| Texp_ident (f,d), [n; {exp_desc = Texp_constant (Const_int m)}]
when m > 0 && let x = Path.name f in x = "Pervasives.mod" || x = "Pervasives./" ->
when m <> 0 && let x = Path.name f in x = "Pervasives.mod" || x = "Pervasives./" ->
find_inlined_primitive (Path.name f) primitive_special
| Texp_ident (f,d), _ ->
let r = find_inlined_primitive (Path.name f) (List.length args) in
......@@ -864,7 +864,7 @@ let rec cfg_structure_item s : cftops =
[ Cftop_coqs [ Coqtop_require_import [ lift_full_path_name path ] ] ]
| Tstr_primitive(id, descr) ->
let id = Ident.name id in
let id = protect_infix (Ident.name id) in
let fvs, typ = lift_typ_sch descr.val_desc.ctyp_type in
let typ = coq_fun_types fvs typ in
[ Cftop_val (id, typ) ]
......
......@@ -159,8 +159,12 @@ let rec coqtops_of_imp_cf cf =
/\ ((forall x1, x <> p [\/ trueb !w]) -> F2 H Q)))
where trueb are implicit by coercions *)
| Cf_match (label, n,cf1) ->
coq_tag "tag_match" ~args:[Coq_var (Printf.sprintf "%d%s" n "%nat")] (*~label:label*) (coq_of_cf cf1)
| Cf_match (label, n, cf1) ->
let f = Coq_app (Coq_var "CFML.CFHeaps.local", (coq_of_cf cf1)) in
coq_tag "tag_match" f
(* DEPRECATED
coq_tag "tag_match" ~args:[Coq_var (Printf.sprintf "%d%s" n "%nat")] (coq_of_cf cf1)
*) (*~label:label*)
| Cf_seq (cf1,cf2) ->
let q' = Coq_var "Q'" in
......
......@@ -34,11 +34,14 @@ let is_inlined_primitive e largs =
let args = List.map snd largs in (* todo: check no labels*)
match e.pexp_desc, args with
| 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 (fullname_of_lident f) primitive_special
(* URGENT:
we could maybe reject programs that rebind these operators,
else it seems we need to have the typed tree in order to normalize...
-- 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 ("Pervasives." ^ fullname_of_lident f) primitive_special
| Pexp_ident f,_ ->
is_inlined_primitive (fullname_of_lident f) (List.length args)
is_inlined_primitive ("Pervasives." ^ fullname_of_lident f) (List.length args)
| _ -> false
let is_failwith_function e =
......
......@@ -109,19 +109,25 @@ let primitive_special = -1
val primitive_special : int
*)
(* URGENT : support lazy operators! *)
(* URGENT : support comparison operators on base types! *)
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.not", (1, "LibBool.neg");
"Pervasives.fst", (1, "(@Coq.Init.Datatypes.fst _ _)");
"Pervasives.snd", (1, "(@Coq.Init.Datatypes.snd _ _)");
"Pervasives.pred", (primitive_special, "CFML.CFHeader.pred");
"Pervasives.succ", (primitive_special, "CFML.CFHeader.succ");
"Pervasives./", (primitive_special, "CFML.CFHeader.int_div");
"Pervasives.mod", (primitive_special, "CFML.CFHeader.int_mod");
"Pervasives.ignore", (primitive_special, "CFML.CFHeader.ignore");
"Pervasives.&&", (2, "LibBool.and");
"Pervasives.||", (2, "LibBool.or");
(*
"Pervasives./", (primitive_special, "Coq.ZArith.Zdiv.Zdiv");
"Pervasives.mod", (primitive_special, "Coq.ZArith.Zdiv.Zmod");
*)
(*
(* TODO (but only for some types):
"Pervasives.=", (2, "(fun _y _z => isTrue (_y = _z))");
"Pervasives.<>", (2, "(fun _y _z => isTrue (_y <> _z))");
"Pervasives.<", (2, "(fun _y _z => isTrue (_y < _z))");
......@@ -130,9 +136,11 @@ let inlined_primitives_table =
"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.abs", (1, "...");
*)
]
(* DEPRECATED
"Pervasives.@", (2, "LibList.append");
"List.rev", (1, "LibList.rev");
"List.length", (1, "LibList.length");
......@@ -143,8 +151,6 @@ let inlined_primitives_table =
"Lazy.force", (1, "");
"Okasaki.!$", (1, ""); (* i.e., @LibLogic.id _*)
*)
]
......@@ -383,35 +389,46 @@ let cf_axiom_name name =
(* ** Renaming of infix function names, and special names *)
(* TODO: rename "infix" into something more general *)
(** Auxiliary function for encoding infix function names *)
(** [infix_name_encode name] encodes an infix function name,
e.g. for "+^+" it produces "infix_plus_hat_plus_". *)
let infix_name_symbols =
['!', 'a';
'$', 'b';
'%', 'c';
'&', 'd';
'*', 'e';
'+', 'f';
'-', 'g';
'.', 'h';
'/', 'i';
':', 'j';
'<', 'k';
'=', 'l';
'>', 'm';
'?', 'n';
'@', 'o';
'^', 'p';
'|', 'q';
'~', 'r';
'>', 's'] (* why was ">" not in the list? TODO *)
['!', "emark";
'$', "dollar";
'%', "percent";
'&', "amp";
'*', "star";
'+', "plus";
'-', "minus";
'.', "dot";
'/', "slash";
':', "column";
'<', "lt";
'=', "eq";
'>', "gt";
'?', "qmark";
'@', "at";
'^', "hat";
'|', "bar";
'~', "tilde" ]
let infix_name_encode name =
let gen = Buffer.create 20 in
String.iter (fun c ->
let s =
try List.assoc c infix_name_symbols
with Not_found -> failwith ("infix_name_encode: cannot encode name: " ^ name)
in
Buffer.add_string gen s;
Buffer.add_string gen "_";
) name;
"infix_" ^ (Buffer.contents gen)
(*DEPRECATED
let gen = String.map (fun c ->
try List.assoc c infix_name_symbols
with Not_found -> failwith ("infix_name_encode: cannot encode name: " ^ name))
name in
"infix_" ^ gen ^ "_"
name in *)
(** Convention for renaming infix function names *)
......
Require Export CFPrint.
Require Coq.ZArith.BinInt.
Local Notation "'int'" := (Coq.ZArith.BinInt.Z).
(********************************************************************)
(* Direct functions to map inlined primitives from Pervasives,
that are not already mapped to existing Coq constants.
(see inlined_primitives_table in renaming.ml) *)
(** Arithmetic of integers *)
(* TODO: define and specify *)
Axiom int_mod : int -> int -> int.
Axiom int_div : int -> int -> int.
(** Pred / Succ *)
Definition pred (n:int) := (Coq.ZArith.BinInt.Zminus n 1).
Definition succ (n:int) := (Coq.ZArith.BinInt.Zplus n 1).
(** Ignore *)
Definition ignore A (x:A) := tt.
(********************************************************************)
(* Preventing simplifications *)
Global Opaque
Coq.ZArith.BinInt.Zplus
Coq.ZArith.BinInt.Zminus
Coq.ZArith.BinInt.Zmult
Coq.ZArith.BinInt.Zopp.
Require Export CFHeader CFTactics.
Require Export LibTactics CFHeaps CFHeader CFTactics.
Open Scope heap_scope.
Notation "x `/` y" := (int_div x y) (at level 69) : machine_op_scope.
Notation "x `mod` y" := (int_mod x y) (at level 69) : machine_op_scope.
(* TODO: check levels for these notations *)
Open Scope machine_op_scope.
......@@ -20,7 +20,7 @@ Inductive tag_type : Type :=
| tag_fun
| tag_let
| tag_app_curried
| tag_match (n : nat)
| tag_match (* DEPRECATED (n : nat) *)
| tag_case
| tag_casewhen
| tag_alias
......@@ -121,8 +121,12 @@ Notation "'!Let' P" := (tag tag_let (local P))
Notation "'!AppCurried' P" := (tag tag_app_curried P)
(at level 95) : tag_scope.
(* DEPRECATED
Notation "'!Match' n P" := (tag (tag_match n) P)
(at level 95, n at level 0).
*)
Notation "'!Match' P" := (tag tag_match (local P))
(at level 95).
Notation "'!Case' P" := (tag tag_case (local P))
(at level 95) : tag_scope.
Notation "'!CaseWhen' P" := (tag tag_casewhen (local P))
......@@ -624,9 +628,15 @@ Notation "'Case' x '=' p [ x1 x2 x3 x4 x5 x6 x7 ] 'When' w 'Then' F1 'Else' F2"
(********************************************************************)
(** Match *)
(* DEPRECATED
Notation "'Match' n Q" :=
(!Match n Q)
(at level 69, n at level 0) : charac.
*)
Notation "'Match' Q" :=
(!Match Q)
(at level 69) : charac.
(********************************************************************)
......
......@@ -1905,6 +1905,7 @@ Tactic Notation "xcase_no_intros" :=
xcase_no_intros_core ltac:(fun _ => idtac) ltac:(fun _ => idtac).
(*--------------------------------------------------------*)
(* ** [xmatch] *)
......@@ -1930,7 +1931,8 @@ Tactic Notation "xcase_no_intros" :=
and introduces and substitutes all aliases.
- [xmatch_no_cases] simply remove the [Match] tag and
leaves the cases to be solved manually using [xcase].
leaves the cases to be solved manually using
[xmatch_case] or [xcase]/[xfail]/[xdone] tactics directly.
- [xmatch_clean] is a shorthand for [xmatch; xcleanpat]:
it does not keep the negation of the patterns as hypotheses
......@@ -1938,11 +1940,11 @@ Tactic Notation "xcase_no_intros" :=
- [xmatch_no_intros] is like [xmatch], but does not
perform any name introduction or any inversion.