Changeset 1515 for src/ERTL/ERTLToLTL.ma


Ignore:
Timestamp:
Nov 18, 2011, 1:03:14 PM (9 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/ERTL/ERTLToLTL.ma

    r1424 r1515  
    380380  ].
    381381
    382 definition bvt_fold ≝
    383   λa, b: Type[0].
    384   λf: label → a → b → b.
    385   λtrie: BitVectorTrie a 16.
    386   λseed: b.
    387     let f' ≝ λbv: BitVector 16. λa. λb.
    388       f (an_identifier LabelTag bv) a b
    389     in
    390       bvtfold_aux a b f' seed 16 ? trie [[]].
    391   //
    392 qed.
    393 
    394382definition graph_fold ≝
    395383  λglobals.
     
    398386  λgraph: graph (ertl_statement globals).
    399387  λseed : b.
    400   match graph with
    401   [ an_id_map tree ⇒ bvt_fold (ertl_statement globals) b f tree seed
    402   ]. 
     388    foldi (ertl_statement globals) b ? f graph seed.
    403389
    404390definition translate_internal: ∀globals: list ident.
Note: See TracChangeset for help on using the changeset viewer.