ProofTreeNumbers.hs

module ProofTreeNumbers (PTree(..), lineNumberHelp, near, full_reverse, tree_reverse)
where 
 

data PTree a = T  a  [PTree a]    
   deriving (Show, Eq)
get1 (aa,b,c) = aa
get2 (aa,b,c) = b
get3 (aa,b,c) = c
   

lineNumberHelp :: [(a, [Int], Int)] ->  [(a, [Int], Int)]  ->  [(a, [Int], Int)]
lineNumberHelp firstseq  secondseq =
     let     
              n = if null firstseq then 0 else (get3 $ head firstseq)
              modify  w = map ( \ (x, listofInts, k) -> (x, (map (\ i -> 1 + n+i) listofInts), k)) w
     in  (firstseq ++ modify secondseq)         
              
------ near of a PTree lists the nodes in depth-first order, along with an extra list for each node.
------ for the node n in the tree it lists the addresses of the children of n in the same tree, again in the 
------ depth-first order of the tree overall.    Getting this right was probably the hardest part of this whole exercise.
------ Note also that what we want in the end is not the depth-first listing of the PTree but rather the 'bottom-up' listing,
------ and these are related by
------     
------                       bottom_up t = reverse (depth_first ( tree_reverse t))
 
near :: (PTree  a) -> [(a, [Int], Int)]
near (T x l) = [(x,s, k+1 )] ++ extrastuff
    where  
                k =  sum r
                --extrastuff :: [(a, [Int], Int)] 
                extrastuff =  foldl lineNumberHelp []  (map near l)
                --q :: [(a, [Int], Int)] 
                q = map head $ map near l               
                r :: [Int]
                r = map get3 q
                s = init( scanl (+) 2 r)
               
tree_reverse (T n t) = T n (map tree_reverse (reverse t))
 
full_reverse ::  [(a, [Int], Int)] -> [(Int, a, [Int])]
full_reverse h = 
   let 
        n = length h
        p = [(i,  reverse( map (\ x -> n  + 1 - x) j )) | (i,j,k) <- h]
        q = reverse p
        w = [1..n]
        mergeMe :: [Int] -> [(a,[Int])] -> [(Int,a,[Int])]
        mergeMe  [] [] = []
        mergeMe (i:wMore)  (pair:pMore) = (i, (fst pair), (snd pair)) : (mergeMe wMore pMore)
   in  mergeMe w q