source: src/common/AST.ma @ 1183

(* *********************************************************************)
(*                                                                     *)
(*              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 ?.

(* XXX backend is currently using untagged words as identifiers. *)
definition Identifier ≝ Word.

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 *)

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.

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

definition size_pointer : region → nat ≝
λsp. match sp with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].

(* 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 size_intsize : intsize → nat ≝
λsz. S match sz with [ I8 ⇒ 0 | I16 ⇒ 1 | I32 ⇒ 3].

definition bitsize_of_intsize : intsize → nat ≝
λsz. S match sz with [ I8 ⇒ 7 | I16 ⇒ 15 | I32 ⇒ 31].

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.

(* [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.


(* 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 ].

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

lemma typesize_pos: ∀ty. typesize ty > 0.
*; try *; try * /2/ 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
  ].

(* * Memory accesses (load and store instructions) are annotated by
  a ``memory chunk'' indicating the type, size and signedness of the
  chunk of memory being accessed. *)

inductive memory_chunk : Type[0] ≝
  | Mint8signed : memory_chunk     (*r 8-bit signed integer *)
  | Mint8unsigned : memory_chunk   (*r 8-bit unsigned integer *)
  | Mint16signed : memory_chunk    (*r 16-bit signed integer *)
  | Mint16unsigned : memory_chunk  (*r 16-bit unsigned integer *)
  | Mint32 : memory_chunk          (*r 32-bit integer, or pointer *)
  | Mfloat32 : memory_chunk        (*r 32-bit single-precision float *)
  | Mfloat64 : memory_chunk        (*r 64-bit double-precision float *)
  | Mpointer : region → memory_chunk. (* pointer addressing given region *)

definition typ_of_memory_chunk : memory_chunk → typ ≝
λc. match c with
[ Mint8signed ⇒ ASTint I8 Signed
| Mint8unsigned ⇒ ASTint I8 Unsigned
| Mint16signed ⇒ ASTint I16 Signed
| Mint16unsigned ⇒ ASTint I16 Unsigned
| Mint32 ⇒ ASTint I32 Unsigned (* XXX signed? *)
| Mfloat32 ⇒ ASTfloat F32
| Mfloat64 ⇒ ASTfloat F64
| Mpointer r ⇒ ASTptr r
].

(* * 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,V: Type[0]) : Type[0] := {
  prog_funct: list (ident × F);
  prog_main: ident;
  prog_vars: list (ident × region × V)
}.


definition prog_funct_names ≝ λF,V: Type[0]. λp: program F V.
  map ? ? (fst ident F) (prog_funct ?? p).

definition prog_var_names ≝ λF,V: Type[0]. λp: program F V.
  map ?? (λx: ident × region × V. (\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.

definition transform_program : ∀A,B,V. (A → B) → program A V → program B V ≝
λA,B,V,transf,p.
  mk_program B V
    (transf_program ?? transf (prog_funct A V p))
    (prog_main A V p)
    (prog_vars 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. mmap ?? (λab. let 〈a,b〉 ≝ ab in do c ← f b; OK ? 〈a,c〉).
(*
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. (A → res B) → program A V → res (program B V) ≝
λA,B,V,transf_partial,p.
  do fl ← map_partial … (*prefix_funct_name*) transf_partial (prog_funct ?? p);
  OK ? (mk_program … fl (prog_main ?? p) (prog_vars ?? 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.
*)
definition transform_partial_program2 : ∀A,B,V,W. (A → res B) → (V → res W) →
                                        program A V → res (program B W) ≝
λA,B,V,W, transf_partial_function, transf_partial_variable, p.
  do fl ← map_partial … (*prefix_funct_name*) transf_partial_function (prog_funct ?? p);
  do vl ← map_partial … (*prefix_var_name*) transf_partial_variable (prog_vars ?? p);
  OK ? (mk_program … fl (prog_main ?? p) vl).
(*
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.

Definition match_funct_entry (x1: ident * A) (x2: ident * B) :=
  match x1, x2 with
  | (id1, fn1), (id2, fn2) => id1 = id2 /\ match_fundef fn1 fn2
  end.

Definition match_var_entry (x1: ident * list init_data * V) (x2: ident * list init_data * W) :=
  match x1, x2 with
  | (id1, init1, info1), (id2, init2, info2) => id1 = id2 /\ init1 = init2 /\ match_varinfo info1 info2
  end.

Definition match_program (p1: program A V) (p2: program B W) : Prop :=
  list_forall2 match_funct_entry p1.(prog_funct) p2.(prog_funct)
  /\ p1.(prog_main) = p2.(prog_main)
  /\ list_forall2 match_var_entry p1.(prog_vars) p2.(prog_vars).

End MATCH_PROGRAM.

Remark transform_partial_program2_match:
  forall (A B V W: Type)
         (transf_partial_function: A -> res B)
         (transf_partial_variable: V -> res W)
         (p: program A V) (tp: program B W),
  transform_partial_program2 transf_partial_function transf_partial_variable p = OK tp ->
  match_program 
    (fun fd tfd => transf_partial_function fd = OK tfd)
    (fun info tinfo => transf_partial_variable info = OK tinfo)
    p tp.
Proof.
  intros. monadInv H. split.
  apply list_forall2_imply with
    (fun (ab: ident * A) (ac: ident * B) =>
       fst ab = fst ac /\ transf_partial_function (snd ab) = OK (snd ac)).
  eapply map_partial_forall2. eauto. 
  intros. destruct v1; destruct v2; simpl in *. auto.
  split. auto.
  apply list_forall2_imply with
    (fun (ab: ident * list init_data * V) (ac: ident * list init_data * W) =>
       fst ab = fst ac /\ transf_partial_variable (snd ab) = OK (snd ac)).
  eapply map_partial_forall2. eauto. 
  intros. destruct v1; destruct v2; simpl in *. destruct p0; destruct p1. intuition congruence.
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
  ].

(* TODO: merge in comparison definitions from Integers.ma. *)
inductive Compare: Type[0] ≝
  Compare_Equal: Compare
| Compare_NotEqual: Compare
| Compare_Less: Compare
| Compare_Greater: Compare
| Compare_LessEqual: Compare
| Compare_GreaterEqual: Compare.

(* XXX unused definitions
inductive Cast: Type[0] ≝
  Cast_Int: Byte → Cast
| Cast_AddrSymbol: Identifier → Cast
| Cast_StackOffset: Immediate → Cast.

inductive Data: Type[0] ≝
  Data_Reserve: nat → Data
| Data_Int8: Byte → Data
| Data_Int16: Word → Data.

inductive DataSize: Type[0] ≝
  DataSize_Byte: DataSize
| DataSize_HalfWord: DataSize
| DataSize_Word: DataSize.
*)

definition Trace ≝ list Identifier.

inductive op1: Type[0] ≝
  | op_cast: nat → signedness → nat → op1
  | op_neg_int: op1          (**r integer opposite *)
  | op_not_bool: op1         (**r boolean negation  *)
  | op_not_int: op1          (**r bitwise complement  *)
  | op_id: op1               (**r identity *)
  | op_ptr_of_int: op1       (**r int to pointer *)
  | op_int_of_ptr: op1.      (**r pointer to int *)

inductive op2: Type[0] ≝
  | op_add: op2         (**r integer addition *)
  | op_sub: op2         (**r integer subtraction *)
  | op_mul: op2         (**r integer multiplication *)
  | op_div: op2         (**r integer signed division *)
  | op_divu: op2        (**r integer unsigned division *)
  | op_mod: op2         (**r integer signed modulus *)
  | op_modu: op2        (**r integer unsigned modulus *)
  | op_and: op2         (**r bitwise ``and'' *)
  | op_or: op2          (**r bitwise ``or'' *)
  | op_xor: op2         (**r bitwise ``xor'' *)
  | op_shl: op2         (**r left shift *)
  | op_shr: op2         (**r right signed shift *)
  | op_shru: op2        (**r right unsigned shift *)
  | op_cmp: Compare → op2   (**r integer signed comparison *)
  | op_cmpu: Compare → op2  (**r integer unsigned comparison *)
  | op_addp: op2        (**r addition for a pointer and an integer *)
  | op_subp: op2        (**r substraction for a pointer and a integer *)
  | op_subpp: op2
  | op_cmpp: Compare → op2. (**r pointer comparaison *)