fungi-lang 0.1.62

/*! Expand static definitions (`Ident` cases of types, indices and effects). */

//use std::fmt;
use std::rc::Rc;
use crate::{normal, ast::*, bitype::*};

// TODO-Someday: Use Rc-based lists instead vectors to represent the
// bound variable lisctx, for cheaper O(1) clones.

pub fn expand_ctype(ctx:&Ctx, ct:CType) -> CType {
    match ct {
        CType::Lift(a) => {
            CType::Lift(expand_type(ctx,a))
        }
        CType::Arrow(a, ce) => {
            CType::Arrow(expand_type(ctx,a),
                         expand_ceffect_rec(ctx,ce))
        }
        CType::NoParse(s) => CType::NoParse(s)
    }
}

pub fn expand_effect_rec(ctx:&Ctx, eff:Rc<Effect>) -> Rc<Effect> {
    Rc::new(expand_effect(ctx, (*eff).clone()))
}

pub fn expand_effect(ctx:&Ctx, eff:Effect) -> Effect {
    match eff {
        Effect::WR(i, j) => {
            Effect::WR(expand_idxtm(ctx, i),
                       expand_idxtm(ctx, j))
        },
        Effect::NoParse(s) => Effect::NoParse(s)
    }
}

pub fn expand_ceffect_rec(ctx:&Ctx, ce:Rc<CEffect>) -> Rc<CEffect> {
    Rc::new(expand_ceffect(ctx, (*ce).clone()))
}

pub fn expand_ceffect(ctx:&Ctx, ce:CEffect) -> CEffect {
    match ce {
        CEffect::Cons(ct, eff) => {
            CEffect::Cons(expand_ctype(ctx, ct),
                          expand_effect(ctx, eff))
        }
        CEffect::ForallType(y, k, ce) => {
            CEffect::ForallType(y, k, expand_ceffect_rec(ctx, ce))
        }
        CEffect::ForallIdx(y, g, p, ce) => {
            CEffect::ForallIdx(y, g,
                               expand_prop(ctx, p),
                               expand_ceffect_rec(ctx, ce))
        }
        CEffect::NoParse(s) => CEffect::NoParse(s)
    }
}

pub fn expand_type_rec(ctx:&Ctx, a:Rc<Type>) -> Rc<Type> {
    Rc::new(expand_type(ctx, (*a).clone()))
}

pub fn expand_type(ctx:&Ctx, a:Type) -> Type {
    match a {
        Type::Unit => Type::Unit,
        Type::Abstract(x) => Type::Abstract(x),
        Type::Prim(pt) => Type::Prim(pt),
        Type::Ident(ident) => {
            match (ident.as_str(), ctx.lookup_type_def(&ident)) {
                ("Nat", _) => { Type::Prim(PrimType::Nat) }
                ("Bool", _) => { Type::Prim(PrimType::Bool) }
                ("String", _) => { Type::Prim(PrimType::String) },
                (_, Some(def)) => { 
                    // identifier is defined: place the definition with the use
                    Type::IdentDef(ident.clone(), Rc::new(def)) 
                }
                (_, None) => {
                    // identifier is not defined. error.
                    fgi_db!("expand_type: undefined type identifer: {}", ident);
                    Type::IdentUndef(ident)
                }
            }
        },
        Type::IdentUndef(x) => Type::IdentUndef(x),
        Type::IdentDef(ident, def) => Type::IdentDef(ident, def),
        Type::Var(y) => Type::Var(y),
        Type::Sum(a1, a2) => {
            Type::Sum(
                expand_type_rec(ctx, a1),
                expand_type_rec(ctx, a2),
            )
        }
        Type::Prod(a1, a2) => {
            Type::Prod(
                expand_type_rec(ctx, a1),
                expand_type_rec(ctx, a2),
            )
        }
        Type::Ref(i, a0) => {
            Type::Ref(
                expand_idxtm(ctx, i),
                expand_type_rec(ctx, a0),
            )
        }
        Type::Thk(i, ce) => {
            Type::Thk(
                expand_idxtm(ctx, i),
                expand_ceffect_rec(ctx, ce),
            )
        }        
        Type::IdxApp(a0, i) => {
            Type::IdxApp(
                expand_type_rec(ctx, a0),
                expand_idxtm(ctx, i)
            )
        }
        Type::TypeApp(a1, a2) => {
            Type::TypeApp(
                expand_type_rec(ctx, a1),
                expand_type_rec(ctx, a2)
            )
        }
        Type::Nm(i) => {
            Type::Nm(expand_idxtm(ctx, i))
        }
        Type::NmFn(n) => {
            Type::NmFn(expand_nmtm(ctx, n))
        }
        Type::Rec(y, a1) => {
            Type::Rec(y, expand_type_rec(ctx, a1))
        }
        Type::TypeFn(y, k, a1) => {
            Type::TypeFn(y, k, expand_type_rec(ctx, a1))
        }
        Type::IdxFn(y, g, a1) => {
            Type::IdxFn(y, g, expand_type_rec(ctx, a1))
        }
        Type::Exists(y, g, p, a1) => {
            Type::Exists(
                y, g,
                expand_prop(ctx, p),
                expand_type_rec(ctx, a1),
            )
        }
        Type::NoParse(s) => Type::NoParse(s)
    }
}

/// Substitute terms into propositions
pub fn expand_prop(ctx:&Ctx, p:Prop) -> Prop {
    match p {
        Prop::Tt => Prop::Tt,
        Prop::Equiv(i, j, g) => {
            Prop::Equiv(
                expand_idxtm(ctx, i),
                expand_idxtm(ctx, j),
                g)
        },
        Prop::Apart(i, j, g) => {
            Prop::Apart(
                expand_idxtm(ctx, i),
                expand_idxtm(ctx, j),
                g)
        },
        Prop::Conj(p1, p2) => {
            Prop::Conj(
                expand_prop_rec(ctx, p1),
                expand_prop_rec(ctx, p2),
            )
        }
        Prop::NoParse(s) => Prop::NoParse(s)
    }
}

/// Substitute terms into propositions
pub fn expand_prop_rec(ctx:&Ctx, p:Rc<Prop>) -> Rc<Prop> {
    Rc::new(expand_prop(ctx,(*p).clone()))
}

/// Substitute terms into index terms
pub fn expand_idxtm_rec(ctx:&Ctx, i:Rc<IdxTm>) -> Rc<IdxTm> {
    Rc::new(expand_idxtm(ctx, (*i).clone()))
}

/// Substitute terms into index terms
pub fn expand_idxtm(ctx:&Ctx, i:IdxTm) -> IdxTm {
    match i {
        IdxTm::Unknown => IdxTm::Unknown,
        // Variables and identifiers are lexically distinct
        IdxTm::Ident(y) => {
            match ctx.lookup_idxtm_def(&y) {
                Some(i) => expand_idxtm(ctx, i),
                _ => {
                    println!("undefined idxtm: {} in\n{:?}", y, ctx);
                    // Give up:
                    IdxTm::Ident(y)
                }
            }
        }
        IdxTm::WriteScope => {
            IdxTm::WriteScope
        },
        IdxTm::Var(y) => {
            IdxTm::Var(y)
        }
        IdxTm::Sing(n) => {
            IdxTm::Sing(expand_nmtm(ctx,n))
        },
        IdxTm::NmTm(n) => {
            IdxTm::NmTm(expand_nmtm(ctx,n))
        },
        IdxTm::Unit  => IdxTm::Unit,
        IdxTm::Empty => IdxTm::Empty,
        IdxTm::NmSet(s) => {
            let mut terms = vec![];
            for tm in s.terms {
                let tm = match tm {
                    normal::NmSetTm::Single(n) => {
                        normal::NmSetTm::Single(expand_nmtm(ctx,n))
                    },
                    normal::NmSetTm::Subset(i) => {
                        normal::NmSetTm::Subset(expand_idxtm(ctx,i))
                    }
                };
                terms.push(tm)
            }
            IdxTm::NmSet(normal::NmSet{cons:s.cons, terms:terms})
        }
        IdxTm::Apart(i, j) => {
            IdxTm::Apart(expand_idxtm_rec(ctx,i),
                         expand_idxtm_rec(ctx,j))
        }
        IdxTm::Union(i, j) => {
            IdxTm::Union(expand_idxtm_rec(ctx,i),
                         expand_idxtm_rec(ctx,j))
        }
        IdxTm::Bin(i, j) => {
            IdxTm::Bin(expand_idxtm_rec(ctx,i),
                       expand_idxtm_rec(ctx,j))
        }
        IdxTm::Pair(i, j) => {
            IdxTm::Pair(expand_idxtm_rec(ctx,i),
                        expand_idxtm_rec(ctx,j))
        }
        IdxTm::Proj1(i) => {
            IdxTm::Proj1(expand_idxtm_rec(ctx,i))
        }
        IdxTm::Proj2(i) => {
            IdxTm::Proj2(expand_idxtm_rec(ctx,i))
        }
        IdxTm::Lam(y,g,i) => {
            IdxTm::Lam(y,g,expand_idxtm_rec(ctx,i))
        }
        IdxTm::App(i, j) => {
            IdxTm::App(expand_idxtm_rec(ctx, i),
                       expand_idxtm_rec(ctx, j))
        }
        IdxTm::Map(n, j) => {
            IdxTm::Map(expand_nmtm_rec(ctx, n),
                       expand_idxtm_rec(ctx, j))
        }
        IdxTm::MapStar(n, j) => {
            IdxTm::MapStar(expand_nmtm_rec(ctx, n),
                           expand_idxtm_rec(ctx, j))
        }
        IdxTm::FlatMap(i, j) => {
            IdxTm::FlatMap(expand_idxtm_rec(ctx, i),
                           expand_idxtm_rec(ctx, j))
        }
        IdxTm::FlatMapStar(i, j) => {
            IdxTm::FlatMapStar(expand_idxtm_rec(ctx, i),
                               expand_idxtm_rec(ctx, j))
        }
        IdxTm::NoParse(s) => IdxTm::NoParse(s)
    }
}

/// Substitute terms into name terms
pub fn expand_nmtm_rec(ctx:&Ctx, m:Rc<NameTm>) -> Rc<NameTm> {
    Rc::new(expand_nmtm(ctx,(*m).clone()))
}


/// Substitute name terms into name terms
pub fn expand_nmtm(ctx:&Ctx, m:NameTm) -> NameTm {
    match m {
        NameTm::ValVar(y) => NameTm::ValVar(y),
        NameTm::Ident(x) => {
            match ctx.lookup_nmtm_def(&x) {
                Some(a) => {
                    expand_nmtm(ctx, a)
                },
                _ => {
                    println!("undefined name term: {} in\n{:?}", x, ctx);
                    // Give up:
                    NameTm::Ident(x.clone())
                }
            }}
        NameTm::Var(y) => NameTm::Var(y),
        NameTm::WriteScope => NameTm::WriteScope,
        NameTm::NoParse(s) => NameTm::NoParse(s),
        NameTm::Name(n) => NameTm::Name(n),
        NameTm::App(n1, n2) => {
            NameTm::App(
                expand_nmtm_rec(ctx, n1),
                expand_nmtm_rec(ctx, n2),
            )                
        }
        NameTm::Bin(n1, n2) => {
            NameTm::Bin(
                expand_nmtm_rec(ctx, n1),
                expand_nmtm_rec(ctx, n2),
            )                
        }
        NameTm::Lam(y,yg,m1) => {
            NameTm::Lam(y,yg,
                        expand_nmtm_rec(ctx,m1))
        }
    }
}