|
|
|
@ -6,52 +6,57 @@ impl Book {
|
|
|
|
|
/// Decides if names inside a term belong to a Var or to a Ref.
|
|
|
|
|
/// Precondition: Refs are encoded as vars.
|
|
|
|
|
/// Postcondition: Refs are encoded as refs, with the correct def id.
|
|
|
|
|
pub fn resolve_refs(&mut self) {
|
|
|
|
|
pub fn resolve_refs(&mut self) -> Result<(), String> {
|
|
|
|
|
for def in self.defs.values_mut() {
|
|
|
|
|
for rule in def.rules.iter_mut() {
|
|
|
|
|
rule.body.resolve_refs(&self.def_names);
|
|
|
|
|
rule.body.resolve_refs(&self.def_names)?;
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
Ok(())
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
impl Term {
|
|
|
|
|
pub fn resolve_refs(&mut self, def_names: &DefNames) {
|
|
|
|
|
pub fn resolve_refs(&mut self, def_names: &DefNames) -> Result<(), String> {
|
|
|
|
|
resolve_refs(self, def_names, &mut HashMap::new())
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
fn resolve_refs(term: &mut Term, def_names: &DefNames, scope: &mut HashMap<Name, usize>) {
|
|
|
|
|
fn resolve_refs(
|
|
|
|
|
term: &mut Term,
|
|
|
|
|
def_names: &DefNames,
|
|
|
|
|
scope: &mut HashMap<Name, usize>,
|
|
|
|
|
) -> Result<(), String> {
|
|
|
|
|
match term {
|
|
|
|
|
Term::Lam { nam, bod, .. } => {
|
|
|
|
|
push_scope(nam.clone(), scope);
|
|
|
|
|
resolve_refs(bod, def_names, scope);
|
|
|
|
|
resolve_refs(bod, def_names, scope)?;
|
|
|
|
|
pop_scope(nam.clone(), scope);
|
|
|
|
|
}
|
|
|
|
|
Term::Let { pat: Pattern::Var(nam), val, nxt } => {
|
|
|
|
|
resolve_refs(val, def_names, scope);
|
|
|
|
|
resolve_refs(val, def_names, scope)?;
|
|
|
|
|
push_scope(nam.clone(), scope);
|
|
|
|
|
resolve_refs(nxt, def_names, scope);
|
|
|
|
|
resolve_refs(nxt, def_names, scope)?;
|
|
|
|
|
pop_scope(nam.clone(), scope);
|
|
|
|
|
}
|
|
|
|
|
Term::Let { pat, val, nxt } => {
|
|
|
|
|
resolve_refs(val, def_names, scope);
|
|
|
|
|
resolve_refs(val, def_names, scope)?;
|
|
|
|
|
|
|
|
|
|
for nam in pat.names() {
|
|
|
|
|
push_scope(Some(nam.clone()), scope)
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
resolve_refs(nxt, def_names, scope);
|
|
|
|
|
resolve_refs(nxt, def_names, scope)?;
|
|
|
|
|
|
|
|
|
|
for nam in pat.names() {
|
|
|
|
|
pop_scope(Some(nam.clone()), scope)
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
Term::Dup { tag: _, fst, snd, val, nxt } => {
|
|
|
|
|
resolve_refs(val, def_names, scope);
|
|
|
|
|
resolve_refs(val, def_names, scope)?;
|
|
|
|
|
push_scope(fst.clone(), scope);
|
|
|
|
|
push_scope(snd.clone(), scope);
|
|
|
|
|
resolve_refs(nxt, def_names, scope);
|
|
|
|
|
resolve_refs(nxt, def_names, scope)?;
|
|
|
|
|
pop_scope(fst.clone(), scope);
|
|
|
|
|
pop_scope(snd.clone(), scope);
|
|
|
|
|
}
|
|
|
|
@ -59,27 +64,31 @@ fn resolve_refs(term: &mut Term, def_names: &DefNames, scope: &mut HashMap<Name,
|
|
|
|
|
// If variable not defined, we check if it's a ref and swap if it is.
|
|
|
|
|
Term::Var { nam } => {
|
|
|
|
|
if is_var_in_scope(nam.clone(), scope) {
|
|
|
|
|
if matches!(nam.0.as_ref(), DefNames::ENTRY_POINT | DefNames::HVM1_ENTRY_POINT) {
|
|
|
|
|
return Err("Main definition can't be referenced inside the program".to_string());
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
if let Some(def_id) = def_names.def_id(nam) {
|
|
|
|
|
*term = Term::Ref { def_id };
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
Term::Chn { bod, .. } => resolve_refs(bod, def_names, scope),
|
|
|
|
|
Term::Chn { bod, .. } => resolve_refs(bod, def_names, scope)?,
|
|
|
|
|
Term::App { fun: fst, arg: snd, .. }
|
|
|
|
|
| Term::Sup { fst, snd, .. }
|
|
|
|
|
| Term::Tup { fst, snd }
|
|
|
|
|
| Term::Opx { fst, snd, .. } => {
|
|
|
|
|
resolve_refs(fst, def_names, scope);
|
|
|
|
|
resolve_refs(snd, def_names, scope);
|
|
|
|
|
resolve_refs(fst, def_names, scope)?;
|
|
|
|
|
resolve_refs(snd, def_names, scope)?;
|
|
|
|
|
}
|
|
|
|
|
Term::Match { scrutinee, arms } => {
|
|
|
|
|
resolve_refs(scrutinee, def_names, scope);
|
|
|
|
|
resolve_refs(scrutinee, def_names, scope)?;
|
|
|
|
|
for (pat, term) in arms {
|
|
|
|
|
if let Pattern::Num(MatchNum::Succ(Some(nam))) = pat {
|
|
|
|
|
push_scope(nam.clone(), scope)
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
resolve_refs(term, def_names, scope);
|
|
|
|
|
resolve_refs(term, def_names, scope)?;
|
|
|
|
|
|
|
|
|
|
if let Pattern::Num(MatchNum::Succ(Some(nam))) = pat {
|
|
|
|
|
pop_scope(nam.clone(), scope)
|
|
|
|
@ -89,6 +98,8 @@ fn resolve_refs(term: &mut Term, def_names: &DefNames, scope: &mut HashMap<Name,
|
|
|
|
|
Term::List { .. } => unreachable!("Should have been desugared already"),
|
|
|
|
|
Term::Lnk { .. } | Term::Ref { .. } | Term::Num { .. } | Term::Str { .. } | Term::Era => (),
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
Ok(())
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
fn push_scope(name: Option<Name>, scope: &mut HashMap<Name, usize>) {
|
|
|
|
|