source: src/LIN/LIN.ma @ 1264

Last change on this file since 1264 was 1264, checked in by sacerdot, 8 years ago

Almost ported to new Joint syntax.

File size: 1.0 KB
RevLine 
[1168]1include "joint/Joint.ma".
[1246]2include "utilities/lists.ma".
[491]3
[1246]4definition lin_params_: params_ ≝
5 mk_params_ (mk_params__ unit unit unit unit registers_move Register False unit unit unit) unit.
[1168]6
[1246]7definition pre_lin_statement ≝ joint_statement lin_params_.
[1168]8
[757]9definition well_formed_P ≝
[723]10  λA, B: Type[0].
11  λcode: list (option A × B).
12    match code with
13    [ nil ⇒ False
14    | cons hd tl ⇒
15      match \fst hd with
16      [ Some lbl ⇒ False
[1233]17      | None ⇒ True]].
[1224]18
[1246]19definition lin_statement ≝ λglobals.(option label) × (pre_lin_statement globals).
20
21definition lin_params: ∀globals. params globals ≝
[1224]22 λglobals.
[1246]23  mk_params globals lin_params_ (Σcode:list (lin_statement globals). well_formed_P … code)
24   (λcode:Σcode.?. λl.
25    find ?? (λs. let 〈l',x〉 ≝ s in
26     match l' with [ None ⇒ None … | Some l'' ⇒ if eq_identifier … l l'' then Some … x else None ?]) code).
[1224]27
[1264]28definition lin_function ≝ λglobals. joint_function … (lin_params globals).
29
[1250]30definition lin_program ≝ joint_program lin_params.
Note: See TracBrowser for help on using the repository browser.