prerr_endline "</NEW_TEXTUAL_PARSER>"
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
-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
+ (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
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
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 *)
return_term loc
(CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
]
+ | "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 = [
];
tactical0: [ [ t = tactical; SYMBOL "." -> t ] ];
tactical:
- [ "sequence" LEFTA
+ [ "command" NONA
+ [ cmd = command -> return_tactical loc (TacticAst.Command cmd) ]
+ | "sequence" LEFTA
[ tactics = LIST1 NEXT SEP SYMBOL ";" ->
return_tactical loc (TacticAst.Seq tactics)
]
| [ 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 "abort" | IDENT "Abort" ] -> return_command loc TacticAst.Abort
+ | [ 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
projects / helm.git / blobdiff