Changeset 2532 for src/joint/Joint.ma


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

added FCOND in LIN, and rewritten linearise so that it never adds a GOTO after a COND (writes in FCOND instead)
LIN to ASM is broken atm

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2490 r2532  
    8080 ; snd_arg : Type[0]  (* second argument of binary op *)
    8181 ; pair_move: Type[0] (* argument of move instructions *)
     82 ; call_spec: Type[0] (* type of call (ident/pointer) *)
    8283 ; call_args: Type[0] (* arguments of function calls *)
    8384 ; call_dest: Type[0] (* possible destination of function computation *)
    8485 (* other instructions not fitting in the general framework *)
    8586 ; ext_seq : Type[0]
     87 ; ext_seq_labels : ext_seq → list label
    8688 ; has_tailcalls : bool
    8789 (* if needed: ; ext_fin_branch : Type[0] ; ext_fin_branch_labels : ext_fin_branch → list label *)
     
    106108  | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_seq p globals
    107109  | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_seq p globals
    108   | CALL: (ident + dpl_arg p×(dph_arg p)) → call_args p → call_dest p → joint_seq p globals
     110  | CALL: call_spec p → call_args p → call_dest p → joint_seq p globals
    109111  | extension_seq : ext_seq p → joint_seq p globals.
    110112
     
    145147  λp, globals.λs : joint_step p globals.
    146148  match s with
    147   [ step_seq s ⇒ [ ]
     149  [ step_seq s ⇒
     150    match s with
     151    [ extension_seq ext ⇒ ext_seq_labels … ext
     152    | _ ⇒ [ ]
     153    ]
    148154  | COND _ l ⇒ [l]
    149155  ].
     
    157163  ; succ : Type[0]
    158164  ; succ_label : succ → option label
    159   }.
     165  ; has_fcond : bool
     166  }.
    160167
    161168inductive joint_fin_step (p: unserialized_params): Type[0] ≝
     
    163170  | RETURN: joint_fin_step p
    164171  | TAILCALL :
    165     has_tailcalls p → (ident + (dpl_arg p) × (dph_arg p))
     172    has_tailcalls p → call_spec p
    166173    call_args p → joint_fin_step p.
    167174
     
    174181inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
    175182  | sequential: joint_step p globals → succ p → joint_statement p globals
    176   | final: joint_fin_step p → joint_statement p globals.
     183  | final: joint_fin_step p → joint_statement p globals
     184  | FCOND: has_fcond p → acc_a_reg p → label → label → joint_statement p globals.
    177185
    178186coercion fin_step_to_stmt : ∀p : stmt_params.∀globals.
     
    193201
    194202(* interpretation "code membership" 'mem p c = (code_has_point ?? c p). *)
    195 
     203(*
    196204definition point_in_code ≝ λp,globals,code.Σpt.bool_to_Prop (code_has_point p globals code pt).
    197205unification hint 0 ≔ p, globals, code ⊢ point_in_code p globals code ≡ Sig (code_point p) (λpt.bool_to_Prop (code_has_point p globals code pt)).
     
    206214  ]. normalize in pt_prf;
    207215    >abs in pt_prf; // qed.
     216*)
    208217
    209218definition forall_statements : ∀p : params.∀globals.pred_transformer (joint_statement p globals) (codeT p globals)  ≝
     
    234243  [ sequential c _ ⇒ step_labels … c
    235244  | final c ⇒ fin_step_labels … c
     245  | FCOND _ _ l1 l2 ⇒ [l1 ; l2]
    236246  ].
    237247
     
    316326  λlp : lin_params.
    317327     mk_params
    318       (mk_stmt_params (l_u_pars lp) unit (λ_.None ?))
     328      (mk_stmt_params (l_u_pars lp) unit (λ_.None ?) true)
    319329    (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals)))
    320330    (* code_point ≝ *)ℕ
     
    358368  λgp : graph_params.
    359369     mk_params
    360       (mk_stmt_params (g_u_pars gp) label (Some ?))
     370      (mk_stmt_params (g_u_pars gp) label (Some ?) false)
    361371    (* codeT ≝ *)(λglobals.graph (joint_statement ? globals))
    362372    (* code_point ≝ *)label
     
    403413  joint_if_stacksize: nat;
    404414  joint_if_code     : codeT p globals ;
    405   joint_if_entry : point_in_code … joint_if_code ;
    406   joint_if_exit : point_in_code … joint_if_code
     415  joint_if_entry : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) ;
     416  joint_if_exit : Σpt.bool_to_Prop (code_has_point … joint_if_code pt)
    407417}.
    408418
Note: See TracChangeset for help on using the changeset viewer.