From: Stefano Zacchiroli Date: Tue, 18 Jan 2005 18:17:33 +0000 (+0000) Subject: added script support X-Git-Tag: V_0_1_0~129 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=18ad62cacbbb08decd4332b0bab449e640114fd7;p=helm.git added script support --- diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 3a5f76b67..49b08a7c5 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -36,6 +36,7 @@ let debug_print s = let use_fresh_num_instances = false open Printf + open DisambiguateTypes exception Parse_error of Token.flocation * string @@ -59,11 +60,12 @@ let tactic = Grammar.Entry.create grammar "tactic" let tactical = Grammar.Entry.create grammar "tactical" let tactical0 = Grammar.Entry.create grammar "tactical0" let command = Grammar.Entry.create grammar "command" +let script = Grammar.Entry.create grammar "script" let return_term loc term = CicAst.AttributedTerm (`Loc loc, term) let return_tactic loc tactic = TacticAst.LocatedTactic (loc, tactic) let return_tactical loc tactical = TacticAst.LocatedTactical (loc, tactical) -let return_command loc cmd = cmd +let return_command loc cmd = cmd (* TODO ZACK FIXME uhm ... why we drop loc? *) let fail floc msg = let (x, y) = CicAst.loc_of_floc floc in @@ -78,7 +80,7 @@ let int_opt = function | Some lexeme -> Some (int_of_string lexeme) EXTEND - GLOBAL: term term0 tactic tactical tactical0 command; + GLOBAL: term term0 tactic tactical tactical0 command script; int: [ [ num = NUM -> try @@ -421,6 +423,12 @@ EXTEND return_command loc (TacticAst.Check t) ] ]; + script_entry: [ + [ cmd = tactical0 -> Command cmd + | s = COMMENT -> Comment (loc, s) + ] + ]; + script: [ [ entries = LIST0 script_entry; EOI -> (loc, entries) ] ]; END let exc_located_wrapper f = @@ -438,6 +446,8 @@ let parse_tactic stream = exc_located_wrapper (fun () -> (Grammar.Entry.parse tactic stream)) let parse_tactical stream = exc_located_wrapper (fun () -> (Grammar.Entry.parse tactical0 stream)) +let parse_script stream = + exc_located_wrapper (fun () -> (Grammar.Entry.parse script stream)) (**/**) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli index 9ed3bdefc..659bb2aa5 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli @@ -30,6 +30,7 @@ exception Parse_error of Token.flocation * string val parse_term: char Stream.t -> DisambiguateTypes.term val parse_tactic: char Stream.t -> DisambiguateTypes.tactic val parse_tactical: char Stream.t -> DisambiguateTypes.tactical +val parse_script: char Stream.t -> DisambiguateTypes.script (** {2 Grammar extensions} *) diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml index 18c78a2e8..292d78e4b 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml @@ -26,6 +26,8 @@ type term = CicAst.term type tactic = (term, string) TacticAst.tactic type tactical = (term, string) TacticAst.tactical +type script_entry = Command of tactical | Comment of CicAst.location * string +type script = CicAst.location * script_entry list type domain_item = | Id of string (* literal *) @@ -50,14 +52,15 @@ and environment = codomain_item Environment.t module type Callbacks = sig - val interactive_user_uri_choice : + val interactive_user_uri_choice: selection_mode:[`SINGLE | `MULTIPLE] -> ?ok:string -> ?enable_button_for_non_vars:bool -> title:string -> msg:string -> id:string -> string list -> string list - val interactive_interpretation_choice : + val interactive_interpretation_choice: (string * string) list list -> int list - val input_or_locate_uri : title:string -> ?id:string -> unit -> UriManager.uri + val input_or_locate_uri: + title:string -> ?id:string -> unit -> UriManager.uri end let string_of_domain_item = function @@ -67,13 +70,6 @@ let string_of_domain_item = function let string_of_domain dom = String.concat "; " (List.map string_of_domain_item dom) -(* -let string_of_domain dom = - let buf = Buffer.create 1024 in - Domain.iter - (fun item -> Buffer.add_string buf (string_of_domain_item item ^ "; ")) - dom; - Buffer.contents buf -*) let empty_environment = Environment.empty + diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli index e88aa51bf..c21084966 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli @@ -52,7 +52,8 @@ module type Callbacks = (** @param title gtk window title for user prompting * @param id unbound identifier which originated this callback invocation *) - val input_or_locate_uri : title:string -> ?id:string -> unit -> UriManager.uri + val input_or_locate_uri: + title:string -> ?id:string -> unit -> UriManager.uri end val string_of_domain_item: domain_item -> string @@ -64,4 +65,10 @@ type term = CicAst.term type tactic = (term, string) TacticAst.tactic type tactical = (term, string) TacticAst.tactical +type script_entry = + | Command of tactical + | Comment of CicAst.location * string +type script = CicAst.location * script_entry list + val empty_environment: environment + diff --git a/helm/ocaml/cic_disambiguation/test_parser.ml b/helm/ocaml/cic_disambiguation/test_parser.ml index 51a0d911f..b7cace0cb 100644 --- a/helm/ocaml/cic_disambiguation/test_parser.ml +++ b/helm/ocaml/cic_disambiguation/test_parser.ml @@ -34,41 +34,53 @@ let mode = | "term" -> prerr_endline "Term"; `Term | "tactic" -> prerr_endline "Tactic"; `Tactic | "tactical" -> prerr_endline "Tactical"; `Tactical + | "script" -> prerr_endline "Script"; `Script | _ -> prerr_endline "What???????"; exit 1 with Invalid_argument _ -> prerr_endline "Term"; `Term let _ = - let ic = stdin in - try - while true do - let line = input_line ic in - let istream = Stream.of_string line in - try - (match mode with - | `Term -> - let term = CicTextualParser2.parse_term istream in - print_endline (BoxPp.pp_term term) - | `Tactic -> - let tac = CicTextualParser2.parse_tactic istream in - print_endline (TacticAstPp.pp_tactic tac) - | `Tactical -> - let tac = CicTextualParser2.parse_tactical istream in - print_endline (pp_tactical tac) - | `Alias -> - let env = CicTextualParser2.EnvironmentP3.of_string line in - print_endline (CicTextualParser2.EnvironmentP3.to_string env)); - flush stdout - with - | CicTextualParser2.Parse_error (floc, msg) -> - let (x, y) = CicAst.loc_of_floc floc in - let before = String.sub line 0 x in - let error = String.sub line x (y - x) in - let after = String.sub line y (String.length line - y) in - eprintf "%s%s%s\n" before error after; - prerr_endline (sprintf "at character %d-%d: %s" x y msg) - done - with End_of_file -> - close_in ic + if mode = `Script then + let ic = open_in Sys.argv.(2) in + let istream = Stream.of_channel ic in + let (loc, script) = CicTextualParser2.parse_script istream in + List.iter + (function + | DisambiguateTypes.Command cmd -> print_endline (pp_tactical cmd) + | DisambiguateTypes.Comment (loc, s) -> print_endline s) + script + else + let ic = stdin in + try + while true do + let line = input_line ic in + let istream = Stream.of_string line in + try + (match mode with + | `Term -> + let term = CicTextualParser2.parse_term istream in + print_endline (BoxPp.pp_term term) + | `Tactic -> + let tac = CicTextualParser2.parse_tactic istream in + print_endline (TacticAstPp.pp_tactic tac) + | `Tactical -> + let tac = CicTextualParser2.parse_tactical istream in + print_endline (pp_tactical tac) + | `Alias -> + let env = CicTextualParser2.EnvironmentP3.of_string line in + print_endline (CicTextualParser2.EnvironmentP3.to_string env) + | _ -> assert false); + flush stdout + with + | CicTextualParser2.Parse_error (floc, msg) -> + let (x, y) = CicAst.loc_of_floc floc in + let before = String.sub line 0 x in + let error = String.sub line x (y - x) in + let after = String.sub line y (String.length line - y) in + eprintf "%s%s%s\n" before error after; + prerr_endline (sprintf "at character %d-%d: %s" x y msg) + done + with End_of_file -> + close_in ic