mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-27 02:07:14 +03:00
Hooking up new evaluate-terms function
This commit is contained in:
parent
e9e0de2e16
commit
7cd2ea1fb6
@ -47,3 +47,8 @@ contains : List k -> Trie k v -> Bool
|
||||
contains k t = case lookup k t of
|
||||
Nothing -> False
|
||||
Just _ -> True
|
||||
|
||||
keys : Trie k v -> List (List k)
|
||||
keys (Trie _ cs) =
|
||||
let f (k,t) = List.map ((::) k) (keys t)
|
||||
in List.concatMap f cs
|
||||
|
@ -212,6 +212,7 @@ type Request
|
||||
| Search Term Path Int (Maybe Type) Metadata.Query -- global search for a given type
|
||||
| Declare Term
|
||||
| Edit Path Path Action.Action Term
|
||||
| Evaluations (List (Path, Term))
|
||||
| Metadatas (List Reference)
|
||||
|
||||
type alias Action = Model -> (Maybe Request, Model)
|
||||
@ -329,9 +330,7 @@ accept : Model -> Model
|
||||
accept model = Maybe.withDefault model <|
|
||||
Selection1D.index model.explorerSelection
|
||||
(List.map fst (filteredCompletions model)) `Maybe.andThen`
|
||||
\term -> model.scope `Maybe.andThen`
|
||||
\scope -> Term.set scope.focus model.term term `Maybe.andThen`
|
||||
\t2 -> Just <| clearScopeHistory { model | term <- t2 }
|
||||
\term -> Just (clearScopeHistory (modifyFocus (always term) model))
|
||||
|
||||
openExplorer : Sink Field.Content -> Action
|
||||
openExplorer = openExplorerWith Field.noContent
|
||||
@ -697,6 +696,22 @@ search2 searchbox origin reqs =
|
||||
in Signal.map edit reqs
|
||||
|> JR.send (Node.editTerm host `JR.to` go) ([],[],Action.Noop,model0.term)
|
||||
|> Signal.map withStatus
|
||||
evaluations r = case r of
|
||||
-- todo: reroot the request to point to tightest bound term
|
||||
Evaluations es -> Just es
|
||||
_ -> Nothing
|
||||
evaluations' =
|
||||
let set model (path,old,new) cur = case Term.at path model.term of
|
||||
Nothing -> cur
|
||||
Just old' -> if old == old'
|
||||
then Trie.insert path new cur
|
||||
else cur
|
||||
go es model =
|
||||
-- todo, don't start with Trie.empty once doing proper dep tracking
|
||||
norequest { model | evaluations <- List.foldl (set model) Trie.empty es }
|
||||
in Signal.map evaluations reqs
|
||||
|> JR.send (Node.evaluateTerms host `JR.to` go) []
|
||||
|> Signal.map withStatus
|
||||
metadatas r = case r of
|
||||
Metadatas rs -> Just rs
|
||||
_ -> Nothing
|
||||
@ -709,7 +724,11 @@ search2 searchbox origin reqs =
|
||||
|> JR.send (Node.metadatas host `JR.to` go) []
|
||||
|> Signal.map withStatus
|
||||
noop model = norequest model
|
||||
in openEdit' `Signal.merge` metadatas' `Signal.merge` edit' `Signal.merge` search'
|
||||
in openEdit' `Signal.merge`
|
||||
metadatas' `Signal.merge`
|
||||
edit' `Signal.merge`
|
||||
search' `Signal.merge`
|
||||
evaluations'
|
||||
|
||||
main =
|
||||
let origin = (15,15)
|
||||
|
@ -63,6 +63,11 @@ editType host = Request.post host "edit-type"
|
||||
(Encoder.tuple3 Path.encodePath A.encode T.encodeType)
|
||||
T.decodeType
|
||||
|
||||
evaluateTerms : Host -> Request (List (Path, Term)) (List (Path,Term,Term))
|
||||
evaluateTerms host = Request.post host "evaluate-terms"
|
||||
(Encoder.list (Encoder.tuple2 Path.encodePath E.encodeTerm))
|
||||
(Decoder.list (Decoder.tuple3 Path.decodePath E.decodeTerm E.decodeTerm))
|
||||
|
||||
type alias LocalInfo =
|
||||
{ current : Type
|
||||
, admissible : Type
|
||||
|
@ -415,3 +415,11 @@ builtins env allowBreak availableWidth ambientPrec cur =
|
||||
App (App (Ref (R.Builtin "View.view")) v) e -> go v e
|
||||
_ -> Nothing
|
||||
|
||||
reactivePaths : Term -> Trie Path.E ()
|
||||
reactivePaths e =
|
||||
let ok e = case e of
|
||||
App (App (Ref (R.Builtin "View.cell")) (App (Ref (R.Builtin "View.reactive")) v)) e -> True
|
||||
App (App (Ref (R.Builtin "View.view")) (App (Ref (R.Builtin "View.reactive")) v)) e -> True
|
||||
_ -> False
|
||||
in Term.matchingPaths ok e
|
||||
|
||||
|
@ -37,15 +37,20 @@ data Node m k t e = Node {
|
||||
dependencies :: Maybe (S.Set k) -> k -> Noted m (S.Set k),
|
||||
-- | Lookup the set of terms/types depending directly on the given @k@, optionally limited to the given set
|
||||
dependents :: Maybe (S.Set k) -> k -> Noted m (S.Set k),
|
||||
-- | Modify the given subterm, which may fail
|
||||
-- | Modify the given subterm, which may fail. First argument is the root path.
|
||||
-- Second argument is path relative to the root.
|
||||
-- Returns (root path, original e, edited e)
|
||||
editTerm :: P.Path -> P.Path -> A.Action -> e -> Noted m (P.Path,e,e),
|
||||
-- | Modify the given type, which may fail
|
||||
editType :: P.Path -> A.Action -> t -> Noted m t,
|
||||
-- Evaluate all terms, returning a list of (path, original e, evaluated e)
|
||||
evaluateTerms :: [(P.Path, e)] -> Noted m [(P.Path,e,e)],
|
||||
-- | Returns ( current type
|
||||
-- , admissible type
|
||||
-- , local vars
|
||||
-- , well-typed applications of focus
|
||||
-- , well-typed expressions involving local vars )
|
||||
-- | Modify the given subterm, which may fail. First argument is the root path.
|
||||
localInfo :: e -> P.Path -> Noted m (t, t, [e], [Int], [e]),
|
||||
-- | Access the metadata for the term and/or types identified by @k@
|
||||
metadatas :: [k] -> Noted m (Map k (MD.Metadata k)),
|
||||
|
@ -3,6 +3,7 @@ module Unison.Node.Common (node) where
|
||||
|
||||
import Control.Applicative
|
||||
import Data.Traversable (traverse)
|
||||
import qualified Data.Foldable as Foldable
|
||||
import Data.List
|
||||
import Data.Ord
|
||||
import Debug.Trace
|
||||
@ -64,6 +65,13 @@ node eval store =
|
||||
|
||||
editType = error "Common.editType.todo"
|
||||
|
||||
evaluateTerms es = join <$> traverse go es
|
||||
where go (path,e) =
|
||||
maybe (pure [])
|
||||
(\e -> (\e' -> [(path,e,e')]) <$>
|
||||
(Eval.whnf eval (readTerm store) e))
|
||||
(Path.at path e)
|
||||
|
||||
metadatas hs =
|
||||
M.fromList <$> sequence (map (\h -> (,) h <$> readMetadata store h) hs)
|
||||
|
||||
@ -139,6 +147,7 @@ node eval store =
|
||||
dependents
|
||||
edit
|
||||
editType
|
||||
evaluateTerms
|
||||
localInfo
|
||||
metadatas
|
||||
search
|
||||
|
@ -90,6 +90,10 @@ server port node = S.scotty port $ do
|
||||
(loc, a, t) <- S.jsonData
|
||||
t <- runN $ N.editType node loc a t
|
||||
S.json t
|
||||
postRoute "/evaluate-terms" $ do
|
||||
es <- S.jsonData
|
||||
e <- runN $ N.evaluateTerms node es
|
||||
S.json e
|
||||
postRoute "/local-info" $ do
|
||||
(e, path) <- S.jsonData
|
||||
t <- runN $ N.localInfo node e path
|
||||
|
Loading…
Reference in New Issue
Block a user