From c18f56f7be09a05776acd164ff96484a7d4d9fe6 Mon Sep 17 00:00:00 2001 From: Ellen Arvidsson Date: Mon, 19 May 2025 12:16:31 +0200 Subject: [PATCH] type fixes and bindings + notes on subtyping --- .clangd | 2 - .gitignore | 21 +- CMakeLists.txt | 19 +- README.md | 37 +- docs/about/contributions.md | 15 + docs/about/cycle.md | 39 +++ docs/about/formalities.md | 398 ++++++++++++++++++++++ docs/about/interpret.md | 88 +++++ example/non-parse/ex6.msph | 21 ++ example/subt/rec-lockstep.msph | 9 + include/msph/decor.h | 33 -- include/msph/sphophi.h | 1 + include/msph/tree.h | 218 ++++++------ include/spho/bind.h | 54 +++ include/spho/err.h | 50 +-- include/spho/scope.h | 83 ++--- include/spho/spho.h | 77 +++++ include/spho/subt.h | 9 + include/spho/tp.h | 25 +- include/spho/util.h | 25 -- src/msph/sphophi.c | 598 +++++++++++++++++++++++---------- src/msph/token.c | 3 + src/msph/tree.c | 566 +++++++++++++++++-------------- src/spho/bind.c | 165 +++++++++ src/spho/ctx.c | 8 +- src/spho/scope.c | 120 +++++-- src/spho/subt.c | 239 +++++++++++++ src/spho/tp.c | 113 +++++-- 28 files changed, 2253 insertions(+), 783 deletions(-) delete mode 100644 .clangd create mode 100644 docs/about/contributions.md create mode 100644 docs/about/cycle.md create mode 100644 docs/about/formalities.md create mode 100644 docs/about/interpret.md create mode 100644 example/non-parse/ex6.msph create mode 100644 example/subt/rec-lockstep.msph delete mode 100644 include/msph/decor.h create mode 100644 include/spho/bind.h create mode 100644 include/spho/subt.h delete mode 100644 include/spho/util.h create mode 100644 src/spho/bind.c create mode 100644 src/spho/subt.c diff --git a/.clangd b/.clangd deleted file mode 100644 index ba4cbb3..0000000 --- a/.clangd +++ /dev/null @@ -1,2 +0,0 @@ -Diagnostics: - UnusedIncludes: None diff --git a/.gitignore b/.gitignore index 75a6986..4929d75 100644 --- a/.gitignore +++ b/.gitignore @@ -51,12 +51,6 @@ Module.symvers Mkfile.old dkms.conf -# CMake build dirs -build-*/ - -# CMake compile commands -compile_commands.json - # vim .*.swp .*.swo @@ -64,3 +58,18 @@ compile_commands.json # 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 8f3758c..81de430 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -6,7 +6,8 @@ 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) @@ -21,17 +22,20 @@ 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}/tp.h ${SPHO_HEADER_DIR}/spho.h + ${SPHO_HEADER_DIR}/subt.h + ${SPHO_HEADER_DIR}/tp.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 ) @@ -53,19 +57,18 @@ 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/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 + ${INCLUDE_DIR}/msph/token.h + ${INCLUDE_DIR}/msph/tree.h ) add_executable(msph ${MSPH_SRC} ${MSPH_HEADER}) diff --git a/README.md b/README.md index 5f66243..2ae6960 100644 --- a/README.md +++ b/README.md @@ -2,25 +2,24 @@ experimental type system implementation -## sappho grammar +## getting and building -``` -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 +```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 ``` +## 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 new file mode 100644 index 0000000..686a257 --- /dev/null +++ b/docs/about/contributions.md @@ -0,0 +1,15 @@ +# 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 new file mode 100644 index 0000000..00822b7 --- /dev/null +++ b/docs/about/cycle.md @@ -0,0 +1,39 @@ +# 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 new file mode 100644 index 0000000..b2b01f1 --- /dev/null +++ b/docs/about/formalities.md @@ -0,0 +1,398 @@ +# 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 new file mode 100644 index 0000000..1e64455 --- /dev/null +++ b/docs/about/interpret.md @@ -0,0 +1,88 @@ +# 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 new file mode 100644 index 0000000..afdeccb --- /dev/null +++ b/example/non-parse/ex6.msph @@ -0,0 +1,21 @@ +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 new file mode 100644 index 0000000..2b74462 --- /dev/null +++ b/example/subt/rec-lockstep.msph @@ -0,0 +1,9 @@ + +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 deleted file mode 100644 index db302d3..0000000 --- a/include/msph/decor.h +++ /dev/null @@ -1,33 +0,0 @@ -#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 052b9bf..65508f1 100644 --- a/include/msph/sphophi.h +++ b/include/msph/sphophi.h @@ -7,6 +7,7 @@ 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 b2e793d..028f329 100644 --- a/include/msph/tree.h +++ b/include/msph/tree.h @@ -5,56 +5,13 @@ #include "msph/common.h" #include "msph/token.h" -#include "msph/decor.h" -/* - * 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) - */ +/* tree decorations */ +struct msph_decor { + struct spho_scope *sc; + struct spho_tp *tp; + struct spho_nom *nom; +}; #define MSPH_TREE_ROOT 0x0000 #define MSPH_TREE_UNIT 0x0001 @@ -70,8 +27,8 @@ #define MSPH_TREE_TPEXPR 0x0040 #define MSPH_TREE_TRUE 0x0041 #define MSPH_TREE_FALSE 0x0042 -#define MSPH_TREE_NAME 0x0043 -#define MSPH_TREE_APPL 0x0044 +#define MSPH_TREE_TPNAME 0x0043 +#define MSPH_TREE_TPAPPL 0x0044 #define MSPH_TREE_TRAIT 0x0045 #define MSPH_TREE_CONJ 0x0046 #define MSPH_TREE_DISJ 0x0047 @@ -82,11 +39,64 @@ #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 { - int type; + unsigned 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; @@ -100,7 +110,7 @@ struct msph_tree_ident; struct msph_tree_tpexpr; struct msph_tree_root { - struct msph_tree htr; + struct msph_tree hd_tr; struct msph_ctx *ctx; @@ -108,155 +118,144 @@ struct msph_tree_root { }; struct msph_tree_unit { - struct msph_tree htr; + struct msph_tree hd_tr; 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 htr; + struct msph_tree hd_tr; STAILQ_HEAD(msph_tree_dir_l, msph_tree_dir) head; }; struct msph_tree_dir { - struct msph_tree_text htxt; + struct msph_tree_text hd_txt; STAILQ_ENTRY(msph_tree_dir) entries; }; struct msph_tree_tpdef { - struct msph_tree_dir hdir; + struct msph_tree_dir hd_dir; - struct msph_tree_ident *id; + struct msph_tree_namedecl *name; + STAILQ_HEAD(msph_tree_namedecl_l, msph_tree_namedecl) params; struct msph_tree_tpexpr *tp; }; struct msph_tree_nomindecl { - struct msph_tree_dir hdir; + struct msph_tree_dir hd_dir; - struct msph_tree_ident *id; + struct msph_tree_namedecl *name; }; struct msph_tree_membdecl { - struct msph_tree_dir hdir; + struct msph_tree_dir hd_dir; - struct msph_tree_ident *id; - struct msph_tree_tpexpr *tp; + struct msph_tree_namedecl *name; + struct msph_tree_tpexpr *tp; }; struct msph_tree_assert { - struct msph_tree_dir hdir; + struct msph_tree_dir hd_dir; struct msph_tree_tpexpr *ltp; struct msph_tree_tpexpr *rtp; }; -struct msph_tree_tpexpr { - struct msph_tree_text htxt; +struct msph_tree_namedecl { + struct msph_tree_ident hd_id; - STAILQ_ENTRY(msph_tree_tpexpr) entries; - - struct msph_tp_decor dec; + STAILQ_ENTRY(msph_tree_namedecl) entries; }; +struct msph_tree_tpexpr { + struct msph_tree_text hd_txt; + + STAILQ_ENTRY(msph_tree_tpexpr) entries; +}; struct msph_tree_true { - struct msph_tree_tpexpr htpe; + struct msph_tree_tpexpr hd_tpe; }; struct msph_tree_false { - struct msph_tree_tpexpr htpe; + struct msph_tree_tpexpr hd_tpe; }; -struct msph_tree_name { - struct msph_tree_tpexpr htpe; - - struct msph_tree_ident *id; +struct msph_tree_nameref { + struct msph_tree_ident hd_id; }; -struct msph_tree_appl { - struct msph_tree_tpexpr htpe; +struct msph_tree_tpname { + struct msph_tree_tpexpr hd_tpe; - struct msph_tree_ident *id; - STAILQ_HEAD(msph_tree_tpexpr_l, msph_tree_tpexpr) head; + 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_trait { - struct msph_tree_tpexpr htpe; + struct msph_tree_tpexpr hd_tpe; struct msph_tree_body *body; - - struct msph_scope_decor dec; }; struct msph_tree_conj { - struct msph_tree_tpexpr htpe; + struct msph_tree_tpexpr hd_tpe; struct msph_tree_tpexpr *ltp; struct msph_tree_tpexpr *rtp; }; struct msph_tree_disj { - struct msph_tree_tpexpr htpe; + struct msph_tree_tpexpr hd_tpe; struct msph_tree_tpexpr *ltp; struct msph_tree_tpexpr *rtp; }; struct msph_tree_impl { - struct msph_tree_tpexpr htpe; + struct msph_tree_tpexpr hd_tpe; struct msph_tree_tpexpr *ltp; struct msph_tree_tpexpr *rtp; }; struct msph_tree_arrow { - struct msph_tree_tpexpr htpe; + struct msph_tree_tpexpr hd_tpe; struct msph_tree_tpexpr *ltp; struct msph_tree_tpexpr *rtp; }; struct msph_tree_box { - struct msph_tree_tpexpr htpe; + struct msph_tree_tpexpr hd_tpe; struct msph_tree_tpexpr *inner; }; struct msph_tree_forall { - struct msph_tree_tpexpr htpe; + struct msph_tree_tpexpr hd_tpe; - struct msph_tree_ident *id; - struct msph_tree_tpexpr *inner; - - struct msph_scope_decor dec; + struct msph_tree_namedecl *name; + struct msph_tree_tpexpr *inner; }; struct msph_tree_paren { - struct msph_tree_tpexpr htpe; + struct msph_tree_tpexpr hd_tpe; 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 *); @@ -264,7 +263,4 @@ 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 new file mode 100644 index 0000000..4e175c3 --- /dev/null +++ b/include/spho/bind.h @@ -0,0 +1,54 @@ +#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 e9bad83..2f56532 100644 --- a/include/spho/err.h +++ b/include/spho/err.h @@ -14,6 +14,8 @@ #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) @@ -41,54 +43,6 @@ (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 843b554..ff682c4 100644 --- a/include/spho/scope.h +++ b/include/spho/scope.h @@ -7,40 +7,18 @@ #define SPHO_NOM_LEN 128 +/* name */ struct spho_nom { char s[SPHO_NOM_LEN]; - SLIST_ENTRY(spho_nom) next; + SLIST_ENTRY(spho_nom) next; // TODO change to allocs }; 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; @@ -51,11 +29,6 @@ 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; }; @@ -70,6 +43,16 @@ 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; @@ -80,22 +63,30 @@ 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 form; + int kind; 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 { @@ -106,24 +97,33 @@ struct spho_tp_ptr { STAILQ_HEAD(spho_tp_ptr_l, spho_tp_ptr); struct spho_tp_alloc { - struct spho_tp tp; + union { + struct spho_tp tp; + struct spho_tp_op tp_op; + } alloc; 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; + 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,9 +140,16 @@ 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_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 **); +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 *); #endif /* _SPHO_SCOPE_H */ diff --git a/include/spho/spho.h b/include/spho/spho.h index f8582dc..e22d7c6 100644 --- a/include/spho/spho.h +++ b/include/spho/spho.h @@ -6,4 +6,81 @@ #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 new file mode 100644 index 0000000..f5a0c22 --- /dev/null +++ b/include/spho/subt.h @@ -0,0 +1,9 @@ +#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 5395d76..c15eb76 100644 --- a/include/spho/tp.h +++ b/include/spho/tp.h @@ -12,20 +12,24 @@ #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_NOM 0x23 +#define SPHO_TP_FORM_NAME 0x23 -#define SPHO_TP_FORM_MEMBER 0x24 +#define SPHO_TP_FORM_VAR 0x40 -// #define SPHO_TP_FORM_SUB 0x96 +#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_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 *, @@ -45,10 +49,11 @@ 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_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 *); +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 *); void spho_tp_destroy(struct spho_tp *); diff --git a/include/spho/util.h b/include/spho/util.h deleted file mode 100644 index 2cb9681..0000000 --- a/include/spho/util.h +++ /dev/null @@ -1,25 +0,0 @@ -#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 8e39263..a9dec26 100644 --- a/src/msph/sphophi.c +++ b/src/msph/sphophi.c @@ -1,5 +1,7 @@ #include +#include "msph/tree.h" +#include "spho/scope.h" #include "spho/spho.h" #include "spho/tp.h" @@ -9,10 +11,20 @@ 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_nom_lookup(struct spho_scope *, +static int msph_tree_sphophi_decor_tpexpr_nom(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, @@ -27,6 +39,10 @@ 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, @@ -37,10 +53,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_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_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_trait(msph_tree_sphophi_f, struct spho_scope *, struct msph_tree_trait *); static int msph_sphophi_foreach_pre_conj(msph_tree_sphophi_f, @@ -57,8 +73,6 @@ 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, @@ -83,10 +97,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_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_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_trait(msph_tree_sphophi_f, struct spho_scope *, struct msph_tree_trait *); static int msph_sphophi_foreach_post_conj(msph_tree_sphophi_f, @@ -103,8 +117,10 @@ 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_ident(msph_tree_sphophi_f, - struct spho_scope *, struct msph_tree_ident *); +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 *); int msph_sphophi_init(struct msph_tree_root *root) { @@ -125,7 +141,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_nom_lookup, + return (msph_sphophi_foreach_pre(msph_tree_sphophi_decor_tpexpr_nom, root)); } @@ -135,6 +151,13 @@ 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; @@ -147,51 +170,47 @@ 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->type) { + switch (TREE_ID(tree)) { case MSPH_TREE_UNIT: - unit = (struct msph_tree_unit *)tree; - if ((unit->dec.sc = spho_scope_create(sc)) == NULL) - ret = -1; - break; 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) + if ((SCOPE(tree) = 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)) { + 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 ((ident->dec.nom = spho_scope_nom_add(sc, ident->str, + if ((NOM(ident) = spho_scope_nom_add(sc, ident->str, sizeof(ident->str))) == NULL) ret = -1; + ADD_FLAG(tree, MSPH_TREE_FLAG_NOM); break; default: break; @@ -201,7 +220,7 @@ msph_tree_sphophi_decor_scope(struct spho_scope *sc, struct msph_tree *tree) } static int -msph_tree_sphophi_decor_nom_lookup(struct spho_scope *sc, +msph_tree_sphophi_decor_tpexpr_nom(struct spho_scope *sc, struct msph_tree *tree) { int ret; @@ -209,16 +228,14 @@ msph_tree_sphophi_decor_nom_lookup(struct spho_scope *sc, ret = 0; - switch (tree->type) { + switch (TREE_ID(tree)) { case MSPH_TREE_IDENT: - if (tree->parent->type != MSPH_TREE_NAME) + if (! IS_TPEXPR(tree->parent)) break; ident = (struct msph_tree_ident *)tree; - if ((ret = spho_scope_nom_lookup(sc, ident->str, - sizeof(ident->str), &ident->dec.nom)) != 0) - break; - if (ident->dec.nom == NULL) - ret = -1; + ret = spho_scope_nom_lookup_str_strict(sc, ident->str, + sizeof(ident->str), &NOM(ident)); + break; default: break; @@ -227,20 +244,17 @@ msph_tree_sphophi_decor_nom_lookup(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, *tpexpr_i; + struct msph_tree_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_name *name; - struct msph_tree_appl *appl; + struct msph_tree_tpname *tpname; + struct msph_tree_tpappl *tpappl; struct msph_tree_box *box; struct msph_tree_forall *forall; struct msph_tree_paren *paren; @@ -260,90 +274,99 @@ msph_tree_sphophi_decor_tp(struct spho_scope *sc, struct msph_tree *tree) if (! (tree->type & MSPH_TREE_TPEXPR)) return (0); - tpexpr = (struct msph_tree_tpexpr *)tree; - - switch (tree->type) { + switch (TREE_ID(tree)) { case MSPH_TREE_CONJ: conj = (struct msph_tree_conj *)tree; - if ((TP(&conj->htpe) = spho_tp_create_conj(sc, TP(conj->ltp), + if ((TP(conj) = 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->htpe) = spho_tp_create_conj(sc, TP(disj->ltp), + if ((TP(disj) = 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->htpe) = spho_tp_create_conj(sc, TP(impl->ltp), + if ((TP(impl) = 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->htpe) = spho_tp_create_conj(sc, TP(arrow->ltp), + if ((TP(arrow) = 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_NAME: - name = (struct msph_tree_name *)tree; - if ((TP(&name->htpe) = spho_tp_create_name(sc, NOM(name->id))) + case MSPH_TREE_TPNAME: + tpname = (struct msph_tree_tpname *)tree; + if ((TP(tpname) = spho_tp_create_name(sc, NOM(tpname->name))) == NULL) goto cleanup; + ADD_FLAG(tpname, MSPH_TREE_FLAG_TP); break; - case MSPH_TREE_APPL: - appl = (struct msph_tree_appl *)tree; + case MSPH_TREE_TPAPPL: + tpappl = (struct msph_tree_tpappl *)tree; if ((tps = malloc(sizeof(*tps))) == NULL) { SPHO_SC_ERR(sc, SPHO_ERR_SYS); goto cleanup; } STAILQ_INIT(tps); - STAILQ_FOREACH(tpexpr_i, &appl->head, entries) { - STAILQ_INSERT_TAIL(tps, tpexpr_i->dec.tp, entries); + STAILQ_FOREACH(tpexpr_i, &tpappl->args, entries) { + STAILQ_INSERT_TAIL(tps, TP(tpexpr_i), entries); } - if ((TP(&appl->htpe) = spho_tp_create_appl(sc, NOM(appl->id), + if ((TP(tpappl) = spho_tp_create_appl(sc, NOM(tpappl->name), tps)) == NULL) goto cleanup; tps = NULL; + ADD_FLAG(tpappl, MSPH_TREE_FLAG_TP); break; case MSPH_TREE_TRUE: - if ((TP(tpexpr) = spho_tp_create_true(sc)) == NULL) + if ((TP(tree) = spho_tp_create_true(sc)) == NULL) goto cleanup; + ADD_FLAG(tree, MSPH_TREE_FLAG_TP); break; case MSPH_TREE_FALSE: - if ((TP(tpexpr) = spho_tp_create_false(sc)) == NULL) + if ((TP(tree) = 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->htpe) = spho_tp_create_forall(sc, - NOM(forall->id), TP(forall->inner))) == NULL) + if ((TP(forall) = spho_tp_create_forall(sc, + NOM(forall->name), 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->htpe) = spho_tp_create_box(sc, TP(box->inner))) + if ((TP(box) = 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->htpe) = TP(paren->inner)) == NULL) + if ((TP(paren) = 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 (T(dir)->type != MSPH_TREE_MEMBDECL) + if (TREE_ID(dir) != 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, membd->id->dec.nom, - membd->tp->dec.tp)) == NULL) + if ((tp_memb = spho_tp_create_member(sc, NOM(membd->name), + TP(membd->tp))) == NULL) goto cleanup; if (tp == NULL) { tp = tp_memb; @@ -352,8 +375,12 @@ 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); @@ -369,6 +396,61 @@ 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) @@ -377,17 +459,14 @@ msph_sphophi_foreach_pre(msph_tree_sphophi_f f, struct msph_tree_root *root) struct spho_scope *sc; struct msph_tree_unit *unit; - if (root == NULL || root->ctx == NULL) - return (-1); - - if (root->ctx->spho == NULL) { - MSPH_ERR(root->ctx, MSPH_ERR_TYPE_INVAL); - return (-1); - } + SPHO_PRECOND(f != NULL); + SPHO_PRECOND(root != NULL); + SPHO_PRECOND(root->ctx != NULL); + SPHO_PRECOND(root->ctx->spho != NULL); sc = spho_scope_global(root->ctx->spho); - if ((ret = f(sc, T(root))) != 0) { + if ((ret = f(sc, TREE(root))) != 0) { goto err; } @@ -409,10 +488,13 @@ msph_sphophi_foreach_pre_unit(msph_tree_sphophi_f f, struct spho_scope *sc, { int ret; - if ((ret = f(sc, T(unit))) != 0) + SPHO_PRECOND(sc != NULL); + SPHO_PRECOND(unit != NULL); + + if ((ret = f(sc, TREE(unit))) != 0) return (ret); - sc = GET_SCOPE(unit); + sc = SCOPE(unit); return (msph_sphophi_foreach_pre_body(f, sc, unit->body)); } @@ -424,7 +506,10 @@ msph_sphophi_foreach_pre_body(msph_tree_sphophi_f f, struct spho_scope *sc, int ret; struct msph_tree_dir *dir; - if ((ret = f(sc, T(body))) != 0) + SPHO_PRECOND(sc != NULL); + SPHO_PRECOND(body != NULL); + + if ((ret = f(sc, TREE(body))) != 0) return (ret); ret = 0; @@ -442,8 +527,11 @@ 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 (dir->htxt.htr.type) { + switch (TREE_ID(dir)) { case MSPH_TREE_TPDEF: ret = msph_sphophi_foreach_pre_tpdef(f, sc, (struct msph_tree_tpdef *)dir); @@ -473,13 +561,26 @@ 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; - if ((ret = f(sc, T(tpdef))) != 0) + SPHO_PRECOND(sc != NULL); + SPHO_PRECOND(tpdef != NULL); + + if ((ret = f(sc, TREE(tpdef))) != 0) return (ret); - if ((ret = msph_sphophi_foreach_pre_ident(f, sc, tpdef->id)) != 0) + if ((ret = msph_sphophi_foreach_pre_namedecl(f, sc, tpdef->name)) != 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)); } @@ -489,10 +590,13 @@ msph_sphophi_foreach_pre_nomindecl(msph_tree_sphophi_f f, struct spho_scope *sc, { int ret; - if ((ret = f(sc, T(nomd))) != 0) + SPHO_PRECOND(sc != NULL); + SPHO_PRECOND(nomd != NULL); + + if ((ret = f(sc, TREE(nomd))) != 0) return (ret); - return (msph_sphophi_foreach_pre_ident(f, sc, nomd->id)); + return (msph_sphophi_foreach_pre_namedecl(f, sc, nomd->name)); } static int @@ -501,10 +605,13 @@ msph_sphophi_foreach_pre_membdecl(msph_tree_sphophi_f f, struct spho_scope *sc, { int ret; - if ((ret = f(sc, T(membd))) != 0) + SPHO_PRECOND(sc != NULL); + SPHO_PRECOND(membd != NULL); + + if ((ret = f(sc, TREE(membd))) != 0) return (ret); - if (msph_sphophi_foreach_pre_ident(f, sc, membd->id) != 0) + if (msph_sphophi_foreach_pre_namedecl(f, sc, membd->name) != 0) return (ret); if (msph_sphophi_foreach_pre_tpexpr(f, sc, membd->tp) != 0) return (ret); @@ -518,7 +625,7 @@ msph_sphophi_foreach_pre_assert(msph_tree_sphophi_f f, struct spho_scope *sc, { int ret; - if ((ret = f(sc, T(ass))) != 0) + if ((ret = f(sc, TREE(ass))) != 0) return (ret); if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, ass->ltp)) != 0) @@ -530,10 +637,23 @@ msph_sphophi_foreach_pre_assert(msph_tree_sphophi_f f, struct spho_scope *sc, } static int -msph_sphophi_foreach_pre_ident(msph_tree_sphophi_f f, struct spho_scope *sc, - struct msph_tree_ident *ident) +msph_sphophi_foreach_pre_namedecl(msph_tree_sphophi_f f, struct spho_scope *sc, + struct msph_tree_namedecl *name) { - return (f(sc, T(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))); } static int @@ -542,9 +662,12 @@ 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 (tpexpr->htxt.htr.type) { + switch (TREE_ID(tpexpr)) { case MSPH_TREE_CONJ: ret = msph_sphophi_foreach_pre_conj(f, sc, (struct msph_tree_conj *)tpexpr); @@ -561,13 +684,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_NAME: - ret = msph_sphophi_foreach_pre_name(f, sc, - (struct msph_tree_name *)tpexpr); + case MSPH_TREE_TPNAME: + ret = msph_sphophi_foreach_pre_tpname(f, sc, + (struct msph_tree_tpname *)tpexpr); break; - case MSPH_TREE_APPL: - ret = msph_sphophi_foreach_pre_appl(f, sc, - (struct msph_tree_appl *)tpexpr); + case MSPH_TREE_TPAPPL: + ret = msph_sphophi_foreach_pre_tpappl(f, sc, + (struct msph_tree_tpappl *)tpexpr); break; case MSPH_TREE_TRAIT: ret = msph_sphophi_foreach_pre_trait(f, sc, @@ -594,7 +717,7 @@ msph_sphophi_foreach_pre_tpexpr(msph_tree_sphophi_f f, struct spho_scope *sc, (struct msph_tree_false *)tpexpr); break; default: - SPHO_ASSERT(0); + SPHO_RIP("default-reach"); break; } @@ -607,7 +730,10 @@ msph_sphophi_foreach_pre_conj(msph_tree_sphophi_f f, struct spho_scope *sc, { int ret; - if ((ret = f(sc, T(conj))) != 0) + SPHO_PRECOND(sc != NULL); + SPHO_PRECOND(conj != NULL); + + if ((ret = f(sc, TREE(conj))) != 0) return (ret); if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, conj->ltp)) != 0) @@ -622,7 +748,10 @@ msph_sphophi_foreach_pre_disj(msph_tree_sphophi_f f, struct spho_scope *sc, { int ret; - if ((ret = f(sc, T(disj))) != 0) + SPHO_PRECOND(sc != NULL); + SPHO_PRECOND(disj != NULL); + + if ((ret = f(sc, TREE(disj))) != 0) return (ret); if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, disj->ltp)) != 0) return (ret); @@ -635,7 +764,10 @@ msph_sphophi_foreach_pre_impl(msph_tree_sphophi_f f, struct spho_scope *sc, { int ret; - if ((ret = f(sc, T(impl))) != 0) + SPHO_PRECOND(sc != NULL); + SPHO_PRECOND(impl != NULL); + + if ((ret = f(sc, TREE(impl))) != 0) return (ret); if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, impl->ltp)) != 0) @@ -649,7 +781,10 @@ msph_sphophi_foreach_pre_arrow(msph_tree_sphophi_f f, struct spho_scope *sc, { int ret; - if ((ret = f(sc, T(arrow))) != 0) + SPHO_PRECOND(sc != NULL); + SPHO_PRECOND(arrow != NULL); + + if ((ret = f(sc, TREE(arrow))) != 0) return (ret); if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, arrow->ltp)) != 0) @@ -658,29 +793,35 @@ msph_sphophi_foreach_pre_arrow(msph_tree_sphophi_f f, struct spho_scope *sc, } static int -msph_sphophi_foreach_pre_name(msph_tree_sphophi_f f, struct spho_scope *sc, - struct msph_tree_name *name) +msph_sphophi_foreach_pre_tpname(msph_tree_sphophi_f f, struct spho_scope *sc, + struct msph_tree_tpname *name) { int ret; - if ((ret = f(sc, T(name))) != 0) + SPHO_PRECOND(sc != NULL); + SPHO_PRECOND(name != NULL); + + if ((ret = f(sc, TREE(name))) != 0) return (ret); - return (msph_sphophi_foreach_pre_ident(f, sc, name->id)); + return (msph_sphophi_foreach_pre_nameref(f, sc, name->name)); } static int -msph_sphophi_foreach_pre_appl(msph_tree_sphophi_f f, struct spho_scope *sc, - struct msph_tree_appl *appl) +msph_sphophi_foreach_pre_tpappl(msph_tree_sphophi_f f, struct spho_scope *sc, + struct msph_tree_tpappl *appl) { int ret; struct msph_tree_tpexpr *tp; - if ((ret = f(sc, T(appl))) != 0) + SPHO_PRECOND(sc != NULL); + SPHO_PRECOND(appl != NULL); + + if ((ret = f(sc, TREE(appl))) != 0) return (ret); ret = 0; - STAILQ_FOREACH(tp, &appl->head, entries) { + STAILQ_FOREACH(tp, &appl->args, entries) { if ((ret = msph_sphophi_foreach_pre_tpexpr(f, sc, tp)) != 0) return (ret); } @@ -693,10 +834,14 @@ msph_sphophi_foreach_pre_trait(msph_tree_sphophi_f f, struct spho_scope *sc, struct msph_tree_trait *trait) { int ret; - if ((ret = f(sc, T(trait))) != 0) + + SPHO_PRECOND(sc != NULL); + SPHO_PRECOND(trait != NULL); + + if ((ret = f(sc, TREE(trait))) != 0) return (ret); - sc = GET_SCOPE(trait); + sc = SCOPE(trait); return (msph_sphophi_foreach_pre_body(f, sc, trait->body)); } @@ -707,7 +852,10 @@ msph_sphophi_foreach_pre_box(msph_tree_sphophi_f f,struct spho_scope *sc, { int ret; - if ((ret = f(sc, T(box))) != 0) + SPHO_PRECOND(sc != NULL); + SPHO_PRECOND(box != NULL); + + if ((ret = f(sc, TREE(box))) != 0) return (ret); return (msph_sphophi_foreach_pre_tpexpr(f, sc, box->inner)); @@ -718,11 +866,14 @@ msph_sphophi_foreach_pre_forall(msph_tree_sphophi_f f, struct spho_scope *sc, struct msph_tree_forall *forall) { int ret; - - if ((ret = f(sc, T(forall))) != 0) + + SPHO_PRECOND(sc != NULL); + SPHO_PRECOND(forall != NULL); + + if ((ret = f(sc, TREE(forall))) != 0) return (ret); - sc = GET_SCOPE(forall); + sc = SCOPE(forall); return (msph_sphophi_foreach_pre_tpexpr(f, sc, forall->inner)); } @@ -733,7 +884,10 @@ msph_sphophi_foreach_pre_paren(msph_tree_sphophi_f f, struct spho_scope *sc, { int ret; - if ((ret = f(sc, T(paren))) != 0) + SPHO_PRECOND(sc != NULL); + SPHO_PRECOND(paren != NULL); + + if ((ret = f(sc, TREE(paren))) != 0) return (ret); return (msph_sphophi_foreach_pre_tpexpr(f, sc, paren->inner)); @@ -743,14 +897,20 @@ static int msph_sphophi_foreach_pre_true(msph_tree_sphophi_f f, struct spho_scope *sc, struct msph_tree_true *tru) { - return (f(sc, T(tru))); + SPHO_PRECOND(sc != NULL); + SPHO_PRECOND(tru != NULL); + + return (f(sc, TREE(tru))); } static int msph_sphophi_foreach_pre_false(msph_tree_sphophi_f f, struct spho_scope *sc, struct msph_tree_false *fls) { - return (f(sc, T(fls))); + SPHO_PRECOND(sc != NULL); + SPHO_PRECOND(fls != NULL); + + return (f(sc, TREE(fls))); } @@ -762,13 +922,10 @@ msph_sphophi_foreach_post(msph_tree_sphophi_f f, struct msph_tree_root *root) struct spho_scope *sc; struct msph_tree_unit *unit; - if (root == NULL || root->ctx == NULL) - return (-1); - - if (root->ctx->spho == NULL) { - MSPH_ERR(root->ctx, MSPH_ERR_TYPE_INVAL); - return (-1); - } + SPHO_PRECOND(f != NULL); + SPHO_PRECOND(root != NULL); + SPHO_PRECOND(root->ctx != NULL); + SPHO_PRECOND(root->ctx->spho != NULL); sc = spho_scope_global(root->ctx->spho); @@ -778,7 +935,7 @@ msph_sphophi_foreach_post(msph_tree_sphophi_f f, struct msph_tree_root *root) goto err; } - if ((ret = f(sc, T(root))) != 0) + if ((ret = f(sc, TREE(root))) != 0) goto err; return (ret); @@ -794,13 +951,17 @@ msph_sphophi_foreach_post_unit(msph_tree_sphophi_f f, struct spho_scope *sc, int ret; struct spho_scope *inner_sc; - inner_sc = GET_SCOPE(unit); + SPHO_PRECOND(sc != NULL); + SPHO_PRECOND(unit != NULL); + + inner_sc = SCOPE(unit); if ((ret = msph_sphophi_foreach_post_body(f, inner_sc, unit->body)) - != 0) + != 0) { return (ret); + } - return (f(sc, T(unit))); + return (f(sc, TREE(unit))); } static int @@ -810,13 +971,16 @@ 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, T(body))); + return (f(sc, TREE(body))); } static int @@ -825,8 +989,11 @@ 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 (dir->htxt.htr.type) { + switch (TREE_ID(dir)) { case MSPH_TREE_TPDEF: ret = msph_sphophi_foreach_post_tpdef(f, sc, (struct msph_tree_tpdef *)dir); @@ -856,13 +1023,32 @@ 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; - if ((ret = msph_sphophi_foreach_post_ident(f, sc, tpdef->id)) != 0) + SPHO_PRECOND(sc != NULL); + SPHO_PRECOND(tpdef != NULL); + + + if ((ret = msph_sphophi_foreach_post_namedecl(f, sc, tpdef->name)) + != 0) { return (ret); - if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, tpdef->tp)) != 0) + } + + 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) return (ret); - return (f(sc, T(tpdef))); + return (f(sc, TREE(tpdef))); } static int @@ -871,10 +1057,13 @@ msph_sphophi_foreach_post_nomindecl(msph_tree_sphophi_f f, { int ret; - if ((ret = msph_sphophi_foreach_post_ident(f, sc, nomd->id)) != 0) + SPHO_PRECOND(sc != NULL); + SPHO_PRECOND(nomd != NULL); + + if ((ret = msph_sphophi_foreach_post_namedecl(f, sc, nomd->name)) != 0) return (ret); - return (f(sc, T(nomd))); + return (f(sc, TREE(nomd))); } static int @@ -883,12 +1072,15 @@ msph_sphophi_foreach_post_membdecl(msph_tree_sphophi_f f, struct spho_scope *sc, { int ret; - if ((ret = msph_sphophi_foreach_post_ident(f, sc, membd->id)) != 0) + SPHO_PRECOND(sc != NULL); + SPHO_PRECOND(membd != NULL); + + if ((ret = msph_sphophi_foreach_post_namedecl(f, sc, membd->name)) != 0) return (ret); if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, membd->tp)) != 0) return (ret); - return (f(sc, T(membd))); + return (f(sc, TREE(membd))); } static int @@ -897,19 +1089,35 @@ 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, T(ass))); + return (f(sc, TREE(ass))); } static int -msph_sphophi_foreach_post_ident(msph_tree_sphophi_f f, struct spho_scope *sc, - struct msph_tree_ident *ident) +msph_sphophi_foreach_post_namedecl(msph_tree_sphophi_f f, struct spho_scope *sc, + struct msph_tree_namedecl *name) { - return (f(sc, T(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))); } static int @@ -918,9 +1126,12 @@ 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 (tpexpr->htxt.htr.type) { + switch (TREE_ID(tpexpr)) { case MSPH_TREE_CONJ: ret = msph_sphophi_foreach_post_conj(f, sc, (struct msph_tree_conj *)tpexpr); @@ -937,13 +1148,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_NAME: - ret = msph_sphophi_foreach_post_name(f, sc, - (struct msph_tree_name *)tpexpr); + case MSPH_TREE_TPNAME: + ret = msph_sphophi_foreach_post_tpname(f, sc, + (struct msph_tree_tpname *)tpexpr); break; - case MSPH_TREE_APPL: - ret = msph_sphophi_foreach_post_appl(f, sc, - (struct msph_tree_appl *)tpexpr); + case MSPH_TREE_TPAPPL: + ret = msph_sphophi_foreach_post_tpappl(f, sc, + (struct msph_tree_tpappl *)tpexpr); break; case MSPH_TREE_TRAIT: ret = msph_sphophi_foreach_post_trait(f, sc, @@ -983,12 +1194,15 @@ 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, T(conj))); + return (f(sc, TREE(conj))); } @@ -998,12 +1212,15 @@ 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, T(disj))); + return (f(sc, TREE(disj))); } static int @@ -1012,12 +1229,15 @@ 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, T(impl))); + return (f(sc, TREE(impl))); } static int @@ -1026,41 +1246,46 @@ 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, T(arrow))); + return (f(sc, TREE(arrow))); } static int -msph_sphophi_foreach_post_name(msph_tree_sphophi_f f, struct spho_scope *sc, - struct msph_tree_name *name) +msph_sphophi_foreach_post_tpname(msph_tree_sphophi_f f, struct spho_scope *sc, + struct msph_tree_tpname *name) { int ret; - if ((ret = msph_sphophi_foreach_post_ident(f, sc, name->id)) != 0) + SPHO_PRECOND(sc != NULL); + SPHO_PRECOND(name != NULL); + + if ((ret = msph_sphophi_foreach_post_nameref(f, sc, name->name)) != 0) return (ret); - return (f(sc, T(name))); - + return (f(sc, TREE(name))); } static int -msph_sphophi_foreach_post_appl(msph_tree_sphophi_f f, struct spho_scope *sc, - struct msph_tree_appl *appl) +msph_sphophi_foreach_post_tpappl(msph_tree_sphophi_f f, struct spho_scope *sc, + struct msph_tree_tpappl *appl) { int ret; struct msph_tree_tpexpr *tp; ret = 0; - STAILQ_FOREACH(tp, &appl->head, entries) { + STAILQ_FOREACH(tp, &appl->args, entries) { if ((ret = msph_sphophi_foreach_post_tpexpr(f, sc, tp)) != 0) return (ret); } - return (f(sc, T(appl))); + return (f(sc, TREE(appl))); } static int @@ -1070,13 +1295,17 @@ msph_sphophi_foreach_post_trait(msph_tree_sphophi_f f, struct spho_scope *sc, int ret; struct spho_scope *inner_sc; - inner_sc = GET_SCOPE(trait); + SPHO_PRECOND(sc != NULL); + SPHO_PRECOND(trait != NULL); + + inner_sc = SCOPE(trait); if ((ret = msph_sphophi_foreach_post_body(f, inner_sc, trait->body)) - != 0) + != 0) { return (ret); + } - return (f(sc, T(trait))); + return (f(sc, TREE(trait))); } static int @@ -1085,10 +1314,13 @@ 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, T(box))); + return (f(sc, TREE(box))); } static int @@ -1098,13 +1330,16 @@ msph_sphophi_foreach_post_forall(msph_tree_sphophi_f f, struct spho_scope *sc, int ret; struct spho_scope *inner_sc; - inner_sc = GET_SCOPE(forall); + SPHO_PRECOND(sc != NULL); + SPHO_PRECOND(forall != NULL); + + inner_sc = SCOPE(forall); if ((ret = msph_sphophi_foreach_post_tpexpr(f, inner_sc, forall->inner)) != 0) return (ret); - return (f(sc, T(forall))); + return (f(sc, TREE(forall))); } @@ -1114,10 +1349,13 @@ 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, T(paren))); + return (f(sc, TREE(paren))); } @@ -1125,12 +1363,18 @@ static int msph_sphophi_foreach_post_true(msph_tree_sphophi_f f, struct spho_scope *sc, struct msph_tree_true *tru) { - return (f(sc, T(tru))); + SPHO_PRECOND(sc != NULL); + SPHO_PRECOND(tru != NULL); + + return (f(sc, TREE(tru))); } static int msph_sphophi_foreach_post_false(msph_tree_sphophi_f f, struct spho_scope *sc, struct msph_tree_false *fls) { - return (f(sc, T(fls))); + SPHO_PRECOND(sc != NULL); + SPHO_PRECOND(fls != NULL); + + return (f(sc, TREE(fls))); } diff --git a/src/msph/token.c b/src/msph/token.c index 1c0adb2..e83a11d 100644 --- a/src/msph/token.c +++ b/src/msph/token.c @@ -5,9 +5,12 @@ #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 440fc53..199628c 100644 --- a/src/msph/tree.c +++ b/src/msph/tree.c @@ -6,7 +6,7 @@ #include #include -#include "spho/util.h" +#include "spho/spho.h" #include "msph/tree.h" @@ -26,7 +26,8 @@ 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 *); @@ -36,8 +37,13 @@ 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(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_dir *tree_parse_tpdef(struct tree_parse *, struct msph_tree *); @@ -50,16 +56,18 @@ 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_name(struct tree_parse *, +static struct msph_tree_tpexpr *tree_parse_tpname_or_tpappl( + struct tree_parse *, struct msph_tree *); -static struct msph_tree_tpexpr *tree_parse_applargs(struct tree_parse *, - struct msph_tree_ident*, +static struct msph_tree_tpexpr *tree_parse_tpapplargs(struct tree_parse *, + struct msph_tree_nameref*, struct msph_tree *); static struct msph_tree_tpexpr *tree_parse_trait(struct tree_parse *, struct msph_tree *); @@ -87,8 +95,8 @@ msph_tree_makeroot(struct msph_ctx *ctx) MSPH_ERR(ctx, MSPH_ERR_SYS); return (NULL); } - T(root)->type = MSPH_TREE_ROOT; - T(root)->parent = NULL; + TREE(root)->type = MSPH_TREE_ROOT; + TREE(root)->parent = NULL; root->ctx = ctx; @@ -138,14 +146,14 @@ msph_tree_parse(struct msph_token_stream *s, struct msph_tree_root *root) struct tree_parse p; struct msph_tree_unit *unit; - if (T(root)->type != MSPH_TREE_ROOT) { + if (TREE(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, T(root))) == NULL) + if ((unit = tree_parse_unit(&p, TREE(root))) == NULL) return (-1); STAILQ_INSERT_TAIL(&root->head, unit, entries); @@ -162,7 +170,7 @@ msph_tree_fprint(FILE *f, struct msph_tree *tree) { __attribute__((format(printf, 3, 4))) static ssize_t -ind_fprintf(FILE *f, int indent, const char *fmt, ...) +indent_fprintf(FILE *f, int indent, const char *fmt, ...) { int res; ssize_t ret; @@ -208,284 +216,298 @@ 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_appl *appl; + struct msph_tree_tpappl *tpappl; struct msph_tree_trait *trait; - struct msph_tree_name *name; + struct msph_tree_tpname *name; struct msph_tree_paren *paren; struct msph_tree_ident *ident; struct msph_tree_tpexpr *tp; ret = 0; - switch (tree->type) { + switch (TREE_ID(tree)) { case MSPH_TREE_ROOT: root = (struct msph_tree_root *)tree; - if ((res = ind_fprintf(f, indent, "(root\n")) < 0) + if ((res = indent_fprintf(f, indent, "(root\n")) < 0) return (res); STAILQ_FOREACH(unit, &root->head, entries) { - if ((res = tree_ind_fprint(f, indent+1, T(unit))) + if ((res = tree_ind_fprint(f, indent+1, TREE(unit))) < 0) return (res); ret += res; } - if ((res = ind_fprintf(f, indent, ")\n")) < 0) + if ((res = indent_fprintf(f, indent, ")\n")) < 0) return (res); break; case MSPH_TREE_UNIT: unit = (struct msph_tree_unit *)tree; - if ((res = ind_fprintf(f, indent, "(unit:%s\n", unit->name)) + if ((res = indent_fprintf(f, indent, "(unit:%s\n", unit->name)) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, T(unit->body))) < 0) + if ((res = tree_ind_fprint(f, indent+1, TREE(unit->body))) < 0) return (res); ret += res; - if ((res = ind_fprintf(f, indent, ")\n")) < 0) + if ((res = indent_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; case MSPH_TREE_BODY: body = (struct msph_tree_body *)tree; - if ((res = ind_fprintf(f, indent, "(body\n")) < 0) + if ((res = indent_fprintf(f, indent, "(body\n")) < 0) return (res); ret += res; STAILQ_FOREACH(dir, &body->head, entries) { - if ((res = tree_ind_fprint(f, indent+1, T(dir))) + if ((res = tree_ind_fprint(f, indent+1, TREE(dir))) < 0) return (res); ret += res; } - if ((res = ind_fprintf(f, indent, ")\n")) < 0) + if ((res = indent_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; case MSPH_TREE_NOMINDECL: nomd = (struct msph_tree_nomindecl *)tree; - if ((res = ind_fprintf(f, indent, "(nomindecl:%u,%u\n", - TXT(nomd)->pos.line, TXT(nomd)->pos.col)) < 0) + if ((res = indent_fprintf(f, indent, "(nomindecl:%u,%u\n", + TEXT(nomd)->pos.line, TEXT(nomd)->pos.col)) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, T(nomd->id))) < 0) + if ((res = tree_ind_fprint(f, indent+1, TREE(nomd->name))) < 0) return (res); ret += res; - if ((res = ind_fprintf(f, indent, ")\n")) < 0) + if ((res = indent_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; case MSPH_TREE_ASSERT: ass = (struct msph_tree_assert *)tree; - if ((res = ind_fprintf(f, indent, "(assert:%u,%u\n", - TXT(ass)->pos.line, TXT(ass)->pos.col)) < 0) + if ((res = indent_fprintf(f, indent, "(assert:%u,%u\n", + TEXT(ass)->pos.line, TEXT(ass)->pos.col)) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, T(ass->ltp))) < 0) + if ((res = tree_ind_fprint(f, indent+1, TREE(ass->ltp))) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, T(ass->rtp))) < 0) + if ((res = tree_ind_fprint(f, indent+1, TREE(ass->rtp))) < 0) return (res); ret += res; - if ((res = ind_fprintf(f, indent, ")\n")) < 0) + if ((res = indent_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; case MSPH_TREE_TPDEF: tpdef = (struct msph_tree_tpdef *)tree; - if ((res = ind_fprintf(f, indent, "(tpdef:%u,%u\n", - TXT(tpdef)->pos.line, TXT(tpdef)->pos.col)) < 0) + if ((res = indent_fprintf(f, indent, "(tpdef:%u,%u\n", + TEXT(tpdef)->pos.line, TEXT(tpdef)->pos.col)) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, T(tpdef->id))) < 0) + if ((res = tree_ind_fprint(f, indent+1, TREE(tpdef->name))) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, T(tpdef->tp))) < 0) + if ((res = tree_ind_fprint(f, indent+1, TREE(tpdef->tp))) < 0) return (res); ret += res; - if ((res = ind_fprintf(f, indent, ")\n")) < 0) + if ((res = indent_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; case MSPH_TREE_MEMBDECL: membdecl = (struct msph_tree_membdecl *)tree; - if ((res = ind_fprintf(f, indent, "(membdecl:%u,%u\n", - TXT(membdecl)->pos.line, TXT(membdecl)->pos.col)) < 0) + if ((res = indent_fprintf(f, indent, "(membdecl:%u,%u\n", + TEXT(membdecl)->pos.line, TEXT(membdecl)->pos.col)) < 0) { return (res); + } ret += res; - if ((res = tree_ind_fprint(f, indent+1, T(membdecl->id))) < 0) + if ((res = tree_ind_fprint(f, indent+1, TREE(membdecl->name))) + < 0) { return (res); + } ret += res; - if ((res = tree_ind_fprint(f, indent+1, T(membdecl->tp))) < 0) + if ((res = tree_ind_fprint(f, indent+1, TREE(membdecl->tp))) + < 0) { return (res); + } ret += res; - if ((res = ind_fprintf(f, indent, ")\n")) < 0) + if ((res = indent_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; case MSPH_TREE_CONJ: conj = (struct msph_tree_conj *)tree; - if ((res = ind_fprintf(f, indent, "(conj:%u,%u\n", - TXT(conj)->pos.line, TXT(conj)->pos.col)) < 0) + if ((res = indent_fprintf(f, indent, "(conj:%u,%u\n", + TEXT(conj)->pos.line, TEXT(conj)->pos.col)) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, T(conj->ltp))) < 0) + if ((res = tree_ind_fprint(f, indent+1, TREE(conj->ltp))) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, T(conj->rtp))) < 0) + if ((res = tree_ind_fprint(f, indent+1, TREE(conj->rtp))) < 0) return (res); ret += res; - if ((res = ind_fprintf(f, indent, ")\n")) < 0) + if ((res = indent_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; case MSPH_TREE_DISJ: disj = (struct msph_tree_disj *)tree; - if ((res = ind_fprintf(f, indent, "(disj:%u,%u\n", - TXT(disj)->pos.line, TXT(disj)->pos.col)) < 0) + if ((res = indent_fprintf(f, indent, "(disj:%u,%u\n", + TEXT(disj)->pos.line, TEXT(disj)->pos.col)) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, T(disj->ltp))) < 0) + if ((res = tree_ind_fprint(f, indent+1, TREE(disj->ltp))) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, T(disj->rtp))) < 0) + if ((res = tree_ind_fprint(f, indent+1, TREE(disj->rtp))) < 0) return (res); ret += res; - if ((res = ind_fprintf(f, indent, ")\n")) < 0) + if ((res = indent_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; case MSPH_TREE_IMPL: impl = (struct msph_tree_impl *)tree; - if ((res = ind_fprintf(f, indent, "(impl:%u,%u\n", - TXT(impl)->pos.line, TXT(impl)->pos.col)) < 0) + if ((res = indent_fprintf(f, indent, "(impl:%u,%u\n", + TEXT(impl)->pos.line, TEXT(impl)->pos.col)) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, T(impl->ltp))) < 0) + if ((res = tree_ind_fprint(f, indent+1, TREE(impl->ltp))) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, T(impl->rtp))) < 0) + if ((res = tree_ind_fprint(f, indent+1, TREE(impl->rtp))) < 0) return (res); ret += res; - if ((res = ind_fprintf(f, indent, ")\n")) < 0) + if ((res = indent_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; case MSPH_TREE_ARROW: arrow = (struct msph_tree_arrow *)tree; - if ((res = ind_fprintf(f, indent, "(arrow:%u,%u\n", - TXT(arrow)->pos.line, TXT(arrow)->pos.col)) < 0) + if ((res = indent_fprintf(f, indent, "(arrow:%u,%u\n", + TEXT(arrow)->pos.line, TEXT(arrow)->pos.col)) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, T(arrow->ltp))) < 0) + if ((res = tree_ind_fprint(f, indent+1, TREE(arrow->ltp))) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, T(arrow->rtp))) < 0) + if ((res = tree_ind_fprint(f, indent+1, TREE(arrow->rtp))) < 0) return (res); ret += res; - if ((res = ind_fprintf(f, indent, ")\n")) < 0) + if ((res = indent_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; case MSPH_TREE_BOX: box = (struct msph_tree_box *)tree; - if ((res = ind_fprintf(f, indent, "(box:%u,%u\n", - TXT(box)->pos.line, TXT(box)->pos.col)) < 0) + if ((res = indent_fprintf(f, indent, "(box:%u,%u\n", + TEXT(box)->pos.line, TEXT(box)->pos.col)) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, T(box->inner))) < 0) + if ((res = tree_ind_fprint(f, indent+1, TREE(box->inner))) < 0) return (res); ret += res; - if ((res = ind_fprintf(f, indent, ")\n")) < 0) + if ((res = indent_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; case MSPH_TREE_FORALL: forall = (struct msph_tree_forall *)tree; - if ((res = ind_fprintf(f, indent, "(forall:%u,%u\n", - TXT(forall)->pos.line, TXT(forall)->pos.col)) < 0) + if ((res = indent_fprintf(f, indent, "(forall:%u,%u\n", + TEXT(forall)->pos.line, TEXT(forall)->pos.col)) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, T(forall->id))) < 0) + if ((res = tree_ind_fprint(f, indent+1, TREE(forall->name))) + < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, T(forall->inner))) < 0) + if ((res = tree_ind_fprint(f, indent+1, TREE(forall->inner))) + < 0) { return (res); + } ret += res; - if ((res = ind_fprintf(f, indent, ")\n")) < 0) + if ((res = indent_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; case MSPH_TREE_PAREN: paren = (struct msph_tree_paren *)tree; - if ((res = ind_fprintf(f, indent, "(paren:%u,%u\n", - TXT(paren)->pos.line, TXT(paren)->pos.col)) < 0) + if ((res = indent_fprintf(f, indent, "(paren:%u,%u\n", + TEXT(paren)->pos.line, TEXT(paren)->pos.col)) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, T(paren->inner))) < 0) + if ((res = tree_ind_fprint(f, indent+1, TREE(paren->inner))) + < 0) { return (res); + } ret += res; - if ((res = ind_fprintf(f, indent, ")\n")) < 0) + if ((res = indent_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; - 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) + 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) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, T(appl->id))) < 0) + if ((res = tree_ind_fprint(f, indent+1, TREE(tpappl->name))) < 0) return (res); ret += res; - STAILQ_FOREACH(tp, &appl->head, entries) { - if ((res = tree_ind_fprint(f, indent+1, T(tp))) < 0) + STAILQ_FOREACH(tp, &tpappl->args, entries) { + if ((res = tree_ind_fprint(f, indent+1, TREE(tp))) < 0) return (res); ret += res; } - if ((res = ind_fprintf(f, indent, ")\n")) < 0) + if ((res = indent_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; - 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) + 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) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, T(name->id))) < 0) + if ((res = tree_ind_fprint(f, indent+1, TREE(name->name))) < 0) return (res); ret += res; - if ((res = ind_fprintf(f, indent, ")\n")) < 0) + if ((res = indent_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; case MSPH_TREE_TRAIT: trait = (struct msph_tree_trait *)tree; - if ((res = ind_fprintf(f, indent, "(trait:%u,%u\n", - TXT(trait)->pos.line, TXT(trait)->pos.col)) < 0) + if ((res = indent_fprintf(f, indent, "(trait:%u,%u\n", + TEXT(trait)->pos.line, TEXT(trait)->pos.col)) < 0) return (res); ret += res; - if ((res = tree_ind_fprint(f, indent+1, T(trait->body))) < 0) + if ((res = tree_ind_fprint(f, indent+1, TREE(trait->body))) + < 0) { return (res); + } ret += res; - if ((res = ind_fprintf(f, indent, ")\n")) < 0) + if ((res = indent_fprintf(f, indent, ")\n")) < 0) return (res); ret += res; break; + case MSPH_TREE_NAMEDECL: + case MSPH_TREE_NAMEREF: case MSPH_TREE_IDENT: - 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)) + ident = IDENT(tree); + if ((res = indent_fprintf(f, indent, "(ident:%u,%u:%s)\n", + TEXT(ident)->pos.line, TEXT(ident)->pos.col, ident->str)) < 0) return (res); ret += res; break; case MSPH_TREE_TRUE: - if ((res = ind_fprintf(f, indent, "(true:%u,%u)\n", - TXT(tree)->pos.line, TXT(tree)->pos.col)) < 0) + if ((res = indent_fprintf(f, indent, "(true:%u,%u)\n", + TEXT(tree)->pos.line, TEXT(tree)->pos.col)) < 0) return (res); ret += res; break; case MSPH_TREE_FALSE: - if ((res = ind_fprintf(f, indent, "(false:%u,%u)\n", - TXT(tree)->pos.line, TXT(tree)->pos.col)) < 0) + if ((res = indent_fprintf(f, indent, "(false:%u,%u)\n", + TEXT(tree)->pos.line, TEXT(tree)->pos.col)) < 0) return (res); ret += res; break; @@ -542,9 +564,9 @@ tree_parse_unit(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - T(unit)->type = MSPH_TREE_UNIT; - T(unit)->parent = parent; - SCOPE_DECOR_INIT(&unit->dec); + TREE(unit)->type = MSPH_TREE_UNIT; + TREE(unit)->parent = parent; + DECOR_INIT(unit); unit->body = NULL; if ((namelen = strlcpy(unit->name, p->s->name, sizeof(unit->name))) @@ -553,13 +575,13 @@ tree_parse_unit(struct tree_parse *p, struct msph_tree *parent) goto err; } - if ((unit->body = tree_parse_body(p, T(unit))) == NULL) + if ((unit->body = tree_parse_body(p, TREE(unit))) == NULL) goto err; return (unit); err: - free_the_tree(T(unit)); + free_the_tree(TREE(unit)); return (NULL); } @@ -576,8 +598,8 @@ tree_parse_body(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - T(body)->type = MSPH_TREE_BODY; - T(body)->parent = parent; + TREE(body)->type = MSPH_TREE_BODY; + TREE(body)->parent = parent; STAILQ_INIT(&body->head); while ((res = tree_parse_next_token(p)) > 0) { @@ -585,16 +607,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, T(body)); + dir = tree_parse_tpdef(p, TREE(body)); break; case TOK_KW_NOMINAL: - dir = tree_parse_nomindecl(p, T(body)); + dir = tree_parse_nomindecl(p, TREE(body)); break; case TOK_KW_MEMBER: - dir = tree_parse_membdecl(p, T(body)); + dir = tree_parse_membdecl(p, TREE(body)); break; case TOK_KW_ASSERT: - dir = tree_parse_assert(p, T(body)); + dir = tree_parse_assert(p, TREE(body)); break; default: if ((tok = msph_token_copy(CTX(p), CURR_TOKEN(p))) @@ -615,7 +637,7 @@ tree_parse_body(struct tree_parse *p, struct msph_tree *parent) ret: return (body); err: - free_the_tree(T(body)); + free_the_tree(TREE(body)); return (NULL); } @@ -633,6 +655,7 @@ 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)); @@ -640,43 +663,98 @@ tree_parse_tpdef(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - 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 + TREE(def)->type = MSPH_TREE_TPDEF; + TREE(def)->parent = parent; + TEXT(def)->pos = CURR_TOKEN(p)->pos; + STAILQ_INIT(&def->params); + DECOR_INIT(def); EXPECT_READ_NEXT(res, p, MSPH_TREE_TPDEF, goto err); - if ((def->id = tree_parse_ident(p, T(def))) == NULL) + if ((def->name = tree_parse_namedecl(p, TREE(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, T(def))) == NULL) + if ((def->tp = tree_parse_tpexpr(p, TREE(def))) == NULL) goto err; return ((struct msph_tree_dir *)def); err: - free_the_tree(T(def)); + free_the_tree(TREE(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(struct tree_parse *p, struct msph_tree *parent) +tree_parse_ident_extsize(struct tree_parse *p, struct msph_tree *parent, + size_t size) { 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(*id))) == NULL) { + if ((id = malloc(sizeof(size))) == NULL) { MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - T(id)->type = MSPH_TREE_IDENT; - T(id)->parent = parent; - TXT(id)->pos = CURR_TOKEN(p)->pos; - NOM_DECOR_INIT(&id->dec); + TREE(id)->type = MSPH_TREE_IDENT; + TREE(id)->parent = parent; + TEXT(id)->pos = CURR_TOKEN(p)->pos; + DECOR_INIT(id); if (SPHO_STRLCPY(id->str, CURR_TOKEN(p)->data.str, sizeof(id->str)) >= sizeof(id->str)) { @@ -686,7 +764,7 @@ tree_parse_ident(struct tree_parse *p, struct msph_tree *parent) return (id); err: - free_the_tree(T(id)); + free_the_tree(TREE(id)); return (NULL); } @@ -715,7 +793,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_name(p, parent); + tp = tree_parse_tpname_or_tpappl(p, parent); break; case TOK_CONST_TRUE: tp = tree_parse_true(p, parent); @@ -734,7 +812,7 @@ tree_parse_tpexpr(struct tree_parse *p, struct msph_tree *parent) tp = NULL; } - SPHO_DEBUG_PRINT("returning tp type=%x\n", T(tp)->type); + SPHO_DEBUG_PRINT("returning tp type=%x\n", TREE(tp)->type); return (tp); } @@ -750,20 +828,20 @@ tree_parse_conj(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - T(conj)->type = MSPH_TREE_CONJ; - T(conj)->parent = parent; - TXT(conj)->pos = CURR_TOKEN(p)->pos; - TP_DECOR_INIT(&conj->htpe.dec); + TREE(conj)->type = MSPH_TREE_CONJ; + TREE(conj)->parent = parent; + TEXT(conj)->pos = CURR_TOKEN(p)->pos; + DECOR_INIT(conj); conj->ltp = NULL; conj->rtp = NULL; EXPECT_READ_NEXT(res, p, MSPH_TREE_CONJ, goto err); - if ((conj->ltp = tree_parse_tpexpr(p, T(conj))) + if ((conj->ltp = tree_parse_tpexpr(p, TREE(conj))) == NULL) goto err; EXPECT_READ_NEXT(res, p, MSPH_TREE_CONJ, goto err); - if ((conj->rtp = tree_parse_tpexpr(p, T(conj))) + if ((conj->rtp = tree_parse_tpexpr(p, TREE(conj))) == NULL) goto err; @@ -786,10 +864,10 @@ tree_parse_disj(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - T(disj)->type = MSPH_TREE_DISJ; - T(disj)->parent = parent; - TXT(disj)->pos = CURR_TOKEN(p)->pos; - TP_DECOR_INIT(&disj->htpe.dec); + TREE(disj)->type = MSPH_TREE_DISJ; + TREE(disj)->parent = parent; + TEXT(disj)->pos = CURR_TOKEN(p)->pos; + DECOR_INIT(disj); disj->ltp = NULL; disj->rtp = NULL; @@ -822,10 +900,10 @@ tree_parse_impl(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - T(impl)->type = MSPH_TREE_IMPL; - T(impl)->parent = parent; - TXT(impl)->pos = CURR_TOKEN(p)->pos; - TP_DECOR_INIT(&impl->htpe.dec); + TREE(impl)->type = MSPH_TREE_IMPL; + TREE(impl)->parent = parent; + TEXT(impl)->pos = CURR_TOKEN(p)->pos; + DECOR_INIT(impl); impl->ltp = NULL; impl->rtp = NULL; @@ -858,10 +936,10 @@ tree_parse_arrow(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - T(arrow)->type = MSPH_TREE_ARROW; - T(arrow)->parent = parent; - TXT(arrow)->pos = CURR_TOKEN(p)->pos; - TP_DECOR_INIT(&arrow->htpe.dec); + TREE(arrow)->type = MSPH_TREE_ARROW; + TREE(arrow)->parent = parent; + TEXT(arrow)->pos = CURR_TOKEN(p)->pos; + DECOR_INIT(arrow); arrow->ltp = NULL; arrow->rtp = NULL; @@ -894,19 +972,19 @@ tree_parse_box(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - T(box)->type = MSPH_TREE_BOX; - T(box)->parent = parent; - TXT(box)->pos = CURR_TOKEN(p)->pos; - TP_DECOR_INIT(&box->htpe.dec); + TREE(box)->type = MSPH_TREE_BOX; + TREE(box)->parent = parent; + TEXT(box)->pos = CURR_TOKEN(p)->pos; + DECOR_INIT(box); box->inner = NULL; EXPECT_READ_NEXT(res, p, MSPH_TREE_BOX, goto err); - if ((box->inner = tree_parse_tpexpr(p, T(box))) == NULL) + if ((box->inner = tree_parse_tpexpr(p, TREE(box))) == NULL) goto err; return ((struct msph_tree_tpexpr *)box); err: - free_the_tree(T(box)); + free_the_tree(TREE(box)); return (NULL); } @@ -922,51 +1000,50 @@ tree_parse_forall(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (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; + TREE(fa)->type = MSPH_TREE_FORALL; + TREE(fa)->parent = parent; + TEXT(fa)->pos = CURR_TOKEN(p)->pos; + DECOR_INIT(fa); + fa->name = NULL; fa->inner = NULL; EXPECT_READ_NEXT(res, p, MSPH_TREE_FORALL, goto err); - if ((fa->id = tree_parse_ident(p, T(fa))) == NULL) + if ((fa->name = tree_parse_namedecl(p, TREE(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, T(fa))) == NULL) + if ((fa->inner = tree_parse_tpexpr(p, TREE(fa))) == NULL) goto err; return ((struct msph_tree_tpexpr *)fa); err: - free_the_tree(T(fa)); + free_the_tree(TREE(fa)); return (NULL); } /* parse name or appl */ struct msph_tree_tpexpr * -tree_parse_name(struct tree_parse *p, struct msph_tree *parent) +tree_parse_tpname_or_tpappl(struct tree_parse *p, struct msph_tree *parent) { int res; - struct msph_tree_ident *id; - struct msph_tree_name *name; + struct msph_tree_tpname *tpname; struct msph_tree_tpexpr *ret; + struct msph_tree_nameref *nameref; struct msph_token *tok; ret = NULL; - name = NULL; + nameref = NULL; - if ((id = tree_parse_ident(p, NULL)) == NULL) + if ((nameref = tree_parse_nameref(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_applargs(p, id, parent)) == NULL) + if ((ret = tree_parse_tpapplargs(p, nameref, parent)) + == NULL) goto err; return (ret); } @@ -980,22 +1057,21 @@ tree_parse_name(struct tree_parse *p, struct msph_tree *parent) goto err; } - SPHO_DEBUG_PRINT("ident is name\n"); - if ((name = malloc(sizeof(*name))) == NULL) { + if ((tpname = malloc(sizeof(*tpname))) == NULL) { MSPH_ERR(CTX(p), MSPH_ERR_SYS); goto err; } - T(name)->type = MSPH_TREE_NAME; - T(name)->parent = parent; + TREE(tpname)->type = MSPH_TREE_TPNAME; + TREE(tpname)->parent = parent; - TXT(name)->pos = TXT(id)->pos; - TP_DECOR_INIT(&name->htpe.dec); - T(id)->parent = T(name); - name->id = id; + TEXT(tpname)->pos = TEXT(nameref)->pos; + DECOR_INIT(tpname); + TREE(nameref)->parent = TREE(tpname); + tpname->name = nameref; - return ((struct msph_tree_tpexpr *)name); + return ((struct msph_tree_tpexpr *)tpname); err: - free_the_tree(T(id)); + free_the_tree(TREE(nameref)); return (NULL); } @@ -1010,26 +1086,26 @@ err: * @return tpexpr node representing A[...]. */ struct msph_tree_tpexpr * -tree_parse_applargs(struct tree_parse *p, struct msph_tree_ident *id, +tree_parse_tpapplargs(struct tree_parse *p, struct msph_tree_nameref *name, struct msph_tree *parent) { int res; - struct msph_tree_appl *appl; + struct msph_tree_tpappl *tpappl; struct msph_tree_tpexpr *tp; tp = NULL; - EXPECT_CURR_TOKEN(p, TOK_LBRAK, MSPH_TREE_APPL, return (NULL)); + EXPECT_CURR_TOKEN(p, TOK_LBRAK, MSPH_TREE_TPAPPL, return (NULL)); - if ((appl = malloc(sizeof(*appl))) == NULL) { + if ((tpappl = malloc(sizeof(*tpappl))) == NULL) { MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - T(appl)->type = MSPH_TREE_APPL; - T(appl)->parent = parent; - TP_DECOR_INIT(&appl->htpe.dec); - appl->id = NULL; - STAILQ_INIT(&appl->head); + TREE(tpappl)->type = MSPH_TREE_TPAPPL; + TREE(tpappl)->parent = parent; + DECOR_INIT(tpappl); + tpappl->name = NULL; + STAILQ_INIT(&tpappl->args); /* parse the argument list */ while ((res = tree_parse_next_token(p)) == 1) { @@ -1037,38 +1113,38 @@ tree_parse_applargs(struct tree_parse *p, struct msph_tree_ident *id, if (CURR_TOKEN(p)->type == TOK_RBRAK) break; - /* if not start of argument list, check for comma and step - * tokenizer */ + /* if not at start of argument list, check for comma to know if + * we should parse another argument */ if (tp != NULL) { - EXPECT_CURR_TOKEN(p, TOK_COMMA, MSPH_TREE_APPL, + EXPECT_CURR_TOKEN(p, TOK_COMMA, MSPH_TREE_TPAPPL, goto err); - EXPECT_READ_NEXT(res, p, MSPH_TREE_APPL, goto err); + EXPECT_READ_NEXT(res, p, MSPH_TREE_TPAPPL, goto err); } - if ((tp = tree_parse_tpexpr(p, T(appl))) == NULL) + if ((tp = tree_parse_tpexpr(p, TREE(tpappl))) == NULL) goto err; - STAILQ_INSERT_TAIL(&appl->head, tp, entries); + STAILQ_INSERT_TAIL(&tpappl->args, tp, entries); } - /* system error */ + /* SYS_ERROR set in tree_parse_next_token */ 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_APPL); + MSPH_ERR_INFO(CTX(p), MSPH_ERR_TREE_EOF, MSPH_TREE_TPAPPL); goto err; } /* finally, appl takes ownership of id */ - T(id)->parent = T(appl); - appl->id = id; - TXT(appl)->pos = TXT(id)->pos; + TREE(name)->parent = TREE(tpappl); + tpappl->name = name; + TEXT(tpappl)->pos = TEXT(name)->pos; - return ((struct msph_tree_tpexpr *)appl); + return ((struct msph_tree_tpexpr *)tpappl); err: - free_the_tree(T(appl)); + free_the_tree(TREE(tpappl)); return (NULL); } @@ -1084,10 +1160,10 @@ tree_parse_true(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - T(t)->type = MSPH_TREE_TRUE; - T(t)->parent = parent; - TXT(t)->pos = CURR_TOKEN(p)->pos; - TP_DECOR_INIT(&t->htpe.dec); + TREE(t)->type = MSPH_TREE_TRUE; + TREE(t)->parent = parent; + TEXT(t)->pos = CURR_TOKEN(p)->pos; + DECOR_INIT(t); return ((struct msph_tree_tpexpr *)t); } @@ -1103,10 +1179,10 @@ tree_parse_false(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - T(f)->type = MSPH_TREE_FALSE; - T(f)->parent = parent; - TXT(f)->pos = CURR_TOKEN(p)->pos; - TP_DECOR_INIT(&f->htpe.dec); + TREE(f)->type = MSPH_TREE_FALSE; + TREE(f)->parent = parent; + TEXT(f)->pos = CURR_TOKEN(p)->pos; + DECOR_INIT(f); return ((struct msph_tree_tpexpr *)f); } @@ -1123,15 +1199,15 @@ tree_parse_paren(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - T(par)->type = MSPH_TREE_PAREN; - T(par)->parent = parent; - TXT(par)->pos = CURR_TOKEN(p)->pos; - TP_DECOR_INIT(&par->htpe.dec); + TREE(par)->type = MSPH_TREE_PAREN; + TREE(par)->parent = parent; + TEXT(par)->pos = CURR_TOKEN(p)->pos; + DECOR_INIT(par); par->inner = NULL; EXPECT_READ_NEXT(res, p, MSPH_TREE_PAREN, goto err); - if ((par->inner = tree_parse_tpexpr(p, T(par))) == NULL) + if ((par->inner = tree_parse_tpexpr(p, TREE(par))) == NULL) goto err; EXPECT_READ_NEXT(res, p, MSPH_TREE_PAREN, goto err); @@ -1139,7 +1215,7 @@ tree_parse_paren(struct tree_parse *p, struct msph_tree *parent) return ((struct msph_tree_tpexpr *)par); err: - free_the_tree(T(par)); + free_the_tree(TREE(par)); return (NULL); } @@ -1156,14 +1232,13 @@ tree_parse_trait(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - 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); + TREE(trait)->type = MSPH_TREE_TRAIT; + TREE(trait)->parent = parent; + TEXT(trait)->pos = CURR_TOKEN(p)->pos; + DECOR_INIT(trait); trait->body = NULL; - if ((trait->body = tree_parse_body(p, T(trait))) == NULL) + if ((trait->body = tree_parse_body(p, TREE(trait))) == NULL) goto err; EXPECT_READ_NEXT(res, p, MSPH_TREE_TRAIT, goto err); @@ -1171,7 +1246,7 @@ tree_parse_trait(struct tree_parse *p, struct msph_tree *parent) return ((struct msph_tree_tpexpr *)trait); err: - free_the_tree(T(trait)); + free_the_tree(TREE(trait)); return (NULL); } @@ -1180,27 +1255,30 @@ struct msph_tree_dir * tree_parse_nomindecl(struct tree_parse *p, struct msph_tree *parent) { int res; - struct msph_tree_nomindecl *nomd; + struct msph_tree_namedecl *name; + struct msph_tree_nomindecl *nomind; EXPECT_CURR_TOKEN(p, TOK_KW_NOMINAL, MSPH_TREE_NOMINDECL, return (NULL)); - if ((nomd = malloc(sizeof(*nomd))) == NULL) { + if ((nomind = malloc(sizeof(*nomind))) == NULL) { MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - T(nomd)->type = MSPH_TREE_NOMINDECL; - T(nomd)->parent = parent; - TXT(nomd)->pos = CURR_TOKEN(p)->pos; - nomd->id = NULL; + TREE(nomind)->type = MSPH_TREE_NOMINDECL; + TREE(nomind)->parent = parent; + TEXT(nomind)->pos = CURR_TOKEN(p)->pos; + nomind->name = NULL; EXPECT_READ_NEXT(res, p, MSPH_TREE_NOMINDECL, goto err); - if ((nomd->id = tree_parse_ident(p, T(nomd))) == NULL) + if ((name = tree_parse_namedecl(p, TREE(nomind))) == NULL) goto err; - return ((struct msph_tree_dir *)nomd); + nomind->name = name; + + return ((struct msph_tree_dir *)nomind); err: - free_the_tree(T(nomd)); + free_the_tree(TREE(nomind)); return (NULL); } @@ -1218,14 +1296,14 @@ tree_parse_membdecl(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - T(membd)->type = MSPH_TREE_MEMBDECL; - T(membd)->parent = parent; - TXT(membd)->pos = CURR_TOKEN(p)->pos; - membd->id = NULL; + TREE(membd)->type = MSPH_TREE_MEMBDECL; + TREE(membd)->parent = parent; + TEXT(membd)->pos = CURR_TOKEN(p)->pos; + membd->name = NULL; membd->tp = NULL; EXPECT_READ_NEXT(res, p, MSPH_TREE_MEMBDECL, goto err); - if ((membd->id = tree_parse_ident(p, T(membd))) == NULL) + if ((membd->name = tree_parse_namedecl(p, TREE(membd))) == NULL) goto err; EXPECT_READ_NEXT(res, p, MSPH_TREE_MEMBDECL, goto err); @@ -1233,12 +1311,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, T(membd))) == NULL) + if ((membd->tp = tree_parse_tpexpr(p, TREE(membd))) == NULL) goto err; return ((struct msph_tree_dir *)membd); err: - free_the_tree(T(membd)); + free_the_tree(TREE(membd)); return (NULL); } @@ -1256,14 +1334,14 @@ tree_parse_assert(struct tree_parse *p, struct msph_tree *parent) MSPH_ERR(CTX(p), MSPH_ERR_SYS); return (NULL); } - T(ass)->type = MSPH_TREE_ASSERT; - T(ass)->parent = parent; - TXT(ass)->pos = CURR_TOKEN(p)->pos; + TREE(ass)->type = MSPH_TREE_ASSERT; + TREE(ass)->parent = parent; + TEXT(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, T(ass))) == NULL) + if ((ass->ltp = tree_parse_tpexpr(p, TREE(ass))) == NULL) goto err; EXPECT_READ_NEXT(res, p, MSPH_TREE_ASSERT, goto err); @@ -1271,12 +1349,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, T(ass))) == NULL) + if ((ass->rtp = tree_parse_tpexpr(p, TREE(ass))) == NULL) goto err; return ((struct msph_tree_dir *)ass); err: - free_the_tree(T(ass)); + free_the_tree(TREE(ass)); return (NULL); } diff --git a/src/spho/bind.c b/src/spho/bind.c new file mode 100644 index 0000000..fc2258b --- /dev/null +++ b/src/spho/bind.c @@ -0,0 +1,165 @@ +#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 fbb0e9d..cd43288 100644 --- a/src/spho/ctx.c +++ b/src/spho/ctx.c @@ -4,7 +4,7 @@ #include #include -#include "spho/ctx.h" +#include "spho/spho.h" static const char *spho_ctx_sys_strerror(struct spho_ctx *); static const char *spho_ctx_intern_strerror(struct spho_ctx *); @@ -23,6 +23,10 @@ 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 } }; @@ -91,7 +95,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 >= sizeof(ctx->errbuf)) + if (res >= (ssize_t)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 442834c..da5c679 100644 --- a/src/spho/scope.c +++ b/src/spho/scope.c @@ -3,26 +3,33 @@ #include #include +#include "spho/spho.h" #include "spho/ctx.h" #include "spho/scope.h" -#include "spho/util.h" +#include "spho/bind.h" static void spho_nom_term(struct spho_nom *); -static int spho_scope_nom_get_norec(struct spho_scope *, const char *, size_t , - 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 *); int spho_scope_init(struct spho_scope *sc, struct spho_ctx *ctx, struct spho_scope *p) { - SLIST_INIT(&sc->subs); - SLIST_INIT(&sc->noms); - TAILQ_INIT(&sc->tps); - 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; + return (0); } @@ -34,6 +41,10 @@ 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 * @@ -67,7 +78,7 @@ spho_scope_create(struct spho_scope *sc) static void -spho_nom_term(struct spho_nom *nom) +spho_nom_term(__attribute__((unused)) struct spho_nom *nom) { return; } @@ -87,16 +98,12 @@ 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 (spho_scope_nom_get_norec(sc, nomstr, sz, &nom) == -1) + if (scope_nom_lookup_str_local(sc, nomstr, sz, &nom) == -1) return (NULL); if (nom != NULL) { @@ -109,25 +116,14 @@ 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: @@ -137,7 +133,7 @@ err: int -spho_scope_nom_get(struct spho_scope *sc, const char *nomstr, size_t sz, +spho_scope_nom_lookup_str(struct spho_scope *sc, const char *nomstr, size_t sz, struct spho_nom **out) { struct spho_nom *nom; @@ -164,12 +160,10 @@ spho_scope_nom_get(struct spho_scope *sc, const char *nomstr, size_t sz, } int -spho_scope_nom_lookup(struct spho_scope *sc, const char *nomstr, size_t sz, - struct spho_nom **out) +spho_scope_nom_lookup_str_strict(struct spho_scope *sc, const char *nomstr, + size_t sz, struct spho_nom **out) { - int ret; - - if (spho_scope_nom_get(sc, nomstr, sz, out) == -1) + if (spho_scope_nom_lookup_str(sc, nomstr, sz, out) == -1) return (-1); if (*out == NULL) { @@ -179,9 +173,56 @@ spho_scope_nom_lookup(struct spho_scope *sc, const char *nomstr, size_t sz, 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 -spho_scope_nom_get_norec(struct spho_scope *sc, const char *nomstr, size_t sz, - struct spho_nom **out) +scope_nom_lookup_str_local(struct spho_scope *sc, const char *nomstr, + size_t sz, struct spho_nom **out) { struct spho_nom *nom; @@ -202,3 +243,16 @@ spho_scope_nom_get_norec(struct spho_scope *sc, const char *nomstr, size_t sz, 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 new file mode 100644 index 0000000..ccc7806 --- /dev/null +++ b/src/spho/subt.c @@ -0,0 +1,239 @@ +/* + * 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 6f73d47..4140633 100644 --- a/src/spho/tp.c +++ b/src/spho/tp.c @@ -2,21 +2,13 @@ #include -#include "spho/ctx.h" -#include "spho/scope.h" +#include "spho/spho.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) { @@ -33,6 +25,22 @@ 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) { @@ -56,7 +64,7 @@ spho_tp_create_conj(struct spho_scope *sc, struct spho_tp *ltp, if ((tp = spho_tp_alloc(sc)) == NULL) return (NULL); - tp->form = SPHO_TP_FORM_CONJ; + tp->kind = SPHO_TP_FORM_CONJ; tp->d.binop.left = ltp; tp->d.binop.right = rtp; @@ -72,7 +80,7 @@ spho_tp_create_disj(struct spho_scope *sc, struct spho_tp *ltp, if ((tp = spho_tp_alloc(sc)) == NULL) return (NULL); - tp->form = SPHO_TP_FORM_DISJ; + tp->kind = SPHO_TP_FORM_DISJ; tp->d.binop.left = ltp; tp->d.binop.right = rtp; @@ -88,7 +96,7 @@ spho_tp_create_impl(struct spho_scope *sc, struct spho_tp *ltp, if ((tp = spho_tp_alloc(sc)) == NULL) return (NULL); - tp->form = SPHO_TP_FORM_IMPL; + tp->kind = SPHO_TP_FORM_IMPL; tp->d.binop.left = ltp; tp->d.binop.right = rtp; @@ -104,7 +112,7 @@ spho_tp_create_arrow(struct spho_scope *sc, struct spho_tp *ltp, if ((tp = spho_tp_alloc(sc)) == NULL) return (NULL); - tp->form = SPHO_TP_FORM_ARROW; + tp->kind = SPHO_TP_FORM_ARROW; tp->d.binop.left = ltp; tp->d.binop.right = rtp; @@ -119,7 +127,7 @@ spho_tp_create_box(struct spho_scope *sc, struct spho_tp *inner) if ((tp = spho_tp_alloc(sc)) == NULL) return (NULL); - tp->form = SPHO_TP_FORM_BOX; + tp->kind = SPHO_TP_FORM_BOX; tp->d.unop.operand = inner; return (tp); @@ -134,9 +142,9 @@ spho_tp_create_forall(struct spho_scope *sc, struct spho_nom *nom, if ((ret = spho_tp_alloc(sc)) == NULL) return (NULL); - ret->form = SPHO_TP_FORM_FORALL; - ret->d.bind.nom = nom; - ret->d.bind.bound = tp; + ret->kind = SPHO_TP_FORM_FORALL; + ret->d.fa.nom = nom; + ret->d.fa.tp = tp; return (ret); } @@ -149,7 +157,7 @@ spho_tp_create_true(struct spho_scope *sc) if ((ret = spho_tp_alloc(sc)) == NULL) return (NULL); - ret->form = SPHO_TP_FORM_TRUE; + ret->kind = SPHO_TP_FORM_TRUE; ret->d.konst = tp_konst_true; return (ret); @@ -163,7 +171,7 @@ spho_tp_create_false(struct spho_scope *sc) if ((ret = spho_tp_alloc(sc)) == NULL) return (NULL); - ret->form = SPHO_TP_FORM_FALSE; + ret->kind = SPHO_TP_FORM_FALSE; ret->d.konst = tp_konst_false; return (ret); @@ -177,7 +185,7 @@ spho_tp_create_name(struct spho_scope *sc, struct spho_nom *nom) if ((ret = spho_tp_alloc(sc)) == NULL) return (NULL); - ret->form = SPHO_TP_FORM_NOM; + ret->kind = SPHO_TP_FORM_NAME; ret->d.nom.nom = nom; return (ret); @@ -192,7 +200,7 @@ spho_tp_create_appl(struct spho_scope *sc, struct spho_nom *nom, if ((ret = spho_tp_alloc(sc)) == NULL) return (NULL); - ret->form = SPHO_TP_FORM_APPL; + ret->kind = SPHO_TP_FORM_APPL; ret->d.appl.nom = nom; ret->d.appl.args = args; @@ -208,23 +216,72 @@ spho_tp_create_member(struct spho_scope *sc, struct spho_nom *nom, if ((ret = spho_tp_alloc(sc)) == NULL) return (NULL); - ret->form = SPHO_TP_FORM_MEMBER; - ret->d.bind.nom = nom; - ret->d.bind.bound = tp; + ret->kind = SPHO_TP_FORM_MEMBER; + ret->d.memb.nom = nom; + ret->d.memb.tp = 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->form) { + switch (tp->kind & SPHO_TP_FORM_MASK) { case SPHO_TP_FORM_TRUE: case SPHO_TP_FORM_FALSE: - case SPHO_TP_FORM_NOM: + case SPHO_TP_FORM_NAME: + case SPHO_TP_FORM_VAR: break; case SPHO_TP_FORM_CONJ: case SPHO_TP_FORM_DISJ: @@ -237,8 +294,10 @@ 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.bind.bound); + spho_tp_destroy(tp->d.memb.tp); break; case SPHO_TP_FORM_APPL: STAILQ_FOREACH(arg, tp->d.appl.args, entries) {