[open-axiom-commit] SF.net SVN: open-axiom:[1209] trunk
A system for computer algebra and symbolic mathematics
Brought to you by:
dos-reis
Menu
▾
▴
[open-axiom-commit] SF.net SVN: open-axiom:[1209] trunk
|
From: <dos...@us...> - 2009-06-14 13:16:10
|
Revision: 1209
http://open-axiom.svn.sourceforge.net/open-axiom/?rev=1209&view=rev
Author: dos-reis
Date: 2009-06-14 12:26:50 +0000 (Sun, 14 Jun 2009)
Log Message:
-----------
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.
Modified Paths:
--------------
trunk/configure
trunk/configure.ac
trunk/configure.ac.pamphlet
trunk/src/ChangeLog
trunk/src/algebra/any.spad.pamphlet
trunk/src/interp/compiler.boot
trunk/src/interp/fnewmeta.lisp
trunk/src/interp/g-opt.boot
trunk/src/interp/metalex.lisp
trunk/src/interp/newaux.lisp
Modified: trunk/configure
===================================================================
--- trunk/configure 2009-06-13 21:53:21 UTC (rev 1208)
+++ trunk/configure 2009-06-14 12:26:50 UTC (rev 1209)
@@ -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 <ope...@li...>.
#
@@ -745,8 +745,8 @@
# 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='ope...@li...'
ac_unique_file="src/Makefile.pamphlet"
@@ -1500,7 +1500,7 @@
# 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 @@
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 @@
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 @@
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 @@
# 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 @@
_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'`\\"
Modified: trunk/configure.ac
===================================================================
--- trunk/configure.ac 2009-06-13 21:53:21 UTC (rev 1208)
+++ trunk/configure.ac 2009-06-14 12:26:50 UTC (rev 1209)
@@ -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],
[ope...@li...])
AC_CONFIG_AUX_DIR(config)
Modified: trunk/configure.ac.pamphlet
===================================================================
--- trunk/configure.ac.pamphlet 2009-06-13 21:53:21 UTC (rev 1208)
+++ trunk/configure.ac.pamphlet 2009-06-14 12:26:50 UTC (rev 1209)
@@ -1131,7 +1131,7 @@
<<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],
[ope...@li...])
@
Modified: trunk/src/ChangeLog
===================================================================
--- trunk/src/ChangeLog 2009-06-13 21:53:21 UTC (rev 1208)
+++ trunk/src/ChangeLog 2009-06-14 12:26:50 UTC (rev 1209)
@@ -1,3 +1,24 @@
+2009-06-14 Gabriel Dos Reis <gd...@cs...>
+
+ 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 <gd...@cs...>
* algebra/any.spad.pamphlet (AnyFunctions1): Remove `pretend'
Modified: trunk/src/algebra/any.spad.pamphlet
===================================================================
--- trunk/src/algebra/any.spad.pamphlet 2009-06-13 21:53:21 UTC (rev 1208)
+++ trunk/src/algebra/any.spad.pamphlet 2009-06-14 12:26:50 UTC (rev 1209)
@@ -143,6 +143,7 @@
)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 @@
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 @@
"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
Modified: trunk/src/interp/compiler.boot
===================================================================
--- trunk/src/interp/compiler.boot 2009-06-13 21:53:21 UTC (rev 1208)
+++ trunk/src/interp/compiler.boot 2009-06-14 12:26:50 UTC (rev 1209)
@@ -1995,6 +1995,22 @@
[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 @@
-- 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 @@
["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 @@
["per",:"compPer"],_
["rep",:"compRep"],_
["%Comma",:"compComma"],_
+ ["%Exist", : "compScheme"] , _
+ ["%Forall", : "compSceheme"] , _
["%Match",:"compMatch"],_
["%SignatureImport",:"compSignatureImport"],_
["[||]", :"compileQuasiquote"]] repeat
Modified: trunk/src/interp/fnewmeta.lisp
===================================================================
--- trunk/src/interp/fnewmeta.lisp 2009-06-13 21:53:21 UTC (rev 1208)
+++ trunk/src/interp/fnewmeta.lisp 2009-06-14 12:26:50 UTC (rev 1209)
@@ -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|))
Modified: trunk/src/interp/g-opt.boot
===================================================================
--- trunk/src/interp/g-opt.boot 2009-06-13 21:53:21 UTC (rev 1208)
+++ trunk/src/interp/g-opt.boot 2009-06-14 12:26:50 UTC (rev 1209)
@@ -492,6 +492,15 @@
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 @@
for x in '( (call optCall) _
(SEQ optSEQ)_
(LET optLET)_
+ (LET_* optLET_*)_
(MINUS optMINUS)_
(QSMINUS optQSMINUS)_
(_- opt_-)_
Modified: trunk/src/interp/metalex.lisp
===================================================================
--- trunk/src/interp/metalex.lisp 2009-06-13 21:53:21 UTC (rev 1208)
+++ trunk/src/interp/metalex.lisp 2009-06-14 12:26:50 UTC (rev 1209)
@@ -570,7 +570,7 @@
(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|
Modified: trunk/src/interp/newaux.lisp
===================================================================
--- trunk/src/interp/newaux.lisp 2009-06-13 21:53:21 UTC (rev 1208)
+++ trunk/src/interp/newaux.lisp 2009-06-14 12:26:50 UTC (rev 1209)
@@ -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|))
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|