Changeset 1640 for src/common/Errors.ma


Ignore:
Timestamp:
Jan 11, 2012, 5:41:45 PM (9 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
File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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 ≝
Note: See TracChangeset for help on using the changeset viewer.