X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=8eca106304e96def0c883fa11885889751abcfcd;hp=f0de0b521b888593faaedf5468c12f0f9d9f715b;hb=7a72e5c5129c814e567f03e14d752eff4086fb52;hpb=e89486cad653803954662a5e543537acd49a866f 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