Ignore:
Timestamp:
Jul 25, 2011, 2:58:10 PM (9 years ago)
Author:
campbell
Message:

Experimental branch where lookups of local variables in Cminor code always
succeed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch/Clight/toCminor.ma

    r1078 r1087  
    153153definition var_types ≝ identifier_map SymbolTag var_type.
    154154
     155axiom UndeclaredIdentifier : String.
     156
     157definition lookup' ≝
     158λvars:var_types.λid. opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id).
     159
     160definition local_id : var_types → ident → Prop ≝
     161λvars,id. match lookup' vars id with [ OK t ⇒ match t with [ Global _ ⇒ False | _ ⇒ True ] | _ ⇒ False ].
     162
    155163(* Note that the semantics allows locals to shadow globals.
    156164   Parameters start out as locals, but get stack allocated if their address
     
    168176definition characterise_vars : list (ident×region) → function → var_types × nat ≝
    169177λglobals, f.
    170   let m ≝ foldl ?? (λm,idr. add ?? m (\fst idr) (Global (\snd idr))) (empty_map ??) globals in
    171   let m ≝ foldl ?? (λm,v. add ?? m (\fst v) Local) m (fn_params f) in
     178  let m ≝ foldr ?? (λidr,m. add ?? m (\fst idr) (Global (\snd idr))) (empty_map ??) globals in
    172179  let mem_vars ≝ gather_mem_vars_stmt (fn_body f) in
    173   let 〈m,stacksize〉 ≝ foldl ?? (λms,v.
     180  let 〈m,stacksize〉 ≝ foldr ?? (λv,ms.
    174181    let 〈m,stack_high〉 ≝ ms in
    175182    let 〈id,ty〉 ≝ v in
     
    180187  〈m,stacksize〉.
    181188
     189lemma local_id_add_global : ∀vars,id,r,id'.
     190  local_id (add ?? vars id (Global r)) id' → local_id vars id'.
     191#var #id #r #id'
     192whd in ⊢ (% → ?) whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?] → ?)
     193cases (identifier_eq ? id id')
     194[ #E >E >lookup_add_hit whd in ⊢ (% → ?) *
     195| #NE >lookup_add_miss // @eq_identifier_elim // #E >E in NE * /2/
     196] qed.
     197
     198lemma local_id_add_miss : ∀vars,id,t,id'.
     199  id ≠ id' → local_id (add ?? vars id t) id' → local_id vars id'.
     200#vars #id #t #id' #NE
     201whd in ⊢ (% → %)
     202whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ] → match % with [ _ ⇒ ? | _ ⇒ ? ])
     203>lookup_add_miss
     204[ #H @H | @eq_identifier_elim // #E >E in NE * /2/ ]
     205qed.
     206
     207lemma contract_pair : ∀A,B.∀e:A×B. (let 〈a,b〉 ≝ e in 〈a,b〉) = e.
     208#A #B * // qed.
     209
     210lemma extract_pair : ∀A,B,C,D.  ∀u:A×B. ∀Q:A → B → C×D. ∀x,y.
     211((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) →
     212∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉.
     213#A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed.
     214
     215include "utilities/extralib.ma". (* for pair_eq1 to work around destruct's excessive normalisation *)
     216
     217lemma characterise_vars_all : ∀l,f,vars,n.
     218  characterise_vars l f = 〈vars,n〉 →
     219  ∀i. local_id vars i →
     220      Exists ? (λx.\fst x = i) (fn_params f @ fn_vars f).
     221#globals #f
     222whd in ⊢ (∀_.∀_.??%? → ?)
     223elim (fn_params f @ fn_vars f)
     224[ #vars #n whd in ⊢ (??%? → ?) #E <(pair_eq1 ?????? E) -E; #i #H @False_ind
     225  elim globals in H
     226  [ normalize //
     227  | * #id #rg #t #IH whd in ⊢ (?%? → ?) #H @IH @(local_id_add_global ???? H)
     228  ]
     229| * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?) #E #i
     230  cases (identifier_eq ? id i)
     231  [ #E' <E' #H % @refl
     232  | #NE #H whd %2 >(contract_pair var_types nat ?) in E;
     233    whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?)
     234    cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?)
     235    #H' lapply (extract_pair ???????? H') -H' * #m0 * #n0 * #EQ #EQ2
     236    @(IH m0 n0)
     237    [ 1,3: @sym_eq whd in ⊢ (???(match ?????% with [ _ ⇒ ? ])) >contract_pair @EQ
     238    | 2,4: <(pair_eq1 ?????? EQ2) in H #H' @(local_id_add_miss … H') @NE
     239    ]
     240  ]
     241] qed.
    182242
    183243include "Cminor/syntax.ma".
     
    186246alias id "CMexpr" = "cic:/matita/cerco/Cminor/syntax/expr.ind(1,0,0)".
    187247
    188 axiom UndeclaredIdentifier : String.
    189248axiom BadlyTypedAccess : String.
    190249axiom BadLvalue : String.
     
    324383].
    325384
     385lemma translate_binop_vars : ∀P,op,ty1,e1,ty2,e2,ty,e.
     386  expr_vars ? e1 P →
     387  expr_vars ? e2 P →
     388  translate_binop op ty1 e1 ty2 e2 ty = OK ? e →
     389  expr_vars ? e P.
     390#P * #ty1 #e1 #ty2 #e2 #ty #e #H1 #H2
     391whd in ⊢ (??%? → ?)
     392[ cases (classify_add ty1 ty2)
     393  [ 3,4: #z ] whd in ⊢ (??%? → ?)
     394  [ generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
     395    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
     396    whd in c:(??%?); destruct % [ @H1 | % // @H2 ]
     397  | generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
     398    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
     399    whd in c:(??%?); destruct % [ @H2 | % // @H1 ]
     400  | *: #E destruct (E) % try @H1 @H2
     401  ]
     402| cases (classify_sub ty1 ty2)
     403  [ 3,4: #z] whd in ⊢ (??%? → ?)
     404  [ 2: generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
     405    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
     406    whd in c:(??%?); destruct % [ % try @H1 @H2 ] @I
     407  | *: #E destruct (E) % try @H1 try @H2 % // @H2
     408  ]
     409| cases (classify_mul ty1 ty2) #E whd in E:(??%?); destruct
     410    % try @H1 @H2
     411| cases (classify_div ty1 ty2) #E whd in E:(??%?); destruct
     412    % try @H1 @H2
     413| cases (classify_mod ty1 ty2) #E whd in E:(??%?); destruct
     414    % try @H1 @H2
     415| 6,7,8,9: #E destruct % try @H1 @H2
     416| cases (classify_shr ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2
     417| 11,12,13,14,15,16: cases (classify_cmp ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2
     418] qed.
    326419
    327420(* We'll need to implement proper translation of pointers if we really do memory
     
    338431  ].
    339432
    340 definition translate_ptr : ∀r1,r2. CMexpr (ASTptr r1) → res (CMexpr (ASTptr r2)) ≝
    341 λr1,r2,e. check_region r1 r2 ? e.
    342 
    343 definition translate_cast : type → ∀ty2:type. CMexpr ? → res (CMexpr (typ_of_type ty2)) ≝
    344 λty1,ty2.
    345 match ty1 return λx.CMexpr (typ_of_type x) → ? with
     433definition translate_ptr : ∀P,r1,r2. (Σe:CMexpr (ASTptr r1). expr_vars ? e P) → res (Σe':CMexpr (ASTptr r2).expr_vars ? e' P) ≝
     434λP,r1,r2,e. check_region r1 r2 (λr.Σe:CMexpr (ASTptr r).expr_vars ? e P) e.
     435
     436notation "hvbox(« term 19 a, break term 19 b»)"
     437with precedence 90 for @{ (dp ?? $a $b) }.
     438
     439lemma sig_ok : ∀A:Type[0]. ∀P:A → Prop. ∀x:Σx:A.P x.
     440  P x.
     441#A #P * #a #p @p
     442qed.
     443
     444definition translate_cast : ∀P.type → ∀ty2:type. (Σe:CMexpr ?. expr_vars ? e P) → res (Σe':CMexpr (typ_of_type ty2). expr_vars ? e' P) ≝
     445λP,ty1,ty2.
     446match ty1 return λx.(Σe:CMexpr (typ_of_type x). expr_vars ? e P) → ? with
    346447[ Tint sz1 sg1 ⇒ λe.
    347     match ty2 return λx.res (CMexpr (typ_of_type x)) with
     448    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
    348449    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ocastint sg1 sz2) e)
    349450    | Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu | _ ⇒ Ofloatofint]) e)
     
    353454    ]
    354455| Tfloat sz1 ⇒ λe.
    355     match ty2 return λx.res (CMexpr (typ_of_type x)) with
    356     [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat sz2 | _ ⇒ Ointoffloat sz2 ]) e)
    357     | Tfloat sz2 ⇒ OK ? (Op1 ?? Oid e) (* FIXME *)
     456    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
     457    [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat sz2 | _ ⇒ Ointoffloat sz2 ]) e, ?»
     458    | Tfloat sz2 ⇒ OK ? «Op1 ?? Oid e, ?» (* FIXME *)
    358459    | _ ⇒ Error ? (msg TypeMismatch)
    359460    ]
    360461| Tpointer r1 _ ⇒ λe. (* will need changed for memory regions *)
    361     match ty2 return λx.res (CMexpr (typ_of_type x)) with
    362     [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ointofptr sz2) e)
    363     | Tarray r2 _ _ ⇒ translate_ptr r1 r2 e
    364     | Tpointer r2 _ ⇒ translate_ptr r1 r2 e
     462    match ty2 return λx.res (Σe':CMexpr (typ_of_type x). expr_vars ? e' P) with
     463    [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (Ointofptr sz2) e, ?»
     464    | Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e
     465    | Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e
    365466    | _ ⇒ Error ? (msg TypeMismatch)
    366467    ]
    367468| Tarray r1 _ _ ⇒ λe. (* will need changed for memory regions *)
    368     match ty2 return λx.res (CMexpr (typ_of_type x)) with
    369     [ Tint sz2 sg2 ⇒ OK ? (Op1 (ASTptr r1) (ASTint sz2 sg2) (Ointofptr sz2) e)
    370     | Tarray r2 _ _ ⇒ translate_ptr r1 r2 e
    371     | Tpointer r2 _ ⇒ translate_ptr r1 r2 e
     469    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
     470    [ Tint sz2 sg2 ⇒ OK ? «Op1 (ASTptr r1) (ASTint sz2 sg2) (Ointofptr sz2) e, ?»
     471    | Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e
     472    | Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e
    372473    | _ ⇒ Error ? (msg TypeMismatch)
    373474    ]
    374475| _ ⇒ λ_. Error ? (msg TypeMismatch)
    375 ].
     476]. whd @sig_ok qed.
    376477
    377478definition type_should_eq : ∀ty1,ty2. ∀P:type → Type[0]. P ty1 → res (P ty2) ≝
     
    404505] qed.
    405506
    406 let rec translate_expr (vars:var_types) (e:expr) on e : res (CMexpr (typ_of_type (typeof e))) ≝
    407 match e return λe. res (CMexpr (typ_of_type (typeof e))) with
     507definition bind_eq ≝ λA,B:Type[0]. λf: res A. λg: ∀a:A. f = OK ? a → res B.
     508  match f return λx. f = x → ? with
     509  [ OK x ⇒ g x
     510  | Error msg ⇒ λ_. Error ? msg
     511  ] (refl ? f).
     512
     513notation > "vbox('do' ident v 'as' ident E ← e; break e')" with precedence 40 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}.
     514
     515let rec translate_expr (vars:var_types) (e:expr) on e : res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) ≝
     516match e return λe. res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) with
    408517[ Expr ed ty ⇒
    409518  match ed with
    410   [ Econst_int sz i ⇒ OK ? (Cst ? (Ointconst sz i))
    411   | Econst_float f ⇒ OK ? (Cst ? (Ofloatconst f))
     519  [ Econst_int sz i ⇒ OK ? «Cst ? (Ointconst sz i), ?»
     520  | Econst_float f ⇒ OK ? «Cst ? (Ofloatconst f), ?»
    412521  | Evar id ⇒
    413       do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
    414       match c with
    415       [ Global r ⇒
     522      do c as E ← lookup' vars id;
     523      match c return λx.? = ? → res (Σe':CMexpr ?. ?) with
     524      [ Global r ⇒ λ_.
    416525          match access_mode ty with
    417           [ By_value q ⇒ OK ? (Mem ? r q (Cst ? (Oaddrsymbol id 0)))
    418           | By_reference _ ⇒ OK ? (Cst ? (Oaddrsymbol id 0))
     526          [ By_value q ⇒ OK ? «Mem ? r q (Cst ? (Oaddrsymbol id 0)), ?»
     527          | By_reference _ ⇒ OK ? «Cst ? (Oaddrsymbol id 0), ?»
    419528          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    420529          ]
    421       | Stack n ⇒
     530      | Stack n ⇒ λE.
    422531          match access_mode ty with
    423           [ By_value q ⇒ OK ? (Mem ? Any q (Cst ? (Oaddrstack n)))
    424           | By_reference _ ⇒ OK ? (Cst ? (Oaddrstack n))
     532          [ By_value q ⇒ OK ? «Mem ? Any q (Cst ? (Oaddrstack n)), ?»
     533          | By_reference _ ⇒ OK ? «Cst ? (Oaddrstack n), ?»
    425534          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    426535          ]
    427       | Local ⇒ OK ? (Id ? id)
    428       ]
     536      | Local ⇒ λE. OK ? «Id ? id, ?»
     537      ] E
    429538  | Ederef e1 ⇒
    430539      do e1' ← translate_expr vars e1;
    431       match typ_of_type (typeof e1) return λx.CMexpr x → ? with
     540      match typ_of_type (typeof e1) return λx.(Σz:CMexpr x.expr_vars ? z (local_id vars)) → ? with
    432541      [ ASTptr r ⇒ λe1'.
    433           match access_mode ty return λx.access_mode ty = x → res (CMexpr (typ_of_type ty)) with
    434           [ By_value q ⇒ λ_.OK ? (Mem (typ_of_type ty) ? q e1')
    435           | By_reference r' ⇒ λE. (region_should_eq r r' ? e1')⌈CMexpr (ASTptr r') ↦ CMexpr (typ_of_type ty)⌉
     542          match access_mode ty return λx.? → res (Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)) with
     543          [ By_value q ⇒ λ_.OK ? «Mem (typ_of_type ty) ? q (eject … e1'), ?»
     544          | By_reference r' ⇒ λE. do e1' ← region_should_eq r r' ? e1';
     545                                  OK ? e1'⌈Σe':CMexpr ?. expr_vars ? e' (local_id vars) ↦ Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)⌉
    436546          | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess)
    437           ] (refl ? (access_mode ty))
     547          ] (access_mode_typ ty)
    438548      | _ ⇒ λ_. Error ? (msg TypeMismatch)
    439549      ] e1'
    440550  | Eaddrof e1 ⇒
    441551      do e1' ← translate_addr vars e1;
    442       match typ_of_type ty return λx.res (CMexpr x) with
     552      match typ_of_type ty return λx.res (Σz:CMexpr x.?) with
    443553      [ ASTptr r ⇒
    444554          match e1' with
     
    450560      do op' ← translate_unop ty op;
    451561      do e1' ← translate_expr vars e1;
    452       OK ? (Op1 ?? op' e1')
     562      OK ? «Op1 ?? op' e1', ?»
    453563  | Ebinop op e1 e2 ⇒
    454564      do e1' ← translate_expr vars e1;
    455565      do e2' ← translate_expr vars e2;
    456       translate_binop op (typeof e1) e1' (typeof e2) e2' ty
     566      do e' as E ← translate_binop op (typeof e1) e1' (typeof e2) e2' ty;
     567      OK ? «e', ?»
    457568  | Ecast ty1 e1 ⇒
    458569      do e1' ← translate_expr vars e1;
    459       do e' ← translate_cast (typeof e1) ty1 e1';
    460       typ_should_eq ? (typ_of_type ty) ? e'
     570      do e' ← translate_cast ? (typeof e1) ty1 e1';
     571      do e' ← typ_should_eq (typ_of_type ty1) (typ_of_type ty) ? e';
     572      OK ? e'
    461573  | Econdition e1 e2 e3 ⇒
    462574      do e1' ← translate_expr vars e1;
    463575      do e2' ← translate_expr vars e2;
    464       do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
     576      do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2';
    465577      do e3' ← translate_expr vars e3;
    466       do e3' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e3';
    467       match typ_of_type (typeof e1) return λx.CMexpr x → ? with
    468       [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' e2' e3')
     578      do e3' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e3';
     579      match typ_of_type (typeof e1) return λx.(Σe1':CMexpr x. expr_vars ? e1' (local_id vars)) → ? with
     580      [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' e3', ?»
    469581      | _ ⇒ λ_.Error ? (msg TypeMismatch)
    470582      ] e1'
     
    474586      match ty with
    475587      [ Tint sz _ ⇒
    476         do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
    477         match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type ty)) with
    478         [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' e2' (Cst ? (Ointconst sz (zero ?))))
     588        do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2';
     589        match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → res ? with
     590        [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' (Cst ? (Ointconst sz (zero ?))), ?»
    479591        | _ ⇒ λ_.Error ? (msg TypeMismatch)
    480592        ] e1'
     
    486598      match ty with
    487599      [ Tint sz _ ⇒
    488         do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2';
    489         match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type ty)) with
    490         [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' (Cst ? (Ointconst sz (repr ? 1))) e2')
     600        do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2';
     601        match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → ? with
     602        [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' (Cst ? (Ointconst sz (repr ? 1))) e2', ?»
    491603        | _ ⇒ λ_.Error ? (msg TypeMismatch)
    492604        ] e1'
     
    495607  | Esizeof ty1 ⇒
    496608      match ty with
    497       [ Tint sz _ ⇒ OK ? (Cst ? (Ointconst sz (repr ? (sizeof ty1))))
     609      [ Tint sz _ ⇒ OK ? «Cst ? (Ointconst sz (repr ? (sizeof ty1))), ?»
    498610      | _ ⇒ Error ? (msg TypeMismatch)
    499611      ]
    500612  | Efield e1 id ⇒
    501       do e' ← match typeof e1 with
     613      match typeof e1 with
    502614      [ Tstruct _ fl ⇒
    503615          do e1' ← translate_addr vars e1;
     
    506618            do off ← field_offset id fl;
    507619            match access_mode ty with
    508             [ By_value q ⇒ OK ? (Mem ? r q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))))
    509             | By_reference _ ⇒ OK ? (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off))))
     620            [ By_value q ⇒ OK ? «Mem ? r q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))),?»
     621            | By_reference _ ⇒ OK ? «Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off))),?»
    510622            | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
    511623            ]
     
    515627          match e1' with
    516628          [ dp r e1' ⇒
    517             match access_mode ty return λx. access_mode ty = x → res (CMexpr (typ_of_type ty)) with
    518             [ By_value q ⇒ λ_. OK ? (Mem ?? q e1')
    519             | By_reference r' ⇒ λE. (region_should_eq r r' ? e1')⌈res (CMexpr (ASTptr r')) ↦ res (CMexpr (typ_of_type ty))⌉
     629            match access_mode ty return λx. access_mode ty = x → res ? with
     630            [ By_value q ⇒ λ_. OK ? «Mem ?? q e1', ?»
     631            | By_reference r' ⇒  λE. do e1' ← region_should_eq r r' ? e1';
     632                                OK ? e1'⌈Σz:CMexpr (ASTptr r').? ↦ Σz:CMexpr (typ_of_type ty).?⌉
    520633            | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess)
    521634            ] (refl ? (access_mode ty))
    522635          ]
    523636      | _ ⇒ Error ? (msg BadlyTypedAccess)
    524       ];
    525       typ_should_eq ? (typ_of_type ty) ? e'
     637      ]
    526638  | Ecost l e1 ⇒
    527639      do e1' ← translate_expr vars e1;
    528       do e' ← OK ? (Ecost ? l e1');
    529       typ_should_eq ? (typ_of_type ty) ? e'
     640      do e' ← OK ? «Ecost ? l e1',?»;
     641      typ_should_eq (typ_of_type (typeof e1)) (typ_of_type ty) (λx.Σe:CMexpr x.?) e'
    530642  ]
    531 ] and translate_addr (vars:var_types) (e:expr) on e : res (Σr.CMexpr (ASTptr r)) ≝
     643] and translate_addr (vars:var_types) (e:expr) on e : res (Σr. Σe':CMexpr (ASTptr r). expr_vars ? e' (local_id vars)) ≝
    532644match e with
    533645[ Expr ed _ ⇒
     
    535647  [ Evar id ⇒
    536648      do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
    537       match c return λ_. res (Σr.CMexpr (ASTptr r)) with
    538       [ Global r ⇒ OK ? (dp ?? r (Cst ? (Oaddrsymbol id 0)))
    539       | Stack n ⇒ OK ? (dp ?? Any (Cst ? (Oaddrstack n)))
     649      match c return λ_. res (Σr.Σz:CMexpr (ASTptr r).?) with
     650      [ Global r ⇒ OK ? «r, «Cst ? (Oaddrsymbol id 0), ?»»
     651      | Stack n ⇒ OK ? «Any, «Cst ? (Oaddrstack n), ?»»
    540652      | Local ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] (* TODO: could rule out? *)
    541653      ]
    542654  | Ederef e1 ⇒
    543655      do e1' ← translate_expr vars e1;
    544       match typ_of_type (typeof e1) return λx. CMexpr x → res (Σr. CMexpr (ASTptr r)) with
    545       [ ASTptr r ⇒ λe1'.OK ? (dp ?? r e1')
     656      match typ_of_type (typeof e1) return λx. (Σz:CMexpr x.expr_vars ? z (local_id vars)) → res (Σr. Σz:CMexpr (ASTptr r). ?) with
     657      [ ASTptr r ⇒ λe1'.OK ? «r, e1'»
    546658      | _ ⇒ λ_.Error ? (msg BadlyTypedAccess)
    547659      ] e1'
     
    552664          do off ← field_offset id fl;
    553665          match e1' with
    554           [ dp r e1' ⇒ OK ? (dp ?? r (Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))))
     666          [ dp r e1'' ⇒ OK (Σr:region.Σe:CMexpr (ASTptr r).?) («r, «Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1'' (Cst ? (Ointconst I32 (repr ? off))), ?» »)
    555667          ]
    556668      | Tunion _ _ ⇒ translate_addr vars e1
     
    560672  ]
    561673].
    562 >(access_mode_typ … E) @refl
    563 qed.
    564 
    565 inductive destination : Type[0] ≝
    566 | IdDest : ident → destination
    567 | MemDest : ∀r:region. memory_chunk → CMexpr (ASTptr r) → destination.
     674whd try @I
     675[ >E @I
     676| >(E ? (refl ??)) @refl
     677| 3,4: @sig_ok
     678| @(translate_binop_vars … E) @sig_ok
     679| % [ % ] @sig_ok
     680| % [ % @sig_ok ] whd @I
     681| % [ % [ @sig_ok | @I ] | @sig_ok ]
     682| % [ @sig_ok | @I ]
     683| % [ @sig_ok | @I ]
     684| >(access_mode_typ … E) @refl
     685| @sig_ok
     686| @sig_ok
     687| % [ @sig_ok | @I ]
     688] qed.
     689
     690inductive destination (vars:var_types) : Type[0] ≝
     691| IdDest : ∀id:ident. local_id vars id → destination vars
     692| MemDest : ∀r:region. memory_chunk → (Σe:CMexpr (ASTptr r).expr_vars ? e (local_id vars)) → destination vars.
    568693
    569694definition translate_dest ≝
     
    578703        match ed1 with
    579704        [ Evar id ⇒
    580             do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
    581             match c with
    582             [ Local ⇒ OK ? (IdDest id)
    583             | Global r ⇒ OK ? (MemDest r q (Cst ? (Oaddrsymbol id 0)))
    584             | Stack n ⇒ OK ? (MemDest Any q (Cst ? (Oaddrstack n)))
    585             ]
     705            do c as E ← lookup' vars id;
     706            match c return λx.? → ? with
     707            [ Local ⇒ λE. OK ? (IdDest vars id ?)
     708            | Global r ⇒ λE. OK ? (MemDest ? r q (Cst ? (Oaddrsymbol id 0)))
     709            | Stack n ⇒ λE. OK ? (MemDest ? Any q (Cst ? (Oaddrstack n)))
     710            ] E
    586711        | _ ⇒
    587712            do e1' ← translate_addr vars e1;
    588             match e1' with [ dp r e1' ⇒ OK ? (MemDest r q e1') ]
     713            match e1' with [ dp r e1' ⇒ OK ? (MemDest ? r q e1') ]
    589714        ]
    590715    ].
     716whd // >E @I
     717qed.
    591718(*
    592719definition translate_assign ≝
     
    614741    ].
    615742*)
    616 definition translate_assign
     743definition translate_assign : ∀vars:var_types. expr → expr → res (Σs:stmt.stmt_vars s (local_id vars))
    617744λvars,e1,e2.
    618745do e2' ← translate_expr vars e2;
    619746do dest ← translate_dest vars e1 (typeof e2);
    620747match dest with
    621 [ IdDest id ⇒ OK ? (St_assign ? id e2')
    622 | MemDest r q e1' ⇒ OK ? (St_store ? r q e1' e2')
    623 ].
     748[ IdDest id p ⇒ OK ? «St_assign ? id e2', ?»
     749| MemDest r q e1' ⇒ OK ? «St_store ? r q e1' e2', ?»
     750].
     751whd
     752[ % // @sig_ok
     753| % @sig_ok
     754] qed.
    624755
    625756definition m_option_map : ∀A,B:Type[0]. (A → res B) → option A → res (option B) ≝
     
    630761].
    631762
    632 definition translate_expr_sigma : var_types → expr → res (Σt:typ.CMexpr t) ≝
     763definition translate_expr_sigma : ∀vars:var_types. expr → res (Σe:(Σt:typ.CMexpr t). match e with [ dp t e ⇒ expr_vars t e (local_id vars) ]) ≝
    633764λv,e.
    634765  do e' ← translate_expr v e;
    635   OK ? (dp ? (λt:typ.CMexpr t) ? e').
     766  OK (Σe:(Σt:typ.CMexpr t).?) ««?, e'», ?».
     767whd @sig_ok
     768qed.
    636769
    637770axiom FIXME : String.
    638771
    639 let rec translate_statement (vars:var_types) (tmp:ident) (tmpp:ident) (s:statement) on s : res stmt ≝
     772let rec mmap_sigma (A,B:Type[0]) (P:B → Prop) (f:A → res (Σx:B.P x)) (l:list A) on l : res (Σl':list B.All B P l') ≝
     773match l with
     774[ nil ⇒ OK ? «nil B, ?»
     775| cons h t ⇒
     776    do h' ← f h;
     777    do t' ← mmap_sigma A B P f t;
     778    OK ? «cons B h' t', ?»
     779].
     780whd // %
     781[ @(sig_ok B P)
     782| cases t' #l' #p @p
     783] qed.
     784
     785let rec translate_statement (vars:var_types) (tmp:Σi:ident.local_id vars i) (tmpp:Σi:ident.local_id vars i) (s:statement) on s : res (Σs:stmt.stmt_vars s (local_id vars)) ≝
    640786match s with
    641 [ Sskip ⇒ OK ? St_skip
     787[ Sskip ⇒ OK ? «St_skip, ?»
    642788| Sassign e1 e2 ⇒ translate_assign vars e1 e2
    643789| Scall ret ef args ⇒
    644790    do ef' ← translate_expr vars ef;
    645     do ef' ← typ_should_eq ? (ASTptr Code) ? ef';
    646     do args' ← mmap … (translate_expr_sigma vars) args;
     791    do ef' ← typ_should_eq (typ_of_type (typeof ef)) (ASTptr Code) ? ef';
     792    do args' ← mmap_sigma … (translate_expr_sigma vars) args;
    647793    match ret with
    648     [ None ⇒ OK ? (St_call (None ?) ef' args')
     794    [ None ⇒ OK ? «St_call (None ?) ef' args', ?»
    649795    | Some e1 ⇒
    650796        do dest ← translate_dest vars e1 (typeof e1); (* TODO: check if it's sane to use e1's type rather than the return type *)
    651797        match dest with
    652         [ IdDest id ⇒ OK ? (St_call (Some ? id) ef' args')
     798        [ IdDest id p ⇒ OK ? «St_call (Some ? id) ef' args', ?»
    653799        | MemDest r q e1' ⇒
    654800            let tmp' ≝ match q with [ Mpointer _ ⇒ tmpp | _ ⇒ tmp ] in
    655             OK ? (St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)))
     801            OK ? «St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)), ?»
    656802        ]
    657803    ]
     
    659805    do s1' ← translate_statement vars tmp tmpp s1;
    660806    do s2' ← translate_statement vars tmp tmpp s2;
    661     OK ? (St_seq s1' s2')
     807    OK ? «St_seq s1' s2', ?»
    662808| Sifthenelse e1 s1 s2 ⇒
    663809    do e1' ← translate_expr vars e1;
    664     match typ_of_type (typeof e1) return λx.CMexpr x → ? with
     810    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
    665811    [ ASTint _ _ ⇒ λe1'.
    666812        do s1' ← translate_statement vars tmp tmpp s1;
    667813        do s2' ← translate_statement vars tmp tmpp s2;
    668         OK ? (St_ifthenelse ?? e1' s1' s2')
     814        OK ? «St_ifthenelse ?? e1' s1' s2', ?»
    669815    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    670816    ] e1'
    671817| Swhile e1 s1 ⇒
    672818    do e1' ← translate_expr vars e1;
    673     match typ_of_type (typeof e1) return λx.CMexpr x → ? with
     819    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
    674820    [ ASTint _ _ ⇒ λe1'.
    675821        do s1' ← translate_statement vars tmp tmpp s1;
    676822        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    677         OK ? (St_block
     823        OK ? «St_block
    678824               (St_loop
    679                  (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))))
     825                 (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))), ?»
    680826    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    681827    ] e1'
    682828| Sdowhile e1 s1 ⇒
    683829    do e1' ← translate_expr vars e1;
    684     match typ_of_type (typeof e1) return λx.CMexpr x → ? with
     830    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
    685831    [ ASTint _ _ ⇒ λe1'.
    686832        do s1' ← translate_statement vars tmp tmpp s1;
    687833        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    688         OK ? (St_block
     834        OK ? «St_block
    689835               (St_loop
    690                  (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))))
     836                 (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))), ?»
    691837    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    692838    ] e1'
    693839| Sfor s1 e1 s2 s3 ⇒
    694840    do e1' ← translate_expr vars e1;
    695     match typ_of_type (typeof e1) return λx.CMexpr x → ? with
     841    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
    696842    [ ASTint _ _ ⇒ λe1'.
    697843        do s1' ← translate_statement vars tmp tmpp s1;
     
    699845        do s3' ← translate_statement vars tmp tmpp s3;
    700846        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    701         OK ? (St_seq s1'
     847        OK ? «St_seq s1'
    702848             (St_block
    703849               (St_loop
    704                  (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))))
     850                 (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))), ?»
    705851    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    706852    ] e1'
    707 | Sbreak ⇒ OK ? (St_exit 1)
    708 | Scontinue ⇒ OK ? (St_exit 0)
     853| Sbreak ⇒ OK ? «St_exit 1, ?»
     854| Scontinue ⇒ OK ? «St_exit 0, ?»
    709855| Sreturn ret ⇒
    710856    match ret with
    711     [ None ⇒ OK ? (St_return (None ?))
     857    [ None ⇒ OK ? «St_return (None ?), ?»
    712858    | Some e1 ⇒
    713859        do e1' ← translate_expr vars e1;
    714         OK ? (St_return (Some ? (dp … e1')))
     860        OK ? «St_return (Some ? (dp … e1')), ?»
    715861    ]
    716862| Sswitch e1 ls ⇒ Error ? (msg FIXME)
    717863| Slabel l s1 ⇒
    718864    do s1' ← translate_statement vars tmp tmpp s1;
    719     OK ? (St_label l s1')
    720 | Sgoto l ⇒ OK ? (St_goto l)
     865    OK ? «St_label l s1', ?»
     866| Sgoto l ⇒ OK ? «St_goto l, ?»
    721867| Scost l s1 ⇒
    722868    do s1' ← translate_statement vars tmp tmpp s1;
    723     OK ? (St_cost l s1')
    724 ].
     869    OK ? «St_cost l s1', ?»
     870].
     871whd try @I
     872[ % [ % [ @p | @sig_ok ] | @(sig_ok ? (All ??)) ]
     873| % [ whd % [ % [ @sig_ok | @sig_ok ] | @(sig_ok ? (All ??)) ] | whd % @sig_ok ]
     874| % [ % [ @I | @sig_ok ] | @(sig_ok ? (All ??)) ]
     875| % @sig_ok
     876| % [ % @sig_ok | @sig_ok ]
     877| % [ % @sig_ok | whd @I ]
     878| % [ @sig_ok | whd % [ % [ @sig_ok | @I ] | @I ] ]
     879| % [ @sig_ok | whd % [ % [ @sig_ok | whd % @sig_ok ] | @I ] ]
     880| @sig_ok
     881| @sig_ok
     882| @sig_ok
     883] qed.
    725884
    726885axiom ParamGlobalMixup : String.
    727886
    728 definition alloc_params : var_types → list (ident×type) → stmt → res stmt
     887definition alloc_params : ∀vars:var_types. list (ident×type) → (Σs:stmt.stmt_vars s (local_id vars)) → res (Σs:stmt.stmt_vars s (local_id vars))
    729888λvars,params,s. foldl ?? (λs,it.
    730889  let 〈id,ty〉 ≝ it in
    731890  do s ← s;
    732   do t ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
    733   match t with
    734   [ Local ⇒ OK ? s
    735   | Stack n ⇒
     891  do t as E ← lookup' vars id;
     892  match t return λx.? → ? with
     893  [ Local ⇒ λE. OK (Σs:stmt.?) s
     894  | Stack n ⇒ λE.
    736895      do q ← match access_mode ty with
    737896      [ By_value q ⇒ OK ? q
     
    739898      | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    740899      ];
    741       OK ? (St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty) id)) s)
    742   | Global _ ⇒ Error ? [MSG ParamGlobalMixup; CTX ? id]
    743   ]) (OK ? s) params.
     900      OK ? «St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty) id)) s, ?»
     901  | Global _ ⇒ λE. Error ? [MSG ParamGlobalMixup; CTX ? id]
     902  ] E) (OK ? s) params.
     903whd % [ whd % [ @I | whd >E @I ] | @sig_ok ]
     904qed.
    744905
    745906definition bigid1 ≝ an_identifier SymbolTag [[
     
    754915false;false;false;true]].
    755916
     917lemma Exists_rm : ∀A,P,l1,x,l2. Exists A P (l1@l2) → Exists A P (l1@x::l2).
     918#A #P #l1 #x #l2 elim l1
     919[ normalize #H %2 @H
     920| #h #t #IH normalize * [ #H %1 @H | #H %2 @IH @H ]
     921qed.
     922
     923lemma Exists_mid : ∀A,P,l1,x,l2. P x → Exists A P (l1@x::l2).
     924#A #P #l1 #x #l2 #H elim l1
     925[ %1 @H
     926| #h #t #IH %2 @IH
     927] qed.
     928
     929lemma Exists_map : ∀A,B,P,Q,f,l.
     930Exists A P l →
     931(∀a.P a → Q (f a)) →
     932Exists B Q (map A B f l).
     933#A #B #P #Q #f #l elim l //
     934#h #t #IH * [ #H #F %1 @F @H | #H #F %2 @IH [ @H | @F ] ] qed.
     935
     936notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)"
     937 with precedence 10
     938for @{ match $t return λx.x = $t → ? with [ pair ${ident x} ${ident y} ⇒
     939        λ${ident E}.$s ] (refl ? $t) }.
     940
     941lemma local_id_add_local : ∀vars,id,id'.
     942  local_id vars id →
     943  local_id (add ?? vars id' Local) id.
     944#vars #id #id' #H
     945whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ?] cases (identifier_eq ? id id')
     946[ #E < E >lookup_add_hit //
     947| #NE >lookup_add_miss // @eq_identifier_elim // #E cases NE >E /2/
     948] qed.
     949
    756950(* FIXME: the temporary handling is nonsense, I'm afraid. *)
    757951definition translate_function : list (ident×region) → function → res internal_function ≝
    758952λglobals, f.
    759   let 〈vartypes, stacksize〉 ≝ characterise_vars globals f in
     953  let 〈vartypes0, stacksize〉 as E ≝ characterise_vars globals f in
    760954  let tmp ≝ bigid1 in (* FIXME *)
    761955  let tmpp ≝ bigid2 in (* FIXME *)
     956  let vartypes ≝ add … (add … vartypes0 tmp Local) tmpp Local in
    762957  do s ← translate_statement vartypes tmp tmpp (fn_body f);
    763958  do s ← alloc_params vartypes (fn_params f) s;
     
    767962    (〈tmp,ASTint I32 Unsigned〉::〈tmpp,ASTptr Any〉::(map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_vars f)))
    768963    stacksize
    769     s).
     964    s ?).
     965[ whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) >lookup_add_hit %
     966| whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) >lookup_add_miss [ >lookup_add_hit %| % ]
     967| @stmt_vars_mp [ 3: @sig_ok | skip ]
     968  #i #H cases (identifier_eq ? tmp i)
     969  [ #E <E @Exists_mid @refl
     970  | #NE1 @Exists_rm cases (identifier_eq ? tmpp i)
     971    [ #E <E @Exists_mid @refl
     972    | #NE2 @Exists_rm
     973      >map_append
     974      @Exists_map [ 2: @(characterise_vars_all … (sym_eq ??? E) i)
     975                       @(local_id_add_miss ?? Local ? NE1)
     976                       @(local_id_add_miss ?? Local ? NE2) @H
     977                  | skip
     978                  | * #id #ty #E1 <E1 @refl
     979                  ]
     980    ]
     981  ]
     982] qed.
    770983
    771984definition translate_fundef : list (ident×region) → clight_fundef → res (fundef internal_function) ≝
Note: See TracChangeset for help on using the changeset viewer.