source: src/ERTL/ERTLToLTL.ma @ 1110

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

changes to get ltl to lin pass to work properly

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