source: src/ERTL/ERTLToLTL.ma @ 1084

Last change on this file since 1084 was 1084, checked in by mulligan, 9 years ago

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

File size: 490 bytes
Line 
1include "ERTL/ERTL.ma".
2include "ERTL/ERTLToLTLI.ma".
3include "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 TracBrowser for help on using the repository browser.