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
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)
| s -> Cic.Name s
EXTEND
- GLOBAL: term term0 tactic tactical tactical0 command script;
+ GLOBAL: term term0 tactic tactical tactical0 command;
int: [
[ num = NUM ->
try
| [ 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 *)
| [ 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<def>> (* ≝ *); body = term -> body ];
- SYMBOL "." ->
- (loc, flavour, name, typ, body)
- | [ IDENT "goal" | IDENT "Goal" ]; typ = term;
- body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); 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<def>> (* ≝ *); body = term -> body ] ->
+ return_command loc (TacticAst.Theorem (flavour, name, typ, body))
+ | [ IDENT "goal" | IDENT "Goal" ]; typ = term;
+ body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); 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 =
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
* 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
projects / helm.git / commitdiff