Changeset 2712


Ignore:
Timestamp:
Feb 22, 2013, 8:04:38 PM (6 years ago)
Author:
tranquil
Message:

changed some fields of joint_internal_function's invariant
fixed linearise

Location:
src/joint
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2688 r2712  
    446446(p : params) (globals : list ident) (def : joint_internal_function p globals)
    447447: Prop ≝
    448 { unique_cost_labels :
    449   ∀l1,l2,c,nxt1,nxt2.
    450         stmt_at … (joint_if_code … def) l1 =
    451           Some … (sequential … (COST_LABEL … c) nxt1) →
    452         stmt_at … (joint_if_code … def) l2 =
    453           Some … (sequential … (COST_LABEL … c) nxt2) →
    454         l1 = l2
    455 ; entry_costed :
     448{ entry_costed :
    456449  ∃l,nxt.
    457450        stmt_at … (joint_if_code … def) (joint_if_entry … def) =
    458451          Some … (sequential … (COST_LABEL … l) nxt)
     452; entry_unused :
     453  let entry ≝ pi1 … (joint_if_entry … def) in
     454  let code ≝ joint_if_code … def in
     455  forall_statements_i …
     456    (λpt,stmt.stmt_forall_labels … (λlbl.point_of_label … code lbl ≠ Some ? entry) stmt ∧
     457              stmt_forall_succ … (λnxt.point_of_succ … pt nxt ≠ entry) stmt) code
    459458; code_is_closed : code_closed … (joint_if_code … def)
    460459; code_is_in_universe :
  • src/joint/linearise.ma

    r2708 r2712  
    661661  ∀g : codeT (mk_graph_params p) globals.code_closed … g →
    662662  ∀entry : (Σl.bool_to_Prop (code_has_label … g l))
    663   .Σ〈c, sigma〉.
     663  .Σc_sigma.
     664    let c ≝ \fst c_sigma in
     665    let sigma ≝ \snd c_sigma in
    664666    good_local_sigma … g entry c sigma ∧
    665667    code_closed … c
     
    809811]
    810812qed.
    811 *)
    812813
    813814definition linearise_int_fun :
     
    815816  ∀globals.
    816817    ∀fn_in : joint_closed_internal_function (mk_graph_params p) globals
    817      .Σ〈fn_out : joint_closed_internal_function (mk_lin_params p) globals,
    818         sigma : ?〉.
     818     .Σfn_out_sigma :
     819      (joint_closed_internal_function (mk_lin_params p) globals × ?).
    819820        good_local_sigma … (joint_if_code … fn_in) (joint_if_entry … fn_in)
    820           (joint_if_code … fn_out) sigma
     821          (joint_if_code … (\fst fn_out_sigma)) (\snd fn_out_sigma)
    821822     (* ∃sigma : identifier_map LabelTag ℕ.
    822823        let g ≝ joint_if_code ?? (pi1 … fin) in
     
    837838  let code_sigma ≝ linearise_code …
    838839    (joint_if_code … f_sig)
    839     (pi2 … f_sig)
     840    (code_is_closed … (pi2 … f_sig))
    840841    (joint_if_entry … f_sig) in
    841842  let code ≝ \fst code_sigma in
    842843  let sigma ≝ \snd code_sigma in
    843844  let entry : Σpt.bool_to_Prop (code_has_point … code pt) ≝ «0, hide_prf ??» in
    844   〈«mk_joint_internal_function (mk_lin_params p) globals
     845  «〈«mk_joint_internal_function (mk_lin_params p) globals
    845846   (joint_if_luniverse ?? f_sig) (joint_if_runiverse ?? f_sig)
    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! *), ?»,
    848    sigma〉.
    849 normalize nodelta
    850 cases (linearise_code ?????) * #code #sigma normalize nodelta * #H1 #H2
    851 [ @H2
    852 | @H1
    853 | cases H1 * #H3 #H4 #H5 elim (H5 … H3)
     847   (joint_if_result ?? f_sig) (joint_if_params ?? f_sig)
     848   (joint_if_stacksize ?? f_sig) code entry (* exit is dummy! *), hide_prf ??»,
     849   sigma〉, proj1 ?? (pi2 ?? code_sigma)».
     850[2: whd in match code; cases code_sigma -code_sigma * #code #sigma
     851  normalize nodelta *** #H3 #H4 #H5
     852   elim (H5 … H3)
    854853  #s ** #_ #_ >lin_code_has_point cases code
    855   [ cases s [ * [ #s' | #a #ltrue ] #nxt | #s' | * ]
    856     [ * #ABS #_ | * [ * #ABS #_ | #ABS ] | #ABS ] normalize in ABS; destruct(ABS)
    857   | #hd #tl #_ %
     854  [ cases s [ * [ #cost | #f #args #dest | #a #ltrue | #s' ] #nxt | #s' | * ]
     855    [1,2,4: * #EQnth_opt #_ |3: * [ * ] #EQnth_opt [ #_ ] |5: #EQnth_opt ]
     856    normalize in EQnth_opt; destruct(EQnth_opt)
     857  | #hd #tl #_ #_ %
     858  ]
     859| @hide_prf %
     860  (* TODO *)
     861  [ cases daemon
     862  | cases daemon
     863  | @(proj2 ?? (pi2 ?? code_sigma))
     864  | cases daemon
    858865  ]
    859866]
Note: See TracChangeset for help on using the changeset viewer.