Changeset 487 for Deliverables/D3.1/Csemantics/Maps.ma
 Timestamp:
 Feb 9, 2011, 11:49:17 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/Maps.ma
r11 r487 42 42 (* * * The abstract signatures of trees *) 43 43 44 nrecord TREE (elt:Type) : Type[1] ≝ {44 record TREE (elt:Type[0]) : Type[1] ≝ { 45 45 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) → 48 48 ∀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; 53 53 (* 54 54 (** The ``good variables'' properties for trees, expressing … … 96 96 (** Applying a function to all data of a tree. *) 97 97 *) 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; 99 99 (* 100 100 Hypothesis gmap: … … 118 118 (** Enumerating the bindings of a tree. *) 119 119 *) 120 elements: ∀A: Type . tree_t A → list (elt × A);120 elements: ∀A: Type[0]. tree_t A → list (elt × A); 121 121 (* 122 122 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), 124 124 get i m = Some v > In (i, v) (elements m). 125 125 Hypothesis elements_complete: … … 132 132 (** Folding a function over all bindings of a tree. *) 133 133 *) 134 tree_fold: ∀A,B: Type . (B → elt → A → B) → tree_t A → B → B134 tree_fold: ∀A,B: Type[0]. (B → elt → A → B) → tree_t A → B → B 135 135 (* 136 136 Hypothesis fold_spec: … … 143 143 (** * The abstract signatures of maps *) 144 144 145 nrecord MAP : Type[1] ≝ {146 elt: Type ;145 record MAP : Type[1] ≝ { 146 elt: Type[0]; 147 147 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 A148 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 152 152 }. 153 153 Hypothesis gi: … … 173 173 174 174 (* XXX: need real tree impl *) 175 nlet rec assoc_get (A:Type) (i:ident) (l:list (ident × A)) on l ≝175 let rec assoc_get (A:Type[0]) (i:ident) (l:list (ident × A)) on l ≝ 176 176 match l with 177 177 [ nil ⇒ None ? 178 178  cons h t ⇒ 179 match h with [ mk_pair hi ha ⇒179 match h with [ pair hi ha ⇒ 180 180 match ident_eq i hi with [ inl _ ⇒ Some ? ha  inr _ ⇒ assoc_get A i t ] ] 181 181 ]. 182 182 183 naxiom assoc_tree_eq: ∀A: Type. ∀x,y: A. (x=y) + (x≠y) →183 axiom assoc_tree_eq: ∀A: Type[0]. ∀x,y: A. (x=y) + (x≠y) → 184 184 ∀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 ≝185 axiom assoc_remove: ∀A: Type[0]. ident → list (ident × A) → list (ident × A). 186 axiom assoc_tree_map: ∀A,B: Type[0]. (ident → A → B) → list (ident × A) → list (ident × B). 187 definition assoc_elements: ∀A: Type[0]. list (ident × A) → list (ident × A) ≝ λA,x.x. 188 axiom assoc_tree_fold: ∀A,B: Type[0]. (B → ident → A → B) → list (ident × A) → B → B. 189 190 definition PTree : TREE ident ≝ 191 191 mk_TREE ? 192 192 ident_eq
Note: See TracChangeset
for help on using the changeset viewer.