Changeset 1084 for src/ERTL/ERTLToLTL.ma


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

more added on ertl pass: not sure how much should be axiomatised wrt register colouring

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1082 r1084  
    11include "ERTL/ERTL.ma".
     2include "ERTL/ERTLToLTLI.ma".
    23include "LTL/LTL.ma".
     4
     5definition translate_funct ≝
     6  λname_def.
     7  let 〈name, def〉 ≝ name_def in
     8  let def' ≝
     9    match def with
     10    [ Internal def ⇒ Internal ? (translate_internal name def)
     11    | External def ⇒ External ? def
     12    ]
     13  in
     14    〈name, def'〉.
     15
     16definition translate ≝
     17  λp.
     18  let functs' ≝ map ? ? translate_funct (ertl_pr_functs p) in
     19    mk_ltl_program (ertl_pr_globals p) functs' (ertl_pr_main p).
Note: See TracChangeset for help on using the changeset viewer.