Changeset 3575


Ignore:
Timestamp:
Jun 19, 2015, 12:00:22 AM (6 years ago)
Author:
piccolo
Message:
 
Location:
LTS
Files:
7 edited

Legend:

Unmodified
Added
Removed

  • LTS/frame_variable_pass.ma

    r3573 r3575  
    3737 λi,map.
    3838  match i with
    39   [ sNop ⇒ Seq_i sNop
    40   | sAss v e ⇒ Seq_i (sAss (map v) (map_exp e map))
     39  [ sAss v e ⇒ Seq_i (sAss (map v) (map_exp e map))
    4140  ].
    4241
    … …  
    200199    frame_assign_var 〈frame::frames,fpsp〉 (m v) val = Some … st2' ∧
    201200     store_rel m st2 st2'.
     201     cases daemon (* si è rotto!!!
    202202 #m #env #var #tl #v #val #frame #frames #st2 #fpsp #Rel1 #Rel2
    203203 whd in ⊢ (??%? → ?); #EQ destruct
    204204 whd in match frame_assign_var; normalize nodelta % [2: % [%] | skip]
    205  cases Rel1 -Rel1 #Rel3 #Rel4 destruct % // whd /6/
     205 cases Rel1 -Rel1 #Rel3 #Rel4 destruct % // whd /6/ *)
    206206qed.
    207207

  • LTS/imp.ma

    r3560 r3575  
    1313(**************************************************************************)
    1414
    15 include "basics/lists/list.ma".
    16 include "arithmetics/nat.ma".
    17 include "basics/bool.ma".
    1815include "Language.ma".
    19 include "basics/finset.ma".
     16
    2017
    2118(* Syntax *)
    … …  
    3330 | Not: condition → condition.
    3431
    35 let rec expr_eq (e1:expr) (e2:expr):bool≝
    36 match e1 with [Var v1⇒ match e2 with [Var v2⇒ v1==v2|_⇒ false]
    37 |Const v1⇒ match e2 with [Const v2⇒ v1==v2|_⇒ false]
     32let rec expr_eq (e1:expr) (e2:expr) on e1 :bool≝
     33match e1 with [Var v1⇒ match e2 with [Var v2⇒ eqb v1 v2|_⇒ false]
     34|Const v1⇒ match e2 with [Const v2⇒ eqb v1 v2|_⇒ false]
    3835|Plus le1 re1 ⇒ match e2 with [Plus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false]
    3936|Minus le1 re1 ⇒ match e2 with [Minus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false]
    4037].
    4138
    42 lemma expr_eq_refl:∀e:expr.expr_eq e e=true.
    43 #e elim e [1,2: #v whd in match (expr_eq ? ?); /2 by /
    44 (*change with (v==v = true); @(\b ?) %*)
    45 |3,4: #f1 #f2 normalize #H1 >H1 #H2 >H2 %]qed.
    46 
    47   (* the predicate expr_eq corresponds to syntactical equality on the type expr *)
    48 
    49 lemma expr_eq_equality:∀e1,e2:expr.expr_eq e1 e2=true ↔ e1=e2.
    50 #e1 #e2 % [2:* lapply e2 -e2 elim e1
    51   [1,2:#n #_ (*change with (n==n = true) @(\b ?) %*)
    52   |3,4:#f1 #f2 #H1 #H2 #e2] @expr_eq_refl
    53 |lapply e2 -e2 elim e1
    54   [1,2: #v1 *
    55     [1,6: #v2 #H >(\P H) %
    56     |2,5: #v2 whd in ⊢((??%?)→ ?); #ABS destruct
    57     |3,4,7,8: #e #f whd in ⊢((??%?)→ ?); #ABS destruct]
    58   |3,4: #e #e2 #H #K *
    59     [1,2,5,6: #v2 normalize #ABS destruct
    60     |3,4,7,8:#f1 #f2 normalize inversion(expr_eq e f1) #INV1 >INV1 inversion(expr_eq e2 f2)
    61     #INV2 >INV2 normalize #T destruct >(H ? INV1) >(K ? INV2) % qed.
    62 
    63 
    64 
    65 
     39lemma expr_eq_elim : ∀P : bool → Prop.∀e1,e2.(e1 = e2 → P true) → (e1 ≠ e2 → P false) → P (expr_eq e1 e2).
     40#P #e1 lapply P -P elim e1 -e1
     41[1,2: #v #P * [1,5: #v' |2,6: #v' |*: #e1 #e2 ] #H1 #H2 normalize try(@H2 % #EQ destruct) @(eqb_elim v v')
     42  [1,3: #EQ destruct @H1 % |*: * #H @H2 % #EQ destruct @H %]
     43|*: #e1 #e2 #IH1 #IH2 #P * [1,5: #v' |2,6: #v' |*: #e1' #e2' ] #H1 #H2 try(@H2 % #EQ destruct) normalize
     44    @IH1
     45    [1,3: #EQ destruct normalize @IH2 [1,3: #EQ destruct @H1 % |*: * #H @H2 % #EQ destruct @H %]
     46    |*: * #H @H2 % #EQ destruct @H %
     47    ]
     48]
     49qed.
     50
     51definition DeqExpr ≝
     52mk_DeqSet expr expr_eq ?.
     53@hide_prf #e1 #e2 @expr_eq_elim
     54[ #EQ destruct % // | * #H % #EQ destruct cases H % ]
     55qed.
     56
     57unification hint  0 ≔ ;
     58    X ≟ DeqExpr
     59(* ---------------------------------------- *) ⊢
     60    expr ≡ carr X.
     61
     62(* ambigous input? why?
     63unification hint  0 ≔ p1,p2;
     64    X ≟ DeqExpr
     65(* ---------------------------------------- *) ⊢
     66    expr_eq p1 p2 ≡ eqb X p1 p2.
     67*)
    6668(* for the syntactical record in Language.ma *)
    6769
    … …  
    6971  (* seq_i: type of sequential instructions *)
    7072
    71 inductive seq_i:Type[0]≝sNop: seq_i|sAss: variable → expr → seq_i.
    72 
    73 definition seq_i_eq:seq_i→ seq_i → bool≝λs1,s2:seq_i.match s1 with [
    74  sNop ⇒ match s2 with [sNop ⇒ true| _⇒ false]
    75 |sAss v e ⇒ match s2 with [sAss v' e' ⇒ (andb (v==v') (expr_eq e e'))| _⇒ false]
    76 ].
    77 
    78   (* technical lemma(s) for seq_i_eq *)
    79 
    80 lemma seq_i_eq_refl:∀s.seq_i_eq s s=true.
    81 #s cases s try(#v) try(#e) try %
    82 whd in ⊢ (??%?); >(\b (refl … v)) >expr_eq_refl %
    83 (*|whd in match(seq_i_eq ? ?); /2 by /*)
    84 (*change with (v==v = true); >(\b ?) %*) qed.
    85 
    86 lemma seq_i_eq_equality:∀s1,s2.seq_i_eq s1 s2=true ↔ s1=s2.
    87 #s1 #s2 % [2: * elim s1 [2:#v try(#e)] @seq_i_eq_refl
    88 |lapply s2 -s2 elim s1 [2:#v] [#e] #s2 cases s2 [2,4:#v' #e']
    89 [2,3,4,6,7,8: normalize #H destruct
    90 |1: whd in ⊢ (??%? → ?); inversion (v==v') [2: normalize #_ #H destruct]
    91  #EQ inversion (expr_eq e e') [2: normalize #_ #H destruct] #H #_
    92  >(proj1 … (expr_eq_equality …) H) >(\P EQ) %
    93 ] %
    94 qed.
    95 
    96   (* cond_i: type of (guards of) conditional instructions,
    97              i.e., possible conditions of IfThenElse *)
    98 
    99 definition cond_i:Type[0]≝condition.
    100 
    101 let rec cond_i_eq (c1:cond_i) (c2:cond_i):bool ≝
     73inductive seq_i:Type[0]≝ |sAss: variable → expr → seq_i.
     74
     75definition seq_i_eq:seq_i→ seq_i → bool≝λs1,s2:seq_i.
     76match s1 with [
     77sAss v e ⇒ match s2 with [sAss v' e' ⇒ (andb (v==v') (expr_eq e e')) ]
     78].
     79
     80
     81lemma seq_i_eq_elim : ∀P : bool → Prop.∀s1,s2.(s1 = s2 → P true) → (s1 ≠ s2→ P false) → P (seq_i_eq s1 s2).
     82#P * #v #e * #v' #e' #H1 #H2 normalize @(eqb_elim v v')
     83[ #EQ destruct @expr_eq_elim [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H %]
     84| * #H @H2 % #EQ destruct @H %
     85]
     86qed.
     87
     88definition DeqSeqI ≝ mk_DeqSet seq_i seq_i_eq ?.
     89@hide_prf #e1 #e2 @seq_i_eq_elim
     90[ #EQ destruct % // | * #H % #EQ destruct cases H % ]
     91qed.
     92
     93unification hint  0 ≔ ;
     94    X ≟ DeqSeqI
     95(* ---------------------------------------- *) ⊢
     96    seq_i ≡ carr X.
     97
     98(* ambigous input! why?
     99unification hint  0 ≔ p1,p2;
     100    X ≟ DeqSeqI
     101(* ---------------------------------------- *) ⊢
     102    seq_i_eq p1 p2 ≡ eqb X p1 p2.
     103*)
     104
     105
     106let rec cond_i_eq (c1:condition) (c2:condition):bool ≝
    102107match c1 with [Eq e1 e2⇒ match c2 with [Eq f1 f2 ⇒
    103108(andb (expr_eq e1 f1) (expr_eq e2 f2))|_⇒ false]
    104109|Not e⇒ match c2 with [Not f⇒ cond_i_eq e f|_⇒ false]].
    105110
    106   (* technical lemma(s) for cond_i *)
    107 
    108 lemma condition_eq_refl:∀c:condition.cond_i_eq c c=true.
    109 #c elim c [#e #f whd in ⊢ (??%?); >expr_eq_refl >expr_eq_refl %
    110 |#c' normalize * %] qed.
    111 
    112 lemma cond_i_eq_equality:∀c1,c2:condition.cond_i_eq c1 c2=true ↔ c1=c2.
    113 #c1 #c2 % [2: * // ]
    114 lapply c2 -c2 elim c1 [ #e1 #e2 *
    115 [ #f1 #f2 whd in ⊢ (??%? → ?);
    116   inversion(expr_eq e1 f1) [2: #_ normalize #EQ destruct ] #H1
    117   >(proj1 … (expr_eq_equality …) … H1)
    118   inversion(expr_eq e2 f2) [2: #_ normalize #EQ destruct ] #H2 *
    119   >(proj1 … (expr_eq_equality …) … H2) %
    120 | normalize #c #H destruct
    121 ]| #c2 #IH *
    122 [ normalize #e1 #e2 #H destruct
    123 | #c3 #H >(IH … H) % ]]
    124 qed.
    125 
    126   (* cond_i: type of (guards of) loop instructions,
    127              i.e., possible conditions of While *)
    128 
    129 definition loop_i:Type[0]≝condition.
    130 
    131 definition loop_i_eq:loop_i → loop_i → bool ≝cond_i_eq.
    132 
    133 lemma loop_i_eq_equality:∀l1,l2.loop_i_eq l1 l2=true ↔ l1=l2.@cond_i_eq_equality qed.
    134 
    135   (* io_i: type of I/O instructions (none in the language considered) *)
    136 
    137 definition io_i ≝ False.
    138 
    139 definition io_i_eq ≝ λi1,i2:False. true.
    140 
    141 lemma io_i_eq_equality: ∀i1,i2. io_i_eq i1 i2 = true ↔ i1=i2. * qed.
     111lemma cond_i_eq_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) → (c1 ≠c2 → P false) → P (cond_i_eq c1 c2).
     112#P #c1 lapply P -P elim c1 -c1
     113[ #e1 #e2 #P * [ #e1' #e2' | #c' ] #H1 #H2 normalize try (@H2 % #EQ destruct) @expr_eq_elim
     114  [ #EQ destruct @expr_eq_elim [#EQ destruct @H1 % | * #H @H2 % #EQ destruct @H %]
     115  | * #H @H2 % #EQ destruct @H %
     116  ]
     117| #c #IH #P * [ #e1' #e2' | #c' ] #H1 #H2 normalize try (@H2 % #EQ destruct) @IH
     118  [#EQ destruct @H1 % | * #H @H2 % #EQ destruct @H %]
     119]
     120qed.
     121
     122definition DeqCondition ≝ mk_DeqSet condition cond_i_eq ?.
     123@hide_prf #e1 #e2 @cond_i_eq_elim
     124[ #EQ destruct % // | * #H % #EQ destruct cases H % ]
     125qed.
     126
     127unification hint  0 ≔ ;
     128    X ≟ DeqCondition
     129(* ---------------------------------------- *) ⊢
     130    condition ≡ carr X.
     131
     132(* ambigous input!!!
     133unification hint  0 ≔ p1,p2;
     134    X ≟ DeqCondition
     135(* ---------------------------------------- *) ⊢
     136    cond_i_eq p1 p2 ≡ eqb X p1 p2.
     137*)
    142138
    143139  (* syntactical record *)
    144140
    145 definition DeqExpr:DeqSet≝(mk_DeqSet expr expr_eq expr_eq_equality).
    146 
    147 definition imp_instr_params: instr_params ≝ mk_instr_params ? ? ? ? ? ?.
    148 [@(mk_DeqSet seq_i seq_i_eq seq_i_eq_equality)
    149 |@(mk_DeqSet io_i io_i_eq io_i_eq_equality)
    150 |@(mk_DeqSet cond_i cond_i_eq cond_i_eq_equality)
    151 |@(mk_DeqSet loop_i loop_i_eq loop_i_eq_equality)
    152 |@(DeqProd variable DeqExpr)
    153 |@DeqExpr].qed.
    154 
     141definition imp_instr_params: instr_params ≝ mk_instr_params DeqSeqI DeqFalse
     142DeqCondition DeqCondition (DeqProd variable DeqExpr) DeqExpr.
    155143
    156144definition environment ≝ DeqSet_List (DeqProd variable DeqNat).
    157  
    158 definition eq_environment: environment → environment → Prop ≝
    159  λenv1,env2.env1 = env2.
    160145
    161146
    … …  
    246231
    247232
    248 definition imp_eval_seq:(seq_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝λi,s.match i with
    249 [sNop ⇒ Some ? s
    250 |sAss v e ⇒ match s with
     233definition imp_eval_seq:seq_i →store_t→ option store_t
     234≝λi,s.
     235match i with
     236[sAss v e ⇒ match s with
    251237  [nil⇒ None ?
    252238  |cons hd tl⇒ let 〈env,var〉 ≝ hd in
    … …  
    257243
    258244
    259 definition imp_eval_io:(io_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝?.
     245definition imp_eval_io: False → store_t→ option store_t≝?.
    260246// qed.
    261247
    262 definition imp_eval_cond_cond:(cond_instr imp_state_params)→ (store_type imp_state_params)→ option (bool × (store_type imp_state_params))≝λc,s.
     248definition imp_eval_cond_cond:condition → store_t→ option (bool × store_t)≝λc,s.
    263249!env ← current_env s;
    264250!b ← sem_condition env c;
    … …  
    266252
    267253
    268 definition imp_eval_loop_cond:(loop_instr imp_state_params)→ (store_type imp_state_params)→ option (bool × (store_type imp_state_params))≝
     254definition imp_eval_loop_cond:condition→ store_t → option (bool × store_t)≝
    269255imp_eval_cond_cond.
    270256
    271 definition imp_init_store: (store_type imp_state_params)≝[〈(nil ?),O〉].
    272 
    273 definition imp_eval_call:(signature imp_state_params imp_state_params)→ act_params_type imp_state_params → store_t → (option store_t)≝
     257definition imp_init_store: store_t≝[〈(nil ?),O〉].
     258
     259definition imp_signature≝signature imp_state_params imp_state_params.
     260
     261definition imp_eval_call:imp_signature→ (variable × expr) → store_t → (option store_t)≝
    274262λsgn,e,st.
    275263  match sgn with
    … …  
    284272  ].
    285273
    286 definition imp_return_call:(return_type imp_state_params)→ store_t→ (option store_t)≝
     274definition imp_return_call:expr→ store_t→ (option store_t)≝
    287275λr,s.match s with
    288276[nil⇒ None ?
    … …  
    293281 
    294282
    295 
    296 
    297283definition imp_sem_state_params : sem_state_params imp_state_params ≝ mk_sem_state_params imp_state_params imp_eval_seq imp_eval_io
    298284imp_eval_cond_cond imp_eval_loop_cond imp_eval_call imp_return_call imp_init_store.
    … …  
    302288definition imp_Instructions≝Instructions imp_state_params flat_labels.
    303289
    304 definition imp_signature≝signature imp_state_params imp_state_params.
    305 
    306 
    307290definition imp_envitem≝ (env_item imp_env_params imp_instr_params flat_labels).
    308 

  • LTS/mono_stack.ma

    r3572 r3575  
    4141].
    4242
    43 definition mono_stack_eval_seq: (seq_instr mono_stack_state_params)→
     43definition mono_stack_eval_seq: stack_seq→
    4444mono_stack_store_t→ option mono_stack_store_t≝
    4545λi,s.match i with
    … …  
    5050
    5151definition mono_stack_eval_cond_cond:
    52 (list guard_combinators) → (store_type mono_stack_state_params)→ option (bool × (store_type mono_stack_state_params))≝
     52(list guard_combinators) → mono_stack_store_t→ option (bool × mono_stack_store_t)≝
    5353λl,st.! fin_St ← m_fold Option … mono_eval_combinators l st;
    5454      !〈val,st2〉← mono_pop fin_St;
    5555      return 〈eqb val 1,st2〉.
    5656
     57definition mono_stack_signature≝signature mono_stack_state_params mono_stack_state_params.
    5758
    58 definition mono_stack_eval_call:(signature mono_stack_state_params mono_stack_state_params) →
    59 act_params_type mono_stack_state_params →
    60 store_type mono_stack_state_params → (option (store_type mono_stack_state_params))≝
    61 λsgn.λ_.λst.
     59definition mono_stack_eval_call:mono_stack_signature →
     60mono_stack_store_t → (option mono_stack_store_t)≝
     61λsgn.λst.
    6262    !〈exp_val,st1〉 ← mono_pop st;
    6363    let new_fp ≝ (|(\fst st1)|) in
    … …  
    103103definition mono_stack_sem_state_params : ℕ → sem_state_params mono_stack_state_params ≝
    104104λn.mk_sem_state_params mono_stack_state_params mono_stack_eval_seq ?
    105 (λ_.mono_stack_eval_cond_cond (nil ?)) mono_stack_eval_cond_cond mono_stack_eval_call (λ_.mono_stack_return_call)
     105(λ_.mono_stack_eval_cond_cond (nil ?)) mono_stack_eval_cond_cond (λx.λ_.mono_stack_eval_call x) (λ_.mono_stack_return_call)
    106106(mono_stack_init_store n). * qed.
    107107
    … …  
    110110definition mono_stack_Instructions≝Instructions mono_stack_state_params flat_labels.
    111111
    112 definition mono_stack_signature≝signature mono_stack_state_params mono_stack_state_params.
    113 
    114112
    115113definition mono_stack_envitem≝ (env_item stack_env_params stack_instr_params flat_labels).

  • LTS/stack.ma

    r3570 r3575  
    8080qed.
    8181 
    82 definition stack_instr_params ≝ mk_instr_params DeqStackSeq (mk_DeqSet io_i io_i_eq io_i_eq_equality)
    83  (mk_DeqSet unit (λ_.λ_.true) ?) (DeqSet_List DeqGuardCombinator) (mk_DeqSet unit (λ_.λ_.true) ?) (mk_DeqSet unit (λ_.λ_.true) ?).
    84 @hide_prf ** % // qed.
     82definition stack_instr_params ≝ mk_instr_params DeqStackSeq DeqFalse
     83 DeqUnit (DeqSet_List DeqGuardCombinator) DeqUnit DeqUnit.
    8584
    8685definition stack_env_params ≝ mk_env_params ℕ.
    … …  
    8988mk_state_params stack_instr_params stack_env_params flat_labels frame_store_t (*DeqEnv*).
    9089
    91 definition push : (store_type stack_state_params) → DeqNat → option (store_type stack_state_params) ≝
     90definition push : frame_store_t → DeqNat → option frame_store_t ≝
    9291λs,n.match \fst s with
    9392[nil ⇒ None ?
    … …  
    9594].
    9695
    97 definition pop : (store_type stack_state_params) → option (DeqNat × (store_type stack_state_params)) ≝
     96definition pop : frame_store_t → option (DeqNat × frame_store_t) ≝
    9897λs.match \fst s with
    9998[nil ⇒ None ?
    … …  
    104103             ].
    105104
    106 definition eval_combinators : guard_combinators → (store_type stack_state_params)→ option (store_type stack_state_params)≝
     105definition eval_combinators : guard_combinators → frame_store_t→ option frame_store_t≝
    107106λc,s.match c with
    108107[ push_var x ⇒ ! curr_env ← frame_current_env s;
    … …  
    117116
    118117
    119 definition stack_eval_seq: (seq_instr stack_state_params)→(store_type stack_state_params)→ option (store_type stack_state_params)≝
     118definition stack_eval_seq: stack_seq→frame_store_t→ option frame_store_t≝
    120119λi,s.match i with
    121120[ pop_Ass v ⇒ ! 〈val1,st1〉 ← pop s;frame_assign_var st1 (to_shift +v) val1
    … …  
    125124
    126125definition stack_eval_cond_cond:
    127 (list guard_combinators) → (store_type stack_state_params)→ option (bool × (store_type stack_state_params))≝
     126(list guard_combinators) → frame_store_t→ option (bool × frame_store_t)≝
    128127λl,st.! fin_St ← m_fold Option … eval_combinators l st;
    129128      !〈val,st2〉← pop fin_St;
    … …  
    137136].
    138137
    139 definition stack_eval_call:(signature stack_state_params stack_state_params)→ act_params_type stack_state_params →
     138definition stack_signature≝signature stack_state_params stack_state_params.
     139
     140definition stack_eval_call:stack_signature→
    140141frame_store_t → (option frame_store_t)≝
    141 λsgn.λvar,st.
     142λsgn.λst.
    142143    !〈n,st1〉 ← pop st; 
    143144    frame_assign_var 〈(list_n … O (pred (to_shift + (f_pars … sgn))))::(\fst st1),(\snd st1)〉 to_shift n.
    … …  
    155156definition stack_sem_state_params : ℕ → sem_state_params stack_state_params ≝
    156157λn.mk_sem_state_params stack_state_params stack_eval_seq frame_eval_io
    157 (λ_.stack_eval_cond_cond (nil ?)) stack_eval_cond_cond stack_eval_call (λ_.stack_return_call) (stack_init_store n).
     158(λ_.stack_eval_cond_cond (nil ?)) stack_eval_cond_cond (λsgn.λ_.stack_eval_call sgn) (λ_.stack_return_call) (stack_init_store n).
    158159
    159160  (* Abitare tipo Instructions *)
    … …  
    161162definition stack_Instructions≝Instructions stack_state_params flat_labels.
    162163
    163 definition stack_signature≝signature stack_state_params stack_state_params.
    164 
    165164
    166165definition stack_envitem≝ (env_item stack_env_params stack_instr_params flat_labels).

  • LTS/utils.ma

    r3574 r3575  
    143143qed.
    144144
     145(* some useful deqsets *)
     146
     147definition DeqUnit ≝ mk_DeqSet unit (λ_.λ_.true) ?.
     148@hide_prf ** % // qed.
     149
     150definition DeqFalse ≝ mk_DeqSet False (λ_.λ_.true) ?.
     151@hide_prf * qed.
     152
    145153(* list of elements with decidable equality *)
    146154

  • LTS/variable.ma

    r3573 r3575  
    132132].
    133133
     134lemma eq_frame_seq_i_elim : ∀P : bool → Prop.∀s1,s2.(s1 = s2 → P true) → (s1 ≠ s2 → P false) →
     135P (eq_frame_seq_i s1 s2).
     136#P * [ #i | #v] * [1,3: #i' |*: # v'] #H1 #H2 whd in match eq_frame_seq_i; normalize nodelta
     137try(@H2 % #EQ destruct)
     138[ @seq_i_eq_elim | @(eqb_elim v v') ]
     139[1,3: #EQ destruct /2/ |*: * #H @H2 % #EQ destruct @H %]
     140qed.
     141
    134142definition DeqFrameSeqI ≝ mk_DeqSet frame_seq_i eq_frame_seq_i ?.
    135 @hide_prf cases daemon qed.
     143@hide_prf #x #y @eq_frame_seq_i_elim
     144[ #EQ destruct /2/ | * #H % #EQ destruct cases H % ]
     145qed.
    136146
    137147definition frame_instr_params : instr_params ≝
    138 mk_instr_params ? ? ? ? ? ?.
    139 [ @DeqFrameSeqI
    140 |@(mk_DeqSet io_i io_i_eq io_i_eq_equality)
    141 |@(mk_DeqSet cond_i cond_i_eq cond_i_eq_equality)
    142 |@(mk_DeqSet loop_i loop_i_eq loop_i_eq_equality)
    143 |@DeqExpr
    144 |@DeqExpr].qed.
     148mk_instr_params DeqFrameSeqI DeqFalse DeqCondition DeqCondition DeqExpr DeqExpr.
    145149
    146150definition frame_state_params:state_params≝
    147151mk_state_params frame_instr_params frame_env_params flat_labels frame_store_t (*DeqEnv*).
    148152
    149 definition frame_current_env:store_type frame_state_params→ option ?≝λs.!hd ← option_hd … (\fst s); return hd.
     153definition frame_current_env:frame_store_t→ option ?≝λs.!hd ← option_hd … (\fst s); return hd.
    150154
    151155definition frame_assign_var ≝ λenv:frame_store_t.λv:variable.λn:DeqNat.
    … …  
    155159].
    156160
    157 definition frame_eval_seq:(seq_instr frame_state_params)→(store_type frame_state_params)→ option (store_type frame_state_params)≝
     161definition frame_eval_seq:frame_seq_i →frame_store_t→ option frame_store_t≝
    158162λi,s.match i with
    159163[ Seq_i instr ⇒
    160164   match instr with
    161    [sNop ⇒ Some ? s
    162    |sAss v e ⇒ !env ← frame_current_env … s;
     165   [sAss v e ⇒ !env ← frame_current_env … s;
    163166               ! n ← frame_sem_expr env e;
    164167               frame_assign_var s v n
    … …  
    168171
    169172
    170 definition frame_eval_io:(io_instr frame_state_params)→(store_type frame_state_params)→ option (store_type frame_state_params)≝?.
     173definition frame_eval_io:False→frame_store_t→ option frame_store_t≝?.
    171174// qed.
    172175
    173 definition frame_eval_cond_cond:(cond_instr frame_state_params)→ (store_type frame_state_params)→ option (bool × (store_type frame_state_params))≝λc,s.
     176definition frame_eval_cond_cond:condition→ frame_store_t→ option (bool × frame_store_t)≝λc,s.
    174177!env ← frame_current_env s;
    175178!b ← frame_sem_condition env c;
    … …  
    177180
    178181
    179 definition frame_eval_loop_cond:(loop_instr frame_state_params)→ (store_type frame_state_params)→ option (bool × (store_type frame_state_params))≝
     182definition frame_eval_loop_cond:condition→ frame_store_t→ option (bool × frame_store_t)≝
    180183frame_eval_cond_cond.
    181184
    182 definition frame_eval_call:(signature frame_state_params frame_state_params)→ act_params_type frame_state_params → frame_store_t → (option frame_store_t)≝
     185definition frame_signature≝signature frame_state_params frame_state_params.
     186
     187definition frame_eval_call:frame_signature→ expr → frame_store_t → (option frame_store_t)≝
    183188λsgn,e,st.
    184189    !env ← frame_current_env … st;
    … …  
    186191    frame_assign_var 〈((nil ?)::(\fst st)),(\snd st)〉 to_shift n.
    187192
    188 definition frame_return_call:(return_type frame_state_params)→ frame_store_t→ (option frame_store_t)≝
     193definition frame_return_call:expr→ frame_store_t→ (option frame_store_t)≝
    189194λr,s.match (\fst s) with
    190195[nil⇒ None ?
    … …  
    193198].
    194199 
    195 definition frame_init_store: (store_type frame_state_params)≝ 〈[(nil ?)],〈O,O〉〉.
     200definition frame_init_store: frame_store_t≝ 〈[(nil ?)],〈O,O〉〉.
    196201
    197202
    … …  
    203208definition frame_Instructions≝Instructions frame_state_params flat_labels.
    204209
    205 definition frame_signature≝signature frame_state_params frame_state_params.
    206 
    207210
    208211definition frame_envitem≝ (env_item frame_env_params frame_instr_params flat_labels).

  • LTS/variable_stack_pass.ma

    r3574 r3575  
    5555  [ Seq_i seq' ⇒
    5656     match seq' with
    57      [ sNop ⇒ 〈t_instr,c_bound〉
    58      | sAss v e ⇒ 〈list_combinators_to_instructions (trans_expr e) (SEQ … (pop_Ass v) opt_l t_instr),
     57     [ sAss v e ⇒ 〈list_combinators_to_instructions (trans_expr e) (SEQ … (pop_Ass v) opt_l t_instr),
    5958                max (get_expr_bound e) c_bound〉
    6059     ]
Note: See TracChangeset for help on using the changeset viewer.