From 179f9ce01d17eacd120ce0bdd254bbbc7cbc3e3d Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Mon, 9 Jan 2006 18:09:28 +0000 Subject: [PATCH] removed reduction-semantics collection svn: r1791 --- collects/reduction-semantics/doc.txt | 930 ------------- .../examples/arithmetic.ss | 47 - .../reduction-semantics/examples/beginner.ss | 961 -------------- .../reduction-semantics/examples/church.ss | 63 - .../examples/combinators.ss | 83 -- .../reduction-semantics/examples/control.ss | 81 -- collects/reduction-semantics/examples/eta.ss | 72 -- .../reduction-semantics/examples/future.ss | 123 -- .../examples/ho-contracts.ss | 567 -------- collects/reduction-semantics/examples/info.ss | 2 - .../reduction-semantics/examples/iswim.ss | 255 ---- .../reduction-semantics/examples/macro.ss | 47 - .../reduction-semantics/examples/omega.ss | 64 - .../examples/semaphores.ss | 190 --- .../examples/subject-reduction.ss | 96 -- .../reduction-semantics/examples/threads.ss | 128 -- .../reduction-semantics/examples/types.ss | 91 -- collects/reduction-semantics/generator.ss | 245 ---- collects/reduction-semantics/graph.ss | 1023 --------------- collects/reduction-semantics/gui.ss | 565 -------- collects/reduction-semantics/helper.ss | 206 --- collects/reduction-semantics/info.ss | 4 - collects/reduction-semantics/mc.ss | 376 ------ collects/reduction-semantics/private/info.ss | 2 - .../reduction-semantics/private/make-plt.ss | 37 - .../private/matcher-test.ss | 634 --------- .../reduction-semantics/private/matcher.ss | 1145 ----------------- .../private/red-sem-macro-helpers.ss | 31 - .../reduction-semantics/private/subst-test.ss | 120 -- collects/reduction-semantics/private/term.ss | 54 - .../reduction-semantics.ss | 317 ----- collects/reduction-semantics/subst.ss | 292 ----- 32 files changed, 8851 deletions(-) delete mode 100644 collects/reduction-semantics/doc.txt delete mode 100644 collects/reduction-semantics/examples/arithmetic.ss delete mode 100644 collects/reduction-semantics/examples/beginner.ss delete mode 100644 collects/reduction-semantics/examples/church.ss delete mode 100644 collects/reduction-semantics/examples/combinators.ss delete mode 100644 collects/reduction-semantics/examples/control.ss delete mode 100644 collects/reduction-semantics/examples/eta.ss delete mode 100644 collects/reduction-semantics/examples/future.ss delete mode 100644 collects/reduction-semantics/examples/ho-contracts.ss delete mode 100644 collects/reduction-semantics/examples/info.ss delete mode 100644 collects/reduction-semantics/examples/iswim.ss delete mode 100644 collects/reduction-semantics/examples/macro.ss delete mode 100644 collects/reduction-semantics/examples/omega.ss delete mode 100644 collects/reduction-semantics/examples/semaphores.ss delete mode 100644 collects/reduction-semantics/examples/subject-reduction.ss delete mode 100644 collects/reduction-semantics/examples/threads.ss delete mode 100644 collects/reduction-semantics/examples/types.ss delete mode 100644 collects/reduction-semantics/generator.ss delete mode 100644 collects/reduction-semantics/graph.ss delete mode 100644 collects/reduction-semantics/gui.ss delete mode 100644 collects/reduction-semantics/helper.ss delete mode 100644 collects/reduction-semantics/info.ss delete mode 100644 collects/reduction-semantics/mc.ss delete mode 100644 collects/reduction-semantics/private/info.ss delete mode 100644 collects/reduction-semantics/private/make-plt.ss delete mode 100644 collects/reduction-semantics/private/matcher-test.ss delete mode 100644 collects/reduction-semantics/private/matcher.ss delete mode 100644 collects/reduction-semantics/private/red-sem-macro-helpers.ss delete mode 100644 collects/reduction-semantics/private/subst-test.ss delete mode 100644 collects/reduction-semantics/private/term.ss delete mode 100644 collects/reduction-semantics/reduction-semantics.ss delete mode 100644 collects/reduction-semantics/subst.ss diff --git a/collects/reduction-semantics/doc.txt b/collects/reduction-semantics/doc.txt deleted file mode 100644 index 5a19a8f94c..0000000000 --- a/collects/reduction-semantics/doc.txt +++ /dev/null @@ -1,930 +0,0 @@ -_Reduction Semantics_ -_reduction-semantics_ - -This collection provides three files: - - _reduction-semantics.ss_: the core reduction semantics - library - - _gui.ss_: a _visualization tool for reduction sequences_. - - _subst.ss_: a library for _capture avoiding substitution_. - -In addition, the examples subcollection contains several -small languages to demonstrate various different uses of -this tool: - - _arithmetic.ss_: an arithmetic language with every - possible order of evaluation - - _church.ss_: church numerals with call by name - normal order evaluation - - _combinators.ss_: fills in the gaps in a proof in - Berendrecht that i and j (defined in the file) are - a combinator basis - - _future.ss_: an adaptation of Cormac Flanagan's future - semantics. - - _ho-contracts.ss_: computes the mechanical portions of a - proof in the Contracts for Higher Order Functions paper - (ICFP 2002). Contains a sophisticated example use of an - alternative pretty printer. - - _macro.ss_: models macro expansion as a reduction semantics. - - _omega.ss_: the call by value lambda calculus with call/cc. - Includes omega and two call/cc-based infinite loops, one of - which has an ever-expanding term size and one of which has - a bounded term size. - - _threads.ss_: shows how non-deterministic choice can be - modeled in a reduction semantics. Contains an example use - of a simple alternative pretty printer. - - _semaphores.ss_: a simple threaded language with semaphores - - - iswim.ss : see further below. - -====================================================================== - -The _reduction-semantics.ss_ library defines a pattern -language, used in various ways: - - pattern = any - | number - | string - | variable - | (variable-except ...) - | hole - | (hole ) - | - | (name ) - | (in-hole ) - | (in-named-hole ) - | (side-condition ) - | (cross >) - | (pattern ...) - | - -The patterns match sexpressions. The _any_ pattern matches -any sepxression. The _number_ pattern matches any -number. The _string_ pattern matches any string. Those three -patterns may also be suffixed with an underscore and another -identifier, in which case they bind the full name (as if it -were an implicit `name' pattern) and match the portion -before the underscore. - -The _variable_ pattern matches any symbol. The -_variable-except_ pattern matches any variable except those -listed in its argument. This is useful for ensuring that -keywords in the language are not accidentally captured by -variables. - -The _hole_ pattern matches anything when inside a matching -in-hole pattern. The (hole ) variation on that -pattern is used in conjunction with in-named-hole to support -languages that require multiple patterns in a hole. - -The __ pattern stands for a literal symbol that must -match exactly, unless it is the name of a non-terminal in a -relevant language or contains an underscore. - -If it is a non-terminal, it matches any of the right-hand -sides of that non-terminal. - -If the symbol is a non-terminal followed by an underscore, -for example e_1, it is implicitly the same as a name pattern -that matches only the non-terminal, (name e_1 e) for the -example. If the symbol otherwise has an underscore, it is -an error. - -_name_: The pattern: - - (name ) - -matches and binds using it to the name . - -_in-hole_: The (in-hole ) matches the first -pattern. This match must include exactly one match against the `hole' -pattern. The `hole' pattern matches any sexpression. Then, the -sexpression that matched the hole pattern is used to match against the -second pattern. - -_in-named-hole_: The pattern: - - (in-named-hole ) - -is similar in spirit to in-hole, except that it supports -languages with multiple holes in a context. The first -argument identifies which hole, using the (hole ) -pattern that this expression requires and the rest of the -arguments are just like in-hole. That is, if there are -multiple holes in a term, each matching a different (hole -) pattern, this one selects only the holes that are -named by the first argument to in-named-hole. - -_side-condition_: The (side-condition pattern guard) pattern matches -what the embedded pattern matches, and then the guard expression is -evaluated. If it returns #f, the pattern fails to match, and if it -returns anything else, the pattern matches. In addition, any -occurrences of `name' in the pattern are bound using `term-let' -(see below) in the guard. - -_cross_: The (cross ) pattern is used for the compatible -closure functions. If the language contains a non-terminal with the -same name as , the pattern (cross ) matches the -context that corresponds to the compatible closure of that -non-terminal. - -The (pattern ...) pattern matches a sexpression list, where -each pattern matches an element of the list. In addition, if -a list pattern contains an ellipses that is not treated as a -literal, instead it matches any number of duplications of the -pattern that came before the ellipses (including 0). Furthermore, -each (name ) in the duplicated pattern -binds a list of matches to , instead of a single match. -(A nested duplicated pattern creates a list of list matches, -etc.) Ellipses may be placed anywhere inside the row of -patterns, except in the first position or immediately after -another ellipses. Multiple ellipses are allowed. - -> (language (non-terminal pattern ...) ...) SYNTAX - -This form defines a context-free language. As an example, -this is the lambda calculus: - - (define lc-lang - (language (e (e e ...) - variable - v) - (c (v ... c e ...) - hole) - (v (lambda (variable ...) e)))) - -with non-terminals e for the expression language, c for the -evaluation contexts and v for values. - -> compiled-lang? : (any? . -> . boolean?) - -Returns #t if its argument was produced by `language', #f -otherwise. - -> (term-let ([tl-pat expr] ...) body) SYNTAX - -Matches each given id pattern to the value yielded by -evaluating the corresponding expr and binds each variable in -the id pattern to the appropriate value (described -below). These bindings are then accessible to the `term' -syntactic form. - -Identifier-patterns are terms in the following grammar: - - tl-pat ::= identifier - | (tl-pat-ele ...) -tl-pat-ele ::= tl-pat - | tl-pat ellipses - -where ellipses is the literal symbol consisting of three -dots (and the ... indicates repetition as usual). If tl-pat -is an identifier, it matches any value and binds it to the -identifier, for use inside `term'. If it is a list, it -matches only if the value being matched is a list value and -only if every subpattern recursively matches the -corresponding list element. There may be a single ellipsis -in any list pattern; if one is present, the pattern before -the ellipses may match multiple adjacent elements in the -list value (possibly none). - -> (term s-expr) SYNTAX - -This form is used for construction of new s-expressions in -the right-hand sides of reductions. It behaves identically -to quasiquote except that names bound by `term-let' are -implicitly substituted with the values that those names were -bound to, expanding ellipses as in-place sublists (in the -same manner as syntax-case patterns). - -For example, - -(term-let ([body '(+ x 1)] - [(expr ...) '(+ - (values * /))] - [((id ...) ...) '((a) (b) (c d))]) - (term (let-values ([(id ...) expr] ...) body))) - -evaluates to - -'(let-values ([(a) +] - [(b) -] - [(c d) (values * /)]) - (+ x 1)) - -It is an error for a term variable to appear in an -expression with an ellipsis-depth different from the depth -with which it was bound by `term-let'. It is also an error -for two `term-let'-bound identifiers bound to lists of -different lengths to appear together inside an ellipsis. - -> (reduction language pattern bodies ...) SYNTAX - -This form defines a reduction. The first position must -evaluate to a language defined by the `language' form. The -pattern determines which terms this reductions apply to and -the last bodies are expressions that must evaluate to a new -sexpression corresponding to the reduct for this term. The -bodies are implicitly wrapped in a begin. - -As an example, the reduction for the lambda calculus above -would be written like this: - - (reduction lc-lang - (in-hole (name c c) - ((lambda (variable_i ...) e_body) - v_i ...)) - (plug - (term c) - (foldl lc-subst (term e_body) - (term (v_i ...)) - (term (variable_i ...))))) - -The in-hole pattern matches a term against `c', and binds -what matches the hole to `hole'. Then, it matches what -matched the hole against ((lambda (variable) e) v). - -Because of the name pattern and the subscripted variable names -we used, c, hole, variable_i, e_body, and v_i -are bound with `term-let' in the right hand side of the -reduction. Then, when the reduction matches, the result is -the result of evaluating the last argument to reduction. -See `plug' below and lc-subst is defined by using the -subst.ss library below. - -> (reduction/name name language pattern bodies ...) SYNTAX - -The reduction/name form is the same as reduction, but -additionally evaluates the `name' expression and names the -reduction to be its result, which must be a string. The -names are used by `traces'. - -> (reduction/context language context pattern bodies ...) SYNTAX - -reduction/context is a short-hand form of reduction. It -automatically adds the `in-hole' pattern and the call to -`plug'. The equivalent reduction/context to the above -example is this: - - (reduction/context - lang - c - ((lambda (variable_i ...) e_body) v_i ...) - (lc-subst (term (variable_i ...)) - (term (v_i ...)) - (term e_body)))) - -> (reduction/context/name name language context pattern bodies ...) SYNTAX - -reduction/context/name is the same as reduction/context, but -additionally evaluates the `name' expression and names the -reduction to be its result, which must be a string. -The names are used by `traces'. - - -> red? : (any? . -> . boolean?) - -Returns #t if its argument is a reduction (produced by `reduction', -`reduction/context', etc.), #f otherwise. - -> compatible-closure : (red? - compiled-lang? - symbol? - . -> . - red?) - -This function accepts a reduction, a language, the name of a -non-terminal in the language and returns the compatible -closure of the reduction for the specified non-terminal. - -> context-closure : (red? - compiled-lang? - any - . -> . - red?) - -This function accepts a reduction, a language, a pattern -representing a context (ie, that can be used as the first -argument to `in-hole'; often just a non-terminal) in the -language and returns the closure of the reduction -in that context. - -> plug : (any? any? . -> . any) - -The first argument to this function is an sexpression to -plug into. The second argument is the sexpression to replace -in the first argument. It returns the replaced term. - -> reduce : ((listof red?) any? . -> . (listof any?)) - -Reduce accepts a list of reductions, a term, and returns a -list of terms that the term reduces to. - -> language->predicate : (compiled-lang? - symbol? - . -> . - (any? . -> . boolean?)) - -Takes a language and a non-terminal name and produces -a predicate that matches instances of the non-terminal. - -> match-pattern : (compiled-pattern - any/c - . -> . - (union false? (listof mtch?))) - -This is mostly used to explore a particular pattern to -determine what is going wrong. It accepts a compiled pattern -and a and returns #f if the pattern doesn't match the term, -and returns a list of mtch structure if the terms do match. - -> compile-pattern : (compiled-lang? any? . -> . compiled-pattern) - -This is mostly used in conjunction with match-pattern to -explore particular patterns and terms when debugging. It -compiles a sexpression pattern to a pattern. - -> mtch? : (any/c . -> . boolean?) - -Determines if a value is a mtch structure. - -> mtch-bindings : (mtch? -> bindings?) - -This returns a bindings structure (see below) that -binds the pattern variables in this match. - -> mtch-context : (mtch? . -> . any/c) - -Returns the current context being built up for a -match. Usually, this is the same as the original term being -matched. - -> mtch-hole : (mtch? . -> . (union none? any/c)) - -Returns the current contents of the hole for this match (if -there was a decomposition). Usually returns none. - -> variable-not-in : (any? symbol? . -> . symbol?) - -This helper function accepts an sexpression and a -variable. It returns a variable not in the sexpression with -a prefix the same as the second argument. - -> make-bindings : ((listof rib?) . -> . bindings?) -> bindings? : (any? . -> . boolean?) -> bindings-table : (bindings? . -> . (listof rib?)) - -Constructor, predicate, and selector functions for the bindings values -returned by match-pattern. Each bindings value represents the bindings -established for a single parse of the term; multiple such parses may be -possible in some situations. - -> make-rib : (symbol? any? . -> . rib?) -> rib? : (any? . -> . boolean?) -> rib-name : (rib? . -> . symbol?) -> rib-exp : (rib? . -> . any?) - -Constructor, predicate, and selector functions for the rib values contained -within a bindings. Each rib associates a name with an s-expression from -the language, or a list of such s-expressions, if the (name ...) clause is -followed by an ellipsis. Nested ellipses produce nested lists. - -====================================================================== - -The _gui.ss_ library provides three functions: - -> (traces language reductions expr [pp] [colors]) - -This function calls traces/multiple with language, reductions -and (list expr), and its optional arguments if supplied. - -> (traces/multiple lang reductions exprs [pp] [colors]) - -This function calls traces/pred with the predicate -(lambda (x) #t) - -> (traces/pred lang reductions exprs pred [pp] [colors]) - lang : language - reductions : (listof reduction) - exprs : (listof sexp) - pred : (sexp -> boolean) - pp : (any -> string) - | (any port number (is-a?/c text%) -> void) - colors : (listof (list string string)) - -This function opens a new window and inserts each -expr. Then, reduces the terms until either -reduction-steps-cutoff (see below) different terms are -found, or no more reductions can occur. It inserts each new -term into the gui. Clicking the `reduce' button reduces -until reduction-steps-cutoff more terms are found. - -The pred function indicates if this term has a particular -property. If the function returns #t, the term is displayed -normally. If it returns #f, the term is displayed with a -red border. - -If the pp function can take four arguments, it renders its -first argument into the port (its second argument) with -width at most given by the number (its third argument). The -final argument is the text where the port is connected -- -characters written to the port go to the end of the editor. -If the pp function cannot take four arguments, it is -instead invoked with a single argument, the s-expression to -render, and it must return a string which the GUI will use -as a representation of the given expression for display. - -The default pp, provided as default-pretty-printer, uses -MzLib's pretty-print function. See threads.ss in the -examples directory for an example use of the one-argument -form of this argument and ho-contracts.ss in the examples -directory for an example use of its four-argument form. - -The colors argument, if provided, specifies a list of -reduction-name/color-string pairs. The traces gui will color -arrows drawn because of the given reduction name with the -given color instead of using the default color. - -You can save the contents of the window as a postscript file -from the menus. - -> (reduction-steps-cutoff) -> (reduction-steps-cutoff number) - -A parameter that controls how many steps the `traces' function -takes before stopping. - -> (initial-font-size) -> (initial-font-size number) - -A parameter that controls the initial font size for the terms shown -in the GUI window. - -> (initial-char-width) -> (initial-char-width number) - -A parameter that determines the initial width of the boxes -where terms are displayed (measured in characters) - -> (dark-pen-color color-or-string) -> (dark-pen-color) => color-or-string - -> (dark-brush-color color-or-string) -> (dark-brush-color) => color-or-string - -> (light-pen-color color-or-string) -> (light-pen-color) => color-or-string - -> (light-brush-color color-or-string) -> (light-brush-color) => color-or-string - -These four parameters control the color of the edges in the graph. - -====================================================================== - -The _subst.ss_ library provides these names: - -> (subst (match-pattern subst-rhs ...) ...) SYNTAX - -The result of this form is a function that performs capture -avoiding substitution for a particular (sexp-based) -language. The function accepts three arguments, a variable, -a term to substitute and a term to substitute into. - -Each of the `match-pattern's specify the forms of -the language and the `subst-rhs's specify what kind of form -it is. Each of the match-patterns are in (lib "match.ss" -"match")'s pattern language and any variable that they bind -are available in the 's described below. - -The language of the subst-rhs follows. - -> (variable) - - this means that the rhs for this form is a symbol that - should be treated like a variable. Nothing may follow - this. - -> (constant) - - this means that the rhs for this form is a constant that - cannot be renamed. Nothing may follow this. - -> (all-vars ) - -This form indicates that this pattern in the language binds -the variables produced by the -. - -Immediately following this in a subst-rhs must be a (build -...) form and some number of (subterm ...) or (subterms ...) -forms. - -> (build ) - -This form must come right after an (all-vars ...) form and -before any (subterm ...) or (subterms ...) forms. - -This form tells subst how to reconstruct this term. The - must evaluate to a procedure that -accepts the (possibly renamed) variables from the all-vars -clause, and one argument for each of the subterms that -follow this declaration (with subterms flattened into the -argument list) in the same order that the subterm or -subterms declarations are listed. - -> (subterm ) - -The first must be a list of variables -that is a sub-list of the variables in the all-vars -expression. The second expression must be an sexp -corresponding to one of the subexpressions of this -expression (matched by the match-patten for this clause of -subst). - -> (subterms ) - -The first must be a list of variables -that is a sub-list of the variables in the all-vars -expression. The second expression must be an sexp -corresponding to one of the subexpressions of this -expression (matched by the match-patten for this clause of -subst). - -Consider this example of a substitution procedure for the -lambda calculus: - - (define lc-subst - (subst - [`(lambda ,vars ,body) - (all-vars vars) - (build (lambda (vars body) `(lambda ,vars ,body))) - (subterm vars body)] - [(? symbol?) (variable)] - [(? number?) (constant)] - [`(,fun ,@(args ...)) - (all-vars '()) - (build (lambda (vars fun . args) `(,fun ,@args))) - (subterm '() fun) - (subterms '() args)])) - -The first clause matches lambda expressions with any number -of arguments and says that there is one subterm, the body of -the lambda, and that all of the variables are bound in it. - -The second clause matches symbols and indicates that they -are variables. - -The third clause matches numbers and indicates that they are -constants. - -The final clause matches function applications. The -`all-vars' shows that applications introduce no new -names. The build procedure reconstructs a new application -form. The subterm declaration says that the function -position is a subterm with no variables bound in it. The -subterms declaration says that all of the arguments are -subterms and that they do not introduce any new terms. - -In this program, lc-subst is bound to a function that does -the substitution. The first argument is the variable to -substitute for, the second is the term to substitute and the -final argument is the term to substitute into. For example, -this call: - - (lc-subst 'q - '(lambda (x) y) - '((lambda (y) (y q)) (lambda (y) y))) - -produces this output: - - '((lambda (y@) (y@ (lambda (x) y))) (lambda (y) y)) - -This library also provides: - -> (plt-subst (match-pattern subst-rhs ...) ...) SYNTAX - -This is identical to subst, described above, except that -the pattern language used is that from (lib "plt-match.ss"), -instead of (lib "match.ss"). - -> subst/proc -> alpha-rename -> free-vars/memoize - -Theses functions are the procedure-based interface to -substitution that subst expands to and uses. - -====================================================================== - -The _iswim.ss_ module in the "examples" sub-collection defines a -grammar and reductions from "Programming Languages and Lambda Calculi" -by Felleisen and Flatt. - - Example S-expression forms of ISWIM expressions: - Book S-expr - ---- ------ - (lambda x . x) ("lam" x x) - (+ '1` '2`) ("+" 1 2) - ((lambda y y) '7`) (("lam" y y) 7) - - CK machine: - Book S-expr - ---- ------ - <(lambda x . x), mt> (("lam" x x) : "mt") - - CEK machine: - Book S-expr - ---- ------ - <<(lambda x . x), ((("lam" x x) - {>}>, : ((X (5 : ())))) - mt> : "mt") - - The full grammar: - - (language (M (M M) - (o1 M) - (o2 M M) - V) - (V X - ("lam" variable M) - b) - (X variable) - (b number) - (o1 "add1" "sub1" "iszero") - (o2 "+" "-" "*" "^") - (on o1 o2) - - ;; Evaluation contexts: - (E hole - (E M) - (V E) - (o1 E) - (o2 E M) - (o2 V E)) - - ;; Continuations (CK machine): - (k "mt" - ("fun" V k) - ("arg" M k) - ("narg" (V ... on) (M ...) k)) - - ;; Environments and closures (CEK): - (env ((X = vcl) ...)) - (cl (M : env)) - (vcl (V- : env)) - - ;; Values that are not variables: - (V- ("lam" variable M) - b) - - ;; Continuations with closures (CEK); - (k- "mt" - ("fun" vcl k-) - ("arg" cl k-) - ("narg" (vcl ... on) (cl ...) k-))) - - The following are provided by "iswim.ss" (case-insensitively): - - Grammar and substitution: -> iswim-grammar : compiled-lang? -> M? : (any? . -> . boolean?) -> V? : (any? . -> . boolean?) -> o1? : (any? . -> . boolean?) -> o2? : (any? . -> . boolean?) -> on? : (any? . -> . boolean?) -> k? : (any? . -> . boolean?) -> env? : (any? . -> . boolean?) -> cl? : (any? . -> . boolean?) -> vcl? : (any? . -> . boolean?) -> k-? : (any? . -> . boolean?) -> iswim-subst : (M? symbol? M? . -> . M?) -> empty-env : env? -> env-extend : (env? symbol? vcl? . -> . env?) -> env-lookup : (env? symbol? . -> . (union false? vcl?)) - Reductions: -> beta_v : red? -> delta : (listof red?) -> ->v : (listof red?) -> :->v : (listof red?) - Abbreviations: -> if0 : (M? M? M? . -> . M?) -> true : M? -> false : M? -> mkpair : M? -> fst : M? -> snd : M? -> Y_v : M? -> sum : M? - Helpers: -> delta*1 : (o1? V? . -> . (union false? V?)) - delta as a function for unary operations. -> delta*2 : (o2? V? V? . -> . (union false? V?)) - delta as a function for binary operations. -> delta*n : (on? (listof V?) . -> . (union false? V?)) - delta as a function for any operation. - -====================================================================== - -The _helper.ss_ module provides additional helper functions and syntax. - - ------- Memoization ------- - -> (define-memoized (f arg ...) expr ...) SYNTAX - - Like `define' for function definitions, except that the function is - "memoized": it automatically remembers each result, and when `eq?' - arguments are provided later, the same result is returned - immediately. - -> (lambda-memoized (arg ...) expr) SYNTAX - - Like `lambda' except that the resulting function is "memoized" (see - `define-memoized' above). - - ------- Matching ------- - -> (lang-match-lambda (variable) grammar-expr - [pattern bodies ...] ...) SYNTAX - - Combines a pattern-matching dispatch with a `lambda', producing a - function that takes a single argument and pattern-matches. Each - `pattern' is as for `reduction', and the names that the pattern - binds are visible in the `bodies'. - -> (lang-match-lambda* (variable ...) main-variable grammar-expr - [pattern bodies ...] ...) SYNTAX - - Generalizes `lang-match-lambda' to create a multi-arity procedure. - The `main-variable' must be one of the `variables', and it is the - variable used for matching. - -> lang-match-lambda-memoized SYNTAX -> lang-match-lambda-memoized* SYNTAX - - Memoized versions of the above. - - ------- Backtracking ------- - -A function that supports backtracking must returns one of the -following: - - * #f to indicate failure - * any other value to indicate simple success - * (many-results l) to indicates success with any of the - results in the list l - * (explore-results ...) or (explore-parallel-results ...), - which explores the results of recursive calls to generate - one or more result values lazily - -Whenever the backtracking function calls itself (or another -backtracking function in a cooperative set), it should use -`explore-results' or `explore-parallel-results' instead of -inspecting the value directly. To get a single result from -the backtracking function, uses `first-result'. - -> many-results : ((listof any) . -> . any) - -Aggregates potential results for future exploration. - -> (explore-results (id) backtrackable-expr SYNTAX - body-expr ...) - - Evaluates `backtrackable-expr'. In the simple case, `id' is bound to - the result, the the result of the `explore-results' expression is - the result of evaluating `body-expr's. - - If `backtrackable-expr' produces multiple alternatives (via - `many-results') or if it produces a backtrackable computation, the - result is a backtrackable computation. This backtrackable - computation proceeds bey generating each successful result from - `backtrackable-expr', and then feeding the result to the - `body-expr's to refine the results. Naturally, `body-expr' can - contain further uses of `explore-results' or `many-results' which are - folded into the backtracking exploration. - -> (explore-parallel-results (results-id) backtrackable-list-expr - body-expr ...) - - Generalizes `explore-results' where `backtrackable-list-expr' - produces a list of backtrackable results, and `body-expr' is called - with successful combinations aggregated into `results-id' as a list. - -> first-result : (any . -> . any) - - If the argument to `first-result' is a backtrackable computation, it - is explored to obtain the first success, and that success is - returned. If complete backtracking fails, the result is #f. If the - argument to `first-result' is any other value, it is returned - immediately. - - ------- Misc ------- - -> function-reduce* : ((listof red?) - any? - (any? . -> . boolean?) - number? - . -> . (listof any?)) - - A poor-man's `gui' for test interaction. The first argument - represents a set of reductions that define a function; the second - argument is the starting expression; the third argument is a - predicate to recognize ending expressions; the fourth argument - limits the number of steps taken. The function applies the - reductions repeatedly until an ending expression is found, or until - the reduction gets stuck. (If the reduction produces multiple - results, an exception is raised.) The result is the list of - expressions leading to the ending expression. - -> unique-names? : ((listof symbol?) . -> . boolean?) - - Checks a list of symbols, returning #t if each symbol appears - only once in the list, #f otherwise. - -> generate-string : (-> string?) - - Returns a string that is generated by incrementing a counter. - -> all-of : (any? (any? . -> . any) . -> . (listof any?)) - - Takes an arbitrary S-expression as the first argument, and a - predicate as the second argument. all-of' then traverses the pairs - that make up the S-expression, calling the predicate on every pair - and every value within a pair. The result is the list of values for - which the predicate returned true. (If the predicate returns true - for a pair, the search does not enter the pair.) - -> transitive-closure : ((listof pair?) . -> . (listof (listof any?)) - - Given the representation of a function as a list of pairs, - `transitive-closure' produces the transitive closure as a list of - lists. Each nested list begins with a domain item and continues - with a list of range items. - - Example: - (transitive-closure '((a . b) (b . c))) = '((a b c) (b c)) - - The input function must be complete (i.e., all range elements - should be in the domain). - - Element equality is determined by `eq?' (with the expectation that - elements are usually symbols). - -====================================================================== - -The _generator.ss_ module provides a tool for generating instances of -a grammar non-terminal. - -> lang->generator-table : (lang? - (listof number?) - (listof symbol?) - (listof string?) - (listof symbol?) - number? - . -> . - generator-table?) - - Prepares generator information for a particular language, - given a set of numbers to use for the `number' keyword, - a set of symbols for `variable' and `variable-except', - and a set of string for `string'. - - The fifth argument lists keywords that appear in the grammar but - that should be skipped (to limit the generation space). The last - argument should be 0, and it is currently ignored. - -> for-each-generated : (generator-table? - (any? number? . -> . any) - generator-table? - symbol? - . -> . any) - - The first argument is a procedure to call with a series of generated - grammar instances and each term's size. Instances are generated from - smallest to largest; the size of an instance is roughly the size of - the proof tree that demonstrates grammar membership. - - The second argument is a generator table created with - `lang->generator-table'. - - The third argument is a symbol, the name of a non-terminal for which - instances should be generated. - -> for-each-generated/size : (generator-table? - (any? number? . -> . any) - generator-table? - symbol? - . -> . any) - - Like `for-each-generated', except minimum and maximum sizes are - provided, and the order of generation is arbitrary (i.e., some - larger instances may be generated before smaller instances). diff --git a/collects/reduction-semantics/examples/arithmetic.ss b/collects/reduction-semantics/examples/arithmetic.ss deleted file mode 100644 index 5515375934..0000000000 --- a/collects/reduction-semantics/examples/arithmetic.ss +++ /dev/null @@ -1,47 +0,0 @@ -(module arithmetic mzscheme - (require "../reduction-semantics.ss" - "../gui.ss") - - (define lang - (language - (e (binop e e) - (sqrt e) - number) - (binop + - - - * - /) - - (e-ctxt (binop v e-ctxt) - (binop e-ctxt e) - (sqrt e-ctxt) - hole) - (v number))) - - (define-syntax (--> stx) - (syntax-case stx () - [(_ op from to) - (syntax (reduction/name op - lang - (in-hole e-ctxt_1 from) - (term (in-hole e-ctxt_1 ,to))))])) - - (define reductions - (list - (--> "add" - (+ number_1 number_2) - (+ (term number_1) (term number_2))) - (--> "subtract" - (- number_1 number_2) - (- (term number_1) (term number_2))) - (--> "multiply" - (* number_1 number_2) - (* (term number_1) (term number_2))) - (--> "divide" - (/ number_1 number_2) - (/ (term number_1) (term number_2))) - (--> "sqrt" - (sqrt number_1) - (sqrt (term number_1))))) - - (traces lang reductions '(- (* (sqrt 36) (/ 1 2)) (+ 1 2)))) \ No newline at end of file diff --git a/collects/reduction-semantics/examples/beginner.ss b/collects/reduction-semantics/examples/beginner.ss deleted file mode 100644 index aecfb1db13..0000000000 --- a/collects/reduction-semantics/examples/beginner.ss +++ /dev/null @@ -1,961 +0,0 @@ -#| - -This is the semantics of Beginner Scheme, one of the -languages in DrScheme. - -The first test case fails because the beginner spec -is broken for that program (ie, the model faithfully -reflects the (broken) spec). - -|# - -(module beginner mzscheme - (require "../reduction-semantics.ss" - "../subst.ss" - (lib "match.ss")) - - (provide run-tests) - - #| - - `lang' below is actually more generous than beginner, but the - reductions assume that the programs are all syntactically - well-formed programs in beginner scheme (with the additional - constraints that all makers are properly applied and function- - defined variables are only applied and non-function-defined - variables are never applied -- except for the maker check, - these will be in a future version of beginner) - - still missing: many primops and characters - - are there any primops that take zero arguments? - (should that be syntacically disallowed?) - - |# - - (define lang - (language - (p (d/e ...)) - (d/e (define (x x x ...) e) - (define x (lambda (x x ...) e)) - (define x e) - (define-struct x (x ...)) - e) - (e (x e e ...) - (prim-op e ...) - (cond (e e) (e e) ...) - (cond (e e) ... (else e)) - (if e e e) - (and e e e ...) - (or e e e ...) - empty - x - 'x - number - boolean - string) - - (prim-op + / cons first rest empty? struct? symbol=?) - - (p-ctxt (d/e-v ... d/e-ctxt d/e ...)) - (d/e-ctxt (define x e-ctxt) - e-ctxt) - (e-ctxt hole - (x v ... e-ctxt e ...) - (prim-op v ... e-ctxt e ...) - (cond [false e] ... [e-ctxt e] [e e] ...) - (cond [false e] ... [e-ctxt e] [e e] ... [else e]) - (and true ... e-ctxt e ...) - (or false ... e-ctxt e ...)) - - (d/e-v (define x (lambda (x x ...) e)) - (define x v) - (define (x x x ...) e) - (define-struct x (x ...)) - v) - - (v (maker v ...) - non-struct-value) - (non-struct-value number - list-value - boolean - string - 'x) - (list-value empty - (cons v list-value)) - (boolean true - false) - - (maker (side-condition variable_1 (maker? (term variable_1)))) - - (x (side-condition - (name - x - (variable-except define - define-struct - lambda - cond - else - if - and - or - empty - true - false - quote)) - (not (prim-op? (term x))))))) - - (define beg-e-subst - (subst - [(? number?) - (constant)] - [(? symbol?) - (variable)] - ;; slight cheat here -- but since cond, if, and, or, etc - ;; aren't allowed to be variables (syntactically), we're okay. - [`(,@(e ...)) - (all-vars '()) - (build (lambda (vars . e) e)) - (subterms '() e)])) - - (define (maker? v) - (and (symbol? v) - (regexp-match #rx"^make-" (symbol->string v)))) - - (define p? (language->predicate lang 'p)) - (define prim-op? (language->predicate lang 'prim-op)) - - (define-syntax (--> stx) - (syntax-case stx () - [(_ lhs rhs) - (syntax (reduction/context lang p-ctxt lhs rhs))])) - - (define-syntax (e--> stx) - (syntax-case stx () - [(_ lhs rhs) - (syntax (reduction lang (in-hole p-ctxt lhs) rhs))])) - - (define reductions - (list - - ((and true ... false e ...) . --> . 'false) - ((and true ...) . --> . 'true) - ((side-condition (and true ... v_1 e ...) - (and (not (eq? (term v_1) 'true)) - (not (eq? (term v_1) 'false)))) - . e--> . - "and: question result is not true or false") - ((or false ... true e ...) . --> . 'true) - ((or false ...) . --> . 'false) - ((side-condition (or false ... v_1 e ...) - (and (not (eq? (term v_1) 'true)) - (not (eq? (term v_1) 'false)))) - . e--> . - "or: question result is not true or false") - - ((if true e_1 e_2) . --> . (term e_1)) - ((if false e_1 e_2) . --> . (term e_2)) - ((side-condition (if v_1 e e) - (and (not (eq? (term v_1) 'false)) - (not (eq? (term v_1) 'true)))) - . e--> . - "if: question result is not true or false") - - - ((cond (false e) ... (true e_1) (e e) ...) . --> . (term e_1)) - ((cond (false e) ... (true e_1) (e e) ... (else e)) . --> . (term e_1)) - ((cond (false e) ... (else e_1)) . --> . (term e_1)) - ((cond (false e) ...) . e--> . "cond: all question results were false") - - ((side-condition - (cond (false e) ... (v_1 e) (e e) ...) - (and (not (eq? (term v_1) 'false)) - (not (eq? (term v_1) 'true)) - (not (eq? (term v_1) 'else)))) - . e--> . - "cond: question result is not true or false") - - ((side-condition - (cond (false e) ... (v_1 e) (e e) ... (else e)) - (and (not (eq? (term v_1) 'false)) - (not (eq? (term v_1) 'true)) - (not (eq? (term v_1) 'else)))) - . e--> . - "cond: question result is not true or false") - - - ((empty? empty) . --> . 'true) - ((side-condition (empty? v_1) - (not (eq? (term v_1) 'empty))) - . --> . - 'false) - ((empty?) . e--> . "empty?: expects one argument") - ((empty? v v v ...) . e--> . "empty?: expects one argument") - - ((side-condition (cons v v_1) - (and (not (eq? (term v_1) 'empty)) - (not (and (pair? (term v_1)) - (eq? (car (term v_1)) 'cons))))) - . e--> . - "cons: second argument must be of type ") - - ((first (cons v_1 list-value)) . --> . (term v_1)) - ((first) . e--> . "first: expects one argument") - ((first v v v ...) . e--> . "first: expects one argument") - ((side-condition (first v_1) - (not (and (pair? (term v_1)) - (eq? (car (term v_1)) 'cons)))) - . e--> . - "first: expects argument of type ") - - ((rest (cons v list-value_1)) . --> . (term list-value_1)) - ((rest v v v ...) . e--> . "rest: expects one argument") - ((rest) . e--> . "rest: expects one argument") - - ((side-condition (rest v_1) - (not (and (pair? (term v_1)) - (eq? (car (term v_1)) 'cons)))) - . e--> . - "rest: expects argument of type ") - - ((symbol=? 'x_1 'x_2) . --> . (if (eq? (term x_1) (term x_2)) 'true 'false)) - ((side-condition (symbol=? v_1 v_2) - (or (not (and (pair? (term v_1)) - (eq? (car (term v_1)) 'quote))) - (not (and (pair? (term v_2)) - (eq? (car (term v_2)) 'quote))))) - . e--> . - "symbol=?: expects argument of type ") - ((symbol=?) - . e--> . - "procedure symbol=?: expects 2 arguments") - ((symbol=? v v v v ...) - . e--> . - "procedure symbol=?: expects 2 arguments") - - ((+ number_1 ...) . --> . (apply + (term (number_1 ...)))) - ((side-condition (+ v_arg ...) - (ormap (lambda (v_arg) (not (number? v_arg))) (term (v_arg ...)))) - . e--> . - "+: expects type ") - - ((side-condition (/ number_1 number_2 ...) - (andmap (lambda (number_2) (not (zero? number_2))) (term (number_2 ...)))) - . --> . - (apply / (term (number_1 number_2 ...)))) - ((side-condition (/ number_1 number_2 ...) - (ormap (lambda (number_2) (zero? number_2)) (term (number_2 ...)))) - . e--> . - "/: division by zero") - ((side-condition (/ v_arg ...) - (ormap (lambda (v_arg) (not (number? v_arg))) (term (v_arg ...)))) - . e--> . - "/: expects type ") - - ;; unbound id application - (reduction - lang - (side-condition - ((name before d/e-v) ... - (in-hole d/e-ctxt (x_f v ...)) - d/e ...) - (and (not (prim-op? (term x_f))) - (not (defined? (term x_f) (term (before ...)))))) - (format "reference to undefined identifier: ~a" (term x_f))) - - ;; procedure application as lambda - (reduction - lang - ((name before d/e-v) ... - (name defn (define x_f (lambda (x_var ...) e_body))) - (name middle d/e-v) ... - (in-hole d/e-ctxt_1 (x_f v_arg ...)) - (name after d/e) ...) - (term - (before ... - defn - middle ... - (in-hole d/e-ctxt_1 - ,(multi-subst (term (x_var ...)) (term (v_arg ...)) (term e_body))) - after ...))) - - ;; define-style procedure application - (reduction - lang - ((name before d/e-v) ... - (name defn (define (x_f x_var ...) e_body)) - (name middle d/e-v) ... - (in-hole (name ctxt d/e-ctxt) ((name f x) (name arg v) ...)) - (name after d/e) ...) - (term - (before ... - defn - middle ... - (in-hole ctxt - ,(multi-subst (term (x_var ...)) - (term (arg ...)) - (term e_body))) - after ...))) - - ;; reference to non-procedure define: - (reduction - lang - ((name before d/e-v) ... - (name defn (define (name a x) (name val v))) - (name middle d/e-v) ... - (in-hole (name ctxt d/e-ctxt) (name a x)) - (name after d/e) ...) - (term - (before ... - defn - middle ... - (in-hole ctxt val) - after ...))) - - ;; unbound reference to top-level id in hole: - (reduction - lang - (side-condition - ((name before d/e-v) ... - (in-hole d/e-ctxt (name a x)) - d/e ...) - (and (not (prim-op? (term a))) - (not (defined? (term a) (term (before ...)))))) - (format "reference to undefined identifier: ~a" (term a))) - - ;; reference to procedure-bound var in hole: - (reduction - lang - (d/e-v ... - (define ((name f x) (name var x) ...) (name body e)) - d/e-v ... - (in-hole d/e-ctxt (name f x)) - d/e ...) - (format "~a is a procedure, so it must be applied to arguments" (term f))) - - ;; reference to non-procedure-bound-var in application - (reduction - lang - (d/e-v ... - (define (name a x) (name val v)) - d/e-v ... - (in-hole d/e-ctxt ((name a x) v ...)) - d/e ...) - (format "procedure application: expected procedure, given: ~a" (term val))) - - ((struct? ((name maker maker) v ...)) . --> . 'true) - ((struct? non-struct-value) . --> . 'false) - - ;; struct predicate passes - (reduction - lang - (side-condition - ((name before d/e-v) ... - (define-struct (name struct x) ((name field x) ...)) - (name middle d/e-v) ... - (in-hole (name ctxt d/e-ctxt) ((name predicate x) ((name maker maker) v ...))) - (name after d/e) ...) - (and (maker-name-match? (term struct) (term maker)) - (predicate-name-match? (term struct) (term predicate)))) - (term - (before ... - (define-struct struct (field ...)) - middle ... - (in-hole ctxt true) - after ...))) - - ;; struct predicate fail to another struct - (reduction - lang - (side-condition - ((name before d/e-v) ... - (define-struct (name struct x) ((name field x) ...)) - (name middle d/e-v) ... - (in-hole (name ctxt d/e-ctxt) ((name predicate x) ((name maker maker) v ...))) - (name after d/e) ...) - (and (not (maker-name-match? (term struct) (term maker))) - (predicate-name-match? (term struct) (term predicate)))) - (term - (before ... - (define-struct struct (field ...)) - middle ... - (in-hole ctxt false) - after ...))) - - ;; struct predicate fail to another value - (reduction - lang - (side-condition - ((name before d/e-v) ... - (define-struct (name struct x) ((name field x) ...)) - (name middle d/e-v) ... - (in-hole (name ctxt d/e-ctxt) ((name predicate x) non-struct-value)) - (name after d/e) ...) - (predicate-name-match? (term struct) (term predicate))) - (term - (before ... - (define-struct struct (field ...)) - middle ... - (in-hole ctxt false) - after ...))) - - ;; misapplied selector 1 - (reduction - lang - (side-condition - (d/e-v - ... - (define-struct (name struct x) ((name field x) ...)) - d/e-v ... - (in-hole d/e-ctxt ((name selector x) ((name maker maker) (name arg v) ...))) - d/e ...) - (and (not (maker-name-match? (term struct) (term maker))) - (selector-name-match? (term struct) (term (field ...)) (term selector)))) - (format "~a: expects argument of matching struct" (term selector))) - - ;; misapplied selector 2 - (reduction - lang - (side-condition - (d/e-v - ... - (define-struct (name struct x) ((name field x) ...)) - d/e-v ... - (in-hole d/e-ctxt ((name selector x) non-struct-value)) - d/e ...) - (selector-name-match? (term struct) (term (field ...)) (term selector))) - (format "~a: expects argument of matching struct" (term selector))) - - ;; well-applied selector - (reduction - lang - (side-condition - ((name before d/e-v) ... - (define-struct (name struct x) ((name field x) ...)) - (name middle d/e-v) ... - (in-hole (name ctxt d/e-ctxt) ((name selector x) ((name maker maker) (name arg v) ...))) - (name after d/e) ...) - (and (maker-name-match? (term struct) (term maker)) - (selector-name-match? (term struct) (term (field ...)) (term selector)))) - (term - (before ... - (define-struct struct (field ...)) - middle ... - (in-hole ctxt - ,(list-ref (term (arg ...)) - (struct-index (term struct) - (term (field ...)) - (term selector)))) - after ...))))) - - (define (defined? f befores) - (ormap - (lambda (before) - (match before - [`(define (,a-name ,@(x ...)) ,b) - (eq? f a-name)] - [`(define ,a-name (lambda ,@(x ...))) - (eq? f a-name)] - [`(define-struct ,struct-name (,@(fields ...))) - (or (ormap (lambda (field) - (eq? f (string->symbol (format "~a-~a" struct-name field)))) - fields) - (eq? f (string->symbol (format "make-~a" struct-name))) - (eq? f (string->symbol (format "~a?" struct-name))))] - [else #t])) - befores)) - - (define (multi-subst vars args body) - (let loop ([args args] - [vars vars] - [body body]) - (cond - [(and (null? args) (null? vars)) - body] - [(or (null? args) (null? vars)) - (error 'multi-subst "malformed program")] - [else (loop (cdr args) - (cdr vars) - (beg-e-subst (car vars) (car args) body))]))) - - (define (selector-name-match? struct fields selector) - (ormap (lambda (field) (string=? (format "~a-~a" struct field) - (symbol->string selector))) - fields)) - - (define (struct-index struct init-fields selector) - (let loop ([i 0] - [fields init-fields]) - (cond - [(null? fields) (error 'struct-index "~s ~s ~s" struct init-fields selector)] - [else (let ([field (car fields)]) - (if (string=? (format "~a-~a" struct field) - (symbol->string selector)) - i - (loop (+ i 1) - (cdr fields))))]))) - - (define (maker-name-match? name maker) - (let* ([names (symbol->string name)] - [makers (symbol->string maker)] - [namel (string-length names)] - [makerl (string-length makers)]) - (and (makerl . > . namel) - (string=? (substring makers (- makerl namel) makerl) - names)))) - - (define (predicate-name-match? name predicate) - (eq? (string->symbol (format "~a?" name)) predicate)) - - (define failed-tests 0) - (define total-tests 0) - - (define (test in out) - (set! total-tests (+ total-tests 1)) - (let/ec k - (let* ([failed - (lambda (msg) - (set! failed-tests (+ failed-tests 1)) - (fprintf (current-error-port) "FAILED: ~a\n" msg) - (k (void)))] - [got (normalize in failed)]) - (unless (equal? got out) - (fprintf (current-error-port) "FAILED: ~s\ngot: ~s\nexpected: ~s\n" in got out) - (set! failed-tests (+ failed-tests 1)))))) - - (define (test-all step . steps) - (set! total-tests (+ total-tests 1)) - (let loop ([this step] - [rest steps]) - (let ([nexts (reduce reductions this)]) - (cond - [(null? rest) - (unless (null? nexts) - (set! failed-tests (+ failed-tests 1)) - (fprintf (current-error-port) "FAILED: ~s\n last step: ~s\n reduced to: ~s\n" - step - this - nexts))] - [else - (cond - [(and (pair? nexts) - (null? (cdr nexts))) - (let ([next (car nexts)]) - (if (equal? next (car rest)) - (loop (car rest) - (cdr rest)) - (begin - (set! failed-tests (+ failed-tests 1)) - (fprintf (current-error-port) - "FAILED: ~s\n step: ~s\n expected: ~s\n got: ~s\n" - step - this - (car rest) - next))))] - [else - (set! failed-tests (+ failed-tests 1)) - (fprintf (current-error-port) - "FAILED: ~s\n step: ~s\n not single step: ~s\n" - step - this - nexts)])])))) - - (define show-dots (make-parameter #f)) - (define (normalize term failed) - (let loop ([term term] - [n 1000]) - (unless (p? term) - (failed (format "not a p: ~s" term))) - (let ([nexts (reduce reductions term)]) - (when (show-dots) - (display #\.) - (flush-output)) - (cond - [(= n 0) - (when (show-dots) - (newline)) - (error 'normalize "found too many reductions")] - [(null? nexts) - (when (show-dots) - (newline)) - term] - [(string? (car nexts)) - (when (show-dots) - (newline)) - (car nexts)] - [(null? (cdr nexts)) (loop (car nexts) (- n 1))] - [else - (when (show-dots) - (newline)) - (failed (format "found more than one reduction\n ~s\n ->\n~s" term nexts))])))) - - (define (show-test-results) - (cond - [(= failed-tests 0) - (fprintf (current-error-port) "passed all ~a tests\n" total-tests)] - [else - (fprintf (current-error-port) "failed ~a out of ~a tests\n" failed-tests total-tests)])) - - (define-syntax (tests stx) - (syntax-case stx () - [(_ args ...) - (syntax - (begin - (set! failed-tests 0) - (set! total-tests 0) - args ... - (show-test-results)))])) - - (define (run-tests) - (tests - (test - '((define-struct s ()) - (s? (make-s))) - '((define-struct s ()) - true)) - - (test - '((define-struct s (a b)) - (s-a (make-s 1 3))) - '((define-struct s (a b)) - 1)) - - (test - '((define-struct s (a b)) - (s-b (make-s 1 3))) - '((define-struct s (a b)) - 3)) - - (test - '((define-struct s (a b)) - (define-struct t (x y)) - (t-x (make-s 1 2))) - "t-x: expects argument of matching struct") - - (test - '((define-struct t (x y)) - (t-x 12)) - "t-x: expects argument of matching struct") - - (test - '((define-struct s (a b)) - (define-struct t (x y)) - (s? (make-s 1 2))) - '((define-struct s (a b)) - (define-struct t (x y)) - true)) - - (test - '((define-struct s (a b)) - (define-struct t (x y)) - (t? (make-s 1 2))) - '((define-struct s (a b)) - (define-struct t (x y)) - false)) - - (test - '((define-struct s (a b)) - (struct? (make-s 1 2)) - (struct? 1)) - '((define-struct s (a b)) - true - false)) - - (test - '((define (f x) x) - (f 1)) - '((define (f x) x) - 1)) - - (test - '((define (double l) (+ l l)) - (double 2)) - '((define (double l) (+ l l)) - 4)) - - (test - '((define f (lambda (x) x)) - (f 1)) - '((define f (lambda (x) x)) - 1)) - - (test - '((define double (lambda (l) (+ l l))) - (double 2)) - '((define double (lambda (l) (+ l l))) - 4)) - - (test - '((f 1)) - "reference to undefined identifier: f") - - (test - '((f 1) - (define (f x) x)) - "reference to undefined identifier: f") - - (test - '((make-s 1) - (define-struct s (a b))) - "reference to undefined identifier: make-s") - - (test - '((+ 1 2 3)) - '(6)) - - (test - '((+ 1 "2" 3)) - "+: expects type ") - - (test - '((/ 1 2 3)) - '(1/6)) - - (test - '((/ 1 2 0 3)) - "/: division by zero") - - (test - '((/ 1 "2" 3)) - "/: expects type ") - - (test '((+ 1 (/ (+ 3 5) (+ 2 2)))) '(3)) - - (test '((symbol=? 'x 'x)) '(true)) - (test '((symbol=? 'x 'y)) '(false)) - (test '((symbol=? 1 'x)) - "symbol=?: expects argument of type ") - (test '((symbol=? 'x 1)) - "symbol=?: expects argument of type ") - - (test '((cons 1 empty)) '((cons 1 empty))) - (test '((cons 1 2)) - "cons: second argument must be of type ") - (test '((+ (first (cons 1 2)) 2)) - "cons: second argument must be of type ") - (test '((+ (first (cons 1 empty)) 2)) - '(3)) - - (test - '((first (cons 1 empty))) - '(1)) - - (test - '((first 1)) - "first: expects argument of type ") - - (test - '((first 1 2)) - "first: expects one argument") - - (test - '((first)) - "first: expects one argument") - - (test - '((rest (cons 1 empty))) - '(empty)) - - (test - '((rest 1)) - "rest: expects argument of type ") - - (test - '((rest 1 2)) - "rest: expects one argument") - - (test - '((rest)) - "rest: expects one argument") - - (test - '((empty? empty)) - '(true)) - - (test - '((empty? 1)) - '(false)) - - (test - '((empty?)) - "empty?: expects one argument") - - (test - '((empty? 1 2)) - "empty?: expects one argument") - - (test - '((cond [true 1])) - '(1)) - - (test - '((cond [else 1])) - '(1)) - - (test-all - '((cond [false 1] [else 2])) - '(2)) - - (test-all - '((cond [false 1] [false 2])) - "cond: all question results were false") - - (test - '((cond [1 1])) - "cond: question result is not true or false") - - (test - '((cond [(empty? empty) 'infinite] [else 3])) - '('infinite)) - - (test-all - '((cond [(if false false false) 'x] [(if true true true) 'y] [(if false false false) 'z])) - '((cond [false 'x] [(if true true true) 'y] [(if false false false) 'z])) - '((cond [false 'x] [true 'y] [(if false false false) 'z])) - '('y)) - - (test-all - '((cond [(if false false false) 'x] [(if true true true) 'y] [else 'z])) - '((cond [false 'x] [(if true true true) 'y] [else 'z])) - '((cond [false 'x] [true 'y] [else 'z])) - '('y)) - - (test-all - '((cond [(if false false false) 'x] [(if false false false) 'y] [else 'z])) - '((cond [false 'x] [(if false false false) 'y] [else 'z])) - '((cond [false 'x] [false 'y] [else 'z])) - '('z)) - - (test-all - '((and true true 3)) - "and: question result is not true or false") - - (test-all - '((and 1 true true)) - "and: question result is not true or false") - - (test-all - '((and true true true false)) - '(false)) - - (test-all - '((and false true)) - '(false)) - - (test-all - '((or false false 3)) - "or: question result is not true or false") - - (test-all - '((or 1 false false)) - "or: question result is not true or false") - - (test-all - '((or false false false true)) - '(true)) - - (test-all - '((or true false)) - '(true)) - - (test-all - '((or (if false false false) (if false false false) (if true true true) (if false false false))) - '((or false (if false false false) (if true true true) (if false false false))) - '((or false false (if true true true) (if false false false))) - '((or false false true (if false false false))) - '(true)) - - (test-all - '((and (if true true true) (if true true true) (if false false false) (if true true true))) - '((and true (if true true true) (if false false false) (if true true true))) - '((and true true (if false false false) (if true true true))) - '((and true true false (if true true true))) - '(false)) - - (test - '((if 1 2 3)) - "if: question result is not true or false") - - (test - '((if true 'x 'y)) - '('x)) - - (test - '((if false 'x 'y)) - '('y)) - - ; test non-procedure-defs in context: - (test - `((+ 3 4) (define a 3) (+ 5 6)) - `(7 (define a 3) 11)) - - ; test reduction of non-procedure-defs: - (test - `((define a 13) (define b (+ a 9)) (+ 3 4)) - `((define a 13) (define b 22) 7)) - - ; test reduction of unbound ids in hole: - (test - `(x) - "reference to undefined identifier: x") - - ; test reduction of function-bound id in hole: - (test - `((define (a x) (+ x 1)) a) - "a is a procedure, so it must be applied to arguments") - - ; test reduction of non-procedure-def in application: - (test - `((define a 3) (a 9)) - "procedure application: expected procedure, given: 3"))) - - - (define (run-big-test) - (parameterize ([show-dots #t]) - (tests - (test - '((define-struct pr (hd tl)) - (define (avg l) - (cond - [(empty? l) 'infinite] - [else (/ (sum l) (howmany/acc l 0))])) - (define (sum l) - (cond - [(empty? (pr-tl l)) (pr-hd l)] - [else (+ (pr-hd l) (sum (pr-tl l)))])) - (define (howmany/acc l acc) - (cond - [(empty? l) acc] - [else (howmany/acc (pr-tl l) (+ acc 1))])) - (avg empty) - (avg (make-pr 3 (make-pr 4 (make-pr 5 empty))))) - '((define-struct pr (hd tl)) - (define (avg l) - (cond - [(empty? l) 'infinite] - [else (/ (sum l) (howmany/acc l 0))])) - (define (sum l) - (cond - [(empty? (pr-tl l)) (pr-hd l)] - [else (+ (pr-hd l) (sum (pr-tl l)))])) - (define (howmany/acc l acc) - (cond - [(empty? l) acc] - [else (howmany/acc (pr-tl l) (+ acc 1))])) - 'infinite - 4)) - (test - '((define (contains-sym? s l) - (cond - [(empty? l) false] - [true (or (symbol=? s (first l)) - (contains-sym? s (rest l)))])) - (contains-sym? 'x (cons 'z (cons 'y (cons 'x empty)))) - (contains-sym? 'a (cons 'p (cons 'q empty)))) - '((define (contains-sym? s l) - (cond - [(empty? l) false] - [true (or (symbol=? s (first l)) - (contains-sym? s (rest l)))])) - true - false)))))) diff --git a/collects/reduction-semantics/examples/church.ss b/collects/reduction-semantics/examples/church.ss deleted file mode 100644 index 6da6534036..0000000000 --- a/collects/reduction-semantics/examples/church.ss +++ /dev/null @@ -1,63 +0,0 @@ -(module church mzscheme - (require "../reduction-semantics.ss" - "../gui.ss" - "../subst.ss") - - (reduction-steps-cutoff 100) - - (define lang - (language (e (lambda (x) e) - (let (x e) e) - (app e e) - (+ e e) - number - x) - (e-ctxt (lambda (x) e-ctxt) - a-ctxt) - (a-ctxt (let (x a-ctxt) e) - (app a-ctxt e) - (app x a-ctxt) - hole) - (v (lambda (x) e) - x) - (x variable))) - - (define reductions - (list - (reduction/context lang - e-ctxt - (app (lambda (x_1) e_body) e_arg) - (ch-subst (term x_1) (term e_arg) (term e_body))) - (reduction/context lang - e-ctxt - (let (x_1 v_1) e_1) - (ch-subst (term x_1) (term v_1) (term e_1))))) - - (define ch-subst - (subst - [`(let (,x ,v) ,b) - (all-vars (list x)) - (build (lambda (vars v b) `(let (,(car vars) ,v) ,b))) - (subterm '() v) - (subterm (list x) b)] - [`(app ,f ,x) - (all-vars '()) - (build (lambda (vars f x) `(app ,f ,x))) - (subterm '() f) - (subterm '() x)] - [`(lambda (,x) ,b) - (all-vars (list x)) - (build (lambda (vars body) `(lambda (,(car vars)) ,body))) - (subterm (list x) b)] - [(? number?) (constant)] - [(? symbol?) (variable)])) - - - (traces lang reductions - '(let (plus (lambda (m) - (lambda (n) - (lambda (s) - (lambda (z) - (app (app m s) (app (app n s) z))))))) - (let (two (lambda (s) (lambda (z) (app s (app s z))))) - (app (app plus two) two))))) \ No newline at end of file diff --git a/collects/reduction-semantics/examples/combinators.ss b/collects/reduction-semantics/examples/combinators.ss deleted file mode 100644 index 532fec589b..0000000000 --- a/collects/reduction-semantics/examples/combinators.ss +++ /dev/null @@ -1,83 +0,0 @@ -;"one point basis" -;"formal aspects of computing" - -(module combinators mzscheme - (require "../reduction-semantics.ss" - "../gui.ss") - - (initial-font-size 12) - (reduction-steps-cutoff 100) - (initial-char-width 80) - - (define lang - (language - (e (e e) - comb - abs1 - abs2 - abs3) - (e-ctxt (e e-ctxt) - (e-ctxt e) - hole) - (comb i - j - b - c - c* - w))) - - (define ij-reductions - (list - (reduction/context lang - e-ctxt - (i e_1) - (term e_1)) - (reduction/context lang - e-ctxt - ((((j e_a) e_b) e_c) e_d) - (term ((e_a e_b) ((e_a e_d) e_c)))))) - - (define reductions - (append - ij-reductions - (list - (reduction/context lang - e-ctxt - (((b e_m) e_n) e_l) - (term (e_m (e_n e_l)))) - (reduction/context lang - e-ctxt - (((c e_m) e_n) e_l) - (term ((e_m e_l) e_n))) - (reduction/context lang - e-ctxt - ((c* e_a) e_b) - (term (e_b e_a))) - (reduction/context lang - e-ctxt - ((w e_a) e_b) - (term ((e_a e_b) e_b)))))) - - - (define c* `((j i) i)) - (define (make-c c*) `(((j ,c*) (j ,c*)) (j ,c*))) - (define (make-b c) `((,c ((j i) ,c)) (j i))) - (define (make-w b c c*) `(,c ((,c ((,b ,c) ((,c ((,b j) ,c*)) ,c*))) ,c*))) - (define (make-s b c w) `((,b ((,b (,b ,w)) ,c)) (,b ,b))) - - (traces/multiple lang - reductions - (list - `((,c* abs1) abs2) - `(((,(make-c 'c*) abs1) abs2) abs3) - `(((,(make-b 'c) abs1) abs2) abs3) - `((,(make-w 'b 'c 'c*) abs1) abs2) - `(((,(make-s 'b 'c 'w) abs1) abs2) abs3))) - - ;; s in terms of i and j ( > 18,000 reductions and probably still long way to go) - '(traces lang ij-reductions - (make-s (make-b (make-c c*)) - (make-c c*) - (make-w (make-b (make-c c*)) - (make-c c*) - c*)))) diff --git a/collects/reduction-semantics/examples/control.ss b/collects/reduction-semantics/examples/control.ss deleted file mode 100644 index 3b1fddc258..0000000000 --- a/collects/reduction-semantics/examples/control.ss +++ /dev/null @@ -1,81 +0,0 @@ -(module control mzscheme - (require "../reduction-semantics.ss" - "../gui.ss" - "../subst.ss") - - (reduction-steps-cutoff 100) - - (define lang - (language (e (e e) - (\# e) - (f e) - variable - (+ e e) - v) - (c (v c) - (c e) - (\# c) - (f c) - (+ v c) - (+ c e) - hole) - (c# (v c#) - (c# e) - (f c#) - (+ v c#) - (+ c# e) - hole) - (v (lambda (variable) e) - number))) - - (define reductions - (list - (reduction lang - (in-hole c_1 (\# (in-hole c#_1 (f v_1)))) - (term-let ([x (variable-not-in (term c#) 'x)]) - (term - (in-hole c_1 - (v_1 (lambda (x) (in-hole c#_1 x))))))) - (reduction lang - (in-hole c#_1 (f v_1)) - (term-let ([x (variable-not-in (term c#_1) 'x)]) - (term (v_1 (lambda (x) (in-hole c#_1 x)))))) - (reduction/context lang - c - ((lambda (variable_x) e_body) v_arg) - (lc-subst (term variable_x) (term v_arg) (term e_body))) - (reduction/context lang - c - (+ number_1 number_2) - (+ (term number_1) (term number_2))))) - - (define lc-subst - (subst - [`(\# ,e) - (all-vars '()) - (build (lambda (vars body) `(\# ,body))) - (subterm '() e)] - [`(f ,e) - (all-vars '()) - (build (lambda (vars body) `(f ,body))) - (subterm '() e)] - [`(+ ,e1 ,e2) - (all-vars '()) - (build (lambda (vars e1 e2) `(+ ,e1 ,e2))) - (subterm '() e1) - (subterm '() e2)] - [(? symbol?) (variable)] - [(? number?) (constant)] - [`(lambda (,x) ,b) - (all-vars (list x)) - (build (lambda (vars body) `(lambda (,(car vars)) ,body))) - (subterm (list x) b)] - [`(,f ,x) - (all-vars '()) - (build (lambda (vars f x) `(,f ,x))) - (subterm '() f) - (subterm '() x)])) - - (traces/multiple lang reductions - (list '(+ 1 (+ 2 (f (lambda (d) (d (d 0)))))) - '(+ 1 (\# (+ 2 (f (lambda (d) (d (d 0)))))))))) \ No newline at end of file diff --git a/collects/reduction-semantics/examples/eta.ss b/collects/reduction-semantics/examples/eta.ss deleted file mode 100644 index ad62cecc36..0000000000 --- a/collects/reduction-semantics/examples/eta.ss +++ /dev/null @@ -1,72 +0,0 @@ -(module eta mzscheme - (require "../reduction-semantics.ss" - "../gui.ss" - "../subst.ss") - - (reduction-steps-cutoff 100) - - (define lang - (language (e (e e) - x - (+ e e) - v) - (c (v c) - (c e) - (+ v c) - (+ c e) - hole) - (v (lambda (x) e) - number) - (x (variable-except lambda +)))) - - (define reductions - (list - (reduction/context lang - c - ((lambda (variable_x) e_body) v_arg) - (lc-subst (term variable_x) (term v_arg) (term e_body))) - (reduction/context lang - c - (+ number_1 number_2) - (+ (term number_1) (term number_2))) - (reduction/context lang - c - (side-condition (lambda (variable_x) (e_fun variable_x)) - (equal? (term e_fun) (lc-subst (term variable_x) 1234 (term e_fun)))) - (term e_fun)) - - (reduction lang - (in-hole c (number_n v_arg)) - (format "procedure application: expected procedure, given: ~a; arguments were: ~a" - (term number_n) - (term v_arg))) - (reduction lang - (in-hole c (+ (name non-num (lambda (variable) e)) (name arg2 v))) - (format "+: expects type as 1st argument, given: ~s; other arguments were: ~s" - (term non-num) (term arg2))) - (reduction lang - (in-hole c (+ (name arg1 v) (name non-num (lambda (variable) e)))) - (format "+: expects type as 2nd argument, given: ~s; other arguments were: ~s" - (term arg1) (term non-num))))) - - (define lc-subst - (subst - [(? symbol?) (variable)] - [(? number?) (constant)] - [`(lambda (,x) ,b) - (all-vars (list x)) - (build (lambda (vars body) `(lambda (,(car vars)) ,body))) - (subterm (list x) b)] - [`(+ ,n2 ,n1) - (all-vars '()) - (build (lambda (vars n1 n2) `(+ ,n1 ,n1))) - (subterm '() n1) - (subterm '() n2)] - [`(,f ,x) - (all-vars '()) - (build (lambda (vars f x) `(,f ,x))) - (subterm '() f) - (subterm '() x)])) - - - (traces lang reductions '(+ (lambda (x) ((+ 1 2) x)) 1))) \ No newline at end of file diff --git a/collects/reduction-semantics/examples/future.ss b/collects/reduction-semantics/examples/future.ss deleted file mode 100644 index e5cd8435c7..0000000000 --- a/collects/reduction-semantics/examples/future.ss +++ /dev/null @@ -1,123 +0,0 @@ -#| - -This is an adaptation of Cormac Flanagan's future semantics -to a scheme where each term only has a single hole, but -there are multiple decompositions for each term. - -|# - -(module future mzscheme - (require "../reduction-semantics.ss" - "../gui.ss" - "../subst.ss") - - (define lang - (language - (state (flet (variable state) state) - m - error) - (m (let (variable (future m)) m) - (let (variable (car v)) m) - (let (variable (cdr v)) m) - (let (variable (if v m m)) m) - (let (variable (apply v v)) m) - (let (variable v) m) - v) - (v number - variable - (cons v v) - (lambda (variable) m)) - - (e-state (flet (variable e-state) state) - (flet (variable state) e-state) - e) - (e hole - (let (variable e) m) - (let (variable (future e)) m)))) - - (define reductions - (list - (reduction lang - (in-hole (name e e-state) - (let (variable_1 v_val) - m_exp)) - (plug (term e) - (future-subst (term variable_1) (term v_val) (term m_exp)))) - (reduction lang - (in-hole (name e e-state) - (let (variable_1 (car (cons v_val v))) - m_exp)) - (plug (term e) (future-subst (term variable_1) - (term v_val) - (term m_exp)))) - (reduction lang - (in-hole (name e e-state) - (let (variable_1 (cdr (cons v v_val))) - m_exp)) - (plug (term e) (future-subst (term variable_1) - (term v_val) - (term m_exp)))) - (reduction lang - (in-hole (name e e-state) - (let (variable_1 (if true m_then m)) - m_exp)) - (plug (term e) (term (let (variable_1 m_then) m_exp)))) - (reduction lang - (in-hole (name e e-state) - (let (variable_1 (if false m m_else)) - m_exp)) - (plug (term e) (term (let (variable_1 m_else) m_exp)))) - (reduction lang - (in-hole (name e e-state) - (let (variable_1 - (apply (lambda (variable_formal) m_body) - v_actual)) - m_exp)) - (plug - (term e) - (term (let (variable_1 ,(future-subst (term variable_formal) (term v_actual) (term m_body))) - m_exp)))) - (reduction lang - (in-hole (name e e-state) - (let (variable_x (future m_1)) m_2)) - (let ([p (variable-not-in (list (term e) (term m_1) (term m_2)) 'p)]) - (term (flet (,p m_1) (let (variable_x ,p) m_2))))) - (reduction lang - (flet (variable_p v_1) state_body) - (future-subst (term variable_p) (term v_1) (term state_body))) - (reduction lang - (flet (variable_2 (flet (variable_1 state_1) state_2)) - state_3) - (term (flet (variable_1 state_1) (flet (variable_2 state_2) state_3)))))) - - (define future-subst - (subst - [`(let (,a-var ,rhs-exp) ,body-exp) - (all-vars (list a-var)) - (build (lambda (vars rhs-exp body-exp) `(let (,(car vars) ,rhs-exp) ,body-exp))) - (subterm '() rhs-exp) - (subterm (list a-var) body-exp)] - [`(lambda (,a-var) ,exp) - (all-vars (list a-var)) - (build (lambda (vars body) `(lambda (,(car vars)) ,body))) - (subterm (list a-var) exp)] - [(? number?) (constant)] - [(? symbol?) (variable)] - [`(cons ,hd ,tl) - (all-vars '()) - (build (lambda (vars hd tl) `(cons ,hd ,tl))) - (subterm '() hd) - (subterm '() tl)])) - - (define (copy-sexp x) (if (pair? x) (cons (copy-sexp (car x)) (copy-sexp (cdr x))) x)) - - '(traces lang reductions '(let (x (future (let (y (cons 1 2)) - (let (z (car y)) - z)))) - (let (p (cons 3 4)) - (let (q (car p)) - (cons x q))))) - - (traces lang reductions '(let (x (future (let (y 1) - y))) - x))) \ No newline at end of file diff --git a/collects/reduction-semantics/examples/ho-contracts.ss b/collects/reduction-semantics/examples/ho-contracts.ss deleted file mode 100644 index ca8df25827..0000000000 --- a/collects/reduction-semantics/examples/ho-contracts.ss +++ /dev/null @@ -1,567 +0,0 @@ - -(module ho-contracts mzscheme - (require "../reduction-semantics.ss" - "../gui.ss" - "../subst.ss" - (lib "mred.ss" "mred") - (lib "framework.ss" "framework") - (lib "class.ss") - (lib "match.ss") - (lib "list.ss")) - - (initial-font-size 7) (reduction-steps-cutoff 10) - ;(initial-font-size 36) (reduction-steps-cutoff 1) - - (define lang - (language - (p ((d ...) e)) - (d (valrec x : e = e)) - (e (lambda (x) e) - (e e) - (let ((x e) ...) e) - x - (fix x e) - number - (aop e e) - (rop e e) - (cons e e) - empty - (hd e) - (tl e) - (mt e) - (if e e e) - true - false - string - (--> e e) - (contract e) - (flatp e) - (pred e) - (dom e) - (rng e) - (blame e)) - (x (variable-except valrec lambda let fix aop rop cons empty hd tl mt if true false --> contract flatp pred dom rng blame)) - - (p-ctxt (((valrec x : v = v) ... - (valrec x : e-ctxt = e) - d ...) - e) - (((valrec x : v = v) ... - (valrec x : v = e-ctxt) - d ...) - e) - (((valrec x : v = v) ...) - e-ctxt)) - (e-ctxt (e-ctxt e) - (v e-ctxt) - (let ((x v) ... (x e-ctxt) (x e) ...) e) - (aop e-ctxt e) - (aop v e-ctxt) - (rop e-ctxt e) - (rop v e-ctxt) - (cons e-ctxt e) - (cons v e-ctxt) - (hd e-ctxt) - (tl e-ctxt) - (mt e-ctxt) - (if e-ctxt e e) - (--> v e-ctxt) - (--> e-ctxt e) - (contract e-ctxt) - (flatp e-ctxt) - (pred e-ctxt) - (dom e-ctxt) - (rng e-ctxt) - (blame e-ctxt) - hole) - (v (cons v v) - (lambda (x) e) - string - number - true - false - (--> v v) - (contract v) - (ob v (--> v v) x x) - compile-v1 - compile-v2) - - (aop + - * /) - (rop = >=))) - - (define ho-contracts-subst - (subst - [`(let ([,a-vars ,rhs-exps] ...) ,body) - (all-vars a-vars) - (build (lambda (vars body . rhss) - `(let (,@(map (lambda (var rhs) `[,var ,rhs]) vars rhss)) - ,body))) - (subterm a-vars body) - (subterms '() rhs-exps)] - [`(lambda (,var) ,body) - (all-vars (list var)) - (build (lambda (vars body) `(lambda (,(car vars)) ,body))) - (subterm (list var) body)] - [`(fix ,variable ,e) - (all-vars (list variable)) - (build (lambda (vars body) `(fix ,(car vars) ,body))) - (subterm (list variable) e)] - [(? number?) (constant)] - [`(,(and op (? (lambda (x) (memq x '(cons + - = > / -->))))) ,e1 ,e2) - (all-vars '()) - (build (lambda (vars e1 e2) `(,op ,e1 ,e2))) - (subterm '() e1) - (subterm '() e2)] - [`empty (constant)] - [`(,(and op (? (lambda (x) (memq x '(hd tl mt contract flat pred dom rng blame))))) ,e1) - (all-vars '()) - (build (lambda (vars e1) `(,op ,e1))) - (subterm '() e1)] - [`(if ,e1 ,e2 ,e3) - (all-vars '()) - (build (lambda (vars e1 e2 e3) `(if ,e1 ,e2 ,e3))) - (subterm '() e1) - (subterm '() e2) - (subterm '() e3)] - [`(,e1 ,e2) - (all-vars '()) - (build (lambda (vars e1 e2) `(,e1 ,e2))) - (subterm '() e1) - (subterm '() e2)] - [`true (constant)] - [`false (constant)] - [(? string?) (constant)] - [(? symbol?) (variable)])) - - (define reductions - (list - (reduction lang - (in-hole (name p p-ctxt) (/ number_n number_m)) - (if (= (term number_m) 0) - (term (error /)) - (plug (term p) (/ (term number_n) (term number_m))))) - (reduction lang - (in-hole (name p p-ctxt) (* number_n number_m)) - (plug (term p) (* (term number_n) (term number_m)))) - (reduction lang - (in-hole (name p p-ctxt) (+ number_n number_m)) - (plug (term p) (+ (term number_n) (term number_m)))) - (reduction lang - (in-hole (name p p-ctxt) (- number_n number_m)) - (plug (term p) (- (term number_n) (term number_m)))) - (reduction lang - (in-hole (name p p-ctxt) (>= number_n number_m)) - (plug (term p) (if (>= (term number_n) (term number_m)) 'true 'false))) - (reduction lang - (in-hole (name p p-ctxt) (= number_n number_m)) - (plug (term p) (if (= (term number_n) (term number_m)) 'true 'false))) - (reduction lang - (in-hole (name p p-ctxt) ((lambda (variable_x) e_body) v_arg)) - (plug (term p) (ho-contracts-subst (term variable_x) - (term v_arg) - (term e_body)))) - (reduction lang - (in-hole (name p p-ctxt) - (let ((variable_i v_i) ...) e_body)) - (plug (term p) - (foldl - ho-contracts-subst - (term e_body) - (term (variable_i ...)) - (term (v_i ...))))) - (reduction lang - (in-hole (name p p-ctxt) (name tot (fix (name x variable) (name body e)))) - (plug (term p) (ho-contracts-subst (term x) (term tot) (term body)))) - (reduction lang - ((name defns - ((valrec (name bvar variable) : (name bctc value) = (name brhs value)) ... - (valrec (name var variable) : value = (name rhs value)) - (valrec variable : value = value) ...)) - (in-hole (name p e-ctxt) (name var variable))) - (term (defns ,(plug (term p) (term rhs))))) - (reduction lang - (in-hole (name p p-ctxt) (if true e_then e)) - (plug (term p) (term e_then))) - (reduction lang - (in-hole (name p p-ctxt) (if false e e_else)) - (plug (term p) (term e_else))) - (reduction lang - (in-hole (name p p-ctxt) (hd (cons v_fst v))) - (plug (term p) (term v_fst))) - (reduction lang - (in-hole (name p p-ctxt) (hd empty)) - (term (error hd))) - (reduction lang - (in-hole (name p p-ctxt) (tl (cons v v_rst))) - (plug (term p) (term v_rst))) - (reduction lang - (in-hole (name p p-ctxt) (tl empty)) - (term (error tl))) - (reduction lang - (in-hole (name p p-ctxt) (mt empty)) - (plug (term p) 'true)) - (reduction lang - (in-hole (name p p-ctxt) (mt (cons v v))) - (plug (term p) 'false)) - (reduction lang - (in-hole (name p p-ctxt) (flatp (contract v))) - (plug (term p) 'true)) - (reduction lang - (in-hole (name p p-ctxt) (flatp (--> v v))) - (plug (term p) 'false)) - (reduction lang - (in-hole (name p p-ctxt) (pred (contract v_pred))) - (plug (term p) (term v_pred))) - (reduction lang - (in-hole (name p p-ctxt) (pred (--> v v))) - (term (error pred))) - (reduction lang - (in-hole (name p p-ctxt) (dom (--> v_dm v))) - (plug (term p) (term v_dm))) - (reduction lang - (in-hole (name p p-ctxt) (dom (contract v))) - (term (error dom))) - (reduction lang - (in-hole (name p p-ctxt) (rng (--> v v_rg))) - (plug (term p) (term v_rg))) - (reduction lang - (in-hole (name p p-ctxt) (rng (contract v))) - (term (error rng))) - (reduction lang - (in-hole (name p p-ctxt) (blame (name x variable))) - (term (error x))))) - - (define (pp v port w spec) - (parameterize ([current-output-port port]) - (pp-prog v spec))) - - (define (pp-prog prog spec) - (for-each (lambda (x) (pp-defn x spec)) (car prog)) - (pp-expr (cadr prog) 0 spec) - (display "\n")) - - (define (pp-defn defn spec) - (let ([var (second defn)] - [ctc (fourth defn)] - [exp (sixth defn)]) - (printf "val rec ") - (display var) - (display " : ") - (pp-expr ctc 0 spec) - (display " = ") - (pp-expr exp 0 spec) - (display "\n"))) - - (define (dp/ct x) - (let* ([str (format "~a" x)] - [ct (string-length str)]) - (display str) - ct)) - - ;; pp-expr : sexp number (snip -> void) -> (union #f number) - ;; returns #f if it started a new line and a - ;; number if it didn't. The number indicates - ;; how many columns were printed - (define (pp-expr x nl-col text) - (cond - [(equal? x wrapbar) - (insert-wrapbar text)] - [else - (match x - [`(lambda (,v) ,e) - (insert-lambda text) - (insert-variable text v) - (dp/ct ". ") - (next-line (+ nl-col 2)) - (pp-expr e (+ nl-col 2) text) - #f] - [`(let ((,vs ,rhss) ...) ,body) - (insert-bold text "let") - (dp/ct " ") - (insert-variable text (car vs)) - (dp/ct " = ") - (pp-expr (car rhss) (+ nl-col (string-length (format "let "))) text) - (for-each (lambda (v rhs) - (next-line (+ nl-col (string-length (format "let ")))) - (insert-variable text v) - (dp/ct " = ") - (pp-expr rhs (+ nl-col (string-length (format "let "))) text)) - (cdr vs) - (cdr rhss)) - (next-line (+ nl-col 2)) - (pp-expr body (+ nl-col 2) text) - #f] - [`(fix ,v ,e) - (insert-bold text "fix") - (dp/ct " ") - (dp/ct v) - (dp/ct ". ") - (next-line (+ nl-col 2)) - (pp-expr e (+ nl-col 2) text) - #f] - [`(if ,e1 ,e2 ,e3) - (insert-bold text "if") - (dp/ct " ") - (pp-expr e1 (+ nl-col 3) text) - (next-line (+ nl-col 2)) - (insert-bold text "then") - (dp/ct " ") - (pp-expr e2 (+ nl-col 2 5) text) - (next-line (+ nl-col 2)) - (insert-bold text "else") - (dp/ct " ") - (pp-expr e3 (+ nl-col 2 5) text) - #f] - [`(,e1 ,e2) - (let* ([fst-res - (cond - [(simple? e1) - (pp-expr e1 nl-col text)] - [else - (comb (dp/ct "(") - (pp-expr e1 (+ nl-col 1) text) - (dp/ct ")"))])] - [break-lines? - (or (not fst-res) - (>= fst-res 10))] - [_ (when break-lines? - (next-line nl-col))] - [snd-res - (cond - [(simple? e2) - (comb - (dp/ct " ") - (pp-expr e2 - (if break-lines? - (+ nl-col 1) - (+ fst-res nl-col 1)) - text))] - [else - (comb (dp/ct " (") - (pp-expr e2 - (if break-lines? - (+ nl-col 2) - (+ nl-col fst-res 2)) - text) - (dp/ct ")"))])]) - (comb - fst-res - snd-res))] - [`(,biop ,e1 ,e2) - (let* ([fst-res - (cond - [(simple? e1) - (pp-expr e1 nl-col text)] - [else - (comb - (dp/ct "(") - (pp-expr e1 (+ nl-col 1) text) - (dp/ct ")"))])] - [spc1 (if fst-res - (dp/ct " ") - (begin (next-line nl-col) - #f))] - [middle - (case biop - [(cons) (dp/ct "::")] - [(-->) - (insert-symbol text (string (integer->char 174))) - 1] - [else (dp/ct biop)])] - [spc2 (if fst-res - (dp/ct " ") - (begin (next-line nl-col) - #f))] - [snd-res - (cond - [(simple? e2) - (pp-expr e2 - (if fst-res - (+ nl-col fst-res spc1 middle spc2) - nl-col) - text)] - [else - (comb - (dp/ct "(") - (pp-expr e2 - (if fst-res - (+ nl-col fst-res spc1 middle spc2 1) - (+ nl-col 1)) - text) - (dp/ct ")"))])]) - (comb fst-res - spc1 - middle - spc2 - snd-res))] - [`compile-v1 - (insert-compile text "V" "1")] - [`compile-v2 - (insert-compile text "V" "2")] - [`compile-e - (insert-compile text "e" #f)] - [`empty - (dp/ct "[]")] - [(? (lambda (x) - (and (symbol? x) - (memq x keywords)))) - (insert-bold text (symbol->string x))] - [(? symbol?) - (insert-variable text x)] - [else - (dp/ct (format "~s" x))])])) - - (define keywords '(contract pred dom rng flatp error blame true false)) - - (define (insert-lambda text) - (insert-symbol text "l ")) - - (define (insert-compile text arg subscript) - (let ([sd (make-object style-delta% 'change-family 'script)] - [b-sd (make-object style-delta% 'change-family 'script)]) - (send b-sd set-delta 'change-bold) - (+ (insert/style text "C" b-sd) - (insert/snip text (make-object sub-snip% "e")) - (insert/style text "(" sd) - (insert/style text arg #f) - (if subscript - (insert/snip text (make-object sub-snip% subscript)) - 0) - (insert/style text ")" sd)))) - - (define (insert-wrapbar text) - (send text insert (make-object wrap-bar%) - (send text last-position) - (send text last-position)) - 4) - - (define (insert-symbol text str) - (insert/style text str (make-object style-delta% 'change-family 'symbol))) - - (define (insert-bold text str) - (insert/style text str (make-object style-delta% 'change-bold)) - (string-length str)) - - (define (insert-variable text sym) - (let ([d (make-object style-delta%)] - [str (symbol->string sym)]) - (send d set-delta-foreground "forest green") - (insert/style text str d) - (string-length str))) - - (define wrap-bar% - (class snip% - (inherit get-style) - (define/override (get-extent dc x y wb hb db ab lspace rspace) - (set-box/f lspace 0) - (set-box/f rspace 0) - (let-values ([(w h d a) (send dc get-text-extent "wrap" - (send (get-style) get-font))]) - (set-box/f wb w) - (set-box/f hb h) - (set-box/f db d) - (set-box/f ab a))) - - (define/override (draw dc x y left top right bottom dx dy draw-caret?) - (let-values ([(w h d a) (send dc get-text-extent "wrap")]) - (send dc draw-text "wrap" x y) - (send dc draw-line x (+ y 1) (+ x w -1) (+ y 1)))) - - (super-instantiate ()))) - - (define sub-snip% - (class snip% - (init-field str) - (inherit get-style) - (define/override (get-extent dc x y wb hb db ab lspace rspace) - (set-box/f lspace 0) - (set-box/f rspace 0) - (let-values ([(w h d a) (send dc get-text-extent str - (send (get-style) get-font))]) - (set-box/f wb w) - (set-box/f hb (+ h (floor (/ h 3)))) - (set-box/f db (- (+ h (floor (/ h 3))) - (- h d))) - (set-box/f ab a))) - - (define/override (draw dc x y left top right bottom dx dy draw-caret?) - (let-values ([(w h d a) (send dc get-text-extent str)]) - (send dc draw-text str x (+ y (floor (/ h 3)))))) - - (super-instantiate ()))) - - (define (set-box/f b v) (when (box? b) (set-box! b v))) - - ;; insert/snip : text snip -> number - ;; returns an approximation to the width of what was inserted - (define (insert/snip text snip) - (send text insert snip (send text last-position) (send text last-position)) - 1) - - ;; insert/style : text string style-delta% -> number - ;; returns the number of characters in the string - ;; (an approximation to the width of what was inserted) - (define (insert/style text str sd) - (let ([pos (send text last-position)]) - (send text insert str pos pos) - (when sd - (send text change-style - sd - pos - (send text last-position))) - (string-length str))) - - ;; comb : (union #f number) *-> (union #f number) - ;; sums up its arguments, unless it gets #f, - ;; in which case it returns #f - (define (comb . x) - (if (memq #f x) - #f - (apply + x))) - - ;; simple : any -> bool - ;; determines if an expression need parenthesis - (define (simple? exp) - (or (not (pair? exp)) - (equal? exp wrapbar))) - - ;; next-line : number -> void - ;; dp/cts a newline and indents to the proper place - (define (next-line n) - (dp/ct "\n") - (let loop ([n n]) - (unless (zero? n) - (dp/ct " ") - (loop (- n 1))))) - - (define wrapbar - `(fix - wrap - (lambda (ct) - (lambda (x) - (lambda (p) - (lambda (n) - (if (flatp ct) - (if ((pred ct) x) - x - (blame p)) - (let ((d (dom ct)) - (r (rng ct))) - (lambda (y) - ((((wrap r) - (x ((((wrap d) y) n) p))) - p) - n)))))))))) - - (define flat-case - `(();; defns... - ((((,wrapbar (contract compile-v2)) compile-v1) "p") "n"))) - - (define ho-case - `(();; defns... - ((((,wrapbar (--> compile-v1 compile-v2)) (lambda (x) compile-e)) "p") "n"))) - - - (traces lang reductions flat-case pp) - (traces lang reductions ho-case pp) - ) diff --git a/collects/reduction-semantics/examples/info.ss b/collects/reduction-semantics/examples/info.ss deleted file mode 100644 index 8e947b6c8e..0000000000 --- a/collects/reduction-semantics/examples/info.ss +++ /dev/null @@ -1,2 +0,0 @@ -(module info (lib "infotab.ss" "setup") - (define name "Reduction Semantics examples")) diff --git a/collects/reduction-semantics/examples/iswim.ss b/collects/reduction-semantics/examples/iswim.ss deleted file mode 100644 index e24bdc45fe..0000000000 --- a/collects/reduction-semantics/examples/iswim.ss +++ /dev/null @@ -1,255 +0,0 @@ -(module iswim mzscheme - (require (lib "reduction-semantics.ss" "reduction-semantics") - (lib "subst.ss" "reduction-semantics") - (lib "contract.ss")) - - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - ;; Expression grammar: - - (define iswim-grammar - (language (M (M M) - (o1 M) - (o2 M M) - V - ("letcc" X M) - ("cc" M M)) - (V X - ("lam" variable M) - b - ("[" M "]")) - (X variable) - (b number) - (o1 "add1" "sub1" "iszero") - (o2 "+" "-" "*" "^") - (on o1 o2) - - ;; Evaluation contexts: - (E hole - (E M) - (V E) - (o1 E) - (o2 E M) - (o2 V E) - ("cc" E M) - ("cc" V E)) - - ;; Continuations (CK machine): - (k "mt" - ("fun" V k) - ("arg" M k) - ("narg" (V ... on) (M ...) k)) - - ;; Environments and closures (CEK): - (env ((X = vcl) ...)) - (cl (M : env)) - (vcl (V- : env)) - - ;; Values that are not variables: - (V- ("lam" variable M) - b) - - ;; Continuations with closures (CEK): - (k- "mt" - ("fun" vcl k-) - ("arg" cl k-) - ("narg" (vcl ... on) (cl ...) k-)))) - - (define M? (language->predicate iswim-grammar 'M)) - (define V? (language->predicate iswim-grammar 'V)) - (define o1? (language->predicate iswim-grammar 'o1)) - (define o2? (language->predicate iswim-grammar 'o2)) - (define on? (language->predicate iswim-grammar 'on)) - (define k? (language->predicate iswim-grammar 'k)) - - (define env? (language->predicate iswim-grammar 'env)) - (define cl? (language->predicate iswim-grammar 'cl)) - (define vcl? (language->predicate iswim-grammar 'vcl)) - (define k-? (language->predicate iswim-grammar 'k-)) - - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - ;; Substitution: - - ;; The subst form makes implemention of capture-avoiding - ;; easier. We just have to describe how variables bind - ;; in our language's forms. - - (define iswim-subst/backwards - (subst - [(? symbol?) (variable)] - [(? number?) (constant)] - [`("lam" ,X ,M) - (all-vars (list X)) - (build (lambda (X-list M) `("lam" ,(car X-list) ,M))) - (subterm (list X) M)] - [`(,(and o (or "add1" "sub1" "iszero")) ,M1) - (all-vars '()) - (build (lambda (vars M1) `(,o ,M1))) - (subterm '() M1)] - [`(,(and o (or "+" "-" "*" "^")) ,M1 ,M2) - (all-vars '()) - (build (lambda (vars M1 M2) `(,o ,M1 ,M2))) - (subterm '() M1) - (subterm '() M2)] - [`(,M1 ,M2) - (all-vars '()) - (build (lambda (empty-list M1 M2) `(,M1 ,M2))) - (subterm '() M1) - (subterm '() M2)] - [`("letcc" ,X ,M) - (all-vars (list X)) - (build (lambda (X-list M) `("letcc" ,(car X-list) ,M))) - (subterm (list X) M)] - [`("cc" ,M1 ,M2) - (all-vars '()) - (build (lambda (vars M1 M2) `("cc" ,M1 ,M2))) - (subterm '() M1) - (subterm '() M2)] - [`("[" ,E "]") - (all-vars '()) - (build (lambda (vars) `("[" ,E "]")))])) - - - ;; the argument order for the subst-generated function - ;; doesn't match the order in the notes: - (define (iswim-subst M Xr Mr) - (iswim-subst/backwards Xr Mr M)) - - (define empty-env '()) - - ;; Environment lookup - (define (env-lookup env X) - (let ([m (assq X env)]) - (and m (caddr m)))) - - ;; Environment extension - (define (env-extend env X vcl) - (cons (list X '= vcl) env)) - - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - ;; Reductions: - - ;; beta_v reduction - (define beta_v - (reduction iswim-grammar - (("lam" X_1 M_1) V_1) - (iswim-subst (term M_1) (term X_1) (term V_1)))) - - - (define delta - (list - (reduction iswim-grammar ("add1" b_1) (add1 (term b_1))) - (reduction iswim-grammar ("sub1" b_1) (sub1 (term b_1))) - (reduction iswim-grammar ("iszero" b_1) - (if (zero? (term b_1)) - '("lam" x ("lam" y x)) - '("lam" x ("lam" y y)))) - (reduction iswim-grammar ("+" b_1 b_2) (+ (term b_1) (term b_2))) - (reduction iswim-grammar ("-" b_1 b_2) (- (term b_1) (term b_2))) - (reduction iswim-grammar ("*" b_1 b_2) (* (term b_1) (term b_2))) - (reduction iswim-grammar ("^" b_1 b_2) (expt (term b_1) (term b_2))))) - - ;; ->v - (define ->v (map (lambda (red) - (compatible-closure red iswim-grammar 'M)) - (cons beta_v delta))) - - ;; :->v - (define :->v (map (lambda (red) - (context-closure red iswim-grammar 'E)) - (cons beta_v delta))) - - ;; :->v+letcc - (define :->v+letcc (append - :->v - (list - - ;; letcc rule: - (reduction - iswim-grammar - (in-hole E_1 ("letcc" X_1 M_1)) - (plug (term E_1) - (iswim-subst (term M_1) (term X_1) `("[" - ,(plug (term E_1) '||) - "]")))) - - ;; cc rule: - (reduction - iswim-grammar - (in-hole E ("cc" ("[" (in-hole E_2 ||) "]") V_1)) - (plug (term E_2) (term V_1)))))) - - - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - ;; Helpers: - - (define (delta*n on Vs) - (let ([l (reduce delta `(,on ,@Vs))]) - (if (null? l) - #f - (car l)))) - - (define (delta*1 o1 V) - (delta*n o1 (list V))) - - (define (delta*2 o2 V1 V2) - (delta*n o2 (list V1 V2))) - - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - ;; Abbreviations: - - (define (if0 test then else) - (let ([X (variable-not-in `(,then ,else) 'X)]) - `(((("iszero" ,test) ("lam" ,X ,then)) ("lam" ,X ,else)) 77))) - - (define true '("lam" x ("lam" y x))) - (define false '("lam" x ("lam" y y))) - (define boolean-not `("lam" x ((x ,false) ,true))) - - (define mkpair '("lam" x ("lam" y ("lam" s ((s x) y))))) - (define fst '("lam" p (p ("lam" x ("lam" y x))))) - (define snd '("lam" p (p ("lam" x ("lam" y y))))) - - (define Y_v '("lam" f ("lam" x - ((("lam" g (f ("lam" x ((g g) x)))) - ("lam" g (f ("lam" x ((g g) x))))) - x)))) - - (define mksum `("lam" s - ("lam" x - ,(if0 'x 0 '("+" x (s ("sub1" x))))))) - (define sum `(,Y_v ,mksum)) - - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - ;; Exports: - - (provide/contract (iswim-grammar compiled-lang?) - (M? (any/c . -> . boolean?)) - (V? (any/c . -> . boolean?)) - (o1? (any/c . -> . boolean?)) - (o2? (any/c . -> . boolean?)) - (on? (any/c . -> . boolean?)) - (k? (any/c . -> . boolean?)) - (env? (any/c . -> . boolean?)) - (cl? (any/c . -> . boolean?)) - (vcl? (any/c . -> . boolean?)) - (iswim-subst (M? symbol? M? . -> . M?)) - (env-lookup (env? symbol? . -> . (union false/c vcl?))) - (env-extend (env? symbol? vcl? . -> . env?)) - (empty-env env?) - (beta_v red?) - (delta (listof red?)) - (delta*1 (o1? V? . -> . (union false/c V?))) - (delta*2 (o2? V? V? . -> . (union false/c V?))) - (delta*n (on? (listof V?) . -> . (union false/c V?))) - (->v (listof red?)) - (:->v (listof red?)) - (:->v+letcc (listof red?)) - (if0 (M? M? M? . -> . M?)) - (true M?) - (false M?) - (boolean-not M?) - (mkpair M?) - (fst M?) - (snd M?) - (Y_v M?) - (sum M?))) diff --git a/collects/reduction-semantics/examples/macro.ss b/collects/reduction-semantics/examples/macro.ss deleted file mode 100644 index 588c4ebcff..0000000000 --- a/collects/reduction-semantics/examples/macro.ss +++ /dev/null @@ -1,47 +0,0 @@ -(module macro mzscheme - (require "../reduction-semantics.ss" - "../gui.ss") - - (define lang - (language - (e (lambda (variable) e) - (app e e) - number - variable) - (e-ctxt (lambda (variable) e-ctxt) - (app e-ctxt any) - (app e e-ctxt) - hole))) - - (define macros '(or let if true false id)) - - (define-syntax (--> stx) - (syntax-case stx () - [(_ frm to) - (syntax (reduction/context lang e-ctxt frm to))])) - - (define reductions - (list - (--> (id (name e any)) - (term e)) - (--> (side-condition ((name e1 any) (name e2 any)) - (not (memq (term e1) macros))) - (term (app e1 e2))) - (--> (or (name e1 any) (name e2 any)) - (let ([var (variable-not-in (list (term e1) (term e2)) 'x)]) - (term (let (,var e1) (if ,var ,var e2))))) - (--> (let ((name var variable) (name rhs any)) - (name body any)) - (term ((lambda (var) body) rhs))) - (--> (if (name test any) - (name thn any) - (name els any)) - (term ((test thn) els))) - (--> (true) - (term (lambda (x) (lambda (y) x)))) - (--> (false) - (term (lambda (x) (lambda (y) y)))))) - - (traces lang reductions '((id id) 5)) - (traces lang reductions '(id 5)) - (traces lang reductions '(or (false) (true)))) diff --git a/collects/reduction-semantics/examples/omega.ss b/collects/reduction-semantics/examples/omega.ss deleted file mode 100644 index ccad3526f3..0000000000 --- a/collects/reduction-semantics/examples/omega.ss +++ /dev/null @@ -1,64 +0,0 @@ -(module omega mzscheme - (require "../reduction-semantics.ss" - "../gui.ss" - "../subst.ss") - - (reduction-steps-cutoff 10) - - (define lang - (language (e (e e) - (abort e) - x - v) - (c (v c) - (c e) - hole) - (v call/cc - number - (lambda (x) e)) - - (x (variable-except lambda call/cc abort)) - )) - - (define reductions - (list - (reduction lang - (in-hole c_1 (call/cc v_arg)) - (term-let ([v (variable-not-in (term c_1) 'x)]) - (term (in-hole c_1 (v_arg (lambda (v) (abort (in-hole c_1 v)))))))) - (reduction lang - (in-hole c (abort e_1)) - (term e_1)) - - (reduction/context lang - c - ((lambda (variable_x) e_body) v_arg) - (lc-subst (term variable_x) (term v_arg) (term e_body))))) - - (define lc-subst - (plt-subst - ['abort (constant)] - ['call/cc (constant)] - [(? symbol?) (variable)] - [(? number?) (constant)] - [`(lambda (,x) ,b) - (all-vars (list x)) - (build (lambda (vars body) `(lambda (,(car vars)) ,body))) - (subterm (list x) b)] - [`(call/cc ,v) - (all-vars '()) - (build (lambda (vars arg) `(call/cc ,arg))) - (subterm '() v)] - [`(,f ,x) - (all-vars '()) - (build (lambda (vars f x) `(,f ,x))) - (subterm '() f) - (subterm '() x)])) - - - ;(traces lang reductions '((lambda (x) (x x)) (lambda (x) (x x)))) - - ;(traces lang reductions '((call/cc call/cc) (call/cc call/cc))) - (traces lang reductions '((lambda (x) ((call/cc call/cc) x)) (call/cc call/cc))) - - ) diff --git a/collects/reduction-semantics/examples/semaphores.ss b/collects/reduction-semantics/examples/semaphores.ss deleted file mode 100644 index 39ab1ce246..0000000000 --- a/collects/reduction-semantics/examples/semaphores.ss +++ /dev/null @@ -1,190 +0,0 @@ -#| - -semaphores make things much more predictable... - -|# - -(module semaphores mzscheme - (require "../reduction-semantics.ss" - "../gui.ss") - - (reduction-steps-cutoff 100) - - (define lang - (language - (p ((store (variable v) ...) - (semas (variable sema-count) ...) - (threads e ...))) - (sema-count number - none) - (e (set! variable e) - (begin e ...) - (semaphore variable) - (semaphore-wait e) - (semaphore-post e) - (lambda (variable) e) - (e e) - variable - (list e ...) - (cons e e) - number - (void)) - (p-ctxt ((store (variable v) ...) - (semas (variable sema-count) ...) - (threads e ... e-ctxt e ...))) - (e-ctxt (e-ctxt e) - (v e-ctxt) - (cons e-ctxt e) - (cons v e-ctxt) - (list v ... e-ctxt e ...) - (set! variable e-ctxt) - (begin e-ctxt e ...) - (semaphore-wait e-ctxt) - (semaphore-post e-ctxt) - hole) - (v (semaphore variable) - (lambda (variable) e) - (list v ...) - number - (void)))) - - (define reductions - (list - (reduction lang - (in-hole (name c p-ctxt) (begin v e_1 e_2 e_rest ...)) - (plug - (term c) - (term (begin e_1 e_2 e_rest ...)))) - (reduction lang - (in-hole (name c p-ctxt) - (cons v_1 (list v_2s ...))) - (plug - (term c) - (term (list v_1 v_2s ...)))) - (reduction lang - (in-hole (name c p-ctxt) (begin v e_1)) - (plug (term c) (term e_1))) - (reduction lang - (in-hole (name c p-ctxt) (begin v_1)) - (plug (term c) (term v_1))) - (reduction lang - ((store - (name befores (variable v)) ... - ((name x variable) (name v v)) - (name afters (variable v)) ...) - (name semas any) - (threads - (name e-before e) ... - (in-hole (name c e-ctxt) (name x variable)) - (name e-after e) ...)) - (term - ((store - befores ... - (x v) - afters ...) - semas - (threads - e-before ... - (in-hole c v) - e-after ...)))) - (reduction lang - ((store - (name befores (variable v)) ... - (variable_i v) - (name afters (variable v)) ...) - (name semas any) - (threads - (name e-before e) ... - (in-hole (name c e-ctxt) (set! variable_i v_new)) - (name e-after e) ...)) - (term - ((store - befores ... - (variable_i v_new) - afters ...) - semas - (threads - e-before ... - (in-hole c (void)) - e-after ...)))) - (reduction lang - ((name store any) - (semas - (name befores (variable v)) ... - (variable_sema number_n) - (name afters (variable v)) ...) - (threads - (name e-before e) ... - (in-hole (name c e-ctxt) (semaphore-wait (semaphore variable_sema))) - (name e-after e) ...)) - (term - (store - (semas - befores ... - (variable_sema ,(if (= (term number_n) 1) - (term none) - (- (term number_n) 1))) - afters ...) - (threads - e-before ... - (in-hole c (void)) - e-after ...)))) - (reduction lang - ((name store any) - (semas - (name befores (variable v)) ... - (variable_sema number_n) - (name afters (variable v)) ...) - (threads - (name e-before e) ... - (in-hole (name c e-ctxt) (semaphore-post (semaphore variable_sema))) - (name e-after e) ...)) - (term - (store - (semas - befores ... - (variable_sema ,(+ (term number_n) 1)) - afters ...) - (threads - e-before ... - (in-hole c (void)) - e-after ...)))) - - (reduction lang - ((name store any) - (semas - (name befores (variable v)) ... - (variable_sema none) - (name afters (variable v)) ...) - (threads - (name e-before e) ... - (in-hole (name c e-ctxt) (semaphore-post (semaphore variable_sema))) - (name e-after e) ...)) - (term - (store - (semas - befores ... - (variable_sema 1) - afters ...) - (threads - e-before ... - (in-hole c (void)) - e-after ...)))))) - - (traces lang - reductions - `((store (y (list))) - (semas) - (threads (set! y (cons 1 y)) - (set! y (cons 2 y))))) - - (traces lang - reductions - `((store (y (list))) - (semas (x 1)) - (threads (begin (semaphore-wait (semaphore x)) - (set! y (cons 1 y)) - (semaphore-post (semaphore x))) - (begin (semaphore-wait (semaphore x)) - (set! y (cons 2 y)) - (semaphore-post (semaphore x))))))) diff --git a/collects/reduction-semantics/examples/subject-reduction.ss b/collects/reduction-semantics/examples/subject-reduction.ss deleted file mode 100644 index cf4f30a239..0000000000 --- a/collects/reduction-semantics/examples/subject-reduction.ss +++ /dev/null @@ -1,96 +0,0 @@ -(module subject-reduction mzscheme - (require "../reduction-semantics.ss" - "../gui.ss" - "../subst.ss" - (lib "plt-match.ss")) - - (reduction-steps-cutoff 10) - - (define lang - (language (e (e e) - (abort e) - x - v) - (x (variable-except lambda call/cc abort)) - (c (v c) - (c e) - hole) - (v call/cc - number - (lambda (x t) e)) - (t num - (t -> t)))) - - (define reductions - (list - (reduction lang - (in-hole c_1 (call/cc v_arg)) - (let ([v (variable-not-in (term c_1) 'x)]) - (plug - (term c_1) - (term (v_arg (lambda (,v) - (abort ,(plug (term c_1) v)))))))) - (reduction lang - (in-hole c (abort e_1)) - (term e_1)) - (reduction/context lang - c - ((lambda (x_format t_1) e_body) v_actual) - ;(lc-subst x_format v_actual e_body) - (lc-subst (term x_format) (term e_body) (term v_actual)) - ))) - - (define lc-subst - (plt-subst - [(? symbol?) (variable)] - [(? number?) (constant)] - [`(lambda (,x ,t) ,b) - (all-vars (list x)) - (build (lambda (vars body) `(lambda (,(car vars) ,t) ,body))) - (subterm (list x) b)] - [`(call/cc ,v) - (all-vars '()) - (build (lambda (vars arg) `(call/cc ,arg))) - (subterm '() v)] - [`(,f ,x) - (all-vars '()) - (build (lambda (vars f x) `(,f ,x))) - (subterm '() f) - (subterm '() x)])) - - (define (type-check term) - (let/ec k - (let loop ([term term] - [env '()]) - (match term - [(? symbol?) - (let ([l (assoc term env)]) - (if l - (cdr l) - (k #f)))] - [(? number?) 'num] - [`(lambda (,x ,t) ,b) - (let ([body (loop b (cons (cons x t) env))]) - `(,t -> ,body))] - [`(,e1 ,e2) - (let ([t1 (loop e1 env)] - [t2 (loop e2 env)]) - (match t1 - [`(,td -> ,tr) - (if (equal? td t2) - tr - (k #f))] - [else (k #f)]))])))) - - (define (pred term1) - (let ([t1 (type-check term1)]) - (lambda (term2) - (and t1 - (equal? (type-check term2) t1))))) - - (define (show term) - (traces/pred lang reductions (list term) (pred term))) - - ;(show '((lambda (x num) x) 1)) - (show '((lambda (x (num -> num)) 1) ((lambda (x (num -> num)) x) (lambda (x num) x)))) - ) diff --git a/collects/reduction-semantics/examples/threads.ss b/collects/reduction-semantics/examples/threads.ss deleted file mode 100644 index d920b4c5ad..0000000000 --- a/collects/reduction-semantics/examples/threads.ss +++ /dev/null @@ -1,128 +0,0 @@ -(module threads mzscheme - (require "../reduction-semantics.ss" - "../gui.ss" - "../subst.ss" - (lib "plt-match.ss")) - - (reduction-steps-cutoff 100) - - (define threads - (language - (p ((store (x v) ...) (threads e ...))) - (e (set! x e) - (let ((x e)) e) - (e e) - x - v - (+ e e)) - (v (lambda (x) e) - number) - (x variable) - (pc ((store (x v) ...) tc)) - (tc (threads e ... ec e ...)) - (ec (ec e) (v ec) (set! variable ec) (let ((x ec)) e) (+ ec e) (+ v ec) hole))) - - (define reductions - (list - - ; sum - (reduction threads - (in-hole pc_1 (+ number_1 number_2)) - (plug (term pc_1) - (+ (term number_1) (term number_2)))) - - ; deref - (reduction threads - ((store - (name befores (x v)) ... - (x_i v_i) - (name afters (x v)) ...) - (in-hole tc_1 x_i)) - (term - ((store - befores ... - (x_i v_i) - afters ...) - ,(plug (term tc_1) (term v_i))))) - ; set! - (reduction threads - ((store (name befores (variable v)) ... - (x_i v) - (name afters (variable v)) ...) - (in-hole tc_1 (set! x_i v_new))) - (term - ((store - befores ... - (x_i v_new) - afters ...) - ,(plug (term tc_1) - (term v_new))))) - ; beta - (reduction threads - (in-hole pc_1 ((lambda (x_1) e_1) v_1)) - (plug (term pc_1) - (substitute (term x_1) (term v_1) (term e_1)))) - - ; let - (reduction threads - ((store (name the-store any) ...) - (in-hole tc_1 (let ((x_1 v_1)) e_1))) - (let ((new-x (variable-not-in (term (the-store ...)) (term x_1)))) - (term - ((store the-store ... (,new-x v_1)) - ,(plug (term tc_1) - (substitute (term x_1) new-x (term e_1))))))))) - - (define substitute - (plt-subst - [(? symbol?) (variable)] - [(? number?) (constant)] - [`(lambda (,x) ,b) - (all-vars (list x)) - (build (lambda (vars body) `(lambda (,(car vars)) ,body))) - (subterm (list x) b)] - [`(set! ,x ,e) - (all-vars '()) - (build (lambda (vars name body) `(set! ,name ,body))) - (subterm '() x) - (subterm '() e)] - [`(let ((,x ,e1)) ,e2) - (all-vars (list x)) - (build (lambda (vars letval body) `(let ((,(car vars) ,letval)) ,body))) - (subterm '() e1) - (subterm (list x) e2)] - [`(+ ,e1 ,e2) - (all-vars '()) - (build (lambda (vars e1 e2) `(+ ,e1 ,e2))) - (subterm '() e1) - (subterm '() e2)] - [`(,f ,x) - (all-vars '()) - (build (lambda (vars f x) `(,f ,x))) - (subterm '() f) - (subterm '() x)])) - - (define (run es) (traces threads reductions `((store) (threads ,@es)))) - (provide run) - - (define (count x) - (match x - [`(set! ,x ,e) (+ 1 (count e))] - [(? symbol?) 1] - [(? number?) 0] - [`(+ ,e1 ,e2) (+ 1 (count e1) (count e2))])) - - (traces threads reductions - '((store (x 1)) - (threads - (set! x (+ x -1)) - (set! x (+ x 1)))) - - (lambda (exp) - (match exp - [`((store (x ,x)) (threads ,t1 ,t2)) - (format "~a ~a ~a" x (count t1) (count t2))]))) - - (parameterize ([initial-char-width 12]) - (traces threads reductions '((store) (threads (+ 1 1) (+ 1 1))))) - ) diff --git a/collects/reduction-semantics/examples/types.ss b/collects/reduction-semantics/examples/types.ss deleted file mode 100644 index 0e4116fc3d..0000000000 --- a/collects/reduction-semantics/examples/types.ss +++ /dev/null @@ -1,91 +0,0 @@ -(module types mzscheme - (require (lib "reduction-semantics.ss" "reduction-semantics") - (lib "gui.ss" "reduction-semantics") - (lib "subst.ss" "reduction-semantics")) - - (reduction-steps-cutoff 10) - - (define lang - (language (e (e e) - x - number - (lambda (x t) e) - (if e e e) - (= e e) - (-> e e) - num - bool) - (c (t c) - (c e) - (-> t c) - (-> c e) - (= t c) - (= c e) - (if c e e) - (if t c e) - (if t t c) - hole) - (x (variable-except lambda -> if =)) - (t num bool (-> t t)))) - - (define-syntax (r--> stx) - (syntax-case stx () - [(_ i r) (syntax (reduction/context lang c i r))])) - - (define-syntax (e--> stx) - (syntax-case stx () - [(_ i msg) (syntax (reduction lang (in-hole c i) msg))])) - - (define reductions - (list - (r--> number - 'num) - - (r--> (lambda (x_1 t_1) e_body) - (term (-> t_1 ,(lc-subst (term x_1) - (term t_1) - (term e_body))))) - - (r--> ((-> t_1 t_2) t_1) - (term t_2)) - - (e--> (side-condition ((-> t_1 t) t_2) - (not (equal? (term t_1) (term t_2)))) - (format "app: domain error ~s and ~s" (term t_1) (term t_2))) - - (e--> (num t_1) - (format "app: non function error ~s" (term t_1))) - - (r--> (if bool t_1 t_1) - (term t_1)) - (e--> (side-condition (if bool t_1 t_2) - (not (equal? (term t_1) (term t_2)))) - (format "if: then and else clause mismatch ~s and ~s" (term t_1) (term t_2))) - (e--> (side-condition (if t_1 t t) - (not (equal? (term t_1) 'bool))) - (format "if: test not boolean ~s" (term t_1))) - - (r--> (= num num) 'bool) - (e--> (side-condition (= t_1 t_2) - (or (not (equal? (term t_1) 'num)) - (not (equal? (term t_2) 'num)))) - (format "=: not comparing numbers ~s and ~s" (term t_1) (term t_2))))) - - (define lc-subst - (subst - [(? symbol?) (variable)] - [(? number?) (constant)] - [`(lambda (,x ,t) ,b) - (all-vars (list x)) - (build (lambda (vars body) `(lambda (,(car vars) ,t) ,body))) - (subterm (list x) b)] - [`(,f ,@(xs ...)) - (all-vars '()) - (build (lambda (vars f . xs) `(,f ,@xs))) - (subterm '() f) - (subterms '() xs)])) - - ; (define theterm '((lambda (x num) (lambda (y num) (if (= x y) 0 x))) 1)) - (define theterm '((lambda (x num) (lambda (y num) (if (= x y) 0 (lambda (x num) x)))) 1)) - (traces lang reductions theterm) - ) diff --git a/collects/reduction-semantics/generator.ss b/collects/reduction-semantics/generator.ss deleted file mode 100644 index 75e436e48b..0000000000 --- a/collects/reduction-semantics/generator.ss +++ /dev/null @@ -1,245 +0,0 @@ -(module generator mzscheme - (require "private/matcher.ss") - - (provide lang->generator-table - for-each-generated - for-each-generated/size) - - (define (lang->generator-table lang - nums - vars - strs - skip-kws - cache-limit) - - ;; -------------------- Cache implementation -------------------- - ;; Cache is currently disabled. It's not clear that it's useful. - (define (cache-small gen) gen) - - ;; -------------------- Build table -------------------- - ;; The `gens' table maps non-terminal symbols to - ;; generator functions. A generator function conumes: - ;; * the min acceptable size of a generated element - ;; * the max acceptable size of a generated element - ;; * a sucess continuation proc that accepts - ;; - the generated value - ;; - the value's size - ;; - a generator proc that produces the next value; - ;; this proc expects to be given the same min, max, - ;; and fail continuation proc as before - ;; * a failure continuation thunk - ;; - (let ([nts (compiled-lang-lang lang)] - [nt-map (make-hash-table)]) - ;; nt-map tells us which symbols are non-terminals; it also - ;; provides conservative min-size and max-size thunks that are - ;; refined as table generation proceeds - (for-each (lambda (nt) (hash-table-put! nt-map (nt-name nt) - (cons (lambda () 1) - (lambda () +inf.0)))) - nts) - ;; gens is the main hash table - (let ([gens (make-hash-table)] - [atomic-alts (lambda (l size) - (values - (lambda (min-size max-size result-k fail-k) - (let loop ([l l][result-k result-k][max-size max-size][fail-k fail-k]) - (if (<= min-size size max-size) - (if (null? l) - (fail-k) - (result-k (car l) - size - (lambda (s xs result-k fail-k) - (loop (cdr l) result-k xs fail-k)))) - (fail-k)))) - (lambda () size) - (lambda () size)))] - [to-do nts]) - (letrec ([make-gen/get-size - (lambda (p) - (cond - [(hash-table-get nt-map p (lambda () #f)) - => (lambda (get-sizes) - (values - (lambda (min-size max-size result-k fail-k) - ((hash-table-get gens p) min-size max-size result-k fail-k)) - (car get-sizes) - (cdr get-sizes)))] - [(eq? 'number p) (atomic-alts nums 1)] - [(eq? 'string p) (atomic-alts strs 1)] - [(eq? 'any p) (atomic-alts (append nums strs vars) 1)] - [(or (eq? 'variable p) - (and (pair? p) - (eq? (car p) 'variable-except))) - (atomic-alts vars 1)] - [(symbol? p) ; not a non-terminal, because we checked above - (if (memq p skip-kws) - (values - (lambda (min-size max-size result-k fail-k) - (fail-k)) - (lambda () +inf.0) - (lambda () -1)) - (atomic-alts (list p) 0))] - [(null? p) (atomic-alts (list null) 0)] - [(and (pair? p) - (or (not (pair? (cdr p))) - (not (eq? '... (cadr p))))) - (make-pair-gen/get-size p cons)] - [(and (pair? p) (pair? (cdr p)) (eq? '... (cadr p))) - (let-values ([(just-rest just-rest-min-size just-rest-max-size) - (make-gen/get-size (cddr p))] - [(both both-min-size both-max-size) - (make-pair-gen/get-size (cons (kleene+ (car p)) (cddr p)) append)]) - (values - (lambda (min-size max-size result-k fail-k) - (let loop ([both both][result-k result-k][max-size max-size][fail-k fail-k]) - (both min-size max-size - (lambda (v size next-both) - (result-k v size - (lambda (ns xs result-k fail-k) - (loop next-both result-k xs fail-k)))) - (lambda () - (just-rest min-size max-size result-k fail-k))))) - just-rest-min-size - (lambda () +inf.0)))] - [else - (error 'make-gen "unrecognized pattern: ~e" p)]))] - [make-pair-gen/get-size - (lambda (p combiner) - (let*-values ([(first first-min-size first-max-size) - (make-gen/get-size (car p))] - [(rest rest-min-size rest-max-size) - (make-gen/get-size (cdr p))] - [(this-min-size) (let ([v #f]) - (lambda () - (unless v - (set! v (+ (first-min-size) - (rest-min-size)))) - v))] - [(this-max-size) (let ([v #f]) - (lambda () - (unless v - (set! v (+ (first-max-size) - (rest-max-size)))) - v))]) - (values - (cache-small - (lambda (min-size max-size result-k fail-k) - (if (min-size . > . (this-max-size)) - (fail-k) - (let rloop ([rest rest][result-k result-k][max-size max-size][fail-k fail-k][failed-size +inf.0]) - (if (max-size . < . (this-min-size)) - (fail-k) - (rest - (max 0 (- min-size (first-max-size))) - (min (sub1 failed-size) (- max-size (first-min-size))) - (lambda (rest rest-size next-rest) - (if (rest-size . >= . failed-size) - (rloop next-rest result-k max-size fail-k failed-size) - (let floop ([first first] - [result-k result-k] - [max-size max-size] - [fail-k fail-k] - [first-fail-k (lambda () - (rloop next-rest result-k max-size fail-k rest-size))]) - (first (max 0 (- min-size rest-size)) - (- max-size rest-size) - (lambda (first first-size next-first) - (result-k - (combiner first rest) - (+ first-size rest-size) - (lambda (ns xs result-k fail-k) - (floop next-first result-k xs fail-k - (lambda () - (rloop next-rest result-k xs fail-k failed-size)))))) - first-fail-k)))) - fail-k)))))) - this-min-size - this-max-size)))] - [kleene+ (lambda (p) - (let ([n (gensym)]) - (hash-table-put! nt-map n (cons (lambda () 1) - (lambda () +inf.0))) - (set! to-do (cons (make-nt - n - (list (make-rhs (cons p '())) - (make-rhs (cons p n)))) - to-do)) - n))]) - (let to-do-loop ([nts (reverse to-do)]) - (set! to-do null) - (for-each (lambda (nt) - (hash-table-put! - gens - (nt-name nt) - (let* ([gens+sizes - (map (lambda (rhs) - (let-values ([(gen get-min-size get-max-size) - (make-gen/get-size - (rhs-pattern rhs))]) - (cons gen (cons get-min-size get-max-size)))) - (nt-rhs nt))] - [get-min-size - (let ([get-min-sizes (map cadr gens+sizes)]) - (let ([v #f]) - (lambda () - (unless v - (set! v (add1 - (apply min (map (lambda (gs) (gs)) - get-min-sizes))))) - v)))] - [get-max-size - (let ([get-max-sizes (map cddr gens+sizes)]) - (let ([v #f]) - (lambda () - (unless v - (set! v (add1 - (apply max (map (lambda (gs) (gs)) - get-max-sizes))))) - v)))]) - (hash-table-put! nt-map (nt-name nt) - (cons get-min-size get-max-size)) - (cache-small - (lambda (min-size max-size result-k fail-k) - (if (min-size . > . (get-max-size)) - (fail-k) - (let loop ([l (map car gens+sizes)][result-k result-k][max-size max-size][fail-k fail-k]) - (if (max-size . < . (get-min-size)) - (fail-k) - (if (null? l) - (fail-k) - (let iloop ([alt-next (car l)] - [result-k result-k] - [max-size max-size] - [fail-k fail-k]) - (alt-next - (max 0 (sub1 min-size)) - (sub1 max-size) - (lambda (alt a-size alt-next) - (result-k - alt - (add1 a-size) - (lambda (ns xs result-k fail-k) - (iloop alt-next result-k xs fail-k)))) - (lambda () - (loop (cdr l) result-k max-size fail-k))))))))))))) - nts) - (unless (null? to-do) - (to-do-loop to-do)))) - gens))) - - (define (for-each-generated/size proc gens min-size max-size nonterm) - (let ([gen (hash-table-get gens nonterm)]) - (let loop ([gen gen]) - (gen - min-size - max-size - (lambda (val z1 gen-next) - (proc val z1) - (loop gen-next)) - void)))) - - (define (for-each-generated proc gens nonterm) - (let loop ([i 0]) - (for-each-generated/size proc gens i i nonterm) - (loop (add1 i))))) diff --git a/collects/reduction-semantics/graph.ss b/collects/reduction-semantics/graph.ss deleted file mode 100644 index 9323ff0430..0000000000 --- a/collects/reduction-semantics/graph.ss +++ /dev/null @@ -1,1023 +0,0 @@ - -;; To be merged back into (lib "graph.ss" "mrlib") eventually... - -(module graph mzscheme - (require (lib "class.ss") - (lib "list.ss") - (lib "math.ss") - (lib "mred.ss" "mred") - (lib "contract.ss")) - - (provide graph-snip<%> - graph-snip-mixin - graph-pasteboard-mixin) - - (define graph-snip<%> - (interface () - get-children - add-child - remove-child - - get-parents - add-parent - remove-parent - has-self-loop? - - find-shortest-path)) - - (define-local-member-name get-parent-links) - - (provide/contract (add-links - (case-> - ((is-a?/c graph-snip<%>) - (is-a?/c graph-snip<%>) - . -> . - void?) - ((is-a?/c graph-snip<%>) - (is-a?/c graph-snip<%>) - (union false/c (is-a?/c pen%)) - (union false/c (is-a?/c pen%)) - (union false/c (is-a?/c brush%)) - (union false/c (is-a?/c brush%)) - number? - number? - . -> . - void?) - ((is-a?/c graph-snip<%>) - (is-a?/c graph-snip<%>) - (union false/c (is-a?/c pen%)) - (union false/c (is-a?/c pen%)) - (union false/c (is-a?/c brush%)) - (union false/c (is-a?/c brush%)) - (union false/c string?) - . -> . - void?) - ((is-a?/c graph-snip<%>) - (is-a?/c graph-snip<%>) - (union false/c (is-a?/c pen%)) - (union false/c (is-a?/c pen%)) - (union false/c (is-a?/c brush%)) - (union false/c (is-a?/c brush%)) - number? - number? - . -> . - void?))) - (add-links/text-colors - ((is-a?/c graph-snip<%>) - (is-a?/c graph-snip<%>) - (union false/c (is-a?/c pen%)) - (union false/c (is-a?/c pen%)) - (union false/c (is-a?/c brush%)) - (union false/c (is-a?/c brush%)) - (union false/c (is-a?/c color%)) - (union false/c (is-a?/c color%)) - number? - number? - (union false/c string?) - . -> . - void?))) - - (define self-offset 10) - - ;; (or-2v arg ...) - ;; like `or', except each `arg' returns two values. The - ;; truth value of each arg is #t if both args are #t and - ;; #f otherwise - (define-syntax (or-2v stx) - (syntax-case stx () - [(_ arg) - (syntax arg)] - [(_ arg args ...) - (syntax - (let-values ([(one two) arg]) - (if (and one two) - (values one two) - (or-2v args ...))))])) - - (define snipclass (make-object snip-class%)) - - (define default-dark-pen (send the-pen-list find-or-create-pen "blue" 1 'solid)) - (define default-light-pen (send the-pen-list find-or-create-pen "light blue" 1 'solid)) - (define default-dark-brush (send the-brush-list find-or-create-brush "light blue" 'solid)) - (define default-light-brush (send the-brush-list find-or-create-brush "white" 'solid)) - (define default-dark-text "blue") - (define default-light-text "light blue") - - - ;; label is boolean or string - (define-struct link (snip dark-pen light-pen dark-brush light-brush dark-text light-text dx dy label)) - - ;; add-links : (is-a?/c graph-snip<%>) (is-a?/c graph-snip<%>) -> void - ;; : (is-a?/c graph-snip<%>) (is-a?/c graph-snip<%>) pen pen brush brush -> void - (define add-links - (case-lambda - [(parent child) (add-links parent child #f #f #f #f)] - [(parent child dark-pen light-pen dark-brush light-brush) - (add-links parent child dark-pen light-pen dark-brush light-brush 0 0)] - [(parent child dark-pen light-pen dark-brush light-brush label) - (add-links parent child dark-pen light-pen dark-brush light-brush 0 0 label)] - [(parent child dark-pen light-pen dark-brush light-brush dx dy) - (add-links parent child dark-pen light-pen dark-brush light-brush dx dy #f)] - [(parent child dark-pen light-pen dark-brush light-brush dx dy label) - (send parent add-child child) - (send child add-parent parent dark-pen light-pen dark-brush light-brush dx dy label)])) - - (define (add-links/text-colors parent child dark-pen light-pen dark-brush light-brush dark-text light-text dx dy label) - (send parent add-child child) - (send child add-parent parent dark-pen light-pen dark-brush light-brush dark-text light-text dx dy label)) - - (define graph-snip-mixin - (mixin ((class->interface editor-snip%)) (graph-snip<%>) - (field (children null)) - (define/public (get-children) children) - (define/public (add-child child) - (unless (memq child children) - (set! children (cons child children)))) - (define/public (remove-child child) - (when (memq child children) - (set! children (remq child children)))) - - (field (parent-links null)) - (define/public (get-parent-links) parent-links) - (define/public (get-parents) (map link-snip parent-links)) - (define/public add-parent - (case-lambda - [(parent) (add-parent parent #f #f #f #f)] - [(parent dark-pen light-pen dark-brush light-brush) - (add-parent parent dark-pen light-pen dark-brush light-brush 0 0)] - [(parent dark-pen light-pen dark-brush light-brush dx dy) - (add-parent parent dark-pen light-pen dark-brush light-brush dx dy #f)] - [(parent dark-pen light-pen dark-brush light-brush dx dy) - (add-parent parent dark-pen light-pen dark-brush light-brush #f #f dx dy #f)] - [(parent dark-pen light-pen dark-brush light-brush dark-text light-text dx dy label) - (unless (memf (lambda (parent-link) (eq? (link-snip parent-link) parent)) parent-links) - (set! parent-links - (cons (make-link parent - (or dark-pen default-dark-pen) - (or light-pen default-light-pen) - (or dark-brush default-dark-brush) - (or light-brush default-light-brush) - (or dark-text default-dark-text) - (or light-text default-light-text) - dx - dy - label) - parent-links)))])) - (define/public (remove-parent parent) - (when (memf (lambda (parent-link) (eq? (link-snip parent-link) parent)) parent-links) - (set! parent-links - (remove - parent - parent-links - (lambda (parent parent-link) (eq? (link-snip parent-link) parent)))))) - - (define/public (has-self-loop?) - (memq this (get-children))) - - (define/public (find-shortest-path other) - (define visited-ht (make-hash-table)) - (define (first-view? n) - (hash-table-get visited-ht n (lambda () - (hash-table-put! visited-ht n #f) - #t))) - (let loop ((horizon (list (list this)))) - (cond - [(null? horizon) #f] - [(assq other horizon) => (lambda (winner) winner)] - [else - (let inner-loop ((paths horizon) - (acc '())) - (cond - [(null? paths) (loop (apply append acc))] - [else - (let ((path (car paths))) - (inner-loop - (cdr paths) - (cons - (map (lambda (child) (cons child path)) (filter first-view? (send (car path) get-children))) - acc)))]))]))) - - (init-field [left-margin 1] - [right-margin 1] - [top-margin 1] - [bottom-margin 1] - - [left-inset 0] - [right-inset 0] - [top-inset 0] - [bottom-inset 0] - ) - - (super-new [left-margin left-margin] - [right-margin right-margin] - [top-margin top-margin] - [bottom-margin bottom-margin] - - [left-inset left-inset] - [right-inset right-inset] - [top-inset top-inset] - [bottom-inset bottom-inset] - ) - - - - (inherit set-snipclass) - (set-snipclass snipclass))) - - (define graph-pasteboard<%> - (interface () - on-mouse-over-snips - set-arrowhead-params)) - - (define-struct rect (left top right bottom)) - - (define graph-pasteboard-mixin - (mixin ((class->interface pasteboard%)) (graph-pasteboard<%>) - (inherit find-first-snip find-next-selected-snip) - - (define arrowhead-angle-width (* 1/4 pi)) - (define arrowhead-short-side 8) - (define arrowhead-long-side 12) - - (define/public (set-arrowhead-params angle-width long-side short-side) - (set! arrowhead-angle-width angle-width) - (set! arrowhead-short-side short-side) - (set! arrowhead-long-side long-side)) - (define/public (get-arrowhead-params) - (values arrowhead-angle-width - arrowhead-long-side - arrowhead-short-side)) - - (inherit dc-location-to-editor-location get-canvas get-dc) - (field (currently-overs null)) - (define/override (on-event evt) - (cond - [(send evt leaving?) - (change-currently-overs null (get-dc)) - (super on-event evt)] - [(or (send evt entering?) - (send evt moving?)) - (let ([ex (send evt get-x)] - [ey (send evt get-y)]) - (let-values ([(x y) (dc-location-to-editor-location ex ey)]) - (change-currently-overs (find-snips-under-mouse x y) (get-dc)))) - (super on-event evt)] - [else - (super on-event evt)])) - - (define/augment (on-interactive-move evt) - (invalidate-selected-snips) - #;(super on-interactive-move evt) - ) - - (define/augment (after-interactive-move evt) - (invalidate-selected-snips) - #;(super on-interactive-move evt)) - - (define/override (interactive-adjust-move snip x y) - (invalidate-to-children/parents snip (get-dc)) - (super interactive-adjust-move snip x y)) - - (define/augment (after-insert snip before x y) - (invalidate-to-children/parents snip (get-dc)) - #;(super after-insert snip before x y)) - - ;; invalidate-selected-snips : -> void - ;; invalidates the region around the selected - ;; snips and their parents and children - (define/private (invalidate-selected-snips) - (let loop ([snip (find-next-selected-snip #f)]) - (when snip - (invalidate-to-children/parents snip (get-dc)) - (loop (find-next-selected-snip snip))))) - - (define/private (add-to-rect from to rect) - (let-values ([(xf yf wf hf) (get-position from)] - [(xt yt wt ht) (get-position to)]) - (make-rect - (if rect - (min xf xt (rect-left rect)) - (min xf xt)) - (if rect - (min yf yt (rect-top rect)) - (min yf yt)) - (if rect - (max (+ xf wf) (+ xt wt) (rect-right rect)) - (max (+ xf wf) (+ xt wt))) - (if rect - (max (+ yf hf) (+ yt ht) (rect-bottom rect)) - (max (+ yf hf) (+ yt ht)))))) - - ;; find-snips-under-mouse : num num -> (listof graph-snip<%>) - (define/private (find-snips-under-mouse x y) - (let loop ([snip (find-first-snip)]) - (cond - [snip - (let-values ([(sx sy sw sh) (get-position snip)]) - (if (and (<= sx x (+ sx sw)) - (<= sy y (+ sy sh)) - (is-a? snip graph-snip<%>)) - (cons snip (loop (send snip next))) - (loop (send snip next))))] - [else null]))) - - ;; change-currently-overs : (listof snip) -> void - (define/private (change-currently-overs new-currently-overs dc) - (unless (set-equal new-currently-overs currently-overs) - (let ([old-currently-overs currently-overs]) - (set! currently-overs new-currently-overs) - - (on-mouse-over-snips currently-overs) - (for-each - (lambda (old-currently-over) - (invalidate-to-children/parents old-currently-over dc)) - old-currently-overs) - (for-each - (lambda (new-currently-over) - (invalidate-to-children/parents new-currently-over dc)) - new-currently-overs)))) - - (define/public (on-mouse-over-snips snips) - (void)) - - ;; set-equal : (listof snip) (listof snip) -> boolean - ;; typically lists will be small (length 1), - ;; so use andmap/memq rather than hash-tables - (define/private (set-equal los1 los2) - (and (andmap (lambda (s1) (memq s1 los2)) los1) - (andmap (lambda (s2) (memq s2 los1)) los2) - #t)) - - ;; invalidate-to-children/parents : snip dc -> void - ;; invalidates the region containing this snip and - ;; all of its children and parents. - (inherit invalidate-bitmap-cache) - (define/private (invalidate-to-children/parents snip dc) - (when (is-a? snip graph-snip<%>) - (let* ([parents-and-children (append (get-all-parents snip) - (get-all-children snip))] - [rects (eliminate-redundancies (get-rectangles snip parents-and-children))] - [union (union-rects rects)] - [text-height (call-with-values - (λ () (send dc get-text-extent "Label" #f #f 0)) - (λ (w h a s) h))] - [invalidate-rect - (lambda (rect) - (invalidate-bitmap-cache (- (rect-left rect) text-height) - (- (rect-top rect) text-height) - (+ (- (rect-right rect) - (rect-left rect)) - text-height) - (+ (- (rect-bottom rect) - (rect-top rect)) - text-height)))]) - (cond - [(< (rect-area union) - (apply + (map (lambda (x) (rect-area x)) rects))) - (invalidate-rect union)] - [else - (for-each invalidate-rect rects)])))) - - ;; (listof rect) -> (listof rect) - (define/private (eliminate-redundancies rects) - (let loop ([rects rects] - [acc null]) - (cond - [(null? rects) acc] - [else (let ([r (car rects)]) - (cond - [(or (ormap (lambda (other-rect) (rect-included-in? r other-rect)) - (cdr rects)) - (ormap (lambda (other-rect) (rect-included-in? r other-rect)) - acc)) - (loop (cdr rects) - acc)] - [else - (loop (cdr rects) - (cons r acc))]))]))) - - ;; rect-included-in? : rect rect -> boolean - (define/private (rect-included-in? r1 r2) - (and ((rect-left r1) . >= . (rect-left r2)) - ((rect-top r1) . >= . (rect-top r2)) - ((rect-right r1) . <= . (rect-right r2)) - ((rect-bottom r1) . <= . (rect-bottom r2)))) - - ;; get-rectangles : snip (listof snip) -> rect - ;; computes the rectangles that need to be invalidated for connecting - (define/private (get-rectangles main-snip c/p-snips) - (let ([main-snip-rect (snip->rect main-snip)]) - (let loop ([c/p-snips c/p-snips]) - (cond - [(null? c/p-snips) null] - [else - (let* ([c/p (car c/p-snips)] - [rect - (if (eq? c/p main-snip) - (let-values ([(sx sy sw sh) (get-position c/p)] - [(_1 h _2 _3) (send (get-dc) get-text-extent "yX")]) - (make-rect (- sx self-offset) - sy - (+ (+ sx sw) self-offset) - (+ (+ sy sh) self-offset h))) - (union-rects (list main-snip-rect - (snip->rect c/p))))]) - (cons rect (loop (cdr c/p-snips))))])))) - - (define/private (snip->rect snip) - (let-values ([(sx sy sw sh) (get-position snip)] - [(_1 h _2 _3) (send (get-dc) get-text-extent "yX")]) - (make-rect sx - sy - (+ sx sw) - (max (+ sy sh) (+ sy (/ sh 2) (* 2 (sin (/ arrowhead-angle-width 2)) arrowhead-long-side) h))))) - - (define/private (rect-area rect) - (* (- (rect-right rect) - (rect-left rect)) - (- (rect-bottom rect) - (rect-top rect)))) - - (define/private (union-rects rects) - (cond - [(null? rects) (make-rect 0 0 0 0)] - [else - (let loop ([rects (cdr rects)] - [l (rect-left (car rects))] - [t (rect-top (car rects))] - [r (rect-right (car rects))] - [b (rect-bottom (car rects))]) - (cond - [(null? rects) (make-rect l t r b)] - [else - (let ([rect (car rects)]) - (loop (cdr rects) - (min l (rect-left rect)) - (min t (rect-top rect)) - (max r (rect-right rect)) - (max b (rect-bottom rect))))]))])) - - ;; on-paint : ... -> void - ;; see docs, same as super - ;; draws all of the lines and then draws all of the arrow heads - (define/private (old-on-paint before? dc left top right bottom dx dy draw-caret) - (let () - ;; draw-connection : link snip boolean boolean -> void - ;; sets the drawing context (pen and brush) - ;; determines if the connection is between a snip and itself or two different snips - ;; and calls draw-self-connection or draw-non-self-connection - (define (draw-connection from-link to dark-lines?) - (let ([from (link-snip from-link)]) - (when (send from get-admin) - (let ([dx (+ dx (link-dx from-link))] - [dy (+ dy (link-dy from-link))]) - (cond - [(eq? from to) - (set-pen/brush from-link dark-lines?) - (draw-self-connection dx dy (link-snip from-link))] - [else - (draw-non-self-connection dx dy from-link dark-lines? to)]))))) - - (define (draw-self-connection dx dy snip) - (let*-values ([(sx sy sw sh) (get-position snip)] - [(s1x s1y) (values (+ sx sw) (+ sy (* sh 1/2)))] - [(s2x s2y) (values (+ sx sw self-offset) (+ sy (* 3/4 sh) (* 1/2 self-offset)))] - [(s3x s3y) (values (+ sx sw) (+ sy sh self-offset))] - [(b12x b12y) (values s2x s1y)] - [(b23x b23y) (values s2x s3y)] - - [(s4x s4y) (values (- sx arrowhead-short-side) - (+ sy (* sh 1/2)))] - [(s5x s5y) (values (- sx arrowhead-short-side self-offset) - (+ sy (* 3/4 sh) (* 1/2 self-offset)))] - [(s6x s6y) (values (- sx arrowhead-short-side) - (+ sy sh self-offset))] - [(b45x b45y) (values s5x s4y)] - [(b56x b56y) (values s5x s6y)]) - - (update-polygon s4x s4y sx s4y) - (send dc draw-spline (+ dx s1x) (+ dy s1y) (+ dx b12x) (+ dy b12y) (+ dx s2x) (+ dy s2y)) - (send dc draw-spline (+ dx s2x) (+ dy s2y) (+ dx b23x) (+ dy b23y) (+ dx s3x) (+ dy s3y)) - (send dc draw-line (+ dx s3x) (+ dy s3y) (+ dx s6x) (+ dy s6y)) - (send dc draw-spline (+ dx s4x) (+ dy s4y) (+ dx b45x) (+ dy b45y) (+ dx s5x) (+ dy s5y)) - (send dc draw-spline (+ dx s5x) (+ dy s5y) (+ dx b56x) (+ dy b56y) (+ dx s6x) (+ dy s6y)) - (send dc draw-polygon points dx dy))) - - (define (draw-non-self-connection dx dy from-link dark-lines? to) - (let ([from (link-snip from-link)]) - (let*-values ([(xf yf wf hf) (get-position from)] - [(xt yt wt ht) (get-position to)] - [(lf tf rf bf) (values xf yf (+ xf wf) (+ yf hf))] - [(lt tt rt bt) (values xt yt (+ xt wt) (+ yt ht))]) - (let ([x1 (+ xf (/ wf 2))] - [y1 (+ yf (/ hf 2))] - [x2 (+ xt (/ wt 2))] - [y2 (+ yt (/ ht 2))]) - - (unless (or (and (x1 . <= . left) - (x2 . <= . left)) - (and (x1 . >= . right) - (x2 . >= . right)) - (and (y1 . <= . top) - (y2 . <= . top)) - (and (y1 . >= . bottom) - (y2 . >= . bottom))) - (set-pen/brush from-link dark-lines?) - (let-values ([(from-x from-y) - (or-2v (find-intersection x1 y1 x2 y2 - lf tf rf tf) - (find-intersection x1 y1 x2 y2 - lf bf rf bf) - (find-intersection x1 y1 x2 y2 - lf tf lf bf) - (find-intersection x1 y1 x2 y2 - rf tf rf bf))] - [(to-x to-y) - (or-2v (find-intersection x1 y1 x2 y2 - lt tt rt tt) - (find-intersection x1 y1 x2 y2 - lt bt rt bt) - (find-intersection x1 y1 x2 y2 - lt tt lt bt) - (find-intersection x1 y1 x2 y2 - rt tt rt bt))]) - (when (and from-x from-y to-x to-y) - (let () - (define (arrow-point-ok? point-x point-y) - (and (in-rectangle? point-x point-y - (min lt rt lf rf) (min tt bt tf bf) - (max lt rt lf rf) (max tt bt tf bf)) - (not (strict-in-rectangle? point-x point-y - (min lt rt) (min tt bt) - (max lt rt) (max tt bt))) - (not (strict-in-rectangle? point-x point-y - (min lf rf) (min tf bf) - (max lf rf) (max tf bf))))) - (cond - [(or (in-rectangle? from-x from-y lt tt rt bt) - (in-rectangle? to-x to-y lf tf rf bf)) - ;; the snips overlap, draw nothing - (void)] - [else - (send dc draw-line - (+ dx from-x) (+ dy from-y) - (+ dx to-x) (+ dy to-y)) - (update-polygon from-x from-y to-x to-y) - (when (and (arrow-point-ok? (send point1 get-x) (send point1 get-y)) - (arrow-point-ok? (send point2 get-x) (send point2 get-y)) - (arrow-point-ok? (send point3 get-x) (send point3 get-y)) - (arrow-point-ok? (send point4 get-x) (send point4 get-y))) - ;; the arrowhead is not overlapping the snips, so draw it - ;; (this is only an approximate test, but probably good enough) - (send dc draw-polygon points dx dy))]))))))))) - - (define (set-pen/brush from-link dark-lines?) - (send dc set-brush - (if dark-lines? - (link-dark-brush from-link) - (link-light-brush from-link))) - (send dc set-pen - (if dark-lines? - (link-dark-pen from-link) - (link-light-pen from-link)))) - - ;;; body of on-paint - (when before? - (let ([old-pen (send dc get-pen)] - [old-brush (send dc get-brush)] - [os (send dc get-smoothing)]) - (send dc set-smoothing 'aligned) - - (let loop ([snip (find-first-snip)]) - (when snip - (when (and (send snip get-admin) - (is-a? snip graph-snip<%>)) - (for-each (lambda (parent-link) - (draw-connection parent-link snip #f)) - (send snip get-parent-links))) - (loop (send snip next)))) - - (for-each - (lambda (currently-over) - (for-each - (lambda (child) - (let ([parent-link-f - (memf (lambda (parent-link) (eq? currently-over (link-snip parent-link))) - (send child get-parent-links))]) - (when parent-link-f - (draw-connection (car parent-link-f) child #t)))) - (send currently-over get-children)) - (for-each - (lambda (parent-link) - (draw-connection parent-link currently-over #t)) - (send currently-over get-parent-links))) - currently-overs) - - (send dc set-smoothing os) - (send dc set-pen old-pen) - (send dc set-brush old-brush))) - - (super on-paint before? dc left top right bottom dx dy draw-caret))) - - (define/override (on-paint before? dc left top right bottom dx dy draw-caret) - (let () - ;; draw-connection : link snip boolean boolean -> void - ;; sets the drawing context (pen and brush) - ;; determines if the connection is between a snip and itself or two different snips - ;; and calls draw-self-connection or draw-non-self-connection - (define (draw-connection from-link to dark-lines?) - (let ([from (link-snip from-link)]) - (when (send from get-admin) - (let ([dx (+ dx (link-dx from-link))] - [dy (+ dy (link-dy from-link))]) - (cond - [(eq? from to) - (set-pen/brush from-link dark-lines?) - (draw-self-connection dx dy (link-snip from-link) from-link dark-lines?)] - [else - (draw-non-self-connection dx dy from-link dark-lines? to)]))))) - - (define (get-text-length txt) - (let-values ([(text-len h d v) (send dc get-text-extent txt)]) - text-len)) - - (define (draw-self-connection dx dy snip the-link dark-lines?) - (let*-values ([(sx sy sw sh) (get-position snip)] - [(s1x s1y) (values (+ sx sw) (+ sy (* sh 1/2)))] - [(s2x s2y) (values (+ sx sw self-offset) (+ sy (* 3/4 sh) (* 1/2 self-offset)))] - [(s3x s3y) (values (+ sx sw) (+ sy sh self-offset))] - [(b12x b12y) (values s2x s1y)] - [(b23x b23y) (values s2x s3y)] - - [(s4x s4y) (values (- sx arrowhead-short-side) - (+ sy (* sh 1/2)))] - [(s5x s5y) (values (- sx arrowhead-short-side self-offset) - (+ sy (* 3/4 sh) (* 1/2 self-offset)))] - [(s6x s6y) (values (- sx arrowhead-short-side) - (+ sy sh self-offset))] - [(b45x b45y) (values s5x s4y)] - [(b56x b56y) (values s5x s6y)]) - - (update-polygon s4x s4y sx s4y) - (send dc draw-spline (+ dx s1x) (+ dy s1y) (+ dx b12x) (+ dy b12y) (+ dx s2x) (+ dy s2y)) - (send dc draw-spline (+ dx s2x) (+ dy s2y) (+ dx b23x) (+ dy b23y) (+ dx s3x) (+ dy s3y)) - (send dc draw-line (+ dx s3x) (+ dy s3y) (+ dx s6x) (+ dy s6y)) - - (let* ((textlen (get-text-length (link-label the-link))) - (linelen (- s6x s3x)) - (offset (* 1/2 (- linelen textlen)))) - (when #t (> sw textlen) - (send dc draw-text - (link-label the-link) - (+ dx s3x offset) - (+ dy s3y) - #f - 0 - 0))) - - (send dc draw-spline (+ dx s4x) (+ dy s4y) (+ dx b45x) (+ dy b45y) (+ dx s5x) (+ dy s5y)) - (send dc draw-spline (+ dx s5x) (+ dy s5y) (+ dx b56x) (+ dy b56y) (+ dx s6x) (+ dy s6y)) - (send dc draw-polygon points dx dy))) - - (define (draw-non-self-connection dx dy from-link dark-lines? to) - (let ([from (link-snip from-link)]) - (let*-values ([(xf yf wf hf) (get-position from)] - [(xt yt wt ht) (get-position to)] - [(lf tf rf bf) (values xf yf (+ xf wf) (+ yf hf))] - [(lt tt rt bt) (values xt yt (+ xt wt) (+ yt ht))]) - (let ([x1 (+ xf (/ wf 2))] - [y1 (+ yf (/ hf 2))] - [x2 (+ xt (/ wt 2))] - [y2 (+ yt (/ ht 2))]) - - (set-pen/brush from-link dark-lines?) - (let-values ([(from-x from-y) - (or-2v (find-intersection x1 y1 x2 y2 - lf tf rf tf) - (find-intersection x1 y1 x2 y2 - lf bf rf bf) - (find-intersection x1 y1 x2 y2 - lf tf lf bf) - (find-intersection x1 y1 x2 y2 - rf tf rf bf))] - [(to-x to-y) - (or-2v (find-intersection x1 y1 x2 y2 - lt tt rt tt) - (find-intersection x1 y1 x2 y2 - lt bt rt bt) - (find-intersection x1 y1 x2 y2 - lt tt lt bt) - (find-intersection x1 y1 x2 y2 - rt tt rt bt))]) - (when (and from-x from-y to-x to-y) - (let ((from-pt (make-rectangular from-x from-y)) - (to-pt (make-rectangular to-x to-y))) - (define (arrow-point-ok? point-x point-y) - (and (in-rectangle? point-x point-y - (min lt rt lf rf) (min tt bt tf bf) - (max lt rt lf rf) (max tt bt tf bf)) - (not (strict-in-rectangle? point-x point-y - (min lt rt) (min tt bt) - (max lt rt) (max tt bt))) - (not (strict-in-rectangle? point-x point-y - (min lf rf) (min tf bf) - (max lf rf) (max tf bf))))) - (cond - [(or (in-rectangle? from-x from-y lt tt rt bt) - (in-rectangle? to-x to-y lf tf rf bf)) - ;; the snips overlap, draw nothing - (void)] - [else - (send dc draw-line - (+ dx from-x) (+ dy from-y) - (+ dx to-x) (+ dy to-y)) - (update-polygon from-x from-y to-x to-y) - (when (and (arrow-point-ok? (send point1 get-x) (send point1 get-y)) - (arrow-point-ok? (send point2 get-x) (send point2 get-y)) - (arrow-point-ok? (send point3 get-x) (send point3 get-y)) - (arrow-point-ok? (send point4 get-x) (send point4 get-y))) - ;; the arrowhead is not overlapping the snips, so draw it - ;; (this is only an approximate test, but probably good enough) - (send dc draw-polygon points dx dy)) - (when (named-link? from-link) - (let*-values ([(text-len h d v) (send dc get-text-extent (link-label from-link))] - [(x) (/ (+ from-x to-x) 2)] - [(y) (/ (+ from-y to-y) 2)] - [(theta) (- (angle (- to-pt from-pt)))] - [(flip?) #f #;(negative? (- to-x from-x))] - [(text-angle) - (if flip? - (+ theta pi) - theta)] - [(x) - (- x (* h (cos (if flip? (+ (- theta) pi) (- theta)))))] - [(y) - (- y (* h (sin (if flip? (+ (- theta) pi) (- theta)))))] - [(sqr) (λ (x) (* x x))]) - (when (> (sqrt (+ (sqr (- to-x from-x)) (sqr (- to-y from-y)))) text-len) - (send dc draw-text (link-label from-link) - (+ dx x) - (+ dy y) - #f - 0 - text-angle)) - ))])))))))) - (define (named-link? l) (link-label l)) - - (define (set-pen/brush from-link dark-lines?) - (send dc set-brush - (if dark-lines? - (link-dark-brush from-link) - (link-light-brush from-link))) - (send dc set-pen - (if dark-lines? - (link-dark-pen from-link) - (link-light-pen from-link))) - (send dc set-text-foreground - (if dark-lines? - (link-dark-text from-link) - (link-light-text from-link)))) - - ;;; body of on-paint - (when before? - (let ([old-pen (send dc get-pen)] - [old-brush (send dc get-brush)] - [old-fg (send dc get-text-foreground)] - [os (send dc get-smoothing)]) - (send dc set-smoothing 'aligned) - - (let ([pairs '()]) - (for-each-to-redraw - left top right bottom - (lambda (from-link to) - (let ([from (link-snip from-link)]) - (cond - [(or (memq from currently-overs) - (memq to currently-overs)) - (set! pairs (cons (cons from-link to) pairs))] - [else - (draw-connection from-link to #f)])))) - (for-each (lambda (pr) - (draw-connection (car pr) (cdr pr) #t)) - pairs)) - - (send dc set-smoothing os) - (send dc set-pen old-pen) - (send dc set-text-foreground old-fg) - (send dc set-brush old-brush))) - - (super on-paint before? dc left top right bottom dx dy draw-caret))) - - ;; for-each-to-redraw : number number number number (link snip -> void) - (define/private (for-each-to-redraw left top right bottom f) - (let () - ;; draw-connection : link snip boolean boolean -> void - ;; sets the drawing context (pen and brush) - ;; determines if the connection is between a snip and itself or two different snips - ;; and calls draw-self-connection or draw-non-self-connection - (define (maybe-call-f from-link to) - (let ([from (link-snip from-link)]) - (when (send from get-admin) - (cond - [(eq? from to) - (f from-link to)] - [else - (let*-values ([(xf yf wf hf) (get-position from)] - [(xt yt wt ht) (get-position to)] - [(lf tf rf bf) (values xf yf (+ xf wf) (+ yf hf))] - [(lt tt rt bt) (values xt yt (+ xt wt) (+ yt ht))]) - (let ([x1 (+ xf (/ wf 2))] - [y1 (+ yf (/ hf 2))] - [x2 (+ xt (/ wt 2))] - [y2 (+ yt (/ ht 2))]) - - (unless (or (and (x1 . <= . left) - (x2 . <= . left)) - (and (x1 . >= . right) - (x2 . >= . right)) - (and (y1 . <= . top) - (y2 . <= . top)) - (and (y1 . >= . bottom) - (y2 . >= . bottom))) - (f from-link to))))])))) - - (let loop ([snip (find-first-snip)]) - (when snip - (when (and (send snip get-admin) - (is-a? snip graph-snip<%>)) - (for-each (lambda (parent-link) (maybe-call-f parent-link snip)) - (send snip get-parent-links))) - (loop (send snip next)))))) - - - (field - [point1 (make-object point% 0 0)] - [point2 (make-object point% 0 0)] - [point3 (make-object point% 0 0)] - [point4 (make-object point% 0 0)] - [points (list point1 point2 point3 point4)]) - - ;; update-polygon : number^4 -> void - ;; updates points1, 2, and 3 with the arrow head's - ;; points. Use a turtle-like movement to find the points. - ;; point3 is the point where the line should end. - (define/private (update-polygon from-x from-y to-x to-y) - (define (move tx ty ta d) (values (+ tx (* d (cos ta))) - (+ ty (* d (sin ta))) - ta)) - (define (turn tx ty ta a) (values tx - ty - (+ ta a))) - (define init-angle - (cond - [(and (from-x . = . to-x) - (from-y . < . to-y)) - (* pi 3/2)] - [(from-x . = . to-x) - (* pi 1/2)] - [(from-x . < . to-x) - (+ pi (atan (/ (- from-y to-y) (- from-x to-x))))] - [else - (atan (/ (- from-y to-y) (- from-x to-x)))])) - (let*-values ([(t1x t1y t1a) (values to-x to-y init-angle)] - [(t2x t2y t2a) (turn t1x t1y t1a (/ arrowhead-angle-width 2))] - [(t3x t3y t3a) (move t2x t2y t2a arrowhead-long-side)] - [(t4x t4y t4a) (turn t1x t1y t1a (- (/ arrowhead-angle-width 2)))] - [(t5x t5y t5a) (move t4x t4y t4a arrowhead-long-side)] - [(t6x t6y t6a) (move t1x t1y t1a arrowhead-short-side)]) - (send point1 set-x t1x) - (send point1 set-y t1y) - (send point2 set-x t3x) - (send point2 set-y t3y) - (send point3 set-x t6x) - (send point3 set-y t6y) - (send point4 set-x t5x) - (send point4 set-y t5y))) - ;; HERE!!! - - (define/private (should-hilite? snip) - (let ([check-one-way - (lambda (way) - (let loop ([snip snip]) - (or (memq snip currently-overs) - (and (is-a? snip graph-snip<%>) - (loop (car (way snip)))))))]) - (or (check-one-way (lambda (snip) (send snip get-children))) - (check-one-way (lambda (snip) (send snip get-parents)))))) - - (inherit get-snip-location) - (field [lb (box 0)] - [tb (box 0)] - [rb (box 0)] - [bb (box 0)]) - (define/private (get-position snip) - (get-snip-location snip lb tb #f) - (get-snip-location snip rb bb #t) - (values (unbox lb) - (unbox tb) - (- (unbox rb) (unbox lb)) - (- (unbox bb) (unbox tb)))) - - (super-new))) - - ;; in-rectangle? : number^2 number^2 number^2 -> boolean - ;; determines if (x,y) is in the rectangle described - ;; by (p1x,p1y) and (p2x,p2y). - (define (in-rectangle? x y p1x p1y p2x p2y) - (and (<= (min p1x p2x) x (max p1x p2x)) - (<= (min p1y p2y) y (max p1y p2y)))) - - ;; strict-in-rectangle? : number^2 number^2 number^2 -> boolean - ;; determines if (x,y) is in the rectangle described - ;; by (p1x,p1y) and (p2x,p2y), but not on the border - (define (strict-in-rectangle? x y p1x p1y p2x p2y) - (and (< (min p1x p2x) x (max p1x p2x)) - (< (min p1y p2y) y (max p1y p2y)))) - - ;; find-intersection : number^8 -> (values (union #f number) (union #f number)) - ;; calculates the intersection between two line segments, - ;; described as pairs of points. Returns #f if they do not intersect - (define (find-intersection x1 y1 x2 y2 x3 y3 x4 y4) - (let-values ([(m1 b1) (find-mb x1 y1 x2 y2)] - [(m2 b2) (find-mb x3 y3 x4 y4)]) - (let-values ([(int-x int-y) - (cond - [(and m1 m2 b1 b2 - (= m1 0) - (= m2 0)) - (values #f #f)] - [(and m1 m2 b1 b2 - (= m1 0)) - (let* ([y y1] - [x (/ (- y b2) m2)]) - (values x y))] - [(and m1 m2 b1 b2 - (= m2 0)) - (let* ([y y3] - [x (/ (- y b1) m1)]) - (values x y))] - [(and m1 m2 b1 b2 - (not (= m1 m2))) - (let* ([y (/ (- b2 b1) (- m1 m2))] - [x (/ (- y b1) m1)]) - (values x y))] - [(and m1 b1) - (let* ([x x3] - [y (+ (* m1 x) b1)]) - (values x y))] - [(and m2 b2) - (let* ([x x1] - [y (+ (* m2 x) b2)]) - (values x y))] - [else - (values #f #f)])]) - - (if (and int-x - int-y - (<= (min x1 x2) int-x (max x1 x2)) - (<= (min y1 y2) int-y (max y1 y2)) - (<= (min x3 x4) int-x (max x3 x4)) - (<= (min y3 y4) int-y (max y3 y4))) - (values int-x int-y) - (values #f #f))))) - - ;; find-mb : number number number number -> (values (union #f number) (union #f number)) - ;; finds the "m" and "b" constants that describe the - ;; lines from (x1, y1) to (x2, y2) - (define (find-mb x1 y1 x2 y2) - (if (= x1 x2) - (values #f #f) - (let-values ([(xl yl xr yr) - (if (x1 . <= . x2) - (values x1 y1 x2 y2) - (values x2 y2 x1 y1))]) - (let* ([m (/ (- yr yl) (- xr xl))] - [b (- y1 (* m x1))]) - (values m b))))) - - ;; get-all-relatives : (snip -> (listof snip)) snip -> (listof snip) - ;; returns all editor-snip relatives (of a particular sort), including - ;; any regular snip relatives along the way. - (define (get-all-relatives get-relatives snip) - (let loop ([flat-relatives (get-relatives snip)] - [relatives null]) - (cond - [(null? flat-relatives) relatives] - [else - (let i-loop ([dummy (car flat-relatives)] - [acc relatives]) - (cond - [(is-a? dummy graph-snip<%>) - (loop (cdr flat-relatives) (cons dummy acc))] - [else - (i-loop (car (get-relatives dummy)) - (cons dummy acc))]))]))) - - ;; get-all-children : snip -> (listof snip) - (define (get-all-children snip) - (get-all-relatives (lambda (snip) (send snip get-children)) snip)) - - ;; get-all-parents : snip -> (listof snip) - (define (get-all-parents snip) - (get-all-relatives (lambda (snip) (send snip get-parents)) snip))) - diff --git a/collects/reduction-semantics/gui.ss b/collects/reduction-semantics/gui.ss deleted file mode 100644 index 8e465fdef9..0000000000 --- a/collects/reduction-semantics/gui.ss +++ /dev/null @@ -1,565 +0,0 @@ -;; should cache the count of new snips -- dont -;; use `count-snips'; use something associated with the -;; equal hash-table - -(module gui mzscheme - (require (lib "etc.ss") - (lib "graph.ss" "reduction-semantics") - "reduction-semantics.ss" - (lib "mred.ss" "mred") - (lib "framework.ss" "framework") - (lib "pretty.ss") - (lib "class.ss") - (lib "contract.ss") - (lib "list.ss") - (lib "match.ss")) - - (provide/contract - [traces (opt-> (compiled-lang? - (listof red?) - any/c) - (procedure? (listof any/c)) - any)] - [traces/pred (opt-> (compiled-lang? - (listof red?) - (listof any/c) - (any/c . -> . boolean?)) - (procedure? (listof any/c)) - any)] - [traces/multiple (opt-> (compiled-lang? - (listof red?) - (listof any/c)) - (procedure? (listof any/c)) - any)]) - - - (provide reduction-steps-cutoff initial-font-size initial-char-width - dark-pen-color light-pen-color dark-brush-color light-brush-color - dark-text-color light-text-color - (rename default-pp default-pretty-printer)) - - (preferences:set-default 'plt-reducer:show-bottom #t boolean?) - - (define dark-pen-color (make-parameter "blue")) - (define light-pen-color (make-parameter "lightblue")) - (define dark-brush-color (make-parameter "lightblue")) - (define light-brush-color (make-parameter "white")) - (define dark-text-color (make-parameter "blue")) - (define light-text-color (make-parameter "lightblue")) - - - ;; after (about) this many steps, stop automatic, initial reductions - (define reduction-steps-cutoff (make-parameter 20)) - - - - (define initial-font-size - (make-parameter - (send (send (send (editor:get-standard-style-list) - find-named-style - "Standard") - get-font) - get-point-size))) - - (define initial-char-width (make-parameter 30)) - - ;; the initial spacing between row and columns of the reduction terms - (define x-spacing 15) - (define y-spacing 15) - - (define (default-pp v port w spec) - (parameterize ([pretty-print-columns w]) - (pretty-print v port))) - - (define traces - (opt-lambda (lang reductions expr [pp default-pp] [colors '()]) - (traces/multiple lang reductions (list expr) pp colors))) - - (define traces/multiple - (opt-lambda (lang reductions exprs [pp default-pp] [colors '()]) - (traces/pred lang reductions exprs (lambda (x) #t) pp colors))) - - (define traces/pred - (opt-lambda (lang reductions exprs pred [pp default-pp] [colors '()]) - (define main-eventspace (current-eventspace)) - (define graph-pb (make-object graph-pasteboard%)) - (define f (instantiate red-sem-frame% () - (label "Reduction Graph") - (graph-pb graph-pb) - (width 600) - (height 400) - (toggle-panel-callback - (lambda () - (send remove-my-contents-panel - change-children - (lambda (l) - (preferences:set 'plt-reducer:show-bottom (null? l)) - (if (null? l) - (list bottom-panel) - null))))))) - (define ec (make-object editor-canvas% (send f get-area-container) graph-pb)) - (define remove-my-contents-panel (new vertical-panel% - (parent (send f get-area-container)) - (stretchable-height #f))) - (define bottom-panel (new vertical-panel% - (parent remove-my-contents-panel) - (stretchable-height #f))) - (define font-size (instantiate slider% () - (label "Font Size") - (min-value 1) - (init-value (initial-font-size)) - (max-value 127) - (parent bottom-panel) - (callback (lambda (slider evt) (set-font-size (send slider get-value)))))) - (define lower-panel (instantiate horizontal-panel% () - (parent bottom-panel) - (stretchable-height #f))) - (define reduce-button (make-object button% - "Reducing..." - lower-panel - (lambda (x y) - (reduce-button-callback)))) - (define status-message (instantiate message% () - (label "") - (parent lower-panel) - (stretchable-width #t))) - - (define snip-cache (make-hash-table 'equal)) - - ;; call-on-eventspace-main-thread : (-> any) -> any - ;; =reduction thread= - (define (call-on-eventspace-main-thread thnk) - (parameterize ([current-eventspace main-eventspace]) - (let ([s (make-semaphore 0)] - [ans #f]) - (queue-callback - (lambda () - (set! ans (thnk)) - (semaphore-post s))) - (semaphore-wait s) - ans))) - - ;; only changed on the reduction thread - ;; frontier : (listof (is-a?/c graph-editor-snip%)) - (define frontier (map (lambda (expr) (build-snip snip-cache #f expr pred pp - (dark-pen-color) (light-pen-color) - (dark-text-color) (light-text-color) #f)) - exprs)) - - ;; set-font-size : number -> void - ;; =eventspace main thread= - (define (set-font-size size) - (let* ([scheme-standard (send (editor:get-standard-style-list) find-named-style - "Standard")] - [scheme-delta (make-object style-delta%)]) - (send scheme-standard get-delta scheme-delta) - (send scheme-delta set-size-mult 0) - (send scheme-delta set-size-add size) - (send scheme-standard set-delta scheme-delta))) - - ;; color-spec-list->color-scheme : (list (union string? #f)^4) -> (list string?^4) - ;; converts a list of user-specified colors (including false) into a list of color strings, filling in - ;; falses with the default colors - (define (color-spec-list->color-scheme l) - (map (λ (c d) (or c d)) - l - (list (dark-pen-color) (light-pen-color) (dark-text-color) (light-text-color)))) - - - (define name->color-ht - (let ((ht (make-hash-table 'equal))) - (for-each - (λ (c) - (hash-table-put! ht (car c) - (color-spec-list->color-scheme - (match (cdr c) - [(color) - (list color color (dark-text-color) (light-text-color))] - [(dark-arrow-color light-arrow-color) - (list dark-arrow-color light-arrow-color (dark-text-color) (light-text-color))] - [(dark-arrow-color light-arrow-color text-color) - (list dark-arrow-color light-arrow-color text-color text-color)] - [(_ _ _ _) - (cdr c)])))) - colors) - ht)) - - ;; red->colors : reduction -> (values string string string string) - (define (red->colors red) - (apply values (hash-table-get name->color-ht (reduction->name red) - (λ () (list (dark-pen-color) (light-pen-color) (dark-text-color) (light-text-color)))))) - - ;; reduce-frontier : -> void - ;; =reduction thread= - ;; updates frontier with the new snip after a single reduction - (define (reduce-frontier) - (let ([col #f]) - (let loop ([snips frontier] - [new-frontier null] - [y 0]) - (cond - [(null? snips) - (set! frontier new-frontier)] - [else - (let* ([snip (car snips)] - [new-snips - (filter - (lambda (x) x) - (map (lambda (red+sexp) - (let-values ([(red sexp) (apply values red+sexp)]) - (call-on-eventspace-main-thread - (λ () - (let-values ([(dark-arrow-color light-arrow-color dark-label-color light-label-color) (red->colors red)]) - (build-snip snip-cache snip sexp pred pp light-arrow-color dark-arrow-color dark-label-color light-label-color - (reduction->name red))))))) - (reduce/tag-with-reduction reductions (send snip get-expr))))] - [new-y - (call-on-eventspace-main-thread - (lambda () ; =eventspace main thread= - (send graph-pb begin-edit-sequence) - (unless col ;; only compute col here, incase user moves snips - (set! col (+ x-spacing (find-rightmost-x graph-pb)))) - (begin0 - (insert-into col y graph-pb new-snips) - (send graph-pb end-edit-sequence) - (send status-message set-label - (string-append (term-count (count-snips)) "...")))))]) - (loop (cdr snips) - (append new-frontier new-snips) - new-y))])))) - - ;; count-snips : -> number - ;; =eventspace main thread= - ;; counts the snips in `pb'. If connections? - ;; is #t, also counts the number of connections - ;; and returns the sum of the connections and snips - (define (count-snips) - (let loop ([n 0] - [snip (send graph-pb find-first-snip)]) - (cond - [snip (loop (+ n 1) (send snip next))] - [else n]))) - - ;; reduce-button-callback : -> void - ;; =eventspace main thread= - (define (reduce-button-callback) - (send reduce-button enable #f) - (send reduce-button set-label "Reducing...") - (thread - (lambda () - (do-some-reductions) - (queue-callback - (lambda () ;; =eventspace main thread= - (scroll-to-rightmost-snip) - (send reduce-button set-label "Reduce") - (cond - [(null? frontier) - (send status-message set-label (term-count (count-snips)))] - [else - (send status-message set-label - (string-append (term-count (count-snips)) - "(possibly more to find)")) - (send reduce-button enable #t)])))))) - - (define (term-count n) - (format "found ~a term~a" n (if (equal? n 1) "" "s"))) - - ;; do-some-reductions : -> void - ;; =reduction thread= - ;; reduces some number of times, - ;; adding at least reduction-steps-cutoff steps - ;; before stopping (unless there aren't that many left) - (define (do-some-reductions) - (let ([initial-size (call-on-eventspace-main-thread count-snips)]) - (let loop () - (cond - [(null? frontier) (void)] - [((call-on-eventspace-main-thread count-snips) . >= . (+ initial-size (reduction-steps-cutoff))) - (void)] - [else - (reduce-frontier) - (loop)])))) - - ;; scroll-to-rightmost-snip : -> void - ;; =eventspace main thread= - (define (scroll-to-rightmost-snip) - (let ([rightmost-snip (send graph-pb find-first-snip)]) - (let loop ([rightmost-snip rightmost-snip] - [rightmost-y (get-right-edge rightmost-snip)] - [snip (send rightmost-snip next)]) - (cond - [(not snip) (make-snip-visible rightmost-snip)] - [else - (let ([snip-y (get-right-edge snip)]) - (if (<= rightmost-y snip-y) - (loop snip snip-y (send snip next)) - (loop rightmost-snip rightmost-y (send snip next))))])))) - - ;; make-snip-visisble : snip -> void - ;; =eventspace-main-thread= - (define (make-snip-visible snip) - (let ([bl (box 0)] - [bt (box 0)] - [br (box 0)] - [bb (box 0)]) - (send graph-pb get-snip-location snip bl bt #f) - (send graph-pb get-snip-location snip br bb #t) - (send graph-pb scroll-to - snip - 0 - 0 - (- (unbox br) (unbox bl)) - (- (unbox bb) (unbox bt)) - #t))) - - ;; get-right-edge : snip -> void - ;; =eventspace-main-thread= - (define (get-right-edge snip) - (let ([br (box 0)]) - (send graph-pb get-snip-location snip br #f #t) - (unbox br))) - - (send remove-my-contents-panel - change-children - (lambda (l) - (if (preferences:get 'plt-reducer:show-bottom) - (list bottom-panel) - null))) - (insert-into init-rightmost-x 0 graph-pb frontier) - (set-font-size (initial-font-size)) - (reduce-button-callback) - (send f show #t))) - - (define red-sem-frame% - (class (frame:standard-menus-mixin (frame:basic-mixin frame%)) - (init-field graph-pb toggle-panel-callback) - (define/override (file-menu:create-save?) #f) - (define/override (file-menu:between-save-as-and-print file-menu) - (make-object menu-item% "Print..." - file-menu - (lambda (item evt) (send graph-pb print))) - (make-object menu-item% "Export as Encapsulted PostScript..." - file-menu - (lambda (item evt) (send graph-pb print #t #f 'postscript this #f))) - (make-object menu-item% "Export as PostScript..." - file-menu - (lambda (item evt) (send graph-pb print #t #f 'postscript this))) - (make-object menu-item% - "Toggle bottom stuff" - file-menu - (lambda (item evt) (toggle-panel-callback)))) - (super-instantiate ()))) - - (define (resizing-pasteboard-mixin pb%) - (class pb% - - (define/augment (on-interactive-resize snip) - (when (is-a? snip reflowing-snip<%>) - (send snip reflow-program)) - #;(super on-interactive-resize snip)) - - (define/augment (after-interactive-resize snip) - (when (is-a? snip reflowing-snip<%>) - (send snip reflow-program)) - #;(super after-interactive-resize snip)) - - (define/override (interactive-adjust-resize snip w h) - (super interactive-adjust-resize snip w h) - (when (is-a? snip reflowing-snip<%>) - (send snip reflow-program))) - (super-instantiate ()))) - - (define reflowing-snip<%> - (interface () - reflow-program)) - - (define graph-pasteboard% - (resizing-pasteboard-mixin - (graph-pasteboard-mixin pasteboard%))) - - (define graph-editor-snip% - (class* (graph-snip-mixin editor-snip%) (reflowing-snip<%>) - (init-field expr pp char-width bad?) - (define/public (get-expr) expr) - - (inherit get-editor) - (define/public (reflow-program) - (let ([ed (get-editor)]) - (when ed - (let ([ed-ad (send ed get-admin)]) - (when ed-ad - (let ([dc (send ed get-dc)] - [wb (box 0)] - [std-style (send (editor:get-standard-style-list) find-named-style "Standard")]) - (send ed-ad get-view #f #f wb #f) - (let-values ([(tw _1 _2 _3) (send dc get-text-extent "w" - (and std-style - (send std-style get-font)))]) - (let ([new-width (max 1 (inexact->exact (floor (/ (- (unbox wb) 2) tw))))]) - (unless (equal? new-width char-width) - (set! char-width new-width) - (format-expr)))))))))) - - (inherit get-extent) - (define/override (draw dc x y left top right bottom dx dy draw-caret) - (when bad? - (let ([bw (box 0)] - [bh (box 0)] - [pen (send dc get-pen)] - [brush (send dc get-brush)]) - (get-extent dc x y bw bh #f #f #f #f) - (send dc set-pen (send the-pen-list find-or-create-pen bad-color 1 'solid)) - (send dc set-brush (send the-brush-list find-or-create-brush bad-color 'solid)) - (send dc draw-rectangle x y (unbox bw) (unbox bh)) - (send dc set-pen pen) - (send dc set-brush brush))) - (super draw dc x y left top right bottom dx dy draw-caret)) - - (define/public (format-expr) - (let* ([text (get-editor)] - [port (make-output-port - 'graph-port - always-evt - (lambda (bytes start end buffering? enable-breaks?) - (send text insert (bytes->string/utf-8 (subbytes bytes start end)) - (send text last-position) - (send text last-position)) - (- end start)) - void)]) - (send text begin-edit-sequence) - (send text thaw-colorer) - (send text set-styles-sticky #f) - (send text erase) - (pp expr port char-width text) - (when (char=? #\newline (send text get-character (- (send text last-position) 1))) - (send text delete (- (send text last-position) 1) (send text last-position))) - (send text freeze-colorer) - (when bad? - (send text change-style bad-style-delta 0 (send text last-position))) - (send text end-edit-sequence))) - - (super-instantiate ()))) - - (define program-text% - (class scheme:text% - (init-field bad?) - (define/override (on-paint before? dc left top right bottom dx dy draw-caret) - (when (and bad? before?) - (let ([pen (send dc get-pen)] - [brush (send dc get-brush)]) - (send dc set-pen (send the-pen-list find-or-create-pen bad-color 1 'solid)) - (send dc set-brush (send the-brush-list find-or-create-brush bad-color 'solid)) - (send dc draw-rectangle (+ dx left) (+ dy top) (- right left) (- bottom top)) - (send dc set-pen pen) - (send dc set-brush brush))) - (super on-paint before? dc left top right bottom dx dy draw-caret)) - (super-new))) - - (define lines-pen (send the-pen-list find-or-create-pen "black" 1 'solid)) - (define bad-style-delta (make-object style-delta% 'change-italic)) - (define bad-color "pink") - - ;; where the first snips are inserted - (define init-rightmost-x 25) - - ;; insert-into : number number pasteboard (listof snip%) -> number - ;; inserts the snips into the pasteboard vertically - ;; aligned, starting at (x,y). Returns - ;; the y coordinate where another snip might be inserted. - (define (insert-into x y pb exprs) - (let loop ([exprs exprs] - [y y]) - (cond - [(null? exprs) y] - [else - (let ([es (car exprs)]) - (send pb insert es x y) - (loop (cdr exprs) - (+ y (find-snip-height pb es) y-spacing)))]))) - - ;; build-snip : hash-table - ;; (union #f (is-a?/c graph-snip<%>)) - ;; sexp - ;; sexp -> boolean - ;; (any port number -> void) - ;; color - ;; (union #f string) - ;; -> (union #f (is-a?/c graph-editor-snip%)) - ;; returns #f if a snip corresponding to the expr has already been created. - ;; also adds in the links to the parent snip - ;; =eventspace main thread= - (define (build-snip cache parent-snip expr pred pp light-arrow-color dark-arrow-color dark-label-color light-label-color label) - (let-values ([(snip new?) - (let/ec k - (k - (hash-table-get - cache - expr - (lambda () - (let ([new-snip (make-snip parent-snip expr pred pp)]) - (hash-table-put! cache expr new-snip) - (k new-snip #t)))) - #f))]) - (when parent-snip - (add-links/text-colors parent-snip snip - (send the-pen-list find-or-create-pen dark-arrow-color 0 'solid) - (send the-pen-list find-or-create-pen light-arrow-color 0 'solid) - (send the-brush-list find-or-create-brush (dark-brush-color) 'solid) - (send the-brush-list find-or-create-brush (light-brush-color) 'solid) - (make-object color% dark-label-color) - (make-object color% light-label-color) - 0 0 - label)) - (and new? snip))) - - ;; make-snip : (union #f (is-a?/c graph-snip<%>)) - ;; sexp - ;; sexp -> boolean - ;; (any port number -> void) - ;; -> (is-a?/c graph-editor-snip%) - ;; unconditionally creates a new graph-editor-snip - ;; =eventspace main thread= - (define (make-snip parent-snip expr pred pp) - (let* ([bad? (not (pred expr))] - [text (new program-text% (bad? bad?))] - [es (instantiate graph-editor-snip% () - (char-width (initial-char-width)) - (editor text) - (pp - (if (procedure-arity-includes? pp 4) - pp - (lambda (v port w spec) (display (pp v) port)))) - (expr expr) - (bad? bad?))]) - (send text set-autowrap-bitmap #f) - (send text freeze-colorer) - (send es format-expr) - es)) - - ;; find-rightmost-x : pasteboard -> number - (define (find-rightmost-x pb) - (let ([first-snip (send pb find-first-snip)]) - (if first-snip - (let loop ([snip first-snip] - [max-x (find-snip-right-edge pb first-snip)]) - (cond - [snip - (loop (send snip next) - (max max-x (find-snip-right-edge pb snip)))] - [else max-x])) - init-rightmost-x))) - - ;; find-snip-right-edge : editor snip -> number - (define (find-snip-right-edge ed snip) - (let ([br (box 0)]) - (send ed get-snip-location snip br #f #t) - (unbox br))) - - ;; find-snip-height : editor snip -> number - (define (find-snip-height ed snip) - (let ([bt (box 0)] - [bb (box 0)]) - (send ed get-snip-location snip #f bt #f) - (send ed get-snip-location snip #f bb #t) - (- (unbox bb) - (unbox bt))))) diff --git a/collects/reduction-semantics/helper.ss b/collects/reduction-semantics/helper.ss deleted file mode 100644 index e34fc3f1ea..0000000000 --- a/collects/reduction-semantics/helper.ss +++ /dev/null @@ -1,206 +0,0 @@ -(module helper mzscheme - (require (lib "contract.ss") - "reduction-semantics.ss") - - (define counter 0) - (define (generate-string) - (set! counter (add1 counter)) - (format "s~a" counter)) - - (define (unique-names? l) - (let ([ht (make-hash-table)]) - (andmap (lambda (n) - (if (hash-table-get ht n (lambda () #f)) - #f - (begin - (hash-table-put! ht n #t) - #t))) - l))) - - (define (all-of P ?) - ;; Traverse P as an sexp, and look for class-name uses: - (let ([l (let loop ([sexp P]) - (cond - [(? sexp) (list sexp)] - [(pair? sexp) (append (loop (car sexp)) (loop (cdr sexp)))] - [else null]))] - [ht (make-hash-table)]) - ;; Filter duplicates by hashing: - (for-each (lambda (i) (hash-table-put! ht i #t)) l) - (hash-table-map ht (lambda (k v) k)))) - - (define-syntaxes (lang-match-lambda* - lang-match-lambda-memoized* - lang-match-lambda - lang-match-lambda-memoized) - (let ([generic - (lambda (lam) - (lambda (stx) - (syntax-case stx () - [(_ (id ...) main-id grammar [pattern result] ...) - (with-syntax ([red (generate-temporaries #'(pattern ...))] - [lam lam] - [ids #'(id ...)]) - (syntax/loc - stx - (let ([lang grammar] - [escape (make-parameter void)]) - (let ([reds (list (reduction grammar pattern ((escape) (lambda ids result))) - ...)]) - (lam (id ...) - ((let/ec esc - (parameterize ([escape esc]) - (reduce reds main-id) - (error 'lang-match-lambda "no pattern matched input: ~e" main-id))) - id ...))))))])))] - [single - (lambda (multi) - (lambda (stx) - (syntax-case stx () - [(_ (id) grammar [pattern result] ...) - (with-syntax ([multi multi]) - #'(multi (id) id grammar [pattern result] ...))])))]) - (values - (generic #'lambda) - (generic #'lambda-memoized) - (single #'lang-match-lambda*) - (single #'lang-match-lambda-memoized*)))) - - (define (transitive-closure orig) - ;; Copy initial mapping: - (let ([map (map (lambda (p) (list (car p) (cdr p))) orig)]) - ;; Extend the map list until nothing changes - (let loop () - (let ([changed? #f]) - (for-each (lambda (pair) - (let ([mapping (cdr pair)]) - (for-each (lambda (item) - (let ([trans (ormap (lambda (transitive) - (and (not (memq transitive mapping)) - transitive)) - (cdr (assq item map)))]) - (when trans - (append! pair (list trans)) - (set! changed? #t)))) - mapping))) - map) - (when changed? (loop)))) - ;; Done - map)) - - (define-syntax (lambda-memoized stx) - (syntax-case stx () - [(_ () body1 body ...) - (syntax/loc stx (lambda () body1 body ...))] - [(_ (arg) body1 body ...) - (syntax/loc - stx - (let ([ht (make-hash-table 'weak)]) - (lambda (arg) - (hash-table-get - ht - arg - (lambda () - (let ([v (begin body1 body ...)]) - (hash-table-put! ht arg v) - v))))))] - [(_ (arg1 arg ...) body1 body ...) - (syntax/loc - stx - (let ([memo (lambda-memoized (arg1) (lambda-memoized (arg ...) body1 body ...))]) - (lambda (arg1 arg ...) - ((memo arg1) arg ...))))])) - - (define-syntax define-memoized - (syntax-rules () - [(_ (f . args) body1 body ...) - (define f (lambda-memoized args body1 body ...))])) - - - ;; function-reduce* - (define (function-reduce* reds expr done? max-steps) - (cons - expr - (if (or (zero? max-steps) (done? expr)) - null - (let ([l (reduce reds expr)]) - (cond - [(null? l) null] - [(= 1 (length l)) - (function-reduce* reds (car l) done? (sub1 max-steps))] - [else - (error 'function-reduce* - "found ~a possible steps from ~e" - (length l) - expr)]))))) - - (define-struct multi-result (choices)) - - ;; ---------------------------------------- - ;; Path exploration: - - (define-syntax (explore-results stx) - (syntax-case stx () - [(_ (id) result-expr body-expr bes ...) - #'(let ([try (lambda (id) body-expr bes ...)]) - (let ([r result-expr]) - (do-explore r try)))])) - - (define-syntax (explore-parallel-results stx) - (syntax-case stx () - [(_ (list-id) result-list-expr body-expr bes ...) - #'(let ([try (lambda (list-id) body-expr bes ...)]) - (let loop ([rs result-list-expr][es null]) - (if (null? rs) - (try (reverse es)) - (do-explore - (car rs) - (lambda (e) - (loop (cdr rs) (cons e es)))))))])) - - (define (do-explore r try) - (cond - [(multi-result? r) - (let loop ([l (multi-result-choices r)]) - (if (null? l) - #f - (let ([a ((car l))]) - (if (multi-result? a) - (loop (append (multi-result-choices a) - (cdr l))) - (let ([v (try a)]) - (if (not v) - (loop (cdr l)) - (make-multi-result - (append (if (multi-result? v) - (multi-result-choices v) - (list (lambda () v))) - (list (lambda () (loop (cdr l))))))))))))] - [else (try r)])) - - (define (many-results l) - (make-multi-result (map (lambda (v) (lambda () v)) l))) - - (define (first-result result) - (let/ec k - (explore-results (x) result - (k x)))) - - (provide - define-memoized - lambda-memoized - lang-match-lambda - lang-match-lambda-memoized - lang-match-lambda* - lang-match-lambda-memoized* - explore-results - explore-parallel-results) - (provide/contract - (function-reduce* ((listof red?) any/c (any/c . -> . boolean?) number? - . -> . (listof any/c))) - (unique-names? ((listof symbol?) . -> . boolean?)) - (generate-string (-> string?)) - (all-of (any/c (any/c . -> . any) . -> . (listof any/c))) - (transitive-closure ((listof pair?) . -> . (listof (listof any/c)))) - (many-results ((listof (lambda (x) (not (multi-result? x)))) . -> . any)) - (first-result (any/c . -> . any)))) diff --git a/collects/reduction-semantics/info.ss b/collects/reduction-semantics/info.ss deleted file mode 100644 index 8a3833adfd..0000000000 --- a/collects/reduction-semantics/info.ss +++ /dev/null @@ -1,4 +0,0 @@ -(module info (lib "infotab.ss" "setup") - (define name "PLT Redex") - (define doc.txt "doc.txt")) - diff --git a/collects/reduction-semantics/mc.ss b/collects/reduction-semantics/mc.ss deleted file mode 100644 index 827dd28992..0000000000 --- a/collects/reduction-semantics/mc.ss +++ /dev/null @@ -1,376 +0,0 @@ - -(module mc mzscheme - (require (lib "reduction-semantics.ss" "reduction-semantics") - (lib "generator.ss" "reduction-semantics") - (prefix matcher: (lib "matcher.ss" "reduction-semantics" "private")) - (lib "list.ss") - (lib "class.ss") - (lib "mred.ss" "mred")) - - (provide build-reductions - generation-depth - reduction-depth - generate-and-test - (struct reduction-graph (initial ht))) - - ;; reduction-graph = (make-graph sexp hash-table[sexp -o> (listof sexp)]) - (define-struct reduction-graph (initial ht)) - - (define generation-depth (make-parameter 2)) - (define reduction-depth (make-parameter 10)) - (define max-queue-size 100) - - ;; computes all of the terms of size `n' or smaller for each non-terminal - ;; in the language - ;; [ sizes are limited by number of recusive constructions of each non terminal; - ;; 4 is huge for even tiny languages ] - (define (generate-and-test lang nt reductions reductions-test) - - (define frame (make-object frame% "Status")) - (define gc-on-bitmap (make-object bitmap% (build-path (collection-path "icons") "recycle.gif"))) - (define gc-off-bitmap (make-object bitmap% - (send gc-on-bitmap get-width) - (send gc-on-bitmap get-height) - #t)) - (define stupid-internal-define-syntax1 - (let ([bdc (make-object bitmap-dc% gc-off-bitmap)]) - (send bdc clear) - (send bdc set-bitmap #f))) - - (define-values (reductions-queue-size-message - total-reductions-message - test-queue-size-message - total-tests-message - memory-allocated-message) - (let* ([outer-hp (make-object horizontal-panel% frame)] - [outer-vp (make-object vertical-panel% outer-hp)] - [hp1 (make-object horizontal-panel% outer-vp)] - [hp2 (make-object horizontal-panel% outer-vp)] - [hp3 (make-object horizontal-panel% outer-vp)] - [hp4 (make-object horizontal-panel% outer-vp)] - [hp5 (make-object horizontal-panel% outer-vp)] - [l1 (make-object message% "To Reduce: " hp1)] - [l2 (make-object message% "Total Expressions: " hp2)] - [l3 (make-object message% "To Test: " hp3)] - [l4 (make-object message% "Total Tests: " hp4)] - [l5 (make-object message% "Megabytes Allocated: " hp5)] - [gc-canvas (instantiate canvas% () - (parent outer-hp) - (stretchable-width #f) - (stretchable-height #f) - (min-width (send gc-on-bitmap get-width)) - (min-height (send gc-on-bitmap get-height)))] - [dms-button (instantiate button% ("DMS" outer-hp) - [callback (lambda (b e) - (dump-memory-stats '))])]) - - (register-collecting-blit gc-canvas - 0 - 0 - (send gc-on-bitmap get-width) - (send gc-on-bitmap get-height) - gc-on-bitmap - gc-off-bitmap) - (let ([w (max (send l1 get-width) - (send l2 get-width) - (send l3 get-width) - (send l4 get-width) - (send l5 get-width))]) - (send l1 min-width w) - (send l2 min-width w) - (send l3 min-width w) - (send l4 min-width w) - (send l5 min-width w)) - - (values - (instantiate message% () - (label "0000000") - ;(stretchable-width #t) - (parent hp1)) - (instantiate message% () - (label "0000000") - ;(stretchable-width #t) - (parent hp2)) - (instantiate message% () - (label "0000000") - ;(stretchable-width #t) - (parent hp3)) - (instantiate message% () - (label "0000000") - ;(stretchable-width #t) - (parent hp4)) - (instantiate message% () - (label "0000000") - ;(stretchable-width #t) - (parent hp5))))) - - (define go (make-semaphore 0)) - - (define no-more-terms (box 'no-more-terms)) - - (define generation-thread - (thread - (lambda () - (semaphore-wait go) - (generate lang nt enqueue-for-reduction-thread) - (enqueue-for-reduction-thread no-more-terms)))) - - (define total-reductions 0) - (define reduction-queue (new-queue)) - (define reduction-queue-sema (make-semaphore 1)) - (define reduction-thread-sema (make-semaphore 0)) - (define reduction-producer-sema (make-semaphore max-queue-size)) - (define (enqueue-for-reduction-thread sexp) - (semaphore-wait reduction-producer-sema) - (semaphore-wait reduction-queue-sema) - (enqueue reduction-queue sexp) - (set! total-reductions (+ total-reductions 1)) - (semaphore-post reduction-thread-sema) - (semaphore-post reduction-queue-sema)) - - (define reduction-thread - (thread - (lambda () - (semaphore-wait go) - (let loop () - (semaphore-wait reduction-thread-sema) - (semaphore-wait reduction-queue-sema) - (let ([sexp (dequeue reduction-queue)]) - (semaphore-post reduction-queue-sema) - (semaphore-post reduction-producer-sema) - (cond - [(eq? sexp no-more-terms) - (enqueue-for-test-thread no-more-terms)] - [else - (enqueue-for-test-thread (build-reductions sexp reductions)) - (loop)])))))) - - (define total-tests 0) - (define test-queue (new-queue)) - (define test-queue-sema (make-semaphore 1)) - (define test-thread-sema (make-semaphore 0)) - (define test-producer-sema (make-semaphore max-queue-size)) - (define (enqueue-for-test-thread sexp) - (semaphore-wait test-producer-sema) - (semaphore-wait test-queue-sema) - (enqueue test-queue sexp) - (set! total-tests (+ total-tests 1)) - (semaphore-post test-thread-sema) - (semaphore-post test-queue-sema)) - - (define test-thread - (thread - (lambda () - (semaphore-wait go) - (let loop () - (semaphore-wait test-thread-sema) - (semaphore-wait test-queue-sema) - (let ([reds (dequeue test-queue)]) - (semaphore-post test-queue-sema) - (semaphore-post test-producer-sema) - (cond - [(eq? reds no-more-terms) - (semaphore-post done-semaphore)] - [else - (reductions-test reds)])) - (loop))))) - - (define mem-divisor (* 1024 1024)) - (define (update-status) - (send test-queue-size-message set-label (format "~a" (queue-size test-queue))) - (send total-tests-message set-label (format "~a" total-tests)) - (send reductions-queue-size-message set-label (format "~a" (queue-size reduction-queue))) - (send total-reductions-message set-label (format "~a" total-reductions)) - (send memory-allocated-message set-label (number->string (quotient (current-memory-use) mem-divisor)))) - - (define status-thread - (thread - (lambda () - (semaphore-wait go) - (with-handlers ([exn:break? (lambda (x) (semaphore-post status-thread-done))]) - (let loop () - (update-status) - (sleep 2) - (loop)))))) - - (define done-semaphore (make-semaphore 0)) - (define status-thread-done (make-semaphore 0)) - - (send frame show #t) - (semaphore-post go) - (semaphore-post go) - (semaphore-post go) - (semaphore-post go) - (yield done-semaphore) - (break-thread status-thread) - (semaphore-wait status-thread-done) - (update-status) - (make-object message% "Done." frame)) - - - -; -; -; -; ; ; ; -; ; ; -; ; ; ; -; ; ;; ;;; ;;; ; ; ; ;;;; ;;;; ; ;;;; ; ;;; ;;; ; ; ;; ;;; ; ;;; ; ;;; -; ;; ; ; ; ;; ; ; ; ; ; ; ; ;; ; ; ;; ;; ; ; ;; ; ;; ; -; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; -; ; ;;;;; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ;;;; ; ; ; ; -; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; -; ; ; ; ;; ; ;; ; ; ; ; ; ; ; ; ;; ; ; ; ;; ; ; ; -; ; ;;;; ;;; ; ;;; ; ;;;; ;; ; ;;;; ; ; ;;; ; ; ;;;;; ; ;;; ; ; -; ; ; -; ; ; ; -; ;;;; ; - - - ;; build-reductions : sexp (listof reductions) -> reduction-graph - ;; builds the reduction graph for expression according to reductions - (define (build-reductions expression reductions) - (let* ([ht (make-hash-table 'equal)] - [reduce/add - (lambda (term) - (let ([reduced (reduce reductions term)]) - (hash-table-put! ht term reduced) - (filter (lambda (term) - (not (hash-table-get ht term (lambda () #f)))) - reduced)))]) - (let loop ([frontier (list expression)] - [depth (reduction-depth)]) - (unless (zero? depth) - (let* ([new-terms (apply append (map reduce/add frontier))]) - (cond - [(null? new-terms) (void)] - [else - (loop new-terms (- depth 1))])))) - (make-reduction-graph expression ht))) - - - - -; -; -; -; ; -; -; ; -; ;;; ; ;;; ; ;;; ;;; ; ;; ;;; ;;;; ; ;;;; ; ;;; -; ; ;; ; ; ;; ; ; ; ;; ; ; ; ; ; ; ;; ; -; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; -; ; ; ;;;;; ; ; ;;;;; ; ;;;; ; ; ; ; ; ; -; ; ; ; ; ; ; ; ; ; ; ; ; ; ; ; -; ; ;; ; ; ; ; ; ; ; ; ; ; ; ; ; -; ;;; ; ;;;; ; ; ;;;; ; ;;;;; ;; ; ;;;; ; ; -; ; -; ; ; -; ;;;; - - - - ;; generate : lang sexp (sexp -> void) -> void - ;; generates the terms up to (generation-depth) in size - ;; passes each that comes from gdesired-nt to enqueue-for-reduction-thread - (define (generate lang desired-nt enqueue-for-reduction-thread) - (let ([gens (lang->generator-table lang - '(0 1) - '(x y) - '("a" "b") - null - 0)]) - (let loop ([n 0]) - (unless (n . > . (generation-depth)) - (for-each-generated/size (lambda (sexp size) - (enqueue-for-reduction-thread sexp)) - gens - n n desired-nt) - (loop (add1 n)))))) - - - ;; find-interesting-nts : (listof nt) sym -> (listof sym) - (define (find-interesting-nts clang desired-nt) - (let* ([lang (matcher:compiled-lang-lang clang)] - [ht (make-hash-table)] - [nt-syms (map matcher:nt-name lang)]) - (let loop ([nt-sym desired-nt]) - (let ([nt-lst (filter (lambda (x) (eq? (matcher:nt-name x) nt-sym)) lang)]) - (cond - [(null? nt-lst) (void)] - [(null? (cdr nt-lst)) - (let ([referenced-nt-syms (get-referenced-nts nt-syms (car nt-lst) lang)]) - (for-each - (lambda (referenced-nt-sym) - (unless (hash-table-get ht referenced-nt-sym (lambda () #f)) - (hash-table-put! ht referenced-nt-sym #t) - (loop referenced-nt-sym))) - referenced-nt-syms))] - [else (error 'mc.ss "found more than one definition of ~s in grammar" nt-sym)]))) - (hash-table-map ht (lambda (x y) x)))) - - (define (get-referenced-nts nt-syms nt lang) - (let loop ([rhss (matcher:nt-rhs nt)] - [refd-nts null]) - (cond - [(null? rhss) refd-nts] - [else (loop (cdr rhss) - (get-referenced-nts/rhs nt-syms (car rhss) refd-nts))]))) - - (define (get-referenced-nts/rhs nt-syms rhs acc) - (let loop ([pat (matcher:rhs-pattern rhs)] - [acc acc]) - (cond - [(null? pat) acc] - [(pair? pat) (loop (car pat) (loop (cdr pat) acc))] - [(symbol? pat) - (if (memq pat nt-syms) - (cons pat acc) - acc)]))) - - - - -; -; -; -; -; -; -; ;;; ; ; ; ;;; ; ; ;;; -; ; ;; ; ; ; ; ; ; ; ; -; ; ; ; ; ; ; ; ; ; ; -; ; ; ; ; ;;;;; ; ; ;;;;; -; ; ; ; ; ; ; ; ; -; ; ;; ; ;; ; ; ;; ; -; ;;; ; ;;; ; ;;;; ;;; ; ;;;; -; ; -; ; -; ; - - - - (define-struct queue (hd tl size)) - (define (new-queue) (make-queue null null 0)) - (define (enqueue queue thnk) - (set-queue-size! queue (+ (queue-size queue) 1)) - (let ([new-tail (cons thnk null)]) - (if (null? (queue-hd queue)) - (begin - (set-queue-hd! queue new-tail) - (set-queue-tl! queue new-tail)) - (begin - (set-cdr! (queue-tl queue) new-tail) - (set-queue-tl! queue new-tail))))) - (define (dequeue queue) - (when (null? (queue-hd queue)) - (error 'dequeue)) - (set-queue-size! queue (- (queue-size queue) 1)) - (let* ([qh (queue-hd queue)] - [fst (car qh)]) - (set-queue-hd! queue (cdr qh)) - (set-cdr! qh #f) - (when (null? (queue-hd queue)) - (set-queue-tl! queue null)) - fst)) - (define (queue-empty? queue) (null? (queue-hd queue)))) diff --git a/collects/reduction-semantics/private/info.ss b/collects/reduction-semantics/private/info.ss deleted file mode 100644 index d35132379f..0000000000 --- a/collects/reduction-semantics/private/info.ss +++ /dev/null @@ -1,2 +0,0 @@ -(module info (lib "infotab.ss" "setup") - (define name "Reduction Semantics private")) diff --git a/collects/reduction-semantics/private/make-plt.ss b/collects/reduction-semantics/private/make-plt.ss deleted file mode 100644 index dfb0232be9..0000000000 --- a/collects/reduction-semantics/private/make-plt.ss +++ /dev/null @@ -1,37 +0,0 @@ -(module make-plt mzscheme - (require (lib "file.ss") - (lib "pack.ss" "setup") - (lib "plthome.ss" "setup")) - - (current-directory plthome) - - (define (display-res f) - (lambda (x) - (let ([ans (f x)]) - (when ans - (printf "including ~s~n" x)) - ans))) - - (define bad-dirs '("CVS" ".svn")) - (define bad-files '(".DS_Store" "reduction-semantics.plt")) - - (pack (build-path "collects" "reduction-semantics" "reduction-semantics.plt") - "Reduction Semantics" - (list (build-path "collects" "reduction-semantics")) - '(("reduction-semantics")) - (display-res - (lambda (filename) - (let ([exp (reverse (explode-path (normalize-path filename)))]) - (cond - [(member (cadr exp) bad-dirs) - #f] - [(member (car exp) bad-dirs) - #f] - [(member (car exp) bad-files) - #f] - [(regexp-match #rx"~$" (path->string filename)) - #f] - [else - (std-filter filename)])))) - #t - 'file-replace)) diff --git a/collects/reduction-semantics/private/matcher-test.ss b/collects/reduction-semantics/private/matcher-test.ss deleted file mode 100644 index 0ef7d30a2a..0000000000 --- a/collects/reduction-semantics/private/matcher-test.ss +++ /dev/null @@ -1,634 +0,0 @@ -(module matcher-test mzscheme - (require "matcher.ss" - (lib "list.ss")) - - (define (make-test-mtch a b c) (make-mtch a (build-flat-context b) c)) - - (define (test) - (print-struct #t) - (test-empty 'any 1 (list (make-test-mtch (make-bindings null) 1 none))) - (test-empty 'any 'true (list (make-test-mtch (make-bindings null) 'true none))) - (test-empty 'any "a" (list (make-test-mtch (make-bindings null) "a" none))) - (test-empty 'any '(a b) (list (make-test-mtch (make-bindings null) '(a b) none))) - (test-empty 1 1 (list (make-test-mtch (make-bindings null) 1 none))) - (test-empty 1 '() #f) - (test-empty 99999999999999999999999999999999999999999999999 - 99999999999999999999999999999999999999999999999 - (list (make-test-mtch (make-bindings null) - 99999999999999999999999999999999999999999999999 - none))) - (test-empty 99999999999999999999999999999999999999999999999 - '() - #f) - (test-empty 'x 'x (list (make-test-mtch (make-bindings null) 'x none))) - (test-empty 'x '() #f) - (test-empty 1 2 #f) - (test-empty "a" "b" #f) - (test-empty "a" '(x) #f) - (test-empty "a" '() #f) - (test-empty "a" "a" (list (make-test-mtch (make-bindings null) "a" none))) - (test-empty 'number 1 (list (make-test-mtch (make-bindings null) 1 none))) - (test-empty 'number 'x #f) - (test-empty 'number '() #f) - (test-empty 'string "a" (list (make-test-mtch (make-bindings null) "a" none))) - (test-empty 'string 1 #f) - (test-empty 'string '() #f) - (test-empty 'variable 'x (list (make-test-mtch (make-bindings null) 'x none))) - (test-empty 'variable 1 #f) - (test-empty '(variable-except x) 1 #f) - (test-empty '(variable-except x) 'x #f) - (test-empty '(variable-except x) 'y (list (make-test-mtch (make-bindings null) 'y none))) - (test-empty 'hole 1 #f) - (test-empty '(hole hole-name) 1 #f) - (test-empty '(name x number) 1 (list (make-test-mtch (make-bindings (list (make-rib 'x 1))) 1 none))) - (test-empty 'number_x 1 (list (make-test-mtch (make-bindings (list (make-rib 'number_x 1))) 1 none))) - (test-empty 'string_y "b" (list (make-test-mtch (make-bindings (list (make-rib 'string_y "b"))) "b" none))) - (test-empty 'any_z '(a b) (list (make-test-mtch (make-bindings (list (make-rib 'any_z '(a b)))) '(a b) none))) - - (test-ellipses '(a) '(a)) - (test-ellipses '(a ...) `(,(make-repeat 'a '()))) - (test-ellipses '((a ...) ...) `(,(make-repeat '(a ...) '()))) - (test-ellipses '(a ... b c ...) `(,(make-repeat 'a '()) b ,(make-repeat 'c '()))) - (test-ellipses '((name x a) ...) `(,(make-repeat '(name x a) (list (make-rib 'x '()))))) - (test-ellipses '((name x (a ...)) ...) - `(,(make-repeat '(name x (a ...)) (list (make-rib 'x '()))))) - (test-ellipses '(((name x a) ...) ...) - `(,(make-repeat '((name x a) ...) (list (make-rib 'x '()))))) - (test-ellipses '((1 (name x a)) ...) - `(,(make-repeat '(1 (name x a)) (list (make-rib 'x '()))))) - (test-ellipses '((any (name x a)) ...) - `(,(make-repeat '(any (name x a)) (list (make-rib 'x '()))))) - (test-ellipses '((number (name x a)) ...) - `(,(make-repeat '(number (name x a)) (list (make-rib 'x '()))))) - (test-ellipses '((variable (name x a)) ...) - `(,(make-repeat '(variable (name x a)) (list (make-rib 'x '()))))) - (test-ellipses '(((name x a) (name y b)) ...) - `(,(make-repeat '((name x a) (name y b)) (list (make-rib 'y '()) (make-rib 'x '()))))) - (test-ellipses '((name x (name y b)) ...) - `(,(make-repeat '(name x (name y b)) (list (make-rib 'y '()) (make-rib 'x '()))))) - (test-ellipses '((in-hole (name x a) (name y b)) ...) - `(,(make-repeat '(in-hole (name x a) (name y b)) - (list (make-rib 'x '()) (make-rib 'y '()))))) - - (test-empty '() '() (list (make-test-mtch (make-bindings null) '() none))) - (test-empty '(a) '(a) (list (make-test-mtch (make-bindings null) '(a) none))) - (test-empty '(a) '(b) #f) - (test-empty '(a b) '(a b) (list (make-test-mtch (make-bindings null) '(a b) none))) - (test-empty '(a b) '(a c) #f) - (test-empty '() 1 #f) - (test-empty '(#f x) '(#f x) (list (make-test-mtch (make-bindings null) '(#f x) none))) - (test-empty '(#f (name y any)) '(#f) #f) - (test-empty '(in-hole (z hole) a) '(z a) (list (make-test-mtch (make-bindings (list)) '(z a) none))) - (test-empty '(in-hole (z hole) (in-hole (x hole) a)) - '(z (x a)) - (list (make-test-mtch (make-bindings (list)) '(z (x a)) none))) - - (test-empty '(in-named-hole h1 (z (hole h1)) a) - '(z a) - (list (make-test-mtch (make-bindings (list)) '(z a) none))) - - (test-empty '(in-named-hole h1 (z (hole h1)) a) '(z a) (list (make-test-mtch (make-bindings (list)) '(z a) none))) - (test-empty '(in-named-hole c (any (hole c)) y) - '(x y) - (list (make-test-mtch (make-bindings (list)) '(x y) none))) - (test-empty '(in-named-hole a (in-named-hole b (x (hole b)) (hole a)) y) - '(x y) - (list (make-test-mtch (make-bindings (list)) '(x y) none))) - (test-empty '(in-hole (in-hole (x hole) hole) y) - '(x y) - (list (make-test-mtch (make-bindings (list)) '(x y) none))) - - (test-empty '((name x number) (name x number)) '(1 1) (list (make-test-mtch (make-bindings (list (make-rib 'x 1))) '(1 1) none))) - (test-empty '((name x number) (name x number)) '(1 2) #f) - - (test-empty '(a ...) '() (list (make-test-mtch (make-bindings empty) '() none))) - (test-empty '(a ...) '(a) (list (make-test-mtch (make-bindings empty) '(a) none))) - (test-empty '(a ...) '(a a) (list (make-test-mtch (make-bindings empty) '(a a) none))) - (test-empty '((name x a) ...) '() (list (make-test-mtch (make-bindings (list (make-rib 'x '()))) '() none))) - (test-empty '((name x a) ...) '(a) (list (make-test-mtch (make-bindings (list (make-rib 'x '(a)))) '(a) none))) - (test-empty '((name x a) ...) '(a a) (list (make-test-mtch (make-bindings (list (make-rib 'x '(a a)))) '(a a) none))) - - (test-empty '(b ... a ...) '() (list (make-test-mtch (make-bindings empty) '() none))) - (test-empty '(b ... a ...) '(a) (list (make-test-mtch (make-bindings empty) '(a) none))) - (test-empty '(b ... a ...) '(b) (list (make-test-mtch (make-bindings empty) '(b) none))) - (test-empty '(b ... a ...) '(b a) (list (make-test-mtch (make-bindings empty) '(b a) none))) - (test-empty '(b ... a ...) '(b b a a) (list (make-test-mtch (make-bindings empty) '(b b a a) none))) - (test-empty '(b ... a ...) '(a a) (list (make-test-mtch (make-bindings empty) '(a a) none))) - (test-empty '(b ... a ...) '(b b) (list (make-test-mtch (make-bindings empty) '(b b) none))) - - (test-empty '((name y b) ... (name x a) ...) '() - (list (make-test-mtch (make-bindings (list (make-rib 'x '()) - (make-rib 'y '()))) - '() - none))) - (test-empty '((name y b) ... (name x a) ...) '(a) - (list (make-test-mtch (make-bindings (list (make-rib 'x '(a)) - (make-rib 'y '()))) - '(a) - none))) - (test-empty '((name y b) ... (name x a) ...) '(b) - (list (make-test-mtch (make-bindings (list (make-rib 'x '()) - (make-rib 'y '(b)))) - '(b) - none))) - (test-empty '((name y b) ... (name x a) ...) '(b b a a) - (list (make-test-mtch (make-bindings (list (make-rib 'x '(a a)) - (make-rib 'y '(b b)))) - '(b b a a) - none))) - (test-empty '((name y a) ... (name x a) ...) '(a) - (list (make-test-mtch (make-bindings (list (make-rib 'x '()) - (make-rib 'y '(a)))) - '(a) - none) - (make-test-mtch (make-bindings (list (make-rib 'x '(a)) - (make-rib 'y '()))) - '(a) - none))) - (test-empty '((name y a) ... (name x a) ...) '(a a) - (list (make-test-mtch (make-bindings (list (make-rib 'x '()) - (make-rib 'y '(a a)))) - '(a a) - none) - (make-test-mtch (make-bindings (list (make-rib 'x '(a)) - (make-rib 'y '(a)))) - '(a a) - none) - (make-test-mtch (make-bindings (list (make-rib 'x '(a a)) - (make-rib 'y '()))) - '(a a) - none))) - - (test-ab '(bb_y ... aa_x ...) '() - (list (make-test-mtch (make-bindings (list (make-rib 'aa_x '()) - (make-rib 'bb_y '()))) - '() - none))) - (test-ab '(bb_y ... aa_x ...) '(a) - (list (make-test-mtch (make-bindings (list (make-rib 'aa_x '(a)) - (make-rib 'bb_y '()))) - '(a) - none))) - (test-ab '(bb_y ... aa_x ...) '(b) - (list (make-test-mtch (make-bindings (list (make-rib 'aa_x '()) - (make-rib 'bb_y '(b)))) - '(b) - none))) - (test-ab '(bb_y ... aa_x ...) '(b b a a) - (list (make-test-mtch (make-bindings (list (make-rib 'aa_x '(a a)) - (make-rib 'bb_y '(b b)))) - '(b b a a) - none))) - (test-ab '(aa_y ... aa_x ...) '(a) - (list (make-test-mtch (make-bindings (list (make-rib 'aa_x '()) - (make-rib 'aa_y '(a)))) - '(a) - none) - (make-test-mtch (make-bindings (list (make-rib 'aa_x '(a)) - (make-rib 'aa_y '()))) - '(a) - none))) - (test-ab '(aa_y ... aa_x ...) '(a a) - (list (make-test-mtch (make-bindings (list (make-rib 'aa_x '()) - (make-rib 'aa_y '(a a)))) - '(a a) - none) - (make-test-mtch (make-bindings (list (make-rib 'aa_x '(a)) - (make-rib 'aa_y '(a)))) - '(a a) - none) - (make-test-mtch (make-bindings (list (make-rib 'aa_x '(a a)) - (make-rib 'aa_y '()))) - '(a a) - none))) - - (test-empty '((name x number) ...) '(1 2) (list (make-test-mtch (make-bindings (list (make-rib 'x '(1 2)))) '(1 2) none))) - - (test-empty '(a ...) '(b) #f) - (test-empty '(a ... b ...) '(c) #f) - (test-empty '(a ... b) '(b c) #f) - (test-empty '(a ... b) '(a b c) #f) - - (test-xab 'lsts '() (list (make-test-mtch (make-bindings null) '() none))) - (test-xab 'lsts '(x) (list (make-test-mtch (make-bindings null) '(x) none))) - (test-xab 'lsts 'x (list (make-test-mtch (make-bindings null) 'x none))) - (test-xab 'lsts #f (list (make-test-mtch (make-bindings null) #f none))) - (test-xab 'split-out '1 (list (make-test-mtch (make-bindings null) '1 none))) - - (test-xab 'exp 1 (list (make-test-mtch (make-bindings null) 1 none))) - (test-xab 'exp '(+ 1 2) (list (make-test-mtch (make-bindings null) '(+ 1 2) none))) - (test-xab '(in-hole ctxt any) - '1 - (list (make-test-mtch (make-bindings (list)) 1 none))) - (test-xab '(in-hole ctxt (name x any)) - '1 - (list (make-test-mtch (make-bindings (list (make-rib 'x 1))) 1 none))) - (test-xab '(in-hole (name c ctxt) (name x any)) - '(+ 1 2) - (list (make-test-mtch (make-bindings (list (make-rib 'c (build-context hole)) (make-rib 'x '(+ 1 2)))) '(+ 1 2) none) - (make-test-mtch (make-bindings (list (make-rib 'c (build-context `(+ ,hole 2))) - (make-rib 'x 1))) - '(+ 1 2) none) - (make-test-mtch (make-bindings (list (make-rib 'c (build-context `(+ 1 ,hole))) - (make-rib 'x 2))) '(+ 1 2) none))) - (test-xab '(in-hole (name c ctxt) (name i (+ number number))) - '(+ (+ 1 2) (+ 3 4)) - (list (make-test-mtch - (make-bindings (list (make-rib 'i '(+ 1 2)) (make-rib 'c (build-context `(+ ,hole (+ 3 4)))))) - '(+ (+ 1 2) (+ 3 4)) - none) - (make-test-mtch (make-bindings (list (make-rib 'i '(+ 3 4)) (make-rib 'c `(+ (+ 1 2) ,hole)))) - '(+ (+ 1 2) (+ 3 4)) - none))) - - (test-empty '(in-hole ((z hole)) (name x any)) - '((z a)) - (list (make-test-mtch (make-bindings (list (make-rib 'x 'a))) '((z a)) none))) - (test-empty '(in-hole (name c (z ... hole z ...)) any) - '(z z) - (list - (make-test-mtch (make-bindings (list (make-rib 'c `(z ,hole)))) '(z z) none) - (make-test-mtch (make-bindings (list (make-rib 'c `(,hole z)))) '(z z) none))) - (test-empty '(in-hole (name c (z ... hole z ...)) any) - '(z z z) - (list - (make-test-mtch (make-bindings (list (make-rib 'c `(z z ,hole)))) '(z z z) none) - (make-test-mtch (make-bindings (list (make-rib 'c `(z ,hole z)))) '(z z z) none) - (make-test-mtch (make-bindings (list (make-rib 'c `(,hole z z)))) '(z z z) none))) - - (test-empty '(z (in-hole (name c (z hole)) a)) - '(z (z a)) - (list - (make-test-mtch (make-bindings (list (make-rib 'c `(z ,hole)))) - '(z (z a)) - none))) - - (test-empty '(a (in-hole (name c1 (b (in-hole (name c2 (c hole)) d) hole)) e)) - '(a (b (c d) e)) - (list - (make-test-mtch (make-bindings (list (make-rib 'c2 `(c ,hole)) - (make-rib 'c1 `(b (c d) ,hole)))) - '(a (b (c d) e)) - none))) - - (test-empty '(in-hole (in-hole hole hole) a) - 'a - (list (make-test-mtch (make-bindings (list)) 'a none))) - - (test-empty '(a (b (in-hole (name c1 (in-hole (name c2 (c hole)) (d hole))) e))) - '(a (b (c (d e)))) - (list - (make-test-mtch (make-bindings (list (make-rib 'c1 `(c (d ,hole))) - (make-rib 'c2 `(c ,hole)))) - '(a (b (c (d e)))) - none))) - - (test-empty `(+ 1 (side-condition any ,(lambda (bindings) #t))) - '(+ 1 b) - (list (make-test-mtch (make-bindings '()) '(+ 1 b) none))) - (test-empty `(+ 1 (side-condition any ,(lambda (bindings) #f))) - '(+ 1 b) - #f) - - (test-empty `(+ 1 (side-condition b ,(lambda (bindings) #t))) - '(+ 1 b) - (list (make-test-mtch (make-bindings '()) '(+ 1 b) none))) - (test-empty `(+ 1 (side-condition a ,(lambda (bindings) #t))) - '(+ 1 b) - #f) - - (test-empty `(side-condition (name x any) ,(lambda (bindings) (eq? (lookup-binding bindings 'x) 'a))) - 'a - (list - (make-test-mtch (make-bindings (list (make-rib 'x 'a))) - 'a - none))) - - (test-empty `(+ 1 (side-condition (name x any) ,(lambda (bindings) (eq? (lookup-binding bindings 'x) 'a)))) - '(+ 1 a) - (list - (make-test-mtch (make-bindings (list (make-rib 'x 'a))) - '(+ 1 a) - none))) - - (test-empty `(side-condition (name x any) ,(lambda (bindings) (eq? (lookup-binding bindings 'x) 'a))) - 'b - #f) - - (test-empty `(+ 1 (side-condition (name x any) ,(lambda (bindings) (eq? (lookup-binding bindings 'x) 'a)))) - '(+ 1 b) - #f) - - (test-xab 'exp_1 - '(+ 1 2) - (list (make-test-mtch (make-bindings (list (make-rib 'exp_1 '(+ 1 2)))) '(+ 1 2) none))) - (test-xab '(exp_1 exp_2) - '((+ 1 2) (+ 3 4)) - (list (make-test-mtch (make-bindings (list (make-rib 'exp_1 '(+ 1 2)) (make-rib 'exp_2 '(+ 3 4)))) - '((+ 1 2) (+ 3 4)) - none))) - (test-xab '(exp_1 exp_1) - '((+ 1 2) (+ 3 4)) - #f) - (test-xab 'nesting-names - 'b - (list (make-test-mtch (make-bindings (list)) 'b none))) - (test-xab 'nesting-names - '(a b) - (list (make-test-mtch (make-bindings (list)) '(a b) none))) - (test-xab 'nesting-names - '(a (a b)) - (list (make-test-mtch (make-bindings (list)) '(a (a b)) none))) - (test-xab '((name x a) nesting-names) - '(a (a (a b))) - (list (make-test-mtch (make-bindings (list (make-rib 'x 'a))) '(a (a (a b))) none))) - (test-xab 'nesting-names - '(a (a (a (a b)))) - (list (make-test-mtch (make-bindings (list)) '(a (a (a (a b)))) none))) - - (test-xab 'same-in-nt - '(x x) - (list (make-test-mtch (make-bindings (list)) '(x x) none))) - (test-xab 'same-in-nt - '(x y) - #f) - - #; - (test-xab '(in-hole ec-multi (+ number number)) - '(+ 1 2) - (list (make-bindings (list (make-rib 'hole (make-hole-binding '(+ 1 2) '() #f)))))) - - #; - (test-xab '(in-hole ec-multi (+ number number)) - '(+ 1 (+ 5 6)) - (list (make-bindings (list (make-rib 'hole (make-hole-binding '(+ 5 6) '(cdr cdr car) #f)))))) - - #; - (test-xab '(in-hole ec-multi (+ number number)) - '(+ (+ (+ 1 2) 3) 4) - (list (make-bindings (list (make-rib 'hole (make-hole-binding '(+ 1 2) '(cdr car cdr car) #f)))))) - - #; - (test-xab '(in-hole ec-multi (+ number number)) - '(+ (+ 3 (+ 1 2)) 4) - (list (make-bindings (list (make-rib 'hole (make-hole-binding '(+ 1 2) '(cdr car cdr cdr car) #f)))))) - - #; - (test-xab '(in-hole ec-multi (+ number number)) - '(+ (+ (+ 1 2) (+ 3 4)) (+ 5 6)) - (list (make-bindings (list (make-rib 'hole (make-hole-binding '(+ 5 6) '(cdr cdr car) #f)))) - (make-bindings (list (make-rib 'hole (make-hole-binding '(+ 1 2) '(cdr car cdr car) #f)))) - (make-bindings (list (make-rib 'hole (make-hole-binding '(+ 3 4) '(cdr car cdr cdr car) #f)))))) - - (run-test - 'compatible-context-language1 - (build-compatible-context-language - (mk-hasheq '((exp . ()) (ctxt . ()))) - (list (make-nt 'exp - (list (make-rhs '(+ exp exp)) - (make-rhs 'number))) - (make-nt 'ctxt - (list (make-rhs '(+ ctxt exp)) - (make-rhs '(+ exp ctxt)) - (make-rhs 'hole))))) - (list - (make-nt 'exp-exp - (list (make-rhs 'hole) - (make-rhs `(+ (cross exp-exp) exp)) - (make-rhs `(+ exp (cross exp-exp))))) - (make-nt 'exp-ctxt - (list (make-rhs `(+ (cross exp-ctxt) exp)) - (make-rhs `(+ ctxt (cross exp-exp))) - (make-rhs `(+ (cross exp-exp) ctxt)) - (make-rhs `(+ exp (cross exp-ctxt))))) - (make-nt 'ctxt-exp - (list (make-rhs `(+ (cross ctxt-exp) exp)) - (make-rhs `(+ exp (cross ctxt-exp))))) - (make-nt 'ctxt-ctxt - (list (make-rhs 'hole) - (make-rhs `(+ (cross ctxt-ctxt) exp)) - (make-rhs `(+ ctxt (cross ctxt-exp))) - (make-rhs `(+ (cross ctxt-exp) ctxt)) - (make-rhs `(+ exp (cross ctxt-ctxt))))))) - - (run-test - 'compatible-context-language2 - (build-compatible-context-language - (mk-hasheq '((m . ()) (v . ()))) - (list (make-nt 'm (list (make-rhs '(m m)) (make-rhs '(+ m m)) (make-rhs 'v))) - (make-nt 'v (list (make-rhs 'number) (make-rhs '(lambda (x) m)))))) - (list - (make-nt 'm-m - (list - (make-rhs 'hole) - (make-rhs (list (list 'cross 'm-m) 'm)) - (make-rhs (list 'm (list 'cross 'm-m))) - (make-rhs (list '+ (list 'cross 'm-m) 'm)) - (make-rhs (list '+ 'm (list 'cross 'm-m))) - (make-rhs (list 'cross 'm-v)))) - (make-nt 'm-v (list (make-rhs (list 'lambda (list 'x) (list 'cross 'm-m))))) - (make-nt 'v-m - (list - (make-rhs (list (list 'cross 'v-m) 'm)) - (make-rhs (list 'm (list 'cross 'v-m))) - (make-rhs (list '+ (list 'cross 'v-m) 'm)) - (make-rhs (list '+ 'm (list 'cross 'v-m))) - (make-rhs (list 'cross 'v-v)))) - (make-nt 'v-v (list (make-rhs 'hole) (make-rhs (list 'lambda (list 'x) (list 'cross 'v-m))))))) - - (run-test - 'compatible-context-language3 - (build-compatible-context-language - (mk-hasheq '((m . ()) (seven . ()))) - (list (make-nt 'm (list (make-rhs '(m seven m)) (make-rhs 'number))) - (make-nt 'seven (list (make-rhs 7))))) - `(,(make-nt - 'm-m - `(,(make-rhs 'hole) ,(make-rhs `((cross m-m) seven m)) ,(make-rhs `(m (cross m-seven) m)) ,(make-rhs `(m seven (cross m-m))))) - ,(make-nt 'm-seven `()) - ,(make-nt - 'seven-m - `(,(make-rhs `((cross seven-m) seven m)) ,(make-rhs `(m (cross seven-seven) m)) ,(make-rhs `(m seven (cross seven-m))))) - ,(make-nt 'seven-seven `(,(make-rhs 'hole))))) - - #; - (test-xab '(in-hole (cross exp) (+ number number)) - '(+ (+ 1 2) 3) - (list (make-bindings (list (make-rib 'hole (make-hole-binding (list '+ 1 2) (list 'cdr 'car) #f)))))) - - (unless failure? - (fprintf (current-error-port) "All ~a tests passed.\n" test-count))) - - ;; mk-hasheq : (listof (cons sym any)) -> hash-table - ;; builds a hash table that has the bindings in assoc-list - (define (mk-hasheq assoc-list) - (let ([ht (make-hash-table)]) - (for-each - (lambda (a) - (hash-table-put! ht (car a) (cdr a))) - assoc-list) - ht)) - - ;; test-empty : sexp[pattern] sexp[term] answer -> void - ;; returns #t if pat matching exp with the empty language produces ans. - (define (test-empty pat exp ans) - (run-match-test - `(match-pattern (compile-pattern (compile-language '()) ',pat) ',exp) - (match-pattern - (compile-pattern (compile-language '()) pat) - exp) - ans)) - - (define xab-lang #f) - ;; test-xab : sexp[pattern] sexp[term] answer -> void - ;; returns #t if pat matching exp with a simple language produces ans. - (define (test-xab pat exp ans) - (unless xab-lang - (set! xab-lang - (compile-language (list (make-nt 'exp - (list (make-rhs '(+ exp exp)) - (make-rhs 'number))) - (make-nt 'ctxt - (list (make-rhs '(+ ctxt exp)) - (make-rhs '(+ exp ctxt)) - (make-rhs 'hole))) - - (make-nt 'ec-multi - (list (make-rhs 'hole) - (make-rhs '(in-named-hole xx ec-one ec-multi)))) - (make-nt 'ec-one - (list (make-rhs '(+ (hole xx) exp)) - (make-rhs '(+ exp (hole xx))))) - - (make-nt 'same-in-nt (list (make-rhs '((name x any) (name x any))))) - - (make-nt 'lsts - (list (make-rhs '()) - (make-rhs '(x)) - (make-rhs 'x) - (make-rhs '#f))) - (make-nt 'split-out - (list (make-rhs 'split-out2))) - (make-nt 'split-out2 - (list (make-rhs 'number))) - - (make-nt 'nesting-names - (list (make-rhs '(a (name x nesting-names))) - (make-rhs 'b))))))) - (run-match-test - `(match-pattern (compile-pattern xab-lang ',pat) ',exp) - (match-pattern (compile-pattern xab-lang pat) exp) - ans)) - - (define ab-lang #f) - ;; test-xab : sexp[pattern] sexp[term] answer -> void - ;; returns #t if pat matching exp with a simple language produces ans. - (define (test-ab pat exp ans) - (unless ab-lang - (set! ab-lang - (compile-language (list (make-nt 'aa - (list (make-rhs 'a))) - (make-nt 'bb - (list (make-rhs 'b))))))) - (run-match-test - `(match-pattern (compile-pattern ab-lang ',pat) ',exp) - (match-pattern (compile-pattern ab-lang pat) exp) - ans)) - - ;; test-ellipses : sexp sexp -> void - (define (test-ellipses pat expected) - (run-test - `(rewrite-ellipses ',pat (lambda (x) (values x #f))) - (let-values ([(compiled-pattern has-hole?) (rewrite-ellipses pat (lambda (x) (values x #f)))]) - (cons compiled-pattern has-hole?)) - (cons expected #f))) - - ;; run-test/cmp : sexp any any (any any -> boolean) - ;; compares ans with expected. If failure, - ;; prints info about the test and sets `failure?' to #t. - (define failure? #f) - (define test-count 0) - (define (run-test/cmp symbolic ans expected cmp?) - (set! test-count (+ test-count 1)) - (cond - [(cmp? ans expected) - '(printf "passed: ~s\n" symbolic)] - [else - (set! failure? #t) - (fprintf (current-error-port) - " test: ~s\nexpected: ~e\n got: ~e\n" - symbolic expected ans)])) - - (define (run-test symbolic ans expected) (run-test/cmp symbolic ans expected equal/bindings?)) - - ;; run-match-test : sexp got expected - ;; expects both ans and expected to be lists or both to be #f and - ;; compares them using a set-like equality if they are lists - (define (run-match-test symbolic ans expected) - (run-test/cmp - symbolic ans expected - (λ (xs ys) - (cond - [(and (not xs) (not ys)) #t] - [(and (list? xs) - (list? ys)) - (and (andmap (λ (x) (memf (λ (y) (equal/bindings? x y)) ys)) xs) - (andmap (λ (y) (memf (λ (x) (equal/bindings? x y)) xs)) ys))] - [else #f])))) - - ;; equal/bindings? : any any -> boolean - ;; compares two sexps (with embedded bindings) for equality. - ;; uses an order-insensitive comparison for the bindings - (define (equal/bindings? fst snd) - (let loop ([fst fst] - [snd snd]) - (cond - [(pair? fst) - (and (pair? snd) - (loop (car fst) (car snd)) - (loop (cdr fst) (cdr snd)))] - [(mtch? fst) - (and (mtch? snd) - (loop (mtch-bindings fst) - (mtch-bindings snd)) - (let ([g1 (gensym 'run-match-test-sym)]) - (equal? (plug (mtch-context fst) g1) - (plug (mtch-context snd) g1))) - (equal? (mtch-hole fst) - (mtch-hole snd)))] - [(bindings? fst) - (and (bindings? snd) - (let ([fst-table (bindings-table fst)] - [snd-table (bindings-table snd)]) - (and (= (length fst-table) - (length snd-table)) - (andmap - loop - (quicksort fst-table rib-lt) - (quicksort snd-table rib-lt)))))] - [(and (rib? fst) - (rib? snd) - (context? (rib-exp fst)) - (context? (rib-exp snd))) - (and (equal? (rib-name fst) (rib-name snd)) - (let ([g (gensym 'run-match-test-sym2)]) - (equal? (plug (rib-exp fst) g) - (plug (rib-exp snd) g))))] - [else (equal? fst snd)]))) - - (define (build-context c) - (let loop ([c c]) - (cond - [(eq? c hole) hole] - [(pair? c) (build-cons-context (loop (car c)) (loop (cdr c)))] - [(or (null? c) - (number? c) - (symbol? c)) - (build-flat-context c)] - [else (error 'build-context "unknown ~s" c)]))) - - ;; rib-lt : rib rib -> boolean - (define (rib-lt r1 r2) (string<=? (format "~s" (rib-name r1)) - (format "~s" (rib-name r2)))) - - (test)) diff --git a/collects/reduction-semantics/private/matcher.ss b/collects/reduction-semantics/private/matcher.ss deleted file mode 100644 index 28b2301048..0000000000 --- a/collects/reduction-semantics/private/matcher.ss +++ /dev/null @@ -1,1145 +0,0 @@ -#| - -Note: the patterns described in the doc.txt file are -slightly different than the patterns processed here. -The difference is in the form of the side-condition -expressions. Here they are procedures that accept -binding structures, instead of expressions. The -reduction (And other) macros do this transformation -before the pattern compiler is invoked. - -|# -(module matcher mzscheme - (require (lib "list.ss") - (lib "match.ss") - (lib "etc.ss") - (lib "contract.ss")) - - ;; lang = (listof nt) - ;; nt = (make-nt sym (listof rhs)) - ;; rhs = (make-rhs single-pattern) - ;; single-pattern = sexp - (define-struct nt (name rhs) (make-inspector)) - (define-struct rhs (pattern) (make-inspector)) - - ;; var = (make-var sym sexp) - ;; patterns are sexps with `var's embedded - ;; in them. It means to match the - ;; embedded sexp and return that binding - - ;; bindings = (make-bindings (listof rib)) - ;; rib = (make-rib sym sexp) - ;; if a rib has a pair, the first element of the pair should be treated as a prefix on the identifer - (define-values (make-bindings bindings-table bindings?) - (let () - (define-struct bindings (table) (make-inspector)) ;; for testing, add inspector - (values (lambda (table) - (unless (and (list? table) - (andmap rib? table)) - (error 'make-bindings "expected <(listof rib)>, got ~e" table)) - (make-bindings table)) - bindings-table - bindings?))) - - (define-struct rib (name exp) (make-inspector)) ;; for testing, add inspector - - ;; repeat = (make-repeat compiled-pattern (listof rib)) - (define-struct repeat (pat empty-bindings) (make-inspector)) ;; inspector for tests below - - ;; compiled-pattern : exp (union #f none sym) -> (union #f (listof mtch)) - ;; mtch = (make-match bindings sexp[context w/none-inside for the hole] (union none sexp[hole])) - ;; mtch is short for "match" - (define-values (mtch-bindings mtch-context mtch-hole make-mtch mtch?) - (let () - (define-struct mtch (bindings context hole) (make-inspector)) - (values mtch-bindings - mtch-context - mtch-hole - (lambda (a b c) - (unless (bindings? a) - (error 'make-mtch "expected bindings for first agument, got ~e" a)) - (make-mtch a b c)) - mtch?))) - ;; used to mean no context is available; also used as the "name" for an unnamed (ie, normal) hole - (define none - (let () - (define-struct none ()) - (make-none))) - (define (none? x) (eq? x none)) - - ;; compiled-lang : (make-compiled-lang (listof nt) - ;; hash-table[sym -o> compiled-pattern] - ;; hash-table[sym -o> compiled-pattern] - ;; hash-table[sym -o> compiled-pattern] - ;; hash-table[sym -o> boolean]) - ;; hash-table[sexp[pattern] -o> (cons compiled-pattern boolean)]) - ;; hole-info = (union #f none symbol) - ;; #f means we're not in a `in-hole' context - ;; none means we're looking for a normal hole - ;; symbol means we're looking for a named hole named by the symbol - (define compiled-pattern (any/c (union false/c none? symbol?) . -> . (union false/c (listof mtch?)))) - - (define-struct compiled-lang (lang ht list-ht across-ht has-hole-ht cache)) - - ;; lookup-binding : bindings (union sym (cons sym sym)) [(-> any)] -> any - (define lookup-binding - (opt-lambda (bindings - sym - [fail (lambda () (error 'lookup-binding "didn't find ~e in ~e" sym bindings))]) - (let loop ([ribs (bindings-table bindings)]) - (cond - [(null? ribs) (fail)] - [else - (let ([rib (car ribs)]) - (if (equal? (rib-name rib) sym) - (rib-exp rib) - (loop (cdr ribs))))])))) - - ;; compile-language : lang -> compiled-lang - (define (compile-language lang) - (let* ([clang-ht (make-hash-table)] - [clang-list-ht (make-hash-table)] - [across-ht (make-hash-table)] - [has-hole-ht (build-has-hole-ht lang)] - [cache (make-hash-table 'equal)] - [clang (make-compiled-lang lang clang-ht clang-list-ht across-ht has-hole-ht cache)] - [non-list-nt-table (build-non-list-nt-label lang)] - [list-nt-table (build-list-nt-label lang)] - [do-compilation - (lambda (ht list-ht lang prefix-cross?) - (for-each - (lambda (nt) - (for-each - (lambda (rhs) - (let-values ([(compiled-pattern has-hole?) - (compile-pattern/cross? clang (rhs-pattern rhs) prefix-cross?)]) - (let ([add-to-ht - (lambda (ht) - (hash-table-put! - ht - (nt-name nt) - (cons compiled-pattern - (hash-table-get ht (nt-name nt)))))]) - (when (may-be-non-list-pattern? (rhs-pattern rhs) - non-list-nt-table) - (add-to-ht ht)) - (when (may-be-list-pattern? (rhs-pattern rhs) - list-nt-table) - (add-to-ht list-ht))))) - (nt-rhs nt))) - lang))] - [init-ht - (lambda (ht) - (for-each (lambda (nt) (hash-table-put! ht (nt-name nt) null)) - lang))]) - - (init-ht clang-ht) - (init-ht clang-list-ht) - - (hash-table-for-each - clang-ht - (lambda (nt rhs) - (when (has-underscore? nt) - (error 'compile-language "cannot use underscore in nonterminal name, ~s" nt)))) - - (let ([compatible-context-language - (build-compatible-context-language clang-ht lang)]) - (for-each (lambda (nt) - (hash-table-put! across-ht (nt-name nt) null)) - compatible-context-language) - (do-compilation clang-ht clang-list-ht lang #t) - (do-compilation across-ht across-ht compatible-context-language #f) - clang))) - - ; build-has-hole-ht : (listof nt) -> hash-table[symbol -o> boolean] - ; produces a map of nonterminal -> whether that nonterminal could produce a hole - (define (build-has-hole-ht lang) - (build-nt-property - lang - (lambda (pattern recur) - (match pattern - [`any #f] - [`number #f] - [`string #f] - [`variable #f] - [`(variable-except ,@(vars ...)) #f] - [`hole #t] - [`(hole ,(? symbol? hole-name)) #t] - [(? string?) #f] - [(? symbol?) - ;; cannot be a non-terminal, otherwise this function isn't called - #f] - [`(name ,name ,pat) - (recur pat)] - [`(in-hole ,context ,contractum) - (recur contractum)] - [`(in-named-hole ,hole-name ,context ,contractum) - (recur contractum)] - [`(side-condition ,pat ,condition) - (recur pat)] - [(? list?) - (ormap recur pattern)] - [else #f])) - #t - (lambda (lst) (ormap values lst)))) - - ;; build-nt-property : lang (pattern[not-non-terminal] (pattern -> boolean) -> boolean) boolean - ;; -> hash-table[symbol[nt] -> boolean] - (define (build-nt-property lang test-rhs conservative-answer combine-rhss) - (let ([ht (make-hash-table)] - [rhs-ht (make-hash-table)]) - (for-each - (lambda (nt) - (hash-table-put! rhs-ht (nt-name nt) (nt-rhs nt)) - (hash-table-put! ht (nt-name nt) 'unknown)) - lang) - (let () - (define (check-nt nt-sym) - (let ([current (hash-table-get ht nt-sym)]) - (case current - [(unknown) - (hash-table-put! ht nt-sym 'computing) - (let ([answer (combine-rhss - (map (lambda (x) (check-rhs (rhs-pattern x))) - (hash-table-get rhs-ht nt-sym)))]) - (hash-table-put! ht nt-sym answer) - answer)] - [(computing) conservative-answer] - [else current]))) - (define (check-rhs rhs) - (cond - [(hash-table-maps? ht rhs) - (check-nt rhs)] - [else (test-rhs rhs check-rhs)])) - (for-each (lambda (nt) (check-nt (nt-name nt))) - lang) - ht))) - - ;; build-compatible-context-language : lang -> lang - (define (build-compatible-context-language clang-ht lang) - (apply - append - (map - (lambda (nt1) - (map - (lambda (nt2) - (let ([compat-nt (build-compatible-contexts/nt clang-ht (nt-name nt1) nt2)]) - (if (eq? (nt-name nt1) (nt-name nt2)) - (make-nt (nt-name compat-nt) - (cons - (make-rhs 'hole) - (nt-rhs compat-nt))) - compat-nt))) - lang)) - lang))) - - ;; build-compatible-contexts : clang-ht prefix nt -> nt - ;; constructs the compatible closure evaluation context from nt. - (define (build-compatible-contexts/nt clang-ht prefix nt) - (make-nt - (symbol-append prefix '- (nt-name nt)) - (apply append - (map - (lambda (rhs) - (let-values ([(maker count) (build-compatible-context-maker clang-ht - (rhs-pattern rhs) - prefix)]) - (let loop ([i count]) - (cond - [(zero? i) null] - [else (let ([nts (build-across-nts (nt-name nt) count (- i 1))]) - (cons (make-rhs (maker (box nts))) - (loop (- i 1))))])))) - (nt-rhs nt))))) - - (define (symbol-append . args) - (string->symbol (apply string-append (map symbol->string args)))) - - ;; build-across-nts : symbol number number -> (listof pattern) - (define (build-across-nts nt count i) - (let loop ([j count]) - (cond - [(zero? j) null] - [else - (cons (= i (- j 1)) - (loop (- j 1)))]))) - - ;; build-compatible-context-maker : symbol pattern -> (values ((box (listof pattern)) -> pattern) number) - ;; when the result function is applied, it takes each element - ;; of the of the boxed list and plugs them into the places where - ;; the nt corresponding from this rhs appeared in the original pattern. - ;; The number result is the number of times that the nt appeared in the pattern. - (define (build-compatible-context-maker clang-ht pattern prefix) - (let ([count 0]) - (values - (let loop ([pattern pattern]) - (match pattern - [`any (lambda (l) 'any)] - [`number (lambda (l) 'number)] - [`string (lambda (l) 'string)] - [`variable (lambda (l) 'variable)] - [`(variable-except ,@(vars ...)) (lambda (l) pattern)] - [`hole (lambda (l) 'hole)] - [`(hole ,(? symbol? hole-name)) (lambda (l) `(hole ,hole-name))] - [(? string?) (lambda (l) pattern)] - [(? symbol?) - (cond - [(hash-table-get clang-ht pattern (lambda () #f)) - (set! count (+ count 1)) - (lambda (l) - (let ([fst (car (unbox l))]) - (set-box! l (cdr (unbox l))) - (if fst - `(cross ,(symbol-append prefix '- pattern)) - pattern)))] - [else - (lambda (l) pattern)])] - [`(name ,name ,pat) - (let ([patf (loop pat)]) - (lambda (l) - `(name ,name ,(patf l))))] - [`(in-hole ,context ,contractum) - (let ([match-context (loop context)] - [match-contractum (loop contractum)]) - (lambda (l) - `(in-hole ,(match-context l) - ,(match-contractum l))))] - [`(in-named-hole ,hole-name ,context ,contractum) - (let ([match-context (loop context)] - [match-contractum (loop contractum)]) - (lambda (l) - `(in-named-hole ,hole-name - ,(match-context l) - ,(match-contractum l))))] - [`(side-condition ,pat ,condition) - (let ([patf (loop pat)]) - (lambda (l) - `(side-condition ,(patf l) ,condition)))] - [(? list?) - (let ([fs (map loop pattern)]) - (lambda (l) - (map (lambda (f) (f l)) fs)))] - [else - (lambda (l) pattern)])) - count))) - - ;; build-list-nt-label : lang -> hash-table[symbol -o> boolean] - (define (build-list-nt-label lang) - (build-nt-property - lang - (lambda (pattern recur) - (may-be-list-pattern?/internal pattern - (lambda (sym) #f) - recur)) - #t - (lambda (lst) (ormap values lst)))) - - (define (may-be-list-pattern? pattern list-nt-table) - (let loop ([pattern pattern]) - (may-be-list-pattern?/internal - pattern - (lambda (sym) - (hash-table-get list-nt-table - sym - (lambda () #f))) - loop))) - - (define (may-be-list-pattern?/internal pattern handle-symbol recur) - (match pattern - [`any #t] - [`number #f] - [`string #f] - [`variable #f] - [`(variable-except ,@(vars ...)) #f] - [`hole #t] - [`(hole ,(? symbol? hole-name)) #t] - [(? string?) #f] - [(? symbol?) - (handle-symbol pattern)] - [`(name ,name ,pat) - (recur pat)] - [`(in-hole ,context ,contractum) - (recur context)] - [`(in-named-hole ,hole-name ,context ,contractum) - (recur context)] - [`(side-condition ,pat ,condition) - (recur pat)] - [(? list?) - #t] - [else - ;; is this right?! - (or (null? pattern) (pair? pattern))])) - - - ;; build-non-list-nt-label : lang -> hash-table[symbol -o> boolean] - (define (build-non-list-nt-label lang) - (build-nt-property - lang - (lambda (pattern recur) - (may-be-non-list-pattern?/internal pattern - (lambda (sym) #t) - recur)) - #t - (lambda (lst) (ormap values lst)))) - - (define (may-be-non-list-pattern? pattern non-list-nt-table) - (let loop ([pattern pattern]) - (may-be-non-list-pattern?/internal - pattern - (lambda (sym) - (hash-table-get non-list-nt-table - sym - (lambda () #t))) - loop))) - - (define (may-be-non-list-pattern?/internal pattern handle-sym recur) - (match pattern - [`any #t] - [`number #t] - [`string #t] - [`variable #t] - [`(variable-except ,@(vars ...)) #t] - [`hole #t] - [`(hole ,(? symbol? hole-name)) #t] - [(? string?) #t] - [(? symbol?) (handle-sym pattern)] - [`(name ,name ,pat) - (recur pat)] - [`(in-hole ,context ,contractum) - (recur context)] - [`(in-named-hole ,hole-name ,context ,contractum) - (recur context)] - [`(side-condition ,pat ,condition) - (recur pat)] - [(? list?) - #f] - [else - ;; is this right?! - (not (or (null? pattern) (pair? pattern)))])) - - ;; match-pattern : compiled-pattern exp -> (union #f (listof bindings)) - (define (match-pattern compiled-pattern exp) - (let ([results (compiled-pattern exp #f)]) - (and results - (let ([filtered (filter-multiples results)]) - (and (not (null? filtered)) - filtered))))) - - ;; filter-multiples : (listof mtch) -> (listof mtch) - (define (filter-multiples matches) - (let loop ([matches matches] - [acc null]) - (cond - [(null? matches) acc] - [else - (let ([merged (merge-multiples/remove (car matches))]) - (if merged - (loop (cdr matches) (cons merged acc)) - (loop (cdr matches) acc)))]))) - - ;; merge-multiples/remove : bindings -> (union #f bindings) - ;; returns #f if all duplicate bindings don't bind the same thing - ;; returns a new bindings - (define (merge-multiples/remove match) - (let/ec fail - (let ([ht (make-hash-table 'equal)] - [ribs (bindings-table (mtch-bindings match))]) - (for-each - (lambda (rib) - (let/ec new - (let ([name (rib-name rib)] - [exp (rib-exp rib)]) - (let ([previous-exp - (hash-table-get - ht - name - (lambda () - (hash-table-put! ht name exp) - (new (void))))]) - (unless (equal? exp previous-exp) - (fail #f)))))) - ribs) - (make-mtch - (make-bindings (hash-table-map ht make-rib)) - (mtch-context match) - (mtch-hole match))))) - - (define underscore-allowed '(any number string variable)) - - ;; compile-pattern : compiled-lang pattern -> compiled-pattern - (define compile-pattern - (opt-lambda (clang pattern) - (let-values ([(pattern has-hole?) (compile-pattern/cross? clang pattern #t)]) - pattern))) - - ;; compile-pattern : compiled-lang pattern boolean -> (values compiled-pattern boolean) - (define (compile-pattern/cross? clang pattern prefix-cross?) - (define clang-ht (compiled-lang-ht clang)) - (define clang-list-ht (compiled-lang-list-ht clang)) - (define has-hole-ht (compiled-lang-has-hole-ht clang)) - (define across-ht (compiled-lang-across-ht clang)) - (define compiled-pattern-cache (compiled-lang-cache clang)) - - (define (compile-pattern/cache pattern) - (let ([compiled-cache (hash-table-get - compiled-pattern-cache - pattern - (lambda () - (let-values ([(compiled-pattern has-hole?) - (true-compile-pattern pattern)]) - (let ([val (cons (memoize compiled-pattern has-hole?) has-hole?)]) - (hash-table-put! compiled-pattern-cache pattern val) - val))))]) - (values (car compiled-cache) (cdr compiled-cache)))) - - ;; consult-compiled-pattern-cache : sexp[pattern] (-> compiled-pattern) -> compiled-pattern - (define (consult-compiled-pattern-cache pattern calc) - (hash-table-get - compiled-pattern-cache - pattern - (lambda () - (let ([res (calc)]) - (hash-table-put! compiled-pattern-cache pattern res) - res)))) - - (define (true-compile-pattern pattern) - (match pattern - [`any - (values - (lambda (exp hole-info) (list (make-mtch - (make-bindings null) - (build-flat-context exp) - none))) - #f)] - [`number - (values - (lambda (exp hole-info) (and (number? exp) (list (make-mtch - (make-bindings null) - (build-flat-context exp) - none)))) - #f)] - [`string - (values - (lambda (exp hole-info) (and (string? exp) (list (make-mtch - (make-bindings null) - (build-flat-context exp) - none)))) - #f)] - [`variable - (values - (lambda (exp hole-info) - (and (symbol? exp) (list (make-mtch (make-bindings null) - (build-flat-context exp) - none)))) - #f)] - [`(variable-except ,@(vars ...)) - (values - (lambda (exp hole-info) - (and (symbol? exp) - (not (memq exp vars)) - (list (make-mtch (make-bindings null) - (build-flat-context exp) - none)))) - #f)] - [`hole (values (match-hole none) #t)] - [`(hole ,hole-id) (values (match-hole hole-id) #t)] - [(? string?) - (values - (lambda (exp hole-info) - (and (string? exp) - (string=? exp pattern) - (list (make-mtch (make-bindings null) - (build-flat-context exp) - none)))) - #f)] - [(? symbol?) - (cond - [(hash-table-maps? clang-ht pattern) - (values - (lambda (exp hole-info) - (match-nt (hash-table-get clang-list-ht pattern) - (hash-table-get clang-ht pattern) - pattern exp hole-info)) - (hash-table-get has-hole-ht pattern))] - [(has-underscore? pattern) - (let ([before (split-underscore pattern)]) - (unless (or (hash-table-maps? clang-ht before) - (memq before underscore-allowed)) - (error 'compile-pattern "before underscore must be either a non-terminal or a built-in pattern, found ~a in ~s" - before - pattern)) - (compile-pattern/cache `(name ,pattern ,before)))] - [else - (values - (lambda (exp hole-info) (and (eq? exp pattern) (list (make-mtch (make-bindings null) - (build-flat-context exp) - none)))) - #f)])] - - [`(cross ,(? symbol? pre-id)) - (let ([id (if prefix-cross? - (symbol-append pre-id '- pre-id) - pre-id)]) - (cond - [(hash-table-maps? across-ht id) - (values - (lambda (exp hole-info) - (let ([rhs-list (hash-table-get across-ht id)]) - (match-nt rhs-list rhs-list id exp hole-info))) - #t)] - [else - (error 'compile-pattern "unknown cross reference ~a" id)]))] - - [`(name ,name ,pat) - (let-values ([(match-pat has-hole?) (compile-pattern/cache pat)]) - (values - (lambda (exp hole-info) - (let ([matches (match-pat exp hole-info)]) - (and matches - (map (lambda (match) - (make-mtch - (make-bindings (cons (make-rib name (mtch-context match)) - (bindings-table (mtch-bindings match)))) - (mtch-context match) - (mtch-hole match))) - matches)))) - has-hole?))] - [`(in-hole ,context ,contractum) - (let-values ([(match-context ctxt-has-hole?) (compile-pattern/cache context)] - [(match-contractum contractum-has-hole?) (compile-pattern/cache contractum)]) - (values - (match-in-hole context contractum exp match-context match-contractum none) - (or ctxt-has-hole? contractum-has-hole?)))] - [`(in-named-hole ,hole-id ,context ,contractum) - (let-values ([(match-context ctxt-has-hole?) (compile-pattern/cache context)] - [(match-contractum contractum-has-hole?) (compile-pattern/cache contractum)]) - (values - (match-in-hole context contractum exp match-context match-contractum hole-id) - (or ctxt-has-hole? contractum-has-hole?)))] - - [`(side-condition ,pat ,condition) - (let-values ([(match-pat has-hole?) (compile-pattern/cache pat)]) - (values - (lambda (exp hole-info) - (let ([matches (match-pat exp hole-info)]) - (and matches - (let ([filtered (filter (λ (m) (condition (mtch-bindings m))) matches)]) - (if (null? filtered) - #f - filtered))))) - has-hole?))] - [(? list?) - (let-values ([(rewritten has-hole?) (rewrite-ellipses pattern compile-pattern/cache)]) - (values - (lambda (exp hole-info) - (match-list rewritten exp hole-info)) - has-hole?))] - - ;; an already comiled pattern - [(? procedure?) - ;; return #t here as a failsafe; no way to check better. - (values pattern - #t)] - - [else - (values - (lambda (exp hole-info) - (and (eqv? pattern exp) - (list (make-mtch (make-bindings null) - (build-flat-context exp) - none)))) - #f)])) - - (compile-pattern/cache pattern)) - - ;; split-underscore : symbol -> symbol - ;; returns the text before the underscore in a symbol (as a symbol) - ;; raise an error if there is more than one underscore in the input - (define (split-underscore sym) - (string->symbol - (list->string - (let loop ([chars (string->list (symbol->string sym))]) - (cond - [(null? chars) (error 'split-underscore "bad")] - [else - (let ([c (car chars)]) - (cond - [(char=? c #\_) - (when (memq #\_ (cdr chars)) - (error 'compile-pattern "found a symbol with multiple underscores: ~s" sym)) - null] - [else (cons c (loop (cdr chars)))]))]))))) - - ;; has-underscore? : symbol -> boolean - (define (has-underscore? sym) - (memq #\_ (string->list (symbol->string sym)))) - - (define (memoize f needs-all-args?) - (if needs-all-args? - (memoize2 f) - (memoize1 f))) - - ; memoize1 : (x y -> w) -> x y -> w - ; memoizes a function of two arguments under the assumption - ; that the function is constant w.r.t the second - (define (memoize1 f) (memoize/key f (lambda (x y) x) nohole)) - (define (memoize2 f) (memoize/key f cons w/hole)) - - (define (memoize/key f key-fn statsbox) - (let ([ht (make-hash-table 'equal)] - [entries 0]) - (lambda (x y) - (set-cache-stats-hits! statsbox (add1 (cache-stats-hits statsbox))) - (let* ([key (key-fn x y)] - [compute/cache - (lambda () - (set! entries (+ entries 1)) - (set-cache-stats-hits! statsbox (sub1 (cache-stats-hits statsbox))) - (set-cache-stats-misses! statsbox (add1 (cache-stats-misses statsbox))) - (let ([res (f x y)]) - (hash-table-put! ht key res) - res))]) - (unless (< entries 10000) - (set! entries 0) - (set! ht (make-hash-table 'equal))) - (hash-table-get ht key compute/cache))))) - - (define-struct cache-stats (name misses hits)) - (define (new-cache-stats name) (make-cache-stats name 0 0)) - - (define w/hole (new-cache-stats "hole")) - (define nohole (new-cache-stats "no-hole")) - - (define (print-stats) - (let ((stats (list w/hole nohole))) - (for-each - (lambda (s) - (when (> (+ (cache-stats-hits s) (cache-stats-misses s)) 0) - (printf "~a has ~a hits, ~a misses (~a% miss rate)\n" - (cache-stats-name s) - (cache-stats-hits s) - (cache-stats-misses s) - (floor - (* 100 (/ (cache-stats-misses s) - (+ (cache-stats-hits s) (cache-stats-misses s)))))))) - stats) - (let ((overall-hits (apply + (map cache-stats-hits stats))) - (overall-miss (apply + (map cache-stats-misses stats)))) - (printf "---\nOverall hits: ~a\n" overall-hits) - (printf "Overall misses: ~a\n" overall-miss) - (when (> (+ overall-hits overall-miss) 0) - (printf "Overall miss rate: ~a%\n" - (floor (* 100 (/ overall-miss (+ overall-hits overall-miss))))))))) - - ;; match-hole : (union #f symbol) -> compiled-pattern - (define (match-hole hole-id) - (lambda (exp hole-info) - (and hole-info - (eq? hole-id hole-info) - (list (make-mtch (make-bindings '()) - hole - exp))))) - - ;; match-in-hole : sexp sexp sexp compiled-pattern compiled-pattern hole-info -> compiled-pattern - (define (match-in-hole context contractum exp match-context match-contractum hole-info) - (lambda (exp old-hole-info) - (let ([mtches (match-context exp hole-info)]) - (and mtches - (let loop ([mtches mtches] - [acc null]) - (cond - [(null? mtches) acc] - [else - (let* ([mtch (car mtches)] - [bindings (mtch-bindings mtch)] - [hole-exp (mtch-hole mtch)] - [contractum-mtches (match-contractum hole-exp old-hole-info)]) - (if contractum-mtches - (let i-loop ([contractum-mtches contractum-mtches] - [acc acc]) - (cond - [(null? contractum-mtches) (loop (cdr mtches) acc)] - [else (let* ([contractum-mtch (car contractum-mtches)] - [contractum-bindings (mtch-bindings contractum-mtch)]) - (i-loop - (cdr contractum-mtches) - (cons - (make-mtch (make-bindings - (append (bindings-table contractum-bindings) - (bindings-table bindings))) - (build-nested-context - (mtch-context mtch) - (mtch-context contractum-mtch)) - (mtch-hole contractum-mtch)) - acc)))])) - (loop (cdr mtches) acc)))])))))) - - ;; match-list : (listof (union repeat compiled-pattern)) sexp hole-info -> (union #f (listof bindings)) - (define (match-list patterns exp hole-info) - (let (;; raw-match : (listof (listof (listof mtch))) - [raw-match (match-list/raw patterns exp hole-info)]) - - (and (not (null? raw-match)) - - (let* (;; combined-matches : (listof (listof mtch)) - ;; a list of complete possibilities for matches - ;; (analagous to multiple matches of a single non-terminal) - [combined-matches (map combine-matches raw-match)] - - ;; flattened-matches : (union #f (listof bindings)) - [flattened-matches (if (null? combined-matches) - #f - (apply append combined-matches))]) - flattened-matches)))) - - ;; match-list/raw : (listof (union repeat compiled-pattern)) - ;; sexp - ;; hole-info - ;; -> (listof (listof (listof mtch))) - ;; the result is the raw accumulation of the matches for each subpattern, as follows: - ;; (listof (listof (listof mtch))) - ;; \ \ \-------------/ a match for one position in the list (failures don't show up) - ;; \ \-------------------/ one element for each position in the pattern list - ;; \-------------------------/ one element for different expansions of the ellipses - ;; the failures to match are just removed from the outer list before this function finishes - ;; via the `fail' argument to `loop'. - (define (match-list/raw patterns exp hole-info) - (let/ec k - (let loop ([patterns patterns] - [exp exp] - ;; fail : -> alpha - ;; causes one possible expansion of ellipses to fail - ;; initially there is only one possible expansion, so - ;; everything fails. - [fail (lambda () (k null))]) - (cond - [(pair? patterns) - (let ([fst-pat (car patterns)]) - (cond - [(repeat? fst-pat) - (if (or (null? exp) (pair? exp)) - (let ([r-pat (repeat-pat fst-pat)] - [r-mt (make-mtch (make-bindings (repeat-empty-bindings fst-pat)) - (build-flat-context '()) - none)]) - (apply - append - (cons (let/ec k - (let ([mt-fail (lambda () (k null))]) - (map (lambda (pat-ele) (cons (list r-mt) pat-ele)) - (loop (cdr patterns) exp mt-fail)))) - (let r-loop ([exp exp] - ;; past-matches is in reverse order - ;; it gets reversed before put into final list - [past-matches (list r-mt)]) - (cond - [(pair? exp) - (let* ([fst (car exp)] - [m (r-pat fst hole-info)]) - (if m - (let* ([combined-matches (collapse-single-multiples m past-matches)] - [reversed (reverse-multiples combined-matches)]) - (cons - (let/ec fail-k - (map (lambda (x) (cons reversed x)) - (loop (cdr patterns) - (cdr exp) - (lambda () (fail-k null))))) - (r-loop (cdr exp) combined-matches))) - (list null)))] - ;; what about dotted pairs? - [else (list null)]))))) - (fail))] - [else - (cond - [(pair? exp) - (let* ([fst-exp (car exp)] - [match (fst-pat fst-exp hole-info)]) - (if match - (let ([exp-match (map (λ (mtch) (make-mtch (mtch-bindings mtch) - (build-list-context (mtch-context mtch)) - (mtch-hole mtch))) - match)]) - (map (lambda (x) (cons exp-match x)) - (loop (cdr patterns) (cdr exp) fail))) - (fail)))] - [else - (fail)])]))] - [else - (if (null? exp) - (list null) - (fail))])))) - - ;; collapse-single-multiples : (listof mtch) (listof mtch[to-lists]) -> (listof mtch[to-lists]) - (define (collapse-single-multiples bindingss multiple-bindingss) - (apply append - (map - (lambda (multiple-match) - (let ([multiple-bindings (mtch-bindings multiple-match)]) - (map - (lambda (single-match) - (let ([single-bindings (mtch-bindings single-match)]) - (let ([ht (make-hash-table 'equal)]) - (for-each - (lambda (multiple-rib) - (hash-table-put! ht (rib-name multiple-rib) (rib-exp multiple-rib))) - (bindings-table multiple-bindings)) - (for-each - (lambda (single-rib) - (let* ([key (rib-name single-rib)] - [rst (hash-table-get ht key (lambda () null))]) - (hash-table-put! ht key (cons (rib-exp single-rib) rst)))) - (bindings-table single-bindings)) - (make-mtch (make-bindings (hash-table-map ht make-rib)) - (build-cons-context - (mtch-context single-match) - (mtch-context multiple-match)) - (pick-hole (mtch-hole single-match) - (mtch-hole multiple-match)))))) - bindingss))) - multiple-bindingss))) - - ;; pick-hole : (union none sexp) (union none sexp) -> (union none sexp) - (define (pick-hole s1 s2) - (cond - [(eq? none s1) s2] - [(eq? none s2) s1] - [(error 'matcher.ss "found two holes in list pattern ~s ~s" s1 s2)])) - - ;; reverse-multiples : (listof mtch[to-lists]) -> (listof mtch[to-lists]) - ;; reverses the rhs of each rib in the bindings and reverses the context. - (define (reverse-multiples matches) - (map (lambda (match) - (let ([bindings (mtch-bindings match)]) - (make-mtch - (make-bindings - (map (lambda (rib) - (make-rib (rib-name rib) - (reverse (rib-exp rib)))) - (bindings-table bindings))) - (reverse-context (mtch-context match)) - (mtch-hole match)))) - matches)) - - ;; match-nt : (listof compiled-rhs) (listof compiled-rhs) sym exp hole-info - ;; -> (union #f (listof bindings)) - (define (match-nt list-rhs non-list-rhs nt term hole-info) - (let loop ([rhss (if (or (null? term) (pair? term)) - list-rhs - non-list-rhs)] - [anss null]) - (cond - [(null? rhss) (if (null? anss) #f (apply append anss))] - [else - (let ([mth (remove-bindings/filter ((car rhss) term hole-info))]) - (if mth - (loop (cdr rhss) (cons mth anss)) - (loop (cdr rhss) anss)))]))) - - ;; remove-bindings/filter : (union #f (listof mtch)) -> (union #f (listof mtch)) - (define (remove-bindings/filter matches) - (and matches - (let ([filtered (filter-multiples matches)]) - (and (not (null? filtered)) - (map (λ (match) - (make-mtch (make-bindings '()) - (mtch-context match) - (mtch-hole match))) - matches))))) - - ;; rewrite-ellipses : (listof pattern) - ;; (pattern -> (values compiled-pattern boolean)) - ;; -> (values (listof (union repeat compiled-pattern)) boolean) - ;; moves the ellipses out of the list and produces repeat structures - (define (rewrite-ellipses pattern compile) - (let loop ([exp-eles pattern] - [fst dummy]) - (cond - [(null? exp-eles) - (if (eq? fst dummy) - (values empty #f) - (let-values ([(compiled has-hole?) (compile fst)]) - (values (list compiled) has-hole?)))] - [else - (let ([exp-ele (car exp-eles)]) - (cond - [(eq? '... exp-ele) - (when (eq? fst dummy) - (error 'match-pattern "bad ellipses placement: ~s" pattern)) - (let-values ([(compiled has-hole?) (compile fst)] - [(rest rest-has-hole?) (loop (cdr exp-eles) dummy)]) - (values - (cons (make-repeat compiled (extract-empty-bindings fst)) rest) - (or has-hole? rest-has-hole?)))] - [(eq? fst dummy) - (loop (cdr exp-eles) exp-ele)] - [else - (let-values ([(compiled has-hole?) (compile fst)] - [(rest rest-has-hole?) (loop (cdr exp-eles) exp-ele)]) - (values - (cons compiled rest) - (or has-hole? rest-has-hole?)))]))]))) - - (define dummy (box 0)) - - ;; extract-empty-bindings : pattern -> (listof rib) - (define (extract-empty-bindings pattern) - (let loop ([pattern pattern] - [ribs null]) - (match pattern - [`any ribs] - [`number ribs] - [`variable ribs] - [`(variable-except ,@(vars ...)) ribs] - - [`hole (error 'match-pattern "cannot have a hole inside an ellipses")] - [(? symbol?) - (cond - [(has-underscore? pattern) - (let ([before (split-underscore pattern)]) - (loop `(name ,pattern ,before) ribs))] - [else ribs])] - [`(name ,name ,pat) (loop pat (cons (make-rib name '()) ribs))] - [`(in-hole ,context ,contractum) (loop context (loop contractum ribs))] - [`(in-named-hole ,hole-name ,context ,contractum) (loop context (loop contractum ribs))] - [`(side-condition ,pat ,test) (loop pat ribs)] - [(? list?) - (let-values ([(rewritten has-hole?) (rewrite-ellipses pattern (lambda (x) (values x #f)))]) - (let i-loop ([r-exps rewritten] - [ribs ribs]) - (cond - [(null? r-exps) ribs] - [else (let ([r-exp (car r-exps)]) - (cond - [(repeat? r-exp) - (i-loop - (cdr r-exps) - (append (repeat-empty-bindings r-exp) ribs))] - [else - (i-loop - (cdr r-exps) - (loop (car r-exps) ribs))]))])))] - [else ribs]))) - - ;; combine-matches : (listof (listof mtch)) -> (listof mtch) - ;; input is the list of bindings corresonding to a piecewise match - ;; of a list. produces all of the combinations of complete matches - (define (combine-matches matchess) - (let loop ([matchess matchess]) - (cond - [(null? matchess) (list (make-mtch (make-bindings null) (build-flat-context '()) none))] - [else (combine-pair (car matchess) (loop (cdr matchess)))]))) - - ;; combine-pair : (listof mtch) (listof mtch) -> (listof mtch) - (define (combine-pair fst snd) - (let ([mtchs null]) - (for-each - (lambda (mtch1) - (for-each - (lambda (mtch2) - (set! mtchs (cons (make-mtch - (make-bindings (append (bindings-table (mtch-bindings mtch1)) - (bindings-table (mtch-bindings mtch2)))) - (build-append-context (mtch-context mtch1) (mtch-context mtch2)) - (pick-hole (mtch-hole mtch1) - (mtch-hole mtch2))) - mtchs))) - snd)) - fst) - mtchs)) - - (define (hash-table-maps? ht key) - (let/ec k - (hash-table-get ht key (lambda () (k #f))) - #t)) - - - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - ;; - ;; context adt - ;; - - #| - ;; This version of the ADT isn't right yet -- - ;; need to figure out what to do about (name ...) patterns. - - (define-values (struct:context make-context context? context-ref context-set!) - (make-struct-type 'context #f 1 0 #f '() #f 0)) - (define hole values) - (define (build-flat-context exp) (make-context (lambda (x) exp))) - (define (build-cons-context c1 c2) (make-context (lambda (x) (cons (c1 x) (c2 x))))) - (define (build-append-context l1 l2) (make-context (lambda (x) (append (l1 x) (l2 x))))) - (define (build-list-context l) (make-context (lambda (x) (list (l x))))) - (define (build-nested-context c1 c2) (make-context (lambda (x) (c1 (c2 x))))) - (define (plug exp hole-stuff) (exp hole-stuff)) - (define (reverse-context c) (make-context (lambda (x) (reverse (c x))))) - -|# - (define (context? x) #t) - (define hole - (let () - (define-struct hole ()) - (make-hole))) - - (define (build-flat-context exp) exp) - (define (build-cons-context e1 e2) (cons e1 e2)) - (define (build-append-context e1 e2) (append e1 e2)) - (define (build-list-context x) (list x)) - (define (reverse-context x) (reverse x)) - (define (build-nested-context c1 c2) (plug c1 c2)) - (define (plug exp hole-stuff) - (let loop ([exp exp]) - (cond - [(pair? exp) (cons (loop (car exp)) (loop (cdr exp)))] - [(eq? exp hole) hole-stuff] - [else exp]))) - - ;; - ;; end context adt - ;; - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - (provide/contract - (match-pattern (compiled-pattern any/c . -> . (union false/c (listof mtch?)))) - (compile-pattern (compiled-lang? any/c . -> . compiled-pattern)) - - (make-bindings ((listof rib?) . -> . bindings?)) - (bindings-table (bindings? . -> . (listof rib?))) - (bindings? (any/c . -> . boolean?)) - - (mtch? (any/c . -> . boolean?)) - (make-mtch (bindings? any/c any/c . -> . mtch?)) - (mtch-bindings (mtch? . -> . bindings?)) - (mtch-context (mtch? . -> . any/c)) - (mtch-hole (mtch? . -> . (union none? any/c))) - - (make-rib (symbol? any/c . -> . rib?)) - (rib? (any/c . -> . boolean?)) - (rib-name (rib? . -> . symbol?)) - (rib-exp (rib? . -> . any/c)) - - (print-stats (-> void?))) - - ;; for test suite - (provide build-cons-context - build-flat-context - context?) - - (provide (struct nt (name rhs)) - (struct rhs (pattern)) - (struct compiled-lang (lang ht across-ht has-hole-ht cache)) - - lookup-binding - compile-language - - compiled-pattern - - plug - none? none - - make-repeat - - hole - - rewrite-ellipses - build-compatible-context-language)) \ No newline at end of file diff --git a/collects/reduction-semantics/private/red-sem-macro-helpers.ss b/collects/reduction-semantics/private/red-sem-macro-helpers.ss deleted file mode 100644 index c88c684e31..0000000000 --- a/collects/reduction-semantics/private/red-sem-macro-helpers.ss +++ /dev/null @@ -1,31 +0,0 @@ -(module red-sem-macro-helpers mzscheme - - (provide extract-names) - - (require (lib "match.ss")) - - (define (extract-names stx) - (let ([dup-names - (let loop ([sexp (syntax-object->datum stx)] - [names null]) - (match sexp - [`(name ,(and sym (? symbol?)) ,pat) - (loop pat (cons sym names))] - [`(in-hole* ,(and sym (? symbol?)) ,pat1 ,pat2) - (loop pat1 - (loop pat2 - (cons sym names)))] - [`(in-hole ,pat1 ,pat2) - (loop pat1 - (loop pat2 - (cons 'hole names)))] - [(? list?) - (let i-loop ([sexp sexp] - [names names]) - (cond - [(null? sexp) names] - [else (i-loop (cdr sexp) (loop (car sexp) names))]))] - [else names]))] - [ht (make-hash-table)]) - (for-each (lambda (name) (hash-table-put! ht name #f)) dup-names) - (hash-table-map ht (lambda (x y) x))))) diff --git a/collects/reduction-semantics/private/subst-test.ss b/collects/reduction-semantics/private/subst-test.ss deleted file mode 100644 index 8d2505eae8..0000000000 --- a/collects/reduction-semantics/private/subst-test.ss +++ /dev/null @@ -1,120 +0,0 @@ -(module subst-test mzscheme - (require "../subst.ss" - (lib "match.ss")) - - (define (lc-subst1 var val exp) (subst/proc var val exp lc-separate)) - (define (lc-free-vars exp) (free-vars/memoize (make-hash-table) exp lc-separate)) - (define (lc-rename old-name new-name exp) (alpha-rename old-name new-name exp lc-separate)) - - (define lc-subst2 - (subst - [`(lambda ,vars ,body) - (all-vars vars) - (build (lambda (vars body) `(lambda ,vars ,body))) - (subterm vars body)] - [`(let (,l-var ,exp) ,body) - (all-vars (list l-var)) - (build (lambda (l-vars exp body) `(let (,@l-vars ,exp) ,body))) - (subterm '() exp) - (subterm (list l-var) body)] - [(? symbol?) (variable)] - [(? number?) (constant)] - [`(,fun ,@(args ...)) - (all-vars '()) - (build (lambda (vars fun . args) `(,fun ,@args))) - (subterm '() fun) - (subterms '() args)])) - - (define (lc-separate exp constant variable combine sub-piece) - (match exp - [`(lambda ,vars ,body) - (combine (lambda (vars body) `(lambda ,vars ,body)) - vars - (sub-piece vars body))] - [`(let (,l-var ,exp) ,body) - (combine (lambda (l-vars exp body) `(let (,(car l-vars) ,exp) ,body)) - (list l-var) - (sub-piece '() exp) - (sub-piece (list l-var) body))] - [(? symbol?) (variable (lambda (x) x) exp)] - [(? number?) (constant exp)] - [`(,fun ,@(args ...)) - (apply - combine - (lambda (variables fun . args) `(,fun ,@args)) - '() - (append - (list (sub-piece '() fun)) - (map (lambda (x) (sub-piece '() x)) args)))])) - - (define-syntax (test stx) - (syntax-case stx () - [(_ test-exp expected) - (syntax (test test-exp expected equal?))] - [(_ test-exp expected same?) - (syntax - (let ([actual test-exp] - [expected-v expected]) - ;(printf "testing: ~s\n" (syntax-object->datum #'test-exp)) - (unless (same? actual expected-v) - (printf " test: ~s\n expected: ~s\n got: ~s\n" - (syntax-object->datum #'test-exp) - expected-v - actual))))])) - - (define (set-equal? xs ys) - (and (andmap (lambda (x) (memq x ys)) xs) - (andmap (lambda (y) (memq y xs)) ys))) - - (define (lc-tests) - (tests lc-free-vars lc-subst1 lc-rename) - (tests #f lc-subst2 #f)) - - (define (tests free-vars subst rename) - (when free-vars - (test (free-vars 'x) '(x) set-equal?) - (test (free-vars '(lambda (x) x)) '() set-equal?) - (test (free-vars '(lambda (x) y)) '(y) set-equal?) - (test (free-vars '(let (x 1) x)) '() set-equal?) - (test (free-vars '(let (x 1) y)) '(y) set-equal?) - (test (free-vars '(let (x x) y)) '(y x) set-equal?) - (test (free-vars '(let (x 1) (y y))) '(y) set-equal?) - (test (free-vars '(lambda (y) (y y))) '() set-equal?)) - - (when rename - (test (rename 'x 'y 'x) 'x) - (test (rename 'x 'y '(lambda (x) x)) '(lambda (y) y))) - - (test (subst 'x 1 'x) 1) - (test (subst 'x 1 'y) 'y) - (test (subst 'x 1 '(lambda (x) x)) '(lambda (x) x)) - (test (subst 'x 1 '(lambda (y) x)) '(lambda (y) 1)) - (test (subst 'x 'y '(lambda (y) x)) '(lambda (y@) y)) - (test (subst 'x 'y '(lambda (y) (x y))) '(lambda (y@) (y y@))) - (test (subst 'x 'y '(let (x 1) 1)) '(let (x 1) 1)) - (test (subst 'x 'y '(let (x 1) x)) '(let (x 1) x)) - (test (subst 'x 'y '(let (x 1) y)) '(let (x 1) y)) - (test (subst 'x 'y '(let (y 1) (x y))) '(let (y@ 1) (y y@))) - (test (subst 'q '(lambda (x) y) '(lambda (y) y)) '(lambda (y) y)) - (test (subst 'q '(lambda (x) y) '(let ([y q]) y)) '(let ([y (lambda (x) y)]) y)) - (test (subst 'p '1 '(let (t 2) ((p t) t))) - '(let (t 2) ((1 t) t))) - (test (subst 'p '(lambda (s) s) - '(let (t (lambda (s) s)) ((p t) t))) - '(let (t (lambda (s) s)) (((lambda (s) s) t) t))) - (test (subst 'p - '(lambda (s) (s s)) - '(let (t (lambda (s) s)) - p)) - '(let (t (lambda (s) s)) - (lambda (s) (s s)))) - - (test (subst 's - '(lambda (z) (s z)) - '(lambda (s) (lambda (z) (s z)))) - '(lambda (s) (lambda (z) (s z)))) - - (test (subst 's - '(lambda (s) (lambda (z) (s z))) - '(lambda (z) (s z))) - '(lambda (z) ((lambda (s) (lambda (z) (s z))) z))))) diff --git a/collects/reduction-semantics/private/term.ss b/collects/reduction-semantics/private/term.ss deleted file mode 100644 index 283f46b95c..0000000000 --- a/collects/reduction-semantics/private/term.ss +++ /dev/null @@ -1,54 +0,0 @@ -(module term mzscheme - (require "matcher.ss") - (provide term term-let) - - (define-syntax (term orig-stx) - (define (rewrite stx) - (let loop ([stx stx]) - (syntax-case stx (unquote unquote-splicing in-hole) - [(unquote x) - (with-syntax ([x-rewrite (loop (syntax x))]) - (syntax (unsyntax x-rewrite)))] - [(unquote . x) - (raise-syntax-error 'term "malformed unquote" orig-stx stx)] - [(unquote-splicing x) - (with-syntax ([x-rewrite (loop (syntax x))]) - (syntax (unsyntax-splicing x-rewrite)))] - [(unquote-splicing . x) - (raise-syntax-error 'term "malformed unquote splicing" orig-stx stx)] - [(in-hole id body) - (and (identifier? (syntax id)) - (identifier? (syntax hole))) - (syntax (unsyntax (plug (term id) (term body))))] - [(in-hole . x) - (raise-syntax-error 'term "malformed in-hole" orig-stx stx)] - [(x ...) - (with-syntax ([(x-rewrite ...) (map loop (syntax->list (syntax (x ...))))]) - (syntax (x-rewrite ...)))] - [_ stx]))) - - (syntax-case orig-stx () - [(_ arg) - (with-syntax ([rewritten (rewrite (syntax arg))]) - (syntax (syntax-object->datum (quasisyntax rewritten))))])) - - (define-syntax (term-let stx) - (syntax-case stx () - [(_ ([x rhs] ...) body1 body2 ...) - (syntax - (with-syntax ([x rhs] ...) - (begin body1 body2 ...)))] - [(_ x) - (raise-syntax-error 'term-let "expected at least one body" stx)])) -#| - (define (test stx exp) - (unless (equal? (eval stx) exp) - (error 'test "~s" (syntax-object->datum stx)))) - - (test (quote-syntax (term 1)) 1) - (test (quote-syntax (term (1 2))) (list 1 2)) - (test (quote-syntax (term (1 ,(+ 1 1)))) (list 1 2)) - (test (quote-syntax (term-let ([x 1]) (term (x x)))) (list 1 1)) - (test (quote-syntax (term-let ([(x ...) (list 1 2 3)]) (term ((y x) ...)))) '((y 1) (y 2) (y 3))) -|# -) diff --git a/collects/reduction-semantics/reduction-semantics.ss b/collects/reduction-semantics/reduction-semantics.ss deleted file mode 100644 index 06ddf04688..0000000000 --- a/collects/reduction-semantics/reduction-semantics.ss +++ /dev/null @@ -1,317 +0,0 @@ -#| - -incompatible changes to be done: - - - make contexts be bound to just the context to avoid a separate `hole' thingy - -|# - -(module reduction-semantics mzscheme - (require "private/matcher.ss" - "private/term.ss" - (lib "contract.ss") - (lib "etc.ss")) - (require-for-syntax (lib "list.ss")) - - - ;; type red = (make-red compiled-pat ((listof (cons sym tst) (union string #f)) -> any) - (define-struct red (contractum reduct name)) - - - (provide reduction - reduction/name - reduction/context - reduction/context/name - language - plug - compiled-lang? - red? - term - term-let - none? - (rename red-name reduction->name)) - - (provide match-pattern - compile-pattern - make-bindings bindings-table bindings? - mtch? mtch-bindings mtch-context mtch-hole - make-rib rib? rib-name rib-exp) - - - (provide/contract - (language->predicate (compiled-lang? symbol? . -> . (any/c . -> . boolean?))) - (reduce ((listof (lambda (x) (red? x))) any/c . -> . (listof any/c))) - (reduce/tag-with-reduction ((listof (lambda (x) (red? x))) any/c . -> . (listof any/c))) - (give-name ((λ (x) (red? x)) string? . -> . red?)) - (variable-not-in (any/c symbol? . -> . symbol?)) - (compatible-closure ((lambda (x) (red? x)) - compiled-lang? - symbol? - . -> . - (lambda (x) (red? x)))) - (context-closure ((lambda (x) (red? x)) - compiled-lang? - any/c - . -> . - (lambda (x) (red? x))))) - - - - ;; give-name : red (union string #f) -> red - ;; gives the reduction the given name - (define (give-name red name) (make-red (red-contractum red) (red-reduct red) name)) - - ;; build-red : language pattern ((listof (cons sym tst)) -> any) (union string #f) -> red - (define (build-red lang contractum reduct name) - (make-red (compile-pattern lang contractum) reduct name)) - - (define (compatible-closure red lang nt) - (context-closure red lang `(cross ,nt))) - - (define (context-closure red lang pattern) - (let ([new-name (gensym 'context-closure)]) - (make-red (compile-pattern - lang - `(in-hole (name ,new-name ,pattern) - ,(red-contractum red))) - (lambda (bindings) - (let ([context (lookup-binding bindings new-name)] - [res ((red-reduct red) bindings)]) - (plug context res))) - #f))) - - (define-syntax-set (reduction/context reduction reduction/name reduction/context/name language) - - ;; (reduction/context lang ctxt pattern expression ...) - (define (reduction/context/proc stx) - (syntax-case stx () - [(_ lang-exp ctxt pattern bodies ...) - (let-values ([(names names/ellipses) (extract-names (syntax pattern))]) - (when (null? (syntax->list (syntax (bodies ...)))) - (raise-syntax-error #f "missing result expression" stx)) - (with-syntax ([(names ...) names] - [(names/ellipses ...) names/ellipses] - [side-condition-rewritten (rewrite-side-conditions (syntax pattern))]) - (syntax - (build-red lang-exp - `(in-hole (name context ctxt) side-condition-rewritten) - (lambda (bindings) - (term-let ([context (lookup-binding bindings 'context)] - [names/ellipses (lookup-binding bindings 'names)] ...) - (plug - (term context) - (begin - (void) - bodies ...)))) - #f))))])) - - (define (reduction/context/name/proc stx) - (syntax-case stx () - [(_ name-exp lang-exp ctxt pattern bodies ...) - #'(give-name (reduction/context lang-exp ctxt pattern bodies ...) - name-exp)])) - - - ;; (reduction lang pattern expression ...) - (define (reduction/proc stx) - (syntax-case stx () - [(_ lang-exp pattern bodies ...) - (let-values ([(names names/ellipses) (extract-names (syntax pattern))]) - (when (null? (syntax->list (syntax (bodies ...)))) - (raise-syntax-error #f "missing result expression" stx)) - (with-syntax ([(name-ellipses ...) names/ellipses] - [(name ...) names] - [side-condition-rewritten (rewrite-side-conditions (syntax pattern))]) - (syntax - (build-red lang-exp - `side-condition-rewritten - (lambda (bindings) - (term-let ([name-ellipses (lookup-binding bindings 'name)] ...) - bodies ...)) - #f))))])) - - (define (reduction/name/proc stx) - (syntax-case stx () - [(_ name-exp lang-exp pattern bodies ...) - #`(give-name (reduction lang-exp pattern bodies ...) name-exp)])) - - (define (language/proc stx) - (syntax-case stx () - [(_ (name rhs ...) ...) - (andmap identifier? (syntax->list (syntax/loc stx (name ...)))) - (with-syntax ([((r-rhs ...) ...) (map (lambda (rhss) (map rewrite-side-conditions (syntax->list rhss))) - (syntax->list (syntax ((rhs ...) ...))))]) - (syntax/loc stx - (compile-language (list (make-nt 'name (list (make-rhs `r-rhs) ...)) ...))))] - [(_ (name rhs ...) ...) - (for-each - (lambda (name) - (unless (identifier? name) - (raise-syntax-error 'language "expected name" stx name))) - (syntax->list (syntax (name ...))))] - [(_ x ...) - (for-each - (lambda (x) - (syntax-case x () - [(name rhs ...) - (void)] - [_ - (raise-syntax-error 'language "malformed non-terminal" stx x)])) - (syntax->list (syntax (x ...))))])) - - (define (rewrite-side-conditions orig-stx) - (let loop ([term orig-stx]) - (syntax-case term (side-condition) - [(side-condition pat exp) - (let-values ([(names names/ellipses) (extract-names (syntax pat))]) - (with-syntax ([(name ...) names] - [(name/ellipses ...) names/ellipses]) - (syntax/loc term - (side-condition - pat - ,(lambda (bindings) - (term-let ([name/ellipses (lookup-binding bindings 'name)] ...) - exp))))))] - [(terms ...) - (map loop (syntax->list (syntax (terms ...))))] - [else term]))) - - (define-struct id/depth (id depth)) - - ;; extract-names : syntax -> (values (listof syntax) (listof syntax[x | (x ...) | ((x ...) ...) | ...])) - (define (extract-names orig-stx) - (let* ([dups - (let loop ([stx orig-stx] - [names null] - [depth 0]) - (syntax-case stx (name in-hole in-named-hole side-condition) - [(name sym pat) - (identifier? (syntax sym)) - (loop (syntax pat) - (cons (make-id/depth (syntax sym) depth) names) - depth)] - [(in-named-hole hlnm sym pat1 pat2) - (identifier? (syntax sym)) - (loop (syntax pat1) - (loop (syntax pat2) names depth) - depth)] - [(in-hole pat1 pat2) - (loop (syntax pat1) - (loop (syntax pat2) names depth) - depth)] - [(side-condition pat e) - (loop (syntax pat) names depth)] - [(pat ...) - (let i-loop ([pats (syntax->list (syntax (pat ...)))] - [names names]) - (cond - [(null? pats) names] - [else - (if (or (null? (cdr pats)) - (not (identifier? (cadr pats))) - (not (module-identifier=? (quote-syntax ...) - (cadr pats)))) - (i-loop (cdr pats) - (loop (car pats) names depth)) - (i-loop (cdr pats) - (loop (car pats) names (+ depth 1))))]))] - [x - (and (identifier? (syntax x)) - (has-underscore? (syntax x))) - (cons (make-id/depth (syntax x) depth) names)] - [else names]))] - [no-dups (filter-duplicates dups)]) - (values (map id/depth-id no-dups) - (map build-dots no-dups)))) - - ;; build-dots : id/depth -> syntax[x | (x ...) | ((x ...) ...) | ...] - (define (build-dots id/depth) - (let loop ([depth (id/depth-depth id/depth)]) - (cond - [(zero? depth) (id/depth-id id/depth)] - [else (with-syntax ([rest (loop (- depth 1))] - [dots (quote-syntax ...)]) - (syntax (rest dots)))]))) - - (define (has-underscore? x) - (memq #\_ (string->list (symbol->string (syntax-e x))))) - - (define (filter-duplicates dups) - (let loop ([dups dups]) - (cond - [(null? dups) null] - [else - (cons - (car dups) - (filter (lambda (x) - (let ([same-id? (module-identifier=? (id/depth-id x) - (id/depth-id (car dups)))]) - (when same-id? - (unless (equal? (id/depth-depth x) - (id/depth-depth (car dups))) - (error 'reduction "found the same binder, ~s, at different depths, ~a and ~a" - (syntax-object->datum (id/depth-id x)) - (id/depth-depth x) - (id/depth-depth (car dups))))) - (not same-id?))) - (loop (cdr dups))))])))) - - (define (language->predicate lang id) - (let ([p (compile-pattern lang id)]) - (lambda (x) - (and (match-pattern p x) #t)))) - - ;; reduce : (listof red) exp -> (listof exp) - (define (reduce reductions exp) - (reduce/internal reductions exp (λ (red) (λ (mtch) ((red-reduct red) (mtch-bindings mtch)))))) - - ; reduce/tag-with-reductions : (listof red) exp -> (listof (list red exp)) - (define (reduce/tag-with-reduction reductions exp) - (reduce/internal reductions exp (λ (red) (λ (mtch) (list red ((red-reduct red) (mtch-bindings mtch))))))) - - ; reduce/internal : (listof red) exp (red -> match -> X) -> listof X - (define (reduce/internal reductions exp f) - (let loop ([reductions reductions] - [acc null]) - (cond - [(null? reductions) acc] - [else (let ([red (car reductions)]) - (let ([mtchs (match-pattern (red-contractum red) exp)]) - (if mtchs - (loop (cdr reductions) - (map/mt - (f red) - mtchs - acc)) - (loop (cdr reductions) acc))))]))) - - ;; map/mt : (a -> b) (listof a) (listof b) -> (listof b) - ;; map/mt is like map, except it uses the last argument - ;; instaed of the empty list - (define (map/mt f l mt-l) - (let loop ([l l]) - (cond - [(null? l) mt-l] - [else (cons (f (car l)) (loop (cdr l)))]))) - - (define re:gen-d #rx".*[^0-9]([0-9]+)$") - (define (variable-not-in sexp var) - (let* ([var-str (symbol->string var)] - [nums (let loop ([sexp sexp] - [nums null]) - (cond - [(pair? sexp) (loop (cdr sexp) (loop (car sexp) nums))] - [(symbol? sexp) (let* ([str (symbol->string sexp)] - [match (regexp-match re:gen-d str)]) - (if (and match - (is-prefix? var-str str)) - (cons (string->number (cadr match)) nums) - nums))] - [else nums]))]) - (if (null? nums) - (string->symbol (format "~a1" var)) - (string->symbol (format "~a~a" var (+ 1 (apply max nums))))))) - - (define (is-prefix? str1 str2) - (and (<= (string-length str1) (string-length str2)) - (equal? str1 (substring str2 0 (string-length str1)))))) diff --git a/collects/reduction-semantics/subst.ss b/collects/reduction-semantics/subst.ss deleted file mode 100644 index 080224c857..0000000000 --- a/collects/reduction-semantics/subst.ss +++ /dev/null @@ -1,292 +0,0 @@ -(module subst mzscheme - (require (lib "match.ss") - (prefix plt: (lib "plt-match.ss")) - (lib "list.ss")) - - (provide plt-subst subst - all-vars variable subterm subterms constant build - subst/proc alpha-rename free-vars/memoize) - - (define-syntax (all-vars stx) (raise-syntax-error 'subst "all-vars out of context" stx)) - (define-syntax (variable stx) (raise-syntax-error 'subst "variable out of context" stx)) - (define-syntax (subterm stx) (raise-syntax-error 'subst "subterm out of context" stx)) - (define-syntax (subterms stx) (raise-syntax-error 'subst "subterms out of context" stx)) - (define-syntax (constant stx) (raise-syntax-error 'subst "constant out of context" stx)) - (define-syntax (build stx) (raise-syntax-error 'subst "build out of context" stx)) - - (define-syntax (make-subst stx) - (syntax-case stx () - [(_ subst match) - (syntax - (define-syntax (subst stx) - (syntax-case stx () - [(_ (pat rhs (... ...)) (... ...)) - (with-syntax ([term/arg #'term/arg] - [constant/arg #'constant/arg] - [variable/arg #'variable/arg] - [combine/arg #'combine/arg] - [sub-piece/arg #'subpiece/arg]) - (define (handle-rhs rhs-stx) - (syntax-case rhs-stx (all-vars build subterm subterms variable constant) - [((all-vars all-vars-exp) (build build-exp) sub-pieces (... ...)) - (with-syntax ([(sub-pieces (... ...)) - (map (lambda (subterm-stx) - (syntax-case subterm-stx (subterm subterms) - [(subterm vars body) (syntax (list (sub-piece/arg vars body)))] - [(subterms vars terms) - (syntax - (let ([terms-var terms]) - (unless (list? terms-var) - (error 'subst - "expected a list of terms for `subterms' subclause, got: ~e" - terms-var)) - (map (lambda (x) (sub-piece/arg vars x)) - terms-var)))] - [else (raise-syntax-error - 'subst - "unknown all-vars subterm" - stx - subterm-stx)])) - (syntax->list (syntax (sub-pieces (... ...)))))]) - (syntax - (apply combine/arg - build-exp - all-vars-exp - (append sub-pieces (... ...)))))] - [((all-vars) sub-pieces (... ...)) - (raise-syntax-error 'subst "expected all-vars must have an argument" stx rhs-stx)] - [((all-vars all-vars-exp) not-build-clause anything (... ...)) - (raise-syntax-error 'subst "expected build clause" (syntax not-build-clause))] - [((all-vars all-vars-exp)) - (raise-syntax-error 'subst "missing build clause" (syntax (all-vars all-vars-exp)))] - [((constant)) - (syntax (constant/arg term/arg))] - [((variable)) - (syntax (variable/arg (lambda (x) x) term/arg))] - [(unk unk-more (... ...)) - (raise-syntax-error 'subst "unknown clause" (syntax unk))])) - (with-syntax ([(expanded-rhs (... ...)) - (map handle-rhs (syntax->list (syntax ((rhs (... ...)) (... ...)))))]) - (syntax - (let ([separate - (lambda (term/arg constant/arg variable/arg combine/arg sub-piece/arg) - (match term/arg - [pat expanded-rhs] (... ...) - [else (error 'subst "no matching clauses for ~s\n" term/arg)]))]) - (lambda (var val exp) - (subst/proc var val exp separate))))))])))])) - - (make-subst subst match) - (make-subst plt-subst plt:match) - - (define (subst/proc var val exp separate) - (let* ([free-vars-cache (make-hash-table 'equal)] - [fv-val (free-vars/memoize free-vars-cache val separate)]) - (let loop ([exp exp]) - (let ([fv-exp (free-vars/memoize free-vars-cache exp separate)] - [handle-constant - (lambda (x) x)] - [handle-variable - (lambda (rebuild var-name) - (if (equal? var-name var) - val - (rebuild var-name)))] - [handle-complex - (lambda (maker vars . subpieces) - (cond - [(ormap (lambda (var) (memq var fv-val)) vars) - => - (lambda (to-be-renamed-l) - (let ([to-be-renamed (car to-be-renamed-l)]) - (loop - (alpha-rename - to-be-renamed - (pick-new-name to-be-renamed (cons to-be-renamed fv-val)) - exp - separate))))] - [else - (apply maker - vars - (map (lambda (subpiece) - (let ([sub-term-binders (subpiece-binders subpiece)] - [sub-term (subpiece-term subpiece)]) - (if (memq var sub-term-binders) - sub-term - (loop sub-term)))) - subpieces))]))]) - (if (member var fv-exp) - (separate - exp - handle-constant - handle-variable - handle-complex - make-subpiece) - exp))))) - - (define-struct subpiece (binders term) (make-inspector)) - - ;; alpha-rename : symbol symbol term separate -> term - ;; renames the occurrences of to-be-renamed that are - ;; bound in the "first level" of exp. - (define (alpha-rename to-be-renamed new-name exp separate) - (define (first exp) - (separate exp - first-handle-constant - first-handle-variable - first-handle-complex - first-handle-complex-subpiece)) - (define (first-handle-constant x) x) - (define (first-handle-variable rebuild var) (rebuild var)) - (define (first-handle-complex maker vars . subpieces) - (let ([replaced-vars - (map (lambda (x) (if (eq? x to-be-renamed) new-name x)) - vars)]) - (apply maker replaced-vars subpieces))) - (define (first-handle-complex-subpiece binders subterm) - (if (memq to-be-renamed binders) - (beyond-first subterm) - subterm)) - - (define (beyond-first exp) - (define (handle-constant x) x) - (define (handle-variable rebuild var) - (if (eq? var to-be-renamed) - (rebuild new-name) - (rebuild var))) - (define (handle-complex maker vars . subpieces) - (apply maker vars subpieces)) - (define (handle-complex-subpiece binders subterm) - (if (memq to-be-renamed binders) - subterm - (beyond-first subterm))) - (separate - exp - handle-constant - handle-variable - handle-complex - handle-complex-subpiece)) - - (first exp)) - - ;; free-vars/memoize : hash-table[sexp -o> (listof symbols)] sexp separate -> (listof symbols) - ;; doesn't cache against separate -- if it changes, a new hash-table must be passed in, - ;; or the caching will be wrong - (define (free-vars/memoize cache exp separate) - (hash-table-get - cache - exp - (lambda () - (let ([res (free-vars/compute cache exp separate)]) - (hash-table-put! cache exp res) - res)))) - - ;; free-vars/memoize : hash-table[sexp -o> (listof symbols)] sexp separate -> (listof symbols) - (define (free-vars/compute cache exp separate) - (let ([handle-constant (lambda (x) '())] - [handle-variable (lambda (rebuild var) (list var))] - [handle-complex - (lambda (maker vars . subpieces) - (apply append subpieces))] - [handle-complex-subpiece - (lambda (binders subterm) - (foldl remove-all - (free-vars/memoize cache subterm separate) - binders))]) - (separate - exp - handle-constant - handle-variable - handle-complex - handle-complex-subpiece))) - - (define (remove-all var lst) - (let loop ([lst lst] - [ans '()]) - (cond - [(null? lst) ans] - [else (if (eq? (car lst) var) - (loop (cdr lst) ans) - (loop (cdr lst) (cons (car lst) ans)))]))) - - (define (lc-direct-subst var val exp) - (let ([fv-exp (lc-direct-free-vars exp)]) - (if (memq var fv-exp) - (match exp - [`(lambda ,vars ,body) - (if (memq var vars) - exp - (let* ([fv-val (lc-direct-free-vars val)] - [vars1 (map (lambda (var) (pick-new-name var fv-val)) vars)]) - `(lambda ,vars1 ,(lc-direct-subst - var - val - (lc-direct-subst/l vars - vars1 - body)))))] - [`(let (,l-var ,exp) ,body) - (if (eq? l-var var) - `(let (,l-var ,(lc-direct-subst var val exp)) ,body) - (let* ([fv-val (lc-direct-free-vars val)] - [l-var1 (pick-new-name l-var fv-val)]) - `(let (,l-var1 ,(lc-direct-subst var val exp)) - ,(lc-direct-subst - var - val - (lc-direct-subst - l-var - l-var1 - body)))))] - [(? number?) exp] - [(and var1 (? symbol?)) - (if (eq? var1 var) - val - var1)] - [`(,@(args ...)) - `(,@(map (lambda (arg) (lc-direct-subst var val arg)) args))]) - exp))) - - ;; lc-direct-subst/l : (listof symbol) (listof symbol) (listof symbol) sexp -> exp - ;; substitutes each of vars with vals in exp - ;; [assume vals don't contain any vars] - (define (lc-direct-subst/l vars vals exp) - (foldr (lambda (var val exp) (lc-direct-subst var val exp)) - exp - vars - vals)) - - ;; lc-direct-free-vars : sexp -> (listof symbol) - ;; returns the free variables in exp - (define (lc-direct-free-vars exp) - (let ([ht (make-hash-table)]) - (let loop ([exp exp] - [binding-vars null]) - (match exp - [(? symbol?) - (unless (memq exp binding-vars) - (hash-table-put! ht exp #t))] - [(? number?) - (void)] - [`(lambda ,vars ,body) - (loop body (append vars binding-vars))] - [`(let (,var ,exp) ,body) - (loop exp binding-vars) - (loop body (cons var binding-vars))] - [`(,@(args ...)) - (for-each (lambda (arg) (loop arg binding-vars)) args)])) - (hash-table-map ht (lambda (x y) x)))) - - ;; pick-new-name : symbol (listof symbol) -> symbol - ;; returns a primed version of `var' that does - ;; not occur in vars (possibly with no primes) - (define (pick-new-name var vars) - (if (member var vars) - (pick-new-name (prime var) vars) - var)) - - ;; prime : symbol -> symbol - ;; adds an @ at the end of the symbol - (define (prime var) - (string->symbol - (string-append - (symbol->string var) - "@")))) \ No newline at end of file