From 7a72e5c5129c814e567f03e14d752eff4086fb52 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 30 Apr 2004 09:24:49 +0000 Subject: [PATCH] - moved command as sub-entries of tactical grammars (as per tactics) --- .../cic_disambiguation/cicTextualParser2.ml | 91 +++---------------- .../cic_disambiguation/cicTextualParser2.mli | 2 - .../cic_disambiguation/disambiguateTypes.ml | 4 +- .../cic_disambiguation/disambiguateTypes.mli | 4 +- helm/ocaml/cic_disambiguation/test_parser.ml | 82 +++++++---------- 5 files changed, 49 insertions(+), 134 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index f0de0b521..8eca10630 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -36,14 +36,10 @@ let debug_print s = let use_fresh_num_instances = false open Printf +open DisambiguateTypes exception Parse_error of string -type tactic = (CicAst.term, string) TacticAst.tactic -type tactical = (CicAst.term, string) TacticAst.tactic TacticAst.tactical -type command = CicAst.term CommandAst.command -type script = CicAst.term CommandAst.Script.script - let fresh_num_instance = let n = ref 0 in if use_fresh_num_instances then @@ -63,13 +59,11 @@ 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_script loc script = script let fail (x, y) msg = failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg) @@ -79,7 +73,7 @@ let name_of_string = function | s -> Cic.Name s EXTEND - GLOBAL: term term0 tactic tactical tactical0 command script; + GLOBAL: term term0 tactic tactical tactical0 command; int: [ [ num = NUM -> try @@ -335,6 +329,7 @@ EXTEND | [ IDENT "id" | IDENT "Id" ] -> return_tactical loc TacticAst.IdTac | PAREN "("; tac = tactical; PAREN ")" -> return_tactical loc tac | tac = tactic -> return_tactical loc (TacticAst.Tactic tac) + | cmd = command -> return_tactical loc (TacticAst.Command cmd) ] ]; theorem_flavour: [ (* all flavours but Goal *) @@ -343,73 +338,23 @@ EXTEND | [ IDENT "lemma" | IDENT "Lemma" ] -> `Lemma | [ IDENT "remark" | IDENT "Remark" ] -> `Remark | [ IDENT "theorem" | IDENT "Theorem" ] -> `Theorem -(* | [ IDENT "goal" | IDENT "Goal" ] -> `Goal *) - ] - ]; - theorem_cmd: [ - [ flavour = theorem_flavour; name = OPT IDENT; SYMBOL ":"; typ = term; - body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ]; - SYMBOL "." -> - (loc, flavour, name, typ, body) - | [ IDENT "goal" | IDENT "Goal" ]; typ = term; - body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ]; - SYMBOL "." -> - (loc, `Goal, None, typ, body) - ] - ]; - proof_cmd: [ [ [ IDENT "proof" | IDENT "Proof" ]; SYMBOL "." -> loc ] ]; - qed_cmd: [ - [ [ IDENT "qed" | IDENT "Qed" ]; SYMBOL "." -> (loc, None) - | [ IDENT "save" | IDENT "Save" ]; name = IDENT; SYMBOL "." -> - (loc, Some name) ] ]; command: [ - [ (loc', flavour, name, typ, body) = theorem_cmd -> - return_command loc (CommandAst.Theorem (loc', flavour, name, typ, body)) - | (loc') = proof_cmd -> return_command loc (CommandAst.Proof loc') - | (loc, name) = qed_cmd -> return_command loc (CommandAst.Qed (loc, name)) - ] - ]; - script_entry: [ - [ theorem = theorem_cmd; - proof = OPT [ - proof_cmd; tacticals = LIST1 tactical0; qed = qed_cmd -> - (tacticals, qed) - ] -> - let (loc', flavour, name', typ, body_verbatim) = theorem in - let name'' = - match proof with - | None | Some (_, (_, None)) -> None - | Some (_, (_, Some name)) -> Some name - in - let name = - match (name', name'') with - | Some name, None -> name - | None, Some name -> name - | None, None -> - Stdpp.raise_with_loc loc (Failure "theorem's name is missing") - | Some name', Some name'' when name' <> name'' -> - Stdpp.raise_with_loc loc (Failure (sprintf - "theorem's name mismatch: %s <> %s" name' name'')) - | Some name, _ -> name - in - let body = - match (body_verbatim, proof) with - | Some term, None -> CommandAst.Script.Verbatim (loc', term) - | None, Some (tacticals, (loc'', _)) -> - CommandAst.Script.Tactics (loc'', tacticals) - | Some _, Some _ -> - Stdpp.raise_with_loc loc (Failure (sprintf - "theorem %s has too many proofs" name)) - | None, None -> - Stdpp.raise_with_loc loc (Failure (sprintf - "theorem %s has no proof" name)) - in - return_script loc (CommandAst.Script.Theorem (flavour, name, typ, body)) + [ [ IDENT "proof" | IDENT "Proof" ] -> return_command loc TacticAst.Proof + | [ IDENT "quit" | IDENT "Quit" ] -> return_command loc TacticAst.Quit + | [ IDENT "qed" | IDENT "Qed" ] -> + return_command loc (TacticAst.Qed None) + | [ IDENT "save" | IDENT "Save" ]; name = IDENT -> + return_command loc (TacticAst.Qed (Some name)) + | flavour = theorem_flavour; name = OPT IDENT; SYMBOL ":"; typ = term; + body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> + return_command loc (TacticAst.Theorem (flavour, name, typ, body)) + | [ IDENT "goal" | IDENT "Goal" ]; typ = term; + body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> + return_command loc (TacticAst.Theorem (`Goal, None, typ, body)) ] ]; - script: [ [ entries = LIST0 script_entry; EOI -> entries ] ]; END let exc_located_wrapper f = @@ -425,17 +370,11 @@ let parse_tactic stream = exc_located_wrapper (lazy (Grammar.Entry.parse tactic stream)) let parse_tactical stream = exc_located_wrapper (lazy (Grammar.Entry.parse tactical0 stream)) -let parse_command stream = - exc_located_wrapper (lazy (Grammar.Entry.parse command stream)) -let parse_script stream = - exc_located_wrapper (lazy (Grammar.Entry.parse script stream)) (**/**) (** {2 Interface for gTopLevel} *) -open DisambiguateTypes - module EnvironmentP3 = struct type t = environment diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli index e6b1ff7e1..351d929e2 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli @@ -30,8 +30,6 @@ exception Parse_error of 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_command: char Stream.t -> DisambiguateTypes.command -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 358f2d49e..a5e0f96f8 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml @@ -25,9 +25,7 @@ type term = CicAst.term type tactic = (term, string) TacticAst.tactic -type tactical = (term, string) TacticAst.tactic TacticAst.tactical -type command = term CommandAst.command -type script = term CommandAst.Script.script +type tactical = (term, string) TacticAst.tactical type domain_item = | Id of string (* literal *) diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli index 2849a858c..ccde1a4e8 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli @@ -62,7 +62,5 @@ val string_of_domain: domain_item list -> string type term = CicAst.term type tactic = (term, string) TacticAst.tactic -type tactical = (term, string) TacticAst.tactic TacticAst.tactical -type command = term CommandAst.command -type script = term CommandAst.Script.script +type tactical = (term, string) TacticAst.tactical diff --git a/helm/ocaml/cic_disambiguation/test_parser.ml b/helm/ocaml/cic_disambiguation/test_parser.ml index dde969555..4ee8ec6ef 100644 --- a/helm/ocaml/cic_disambiguation/test_parser.ml +++ b/helm/ocaml/cic_disambiguation/test_parser.ml @@ -23,67 +23,49 @@ * http://helm.cs.unibo.it/ *) -let default_mode = `Term - -let mode = ref default_mode - -(* let pp_tactical = TacticAstPp.pp_tactical *) - let pp_tactical = TacticAst2Box.tacticalPp -let pp_command = CommandAst.pp_command -let pp_script = CommandAst.pp_script -let _ = +let mode = try match Sys.argv.(1) with - | "alias" -> mode := `Alias - | "term" -> mode := `Term - | "tactic" -> mode := `Tactic - | "tactical" -> mode := `Tactical - | "command" -> mode := `Command - | "script" -> mode := `Script + | "alias" -> prerr_endline "Alias"; `Alias + | "term" -> prerr_endline "Term"; `Term + | "tactic" -> prerr_endline "Tactic"; `Tactic + | "tactical" -> prerr_endline "Tactical"; `Tactical | _ -> prerr_endline "What???????"; exit 1 - with Invalid_argument _ -> () + with Invalid_argument _ -> prerr_endline "Term"; `Term let _ = let ic = stdin in try - if !mode = `Script then begin - let script = CicTextualParser2.parse_script (Stream.of_channel ic) in - print_endline (pp_script script) - end else - while true do - try - let line = input_line ic in - let istream = Stream.of_string line in - (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) - | `Command -> - let cmd = CicTextualParser2.parse_command istream in - print_endline (pp_command cmd) - | `Script -> assert false (* catched above *) - | `Alias -> - let env = CicTextualParser2.EnvironmentP3.of_string line in - print_endline (CicTextualParser2.EnvironmentP3.to_string env)); - flush stdout - with - | CicTextualParser2.Parse_error msg -> prerr_endline msg - (* - | Stdpp.Exc_located ((p_start, p_end), exn) -> - prerr_endline (Printf.sprintf "Exception at character %d-%d: %s" - p_start p_end (Printexc.to_string exn)) - *) - done + while true do + try + let line = input_line ic in + let istream = Stream.of_string line in + (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 msg -> prerr_endline msg +(* + | Stdpp.Exc_located ((p_start, p_end), exn) -> + prerr_endline (Printf.sprintf "Exception at character %d-%d: %s" + p_start p_end (Printexc.to_string exn)) +*) + done with End_of_file -> close_in ic -- 2.39.2