Changeset 1369


Ignore:
Timestamp:
Oct 14, 2011, 10:56:45 AM (8 years ago)
Author:
campbell
Message:

Put type information into front-end unary ops.
Slight change to semantics: booleans produced by Onotbool can be any given
integer size.

Location:
src
Files:
9 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r1351 r1369  
    172172axiom MissingField : String.
    173173
     174
     175definition type_should_eq : ∀ty1,ty2. ∀P:type → Type[0]. P ty1 → res (P ty2) ≝
     176λty1,ty2,P,p.
     177  do E ← assert_type_eq ty1 ty2;
     178  OK ? (match E return λx.λ_. P ty1 → P x with [ refl ⇒ λp.p ] p).
     179
     180definition region_should_eq : ∀r1,r2. ∀P:region → Type[0]. P r1 → res (P r2).
     181* * #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
     182qed.
     183
     184definition typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2).
     185* [ #sz1 #sg1 | #r1 | #sz1 ]
     186* [ 1,5,9: | *: #a #b #c try #d @(Error ? (msg TypeMismatch)) ]
     187[ *; cases sz1 [ 1,5,9: | *: #a #b #c @(Error ? (msg TypeMismatch)) ]
     188  *; cases sg1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
     189| *; #P #p @(region_should_eq r1 ?? p)
     190| *; cases sz1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
     191] qed.
     192
     193
    174194alias id "CLunop" = "cic:/matita/cerco/Clight/Csyntax/unary_operation.ind(1,0,0)".
    175195alias id "CMunop" = "cic:/matita/cerco/common/FrontEndOps/unary_operation.ind(1,0,0)".
    176196
    177197(* XXX: For some reason matita refuses to pick the right one unless forced. *)
    178 alias id "CMnotbool" = "cic:/matita/cerco/common/FrontEndOps/unary_operation.con(0,6,0)".
    179 
    180 definition translate_unop : type → CLunop → res CMunop
    181 λty.λop:CLunop.
     198alias id "CMnotbool" = "cic:/matita/cerco/common/FrontEndOps/unary_operation.con(0,3,0)".
     199
     200definition translate_unop : ∀t,t':typ. CLunop → res (CMunop t t')
     201λt,t'.λop:CLunop.
    182202  match op with
    183   [ Onotbool ⇒ OK ? CMnotbool
    184   | Onotint ⇒ OK ? Onotint
    185   | Oneg ⇒
    186       match ty with
    187       [ Tint _ _ ⇒ OK ? Onegint
    188       | Tfloat _ ⇒ OK ? Onegf
     203  [ Onotbool ⇒
     204      match t return λt. res (CMunop t t') with
     205      [ ASTint sz sg ⇒
     206          match t' return λt'. res (CMunop ? t') with
     207          [ ASTint sz' sg' ⇒ OK ? (CMnotbool ????)
     208          | _ ⇒ Error ? (msg TypeMismatch)
     209          ]
     210      | ASTptr r ⇒
     211          match t' return λt'. res (CMunop ? t') with
     212          [ ASTint sz' sg' ⇒ OK ? (CMnotbool ????)
     213          | _ ⇒ Error ? (msg TypeMismatch)
     214          ]
    189215      | _ ⇒ Error ? (msg TypeMismatch)
    190216      ]
    191   ].
     217  | Onotint ⇒
     218      match t' return λt'. res (CMunop t t') with
     219      [ ASTint sz sg ⇒ typ_should_eq ?? (λt. CMunop t (ASTint ??)) (Onotint sz sg)
     220      | _ ⇒ Error ? (msg TypeMismatch)
     221      ]
     222  | Oneg ⇒
     223      match t' return λt'. res (CMunop t t') with
     224      [ ASTint sz sg ⇒ typ_should_eq ?? (λt.CMunop t (ASTint ??)) (Onegint sz sg)
     225      | ASTfloat sz ⇒ typ_should_eq ?? (λt.CMunop t (ASTfloat sz)) (Onegf sz)
     226      | _ ⇒ Error ? (msg TypeMismatch)
     227      ]
     228  ]. @I qed.
    192229
    193230definition translate_add ≝
     
    356393λP,r1,r2,e. check_region r1 r2 (λr.Σe:CMexpr (ASTptr r).expr_vars ? e P) e.
    357394
     395axiom FIXME : String.
     396
    358397definition translate_cast : ∀P.type → ∀ty2:type. (Σe:CMexpr ?. expr_vars ? e P) → res (Σe':CMexpr (typ_of_type ty2). expr_vars ? e' P) ≝
    359398λP,ty1,ty2.
     
    361400[ Tint sz1 sg1 ⇒ λe.
    362401    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
    363     [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ocastint sg1 sz2) e)
    364     | Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu | _ ⇒ Ofloatofint]) e)
    365     | Tpointer r _ ⇒ OK ? (Op1 ?? (Optrofint r) e)
    366     | Tarray r _ _ ⇒ OK ? (Op1 ?? (Optrofint r) e)
     402    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ocastint ? sg1 sz2 ?) e)
     403    | Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu ?? | _ ⇒ Ofloatofint ??]) e)
     404    | Tpointer r _ ⇒ OK ? (Op1 ?? (Optrofint ?? r) e)
     405    | Tarray r _ _ ⇒ OK ? (Op1 ?? (Optrofint ?? r) e)
    367406    | _ ⇒ Error ? (msg TypeMismatch)
    368407    ]
    369408| Tfloat sz1 ⇒ λe.
    370409    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
    371     [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat sz2 | _ ⇒ Ointoffloat sz2 ]) e, ?»
    372     | Tfloat sz2 ⇒ OK ? «Op1 ?? Oid e, ?» (* FIXME *)
     410    [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat ? sz2 | _ ⇒ Ointoffloat ? sz2 ]) e, ?»
     411    | Tfloat sz2 ⇒ Error ? (msg FIXME) (* OK ? «Op1 ?? (Oid ?) e, ?» (* FIXME *) *)
    373412    | _ ⇒ Error ? (msg TypeMismatch)
    374413    ]
    375414| Tpointer r1 _ ⇒ λe. (* will need changed for memory regions *)
    376415    match ty2 return λx.res (Σe':CMexpr (typ_of_type x). expr_vars ? e' P) with
    377     [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (Ointofptr sz2) e, ?»
     416    [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (Ointofptr sz2 ??) e, ?»
    378417    | Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e
    379418    | Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e
     
    382421| Tarray r1 _ _ ⇒ λe. (* will need changed for memory regions *)
    383422    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
    384     [ Tint sz2 sg2 ⇒ OK ? «Op1 (ASTptr r1) (ASTint sz2 sg2) (Ointofptr sz2) e, ?»
     423    [ Tint sz2 sg2 ⇒ OK ? «Op1 (ASTptr r1) (ASTint sz2 sg2) (Ointofptr sz2 ??) e, ?»
    385424    | Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e
    386425    | Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e
     
    389428| _ ⇒ λ_. Error ? (msg TypeMismatch)
    390429]. whd @use_sig qed.
    391 
    392 definition type_should_eq : ∀ty1,ty2. ∀P:type → Type[0]. P ty1 → res (P ty2) ≝
    393 λty1,ty2,P,p.
    394   do E ← assert_type_eq ty1 ty2;
    395   OK ? (match E return λx.λ_. P ty1 → P x with [ refl ⇒ λp.p ] p).
    396 
    397 definition region_should_eq : ∀r1,r2. ∀P:region → Type[0]. P r1 → res (P r2).
    398 * * #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
    399 qed.
    400 
    401 definition typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2).
    402 * [ #sz1 #sg1 | #r1 | #sz1 ]
    403 * [ 1,5,9: | *: #a #b #c try #d @(Error ? (msg TypeMismatch)) ]
    404 [ *; cases sz1 [ 1,5,9: | *: #a #b #c @(Error ? (msg TypeMismatch)) ]
    405   *; cases sg1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
    406 | *; #P #p @(region_should_eq r1 ?? p)
    407 | *; cases sz1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
    408 ] qed.
    409 
    410430
    411431lemma access_mode_typ : ∀ty,r. access_mode ty = By_reference r → typ_of_type ty = ASTptr r.
     
    464484      ]
    465485  | Eunop op e1 ⇒
    466       do op' ← translate_unop ty op;
     486      do op' ← translate_unop (typ_of_type (typeof e1)) (typ_of_type ty) op;
    467487      do e1' ← translate_expr vars e1;
    468488      OK ? «Op1 ?? op' e1', ?»
     
    690710qed.
    691711
    692 axiom FIXME : String.
    693 
    694712record tmpgen : Type[0] ≝ {
    695713  tmp_universe : universe SymbolTag;
  • src/Cminor/initialisation.ma

    r1316 r1369  
    1717| Init_float64 f       ⇒ Some ? (dp ?? Mfloat64 (Cst ? (Ofloatconst f)))
    1818| Init_space n         ⇒ None ?
    19 | Init_null r          ⇒ Some ? (dp ?? (Mpointer r) (Op1 (ASTint I8 Unsigned) ? (Optrofint r) (Cst ? (Ointconst I8 (zero ?)))))
     19| Init_null r          ⇒ Some ? (dp ?? (Mpointer r) (Op1 (ASTint I8 Unsigned) ? (Optrofint ?? r) (Cst ? (Ointconst I8 (zero ?)))))
    2020| Init_addrof r id off ⇒ Some ? (dp ?? (Mpointer r) (Cst ? (Oaddrsymbol id off)))
    2121].
  • src/Cminor/semantics.ma

    r1352 r1369  
    102102| Op1 ty ty' op e' ⇒ λEnv.
    103103    do 〈tr,v〉 ← eval_expr ge ? e' en ? sp m;
    104     do r ← opt_to_res … (msg FailedOp) (eval_unop op v);
     104    do r ← opt_to_res … (msg FailedOp) (eval_unop ?? op v);
    105105    OK ? 〈tr, r〉
    106106| Op2 ty1 ty2 ty' op e1 e2 ⇒ λEnv.
  • src/Cminor/syntax.ma

    r1316 r1369  
    1010| Id : ∀t. ident → expr t
    1111| Cst : ∀t. constant → expr t
    12 | Op1 : ∀t,t'. unary_operation → expr t → expr t'
     12| Op1 : ∀t,t'. unary_operation t t' → expr t → expr t'
    1313| Op2 : ∀t1,t2,t'. binary_operation → expr t1 → expr t2 → expr t'
    1414| Mem : ∀t,r. memory_chunk → expr (ASTptr r) → expr t
  • src/Cminor/toRTLabs.ma

    r1316 r1369  
    296296let rec add_expr (le:label_env) (env:env) (ty:typ) (e:expr ty) (Env:expr_vars ty e (present ?? env)) (dst:register) (f:partial_fn le) on e: Σf':partial_fn le. fn_graph_included le f f' ≝
    297297match e return λty,e.expr_vars ty e (present ?? env) → Σf':partial_fn le. fn_graph_included le f f' with
    298 [ Id _ i ⇒ λEnv.
     298[ Id t i ⇒ λEnv.
    299299    let r ≝ lookup_reg env i Env in
    300300    match register_eq r dst with
    301301    [ inl _ ⇒ «f, ?»
    302     | inr _ ⇒ «eject … (add_fresh_to_graph ? (St_op1 Oid dst r) f ?), ?»
     302    | inr _ ⇒ «eject … (add_fresh_to_graph ? (St_op1 t t (Oid t) dst r) f ?), ?»
    303303    ]
    304304| Cst _ c ⇒ λ_. «add_fresh_to_graph ? (St_const dst c) f ?, ?»
    305 | Op1 _ _ op e' ⇒ λEnv.
     305| Op1 t t' op e' ⇒ λEnv.
    306306    let 〈r,f〉 ≝ choose_reg ? env ? e' f Env in
    307     let f ≝ add_fresh_to_graph ? (St_op1 op dst r) f ? in
     307    let f ≝ add_fresh_to_graph ? (St_op1 t t' op dst r) f ? in
    308308    let f ≝ add_expr ? env ? e' Env r f in
    309309      «eject … f, ?»
  • src/RTLabs/semantics.ma

    r1238 r1369  
    9898      ! locals ← reg_store r v (locals f);
    9999      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
    100   | St_op1 op dst src l ⇒
     100  | St_op1 _ _ op dst src l ⇒
    101101      ! v ← reg_retrieve (locals f) src;
    102       ! v' ← opt_to_res … (msg FailedOp) (eval_unop op v);
     102      ! v' ← opt_to_res … (msg FailedOp) (eval_unop ?? op v);
    103103      ! locals ← reg_store dst v' (locals f);
    104104      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
  • src/RTLabs/syntax.ma

    r1316 r1369  
    1313| St_cost : costlabel → label → statement
    1414| St_const : register → constant → label → statement
    15 | St_op1 : unary_operation → register → register → label → statement (* destination source *)
     15| St_op1 : ∀t,t'. unary_operation t t' → register → register → label → statement (* destination source *)
    1616| St_op2 : binary_operation → register → register → register → label → statement (* destination source1 source2 *)
    1717| St_load : memory_chunk → register → register → label → statement
     
    3131| St_cost _ l ⇒ P l
    3232| St_const _ _ l ⇒ P l
    33 | St_op1 _ _ _ l ⇒ P l
     33| St_op1 _ _ _ _ _ l ⇒ P l
    3434| St_op2 _ _ _ _ l ⇒ P l
    3535| St_load _ _ _ l ⇒ P l
  • src/common/FrontEndOps.ma

    r962 r1369  
    2626  | Oaddrstack: nat → constant.            (**r stack pointer plus the given offset *)
    2727
    28 inductive unary_operation : Type[0] ≝
    29   | Ocastint: signedness → intsize → unary_operation (**r integer casts *)
    30   | Onegint: unary_operation               (**r integer opposite *)
    31   | Onotbool: unary_operation              (**r boolean negation  *)
    32   | Onotint: unary_operation               (**r bitwise complement  *)
    33   | Onegf: unary_operation                 (**r float opposite *)
    34   | Oabsf: unary_operation                 (**r float absolute value *)
    35   | Osingleoffloat: unary_operation        (**r float truncation *)
    36   | Ointoffloat: intsize → unary_operation (**r signed integer to float *)
    37   | Ointuoffloat: intsize → unary_operation (**r unsigned integer to float *)
    38   | Ofloatofint: unary_operation           (**r float to signed integer *)
    39   | Ofloatofintu: unary_operation          (**r float to unsigned integer *)
    40   | Oid: unary_operation                   (**r identity (used to move between registers *)
    41   | Optrofint: region → unary_operation    (**r int to pointer with given representation *)
    42   | Ointofptr: intsize → unary_operation.  (**r pointer to int *)
     28definition boolsrc : typ → Prop ≝ λt. match t with [ ASTint _ _ ⇒ True | ASTptr _ ⇒ True | _ ⇒ False ].
     29
     30inductive unary_operation : typ → typ → Type[0] ≝
     31  | Ocastint: ∀sz,sg,sz',sg'. unary_operation (ASTint sz sg) (ASTint sz' sg')  (**r integer casts *)
     32  | Onegint:  ∀sz,sg. unary_operation (ASTint sz sg) (ASTint sz sg)            (**r integer opposite *)
     33  | Onotbool: ∀t,sz,sg. boolsrc t → unary_operation t (ASTint sz sg)           (**r boolean negation  *)
     34  | Onotint:  ∀sz,sg. unary_operation (ASTint sz sg) (ASTint sz sg)            (**r bitwise complement  *)
     35  | Onegf: ∀sz. unary_operation (ASTfloat sz) (ASTfloat sz)                    (**r float opposite *)
     36  | Oabsf: ∀sz. unary_operation (ASTfloat sz) (ASTfloat sz)                    (**r float absolute value *)
     37  | Osingleoffloat: unary_operation (ASTfloat F64) (ASTfloat F32)              (**r float truncation *)
     38  | Ointoffloat:  ∀fsz,sz. unary_operation (ASTfloat fsz) (ASTint sz Signed)   (**r signed integer to float *)
     39  | Ointuoffloat: ∀fsz,sz. unary_operation (ASTfloat fsz) (ASTint sz Unsigned) (**r unsigned integer to float *)
     40  | Ofloatofint:  ∀fsz,sz. unary_operation (ASTint sz Signed) (ASTfloat fsz)   (**r float to signed integer *)
     41  | Ofloatofintu: ∀fsz,sz. unary_operation (ASTint sz Unsigned) (ASTfloat fsz) (**r float to unsigned integer *)
     42  | Oid: ∀t. unary_operation t t                                               (**r identity (used to move between registers *)
     43  | Optrofint: ∀sz,sg,r. unary_operation (ASTint sz sg) (ASTptr r)             (**r int to pointer with given representation *)
     44  | Ointofptr: ∀sz,sg,r. unary_operation (ASTptr r) (ASTint sz sg).            (**r pointer to int *)
    4345
    4446inductive binary_operation : Type[0] ≝
     
    8890  ]. cases sp // qed.
    8991
    90 definition eval_unop : unary_operation → val → option val ≝
    91 λop,arg.
     92definition eval_unop : ∀t,t'. unary_operation t t' → val → option val ≝
     93λt,t',op,arg.
    9294  match op with
    93   [ Ocastint sg sz
     95  [ Ocastint sz sg sz' sg'
    9496      match sg with
    95       [ Unsigned ⇒ Some ? (zero_ext sz arg)
    96       |   Signed ⇒ Some ? (sign_ext sz arg)
     97      [ Unsigned ⇒ Some ? (zero_ext sz' arg)
     98      |   Signed ⇒ Some ? (sign_ext sz' arg)
    9799      ]
    98   | Onegint ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vint sz1 (two_complement_negation ? n1)) | _ ⇒ None ? ]
    99   | Onotbool ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (of_bool (eq_bv ? n1 (zero ?)))
    100                               | Vptr _ _ _ _ ⇒ Some ? Vfalse
    101                               | Vnull _ ⇒ Some ? Vtrue
    102                               | _ ⇒ None ?
    103                               ]
    104   | Onotint ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vint sz1 (exclusive_disjunction_bv ? n1 (mone ?))) | _ ⇒ None ? ]
    105   | Onegf ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fneg f1)) | _ ⇒ None ? ]
    106   | Oabsf ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fabs f1)) | _ ⇒ None ? ]
     100  | Onegint sz sg ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vint sz1 (two_complement_negation ? n1)) | _ ⇒ None ? ]
     101  | Onotbool t sz sg _ ⇒
     102      match arg with
     103      [ Vint sz1 n1 ⇒ Some ? (Vint sz (if (eq_bv ? n1 (zero ?)) then (repr ? 1) else (zero ?)))
     104      | Vptr _ _ _ _ ⇒ Some ? (Vint sz (zero ?))
     105      | Vnull _ ⇒ Some ? (Vint sz (repr ? 1))
     106      | _ ⇒ None ?
     107      ]
     108  | Onotint sz sg ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vint sz1 (exclusive_disjunction_bv ? n1 (mone ?))) | _ ⇒ None ? ]
     109  | Onegf _ ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fneg f1)) | _ ⇒ None ? ]
     110  | Oabsf _ ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fabs f1)) | _ ⇒ None ? ]
    107111  | Osingleoffloat ⇒ Some ? (singleoffloat arg)
    108   | Ointoffloat sz ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint sz (intoffloat ? f1)) | _ ⇒ None ? ]
    109   | Ointuoffloat sz ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint sz (intuoffloat ? f1)) | _ ⇒ None ? ]
    110   | Ofloatofint ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vfloat (floatofint ? n1)) | _ ⇒ None ? ]
    111   | Ofloatofintu ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vfloat (floatofintu ? n1)) | _ ⇒ None ? ]
    112   | Oid ⇒ Some ? arg (* XXX should we restricted the values allowed? *)
     112  | Ointoffloat _ sz ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint sz (intoffloat ? f1)) | _ ⇒ None ? ]
     113  | Ointuoffloat _ sz ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint sz (intuoffloat ? f1)) | _ ⇒ None ? ]
     114  | Ofloatofint _ _ ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vfloat (floatofint ? n1)) | _ ⇒ None ? ]
     115  | Ofloatofintu _ _ ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vfloat (floatofintu ? n1)) | _ ⇒ None ? ]
     116  | Oid t ⇒ Some ? arg (* XXX should we restricted the values allowed? *)
    113117  (* Only conversion of null pointers is specified. *)
    114   | Optrofint r ⇒ match arg with [ Vint sz1 n1 ⇒ if eq_bv ? n1 (zero ?) then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
    115   | Ointofptr sz ⇒ match arg with [ Vnull _ ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
    116   ].
    117 
     118  | Optrofint sz sg r ⇒ match arg with [ Vint sz1 n1 ⇒ if eq_bv ? n1 (zero ?) then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
     119  | Ointofptr sz sg r ⇒ match arg with [ Vnull _ ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
     120  ].
     121
     122lemma elim_val_typ : ∀v,t. ∀P:val → Prop.
     123val_typ v t →
     124match t with
     125[ ASTint sz sg ⇒ ∀i.P (Vint sz i)
     126| ASTfloat sz ⇒ ∀f.P (Vfloat f)
     127| ASTptr r ⇒ P (Vnull r) ∧ ∀b,c,o. P (Vptr r b c o)
     128] →
     129P v.
     130#v #t #P *
     131[ 1,2: //
     132| #r * //
     133| #r #b #c #o * //
     134] qed.
     135
     136lemma eval_unop_typ_correct : ∀t,t',op,v,v'.
     137  val_typ v t →
     138  eval_unop t t' op v = Some ? v' →
     139  val_typ v' t'.
     140#t #t' #op elim op
     141[ #sz #sg #sz' #sg' #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?)
     142  cases sg whd in ⊢ (??%? → ?) #E' destruct %
     143| #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?) #E' destruct %
     144| #t'' #sz #sg cases t''
     145  [ #sz' #sg' #H #v #v' #H1 @(elim_val_typ … H1) #i whd in ⊢ (??%? → ?) #E' destruct cases (eq_bv ???) whd in ⊢ (?%?) %
     146  | #r #H #v #v' #H1 @(elim_val_typ … H1) whd %
     147    [ whd in ⊢ (??%? → ?) #E'
     148      (* XXX need to normalize or destruct is intractable *)
     149      normalize in E'; destruct (E') ; %
     150    | #b #c #o whd in ⊢ (??%? → ?) #E' destruct %
     151    ]
     152  | #f *
     153  ]
     154| #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?) #E destruct %
     155| #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?) #E destruct %2
     156| #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?) #E destruct %2
     157| #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?) #E destruct %2
     158| #fsz #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?) #E destruct %
     159| #fsz #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?) #E destruct %
     160| #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?) #E destruct %2
     161| #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?) #E destruct %2
     162| #t'' #v #v' #H whd in ⊢ (??%? → ?) #E destruct @H
     163| #sz #sg #r #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?) cases (eq_bv ???)
     164  whd in ⊢ (??%? → ?) #E destruct //
     165| #sz #sg #r #v #v' #H @(elim_val_typ … H) %
     166  [ whd in ⊢ (??%? → ?) #E destruct %
     167  | #b #c #o whd in ⊢ (??%? → ?) #E destruct
     168  ]
     169] qed.
     170 
    118171(* I think this is duplicated somewhere else *)
    119172definition eval_compare_mismatch : comparison → option val ≝
  • src/common/Values.ma

    r1347 r1369  
    4949definition Vtrue: val ≝ Vone I32.
    5050definition Vfalse: val ≝ Vzero I32.
     51
     52inductive val_typ : val → typ → Prop ≝
     53  | VTint: ∀sz,sg,i. val_typ (Vint sz i) (ASTint sz sg)
     54  | VTfloat: ∀sz,f. val_typ (Vfloat f) (ASTfloat sz)
     55  | VTnull: ∀r. val_typ (Vnull r) (ASTptr r)
     56  | VTptr: ∀r,b,c,o. val_typ (Vptr r b c o) (ASTptr r).
    5157
    5258(*
Note: See TracChangeset for help on using the changeset viewer.