Changeset 1515 for src/Clight/fresh.ma


Ignore:
Timestamp:
Nov 18, 2011, 1:03:14 PM (8 years ago)
Author:
campbell
Message:

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/fresh.ma

    r1207 r1515  
    1111λa,b. match a with [ an_identifier a ⇒
    1212      match b with [ an_identifier b ⇒
    13         an_identifier ? (max_u ? a b)
     13        an_identifier ? (max a b)
    1414      ]].
    1515
    1616definition max_id_of_env : list (ident × type) → ident ≝
    17 foldr ?? (λit,id. max_id (\fst it) id) (an_identifier ? (zero ?)).
     17foldr ?? (λit,id. max_id (\fst it) id) (an_identifier ? one).
    1818
    1919definition max_id_of_fn : function → ident ≝
     
    2727
    2828definition max_id_of_functs : list (ident × clight_fundef) → ident ≝
    29 foldr ?? (λidf,id. max_id (max_id (\fst idf) (max_id_of_fundef (\snd idf))) id) (an_identifier ? (zero ?)).
     29foldr ?? (λidf,id. max_id (max_id (\fst idf) (max_id_of_fundef (\snd idf))) id) (an_identifier ? one).
    3030
    3131definition max_id_of_globvars : list (ident × region × (list init_data × type)) → ident ≝
    32 foldr ?? (λit,id. max_id (\fst (\fst it)) id) (an_identifier ? (zero ?)).
     32foldr ?? (λit,id. max_id (\fst (\fst it)) id) (an_identifier ? one).
    3333
    3434definition max_id_of_program : clight_program → ident ≝
     
    3939definition universe_for_program : clight_program → universe SymbolTag ≝
    4040λp. match max_id_of_program p with [ an_identifier i ⇒
    41       let next ≝ increment ? i in
    42       mk_universe SymbolTag next (eq_bv ? next (zero ?))
     41      let next ≝ succ i in
     42      mk_universe SymbolTag next
    4343    ].
Note: See TracChangeset for help on using the changeset viewer.