Changeset 1640 for src/common


Ignore:
Timestamp:
Jan 11, 2012, 5:41:45 PM (8 years ago)
Author:
tranquil
Message:
  • finished fork of semantics.ma
  • unification of Errors under the monad notations brings problems in type checking when res and IO are used together. Needs a lot of annotations, and may break the pre-fork material
Location:
src/common
Files:
3 edited

Legend:

Unmodified
Added
Removed

  • src/common/AST.ma

    r1516 r1640  
    196196
    197197lemma typesize_pos: ∀ty. typesize ty > 0.
    198 *; try *; try * /2/ qed.
     198*; try *; try * /2 by le_n/ qed.
    199199
    200200lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2).
    … …  
    343343definition map_partial : ∀A,B,C:Type[0]. (B → res C) →
    344344                         list (A × B) → res (list (A × C)) ≝
    345 λA,B,C,f. mmap ?? (λab. let 〈a,b〉 ≝ ab in do c ← f b; OK ? 〈a,c〉).
     345λA,B,C,f. m_mmap ??? (λab. let 〈a,b〉 ≝ ab in do c ← f b; OK ? 〈a,c〉).
    346346
    347347lemma map_partial_preserves_first:

  • src/common/Errors.ma

    r1626 r1640  
    1919include "common/PreIdentifiers.ma".
    2020include "basics/russell.ma".
     21include "utilities/monad.ma".
    2122
    2223(* * Error reporting and the error monad. *)
    … …  
    4849(*Implicit Arguments Error [A].*)
    4950
    50 (* * To automate the propagation of errors, we use a monadic style
    51   with the following [bind] operation. *)
    52 
    53 definition bind ≝ λA,B:Type[0]. λf: res A. λg: A → res B.
    54   match f with
    55   [ OK x ⇒ g x
    56   | Error msg ⇒ Error ? msg
    57   ].
    58 
    59 definition bind2 ≝ λA,B,C: Type[0]. λf: res (A × B). λg: A → B → res C.
    60   match f with
    61   [ OK v ⇒ g (fst … v) (snd … v)
    62   | Error msg => Error ? msg
    63   ].
    64 
    65 definition bind3 ≝ λA,B,C,D: Type[0]. λf: res (A × B × C). λg: A → B → C → res D.
    66   match f with
    67   [ OK v ⇒ g (fst … (fst … v)) (snd … (fst … v)) (snd … v)
    68   | Error msg => Error ? msg
    69   ].
    70  
    71 (* Not sure what level to use *)
    72 notation > "vbox('do' ident v ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v}.${e'})}.
    73 notation > "vbox('do' ident v : ty ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v} : ${ty}.${e'})}.
    74 notation < "vbox('do' \nbsp ident v ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v}.${e'})}.
    75 notation < "vbox('do' \nbsp ident v : ty ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v} : ${ty}.${e'})}.
    76 interpretation "error monad bind" 'bind e f = (bind ?? e f).
    77 notation > "vbox('do' 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
    78 notation > "vbox('do' 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.
    79 notation < "vbox('do' \nbsp 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
    80 notation < "vbox('do' \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.
    81 interpretation "error monad Prod bind" 'bind2 e f = (bind2 ??? e f).
    82 notation > "vbox('do' 〈ident v1, ident v2, ident v3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1}.λ${ident v2}.λ${ident v3}.${e'})}.
    83 notation > "vbox('do' 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.λ${ident v3} : ${ty3}.${e'})}.
    84 notation < "vbox('do' \nbsp 〈ident v1, ident v2, ident v3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1}.λ${ident v2}.λ${ident v3}.${e'})}.
    85 notation < "vbox('do' \nbsp 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.λ${ident v3} : ${ty3}.${e'})}.
    86 interpretation "error monad triple bind" 'bind3 e f = (bind3 ???? e f).
    87 (*interpretation "error monad ret" 'ret e = (ret ? e).
    88 notation "'ret' e" non associative with precedence 45 for @{'ret ${e}}.*)
    89 
    90 (* Dependent pair version. *)
     51definition Res : Monad ≝ MakeMonad (mk_MonadDefinition
     52  (* the monad *)
     53  res
     54  (* return *)
     55  (λX.OK X)
     56  (* bind *)
     57  (λX,Y,m,f. match m with [ OK x ⇒ f x | Error msg ⇒ Error ? msg])
     58  ???).
     59//
     60[(* bind_bind *)
     61 #X#Y#Z*normalize //
     62|(* bind_ret *)
     63 #X*normalize //
     64]
     65qed.
     66
     67include "hints_declaration.ma".
     68unification hint 0 ≔ X;
     69M ≟ m_def Res
     70(*---------------*) ⊢
     71res X ≡ monad M X
     72.
     73
     74(*(* Dependent pair version. *)
    9175notation > "vbox('do' « ident v , ident p » ← e; break e')" with precedence 40
    9276  for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ mk_Sig ${ident v} ${ident p} ⇒ ${e'} ]) }.
    … …  
    11094
    11195notation > "vbox('do' «ident v1, ident v2, ident H» ← e; break e')" with precedence 40 for @{'sigbind2 ${e} (λ${ident v1}.λ${ident v2}.λ${ident H}.${e'})}.
    112 interpretation "error monad sig Prod bind" 'sigbind2 e f = (sigbind2 ???? e f).
    113 
    114 (*
    115 (** The [do] notation, inspired by Haskell's, keeps the code readable. *)
    116 
    117 Notation "'do' X <- A ; B" := (bind A (fun X => B))
    118  (at level 200, X ident, A at level 100, B at level 200)
    119  : error_monad_scope.
    120 
    121 Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B))
    122  (at level 200, X ident, Y ident, A at level 100, B at level 200)
    123  : error_monad_scope.
    124 *)
    125 lemma bind_inversion:
     96interpretation "error monad sig Prod bind" 'sigbind2 e f = (sigbind2 ???? e f).*)
     97
     98lemma res_bind_inversion:
    12699  ∀A,B: Type[0]. ∀f: res A. ∀g: A → res B. ∀y: B.
    127   bind ?? f g = OK ? y →
    128   ∃x. f = OK ? x ∧ g x = OK ? y.
    129 #A #B #f #g #y cases f;
    130 [ #a #e %{a} whd in e:(??%?); /2/;
    131 | #m #H whd in H:(??%?); destruct (H);
     100  (f »= g = return y) →
     101  ∃x. (f = return x) ∧ (g x = return y).
     102#A #B #f #g #y cases f normalize
     103[ #a #e %{a} /2 by conj/
     104| #m #H destruct (H)
    132105] qed.
    133106
    134107lemma bind2_inversion:
    135108  ∀A,B,C: Type[0]. ∀f: res (A×B). ∀g: A → B → res C. ∀z: C.
    136   bind2 ??? f g = OK ? z →
    137   ∃x. ∃y. f = OK ? 〈x, y〉 ∧ g x y = OK ? z.
    138 #A #B #C #f #g #z cases f;
    139 [ #ab cases ab; #a #b #e %{a} %{b} whd in e:(??%?); /2/;
    140 | #m #H whd in H:(??%?); destruct
     109  m_bind2 ???? f g = return z →
     110  ∃x. ∃y. f = return 〈x, y〉 ∧ g x y = return z.
     111#A #B #C #f #g #z cases f normalize
     112[ * #a #b normalize #e %{a} %{b} /2 by conj/
     113| #m #H destruct (H)
    141114] qed.
    142115
    143116(*
    144 Open Local Scope error_monad_scope.
    145 
    146 (** This is the familiar monadic map iterator. *)
    147 *)
    148 
    149 let rec mmap (A, B: Type[0]) (f: A → res B) (l: list A) on l : res (list B) ≝
    150   match l with
    151   [ nil ⇒ OK ? []
    152   | cons hd tl ⇒ do hd' ← f hd; do tl' ← mmap ?? f tl; OK ? (hd'::tl')
    153   ].
    154 
    155 (* And mmap coupled with proofs. *)
    156 
    157 let rec mmap_sigma (A,B:Type[0]) (P:B → Prop) (f:A → res (Σx:B.P x)) (l:list A) on l : res (Σl':list B.All B P l') ≝
    158 match l with
    159 [ nil ⇒ OK ? «nil B, ?»
    160 | cons h t ⇒
    161     do h' ← f h;
    162     do t' ← mmap_sigma A B P f t;
    163     OK ? «cons B h' t', ?»
    164 ].
    165 whd // %
    166 [ @(pi2 … h')
    167 | cases t' #l' #p @p
    168 ] qed.
     117Open Local Scope error_monad_scope.*)
    169118
    170119(*
    … …  
    189138    [ nil ⇒ x
    190139    | cons hd tl ⇒
    191        do x ← x ;
     140       ! x ← x ;
    192141       mfold_left_i_aux A B f (f i x hd) (S i) tl
    193142    ].
    … …  
    213162    [ nil ⇒ Error ? (msg WrongLength)
    214163    | cons hd' tl' ⇒
    215        do accu ← accu;
     164       ! accu ← accu;
    216165       mfold_left2 … f (f accu hd hd') tl tl'
    217166    ]
    … …  
    301250  ] (refl ? f).
    302251
    303 notation > "vbox('do' ident v 'as' ident E ← e; break e')" with precedence 40 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}.
     252notation > "vbox('!' ident v 'as' ident E ← e; break e')" with precedence 40 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}.
    304253
    305254definition bind2_eq ≝ λA,B,C:Type[0]. λf: res (A×B). λg: ∀a:A.∀b:B. f = OK ? 〈a,b〉 → res C.
    … …  
    309258  ] (refl ? f).
    310259
    311 notation > "vbox('do' 〈ident v1, ident v2〉 'as' ident E ← e; break e')" with precedence 40 for @{ bind2_eq ??? ${e} (λ${ident v1}.λ${ident v2}.λ${ident E}.${e'})}.
     260notation > "vbox('!' 〈ident v1, ident v2〉 'as' ident E ← e; break e')" with precedence 40 for @{ bind2_eq ??? ${e} (λ${ident v1}.λ${ident v2}.λ${ident E}.${e'})}.
    312261
    313262definition res_to_opt : ∀A:Type[0]. res A → option A ≝

  • src/common/IOMonad.ma

    r1601 r1640  
    88| Value : T → IO output input T
    99| Wrong : errmsg → IO output input T.
     10
     11include "utilities/proper.ma".
     12(* a weak form of extensionality *)
     13axiom interact_proper :
     14  ∀O,I,T,o.∀f,g : I o → IO O I T.(∀i. f i = g i) → Interact … o f = Interact … o g.
    1015
    1116let rec bindIO (O:Type[0]) (I:O → Type[0]) (T,T':Type[0]) (v:IO O I T) (f:T → IO O I T') on v : IO O I T' ≝
    … …  
    1621].
    1722
    18 let rec bindIO2 (O:Type[0]) (I:O → Type[0]) (T1,T2,T':Type[0]) (v:IO O I (T1×T2)) (f:T1 → T2 → IO O I T') on v : IO O I T' ≝
    19 match v with
    20 [ Interact out k ⇒ (Interact ??? out (λres. bindIO2 ?? T1 T2 T' (k res) f))
    21 | Value v' ⇒ let 〈v1,v2〉 ≝ v' in f v1 v2
    22 | Wrong m ⇒ Wrong ?? T' m
    23 ].
     23include "utilities/monad.ma".
     24
     25definition IOMonad ≝ λO,I.
     26  MakeMonad (mk_MonadDefinition
     27  (* the monad *)
     28  (IO O I)
     29  (* return *)
     30  (λX.Value … X)
     31  (* bind *)
     32  (bindIO O I)
     33  ???). / by /
     34[(* bind_bind *)
     35 #X#Y#Z#m#f#g elim m normalize [2,3://]
     36 (* Interact *)
     37  #o#f #Hi @interact_proper //
     38|(* bind_ret *)
     39 #X#m elim m normalize // #o#f#Hi @interact_proper //
     40]
     41qed.
     42
     43definition bindIO2 ≝ λO,I. m_bind2 (IOMonad O I).
     44
     45include "hints_declaration.ma".
     46
     47unification hint 0 ≔ O, I, T;
     48  N ≟ IOMonad O I, M ≟ m_def N
     49(*******************************************) ⊢
     50  IO O I T ≡ monad M T
     51.
     52
    2453
    2554definition err_to_io : ∀O,I,T. res T → IO O I T ≝
    2655λO,I,T,v. match v with [ OK v' ⇒ Value O I T v' | Error m ⇒ Wrong O I T m ].
     56
    2757coercion err_to_io : ∀O,I,A.∀c:res A.IO O I A ≝ err_to_io on _c:res ? to IO ???.
     58
    2859definition err_to_io_sig : ∀O,I,T.∀P:T → Prop. res (Sig T P) → IO O I (Sig T P) ≝
    2960λO,I,T,P,v. match v with [ OK v' ⇒ Value O I (Sig T P) v' | Error m ⇒ Wrong O I (Sig T P) m ].
    3061(*coercion err_to_io_sig : ∀O,I,A.∀P:A → Prop.∀c:res (Sig A P).IO O I (Sig A P) ≝ err_to_io_sig on _c:res (Sig ??) to IO ?? (Sig ??).*)
    3162
    32 
    33 (* If the original definitions are vague enough, do I need to do this? *)
    34 notation > "! ident v ← e; e'" with precedence 40 for @{'bindIO ${e} (λ${ident v}.${e'})}.
    35 notation > "! ident v : ty ← e; e'" with precedence 40 for @{'bindIO ${e} (λ${ident v} : ${ty}.${e'})}.
    36 notation < "vbox(! \nbsp ident v ← e; break e')" with precedence 40 for @{'bindIO ${e} (λ${ident v}.${e'})}.
    37 notation < "vbox(! \nbsp ident v : ty ← e; break e')" with precedence 40 for @{'bindIO ${e} (λ${ident v} : ${ty}.${e'})}.
    38 notation > "! 〈ident v1, ident v2〉 ← e; e'" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
    39 notation > "! 〈ident v1 : ty1, ident v2 : ty2〉 ← e; e'" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.
    40 notation < "vbox(! \nbsp 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
    41 notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.
    42 interpretation "IO monad bind" 'bindIO e f = (bindIO ???? e f).
    43 interpretation "IO monad Prod bind" 'bindIO2 e f = (bindIO2 ????? e f).
    44 (**)
    4563let rec P_io O I (A:Type[0]) (P:A → Prop) (v:IO O I A) on v : Prop ≝
    4664match v return λ_.Prop with
    … …  
    176194
    177195(* Is there a way to prove this without extensionality? *)
    178 
     196(*
    179197lemma bind_assoc_r: ∀O,I,A,B,C,e,f,g.
    180198  ∀ext:(∀T1,T2:Type[0].∀f,f':T1 → T2.(∀x.f x = f' x) → f = f').
    … …  
    186204| #m @refl
    187205] qed.
     206*)
     207definition bind_assoc_r ≝ λO,I.m_bind_bind (IOMonad O I).
    188208
    189209(*
Note: See TracChangeset for help on using the changeset viewer.