(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the GNU General Public License as published by  *)
(*  the Free Software Foundation, either version 2 of the License, or  *)
(*  (at your option) any later version.  This file is also distributed *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(* * This file defines a number of data types and operations used in
  the abstract syntax trees of many of the intermediate languages. *)

include "basics/types.ma".
include "common/Integers.ma".
include "common/Floats.ma".
include "ASM/Arithmetic.ma".
include "common/Identifiers.ma".


(* * * Syntactic elements *)

(* Global variables and functions are represented by identifiers with the
   tag for symbols.  Note that Clight also uses them for locals due to
   the ambiguous syntax. *)

axiom SymbolTag : String.

definition ident ≝ identifier SymbolTag.

definition ident_eq : ∀x,y:ident. (x=y) + (x≠y) ≝ identifier_eq ?.

definition ident_of_nat : nat → ident ≝ identifier_of_nat ?.

definition Immediate ≝ nat. (* XXX is this the best place to put this? *)

(* dpm: not needed
inductive quantity: Type[0] ≝
  | q_int: Byte → quantity
  | q_offset: quantity
  | q_ptr: quantity.
  
inductive abstract_size: Type[0] ≝
  | size_q: quantity → abstract_size
  | size_prod: list abstract_size → abstract_size
  | size_sum: list abstract_size → abstract_size
  | size_array: nat → abstract_size → abstract_size.
*)


(* Memory spaces

   For full 8051 memory spaces support we have internal memory pointers,
   PData pointers which are 8 bit pointers to the first page of XData, and
   a tagged Any pointer for any of the spaces.
   
   We only support the 16 bit XData and Code pointers for now.  Some commented
   out code is still present to suggest how to add the rest, which includes
   having pointers and pointer types contain a region field to indicate what
   kind of pointer they are (in addition to the region in the block which
   indicates where the pointer points to).

 *)

inductive region : Type[0] ≝
(*  | Any : region
  | Data : region
  | IData : region
  | PData : region*)
  | XData : region
  | Code : region.

definition eq_region : region → region → bool ≝
λr1,r2.
  match r1 with
  [ (*Any ⇒   match r2 with [ Any ⇒ true | _ ⇒ false ]
  | Data ⇒  match r2 with [ Data ⇒ true | _ ⇒ false ]
  | IData ⇒ match r2 with [ IData ⇒ true | _ ⇒ false ]
  | PData ⇒ match r2 with [ PData ⇒ true | _ ⇒ false ]
  |*) XData ⇒ match r2 with [ XData ⇒ true | _ ⇒ false ]
  | Code ⇒  match r2 with [ Code ⇒ true | _ ⇒ false ]
  ].

lemma eq_region_elim : ∀P:bool → Type[0]. ∀r1,r2.
  (r1 = r2 → P true) → (r1 ≠ r2 → P false) →
  P (eq_region r1 r2).
#P #r1 #r2 cases r1; cases r2; #Ptrue #Pfalse
try ( @Ptrue // )
@Pfalse % #E destruct
qed.

lemma reflexive_eq_region: ∀r. eq_region r r = true.
 * //
qed.

definition eq_region_dec : ∀r1,r2:region. (r1=r2)+(r1≠r2).
#r1 #r2 @(eq_region_elim ? r1 r2) /2/; qed.

(*
(* Carefully defined to be convertably nonzero *)
definition size_pointer : region → nat ≝
λsp. S match sp with [ Data ⇒ 0 | IData ⇒ 0 | PData ⇒ 0 | XData ⇒ 1 | Code ⇒ 1 | Any ⇒ 2 ].
*)
definition size_pointer : nat ≝ 2.

(* We maintain some reasonable type information through the front end of the
   compiler. *)

inductive signedness : Type[0] ≝
  | Signed: signedness
  | Unsigned: signedness.

inductive intsize : Type[0] ≝
  | I8: intsize
  | I16: intsize
  | I32: intsize.

(* * Float types come in two sizes: 32 bits (single precision)
  and 64-bit (double precision). *)

inductive floatsize : Type[0] ≝
  | F32: floatsize
  | F64: floatsize.

inductive typ : Type[0] ≝
  | ASTint : intsize → signedness → typ
  | ASTptr : (*region →*) typ
  | ASTfloat : floatsize → typ.

(* XXX aliases *)
definition SigType ≝ typ.
definition SigType_Int ≝ ASTint I32 Unsigned.
(*
| SigType_Float: SigType
*)
definition SigType_Ptr ≝ ASTptr (*Any*).

(* Define these carefully so that we always know that the result is nonzero,
   and can be used in dependent types of the form (S n).
   (At the time of writing this is only used for bitsize_of_intsize.) *)

definition pred_size_intsize : intsize → nat ≝
λsz. match sz with [ I8 ⇒ 0 | I16 ⇒ 1 | I32 ⇒ 3].

definition size_intsize : intsize → nat ≝
λsz. S (pred_size_intsize sz).

definition bitsize_of_intsize : intsize → nat ≝
λsz. size_intsize sz * 8.

definition eq_intsize : intsize → intsize → bool ≝
λsz1,sz2.
  match sz1 with
  [ I8  ⇒ match sz2 with [ I8  ⇒ true | _ ⇒ false ]
  | I16 ⇒ match sz2 with [ I16 ⇒ true | _ ⇒ false ]
  | I32 ⇒ match sz2 with [ I32 ⇒ true | _ ⇒ false ]
  ].

lemma eq_intsize_elim : ∀sz1,sz2. ∀P:bool → Type[0].
  (sz1 ≠ sz2 → P false) → (sz1 = sz2 → P true) → P (eq_intsize sz1 sz2).
* * #P #Hne #Heq whd in ⊢ (?%); try (@Heq @refl) @Hne % #E destruct
qed.

lemma eq_intsize_true : ∀sz. eq_intsize sz sz = true.
* @refl
qed.

lemma eq_intsize_false : ∀sz,sz'. sz ≠ sz' → eq_intsize sz sz' = false.
* * * #NE try @refl @False_ind @NE @refl
qed.

definition signedness_check : ∀sg1,sg2:signedness. ∀P:signedness → signedness → Type[0].
 P sg1 sg1 → P sg1 sg2 → P sg1 sg2 ≝
λsg1,sg2,P.
match sg1 return λsg1. P sg1 sg1 → P sg1 sg2 → P sg1 sg2 with
[ Signed ⇒ λx. match sg2 return λsg2. P ? sg2 → P Signed sg2 with [ Signed ⇒ λd. x | _ ⇒ λd. d ]
| Unsigned ⇒ λx. match sg2 return λsg2. P ? sg2 → P Unsigned sg2 with [ Unsigned ⇒ λd. x | _ ⇒ λd. d ]
].

let rec inttyp_eq_elim' (sz1,sz2:intsize) (sg1,sg2:signedness) (P:intsize → signedness → intsize → signedness → Type[0]) on sz1 :
  P sz1 sg1 sz1 sg1 → P sz1 sg1 sz2 sg2 → P sz1 sg1 sz2 sg2 ≝
match sz1 return λsz. P sz sg1 sz sg1 → P sz sg1 sz2 sg2 → P sz sg1 sz2 sg2 with
[ I8  ⇒ λx. match sz2 return λsz. P ?? sz ? → P I8 ? sz ? with [ I8  ⇒ signedness_check sg1 sg2 (λs1,s2. P ? s1 ? s2) x | _ ⇒ λd. d ]
| I16 ⇒ λx. match sz2 return λsz. P I16 sg1 sz sg2 → P I16 sg1 sz sg2 with [ I16 ⇒ signedness_check sg1 sg2 (λs1,s2. P ? s1 ? s2) x | _ ⇒ λd. d ]
| I32 ⇒ λx. match sz2 return λsz. P I32 sg1 sz sg2 → P I32 sg1 sz sg2 with [ I32 ⇒ signedness_check sg1 sg2 (λs1,s2. P ? s1 ? s2) x | _ ⇒ λd. d ]
].

let rec intsize_eq_elim' (sz1,sz2:intsize) (P:intsize → intsize → Type[0]) on sz1 :
  P sz1 sz1 → P sz1 sz2 → P sz1 sz2 ≝
match sz1 return λsz. P sz sz → P sz sz2 → P sz sz2 with
[ I8  ⇒ λx. match sz2 return λsz. P ? sz → P I8 sz with [ I8  ⇒ λd. x | _ ⇒ λd. d ]
| I16 ⇒ λx. match sz2 return λsz. P ? sz → P I16 sz with [ I16 ⇒ λd. x | _ ⇒ λd. d ]
| I32 ⇒ λx. match sz2 return λsz. P ? sz → P I32 sz with [ I32 ⇒ λd. x | _ ⇒ λd. d ]
].

(* [intsize_eq_elim ? sz1 sz2 ? n (λn.e1) e2] checks if [sz1] equals [sz2] and
   if it is returns [e1] where the type of [n] has its dependency on [sz1]
   changed to [sz2], and if not returns [e2]. *)
let rec intsize_eq_elim (A:Type[0]) (sz1,sz2:intsize) (P:intsize → Type[0]) on sz1 :
  P sz1 → (P sz2 → A) → A → A ≝
match sz1 return λsz. P sz → (P sz2 → A) → A → A with
[ I8  ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I8  ⇒ λf,d. f x | _ ⇒ λf,d. d ]
| I16 ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I16 ⇒ λf,d. f x | _ ⇒ λf,d. d ]
| I32 ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I32 ⇒ λf,d. f x | _ ⇒ λf,d. d ]
].

lemma intsize_eq_elim_true : ∀A,sz,P,p,f,d.
  intsize_eq_elim A sz sz P p f d = f p.
#A * //
qed.

lemma intsize_eq_elim_elim : ∀A,sz1,sz2,P,p,f,d. ∀Q:A → Type[0].
  (sz1 ≠ sz2 → Q d) → (∀E:sz1 = sz2. match sym_eq ??? E return λx.λ_.P x → Type[0] with [ refl ⇒ λp. Q (f p) ] p ) → Q (intsize_eq_elim A sz1 sz2 P p f d).
#A * * #P #p #f #d #Q #Hne #Heq
[ 1,5,9: whd in ⊢ (?%); @(Heq (refl ??))
| *: whd in ⊢ (?%); @Hne % #E destruct
] qed.

lemma intsize_eq_elim_false : ∀A,sz,sz',P,p,f,d.
  sz ≠ sz' →
  intsize_eq_elim A sz sz' P p f d = d.
#A * * // #P #p #f #d * #H cases (H (refl ??))
qed.

(* A type for the integers that appear in the semantics. *)
definition bvint : intsize → Type[0] ≝ λsz. BitVector (bitsize_of_intsize sz).

definition repr : ∀sz:intsize. nat → bvint sz ≝
λsz,x. bitvector_of_nat (bitsize_of_intsize sz) x.

definition size_floatsize : floatsize → nat ≝
λsz. S match sz with [ F32 ⇒ 3 | F64 ⇒ 7 ].

let rec floatsize_eq_elim (sz1,sz2:floatsize) (P:floatsize → floatsize → Type[0]) on sz1 :
  P sz1 sz1 → P sz1 sz2 → P sz1 sz2 ≝
match sz1 return λsz. P sz sz → P sz sz2 → P sz sz2 with
[ F32 ⇒ λx. match sz2 return λsz. P ? sz → P F32 sz with [ F32 ⇒ λd. x | _ ⇒ λd. d ]
| F64 ⇒ λx. match sz2 return λsz. P ? sz → P F64 sz with [ F64 ⇒ λd. x | _ ⇒ λd. d ]
].


definition typesize : typ → nat ≝ λty.
  match ty with
  [ ASTint sz _ ⇒ size_intsize sz
  | ASTptr  ⇒ size_pointer 
  | ASTfloat sz ⇒ size_floatsize sz ].

lemma typesize_pos: ∀ty. typesize ty > 0.
*; try *; try * /2 by le_n/ qed.

lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2).
* *; try *; try *; try *; try *; try (%1 @refl) %2 @nmk #H destruct
qed.

lemma opt_typ_eq: ∀t1,t2: option typ. (t1=t2) + (t1≠t2).
#t1 #t2 cases t1 cases t2
[ %1 @refl
| 2,3: #ty %2 % #H destruct
| #ty1 #ty2 elim (typ_eq ty1 ty2) #E [ %1 >E @refl | %2 % #E' destruct cases E /2/
]
qed.

(* * Additionally, function definitions and function calls are annotated
  by function signatures indicating the number and types of arguments,
  as well as the type of the returned value if any.  These signatures
  are used in particular to determine appropriate calling conventions
  for the function. *)

record signature : Type[0] ≝ {
  sig_args: list typ;
  sig_res: option typ
}.

(* XXX aliases *)
definition Signature ≝ signature.
definition signature_args ≝ sig_args.
definition signature_return ≝ sig_res.

definition proj_sig_res : signature → typ ≝ λs.
  match sig_res s with
  [ None ⇒ ASTint I32 Unsigned
  | Some t ⇒ t
  ].

(* * Initialization data for global variables. *)

inductive init_data: Type[0] ≝ 
  | Init_int8: bvint I8 → init_data
  | Init_int16: bvint I16 → init_data
  | Init_int32: bvint I32 → init_data
  | Init_float32: float → init_data
  | Init_float64: float → init_data
  | Init_space: nat → init_data 
  | Init_null: (*region →*) init_data
  | Init_addrof: (*region →*) ident → nat → init_data.   (*r address of symbol + offset *)

(* * Whole programs consist of:
- a collection of function definitions (name and description);
- the name of the ``main'' function that serves as entry point in the program;
- a collection of global variable declarations, consisting of
  a name, initialization data, and additional information.

The type of function descriptions and that of additional information
for variables vary among the various intermediate languages and are
taken as parameters to the [program] type.  The other parts of whole
programs are common to all languages. *)

record program (F: list ident → Type[0]) (V: Type[0]) : Type[0] := {
  prog_vars: list (ident × region × V);
  prog_funct: list (ident × (F (map … (λx. \fst (\fst x)) prog_vars)));
  prog_main: ident
}.


definition prog_funct_names ≝ λF,V. λp: program F V.
  map ?? \fst (prog_funct … p).

definition prog_var_names ≝ λF,V. λp: program F V.
  map ?? (λx. \fst (\fst x)) (prog_vars … p).

(* * * Generic transformations over programs *)

(* * We now define a general iterator over programs that applies a given
  code transformation function to all function descriptions and leaves
  the other parts of the program unchanged. *)
(*
Section TRANSF_PROGRAM.

Variable A B V: Type.
Variable transf: A -> B.
*)

definition transf_program : ∀A,B. (A → B) → list (ident × A) → list (ident × B) ≝
λA,B,transf,l.
  map ?? (λid_fn. 〈fst ?? id_fn, transf (snd ?? id_fn)〉) l.

(* In principle we could allow the transformation to be specialised to a
   particular set of variable names, but that makes it much harder to state
   and prove properties. *)

definition transform_program : ∀A,B,V. ∀p:program A V. (∀varnames. A varnames → B varnames) → program B V ≝
λA,B,V,p,transf.
  mk_program B V
    (prog_vars A V p)
    (transf_program ?? (transf ?) (prog_funct A V p))
    (prog_main A V p).
(*
lemma transform_program_function:
  ∀A,B,V,transf,p,i,tf.
  in_list ? 〈i, tf〉 (prog_funct ?? (transform_program A B V transf p)) →
  ∃f. in_list ? 〈i, f〉 (prog_funct ?? p) ∧ transf f = tf.
normalize; #A #B #V #transf #p #i #tf #H elim (list_in_map_inv ????? H);
#x elim x; #i' #tf' *; #e #H destruct; %{tf'} /2/;
qed.
*)
(*
End TRANSF_PROGRAM.

(** The following is a variant of [transform_program] where the
  code transformation function can fail and therefore returns an
  option type. *)

Open Local Scope error_monad_scope.
Open Local Scope string_scope.

Section MAP_PARTIAL.

Variable A B C: Type.
Variable prefix_errmsg: A -> errmsg.
Variable f: B -> res C.
*)
definition map_partial : ∀A,B,C:Type[0]. (B → res C) →
                         list (A × B) → res (list (A × C)) ≝
λA,B,C,f. m_list_map ??? (λab. let 〈a,b〉 ≝ ab in do c ← f b; OK ? 〈a,c〉).

lemma map_partial_preserves_first:
 ∀A,B,C:Type[0]. ∀f: B → res C. ∀l: list (A × B). ∀l': list (A × C).
  map_partial … f l = OK ? l' →
   map … \fst l = map … \fst l'.
 #A #B #C #f #l elim l
  [ #l' #E normalize in E; destruct %
  | * #a #b #tl #IH #l' normalize in ⊢ (??%? → ?); cases (f b) normalize in ⊢ (? → ??%? → ?);
    [2: #err #E destruct
    | #c change with (match map_partial … f tl with [ OK x ⇒ ? | Error y ⇒ ?] = ? → ?)
      cases (map_partial … f tl) in IH ⊢ %;
      #x #IH normalize in ⊢ (??%? → ?); #ABS destruct normalize
      >(IH x) // ]]
qed.

lemma map_partial_All2 : ∀A,B,C,f. ∀P:A×B → A×C → Prop.
  (∀i,x,y. f x = OK ? y → P 〈i,x〉 〈i,y〉) →
  ∀l,l'.
  map_partial A B C f l = OK ? l' →
  All2 (A×B) (A×C) P l l'.
#A #B #C #f #P #H #l elim l
[ * [ // | #h #t #E normalize in E; destruct ]
| * #a #b #tl #IH #l' #M
  cases (bind_inversion ????? M) -M * #a' #c * #AC #M
  cases (bind_inversion ????? M) -M #tl' * #TL #M
  cases (bind_inversion ????? AC) -AC #c' * #C #C'
  normalize in C C' M; destruct %
  [ @H @C
  | @IH @TL
  ]
] qed.

(*
Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) :=
  match l with
  | nil => OK nil
  | (a, b) :: rem =>
      match f b with
      | Error msg => Error (prefix_errmsg a ++ msg)%list
      | OK c =>
          do rem' <- map_partial rem; 
          OK ((a, c) :: rem')
      end
  end.

Remark In_map_partial:
  forall l l' a c,
  map_partial l = OK l' ->
  In (a, c) l' ->
  exists b, In (a, b) l /\ f b = OK c.
Proof.
  induction l; simpl.
  intros. inv H. elim H0.
  intros until c. destruct a as [a1 b1].
  caseEq (f b1); try congruence.
  intro c1; intros. monadInv H0. 
  elim H1; intro. inv H0. exists b1; auto. 
  exploit IHl; eauto. intros [b [P Q]]. exists b; auto.
Qed.

Remark map_partial_forall2:
  forall l l',
  map_partial l = OK l' ->
  list_forall2
    (fun (a_b: A * B) (a_c: A * C) =>
       fst a_b = fst a_c /\ f (snd a_b) = OK (snd a_c))
    l l'.
Proof.
  induction l; simpl.
  intros. inv H. constructor.
  intro l'. destruct a as [a b].
  caseEq (f b). 2: congruence. intro c; intros. monadInv H0.  
  constructor. simpl. auto. auto. 
Qed.

End MAP_PARTIAL.

Remark map_partial_total:
  forall (A B C: Type) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)),
  map_partial prefix (fun b => OK (f b)) l =
  OK (List.map (fun a_b => (fst a_b, f (snd a_b))) l).
Proof.
  induction l; simpl.
  auto.
  destruct a as [a1 b1]. rewrite IHl. reflexivity.
Qed.

Remark map_partial_identity:
  forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)),cmp
  map_partial prefix (fun b => OK b) l = OK l.
Proof.
  induction l; simpl.
  auto.
  destruct a as [a1 b1]. rewrite IHl. reflexivity.
Qed.

Section TRANSF_PARTIAL_PROGRAM.

Variable A B V: Type.
Variable transf_partial: A -> res B.

Definition prefix_funct_name (id: ident) : errmsg :=
  MSG "In function " :: CTX id :: MSG ": " :: nil.
*)
definition transform_partial_program : ∀A,B,V. ∀p:program A V. (∀varnames. A varnames → res (B varnames)) →  res (program B V) ≝
λA,B,V,p,transf_partial.
  do fl ← map_partial … (transf_partial ?) (prog_funct … p);
  OK (program B V) (mk_program … (prog_vars … p) fl (prog_main ?? p)).

(*
Lemma transform_partial_program_function:
  forall p tp i tf,
  transform_partial_program p = OK tp ->
  In (i, tf) tp.(prog_funct) ->
  exists f, In (i, f) p.(prog_funct) /\ transf_partial f = OK tf.
Proof.
  intros. monadInv H. simpl in H0.  
  eapply In_map_partial; eauto.
Qed.

Lemma transform_partial_program_main:
  forall p tp,
  transform_partial_program p = OK tp ->
  tp.(prog_main) = p.(prog_main).
Proof.
  intros. monadInv H. reflexivity.
Qed.

Lemma transform_partial_program_vars:
  forall p tp,
  transform_partial_program p = OK tp ->
  tp.(prog_vars) = p.(prog_vars).
Proof.
  intros. monadInv H. reflexivity.
Qed.

End TRANSF_PARTIAL_PROGRAM.

(** The following is a variant of [transform_program_partial] where
  both the program functions and the additional variable information
  are transformed by functions that can fail. *)

Section TRANSF_PARTIAL_PROGRAM2.

Variable A B V W: Type.
Variable transf_partial_function: A -> res B.
Variable transf_partial_variable: V -> res W.

Definition prefix_var_name (id_init: ident * list init_data) : errmsg :=
  MSG "In global variable " :: CTX (fst id_init) :: MSG ": " :: nil.
*)

(* CSC: ad hoc lemma, move away? *)
lemma map_fst:
 ∀A,B,C,C':Type[0].∀l:list (A × B × C).∀l':list (A × B × C').
  map … \fst l = map … \fst l' →
  map … (λx. \fst (\fst x)) l = map … (λx. \fst (\fst x)) l'.
#A #B #C #C' #l elim l
 [ #l' elim l' // #he #tl #IH #ABS normalize in ABS; destruct
 | #he1 #tl1 #IH #l' cases l' [ #ABS normalize in ABS; destruct ]
   #he2 #tl2 #EQ whd in EQ:(??%%) ⊢ (??%%); >(IH tl2) destruct normalize in e1 ⊢ %; >e0 //
   >e0 in e1; normalize #H @H ]
qed.

definition transform_partial_program2 :
 ∀A,B,V,W. ∀p: program A V.
  (∀varnames. A varnames → res (B varnames))
  →  (V → res W) → res (program B W) ≝
λA,B,V,W,p, transf_partial_function, transf_partial_variable.
  do fl ← map_partial … (*prefix_funct_name*) (transf_partial_function ?) (prog_funct ?? p); ?.
  (*CSC: interactive mode because of dependent types *)
  generalize in match (map_partial_preserves_first … transf_partial_variable (prog_vars … p));
  cases (map_partial … transf_partial_variable (prog_vars … p))
  [ #vl #EQ
    @(OK (program B W) (mk_program … vl … (prog_main … p)))
    <(map_fst … (EQ vl (refl …))) @fl
  | #err #_ @(Error … err)]
qed.

lemma transform_partial_program2_preserves_var_names : ∀A,B,V,W,p,tf,tv,p'.
  transform_partial_program2 A B V W p tf tv = OK ? p' →
  prog_var_names … p = prog_var_names … p'.
#A #B #V #W * #vars #fns #main #tf #tv * #vars' #fns' #main'
#T cases (bind_inversion ????? T) -T #vars1 * #Evars1
generalize in match (map_partial_preserves_first ?????); #MPPF
lapply (refl ? (map_partial ??? tv vars))
cases (map_partial ?????) in ⊢ (???% → ?);
[ 2: #m #M >M in MPPF ⊢ %; #MPPF #E normalize in E; destruct ]
#vs #VS >VS in MPPF ⊢ %; #MPPF
whd in ⊢ (??%% → ?);
generalize in match (map_fst ???????); #MF
#E destruct
whd in ⊢ (??%%); @MF
qed.


(*
Lemma transform_partial_program2_function:
  forall p tp i tf,
  transform_partial_program2 p = OK tp ->
  In (i, tf) tp.(prog_funct) ->
  exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf.
Proof.
  intros. monadInv H.  
  eapply In_map_partial; eauto. 
Qed.

Lemma transform_partial_program2_variable:
  forall p tp i tv,
  transform_partial_program2 p = OK tp ->
  In (i, tv) tp.(prog_vars) ->
  exists v, In (i, v) p.(prog_vars) /\ transf_partial_variable v = OK tv.
Proof.
  intros. monadInv H. 
  eapply In_map_partial; eauto. 
Qed.

Lemma transform_partial_program2_main:
  forall p tp,
  transform_partial_program2 p = OK tp ->
  tp.(prog_main) = p.(prog_main).
Proof.
  intros. monadInv H. reflexivity.
Qed.

End TRANSF_PARTIAL_PROGRAM2.

(** The following is a relational presentation of 
  [transform_program_partial2].  Given relations between function
  definitions and between variable information, it defines a relation
  between programs stating that the two programs have the same shape
  (same global names, etc) and that identically-named function definitions 
  are variable information are related. *)

Section MATCH_PROGRAM.

Variable A B V W: Type.
Variable match_fundef: A -> B -> Prop.
Variable match_varinfo: V -> W -> Prop.

*)

record matching : Type[1] ≝ {
  m_A : list ident → Type[0];  m_B : list ident → Type[0];  (* function types *)
  m_V : Type[0];  m_W : Type[0];  (* variable types *)
  match_fundef : ∀vs. m_A vs → m_B vs → Prop;
  match_varinfo : m_V → m_W → Prop
}.

(* When defining a matching between function entries, quietly enforce equality
   of the list of global variables (vs and vs'). *)

inductive match_funct_entry (M:matching) : ∀vs,vs'. ident × (m_A M vs) → ident × (m_B M vs') → Prop ≝
| mfe_intro : ∀vs,id,f1,f2. match_fundef M vs f1 f2 → match_funct_entry M vs vs 〈id,f1〉 〈id,f2〉.

(* but we'll need some care to usefully invert it *)

definition mfe_cast_fn_type : ∀M,vs,vs'. ∀E:vs'=vs. m_B M vs' → m_B M vs ≝
λM,vs,vs',E. ?.
>E #m @m
qed.

let rec match_funct_entry_inv (M:matching)
  (P:∀vs,id,f,id',f'. Prop)
  (H:∀vs,id,f,id',f'. match_fundef M vs f f' → P vs id f id' f')
  vs id f id' f'
  (MFE:match_funct_entry M vs vs 〈id,f〉 〈id',f'〉) on MFE : P vs id f id' f' ≝
match MFE return λvs,vs',idf,idf',MFE. ∀E:vs'=vs. P vs (\fst idf) (\snd idf) (\fst idf') (mfe_cast_fn_type … E (\snd idf')) with
[ mfe_intro vs id f1 f2 MF ⇒ ?
] (refl ??).
#E >(K ?? E) @H @MF
qed.

(* and continue as before *)

inductive match_var_entry (M:matching) : ident × region × (m_V M) → ident × region × (m_W M) → Prop ≝
| mve_intro : ∀id,r,v1,v2. match_varinfo M v1 v2 → match_var_entry M 〈id,r,v1〉 〈id,r,v2〉.

lemma matching_vars : ∀M.∀p1:program (m_A M) (m_V M).∀p2:program (m_B M) (m_W M).
  All2 … (match_var_entry M) (prog_vars … p1) (prog_vars … p2) →
  prog_var_names … p1 = prog_var_names … p2.
#M * #vs1 #mn1 #fn1 * #vs2 #mn2 #fn2
normalize generalize in match vs2;
elim vs1
[ * [ // | #h #t * ]
| * * #id1 #r1 #v1 #tl1 #IH * [ * ]
  * * #id2 #r2 #v2 #tl2 * *
  #id #r #v1' #v2' #_ #H
  whd in ⊢ (??%%); >(IH … H) %
] qed.

record match_program (M:matching) (p1: program (m_A M) (m_V M)) (p2: program (m_B M) (m_W M)) : Prop ≝ {
  mp_vars : All2 … (match_var_entry M) (prog_vars … p1) (prog_vars … p2);
  mp_funct : All2 ?? … (match_funct_entry M (prog_var_names … p1) (prog_var_names … p2)) (prog_funct … p1) (prog_funct ??… p2);
  mp_main : prog_main … p1 = prog_main … p2
}.

(*
End MATCH_PROGRAM.
*)

(* Now show that all the transformations are instances of match_program. *)

lemma transform_partial_program2_match:
  ∀A,B,V,W.
         ∀transf_partial_function: ∀vs. A vs -> res (B vs).
         ∀transf_partial_variable: V -> res W.
         ∀p: program A V. ∀tp: program B W.
  transform_partial_program2 … p transf_partial_function transf_partial_variable = OK ? tp →
  match_program (mk_matching A B V W
    (λvs,fd,tfd. transf_partial_function vs … fd = OK ? tfd)
    (λinfo,tinfo. transf_partial_variable info = OK ? tinfo))
    p tp.
#A #B #V #W #transf_partial_function #transf_partial_variable
* #vars #main #functs * #vars' #main' #functs'
#T cases (bind_inversion ????? T) -T #fl * #Efl
generalize in match (map_partial_preserves_first ?????); #MPPF
lapply (refl ? (map_partial ??? transf_partial_variable vars))
cases (map_partial ?????) in ⊢ (???% → ?);
[ 2: #m #M >M in MPPF ⊢ %; #MPPF #E normalize in E; destruct ]
#vs #VS >VS in MPPF ⊢ %; #MPPF
whd in ⊢ (??%% → ?);
generalize in match (map_fst ???????); #MF
#E destruct
%
[ @(map_partial_All2 … VS) * /2/
| whd in match (prog_var_names ???);
  whd in match (prog_var_names ???);
  <MF @(map_partial_All2 … Efl) #id #f1 #f2 /2/
| //
] qed.

lemma transform_partial_program_match:
  ∀A,B,V.
    ∀trans_partial_function: ∀vs. A vs → res (B vs).
    ∀p: program A V. ∀tp: program B V.
  transform_partial_program … p trans_partial_function = OK ? tp →
  match_program (mk_matching A B V V
    (λvs,fd,tfd. trans_partial_function vs fd = OK ? tfd)
    (λv,w. v = w))
    p tp.
#A #B #V #tpf
* #vars #fns #main * #vars' #fns' #main'
#TPP cases (bind_inversion ????? TPP) -TPP #fns'' * #MAP
#E normalize in E; destruct
%
[ elim vars' // * * #id #r #v #tl #H % /2/
| @(map_partial_All2 … MAP) #i #f #f' #TPF % @TPF
| //
] qed.

lemma transform_program_match:
  ∀A,B,V.
    ∀trans_function: ∀vs. A vs → B vs.
    ∀p: program A V. 
  match_program (mk_matching A B V V
    (λvs,fd,tfd. trans_function vs fd = tfd)
    (λv,w. v = w))
    p (transform_program … p trans_function).
#A #B #V #tf
* #vars #fns #main
%
[ normalize elim vars // * * #id #r #v #tl #H % /2/
| whd in match (prog_var_names ???);
  whd in match (prog_vars ???);
  elim fns
  [ //
  | * #id #f #tl #IH % // % //
  ]
| //
] qed.

(* * * External functions *)

(* * For most languages, the functions composing the program are either
  internal functions, defined within the language, or external functions
  (a.k.a. system calls) that emit an event when applied.  We define
  a type for such functions and some generic transformation functions. *)

record external_function : Type[0] ≝ {
  ef_id: ident;
  ef_sig: signature
}.

definition ExternalFunction ≝ external_function.
definition external_function_tag ≝ ef_id.
definition external_function_sig ≝ ef_sig.

inductive fundef (F: Type[0]): Type[0] ≝
  | Internal: F → fundef F
  | External: external_function → fundef F.

(* Implicit Arguments External [F]. *)
(*
Section TRANSF_FUNDEF.

Variable A B: Type.
Variable transf: A -> B.
*)
definition transf_fundef : ∀A,B. (A→B) → fundef A → fundef B ≝
λA,B,transf,fd.
  match fd with
  [ Internal f ⇒ Internal ? (transf f)
  | External ef ⇒ External ? ef
  ].

(*
End TRANSF_FUNDEF.

Section TRANSF_PARTIAL_FUNDEF.

Variable A B: Type.
Variable transf_partial: A -> res B.
*)

definition transf_partial_fundef : ∀A,B. (A → res B) → fundef A → res (fundef B) ≝
λA,B,transf_partial,fd.
  match fd with
  [ Internal f ⇒ do f' ← transf_partial f; OK ? (Internal ? f')
  | External ef ⇒ OK ? (External ? ef)
  ].
(*
End TRANSF_PARTIAL_FUNDEF.
*)



(* Partially merged stuff derived from the prototype cerco compiler. *)

(*
definition bool_to_Prop ≝
 λb. match b with [ true ⇒ True | false ⇒ False ].

coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0]. 
*)

(* dpm: should go to standard library *)
let rec member (i: ident) (eq_i: ident → ident → bool)
               (g: list ident) on g: Prop ≝
  match g with
  [ nil ⇒ False
  | cons hd tl ⇒
      bool_to_Prop (eq_i hd i) ∨ member i eq_i tl
  ].