-- This file can be used to generate the Agda definitions of (truncated) semi-simplicial types. For explanations, see the accompanying Agda file.
-- For general explanations of the problem, see 
-- http://uf-ias-2012.wikispaces.com/Semi-simplicial+types

-- Caveat: This is a rather ugly ad-hoc implementation. A better way to do this would be to use Haskell's packages for Agda's Syntax and generate the abstract syntax tree before printing it nicely.

-- The main function is the following.
-- generateAll n will, for some number n, generate the types of semi-simplicial "standard" simplices Xi (together with their boundaries, here called 'Pi').
-- Putting the output into the Agda file Semisimplicial.agda allows to check whether everything type checks (it works with Agda 2.3.3 and probably most other versions, as I do not use any special features at all and not even any kind of library)

generateAll n = generateAllAux n 0



-- The actual construction (for explanations, see the Agda file).
-- First: generate the list [ λ (gj : (S j) ⇒+ (S k)) . x_j(fk ∘+ gj)]_{j : Fin k} with a "*" (unique element of the unit type) in the end. 

genArgsAux k j =
  if k == j 
    then "*"
    else "(λ (g" ++ (show j) ++ " : (S " ++ (show j) ++ ") ⇒+ (S " ++ (show k) ++ ")) " ++
         "→ x" ++ (show j) ++ "(f" ++ (show k) ++ " ∘+ g" ++ (show j) ++ ")) , " ++ (genArgsAux k (j + 1))

genArgs k = genArgsAux k 0



genSkelAux n k = 
  if k == n 
    then "⊤" 
    else "Σ ((f" ++ (show k) ++ " : (S " ++ (show k) ++ ") ⇒+ (S " ++ (show n) ++ ")) " ++ 
                                             "→ X" ++ (show k) ++ " (" ++ genArgs k ++ "))" ++ 
         "  λ x" ++ (show k) ++ " → " ++ (genSkelAux n (k+1)) ++ " "

genSkel n = genSkelAux n 0


genP n = ("P" ++ (show n) ++ " = " ++ genSkel n)

genXty n = "X" ++ (show n) ++ " : P" ++ (show n) ++ " → Type"
genXtm n = "X" ++ (show n) ++ " = ?"

generateAllAux n k = 
  if k > n 
    then putStrLn ""
    else 
      do
        putStrLn (genP k ++ "\n\n" ++ genXty k ++ "\n" ++ genXtm k ++ "\n\n")
        generateAllAux n (k+1)