Changeset 2590 for src/common


Ignore:
Timestamp:
Jan 24, 2013, 7:52:38 PM (7 years ago)
Author:
piccolo
Message:

added monad machineary for ERTL to ERTLptr translation
eval_seq_no_pc case in place in ERTLptr translation

Location:
src/common
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/common/ExtraMonads.ma

    r2570 r2590  
    6363  ; m_frel_ext : ∀X,Y,P,F,G.(∀x,prf1,prf2.F x prf1 = G x prf2) → ∀u,v.m_frel X Y P F u v → m_frel X Y P G u v
    6464  }.
     65 
     66record MonadFunctRel1 (M1 : Monad) (M2 : Monad) : Type[1] ≝
     67{ m_frel1  :5> ∀X,Y.(Y → X) → (M1 X → M2 Y → Prop)
     68; mfr_return1 : ∀X,Y,F,y.m_frel1 X Y F (return (F y)) (return y)
     69; mfr_bind1 : ∀X,Y,Z,W,F,G,m,n. m_frel1 X Y F m n →
     70       ∀f,g.(∀x.m_frel1 Z W G (f (F x)) (g x)) → m_frel1 ?? G (m_bind … m f) (m_bind … n g)
     71; m_frel_ext1 : ∀X,Y,F,G.(∀x.F  x = G x) → ∀ u,v.m_frel1 X Y F u v → m_frel1 X Y G u v
     72}.
     73
    6574
    6675definition res_preserve : MonadFunctRel Res Res ≝
     
    7887qed.
    7988
     89definition res_preserve1 : MonadFunctRel1 Res Res ≝
     90mk_MonadFunctRel1 ??
     91(λX,Y,F,m,n.∀y.m = return y → ∃ x. n = return x ∧ y = F x)
     92???.
     93[ #X #Y #F #y #x normalize #EQ destruct(EQ) %{y} % //
     94| #X #Y #Z #W #F #G * [#x | #e] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?); #EQ destruct
     95  cases(H x (refl …)) #y * #n_spec #x_spec
     96  cases(H1 y z ?) [2: <x_spec whd in ⊢ (???%); assumption] #w * #w_spec #z_spec %{w}
     97  >n_spec <w_spec % //
     98| #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y}
     99  % //
     100]
     101qed.
     102
    80103definition opt_preserve : MonadFunctRel Option Option ≝
    81104  mk_MonadFunctRel ??
     
    92115qed.
    93116
     117definition opt_preserve1 : MonadFunctRel1 Option Option ≝
     118  mk_MonadFunctRel1 ??
     119  (λX,Y,F,m,n.∀y.m = return y → ∃ x. n = return x ∧ y = F x)
     120???.
     121[ #X #Y #F #y #x normalize #EQ destruct(EQ) %{y} % //
     122| #X #Y #Z #W #F #G * [| #x] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?); #EQ destruct
     123  cases(H x (refl …)) #y * #n_spec #x_spec
     124  cases(H1 y z ?) [2: <x_spec whd in ⊢ (???%); assumption] #w * #w_spec #z_spec %{w}
     125  >n_spec <w_spec % //
     126| #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y}
     127  % //
     128]
     129qed.
     130
    94131definition io_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝
    95132  λO,I.mk_MonadFunctRel ??
     
    103140| #X #Y #P #F #G #H #u #v #K #x #EQ
    104141  cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try %
     142]
     143qed.
     144
     145definition io_preserve1 :  ∀O,I.MonadFunctRel1 (IOMonad O I) (IOMonad O I) ≝
     146  λO,I.mk_MonadFunctRel1 ??
     147  (λX,Y,F,m,n.∀y.m = return y → ∃ x. n = return x ∧ y = F x)
     148???.
     149[ #X #Y #F #y #x normalize #EQ destruct(EQ) %{y} % //
     150| #X #Y #Z #W #F #G * [#o #r | #x | #e] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?); #EQ destruct
     151  cases(H x (refl …)) #y * #n_spec #x_spec
     152  cases(H1 y z ?) [2: <x_spec whd in ⊢ (???%); assumption] #w * #w_spec #z_spec %{w}
     153  >n_spec <w_spec % //
     154| #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y}
     155  % //
    105156]
    106157qed.
     
    118169  FR … G
    119170    (f x) (g (F x prf)).
     171
     172definition preserving1 ≝   
     173  λM1,M2.λFR : MonadFunctRel1 M1 M2.
     174  λX,Y,A,B : Type[0].
     175  λF : Y → X.
     176  λG : B → A.
     177  λf : X → M1 A.
     178  λg : Y → M2 B.
     179  ∀ y.
     180  FR ?? G (f (F y)) (g y).
    120181
    121182definition preserving2 ≝
     
    133194  FR … H
    134195    (f x y) (g (F x prf1) (G y prf2)).
    135 
     196   
     197definition preserving21 ≝
     198   λM1,M2.λFR : MonadFunctRel1 M1 M2.
     199   λX,Y,Z,W,A,B : Type[0].
     200   λF : Z → X.
     201   λG : W → Y.
     202   λH : B → A.
     203   λf : X → Y → M1 A.
     204   λg : Z → W → M2 B.
     205   ∀z,w. FR ?? H (f (F z) (G w)) (g z w).
     206   
    136207lemma res_preserve_error : ∀X,Y,P,F,e,n.res_preserve X Y P F (Error … e) n.
    137208#X #Y #P #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
     209
     210lemma res_preserve_error1 : ∀X,Y,F,e,n.res_preserve1 X Y F (Error … e) n.
     211#X #Y #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
    138212
    139213lemma mfr_return_eq : ∀M1,M2.∀FR : MonadFunctRel M1 M2.
     
    143217#M1 #M2 #FR #X #Y #P #F #v #n #prf #EQ >EQ @mfr_return qed.
    144218
     219lemma mfr_return_eq1 :∀M1,M2.∀FR : MonadFunctRel1 M1 M2.
     220∀X,Y,F,v,n.
     221n = return F v →
     222FR X Y F n (return v).
     223#M1 #M2 #FR #X #Y #F #v #n #EQ >EQ @mfr_return1
     224qed.
     225
    145226lemma opt_safe_eq : ∀A,m,x,prf.m = Some A x → opt_safe A m prf = x.
    146227#A #m #x #prf @opt_safe_elim #x' #EQ >EQ #EQ' destruct % qed.
     
    148229lemma opt_preserve_none : ∀X,Y,P,F,n.opt_preserve X Y P F (None ?) n.
    149230#X #Y #P #F #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
     231
     232lemma opt_preserve_none1 :  ∀X,Y,F,n.opt_preserve1 X Y F (None ?) n.
     233#X #Y #F #n #x whd in ⊢ (???% → ?); #EQ destruct qed.
    150234
    151235lemma m_list_map_All_ok :
     
    176260qed.
    177261
     262lemma res_to_opt__preserve : ∀X,Y,F,m,n.
     263  res_preserve1 X Y F m n → opt_preserve1 X Y F (res_to_opt … m) (res_to_opt … n).
     264#X #Y #F #m #n #H #x #EQ
     265whd in H; cases (H x ?)
     266[ #y * #y_spec #x_spec %{y} % [ >y_spec %|assumption]
     267| cases m in EQ; normalize #x #EQ destruct %
     268]
     269qed.
     270
    178271lemma opt_to_res_preserve : ∀X,Y,P,F,m,n,e1,e2.
    179272       opt_preserve X Y P F m n →
     
    184277qed.
    185278
     279lemma opt_to_res_preserve1 :  ∀X,Y,F,m,n,e1,e2.
     280       opt_preserve1 X Y F m n →
     281       res_preserve1 X Y F (opt_to_res … e1 m) (opt_to_res … e2 n).
     282#X #Y #F #m #n #e1 #e2 #H #x #EQ
     283cases(H x ?)
     284[ #y * #y_spec #x_spec %{y} % [>y_spec %|assumption]
     285| cases m in EQ; normalize [2: #x1] #EQ destruct %
     286]
     287qed.
     288
    186289lemma err_eq_from_io : ∀O,I,X,m,v.
    187290  err_to_io O I X m = return v → m = return v.
     
    196299qed.
    197300
     301lemma res_to_io_preserve1 : ∀O,I,X,Y,F,m,n.
     302       res_preserve1 X Y F m n →
     303       io_preserve1 O I X Y F m n.
     304#O #I #X #Y #F #m #n #H #v #EQ cases(H v (err_eq_from_io ????? EQ))
     305#y * #y_spec #v_spec %{y} % // >y_spec %
     306qed.
  • src/common/PositiveMap.ma

    r2541 r2590  
    458458  [ pm_leaf ⇒ map_opt ?? (λx.choice (Some ? x) (None ?)) a
    459459  | pm_node o' l' r' ⇒
    460     pm_node ? (choice o o')
     460    match (choice o o') with 
     461    [None ⇒
     462      match (merge … choice l l') with
     463      [pm_leaf ⇒ match (merge … choice r r') with
     464          [pm_leaf ⇒ pm_leaf ?
     465          |_ ⇒ pm_node ? (None ?) (merge … choice l l') (merge … choice r r')
     466          ]
     467      |_ ⇒ pm_node ? (None ?) (merge … choice l l') (merge … choice r r')
     468      ]
     469   |Some x ⇒
     470    pm_node ? (Some ? x)
    461471      (merge … choice l l')
    462472      (merge … choice r r')
    463473  ]
    464 ].
     474]].
    465475
    466476lemma lookup_opt_merge : ∀A,B,C,choice,a,b,p.
     
    470480 #A#B#C#choice#a elim a
    471481[ normalize #b
    472 | #o#l#r#Hil#Hir * [2: #o'#l'#r' * normalize /2 by /]
    473 ]
    474 #p#choice_good >lookup_opt_map
     482| #o#l#r#Hil#Hir * [2: #o'#l'#r' * [2,3: #x] normalize cases(choice o o') normalize /2 by /
     483  [3: cases (merge A B C choice l l') normalize /2 by / cases(merge A B C choice r r')
     484      normalize /2 by /
     485  |*: #H [<Hir|<Hil] /2 by / cases(merge A B C choice l l') normalize /2 by /
     486      cases (merge A B C choice r r') normalize /2 by /
     487  ]
     488]]
     489#p #choice_good >lookup_opt_map
    475490elim (lookup_opt ???)
    476491normalize //
    477 qed.
     492qed. 
    478493
    479494let rec domain_size (A : Type[0]) (b : positive_map A) on b : ℕ ≝
  • src/common/extraGlobalenvs.ma

    r2570 r2590  
    2121    In ? (prog_vars ?? p) 〈〈id, r〉, v〉 →
    2222    ∃b. find_symbol ? (globalenv ?? init p) id = Some ? b.
    23 *)
    2423
    2524definition is_function ≝ λF.λge : genv_t F.
     
    4746| None ⇒ λ_.None ?
    4847] (refl …).
     48*)
    4949
    5050lemma symbol_of_function_block_ok :
     
    6161qed.
    6262
     63(*
    6364definition funct_of_block : ∀F,ge.
    6465  block → option  (Σi.is_function F ge i) ≝
     
    193194>(find_funct_ptr_transf … EQfunct) #EQ'' destruct %
    194195qed.
    195 
     196*)
    196197
    197198include alias "common/PositiveMap.ma".
     
    234235qed.
    235236
    236 
    237 
     237lemma globalenv_no_zero :
     238 ∀F,V,i,p.
     239  find_funct_ptr … (globalenv F V i p) (mk_block Code OZ) = None ?. //
     240qed.
     241
Note: See TracChangeset for help on using the changeset viewer.