Changeset 1640 for src/joint


Ignore:
Timestamp:
Jan 11, 2012, 5:41:45 PM (9 years ago)
Author:
tranquil
Message:
  • finished fork of semantics.ma
  • unification of Errors under the monad notations brings problems in type checking when res and IO are used together. Needs a lot of annotations, and may break the pre-fork material
Location:
src/joint
Files:
1 added
2 edited

Legend:

Unmodified
Added
Removed

  • src/joint/Joint_paolo.ma

    r1635 r1640  
    66
    77(* Here is the structure of parameter records (downward edges are coercions,
    8    the ¦ edge is the only explicitly defined coercion):
    9 
    10        _____graph_params___
    11       /           ¦        \
    12      /         params       \
    13     /         /      \      |
    14    / stmt_params      local_params
    15    \    |                  |
     8   the ↓ edges are the only explicitly defined coercions). lin_params and
     9   graph_params are simple wrappers of unserialized_params, and the coercions
     10   from them to params instantiate the missing bits with values for linarized
     11   programs and graph programs respectively.
     12
     13        lin_params      graph_params
     14          |       \_____ /____   |
     15          |             /     \  |
     16          \_______     /      ↓  ↓
     17                  \   _\____ params
     18                   \_/  \      |
     19                    / \  \     ↓
     20              _____/   unserialized_params
     21             /      _______/   |
     22            /      /           |
     23     stmt_params  /   local_params
     24        |      __/             |
    1625    inst_params       funct_params
    1726
    … …  
    3443 ; dph_arg: Type[0]   (* high address registers *)
    3544 ; snd_arg : Type[0]  (* second argument of binary op *)
    36  ; operator1 : Type[0] (* = Op1 in all but RTLabs *)
    37  ; operator2 : Type[0] (* = Op2 in all but RTLabs *)
    3845 ; pair_move: Type[0] (* argument of move instructions *)
    3946 ; call_args: Type[0] (* arguments of function calls *)
    … …  
    5158  | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals
    5259  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_instruction p globals
    53   | OP1: operator1 p → acc_a_reg p → acc_a_reg p → joint_instruction p globals
    54   | OP2: operator2 p → acc_a_reg p → acc_a_arg p → snd_arg p → joint_instruction p globals
    55   (* int, clear and set carry can be done with generic move *)
    56 (*| INT: generic_reg p → Byte → joint_instruction p globals
     60  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_instruction p globals
     61  | OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_instruction p globals
     62  (* int done with generic move *)
     63(*| INT: generic_reg p → Byte → joint_instruction p globals *)
    5764  | CLEAR_CARRY: joint_instruction p globals
    58   | SET_CARRY: joint_instruction p globals *)
     65  | SET_CARRY: joint_instruction p globals
    5966  | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_instruction p globals
    6067  | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_instruction p globals
    … …  
    6269  | COND: acc_a_reg p → label → joint_instruction p globals
    6370  | extension: extend_statements p → joint_instruction p globals.
     71
     72(* Paolo: to be moved elsewhere *)
     73
     74notation "r ← a1 .op. a2" with precedence 50 for
     75  @{'op2 $op $r $a1 $a2}.
     76notation "r ← . op . a" with precedence 50 for
     77  @{'op1 $op $r $a}.
     78notation "r ← a" with precedence 50 for
     79  @{'mov $r $a}. (* to be set in individual languages *)
     80notation "❮r, s❯ ← a1 . op . a2" with precedence 50 for
     81  @{'opaccs $op $r $s $a1 $a2}.
     82
     83interpretation "op2" 'op2 op r a1 a2 = (OP2 ? ? op r a1 a2).
     84interpretation "op1" 'op1 op r a = (OP1 ? ? op r a).
     85interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2).
     86
     87
    6488
    6589definition inst_forall_labels : ∀p : inst_params.∀globals.
    … …  
    7094  | _ ⇒ True
    7195 ].
    72 
    73 record stmt_params : Type[1] ≝
    74   { inst_pars :> inst_params
    75   ; succ : Type[0]
    76   ; succ_choice : (succ = label) + (succ = unit)
    77   }.
    78 
    79 inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
    80   | sequential: joint_instruction p globals → succ p → joint_statement p globals
    81   | GOTO: label → joint_statement p globals
    82   | RETURN: joint_statement p globals.
    83 
    84 (* for all labels in statement. Uses succ_choice to consider the successor of
    85    a statement when such successors are labels *)
    86 definition stmt_forall_labels : ∀p : stmt_params.∀globals.
    87     (label → Prop) → joint_statement p globals → Prop.
    88 *#i_pr#succ#succ_choice#globals#P*
    89 [#instr cases succ_choice #eq >eq #next
    90   [@(inst_forall_labels … P instr ∧ P next)
    91   |@(inst_forall_labels … P instr)
    92   ]
    93 |@P
    94 |@True
    95 ]qed.
    9696
    9797record funct_params : Type[1] ≝
    … …  
    105105 }.
    106106
     107record unserialized_params : Type[1] ≝
     108 { u_inst_pars :> inst_params
     109 ; u_local_pars :> local_params
     110 }.
     111
     112record stmt_params : Type[1] ≝
     113  { unserialized_pars :> unserialized_params
     114  ; succ : Type[0]
     115  ; succ_forall_labels : (label → Prop) → succ → Prop
     116  }.
     117
     118inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
     119  | sequential: joint_instruction p globals → succ p → joint_statement p globals
     120  | GOTO: label → joint_statement p globals
     121  | RETURN: joint_statement p globals.
     122
    107123record params : Type[1] ≝
    108124 { stmt_pars :> stmt_params
    109  ; local_pars :> local_params
    110125 ; codeT: list ident → Type[0]
    111126 ; lookup: ∀globals.codeT globals → label → option (joint_statement stmt_pars globals)
    112127 }.
    113128
     129
     130(* for all labels in statement. Uses succ_choice to consider the successor of
     131   a statement when such successors are labels *)
     132definition stmt_forall_labels : ∀p : stmt_params.∀globals.
     133    (label → Prop) → joint_statement p globals → Prop ≝
     134  λp,g,P,stmt. match stmt with
     135  [ sequential inst next ⇒ inst_forall_labels p g P inst ∧ succ_forall_labels p P next
     136  | GOTO l ⇒ P l
     137  | RETURN ⇒ True
     138  ].
     139
     140record lin_params : Type[1] ≝
     141  { l_u_pars :> unserialized_params }.
     142
     143include "utilities/option.ma".
     144
     145definition 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).
     153
     154coercion lp_to_p : ∀lp : lin_params.params ≝ lin_params_to_params
     155  on _lp : lin_params to params.
     156
    114157record graph_params : Type[1] ≝
    115  { g_inst_pars :> inst_params
    116  ; g_local_pars :> local_params
    117  }.
     158  { g_u_pars :> unserialized_params }.
     159
     160include alias "common/Graphs.ma". (* To pick the right lookup *)
     161
     162(* One common instantiation of params via Graphs of joint_statements
     163   (all languages but LIN) *)
     164definition 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 …).
     169   
     170coercion gp_to_p : ∀gp:graph_params.params ≝ λgp.graph_params_to_params gp
     171on _gp : graph_params to params.
     172   
    118173
    119174definition labels_present : ∀p : params.∀globals.
    … …  
    130185    forall_stmts … (labels_present … code) code.
    131186
    132 include alias "common/Graphs.ma". (* To pick the right lookup *)
    133 
    134 
    135 (* One common instantiation of params via Graphs of joint_statements
    136    (all languages but LIN) *)
    137 definition params_of_graph_params: graph_params → params ≝
    138  λgp.
    139   let stmt_pars ≝ mk_stmt_params gp label (inl … (refl …)) in
    140   mk_params
    141    stmt_pars
    142    gp
    143    (* codeT ≝ *)(λglobals.graph (joint_statement stmt_pars globals))
    144    (λglobals.lookup …).
    145    
    146 coercion graph_params_to_params :
    147   ∀gp : graph_params.params ≝
    148     λgp.params_of_graph_params gp
    149     on _gp : graph_params to params.
    150 
    151187(* CSC: special case where localsT is a list of registers (RTL and ERTL) *)
    152 definition rtl_ertl_params ≝ λinst_pars,funct_pars.
    153   params_of_graph_params (mk_graph_params inst_pars (mk_local_params funct_pars (list register))).
     188definition rtl_ertl_params : ?→?→params ≝ λinst_pars,funct_pars.
     189  (mk_graph_params (mk_unserialized_params inst_pars (mk_local_params funct_pars (list register)))).
    154190
    155191record joint_internal_function (globals: list ident) (p:params) : Type[0] ≝

  • src/joint/TranslateUtils_paolo.ma

    r1635 r1640  
    104104  joint_internal_function globals dst_g_pars ≝
    105105  λsrc_g_pars,dst_g_pars,globals,registerT,fresh_reg,trans,empty,def.
    106   let f : label → joint_statement src_g_pars globals →
     106  let f : label → joint_statement (src_g_pars : params) globals →
    107107    joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝
    108108    λlbl,stmt,def.
    … …  
    128128  joint_internal_function … dst_g_pars ≝
    129129  λsrc_g_pars,dst_g_pars,globals,trans,empty,def.
    130   let f : label → joint_statement src_g_pars globals →
     130  let f : label → joint_statement (src_g_pars : params) globals →
    131131    joint_internal_function … dst_g_pars → joint_internal_function … dst_g_pars ≝
    132132    λlbl,stmt,def.
Note: See TracChangeset for help on using the changeset viewer.