<commit_before>use super::TyCtxt;

use super::super::core::*;
use super::name_generator::*;

/// A context with the needed state to deal with operations that process an inductive definition.
pub struct RecursorCx<'i, 'tcx> {
    ty_cx: &'tcx mut TyCtxt,
    inductive_ty: &'i Data,
    ind_hyp: Name,
}

impl<'i, 'tcx> RecursorCx<'i, 'tcx> {
    fn new(ty_cx: &'tcx mut TyCtxt, inductive_ty: &'i Data) -> RecursorCx<'i, 'tcx> {

        let mut rcx = RecursorCx {
            ty_cx: ty_cx,
            inductive_ty: inductive_ty,
            ind_hyp: inductive_ty.name.clone(),
        };

        let ty = rcx.eta_expand();

        let ty = rcx.with_params(ty);
        let ind_hyp = rcx.ty_cx.local_with_repr("C".to_string(),
            Term::abstract_pi(vec![rcx.ty_cx.local_with_repr("".to_string(), ty)],
                Term::Type));

        rcx.ind_hyp = ind_hyp;

        rcx
    }

    fn eta_expand(&self) -> Term {
        let mut pi = self.inductive_ty.ty.clone();
        let mut result = self.inductive_ty.name.to_term();
        let mut i = 0;
        let mut locals = vec![];
        while let Term::Forall { ty, term, .. } = pi {
            let local = self.ty_cx.local_with_repr(format!("x{}", 0), *ty);
            locals.push(local);
            pi = *term;
        }
        Term::abstract_lambda(
            locals.clone(),
            Term::apply_all(result, locals.into_iter().map(|t| t.to_term()).collect()))
    }

    pub fn with_params(&self, term: Term) -> Term {
        let params = self.inductive_ty
                         .parameters
                         .iter()
                         .map(|x| x.to_term())
                         .collect();

        Term::apply_all(term, params).whnf()
    }

    fn is_recursive_arg(&self, term: &Term) -> bool {
        match term.head() {
            None => false,
            Some(h) => h == self.inductive_ty.name.to_term(),
        }
    }

    pub fn minor_premise_for(&mut self, ind_hyp: &Name, ctor: &(Name, Term)) -> Term {
        // Apply the constructor name to the parameters.
        let ctor_with_params =
            self.with_params(ctor.0.to_term());

        // Apply the constructor type to the parameters.
        let mut ctor_ty_with_params =
            self.with_params(ctor.1.clone());

        let mut i = 0;
        let mut binders = Vec::new();
        let mut arguments = Vec::new();
        let mut pi = &ctor_ty_with_params;

        while let &Term::Forall { ref ty, ref term, .. } = pi {
            // Create a local with a fresh name and type of the binder.
            let arg_local =
                self.ty_cx.local_with_repr(
                    format!("a{}", i),
                    *ty.clone());

            // Add this to the list of binders (a0 : A) (a1 : List A)
            binders.push(arg_local.clone());
            // (a0 : A) (a1 : List A) -> C a1 -> C (Cons a0 a1)

            // If this is a recursive argument we all need to generate a piece of proof
            // for that case for example `C a1`.
            if self.is_recursive_arg(&*ty) {
                let local_x =
                    self.ty_cx.local_with_repr(
                        "".to_string(),
                        Term::apply(ind_hyp.to_term(), arg_local.to_term()));

                 arguments.push(local_x);
            }

            pi = &**term;
            i += 1;
        }

        let c_for_ctor = Term::apply(
            ind_hyp.to_term(),
            Term::apply_all(
                ctor_with_params,
                binders.iter()
                       .map(|x| x.to_term())
                       .collect()));

        Term::abstract_pi(
            binders,
            Term::abstract_pi(
                arguments,
                c_for_ctor))
    }

    pub fn construct_recursor(&self,
                              minor_premises: Vec<Name>,
                              major_premise_args: Vec<Name>,
                              major_premise: Term) -> (Term, Term) {
        let ind_hyp = self.ind_hyp.clone();
        let params =
            self.inductive_ty
                .parameters
                .clone();

        let recursor_ty =
            Term::abstract_pi(
                params.clone(),
                Term::abstract_pi(vec![ind_hyp.clone()],
                    Term::abstract_pi(minor_premises.clone(),
                        Term::abstract_pi(major_premise_args.clone(),
                            major_premise))));

        let mut recursor_terms = vec![ind_hyp.clone().to_term()];
        recursor_terms.extend(minor_premises.iter().map(|x| x.to_term()));
        recursor_terms.extend(major_premise_args.iter().map(|x| x.to_term()));

        let recursor_body =
            Term::abstract_lambda(
                params.clone(),
                Term::abstract_lambda(
                    vec![ind_hyp.clone()],
                    Term::abstract_lambda(
                        minor_premises,
                        Term::abstract_lambda(
                            major_premise_args,
                            Term::Recursor(
                                self.inductive_ty.name.clone(),
                                1, // this needs to be fixed
                                recursor_terms)))));

        (recursor_ty, recursor_body)
    }

    pub fn major_premise(&self) -> (Vec<Name>, Term) {
        let mut data_type_ty = self.with_params(
            self.inductive_ty.ty.clone());

        let mut arguments = Vec::new();
        while let Term::Forall { ty, term, .. } = data_type_ty {
            arguments.push(*ty.clone());
            data_type_ty = *term;
        }

        let mut arguments: Vec<_> = arguments.into_iter()
                                         .enumerate()
                                         .map(|(i, ty)|
                                            self.ty_cx.local_with_repr(format!("a{}", i), ty))
                                         .collect();
        let scrutinee =
            Term::apply_all(
                self.with_params(self.inductive_ty.name.to_term()),
                arguments.iter().map(|x| x.to_term()).collect());

        arguments.push(self.ty_cx.local_with_repr(
            "c".to_string(),
            scrutinee));

        let premise =
            self.ind_hyp.to_term();

        let premise = Term::apply_all(
            premise,
            arguments.
            iter().
            map(|a| a.to_term()).
            collect());

        (arguments, premise)
    }
}

/// Construct a recursor for `data_type`.
pub fn make_recursor(ty_cx: &mut TyCtxt, data_type: &Data) {
    let mut rcx = RecursorCx::new(ty_cx, data_type);

    let ind_hyp = rcx.ind_hyp.clone();

    let params = data_type.parameters.clone();

    let minor_premises =
        data_type.ctors
                 .iter()
                 .map(|ctor| {
                     let p = rcx.minor_premise_for(&ind_hyp, ctor);
                     rcx.ty_cx.local_with_repr("".to_string(), p)
                 })
                 .collect();

    let (tys, major_premise) =
        rcx.major_premise();

    let (recursor_ty, recursor_body) =
        rcx.construct_recursor(
            minor_premises,
            tys,
            major_premise);

    let recursor_name = data_type.name.in_scope("rec".to_string()).unwrap();

    rcx.ty_cx
       .definitions
       .insert(recursor_name, (recursor_ty, recursor_body));
}
<commit_msg>Recursors work for data types with parameters<commit_after>use super::TyCtxt;

use super::super::core::*;
use super::name_generator::*;

/// A context with the needed state to deal with operations that process an inductive definition.
pub struct RecursorCx<'i, 'tcx> {
    ty_cx: &'tcx mut TyCtxt,
    inductive_ty: &'i Data,
    ind_hyp: Name,
}

impl<'i, 'tcx> RecursorCx<'i, 'tcx> {
    fn new(ty_cx: &'tcx mut TyCtxt, inductive_ty: &'i Data) -> RecursorCx<'i, 'tcx> {

        let mut rcx = RecursorCx {
            ty_cx: ty_cx,
            inductive_ty: inductive_ty,
            ind_hyp: inductive_ty.name.clone(),
        };

        let ty = rcx.make_ind_hyp_ty();

        let ty = rcx.with_params(ty);
        let ind_hyp = rcx.ty_cx.local_with_repr("C".to_string(),
            Term::abstract_pi(vec![rcx.ty_cx.local_with_repr("".to_string(), ty)],
                Term::Type));

        rcx.ind_hyp = ind_hyp;

        rcx
    }

    fn  make_ind_hyp_ty(&self) -> Term {
        let mut pi = self.inductive_ty.ty.clone();
        let mut result = self.inductive_ty.name.to_term();
        let mut i = 0;
        let mut locals = vec![];
        while let Term::Forall { ty, term, .. } = pi {
            let local = self.ty_cx.local_with_repr(format!("x{}", 0), *ty);
            locals.push(local);
            pi = *term;
        }

        let applied_ty =
            Term::apply_all(
                result,
                locals.into_iter().map(|t| t.to_term()).collect());

        locals.push(
            self.ty_cx.local_with_repr("".to_string(), applied_ty));

        Term::abstract_pi(
            locals.clone(),
            Term::Type)
    }

    pub fn with_params(&self, term: Term) -> Term {
        let params = self.inductive_ty
                         .parameters
                         .iter()
                         .map(|x| x.to_term())
                         .collect();

        Term::apply_all(term, params).whnf()
    }

    fn is_recursive_arg(&self, term: &Term) -> bool {
        match term.head() {
            None => false,
            Some(h) => h == self.inductive_ty.name.to_term(),
        }
    }

    pub fn minor_premise_for(&mut self, ind_hyp: &Name, ctor: &(Name, Term)) -> Term {
        // Apply the constructor name to the parameters.
        let ctor_with_params =
            self.with_params(ctor.0.to_term());

        // Apply the constructor type to the parameters.
        let mut ctor_ty_with_params =
            self.with_params(ctor.1.clone());

        let mut i = 0;
        let mut binders = Vec::new();
        let mut arguments = Vec::new();
        let mut pi = &ctor_ty_with_params;

        while let &Term::Forall { ref ty, ref term, .. } = pi {
            // Create a local with a fresh name and type of the binder.
            let arg_local =
                self.ty_cx.local_with_repr(
                    format!("a{}", i),
                    *ty.clone());

            // Add this to the list of binders (a0 : A) (a1 : List A)
            binders.push(arg_local.clone());
            // (a0 : A) (a1 : List A) -> C a1 -> C (Cons a0 a1)

            // If this is a recursive argument we all need to generate a piece of proof
            // for that case for example `C a1`.
            if self.is_recursive_arg(&*ty) {
                let local_x =
                    self.ty_cx.local_with_repr(
                        "".to_string(),
                        Term::apply(ind_hyp.to_term(), arg_local.to_term()));

                 arguments.push(local_x);
            }

            pi = &**term;
            i += 1;
        }

        let c_for_ctor = Term::apply(
            ind_hyp.to_term(),
            Term::apply_all(
                ctor_with_params,
                binders.iter()
                       .map(|x| x.to_term())
                       .collect()));

        Term::abstract_pi(
            binders,
            Term::abstract_pi(
                arguments,
                c_for_ctor))
    }

    pub fn construct_recursor(&self,
                              minor_premises: Vec<Name>,
                              major_premise_args: Vec<Name>,
                              major_premise: Term) -> (Term, Term) {
        let ind_hyp = self.ind_hyp.clone();
        let params =
            self.inductive_ty
                .parameters
                .clone();

        let recursor_ty =
            Term::abstract_pi(
                params.clone(),
                Term::abstract_pi(vec![ind_hyp.clone()],
                    Term::abstract_pi(minor_premises.clone(),
                        Term::abstract_pi(major_premise_args.clone(),
                            major_premise))));

        let mut recursor_terms = vec![ind_hyp.clone().to_term()];
        recursor_terms.extend(minor_premises.iter().map(|x| x.to_term()));
        recursor_terms.extend(major_premise_args.iter().map(|x| x.to_term()));

        let recursor_body =
            Term::abstract_lambda(
                params.clone(),
                Term::abstract_lambda(
                    vec![ind_hyp.clone()],
                    Term::abstract_lambda(
                        minor_premises,
                        Term::abstract_lambda(
                            major_premise_args,
                            Term::Recursor(
                                self.inductive_ty.name.clone(),
                                1, // this needs to be fixed
                                recursor_terms)))));

        (recursor_ty, recursor_body)
    }

    pub fn major_premise(&self) -> (Vec<Name>, Term) {
        let mut data_type_ty = self.with_params(
            self.inductive_ty.ty.clone());

        let mut arguments = Vec::new();
        while let Term::Forall { ty, term, .. } = data_type_ty {
            arguments.push(*ty.clone());
            data_type_ty = *term;
        }

        let mut arguments: Vec<_> = arguments.into_iter()
                                         .enumerate()
                                         .map(|(i, ty)|
                                            self.ty_cx.local_with_repr(format!("a{}", i), ty))
                                         .collect();
        let scrutinee =
            Term::apply_all(
                self.with_params(self.inductive_ty.name.to_term()),
                arguments.iter().map(|x| x.to_term()).collect());

        arguments.push(self.ty_cx.local_with_repr(
            "c".to_string(),
            scrutinee));

        let premise =
            self.ind_hyp.to_term();

        let premise = Term::apply_all(
            premise,
            arguments.
            iter().
            map(|a| a.to_term()).
            collect());

        (arguments, premise)
    }
}

/// Construct a recursor for `data_type`.
pub fn make_recursor(ty_cx: &mut TyCtxt, data_type: &Data) {
    let mut rcx = RecursorCx::new(ty_cx, data_type);

    let ind_hyp = rcx.ind_hyp.clone();

    let params = data_type.parameters.clone();

    let minor_premises =
        data_type.ctors
                 .iter()
                 .map(|ctor| {
                     let p = rcx.minor_premise_for(&ind_hyp, ctor);
                     rcx.ty_cx.local_with_repr("".to_string(), p)
                 })
                 .collect();

    let (tys, major_premise) =
        rcx.major_premise();

    let (recursor_ty, recursor_body) =
        rcx.construct_recursor(
            minor_premises,
            tys,
            major_premise);

    let recursor_name = data_type.name.in_scope("rec".to_string()).unwrap();

    rcx.ty_cx
       .definitions
       .insert(recursor_name, (recursor_ty, recursor_body));
}

{'fraction_non_alphanumeric': 0.1223088099326377, 'fraction_numerical': 0.001981244221371021, 'mean_word_length': 1.4428133569930635, 'pattern_counts': {'":': 0, '<': 19, '<?xml version=': 0, '>': 41, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 18, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3078790', 'n_tokens_mistral': 4667, 'n_tokens_neox': 4409, 'n_words': 921}