aboutsummaryrefslogtreecommitdiff
path: root/src/algebra
diff options
context:
space:
mode:
Diffstat (limited to 'src/algebra')
-rw-r--r--src/algebra/Makefile.in13
-rw-r--r--src/algebra/Makefile.pamphlet13
-rw-r--r--src/algebra/boolean.spad.pamphlet2
-rw-r--r--src/algebra/syntax.spad.pamphlet158
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}
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-03 21:38:27 +0000