Changeset 1976 for src/common


Ignore:
Timestamp:
May 21, 2012, 7:04:21 PM (8 years ago)
Author:
tranquil
Message:
  • monads: just changed some defs, which had to be propagated in some files
  • ASM/CostProof.ma: linked cost as defined there to the one in StructuredTraces? that uses fold
  • added a library for permutations of lists (useful with fold AC ops on lists)
  • first draft of abstract_status implementation for joint languages (file joint/as_semantics.ma)
Location:
src/common
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/IOMonad.ma

    r1949 r1976  
    165165
    166166definition IOPred ≝ λO,I,Perr.
    167   mk_MonadPred (IOMonad O I)
    168     (λA.pred_io O I A Perr)
     167  mk_InjMonadPred (IOMonad O I)
     168    (mk_MonadPred ? (λA.pred_io O I A Perr) ???)
    169169    (λA,P,a_sig.match a_sig with [ mk_Sig a prf ⇒ pred_io_inject O I A Perr P a prf ])
    170     ????.
    171 [//
    172 |#X #Y #relin #relout #m elim m
     170    ?. //
     171[ #X #P #Q #H #m elim m
     172  [#o #f #IH #H #i @IH @H
     173  | #v @H
     174  | #e //
     175  ]
     176| #X #Y #relin #relout #m elim m
    173177  [ #o #f #IH whd in ⊢ (%→?); #H
    174178    #f #G whd #i
     
    177181  | #e //
    178182  ]
    179 | #X #P #Q #H #m elim m
    180   [#o #f #IH #H #i @IH @H
    181   | #v @H
    182   | #e //
    183   ]
    184 |#X #P * #m elim m
     183| #X #P * #m elim m
    185184  [ #o #f #IH whd in ⊢ (%→?); #H
    186185    change with (Interact ?????) in ⊢ (???%);
     
    200199coercion err_to_io : ∀O,I,A.∀c:res A.IO O I A ≝ err_to_io on _c:res ? to IO ???.
    201200
     201(*
    202202lemma res_io_pred : ∀O,I,A,Perr,P.∀m : res A.pred_res … Perr P m → pred_io O I ? Perr P m.
    203203#O #I #A #Perr #P * /2/ qed.
     
    205205lemma io_res_pred : ∀O,I,A,Perr,P.∀m : res A.pred_io O I ? Perr P m → pred_res ? Perr P m.
    206206#O #I #A #Perr #P * /2/ qed.
    207 
     207*)
    208208definition err_to_io_sig : ∀O,I,T.∀P:T → Prop. res (Sig T P) → IO O I (Sig T P) ≝
    209209λO,I,T,P,v. match v with [ OK v' ⇒ Value O I (Sig T P) v' | Error m ⇒ Wrong O I (Sig T P) m ].
  • src/common/StructuredTraces.ma

    r1964 r1976  
    632632for @{'fold plus 0 (λ${ident i}:$X.true) (λ${ident i}:$Y. $f) $l}.
    633633
    634 definition as_cost_of_trace_any_label :
    635   ∀S : abstract_status.
    636   ∀fl, start, end.
    637   as_cost_map S →
    638   trace_any_label S fl start end → ℕ ≝
    639   λS,fl,start,end,m,the_trace.
    640   Σ_{ l_sig ∈ flatten_trace_any_label … the_trace } (m l_sig).
    641 
    642 definition as_cost_of_trace_label_label :
    643   ∀S : abstract_status.
    644   ∀fl, start, end.
    645   as_cost_map S →
    646   trace_label_label S fl start end → ℕ ≝
    647   λS,fl,start,end,m,the_trace.
    648   Σ_{ l_sig ∈ flatten_trace_label_label … the_trace } (m l_sig).
    649 
    650 definition as_cost_of_trace_label_return :
    651   ∀S : abstract_status.
    652   ∀start, end.
    653   as_cost_map S →
    654   trace_label_return S start end → ℕ ≝
    655   λS,start,end,m,the_trace.
    656   Σ_{ l_sig ∈ flatten_trace_label_return … the_trace } (m l_sig).
    657 
    658634lemma lift_cost_map_same_cost :
    659635  ∀S_in, S_out, dec, m_out, trace_in, trace_out.
     
    680656  ∀the_trace_out : trace_any_label S_out f_out start_out end_out.
    681657  tal_rel … the_trace_in the_trace_out →
    682   as_cost_of_trace_any_label … (lift_cost_map_id S_in S_out dec m_out) the_trace_in =
    683     as_cost_of_trace_any_label … m_out the_trace_out.
     658  (Σ_{l ∈ flatten_trace_any_label … the_trace_in}
     659    (lift_cost_map_id … dec m_out l)) =
     660  (Σ_{l ∈ flatten_trace_any_label … the_trace_out} (m_out l)).
    684661#S_in #S_out #dec #m_out #f_in #f_out #start_in #start_out #end_in #end_out
    685662#tal_in #tal_out #H_tal
     
    692669  ∀the_trace_out : trace_label_label S_out f_out start_out end_out.
    693670  tll_rel … the_trace_in the_trace_out →
    694   as_cost_of_trace_label_label … (lift_cost_map_id S_in S_out dec m_out) the_trace_in =
    695     as_cost_of_trace_label_label … m_out the_trace_out.
     671  (Σ_{l ∈ flatten_trace_label_label … the_trace_in}
     672    (lift_cost_map_id … dec m_out l)) =
     673  (Σ_{l ∈ flatten_trace_label_label … the_trace_out} (m_out l)).
    696674#S_in #S_out #dec #m_out #f_in #f_out #start_in #start_out #end_in #end_out
    697675#tll_in #tll_out #H_tll
     
    704682  ∀the_trace_out : trace_label_return S_out start_out end_out.
    705683  tlr_rel … the_trace_in the_trace_out →
    706   as_cost_of_trace_label_return … (lift_cost_map_id S_in S_out dec m_out) the_trace_in =
    707     as_cost_of_trace_label_return … m_out the_trace_out.
     684  (Σ_{l ∈ flatten_trace_label_return … the_trace_in}
     685    (lift_cost_map_id … dec m_out l)) =
     686  (Σ_{l ∈ flatten_trace_label_return … the_trace_out} (m_out l)).
    708687#S_in #S_out #dec #m_out #start_in #start_out #end_in #end_out
    709688#tlr_in #tlr_out #H_tlr
Note: See TracChangeset for help on using the changeset viewer.