Changeset 1470


Ignore:
Timestamp:
Oct 27, 2011, 5:29:32 PM (8 years ago)
Author:
mulligan
Message:

finished, pretty ugly though as matita's disambiguation is a nightmare, so had to use tactics in some places

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/ProofUtils.ma

    r1469 r1470  
    158158    [ None ⇒ ⊥ (* XXX: should not happen *)
    159159    | Some statement ⇒
     160      let entered_previously ≝ ? in
    160161      let visited ≝ insert … entry_point' true visited in
    161       let entered_previously ≝ ? in
    162162      match entered_previously return λe: bool. ((BitVectorTrie Word 16) × (BitVectorTrie bool 16) × (codeT globals (graph_params params1 globals))) with
    163163      [ true ⇒ 〈map, visited, the_graph〉
     
    206206      〈map, the_graph〉.
    207207
    208 axiom relabel_graph':
    209   ∀params1: params1.
    210   ∀globals: list ident.
    211   ∀the_graph: codeT globals (graph_params params1 globals).
    212   ∀map: BitVectorTrie Word 16.
    213   ∀visited: BitVectorTrie bool 16.
    214   ∀num_nodes: nat.
    215     codeT globals (graph_params params1 globals).
     208let rec relabel_graph'
     209  (params1: params1) (globals: list ident)
     210    (the_graph: codeT globals (graph_params params1 globals)) (map: BitVectorTrie Word 16)
     211      (visited: BitVectorTrie bool 16) (entry_point: label) (size_counter: nat)
     212        on size_counter: codeT globals (graph_params params1 globals) ≝
     213  match size_counter return λs: nat. codeT globals (graph_params params1 globals) with
     214  [ O ⇒ empty_graph …
     215  | S size_counter ⇒
     216    let entry_point' ≝ match entry_point with [ an_identifier e ⇒ e ] in
     217    let relabelled_entry_point ≝ an_identifier LabelTag ? in
     218    let statement ≝ lookup LabelTag ? the_graph entry_point in
     219    match statement return λs: option (joint_statement (graph_params params1 globals) globals). codeT globals (graph_params params1 globals) with
     220    [ None ⇒ ⊥ (* XXX: should not happen *)
     221    | Some statement ⇒
     222      let entered_previously ≝ ? in
     223      let visited ≝ insert … entry_point' true visited in
     224      match entered_previously return λe: bool. codeT globals (graph_params params1 globals) with
     225      [ true ⇒ the_graph
     226      | false ⇒ (* XXX: never visited here before *)
     227        match statement return λs: joint_statement (graph_params params1 globals) globals. codeT globals (graph_params params1 globals) with
     228        [ sequential seq l ⇒
     229          let l' ≝ match l with [ an_identifier l ⇒ l ] in
     230          let 〈the_graph, new_seq〉 ≝
     231            match seq return λs. (codeT globals (graph_params params1 globals)) × ? with
     232            [ COND acc_a cond_label ⇒
     233              let cond_label' ≝ match cond_label with [ an_identifier l ⇒ l ] in
     234              let relabelled ≝ an_identifier LabelTag ? in
     235              let tail_graph ≝ relabel_graph' params1 globals the_graph map visited cond_label size_counter in
     236                〈tail_graph, COND … acc_a relabelled〉
     237            | _ ⇒ 〈the_graph, seq〉
     238            ]
     239          in
     240            match size_counter with
     241            [ O ⇒ ⊥ (* XXX: impossible *)
     242            | S size_counter ⇒
     243              let tail_graph ≝ relabel_graph' params1 globals the_graph map visited l size_counter in
     244              let relabelled ≝ an_identifier LabelTag ? in
     245                add LabelTag … tail_graph relabelled_entry_point (sequential … new_seq relabelled)
     246            ]
     247        | RETURN ⇒ the_graph
     248        | GOTO l ⇒
     249          let l' ≝ match l with [ an_identifier l ⇒ l ] in
     250          let relabelled ≝ an_identifier LabelTag ? in
     251            add LabelTag … the_graph relabelled_entry_point (GOTO … relabelled)         
     252        ]
     253      ]
     254    ]
     255  ].
     256  [3: @(lookup … l' map l')
     257  |4: @(lookup … cond_label' map cond_label')
     258  |5: @(lookup … l' map l')
     259  |6: @(lookup … entry_point' visited false)
     260  |7: @(lookup … entry_point' map entry_point')
     261  |*: cases daemon
     262  ]
     263qed.
    216264
    217265definition relabel_graph ≝
     
    219267  λglobals: list ident.
    220268  λthe_graph: codeT globals (graph_params params1 globals).
     269  λentry_point: label.
    221270  λmap: BitVectorTrie Word 16.
    222     relabel_graph' params1 globals the_graph map (Stub …) (graph_num_nodes … the_graph).
     271    relabel_graph' params1 globals the_graph map (Stub …) entry_point (graph_num_nodes … the_graph).
    223272
    224273definition pre_erase_graph_joint_internal_function ≝
     
    238287    [ dp exit exit_prf ⇒
    239288      let 〈maps, code〉 ≝ pre_erase_graph_internal_function params1 globals code entry in
    240       let code ≝ relabel_graph params1 globals code maps in
     289      let code ≝ relabel_graph params1 globals code entry maps in
    241290        mk_joint_internal_function …
    242291          luniverse runiverse result params
Note: See TracChangeset for help on using the changeset viewer.