- Timestamp:
- Jan 11, 2012, 5:41:45 PM (9 years ago)
- Location:
- src
- Files:
-
- 1 added
- 10 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTL/RTL_paolo.ma
r1636 r1640 25 25 | rtl_st_ext_tailcall_ptr: register → register → list rtl_argument → rtl_statement_extension. 26 26 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 27 definition rtl_params ≝ mk_graph_params (mk_unserialized_params 34 28 (mk_inst_params 35 29 (* acc_a_reg ≝ *) register … … 42 36 (* dph_arg ≝ *) rtl_argument 43 37 (* snd_arg ≝ *) rtl_argument 44 (* operator1 ≝ *) Op1 45 (* operator2 ≝ *) Op2 46 (* pair_move ≝ *) rtl_move 38 (* pair_move ≝ *) (register × rtl_argument) 47 39 (* call_args ≝ *) (list rtl_argument) 48 40 (* call_dest ≝ *) (list register) … … 53 45 (* resultT ≝ *) (list register) 54 46 (* paramsT ≝ *) (list register)) 55 (* localsT ≝ *) (list register)). 47 (* localsT ≝ *) (list register))). 48 49 interpretation "move" 'mov r a = (MOVE ? ? (mk_Prod ?? r a)). 56 50 57 51 (* aid unification *) … … 59 53 unification hint 0 ≔ 60 54 (*---------------*) ⊢ 61 acc_a_reg ( g_inst_pars rtl_params) ≡ register.55 acc_a_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register. 62 56 unification hint 0 ≔ 63 57 (*---------------*) ⊢ 64 acc_b_reg ( g_inst_pars rtl_params) ≡ register.58 acc_b_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register. 65 59 unification hint 0 ≔ 66 60 (*---------------*) ⊢ 67 acc_a_arg ( g_inst_pars rtl_params) ≡ rtl_argument.61 acc_a_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument. 68 62 unification hint 0 ≔ 69 63 (*---------------*) ⊢ 70 acc_b_arg ( g_inst_pars rtl_params) ≡ rtl_argument.64 acc_b_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument. 71 65 unification hint 0 ≔ 72 66 (*---------------*) ⊢ 73 dpl_reg ( g_inst_pars rtl_params) ≡ register.67 dpl_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register. 74 68 unification hint 0 ≔ 75 69 (*---------------*) ⊢ 76 dph_reg ( g_inst_pars rtl_params) ≡ register.70 dph_reg (u_inst_pars (g_u_pars rtl_params)) ≡ register. 77 71 unification hint 0 ≔ 78 72 (*---------------*) ⊢ 79 dpl_arg ( g_inst_pars rtl_params) ≡ rtl_argument.73 dpl_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument. 80 74 unification hint 0 ≔ 81 75 (*---------------*) ⊢ 82 dph_arg ( g_inst_pars rtl_params) ≡ rtl_argument.76 dph_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument. 83 77 unification hint 0 ≔ 84 78 (*---------------*) ⊢ 85 snd_arg ( g_inst_pars rtl_params) ≡ rtl_argument.79 snd_arg (u_inst_pars (g_u_pars rtl_params)) ≡ rtl_argument. 86 80 unification hint 0 ≔ 87 81 (*---------------*) ⊢ 88 operator1 (g_inst_pars rtl_params) ≡ Op1.82 pair_move (u_inst_pars (g_u_pars rtl_params)) ≡ register × rtl_argument. 89 83 unification hint 0 ≔ 90 84 (*---------------*) ⊢ 91 operator2 (g_inst_pars rtl_params) ≡ Op2.85 call_args (u_inst_pars (g_u_pars rtl_params)) ≡ list rtl_argument. 92 86 unification hint 0 ≔ 93 87 (*---------------*) ⊢ 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. 88 call_dest (u_inst_pars (g_u_pars rtl_params)) ≡ list register. 101 89 102 check (λglobals,r.OP2 rtl_params globals Or r r r)103 90 104 91 definition 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 *) 93 definition rtl_statement ≝ joint_statement (rtl_params : params). 126 94 127 95 definition rtl_internal_function ≝ … … 136 104 | rtlntc_st_ext_call_ptr: register → register → list register → list register → rtlntc_statement_extension. 137 105 138 definition rtlntc_params : graph_params ≝ mk_graph_params106 definition rtlntc_params ≝ mk_graph_params (mk_unserialized_params 139 107 (mk_inst_params 140 108 (* acc_a_reg ≝ *) register … … 147 115 (* dph_arg ≝ *) rtl_argument 148 116 (* snd_arg ≝ *) rtl_argument 149 (* operator1 ≝ *) Op1 150 (* operator2 ≝ *) Op2 151 (* pair_move ≝ *) rtl_move 117 (* pair_move ≝ *) (register × rtl_argument) 152 118 (* call_args ≝ *) (list rtl_argument) 153 119 (* call_dest ≝ *) (list register) … … 158 124 (* resultT ≝ *) (list register) 159 125 (* paramsT ≝ *) (list register)) 160 (* localsT ≝ *) (list register)) .126 (* localsT ≝ *) (list register))). 161 127 162 definition rtlntc_statement ≝ joint_statement rtlntc_params.128 definition rtlntc_statement ≝ joint_statement (rtlntc_params : params). 163 129 164 130 definition rtlntc_internal_function ≝ -
src/RTLabs/RTLabsToRTL_paolo.ma
r1636 r1640 8 8 include alias "ASM/BitVector.ma". 9 9 include alias "arithmetics/nat.ma". 10 11 12 (* Paolo: to be moved elsewhere *)13 14 notation "r ← a1 .op. a2" with precedence 50 for15 @{'op2 $op $r $a1 $a2}.16 notation "r ← . op . a" with precedence 50 for17 @{'op1 $op $r $a}.18 notation "r ← a" with precedence 50 for19 @{'mov $r $a}.20 notation "❮r, s❯ ← a1 . op . a2" with precedence 50 for21 @{'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).27 10 28 11 … … 141 124 eqb m n = true → m = n. 142 125 #m#n@eqb_elim // #_ #F destruct(F) qed. 143 126 144 127 definition translate_op: 145 128 ∀globals. Op2 → … … 161 144 (* first, clear carry if op relies on it *) 162 145 match op with 163 [ Addc ⇒ [ clear_carry?]164 | Sub ⇒ [ clear_carry?]146 [ Addc ⇒ [CLEAR_CARRY ??] 147 | Sub ⇒ [CLEAR_CARRY ??] 165 148 | _ ⇒ [ ] 166 149 ] @ … … 228 211 match split_into_bytes size const with 229 212 [ 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 ? 231 214 ] 232 215 | Ofloatconst float ⇒ λ_.⊥ … … 374 357 | cons srcr srcrs' ⇒ 375 358 let f : register → rtl_instruction globals ≝ 376 λr. OP2 ?? Or destr (Reg destr) (Reg r)in377 reg_from_reg … srcr destr::359 λr. destr ← destr .Or. r in 360 MOVE rtl_params globals 〈destr,srcr〉 :: 378 361 map … f srcrs' @ 379 362 (* now destr is non-null iff srcrs was non-null *) 380 clear_carry …::363 CLEAR_CARRY ? ? :: 381 364 (* many uses of 0, better not use immediates *) 382 365 ν tmp in … … 420 403 ] 421 404 qed. 405 406 include alias "arithmetics/nat.ma". 422 407 423 408 let rec range_strong_internal (start : ℕ) (count : ℕ) … … 615 600 acc in 616 601 let epilogue : list (rtl_instruction globals) ≝ 617 [ clear_carry… ;602 [ CLEAR_CARRY … ; 618 603 tmpr ← 0 .Sub. destr ; 619 604 (* now carry bit is 1 iff destrs != 0 *) … … 782 767 | cons srcr srcrs' ⇒ 783 768 ν 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〉 :: 786 772 map … f srcrs' @ 787 [ COND …tmpr lbl_true ]773 [ COND ?? tmpr lbl_true ] 788 774 ]. 789 775 … … 926 912 let 〈lenv,runiverse〉 ≝ initialize_local_env runiverse 927 913 (f_params def @ f_locals def) (f_result def) in 928 let param s ≝ map_list_local_env lenv (map … \fst (f_params def)) in914 let parameters ≝ map_list_local_env lenv (map … \fst (f_params def)) in 929 915 let locals ≝ map_list_local_env lenv (map … \fst (f_locals def)) in 930 916 let result ≝ … … 939 925 let runiverse' ≝ runiverse in 940 926 let result' ≝ result in 941 let params' ≝ param s in927 let params' ≝ parameters in 942 928 let locals' ≝ locals in 943 929 let stack_size' ≝ f_stacksize def in 944 930 let entry' ≝ f_entry def in 945 931 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 948 936 let res ≝ 949 937 mk_joint_internal_function globals rtl_params luniverse' runiverse' result' params' -
src/common/AST.ma
r1516 r1640 196 196 197 197 lemma typesize_pos: ∀ty. typesize ty > 0. 198 *; try *; try * /2 / qed.198 *; try *; try * /2 by le_n/ qed. 199 199 200 200 lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2). … … 343 343 definition map_partial : ∀A,B,C:Type[0]. (B → res C) → 344 344 list (A × B) → res (list (A × C)) ≝ 345 λA,B,C,f. m map?? (λ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〉). 346 346 347 347 lemma map_partial_preserves_first: -
src/common/Errors.ma
r1626 r1640 19 19 include "common/PreIdentifiers.ma". 20 20 include "basics/russell.ma". 21 include "utilities/monad.ma". 21 22 22 23 (* * Error reporting and the error monad. *) … … 48 49 (*Implicit Arguments Error [A].*) 49 50 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. *) 51 definition 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 ] 65 qed. 66 67 include "hints_declaration.ma". 68 unification hint 0 ≔ X; 69 M ≟ m_def Res 70 (*---------------*) ⊢ 71 res X ≡ monad M X 72 . 73 74 (*(* Dependent pair version. *) 91 75 notation > "vbox('do' « ident v , ident p » ← e; break e')" with precedence 40 92 76 for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ mk_Sig ${ident v} ${ident p} ⇒ ${e'} ]) }. … … 110 94 111 95 notation > "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: 96 interpretation "error monad sig Prod bind" 'sigbind2 e f = (sigbind2 ???? e f).*) 97 98 lemma res_bind_inversion: 126 99 ∀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) 132 105 ] qed. 133 106 134 107 lemma bind2_inversion: 135 108 ∀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:(??%?); destruct109 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) 141 114 ] qed. 142 115 143 116 (* 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. 117 Open Local Scope error_monad_scope.*) 169 118 170 119 (* … … 189 138 [ nil ⇒ x 190 139 | cons hd tl ⇒ 191 dox ← x ;140 ! x ← x ; 192 141 mfold_left_i_aux A B f (f i x hd) (S i) tl 193 142 ]. … … 213 162 [ nil ⇒ Error ? (msg WrongLength) 214 163 | cons hd' tl' ⇒ 215 doaccu ← accu;164 ! accu ← accu; 216 165 mfold_left2 … f (f accu hd hd') tl tl' 217 166 ] … … 301 250 ] (refl ? f). 302 251 303 notation > "vbox(' do' ident v 'as' ident E ← e; break e')" with precedence 40 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}.252 notation > "vbox('!' ident v 'as' ident E ← e; break e')" with precedence 40 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}. 304 253 305 254 definition bind2_eq ≝ λA,B,C:Type[0]. λf: res (A×B). λg: ∀a:A.∀b:B. f = OK ? 〈a,b〉 → res C. … … 309 258 ] (refl ? f). 310 259 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'})}.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'})}. 312 261 313 262 definition res_to_opt : ∀A:Type[0]. res A → option A ≝ -
src/common/IOMonad.ma
r1601 r1640 8 8 | Value : T → IO output input T 9 9 | Wrong : errmsg → IO output input T. 10 11 include "utilities/proper.ma". 12 (* a weak form of extensionality *) 13 axiom 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. 10 15 11 16 let 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' ≝ … … 16 21 ]. 17 22 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 ]. 23 include "utilities/monad.ma". 24 25 definition 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 ] 41 qed. 42 43 definition bindIO2 ≝ λO,I. m_bind2 (IOMonad O I). 44 45 include "hints_declaration.ma". 46 47 unification 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 24 53 25 54 definition err_to_io : ∀O,I,T. res T → IO O I T ≝ 26 55 λO,I,T,v. match v with [ OK v' ⇒ Value O I T v' | Error m ⇒ Wrong O I T m ]. 56 27 57 coercion err_to_io : ∀O,I,A.∀c:res A.IO O I A ≝ err_to_io on _c:res ? to IO ???. 58 28 59 definition err_to_io_sig : ∀O,I,T.∀P:T → Prop. res (Sig T P) → IO O I (Sig T P) ≝ 29 60 λ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 ]. 30 61 (*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 ??).*) 31 62 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 (**)45 63 let rec P_io O I (A:Type[0]) (P:A → Prop) (v:IO O I A) on v : Prop ≝ 46 64 match v return λ_.Prop with … … 176 194 177 195 (* Is there a way to prove this without extensionality? *) 178 196 (* 179 197 lemma bind_assoc_r: ∀O,I,A,B,C,e,f,g. 180 198 ∀ext:(∀T1,T2:Type[0].∀f,f':T1 → T2.(∀x.f x = f' x) → f = f'). … … 186 204 | #m @refl 187 205 ] qed. 206 *) 207 definition bind_assoc_r ≝ λO,I.m_bind_bind (IOMonad O I). 188 208 189 209 (* -
src/joint/Joint_paolo.ma
r1635 r1640 6 6 7 7 (* 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 | __/ | 16 25 inst_params funct_params 17 26 … … 34 43 ; dph_arg: Type[0] (* high address registers *) 35 44 ; 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 *)38 45 ; pair_move: Type[0] (* argument of move instructions *) 39 46 ; call_args: Type[0] (* arguments of function calls *) … … 51 58 | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals 52 59 | 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 globals54 | OP2: operator2 p→ acc_a_reg p → acc_a_arg p → snd_arg p → joint_instruction p globals55 (* int , clear and set carry can bedone 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 *) 57 64 | CLEAR_CARRY: joint_instruction p globals 58 | SET_CARRY: joint_instruction p globals *)65 | SET_CARRY: joint_instruction p globals 59 66 | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_instruction p globals 60 67 | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_instruction p globals … … 62 69 | COND: acc_a_reg p → label → joint_instruction p globals 63 70 | extension: extend_statements p → joint_instruction p globals. 71 72 (* Paolo: to be moved elsewhere *) 73 74 notation "r ← a1 .op. a2" with precedence 50 for 75 @{'op2 $op $r $a1 $a2}. 76 notation "r ← . op . a" with precedence 50 for 77 @{'op1 $op $r $a}. 78 notation "r ← a" with precedence 50 for 79 @{'mov $r $a}. (* to be set in individual languages *) 80 notation "❮r, s❯ ← a1 . op . a2" with precedence 50 for 81 @{'opaccs $op $r $s $a1 $a2}. 82 83 interpretation "op2" 'op2 op r a1 a2 = (OP2 ? ? op r a1 a2). 84 interpretation "op1" 'op1 op r a = (OP1 ? ? op r a). 85 interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2). 86 87 64 88 65 89 definition inst_forall_labels : ∀p : inst_params.∀globals. … … 70 94 | _ ⇒ True 71 95 ]. 72 73 record stmt_params : Type[1] ≝74 { inst_pars :> inst_params75 ; 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 globals81 | GOTO: label → joint_statement p globals82 | RETURN: joint_statement p globals.83 84 (* for all labels in statement. Uses succ_choice to consider the successor of85 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 #next90 [@(inst_forall_labels … P instr ∧ P next)91 |@(inst_forall_labels … P instr)92 ]93 |@P94 |@True95 ]qed.96 96 97 97 record funct_params : Type[1] ≝ … … 105 105 }. 106 106 107 record unserialized_params : Type[1] ≝ 108 { u_inst_pars :> inst_params 109 ; u_local_pars :> local_params 110 }. 111 112 record stmt_params : Type[1] ≝ 113 { unserialized_pars :> unserialized_params 114 ; succ : Type[0] 115 ; succ_forall_labels : (label → Prop) → succ → Prop 116 }. 117 118 inductive 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 107 123 record params : Type[1] ≝ 108 124 { stmt_pars :> stmt_params 109 ; local_pars :> local_params110 125 ; codeT: list ident → Type[0] 111 126 ; lookup: ∀globals.codeT globals → label → option (joint_statement stmt_pars globals) 112 127 }. 113 128 129 130 (* for all labels in statement. Uses succ_choice to consider the successor of 131 a statement when such successors are labels *) 132 definition 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 140 record lin_params : Type[1] ≝ 141 { l_u_pars :> unserialized_params }. 142 143 include "utilities/option.ma". 144 145 definition 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 154 coercion lp_to_p : ∀lp : lin_params.params ≝ lin_params_to_params 155 on _lp : lin_params to params. 156 114 157 record graph_params : Type[1] ≝ 115 { g_inst_pars :> inst_params 116 ; g_local_pars :> local_params 117 }. 158 { g_u_pars :> unserialized_params }. 159 160 include 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) *) 164 definition 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 170 coercion gp_to_p : ∀gp:graph_params.params ≝ λgp.graph_params_to_params gp 171 on _gp : graph_params to params. 172 118 173 119 174 definition labels_present : ∀p : params.∀globals. … … 130 185 forall_stmts … (labels_present … code) code. 131 186 132 include alias "common/Graphs.ma". (* To pick the right lookup *)133 134 135 (* One common instantiation of params via Graphs of joint_statements136 (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 …)) in140 mk_params141 stmt_pars142 gp143 (* 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 gp149 on _gp : graph_params to params.150 151 187 (* 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))).188 definition rtl_ertl_params : ?→?→params ≝ λinst_pars,funct_pars. 189 (mk_graph_params (mk_unserialized_params inst_pars (mk_local_params funct_pars (list register)))). 154 190 155 191 record joint_internal_function (globals: list ident) (p:params) : Type[0] ≝ -
src/joint/TranslateUtils_paolo.ma
r1635 r1640 104 104 joint_internal_function globals dst_g_pars ≝ 105 105 λsrc_g_pars,dst_g_pars,globals,registerT,fresh_reg,trans,empty,def. 106 let f : label → joint_statement src_g_parsglobals →106 let f : label → joint_statement (src_g_pars : params) globals → 107 107 joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝ 108 108 λlbl,stmt,def. … … 128 128 joint_internal_function … dst_g_pars ≝ 129 129 λsrc_g_pars,dst_g_pars,globals,trans,empty,def. 130 let f : label → joint_statement src_g_parsglobals →130 let f : label → joint_statement (src_g_pars : params) globals → 131 131 joint_internal_function … dst_g_pars → joint_internal_function … dst_g_pars ≝ 132 132 λlbl,stmt,def. -
src/utilities/monad.ma
r1635 r1640 3 3 include "utilities/setoids.ma". 4 4 include "utilities/proper.ma". 5 5 6 6 record MonadDefinition : Type[1] ≝ { 7 7 monad : Type[0] → Type[0] ; … … 37 37 with precedence 48 for @{'m_bind ${e} (λ_. ${e'})}. 38 38 notation > "! 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}}. 40 40 notation > "! ident v : ty ← e; e'" 41 41 with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}. 42 42 notation < "vbox(! \nbsp ident v ← e ; break e')" 43 43 with precedence 48 for @{'m_bind ${e} (λ${ident v}.${e'})}. 44 notation > "! ident v ← e : ty ; e'" 45 with precedence 48 for @{'m_bind (${e} : ${ty}) (λ${ident v}.${e'})}. 44 46 notation < "vbox(! \nbsp ident v : ty ← e ; break e')" 45 47 with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}. 48 notation > "! ident v : ty ← e : ty' ; e'" 49 with precedence 48 for @{'m_bind (${e} : ${ty'}) (λ${ident v} : ${ty}. ${e'})}. 46 50 notation > "! 〈ident v1, ident v2〉 ← e ; e'" 47 51 with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}. … … 52 56 notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e ; break e')" 53 57 with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}. 58 notation > "! 〈ident v1, ident v2, ident v3〉 ← e ; e'" 59 with precedence 48 for @{'m_bind3 ${e} (λ${ident v1}. λ${ident v2}. λ${ident v3}. ${e'})}. 60 notation > "! 〈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'})}. 62 notation < "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'})}. 64 notation < "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 *) 69 notation > "'do' ident v ← e; e'" 70 with precedence 48 for @{'m_bind ${e} (λ${ident v}. ${e'})}. 71 notation > "'do' ident v : ty ← e; e'" 72 with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}. 73 notation > "'do' 〈ident v1, ident v2〉 ← e ; e'" 74 with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}. 75 notation > "'do' 〈ident v1 : ty1, ident v2 : ty2〉 ← e ; e'" 76 with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}. 77 notation > "'do' 〈ident v1, ident v2, ident v3〉 ← e ; e'" 78 with precedence 48 for @{'m_bind3 ${e} (λ${ident v1}. λ${ident v2}. λ${ident v3}. ${e'})}. 79 notation > "'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'})}. 54 81 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 *) 83 notation > "! «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 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 99 notation > "'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 105 notation > "'return' t" with precedence 46 for @{'m_return $t}. 106 notation < "'return' \nbsp t" with precedence 46 for @{'m_return $t}. 86 107 87 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). 88 110 interpretation "setoid monad return" 'm_return x = (sm_return ? ? x). 89 111 interpretation "monad bind" 'm_bind m f = (m_bind ? ? ? m f). 112 interpretation "monad bind'" 'm_bind' f m = (m_bind ? ? ? m f). 90 113 interpretation "monad return" 'm_return x = (m_return ? ? x). 114 115 include "basics/lists/list.ma". 91 116 92 117 (* add structure and properties as needed *) … … 97 122 monad m_def X → monad m_def Y → monad m_def Z; 98 123 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 130 interpretation "monad bind2" 'm_bind2 m f = (m_bind2 ? ? ? ? m f). 131 interpretation "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. 101 143 102 144 definition MakeMonad : MonadDefinition → Monad ≝ λM. … … 116 158 let 〈x, y〉 ≝ p in 117 159 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) 118 164 (* 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 120 171 (* add structure and properties as needed *) 121 172 record SetoidMonad : Type[1] ≝ { … … 145 196 f x y). 146 197 147 interpretation "monad bind2" 'm_bind2 m f = (sm_map2 ? ? ? ? m f). 148 198 interpretation "setoid monad bind2" 'm_bind2 m f = (sm_bind2 ? ? ? ? m f). 149 199 150 200 record MonadTransformer : Type[1] ≝ { … … 155 205 m_lift … (! x ← m ; f x) = ! x ← m_lift … m ; m_lift … (f x) 156 206 }. 157 158 159 -
src/utilities/option.ma
r1635 r1640 1 1 include "utilities/monad.ma". 2 2 include "basics/types.ma". 3 3 4 definition Option ≝ MakeMonad (mk_MonadDefinition 4 5 (* the monad *) … … 9 10 (λX,Y,m,f. match m with [ Some x ⇒ f x | None ⇒ None ?]) 10 11 ???). 11 // 12 [(* bind_bind *) 13 #X#Y#Z*normalize // 14 |(* bind_ret *) 15 #X*normalize // 16 ] 17 qed. 12 // #X[#Y#Z]*normalize//qed. 18 13 19 14 include "hints_declaration.ma". 20 15 unification hint 0 ≔ X; 21 M ≟ Option16 M ≟ m_def Option 22 17 (*---------------*) ⊢ 23 option X ≡ monad (m_def M)X18 option X ≡ monad M X 24 19 . 20 21 definition 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 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/proper.ma
r1635 r1640 19 19 @{'proper_contra $r $s}. 20 20 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 *) 22 notation > "f ⊨ p " with precedence 50 for @{$p $f $f}.
Note: See TracChangeset
for help on using the changeset viewer.