Make inline forget inlined defs and use strict parser to save memory.

dedukti-parse/examples/README.md

@@ -0,0 +1,23 @@
+When we have a theory with many definitions that are used exactly one
+(after having been declared), then we might want to eliminate these definitions
+by inlining them, so that the signature during type checking remains small.
+
+For this, we have to traverse our theory file twice:
+first to find out which definitions are used exactly once, and
+second to eliminate these definitions and to inline them.
+
+The first step is done by `symcount`.
+It actually counts for every constant how often it is used.
+A count of 0 means that the constant was declared, but never used.
+
+    cargo run --release --example symcount -- in.dk > in.symcount
+
+To get those constants that are used exactly once, we use some UNIX magic:
+
+    grep "^1[^0-9]" in.symcount | sed 's/^1.//' > in.inline
+
+Finally, we use `inline`.
+To save memory, this will forget any definition that has been inlined once,
+so you currently cannot use this to inline definitions that are used more than once!
+
+    cargo run --release --example inline -- in.dk in.inline > in.inlined.dk

dedukti-parse/examples/inline.rs

@@ -1,10 +1,10 @@
 use core::hash::Hash;
-use dedukti_parse::{term, Command, Intro, Lazy, Symb};
+use dedukti_parse::{term, Command, Intro, Strict, Symb};
 use std::collections::{HashMap, HashSet};
 
-fn map_atoms<A, B, V>(t: term::Term<A, V>, f: &impl Fn(A) -> term::Term<B, V>) -> term::Term<B, V> {
+fn map_atoms<A, B, V>(t: term::Term<A, V>, f: &mut impl FnMut(A) -> term::Term<B, V>) -> term::Term<B, V> {
     use term::AppH;
-    let args = t.args.into_iter().map(|a| map_atoms(a, f));
+    let args = t.args.into_iter().map(|a| map_atoms(a, f)).collect();
     let head = match t.head {
         AppH::Atom(a) => {
             let b = f(a);
@@ -18,61 +18,56 @@ fn map_atoms<A, B, V>(t: term::Term<A, V>, f: &impl Fn(A) -> term::Term<B, V>) -
             ty.map(|t| Box::new(map_atoms(*t, f))),
             Box::new(map_atoms(*tm, f)),
         ),
-        AppH::Prod(v, ty, tm) => AppH::Prod(
-            v,
-            Box::new(map_atoms(*ty, f)),
-            Box::new(map_atoms(*tm, f)),
-        ),
+        AppH::Prod(v, ty, tm) => {
+            AppH::Prod(v, Box::new(map_atoms(*ty, f)), Box::new(map_atoms(*tm, f)))
+        }
     };
-    let args = args.collect();
     term::Term { head, args }
 }
 
 fn subst<A: Clone + Eq + Hash, V: Clone>(
-    map: &HashMap<A, term::Term<A, V>>,
+    map: &mut HashMap<A, term::Term<A, V>>,
     t: term::Term<A, V>,
 ) -> term::Term<A, V> {
-    map_atoms(t, &|a| match map.get(&a) {
+    map_atoms(t, &mut |a| match map.remove(&a) {
         None => term::Term {
             head: term::AppH::Atom(a),
             args: Vec::new(),
         },
-        Some(t) => t.clone(),
+        Some(t) => t,
     })
 }
 
 fn main() -> std::io::Result<()> {
-    let mut map = HashMap::new();
-
-    use std::fs::File;
-    use std::io::{BufRead, BufReader};
+    let mut map: HashMap<Symb<&str>, _> = HashMap::new();
 
     let args: Vec<String> = std::env::args().collect();
-    let set: Result<HashSet<String>, _> = BufReader::new(File::open(&args[2])?).lines().collect();
-    let set = set?;
+    let to_inline = std::fs::read_to_string(&args[2])?;
+    let set: HashSet<&str> = to_inline.lines().collect();
 
-    let file = File::open(&args[1])?;
-    let reader = BufReader::new(file);
+    let file = std::fs::read_to_string(&args[1])?;
 
-    let cmds = Lazy::<_, _, String>::new(reader.lines().map(|l| l.unwrap()));
+    let cmds = Strict::<_, _, &str>::new(&file);
     for cmd in cmds {
         let cmd = cmd.unwrap();
         //println!("{cmd:?}");
 
         match cmd {
-            Command::Intro(name, args, Intro::Definition(_, Some(tm)) | Intro::Theorem(_, tm)) if set.contains(&name) && args.is_empty() => {
-                map.insert(Symb::new(name), subst(&map, tm));
+            Command::Intro(name, args, Intro::Definition(_, Some(tm)) | Intro::Theorem(_, tm))
+                if set.contains(&name) && args.is_empty() =>
+            {
+                let tm = subst(&mut map, tm);
+                map.insert(Symb::new(name), tm);
             }
             Command::Intro(name, args, intro) => {
                 let args = args
                     .into_iter()
-                    .map(|(v, ty)| (v, subst(&map, ty)))
+                    .map(|(v, ty)| (v, subst(&mut map, ty)))
                     .collect();
                 let intro = intro
-                    .map_type(|t| subst(&map, t))
-                    .map_term(|t| subst(&map, t));
+                    .map_type(|t| subst(&mut map, t))
+                    .map_term(|t| subst(&mut map, t));
                 println!("{}.", Command::Intro(name, args, intro));
-
             }
             cmd @ Command::Rules(..) => println!("{cmd}."),
         }