source: src/utilities/option.ma @ 2896

Last change on this file since 2896 was 2770, checked in by mckinna, 7 years ago

WARNING: another big commit, touching many files in ASM/*.ma

This edit
a) prunes many redundant "include"s from ASM/*.ma hierarchy
b) adjusts the use of aliases from ASM/ and elsewhere (big, annoying, hard-to-debug disambiguation errors), from the earlier adjustment to ASM/ASM.ma
c) adds ONE (and once repeated) type annotation to ASM/Interpret.ma

As with the continual failures with Clight/switchRemoval.ma, the (revised) definition of execute_1_preinstruction causes no end of disambiguation thrashing. One type annotation (in the JMP case, to ensure that program_counter calculations actually produce values in Word) is enough to cut that particular Gordian knot. By russell-style reasoning, the annotation then gets repeated later, though in fact in that later instance is redundant...

File size: 2.8 KB
RevLine 
[2770]1include "basics/types.ma".
[1635]2include "utilities/monad.ma".
[1640]3
[1647]4definition Option ≝ MakeMonadProps
[1635]5  (* the monad *)
6  option
7  (* return *)
8  (λX.Some X)
9  (* bind *)
10  (λX,Y,m,f. match m with [ Some x ⇒ f x | None ⇒ None ?])
[1882]11  ????.
12// #X[|*:#Y[#Z]]*normalize//qed.
[1635]13
14include "hints_declaration.ma".
[1949]15alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
[1635]16unification hint 0 ≔ X;
[1882]17N ≟ max_def Option
[1635]18(*---------------*) ⊢
[1882]19option X ≡ monad N X
[1635]20.
[1640]21
22definition opt_safe : ∀X.∀m : option X. m ≠ None X → X ≝
23λX,m,prf.match m return λx.m = x → X with
24  [ Some t ⇒ λ_.t
25  | None ⇒ λeq_m.?
[1882]26  ] (refl …). elim (absurd … eq_m prf) qed.
27
28lemma opt_to_opt_safe : ∀A,m,prf. m = Some ? (opt_safe A m prf).
29#A *
30[ #ABS elim (absurd ? (refl ??) ABS)
31| //
32] qed.
33
34lemma opt_safe_elim : ∀A.∀P : A → Prop.∀m,prf.
35  (∀x.m = Some ? x → P x) → P (opt_safe ? m prf).
36#A#P*
37[#prf elim(absurd … (refl ??) prf)
38|#x normalize #_ #H @H @refl
39] qed.
40
[1949]41lemma opt_safe_proof_irr : ∀A,m,prf1,prf2.
42  opt_safe A m prf1 = opt_safe A m prf2.
43  #A* // qed.
44
[1882]45definition opt_try_catch : ∀X.option X → (unit → X) → X ≝
46  λX,m,f.match m with [Some x ⇒ x | None ⇒ f it].
47
48notation > "'Try' m 'catch' opt (ident e opt( : ty)) ⇒ f" with precedence 46 for
49  ${ default
50    @{ ${ default
51      @{'trycatch $m (λ${ident e}:$ty.$f)}
52      @{'trycatch $m (λ${ident e}.$f)}
53    }}
54    @{'trycatch $m (λ_.$f)}
55  }.
56
57notation < "hvbox('Try' \nbsp break m \nbsp break 'catch' \nbsp ident e : ty \nbsp ⇒ \nbsp break f)" with precedence 46 for
58  @{'trycatch $m (λ${ident e}:$ty.$f)}.
59notation < "hvbox('Try' \nbsp break m \nbsp break 'catch' \nbsp ⇒ \nbsp break f)" with precedence 46 for
60  @{'trycatch $m (λ_:$ty.$f)}.
61
62interpretation "option try and catch" 'trycatch m f = (opt_try_catch ? m f).
63
[1976]64definition OptPred ≝ λPdef : Prop.mk_InjMonadPred Option
65  (mk_MonadPred ?
66    (λX,P,x.Try ! y ← x ; return P y catch ⇒ Pdef)
67    ???)
[1949]68  (λX,P,m_sig.match m_sig with [ mk_Sig m prf ⇒ match m return λx.Try ! y ← x ; return P y catch ⇒ Pdef → option (Σy.?) with [ Some x ⇒ λprf.Some ? x | None ⇒ λ_.None ? ] prf ])
[1976]69  ?.
70[4: @prf
[1949]71|*:
[1976]72#X[2:#Y]#P1[1,2:#P2[2:#H]]
[1949]73[1,2,4: * [5: *]] normalize /2/
[1882]74qed.
75
76definition opt_All : ∀X.(X → Prop) → option X → Prop ≝ m_pred … (OptPred True).
[1949]77
[1882]78lemma opt_All_mp : ∀A,P,Q.(∀x. P x → Q x) → ∀o.opt_All A P o → opt_All ? Q o
79  ≝ m_pred_mp ….
80
81definition opt_Exists : ∀X.(X → Prop) → option X → Prop ≝ m_pred … (OptPred False).
82 
83lemma opt_Exists_mp : ∀A,P,Q.(∀x. P x → Q x) → ∀o.opt_Exists A P o → opt_Exists ? Q o
[2767]84  ≝ m_pred_mp ….
85 
86(* moved from ASM/ASM.ma! *)
87definition partial_injection : ∀A,B.(A → option B) → Prop ≝
88λA,B,f.∀x,y,z.f x = Some ? z → f y = Some ? z → x = y.
Note: See TracBrowser for help on using the repository browser.