Ignore:
Timestamp:
Feb 22, 2013, 7:11:30 PM (8 years ago)
Author:
tranquil
Message:

fixed linearise and LINToASM
LINToASM has now correct transformation of idents and labels to Identifier

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/linearise.ma

    r2702 r2708  
    256256    cases s in H3; [3: *]
    257257    [ * ] normalize nodelta
    258     [2,4: [#f #args #dest |#s'] #nxt * #EQnth_opt #H %{EQnth_opt}
    259       inversion (lookup … visited nxt) in H; [2: #n'] #EQlookup
     258    [1,2,4: [ #c | #f #args #dest |#s'] #nxt * #EQnth_opt #H %{EQnth_opt}
     259      inversion (lookup … visited nxt) in H; [2,4,6: #n'] normalize nodelta
     260      #EQlookup
    260261      normalize nodelta *
    261       [ #EQn' %1 >EQn' %
    262       | #H %2{H}
    263       | #H' lapply (All_nth … H … H')
     262      [1,3,5: #EQn' %1 >EQn' %
     263      |2,4,6: #H %2{H}
     264      |*: #H' lapply (All_nth … H … H')
    264265        whd in ⊢ (?%→?); >EQlookup *
    265266      ]
    266     |3: #a #ltrue #lfalse * [2: #H %2{H} ] * #H1 #H2 %1 %{H1}
     267    | #a #ltrue #lfalse * [2: #H %2{H} ] * #H1 #H2 %1 %{H1}
    267268      inversion (lookup … visited lfalse) in H2;
    268269      [ #ABS * #H' lapply (All_nth … H … H')
     
    270271      | #n' #_ normalize nodelta #EQ >EQ %
    271272      ]
    272     | #s #H (*CSC XXXXXXXXXXXXXXXXXXXX @H *)
     273    | #s #H @H
    273274    ]
    274275  ]
     
    326327|12: (* add_req_gen utility *)
    327328  #P whd in match add_req_gen;
    328   cases statement [ * [#f #args #dest|  #a #ltrue | #s ] #nxt | #s | * ]
    329  [2,4: normalize nodelta #l #H1 #H2 lapply (H2 … (refl …)) -H2
    330       cases (l ∈ add …) in H1; normalize nodelta #H1 #H2 try @H2 try @H1 try %
    331       //
    332  |3,5: normalize nodelta [#_] #H #_ @H %
    333  | normalize nodelta in dest nxt ⊢ %; inversion (args ∈ add …) #EQ
    334    normalize nodelta [ @nxt | @dest ] >EQ try % ]
    335 |14: skip
    336 ] cases daemon (*CSC: XXXXXXXXX
     329  cases statement [ * [ #cost | #f #args #dest|  #a #ltrue | #s ] #nxt | #s | * ]
     330  normalize nodelta
     331  [3,5: #H #_ @(H I) ]
     332  inversion (nxt ∈ visited') #EQ normalize nodelta
     333  #H1 #H2 [1,3,5: @(H2 … (refl …)) >EQ % |*: @H1 % * ]
    337334|3: elim H #pre ** #H1 #H2 #_
    338335  #i >mem_set_union
     
    341338    #next #_ #next_vis #H >(mem_set_singl_to_eq … H) %2 assumption
    342339  | >mem_set_union
    343     #H elim (orb_Prop_true … H) -H (*CSC XXXXXXXXXX
     340    #H elim (orb_Prop_true … H) -H
    344341    [ #i_expl %1 @Exists_append_l
    345342      lapply i_expl whd in match translated_statement;
    346       cases statement [ * [ #f #args #dest | #a #ltrue | #s ] #nxt | #s | *] normalize nodelta #H
     343      cases statement [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s | *]
     344      normalize nodelta #H
    347345      lapply (mem_list_as_set … H) -H #H
    348       [1,3,4: @Exists_append_r assumption ]
     346      [1,2,4,5: @Exists_append_r assumption ]
    349347      cases (nxt ∈ visited') in H; normalize nodelta * [2,4: * [2: * ]]
    350348      #EQ destruct(EQ) [ %1 % |*: %2 %1 % ]
     
    366364        #i_vis %2 >mem_set_add @orb_Prop_r assumption
    367365      ]
    368     ]*) cases daemon
     366    ]
    369367  ]
    370368|4,5,6: change with reverse in match rev;
     
    423421        lapply (in_map_domain … visited vis_hd)
    424422        >H3 normalize nodelta //
    425       | %{statement}  (*CSC XXXXXXX
     423      | %{statement}
    426424        %
    427425        [ @lookup_eq_safe
     
    429427          change with statement in match (lookup_safe ?????);
    430428          cases statement;
    431           [ * [ #f #args #dest | #a #ltrue | #s ] #nxt | #s | * ] normalize nodelta
    432           [1,2,3: inversion (nxt ∈ visited') normalize nodelta #nxt_vis ]
    433           [1,2,5,6: % | %2 | %1 % ]
    434           [1,3,5,7,9,10,12:
     429          [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s | * ] normalize nodelta
     430          [1,2,3,4: inversion (nxt ∈ visited') normalize nodelta #nxt_vis ]
     431          [1,2,3,4,7,8: % | %2 | %1 % ]
     432          [1,3,5,7,9,11,13,14,16:
    435433            >nth_opt_append_r >rev_length <gen_length_prf try %
    436             <minus_n_n try % whd in match graph_to_lin_statement; normalize nodelta
    437             >nxt_vis %
     434            <minus_n_n try % try( whd in match graph_to_lin_statement; normalize nodelta
     435            >nxt_vis %)
    438436          |*:
    439437            lapply (in_map_domain … visited' nxt) >nxt_vis normalize nodelta
    440             [1,3: * #n' ] #EQlookup >EQlookup normalize nodelta
    441             [1,2: %2 >nth_opt_append_r >rev_length <gen_length_prf [2,4: %2 %1 ]
    442               <minus_Sn_n %
    443             |*: %%
    444             ]
    445           ]*) cases daemon
     438            [1,3,5: * #n' ] #EQlookup >EQlookup normalize nodelta
     439            try (%% @False)
     440            %2 >nth_opt_append_r >rev_length <gen_length_prf [2,4,6: %2 %1 ]
     441            <minus_Sn_n %
     442          ]
    446443        ]
    447444      ]
    448445    | #NEQ #n_i >(lookup_add_miss … visited … NEQ)
    449       cases daemon (*CSC XXXX
    450446      #Hlookup elim (generated_prf1 … Hlookup)
    451447      #G1 * #s * #G2 #G3
     
    463459        %{G2}
    464460        cases s in G3;
    465         [ * [ #f #args #dest | #a #ltrue | #s ] #nxt | #s | * ]
    466         [1,3: * #EQnth_opt #next_spec % | * [*] #EQnth_opt [#next_spec %1 % | %2] | #EQnth_opt ]
    467         [1,3,5,7: @nth_opt_append_hit_l assumption
    468         |2,4,6: @(eq_identifier_elim … nxt vis_hd)
    469           [1,3: #EQ destruct(EQ) >lookup_add_hit whd [ %1 ]
     461        [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s | * ]
     462        [1,2,4: normalize nodelta #H cases H in ⊢ ?; -H
     463          #EQnth_opt #next_spec % |3: normalize nodelta * [*] #EQnth_opt [#next_spec %1 % | %2] | #EQnth_opt ]
     464        [1,3,5,7,9: @nth_opt_append_hit_l assumption
     465        |2,4,6,8: @(eq_identifier_elim … nxt vis_hd)
     466          [1,3,5,7: #EQ destruct(EQ) >lookup_add_hit whd
     467            [1,2,3: %1]
    470468            lapply (in_map_domain … visited vis_hd)
    471469            >H3 #EQ >EQ in next_spec; * #_ #OK >OK %
    472           |*: #NEQ' >(lookup_add_miss … visited … NEQ')
    473             lapply (in_map_domain … visited nxt)
    474             inversion (nxt ∈ visited) #nxt_vis [1,3: * #n'' ] #EQlookup'
    475             >EQlookup' in next_spec; whd in ⊢ (%→%);
    476             [ * [ #H %1{H} ] #H %2 @nth_opt_append_hit_l assumption
    477             | #H @H
    478             |*: * >H2
     470          |*: #NEQ' >(lookup_add_miss … visited … NEQ') in
     471            ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
     472            generalize in match next_spec in ⊢ ?;
     473            inversion (lookup … visited nxt) normalize nodelta
     474            [2,4,6,8: #n'' ] #EQlookup'
     475            [1,2,3: * [1,3,5: #H %1{H} ] #H %2 @nth_opt_append_hit_l assumption
     476            |4: #H @H
     477            |*: * #nxt_visiting @⊥
     478              >H2 in nxt_visiting;
    479479              cases pre in H1;
    480               [1,3: #_
     480              [1,3,5,7: #_
    481481              |*: #frst #pre_tl * #ABS #_
    482482              ] whd in ⊢ (??%?→?); #EQ destruct(EQ)
    483               [1,2: cases NEQ' #ABS cases (ABS ?) %
    484               |*: >nxt_vis in ABS; *
     483              [1,2,3,4: cases NEQ' #ABS cases (ABS ?) %
     484              |*: lapply ABS; whd in ⊢ (?%→?); >EQlookup' *
    485485              ]
    486486            ]
    487487          ]
     488        |10: @nth_opt_append_hit_l assumption
    488489        ]
    489       ] *)
     490      ]
    490491    ]
    491492  | #i whd in match visited';
     
    498499    | change with (bool_to_Prop (¬eq_identifier ??? ∧ ?))
    499500      >eq_identifier_false [2: % #ABS <ABS in Heq; * #ABS' @ABS' % ]
    500       @add_req_gen_prf [ #_ | #s #next #_ #_ ] %
     501      @add_req_gen_prf [ #_ | #s #next #_ ] %
    501502    ]
    502503  ]
    503504| @add_req_gen_prf
    504   [ #K | #s #next #K #next_vis %1 %1 %{(GOTO … next)} % ]
     505  [ #K | #next #K #next_vis %1 %1 %{(GOTO … next)} % ]
    505506  whd in match generated'; whd in match translated_statement;
    506507  normalize nodelta
    507508  change with statement in match (lookup_safe ?????);
    508509  cases statement in K;
    509   [ * [ #s | #a #ltrue ] #nxt | #s #_ %1 %1 %{s} % | * ] normalize nodelta
    510   [2: #_ cases (true_or_false_Prop (nxt ∈ visited')) #nxt_vis
     510  [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s #_ %1 %1 %{s} % | * ] normalize nodelta
     511  [3: #_ cases (true_or_false_Prop (nxt ∈ visited')) #nxt_vis
    511512    [ >nxt_vis normalize nodelta %1 %2 %{a} %{ltrue} %{nxt} % ]
    512   | #nxt_vis ]
     513  |*: #nxt_vis ]
    513514  %2 % * >nxt_vis *
    514515| whd in match generated';
    515   @add_req_gen_prf [ #_ | #s #next #_ #_ ] normalize >gen_length_prf %
     516  @add_req_gen_prf [ #_ | #next #_ #_ ] normalize >gen_length_prf %
    516517|
    517 ]*)
     518]
    518519qed.
    519520
     
    643644           [ sequential s' nxt ⇒
    644645             match s' with
    645              [ step_seq _ ⇒
    646                (stmt_at … c n = Some ? (sequential … s' it)) ∧
     646             [ COND a ltrue ⇒
     647               (stmt_at … c n = Some ? (sequential … s' it) ∧ sigma nxt = Some ? (S n)) ∨
     648               (stmt_at … c n = Some ? (FCOND … I a ltrue nxt))
     649             | _ ⇒
     650                (stmt_at … c n = Some ? (sequential … s' it)) ∧
    647651                  ((sigma nxt = Some ? (S n)) ∨
    648652                   (stmt_at … c (S n) = Some ? (GOTO … nxt)))
    649              | COND a ltrue ⇒
    650                (stmt_at … c n = Some ? (sequential … s' it) ∧ sigma nxt = Some ? (S n)) ∨
    651                (stmt_at … c n = Some ? (FCOND … I a ltrue nxt))
    652              | CALL _ _ _ ⇒
    653                (stmt_at … c n = Some ? (sequential … s' it)) ∧
    654                   ((sigma nxt = Some ? (S n)) ∨
    655                    (stmt_at … c (S n) = Some ? (GOTO … nxt)))               
    656              | COST_LABEL _ ⇒
    657                (stmt_at … c n = Some ? (sequential … s' it)) ∧
    658                   ((sigma nxt = Some ? (S n)) ∨
    659                    (stmt_at … c (S n) = Some ? (GOTO … nxt)))               
    660653             ]
    661654           | final s' ⇒
     
    708701| >commutative_plus change with (? ≤ |g|) %
    709702]
    710 cases daemon qed. (*
    711703**
    712704#visited #required #generated normalize nodelta ****
     
    725717    * #n_lbl #EQsigma
    726718    elim (sigma_prop … EQsigma) #_ * #stmt * #_
    727     cases stmt [ * [ #s | #a #ltrue ] #nxt | #s | * ] normalize nodelta
    728     [ * #EQnth_opt #_ | * [ * ] #EQnth_opt [ #_ ] | #EQnth_opt ]
     719    cases stmt [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s | * ] normalize nodelta
     720    [1,2,4: * #EQnth_opt #_ |3: * [ * ] #EQnth_opt [ #_ ] |5: #EQnth_opt ]
    729721    >(nth_opt_index_of_label ???? n_lbl ? H)
    730     [1,4,7,10: normalize in ⊢ (% → ?); #EQ destruct(EQ) assumption
    731     |3: @(sequential … s it) |6: @(sequential … (COND … a ltrue) it)
    732     |9: @(FCOND … I a ltrue nxt) |12: @(final … s)
    733     |2,5,8,11: >nth_opt_filter_labels >EQnth_opt >m_return_bind >m_return_bind
    734       >H2 %
     722    try (normalize in ⊢ (% → ?); #EQ destruct(EQ) assumption)
     723    [1,3,5,7,9,11:
     724      >nth_opt_filter_labels in ⊢ (??%?);
     725      (* without the try it does not work *)
     726      try >EQnth_opt in ⊢ (??%?);
     727      >m_return_bind in ⊢ (??%?);
     728      >m_return_bind in ⊢ (??%?);
     729      >H2 in ⊢ (??%?); %
     730    |*:
    735731    ]
    736732  | #eq_lookup elim (sigma_prop ?? eq_lookup)
     
    739735    [ @All_append
    740736      [ cases stmt in stmt_spec;
    741         [ * [ #s | #a #ltrue ] #nxt | #s #_ % | * ]
    742         normalize nodelta * [ #stmt_at_EQ * #nxt_spec | * #stmt_at_EQ #nxt_spec | #stmt_at_EQ ]
     737        [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s #_ % | * ]
     738        normalize nodelta
     739        [1,2,4: * #stmt_at_EQ * #nxt_spec |3: * [ * ] #stmt_at_EQ [ #nxt_spec ]]
    743740        %{I}
    744         [1,3: >nxt_spec % #ABS destruct(ABS)
    745         |*: lapply (in_map_domain … visited nxt)
    746           >req_vis
    747           [1,3: * #x #EQ >EQ % #ABS destruct(ABS)
    748           |2: @(proj1 … (labels_in_req (S n) (GOTO … nxt) …))
    749             whd in ⊢ (??%?); >nxt_spec %
    750           |4: @(proj1 … (proj2 … (labels_in_req n (FCOND … I a ltrue nxt) …)))
    751             whd in ⊢ (??%?); >stmt_at_EQ %
    752           ]
     741        try (>nxt_spec % #ABS destruct(ABS) @False)
     742        lapply (in_map_domain … visited nxt)
     743        >req_vis
     744        [1,3,5,7: * #x #EQ >EQ % #ABS destruct(ABS)
     745        |2,4,6: @(proj1 … (labels_in_req (S n) (GOTO … nxt) …))
     746          whd in ⊢ (??%?); >nxt_spec %
     747        |8: @(proj1 … (proj2 … (labels_in_req n (FCOND … I a ltrue nxt) …)))
     748          whd in ⊢ (??%?); >stmt_at_EQ %
    753749        ]
    754750      | cases stmt in stmt_spec;
    755         [ * [ #s | #a #ltrue ] #nxt | #s | * ] normalize nodelta
    756         [ * #EQ #_ | * [ * #EQ #_ | #EQ ] | #EQ ]
     751        [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s | * ] normalize nodelta
     752        [1,2,4: * #EQ #_ |3: * [ * ] #EQ [ #_ ] |5: #EQ ]
    757753        whd in match stmt_explicit_labels; normalize nodelta
    758         [ @(All_mp … (labels_in_req n (sequential … s it) ?))
     754        [ @(All_mp … (labels_in_req n (sequential … (COST_LABEL … cost) it) ?))
     755        | @(All_mp … (labels_in_req n (sequential … (CALL … f args dest) it) ?))
     756        | @(All_mp … (labels_in_req n (sequential … s it) ?))
    759757        | @(All_mp … (labels_in_req n (sequential … (COND … a ltrue) it) ?))
     758        |6: @(All_mp … (labels_in_req n (final … s) ?))
    760759        | cases (labels_in_req n (FCOND … I a ltrue nxt) ?)
    761760          [ #l_req #_ %{I} lapply (in_map_domain … visited ltrue)
    762761            >(req_vis … l_req) * #n #EQ' >EQ' % #ABS destruct(ABS) ]
    763         | @(All_mp … (labels_in_req n (final … s) ?))
    764762        ]
    765         [1,3,6: #l #l_req >(lookup_eq_safe … (req_vis … l_req)) % #ABS destruct(ABS)
     763        [1,3,5,7,9: #l #l_req >(lookup_eq_safe … (req_vis … l_req))
     764          % #ABS destruct(ABS)
    766765        |*: whd in ⊢ (??%?); >EQ %
    767766        ]
    768767      ]
    769768    | cases stmt in stmt_spec;
    770       [ * [ #s | #a #ltrue ] #nxt | #s | * ] normalize nodelta
    771       [ * #EQ #H | * [ * #EQ #H | #EQ ] | #EQ ]
     769      [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s | * ] normalize nodelta
     770      [1,2,4: * #EQ #H |3: * [ * ] #EQ [ #H ] |5: #EQ ]
    772771      >stmt_at_filter_labels
    773772      whd in match (stmt_at (mk_lin_params p) ?? n); >EQ normalize nodelta
    774       [ % [%] cases H -H [#H %1{H} | #EQ' %2 >stmt_at_filter_labels whd in ⊢ (??%?); >EQ' % ]
     773      [1,2,3: % [1,3,5: %] cases H -H
     774        #H try (%1{H}) %2 >stmt_at_filter_labels whd in ⊢ (??%?); >H %
    775775      | %1 %{H} %
    776776      | %2 %
     
    796796    cut (|generated| = S i)
    797797    [ @(le_to_le_to_eq … (not_lt_to_le … INEQ) )
    798       elim (option_bind_inverse ????? EQ) #x * #EQ1 #EQ2
     798      whd in EQ : (??%?); inversion (nth_opt ???) in EQ;
     799      [2: #x ] #EQ1 whd in ⊢ (??%%→?); #EQ2 destruct
    799800      <length_reverse
    800801      @(nth_opt_hit_length … EQ1)
     
    843844  〈«mk_joint_internal_function (mk_lin_params p) globals
    844845   (joint_if_luniverse ?? f_sig) (joint_if_runiverse ?? f_sig)
    845    (joint_if_result ?? f_sig) (joint_if_params ?? f_sig)
    846    (joint_if_stacksize ?? f_sig) code entry, ?»,
     846   (joint_if_result ?? f_sig) (joint_if_params ?? f_sig) (joint_if_locals ?? f_sig)
     847   (joint_if_stacksize ?? f_sig) code entry entry (* exit is dummy! *), ?»,
    847848   sigma〉.
    848849normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.