Changeset 878


Ignore:
Timestamp:
Jun 3, 2011, 5:35:27 PM (8 years ago)
Author:
campbell
Message:

Removal of manually inserted record projections.

Location:
src
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/syntax.ma

    r816 r878  
    3939; f_body      : stmt
    4040}.
    41 (* XXX: matita interpretations bug workaround *)
    42 definition f_stacksize : internal_function → nat ≝
    43 λf.match f with [ mk_internal_function _ _ _ _ s _ ⇒ s ].
    4441
    4542definition Cminor_program ≝ program (fundef internal_function) unit.
  • src/ERTL/ERTL.ma

    r783 r878  
    4949}.
    5050
    51 definition ertl_if_params: ertl_internal_function → nat.
    52   # E
    53   cases E
    54   # H1 # H2 # H3 # H4 # H5 # H6 # H7 # H8
    55   @ H3
    56 qed.
    57 
    58 definition ertl_if_stacksize: ertl_internal_function → nat.
    59   # E
    60   cases E
    61   # H1 # H2 # H3 # H4 # H5 # H6 # H7 # H8
    62   @ H5
    63 qed.
    64 
    6551inductive ertl_function: Type[0] ≝
    6652  | ertl_f_internal: ertl_internal_function → ertl_function
     
    7359  ertl_pr_main: option ident
    7460}.
    75 
    76 definition ertl_pr_vars: ertl_program → list (ident × nat).
    77   # E
    78   cases E
    79   # H1 # H2 # H3
    80   @ H1
    81 qed.
  • src/LIN/LIN.ma

    r757 r878  
    2929  lin_pr_main: option ident
    3030}.
    31 
    32 definition lin_pr_vars:
    33     lin_program → list (ident × nat).
    34   # r
    35   cases r
    36   # H1 # H2 #H3
    37   @ H1
    38 qed.
    39 
    40 definition lin_pr_funcs:
    41   ∀p: lin_program.
    42     list (ident × (lin_function_definition (map ? ? (fst ? ?) (lin_pr_vars p)))).
    43   # r
    44   cases r
    45   # H1 # H2 #H3
    46   @ H2
    47 qed.
  • src/RTL/RTL.ma

    r783 r878  
    4444}.
    4545
    46 definition rtl_if_stacksize: rtl_internal_function → nat.
    47   # R
    48   cases R
    49   # H1 # H2 # H3 # H4 # H5 # H6 # H7 # H8 # H9 # H10
    50   @ H7
    51 qed.
    5246
    5347inductive rtl_function_definition: Type[0] ≝
     
    6155  rtl_pr_main: option ident
    6256}.
    63 
    64 definition rtl_pr_vars: rtl_program → list (ident × nat).
    65   # P
    66   cases P
    67   # H1 # H2 # H3
    68   @ H1
    69 qed.
  • src/RTLabs/import.ma

    r816 r878  
    2323; pf_exit      : nat
    2424}.
    25 (* XXX projection generation with nat broken *)
    26 definition pf_stacksize ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ s _ _ _ ⇒ s ].
    27 definition pf_graph ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ g _ _ ⇒ g ].
    28 definition pf_entry ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ _ e _ ⇒ e ].
    29 definition pf_exit ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ _ _ e ⇒ e ].
    3025
    3126definition make_register :
  • src/RTLabs/syntax.ma

    r816 r878  
    7070; f_exit      : label
    7171}.
    72 (* XXX: matita interpretations bug workaround *)
    73 definition f_stacksize : internal_function → nat ≝
    74 λf.match f with [ mk_internal_function _ _ _ _ _ _ _ s _ _  _ ⇒ s ].
    7572
    7673(* Note that the global variables will be initialised by the code in main
Note: See TracChangeset for help on using the changeset viewer.