Ignore:
Timestamp:
Mar 7, 2013, 2:51:40 PM (7 years ago)
Author:
tranquil
Message:

new b_graph_translate obligations

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToERTLptr.ma

    r2696 r2806  
    8282    (* init_stack_size ≝ *) (joint_if_stacksize … def)
    8383    (* added_prologue ≝ *) [ ]
     84    (* new_regs ≝ *) [ ]
    8485    (* f_step ≝ *) (translate_step globals)
    8586    (* f_fin ≝ *) (translate_fin_step globals)
    86     ???).
     87    ????).
    8788@hide_prf
    88 [ #l #c % ]
     89[ #l * [ #c' | * #f #args #dest | #a #ltrue | #s ] #c whd
     90  [3: #r1 ] #l' #EQ destruct try %
     91  cases s in EQ; whd in match ensure_step_block; normalize nodelta
     92  try #a try #b try #c try #d try #e try #f destruct
     93| #l #c %
     94]
    8995#l *
    90 [ #l whd %{I} %{I} %1 %
    91 | whd %{I I}
    92 | #abs #called #args whd %{I I}
    93 | #c %{I} %{I} #l %
     96[ #l' whd %{I} %{I} %{I} %2 % %
     97| whd %{I} %{I I}
     98| #abs #called #args whd %{I} %{I I}
     99| #c #l' whd %{I} %{I} %{I} %
    94100| * #called #args #dest whd in match translate_step; normalize nodelta whd
    95   [ %{I} %{I} #l %
    96   | #r whd %{I} %{(λ_.I)} % [| % [| % [| %{I} ]]] #l
    97     [1,3: %{I} %1 %
    98     |*: %
    99     ]
     101  [ #l' %{I} %{I} %{I} %
     102  | #r #l' whd %{I} % [2: %{I I} ] % [2: % [2: % [2: %{I} ]]] % try @I %{I} %1 %
    100103  ]
    101 | #a #l_true whd %{I} %{I} #l %{I} %2 %1 %
    102 | #s whd %{I} %{I} #l whd @(All_mp … (In ? (step_labels … s)))
    103   [ #l' #H %2{H} ] cases s -s //
     104| #a #l_true whd #l %{I} %{I} % %{I} [ %2 ] %1 %
     105| #s whd #l %{I} %{I} whd %
     106  [ @(All_mp … (In ? (step_labels … s))) [ #l' #H %2{H} ] cases s -s // ]
     107  cut (∀X,l1,l2.l1 = l2 → All X (In X l1) l2)
     108  [ #X #l1 #l2 #EQ destruct elim l2 [ % ] #hd #tl #IH % [ %1 % ] @(All_mp … IH) #x #H %2{H} ]
     109  #aux @aux cases s //
    104110]
    105111qed.
Note: See TracChangeset for help on using the changeset viewer.