From 12b1b74f1e952694c8f182eb2b4ab369f6005ddf Mon Sep 17 00:00:00 2001
From: dos-reis <gdr@axiomatics.org>
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/fnewmeta.lisp | 42 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 42 insertions(+)

(limited to 'src/interp/fnewmeta.lisp')

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|))
-- 
cgit v1.2.3