syntax/parse: add progress-ordering to ~and

In (~and p1 p2), a failure in p2 now always dominates a failure in p1.
Consequently, if a pattern succeeds, its failures don't matter.

Add {pat,hpat,action}:ord wrappers, ord prframes. Apply ordering to
main pattern and side clauses. Add better progress analysis to
eliminate order wrapping.

pkgs/racket-test/tests/stxparse/select.rkt

@@ -11,9 +11,12 @@
 (define-syntax-rule (terx s p stuff ...)
   (terx* s [p] stuff ...))
 
-(define-syntax terx*
+(define-syntax-rule (terx* s [p ...] stuff ...)
+  (terx** s [[p] ...] stuff ...))
+
+(define-syntax terx**
   (syntax-parser
-    [(terx s [p ...] (~optional (~seq #:term term) #:defaults ([term #'#f])) rx ...)
+    [(terx s [[p c ...] ...] (~optional (~seq #:term term) #:defaults ([term #'#f])) rx ...)
      #`(test-case (format "line ~s: ~a match ~s for error"
                           '#,(syntax-line #'s)
                           's '(p ...))
@@ -22,7 +25,7 @@
                                    (escape exn))
                                  (lambda ()
                                    (syntax-parse (quote-syntax s)
-                                     [p (void)] ...))))])
+                                     [p c ... (void)] ...))))])
            (let ([msg (exn-message exn)]
                  [stxs (and (exn:fail:syntax? exn)
                             (exn:fail:syntax-exprs exn))])
@@ -171,6 +174,27 @@
       #rx"expected identifier"
       (not #rx"exact-nonnegative-integer"))
 
+;; sequential ~and
+
+(terx 1
+      (~and (~or x:nat x:id) (~fail "never happy"))
+      #rx"never happy"
+      (not #rx"expected identifier"))
+
+(terx** 1
+        ([(~post (~or x:nat x:id)) #:fail-when #t "never happy"])
+        #rx"never happy"
+        (not #rx"expected identifier"))
+
+;; indexes only compared within same ~and pattern
+(terx** 1
+        ([(~and (~fail "banana") _)]
+         [(~and x:nat (~fail "apple"))]
+         [(~and x:nat y:nat (~fail "orange"))])
+        #rx"apple"
+        #rx"orange"
+        #rx"banana")
+
 ;; ----------------------------------------
 ;; See "Simplification" from syntax/parse/private/runtime-report
 

racket/collects/syntax/parse/private/opt.rkt

@@ -213,6 +213,8 @@
      (pattern-factorable? pattern)]
     [(pat:commit pattern) #t]
     [(? pat:reflect?) #f]
+    [(pat:ord pattern _ _)
+     (pattern-factorable? pattern)]
     [(pat:post pattern)
      (pattern-factorable? pattern)]
     ;; ----
@@ -290,6 +292,10 @@
           [(and (pat:commit? a) (pat:commit? b))
            (pattern-equal? (pat:commit-pattern a) (pat:commit-pattern b))]
           [(and (pat:reflect? a) (pat:reflect? b)) #f] ;; FIXME: ?
+          [(and (pat:ord? a) (pat:ord? b))
+           (and (pattern-equal? (pat:ord-pattern a) (pat:ord-pattern b))
+                (equal? (pat:ord-group a) (pat:ord-group b))
+                (equal? (pat:ord-index a) (pat:ord-index b)))]
           [(and (pat:post? a) (pat:post? b))
            (pattern-equal? (pat:post-pattern a) (pat:post-pattern b))]
           ;; ---

racket/collects/syntax/parse/private/parse.rkt

@@ -645,6 +645,9 @@ Conventions:
                        (with ([cut-prompt cp0]
                               [fail-handler fh0])
                              k))))]
+       [#s(pat:ord pattern group index)
+        #`(let ([pr* (ps-add pr '#s(ord group index))])
+            (parse:S x cx pattern pr* es k))]
        [#s(pat:post pattern)
         #`(let ([pr* (ps-add-post pr)])
             (parse:S x cx pattern pr* es k))]
@@ -680,6 +683,8 @@ Conventions:
         #'(first-desc:S pattern)]
        [#s(pat:commit pattern)
         #'(first-desc:S pattern)]
+       [#s(pat:ord pattern _ _)
+        #'(first-desc:S pattern)]
        [#s(pat:post pattern)
         #'(first-desc:S pattern)]
        [#s(pat:integrated _name _pred description _role)
@@ -723,8 +728,11 @@ Conventions:
             (parse:S y cy pattern pr* es k))]
        [#s(action:do (stmt ...))
         #'(let () (no-shadow stmt) ... (#%expression k))]
-       [#s(action:post pattern group index)
+       [#s(action:ord pattern group index)
-        #'(let ([pr* (ps-add-post pr 'group 'index)])
+        #'(let ([pr* (ps-add pr '#s(ord group index))])
+            (parse:A x cx pattern pr* es k))]
+       [#s(action:post pattern)
+        #'(let ([pr* (ps-add-post pr)])
             (parse:A x cx pattern pr* es k))])]))
 
 ;; (bind/sides clauses k) : expr[Ans]
@@ -852,9 +860,14 @@ Conventions:
                        (with ([cut-prompt cp0]
                               [fail-handler fh0])
                              k))))]
+       [#s(hpat:ord pattern group index)
+        #`(let ([pr* (ps-add pr '#s(ord group index))])
+            (parse:H x cx rest-x rest-cx rest-pr pattern pr* es
+                     (let ([rest-pr (ps-pop-ord rest-pr)]) k)))]
        [#s(hpat:post pattern)
-        #'(let ([pr (ps-add-post pr)])
+        #'(let ([pr* (ps-add-post pr)])
-            (parse:H x cx rest-x rest-cx rest-pr pattern pr es k))]
+            (parse:H x cx rest-x rest-cx rest-pr pattern pr* es
+                     (let ([rest-pr (ps-pop-post rest-pr)]) k)))]
        [#s(hpat:peek pattern)
         #`(let ([saved-x x] [saved-cx cx] [saved-pr pr])
             (parse:H x cx dummy-x dummy-cx dummy-pr pattern pr es

racket/collects/syntax/parse/private/rep-patterns.rkt

@@ -33,6 +33,7 @@ A SinglePattern is one of
   (pat:delimit SinglePattern)
   (pat:commit SinglePattern)
   (pat:reflect stx Arguments (listof SAttr) id (listof IAttr))
+  (pat:ord SinglePattern UninternedSymbol Nat)
   (pat:post SinglePattern)
   (pat:integrated id/#f id string stx)
 
@@ -63,6 +64,7 @@ A ListPattern is a subtype of SinglePattern; one of
 (define-struct pat:delimit (pattern) #:prefab)
 (define-struct pat:commit (pattern) #:prefab)
 (define-struct pat:reflect (obj argu attr-decls name nested-attrs) #:prefab)
+(define-struct pat:ord (pattern group index) #:prefab)
 (define-struct pat:post (pattern) #:prefab)
 (define-struct pat:integrated (name predicate description role) #:prefab)
 
@@ -74,7 +76,8 @@ A ActionPattern is one of
   (action:and (listof ActionPattern))
   (action:parse SinglePattern stx)
   (action:do (listof stx))
-  (action:post ActionPattern Quotable Nat)
+  (action:ord ActionPattern UninternedSymbol Nat)
+  (action:post ActionPattern)
 |#
 
 (define-struct action:cut () #:prefab)
@@ -83,7 +86,8 @@ A ActionPattern is one of
 (define-struct action:and (patterns) #:prefab)
 (define-struct action:parse (pattern expr) #:prefab)
 (define-struct action:do (stmts) #:prefab)
-(define-struct action:post (pattern group index) #:prefab)
+(define-struct action:ord (pattern group index) #:prefab)
+(define-struct action:post (pattern) #:prefab)
 
 #|
 A HeadPattern is one of 
@@ -96,6 +100,7 @@ A HeadPattern is one of
   (hpat:delimit HeadPattern)
   (hpat:commit HeadPattern)
   (hpat:reflect stx Arguments (listof SAttr) id (listof IAttr))
+  (hpat:ord HeadPattern UninternedSymbol Nat)
   (hpat:post HeadPattern)
   (hpat:peek HeadPattern)
   (hpat:peek-not HeadPattern)
@@ -110,6 +115,7 @@ A HeadPattern is one of
 (define-struct hpat:delimit (pattern) #:prefab)
 (define-struct hpat:commit (pattern) #:prefab)
 (define-struct hpat:reflect (obj argu attr-decls name nested-attrs) #:prefab)
+(define-struct hpat:ord (pattern group index) #:prefab)
 (define-struct hpat:post (pattern) #:prefab)
 (define-struct hpat:peek (pattern) #:prefab)
 (define-struct hpat:peek-not (pattern) #:prefab)
@@ -163,6 +169,7 @@ A SideClause is one of
       (pat:delimit? x)
       (pat:commit? x)
       (pat:reflect? x)
+      (pat:ord? x)
       (pat:post? x)
       (pat:integrated? x)))
 
@@ -173,6 +180,7 @@ A SideClause is one of
       (action:and? x)
       (action:parse? x)
       (action:do? x)
+      (action:ord? x)
       (action:post? x)))
 
 (define (head-pattern? x)
@@ -185,6 +193,7 @@ A SideClause is one of
       (hpat:delimit? x)
       (hpat:commit? x)
       (hpat:reflect? x)
+      (hpat:ord? x)
       (hpat:post? x)
       (hpat:peek? x)
       (hpat:peek-not? x)))
@@ -252,6 +261,8 @@ A SideClause is one of
      (pattern-attrs sp)]
     [(pat:commit sp)
      (pattern-attrs sp)]
+    [(pat:ord sp _ _)
+     (pattern-attrs sp)]
     [(pat:post sp)
      (pattern-attrs sp)]
     [(pat:integrated name _ _ _)
@@ -270,7 +281,9 @@ A SideClause is one of
      (pattern-attrs sp)]
     [(action:do _)
      null]
-    [(action:post sp _ _)
+    [(action:ord sp _ _)
+     (pattern-attrs sp)]
+    [(action:post sp)
      (pattern-attrs sp)]
 
     ;; -- H patterns
@@ -292,6 +305,8 @@ A SideClause is one of
      (pattern-attrs hp)]
     [(hpat:commit hp)
      (pattern-attrs hp)]
+    [(hpat:ord hp _ _)
+     (pattern-attrs hp)]
     [(hpat:post hp)
      (pattern-attrs hp)]
     [(hpat:peek hp)
@@ -352,3 +367,121 @@ A SideClause is one of
       (and (pat:head? p) (proper-list-pattern? (pat:head-tail p) trust-pair?))
       (and (pat:dots? p) (proper-list-pattern? (pat:dots-tail p) trust-pair?))
       (and (pat:action? p) (proper-list-pattern? (pat:action-inner p) trust-pair?))))
+
+;; ----
+
+(define-syntax-rule (define/memo (f x) body ...)
+  (define f
+    (let ([memo-table (make-weak-hasheq)])
+      (lambda (x)
+        (hash-ref! memo-table x (lambda () body ...))))))
+
+;; ----
+
+;; An AbsFail is a Nat encoding the bitvector { sub? : 1, post? : 1 }
+;; Finite abstraction of failuresets based on progress bins. That is:
+(define AF-NONE 0)  ;; cannot fail
+(define AF-SUB  1)  ;; can fail with progress < POST
+(define AF-POST 2)  ;; can fail with progress >= POST
+(define AF-ANY  3)  ;; can fail with progress either < or >= POST
+
+;; AF-nz? : AbsFail -> {0, 1}
+(define (AF-nz? af) (if (= af AF-NONE) 0 1))
+
+;; AF<? : AbsFail AbsFail -> Boolean
+;; True if every failure in af1 has strictly less progress than any failure in af2.
+;; Note: trivially satisfied if either side cannot fail.
+(define (AF<? af1 af2)
+  ;; (0, *), (*, 0), (1, 2)
+  (or (= af1 AF-NONE)
+      (= af2 AF-NONE)
+      (and (= af1 AF-SUB) (= af2 AF-POST))))
+
+;; pattern-absfail : *Pattern -> AbsFail
+(define/memo (pattern-AF p)
+  (define (patterns-AF ps)
+    (for/fold ([af 0]) ([p (in-list ps)]) (bitwise-ior af (pattern-AF p))))
+  (cond [(pat:any? p) AF-NONE]
+        [(pat:svar? p) AF-NONE]
+        [(pat:var/p? p) AF-ANY]
+        [(pat:literal? p) AF-SUB]
+        [(pat:datum? p) AF-SUB]
+        [(pat:action? p) (bitwise-ior (pattern-AF (pat:action-action p))
+                                      (pattern-AF (pat:action-inner p)))]
+        [(pat:head? p) AF-ANY]
+        [(pat:dots? p) AF-ANY]
+        [(pat:and? p) (patterns-AF (pat:and-patterns p))]
+        [(pat:or? p) (patterns-AF (pat:or-patterns p))]
+        [(pat:not? p) AF-SUB]
+        [(pat:pair? p) AF-SUB]
+        [(pat:vector? p) AF-SUB]
+        [(pat:box? p) AF-SUB]
+        [(pat:pstruct? p) AF-SUB]
+        [(pat:describe? p) (pattern-AF (pat:describe-pattern p))]
+        [(pat:delimit? p) (pattern-AF (pat:delimit-pattern p))]
+        [(pat:commit? p) (pattern-AF (pat:commit-pattern p))]
+        [(pat:reflect? p) AF-ANY]
+        [(pat:ord? p) (pattern-AF (pat:ord-pattern p))]
+        [(pat:post? p) (if (AF-nz? (pattern-AF (pat:post-pattern p))) AF-POST AF-NONE)]
+        [(pat:integrated? p) AF-SUB]
+        ;; Action patterns
+        [(action:cut? p) AF-NONE]
+        [(action:fail? p) AF-SUB]
+        [(action:bind? p) AF-NONE]
+        [(action:and? p) (patterns-AF (action:and-patterns p))]
+        [(action:parse? p) (if (AF-nz? (pattern-AF (action:parse-pattern p))) AF-SUB AF-NONE)]
+        [(action:do? p) AF-NONE]
+        [(action:ord? p) (pattern-AF (action:ord-pattern p))]
+        [(action:post? p) (if (AF-nz? (pattern-AF (action:post-pattern p))) AF-POST AF-NONE)]
+        ;; Head patterns, eh patterns, etc
+        [else AF-ANY]))
+
+;; pattern-cannot-fail? : *Pattern -> Boolean
+(define (pattern-cannot-fail? p)
+  (= (pattern-AF p) AF-NONE))
+
+;; pattern-can-fail? : *Pattern -> Boolean
+(define (pattern-can-fail? p)
+  (not (pattern-cannot-fail? p)))
+
+;; patterns-AF-sorted? : (Listof *Pattern) -> AF/#f
+;; Returns AbsFail (true) if any failure from pattern N+1 has strictly
+;; greater progress than any failure from patterns 0 through N.
+(define (patterns-AF-sorted? ps)
+  (for/fold ([af AF-NONE]) ([p (in-list ps)])
+    (define afp (pattern-AF p))
+    (and af (AF<? af afp) (bitwise-ior af afp))))
+
+;; create-post-pattern : *Pattern -> *Pattern
+(define (create-post-pattern p)
+  (cond [(pattern-cannot-fail? p)
+         p]
+        [(pattern? p)
+         (pat:post p)]
+        [(head-pattern? p)
+         (hpat:post p)]
+        [(action-pattern? p)
+         (action:post p)]
+        [else (error 'syntax-parse "INTERNAL ERROR: create-post-pattern ~e" p)]))
+
+;; create-ord-pattern : *Pattern UninternedSymbol Nat -> *Pattern
+(define (create-ord-pattern p group index)
+  (cond [(pattern-cannot-fail? p)
+         p]
+        [(pattern? p)
+         (pat:ord p group index)]
+        [(head-pattern? p)
+         (hpat:ord p group index)]
+        [(action-pattern? p)
+         (action:ord p group index)]
+        [else (error 'syntax-parse "INTERNAL ERROR: create-ord-pattern ~e" p)]))
+
+;; ord-and-patterns : (Listof *Pattern) UninternedSymbol -> (Listof *Pattern)
+;; If at most one subpattern can fail, no need to wrap.  More
+;; generally, if possible failures are already consistent with and
+;; ordering, no need to wrap.
+(define (ord-and-patterns patterns group)
+  (cond [(patterns-AF-sorted? patterns) patterns]
+        [else
+         (for/list ([p (in-list patterns)] [index (in-naturals)])
+           (create-ord-pattern p group index))]))

racket/collects/syntax/parse/private/rep.rkt

@@ -406,20 +406,24 @@
    (cond [(pair? sides)
           (define group (gensym*))
           (define actions-pattern
+            (create-post-pattern
              (action:and
               (for/list ([side (in-list sides)] [index (in-naturals)])
-               (side-clause->pattern side group index))))
+                (create-ord-pattern (side-clause->pattern side) group index)))))
-          (cond [splicing? (hpat:and pattern (pat:action actions-pattern (pat:any)))]
+          (define and-patterns
-                [else (pat:and (list pattern (pat:action actions-pattern (pat:any))))])]
+            (ord-and-patterns (list pattern (pat:action actions-pattern (pat:any)))
+                              (gensym*)))
+          (cond [splicing? (apply hpat:and and-patterns)]
+                [else (pat:and and-patterns)])]
          [else pattern])))
 
-;; side-clause->pattern : SideClause UninternedSymbol Nat -> ActionPattern
+;; side-clause->pattern : SideClause -> ActionPattern
-(define (side-clause->pattern side group index)
+(define (side-clause->pattern side)
   (match side
     [(clause:fail condition message)
-     (action:post (action:fail condition message) group index)]
+     (action:fail condition message)]
     [(clause:with wpat expr defs)
-     (let ([ap (action:post (action:parse wpat expr) group index)])
+     (let ([ap (action:parse wpat expr)])
        (if (pair? defs) (action:and (list (action:do defs) ap)) ap))]
     [(clause:attr attr expr)
      (action:bind (list side))]
@@ -927,7 +931,8 @@
   ;; allow-action? = allowed to *return* pure action pattern;
   ;; all ~and patterns are allowed to *contain* action patterns
   (define patterns0 (parse-cdr-patterns stx decls allow-head? #t))
-  (define-values (actions patterns) (split-prefix patterns0 action-pattern?))
+  (define patterns1 (ord-and-patterns patterns0 (gensym*)))
+  (define-values (actions patterns) (split-prefix patterns1 action-pattern?))
   (cond [(null? patterns)
          (cond [allow-action?
                 (action:and actions)]
@@ -1047,7 +1052,7 @@
     [(_ pattern)
      (let ([p (parse-*-pattern #'pattern decls allow-head? allow-action?)])
        (cond [(action-pattern? p)
-              (cond [allow-action? (action:post p #f 0)]
+              (cond [allow-action? (action:post p)]
                     [(not allow-head?) (pat:post (action-pattern->single-pattern p))]
                     [else (wrong-syntax stx "action pattern not allowed here")])]
              [(head-pattern? p)

racket/collects/syntax/parse/private/runtime-progress.rkt

@@ -4,15 +4,18 @@
 (provide ps-empty
          ps-add-car
          ps-add-cdr
-         ps-add-post
          ps-add-stx
          ps-add-unbox
          ps-add-unvector
          ps-add-unpstruct
          ps-add-opaque
-         (struct-out post)
+         ps-add-post
+         ps-add
+         (struct-out ord)
 
          ps-pop-opaque
+         ps-pop-ord
+         ps-pop-post
          ps-context-syntax
          ps-difference
 
@@ -56,7 +59,8 @@ A Progress Frame (PF) is one of
   - stx     ;; "Base" frame, or ~parse/#:with term
   - 'car    ;; car of pair; also vector->list, unbox, struct->list, etc
   - nat     ;; Represents that many repeated cdrs
-  - #s(post group index) ;; late/post-traversal check, only comparable w/in group
+  - 'post   ;; late/post-traversal check
+  - #s(ord group index) ;; ~and subpattern, only comparable w/in group
   - 'opaque
 
 The error-reporting context (ie, syntax-parse #:context arg) is always
@@ -77,7 +81,7 @@ Interpretation: later frames are applied first.
       means ( car of ( cdr once of stx ) )
       NOT apply car, then apply cdr once, then stop
 |#
-(define-struct post (group index) #:prefab)
+(define-struct ord (group index) #:prefab)
 
 (define (ps-empty stx ctx)
   (if (eq? stx ctx)
@@ -93,8 +97,6 @@ Interpretation: later frames are applied first.
          (cons (+ times n) (cdr parent))]
         [_
          (cons times parent)])))
-(define (ps-add-post parent [group #f] [index 0])
-  (cons (post group index) parent))
 (define (ps-add-stx parent stx)
   (cons stx parent))
 (define (ps-add-unbox parent)
@@ -105,6 +107,10 @@ Interpretation: later frames are applied first.
   (ps-add-car parent))
 (define (ps-add-opaque parent)
   (cons 'opaque parent))
+(define (ps-add parent frame)
+  (cons frame parent))
+(define (ps-add-post parent)
+  (cons 'post parent))
 
 ;; ps-context-syntax : Progress -> syntax
 (define (ps-context-syntax ps)
@@ -114,29 +120,47 @@ Interpretation: later frames are applied first.
 ;; ps-difference : PS PS -> nat
 ;; Returns N s.t. B = (ps-add-cdr^N A)
 (define (ps-difference a b)
-  (define (whoops)
+  (define-values (a-cdrs a-base)
-    (error 'ps-difference "~e is not an extension of ~e" a b))
+    (match a
-  (match (list a b)
+      [(cons (? exact-positive-integer? a-cdrs) a-base)
-    [(list (cons (? exact-positive-integer? na) pa)
+       (values a-cdrs a-base)]
-           (cons (? exact-positive-integer? nb) pb))
+      [_ (values 0 a)]))
-     (unless (equal? pa pb) (whoops))
+  (define-values (b-cdrs b-base)
-     (- nb na)]
+    (match b
-    [(list pa (cons (? exact-positive-integer? nb) pb))
+      [(cons (? exact-positive-integer? b-cdrs) b-base)
-     (unless (equal? pa pb) (whoops))
+       (values b-cdrs b-base)]
-     nb]
+      [_ (values 0 b)]))
-    [_
+  (unless (eq? a-base b-base)
-     (unless (equal? a b) (whoops))
+    (error 'ps-difference "INTERNAL ERROR: ~e does not extend ~e" b a))
-     0]))
+  (- b-cdrs a-cdrs))
 
 ;; ps-pop-opaque : PS -> PS
 ;; Used to continue with progress from opaque head pattern.
 (define (ps-pop-opaque ps)
   (match ps
     [(cons (? exact-positive-integer? n) (cons 'opaque ps*))
-     (cons n ps*)]
+     (ps-add-cdr ps* n)]
     [(cons 'opaque ps*)
      ps*]
-    [_ (error 'ps-pop-opaque "opaque marker not found: ~e" ps)]))
+    [_ (error 'ps-pop-opaque "INTERNAL ERROR: opaque frame not found: ~e" ps)]))
+
+;; ps-pop-ord : PS -> PS
+(define (ps-pop-ord ps)
+  (match ps
+    [(cons (? exact-positive-integer? n) (cons (? ord?) ps*))
+     (ps-add-cdr ps* n)]
+    [(cons (? ord?) ps*)
+     ps*]
+    [_ (error 'ps-pop-ord "INTERNAL ERROR: ord frame not found: ~e" ps)]))
+
+;; ps-pop-post : PS -> PS
+(define (ps-pop-post ps)
+  (match ps
+    [(cons (? exact-positive-integer? n) (cons 'post ps*))
+     (ps-add-cdr ps* n)]
+    [(cons 'post ps*)
+     ps*]
+    [_ (error 'ps-pop-post "INTERNAL ERROR: post frame not found: ~e" ps)]))
 
 
 ;; == Expectations ==

racket/collects/syntax/parse/private/runtime-report.rkt

@@ -86,16 +86,21 @@ deals with the fact that they might not be talking about the same terms.
 (define (maximal-failures fs)
   (maximal/progress
    (for/list ([f (in-list fs)])
-     (cons f (failure-progress f)))))
+     (cons (failure-progress f) f))))
 
 #|
 Progress ordering
 -----------------
 
-Lexicographic generalization of partial order on frames
+Nearly a lexicographic generalization of partial order on frames.
-  CAR < CDR < POST, stx incomparable except to self
+  (( CAR < CDR ) || stx ) < POST )
-  (post g i1) < (post g i2) if i1 < i2
+  - stx incomparable except with self
-  (post g1 i1) incomp (post g2 i2) when g1 != g2
+
+But ORD prefixes are sorted out (and discarded) before comparison with 
+rest of progress. Like post, ord comparable only w/in same group:
+  - (ord g n1) < (ord g n2) if n1 < n2
+  - (ord g1 n1) || (ord g2 n2) when g1 != g2
+
 
 Progress equality
 -----------------
@@ -122,104 +127,114 @@ ie (ps->stx+index ps1) = (ps->stx+index ps2).
            (loop (cdr ps) (cdr ps))]
           [else (loop (cdr ps) acc)])))
 
-;; maximal/progress : (listof (cons A IPS)) -> (listof (listof A))
+;; maximal/progress : (listof (cons IPS A)) -> (listof (listof A))
 ;; Eliminates As with non-maximal progress, then groups As into
 ;; equivalence classes according to progress.
 (define (maximal/progress items)
   (cond [(null? items)
          null]
         [(null? (cdr items))
-         (list (list (car (car items))))]
+         (list (list (cdr (car items))))]
         [else
-         (let-values ([(rNULL rCAR rCDR rPOST rSTX leastCDR)
+         (let loop ([items items] [non-ORD-items null])
-                       (partition/pf items)])
+           (define-values (ORD non-ORD)
-           (append (maximal/pf rNULL rCAR rCDR rPOST leastCDR)
+             (partition (lambda (item) (ord? (item-first-prf item))) items))
-                   (if (pair? rSTX)
+           (cond [(pair? ORD)
-                       (maximal/stx rSTX)
+                  (loop (maximal-prf1/ord ORD) (append non-ORD non-ORD-items))]
-                       null)))]))
-
-;; partition/pf : (listof (cons A IPS)) -> (listof (cons A IPS))^5 & nat/#f
-;; Partition by progress first frame (or lack thereof). leastCDR is #f iff rCDR is null
-(define (partition/pf items)
-  (let ([rNULL null] [rCAR null] [rCDR null] [rPOST null] [rSTX null] [leastCDR #f])
-    (for ([a+ips (in-list items)])
-      (let ([ips (cdr a+ips)])
-        (cond [(null? ips)
-               (set! rNULL (cons a+ips rNULL))]
-              [(eq? (car ips) 'car)
-               (set! rCAR (cons a+ips rCAR))]
-              [(exact-positive-integer? (car ips))
-               (set! rCDR (cons a+ips rCDR))
-               (set! leastCDR (if leastCDR (min leastCDR (car ips)) (car ips)))]
-              [(post? (car ips))
-               (set! rPOST (cons a+ips rPOST))]
-              [(syntax? (car ips))
-               (set! rSTX (cons a+ips rSTX))]
                  [else
-               (error 'syntax-parse "INTERNAL ERROR in partition/pf: ~e" ips)])))
+                  (maximal/prf1 (append non-ORD non-ORD-items))]))]))
-    (values rNULL rCAR rCDR rPOST rSTX leastCDR)))
 
-;; maximal/pf : (listof (cons A IPS))^4 & nat/#f -> (listof (listof A))
+;; maximal/prf1 : (Listof (Cons IPS A) -> (Listof (Listof A))
-(define (maximal/pf rNULL rCAR rCDR rPOST leastCDR)
+(define (maximal/prf1 items)
-  (cond [(pair? rPOST)
+  (define-values (POST rest1)
-         (maximal/post rPOST)]
+    (partition (lambda (item) (eq? 'post (item-first-prf item))) items))
-        [(pair? rCDR)
+  (cond [(pair? POST)
-         (maximal/progress (rmap (lambda (a+ips) (pop-item-ips-ncdrs a+ips leastCDR)) rCDR))]
+         (maximal/progress (map item-pop-prf POST))]
-        [(pair? rCAR)
-         (maximal/progress (rmap pop-item-ips rCAR))]
-        [(pair? rNULL)
-         (list (map car rNULL))]
         [else
-         null]))
+         (define-values (STX rest2)
+           (partition (lambda (item) (syntax? (item-first-prf item))) rest1))
+         (define-values (CDR rest3)
+           (partition (lambda (item) (exact-integer? (item-first-prf item))) rest2))
+         (define-values (CAR rest4)
+           (partition (lambda (item) (eq? 'car (item-first-prf item))) rest3))
+         (define-values (NULL rest5)
+           (partition (lambda (item) (eq? '#f (item-first-prf item))) rest4))
+         (unless (null? rest5)
+           (error 'syntax-parse "INTERNAL ERROR: bad progress: ~e\n" rest5))
+         (append
+          (maximal/stx STX)
+          (cond [(pair? CDR)
+                 (define leastCDR (apply min (map item-first-prf CDR)))
+                 (maximal/progress (map (lambda (item) (item-pop-prf-ncdrs item leastCDR)) CDR))]
+                [(pair? CAR)
+                 (maximal/progress (map item-pop-prf CAR))]
+                [(pair? NULL)
+                 (list (map cdr NULL))]
+                [else null]))]))
 
-;; maximal/post : (NEListof (cons A IPS)) -> (NEListof (NEListof A))
+;; maximal-prf1/ord : (NEListof (Cons IPS A)) -> (NEListof (Cons IPS A))
-;; PRE: Each IPS starts with a post frame.
+;; PRE: each item has ORD first frame
-(define (maximal/post items)
+;; Keep only maximal by first frame and pop first frame from each item.
-  ;; groups : (Listof (Listof (cons A IPS)))
+(define (maximal-prf1/ord items)
-  (define groups (group-by (lambda (a+ips) (post-group (car (cdr a+ips)))) items))
+  ;; groups : (NEListof (NEListof (cons A IPS)))
-  (define groups* (map post-group-max-items groups))
+  (define groups (group-by (lambda (item) (ord-group (item-first-prf item))) items))
-  (append*
-   (for/list ([group (in-list groups*)])
-     (maximal/progress (map pop-item-ips group)))))
-
-;; post-group-max-items : (NEListof (cons A IPS)) -> (Listof (cons A IPS))
-;; PRE: Each IPS starts with a post frame; all items have same post-group.
-;; Keep only items with max post-index.
-(define (post-group-max-items items)
-  (let loop ([items items] [best-items null] [best-index -inf.0])
-    (cond [(null? items) (reverse best-items)]
-          [else
-           (define item0 (car items))
-           (define index0 (post-index (car (cdr item0))))
-           (cond [(> index0 best-index)
-                  (loop (cdr items) (list item0) index0)]
-                 [(= index0 best-index)
-                  (loop (cdr items) (cons item0 best-items) best-index)]
-                 [else
-                  (loop (cdr items) best-items best-index)])])))
-
-;; maximal/stx : (listof (cons A IPS)) -> (listof (listof A))
-;; PRE: Each IPS starts with a stx frame.
-(define (maximal/stx rSTX)
-  ;; groups : (Listof (Listof (cons A IPS)))
-  (define groups (group-by (lambda (a+ips) (car (cdr a+ips))) rSTX))
   (append*
    (for/list ([group (in-list groups)])
-     (maximal/progress (map pop-item-ips group)))))
+     (define group* (filter-max group (lambda (item) (ord-index (item-first-prf item)))))
+     (map item-pop-prf group*))))
 
-;; pop-item-ips : (cons A IPS) -> (cons A IPS)
+;; maximal/stx : (NEListof (cons IPS A)) -> (NEListof (NEListof A))
-(define (pop-item-ips a+ips)
+;; PRE: Each IPS starts with a stx frame.
-  (let ([a (car a+ips)]
+(define (maximal/stx items)
-        [ips (cdr a+ips)])
+  ;; groups : (Listof (Listof (cons IPS A)))
-    (cons a (cdr ips))))
+  (define groups (group-by item-first-prf items))
+  (append*
+   (for/list ([group (in-list groups)])
+     (maximal/progress (map item-pop-prf group)))))
 
-;; pop-item-ips-ncdrs : (cons A IPS) -> (cons A IPS)
+;; filter-max : (Listof X) (X -> Nat) -> (Listof X)
+(define (filter-max xs x->nat)
+  (let loop ([xs xs] [nmax -inf.0] [r-keep null])
+    (cond [(null? xs)
+           (reverse r-keep)]
+          [else
+           (define n0 (x->nat (car xs)))
+           (cond [(> n0 nmax)
+                  (loop (cdr xs) n0 (list (car xs)))]
+                 [(= n0 nmax)
+                  (loop (cdr xs) nmax (cons (car xs) r-keep))]
+                 [else
+                  (loop (cdr xs) nmax r-keep)])])))
+
+;; item-first-prf : (cons IPS A) -> prframe/#f
+(define (item-first-prf item)
+  (define ips (car item))
+  (and (pair? ips) (car ips)))
+
+;; item-split-ord : (cons IPS A) -> (cons IPS (cons IPS A))
+(define (item-split-ord item)
+  (define ips (car item))
+  (define a (cdr item))
+  (define-values (rest-ips r-ord)
+    (let loop ([ips ips] [r-ord null])
+      (cond [(and (pair? ips) (ord? (car ips)))
+             (loop (cdr ips) (cons (car ips) r-ord))]
+            [else (values ips r-ord)])))
+  (list* (reverse r-ord) rest-ips a))
+
+;; item-pop-prf : (cons IPS A) -> (cons IPS A)
+(define (item-pop-prf item)
+  (let ([ips (car item)]
+        [a (cdr item)])
+    (cons (cdr ips) a)))
+
+;; item-pop-prf-ncdrs : (cons IPS A) -> (cons IPS A)
 ;; Assumes first frame is nat > ncdrs.
-(define (pop-item-ips-ncdrs a+ips ncdrs)
+(define (item-pop-prf-ncdrs item ncdrs)
-  (let ([a (car a+ips)]
+  (let ([ips (car item)]
-        [ips (cdr a+ips)])
+        [a (cdr item)])
-    (cond [(= (car ips) ncdrs) (cons a (cdr ips))]
+    (cond [(= (car ips) ncdrs) (cons (cdr ips) a)]
-          [else (cons a (cons (- (car ips) ncdrs) (cdr ips)))])))
+          [else (cons (cons (- (car ips) ncdrs) (cdr ips)) a)])))
 
 ;; ps->stx+index : Progress -> (cons Syntax Nat)
 ;; Gets the innermost stx that should have a real srcloc, and the offset
@@ -239,7 +254,9 @@ ie (ps->stx+index ps1) = (ps->stx+index ps2).
       [(cons (? exact-positive-integer? n) parent)
        (for/fold ([stx (interp parent)]) ([i (in-range n)])
          (stx-cdr stx))]
-      [(cons (? post?) parent)
+      [(cons (? ord?) parent)
+       (interp parent)]
+      [(cons 'post parent)
        (interp parent)]))
   (let ([ps (ps-truncate-opaque ps)])
     (match ps
@@ -249,14 +266,11 @@ ie (ps->stx+index ps1) = (ps->stx+index ps2).
        (cons (interp ps) 0)]
       [(cons (? exact-positive-integer? n) parent)
        (cons (interp parent) n)]
-      [(cons (? post?) parent)
+      [(cons (? ord?) parent)
+       (ps->stx+index parent)]
+      [(cons 'post parent)
        (ps->stx+index parent)])))
 
-(define (rmap f xs)
-  (let loop ([xs xs] [acc null])
-    (cond [(pair? xs) (loop (cdr xs) (cons (f (car xs)) acc))]
-          [else acc])))
-
 
 ;; ============================================================
 ;; Expectation simplification