diff --git a/src/dict.rs b/src/dict.rs
index e5cb464..d6636c4 100644
--- a/src/dict.rs
+++ b/src/dict.rs
@@ -25,11 +25,11 @@ pub trait TypeDict : Send + Sync {
}
}
- fn get_typeid_creat(&mut self, tn: &String) -> TypeID {
- if let Some(id) = self.get_typeid(tn) {
+ fn get_typeid_creat(&mut self, tn: &str) -> TypeID {
+ if let Some(id) = self.get_typeid(&tn.to_string()) {
id
} else {
- self.add_typename(tn.clone())
+ self.add_typename(tn.to_string())
}
}
}
diff --git a/src/lib.rs b/src/lib.rs
index 6c844a6..882082c 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -1,21 +1,37 @@
+#![allow(mixed_script_confusables)]
pub mod bimap;
pub mod dict;
-pub mod term;
-pub mod substitution;
pub mod lexer;
pub mod parser;
pub mod unparser;
-pub mod sugar;
pub mod curry;
-pub mod lnf;
+
+pub mod lnf; // deprecated
+pub mod subtype; // deprecated
+
pub mod pnf;
-pub mod subtype;
+pub mod pnf_sugared;
+
+pub mod term;
+pub mod sugar;
+
+pub mod substitution;
+pub mod substitution_sugared;
+
pub mod unification;
+pub mod unification_sugared;
+
pub mod morphism;
+pub mod morphism_sugared;
+
pub mod morphism_base;
+pub mod morphism_base_sugared;
+
pub mod morphism_path;
+pub mod morphism_path_sugared;
+
pub mod steiner_tree;
#[cfg(test)]
diff --git a/src/morphism.rs b/src/morphism.rs
index 69853f3..dc99b38 100644
--- a/src/morphism.rs
+++ b/src/morphism.rs
@@ -1,6 +1,13 @@
use {
crate::{
- subtype_unify, sugar::SugaredTypeTerm, unification::UnificationProblem, unparser::*, TypeDict, TypeID, TypeTerm
+ pnf::splice_ladders,
+ substitution_sugared::SugaredSubstitution,
+ subtype_unify,
+ sugar::{SugaredStructMember, SugaredTypeTerm},
+ unification::UnificationProblem,
+ unification_sugared::SugaredUnificationProblem,
+ unparser::*,
+ TypeDict, TypeID, TypeTerm
},
std::{collections::HashMap, u64}
};
@@ -11,11 +18,6 @@ use {
pub struct MorphismType {
pub src_type: TypeTerm,
pub dst_type: TypeTerm,
-/*
- pub subtype_bounds: Vec< (TypeTerm, TypeTerm) >,
- pub trait_bounds: Vec< (TypeTerm, TypeTerm) >,
- pub equal_bounds: Vec< (TypeTerm, TypeTerm) >,
-*/
}
impl MorphismType {
@@ -23,10 +25,6 @@ impl MorphismType {
MorphismType {
src_type: self.src_type.strip().param_normalize(),
dst_type: self.dst_type.strip().param_normalize(),
-/*
- subtype_bounds: Vec::new(),
- trait_bounds: Vec::new()
- */
}
}
}
@@ -65,12 +63,6 @@ impl<M: Morphism + Clone> MorphismInstance<M> {
self.m.get_type().dst_type.clone()
]).apply_subst(&self.σ)
.clone(),
-/*
- trait_bounds: Vec::new(),
- subtype_bounds: Vec::new()
- */
}.normalize()
}
}
-
-//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
diff --git a/src/morphism_base.rs b/src/morphism_base.rs
index 91dcba0..f922046 100644
--- a/src/morphism_base.rs
+++ b/src/morphism_base.rs
@@ -1,9 +1,7 @@
use {
crate::{
- subtype_unify, sugar::SugaredTypeTerm, unification::UnificationProblem, unparser::*, TypeDict, TypeID, TypeTerm,
- morphism::{MorphismType, Morphism, MorphismInstance}
- },
- std::{collections::HashMap, u64}
+ morphism::{Morphism, MorphismInstance, MorphismType}, morphism_path_sugared::SugaredShortestPathProblem, morphism_sugared::{MorphismInstance2, SugaredMorphismType}, subtype_unify, sugar::SugaredTypeTerm, unification::UnificationProblem, TypeDict, TypeID, TypeTerm
+ }
};
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
@@ -101,29 +99,29 @@ impl<M: Morphism + Clone> MorphismBase<M> {
ty: &MorphismType,
dict: &mut impl TypeDict
) -> Option< MorphismInstance<M> > {
- eprintln!("find direct morph");
+ //eprintln!("find direct morph");
for m in self.morphisms.iter() {
let ty = ty.clone().normalize();
let morph_type = m.get_type().normalize();
-
+ /*
eprintln!("find direct morph:\n {} <= {}",
dict.unparse(&ty.src_type), dict.unparse(&morph_type.src_type),
);
-
+*/
if let Ok((halo, σ)) = subtype_unify(&ty.src_type, &morph_type.src_type) {
- eprintln!("halo: {}", dict.unparse(&halo));
+ //eprintln!("halo: {}", dict.unparse(&halo));
let dst_type = TypeTerm::Ladder(vec![
halo.clone(),
morph_type.dst_type.clone()
]).normalize().param_normalize();
-
+/*
eprintln!("-----------> {} <= {}",
dict.unparse(&dst_type), dict.unparse(&ty.dst_type)
);
-
+*/
if let Ok((halo2, σ2)) = subtype_unify(&dst_type, &ty.dst_type) {
- eprintln!("match. halo2 = {}", dict.unparse(&halo2));
+ //eprintln!("match. halo2 = {}", dict.unparse(&halo2));
return Some(MorphismInstance {
m: m.clone(),
halo,
diff --git a/src/morphism_base_sugared.rs b/src/morphism_base_sugared.rs
new file mode 100644
index 0000000..1fb1dcf
--- /dev/null
+++ b/src/morphism_base_sugared.rs
@@ -0,0 +1,143 @@
+use {
+ crate::{
+ morphism_path_sugared::{SugaredMorphismPath, SugaredShortestPathProblem}, morphism_sugared::{MorphismInstance2, SugaredMorphism, SugaredMorphismType}, sugar::SugaredTypeTerm, SugaredStructMember, TypeDict, TypeID, TypeTerm
+ }
+};
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+#[derive(Clone)]
+pub struct SugaredMorphismBase<M: SugaredMorphism + Clone> {
+ morphisms: Vec< M >
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+impl<M: SugaredMorphism + Clone> SugaredMorphismBase<M> {
+ pub fn new() -> Self {
+ SugaredMorphismBase {
+ morphisms: Vec::new()
+ }
+ }
+
+ pub fn add_morphism(&mut self, m: M) {
+ self.morphisms.push( m );
+ }
+
+ pub fn get_morphism_instance(&self, ty: &SugaredMorphismType) -> Option<MorphismInstance2<M>> {
+ if let Some(path) = SugaredShortestPathProblem::new(self, ty.clone()).solve() {
+ if path.len() == 1 {
+ Some(path[0].clone())
+ } else {
+ Some(MorphismInstance2::Chain { path })
+ }
+ } else {
+ None
+ }
+ }
+
+ pub fn complex_morphism_decomposition(&self, src_type: &SugaredTypeTerm, dst_type: &SugaredTypeTerm) -> Option< MorphismInstance2<M> > {
+ let (src_ψ, src_floor) = src_type.get_floor_type();
+ let (dst_ψ, dst_floor) = dst_type.get_floor_type();
+
+ if !dst_ψ.is_empty() {
+ if !crate::unification_sugared::subtype_unify(&src_ψ, &dst_ψ).is_ok() {
+ return None;
+ }
+ }
+
+ match (src_floor, dst_floor) {
+ (SugaredTypeTerm::Struct{ struct_repr: struct_repr_lhs, members: members_lhs},
+ SugaredTypeTerm::Struct { struct_repr: _struct_repr_rhs, members: members_rhs })
+ => {
+ // todo: optimization: check if struct repr match
+
+ let mut member_morph = Vec::new();
+ let mut failed = false;
+ let mut necessary = false;
+
+ for SugaredStructMember{ symbol: symbol_rhs, ty: ty_rhs } in members_rhs.iter() {
+ let mut found_src_member = false;
+ for SugaredStructMember{ symbol: symbol_lhs, ty: ty_lhs } in members_lhs.iter() {
+ if symbol_rhs == symbol_lhs {
+ found_src_member = true;
+
+ if let Some(mm) = self.get_morphism_instance(&SugaredMorphismType { src_type: ty_lhs.clone(), dst_type: ty_rhs.clone() }) {
+ if ty_lhs != ty_rhs {
+ necessary = true;
+ }
+ member_morph.push((symbol_lhs.clone(), mm))
+ } else {
+ failed = true;
+ }
+ break;
+ }
+ }
+
+ // member of rhs not found in lhs
+ if ! found_src_member {
+ failed = true;
+ break;
+ }
+ }
+
+ if ! failed && necessary {
+ Some(MorphismInstance2::MapStruct {
+ ψ: src_ψ,
+ struct_repr: struct_repr_lhs.clone(),
+ member_morph
+ })
+ } else {
+ None
+ }
+ }
+
+
+ (SugaredTypeTerm::Seq{ seq_repr: seq_repr_lhs, items: items_lhs },
+ SugaredTypeTerm::Seq{ seq_repr: _seq_rerpr_rhs, items: items_rhs })
+ => {
+ //let mut item_morphs = Vec::new();
+
+ for (ty_lhs, ty_rhs) in items_lhs.iter().zip(items_rhs.iter()) {
+ if let Some(item_morph) = self.get_morphism_instance(&SugaredMorphismType{ src_type: ty_lhs.clone(), dst_type: ty_rhs.clone() }) {
+ return Some(MorphismInstance2::MapSeq { ψ: src_ψ, seq_repr: seq_repr_lhs.clone(), item_morph: Box::new(item_morph) });
+ }
+ break;
+ }
+ None
+ }
+
+ _ => {
+ None
+ }
+ }
+ }
+
+ pub fn enum_morphisms_from(&self, src_type: &SugaredTypeTerm) -> Vec< MorphismInstance2<M> > {
+ let mut morphs = Vec::new();
+
+ for m in self.morphisms.iter() {
+ let m_src_type = m.get_type().src_type;
+ let m_dst_type = m.get_type().dst_type;
+
+ /* 1. primitive morphisms */
+
+ // check if the given start type is compatible with the
+ // morphisms source type,
+ // i.e. check if `src_type` is a subtype of `m_src_type`
+ if let Ok((ψ, σ)) = crate::unification_sugared::subtype_unify(src_type, &m_src_type) {
+ morphs.push(MorphismInstance2::Primitive { ψ, σ, morph: m.clone() });
+ }
+
+ /* 2. check complex types */
+ if let Some(complex_morph) = self.complex_morphism_decomposition(src_type, &m_src_type) {
+ morphs.push(complex_morph);
+ }
+ }
+
+ morphs
+ }
+
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
diff --git a/src/morphism_path.rs b/src/morphism_path.rs
index 849603d..c67e0cc 100644
--- a/src/morphism_path.rs
+++ b/src/morphism_path.rs
@@ -39,10 +39,14 @@ impl<'a, M:Morphism+Clone> ShortestPathProblem<'a, M> {
pub fn solve(&mut self) -> Option< Vec<MorphismInstance<M>> > {
while ! self.queue.is_empty() {
+ /* take the shortest partial path and try to advance it by one step */
self.queue.sort_by( |p1,p2| p2.weight.cmp(&p1.weight));
if let Some(mut cur_path) = self.queue.pop() {
- if let Ok((halo, σ)) = crate::unification::subtype_unify( &cur_path.cur_type, &self.goal ) {
+
+ /* 1. Check if goal is already reached by the current path */
+
+ if let Ok((ψ, σ)) = crate::unification::subtype_unify( &cur_path.cur_type, &self.goal ) {
/* found path,
* now apply substitution and trim to variables in terms of each step
*/
@@ -78,6 +82,9 @@ impl<'a, M:Morphism+Clone> ShortestPathProblem<'a, M> {
return Some(cur_path.morphisms);
}
+ /* 2. Try to advance the path */
+ /* 2.1. Direct Morphisms */
+
//eprintln!("cur path (w ={}) : @ {:?}", cur_path.weight, cur_path.cur_type);//.clone().sugar(type_dict).pretty(type_dict, 0) );
for mut next_morph_inst in self.morphism_base.enum_morphisms(&cur_path.cur_type) {
let dst_type = next_morph_inst.get_type().dst_type;
@@ -125,6 +132,12 @@ impl<'a, M:Morphism+Clone> ShortestPathProblem<'a, M> {
self.queue.push(new_path);
}
}
+
+ /* 2.2. Try to decompose */
+ /* 2.2.1. Seq - Map */
+ /* 2.2.2. Struct - Map */
+ /* 2.2.3. Enum - Map */
+
}
}
None
diff --git a/src/morphism_path_sugared.rs b/src/morphism_path_sugared.rs
new file mode 100644
index 0000000..c2b6cf7
--- /dev/null
+++ b/src/morphism_path_sugared.rs
@@ -0,0 +1,108 @@
+use {
+ crate::{
+ dict::*,
+ morphism_sugared::{SugaredMorphism, SugaredMorphismType, MorphismInstance2},
+ morphism_base_sugared::SugaredMorphismBase,
+ substitution_sugared::SugaredSubstitution,
+ sugar::*, term::*,
+ }
+};
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+#[derive(Clone)]
+pub struct SugaredMorphismPath<M: SugaredMorphism + Clone> {
+ pub weight: u64,
+ pub cur_type: SugaredTypeTerm,
+ pub morphisms: Vec< MorphismInstance2<M> >
+}
+
+
+impl<M: SugaredMorphism+Clone> SugaredMorphismPath<M> {
+ fn apply_subst(&mut self, σ: &std::collections::HashMap<TypeID, SugaredTypeTerm>) {
+ for m in self.morphisms.iter_mut() {
+ m.apply_subst(σ);
+ }
+ }
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+pub struct SugaredShortestPathProblem<'a, M: SugaredMorphism + Clone> {
+ pub morphism_base: &'a SugaredMorphismBase<M>,
+ pub goal: SugaredTypeTerm,
+ queue: Vec< SugaredMorphismPath<M> >
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+impl<'a, M:SugaredMorphism+Clone> SugaredShortestPathProblem<'a, M> {
+ pub fn new(morphism_base: &'a SugaredMorphismBase<M>, ty: SugaredMorphismType) -> Self {
+ SugaredShortestPathProblem {
+ morphism_base,
+ queue: vec![
+ SugaredMorphismPath::<M> { weight: 0, cur_type: ty.src_type, morphisms: vec![] }
+ ],
+ goal: ty.dst_type
+ }
+ }
+
+ pub fn advance(&mut self, prev_path: &SugaredMorphismPath<M>, morph_inst: MorphismInstance2<M>) {
+ let dst_type = morph_inst.get_type().dst_type;
+ //eprintln!("try morph to {:?}", dst_type.clone());//.sugar(type_dict).pretty(type_dict, 0));
+
+ let mut creates_loop = false;
+
+ let mut new_path = prev_path.clone();
+ for n in new_path.morphisms.iter_mut() {
+ n.apply_subst(&morph_inst.get_subst());
+ }
+
+ for m in new_path.morphisms.iter() {
+ if m.get_type().src_type == dst_type {
+ creates_loop = true;
+ break;
+ }
+ }
+
+ if ! creates_loop {
+ new_path.weight += 1;//next_morph_inst.get_weight();
+ new_path.cur_type = dst_type;
+
+ new_path.morphisms.push(morph_inst);
+ self.queue.push(new_path);
+ }
+ }
+
+ pub fn solve(&mut self) -> Option< Vec<MorphismInstance2<M>> > {
+ while ! self.queue.is_empty() {
+ /* take the shortest partial path and try to advance it by one step */
+ self.queue.sort_by( |p1,p2| p2.weight.cmp(&p1.weight));
+ if let Some(mut cur_path) = self.queue.pop() {
+
+ /* 1. Check if goal is already reached by the current path */
+ if let Ok((_ψ, σ)) = crate::unification_sugared::subtype_unify( &cur_path.cur_type, &self.goal ) {
+ /* found path,
+ * now apply substitution and trim to variables in terms of each step
+ */
+ cur_path.apply_subst(&σ);
+ return Some(cur_path.morphisms);
+ }
+
+ /* 2. Try to advance current path */
+ else if let Some(complex_morph) =
+ self.morphism_base.complex_morphism_decomposition( &cur_path.cur_type, &self.goal )
+ {
+ self.advance(&cur_path, complex_morph);
+ } else {
+ for next_morph_inst in self.morphism_base.enum_morphisms_from(&cur_path.cur_type) {
+ self.advance(&cur_path, next_morph_inst);
+ }
+ }
+ }
+ }
+ None
+ }
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
diff --git a/src/morphism_sugared.rs b/src/morphism_sugared.rs
new file mode 100644
index 0000000..cd41216
--- /dev/null
+++ b/src/morphism_sugared.rs
@@ -0,0 +1,205 @@
+use {
+ crate::{
+ substitution_sugared::SugaredSubstitution,
+ sugar::{SugaredStructMember, SugaredTypeTerm},
+ unification::UnificationProblem,
+ unification_sugared::SugaredUnificationProblem,
+ unparser::*, TypeDict,
+ TypeID, TypeTerm
+ },
+ std::{collections::HashMap, u64}
+};
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct SugaredMorphismType {
+ pub src_type: SugaredTypeTerm,
+ pub dst_type: SugaredTypeTerm
+}
+
+pub trait SugaredMorphism : Sized {
+ fn get_type(&self) -> SugaredMorphismType;
+ fn weight(&self) -> u64 {
+ 1
+ }
+}
+
+#[derive(Clone)]
+pub enum MorphismInstance2<M: SugaredMorphism + Clone> {
+ Primitive{
+ ψ: SugaredTypeTerm,
+ σ: HashMap<TypeID, SugaredTypeTerm>,
+ morph: M,
+ },
+ Chain{
+ path: Vec<MorphismInstance2<M>>
+ },
+ MapSeq{
+ ψ: SugaredTypeTerm,
+ seq_repr: Option<Box<SugaredTypeTerm>>,
+ item_morph: Box<MorphismInstance2<M>>,
+ },
+ MapStruct{
+ ψ: SugaredTypeTerm,
+ struct_repr: Option<Box<SugaredTypeTerm>>,
+ member_morph: Vec< (String, MorphismInstance2<M>) >
+ },
+ MapEnum{
+ ψ: SugaredTypeTerm,
+ enum_repr: Option<Box<SugaredTypeTerm>>,
+ variant_morph: Vec< (String, MorphismInstance2<M>) >
+ }
+}
+
+
+impl<M: SugaredMorphism + Clone> MorphismInstance2<M> {
+ pub fn get_type(&self) -> SugaredMorphismType {
+ match self {
+ MorphismInstance2::Primitive { ψ, σ, morph } => {
+ SugaredMorphismType {
+ src_type:
+ SugaredTypeTerm::Ladder(vec![
+ ψ.clone(),
+ morph.get_type().src_type
+ .apply_subst(σ).clone()
+ ]).strip(),
+
+ dst_type: SugaredTypeTerm::Ladder(vec![
+ ψ.clone(),
+ morph.get_type().dst_type
+ .apply_subst(σ).clone()
+ ]).strip(),
+ }
+ }
+ MorphismInstance2::Chain { path } => {
+ if path.len() > 0 {
+ SugaredMorphismType {
+ src_type: path.first().unwrap().get_type().src_type,
+ dst_type: path.last().unwrap().get_type().dst_type
+ }
+ } else {
+ SugaredMorphismType {
+ src_type: SugaredTypeTerm::TypeID(TypeID::Var(45454)),
+ dst_type: SugaredTypeTerm::TypeID(TypeID::Var(45454))
+ }
+ }
+ }
+ MorphismInstance2::MapSeq { ψ, seq_repr, item_morph } => {
+ SugaredMorphismType {
+ src_type: SugaredTypeTerm::Ladder(vec![
+ ψ.clone(),
+ SugaredTypeTerm::Seq{ seq_repr: seq_repr.clone(),
+ items: vec![ item_morph.get_type().src_type ]}
+ ]).strip(),
+ dst_type: SugaredTypeTerm::Ladder(vec![
+ ψ.clone(),
+ SugaredTypeTerm::Seq{ seq_repr: seq_repr.clone(),
+ items: vec![ item_morph.get_type().dst_type ]}
+ ]).strip()
+ }
+ }
+ MorphismInstance2::MapStruct { ψ, struct_repr, member_morph } => {
+ SugaredMorphismType {
+ src_type: SugaredTypeTerm::Ladder(vec![ ψ.clone(),
+ SugaredTypeTerm::Struct{
+ struct_repr: struct_repr.clone(),
+ members:
+ member_morph.iter().map(|(symbol, morph)| {
+ SugaredStructMember{ symbol:symbol.clone(), ty: morph.get_type().src_type }
+ }).collect()
+ }
+ ]).strip(),
+ dst_type: SugaredTypeTerm::Ladder(vec![ ψ.clone(),
+ SugaredTypeTerm::Struct{
+ struct_repr: struct_repr.clone(),
+ members: member_morph.iter().map(|(symbol, morph)| {
+ SugaredStructMember { symbol: symbol.clone(), ty: morph.get_type().dst_type}
+ }).collect()
+ }
+ ]).strip()
+ }
+ }
+ MorphismInstance2::MapEnum { ψ, enum_repr, variant_morph } => {
+ SugaredMorphismType {
+ src_type: SugaredTypeTerm::Ladder(vec![ ψ.clone(),
+ SugaredTypeTerm::Struct{
+ struct_repr: enum_repr.clone(),
+ members:
+ variant_morph.iter().map(|(symbol, morph)| {
+ SugaredStructMember{ symbol:symbol.clone(), ty: morph.get_type().src_type }
+ }).collect()
+ }
+ ]).strip(),
+ dst_type: SugaredTypeTerm::Ladder(vec![ ψ.clone(),
+ SugaredTypeTerm::Struct{
+ struct_repr: enum_repr.clone(),
+ members: variant_morph.iter().map(|(symbol, morph)| {
+ SugaredStructMember { symbol: symbol.clone(), ty: morph.get_type().dst_type}
+ }).collect()
+ }
+ ]).strip()
+ }
+ }
+ }
+ }
+
+ pub fn get_subst(&self) -> std::collections::HashMap< TypeID, SugaredTypeTerm > {
+ match self {
+ MorphismInstance2::Primitive { ψ, σ, morph } => σ.clone(),
+ MorphismInstance2::Chain { path } => {
+ path.iter().fold(
+ std::collections::HashMap::new(),
+ |mut σ, m| {
+ σ = σ.append(&m.get_subst());
+ σ
+ }
+ )
+ },
+ MorphismInstance2::MapSeq { ψ, seq_repr, item_morph } => {
+ item_morph.get_subst()
+ },
+ MorphismInstance2::MapStruct { ψ, struct_repr, member_morph } => {
+ let mut σ = HashMap::new();
+ for (symbol, m) in member_morph.iter() {
+ σ = σ.append(&mut m.get_subst());
+ }
+ σ
+ },
+ MorphismInstance2::MapEnum { ψ, enum_repr, variant_morph } => {
+ todo!();
+ HashMap::new()
+ },
+ }
+ }
+
+ pub fn apply_subst(&mut self, γ: &std::collections::HashMap< TypeID, SugaredTypeTerm >) {
+ match self {
+ MorphismInstance2::Primitive { ψ, σ, morph } => {
+ ψ.apply_subst(σ);
+ *σ = σ.clone().append(γ);
+ },
+ MorphismInstance2::Chain { path } => {
+ for n in path.iter_mut() {
+ n.apply_subst(γ);
+ }
+ }
+ MorphismInstance2::MapSeq { ψ, seq_repr, item_morph } => {
+ ψ.apply_subst(γ);
+ item_morph.apply_subst(γ);
+ }
+ MorphismInstance2::MapStruct { ψ, struct_repr, member_morph } => {
+ for (_,ty) in member_morph {
+ ty.apply_subst(γ);
+ }
+ },
+ MorphismInstance2::MapEnum { ψ, enum_repr, variant_morph } => {
+ for (_,ty) in variant_morph {
+ ty.apply_subst(γ);
+ }
+ }
+ }
+ }
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
diff --git a/src/pnf_sugared.rs b/src/pnf_sugared.rs
new file mode 100644
index 0000000..f5a72d7
--- /dev/null
+++ b/src/pnf_sugared.rs
@@ -0,0 +1,161 @@
+use crate::{sugar::SugaredTypeTerm, SugaredEnumVariant, SugaredStructMember};
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+pub fn splice_ladders( mut upper: Vec< SugaredTypeTerm >, mut lower: Vec< SugaredTypeTerm > ) -> Vec< SugaredTypeTerm > {
+ for i in 0 .. upper.len() {
+ if upper[i] == lower[0] {
+ let mut result_ladder = Vec::<SugaredTypeTerm>::new();
+ result_ladder.append(&mut upper[0..i].iter().cloned().collect());
+ result_ladder.append(&mut lower);
+ return result_ladder;
+ }
+ }
+
+ upper.append(&mut lower);
+ upper
+}
+
+impl SugaredTypeTerm {
+ /// transmute type into Parameter-Normal-Form (PNF)
+ ///
+ /// Example:
+ /// ```ignore
+ /// <Seq <Digit 10>>~<Seq Char>
+ /// ⇒ <Seq <Digit 10>~Char>
+ /// ```
+ pub fn param_normalize(mut self) -> Self {
+
+ match self {
+ SugaredTypeTerm::Ladder(mut rungs) => {
+ if rungs.len() > 0 {
+ let mut new_rungs = Vec::new();
+ while let Some(bottom) = rungs.pop() {
+ if let Some(last_but) = rungs.last_mut() {
+ match (bottom, last_but) {
+ (SugaredTypeTerm::Spec(bot_args), SugaredTypeTerm::Spec(last_args)) => {
+ if bot_args.len() == last_args.len() {
+ let mut new_rung_params = Vec::new();
+ let mut require_break = false;
+
+ if bot_args.len() > 0 {
+ todo!();
+ /*
+ if let Ok(_idx) = last_args[0].is_syntactic_subtype_of(&bot_args[0]) {
+ for i in 0 .. bot_args.len() {
+
+ let spliced_type_ladder = splice_ladders(
+ last_args[i].clone().get_lnf_vec(),
+ bot_args[i].clone().get_lnf_vec()
+ );
+ let spliced_type =
+ if spliced_type_ladder.len() == 1 {
+ spliced_type_ladder[0].clone()
+ } else if spliced_type_ladder.len() > 1 {
+ SugaredTypeTerm::Ladder(spliced_type_ladder)
+ } else {
+ SugaredTypeTerm::unit()
+ };
+
+ new_rung_params.push( spliced_type.param_normalize() );
+ }
+
+ } else {
+ new_rung_params.push(
+ SugaredTypeTerm::Ladder(vec![
+ last_args[0].clone(),
+ bot_args[0].clone()
+ ])//.normalize()
+ );
+
+ for i in 1 .. bot_args.len() {
+ if let Ok(_idx) = last_args[i].is_syntactic_subtype_of(&bot_args[i]) {
+ let spliced_type_ladder = splice_ladders(
+ last_args[i].clone().get_lnf_vec(),
+ bot_args[i].clone().get_lnf_vec()
+ );
+ let spliced_type =
+ if spliced_type_ladder.len() == 1 {
+ spliced_type_ladder[0].clone()
+ } else if spliced_type_ladder.len() > 1 {
+ SugaredTypeTerm::Ladder(spliced_type_ladder)
+ } else {
+ SugaredTypeTerm::unit()
+ };
+
+ new_rung_params.push( spliced_type.param_normalize() );
+ } else {
+ new_rung_params.push( bot_args[i].clone() );
+ require_break = true;
+ }
+ }
+ }
+ */
+ }
+
+ if require_break {
+ new_rungs.push( SugaredTypeTerm::Spec(new_rung_params) );
+ } else {
+ rungs.pop();
+ rungs.push(SugaredTypeTerm::Spec(new_rung_params));
+ }
+
+ } else {
+ new_rungs.push( SugaredTypeTerm::Spec(bot_args) );
+ }
+ }
+ (bottom, last_buf) => {
+ new_rungs.push( bottom );
+ }
+ }
+ } else {
+ new_rungs.push( bottom );
+ }
+ }
+
+ new_rungs.reverse();
+
+ if new_rungs.len() > 1 {
+ SugaredTypeTerm::Ladder(new_rungs)
+ } else if new_rungs.len() == 1 {
+ new_rungs[0].clone()
+ } else {
+ SugaredTypeTerm::unit()
+ }
+ } else {
+ SugaredTypeTerm::unit()
+ }
+ }
+
+ SugaredTypeTerm::Spec(params) => {
+ SugaredTypeTerm::Spec(
+ params.into_iter()
+ .map(|p| p.param_normalize())
+ .collect())
+ }
+
+ SugaredTypeTerm::Seq { seq_repr, items } => SugaredTypeTerm::Seq {
+ seq_repr: if let Some(seq_repr) = seq_repr { Some(Box::new(seq_repr.param_normalize())) } else { None },
+ items: items.into_iter().map(|p| p.param_normalize()).collect()
+ },
+ SugaredTypeTerm::Struct { struct_repr, members } =>SugaredTypeTerm::Struct {
+ struct_repr: if let Some(struct_repr) = struct_repr { Some(Box::new(struct_repr.param_normalize())) } else { None },
+ members: members.into_iter()
+ .map(|SugaredStructMember{symbol, ty}|
+ SugaredStructMember{ symbol, ty: ty.param_normalize() })
+ .collect()
+ },
+ SugaredTypeTerm::Enum{ enum_repr, variants } => SugaredTypeTerm::Enum{
+ enum_repr: if let Some(enum_repr) = enum_repr { Some(Box::new(enum_repr.param_normalize())) } else { None },
+ variants: variants.into_iter()
+ .map(|SugaredEnumVariant{symbol, ty}|
+ SugaredEnumVariant{ symbol, ty: ty.param_normalize() })
+ .collect()
+ },
+
+ atomic => atomic
+ }
+ }
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
diff --git a/src/pretty.rs b/src/pretty.rs
index 47f85f7..c3cc103 100644
--- a/src/pretty.rs
+++ b/src/pretty.rs
@@ -5,18 +5,18 @@ use {
impl SugaredStructMember {
- pub fn pretty(&self, dict: &TypeDict, indent: u64) -> String {
+ pub fn pretty(&self, dict: &impl TypeDict, indent: u64) -> String {
format!("{}: {}", self.symbol, self.ty.pretty(dict, indent+1))
}
}
impl SugaredEnumVariant {
- pub fn pretty(&self, dict: &TypeDict, indent: u64) -> String {
+ pub fn pretty(&self, dict: &impl TypeDict, indent: u64) -> String {
format!("{}: {}", self.symbol, self.ty.pretty(dict, indent+1))
}
}
impl SugaredTypeTerm {
- pub fn pretty(&self, dict: &TypeDict, indent: u64) -> String {
+ pub fn pretty(&self, dict: &impl TypeDict, indent: u64) -> String {
let indent_width = 4;
match self {
SugaredTypeTerm::TypeID(id) => {
@@ -64,15 +64,20 @@ impl SugaredTypeTerm {
s
}
- SugaredTypeTerm::Struct(args) => {
+ SugaredTypeTerm::Struct{ struct_repr, members } => {
let mut s = String::new();
s.push_str(&"{".yellow().bold());
- for arg in args {
+
+ if let Some(struct_repr) = struct_repr {
+ s.push_str(&format!("{}{} ", "~".yellow(), struct_repr.pretty(dict, indent+1)));
+ }
+
+ for member in members {
s.push('\n');
for x in 0..(indent+1)*indent_width {
s.push(' ');
}
- s.push_str(&arg.pretty(dict, indent + 1));
+ s.push_str(&member.pretty(dict, indent + 1));
s.push_str(&";\n".bright_yellow());
}
@@ -84,11 +89,16 @@ impl SugaredTypeTerm {
s
}
- SugaredTypeTerm::Enum(args) => {
+ SugaredTypeTerm::Enum{ enum_repr, variants } => {
let mut s = String::new();
s.push_str(&"(".yellow().bold());
- for i in 0..args.len() {
- let arg = &args[i];
+
+ if let Some(enum_repr) = enum_repr {
+ s.push_str(&format!("{}{} ", "~".yellow(), enum_repr.pretty(dict, indent+1)));
+ }
+
+
+ for (i,variant) in variants.iter().enumerate() {
s.push('\n');
for x in 0..(indent+1)*indent_width {
s.push(' ');
@@ -96,7 +106,7 @@ impl SugaredTypeTerm {
if i > 0 {
s.push_str(&"| ".yellow().bold());
}
- s.push_str(&arg.pretty(dict, indent + 1));
+ s.push_str(&variant.pretty(dict, indent + 1));
}
s.push('\n');
@@ -107,15 +117,20 @@ impl SugaredTypeTerm {
s
}
- SugaredTypeTerm::Seq(args) => {
+ SugaredTypeTerm::Seq{ seq_repr, items } => {
let mut s = String::new();
- s.push_str(&"[ ".yellow().bold());
- for i in 0..args.len() {
- let arg = &args[i];
+ s.push_str(&"[".yellow().bold());
+
+ if let Some(seq_repr) = seq_repr {
+ s.push_str(&format!("{}{}", "~".yellow(), seq_repr.pretty(dict, indent+1)));
+ }
+ s.push(' ');
+
+ for (i, item) in items.iter().enumerate() {
if i > 0 {
s.push(' ');
}
- s.push_str(&arg.pretty(dict, indent+1));
+ s.push_str(&item.pretty(dict, indent+1));
}
s.push_str(&" ]".yellow().bold());
s
diff --git a/src/substitution.rs b/src/substitution.rs
index b0f70ff..09935d0 100644
--- a/src/substitution.rs
+++ b/src/substitution.rs
@@ -60,3 +60,5 @@ impl TypeTerm {
self
}
}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
diff --git a/src/substitution_sugared.rs b/src/substitution_sugared.rs
new file mode 100644
index 0000000..1386e35
--- /dev/null
+++ b/src/substitution_sugared.rs
@@ -0,0 +1,114 @@
+
+use std::ops::DerefMut;
+use crate::{
+ TypeID,
+ TypeTerm
+};
+use crate::sugar::*;
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+pub trait SugaredSubstitution {
+ fn get(&self, t: &TypeID) -> Option< SugaredTypeTerm >;
+ fn add(&mut self, tyid: TypeID, val: SugaredTypeTerm);
+ fn append(self, rhs: &Self) -> Self;
+}
+
+impl SugaredSubstitution for std::collections::HashMap< TypeID, SugaredTypeTerm > {
+ fn get(&self, t: &TypeID) -> Option< SugaredTypeTerm > {
+ (self as &std::collections::HashMap< TypeID, SugaredTypeTerm >).get(t).cloned()
+ }
+
+ fn add(&mut self, tyid: TypeID, val: SugaredTypeTerm) {
+ if let TypeID::Var(id) = tyid {
+ if !val.contains_var(id) {
+ self.insert(tyid, val);
+ } else {
+ eprintln!("substitution cannot contain loop");
+ }
+ }
+ }
+
+ fn append(self, rhs: &Self) -> Self {
+ let mut new_σ = std::collections::HashMap::new();
+ for (v, tt) in self.iter() {
+ let mut tt = tt.clone();
+ tt.apply_subst(rhs);
+ tt.apply_subst(&self);
+ new_σ.add(v.clone(), tt);
+ }
+ for (v, tt) in rhs.iter() {
+ new_σ.add(v.clone(), tt.clone());
+ }
+
+ new_σ
+ }
+}
+
+impl SugaredTypeTerm {
+ /// recursively apply substitution to all subterms,
+ /// which will replace all occurences of variables which map
+ /// some type-term in `subst`
+ pub fn apply_substitution(
+ &mut self,
+ σ: &impl SugaredSubstitution
+ ) -> &mut Self {
+ self.apply_subst(σ)
+ }
+
+ pub fn apply_subst(
+ &mut self,
+ σ: &impl SugaredSubstitution
+ ) -> &mut Self {
+ match self {
+ SugaredTypeTerm::Num(_) => {},
+ SugaredTypeTerm::Char(_) => {},
+
+ SugaredTypeTerm::TypeID(typid) => {
+ if let Some(t) = σ.get(typid) {
+ *self = t;
+ }
+ }
+ SugaredTypeTerm::Ladder(args) |
+ SugaredTypeTerm::Spec(args) |
+ SugaredTypeTerm::Func(args) |
+ SugaredTypeTerm::Morph(args)
+ => {
+ for r in args.iter_mut() {
+ r.apply_subst(σ);
+ }
+ }
+
+ SugaredTypeTerm::Univ(t) => { t.apply_subst(σ); }
+
+ SugaredTypeTerm::Struct { struct_repr, members } => {
+ if let Some(struct_repr) = struct_repr.as_mut() {
+ struct_repr.apply_subst(σ);
+ }
+ for SugaredStructMember{ symbol:_, ty } in members.iter_mut() {
+ ty.apply_subst(σ);
+ }
+ },
+ SugaredTypeTerm::Enum { enum_repr, variants } => {
+ if let Some(enum_repr) = enum_repr.as_mut() {
+ enum_repr.apply_subst(σ);
+ }
+ for SugaredEnumVariant{ symbol:_, ty } in variants.iter_mut() {
+ ty.apply_subst(σ);
+ }
+ }
+ SugaredTypeTerm::Seq { seq_repr, items } => {
+ if let Some(seq_repr) = seq_repr {
+ seq_repr.apply_subst(σ);
+ }
+ for ty in items.iter_mut() {
+ ty.apply_subst(σ);
+ }
+ },
+ }
+
+ self
+ }
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
diff --git a/src/subtype.rs b/src/subtype.rs
index 8c46752..6843160 100644
--- a/src/subtype.rs
+++ b/src/subtype.rs
@@ -2,7 +2,7 @@ use crate::term::TypeTerm;
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
-impl TypeTerm {
+impl TypeTerm {
// returns ladder-step of first match and provided representation-type
pub fn is_semantic_subtype_of(&self, expected_type: &TypeTerm) -> Option<(usize, TypeTerm)> {
let provided_lnf = self.clone().get_lnf_vec();
@@ -49,3 +49,28 @@ impl TypeTerm {
}
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+use crate::sugar::*;
+
+impl SugaredTypeTerm {
+ pub fn is_compatible(&self, supertype: SugaredTypeTerm) -> bool {
+ match (self, supertype) {
+ (SugaredTypeTerm::TypeID(idl), SugaredTypeTerm::TypeID(idr)) => {
+ if *idl == idr {
+ true
+ } else {
+ false
+ }
+ }
+
+
+ (SugaredTypeTerm::Ladder(l_rungs), SugaredTypeTerm::Ladder(r_rungs)) => {
+ false
+ }
+
+ _ => {
+ false
+ }
+ }
+ }
+}
diff --git a/src/sugar.rs b/src/sugar.rs
index aa1ff4e..eef8dee 100644
--- a/src/sugar.rs
+++ b/src/sugar.rs
@@ -1,20 +1,20 @@
use {
- crate::{parser::ParseLadderType, TypeDict, TypeID, TypeTerm}
+ crate::{parser::ParseLadderType, subtype_unify, TypeDict, TypeID, TypeTerm}
};
-#[derive(Clone, PartialEq)]
+#[derive(Clone, PartialEq, Eq, Debug)]
pub struct SugaredStructMember {
pub symbol: String,
pub ty: SugaredTypeTerm
}
-#[derive(Clone, PartialEq)]
+#[derive(Clone, PartialEq, Eq, Debug)]
pub struct SugaredEnumVariant {
pub symbol: String,
pub ty: SugaredTypeTerm
}
-#[derive(Clone, PartialEq)]
+#[derive(Clone, PartialEq, Eq, Debug)]
pub enum SugaredTypeTerm {
TypeID(TypeID),
Num(i64),
@@ -24,24 +24,37 @@ pub enum SugaredTypeTerm {
Func(Vec< SugaredTypeTerm >),
Morph(Vec< SugaredTypeTerm >),
Ladder(Vec< SugaredTypeTerm >),
- Struct(Vec< SugaredStructMember >),
- Enum(Vec< SugaredEnumVariant >),
- Seq(Vec< SugaredTypeTerm >)
+ Struct{
+ struct_repr: Option< Box<SugaredTypeTerm> >,
+ members: Vec< SugaredStructMember >
+ },
+ Enum{
+ enum_repr: Option<Box< SugaredTypeTerm >>,
+ variants: Vec< SugaredEnumVariant >
+ },
+ Seq{
+ seq_repr: Option<Box< SugaredTypeTerm >>,
+ items: Vec< SugaredTypeTerm >
+ },
+
+ /*
+ Todo: Ref, RefMut
+ */
}
impl SugaredStructMember {
pub fn parse( dict: &mut impl TypeDict, ty: &TypeTerm ) -> Option<Self> {
match ty {
TypeTerm::App(args) => {
- if args.len() != 3 {
+ if args.len() != 2 {
return None;
}
-
+/*
if args[0] != dict.parse("Struct.Field").expect("parse") {
return None;
}
-
- let symbol = match args[1] {
+*/
+ let symbol = match args[0] {
TypeTerm::Char(c) => c.to_string(),
TypeTerm::TypeID(id) => dict.get_typename(&id).expect("cant get member name"),
_ => {
@@ -49,7 +62,7 @@ impl SugaredStructMember {
}
};
- let ty = args[2].clone().sugar(dict);
+ let ty = args[1].clone().sugar(dict);
Some(SugaredStructMember { symbol, ty })
}
@@ -64,15 +77,15 @@ impl SugaredEnumVariant {
pub fn parse( dict: &mut impl TypeDict, ty: &TypeTerm ) -> Option<Self> {
match ty {
TypeTerm::App(args) => {
- if args.len() != 3 {
+ if args.len() != 2 {
return None;
}
-
+/*
if args[0] != dict.parse("Enum.Variant").expect("parse") {
return None;
}
-
- let symbol = match args[1] {
+*/
+ let symbol = match args[0] {
TypeTerm::Char(c) => c.to_string(),
TypeTerm::TypeID(id) => dict.get_typename(&id).expect("cant get member name"),
_ => {
@@ -80,7 +93,7 @@ impl SugaredEnumVariant {
}
};
- let ty = args[2].clone().sugar(dict);
+ let ty = args[1].clone().sugar(dict);
Some(SugaredEnumVariant { symbol, ty })
}
@@ -93,6 +106,10 @@ impl SugaredEnumVariant {
impl TypeTerm {
pub fn sugar(self: TypeTerm, dict: &mut impl crate::TypeDict) -> SugaredTypeTerm {
+ dict.add_varname("StructRepr".into());
+ dict.add_varname("EnumRepr".into());
+ dict.add_varname("SeqRepr".into());
+
match self {
TypeTerm::TypeID(id) => SugaredTypeTerm::TypeID(id),
TypeTerm::Num(n) => SugaredTypeTerm::Num(n),
@@ -105,13 +122,52 @@ impl TypeTerm {
SugaredTypeTerm::Morph( args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect() )
}
else if first == &dict.parse("Struct").unwrap() {
- SugaredTypeTerm::Struct( args[1..].into_iter().map(|t| SugaredStructMember::parse(dict, t).expect("cant parse field")).collect() )
+ SugaredTypeTerm::Struct{
+ struct_repr: None,
+ members: args[1..].into_iter()
+ .map(|t| SugaredStructMember::parse(dict, t).expect("cant parse field"))
+ .collect()
+ }
+ }
+ else if let Ok(σ) = crate::unify( first, &dict.parse("Struct ~ StructRepr").expect("") ) {
+ SugaredTypeTerm::Struct{
+ struct_repr: Some(Box::new(σ.get(&dict.get_typeid(&"StructRepr".into()).expect("")).unwrap().clone().sugar(dict))),
+ members: args[1..].into_iter()
+ .map(|t| SugaredStructMember::parse(dict, t).expect("cant parse field"))
+ .collect()
+ }
}
else if first == &dict.parse("Enum").unwrap() {
- SugaredTypeTerm::Enum( args[1..].into_iter().map(|t| SugaredEnumVariant::parse(dict, t).expect("cant parse variant")).collect() )
+ SugaredTypeTerm::Enum{
+ enum_repr: None,
+ variants: args[1..].into_iter()
+ .map(|t| SugaredEnumVariant::parse(dict, t).expect("cant parse variant"))
+ .collect()
+ }
+ }
+ else if let Ok(σ) = crate::unify( first, &dict.parse("Enum ~ EnumRepr").expect("") ) {
+ SugaredTypeTerm::Enum{
+ enum_repr: Some(Box::new(σ.get(&dict.get_typeid(&"EnumRepr".into()).expect("")).unwrap().clone().sugar(dict))),
+ variants: args[1..].into_iter()
+ .map(|t| SugaredEnumVariant::parse(dict, t).expect("cant parse variant"))
+ .collect()
+ }
}
else if first == &dict.parse("Seq").unwrap() {
- SugaredTypeTerm::Seq( args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect() )
+ SugaredTypeTerm::Seq {
+ seq_repr: None,
+ items: args[1..].into_iter()
+ .map(|t| t.clone().sugar(dict))
+ .collect()
+ }
+ }
+ else if let Ok(σ) = crate::unify( first, &dict.parse("Seq ~ SeqRepr").expect("") ) {
+ SugaredTypeTerm::Seq {
+ seq_repr: Some(Box::new(σ.get(&dict.get_typeid(&"SeqRepr".into()).expect("")).unwrap().clone().sugar(dict))),
+ items: args[1..].into_iter()
+ .map(|t| t.clone().sugar(dict))
+ .collect()
+ }
}
else if first == &dict.parse("Spec").unwrap() {
SugaredTypeTerm::Spec( args[1..].into_iter().map(|t| t.clone().sugar(dict)).collect() )
@@ -139,7 +195,7 @@ impl TypeTerm {
impl SugaredStructMember {
pub fn desugar(self, dict: &mut impl crate::TypeDict) -> TypeTerm {
TypeTerm::App(vec![
- dict.parse("Struct.Field").expect("parse"),
+ //dict.parse("Struct.Field").expect("parse"),
dict.parse(&self.symbol).expect("parse"),
self.ty.desugar(dict)
])
@@ -149,7 +205,7 @@ impl SugaredStructMember {
impl SugaredEnumVariant {
pub fn desugar(self, dict: &mut impl crate::TypeDict) -> TypeTerm {
TypeTerm::App(vec![
- dict.parse("Enum.Variant").expect("parse"),
+ //dict.parse("Enum.Variant").expect("parse"),
dict.parse(&self.symbol).expect("parse"),
self.ty.desugar(dict)
])
@@ -157,6 +213,10 @@ impl SugaredEnumVariant {
}
impl SugaredTypeTerm {
+ pub fn unit() -> Self {
+ SugaredTypeTerm::Ladder(vec![])
+ }
+
pub fn desugar(self, dict: &mut impl crate::TypeDict) -> TypeTerm {
match self {
SugaredTypeTerm::TypeID(id) => TypeTerm::TypeID(id),
@@ -173,21 +233,270 @@ impl SugaredTypeTerm {
std::iter::once( dict.parse("Morph").unwrap() ).chain(
ts.into_iter().map(|t| t.desugar(dict))
).collect()),
- SugaredTypeTerm::Struct(ts) => TypeTerm::App(
- std::iter::once( dict.parse("Struct").unwrap() ).chain(
- ts.into_iter().map(|t| t.desugar(dict))
+ SugaredTypeTerm::Struct{ struct_repr, members } => TypeTerm::App(
+ std::iter::once(
+ if let Some(sr) = struct_repr {
+ TypeTerm::Ladder(vec![
+ dict.parse("Struct").unwrap(),
+ sr.desugar(dict)
+ ])
+ } else {
+ dict.parse("Struct").unwrap()
+ }
+ ).chain(
+ members.into_iter().map(|t| t.desugar(dict))
).collect()),
- SugaredTypeTerm::Enum(ts) => TypeTerm::App(
+ SugaredTypeTerm::Enum{ enum_repr, variants } => TypeTerm::App(
std::iter::once( dict.parse("Enum").unwrap() ).chain(
- ts.into_iter().map(|t| t.desugar(dict))
+ variants.into_iter().map(|t| t.desugar(dict))
).collect()),
- SugaredTypeTerm::Seq(ts) => TypeTerm::App(
+ SugaredTypeTerm::Seq{ seq_repr, items } => TypeTerm::App(
std::iter::once( dict.parse("Seq").unwrap() ).chain(
- ts.into_iter().map(|t| t.desugar(dict))
+ items.into_iter().map(|t| t.desugar(dict))
).collect()),
}
}
+ pub fn contains_var(&self, var_id: u64) -> bool {
+ match self {
+ SugaredTypeTerm::TypeID(TypeID::Var(v)) => (&var_id == v),
+ SugaredTypeTerm::Spec(args) |
+ SugaredTypeTerm::Func(args) |
+ SugaredTypeTerm::Morph(args) |
+ SugaredTypeTerm::Ladder(args) => {
+ for a in args.iter() {
+ if a.contains_var(var_id) {
+ return true;
+ }
+ }
+ false
+ }
+ SugaredTypeTerm::Univ(t) => {
+ t.contains_var(var_id)
+ }
+ SugaredTypeTerm::Struct { struct_repr, members } => {
+ if let Some(struct_repr) = struct_repr {
+ if struct_repr.contains_var(var_id) {
+ return true;
+ }
+ }
+
+ for SugaredStructMember{ symbol, ty } in members {
+ if ty.contains_var(var_id) {
+ return true;
+ }
+ }
+ false
+ }
+ SugaredTypeTerm::Enum { enum_repr, variants } => {
+ if let Some(enum_repr) = enum_repr {
+ if enum_repr.contains_var(var_id) {
+ return true;
+ }
+ }
+
+ for SugaredEnumVariant{ symbol, ty } in variants {
+ if ty.contains_var(var_id) {
+ return true;
+ }
+ }
+ false
+ }
+ SugaredTypeTerm::Seq { seq_repr, items } => {
+ if let Some(seq_repr) = seq_repr {
+ if seq_repr.contains_var(var_id) {
+ return true;
+ }
+ }
+
+ for ty in items {
+ if ty.contains_var(var_id) {
+ return true;
+ }
+ }
+ false
+ }
+
+ SugaredTypeTerm::Num(_) |
+ SugaredTypeTerm::Char(_) |
+ SugaredTypeTerm::TypeID(TypeID::Fun(_)) => false
+ }
+ }
+
+ pub fn strip(self) -> SugaredTypeTerm {
+ if self.is_empty() {
+ return SugaredTypeTerm::unit();
+ }
+
+ match self {
+ SugaredTypeTerm::Ladder(rungs) => {
+ let mut rungs :Vec<_> = rungs.into_iter()
+ .filter_map(|mut r| {
+ r = r.strip();
+ if r != SugaredTypeTerm::unit() {
+ Some(match r {
+ SugaredTypeTerm::Ladder(r) => r,
+ a => vec![ a ]
+ })
+ }
+ else { None }
+ })
+ .flatten()
+ .collect();
+
+ if rungs.len() == 1 {
+ rungs.pop().unwrap()
+ } else {
+ SugaredTypeTerm::Ladder(rungs)
+ }
+ },
+ SugaredTypeTerm::Spec(args) => {
+ let mut args :Vec<_> = args.into_iter().map(|arg| arg.strip()).collect();
+ if args.len() == 0 {
+ SugaredTypeTerm::unit()
+ } else if args.len() == 1 {
+ args.pop().unwrap()
+ } else {
+ SugaredTypeTerm::Spec(args)
+ }
+ }
+ SugaredTypeTerm::Seq{ mut seq_repr, mut items } => {
+ if let Some(seq_repr) = seq_repr.as_mut() {
+ *seq_repr = Box::new(seq_repr.clone().strip());
+ }
+ for i in items.iter_mut() {
+ *i = i.clone().strip();
+ }
+
+ SugaredTypeTerm::Seq { seq_repr, items }
+ }
+ atom => atom
+ }
+ }
+
+
+ pub fn get_interface_type(&self) -> SugaredTypeTerm {
+ match self {
+ SugaredTypeTerm::Ladder(rungs) => {
+ if let Some(top) = rungs.first() {
+ top.get_interface_type()
+ } else {
+ SugaredTypeTerm::unit()
+ }
+ }
+ SugaredTypeTerm::Spec(args)
+ => SugaredTypeTerm::Spec(args.iter().map(|a| a.get_interface_type()).collect()),
+
+ SugaredTypeTerm::Func(args)
+ => SugaredTypeTerm::Func(args.iter().map(|a| a.get_interface_type()).collect()),
+
+ SugaredTypeTerm::Morph(args)
+ => SugaredTypeTerm::Spec(args.iter().map(|a| a.get_interface_type()).collect()),
+
+ SugaredTypeTerm::Univ(t)
+ => SugaredTypeTerm::Univ(Box::new(t.get_interface_type())),
+
+ SugaredTypeTerm::Seq { seq_repr, items } => {
+ SugaredTypeTerm::Seq {
+ seq_repr: if let Some(sr) = seq_repr {
+ Some(Box::new(sr.clone().get_interface_type()))
+ } else { None },
+ items: items.iter().map(|t| t.get_interface_type()).collect()
+ }
+ }
+ SugaredTypeTerm::Struct { struct_repr, members } => {
+ SugaredTypeTerm::Struct {
+ struct_repr: if let Some(sr) = struct_repr {
+ Some(Box::new(sr.clone().get_interface_type()))
+ } else { None },
+ members: members.iter()
+ .map(|SugaredStructMember{symbol,ty}|
+ SugaredStructMember {symbol:symbol.clone(), ty:ty.get_interface_type() })
+ .collect()
+ }
+ }
+ SugaredTypeTerm::Enum { enum_repr, variants } => {
+ SugaredTypeTerm::Enum {
+ enum_repr: if let Some(sr) = enum_repr {
+ Some(Box::new(sr.clone().get_interface_type()))
+ } else { None },
+ variants: variants.iter()
+ .map(|SugaredEnumVariant{symbol,ty}|
+ SugaredEnumVariant{ symbol:symbol.clone(), ty:ty.get_interface_type() })
+ .collect()
+ }
+ }
+
+ SugaredTypeTerm::TypeID(tyid) => SugaredTypeTerm::TypeID(tyid.clone()),
+ SugaredTypeTerm::Num(n) => SugaredTypeTerm::Num(*n),
+ SugaredTypeTerm::Char(c) => SugaredTypeTerm::Char(*c)
+ }
+ }
+
+ pub fn get_floor_type(&self) -> (SugaredTypeTerm, SugaredTypeTerm) {
+ match self.clone() {
+ SugaredTypeTerm::Ladder(mut rungs) => {
+ if let Some(bot) = rungs.pop() {
+ let (bot_ψ, bot_floor) = bot.get_floor_type();
+ rungs.push(bot_ψ);
+ (SugaredTypeTerm::Ladder(rungs).strip(), bot_floor.strip())
+ } else {
+ (SugaredTypeTerm::unit(), SugaredTypeTerm::unit())
+ }
+ }
+ /*
+ SugaredTypeTerm::Spec(args)
+ => (SugaredTypeTerm::SugaredTypeTerm::Spec(args.iter().map(|a| a.get_floor_type()).collect()),
+
+ SugaredTypeTerm::Func(args)
+ => SugaredTypeTerm::Func(args.iter().map(|a| a.get_floor_type()).collect()),
+
+ SugaredTypeTerm::Morph(args)
+ => SugaredTypeTerm::Spec(args.iter().map(|a| a.get_floor_type()).collect()),
+
+ SugaredTypeTerm::Univ(t)
+ => SugaredTypeTerm::Univ(Box::new(t.get_floor_type())),
+
+ SugaredTypeTerm::Seq { seq_repr, items } => {
+ SugaredTypeTerm::Seq {
+ seq_repr: if let Some(sr) = seq_repr {
+ Some(Box::new(sr.clone().get_floor_type()))
+ } else { None },
+ items: items.iter().map(|t| t.get_floor_type()).collect()
+ }
+ }
+ SugaredTypeTerm::Struct { struct_repr, members } => {
+ SugaredTypeTerm::Struct {
+ struct_repr: if let Some(sr) = struct_repr {
+ Some(Box::new(sr.clone().get_floor_type()))
+ } else { None },
+ members: members.iter()
+ .map(|SugaredStructMember{symbol,ty}|
+ SugaredStructMember {symbol:symbol.clone(), ty:ty.get_floor_type() })
+ .collect()
+ }
+ }
+ SugaredTypeTerm::Enum { enum_repr, variants } => {
+ SugaredTypeTerm::Enum {
+ enum_repr: if let Some(sr) = enum_repr {
+ Some(Box::new(sr.clone().get_floor_type()))
+ } else { None },
+ variants: variants.iter()
+ .map(|SugaredEnumVariant{symbol,ty}|
+ SugaredEnumVariant{ symbol:symbol.clone(), ty:ty.get_floor_type() })
+ .collect()
+ }
+ }
+
+ SugaredTypeTerm::TypeID(tyid) => SugaredTypeTerm::TypeID(tyid.clone()),
+ SugaredTypeTerm::Num(n) => SugaredTypeTerm::Num(*n),
+ SugaredTypeTerm::Char(c) => SugaredTypeTerm::Char(*c)
+ */
+
+ other => (SugaredTypeTerm::unit(), other.clone().strip())
+ }
+ }
+
pub fn is_empty(&self) -> bool {
match self {
SugaredTypeTerm::TypeID(_) => false,
@@ -197,16 +506,18 @@ impl SugaredTypeTerm {
SugaredTypeTerm::Spec(ts) |
SugaredTypeTerm::Ladder(ts) |
SugaredTypeTerm::Func(ts) |
- SugaredTypeTerm::Morph(ts) |
- SugaredTypeTerm::Seq(ts) => {
+ SugaredTypeTerm::Morph(ts) => {
ts.iter().fold(true, |s,t| s && t.is_empty() )
}
- SugaredTypeTerm::Struct(ts) => {
- ts.iter()
+ SugaredTypeTerm::Seq{ seq_repr, items } => {
+ items.iter().fold(true, |s,t| s && t.is_empty() )
+ }
+ SugaredTypeTerm::Struct{ struct_repr, members } => {
+ members.iter()
.fold(true, |s,member_decl| s && member_decl.ty.is_empty() )
}
- SugaredTypeTerm::Enum(ts) => {
- ts.iter()
+ SugaredTypeTerm::Enum{ enum_repr, variants } => {
+ variants.iter()
.fold(true, |s,variant_decl| s && variant_decl.ty.is_empty() )
}
}
diff --git a/src/test/unification.rs b/src/test/unification.rs
index 99ea7ed..ae99a18 100644
--- a/src/test/unification.rs
+++ b/src/test/unification.rs
@@ -336,14 +336,14 @@ pub fn test_subtype_delim() {
UnificationProblem::new_sub(vec![
(
- //given type
+ // given type
dict.parse("
< Seq <Seq <Digit 10>~Char~Ascii~UInt8> >
~ < ValueSep ':' Char~Ascii~UInt8 >
~ < Seq~<LengthPrefix UInt64> Char~Ascii~UInt8 >
").expect(""),
- //expected type
+ // expected type
dict.parse("
< Seq <Seq T> >
~ < ValueSep Delim T >
@@ -378,3 +378,78 @@ pub fn test_subtype_delim() {
))
);
}
+
+
+
+use crate::{sugar::*, unification_sugared::{SugaredUnificationPair, SugaredUnificationProblem}};
+
+#[test]
+fn test_list_subtype_sugared() {
+ let mut dict = BimapTypeDict::new();
+
+ dict.add_varname("Item".into());
+
+ let subtype_constraints = vec![
+ SugaredUnificationPair::new(
+ dict.parse("<List~Vec <Digit 10>~Char~ReprTree>").expect("").sugar(&mut dict),
+ dict.parse("<List~Vec Item~ReprTree>").expect("").sugar(&mut dict)
+ )
+ ];
+
+ assert_eq!(
+ SugaredUnificationProblem::new_sub(&mut dict, subtype_constraints).solve(),
+ Ok((
+ vec![ SugaredTypeTerm::Ladder(vec![]) ],
+ vec![
+ (dict.get_typeid(&"Item".into()).unwrap(),
+ dict.parse("<Digit 10>~Char").unwrap().sugar(&mut dict))
+ ].into_iter().collect()
+ ))
+ );
+}
+
+
+#[test]
+pub fn test_subtype_delim_sugared() {
+ let mut dict = BimapTypeDict::new();
+
+ dict.add_varname(String::from("T"));
+ dict.add_varname(String::from("Delim"));
+
+ let subtype_constraints = vec![
+ SugaredUnificationPair::new(
+ dict.parse("
+ < Seq <Seq <Digit 10>~Char~Ascii~UInt8> >
+ ~ < ValueSep ':' Char~Ascii~UInt8 >
+ ~ < Seq~<LengthPrefix UInt64> Char~Ascii~UInt8 >
+ ").expect("").sugar(&mut dict),
+
+ dict.parse("
+ < Seq <Seq T> >
+ ~ < ValueSep Delim T >
+ ~ < Seq~<LengthPrefix UInt64> T >
+ ").expect("").sugar(&mut dict),
+ ),
+ SugaredUnificationPair::new(
+ dict.parse("T").expect("").sugar(&mut dict),
+ dict.parse("UInt8").expect("").sugar(&mut dict),
+ ),
+ ];
+
+ assert_eq!(
+ SugaredUnificationProblem::new_sub(&mut dict, subtype_constraints).solve(),
+ Ok((
+ // halo types for each rhs in the sub-equations
+ vec![
+ dict.parse("<Seq <Seq <Digit 10>>>").expect("").sugar(&mut dict),
+ dict.parse("Char~Ascii").expect("").sugar(&mut dict),
+ ],
+
+ // variable substitution
+ vec![
+ (dict.get_typeid(&"T".into()).unwrap(), dict.parse("Char~Ascii~UInt8").expect("").sugar(&mut dict)),
+ (dict.get_typeid(&"Delim".into()).unwrap(), SugaredTypeTerm::Char(':')),
+ ].into_iter().collect()
+ ))
+ );
+}
diff --git a/src/unification.rs b/src/unification.rs
index 32d45df..6cbe842 100644
--- a/src/unification.rs
+++ b/src/unification.rs
@@ -25,16 +25,19 @@ pub struct UnificationProblem {
σ: HashMap<TypeID, TypeTerm>,
upper_bounds: HashMap< u64, TypeTerm >,
lower_bounds: HashMap< u64, TypeTerm >,
+
equal_pairs: Vec<UnificationPair>,
subtype_pairs: Vec<UnificationPair>,
- trait_pairs: Vec<UnificationPair>
+ trait_pairs: Vec<UnificationPair>,
+ parallel_pairs: Vec<UnificationPair>
}
impl UnificationProblem {
pub fn new(
equal_pairs: Vec<(TypeTerm, TypeTerm)>,
subtype_pairs: Vec<(TypeTerm, TypeTerm)>,
- trait_pairs: Vec<(TypeTerm, TypeTerm)>
+ trait_pairs: Vec<(TypeTerm, TypeTerm)>,
+ parallel_pairs: Vec<(TypeTerm, TypeTerm)>
) -> Self {
UnificationProblem {
σ: HashMap::new(),
@@ -60,17 +63,24 @@ impl UnificationProblem {
addr: Vec::new()
}).collect(),
+ parallel_pairs: parallel_pairs.into_iter().map(|(lhs,rhs)|
+ UnificationPair{
+ lhs,rhs,
+ halo: TypeTerm::unit(),
+ addr: Vec::new()
+ }).collect(),
+
upper_bounds: HashMap::new(),
lower_bounds: HashMap::new(),
}
}
pub fn new_eq(eqs: Vec<(TypeTerm, TypeTerm)>) -> Self {
- UnificationProblem::new( eqs, Vec::new(), Vec::new() )
+ UnificationProblem::new( eqs, Vec::new(), Vec::new(), Vec::new() )
}
pub fn new_sub(subs: Vec<(TypeTerm, TypeTerm)>) -> Self {
- UnificationProblem::new( Vec::new(), subs, Vec::new() )
+ UnificationProblem::new( Vec::new(), subs, Vec::new(), Vec::new() )
}
@@ -527,4 +537,12 @@ pub fn subtype_unify(
unification.solve().map( |(halos,σ)| ( halos.first().cloned().unwrap_or(TypeTerm::unit()), σ) )
}
+pub fn parallel_unify(
+ t1: &TypeTerm,
+ t2: &TypeTerm
+) -> Result<(TypeTerm, HashMap<TypeID, TypeTerm>), UnificationError> {
+ let unification = UnificationProblem::new(vec![], vec![], vec![], vec![ (t1.clone(), t2.clone()) ]);
+ unification.solve().map( |(halos,σ)| ( halos.first().cloned().unwrap_or(TypeTerm::unit()), σ) )
+}
+
//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
diff --git a/src/unification_sugared.rs b/src/unification_sugared.rs
new file mode 100644
index 0000000..2e61e80
--- /dev/null
+++ b/src/unification_sugared.rs
@@ -0,0 +1,686 @@
+use {
+ crate::{dict::*, sugar::SugaredTypeTerm, term::*, SugaredEnumVariant, SugaredStructMember}, std::collections::HashMap
+};
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\
+
+#[derive(Clone, Eq, PartialEq, Debug)]
+pub struct SugaredUnificationError {
+ pub addr: Vec<usize>,
+ pub t1: SugaredTypeTerm,
+ pub t2: SugaredTypeTerm
+}
+
+#[derive(Clone)]
+pub struct SugaredUnificationPair {
+ addr: Vec<usize>,
+ lhs: SugaredTypeTerm,
+ rhs: SugaredTypeTerm,
+}
+
+impl SugaredUnificationPair {
+ pub fn new(lhs: SugaredTypeTerm, rhs: SugaredTypeTerm) -> Self {
+ SugaredUnificationPair {
+ lhs,rhs, addr:vec![]
+ }
+ }
+}
+
+pub struct SugaredUnificationProblem {
+ // dict: &'a Dict,
+
+ σ: HashMap<TypeID, SugaredTypeTerm>,
+ upper_bounds: HashMap< u64, SugaredTypeTerm >,
+ lower_bounds: HashMap< u64, SugaredTypeTerm >,
+
+ equal_pairs: Vec<SugaredUnificationPair>,
+ subtype_pairs: Vec<SugaredUnificationPair>,
+ trait_pairs: Vec<SugaredUnificationPair>,
+ parallel_pairs: Vec<SugaredUnificationPair>
+}
+
+impl SugaredUnificationProblem {
+ pub fn new(
+ // dict: &'a mut Dict,
+ equal_pairs: Vec<SugaredUnificationPair>,
+ subtype_pairs: Vec<SugaredUnificationPair>,
+ trait_pairs: Vec<SugaredUnificationPair>,
+ parallel_pairs: Vec<SugaredUnificationPair>
+ ) -> Self {
+ SugaredUnificationProblem {
+ // dict,
+ σ: HashMap::new(),
+
+ equal_pairs,
+ subtype_pairs,
+ trait_pairs,
+ parallel_pairs,
+
+ upper_bounds: HashMap::new(),
+ lower_bounds: HashMap::new(),
+ }
+ }
+
+ pub fn new_eq(eqs: Vec<SugaredUnificationPair>) -> Self {
+ SugaredUnificationProblem::new( eqs, Vec::new(), Vec::new(), Vec::new() )
+ }
+
+ pub fn new_sub( subs: Vec<SugaredUnificationPair>) -> Self {
+ SugaredUnificationProblem::new( Vec::new(), subs, Vec::new(), Vec::new() )
+ }
+
+ pub fn new_trait(traits: Vec<SugaredUnificationPair>) -> Self {
+ SugaredUnificationProblem::new( Vec::new(), Vec::new(), traits, Vec::new() )
+ }
+
+ pub fn new_parallel( parallels: Vec<SugaredUnificationPair>) -> Self {
+ SugaredUnificationProblem::new(Vec::new(), Vec::new(), Vec::new(), parallels )
+ }
+
+
+ /// update all values in substitution
+ pub fn reapply_subst(&mut self) {
+ let mut new_σ = HashMap::new();
+ for (v, tt) in self.σ.iter() {
+ let mut tt = tt.clone();
+ tt.apply_subst(&self.σ);
+ //eprintln!("update σ : {:?} --> {:?}", v, tt);
+ new_σ.insert(v.clone(), tt);
+ }
+ self.σ = new_σ;
+ }
+
+
+ pub fn eval_equation(&mut self, unification_pair: SugaredUnificationPair) -> Result<(), SugaredUnificationError> {
+ match (&unification_pair.lhs, &unification_pair.rhs) {
+ (SugaredTypeTerm::TypeID(TypeID::Var(varid)), t) |
+ (t, SugaredTypeTerm::TypeID(TypeID::Var(varid))) => {
+ if ! t.contains_var( *varid ) {
+ self.σ.insert(TypeID::Var(*varid), t.clone());
+ self.reapply_subst();
+ Ok(())
+ } else if t == &SugaredTypeTerm::TypeID(TypeID::Var(*varid)) {
+ Ok(())
+ } else {
+ Err(SugaredUnificationError{ addr: unification_pair.addr, t1: SugaredTypeTerm::TypeID(TypeID::Var(*varid)), t2: t.clone() })
+ }
+ }
+
+ (SugaredTypeTerm::TypeID(a1), SugaredTypeTerm::TypeID(a2)) => {
+ if a1 == a2 { Ok(()) } else { Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) }
+ }
+ (SugaredTypeTerm::Num(n1), SugaredTypeTerm::Num(n2)) => {
+ if n1 == n2 { Ok(()) } else { Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) }
+ }
+ (SugaredTypeTerm::Char(c1), SugaredTypeTerm::Char(c2)) => {
+ if c1 == c2 { Ok(()) } else { Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) }
+ }
+
+ (SugaredTypeTerm::Ladder(a1), SugaredTypeTerm::Ladder(a2)) |
+ (SugaredTypeTerm::Spec(a1), SugaredTypeTerm::Spec(a2)) => {
+ if a1.len() == a2.len() {
+ for (i, (x, y)) in a1.iter().cloned().zip(a2.iter().cloned()).enumerate().rev() {
+ let mut new_addr = unification_pair.addr.clone();
+ new_addr.push(i);
+ self.equal_pairs.push(
+ SugaredUnificationPair {
+ lhs: x,
+ rhs: y,
+ addr: new_addr
+ });
+ }
+ Ok(())
+ } else {
+ Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+ }
+ }
+
+ (SugaredTypeTerm::Seq{ seq_repr: lhs_seq_repr, items: lhs_items },
+ SugaredTypeTerm::Seq { seq_repr: rhs_seq_repr, items: rhs_items })
+ => {
+ // todo: unify seq reprü
+
+ if lhs_items.len() == rhs_items.len() {
+ for (i, (lhs_ty, rhs_ty)) in lhs_items.into_iter().zip(rhs_items.into_iter()).enumerate()
+ {
+ let mut new_addr = unification_pair.addr.clone();
+ new_addr.push(i);
+ self.equal_pairs.push( SugaredUnificationPair { addr: new_addr, lhs: lhs_ty.clone(), rhs: rhs_ty.clone() } );
+ }
+ Ok(())
+ } else {
+ Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+ }
+ }
+ (SugaredTypeTerm::Struct{ struct_repr: lhs_struct_repr, members: lhs_members },
+ SugaredTypeTerm::Struct{ struct_repr: rhs_struct_repr, members: rhs_members })
+ => {
+ // todo: unify struct repr
+
+ if lhs_members.len() == rhs_members.len() {
+ for (i,
+ (SugaredStructMember{ symbol: lhs_symbol, ty: lhs_ty},
+ SugaredStructMember{ symbol: rhs_symbol, ty: rhs_ty })
+ ) in
+ lhs_members.into_iter().zip(rhs_members.into_iter()).enumerate()
+ {
+ let mut new_addr = unification_pair.addr.clone();
+ new_addr.push(i);
+ self.equal_pairs.push( SugaredUnificationPair { addr: new_addr, lhs: lhs_ty.clone(), rhs: rhs_ty.clone() } );
+ }
+ Ok(())
+ } else {
+ Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+ }
+ }
+ (SugaredTypeTerm::Enum{ enum_repr: lhs_enum_repr, variants: lhs_variants },
+ SugaredTypeTerm::Enum{ enum_repr: rhs_enum_repr, variants: rhs_variants })
+ => {
+ // todo: unify enum repr
+
+ if lhs_variants.len() == rhs_variants.len() {
+ for (i,
+ (SugaredEnumVariant{ symbol: lhs_symbol, ty: lhs_ty },
+ SugaredEnumVariant{ symbol: rhs_symbol, ty: rhs_ty })
+ ) in
+ lhs_variants.into_iter().zip(rhs_variants.into_iter()).enumerate()
+ {
+ let mut new_addr = unification_pair.addr.clone();
+ new_addr.push(i);
+ self.equal_pairs.push( SugaredUnificationPair { addr: new_addr, lhs: lhs_ty.clone(), rhs: rhs_ty.clone() } );
+ }
+ Ok(())
+ } else {
+ Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+ }
+ }
+
+ _ => Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+ }
+ }
+
+
+
+ pub fn add_lower_subtype_bound(&mut self, v: u64, new_lower_bound: SugaredTypeTerm) -> Result<(),()> {
+
+ if new_lower_bound == SugaredTypeTerm::TypeID(TypeID::Var(v)) {
+ return Ok(());
+ }
+
+ if new_lower_bound.contains_var(v) {
+ // loop
+ return Err(());
+ }
+
+ if let Some(lower_bound) = self.lower_bounds.get(&v).cloned() {
+// eprintln!("var already exists. check max. type");
+ if let Ok(halo) = self.eval_subtype(
+ SugaredUnificationPair {
+ lhs: lower_bound.clone(),
+ rhs: new_lower_bound.clone(),
+ addr: vec![]
+ }
+ ) {
+// eprintln!("found more general lower bound");
+// eprintln!("set var {}'s lowerbound to {:?}", varid, t.clone());
+ // generalize variable type to supertype
+ self.lower_bounds.insert(v, new_lower_bound);
+ Ok(())
+ } else if let Ok(halo) = self.eval_subtype(
+ SugaredUnificationPair{
+ lhs: new_lower_bound,
+ rhs: lower_bound,
+ addr: vec![]
+ }
+ ) {
+// eprintln!("OK, is already larger type");
+ Ok(())
+ } else {
+// eprintln!("violated subtype restriction");
+ Err(())
+ }
+ } else {
+// eprintln!("set var {}'s lowerbound to {:?}", varid, t.clone());
+ self.lower_bounds.insert(v, new_lower_bound);
+ Ok(())
+ }
+ }
+
+
+ pub fn add_upper_subtype_bound(&mut self, v: u64, new_upper_bound: SugaredTypeTerm) -> Result<(),()> {
+ if new_upper_bound == SugaredTypeTerm::TypeID(TypeID::Var(v)) {
+ return Ok(());
+ }
+
+ if new_upper_bound.contains_var(v) {
+ // loop
+ return Err(());
+ }
+
+ if let Some(upper_bound) = self.upper_bounds.get(&v).cloned() {
+ if let Ok(_halo) = self.eval_subtype(
+ SugaredUnificationPair {
+ lhs: new_upper_bound.clone(),
+ rhs: upper_bound,
+ addr: vec![]
+ }
+ ) {
+ // found a lower upper bound
+ self.upper_bounds.insert(v, new_upper_bound);
+ Ok(())
+ } else {
+ Err(())
+ }
+ } else {
+ self.upper_bounds.insert(v, new_upper_bound);
+ Ok(())
+ }
+ }
+
+ pub fn eval_subtype(&mut self, unification_pair: SugaredUnificationPair) -> Result<
+ // ok: halo type
+ SugaredTypeTerm,
+ // error
+ SugaredUnificationError
+ > {
+ // eprintln!("eval_subtype {:?} <=? {:?}", unification_pair.lhs, unification_pair.rhs);
+ match (unification_pair.lhs.clone().strip(), unification_pair.rhs.clone().strip()) {
+
+ /*
+ Variables
+ */
+
+ (t, SugaredTypeTerm::TypeID(TypeID::Var(v))) => {
+ //eprintln!("t <= variable");
+ if self.add_lower_subtype_bound(v, t.clone()).is_ok() {
+ Ok(SugaredTypeTerm::unit())
+ } else {
+ Err(SugaredUnificationError{ addr: unification_pair.addr, t1: SugaredTypeTerm::TypeID(TypeID::Var(v)), t2: t })
+ }
+ }
+
+ (SugaredTypeTerm::TypeID(TypeID::Var(v)), t) => {
+ //eprintln!("variable <= t");
+ if self.add_upper_subtype_bound(v, t.clone()).is_ok() {
+ Ok(SugaredTypeTerm::unit())
+ } else {
+ Err(SugaredUnificationError{ addr: unification_pair.addr, t1: SugaredTypeTerm::TypeID(TypeID::Var(v)), t2: t })
+ }
+ }
+
+
+ /*
+ Atoms
+ */
+ (SugaredTypeTerm::TypeID(a1), SugaredTypeTerm::TypeID(a2)) => {
+ if a1 == a2 { Ok(SugaredTypeTerm::unit()) } else { Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs}) }
+ }
+ (SugaredTypeTerm::Num(n1), SugaredTypeTerm::Num(n2)) => {
+ if n1 == n2 { Ok(SugaredTypeTerm::unit()) } else { Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) }
+ }
+ (SugaredTypeTerm::Char(c1), SugaredTypeTerm::Char(c2)) => {
+ if c1 == c2 { Ok(SugaredTypeTerm::unit()) } else { Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs }) }
+ }
+
+ /*
+ Complex Types
+ */
+
+ (SugaredTypeTerm::Seq{ seq_repr: lhs_seq_repr, items: lhs_items },
+ SugaredTypeTerm::Seq { seq_repr: rhs_seq_repr, items: rhs_items })
+ => {
+ if lhs_items.len() == rhs_items.len() && lhs_items.len() > 0 {
+ let mut new_addr = unification_pair.addr.clone();
+ new_addr.push(0);
+ match self.eval_subtype( SugaredUnificationPair { addr: new_addr.clone(), lhs: lhs_items[0].clone(), rhs: rhs_items[0].clone() } ) {
+ Ok(ψ) => Ok(SugaredTypeTerm::Seq {
+ seq_repr: None, // <<- todo
+ items: vec![ψ]
+ }.strip()),
+ Err(e) => Err(SugaredUnificationError{
+ addr: new_addr,
+ t1: e.t1,
+ t2: e.t2,
+ })
+ }
+ } else {
+ Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+ }
+ }
+ (SugaredTypeTerm::Struct{ struct_repr: lhs_struct_repr, members: lhs_members },
+ SugaredTypeTerm::Struct{ struct_repr: rhs_struct_repr, members: rhs_members })
+ => {
+ if lhs_members.len() == rhs_members.len() {
+ let mut halo_members = Vec::new();
+ for (i,
+ (SugaredStructMember{ symbol: lhs_symbol, ty: lhs_ty},
+ SugaredStructMember{ symbol: rhs_symbol, ty: rhs_ty })
+ ) in
+ lhs_members.into_iter().zip(rhs_members.into_iter()).enumerate()
+ {
+ let mut new_addr = unification_pair.addr.clone();
+ new_addr.push(i);
+
+ let ψ = self.eval_subtype( SugaredUnificationPair { addr: new_addr, lhs: lhs_ty.clone(), rhs: rhs_ty.clone() } )?;
+ halo_members.push(SugaredStructMember { symbol: lhs_symbol, ty: ψ });
+ }
+ Ok(SugaredTypeTerm::Struct {
+ struct_repr: None,
+ members: halo_members
+ })
+ } else {
+ Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+ }
+ }
+ (SugaredTypeTerm::Enum{ enum_repr: lhs_enum_repr, variants: lhs_variants },
+ SugaredTypeTerm::Enum{ enum_repr: rhs_enum_repr, variants: rhs_variants })
+ => {
+ if lhs_variants.len() == rhs_variants.len() {
+ let mut halo_variants = Vec::new();
+ for (i,
+ (SugaredEnumVariant{ symbol: lhs_symbol, ty: lhs_ty },
+ SugaredEnumVariant{ symbol: rhs_symbol, ty: rhs_ty })
+ ) in
+ lhs_variants.into_iter().zip(rhs_variants.into_iter()).enumerate()
+ {
+ let mut new_addr = unification_pair.addr.clone();
+ new_addr.push(i);
+ let ψ = self.eval_subtype( SugaredUnificationPair { addr: new_addr, lhs: lhs_ty.clone(), rhs: rhs_ty.clone() } )?;
+ halo_variants.push(SugaredEnumVariant { symbol: lhs_symbol, ty: ψ });
+ }
+ Ok(SugaredTypeTerm::Enum {
+ enum_repr: None,
+ variants: halo_variants
+ })
+ } else {
+ Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+ }
+ }
+
+
+
+ /*
+ Ladders
+ */
+
+ (SugaredTypeTerm::Ladder(a1), SugaredTypeTerm::Ladder(a2)) => {
+
+ let mut l1_iter = a1.into_iter().enumerate().rev();
+ let mut l2_iter = a2.into_iter().rev();
+
+ let mut halo_ladder = Vec::new();
+
+ while let Some(rhs) = l2_iter.next() {
+ //eprintln!("take rhs = {:?}", rhs);
+ if let Some((i, lhs)) = l1_iter.next() {
+ //eprintln!("take lhs ({}) = {:?}", i, lhs);
+ let mut addr = unification_pair.addr.clone();
+ addr.push(i);
+ //eprintln!("addr = {:?}", addr);
+
+ match (lhs.clone(), rhs.clone()) {
+ (t, SugaredTypeTerm::TypeID(TypeID::Var(v))) => {
+
+ if self.add_upper_subtype_bound(v,t.clone()).is_ok() {
+ let mut new_upper_bound_ladder = vec![ t ];
+
+ if let Some(next_rhs) = l2_iter.next() {
+
+ // TODO
+ todo!();
+
+ } else {
+ // ladder of rhs is empty
+ // take everything
+
+ while let Some((i,t)) = l1_iter.next() {
+ new_upper_bound_ladder.push(t);
+ }
+ }
+
+ new_upper_bound_ladder.reverse();
+ if self.add_upper_subtype_bound(v, SugaredTypeTerm::Ladder(new_upper_bound_ladder)).is_ok() {
+ // ok
+ } else {
+ return Err(SugaredUnificationError {
+ addr,
+ t1: lhs,
+ t2: rhs
+ });
+ }
+ } else {
+ return Err(SugaredUnificationError {
+ addr,
+ t1: lhs,
+ t2: rhs
+ });
+ }
+ }
+ (lhs, rhs) => {
+ if let Ok(ψ) = self.eval_subtype(
+ SugaredUnificationPair {
+ lhs: lhs.clone(),
+ rhs: rhs.clone(),
+ addr:addr.clone(),
+ }
+ ) {
+ // ok.
+ //eprintln!("rungs are subtypes. continue");
+ halo_ladder.push(ψ);
+ } else {
+ return Err(SugaredUnificationError {
+ addr,
+ t1: lhs,
+ t2: rhs
+ });
+ }
+ }
+ }
+ } else {
+ // not a subtype,
+ return Err(SugaredUnificationError {
+ addr: vec![],
+ t1: unification_pair.lhs,
+ t2: unification_pair.rhs
+ });
+ }
+ }
+ //eprintln!("left ladder fully consumed");
+
+ for (i,t) in l1_iter {
+ //!("push {} to halo ladder", t.pretty(self.dict,0));
+ halo_ladder.push(t);
+ }
+ halo_ladder.reverse();
+ Ok(SugaredTypeTerm::Ladder(halo_ladder).strip())//.param_normalize())
+ },
+
+ (t, SugaredTypeTerm::Ladder(a1)) => {
+ Err(SugaredUnificationError{ addr: unification_pair.addr, t1: t, t2: SugaredTypeTerm::Ladder(a1) })
+ }
+
+ (SugaredTypeTerm::Ladder(mut a1), t) => {
+ if a1.len() > 0 {
+ let mut new_addr = unification_pair.addr.clone();
+ new_addr.push( a1.len() -1 );
+ if let Ok(halo) = self.eval_subtype(
+ SugaredUnificationPair {
+ lhs: a1.pop().unwrap(),
+ rhs: t.clone(),
+ addr: new_addr
+ }
+ ) {
+ a1.push(halo);
+ if a1.len() == 1 {
+ Ok(a1.pop().unwrap())
+ } else {
+ Ok(SugaredTypeTerm::Ladder(a1))
+ }
+ } else {
+ Err(SugaredUnificationError{ addr: unification_pair.addr, t1: SugaredTypeTerm::Ladder(a1), t2: t })
+ }
+ } else if t == SugaredTypeTerm::unit() {
+ Ok(SugaredTypeTerm::unit())
+ } else {
+ Err(SugaredUnificationError { addr: unification_pair.addr, t1: SugaredTypeTerm::unit(), t2: t })
+ }
+ }
+
+
+ /*
+ Application
+ */
+
+ (SugaredTypeTerm::Spec(a1), SugaredTypeTerm::Spec(a2)) => {
+ if a1.len() == a2.len() {
+ let mut halo_args = Vec::new();
+ let mut n_halos_required = 0;
+
+ for (i, (mut x, mut y)) in a1.iter().cloned().zip(a2.iter().cloned()).enumerate() {
+ let mut new_addr = unification_pair.addr.clone();
+ new_addr.push(i);
+
+ x = x.strip();
+
+// eprintln!("before strip: {:?}", y);
+ y = y.strip();
+// eprintln!("after strip: {:?}", y);
+// eprintln!("APP<> eval {:?} \n ?<=? {:?} ", x, y);
+
+ match self.eval_subtype(
+ SugaredUnificationPair {
+ lhs: x.clone(),
+ rhs: y.clone(),
+ addr: new_addr,
+ }
+ ) {
+ Ok(halo) => {
+ if halo == SugaredTypeTerm::unit() {
+ let mut y = y.clone();
+ y.apply_subst(&self.σ);
+ y = y.strip();
+
+ let top = y.get_interface_type();
+ // eprintln!("add top {}", top.pretty(self.dict, 0));
+ halo_args.push(top);
+ } else {
+ //println!("add halo {}", halo.pretty(self.dict, 0));
+ if n_halos_required > 0 {
+ let x = &mut halo_args[n_halos_required-1];
+ if let SugaredTypeTerm::Ladder(arg_rungs) = x {
+ let mut a = a2[n_halos_required-1].clone();
+ a.apply_subst(&self.σ);
+ arg_rungs.push(a.get_interface_type());
+ } else {
+ *x = SugaredTypeTerm::Ladder(vec![
+ x.clone(),
+ a2[n_halos_required-1].get_interface_type()
+ ]);
+
+ x.apply_subst(&self.σ);
+ }
+ }
+
+ halo_args.push(halo);
+ n_halos_required += 1;
+ }
+ },
+ Err(err) => { return Err(err); }
+ }
+ }
+
+ if n_halos_required > 0 {
+ //eprintln!("halo args : {:?}", halo_args);
+ Ok(SugaredTypeTerm::Spec(halo_args))
+ } else {
+ Ok(SugaredTypeTerm::unit())
+ }
+ } else {
+ Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+ }
+ }
+
+ _ => Err(SugaredUnificationError{ addr: unification_pair.addr, t1: unification_pair.lhs, t2: unification_pair.rhs })
+ }
+ }
+
+ pub fn solve(mut self) -> Result<(Vec<SugaredTypeTerm>, HashMap<TypeID, SugaredTypeTerm>), SugaredUnificationError> {
+ // solve equations
+ while let Some( mut equal_pair ) = self.equal_pairs.pop() {
+ equal_pair.lhs.apply_subst(&self.σ);
+ equal_pair.rhs.apply_subst(&self.σ);
+
+ self.eval_equation(equal_pair)?;
+ }
+
+ // solve subtypes
+// eprintln!("------ SOLVE SUBTYPES ---- ");
+ for mut subtype_pair in self.subtype_pairs.clone().into_iter() {
+ subtype_pair.lhs.apply_subst(&self.σ);
+ subtype_pair.rhs.apply_subst(&self.σ);
+ let _halo = self.eval_subtype( subtype_pair.clone() )?.strip();
+ }
+
+ // add variables from subtype bounds
+ for (var_id, t) in self.upper_bounds.iter() {
+// eprintln!("VAR {} upper bound {:?}", var_id, t);
+ self.σ.insert(TypeID::Var(*var_id), t.clone().strip());
+ }
+
+ for (var_id, t) in self.lower_bounds.iter() {
+// eprintln!("VAR {} lower bound {:?}", var_id, t);
+ self.σ.insert(TypeID::Var(*var_id), t.clone().strip());
+ }
+
+ self.reapply_subst();
+
+// eprintln!("------ MAKE HALOS -----");
+ let mut halo_types = Vec::new();
+ for mut subtype_pair in self.subtype_pairs.clone().into_iter() {
+ subtype_pair.lhs = subtype_pair.lhs.apply_subst(&self.σ).clone().strip();
+ subtype_pair.rhs = subtype_pair.rhs.apply_subst(&self.σ).clone().strip();
+
+ subtype_pair.lhs.apply_subst(&self.σ);
+ subtype_pair.rhs.apply_subst(&self.σ);
+
+ // eprintln!("find halo.\n lhs={}", subtype_pair.lhs.pretty(self.dict,0));
+ // eprintln!("rhs={}", subtype_pair.rhs.pretty(self.dict,0));
+
+ let halo = self.eval_subtype( subtype_pair.clone() )?.strip();
+ halo_types.push(halo);
+ }
+
+ // solve traits
+ while let Some( trait_pair ) = self.trait_pairs.pop() {
+ unimplemented!();
+ }
+
+ Ok((halo_types, self.σ))
+ }
+}
+
+pub fn unify(
+ t1: &SugaredTypeTerm,
+ t2: &SugaredTypeTerm
+) -> Result<HashMap<TypeID, SugaredTypeTerm>, SugaredUnificationError> {
+ let unification = SugaredUnificationProblem::new_eq(vec![ SugaredUnificationPair{ lhs: t1.clone(), rhs: t2.clone(), addr:vec![] } ]);
+ Ok(unification.solve()?.1)
+}
+
+pub fn subtype_unify(
+ t1: &SugaredTypeTerm,
+ t2: &SugaredTypeTerm
+) -> Result<(SugaredTypeTerm, HashMap<TypeID, SugaredTypeTerm>), SugaredUnificationError> {
+ let unification = SugaredUnificationProblem::new_sub(vec![ SugaredUnificationPair{ lhs: t1.clone(), rhs: t2.clone(), addr:vec![] } ]);
+ unification.solve().map( |(halos,σ)| ( halos.first().cloned().unwrap_or(SugaredTypeTerm::unit()), σ) )
+}
+
+pub fn parallel_unify(
+ t1: &SugaredTypeTerm,
+ t2: &SugaredTypeTerm
+) -> Result<(SugaredTypeTerm, HashMap<TypeID, SugaredTypeTerm>), SugaredUnificationError> {
+ let unification = SugaredUnificationProblem::new_parallel(vec![ SugaredUnificationPair{ lhs: t1.clone(), rhs: t2.clone(), addr:vec![] } ]);
+ unification.solve().map( |(halos,σ)| ( halos.first().cloned().unwrap_or(SugaredTypeTerm::unit()), σ) )
+}
+
+//<<<<>>>><<>><><<>><<<*>>><<>><><<>><<<<>>>>\\