Ignore:
Timestamp:
Nov 16, 2012, 6:59:24 PM (7 years ago)
Author:
tranquil
Message:

put some generic stuff we need in the back end in extraGlobalenvs (with some axioms that are
in the commented section of Globalenvs)
linearise now has a full spec

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/linearise.ma

    r2440 r2473  
    11include "joint/TranslateUtils.ma".
     2include "common/extraGlobalenvs.ma".
    23include "utilities/hide.ma".
    34
     
    553554qed.
    554555
     556
     557definition good_local_sigma :
     558  ∀p:unserialized_params.
     559  ∀globals.
     560  ∀g:codeT (mk_graph_params p) globals.
     561  (Σl.bool_to_Prop (code_has_label … g l)) →
     562  codeT (mk_lin_params p) globals →
     563  (label → option ℕ) → Prop ≝
     564  λp,globals,g,entry,c,sigma.
     565    sigma entry = Some ? 0 ∧
     566    ∀l,n.sigma l = Some ? n →
     567      ∃s. lookup … g l = Some ? s ∧
     568        opt_Exists ?
     569          (λls.let 〈lopt, ts〉 ≝ ls in
     570            opt_All ? (eq ? l) lopt ∧
     571            ts = graph_to_lin_statement … s ∧
     572            opt_All ?
     573              (λnext.Or (sigma next = Some ? (S n))
     574              (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
     575              (stmt_implicit_label … s)) (nth_opt … n c).
     576
    555577definition linearise_code:
    556578 ∀p : unserialized_params.∀globals.
    557579  ∀g : codeT (mk_graph_params p) globals.code_closed … g →
    558   ∀entry : (Σl.bool_to_Prop (code_has_label … g l)).
    559     (Σc : codeT (mk_lin_params p) globals.
    560       code_closed … c ∧
     580  ∀entry : (Σl.bool_to_Prop (code_has_label … g l))
     581  .Σ〈c, sigma〉.
     582    good_local_sigma … g entry c sigma ∧
     583    code_closed … c
     584       (* ∧
    561585      ∃ sigma : identifier_map LabelTag ℕ.
    562586      lookup … sigma entry = Some ? 0 ∧
     
    570594                (λnext.Or (lookup … sigma next = Some ? (S n))
    571595                (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
    572                 (stmt_implicit_label … s)) (nth_opt … n c))
     596                (stmt_implicit_label … s)) (nth_opt … n c)*)
    573597
    574598 λp,globals,g,g_prf,entry_sig.
     
    583607      let crev ≝ \snd triple in
    584608      let lbld_code ≝ rev ? crev in
    585       mk_Sig ?? (filter_labels … (λl.l∈required) lbld_code) ? ].
    586 [ (* done later *)
     609      〈filter_labels … (λl.l∈required) lbld_code, lookup … sigma〉 ].
     610[ cases (graph_visit ????????????????????)
     611 (* done later *)
    587612| #i >mem_set_empty *
    588613|3,4: #a #b whd in ⊢ (??%?→?); #ABS destruct(ABS)
     
    594619| >commutative_plus change with (? ≤ |g|) %
    595620]
    596 lapply (refl … triple)
    597 generalize in match triple in ⊢ (???%→%); **
    598 #visited #required #generated #EQtriple
    599 >EQtriple in H ⊢ %; normalize nodelta ****
     621**
     622#visited #required #generated normalize nodelta ****
    600623#entry_O #req_vis #last_fin #labels_in_req #sigma_prop
    601 % >EQtriple
    602 [ #i #s
     624%
     625[ % [assumption]
     626  #lbl #n #eq_lookup elim (sigma_prop ?? eq_lookup)
     627  #lbl_in_gen * #stmt ** #stmt_in_g #nth_opt_is_stmt #succ_is_in
     628  % [2: % [ assumption ] |]
     629  >nth_opt_filter_labels in ⊢ (???%);
     630  >nth_opt_is_stmt >m_return_bind whd >m_return_bind
     631  % [ % ]
     632  [ elim (lbl ∈ required) %
     633  | %
     634  | lapply succ_is_in
     635    lapply (refl … (stmt_implicit_label … stmt))
     636    cases (stmt_implicit_label … stmt) in ⊢ (???%→%); [#_ #_ %]
     637    #next #EQ_next *
     638    [ #H %1{H} ]
     639    #H %2
     640    >nth_opt_filter_labels >H %
     641  ]
     642| #i #s
    603643  >stmt_at_filter_labels #EQ
    604644  %
     
    628668  ]
    629669]
    630 %{visited} % [assumption]
    631 #lbl #n #eq_lookup elim (sigma_prop ?? eq_lookup)
    632 #lbl_in_gen * #stmt ** #stmt_in_g #nth_opt_is_stmt #succ_is_in
    633 % [2: % [ assumption ] |]
    634 >nth_opt_filter_labels in ⊢ (???%);
    635 >nth_opt_is_stmt >m_return_bind whd >m_return_bind
    636 % [ % ]
    637 [ elim (lbl ∈ required) %
    638 | %
    639 | lapply succ_is_in
    640   lapply (refl … (stmt_implicit_label … stmt))
    641   cases (stmt_implicit_label … stmt) in ⊢ (???%→%); [#_ #_ %]
    642   #next #EQ_next *
    643   [ #H %1{H} ]
    644   #H %2
    645   >nth_opt_filter_labels >H %
    646 ]
    647 qed.
    648 
    649 (* Paolo: for now I'm leaving the closed graph stuff out, waiting for it to
    650    be done on all passes *)
     670qed.
     671
    651672definition linearise_int_fun :
    652673  ∀p : unserialized_params.
    653674  ∀globals.
    654     joint_closed_internal_function (mk_graph_params p) globals →
    655     joint_closed_internal_function (mk_lin_params p) globals
     675    ∀fn_in : joint_closed_internal_function (mk_graph_params p) globals
     676     .Σ〈fn_out : joint_closed_internal_function (mk_lin_params p) globals,
     677        sigma : ?〉.
     678        good_local_sigma … (joint_if_code … fn_in) (joint_if_entry … fn_in)
     679          (joint_if_code … fn_out) sigma
    656680     (* ∃sigma : identifier_map LabelTag ℕ.
    657681        let g ≝ joint_if_code ?? (pi1 … fin) in
     
    669693                    (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
    670694                    (stmt_implicit_label … s)) (nth_opt … n c)*) ≝
    671   λp,globals,f_sig.let f_in ≝ pi1 … f_sig in
    672   «mk_joint_internal_function (mk_lin_params p) globals
    673    (joint_if_luniverse ?? f_in) (joint_if_runiverse ?? f_in)
    674    (joint_if_result ?? f_in) (joint_if_params ?? f_in) (joint_if_locals ?? f_in)
    675    (joint_if_stacksize ?? f_in)
    676    (linearise_code p globals (joint_if_code … f_in) (pi2 … f_sig) (joint_if_entry … f_in))
    677    0 0 (* exit is dummy! *), ?». [2,4:// ]
    678 elim (linearise_code ?????) #c * #code_closed
    679 [3: #_ assumption ]
    680 @hide_prf
    681 * #sigma * #O_in #sigma_prop
    682 >lin_code_has_point
    683 elim (sigma_prop … O_in) #s * #_
    684 cases c
    685 [1,3: *
    686 |*: #hd #tl #_ %
     695  λp,globals,f_sig.
     696  let code_sigma ≝ linearise_code …
     697    (joint_if_code … f_sig)
     698    (pi2 … f_sig)
     699    (joint_if_entry … f_sig) in
     700  let code ≝ \fst code_sigma in
     701  let sigma ≝ \snd code_sigma in
     702  let entry : Σpt.bool_to_Prop (code_has_point … code pt) ≝ «0, hide_prf ??» in
     703  〈«mk_joint_internal_function (mk_lin_params p) globals
     704   (joint_if_luniverse ?? f_sig) (joint_if_runiverse ?? f_sig)
     705   (joint_if_result ?? f_sig) (joint_if_params ?? f_sig) (joint_if_locals ?? f_sig)
     706   (joint_if_stacksize ?? f_sig) code entry entry (* exit is dummy! *), ?»,
     707   sigma〉.
     708normalize nodelta
     709cases (linearise_code ?????) * #code #sigma normalize nodelta * #H1 #H2
     710[ @H2
     711| @H1
     712| cases H1 #H3 #H4 elim (H4 … H3)
     713  #s * #_ >lin_code_has_point cases code
     714  [ * | #hd #tl #_ % ]
    687715]
    688716qed.
     
    690718definition linearise : ∀p : unserialized_params.
    691719  program (joint_function (mk_graph_params p)) ℕ →
    692   program (joint_function (mk_lin_params p)) ℕ ≝
     720  program (joint_function (mk_lin_params p)) ℕ
     721   ≝
    693722  λp,pr.transform_program ??? pr
    694     (λglobals.transf_fundef ?? (linearise_int_fun p globals)).
     723    (λglobals.transf_fundef ?? (λf_in.\fst (linearise_int_fun p globals f_in))).
     724
     725
     726definition good_sigma :
     727  ∀p:unserialized_params.
     728  ∀prog_in : joint_program (mk_graph_params p).
     729  ((Σi.is_internal_function_of_program … prog_in i) → label → option ℕ) → Prop ≝
     730  λp,prog_in,sigma.
     731  let prog_out ≝ linearise … prog_in in
     732  ∀i.
     733  let fn_in ≝ prog_if_of_function ?? prog_in i in
     734  let fn_out ≝ prog_if_of_function ?? prog_out «i, hide_prf ??» in
     735  let sigma_local ≝ sigma i in
     736  good_local_sigma ?? (joint_if_code ?? fn_in) (joint_if_entry … fn_in)
     737          (joint_if_code ?? fn_out) sigma_local.
     738@if_propagate @(pi2 … i)
     739qed.
     740
     741lemma linearise_spec : ∀p,prog.∃sigma.good_sigma p prog sigma.
     742#p #prog
     743letin sigma ≝
     744  (λi.
     745    let fn_in ≝ prog_if_of_function ?? prog i in
     746    \snd (linearise_int_fun … fn_in))
     747%{sigma}
     748* #i #i_prf >(prog_if_of_function_transform … i_prf)
     749normalize nodelta
     750cases (linearise_int_fun ???) * #fn_out #sigma_loc
     751normalize nodelta #prf @prf
     752qed.
Note: See TracChangeset for help on using the changeset viewer.