lnsol/log-e-sappho
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

type fixes and bindings + notes on subtyping #1

Merged
lnsol merged 1 commit from subt-resurrection into main 2025-06-25 18:37:30 +00:00
Conversation 0 Commits 1 Files changed 28 +2253 -783
28 changed files with 2253 additions and 783 deletions
Download patch file Download diff file Expand all files Collapse all files

2
.clangd
View file

@ -1,2 +0,0 @@
Diagnostics:
UnusedIncludes: None

21
.gitignore vendored
View file

@ -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/

19
CMakeLists.txt
View file

@ -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})

37
README.md
View file

@ -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/`

15
docs/about/contributions.md Normal file
View file

@ -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...

39
docs/about/cycle.md Normal file
View file

@ -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
]

398
docs/about/formalities.md Normal file
View file

@ -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
```

88
docs/about/interpret.md Normal file
View file

@ -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

21
example/non-parse/ex6.msph Normal file
View file

@ -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
}
}

9
example/subt/rec-lockstep.msph Normal file
View file

@ -0,0 +1,9 @@
type A = { x : { y : A } }
type B = { y : { x : B } }
assert { x : B } <: A
assert A <: { x : B }

33
include/msph/decor.h
View file

@ -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 */

1
include/msph/sphophi.h
View file

@ -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 *);

218
include/msph/tree.h
View file

@ -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

54
include/spho/bind.h Normal file
View file

@ -0,0 +1,54 @@
#ifndef _SPHO_BIND_H
#define _SPHO_BIND_H
#include <sys/queue.h>
#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

50
include/spho/err.h
View file

@ -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 */

83
include/spho/scope.h
View file

@ -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 */

77
include/spho/spho.h
View file

@ -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

9
include/spho/subt.h Normal file
View file

@ -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 */

25
include/spho/tp.h
View file

@ -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 *);

25
include/spho/util.h
View file

@ -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

598
src/msph/sphophi.c
View file

File diff suppressed because it is too large Load diff

3
src/msph/token.c
View file

@ -5,9 +5,12 @@
#include <string.h>
#include <ctype.h>
#include "spho/spho.h"
#include "msph/err.h"
#include "msph/token.h"
struct msph_matcher {
size_t off;
size_t matchlen;

566
src/msph/tree.c
View file

File diff suppressed because it is too large Load diff

165
src/spho/bind.c Normal file
View file

@ -0,0 +1,165 @@
#include <sys/queue.h>
#include <string.h>
#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);
}

8
src/spho/ctx.c
View file

@ -4,7 +4,7 @@
#include <stdlib.h>
#include <string.h>
#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),

120
src/spho/scope.c
View file

@ -3,26 +3,33 @@
#include <stdlib.h>
#include <string.h>
#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);
}

239
src/spho/subt.c Normal file
View file

@ -0,0 +1,239 @@
/*
* Subtyping
*/
#include <stdlib.h>
#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);
}

113
src/spho/tp.c
View file

@ -2,21 +2,13 @@
#include <stdlib.h>
#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) {