From f04d1f935b8e4b87ca156932b723a323ef8808d9 Mon Sep 17 00:00:00 2001
From: dos-reis <gdr@axiomatics.org>
Date: Fri, 25 Jul 2008 02:06:33 +0000
Subject: 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.
---
src/interp/cparse.boot | 30 +++++++++++++++++++++++++++---
src/interp/pf2sex.boot | 12 +++++++-----
src/interp/ptrees.boot | 8 +++++++-
src/interp/scan.boot | 35 +++++++++++++++++++----------------
4 files changed, 60 insertions(+), 25 deletions(-)
(limited to 'src')
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)
--
cgit v1.2.3