path: root/cfrontend/SimplExpr.v

(* *********************************************************************)
(*                                                                     *)
(*              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 INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(** Translation from Compcert C to Clight.
    Side effects are pulled out of Compcert C expressions. *)

Require Import Coqlib Maps Integers Floats Values AST Memory Errors.
Require Import Ctypes Cop Csyntax Clight.

Local Open Scope string_scope.
Local Open Scope list_scope.

(** State and error monad for generating fresh identifiers. *)

Record generator : Type := mkgenerator {
  gen_next: ident;
  gen_trail: list (ident * type)
}.

Inductive result (A: Type) (g: generator) : Type :=
  | Err: Errors.errmsg -> result A g
  | Res: A -> forall (g': generator), Ple (gen_next g) (gen_next g') -> result A g.

Arguments Err [A g].
Arguments Res [A g].

Definition mon (A: Type) := forall (g: generator), result A g.

Definition ret {A: Type} (x: A) : mon A :=
  fun g => Res x g (Ple_refl (gen_next g)).

Definition error {A: Type} (msg: Errors.errmsg) : mon A :=
  fun g => Err msg.

Definition bind {A B: Type} (x: mon A) (f: A -> mon B) : mon B :=
  fun g =>
    match x g with
      | Err msg => Err msg
      | Res a g' i =>
          match f a g' with
          | Err msg => Err msg
          | Res b g'' i' => Res b g'' (Ple_trans _ _ _ i i')
      end
    end.

Definition bind2 {A B C: Type} (x: mon (A * B)) (f: A -> B -> mon C) : mon C :=
  bind x (fun p => f (fst p) (snd p)).

Notation "'do' X <- A ; B" := (bind A (fun X => B))
   (at level 200, X ident, A at level 100, B at level 200)
   : gensym_monad_scope.
Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B))
   (at level 200, X ident, Y ident, A at level 100, B at level 200)
   : gensym_monad_scope.

Parameter first_unused_ident: unit -> ident.

Definition initial_generator (x: unit) : generator :=
  mkgenerator (first_unused_ident x) nil.

Definition gensym (ty: type): mon ident :=
  fun (g: generator) =>
    Res (gen_next g)
        (mkgenerator (Pos.succ (gen_next g)) ((gen_next g, ty) :: gen_trail g))
        (Ple_succ (gen_next g)).

(** Construct a sequence from a list of statements.  To facilitate the
   proof, the sequence is nested to the left and starts with a [Sskip]. *)

Fixpoint makeseq_rec (s: statement) (l: list statement) : statement :=
  match l with
  | nil => s
  | s' :: l' => makeseq_rec (Ssequence s s') l'
  end.

Definition makeseq (l: list statement) : statement :=
  makeseq_rec Sskip l.

Section SIMPL_EXPR.

Local Open Scope gensym_monad_scope.

Variable ce: composite_env.

(** Smart constructor for [if ... then ... else]. *)

Fixpoint eval_simpl_expr (a: expr) : option val :=
  match a with
  | Econst_int n _ => Some(Vint n)
  | Econst_float n _ => Some(Vfloat n)
  | Econst_single n _ => Some(Vsingle n)
  | Econst_long n _ => Some(Vlong n)
  | Ecast b ty =>
      match eval_simpl_expr b with
      | None => None
      | Some v => sem_cast v (typeof b) ty Mem.empty
      end
  | _ => None
  end.

Function makeif (a: expr) (s1 s2: statement) : statement :=
  match eval_simpl_expr a with
  | Some v =>
      match bool_val v (typeof a) Mem.empty with
      | Some b => if b then s1 else s2
      | None   => Sifthenelse a s1 s2
      end
  | None => Sifthenelse a s1 s2
  end.

(** Smart constructors for [&] and [*].  They optimize away [&*] and [*&] sequences. *)

Definition Ederef' (a: expr) (t: type) : expr :=
  match a with
  | Eaddrof a' t' => if type_eq t (typeof a') then a' else Ederef a t
  | _ => Ederef a t
  end.

Definition Eaddrof' (a: expr) (t: type) : expr :=
  match a with
  | Ederef a' t' => if type_eq t (typeof a') then a' else Eaddrof a t
  | _ => Eaddrof a t
  end.

(** Translation of pre/post-increment/decrement. *)

Definition transl_incrdecr (id: incr_or_decr) (a: expr) (ty: type) : expr :=
  match id with
  | Incr => Ebinop Oadd a (Econst_int Int.one type_int32s) (incrdecr_type ty)
  | Decr => Ebinop Osub a (Econst_int Int.one type_int32s) (incrdecr_type ty)
  end.

(** Given a simple l-value expression [l], determine whether it
    designates a bitfield.  *)

Definition is_bitfield_access_aux
              (fn: composite_env -> ident -> members -> res (Z * bitfield))
              (id: ident) (fld: ident) : mon bitfield :=
  match ce!id with
  | None => error (MSG "unknown composite " :: CTX id :: nil)
  | Some co =>
      match fn ce fld (co_members co) with
      | OK (_, bf) => ret bf
      | Error _ => error (MSG "unknown field " :: CTX fld :: nil)
      end
  end.

Definition is_bitfield_access (l: expr) : mon bitfield :=
  match l with
  | Efield r f _ =>
      match typeof r with
      | Tstruct id _ => is_bitfield_access_aux field_offset id f
      | Tunion id _  => is_bitfield_access_aux union_field_offset id f
      | _ => error (msg "is_bitfield_access")
      end
  | _ => ret Full
  end.

(** According to the CompCert C semantics, an access to a l-value of
    volatile-qualified type can either
  - produce an event in the trace of observable events, or
  - produce no event and behave as if no volatile qualifier was there.

    The latter case, where the volatile qualifier is ignored, happens if
  - the l-value is a struct or union
  - the l-value is an access to a bit field.

    The [chunk_for_volatile_type] function distinguishes between the two
    cases.  It returns [Some chunk] if the semantics is to produce
    an observable event of the [Event_vload chunk] or [Event_vstore chunk]
    kind.  It returns [None] if the semantics is that of a non-volatile
    access. *)

Definition chunk_for_volatile_type (ty: type) (bf: bitfield) : option memory_chunk :=
  if type_is_volatile ty then
    match access_mode ty with
    | By_value chunk =>
        match bf with
        | Full => Some chunk
        | Bits _ _ _ _ => None
        end
    | _ => None
    end
  else None.

(** Generate a [Sset] or [Sbuiltin] operation as appropriate
  to dereference a l-value [l] and store its result in temporary variable [id]. *)

Definition make_set (bf: bitfield) (id: ident) (l: expr) : statement :=
  match chunk_for_volatile_type (typeof l) bf with
  | None => Sset id l
  | Some chunk =>
      let typtr := Tpointer (typeof l) noattr in
      Sbuiltin (Some id) (EF_vload chunk) (Tcons typtr Tnil) ((Eaddrof l typtr):: nil)
  end.

(** Translation of a "valof" operation.
  If the l-value accessed is of volatile type, we go through a temporary. *)

Definition transl_valof (ty: type) (l: expr) : mon (list statement * expr) :=
  if type_is_volatile ty
  then do t <- gensym ty;
       do bf <- is_bitfield_access l;
       ret (make_set bf t l :: nil, Etempvar t ty)
  else ret (nil, l).

(** Translation of an assignment. *)

Definition make_assign (bf: bitfield) (l r: expr) : statement :=
  match chunk_for_volatile_type (typeof l) bf with
  | None =>
      Sassign l r
  | Some chunk =>
      let ty := typeof l in
      let typtr := Tpointer ty noattr in
      Sbuiltin None (EF_vstore chunk) (Tcons typtr (Tcons ty Tnil))
                    (Eaddrof l typtr :: r :: nil)
  end.

(** Translation of the value of an assignment expression.
    For non-bitfield assignments, it's the value of the right-hand side
    converted to the type of the left-hand side.
    For assignments to bitfields, an additional normalization to
    the width and signedness of the bitfield is required. *)

Definition make_normalize (sz: intsize) (sg: signedness) (width: Z) (r: expr) :=
  let intconst (n: Z) := Econst_int (Int.repr n) type_int32s in
  if intsize_eq sz IBool || signedness_eq sg Unsigned then
    let mask := two_p width - 1 in
    Ebinop Oand r (intconst mask) (typeof r)
  else
    let amount := Int.zwordsize - width in
    Ebinop Oshr
           (Ebinop Oshl r (intconst amount) type_int32s)
           (intconst amount)
           (typeof r).

Definition make_assign_value (bf: bitfield) (r: expr): expr :=
  match bf with
  | Full => r
  | Bits sz sg pos width => make_normalize sz sg width r
  end.

(** Translation of expressions.  Return a pair [(sl, a)] of
    a list of statements [sl] and a pure expression [a].
- If the [dst] argument is [For_val], the statements [sl]
  perform the side effects of the original expression,
  and [a] evaluates to the same value as the original expression.
- If the [dst] argument is [For_effects], the statements [sl]
  perform the side effects of the original expression,
  and [a] is meaningless.
- If the [dst] argument is [For_set tyl tvar], the statements [sl]
  perform the side effects of the original expression, then
  assign the value of the original expression to the temporary [tvar].
  The value is casted according to the list of types [tyl] before
  assignment.  In this case, [a] is meaningless.
*)

Inductive set_destination : Type :=
  | SDbase (tycast ty: type) (tmp: ident)
  | SDcons (tycast ty: type) (tmp: ident) (sd: set_destination).

Inductive destination : Type :=
  | For_val
  | For_effects
  | For_set (sd: set_destination).

Definition dummy_expr := Econst_int Int.zero type_int32s.

Fixpoint do_set (sd: set_destination) (a: expr) : list statement :=
  match sd with
  | SDbase tycast ty tmp => Sset tmp (Ecast a tycast) :: nil
  | SDcons tycast ty tmp sd' => Sset tmp (Ecast a tycast) :: do_set sd' (Etempvar tmp ty)
  end.

Definition finish (dst: destination) (sl: list statement) (a: expr) :=
  match dst with
  | For_val => (sl, a)
  | For_effects => (sl, a)
  | For_set sd => (sl ++ do_set sd a, a)
  end.

Definition sd_temp (sd: set_destination) :=
  match sd with SDbase _ _ tmp => tmp | SDcons _ _ tmp _ => tmp end.
Definition sd_seqbool_val (tmp: ident) (ty: type) :=
  SDbase type_bool ty tmp.
Definition sd_seqbool_set (ty: type) (sd: set_destination) :=
  let tmp :=  sd_temp sd in SDcons type_bool ty tmp sd.

Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement * expr) :=
  match a with
  | Csyntax.Eloc b ofs bf ty =>
      error (msg "SimplExpr.transl_expr: Eloc")
  | Csyntax.Evar x ty =>
      ret (finish dst nil (Evar x ty))
  | Csyntax.Ederef r ty =>
      do (sl, a) <- transl_expr For_val r;
      ret (finish dst sl (Ederef' a ty))
  | Csyntax.Efield r f ty =>
      do (sl, a) <- transl_expr For_val r;
      ret (finish dst sl (Efield a f ty))
  | Csyntax.Eval (Vint n) ty =>
      ret (finish dst nil (Econst_int n ty))
  | Csyntax.Eval (Vfloat n) ty =>
      ret (finish dst nil (Econst_float n ty))
  | Csyntax.Eval (Vsingle n) ty =>
      ret (finish dst nil (Econst_single n ty))
  | Csyntax.Eval (Vlong n) ty =>
      ret (finish dst nil (Econst_long n ty))
  | Csyntax.Eval _ ty =>
      error (msg "SimplExpr.transl_expr: Eval")
  | Csyntax.Esizeof ty' ty =>
      ret (finish dst nil (Esizeof ty' ty))
  | Csyntax.Ealignof ty' ty =>
      ret (finish dst nil (Ealignof ty' ty))
  | Csyntax.Evalof l ty =>
      do (sl1, a1) <- transl_expr For_val l;
      do (sl2, a2) <- transl_valof (Csyntax.typeof l) a1;
      ret (finish dst (sl1 ++ sl2) a2)
  | Csyntax.Eaddrof l ty =>
      do (sl, a) <- transl_expr For_val l;
      ret (finish dst sl (Eaddrof' a ty))
  | Csyntax.Eunop op r1 ty =>
      do (sl1, a1) <- transl_expr For_val r1;
      ret (finish dst sl1 (Eunop op a1 ty))
  | Csyntax.Ebinop op r1 r2 ty =>
      do (sl1, a1) <- transl_expr For_val r1;
      do (sl2, a2) <- transl_expr For_val r2;
      ret (finish dst (sl1 ++ sl2) (Ebinop op a1 a2 ty))
  | Csyntax.Ecast r1 ty =>
      match dst with
      | For_val | For_set _ =>
          do (sl1, a1) <- transl_expr For_val r1;
          ret (finish dst sl1 (Ecast a1 ty))
      | For_effects =>
          transl_expr For_effects r1
      end
  | Csyntax.Eseqand r1 r2 ty =>
      do (sl1, a1) <- transl_expr For_val r1;
      match dst with
      | For_val =>
          do t <- gensym ty;
          do (sl2, a2) <- transl_expr (For_set (sd_seqbool_val t ty)) r2;
          ret (sl1 ++
               makeif a1 (makeseq sl2) (Sset t (Econst_int Int.zero ty)) :: nil,
               Etempvar t ty)
      | For_effects =>
          do (sl2, a2) <- transl_expr For_effects r2;
          ret (sl1 ++ makeif a1 (makeseq sl2) Sskip :: nil, dummy_expr)
      | For_set sd =>
          do (sl2, a2) <- transl_expr (For_set (sd_seqbool_set ty sd)) r2;
          ret (sl1 ++
               makeif a1 (makeseq sl2) (makeseq (do_set sd (Econst_int Int.zero ty))) :: nil,
               dummy_expr)
      end
  | Csyntax.Eseqor r1 r2 ty =>
      do (sl1, a1) <- transl_expr For_val r1;
      match dst with
      | For_val =>
          do t <- gensym ty;
          do (sl2, a2) <- transl_expr (For_set (sd_seqbool_val t ty)) r2;
          ret (sl1 ++
               makeif a1 (Sset t (Econst_int Int.one ty)) (makeseq sl2) :: nil,
               Etempvar t ty)
      | For_effects =>
          do (sl2, a2) <- transl_expr For_effects r2;
          ret (sl1 ++ makeif a1 Sskip (makeseq sl2) :: nil, dummy_expr)
      | For_set sd =>
          do (sl2, a2) <- transl_expr (For_set (sd_seqbool_set ty sd)) r2;
          ret (sl1 ++
               makeif a1 (makeseq (do_set sd (Econst_int Int.one ty))) (makeseq sl2) :: nil,
               dummy_expr)
      end
  | Csyntax.Econdition r1 r2 r3 ty =>
      do (sl1, a1) <- transl_expr For_val r1;
      match dst with
      | For_val =>
          do t <- gensym ty;
          do (sl2, a2) <- transl_expr (For_set (SDbase ty ty t)) r2;
          do (sl3, a3) <- transl_expr (For_set (SDbase ty ty t)) r3;
          ret (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil,
               Etempvar t ty)
      | For_effects =>
          do (sl2, a2) <- transl_expr For_effects r2;
          do (sl3, a3) <- transl_expr For_effects r3;
          ret (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil,
               dummy_expr)
      | For_set sd =>
          do t <- gensym ty;
          do (sl2, a2) <- transl_expr (For_set (SDcons ty ty t sd)) r2;
          do (sl3, a3) <- transl_expr (For_set (SDcons ty ty t sd)) r3;
          ret (sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil,
               dummy_expr)
      end
  | Csyntax.Eassign l1 r2 ty =>
      do (sl1, a1) <- transl_expr For_val l1;
      do (sl2, a2) <- transl_expr For_val r2;
      do bf <- is_bitfield_access a1;
      let ty1 := Csyntax.typeof l1 in
      let ty2 := Csyntax.typeof r2 in
      match dst with
      | For_val | For_set _ =>
          do t <- gensym ty1;
          ret (finish dst
                 (sl1 ++ sl2 ++ Sset t (Ecast a2 ty1) :: make_assign bf a1 (Etempvar t ty1) :: nil)
                 (make_assign_value bf (Etempvar t ty1)))
      | For_effects =>
          ret (sl1 ++ sl2 ++ make_assign bf a1 a2 :: nil,
               dummy_expr)
      end
  | Csyntax.Eassignop op l1 r2 tyres ty =>
      let ty1 := Csyntax.typeof l1 in
      do (sl1, a1) <- transl_expr For_val l1;
      do (sl2, a2) <- transl_expr For_val r2;
      do (sl3, a3) <- transl_valof ty1 a1;
      do bf <- is_bitfield_access a1;
      match dst with
      | For_val | For_set _ =>
          do t <- gensym ty1;
          ret (finish dst
                 (sl1 ++ sl2 ++ sl3 ++
                  Sset t (Ecast (Ebinop op a3 a2 tyres) ty1) ::
                  make_assign bf a1 (Etempvar t ty1) :: nil)
                 (make_assign_value bf (Etempvar t ty1)))
      | For_effects =>
          ret (sl1 ++ sl2 ++ sl3 ++ make_assign bf a1 (Ebinop op a3 a2 tyres) :: nil,
               dummy_expr)
      end
  | Csyntax.Epostincr id l1 ty =>
      let ty1 := Csyntax.typeof l1 in
      do (sl1, a1) <- transl_expr For_val l1;
      do bf <- is_bitfield_access a1;
      match dst with
      | For_val | For_set _ =>
          do t <- gensym ty1;
          ret (finish dst
                 (sl1 ++ make_set bf t a1 ::
                  make_assign bf a1 (transl_incrdecr id (Etempvar t ty1) ty1) :: nil)
                 (Etempvar t ty1))
      | For_effects =>
          do (sl2, a2) <- transl_valof ty1 a1;
          ret (sl1 ++ sl2 ++ make_assign bf a1 (transl_incrdecr id a2 ty1) :: nil,
               dummy_expr)
      end
  | Csyntax.Ecomma r1 r2 ty =>
      do (sl1, a1) <- transl_expr For_effects r1;
      do (sl2, a2) <- transl_expr dst r2;
      ret (sl1 ++ sl2, a2)
  | Csyntax.Ecall r1 rl2 ty =>
      do (sl1, a1) <- transl_expr For_val r1;
      do (sl2, al2) <- transl_exprlist rl2;
      match dst with
      | For_val | For_set _ =>
          do t <- gensym ty;
          ret (finish dst (sl1 ++ sl2 ++ Scall (Some t) a1 al2 :: nil)
                          (Etempvar t ty))
      | For_effects =>
          ret (sl1 ++ sl2 ++ Scall None a1 al2 :: nil, dummy_expr)
      end
  | Csyntax.Ebuiltin ef tyargs rl ty =>
      do (sl, al) <- transl_exprlist rl;
      match dst with
      | For_val | For_set _ =>
          do t <- gensym ty;
          ret (finish dst (sl ++ Sbuiltin (Some t) ef tyargs al :: nil)
                          (Etempvar t ty))
      | For_effects =>
          ret (sl ++ Sbuiltin None ef tyargs al :: nil, dummy_expr)
      end
  | Csyntax.Eparen r1 tycast ty =>
      error (msg "SimplExpr.transl_expr: paren")
  end

with transl_exprlist (rl: exprlist) : mon (list statement * list expr) :=
  match rl with
  | Csyntax.Enil =>
      ret (nil, nil)
  | Csyntax.Econs r1 rl2 =>
      do (sl1, a1) <- transl_expr For_val r1;
      do (sl2, al2) <- transl_exprlist rl2;
      ret (sl1 ++ sl2, a1 :: al2)
  end.

Definition transl_expression (r: Csyntax.expr) : mon (statement * expr) :=
  do (sl, a) <- transl_expr For_val r; ret (makeseq sl, a).

Definition transl_expr_stmt (r: Csyntax.expr) : mon statement :=
  do (sl, a) <- transl_expr For_effects r; ret (makeseq sl).

Definition transl_if (r: Csyntax.expr) (s1 s2: statement) : mon statement :=
  do (sl, a) <- transl_expr For_val r;
  ret (makeseq (sl ++ makeif a s1 s2 :: nil)).

(** Translation of statements *)

Definition expr_true := Econst_int Int.one type_int32s.

Definition is_Sskip:
  forall s, {s = Csyntax.Sskip} + {s <> Csyntax.Sskip}.
Proof.
  destruct s; ((left; reflexivity) || (right; congruence)).
Defined.

Fixpoint transl_stmt (s: Csyntax.statement) : mon statement :=
  match s with
  | Csyntax.Sskip => ret Sskip
  | Csyntax.Sdo e => transl_expr_stmt e
  | Csyntax.Ssequence s1 s2 =>
      do ts1 <- transl_stmt s1;
      do ts2 <- transl_stmt s2;
      ret (Ssequence ts1 ts2)
  | Csyntax.Sifthenelse e s1 s2 =>
      do ts1 <- transl_stmt s1;
      do ts2 <- transl_stmt s2;
      do (s', a) <- transl_expression e;
      if is_Sskip s1 && is_Sskip s2 then
        ret (Ssequence s' Sskip)
      else
        ret (Ssequence s' (Sifthenelse a ts1 ts2))
  | Csyntax.Swhile e s1 =>
      do s' <- transl_if e Sskip Sbreak;
      do ts1 <- transl_stmt s1;
      ret (Sloop (Ssequence s' ts1) Sskip)
  | Csyntax.Sdowhile e s1 =>
      do s' <- transl_if e Sskip Sbreak;
      do ts1 <- transl_stmt s1;
      ret (Sloop ts1 s')
  | Csyntax.Sfor s1 e2 s3 s4 =>
      do ts1 <- transl_stmt s1;
      do s' <- transl_if e2 Sskip Sbreak;
      do ts3 <- transl_stmt s3;
      do ts4 <- transl_stmt s4;
      if is_Sskip s1 then
        ret (Sloop (Ssequence s' ts4) ts3)
      else
        ret (Ssequence ts1 (Sloop (Ssequence s' ts4) ts3))
  | Csyntax.Sbreak =>
      ret Sbreak
  | Csyntax.Scontinue =>
      ret Scontinue
  | Csyntax.Sreturn None =>
      ret (Sreturn None)
  | Csyntax.Sreturn (Some e) =>
      do (s', a) <- transl_expression e;
      ret (Ssequence s' (Sreturn (Some a)))
  | Csyntax.Sswitch e ls =>
      do (s', a) <- transl_expression e;
      do tls <- transl_lblstmt ls;
      ret (Ssequence s' (Sswitch a tls))
  | Csyntax.Slabel lbl s1 =>
      do ts1 <- transl_stmt s1;
      ret (Slabel lbl ts1)
  | Csyntax.Sgoto lbl =>
      ret (Sgoto lbl)
  end

with transl_lblstmt (ls: Csyntax.labeled_statements) : mon labeled_statements :=
  match ls with
  | Csyntax.LSnil =>
      ret LSnil
  | Csyntax.LScons c s ls1 =>
      do ts <- transl_stmt s;
      do tls1 <- transl_lblstmt ls1;
      ret (LScons c ts tls1)
  end.

(** Translation of a function *)

Definition transl_function (f: Csyntax.function) : res function :=
  match transl_stmt f.(Csyntax.fn_body) (initial_generator tt) with
  | Err msg =>
      Error msg
  | Res tbody g i =>
      OK (mkfunction
              f.(Csyntax.fn_return)
              f.(Csyntax.fn_callconv)
              f.(Csyntax.fn_params)
              f.(Csyntax.fn_vars)
              g.(gen_trail)
              tbody)
  end.

Local Open Scope error_monad_scope.

Definition transl_fundef (fd: Csyntax.fundef) : res fundef :=
  match fd with
  | Internal f =>
      do tf <- transl_function f; OK (Internal tf)
  | External ef targs tres cc =>
      OK (External ef targs tres cc)
  end.

End SIMPL_EXPR.

Local Open Scope error_monad_scope.

Definition transl_program (p: Csyntax.program) : res program :=
  do p1 <- AST.transform_partial_program (transl_fundef p.(prog_comp_env)) p;
  OK {| prog_defs := AST.prog_defs p1;
        prog_public := AST.prog_public p1;
        prog_main := AST.prog_main p1;
        prog_types := prog_types p;
        prog_comp_env := prog_comp_env p;
        prog_comp_env_eq := prog_comp_env_eq p |}.