Ignore:
Timestamp:
Apr 6, 2012, 8:02:10 PM (9 years ago)
Author:
tranquil
Message:

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint_paolo.ma

    r1644 r1882  
    44include "common/Registers.ma".
    55include "common/Graphs.ma".
     6include "utilities/lists.ma".
     7include "common/LabelledObjects.ma".
     8include "ASM/Util.ma".
    69
    710(* Here is the structure of parameter records (downward edges are coercions,
     
    1215
    1316        lin_params      graph_params
    14           |       \_____ /____   |
    15           |             /     \  |
    16           \_______     /      ↓  ↓
    17                   \   _\____ params
    18                    \_/  \      |
    19                     / \  \     ↓
    20               _____/   unserialized_params
    21              /      _______/   |
    22             /      /           |
    23      stmt_params  /   local_params
    24         |      __/             |
    25     inst_params       funct_params
    26 
    27 inst_params : types needed to define instructions
     17              |   \_____ /____   |
     18              |         /     \  |
     19              |        /      ↓  ↓
     20              |       |      params
     21              |       |        |
     22              |       |   stmt_params
     23              |       |    /   
     24          unserialized_params             
     25            |            \       
     26            |             \     
     27            |         local_params
     28            |              |   
     29    step_params       funct_params
     30
     31step_params : types needed to define steps (stmts with a default fallthrough)
    2832stmt_params : adds successor type needed to define statements
    2933funct_params : types of result register and parameters of function
    3034local_params : adds types of local registers
    31 params : adds type of code and lookup function
    32 graph_params : is made just of inst_params and local_params, and the coercion
    33   to params adds structure common to graph languages *)
    34 
    35 record inst_params : Type[1] ≝
     35params : adds type of code and related properties *)
     36
     37record step_params : Type[1] ≝
    3638 { acc_a_reg: Type[0] (* registers that will eventually need to be A *)
    3739 ; acc_b_reg: Type[0] (* registers that will eventually need to be B *)
     
    4648 ; call_args: Type[0] (* arguments of function calls *)
    4749 ; call_dest: Type[0] (* possible destination of function computation *)
    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
     50 ; ext_step: Type[0] (* other instructions not fitting in the general framework *)
     51 ; ext_step_labels : ext_step → list label
     52 ; ext_fin_stmt: Type[0] (* final instructions (e.g. tailcalls) not fitting in the general framework *)
     53 ; ext_fin_stmt_labels : ext_fin_stmt → list label
    5254 }.
    5355 
    54 inductive joint_instruction (p:inst_params) (globals: list ident): Type[0] ≝
    55   | COMMENT: String → joint_instruction p globals
    56   | COST_LABEL: costlabel → joint_instruction p globals
    57   | MOVE: pair_move p → joint_instruction p globals
    58   | POP: acc_a_reg p → joint_instruction p globals
    59   | PUSH: acc_a_arg p → joint_instruction p globals
    60   | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals
    61   | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_instruction p globals
    62   | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_instruction p globals
    63   | OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_instruction p globals
     56inductive joint_step (p:step_params) (globals: list ident): Type[0] ≝
     57  | COMMENT: String → joint_step p globals
     58  | COST_LABEL: costlabel → joint_step p globals
     59  | MOVE: pair_move p → joint_step p globals
     60  | POP: acc_a_reg p → joint_step p globals
     61  | PUSH: acc_a_arg p → joint_step p globals
     62  | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_step p globals
     63  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_step p globals
     64  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_step p globals
     65  | OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_step p globals
    6466  (* int done with generic move *)
    65 (*| INT: generic_reg p → Byte → joint_instruction p globals *)
    66   | CLEAR_CARRY: joint_instruction p globals
    67   | SET_CARRY: joint_instruction p globals
    68   | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_instruction p globals
    69   | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_instruction p globals
    70   | CALL_ID: ident → call_args p → call_dest p → joint_instruction p globals
    71   | COND: acc_a_reg p → label → joint_instruction p globals
    72   | extension: ext_instruction p → joint_instruction p globals.
    73 
    74 coercion extension_to_instruction :
    75   ∀p,globals.∀c : ext_instruction p.joint_instruction p globals ≝
    76   extension
    77   on _c : ext_instruction ? to joint_instruction ??.
    78 
    79 notation "r ← a1 .op. a2" with precedence 50 for
     67(*| INT: generic_reg p → Byte → joint_step p globals *)
     68  | CLEAR_CARRY: joint_step p globals
     69  | SET_CARRY: joint_step p globals
     70  | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_step p globals
     71  | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_step p globals
     72  | CALL_ID: ident → call_args p → call_dest p → joint_step p globals
     73  | COND: acc_a_reg p → label → joint_step p globals
     74  | extension: ext_step p → joint_step p globals.
     75
     76notation "r ← a1 .op. a2" with precedence 55 for
    8077  @{'op2 $op $r $a1 $a2}.
    81 notation "r ← . op . a" with precedence 50 for
     78notation "r ← . op . a" with precedence 55 for
    8279  @{'op1 $op $r $a}.
    83 notation "r ← a" with precedence 50 for
     80notation "r ← a" with precedence 55 for
    8481  @{'mov $r $a}. (* to be set in individual languages *)
    8582notation "❮r, s❯ ← a1 . op . a2" with precedence 50 for
     
    9087interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2).
    9188
    92 
    93 definition inst_forall_labels : ∀p : inst_params.∀globals.
    94     (label → Prop) → joint_instruction p globals → Prop ≝
    95 λp,g,P,inst. match inst with
    96   [ COND _ l ⇒ P l
    97   | extension ext_s ⇒ ext_forall_labels p P ext_s
    98   | _ ⇒ True
    99  ].
    100 
     89coercion extension_to_step : ∀p,globals.∀s : ext_step p.joint_step p globals ≝
     90  extension on _s : ext_step ? to joint_step ??.
     91
     92definition step_labels ≝
     93  λp, globals.λs : joint_step p globals.
     94    match s with
     95    [ COND _ l ⇒ [l]
     96    | extension ext_s ⇒ ext_step_labels ? ext_s
     97    | _ ⇒ [ ]
     98    ].
     99
     100definition step_forall_labels : ∀p : step_params.∀globals.
     101    (label → Prop) → joint_step p globals → Prop ≝
     102λp,g,P,inst. All … P (step_labels … inst).
     103 
    101104record funct_params : Type[1] ≝
    102105  { resultT : Type[0]
     
    109112 }.
    110113
     114
    111115record unserialized_params : Type[1] ≝
    112  { u_inst_pars :> inst_params
     116 { u_inst_pars :> step_params
    113117 ; u_local_pars :> local_params
    114118 }.
    115119
    116120record stmt_params : Type[1] ≝
    117   { unserialized_pars :> unserialized_params
     121  { uns_pars :> unserialized_params
    118122  ; succ : Type[0]
    119   ; succ_forall_labels : (label → Prop) → succ → Prop
     123  ; succ_label : succ → option label
    120124  }.
    121125
    122126inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
    123   | sequential: joint_instruction p globals → succ p → joint_statement p globals
     127  | sequential: joint_step p globals → succ p → joint_statement p globals
    124128  | GOTO: label → joint_statement p globals
    125129  | RETURN: joint_statement p globals
    126   | extension_fin : ext_fin_instruction p → joint_statement p globals.
    127 
    128 coercion extension_fin_to_statement :
    129   ∀p : stmt_params.∀globals.∀c : ext_fin_instruction p.joint_statement p globals ≝
    130   extension_fin
    131   on _c : ext_fin_instruction ? to joint_statement ??.
     130  | extension_fin : ext_fin_stmt p → joint_statement p globals.
     131
     132coercion extension_fin_to_stmt : ∀p : stmt_params.∀globals.∀s : ext_fin_stmt p.joint_statement p globals ≝
     133  extension_fin on _s : ext_fin_stmt ? to joint_statement ??.
     134
     135definition no_seq ≝ λp : stmt_params.λglobals.λs : joint_statement p globals.
     136  match s with
     137  [ sequential _ _ ⇒ False
     138  | _ ⇒ True
     139  ].
    132140
    133141record params : Type[1] ≝
    134142 { stmt_pars :> stmt_params
    135143 ; codeT: list ident → Type[0]
    136  ; code_has_label: ∀globals.codeT globals → label → Prop
    137  ; forall_statements : ∀globals.(joint_statement stmt_pars globals → Prop) →
    138     codeT globals → Prop
     144 ; code_point : Type[0]
     145 ; stmt_at : ∀globals.codeT globals → code_point → option (joint_statement stmt_pars globals)
     146 ; point_of_label : ∀globals.codeT globals → label → option code_point
     147 ; point_of_succ : code_point → succ stmt_pars → code_point
    139148 }.
    140149
    141 
    142 definition stmt_forall_labels : ∀p : stmt_params.∀globals.
    143     (label → Prop) → joint_statement p globals → Prop ≝
    144   λp,g,P,stmt. match stmt with
    145   [ sequential inst next ⇒ inst_forall_labels p g P inst ∧ succ_forall_labels p P next
    146   | GOTO l ⇒ P l
    147   | RETURN ⇒ True
    148   | extension_fin c ⇒ ext_fin_forall_labels … P c
     150definition code_has_point ≝
     151  λp,globals,c,pt.match stmt_at p globals c pt with [Some _ ⇒ true | None ⇒ false].
     152
     153interpretation "code membership" 'mem p c = (code_has_point ?? c p).
     154
     155definition point_in_code ≝ λp,globals,code.Σpt.bool_to_Prop (code_has_point p globals code pt).
     156unification 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)).
     157
     158definition stmt_at_safe ≝ λp,globals,code.λpt : point_in_code p globals code.
     159  match pt with
     160  [ mk_Sig pt' pt_prf ⇒
     161    match stmt_at … code pt' return λx.stmt_at … code pt' = x → ? with
     162    [ Some x ⇒ λ_.x
     163    | None ⇒ λabs.⊥
     164    ] (refl …)
     165  ]. normalize in pt_prf;
     166    >abs in pt_prf; // qed.
     167
     168definition forall_statements : ∀p : params.∀globals.pred_transformer (joint_statement p globals) (codeT p globals)  ≝
     169  λp,globals,P,c. ∀pt,s.stmt_at ?? c pt = Some ? s → P s.
     170
     171definition forall_statements_i :
     172  ∀p : params.∀globals.(code_point p → joint_statement p globals → Prop) →
     173    codeT p globals → Prop  ≝
     174  λp,globals,P,c. ∀pt,s.stmt_at ?? c pt = Some ? s → P pt s.
     175
     176lemma forall_statements_mp : ∀p,globals.modus_ponens ?? (forall_statements p globals).
     177#p #globals #P #Q #H #y #G #pnt #s #EQ @H @(G … EQ) qed.
     178
     179lemma forall_statements_i_mp : ∀p,globals.∀P,Q.(∀pt,s.P pt s → Q pt s) →
     180  ∀c.forall_statements_i p globals P c → forall_statements_i p globals Q c.
     181#p #globals #P #Q #H #y #G #pnt #s #EQ @H @(G … EQ) qed.
     182
     183definition code_has_label ≝ λp,globals,c,l.
     184  match point_of_label p globals c l with
     185  [ Some pt ⇒ code_has_point … c pt
     186  | None ⇒ false
    149187  ].
     188
     189definition stmt_explicit_labels :
     190  ∀p,globals.
     191  joint_statement p globals → list label ≝
     192  λp,globals,stmt. match stmt with
     193  [ sequential c _ ⇒ step_labels … c
     194  | GOTO l ⇒ [ l ]
     195  | RETURN ⇒ [ ]
     196  | extension_fin c ⇒ ext_fin_stmt_labels … c
     197  ].
     198
     199definition stmt_implicit_label : ∀p,globals.joint_statement p globals →
     200  option label ≝
     201 λp,globals,s.match s with [ sequential _ s ⇒ succ_label … s | _ ⇒ None ?].
     202 
     203definition stmt_labels : ∀p : stmt_params.∀globals.
     204    joint_statement p globals → list label ≝
     205  λp,g,stmt.
     206  (match stmt_implicit_label … stmt with
     207     [ Some l ⇒ [l]
     208     | None ⇒ [ ]
     209     ]) @ stmt_explicit_labels … stmt.
     210
     211definition stmt_forall_labels ≝
     212  λp, globals.λ P : label → Prop.λs : joint_statement p globals.
     213  All … P (stmt_labels … s).
     214
     215lemma stmt_forall_labels_explicit : ∀p,globals,P.∀s : joint_statement p globals.
     216  stmt_forall_labels … P s → All … P (stmt_explicit_labels … s).
     217#p#globals#P #s
     218whd in ⊢ (% → ?);
     219whd in ⊢ (???% → ?);
     220elim (stmt_implicit_label ???) [2: #next * #_] //
     221qed.
     222
     223lemma stmt_forall_labels_implicit : ∀p,globals,P.∀s : joint_statement p globals.
     224  stmt_forall_labels … P s →
     225    opt_All … P (stmt_implicit_label … s).
     226#p#globals#P#s
     227whd in ⊢ (% → ?);
     228whd in ⊢ (???% → ?);
     229elim (stmt_implicit_label ???)
     230[ //
     231| #next * #Pnext #_ @Pnext
     232]
     233qed.
     234
     235definition code_forall_labels ≝
     236  λp,globals,P,c.forall_statements p globals (stmt_forall_labels … P) c.
     237
     238lemma code_forall_labels_mp : ∀p,globals,P,Q.(∀l.P l → Q l) →
     239  ∀c.code_forall_labels p globals P c → code_forall_labels … Q c ≝
     240  λp,globals,P,Q,H.forall_statements_mp … (λs. All_mp … H ?).
    150241
    151242record lin_params : Type[1] ≝
    152243  { l_u_pars :> unserialized_params }.
    153 
    154 include "utilities/option.ma".
     244 
     245lemma index_of_label_length : ∀tag,A,lbl,l.occurs_exactly_once ?? lbl l → lt (index_of_label tag A lbl l) (|l|).
     246#tag #A #lbl #l elim l [*]
     247** [2: #id] #a #tl #IH
     248[ change with (if (eq_identifier ???) then ? else ?) in match (occurs_exactly_once ????);
     249  change with (if (eq_identifier ???) then ? else ?) in match (index_of_label ????);
     250  @eq_identifier_elim #Heq normalize nodelta
     251  [ #_ normalize / by /]
     252| whd in ⊢ (?%→?%?);
     253]
     254#H >(index_of_label_from_internal … H)
     255@le_S_S @(IH H)
     256qed.
     257
     258(* mv *)
     259lemma nth_opt_hit_length : ∀A,l,n,x.nth_opt A n l = Some ? x → n < |l|.
     260#A #l elim l normalize [ #n #x #ABS destruct(ABS)]
     261#hd #tl #IH * [2:#n] #x normalize [#H @le_S_S @(IH … H)] /2 by /
     262qed.
     263
     264lemma nth_opt_miss_length : ∀A,l,n.nth_opt A n l = None ? → n ≥ |l|.
     265#A #l elim l [//] #hd #tl #IH * normalize [#ABS destruct(ABS)]
     266#n' #H @le_S_S @(IH … H)
     267qed.
     268
     269lemma nth_opt_safe : ∀A,l,n,prf.nth_opt A n l = Some ? (nth_safe A n l prf).
     270#A #l elim l
     271[ #n #ABS @⊥ /2 by absurd/
     272| #hd #tl #IH * normalize //
     273]
     274qed.
    155275
    156276definition lin_params_to_params ≝
    157277  λlp : lin_params.
    158278     mk_params
    159       (mk_stmt_params lp unit (λ_.λ_.True))
     279      (mk_stmt_params lp unit (λ_.None ?))
    160280    (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals)))
    161     (* code_has_label ≝ *)(λglobals,code,lbl.Exists ?
    162         (λl_stmt. \fst l_stmt = Some ? lbl) code)
    163     (* forall_statements ≝ *)(λglobals,P,code.All ?
    164         (λl_stmt. P (\snd l_stmt)) code).
     281    (* code_point ≝ *)ℕ
     282    (* stmt_at ≝ *)(λglobals,code,point.! ls ← nth_opt ? point code ; return \snd ls)
     283    (* point_of_label ≝ *)(λglobals,c,lbl.
     284      If occurs_exactly_once ?? lbl c then with prf do
     285        return index_of_label ?? lbl c
     286      else
     287        None ?)
     288    (* point_of_succ ≝ *)(λcurrent.λ_.S (current)).
    165289
    166290coercion lp_to_p : ∀lp : lin_params.params ≝ lin_params_to_params
    167291  on _lp : lin_params to params.
     292 
     293lemma lin_code_has_point : ∀lp : lin_params.∀globals.∀code:codeT lp globals.
     294  ∀pt.pt ∈ code = leb (S pt) (|code|).
     295#lp #globals #code elim code
     296[ #pt %
     297| #hd #tl #IH * [%]
     298  #n @IH
     299]qed.
     300
     301lemma lin_code_has_label : ∀lp : lin_params.∀globals.∀code:codeT lp globals.
     302  ∀lbl.code_has_label … code lbl = occurs_exactly_once ?? lbl code.
     303#lp #globals #code #lbl
     304whd in match (code_has_label ????);
     305whd in match (point_of_label ????);
     306elim (true_or_false_Prop (occurs_exactly_once ?? lbl code))
     307#Heq >Heq normalize nodelta
     308[ >lin_code_has_point @(leb_elim (S ?)) [#_ |
     309  #ABS elim(absurd ?? ABS) -ABS
     310  @index_of_label_length assumption ]] %
     311qed.
    168312
    169313record graph_params : Type[1] ≝
    170314  { g_u_pars :> unserialized_params }.
     315
     316(* move *)
     317definition lookup_safe : ∀tag,A.∀m : identifier_map tag A.∀i.i ∈ m → A ≝
     318  λtag,A,m.match m return λx : identifier_map tag A.∀i.i ∈ x → ? with
     319  [ an_id_map m' ⇒ λi.match i return λx.x ∈ an_id_map ?? m' → ? with
     320    [ an_identifier i' ⇒
     321      match lookup_opt … i' m' return λx.match x with [Some y ⇒ true | None ⇒ false] → ? with
     322      [ Some y ⇒ λ_.y
     323      | None ⇒ Ⓧ
     324      ]
     325    ]
     326  ].
     327 
     328lemma lookup_safe_elim : ∀tag,A.∀P : A → Prop.∀m,i,prf.
     329  (∀x.lookup tag A m i = Some ? x → P x) → P (lookup_safe tag A m i prf).
     330#tag #A #P *#m *#i normalize elim (lookup_opt A i m) normalize
     331[ * ]
     332#s * #H @H %
     333qed.
    171334
    172335(* One common instantiation of params via Graphs of joint_statements
     
    175338  λgp : graph_params.
    176339     mk_params
    177       (mk_stmt_params gp label (λP.P))
     340      (mk_stmt_params gp label (Some ?))
    178341    (* codeT ≝ *)(λglobals.graph (joint_statement ? globals))
    179     (* code_has_label ≝ *)(λglobals,code,lbl.lookup … code lbl ≠ None ?)
    180     (* forall_statements ≝ *)(λglobals,P,code.
    181       ∀l,s.lookup … code l = Some ? s → P s).
    182    
     342    (* code_point ≝ *)label
     343    (* stmt_at ≝ *)(λglobals,code.lookup LabelTag ? code)
     344    (* point_of_label ≝ *)(λ_.λ_.λlbl.return lbl)
     345    (* point_of_succ ≝ *)(λ_.λlbl.lbl).
     346
    183347coercion gp_to_p : ∀gp:graph_params.params ≝ graph_params_to_params
    184348on _gp : graph_params to params.
    185    
    186 
    187 definition labels_present : ∀globals.∀p : params.
    188   codeT p globals → (joint_statement p globals) → Prop ≝
    189 λglobals,p,code,s. stmt_forall_labels p globals
    190   (λl.code_has_label ?? code l) s.
     349
     350lemma graph_code_has_point : ∀gp : graph_params.∀globals.∀code:codeT gp globals.
     351  ∀pt.code_has_point … code pt = mem_set … code pt.
     352#gp#globals*#m*#i % qed.
     353
     354lemma graph_code_has_label : ∀gp : graph_params.∀globals.∀code:codeT gp globals.
     355  ∀lbl.code_has_label … code lbl = mem_set … code lbl.
     356#gp #globals * #m * #i % qed.
     357
     358definition stmt_forall_succ ≝ λp,globals.λP : succ p → Prop.
     359  λs : joint_statement p globals.
     360  match s with
     361  [ sequential _ n ⇒ P n
     362  | _ ⇒ True
     363  ].
     364
     365definition statement_closed : ∀globals.∀p : params.
     366  codeT p globals → code_point p → (joint_statement p globals) → Prop ≝
     367λglobals,p,code,pt,s.
     368  All ? (λl.bool_to_Prop (code_has_label ?? code l)) (stmt_explicit_labels … s) ∧
     369  stmt_forall_succ … (λn.bool_to_Prop (point_of_succ ? pt n ∈ code)) s.
    191370
    192371definition code_closed : ∀p : params.∀globals.
    193372  codeT p globals → Prop ≝ λp,globals,code.
    194     forall_statements … (labels_present … code) code.
     373    forall_statements_i … (statement_closed … code) code.
    195374
    196375(* CSC: special case where localsT is a list of registers (RTL and ERTL) *)
    197376definition rtl_ertl_params : ?→?→params ≝ λinst_pars,funct_pars.
    198   (mk_graph_params (mk_unserialized_params inst_pars (mk_local_params funct_pars (list register)))).
     377  (mk_graph_params (mk_unserialized_params inst_pars (mk_local_params funct_pars register))).
    199378
    200379record joint_internal_function (globals: list ident) (p:params) : Type[0] ≝
     
    206385  joint_if_result   : resultT p;
    207386  joint_if_params   : paramsT p;
    208   joint_if_locals   : localsT p;
     387  joint_if_locals   : list (localsT p); (* use void where no locals are present *)
    209388(*CSC: XXXXX stacksize unused for LTL-...*)
    210389  joint_if_stacksize: nat;
    211390  joint_if_code     : codeT p globals ;
    212 (*CSC: XXXXX entry unused for LIN, but invariant in that case... *)
    213   joint_if_entry    : Σl: label. code_has_label … joint_if_code l;
    214 (*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *)
    215   joint_if_exit     : Σl: label. code_has_label …  … joint_if_code l
     391  joint_if_entry : point_in_code … joint_if_code ;
     392  joint_if_exit : point_in_code … joint_if_code
    216393}.
    217394
     
    219396  λglobals,p.
    220397    Σdef : joint_internal_function globals p. code_closed … (joint_if_code … def).
    221 
    222 (* Currified form *)
    223 definition set_joint_if_exit ≝
    224   λglobals,pars.
    225   λexit: label.
    226   λp:joint_internal_function globals pars.
    227   λprf: code_has_label … (joint_if_code … p) exit.
    228    mk_joint_internal_function globals pars
    229     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    230     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
    231     (joint_if_code … p) (joint_if_entry … p) (mk_Sig … exit prf).
    232398
    233399definition set_joint_code ≝
     
    244410
    245411definition set_joint_if_graph ≝
    246   λglobals,pars.
     412  λglobals.λpars : graph_params.
    247413  λgraph.
    248414  λp:joint_internal_function globals pars.
    249   λentry_prf: code_has_label … graph (joint_if_entry … p).
    250   λexit_prf: code_has_label … graph (joint_if_exit … p).
     415  λentry_prf.
     416  λexit_prf.
    251417    set_joint_code globals pars p
    252418      graph
    253       (mk_Sig … (joint_if_entry … p) entry_prf)
    254       (mk_Sig … (joint_if_exit p) exit_prf).
     419      (mk_Sig ?? (joint_if_entry ?? p) entry_prf)
     420      (mk_Sig … (joint_if_exit ?? p) exit_prf).
    255421
    256422definition set_luniverse ≝
     
    272438    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
    273439   
    274 (* Paolo: probably should move these elsewhere *)
    275 definition graph_dom ≝ λX.λg : graph X.Σl : label.lookup … g l ≠ None ?.
    276 definition graph_dom_add_incl : ∀X.∀g : graph X.∀l : label.∀x : X.
    277   graph_dom ? g → graph_dom ? (add … g l x) ≝ λX,g,l,x,sig_l.
    278   mk_Sig … (pi1 ?? sig_l) ?.
    279 @graph_add_lookup
    280 @(pi2 … sig_l)
    281 qed.
    282 
    283440(* Specialized for graph_params *)
    284441definition add_graph ≝
     
    290447     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
    291448     code
    292      (graph_dom_add_incl … (joint_if_entry … p))
    293      (graph_dom_add_incl … (joint_if_exit … p)).
     449     (pi1 … (joint_if_entry … p))
     450     (pi1 … (joint_if_exit … p)).
     451>graph_code_has_point whd in match code; >mem_set_add
     452@orb_Prop_r [elim (joint_if_entry ???) | elim (joint_if_exit ???) ]
     453#x #H <graph_code_has_point @H
     454qed.
    294455
    295456definition set_locals ≝
Note: See TracChangeset for help on using the changeset viewer.