Automation

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
 

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

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