Ignore:
Timestamp:
Feb 9, 2011, 11:49:17 AM (9 years ago)
Author:
campbell
Message:

Port Clight semantics to the new-new matita syntax.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Errors.ma

    r485 r487  
    1414(* *********************************************************************)
    1515
    16 include "datatypes/pairs.ma".
    17 include "Plogic/equality.ma".
    18 include "Plogic/connectives.ma".
    19 include "datatypes/sums.ma".
     16include "basics/types.ma".
     17include "basics/logic.ma".
    2018
    2119(* * Error reporting and the error monad. *)
     
    4139  or [Error msg] to indicate failure. *)
    4240
    43 ninductive res (A: Type) : Type
     41inductive res (A: Type[0]) : Type[0]
    4442| OK: A → res A
    4543| Error: (* FIXME errmsg →*) res A.
     
    5048  with the following [bind] operation. *)
    5149
    52 ndefinition bind ≝ λA,B:Type. λf: res A. λg: A → res B.
     50definition bind ≝ λA,B:Type[0]. λf: res A. λg: A → res B.
    5351  match f with
    5452  [ OK x ⇒ g x
     
    5654  ].
    5755
    58 ndefinition bind2 ≝ λA,B,C: Type. λf: res (A × B). λg: A → B → res C.
     56definition bind2 ≝ λA,B,C: Type[0]. λf: res (A × B). λg: A → B → res C.
    5957  match f with
    60   [ OK v ⇒ match v with [ mk_pair x y ⇒ g x y ]
     58  [ OK v ⇒ match v with [ pair x y ⇒ g x y ]
    6159  | Error (*msg*) => Error ? (*msg*)
    6260  ].
     
    7270notation < "vbox('do' \nbsp 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
    7371notation < "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'})}.
    74 interpretation "error monad pair bind" 'bind2 e f = (bind2 ??? e f).
     72interpretation "error monad Prod bind" 'bind2 e f = (bind2 ??? e f).
    7573(*interpretation "error monad ret" 'ret e = (ret ? e).
    7674notation "'ret' e" non associative with precedence 45 for @{'ret ${e}}.*)
     
    8785 : error_monad_scope.
    8886*)
    89 nremark bind_inversion:
    90   ∀A,B: Type. ∀f: res A. ∀g: A → res B. ∀y: B.
     87lemma bind_inversion:
     88  ∀A,B: Type[0]. ∀f: res A. ∀g: A → res B. ∀y: B.
    9189  bind ?? f g = OK ? y →
    9290  ∃x. f = OK ? x ∧ g x = OK ? y.
    93 #A B f g y; ncases f;
    94 ##[ #a e; @a; nwhd in e:(??%?); /2/;
    95 ##| #H; nwhd in H:(??%?); ndestruct (H);
    96 ##] nqed.
    97 
    98 nremark bind2_inversion:
    99   ∀A,B,C: Type. ∀f: res (A×B). ∀g: A → B → res C. ∀z: C.
     91#A #B #f #g #y cases f;
     92[ #a #e %{a} whd in e:(??%?); /2/;
     93| #H whd in H:(??%?); destruct (H);
     94] qed.
     95
     96lemma bind2_inversion:
     97  ∀A,B,C: Type[0]. ∀f: res (A×B). ∀g: A → B → res C. ∀z: C.
    10098  bind2 ??? f g = OK ? z →
    10199  ∃x. ∃y. f = OK ? 〈x, y〉 ∧ g x y = OK ? z.
    102 #A B C f g z; ncases f;
    103 ##[ #ab; ncases ab; #a b e; @a; @b; nwhd in e:(??%?); /2/;
    104 ##| #H; nwhd in H:(??%?); ndestruct
    105 ##] nqed.
     100#A #B #C #f #g #z cases f;
     101[ #ab cases ab; #a #b #e %{a} %{b} whd in e:(??%?); /2/;
     102| #H whd in H:(??%?); destruct
     103] qed.
    106104
    107105(*
     
    195193
    196194
    197 ndefinition opt_to_res ≝ λA.λv:option A. match v with [ None ⇒ Error A | Some v ⇒ OK A v ].
    198 nlemma opt_OK: ∀A,P,e.
     195definition opt_to_res ≝ λA.λv:option A. match v with [ None ⇒ Error A | Some v ⇒ OK A v ].
     196lemma opt_OK: ∀A,P,e.
    199197  (∀v. e = Some ? v → P v) →
    200198  match opt_to_res A e with [ Error ⇒ True | OK v ⇒ P v ].
    201 #A P e; nelim e; /2/;
    202 nqed.
     199#A #P #e elim e; /2/;
     200qed.
Note: See TracChangeset for help on using the changeset viewer.