fix french quotes in dk output

Dedukti/Print.lean

@@ -251,7 +251,7 @@ mutual
               -- is correctly linearized upon printing the .dk file
               let some const := (← read).env.constMap.find? name | throw s!"could not find referenced constant \"{name}\""
               const.print
-      pure $ toString name
+      pure $ name.toString false
     | .fixme msg => pure s!"Type (;{msg};)"
     | .app fn arg =>
       let fnExprString ← fn.print
@@ -287,7 +287,7 @@ mutual
       | .definable (name : Name) (type : Expr) (rules : List Rule) => do
         -- dbg_trace s!"printing: {name}"
         -- modify fun s => { s with pendingRules := s.pendingRules.insert name [] } -- TODO needed?
-        let declString := s!"def {name} : {← withPendingType name type.print}."
+        let declString := s!"def {name.toString false} : {← withPendingType name type.print}."
         -- dbg_trace s!"done printing type of: {name}"
         modify fun s => { s with out := s.out ++ [declString], pendingRules := s.pendingRules.insert name [] }
 

Dedukti/TransM.lean

@@ -59,7 +59,7 @@ def withFVars (fvarTypes : Std.RBMap Name Expr compare) (fvars : Array Lean.Expr
   let newFvarTypes := (← read).fvarTypes.mergeWith (fun _ _ t => t) fvarTypes
   withReader (fun ctx => { ctx with fvarTypes := newFvarTypes, fvars := newFvars }) m
 
-def nextLetName : TransM Name := do pure $ fixLeanName $ ((← read).constName).toString ++ "_let" ++ (toString (← read).numLets)
+def nextLetName : TransM Name := do pure $ fixLeanName $ ((← read).constName).toString false ++ "_let" ++ (toString (← read).numLets)
 
 def withLet (varName : Name) (m : TransM α) : TransM α := do
   let lvars := (← read).lvars.insert varName ((← read).fvars.size, ← nextLetName)

Dedukti/Util.lean

@@ -1,7 +1,21 @@
 import Lean
 open Lean
 
-def fixLeanName (name : Name) : Name := name.toStringWithSep "_" false -- TODO what does the "escape" param do exactly?
+def charSubs := [
+  -- ("»", "-_"),
+  -- ("«", "_-"),
+  (":", "_cln_"),
+]
+
+def fixLeanNameStr (name : String) : String := charSubs.foldl (init := name) fun acc (orig, sub) => acc.replace orig sub
+
+def fixLeanName' : Name → Name
+| .str p s   => .str (fixLeanName' p) $ fixLeanNameStr s
+| .num p n   => .num (fixLeanName' p) n
+| .anonymous => .anonymous
+
+def fixLeanName (n : Name) : Name :=
+  fixLeanName' n |>.toStringWithSep "_" false
 
 partial def Lean.Name.isCStage : Name → Bool
 | .str p s   => s.startsWith "_cstage" || p.isCStage

Main.lean

@@ -55,7 +55,7 @@ def getCheckableConstants (env : Lean.Environment) (consts : Lean.NameSet) (prin
 
         let erredConsts : Lean.NameSet := mapConsts.intersectBy (fun _ _ _ => default) errConsts
         if erredConsts.size > 0 then
-          throw $ IO.userError "Encountered untypecheckable constant dependencies: {erredConsts}."
+          throw $ IO.userError s!"Encountered untypecheckable constant dependencies: {erredConsts.toList}."
 
         let skippedConsts : Lean.NameSet := mapConsts.intersectBy (fun _ _ _ => default) skipConsts
         for skipConst in skippedConsts do
@@ -108,6 +108,7 @@ def runTransCmd (p : Parsed) : IO UInt32 := do
   if ignoredConsts.size > 0 then
     printColor RED s!"WARNING: Skipping translation of {ignoredConsts.size} constants: {ignoredConsts.toArray}..."
 
+  -- printColor BLUE s!">> Translating {onlyConsts.size} constants: {onlyConsts.toArray}..."
   printColor BLUE s!">> Translating {onlyConsts.size} constants..."
 
   -- translate elaborated Lean environment to Dedukti

fixtures/StdLib.lean

@@ -1,44 +1,9 @@
-import Init
 universe u
 theorem em (p : Prop) : p ∨ ¬p := Classical.em p
 set_option pp.all true
 
 open Classical
 
-axiom myRefl {α : Type} (a b : α) : Eq a b
-
-theorem myEm (p : Prop) : p ∨ ¬p :=
-  let U (x : Prop) : Prop := x = True ∨ p
-  let V (x : Prop) : Prop := x = False ∨ p
-  have exU : ∃ x, U x := ⟨True, Or.inl rfl⟩
-  have exV : ∃ x, V x := ⟨False, Or.inl rfl⟩
-  let u : Prop := choose exU
-  let v : Prop := choose exV
-  have u_def : U u := choose_spec exU
-  have v_def : V v := choose_spec exV
-  have not_uv_or_p : u ≠ v ∨ p :=
-    match u_def, v_def with
-    | Or.inr h, _ => Or.inr h
-    | _, Or.inr h => Or.inr h
-    | Or.inl hut, Or.inl hvf =>
-      have hne : u ≠ v := by simp [hvf, hut, true_ne_false]
-      Or.inl hne
-  have p_implies_uv : p → u = v :=
-    fun hp =>
-    have hpred : U = V :=
-      funext fun x =>
-        have hl : (x = True ∨ p) → (x = False ∨ p) :=
-          fun _ => Or.inr hp
-        have hr : (x = False ∨ p) → (x = True ∨ p) :=
-          fun _ => Or.inr hp
-        show (x = True ∨ p) = (x = False ∨ p) from
-          propext (Iff.intro hl hr)
-    have h₀ : ∀ exU exV, @choose _ U exU = @choose _ V exV := by
-      rw [hpred]; intros; exact myRefl _ _
-    show u = v from h₀ _ _
-  match not_uv_or_p with
-  | Or.inl hne => Or.inr (mt p_implies_uv hne)
-  | Or.inr h   => Or.inl h
 -- #print CoeOut.mk
 -- #print Quot
 -- #print Quot.lift
@@ -53,11 +18,6 @@ theorem myEm (p : Prop) : p ∨ ¬p :=
 
 def test1 (s : Subtype P1) : Subtype.mk (Subtype.val s) (Subtype.property s) = s := rfl
 
-noncomputable instance (priority := low) myPropDecidable (a : Prop) : Decidable a :=
-  choice <| match myEm a with
-    | Or.inl h => ⟨isTrue h⟩
-    | Or.inr h => ⟨isFalse h⟩
-
 def P1 : Bool → Prop
   | .true => True
   | .false => True