Editor with some commands, using PGF API, with demo shell in exper/EditShell; still buggy

1 files changed, 83 insertions, 24 deletions

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
+
+--tree2etree :: Tree -> ETree
+
 
-----
+---- TODO
+-- getPosition :: Language -> Int -> ETree -> Position
 
-data Tree = Tree {
+---- 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)
+