Changeset 388


Ignore:
Timestamp:
Dec 8, 2010, 11:40:42 AM (9 years ago)
Author:
campbell
Message:

Tidy up some decidability functions.

Location:
C-semantics
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r387 r388  
    686686nqed.
    687687
    688 ndefinition is_not_void : ∀t:type. res (Σu:unit. t ≠ Tvoid) ≝
    689 λt. match t with
    690 [ Tvoid ⇒ Some ? (Error ?)
    691 | _ ⇒ Some ? (OK ??)
    692 ]. nwhd; //; @; #H; ndestruct; nqed.
    693 
    694 ninductive decide : Type ≝
    695 | dy : decide | dn : decide.
    696 
    697 ndefinition dodecide : ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ ¬P ]).P + ¬P.
    698 #P d;ncases d;/2/; nqed.
    699 
    700 ncoercion decide_inject :
    701   ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ ¬P ]).P + ¬P ≝ dodecide
    702   on d:decide to ? + (¬?).
    703 
    704 ndefinition dodecide2 : ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ True ]).res P.
    705 #P d; ncases d; nnormalize; #p; ##[ napply (OK ? p); ##| napply Error ##] nqed.
    706 
    707 ncoercion decide_inject2 :
    708   ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ True ]).res P ≝ dodecide2
    709   on d:decide to res ?.
    710 
    711688alias id "Tint" = "cic:/matita/c-semantics/Csyntax/type.con(0,2,0)".
    712689alias id "Tfloat" = "cic:/matita/c-semantics/Csyntax/type.con(0,3,0)".
     
    794771
    795772nlet rec is_is_call_cont (k:cont) : (is_call_cont k) + (¬is_call_cont k) ≝
    796 match k with
    797 [ Kstop ⇒ dy
    798 | Kcall _ _ _ _ ⇒ dy
    799 | _ ⇒ dn
    800 ]. nwhd; //; @; #H; nelim H; nqed.
    801 
    802 nlet rec is_Sskip (s:statement) : (s = Sskip) + (s ≠ Sskip) ≝
    803 match s with
    804 [ Sskip ⇒ dy
    805 | _ ⇒ dn
    806 ].
    807 ##[ //;
    808 ##| ##*: @; #H; ndestruct;
    809 ##] nqed.
     773match k return λk'.(is_call_cont k') + (¬is_call_cont k') with
     774[ Kstop ⇒ ?
     775| Kcall _ _ _ _ ⇒ ?
     776| _ ⇒ ?
     777].
     778##[ ##1,8: @1; //
     779##| ##*: @2; /2/
     780##] nqed.
     781
     782ndefinition is_Sskip : ∀s:statement. (s = Sskip) + (s ≠ Sskip) ≝
     783λs.match s return λs'.(s' = Sskip) + (s' ≠ Sskip) with
     784[ Sskip ⇒ inl ?? (refl ??)
     785| _ ⇒ inr ?? (nmk ? (λH.?))
     786]. ndestruct;
     787nqed.
    810788
    811789(* Checking types of values given to / received from an external function call. *)
     
    897875    ! fd ← find_funct ? ? ge vf;
    898876    ! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (typeof a));
    899 (*
     877(* requires associativity of IOMonad, so rearrange it below
    900878    ! k' ← match lhs with
    901879         [ None ⇒ ret ? (Kcall (None ?) f e k)
     
    988966      ]
    989967    | Some a ⇒
    990         ! u ← err_to_io_sig … (is_not_void (fn_return f));
    991         ! 〈v,tr〉 ← exec_expr ge e m a;
    992         ret ? 〈tr, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉
     968        match type_eq_dec (fn_return f) Tvoid with
     969        [ inl _ ⇒ Wrong ???
     970        | inr _ ⇒
     971          ! 〈v,tr〉 ← exec_expr ge e m a;
     972          ret ? 〈tr, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉
     973        ]
    993974    ]
    994975  | Sswitch a sl ⇒
     
    11401121    ##[ nwhd; nlapply (refl ? (fn_return f)); ncases (fn_return f) in ⊢ (???% → %); //; #H;
    11411122        napply step_return_0; napply H;
    1142     ##| #ex; napply sig_bindIO_OK; #u Hnotvoid;
     1123    ##| #ex; ncases (type_eq_dec (fn_return f) Tvoid); //; nwhd in ⊢ (% → ?????%); #Hnotvoid;
    11431124        napply res_bindIO2_OK; #v tr Hv;
    11441125        nwhd; napply (step_return_1 … Hnotvoid (exec_expr_sound' … Hv));
  • C-semantics/CexecIOcomplete.ma

    r387 r388  
    325325##] nqed.
    326326
    327 nlemma is_not_void_true: ∀f. ¬fn_return f = Tvoid → ∃p. is_not_void (fn_return f) = OK ? p.
    328 #f; ncases f; #ty; #_; #_; #_; ncases ty;
    329 ##[ #H; napply False_ind; /2/;
    330 ##| #sz sg e; @ ?; //; ##| #sz e; @ ?; // ##| #sp ty e; @ ?; // ##| #sp ty n e; @ ?; // ##|
    331     #tys ty e; @ ?; // ##| #id fs e; @ ?; // ##| #id fs e; @ ?; // ##| #id e; @ ?; // ##]
    332 nqed.
    333 
    334327nlemma alloc_vars_complete: ∀env,m,l,env',m'.
    335328  alloc_variables env m l env' m' →
     
    368361    nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?);
    369362    napply refl;
    370 ##] nqed.   
    371 
     363##] nqed.
     364
     365nlemma dec_true: ∀P:Prop.∀f:P + ¬P.∀p:P.∀Q:(P + ¬P) → Prop. (∀p'.Q (inl ?? p')) → Q f.
     366#P f p Q H; ncases f;
     367##[ napply H
     368##| #np; napply False_ind; napply (absurd ? p np);
     369##] nqed.
     370
     371nlemma dec_false: ∀P:Prop.∀f:P + ¬P.∀p:¬P.∀Q:(P + ¬P) → Prop. (∀p'.Q (inr ?? p')) → Q f.
     372#P f p Q H; ncases f;
     373##[ #np; napply False_ind; napply (absurd ? np p);
     374##| napply H
     375##] nqed.
    372376
    373377ntheorem step_complete: ∀ge,s,tr,s'.
     
    436440##| #f k env m H; nwhd in ⊢ (??%?); nrewrite > H; napply refl;
    437441##| #f e k env m v tr H1 H2; nwhd in ⊢ (??%?);
    438     nelim (is_not_void_true f H1); #pf ef; nrewrite > ef; nwhd in ⊢ (??%?);
     442    napply (dec_false ? (type_eq_dec (fn_return f) Tvoid) H1); #pf';
     443    nwhd in ⊢ (??%?);
    439444    nrewrite > (yieldsbare_eq ??? (expr_complete … H2)); nwhd in ⊢ (??%?);
    440445    napply refl;
     
    552557  nwhd in ⊢ (???%);
    553558  ##[ ncases a; ##[ ncases (fn_return f); //; ##| #e; nwhd nodelta in ⊢ (???%);
    554                     napply err_sig_does_not_interact; #x; napply err2_does_not_interact; // ##]
     559                    ncases (type_eq_dec (fn_return f) Tvoid); #x; //; napply err2_does_not_interact; // ##]
    555560  ##| ncases (find_label a (fn_body f) (call_cont kk)); ##[ napply I ##| #z; ncases z; #x y; napply I ##]
    556561  ##| napply err2_does_not_interact; #x1 x2; napply err2_does_not_interact; #x3 x4; napply opt_does_not_interact; #x5; napply I
Note: See TracChangeset for help on using the changeset viewer.