Check-in [05a19c2cc0]
Not logged in

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:Add org file, and work from Idris book
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA3-256:05a19c2cc05709d34c5e505fab3283e48b5493ace99ea86ead6d1f5586fca45b
User & Date: sehqlr 2017-11-10 18:32:55
Context
2017-11-14
23:09
Wrote out more of the decription of the app check-in: 4288c65de8 user: sehqlr tags: trunk
2017-11-10
18:32
Add org file, and work from Idris book check-in: 05a19c2cc0 user: sehqlr tags: trunk
18:28
initial empty check-in check-in: 6a1458dc71 user: sehqlr tags: trunk
Changes
Hide Diffs Unified Diffs Ignore Whitespace Patch

Added DataStore.idr.



























































































































































































































































>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
module Main

import Data.Vect

infixr 5 .+.

data Schema = SString
            | SInt
            | (.+.) Schema Schema

SchemaType : Schema -> Type
SchemaType SString = String
SchemaType SInt = Int
SchemaType (x .+. y) = (SchemaType x, SchemaType y)

record DataStore where
       constructor MkData
       schema : Schema
       size : Nat
       items : Vect size (SchemaType schema)

addToStore : (store : DataStore) -> SchemaType (schema store) -> DataStore
addToStore (MkData schema size store) newitem
           = MkData schema _ (addToData store)
  where
    addToData : Vect oldsize (SchemaType schema) ->
                Vect (S oldsize) (SchemaType schema)
    addToData [] = [newitem]
    addToData (item :: items) = item :: addToData items

data Command : Schema -> Type where
     SetSchema : (newschema : Schema) -> Command schema
     Add : SchemaType schema -> Command schema
     Get : Integer -> Command schema
     Quit : Command schema

parsePrefix : (schema : Schema) -> String -> Maybe (SchemaType schema, String)
parsePrefix SString input = getQuoted (unpack input)
  where
    getQuoted : List Char -> Maybe (String, String)
    getQuoted ('"' :: xs)
      = case span (/= '"') xs of
        (quoted, '"' :: rest) => Just (pack quoted, ltrim (pack rest))
        _ => Nothing
    getQuoted _ = Nothing
parsePrefix SInt input = case span isDigit input of
                              ("", rest) => Nothing
                              (num, rest) => Just (cast num, ltrim rest)
parsePrefix (schemal .+. schemar) input = do
                                        (l_val, input') <- parsePrefix schemal input
                                        (r_val, input'') <- parsePrefix schemar input'
                                        Just ((l_val, r_val), input')

parseBySchema : (schema : Schema) -> String -> Maybe (SchemaType schema)
parseBySchema schema input = case parsePrefix schema input of
                                  Nothing => Nothing
                                  Just (res, "") => Just res
                                  Just _ => Nothing

parseSchema : List String -> Maybe Schema
parseSchema ("String" :: xs) = case xs of
                                    [] => Just SString
                                    _ => case parseSchema xs of
                                               Nothing => Nothing
                                               Just xs_sch => Just (SString .+. xs_sch)
parseSchema ("Int" :: xs) = case xs of
                                 [] => Just SInt
                                 _ => case parseSchema xs of
                                            Nothing => Nothing
                                            Just xs_sch => Just (SInt .+. xs_sch)
parseSchema _ = Nothing

parseCommand : (schema : Schema) -> String -> String -> Maybe (Command schema)
parseCommand schema "add" rest = case parseBySchema schema rest of
                                      Nothing => Nothing
                                      Just restok => Just (Add restok)
parseCommand schema "get" val = case all isDigit (unpack val) of
                                     False => Nothing
                                     True => Just (Get (cast val))
parseCommand schema "quit" "" = Just Quit
parseCommand schema "schema" rest = case parseSchema (words rest) of
                                         Nothing => Nothing
                                         Just schemaok => Just (SetSchema schemaok)
parseCommand _ _ _ = Nothing

parse : (schema : Schema) ->
        (input : String) -> Maybe (Command schema)
parse schema input = case span (/= ' ') input of
                          (cmd, args) => parseCommand schema cmd (ltrim args)

display : SchemaType schema -> String
display {schema = SString} item = show item
display {schema = SInt} item = show item
display {schema = (x .+. y)} (iteml, itemr)
        = display iteml ++ ", " ++ display itemr

getEntry : (pos : Integer) -> (store : DataStore) ->
           Maybe (String, DataStore)
getEntry pos store
  = let store_items = items store in
        case integerToFin pos (size store) of
             Nothing => Just ("Out of range\n", store)
             Just id => let display' = display (index id store_items) in
                            Just (display' ++ "\n", store)

setSchema : (store : DataStore) -> Schema -> Maybe DataStore
setSchema store schema = case size store of
                              Z => Just (MkData schema _ [])
                              (S k) => Nothing

processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store input
  = case parse (schema store) input of
         Nothing => Just ("Invalid command\n", store)
         Just (Add item) =>
           Just ("ID " ++ show (size store) ++ "\n", addToStore store item)
         Just (Get pos) => getEntry pos store
         Just (SetSchema schema') => case setSchema store schema' of
                                           Nothing => Just ("Can't update schema\n", store)
                                           Just store' => Just ("OK\n", store')
         Just Quit => Nothing

main : IO ()
main = replWith (MkData SString _ [])
                "Command: " processInput

Added Project.org.





















































































>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
#+TITLE: Static: a semi-dynamic documents-as-database web content management system

This is a literate programming document for this project. Version control will
be Fossil SCM.

* What does the tagline mean?
  The tagline for this project is, "a database-as-document web content
  management system". Since these are pre-buzzwords, no one can guess the meaning.
  
** "semi-dynamic" means blending the best parts of static and dynamic sites
   Web sites and applications are either static files only or
   static template files injected with data, AKA "dynamic web
   pages". This system will be a hybrid of the two. The first
   iterations of this project will only support the static site
   half of the equation first, since the dynamic site features
   depend on them.
** "database-as-documents" means whole documents are stored in a database
   HTTP revolves around documents, which are typically stored within a web
   servers' file system. Dynamic sites combine static template files with
   queries to a data store. I want to create is a system where all of the
   documents on a server are wholly within a database system, and HTTP
   requests are mapped to SQL statements. There are a lot of technical
   implications with this kind of system, especially when it comes to
   security, which we'll explore.
** Web Content Management System means an integrated tool
   I want an integrated tool that handles the web server, document
   versioning, static site generation, and everything else that developers
   know how to do today, but can also be used by normal folks. I also want
   a tool that can run locally and remotely the same, like Fossil SCM.

* What this document is
  This is going to be a Literate Programming document that will implement the
  software described above, or at least, some integration testing. I plan on
  using Idris as the language, since it's the newest thing I'm learning, but
  if I'm serious about this idea, then I'd need to implement it in a more
  mainstream language. This will also chronicle the TODO items for this.

  The tangled version of this will actually export Literate Idris files,
  which will then be tangled and woven separately.

* Functional Description
  This is the beginnings of a specification that will be implemented as 

Added main.idr.





>
>
1
2
module Main