Ignore:
Timestamp:
Dec 19, 2012, 10:38:43 AM (8 years ago)
Author:
piccolo
Message:

linearise modified

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/linearise.ma

    r2547 r2562  
    1414      if nxt ∈ visited then FCOND … I a ltrue nxt else
    1515      sequential (mk_lin_params p) … c it
    16     | _ ⇒ sequential … c it
     16    | _ ⇒ sequential (mk_lin_params p) … c it
    1717    ]
    1818  | final c ⇒ final … c
     
    8888               [ sequential s' nxt ⇒
    8989                 match s' with
    90                  [ step_seq _ ⇒
     90                 [ COND a ltrue ⇒
     91                   Or
     92                    (And (nth_opt … n (rev … generated') =
     93                            Some ? 〈Some ? l, sequential … (COND … a ltrue) it〉)
     94                         (lookup … visited' nxt = Some ? (S n)))
     95                    (nth_opt … n (rev … generated') =
     96                            Some ? 〈Some ? l, FCOND … I a ltrue nxt〉)
     97                 |  _ ⇒
    9198                   And
    9299                     (nth_opt … n (rev … generated') =
     
    95102                      (nth_opt … (S n) (rev … generated') =
    96103                       Some ? 〈None ?, GOTO … nxt〉))
    97                  | COND a ltrue ⇒
    98                    Or
    99                     (And (nth_opt … n (rev … generated') =
    100                             Some ? 〈Some ? l, sequential … (COND … a ltrue) it〉)
    101                          (lookup … visited' nxt = Some ? (S n)))
    102                     (nth_opt … n (rev … generated') =
    103                             Some ? 〈Some ? l, FCOND … I a ltrue nxt〉)
     104               
    104105                 ]
    105106               | final s' ⇒
     
    140141       [ sequential s' nxt ⇒
    141142         match s' with
    142          [ step_seq _ ⇒
    143            And
    144              (nth_opt … n (rev … generated) =
    145                 Some ? 〈Some ? l, sequential … s' it〉)
    146              (match lookup … visited nxt with
    147               [ Some n' ⇒ Or (n' = S n) (nth_opt … (S n) (rev … generated) = Some ? 〈None ?, GOTO … nxt〉)
    148               | None ⇒ And (nth_opt ? 0 visiting = Some ? nxt) (S n = gen_length)
    149               ])
    150          | COND a ltrue ⇒
     143         [ COND a ltrue ⇒
    151144           Or
    152145            (And (nth_opt … n (rev … generated) =
     
    158151            (nth_opt … n (rev … generated) =
    159152                    Some ? 〈Some ? l, FCOND … I a ltrue nxt〉)
     153         | _ ⇒
     154           And
     155             (nth_opt … n (rev … generated) =
     156                Some ? 〈Some ? l, sequential … s' it〉)
     157             (match lookup … visited nxt with
     158              [ Some n' ⇒ Or (n' = S n) (nth_opt … (S n) (rev … generated) = Some ? 〈None ?, GOTO … nxt〉)
     159              | None ⇒ And (nth_opt ? 0 visiting = Some ? nxt) (S n = gen_length)
     160              ])
    160161         ]
    161162       | final s' ⇒
     
    220221           match s with [ COND _ _ ⇒ True | _ ⇒ ¬bool_to_Prop (nxt ∈ visited') ]
    221222         | _ ⇒ True] → P 〈0,∅,[ ]〉) →
    222         (∀s,nxt.
    223           statement = sequential … (step_seq … s) nxt →
    224           nxt ∈ visited' → P 〈1, {(nxt)}, [〈None ?, GOTO (mk_lin_params p) nxt〉]〉) →
     223        (∀nxt.match statement with
     224         [ sequential s nxt' ⇒
     225          match s with [ COND _ _ ⇒ False | _ ⇒
     226            nxt = nxt']
     227         | _ ⇒ False]
     228         → nxt ∈ visited' → P 〈1, {(nxt)}, [〈None ?, GOTO (mk_lin_params p) nxt〉]〉) →
    225229        P add_req_gen ≝ hide_prf ?? in
    226230      graph_visit ???
     
    233237    ] n_prf
    234238  ] (chop_ok ? (λx.x∈visited) visiting).
    235 cases daemon qed. (*)
    236239whd
    237240[ (* base case, visiting is all visited *)
     
    253256    cases s in H3; [3: *]
    254257    [ * ] normalize nodelta
    255     [ #s' #nxt * #EQnth_opt #H %{EQnth_opt}
     258    [1,3: [#f #args #dest |#s'] #nxt * #EQnth_opt #H %{EQnth_opt}
    256259      inversion (lookup … visited nxt) in H; [2: #n'] #EQlookup
    257260      normalize nodelta *
     
    323326|12: (* add_req_gen utility *)
    324327  #P whd in match add_req_gen;
    325   cases statement [ * ] [|*: [ #a #ltrue #lfalse | #s | * ] #H #_ @(H I) ]
    326   #s #nxt normalize nodelta inversion (nxt ∈ visited') #EQ normalize nodelta
    327   #H1 #H2 [ @(H2 … (refl …)) >EQ % | @H1 % * ]
     328  cases statement [ * [#f #args #dest|  #a #ltrue | #s ] #nxt | #s | * ]
     329[2,4: normalize nodelta #H #_ @(H I) ]
     330  normalize nodelta inversion (nxt ∈ visited') #EQ normalize nodelta
     331  #H1 #H2 [1,3: @(H2 … (refl …)) >EQ % |*: @H1 % * ]
    328332|3: elim H #pre ** #H1 #H2 #_
    329333  #i >mem_set_union
    330334  #H elim (orb_Prop_true … H) -H
    331335  [ @add_req_gen_prf [ #_ >mem_set_empty * ]
    332     #s #next #_ #next_vis #H >(mem_set_singl_to_eq … H) %2 assumption
     336    #next #_ #next_vis #H >(mem_set_singl_to_eq … H) %2 assumption
    333337  | >mem_set_union
    334338    #H elim (orb_Prop_true … H) -H
    335339    [ #i_expl %1 @Exists_append_l
    336340      lapply i_expl whd in match translated_statement;
    337       cases statement [ * [ #s | #a #ltrue ] #nxt | #s | *] normalize nodelta #H
     341      cases statement [ * [ #f #args #dest | #a #ltrue | #s ] #nxt | #s | *] normalize nodelta #H
    338342      lapply (mem_list_as_set … H) -H #H
    339       [1,3: @Exists_append_r assumption ]
     343      [1,3,4: @Exists_append_r assumption ]
    340344      cases (nxt ∈ visited') in H; normalize nodelta * [2,4: * [2: * ]]
    341345      #EQ destruct(EQ) [ %1 % |*: %2 %1 % ]
     
    386390        #i_l @orb_Prop_r @orb_Prop_l assumption
    387391      | @add_req_gen_prf
    388         [ #_ | #s #next #_ #next_vis *
     392        [ #_ | #next #_ #next_vis *
    389393          [ whd in ⊢ (??%?→?);
    390394            #EQ' destruct(EQ') whd %{I} >mem_set_union
     
    405409        @add_req_gen_prf
    406410        [ #_
    407         | #s #next #_ #next_vis
     411        | #next #_ #next_vis
    408412          change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
    409413          <associative_append >occurs_exactly_once_None
     
    420424          change with statement in match (lookup_safe ?????);
    421425          cases statement;
    422           [ * [ #s | #a #ltrue ] #nxt | #s | * ] normalize nodelta
    423           [1,2: inversion (nxt ∈ visited') normalize nodelta #nxt_vis ]
    424           [1,2: % | %2 | %1 % ]
    425           [1,3,5,6,8:
     426          [ * [ #f #args #dest | #a #ltrue | #s ] #nxt | #s | * ] normalize nodelta
     427          [1,2,3: inversion (nxt ∈ visited') normalize nodelta #nxt_vis ]
     428          [1,2,5,6: % | %2 | %1 % ]
     429          [1,3,5,7,9,10,12:
    426430            >nth_opt_append_r >rev_length <gen_length_prf try %
    427431            <minus_n_n try % whd in match graph_to_lin_statement; normalize nodelta
     
    429433          |*:
    430434            lapply (in_map_domain … visited' nxt) >nxt_vis normalize nodelta
    431             [ * #n' ] #EQlookup >EQlookup normalize nodelta
    432             [ %2 >nth_opt_append_r >rev_length <gen_length_prf [2: %2 %1 ]
     435            [1,3: * #n' ] #EQlookup >EQlookup normalize nodelta
     436            [1,2: %2 >nth_opt_append_r >rev_length <gen_length_prf [2,4: %2 %1 ]
    433437              <minus_Sn_n %
    434438            |*: %%
     
    448452          normalize nodelta >lin_code_has_label in G1; #K @K
    449453        | @add_req_gen_prf
    450           [ #_ % | #s' #next #_ #_ % ]
     454          [ #_ % |  #next #_ #_ % ]
    451455        ]
    452456      | %{s}
    453457        %{G2}
    454458        cases s in G3;
    455         [ * [ #s | #a #ltrue ] #nxt | #s | * ]
    456         [ * #EQnth_opt #next_spec % | * [*] #EQnth_opt [#next_spec %1 % | %2] | #EQnth_opt ]
    457         [1,3,5,6: @nth_opt_append_hit_l assumption
    458         |*: @(eq_identifier_elim … nxt vis_hd)
     459        [ * [ #f #args #dest | #a #ltrue | #s ] #nxt | #s | * ]
     460        [1,3: * #EQnth_opt #next_spec % | * [*] #EQnth_opt [#next_spec %1 % | %2] | #EQnth_opt ]
     461        [1,3,5,7: @nth_opt_append_hit_l assumption
     462        |2,4,6: @(eq_identifier_elim … nxt vis_hd)
    459463          [1,3: #EQ destruct(EQ) >lookup_add_hit whd [ %1 ]
    460464            lapply (in_map_domain … visited vis_hd)
     
    506510|
    507511]
    508 qed. *)
     512qed.
    509513
    510514(* CSC: The branch compression (aka tunneling) optimization is not implemented
Note: See TracChangeset for help on using the changeset viewer.