Changeset 3544 for LTS


Ignore:
Timestamp:
Mar 19, 2015, 4:55:46 PM (5 years ago)
Author:
pellitta
Message:

record semantico: abitato eval_call

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/imp.ma

    r3543 r3544  
    174174  (* syntactical record *)
    175175
     176definition DeqExpr:DeqSet≝(mk_DeqSet expr expr_eq expr_eq_equality).
     177
    176178definition imp_instr_params: instr_params ≝ mk_instr_params ? ? ? ? ? ?.
    177179[@(mk_DeqSet seq_i seq_i_eq seq_i_eq_equality)
     
    179181|@(mk_DeqSet cond_i cond_i_eq cond_i_eq_equality)
    180182|@(mk_DeqSet loop_i loop_i_eq loop_i_eq_equality)
    181 |@(mk_DeqSet expr expr_eq expr_eq_equality)
     183|@DeqExpr
    182184|@(mk_DeqSet expr expr_eq expr_eq_equality)].qed.
    183185
     
    336338
    337339
    338 definition imp_env_params:env_params≝mk_env_params environment.
     340definition imp_env_params:env_params≝mk_env_params variable.
    339341
    340342let rec env_eq (env1:environment) (env2:environment):bool≝match env1 with
     
    425427*)
    426428
     429
     430
    427431definition imp_eval_loop_cond:(loop_instr imp_state_params)→ (store_type imp_state_params)→ option (bool × (store_type imp_state_params))≝imp_eval_cond_cond.
    428432(*λl,s.match l with
    429433[lWhile g l⇒ match (sem_condition g) with [None ⇒ None ?|Some b⇒ Some ? (mk_Prod b s)]].*)
     434
     435definition imp_eval_call:(signature imp_state_params imp_state_params)→ DeqExpr→ imp_store→ (option imp_store)≝
     436λsgn,e,st.match sgn with [mk_signature fun fpt rt ⇒ match st with
     437  [nil ⇒ None ?
     438  |cons hd tl⇒ match hd with
     439    [mk_Prod env v ⇒ match (sem_expr env e) with
     440      [None ⇒ None ?
     441      |Some n⇒ Some ? (cons ? (mk_Prod … (assign default_env fpt n) v) st)
     442      ]
     443    ]
     444  ]
     445].
    430446
    431447definition imp_sem_state_params : sem_state_params imp_state_params ≝ mk_sem_state_params … imp_eval_seq imp_eval_io
Note: See TracChangeset for help on using the changeset viewer.