Changeset 1100 for Deliverables/D3.3/id-lookup-branch

Timestamp:

Aug 3, 2011, 5:18:15 PM (10 years ago)

Author:

campbell

Message:

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

File:

• Deliverables/D3.3/id-lookup-branch/Clight/toCminor.ma (modified) (7 diffs)

Deliverables/D3.3/id-lookup-branch/Clight/toCminor.ma

@@ -744 +744 @@
 definition lenv ≝ identifier_map SymbolTag (identifier Label).
 
-definition lpresent ≝ λlbls:lenv. λl. ∃l'. lookup ?? lbls l' = Some ? l.
+axiom MissingLabel : String.
+
+definition lookup_label ≝
+λlbls:lenv.λl. opt_to_res … [MSG MissingLabel; CTX ? l] (lookup ?? lbls l).
+
+definition lpresent ≝ λlbls:lenv. λl. ∃l'. lookup_label lbls l' = OK ? l.
 
 let rec labels_defined (s:statement) : list ident ≝
@@ -766 +771 @@
 definition ldefined ≝ λs.λl.Exists ? (λl'.l' = l) (labels_of s).
 
-axiom MissingLabel : String.
-
-definition lookup_label ≝
-λlbls:lenv.λl. opt_to_res … [MSG MissingLabel; CTX ? l] (lookup ?? lbls l).
-
 definition labels_translated : lenv → statement → stmt → Prop ≝
 λlbls,s,s'.  ∀l.
@@ -827 +827 @@
   lookup_label lbls l = OK ? l' →
   lpresent lbls l'.
-#lbls #l #l' whd in ⊢ (??%? → %) #E %{l} cases (lookup ??? l) in E ⊢ %
-normalize #x try #y destruct /2/
+#lbls #l #l' #E whd %{l} @E
 qed.
 
@@ -1082 +1081 @@
 ] qed. 
 
-definition lenv_inv : lenv → lenv → statement → Prop ≝
-λlbls0,lbls,s. (∀l. Exists ? (λl'. l' = l) (labels_defined s) → ∃lm. lookup_label lbls l = OK ? lm) ∧
-  ∀l,l'. lookup_label lbls0 l = OK ? l' → lookup_label lbls l = OK ? l'.
-
-definition lenv_inv_switch : lenv → lenv → labeled_statements → Prop ≝
-λlbls0,lbls,ls. (∀l. Exists ? (λl'. l' = l) (labels_defined_switch ls) → ∃lm. lookup_label lbls l = OK ? lm) ∧
-  ∀l,l'. lookup_label lbls0 l = OK ? l' → lookup_label lbls l = OK ? l'.
-
 axiom DuplicateLabel : String.
-(*
-(* We only record labels from Slabel, not Sgoto, so that we detect badly formed
-   programs.  The gratutitous let-in expansion is so that Russell generated
-   nice hypotheses for us. *)
-let rec extend_label_env (s:statement) (lu0:lenv×(universe ?)) : res (Σx:lenv × (universe ?). lenv_inv (\fst lu0) (\fst x) s) ≝
-match s return λs.res (Σx:lenv × (universe ?). lenv_inv (\fst lu0) (\fst x) s) with
-[ Ssequence s1 s2 ⇒ 
-    do lu1 ← extend_label_env s1 lu0;
-    do lu2 ← extend_label_env s2 lu1; OK ? «eject … lu2, ?»
-| Sifthenelse _ s1 s2 ⇒
-    do lu1 ← extend_label_env s1 lu0;
-    do lu2 ← extend_label_env s2 lu1; OK ? «eject … lu2, ?»
-| Swhile _ s ⇒ do lu ← extend_label_env s lu0; OK ? «eject … lu, ?»
-| Sdowhile _ s ⇒ do lu ← extend_label_env s lu0; OK ? «eject … lu, ?»
-| Sfor s1 _ s2 s3 ⇒
-    do lu1 ← extend_label_env s1 lu0;
-    do lu2 ← extend_label_env s2 lu1;
-    do lu3 ← extend_label_env s3 lu2; OK ? «eject … lu3, ?»
-| Sswitch _ ls ⇒ do lu ← extend_label_env' ls lu0; OK ? «eject … lu, ?»
-| Slabel l s ⇒
-    let 〈lbls, u〉 ≝ lu0 in
-    match lookup_label lbls l with
-    [ OK _ ⇒ Error ? (msg DuplicateLabel)
-    | Error _ ⇒
-        let 〈l',u〉 ≝ fresh ? u in
-        do lu ← extend_label_env s 〈add … lbls l l', u〉; OK ? «eject … lu, ?»
-    ]
-| Scost _ s ⇒ do lu ← extend_label_env s lu0; OK ? «eject … lu, ?»
-| _ ⇒ OK ? «lu0, ?»
-]
-and extend_label_env' (ls:labeled_statements) (lu0:lenv×(universe ?)) : res (Σx:lenv × (universe ?). lenv_inv_switch (\fst lu0) (\fst x) ls) ≝
-match ls return λls.res (Σx:lenv × (universe ?). lenv_inv_switch (\fst lu0) (\fst x) ls) with
-[ LSdefault s ⇒ do lu ← extend_label_env s lu0; OK ? «eject … lu, ?»
-| LScase _ _ s ls ⇒
-    do lu1 ← extend_label_env s lu0;
-    do lu2 ← extend_label_env' ls lu1; OK ? «eject … lu2, ?»
-]. @conj
-[ 1,3,5,17,19,21,27: #l *
-| 2,4,6,18,20,22,28: #l #l' #H @H
-| cases lu1 in lu2 ⊢ % * #lbls1 #u1 * #I1 #E1 * * #lbls2 #u2 * #I2 #E2 whd in E2:(∀_.∀_.??(?%?)? → ?) ⊢ (∀_.? → ??(λ_.??(?%?)?))
-  #l #H cases (Exists_append … H)
-  [ #H1 cases (I1 l H1) #l' #L1 %{l'} @E2 @L1
-  | #H2 cases (I2 l H2) #l' #L2 %{l'} @L2
-  ]
-
-definition build_label_env ≝ λbody. extend_label_env body (empty_map ??) (new_universe ?).
-*)
 
 definition lenv_list_inv : lenv → lenv → list ident → Prop ≝
-λlbls0,lbls,ls. (∀l. Exists ? (λl'. l' = l) ls → ∃lm. lookup_label lbls l = OK ? lm) ∧
-  ∀l,l'. lookup_label lbls0 l = OK ? l' → lookup_label lbls l = OK ? l'.
+λlbls0,lbls,ls.
+ ∀l,l'. lookup_label lbls l = OK ? l' →
+ Exists ? (λl'. l' = l) ls ∨ lookup_label lbls0 l = OK ? l'.
 
 lemma lookup_label_add : ∀lbls,l,l'.
@@ -1148 +1093 @@
 qed.
 
-lemma lookup_label_new : ∀lbls,l,l',msg,l0,l0'.
-  lookup_label lbls l = Error ? msg →
-  lookup_label lbls l0 = OK ? l0' →
-  lookup_label (add … lbls l l') l0 = OK ? l0'.
-#lbls #l #l' #msg #l0 #l0' #E1 #E2
+lemma lookup_label_miss : ∀lbls,l,l',l0.
+  l0 ≠ l →
+  lookup_label (add … lbls l l') l0 = lookup_label lbls l0.
+#lbls #l #l' #l0 * #NE
 whd in ⊢ (??%%)
 >lookup_add_miss
-[ @E2 | @(eq_identifier_elim ?? l0 l) // #E >E in E2 >E1 #X destruct ]
+[ @refl | @(eq_identifier_elim ?? l0 l)
+  [ #E cases (NE E)
+  | #_ @I
+  ]
+]
 qed.  
 
@@ -1169 +1117 @@
         OK ? «eject … lbls1, ?»
     ] (refl ? (lookup_label lbls l))
-]. @conj
-[  #l *
-| #l #l' #H @H
-| cases lbls1 #lbls' * #E1 #E2 whd in ⊢ (∀_.?→??(λ_.??(?%?)?)) #l0 *
-  [ #E <E %{l'} @E2 @lookup_label_add
-  | @E1
-  ]
-| cases lbls1 #lbls' * #E1 #E2 #l1 #l2 #L whd in ⊢ (??(?%?)?)
-  @E2 @(lookup_label_new … LOOK L)
-] qed.
-
-definition build_label_env : ∀body:statement. res (Σlbls:lenv. ∀l.Exists ? (λl'.l' = l) (labels_defined body) → ∃l'.lookup_label lbls l = OK ? l') ≝
-λbody.
-  do lbls ← populate_lenv (labels_defined body) (empty_map ??) (new_universe ?);
-  OK ? «eject … lbls, ?».
-cases lbls #lbls * #E1 #E2 @E1
-qed.
+].
+[ #l #l' #H %2 @H
+| cases lbls1 #lbls' #I whd in ⊢ (??%?)
+  #l1 #l1' #E1 @(eq_identifier_elim … l l1)
+  [ #E %1 %1 @E
+  | #NE cases (I l1 l1' E1)
+    [ #H %1 %2 @H
+    | #LOOK' %2 >lookup_label_miss in LOOK' /2/ #H @H
+    ]
+  ]
+] qed.
 
 notation > "vbox('do' « ident v , ident p » ← e; break e')" with precedence 40
   for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ dp ${ident v} ${ident p} ⇒ ${e'} ]) }.
+
+definition build_label_env : ∀body:statement. res (Σlbls:lenv. ∀l,l'.lookup_label lbls l = OK ? l' → Exists ? (λl'.l' = l) (labels_defined body)) ≝
+λbody.
+  do «lbls, H» ← populate_lenv (labels_defined body) (empty_map ??) (new_universe ?);
+  OK ? «lbls, ?».
+#l #l' #E cases (H l l' E) //
+whd in ⊢ (??%? → ?) #H destruct
+qed.
 
 (* FIXME: the temporary handling is nonsense, I'm afraid. *)
@@ -1226 +1176 @@
   | @(stmt_labels_mp … H2)
     #l * #l' #LOOKUP
-    
-     generalize in ⊢ (???(?(???(????%))))
-    * #S #L
+    lapply (Ilbls l' l LOOKUP) #DEFINED
+    cases (L … DEFINED) #lx * #LOOKUPx >LOOKUPx in LOOKUP #Ex destruct (Ex)
+    #H @H
+  ]
+| whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) >lookup_add_miss [ >lookup_add_hit %| % ]
 | whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) >lookup_add_hit %
-| whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) >lookup_add_miss [ >lookup_add_hit %| % ]
-
 ] qed.