(;module:
  lux
  (lux (data [bool "B/" Eq<Bool>]
             [text "T/" Eq<Text>]
             [number]
             (coll [list "L/" Functor<List> Fold<List> Monoid<List>]
                   ["s" set])))
  (luxc (lang ["la" analysis]
              ["ls" synthesis])
        (synthesizer ["&;" function])))

(def: (bound-vars path)
  (-> ls;Path (List ls;Variable))
  (case path
    (#ls;BindP register)
    (list (nat-to-int register))

    (^or (#ls;SeqP pre post) (#ls;AltP pre post))
    (L/compose (bound-vars pre) (bound-vars post))
    
    _
    (list)))

(def: (path-bodies path)
  (-> ls;Path (List ls;Synthesis))
  (case path
    (#ls;ExecP body)
    (list body)

    (#ls;SeqP pre post)
    (path-bodies post)

    (#ls;AltP pre post)
    (L/compose (path-bodies pre) (path-bodies post))
    
    _
    (list)))

(def: (non-arg? arity var)
  (-> ls;Arity ls;Variable Bool)
  (and (&function;local? var)
       (n.> arity (int-to-nat var))))

(type: Tracker (s;Set ls;Variable))

(def: init-tracker Tracker (s;new number;Hash<Int>))

(def: (unused-vars current-arity bound exprS)
  (-> ls;Arity (List ls;Variable) ls;Synthesis (List ls;Variable))
  (let [tracker (loop [exprS exprS
                       tracker (L/fold s;add init-tracker bound)]
                  (case exprS
                    (#ls;Variable var)
                    (if (non-arg? current-arity var)
                      (s;remove var tracker)
                      tracker)
                    
                    (#ls;Variant tag last? memberS)
                    (recur memberS tracker)

                    (#ls;Tuple membersS)
                    (L/fold recur tracker membersS)

                    (#ls;Call funcS argsS)
                    (L/fold recur (recur funcS tracker) argsS)
                    
                    (^or (#ls;Recur argsS)
                         (#ls;Procedure name argsS))
                    (L/fold recur tracker argsS)

                    (#ls;Let offset inputS outputS)
                    (|> tracker (recur inputS) (recur outputS))

                    (#ls;If testS thenS elseS)
                    (|> tracker (recur testS) (recur thenS) (recur elseS))

                    (#ls;Loop offset initsS bodyS)
                    (recur bodyS (L/fold recur tracker initsS))

                    (#ls;Case inputS outputPS)
                    (let [tracker' (L/fold s;add
                                           (recur inputS tracker)
                                           (bound-vars outputPS))]
                      (L/fold recur tracker' (path-bodies outputPS)))

                    (#ls;Function arity env bodyS)
                    (L/fold s;remove tracker env)

                    _
                    tracker
                    ))]
    (s;to-list tracker)))

## (def: (optimize-register-use current-arity [pathS bodyS])
##   (-> ls;Arity [ls;Path ls;Synthesis] [ls;Path ls;Synthesis])
##   (let [bound (bound-vars pathS)
##         unused (unused-vars current-arity bound bodyS)
##         adjusted (adjust-vars unused bound)]
##     [(|> pathS (clean-pattern adjusted) simplify-pattern)
##      (clean-expression adjusted bodyS)]))