(* Copyright (C) 2005, HELM Team.
 * 
 * This file is part of HELM, an Hypertextual, Electronic
 * Library of Mathematics, developed at the Computer Science
 * Department, University of Bologna, Italy.
 * 
 * HELM is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License
 * as published by the Free Software Foundation; either version 2
 * of the License, or (at your option) any later version.
 * 
 * HELM is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with HELM; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
 * MA  02111-1307, USA.
 * 
 * For details, see the HELM World-Wide-Web page,
 * http://helm.cs.unibo.it/
 *)

(* $Id: cicNotationLexer.ml 11028 2010-11-02 17:08:43Z tassi $ *)

open Printf

exception Error of int * int * string

module StringSet = Set.Make(String)



(* Lexer *)
let regexp number = xml_digit+

let regexp ident_letter = [ 'a' - 'z' 'A' - 'Z' ]

  (* must be in sync with "is_ligature_char" below *)
let regexp ligature_char = [ "'`~!?@*()[]<>-+=|:;.,/\"" ]
let regexp ligature = ligature_char ligature_char+

let regexp ident_decoration = '\'' | '?' | '`'
let regexp ident_cont = ident_letter | xml_digit | '_'
let regexp ident_start = ident_letter 
let regexp ident = ident_letter ident_cont* ident_decoration* 
let regexp variable_ident = '_' '_' number
let regexp pident = '_' ident

let regexp tex_token = '\\' ident

let regexp csymbol = '\'' ident

let regexp begincom = "(*"
let regexp endcom = "*)"
let regexp qstring = '"' [^ '"']* '"'




  (* (string, int) Hashtbl.t, with multiple bindings.
   * int is the unicode codepoint *)
let ligatures = Hashtbl.create 23

let _ =
  List.iter
    (fun (ligature, symbol) -> Hashtbl.add ligatures ligature symbol)
    [ ("->", <:unicode<to>>);   ("=>", <:unicode<Rightarrow>>);
      (":=", <:unicode<def>>);
    ]

let error lexbuf msg =
  let begin_cnum, end_cnum = Ulexing.loc lexbuf in
  raise (Error (begin_cnum, end_cnum, msg))
let error_at_end lexbuf msg =
  let begin_cnum, end_cnum = Ulexing.loc lexbuf in
  raise (Error (begin_cnum, end_cnum, msg))


(*
let return_symbol lexbuf s = return lexbuf ("SYMBOL", s)
let return_eoi lexbuf = return lexbuf ("EOI", "")
*)

let remove_quotes s = String.sub s 1 (String.length s - 2)

let mk_lexer token =
  let tok_func stream =
(*     let lexbuf = Ulexing.from_utf8_stream stream in *)
(** XXX Obj.magic rationale.
 * The problem.
 *  camlp5 constraints the tok_func field of Token.glexer to have type:
 *    Stream.t char -> (Stream.t 'te * flocation_function)
 *  In order to use ulex we have (in theory) to instantiate a new lexbuf each
 *  time a char Stream.t is passed, destroying the previous lexbuf which may
 *  have consumed a character from the old stream which is lost forever :-(
 * The "solution".
 *  Instead of passing to camlp5 a char Stream.t we pass a lexbuf, casting it to
 *  char Stream.t with Obj.magic where needed.
 *)
    let lexbuf = Obj.magic stream in
    Token.make_stream_and_location
      (fun () ->
        try
          token lexbuf
        with
        | Ulexing.Error -> error_at_end lexbuf "Unexpected character"
        | Ulexing.InvalidCodepoint p ->
            error_at_end lexbuf (sprintf "Invalid code point: %d" p))
  in
  {
    Token.tok_func = tok_func;
    Token.tok_using = (fun _ -> ());
    Token.tok_removing = (fun _ -> ()); 
    Token.tok_match = (* Token.default_match *) (fun (a,b) () -> a);  
    Token.tok_text = Token.lexer_text;
    Token.tok_comm = None;
  }

let expand_macro lexbuf =
  let macro =
    Ulexing.utf8_sub_lexeme lexbuf 1 (Ulexing.lexeme_length lexbuf - 1)
  in
  try
    ("SYMBOL" ^ (Utf8Macro.expand macro))
  with Utf8Macro.Macro_not_found _ -> 
(* FG: unexpanded TeX macros are terminated by a space for rendering *)     
     "SYMBOL" ^ (Ulexing.utf8_lexeme lexbuf ^ " ")

let remove_quotes s = String.sub s 1 (String.length s - 2)
let remove_left_quote s = String.sub s 1 (String.length s - 1)

let print s t = s := (!s ^ t) (* Printf.fprintf *)

let xmarkup = "\005"
let ymarkup = "\006"

let handle_full_id ch id uri =
  let id' = Printf.sprintf "\005A href=\"%s\"\006%s\005/A\006" uri id
  in
  print ch id'

let handle_full_sym ch s uri desc =
  let uri = try HExtlib.unopt uri
            with Failure _ -> "cic:/fakeuri.def(1)" in
  let s' = Printf.sprintf "\005A title=\"%s\" href=\"%s\"\006%s\005/A\006" desc uri s
  in
  print ch s'

let handle_full_num ch num uri desc =
  let uri = try HExtlib.unopt uri
            with Failure _ -> "cic:/fakeuri.def(1)"
  in 
  let num' = Printf.sprintf "\005A title=\"%s\" href=\"%s\"\006%s\005/A\006" desc uri num
  in
  print ch num'

let handle_tex ch s =
 (* print "TEX:%s" (remove_left_quote (Ulexing.utf8_lexeme lexbuf)) *)
 print ch s

let return_with_loc token begin_cnum end_cnum =
  let flocation = HExtlib.floc_of_loc (begin_cnum,end_cnum) in
   token, flocation

let return lexbuf token =
  let begin_cnum, end_cnum = Ulexing.loc lexbuf in
    return_with_loc token begin_cnum end_cnum

  (** @param k continuation to be invoked when no ligature has been found *)
let ligatures_token k =
  lexer
(*  | ligature ->
      let lexeme = Ulexing.utf8_lexeme lexbuf in
      (match List.rev (Hashtbl.find_all ligatures lexeme) with
      | [] -> (* ligature not found, rollback and try default lexer *)
          Ulexing.rollback lexbuf;
          k lexbuf
      | default_lig :: _ -> (* ligatures found, use the default one *)
          return_symbol lexbuf default_lig) *)
  | eof -> return lexbuf ()
  | _ ->  (* not a ligature, rollback and try default lexer *)
      Ulexing.rollback lexbuf;
      k lexbuf

let handle_interpr loc literal interp outstr =
  try
  (match DisambiguateTypes.InterprEnv.find loc interp with
   | GrafiteAst.Ident_alias (_,uri) -> 
       handle_full_id outstr literal uri
   | GrafiteAst.Symbol_alias (_,uri,desc) -> 
       handle_full_sym outstr literal uri desc
   | GrafiteAst.Number_alias (uri,desc) ->
       handle_full_num outstr literal uri desc)
  with Not_found -> print outstr literal
;;

let level2_ast_token interp outstr =
  let rec aux nesting =
    lexer
    | begincom -> (print outstr (Ulexing.utf8_lexeme lexbuf);
                   aux (nesting+1) lexbuf)
    | endcom -> (print outstr (Ulexing.utf8_lexeme lexbuf);
                 aux (max 0 (nesting-1)) lexbuf)
    | eof -> return lexbuf ()
    | _ -> if nesting > 0
             then (print outstr (Ulexing.utf8_lexeme lexbuf);
                   aux nesting lexbuf)
             else (Ulexing.rollback lexbuf;
                   basic_lexer lexbuf)
  and basic_lexer =
    lexer
    | ident -> let loc = HExtlib.floc_of_loc (Ulexing.loc lexbuf) in
               let id = Ulexing.utf8_lexeme lexbuf in
               handle_interpr loc id interp outstr;
               aux 0 lexbuf
    | variable_ident -> 
               let loc = HExtlib.floc_of_loc (Ulexing.loc lexbuf) in
               let id = Ulexing.utf8_lexeme lexbuf in
               handle_interpr loc id interp outstr;
               aux 0 lexbuf
    | pident -> let loc = HExtlib.floc_of_loc (Ulexing.loc lexbuf) in
                let id = Ulexing.utf8_lexeme lexbuf in
                handle_interpr loc id interp outstr;
                aux 0 lexbuf
    | number -> 
               let loc = HExtlib.floc_of_loc (Ulexing.loc lexbuf) in
               let num = Ulexing.utf8_lexeme lexbuf in
               handle_interpr loc num interp outstr;
               aux 0 lexbuf
    | tex_token -> 
               let loc = HExtlib.floc_of_loc (Ulexing.loc lexbuf) in
               let s = Ulexing.utf8_lexeme lexbuf in
               handle_interpr loc s interp outstr;
               aux 0 lexbuf
    | qstring -> (print outstr (Ulexing.utf8_lexeme lexbuf); aux 0 lexbuf)
    | csymbol -> 
               let loc = HExtlib.floc_of_loc (Ulexing.loc lexbuf) in
               let s = Ulexing.utf8_lexeme lexbuf in
               handle_interpr loc s interp outstr;
               aux 0 lexbuf
    | eof -> return lexbuf ()
    | _ ->
               let loc = HExtlib.floc_of_loc (Ulexing.loc lexbuf) in
               let s = Ulexing.utf8_lexeme lexbuf in
               handle_interpr loc s interp outstr;
               aux 0 lexbuf
  in aux 0
          

(* API implementation *)

(*let mk_small_lexer interpr keywords = 
  let initial_keywords = 
   [ "CProp"; "Prop"; "Type"; "Set"; "let"; "match";
   "with"; "in"; "and"; "to"; "as"; "on"; "return"; "done";
   "rec"; "corec" ]
  in
  (*let status = 
    List.fold_right StringSet.add (initial_keywords @ keywords) StringSet.empty 
  in*)
  mk_lexer (level2_ast_token outstr interpr)
;;*)

let mk_small_printer interpr outstr = 
  let initial_keywords = 
   [ "CProp"; "Prop"; "Type"; "Set"; "let"; "match";
   "with"; "in"; "and"; "to"; "as"; "on"; "return"; "done";
   "rec"; "corec" ]
  in
  (* let status = 
    List.fold_right StringSet.add initial_keywords StringSet.empty 
  in *)
  level2_ast_token interpr outstr
;;

(* let mk_small_lexer interpr = mk_small_lexer interpr [];;*)