diff options
author | dos-reis <gdr@axiomatics.org> | 2010-03-13 17:54:08 +0000 |
---|---|---|
committer | dos-reis <gdr@axiomatics.org> | 2010-03-13 17:54:08 +0000 |
commit | e99018bd6a64e8d7d63a240a96ce213bb9e99b0f (patch) | |
tree | 432c7aec70fa45ff2d3db0809005587e536d8378 /src/algebra | |
parent | f438cc0b50fa559bebd0371a911c9fce342156f4 (diff) | |
download | open-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.pamphlet | 92 |
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] + @ |