Changeset 10 for C-semantics/Maps.ma


Ignore:
Timestamp:
Jul 6, 2010, 11:53:23 AM (10 years ago)
Author:
campbell
Message:

Add binary arithmetic libraries, use for integers and identifiers (but
we're not doing modular arithmetic yet.)
Add a dummy "tree" implementation to make environment lookups executable.
Fix if .. then .. else .. precedence.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Maps.ma

    r3 r10  
    172172*)
    173173
    174 naxiom PTree : TREE ident.
     174(* XXX: need real tree impl *)
     175nlet rec assoc_get (A:Type) (i:ident) (l:list (ident × A)) on l ≝
     176match l with
     177[ nil ⇒ None ?
     178| cons h t ⇒
     179  match h with [ mk_pair hi ha ⇒
     180    match ident_eq i hi with [ inl _ ⇒ Some ? ha | inr _ ⇒ assoc_get A i t ] ]
     181].
     182
     183naxiom assoc_tree_eq: ∀A: Type. ∀x,y: A. (x=y) + (x≠y) →
     184      ∀a,b: list (ident × A). (a = b) + (a ≠ b).
     185naxiom assoc_remove: ∀A: Type. ident → list (ident × A) → list (ident × A).
     186naxiom assoc_tree_map: ∀A,B: Type. (ident → A → B) → list (ident × A) → list (ident × B).
     187naxiom assoc_elements: ∀A: Type. list (ident × A) → list (ident × A).
     188naxiom assoc_tree_fold: ∀A,B: Type. (B → ident → A → B) → list (ident × A) → B → B.
     189
     190ndefinition PTree : TREE ident ≝
     191mk_TREE ?
     192  ident_eq
     193  (λA. list (ident × A))
     194  assoc_tree_eq
     195  (λA. nil ?)
     196  assoc_get
     197  (λA,i,a,l.〈i,a〉::l)
     198  assoc_remove
     199  assoc_tree_map
     200  assoc_elements
     201  assoc_tree_fold.
    175202
    176203(*
Note: See TracChangeset for help on using the changeset viewer.