let use_fresh_num_instances = false
open Printf
+
open DisambiguateTypes
exception Parse_error of Token.flocation * string
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
| 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
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 =
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))
(**/**)
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} *)
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 *)
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
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
+
(** @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
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
+
| "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\e[01;31m%s\e[00m%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\e[01;31m%s\e[00m%s\n" before error after;
+ prerr_endline (sprintf "at character %d-%d: %s" x y msg)
+ done
+ with End_of_file ->
+ close_in ic
projects / helm.git / commitdiff