-- This file:
--   http://angg.twu.net/LATEX/2021lean.lua.html
--   http://angg.twu.net/LATEX/2021lean.lua
--           (find-angg "LATEX/2021lean.lua")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
--
-- (defun e () (interactive) (find-angg "LATEX/2021lean-nng.tex"))
-- (defun l () (interactive) (find-angg "LATEX/2021lean.lua"))

-- «.lean_translate»		(to "lean_translate")
-- «.lean_translate-tests»	(to "lean_translate-tests")
-- «.lean_tactranslate»		(to "lean_tactranslate")
-- «.lean_tactranslate-tests»	(to "lean_tactranslate-tests")
-- «.use_proofsty_lean»		(to "use_proofsty_lean")

re = require "re"               -- (find-angg "LUA/Re.lua")



--  _                     _                       _       _       
-- | | ___  __ _ _ __    | |_ _ __ __ _ _ __  ___| | __ _| |_ ___ 
-- | |/ _ \/ _` | '_ \   | __| '__/ _` | '_ \/ __| |/ _` | __/ _ \
-- | |  __/ (_| | | | |  | |_| | | (_| | | | \__ \ | (_| | ||  __/
-- |_|\___|\__,_|_| |_|___\__|_|  \__,_|_| |_|___/_|\__,_|\__\___|
--                   |_____|                                      
--
-- «lean_translate»  (to ".lean_translate")

lean_specials = {
  ["["]   = "⟦",
  ["]"]   = "⟧",
  [":"]   = "{:}",
  ["..."] = "\\ldots ",
  [".."]  = ".\\;",
  ["."]   = "\\,",
  [" "]   = "\\,",
}

lean_gram = [=[

  sfword       <- {~ ("" -> "\textsf{") sfchars ("" -> "}")~}
    sfchars    <- sfchar+
    sfchar     <- ([A-Za-z0-9]+ / ('_' -> '\_'))

  leansspecial <- ( '[' / ']' / ':' / '...' / ' '        ) -> specials
  leanspecial  <- ( '[' / ']' / ':' / '...' / '..' / '.' ) -> specials
  leanchar     <- [^\{}]

  leansstr     <- {~ (sfword / leansspecial / leanchar)* ~}
  leanstr      <- {~ (sfword / leanspecial  / leanchar)* ~}

]=]

lean_Re0 = Re { grammar = lean_gram,  defs = {specials = lean_specials} }
lean_stranslate = lean_Re0:cc 'top <- leansstr'
lean_translate  = lean_Re0:cc 'top <- leanstr'
lean_trimtranslate = function (str) return lean_stranslate(bitrim(str)) end

-- «lean_translate-tests»  (to ".lean_translate-tests")
--[==[
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
dofile "2021lean.lua"

= lean_translate     [=[ foo_bar+add0 ]=]
= lean_stranslate    [=[ foo_bar+add0 ]=]
= lean_stranslate    [=[ (h n):mynat  ]=]
= lean_trimtranslate [=[ (h n):mynat  ]=]

--]==]



--  _                     _             _                       _       _       
-- | | ___  __ _ _ __    | |_ __ _  ___| |_ _ __ __ _ _ __  ___| | __ _| |_ ___ 
-- | |/ _ \/ _` | '_ \   | __/ _` |/ __| __| '__/ _` | '_ \/ __| |/ _` | __/ _ \
-- | |  __/ (_| | | | |  | || (_| | (__| |_| | | (_| | | | \__ \ | (_| | ||  __/
-- |_|\___|\__,_|_| |_|___\__\__,_|\___|\__|_|  \__,_|_| |_|___/_|\__,_|\__\___|
--                   |_____|                                                    
--
-- «lean_tactranslate»  (to ".lean_tactranslate")

lean_tacgram = [=[
  inner <- [^{}] / ('{' inner* '}')
  arg   <- { '{'   inner*                '}' }
  argt  <- {~'{' { inner* } -> translate '}'~} 
  lean  <- {~ '\Lean' argt     ~}
  tac   <- {~ '\Tac'  argt arg ~}
  by    <- {~ '\By'        arg ~}
]=]

lean_tacdefs = { translate = lean_trimtranslate }
lean_tacRe0 = Re { grammar = lean_tacgram, defs = lean_tacdefs }
lean_tactranslate0 = lean_tacRe0:cc 'top <- lean / tac / by / {.*}'
lean_tactranslate  = function (str) return lean_tactranslate0(bitrim(str)) end

-- «lean_tactranslate-tests»  (to ".lean_tactranslate-tests")
--[==[
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
dofile "2021lean.lua"

= lean_trimtranslate 'foo'

= lean_tacRe0:cc 'top <- argt'      [=[{foo}]=]
= lean_tacRe0:cc 'top <- lean' [=[\Lean{foo}]=]

= lean_tactranslate [=[       foo bar       ]=]
= lean_tactranslate [=[   \By{foo bar}      ]=]
= lean_tactranslate [=[ \Lean{foo bar}      ]=]
= lean_tactranslate [=[ \Tac{foo bar}{plic} ]=]
= lean_tactranslate [=[ \tac{foo bar}{plic} ]=]

--]==]



--  ____                   __ ____  _         
-- |  _ \ _ __ ___   ___  / _/ ___|| |_ _   _ 
-- | |_) | '__/ _ \ / _ \| |_\___ \| __| | | |
-- |  __/| | | (_) | (_) |  _|___) | |_| |_| |
-- |_|   |_|  \___/ \___/|_| |____/ \__|\__, |
--                                      |___/ 
--
-- «use_proofsty_lean»  (to ".use_proofsty_lean")
-- (find-dn6 "heads6.lua" "tree-head")
-- (find-dn6 "treetex.lua" "ProofSty")
-- (find-dn6 "treetex.lua" "TreeNode")
-- (find-dn6 "treetex.lua" "TreeNode" "TeX_deftree =")
--
use_proofsty_lean = function ()
    --
    proofsty = ProofSty.new()
    proofsty.unabbrev = function (ps, str)
        return lean_translate(str)
      end
    TreeNode.__index.TeX_deftree = function (tn, name, link)
        return proofsty:todefded(tn, name, link)
      end
    --
  end


-- Old tests:
--[[
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
dofile "2021lean.lua"

   lean_translate 'foo_bar0plic.[bletch]'
PP(lean_translate 'foo_bar0plic.[bletch]')

loaddednat6()
output = print
require "block" -- (find-dn6 "block.lua")

--   (find-LATEX "2021lean-nng.tex" "tree")
texfile0("~/LATEX/2021lean-nng.tex")
= tf
tf:processuntil(tf.j)
= tf

-- (find-dn6 "treesegs.lua" "allsegments")
-- (find-dn6 "heads6.lua" "tree-head")
-- (find-dn6 "treetex.lua" "TreeNode")
-- (find-dn6 "treetex.lua" "TreeNode" "TeX_deftree =")
--
= allsegments:last(2000)
= allsegments:last(2000):rootnode()
= allsegments:last(2000):rootnode():totreenode()
= allsegments:last(2000):rootnode():totreenode():TeX_deftree("FOO")
tn = allsegments:last(2000):rootnode():totreenode()

--]]







-- Local Variables:
-- coding:  utf-8-unix
-- End: