Changeset 1463 for src/joint


Ignore:
Timestamp:
Oct 25, 2011, 5:33:53 PM (8 years ago)
Author:
mulligan
Message:

added erasure for lin

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/ProofUtils.ma

    r1458 r1463  
     1include "joint/Joint.ma".
     2include "LIN/LIN.ma".
     3
     4let rec pre_erase_lin_internal_function'
     5  (globals: list ident) (the_program: list (lin_statement globals))
     6    (labels: list label)
     7      on the_program: ((BitVectorTrie Word 16) × (list (lin_statement globals))) ≝
     8  match the_program with
     9  [ nil        ⇒
     10    match labels with
     11    [ nil ⇒ 〈Stub Word 16, [ ]〉 (* XXX: labels should be empty *)
     12    | _   ⇒ ⊥
     13    ]
     14  | cons hd tl ⇒
     15    let 〈lbl, instr〉 ≝ hd in
     16      match lbl with
     17      [ None ⇒
     18        let 〈maps, instructions〉 ≝ pre_erase_lin_internal_function' globals tl labels in
     19          match instr with
     20          [ sequential seq l ⇒
     21            match seq with
     22            [ COST_LABEL cost ⇒ 〈maps, instructions〉
     23            | _ ⇒ 〈maps, 〈None …, instr〉 :: instructions〉
     24            ]
     25          | _ ⇒ 〈maps, 〈None …, instr〉 :: instructions〉
     26          ]
     27      | Some lbl ⇒
     28        let lbl' ≝ match lbl with [ an_identifier lbl ⇒ lbl ] in
     29        match instr with
     30        [ sequential seq l ⇒
     31          match seq with
     32          [ COST_LABEL cost ⇒ pre_erase_lin_internal_function' globals tl (lbl :: labels)
     33          | _ ⇒
     34            let 〈maps, instructions〉 ≝ pre_erase_lin_internal_function' globals tl labels in
     35            let maps ≝ foldr ? ? (λl. λmap.
     36              match l with
     37              [ an_identifier l ⇒ insert … l lbl' map
     38              ]) maps (lbl :: labels)
     39            in
     40              〈maps, instructions〉
     41          ]
     42        | _ ⇒
     43          let 〈maps, instructions〉 ≝ pre_erase_lin_internal_function' globals tl labels in
     44          let maps ≝ foldr ? ? (λl. λmap.
     45            match l with
     46            [ an_identifier l ⇒ insert … l lbl' map
     47            ]) maps (lbl :: labels)
     48          in
     49            〈maps, instructions〉
     50        ]
     51      ]
     52  ].
     53  @daemon
     54qed.
     55
     56definition relabel_lin_instruction:
     57    ∀globals: list ident. BitVectorTrie Word 16 → joint_instruction lin_params_ globals → joint_instruction lin_params_ globals ≝
     58  λglobals: list ident.
     59  λmap.
     60  λinstr.
     61  match instr with
     62  [ COND acc_a lbl ⇒
     63    let lbl ≝ match lbl with [ an_identifier lbl ⇒ lbl ] in
     64    let located ≝ an_identifier LabelTag (lookup … lbl map lbl) in
     65      COND lin_params_ globals acc_a located
     66  | _ ⇒ instr
     67  ].
     68
     69definition relabel_lin_statement:
     70    ∀globals: list ident. BitVectorTrie Word 16 → pre_lin_statement globals → pre_lin_statement globals ≝
     71  λglobals: list ident.
     72  λmap: BitVectorTrie Word 16.
     73  λstmt: pre_lin_statement globals.
     74  match stmt with
     75  [ sequential seq l ⇒
     76    let relabelled ≝ relabel_lin_instruction globals map seq in
     77      sequential lin_params_ globals relabelled it
     78  | RETURN ⇒ RETURN lin_params_ globals
     79  | GOTO l ⇒
     80    let l ≝ match l with [ an_identifier l ⇒ l ] in
     81    let located ≝ an_identifier LabelTag (lookup … l map l) in
     82      GOTO lin_params_ globals located
     83  ].
     84
     85let rec relabel
     86  (globals: list ident) (map: BitVectorTrie Word 16)
     87    (program: list (lin_statement globals))
     88      on program: list (lin_statement globals) ≝
     89  match program with
     90  [ nil        ⇒ [ ]
     91  | cons hd tl ⇒
     92    let 〈label, stmt〉 ≝ hd in
     93    let relabelled ≝ relabel_lin_statement globals map stmt in
     94    let label ≝
     95      match label with
     96      [ None ⇒ None …
     97      | Some label ⇒
     98        let label ≝ match label with [ an_identifier l ⇒ l ] in
     99          Some … (an_identifier LabelTag (lookup … label map label))
     100      ]
     101    in
     102      〈label, relabelled〉 :: relabel globals map tl
     103  ].
     104
     105definition pre_erase_lin_internal_function:
     106    ∀globals: list ident. joint_internal_function globals (lin_params globals) → joint_internal_function globals (lin_params globals) ≝
     107  λglobals.
     108  λfunction.
     109    let luniverse ≝ joint_if_luniverse … function in
     110    let runiverse ≝ joint_if_runiverse … function in
     111    let result ≝ joint_if_result … function in
     112    let params ≝ joint_if_params … function in
     113    let locals ≝ joint_if_locals … function in
     114    let stacksize ≝ joint_if_stacksize … function in
     115    let code ≝ joint_if_code … function in
     116    let entry ≝ ? in
     117    let exit ≝ ? in
     118    let 〈maps, code〉 ≝ pre_erase_lin_internal_function' globals code [ ] in
     119    let code ≝ relabel globals maps code in
     120      mk_joint_internal_function …
     121        luniverse runiverse result params
     122        locals stacksize code entry exit.
     123  cases daemon (* XXX *)
     124qed.
     125
     126definition erase_lin_program: lin_program → lin_program ≝
     127  λprogram.
     128    transform_program … program (transf_fundef … (pre_erase_lin_internal_function …)).
Note: See TracChangeset for help on using the changeset viewer.