diff --git a/.clangd b/.clangd new file mode 100644 index 0000000..ba4cbb3 --- /dev/null +++ b/.clangd @@ -0,0 +1,2 @@ +Diagnostics: + UnusedIncludes: None diff --git a/.gitignore b/.gitignore index 4929d75..75a6986 100644 --- a/.gitignore +++ b/.gitignore @@ -51,6 +51,12 @@ Module.symvers Mkfile.old dkms.conf +# CMake build dirs +build-*/ + +# CMake compile commands +compile_commands.json + # vim .*.swp .*.swo @@ -58,18 +64,3 @@ dkms.conf # vscode .vscode .cache - -# CMake -build*/ -compile_commands.json - -# clangd -.clangd - -# ctags tagfile -tags - -# other stuff -local/ - - diff --git a/CMakeLists.txt b/CMakeLists.txt index 81de430..8f3758c 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -6,8 +6,7 @@ set(CMAKE_C_STANDARD_REQUIRED True) string(JOIN " " CMAKE_C_FLAGS "-Wall -Wextra -Wformat=2" "-Wconversion -Wsign-conversion -Wimplicit-fallthrough" - "-Werror=implicit" - "-Werror=incompatible-pointer-types" + "-Werror=implicit -Werror=incompatible-pointer-types" "-Werror=int-conversion") set(CMAKE_VERBOSE_MAKEFILE ON) @@ -22,20 +21,17 @@ set(SRC_DIR src) set(SPHO_HEADER_DIR ${INCLUDE_DIR}/spho) set(SPHO_HEADER - ${SPHO_HEADER_DIR}/bind.h ${SPHO_HEADER_DIR}/ctx.h ${SPHO_HEADER_DIR}/err.h + ${SPHO_HEADER_DIR}/loc.h ${SPHO_HEADER_DIR}/scope.h - ${SPHO_HEADER_DIR}/spho.h - ${SPHO_HEADER_DIR}/subt.h ${SPHO_HEADER_DIR}/tp.h + ${SPHO_HEADER_DIR}/spho.h ) set(SPHO_SRC - ${SRC_DIR}/spho/bind.c ${SRC_DIR}/spho/ctx.c ${SRC_DIR}/spho/scope.c - ${SRC_DIR}/spho/subt.c ${SRC_DIR}/spho/tp.c ) @@ -57,18 +53,19 @@ target_compile_definitions(devcheck PRIVATE set(MSPH_SRC - ${SRC_DIR}/msph/msph.c - ${SRC_DIR}/msph/sphophi.c ${SRC_DIR}/msph/token.c ${SRC_DIR}/msph/tree.c + ${SRC_DIR}/msph/sphophi.c + ${SRC_DIR}/msph/msph.c ) set(MSPH_HEADER - ${INCLUDE_DIR}/msph/common.h - ${INCLUDE_DIR}/msph/err.h - ${INCLUDE_DIR}/msph/sphophi.h ${INCLUDE_DIR}/msph/token.h ${INCLUDE_DIR}/msph/tree.h + ${INCLUDE_DIR}/msph/common.h + ${INCLUDE_DIR}/msph/err.h + ${INCLUDE_DIR}/msph/decor.h + ${INCLUDE_DIR}/msph/sphophi.h ) add_executable(msph ${MSPH_SRC} ${MSPH_HEADER}) diff --git a/README.md b/README.md index 2ae6960..5f66243 100644 --- a/README.md +++ b/README.md @@ -2,24 +2,25 @@ experimental type system implementation -## getting and building +## sappho grammar -```sh -git clone ssh://git@gitta.log-e.se:222/lnsol/log-e-sappho.git -cd ./log-e-sappho -cmake . -B build -cd build -make +``` +s, t ::= s | t (disjunction, a.k.a. union) + | s & t (conjunction, a.k.a. intersection) + | s => t (implication) + | s -> t (arrow, a.k.a. function) + | forall x . t (forall, polymorphic) + | box t (box, modular logic) + | a [t..] (type operator application) + | x (variable) + | n (nominal) + | true (true, a.k.a. top) + | false (false, a.k.a. bottom) + | { m : t } (member, a.k.a. atomic record) + + +x ∈ var +n ∈ nominal +a ∈ opname ``` -## repository content - -This repository contains: - -* a library implementation of *sappho* called `spho`. -* a simple language parser (and soon type checker), called `msph`, developed in - tandem with `spho`. -* documentation of the sappho type system in `docs/` - - - diff --git a/docs/about/contributions.md b/docs/about/contributions.md deleted file mode 100644 index 686a257..0000000 --- a/docs/about/contributions.md +++ /dev/null @@ -1,15 +0,0 @@ -# Contributions - -* We introduce a type system able to express predicated types, a unified way to - express existance of method- and traits depending on some predicate on the - subtyping relation. -* We define our subtyping relation as a natural extension to type systems based - on semantic subtyping. -* We express our subtyping using a novel approach based on the sequent calculus. -* We show the correctness of our subtyping relation and type system. -* We explain how this type system may be used to succinctly describe programs - involving for example capabilities and constructions such as type classes. -* We have implemented the type system and give examples of how its use - simplifies expressing many properties in object oriented languages, including - things like... - diff --git a/docs/about/cycle.md b/docs/about/cycle.md deleted file mode 100644 index 00822b7..0000000 --- a/docs/about/cycle.md +++ /dev/null @@ -1,39 +0,0 @@ -# Cyclic proofs and sappho - -It seems that cyclic proofs and sappho would be a good fit. The decision -process of sappho's subtyping relation is based on the sequent calculus. Cyclic -proofs is a system of proof search which looks for cycles in a proof tree where -recursion leads to infinite growth of its branches. It would allow us to avoid -explicitly using co-induction and thus simplify the description of the -subtyping relation substantially. - - -## Cyclic proofs summarized - -A pre-proof tree is made up of nodes representing the sequents and -edges corresponding to the pairing of a premise with the conclusion of the -proof rules used to derive it. - -In an infinite pre-proof tree there might be cycles. These are paths along -which equivalent nodes repeat infinitely often. If we are able to identify such -a path, and the proof makes "progress" each round of the cycle, we can admiss -it as a proof. If this can be done for all infinite paths, the pre-proof tree -admissable as an actual proof tree. - - -In order to use this strategy to decide our subtyping relation, we need: -* Proof rules -* Proof tree cycle detection -* Admissability check, i.e. does the cycle make progress. - -See here for more info: - -* [fxpl/ln notes on cyclic -proofs][github.com/fxpl/ln/blob/main/sequel/papper/notes/cyclic-proofs.md] -* [slides on cyclic proofs, part 1][ -http://www0.cs.ucl.ac.uk/staff/J.Brotherston/slides/PARIS_FLoC_07_18_part1.pdf -] -* [slides on cyclic proofs, part 2][ -http://www0.cs.ucl.ac.uk/staff/J.Brotherston/slides/PARIS_FLoC_07_18_part2.pdf -] - diff --git a/docs/about/formalities.md b/docs/about/formalities.md deleted file mode 100644 index b2b01f1..0000000 --- a/docs/about/formalities.md +++ /dev/null @@ -1,398 +0,0 @@ -# description of sappho formals - -## sappho grammar - -``` -s, t ::= s | t (disjunction, a.k.a. union) - | s & t (conjunction, a.k.a. intersection) - | s => t (implication) - | s -> t (arrow, a.k.a. function) - | forall x . t (forall, polymorphic) - | box t (box, c.f. modular logic) - | a [t..] (type operator application) - | x (variable) - | n (nominal) - | true (true, a.k.a. top) - | false (false, a.k.a. bottom) - | { m : t } (member, a.k.a. atomic record) - - -x ∈ var -n ∈ nominal -a ∈ opname -``` - -## sappho subtyping rules - -```cmath -// trace pairs: none ----- [identity] -s, γ ⊢ s, δ - -// trace pairs: none ----- [true-right] -γ ⊢ true, δ - -// trace pairs: none ----- [false-left] -false, γ ⊢ δ - -// trace pairs: none -s, t, γ ⊢ δ ----- [conj-left] -s & t, γ ⊢ δ - -// trace pairs: none -γ ⊢ s, t, δ ----- [disj-right] -γ ⊢ s | t, δ - -// trace pairs: none -s, γ ⊢ δ -t, γ ⊢ δ ----- [disj-left] -s | t, γ ⊢ δ - -// trace pairs: none -γ ⊢ s, δ -γ ⊢ t, δ ----- [conj-right] -γ ⊢ s & t, δ - -// XXX -// remove s => t? always make progress -// trace pairs: none -s => t, s, t, γ ⊢ δ ----- [impl-left] -s => t, s, γ ⊢ δ - -// trace pairs: none -s, γ ⊢ t, δ ----- [impl-right] -γ ⊢ s => t, δ - -// box works as a kind of "forall" for concrete types -// trace pairs: none -box t, t, γ ⊢ δ ----- [box-left] -box t, γ ⊢ δ - -// (.)-- filters the contexts. -// trace pairs: premise[0] -- conclusion -γ-- ⊢ t, δ-- ----- [box-right] -γ ⊢ box t, δ - - -// using cyclic proof strategy, rule for dealing with aliases/type operators -// becomes really simple. However, this requires well-formedness rules on types -// to exclude typedefs like -// type A = A -// Or that our cycle detection excludes paths between "identical" states. -// trace pairs: none -γ ⊢ expand(a[t..]), δ ----- -γ ⊢ a[t..], δ - -expand(a[t..]), γ ⊢ δ ----- -a[t..], γ ⊢ δ - - -// member types are filtered according to member name -// trace pairs: premise[0] -- conclusion -γ >> m ⊢ δ >> m ----- [member] -γ ⊢ δ - - -// foralls are unwrapped and variable substituted with fresh name -// i.e. we treat the bound variable nominally -// trace pairs: premise[1] -- conclusion -n fresh -γ [n] ⊢ δ [n] ----- [forall] -γ ⊢ δ - -// 1 + n! premises -// trace pairs: i ∈ [1..(n! + 1)], premise[i] -- conclusion -c, γ* ⊢ a_1, ..., a_n -∀ I ⊆ {1, ..., n}. - c, γ* ⊢ { a_i | i ∈ I }, δ* - OR - { b_i | i ∈ ¬I }, γ* ⊢ d, δ* ----- [loads-of-fun] -a_1 -> b_1, ..., a_n -> b_n, γ ⊢ c -> d, δ -``` - -### context operators - -* box filtering -``` -(t, γ)-- =def= t, γ-- if t == box s, for some s - γ-- otherwise -``` - -* member unwrapping -``` -(t, γ) >> m =def= s, (γ >> m) if t == { m : s }, for some s - t, (γ >> m) if t == box s, for some s - γ >> m otherwise -``` - -* forall-unwrapping and substitution -``` -(t, γ) [n] =def= s [n/x], (γ [n]) if t == forall x . s, for some x, s - t, (γ [n]) if t == box s, for some s - γ [n] otherwise -``` - -### trace pairs -Trace pairs are related to cyclic proofs. They identify the pairs of -`premise -- conclusion` that are *productive*, i.e. leads to some progress -making a cycle in the proof tree admissable as a cyclic proof of the nodes in -the cycle. - -The trace pairs are described in the comments for each subtyping rule. - -### Semantic function subtyping - -*Here we try to give an intuitive explainer of how to reason about function -subtyping in the semantic subtyping domain.* - -Given function types -``` -a_1 -> b_1, ..., a_n -> b_n -``` -the conjunction (intersection) of `a_i -> b_i`, i.e. -``` -intsec = (a_1 -> b_1) & ... & (a_n -> b_n) -``` -represents the set of functions that combines the properties of all -`a_i -> b_i` by themselves. To get an idea of what functions this describes, -let's start with reasoning about values, that is, functions in `intsec`. -First we note that any function in this set accepts any argument that are in -either of the `a_i`s. That is, it can take any argument in the set represented -by -``` -a = a_1 | ... | a_n -``` -Furthermore, a function `f` in `intsec` "promises" to map any value in `a_i` to -a value in its corresponding `b_i`. -Specifically, given `I ⊆ {1..n}`, a value `v` in the intersection -``` -a_I_intsec = &[i ∈ I] a_i -``` -is mapped to a value in -``` -b_I_intsec = &[i ∈ I] b_i -``` -that is, -``` -v ∈ &[i ∈ I] a_i implies f(v) ∈ &[i ∈ I] b_i -``` - -*In the following we will "abuse notation" a bit. Try to look at it like -talking to an old friend, and you just instinctively know exactly what they -mean without explaining...* - -Now, given a type `c -> d`, how do we know if -``` -intsec = &[i ∈ {1..n}] a_i -> b_i <: c -> d -``` -? -Or equivalently, friend speaking, if -``` -∩[i ∈ {1..n}] a_i -> b_i ⊆ c -> d -``` -? - -Immediately, it should be obvious that -``` -c ⊆ a (= ∪[i ∈ {1..}] a_i) -``` -Furthermore, it is necessary that any function in `intsec` will have to map all -values in `c` into `d`, specifically -``` -f ∈ intsec, v ∈ c implies f(v) ∈ d -``` -Note that this does not mean that any function in `a_i -> b_i` must map all -values in `a_i` into `d`, since it's not necessary that `a_i \ c = ø`. -Specifically, it is not necessary that `b_i ⊆ d`. However, taking `I ⊆ {1..n}`, -assuming -``` -a_I_intsec = &[i ∈ I] a_i ⊆ c -``` -then, necessarily -``` -b_I_intsec = &[i ∈ I] b_i ⊆ d -``` - -Conversely, if -``` -b_I_intsect ⊆ d -``` -then any function in `intsec` maps `a_I_intsec` into `d`. If `a_I_intsec` -happens to intersect with `c`, it "covers" a part of `c`. I.e. the set `I` can -be understood as promising to map a part of `c` into `d`. - -Defining this formally, we say that `I_cand ⊆ {1..n}` is a (`d`-)*candidate* if, -``` -∩[i ∈ I_cand] b_i ⊆ d -``` -We can thus see a candidate `I_cand` as a combination, or more specifically, -intersection of the function types `{a_i -> b_i | i ∈ I_cand}`, that according -to the reasoning above promises to map a part of the domain into `d`, namely -``` -∩[i ∈ I_cand] a_i -``` -A candidate thus "covers" part of the domain or formally speaking, `I` -(`d`-)covers a domain `s` if `I` is a (`d`-)candidate and -``` -s ⊆ ∩[i ∈ I] a_i -``` -If `IS ⊆ P({1..n})` then we say that `IS` (`d`-)covers `s` if all of `s` is -covered by some `I ∈ IS`, that is -``` -s ⊆ ∪[I ∈ IS | I is d-candidate] ∩[i ∈ I] a_i -``` - -Given the function types `{a_i -> b_i | i ∈ {1..n}}` and its set of candidates -`IC = {I_cand_1..I_cand_k}`, it is fairly easy to see that -``` -&[i ∈ {1..n}] (a_i -> b_i) <: c -> d -``` -iff `IC` `d`-covers `c`: -``` -c ⊆ ( ∪[I_cand ∈ IC] ∩[i ∈ I_cand] a_i ) -``` -Using some *pro gamer moves*, we can see that this is equivalent to -``` -c ⊆ ( ∩[I_cand ∈ IC] ∪[i ∉ I_cand] a_i ) -``` -This gives us the final form for our subtyping rule -``` -c, γ* ⊢ a_i | ... | a_n, δ* -forall I ⊆ {1..n}. - &[i ∈ I] b_i, γ* ⊢ d, δ* - or - c, γ* ⊢ |[i ∉ I] a_i, δ* ----- [loads-o-fun] -a_1 -> b_1, ..., a_n -> b_n, γ ⊢ c -> d, δ -``` - -### Recursive subtyping - -Type aliases creates the possibility of recursive types, and thus we need to -handle recursive subtyping - -Handling subtyping co-inductively would enable us to handle the relation -``` -type A = { x : { y : A } } -type B = { y : { x : B } } - -A <: { x : B } -{ x : B } <: A -``` - - -We have made progress if we "switch context" - -If we make progress and end up at the same sequent, co-induction gives us the -conclusion. - -Some actions/rules lead to equivalent contexts, i.e. does not switch -context/make progress. - -### Other - -True ~ { x : True } on the left -False ~ { x : False } on the right - -or rather - -True ~ { x : True } in positive position -False ~ { x : False } in negative position - - - - - -### implication -``` - -γ ⊢ s => t, u => s, δ - -if s, then u => s holds -if ¬s, then s => t holds - -``` - - -altho -``` -γ ⊢ s => t, s, δ -``` - -Given the msph program -``` -nominal n - -type Woops[e] = { - member f : (e <: false => n) | (e <: false) -} - -type Noooes = { - member f : true -} -``` -we can prove that, for any type `t` -``` -Noooes <: Woops[t] -``` - -The derivation looks like this: -``` ----- [identity] -true, t <: false ⊢ n, (t <: false) ----- [impl-right] -true ⊢ (t <: false => n), (t <: false) ----- [disj-right] -true ⊢ (t <: false => n) | (t <: false) ----- [member] -{ f : true } ⊢ { f : (t <: false => n) | (t <: false) } ----- [expand-right] -{ f : true } ⊢ Woops[t] ----- [expand-left] -Nooes ⊢ Woops[t] ----- [impl-right] -⊢ Nooes => Woops[t] ----- [box-right] -⊢ Nooes <: Woops[t] -``` - -This looks a bit dangerous at first. However, if we translate the implication to -using disjunction and negation, we get -``` -(t <: false => N) | (t <: false) == (¬(t <: false) | n) | (t <: false) -``` - -Considering the two cases -``` -(1) t == false -(2) t != false -``` -we see that in (1) -``` -(¬(t <: false) | n) | (t <: false) == -(¬(true) | n) | (true) == -true -``` -and in (2) -``` -(¬(t <: false) | n) | (t <: false) == -(¬(false) | n) | false == -(true | n) | false == -true -``` - diff --git a/docs/about/interpret.md b/docs/about/interpret.md deleted file mode 100644 index 1e64455..0000000 --- a/docs/about/interpret.md +++ /dev/null @@ -1,88 +0,0 @@ -# interpretation of sappho - -Different aspects of sappho interpreted. - -## What is true? - -Our "set interpretation" of types says `true` represents the full universe of -"things". - -What are these things? - -For all intents and purposes, a programmer can look at them as the values of -our language. - -What does this mean in practical terms? - -Well, it means something of type `true` is "a value". - -What is "a value" then? - -That's a good question. It can be anything really. - -An integer? - -Yep! - -A function? - -Yes, m'am! - -A solution to the halting problem? - -Well, yeah! But good luck constructing that. - -A... - -I think you get my point. A value can be anything from a simple integer to -nuclear apocalypse. The thing is, from the point of view of our program, it -means "we cannot really say anything here". - -But couldn't that be dangerous? - -Depends on what you mean by dangerous. - -I mean, to be able to give everything a type? - -Well, let me ask you this: do you like rat poison? - -What? To eat? - -Yeah! - -Nooo, that'd be dangerous! - -Yeah, exactly my point. - -What? - -You know what rat poison is obviously, despite it being dangerous? - -Well, yeah... - -Maybe you got it already, but my point is: rat poison is dangerous, but you -still know about it, and its existance. So, something being dangerous does not -mean you have this blank spot of knowledge that you just keep ignoring because -of this perceived danger. - - - - - -### interpretation of ⊢ -what is the interpretation of - -γ ⊢ δ? - - -given a concrete type k - -conjunction of γ hold for k - -then - -disjunction of δ hold for k - - - - diff --git a/example/non-parse/ex6.msph b/example/non-parse/ex6.msph deleted file mode 100644 index afdeccb..0000000 --- a/example/non-parse/ex6.msph +++ /dev/null @@ -1,21 +0,0 @@ -type A[X, Y] = { - type B[Z] = { - mb : X & Z - } - - ma : B[Y] -} - - -m : A[M, N] - - -m : ⟨X -> M, Y -> N⟩ { - ma : B[Y] -} - -m : ⟨X -> M, Y -> N⟩ { - ma : ⟨Z -> Y⟩ { - mb : X & Z - } -} diff --git a/example/subt/rec-lockstep.msph b/example/subt/rec-lockstep.msph deleted file mode 100644 index 2b74462..0000000 --- a/example/subt/rec-lockstep.msph +++ /dev/null @@ -1,9 +0,0 @@ - -type A = { x : { y : A } } - -type B = { y : { x : B } } - - -assert { x : B } <: A - -assert A <: { x : B } diff --git a/include/msph/decor.h b/include/msph/decor.h new file mode 100644 index 0000000..db302d3 --- /dev/null +++ b/include/msph/decor.h @@ -0,0 +1,33 @@ +#ifndef _MSPH_DECOR_H +#define _MSPH_DECOR_H + +struct msph_tp_decor { + struct spho_tp *tp; +}; + +#define TP_DECOR_INIT(ptr) \ + do { \ + (ptr)->tp = NULL; \ + } while (0) + +struct msph_scope_decor { + struct spho_scope *sc; +}; + +#define SCOPE_DECOR_INIT(ptr) \ + do { \ + (ptr)->sc = NULL; \ + } while (0) + +struct msph_nom_decor { + struct spho_nom *nom; +}; + +#define NOM_DECOR_INIT(ptr) \ + do { \ + (ptr)->nom = NULL; \ + } while (0) + +#define GET_SCOPE(ptr) ((ptr)->dec.sc) + +#endif /* _MSPH_DECOR_H */ diff --git a/include/msph/sphophi.h b/include/msph/sphophi.h index 65508f1..052b9bf 100644 --- a/include/msph/sphophi.h +++ b/include/msph/sphophi.h @@ -7,7 +7,6 @@ int msph_sphophi_init(struct msph_tree_root *); int msph_sphophi_scope(struct msph_tree_root *); int msph_sphophi_nom_lookup(struct msph_tree_root *); int msph_sphophi_tp(struct msph_tree_root *); -int msph_sphophi_tp_prebind(struct msph_tree_root *); int msph_sphophi(struct msph_tree_root *); diff --git a/include/msph/tree.h b/include/msph/tree.h index 028f329..b2e793d 100644 --- a/include/msph/tree.h +++ b/include/msph/tree.h @@ -5,13 +5,56 @@ #include "msph/common.h" #include "msph/token.h" +#include "msph/decor.h" -/* tree decorations */ -struct msph_decor { - struct spho_scope *sc; - struct spho_tp *tp; - struct spho_nom *nom; -}; +/* + * TYPES: + * Conj + * Disj + * Impl + * Arrow + * Box + * (Sub) + * Forall + * + * True + * False + * Var + * Nominal + * + * Record + * + * DEFINITIONS/DIRECTIVES: + * Type definition (type A[X..] = T) + * Nominal definition (nominal N) + * Member definition (member mname : T) + * + * { + * member a: A + * member b: B + * } + * + * Subtyping assert (assert A <: B, asserts that A <: B) + * + * EXTRA DEFINITIONS + * Class definition (class C[...] { ... }, shorthand) + * + * EXPRESSIONS + * Conj + * Disj + * Impl + * Arrow + * Box + * (Sub) + * Forall + * + * True + * False + * Var + * Nominal + * + * Trait ({ ... }, creates scoping) + */ #define MSPH_TREE_ROOT 0x0000 #define MSPH_TREE_UNIT 0x0001 @@ -27,8 +70,8 @@ struct msph_decor { #define MSPH_TREE_TPEXPR 0x0040 #define MSPH_TREE_TRUE 0x0041 #define MSPH_TREE_FALSE 0x0042 -#define MSPH_TREE_TPNAME 0x0043 -#define MSPH_TREE_TPAPPL 0x0044 +#define MSPH_TREE_NAME 0x0043 +#define MSPH_TREE_APPL 0x0044 #define MSPH_TREE_TRAIT 0x0045 #define MSPH_TREE_CONJ 0x0046 #define MSPH_TREE_DISJ 0x0047 @@ -39,64 +82,11 @@ struct msph_decor { #define MSPH_TREE_PAREN 0x004c #define MSPH_TREE_IDENT 0x0100 -#define MSPH_TREE_NAMEDECL 0x0101 -#define MSPH_TREE_NAMEREF 0x0102 -#define MSPH_TREE_FLAG_OFFSET 16 - -#define MSPH_TREE_FLAG_SCOPE (1 << (MSPH_TREE_FLAG_OFFSET)) -#define MSPH_TREE_FLAG_TP (1 << (MSPH_TREE_FLAG_OFFSET + 1)) -#define MSPH_TREE_FLAG_NOM (1 << (MSPH_TREE_FLAG_OFFSET + 2)) - -#define MSPH_TREE_MASK_FLAGS ((~0x0u) << MSPH_TREE_FLAG_OFFSET) -#define MSPH_TREE_MASK_ID ((~0x0u) ^ MSPH_TREE_MASK_FLAGS) - -#define ADD_FLAG(tree, flag) \ - do { \ - TREE(tree)->type |= flag; \ - } while (0) -#define HAS_FLAG(tree, flag) (TREE(tree)->type & (flag)) - -#define TREE(tree) ((struct msph_tree *)tree) -#define TEXT(tree) ((struct msph_tree_text *)tree) -#define IDENT(tree) ((struct msph_tree_ident *)tree) -#define TPEXPR(tree) ((struct msph_tree_tpexpr *)tree) - -#define HAS_SCOPE(tree) HAS_FLAG((tree), MSPH_TREE_FLAG_SCOPE) -#define HAS_TP(tree) HAS_FLAG((tree), MSPH_TREE_FLAG_TP) -#define HAS_NOM(tree) HAS_FLAG((tree), MSPH_TREE_FLAG_NOM) - -#define HAS_PARAMS(tpdef) (! STAILQ_EMPTY(&(tpdef)->params)) - -#define TREE_ID(tree) (((struct msph_tree *)tree)->type & \ - MSPH_TREE_MASK_ID) - -#define DECOR(tree) (TREE(tree)->decor) -#define SCOPE(tree) (TREE(tree)->decor.sc) -#define TP(tree) (TREE(tree)->decor.tp) -#define NOM(tree) (TREE(tree)->decor.nom) - -#define DECOR_INIT(tree) \ - do { \ - DECOR(tree) = (struct msph_decor) { NULL, NULL, NULL }; \ - } while (0) struct msph_tree { - unsigned int type; + int type; struct msph_tree *parent; - struct msph_decor decor; -}; - - -struct msph_tree_text { - struct msph_tree hd_tr; - struct msph_text_pos pos; -}; - -struct msph_tree_ident { - struct msph_tree_text hd_txt; - - char str[MSPH_IDENT_LEN]; }; struct msph_tree_root; @@ -110,7 +100,7 @@ struct msph_tree_ident; struct msph_tree_tpexpr; struct msph_tree_root { - struct msph_tree hd_tr; + struct msph_tree htr; struct msph_ctx *ctx; @@ -118,144 +108,155 @@ struct msph_tree_root { }; struct msph_tree_unit { - struct msph_tree hd_tr; + struct msph_tree htr; char name[MSPH_NAME_LEN]; struct msph_tree_body *body; + struct msph_scope_decor dec; STAILQ_ENTRY(msph_tree_unit) entries; }; +struct msph_tree_text { + struct msph_tree htr; + struct msph_text_pos pos; +}; + struct msph_tree_body { - struct msph_tree hd_tr; + struct msph_tree htr; STAILQ_HEAD(msph_tree_dir_l, msph_tree_dir) head; }; struct msph_tree_dir { - struct msph_tree_text hd_txt; + struct msph_tree_text htxt; STAILQ_ENTRY(msph_tree_dir) entries; }; struct msph_tree_tpdef { - struct msph_tree_dir hd_dir; + struct msph_tree_dir hdir; - struct msph_tree_namedecl *name; - STAILQ_HEAD(msph_tree_namedecl_l, msph_tree_namedecl) params; + struct msph_tree_ident *id; struct msph_tree_tpexpr *tp; }; struct msph_tree_nomindecl { - struct msph_tree_dir hd_dir; + struct msph_tree_dir hdir; - struct msph_tree_namedecl *name; + struct msph_tree_ident *id; }; struct msph_tree_membdecl { - struct msph_tree_dir hd_dir; + struct msph_tree_dir hdir; - struct msph_tree_namedecl *name; - struct msph_tree_tpexpr *tp; + struct msph_tree_ident *id; + struct msph_tree_tpexpr *tp; }; struct msph_tree_assert { - struct msph_tree_dir hd_dir; + struct msph_tree_dir hdir; struct msph_tree_tpexpr *ltp; struct msph_tree_tpexpr *rtp; }; -struct msph_tree_namedecl { - struct msph_tree_ident hd_id; - - STAILQ_ENTRY(msph_tree_namedecl) entries; -}; - struct msph_tree_tpexpr { - struct msph_tree_text hd_txt; + struct msph_tree_text htxt; STAILQ_ENTRY(msph_tree_tpexpr) entries; + + struct msph_tp_decor dec; }; + struct msph_tree_true { - struct msph_tree_tpexpr hd_tpe; + struct msph_tree_tpexpr htpe; }; struct msph_tree_false { - struct msph_tree_tpexpr hd_tpe; + struct msph_tree_tpexpr htpe; }; -struct msph_tree_nameref { - struct msph_tree_ident hd_id; +struct msph_tree_name { + struct msph_tree_tpexpr htpe; + + struct msph_tree_ident *id; }; -struct msph_tree_tpname { - struct msph_tree_tpexpr hd_tpe; +struct msph_tree_appl { + struct msph_tree_tpexpr htpe; - struct msph_tree_nameref *name; -}; - -struct msph_tree_tpappl { - struct msph_tree_tpexpr hd_tpe; - - struct msph_tree_nameref *name; - STAILQ_HEAD(msph_tree_tpexpr_l, msph_tree_tpexpr) args; + struct msph_tree_ident *id; + STAILQ_HEAD(msph_tree_tpexpr_l, msph_tree_tpexpr) head; }; struct msph_tree_trait { - struct msph_tree_tpexpr hd_tpe; + struct msph_tree_tpexpr htpe; struct msph_tree_body *body; + + struct msph_scope_decor dec; }; struct msph_tree_conj { - struct msph_tree_tpexpr hd_tpe; + struct msph_tree_tpexpr htpe; struct msph_tree_tpexpr *ltp; struct msph_tree_tpexpr *rtp; }; struct msph_tree_disj { - struct msph_tree_tpexpr hd_tpe; + struct msph_tree_tpexpr htpe; struct msph_tree_tpexpr *ltp; struct msph_tree_tpexpr *rtp; }; struct msph_tree_impl { - struct msph_tree_tpexpr hd_tpe; + struct msph_tree_tpexpr htpe; struct msph_tree_tpexpr *ltp; struct msph_tree_tpexpr *rtp; }; struct msph_tree_arrow { - struct msph_tree_tpexpr hd_tpe; + struct msph_tree_tpexpr htpe; struct msph_tree_tpexpr *ltp; struct msph_tree_tpexpr *rtp; }; struct msph_tree_box { - struct msph_tree_tpexpr hd_tpe; + struct msph_tree_tpexpr htpe; struct msph_tree_tpexpr *inner; }; struct msph_tree_forall { - struct msph_tree_tpexpr hd_tpe; + struct msph_tree_tpexpr htpe; - struct msph_tree_namedecl *name; - struct msph_tree_tpexpr *inner; + struct msph_tree_ident *id; + struct msph_tree_tpexpr *inner; + + struct msph_scope_decor dec; }; struct msph_tree_paren { - struct msph_tree_tpexpr hd_tpe; + struct msph_tree_tpexpr htpe; struct msph_tree_tpexpr *inner; }; +struct msph_tree_ident { + struct msph_tree_text htxt; + + char str[MSPH_IDENT_LEN]; + STAILQ_ENTRY(msph_tree_ident) entries; + + struct msph_nom_decor dec; +}; + struct msph_tree_root *msph_tree_makeroot(struct msph_ctx *); @@ -263,4 +264,7 @@ int msph_tree_parse(struct msph_token_stream *, struct msph_tree_root *); ssize_t msph_tree_fprint(FILE *, struct msph_tree *); +#define T(ptr) ((struct msph_tree *)ptr) +#define TXT(ptr) ((struct msph_tree_text *)ptr) + #endif diff --git a/include/spho/bind.h b/include/spho/bind.h deleted file mode 100644 index 4e175c3..0000000 --- a/include/spho/bind.h +++ /dev/null @@ -1,54 +0,0 @@ -#ifndef _SPHO_BIND_H -#define _SPHO_BIND_H - -#include - -#include "spho/scope.h" - -#define SPHO_BIND_UNDECLARED 0x0 -#define SPHO_BIND_UNDEFINED 0x01 -#define SPHO_BIND_TP 0x11 -#define SPHO_BIND_TP_OP 0x12 -#define SPHO_BIND_MEMB_TP 0x13 - -union spho_prebind_val { - const void *undef; - const struct spho_tp *tp; - const struct spho_tp_op *op; -}; - -struct spho_prebind_pair { - const struct spho_nom *nom; - - int kind; - union spho_prebind_val val; -}; - -struct spho_prebind { - struct spho_scope *sc; - - size_t sz; - struct spho_prebind_pair *binds; -}; - -struct spho_prebind *spho_prebind_create(struct spho_scope *); - -int spho_prebind_undef(struct spho_prebind *, const struct spho_nom *); -int spho_prebind_tp(struct spho_prebind *, const struct spho_nom *, - const struct spho_tp *); -int spho_prebind_tp_op(struct spho_prebind *, const struct spho_nom *, - const struct spho_tp_op *); -int spho_prebind_member_tp(struct spho_prebind *, const struct spho_nom *, - const struct spho_tp *); - -struct spho_prebind *spho_prebind_dupl(const struct spho_prebind *); - -void spho_prebind_free(struct spho_prebind *); - - -struct spho_bind { - struct spho_prebind *loc; - struct spho_bind *parent; -}; - -#endif diff --git a/include/spho/err.h b/include/spho/err.h index 2f56532..e9bad83 100644 --- a/include/spho/err.h +++ b/include/spho/err.h @@ -14,8 +14,6 @@ #define SPHO_ERR_ARGINVAL 0x010003 #define SPHO_ERR_NOM_INUSE 0x020001 #define SPHO_ERR_NOM_NOTINSCOPE 0x020002 -#define SPHO_ERR_BIND_DUPL 0x030001 -#define SPHO_ERR_BIND_NOTFOUND 0x030002 #define SPHO_ERR_IS_SYSERR(err) (SPHO_ERR_SYS == err) @@ -43,6 +41,54 @@ (ctx)->errline = __LINE__; \ } while (0) +#define SPHO_STRINGIFY(a) #a +#define SPHO_MACRO_STR(b) SPHO_STRINGIFY(b) + +#define __LINE__S SPHO_MACRO_STR(__LINE__) + +#define SPHO_PRECOND(cond) \ + do { \ + if (! (cond) ) { \ + fprintf(stderr, "SPHO_PRECOND(" #cond ")@" \ + __FILE__ ":" __LINE__S \ + " failed. Aborting.\n"); \ + abort(); \ + } \ + } while (0) + +#define SPHO_ASSERT(cond) \ + do { \ + if (! (cond) ) { \ + fprintf(stderr, "SPHO_ASSERT(" #cond ")@" \ + __FILE__ ":" __LINE__S \ + " failed. Aborting.\n"); \ + abort(); \ + } \ + } while (0) + +#define SPHO_POSTCOND(cond) \ + do { \ + if (! (cond) ) { \ + fprintf(stderr, "SPHO_POSTCOND(" #cond ")@" \ + __FILE__ ":" __LINE__S \ + " failed. Aborting.\n"); \ + abort(); \ + } \ + } while (0) + + +#ifdef SPHO_ENABLE_DEBUG_PRINT + +#define SPHO_DEBUG_PRINT(fmt, ...) \ + do { \ + fprintf(stderr, fmt __VA_OPT__(,) __VA_ARGS__); \ + } while (0) + +#else /* SPHO_ENABLE_DEBUG_PRINT */ + +#define SPHO_DEBUG_PRINT(fmt, ...) + +#endif /* SPHO_ENABLE_DEBUG_PRINT */ #else /* SPHO_DEBUG */ diff --git a/include/spho/scope.h b/include/spho/scope.h index ff682c4..843b554 100644 --- a/include/spho/scope.h +++ b/include/spho/scope.h @@ -7,18 +7,40 @@ #define SPHO_NOM_LEN 128 -/* name */ struct spho_nom { char s[SPHO_NOM_LEN]; - SLIST_ENTRY(spho_nom) next; // TODO change to allocs + SLIST_ENTRY(spho_nom) next; }; SLIST_HEAD(spho_nom_l, spho_nom); - #define TP_KONST_KEY_TRUE 0x43445 /* don't change!!!!! */ #define TP_KONST_KEY_FALSE 0x66a57 /* don't change!1! */ + +struct spho_var { + struct spho_nom nom; + + STAILQ_ENTRY(spho_var) next; +}; + +STAILQ_HEAD(spho_var_l, spho_var); + +struct spho_bind { + struct spho_nom nom; + struct spho_tpop *op; +}; + +struct spho_tpop { + struct spho_var_l params; + struct spho_tp *def; +}; + +struct spho_rec { + struct spho_nom mnom; + struct spho_tp *tp; +}; + /* type data */ struct tp_binop_data { struct spho_tp *left; @@ -29,6 +51,11 @@ struct tp_unop_data { struct spho_tp *operand; }; +struct tp_binding_data { + struct spho_nom *nom; + struct spho_tp *bound; +}; + struct tp_nom_data { struct spho_nom *nom; }; @@ -43,16 +70,6 @@ struct tp_konst_data { const char *str; }; -struct tp_forall_data { - struct spho_nom *nom; - struct spho_tp *tp; -}; - -struct tp_member_data { - struct spho_nom *nom; - struct spho_tp *tp; -}; - extern const struct tp_konst_data tp_konst_true; extern const struct tp_konst_data tp_konst_false; @@ -63,30 +80,22 @@ extern const struct tp_konst_data tp_konst_false; union tp_data { struct tp_binop_data binop; struct tp_unop_data unop; + struct tp_binding_data bind; struct tp_appl_data appl; struct tp_nom_data nom; struct tp_konst_data konst; - struct tp_forall_data fa; - struct tp_member_data memb; }; /* sappho type */ struct spho_tp { struct spho_scope *sc; - int kind; + int form; union tp_data d; STAILQ_ENTRY(spho_tp) entries; }; -struct spho_tp_op { - struct spho_scope *sc; - - struct spho_scope *op_sc; - struct spho_tp *op_tp; -}; - STAILQ_HEAD(spho_tp_l, spho_tp); struct spho_tp_ptr { @@ -97,33 +106,24 @@ struct spho_tp_ptr { STAILQ_HEAD(spho_tp_ptr_l, spho_tp_ptr); struct spho_tp_alloc { - union { - struct spho_tp tp; - struct spho_tp_op tp_op; - } alloc; + struct spho_tp tp; TAILQ_ENTRY(spho_tp_alloc) allocs; }; TAILQ_HEAD(spho_tp_alloc_l, spho_tp_alloc); -SLIST_HEAD(spho_scope_l, spho_scope); -/* defined in spho/bind.h */ -struct spho_bind; +SLIST_HEAD(spho_scope_l, spho_scope); struct spho_scope { struct spho_ctx *ctx; struct spho_scope *parent; struct spho_scope_l subs; - - size_t n_noms; struct spho_nom_l noms; struct spho_tp_alloc_l tps; - struct spho_prebind *bind_loc; - SLIST_ENTRY(spho_scope) next; }; @@ -140,16 +140,9 @@ struct spho_scope *spho_scope_create(struct spho_scope *); void spho_scope_destroy(struct spho_scope *); struct spho_nom *spho_scope_nom_add(struct spho_scope *, const char *, size_t); -int spho_scope_nom_lookup_str(struct spho_scope *, const char *, size_t, - struct spho_nom **); -int spho_scope_nom_lookup_str_strict(struct spho_scope *, const char *, - size_t, struct spho_nom **); - -int spho_scope_prebind_init(struct spho_scope *); -int spho_scope_prebind_tp(struct spho_scope *, struct spho_nom *, - struct spho_tp *); -int spho_scope_prebind_tp_op(struct spho_scope *, struct spho_nom *, - struct spho_tp_op *); -int spho_scope_prebind_undef(struct spho_scope *, struct spho_nom *); +int spho_scope_nom_get(struct spho_scope *, const char *, size_t, + struct spho_nom **); +int spho_scope_nom_lookup(struct spho_scope *, const char *, size_t, + struct spho_nom **); #endif /* _SPHO_SCOPE_H */ diff --git a/include/spho/spho.h b/include/spho/spho.h index e22d7c6..f8582dc 100644 --- a/include/spho/spho.h +++ b/include/spho/spho.h @@ -6,81 +6,4 @@ #include "spho/err.h" #include "spho/ctx.h" - -#define SPHO_UTIL_SLIST_DESTROY(l, elmtype, next, term) \ -do { \ - struct elmtype *elm; \ - while (! SLIST_EMPTY(l)) { \ - elm = SLIST_FIRST(l); \ - SLIST_REMOVE_HEAD(l, next); \ - term(elm); \ - free(elm); \ - } \ -} while (0) - -#ifdef SPHO_USE_STRLCPY -#define SPHO_STRLCPY(dst, src, len) strlcpy(dst, src, len) -#else -#define SPHO_STRLCPY(dst, src, len) \ - (size_t)snprintf(dst, len, "%s", src) -#endif /* ifdef SPHO_USE_STRLCPY */ - -#define SPHO_STRINGIFY(a) #a -#define SPHO_MACRO_STR(b) SPHO_STRINGIFY(b) -#define __LINE__S SPHO_MACRO_STR(__LINE__) - - -#define SPHO_RIP(msg, ...) \ - do { \ - fprintf(stderr, "SPHO_RIP(" msg ")@" \ - __FILE__ ":" __LINE__S \ - " failed. Aborting.\n" __VA_OPT__(,) __VA_ARGS__); \ - abort(); \ - } while (0) - - -#ifdef SPHO_DEBUG - -#define SPHO_PRECOND(cond) \ - do { \ - if (! (cond) ) { \ - fprintf(stderr, "SPHO_PRECOND(" #cond ")@" \ - __FILE__ ":" __LINE__S \ - " failed. Aborting.\n"); \ - abort(); \ - } \ - } while (0) - -#define SPHO_ASSERT(cond) \ - do { \ - if (! (cond) ) { \ - fprintf(stderr, "SPHO_ASSERT(" #cond ")@" \ - __FILE__ ":" __LINE__S \ - " failed. Aborting.\n"); \ - abort(); \ - } \ - } while (0) - -#define SPHO_POSTCOND(cond) \ - do { \ - if (! (cond) ) { \ - fprintf(stderr, "SPHO_POSTCOND(" #cond ")@" \ - __FILE__ ":" __LINE__S \ - " failed. Aborting.\n"); \ - abort(); \ - } \ - } while (0) - - -#ifdef SPHO_ENABLE_DEBUG_PRINT -#define SPHO_DEBUG_PRINT(fmt, ...) \ - do { \ - fprintf(stderr, fmt __VA_OPT__(,) __VA_ARGS__); \ - } while (0) -#else -#define SPHO_DEBUG_PRINT(fmt, ...) -#endif /* ifdef SPHO_ENABLE_DEBUG_PRINT */ - -#endif /* ifdef SPHO_DEBUG */ - #endif diff --git a/include/spho/subt.h b/include/spho/subt.h deleted file mode 100644 index f5a0c22..0000000 --- a/include/spho/subt.h +++ /dev/null @@ -1,9 +0,0 @@ -#ifndef _SPHO_SUBT_H -#define _SPHO_SUBT_H - -#include "spho/scope.h" - -int spho_is_subt(struct spho_ctx *, const struct spho_tp *, - const struct spho_tp *); - -#endif /* ifndef _SPHO_SUBT_H */ diff --git a/include/spho/tp.h b/include/spho/tp.h index c15eb76..5395d76 100644 --- a/include/spho/tp.h +++ b/include/spho/tp.h @@ -12,24 +12,20 @@ #define SPHO_TP_FORM_BOX 0x14 #define SPHO_TP_FORM_FORALL 0x15 #define SPHO_TP_FORM_APPL 0x16 -#define SPHO_TP_FORM_MEMBER 0x17 -#define SPHO_TP_FORM_NOMINAL 0x18 #define SPHO_TP_FORM_TRUE 0x20 #define SPHO_TP_FORM_FALSE 0x21 -#define SPHO_TP_FORM_NAME 0x23 +#define SPHO_TP_FORM_NOM 0x23 -#define SPHO_TP_FORM_VAR 0x40 +#define SPHO_TP_FORM_MEMBER 0x24 -#define SPHO_TP_FORM_MASK 0xff - -#define SPHO_TP_MOD_FIRST (SPHO_TP_FORM_MASK + 1) - -// #define SPHO_TP_MOD_VAR (SPHO_TP_FLAG_FIRST) -// #define SPHO_TP_MOD_NOMINAL (SPHO_TP_FLAG_FIRST << 1) +// #define SPHO_TP_FORM_SUB 0x96 #define SPHO_TP_ERR(tp, err) SPHO_ERR((tp)->sc->ctx, (err)) +//struct spho_var *spho_var_create(struct spho_scope *, char *, size_t); +//struct spho_var *spho_var_get(struct spho_scope *, char *, size_t); + struct spho_tp *spho_tp_create_conj(struct spho_scope *, struct spho_tp *, struct spho_tp *); struct spho_tp *spho_tp_create_disj(struct spho_scope *, struct spho_tp *, @@ -49,11 +45,10 @@ struct spho_tp *spho_tp_create_appl(struct spho_scope *, struct spho_nom *, struct spho_tp_l *); struct spho_tp *spho_tp_create_member(struct spho_scope *, struct spho_nom *, struct spho_tp *); -struct spho_tp *spho_tp_create_var(struct spho_scope *, struct spho_nom *); -struct spho_tp *spho_tp_create_nominal(struct spho_scope *, struct spho_nom *); - -struct spho_tp_op *spho_tp_op_create(struct spho_scope *, - struct spho_scope *, struct spho_tp *); +//struct spho_tp *spho_tp_create_const(struct spho_scope *, struct spho_const *); +// struct spho_tp *spho_tp_create_var(struct spho_scope *, struct spho_var *); +// struct spho_tp *spho_tp_create_sub(struct spho_scope *, struct spho_tp *, +// struct spho_tp *); void spho_tp_destroy(struct spho_tp *); diff --git a/include/spho/util.h b/include/spho/util.h new file mode 100644 index 0000000..2cb9681 --- /dev/null +++ b/include/spho/util.h @@ -0,0 +1,25 @@ +#ifndef _SPHO_UTIL_H +#define _SPHO_UTIL_H + + +#define SPHO_UTIL_SLIST_DESTROY(l, elmtype, next, term) \ +do { \ + struct elmtype *elm; \ + while (! SLIST_EMPTY(l)) { \ + elm = SLIST_FIRST(l); \ + SLIST_REMOVE_HEAD(l, next); \ + term(elm); \ + free(elm); \ + } \ +} while (0) + +#ifdef SPHO_USE_STRLCPY +#define SPHO_STRLCPY(dst, src, len) strlcpy(dst, src, len) +#else +#define SPHO_STRLCPY(dst, src, len) \ + (size_t)snprintf(dst, len, "%s", src) +#endif + + +#endif + diff --git a/src/msph/sphophi.c b/src/msph/sphophi.c index a9dec26..8e39263 100644 --- a/src/msph/sphophi.c +++ b/src/msph/sphophi.c @@ -1,7 +1,5 @@ #include -#include "msph/tree.h" -#include "spho/scope.h" #include "spho/spho.h" #include "spho/tp.h" @@ -11,20 +9,10 @@ typedef int (*msph_tree_sphophi_f)(struct spho_scope *, struct msph_tree *); static int msph_tree_sphophi_decor_scope(struct spho_scope *, struct msph_tree *); -static int msph_tree_sphophi_decor_tpexpr_nom(struct spho_scope *, +static int msph_tree_sphophi_decor_nom_lookup(struct spho_scope *, struct msph_tree *); static int msph_tree_sphophi_decor_tp(struct spho_scope *, struct msph_tree *); -static int msph_tree_sphophi_tp_prebind(struct spho_scope *, - struct msph_tree *); - -/* is the tree a name binding? */ -#define IS_BINDING(tree) (TREE_ID(tree) == MSPH_TREE_TPDEF || \ - TREE_ID(tree) == MSPH_TREE_NOMINDECL || \ - TREE_ID(tree) == MSPH_TREE_MEMBDECL || \ - TREE_ID(tree) == MSPH_TREE_FORALL) -/* is the tree a type expression? */ -#define IS_TPEXPR(tree) ((tree)->type & MSPH_TREE_TPEXPR) /* foreach_pre: top down foreach */ static int msph_sphophi_foreach_pre(msph_tree_sphophi_f, @@ -39,10 +27,6 @@ static int msph_sphophi_foreach_pre_assert(msph_tree_sphophi_f, struct spho_scope *, struct msph_tree_assert *); static int msph_sphophi_foreach_pre_membdecl(msph_tree_sphophi_f, struct spho_scope *, struct msph_tree_membdecl *); -static int msph_sphophi_foreach_pre_namedecl(msph_tree_sphophi_f, - struct spho_scope *, struct msph_tree_namedecl *); -static int msph_sphophi_foreach_pre_nameref(msph_tree_sphophi_f, - struct spho_scope *, struct msph_tree_nameref *); static int msph_sphophi_foreach_pre_tpdef(msph_tree_sphophi_f, struct spho_scope *, struct msph_tree_tpdef *); static int msph_sphophi_foreach_pre_nomindecl(msph_tree_sphophi_f, @@ -53,10 +37,10 @@ static int msph_sphophi_foreach_pre_true(msph_tree_sphophi_f, struct spho_scope *, struct msph_tree_true *); static int msph_sphophi_foreach_pre_false(msph_tree_sphophi_f, struct spho_scope *, struct msph_tree_false *); -static int msph_sphophi_foreach_pre_tpname(msph_tree_sphophi_f, - struct spho_scope *, struct msph_tree_tpname *); -static int msph_sphophi_foreach_pre_tpappl(msph_tree_sphophi_f, - struct spho_scope *, struct msph_tree_tpappl *); +static int msph_sphophi_foreach_pre_name(msph_tree_sphophi_f, + struct spho_scope *, struct msph_tree_name *); +static int msph_sphophi_foreach_pre_appl(msph_tree_sphophi_f, + struct spho_scope *, struct msph_tree_appl *); static int msph_sphophi_foreach_pre_trait(msph_tree_sphophi_f, struct spho_scope *, struct msph_tree_trait *); static int msph_sphophi_foreach_pre_conj(msph_tree_sphophi_f, @@ -73,6 +57,8 @@ static int msph_sphophi_foreach_pre_forall(msph_tree_sphophi_f, struct spho_scope *, struct msph_tree_forall *); static int msph_sphophi_foreach_pre_paren(msph_tree_sphophi_f, struct spho_scope *, struct msph_tree_paren *); +static int msph_sphophi_foreach_pre_ident(msph_tree_sphophi_f, + struct spho_scope *, struct msph_tree_ident *); /* foreach_post: bottom up foreach */ static int msph_sphophi_foreach_post(msph_tree_sphophi_f, @@ -97,10 +83,10 @@ static int msph_sphophi_foreach_post_true(msph_tree_sphophi_f, struct spho_scope *, struct msph_tree_true *); static int msph_sphophi_foreach_post_false(msph_tree_sphophi_f, struct spho_scope *, struct msph_tree_false *); -static int msph_sphophi_foreach_post_tpname(msph_tree_sphophi_f, - struct spho_scope *, struct msph_tree_tpname *); -static int msph_sphophi_foreach_post_tpappl(msph_tree_sphophi_f, - struct spho_scope *, struct msph_tree_tpappl *); +static int msph_sphophi_foreach_post_name(msph_tree_sphophi_f, + struct spho_scope *, struct msph_tree_name *); +static int msph_sphophi_foreach_post_appl(msph_tree_sphophi_f, + struct spho_scope *, struct msph_tree_appl *); static int msph_sphophi_foreach_post_trait(msph_tree_sphophi_f, struct spho_scope *, struct msph_tree_trait *); static int msph_sphophi_foreach_post_conj(msph_tree_sphophi_f, @@ -117,10 +103,8 @@ static int msph_sphophi_foreach_post_forall(msph_tree_sphophi_f, struct spho_scope *, struct msph_tree_forall *); static int msph_sphophi_foreach_post_paren(msph_tree_sphophi_f, struct spho_scope *, struct msph_tree_paren *); -static int msph_sphophi_foreach_post_namedecl(msph_tree_sphophi_f, - struct spho_scope *, struct msph_tree_namedecl *); -static int msph_sphophi_foreach_post_nameref(msph_tree_sphophi_f, - struct spho_scope *, struct msph_tree_nameref *); +static int msph_sphophi_foreach_post_ident(msph_tree_sphophi_f, + struct spho_scope *, struct msph_tree_ident *); int msph_sphophi_init(struct msph_tree_root *root) { @@ -141,7 +125,7 @@ msph_sphophi_scope(struct msph_tree_root *root) int msph_sphophi_nom_lookup(struct msph_tree_root *root) { - return (msph_sphophi_foreach_pre(msph_tree_sphophi_decor_tpexpr_nom, + return (msph_sphophi_foreach_pre(msph_tree_sphophi_decor_nom_lookup, root)); } @@ -151,13 +135,6 @@ msph_sphophi_tp(struct msph_tree_root *root) return (msph_sphophi_foreach_post(msph_tree_sphophi_decor_tp, root)); } -int -msph_sphophi_tp_prebind(struct msph_tree_root *root) -{ - return (msph_sphophi_foreach_pre(msph_tree_sphophi_tp_prebind, - root)); -} - int msph_sphophi(struct msph_tree_root *root) { int ret; @@ -170,47 +147,51 @@ int msph_sphophi(struct msph_tree_root *root) return (ret); if ((ret = msph_sphophi_tp(root)) != 0) return (ret); - if ((ret = msph_sphophi_tp_prebind(root)) != 0) - return (ret); return (ret); } +#define IS_BINDING(tree) (((tree)->type == MSPH_TREE_TPDEF) || \ + ((tree)->type == MSPH_TREE_NOMINDECL) || \ + ((tree)->type == MSPH_TREE_MEMBDECL) || \ + ((tree)->type == MSPH_TREE_FORALL)) +#define IS_TPEXPR(tree) (((tree)->type & MSPH_TREE_TPEXPR)) static int msph_tree_sphophi_decor_scope(struct spho_scope *sc, struct msph_tree *tree) { int ret; + struct msph_tree_unit *unit; + struct msph_tree_trait *trait; + struct msph_tree_forall *forall; struct msph_tree_ident *ident; - struct msph_tree_tpdef *tpdef; ret = 0; - switch (TREE_ID(tree)) { + switch (tree->type) { case MSPH_TREE_UNIT: - case MSPH_TREE_TRAIT: - case MSPH_TREE_FORALL: - if ((SCOPE(tree) = spho_scope_create(sc)) == NULL) + unit = (struct msph_tree_unit *)tree; + if ((unit->dec.sc = spho_scope_create(sc)) == NULL) ret = -1; - ADD_FLAG(tree, MSPH_TREE_FLAG_SCOPE); break; - case MSPH_TREE_TPDEF: - tpdef = (struct msph_tree_tpdef *)tree; - if (! STAILQ_EMPTY(&tpdef->params) && - ((SCOPE(tpdef) = spho_scope_create(sc)) == NULL)) { + case MSPH_TREE_TRAIT: + trait = (struct msph_tree_trait *)tree; + if ((trait->dec.sc = spho_scope_create(sc)) == NULL) + ret = -1; + break; + case MSPH_TREE_FORALL: + forall = (struct msph_tree_forall *)tree; + if ((forall->dec.sc = spho_scope_create(sc)) == NULL) ret = -1; - } - ADD_FLAG(tree, MSPH_TREE_FLAG_SCOPE); break; case MSPH_TREE_IDENT: if (! IS_BINDING(tree->parent)) break; ident = (struct msph_tree_ident *)tree; - if ((NOM(ident) = spho_scope_nom_add(sc, ident->str, + if ((ident->dec.nom = spho_scope_nom_add(sc, ident->str, sizeof(ident->str))) == NULL) ret = -1; - ADD_FLAG(tree, MSPH_TREE_FLAG_NOM); break; default: break; @@ -220,7 +201,7 @@ msph_tree_sphophi_decor_scope(struct spho_scope *sc, struct msph_tree *tree) } static int -msph_tree_sphophi_decor_tpexpr_nom(struct spho_scope *sc, +msph_tree_sphophi_decor_nom_lookup(struct spho_scope *sc, struct msph_tree *tree) { int ret; @@ -228,14 +209,16 @@ msph_tree_sphophi_decor_tpexpr_nom(struct spho_scope *sc, ret = 0; - switch (TREE_ID(tree)) { + switch (tree->type) { case MSPH_TREE_IDENT: - if (! IS_TPEXPR(tree->parent)) + if (tree->parent->type != MSPH_TREE_NAME) break; ident = (struct msph_tree_ident *)tree; - ret = spho_scope_nom_lookup_str_strict(sc, ident->str, - sizeof(ident->str), &NOM(ident)); - + if ((ret = spho_scope_nom_lookup(sc, ident->str, + sizeof(ident->str), &ident->dec.nom)) != 0) + break; + if (ident->dec.nom == NULL) + ret = -1; break; default: break; @@ -244,17 +227,20 @@ msph_tree_sphophi_decor_tpexpr_nom(struct spho_scope *sc, return (ret); } +#define TP(ptr) ((ptr)->dec.tp) +#define NOM(ptr) ((ptr)->dec.nom) + static int msph_tree_sphophi_decor_tp(struct spho_scope *sc, struct msph_tree *tree) { int ret; - struct msph_tree_tpexpr *tpexpr_i; + struct msph_tree_tpexpr *tpexpr, *tpexpr_i; struct msph_tree_conj *conj; struct msph_tree_disj *disj; struct msph_tree_impl *impl; struct msph_tree_arrow *arrow; - struct msph_tree_tpname *tpname; - struct msph_tree_tpappl *tpappl; + struct msph_tree_name *name; + struct msph_tree_appl *appl; struct msph_tree_box *box; struct msph_tree_forall *forall; struct msph_tree_paren *paren; @@ -274,99 +260,90 @@ msph_tree_sphophi_decor_tp(struct spho_scope *sc, struct msph_tree *tree) if (! (tree->type & MSPH_TREE_TPEXPR)) return (0); - switch (TREE_ID(tree)) { + tpexpr = (struct msph_tree_tpexpr *)tree; + + switch (tree->type) { case MSPH_TREE_CONJ: conj = (struct msph_tree_conj *)tree; - if ((TP(conj) = spho_tp_create_conj(sc, TP(conj->ltp), + if ((TP(&conj->htpe) = spho_tp_create_conj(sc, TP(conj->ltp), TP(conj->rtp))) == NULL) goto cleanup; - ADD_FLAG(conj, MSPH_TREE_FLAG_TP); break; case MSPH_TREE_DISJ: disj = (struct msph_tree_disj *)tree; - if ((TP(disj) = spho_tp_create_conj(sc, TP(disj->ltp), + if ((TP(&disj->htpe) = spho_tp_create_conj(sc, TP(disj->ltp), TP(disj->rtp))) == NULL) goto cleanup; - ADD_FLAG(disj, MSPH_TREE_FLAG_TP); break; case MSPH_TREE_IMPL: impl = (struct msph_tree_impl *)tree; - if ((TP(impl) = spho_tp_create_conj(sc, TP(impl->ltp), + if ((TP(&impl->htpe) = spho_tp_create_conj(sc, TP(impl->ltp), TP(impl->rtp))) == NULL) goto cleanup; - ADD_FLAG(impl, MSPH_TREE_FLAG_TP); break; case MSPH_TREE_ARROW: arrow = (struct msph_tree_arrow *)tree; - if ((TP(arrow) = spho_tp_create_conj(sc, TP(arrow->ltp), + if ((TP(&arrow->htpe) = spho_tp_create_conj(sc, TP(arrow->ltp), TP(arrow->rtp))) == NULL) goto cleanup; - ADD_FLAG(arrow, MSPH_TREE_FLAG_TP); break; - case MSPH_TREE_TPNAME: - tpname = (struct msph_tree_tpname *)tree; - if ((TP(tpname) = spho_tp_create_name(sc, NOM(tpname->name))) + case MSPH_TREE_NAME: + name = (struct msph_tree_name *)tree; + if ((TP(&name->htpe) = spho_tp_create_name(sc, NOM(name->id))) == NULL) goto cleanup; - ADD_FLAG(tpname, MSPH_TREE_FLAG_TP); break; - case MSPH_TREE_TPAPPL: - tpappl = (struct msph_tree_tpappl *)tree; + case MSPH_TREE_APPL: + appl = (struct msph_tree_appl *)tree; if ((tps = malloc(sizeof(*tps))) == NULL) { SPHO_SC_ERR(sc, SPHO_ERR_SYS); goto cleanup; } STAILQ_INIT(tps); - STAILQ_FOREACH(tpexpr_i, &tpappl->args, entries) { - STAILQ_INSERT_TAIL(tps, TP(tpexpr_i), entries); + STAILQ_FOREACH(tpexpr_i, &appl->head, entries) { + STAILQ_INSERT_TAIL(tps, tpexpr_i->dec.tp, entries); } - if ((TP(tpappl) = spho_tp_create_appl(sc, NOM(tpappl->name), + if ((TP(&appl->htpe) = spho_tp_create_appl(sc, NOM(appl->id), tps)) == NULL) goto cleanup; tps = NULL; - ADD_FLAG(tpappl, MSPH_TREE_FLAG_TP); break; case MSPH_TREE_TRUE: - if ((TP(tree) = spho_tp_create_true(sc)) == NULL) + if ((TP(tpexpr) = spho_tp_create_true(sc)) == NULL) goto cleanup; - ADD_FLAG(tree, MSPH_TREE_FLAG_TP); break; case MSPH_TREE_FALSE: - if ((TP(tree) = spho_tp_create_false(sc)) == NULL) + if ((TP(tpexpr) = spho_tp_create_false(sc)) == NULL) goto cleanup; - ADD_FLAG(tree, MSPH_TREE_FLAG_TP); break; case MSPH_TREE_FORALL: forall = (struct msph_tree_forall *)tree; - if ((TP(forall) = spho_tp_create_forall(sc, - NOM(forall->name), TP(forall->inner))) == NULL) + if ((TP(&forall->htpe) = spho_tp_create_forall(sc, + NOM(forall->id), TP(forall->inner))) == NULL) goto cleanup; - ADD_FLAG(forall, MSPH_TREE_FLAG_TP); break; case MSPH_TREE_BOX: box = (struct msph_tree_box *)tree; - if ((TP(box) = spho_tp_create_box(sc, TP(box->inner))) + if ((TP(&box->htpe) = spho_tp_create_box(sc, TP(box->inner))) == NULL) goto cleanup; - ADD_FLAG(box, MSPH_TREE_FLAG_TP); break; case MSPH_TREE_PAREN: paren = (struct msph_tree_paren *)tree; - if ((TP(paren) = TP(paren->inner)) == NULL) + if ((TP(&paren->htpe) = TP(paren->inner)) == NULL) goto cleanup; - ADD_FLAG(paren, MSPH_TREE_FLAG_TP); break; case MSPH_TREE_TRAIT: trait = (struct msph_tree_trait *)tree; STAILQ_FOREACH(dir, &trait->body->head, entries) { - if (TREE_ID(dir) != MSPH_TREE_MEMBDECL) + if (T(dir)->type != MSPH_TREE_MEMBDECL) continue; membd = (struct msph_tree_membdecl *)dir; // TODO check that we make sure to dealloc when // spho has stabilized a bit - if ((tp_memb = spho_tp_create_member(sc, NOM(membd->name), - TP(membd->tp))) == NULL) + if ((tp_memb = spho_tp_create_member(sc, membd->id->dec.nom, + membd->tp->dec.tp)) == NULL) goto cleanup; if (tp == NULL) { tp = tp_memb; @@ -375,12 +352,8 @@ msph_tree_sphophi_decor_tp(struct spho_scope *sc, struct msph_tree *tree) == NULL) goto cleanup; } + trait->htpe.dec.tp = tp; } - if (tp == NULL) - tp = spho_tp_create_true(sc); - SPHO_ASSERT(tp != NULL); - TP(trait) = tp; - ADD_FLAG(trait, MSPH_TREE_FLAG_TP); break; default: SPHO_ASSERT(0); @@ -396,61 +369,6 @@ cleanup: return (ret); } -static int -msph_tree_sphophi_tp_prebind(struct spho_scope *sc, - struct msph_tree *tree) -{ - int ret; - struct spho_tp_op *op; - struct msph_tree_tpdef *tpdef; - struct msph_tree_namedecl *name; - - ret = 0; - - if (HAS_SCOPE(tree)) { - if (spho_scope_prebind_init(SCOPE(tree)) == -1) - return (-1); - } - - switch (TREE_ID(tree)) { - case MSPH_TREE_TPDEF: - tpdef = (struct msph_tree_tpdef *)tree; - - if (HAS_PARAMS(tpdef)) { - SPHO_ASSERT(HAS_SCOPE(tpdef)); - SPHO_ASSERT(SCOPE(tpdef) != NULL); - SPHO_ASSERT(SCOPE(tpdef)->bind_loc != NULL); - - STAILQ_FOREACH(name, &tpdef->params, entries) { - if (spho_scope_prebind_undef(SCOPE(tpdef), - NOM(name)) == -1) { - return (-1); - } - } - - if ((op = spho_tp_op_create(sc, SCOPE(tpdef), - TP(tpdef->tp))) == NULL) { - return (-1); - } - - if ((ret = spho_scope_prebind_tp_op(sc, NOM(name), op)) - == -1) { - return (-1); - } - } else { - if ((ret = spho_scope_prebind_tp(sc, NOM(tpdef->name), - TP(tpdef->tp))) == -1) { - return (-1); - } - } - break; - default: - break; - } - - return (ret); -} - /* foreach pre: top down foreach node */ static int msph_sphophi_foreach_pre(msph_tree_sphophi_f f, struct msph_tree_root *root) @@ -459,14 +377,17 @@ msph_sphophi_foreach_pre(msph_tree_sphophi_f f, struct msph_tree_root *root) struct spho_scope *sc; struct msph_tree_unit *unit; - SPHO_PRECOND(f != NULL); - SPHO_PRECOND(root != NULL); - SPHO_PRECOND(root->ctx != NULL); - SPHO_PRECOND(root->ctx->spho != NULL); + if (root == NULL || root->ctx == NULL) + return (-1); + + if (root->ctx->spho == NULL) { + MSPH_ERR(root->ctx, MSPH_ERR_TYPE_INVAL); + return (-1); + } sc = spho_scope_global(root->ctx->spho); - if ((ret = f(sc, TREE(root))) != 0) { + if ((ret = f(sc, T(root))) != 0) { goto err; } @@ -488,13 +409,10 @@ msph_sphophi_foreach_pre_unit(msph_tree_sphophi_f f, struct spho_scope *sc, { int ret; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(unit != NULL); - - if ((ret = f(sc, TREE(unit))) != 0) + if ((ret = f(sc, T(unit))) != 0) return (ret); - sc = SCOPE(unit); + sc = GET_SCOPE(unit); return (msph_sphophi_foreach_pre_body(f, sc, unit->body)); } @@ -506,10 +424,7 @@ msph_sphophi_foreach_pre_body(msph_tree_sphophi_f f, struct spho_scope *sc, int ret; struct msph_tree_dir *dir; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(body != NULL); - - if ((ret = f(sc, TREE(body))) != 0) + if ((ret = f(sc, T(body))) != 0) return (ret); ret = 0; @@ -527,11 +442,8 @@ msph_sphophi_foreach_pre_dir(msph_tree_sphophi_f f, struct spho_scope *sc, { int ret; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(dir != NULL); - ret = -1; - switch (TREE_ID(dir)) { + switch (dir->htxt.htr.type) { case MSPH_TREE_TPDEF: ret = msph_sphophi_foreach_pre_tpdef(f, sc, (struct msph_tree_tpdef *)dir); @@ -561,26 +473,13 @@ msph_sphophi_foreach_pre_tpdef(msph_tree_sphophi_f f, struct spho_scope *sc, struct msph_tree_tpdef *tpdef) { int ret; - struct msph_tree_namedecl *name; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(tpdef != NULL); - - if ((ret = f(sc, TREE(tpdef))) != 0) + if ((ret = f(sc, T(tpdef))) != 0) return (ret); - if ((ret = msph_sphophi_foreach_pre_namedecl(f, sc, tpdef->name)) != 0) + if ((ret = msph_sphophi_foreach_pre_ident(f, sc, tpdef->id)) != 0) return (ret); - sc = HAS_SCOPE(tpdef) ? SCOPE(tpdef) : sc; - - STAILQ_FOREACH(name, &tpdef->params, entries) { - if ((ret = msph_sphophi_foreach_pre_namedecl(f, sc, name)) - != 0) { - return (ret); - } - } - return (msph_sphophi_foreach_pre_tpexpr(f, sc, tpdef->tp)); } @@ -590,13 +489,10 @@ msph_sphophi_foreach_pre_nomindecl(msph_tree_sphophi_f f, struct spho_scope *sc, { int ret; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(nomd != NULL); - - if ((ret = f(sc, TREE(nomd))) != 0) + if ((ret = f(sc, T(nomd))) != 0) return (ret); - return (msph_sphophi_foreach_pre_namedecl(f, sc, nomd->name)); + return (msph_sphophi_foreach_pre_ident(f, sc, nomd->id)); } static int @@ -605,13 +501,10 @@ msph_sphophi_foreach_pre_membdecl(msph_tree_sphophi_f f, struct spho_scope *sc, { int ret; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(membd != NULL); - - if ((ret = f(sc, TREE(membd))) != 0) + if ((ret = f(sc, T(membd))) != 0) return (ret); - if (msph_sphophi_foreach_pre_namedecl(f, sc, membd->name) != 0) + if (msph_sphophi_foreach_pre_ident(f, sc, membd->id) != 0) return (ret); if (msph_sphophi_foreach_pre_tpexpr(f, sc, membd->tp) != 0) return (ret); @@ -625,7 +518,7 @@ msph_sphophi_foreach_pre_assert(msph_tree_sphophi_f f, struct spho_scope *sc, { int ret; - if ((ret = f(sc, TREE(ass))) != 0) + if ((ret = f(sc, T(ass))) != 0) return (ret); if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, ass->ltp)) != 0) @@ -637,23 +530,10 @@ msph_sphophi_foreach_pre_assert(msph_tree_sphophi_f f, struct spho_scope *sc, } static int -msph_sphophi_foreach_pre_namedecl(msph_tree_sphophi_f f, struct spho_scope *sc, - struct msph_tree_namedecl *name) +msph_sphophi_foreach_pre_ident(msph_tree_sphophi_f f, struct spho_scope *sc, + struct msph_tree_ident *ident) { - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(name != NULL); - - return (f(sc, TREE(name))); -} - -static int -msph_sphophi_foreach_pre_nameref(msph_tree_sphophi_f f, struct spho_scope *sc, - struct msph_tree_nameref *name) -{ - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(name != NULL); - - return (f(sc, TREE(name))); + return (f(sc, T(ident))); } static int @@ -662,12 +542,9 @@ msph_sphophi_foreach_pre_tpexpr(msph_tree_sphophi_f f, struct spho_scope *sc, { int ret; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(tpexpr != NULL); - ret = -1; - switch (TREE_ID(tpexpr)) { + switch (tpexpr->htxt.htr.type) { case MSPH_TREE_CONJ: ret = msph_sphophi_foreach_pre_conj(f, sc, (struct msph_tree_conj *)tpexpr); @@ -684,13 +561,13 @@ msph_sphophi_foreach_pre_tpexpr(msph_tree_sphophi_f f, struct spho_scope *sc, ret = msph_sphophi_foreach_pre_arrow(f, sc, (struct msph_tree_arrow *)tpexpr); break; - case MSPH_TREE_TPNAME: - ret = msph_sphophi_foreach_pre_tpname(f, sc, - (struct msph_tree_tpname *)tpexpr); + case MSPH_TREE_NAME: + ret = msph_sphophi_foreach_pre_name(f, sc, + (struct msph_tree_name *)tpexpr); break; - case MSPH_TREE_TPAPPL: - ret = msph_sphophi_foreach_pre_tpappl(f, sc, - (struct msph_tree_tpappl *)tpexpr); + case MSPH_TREE_APPL: + ret = msph_sphophi_foreach_pre_appl(f, sc, + (struct msph_tree_appl *)tpexpr); break; case MSPH_TREE_TRAIT: ret = msph_sphophi_foreach_pre_trait(f, sc, @@ -717,7 +594,7 @@ msph_sphophi_foreach_pre_tpexpr(msph_tree_sphophi_f f, struct spho_scope *sc, (struct msph_tree_false *)tpexpr); break; default: - SPHO_RIP("default-reach"); + SPHO_ASSERT(0); break; } @@ -730,10 +607,7 @@ msph_sphophi_foreach_pre_conj(msph_tree_sphophi_f f, struct spho_scope *sc, { int ret; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(conj != NULL); - - if ((ret = f(sc, TREE(conj))) != 0) + if ((ret = f(sc, T(conj))) != 0) return (ret); if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, conj->ltp)) != 0) @@ -748,10 +622,7 @@ msph_sphophi_foreach_pre_disj(msph_tree_sphophi_f f, struct spho_scope *sc, { int ret; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(disj != NULL); - - if ((ret = f(sc, TREE(disj))) != 0) + if ((ret = f(sc, T(disj))) != 0) return (ret); if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, disj->ltp)) != 0) return (ret); @@ -764,10 +635,7 @@ msph_sphophi_foreach_pre_impl(msph_tree_sphophi_f f, struct spho_scope *sc, { int ret; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(impl != NULL); - - if ((ret = f(sc, TREE(impl))) != 0) + if ((ret = f(sc, T(impl))) != 0) return (ret); if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, impl->ltp)) != 0) @@ -781,10 +649,7 @@ msph_sphophi_foreach_pre_arrow(msph_tree_sphophi_f f, struct spho_scope *sc, { int ret; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(arrow != NULL); - - if ((ret = f(sc, TREE(arrow))) != 0) + if ((ret = f(sc, T(arrow))) != 0) return (ret); if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, arrow->ltp)) != 0) @@ -793,35 +658,29 @@ msph_sphophi_foreach_pre_arrow(msph_tree_sphophi_f f, struct spho_scope *sc, } static int -msph_sphophi_foreach_pre_tpname(msph_tree_sphophi_f f, struct spho_scope *sc, - struct msph_tree_tpname *name) +msph_sphophi_foreach_pre_name(msph_tree_sphophi_f f, struct spho_scope *sc, + struct msph_tree_name *name) { int ret; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(name != NULL); - - if ((ret = f(sc, TREE(name))) != 0) + if ((ret = f(sc, T(name))) != 0) return (ret); - return (msph_sphophi_foreach_pre_nameref(f, sc, name->name)); + return (msph_sphophi_foreach_pre_ident(f, sc, name->id)); } static int -msph_sphophi_foreach_pre_tpappl(msph_tree_sphophi_f f, struct spho_scope *sc, - struct msph_tree_tpappl *appl) +msph_sphophi_foreach_pre_appl(msph_tree_sphophi_f f, struct spho_scope *sc, + struct msph_tree_appl *appl) { int ret; struct msph_tree_tpexpr *tp; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(appl != NULL); - - if ((ret = f(sc, TREE(appl))) != 0) + if ((ret = f(sc, T(appl))) != 0) return (ret); ret = 0; - STAILQ_FOREACH(tp, &appl->args, entries) { + STAILQ_FOREACH(tp, &appl->head, entries) { if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, tp)) != 0) return (ret); } @@ -834,14 +693,10 @@ msph_sphophi_foreach_pre_trait(msph_tree_sphophi_f f, struct spho_scope *sc, struct msph_tree_trait *trait) { int ret; - - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(trait != NULL); - - if ((ret = f(sc, TREE(trait))) != 0) + if ((ret = f(sc, T(trait))) != 0) return (ret); - sc = SCOPE(trait); + sc = GET_SCOPE(trait); return (msph_sphophi_foreach_pre_body(f, sc, trait->body)); } @@ -852,10 +707,7 @@ msph_sphophi_foreach_pre_box(msph_tree_sphophi_f f,struct spho_scope *sc, { int ret; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(box != NULL); - - if ((ret = f(sc, TREE(box))) != 0) + if ((ret = f(sc, T(box))) != 0) return (ret); return (msph_sphophi_foreach_pre_tpexpr(f, sc, box->inner)); @@ -866,14 +718,11 @@ msph_sphophi_foreach_pre_forall(msph_tree_sphophi_f f, struct spho_scope *sc, struct msph_tree_forall *forall) { int ret; - - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(forall != NULL); - - if ((ret = f(sc, TREE(forall))) != 0) + + if ((ret = f(sc, T(forall))) != 0) return (ret); - sc = SCOPE(forall); + sc = GET_SCOPE(forall); return (msph_sphophi_foreach_pre_tpexpr(f, sc, forall->inner)); } @@ -884,10 +733,7 @@ msph_sphophi_foreach_pre_paren(msph_tree_sphophi_f f, struct spho_scope *sc, { int ret; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(paren != NULL); - - if ((ret = f(sc, TREE(paren))) != 0) + if ((ret = f(sc, T(paren))) != 0) return (ret); return (msph_sphophi_foreach_pre_tpexpr(f, sc, paren->inner)); @@ -897,20 +743,14 @@ static int msph_sphophi_foreach_pre_true(msph_tree_sphophi_f f, struct spho_scope *sc, struct msph_tree_true *tru) { - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(tru != NULL); - - return (f(sc, TREE(tru))); + return (f(sc, T(tru))); } static int msph_sphophi_foreach_pre_false(msph_tree_sphophi_f f, struct spho_scope *sc, struct msph_tree_false *fls) { - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(fls != NULL); - - return (f(sc, TREE(fls))); + return (f(sc, T(fls))); } @@ -922,10 +762,13 @@ msph_sphophi_foreach_post(msph_tree_sphophi_f f, struct msph_tree_root *root) struct spho_scope *sc; struct msph_tree_unit *unit; - SPHO_PRECOND(f != NULL); - SPHO_PRECOND(root != NULL); - SPHO_PRECOND(root->ctx != NULL); - SPHO_PRECOND(root->ctx->spho != NULL); + if (root == NULL || root->ctx == NULL) + return (-1); + + if (root->ctx->spho == NULL) { + MSPH_ERR(root->ctx, MSPH_ERR_TYPE_INVAL); + return (-1); + } sc = spho_scope_global(root->ctx->spho); @@ -935,7 +778,7 @@ msph_sphophi_foreach_post(msph_tree_sphophi_f f, struct msph_tree_root *root) goto err; } - if ((ret = f(sc, TREE(root))) != 0) + if ((ret = f(sc, T(root))) != 0) goto err; return (ret); @@ -951,17 +794,13 @@ msph_sphophi_foreach_post_unit(msph_tree_sphophi_f f, struct spho_scope *sc, int ret; struct spho_scope *inner_sc; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(unit != NULL); - - inner_sc = SCOPE(unit); + inner_sc = GET_SCOPE(unit); if ((ret = msph_sphophi_foreach_post_body(f, inner_sc, unit->body)) - != 0) { + != 0) return (ret); - } - return (f(sc, TREE(unit))); + return (f(sc, T(unit))); } static int @@ -971,16 +810,13 @@ msph_sphophi_foreach_post_body(msph_tree_sphophi_f f, struct spho_scope *sc, int ret; struct msph_tree_dir *dir; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(body != NULL); - ret = 0; STAILQ_FOREACH(dir, &body->head, entries) { if ((ret = msph_sphophi_foreach_post_dir(f, sc, dir)) != 0) return (ret); } - return (f(sc, TREE(body))); + return (f(sc, T(body))); } static int @@ -989,11 +825,8 @@ msph_sphophi_foreach_post_dir(msph_tree_sphophi_f f, struct spho_scope *sc, { int ret; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(dir != NULL); - ret = -1; - switch (TREE_ID(dir)) { + switch (dir->htxt.htr.type) { case MSPH_TREE_TPDEF: ret = msph_sphophi_foreach_post_tpdef(f, sc, (struct msph_tree_tpdef *)dir); @@ -1023,32 +856,13 @@ msph_sphophi_foreach_post_tpdef(msph_tree_sphophi_f f, struct spho_scope *sc, struct msph_tree_tpdef *tpdef) { int ret; - struct spho_scope *sub_sc; - struct msph_tree_namedecl *name; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(tpdef != NULL); - - - if ((ret = msph_sphophi_foreach_post_namedecl(f, sc, tpdef->name)) - != 0) { + if ((ret = msph_sphophi_foreach_post_ident(f, sc, tpdef->id)) != 0) return (ret); - } - - sub_sc = HAS_SCOPE(tpdef) ? SCOPE(tpdef) : sc; - - STAILQ_FOREACH(name, &tpdef->params, entries) { - if ((ret = msph_sphophi_foreach_post_namedecl(f, sub_sc, name)) - != 0) { - return (ret); - } - } - - if ((ret = msph_sphophi_foreach_post_tpexpr(f, sub_sc, tpdef->tp)) - != 0) + if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, tpdef->tp)) != 0) return (ret); - return (f(sc, TREE(tpdef))); + return (f(sc, T(tpdef))); } static int @@ -1057,13 +871,10 @@ msph_sphophi_foreach_post_nomindecl(msph_tree_sphophi_f f, { int ret; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(nomd != NULL); - - if ((ret = msph_sphophi_foreach_post_namedecl(f, sc, nomd->name)) != 0) + if ((ret = msph_sphophi_foreach_post_ident(f, sc, nomd->id)) != 0) return (ret); - return (f(sc, TREE(nomd))); + return (f(sc, T(nomd))); } static int @@ -1072,15 +883,12 @@ msph_sphophi_foreach_post_membdecl(msph_tree_sphophi_f f, struct spho_scope *sc, { int ret; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(membd != NULL); - - if ((ret = msph_sphophi_foreach_post_namedecl(f, sc, membd->name)) != 0) + if ((ret = msph_sphophi_foreach_post_ident(f, sc, membd->id)) != 0) return (ret); if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, membd->tp)) != 0) return (ret); - return (f(sc, TREE(membd))); + return (f(sc, T(membd))); } static int @@ -1089,35 +897,19 @@ msph_sphophi_foreach_post_assert(msph_tree_sphophi_f f, struct spho_scope *sc, { int ret; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(ass != NULL); - if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, ass->ltp)) != 0) return (ret); if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, ass->rtp)) != 0) return (ret); - return (f(sc, TREE(ass))); + return (f(sc, T(ass))); } static int -msph_sphophi_foreach_post_namedecl(msph_tree_sphophi_f f, struct spho_scope *sc, - struct msph_tree_namedecl *name) +msph_sphophi_foreach_post_ident(msph_tree_sphophi_f f, struct spho_scope *sc, + struct msph_tree_ident *ident) { - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(name != NULL); - - return (f(sc, TREE(name))); -} - -static int -msph_sphophi_foreach_post_nameref(msph_tree_sphophi_f f, struct spho_scope *sc, - struct msph_tree_nameref *name) -{ - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(name != NULL); - - return (f(sc, TREE(name))); + return (f(sc, T(ident))); } static int @@ -1126,12 +918,9 @@ msph_sphophi_foreach_post_tpexpr(msph_tree_sphophi_f f, struct spho_scope *sc, { int ret; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(tpexpr != NULL); - ret = -1; - switch (TREE_ID(tpexpr)) { + switch (tpexpr->htxt.htr.type) { case MSPH_TREE_CONJ: ret = msph_sphophi_foreach_post_conj(f, sc, (struct msph_tree_conj *)tpexpr); @@ -1148,13 +937,13 @@ msph_sphophi_foreach_post_tpexpr(msph_tree_sphophi_f f, struct spho_scope *sc, ret = msph_sphophi_foreach_post_arrow(f, sc, (struct msph_tree_arrow *)tpexpr); break; - case MSPH_TREE_TPNAME: - ret = msph_sphophi_foreach_post_tpname(f, sc, - (struct msph_tree_tpname *)tpexpr); + case MSPH_TREE_NAME: + ret = msph_sphophi_foreach_post_name(f, sc, + (struct msph_tree_name *)tpexpr); break; - case MSPH_TREE_TPAPPL: - ret = msph_sphophi_foreach_post_tpappl(f, sc, - (struct msph_tree_tpappl *)tpexpr); + case MSPH_TREE_APPL: + ret = msph_sphophi_foreach_post_appl(f, sc, + (struct msph_tree_appl *)tpexpr); break; case MSPH_TREE_TRAIT: ret = msph_sphophi_foreach_post_trait(f, sc, @@ -1194,15 +983,12 @@ msph_sphophi_foreach_post_conj(msph_tree_sphophi_f f, struct spho_scope *sc, { int ret; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(conj != NULL); - if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, conj->ltp)) != 0) return (ret); if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, conj->rtp)) != 0) return (ret); - return (f(sc, TREE(conj))); + return (f(sc, T(conj))); } @@ -1212,15 +998,12 @@ msph_sphophi_foreach_post_disj(msph_tree_sphophi_f f, struct spho_scope *sc, { int ret; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(disj != NULL); - if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, disj->ltp)) != 0) return (ret); if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, disj->rtp)) != 0) return (ret); - return (f(sc, TREE(disj))); + return (f(sc, T(disj))); } static int @@ -1229,15 +1012,12 @@ msph_sphophi_foreach_post_impl(msph_tree_sphophi_f f, struct spho_scope *sc, { int ret; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(impl != NULL); - if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, impl->ltp)) != 0) return (ret); if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, impl->rtp)) != 0) return (ret); - return (f(sc, TREE(impl))); + return (f(sc, T(impl))); } static int @@ -1246,46 +1026,41 @@ msph_sphophi_foreach_post_arrow(msph_tree_sphophi_f f, struct spho_scope *sc, { int ret; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(arrow != NULL); - if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, arrow->ltp)) != 0) return (ret); if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, arrow->rtp)) != 0) return (ret); - return (f(sc, TREE(arrow))); + return (f(sc, T(arrow))); } static int -msph_sphophi_foreach_post_tpname(msph_tree_sphophi_f f, struct spho_scope *sc, - struct msph_tree_tpname *name) +msph_sphophi_foreach_post_name(msph_tree_sphophi_f f, struct spho_scope *sc, + struct msph_tree_name *name) { int ret; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(name != NULL); - - if ((ret = msph_sphophi_foreach_post_nameref(f, sc, name->name)) != 0) + if ((ret = msph_sphophi_foreach_post_ident(f, sc, name->id)) != 0) return (ret); - return (f(sc, TREE(name))); + return (f(sc, T(name))); + } static int -msph_sphophi_foreach_post_tpappl(msph_tree_sphophi_f f, struct spho_scope *sc, - struct msph_tree_tpappl *appl) +msph_sphophi_foreach_post_appl(msph_tree_sphophi_f f, struct spho_scope *sc, + struct msph_tree_appl *appl) { int ret; struct msph_tree_tpexpr *tp; ret = 0; - STAILQ_FOREACH(tp, &appl->args, entries) { + STAILQ_FOREACH(tp, &appl->head, entries) { if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, tp)) != 0) return (ret); } - return (f(sc, TREE(appl))); + return (f(sc, T(appl))); } static int @@ -1295,17 +1070,13 @@ msph_sphophi_foreach_post_trait(msph_tree_sphophi_f f, struct spho_scope *sc, int ret; struct spho_scope *inner_sc; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(trait != NULL); - - inner_sc = SCOPE(trait); + inner_sc = GET_SCOPE(trait); if ((ret = msph_sphophi_foreach_post_body(f, inner_sc, trait->body)) - != 0) { + != 0) return (ret); - } - return (f(sc, TREE(trait))); + return (f(sc, T(trait))); } static int @@ -1314,13 +1085,10 @@ msph_sphophi_foreach_post_box(msph_tree_sphophi_f f,struct spho_scope *sc, { int ret; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(box != NULL); - if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, box->inner)) != 0) return (ret); - return (f(sc, TREE(box))); + return (f(sc, T(box))); } static int @@ -1330,16 +1098,13 @@ msph_sphophi_foreach_post_forall(msph_tree_sphophi_f f, struct spho_scope *sc, int ret; struct spho_scope *inner_sc; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(forall != NULL); - - inner_sc = SCOPE(forall); + inner_sc = GET_SCOPE(forall); if ((ret = msph_sphophi_foreach_post_tpexpr(f, inner_sc, forall->inner)) != 0) return (ret); - return (f(sc, TREE(forall))); + return (f(sc, T(forall))); } @@ -1349,13 +1114,10 @@ msph_sphophi_foreach_post_paren(msph_tree_sphophi_f f, struct spho_scope *sc, { int ret; - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(paren != NULL); - if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, paren->inner)) != 0) return (ret); - return (f(sc, TREE(paren))); + return (f(sc, T(paren))); } @@ -1363,18 +1125,12 @@ static int msph_sphophi_foreach_post_true(msph_tree_sphophi_f f, struct spho_scope *sc, struct msph_tree_true *tru) { - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(tru != NULL); - - return (f(sc, TREE(tru))); + return (f(sc, T(tru))); } static int msph_sphophi_foreach_post_false(msph_tree_sphophi_f f, struct spho_scope *sc, struct msph_tree_false *fls) { - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(fls != NULL); - - return (f(sc, TREE(fls))); + return (f(sc, T(fls))); } diff --git a/src/msph/token.c b/src/msph/token.c index e83a11d..1c0adb2 100644 --- a/src/msph/token.c +++ b/src/msph/token.c @@ -5,12 +5,9 @@ #include #include -#include "spho/spho.h" - #include "msph/err.h" #include "msph/token.h" - struct msph_matcher { size_t off; size_t matchlen; diff --git a/src/msph/tree.c b/src/msph/tree.c index 199628c..440fc53 100644 --- a/src/msph/tree.c +++ b/src/msph/tree.c @@ -6,7 +6,7 @@ #include #include -#include "spho/spho.h" +#include "spho/util.h" #include "msph/tree.h" @@ -26,8 +26,7 @@ struct tree_parse { static void tree_parse_init(struct tree_parse *, struct msph_token_stream *); static int tree_parse_next_token(struct tree_parse *); -static void tree_parse_push_token(struct tree_parse *, - struct msph_token *); +static void tree_parse_push_token(struct tree_parse *, struct msph_token *); static ssize_t tree_ind_fprint(FILE *, int, struct msph_tree *); @@ -37,13 +36,8 @@ static struct msph_tree_unit *tree_parse_unit(struct tree_parse *, struct msph_tree *); static struct msph_tree_body *tree_parse_body(struct tree_parse *, struct msph_tree *); -static struct msph_tree_ident *tree_parse_ident_extsize(struct tree_parse *, - struct msph_tree *, size_t); - -static struct msph_tree_namedecl *tree_parse_namedecl(struct tree_parse *, - struct msph_tree *); -static struct msph_tree_nameref *tree_parse_nameref(struct tree_parse *, - struct msph_tree *); +static struct msph_tree_ident *tree_parse_ident(struct tree_parse *, + struct msph_tree *); static struct msph_tree_dir *tree_parse_tpdef(struct tree_parse *, struct msph_tree *); @@ -56,18 +50,16 @@ static struct msph_tree_dir *tree_parse_membdecl( struct tree_parse *, struct msph_tree *); - static struct msph_tree_tpexpr *tree_parse_tpexpr(struct tree_parse *, struct msph_tree *); static struct msph_tree_tpexpr *tree_parse_true(struct tree_parse *, struct msph_tree *); static struct msph_tree_tpexpr *tree_parse_false(struct tree_parse *, struct msph_tree *); -static struct msph_tree_tpexpr *tree_parse_tpname_or_tpappl( - struct tree_parse *, +static struct msph_tree_tpexpr *tree_parse_name(struct tree_parse *, struct msph_tree *); -static struct msph_tree_tpexpr *tree_parse_tpapplargs(struct tree_parse *, - struct msph_tree_nameref*, +static struct msph_tree_tpexpr *tree_parse_applargs(struct tree_parse *, + struct msph_tree_ident*, struct msph_tree *); static struct msph_tree_tpexpr *tree_parse_trait(struct tree_parse *, struct msph_tree *); @@ -95,8 +87,8 @@ msph_tree_makeroot(struct msph_ctx *ctx) MSPH_ERR(ctx, MSPH_ERR_SYS); return (NULL); } - TREE(root)->type = MSPH_TREE_ROOT; - TREE(root)->parent = NULL; + T(root)->type = MSPH_TREE_ROOT; + T(root)->parent = NULL; root->ctx = ctx; @@ -146,14 +138,14 @@ msph_tree_parse(struct msph_token_stream *s, struct msph_tree_root *root) struct tree_parse p; struct msph_tree_unit *unit; - if (TREE(root)->type != MSPH_TREE_ROOT) { + if (T(root)->type != MSPH_TREE_ROOT) { MSPH_ERR(s->ctx, MSPH_ERR_INVAL); return (-1); } tree_parse_init(&p, s); - if ((unit = tree_parse_unit(&p, TREE(root))) == NULL) + if ((unit = tree_parse_unit(&p, T(root))) == NULL) return (-1); STAILQ_INSERT_TAIL(&root->head, unit, entries); @@ -170,7 +162,7 @@ msph_tree_fprint(FILE *f, struct msph_tree *tree) { __attribute__((format(printf, 3, 4))) static ssize_t -indent_fprintf(FILE *f, int indent, const char *fmt, ...) +ind_fprintf(FILE *f, int indent, const char *fmt, ...) { int res; ssize_t ret; @@ -216,298 +208,284 @@ tree_ind_fprint(FILE *f, int indent, struct msph_tree *tree) struct msph_tree_arrow *arrow; struct msph_tree_box *box; struct msph_tree_forall *forall; - struct msph_tree_tpappl *tpappl; + struct msph_tree_appl *appl; struct msph_tree_trait *trait; - struct msph_tree_tpname *name; + struct msph_tree_name *name; struct msph_tree_paren *paren; struct msph_tree_ident *ident; struct msph_tree_tpexpr *tp; ret = 0; - switch (TREE_ID(tree)) { + switch (tree->type) { case MSPH_TREE_ROOT: root = (struct msph_tree_root *)tree; - if ((res = indent_fprintf(f, indent, "(root\n")) < 0) + if ((res = ind_fprintf(f, indent, "(root\n")) < 0) return (res); STAILQ_FOREACH(unit, &root->head, entries) { - if ((res = tree_ind_fprint(f, indent+1, TREE(unit))) + if ((res = tree_ind_fprint(f, indent+1, T(unit))) < 0) return (res); ret += res; } - if ((res = indent_fprintf(f, indent, ")\n")) < 0) + if ((res = ind_fprintf(f, indent, ")\n")) < 0) return (res); break; case MSPH_TREE_UNIT: unit = (struct msph_tree_unit *)tree; - if ((res = indent_fprintf(f, indent, "(unit:%s\n", unit->name)) + if ((res = ind_fprintf(f, indent, "(unit:%s\n", unit->name)) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, TREE(unit->body))) < 0) + if ((res = tree_ind_fprint(f, indent+1, T(unit->body))) < 0) return (res); ret += res; - if ((res = indent_fprintf(f, indent, ")\n")) < 0) + if ((res = ind_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; case MSPH_TREE_BODY: body = (struct msph_tree_body *)tree; - if ((res = indent_fprintf(f, indent, "(body\n")) < 0) + if ((res = ind_fprintf(f, indent, "(body\n")) < 0) return (res); ret += res; STAILQ_FOREACH(dir, &body->head, entries) { - if ((res = tree_ind_fprint(f, indent+1, TREE(dir))) + if ((res = tree_ind_fprint(f, indent+1, T(dir))) < 0) return (res); ret += res; } - if ((res = indent_fprintf(f, indent, ")\n")) < 0) + if ((res = ind_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; case MSPH_TREE_NOMINDECL: nomd = (struct msph_tree_nomindecl *)tree; - if ((res = indent_fprintf(f, indent, "(nomindecl:%u,%u\n", - TEXT(nomd)->pos.line, TEXT(nomd)->pos.col)) < 0) + if ((res = ind_fprintf(f, indent, "(nomindecl:%u,%u\n", + TXT(nomd)->pos.line, TXT(nomd)->pos.col)) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, TREE(nomd->name))) < 0) + if ((res = tree_ind_fprint(f, indent+1, T(nomd->id))) < 0) return (res); ret += res; - if ((res = indent_fprintf(f, indent, ")\n")) < 0) + if ((res = ind_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; case MSPH_TREE_ASSERT: ass = (struct msph_tree_assert *)tree; - if ((res = indent_fprintf(f, indent, "(assert:%u,%u\n", - TEXT(ass)->pos.line, TEXT(ass)->pos.col)) < 0) + if ((res = ind_fprintf(f, indent, "(assert:%u,%u\n", + TXT(ass)->pos.line, TXT(ass)->pos.col)) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, TREE(ass->ltp))) < 0) + if ((res = tree_ind_fprint(f, indent+1, T(ass->ltp))) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, TREE(ass->rtp))) < 0) + if ((res = tree_ind_fprint(f, indent+1, T(ass->rtp))) < 0) return (res); ret += res; - if ((res = indent_fprintf(f, indent, ")\n")) < 0) + if ((res = ind_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; case MSPH_TREE_TPDEF: tpdef = (struct msph_tree_tpdef *)tree; - if ((res = indent_fprintf(f, indent, "(tpdef:%u,%u\n", - TEXT(tpdef)->pos.line, TEXT(tpdef)->pos.col)) < 0) + if ((res = ind_fprintf(f, indent, "(tpdef:%u,%u\n", + TXT(tpdef)->pos.line, TXT(tpdef)->pos.col)) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, TREE(tpdef->name))) < 0) + if ((res = tree_ind_fprint(f, indent+1, T(tpdef->id))) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, TREE(tpdef->tp))) < 0) + if ((res = tree_ind_fprint(f, indent+1, T(tpdef->tp))) < 0) return (res); ret += res; - if ((res = indent_fprintf(f, indent, ")\n")) < 0) + if ((res = ind_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; case MSPH_TREE_MEMBDECL: membdecl = (struct msph_tree_membdecl *)tree; - if ((res = indent_fprintf(f, indent, "(membdecl:%u,%u\n", - TEXT(membdecl)->pos.line, TEXT(membdecl)->pos.col)) < 0) { + if ((res = ind_fprintf(f, indent, "(membdecl:%u,%u\n", + TXT(membdecl)->pos.line, TXT(membdecl)->pos.col)) < 0) return (res); - } ret += res; - if ((res = tree_ind_fprint(f, indent+1, TREE(membdecl->name))) - < 0) { + if ((res = tree_ind_fprint(f, indent+1, T(membdecl->id))) < 0) return (res); - } ret += res; - if ((res = tree_ind_fprint(f, indent+1, TREE(membdecl->tp))) - < 0) { + if ((res = tree_ind_fprint(f, indent+1, T(membdecl->tp))) < 0) return (res); - } ret += res; - if ((res = indent_fprintf(f, indent, ")\n")) < 0) + if ((res = ind_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; case MSPH_TREE_CONJ: conj = (struct msph_tree_conj *)tree; - if ((res = indent_fprintf(f, indent, "(conj:%u,%u\n", - TEXT(conj)->pos.line, TEXT(conj)->pos.col)) < 0) + if ((res = ind_fprintf(f, indent, "(conj:%u,%u\n", + TXT(conj)->pos.line, TXT(conj)->pos.col)) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, TREE(conj->ltp))) < 0) + if ((res = tree_ind_fprint(f, indent+1, T(conj->ltp))) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, TREE(conj->rtp))) < 0) + if ((res = tree_ind_fprint(f, indent+1, T(conj->rtp))) < 0) return (res); ret += res; - if ((res = indent_fprintf(f, indent, ")\n")) < 0) + if ((res = ind_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; case MSPH_TREE_DISJ: disj = (struct msph_tree_disj *)tree; - if ((res = indent_fprintf(f, indent, "(disj:%u,%u\n", - TEXT(disj)->pos.line, TEXT(disj)->pos.col)) < 0) + if ((res = ind_fprintf(f, indent, "(disj:%u,%u\n", + TXT(disj)->pos.line, TXT(disj)->pos.col)) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, TREE(disj->ltp))) < 0) + if ((res = tree_ind_fprint(f, indent+1, T(disj->ltp))) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, TREE(disj->rtp))) < 0) + if ((res = tree_ind_fprint(f, indent+1, T(disj->rtp))) < 0) return (res); ret += res; - if ((res = indent_fprintf(f, indent, ")\n")) < 0) + if ((res = ind_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; case MSPH_TREE_IMPL: impl = (struct msph_tree_impl *)tree; - if ((res = indent_fprintf(f, indent, "(impl:%u,%u\n", - TEXT(impl)->pos.line, TEXT(impl)->pos.col)) < 0) + if ((res = ind_fprintf(f, indent, "(impl:%u,%u\n", + TXT(impl)->pos.line, TXT(impl)->pos.col)) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, TREE(impl->ltp))) < 0) + if ((res = tree_ind_fprint(f, indent+1, T(impl->ltp))) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, TREE(impl->rtp))) < 0) + if ((res = tree_ind_fprint(f, indent+1, T(impl->rtp))) < 0) return (res); ret += res; - if ((res = indent_fprintf(f, indent, ")\n")) < 0) + if ((res = ind_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; case MSPH_TREE_ARROW: arrow = (struct msph_tree_arrow *)tree; - if ((res = indent_fprintf(f, indent, "(arrow:%u,%u\n", - TEXT(arrow)->pos.line, TEXT(arrow)->pos.col)) < 0) + if ((res = ind_fprintf(f, indent, "(arrow:%u,%u\n", + TXT(arrow)->pos.line, TXT(arrow)->pos.col)) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, TREE(arrow->ltp))) < 0) + if ((res = tree_ind_fprint(f, indent+1, T(arrow->ltp))) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, TREE(arrow->rtp))) < 0) + if ((res = tree_ind_fprint(f, indent+1, T(arrow->rtp))) < 0) return (res); ret += res; - if ((res = indent_fprintf(f, indent, ")\n")) < 0) + if ((res = ind_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; case MSPH_TREE_BOX: box = (struct msph_tree_box *)tree; - if ((res = indent_fprintf(f, indent, "(box:%u,%u\n", - TEXT(box)->pos.line, TEXT(box)->pos.col)) < 0) + if ((res = ind_fprintf(f, indent, "(box:%u,%u\n", + TXT(box)->pos.line, TXT(box)->pos.col)) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, TREE(box->inner))) < 0) + if ((res = tree_ind_fprint(f, indent+1, T(box->inner))) < 0) return (res); ret += res; - if ((res = indent_fprintf(f, indent, ")\n")) < 0) + if ((res = ind_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; case MSPH_TREE_FORALL: forall = (struct msph_tree_forall *)tree; - if ((res = indent_fprintf(f, indent, "(forall:%u,%u\n", - TEXT(forall)->pos.line, TEXT(forall)->pos.col)) < 0) + if ((res = ind_fprintf(f, indent, "(forall:%u,%u\n", + TXT(forall)->pos.line, TXT(forall)->pos.col)) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, TREE(forall->name))) - < 0) + if ((res = tree_ind_fprint(f, indent+1, T(forall->id))) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, TREE(forall->inner))) - < 0) { + if ((res = tree_ind_fprint(f, indent+1, T(forall->inner))) < 0) return (res); - } ret += res; - if ((res = indent_fprintf(f, indent, ")\n")) < 0) + if ((res = ind_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; case MSPH_TREE_PAREN: paren = (struct msph_tree_paren *)tree; - if ((res = indent_fprintf(f, indent, "(paren:%u,%u\n", - TEXT(paren)->pos.line, TEXT(paren)->pos.col)) < 0) + if ((res = ind_fprintf(f, indent, "(paren:%u,%u\n", + TXT(paren)->pos.line, TXT(paren)->pos.col)) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, TREE(paren->inner))) - < 0) { + if ((res = tree_ind_fprint(f, indent+1, T(paren->inner))) < 0) return (res); - } ret += res; - if ((res = indent_fprintf(f, indent, ")\n")) < 0) + if ((res = ind_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; - case MSPH_TREE_TPAPPL: - tpappl = (struct msph_tree_tpappl *)tree; - if ((res = indent_fprintf(f, indent, "(tpappl:%u,%u\n", - TEXT(tpappl)->pos.line, TEXT(tpappl)->pos.col)) < 0) + case MSPH_TREE_APPL: + appl = (struct msph_tree_appl *)tree; + if ((res = ind_fprintf(f, indent, "(appl:%u,%u\n", + TXT(appl)->pos.line, TXT(appl)->pos.col)) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, TREE(tpappl->name))) < 0) + if ((res = tree_ind_fprint(f, indent+1, T(appl->id))) < 0) return (res); ret += res; - STAILQ_FOREACH(tp, &tpappl->args, entries) { - if ((res = tree_ind_fprint(f, indent+1, TREE(tp))) < 0) + STAILQ_FOREACH(tp, &appl->head, entries) { + if ((res = tree_ind_fprint(f, indent+1, T(tp))) < 0) return (res); ret += res; } - if ((res = indent_fprintf(f, indent, ")\n")) < 0) + if ((res = ind_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; - case MSPH_TREE_TPNAME: - name = (struct msph_tree_tpname *)tree; - if ((res = indent_fprintf(f, indent, "(name:%u,%u\n", - TEXT(name)->pos.line, TEXT(name)->pos.col)) < 0) + case MSPH_TREE_NAME: + name = (struct msph_tree_name *)tree; + if ((res = ind_fprintf(f, indent, "(name:%u,%u\n", + TXT(name)->pos.line, TXT(name)->pos.col)) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, TREE(name->name))) < 0) + if ((res = tree_ind_fprint(f, indent+1, T(name->id))) < 0) return (res); ret += res; - if ((res = indent_fprintf(f, indent, ")\n")) < 0) + if ((res = ind_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; case MSPH_TREE_TRAIT: trait = (struct msph_tree_trait *)tree; - if ((res = indent_fprintf(f, indent, "(trait:%u,%u\n", - TEXT(trait)->pos.line, TEXT(trait)->pos.col)) < 0) + if ((res = ind_fprintf(f, indent, "(trait:%u,%u\n", + TXT(trait)->pos.line, TXT(trait)->pos.col)) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, TREE(trait->body))) - < 0) { + if ((res = tree_ind_fprint(f, indent+1, T(trait->body))) < 0) return (res); - } ret += res; - if ((res = indent_fprintf(f, indent, ")\n")) < 0) + if ((res = ind_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; - case MSPH_TREE_NAMEDECL: - case MSPH_TREE_NAMEREF: case MSPH_TREE_IDENT: - ident = IDENT(tree); - if ((res = indent_fprintf(f, indent, "(ident:%u,%u:%s)\n", - TEXT(ident)->pos.line, TEXT(ident)->pos.col, ident->str)) + ident = (struct msph_tree_ident *)tree; + if ((res = ind_fprintf(f, indent, "(ident:%u,%u:%s)\n", + TXT(ident)->pos.line, TXT(ident)->pos.col, ident->str)) < 0) return (res); ret += res; break; case MSPH_TREE_TRUE: - if ((res = indent_fprintf(f, indent, "(true:%u,%u)\n", - TEXT(tree)->pos.line, TEXT(tree)->pos.col)) < 0) + if ((res = ind_fprintf(f, indent, "(true:%u,%u)\n", + TXT(tree)->pos.line, TXT(tree)->pos.col)) < 0) return (res); ret += res; break; case MSPH_TREE_FALSE: - if ((res = indent_fprintf(f, indent, "(false:%u,%u)\n", - TEXT(tree)->pos.line, TEXT(tree)->pos.col)) < 0) + if ((res = ind_fprintf(f, indent, "(false:%u,%u)\n", + TXT(tree)->pos.line, TXT(tree)->pos.col)) < 0) return (res); ret += res; break; @@ -564,9 +542,9 @@ tree_parse_unit(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - TREE(unit)->type = MSPH_TREE_UNIT; - TREE(unit)->parent = parent; - DECOR_INIT(unit); + T(unit)->type = MSPH_TREE_UNIT; + T(unit)->parent = parent; + SCOPE_DECOR_INIT(&unit->dec); unit->body = NULL; if ((namelen = strlcpy(unit->name, p->s->name, sizeof(unit->name))) @@ -575,13 +553,13 @@ tree_parse_unit(struct tree_parse *p, struct msph_tree *parent) goto err; } - if ((unit->body = tree_parse_body(p, TREE(unit))) == NULL) + if ((unit->body = tree_parse_body(p, T(unit))) == NULL) goto err; return (unit); err: - free_the_tree(TREE(unit)); + free_the_tree(T(unit)); return (NULL); } @@ -598,8 +576,8 @@ tree_parse_body(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - TREE(body)->type = MSPH_TREE_BODY; - TREE(body)->parent = parent; + T(body)->type = MSPH_TREE_BODY; + T(body)->parent = parent; STAILQ_INIT(&body->head); while ((res = tree_parse_next_token(p)) > 0) { @@ -607,16 +585,16 @@ tree_parse_body(struct tree_parse *p, struct msph_tree *parent) switch(CURR_TOKEN(p)->type) { case TOK_KW_TYPE: SPHO_DEBUG_PRINT("parsing tpdef\n"); - dir = tree_parse_tpdef(p, TREE(body)); + dir = tree_parse_tpdef(p, T(body)); break; case TOK_KW_NOMINAL: - dir = tree_parse_nomindecl(p, TREE(body)); + dir = tree_parse_nomindecl(p, T(body)); break; case TOK_KW_MEMBER: - dir = tree_parse_membdecl(p, TREE(body)); + dir = tree_parse_membdecl(p, T(body)); break; case TOK_KW_ASSERT: - dir = tree_parse_assert(p, TREE(body)); + dir = tree_parse_assert(p, T(body)); break; default: if ((tok = msph_token_copy(CTX(p), CURR_TOKEN(p))) @@ -637,7 +615,7 @@ tree_parse_body(struct tree_parse *p, struct msph_tree *parent) ret: return (body); err: - free_the_tree(TREE(body)); + free_the_tree(T(body)); return (NULL); } @@ -655,7 +633,6 @@ tree_parse_tpdef(struct tree_parse *p, struct msph_tree *parent) { int res; struct msph_tree_tpdef *def; - struct msph_tree_namedecl *name; EXPECT_CURR_TOKEN(p, TOK_KW_TYPE, MSPH_TREE_TPDEF, return (NULL)); @@ -663,98 +640,43 @@ tree_parse_tpdef(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - TREE(def)->type = MSPH_TREE_TPDEF; - TREE(def)->parent = parent; - TEXT(def)->pos = CURR_TOKEN(p)->pos; - STAILQ_INIT(&def->params); - DECOR_INIT(def); + T(def)->type = MSPH_TREE_TPDEF; + T(def)->parent = parent; + TXT(def)->pos = CURR_TOKEN(p)->pos; + // TODO add scope decor when generalizing to type operators EXPECT_READ_NEXT(res, p, MSPH_TREE_TPDEF, goto err); - if ((def->name = tree_parse_namedecl(p, TREE(def))) == NULL) + if ((def->id = tree_parse_ident(p, T(def))) == NULL) goto err; EXPECT_READ_NEXT(res, p, MSPH_TREE_TPDEF, goto err); - - if (CURR_TOKEN(p)->type == TOK_LBRAK) { - ADD_FLAG(TREE(def), MSPH_TREE_FLAG_SCOPE); - - do { - EXPECT_READ_NEXT(res, p, MSPH_TREE_TPDEF, goto err); - name = tree_parse_namedecl(p, TREE(def)); - if (name == NULL) - goto err; - STAILQ_INSERT_TAIL(&def->params, name, entries); - - EXPECT_READ_NEXT(res, p, MSPH_TREE_TPDEF, goto err); - } while (CURR_TOKEN(p)->type == TOK_COMMA); - - EXPECT_CURR_TOKEN(p, TOK_RBRAK, MSPH_TREE_TPDEF, goto err); - } EXPECT_CURR_TOKEN(p, TOK_EQUALS, MSPH_TREE_TPDEF, goto err); EXPECT_READ_NEXT(res, p, MSPH_TREE_TPDEF, goto err); - if ((def->tp = tree_parse_tpexpr(p, TREE(def))) == NULL) + if ((def->tp = tree_parse_tpexpr(p, T(def))) == NULL) goto err; return ((struct msph_tree_dir *)def); err: - free_the_tree(TREE(def)); + free_the_tree(T(def)); return (NULL); } -struct msph_tree_namedecl * -tree_parse_namedecl(struct tree_parse *p, struct msph_tree *parent) -{ - struct msph_tree_namedecl *name; - - EXPECT_CURR_TOKEN(p, TOK_IDENT, MSPH_TREE_NAMEDECL, return (NULL)); - - name = (struct msph_tree_namedecl *)tree_parse_ident_extsize(p, parent, - sizeof(*name)); - if (name == NULL) - return (NULL); - - SPHO_ASSERT(TREE(name)->type == MSPH_TREE_IDENT); - TREE(name)->type |= MSPH_TREE_NAMEDECL; - - return (name); -} - -struct msph_tree_nameref * -tree_parse_nameref(struct tree_parse *p, struct msph_tree *parent) -{ - struct msph_tree_nameref *name; - - EXPECT_CURR_TOKEN(p, TOK_IDENT, MSPH_TREE_NAMEREF, return (NULL)); - - name = (struct msph_tree_nameref *)tree_parse_ident_extsize(p, parent, - sizeof(*name)); - if (name == NULL) - return (NULL); - - SPHO_ASSERT(TREE(name)->type == MSPH_TREE_IDENT); - TREE(name)->type |= MSPH_TREE_NAMEREF; - - return (name); -} - struct msph_tree_ident * -tree_parse_ident_extsize(struct tree_parse *p, struct msph_tree *parent, - size_t size) +tree_parse_ident(struct tree_parse *p, struct msph_tree *parent) { struct msph_tree_ident *id; - SPHO_PRECOND(size >= sizeof(struct msph_tree_ident)); EXPECT_CURR_TOKEN(p, TOK_IDENT, MSPH_TREE_IDENT, return (NULL)); - if ((id = malloc(sizeof(size))) == NULL) { + if ((id = malloc(sizeof(*id))) == NULL) { MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - TREE(id)->type = MSPH_TREE_IDENT; - TREE(id)->parent = parent; - TEXT(id)->pos = CURR_TOKEN(p)->pos; - DECOR_INIT(id); + T(id)->type = MSPH_TREE_IDENT; + T(id)->parent = parent; + TXT(id)->pos = CURR_TOKEN(p)->pos; + NOM_DECOR_INIT(&id->dec); if (SPHO_STRLCPY(id->str, CURR_TOKEN(p)->data.str, sizeof(id->str)) >= sizeof(id->str)) { @@ -764,7 +686,7 @@ tree_parse_ident_extsize(struct tree_parse *p, struct msph_tree *parent, return (id); err: - free_the_tree(TREE(id)); + free_the_tree(T(id)); return (NULL); } @@ -793,7 +715,7 @@ tree_parse_tpexpr(struct tree_parse *p, struct msph_tree *parent) tp = tree_parse_forall(p, parent); break; case TOK_IDENT: - tp = tree_parse_tpname_or_tpappl(p, parent); + tp = tree_parse_name(p, parent); break; case TOK_CONST_TRUE: tp = tree_parse_true(p, parent); @@ -812,7 +734,7 @@ tree_parse_tpexpr(struct tree_parse *p, struct msph_tree *parent) tp = NULL; } - SPHO_DEBUG_PRINT("returning tp type=%x\n", TREE(tp)->type); + SPHO_DEBUG_PRINT("returning tp type=%x\n", T(tp)->type); return (tp); } @@ -828,20 +750,20 @@ tree_parse_conj(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - TREE(conj)->type = MSPH_TREE_CONJ; - TREE(conj)->parent = parent; - TEXT(conj)->pos = CURR_TOKEN(p)->pos; - DECOR_INIT(conj); + T(conj)->type = MSPH_TREE_CONJ; + T(conj)->parent = parent; + TXT(conj)->pos = CURR_TOKEN(p)->pos; + TP_DECOR_INIT(&conj->htpe.dec); conj->ltp = NULL; conj->rtp = NULL; EXPECT_READ_NEXT(res, p, MSPH_TREE_CONJ, goto err); - if ((conj->ltp = tree_parse_tpexpr(p, TREE(conj))) + if ((conj->ltp = tree_parse_tpexpr(p, T(conj))) == NULL) goto err; EXPECT_READ_NEXT(res, p, MSPH_TREE_CONJ, goto err); - if ((conj->rtp = tree_parse_tpexpr(p, TREE(conj))) + if ((conj->rtp = tree_parse_tpexpr(p, T(conj))) == NULL) goto err; @@ -864,10 +786,10 @@ tree_parse_disj(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - TREE(disj)->type = MSPH_TREE_DISJ; - TREE(disj)->parent = parent; - TEXT(disj)->pos = CURR_TOKEN(p)->pos; - DECOR_INIT(disj); + T(disj)->type = MSPH_TREE_DISJ; + T(disj)->parent = parent; + TXT(disj)->pos = CURR_TOKEN(p)->pos; + TP_DECOR_INIT(&disj->htpe.dec); disj->ltp = NULL; disj->rtp = NULL; @@ -900,10 +822,10 @@ tree_parse_impl(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - TREE(impl)->type = MSPH_TREE_IMPL; - TREE(impl)->parent = parent; - TEXT(impl)->pos = CURR_TOKEN(p)->pos; - DECOR_INIT(impl); + T(impl)->type = MSPH_TREE_IMPL; + T(impl)->parent = parent; + TXT(impl)->pos = CURR_TOKEN(p)->pos; + TP_DECOR_INIT(&impl->htpe.dec); impl->ltp = NULL; impl->rtp = NULL; @@ -936,10 +858,10 @@ tree_parse_arrow(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - TREE(arrow)->type = MSPH_TREE_ARROW; - TREE(arrow)->parent = parent; - TEXT(arrow)->pos = CURR_TOKEN(p)->pos; - DECOR_INIT(arrow); + T(arrow)->type = MSPH_TREE_ARROW; + T(arrow)->parent = parent; + TXT(arrow)->pos = CURR_TOKEN(p)->pos; + TP_DECOR_INIT(&arrow->htpe.dec); arrow->ltp = NULL; arrow->rtp = NULL; @@ -972,19 +894,19 @@ tree_parse_box(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - TREE(box)->type = MSPH_TREE_BOX; - TREE(box)->parent = parent; - TEXT(box)->pos = CURR_TOKEN(p)->pos; - DECOR_INIT(box); + T(box)->type = MSPH_TREE_BOX; + T(box)->parent = parent; + TXT(box)->pos = CURR_TOKEN(p)->pos; + TP_DECOR_INIT(&box->htpe.dec); box->inner = NULL; EXPECT_READ_NEXT(res, p, MSPH_TREE_BOX, goto err); - if ((box->inner = tree_parse_tpexpr(p, TREE(box))) == NULL) + if ((box->inner = tree_parse_tpexpr(p, T(box))) == NULL) goto err; return ((struct msph_tree_tpexpr *)box); err: - free_the_tree(TREE(box)); + free_the_tree(T(box)); return (NULL); } @@ -1000,50 +922,51 @@ tree_parse_forall(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - TREE(fa)->type = MSPH_TREE_FORALL; - TREE(fa)->parent = parent; - TEXT(fa)->pos = CURR_TOKEN(p)->pos; - DECOR_INIT(fa); - fa->name = NULL; + T(fa)->type = MSPH_TREE_FORALL; + T(fa)->parent = parent; + TXT(fa)->pos = CURR_TOKEN(p)->pos; + TP_DECOR_INIT(&fa->htpe.dec); + SCOPE_DECOR_INIT(&fa->dec); + fa->id = NULL; fa->inner = NULL; EXPECT_READ_NEXT(res, p, MSPH_TREE_FORALL, goto err); - if ((fa->name = tree_parse_namedecl(p, TREE(fa))) == NULL) + if ((fa->id = tree_parse_ident(p, T(fa))) == NULL) goto err; EXPECT_READ_NEXT(res, p, MSPH_TREE_FORALL, goto err); EXPECT_CURR_TOKEN(p, TOK_DOT, MSPH_TREE_FORALL, goto err); EXPECT_READ_NEXT(res, p, MSPH_TREE_FORALL, goto err); - if ((fa->inner = tree_parse_tpexpr(p, TREE(fa))) == NULL) + if ((fa->inner = tree_parse_tpexpr(p, T(fa))) == NULL) goto err; return ((struct msph_tree_tpexpr *)fa); err: - free_the_tree(TREE(fa)); + free_the_tree(T(fa)); return (NULL); } /* parse name or appl */ struct msph_tree_tpexpr * -tree_parse_tpname_or_tpappl(struct tree_parse *p, struct msph_tree *parent) +tree_parse_name(struct tree_parse *p, struct msph_tree *parent) { int res; - struct msph_tree_tpname *tpname; + struct msph_tree_ident *id; + struct msph_tree_name *name; struct msph_tree_tpexpr *ret; - struct msph_tree_nameref *nameref; struct msph_token *tok; ret = NULL; - nameref = NULL; + name = NULL; - if ((nameref = tree_parse_nameref(p, NULL)) == NULL) + if ((id = tree_parse_ident(p, NULL)) == NULL) return (NULL); + SPHO_DEBUG_PRINT("parsed ident=%s\n", id->str); if ((res = tree_parse_next_token(p)) == 1) { if (CURR_TOKEN(p)->type == TOK_LBRAK) { - if ((ret = tree_parse_tpapplargs(p, nameref, parent)) - == NULL) + if ((ret = tree_parse_applargs(p, id, parent)) == NULL) goto err; return (ret); } @@ -1057,21 +980,22 @@ tree_parse_tpname_or_tpappl(struct tree_parse *p, struct msph_tree *parent) goto err; } - if ((tpname = malloc(sizeof(*tpname))) == NULL) { + SPHO_DEBUG_PRINT("ident is name\n"); + if ((name = malloc(sizeof(*name))) == NULL) { MSPH_ERR(CTX(p), MSPH_ERR_SYS); goto err; } - TREE(tpname)->type = MSPH_TREE_TPNAME; - TREE(tpname)->parent = parent; + T(name)->type = MSPH_TREE_NAME; + T(name)->parent = parent; - TEXT(tpname)->pos = TEXT(nameref)->pos; - DECOR_INIT(tpname); - TREE(nameref)->parent = TREE(tpname); - tpname->name = nameref; + TXT(name)->pos = TXT(id)->pos; + TP_DECOR_INIT(&name->htpe.dec); + T(id)->parent = T(name); + name->id = id; - return ((struct msph_tree_tpexpr *)tpname); + return ((struct msph_tree_tpexpr *)name); err: - free_the_tree(TREE(nameref)); + free_the_tree(T(id)); return (NULL); } @@ -1086,26 +1010,26 @@ err: * @return tpexpr node representing A[...]. */ struct msph_tree_tpexpr * -tree_parse_tpapplargs(struct tree_parse *p, struct msph_tree_nameref *name, +tree_parse_applargs(struct tree_parse *p, struct msph_tree_ident *id, struct msph_tree *parent) { int res; - struct msph_tree_tpappl *tpappl; + struct msph_tree_appl *appl; struct msph_tree_tpexpr *tp; tp = NULL; - EXPECT_CURR_TOKEN(p, TOK_LBRAK, MSPH_TREE_TPAPPL, return (NULL)); + EXPECT_CURR_TOKEN(p, TOK_LBRAK, MSPH_TREE_APPL, return (NULL)); - if ((tpappl = malloc(sizeof(*tpappl))) == NULL) { + if ((appl = malloc(sizeof(*appl))) == NULL) { MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - TREE(tpappl)->type = MSPH_TREE_TPAPPL; - TREE(tpappl)->parent = parent; - DECOR_INIT(tpappl); - tpappl->name = NULL; - STAILQ_INIT(&tpappl->args); + T(appl)->type = MSPH_TREE_APPL; + T(appl)->parent = parent; + TP_DECOR_INIT(&appl->htpe.dec); + appl->id = NULL; + STAILQ_INIT(&appl->head); /* parse the argument list */ while ((res = tree_parse_next_token(p)) == 1) { @@ -1113,38 +1037,38 @@ tree_parse_tpapplargs(struct tree_parse *p, struct msph_tree_nameref *name, if (CURR_TOKEN(p)->type == TOK_RBRAK) break; - /* if not at start of argument list, check for comma to know if - * we should parse another argument */ + /* if not start of argument list, check for comma and step + * tokenizer */ if (tp != NULL) { - EXPECT_CURR_TOKEN(p, TOK_COMMA, MSPH_TREE_TPAPPL, + EXPECT_CURR_TOKEN(p, TOK_COMMA, MSPH_TREE_APPL, goto err); - EXPECT_READ_NEXT(res, p, MSPH_TREE_TPAPPL, goto err); + EXPECT_READ_NEXT(res, p, MSPH_TREE_APPL, goto err); } - if ((tp = tree_parse_tpexpr(p, TREE(tpappl))) == NULL) + if ((tp = tree_parse_tpexpr(p, T(appl))) == NULL) goto err; - STAILQ_INSERT_TAIL(&tpappl->args, tp, entries); + STAILQ_INSERT_TAIL(&appl->head, tp, entries); } - /* SYS_ERROR set in tree_parse_next_token */ + /* system error */ if (res == -1) goto err; /* did not read final ']' because of EOF */ if (res == 0) { - MSPH_ERR_INFO(CTX(p), MSPH_ERR_TREE_EOF, MSPH_TREE_TPAPPL); + MSPH_ERR_INFO(CTX(p), MSPH_ERR_TREE_EOF, MSPH_TREE_APPL); goto err; } /* finally, appl takes ownership of id */ - TREE(name)->parent = TREE(tpappl); - tpappl->name = name; - TEXT(tpappl)->pos = TEXT(name)->pos; + T(id)->parent = T(appl); + appl->id = id; + TXT(appl)->pos = TXT(id)->pos; - return ((struct msph_tree_tpexpr *)tpappl); + return ((struct msph_tree_tpexpr *)appl); err: - free_the_tree(TREE(tpappl)); + free_the_tree(T(appl)); return (NULL); } @@ -1160,10 +1084,10 @@ tree_parse_true(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - TREE(t)->type = MSPH_TREE_TRUE; - TREE(t)->parent = parent; - TEXT(t)->pos = CURR_TOKEN(p)->pos; - DECOR_INIT(t); + T(t)->type = MSPH_TREE_TRUE; + T(t)->parent = parent; + TXT(t)->pos = CURR_TOKEN(p)->pos; + TP_DECOR_INIT(&t->htpe.dec); return ((struct msph_tree_tpexpr *)t); } @@ -1179,10 +1103,10 @@ tree_parse_false(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - TREE(f)->type = MSPH_TREE_FALSE; - TREE(f)->parent = parent; - TEXT(f)->pos = CURR_TOKEN(p)->pos; - DECOR_INIT(f); + T(f)->type = MSPH_TREE_FALSE; + T(f)->parent = parent; + TXT(f)->pos = CURR_TOKEN(p)->pos; + TP_DECOR_INIT(&f->htpe.dec); return ((struct msph_tree_tpexpr *)f); } @@ -1199,15 +1123,15 @@ tree_parse_paren(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - TREE(par)->type = MSPH_TREE_PAREN; - TREE(par)->parent = parent; - TEXT(par)->pos = CURR_TOKEN(p)->pos; - DECOR_INIT(par); + T(par)->type = MSPH_TREE_PAREN; + T(par)->parent = parent; + TXT(par)->pos = CURR_TOKEN(p)->pos; + TP_DECOR_INIT(&par->htpe.dec); par->inner = NULL; EXPECT_READ_NEXT(res, p, MSPH_TREE_PAREN, goto err); - if ((par->inner = tree_parse_tpexpr(p, TREE(par))) == NULL) + if ((par->inner = tree_parse_tpexpr(p, T(par))) == NULL) goto err; EXPECT_READ_NEXT(res, p, MSPH_TREE_PAREN, goto err); @@ -1215,7 +1139,7 @@ tree_parse_paren(struct tree_parse *p, struct msph_tree *parent) return ((struct msph_tree_tpexpr *)par); err: - free_the_tree(TREE(par)); + free_the_tree(T(par)); return (NULL); } @@ -1232,13 +1156,14 @@ tree_parse_trait(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - TREE(trait)->type = MSPH_TREE_TRAIT; - TREE(trait)->parent = parent; - TEXT(trait)->pos = CURR_TOKEN(p)->pos; - DECOR_INIT(trait); + T(trait)->type = MSPH_TREE_TRAIT; + T(trait)->parent = parent; + TXT(trait)->pos = CURR_TOKEN(p)->pos; + TP_DECOR_INIT(&trait->htpe.dec); + SCOPE_DECOR_INIT(&trait->dec); trait->body = NULL; - if ((trait->body = tree_parse_body(p, TREE(trait))) == NULL) + if ((trait->body = tree_parse_body(p, T(trait))) == NULL) goto err; EXPECT_READ_NEXT(res, p, MSPH_TREE_TRAIT, goto err); @@ -1246,7 +1171,7 @@ tree_parse_trait(struct tree_parse *p, struct msph_tree *parent) return ((struct msph_tree_tpexpr *)trait); err: - free_the_tree(TREE(trait)); + free_the_tree(T(trait)); return (NULL); } @@ -1255,30 +1180,27 @@ struct msph_tree_dir * tree_parse_nomindecl(struct tree_parse *p, struct msph_tree *parent) { int res; - struct msph_tree_namedecl *name; - struct msph_tree_nomindecl *nomind; + struct msph_tree_nomindecl *nomd; EXPECT_CURR_TOKEN(p, TOK_KW_NOMINAL, MSPH_TREE_NOMINDECL, return (NULL)); - if ((nomind = malloc(sizeof(*nomind))) == NULL) { + if ((nomd = malloc(sizeof(*nomd))) == NULL) { MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - TREE(nomind)->type = MSPH_TREE_NOMINDECL; - TREE(nomind)->parent = parent; - TEXT(nomind)->pos = CURR_TOKEN(p)->pos; - nomind->name = NULL; + T(nomd)->type = MSPH_TREE_NOMINDECL; + T(nomd)->parent = parent; + TXT(nomd)->pos = CURR_TOKEN(p)->pos; + nomd->id = NULL; EXPECT_READ_NEXT(res, p, MSPH_TREE_NOMINDECL, goto err); - if ((name = tree_parse_namedecl(p, TREE(nomind))) == NULL) + if ((nomd->id = tree_parse_ident(p, T(nomd))) == NULL) goto err; - nomind->name = name; - - return ((struct msph_tree_dir *)nomind); + return ((struct msph_tree_dir *)nomd); err: - free_the_tree(TREE(nomind)); + free_the_tree(T(nomd)); return (NULL); } @@ -1296,14 +1218,14 @@ tree_parse_membdecl(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - TREE(membd)->type = MSPH_TREE_MEMBDECL; - TREE(membd)->parent = parent; - TEXT(membd)->pos = CURR_TOKEN(p)->pos; - membd->name = NULL; + T(membd)->type = MSPH_TREE_MEMBDECL; + T(membd)->parent = parent; + TXT(membd)->pos = CURR_TOKEN(p)->pos; + membd->id = NULL; membd->tp = NULL; EXPECT_READ_NEXT(res, p, MSPH_TREE_MEMBDECL, goto err); - if ((membd->name = tree_parse_namedecl(p, TREE(membd))) == NULL) + if ((membd->id = tree_parse_ident(p, T(membd))) == NULL) goto err; EXPECT_READ_NEXT(res, p, MSPH_TREE_MEMBDECL, goto err); @@ -1311,12 +1233,12 @@ tree_parse_membdecl(struct tree_parse *p, struct msph_tree *parent) goto err); EXPECT_READ_NEXT(res, p, MSPH_TREE_MEMBDECL, goto err); - if ((membd->tp = tree_parse_tpexpr(p, TREE(membd))) == NULL) + if ((membd->tp = tree_parse_tpexpr(p, T(membd))) == NULL) goto err; return ((struct msph_tree_dir *)membd); err: - free_the_tree(TREE(membd)); + free_the_tree(T(membd)); return (NULL); } @@ -1334,14 +1256,14 @@ tree_parse_assert(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - TREE(ass)->type = MSPH_TREE_ASSERT; - TREE(ass)->parent = parent; - TEXT(ass)->pos = CURR_TOKEN(p)->pos; + T(ass)->type = MSPH_TREE_ASSERT; + T(ass)->parent = parent; + TXT(ass)->pos = CURR_TOKEN(p)->pos; ass->ltp = NULL; ass->rtp = NULL; EXPECT_READ_NEXT(res, p, MSPH_TREE_ASSERT, goto err); - if ((ass->ltp = tree_parse_tpexpr(p, TREE(ass))) == NULL) + if ((ass->ltp = tree_parse_tpexpr(p, T(ass))) == NULL) goto err; EXPECT_READ_NEXT(res, p, MSPH_TREE_ASSERT, goto err); @@ -1349,12 +1271,12 @@ tree_parse_assert(struct tree_parse *p, struct msph_tree *parent) goto err); EXPECT_READ_NEXT(res, p, MSPH_TREE_ASSERT, goto err); - if ((ass->rtp = tree_parse_tpexpr(p, TREE(ass))) == NULL) + if ((ass->rtp = tree_parse_tpexpr(p, T(ass))) == NULL) goto err; return ((struct msph_tree_dir *)ass); err: - free_the_tree(TREE(ass)); + free_the_tree(T(ass)); return (NULL); } diff --git a/src/spho/bind.c b/src/spho/bind.c deleted file mode 100644 index fc2258b..0000000 --- a/src/spho/bind.c +++ /dev/null @@ -1,165 +0,0 @@ -#include -#include - -#include "spho/spho.h" -#include "spho/scope.h" -#include "spho/bind.h" - -struct spho_prebind * -spho_prebind_create(struct spho_scope *sc) -{ - size_t i; - struct spho_nom *nom; - struct spho_prebind *bind; - - SPHO_PRECOND(sc != NULL); - - if ((bind = calloc(1, sizeof(*bind))) == NULL) { - SPHO_ERR(sc->ctx, SPHO_ERR_SYS); - return (NULL); - } - - if ((bind->binds = calloc(sc->n_noms, sizeof(*bind->binds))) == NULL) { - SPHO_ERR(sc->ctx, SPHO_ERR_SYS); - free(bind); - return (NULL); - } - - bind->sc = sc; - bind->sz = sc->n_noms; - - - i = 0; - SLIST_FOREACH(nom, &sc->noms, next) { - SPHO_ASSERT(i < bind->sz); - bind->binds[i++] = (struct spho_prebind_pair) { NULL, 0, NULL }; - } - - return (bind); -} - -int -spho_prebind_undef(struct spho_prebind *bind, - const struct spho_nom *nom) -{ - size_t i; - SPHO_PRECOND(bind != NULL); - SPHO_PRECOND(nom != NULL); - - for (i = 0; i < bind->sz; i++) { - if (nom == bind->binds[i].nom) { - if (bind->binds[i].kind != SPHO_BIND_UNDECLARED) { - SPHO_ERR(bind->sc->ctx, SPHO_ERR_BIND_DUPL); - return (-1); - } - bind->binds[i].kind = SPHO_BIND_UNDEFINED; - } - } - - return (0); -} -int -spho_prebind_tp(struct spho_prebind *bind, const struct spho_nom *nom, - const struct spho_tp *tp) -{ - size_t i; - - SPHO_PRECOND(bind != NULL); - SPHO_PRECOND(nom != NULL); - SPHO_PRECOND(tp != NULL); - - for (i = 0; i < bind->sz; i++) { - if (nom == bind->binds[i].nom) { - if (bind->binds[i].kind != SPHO_BIND_UNDECLARED) { - SPHO_ERR(bind->sc->ctx, SPHO_ERR_BIND_DUPL); - return (-1); - } - bind->binds[i].kind = SPHO_BIND_TP; - bind->binds[i].val = (union spho_prebind_val) tp; - return (0); - } - } - - SPHO_ERR(bind->sc->ctx, SPHO_ERR_BIND_NOTFOUND); - return (-1); -} - -int -spho_prebind_tp_op(struct spho_prebind *bind, const struct spho_nom *nom, - const struct spho_tp_op *op) -{ - size_t i; - - SPHO_PRECOND(bind != NULL); - SPHO_PRECOND(nom != NULL); - SPHO_PRECOND(op != NULL); - - for (i = 0; i < bind->sz; i++) { - if (nom == bind->binds[i].nom) { - if (bind->binds[i].kind != SPHO_BIND_UNDECLARED) { - SPHO_ERR(bind->sc->ctx, SPHO_ERR_BIND_DUPL); - return (-1); - } - bind->binds[i].kind = SPHO_BIND_TP_OP; - bind->binds[i].val = (union spho_prebind_val) op; - return (0); - } - } - - SPHO_ERR(bind->sc->ctx, SPHO_ERR_BIND_NOTFOUND); - return (-1); -} - -int -spho_prebind_member_tp(struct spho_prebind *bind, const struct spho_nom *nom, - const struct spho_tp *memb_tp) -{ - size_t i; - - SPHO_PRECOND(bind != NULL); - SPHO_PRECOND(nom != NULL); - SPHO_PRECOND(memb_tp != NULL); - - for (i = 0; i < bind->sz; i++) { - if (nom == bind->binds[i].nom) { - if (bind->binds[i].kind != SPHO_BIND_UNDECLARED) { - SPHO_ERR(bind->sc->ctx, SPHO_ERR_BIND_DUPL); - return (-1); - } - bind->binds[i].kind = SPHO_BIND_MEMB_TP; - bind->binds[i].val = (union spho_prebind_val) memb_tp; - return (0); - } - } - - SPHO_ERR(bind->sc->ctx, SPHO_ERR_BIND_NOTFOUND); - return (-1); -} - -struct spho_prebind * -spho_prebind_dupl(const struct spho_prebind *bind) -{ - struct spho_prebind *cp; - - if ((cp = calloc(1, sizeof(*cp))) == NULL) { - SPHO_ERR(bind->sc->ctx, SPHO_ERR_SYS); - return (NULL); - } - - if ((cp->binds = calloc(bind->sz, sizeof(*cp->binds))) == NULL) { - SPHO_ERR(bind->sc->ctx, SPHO_ERR_SYS); - free(cp); - return (NULL); - } - - memcpy(cp->binds, bind->binds, bind->sz * sizeof(*bind->binds)); - - return (cp); -} - -void -spho_prebind_free(struct spho_prebind *bind) -{ - free(bind->binds); - free(bind); -} diff --git a/src/spho/ctx.c b/src/spho/ctx.c index cd43288..fbb0e9d 100644 --- a/src/spho/ctx.c +++ b/src/spho/ctx.c @@ -4,7 +4,7 @@ #include #include -#include "spho/spho.h" +#include "spho/ctx.h" static const char *spho_ctx_sys_strerror(struct spho_ctx *); static const char *spho_ctx_intern_strerror(struct spho_ctx *); @@ -23,10 +23,6 @@ struct spho_err spho_errmsgs[] = { { SPHO_ERR_NOM_INUSE, "name already declared in current scope" }, { SPHO_ERR_NOM_NOTINSCOPE, "name not in scope" }, - - { SPHO_ERR_BIND_NOTFOUND, "binding name not found in scope" }, - { SPHO_ERR_BIND_DUPL, "duplicate binding" }, - { -1, NULL } }; @@ -95,7 +91,7 @@ spho_ctx_sys_strerror(struct spho_ctx *ctx) res = snprintf(ctx->errbuf, sizeof(ctx->errbuf), "spho_syserr: %s (%d) (%s:%d)", strerror(ctx->err_info), ctx->err_info, ctx->filebuf, ctx->errline); - if (res >= (ssize_t)sizeof(ctx->errbuf)) + if (res >= sizeof(ctx->errbuf)) ctx->errbuf[sizeof(ctx->errbuf) - 1] = '\0'; #else res = snprintf(ctx->errbuf, sizeof(ctx->errbuf), diff --git a/src/spho/scope.c b/src/spho/scope.c index da5c679..442834c 100644 --- a/src/spho/scope.c +++ b/src/spho/scope.c @@ -3,32 +3,25 @@ #include #include -#include "spho/spho.h" #include "spho/ctx.h" #include "spho/scope.h" -#include "spho/bind.h" +#include "spho/util.h" static void spho_nom_term(struct spho_nom *); -static int scope_nom_lookup_str_local(struct spho_scope *, const char *, - size_t, struct spho_nom **); -static int scope_nom_in_local(struct spho_scope *, struct spho_nom *); +static int spho_scope_nom_get_norec(struct spho_scope *, const char *, size_t , + struct spho_nom **); int spho_scope_init(struct spho_scope *sc, struct spho_ctx *ctx, struct spho_scope *p) { - sc->ctx = ctx; - sc->parent = p; - SLIST_INIT(&sc->subs); - SLIST_INIT(&sc->noms); - sc->n_noms = 0; - TAILQ_INIT(&sc->tps); - sc->bind_loc = NULL; + sc->ctx = ctx; + sc->parent = p; return (0); } @@ -41,10 +34,6 @@ spho_scope_term(struct spho_scope *sc) SPHO_UTIL_SLIST_DESTROY(&sc->noms, spho_nom, next, spho_nom_term); sc->parent = NULL; - - if (sc->bind_loc == NULL) - spho_prebind_free(sc->bind_loc); - sc->bind_loc = NULL; } struct spho_scope * @@ -78,7 +67,7 @@ spho_scope_create(struct spho_scope *sc) static void -spho_nom_term(__attribute__((unused)) struct spho_nom *nom) +spho_nom_term(struct spho_nom *nom) { return; } @@ -98,12 +87,16 @@ spho_scope_destroy(struct spho_scope *sc) struct spho_nom * spho_scope_nom_add(struct spho_scope *sc, const char *nomstr, size_t sz) { +#ifdef SPHO_USE_STRLCPY size_t res; +#else + ssize_t res; +#endif struct spho_nom *nom; nom = NULL; - if (scope_nom_lookup_str_local(sc, nomstr, sz, &nom) == -1) + if (spho_scope_nom_get_norec(sc, nomstr, sz, &nom) == -1) return (NULL); if (nom != NULL) { @@ -116,14 +109,25 @@ spho_scope_nom_add(struct spho_scope *sc, const char *nomstr, size_t sz) return (NULL); } +#ifdef SPHO_USE_STRLCPY res = strlcpy(nom->s, nomstr, sizeof(nom->s)); if (res >= sizeof(nom->s)) { SPHO_SC_ERR(sc, SPHO_ERR_TOOBIG); goto err; } +#else + res = snprintf(nom->s, sizeof(nom->s), "%s", nomstr); + if (res < 0) { + SPHO_SC_ERR(sc, SPHO_ERR_SYS); + goto err; + } + if (res >= (ssize_t)sizeof(nom->s)) { + SPHO_SC_ERR(sc, SPHO_ERR_TOOBIG); + goto err; + } +#endif SLIST_INSERT_HEAD(&sc->noms, nom, next); - sc->n_noms++; return (nom); err: @@ -133,7 +137,7 @@ err: int -spho_scope_nom_lookup_str(struct spho_scope *sc, const char *nomstr, size_t sz, +spho_scope_nom_get(struct spho_scope *sc, const char *nomstr, size_t sz, struct spho_nom **out) { struct spho_nom *nom; @@ -160,10 +164,12 @@ spho_scope_nom_lookup_str(struct spho_scope *sc, const char *nomstr, size_t sz, } int -spho_scope_nom_lookup_str_strict(struct spho_scope *sc, const char *nomstr, - size_t sz, struct spho_nom **out) +spho_scope_nom_lookup(struct spho_scope *sc, const char *nomstr, size_t sz, + struct spho_nom **out) { - if (spho_scope_nom_lookup_str(sc, nomstr, sz, out) == -1) + int ret; + + if (spho_scope_nom_get(sc, nomstr, sz, out) == -1) return (-1); if (*out == NULL) { @@ -173,56 +179,9 @@ spho_scope_nom_lookup_str_strict(struct spho_scope *sc, const char *nomstr, return (0); } - -int -spho_scope_prebind_init(struct spho_scope *sc) -{ - if ((sc->bind_loc = spho_prebind_create(sc)) - == NULL) { - return (-1); - } - - return (0); -} - -int -spho_scope_prebind_tp(struct spho_scope *sc, struct spho_nom *nom, - struct spho_tp *tp) -{ - if (! scope_nom_in_local(sc, nom)) { - SPHO_ERR(sc->ctx, SPHO_ERR_NOM_NOTINSCOPE); - return (-1); - } - - return (spho_prebind_tp(sc->bind_loc, nom, tp)); -} - -int -spho_scope_prebind_tp_op(struct spho_scope *sc, struct spho_nom *nom, - struct spho_tp_op *tp_op) -{ - if (! scope_nom_in_local(sc, nom)) { - SPHO_ERR(sc->ctx, SPHO_ERR_NOM_NOTINSCOPE); - return (-1); - } - - return (spho_prebind_tp_op(sc->bind_loc, nom, tp_op)); -} - -int -spho_scope_prebind_undef(struct spho_scope *sc, struct spho_nom *nom) -{ - if (! scope_nom_in_local(sc, nom)) { - SPHO_ERR(sc->ctx, SPHO_ERR_NOM_NOTINSCOPE); - return (-1); - } - - return (spho_prebind_undef(sc->bind_loc, nom)); -} - static int -scope_nom_lookup_str_local(struct spho_scope *sc, const char *nomstr, - size_t sz, struct spho_nom **out) +spho_scope_nom_get_norec(struct spho_scope *sc, const char *nomstr, size_t sz, + struct spho_nom **out) { struct spho_nom *nom; @@ -243,16 +202,3 @@ scope_nom_lookup_str_local(struct spho_scope *sc, const char *nomstr, return (0); } - -static int -scope_nom_in_local(struct spho_scope *sc, struct spho_nom *nom) -{ - struct spho_nom *sc_nom; - - SLIST_FOREACH(sc_nom, &sc->noms, next) { - if (sc_nom == nom) - return (1); - } - - return (0); -} diff --git a/src/spho/subt.c b/src/spho/subt.c deleted file mode 100644 index ccc7806..0000000 --- a/src/spho/subt.c +++ /dev/null @@ -1,239 +0,0 @@ -/* - * Subtyping - */ -#include - -#include "spho/bind.h" -#include "spho/bind.h" -#include "spho/spho.h" - -#include "spho/subt.h" - -/* bound type */ -struct bound { - struct spho_bind *bind; - const struct spho_tp *tp; -}; - -/* sequent */ -struct sqnt { - struct spho_ctx *ctx; - - size_t sz; - size_t filled; - struct bound *elms; -}; - -/* sequent turnstile */ -struct tstl { - struct sqnt left; - struct sqnt right; -}; - - -static struct bound *bound_tp(const struct spho_tp *); - - -/* read scopes and create bound type */ -struct bound * -bound_tp(const struct spho_tp *tp) -{ - struct spho_scope *sc; - struct spho_bind *bind, *more_bind; - - struct bound *ret; - - SPHO_PRECOND(tp != NULL); - SPHO_PRECOND(tp->sc != NULL); - SPHO_PRECOND(tp->sc->bind_loc != NULL); - - sc = tp->sc; - bind = NULL; - - if ((ret = calloc(1, sizeof(*ret))) == NULL) { - SPHO_ERR(sc->ctx, SPHO_ERR_SYS); - return (NULL); - } - ret->tp = tp; - - - if ((ret->bind = calloc(1, sizeof(*ret->bind))) == NULL) { - SPHO_ERR(sc->ctx, SPHO_ERR_SYS); - goto err; - } - - /* initialize parent and duplicate scope-local bindings */ - ret->bind->parent = NULL; - if ((ret->bind->loc = spho_prebind_dupl(sc->bind_loc)) == NULL) { - goto err; - } - - /* iterate up through parent scopes and gather their local bindings */ - bind = ret->bind; - while ((sc = sc->parent) != NULL) { - if ((more_bind = calloc(1, sizeof(*more_bind))) == NULL) { - SPHO_ERR(sc->ctx, SPHO_ERR_SYS); - goto err; - } - more_bind->parent = NULL; - if ((more_bind->loc = spho_prebind_dupl(sc->bind_loc)) - == NULL) { - goto err; - } - bind->parent = more_bind; - bind = bind->parent; - } - - return (ret); - -err: - while (ret->bind != NULL) { - bind = ret->bind; - ret->bind = ret->bind->parent; - - spho_prebind_free(bind->loc); - free(bind); - } - - return (NULL); -} - -static int -sqnt_init(struct spho_ctx *ctx, size_t initsz, struct sqnt *seq) -{ - if (initsz == 0) - initsz = 0x10; /* just feels good */ - - seq->ctx = ctx; - - if ((seq->elms = calloc(initsz, sizeof(*seq->elms))) == NULL) { - SPHO_ERR(seq->ctx, SPHO_ERR_SYS); - goto err; - } - - seq->sz = initsz; - seq->filled = 0; - - return (0); -err: - if (seq->elms != NULL) - free(seq->elms); - seq->elms = NULL; - - return (-1); -} - -static int -sqnt_makebig(struct sqnt *seq) -{ - size_t new_sz; - struct bound *new_elms; - - SPHO_PRECOND(seq != NULL); - SPHO_PRECOND(seq->sz > 0); - SPHO_PRECOND(seq->sz <= (SIZE_MAX >> 1)); - SPHO_PRECOND(seq->elms != NULL); - - new_sz = seq->sz << 1; - - if ((new_elms = realloc(seq->elms, new_sz)) == NULL) { - SPHO_ERR(seq->ctx, SPHO_ERR_SYS); - return (-1); - } - - seq->sz = new_sz; - seq->elms = new_elms; - - return (0); -} - -static int -sqnt_add_bound(struct sqnt *seq, struct bound *elm) -{ - SPHO_PRECOND(seq->filled <= seq->sz); - - if (seq->filled >= seq->sz && (sqnt_makebig(seq) == -1)) - return (-1); - - seq->elms[seq->filled++] = *elm; - - SPHO_POSTCOND(seq->filled <= seq->sz); - - return (0); -} - -static int -tstl_init(struct spho_ctx *ctx, size_t lsz, size_t rsz, - struct tstl *ts) -{ - if (sqnt_init(ctx, lsz, &ts->left) == -1) - return (-1); - if (sqnt_init(ctx, rsz, &ts->right) == -1) - return (-1); - - return (0); -} - -static struct tstl * -tstl_alloc(struct spho_ctx *ctx) -{ - struct tstl *ts; - - if ((ts = calloc(1, sizeof(*ts))) == NULL) { - SPHO_ERR(ctx, SPHO_ERR_SYS); - return (NULL); - } - if (tstl_init(ctx, 0, 0, ts) == -1) { - free(ts); - return (NULL); - } - - return (ts); -} - -static int -tstl_add_left(struct tstl *ts, struct bound *tp) -{ - return (sqnt_add_bound(&ts->left, tp)); -} - -static int -tstl_add_right(struct tstl *ts, struct bound *tp) -{ - return (sqnt_add_bound(&ts->right, tp)); -} - -static int -tstl_decide(struct tstl *ts) -{ - SPHO_RIP("implement"); -} - -int -spho_is_subt(struct spho_ctx *ctx, const struct spho_tp *tp_left, - const struct spho_tp *tp_right) -{ - struct tstl ts; - struct bound *left, *right; - - if ((left = bound_tp(tp_left)) == NULL) - return (-1); - if ((right = bound_tp(tp_right)) == NULL) - return (-1); - - // TODO check well-definedness of types (e.g. no undefs) - - if ((tstl_init(ctx, 0, 0, &ts)) == -1) - return (-1); - - if (tstl_add_left(&ts, left) == -1) - return (-1); - if (tstl_add_right(&ts, right) == -1) - return (-1); - - if (tstl_decide(&ts) == -1) - return (-1); - - return (-1); -} - diff --git a/src/spho/tp.c b/src/spho/tp.c index 4140633..6f73d47 100644 --- a/src/spho/tp.c +++ b/src/spho/tp.c @@ -2,13 +2,21 @@ #include -#include "spho/spho.h" +#include "spho/ctx.h" +#include "spho/scope.h" #include "spho/tp.h" const struct tp_konst_data tp_konst_true = { TP_KONST_KEY_TRUE, "True" }; const struct tp_konst_data tp_konst_false = { TP_KONST_KEY_FALSE, "False" }; +//struct spho_tp * +//spho_tp_create_disj(struct spho_ctx *, struct spho_tp *, struct spho_tp *, +// struct spho_tp *) +//{ +// +//} + static struct spho_tp * spho_tp_alloc(struct spho_scope *sc) { @@ -25,22 +33,6 @@ spho_tp_alloc(struct spho_scope *sc) return ((struct spho_tp *)tp_alloc); } -static struct spho_tp_op * -spho_tp_op_alloc(struct spho_scope *sc) -{ - struct spho_tp_alloc *tp_alloc; - - if ((tp_alloc = calloc(1, sizeof(*tp_alloc))) == NULL) { - SPHO_SC_ERR(sc, SPHO_ERR_SYS); - return (NULL); - } - - ((struct spho_tp_op *)tp_alloc)->sc = sc; - TAILQ_INSERT_TAIL(&sc->tps, tp_alloc, allocs); - - return ((struct spho_tp_op *)tp_alloc); -} - static void spho_tp_free(struct spho_tp *tp) { @@ -64,7 +56,7 @@ spho_tp_create_conj(struct spho_scope *sc, struct spho_tp *ltp, if ((tp = spho_tp_alloc(sc)) == NULL) return (NULL); - tp->kind = SPHO_TP_FORM_CONJ; + tp->form = SPHO_TP_FORM_CONJ; tp->d.binop.left = ltp; tp->d.binop.right = rtp; @@ -80,7 +72,7 @@ spho_tp_create_disj(struct spho_scope *sc, struct spho_tp *ltp, if ((tp = spho_tp_alloc(sc)) == NULL) return (NULL); - tp->kind = SPHO_TP_FORM_DISJ; + tp->form = SPHO_TP_FORM_DISJ; tp->d.binop.left = ltp; tp->d.binop.right = rtp; @@ -96,7 +88,7 @@ spho_tp_create_impl(struct spho_scope *sc, struct spho_tp *ltp, if ((tp = spho_tp_alloc(sc)) == NULL) return (NULL); - tp->kind = SPHO_TP_FORM_IMPL; + tp->form = SPHO_TP_FORM_IMPL; tp->d.binop.left = ltp; tp->d.binop.right = rtp; @@ -112,7 +104,7 @@ spho_tp_create_arrow(struct spho_scope *sc, struct spho_tp *ltp, if ((tp = spho_tp_alloc(sc)) == NULL) return (NULL); - tp->kind = SPHO_TP_FORM_ARROW; + tp->form = SPHO_TP_FORM_ARROW; tp->d.binop.left = ltp; tp->d.binop.right = rtp; @@ -127,7 +119,7 @@ spho_tp_create_box(struct spho_scope *sc, struct spho_tp *inner) if ((tp = spho_tp_alloc(sc)) == NULL) return (NULL); - tp->kind = SPHO_TP_FORM_BOX; + tp->form = SPHO_TP_FORM_BOX; tp->d.unop.operand = inner; return (tp); @@ -142,9 +134,9 @@ spho_tp_create_forall(struct spho_scope *sc, struct spho_nom *nom, if ((ret = spho_tp_alloc(sc)) == NULL) return (NULL); - ret->kind = SPHO_TP_FORM_FORALL; - ret->d.fa.nom = nom; - ret->d.fa.tp = tp; + ret->form = SPHO_TP_FORM_FORALL; + ret->d.bind.nom = nom; + ret->d.bind.bound = tp; return (ret); } @@ -157,7 +149,7 @@ spho_tp_create_true(struct spho_scope *sc) if ((ret = spho_tp_alloc(sc)) == NULL) return (NULL); - ret->kind = SPHO_TP_FORM_TRUE; + ret->form = SPHO_TP_FORM_TRUE; ret->d.konst = tp_konst_true; return (ret); @@ -171,7 +163,7 @@ spho_tp_create_false(struct spho_scope *sc) if ((ret = spho_tp_alloc(sc)) == NULL) return (NULL); - ret->kind = SPHO_TP_FORM_FALSE; + ret->form = SPHO_TP_FORM_FALSE; ret->d.konst = tp_konst_false; return (ret); @@ -185,7 +177,7 @@ spho_tp_create_name(struct spho_scope *sc, struct spho_nom *nom) if ((ret = spho_tp_alloc(sc)) == NULL) return (NULL); - ret->kind = SPHO_TP_FORM_NAME; + ret->form = SPHO_TP_FORM_NOM; ret->d.nom.nom = nom; return (ret); @@ -200,7 +192,7 @@ spho_tp_create_appl(struct spho_scope *sc, struct spho_nom *nom, if ((ret = spho_tp_alloc(sc)) == NULL) return (NULL); - ret->kind = SPHO_TP_FORM_APPL; + ret->form = SPHO_TP_FORM_APPL; ret->d.appl.nom = nom; ret->d.appl.args = args; @@ -216,72 +208,23 @@ spho_tp_create_member(struct spho_scope *sc, struct spho_nom *nom, if ((ret = spho_tp_alloc(sc)) == NULL) return (NULL); - ret->kind = SPHO_TP_FORM_MEMBER; - ret->d.memb.nom = nom; - ret->d.memb.tp = tp; + ret->form = SPHO_TP_FORM_MEMBER; + ret->d.bind.nom = nom; + ret->d.bind.bound = tp; return (ret); } -struct spho_tp * -spho_tp_create_nominal(struct spho_scope *sc, struct spho_nom *nom) -{ - struct spho_tp *ret; - - if ((ret = spho_tp_alloc(sc)) == NULL) - return (NULL); - - ret->kind = SPHO_TP_FORM_NOMINAL; - ret->d.nom.nom = nom; - - return (ret); -} - -struct spho_tp * -spho_tp_create_var(struct spho_scope *sc, struct spho_nom *nom) -{ - struct spho_tp *ret; - - if ((ret = spho_tp_alloc(sc)) == NULL) - return (NULL); - - ret->kind = SPHO_TP_FORM_VAR; - ret->d.nom.nom = nom; - - return (ret); -} - - -struct spho_tp_op * -spho_tp_op_create(struct spho_scope *sc, struct spho_scope *op_sc, struct spho_tp *tp) -{ - struct spho_tp_op *op; - - SPHO_PRECOND(sc != NULL); - SPHO_PRECOND(op_sc != NULL); - SPHO_PRECOND(tp != NULL); - - if ((op = spho_tp_op_alloc(sc)) == NULL) - return (NULL); - - op->sc = sc; - op->op_sc = op_sc; - op->op_tp = tp; - - return (op); -} - /* Free type structure. External data (like nom) are freed elsewhere. */ void spho_tp_destroy(struct spho_tp *tp) { struct spho_tp *arg; - switch (tp->kind & SPHO_TP_FORM_MASK) { + switch (tp->form) { case SPHO_TP_FORM_TRUE: case SPHO_TP_FORM_FALSE: - case SPHO_TP_FORM_NAME: - case SPHO_TP_FORM_VAR: + case SPHO_TP_FORM_NOM: break; case SPHO_TP_FORM_CONJ: case SPHO_TP_FORM_DISJ: @@ -294,10 +237,8 @@ spho_tp_destroy(struct spho_tp *tp) spho_tp_destroy(tp->d.unop.operand); break; case SPHO_TP_FORM_FORALL: - spho_tp_destroy(tp->d.fa.tp); - break; case SPHO_TP_FORM_MEMBER: - spho_tp_destroy(tp->d.memb.tp); + spho_tp_destroy(tp->d.bind.bound); break; case SPHO_TP_FORM_APPL: STAILQ_FOREACH(arg, tp->d.appl.args, entries) {