diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/interp/cparse.boot | 30 | ||||
| -rw-r--r-- | src/interp/pf2sex.boot | 12 | ||||
| -rw-r--r-- | src/interp/ptrees.boot | 8 | ||||
| -rw-r--r-- | src/interp/scan.boot | 35 |
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) |