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/Clight/toCminor.ma

    r1515 r1516  
    122122  local_id (add ?? vars id (Global r)) id' → local_id vars id'.
    123123#var #id #r #id'
    124 whd in ⊢ (% → ?) whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?] → ?)
     124whd in ⊢ (% → ?); whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?] → ?);
    125125cases (identifier_eq ? id id')
    126 [ #E >E >lookup_add_hit whd in ⊢ (% → ?) *
     126[ #E >E >lookup_add_hit whd in ⊢ (% → ?); *
    127127| #NE >lookup_add_miss /2/
    128128] qed.
     
    131131  id ≠ id' → local_id (add ?? vars id t) id' → local_id vars id'.
    132132#vars #id #t #id' #NE
    133 whd in ⊢ (% → %)
    134 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ] → match % with [ _ ⇒ ? | _ ⇒ ? ])
     133whd in ⊢ (% → %);
     134whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ] → match % with [ _ ⇒ ? | _ ⇒ ? ]);
    135135>lookup_add_miss
    136136[ #H @H | /2/ ]
     
    142142      Exists ? (λx.\fst x = i) (fn_params f @ fn_vars f).
    143143#globals #f
    144 whd in ⊢ (∀_.∀_.??%? → ?)
     144whd in ⊢ (∀_.∀_.??%? → ?);
    145145elim (fn_params f @ fn_vars f)
    146 [ #vars #n whd in ⊢ (??%? → ?) #E destruct #i #H @False_ind
    147   elim globals in H
     146[ #vars #n whd in ⊢ (??%? → ?); #E destruct #i #H @False_ind
     147  elim globals in H;
    148148  [ normalize //
    149   | * #id #rg #t #IH whd in ⊢ (?%? → ?) #H @IH @(local_id_add_global ???? H)
     149  | * #id #rg #t #IH whd in ⊢ (?%? → ?); #H @IH @(local_id_add_global ???? H)
    150150  ]
    151 | * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?) #E #i
     151| * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?); #E #i
    152152  cases (identifier_eq ? id i)
    153153  [ #E' <E' #H % @refl
    154154  | #NE #H whd %2 >(contract_pair var_types nat ?) in E;
    155     whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?)
    156     cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?)
     155    whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
     156    cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
    157157    #H' lapply (extract_pair ???????? H') -H' * #m0 * #n0 * #EQ #EQ2
    158158    @(IH m0 n0)
    159     [ 1,3: @sym_eq whd in ⊢ (???(match ?????% with [ _ ⇒ ? ])) >contract_pair @EQ
     159    [ 1,3: @sym_eq whd in ⊢ (???(match ?????% with [ _ ⇒ ? ])); >contract_pair @EQ
    160160    | 2,4: destruct (EQ2) @(local_id_add_miss … H) @NE
    161161    ]
     
    348348  expr_vars ? e P.
    349349#P * #ty1 #e1 #ty2 #e2 #ty #e #H1 #H2
    350 whd in ⊢ (??%? → ?)
     350whd in ⊢ (??%? → ?);
    351351[ cases (classify_add ty1 ty2)
    352   [ 3,4: #z ] whd in ⊢ (??%? → ?)
    353   [ generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
     352  [ 3,4: #z ] whd in ⊢ (??%? → ?);
     353  [ generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?);
    354354    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
    355355    whd in c:(??%?); destruct % [ @H1 | % // @H2 ]
    356   | generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
     356  | generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?);
    357357    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
    358358    whd in c:(??%?); destruct % [ @H2 | % // @H1 ]
     
    360360  ]
    361361| cases (classify_sub ty1 ty2)
    362   [ 3,4: #z] whd in ⊢ (??%? → ?)
    363   [ 2: generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
     362  [ 3,4: #z] whd in ⊢ (??%? → ?);
     363  [ 2: generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?);
    364364    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
    365365    whd in c:(??%?); destruct % [ % try @H1 @H2 ] @I
     
    737737  〈tmp,u'〉 = alloc_tmp q u → tmps_preserved vars u u'.
    738738#tmp #g #g' #vars #q
    739 whd in ⊢ (???% → ?) #E
     739whd in ⊢ (???% → ?); #E
    740740#id #H
    741741cases (identifier_eq ? id tmp)
    742742destruct #E
    743 whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]
     743whd in ⊢ (?%?); whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ];
    744744[ >E >lookup_add_hit @I
    745745| cases E #NE >lookup_add_miss [ @H | /2/
     
    765765lemma local_id_add_local_oblivious : ∀vars,id,id'.
    766766  local_id vars id → local_id (add ?? vars id' Local) id.
    767 #vars #id #id' #H whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
     767#vars #id #id' #H whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
    768768cases (identifier_eq ? id id')
    769769[ #E >E >lookup_add_hit @I
     
    791791  〈tmp,u〉 = alloc_tmp q u0 → local_id (add_tmps vars u) tmp.
    792792#tmp #u #q #u0 #vars
    793 whd in ⊢ (???% → ?) #E
     793whd in ⊢ (???% → ?); #E
    794794destruct
    795 whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ] >lookup_add_hit
     795whd in ⊢ (?%?); whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]; >lookup_add_hit
    796796@I
    797797qed.
     
    987987lemma lookup_label_add : ∀lbls,l,l'.
    988988  lookup_label (add … lbls l l') l = OK ? l'.
    989 #lbls #l #l' whd in ⊢ (??%?) >lookup_add_hit @refl
     989#lbls #l #l' whd in ⊢ (??%?); >lookup_add_hit @refl
    990990qed.
    991991
     
    994994  lookup_label (add … lbls l l') l0 = lookup_label lbls l0.
    995995#lbls #l #l' #l0 #NE
    996 whd in ⊢ (??%%)
     996whd in ⊢ (??%%);
    997997>lookup_add_miss
    998998[ @refl | @NE ]
     
    10121012].
    10131013[ #l #l' #H %2 @H
    1014 | cases lbls1 #lbls' #I whd in ⊢ (??%?)
     1014| cases lbls1 #lbls' #I whd in ⊢ (??%?);
    10151015  #l1 #l1' #E1 @(eq_identifier_elim … l l1)
    10161016  [ #E %1 %1 @E
    10171017  | #NE cases (I l1 l1' E1)
    10181018    [ #H %1 %2 @H
    1019     | #LOOK' %2 >lookup_label_miss in LOOK' /2/ #H @H
     1019    | #LOOK' %2 >lookup_label_miss in LOOK'; /2/ #H @H
    10201020    ]
    10211021  ]
     
    10271027  OK ? «lbls, ?».
    10281028#l #l' #E cases (H l l' E) //
    1029 whd in ⊢ (??%? → ?) #H destruct
     1029whd in ⊢ (??%? → ?); #H destruct
    10301030qed.
    10311031
     
    10341034  local_id vars i ∨ Exists ? (λx.\fst x = i) (tmp_env tmpgen).
    10351035#vars #tmpgen #i
    1036 whd in ⊢ (?%? → ?)
     1036whd in ⊢ (?%? → ?);
    10371037elim (tmp_env tmpgen)
    10381038[ #H %1 @H
     
    10861086  #l * #l' #LOOKUP
    10871087  lapply (Ilbls l' l LOOKUP) #DEFINED
    1088   cases (L … DEFINED) #lx * #LOOKUPx >LOOKUPx in LOOKUP #Ex destruct (Ex)
     1088  cases (L … DEFINED) #lx * #LOOKUPx >LOOKUPx in LOOKUP; #Ex destruct (Ex)
    10891089  #H @H
    10901090] qed.
Note: See TracChangeset for help on using the changeset viewer.