2008-07-24 Gabriel Dos Reis <gdr@cs.tamu.edu>

	* interp/scan.boot: Tidy.
	* interp/ptrees.boot: Define AST for type schemes.
	* interp/cparse.boot (npType): Parse type schemes.
	(npQuantifierVariable): New.
	(npADD): Accept only monotypes.
	* interp/pf2sex.boot (pf2Sex1): Handle type schemes.
	(pfQuantified2Sex): New.

2008-07-23  Gabriel Dos Reis  <gdr@cs.tamu.edu>

	* interp/cparse.boot (npMonoType): Rename from npType.

4 files changed, 60 insertions, 25 deletions

diff --git a/src/interp/cparse.boot b/src/interp/cparse.boot
index ab65c697..d21743eb 100644
--- a/src/interp/cparse.boot
+++ b/src/interp/cparse.boot
@@ -1,6 +1,6 @@
 -- Copyright (c) 1991-2002, The Numerical ALgorithms Group Ltd.
 -- All rights reserved.
--- Copyright (C) 2007, Gabriel Dos Reis.
+-- Copyright (C) 2007-2008, Gabriel Dos Reis.
 -- All rights reserved.
 --
 -- Redistribution and use in source and binary forms, with or without
@@ -532,11 +532,24 @@ npLogical()   ==  npLeftAssoc('(OR ),function npDisjand)
 npSuch() == npLeftAssoc( '(BAR),function npLogical)
 npMatch()   ==    npLeftAssoc ('(IS ISNT ), function npSuch)
 
-npType()    ==  npMatch()  and
+++ Parse a type expression
+++   Type:
+++     MonoType
+++     QuantifiedVariable Type
+npType() ==
+  npEqPeek "FORALL" =>
+    npQuantifierVariable "FORALL" and npType() and
+      npPush %Forall(npPop2(), npPop1())
+  npEqPeek "EXIST" =>
+    npQuantifierVariable "EXIST" and npType() and
+      npPush %Exist(npPop2(), npPop1())
+  npMonoType()
+
+npMonoType() ==  npMatch()  and
                 a:=npPop1()
                 npWith(a) or npPush a
 
-npADD()    ==   npType() and
+npADD()    ==   npMonoType() and
                 a:=npPop1()
                 npAdd(a) or npPush a
 
@@ -793,6 +806,17 @@ npVariable()== npParenthesized function npVariablelist or
 
 npVariablelist()== npListing function npVariableName
 
+++ Parse binders of a quantified expression
+++   QuantifiedVariable:
+++      Quantifier Variable DOT
+++   Quantifier:
+++      EXIST
+++      FORALL
+npQuantifierVariable quantifier ==
+  npEqKey quantifier and (npVariable() or npTrap())
+    and npEqKey "DOT"
+
+
 npListing (p)==npList(p,"COMMA",function pfListOf)
 npQualified(f)==
     if FUNCALL f
diff --git a/src/interp/pf2sex.boot b/src/interp/pf2sex.boot
index 85ebedb1..bcb508f5 100644
--- a/src/interp/pf2sex.boot
+++ b/src/interp/pf2sex.boot
@@ -1,6 +1,6 @@
 -- Copyright (c) 1991-2002, The Numerical ALgorithms Group Ltd.
 -- All rights reserved.
--- Copyright (C) 2007, Gabriel Dos Reis.
+-- Copyright (C) 2007-2008, Gabriel Dos Reis.
 -- All rights reserved.
 --
 -- Redistribution and use in source and binary forms, with or without
@@ -165,7 +165,10 @@ pf2Sex1 pf ==
   -- the user to figure out what happened.
   pfAbSynOp(pf) = "command" => tokPart(pf)
 
-  keyedSystemError('"S2GE0017", ['"pf2Sex1"])
+  case pf of
+    %Exist(vars,expr) => pfQuantified2Sex("%Exist",vars,expr)
+    %Forall(vars,expr) => pfQuantified2Sex("%Forall",vars,expr)
+    otherwise => keyedSystemError('"S2GE0017", ['"pf2Sex1"])
 
 pfLiteral2Sex pf ==
   type := pfLiteralClass pf
@@ -479,6 +482,5 @@ pfSuchThat2Sex args ==
   $predicateList := [[name, lhsSex, :rhsSex], :$predicateList]
   name
 
-
-
-
+pfQuantified2Sex(quantifier,vars,expr) ==
+  [quantifier, [pf2Sex1 t for t in pfParts vars], pf2Sex1 expr]
diff --git a/src/interp/ptrees.boot b/src/interp/ptrees.boot
index fc4f57e1..ed40c466 100644
--- a/src/interp/ptrees.boot
+++ b/src/interp/ptrees.boot
@@ -1,6 +1,6 @@
 -- Copyright (c) 1991-2002, The Numerical ALgorithms Group Ltd.
 -- All rights reserved.
--- Copyright (C) 2007, Gabriel Dos Reis.
+-- Copyright (C) 2007-2008, Gabriel Dos Reis.
 -- All rights reserved.
 --
 -- Redistribution and use in source and binary forms, with or without
@@ -50,6 +50,12 @@
 import posit
 import serror
 namespace BOOT
+module ptrees
+
+--% This structure is incomplet
+structure %Ast ==
+  %Exist(%Vars,%Ast)
+  %Forall(%Vars,%Ast)
 
 --% SPECIAL NODES
 pfListOf x          == pfTree('listOf,x)
diff --git a/src/interp/scan.boot b/src/interp/scan.boot
index 34dc2bb6..188184c8 100644
--- a/src/interp/scan.boot
+++ b/src/interp/scan.boot
@@ -1,6 +1,6 @@
 -- Copyright (c) 1991-2002, The Numerical ALgorithms Group Ltd.
 -- All rights reserved.
--- Copyright (C) 2007, Gabriel Dos Reis.
+-- Copyright (C) 2007-2008, Gabriel Dos Reis.
 -- All rights reserved.
 --
 -- Redistribution and use in source and binary forms, with or without
@@ -36,26 +36,27 @@ import bits
 import dq
 import incl
 namespace BOOT
+module scan
 
 --% Separators
 
-$SPACE       := QENUM('"    ", 0)
-ESCAPE      := QENUM('"__  ", 0)
-STRING_CHAR := QENUM('"_"  ", 0)
-PLUSCOMMENT := QENUM('"+   ", 0)
-MINUSCOMMENT:= QENUM('"-   ", 0)
-RADIX_CHAR  := QENUM('"r   ", 0)
-DOT         := QENUM('".   ", 0)
-EXPONENT1   := QENUM('"E   ", 0)
-EXPONENT2   := QENUM('"e   ", 0)
-CLOSEPAREN  := QENUM('")   ", 0)
-CLOSEANGLE  := QENUM('">   ", 0)
-QUESTION    := QENUM('"?   ",0)
+$SPACE       == QENUM('"    ", 0)
+ESCAPE       == QENUM('"__  ", 0)
+STRING_CHAR  == QENUM('"_"  ", 0)
+PLUSCOMMENT  == QENUM('"+   ", 0)
+MINUSCOMMENT == QENUM('"-   ", 0)
+RADIX_CHAR   == QENUM('"r   ", 0)
+DOT          == QENUM('".   ", 0)
+EXPONENT1    == QENUM('"E   ", 0)
+EXPONENT2    == QENUM('"e   ", 0)
+CLOSEPAREN   == QENUM('")   ", 0)
+CLOSEANGLE   == QENUM('">   ", 0)
+QUESTION     == QENUM('"?   ",0)
 
 
 --% Keywords
 
-scanKeyWords := [ _
+scanKeyWords == [ _
            ['"add",      "ADD" ],_
            ['"and",      "AND" ],_
            ['"break",   "BREAK" ],_
@@ -65,8 +66,10 @@ scanKeyWords := [ _
            ['"define",  "DEFN" ],_
            ['"do",        "DO"],_
            ['"else",    "ELSE" ],_
+           ['"exist",   "EXIST"],_
            ['"exit",    "EXIT" ],_
            ['"export","EXPORT" ],_
+           ['"forall", "FORALL"],_
            ['"for",      "FOR" ],_
            ['"free",    "FREE" ],_
            ['"from",    "FROM" ],_
@@ -294,7 +297,7 @@ lineoftoks(s)==
       else cons([[toks,s]],$r)
 
 
-scanToken () ==
+scanToken() ==
       ln:=$ln
       c:=QENUM($ln,$n)
       linepos:=$linepos
@@ -451,7 +454,7 @@ scanPossFloat (w)==
        w:=spleI(function digit?)
        scanExponent('"0",w)
 
-scanCloser:=[")","}","]","|)","|}","|]"]
+scanCloser == [")","}","]","|)","|}","|]"]
 
 scanCloser? w== MEMQ(keyword w,scanCloser)