Ignore:
Timestamp:
Sep 20, 2012, 6:57:34 PM (8 years ago)
Author:
campbell
Message:

Deal with goto labels in RTLabs to Cminor by fixing up goto statements
after the main translation to avoid generating extra skips in awkward
locations.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/PositiveMap.ma

    r2307 r2335  
    567567] qed.
    568568
    569 
     569(* An "informative" dependently typed fold *)
     570
     571let rec pm_fold_inf_aux
     572 (A, B: Type[0])
     573 (t: positive_map A)
     574 (f: ∀p:Pos. ∀a:A. lookup_opt … p t = Some A a → B → B)
     575 (t': positive_map A)
     576 (pre: Pos → Pos)
     577 (b: B) on t': (∀p. lookup_opt … p t' = lookup_opt … (pre p) t) → B ≝
     578match t' return λt'. (∀p. lookup_opt A p t' = lookup_opt A (pre p) t) → B with
     579[ pm_leaf ⇒ λ_. b
     580| pm_node a l r ⇒ λH.
     581    let b ≝ match a return λa. lookup_opt A one (pm_node A a ??) = ? → B with [ None ⇒ λ_.b | Some a ⇒ λH. f (pre one) a ? b ] (H one) in
     582    let b ≝ pm_fold_inf_aux A B t f l (λx. pre (p0 x)) b ? in
     583            pm_fold_inf_aux A B t f r (λx. pre (p1 x)) b ?
     584].
     585[ #p @(H (p1 p)) | #p @(H (p0 p)) | <H % ]
     586qed.
     587
     588definition pm_fold_inf : ∀A, B: Type[0]. ∀t: positive_map A.
     589 ∀f: (∀p:Pos. ∀a:A. lookup_opt … p t = Some A a → B → B). B → B ≝
     590  λA,B,t,f,b. pm_fold_inf_aux A B t f t (λx.x) b (λp. refl ??).
     591
Note: See TracChangeset for help on using the changeset viewer.