Start implementing types

Author: suhr

doc/razbor.makam

@@ -0,0 +1,182 @@
+path: type.
+mkpath: (Modules: list string) (Data: list string) -> path.
+
+endinanness: type.
+big_endian: endinanness.
+little_endian: endinanness.
+
+rel_expr: type.
+rel_hole: rel_expr.
+rel_sizeof: rel_expr.
+rel_int: int -> rel_expr.
+rel_ref: path -> rel_expr.
+
+rel: type.
+rel_lt: rel_expr -> rel_expr -> rel.
+rel_le: rel_expr -> rel_expr -> rel.
+rel_eq: rel_expr -> rel_expr -> rel.
+rel_ge: rel_expr -> rel_expr -> rel.
+rel_gt: rel_expr -> rel_expr -> rel.
+
+value: type.
+value_bool: bool -> value.
+value_int: int -> value.
+
+ty: type.
+top: ty.
+bottom: ty.
+
+boolean: ty.
+integer: ty.
+
+u: int -> endinanness -> ty.
+s: int -> endinanness -> ty.
+
+arr: ty -> list rel -> ty.
+str: list rel -> ty.
+
+meet: list ty -> ty.
+join: list ty -> ty.
+
+ref: path -> ty.
+
+liq: ty -> list rel -> ty.
+size: list rel -> ty.
+val: value -> ty -> ty.
+
+prod: list path -> ty.
+
+reduced: ty -> ty.
+
+typeof: (Path: path) (Type: ty) -> prop.
+ctypeof: (Path: path) (Type: ty) -> prop.
+
+simpl: (Complex: ty) (Simple: ty) -> prop.
+subst: ty -> ty -> prop.
+reduce_meet: ty -> ty -> ty -> prop.
+
+ctypeof P T :-
+    typeof P Tx,
+    subst Tx Ty,
+    simpl Ty T.
+
+is_simple: ty -> prop.
+is_simple (join X::Xs) :-
+    failure.
+is_simple (prod X::Xs) :-
+    failure.
+is_simple _ :-
+    success.
+
+subst (arr Tx Nx) (arr Ty Ny) :-
+    subst Tx Ty,
+    subst Nx Ny.
+subst (str X) (str Y) :-
+    subst X Y.
+subst (meet X::Xs) (meet Y::Ys) :-
+    subst X Y,
+    subst (meet Xs) (meet Ys).
+subst (liq Tx P) (liq Ty P) :-
+    subst Tx Ty.
+subst (size X) (size Y) :-
+    subst X Y.
+subst (val V Tx) (val V Ty) :-
+    subst Tx Ty.
+subst (ref P) T :-
+    ctypeof P Tx,
+    if is_simple Tx
+        then eq T Tx
+        else eq T (ref P).
+subst T T.
+
+simpl (arr Tx Nx) (arr Ty Ny) :-
+    simpl Tx Ty,
+    simpl Nx Ny.
+simpl (str Tx) (str Ty) :-
+    simpl Tx Ty.
+simpl (liq Tx P) (liq Ty P) :-
+    simpl Tx Ty.
+simpl (size Tx) (size Ty) :-
+    simpl Tx Ty.
+simpl (val V Tx) (val V Ty) :-
+    simpl Tx Ty.
+simpl (meet []) top.
+simpl (join []) bottom.
+simpl (meet X::Xs) T :-
+    reduce_meet X (meet Xs) T.
+simpl (join X::[]) Y :-
+    simpl X Y.
+simpl (join X::Xs) (join Z) :-
+    simpl X Y,
+    simpl (join Xs) (join Ys),
+    reduce_join Y::Ys Z.
+simpl T T.
+
+reduce_join (join X)::Xs Y :-
+    append X Xs Z,
+    reduce_join Z Y.
+reduce_join X::Ys X::Zs :-
+    reduce_join Ys Zs.
+reduce_join [] [].
+
+reduce_meet X X X.
+reduce_meet top X X.
+reduce_meet X top X.
+reduce_meet bottom X bottom.
+reduce_meet X bottom bottom.
+reduce_meet integer (u S E) (u S E).
+reduce_meet integer (s S E) (s S E).
+reduce_meet (arr Tx Sx) (arr Ty Sy) (arr T S) :-
+    reduce_meet Tx Ty T,
+    reduce_meet Sx Sy S.
+reduce_meet (str Sx) (str Sy) (str S) :-
+    reduce_meet Sx Sy S.
+
+reduce_meet (liq Tx Px) (liq Ty Py) (liq T P) :-
+    reduce_meet Tx Ty T,
+    append Px Py P.
+reduce_meet (liq Tx P) (val V Ty) (val V (liq T P)) :-
+    reduce_meet Tx Ty T.
+reduce_meet (val V Tx) (liq Ty P) (val V (liq T P)) :-
+    reduce_meet Tx Ty T.
+reduce_meet (val Vx Tx) (val Vy Ty) (val V T) :-
+    reduce_meet Vx Vy V,
+    reduce_meet Tx Ty T.
+reduce_meet (val V Tx) Ty (val V T) :-
+    reduce_meet Tx Ty T.
+reduce_meet Tx (val V Ty) (val V T) :-
+    reduce_meet Tx Ty T.
+
+(* TODO: support non-reducible terms *)
+reduce_meet (meet X::Xs) (meet Y) Z :-
+    append Xs Y Ts,
+    reduce_meet X (meet Ts) Z.
+reduce_meet (meet []) Y Y.
+reduce_meet (meet X::Xs) Y Z :-
+    append Xs [Y] Ts,
+    reduce_meet X (meet Ts) Z.
+reduce_meet X (meet []) X.
+reduce_meet X (meet Y::Ys) Z :-
+    reduce_meet X Y T,
+    reduce_meet T (meet Ys) Z.
+
+reduce_meet X (join [Y]) Z :-
+    reduce_meet X Y Z.
+reduce_meet X (join Y::Ys) (join Z::Zs) :-
+    reduce_meet X Y Z,
+    reduce_meet X (join Ys) (join Zs).
+
+reduce_meet (join [X]) Y Z :-
+    reduce_meet X Y Z.
+reduce_meet (join X::Xs) Y (join Z::Zs) :-
+    reduce_meet X Y Z,
+    reduce_meet (join Xs) Y (join Zs).
+
+reduce_meet (ref X) Y (reduced (meet [X, Y])).
+reduce_meet X (ref Y) Z (reduced (meet [X, Y])).
+
+reduce_meet (prod X) Y Z :- failure.
+reduce_meet X (prod Y) Z :- failure.
+
+(* TODO: everything else *)
+reduce_meet _ _ bottom.

src/lib.rs

@@ -4,6 +4,7 @@ use pest_derive::Parser;
 
 pub mod path;
 pub mod expr;
+pub mod types;
 pub mod report;
 
 #[derive(Parser)]

src/main.rs

@@ -7,14 +7,17 @@ type Error = Box<dyn std::error::Error>;
 
 fn main() -> Result<(), Error> {
     let loader = razbor::expr::ExprLoader::new();
-    let (file_table, tox) = loader.load("../tox/tox-ksy/razbor/tox.mexpr");
+    let (file_table, tox) = loader.load("../tox/tox-razbor/src/tox.mexpr");
     let mods = tox.unwrap();
 
     let converter = razbor::path::ExprConverter::new();
     let mut table = converter.convert(&mods).unwrap();
 
     let namer = razbor::path::NameResolver::new();
-    let errors = namer.resolve(&mut table).unwrap_err();
+    namer.resolve(&mut table).unwrap();
+
+    let ty_conv = razbor::types::ExprToType::new();
+    let errors = ty_conv.into_types(table).unwrap_err();
 
     let mut sourcer = razbor::report::Sourcer::default();
     for err in &errors {

src/path.rs

@@ -13,6 +13,15 @@ pub enum PathSegment {
     Name(SmolStr),
 }
 
+impl std::fmt::Display for PathSegment {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        match self {
+            PathSegment::Pos(n) => write!(f, "{}", n),
+            PathSegment::Name(name) => write!(f, "{}", name)
+        }
+    }
+}
+
 #[derive(Debug, Clone, PartialEq, PartialOrd, Eq, Ord, Default)]
 pub struct RzPath {
     pub modules: Vec<SmolStr>,