From 3e0f0e90d2cfdb2e12379c0c3fb0646adaeec813 Mon Sep 17 00:00:00 2001 From: David Binder Date: Tue, 16 Apr 2024 16:34:37 +0200 Subject: [PATCH 1/6] Remove FreeVarsExt trait --- lang/lifting/src/fv.rs | 28 +++++++++++----------------- lang/lifting/src/lib.rs | 11 +++++------ 2 files changed, 16 insertions(+), 23 deletions(-) diff --git a/lang/lifting/src/fv.rs b/lang/lifting/src/fv.rs index 23cdc34e1..4a2d43ee7 100644 --- a/lang/lifting/src/fv.rs +++ b/lang/lifting/src/fv.rs @@ -11,8 +11,17 @@ use syntax::generic::{Visit, Visitor}; use syntax::ust::{self, Occurs}; /// Find all free variables -pub trait FreeVarsExt { - fn free_vars(&self, ctx: &TypeCtx) -> FreeVars; +pub fn free_vars>(arg: &T, ctx: &TypeCtx) -> FreeVars { + let mut v = USTVisitor { + fvs: Default::default(), + cutoff: ctx.len(), + type_ctx: ctx, + lvl_ctx: ctx.levels(), + }; + + arg.visit(&mut v); + + FreeVars { fvs: v.fvs, cutoff: ctx.len() } } #[derive(Debug)] @@ -152,21 +161,6 @@ impl Ord for FreeVar { } } -impl> FreeVarsExt for T { - fn free_vars(&self, type_ctx: &TypeCtx) -> FreeVars { - let mut v = USTVisitor { - fvs: Default::default(), - cutoff: type_ctx.len(), - type_ctx, - lvl_ctx: type_ctx.levels(), - }; - - self.visit(&mut v); - - FreeVars { fvs: v.fvs, cutoff: type_ctx.len() } - } -} - /// Visitor that collects free variables in an untyped syntax tree struct USTVisitor<'a> { /// Set of collected free variables diff --git a/lang/lifting/src/lib.rs b/lang/lifting/src/lib.rs index 0f568dddf..00e5cf60c 100644 --- a/lang/lifting/src/lib.rs +++ b/lang/lifting/src/lib.rs @@ -488,15 +488,14 @@ impl Ctx { // Build a telescope of the types of the lifted variables let ret_fvs = motive .as_ref() - .map(|m| m.forget_tst().free_vars(type_ctx)) - .unwrap_or_else(|| ret_typ.as_exp().forget_tst().free_vars(type_ctx)); + .map(|m| free_vars(&m.forget_tst(), type_ctx)) + .unwrap_or_else(|| free_vars(&ret_typ.as_exp().forget_tst(), type_ctx)); let body = body.lift(self); let self_typ = info.typ.lift(self); - let FreeVarsResult { telescope, subst, args } = body - .free_vars(type_ctx) - .union(self_typ.free_vars(type_ctx)) + let FreeVarsResult { telescope, subst, args } = free_vars(&body, type_ctx) + .union(free_vars(&self_typ, type_ctx)) .union(ret_fvs) .telescope(&self.ctx); @@ -561,7 +560,7 @@ impl Ctx { // Collect the free variables in the comatch and the return type // Build a telescope of the types of the lifted variables let FreeVarsResult { telescope, subst, args } = - body.free_vars(type_ctx).union(typ.free_vars(type_ctx)).telescope(&self.ctx); + free_vars(&body, type_ctx).union(free_vars(&typ, type_ctx)).telescope(&self.ctx); // Substitute the new parameters for the free variables let body = body.subst(&mut self.ctx, &subst.in_body()); From 0dae2459fef80e5bcb9ead3bf065dd35dc06855b Mon Sep 17 00:00:00 2001 From: David Binder Date: Tue, 16 Apr 2024 16:45:59 +0200 Subject: [PATCH 2/6] Rewrite Visitor --- lang/lifting/src/fv.rs | 181 +++++++++++++++++++++++++---------------- 1 file changed, 112 insertions(+), 69 deletions(-) diff --git a/lang/lifting/src/fv.rs b/lang/lifting/src/fv.rs index 4a2d43ee7..bf4472ea9 100644 --- a/lang/lifting/src/fv.rs +++ b/lang/lifting/src/fv.rs @@ -7,11 +7,10 @@ use derivative::Derivative; use syntax::common::*; use syntax::ctx::values::TypeCtx; use syntax::ctx::*; -use syntax::generic::{Visit, Visitor}; use syntax::ust::{self, Occurs}; /// Find all free variables -pub fn free_vars>(arg: &T, ctx: &TypeCtx) -> FreeVars { +pub fn free_vars(arg: &T, ctx: &TypeCtx) -> FreeVars { let mut v = USTVisitor { fvs: Default::default(), cutoff: ctx.len(), @@ -19,11 +18,55 @@ pub fn free_vars>(arg: &T, ctx: &TypeCtx) -> FreeVars { lvl_ctx: ctx.levels(), }; - arg.visit(&mut v); + arg.visit_fv(&mut v); FreeVars { fvs: v.fvs, cutoff: ctx.len() } } +trait FV { + fn visit_fv(&self,v: &mut USTVisitor); +} + +impl FV for ust::Exp { + fn visit_fv(&self,v: &mut USTVisitor) { + match self { + ust::Exp::Anno { info, exp, typ } => todo!(), + ust::Exp::Var { info, name, ctx, idx } => todo!(), + ust::Exp::Comatch { info, ctx, name, is_lambda_sugar, body } => todo!(), + ust::Exp::Ctor { info, name, args } => todo!(), + ust::Exp::Dtor { info, exp, name, args } => todo!(), + ust::Exp::TypCtor { info, name, args } => todo!(), + ust::Exp::Hole { info } => todo!(), + ust::Exp::Type { info } => todo!(), + ust::Exp::Match { info, ctx, name, on_exp, motive, ret_typ, body } => todo!(), + } + } +} + +impl FV for ust::Match { + fn visit_fv(&self,v: &mut USTVisitor) { + todo!() + } +} + +impl FV for ust::Motive { + fn visit_fv(&self,v: &mut USTVisitor) { + todo!() + } +} + +impl FV for ust::TypApp { + fn visit_fv(&self,v: &mut USTVisitor) { + todo!() + } +} + +impl FV for Rc { + fn visit_fv(&self,v: &mut USTVisitor) { + todo!() + } +} + #[derive(Debug)] pub struct FreeVars { /// The De-Bruijn level (fst index) up to which a variable counts as free @@ -173,18 +216,18 @@ struct USTVisitor<'a> { lvl_ctx: LevelCtx, } -impl<'a> USTVisitor<'a> { - /// Add a free variable as well as all free variables its type - fn add_fv(&mut self, name: ust::Ident, lvl: Lvl, typ: Rc, ctx: LevelCtx) { - // Add the free variable - let fv = FreeVar { name, lvl, typ: typ.clone(), ctx }; - if self.fvs.insert(fv) { - // If it has not already been added: - // Find all free variables in the type of the free variable - typ.visit(self); - } - } -} +// impl<'a> USTVisitor<'a> { +// /// Add a free variable as well as all free variables its type +// fn add_fv(&mut self, name: ust::Ident, lvl: Lvl, typ: Rc, ctx: LevelCtx) { +// // Add the free variable +// let fv = FreeVar { name, lvl, typ: typ.clone(), ctx }; +// if self.fvs.insert(fv) { +// // If it has not already been added: +// // Find all free variables in the type of the free variable +// typ.visit(self); +// } +// } +// } impl<'a> BindContext for USTVisitor<'a> { type Ctx = LevelCtx; @@ -194,60 +237,60 @@ impl<'a> BindContext for USTVisitor<'a> { } } -impl<'b> Visitor for USTVisitor<'b> { - fn visit_telescope<'a, I, F1, F2>(&mut self, params: I, f_acc: F1, f_inner: F2) - where - I: IntoIterator, - F1: Fn(&mut Self, &'a ust::Param), - F2: FnOnce(&mut Self), - { - self.ctx_visit_telescope(params, f_acc, f_inner) - } - - fn visit_telescope_inst<'a, I, F1, F2>(&mut self, params: I, f_acc: F1, f_inner: F2) - where - I: IntoIterator, - F1: Fn(&mut Self, &'a ust::ParamInst), - F2: FnOnce(&mut Self), - { - self.ctx_visit_telescope_inst(params, f_acc, f_inner) - } - - fn visit_motive_param(&mut self, param: &ust::ParamInst, f_inner: F) -> X - where - F: FnOnce(&mut Self, &ust::ParamInst) -> X, - { - self.ctx_visit_motive_param(param, f_inner) - } - - fn visit_self_param( - &mut self, - info: &Option, - name: &Option, - typ: &ust::TypApp, - f_inner: F, - ) -> X - where - F: FnOnce(&mut Self) -> X, - { - self.ctx_visit_self_param(info, name, typ, f_inner) - } - - fn visit_exp_var(&mut self, _info: &Option, name: &ust::Ident, _ctx: &(), idx: &Idx) { - // We use the level context to convert the De Bruijn index to a De Bruijn level - let lvl = self.lvl_ctx.idx_to_lvl(*idx); - // If the variable is considered free (based on the cutoff), we look up its type in the typing context - // The typing context contains the types for all free variables where lvl < cutoff - if lvl.fst < self.cutoff { - let typ = self - .type_ctx - .lookup(lvl) - .typ - .shift(((self.lvl_ctx.len() - self.type_ctx.len()) as isize, 0)); - self.add_fv(name.clone(), lvl, typ, self.lvl_ctx.clone()) - } - } -} +// impl<'b> Visitor for USTVisitor<'b> { +// fn visit_telescope<'a, I, F1, F2>(&mut self, params: I, f_acc: F1, f_inner: F2) +// where +// I: IntoIterator, +// F1: Fn(&mut Self, &'a ust::Param), +// F2: FnOnce(&mut Self), +// { +// self.ctx_visit_telescope(params, f_acc, f_inner) +// } + +// fn visit_telescope_inst<'a, I, F1, F2>(&mut self, params: I, f_acc: F1, f_inner: F2) +// where +// I: IntoIterator, +// F1: Fn(&mut Self, &'a ust::ParamInst), +// F2: FnOnce(&mut Self), +// { +// self.ctx_visit_telescope_inst(params, f_acc, f_inner) +// } + +// fn visit_motive_param(&mut self, param: &ust::ParamInst, f_inner: F) -> X +// where +// F: FnOnce(&mut Self, &ust::ParamInst) -> X, +// { +// self.ctx_visit_motive_param(param, f_inner) +// } + +// fn visit_self_param( +// &mut self, +// info: &Option, +// name: &Option, +// typ: &ust::TypApp, +// f_inner: F, +// ) -> X +// where +// F: FnOnce(&mut Self) -> X, +// { +// self.ctx_visit_self_param(info, name, typ, f_inner) +// } + +// fn visit_exp_var(&mut self, _info: &Option, name: &ust::Ident, _ctx: &(), idx: &Idx) { +// // We use the level context to convert the De Bruijn index to a De Bruijn level +// let lvl = self.lvl_ctx.idx_to_lvl(*idx); +// // If the variable is considered free (based on the cutoff), we look up its type in the typing context +// // The typing context contains the types for all free variables where lvl < cutoff +// if lvl.fst < self.cutoff { +// let typ = self +// .type_ctx +// .lookup(lvl) +// .typ +// .shift(((self.lvl_ctx.len() - self.type_ctx.len()) as isize, 0)); +// self.add_fv(name.clone(), lvl, typ, self.lvl_ctx.clone()) +// } +// } +// } /// Substitution of free variables #[derive(Clone, Debug)] From 2bc6e3918cbc31dbeb9df182a1ff7168cc0ae6bf Mon Sep 17 00:00:00 2001 From: David Binder Date: Tue, 16 Apr 2024 16:46:48 +0200 Subject: [PATCH 3/6] Remove old visitor --- lang/syntax/src/trees/generic/mod.rs | 2 - lang/syntax/src/trees/generic/visit.rs | 467 ------------------------- 2 files changed, 469 deletions(-) delete mode 100644 lang/syntax/src/trees/generic/visit.rs diff --git a/lang/syntax/src/trees/generic/mod.rs b/lang/syntax/src/trees/generic/mod.rs index 9653dabbe..e2a03b621 100644 --- a/lang/syntax/src/trees/generic/mod.rs +++ b/lang/syntax/src/trees/generic/mod.rs @@ -1,8 +1,6 @@ mod def; mod lookup; pub mod lookup_table; -mod visit; pub use def::*; pub use lookup::*; -pub use visit::*; diff --git a/lang/syntax/src/trees/generic/visit.rs b/lang/syntax/src/trees/generic/visit.rs deleted file mode 100644 index 08a8a792a..000000000 --- a/lang/syntax/src/trees/generic/visit.rs +++ /dev/null @@ -1,467 +0,0 @@ -use std::rc::Rc; - -use codespan::Span; - -use crate::common::*; - -use super::def::*; -use super::lookup_table::LookupTable; - -#[rustfmt::skip] -#[allow(unused_variables)] -#[allow(clippy::too_many_arguments)] -pub trait Visitor { - fn visit_prg(&mut self, decls: &Decls

) {} - fn visit_decls(&mut self, map: &HashMap>, source: &LookupTable) {} - fn visit_decl(&mut self, decl: &Decl

) {} - fn visit_decl_data(&mut self, data: &Data

) {} - fn visit_decl_codata(&mut self, codata: &Codata

) {} - fn visit_decl_ctor(&mut self, ctor: &Ctor

) {} - fn visit_decl_dtor(&mut self, dtor: &Dtor

) {} - fn visit_decl_def(&mut self, def: &Def

) {} - fn visit_decl_codef(&mut self, codef: &Codef

) {} - fn visit_decl_let(&mut self, tl_let: &Let

) {} - fn visit_data(&mut self, info: &Option, doc: &Option, name: &Ident, attr: &Attribute, typ: &Rc>, ctors: &[Ident]) {} - fn visit_codata(&mut self, info: &Option, doc: &Option, name: &Ident, attr: &Attribute, typ: &Rc>, dtors: &[Ident]) {} - fn visit_typ_abs(&mut self, params: &Telescope

) {} - fn visit_ctor(&mut self, info: &Option, doc: &Option, name: &Ident, params: &Telescope

, typ: &TypApp

) {} - fn visit_dtor(&mut self, info: &Option, doc: &Option, name: &Ident, params: &Telescope

, self_param: &SelfParam

, ret_typ: &Rc>) {} - fn visit_def(&mut self, info: &Option, doc: &Option, name: &Ident, attr: &Attribute, params: &Telescope

, self_param: &SelfParam

, ret_typ: &Rc>, body: &Match

) {} - fn visit_codef(&mut self, info: &Option, doc: &Option, name: &Ident, attr: &Attribute, params: &Telescope

, typ: &TypApp

, body: &Match

) {} - fn visit_let(&mut self, info: &Option, doc: &Option, name: &Ident, attr: &Attribute, params: &Telescope

, typ: &Rc>, body: &Rc>) {} - fn visit_match(&mut self, info: &Option, cases: &[Case

], omit_absurd: bool) {} - fn visit_case(&mut self, info: &Option, name: &Ident, args: &TelescopeInst

, body: &Option>>) {} - fn visit_typ_app(&mut self, info: &P::TypeInfo, name: &Ident, args: &Args

) {} - fn visit_exp_var(&mut self, info: &P::TypeInfo, name: &Ident, ctx: &P::Ctx, idx: &Idx) {} - fn visit_exp_typ_ctor(&mut self, info: &P::TypeInfo, name: &Ident, args: &Args

) {} - fn visit_exp_ctor(&mut self, info: &P::TypeInfo, name: &Ident, args: &Args

) {} - fn visit_exp_dtor(&mut self, info: &P::TypeInfo, exp: &Rc>, name: &Ident, args: &Args

) {} - fn visit_exp_anno(&mut self, info: &P::TypeInfo, exp: &Rc>, typ: &Rc>) {} - fn visit_exp_type(&mut self, info: &P::TypeInfo) {} - fn visit_exp_match(&mut self, info: &P::TypeAppInfo, ctx: &P::Ctx, name: &Label, on_exp: &Rc>, ret_typ: &P::InfTyp, body: &Match

) {} - fn visit_exp_comatch(&mut self, info: &P::TypeAppInfo, ctx: &P::Ctx, name: &Label, is_lambda_sugar: &bool, body: &Match

) {} - fn visit_exp_hole(&mut self, info: &P::TypeInfo) {} - fn visit_motive(&mut self, info: &Option, param: &ParamInst

, ret_typ: &Rc>) {} - fn visit_motive_param(&mut self, param: &ParamInst

, f_inner: F) -> X - where - F: FnOnce(&mut Self, &ParamInst

) -> X - { - f_inner(self, param) - } - fn visit_telescope<'a, I, F1, F2>(&mut self, params: I, f_acc: F1, f_inner: F2) - where - P: 'a, - I: IntoIterator>, - F1: Fn(&mut Self, &'a Param

), - F2: FnOnce(&mut Self) - { - for param in params.into_iter() { - f_acc(self, param); - } - f_inner(self) - } - fn visit_telescope_inst<'a, I, F1, F2>(&mut self, params: I, f_acc: F1, f_inner: F2) - where - P: 'a, - I: IntoIterator>, - F1: Fn(&mut Self, &'a ParamInst

), - F2: FnOnce(&mut Self) - { - for param in params.into_iter() { - f_acc(self, param); - } - f_inner(self) - } - fn visit_self_param(&mut self, info: &Option, name: &Option, typ: &TypApp

, f_inner: F) -> X - where - F: FnOnce(&mut Self) -> X - { - f_inner(self) - } - fn visit_param(&mut self, name: &Ident, typ: &Rc>) {} - fn visit_param_inst(&mut self, info: &P::TypeInfo, name: &Ident, typ: &P::InfTyp) {} - fn visit_info(&mut self, info: &Option) {} - fn visit_type_info(&mut self, info: &P::TypeInfo) {} - fn visit_type_app_info(&mut self, info: &P::TypeAppInfo) {} - fn visit_idx(&mut self, idx: &Idx) {} - fn visit_typ(&mut self, typ: &P::InfTyp) {} - fn visit_ctx(&mut self, ctx: &P::Ctx) {} -} - -pub trait Visit { - fn visit(&self, v: &mut V) - where - V: Visitor

; -} - -impl + Clone> Visit

for Rc { - fn visit(&self, v: &mut V) - where - V: Visitor

, - { - T::visit(self, v) - } -} - -impl> Visit

for Option { - fn visit(&self, v: &mut V) - where - V: Visitor

, - { - if let Some(inner) = self { - inner.visit(v); - } - } -} - -impl> Visit

for Vec { - fn visit(&self, v: &mut V) - where - V: Visitor

, - { - for inner in self.iter() { - inner.visit(v); - } - } -} - -impl Visit

for Prg

{ - fn visit(&self, v: &mut V) - where - V: Visitor

, - { - let Prg { decls } = self; - decls.visit(v); - v.visit_prg(decls) - } -} - -impl Visit

for Decls

{ - fn visit(&self, v: &mut V) - where - V: Visitor

, - { - let Decls { map, lookup_table } = self; - for decl in map.values() { - decl.visit(v) - } - v.visit_decls(map, lookup_table) - } -} - -impl Visit

for Decl

{ - fn visit(&self, v: &mut V) - where - V: Visitor

, - { - match self { - Decl::Data(inner) => { - inner.visit(v); - v.visit_decl_data(inner) - } - Decl::Codata(inner) => { - inner.visit(v); - v.visit_decl_codata(inner) - } - Decl::Ctor(inner) => { - inner.visit(v); - v.visit_decl_ctor(inner) - } - Decl::Dtor(inner) => { - inner.visit(v); - v.visit_decl_dtor(inner) - } - Decl::Def(inner) => { - inner.visit(v); - v.visit_decl_def(inner) - } - Decl::Codef(inner) => { - inner.visit(v); - v.visit_decl_codef(inner) - } - Decl::Let(inner) => { - inner.visit(v); - v.visit_decl_let(inner) - } - } - v.visit_decl(self) - } -} - -impl Visit

for Data

{ - fn visit(&self, v: &mut V) - where - V: Visitor

, - { - let Data { info, doc, name, attr, typ, ctors } = self; - typ.visit(v); - v.visit_info(info); - v.visit_data(info, doc, name, attr, typ, ctors) - } -} - -impl Visit

for Codata

{ - fn visit(&self, v: &mut V) - where - V: Visitor

, - { - let Codata { info, doc, name, attr, typ, dtors } = self; - typ.visit(v); - v.visit_info(info); - v.visit_codata(info, doc, name, attr, typ, dtors) - } -} - -impl Visit

for TypAbs

{ - fn visit(&self, v: &mut V) - where - V: Visitor

, - { - let TypAbs { params } = self; - v.visit_telescope(¶ms.params, |v, param| param.visit(v), |_| ()); - v.visit_typ_abs(params) - } -} - -impl Visit

for Ctor

{ - fn visit(&self, v: &mut V) - where - V: Visitor

, - { - let Ctor { info, doc, name, params, typ } = self; - v.visit_telescope(¶ms.params, |v, param| param.visit(v), |v| typ.visit(v)); - v.visit_info(info); - v.visit_ctor(info, doc, name, params, typ) - } -} - -impl Visit

for Dtor

{ - fn visit(&self, v: &mut V) - where - V: Visitor

, - { - let Dtor { info, doc, name, params, self_param, ret_typ } = self; - v.visit_telescope( - ¶ms.params, - |v, param| param.visit(v), - |v| { - v.visit_info(&self_param.info); - self_param.typ.visit(v); - v.visit_self_param(&self_param.info, &self_param.name, &self_param.typ, |v| { - ret_typ.visit(v); - }); - }, - ); - v.visit_info(info); - v.visit_dtor(info, doc, name, params, self_param, ret_typ) - } -} - -impl Visit

for Def

{ - fn visit(&self, v: &mut V) - where - V: Visitor

, - { - let Def { info, doc, name, attr, params, self_param, ret_typ, body } = self; - v.visit_telescope( - ¶ms.params, - |v, param| param.visit(v), - |v| { - v.visit_info(&self_param.info); - self_param.typ.visit(v); - v.visit_self_param(&self_param.info, &self_param.name, &self_param.typ, |v| { - ret_typ.visit(v); - }); - body.visit(v); - }, - ); - v.visit_info(info); - v.visit_def(info, doc, name, attr, params, self_param, ret_typ, body) - } -} - -impl Visit

for Codef

{ - fn visit(&self, v: &mut V) - where - V: Visitor

, - { - let Codef { info, doc, name, attr, params, typ, body } = self; - v.visit_telescope( - ¶ms.params, - |v, param| param.visit(v), - |v| { - typ.visit(v); - body.visit(v); - }, - ); - v.visit_info(info); - v.visit_codef(info, doc, name, attr, params, typ, body) - } -} - -impl Visit

for Let

{ - fn visit(&self, v: &mut V) - where - V: Visitor

, - { - let Let { info, doc, name, attr, params, typ, body } = self; - v.visit_telescope( - ¶ms.params, - |v, param| param.visit(v), - |v| { - typ.visit(v); - body.visit(v); - }, - ); - v.visit_info(info); - v.visit_let(info, doc, name, attr, params, typ, body) - } -} - -impl Visit

for Match

{ - fn visit(&self, v: &mut V) - where - V: Visitor

, - { - let Match { info, cases, omit_absurd } = self; - cases.visit(v); - v.visit_info(info); - v.visit_match(info, cases, *omit_absurd) - } -} - -impl Visit

for Case

{ - fn visit(&self, v: &mut V) - where - V: Visitor

, - { - let Case { info, name, args, body } = self; - let TelescopeInst { params } = args; - v.visit_telescope_inst(params, |v, arg| arg.visit(v), |v| body.visit(v)); - v.visit_info(info); - v.visit_case(info, name, args, body) - } -} - -impl Visit

for TypApp

{ - fn visit(&self, v: &mut V) - where - V: Visitor

, - { - let TypApp { info, name, args } = self; - args.visit(v); - v.visit_type_info(info); - v.visit_typ_app(info, name, args) - } -} - -impl Visit

for Exp

{ - fn visit(&self, v: &mut V) - where - V: Visitor

, - { - match self { - Exp::Var { info, name, ctx, idx } => { - v.visit_type_info(info); - v.visit_idx(idx); - v.visit_ctx(ctx); - v.visit_exp_var(info, name, ctx, idx) - } - Exp::TypCtor { info, name, args } => { - args.visit(v); - v.visit_type_info(info); - v.visit_exp_typ_ctor(info, name, args) - } - Exp::Ctor { info, name, args } => { - args.visit(v); - v.visit_type_info(info); - v.visit_exp_ctor(info, name, args) - } - Exp::Dtor { info, exp, name, args } => { - exp.visit(v); - args.visit(v); - v.visit_type_info(info); - v.visit_exp_dtor(info, exp, name, args) - } - Exp::Anno { info, exp, typ } => { - exp.visit(v); - typ.visit(v); - v.visit_type_info(info); - v.visit_exp_anno(info, exp, typ) - } - Exp::Type { info } => { - v.visit_type_info(info); - v.visit_exp_type(info) - } - Exp::Match { info, ctx, name, on_exp, motive, ret_typ, body } => { - v.visit_type_app_info(info); - v.visit_ctx(ctx); - on_exp.visit(v); - body.visit(v); - if let Some(m) = motive { - m.visit(v); - } - v.visit_typ(ret_typ); - v.visit_exp_match(info, ctx, name, on_exp, ret_typ, body) - } - Exp::Comatch { info, ctx, name, is_lambda_sugar, body } => { - v.visit_type_app_info(info); - v.visit_ctx(ctx); - body.visit(v); - v.visit_exp_comatch(info, ctx, name, is_lambda_sugar, body) - } - Exp::Hole { info } => { - v.visit_type_info(info); - v.visit_exp_hole(info) - } - } - } -} - -impl Visit

for Motive

{ - fn visit(&self, v: &mut V) - where - V: Visitor

, - { - let Motive { info, param, ret_typ } = self; - v.visit_info(info); - param.visit(v); - v.visit_motive_param(param, |v, param| { - ret_typ.visit(v); - v.visit_motive(info, param, ret_typ) - }) - } -} - -impl Visit

for Param

{ - fn visit(&self, v: &mut V) - where - V: Visitor

, - { - let Param { name, typ } = self; - typ.visit(v); - v.visit_param(name, typ) - } -} - -impl Visit

for ParamInst

{ - fn visit(&self, v: &mut V) - where - V: Visitor

, - { - let ParamInst { info, name, typ } = self; - v.visit_type_info(info); - v.visit_typ(typ); - v.visit_param_inst(info, name, typ) - } -} - -impl Visit

for Args

{ - fn visit(&self, v: &mut V) - where - V: Visitor

, - { - let Args { args } = self; - args.visit(v) - } -} From fcd0090125bb26ca0cb6c3570f35695303d4def3 Mon Sep 17 00:00:00 2001 From: David Binder Date: Tue, 16 Apr 2024 17:15:46 +0200 Subject: [PATCH 4/6] Almost finish rewrite --- lang/lifting/src/fv.rs | 184 +++++++++++++++++++++-------------------- 1 file changed, 96 insertions(+), 88 deletions(-) diff --git a/lang/lifting/src/fv.rs b/lang/lifting/src/fv.rs index bf4472ea9..3622067bd 100644 --- a/lang/lifting/src/fv.rs +++ b/lang/lifting/src/fv.rs @@ -1,7 +1,6 @@ use std::cmp; use std::rc::Rc; -use codespan::Span; use derivative::Derivative; use syntax::common::*; @@ -24,46 +23,110 @@ pub fn free_vars(arg: &T, ctx: &TypeCtx) -> FreeVars { } trait FV { - fn visit_fv(&self,v: &mut USTVisitor); + fn visit_fv(&self, v: &mut USTVisitor); } impl FV for ust::Exp { - fn visit_fv(&self,v: &mut USTVisitor) { + fn visit_fv(&self, v: &mut USTVisitor) { match self { - ust::Exp::Anno { info, exp, typ } => todo!(), - ust::Exp::Var { info, name, ctx, idx } => todo!(), - ust::Exp::Comatch { info, ctx, name, is_lambda_sugar, body } => todo!(), - ust::Exp::Ctor { info, name, args } => todo!(), - ust::Exp::Dtor { info, exp, name, args } => todo!(), - ust::Exp::TypCtor { info, name, args } => todo!(), - ust::Exp::Hole { info } => todo!(), - ust::Exp::Type { info } => todo!(), - ust::Exp::Match { info, ctx, name, on_exp, motive, ret_typ, body } => todo!(), + ust::Exp::Anno { info: _, exp, typ } => { + exp.visit_fv(v); + typ.visit_fv(v) + } + ust::Exp::Var { info: _, name, ctx: _, idx } => { + // We use the level context to convert the De Bruijn index to a De Bruijn level + let lvl = v.lvl_ctx.idx_to_lvl(*idx); + // If the variable is considered free (based on the cutoff), we look up its type in the typing context + // The typing context contains the types for all free variables where lvl < cutoff + if lvl.fst < v.cutoff { + let typ = v + .type_ctx + .lookup(lvl) + .typ + .shift(((v.lvl_ctx.len() - v.type_ctx.len()) as isize, 0)); + v.add_fv(name.clone(), lvl, typ, v.lvl_ctx.clone()) + } + } + ust::Exp::Comatch { info: _, ctx: _, name: _, is_lambda_sugar: _, body } => { + body.visit_fv(v) + } + ust::Exp::Ctor { info: _, name: _, args } => args.visit_fv(v), + ust::Exp::Dtor { info: _, exp, name: _, args } => { + exp.visit_fv(v); + args.visit_fv(v); + } + ust::Exp::TypCtor { info: _, name: _, args } => args.visit_fv(v), + ust::Exp::Hole { info: _ } => {} + ust::Exp::Type { info: _ } => {} + ust::Exp::Match { info: _, ctx: _, name: _, on_exp, motive, ret_typ: _, body } => { + on_exp.visit_fv(v); + motive.visit_fv(v); + body.visit_fv(v) + } + } + } +} + +impl FV for ust::Args { + fn visit_fv(&self, v: &mut USTVisitor) { + let ust::Args { args } = self; + for arg in args { + arg.visit_fv(v) } } } impl FV for ust::Match { - fn visit_fv(&self,v: &mut USTVisitor) { - todo!() + fn visit_fv(&self, v: &mut USTVisitor) { + let ust::Match { info: _, cases, omit_absurd: _ } = self; + for case in cases { + case.visit_fv(v) + } + } +} + +impl FV for ust::Case { + fn visit_fv(&self, _v: &mut USTVisitor) { + let ust::Case { info: _, name: _, args: _, body: _ } = self; + + //body.visit_fv(v); + // TODO: The visitor context must be extended somehow. } } impl FV for ust::Motive { - fn visit_fv(&self,v: &mut USTVisitor) { - todo!() + fn visit_fv(&self, v: &mut USTVisitor) { + let ust::Motive { info: _, param, ret_typ } = self; + param.visit_fv(v); + ret_typ.visit_fv(v); + } +} + +impl FV for ust::ParamInst { + fn visit_fv(&self, _v: &mut USTVisitor) { + //contains no type info for ust. } } impl FV for ust::TypApp { - fn visit_fv(&self,v: &mut USTVisitor) { - todo!() + fn visit_fv(&self, v: &mut USTVisitor) { + let ust::TypApp { info: _, name: _, args } = self; + args.visit_fv(v) } } -impl FV for Rc { - fn visit_fv(&self,v: &mut USTVisitor) { - todo!() +impl FV for Rc { + fn visit_fv(&self, v: &mut USTVisitor) { + (**self).visit_fv(v) + } +} + +impl FV for Option { + fn visit_fv(&self, v: &mut USTVisitor) { + match self { + None => {} + Some(x) => x.visit_fv(v), + } } } @@ -216,18 +279,18 @@ struct USTVisitor<'a> { lvl_ctx: LevelCtx, } -// impl<'a> USTVisitor<'a> { -// /// Add a free variable as well as all free variables its type -// fn add_fv(&mut self, name: ust::Ident, lvl: Lvl, typ: Rc, ctx: LevelCtx) { -// // Add the free variable -// let fv = FreeVar { name, lvl, typ: typ.clone(), ctx }; -// if self.fvs.insert(fv) { -// // If it has not already been added: -// // Find all free variables in the type of the free variable -// typ.visit(self); -// } -// } -// } +impl<'a> USTVisitor<'a> { + /// Add a free variable as well as all free variables its type + fn add_fv(&mut self, name: ust::Ident, lvl: Lvl, typ: Rc, ctx: LevelCtx) { + // Add the free variable + let fv = FreeVar { name, lvl, typ: typ.clone(), ctx }; + if self.fvs.insert(fv) { + // If it has not already been added: + // Find all free variables in the type of the free variable + typ.visit_fv(self); + } + } +} impl<'a> BindContext for USTVisitor<'a> { type Ctx = LevelCtx; @@ -237,61 +300,6 @@ impl<'a> BindContext for USTVisitor<'a> { } } -// impl<'b> Visitor for USTVisitor<'b> { -// fn visit_telescope<'a, I, F1, F2>(&mut self, params: I, f_acc: F1, f_inner: F2) -// where -// I: IntoIterator, -// F1: Fn(&mut Self, &'a ust::Param), -// F2: FnOnce(&mut Self), -// { -// self.ctx_visit_telescope(params, f_acc, f_inner) -// } - -// fn visit_telescope_inst<'a, I, F1, F2>(&mut self, params: I, f_acc: F1, f_inner: F2) -// where -// I: IntoIterator, -// F1: Fn(&mut Self, &'a ust::ParamInst), -// F2: FnOnce(&mut Self), -// { -// self.ctx_visit_telescope_inst(params, f_acc, f_inner) -// } - -// fn visit_motive_param(&mut self, param: &ust::ParamInst, f_inner: F) -> X -// where -// F: FnOnce(&mut Self, &ust::ParamInst) -> X, -// { -// self.ctx_visit_motive_param(param, f_inner) -// } - -// fn visit_self_param( -// &mut self, -// info: &Option, -// name: &Option, -// typ: &ust::TypApp, -// f_inner: F, -// ) -> X -// where -// F: FnOnce(&mut Self) -> X, -// { -// self.ctx_visit_self_param(info, name, typ, f_inner) -// } - -// fn visit_exp_var(&mut self, _info: &Option, name: &ust::Ident, _ctx: &(), idx: &Idx) { -// // We use the level context to convert the De Bruijn index to a De Bruijn level -// let lvl = self.lvl_ctx.idx_to_lvl(*idx); -// // If the variable is considered free (based on the cutoff), we look up its type in the typing context -// // The typing context contains the types for all free variables where lvl < cutoff -// if lvl.fst < self.cutoff { -// let typ = self -// .type_ctx -// .lookup(lvl) -// .typ -// .shift(((self.lvl_ctx.len() - self.type_ctx.len()) as isize, 0)); -// self.add_fv(name.clone(), lvl, typ, self.lvl_ctx.clone()) -// } -// } -// } - /// Substitution of free variables #[derive(Clone, Debug)] pub struct FVSubst { From 93f26a8b011abfd0f0496e41348068156e516c34 Mon Sep 17 00:00:00 2001 From: David Binder Date: Wed, 17 Apr 2024 17:14:06 +0200 Subject: [PATCH 5/6] Fix warnings --- lang/lifting/src/fv.rs | 4 ++-- lang/syntax/src/common/de_bruijn.rs | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/lang/lifting/src/fv.rs b/lang/lifting/src/fv.rs index 3622067bd..9566857fc 100644 --- a/lang/lifting/src/fv.rs +++ b/lang/lifting/src/fv.rs @@ -22,7 +22,7 @@ pub fn free_vars(arg: &T, ctx: &TypeCtx) -> FreeVars { FreeVars { fvs: v.fvs, cutoff: ctx.len() } } -trait FV { +pub trait FV { fn visit_fv(&self, v: &mut USTVisitor); } @@ -268,7 +268,7 @@ impl Ord for FreeVar { } /// Visitor that collects free variables in an untyped syntax tree -struct USTVisitor<'a> { +pub struct USTVisitor<'a> { /// Set of collected free variables fvs: HashSet, /// The De-Bruijn level (fst index) up to which a variable counts as free diff --git a/lang/syntax/src/common/de_bruijn.rs b/lang/syntax/src/common/de_bruijn.rs index ce244fdd9..537812cde 100644 --- a/lang/syntax/src/common/de_bruijn.rs +++ b/lang/syntax/src/common/de_bruijn.rs @@ -95,7 +95,7 @@ pub trait Leveled { /// Note: We use two-level de Bruijn indices. The cutoff-range only applies to /// the first element of a two-level de Bruijn index. /// -/// Ref: https://www.cs.cornell.edu/courses/cs4110/2018fa/lectures/lecture15.pdf +/// Ref: pub trait Shift: Sized { /// Shift all open variables in `self` by the the value indicated with the /// `by` argument. From 691142f6385766dbff9853d1c37d25431e98d4c0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tim=20S=C3=BCberkr=C3=BCb?= Date: Sun, 21 Apr 2024 15:44:40 +0200 Subject: [PATCH 6/6] Finish removal of generic visitor --- lang/lifting/src/fv.rs | 18 ++++--- lang/syntax/src/ctx/mod.rs | 2 - lang/syntax/src/ctx/visit.rs | 101 ----------------------------------- 3 files changed, 10 insertions(+), 111 deletions(-) delete mode 100644 lang/syntax/src/ctx/visit.rs diff --git a/lang/lifting/src/fv.rs b/lang/lifting/src/fv.rs index 9566857fc..c44cab51f 100644 --- a/lang/lifting/src/fv.rs +++ b/lang/lifting/src/fv.rs @@ -86,19 +86,22 @@ impl FV for ust::Match { } impl FV for ust::Case { - fn visit_fv(&self, _v: &mut USTVisitor) { - let ust::Case { info: _, name: _, args: _, body: _ } = self; + fn visit_fv(&self, v: &mut USTVisitor) { + let ust::Case { info: _, name: _, args, body } = self; - //body.visit_fv(v); - // TODO: The visitor context must be extended somehow. + v.bind_iter(args.params.iter(), |v| { + body.visit_fv(v); + }) } } impl FV for ust::Motive { fn visit_fv(&self, v: &mut USTVisitor) { let ust::Motive { info: _, param, ret_typ } = self; + param.visit_fv(v); - ret_typ.visit_fv(v); + + v.bind_single(param, |v| ret_typ.visit_fv(v)) } } @@ -123,9 +126,8 @@ impl FV for Rc { impl FV for Option { fn visit_fv(&self, v: &mut USTVisitor) { - match self { - None => {} - Some(x) => x.visit_fv(v), + if let Some(x) = self { + x.visit_fv(v) } } } diff --git a/lang/syntax/src/ctx/mod.rs b/lang/syntax/src/ctx/mod.rs index 630b2e075..8a039ff0f 100644 --- a/lang/syntax/src/ctx/mod.rs +++ b/lang/syntax/src/ctx/mod.rs @@ -3,9 +3,7 @@ mod levels; mod map; pub mod map_idx; pub mod values; -mod visit; pub use def::*; pub use levels::*; pub use map::*; -pub use visit::*; diff --git a/lang/syntax/src/ctx/visit.rs b/lang/syntax/src/ctx/visit.rs deleted file mode 100644 index 668c74e7b..000000000 --- a/lang/syntax/src/ctx/visit.rs +++ /dev/null @@ -1,101 +0,0 @@ -use std::rc::Rc; - -use crate::ctx::*; -use crate::generic::*; -use codespan::Span; - -pub trait VisitCtxExt { - fn ctx_visit_telescope<'a, I, F1, F2>(&mut self, params: I, f_acc: F1, f_inner: F2) - where - P: 'a, - I: IntoIterator>, - F1: Fn(&mut Self, &'a Param

), - F2: FnOnce(&mut Self); - - fn ctx_visit_telescope_inst<'a, I, F1, F2>(&mut self, params: I, f_acc: F1, f_inner: F2) - where - P: 'a, - I: IntoIterator>, - F1: Fn(&mut Self, &'a ParamInst

), - F2: FnOnce(&mut Self); - - fn ctx_visit_motive_param(&mut self, param: &ParamInst

, f_inner: F) -> X - where - F: FnOnce(&mut Self, &ParamInst

) -> X; - - fn ctx_visit_self_param( - &mut self, - info: &Option, - name: &Option, - typ: &TypApp

, - f_inner: F, - ) -> X - where - F: FnOnce(&mut Self) -> X; -} - -impl VisitCtxExt

for C -where - for<'a> &'a Param

: ContextElem, - for<'a> &'a ParamInst

: ContextElem, -{ - fn ctx_visit_telescope<'a, I, F1, F2>(&mut self, params: I, f_acc: F1, f_inner: F2) - where - P: 'a, - I: IntoIterator>, - F1: Fn(&mut Self, &'a Param

), - F2: FnOnce(&mut Self), - { - self.bind_fold( - params.into_iter(), - Vec::new(), - |this, mut params_out, param| { - f_acc(this, param); - params_out.push(()); - params_out - }, - |this, _params| f_inner(this), - ) - } - - fn ctx_visit_telescope_inst<'a, I, F1, F2>(&mut self, params: I, f_acc: F1, f_inner: F2) - where - P: 'a, - I: IntoIterator>, - F1: Fn(&mut Self, &'a ParamInst

), - F2: FnOnce(&mut Self), - { - self.bind_fold( - params.into_iter(), - Vec::new(), - |this, mut params_out, param| { - f_acc(this, param); - params_out.push(()); - params_out - }, - |this, _params| f_inner(this), - ) - } - - fn ctx_visit_motive_param(&mut self, param: &ParamInst

, f_inner: F) -> X - where - F: FnOnce(&mut Self, &ParamInst

) -> X, - { - self.bind_single(param, |ctx| f_inner(ctx, param)) - } - - fn ctx_visit_self_param( - &mut self, - _info: &Option, - name: &Option, - typ: &TypApp

, - f_inner: F, - ) -> X - where - F: FnOnce(&mut Self) -> X, - { - let param = Param { name: name.clone().unwrap_or_default(), typ: Rc::new(typ.to_exp()) }; - - self.bind_single(¶m, |ctx| f_inner(ctx)) - } -}