Ignore:
Timestamp:
Jan 13, 2012, 12:23:30 PM (9 years ago)
Author:
tranquil
Message:
  • some changes in everything
  • separated extensions in sequential and final, to accomodate tailcalls
  • finished RTL's semantics
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint_paolo.ma

    r1640 r1643  
    4646 ; call_args: Type[0] (* arguments of function calls *)
    4747 ; call_dest: Type[0] (* possible destination of function computation *)
    48  ; extend_statements: Type[0] (* other statements not fitting in the general framework *)
    49  ; ext_forall_labels : (label → Prop) → extend_statements → Prop
     48 ; ext_instruction: Type[0] (* other instructions not fitting in the general framework *)
     49 ; ext_forall_labels : (label → Prop) → ext_instruction → Prop
     50 ; ext_fin_instruction: Type[0] (* final instructions (e.g. tailcalls) not fitting in the general framework *)
     51 ; ext_fin_forall_labels : (label → Prop) → ext_fin_instruction → Prop
    5052 }.
    5153 
     
    6870  | CALL_ID: ident → call_args p → call_dest p → joint_instruction p globals
    6971  | COND: acc_a_reg p → label → joint_instruction p globals
    70   | extension: extend_statements p → joint_instruction p globals.
     72  | extension: ext_instruction p → joint_instruction p globals.
    7173
    7274(* Paolo: to be moved elsewhere *)
     
    8688
    8789
    88 
    8990definition inst_forall_labels : ∀p : inst_params.∀globals.
    9091    (label → Prop) → joint_instruction p globals → Prop ≝
     
    119120  | sequential: joint_instruction p globals → succ p → joint_statement p globals
    120121  | GOTO: label → joint_statement p globals
    121   | RETURN: joint_statement p globals.
     122  | RETURN: joint_statement p globals
     123  | extension_fin : ext_fin_instruction p → joint_statement p globals.
    122124
    123125record params : Type[1] ≝
    124126 { stmt_pars :> stmt_params
    125127 ; codeT: list ident → Type[0]
    126  ; lookup: ∀globals.codeT globals → label → option (joint_statement stmt_pars globals)
    127  }.
    128 
    129 
    130 (* for all labels in statement. Uses succ_choice to consider the successor of
    131    a statement when such successors are labels *)
     128 ; code_has_label: ∀globals.codeT globals → label → Prop
     129 ; forall_statements : ∀globals.(joint_statement stmt_pars globals → Prop) →
     130    codeT globals → Prop
     131 }.
     132
     133
    132134definition stmt_forall_labels : ∀p : stmt_params.∀globals.
    133135    (label → Prop) → joint_statement p globals → Prop ≝
     
    136138  | GOTO l ⇒ P l
    137139  | RETURN ⇒ True
     140  | extension_fin c ⇒ ext_fin_forall_labels … P c
    138141  ].
    139142
     
    144147
    145148definition lin_params_to_params ≝
    146   λlp : lin_params. mk_params
    147     (mk_stmt_params lp unit (λ_.λ_.True))
    148     (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals)))
    149     (* lookup ≝ *)(λglobals,code,lbl.find ??
    150         (λl_stmt. let 〈lbl_opt, stmt〉 ≝ l_stmt in
    151           ! lbl' ← lbl_opt ;
    152           if eq_identifier … lbl lbl' then return stmt else None ?) code).
     149  λlp : lin_params.let stmt_pars ≝ (mk_stmt_params lp unit (λ_.λ_.True)) in
     150     mk_params
     151      stmt_pars
     152    (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement stmt_pars globals)))
     153    (* code_has_label ≝ *)(λglobals,code,lbl.Exists ?
     154        (λl_stmt. \fst l_stmt = Some ? lbl) code)
     155    (* forall_statements ≝ *)(λglobals,P,code.All ?
     156        (λl_stmt. P (\snd l_stmt)) code).
    153157
    154158coercion lp_to_p : ∀lp : lin_params.params ≝ lin_params_to_params
     
    157161record graph_params : Type[1] ≝
    158162  { g_u_pars :> unserialized_params }.
    159 
    160 include alias "common/Graphs.ma". (* To pick the right lookup *)
    161163
    162164(* One common instantiation of params via Graphs of joint_statements
    163165   (all languages but LIN) *)
    164166definition graph_params_to_params ≝
    165   λgp : graph_params. mk_params
    166     (mk_stmt_params gp label (λP.P))
    167     (* codeT ≝ *)(λglobals.graph (joint_statement ? globals))
    168     (* lookup ≝ *)(λglobals.lookup …).
     167  λgp : graph_params.let stmt_pars ≝ mk_stmt_params gp label (λP.P) in
     168     mk_params
     169      stmt_pars
     170    (* codeT ≝ *)(λglobals.graph (joint_statement stmt_pars globals))
     171    (* code_has_label ≝ *)(λglobals,code,lbl.lookup … code lbl ≠ None ?)
     172    (* forall_statements ≝ *)(λglobals,P,code.
     173      ∀l,s.lookup … code l = Some ? s → P s).
    169174   
    170 coercion gp_to_p : ∀gp:graph_params.params ≝ λgp.graph_params_to_params gp
     175coercion gp_to_p : ∀gp:graph_params.params ≝ graph_params_to_params
    171176on _gp : graph_params to params.
    172177   
    173178
    174 definition labels_present : ∀p : params.∀globals.
     179definition labels_present : ∀globals.∀p : params.
    175180  codeT p globals → (joint_statement p globals) → Prop ≝
    176 λglobals,p,code,s. stmt_forall_labels globals p
    177   (λl.lookup … code l ≠ None ?) s.
    178 
    179 definition forall_stmts : ∀p : params.∀globals.
    180   ∀P: joint_statement p globals → Prop. codeT p globals → Prop ≝
    181 λglobals,p,P,code. ∀l,s. lookup … code l = Some ? s → P s.
     181λglobals,p,code,s. stmt_forall_labels p globals
     182  (λl.code_has_label ?? code l) s.
    182183
    183184definition code_closed : ∀p : params.∀globals.
    184185  codeT p globals → Prop ≝ λp,globals,code.
    185     forall_stmts … (labels_present … code) code.
     186    forall_statements … (labels_present … code) code.
    186187
    187188(* CSC: special case where localsT is a list of registers (RTL and ERTL) *)
     
    202203  joint_if_code     : codeT p globals ;
    203204(*CSC: XXXXX entry unused for LIN, but invariant in that case... *)
    204   joint_if_entry    : Σl: label. lookup … joint_if_code l ≠ None ?;
     205  joint_if_entry    : Σl: label. code_has_label … joint_if_code l;
    205206(*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *)
    206   joint_if_exit     : Σl: label. lookup … joint_if_code l ≠ None ?
     207  joint_if_exit     : Σl: label. code_has_label …  … joint_if_code l
    207208}.
    208209
     
    216217  λexit: label.
    217218  λp:joint_internal_function globals pars.
    218   λprf: lookup … (joint_if_code … p) exit ≠ None ?.
     219  λprf: code_has_label … (joint_if_code … p) exit.
    219220   mk_joint_internal_function globals pars
    220221    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
     
    238239  λgraph.
    239240  λp:joint_internal_function globals pars.
    240   λentry_prf: lookup … graph (joint_if_entry … p) ≠ None ?.
    241   λexit_prf: lookup … graph (joint_if_exit … p) ≠ None ?.
     241  λentry_prf: code_has_label … graph (joint_if_entry … p).
     242  λexit_prf: code_has_label … graph (joint_if_exit … p).
    242243    set_joint_code globals pars p
    243244      graph
Note: See TracChangeset for help on using the changeset viewer.