Changeset 24 for Csemantics/AST.ma
 Timestamp:
 Aug 27, 2010, 1:21:50 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/AST.ma
r10 r24 149 149 Variable A B V: Type. 150 150 Variable 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 153 ndefinition 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 157 ndefinition 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 164 nlemma 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. 168 nnormalize; #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/; 170 nqed. 171 172 (* 172 173 End TRANSF_PROGRAM. 173 174 … … 413 414 Variable A B: Type. 414 415 Variable transf: A > B. 415 416 Definition transf_fundef (fd: fundef A): fundef B := 416 *) 417 ndefinition transf_fundef : ∀A,B. (A→B) → fundef A → fundef B ≝ 418 λA,B,transf,fd. 417 419 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 (* 422 425 End TRANSF_FUNDEF. 423 426
Note: See TracChangeset
for help on using the changeset viewer.