Changeset 1466 for src/joint


Ignore:
Timestamp:
Oct 26, 2011, 5:08:59 PM (8 years ago)
Author:
mulligan
Message:

erasure for graph based joint languages almost complete

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/ProofUtils.ma

    r1463 r1466  
    5454qed.
    5555
    56 definition relabel_lin_instruction:
    57     ∀globals: list ident. BitVectorTrie Word 16 → joint_instruction lin_params_ globals → joint_instruction lin_params_ globals ≝
    58   λglobals: list ident.
     56definition relabel_joint_instruction:
     57    ∀globals: list ident.
     58    ∀params: params_.
     59      BitVectorTrie Word 16 → joint_instruction params globals → joint_instruction params globals ≝
     60  λglobals: list ident.
     61  λparams.
    5962  λmap.
    6063  λinstr.
     
    6366    let lbl ≝ match lbl with [ an_identifier lbl ⇒ lbl ] in
    6467    let located ≝ an_identifier LabelTag (lookup … lbl map lbl) in
    65       COND lin_params_ globals acc_a located
     68      COND params globals acc_a located
    6669  | _ ⇒ instr
    6770  ].
    6871
    69 definition relabel_lin_statement:
    70     ∀globals: list ident. BitVectorTrie Word 16 → pre_lin_statement globals → pre_lin_statement globals ≝
    71   λglobals: list ident.
     72definition relabel_joint_statement:
     73  ∀globals: list ident.
     74  ∀params: params_.
     75    BitVectorTrie Word 16 → joint_statement params globals → joint_statement params globals ≝
     76  λglobals: list ident.
     77  λparams: params_.
    7278  λmap: BitVectorTrie Word 16.
    73   λstmt: pre_lin_statement globals.
     79  λstmt: joint_statement params globals.
    7480  match stmt with
    7581  [ 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
     82    let relabelled ≝ relabel_joint_instruction globals params map seq in
     83      sequential params globals relabelled l
     84  | RETURN ⇒ RETURN params globals
    7985  | GOTO l ⇒
    8086    let l ≝ match l with [ an_identifier l ⇒ l ] in
    8187    let located ≝ an_identifier LabelTag (lookup … l map l) in
    82       GOTO lin_params_ globals located
     88      GOTO params globals located
    8389  ].
    8490
     
    9197  | cons hd tl ⇒
    9298    let 〈label, stmt〉 ≝ hd in
    93     let relabelled ≝ relabel_lin_statement globals map stmt in
     99    let relabelled ≝ relabel_joint_statement globals lin_params_ map stmt in
    94100    let label ≝
    95101      match label with
     
    127133  λprogram.
    128134    transform_program … program (transf_fundef … (pre_erase_lin_internal_function …)).
     135
     136include "joint/SemanticUtils.ma".
     137
     138definition empty_graph ≝
     139  λa: Type[0].
     140    an_id_map LabelTag a (Stub a 16).
     141
     142let rec pre_erase_graph_internal_function'
     143  (params1: params1) (sem_params: sem_params) (globals: list ident)
     144    (state: state sem_params) (the_graph: codeT globals (graph_params params1 globals))
     145      (labels: list label) (num_nodes: nat)
     146        on num_nodes: ((BitVectorTrie Word 16) × (codeT globals (graph_params params1 globals))) ≝
     147  match num_nodes return λn. ((BitVectorTrie Word 16) × (codeT globals (graph_params params1 globals))) with
     148  [ O ⇒
     149    match labels with
     150    [ nil ⇒ 〈Stub Word 16, empty_graph …〉
     151    | _   ⇒ ⊥
     152    ]
     153  | S num_nodes ⇒
     154    let program_counter ≝ (pc … state) in
     155      match code_pointer_of_address program_counter with
     156      [ OK code_pointer ⇒
     157        match graph_label_of_pointer code_pointer with
     158        [ OK lbl ⇒
     159          match lookup … the_graph lbl with
     160          [ Some statement ⇒
     161            let lbl' ≝ match lbl with [ an_identifier lbl ⇒ lbl ] in
     162            let state ≝ set_pc … program_counter state in
     163            match statement with
     164            [ sequential seq l ⇒
     165              match seq with
     166              [ COST_LABEL cost_label ⇒ pre_erase_graph_internal_function' params1 sem_params globals state the_graph (lbl :: labels) num_nodes
     167              | _ ⇒
     168                let 〈maps, instructions〉 ≝ pre_erase_graph_internal_function' params1 sem_params globals state the_graph labels num_nodes in
     169                let maps ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l lbl' map ]) maps (lbl :: labels) in
     170                  〈maps, instructions〉
     171              ]
     172            | _ ⇒
     173              let 〈maps, instructions〉 ≝ pre_erase_graph_internal_function' params1 sem_params globals state the_graph labels num_nodes in
     174              let maps ≝ foldr … (λl. λmap. match l with [ an_identifier l ⇒ insert … l lbl' map ]) maps (lbl :: labels) in
     175                〈maps, instructions〉
     176            ]
     177          | None           ⇒ ⊥ (* XXX: shouldn't happen *)
     178          ]
     179        | Error message ⇒ ⊥ (* XXX: shouldn't happen *)
     180        ]
     181      | Error message   ⇒ ⊥ (* XXX: shouldn't happen *)
     182      ]
     183  ].
     184  cases daemon (* XXX *)
     185qed.
     186
     187definition pre_erase_graph_internal_function ≝
     188  λparams1: params1.
     189  λsem_params: sem_params.
     190  λglobals: list ident.
     191  λstate: state sem_params.
     192  λthe_graph: codeT globals (graph_params params1 globals).
     193  λlabels: list label.
     194    pre_erase_graph_internal_function' params1 sem_params globals state the_graph labels (graph_num_nodes … the_graph).
     195
     196let rec relabel_graph'
     197  (params1: params1) (sem_params: sem_params) (globals: list ident)
     198    (state: state sem_params) (the_graph: codeT globals (graph_params params1 globals))
     199      (map: BitVectorTrie Word 16) (num_nodes: nat)
     200        on num_nodes: codeT globals (graph_params params1 globals) ≝
     201  match num_nodes with
     202  [ O ⇒ empty_graph …
     203  | S num_nodes ⇒
     204    let program_counter ≝ (pc … state) in
     205    match code_pointer_of_address program_counter with
     206    [ OK code_pointer ⇒
     207      match graph_label_of_pointer code_pointer with
     208      [ OK lbl ⇒
     209        match lookup … the_graph lbl with
     210        [ Some statement ⇒
     211          let lbl' ≝ match lbl with [ an_identifier lbl ⇒ lbl ] in
     212          let new_statement ≝ relabel_joint_statement globals (graph_params params1 globals) map statement in
     213          let new_lbl ≝ an_identifier LabelTag ? in
     214          let state' ≝ set_pc … program_counter state in
     215          let tail_graph ≝ relabel_graph' params1 sem_params globals state' the_graph map num_nodes in
     216            add … tail_graph new_lbl new_statement
     217        | None ⇒ ⊥
     218        ]
     219      | Error message ⇒ ⊥
     220      ]
     221    | Error message ⇒ ⊥
     222    ]         
     223  ].
     224  [2: @(lookup … lbl' map lbl')
     225  |*: cases daemon (* XXX *)
     226  ]
     227qed.
     228
     229definition relabel_graph ≝
     230  λparams1.
     231  λsem_params.
     232  λglobals.
     233  λstate: state sem_params.
     234  λthe_graph: codeT globals (graph_params params1 globals).
     235  λmap: BitVectorTrie Word 16.
     236    relabel_graph' params1 sem_params globals state the_graph map (graph_num_nodes … the_graph).
     237
     238definition pre_erase_graph_joint_internal_function ≝
     239  λparams1: params1.
     240  λsem_params: sem_params.
     241  λglobals: list ident.
     242  λstate: state sem_params.
     243  λint_fun: joint_internal_function globals (graph_params params1 globals).
     244  let luniverse ≝ joint_if_luniverse globals (graph_params params1 globals) int_fun in
     245  let runiverse ≝ joint_if_runiverse … int_fun in
     246  let result ≝ joint_if_result … int_fun in
     247  let params ≝ joint_if_params … int_fun in
     248  let locals ≝ joint_if_locals … int_fun in
     249  let stacksize ≝ joint_if_stacksize … int_fun in
     250  let code ≝ joint_if_code … int_fun in
     251  let entry ≝ ? in
     252  let exit ≝ ? in
     253  let 〈maps, code〉 ≝ pre_erase_graph_internal_function params1 sem_params globals state code [ ] in
     254  let code ≝ relabel_graph params1 sem_params globals state code maps in
     255      mk_joint_internal_function …
     256        luniverse runiverse result params
     257        locals stacksize code entry exit.
     258  cases daemon (* XXX *)
     259qed.
     260
     261(* XXX: use make_initial_state to build an initial state for a program *)
Note: See TracChangeset for help on using the changeset viewer.