Ignore:
Timestamp:
Dec 4, 2012, 6:16:25 PM (7 years ago)
Author:
tranquil
Message:

rewritten function handling in joint
swapped call_rel with ret_rel in the definition of status_rel, and parameterised status_simulation on status_rel
renamed SemanticUtils?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/linearise.ma

    r2481 r2529  
    173173    ] n_prf
    174174  ] (chop_ok ? (λx.x∈visited) visiting).
    175 (*cases daemon qed. *)
     175(* cases daemon qed. *)
    176176whd
    177177[ (* base case, visiting is all visited *)
     
    555555qed.
    556556
    557 
    558557definition good_local_sigma :
    559558  ∀p:unserialized_params.
     
    565564  λp,globals,g,entry,c,sigma.
    566565    sigma entry = Some ? 0 ∧
     566    (∀l,n.point_of_label … c l = Some ? n → sigma l = Some ? n) ∧
    567567    ∀l,n.sigma l = Some ? n →
    568       ∃s. lookup … g l = Some ? s ∧
    569         opt_Exists ?
    570           (λls.let 〈lopt, ts〉 ≝ ls in
    571             opt_All ? (eq ? l) lopt ∧
    572             ts = graph_to_lin_statement … s ∧
    573             opt_All ?
    574               (λnext.Or (sigma next = Some ? (S n))
    575               (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
    576               (stmt_implicit_label … s)) (nth_opt … n c).
     568      ∃s. stmt_at … g l = Some ? s ∧
     569        All ? (λl.sigma l ≠ None ?) (stmt_labels … s) ∧
     570        opt_All ?
     571            (λnext.Or (sigma next = Some ? (S n))
     572            (stmt_at … c (S n) = Some ? (GOTO … next)))
     573            (stmt_implicit_label … s) ∧
     574        stmt_at … c n = Some ? (graph_to_lin_statement … s).
    577575
    578576definition linearise_code:
     
    624622#entry_O #req_vis #last_fin #labels_in_req #sigma_prop
    625623%
    626 [ % [assumption]
    627   #lbl #n #eq_lookup elim (sigma_prop ?? eq_lookup)
    628   #lbl_in_gen * #stmt ** #stmt_in_g #nth_opt_is_stmt #succ_is_in
    629   % [2: % [ assumption ] |]
    630   >nth_opt_filter_labels in ⊢ (???%);
    631   >nth_opt_is_stmt >m_return_bind whd >m_return_bind
    632   % [ % ]
    633   [ elim (lbl ∈ required) %
    634   | %
    635   | lapply succ_is_in
    636     lapply (refl … (stmt_implicit_label … stmt))
    637     cases (stmt_implicit_label … stmt) in ⊢ (???%→%); [#_ #_ %]
    638     #next #EQ_next *
    639     [ #H %1{H} ]
    640     #H %2
    641     >nth_opt_filter_labels >H %
     624[ % [ % [assumption]]
     625  #lbl #n
     626  [ change with (If ? then with prf do ? else ? = ? → ?)
     627    @If_elim [2: #_ #ABS destruct(ABS) ]
     628    #H lapply H
     629    >occurs_exactly_once_filter_labels
     630    elim (true_or_false_Prop … (occurs_exactly_once ?? lbl ?))
     631    [1,2: #H1 >H1 |*:] [2: * ]
     632    elim (true_or_false_Prop … (lbl ∈ required)) #H2 >H2 *
     633    lapply (in_map_domain … visited lbl) >(req_vis … H2)
     634    * #n_lbl #EQsigma
     635    elim (sigma_prop … EQsigma) #_ * #stmt ** #_ #EQnth_opt #_
     636    >(nth_opt_index_of_label ???? n_lbl (graph_to_lin_statement … stmt) H)
     637    [ normalize in ⊢ (% → ?); #EQ destruct(EQ) assumption
     638    | >nth_opt_filter_labels >EQnth_opt >m_return_bind >m_return_bind
     639      >H2 %
     640    ]
     641  | #eq_lookup elim (sigma_prop ?? eq_lookup)
     642    #lbl_in_gen * #stmt ** #stmt_in_g #nth_opt_is_stmt #succ_is_in
     643    % [2: % [ % [ % [ assumption ]]] |]
     644    [ @All_append
     645      [ lapply succ_is_in elim (stmt_implicit_label ???) [ * % ]
     646        #nxt #nxt_spec % [2: %] cases nxt_spec -nxt_spec
     647        [ #EQ >EQ % #ABS destruct(ABS)
     648        | #goto_in lapply (in_map_domain … visited nxt)
     649          >req_vis [ * #n #EQ >EQ % #ABS destruct(ABS) ]
     650          @(proj1 … (labels_in_req (S n) (GOTO … nxt) …))
     651          whd in ⊢ (??%?); >goto_in %
     652        ]
     653      | <graph_to_lin_labels @(All_mp … (labels_in_req …))
     654        [ #lbl #H
     655          lapply (in_map_domain … visited lbl) >(req_vis … H) * #n #EQ >EQ % #ABS destruct(ABS)
     656        | whd in ⊢ (??%?); >nth_opt_is_stmt % |
     657        ]
     658      ]
     659    | lapply succ_is_in
     660      cases (stmt_implicit_label … stmt) [#_ %]
     661      #next *
     662      [ #H %1{H} ]
     663      #H %2
     664      >stmt_at_filter_labels whd in ⊢ (??%?); >H %
     665    | >stmt_at_filter_labels whd in ⊢ (??%?); >nth_opt_is_stmt %
     666    ]
    642667  ]
    643668| #i #s
     
    711736[ @H2
    712737| @H1
    713 | cases H1 #H3 #H4 elim (H4 … H3)
    714   #s * #_ >lin_code_has_point cases code
    715   [ * | #hd #tl #_ % ]
     738| cases H1 * #H3 #H4 #H5 elim (H5 … H3)
     739  #s *** #_ #_ #_ >lin_code_has_point cases code
     740  [ #ABS normalize in ABS; destruct(ABS) | #hd #tl #_ % ]
    716741]
    717742qed.
     
    724749    (λglobals.transf_fundef ?? (λf_in.\fst (linearise_int_fun p globals f_in))).
    725750
    726 
     751(*
    727752definition good_sigma :
    728753  ∀p:unserialized_params.
     
    742767#p #prog
    743768letin sigma ≝
    744   (λi : Σi.is_internal_function_of_program … prog i.
    745     let fn_in ≝ if_of_function … i in
     769  (λi : Σi.is_internal_function_of_program … prog i.    let fn_in ≝ if_of_function … i in
    746770    \snd (linearise_int_fun … fn_in))
    747771%{sigma}
     
    751775normalize nodelta #prf @prf
    752776qed.
     777*)
Note: See TracChangeset for help on using the changeset viewer.