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.

File:
1 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;
Note: See TracChangeset for help on using the changeset viewer.