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.

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|))