Ignore:
Timestamp:
Nov 27, 2012, 5:50:51 PM (7 years ago)
Author:
garnier
Message:

Some tentative work on the simulation proof for expressions, in order to adjust the invariant
on memories.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r2469 r2496  
    621621      ] *)
    622622  | Evar id ⇒
    623       do 〈c,t〉 as E ← lookup' vars id; (* E is an equality proof of the shape "lookup' vars id = Ok <c,t>" *)
    624       match c return λx.? = ? → res (Σe':CMexpr ?. ?) with
    625       [ Global r ⇒ λ_.
     623      (* E is an equality proof of the shape "lookup' vars id = Ok <c,t>" *) 
     624      do 〈c,t〉 as E ← lookup' vars id;
     625      match c return λx. (c = x) → res (Σe':CMexpr ?. ?) with
     626      [ Global r ⇒ λHeq_c.
    626627          (* We are accessing a global variable in an expression. Its Cminor counterpart also depends on
    627628             its access mode:
     
    635636          | By_nothing _ ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    636637          ]
    637       | Stack n ⇒ λE.
     638      | Stack n ⇒ λHeq_c.
    638639          (* We have decided that the variable should be allocated on the stack,
    639640           * because its adress was taken somewhere or becauste it's a structured data. *)
     
    647648          ]
    648649          (* This is a local variable. Keep it as an identifier in the Cminor code, ensuring that the type of the original expr and of ty match. *)
    649       | Local ⇒ λE. type_should_eq t ty (λt.Σe':CMexpr (typ_of_type t).expr_vars (typ_of_type t) e' (local_id vars))  («Id (typ_of_type t) id, ?»)
    650       ] E
     650      | Local ⇒ λHeq_c. type_should_eq t ty (λt.Σe':CMexpr (typ_of_type t).expr_vars (typ_of_type t) e' (local_id vars))  («Id (typ_of_type t) id, ?»)
     651      ] (refl ? c)
    651652  | Ederef e1 ⇒
    652653      do e1' ← translate_expr vars e1;
     
    796797].
    797798whd try @I
    798 [ >E whd @refl
     799[ >E whd >Heq_c @refl
    799800| 2,3: @pi2
    800801| @(translate_binop_vars … E) @pi2
Note: See TracChangeset for help on using the changeset viewer.