diff --git a/Examples/SystemFWithNat/Term.lean b/Examples/SystemFWithNat/Term.lean index 75445c4..08d563b 100644 --- a/Examples/SystemFWithNat/Term.lean +++ b/Examples/SystemFWithNat/Term.lean @@ -23,15 +23,16 @@ inductive Term where | tlam (t : Term) : Term -- binds Ty in t (does it make sense to allow a user to give a name instead of a position?) | zero : Term | succ : Term -> Term -| nrec (motive : Ty) (z : Term) (s : Term) (n : Term) : Term -- binds 2 Term's in s +| nrec (motive : Ty) (z : Term) (s : Term) (n : Term) : Term -- binds 2 Terms in s #leansubst var Term.var #leansubst bind Term at pos 1 in Term.lam #leansubst bind Ty at pos 0 in Term.tlam -#leansubst bind 2 of Term at pos 2 in Term.nrec - ---set_option diagnostics true +#leansubst bind + 2 of Term at pos 2, + 1 of Ty at pos 2 + in Term.nrec -- #leansubst generate Ty, Term diff --git a/Examples/VariadicSTLC/Term.lean b/Examples/VariadicSTLC/Term.lean index 8dbf78c..3c08659 100644 --- a/Examples/VariadicSTLC/Term.lean +++ b/Examples/VariadicSTLC/Term.lean @@ -8,10 +8,13 @@ inductive Ty where | base : Ty | arrow : Ty -> Ty +@[reducible] +def Variadic (n : Nat) (ty : Type) := Fin n → ty + inductive Term where | var : Nat -> Term -| app n : Term -> (Fin n -> Term) -> Term -| lam n : (Fin n -> Ty) -> Term -> Term +| app n : Term -> Variadic n Term -> Term +| lam n : Variadic n Ty -> Term -> Term @[coe] def Term.from_action : Action Term -> Term diff --git a/LeanSubst/Automation/Basic.lean b/LeanSubst/Automation/Basic.lean index 578b470..5da3292 100644 --- a/LeanSubst/Automation/Basic.lean +++ b/LeanSubst/Automation/Basic.lean @@ -176,19 +176,24 @@ namespace Automation `($stx.1) -- Applies a computation for each suffix in the list Tys. - def forEachSuffix : (tys : List Ident) → (f : List Ident → CommandElabM Unit) → CommandElabM Unit + def forEachSuffix {A : Type} : (tys : List A) → (f : List A → CommandElabM Unit) → CommandElabM Unit | [], _ => pure () | tys@(.cons _ tys'), f => do f tys forEachSuffix tys' f - def forEachPrefix : (tys : List Ident) → (f : List Ident → CommandElabM Unit) → CommandElabM Unit + def mapEachSuffix {A B : Type} : (tys : List A) → (f : List A → CommandElabM B) → CommandElabM $ List B + | [], _ => pure [] + | tys@(.cons _ tys'), f => do + pure $ (← (f tys)) :: (← mapEachSuffix tys' f) + + def forEachPrefix {A : Type} : (tys : List A) → (f : List A → CommandElabM Unit) → CommandElabM Unit | [], _ => pure () | tys@(.cons _ _), f => do f tys forEachSuffix tys.reverse.tail.reverse f - def forHeadAndEachSuffix : (tys : List Ident) → (f : List Ident → CommandElabM Unit) → CommandElabM Unit + def forHeadAndEachSuffix {A : Type} : (tys : List A) → (f : List A → CommandElabM Unit) → CommandElabM Unit | [], _ => pure () | .cons ty [], f => do f [ty] | tys@(.cons ty _), f => do @@ -209,14 +214,14 @@ namespace Automation -- The main function def genTy (tys : List Ident) : CommandElabM Unit := do + let numTotalTys := tys.length + let toGlobal (ty : Ident) : CommandElabM Name := Command.liftCoreM $ realizeGlobalConstNoOverload ty.raw let ty := tys[0]! let tyName := ty.raw.getId -- let tyStr := tyName.toString let tyNameGlobal ← toGlobal ty - dbg_trace s!"Generating {ty} with list {tys}" - -- let tyArr ← `([$tys.toArray,*]) -- let tysNamesGlobal ← tys.mapM toGlobal @@ -355,35 +360,42 @@ namespace Automation pure ⟨mkIdent ty', Syntax.mkNatLit 0⟩) pure $ increments.filter (fun (_, stx) ↦ match stx with | `(0) => false | _ => true) - let mkMapArr (data : ArgData) (xs : List Ident) (tys : List Ident) : CommandElabM $ Option MapOrLift := + let mkLiftsAndRens (data : ArgData) (xs : List Ident) (tys' : List Ident) : CommandElabM $ Option $ Term × List Term := match data with | .binder _ => do + let ⟨tys, headOnly⟩ : (List Ident) × Bool ← + if tys'.length = 1 ∧ tys.length > 1 then do + let ty'0_eq_ty0 ← liftCoreM $ runMetaMAsCoreM $ isDefEq (← liftTermElabM $ Term.elabTerm (tys'.head!) none) (← liftTermElabM $ Term.elabTerm (tys.head!) none) + if ty'0_eq_ty0 then -- The head-only case (for instance, tys' = [Term] and tys = [Term, Ty]) + pure ⟨tys, true⟩ + else + pure ⟨tys', false⟩ + else + pure ⟨tys', false⟩ + let lifts ← tys.mapM $ getLiftsOfTy data xs let optionLifts := lifts.map (fun stx : Term ↦ if BEq.beq stx $ Syntax.mkNatLit 0 then none else some stx) -- Check if all lifts are syntactically just 0 - if optionLifts.all (fun | none => true | some _ => false) then + if optionLifts.all Option.isNone then pure none else let tysNamesGlobal ← tys.mapM toGlobal - let incrementsList ← tysNamesGlobal.mapM $ getIncrementsOfTy lifts tysNamesGlobal - let zipped := incrementsList.zip optionLifts - let ops : List $ Term × Bool ← zipped.mapM (fun ⟨incs, lift⟩ ↦ do - let incOps ← incs.mapM (fun ⟨ty, inc⟩ ↦ - if BEq.beq inc $ Syntax.mkNatLit 0 then `(Ren.id $ty:ident) else `(Ren.add $ty:ident $inc)) - let anyIncs := incs.tail.any (fun ⟨_, inc⟩ ↦ ¬ (BEq.beq inc $ Syntax.mkNatLit 0)) - - let tyTail := tysNamesGlobal.tail.toArray.map mkIdent - let op ← match (anyIncs, lift) with - | (false, none) => `(.skip) - | (true, none) => `(.ren [$tyTail,*] ⟨$incOps.tail.toArray,*, .nil⟩) - | (false, some ℓ) => `(.lift $ℓ) - | (true, some ℓ) => `(.both [$tyTail,*] ⟨$incOps.tail.toArray,*, .nil⟩ $ℓ) - pure ⟨op, anyIncs⟩ + let zipped := tysNamesGlobal.zip optionLifts + let rens : List $ Option Term ← mapEachSuffix zipped (fun zippedSfx ↦ do + let ⟨tys, optionLifts⟩ := zippedSfx.unzip + if optionLifts.tail.all Option.isNone then + pure none + else + let lifts ← zippedSfx.tail.mapM (fun | ⟨ty, .none⟩ => `(Ren.id $(mkIdent ty)) | ⟨ty, .some n⟩ => `(Ren.add $(mkIdent ty) $n)) + let tysHd := mkIdent tys.head! + let tysTail := (tys.tail!.map mkIdent).toArray + let i := Syntax.mkNatLit $ numTotalTys - tys.length -- shadowing is bad, kids + pure $ some $ ← `(.ren $tysHd [$tysTail,*] ⟨$lifts.toArray,*, .nil⟩ $i rfl) ) - if ops.all (¬ ·.2) then -- If we don't have to apply any renamings - pure $ MapOrLift.lift $ ← `([$lifts.toArray,*]) - else - pure $ MapOrLift.map $ ← (ops.map Prod.fst).foldrM (fun t1 t2 ↦ `($t1 $ $t2)) $ ← `(LeanSubst.SubstVec.MapOps.nil) + let rens := rens.reverse.tail.reverse -- dropLast + let rens ← (rens.filter (Option.isSome)).mapM (fun | .none => `(0) | .some t => pure t) + let liftsTm ← `([$lifts.toArray,*]) + pure $ some ⟨liftsTm, rens⟩ | _ => pure none let smap_fVar (tys : List Ident) xs ctor : CommandElabM Term := do @@ -412,10 +424,13 @@ namespace Automation else if useTCSyntax then `(($x)⟨$(r),⟩) else `($rmap $r $x) | .smap => - if let MapOrLift.map opsArr ← mkMapArr data xs tys then - if useTCSyntax then `(($x)[$(σ).map $opsArr,]) else `($smap ($(σ).map $opsArr) $x) - else if let MapOrLift.lift opsArr ← mkMapArr data xs tys then - if useTCSyntax then `(($x)[$(σ).lift $opsArr,]) else `($smap ($(σ).lift $opsArr) $x) + if let some ⟨lifts, []⟩ ← mkLiftsAndRens data xs tys then + if useTCSyntax then `(($x)[($(σ).lift $lifts),]) else `($smap ($(σ).lift $lifts) $x) + else if let some ⟨lifts, rens⟩ ← mkLiftsAndRens data xs tys then + let mut σ' ← `($(σ) |> SubstVec.lift $lifts) + for ren in rens do + σ' ← `($σ' |> $ren) + if useTCSyntax then `(($x)[$(σ'),]) else `($smap ($σ') $x) else if useTCSyntax then `(($x)[$(σ),]) else `($smap $σ $x) else if let some theTy ← List.findM? (fun (ty : Ident) ↦ do pure (← liftCoreM $ runMetaMAsCoreM $ isDefEq (← liftTermElabM $ Term.elabTerm ty.raw none) ty')) tys then