Changeset 2469


Ignore:
Timestamp:
Nov 15, 2012, 6:33:55 PM (7 years ago)
Author:
campbell
Message:

Fix up opaque type errors from recent changes.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r2468 r2469  
    695695      do e3' ← translate_expr vars e3;
    696696      do e3' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e3';
    697       match typ_of_type (typeof e1) return λx.(Σe1':CMexpr x. expr_vars ? e1' (local_id vars)) → ? with
     697      match typ_of_type (typeof e1) return λx.(Σe1':CMexpr x. expr_vars ? e1' (local_id vars)) → res ? with
    698698      [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' e3', ?»
    699699      | _ ⇒ λ_.Error ? (msg TypeMismatch)
     
    705705      [ Tint sz sg ⇒
    706706        do e2' ← type_should_eq ? (Tint sz sg) (λx.Σe:CMexpr (typ_of_type x).?) e2';
    707         match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → (res (Σe:CMexpr x. expr_vars ? e (local_id vars))) with
     707        match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → (res ?) with
    708708        [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' (Cst ? (Ointconst sz sg (zero ?))), ?»
    709709        | _ ⇒ λ_.Error ? (msg TypeMismatch)
     
    718718        do e2' ← type_should_eq ? (Tint sz sg) (λx.Σe:CMexpr (typ_of_type x).?) e2';
    719719        match typ_of_type (typeof e1)
    720         return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → ? with
     720        return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → res ? with
    721721        [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' (Cst ? (Ointconst sz sg (repr ? 1))) e2', ?»
    722722        | _ ⇒ λ_. Error ? (msg TypeMismatch)
     
    11491149| Sifthenelse e1 s1 s2 ⇒
    11501150    do e1' ← translate_expr vars e1;
    1151     match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
     1151    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → res ? with
    11521152    [ ASTint _ _ ⇒ λe1'.
    11531153         do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag rettyp s1;
     
    11621162| Swhile e1 s1 ⇒
    11631163    do e1' ← translate_expr vars e1;
    1164     match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
     1164    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → res ? with
    11651165    [ ASTint _ _ ⇒ λe1'.         
    11661166        let 〈labels, ul1〉 as E1 ≝ mklabels ul in
     
    11781178| Sdowhile e1 s1 ⇒
    11791179    do e1' ← translate_expr vars e1;
    1180     match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
     1180    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → res ? with
    11811181    [ ASTint _ _ ⇒ λe1'.
    11821182        let 〈labels, ul1〉 as E1 ≝ mklabels ul in
     
    12071207| Sfor s1 e1 s2 s3 ⇒
    12081208    do e1' ← translate_expr vars e1;
    1209     match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
     1209    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → res ? with
    12101210    [ ASTint _ _ ⇒ λe1'.
    12111211        let 〈labels, ul1〉 as E ≝ mklabels ul in
     
    12771277try (#H1 try #H2 assumption)
    12781278[ 1,5: @(tmp_preserved … p) ]
    1279 [ 1,3: elim e2' | 2,9,24: elim e1' | 4,7,14: elim ef' ]
     1279[ 1,3: elim e2' | 2,9,23: elim e1' | 4,7,13: elim ef' ]
    12801280[ 1,2,3,4,5,6,7,8 : #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) ]
    12811281[ 1: @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ])
    12821282             | 2: * #t #e #Hev whd in Hev ⊢ %; @(expr_vars_mp … Hev) #i #t #Hp @(tmp_preserved … Hp)
    12831283             | 3: elim args' // ]
    1284 | 8: (* we should be able to merge this case with the previous ... *)
     1284| 7: (* we should be able to merge this case with the previous ... *)
    12851285     @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ])
    12861286             | 2: * #t #e #Hev whd in Hev ⊢ %; @(expr_vars_mp … Hev) #i #t #Hp @(tmp_preserved … Hp)
     
    12931293       | 2: elim args' // ]
    12941294| 4: @(local_id_fresh_tmp vars tmp uv1 (typeof e1) uv Etmp) ]
    1295 [ 1: #size #sign | 2: | 3: #fsize ]
    1296 [ 1,2,3: #H @(alloc_tmp_preserves vars tmp uv uv1 … Etmp) @H ]
     1295[ 1: #size #sign | 2: ]
     1296[ 1,2: #H @(alloc_tmp_preserves vars tmp uv uv1 … Etmp) @H ]
    12971297try @refl (* Does (at least) the return_ok cases *)
    12981298try @(match fgens1 return λx.x=fgens1 → ? with
Note: See TracChangeset for help on using the changeset viewer.