source: src/ERTL/ERTLToLTL.ma @ 1128

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

fixed ERTLtoLTLI so it type checks again

File size: 774 bytes
RevLine 
[733]1include "ERTL/ERTL.ma".
[1084]2include "ERTL/ERTLToLTLI.ma".
3include "LTL/LTL.ma".
[1128]4include "ERTL/spill.ma".
[1084]5
[1088]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
[1084]17definition translate_funct ≝
18  λname_def.
19  let 〈name, def〉 ≝ name_def in
20  let def' ≝
21    match def with
22    [ Internal def ⇒ Internal ? (translate_internal name def)
23    | External def ⇒ External ? def
24    ]
25  in
26    〈name, def'〉.
27
28definition translate ≝
29  λp.
30  let functs' ≝ map ? ? translate_funct (ertl_pr_functs p) in
31    mk_ltl_program (ertl_pr_globals p) functs' (ertl_pr_main p).
Note: See TracBrowser for help on using the repository browser.