0 | module Protocol.IDE.Holes
 1 |
 2 | import Protocol.SExp
 3 |
 4 | %default total
 5 |
 6 | public export
 7 | record HolePremise where
 8 |   constructor MkHolePremise
 9 |   name : String -- Future: send more structured representation of:
10 |                 -- im/explicity (+ default value?) + quantity
11 |   type : String -- Future: String + highlighting info
12 |
13 | export
14 | SExpable HolePremise where
15 |   toSExp premise =
16 |     SExpList [ StringAtom premise.name
17 |              , StringAtom premise.type
18 |              , SExpList [] -- TODO: metadata
19 |              ]
20 |
21 | export
22 | FromSExpable HolePremise where
23 |   fromSExp (SExpList [ StringAtom name
24 |              , StringAtom type
25 |              , SExpList [] -- TODO: metadata
26 |              ]) = do pure $ MkHolePremise
27 |                       {name, type}
28 |   fromSExp _ = Nothing
29 |
30 | public export
31 | record HoleData where
32 |   constructor MkHoleData
33 |   name : String
34 |   type : String -- Future : String + highlighting info
35 |   context : List HolePremise
36 |
37 | export
38 | SExpable HoleData where
39 |   toSExp hole = SExpList
40 |     [ StringAtom (show hole.name)
41 |     , toSExp hole.context
42 |     , SExpList [ toSExp hole.type   -- Conclusion
43 |                , SExpList[]]        -- TODO: Highlighting information
44 |     ]
45 |
46 | export
47 | FromSExpable HoleData where
48 |   fromSExp (SExpList
49 |     [ StringAtom name
50 |     , context
51 |     , SExpList [ conclusion
52 |                , SExpList[]]        -- TODO: Highlighting information
53 |     ]) = do pure $ MkHoleData {name, type = !(fromSExp conclusion), context = !(fromSExp context)}
54 |   fromSExp _ = Nothing
55 |