Ignore:
Timestamp:
May 21, 2012, 7:04:21 PM (8 years ago)
Author:
tranquil
Message:
  • monads: just changed some defs, which had to be propagated in some files
  • ASM/CostProof.ma: linked cost as defined there to the one in StructuredTraces? that uses fold
  • added a library for permutations of lists (useful with fold AC ops on lists)
  • first draft of abstract_status implementation for joint languages (file joint/as_semantics.ma)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint_paolo.ma

    r1949 r1976  
    77include "common/LabelledObjects.ma".
    88include "ASM/Util.ma".
     9include "basics/deqsets.ma".
     10include "basics/finset.ma". (* for DeqNat *)
    911
    1012(* Here is the structure of parameter records (downward edges are coercions,
     
    147149 { stmt_pars :> stmt_params
    148150 ; codeT: list ident → Type[0]
    149  ; code_point : Type[0]
     151 ; code_point : DeqSet
    150152 ; stmt_at : ∀globals.codeT globals → code_point → option (joint_statement stmt_pars globals)
    151153 ; point_of_label : ∀globals.codeT globals → label → option code_point
     
    290292      (mk_stmt_params lp unit (λ_.None ?))
    291293    (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals)))
    292     (* code_point ≝ *)
     294    (* code_point ≝ *)DeqNat
    293295    (* stmt_at ≝ *)(λglobals,code,point.! ls ← nth_opt ? point code ; return \snd ls)
    294296    (* point_of_label ≝ *)(λglobals,c,lbl.
     
    325327  { g_u_pars :> unserialized_params }.
    326328
    327 (* move *)
    328 definition lookup_safe : ∀tag,A.∀m : identifier_map tag A.∀i.i ∈ m → A ≝
    329   λtag,A,m.match m return λx : identifier_map tag A.∀i.i ∈ x → ? with
    330   [ an_id_map m' ⇒ λi.match i return λx.x ∈ an_id_map ?? m' → ? with
    331     [ an_identifier i' ⇒
    332       match lookup_opt … i' m' return λx.match x with [Some y ⇒ true | None ⇒ false] → ? with
    333       [ Some y ⇒ λ_.y
    334       | None ⇒ Ⓧ
    335       ]
    336     ]
    337   ].
    338  
    339 lemma lookup_safe_elim : ∀tag,A.∀P : A → Prop.∀m,i,prf.
    340   (∀x.lookup tag A m i = Some ? x → P x) → P (lookup_safe tag A m i prf).
    341 #tag #A #P *#m *#i normalize elim (lookup_opt A i m) normalize
    342 [ * ]
    343 #s * #H @H %
    344 qed.
    345 
    346329(* One common instantiation of params via Graphs of joint_statements
    347330   (all languages but LIN) *)
     
    351334      (mk_stmt_params gp label (Some ?))
    352335    (* codeT ≝ *)(λglobals.graph (joint_statement ? globals))
    353     (* code_point ≝ *)label
     336    (* code_point ≝ *)(Deq_identifier LabelTag)
    354337    (* stmt_at ≝ *)(λglobals,code.lookup LabelTag ? code)
    355338    (* point_of_label ≝ *)(λ_.λ_.λlbl.return lbl)
Note: See TracChangeset for help on using the changeset viewer.