Changeset 24 for C-semantics/AST.ma


Ignore:
Timestamp:
Aug 27, 2010, 1:21:50 PM (10 years ago)
Author:
campbell
Message:

Separate out IOMonad from the rest of the executable semantics.
Start adding simulation results.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/AST.ma

    r10 r24  
    149149Variable A B V: Type.
    150150Variable transf: A -> B.
    151 
    152 Definition transf_program (l: list (ident * A)) : list (ident * B) :=
    153   List.map (fun id_fn => (fst id_fn, transf (snd id_fn))) l.
    154 
    155 Definition transform_program (p: program A V) : program B V :=
    156   mkprogram
    157     (transf_program p.(prog_funct))
    158     p.(prog_main)
    159     p.(prog_vars).
    160 
    161 Lemma transform_program_function:
    162   forall p i tf,
    163   In (i, tf) (transform_program p).(prog_funct) ->
    164   exists f, In (i, f) p.(prog_funct) /\ transf f = tf.
    165 Proof.
    166   simpl. unfold transf_program. intros.
    167   exploit list_in_map_inv; eauto.
    168   intros [[i' f] [EQ IN]]. simpl in EQ. inversion EQ; subst.
    169   exists f; split; auto.
    170 Qed.
    171 
     151*)
     152
     153ndefinition transf_program : ∀A,B. (A → B) → list (ident × A) → list (ident × B) ≝
     154λA,B,transf,l.
     155  map ?? (λid_fn. 〈fst ?? id_fn, transf (snd ?? id_fn)〉) l.
     156
     157ndefinition transform_program : ∀A,B,V. (A → B) → program A V → program B V ≝
     158λA,B,V,transf,p.
     159  mk_program B V
     160    (transf_program ?? transf (prog_funct A V p))
     161    (prog_main A V p)
     162    (prog_vars A V p).
     163
     164nlemma transform_program_function:
     165  ∀A,B,V,transf,p,i,tf.
     166  in_list ? 〈i, tf〉 (prog_funct ?? (transform_program A B V transf p)) →
     167  ∃f. in_list ? 〈i, f〉 (prog_funct ?? p) ∧ transf f = tf.
     168nnormalize; #A B V transf p i tf H; nelim (list_in_map_inv ????? H);
     169#x; nelim x; #i' tf'; *; #e H; ndestruct; @tf'; /2/;
     170nqed.
     171
     172(*
    172173End TRANSF_PROGRAM.
    173174
     
    413414Variable A B: Type.
    414415Variable transf: A -> B.
    415 
    416 Definition transf_fundef (fd: fundef A): fundef B :=
     416*)
     417ndefinition transf_fundef : ∀A,B. (A→B) → fundef A → fundef B ≝
     418λA,B,transf,fd.
    417419  match fd with
    418   | Internal f => Internal (transf f)
    419   | External ef => External ef
    420   end.
    421 
     420  [ Internal f ⇒ Internal ? (transf f)
     421  | External ef ⇒ External ? ef
     422  ].
     423
     424(*
    422425End TRANSF_FUNDEF.
    423426
Note: See TracChangeset for help on using the changeset viewer.