diff --git a/src/PGF/Editor.hs b/src/PGF/Editor.hs index c01c9ca1b..15ce117b8 100644 --- a/src/PGF/Editor.hs +++ b/src/PGF/Editor.hs @@ -1,42 +1,71 @@ module PGF.Editor where +import PGF.Data +import PGF.CId import qualified Data.Map as M -- API -replace :: Tree -> State -> State +new :: Type -> State +new (DTyp _ t _) = etree2state (uETree t) + +refine :: Dict -> CId -> State -> State +refine dict f = replace (mkRefinement dict f) + +replace :: ETree -> State -> State replace t = doInState (const t) delete :: State -> State -delete s = replace (uTree (typ (tree s))) s +delete s = replace (uETree (typ (tree s))) s -new :: Type -> State -new t = tree2state (uTree t) +goNextMeta :: State -> State +goNextMeta = untilPosition isMetaFocus goNext -refineMenu :: Dict -> State -> [(Id,FType)] +goTop :: State -> State +goTop = navigate (const top) + +refineMenu :: Dict -> State -> [(CId,FType)] refineMenu dict s = maybe [] id $ M.lookup (focusType s) (refines dict) +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 -data Tree = Tree { +--tree2etree :: Tree -> ETree + + +---- TODO +-- getPosition :: Language -> Int -> ETree -> Position + +---- Trees and navigation + +data ETree = ETree { atom :: Atom, - typ :: Type, - children :: [Tree] + typ :: BType, + children :: [ETree] } deriving Show data Atom = - ACon Id + ACon CId | AMeta Int deriving Show -uTree :: Type -> Tree -uTree ty = Tree (AMeta 0) ty [] +uETree :: BType -> ETree +uETree ty = ETree (AMeta 0) ty [] data State = State { position :: Position, - tree :: Tree + tree :: ETree } deriving Show @@ -61,37 +90,67 @@ right p = case p of (n:ns) -> n+1 : ns _ -> top -tree2state :: Tree -> State -tree2state = State top +etree2state :: ETree -> State +etree2state = State top -doInState :: (Tree -> Tree) -> State -> State +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 -> Tree -> Tree +subtree :: Position -> ETree -> ETree subtree p t = case p of [] -> t n:ns -> subtree ns (children t !! n) -focus :: State -> Tree +focus :: State -> ETree focus s = subtree (position s) (tree s) -focusType :: State -> Type +focusType :: State -> BType focusType 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 + _ -> navigate right (untilPosition hasYoungerSisters (navigate up) s) + where + hasYoungerSisters s = case position s of + n:ns -> length (children (subtree ns (tree s))) > n + 1 + +isMetaFocus :: State -> Bool +isMetaFocus s = case atom (focus s) of + AMeta _ -> True + _ -> False + + ------- -type Id = String ---- -type Type = Id ---- -type FType = ([Id],Id) ---- +type BType = CId ---- +type FType = ([BType],BType) ---- data Dict = Dict { - funs :: M.Map Id FType, - refines :: M.Map Type [(Id,FType)] + 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) + diff --git a/src/exper/EditShell.hs b/src/exper/EditShell.hs new file mode 100644 index 000000000..a50317d47 --- /dev/null +++ b/src/exper/EditShell.hs @@ -0,0 +1,39 @@ +module Main where + +import PGF.Editor +import PGF + +import System (getArgs) + +main = do + putStrLn "Hi, I'm the Editor!" + file:_ <- getArgs + pgf <- readPGF file + let dict = pgf2dict pgf + let st0 = new (startCat pgf) + editLoop pgf dict st0 + +editLoop :: PGF -> Dict -> State -> IO State +editLoop pgf dict st = do + putStrLn ("I want something of type " ++ prCId (focusType st)) + c <- getLine + st' <- interpret pgf dict st c + let t = etree2tree (tree st') + putStrLn (unlines ([ + "Now I have", + showTree t] ++ + linearizeAll pgf t)) + editLoop pgf dict st' + +interpret :: PGF -> Dict -> State -> String -> IO State +interpret pgf dict st c = case words c of + "r":f:_ -> do + return $ goNextMeta (refine dict (mkCId f) st) + "m":_ -> do + putStrLn (unwords (map (prCId . fst) (refineMenu dict st))) + return st + _ -> do + putStrLn "command not understood" + return st + +