propagate

(in-package "CGEN")

(include-book "basis")

(include-book "utilities")

(include-book "misc/expander" :dir :system)

(defun easy-simplify-term1-fn
  (term hyps
    hints
    equiv
    normalize
    rewrite
    repeat
    backchain-limit
    state)
  (declare (xargs :mode :program :stobjs state))
  (b* ((world (w state)) ((er hint-settings) (translate-hint-settings 'simp-term
          "Goal"
          hints
          'easy-simplify-term
          world
          state))
      (ens (ens state))
      (base-rcnst (change rewrite-constant
          *empty-rewrite-constant*
          :current-enabled-structure ens
          :force-info t))
      ((er rcnst) (load-hint-settings-into-rcnst hint-settings
          base-rcnst
          nil
          world
          'easy-simplify-term
          state))
      (ens (access rewrite-constant
          rcnst
          :current-enabled-structure))
      ((mv flg hyps-type-alist ?ttree) (hyps-type-alist hyps
          ens
          world
          state))
      ((when flg) (mv "Contradiction in the hypotheses" nil state))
      ((mv ?step-limit
         new-term
         ?new-ttree
         state) (pc-rewrite* term
          hyps-type-alist
          (if (eq equiv 'equal)
            nil
            (list (make congruence-rule
                :rune *fake-rune-for-anonymous-enabled-rule*
                :nume nil
                :equiv equiv)))
          (eq equiv 'iff)
          world
          rcnst
          nil
          nil
          normalize
          rewrite
          ens
          state
          repeat
          backchain-limit
          (initial-step-limit world state))))
    (value new-term)))

(def easy-simplify-term
  (term hyps hints state)
  (decl :sig ((pseudo-term pseudo-term-list
       true-list
       state) ->
      (mv erp pseudo-term state))
    :mode :program :doc "simplify term under hyps. erp is T if hyps have a contradiction
  in them. return the simplifed term in error triple")
  (easy-simplify-term1-fn term
    hyps
    hints
    'equal
    't
    't
    1000
    1000
    state))

(def easy-simplify-terms
  (terms hyps hints state)
  (decl :sig ((pseudo-term pseudo-term-list
       true-list
       state) ->
      (mv erp pseudo-term state))
    :mode :program :doc "loop over simplify-term")
  (if (endp terms)
    (value nil)
    (er-let* ((sterm (easy-simplify-term (car terms)
           hyps
           hints
           state)) (rest (easy-simplify-terms (cdr terms)
            hyps
            hints
            state)))
      (value (cons sterm rest)))))

(def simplify-term
  (hyp other-hyps hints state)
  (decl :sig ((pseudo-term pseudo-term-list
       true-list
       state) ->
      (mv erp pseudo-term state))
    :mode :program :doc "simplify term under hyps. erp is T if hyps have a contradiction
  in them. return the simplifed term in error triple")
  (b* ((ens (ens state)) (wrld (w state))
      (ctx 'simplify-term)
      ((mv erp x state) (tool2-fn0 hyp
          other-hyps
          'iff
          ctx
          ens
          wrld
          state
          hints
          nil
          t
          nil
          nil
          nil))
      (shyp (if erp
          hyp
          (normalize-no-ttree (cadr x)
            t
            nil
            ens
            wrld))))
    (value shyp)))

(def simplify-term-lst
  (terms hyps hints state)
  (decl :sig ((pseudo-term pseudo-term-list
       true-list
       state) ->
      (mv erp pseudo-term state))
    :mode :program :doc "loop over simplify-term, but be conservative")
  (if (endp terms)
    (value nil)
    (b* ((term (car terms)) ((er sterm) (simplify-term (car terms)
            hyps
            hints
            state))
        (simplified? (term-order sterm term))
        (sterm (if simplified?
            sterm
            term))
        ((er rest) (simplify-term-lst (cdr terms)
            hyps
            hints
            state)))
      (value (cons sterm rest)))))

(include-book "acl2s/defdata/defdata-util" :dir :system)

(defun type-hyp-p
  (hyp wrld)
  (and (consp hyp)
    (let ((hyp (expand-lambda hyp)))
      (and (is-type-predicate (car hyp) wrld)
        (proper-symbolp (cadr hyp))))))

(def simplify-hyps1
  (rem-hyps init-hyps
    hints
    ans.
    vl
    state)
  (decl :sig ((pseudo-term-list pseudo-term-list
       true-list
       pseudo-term-list
       bool
       state) ->
      (mv erp pseudo-term state))
    :mode :program :doc "simplify each hyp in rem-hyps assuming init-hyps (minus
  hyp), accumulate in ans. and return a value triple containing shyps
  and an error triple if a contradiction is found in an syhp")
  (if (endp rem-hyps)
    (value ans.)
    (b* ((hyp (car rem-hyps)) (other-hyps (remove1-equal hyp init-hyps))
        ((er shyp) (easy-simplify-term hyp
            other-hyps
            hints
            state))
        (simplified? (term-order shyp hyp))
        ((when (equal shyp ''nil)) (mv t ans. state))
        (- (cw? (and (debug-flag vl) (not simplified?))
            "~|ACHTUNG: simplify-hyps result not less than hyp in term-order~|"))
        (shyp-list (expand-assumptions-1 shyp)))
      (simplify-hyps1 (cdr rem-hyps)
        init-hyps
        hints
        (cond ((type-hyp-p hyp (w state)) (append ans. (list hyp)))
          ((equal shyp ''t) ans.)
          (t (append ans. shyp-list)))
        vl
        state))))

(def simplify-hyps-under-assignment
  (hyps x a vl state)
  (decl :sig ((pseudo-term-list symbol
       quoted-constant
       boolean
       state) ->
      (mv erp pseudo-term-list state))
    :mode :program :doc "simplify hyps assuming x=a. return shyps in an error
        triple. erp=T if contradiction found in shyps")
  (b* ((hyps (remove-duplicates-equal hyps)) (hyps1 (subst-var-lst a x hyps))
      ((er shyps1) (simplify-hyps1 hyps1
          hyps1
          'nil
          'nil
          vl
          state)))
    (simplify-hyps1 shyps1
      shyps1
      'nil
      'nil
      vl
      state)))

(def translate-lst
  (terms state)
  (decl :sig ((true-list true-list state) ->
      (mv erp pseudo-term-list state))
    :mode :program :doc "loop over translate")
  (if (endp terms)
    (value nil)
    (er-let* ((sterm (translate (car terms)
           t
           t
           t
           "t-lst"
           (w state)
           state)) (rest (translate-lst (cdr terms) state)))
      (value (cons sterm rest)))))

(def propagate
  (x a
    hyps
    concl
    vl
    state)
  (decl :sig ((symbol pseudo-term
       pseudo-term-list
       pseudo-term
       fixnum
       state) ->
      (mv erp
        (list pseudo-term-list pseudo-term)
        state))
    :mode :program :doc "propagate the assignment of a to variable x by using a utility
  function from tools/easy-simplify.lisp (earlier I was using
  expander.lisp). return (mv erp (shyps sconcl) state) where erp might be T
  indicating discovery of inconsistency/contradiction in the hypotheses")
  (b* (((er shyps) (simplify-hyps-under-assignment hyps
         x
         a
         vl
         state)) (- (cw? (debug-flag vl)
          "~|CEGen/Debug/Propagate: ~x0 ---~x1=~x2--> ~x3~|"
          hyps
          x
          a
          shyps))
      (?eq-hyp (list 'equal x a))
      ((er sconcl) (simplify-term (subst-var a x concl)
          shyps
          nil
          state))
      (- (cw? (debug-flag vl)
          "~|CEGen/Debug/Propagate: ~x0 ---~x1=~x2--> ~x3~|"
          concl
          x
          a
          sconcl))
      ((when (or (equal sconcl 't) (equal sconcl ''t))) (mv t nil state))
      (vars (all-vars-lst (cons sconcl shyps))))
    (assert$ (not (member-eq x vars))
      (mv nil
        (list vars shyps sconcl)
        state))))