diff options
author | dos-reis <gdr@axiomatics.org> | 2009-06-14 12:26:50 +0000 |
---|---|---|
committer | dos-reis <gdr@axiomatics.org> | 2009-06-14 12:26:50 +0000 |
commit | 12b1b74f1e952694c8f182eb2b4ab369f6005ddf (patch) | |
tree | 70446f3ea05944feb6beb68dd35f27573d9ee6f6 /src | |
parent | 700e13eca3eaac940000e3529d761dc7b4b15e5e (diff) | |
download | open-axiom-12b1b74f1e952694c8f182eb2b4ab369f6005ddf.tar.gz |
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.
Diffstat (limited to 'src')
-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 |
7 files changed, 134 insertions, 12 deletions
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|)) |