* algebra/syntax.spad.pamphlet (SpadAst): New.

	* algebra/Makefile.pamphlet (axiom_algebra_layer_user): Add SPADAST.
	* share/algebra: Update algebra databases.

4 files changed, 148 insertions, 38 deletions

diff --git a/src/algebra/Makefile.in b/src/algebra/Makefile.in
index db67d2ad..0e82462f 100644
--- a/src/algebra/Makefile.in
+++ b/src/algebra/Makefile.in
@@ -825,7 +825,7 @@ axiom_algebra_layer_user =  \
 	LSTAST   EXITAST  RETAST   SEGAST   PRTDAST  CRCAST   \
 	LETAST   SUCHAST  RDUCEAST COLONAST ADDAST   CAPSLAST \
 	CASEAST  HASAST   ISAST    CATAST   WHEREAST COMMAAST \
-	QQUTAST  DEFAST   MACROAST SPADXPT
+	QQUTAST  DEFAST   MACROAST SPADXPT  SPADAST
 
 axiom_algebra_layer_user_nrlibs = \
 	$(addsuffix .NRLIB/code.$(FASLEXT),$(axiom_algebra_layer_user))
@@ -843,7 +843,7 @@ ATTRAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
 TYPEAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
 IMPTAST.NRLIB/code.$(FASLEXT): $(OUT)/TYPEAST.$(FASLEXT)
 MAPPAST.NRLIB/code.$(FASLEXT): $(OUT)/TYPEAST.$(FASLEXT)
-SIGAST.NRLIB/code.$(FASLEXT): $(OUT)/SIG.$(FASLEXT)
+SIGAST.NRLIB/code.$(FASLEXT): $(OUT)/SIG.$(FASLEXT) $(OUT)/IDENT.$(FASLEXT)
 JOINAST.NRLIB/code.$(FASLEXT): $(OUT)/TYPEAST.$(FASLEXT)
 IFAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
 RPTAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
@@ -865,7 +865,7 @@ COLONAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
 ADDAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
 CAPSLAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
 CASEAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
-HASEAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
+HASAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
 ISAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
 CATAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
 WHEREAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
@@ -873,6 +873,13 @@ COMMAAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
 QQUTAST.NRLIB/code.$(FASLEXT): $(OUT)/SASTCAT.$(FASLEXT)
 DEFAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
 MACROAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
+SPADAST.NRLIB/code.$(FASLEXT): \
+  $(addprefix $(OUT)/,$(addsuffix .$(FASLEXT), \
+     IMPTAST DEFAST MACROAST WHEREAST  CATAST CAPSLAST \
+     SIGAST ATTRAST MAPPAST IFAST RPTAST WHILEAST INAST \
+     CLLCTAST LSTAST EXITAST RETAST CRCEAST PRTDAST RSTRCAST \
+     SEGAST SEQAST LETAST SUCHTAST COLONAST CASEAST HASAST \
+     ISAST))
 
 .PHONY: all all-algebra mkdir-output-directory
 all: all-ax
diff --git a/src/algebra/Makefile.pamphlet b/src/algebra/Makefile.pamphlet
index c4a89300..11bc702a 100644
--- a/src/algebra/Makefile.pamphlet
+++ b/src/algebra/Makefile.pamphlet
@@ -1252,7 +1252,7 @@ axiom_algebra_layer_user =  \
 	LSTAST   EXITAST  RETAST   SEGAST   PRTDAST  CRCAST   \
 	LETAST   SUCHAST  RDUCEAST COLONAST ADDAST   CAPSLAST \
 	CASEAST  HASAST   ISAST    CATAST   WHEREAST COMMAAST \
-	QQUTAST  DEFAST   MACROAST SPADXPT
+	QQUTAST  DEFAST   MACROAST SPADXPT  SPADAST
 
 axiom_algebra_layer_user_nrlibs = \
 	$(addsuffix .NRLIB/code.$(FASLEXT),$(axiom_algebra_layer_user))
@@ -1270,7 +1270,7 @@ ATTRAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
 TYPEAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
 IMPTAST.NRLIB/code.$(FASLEXT): $(OUT)/TYPEAST.$(FASLEXT)
 MAPPAST.NRLIB/code.$(FASLEXT): $(OUT)/TYPEAST.$(FASLEXT)
-SIGAST.NRLIB/code.$(FASLEXT): $(OUT)/SIG.$(FASLEXT)
+SIGAST.NRLIB/code.$(FASLEXT): $(OUT)/SIG.$(FASLEXT) $(OUT)/IDENT.$(FASLEXT)
 JOINAST.NRLIB/code.$(FASLEXT): $(OUT)/TYPEAST.$(FASLEXT)
 IFAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
 RPTAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
@@ -1292,7 +1292,7 @@ COLONAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
 ADDAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
 CAPSLAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
 CASEAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
-HASEAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
+HASAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
 ISAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
 CATAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
 WHEREAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
@@ -1300,6 +1300,13 @@ COMMAAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
 QQUTAST.NRLIB/code.$(FASLEXT): $(OUT)/SASTCAT.$(FASLEXT)
 DEFAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
 MACROAST.NRLIB/code.$(FASLEXT): $(OUT)/SPADXPT.$(FASLEXT)
+SPADAST.NRLIB/code.$(FASLEXT): \
+  $(addprefix $(OUT)/,$(addsuffix .$(FASLEXT), \
+     IMPTAST DEFAST MACROAST WHEREAST  CATAST CAPSLAST \
+     SIGAST ATTRAST MAPPAST IFAST RPTAST WHILEAST INAST \
+     CLLCTAST LSTAST EXITAST RETAST CRCEAST PRTDAST RSTRCAST \
+     SEGAST SEQAST LETAST SUCHTAST COLONAST CASEAST HASAST \
+     ISAST))
 @
 
 \section{Broken Files}
diff --git a/src/algebra/boolean.spad.pamphlet b/src/algebra/boolean.spad.pamphlet
index d685c2cf..cee0e13d 100644
--- a/src/algebra/boolean.spad.pamphlet
+++ b/src/algebra/boolean.spad.pamphlet
@@ -560,6 +560,8 @@ KleeneTrivalentLogic(): Public == Private where
 @
 
 
+
+
 \section{License}
 
 <<license>>=
diff --git a/src/algebra/syntax.spad.pamphlet b/src/algebra/syntax.spad.pamphlet
index e38347eb..0c2da993 100644
--- a/src/algebra/syntax.spad.pamphlet
+++ b/src/algebra/syntax.spad.pamphlet
@@ -555,170 +555,170 @@ SpadSyntaxCategory(): Category == AbstractSyntaxCategory
 ++ Description: This category describes the exported
 ++   signatures of the SpadAst domain.
 SpadAstExports(): Category == Join(SpadSyntaxCategory, UnionType) with
-   _case: (%, ImportAst()) -> Boolean
+  _case: (%, [|ImportAst()|]) -> Boolean
     ++ s case ImportAst holds if `s' represents an `import' statement.
   autoCoerce: % -> ImportAst()
     ++ autoCoerce(s) returns the ImportAst view of `s'.  Left at the
     ++ discretion of the compiler.
 
-   _case: (%, DefinitionAst()) -> Boolean
+  _case: (%, [|DefinitionAst()|]) -> Boolean
     ++ s case DefinitionAst holds if `s' represents a definition.
   autoCoerce: % -> DefinitionAst()
     ++ autoCoerce(s) returns the DefinitionAst view of `s'.  Left at the
     ++ discretion of the compiler.
 
-   _case: (%, MacroAst()) -> Boolean
+  _case: (%, [|MacroAst()|]) -> Boolean
     ++ s case MacroAst holds if `s' represents a macro definition.
   autoCoerce: % -> MacroAst()
     ++ autoCoerce(s) returns the MacroAst view of `s'.  Left at the
     ++ discretion of the compiler.
 
-   _case: (%, WhereAst()) -> Boolean
+  _case: (%, [|WhereAst()|]) -> Boolean
     ++ s case WhereAst holds if `s' represents an expression with
     ++ local definitions.
   autoCoerce: % -> WhereAst()
     ++ autoCoerce(s) returns the WhereAst view of `s'.  Left at the
     ++ discretion of the compiler.
 
-   _case: (%, CategoryAst()) -> Boolean
+  _case: (%, [|CategoryAst()|]) -> Boolean
     ++ s case CategoryAst holds if `s' represents an unnamed category.
   autoCoerce: % -> CategoryAst()
     ++ autoCoerce(s) returns the CategoryAst view of `s'.  Left at the
     ++ discretion of the compiler.
 
-   _case: (%, CapsuleAst()) -> Boolean
+  _case: (%, [|CapsuleAst()|]) -> Boolean
     ++ s case CapsuleAst holds if `s' represents a domain capsule.
   autoCoerce: % -> CapsuleAst()
     ++ autoCoerce(s) returns the CapsuleAst view of `s'.  Left at the
     ++ discretion of the compiler.
 
-   _case: (%, SignatureAst()) -> Boolean
+  _case: (%, [|SignatureAst()|]) -> Boolean
     ++ s case SignatureAst holds if `s' represents a signature export.
   autoCoerce: % -> SignatureAst()
     ++ autoCoerce(s) returns the SignatureAst view of `s'.  Left at the
     ++ discretion of the compiler.
 
-   _case: (%, AttributeAst()) -> Boolean
+  _case: (%, [|AttributeAst()|]) -> Boolean
     ++ s case AttributeAst holds if `s' represents an attribute.
   autoCoerce: % -> AttributeAst()
     ++ autoCoerce(s) returns the AttributeAst view of `s'.  Left at the
     ++ discretion of the compiler.
 
-   _case: (%, MappingAst()) -> Boolean
+  _case: (%, [|MappingAst()|]) -> Boolean
     ++ s case MappingAst holds if `s' represents a mapping type.
   autoCoerce: % -> MappingAst()
     ++ autoCoerce(s) returns the MappingAst view of `s'.  Left at the
     ++ discretion of the compiler.
 
-   _case: (%, IfAst()) -> Boolean
+  _case: (%, [|IfAst()|]) -> Boolean
     ++ s case IfAst holds if `s' represents an if-statement.
   autoCoerce: % -> IfAst()
     ++ autoCoerce(s) returns the IfAst view of `s'.  Left at the
     ++ discretion of the compiler.
 
-   _case: (%, RepeatAst()) -> Boolean
+  _case: (%, [|RepeatAst()|]) -> Boolean
     ++ s case RepeatAst holds if `s' represents an repeat-loop.
   autoCoerce: % -> RepeatAst()
     ++ autoCoerce(s) returns the RepeatAst view of `s'.  Left at the
     ++ discretion of the compiler.
 
-   _case: (%, WhileAst()) -> Boolean
+  _case: (%, [|WhileAst()|]) -> Boolean
     ++ s case WhileAst holds if `s' represents a while-iterator
   autoCoerce: % -> WhileAst()
     ++ autoCoerce(s) returns the WhileAst view of `s'.  Left at the
     ++ discretion of the compiler.
 
-   _case: (%, InAst()) -> Boolean
+  _case: (%, [|InAst()|]) -> Boolean
     ++ s case InAst holds if `s' represents a in-iterator
   autoCoerce: % -> InAst()
     ++ autoCoerce(s) returns the InAst view of `s'.  Left at the
     ++ discretion of the compiler.
 
-   _case: (%, CollectAst()) -> Boolean
+  _case: (%, [|CollectAst()|]) -> Boolean
     ++ s case CollectAst holds if `s' represents a list-comprehension.
   autoCoerce: % -> CollectAst()
     ++ autoCoerce(s) returns the CollectAst view of `s'.  Left at the
     ++ discretion of the compiler.
 
-   _case: (%, ConstructAst()) -> Boolean
+  _case: (%, [|ConstructAst()|]) -> Boolean
     ++ s case ConstructAst holds if `s' represents a list-expression.
   autoCoerce: % -> ConstructAst()
     ++ autoCoerce(s) returns the ConstructAst view of `s'.  Left at the
     ++ discretion of the compiler.
 
-   _case: (%, ExitAst()) -> Boolean
+  _case: (%, [|ExitAst()|]) -> Boolean
     ++ s case ExitAst holds if `s' represents an exit-expression.
   autoCoerce: % -> ExitAst()
     ++ autoCoerce(s) returns the ExitAst view of `s'.  Left at the
     ++ discretion of the compiler.
 
-   _case: (%, ReturnAst()) -> Boolean
+  _case: (%, [|ReturnAst()|]) -> Boolean
     ++ s case ReturnAst holds if `s' represents a return-statement.
-  autoCoerce: % -> ReurnAst()
+  autoCoerce: % -> ReturnAst()
     ++ autoCoerce(s) returns the ReturnAst view of `s'.  Left at the
     ++ discretion of the compiler.
 
-   _case: (%, CoerceAst()) -> Boolean
+  _case: (%, [|CoerceAst()|]) -> Boolean
     ++ s case ReturnAst holds if `s' represents a coerce-expression.
   autoCoerce: % -> CoerceAst()
     ++ autoCoerce(s) returns the CoerceAst view of `s'.  Left at the
     ++ discretion of the compiler.
 
-   _case: (%, PretendAst()) -> Boolean
+  _case: (%, [|PretendAst()|]) -> Boolean
     ++ s case PretendAst holds if `s' represents a pretend-expression.
   autoCoerce: % -> PretendAst()
     ++ autoCoerce(s) returns the PretendAst view of `s'.  Left at the
     ++ discretion of the compiler.
 
-   _case: (%, RestrictAst()) -> Boolean
+  _case: (%, [|RestrictAst()|]) -> Boolean
     ++ s case RestrictAst holds if `s' represents a restrict-expression.
   autoCoerce: % -> RestrictAst()
     ++ autoCoerce(s) returns the RestrictAst view of `s'.  Left at the
     ++ discretion of the compiler.
 
-   _case: (%, SegmentAst()) -> Boolean
+  _case: (%, [|SegmentAst()|]) -> Boolean
     ++ s case SegmentAst holds if `s' represents a segment-expression.
   autoCoerce: % -> SegmentAst()
     ++ autoCoerce(s) returns the SegmentAst view of `s'.  Left at the
     ++ discretion of the compiler.
 
-   _case: (%, SequenceAst()) -> Boolean
+  _case: (%, [|SequenceAst()|]) -> Boolean
     ++ s case SequenceAst holds if `s' represents a sequence-of-statements.
   autoCoerce: % -> SequenceAst()
     ++ autoCoerce(s) returns the SequenceAst view of `s'.  Left at the
     ++ discretion of the compiler.
 
-   _case: (%, LetAst()) -> Boolean
+  _case: (%, [|LetAst()|]) -> Boolean
     ++ s case LetAst holds if `s' represents an assignment-expression.
   autoCoerce: % -> LetAst()
     ++ autoCoerce(s) returns the LetAst view of `s'.  Left at the
     ++ discretion of the compiler.
 
-   _case: (%, SuchThatAst()) -> Boolean
+  _case: (%, [|SuchThatAst()|]) -> Boolean
     ++ s case SuchThatAst holds if `s' represents a qualified-expression.
   autoCoerce: % -> SuchThatAst()
     ++ autoCoerce(s) returns the SuchThatAst view of `s'.  Left at the
     ++ discretion of the compiler.
 
-   _case: (%, ColonAst()) -> Boolean
+  _case: (%, [|ColonAst()|]) -> Boolean
     ++ s case ColonAst holds if `s' represents a colon-expression.
   autoCoerce: % -> ColonAst()
     ++ autoCoerce(s) returns the ColoonAst view of `s'.  Left at the
     ++ discretion of the compiler.
  
-   _case: (%, CaseAst()) -> Boolean
+  _case: (%, [|CaseAst()|]) -> Boolean
     ++ s case CaseAst holds if `s' represents a case-expression.
   autoCoerce: % -> CaseAst()
     ++ autoCoerce(s) returns the CaseAst view of `s'.  Left at the
     ++ discretion of the compiler.
  
-   _case: (%, HasAst()) -> Boolean
+  _case: (%, [|HasAst()|]) -> Boolean
     ++ s case HasAst holds if `s' represents a has-expression.
   autoCoerce: % -> HasAst()
     ++ autoCoerce(s) returns the HasAst view of `s'.  Left at the
     ++ discretion of the compiler.
  
-   _case: (%, IsAst()) -> Boolean
+  _case: (%, [|IsAst()|]) -> Boolean
     ++ s case IsAst holds if `s' represents an is-expression.
   autoCoerce: % -> IsAst()
     ++ autoCoerce(s) returns the IsAst view of `s'.  Left at the
@@ -881,13 +881,13 @@ SignatureAst(): Public == Private where
   Public ==  SpadSyntaxCategory with
     signatureAst: (Identifier, Signature) -> %
       ++ signatureAst(n,s,t) builds the signature AST n: s -> t
-    name: % -> Symbol
+    name: % -> Identifier
       ++ name(s) returns the name of the signature `s'.
     signature: % -> Signature
       ++ signature(s) returns AST of the declared signature for `s'.
   Private == add
     import List
-    Rep == Pair(Symbol, Pair(Symbol,List Signature))
+    Rep == Pair(Symbol, Pair(Identifier,List Signature))
     signatureAst(n,sig) == 
       per pair('SIGNATURE,pair(n,[sig]))
     name x == first second rep x
@@ -1303,7 +1303,7 @@ SuchThatAst(): Public == Private where
       ++ in the filter iterator syntax `e'.
   Private == add
     Rep == List Syntax
-    predicate e == second rep x
+    predicate e == second rep e
 @
 
 \subsection{The ColonAst domain}
@@ -1559,6 +1559,100 @@ MacroAst(): Public == Private where
 
 @
 
+\subsection{The SpadAst domain}
+<<domain SPADAST SpadAst>>=
+)abbrev domain SPADAST SpadAst
+SpadAst(): SpadAstExports() == add
+  isAst(x: %, tag: Symbol): Boolean ==
+    (op := getOperator(x::Syntax)) case Symbol and op = tag
+
+  x case ImportAst == isAst(x,'import)
+  autoCoerce(x: %): ImportAst == x : ImportAst
+
+  x case DefinitionAst == isAst(x,'DEF)
+  autoCoerce(x: %): DefinitionAst == x : DefinitionAst
+
+  x case MacroAst == isAst(x,'MDEF)
+  autoCoerce(x: %): MacroAst == x : MacroAst
+
+  x case WhereAst == isAst(x,'where)
+  autoCoerce(x: %): WhereAst == x : WhereAst
+
+  x case CategoryAst == isAst(x,'CATEGORY)
+  autoCoerce(x: %): CategoryAst == x : CategoryAst
+
+  x case CapsuleAst == isAst(x,'CAPSULE)
+  autoCoerce(x: %): CapsuleAst == x : CapsuleAst
+
+  x case SignatureAst == isAst(x,'SIGNATURE)
+  autoCoerce(x: %): SignatureAst == x : SignatureAst
+
+  x case AttributeAst == isAst(x,'ATTRIBUTE)
+  autoCoerce(x: %): AttributeAst == x : AttributeAst
+
+  x case MappingAst == isAst(x,'Mapping)
+  autoCoerce(x: %): MappingAst == x : MappingAst
+
+  x case IfAst == isAst(x,'IF)
+  autoCoerce(x: %): IfAst == x : IfAst
+
+  x case RepeatAst == isAst(x,'REPEAT)
+  autoCoerce(x: %): RepeatAst == x : RepeatAst
+
+  x case WhileAst == isAst(x,'WHILE)
+  autoCoerce(x: %): WhileAst == x : WhileAst
+
+  x case InAst == isAst(x,'IN)
+  autoCoerce(x: %): InAst == x : InAst
+
+  x case CollectAst == isAst(x,'COLLECT)
+  autoCoerce(x: %): CollectAst == x : CollectAst
+
+  x case ConstructAst == isAst(x,'construct)
+  autoCoerce(x: %): ConstructAst == x : ConstructAst
+
+  x case ExitAst == isAst(x,'exit)
+  autoCoerce(x: %): ExitAst == x : ExitAst
+
+  x case ReturnAst == isAst(x,'RETURN)
+  autoCoerce(x: %): ReturnAst == x : ReturnAst
+
+  x case CoerceAst == isAst(x,'_:_:)
+  autoCoerce(x: %): CoerceAst == x : CoerceAst
+
+  x case PretendAst == isAst(x,'pretend)
+  autoCoerce(x: %): PretendAst == x : PretendAst
+
+  x case RestrictAst == isAst(x,'_@)
+  autoCoerce(x: %): RestrictAst == x : RestrictAst
+
+  x case SegmentAst == isAst(x,'SEGMENT)
+  autoCoerce(x: %): SegmentAst == x : SegmentAst
+
+  x case SequenceAst == isAst(x,'SEQ)
+  autoCoerce(x: %): SequenceAst == x : SequenceAst
+
+  x case LetAst == isAst(x,'_%LET)
+  autoCoerce(x: %): LetAst == x : LetAst
+
+  x case SuchThatAst == isAst(x,'_|)
+  autoCoerce(x: %): SuchThatAst == x : SuchThatAst
+
+  x case ColonAst == isAst(x,'_:)
+  autoCoerce(x: %): ColonAst == x : ColonAst
+
+  x case CaseAst == isAst(x,'_case)
+  autoCoerce(x: %): CaseAst == x : CaseAst
+
+  x case HasAst == isAst(x,'_has)
+  autoCoerce(x: %): HasAst == x : HasAst
+
+  x case IsAst == isAst(x,'_is)
+  autoCoerce(x: %): IsAst == x : IsAst
+  
+@
+
+
 
 \section{License}