X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=8eca106304e96def0c883fa11885889751abcfcd;hb=7a72e5c5129c814e567f03e14d752eff4086fb52;hp=cd1de44879c723caadc256fd30cbdc8fc72f4e9d;hpb=c0dd3e6a0100462e79d40e4dca2df7d9b89afe76;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index cd1de4487..8eca10630 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -31,10 +31,22 @@ let debug_print s = prerr_endline "" end + (** if set to true each number will have a different insance number and can + * thus be interpreted differently than others *) +let use_fresh_num_instances = false + open Printf +open DisambiguateTypes exception Parse_error of string +let fresh_num_instance = + let n = ref 0 in + if use_fresh_num_instances then + (fun () -> incr n; !n) + else + (fun () -> 0) + let choice_of_uri (uri: string) = let cic = HelmLibraryObjects.term_of_uri (UriManager.uri_of_string uri) in (uri, (fun _ _ _ -> cic)) @@ -46,10 +58,12 @@ 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 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 fail (x, y) msg = failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg) @@ -59,7 +73,7 @@ let name_of_string = function | s -> Cic.Name s EXTEND - GLOBAL: term term0 tactic tactical tactical0; + GLOBAL: term term0 tactic tactical tactical0 command; int: [ [ num = NUM -> try @@ -103,9 +117,7 @@ EXTEND PAREN "]" -> substs ] -> - (match subst with - | Some l -> CicAst.Ident (s, l) - | None -> CicAst.Ident (s, [])) + CicAst.Ident (s, subst) ] ]; name: [ (* as substituted_name with no explicit substitution *) @@ -162,19 +174,23 @@ EXTEND return_term loc (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2)) ] - | "eq" LEFTA + | "logic_add" LEFTA [ (* nothing here by default *) ] + | "logic_mult" LEFTA [ (* nothing here by default *) ] + | "logic_inv" NONA [ (* nothing here by default *) ] + | "relop" LEFTA [ t1 = term; SYMBOL "="; t2 = term -> return_term loc (CicAst.Appl [CicAst.Symbol ("eq", 0); t1; t2]) ] | "add" LEFTA [ (* nothing here by default *) ] | "mult" LEFTA [ (* nothing here by default *) ] + | "power" LEFTA [ (* nothing here by default *) ] | "inv" NONA [ (* nothing here by default *) ] | "simple" NONA [ sort = sort -> CicAst.Sort sort | n = substituted_name -> return_term loc n | PAREN "("; head = term; args = LIST1 term; PAREN ")" -> return_term loc (CicAst.Appl (head :: args)) - | i = NUM -> return_term loc (CicAst.Num (i, 0)) + | i = NUM -> return_term loc (CicAst.Num (i, (fresh_num_instance ()))) | IMPLICIT -> return_term loc CicAst.Implicit | m = META; substs = [ @@ -200,10 +216,14 @@ EXTEND PAREN "]" -> return_term loc (CicAst.Case (t, indty_ident, outtyp, patterns)) + | PAREN "("; t1 = term; SYMBOL ":"; t2 = term; PAREN ")" -> + return_term loc (CicAst.Appl [CicAst.Symbol ("cast", 0); t1; t2]) | PAREN "("; t = term; PAREN ")" -> return_term loc t ] ]; - tactic_where: [ [ where = OPT [ "in"; ident = IDENT -> ident ] -> where ] ]; + tactic_where: [ + [ where = OPT [ IDENT "in"; ident = IDENT -> ident ] -> where ] + ]; tactic_term: [ [ t = term -> t ] ]; ident_list0: [ [ PAREN "["; idents = LIST0 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ] @@ -217,54 +237,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; - using = OPT [ IDENT "using"; using = tactic_term -> using ] -> + | [ 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 ";" -> @@ -276,51 +314,67 @@ 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) + | cmd = command -> return_tactical loc (TacticAst.Command cmd) ] ]; + 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 + ] + ]; + command: [ + [ [ 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)) + ] + ]; 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)) (**/**) (** {2 Interface for gTopLevel} *) -open DisambiguateTypes - module EnvironmentP3 = struct type t = environment @@ -388,3 +442,4 @@ module EnvironmentP3 = (Printexc.to_string exn))) end +(* vim:set encoding=utf8: *)