Hanoi.hss

flatten-module

-- do the w/w split
consider 'hanoi
{ ww-split-unsafe [| wrap |] [| unwrap |] }

{ binding-of 'work
  remember origwork

  any-call (unfold 'unwrap)

  -- establish the zero base case
  [ def-rhs, lam-body, lam-body, lam-body, lam-body]
  case-split-inline 'n
  { case-alt 0 ; any-call (unfold 'f) ; simplify }

  -- establish the one base case
  { [case-alt 1, alt-rhs] ; case-split-inline 'a
    { case-alt 0 ; any-call (unfold 'f) ; simplify
      any-call (unfold origwork)
      any-call (forward (ww-assumption-A-unsafe [| wrap |] [| unwrap |]))
      any-call (unfold 'f)
      simplify
      any-call (unfold-rule "[] ++")
      any-call (unfold-rule "++ []")
    }
    { case-alt 1 ; any-call (unfold 'f) ; simplify

      any-call (unfold origwork)
      any-call (forward (ww-assumption-A-unsafe [| wrap |] [| unwrap |]))
      any-call (unfold 'f)
      innermost let-subst ; simplify

      -- recursion decrements by two, so must do this again
      any-call (unfold origwork)
      any-call (forward (ww-assumption-A-unsafe [| wrap |] [| unwrap |]))

      -- time to let intro
      -- need a "occurance 'work" like consider
      { alt-rhs
        { arg 5
          { arg 1
            { arg 1 ; let-intro 'u }
            { arg 2 ; arg 2 ; let-intro 'v }
          }
          { arg 2 ; arg 2 ; arg 1 ; let-intro 'w }
        }
        innermost let-float
        try (reorder-lets ['u,'v,'w])
        any-call (fold 'u)
        any-call (fold 'v)
        any-call (fold 'w)
        let-tuple 'uvw
        any-call (fold 'unwrap)
        any-call (fold origwork)
      }
    }
  }
}
innermost let-elim