{"size": 1973, "ext": "scrbl", "max_stars_repo_path": "rosette/guide/scribble/datatypes/procedures.scrbl", "max_stars_repo_name": "remysucre/rosette", "max_stars_repo_stars_event_min_datetime": null, "max_stars_repo_stars_event_max_datetime": null, "max_issues_repo_path": "rosette/guide/scribble/datatypes/procedures.scrbl", "max_issues_repo_name": "remysucre/rosette", "max_issues_repo_issues_event_min_datetime": null, "max_issues_repo_issues_event_max_datetime": null, "max_forks_repo_path": "rosette/guide/scribble/datatypes/procedures.scrbl", "max_forks_repo_name": "remysucre/rosette", "max_forks_repo_forks_event_min_datetime": "2016-01-27T20:39:05.000Z", "max_forks_repo_forks_event_max_datetime": "2016-01-27T20:39:05.000Z"}
{"max_stars_count": null, "max_issues_count": null, "max_forks_count": 1, "avg_line_length": 45.8837209302, "max_line_length": 156, "alphanum_fraction": 0.6761277243}
#lang scribble/manual

@(require (for-label 
           rosette/base/form/define rosette/query/query rosette/query/eval  
           rosette/base/core/term  
           (only-in rosette/base/core/safe assert) 
           racket)
          scribble/core scribble/html-properties scribble/eval racket/sandbox racket/runtime-path
          "../util/lifted.rkt")


@(define-runtime-path root ".")
@(define rosette-eval (rosette-log-evaluator (logfile root "procedures-log")))

@(define proc-ops (select '(procedure? apply compose compose1 procedure-rename procedure->method procedure-closure-contents-eq? )))
@(define more-proc-ops (select '(identity const thunk thunk* negate curry curryr normalized-arity? normalize-arity arity=? arity-includes? prop:procedure)))

@title[#:tag "sec:proc"]{Procedures}

Rosette procedures are references to procedure objects, just like in Racket.  
Two procedure references are @racket[eq?] and @racket[equal?] only if they point to the 
same procedure object.  Procedures may be concrete or symbolic.  Symbolic procedures  
may, in the worst case, take as much time to execute as the slowest concrete procedure to 
which any symbolic procedure could @racket[evaluate] under any @racket[solution?].

@(rosette-eval '(require (only-in racket string->symbol)))
@examples[#:eval rosette-eval
(define-symbolic b boolean?)
(define-symbolic x integer?)
(code:line (define p (if b * -)) (code:comment "p is a symbolic procedure"))
(define sol (synthesize #:forall (list x)
                        #:guarantee (assert (= x (p x 1)))))
(evaluate p sol)
(define sol (synthesize #:forall (list x)
                        #:guarantee (assert (= x (p x 0)))))
(evaluate p sol)                                                         
]

Rosette lifts the following operations on procedures:
@tabular[#:style (style #f (list (attributes '((id . "lifted")(class . "boxed")))))
(list (list @elem{@proc-ops,  @more-proc-ops}))]

@(kill-evaluator rosette-eval)