Editor.hs

module PGF.Editor (
  State,       -- datatype  -- type-annotated possibly open tree with a focus
  Dict,        -- datatype  -- abstract syntax information optimized for editing
  Position,    -- datatype  -- path from top to focus 
  new,         -- :: Type  -> State                    -- create new State
  refine,      -- :: Dict  -> CId -> State -> State    -- refine focus with CId
  replace,     -- :: Dict  -> Tree -> State -> State   -- replace focus with Tree
  delete,      -- :: State -> State                    -- replace focus with ?
  goNextMeta,  -- :: State -> State                    -- move focus to next ? node
  goNext,      -- :: State -> State                    -- move to next node
  goTop,       -- :: State -> State                    -- move focus to the top (=root)
  goPosition,  -- :: Position -> State -> State        -- move focus to given position
  mkPosition,  -- :: [Int] -> Position                 -- list of choices (top = [])
  showPosition,-- :: Position -> [Int]                 -- readable position 
  focusType,   -- :: State -> Type                     -- get the type of focus
  stateTree,   -- :: State -> Tree                     -- get the current tree
  isMetaFocus, -- :: State -> Bool                     -- whether focus is ?
  allMetas,    -- :: State -> [(Position,Type)]        -- all ?s and their positions
  prState,     -- :: State -> String                   -- print state, focus marked *
  refineMenu,  -- :: Dict  -> State -> [CId]           -- get refinement menu
  pgf2dict     -- :: PGF   -> Dict                     -- create editing Dict from PGF
  ) where

import PGF.Data
import PGF.CId
import qualified Data.Map as M
import Debug.Trace ----

-- API

new :: Type -> State
new (DTyp _ t _) = etree2state (uETree t)

refine :: Dict -> CId -> State -> State
refine dict f = replaceInState (mkRefinement dict f)

replace :: Dict -> Tree -> State -> State
replace dict t = replaceInState (tree2etree dict t)

delete :: State -> State
delete s = replaceInState (uETree (typ (tree s))) s

goNextMeta :: State -> State
goNextMeta s = 
  if isComplete s then s
  else let s1 = goNext s in if isMetaFocus s1 
    then s1 else goNextMeta s1

isComplete :: State -> Bool
isComplete s = isc (tree s) where
  isc t = case atom t of
    AMeta _ -> False
    ACon  _ -> all isc (children t)

goTop :: State -> State
goTop = navigate (const top)

goPosition :: [Int] -> State -> State
goPosition p s = s{position = p}

mkPosition :: [Int] -> Position
mkPosition = id

refineMenu :: Dict -> State -> [CId]
refineMenu dict s = maybe [] (map fst) $ M.lookup (focusBType s) (refines dict)

focusType :: State -> Type
focusType s = btype2type (focusBType s)

stateTree :: State -> Tree
stateTree = etree2tree . tree

pgf2dict :: PGF -> Dict
pgf2dict pgf = Dict (M.fromAscList fus) refs where
  fus  = [(f,mkFType ty)  | (f,(ty,_)) <- M.toList (funs abs)]
  refs = M.fromAscList [(c, fusTo c) | (c,_) <- M.toList (cats abs)]
  fusTo c = [(f,ty) | (f,ty@(_,k)) <- fus, k==c] ---- quadratic
  mkFType (DTyp hyps c _) = ([k | Hyp _ (DTyp _ k _) <- hyps],c)  ----dep types
  abs  = abstract pgf

etree2tree :: ETree -> Tree
etree2tree t = case atom t of
  ACon f  -> Fun f (map etree2tree (children t))
  AMeta i -> Meta i

tree2etree :: Dict -> Tree -> ETree
tree2etree dict t = case t of
  Fun f _ -> annot (look f) t
 where
  annot (tys,ty) tr = case tr of 
    Fun f trs -> ETree (ACon f)  ty [annt t tr | (t,tr) <- zip tys trs]
    Meta i    -> ETree (AMeta i) ty []
  annt ty tr = case tr of
    Fun _ _ -> tree2etree dict tr
    Meta _  -> annot ([],ty) tr
  look f = maybe undefined id $ M.lookup f (functs dict)

prState :: State -> String
prState s = unlines [replicate i ' ' ++ f | (i,f) <- pr [] (tree s)] where
  pr i t = 
    (ind i,prAtom i (atom t)) : concat [pr (sub j i) c | (j,c) <- zip [0..] (children t)]
  prAtom i a = prFocus i ++ case a of
    ACon f -> prCId f
    AMeta i -> "?" ++ show i
  prFocus i = if i == position s then "*" else ""
  ind i = 2 * length i
  sub j i = i ++ [j]

showPosition :: Position -> [Int]
showPosition = id

allMetas :: State -> [(Position,Type)]
allMetas s = [(reverse p, btype2type ty) | (p,ty) <- metas [] (tree s)] where
  metas p t = 
    (if isMetaAtom (atom t) then [(p,typ t)] else []) ++ 
      concat [metas (i:p) u | (i,u) <- zip [0..] (children t)]

---- Trees and navigation

data ETree = ETree {
  atom  :: Atom,
  typ   :: BType,
  children :: [ETree]
  }
  deriving Show

data Atom =
    ACon CId
  | AMeta Int
  deriving Show

btype2type :: BType -> Type
btype2type t = DTyp [] t []

uETree :: BType -> ETree
uETree ty = ETree (AMeta 0) ty []

data State = State {
  position :: Position,
  tree :: ETree
  }
  deriving Show

type Position = [Int]

top :: Position
top = []

up :: Position -> Position
up p = case p of
  _:_ -> init p
  _ -> p

down :: Position -> Position
down = (++[0])

left :: Position -> Position
left p = case p of
  _:_ | last p > 0 -> init p ++ [last p - 1]
  _ -> top

right :: Position -> Position
right p = case p of
  _:_ -> init p ++ [last p + 1]
  _ -> top

etree2state :: ETree -> State
etree2state = State top

doInState :: (ETree -> ETree) -> State -> State
doInState f s = s{tree = change (position s) (tree s)} where
  change p t = case p of
    [] -> f t
    n:ns -> let (ts1,t0:ts2) = splitAt n (children t) in 
              t{children = ts1 ++ [change ns t0] ++ ts2}

subtree :: Position -> ETree -> ETree
subtree p t = case p of
  [] -> t
  n:ns -> subtree ns (children t !! n)

focus :: State -> ETree
focus s = subtree (position s) (tree s)

focusBType :: State -> BType
focusBType s = typ (focus s)

navigate :: (Position -> Position) -> State -> State
navigate p s = s{position = p (position s)}

-- p is a fix-point aspect of state change
untilFix :: Eq a => (State -> a) -> (State -> Bool) -> (State -> State) -> State -> State
untilFix p b f s = 
  if b s  
    then s 
    else let fs = f s in if p fs == p s 
      then s 
      else untilFix p b f fs

untilPosition :: (State -> Bool) -> (State -> State) -> State -> State
untilPosition = untilFix position

goNext :: State -> State
goNext s = case focus s of
  st | not (null (children st)) -> navigate down s
  _ -> findSister s
 where
  findSister s = case s of
    s' | null (position s') -> s'
    s' | hasYoungerSisters s' -> navigate right s'
    s' -> findSister (navigate up s')
  hasYoungerSisters s = case position s of
    p@(_:_) -> length (children (focus (navigate up s))) > last p + 1
    _ -> False

isMetaFocus :: State -> Bool
isMetaFocus s = isMetaAtom (atom (focus s))

isMetaAtom :: Atom -> Bool
isMetaAtom a = case a of
  AMeta _ -> True
  _ -> False

replaceInState :: ETree -> State -> State
replaceInState t = doInState (const t)


-------

type BType = CId ----dep types
type FType = ([BType],BType) ----dep types

data Dict = Dict {
  functs  :: M.Map CId FType,
  refines :: M.Map BType [(CId,FType)]
  }

mkRefinement :: Dict -> CId -> ETree
mkRefinement dict f = ETree (ACon f) val (map uETree args) where
  (args,val) = maybe undefined id $ M.lookup f (functs dict)