From 12b1b74f1e952694c8f182eb2b4ab369f6005ddf Mon Sep 17 00:00:00 2001 From: dos-reis Date: Sun, 14 Jun 2009 12:26:50 +0000 Subject: 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. --- src/interp/compiler.boot | 58 ++++++++++++++++++++++++++++++++++++++++-------- src/interp/fnewmeta.lisp | 42 +++++++++++++++++++++++++++++++++++ src/interp/g-opt.boot | 10 +++++++++ src/interp/metalex.lisp | 2 +- src/interp/newaux.lisp | 2 ++ 5 files changed, 104 insertions(+), 10 deletions(-) (limited to 'src/interp') 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|)) -- cgit v1.2.3