Ignore:
Timestamp:
Nov 19, 2011, 12:38:20 AM (8 years ago)
Author:
sacerdot
Message:

Ported to syntax of Matita 0.99.1.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r1515 r1516  
    2323[ #e #u #l' #e' #u' #E whd in E:(??%?); #i destruct (E) *
    2424| * #id #t #tl #IH #e #u #l' #e' #u' #E #i whd in E:(??%?) ⊢ (% → ?);
    25   * [ whd in ⊢ (??%? → ?) #E1 <E1
    26       generalize in E:(??(match % with [ _ ⇒ ? ])?) ⊢ ? * * #x #y #z
    27       whd in ⊢ (??%? → ?) elim (fresh RegisterTag z) #r #gen' #E
     25  * [ whd in ⊢ (??%? → ?); #E1 <E1
     26      generalize in E:(??(match % with [ _ ⇒ ? ])?) ⊢ ?; * * #x #y #z
     27      whd in ⊢ (??%? → ?); elim (fresh RegisterTag z) #r #gen' #E
    2828      whd in E:(??%?); destruct;
    2929      whd >lookup_add_hit % #A destruct
    30     | #H change in E:(??(match % with [ _ ⇒ ? ])?) with (populate_env e u tl)
     30    | #H change in E:(??(match % with [ _ ⇒ ? ])?); with (populate_env e u tl)
    3131      lapply (refl ? (populate_env e u tl))
    32       cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?) (* XXX if I do this directly it rewrites both sides of the equality *)
    33       * #rs #e1 #u1 #E1 >E1 in E; whd in ⊢ (??%? → ?) cases (fresh RegisterTag u1) #r #u''
    34       whd in ⊢ (??%? → ?) #E destruct
     32      cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); (* XXX if I do this directly it rewrites both sides of the equality *)
     33      * #rs #e1 #u1 #E1 >E1 in E; whd in ⊢ (??%? → ?); cases (fresh RegisterTag u1) #r #u''
     34      whd in ⊢ (??%? → ?); #E destruct
    3535      @lookup_add_oblivious
    3636      @(IH … E1 ? H)
     
    4444[ #e #u #l' #e' #u' #E whd in E:(??%?); destruct //
    4545| * #id #t #tl #IH #e #u #l' #e' #u' #E whd in E:(??%?);
    46   change in E:(??(match % with [ _ ⇒ ?])?) with (populate_env e u tl)
     46  change in E:(??(match % with [ _ ⇒ ?])?); with (populate_env e u tl)
    4747  lapply (refl ? (populate_env e u tl))
    48   cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?) * #l0 #e0 #u0 #E0
    49   >E0 in E; whd in ⊢ (??%? → ?) #E
     48  cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); * #l0 #e0 #u0 #E0
     49  >E0 in E; whd in ⊢ (??%? → ?); #E
    5050  destruct
    5151  #i #H @lookup_add_oblivious @(IH … E0) @H
     
    6464#ls elim ls
    6565[ #lbls #u #lbls' #u' #E #l *
    66 | #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?)
    67   change in ⊢ (??match % with [ _ ⇒ ? ]? → ?) with (populate_label_env ???)
     66| #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?);
     67  change in ⊢ (??match % with [ _ ⇒ ? ]? → ?); with (populate_label_env ???)
    6868  lapply (refl ? (populate_label_env lbls u t))
    69   cases (populate_label_env lbls u t) in ⊢ (???% → %)
    70   #lbls1 #u1 #E1 whd in ⊢ (??%? → ?)
     69  cases (populate_label_env lbls u t) in ⊢ (???% → %);
     70  #lbls1 #u1 #E1 whd in ⊢ (??%? → ?);
    7171  #E destruct
    7272  #l *
     
    8181#ls elim ls
    8282[ #lbls #u #lbls' #u' #E #l #H %2 whd in E:(??%?); destruct @H
    83 | #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?)
    84   change in ⊢ (??match % with [ _ ⇒ ? ]? → ?) with (populate_label_env ???)
     83| #h #t #IH #lbls #u #lbls' #u' whd in ⊢ (??%? → ?);
     84  change in ⊢ (??match % with [ _ ⇒ ? ]? → ?); with (populate_label_env ???)
    8585  lapply (refl ? (populate_label_env lbls u t))
    86   cases (populate_label_env lbls u t) in ⊢ (???% → %)
    87   #lbls1 #u1 #E1 whd in ⊢ (??%? → ?) 
     86  cases (populate_label_env lbls u t) in ⊢ (???% → %);
     87  #lbls1 #u1 #E1 whd in ⊢ (??%? → ?);
    8888  #E destruct
    8989  #l #H cases (identifier_eq ? l h)
    9090  [ #El %1 %1 @El
    9191  | #NE cases (IH … E1 l ?)
    92     [ #H' %1 %2 @H' | #H' %2 @H' | whd in H >lookup_add_miss in H //  ]
     92    [ #H' %1 %2 @H' | #H' %2 @H' | whd in H; >lookup_add_miss in H; //  ]
    9393  ]
    9494] qed.
     
    149149#le #l #s #f #p
    150150#l' #s' #H cases (identifier_eq … l l')
    151 [ #E >E in H >lookup_add_hit #E' <(?:s = s') [2:destruct //]
     151[ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //]
    152152  @(labels_P_mp … p) #l0 #H %1 @lookup_add_oblivious @H
    153153| #NE @(labels_P_mp … (pf_closed ? f l' s' ?))
    154154  [ #lx * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
    155   | >lookup_add_miss in H /2/
     155  | >lookup_add_miss in H; /2/
    156156  ]
    157157] qed.
     
    205205#le #l #s #f #p
    206206#l' #s' #H cases (identifier_eq … l l')
    207 [ #E >E in H >lookup_add_hit #E' <(?:s = s') [2:destruct //]
     207[ #E >E in H; >lookup_add_hit #E' <(?:s = s') [2:destruct //]
    208208  @(labels_P_mp … p) #l0 * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
    209209| #NE @(labels_P_mp … (pf_closed ? f l' s' ?))
    210210  [ #lx * [ #H %1 @lookup_add_oblivious @H | #H %2 @H ]
    211   | >lookup_add_miss in H /2/
     211  | >lookup_add_miss in H; /2/
    212212  ]
    213213] qed.
     
    273273#le #env #es #f elim es
    274274[ #p #rs #f normalize #E destruct @refl
    275 | * #ty #e #t #IH #p #rs #f' whd in ⊢ (??%? → ??%?) #E
     275| * #ty #e #t #IH #p #rs #f' whd in ⊢ (??%? → ??%?); #E
    276276  cases (extract_pair ???????? E) #rs' * #f'' * #E1 #E2 -E;
    277277  cases (extract_pair ???????? E2) #r * #f3 * #E3 #E4 -E2;
     
    453453#lenv #l #l' #p
    454454cut (∃lx. lookup ?? lenv l = Some ? lx)
    455 [ whd in p; cases (lookup ?? lenv l) in p ⊢ %
     455[ whd in p; cases (lookup ?? lenv l) in p ⊢ %;
    456456  [ * #H cases (H (refl ??))
    457457  | #lx #_ %{lx} @refl
    458458  ]
    459 | * #lx #E whd in ⊢ (??%? → ?) cases p >E #q whd in ⊢ (??%? → ?) #E' >E' @refl
     459| * #lx #E whd in ⊢ (??%? → ?); cases p >E #q whd in ⊢ (??%? → ?); #E' >E' @refl
    460460] qed.
    461461
     
    478478  labels_of s = labels_of s' → Cminor_labels_added le s' f →
    479479  Cminor_labels_added le s f.
    480 #le #s #s' #f #E whd in ⊢ (% → %) > E #H @H
     480#le #s #s' #f #E whd in ⊢ (% → %); > E #H @H
    481481qed.
    482482
     
    621621try (#l #H @H)
    622622[ -f @(choose_regs_length … (sym_eq … Eregs))
    623 | whd in Env @(π1 (π1 (π1 Env)))
     623| whd in Env; @(π1 (π1 (π1 Env)))
    624624| -f @(choose_regs_length … (sym_eq … Eregs))
    625625| #l #H cases (Exists_append … H)
     
    709709  | cases (label_env_contents … (sym_eq ??? El) l ?)
    710710    [ #H @H
    711     | whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?) * #H cases (H (refl ??))
     711    | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); * #H cases (H (refl ??))
    712712    | whd >H % #E' destruct (E')
    713713    ]
     
    716716| #l1 #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
    717717  [ * #E1 #E2 >E2 @I
    718   | whd in ⊢ (??%? → ?) #E' destruct (E')
     718  | whd in ⊢ (??%? → ?); #E' destruct (E')
    719719  ]
    720720| *: whd >lookup_add_hit % #E destruct
Note: See TracChangeset for help on using the changeset viewer.