Apply solved metavars (#332)

* Extract meta var solving to method

* Zonk after solving meta vars and module checking

* Use destructoring let syntax in expression zonking

* Print metavar solutions when printing holes

* wip: Add check for unresolved metavars

* Fix check that metavars are resolved

lang/ast/src/decls.rs

@@ -25,6 +25,7 @@ use url::Url;
 use crate::ctx::LevelCtx;
 use crate::named::Named;
 use crate::shift_and_clone;
+use crate::ContainsMetaVars;
 use crate::Zonk;
 
 use super::exp::*;
@@ -414,6 +415,18 @@ impl Zonk for Decl {
     }
 }
 
+impl ContainsMetaVars for Decl {
+    fn contains_metavars(&self) -> bool {
+        match self {
+            Decl::Data(data) => data.contains_metavars(),
+            Decl::Codata(codata) => codata.contains_metavars(),
+            Decl::Def(def) => def.contains_metavars(),
+            Decl::Codef(codef) => codef.contains_metavars(),
+            Decl::Let(tl_let) => tl_let.contains_metavars(),
+        }
+    }
+}
+
 // Data
 //
 //
@@ -474,6 +487,14 @@ impl Zonk for Data {
     }
 }
 
+impl ContainsMetaVars for Data {
+    fn contains_metavars(&self) -> bool {
+        let Data { span: _, doc: _, name: _, attr: _, typ, ctors } = self;
+
+        typ.contains_metavars() || ctors.contains_metavars()
+    }
+}
+
 // Codata
 //
 //
@@ -534,6 +555,14 @@ impl Zonk for Codata {
     }
 }
 
+impl ContainsMetaVars for Codata {
+    fn contains_metavars(&self) -> bool {
+        let Codata { span: _, doc: _, name: _, attr: _, typ, dtors } = self;
+
+        typ.contains_metavars() || dtors.contains_metavars()
+    }
+}
+
 // Ctor
 //
 //
@@ -574,6 +603,14 @@ impl Zonk for Ctor {
     }
 }
 
+impl ContainsMetaVars for Ctor {
+    fn contains_metavars(&self) -> bool {
+        let Ctor { span: _, doc: _, name: _, params, typ } = self;
+
+        params.contains_metavars() || typ.contains_metavars()
+    }
+}
+
 // Dtor
 //
 //
@@ -617,6 +654,14 @@ impl Zonk for Dtor {
     }
 }
 
+impl ContainsMetaVars for Dtor {
+    fn contains_metavars(&self) -> bool {
+        let Dtor { span: _, doc: _, name: _, params, self_param, ret_typ } = self;
+
+        params.contains_metavars() || self_param.contains_metavars() || ret_typ.contains_metavars()
+    }
+}
+
 // Def
 //
 //
@@ -684,6 +729,17 @@ impl Zonk for Def {
     }
 }
 
+impl ContainsMetaVars for Def {
+    fn contains_metavars(&self) -> bool {
+        let Def { span: _, doc: _, name: _, attr: _, params, self_param, ret_typ, cases } = self;
+
+        params.contains_metavars()
+            || self_param.contains_metavars()
+            || ret_typ.contains_metavars()
+            || cases.contains_metavars()
+    }
+}
+
 // Codef
 //
 //
@@ -750,6 +806,14 @@ impl Zonk for Codef {
     }
 }
 
+impl ContainsMetaVars for Codef {
+    fn contains_metavars(&self) -> bool {
+        let Codef { span: _, doc: _, name: _, attr: _, params, typ, cases } = self;
+
+        params.contains_metavars() || typ.contains_metavars() || cases.contains_metavars()
+    }
+}
+
 // Let
 //
 //
@@ -805,6 +869,14 @@ impl Zonk for Let {
     }
 }
 
+impl ContainsMetaVars for Let {
+    fn contains_metavars(&self) -> bool {
+        let Let { span: _, doc: _, name: _, attr: _, params, typ, body } = self;
+
+        params.contains_metavars() || typ.contains_metavars() || body.contains_metavars()
+    }
+}
+
 // SelfParam
 //
 //
@@ -861,6 +933,15 @@ impl Zonk for SelfParam {
     }
 }
 
+impl ContainsMetaVars for SelfParam {
+    fn contains_metavars(&self) -> bool {
+        // Info is just a span here
+        let SelfParam { info: _, name: _, typ } = self;
+
+        typ.contains_metavars()
+    }
+}
+
 // Telescope
 //
 //
@@ -979,6 +1060,14 @@ impl Zonk for Telescope {
     }
 }
 
+impl ContainsMetaVars for Telescope {
+    fn contains_metavars(&self) -> bool {
+        let Telescope { params } = self;
+
+        params.contains_metavars()
+    }
+}
+
 #[cfg(test)]
 mod print_telescope_tests {
 
@@ -1132,6 +1221,15 @@ impl Print for Param {
 
 impl Zonk for Param {
     fn zonk(&mut self, meta_vars: &HashMap<MetaVar, MetaVarState>) -> Result<(), crate::ZonkError> {
-        self.typ.zonk(meta_vars)
+        let Param { implicit: _, name: _, typ } = self;
+        typ.zonk(meta_vars)
+    }
+}
+
+impl ContainsMetaVars for Param {
+    fn contains_metavars(&self) -> bool {
+        let Param { implicit: _, name: _, typ } = self;
+
+        typ.contains_metavars()
     }
 }