Changeset 1601


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
Files:
15 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1515 r1601  
    404404  in
    405405    match joint_if_entry … int_fun with
    406     [ dp entry_label entry_label_prf ⇒
     406    [ mk_Sig entry_label entry_label_prf ⇒
    407407      match joint_if_exit … int_fun with
    408       [ dp exit_label exit_label_prf ⇒
     408      [ mk_Sig exit_label exit_label_prf ⇒
    409409          mk_joint_internal_function globals (ltl_params globals)
    410410            luniv (joint_if_runiverse … int_fun)
  • src/LIN/LIN.ma

    r1379 r1601  
    11include "LIN/joint_LTL_LIN.ma".
    2 include "utilities/lists.ma".
     2include "basics/lists/list.ma".
    33
    44definition lin_params_ : params_ ≝ mk_params_ ltl_lin_params__ unit.
  • src/LIN/semantics.ma

    r1451 r1601  
    2727        match l' with [ None ⇒ false | Some l'' ⇒ if eq_identifier … l l'' then true else false])
    2828     (joint_if_code … (lin_params …) fn)) ;
    29   OK … (inject … (mk_pointer Code (mk_block Code (block_id (pblock old))) ? (mk_offset pos)) ?).
     29  OK … (mk_Sig … (mk_pointer Code (mk_block Code (block_id (pblock old))) ? (mk_offset pos)) ?).
    3030// qed.
    3131
  • src/RTL/RTLToERTL.ma

    r1516 r1601  
    108108  let 〈def, tmpr〉 ≝ fresh_reg … def in
    109109  match reduce_strong ? ? RegisterSTS ret_regs with
    110   [ dp crl crl_proof ⇒
     110  [ mk_Sig crl crl_proof ⇒
    111111    let commonl ≝ \fst (\fst crl) in
    112112    let commonr ≝ \fst (\snd crl) in
     
    124124  λglobals.λstart_lbl: label.
    125125  match reduce_strong ? ? RegisterRets RegisterSTS with
    126   [ dp crl crl_proof ⇒
     126  [ mk_Sig crl crl_proof ⇒
    127127    let commonl ≝ \fst (\fst crl) in
    128128    let commonr ≝ \fst (\snd crl) in
     
    189189  λdef.
    190190  match fresh_regs_strong … globals def 2 with
    191   [ dp def_sra def_sra_proof ⇒
     191  [ mk_Sig def_sra def_sra_proof ⇒
    192192    let def ≝ \fst def_sra in
    193193    let sra ≝ \snd def_sra in
     
    256256  λstart_lbl: label.
    257257  match reduce_strong ? ? RegisterSTS RegisterRets with
    258   [ dp crl first_crl_proof ⇒
     258  [ mk_Sig crl first_crl_proof ⇒
    259259    let commonl ≝ \fst (\fst crl) in
    260260    let commonr ≝ \fst (\snd crl) in
     
    262262    let saves ≝ map2 ? ? ? f_save commonl commonr ? in
    263263    match reduce_strong ? ? ret_regs RegisterSTS with
    264     [ dp crl second_crl_proof ⇒
     264    [ mk_Sig crl second_crl_proof ⇒
    265265      let commonl ≝ \fst (\fst crl) in
    266266      let commonr ≝ \fst (\snd crl) in
  • src/RTLabs/RTLabsToRTL.ma

    r1529 r1601  
    176176  λdef: rtl_internal_function globals.
    177177  match reduce_strong register register srcrs1 srcrs2 with
    178   [ dp reduced first_reduced_proof ⇒
     178  [ mk_Sig reduced first_reduced_proof ⇒
    179179    let srcrsl_common ≝ \fst (\fst reduced) in
    180180    let srcrsr_common ≝ \fst (\snd reduced) in
     
    183183    let srcrs_rest ≝ srcrsl_rest @ srcrsr_rest in
    184184    match reduce_strong register register destrs srcrsl_common with
    185     [ dp reduced second_reduced_proof ⇒
     185    [ mk_Sig reduced second_reduced_proof ⇒
    186186      let destrs_common ≝ \fst (\fst reduced) in
    187187      let destrs_rest ≝ \snd (\fst reduced) in
    188188      match reduce_strong register register destrs_rest srcrs_rest with
    189       [ dp reduced third_reduced_proof ⇒
     189      [ mk_Sig reduced third_reduced_proof ⇒
    190190        let destrs_cted ≝ \fst (\fst reduced) in
    191191        let destrs_rest ≝ \snd (\fst reduced) in
     
    225225        [ true  ⇒ λgood_case.
    226226          match split_into_bytes size const with
    227           [ dp bytes bytes_length_proof ⇒
     227          [ mk_Sig bytes bytes_length_proof ⇒
    228228            let mapped ≝ map2 … (λd. λb. (sequential … (INT rtl_params_ globals d b))) destrs bytes ? in
    229229              adds_graph rtl_params1 globals mapped start_lbl dest_lbl def
     
    269269  λstart_lbl: label.
    270270    match reduce_strong register register destrs srcrs with
    271     [ dp crl_crr len_proof ⇒
     271    [ mk_Sig crl_crr len_proof ⇒
    272272      let commonl ≝ \fst (\fst crl_crr) in
    273273      let commonr ≝ \fst (\snd crl_crr) in
     
    357357    else
    358358      match reduce_strong register register destrs srcrs with
    359       [ dp crl len_proof ⇒
     359      [ mk_Sig crl len_proof ⇒
    360360        let commonl ≝ \fst (\fst crl) in
    361361        let commonr ≝ \fst (\snd crl) in
     
    628628  let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
    629629    match fresh_regs_strong rtl_params0 globals def (|destrs|) with
    630     [ dp def_tmp_destrs tmp_destrs_prf ⇒
     630    [ mk_Sig def_tmp_destrs tmp_destrs_prf ⇒
    631631      let def ≝ \fst def_tmp_destrs in
    632632      let tmp_destrs ≝ \snd def_tmp_destrs in
     
    689689    let save_srcrs2 ≝ translate_move globals tmp_srcrs2 srcrs2 in
    690690    match reduce_strong register register tmp_srcrs1 tmp_srcrs2 with
    691     [ dp crl their_proof ⇒
     691    [ mk_Sig crl their_proof ⇒
    692692      let commonl ≝ \fst (\fst crl) in
    693693      let commonr ≝ \fst (\snd crl) in
     
    826826  | _ ⇒
    827827    match fresh_regs_strong globals def (|destrs|) with
    828     [ dp def_tmp_destrs tmp_destrs_proof ⇒
     828    [ mk_Sig def_tmp_destrs tmp_destrs_proof ⇒
    829829      let def ≝ \fst def_tmp_destrs in
    830830      let tmp_destrs ≝ \snd def_tmp_destrs in
     
    836836      let 〈def, tmpr3〉 ≝ fresh_reg rtl_params1 globals def in
    837837      match complete_regs_strong globals def srcrs1 srcrs2 with
    838       [ dp srcrs12_added srcrs12_proof ⇒
     838      [ mk_Sig srcrs12_added srcrs12_proof ⇒
    839839        let srcrs1 ≝ \fst (\fst srcrs12_added) in
    840840        let srcrs2 ≝ \snd (\fst srcrs12_added) in
     
    893893  λdef: rtl_internal_function globals.
    894894  match fresh_regs_strong globals def (|srcrs1|) with
    895   [ dp def_tmp_srcrs1 srcrs1_prf ⇒
     895  [ mk_Sig def_tmp_srcrs1 srcrs1_prf ⇒
    896896    let def ≝ \fst def_tmp_srcrs1 in
    897897    let tmp_srcrs1 ≝ \snd def_tmp_srcrs1 in
    898898    match fresh_regs_strong globals def (|srcrs2|) with
    899     [ dp def_tmp_srcrs2 srcrs2_prf ⇒
     899    [ mk_Sig def_tmp_srcrs2 srcrs2_prf ⇒
    900900      let def ≝ \fst def_tmp_srcrs2 in
    901901      let tmp_srcrs2 ≝ \snd def_tmp_srcrs2 in
     
    10731073  λdef: rtl_internal_function globals.
    10741074  match fresh_regs_strong rtl_params0 globals def (|addr|) with
    1075   [ dp def_save_addr save_addr_prf ⇒
     1075  [ mk_Sig def_save_addr save_addr_prf ⇒
    10761076    let def ≝ \fst def_save_addr in
    10771077    let save_addr ≝ \snd def_save_addr in
    10781078    match fresh_regs_strong rtl_params0 globals def (|addr|) with
    1079     [ dp def_tmp_addr tmp_addr_prf ⇒
     1079    [ mk_Sig def_tmp_addr tmp_addr_prf ⇒
    10801080      let def ≝ \fst def_tmp_addr in
    10811081      let tmp_addr ≝ \snd def_tmp_addr in
     
    11211121  λdef: rtl_internal_function globals.
    11221122  match fresh_regs_strong rtl_params0 globals def (|addr|) with
    1123   [ dp def_tmp_addr tmp_addr_prf ⇒
     1123  [ mk_Sig def_tmp_addr tmp_addr_prf ⇒
    11241124    let def ≝ \fst def_tmp_addr in
    11251125    let tmp_addr ≝ \snd def_tmp_addr in
  • src/RTLabs/Traces.ma

    r1596 r1601  
    3838    (λs. RTLabs_cost s = true)
    3939    (λs,s'. match s with
    40       [ dp s p ⇒
     40      [ mk_Sig s p ⇒
    4141        match s return λs. RTLabs_classify s = cl_call → ? with
    4242        [ Callstate fd args dst stk m ⇒
  • src/RTLabs/semantics.ma

    r1583 r1601  
    33           compilers yet! *)
    44
    5 include "utilities/lists.ma".
     5include "basics/lists/list.ma".
    66
    77include "common/Errors.ma".
  • 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 →
  • src/joint/BEValues.ma

    r1516 r1601  
    33
    44include "common/Pointers.ma".
    5 include "utilities/sigma.ma".
    65
    76record part (r: region): Type[0] ≝
     
    121120  do p ← pointer_of_bevals [v1;v2] ;
    122121  match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = Code) with
    123   [ Code ⇒ λE.OK ? (inject … p ?)
     122  [ Code ⇒ λE.OK ? (mk_Sig … p ?)
    124123  | _ ⇒ λ_.Error … [MSG NotACodePointer]] ?.
    125124// qed.
  • src/joint/Joint.ma

    r1471 r1601  
    33include "common/AST.ma".
    44include "common/Registers.ma".
    5 include "utilities/sigma.ma". (* CSC: Only for Sigma type projections *)
    65include "common/Graphs.ma".
    76
     
    115114    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    116115    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
    117     (joint_if_code … p) (joint_if_entry … p) (dp … exit prf).
     116    (joint_if_code … p) (joint_if_entry … p) (mk_Sig … exit prf).
    118117
    119118definition set_joint_code ≝
     
    136135  λexit_prf: lookup … graph (joint_if_exit … p) ≠ None ?.
    137136    set_joint_code globals pars p graph
    138       (dp … (joint_if_entry … p) entry_prf) (dp … (joint_if_exit … p) exit_prf).
     137      (mk_Sig … (joint_if_entry … p) entry_prf) (mk_Sig … (joint_if_exit … p) exit_prf).
    139138
    140139definition set_luniverse ≝
  • src/joint/semantics.ma

    r1457 r1601  
    1 include "utilities/lists.ma".
     1include "basics/lists/list.ma".
    22include "joint/BEGlobalenvs.ma".
    33include "common/IO.ma".
Note: See TracChangeset for help on using the changeset viewer.