Changeset 2793 for src/Cminor

Timestamp:

Mar 6, 2013, 7:23:42 PM (7 years ago)

Author:

campbell

Message:

Oops, gave fields wrong order during initialisation.

File:

• src/Cminor/initialisation.ma (modified) (1 diff)

src/Cminor/initialisation.ma

@@ -45 +45 @@
 definition init_var : ident → region → list init_data → Σs:stmt. stmt_inv s ≝
 λid,r,init.
-\snd (foldr ??
-  (λdatum,os.
+\snd (foldl ??
+  (λos,datum.
    let 〈off,s〉 ≝ os in
      〈off + (size_init_data datum), St_seq (init_datum id r datum off) s〉)
   〈0, mk_Sig ? (λx.stmt_inv x) St_skip ?〉 init).
 [ % /3/
-| elim init
-  [ % /3/
-  | #h #t #IH whd in ⊢ (?(???%)); @breakup_pair
+| cut (stmt_inv St_skip) [ % /3/ ]
+  generalize in match St_skip;
+  generalize in match 0;
+  elim init
+  [ #off #s #H @H
+  | #h #t #IH #off #s #H whd in ⊢ (?(???%)); @breakup_pair @IH
     %
     [ /3/
-    | % [ @(pi2 … (init_datum …)) | @IH ]
+    | % [ @(pi2 … (init_datum …)) | @H ]
     ]
+  ]
 ] qed.