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

Legend:

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