#|
The state recorded here does not affect programs that run in ACL2-language-level,
but these bindings occur in enough ACL2 code that we just fake their presence.

We make a modest effort to report a useful error wrt ACL2's `state'.  It's a reserved
name unless state is available, in which case it may be used as a parameter name.
Real ACL2 enforces more restrictions than we do.
|#
(module parameters mzscheme
  (require (file "constants.scm"))
  (provide (all-defined-except real-state false->nil))
  
  (define (false->nil x)
    (if (eq? x #f)
        nil
        x))
  (define set-irrelevant-formals-ok
    (make-parameter nil
                    (lambda (x) (let ([value (false->nil x)]) value))))
  (define set-guard-checking
    (make-parameter 
     t 
     (lambda (x)
       (let ([value (false->nil x)])
         #;(acl2-repl `(set-guard-checking ,(acl2-if value 't 'nil)))
         value))))
  
  (define-for-syntax state-ok? (make-parameter #f))
  
  (define-syntax (set-state-ok stx)
    (syntax-case stx (nil)
      [(_ nil) (begin (state-ok? #f) #'nil)]
      [(_ e) (begin (state-ok? #t) #'t)]))
  
  (define-syntax (real-state stx)
    (syntax-case stx ()
      [(_ st) (if (state-ok?) 
               (syntax 'STATE) 
               (raise-syntax-error 'state "State is not enabled; use (set-state-ok t) to enable it" #'st))]))
  (define-syntax state
    (syntax-id-rules ()
      [state (real-state state)]))
  
  (define set-ignore-ok
    (make-parameter nil
                    (lambda (x) (let ([value (false->nil x)]) value))))
  
  (define set-compile-fns 
    (make-parameter 
     nil 
     (lambda (x)
       (let ([value (false->nil x)])
         #;(acl2-repl `(set-compile-fns ,(acl2-if value 't 'nil)))
         value))))
  
  
  )