Ignore:
Timestamp:
Nov 15, 2012, 6:12:57 PM (8 years ago)
Author:
garnier
Message:

Floats are gone from the front-end. Some trace amount might remain in RTL/RTLabs, but this should be easily fixable.
Also, work-in-progress in Clight/memoryInjections.ma

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/Clight/toCminor.ma

    r2465 r2468  
    268268(* same gig for AST typs *)
    269269definition typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2).
    270 * [ #sz1 #sg1 | | #sz1 ]
    271 * [ 1,5,9: | *: #a #b try #c try #d @(Error ? (msg TypeMismatch)) ]
    272 [ *; cases sz1 [ 1,5,9: | *: #a #b #c @(Error ? (msg TypeMismatch)) ]
    273   *; cases sg1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
    274 | #P #p @(OK ? p)
    275 | *; cases sz1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
    276 ] qed.
     270* [ #sz1 #sg1 | ]
     271* try /2 by Error/
     272qed.
    277273
    278274alias id "CLunop" = "cic:/matita/cerco/Clight/Csyntax/unary_operation.ind(1,0,0)".
    … …  
    309305      match t' return λt'. res (CMunop t t') with
    310306      [ ASTint sz sg ⇒ typ_should_eq ?? (λt.CMunop t (ASTint ??)) (Onegint sz sg)
    311       | ASTfloat sz ⇒ typ_should_eq ?? (λt.CMunop t (ASTfloat sz)) (Onegf sz)
     307    (*  | ASTfloat sz ⇒ typ_should_eq ?? (λt.CMunop t (ASTfloat sz)) (Onegf sz) *)
    312308      | _ ⇒ Error ? (msg TypeMismatch)
    313309      ]
    … …  
    334330match classify_add ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
    335331[ add_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oadd ??) e1 e2)
    336 | add_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddf sz) e1 e2)
     332(*| add_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddf sz) e1 e2) *)
    337333(* XXX we cast up to I16 Signed to prevent overflow, but often we could use I8 *)
    338334| add_case_pi n ty sz sg ⇒
    … …  
    350346match classify_sub ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
    351347[ sub_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Osub ??) e1 e2)
    352 | sub_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Osubf sz) e1 e2)
     348(* | sub_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Osubf sz) e1 e2) *)
    353349(* XXX could optimise cast as above *)
    354350| sub_case_pi n ty sz sg ⇒
    … …  
    369365match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with
    370366[ aop_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omul …) e1 e2)
    371 | aop_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omulf …) e1 e2)
     367(* | aop_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omulf …) e1 e2) *)
    372368| aop_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
    373369].
    … …  
    383379    | Signed ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Odiv …) e1 e2)
    384380    ]
    385 | aop_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Odivf …) e1 e2)
     381(* | aop_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Odivf …) e1 e2) *)
    386382| aop_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
    387383].
    … …  
    434430| cmp_case_pp n ty ⇒
    435431    λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpp … c) (fix_ptr_type … e1) (fix_ptr_type … e2))
    436 | cmp_case_ff sz ⇒ λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpf … c) e1 e2)
     432(* | cmp_case_ff sz ⇒ λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpf … c) e1 e2) *)
    437433| cmp_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch)
    438434].
    … …  
    473469  P t1 v1 →
    474470  P t2 v2.
    475 * [ * * | | * ]
    476 * try * try *
     471* [ #sz #sg | ]
     472* [ 1,3: * * ]
    477473#P #v1 #v2 #E whd in E:(??%?); destruct
    478 #H @H
    479474qed.
    480475
    … …  
    501496  [ #sz #sg #E1 #E2 #E3 destruct >E3 #E4 -E3 change with (typ_should_eq ???? = OK ??) in E4;
    502497    @(typ_equals … E4) % //
    503   | #sz #E1 #E2 #E3 destruct >E3 #E4
    504     @(typ_equals … E4) % //
     498(*  | #sz #E1 #E2 #E3 destruct >E3 #E4
     499    @(typ_equals … E4) % // *)
    505500  | #n #ty0 #sz #sg #E1 #E2 #E3 destruct >E3 #E4
    506501    @(typ_equals … E4) -E4 -E3 % [ @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H1)| % // ]
    … …  
    509504  | #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct
    510505  ]
     506 
    511507| inversion (classify_sub ty1 ty2) in ⊢ ?;
    512508  [ #sz #sg #E1 #E2 #E3 destruct >E3 #E4
    513509    @(typ_equals … E4) % //
    514   | #sz #E1 #E2 #E3 destruct >E3 #E4
    515     @(typ_equals … E4) % //
     510(*  | #sz #E1 #E2 #E3 destruct >E3 #E4
     511    @(typ_equals … E4) % // *)
    516512  | #n #ty0 #sz #sg #E1 #E2 #E3 destruct >E3 #E4
    517513    @(typ_equals … E4) % [ @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H1)| % // ]
    518514  | #n1 #n2 #ty1' #ty2' #E1 #E2 #E3 destruct >E3
    519515    whd in ⊢ (??%? → ?); cases ty in e ⊢ %;
    520     [ 2: #sz #sg #e #E4 | 4: #ty #e #E4 | 5: #ty' #n' #e #E4
     516    [ 2: #sz #sg #e #E4 | 3: #ty #e #E4 | 4: #ty' #n' #e #E4
    521517    | *: normalize #X1 #X2 try #X3 try #X4 destruct
    522518    ] whd in E4:(??%?); destruct % // %
    … …  
    526522| 3,4,5,6,7,8,9,10: inversion (classify_aop ty1 ty2) in ⊢ ?;
    527523  (* Note that some cases require a split on signedness of integer type. *)
    528   [ 1,4,7,10,13,16,19,22: #sz * #E1 #E2 #E3 destruct >E3 #E4
     524  [ 1,3,5,7,9,11,13,15: #sz * #E1 #E2 #E3 destruct >E3 #E4
    529525    @(typ_equals … E4) % //
    530   | 2,5: #sz #E1 #E2 #E3 destruct >E3 #E4
    531     @(typ_equals … E4) % //
    532   | 8,11,14,17,20,23: #sz #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct
    533   | 3,6,9,12,15,18,21,24: #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct
     526  | 2,4,6,8,10,12,14,16,18: #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct
    534527  ]
    535 | 11,12,13,14,15,16: inversion (classify_cmp ty1 ty2) in ⊢ ?;
    536   [ 1,5,9,13,17,21: #sz * #E1 #E2 #E3 destruct >E3
    537   | 2,6,10,14,18,22: #n #ty' #E1 #E2 #E3 destruct >E3
    538   | 3,7,11,15,19,23: #sz #E1 #E2 #E3 destruct >E3
     528| *: inversion (classify_cmp ty1 ty2) in ⊢ ?;
     529  [ 1,4,7,10,13,16: #sz * #E1 #E2 #E3 destruct >E3
     530  | 2,5,8,11,14,17: #n #ty' #E1 #E2 #E3 destruct >E3
    539531  | *: #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); @⊥ destruct
    540   ] whd in ⊢ (??%? → ?); cases ty in e ⊢ %;
     532  ] whd in ⊢ (??%? → ?); cases ty in e ⊢ %; normalize nodelta
    541533  try (normalize #X1 #X2 try #X3 try #X4 try #X5 destruct #FAIL)
    542534  #sz #sg #e #E4
    543   whd in E4:(??%?); destruct %
    544   [ 25,27,29,31,33,35: @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H1)
    545   | 26,28,30,32,34,36: @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H2)
    546   | *: //
    547   ]
    548 ] qed.
    549 
     535  whd in E4:(??%?); destruct % try @H1 try @H2
     536  try  @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H1)
     537  try  @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H2)
     538] qed. 
    550539
    551540(* We'll need to implement proper translation of pointers if we really do memory
    … …  
    576565    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
    577566    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ocastint ? sg1 sz2 ?) e)
    578     | Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu ?? | _ ⇒ Ofloatofint ??]) e)
     567  (*  | Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu ?? | _ ⇒ Ofloatofint ??]) e)*)
    579568    | Tpointer _ ⇒ OK ? (Op1 ?? (Optrofint ??) e)
    580569    | Tarray _ _ ⇒ OK ? (Op1 ?? (Optrofint ??) e)
    581570    | _ ⇒ Error ? (msg TypeMismatch)
    582571    ]
    583 | Tfloat sz1 ⇒ λe.
     572(* | Tfloat sz1 ⇒ λe.
    584573    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
    585574    [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat ? sz2 | _ ⇒ Ointoffloat ? sz2 ]) e, ?»
    586575    | Tfloat sz2 ⇒ Error ? (msg FIXME) (* OK ? «Op1 ?? (Oid ?) e, ?» (* FIXME *) *)
    587576    | _ ⇒ Error ? (msg TypeMismatch)
    588     ]
     577    ] *)
    589578| Tpointer _ ⇒ λe. (* will need changed for memory regions *)
    590579    match ty2 return λx.res (Σe':CMexpr (typ_of_type x). expr_vars ? e' P) with
    … …  
    626615      | _ ⇒ Error ? (msg TypeMismatch)
    627616      ]
    628   | Econst_float f ⇒
     617 (* | Econst_float f ⇒
    629618      match ty return λty. res (Σe':CMexpr (typ_of_type ty). ?) with
    630619      [ Tfloat sz ⇒ OK ? «Cst ? (Ofloatconst sz f), ?»
    631620      | _ ⇒ Error ? (msg TypeMismatch)
    632       ]
     621      ] *)
    633622  | Evar id ⇒
    634623      do 〈c,t〉 as E ← lookup' vars id; (* E is an equality proof of the shape "lookup' vars id = Ok <c,t>" *)
    … …  
    676665          ]
    677666      | _ ⇒ λ_. Error ? (msg TypeMismatch)
    678       ] e1'
     667      ] e1'             
    679668  | Eaddrof e1 ⇒
    680669      do e1' ← translate_addr vars e1;
    … …  
    716705      [ Tint sz sg ⇒
    717706        do e2' ← type_should_eq ? (Tint sz sg) (λx.Σe:CMexpr (typ_of_type x).?) e2';
    718         match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → res ? with
     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
    719708        [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' (Cst ? (Ointconst sz sg (zero ?))), ?»
    720709        | _ ⇒ λ_.Error ? (msg TypeMismatch)
    721710        ] e1'
    722711      | _ ⇒ Error ? (msg TypeMismatch)
    723       ]
     712      ]     
    724713  | Eorbool e1 e2 ⇒
    725714      do e1' ← translate_expr vars e1;
    … …  
    728717      [ Tint sz sg ⇒
    729718        do e2' ← type_should_eq ? (Tint sz sg) (λx.Σe:CMexpr (typ_of_type x).?) e2';
    730         match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → ? with
     719        match typ_of_type (typeof e1)
     720        return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → ? with
    731721        [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' (Cst ? (Ointconst sz sg (repr ? 1))) e2', ?»
    732         | _ ⇒ λ_.Error ? (msg TypeMismatch)
     722        | _ ⇒ λ_. Error ? (msg TypeMismatch)
    733723        ] e1'
    734724      | _ ⇒ Error ? (msg TypeMismatch)
    735       ]
     725      ]     
    736726  | Esizeof ty1 ⇒
    737727      match ty return λty. res (Σe':CMexpr (typ_of_type ty). ?) with
    738728      [ Tint sz sg ⇒ OK ? «Cst ? (Ointconst sz sg (repr ? (sizeof ty1))), ?»
    739729      | _ ⇒ Error ? (msg TypeMismatch)
    740       ]
     730      ]     
    741731  | Efield e1 id ⇒
    742732      match typeof e1 with
    … …  
    764754            ]
    765755      | _ ⇒ Error ? (msg BadlyTypedAccess)
    766       ]
     756      ]           
    767757  | Ecost l e1 ⇒
    768758      do e1' ← translate_expr vars e1;
    769759      do e' ← OK ? «Ecost ? l e1',?»;
    770       typ_should_eq (typ_of_type (typeof e1)) (typ_of_type ty) (λx.Σe:CMexpr x.?) e'
     760      typ_should_eq (typ_of_type (typeof e1)) (typ_of_type ty) (λx.Σe:CMexpr x.?) e'     
    771761  ]
    772762]
Note: See TracChangeset for help on using the changeset viewer.