X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=49b08a7c5d6b46bb942c01899ecfdf1dde178b61;hb=18ad62cacbbb08decd4332b0bab449e640114fd7;hp=2474191fe4f0c9f866b40e8949f40e504e0fd91f;hpb=ae25bae855f66b7ebc9926a80dc38e622f0cff38;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 2474191fe..49b08a7c5 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -31,18 +31,26 @@ 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 -exception Parse_error of string +open DisambiguateTypes + +exception Parse_error of Token.flocation * 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 - (uri, (fun _ _ _ -> cic)) +let choice_of_uri uri = + let term = CicUtil.term_of_uri uri in + (uri, (fun _ _ _ -> term)) let grammar = Grammar.gcreate CicTextualLexer2.cic_lexer @@ -57,26 +65,27 @@ 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 return_command loc cmd = cmd (* TODO ZACK FIXME uhm ... why we drop loc? *) -let fail (x, y) msg = +let fail floc msg = + let (x, y) = CicAst.loc_of_floc floc in failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg) let name_of_string = function | "_" -> Cic.Anonymous | s -> Cic.Name s +let int_opt = function + | None -> None + | Some lexeme -> Some (int_of_string lexeme) + EXTEND GLOBAL: term term0 tactic tactical tactical0 command script; int: [ [ num = NUM -> try int_of_string num - with Failure _ -> - let (x, y) = loc in - raise (Parse_error (sprintf - "integer literal expected at characters %d-%d" x y)) + with Failure _ -> raise (Parse_error (loc, "integer literal expected")) ] ]; meta_subst: [ @@ -102,9 +111,9 @@ EXTEND ] ]; substituted_name: [ (* a subs.name is an explicit substitution subject *) - [ s = [ IDENT | SYMBOL ]; + [ s = IDENT; subst = OPT [ - SYMBOL "\subst"; (* to avoid catching frequent "a [1]" cases *) + SYMBOL "\\subst"; (* to avoid catching frequent "a [1]" cases *) PAREN "["; substs = LIST1 [ i = IDENT; SYMBOL <:unicode> (* ≔ *); t = term -> (i, t) @@ -112,9 +121,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 *) @@ -126,15 +133,13 @@ EXTEND (head, vars) ] ]; + constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ]; term0: [ [ t = term; EOI -> return_term loc t ] ]; term: [ "letin" NONA - (* actually "in" and "and" are _not_ keywords. Parsing works anyway - * since applications are required to be bound by parens *) [ "let"; var = typed_name; SYMBOL "="; (* SYMBOL <:unicode> (* ≝ *); *) - t1 = term; - IDENT "in"; t2 = term -> + t1 = term; "in"; t2 = term -> return_term loc (CicAst.LetIn (var, t1, t2)) | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; defs = LIST1 [ @@ -145,8 +150,8 @@ EXTEND SYMBOL "="; (* SYMBOL <:unicode> (* ≝ *); *) t1 = term -> (var, t1, (match index with None -> 0 | Some i -> i)) - ] SEP (IDENT "and"); - IDENT "in"; body = term -> + ] SEP "and"; + "in"; body = term -> return_term loc (CicAst.LetRec (ind_kind, defs, body)) ] | "binder" RIGHTA @@ -171,19 +176,29 @@ EXTEND 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 *) ] + | "apply" LEFTA + [ t1 = term; t2 = term -> + let rec aux = function + | CicAst.Appl (hd :: tl) -> aux hd @ tl + | term -> [term] + in + CicAst.Appl (aux t1 @ [t2]) + ] | "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 = [ @@ -209,11 +224,13 @@ 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 [ IDENT "in"; ident = IDENT -> ident ] -> where ] + [ where = OPT [ "in"; ident = IDENT -> ident ] -> where ] ]; tactic_term: [ [ t = term -> t ] ]; ident_list0: [ @@ -223,16 +240,18 @@ EXTEND [ PAREN "["; idents = LIST1 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ] ]; reduction_kind: [ - [ "reduce" -> `Reduce - | "simpl" -> `Simpl - | "whd" -> `Whd ] + [ [ IDENT "reduce" | IDENT "Reduce" ] -> `Reduce + | [ IDENT "simplify" | IDENT "Simplify" ] -> `Simpl + | [ IDENT "whd" | IDENT "Whd" ] -> `Whd ] ]; tactic: [ - [ [ IDENT "absurd" | IDENT "Absurd" ] -> return_tactic loc TacticAst.Absurd - | [ IDENT "apply" | IDENT "Apply" ]; - t = tactic_term -> return_tactic loc (TacticAst.Apply t) + [ [ IDENT "absurd" | IDENT "Absurd" ]; t = tactic_term -> + return_tactic loc (TacticAst.Absurd t) + | [ IDENT "apply" | IDENT "Apply" ]; t = tactic_term -> + return_tactic loc (TacticAst.Apply t) | [ IDENT "assumption" | IDENT "Assumption" ] -> return_tactic loc TacticAst.Assumption + | [ IDENT "auto" | IDENT "Auto" ] -> return_tactic loc TacticAst.Auto | [ IDENT "change" | IDENT "Change" ]; t1 = tactic_term; "with"; t2 = tactic_term; where = tactic_where -> @@ -248,8 +267,7 @@ EXTEND | [ IDENT "discriminate" | IDENT "Discriminate" ]; hyp = IDENT -> return_tactic loc (TacticAst.Discriminate hyp) - | [ IDENT "elim" | IDENT "Elim" ]; IDENT "type"; - t = tactic_term -> + | [ IDENT "elimType" | IDENT "ElimType" ]; t = tactic_term -> return_tactic loc (TacticAst.ElimType t) | [ IDENT "elim" | IDENT "Elim" ]; t1 = tactic_term; @@ -264,6 +282,7 @@ EXTEND return_tactic loc (TacticAst.Fold (kind, t)) | [ IDENT "fourier" | IDENT "Fourier" ] -> return_tactic loc TacticAst.Fourier + | [ IDENT "hint" | IDENT "Hint" ] -> return_tactic loc TacticAst.Hint | [ IDENT "injection" | IDENT "Injection" ]; ident = IDENT -> return_tactic loc (TacticAst.Injection ident) | [ IDENT "intros" | IDENT "Intros" ]; @@ -271,11 +290,26 @@ EXTEND idents = OPT ident_list0 -> let idents = match idents with None -> [] | Some idents -> idents in return_tactic loc (TacticAst.Intros (num, idents)) + | [ IDENT "intro" | IDENT "Intro" ] -> + return_tactic loc (TacticAst.Intros (Some 1, [])) | [ IDENT "left" | IDENT "Left" ] -> return_tactic loc TacticAst.Left | [ "let" | "Let" ]; - t = tactic_term; IDENT "in"; where = IDENT -> + t = tactic_term; "in"; where = IDENT -> return_tactic loc (TacticAst.LetIn (t, where)) - (* TODO Reduce *) + | kind = reduction_kind; + pat = OPT [ + "in"; pat = [ IDENT "goal" -> `Goal | IDENT "hyp" -> `Everywhere ] -> + pat + ]; + terms = LIST0 term SEP SYMBOL "," -> + let tac = + (match (pat, terms) with + | None, [] -> TacticAst.Reduce (kind, None) + | None, terms -> TacticAst.Reduce (kind, Some (terms, `Goal)) + | Some pat, [] -> TacticAst.Reduce (kind, Some ([], pat)) + | Some pat, terms -> TacticAst.Reduce (kind, Some (terms, pat))) + in + return_tactic loc tac | [ IDENT "reflexivity" | IDENT "Reflexivity" ] -> return_tactic loc TacticAst.Reflexivity | [ IDENT "replace" | IDENT "Replace" ]; @@ -293,9 +327,11 @@ EXTEND return_tactic loc (TacticAst.Transitivity t) ] ]; - tactical0: [ [ t = tactical; SYMBOL "." -> t ] ]; + tactical0: [ [ t = tactical; SYMBOL ";;" -> return_tactical loc 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) ] @@ -328,99 +364,95 @@ 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) ] ]; + inductive_spec: [ [ + fst_name = IDENT; params = LIST0 [ + PAREN "("; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":"; + typ = term; PAREN ")" -> (names, typ) ]; + SYMBOL ":"; fst_typ = term; SYMBOL <:unicode>; OPT SYMBOL "|"; + fst_constructors = LIST0 constructor SEP SYMBOL "|"; + tl = OPT [ "with"; + types = LIST1 [ + name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode>; + OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" -> + (name, true, typ, constructors) ] SEP "with" -> types + ] -> + let params = + List.fold_right + (fun (names, typ) acc -> + (List.map (fun name -> (name, typ)) names) @ acc) + params [] + in + let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in + let tl_ind_types = match tl with None -> [] | Some types -> types in + let ind_types = fst_ind_type :: tl_ind_types in + (params, ind_types) + ] ]; 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)) + [ [ 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> (* ≝ *); body = term -> body ] -> + return_command loc (TacticAst.Theorem (flavour, name, typ, body)) + | [ IDENT "inductive" | IDENT "Inductive" ]; spec = inductive_spec -> + let (params, ind_types) = spec in + return_command loc (TacticAst.Inductive (params, ind_types)) + | [ IDENT "coinductive" | IDENT "CoInductive" ]; spec = inductive_spec -> + let (params, ind_types) = spec in + let ind_types = (* set inductive flags to false (coinductive) *) + List.map (fun (name, _, term, ctors) -> (name, false, term, ctors)) + ind_types + in + return_command loc (TacticAst.Inductive (params, ind_types)) + | [ IDENT "goal" | IDENT "Goal" ]; typ = term; + body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> + return_command loc (TacticAst.Theorem (`Goal, None, typ, body)) + | [ IDENT "undo" | IDENT "Undo" ]; steps = OPT NUM -> + return_command loc (TacticAst.Undo (int_opt steps)) + | [ IDENT "redo" | IDENT "Redo" ]; steps = OPT NUM -> + return_command loc (TacticAst.Redo (int_opt steps)) + | [ IDENT "baseuri" | IDENT "Baseuri" ]; uri = OPT QSTRING -> + return_command loc (TacticAst.Baseuri uri) + | [ IDENT "check" | IDENT "Check" ]; t = term -> + return_command loc (TacticAst.Check t) ] ]; 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)) + [ cmd = tactical0 -> Command cmd + | s = COMMENT -> Comment (loc, s) ] ]; - script: [ [ entries = LIST0 script_entry; EOI -> entries ] ]; + script: [ [ entries = LIST0 script_entry; EOI -> (loc, entries) ] ]; END let exc_located_wrapper f = try - 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))) + f () + with + | Stdpp.Exc_located (floc, Stream.Error msg) -> + raise (Parse_error (floc, msg)) + | Stdpp.Exc_located (floc, exn) -> + raise (Parse_error (floc, (Printexc.to_string exn))) let parse_term stream = - exc_located_wrapper (lazy (Grammar.Entry.parse term0 stream)) + exc_located_wrapper (fun () -> (Grammar.Entry.parse term0 stream)) let parse_tactic stream = - exc_located_wrapper (lazy (Grammar.Entry.parse tactic stream)) + exc_located_wrapper (fun () -> (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)) + exc_located_wrapper (fun () -> (Grammar.Entry.parse tactical0 stream)) let parse_script stream = - exc_located_wrapper (lazy (Grammar.Entry.parse script stream)) + exc_located_wrapper (fun () -> (Grammar.Entry.parse script stream)) (**/**) (** {2 Interface for gTopLevel} *) -open DisambiguateTypes - module EnvironmentP3 = struct type t = environment @@ -481,11 +513,8 @@ module EnvironmentP3 = if s = empty then Environment.empty else - try - Grammar.Entry.parse aliases (Stream.of_string s) - 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 + (fun () -> Grammar.Entry.parse aliases (Stream.of_string s)) end (* vim:set encoding=utf8: *)