Ignore:
Timestamp:
Jul 18, 2011, 5:21:14 PM (9 years ago)
Author:
mulligan
Message:

nearly completed rtl -> ertl pass removing all option types with dep. types

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/RegisterSet.ma

    r782 r1075  
    66  rs_set: Type[0];
    77  rs_empty: rs_set;
    8   rs_singleton: register → rs_set;
    9   rs_fold: ∀A: Type[0]. (register → A → A) → rs_set → A → A;
    10   rs_insert: register → rs_set → rs_set;
    11   rs_exists: register → rs_set → bool;
     8  rs_singleton: Register → rs_set;
     9  rs_fold: ∀A: Type[0]. (Register → A → A) → rs_set → A → A;
     10  rs_insert: Register → rs_set → rs_set;
     11  rs_exists: Register → rs_set → bool;
    1212  rs_union: rs_set → rs_set → rs_set;
    13   rs_to_list: rs_set → list register;
    14   rs_from_list: list register → rs_set
     13  rs_to_list: rs_set → list Register;
     14  rs_from_list: list Register → rs_set
    1515}.
    1616
    1717(* dpm: horrendously inefficient, but will do for now *)
    1818
    19 definition rs_list_set_empty: list register ≝ [ ].
     19definition rs_list_set_empty: list Register ≝ [ ].
    2020
    21 definition rs_list_set_singleton: register → list register ≝ λr. [ r ].
     21definition rs_list_set_singleton: Register → list Register ≝ λr. [ r ].
    2222
    2323definition rs_list_set_fold ≝
    2424  λA: Type[0].
    25   λf: register → A → A.
    26   λl: list register.
     25  λf: Register → A → A.
     26  λl: list Register.
    2727  λa: A.
    2828    foldr ? ? f a l.
    2929   
    3030definition rs_list_set_insert ≝
    31   λr: register.
    32   λs: list register.
    33   match member ? (eq_identifier ?) r s with
     31  λr: Register.
     32  λs: list Register.
     33  match member ? eq_Register r s with
    3434  [ true ⇒ r :: s
    3535  | false ⇒ s
     
    3737 
    3838definition rs_list_set_exists ≝
    39   λr: register.
    40   λs: list register.
    41     member ? (eq_identifier ?) r s.
     39  λr: Register.
     40  λs: list Register.
     41    member ? eq_Register r s.
    4242   
    4343definition rs_list_set_union ≝
    44   λr: list register.
    45   λs: list register.
    46     nub_by ? (eq_identifier ?) (r @ s).
     44  λr: list Register.
     45  λs: list Register.
     46    nub_by ? eq_Register (r @ s).
    4747 
    4848definition rs_list_set_from_list ≝
    49   λr: list register.
    50     nub_by ? (eq_identifier ?) r.
     49  λr: list Register.
     50    nub_by ? eq_Register r.
    5151 
    5252definition register_list_set: register_set ≝
    53   mk_register_set (list register) rs_list_set_empty
     53  mk_register_set (list Register) rs_list_set_empty
    5454                  rs_list_set_singleton rs_list_set_fold
    5555                  rs_list_set_insert rs_list_set_exists
Note: See TracChangeset for help on using the changeset viewer.