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/Maps.ma

    r11 r487  
    4242(* * * The abstract signatures of trees *)
    4343
    44 nrecord TREE (elt:Type) : Type[1] ≝ {
     44record TREE (elt:Type[0]) : Type[1] ≝ {
    4545  elt_eq: ∀a,b: elt. (a = b) + (a ≠ b);
    46   tree_t: Type → Type;
    47   tree_eq: ∀A: Type. ∀x,y: A. (x=y) + (x≠y) →
     46  tree_t: Type[0] → Type[0];
     47  tree_eq: ∀A: Type[0]. ∀x,y: A. (x=y) + (x≠y) →
    4848      ∀a,b: tree_t A. (a = b) + (a ≠ b);
    49   empty: ∀A: Type. tree_t A;
    50   get: ∀A: Type. elt → tree_t A → option A;
    51   set: ∀A: Type. elt → A → tree_t A → tree_t A;
    52   remove: ∀A: Type. elt → tree_t A → tree_t A;
     49  empty: ∀A: Type[0]. tree_t A;
     50  get: ∀A: Type[0]. elt → tree_t A → option A;
     51  set: ∀A: Type[0]. elt → A → tree_t A → tree_t A;
     52  remove: ∀A: Type[0]. elt → tree_t A → tree_t A;
    5353(*
    5454  (** The ``good variables'' properties for trees, expressing
     
    9696  (** Applying a function to all data of a tree. *)
    9797*)
    98   tree_map: ∀A,B: Type. (elt → A → B) → tree_t A → tree_t B;
     98  tree_map: ∀A,B: Type[0]. (elt → A → B) → tree_t A → tree_t B;
    9999(*
    100100  Hypothesis gmap:
     
    118118  (** Enumerating the bindings of a tree. *)
    119119*)
    120   elements: ∀A: Type. tree_t A → list (elt × A);
     120  elements: ∀A: Type[0]. tree_t A → list (elt × A);
    121121(*
    122122  Hypothesis elements_correct:
    123     forall (A: Type) (m: t A) (i: elt) (v: A),
     123    forall (A: Type[0]) (m: t A) (i: elt) (v: A),
    124124    get i m = Some v -> In (i, v) (elements m).
    125125  Hypothesis elements_complete:
     
    132132  (** Folding a function over all bindings of a tree. *)
    133133*)
    134   tree_fold: ∀A,B: Type. (B → elt → A → B) → tree_t A → B → B
     134  tree_fold: ∀A,B: Type[0]. (B → elt → A → B) → tree_t A → B → B
    135135(*
    136136  Hypothesis fold_spec:
     
    143143(** * The abstract signatures of maps *)
    144144
    145 nrecord MAP : Type[1] ≝ {
    146   elt: Type;
     145record MAP : Type[1] ≝ {
     146  elt: Type[0];
    147147  elt_eq: ∀a,b: elt. (a = b) + (a ≠ b);
    148   t: Type → Type;
    149   init: ∀A: Type. A → t A;
    150   get: ∀A: Type. elt → t A → A;
    151   set: ∀A: Type. elt → A → t A → t A
     148  t: Type[0] → Type[0];
     149  init: ∀A: Type[0]. A → t A;
     150  get: ∀A: Type[0]. elt → t A → A;
     151  set: ∀A: Type[0]. elt → A → t A → t A
    152152}.
    153153  Hypothesis gi:
     
    173173
    174174(* XXX: need real tree impl *)
    175 nlet rec assoc_get (A:Type) (i:ident) (l:list (ident × A)) on l ≝
     175let rec assoc_get (A:Type[0]) (i:ident) (l:list (ident × A)) on l ≝
    176176match l with
    177177[ nil ⇒ None ?
    178178| cons h t ⇒
    179   match h with [ mk_pair hi ha ⇒
     179  match h with [ pair hi ha ⇒
    180180    match ident_eq i hi with [ inl _ ⇒ Some ? ha | inr _ ⇒ assoc_get A i t ] ]
    181181].
    182182
    183 naxiom assoc_tree_eq: ∀A: Type. ∀x,y: A. (x=y) + (x≠y) →
     183axiom assoc_tree_eq: ∀A: Type[0]. ∀x,y: A. (x=y) + (x≠y) →
    184184      ∀a,b: list (ident × A). (a = b) + (a ≠ b).
    185 naxiom assoc_remove: ∀A: Type. ident → list (ident × A) → list (ident × A).
    186 naxiom assoc_tree_map: ∀A,B: Type. (ident → A → B) → list (ident × A) → list (ident × B).
    187 ndefinition assoc_elements: ∀A: Type. list (ident × A) → list (ident × A) ≝ λA,x.x.
    188 naxiom assoc_tree_fold: ∀A,B: Type. (B → ident → A → B) → list (ident × A) → B → B.
    189 
    190 ndefinition PTree : TREE ident ≝
     185axiom assoc_remove: ∀A: Type[0]. ident → list (ident × A) → list (ident × A).
     186axiom assoc_tree_map: ∀A,B: Type[0]. (ident → A → B) → list (ident × A) → list (ident × B).
     187definition assoc_elements: ∀A: Type[0]. list (ident × A) → list (ident × A) ≝ λA,x.x.
     188axiom assoc_tree_fold: ∀A,B: Type[0]. (B → ident → A → B) → list (ident × A) → B → B.
     189
     190definition PTree : TREE ident ≝
    191191mk_TREE ?
    192192  ident_eq
Note: See TracChangeset for help on using the changeset viewer.