Changeset 1095


Ignore:
Timestamp:
Aug 3, 2011, 1:04:45 PM (8 years ago)
Author:
campbell
Message:

Make add_exprs total (on branch).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch/Cminor/toRTLabs.ma

    r1087 r1095  
    126126definition exprtyp_present ≝ λenv:env.λe:Σt:typ.expr t.match e with [ dp ty e ⇒ expr_vars ty e (present ?? env) ].
    127127
    128 definition choose_regs : ∀env:env. ∀es:list (Σt:typ.expr t). internal_function → All ? (exprtyp_present env) es → list register × internal_function ≝
     128definition choose_regs : ∀env:env. ∀es:list (Σt:typ.expr t).
     129                         internal_function → All ? (exprtyp_present env) es →
     130                         list register × internal_function ≝
    129131λenv,es,f,Env.
    130132  foldr_all (Σt:typ.expr t) ??
     
    133135             〈r::rs,f'〉) 〈[ ], f〉 es Env.
    134136@p qed.
     137
     138lemma extract_pair : ∀A,B,C,D.  ∀u:A×B. ∀Q:A → B → C×D. ∀x,y.
     139((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) →
     140∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉.
     141#A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed.
     142
     143
     144lemma choose_regs_length : ∀env,es,f,p,rs,f'.
     145  choose_regs env es f p = 〈rs,f'〉 → |es| = |rs|.
     146#env #es #f elim es
     147[ #p #rs #f normalize #E destruct @refl
     148| * #ty #e #t #IH #p #rs #f' whd in ⊢ (??%? → ??%?) #E
     149  cases (extract_pair ???????? E) #rs' * #f'' * #E1 #E2 -E;
     150  cases (extract_pair ???????? E2) #r * #f3 * #E3 #E4 -E2;
     151  destruct (E4) skip (E1 E3) @eq_f @IH
     152  [ @(proj2 … p)
     153  | 3: @sym_eq @E1
     154  | 2: skip
     155  ]
     156] qed.
    135157
    136158axiom BadCminorProgram : String.
     
    173195] Env.
    174196
    175 (* This shouldn't occur; maybe use vectors? *)
    176 axiom WrongNumberOfArguments : String.
    177 
    178 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 ≝
    179 match es return λes.All ?? es → ? with
    180 [ nil ⇒ λ_. match dsts with [ nil ⇒ OK ? f | cons _ _ ⇒ Error ? (msg WrongNumberOfArguments) ]
     197let rec add_exprs (env:env) (es:list (Σt:typ.expr t)) (Env:All ? (exprtyp_present env) es)
     198                  (dsts:list register) (pf:|es|=|dsts|) (f:internal_function) on es: internal_function ≝
     199match es return λes.All ?? es → |es|=|dsts| → ? with
     200[ nil ⇒ λ_. match dsts return λx. ?=|x| → ? with [ nil ⇒ λ_. f | cons _ _ ⇒ λpf.⊥ ]
    181201| cons e et ⇒ λEnv.
    182     match dsts with
    183     [ nil ⇒ Error ? (msg WrongNumberOfArguments)
    184     | cons r rt ⇒
    185         do f ← add_exprs env et ? rt f;
    186         match e return λe.? → ? with [ dp ty e ⇒ λEnv. OK ? (add_expr env ty e ? r f) ] (proj1 ?? Env)
     202    match dsts return λx. ?=|x| → ? with
     203    [ nil ⇒ λpf.⊥
     204    | cons r rt ⇒ λpf.
     205        let f ≝ add_exprs env et ? rt ? f in
     206        match e return λe.? → ? with [ dp ty e ⇒ λEnv. add_expr env ty e ? r f ] (proj1 ?? Env)
    187207    ]
    188 ] Env.
    189 whd in Env
    190 [ @(proj2 … Env) | @Env ] qed.
     208] Env pf.
     209[ 1,2,3: normalize in pf; destruct //
     210| whd in Env @(proj2 … Env)
     211| normalize in pf; destruct @e0 ] qed.
    191212
    192213axiom UnknownLabel : String.
    193214axiom ReturnMismatch : String.
     215
     216notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)"
     217 with precedence 10
     218for @{ match $t return λx.x = $t → ? with [ pair ${ident x} ${ident y} ⇒
     219        λ${ident E}.$s ] (refl ? $t) }.
    194220
    195221let 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 ≝
     
    211237      | Some id ⇒ λEnv. Some ? (lookup' env id ?)
    212238      ] Env in
    213     let 〈args_regs, f〉 ≝ choose_regs env args f (proj2 … Env) in
     239    let 〈args_regs, f〉 as Eregs ≝ choose_regs env args f (proj2 … Env) in
    214240    let f ≝
    215241      match e with
     
    220246        add_expr env ? e (proj2 … (proj1 … Env)) fnr f
    221247      ] in
    222     add_exprs env args (proj2 … Env) args_regs f
     248    OK ? (add_exprs env args (proj2 … Env) args_regs ? f)
    223249| St_tailcall e args ⇒ λEnv.
    224     let 〈args_regs, f〉 ≝ choose_regs env args f (proj2 … Env) in
     250    let 〈args_regs, f〉 as Eregs ≝ choose_regs env args f (proj2 … Env) in
    225251    let f ≝
    226252      match e with
     
    231257        add_expr env ? e (proj1 … Env) fnr f
    232258      ] in
    233     add_exprs env args (proj2 … Env) args_regs f
     259    OK ? (add_exprs env args (proj2 … Env) args_regs ? f)
    234260| St_seq s1 s2 ⇒ λEnv.
    235261    do f ← add_stmt env label_env s2 (proj2 … Env) exits f;
     
    289315    OK ? (add_fresh_to_graph (St_cost l) f)
    290316] Env.
    291 [ whd in Env @(proj1 … (proj1 … Env))
     317[ -f @(choose_regs_length … (sym_eq … Eregs))
     318| whd in Env @(proj1 … (proj1 … Env))
     319| -f @(choose_regs_length … (sym_eq … Eregs))
    292320| @(λ_. St_skip l_next)
    293321| @(St_skip (f_entry f))
Note: See TracChangeset for help on using the changeset viewer.