Changeset 1095 for Deliverables/D3.3/id-lookup-branch/Cminor/toRTLabs.ma

Timestamp:

Aug 3, 2011, 1:04:45 PM (10 years ago)

Author:

campbell

Message:

Make add_exprs total (on branch).

File:

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

Deliverables/D3.3/id-lookup-branch/Cminor/toRTLabs.ma

@@ -126 +126 @@
 definition exprtyp_present ≝ λenv:env.λe:Σt:typ.expr t.match e with [ dp ty e ⇒ expr_vars ty e (present ?? env) ].
 
-definition choose_regs : ∀env:env. ∀es:list (Σt:typ.expr t). internal_function → All ? (exprtyp_present env) es → list register × internal_function ≝
+definition choose_regs : ∀env:env. ∀es:list (Σt:typ.expr t).
+                         internal_function → All ? (exprtyp_present env) es →
+                         list register × internal_function ≝
 λenv,es,f,Env.
   foldr_all (Σt:typ.expr t) ??
@@ -133 +135 @@
              〈r::rs,f'〉) 〈[ ], f〉 es Env.
 @p qed.
+
+lemma extract_pair : ∀A,B,C,D.  ∀u:A×B. ∀Q:A → B → C×D. ∀x,y.
+((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) →
+∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉.
+#A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed.
+
+
+lemma choose_regs_length : ∀env,es,f,p,rs,f'.
+  choose_regs env es f p = 〈rs,f'〉 → |es| = |rs|.
+#env #es #f elim es
+[ #p #rs #f normalize #E destruct @refl
+| * #ty #e #t #IH #p #rs #f' whd in ⊢ (??%? → ??%?) #E
+  cases (extract_pair ???????? E) #rs' * #f'' * #E1 #E2 -E;
+  cases (extract_pair ???????? E2) #r * #f3 * #E3 #E4 -E2;
+  destruct (E4) skip (E1 E3) @eq_f @IH
+  [ @(proj2 … p)
+  | 3: @sym_eq @E1
+  | 2: skip
+  ]
+] qed.
 
 axiom BadCminorProgram : String.
@@ -173 +195 @@
 ] Env.
 
-(* This shouldn't occur; maybe use vectors? *)
-axiom WrongNumberOfArguments : String.
-
-let rec add_exprs (env:env) (es:list (Σt:typ.expr t)) (Env:All ? (exprtyp_present env) es) (dsts:list register) (f:internal_function) on es: res internal_function ≝
-match es return λes.All ?? es → ? with
-[ nil ⇒ λ_. match dsts with [ nil ⇒ OK ? f | cons _ _ ⇒ Error ? (msg WrongNumberOfArguments) ]
+let rec add_exprs (env:env) (es:list (Σt:typ.expr t)) (Env:All ? (exprtyp_present env) es)
+                  (dsts:list register) (pf:|es|=|dsts|) (f:internal_function) on es: internal_function ≝
+match es return λes.All ?? es → |es|=|dsts| → ? with
+[ nil ⇒ λ_. match dsts return λx. ?=|x| → ? with [ nil ⇒ λ_. f | cons _ _ ⇒ λpf.⊥ ]
 | cons e et ⇒ λEnv.
-    match dsts with
-    [ nil ⇒ Error ? (msg WrongNumberOfArguments)
-    | cons r rt ⇒
-        do f ← add_exprs env et ? rt f;
-        match e return λe.? → ? with [ dp ty e ⇒ λEnv. OK ? (add_expr env ty e ? r f) ] (proj1 ?? Env)
+    match dsts return λx. ?=|x| → ? with
+    [ nil ⇒ λpf.⊥
+    | cons r rt ⇒ λpf.
+        let f ≝ add_exprs env et ? rt ? f in
+        match e return λe.? → ? with [ dp ty e ⇒ λEnv. add_expr env ty e ? r f ] (proj1 ?? Env)
     ]
-] Env.
-whd in Env
-[ @(proj2 … Env) | @Env ] qed.
+] Env pf.
+[ 1,2,3: normalize in pf; destruct //
+| whd in Env @(proj2 … Env)
+| normalize in pf; destruct @e0 ] qed.
 
 axiom UnknownLabel : String.
 axiom ReturnMismatch : String.
+
+notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)"
+ with precedence 10
+for @{ match $t return λx.x = $t → ? with [ pair ${ident x} ${ident y} ⇒
+        λ${ident E}.$s ] (refl ? $t) }.
 
 let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_vars s (present ?? env)) (exits:list label) (f:internal_function) on s : res internal_function ≝
@@ -211 +237 @@
       | Some id ⇒ λEnv. Some ? (lookup' env id ?)
       ] Env in
-    let 〈args_regs, f〉 ≝ choose_regs env args f (proj2 … Env) in
+    let 〈args_regs, f〉 as Eregs ≝ choose_regs env args f (proj2 … Env) in
     let f ≝
       match e with
@@ -220 +246 @@
         add_expr env ? e (proj2 … (proj1 … Env)) fnr f
       ] in
-    add_exprs env args (proj2 … Env) args_regs f
+    OK ? (add_exprs env args (proj2 … Env) args_regs ? f)
 | St_tailcall e args ⇒ λEnv.
-    let 〈args_regs, f〉 ≝ choose_regs env args f (proj2 … Env) in
+    let 〈args_regs, f〉 as Eregs ≝ choose_regs env args f (proj2 … Env) in
     let f ≝
       match e with
@@ -231 +257 @@
         add_expr env ? e (proj1 … Env) fnr f
       ] in
-    add_exprs env args (proj2 … Env) args_regs f
+    OK ? (add_exprs env args (proj2 … Env) args_regs ? f)
 | St_seq s1 s2 ⇒ λEnv.
     do f ← add_stmt env label_env s2 (proj2 … Env) exits f;
@@ -289 +315 @@
     OK ? (add_fresh_to_graph (St_cost l) f)
 ] Env.
-[ whd in Env @(proj1 … (proj1 … Env))
+[ -f @(choose_regs_length … (sym_eq … Eregs))
+| whd in Env @(proj1 … (proj1 … Env))
+| -f @(choose_regs_length … (sym_eq … Eregs))
 | @(λ_. St_skip l_next)
 | @(St_skip (f_entry f))