Changeset 3579 for LTS/Language.ma


Ignore:
Timestamp:
Jul 10, 2015, 4:08:09 PM (4 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3576 r3579  
    348348  eq_instructions … (code … st) (EMPTY …) ∧
    349349  eqb_list … (cont … st) [〈spec_act,(main … prog)〉 ; 〈spec_act,EMPTY …〉] ∧
    350   store … st == init_store … p' ∧ io_info … st.
     350  store … st == init_store … p' ∧
     351  io_info … st.
    351352
    352353definition lang_final : ∀p.state p → bool ≝
     
    354355 eq_instructions … (code … st) (EMPTY …) ∧ isnilb … (cont … st).
    355356
     357definition lang_classify : ∀p.state p → ? ≝
     358(λp,s.match (code … s) with
     359                    [ COND _ _ _ _ _ _ ⇒ cl_jump
     360                    | LOOP _ _ _ _ _ ⇒ cl_jump
     361                    | EMPTY ⇒ if io_info … s then cl_io else cl_other
     362                    | _ ⇒ cl_other
     363                    ]).
     364                   
    356365definition operational_semantics : ∀p : state_params.sem_state_params p → Program p p p → abstract_status p ≝
    357366λp,p',prog.mk_abstract_status ?
     
    359368                (execute_l ? p' (env … prog))
    360369                (is_synt_succ …)
    361                 (λs.match (code … s) with
    362                     [ COND _ _ _ _ _ _ ⇒ cl_jump
    363                     | LOOP _ _ _ _ _ ⇒ cl_jump
    364                     | EMPTY ⇒ if io_info … s then cl_io else cl_other
    365                     | _ ⇒ cl_other
    366                     ])
     370                (lang_classify p)
    367371                (λs.match (code … s) with
    368372                    [CALL _ _ m _ ⇒ match m with [ Some _ ⇒ true | None ⇒ false ]
     
    393397 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10
    394398 ]
    395  #_ destruct >EQcode in H; normalize nodelta /2 by ex_intro/
     399 #_ destruct whd in match lang_classify in H ⊢ %; normalize nodelta in H ⊢ %;
     400 >EQcode in H; whd in match lang_classify; normalize nodelta /2 by ex_intro/
    396401 [ cases(io_info ??) normalize nodelta] #EQ destruct
    397402| #s1 #s2 #l #H #H1 inversion H1 #st #st'
     
    415420 | #EQ1 #EQ2 #EQ3 #EQiost' #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10
    416421 ]
    417  #_ destruct
    418  cases(code ? st') in H; normalize nodelta >EQiost' normalize nodelta
     422 #_ destruct whd in match lang_classify in H ⊢ %; normalize nodelta in H ⊢ %;
     423 cases(code ? st') in H; whd in match lang_classify; normalize nodelta >EQiost' normalize nodelta
    419424 #eq destruct try (#eq1 destruct) try (#eq2 destruct) try (#eq3 destruct)
    420425 try (#eq4 destruct) try (#eq5 destruct) try (#eq6 destruct) %{lin} %
     
    439444 | #EQ1 #EQ2 #EQiost #EQiost' #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10
    440445 ]
    441  #_ destruct >EQcode in H; normalize nodelta [|*: #EQ destruct]
     446 #_ destruct whd in match lang_classify in H ⊢ %; normalize nodelta in H ⊢ %;
     447 >EQcode in H; normalize nodelta [|*: #EQ destruct]
    442448 cases(io_info … st) in x; normalize nodelta [2: #_ #EQ destruct]
    443449 #H3 #_ @H3 %
Note: See TracChangeset for help on using the changeset viewer.