filter out uncheckable definitions per-module

Dedukti/Trans.lean

@@ -240,24 +240,18 @@ mutual
     set s -- FIXME why can't use modify here?
 
   partial def transNamedConst (const : Name) : TransM Unit := do
-      match (← get).env.constMap.find? (fixLeanName const) with -- only translate if not already translated
-      | some _ => pure ()
-      | none =>
-        match (← read).env.constants.find? const with
-        | some cinfo => transConst cinfo
-        | none => tthrow s!"could not find constant \"{const}\" for translation, verify that it exists in the Lean input"
+    match (← get).env.constMap.find? (fixLeanName const) with -- only translate if not already translated
+    | some _ => pure ()
+    | none =>
+      match (← read).env.constants.find? const with
+      | some cinfo => if !cinfo.name.isImplementationDetail && !cinfo.name.isCStage then
+        transConst cinfo
+      | none => tthrow s!"could not find constant \"{const}\" for translation, verify that it exists in the Lean input"
 
 end
 
-def translateEnv (consts? : Option $ Lean.NameSet := none) (transDeps : Bool := false) : TransM Unit := do
-  match consts? with
-  | some consts =>
-    for const in consts do
-      withTransDeps transDeps $ transNamedConst const
-  | none =>
-    (← read).env.constants.forM (fun _ cinfo => do
-      if !cinfo.name.isInternal then
-        transConst cinfo
-    )
+def translateEnv (consts : Lean.NameSet) (transDeps : Bool := false) : TransM Unit := do
+  for const in consts do
+    withTransDeps transDeps $ transNamedConst const
 
 end Trans

Dedukti/Util.lean

@@ -3,6 +3,14 @@ open Lean
 
 def fixLeanName (name : Name) : Name := name.toStringWithSep "_" false -- TODO what does the "escape" param do exactly?
 
+partial def Lean.Name.isCStage : Name → Bool
+| .str p s   => s.startsWith "_cstage" || p.isCStage
+| .num p _   => p.isCStage
+| .anonymous => false
+
+def ignoredConstant : Name → Bool
+| n => !n.isImplementationDetail && !n.isCStage
+
 namespace Deps
   structure Context where
     env        : Environment
@@ -25,7 +33,8 @@ namespace Deps
       modify fun s => { s with map := s.map.insert name const }
       let deps := const.getUsedConstantsAsSet
       for dep in deps do
-        namedConstDeps dep
+        if !dep.isImplementationDetail && !dep.isCStage then
+          namedConstDeps dep
     | .some _ => pure default
 end Deps
 

Main.lean

@@ -49,19 +49,20 @@ def getCheckableConstants (env : Lean.Environment) (consts : Lean.NameSet) (prin
   let mut modEnv := (← Lean.mkEmptyEnvironment).setProofIrrelevance false
   for const in consts do
     try
-      let mut (_, {map := map, ..}) ← ((Deps.namedConstDeps const).toIO { options := default, fileName := "", fileMap := default } {env} {env})
-      let mapConsts := map.fold (init := default) fun acc const _ => acc.insert const
+      if not $ skipConsts.contains const then
+        let mut (_, {map := map, ..}) ← ((Deps.namedConstDeps const).toIO { options := default, fileName := "", fileMap := default } {env} {env})
+        let mapConsts := map.fold (init := default) fun acc const _ => acc.insert const
 
-      let erredConsts : Lean.NameSet := mapConsts.intersectBy (fun _ _ _ => default) errConsts
-      if erredConsts.size > 0 then
-        throw $ IO.userError "Encountered untypecheckable constant dependencies: {erredConsts}."
+        let erredConsts : Lean.NameSet := mapConsts.intersectBy (fun _ _ _ => default) errConsts
+        if erredConsts.size > 0 then
+          throw $ IO.userError "Encountered untypecheckable constant dependencies: {erredConsts}."
 
-      let skippedConsts : Lean.NameSet := mapConsts.intersectBy (fun _ _ _ => default) skipConsts
-      for skipConst in skippedConsts do
-        map := map.erase skipConst
+        let skippedConsts : Lean.NameSet := mapConsts.intersectBy (fun _ _ _ => default) skipConsts
+        for skipConst in skippedConsts do
+          map := map.erase skipConst
 
-      modEnv ← modEnv.replay map
-      skipConsts := skipConsts.union mapConsts -- TC success, so want to skip in future runs (already in environment)
+        modEnv ← modEnv.replay map
+        skipConsts := skipConsts.union mapConsts -- TC success, so want to skip in future runs (already in environment)
       onlyConstsToTrans := onlyConstsToTrans.insert const
     catch
     | e =>
@@ -74,35 +75,43 @@ def getCheckableConstants (env : Lean.Environment) (consts : Lean.NameSet) (prin
 def runTransCmd (p : Parsed) : IO UInt32 := do
   let path := ⟨p.positionalArg! "input" |>.value⟩
   let fileName := path.toString
+  let moduleName ← Lean.moduleNameOfFileName path .none 
   IO.println s!"\n{BLUE}>> Translation file: {YELLOW}{fileName}{NOCOLOR}"
   let onlyConsts? := p.flag? "only" |>.map fun setPathsFlag => 
     setPathsFlag.as! (Array String)
 
   IO.println s!"\n{BLUE}>> Elaborating... {YELLOW}\n"
   -- run elaborator on Lean file
   Lean.initSearchPath (← Lean.findSysroot)
-  let (env, success) ← Lean.Elab.runFrontend (← IO.FS.readFile path) default fileName default
+  let (env, success) ← Lean.Elab.runFrontend (← IO.FS.readFile path) default fileName moduleName
   if not success then
     throw $ IO.userError $ "elab failed"
 
-  let mut onlyConstsToTrans? := none
   let mut write := true
   IO.println s!"{NOCOLOR}"
-  if let some onlyConsts := onlyConsts? then
+
+  let mut onlyConstsArr := #[]
+  if let some _onlyConsts := onlyConsts? then
     write := (not $ p.hasFlag "print") || p.hasFlag "write"
+    printColor BLUE s!">> Using CLI-specified constants: {_onlyConsts}..."
+    onlyConstsArr := _onlyConsts.map (·.toName)
+  else
+    printColor BLUE s!">> Using all constants from given module: {moduleName}..."
+    onlyConstsArr := env.constants.map₂.toArray.map fun (x : Name × Lean.ConstantInfo) => x.1
 
-    printColor BLUE s!">> Re-typechecking specified constants: {onlyConsts}..."
-    -- env := modEnv
-    let onlyConstsSet := onlyConsts.foldl (init := default) fun acc const => acc.insert const.toName
+  let onlyConstsInit := onlyConstsArr.foldl (init := default) fun acc const =>
+    if !const.isImplementationDetail && !const.isCStage then acc.insert const else acc
 
-    let onlyConstsToTrans ← getCheckableConstants env onlyConstsSet (printErr := true)
+  let onlyConsts ← getCheckableConstants env onlyConstsInit (printErr := true)
+
+  let ignoredConsts := onlyConstsInit.diff onlyConsts
+  if ignoredConsts.size > 0 then
+    printColor RED s!"WARNING: Skipping translation of {ignoredConsts.size} constants: {ignoredConsts.toArray}..."
+
+  printColor BLUE s!">> Translating {onlyConsts.size} constants..."
 
-    onlyConstsToTrans? := .some onlyConstsToTrans
-    printColor BLUE s!">> Only translating constants [{onlyConstsToTrans.size}/{onlyConsts.size}]: {onlyConstsToTrans.toArray}..."
-  else
-    printColor BLUE s!">> Translating entire file..."
   -- translate elaborated Lean environment to Dedukti
-  let (_, {env := dkEnv, ..}) ← (Trans.translateEnv onlyConstsToTrans? (transDeps := write)).toIO { options := default, fileName := "", fileMap := default } {env} {env}
+  let (_, {env := dkEnv, ..}) ← (Trans.translateEnv onlyConsts (transDeps := write)).toIO { options := default, fileName := "", fileMap := default } {env} {env}
 
   -- let write := if let some _ := onlyConsts? then (p.hasFlag "write") else true -- REPORT why does this not work?
 
@@ -111,7 +120,7 @@ def runTransCmd (p : Parsed) : IO UInt32 := do
     printDkEnv dkEnv none
 
   if p.hasFlag "print" then
-    printDkEnv dkEnv onlyConstsToTrans?
+    printDkEnv dkEnv $ .some onlyConsts
   IO.print s!"{NOCOLOR}"
 
   return 0

fixtures/StdLib.lean

@@ -46,7 +46,8 @@ theorem myEm (p : Prop) : p ∨ ¬p :=
 -- #reduce semiOutParam (Sort u)
 --
 -- #print Classical.em
-#print Subtype.mk
+-- #print myEm
+-- #print Classical.em
 #print Subtype.val
 #print Subtype.property