From ae25bae855f66b7ebc9926a80dc38e622f0cff38 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 26 Feb 2004 14:53:18 +0000 Subject: [PATCH] added support for commands and scripts --- .../cic_disambiguation/cicTextualLexer2.ml | 2 +- .../cic_disambiguation/cicTextualParser2.ml | 191 +++++++++++++----- .../cic_disambiguation/cicTextualParser2.mli | 17 +- helm/ocaml/cic_disambiguation/test_parser.ml | 65 +++--- 4 files changed, 196 insertions(+), 79 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml index 71574dbb1..22c911eaf 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml @@ -51,7 +51,7 @@ let regexp uri = let keywords = Hashtbl.create 17 let _ = List.iter (fun keyword -> Hashtbl.add keywords keyword ("", keyword)) - [ "Prop"; "Type"; "Set"; "let"; "rec"; "using"; "match"; "with" ] + [ "Prop"; "Type"; "Set"; "let"; "Let"; "rec"; "using"; "match"; "with" ] let error lexbuf msg = raise (Error (Ulexing.lexeme_start lexbuf, Ulexing.lexeme_end lexbuf, msg)) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 7c0dfc1c6..2474191fe 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -35,6 +35,11 @@ open Printf 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 choice_of_uri (uri: string) = let cic = HelmLibraryObjects.term_of_uri (UriManager.uri_of_string uri) in (uri, (fun _ _ _ -> cic)) @@ -46,10 +51,14 @@ let term0 = Grammar.Entry.create grammar "term0" 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) @@ -59,7 +68,7 @@ let name_of_string = function | s -> Cic.Name s EXTEND - GLOBAL: term term0 tactic tactical tactical0; + GLOBAL: term term0 tactic tactical tactical0 command script; int: [ [ num = NUM -> try @@ -219,54 +228,72 @@ EXTEND | "whd" -> `Whd ] ]; tactic: [ - [ IDENT "absurd" -> return_tactic loc TacticAst.Absurd - | IDENT "apply"; t = tactic_term -> return_tactic loc (TacticAst.Apply t) - | IDENT "assumption" -> return_tactic loc TacticAst.Assumption - | IDENT "change"; t1 = tactic_term; "with"; t2 = tactic_term; + [ [ IDENT "absurd" | IDENT "Absurd" ] -> return_tactic loc TacticAst.Absurd + | [ IDENT "apply" | IDENT "Apply" ]; + t = tactic_term -> return_tactic loc (TacticAst.Apply t) + | [ IDENT "assumption" | IDENT "Assumption" ] -> + return_tactic loc TacticAst.Assumption + | [ IDENT "change" | IDENT "Change" ]; + t1 = tactic_term; "with"; t2 = tactic_term; where = tactic_where -> return_tactic loc (TacticAst.Change (t1, t2, where)) (* TODO Change_pattern *) - | IDENT "contradiction" -> return_tactic loc TacticAst.Contradiction - | IDENT "cut"; t = tactic_term -> return_tactic loc (TacticAst.Cut t) - | IDENT "decompose"; principles = ident_list1; where = IDENT -> + | [ IDENT "contradiction" | IDENT "Contradiction" ] -> + return_tactic loc TacticAst.Contradiction + | [ IDENT "cut" | IDENT "Cut" ]; + t = tactic_term -> return_tactic loc (TacticAst.Cut t) + | [ IDENT "decompose" | IDENT "Decompose" ]; + principles = ident_list1; where = IDENT -> return_tactic loc (TacticAst.Decompose (where, principles)) - | IDENT "discriminate"; hyp = IDENT -> + | [ IDENT "discriminate" | IDENT "Discriminate" ]; + hyp = IDENT -> return_tactic loc (TacticAst.Discriminate hyp) - | IDENT "elim"; IDENT "type"; t = tactic_term -> + | [ IDENT "elim" | IDENT "Elim" ]; IDENT "type"; + t = tactic_term -> return_tactic loc (TacticAst.ElimType t) - | IDENT "elim"; t1 = tactic_term; + | [ IDENT "elim" | IDENT "Elim" ]; + t1 = tactic_term; using = OPT [ "using"; using = tactic_term -> using ] -> return_tactic loc (TacticAst.Elim (t1, using)) - | IDENT "exact"; t = tactic_term -> return_tactic loc (TacticAst.Exact t) - | IDENT "exists" -> return_tactic loc TacticAst.Exists - | IDENT "fold"; kind = reduction_kind; t = tactic_term -> + | [ IDENT "exact" | IDENT "Exact" ]; t = tactic_term -> + return_tactic loc (TacticAst.Exact t) + | [ IDENT "exists" | IDENT "Exists" ] -> + return_tactic loc TacticAst.Exists + | [ IDENT "fold" | IDENT "Fold" ]; + kind = reduction_kind; t = tactic_term -> return_tactic loc (TacticAst.Fold (kind, t)) - | IDENT "fourier" -> return_tactic loc TacticAst.Fourier - | IDENT "injection"; ident = IDENT -> + | [ IDENT "fourier" | IDENT "Fourier" ] -> + return_tactic loc TacticAst.Fourier + | [ IDENT "injection" | IDENT "Injection" ]; ident = IDENT -> return_tactic loc (TacticAst.Injection ident) - | IDENT "intros"; + | [ IDENT "intros" | IDENT "Intros" ]; num = OPT [ num = int -> num ]; idents = OPT ident_list0 -> let idents = match idents with None -> [] | Some idents -> idents in return_tactic loc (TacticAst.Intros (num, idents)) - | IDENT "left" -> return_tactic loc TacticAst.Left - | "let"; t = tactic_term; IDENT "in"; where = IDENT -> + | [ IDENT "left" | IDENT "Left" ] -> return_tactic loc TacticAst.Left + | [ "let" | "Let" ]; + t = tactic_term; IDENT "in"; where = IDENT -> return_tactic loc (TacticAst.LetIn (t, where)) (* TODO Reduce *) - | IDENT "reflexivity" -> return_tactic loc TacticAst.Reflexivity - | IDENT "replace"; t1 = tactic_term; "with"; t2 = tactic_term -> + | [ IDENT "reflexivity" | IDENT "Reflexivity" ] -> + return_tactic loc TacticAst.Reflexivity + | [ IDENT "replace" | IDENT "Replace" ]; + t1 = tactic_term; "with"; t2 = tactic_term -> return_tactic loc (TacticAst.Replace (t1, t2)) (* TODO Rewrite *) (* TODO Replace_pattern *) - | IDENT "right" -> return_tactic loc TacticAst.Right - | IDENT "ring" -> return_tactic loc TacticAst.Ring - | IDENT "split" -> return_tactic loc TacticAst.Split - | IDENT "symmetry" -> return_tactic loc TacticAst.Symmetry - | IDENT "transitivity"; t = tactic_term -> + | [ IDENT "right" | IDENT "Right" ] -> return_tactic loc TacticAst.Right + | [ IDENT "ring" | IDENT "Ring" ] -> return_tactic loc TacticAst.Ring + | [ IDENT "split" | IDENT "Split" ] -> return_tactic loc TacticAst.Split + | [ IDENT "symmetry" | IDENT "Symmetry" ] -> + return_tactic loc TacticAst.Symmetry + | [ IDENT "transitivity" | IDENT "Transitivity" ]; + t = tactic_term -> return_tactic loc (TacticAst.Transitivity t) ] ]; - tactical0 : [ [ t = tactical; SYMBOL "." -> t ] ]; + tactical0: [ [ t = tactical; SYMBOL "." -> t ] ]; tactical: [ "sequence" LEFTA [ tactics = LIST1 NEXT SEP SYMBOL ";" -> @@ -278,44 +305,115 @@ EXTEND return_tactical loc (TacticAst.Then (tac, tacs)) ] | "loops" RIGHTA - [ IDENT "do"; count = int; tac = tactical -> + [ [ IDENT "do" | IDENT "Do" ]; count = int; tac = tactical -> return_tactical loc (TacticAst.Do (count, tac)) - | IDENT "repeat"; tac = tactical -> + | [ IDENT "repeat" | IDENT "Repeat" ]; tac = tactical -> return_tactical loc (TacticAst.Repeat tac) ] | "simple" NONA - [ IDENT "tries"; + [ [ IDENT "tries" | IDENT "Tries" ]; PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" -> return_tactical loc (TacticAst.Tries tacs) - | IDENT "try"; tac = NEXT -> return_tactical loc (TacticAst.Try tac) - | IDENT "fail" -> return_tactical loc TacticAst.Fail - | IDENT "id" -> return_tactical loc TacticAst.IdTac + | [ IDENT "try" | IDENT "Try" ]; tac = NEXT -> + return_tactical loc (TacticAst.Try tac) + | [ IDENT "fail" | IDENT "Fail" ] -> return_tactical loc TacticAst.Fail + | [ 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) ] ]; + theorem_flavour: [ (* all flavours but Goal *) + [ [ IDENT "definition" | IDENT "Definition" ] -> `Definition + | [ IDENT "fact" | IDENT "Fact" ] -> `Fact + | [ 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)) + ] + ]; + script: [ [ entries = LIST0 script_entry; EOI -> entries ] ]; END -let parse_term stream = +let exc_located_wrapper f = try - Grammar.Entry.parse term0 stream + Lazy.force f with Stdpp.Exc_located ((x, y), exn) -> raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y (Printexc.to_string exn))) +let parse_term stream = + exc_located_wrapper (lazy (Grammar.Entry.parse term0 stream)) let parse_tactic stream = - try - Grammar.Entry.parse tactic stream - with Stdpp.Exc_located ((x, y), exn) -> - raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y - (Printexc.to_string exn))) - + exc_located_wrapper (lazy (Grammar.Entry.parse tactic stream)) let parse_tactical stream = - try - Grammar.Entry.parse tactical0 stream - with Stdpp.Exc_located ((x, y), exn) -> - raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y - (Printexc.to_string exn))) + 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)) (**/**) @@ -390,3 +488,4 @@ module EnvironmentP3 = (Printexc.to_string exn))) end +(* vim:set encoding=utf8: *) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli index a6f8dcce3..e867d3435 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli @@ -25,13 +25,20 @@ exception Parse_error of string +(** {3 type shortands} *) + +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 + (** {2 Parsing functions} *) -val parse_term: char Stream.t -> CicAst.term -val parse_tactic: char Stream.t -> (CicAst.term, string) TacticAst.tactic -val parse_tactical: - char Stream.t -> - (CicAst.term, string) TacticAst.tactic TacticAst.tactical +val parse_term: char Stream.t -> CicAst.term +val parse_tactic: char Stream.t -> tactic +val parse_tactical: char Stream.t -> tactical +val parse_command: char Stream.t -> command +val parse_script: char Stream.t -> script (** {2 Grammar extensions} *) diff --git a/helm/ocaml/cic_disambiguation/test_parser.ml b/helm/ocaml/cic_disambiguation/test_parser.ml index d6afddc67..dde969555 100644 --- a/helm/ocaml/cic_disambiguation/test_parser.ml +++ b/helm/ocaml/cic_disambiguation/test_parser.ml @@ -30,7 +30,8 @@ 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 _ = try @@ -39,6 +40,8 @@ let _ = | "term" -> mode := `Term | "tactic" -> mode := `Tactic | "tactical" -> mode := `Tactical + | "command" -> mode := `Command + | "script" -> mode := `Script | _ -> prerr_endline "What???????"; exit 1 @@ -47,32 +50,40 @@ let _ = let _ = let ic = stdin in try - 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 term = CicTextualParser2.parse_tactic istream in - print_endline (TacticAstPp.pp_tactic term) - | `Tactical -> - let term = CicTextualParser2.parse_tactical istream in - print_endline (pp_tactical term) - | `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 + 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 with End_of_file -> close_in ic -- 2.39.2