Changeset 3545 for LTS


Ignore:
Timestamp:
Mar 19, 2015, 5:44:48 PM (5 years ago)
Author:
pellitta
Message:

risolto un problema di mismatch di tipo legato al fatto che lo store precedentemente era un ambiente e non uno stack di coppie ambiente variabile di ritorno

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/imp.ma

    r3544 r3545  
    394394] qed.
    395395
    396 
    397396(* store is actually a stack of pairs 〈environment, return-variable〉 *)
    398 definition imp_store:Type[0]≝mk_DeqSet store_t store_eq store_eq_equality.
    399 
    400 definition imp_state_params:state_params≝mk_state_params imp_instr_params imp_env_params DeqEnv.
     397definition imp_store:DeqSet≝mk_DeqSet store_t store_eq store_eq_equality.
     398
     399definition imp_state_params:state_params≝mk_state_params imp_instr_params imp_env_params imp_store (*DeqEnv*).
     400
     401definition current_env:store_type imp_state_params→ option environment≝λs.match s with [nil⇒ None ?
     402|cons hd tl⇒ match hd with [(mk_Prod env var)⇒ Some ? env]].
    401403
    402404definition imp_eval_seq:(seq_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝λi,s.match i with
    403405[sNop ⇒ Some ? s
    404 |sAss v e ⇒ match (sem_expr s e) with [None ⇒ None ?| Some n⇒ Some ? (assign s v n)]
    405 |sInc v ⇒ match (read s v) with [None ⇒ None ?|Some n⇒ Some ? (assign s v (S n))]
     406|sAss v e ⇒ match s with
     407  [nil⇒ None ?
     408  |cons hd tl⇒ match hd with
     409    [(mk_Prod env var) ⇒ match (sem_expr env e) with
     410      [None ⇒ None ?
     411      | Some n⇒ Some ? (cons ? (mk_Prod ? ? (assign env v n) var) tl)
     412      ]
     413    ]
     414  ]
     415|sInc v ⇒ match s with [nil⇒ None ?|cons hd tl⇒ match hd with [(mk_Prod env var)⇒
     416match (read env v) with [None ⇒ None ?|Some n⇒ Some ? (cons ? (mk_Prod ? ? (assign env v (S n)) var) tl)]]]
    406417].
    407418
     
    410421
    411422definition imp_eval_cond_cond:(cond_instr imp_state_params)→ (store_type imp_state_params)→ option (bool × (store_type imp_state_params))≝λc,s.match c with
    412 [Eq e1 e2⇒ match (sem_expr s e1) with
    413   [None⇒ None ?
    414   |Some n ⇒ match (sem_expr s e2) with
     423[Eq e1 e2⇒ match (current_env s) with
     424  [None ⇒ None ?
     425  |Some env⇒ match (sem_expr env e1) with
     426    [None⇒ None ?
     427    |Some n ⇒ match (sem_expr env e2) with
     428      [None ⇒ None ?
     429      |Some m ⇒ Some ? (mk_Prod ?? (eqb n m) s)]
     430    ]
     431  ]
     432|Not e ⇒ match (current_env s) with
     433  [None ⇒ None ?
     434  |Some env⇒ match (sem_condition env e) with
    415435    [None ⇒ None ?
    416     |Some m ⇒ Some ? (mk_Prod ?? (eqb n m) s)]
    417   ]
    418 |Not e ⇒ match (sem_condition s e) with [None ⇒ None ?|Some b ⇒ Some ? (mk_Prod ?? b s)]
     436    |Some b ⇒ Some ? (mk_Prod ?? b s)
     437    ]
     438  ]
    419439].
    420440
     
    433453[lWhile g l⇒ match (sem_condition g) with [None ⇒ None ?|Some b⇒ Some ? (mk_Prod b s)]].*)
    434454
    435 definition imp_eval_call:(signature imp_state_params imp_state_params)→ DeqExpr→ imp_store→ (option imp_store)≝
     455definition imp_eval_call:(signature imp_state_params imp_state_params)→ expr→ imp_store→ (option imp_store)≝
    436456λsgn,e,st.match sgn with [mk_signature fun fpt rt ⇒ match st with
    437457  [nil ⇒ None ?
     
    445465].
    446466
    447 definition imp_sem_state_params : sem_state_params imp_state_params ≝ mk_sem_state_params imp_eval_seq imp_eval_io
    448 imp_eval_cond_cond imp_eval_loop_cond ….
     467definition imp_sem_state_params : sem_state_params imp_state_params ≝ mk_sem_state_params imp_state_params imp_eval_seq imp_eval_io
     468imp_eval_cond_cond imp_eval_loop_cond imp_eval_call ….
    449469
    450470
Note: See TracChangeset for help on using the changeset viewer.