Set Implicit Arguments.
(* LibInt LibWf *)
Require Import CFLib.
Require Import Demo_ml.

Require Import Pervasives_ml. (* optional, improves display of, e.g. [incr] *)

(*Open Scope tag_scope.*)












Lemma if_true_spec : 
  app if_true [tt] \[] \[= 1].
Proof using.
  xcf. xif. xret. xsimpl. auto.
Qed.

Lemma if_term_spec :
  app if_term [tt] \[] \[= 1].
Proof using.
  xcf. xfun. xapp. xret. xextracts.
  xif. xrets~.
Qed.

Lemma if_else_if_spec : 
  app if_else_if [tt] \[] \[= 0].
Proof using.
  xcf. xfun (fun f => forall (x:int), app f [x] \[] \[= false]).
    { xrets~. }
  xapps. xif. xapps. xif. xrets~.
Qed.


Definition Ref a (v:a) (l:loc) :=  (* TODO: change *)
  heap_is_single l v.

Notation "l '~~>' v" := (hdata (Ref v) l)
  (at level 32, no associativity) : heap_scope.

Notation "'app_keep' f xs H Q" :=
  (app f xs H%h (Q \*+ H))
  (at level 80, f at level 0, xs at level 0, H at level 0) : charac.



Parameter ref_spec : forall a (v:a),
  app ref [v] \[] (fun l => l ~~> v).

Parameter get_spec : forall a (v:a) l,
  app_keep get [l] (l ~~> v) \[= v].
(* Print get_spec. *)
(* keep (app get [l]) (l ~~> v) \[= v].*)

Parameter set_spec : forall a (v w:a) l,
  app set [l w] (l ~~> v) (# l ~~> w).

Parameter incr_spec : forall (n:int) l,
  app incr [l] (l ~~> n) (# l ~~> (n+1)).

Parameter decr_spec : forall (n:int) l,
  app decr [l] (l ~~> n) (# l ~~> (n+1)).


Hint Extern 1 (RegisterSpec ref) => Provide ref_spec.
Hint Extern 1 (RegisterSpec get) => Provide get_spec.
Hint Extern 1 (RegisterSpec set) => Provide set_spec.
Hint Extern 1 (RegisterSpec incr) => Provide incr_spec.
Hint Extern 1 (RegisterSpec decr) => Provide decr_spec.





Notation "`! l" := (App infix_emark_ l;)
  (at level 69, no associativity, format "`! l") : machine_op_scope.


Lemma if_then_no_else_spec : forall (b:bool),
  app if_then_no_else [b] \[] \[= 1].
Proof using.
  xcf. xapp. dup 3.
  { xseq. xif. { xapp. } { xrets. skip. (* stuck *) } skip. } 
  { xseq....

  (* TODO: raise error message on xif *)
Qed.



(********************************************************************)
(********************************************************************)
(********************************************************************)


(********************************************************************)
(* ** Top-level values *)

Lemma top_val_int_spec :
  top_val_int = 5.
Proof using.
  dup 5.
  xcf. auto.
  (* demos: *)
  xcf_show. skip.
  xcf_show top_val_int. skip. 
  xcf. skip.
  xcf top_val_int. skip.
Qed.

Lemma top_val_int_list_spec : 
  top_val_int_list = @nil int.
Proof using.
  xcf. auto.
Qed.

Lemma top_val_poly_list_spec : forall A,
  top_val_poly_list = @nil A.
Proof using. xcf*. Qed.

Lemma top_val_poly_list_pair_spec : forall A B,
  top_val_poly_list_pair = (@nil A, @nil B).
Proof using. xcf*. Qed.



(********************************************************************)
(* ** Return *)

Lemma ret_unit_spec : 
  app ret_unit [tt] \[] \[= tt]. (* (fun (_:unit) => \[]).*) (* same as (# \[]). *)
Proof using.
  xcf. dup 5.
  xret. xsimpl. auto.
  (* demos *)
  xrets. auto.
  xrets*.
  xret_no_gc. xsimpl. auto.
  xret_no_clean. xsimpl*. 
Qed.

Lemma ret_int_spec : 
  app ret_int [tt] \[] \[= 3].
Proof using. xcf. xrets*. Qed.

Lemma ret_int_pair_spec :
  app ret_int_pair [tt] \[] \[= (3,4)].
Proof using. xcf. xrets*. Qed.

Lemma ret_poly_spec : forall A,
  app ret_poly [tt] \[] \[= @nil A].
Proof using. xcf. xrets*. Qed.


(********************************************************************)
(* ** Sequence *)

Axiom ret_unit_spec' : forall A (x:A),
  app ret_unit [x] \[] \[= tt]. (* (fun (_:unit) => \[]).*) (* same as (# \[]). *)

Hint Extern 1 (RegisterSpec ret_unit) => Provide ret_unit_spec'.

Lemma seq_ret_unit_spec :
  app seq_ret_unit [tt] \[] \[= tt].
Proof using.
  xcf.
  (* xlet. -- make sure we get a good error here *)
  xseq.
  xapp1.
  xapp2.
  dup 3. 
  { xapp3_no_apply. apply S. }
  { xapp3_no_simpl. }
  { xapp3. }
  dup 4.
  { xseq. xapp. xapp. xsimpl~. }
  { xapp. intro_subst. xapp. xsimpl~. }
  { xapps. xapps. xsimpl~. }
  { xapps. xapps~. }
Qed.



(********************************************************************)
(* ** Let-value *)

Lemma let_val_int_spec : 
  app let_val_int [tt] \[] \[= 3].
Proof using.
  xcf. dup 7.
  xval. xrets~.
  (* demos *)
  xval as r. xrets~.
  xval as r Er. xrets~.
  xvals. xrets~.
  xval_st (= 3). auto. xrets~.
  xval_st (= 3) as r. auto. xrets~.
  xval_st (= 3) as r Er. auto. xrets~.
Qed.

Lemma let_val_pair_int_spec :
  app let_val_pair_int [tt] \[] \[= (3,4)].
Proof using. xcf. xvals. xrets*. Qed.

Lemma let_val_poly_spec :
  app let_val_poly [tt] \[] \[= 3].
Proof using.
  xcf. dup 3.
  xval. xret. xsimpl. auto.
  xval as r. xrets~.
  xvals. xrets~.
Qed.


(********************************************************************)
(* ** Let-function *)

Lemma let_fun_const_spec : 
  app let_fun_const [tt] \[] \[= 3].
Proof using.
  xcf. dup 9.
  { xfun. apply Sf. xrets~. }
  { xfun as g. apply Sg. skip. }
  { xfun as g G. apply G. skip. }
  { xfun_no_simpl (fun g => app g [tt] \[] \[=3]).
    { apply Sf. skip. } 
    { apply Sf. } }
  { xfun_no_simpl (fun g => app g [tt] \[] \[=3]) as h.
    { apply Sh. skip. } 
    { apply Sh. } }
  { xfun_no_simpl (fun g => app g [tt] \[] \[=3]) as h H.
    { apply H. skip. } 
    { apply H. } }
  { xfun (fun g => app g [tt] \[] \[=3]).
    { xrets~. } 
    { apply Sf. } }
  { xfun (fun g => app g [tt] \[] \[=3]) as h.
    { skip. } 
    { skip. } }
  { xfun (fun g => app g [tt] \[] \[=3]) as h H.
    { skip. } 
    { skip. } }
Qed.

Lemma let_fun_poly_id_spec :
  app let_fun_poly_id [tt] \[] \[= 3].
Proof using.
  xcf. xfun. dup 2.
  { xapp. xret. xsimpl~. }
  { xapp1.
    xapp2.
    dup 5. 
    { apply Spec. xret. }
    { xapp3_no_apply. Focus 2. apply S. xret. }
    { xapp3_no_simpl. xret. }
    { xapp3. xret. }
    { xapp. xret. xsimpl~. }
    xsimpl~.
Qed.

Lemma let_fun_poly_pair_homogeneous_spec : 
  app let_fun_poly_pair_homogeneous [tt] \[] \[= (3,3)].
Proof using.
  xcf. 
  xfun.
  xapp. 
  xret.
  xsimpl~.
Qed.

Lemma let_fun_on_the_fly_spec :
  app let_fun_on_the_fly [tt] \[] \[= 4].
Proof using.
  xcf.
  xfun.
  xfun.
  xapp. 
  xapp.
  xret.
  xsimpl~.
Qed.


(********************************************************************)
(* ** Let-term *)

Lemma let_term_nested_id_calls_spec :
  app let_term_nested_id_calls [tt] \[] \[= 2].
Proof using.
  xcf.
  xfun (fun f => forall (x:int), app f [x] \[] \[= x]). { xret~. }
  xapps. 
  xapps.
  xapps.
  xrets~.
Qed.

Lemma let_term_nested_pairs_calls_spec :
  app let_term_nested_pairs_calls [tt] \[] \[= ((1,2),(3,(4,5))) ].
Proof using.
  xcf. 
  xfun (fun f => forall A B (x:A) (y:B), app f [x y] \[] \[= (x,y)]). { xret~. }
  xapps.
  xapps.
  xapps.
  xapps.
  xrets~.
Qed.

(********************************************************************)
(* ** Pattern-matching *)

Lemma match_pair_as_spec : 
  app match_pair_as [tt] \[] \[= (4,(3,4))].
Proof using.
  xcf. dup 8.
  { xmatch. xrets*. }
  { xmatch_subst_alias. xrets*. }
  { xmatch_no_alias. xalias. xalias as L. skip. }
  { xmatch_no_cases. dup 6. 
    { xmatch_case.
      { xrets~. } 
      { xmatch_case. } }
    { xcase_no_simpl.
      { dup 3.
        { xalias. xalias. xret. xsimpl. xauto*. }
        { xalias as u U. 
          xalias as v. skip. }
        { xalias_subst. xalias_subst. skip. } }
      { xdone. } } 
    { xcase_no_simpl as E. skip. skip. }
    { xcase_no_intros. intros x y E. skip. intros F. skip. }
    { xcase. skip. skip. }
    { xcase as C. skip. skip. 
      (* note: inversion got rid of C *) 
    } }
  { xmatch_no_simpl_no_alias. skip. }
  { xmatch_no_simpl_subst_alias. 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.
  xcf. xval. dup 3.
  { xmatch_no_simpl.  
    { xrets~. } 
    { false. (* note: [xrets] would produce a ununified [hprop]. 
     caused by [tryfalse] in [hextract_cleanup]. TODO: avoid this. *) } }
  { xmatch.
    xrets~. 
    (* second case is killed by [xcase_post] *) }
  { xmatch_no_intros. skip. skip. }
Qed.


(********************************************************************)
(* ** Let-pattern *)

Lemma let_pattern_pair_int_spec : 
  app let_pattern_pair_int [tt] \[] \[= 3].
Proof using. xcf. xmatch. xrets~. Qed.

Lemma let_pattern_pair_int_wildcard_spec :
  app let_pattern_pair_int_wildcard [tt] \[] \[= 3].
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.


(********************************************************************)
(* ** 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 inlined_fun_other_spec : forall (n:int),
  app inlined_fun_others [n] \[] \[= n+1].
Proof using.
  xcf. xret. xsimpl. simpl. auto.
Qed.




(********************************************************************)
(********************************************************************)
(********************************************************************)

(*


(********************************************************************)
(* ** Partial applications *)

Lemma app_partial_2_1 () =
   let f x y = (x,y) in
   f 3
Proof using.
  xcf.
Qed.

Lemma app_partial_3_2 () =
   let f x y z = (x,z) in
   f 2 4
Proof using.
  xcf.
Qed.

Lemma app_partial_add () =
  let add x y = x + y in
  let g = add 1 in g 2
Proof using.
  xcf.
Qed.

Lemma app_partial_appto () =
  let appto x f = f x in
  let _r = appto 3 ((+) 1) in
  appto 3 (fun x -> x + 1)
Proof using.
  xcf.
Qed.

Lemma test_partial_app_arities () =
   let func4 a b c d = a + b + c + d in
   let f1 = func4 1 in
   let f2 = func4 1 2 in
   let f3 = func4 1 2 3 in
   f1 2 3 4 + f2 3 4 + f3 4
Proof using.
  xcf.
Qed.

Lemma app_partial_builtin () =
  let f = (+) 1 in
  f 2
Proof using.
  xcf.
Qed.


let app_partial_builtin_and () =
  let f = (&&) true in
  f false




(********************************************************************)
(* ** Over applications *)

Lemma app_over_id () =
   let f x = x in
   f f 3
Proof using.
  xcf.
Qed.




(********************************************************************)
(* ** Polymorphic functions *)



Lemma top_fun_poly_id : forall A (x:A),
  app top_fun_poly_id [x] \[] \[= x].  (* (fun r => \[r = x]). *)
Proof using.
  xcf.
Qed.

Lemma top_fun_poly_proj1 : forall A B (x:A) (y:B),
  app top_fun_poly_proj1 [(x,y)] \[] \[= x]
Proof using.
  xcf.
Qed.

Lemma top_fun_poly_proj1' : forall A B (p:A*B),
  app top_fun_poly_proj1 [p] \[] \[= fst x]. (* (fun r => \[r = fst x]).  *)
Proof using.
  xcf.
Qed.

Lemma top_fun_poly_pair_homogeneous : forall A (x y : A), 
  app top_fun_poly_pair_homogeneous [x y] \[] \[= (x,y)]. 
Proof using.
  xcf.
Qed.


(********************************************************************)
(* ** Polymorphic let bindings *)

Lemma let_poly_nil () = 
  let x = [] in x
Proof using.
  xcf.
Qed.

Lemma let_poly_nil_pair () = 
  let x = ([], []) in x
Proof using.
  xcf.
Qed.

Lemma let_poly_nil_pair_homogeneous () =
  let x : ('a list * 'a list) = ([], []) in x
Proof using.
  xcf.
Qed.

Lemma let_poly_nil_pair_heterogeneous () =
  let x : ('a list * int list) = ([], []) in x
Proof using.
  xcf.
Qed.


*)


(********************************************************************)
(********************************************************************)
(********************************************************************)
(* TODO: xgc demo *)


(********************************************************************)
(********************************************************************)
(********************************************************************)
(*


(********************************************************************)
(* ** Fatal Exceptions *)

Lemma exn_assert_false () =
   assert false
Proof using.
  xcf.
Qed.

Lemma exn_failwith () =
   failwith "ok"
Proof using.
  xcf.
Qed.

exception My_exn 

Lemma exn_raise () =
   raise My_exn
Proof using.
  xcf.
Qed.


(********************************************************************)
(* ** Assertions *)

Lemma assert_true () =
  assert true; 3
Proof using.
  xcf.
Qed.

Lemma assert_pos x =
  assert (x > 0); 3
Proof using.
  xcf.
Qed.

Lemma assert_same (x:int) (y:int) =
  assert (x = y); 3
Proof using.
  xcf.
Qed.



(********************************************************************)
(* ** Conditionals *)



(********************************************************************)
(* ** Records *)

type 'a sitems = {
  mutable nb : int;
  mutable items : 'a list; }

Lemma sitems_build n =
  { nb = n; items = [] }
Proof using.
  xcf.
Qed.

Lemma sitems_get_nb r =
  r.nb
Proof using.
  xcf.
Qed.

Lemma sitems_incr_nb r =
  r.nb <- r.nb + 1 
Proof using.
  xcf.
Qed.

Lemma sitems_length_items r =
  List.length r.items
Proof using.
  xcf.
Qed.

Lemma sitems_push x r =
  r.nb <- r.nb + 1;
  r.items <- x :: r.items
Proof using.
  xcf.
Qed.


(********************************************************************)
(* ** Arrays *)

Lemma array_ops () =
  let t = Array.make 3 0 in
  let _x = t.(1) in
  t.(2) <- 4;
  let _y = t.(2) in
  let _z = t.(1) in
  Array.length t
Proof using.
  xcf.
Qed.


(********************************************************************)
(* ** While loops *)

Lemma while_decr () =
   let n = ref 3 in
   let c = ref 0 in
   while !n > 0 do 
      incr c;
      decr n;
   done;
   !c
Proof using.
  xcf.
Qed.

Lemma while_false () =
   while false do () done
Proof using.
  xcf.
Qed.


(********************************************************************)
(* ** For loops *)

Lemma for_incr () =
   let n = ref 0 in
   for i = 1 to 10 do
      incr n;
   done;
   !n

(* "for .. down to" not yet supported *)
Proof using.
  xcf.
Qed.


(********************************************************************)
(* ** Recursive function *)

Lemma rec rec_partial_half x =
  if x = 0 then 0
  else if x = 1 then assert false
  else 1 + rec_partial_half(x-2)
Proof using.
  xcf.
Qed.



let rec rec_mutual_f x =
  if x <= 0 then x else 1 + rec_mutual_g (x-2)
and rec rec_mutual g x =
  rec_mutual_f (x+1)
*)


(********************************************************************)
(* ** Lazy binary operators 

let lazyop_val () =
  if true && (false || true) then 1 else 0

let lazyop_term () =
  let f x = (x = 0) in
  if f 1 || f 0 then 1 else 0

let lazyop_mixed () =
  let f x = (x = 0) in
  if true && (f 1 || (f 0 && true)) then 1 else 0

*)


(* TODO: include demo of  xpost (fun r =>\[r = 3]). *)


(********************************************************************)
(* ** Evaluation order 

let order_app () =
  let r = ref 0 in
  let f () = incr r; 1 in
  let g () = assert (!r = 1); 1 in
  g() + f()

let order_constr () =
  let r = ref 0 in
  let f () = incr r; 1 in
  let g () = assert (!r = 1); 1 in
  (g() :: f() :: nil)

let order_array () =
  let r = ref 0 in
  let f () = incr r; 1 in
  let g () = assert (!r = 1); 1 in
  [| g() ; f() |]

let order_list () =
  let r = ref 0 in
  let f () = incr r; 1 in
  let g () = assert (!r = 1); 1 in
  [ g() ; f() ]

let order_tuple () =
  let r = ref 0 in
  let f () = incr r; 1 in
  let g () = assert (!r = 1); 1 in
  (g(), f())

let order_record () =
  let r = ref 0 in
  let g () = incr r; [] in
  let f () = assert (!r = 1); 1 in
  { nb = f(); items = g() }
*)



(*************************************************************************)
(*************************************************************************)
(*************************************************************************)
(** * Polymorphic let demos


(** Demo top-level polymorphic let. *)

Lemma poly_top_spec : forall A,
  poly_top = @nil A.
Proof using. xcf. Qed.

(** Demo local polymorphic let. *)

Lemma poly_let_1_spec : forall A,
  Spec poly_let_1 () |B>>
    B \[] (fun (x:list A) => \[x = nil]).
Proof using. xcf. xval. subst. xrets. auto. Qed.  

(** Demo [xval_st P] *)

Lemma poly_let_1_spec' : forall A,
  Spec poly_let_1 () |B>>
    B \[] (fun (x:list A) => \[x = nil]).
Proof using. xcf. xval_st (fun a => a = @nil). extens~. xrets. subst~. Qed.

(** Demo [xval_st P as x Hx] *)

Lemma poly_let_1_spec'' : forall A,
  Spec poly_let_1 () |B>>
    B \[] (fun (x:list A) => \[x = nil]).
Proof using. xcf. xval_st (fun a => a = @nil) as p Hp. extens~. xrets. subst~. Qed.

(** Demo for partially-polymorphic values. *)

Lemma poly_let_2_spec : forall A1 A2,
  Spec poly_let_2 () |B>>
    B \[] (fun '(x,y) : list A1 * list A2 => \[x = nil /\ y = nil]).
Proof using. intros. xcf. xvals. xrets. auto. Qed.

Lemma poly_let_2_same_spec : forall A,
  Spec poly_let_2_same () |B>>
    B \[] (fun '(x,y) : list A * list A => \[x = nil /\ y = nil]).
Proof using. intros. xcf. xvals. xrets. auto. Qed.

Lemma poly_let_2_partial_spec : forall A,
  Spec poly_let_2_partial () |B>>
    B \[] (fun '(x,y) : list A * list int => \[x = nil /\ y = nil]).
Proof using. intros. xcf. xval as p Hp. subst p. xrets. auto. Qed.
 *)