Changeset 1100


Ignore:
Timestamp:
Aug 3, 2011, 5:18:15 PM (8 years ago)
Author:
campbell
Message:

Finally show that labels in generated Cminor programs are properly defined
on branch.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch/Clight/toCminor.ma

    r1097 r1100  
    744744definition lenv ≝ identifier_map SymbolTag (identifier Label).
    745745
    746 definition lpresent ≝ λlbls:lenv. λl. ∃l'. lookup ?? lbls l' = Some ? l.
     746axiom MissingLabel : String.
     747
     748definition lookup_label ≝
     749λlbls:lenv.λl. opt_to_res … [MSG MissingLabel; CTX ? l] (lookup ?? lbls l).
     750
     751definition lpresent ≝ λlbls:lenv. λl. ∃l'. lookup_label lbls l' = OK ? l.
    747752
    748753let rec labels_defined (s:statement) : list ident ≝
     
    766771definition ldefined ≝ λs.λl.Exists ? (λl'.l' = l) (labels_of s).
    767772
    768 axiom MissingLabel : String.
    769 
    770 definition lookup_label ≝
    771 λlbls:lenv.λl. opt_to_res … [MSG MissingLabel; CTX ? l] (lookup ?? lbls l).
    772 
    773773definition labels_translated : lenv → statement → stmt → Prop ≝
    774774λlbls,s,s'.  ∀l.
     
    827827  lookup_label lbls l = OK ? l' →
    828828  lpresent lbls l'.
    829 #lbls #l #l' whd in ⊢ (??%? → %) #E %{l} cases (lookup ??? l) in E ⊢ %
    830 normalize #x try #y destruct /2/
     829#lbls #l #l' #E whd %{l} @E
    831830qed.
    832831
     
    10821081] qed.
    10831082
    1084 definition lenv_inv : lenv → lenv → statement → Prop ≝
    1085 λlbls0,lbls,s. (∀l. Exists ? (λl'. l' = l) (labels_defined s) → ∃lm. lookup_label lbls l = OK ? lm) ∧
    1086   ∀l,l'. lookup_label lbls0 l = OK ? l' → lookup_label lbls l = OK ? l'.
    1087 
    1088 definition lenv_inv_switch : lenv → lenv → labeled_statements → Prop ≝
    1089 λlbls0,lbls,ls. (∀l. Exists ? (λl'. l' = l) (labels_defined_switch ls) → ∃lm. lookup_label lbls l = OK ? lm) ∧
    1090   ∀l,l'. lookup_label lbls0 l = OK ? l' → lookup_label lbls l = OK ? l'.
    1091 
    10921083axiom DuplicateLabel : String.
    1093 (*
    1094 (* We only record labels from Slabel, not Sgoto, so that we detect badly formed
    1095    programs.  The gratutitous let-in expansion is so that Russell generated
    1096    nice hypotheses for us. *)
    1097 let rec extend_label_env (s:statement) (lu0:lenv×(universe ?)) : res (Σx:lenv × (universe ?). lenv_inv (\fst lu0) (\fst x) s) ≝
    1098 match s return λs.res (Σx:lenv × (universe ?). lenv_inv (\fst lu0) (\fst x) s) with
    1099 [ Ssequence s1 s2 ⇒
    1100     do lu1 ← extend_label_env s1 lu0;
    1101     do lu2 ← extend_label_env s2 lu1; OK ? «eject … lu2, ?»
    1102 | Sifthenelse _ s1 s2 ⇒
    1103     do lu1 ← extend_label_env s1 lu0;
    1104     do lu2 ← extend_label_env s2 lu1; OK ? «eject … lu2, ?»
    1105 | Swhile _ s ⇒ do lu ← extend_label_env s lu0; OK ? «eject … lu, ?»
    1106 | Sdowhile _ s ⇒ do lu ← extend_label_env s lu0; OK ? «eject … lu, ?»
    1107 | Sfor s1 _ s2 s3 ⇒
    1108     do lu1 ← extend_label_env s1 lu0;
    1109     do lu2 ← extend_label_env s2 lu1;
    1110     do lu3 ← extend_label_env s3 lu2; OK ? «eject … lu3, ?»
    1111 | Sswitch _ ls ⇒ do lu ← extend_label_env' ls lu0; OK ? «eject … lu, ?»
    1112 | Slabel l s ⇒
    1113     let 〈lbls, u〉 ≝ lu0 in
    1114     match lookup_label lbls l with
    1115     [ OK _ ⇒ Error ? (msg DuplicateLabel)
    1116     | Error _ ⇒
    1117         let 〈l',u〉 ≝ fresh ? u in
    1118         do lu ← extend_label_env s 〈add … lbls l l', u〉; OK ? «eject … lu, ?»
    1119     ]
    1120 | Scost _ s ⇒ do lu ← extend_label_env s lu0; OK ? «eject … lu, ?»
    1121 | _ ⇒ OK ? «lu0, ?»
    1122 ]
    1123 and extend_label_env' (ls:labeled_statements) (lu0:lenv×(universe ?)) : res (Σx:lenv × (universe ?). lenv_inv_switch (\fst lu0) (\fst x) ls) ≝
    1124 match ls return λls.res (Σx:lenv × (universe ?). lenv_inv_switch (\fst lu0) (\fst x) ls) with
    1125 [ LSdefault s ⇒ do lu ← extend_label_env s lu0; OK ? «eject … lu, ?»
    1126 | LScase _ _ s ls ⇒
    1127     do lu1 ← extend_label_env s lu0;
    1128     do lu2 ← extend_label_env' ls lu1; OK ? «eject … lu2, ?»
    1129 ]. @conj
    1130 [ 1,3,5,17,19,21,27: #l *
    1131 | 2,4,6,18,20,22,28: #l #l' #H @H
    1132 | cases lu1 in lu2 ⊢ % * #lbls1 #u1 * #I1 #E1 * * #lbls2 #u2 * #I2 #E2 whd in E2:(∀_.∀_.??(?%?)? → ?) ⊢ (∀_.? → ??(λ_.??(?%?)?))
    1133   #l #H cases (Exists_append … H)
    1134   [ #H1 cases (I1 l H1) #l' #L1 %{l'} @E2 @L1
    1135   | #H2 cases (I2 l H2) #l' #L2 %{l'} @L2
    1136   ]
    1137 
    1138 definition build_label_env ≝ λbody. extend_label_env body (empty_map ??) (new_universe ?).
    1139 *)
    11401084
    11411085definition lenv_list_inv : lenv → lenv → list ident → Prop ≝
    1142 λlbls0,lbls,ls. (∀l. Exists ? (λl'. l' = l) ls → ∃lm. lookup_label lbls l = OK ? lm) ∧
    1143   ∀l,l'. lookup_label lbls0 l = OK ? l' → lookup_label lbls l = OK ? l'.
     1086λlbls0,lbls,ls.
     1087 ∀l,l'. lookup_label lbls l = OK ? l' →
     1088 Exists ? (λl'. l' = l) ls ∨ lookup_label lbls0 l = OK ? l'.
    11441089
    11451090lemma lookup_label_add : ∀lbls,l,l'.
     
    11481093qed.
    11491094
    1150 lemma lookup_label_new : ∀lbls,l,l',msg,l0,l0'.
    1151   lookup_label lbls l = Error ? msg →
    1152   lookup_label lbls l0 = OK ? l0' →
    1153   lookup_label (add … lbls l l') l0 = OK ? l0'.
    1154 #lbls #l #l' #msg #l0 #l0' #E1 #E2
     1095lemma lookup_label_miss : ∀lbls,l,l',l0.
     1096  l0 ≠ l →
     1097  lookup_label (add … lbls l l') l0 = lookup_label lbls l0.
     1098#lbls #l #l' #l0 * #NE
    11551099whd in ⊢ (??%%)
    11561100>lookup_add_miss
    1157 [ @E2 | @(eq_identifier_elim ?? l0 l) // #E >E in E2 >E1 #X destruct ]
     1101[ @refl | @(eq_identifier_elim ?? l0 l)
     1102  [ #E cases (NE E)
     1103  | #_ @I
     1104  ]
     1105]
    11581106qed. 
    11591107
     
    11691117        OK ? «eject … lbls1, ?»
    11701118    ] (refl ? (lookup_label lbls l))
    1171 ]. @conj
    1172 [  #l *
    1173 | #l #l' #H @H
    1174 | cases lbls1 #lbls' * #E1 #E2 whd in ⊢ (∀_.?→??(λ_.??(?%?)?)) #l0 *
    1175   [ #E <E %{l'} @E2 @lookup_label_add
    1176   | @E1
    1177   ]
    1178 | cases lbls1 #lbls' * #E1 #E2 #l1 #l2 #L whd in ⊢ (??(?%?)?)
    1179   @E2 @(lookup_label_new … LOOK L)
    1180 ] qed.
    1181 
    1182 definition build_label_env : ∀body:statement. res (Σlbls:lenv. ∀l.Exists ? (λl'.l' = l) (labels_defined body) → ∃l'.lookup_label lbls l = OK ? l') ≝
    1183 λbody.
    1184   do lbls ← populate_lenv (labels_defined body) (empty_map ??) (new_universe ?);
    1185   OK ? «eject … lbls, ?».
    1186 cases lbls #lbls * #E1 #E2 @E1
    1187 qed.
     1119].
     1120[ #l #l' #H %2 @H
     1121| cases lbls1 #lbls' #I whd in ⊢ (??%?)
     1122  #l1 #l1' #E1 @(eq_identifier_elim … l l1)
     1123  [ #E %1 %1 @E
     1124  | #NE cases (I l1 l1' E1)
     1125    [ #H %1 %2 @H
     1126    | #LOOK' %2 >lookup_label_miss in LOOK' /2/ #H @H
     1127    ]
     1128  ]
     1129] qed.
    11881130
    11891131notation > "vbox('do' « ident v , ident p » ← e; break e')" with precedence 40
    11901132  for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ dp ${ident v} ${ident p} ⇒ ${e'} ]) }.
     1133
     1134definition build_label_env : ∀body:statement. res (Σlbls:lenv. ∀l,l'.lookup_label lbls l = OK ? l' → Exists ? (λl'.l' = l) (labels_defined body)) ≝
     1135λbody.
     1136  do «lbls, H» ← populate_lenv (labels_defined body) (empty_map ??) (new_universe ?);
     1137  OK ? «lbls, ?».
     1138#l #l' #E cases (H l l' E) //
     1139whd in ⊢ (??%? → ?) #H destruct
     1140qed.
    11911141
    11921142(* FIXME: the temporary handling is nonsense, I'm afraid. *)
     
    12261176  | @(stmt_labels_mp … H2)
    12271177    #l * #l' #LOOKUP
    1228    
    1229      generalize in ⊢ (???(?(???(????%))))
    1230     * #S #L
     1178    lapply (Ilbls l' l LOOKUP) #DEFINED
     1179    cases (L … DEFINED) #lx * #LOOKUPx >LOOKUPx in LOOKUP #Ex destruct (Ex)
     1180    #H @H
     1181  ]
     1182| whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) >lookup_add_miss [ >lookup_add_hit %| % ]
    12311183| whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) >lookup_add_hit %
    1232 | whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) >lookup_add_miss [ >lookup_add_hit %| % ]
    1233 
    12341184] qed.
    12351185
Note: See TracChangeset for help on using the changeset viewer.