mirror of
https://github.com/HigherOrderCO/Bend.git
synced 2024-10-26 14:05:36 +03:00
Add detach combinators pass
This commit is contained in:
parent
6904e81e67
commit
52a2f02fdd
@ -25,6 +25,7 @@ pub fn check_book(book: DefinitionBook) -> anyhow::Result<()> {
|
||||
pub fn compile_book(mut book: DefinitionBook) -> anyhow::Result<(Book, DefNames)> {
|
||||
// book.check_rule_arities()?;
|
||||
book.sanitize_vars()?;
|
||||
book.detach_combinators();
|
||||
// book.try_into_affine()?;
|
||||
let core_book = book_to_hvm_core(&book)?;
|
||||
Ok((core_book, book.def_names))
|
||||
|
@ -1,7 +1,7 @@
|
||||
use hvm_core::Val;
|
||||
|
||||
use crate::ast::{hvm_lang::DefNames, var_id_to_name, DefinitionBook, Name, Term};
|
||||
use std::collections::HashMap;
|
||||
use crate::ast::{hvm_lang::DefNames, var_id_to_name, DefId, Definition, DefinitionBook, Name, Rule, Term};
|
||||
use std::collections::{HashMap, HashSet};
|
||||
|
||||
/// For all var declarations:
|
||||
/// If they're used 0 times: erase the declaration
|
||||
@ -372,3 +372,161 @@ fn term_to_affine(
|
||||
};
|
||||
Ok(term)
|
||||
}
|
||||
|
||||
/// Replaces closed Terms (i.e. without free variables) with a Ref to the extracted term
|
||||
/// Precondition: Vars must have been sanitized
|
||||
impl DefinitionBook {
|
||||
pub fn detach_combinators(&mut self) {
|
||||
let mut combinators = Vec::new();
|
||||
let new_ids_base = self.defs.len() as u32;
|
||||
|
||||
for def in self.defs.iter_mut() {
|
||||
for rule in def.rules.iter_mut() {
|
||||
rule.body.detach_combinators(rule.def_id, new_ids_base, &self.def_names, &mut combinators);
|
||||
}
|
||||
}
|
||||
|
||||
for (name, def_id, body) in combinators {
|
||||
self.def_names.insert(def_id, name);
|
||||
let rules = vec![Rule { def_id, pats: Vec::new(), body }];
|
||||
|
||||
self.defs.push(Definition { def_id, rules })
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
type Combinators = Vec<(Name, DefId, Term)>;
|
||||
|
||||
struct TermInfo<'d> {
|
||||
//Number of times a Term has been detached from the current Term
|
||||
counter: u32,
|
||||
//Base value for creating new DefIds
|
||||
new_ids_base: u32,
|
||||
rule_id: DefId,
|
||||
def_names: &'d DefNames,
|
||||
needed_names: HashSet<Name>,
|
||||
combinators: &'d mut Combinators,
|
||||
}
|
||||
|
||||
impl<'d> TermInfo<'d> {
|
||||
fn new(
|
||||
new_ids_base: u32,
|
||||
rule_id: DefId,
|
||||
def_names: &'d DefNames,
|
||||
combinators: &'d mut Combinators,
|
||||
) -> Self {
|
||||
Self { counter: 0, new_ids_base, rule_id, def_names, needed_names: HashSet::new(), combinators }
|
||||
}
|
||||
fn request_name(&mut self, name: &Name) {
|
||||
self.needed_names.insert(name.to_owned());
|
||||
}
|
||||
|
||||
fn provide(&mut self, name: &Name) {
|
||||
self.needed_names.remove(name);
|
||||
}
|
||||
|
||||
fn check(&self) -> bool {
|
||||
self.needed_names.is_empty()
|
||||
}
|
||||
|
||||
fn replace_scope(&mut self, new_scope: HashSet<Name>) -> HashSet<Name> {
|
||||
std::mem::replace(&mut self.needed_names, new_scope)
|
||||
}
|
||||
|
||||
fn merge_scope(&mut self, target: HashSet<Name>) {
|
||||
self.needed_names.extend(target);
|
||||
}
|
||||
|
||||
fn detach_term(&mut self, term: &mut Term) {
|
||||
let Name(name) = self.def_names.get_by_left(&self.rule_id).unwrap();
|
||||
let combinator = Name(format!("{name}{}", self.counter));
|
||||
self.counter += 1;
|
||||
|
||||
let def_id = DefId(self.new_ids_base + (self.combinators.len() as u32));
|
||||
|
||||
let combinator_var = Term::Ref { def_id };
|
||||
let extracted_term = std::mem::replace(term, combinator_var);
|
||||
|
||||
self.combinators.push((combinator, def_id, extracted_term));
|
||||
}
|
||||
}
|
||||
|
||||
impl Term {
|
||||
pub fn detach_combinators(
|
||||
&mut self,
|
||||
rule_id: DefId,
|
||||
new_ids_base: u32,
|
||||
def_names: &DefNames,
|
||||
combinators: &mut Combinators,
|
||||
) {
|
||||
fn go(term: &mut Term, depth: usize, term_info: &mut TermInfo) -> bool {
|
||||
match term {
|
||||
Term::Lam { nam, bod } => {
|
||||
let parent_scope = term_info.replace_scope(HashSet::new());
|
||||
|
||||
let is_super = go(bod, depth + 1, term_info);
|
||||
|
||||
if let Some(name) = nam {
|
||||
term_info.provide(name);
|
||||
}
|
||||
|
||||
if is_super && depth != 0 && term_info.check() {
|
||||
term_info.detach_term(term);
|
||||
}
|
||||
|
||||
term_info.merge_scope(parent_scope);
|
||||
|
||||
is_super
|
||||
}
|
||||
Term::Var { nam } => {
|
||||
term_info.request_name(nam);
|
||||
true
|
||||
}
|
||||
Term::Chn { nam: _, bod } => {
|
||||
go(bod, depth + 1, term_info);
|
||||
false
|
||||
}
|
||||
Term::Lnk { .. } => false,
|
||||
Term::Let { nam, val, nxt } => {
|
||||
let val_is_super = go(val, depth + 1, term_info);
|
||||
let nxt_is_super = go(nxt, depth + 1, term_info);
|
||||
term_info.provide(nam);
|
||||
|
||||
val_is_super && nxt_is_super
|
||||
}
|
||||
Term::Ref { .. } => true,
|
||||
Term::App { fun, arg } => {
|
||||
let fun_is_super = go(fun, depth + 1, term_info);
|
||||
let arg_is_super = go(arg, depth + 1, term_info);
|
||||
|
||||
fun_is_super && arg_is_super
|
||||
}
|
||||
Term::Dup { fst, snd, val, nxt } => {
|
||||
let val_is_super = go(val, depth + 1, term_info);
|
||||
let nxt_is_supper = go(nxt, depth + 1, term_info);
|
||||
|
||||
if let Some(snd) = snd {
|
||||
term_info.provide(snd);
|
||||
}
|
||||
if let Some(fst) = fst {
|
||||
term_info.provide(fst);
|
||||
}
|
||||
|
||||
val_is_super && nxt_is_supper
|
||||
}
|
||||
|
||||
Term::Sup { .. } => todo!(),
|
||||
Term::Era => true,
|
||||
|
||||
#[cfg(feature = "nums")]
|
||||
Term::U32 { .. } => true,
|
||||
#[cfg(feature = "nums")]
|
||||
Term::I32 { .. } => true,
|
||||
#[cfg(feature = "nums")]
|
||||
Term::Opx { .. } => true,
|
||||
}
|
||||
}
|
||||
|
||||
go(self, 0, &mut TermInfo::new(new_ids_base, rule_id, def_names, combinators));
|
||||
}
|
||||
}
|
||||
|
@ -2,7 +2,7 @@
|
||||
$ (0 a (0 * a))
|
||||
|
||||
2 (fals) =
|
||||
$ (0 * (0 a a))
|
||||
$ (0 * @5)
|
||||
|
||||
3 (Not) =
|
||||
$ (0 (0 @2 (0 @1 a)) a)
|
||||
@ -11,4 +11,7 @@
|
||||
$ a
|
||||
& (0 @1 a)
|
||||
~ @3
|
||||
|
||||
5 (fals0) =
|
||||
$ (0 a a)
|
||||
|
@ -1,11 +1,11 @@
|
||||
1 (C_z) =
|
||||
$ (0 * (0 a a))
|
||||
$ (0 * @8)
|
||||
|
||||
2 (C_s) =
|
||||
$ (0 (0 a (0 b c)) (0 (1 (0 c d) a) (0 b d)))
|
||||
|
||||
3 (Z) =
|
||||
$ (0 * (0 a a))
|
||||
$ (0 * @9)
|
||||
|
||||
4 (S) =
|
||||
$ (0 a (0 (0 a b) (0 * b)))
|
||||
@ -20,4 +20,10 @@
|
||||
$ a
|
||||
& (0 @4 (0 @3 a))
|
||||
~ @6
|
||||
|
||||
8 (C_z0) =
|
||||
$ (0 a a)
|
||||
|
||||
9 (Z0) =
|
||||
$ (0 a a)
|
||||
|
@ -8,7 +8,7 @@
|
||||
$ (0 a (0 * (0 (0 a b) (0 * b))))
|
||||
|
||||
4 (E) =
|
||||
$ (0 * (0 * (0 a a)))
|
||||
$ (0 * @G)
|
||||
|
||||
5 (run) =
|
||||
$ (0 (0 @6 (0 @7 (0 @4 a))) a)
|
||||
@ -69,4 +69,10 @@ E (Ex2) =
|
||||
~ @5
|
||||
& (0 @3 (0 @4 b))
|
||||
~ @1
|
||||
|
||||
F (E0) =
|
||||
$ (0 a a)
|
||||
|
||||
G (E1) =
|
||||
$ (0 * @F)
|
||||
|
@ -3,6 +3,9 @@
|
||||
|
||||
2 (b) =
|
||||
$ a
|
||||
& (0 (0 b b) a)
|
||||
& (0 @3 a)
|
||||
~ @1
|
||||
|
||||
3 (b0) =
|
||||
$ (0 a a)
|
||||
|
@ -1 +1 @@
|
||||
λa λ* ((a 1) λb λ* ((b 2) λc λ* ((c 3) λ* λd d)))
|
||||
λa λ* ((a 1) λb λ* ((b 2) λc λ* ((c 3) λ* Nil0)))
|
Loading…
Reference in New Issue
Block a user