Changeset 2784


Ignore:
Timestamp:
Mar 6, 2013, 2:35:39 PM (7 years ago)
Author:
sacerdot
Message:

Repaired after Mauro's commit.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/linearise.ma

    r2712 r2784  
    44
    55definition graph_to_lin_statement :
    6   ∀p : unserialized_params.∀globals.
     6  ∀p : uns_params.∀globals.
    77  ∀A.identifier_map LabelTag A →
    88  joint_statement (mk_graph_params p) globals → joint_statement (mk_lin_params p) globals ≝
     
    2222(*
    2323lemma graph_to_lin_labels :
    24   ∀p : unserialized_params.∀globals,s.
     24  ∀p : uns_params.∀globals,s.
    2525  stmt_labels … (graph_to_lin_statement p globals s) =
    2626  stmt_explicit_labels … s.
     
    119119
    120120let rec graph_visit
    121   (p : unserialized_params)
     121  (p : uns_params)
    122122  (globals: list ident)
    123123  (g : codeT (mk_graph_params p) globals)
     
    629629
    630630definition good_local_sigma :
    631   ∀p:unserialized_params.
     631  ∀p:uns_params.
    632632  ∀globals.
    633633  ∀g:codeT (mk_graph_params p) globals.
     
    658658
    659659definition linearise_code:
    660  ∀p : unserialized_params.∀globals.
     660 ∀p : uns_params.∀globals.
    661661  ∀g : codeT (mk_graph_params p) globals.code_closed … g →
    662662  ∀entry : (Σl.bool_to_Prop (code_has_label … g l))
     
    813813
    814814definition linearise_int_fun :
    815   ∀p : unserialized_params.
     815  ∀p : uns_params.
    816816  ∀globals.
    817817    ∀fn_in : joint_closed_internal_function (mk_graph_params p) globals
     
    863863  | @(proj2 ?? (pi2 ?? code_sigma))
    864864  | cases daemon
     865  | (* We need to add this to graph_visit_ret_type as an invariant.
     866       To prove the invariant at each step in graph_visit we will exploit
     867       (regs_are_in_univers … (pi2 … f_sig))
     868       More generally, to close all the daemons here we need to strengthen
     869       the invariant of graph_visit_ret_type so that the partial code
     870       emitted is also good_if at each step *)
     871    cases daemon
    865872  ]
    866873]
    867874qed.
    868875
    869 definition linearise : ∀p : unserialized_params.
     876definition linearise : ∀p : uns_params.
    870877  program (joint_function (mk_graph_params p)) ℕ →
    871878  program (joint_function (mk_lin_params p)) ℕ
     
    876883(*
    877884definition good_sigma :
    878   ∀p:unserialized_params.
     885  ∀p:uns_params.
    879886  ∀prog_in : joint_program (mk_graph_params p).
    880887  ((Σi.is_internal_function_of_program … prog_in i) → label → option ℕ) → Prop ≝
Note: See TracChangeset for help on using the changeset viewer.