Changeset 1601 for src/common


Ignore:
Timestamp:
Dec 13, 2011, 2:49:52 PM (8 years ago)
Author:
sacerdot
Message:

Files ported to new version of the standard library.

Location:
src/common
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/common/Errors.ma

    r1599 r1601  
    1818include "basics/lists/list.ma".
    1919include "common/PreIdentifiers.ma".
    20 include "utilities/lists.ma".
    21 include "utilities/deppair.ma".
     20include "basics/lists/list.ma".
     21include "basics/russell.ma".
    2222
    2323(* * Error reporting and the error monad. *)
     
    103103λA,B,C,P,e,f.
    104104  match e with
    105   [ OK v ⇒ match v with [ dp v' p ⇒ f (fst … v') (snd … v') ? ]
     105  [ OK v ⇒ match v with [ mk_Sig v' p ⇒ f (fst … v') (snd … v') ? ]
    106106  | Error msg ⇒ Error ? msg
    107107  ].
     
    165165].
    166166whd // %
    167 [ @(use_sig B P)
     167[ @(pi2 … h')
    168168| cases t' #l' #p @p
    169169] qed.
  • src/common/IOMonad.ma

    r1599 r1601  
    6666(match a return λa'.P_io O I A P a' → ? with
    6767 [ Wrong m ⇒ λ_. Wrong O I ? m
    68  | Value c ⇒ λp'. Value ??? (dp A P c p')
     68 | Value c ⇒ λp'. Value ??? (mk_Sig A P c p')
    6969 | Interact out k ⇒ λp'. Interact ??? out (λv. io_inject_0 O I A P (k v) (p' v))
    7070 ]) p.
     
    8181match a with
    8282[ Wrong m ⇒ Wrong ??? m
    83 | Value b ⇒ match b with [ dp w p ⇒ Value ??? w]
     83| Value b ⇒ match b with [ mk_Sig w p ⇒ Value ??? w]
    8484| Interact out k ⇒ Interact ??? out (λv. io_eject ?? A P (k v))
    8585].
     
    9595
    9696lemma sig_bindIO_OK: ∀O,I,A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:IO O I (Sig A P). ∀f:Sig A P → IO O I B.
    97   (∀v:A. ∀p:P v. P_io O I ? P' (f (dp A P v p))) →
     97  (∀v:A. ∀p:P v. P_io O I ? P' (f (mk_Sig A P v p))) →
    9898  P_io O I ? P' (bindIO O I (Sig A P) B e f).
    9999#O #I #A #B #P #P' #e #f elim e;
  • src/common/Identifiers.ma

    r1562 r1601  
    33include "utilities/binary/positive.ma".
    44include "common/Errors.ma".
    5 include "utilities/option.ma".
    65
    76(* identifiers and their generators are tagged to differentiate them, and to
  • src/common/PositiveMap.ma

    r1566 r1601  
    11include "basics/types.ma".
    2 include "utilities/option.ma".
    32include "utilities/binary/positive.ma".
    43
  • src/common/StructuredTraces.ma

    r1583 r1601  
    6464        as_execute S status_pre_fun_call status_start_fun_call →
    6565        ∀H:as_classifier S status_pre_fun_call cl_call.
    66           as_after_return S (dp ?? status_pre_fun_call H) status_after_fun_call →
     66          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call →
    6767          trace_label_return S status_start_fun_call status_after_fun_call →
    6868          trace_any_label S end_flag status_after_fun_call status_final →
     
    118118        as_execute S status_pre_fun_call status_start_fun_call →
    119119        ∀H:as_classifier S status_pre_fun_call cl_call.
    120           as_after_return S (dp ?? status_pre_fun_call H) status_after_fun_call →
     120          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call →
    121121          trace_label_return S status_start_fun_call status_after_fun_call →
    122122          trace_any_call S status_after_fun_call status_final →
Note: See TracChangeset for help on using the changeset viewer.