diff options
| -rwxr-xr-x | configure | 18 | ||||
| -rw-r--r-- | configure.ac | 2 | ||||
| -rw-r--r-- | configure.ac.pamphlet | 2 | ||||
| -rw-r--r-- | src/ChangeLog | 21 | ||||
| -rw-r--r-- | src/algebra/any.spad.pamphlet | 11 | ||||
| -rw-r--r-- | src/interp/compiler.boot | 58 | ||||
| -rw-r--r-- | src/interp/fnewmeta.lisp | 42 | ||||
| -rw-r--r-- | src/interp/g-opt.boot | 10 | ||||
| -rw-r--r-- | src/interp/metalex.lisp | 2 | ||||
| -rw-r--r-- | src/interp/newaux.lisp | 2 |
10 files changed, 145 insertions, 23 deletions
@@ -1,6 +1,6 @@ #! /bin/sh # Guess values for system-dependent variables and create Makefiles. -# Generated by GNU Autoconf 2.63 for OpenAxiom 1.3.0-2009-06-13. +# Generated by GNU Autoconf 2.63 for OpenAxiom 1.3.0-2009-06-14. # # Report bugs to <open-axiom-bugs@lists.sf.net>. # @@ -745,8 +745,8 @@ SHELL=${CONFIG_SHELL-/bin/sh} # Identity of this package. PACKAGE_NAME='OpenAxiom' PACKAGE_TARNAME='openaxiom' -PACKAGE_VERSION='1.3.0-2009-06-13' -PACKAGE_STRING='OpenAxiom 1.3.0-2009-06-13' +PACKAGE_VERSION='1.3.0-2009-06-14' +PACKAGE_STRING='OpenAxiom 1.3.0-2009-06-14' PACKAGE_BUGREPORT='open-axiom-bugs@lists.sf.net' ac_unique_file="src/Makefile.pamphlet" @@ -1500,7 +1500,7 @@ if test "$ac_init_help" = "long"; then # Omit some internal or obsolete options to make the list less imposing. # This message is too long to be a string in the A/UX 3.1 sh. cat <<_ACEOF -\`configure' configures OpenAxiom 1.3.0-2009-06-13 to adapt to many kinds of systems. +\`configure' configures OpenAxiom 1.3.0-2009-06-14 to adapt to many kinds of systems. Usage: $0 [OPTION]... [VAR=VALUE]... @@ -1570,7 +1570,7 @@ fi if test -n "$ac_init_help"; then case $ac_init_help in - short | recursive ) echo "Configuration of OpenAxiom 1.3.0-2009-06-13:";; + short | recursive ) echo "Configuration of OpenAxiom 1.3.0-2009-06-14:";; esac cat <<\_ACEOF @@ -1672,7 +1672,7 @@ fi test -n "$ac_init_help" && exit $ac_status if $ac_init_version; then cat <<\_ACEOF -OpenAxiom configure 1.3.0-2009-06-13 +OpenAxiom configure 1.3.0-2009-06-14 generated by GNU Autoconf 2.63 Copyright (C) 1992, 1993, 1994, 1995, 1996, 1998, 1999, 2000, 2001, @@ -1686,7 +1686,7 @@ cat >config.log <<_ACEOF This file contains any messages produced by compilers while running configure, to aid debugging if configure makes a mistake. -It was created by OpenAxiom $as_me 1.3.0-2009-06-13, which was +It was created by OpenAxiom $as_me 1.3.0-2009-06-14, which was generated by GNU Autoconf 2.63. Invocation command line was $ $0 $@ @@ -17686,7 +17686,7 @@ exec 6>&1 # report actual input values of CONFIG_FILES etc. instead of their # values after options handling. ac_log=" -This file was extended by OpenAxiom $as_me 1.3.0-2009-06-13, which was +This file was extended by OpenAxiom $as_me 1.3.0-2009-06-14, which was generated by GNU Autoconf 2.63. Invocation command line was CONFIG_FILES = $CONFIG_FILES @@ -17749,7 +17749,7 @@ Report bugs to <bug-autoconf@gnu.org>." _ACEOF cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1 ac_cs_version="\\ -OpenAxiom config.status 1.3.0-2009-06-13 +OpenAxiom config.status 1.3.0-2009-06-14 configured by $0, generated by GNU Autoconf 2.63, with options \\"`$as_echo "$ac_configure_args" | sed 's/^ //; s/[\\""\`\$]/\\\\&/g'`\\" diff --git a/configure.ac b/configure.ac index 639acd36..bbe8c381 100644 --- a/configure.ac +++ b/configure.ac @@ -1,6 +1,6 @@ sinclude(config/open-axiom.m4) sinclude(config/aclocal.m4) -AC_INIT([OpenAxiom], [1.3.0-2009-06-13], +AC_INIT([OpenAxiom], [1.3.0-2009-06-14], [open-axiom-bugs@lists.sf.net]) AC_CONFIG_AUX_DIR(config) diff --git a/configure.ac.pamphlet b/configure.ac.pamphlet index 03192074..bb662ab1 100644 --- a/configure.ac.pamphlet +++ b/configure.ac.pamphlet @@ -1131,7 +1131,7 @@ information: <<Autoconf init>>= sinclude(config/open-axiom.m4) sinclude(config/aclocal.m4) -AC_INIT([OpenAxiom], [1.3.0-2009-06-13], +AC_INIT([OpenAxiom], [1.3.0-2009-06-14], [open-axiom-bugs@lists.sf.net]) @ diff --git a/src/ChangeLog b/src/ChangeLog index 87ae21c9..afa502b3 100644 --- a/src/ChangeLog +++ b/src/ChangeLog @@ -1,3 +1,24 @@ +2009-06-14 Gabriel Dos Reis <gdr@cs.tamu.edu> + + Add support for existential type recovery. + * interp/compiler.boot (compRecoverDomain): New. Split from + compRecoverGuard. + (compRecoverGuard): Split. Handle existential type recovery. + (compScheme): New. Register as compiler. + * interp/g-opt.boot (optLET*): New. Turn into LET-form if + appropriate. Register as backend transformer. + * interp/fnewmeta.lisp (|PARSE-Scheme|): New. + (|PARSE-Quantifier|): Likewise. + (|PARSE-QuantifiedVariableList|): Likewise. + (|PARSE-QuantifiedVariable|): Likewise. + * interp/metalex.lisp (KEYWORDS): Add 'forall' and 'exist' as new + keywords. + * interp/newaux.lisp: Register parser for expression schemes. + * algebra/any.spad.pamphlet (=$Any): If the underlying domain has + BasicType, use that equality operator. + (coerce$Any): If the underlying domain has CoercibleTo OutputForm + then use it. + 2009-06-13 Gabriel Dos Reis <gdr@cs.tamu.edu> * algebra/any.spad.pamphlet (AnyFunctions1): Remove `pretend' diff --git a/src/algebra/any.spad.pamphlet b/src/algebra/any.spad.pamphlet index e7818eb2..b15f486f 100644 --- a/src/algebra/any.spad.pamphlet +++ b/src/algebra/any.spad.pamphlet @@ -143,6 +143,7 @@ import None )abbrev domain ANY Any ++ Author: Robert S. Sutor ++ Date Created: +++ Date Last Updated: June 14, 2009. ++ Change History: ++ Basic Functions: any, domainOf, objectOf, dom, obj, showTypeInOutput ++ Related Constructors: AnyFunctions1 @@ -191,7 +192,10 @@ Any(): SetCategory with obj x == x.ob dom x == x.dm domainOf x == x.dm pretend OutputForm - x = y == (x.dm = y.dm) and EQ(x.ob, y.ob)$Lisp + x = y == + case (x,y) is + (x': exist(S: BasicType) . S, y': S) => x' = y' + otherwise => EQ(x,y)$Foreign(Builtin) objectOf(x : %) : OutputForm == spad2BootCoerce(x.ob, x.dm, @@ -203,7 +207,10 @@ Any(): SetCategory with "Type of object will not be displayed in output of a member of Any" coerce(x):OutputForm == - obj1 : OutputForm := objectOf x + obj1 : OutputForm := + case x is + x': exist(S: CoercibleTo OutputForm) . S => x'::OutputForm + otherwise => (x.ob pretend SExpression)::OutputForm not deref printTypeInOutputP => obj1 dom1 := p:Symbol := prefix2String(devaluate(x.dm)$Lisp)$Lisp diff --git a/src/interp/compiler.boot b/src/interp/compiler.boot index 22c5471c..43433524 100644 --- a/src/interp/compiler.boot +++ b/src/interp/compiler.boot @@ -1995,6 +1995,22 @@ compRetractGuard(x,t,sn,sm,e) == [caseCode, [[x,restrictCode]],e,envFalse] +++ Subroutine of compRecoverGuard. The parameters and the result +++ have the same meaning as in compRecoverGuard. +++ Note: a value of type Any is a dotted pair (dom . val) where +++ `dom' is a devaluated form of the domain of `val'. +compRecoverDomain(x,t,sn,e) == + -- 1. We recover domains only. + not isDomainForm(t,e) => + stackAndThrow('"Form %1b does not designate a domain",[t]) + caseCode := ["EQUAL",["devaluate",t],["CAR",sn]] + -- 2. Declare `x'. + originalEnv := e + [.,.,e] := compMakeDeclaration(x,t,e) or return nil + e := put(x,"value",[genSomeVariable(),t,$noEnv],e) + -- 3. Assemble the result + [caseCode,[[x,["CDR",sn]]],e,originalEnv] + ++ Subroutine of compAlternativeGuardItem, responsible for ++ compiling a guad item of the form ++ x: t @@ -2014,16 +2030,35 @@ compRecoverGuard(x,t,sn,sm,e) == -- for `x' under the condition that sm is Any, and the -- underlying type is t. -- - -- 1. Evaluate the recovery condition - sm ^= $Any => + -- 0. Type recovery is for expressions of type 'Any'. + (sm = "$" => $functorForm; sm) ^= $Any => stackAndThrow('"Scrutinee must be of type %b Any %d in type recovery alternative of case pattern",nil) - caseCode := ["EQUAL",["devaluate",t],["objMode",sn]] - -- 2. Declare `x'. - originalEnv := e - [.,.,e] := compMakeDeclaration(x,t,e) or return nil - e := put(x,"value",[genSomeVariable(),t,$noEnv],e) - -- 3. Assemble the result - [caseCode,[[x,["objVal",sn]]],e,originalEnv] + -- 1. Do some preprocessing if this is existential type recovery. + t is ["%Exist",var,t'] => + var isnt [":",var',cat'] => + stackAndThrow('"Sorry: Only univariate type schemes are supported in this context",nil) + -- We have a univariate type scheme. At the moment we insist + -- that the body of the type scheme be identical to the type + -- variable. This restriction should be lifted in future work. + not IDENTP t' or t' ^= var' => + stackAndThrow('"Sorry: type %1b too complex",[t']) + not isCategoryForm(cat',e) => + stackAndThrow('"Expression %1b does not designate a category",[cat']) + getmode(var',e) => + stackAndThrow('"You cannot redeclare identifier %1b",[var']) + -- Extract the type component. Here note that we use a wider + -- assignment scope (e.g. "%LET") as opposed to local assignment + -- because the recovered type may be needed in the body of + -- the alternative. + varDef := ["%LET",[":",var',$Type], + [["elt",["Foreign","Builtin"],"evalDomain"], + [["elt",["Foreign","Builtin"],"CAR"], sn]]] + [def,.,e] := compOrCroak(varDef,$EmptyMode,e) + [hasTest,.,e] := compOrCroak(["has",var',cat'],$EmptyMode,e) + [guard,inits,e,envFalse] := compRecoverDomain(x,var',sn,e) + [["PROGN",def,hasTest],inits,e,envFalse] + -- 2. Hand it to whoever is in charge. + compRecoverDomain(x,t,sn,e) warnUnreachableAlternative pat == stackWarning('"Alternative with pattern %1b will not be reached",[pat]) @@ -2147,6 +2182,9 @@ compMatch(["%Match",subject,altBlock],m,env) == ["COND",:nreverse altsCode]] [code,m,savedEnv] +++ Compile the form scheme `x'. +compScheme(x,m,e) == + stackSemanticError(["Sorry: Expression schemes are not supported in this context"],nil) --% --% Inline Requests @@ -2556,6 +2594,8 @@ for x in [["|", :"compSuchthat"],_ ["per",:"compPer"],_ ["rep",:"compRep"],_ ["%Comma",:"compComma"],_ + ["%Exist", : "compScheme"] , _ + ["%Forall", : "compSceheme"] , _ ["%Match",:"compMatch"],_ ["%SignatureImport",:"compSignatureImport"],_ ["[||]", :"compileQuasiquote"]] repeat diff --git a/src/interp/fnewmeta.lisp b/src/interp/fnewmeta.lisp index 60027f80..e6af7e4c 100644 --- a/src/interp/fnewmeta.lisp +++ b/src/interp/fnewmeta.lisp @@ -474,6 +474,48 @@ (PUSH-REDUCTION '|PARSE-Inline| (CONS '|%Inline| (CONS (POP-STACK-1) NIL))))) +;; quantified types. At the moment, these are used only in +;; pattern-mathing cases. +;; -- gdr, 2009-06-14. +(DEFUN |PARSE-Scheme| () + (OR (AND (|PARSE-Quantifier|) + (MUST (|PARSE-QuantifiedVariableList|)) + (MUST (MATCH-ADVANCE-STRING ".")) + (MUST (|PARSE-Application|)) + (MUST (PUSH-REDUCTION '|PARSE-Forall| + (CONS (POP-STACK-3) + (CONS (POP-STACK-2) + (CONS (POP-STACK-1) NIL)))))) + (|PARSE-Application|))) + +(DEFUN |PARSE-Quantifier| () + (OR (AND (MATCH-ADVANCE-STRING "forall") + (MUST (PUSH-REDUCTION '|PARSE-Quantifier| '|%Forall|))) + (AND (MATCH-ADVANCE-STRING "exist") + (MUST (PUSH-REDUCTION '|PARSE-Quantifier| '|%Exist|))))) + +(DEFUN |PARSE-QuantifiedVariableList| () + (AND (MATCH-ADVANCE-STRING "(") + (MUST (|PARSE-QuantifiedVariable|)) + (OPTIONAL + (AND (STAR REPEATOR + (AND (MATCH-ADVANCE-STRING ",") + (MUST (|PARSE-QuantifiedVariable|)))) + (PUSH-REDUCTION '|PARSE-QuantifiedVariableList| + (CONS '|%Sequence| + (CONS (POP-STACK-2) + (APPEND (POP-STACK-1) NIL)))))) + (MUST (MATCH-ADVANCE-STRING ")")))) + +(DEFUN |PARSE-QuantifiedVariable| () + (AND (PARSE-IDENTIFIER) + (MUST (MATCH-ADVANCE-STRING ":")) + (MUST (|PARSE-Application|)) + (MUST (PUSH-REDUCTION '|PARSE-QuantifiedVariable| + (CONS '|:| + (CONS (POP-STACK-2) + (CONS (POP-STACK-1) NIL))))))) + (DEFUN |PARSE-Infix| () (AND (PUSH-REDUCTION '|PARSE-Infix| (CURRENT-SYMBOL)) (ACTION (ADVANCE-TOKEN)) (OPTIONAL (|PARSE-TokTail|)) diff --git a/src/interp/g-opt.boot b/src/interp/g-opt.boot index c51987dc..0fb44255 100644 --- a/src/interp/g-opt.boot +++ b/src/interp/g-opt.boot @@ -492,6 +492,15 @@ optLET u == rplac(rest def, second def) SUBLIS(inits,body) +optLET_* form == + form isnt ["LET*",:.] => form + ok := true + while ok for [[var,.],:inits] in tails second form repeat + if CONTAINED(var,inits) then ok := false + not ok => form + rplac(first form,"LET") + optLET form + lispize x == first optimize [x] --% optimizer hash table @@ -499,6 +508,7 @@ lispize x == first optimize [x] for x in '( (call optCall) _ (SEQ optSEQ)_ (LET optLET)_ + (LET_* optLET_*)_ (MINUS optMINUS)_ (QSMINUS optQSMINUS)_ (_- opt_-)_ diff --git a/src/interp/metalex.lisp b/src/interp/metalex.lisp index 690c6243..27b82522 100644 --- a/src/interp/metalex.lisp +++ b/src/interp/metalex.lisp @@ -570,7 +570,7 @@ empty (if File-Closed (return nil)) (defconstant Keywords - '(|or| |and| |isnt| |is| |when| |where| + '(|or| |and| |isnt| |is| |when| |where| |forall| |exist| |has| |with| |add| |case| |in| |by| |pretend| |mod| |exquo| |div| |quo| |else| |rem| |then| |suchthat| |if| |yield| |iterate| |from| |exit| |leave| |return| diff --git a/src/interp/newaux.lisp b/src/interp/newaux.lisp index a3d2ef79..db00f018 100644 --- a/src/interp/newaux.lisp +++ b/src/interp/newaux.lisp @@ -135,6 +135,8 @@ (|repeat| 130 190 (|PARSE-Loop|)) (|import| 120 0 (|PARSE-Import|) ) (|inline| 120 0 (|PARSE-Inline|) ) + (|forall| 998 999 (|PARSE-Scheme|)) + (|exist| 998 999 (|PARSE-Scheme|)) (|unless|) (|add| 900 120) (|with| 1000 300 (|PARSE-With|)) |