Ignore:
Timestamp:
Jul 12, 2012, 1:28:28 PM (7 years ago)
Author:
campbell
Message:

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r1884 r2176  
    102102definition always_alloc : type → bool ≝
    103103λt. match t with
    104 [ Tarray _ _ _ ⇒ true
     104[ Tarray _ _ ⇒ true
    105105| Tstruct _ _ ⇒ true
    106106| Tunion _ _ ⇒ true
     
    268268(* same gig for AST typs *)
    269269definition typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2).
    270 * [ #sz1 #sg1 | #r1 | #sz1 ]
    271 * [ 1,5,9: | *: #a #b #c try #d @(Error ? (msg TypeMismatch)) ]
     270* [ #sz1 #sg1 | | #sz1 ]
     271* [ 1,5,9: | *: #a #b try #c try #d @(Error ? (msg TypeMismatch)) ]
    272272[ *; cases sz1 [ 1,5,9: | *: #a #b #c @(Error ? (msg TypeMismatch)) ]
    273273  *; cases sg1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
    274 | *; #P #p @(region_should_eq r1 ?? p)
     274| #P #p @(OK ? p)
    275275| *; cases sz1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
    276276] qed.
     
    294294          | _ ⇒ Error ? (msg TypeMismatch)
    295295          ]
    296       | ASTptr r
     296      | ASTptr
    297297          match t' return λt'. res (CMunop ? t') with
    298298          [ ASTint sz' sg' ⇒ OK ? (CMnotbool ????)
     
    323323
    324324(* First, how to get rid of a abstract-away pointer or array type *)
    325 definition fix_ptr_type : ∀r,ty,n. expr (typ_of_type (ptr_type r ty n)) → expr (ASTptr r)
    326 λr,ty,n,e. e⌈expr (typ_of_type (ptr_type r ty n)) ↦ expr (ASTptr r)⌉.
     325definition fix_ptr_type : ∀ty,n. expr (typ_of_type (ptr_type ty n)) → expr ASTptr
     326λty,n,e. e⌈expr (typ_of_type (ptr_type ty n)) ↦ expr ASTptr⌉.
    327327cases n //
    328328qed.
     
    336336| add_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddf sz) e1 e2)
    337337(* XXX we cast up to I16 Signed to prevent overflow, but often we could use I8 *)
    338 | add_case_pi n r ty sz sg ⇒
    339     λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddp I16 r) (fix_ptr_type … e1) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e2) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))))
    340 | add_case_ip n sz sg r ty ⇒
    341     λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddp I16 r) (fix_ptr_type … e2) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e1) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))))
     338| add_case_pi n ty sz sg ⇒
     339    λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddp I16) (fix_ptr_type … e1) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e2) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))))
     340| add_case_ip n sz sg ty ⇒
     341    λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddp I16) (fix_ptr_type … e2) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e1) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))))
    342342| add_default _ _ ⇒ λe1,e2. Error ? (msg TypeMismatch)
    343343].
     
    352352| sub_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Osubf sz) e1 e2)
    353353(* XXX could optimise cast as above *)
    354 | sub_case_pi n r ty sz sg ⇒
    355     λe1,e2. typ_should_eq ??? (Op2 ??? (Osubpi I16 r) (fix_ptr_type … e1) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e2) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))))
     354| sub_case_pi n ty sz sg ⇒
     355    λe1,e2. typ_should_eq ??? (Op2 ??? (Osubpi I16) (fix_ptr_type … e1) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e2) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty))))))
    356356(* XXX check in detail? *)
    357 | sub_case_pp n1 n2 r1 ty1 r2 ty2 ⇒
     357| sub_case_pp n1 n2 ty1 ty2 ⇒
    358358    λe1,e2. match ty' return λty'. res (CMexpr (typ_of_type ty')) with
    359     [ Tint sz sg ⇒ OK ? (Op1 ?? (Ocastint I16 Signed sz sg) (Op2 ??? (Odiv I16) (Op2 ??? (Osubpp I16 r1 r2) (fix_ptr_type … e1) (fix_ptr_type ??? e2)) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty2))))))
     359    [ Tint sz sg ⇒ OK ? (Op1 ?? (Ocastint I16 Signed sz sg) (Op2 ??? (Odiv I16) (Op2 ??? (Osubpp I16) (fix_ptr_type … e1) (fix_ptr_type ?? e2)) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty2))))))
    360360    | _ ⇒ Error ? (msg TypeMismatch)
    361361    ]
     
    432432    | Signed ⇒ λe1,e2. complete_cmp ty' (Op2 ??? (Ocmp … c) e1 e2)
    433433    ]
    434 | cmp_case_pp n r ty ⇒
     434| cmp_case_pp n ty ⇒
    435435    λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpp … c) (fix_ptr_type … e1) (fix_ptr_type … e2))
    436436| cmp_case_ff sz ⇒ λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpf … c) e1 e2)
     
    473473  P t1 v1 →
    474474  P t2 v2.
    475 * [ * * | * | * ]
     475* [ * * | | * ]
    476476* try * try *
    477477#P #v1 #v2 #E whd in E:(??%?); destruct
     
    479479qed.
    480480
    481 lemma unfix_ptr_type : ∀r,ty,n,e.∀P:∀t. expr t → Prop.
    482   P (typ_of_type (ptr_type r ty n)) e →
    483   P (ASTptr r) (fix_ptr_type r ty n e).
    484 #r #ty * [ 2: #n ] #e #P #H @H
     481lemma unfix_ptr_type : ∀ty,n,e.∀P:∀t. expr t → Prop.
     482  P (typ_of_type (ptr_type ty n)) e →
     483  P ASTptr (fix_ptr_type ty n e).
     484#ty * [ 2: #n ] #e #P #H @H
    485485qed.
    486486
     
    503503  | #sz #E1 #E2 #E3 destruct >E3 #E4
    504504    @(typ_equals … E4) % //
    505   | #n #r #ty0 #sz #sg #E1 #E2 #E3 destruct >E3 #E4
    506     @(typ_equals … E4) -E4 -E3 % [ @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H1)| % // ]
    507   | #n #sz #sg #r #ty0 #E1 #E2 #E3 destruct >E3 #E4
    508     @(typ_equals … E4) % [ @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H2)| % // ]
     505  | #n #ty0 #sz #sg #E1 #E2 #E3 destruct >E3 #E4
     506    @(typ_equals … E4) -E4 -E3 % [ @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H1)| % // ]
     507  | #n #sz #sg #ty0 #E1 #E2 #E3 destruct >E3 #E4
     508    @(typ_equals … E4) % [ @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H2)| % // ]
    509509  | #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct
    510510  ]
     
    514514  | #sz #E1 #E2 #E3 destruct >E3 #E4
    515515    @(typ_equals … E4) % //
    516   | #n #r #ty0 #sz #sg #E1 #E2 #E3 destruct >E3 #E4
    517     @(typ_equals … E4) % [ @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H1)| % // ]
    518   | #n1 #n2 #r1 #ty1' #r2 #ty2' #E1 #E2 #E3 destruct >E3
     516  | #n #ty0 #sz #sg #E1 #E2 #E3 destruct >E3 #E4
     517    @(typ_equals … E4) % [ @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H1)| % // ]
     518  | #n1 #n2 #ty1' #ty2' #E1 #E2 #E3 destruct >E3
    519519    whd in ⊢ (??%? → ?); cases ty in e ⊢ %;
    520     [ 2: #sz #sg #e #E4 | 4: #r #ty #e #E4 | 5: #r #ty' #n' #e #E4
     520    [ 2: #sz #sg #e #E4 | 4: #ty #e #E4 | 5: #ty' #n' #e #E4
    521521    | *: normalize #X1 #X2 try #X3 try #X4 destruct
    522522    ] whd in E4:(??%?); destruct % // %
    523     [ @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H1) | @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H2) ]
     523    [ @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H1) | @(unfix_ptr_type ??? (λt,e. expr_vars t e P) H2) ]
    524524  | #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct
    525525  ]
     
    535535| 11,12,13,14,15,16: inversion (classify_cmp ty1 ty2) in ⊢ ?;
    536536  [ 1,5,9,13,17,21: #sz * #E1 #E2 #E3 destruct >E3
    537   | 2,6,10,14,18,22: #n #r #ty' #E1 #E2 #E3 destruct >E3
     537  | 2,6,10,14,18,22: #n #ty' #E1 #E2 #E3 destruct >E3
    538538  | 3,7,11,15,19,23: #sz #E1 #E2 #E3 destruct >E3
    539539  | *: #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); @⊥ destruct
     
    542542  #sz #sg #e #E4
    543543  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)
     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)
    546546  | *: //
    547547  ]
     
    550550
    551551(* We'll need to implement proper translation of pointers if we really do memory
    552    spaces. *)
     552   spaces.
    553553(* This function performs leibniz-style subst if r1 = r2, and fails otherwise. *)
    554554definition check_region : ∀r1:region. ∀r2:region. ∀P:region → Type[0]. P r1 → res (P r2) ≝
     
    566566definition translate_ptr : ∀P,r1,r2. (Σe:CMexpr (ASTptr r1). expr_vars ? e P) → res (Σe':CMexpr (ASTptr r2).expr_vars ? e' P) ≝
    567567λP,r1,r2,e. check_region r1 r2 (λr.Σe:CMexpr (ASTptr r).expr_vars ? e P) e.
    568 
     568*)
    569569axiom FIXME : String.
    570570
     
    577577    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ocastint ? sg1 sz2 ?) e)
    578578    | Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu ?? | _ ⇒ Ofloatofint ??]) e)
    579     | Tpointer r _ ⇒ OK ? (Op1 ?? (Optrofint ?? r) e)
    580     | Tarray r _ _ ⇒ OK ? (Op1 ?? (Optrofint ?? r) e)
     579    | Tpointer _ ⇒ OK ? (Op1 ?? (Optrofint ??) e)
     580    | Tarray _ _ ⇒ OK ? (Op1 ?? (Optrofint ??) e)
    581581    | _ ⇒ Error ? (msg TypeMismatch)
    582582    ]
     
    587587    | _ ⇒ Error ? (msg TypeMismatch)
    588588    ]
    589 | Tpointer r1 _ ⇒ λe. (* will need changed for memory regions *)
     589| Tpointer _ ⇒ λe. (* will need changed for memory regions *)
    590590    match ty2 return λx.res (Σe':CMexpr (typ_of_type x). expr_vars ? e' P) with
    591     [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (Ointofptr sz2 ??) e, ?»
    592     | Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e
    593     | Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e
     591    [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (Ointofptr sz2 ?) e, ?»
     592    | Tarray _ _ ⇒ (*translate_ptr ? r1 r2 e*) OK ? e
     593    | Tpointer _ ⇒ OK ? e
    594594    | _ ⇒ Error ? (msg TypeMismatch)
    595595    ]
    596 | Tarray r1 _ _ ⇒ λe. (* will need changed for memory regions *)
     596| Tarray _ _ ⇒ λe. (* will need changed for memory regions *)
    597597    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
    598     [ Tint sz2 sg2 ⇒ OK ? «Op1 (ASTptr r1) (ASTint sz2 sg2) (Ointofptr sz2 ??) e, ?»
    599     | Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e
    600     | Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e
     598    [ Tint sz2 sg2 ⇒ OK ? «Op1 ASTptr (ASTint sz2 sg2) (Ointofptr sz2 ?) e, ?»
     599    | Tarray _ _ ⇒ OK ? e
     600    | Tpointer _ ⇒ OK ? e
    601601    | _ ⇒ Error ? (msg TypeMismatch)
    602602    ]
     
    642642           *)
    643643          match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with
    644           [ By_value t ⇒ OK ? «Mem t r (Cst ? (Oaddrsymbol r id 0)), ?» (* Mem is "load" in compcert *)
    645           | By_reference r ⇒ OK ? «Cst ? (Oaddrsymbol r id 0), ?»
     644          [ By_value t ⇒ OK ? «Mem t (Cst ? (Oaddrsymbol id 0)), ?» (* Mem is "load" in compcert *)
     645          | By_reference ⇒ OK ? «Cst ? (Oaddrsymbol id 0), ?»
    646646          | By_nothing _ ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    647647          ]
     
    650650           * because its adress was taken somewhere or becauste it's a structured data. *)
    651651          match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with
    652           [ By_value t ⇒ OK ? «Mem t Any (Cst ? (Oaddrstack n)), ?»
    653           | By_reference r ⇒ match r return λr. res (Σe':CMexpr (ASTptr r). ?) with
    654                              [ Any ⇒ OK ? «Cst ? (Oaddrstack n), ?»
     652          [ By_value t ⇒ OK ? «Mem t (Cst ? (Oaddrstack n)), ?»
     653          | By_reference ⇒ (*match r return λr. res (Σe':CMexpr (ASTptr r). ?) with
     654                             [ Any ⇒*) OK ? «Cst ? (Oaddrstack n), ?» (*
    655655                             | _ ⇒ Error  ? [MSG BadlyTypedAccess; CTX ? id]
    656                              ]
     656                             ]*)
    657657          | By_nothing _ ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
    658658          ]
     
    669669      *)
    670670      match typ_of_type (typeof e1) return λx.(Σz:CMexpr x.expr_vars ? z (local_id vars)) → ? with
    671       [ ASTptr r ⇒ λe1'.
     671      [ ASTptr ⇒ λe1'.
    672672          match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with
    673           [ By_value t ⇒ OK ? «Mem t ? (pi1 … e1'), ?»
    674           | By_reference r' ⇒ region_should_eq r r' ? e1'
     673          [ By_value t ⇒ OK ? «Mem t (pi1 … e1'), ?»
     674          | By_reference ⇒ OK ? e1'
    675675          | By_nothing _ ⇒ Error ? (msg BadlyTypedAccess)
    676676          ]
     
    680680      do e1' ← translate_addr vars e1;
    681681      match typ_of_type ty return λx.res (Σz:CMexpr x.?) with
    682       [ ASTptr r ⇒
    683           match e1' with
     682      [ ASTptr ⇒ OK ? e1'
     683(*          match e1' with
    684684          [ mk_DPair r1 e1' ⇒ region_should_eq r1 r ? e1'
    685           ]
     685          ]*)
    686686      | _ ⇒ Error ? (msg TypeMismatch)
    687687      ]
     
    743743      [ Tstruct _ fl ⇒
    744744          do e1' ← translate_addr vars e1;
    745           match e1' with
    746           [ mk_DPair r e1' ⇒
     745(*          match e1' with
     746          [ mk_DPair r e1' ⇒*)
    747747            do off ← field_offset id fl;
    748748            match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with
    749749            [ By_value t ⇒
    750                 OK ? «Mem t r (Op2 ? (ASTint I16 Signed (* XXX efficiency? *)) ?
     750                OK ? «Mem t (Op2 ? (ASTint I16 Signed (* XXX efficiency? *)) ?
    751751                                   (Oaddp …) e1' (Cst ? (Ointconst I16 Signed (repr ? off)))),?»
    752             | By_reference r'
    753                 do e1' ← region_should_eq r r' ? e1';
    754                 OK ? «Op2 (ASTptr r') (ASTint I16 Signed (* XXX efficiency? *)) (ASTptr r')
     752            | By_reference
     753(*                do e1' ← region_should_eq r r' ? e1';*)
     754                OK ? «Op2 ASTptr (ASTint I16 Signed (* XXX efficiency? *)) ASTptr
    755755                        (Oaddp …) e1' (Cst ? (Ointconst I16 Signed (repr ? off))),?»
    756756            | By_nothing _ ⇒ Error ? (msg BadlyTypedAccess)
    757757            ]
    758           ]
    759758      | Tunion _ _ ⇒
    760759          do e1' ← translate_addr vars e1;
    761           match e1' with
    762           [ mk_DPair r e1' ⇒
    763760            match access_mode ty return λt.λ_. res (Σz:CMexpr t.?) with
    764             [ By_value t ⇒ OK ? «Mem t ? e1', ?»
    765             | By_reference r' ⇒ region_should_eq r r' ? e1'
     761            [ By_value t ⇒ OK ? «Mem t e1', ?»
     762            | By_reference ⇒ OK ? e1'
    766763            | By_nothing _ ⇒ Error ? (msg BadlyTypedAccess)
    767764            ]
    768           ]
    769765      | _ ⇒ Error ? (msg BadlyTypedAccess)
    770766      ]
     
    777773
    778774(* Translate addr takes an expression e1, and returns a Cminor code computing the address of the result of [e1].   *)
    779 and translate_addr (vars:var_types) (e:expr) on e : res (𝚺r. Σe':CMexpr (ASTptr r). expr_vars ? e' (local_id vars)) ≝
     775and translate_addr (vars:var_types) (e:expr) on e : res ((*𝚺r.*) Σe':CMexpr ASTptr. expr_vars ? e' (local_id vars)) ≝
    780776match e with
    781777[ Expr ed _ ⇒
     
    783779  [ Evar id ⇒
    784780      do 〈c,t〉 ← lookup' vars id;
    785       match c return λ_. res (𝚺r.Σz:CMexpr (ASTptr r).?) with
    786       [ Global r ⇒ OK ? ❬r, «Cst ? (Oaddrsymbol r id 0), ?»❭
    787       | Stack n ⇒ OK ? ❬Any, «Cst ? (Oaddrstack n), ?»❭
     781      match c return λ_. res (Σz:CMexpr ASTptr.?) with
     782      [ Global r ⇒ OK ? «Cst ? (Oaddrsymbol id 0), ?»
     783      | Stack n ⇒ OK ? «Cst ? (Oaddrstack n), ?»
    788784      | Local ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] (* TODO: could rule out? *)
    789785      ]
    790786  | Ederef e1 ⇒
    791787      do e1' ← translate_expr vars e1;
    792       match typ_of_type (typeof e1) return λx. (Σz:CMexpr x.expr_vars ? z (local_id vars)) → res (𝚺r. Σz:CMexpr (ASTptr r). ?) with
    793       [ ASTptr r ⇒ λe1'.OK ? ❬r, e1'❭
     788      match typ_of_type (typeof e1) return λx. (Σz:CMexpr x.expr_vars ? z (local_id vars)) → res (Σz:CMexpr ASTptr. expr_vars ? z (local_id vars)) with
     789      [ ASTptr ⇒ λe1'.OK ? e1'
    794790      | _ ⇒ λ_.Error ? (msg BadlyTypedAccess)
    795791      ] e1'
     
    799795          do e1' ← translate_addr vars e1;
    800796          do off ← field_offset id fl;
    801           match e1' with
    802           [ mk_DPair r e1'' ⇒ OK (𝚺r:region.Σe:CMexpr (ASTptr r).?)
    803              (❬r, «Op2 (ASTptr r) (ASTint I16 Signed (* FIXME inefficient?*)) (ASTptr r)
    804                      (Oaddp I16 r) e1'' (Cst ? (Ointconst I16 Signed (repr ? off))), ?» ❭)
    805           ]
     797(*          match e1' with
     798          [ mk_DPair r e1'' ⇒ OK (𝚺r:region.Σe:CMexpr (ASTptr r).?)*)
     799             OK ? «Op2 ASTptr (ASTint I16 Signed (* FIXME inefficient?*)) ASTptr
     800                   (Oaddp I16) e1' (Cst ? (Ointconst I16 Signed (repr ? off))), ?»
    806801      | Tunion _ _ ⇒ translate_addr vars e1
    807802      | _ ⇒ Error ? (msg BadlyTypedAccess)
     
    832827inductive destination (vars:var_types) : Type[0] ≝
    833828| IdDest : ∀id,ty. local_id vars id (typ_of_type ty) → destination vars
    834 | MemDest : ∀r:region. (Σe:CMexpr (ASTptr r).expr_vars ? e (local_id vars)) → destination vars.
     829| MemDest : (Σe:CMexpr ASTptr.expr_vars ? e (local_id vars)) → destination vars.
    835830
    836831(* Let a source Clight expression be assign(e1, e2). First of all, observe that [e1] is a
     
    858853          match c return λx.? → ? with
    859854          [ Local ⇒ λE. OK ? (IdDest vars id t ?)
    860           | Global r ⇒ λE. OK ? (MemDest ? r (Cst ? (Oaddrsymbol r id 0)))
    861           | Stack n ⇒ λE. OK ? (MemDest ? Any (Cst ? (Oaddrstack n)))
     855          | Global r ⇒ λE. OK ? (MemDest ? (Cst ? (Oaddrsymbol id 0)))
     856          | Stack n ⇒ λE. OK ? (MemDest ? (Cst ? (Oaddrstack n)))
    862857          ] E
    863858      | _ ⇒
    864859          do e1' ← translate_addr vars e1;
    865           match e1' with [ mk_DPair r e1' ⇒ OK ? (MemDest ? r e1') ]
     860          OK ? (MemDest ? e1')
    866861      ]
    867862  ].
     
    968963    do e2' ← type_should_eq (typeof e2) ty ? e2';
    969964    OK ? «St_assign ? id e2', ?»
    970 | MemDest r e1' ⇒ OK ? «St_store ? r e1' e2', ?»
     965| MemDest e1' ⇒ OK ? «St_store ? e1' e2', ?»
    971966].
    972967% try (//)  try (elim e2' //) elim e1' //
     
    11301125       do e2' ← type_should_eq (typeof e2) ty ? e2';
    11311126       OK ? «〈uv, ul, St_assign ? id e2'〉, ?»
    1132     | MemDest r e1' ⇒
    1133        OK ? «〈uv, ul, St_store ? r e1' e2'〉, ?»
     1127    | MemDest e1' ⇒
     1128       OK ? «〈uv, ul, St_store ? e1' e2'〉, ?»
    11341129    ]
    11351130| Scall ret ef args ⇒
    11361131    do ef' ← translate_expr vars ef;
    1137     do ef' ← typ_should_eq (typ_of_type (typeof ef)) (ASTptr Code) ? ef';
     1132    do ef' ← typ_should_eq (typ_of_type (typeof ef)) ASTptr ? ef';
    11381133    do args' ← mmap_sigma ??? (translate_expr_sigma vars) args;
    11391134    match ret with
     
    11431138        match dest with
    11441139        [ IdDest id ty p ⇒ OK ? «〈uv, ul, St_call (Some ? 〈id,typ_of_type ty〉) ef' args'〉, ?»
    1145         | MemDest r e1' ⇒
     1140        | MemDest e1' ⇒
    11461141            let 〈tmp, uv1〉 as Etmp ≝ alloc_tmp ? (typeof e1) uv in
    1147             OK ? «〈uv1, ul, St_seq (St_call (Some ? 〈tmp,typ_of_type (typeof e1)〉) ef' args') (St_store (typ_of_type (typeof e1)) r e1' (Id ? tmp))〉, ?»
     1142            OK ? «〈uv1, ul, St_seq (St_call (Some ? 〈tmp,typ_of_type (typeof e1)〉) ef' args') (St_store (typ_of_type (typeof e1)) e1' (Id ? tmp))〉, ?»
    11481143        ]
    11491144    ]
     
    12661261try (#l #H elim H)
    12671262try (#size #sign #H assumption)
    1268 try (#region #H assumption)
     1263try (#H1 try #H2 assumption)
    12691264[ 1,5: @(tmp_preserved … p) ]
    12701265[ 1,3: elim e2' | 2,9: elim e1' | 4,7,14: elim ef' ]
     
    12841279       | 2: elim args' // ]
    12851280| 4: @(local_id_fresh_tmp vars tmp uv1 (typeof e1) uv Etmp) ]
    1286 [ 1: #size #sign | 2: #reg | 3: #fsize ]
     1281[ 1: #size #sign | 2: | 3: #fsize ]
    12871282[ 1,2,3: #H @(alloc_tmp_preserves vars tmp uv uv1 … Etmp) @H ]
    12881283try @(match fgens1 return λx.x=fgens1 → ? with
     
    14421437  [ Local ⇒ λE. OK (Σs:(tmpgen vars)×labgen×stmt.?) «result,Is»
    14431438  | Stack n ⇒ λE.
    1444       OK ? «〈fgens1, St_seq (St_store ? Any (Cst ? (Oaddrstack n)) (Id (typ_of_type ty') id)) s〉, ?»
     1439      OK ? «〈fgens1, St_seq (St_store ? (Cst ? (Oaddrstack n)) (Id (typ_of_type ty') id)) s〉, ?»
    14451440  | Global _ ⇒ λE. Error ? [MSG ParamGlobalMixup; CTX ? id]
    14461441  ] E) (OK ? s) params.
Note: See TracChangeset for help on using the changeset viewer.