Changeset 2286 for src/joint/Joint.ma


Ignore:
Timestamp:
Aug 2, 2012, 3:18:11 PM (8 years ago)
Author:
tranquil
Message:

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r1601 r2286  
     1include "common/BackEndOps.ma".
     2include "common/CostLabel.ma".
     3include "common/Registers.ma".
    14include "ASM/I8051.ma".
    2 include "common/CostLabel.ma".
    3 include "common/AST.ma".
    4 include "common/Registers.ma".
    55include "common/Graphs.ma".
    6 
    7 record params__: Type[1] ≝
    8  { acc_a_reg: Type[0]
    9  ; acc_b_reg: Type[0]
    10  ; dpl_reg: Type[0]
    11  ; dph_reg: Type[0]
    12  ; pair_reg: Type[0]
    13  ; generic_reg: Type[0]
    14  ; call_args: Type[0]
    15  ; call_dest: Type[0]
    16  
    17  ; extend_statements: Type[0]
     6include "utilities/lists.ma".
     7include "common/LabelledObjects.ma".
     8include "ASM/Util.ma".
     9include "common/StructuredTraces.ma".
     10
     11(* Here is the structure of parameter records (downward edges are coercions,
     12   the ↓ edges are the only explicitly defined coercions). lin_params and
     13   graph_params are simple wrappers of unserialized_params, and the coercions
     14   from them to params instantiate the missing bits with values for linarized
     15   programs and graph programs respectively.
     16
     17        lin_params      graph_params
     18              |   \_____ /____   |
     19              |         /     \  |
     20              |        /      ↓  ↓
     21              |       |      params
     22              |       |        |
     23              |       |   stmt_params
     24              |       |    /   
     25          unserialized_params             
     26
     27unserialized_params : things unrelated to being in graph or linear form
     28stmt_params : adds successor type needed to define statements
     29params : adds type of code and related properties *)
     30
     31inductive possible_flows : Type[0] ≝
     32| Labels : list label → possible_flows
     33| Call : possible_flows.
     34
     35inductive argument (T : Type[0]) : Type[0] ≝
     36| Reg : T → argument T
     37| Imm : beval → argument T.
     38
     39definition psd_argument ≝ argument register.
     40 
     41definition psd_argument_from_reg : register → psd_argument ≝ Reg register.
     42coercion reg_to_psd_argument : ∀r : register.psd_argument ≝ psd_argument_from_reg
     43  on _r : register to psd_argument.
     44
     45definition psd_argument_from_beval : beval → psd_argument ≝ Imm register.
     46coercion beval_to_psd_argument : ∀b : beval.psd_argument ≝ psd_argument_from_beval
     47  on _b : beval to psd_argument.
     48
     49definition psd_argument_from_byte : Byte → psd_argument ≝ λb.Imm ? (BVByte b).
     50coercion byte_to_psd_argument : ∀b : Byte.psd_argument ≝ psd_argument_from_byte
     51  on _b : Byte to psd_argument.
     52
     53definition hdw_argument ≝ argument Register.
     54 
     55definition hdw_argument_from_reg : Register → hdw_argument ≝ Reg Register.
     56coercion reg_to_hdw_argument : ∀r : Register.hdw_argument ≝ hdw_argument_from_reg
     57  on _r : Register to hdw_argument.
     58
     59definition hdw_argument_from_beval : beval → hdw_argument ≝ Imm Register.
     60coercion beval_to_hdw_argument : ∀b : beval.hdw_argument ≝ hdw_argument_from_beval
     61  on _b : beval to hdw_argument.
     62
     63definition hdw_argument_from_byte : Byte → hdw_argument ≝ λb.Imm ? (BVByte b).
     64coercion byte_to_hdw_argument : ∀b : Byte.psd_argument ≝ psd_argument_from_byte
     65  on _b : Byte to hdw_argument.
     66
     67definition byte_of_nat : nat → Byte ≝ bitvector_of_nat 8.
     68definition zero_byte : Byte ≝ bv_zero 8.
     69
     70record unserialized_params : Type[1] ≝
     71 { acc_a_reg: Type[0] (* registers that will eventually need to be A *)
     72 ; acc_b_reg: Type[0] (* registers that will eventually need to be B *)
     73 ; acc_a_arg: Type[0] (* arguments that will eventually need to be A *)
     74 ; acc_b_arg: Type[0] (* arguments that will eventually need to be B *)
     75 ; dpl_reg: Type[0]   (* low address registers *)
     76 ; dph_reg: Type[0]   (* high address registers *)
     77 ; dpl_arg: Type[0]   (* low address registers *)
     78 ; dph_arg: Type[0]   (* high address registers *)
     79 ; snd_arg : Type[0]  (* second argument of binary op *)
     80 ; pair_move: Type[0] (* argument of move instructions *)
     81 ; call_args: Type[0] (* arguments of function calls *)
     82 ; call_dest: Type[0] (* possible destination of function computation *)
     83 (* other instructions not fitting in the general framework *)
     84 ; ext_seq : Type[0]
     85(* ; ext_branch : Type[0]
     86 ; ext_branch_labels : ext_branch → list label*)
     87 ; ext_call : Type[0]
     88 ; ext_tailcall : Type[0]
     89 (* if needed: ; ext_fin_branch : Type[0] ; ext_fin_branch_labels : ext_fin_branch → list label *)
     90 ; paramsT : Type[0]
     91 ; localsT: Type[0]
    1892 }.
    1993
    20 record params_: Type[1] ≝
    21  { pars__:> params__
    22  ; succ: Type[0]
     94inductive joint_seq (p:unserialized_params) (globals: list ident): Type[0] ≝
     95  | COMMENT: String → joint_seq p globals
     96  | COST_LABEL: costlabel → joint_seq p globals
     97  | MOVE: pair_move p → joint_seq p globals
     98  | POP: acc_a_reg p → joint_seq p globals
     99  | PUSH: acc_a_arg p → joint_seq p globals
     100  | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_seq p globals
     101  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_seq p globals
     102  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_seq p globals
     103  | OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_seq p globals
     104  (* int done with generic move *)
     105(*| INT: generic_reg p → Byte → joint_seq p globals *)
     106  | CLEAR_CARRY: joint_seq p globals
     107  | SET_CARRY: joint_seq p globals
     108  | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_seq p globals
     109  | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_seq p globals
     110  | CALL_ID: ident → call_args p → call_dest p → joint_seq p globals
     111  | extension_seq : ext_seq p → joint_seq p globals
     112  | extension_call : ext_call p → joint_seq p globals.
     113
     114axiom EmptyString : String.
     115definition NOOP ≝ λp,globals.COMMENT p globals EmptyString.
     116
     117notation "r ← a1 .op. a2" with precedence 60 for
     118  @{'op2 $op $r $a1 $a2}.
     119notation "r ← . op . a" with precedence 60 for
     120  @{'op1 $op $r $a}.
     121notation "r ← a" with precedence 60 for
     122  @{'mov $r $a}. (* to be set in individual languages *)
     123notation "❮r, s❯ ← a1 . op . a2" with precedence 55 for
     124  @{'opaccs $op $r $s $a1 $a2}.
     125
     126interpretation "op2" 'op2 op r a1 a2 = (OP2 ? ? op r a1 a2).
     127interpretation "op1" 'op1 op r a = (OP1 ? ? op r a).
     128interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2).
     129
     130coercion extension_seq_to_seq : ∀p,globals.∀s : ext_seq p.joint_seq p globals ≝
     131  extension_seq on _s : ext_seq ? to joint_seq ??.
     132coercion extension_call_to_seq : ∀p,globals.∀s : ext_call p.joint_seq p globals ≝
     133  extension_call on _s : ext_call ? to joint_seq ??.
     134 
     135(* inductive joint_branch (p : step_params) : Type[0] ≝
     136  | COND: acc_a_reg p → label → joint_branch p
     137  | extension_branch : ext_branch p → joint_branch p.*)
     138
     139(*coercion extension_to_branch : ∀p.∀s : ext_branch p.joint_branch p ≝
     140  extension_branch on _s : ext_branch ? to joint_branch ?.*)
     141
     142inductive joint_step (p : unserialized_params) (globals : list ident) : Type[0] ≝
     143  | step_seq : joint_seq p globals → joint_step p globals
     144  | COND: acc_a_reg p → label → joint_step p globals.
     145
     146coercion seq_to_step : ∀p,globals.∀s : joint_seq p globals.joint_step p globals ≝
     147  step_seq on _s : joint_seq ?? to joint_step ??.
     148
     149definition step_flows ≝ λp,globals.λs : joint_step p globals.
     150  match s with
     151  [ step_seq s ⇒
     152    match s with
     153    [ CALL_ID _ _ _ ⇒ Call
     154    | extension_call _ ⇒ Call
     155    | _ ⇒ Labels … [ ]
     156    ]
     157  | COND _ l ⇒ Labels … [l]
     158  ].
     159
     160definition step_labels ≝
     161  λp, globals.λs : joint_step p globals.
     162    match step_flows … s with
     163    [ Labels lbls ⇒ lbls
     164    | Call ⇒ [ ]
     165    ].
     166
     167definition step_forall_labels : ∀p.∀globals.
     168    (label → Prop) → joint_step p globals → Prop ≝
     169λp,g,P,inst. All … P (step_labels … inst).
     170
     171definition step_classifier :
     172  ∀p.∀globals.
     173    joint_step p globals → status_class ≝ λp,g,s.
     174  match s with
     175  [ step_seq s ⇒
     176    match s with
     177    [ CALL_ID _ _ _ ⇒ cl_call
     178    | extension_call _ ⇒ cl_call
     179    | _ ⇒ cl_other
     180    ]
     181  | COND _ _ ⇒ cl_jump
     182  ].
     183
     184record stmt_params : Type[1] ≝
     185  { uns_pars :> unserialized_params
     186  ; succ : Type[0]
     187  ; succ_label : succ → option label
     188  }.
     189
     190inductive joint_fin_step (p: unserialized_params): Type[0] ≝
     191  | GOTO: label → joint_fin_step p
     192  | RETURN: joint_fin_step p
     193  | tailcall : ext_tailcall p → joint_fin_step p.
     194
     195definition fin_step_flows ≝ λp.λs : joint_fin_step p.
     196  match s with
     197  [ GOTO l ⇒ Labels … [l]
     198  | tailcall _ ⇒ Call (* tailcalls will need to be integrated in structured traces *)
     199  | _ ⇒ Labels … [ ]
     200  ].
     201
     202definition fin_step_labels ≝
     203  λp.λs : joint_fin_step p.
     204    match fin_step_flows … s with
     205    [ Labels lbls ⇒ lbls
     206    | Call ⇒ [ ]
     207    ].
     208
     209definition fin_step_classifier :
     210  ∀p : stmt_params.
     211    joint_fin_step p → status_class
     212  ≝ λp,s.
     213  match s with
     214  [ GOTO _ ⇒ cl_other
     215  | _ ⇒ cl_return
     216  ].
     217
     218inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
     219  | sequential: joint_step p globals → succ p → joint_statement p globals
     220  | final: joint_fin_step p → joint_statement p globals.
     221
     222definition stmt_classifier :
     223  ∀p : stmt_params.∀globals.
     224    joint_statement p globals → status_class
     225  ≝ λp,g,s.
     226  match s with
     227  [ sequential stp _ ⇒ step_classifier p g stp
     228  | final stp ⇒ fin_step_classifier p stp
     229  ].
     230
     231coercion extension_fin_to_fin_step : ∀p : stmt_params.
     232  ∀s : ext_tailcall p.joint_fin_step p ≝
     233  tailcall on _s : ext_tailcall ? to joint_fin_step ?.
     234
     235coercion fin_step_to_stmt : ∀p : stmt_params.∀globals.
     236  ∀s : joint_fin_step p.joint_statement p globals ≝
     237  final on _s : joint_fin_step ? to joint_statement ??.
     238
     239record params : Type[1] ≝
     240 { stmt_pars :> stmt_params
     241 ; codeT: list ident → Type[0]
     242 ; code_point : Type[0]
     243 ; stmt_at : ∀globals.codeT globals → code_point → option (joint_statement stmt_pars globals)
     244 ; point_of_label : ∀globals.codeT globals → label → option code_point
     245 ; point_of_succ : code_point → succ stmt_pars → code_point
    23246 }.
     247
     248definition code_has_point ≝
     249  λp,globals,c,pt.match stmt_at p globals c pt with [Some _ ⇒ true | None ⇒ false].
     250
     251(* interpretation "code membership" 'mem p c = (code_has_point ?? c p). *)
     252
     253definition point_in_code ≝ λp,globals,code.Σpt.bool_to_Prop (code_has_point p globals code pt).
     254unification 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)).
     255
     256definition stmt_at_safe ≝ λp,globals,code.λpt : point_in_code p globals code.
     257  match pt with
     258  [ mk_Sig pt' pt_prf ⇒
     259    match stmt_at … code pt' return λx.stmt_at … code pt' = x → ? with
     260    [ Some x ⇒ λ_.x
     261    | None ⇒ λabs.⊥
     262    ] (refl …)
     263  ]. normalize in pt_prf;
     264    >abs in pt_prf; // qed.
     265
     266definition forall_statements : ∀p : params.∀globals.pred_transformer (joint_statement p globals) (codeT p globals)  ≝
     267  λp,globals,P,c. ∀pt,s.stmt_at ?? c pt = Some ? s → P s.
     268
     269definition forall_statements_i :
     270  ∀p : params.∀globals.(code_point p → joint_statement p globals → Prop) →
     271    codeT p globals → Prop  ≝
     272  λp,globals,P,c. ∀pt,s.stmt_at ?? c pt = Some ? s → P pt s.
     273
     274lemma forall_statements_mp : ∀p,globals.modus_ponens ?? (forall_statements p globals).
     275#p #globals #P #Q #H #y #G #pnt #s #EQ @H @(G … EQ) qed.
     276
     277lemma forall_statements_i_mp : ∀p,globals.∀P,Q.(∀pt,s.P pt s → Q pt s) →
     278  ∀c.forall_statements_i p globals P c → forall_statements_i p globals Q c.
     279#p #globals #P #Q #H #y #G #pnt #s #EQ @H @(G … EQ) qed.
     280
     281definition code_has_label ≝ λp,globals,c,l.
     282  match point_of_label p globals c l with
     283  [ Some pt ⇒ code_has_point … c pt
     284  | None ⇒ false
     285  ].
     286
     287definition stmt_explicit_labels :
     288  ∀p,globals.
     289  joint_statement p globals → list label ≝
     290  λp,globals,stmt. match stmt with
     291  [ sequential c _ ⇒ step_labels … c
     292  | final c ⇒ fin_step_labels … c
     293  ].
     294
     295definition stmt_implicit_label : ∀p,globals.joint_statement p globals →
     296  option label ≝
     297 λp,globals,s.match s with [ sequential _ s ⇒ succ_label … s | _ ⇒ None ?].
     298 
     299definition stmt_labels : ∀p : stmt_params.∀globals.
     300    joint_statement p globals → list label ≝
     301  λp,g,stmt.
     302  (match stmt_implicit_label … stmt with
     303     [ Some l ⇒ [l]
     304     | None ⇒ [ ]
     305     ]) @ stmt_explicit_labels … stmt.
     306
     307definition stmt_forall_labels ≝
     308  λp, globals.λ P : label → Prop.λs : joint_statement p globals.
     309  All … P (stmt_labels … s).
     310
     311lemma stmt_forall_labels_explicit : ∀p,globals,P.∀s : joint_statement p globals.
     312  stmt_forall_labels … P s → All … P (stmt_explicit_labels … s).
     313#p#globals#P #s
     314whd in ⊢ (% → ?);
     315whd in ⊢ (???% → ?);
     316elim (stmt_implicit_label ???) [2: #next * #_] //
     317qed.
     318
     319lemma stmt_forall_labels_implicit : ∀p,globals,P.∀s : joint_statement p globals.
     320  stmt_forall_labels … P s →
     321    opt_All … P (stmt_implicit_label … s).
     322#p#globals#P#s
     323whd in ⊢ (% → ?);
     324whd in ⊢ (???% → ?);
     325elim (stmt_implicit_label ???)
     326[ //
     327| #next * #Pnext #_ @Pnext
     328]
     329qed.
     330
     331definition code_forall_labels ≝
     332  λp,globals,P,c.forall_statements p globals (stmt_forall_labels … P) c.
     333
     334lemma code_forall_labels_mp : ∀p,globals,P,Q.(∀l.P l → Q l) →
     335  ∀c.code_forall_labels p globals P c → code_forall_labels … Q c ≝
     336  λp,globals,P,Q,H.forall_statements_mp … (λs. All_mp … H ?).
     337
     338record lin_params : Type[1] ≝
     339  { l_u_pars : unserialized_params }.
     340 
     341lemma index_of_label_length : ∀tag,A,lbl,l.occurs_exactly_once ?? lbl l → lt (index_of_label tag A lbl l) (|l|).
     342#tag #A #lbl #l elim l [*]
     343** [2: #id] #a #tl #IH
     344[ change with (if (eq_identifier ???) then ? else ?) in match (occurs_exactly_once ????);
     345  change with (if (eq_identifier ???) then ? else ?) in match (index_of_label ????);
     346  @eq_identifier_elim #Heq normalize nodelta
     347  [ #_ normalize / by /]
     348| whd in ⊢ (?%→?%?);
     349]
     350#H >(index_of_label_from_internal … H)
     351@le_S_S @(IH H)
     352qed.
     353
     354(* mv *)
     355lemma nth_opt_hit_length : ∀A,l,n,x.nth_opt A n l = Some ? x → n < |l|.
     356#A #l elim l normalize [ #n #x #ABS destruct(ABS)]
     357#hd #tl #IH * [2:#n] #x normalize [#H @le_S_S @(IH … H)] /2 by /
     358qed.
     359
     360lemma nth_opt_miss_length : ∀A,l,n.nth_opt A n l = None ? → n ≥ |l|.
     361#A #l elim l [//] #hd #tl #IH * normalize [#ABS destruct(ABS)]
     362#n' #H @le_S_S @(IH … H)
     363qed.
     364
     365lemma nth_opt_safe : ∀A,l,n,prf.nth_opt A n l = Some ? (nth_safe A n l prf).
     366#A #l elim l
     367[ #n #ABS @⊥ /2 by absurd/
     368| #hd #tl #IH * normalize //
     369]
     370qed.
     371
     372definition lin_params_to_params ≝
     373  λlp : lin_params.
     374     mk_params
     375      (mk_stmt_params (l_u_pars lp) unit (λ_.None ?))
     376    (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals)))
     377    (* code_point ≝ *)ℕ
     378    (* stmt_at ≝ *)(λglobals,code,point.! ls ← nth_opt ? point code ; return \snd ls)
     379    (* point_of_label ≝ *)(λglobals,c,lbl.
     380      If occurs_exactly_once ?? lbl c then with prf do
     381        return index_of_label ?? lbl c
     382      else
     383        None ?)
     384    (* point_of_succ ≝ *)(λcurrent.λ_.S (current)).
     385
     386coercion lp_to_p : ∀lp : lin_params.params ≝ lin_params_to_params
     387  on _lp : lin_params to params.
     388 
     389lemma lin_code_has_point : ∀lp : lin_params.∀globals.∀code:codeT lp globals.
     390  ∀pt.code_has_point … code pt = leb (S pt) (|code|).
     391#lp #globals #code elim code
     392[ #pt %
     393| #hd #tl #IH * [%]
     394  #n @IH
     395]qed.
     396
     397lemma lin_code_has_label : ∀lp : lin_params.∀globals.∀code:codeT lp globals.
     398  ∀lbl.code_has_label … code lbl = occurs_exactly_once ?? lbl code.
     399#lp #globals #code #lbl
     400whd in match (code_has_label ????);
     401whd in match (point_of_label ????);
     402elim (true_or_false_Prop (occurs_exactly_once ?? lbl code))
     403#Heq >Heq normalize nodelta
     404[ >lin_code_has_point @(leb_elim (S ?)) [#_ |
     405  #ABS elim(absurd ?? ABS) -ABS
     406  @index_of_label_length assumption ]] %
     407qed.
     408
     409record graph_params : Type[1] ≝
     410  { g_u_pars : unserialized_params }.
    24411
    25412(* One common instantiation of params via Graphs of joint_statements
    26413   (all languages but LIN) *)
    27 definition graph_params_ : params__ → params_ ≝
    28  λpars__. mk_params_ pars__ label.
    29 
    30 inductive joint_instruction (p:params__) (globals: list ident): Type[0] ≝
    31   | COMMENT: String → joint_instruction p globals
    32   | COST_LABEL: costlabel → joint_instruction p globals
    33   | INT: generic_reg p → Byte → joint_instruction p globals
    34   | MOVE: pair_reg p → joint_instruction p globals
    35   | POP: acc_a_reg p → joint_instruction p globals
    36   | PUSH: acc_a_reg p → joint_instruction p globals
    37   | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals
    38   | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_reg p → acc_b_reg p → joint_instruction p globals
    39   | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_instruction p globals
    40   | OP2: Op2 → acc_a_reg p → acc_a_reg p → generic_reg p → joint_instruction p globals
    41   | CLEAR_CARRY: joint_instruction p globals
    42   | SET_CARRY: joint_instruction p globals
    43   | LOAD: acc_a_reg p → dpl_reg p → dph_reg p → joint_instruction p globals
    44   | STORE: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals
    45   | CALL_ID: ident → call_args p → call_dest p → joint_instruction p globals
    46   | COND: acc_a_reg p → label → joint_instruction p globals
    47   | extension: extend_statements p → joint_instruction p globals.
    48 
    49 inductive joint_statement (p:params_) (globals: list ident): Type[0] ≝
    50   | sequential: joint_instruction p globals → succ p → joint_statement p globals
    51   | GOTO: label → joint_statement p globals
    52   | RETURN: joint_statement p globals.
    53 
    54 record params0: Type[1] ≝
    55  { pars__' :> params__
    56  ; resultT: Type[0]
    57  ; paramsT: Type[0]
    58  }.
    59 
    60 record params1 : Type[1] ≝
    61  { pars0 :> params0
    62  ; localsT: Type[0]
    63  }.
    64 
    65 record params (globals: list ident): Type[1] ≝
    66  { succ_ : Type[0]
    67  ; pars1 :> params1
    68  ; codeT: Type[0]
    69  ; lookup: codeT → label → option (joint_statement (mk_params_ pars1 succ_) globals)
    70  }.
    71  
    72 definition params__of_params: ∀globals. params globals → params_ ≝
    73  λglobals,pars. mk_params_ pars (succ_ … pars).
    74 coercion params__of_params: ∀globals.∀p: params globals. params_ ≝ params__of_params
    75  on _p: params ? to params_.
    76 
    77 include alias "common/Graphs.ma". (* To pick the right lookup *)
    78 
    79 (* One common instantiation of params via Graphs of joint_statements
    80    (all languages but LIN) *)
    81 definition graph_params: params1 → ∀globals: list ident. params globals ≝
    82  λpars1,globals.
    83   mk_params globals label pars1
    84    (graph (joint_statement (graph_params_ pars1) globals)) (lookup …).
    85 
    86 
    87 (* CSC: special case where localsT is a list of register (RTL and ERTL) *)
    88 definition rtl_ertl_params1 ≝ λpars0. mk_params1 pars0 (list register).
    89 definition rtl_ertl_params ≝ λpars0. graph_params (rtl_ertl_params1 pars0).
    90 
    91 record joint_internal_function (globals: list ident) (p:params globals) : Type[0] ≝
     414definition graph_params_to_params ≝
     415  λgp : graph_params.
     416     mk_params
     417      (mk_stmt_params (g_u_pars gp) label (Some ?))
     418    (* codeT ≝ *)(λglobals.graph (joint_statement ? globals))
     419    (* code_point ≝ *)label
     420    (* stmt_at ≝ *)(λglobals,code.lookup LabelTag ? code)
     421    (* point_of_label ≝ *)(λ_.λ_.λlbl.return lbl)
     422    (* point_of_succ ≝ *)(λ_.λlbl.lbl).
     423
     424coercion gp_to_p : ∀gp:graph_params.params ≝ graph_params_to_params
     425on _gp : graph_params to params.
     426
     427lemma graph_code_has_point : ∀gp : graph_params.∀globals.∀code:codeT gp globals.
     428  ∀pt.code_has_point … code pt = (pt ∈ code). // qed.
     429
     430lemma graph_code_has_label : ∀gp : graph_params.∀globals.∀code:codeT gp globals.
     431  ∀lbl.code_has_label … code lbl = (lbl ∈ code). // qed.
     432
     433definition stmt_forall_succ ≝ λp,globals.λP : succ p → Prop.
     434  λs : joint_statement p globals.
     435  match s with
     436  [ sequential _ n ⇒ P n
     437  | _ ⇒ True
     438  ].
     439
     440definition statement_closed : ∀globals.∀p : params.
     441  codeT p globals → code_point p → (joint_statement p globals) → Prop ≝
     442λglobals,p,code,pt,s.
     443  All ? (λl.bool_to_Prop (code_has_label ?? code l)) (stmt_explicit_labels … s) ∧
     444  stmt_forall_succ … (λn.bool_to_Prop (code_has_point … code (point_of_succ ? pt n))) s.
     445
     446definition code_closed : ∀p : params.∀globals.
     447  codeT p globals → Prop ≝ λp,globals,code.
     448    forall_statements_i … (statement_closed … code) code.
     449
     450record joint_internal_function (p:params) (globals: list ident) : Type[0] ≝
    92451{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
    93452  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
     453  (* Paolo: if we want this machinery to work for RTLabs too, we will need the
     454     following, right? *)
    94455(*  joint_if_sig: signature;  -- dropped in front end *)
    95   joint_if_result   : resultT p;
     456  joint_if_result   : call_dest p;
    96457  joint_if_params   : paramsT p;
    97   joint_if_locals   : localsT p;
     458  joint_if_locals   : list (localsT p); (* use void where no locals are present *)
    98459(*CSC: XXXXX stacksize unused for LTL-...*)
    99460  joint_if_stacksize: nat;
    100   joint_if_code     : codeT … p;
    101 (*CSC: XXXXX entry unused for LIN, but invariant in that case... *)
    102   joint_if_entry    : Σl: label. lookup … joint_if_code l ≠ None ?;
    103 (*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *)
    104   joint_if_exit     : Σl: label. lookup … joint_if_code l ≠ None ?
     461  joint_if_code     : codeT p globals ;
     462  joint_if_entry : point_in_code … joint_if_code ;
     463  joint_if_exit : point_in_code … joint_if_code
    105464}.
    106465
    107 (* Currified form *)
    108 definition set_joint_if_exit ≝
    109   λglobals,pars.
    110   λexit: label.
    111   λp:joint_internal_function globals pars.
    112   λprf: lookup … (joint_if_code … p) exit ≠ None ?.
    113    mk_joint_internal_function globals pars
    114     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    115     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
    116     (joint_if_code … p) (joint_if_entry … p) (mk_Sig … exit prf).
     466definition joint_closed_internal_function ≝
     467  λp,globals.
     468    Σdef : joint_internal_function globals p. code_closed … (joint_if_code … def).
    117469
    118470definition set_joint_code ≝
    119471  λglobals: list ident.
    120   λpars: params globals.
    121   λint_fun: joint_internal_function globals pars.
    122   λgraph: codeT … pars.
     472  λpars: params.
     473  λint_fun: joint_internal_function pars globals.
     474  λgraph: codeT pars globals.
    123475  λentry.
    124476  λexit.
    125     mk_joint_internal_function globals pars
     477    mk_joint_internal_function pars globals
    126478      (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun)
    127479      (joint_if_params … int_fun) (joint_if_locals … int_fun) (joint_if_stacksize … int_fun)
     
    129481
    130482definition set_joint_if_graph ≝
    131   λglobals,pars.
     483  λglobals.λpars : graph_params.
    132484  λgraph.
    133   λp:joint_internal_function globals pars.
    134   λentry_prf: lookup … graph (joint_if_entry … p) ≠ None ?.
    135   λexit_prf: lookup … graph (joint_if_exit … p) ≠ None ?.
    136     set_joint_code globals pars p graph
    137       (mk_Sig … (joint_if_entry … p) entry_prf) (mk_Sig … (joint_if_exit … p) exit_prf).
     485  λp:joint_internal_function pars globals.
     486  λentry_prf.
     487  λexit_prf.
     488    set_joint_code globals pars p
     489      graph
     490      (mk_Sig ?? (joint_if_entry ?? p) entry_prf)
     491      (mk_Sig … (joint_if_exit ?? p) exit_prf).
    138492
    139493definition set_luniverse ≝
     
    154508    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
    155509    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
    156 
     510   
    157511(* Specialized for graph_params *)
    158512definition add_graph ≝
    159   λpars1,globals.λl:label.λstmt.λp:joint_internal_function globals (graph_params pars1 globals).
    160    let code ≝ add … (joint_if_code ?? p) l stmt in
    161     mk_joint_internal_function … (graph_params … globals)
     513  λg_pars : graph_params.λglobals.λl:label.λstmt.
     514    λp:joint_internal_function g_pars globals.
     515   let code ≝ add … (joint_if_code … p) l stmt in
     516    mk_joint_internal_function …
    162517     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    163518     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
    164      code (pi1 ?? (joint_if_entry … p)) (pi1 … (joint_if_exit … p)).
    165   normalize nodelta;
    166   [ cases (joint_if_entry … p) | cases (joint_if_exit … p)]
    167   #LBL #LBL_PRF @graph_add_lookup @LBL_PRF
    168 qed.
     519     code
     520     (pi1 … (joint_if_entry … p))
     521     (pi1 … (joint_if_exit … p)).
     522>graph_code_has_point whd in match code; >mem_set_add
     523@orb_Prop_r [elim (joint_if_entry ???) | elim (joint_if_exit ???) ]
     524#x #H <graph_code_has_point @H
     525qed.
    169526
    170527definition set_locals ≝
    171   λglobals,pars.
    172   λp : joint_internal_function globals pars.
     528  λpars,globals.
     529  λp : joint_internal_function pars globals.
    173530  λlocals.
    174    mk_joint_internal_function globals pars
     531   mk_joint_internal_function pars globals
    175532    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    176533    (joint_if_params … p) locals (joint_if_stacksize … p)
     
    180537
    181538definition joint_program ≝
    182  λp:∀globals.params globals. program (λglobals. joint_function globals (p globals)) nat.
     539 λp:params. program (joint_function p) nat.
Note: See TracChangeset for help on using the changeset viewer.