From 2914bfbeac3c2e0f53ba8c612cd11b3b2afbabce Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Thu, 19 May 2011 14:14:06 +0000 Subject: [PATCH] Added matitadaemon. --- matitaB/components/content_pres/.depend | 6 + .../content_pres/cicNotationLexer.ml | 4 +- .../components/disambiguation/disambiguate.ml | 37 +- matitaB/components/ng_library/nCicLibrary.ml | 5 +- matitaB/matita/.depend | 48 +-- matitaB/matita/matitaScriptLexer.ml | 344 ++++++++++++++++++ matitaB/matita/matitaScriptLexer.mli | 34 ++ matitaB/matita/matitadaemon.ml | 203 +++++++++++ 8 files changed, 637 insertions(+), 44 deletions(-) create mode 100644 matitaB/matita/matitaScriptLexer.ml create mode 100644 matitaB/matita/matitaScriptLexer.mli create mode 100644 matitaB/matita/matitadaemon.ml diff --git a/matitaB/components/content_pres/.depend b/matitaB/components/content_pres/.depend index 5c11c1ded..f519ea34f 100644 --- a/matitaB/components/content_pres/.depend +++ b/matitaB/components/content_pres/.depend @@ -1,5 +1,7 @@ renderingAttrs.cmi: cicNotationLexer.cmi: +interpTable.cmi: +smallLexer.cmi: cicNotationParser.cmi: mpresentation.cmi: box.cmi: @@ -12,6 +14,10 @@ renderingAttrs.cmo: renderingAttrs.cmi renderingAttrs.cmx: renderingAttrs.cmi cicNotationLexer.cmo: cicNotationLexer.cmi cicNotationLexer.cmx: cicNotationLexer.cmi +interpTable.cmo: interpTable.cmi +interpTable.cmx: interpTable.cmi +smallLexer.cmo: smallLexer.cmi +smallLexer.cmx: smallLexer.cmi cicNotationParser.cmo: cicNotationLexer.cmi cicNotationParser.cmi cicNotationParser.cmx: cicNotationLexer.cmx cicNotationParser.cmi mpresentation.cmo: mpresentation.cmi diff --git a/matitaB/components/content_pres/cicNotationLexer.ml b/matitaB/components/content_pres/cicNotationLexer.ml index 2f428babc..ce8fcec54 100644 --- a/matitaB/components/content_pres/cicNotationLexer.ml +++ b/matitaB/components/content_pres/cicNotationLexer.ml @@ -73,10 +73,10 @@ let regexp uri = ("(" number (',' number)* ")")? (* reference spec *) let regexp qstring = '"' [^ '"']* '"' -let regexp hreftag = "" let regexp tex_token = '\\' ident diff --git a/matitaB/components/disambiguation/disambiguate.ml b/matitaB/components/disambiguation/disambiguate.ml index 34cb4ee2f..5ce1386ae 100644 --- a/matitaB/components/disambiguation/disambiguate.ml +++ b/matitaB/components/disambiguation/disambiguate.ml @@ -525,8 +525,8 @@ let bfvisit ~pp_term top_split test t = | [] -> None | (ctx0,t0 as hd)::tl -> (* prerr_endline ("ok! length tl = " ^ string_of_int (List.length tl)); *) - prerr_endline ("visiting t0 = " ^ pp_term t0); - if test t0 then (prerr_endline "t0 is ambiguous"; Some hd) + debug_print (lazy ("visiting t0 = " ^ pp_term t0)); + if test t0 then (debug_print (lazy "t0 is ambiguous"); Some hd) else (* (prerr_endline ("splitting not ambiguous t0:"); @@ -590,7 +590,7 @@ let test_interpr ~context ~metasenv ~subst ~use_coercions ~expty ~env ~universe in match (refine_profiler.HExtlib.profile foo ()) with | Ko x -> let _,err = Lazy.force x in - prerr_endline ("test_interpr error: " ^ err); + debug_print (lazy ("test_interpr error: " ^ err)); false | _ -> true with @@ -625,8 +625,8 @@ let rec disambiguate_list let res = Environment.find item universe in - prerr_endline (Printf.sprintf "choices for %s :\n%s" - (d2s item) (String.concat ", " (List.map a2s res))); + debug_print (lazy (Printf.sprintf "choices for %s :\n%s" + (d2s item) (String.concat ", " (List.map a2s res)))); res in @@ -641,7 +641,7 @@ let rec disambiguate_list match ts with | [] -> None | t0 :: tl -> - prerr_endline ("disambiguate_list: t0 = " ^ pp_thing t0); + debug_print (lazy ("disambiguate_list: t0 = " ^ pp_thing t0)); let is_ambiguous = function | Ast.Ident (_,`Ambiguous) | Ast.Num (_,None) @@ -658,21 +658,21 @@ let rec disambiguate_list (* get first ambiguous subterm (or return disambiguated term) *) match visit ~pp_term is_ambiguous t0 with | None -> - prerr_endline ("visit -- not ambiguous node:\n" ^ pp_thing t0); + debug_print (lazy ("visit -- not ambiguous node:\n" ^ pp_thing t0)); Some (t0,tl) | Some (ctx, t) -> - prerr_endline ("visit -- found ambiguous node: " ^ astpp t ^ - "\nin " ^ pp_thing (ctx t)); + debug_print (lazy ("visit -- found ambiguous node: " ^ astpp t ^ + "\nin " ^ pp_thing (ctx t))); (* get possible instantiations of t *) let instances = get_instances ctx t in - prerr_endline ("-- possible instances:"); + debug_print (lazy "-- possible instances:"); List.iter - (fun u0 -> prerr_endline ("-- instance: " ^ (pp_thing u0))) instances; + (fun u0 -> debug_print (lazy ("-- instance: " ^ (pp_thing u0)))) instances; (* perforate ambiguous subterms and test refinement *) - prerr_endline ("-- survivors:"); + debug_print (lazy "-- survivors:"); let survivors = List.filter test_interpr instances in List.iter - (fun u0 -> prerr_endline ("-- survivor: " ^ (pp_thing u0))) survivors; + (fun u0 -> debug_print (lazy ("-- survivor: " ^ (pp_thing u0)))) survivors; disambiguate_list (survivors@tl) ;; @@ -703,29 +703,30 @@ let disambiguate_thing let refine t = let localization_tbl = mk_localization_tbl 503 in - prerr_endline "before interpretate_thing"; + debug_print (lazy "before interpretate_thing"); let t' = interpretate_thing ~context ~env ~universe ~uri ~is_path:false t ~localization_tbl in - prerr_endline "after interpretate_thing"; + debug_print (lazy "after interpretate_thing"); match refine_thing metasenv subst context uri ~use_coercions t' expty base_univ ~localization_tbl with | Ok (t',m',s',u') -> t,m',s',t',u' | Uncertain x -> let _,err = Lazy.force x in - prerr_endline ("refinement uncertain after disambiguation: " ^ err); + debug_print (lazy ("refinement uncertain after disambiguation: " ^ err)); assert false | _ -> assert false in if not (test_interpr thing) then - (prerr_endline ("preliminary test fail: " ^ pp_thing thing); + (debug_print (lazy ("preliminary test fail: " ^ pp_thing thing)); raise (NoWellTypedInterpretation (0,[]))) else let res = aux [thing] in let res = HExtlib.filter_map (fun t -> try Some (refine t) - with _ -> prerr_endline ("can't interpretate/refine " ^ (pp_thing t));None) res + with _ -> + debug_print (lazy ("can't interpretate/refine " ^ (pp_thing t)));None) res in match res with | [] -> raise (NoWellTypedInterpretation (0,[])) diff --git a/matitaB/components/ng_library/nCicLibrary.ml b/matitaB/components/ng_library/nCicLibrary.ml index 87f0cb31b..92c57b123 100644 --- a/matitaB/components/ng_library/nCicLibrary.ml +++ b/matitaB/components/ng_library/nCicLibrary.ml @@ -231,13 +231,16 @@ module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status assert (not (List.mem tag !already_registered)); already_registered := tag :: !already_registered; let old_require1 = !require1 in + prerr_endline "let old_require 1 superata"; require1 := (fun ~alias_only ((tag',data) as x) -> if tag=tag' then + (prerr_endline ("requiring tag': " ^ tag'); require (Obj.magic data) ~refresh_uri_in_universe ~refresh_uri_in_term - ~refresh_uri_in_reference ~alias_only + ~refresh_uri_in_reference ~alias_only) else old_require1 ~alias_only x); + prerr_endline ("added require tag" ^ tag); (fun x -> tag,Obj.repr x) end diff --git a/matitaB/matita/.depend b/matitaB/matita/.depend index b2221fe0b..83c43b74d 100644 --- a/matitaB/matita/.depend +++ b/matitaB/matita/.depend @@ -12,8 +12,10 @@ matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi matitac.cmo: matitaclean.cmi matitaMisc.cmi matitaInit.cmi matitaEngine.cmi matitac.cmx: matitaclean.cmx matitaMisc.cmx matitaInit.cmx matitaEngine.cmx -matitaEngine.cmo: matitaEngine.cmi -matitaEngine.cmx: matitaEngine.cmi +matitadaemon.cmo: matitaInit.cmi matitaGtkMisc.cmi matitaEngine.cmi +matitadaemon.cmx: matitaInit.cmx matitaGtkMisc.cmx matitaEngine.cmx +matitaEngine.cmo: applyTransformation.cmi matitaEngine.cmi +matitaEngine.cmx: applyTransformation.cmx matitaEngine.cmi matitaExcPp.cmo: matitaEngine.cmi matitaExcPp.cmi matitaExcPp.cmx: matitaEngine.cmx matitaExcPp.cmi matitaGeneratedGui.cmo: @@ -23,33 +25,33 @@ matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmo buildTimeConf.cmo \ matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \ matitaGtkMisc.cmi matitaGui.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ - matitaMathView.cmi matitaGtkMisc.cmi matitaGeneratedGui.cmo \ - matitaExcPp.cmi buildTimeConf.cmo matitaGui.cmi + matitaMathView.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi \ + matitaGeneratedGui.cmo matitaExcPp.cmi buildTimeConf.cmo matitaGui.cmi matitaGui.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ - matitaMathView.cmx matitaGtkMisc.cmx matitaGeneratedGui.cmx \ - matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi + matitaMathView.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx \ + matitaGeneratedGui.cmx matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi matitaInit.cmo: matitaExcPp.cmi buildTimeConf.cmo matitaInit.cmi matitaInit.cmx: matitaExcPp.cmx buildTimeConf.cmx matitaInit.cmi matitaMathView.cmo: virtuals.cmi matitaTypes.cmi matitaMisc.cmi \ - matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi lablGraphviz.cmi \ - cicMathView.cmi buildTimeConf.cmo applyTransformation.cmi \ - matitaMathView.cmi + matitaGuiTypes.cmi matitaGtkMisc.cmi matitaGeneratedGui.cmo \ + matitaExcPp.cmi lablGraphviz.cmi cicMathView.cmi buildTimeConf.cmo \ + applyTransformation.cmi matitaMathView.cmi matitaMathView.cmx: virtuals.cmx matitaTypes.cmx matitaMisc.cmx \ - matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx lablGraphviz.cmx \ - cicMathView.cmx buildTimeConf.cmx applyTransformation.cmx \ - matitaMathView.cmi + matitaGuiTypes.cmi matitaGtkMisc.cmx matitaGeneratedGui.cmx \ + matitaExcPp.cmx lablGraphviz.cmx cicMathView.cmx buildTimeConf.cmx \ + applyTransformation.cmx matitaMathView.cmi matitaMisc.cmo: matitaGuiTypes.cmi buildTimeConf.cmo matitaMisc.cmi matitaMisc.cmx: matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi matita.cmo: predefined_virtuals.cmi matitaScript.cmi matitaInit.cmi \ - matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmo + matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmo applyTransformation.cmi matita.cmx: predefined_virtuals.cmx matitaScript.cmx matitaInit.cmx \ - matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx -matitaScript.cmo: virtuals.cmi matitaTypes.cmi matitaMisc.cmi \ - matitaMathView.cmi matitaGtkMisc.cmi matitaEngine.cmi cicMathView.cmi \ - buildTimeConf.cmo matitaScript.cmi -matitaScript.cmx: virtuals.cmx matitaTypes.cmx matitaMisc.cmx \ - matitaMathView.cmx matitaGtkMisc.cmx matitaEngine.cmx cicMathView.cmx \ - buildTimeConf.cmx matitaScript.cmi + matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx applyTransformation.cmx +matitaScript.cmo: virtuals.cmi matitaTypes.cmi matitaScriptLexer.cmi \ + matitaMisc.cmi matitaMathView.cmi matitaGtkMisc.cmi matitaEngine.cmi \ + cicMathView.cmi buildTimeConf.cmo matitaScript.cmi +matitaScript.cmx: virtuals.cmx matitaTypes.cmx matitaScriptLexer.cmx \ + matitaMisc.cmx matitaMathView.cmx matitaGtkMisc.cmx matitaEngine.cmx \ + cicMathView.cmx buildTimeConf.cmx matitaScript.cmi matitaTypes.cmo: matitaTypes.cmi matitaTypes.cmx: matitaTypes.cmi predefined_virtuals.cmo: virtuals.cmi predefined_virtuals.cmi @@ -60,15 +62,15 @@ applyTransformation.cmi: cicMathView.cmi: matitaGuiTypes.cmi applyTransformation.cmi lablGraphviz.cmi: matitaclean.cmi: -matitaEngine.cmi: +matitaEngine.cmi: applyTransformation.cmi matitaExcPp.cmi: matitaGtkMisc.cmi: matitaGeneratedGui.cmo matitaGui.cmi: matitaGuiTypes.cmi -matitaGuiTypes.cmi: matitaTypes.cmi matitaGeneratedGui.cmo \ - applyTransformation.cmi +matitaGuiTypes.cmi: matitaGeneratedGui.cmo applyTransformation.cmi matitaInit.cmi: matitaMathView.cmi: matitaTypes.cmi matitaGuiTypes.cmi matitaMisc.cmi: matitaGuiTypes.cmi +matitaScriptLexer.cmi: matitaScript.cmi: matitaTypes.cmi: predefined_virtuals.cmi: diff --git a/matitaB/matita/matitaScriptLexer.ml b/matitaB/matita/matitaScriptLexer.ml new file mode 100644 index 000000000..a7ce7142f --- /dev/null +++ b/matitaB/matita/matitaScriptLexer.ml @@ -0,0 +1,344 @@ +(* 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 11231 2011-03-30 11:52:27Z ricciott $ *) + +open Printf + +exception Error of int * int * string + +module StringSet = Set.Make(String) + +(* Lexer *) +let regexp number = xml_digit+ +let regexp utf8_blank = " " | "\r\n" | "\n" | "\t" | [160] (* this is a nbsp *) +let regexp percentage = + ('-' | "") [ '0' - '9' ] + '%' +let regexp floatwithunit = + ('-' | "") [ '0' - '9' ] + ["."] [ '0' - '9' ] + ([ 'a' - 'z' ] + | "" ) +let regexp color = "#" [ '0' - '9' 'a' - 'f' 'A' - 'F' ] [ '0' - '9' 'a' - 'f' +'A' - 'F' ] [ '0' - '9' 'a' - 'f' 'A' - 'F' ] [ '0' - '9' 'a' - 'f' 'A' - 'F' ] +[ '0' - '9' 'a' - 'f' 'A' - 'F' ] [ '0' - '9' 'a' - 'f' 'A' - 'F' ] + + (* ZACK: breaks unicode's binder followed by an ascii letter without blank *) +(* let regexp ident_letter = xml_letter *) + +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 we_proved = "we" utf8_blank+ "proved" +let regexp we_have = "we" utf8_blank+ "have" +let regexp let_rec = "let" utf8_blank+ "rec" +let regexp let_corec = "let" utf8_blank+ "corec" +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 uri_step = [ 'a' - 'z' 'A' - 'Z' '0' - '9' '_' '-' ''' ]+ + +let regexp uri = + ("cic:/" | "theory:/") (* schema *) +(* ident ('/' ident)* |+ path +| *) + uri_step ('/' uri_step)* (* path *) + ('.' ident)+ (* ext *) +(* ("#xpointer(" number ('/' number)+ ")")? (* xpointer *) *) + ("(" number (',' number)* ")")? (* reference spec *) + +let regexp qstring = '"' [^ '"']* '"' +let regexp hreftag = "<" [ 'A' 'a' ] +let regexp href = "href=\"" uri "\"" +let regexp hreftitle = "title=" qstring +let regexp hrefclose = "" + +let regexp tex_token = '\\' ident + +let regexp delim_begin = "\\[" +let regexp delim_end = "\\]" + +let regexp qkeyword = "'" ( ident | pident ) "'" + +let regexp implicit = '?' +let regexp placeholder = '%' +let regexp meta = implicit number + +let regexp csymbol = '\'' ident + +let regexp begin_group = "@{" | "${" +let regexp end_group = '}' +let regexp wildcard = "$_" +let regexp ast_ident = "@" ident +let regexp ast_csymbol = "@" csymbol +let regexp meta_ident = "$" ident +let regexp meta_anonymous = "$_" + +let regexp begincom = "(*" +let regexp endcom = "*)" +(* let regexp comment_char = [^'*'] | '*'[^')'] +let regexp note = "|+" ([^'*'] | "**") comment_char* "+|" *) + +let level1_layouts = + [ "sub"; "sup"; + "below"; "above"; + "over"; "atop"; "frac"; + "sqrt"; "root"; "mstyle" ; "mpadded"; "maction" + + ] + +let level1_keywords = + [ "hbox"; "hvbox"; "hovbox"; "vbox"; + "break"; + "list0"; "list1"; "sep"; + "opt"; + "term"; "ident"; "number"; + ] @ level1_layouts + +let level2_meta_keywords = + [ "if"; "then"; "elCicNotationParser.se"; + "fold"; "left"; "right"; "rec"; + "fail"; + "default"; + "anonymous"; "ident"; "number"; "term"; "fresh" + ] + + (* (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>); ("=>", <:unicode>); + (":=", <:unicode>); + ] + +let regexp nreference = + "cic:/" (* schema *) + uri_step ('/' uri_step)* (* path *) + '.' + ( "dec" + | "def" "(" number ")" + | "fix" "(" number "," number "," number ")" + | "cfx" "(" number ")" + | "ind" "(" number "," number "," number ")" + | "con" "(" number "," number "," number ")") (* ext + reference *) + +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 loc_of_buf lexbuf = + HExtlib.floc_of_loc (Ulexing.loc lexbuf) + +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 + +let return_lexeme lexbuf name = return lexbuf (name, Ulexing.utf8_lexeme lexbuf) + +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; + 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 rec level2_pattern_token_group counter buffer = + lexer + | end_group -> + if (counter > 0) then + Buffer.add_string buffer (Ulexing.utf8_lexeme lexbuf) ; + snd (Ulexing.loc lexbuf) + | begin_group -> + Buffer.add_string buffer (Ulexing.utf8_lexeme lexbuf) ; + ignore (level2_pattern_token_group (counter + 1) buffer lexbuf) ; + level2_pattern_token_group counter buffer lexbuf + | _ -> + Buffer.add_string buffer (Ulexing.utf8_lexeme lexbuf) ; + level2_pattern_token_group counter buffer lexbuf + +let read_unparsed_group token_name lexbuf = + let buffer = Buffer.create 16 in + let begin_cnum, _ = Ulexing.loc lexbuf in + let end_cnum = level2_pattern_token_group 0 buffer lexbuf in + return_with_loc (token_name, Buffer.contents buffer) begin_cnum end_cnum + +let handle_keywords lexbuf k name = + let s = Ulexing.utf8_lexeme lexbuf in + if k s then + return lexbuf ("", s) + else + return lexbuf (name, s) +;; + +let rec level2_meta_token = + lexer + | utf8_blank+ -> level2_meta_token lexbuf + | hreftag -> return lexbuf ("ATAG","") + | hrefclose -> return lexbuf ("ATAGEND","") + | ident -> + handle_keywords lexbuf (fun x -> List.mem x level2_meta_keywords) "IDENT" + | variable_ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf) + | pident -> + handle_keywords lexbuf (fun x -> List.mem x level2_meta_keywords) "PIDENT" + | "@{" -> read_unparsed_group "UNPARSED_AST" lexbuf + | ast_ident -> + return lexbuf ("UNPARSED_AST", + remove_left_quote (Ulexing.utf8_lexeme lexbuf)) + | ast_csymbol -> + return lexbuf ("UNPARSED_AST", + remove_left_quote (Ulexing.utf8_lexeme lexbuf)) + | eof -> return_eoi lexbuf + + + (** @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_eoi lexbuf + | _ -> (* not a ligature, rollback and try default lexer *) + Ulexing.rollback lexbuf; + k lexbuf + + +let so_pp = function +| None -> "()" +| Some s -> s +;; + +(* let update_table loc desc href loctable = + if desc <> None || href <> None + then + (let s,e = HExtlib.loc_of_floc loc in + prerr_endline (Printf.sprintf "*** [%d,%d] \"%s\",\"%s\"" + s e (so_pp href) (so_pp desc)); + CicNotationLexer.LocalizeEnv.add loc (href,desc) loctable) + else loctable +;; *) + +let get_hot_spots = + + (* k = lexing continuation *) + let rec aux nesting k = + lexer + | begincom -> aux (nesting+1) k lexbuf + | endcom -> aux (max 0 (nesting-1)) k lexbuf + | eof -> [] + | _ -> if nesting > 0 + then aux nesting k lexbuf + else (Ulexing.rollback lexbuf; + k lexbuf) + and aux_basic loc1 desc href = + lexer + | hreftag -> aux 0 (aux_in_tag (Ulexing.loc lexbuf) None None) lexbuf + | hrefclose -> + (try + let loc1 = HExtlib.floc_of_loc (HExtlib.unopt loc1) in + let loc2 = HExtlib.floc_of_loc (Ulexing.loc lexbuf) in + (loc1,loc2,href,desc) :: aux 0 (aux_basic None None None) lexbuf + with Failure _ -> aux 0 (aux_basic None None None) lexbuf) + | eof -> [] + | _ -> aux 0 (aux_basic loc1 desc href) lexbuf + and aux_in_tag loc1 desc href = lexer + | utf8_blank+ -> aux 0 (aux_in_tag loc1 desc href) lexbuf + | href -> + aux 0 (aux_in_tag loc1 desc (Some (Ulexing.utf8_sub_lexeme + lexbuf 6 (Ulexing.lexeme_length lexbuf - 7)))) + lexbuf + | hreftitle -> + aux 0 (aux_in_tag loc1 (Some (Ulexing.utf8_sub_lexeme lexbuf 7 + (Ulexing.lexeme_length lexbuf - 8))) href) + lexbuf + | ">" -> + let merge (a,b) (c,d) = (a,d) in + aux 0 + (aux_basic (Some (merge loc1 (Ulexing.loc lexbuf))) desc href) lexbuf + | _ -> aux 0 (aux_basic None None None) lexbuf + in aux 0 (aux_basic None None None) + +let get_hot_spots s = get_hot_spots (Ulexing.from_utf8_string s) diff --git a/matitaB/matita/matitaScriptLexer.mli b/matitaB/matita/matitaScriptLexer.mli new file mode 100644 index 000000000..29980c6db --- /dev/null +++ b/matitaB/matita/matitaScriptLexer.mli @@ -0,0 +1,34 @@ +(* 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/ + *) + + (** begin of error offset (counted in unicode codepoint) + * end of error offset (counted as above) + * error message *) +exception Error of int * int * string + +val get_hot_spots : string -> + (Stdpp.location * Stdpp.location * string option * string option) list + + diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml new file mode 100644 index 000000000..5c58db371 --- /dev/null +++ b/matitaB/matita/matitadaemon.ml @@ -0,0 +1,203 @@ +open Printf;; +open Http_types;; + +(*** from matitaScript.ml ***) +(* let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$" *) + +let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script *) + statement += + let ast,unparsed_text = + match statement with + | `Raw text -> + (* if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; *) + let strm = + GrafiteParser.parsable_statement status + (Ulexing.from_utf8_string text) in + let ast = MatitaEngine.get_ast status include_paths strm in + ast, text + | `Ast (st, text) -> st, text + in + let floc = match ast with + | GrafiteAst.Executable (loc, _) + | GrafiteAst.Comment (loc, _) -> loc in + + let _,lend = HExtlib.loc_of_floc floc in + let parsed_text, parsed_text_len = + MatitaGtkMisc.utf8_parsed_text unparsed_text (HExtlib.floc_of_loc (0,lend)) in + + let status = + MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:false status ("",0,ast) + in + (status, parsed_text),"",(*parsed_text_len*) Glib.Utf8.length parsed_text + + +let status = ref (new MatitaEngine.status "cic:/matita");; + +let include_paths = ["/home/barolo/matitaB/matita/lib"];; + +let advance text (* (?bos=false) *) = + (* if bos then LibraryClean.clean_baseuris [self#buri_of_current_file]; + (* HLog.debug ("evaluating: " ^ first_line s ^ " ...");*) + let time1 = Unix.gettimeofday () in + let entries, newtext, parsed_len = *) + let (st,_),_,parsed_len = + (* try *) + eval_statement include_paths (*buffer*) !status (`Raw text) + (* with End_of_file -> raise Margin *) + in + status := st; + let _,_,metasenv,subst,_ = !status#obj in + let txt = List.fold_left + (fun acc (nmeta,_ as meta) -> + let txt0 = Netencoding.Html.encode ~in_enc:`Enc_utf8 () + (snd (ApplyTransformation.ntxt_of_cic_sequent + ~metasenv ~subst ~map_unicode_to_tex:false 80 !status meta)) in + ("Goal ?" ^ (string_of_int nmeta) ^ "\n" ^ txt0)::acc) + [] metasenv + in + let txt = String.concat "\n\n" txt in + parsed_len, txt + (*in + let time2 = Unix.gettimeofday () in + HLog.debug ("... done in " ^ string_of_float (time2 -. time1) ^ "s"); + let new_statuses, new_statements = + let statuses, texts = List.split entries in + statuses, texts + in + history <- new_statuses @ history; + statements <- new_statements @ statements; + let start = buffer#get_iter_at_mark (`MARK locked_mark) in + let new_text = String.concat "" (List.rev new_statements) in + if statement <> None then + buffer#insert ~iter:start new_text + else begin + let parsed_text = String.sub s 0 parsed_len in + if new_text <> parsed_text then begin + let stop = start#copy#forward_chars (Glib.Utf8.length parsed_text) in + buffer#delete ~start ~stop; + buffer#insert ~iter:start new_text; + end; + end; + self#moveMark (Glib.Utf8.length new_text); + buffer#insert ~iter:(buffer#get_iter_at_mark (`MARK locked_mark)) newtext*) +;; + +let read_file fname = + let chan = open_in fname in + let lines = ref [] in + (try + while true do + lines := input_line chan :: !lines + done; + with End_of_file -> close_in chan); + String.concat "\r\n" (List.rev !lines) +;; + +let load_index outchan = + let s = read_file "index.html" in + Http_daemon.respond ~headers:["Content-Type", "text/html"] ~code:(`Code 200) ~body:s outchan +;; + +let call_service outchan = + try + (ignore(MatitaEngine.assert_ng + ~include_paths:["/home/barolo/matitaB/matita/lib"] (* ~outch:outchan *) + "/home/barolo/matitaB/matita/lib/basics/pts.ma"); + prerr_endline "fatto"; + let s = read_file "/home/barolo/matitaB/matita/lib/basics/pts.ma.mad" + in + Http_daemon.respond ~headers:["Content-Type", "text/html"] ~code:(`Code 200) ~body:s outchan + ) + with + e -> Http_daemon.respond ~code:(`Code 500) outchan +;; + +let callback req outchan = + let str = + (sprintf "request path = %s\n" req#path) ^ + (sprintf "request GET params = %s\n" + (String.concat ";" + (List.map (fun (h,v) -> String.concat "=" [h;v]) req#params_GET))) ^ + (sprintf "request POST params = %s\n" + (String.concat ";" + (List.map (fun (h,v) -> String.concat "=" [h;v]) req#params_POST))) ^ + (sprintf "request ALL params = %s\n" + (String.concat ";" + (List.map (fun (h,v) -> String.concat "=" [h;v]) req#params))) ^ + (sprintf "cookies = %s\n" + (match req#cookies with + | None -> + "NO COOKIES " + ^ (if req#hasHeader ~name:"cookie" + then "('Cookie:' header was '" ^ req#header ~name:"cookie" ^ "')" + else "(No 'Cookie:' header received)") + | Some cookies -> + (String.concat ";" + (List.map (fun (n,v) -> String.concat "=" [n;v]) cookies)))) ^ + (sprintf "request BODY = '%s'\n\n" req#body) + in + (* Http_daemon.respond ~code:(`Code 200) ~body: str outchan *) + + prerr_endline str; + + match req#path with + | "/" -> load_index outchan + | "/matita" -> call_service outchan + | "/open" -> + prerr_endline "getting 'file' argument"; + let filename = List.assoc "file" req#params_GET in + prerr_endline ("reading file " ^ filename); + let body = read_file filename in + let _,baseuri,_,_ = + Librarian.baseuri_of_script ~include_paths:[] filename + in + status := (!status)#set_baseuri baseuri; + Http_daemon.respond ~code:(`Code 200) ~body outchan + | "/advance" -> + let script = req#body in + prerr_endline ("body length = " ^ (string_of_int (String.length script))); + let (parsed_len,txt), res, code = + try advance script, "OK", `Code 200 + with + | HExtlib.Localized(_,e) + | e -> + (prerr_endline ("exception: " ^ Printexc.to_string e); + (try + NTacStatus.pp_tac_status !status + with e -> prerr_endline ("inner exception: " ^ + Printexc.to_string e)); + prerr_endline "end status"; + let _,_,metasenv,subst,_ = !status#obj in + let txt = List.fold_left + (fun acc (nmeta,_ as meta) -> + let txt0 = Netencoding.Html.encode ~in_enc:`Enc_utf8 () + (snd (ApplyTransformation.ntxt_of_cic_sequent + ~metasenv ~subst ~map_unicode_to_tex:false 80 !status meta)) in + ("Goal ?" ^ (string_of_int nmeta) ^ "\n" ^ txt0)::acc) + [] metasenv + in + let txt = String.concat "\n\n" txt in + (0,txt), Printexc.to_string e, `Code 500) + in + let txt = Netencoding.Url.encode ~plus:false txt in + let body = (string_of_int parsed_len) ^ "#" ^ txt in + Http_daemon.respond ~code ~body outchan + | url -> Http_daemon.respond_not_found ~url outchan + +;; + + + +let spec = + { Http_daemon.default_spec with + callback = callback; + port = 9999; + mode = `Single; + } +;; + +let _ = + MatitaInit.initialize_all (); + Http_daemon.main spec +;; -- 2.39.2