Changeset 1647


Ignore:
Timestamp:
Jan 17, 2012, 1:13:08 PM (6 years ago)
Author:
tranquil
Message:
  • corrected some notation problems
  • adapted Cligth with slight modifications to new monad framework
Location:
src
Files:
9 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r1603 r1647  
    350350  match s with
    351351  [ Sassign a1 a2 ⇒
    352     ! 〈l,tr1〉 ← exec_lvalue ge e m a1;
    353     ! 〈v2,tr2〉 ← exec_expr ge e m a2;
     352    ! 〈l,tr1〉 ← exec_lvalue ge e m a1 : IO ???;
     353    ! 〈v2,tr2〉 ← exec_expr ge e m a2 : IO ???;
    354354    ! m' ← opt_to_io … (msg FailedStore) (store_value_of_type' (typeof a1) m l v2);
    355355    ret ? 〈tr1⧺tr2, State f Sskip k e m'〉
    356356  | Scall lhs a al ⇒
    357     ! 〈vf,tr2〉 ← exec_expr ge e m a;
    358     ! 〈vargs,tr3〉 ← exec_exprlist ge e m al;
     357    ! 〈vf,tr2〉 ← exec_expr ge e m a : IO ???;
     358    ! 〈vargs,tr3〉 ← exec_exprlist ge e m al : IO ???;
    359359    ! fd ← opt_to_io … (msg BadFunctionValue) (find_funct ? ? ge vf);
    360360    ! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (fun_typeof a));
     
    371371         [ None ⇒ ret ? 〈tr2⧺tr3, Callstate fd vargs (Kcall (None ?) f e k) m〉
    372372         | Some lhs' ⇒
    373            ! 〈locofs,tr1〉 ← exec_lvalue ge e m lhs';
     373           ! 〈locofs,tr1〉 ← exec_lvalue ge e m lhs' : IO ???;
    374374           ret ? 〈tr1⧺tr2⧺tr3, Callstate fd vargs (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k) m〉
    375375         ]
     
    390390      | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
    391391      | Kdowhile a s' k' ⇒
    392           ! 〈v,tr〉 ← exec_expr ge e m a;
     392          ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
    393393          ! b ← err_to_io … (exec_bool_of_val v (typeof a));
    394394          match b with
     
    406406      | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
    407407      | Kdowhile a s' k' ⇒
    408           ! 〈v,tr〉 ← exec_expr ge e m a;
     408          ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
    409409          ! b ← err_to_io … (exec_bool_of_val v (typeof a));
    410410          match b with
     
    426426      ]
    427427  | Sifthenelse a s1 s2 ⇒
    428       ! 〈v,tr〉 ← exec_expr ge e m a;
     428      ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
    429429      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
    430430      ret ? 〈tr, State f (if b then s1 else s2) k e m〉
    431431  | Swhile a s' ⇒
    432       ! 〈v,tr〉 ← exec_expr ge e m a;
     432      ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
    433433      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
    434434      ret ? 〈tr, if b then State f s' (Kwhile a s' k) e m
     
    438438      match is_Sskip a1 with
    439439      [ inl _ ⇒
    440           ! 〈v,tr〉 ← exec_expr ge e m a2;
     440          ! 〈v,tr〉 ← exec_expr ge e m a2 : IO ???;
    441441          ! b ← err_to_io … (exec_bool_of_val v (typeof a2));
    442442          ret ? 〈tr, State f (if b then s' else Sskip) (if b then (Kfor2 a2 a3 s' k) else k) e m〉
     
    453453        [ inl _ ⇒ Wrong ??? (msg ReturnMismatch)
    454454        | inr _ ⇒
    455           ! 〈v,tr〉 ← exec_expr ge e m a;
     455          ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
    456456          ret ? 〈tr, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉
    457457        ]
    458458    ]
    459459  | Sswitch a sl ⇒
    460       ! 〈v,tr〉 ← exec_expr ge e m a;
     460      ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
    461461      match v with [ Vint sz n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch sz n sl)) (Kswitch k) e m〉
    462462                   | _ ⇒ Wrong ??? (msg TypeMismatch)]
     
    473473  [ CL_Internal f ⇒
    474474    let 〈e,m1〉 ≝ exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) in
    475       ! m2 ← exec_bind_parameters e m1 (fn_params f) vargs;
     475      ! m2 ← exec_bind_parameters e m1 (fn_params f) vargs : IO ???;
    476476      ret ? 〈E0, State f (fn_body f) k e m2〉
    477477  | CL_External f argtys retty ⇒
    478       ! evargs ← check_eventval_list vargs (typlist_of_typelist argtys);
     478      ! evargs ← check_eventval_list vargs (typlist_of_typelist argtys) : IO ???;
    479479      ! evres ← do_io f evargs (proj_sig_res (signature_of_type argtys retty));
    480480      ret ? 〈Eextcall f evargs (mk_eventval ? evres), Returnstate (mk_val ? evres) k m〉
  • src/Clight/CexecSound.ma

    r1545 r1647  
    106106    cut (type_region ty s);
    107107    [ cases ty in es:(??%?) ⊢ %; [ #e | 3: #a #e | 2,4,6,7,8,9: #a #b #e | #a #b #c #e ]
    108         whd in e:(??%?); destruct; //;
     108        whd in e:(??%%); destruct; //;
    109109    | #Hty
    110110        cut (type_region ty' s');
    111111        [ cases ty' in es' ⊢ %; [ #e | 3: #a #e | 2,4,6,7,8,9: #a #b #e | #a #b #c #e ]
    112             whd in e:(??%?); destruct; //;
     112            whd in e:(??%%); destruct; //;
    113113        | #Hty'
    114114            cut (s = ptype ptr). elim (eq_region_dec (ptype ptr) s) in eu; //; normalize; #_ #e destruct.
    115115            #e >e in Hty; #Hty
    116116            cases (pointer_compat_dec (pblock ptr) s') in e''';
    117             #Hcompat #e''' whd in e''':(??%?); destruct (e'''); /2/
     117            #Hcompat #e''' whd in e''':(??%%); destruct /2 by cast_pp/
    118118        ]
    119119    ]
     
    207207    ]
    208208| #ty #e #He whd in ⊢ (???%);
    209     @bind2_OK #v cases v // * #r #l #pc #ofs #tr #Hv whd
     209    @bind2_OK #v cases v / by / * #r #l #pc #ofs #tr #Hv whd
    210210    >Hv in He; #He
    211211    @eval_Ederef [ 3: @He | *: skip ]
     
    505505    whd; @(step_internal_function … (exec_alloc_variables_sound … ALLOC))
    506506    @(P_res_to_P … (exec_bind_parameters_sound …) BIND)
    507   | #id #argtys #rty @res_bindIO_OK #evs #Hevs
    508     @bindIO_OK #eres whd;
     507  | #id #argtys #rty @res_bindIO_OK #evs #Hevs #v'
     508    @bindIO_OK #eres whd
    509509    @step_external_function % [ @(P_res_to_P … (check_eventval_list_sound …) Hevs)
    510510                              | @mk_val_correct ]
     
    536536  [ whd; %
    537537  | @(P_bindIO2_OK ????????? (exec_step_sound …)) #t #s' cases s';
    538       [ #f #s #k #e #m | #fd #args #k #m | #r #k #m ]
    539       whd in ⊢ (? → ?????(??????%?));
    540       cases m; #mc #mn #mp #Hstep
    541       whd in ⊢ (?????(??????%?));
     538      [ #f #s #k #e #m | #fd #args #k #m | #r #k #m ] normalize
     539(*      whd in ⊢ (? → ?????(??????%?)); *)
     540      cases m; #mc #mn #mp #Hstep normalize
     541(*      whd in ⊢ (?????(??????%?));*)
    542542      @(P_bindIO2_OK ????????? (IH …)) #t' #s'' #Hsteps
    543543      whd; @(star_step ????????? Hsteps) [ 2,5,8: @Hstep | 3,6,9: // ]
  • src/common/Errors.ma

    r1640 r1647  
    4949(*Implicit Arguments Error [A].*)
    5050
    51 definition Res : Monad ≝ MakeMonad (mk_MonadDefinition
     51definition Res ≝ MakeMonadProps
    5252  (* the monad *)
    5353  res
     
    5656  (* bind *)
    5757  (λX,Y,m,f. match m with [ OK x ⇒ f x | Error msg ⇒ Error ? msg])
    58   ???).
     58  ???.
    5959//
    60 [(* bind_bind *)
     60[(* bind_ret *)
     61 #X*normalize //
     62|(* bind_bind *)
    6163 #X#Y#Z*normalize //
    62 |(* bind_ret *)
    63  #X*normalize //
    6464]
    6565qed.
     
    6767include "hints_declaration.ma".
    6868unification hint 0 ≔ X;
    69 M ≟ m_def Res
     69N ≟ max_def Res, M ≟ m_def N
    7070(*---------------*) ⊢
    7171res X ≡ monad M X
     
    9696interpretation "error monad sig Prod bind" 'sigbind2 e f = (sigbind2 ???? e f).*)
    9797
    98 lemma res_bind_inversion:
     98lemma bind_inversion:
    9999  ∀A,B: Type[0]. ∀f: res A. ∀g: A → res B. ∀y: B.
    100100  (f »= g = return y) →
     
    250250  ] (refl ? f).
    251251
    252 notation > "vbox('!' ident v 'as' ident E ← e; break e')" with precedence 40 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}.
     252notation > "vbox('do' ident v 'as' ident E ← e; break e')" with precedence 48 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}.
    253253
    254254definition bind2_eq ≝ λA,B,C:Type[0]. λf: res (A×B). λg: ∀a:A.∀b:B. f = OK ? 〈a,b〉 → res C.
     
    258258  ] (refl ? f).
    259259
    260 notation > "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'})}.
     260notation > "vbox('do' 〈ident v1, ident v2〉 'as' ident E ← e; break e')" with precedence 48 for @{ bind2_eq ??? ${e} (λ${ident v1}.λ${ident v2}.λ${ident E}.${e'})}.
    261261
    262262definition res_to_opt : ∀A:Type[0]. res A → option A ≝
    263263 λA.λv. match v with [ Error _ ⇒ None ? | OK v ⇒ Some … v].
    264264
     265(* aliases for backward compatibility *)
     266definition bind ≝ m_bind Res.
     267definition bind2 ≝ m_bind2 Res.
     268definition bind3 ≝ m_bind3 Res.
     269definition mmap ≝ m_mmap Res.
     270definition mmap_sigma ≝ m_mmap_sigma Res.
  • src/common/IOMonad.ma

    r1640 r1647  
    2424
    2525definition IOMonad ≝ λO,I.
    26   MakeMonad (mk_MonadDefinition
     26  MakeMonadProps
    2727  (* the monad *)
    2828  (IO O I)
     
    3131  (* bind *)
    3232  (bindIO O I)
    33   ???). / by /
    34 [(* bind_bind *)
     33  ???. / by /
     34[(* bind_ret *)
     35 #X#m elim m normalize // #o#f#Hi @interact_proper //
     36|(* bind_bind *)
    3537 #X#Y#Z#m#f#g elim m normalize [2,3://]
    3638 (* Interact *)
    3739  #o#f #Hi @interact_proper //
    38 |(* bind_ret *)
    39  #X#m elim m normalize // #o#f#Hi @interact_proper //
    4040]
    4141qed.
     
    4646
    4747unification hint 0 ≔ O, I, T;
    48   N ≟ IOMonad O I, M ≟ m_def N
     48  N ≟ IOMonad O I, M ≟ max_def N, M' ≟ m_def M
    4949(*******************************************) ⊢
    50   IO O I T ≡ monad M T
     50  IO O I T ≡ monad M' T
    5151.
    5252
     
    177177  P_io O I ? P (bindIO O I A B e f).
    178178#I #O #A #B #P' #P #e elim e;
    179 [ #out #k #IH #f #He #H whd in He ⊢ %; #res @IH /2/;
     179[ #out #k #IH #f #He #H whd in He ⊢ %; #res @IH /2 by /;
    180180| #v #f #He #H @H @He
    181181| //;
     
    187187  P_io O I ? P (bindIO2 O I A B C e f).
    188188#I #O #A #B #C #P' #P #e elim e;
    189 [ #out #k #IH #f #He #H whd in He ⊢ %; #res @IH /2/;
     189[ #out #k #IH #f #He #H whd in He ⊢ %; #res @IH /2 by /;
    190190| #v cases v; #v1 #v2 #f #He #H @H @He
    191191| //;
     
    213213#I #O #A #B #C #P #e #Q #R cases e; #e' cases e'; normalize;
    214214[ *;
    215 | #e'' cases e''; #a #b #Pab #H normalize; /2/;
     215| #e'' cases e''; #a #b #Pab #H normalize; /2 by _/;
    216216] qed.
    217217*)
  • src/utilities/bindLists.ma

    r1636 r1647  
    7878   @{ 'tnews $ts (λ${ident l} : $ty.$f) }.
    7979
    80 notation > "νν ident l × n opt('with' ident EQ) 'in' f" with precedence 47 for
     80notation > "νν ident l ^ n opt('with' ident EQ) 'in' f" with precedence 47 for
    8181 ${default
    8282   @{ 'sunews $n (λ${ident l}.λ${ident EQ}.$f) }
     
    8484 }.
    8585 
    86 notation > "νν ident l : ty × n opt('with' ident EQ) 'in' f" with precedence 47 for
     86notation > "νν ident l : ty ^ n opt('with' ident EQ) 'in' f" with precedence 47 for
    8787 ${default
    8888   @{ 'sunews $n (λ${ident l}:$ty.λ${ident EQ}.$f) }
     
    9090 }.
    9191 
    92 notation < "hvbox(νν \nbsp ident l : ty × n \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for
     92notation < "hvbox(νν \nbsp ident l : ty ^ n \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for
    9393   @{ 'sunews $n (λ${ident l} : $ty.λ${ident EQ} : $tyeq.$f) }.
    94 notation < "hvbox(νν_ n \nbsp ident l : ty × n \nbsp 'in' \nbsp break f)" with precedence 47 for
     94notation < "hvbox(νν_ n \nbsp ident l : ty ^ n \nbsp 'in' \nbsp break f)" with precedence 47 for
    9595   @{ 'unews $n (λ${ident l} : $ty.$f) }.
    9696
     
    112112 
    113113 
    114 coercion blist_from_list nocomposites :
     114coercion blist_from_list :
    115115  ∀B,T,E. ∀l:list E. bind_list B T E ≝ blist_of_list on _l : list ? to bind_list ???.
    116116
     
    154154 
    155155definition BindList ≝
    156   λB,T.MakeMonad (mk_MonadDefinition
     156  λB,T.MakeMonadProps
    157157  (* the monad *)
    158158  (λX.bind_list B T X)
     
    161161  (* bind *)
    162162  (bbind B T)
    163   ???).
    164 [(* bind_bind *)
     163  ???.
     164[(* ret_bind *)
     165  #X#Y#x#f normalize @bappend_bnil
     166|(* bind_ret *)
     167 #X#m elim m normalize /2 by /
     168 #t #l' #Hi @bnew_proper // normalize #s#t#eq destruct @Hi
     169|(* bind_bind *)
    165170 #X#Y#Z#m#f#g elim m normalize
    166171 [//
     
    169174 |(* case bnew *)
    170175  #t #l #Hi @bnew_proper //
     176  #x#y #x_eq_y destruct(x_eq_y) @Hi
    171177 ]
    172 |(* bind_ret *)
    173  #X#m elim m normalize /2 by /
    174  #t #l' #Hi @bnew_proper normalize // #s#t#eq destruct @Hi
    175 |(* ret_bind *)
    176   #X#Y#x#f normalize @bappend_bnil
    177178]
    178179qed.
     180
     181unification hint 0 ≔ B, T, X;
     182  N ≟ BindList B T, M ≟ max_def N, O ≟ m_def M
     183(*--------------------------------------------*) ⊢
     184  bind_list B T X ≡ monad O X.
    179185
    180186include "utilities/state.ma".
     
    195201theorem bcompile_append :
    196202  ∀E, R, T, U, fresh, bl1, bl2.
    197   bcompile E R T U fresh (bl1 @ bl2) ≅
     203  (bcompile E R T U fresh (bl1 @ bl2)) ≅
    198204  (
    199205  ! l1 ← bcompile … fresh bl1 ;
  • src/utilities/lists.ma

    r1631 r1647  
    5757] H.
    5858
     59include "utilities/monad.ma".
     60
     61definition Append : ∀A.Aop ? (nil A) ≝ λA.mk_Aop ? ? (append ?) ? ? ?.
     62// qed.
     63
     64definition List ≝ MakeMonadProps
     65  list
     66  (λX,x.[x])
     67  (λX,Y,l,f.\fold [append ?, [ ]]_{x ∈ l} (f x))
     68  ???. normalize
     69[ / by /
     70| #X#m elim m normalize //
     71| #X#Y#Z #m #f#g
     72  elim m normalize [//]
     73  #x#l' #Hi
     74  <(fold_sum ?? (f x) ? [ ] (Append ?))
     75  >Hi //
     76] qed.
     77
     78unification hint 0 ≔ X ;
     79N ≟ max_def List, M ≟ m_def N
     80(*---------------------------*)⊢
     81list X ≡ monad M X.
  • src/utilities/monad.ma

    r1640 r1647  
    77  monad : Type[0] → Type[0] ;
    88  m_return : ∀X. X → monad X ;
    9   m_bind : ∀X,Y. monad X → (X → monad Y) → monad Y;
    10   m_return_bind : ∀X,Y.∀x : X.∀f : X → monad Y.
    11     m_bind ?? (m_return ? x) f = f x ;
    12   m_bind_return : ∀X.∀m : monad X.
    13     m_bind ?? m (m_return ?) = m ;
    14   m_bind_bind : ∀X,Y,Z. ∀m : monad X.∀f : X → monad Y.∀g : Y → monad Z.
    15     m_bind ?? (m_bind ?? m f) g = m_bind ?? m (λx. m_bind ?? (f x) g)
     9  m_bind : ∀X,Y. monad X → (X → monad Y) → monad Y
    1610}.
    1711
    18 record SetoidMonadDefinition : Type[1] ≝ {
    19   std_monad : Type[0] → Setoid ;
    20   sm_return : ∀X. X → std_monad X ;
    21   sm_bind : ∀X,Y. std_monad X → (X → std_monad Y) → std_monad Y;
    22   sm_return_proper : ∀X. sm_return X ⊨ eq ? ++> std_eq …;
    23   sm_bind_proper : ∀X,Y.
    24     sm_bind X Y ⊨ std_eq … ++> (eq ? ++> std_eq …) ++> std_eq …;
    25   sm_return_bind : ∀X,Y : Setoid.∀x : X.∀f : X → std_monad Y.
    26     sm_bind ?? (sm_return ? x) f ≅ f x ;
    27   sm_bind_return : ∀X.∀m : std_monad X.
    28     sm_bind ?? m (sm_return ?) ≅ m ;
    29   sm_bind_bind : ∀X,Y,Z. ∀m : std_monad X.∀f : X → std_monad Y.∀g : Y → std_monad Z.
    30     sm_bind ?? (sm_bind ?? m f) g ≅ sm_bind ?? m (λx. sm_bind ?? (f x) g)
    31 }.
    32 
    33 notation "m »= f" with precedence 47
     12notation "m »= f" with precedence 49
    3413  for @{'m_bind $m $f) }.
    3514
     
    3716  with precedence 48 for @{'m_bind ${e} (λ_. ${e'})}.
    3817notation > "! ident v ← e; e'"
    39   with precedence 48 for @{'m_bind' (λ${ident v}. ${e'}) ${e}}.
     18  with precedence 48 for @{'m_bind ${e} (λ${ident v}. ${e'})}.
    4019notation > "! ident v : ty ← e; e'"
    4120  with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}.
    42 notation < "vbox(! \nbsp ident v ← e ; break e')"
     21notation < "vbox(! \nbsp ident v ← e ; break e')"
    4322  with precedence 48 for @{'m_bind ${e} (λ${ident v}.${e'})}.
    4423notation > "! ident v ← e : ty ; e'"
    4524  with precedence 48 for @{'m_bind (${e} : ${ty}) (λ${ident v}.${e'})}.
    46 notation < "vbox(! \nbsp ident v : ty ← e ; break e')"
     25notation < "vbox(! \nbsp ident v : ty \nbsp ←  \nbsp e ; break e')"
    4726  with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}.
    4827notation > "! ident v : ty ← e : ty' ; e'"
     
    5029notation > "! 〈ident v1, ident v2〉 ← e ; e'"
    5130  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}.
     31notation > "! 〈ident v1, ident v2〉 ← e : ty ; e'"
     32  with precedence 48 for @{'m_bind2 (${e} : $ty) (λ${ident v1}. λ${ident v2}. ${e'})}.
    5233notation > "! 〈ident v1 : ty1, ident v2 : ty2〉 ← e ; e'"
    5334  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}.
    5435notation < "vbox(! \nbsp 〈ident v1, ident v2〉 ← e ; break e')"
    5536  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}.
    56 notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 e ; break e')"
     37notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2〉  \nbsp ←  \nbsp e ; break e')"
    5738  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}.
    5839notation > "! 〈ident v1, ident v2, ident v3〉 ← e ; e'"
    5940  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1}. λ${ident v2}. λ${ident v3}. ${e'})}.
     41notation > "! 〈ident v1, ident v2, ident v3〉 ← e : ty ; e'"
     42  with precedence 48 for @{'m_bind3 (${e} : ${ty}) (λ${ident v1}. λ${ident v2}. λ${ident v3}. ${e'})}.
    6043notation > "! 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e ; e'"
    6144  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. λ${ident v3} : ${ty3}. ${e'})}.
    62 notation < "vbox(! \nbsp 〈ident v1, ident v2, ident v3〉 e ; break e')"
     45notation < "vbox(! \nbsp 〈ident v1, ident v2, ident v3〉 \nbsp ← \nbsp e ; break e')"
    6346  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1}. λ${ident v2}. λ${ident v3}. ${e'})}.
    64 notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e ; break e')"
     47notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 \nbsp ← e \nbsp ; break e')"
    6548  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. λ${ident v3} : ${ty3}. ${e'})}.
    6649
    67  
    68 (* "do" alternative notation for backward compatibility *)
     50(* dependent pair versions *)
     51notation > "! «ident v1, ident v2» ← e ; e'"
     52  with precedence 48 for
     53  @{'m_bind ${e} (λ${fresh p_sig}.
     54    match ${fresh p_sig} with [mk_Sig ${ident v1} ${ident v2} ⇒ ${e'}])}.
     55notation < "vbox(! \nbsp «ident v1, ident v2» \nbsp ← \nbsp e ; break e')"
     56  with precedence 48 for
     57  @{'m_bind ${e} (λ${fresh p_sig}.
     58    match ${fresh p_sig} with [mk_Sig ${ident v1} ${ident v2} ⇒ ${e'}])}.
     59   
     60notation > "! «ident v1, ident v2, ident H» ← e ; e'"
     61  with precedence 48 for
     62  @{'m_sigbind2 ${e} (λ${ident v1},${ident v2},${ident H}. ${e'})}.
     63notation < "vbox(! \nbsp «ident v1, ident v2, ident H» \nbsp ← \nbsp e ; e')"
     64  with precedence 48 for
     65  @{'m_sigbind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.
     66    λ${ident H} : ${ty3}. ${e'})}.
     67   
     68 
     69(*alternative do notation for backward compatibility *)
     70notation > "'do'_ e; e'"
     71  with precedence 48 for @{'m_bind ${e} (λ_. ${e'})}.
    6972notation > "'do' ident v ← e; e'"
    7073  with precedence 48 for @{'m_bind ${e} (λ${ident v}. ${e'})}.
    7174notation > "'do' ident v : ty ← e; e'"
    7275  with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}.
     76notation > "'do' ident v ← e : ty ; e'"
     77  with precedence 48 for @{'m_bind (${e} : ${ty}) (λ${ident v}.${e'})}.
     78notation > "'do' ident v : ty ← e : ty' ; e'"
     79  with precedence 48 for @{'m_bind (${e} : ${ty'}) (λ${ident v} : ${ty}. ${e'})}.
    7380notation > "'do' 〈ident v1, ident v2〉 ← e ; e'"
    7481  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}.
     
    7986notation > "'do' 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e ; e'"
    8087  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. λ${ident v3} : ${ty3}. ${e'})}.
    81  
     88
    8289(* dependent pair versions *)
    83 notation > "! «ident v1, ident v2» ← e ; e'"
     90notation > "'do' «ident v1, ident v2» ← e ; e'"
    8491  with precedence 48 for
    8592  @{'m_bind ${e} (λ${fresh p_sig}.
    8693    match ${fresh p_sig} with [mk_Sig ${ident v1} ${ident v2} ⇒ ${e'}])}.
    8794
    88 notation > "! «ident v1, ident v2, ident H» ← e ; e'"
    89   with precedence 48 for
    90   @{'m_bind ${e} (λ${fresh p_sig}.
    91     match ${fresh p_sig} with [mk_Sig ${fresh p} ${ident H} ⇒
    92       match ${fresh p} with [mk_Prod ${ident v1} ${ident v2} ⇒ ${e'}]])}.
    93 
    94 notation > "'do' «ident v1, ident v2» ← e ; e'"
    95   with precedence 48 for
    96   @{'m_bind ${e} (λ${fresh p_sig}.
    97     match ${fresh p_sig} with [mk_Sig ${ident v1} ${ident v2} ⇒ ${e'}])}.
    98 
    9995notation > "'do' «ident v1, ident v2, ident H» ← e ; e'"
    10096  with precedence 48 for
    101   @{'m_bind ${e} (λ${fresh p_sig}.
    102     match ${fresh p_sig} with [mk_Sig ${fresh p} ${ident H} ⇒
    103       match ${fresh p} with [mk_Prod ${ident v1} ${ident v2} ⇒ ${e'}]])}.
    104 
    105 notation > "'return' t" with precedence 46 for @{'m_return $t}.
    106 notation < "'return' \nbsp t" with precedence 46 for @{'m_return $t}.
    107 
    108 interpretation "setoid monad bind" 'm_bind m f = (sm_bind ? ? ? m f).
    109 interpretation "setoid monad bind'" 'm_bind' f m = (sm_bind ? ? ? m f).
    110 interpretation "setoid monad return" 'm_return x = (sm_return ? ? x).
     97  @{'m_sigbind2 ${e} (λ${ident v1},${ident v2},${ident H}. ${e'})}.
     98
     99notation > "'return' t" with precedence 49 for @{'m_return $t}.
     100notation < "'return' \nbsp t" with precedence 49 for @{'m_return $t}.
     101
    111102interpretation "monad bind" 'm_bind m f = (m_bind ? ? ? m f).
    112 interpretation "monad bind'" 'm_bind' f m = (m_bind ? ? ? m f).
    113103interpretation "monad return" 'm_return x = (m_return ? ? x).
    114104
     105
    115106include "basics/lists/list.ma".
     107
    116108
    117109(* add structure and properties as needed *)
     
    124116  m_bind3 : ∀X,Y,Z,W.monad m_def (X×Y×Z) → (X → Y → Z → monad m_def W) → monad m_def W;
    125117  m_join : ∀X.monad m_def (monad m_def X) → monad m_def X;
     118  m_sigbind2 : ∀A,B,C.∀P:A×B → Prop. monad m_def (Σx:A×B.P x) →
     119      (∀a,b. P 〈a,b〉 → monad m_def C) → monad m_def C;
    126120  m_mmap : ∀X,Y.(X → monad m_def Y) → list X → monad m_def (list Y);
    127121  m_mmap_sigma : ∀X,Y,P.(X → monad m_def (Σy : Y.P y)) → list X → monad m_def (Σl : list Y.All ? P l)
     
    130124interpretation "monad bind2" 'm_bind2 m f = (m_bind2 ? ? ? ? m f).
    131125interpretation "monad bind3" 'm_bind3 m f = (m_bind3 ? ? ? ? ? m f).
    132 
    133 (* notation breaks completely here.... *)
    134 definition mmap_sigma_helper : ∀M.∀X,Y,P.?→?→?→monad M (Σl : list Y.All ? P l) ≝
    135   λM.λX,Y:Type[0].λP.λf : X → monad M (Σy : Y.P y).
    136   λel.λmacc : monad M (Σl : list Y.All ? P l).
    137     m_bind M ?? (f el) (λp.
    138     match p with [mk_Sig r r_prf ⇒
    139     m_bind M ?? macc (λq.
    140     match q with [mk_Sig acc acc_prf ⇒
    141     return (mk_Sig … (r :: acc) ?)])]).
    142 whd %{r_prf acc_prf} qed.
    143 
    144 definition MakeMonad : MonadDefinition → Monad ≝ λM.
    145   mk_Monad M
     126interpretation "monad sigbind2" 'm_sigbind2 m f = (m_sigbind2 ????? m f).
     127
     128check (λM : Monad.λA,B,C,P.λp.λf : ∀a,b.P 〈a,b〉 → monad M C.! «a,b,H» ← p; f a b H)
     129
     130record MonadProps : Type[1] ≝
     131  { max_def :> Monad
     132  ; m_return_bind : ∀X,Y.∀x : X.∀f : X → monad max_def Y. ! y ← return x ; f y = f x
     133  ; m_bind_return : ∀X.∀m : monad max_def X.! x ← m ; return x = m
     134  ; m_bind_bind : ∀X,Y,Z. ∀m : monad max_def X.∀f : X → monad max_def Y.
     135      ∀g : Y → monad max_def Z.! y ← (! x ← m ; f x) ; g y = ! x ← m; ! y ← f x ; g y
     136  }.
     137
     138record SetoidMonadProps : Type[1] ≝
     139  { smax_def :> Monad
     140  ; sm_eq : ∀X.relation (monad smax_def X)
     141  ; sm_eq_refl : ∀X.reflexive ? (sm_eq X)
     142  ; sm_eq_trans : ∀X.transitive ? (sm_eq X)
     143  ; sm_eq_sym : ∀X.symmetric ? (sm_eq X)
     144  ; sm_return_proper : ∀X .m_return smax_def X ⊨ eq ? ++> sm_eq ?
     145  ; sm_bind_proper : ∀X, Y.m_bind smax_def X Y ⊨ sm_eq ? ++> (eq ? ++> sm_eq ?) ++> sm_eq ?
     146  ; sm_return_bind : ∀X,Y.∀x : X.∀f : X → monad smax_def Y.
     147      sm_eq Y (! y ← return x ; f y) (f x)
     148  ; sm_bind_return : ∀X.∀m : monad smax_def X.sm_eq X (! x ← m ; return x) m
     149  ; sm_bind_bind : ∀X,Y,Z. ∀m : monad smax_def X.∀f : X → monad smax_def Y.
     150      ∀g : Y → monad smax_def Z.sm_eq Z (! y ← (! x ← m ; f x) ; g y) (! x ← m; ! y ← f x ; g y)
     151  }.
     152
     153interpretation "monad setoid equality" 'std_eq x y = (sm_eq ?? x y).
     154
     155
     156definition MakeMonad : ?→?→?→Monad ≝ λmonad,m_return,m_bind.
     157  mk_Monad (mk_MonadDefinition monad m_return m_bind)
    146158  (* map *)
    147159  (λX,Y,f,m.
     
    164176  (* join *)
    165177  (λX,m.! x ← m ; x)
     178  (* m_sigbind2 *)
     179  (λA,B,C,P,e,f.
     180    ! e_sig ← e ;
     181    match e_sig with
     182    [ mk_Sig p p_prf ⇒
     183      match p return λx.x = p → ? with
     184      [ mk_Prod a b ⇒
     185      λeq_p.  f a b (eq_ind_r ?? (λx.λ_.P x) p_prf ? eq_p)
     186      ](refl …)
     187    ])
    166188  (λX,Y,f,l.foldr … (λel,macc.! r ← f el; !acc ← macc; return (r :: acc)) (return [ ]) l)
    167   (λX,Y,P,f,l.foldr … (mmap_sigma_helper M … f) (return (mk_Sig … [ ] ?)) l).
    168   % qed.
    169 
    170 
    171 (* add structure and properties as needed *)
    172 record SetoidMonad : Type[1] ≝ {
    173   sm_def :> SetoidMonadDefinition ;
    174   sm_map : ∀X, Y. (X → Y) → std_monad sm_def X → std_monad sm_def Y ;
    175   sm_map2 : ∀X, Y, Z. (X → Y → Z) →
    176     std_monad sm_def X → std_monad sm_def Y → std_monad sm_def Z;
    177   sm_bind2 : ∀X,Y,Z.std_monad sm_def (X×Y) →
    178     (X → Y → std_monad sm_def Z) → std_monad sm_def Z
    179 }.
    180 
    181 definition MakeSetoidMonad : SetoidMonadDefinition → SetoidMonad ≝ λM.
    182   mk_SetoidMonad M
    183   (* map *)
    184   (λX,Y,f,m.
    185     ! x ← m ;
    186     return f x)
    187   (* map2 *)
    188   (λX,Y,Z,f,m,n.
    189     ! x ← m ;
    190     ! y ← n ;
    191     return (f x y))
    192   (* bind2 *)
    193   (λX,Y,Z,m,f.
    194     ! p ← m ;
    195     let 〈x, y〉 ≝ p in
    196     f x y).
    197 
    198 interpretation "setoid monad bind2" 'm_bind2 m f = (sm_bind2 ? ? ? ? m f).
    199 
    200 record MonadTransformer : Type[1] ≝ {
    201   monad_trans : MonadDefinition → MonadDefinition ;
    202   m_lift : ∀M,X. monad M X → monad (monad_trans M) X ;
    203   m_lift_return : ∀M,X.∀x : X. m_lift M X (return x) = return x ;
    204   m_lift_bind : ∀M,X,Y.∀m : monad M X.∀f : X → monad M Y.
    205     m_lift … (! x ← m ; f x) = ! x ← m_lift … m ; m_lift … (f x)
    206 }.
     189  (λX,Y,P,f,l.foldr … (λel,macc.
     190    ! «r, r_prf» ← f el ;
     191    ! «acc, acc_prf» ← macc ;
     192    return (mk_Sig ?? (r :: acc) ?))
     193    (return (mk_Sig … [ ] ?)) l).
     194  % assumption qed.
     195
     196definition MakeMonadProps : ?→?→?→?→?→?→MonadProps ≝ λmonad,m_return,m_bind,p1,p2,p3.
     197mk_MonadProps (MakeMonad monad m_return m_bind) p1 p2 p3.
     198
     199definition MakeSetoidMonadProps : ?→?→?→?→?→?→?→?→?→?→?→?→SetoidMonadProps ≝
     200  λmonad,m_return,m_bind,sm_eq,p1,p2,p3,p4,p5,p6,p7,p8.
     201  mk_SetoidMonadProps (MakeMonad monad m_return m_bind) sm_eq p1 p2 p3 p4 p5 p6 p7 p8.
  • src/utilities/option.ma

    r1640 r1647  
    22include "basics/types.ma".
    33
    4 definition Option ≝ MakeMonad (mk_MonadDefinition
     4definition Option ≝ MakeMonadProps
    55  (* the monad *)
    66  option
     
    99  (* bind *)
    1010  (λX,Y,m,f. match m with [ Some x ⇒ f x | None ⇒ None ?])
    11   ???).
    12 // #X[#Y#Z]*normalize//qed.
     11  ???.
     12// #X[2:#Y#Z]*normalize//qed.
    1313
    1414include "hints_declaration.ma".
    1515unification hint 0 ≔ X;
    16 M ≟ m_def Option
     16N ≟ max_def Option, M ≟ m_def N
    1717(*---------------*) ⊢
    1818option X ≡ monad M X
     
    2424  | None ⇒ λeq_m.?
    2525  ] (refl …). elim (absurd … eq_m prf) qed.
    26 
    27 (* playground for notation problems *)
    28 
    29 inductive option_bis (X : Type[0]) : Type[0] ≝
    30 | Some' : X → option_bis X
    31 | None' : option_bis X.
    32 
    33 definition option_to_option' ≝ λX.λm : option X. match m with [ Some x ⇒ Some' ? x | None ⇒ None' ?].
    34 
    35 coercion o_to_o' : ∀X.∀m : option X. option_bis X ≝ option_to_option'
    36   on _m : option ? to option_bis ?.
    37  
    38 
    39 definition Option_bis ≝ MakeMonad (mk_MonadDefinition
    40   option_bis
    41   (λX.Some' X)
    42   (λX,Y,m,f.match m with [Some' x ⇒ f x | None' ⇒ None' ?])
    43   ???). //
    44 #X[#Y#Z] * normalize // qed.
    45 
    46 unification hint 0 ≔ X ;
    47 M ≟ m_def Option_bis
    48 (*---------------*) ⊢
    49 option_bis X ≡ monad M X
    50 .
    51 
    52 (* does not typecheck
    53 check (λX.λm : option_bis X.λn : option X.! x ← n ; m)
    54 *)
  • src/utilities/state.ma

    r1635 r1647  
    11include "utilities/monad.ma".
    22
    3 definition state_setoid ≝ λS,X : Type[0].
    4   mk_Setoid (S → S × X)
    5     (λf,g.∀x.f x = g x) ???.
    6 //qed.
    7 
    83definition State ≝
    9   λS : Type[0].MakeSetoidMonad (mk_SetoidMonadDefinition
     4  λS : Type[0].MakeSetoidMonadProps
    105  (* the monad *)
    11   (state_setoid S)
     6  (λX.S → S × X)
    127  (* return *)
    138  (λX,x,s.〈s,x〉)
    149  (* bind *)
    1510  (λX,Y,m,f,s. let 〈s', x〉 ≝ m s in f x s')
    16   ?????).
    17 / by /
    18 [(* bind_bind *)
    19  #X#Y#Z#m#f#g#s
    20  elim (m s) #s' #x normalize
    21  elim (f x s') #s'' #y normalize //
    22 |(* bind_ret *)
    23  #X#m#s elim (m s) #s' #x normalize //
    24 |(*bind proper*)
    25   #X#Y#m#n#eqmn#f#g#eqfg#s
    26  generalize in match (eqmn s); -eqmn
    27  elim (m s) #s' #x normalize
    28  elim (n s) #s'' #x' normalize
    29  #E destruct
    30  /2 by /
     11  (* monad eq *)
     12  (λX,c1,c2.∀s.c1 s = c2 s)
     13  ????????.
     14//
     15#X
     16[ (* bind_proper *)
     17  #Y #m#n #m_eq_n
     18  #f #g #f_eq_g
     19  #s
     20  generalize in match (m_eq_n s); -m_eq_n
     21  normalize
     22  #m_eq_n >m_eq_n -m_eq_n
     23  elim (n s) #s' #y
     24  normalize @f_eq_g //
     25| #m#s normalize
     26  elim (m s) normalize /2 by /
     27| #Y #Z #m #f #g #s normalize
     28  elim (m s) normalize
     29  #s' #x
     30  elim (f x s') normalize
     31  #s'' #y //
    3132]
    3233qed.
    3334
    34 definition state_monad ≝ λS.std_monad (State S).
     35definition state_monad ≝ λS.monad (State S).
    3536
    3637definition state_get : ∀S.state_monad S S ≝ λS,s.〈s,s〉.
     
    4041include "hints_declaration.ma".
    4142unification hint 0 ≔ S,X;
    42 M ≟ State S
     43N ≟ State S, M ≟ smax_def N, O ≟ m_def M
    4344(*---------------*) ⊢
    44 state_monad S X ≡ std_monad (sm_def M) X
     45state_monad S X ≡ monad O X
    4546.
    4647
Note: See TracChangeset for help on using the changeset viewer.