src/Tools/Find_Facts/web/src/Query.elm
author wenzelm
Sat, 11 Jan 2025 21:31:13 +0100 (3 months ago)
changeset 81764 fcba3250fb2a
permissions -rw-r--r--
original sources of find-facts 271b5af0c4c8;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
81764
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
     1
{- Author: Fabian Huch, TU Muenchen
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
     2
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
     3
Queries against the find facts server.
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
     4
-}
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
     5
module Query exposing (Atom(..), Filter(..), Select, Query, Query_Blocks, empty, empty_query,
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
     6
  encode_query, encode_query_blocks, encode_query_block, Block, Blocks, Facets, Result,
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
     7
  decode_block, decode_blocks, decode_result)
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
     8
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
     9
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    10
import Dict exposing (Dict)
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    11
import Json.Decode as Decode
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    12
import Json.Decode.Extra as Decode
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    13
import Json.Encode as Encode
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    14
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    15
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    16
{- queries -}
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    17
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    18
type Atom = Value String | Exact String
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    19
type Filter = Any_Filter (List Atom) | Field_Filter String (List Atom)
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    20
type alias Select = {field: String, values: List String}
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    21
type alias Query = {filters: List Filter, exclude: List Filter, selects: List Select}
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    22
type alias Query_Blocks = {query: Query, cursor: String}
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    23
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    24
empty: Query
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    25
empty = Query [] [] []
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    26
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    27
empty_atom: Atom -> Bool
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    28
empty_atom atom =
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    29
  case atom of
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    30
    Value s -> String.words s |> List.isEmpty
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    31
    Exact s -> String.words s |> List.isEmpty
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    32
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    33
empty_filter: Filter -> Bool
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    34
empty_filter filter =
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    35
  case filter of
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    36
    Any_Filter atoms -> List.all empty_atom atoms
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    37
    Field_Filter _ atoms -> List.all empty_atom atoms
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    38
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    39
empty_select: Select -> Bool
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    40
empty_select select = List.isEmpty select.values
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    41
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    42
empty_query: Query -> Bool
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    43
empty_query query =
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    44
  List.all empty_filter (query.filters ++ query.exclude) && List.all empty_select query.selects
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    45
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    46
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    47
{- json encoding -}
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    48
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    49
encode_atom: Atom -> Encode.Value
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    50
encode_atom atom =
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    51
  case atom of
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    52
    Exact phrase -> Encode.object [("exact", Encode.string phrase)]
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    53
    Value wildcard -> Encode.object [("value", Encode.string wildcard)]
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    54
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    55
encode_filter: Filter -> Encode.Value
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    56
encode_filter filter =
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    57
  case filter of
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    58
    Any_Filter atoms -> Encode.object [("either", Encode.list encode_atom atoms)]
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    59
    Field_Filter field atoms ->
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    60
      Encode.object [("either", Encode.list encode_atom atoms), ("field", Encode.string field)]
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    61
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    62
encode_select: Select -> Encode.Value
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    63
encode_select select =
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    64
  Encode.object [
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    65
    ("field", Encode.string select.field),
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    66
    ("values", Encode.list Encode.string select.values)]
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    67
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    68
encode_query: Query -> Encode.Value
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    69
encode_query query =
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    70
  Encode.object [
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    71
    ("filters", Encode.list encode_filter query.filters),
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    72
    ("exclude", Encode.list encode_filter query.exclude),
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    73
    ("selects", Encode.list encode_select query.selects)]
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    74
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    75
encode_query_blocks: Query_Blocks -> Encode.Value
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    76
encode_query_blocks query_blocks =
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    77
  Encode.object
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    78
    [("query", encode_query query_blocks.query), ("cursor", Encode.string query_blocks.cursor)]
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    79
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    80
encode_query_block: String -> Encode.Value
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    81
encode_query_block id = Encode.object [("id", Encode.string id)]
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    82
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    83
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    84
{- results -}
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    85
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    86
type alias Block = {
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    87
  id: String,
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    88
  chapter: String,
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    89
  session: String,
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    90
  theory: String,
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    91
  file: String,
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    92
  file_name: String,
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    93
  url: String,
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    94
  command: String,
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    95
  start_line: Int,
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    96
  src_before: String,
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    97
  src_after: String,
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    98
  html: String,
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
    99
  entity_kname: Maybe String}
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   100
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   101
type alias Blocks = {num_found: Int, blocks: List Block, cursor: String}
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   102
type alias Facets = Dict String (Dict String Int)
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   103
type alias Result = {blocks: Blocks, facets: Facets}
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   104
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   105
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   106
{- json decoding -}
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   107
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   108
decode_block: Decode.Decoder Block
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   109
decode_block =
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   110
  Decode.succeed Block
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   111
  |> Decode.andMap (Decode.field "id" Decode.string)
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   112
  |> Decode.andMap (Decode.field "chapter" Decode.string)
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   113
  |> Decode.andMap (Decode.field "session" Decode.string)
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   114
  |> Decode.andMap (Decode.field "theory" Decode.string)
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   115
  |> Decode.andMap (Decode.field "file" Decode.string)
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   116
  |> Decode.andMap (Decode.field "file_name" Decode.string)
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   117
  |> Decode.andMap (Decode.field "url" Decode.string)
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   118
  |> Decode.andMap (Decode.field "command" Decode.string)
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   119
  |> Decode.andMap (Decode.field "start_line" Decode.int)
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   120
  |> Decode.andMap (Decode.field "src_before" Decode.string)
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   121
  |> Decode.andMap (Decode.field "src_after" Decode.string)
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   122
  |> Decode.andMap (Decode.field "html" Decode.string)
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   123
  |> Decode.andMap (Decode.field "entity_kname" (Decode.maybe Decode.string))
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   124
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   125
decode_blocks: Decode.Decoder Blocks
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   126
decode_blocks =
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   127
  Decode.map3 Blocks
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   128
    (Decode.field "num_found" Decode.int)
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   129
    (Decode.field "blocks" (Decode.list decode_block))
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   130
    (Decode.field "cursor" Decode.string)
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   131
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   132
decode_facets: Decode.Decoder Facets
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   133
decode_facets = Decode.dict (Decode.dict Decode.int)
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   134
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   135
decode_result: Decode.Decoder Result
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   136
decode_result =
fcba3250fb2a original sources of find-facts 271b5af0c4c8;
wenzelm
parents:
diff changeset
   137
  Decode.map2 Result (Decode.field "blocks" decode_blocks) (Decode.field "facets" decode_facets)