aboutsummaryrefslogtreecommitdiff
path: root/src/algebra
diff options
context:
space:
mode:
authordos-reis <gdr@axiomatics.org>2010-03-13 17:54:08 +0000
committerdos-reis <gdr@axiomatics.org>2010-03-13 17:54:08 +0000
commite99018bd6a64e8d7d63a240a96ce213bb9e99b0f (patch)
tree432c7aec70fa45ff2d3db0809005587e536d8378 /src/algebra
parentf438cc0b50fa559bebd0371a911c9fce342156f4 (diff)
downloadopen-axiom-e99018bd6a64e8d7d63a240a96ce213bb9e99b0f.tar.gz
* algebra/compiler.spad.pamphlet: Add more IR contructor
functions. Elaborate definitions.
Diffstat (limited to 'src/algebra')
-rw-r--r--src/algebra/compiler.spad.pamphlet92
1 files changed, 86 insertions, 6 deletions
diff --git a/src/algebra/compiler.spad.pamphlet b/src/algebra/compiler.spad.pamphlet
index 2a0df829..49d87f80 100644
--- a/src/algebra/compiler.spad.pamphlet
+++ b/src/algebra/compiler.spad.pamphlet
@@ -23,11 +23,31 @@
++ This domain provides representations for the intermediate
++ form data structure used by the Spad elaborator.
InternalRepresentationForm(): Public == Private where
- Public == Join(SetCategory, HomotopicTo Syntax)
+ Public == Join(SetCategory, HomotopicTo Syntax) with
+ irVar: (Identifier, InternalTypeForm) -> %
+ ++ \spad{irVar(x,t)} returns an IR for a variable reference
+ ++ of type designated by the type form \spad{t}
+ irCtor: (Identifier, InternalTypeForm) -> %
+ ++ \spad{irCtor(n,t)} returns an IR for a constructor reference
+ ++ of type designated by the type form \spad{t}
+ irDef: (Identifier, InternalTypeForm, %) -> %
+ ++ \spad{irDef(f,ts,e)} returns an IR representation for a definition
+ ++ of a function named \spad{f}, with signature \spad{ts}
+ ++ and body \spad{e}.
Private == Syntax add
coerce(x: %): Syntax == rep x
+
coerce(x: Syntax): % == per x
+ irVar(x,t) ==
+ buildSyntax('%irVar,[x::Syntax,t::Syntax])::%
+
+ irCtor(x,t) ==
+ buildSyntax('%irCtor,[x::Syntax,t::Syntax])::%
+
+ irDef(f,ts,e) ==
+ buildSyntax('%irDef,[f::Syntax, ts::Syntax, e::Syntax])::%
+
@
<<domain ITFORM InternalTypeForm>>=
@@ -47,11 +67,19 @@ InternalTypeForm(): Public == Private where
++ the value of an expression is to be ignored.
voidMode: %
++ \spad{voidMode} is a constant mode denoting Void.
+ categoryMode: %
+ ++ \spad{categoryMode} is a constant mode denoting Category.
+ mappingMode: (%, List %) -> %
+ ++ \spad{mappingMode(r,ts)} returns a mapping mode with return
+ ++ mode \spad{r}, and parameter modes \spad{ts}.
Private == InternalRepresentationForm add
jokerMode == _$EmptyMode$Foreign(Builtin)
noValueMode == _$NoValueMode$Foreign(Builtin)
voidMode == _$Void$Foreign(Builtin)
+ mappingMode(r,ts) ==
+ buildSyntax('Mapping,cons(r::Syntax, ts : List(Syntax)))::%
+
@
\section{Elaboration domain}
@@ -82,6 +110,18 @@ Elaboration(): Public == Private where
environment(x)::OutputForm])$OutputForm
@
+\section{Compilation Context}
+
+<<domain CMPCTXT CompilationContext>>=
+)abbrev domain CMPCTXT CompilationContext
+CompilationContext(): Public == Private where
+ Public == SetCategory with
+ getExitMode: (%,Integer) -> InternalTypeForm
+ pushExitMode!: (%, InternalTypeForm) -> %
+ Private == add
+ Rep == Record(exitModes: List Integer)
+@
+
\section{A Package for the Spad Compiler}
<<package COMPILER CompilerPackage>>=
@@ -100,6 +140,7 @@ CompilerPackage(): Public == Private where
elaborate: SpadAst -> Maybe Elaboration
++ \spad{elaborate(s)} returns the elaboration of the syntax
++ object \spad{s} in the empty environement.
+ elaborateFile: String -> List Maybe Elaboration
Private == add
macro IR == InternalRepresentationForm
macro TFORM == InternalTypeForm
@@ -110,6 +151,9 @@ CompilerPackage(): Public == Private where
import RESULT
inline RESULT
+ -- forward declaration
+ doElaborate: (SpadAst,TFORM,ENV) -> RESULT
+
macroExpand(s,e) ==
-- FIXME: this is a short-term stopgap.
macroExpand(s,e)$Foreign(Builtin)
@@ -130,7 +174,7 @@ CompilerPackage(): Public == Private where
decl case nothing => nothing -- nor declared
T := destruct(decl)$SExpression
just(second(T) : TFORM)
- typeForm val
+ just typeForm(val@Elaboration)
-- simply coerce the elaboration `T' to mode `m'.
coerceSimply(T: RESULT, m: TFORM): RESULT ==
@@ -150,10 +194,43 @@ CompilerPackage(): Public == Private where
elaborateIdentifier(x: Identifier, t: TFORM, e: ENV): RESULT ==
r :=
case getValue(x,e) is
- val@Elaboration => just val
- otherwise => case getMode(x,e) is
- decl@Elaboration =>
- coerceTo(getValue(x,e), t)
+ v@Elaboration => just v
+ otherwise =>
+ case getMode(x,e) is
+ m@TFORM => just elaboration(irVar(x,m), m, e)
+ otherwise => nothing$RESULT
+ coerceTo(r, t)
+
+ -- elaborate a form designating a mode
+ elaborateMode(x: SpadAst, e: ENV): Maybe TFORM ==
+ t := doElaborate(x,jokerMode,e)
+ t case nothing => nothing
+ just(t : TFORM) -- FIXME: use conversion.
+
+ -- elaborate a definition.
+ elaborateDefinition(x: DefinitionAst, m: TFORM, e: ENV): RESULT ==
+ import HeadAst
+ e' := e
+ parms := parameters head x
+ n := name head x
+ srcSig := signature x
+ irSig := nil$List(TFORM)
+ -- elaborate parameters and push them in scope.
+ for p in parms for t in source srcSig repeat
+ nil? t => return nothing -- FIXME: should infer first
+ irT := elaborateMode(t::SpadAst,e)
+ irT case nothing => return nothing
+ irSig := cons(irT@TFORM,irSig)
+ -- elaborate return type.
+ ret := target srcSig
+ nil? ret => nothing -- FIXME: should infer first
+ irRet := elaborateMode(ret::SpadAst,e)
+ irRet case nothing => nothing
+ -- elaborate the body.
+ b := doElaborate(body x, irRet@TFORM, e)
+ b case nothing => nothing
+ t := mappingMode(irRet@TFORM, reverse irSig)
+ just elaboration(irDef(n,t,irForm b),t,e')
-- elaborate a syntax `s' under context `m', in the envionment `e'.
doElaborate(s: SpadAst, t: TFORM, e: ENV): RESULT ==
@@ -164,6 +241,9 @@ CompilerPackage(): Public == Private where
elaborate s ==
doElaborate(s,jokerMode,empty()$ENV)
+ elaborateFile f ==
+ [elaborate(s::SpadAst) for s in parse(f)$SpadParser]
+
@