OCaml

(* Copyright 2023 - 2023, Nitrokey GmbH
   SPDX-License-Identifier: EUPL-1.2
*)

val reporter : Logs.reporter -> Logs.reporter

open Eliom_content
open Html5.D

module type Skeleton =
  sig

    val css_files : string list list
    val js_files : string list list
    val other_header : Html5_types.head_content_fun Html5.elt list
  end

    
module Make (F : Skeleton) =
  struct 

    let raw title content =
      Eliom_tools.F.html
        ~title:title
        ~css:F.css_files
        ~js:F.js_files
        ~other_head:([
          meta
            ~a:[
              a_name "viewport";
              a_content "width = device-width"
            ] ()
        ]@F.other_header)
        (Html5.F.body content)
        
    let return title content =
      raw title content
      |> Lwt.return
                      
  end

module Base : Skeleton =
  struct

    let js_files = []
    let css_files =
      [
        ["css"; "knacss.css"];
        ["css"; "constrictor.css"];
        ["css"; "boa.css"];
        ["css"; "ghost.css"];
      ]
    let other_header = []
  end

include Make(Base)

module MBBase : Skeleton =
  struct

    let css_files = Base.css_files  
    let js_files = []
    let other_header =
      [
        css_link
          ~uri:(
            Raw.uri_of_string
              "https://api.tiles.mapbox.com/mapbox.js/v2.1.5/mapbox.css"
          ) ();
        js_script
          ~uri:(
            Raw.uri_of_string
              "https://api.tiles.mapbox.com/mapbox.js/v2.1.5/mapbox.js"
          ) ();
        
      ]
  end

module Mapbox = Make(MBBase)

{
  open Lexing
  open CodeLoc
  open WParser

  exception SyntaxError of string
  let l_start_string = ref CodeLoc.dummy
}


let digit = ['0'-'9']
let letter = ['a'-'z''A'-'Z']
let gvars = "gvar_" digit+ (* generated variables during compilation *)
let identifier = letter(letter|digit|'_')*
let lvar = '#' (letter|digit|'_'|'$')*
let integer = digit+
let float = digit* '.' digit*
let loc = "$l" (letter|digit|'_')*
let white = [' ' '\t']+
let newline = '\r' | '\n' | "\r\n"

rule read =
  parse
  (* keywords *)
  | "@config" { CONFIG (curr lexbuf) }
  | "true"   { TRUE (curr lexbuf) }
  | "false"  { FALSE (curr lexbuf) }
  | "nil"    { LSTNIL (curr lexbuf) }
  | "null"   { NULL (curr lexbuf) }
  | "while"  { WHILE (curr lexbuf) }
  | "if"     { IF (curr lexbuf) }
  | "else"   { ELSE (curr lexbuf) }
  | "skip"   { SKIP (curr lexbuf) }
  | "fresh"  { FRESH (curr lexbuf) }
  | "new"    { NEW (curr lexbuf) }
  | "free"   { DELETE (curr lexbuf) }
  | "dispose"{ DELETE (curr lexbuf) }
  | "function" { FUNCTION (curr lexbuf) }
  | "par"    { PAR (curr lexbuf) }
  | "predicate" { PREDICATE (curr lexbuf) }
  | "invariant" { INVARIANT (curr lexbuf) }
  | "return" { RETURN (curr lexbuf) }
  | "fold"   { FOLD (curr lexbuf) }
  | "package" { PACKAGE (curr lexbuf) }
  | "unfold" { UNFOLD (curr lexbuf) }
  | "nounfold" { NOUNFOLD (curr lexbuf) }
  | "apply"  { APPLY (curr lexbuf) }
  | "assert" { ASSERT (curr lexbuf) }
  | "assume" { ASSUME (curr lexbuf) }
  | "assume_type" { ASSUME_TYPE (curr lexbuf) }
  | "with" { WITH (curr lexbuf) }
  | "variant" { VARIANT (curr lexbuf) }
  | "statement" { STATEMENT (curr lexbuf) }
  | "proof"  { PROOF (curr lexbuf) }
  | "lemma"  { LEMMA (curr lexbuf) }
  | "forall" { FORALL (curr lexbuf) }
  | "bind" { EXIST (curr lexbuf) }
  | "spec" { SPEC (curr lexbuf) }
  (* types *)
  | "List" { TLIST (curr lexbuf) }
  | "Int" { TINT (curr lexbuf) }
  | "Bool" { TBOOL (curr lexbuf) }
  | "String" { TSTRING (curr lexbuf) }
  | "Float" { TFLOAT (curr lexbuf) }
  (* strings and comments *)
  | '"'      { let () = l_start_string := curr lexbuf in
               read_string (Buffer.create 17) lexbuf }
  | "//"     { read_comment lexbuf }
  (* logical binary stuff *)
  | "-*"     { WAND }
  | "->"     { ARROW }
  | "-b>"   { BLOCK_ARROW }
  | "/\\"    { AND }
  | "\\/"    { OR }
  (* punctuation *)
  | "-{"     { SETOPEN (curr lexbuf) }
  | "}-"     { SETCLOSE (curr lexbuf) }
  | "[["     { LOGOPEN (curr lexbuf) }
  | "]]"     { LOGCLOSE(curr lexbuf) }
  | '['      { LBRACK (curr lexbuf) }
  | ']'      { RBRACK (curr lexbuf) }
  | '{'      { LCBRACE (curr lexbuf) }
  | '}'      { RCBRACE (curr lexbuf) }
  | '('      { LBRACE (curr lexbuf) }
  | ')'      { RBRACE (curr lexbuf) }
  | ":="     { ASSIGN (curr lexbuf) }
  | ':'      { COLON (curr lexbuf) }
  | ','      { COMMA (curr lexbuf) }
  | "."      { DOT (curr lexbuf) }
  | ';'      { SEMICOLON (curr lexbuf) }
  | "|-"     { VDASH (curr lexbuf) }
  (* binary operators *)
  | "::"     { LSTCONS }
  | '@'      { LSTCAT }
  | "=="     { EQUAL }
  | ">="     { GREATEREQUAL }
  | '>'      { GREATERTHAN }
  | '<'      { LESSTHAN }
  | "<="     { LESSEQUAL }
  | "f>="    { FGREATEREQUAL }
  | "f>"     { FGREATERTHAN }
  | "f<"     { FLESSTHAN }
  | "f<="    { FLESSEQUAL }
  | '+'      { PLUS }
  | '-'      { MINUS }
  | '*'      { TIMES }
  | '/'      { DIV }
  | '%'      { MOD }
  | "f+"     { FPLUS }
  | "f-"     { FMINUS }
  | "f*"     { FTIMES }
  | "f/"     { FDIV }
  | "f%"     { FMOD }
  | "&&"     { AND }
  | "||"     { OR }
  | "!="     { NEQ }
  | "lnth"   { LSTNTH }
  (* unary operators *)
  | "emp"    { EMP (curr lexbuf) }
  | "len"    { LEN (curr lexbuf) }
  | "hd"     { HEAD (curr lexbuf) }
  | "tl"     { TAIL (curr lexbuf) }
  | "rev"    { REV (curr lexbuf) }
  | "sub"    { SUB (curr lexbuf) }
  | '!'      { NOT (curr lexbuf) }
  (* identifiers *)
  | white    { read lexbuf }
  | newline  { new_line lexbuf; read lexbuf }
  | float    { FLOAT (curr lexbuf, float_of_string (Lexing.lexeme lexbuf)) }
  | integer   { INTEGER (curr lexbuf, int_of_string (Lexing.lexeme lexbuf)) }
  | gvars    { IDENTIFIER (curr lexbuf, (Lexing.lexeme lexbuf)^"_user") } (* if it has a name of generated var, we add _user *)
  | identifier { IDENTIFIER (curr lexbuf, Lexing.lexeme lexbuf) }
  | lvar       { LVAR (curr lexbuf, Lexing.lexeme lexbuf) }
  | _ { raise (SyntaxError ("Unexpected char: " ^ Lexing.lexeme lexbuf)) }
  | eof      { EOF }

and read_string buf =
  parse
  | '"'       { let lend = curr lexbuf in
                let loc = merge (!l_start_string) lend in
                STRING (loc, Buffer.contents buf) }
  | '\\' '/'  { Buffer.add_char buf '/'; read_string buf lexbuf }
  | '\\' '\\' { Buffer.add_char buf '\\'; read_string buf lexbuf }
  | '\\' 'b'  { Buffer.add_char buf '\b'; read_string buf lexbuf }
  | '\\' 'f'  { Buffer.add_char buf '\012'; read_string buf lexbuf }
  | '\\' 'n'  { Buffer.add_char buf '\n'; read_string buf lexbuf }
  | '\\' 'r'  { Buffer.add_char buf '\r'; read_string buf lexbuf }
  | '\\' 't'  { Buffer.add_char buf '\t'; read_string buf lexbuf }
  | [^ '"' '\\']+
    { Buffer.add_string buf (Lexing.lexeme lexbuf);
      read_string buf lexbuf
    }
  | _ { raise (SyntaxError ("Illegal string character: " ^ Lexing.lexeme lexbuf)) }
  | eof { raise (SyntaxError ("String is not terminated")) }

and read_comment =
  parse
  | newline { new_line lexbuf; read lexbuf }
  | eof     { EOF }
  | _       { read_comment lexbuf }