source: src/ERTL/ERTLToLTL.ma @ 1124

Last change on this file since 1124 was 1124, checked in by mulligan, 8 years ago

finished off liveness analysis by axiomatising properties

File size: 749 bytes
Line 
1include "ERTL/ERTL.ma".
2include "ERTL/ERTLToLTLI.ma".
3include "LTL/LTL.ma".
4
5definition translate_internal ≝
6  λf.
7  λint_fun: ertl_internal_function.
8    mk_ltl_internal_function ?
9      (ertl_if_luniverse int_fun)
10      (ertl_if_runiverse int_fun)
11      (ertl_if_stacksize int_fun)
12      (ertl_if_graph int_fun)
13      ?
14      ?.
15
16definition translate_funct ≝
17  λname_def.
18  let 〈name, def〉 ≝ name_def in
19  let def' ≝
20    match def with
21    [ Internal def ⇒ Internal ? (translate_internal name def)
22    | External def ⇒ External ? def
23    ]
24  in
25    〈name, def'〉.
26
27definition translate ≝
28  λp.
29  let functs' ≝ map ? ? translate_funct (ertl_pr_functs p) in
30    mk_ltl_program (ertl_pr_globals p) functs' (ertl_pr_main p).
Note: See TracBrowser for help on using the repository browser.