package lambdapi

You can search for identifiers within the package.

in-package search v0.2.0

Proof assistant for the λΠ-calculus modulo rewriting

Install

dune-project

Dependency

github.com Readme Changelog Edit opam file Versions (12)

Authors

D

Deducteam

Maintainers

D

dedukti-dev@inria.fr

Sources

lambdapi-3.0.0.tbz

sha256=1066aed2618fd8e6a400c5147dbf55ea977ce8d3fe2e518ac6785c6775a1b8be

sha512=f7f499626aba92e070ae69581299a58525973fdbfd04a160ed3ac89209fb6cbe307b816d0b23e1b75bc83467ce8b4b0530c6f9816eaf58f7a07fde65a450106c

doc/src/lambdapi.tool/websearch.ml.html

Source file `websearch.ml`

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
#1 "src/tool/websearch.eml.ml"

let show_form ~from ?(message="") ?output request ~hide_description=

let ___eml_buffer = Buffer.create 4096 in
(Buffer.add_string ___eml_buffer "<link rel=\"stylesheet\"\nhref=\"https://cdnjs.cloudflare.com/ajax/libs/\\\nfont-awesome/6.5.0/css/all.min.css\">\n\n<button id=\"b_showdescription\" name=\"showHideButton\"\nonclick=\"toggleDescription()\" style=\"width: 100%;\">\n<i class=\"fas fa-angles-up\"></i>\n</button>\n\n<script>\nfunction toggleDescription() {\n  const descriptionSection = document.getElementById(\"descriptionSection\");\n  const hideDescrition = document.getElementById(\"hideDescritionSection\");\n  const icon = document.querySelector(\"button i\");\nif(descriptionSection.style.display === \"none\"){\n  descriptionSection.style.display = \"block\";\n  hideDescrition.value = \"false\";\n  icon.className = \"fas fa-angles-up\";\n} else {\n  descriptionSection.style.display = \"none\";\n  hideDescrition.value = \"true\";\n  icon.className = \"fas fa-angles-down\";\n}\n\n}\n</script>\n<html>\n<body>\n\n\n\n  <script>\n  function incr(delta) {\n    document.getElementById(\"from\").value =\n      Math.max(0,delta + Number(document.getElementById(\"from\").value));\n    document.getElementById(\"search\").click();\n  }\n  </script>\n\n  <form method=\"POST\" id=\"form\">\n    ");
(Printf.bprintf ___eml_buffer "%s" (
#44 "src/tool/websearch.eml.ml"
           Dream.csrf_tag request 
));
(Buffer.add_string ___eml_buffer "\n    <p>\n    <input type=\"search\" required=\"true\" size=\"100\"\n      name=\"message\" value=\"");
(Printf.bprintf ___eml_buffer "%s" (Dream.html_escape (
#47 "src/tool/websearch.eml.ml"
                                  message 
)));
(Buffer.add_string ___eml_buffer "\"\n      onfocus=\"this.select();\" autofocus>\n    </p>\n    <p>\n    <input type=\"hidden\" name=\"hideDescritionSection\"\n      id=\"hideDescritionSection\" value=\"");
(Printf.bprintf ___eml_buffer "%s" (Dream.html_escape (
#52 "src/tool/websearch.eml.ml"
                                              hide_description 
)));
(Buffer.add_string ___eml_buffer "\">\n    </p>\n    <p>\n    <input type=\"submit\" value=\"search\" id=\"search\" name=\"search\">\n    </p>\n\n");
#58 "src/tool/websearch.eml.ml"
    begin match output with

#59 "src/tool/websearch.eml.ml"
    | None ->

(Buffer.add_string ___eml_buffer "       <input type=\"hidden\" name=\"from\" value=\"");
(Printf.bprintf ___eml_buffer "%s" (Dream.html_escape (
#60 "src/tool/websearch.eml.ml"
                                                   string_of_int from 
)));
(Buffer.add_string ___eml_buffer "\">\n");
#61 "src/tool/websearch.eml.ml"
    | Some output ->

(Buffer.add_string ___eml_buffer "    <p>\n  <input type=\"number\" required=\"true\" style=\"width: 5em\" min=\"0\" id=\"from\"\n    name=\"from\" value=\"");
(Printf.bprintf ___eml_buffer "%s" (Dream.html_escape (
#64 "src/tool/websearch.eml.ml"
                             string_of_int from 
)));
(Buffer.add_string ___eml_buffer "\" onfocus=\"this.select()\">\n  <input type=\"button\"\n    name=\"prev\" value=\"Prev\" onclick=\"incr(-100)\">\n  <input type=\"button\"\n    name=\"next\" value=\"Next\" onclick=\"incr(100)\">\n  </p>\n  ");
(Printf.bprintf ___eml_buffer "%s" (
#70 "src/tool/websearch.eml.ml"
         output 
));
(Buffer.add_string ___eml_buffer "\n");
#71 "src/tool/websearch.eml.ml"
    end;

(Buffer.add_string ___eml_buffer "    </form>\n\n</body>\n</html>\n\n");
(Buffer.contents ___eml_buffer)
#77 "src/tool/websearch.eml.ml"
let start ~header ss ~port ~dbpath ~path_in_url () =
  (*Common.Logger.set_debug true "e" ;*)
  let interface = "0.0.0.0" in
  Dream.run ~port ~interface
  @@ Dream.logger
  @@ Dream.memory_sessions
  @@ Dream.router [

    Dream.get  ("/" ^ path_in_url)
      (fun request ->
        Dream.html
          (header ^ show_form ~from:0 request ~hide_description:"false"));

    Dream.post ("/" ^ path_in_url)
      (fun request ->
        match%lwt Dream.form request with
        | `Ok
          [ "from", from;
            "hideDescritionSection", hideDescritionSection;
            "message", message;
            "search", _search ] ->
          Dream.log "from1 = %s" from ;
          let from = int_of_string from in (* XXX CSC exception XXX *)
          Dream.log "from2 = %d" from ;
          if Timed.(!Common.Console.verbose) >= 2 then
            Dream.log "Received request = %s" message;
          let output =
            Indexing.search_cmd_html ss ~from ~how_many:100
            message ~dbpath in
          if Timed.(!Common.Console.verbose) >= 3 then
            Dream.log "sending response: %s" output;
          let header = match hideDescritionSection with
          | "true" ->
              Str.global_replace (Str.regexp_string "%%HIDE_DESCRIPTION%%")
                "none"
                header
          | _ ->
              Str.global_replace (Str.regexp_string "%%HIDE_DESCRIPTION%%")
                "block"
                header
          in
          Dream.html
            (header ^
            show_form ~from ~message ~output request
              ~hide_description:hideDescritionSection)

        | _ ->
          Dream.log "no match" ;
          Dream.empty `Bad_Request);

  ]