wip type checking

This commit is contained in:
Nicolas Abril 2024-08-06 11:13:15 +02:00
parent 6f0590f15f
commit 4e9a4d6100
9 changed files with 1362 additions and 43 deletions

View File

@ -49,6 +49,7 @@
"ints",
"itertools",
"ITRS",
"kindc",
"kwarg",
"kwargs",
"lcons",

View File

@ -1,10 +1,10 @@
type String:
Nil
Cons { head: u24, ~tail: String }
Cons { head: u24, ~tail: String }
type List(T):
Nil
Cons { head: T, ~tail: List(T) }
Cons { head: T, ~tail: List(T) }
# Returns the length of a list and the list itself.
def List/length(xs: List(T)) -> (u24, List(T)):
@ -109,7 +109,7 @@ type Map T = (Node (value: T) ~(left: (Map T)) ~(right: (Map T))) | (Leaf)
Map/empty : (Map T) = Map/Leaf
Map/get (map: (Map T)) (key: u24) : ((Map T), T) =
Map/get (map: (Map T)) (key: u24) : (T, (Map T)) =
match map {
Map/Leaf: (*, map)
Map/Node:
@ -180,7 +180,7 @@ def IO/bind(a: IO(A), b: A -> IO(B)) -> IO(B):
case IO/Call:
return IO/Call(IO/MAGIC, a.func, a.argm, lambda x: IO/bind(a.cont(x), b))
def IO/call(func: String, argm: Any) -> IO(T):
def IO/call(func: String, argm: Any) -> IO(Any):
return IO/Call(IO/MAGIC, func, argm, lambda x: IO/Done(IO/MAGIC, x))
## Time and sleep
@ -286,23 +286,6 @@ def IO/FS/write_file(path: String, bytes: List(u24)) -> IO(None):
* <- IO/FS/close(f)
return wrap(*)
def Bytes/split_once(xs: List(u24), cond: u24) -> Result((List(u24), List(u24)), List(u24)):
return Bytes/split_once.go(xs, cond, DiffList/new)
def Bytes/split_once.go(
xs: List(u24),
cond: u24,
acc: List(u24) -> List(u24)
) -> Result((List(u24), List(u24)), List(u24)):
match xs:
case List/Nil:
return Result/Err(DiffList/to_list(acc))
case List/Cons:
if xs.head == cond:
return Result/Ok((DiffList/to_list(acc), xs.tail))
else:
return Bytes/split_once.go(xs.tail, cond, DiffList/append(acc, xs.head))
### Standard input and output utilities
# Prints a string to stdout, encoding it with utf-8.
@ -334,25 +317,24 @@ def IO/input.go(acc: List(u24) -> List(u24)) -> IO(String):
### Dynamically linked libraries
# Returns an unique id to the library object encoded as a u24
# 'path' is the path to the library file.
# 'lazy' is a boolean encoded as a u24 that determines if all functions are loaded lazily or upfront.
# Returns an unique id to the library object encoded as a u24
def IO/DyLib/open(path: String, lazy: u24) -> IO(u24):
return IO/call("DL_OPEN", (path, lazy))
# Calls a function of a previously opened library.
# The returned value is determined by the called function.
# 'dl' is the id of the library object.
# 'fn' is the name of the function in the library.
# 'args' are the arguments to the function. The expected values depend on the called function.
# The returned value is determined by the called function.
def IO/DyLib/call(dl: u24, fn: String, args: Any) -> IO(Any):
return IO/call("DL_CALL", (dl, (fn, args)))
# IO/DyLib/close(dl: u24) -> None
# Closes a previously open library.
# 'dl' is the id of the library object.
# Returns nothing.
def IO/DyLib/close(dl):
# 'dl' is the id of the library object.
def IO/DyLib/close(dl: u24) -> IO(None):
return IO/Call(IO/MAGIC, "DL_CLOSE", (dl), IO/wrap)
# Lazy thunks
@ -363,18 +345,49 @@ def IO/DyLib/close(dl):
# We can build a defered call directly or by by using defer and defer_arg
# The example above can be written as:
# (defer_arg (defer_arg (defer_arg (defer @arg1 @arg2 @arg3 (f arg1 arg2 arg3)) arg1) arg2) arg3)
defer val =
defer (val: a) : (a -> b) -> b =
@x (x val)
# defer_arg(defered: A -> B -> C, arg: B) -> (A -> C)
defer_arg defered arg =
defer_arg (defered: a -> b -> c) (arg: b) : (a -> c) -> c =
@x (defered x arg)
# undefer(defered: (A -> A) -> B) -> B
undefer defered =
undefer (defered: (a -> a) -> b) : b =
(defered @x x)
# Native number casts
# f24_to_u24(x: f24) -> u24
# Casts a f24 number to a u24.
hvm f24_to_u24 -> (f24 -> u24):
($([u24] ret) ret)
# i24_to_u24(x: i24) -> u24
# Casts an i24 number to a u24.
hvm i24_to_u24 -> (i24 -> u24):
($([u24] ret) ret)
# u24_to_i24(x: u24) -> i24
# Casts a u24 number to an i24.
hvm u24_to_i24 -> (u24 -> i24):
($([i24] ret) ret)
# f24_to_i24(x: f24) -> i24
# Casts a f24 number to an i24.
hvm f24_to_i24 -> (f24 -> i24):
($([i24] ret) ret)
# u24_to_f24(x: u24) -> f24
# Casts a u24 number to a f24.
hvm u24_to_f24 -> (u24 -> f24):
($([f24] ret) ret)
# i24_to_f24(x: i24) -> f24
# Casts an i24 number to a f24.
hvm i24_to_f24 -> (i24 -> f24):
($([f24] ret) ret)
# String Encoding and Decoding
Utf8/REPLACEMENT_CHARACTER : u24 = '\u{FFFD}'

View File

@ -305,6 +305,7 @@ pub struct AdtCtr {
pub struct CtrField {
pub nam: Name,
pub rec: bool,
pub typ: Type,
}
#[derive(Debug, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]

View File

@ -221,7 +221,7 @@ impl<'a> FunParser<'a> {
let ctr_name = Name::new(format!("{type_name}/{ctr_name}"));
let fields = self.list_like(|p| p.parse_type_ctr_field(), "", ")", "", false, 0)?;
let (fields, field_types): (Vec<_>, Vec<_>) = fields.into_iter().unzip();
let field_types = fields.iter().map(|f| f.typ.clone()).collect::<Vec<_>>();
let end_idx = *self.index();
self.check_repeated_ctr_fields(&fields, &ctr_name, ini_idx..end_idx)?;
@ -238,7 +238,7 @@ impl<'a> FunParser<'a> {
}
}
fn parse_type_ctr_field(&mut self) -> ParseResult<(CtrField, Type)> {
fn parse_type_ctr_field(&mut self) -> ParseResult<CtrField> {
let rec = self.try_consume("~");
let nam;
@ -255,7 +255,7 @@ impl<'a> FunParser<'a> {
nam = self.parse_var_name()?;
typ = Type::Any;
}
Ok((CtrField { nam, rec }, typ))
Ok(CtrField { nam, typ, rec })
}
fn parse_fun_def(&mut self) -> ParseResult<FunDefinition> {

View File

@ -40,13 +40,16 @@ impl Term {
Term::Ref { nam } => {
if seen.contains(nam) {
// Don't expand recursive references
} else {
} else if let Some(def) = book.defs.get(nam) {
// Regular function, expand
seen.push(nam.clone());
let mut body = book.defs.get(nam).unwrap().rule().body.clone();
let mut body = def.rule().body.clone();
body.rename_unscoped(globals_count, &mut HashMap::new());
*self = body;
self.expand_ref_return(book, seen, globals_count);
seen.pop().unwrap();
} else {
// Not a regular function, don't expand
}
}
Term::Fan { els, .. } | Term::List { els } => {

View File

@ -21,4 +21,5 @@ pub mod resolve_refs;
pub mod resolve_type_ctrs;
pub mod resugar_list;
pub mod resugar_string;
pub mod type_check;
pub mod unique_names;

File diff suppressed because it is too large Load Diff

View File

@ -101,13 +101,12 @@ impl<'a> ImpParser<'a> {
};
self.skip_trivia_inline()?;
let (fields, field_types): (Vec<_>, Vec<_>) = if self.starts_with("{") {
let fields = if self.starts_with("{") {
self.list_like(|p| p.parse_variant_field(), "{", "}", ",", true, 0)?
} else {
vec![]
}
.into_iter()
.unzip();
};
let field_types = fields.iter().map(|f| f.typ.clone()).collect::<Vec<_>>();
let end_idx = *self.index();
self.check_repeated_ctr_fields(&fields, &name, ini_idx..end_idx)?;
@ -165,7 +164,7 @@ impl<'a> ImpParser<'a> {
} else {
vec![]
};
let (fields, field_types): (Vec<_>, Vec<_>) = fields.into_iter().unzip();
let field_types = fields.iter().map(|f| f.typ.clone()).collect::<Vec<_>>();
let end_idx = *self.index();
self.check_repeated_ctr_fields(&fields, &name, ini_idx..end_idx)?;
@ -173,7 +172,7 @@ impl<'a> ImpParser<'a> {
Ok(AdtCtr { name, typ, fields })
}
fn parse_variant_field(&mut self) -> ParseResult<(CtrField, Type)> {
fn parse_variant_field(&mut self) -> ParseResult<CtrField> {
let rec = self.try_consume_exactly("~");
self.skip_trivia_inline()?;
@ -182,7 +181,7 @@ impl<'a> ImpParser<'a> {
let typ = if self.try_consume_exactly(":") { self.parse_type_expr()? } else { Type::Any };
Ok((CtrField { nam, rec }, typ))
Ok(CtrField { nam, typ, rec })
}
fn parse_primary_expr(&mut self, inline: bool) -> ParseResult<Expr> {

View File

@ -128,6 +128,8 @@ pub fn desugar_book(
// Manual match linearization
ctx.book.linearize_match_with();
type_check_book(&mut ctx)?;
ctx.book.encode_matches(opts.adt_encoding);
// sanity check
@ -165,6 +167,17 @@ pub fn desugar_book(
}
}
pub fn type_check_book(ctx: &mut Ctx) -> Result<(), Diagnostics> {
// TODO: Check unbound type variables and constructors
let old_book = std::mem::replace(ctx.book, ctx.book.clone());
ctx.make_native_defs();
ctx.book.encode_adts(AdtEncoding::Scott);
let res = ctx.type_check();
*ctx.book = old_book;
res?;
Ok(())
}
pub fn run_book(
mut book: Book,
run_opts: RunOpts,