Preliminary work for ConcreteType Hindley-Milner

pc2 · Nov 7, 2024 · 4db8d46 · 4db8d46
1 parent ac35308
commit 4db8d46
Show file tree

Hide file tree

Showing 9 changed files with 107 additions and 35 deletions.
diff --git a/src/codegen_fallback.rs b/src/codegen_fallback.rs
@@ -54,7 +54,7 @@ fn typ_to_declaration(mut typ: &ConcreteType, var_name: &str) -> String {
             }
         }
         ConcreteType::Array(_) => unreachable!("All arrays have been used up already"),
-        ConcreteType::Value(_) | ConcreteType::Unknown => unreachable!(),
+        ConcreteType::Value(_) | ConcreteType::Unknown(_) => unreachable!(),
     }
 }
 

diff --git a/src/instantiation/execute.rs b/src/instantiation/execute.rs
@@ -193,6 +193,7 @@ impl<'fl, 'l> InstantiationContext<'fl, 'l> {
         }
     }
 
+    /// TODO make builtins that depend on parameters
     fn get_named_constant_value(&self, cst_ref: &GlobalReference<ConstantUUID>) -> TypedValue {
         let linker_cst = &self.linker.constants[cst_ref.id];
 
@@ -489,7 +490,7 @@ impl<'fl, 'l> InstantiationContext<'fl, 'l> {
                 source,
                 original_instruction: submod_instance.original_instruction,
                 domain: domain.unwrap_physical(),
-                typ: ConcreteType::Unknown,
+                typ: ConcreteType::Unknown(self.type_substitutor.alloc()),
                 name: self.unique_name_producer.get_unique_name(format!("{}_{}", submod_instance.name, port_data.name)),
                 absolute_latency: CALCULATE_LATENCY_LATER,
             });
@@ -569,7 +570,7 @@ impl<'fl, 'l> InstantiationContext<'fl, 'l> {
         };
         Ok(self.wires.alloc(RealWire {
             name : self.unique_name_producer.get_unique_name(""),
-            typ: ConcreteType::Unknown,
+            typ: ConcreteType::Unknown(self.type_substitutor.alloc()),
             original_instruction,
             domain,
             source,

diff --git a/src/instantiation/mod.rs b/src/instantiation/mod.rs
@@ -8,6 +8,7 @@ mod unique_names;
 use unique_names::UniqueNames;
 
 use crate::prelude::*;
+use crate::typing::type_inference::{ConcreteTypeVariableIDMarker, TypeSubstitutor};
 
 use std::{cell::RefCell, collections::HashMap, rc::Rc};
 
@@ -277,6 +278,8 @@ struct InstantiationContext<'fl, 'l> {
     wires: FlatAlloc<RealWire, WireIDMarker>,
     submodules: FlatAlloc<SubModule, SubModuleIDMarker>,
 
+    type_substitutor: TypeSubstitutor<ConcreteType, ConcreteTypeVariableIDMarker>,
+
     // Used for Execution
     unique_name_producer: UniqueNames,
     condition_stack : Vec<ConditionStackElem>,
@@ -417,6 +420,7 @@ fn perform_instantiation(
             md,
             generation_state: md.link_info.instructions.map(|(_, _)| SubModuleOrWire::Unnasigned),
         },
+        type_substitutor: TypeSubstitutor::new(),
         condition_stack: Vec::new(),
         wires: FlatAlloc::new(),
         submodules: FlatAlloc::new(),

diff --git a/src/to_string.rs b/src/to_string.rs
@@ -93,7 +93,7 @@ impl ConcreteType {
                 )
             }
             ConcreteType::Value(v) => format!("{{concrete_type_{v}}}"),
-            ConcreteType::Unknown => format!("{{concrete_type_unknown}}"),
+            ConcreteType::Unknown(u) => format!("{{{u:?}}}"),
         }
     }
 }

diff --git a/src/typing/concrete_type.rs b/src/typing/concrete_type.rs
@@ -9,6 +9,8 @@ use crate::{
     value::Value,
 };
 
+use super::type_inference::ConcreteTypeVariableID;
+
 pub const BOOL_CONCRETE_TYPE: ConcreteType = ConcreteType::Named(get_builtin_type("bool"));
 pub const INT_CONCRETE_TYPE: ConcreteType = ConcreteType::Named(get_builtin_type("int"));
 
@@ -17,7 +19,7 @@ pub enum ConcreteType {
     Named(TypeUUID),
     Value(Value),
     Array(Box<(ConcreteType, ConcreteType)>),
-    Unknown
+    Unknown(ConcreteTypeVariableID)
 }
 
 /// Panics on Type Errors that should have been caught by [AbstractType]
@@ -103,7 +105,7 @@ impl ConcreteType {
                     && target_arr_size.type_compare(found_arr_size)
             }
             (ConcreteType::Value(lv), ConcreteType::Value(rv)) => lv == rv,
-            (ConcreteType::Unknown, _) | (_, ConcreteType::Unknown) => {
+            (ConcreteType::Unknown(_), _) | (_, ConcreteType::Unknown(_)) => {
                 todo!("Type Unification {self:?} {found:?}")
             }
             _ => false,
@@ -135,7 +137,7 @@ impl ConcreteType {
         linker_types: &TypVec,
         errors: &ErrorCollector,
     ) {
-        if *self == ConcreteType::Unknown {
+        if let ConcreteType::Unknown(_) = self {
             *self = source_type.clone();
         } else {
             self.check_type(source_type, span, linker_types, errors);

diff --git a/src/typing/type_inference.rs b/src/typing/type_inference.rs
@@ -3,15 +3,17 @@
 use std::cell::{OnceCell, RefCell};
 use std::fmt::Debug;
 use std::marker::PhantomData;
-use std::ops::Index;
+use std::ops::{Deref, DerefMut, Index};
 
 use crate::block_vector::{BlockVec, BlockVecIter};
 use crate::prelude::*;
 
 use crate::alloc::{UUIDAllocator, UUIDMarker, UUID};
+use crate::value::Value;
 
 use super::abstract_type::AbstractType;
 use super::abstract_type::DomainType;
+use super::concrete_type::ConcreteType;
 
 pub struct TypeVariableIDMarker;
 impl UUIDMarker for TypeVariableIDMarker {
@@ -25,6 +27,12 @@ impl UUIDMarker for DomainVariableIDMarker {
 }
 pub type DomainVariableID = UUID<DomainVariableIDMarker>;
 
+pub struct ConcreteTypeVariableIDMarker;
+impl UUIDMarker for ConcreteTypeVariableIDMarker {
+    const DISPLAY_NAME: &'static str = "concrete_type_variable_";
+}
+pub type ConcreteTypeVariableID = UUID<ConcreteTypeVariableIDMarker>;
+
 pub struct FailedUnification<MyType> {
     pub found: MyType,
     pub expected: MyType,
@@ -62,6 +70,14 @@ impl<MyType : HindleyMilner<VariableIDMarker>, VariableIDMarker : UUIDMarker> In
 
 
 impl<MyType : HindleyMilner<VariableIDMarker>+Clone, VariableIDMarker : UUIDMarker> TypeSubstitutor<MyType, VariableIDMarker> {
+    pub fn new() -> Self {
+        Self {
+            substitution_map: BlockVec::new(),
+            failed_unifications: RefCell::new(Vec::new()),
+            _ph: PhantomData
+        }
+    }
+
     pub fn init(variable_alloc : &UUIDAllocator<VariableIDMarker>) -> Self {
         Self {
             substitution_map: variable_alloc.into_iter().map(|_| OnceCell::new()).collect(),
@@ -143,9 +159,9 @@ pub enum HindleyMilnerInfo<TypeFuncIdent, VariableIDMarker : UUIDMarker> {
 }
 
 pub trait HindleyMilner<VariableIDMarker: UUIDMarker> : Sized {
-    type TypeFuncIdent : Eq;
+    type TypeFuncIdent<'slf> : Eq where Self : 'slf;
 
-    fn get_hm_info(&self) -> HindleyMilnerInfo<Self::TypeFuncIdent, VariableIDMarker>;
+    fn get_hm_info<'slf>(&'slf self) -> HindleyMilnerInfo<Self::TypeFuncIdent<'slf>, VariableIDMarker>;
 
     /// Iterate through all arguments and unify them
     /// 
@@ -169,7 +185,7 @@ pub enum AbstractTypeHMInfo {
 }
 
 impl HindleyMilner<TypeVariableIDMarker> for AbstractType {
-    type TypeFuncIdent = AbstractTypeHMInfo;
+    type TypeFuncIdent<'slf> = AbstractTypeHMInfo;
 
     fn get_hm_info(&self) -> HindleyMilnerInfo<AbstractTypeHMInfo, TypeVariableIDMarker> {
         match self {
@@ -205,7 +221,7 @@ impl HindleyMilner<TypeVariableIDMarker> for AbstractType {
 }
 
 impl HindleyMilner<DomainVariableIDMarker> for DomainType {
-    type TypeFuncIdent = DomainID;
+    type TypeFuncIdent<'slf> = DomainID;
 
     fn get_hm_info(&self) -> HindleyMilnerInfo<DomainID, DomainVariableIDMarker> {
         match self {
@@ -231,3 +247,52 @@ impl HindleyMilner<DomainVariableIDMarker> for DomainType {
         }
     }
 }
+
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub enum ConcreteTypeHMInfo<'slf> {
+    Named(TypeUUID),
+    Value(&'slf Value),
+    Array
+}
+
+
+impl HindleyMilner<ConcreteTypeVariableIDMarker> for ConcreteType {
+    type TypeFuncIdent<'slf> = ConcreteTypeHMInfo<'slf>;
+
+    fn get_hm_info(&self) -> HindleyMilnerInfo<ConcreteTypeHMInfo, ConcreteTypeVariableIDMarker> {
+        match self {
+            ConcreteType::Unknown(var_id) => HindleyMilnerInfo::TypeVar(*var_id),
+            ConcreteType::Named(named_id) => HindleyMilnerInfo::TypeFunc(ConcreteTypeHMInfo::Named(*named_id)),
+            ConcreteType::Value(v) => HindleyMilnerInfo::TypeFunc(ConcreteTypeHMInfo::Value(v)),
+            ConcreteType::Array(_) => HindleyMilnerInfo::TypeFunc(ConcreteTypeHMInfo::Array),
+        }
+    }
+
+    fn unify_all_args<F : FnMut(&Self, &Self) -> bool>(left : &Self, right : &Self, unify : &mut F) -> bool {
+        match (left, right) {
+            (ConcreteType::Named(na), ConcreteType::Named(nb)) => {assert!(*na == *nb); true}, // Already covered by get_hm_info
+            (ConcreteType::Array(arr_typ_1), ConcreteType::Array(arr_typ_2)) => {
+                let (arr_typ_1_arr, arr_typ_1_sz) = arr_typ_1.deref();
+                let (arr_typ_2_arr, arr_typ_2_sz) = arr_typ_2.deref();
+                unify(arr_typ_1_arr, arr_typ_2_arr) & unify(arr_typ_1_sz, arr_typ_2_sz)
+            }
+            (_, _) => unreachable!("All others should have been eliminated by get_hm_info check")
+        }
+    }
+
+    fn fully_substitute(&mut self, substitutor: &TypeSubstitutor<Self, ConcreteTypeVariableIDMarker>) -> Result<(), ()> {
+        match self {
+            ConcreteType::Named(_) | ConcreteType::Value(_) => Ok(()), // Already included in get_hm_info
+            ConcreteType::Array(arr_typ) => {
+                let (arr_typ, arr_sz) = arr_typ.deref_mut();
+                arr_typ.fully_substitute(substitutor)?;
+                arr_sz.fully_substitute(substitutor)
+            },
+            ConcreteType::Unknown(var) => {
+                *self = substitutor.substitution_map[var.get_hidden_value()].get().ok_or(())?.clone();
+                self.fully_substitute(substitutor)
+            }
+        }
+    }
+}
diff --git a/src/value.rs b/src/value.rs
@@ -211,7 +211,7 @@ impl ConcreteType {
                 }
                 Value::Array(arr.into_boxed_slice())
             }
-            ConcreteType::Value(_) | ConcreteType::Unknown => unreachable!(),
+            ConcreteType::Value(_) | ConcreteType::Unknown(_) => unreachable!(),
         }
     }