Changeset 1640 for src


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
Location:
src
Files:
1 added
10 edited

Legend:

Unmodified
Added
Removed

  • src/RTL/RTL_paolo.ma

    r1636 r1640  
    2525  | rtl_st_ext_tailcall_ptr: register → register → list rtl_argument → rtl_statement_extension.
    2626
    27  
    28 inductive rtl_move : Type[0] ≝
    29   | CARRY : bool → rtl_move
    30   | REG : register → rtl_argument → rtl_move.
    31  
    32 (* avoid expansion *)
    33 definition rtl_params : graph_params ≝ mk_graph_params
     27definition rtl_params ≝ mk_graph_params (mk_unserialized_params
    3428  (mk_inst_params
    3529    (* acc_a_reg ≝ *) register
    … …  
    4236    (* dph_arg   ≝ *) rtl_argument
    4337    (* snd_arg   ≝ *) rtl_argument
    44     (* operator1 ≝ *) Op1
    45     (* operator2 ≝ *) Op2
    46     (* pair_move ≝ *) rtl_move
     38    (* pair_move ≝ *) (register × rtl_argument)
    4739    (* call_args ≝ *) (list rtl_argument)
    4840    (* call_dest ≝ *) (list register)
    … …  
    5345      (* resultT ≝ *) (list register)
    5446      (* paramsT ≝ *) (list register))
    55       (* localsT ≝ *) (list register)).
     47      (* localsT ≝ *) (list register))).
     48
     49interpretation "move" 'mov r a = (MOVE ? ? (mk_Prod ?? r a)).
    5650
    5751(* aid unification *)
    … …  
    5953unification hint 0 ≔
    6054(*---------------*) ⊢
    61 acc_a_reg (g_inst_pars rtl_params) ≡ register.
     55acc_a_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
    6256unification hint 0 ≔
    6357(*---------------*) ⊢
    64 acc_b_reg (g_inst_pars rtl_params) ≡ register.
     58acc_b_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
    6559unification hint 0 ≔
    6660(*---------------*) ⊢
    67 acc_a_arg (g_inst_pars rtl_params) ≡ rtl_argument.
     61acc_a_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
    6862unification hint 0 ≔
    6963(*---------------*) ⊢
    70 acc_b_arg (g_inst_pars rtl_params) ≡ rtl_argument.
     64acc_b_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
    7165unification hint 0 ≔
    7266(*---------------*) ⊢
    73 dpl_reg (g_inst_pars rtl_params) ≡ register.
     67dpl_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
    7468unification hint 0 ≔
    7569(*---------------*) ⊢
    76 dph_reg (g_inst_pars rtl_params) ≡ register.
     70dph_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register.
    7771unification hint 0 ≔
    7872(*---------------*) ⊢
    79 dpl_arg (g_inst_pars rtl_params) ≡ rtl_argument.
     73dpl_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
    8074unification hint 0 ≔
    8175(*---------------*) ⊢
    82 dph_arg (g_inst_pars rtl_params) ≡ rtl_argument.
     76dph_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
    8377unification hint 0 ≔
    8478(*---------------*) ⊢
    85 snd_arg (g_inst_pars rtl_params) ≡ rtl_argument.
     79snd_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument.
    8680unification hint 0 ≔
    8781(*---------------*) ⊢
    88 operator1 (g_inst_pars rtl_params) ≡ Op1.
     82pair_move (u_inst_pars (g_u_pars rtl_params)) ≡ register × rtl_argument.
    8983unification hint 0 ≔
    9084(*---------------*) ⊢
    91 operator2 (g_inst_pars rtl_params) ≡ Op2.
     85call_args (u_inst_pars (g_u_pars rtl_params)) ≡ list rtl_argument.
    9286unification hint 0 ≔
    9387(*---------------*) ⊢
    94 pair_move (g_inst_pars rtl_params) ≡ rtl_move.
    95 unification hint 0 ≔
    96 (*---------------*) ⊢
    97 call_args (g_inst_pars rtl_params) ≡ list rtl_argument.
    98 unification hint 0 ≔
    99 (*---------------*) ⊢
    100 call_dest (g_inst_pars rtl_params) ≡ list register.
     88call_dest (u_inst_pars (g_u_pars rtl_params)) ≡ list register.
    10189
    102 check (λglobals,r.OP2 rtl_params globals Or r r r)
    10390
    10491definition rtl_instruction ≝ joint_instruction rtl_params.
    105 definition rtl_statement ≝ joint_statement rtl_params.
    106 
    107 
    108 definition reg_from_nat : ∀globals.register → ℕ → rtl_instruction globals ≝
    109   λglobals,r,k.
    110   MOVE rtl_params globals (REG r (imm_nat k)).
    111 
    112 definition reg_from_byte : ∀globals.register → Byte → rtl_instruction globals ≝
    113   λglobals,r,k.
    114   MOVE rtl_params globals (REG r (Imm k)).
    115 
    116 definition reg_from_reg : ∀globals.register → register → rtl_instruction globals ≝
    117   λglobals,r,k.
    118   MOVE … (REG r (Reg k)).
    119 
    120 definition set_carry : ∀globals.rtl_instruction globals ≝
    121   λglobals.MOVE … (CARRY true).
    122 
    123 definition clear_carry : ∀globals.rtl_instruction globals ≝
    124   λglobals.MOVE … (CARRY false).
    125  
     92(* Paolo: can't understand why coercions do not compose implicitly here *)
     93definition rtl_statement ≝ joint_statement (rtl_params : params).
    12694
    12795definition rtl_internal_function ≝
    … …  
    136104  | rtlntc_st_ext_call_ptr: register → register → list register → list register → rtlntc_statement_extension.
    137105
    138 definition rtlntc_params : graph_params ≝ mk_graph_params
     106definition rtlntc_params ≝ mk_graph_params (mk_unserialized_params
    139107  (mk_inst_params
    140108    (* acc_a_reg ≝ *) register
    … …  
    147115    (* dph_arg   ≝ *) rtl_argument
    148116    (* snd_arg   ≝ *) rtl_argument
    149     (* operator1 ≝ *) Op1
    150     (* operator2 ≝ *) Op2
    151     (* pair_move ≝ *) rtl_move
     117    (* pair_move ≝ *) (register × rtl_argument)
    152118    (* call_args ≝ *) (list rtl_argument)
    153119    (* call_dest ≝ *) (list register)
    … …  
    158124      (* resultT ≝ *) (list register)
    159125      (* paramsT ≝ *) (list register))
    160       (* localsT ≝ *) (list register)).
     126      (* localsT ≝ *) (list register))).
    161127
    162 definition rtlntc_statement ≝ joint_statement rtlntc_params.
     128definition rtlntc_statement ≝ joint_statement (rtlntc_params : params).
    163129
    164130definition rtlntc_internal_function ≝

  • src/RTLabs/RTLabsToRTL_paolo.ma

    r1636 r1640  
    88include alias "ASM/BitVector.ma".
    99include alias "arithmetics/nat.ma".
    10 
    11 
    12 (* Paolo: to be moved elsewhere *)
    13 
    14 notation "r ← a1 .op. a2" with precedence 50 for
    15   @{'op2 $op $r $a1 $a2}.
    16 notation "r ← . op . a" with precedence 50 for
    17   @{'op1 $op $r $a}.
    18 notation "r ← a" with precedence 50 for
    19   @{'mov $r $a}.
    20 notation "❮r, s❯ ← a1 . op . a2" with precedence 50 for
    21   @{'opaccs $op $r $s $a1 $a2}.
    22 
    23 interpretation "op2" 'op2 op r a1 a2 = (OP2 ? ? op r a1 a2).
    24 interpretation "op1" 'op1 op r a = (OP1 ? ? op r a).
    25 interpretation "move" 'mov r a = (MOVE ? ? (REG r a)).
    26 interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2).
    2710
    2811
    … …  
    141124    eqb m n = true → m = n.
    142125    #m#n@eqb_elim // #_ #F destruct(F) qed.
    143    
     126
    144127definition translate_op:
    145128  ∀globals. Op2 →
    … …  
    161144  (* first, clear carry if op relies on it *)
    162145  match op with
    163   [ Addc ⇒ [clear_carry ?]
    164   | Sub ⇒ [clear_carry ?]
     146  [ Addc ⇒ [CLEAR_CARRY ??]
     147  | Sub ⇒ [CLEAR_CARRY ??]
    165148  | _ ⇒ [ ]
    166149  ] @
    … …  
    228211      match split_into_bytes size const with
    229212      [ mk_Sig bytes bytes_length_proof ⇒
    230         map2 … (reg_from_byte globals) destrs bytes ?
     213        map2 … (λr.λb : Byte.r ← (b : rtl_argument)) destrs bytes ?
    231214      ]
    232215    | Ofloatconst float ⇒ λ_.⊥
    … …  
    374357    | cons srcr srcrs' ⇒
    375358      let f : register → rtl_instruction globals ≝
    376         λr. OP2 ?? Or destr (Reg destr) (Reg r) in
    377       reg_from_reg … srcr destr ::
     359        λr. destr ← destr .Or. r in
     360      MOVE rtl_params globals 〈destr,srcr〉 ::
    378361      map … f srcrs' @
    379362      (* now destr is non-null iff srcrs was non-null *)
    380       clear_carry … ::
     363      CLEAR_CARRY ? ? ::
    381364      (* many uses of 0, better not use immediates *)
    382365      ν tmp in
    … …  
    420403  ]
    421404qed.
     405
     406include alias "arithmetics/nat.ma".
    422407
    423408let rec range_strong_internal (start : ℕ) (count : ℕ)
    … …  
    615600          acc in
    616601        let epilogue : list (rtl_instruction globals) ≝
    617           [ clear_carry … ;
     602          [ CLEAR_CARRY … ;
    618603            tmpr ← 0 .Sub. destr ;
    619604            (* now carry bit is 1 iff destrs != 0 *)
    … …  
    782767  | cons srcr srcrs' ⇒
    783768    ν tmpr in
    784     let f ≝ λr. OP2 rtl_params globals Or tmpr (Reg tmpr) (Reg r) in
    785     reg_from_reg globals tmpr srcr ::
     769    let f : register → rtl_instruction globals ≝
     770      λr. tmpr ← tmpr .Or. r in
     771    MOVE rtl_params globals 〈tmpr,srcr〉 ::
    786772    map … f srcrs' @
    787     [ COND … tmpr lbl_true ]
     773    [ COND ?? tmpr lbl_true ]
    788774  ].
    789775
    … …  
    926912  let 〈lenv,runiverse〉 ≝ initialize_local_env runiverse
    927913    (f_params def @ f_locals def) (f_result def) in
    928   let params ≝ map_list_local_env lenv (map … \fst (f_params def)) in
     914  let parameters ≝ map_list_local_env lenv (map … \fst (f_params def)) in
    929915  let locals ≝ map_list_local_env lenv (map … \fst (f_locals def)) in
    930916  let result ≝
    … …  
    939925  let runiverse' ≝ runiverse in
    940926  let result' ≝ result in
    941   let params' ≝ params in
     927  let params' ≝ parameters in
    942928  let locals' ≝ locals in
    943929  let stack_size' ≝ f_stacksize def in
    944930  let entry' ≝ f_entry def in
    945931  let exit' ≝ f_exit def in
    946   let graph' ≝ add LabelTag ? (empty_map LabelTag ?) entry' (GOTO rtl_params globals entry') in
    947   let graph' ≝ add LabelTag ? graph' exit' (RETURN rtl_params globals) in
     932  let graph' ≝ add LabelTag ? (empty_map LabelTag ?) entry'
     933    (GOTO (rtl_params : params) globals entry') in
     934  let graph' ≝ add LabelTag ? graph' exit'
     935    (RETURN (rtl_params : params) globals) in
    948936  let res ≝
    949937    mk_joint_internal_function globals rtl_params luniverse' runiverse' result' params'

  • 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(*

  • src/joint/Joint_paolo.ma

    r1635 r1640  
    66
    77(* Here is the structure of parameter records (downward edges are coercions,
    8    the ¦ edge is the only explicitly defined coercion):
    9 
    10        _____graph_params___
    11       /           ¦        \
    12      /         params       \
    13     /         /      \      |
    14    / stmt_params      local_params
    15    \    |                  |
     8   the ↓ edges are the only explicitly defined coercions). lin_params and
     9   graph_params are simple wrappers of unserialized_params, and the coercions
     10   from them to params instantiate the missing bits with values for linarized
     11   programs and graph programs respectively.
     12
     13        lin_params      graph_params
     14          |       \_____ /____   |
     15          |             /     \  |
     16          \_______     /      ↓  ↓
     17                  \   _\____ params
     18                   \_/  \      |
     19                    / \  \     ↓
     20              _____/   unserialized_params
     21             /      _______/   |
     22            /      /           |
     23     stmt_params  /   local_params
     24        |      __/             |
    1625    inst_params       funct_params
    1726
    … …  
    3443 ; dph_arg: Type[0]   (* high address registers *)
    3544 ; snd_arg : Type[0]  (* second argument of binary op *)
    36  ; operator1 : Type[0] (* = Op1 in all but RTLabs *)
    37  ; operator2 : Type[0] (* = Op2 in all but RTLabs *)
    3845 ; pair_move: Type[0] (* argument of move instructions *)
    3946 ; call_args: Type[0] (* arguments of function calls *)
    … …  
    5158  | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals
    5259  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_instruction p globals
    53   | OP1: operator1 p → acc_a_reg p → acc_a_reg p → joint_instruction p globals
    54   | OP2: operator2 p → acc_a_reg p → acc_a_arg p → snd_arg p → joint_instruction p globals
    55   (* int, clear and set carry can be done with generic move *)
    56 (*| INT: generic_reg p → Byte → joint_instruction p globals
     60  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_instruction p globals
     61  | OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_instruction p globals
     62  (* int done with generic move *)
     63(*| INT: generic_reg p → Byte → joint_instruction p globals *)
    5764  | CLEAR_CARRY: joint_instruction p globals
    58   | SET_CARRY: joint_instruction p globals *)
     65  | SET_CARRY: joint_instruction p globals
    5966  | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_instruction p globals
    6067  | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_instruction p globals
    … …  
    6269  | COND: acc_a_reg p → label → joint_instruction p globals
    6370  | extension: extend_statements p → joint_instruction p globals.
     71
     72(* Paolo: to be moved elsewhere *)
     73
     74notation "r ← a1 .op. a2" with precedence 50 for
     75  @{'op2 $op $r $a1 $a2}.
     76notation "r ← . op . a" with precedence 50 for
     77  @{'op1 $op $r $a}.
     78notation "r ← a" with precedence 50 for
     79  @{'mov $r $a}. (* to be set in individual languages *)
     80notation "❮r, s❯ ← a1 . op . a2" with precedence 50 for
     81  @{'opaccs $op $r $s $a1 $a2}.
     82
     83interpretation "op2" 'op2 op r a1 a2 = (OP2 ? ? op r a1 a2).
     84interpretation "op1" 'op1 op r a = (OP1 ? ? op r a).
     85interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2).
     86
     87
    6488
    6589definition inst_forall_labels : ∀p : inst_params.∀globals.
    … …  
    7094  | _ ⇒ True
    7195 ].
    72 
    73 record stmt_params : Type[1] ≝
    74   { inst_pars :> inst_params
    75   ; succ : Type[0]
    76   ; succ_choice : (succ = label) + (succ = unit)
    77   }.
    78 
    79 inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
    80   | sequential: joint_instruction p globals → succ p → joint_statement p globals
    81   | GOTO: label → joint_statement p globals
    82   | RETURN: joint_statement p globals.
    83 
    84 (* for all labels in statement. Uses succ_choice to consider the successor of
    85    a statement when such successors are labels *)
    86 definition stmt_forall_labels : ∀p : stmt_params.∀globals.
    87     (label → Prop) → joint_statement p globals → Prop.
    88 *#i_pr#succ#succ_choice#globals#P*
    89 [#instr cases succ_choice #eq >eq #next
    90   [@(inst_forall_labels … P instr ∧ P next)
    91   |@(inst_forall_labels … P instr)
    92   ]
    93 |@P
    94 |@True
    95 ]qed.
    9696
    9797record funct_params : Type[1] ≝
    … …  
    105105 }.
    106106
     107record unserialized_params : Type[1] ≝
     108 { u_inst_pars :> inst_params
     109 ; u_local_pars :> local_params
     110 }.
     111
     112record stmt_params : Type[1] ≝
     113  { unserialized_pars :> unserialized_params
     114  ; succ : Type[0]
     115  ; succ_forall_labels : (label → Prop) → succ → Prop
     116  }.
     117
     118inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
     119  | sequential: joint_instruction p globals → succ p → joint_statement p globals
     120  | GOTO: label → joint_statement p globals
     121  | RETURN: joint_statement p globals.
     122
    107123record params : Type[1] ≝
    108124 { stmt_pars :> stmt_params
    109  ; local_pars :> local_params
    110125 ; codeT: list ident → Type[0]
    111126 ; lookup: ∀globals.codeT globals → label → option (joint_statement stmt_pars globals)
    112127 }.
    113128
     129
     130(* for all labels in statement. Uses succ_choice to consider the successor of
     131   a statement when such successors are labels *)
     132definition stmt_forall_labels : ∀p : stmt_params.∀globals.
     133    (label → Prop) → joint_statement p globals → Prop ≝
     134  λp,g,P,stmt. match stmt with
     135  [ sequential inst next ⇒ inst_forall_labels p g P inst ∧ succ_forall_labels p P next
     136  | GOTO l ⇒ P l
     137  | RETURN ⇒ True
     138  ].
     139
     140record lin_params : Type[1] ≝
     141  { l_u_pars :> unserialized_params }.
     142
     143include "utilities/option.ma".
     144
     145definition lin_params_to_params ≝
     146  λlp : lin_params. mk_params
     147    (mk_stmt_params lp unit (λ_.λ_.True))
     148    (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals)))
     149    (* lookup ≝ *)(λglobals,code,lbl.find ??
     150        (λl_stmt. let 〈lbl_opt, stmt〉 ≝ l_stmt in
     151          ! lbl' ← lbl_opt ;
     152          if eq_identifier … lbl lbl' then return stmt else None ?) code).
     153
     154coercion lp_to_p : ∀lp : lin_params.params ≝ lin_params_to_params
     155  on _lp : lin_params to params.
     156
    114157record graph_params : Type[1] ≝
    115  { g_inst_pars :> inst_params
    116  ; g_local_pars :> local_params
    117  }.
     158  { g_u_pars :> unserialized_params }.
     159
     160include alias "common/Graphs.ma". (* To pick the right lookup *)
     161
     162(* One common instantiation of params via Graphs of joint_statements
     163   (all languages but LIN) *)
     164definition graph_params_to_params ≝
     165  λgp : graph_params. mk_params
     166    (mk_stmt_params gp label (λP.P))
     167    (* codeT ≝ *)(λglobals.graph (joint_statement ? globals))
     168    (* lookup ≝ *)(λglobals.lookup …).
     169   
     170coercion gp_to_p : ∀gp:graph_params.params ≝ λgp.graph_params_to_params gp
     171on _gp : graph_params to params.
     172   
    118173
    119174definition labels_present : ∀p : params.∀globals.
    … …  
    130185    forall_stmts … (labels_present … code) code.
    131186
    132 include alias "common/Graphs.ma". (* To pick the right lookup *)
    133 
    134 
    135 (* One common instantiation of params via Graphs of joint_statements
    136    (all languages but LIN) *)
    137 definition params_of_graph_params: graph_params → params ≝
    138  λgp.
    139   let stmt_pars ≝ mk_stmt_params gp label (inl … (refl …)) in
    140   mk_params
    141    stmt_pars
    142    gp
    143    (* codeT ≝ *)(λglobals.graph (joint_statement stmt_pars globals))
    144    (λglobals.lookup …).
    145    
    146 coercion graph_params_to_params :
    147   ∀gp : graph_params.params ≝
    148     λgp.params_of_graph_params gp
    149     on _gp : graph_params to params.
    150 
    151187(* CSC: special case where localsT is a list of registers (RTL and ERTL) *)
    152 definition rtl_ertl_params ≝ λinst_pars,funct_pars.
    153   params_of_graph_params (mk_graph_params inst_pars (mk_local_params funct_pars (list register))).
     188definition rtl_ertl_params : ?→?→params ≝ λinst_pars,funct_pars.
     189  (mk_graph_params (mk_unserialized_params inst_pars (mk_local_params funct_pars (list register)))).
    154190
    155191record joint_internal_function (globals: list ident) (p:params) : Type[0] ≝

  • src/joint/TranslateUtils_paolo.ma

    r1635 r1640  
    104104  joint_internal_function globals dst_g_pars ≝
    105105  λsrc_g_pars,dst_g_pars,globals,registerT,fresh_reg,trans,empty,def.
    106   let f : label → joint_statement src_g_pars globals →
     106  let f : label → joint_statement (src_g_pars : params) globals →
    107107    joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝
    108108    λlbl,stmt,def.
    … …  
    128128  joint_internal_function … dst_g_pars ≝
    129129  λsrc_g_pars,dst_g_pars,globals,trans,empty,def.
    130   let f : label → joint_statement src_g_pars globals →
     130  let f : label → joint_statement (src_g_pars : params) globals →
    131131    joint_internal_function … dst_g_pars → joint_internal_function … dst_g_pars ≝
    132132    λlbl,stmt,def.

  • src/utilities/monad.ma

    r1635 r1640  
    33include "utilities/setoids.ma".
    44include "utilities/proper.ma".
    5 
     5 
    66record MonadDefinition : Type[1] ≝ {
    77  monad : Type[0] → Type[0] ;
    … …  
    3737  with precedence 48 for @{'m_bind ${e} (λ_. ${e'})}.
    3838notation > "! ident v ← e; e'"
    39   with precedence 48 for @{'m_bind ${e} (λ${ident v}. ${e'})}.
     39  with precedence 48 for @{'m_bind' (λ${ident v}. ${e'}) ${e}}.
    4040notation > "! ident v : ty ← e; e'"
    4141  with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}.
    4242notation < "vbox(! \nbsp ident v ← e ; break e')"
    4343  with precedence 48 for @{'m_bind ${e} (λ${ident v}.${e'})}.
     44notation > "! ident v ← e : ty ; e'"
     45  with precedence 48 for @{'m_bind (${e} : ${ty}) (λ${ident v}.${e'})}.
    4446notation < "vbox(! \nbsp ident v : ty ← e ; break e')"
    4547  with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}.
     48notation > "! ident v : ty ← e : ty' ; e'"
     49  with precedence 48 for @{'m_bind (${e} : ${ty'}) (λ${ident v} : ${ty}. ${e'})}.
    4650notation > "! 〈ident v1, ident v2〉 ← e ; e'"
    4751  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}.
    … …  
    5256notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e ; break e')"
    5357  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}.
     58notation > "! 〈ident v1, ident v2, ident v3〉 ← e ; e'"
     59  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1}. λ${ident v2}. λ${ident v3}. ${e'})}.
     60notation > "! 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e ; e'"
     61  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. λ${ident v3} : ${ty3}. ${e'})}.
     62notation < "vbox(! \nbsp 〈ident v1, ident v2, ident v3〉 ← e ; break e')"
     63  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1}. λ${ident v2}. λ${ident v3}. ${e'})}.
     64notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e ; break e')"
     65  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. λ${ident v3} : ${ty3}. ${e'})}.
     66
     67 
     68(* "do" alternative notation for backward compatibility *)
     69notation > "'do' ident v ← e; e'"
     70  with precedence 48 for @{'m_bind ${e} (λ${ident v}. ${e'})}.
     71notation > "'do' ident v : ty ← e; e'"
     72  with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}.
     73notation > "'do' 〈ident v1, ident v2〉 ← e ; e'"
     74  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}.
     75notation > "'do' 〈ident v1 : ty1, ident v2 : ty2〉 ← e ; e'"
     76  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}.
     77notation > "'do' 〈ident v1, ident v2, ident v3〉 ← e ; e'"
     78  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1}. λ${ident v2}. λ${ident v3}. ${e'})}.
     79notation > "'do' 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e ; e'"
     80  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. λ${ident v3} : ${ty3}. ${e'})}.
    5481 
    55 notation > "'return' t" with precedence 30 for @{'m_return $t}.
    56 notation < "'return' \nbsp t" with precedence 30 for @{'m_return $t}.
    57 
    58 (*
    59 notation > "!!_ e; e'"
    60   with precedence 40 for @{'sm_bind ${e} (λ_.${e'})}.
    61 notation > "!! ident v ← e; e'"
    62   with precedence 40 for @{'sm_bind ${e} (λ${ident v}.${e'})}.
    63 notation > "!! ident v : ty ← e; e'"
    64   with precedence 40 for @{'sm_bind ${e} (λ${ident v} : ${ty}.${e'})}.
    65 notation < "vbox(!!  ident v ← e; break e')"
    66   with precedence 40 for @{'sm_bind ${e} (λ${ident v}.${e'})}.
    67 notation < "vbox(!!  ident v : ty ← e; break e')"
    68   with precedence 40 for @{'sm_bind ${e} (λ${ident v} : ${ty}.${e'})}.
    69 notation > "!! 〈ident v1, ident v2〉 ← e; e'"
    70   with precedence 40 for @{'sm_bind ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
    71 notation > "!! 〈ident v1 : ty1, ident v2 : ty2〉 ← e; e'"
    72   with precedence 40 for @{'sm_bind ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.
    73 notation < "vbox(!! \nbsp 〈ident v1, ident v2〉 ← e; break e')"
    74   with precedence 40 for @{'sm_bind ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
    75 notation < "vbox(!! \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')"
    76   with precedence 40 for @{'sm_bind ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.
    77 
    78 notation "m !»= f" with precedence 40
    79   for @{'sm_bind $m $f) }.
    80 
    81 notation "'sreturn' t" with precedence 30 for @{'sm_return $t}.
    82 
    83 interpretation "setoid monad bind" 'sm_bind m f = (sm_bind ? ? ? m f).
    84 interpretation "setoid monad return" 'sm_return x = (sm_return ? ? x).
    85 *)
     82(* dependent pair versions *)
     83notation > "! «ident v1, ident v2» ← e ; e'"
     84  with precedence 48 for
     85  @{'m_bind ${e} (λ${fresh p_sig}.
     86    match ${fresh p_sig} with [mk_Sig ${ident v1} ${ident v2} ⇒ ${e'}])}.
     87
     88notation > "! «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
     94notation > "'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
     99notation > "'do' «ident v1, ident v2, ident H» ← e ; e'"
     100  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
     105notation > "'return' t" with precedence 46 for @{'m_return $t}.
     106notation < "'return' \nbsp t" with precedence 46 for @{'m_return $t}.
    86107
    87108interpretation "setoid monad bind" 'm_bind m f = (sm_bind ? ? ? m f).
     109interpretation "setoid monad bind'" 'm_bind' f m = (sm_bind ? ? ? m f).
    88110interpretation "setoid monad return" 'm_return x = (sm_return ? ? x).
    89111interpretation "monad bind" 'm_bind m f = (m_bind ? ? ? m f).
     112interpretation "monad bind'" 'm_bind' f m = (m_bind ? ? ? m f).
    90113interpretation "monad return" 'm_return x = (m_return ? ? x).
     114
     115include "basics/lists/list.ma".
    91116
    92117(* add structure and properties as needed *)
    … …  
    97122    monad m_def X → monad m_def Y → monad m_def Z;
    98123  m_bind2 : ∀X,Y,Z.monad m_def (X×Y) → (X → Y → monad m_def Z) → monad m_def Z;
    99   m_join : ∀X.monad m_def (monad m_def X) → monad m_def X
    100 }.
     124  m_bind3 : ∀X,Y,Z,W.monad m_def (X×Y×Z) → (X → Y → Z → monad m_def W) → monad m_def W;
     125  m_join : ∀X.monad m_def (monad m_def X) → monad m_def X;
     126  m_mmap : ∀X,Y.(X → monad m_def Y) → list X → monad m_def (list Y);
     127  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)
     128}.
     129
     130interpretation "monad bind2" 'm_bind2 m f = (m_bind2 ? ? ? ? m f).
     131interpretation "monad bind3" 'm_bind3 m f = (m_bind3 ? ? ? ? ? m f).
     132
     133(* notation breaks completely here.... *)
     134definition 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) ?)])]).
     142whd %{r_prf acc_prf} qed.
    101143
    102144definition MakeMonad : MonadDefinition → Monad ≝ λM.
    … …  
    116158    let 〈x, y〉 ≝ p in
    117159    f x y)
     160  (λX,Y,Z,W,m,f.
     161    ! p ← m ;
     162    let 〈x, y, z〉 ≝ p in
     163    f x y z)
    118164  (* join *)
    119   (λX,m.! x ← m ; x).
     165  (λX,m.! x ← m ; x)
     166  (λ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
    120171(* add structure and properties as needed *)
    121172record SetoidMonad : Type[1] ≝ {
    … …  
    145196    f x y).
    146197
    147 interpretation "monad bind2" 'm_bind2 m f = (sm_map2 ? ? ? ? m f).
    148 
     198interpretation "setoid monad bind2" 'm_bind2 m f = (sm_bind2 ? ? ? ? m f).
    149199
    150200record MonadTransformer : Type[1] ≝ {
    … …  
    155205    m_lift … (! x ← m ; f x) = ! x ← m_lift … m ; m_lift … (f x)
    156206}.
    157 
    158 
    159 

  • src/utilities/option.ma

    r1635 r1640  
    11include "utilities/monad.ma".
    22include "basics/types.ma".
     3
    34definition Option ≝ MakeMonad (mk_MonadDefinition
    45  (* the monad *)
    … …  
    910  (λX,Y,m,f. match m with [ Some x ⇒ f x | None ⇒ None ?])
    1011  ???).
    11 //
    12 [(* bind_bind *)
    13  #X#Y#Z*normalize //
    14 |(* bind_ret *)
    15  #X*normalize //
    16 ]
    17 qed.
     12// #X[#Y#Z]*normalize//qed.
    1813
    1914include "hints_declaration.ma".
    2015unification hint 0 ≔ X;
    21 M ≟ Option
     16M ≟ m_def Option
    2217(*---------------*) ⊢
    23 option X ≡ monad (m_def M) X
     18option X ≡ monad M X
    2419.
     20
     21definition opt_safe : ∀X.∀m : option X. m ≠ None X → X ≝
     22λX,m,prf.match m return λx.m = x → X with
     23  [ Some t ⇒ λ_.t
     24  | None ⇒ λeq_m.?
     25  ] (refl …). elim (absurd … eq_m prf) qed.
     26
     27(* playground for notation problems *)
     28
     29inductive option_bis (X : Type[0]) : Type[0] ≝
     30| Some' : X → option_bis X
     31| None' : option_bis X.
     32
     33definition option_to_option' ≝ λX.λm : option X. match m with [ Some x ⇒ Some' ? x | None ⇒ None' ?].
     34
     35coercion o_to_o' : ∀X.∀m : option X. option_bis X ≝ option_to_option'
     36  on _m : option ? to option_bis ?.
     37 
     38
     39definition 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
     46unification hint 0 ≔ X ;
     47M ≟ m_def Option_bis
     48(*---------------*) ⊢
     49option_bis X ≡ monad M X
     50.
     51
     52(* does not typecheck
     53check (λX.λm : option_bis X.λn : option X.! x ← n ; m)
     54*)

  • src/utilities/proper.ma

    r1635 r1640  
    1919  @{'proper_contra $r $s}.
    2020
    21 interpretation "is proper" 'is_proper f p = (p f f).
    22 notation "f ⊨ p" with precedence 50 for @{'is_proper $f $p}.
     21(* avoid notation from kikcing in in outputm to avoid things like X ⊨ Prod *)
     22notation > "f ⊨ p " with precedence 50 for @{$p $f $f}.
Note: See TracChangeset for help on using the changeset viewer.