Changeset 1274


Ignore:
Timestamp:
Sep 26, 2011, 5:58:21 PM (8 years ago)
Author:
mulligan
Message:

starting removing axioms from adts and giving them proper implementations

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1271 r1274  
    501501      ]) (joint_if_code globals (ertl_params globals) int_fun) 〈graph, joint_if_luniverse … int_fun〉
    502502  in
    503     mk_joint_internal_function globals (ltl_params globals)
    504       luniv (joint_if_runiverse … int_fun)
    505         it it it (joint_if_stacksize … int_fun)
    506           graph ? ?.
    507   cases daemon (* XXX *)
     503    match joint_if_entry … int_fun with
     504    [ dp entry_label entry_label_prf ⇒
     505      match joint_if_exit … int_fun with
     506      [ dp exit_label exit_label_prf ⇒
     507          mk_joint_internal_function globals (ltl_params globals)
     508            luniv (joint_if_runiverse … int_fun)
     509              it it it (joint_if_stacksize … int_fun)
     510                graph ? ?
     511      ]
     512    ].
     513  [1: %
     514    [1: @entry_label
     515    |2: cases daemon (* XXX *)
     516    ]
     517  |2: %
     518    [1: @exit_label
     519    |2: cases daemon (* XXX *)
     520    ]
     521  ]
    508522qed.
    509523
    510 definition ertl_to_ltl : ertl_program → ltl_program ≝
    511  λp. transform_program … p (transf_fundef … (translate_internal …)).
     524definition ertl_to_ltl: ertl_program → ltl_program ≝
     525  λp.
     526    transform_program … p (transf_fundef … (translate_internal …)).
  • src/utilities/adt/table_adt.ma

    r1223 r1274  
    66
    77include "utilities/adt/equal.ma".
     8include "utilities/adt/ordering.ma".
    89
    910include "ASM/Util.ma".
    1011
    11 axiom table: Type[0] → Type[0] → Type[0].
     12inductive table (dom_type: Type[0]) (rng_type: Type[0]): Type[0] ≝
     13  | empty: table dom_type rng_type
     14  | node : nat → dom_type → rng_type → table dom_type rng_type → table dom_type rng_type → table dom_type rng_type.
    1215 
    13 axiom tbl_empty  : ∀key_type, rng_type. table key_type rng_type.
    14 axiom tbl_size   : ∀key_type, rng_type. table key_type rng_type → nat.
    15  
    16 axiom tbl_to_list: ∀key_type, rng_type. table key_type rng_type → list (key_type × rng_type).
     16definition tbl_empty ≝ empty.
     17
     18definition tbl_size ≝
     19  λdom_type : Type[0].
     20  λrng_type : Type[0].
     21  λthe_table: table dom_type rng_type.
     22  match the_table with
     23  [ empty ⇒ 0
     24  | node sz key val l r ⇒ sz
     25  ].
     26
     27let rec tbl_to_list
     28  (dom_type: Type[0]) (rng_type: Type[0]) (the_table: table dom_type rng_type)
     29    on the_table: list (dom_type × rng_type) ≝
     30  match the_table with
     31  [ empty ⇒ [ ]
     32  | node sz key val l r ⇒ 〈key, val〉 :: tbl_to_list … l @ tbl_to_list … r
     33  ].
    1734 
    1835axiom tbl_insert : ∀key_type, rng_type. key_type → rng_type → table key_type rng_type → table key_type rng_type.
     36
     37axiom tbl_merge:
     38  ∀key_type, rng_type.
     39    (key_type → key_type → order) → table key_type rng_type → table key_type rng_type → table key_type rng_type.
     40
    1941axiom tbl_remove : ∀key_type, rng_type. key_type → table key_type rng_type → table key_type rng_type.
    2042 
    21 axiom tbl_find   : ∀key_type, rng_type. key_type → table key_type rng_type → option rng_type.
    22 axiom tbl_update : ∀key_type, rng_type. key_type → (rng_type → rng_type) → table key_type rng_type →
    23                     table key_type rng_type.
     43let rec tbl_find
     44  (dom_type: Type[0]) (rng_type: Type[0]) (ord: dom_type → dom_type → order)
     45    (to_find: dom_type) (the_table: table dom_type rng_type)
     46      on the_table: option rng_type ≝
     47  match the_table with
     48  [ empty               ⇒ None …
     49  | node sz key val l r ⇒
     50    match ord to_find key with
     51    [ order_lt ⇒ tbl_find … ord to_find l
     52    | order_eq ⇒ Some … val
     53    | order_gt ⇒ tbl_find … ord to_find r
     54    ]
     55  ].
     56
     57let rec tbl_update
     58  (dom_type: Type[0]) (rng_type: Type[0]) (ord: dom_type → dom_type → order)
     59    (to_find: dom_type) (update: rng_type → rng_type)
     60      (the_table: table dom_type rng_type)
     61        on the_table: table dom_type rng_type ≝
     62  match the_table with
     63  [ empty               ⇒ empty …
     64  | node sz key val l r ⇒
     65    match ord to_find key with
     66    [ order_lt ⇒ tbl_update … ord to_find update l
     67    | order_eq ⇒ node … sz key (update val) l r
     68    | order_gt ⇒ tbl_update … ord to_find update r
     69    ]
     70  ].
     71
     72let rec tbl_forall
     73  (dom_type: Type[0]) (rng_type: Type[0]) (f: rng_type → bool)
     74    (the_table: table dom_type rng_type)
     75      on the_table: bool ≝
     76  match the_table with
     77  [ empty               ⇒ true
     78  | node sz key val l r ⇒ f val ∧ tbl_forall … f l ∧ tbl_forall … f r
     79  ].
    2480 
    25 axiom tbl_forall : ∀key_type, rng_type. (rng_type → bool) → table key_type rng_type → bool.
    26 axiom tbl_exists : ∀key_type, rng_type. (rng_type → bool) → table key_type rng_type → bool.
    27 axiom tbl_filter : ∀key_type, rng_type. (rng_type → bool) → table key_type rng_type → table key_type rng_type.
     81let rec tbl_exists
     82  (dom_type: Type[0]) (rng_type: Type[0]) (f: rng_type → bool)
     83    (the_table: table dom_type rng_type)
     84      on the_table: bool ≝
     85  match the_table with
     86  [ empty               ⇒ false
     87  | node sz key val l r ⇒ f val ∨ tbl_exists … f l ∨ tbl_exists … f r
     88  ].
    2889 
    2990axiom tbl_equal  : ∀key_type, rng_type. table key_type rng_type
    3091                    → table key_type rng_type → bool.
    31  
    32 axiom tbl_mapi   : ∀key_type, rng_type. ∀a: Type[0]. (key_type → rng_type → a)
    33                    → table key_type rng_type → table key_type a.
    34 axiom tbl_map    : ∀key_type, rng_type. ∀a: Type[0]. (rng_type → a) → table key_type rng_type
    35                    → table key_type a.
    36 axiom tbl_fold   : ∀key_type, a, b: Type[0]. (key_type → a → b → b) → table key_type a → b → b.
     92
     93let rec tbl_mapi
     94  (dom_type: Type[0]) (rng_type: Type[0]) (a: Type[0]) (f: dom_type → rng_type → a)
     95    (the_table: table dom_type rng_type)
     96      on the_table: table dom_type a ≝
     97  match the_table with
     98  [ empty               ⇒ empty …
     99  | node sz key val l r ⇒ node  … sz key (f key val) (tbl_mapi … f l) (tbl_mapi … f r)
     100  ].
     101
     102let rec tbl_map
     103  (dom_type: Type[0]) (rng_type: Type[0]) (a: Type[0]) (f: rng_type → a)
     104    (the_table: table dom_type rng_type)
     105      on the_table: table dom_type a ≝
     106  match the_table with
     107  [ empty               ⇒ empty …
     108  | node sz key val l r ⇒ node  … sz key (f val) (tbl_map … f l) (tbl_map … f r)
     109  ].
     110
     111let rec tbl_fold
     112  (dom_type: Type[0]) (a: Type[0]) (b: Type[0]) (f: dom_type → a → b → b)
     113    (the_table: table dom_type a) (seed: b)
     114      on the_table: b ≝
     115  match the_table with
     116  [ empty               ⇒ seed
     117  | node sz key val l r ⇒ tbl_fold … f r (f key val (tbl_fold … f l seed))
     118  ].
    37119
    38120definition tbl_is_empty ≝
     
    57139        tbl_insert … key rng) (tbl_empty …) the_list.
    58140
     141definition tbl_filter ≝
     142  λdom_type : Type[0].
     143  λrng_type : Type[0].
     144  λf        : rng_type → bool.
     145  λthe_table: table dom_type rng_type.
     146  let as_list  ≝ tbl_to_list … the_table in
     147  let filtered ≝ filter … (λx. f (\snd x)) as_list in
     148    tbl_from_list … filtered.
     149
Note: See TracChangeset for help on using the changeset viewer.