Changeset 388 for C-semantics/CexecIO.ma


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

Tidy up some decidability functions.

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