Fix config inside adjust

src/driver/loader.rs

@@ -74,7 +74,7 @@ pub fn load_entry(config: &Config, name: &str, load: &mut Load) -> Result<(), St
             load.book.entrs.insert(Ident(name.clone()), new_book.entrs.get(&Ident(name.to_string())).unwrap().clone());
         }
 
-        for unbound in &new_book.get_unbounds() {
+        for unbound in &new_book.get_unbounds(config) {
             load_entry(config, &unbound.0, load)?;
         }
     }
@@ -90,7 +90,7 @@ pub fn load(config: &Config, name: &str) -> Result<Load, String> {
 
     load_entry(config, name, &mut load)?;
 
-    match load.book.adjust() {
+    match load.book.adjust(config) {
         Ok(book) => {
             load.book = book;
         }

src/lowering.rs

@@ -1,6 +1,7 @@
 pub mod adjust;
 pub mod load;
 
+use crate::driver::config::Config;
 use crate::lowering::load::load_newtype_cached;
 use crate::book::{Argument, Book, Entry, Rule};
 use crate::book::name::Ident;
@@ -11,7 +12,7 @@ use std::collections::{HashMap, HashSet};
 use std::rc::Rc;
 
 // The state that adjusts uses and update a term, book, rule or entry.
-pub struct UnboundState {
+pub struct UnboundState<'a> {
     // All the vars that are bound in the context.
     vars: Vec<Ident>,
     // TODO: Describe
@@ -19,14 +20,17 @@ pub struct UnboundState {
     // Definitions of types that are useful to the
     // "match" expression.
     types: HashMap<Ident, Rc<NewType>>,
+
+    config: &'a Config
 }
 
-impl UnboundState {
-    pub fn new(types: HashMap<Ident, Rc<NewType>>) -> UnboundState {
+impl<'a> UnboundState<'a> {
+    pub fn new(types: HashMap<Ident, Rc<NewType>>, config: &'a Config) -> UnboundState<'a> {
         UnboundState {
             vars: Vec::new(),
             unbound: HashSet::new(),
             types,
+            config
         }
     }
 }
@@ -34,8 +38,8 @@ impl UnboundState {
 pub trait Unbound {
     fn fill_unbound(&self, rhs: bool, state: &mut UnboundState);
 
-    fn get_unbounds(&self, types: HashMap<Ident, Rc<NewType>>) -> HashSet<Ident> {
-        let mut state = UnboundState::new(types);
+    fn get_unbounds(&self, types: HashMap<Ident, Rc<NewType>>, config: &Config) -> HashSet<Ident> {
+        let mut state = UnboundState::new(types, config);
         self.fill_unbound(false, &mut state);
         state.unbound
     }
@@ -117,7 +121,7 @@ impl Unbound for Term {
                 ..
             } => {
                 //println!("finding unbounds of match {} {}", tipo, name);
-                if let Ok(newtype) = load_newtype_cached(&mut state.types, tipo) {
+                if let Ok(newtype) = load_newtype_cached(state.config, &mut state.types, tipo) {
                     state.unbound.insert(Ident(format!("{}.match", tipo.clone())));
                     // Expr
                     expr.fill_unbound(rhs, state);
@@ -177,8 +181,8 @@ impl Unbound for Argument {
 }
 
 impl Book {
-    pub fn get_unbounds(&self) -> HashSet<Ident> {
-        let mut state = UnboundState::new(HashMap::new());
+    pub fn get_unbounds(&self, config: &Config) -> HashSet<Ident> {
+        let mut state = UnboundState::new(HashMap::new(), config);
         for name in &self.names {
             let entry = self.entrs.get(&Ident(name.clone())).unwrap();
             entry.fill_unbound(false, &mut state);

src/lowering/adjust.rs

@@ -3,6 +3,7 @@ use crate::book::new_type::NewType;
 use crate::book::span::{Localized, Span};
 use crate::book::term::Term;
 use crate::book::{Argument, Book, Entry, Rule};
+use crate::driver::config::Config;
 use crate::lowering::load::load_newtype_cached;
 
 use std::collections::HashMap;
@@ -39,16 +40,21 @@ pub struct AdjustState<'a> {
     // Definitions of types that are useful to the
     // "match" expression.
     types: HashMap<Ident, Rc<NewType>>,
+
+    // Configuration provided by the user. It's useful
+    // to load paths correctly.
+    config: &'a Config
 }
 
 impl<'a> AdjustState<'a> {
-    pub fn new(book: &'a Book) -> AdjustState<'a> {
+    pub fn new(book: &'a Book, config: &'a Config) -> AdjustState<'a> {
         AdjustState {
             book,
             eras: 0,
             holes: 0,
             vars: Vec::new(),
             types: HashMap::new(),
+            config,
         }
     }
 }
@@ -58,7 +64,7 @@ pub trait Adjust {
     where
         Self: Sized;
 
-    fn adjust_with_book(&self, book: &Book) -> Result<Self, AdjustError>
+    fn adjust_with_book(&self, book: &Book, config: &Config) -> Result<Self, AdjustError>
     where
         Self: Sized,
     {
@@ -70,6 +76,7 @@ pub trait Adjust {
                 holes: 0,
                 vars: Vec::new(),
                 types: HashMap::new(),
+                config
             },
         )
     }
@@ -332,7 +339,7 @@ impl Adjust for Term {
                 ref moti,
             } => {
                 let orig = *orig;
-                if let Ok(newtype) = load_newtype_cached(&mut state.types, tipo) {
+                if let Ok(newtype) = load_newtype_cached(state.config, &mut state.types, tipo) {
                     let mut args = vec![];
                     args.push(expr.clone());
                     args.push(Box::new(Term::Lam {
@@ -483,10 +490,10 @@ impl Adjust for Entry {
 }
 
 impl Book {
-    pub fn adjust(&mut self) -> Result<Self, AdjustError> {
+    pub fn adjust(&mut self, config: &Config) -> Result<Self, AdjustError> {
         let mut names = Vec::new();
         let mut entrs = HashMap::new();
-        let mut state = AdjustState::new(self);
+        let mut state = AdjustState::new(self, config);
 
         for name in &self.names {
             let ident = Ident(name.clone());

src/lowering/load.rs

@@ -1,17 +1,16 @@
 use crate::book::name::Ident;
 use crate::book::new_type::NewType;
 
+use crate::driver::config::Config;
 use crate::parser::new_type::read_newtype;
 use std::collections::HashMap;
 use std::path::Path;
 use std::rc::Rc;
-use std::env;
 
 // TODO: Remove this from the adjust layer. I think that we need to move it
 // to the driver.
-fn load_newtype(name: &Ident) -> Result<Box<NewType>, String> {
-
-    let path = env::var_os("KIND2_PATH").map(|x| x.into_string().unwrap()).unwrap_or("".to_string());
+fn load_newtype(config: &Config,name: &Ident) -> Result<Box<NewType>, String> {
+    let path = config.kind2_path.clone();
     let root = Path::new(&path).join(name.to_string().replace('.', "/"));
     let path = root.clone().join("_.type");
 
@@ -30,9 +29,9 @@ fn load_newtype(name: &Ident) -> Result<Box<NewType>, String> {
     Ok(newtype)
 }
 
-pub fn load_newtype_cached(cache: &mut HashMap<Ident, Rc<NewType>>, name: &Ident) -> Result<Rc<NewType>, String> {
+pub fn load_newtype_cached(config: &Config, cache: &mut HashMap<Ident, Rc<NewType>>, name: &Ident) -> Result<Rc<NewType>, String> {
     if !cache.contains_key(name) {
-        let newtype = Rc::new(*load_newtype(name)?);
+        let newtype = Rc::new(*load_newtype(config, name)?);
         cache.insert(name.clone(), newtype);
     }
     return Ok(cache.get(name).unwrap().clone());

src/main.rs

@@ -68,7 +68,7 @@ fn run_cli() -> Result<(), String> {
     let config = Config {
         no_high_line: cli_matches.no_high_line,
         color_output: cli_matches.color_output,
-        kind2_path: env::var_os("KIND2_PATH").map(|x| x.into_string().unwrap()).unwrap_or("".to_string())
+        kind2_path: env::var_os("KIND2_PATH").map(|x| x.into_string().unwrap()).unwrap_or_else(|| "".to_string())
     };
 
     match cli_matches.command {