X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=9a4340f9fb4b692a9c797e63de88875f57c5ff6f;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;hp=a539fef6c238783365912191b037985ec8a75a3d;hpb=797b256a0e91614b8ef8e0061fa0d624189a93db;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index a539fef6c..9a4340f9f 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -23,7 +23,7 @@ * http://helm.cs.unibo.it/ *) -let debug = true +let debug = false let debug_print s = if debug then begin prerr_endline ""; @@ -35,10 +35,16 @@ let debug_print s = * thus be interpreted differently than others *) let use_fresh_num_instances = false + (** does the lexer return COMMENT tokens? *) +let return_comments = false + open Printf + open DisambiguateTypes -exception Parse_error of string +exception Parse_error of Token.flocation * string + +let cic_lexer = CicTextualLexer2.cic_lexer ~comments:return_comments () let fresh_num_instance = let n = ref 0 in @@ -47,11 +53,11 @@ let fresh_num_instance = 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 suri = + let term = CicUtil.term_of_uri (UriManager.uri_of_string suri) in + (suri, (fun _ _ _ -> term)) -let grammar = Grammar.gcreate CicTextualLexer2.cic_lexer +let grammar = Grammar.gcreate cic_lexer let term = Grammar.Entry.create grammar "term" let term0 = Grammar.Entry.create grammar "term0" @@ -59,11 +65,13 @@ 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 alias_spec = Grammar.Entry.create grammar "alias_spec" +let macro = Grammar.Entry.create grammar "macro" +let script = Grammar.Entry.create grammar "script" +let statement = Grammar.Entry.create grammar "statement" +let statements = Grammar.Entry.create grammar "statements" 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 floc msg = let (x, y) = CicAst.loc_of_floc floc in @@ -73,32 +81,60 @@ let name_of_string = function | "_" -> Cic.Anonymous | s -> Cic.Name s +let string_of_name = function + | Cic.Anonymous -> "_" + | Cic.Name s -> s + let int_opt = function | None -> None | Some lexeme -> Some (int_of_string lexeme) +let int_of_string s = + try + Pervasives.int_of_string s + with Failure _ -> + failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s) + + (** the uri of an inductive type (a ".ind" uri) is not meaningful without an + * xpointer. Still, it's likely that an user who wrote "cic:/blabla/foo.ind" + * actually meant "cic:/blabla/foo.ind#xpointer(1/1)", i.e. the first inductive + * type in a block of mutual inductive types. + * + * This function performs the expansion foo.ind -> foo#xpointer..., if needed + *) +let ind_expansion uri = + let len = String.length uri in + if len >= 4 && String.sub uri (len - 4) 4 = ".ind" then + uri ^ "#xpointer(1/1)" + else + uri + +let mk_binder_ast binder typ vars body = + List.fold_right + (fun var body -> + let name = name_of_string var in + CicAst.Binder (binder, (name, typ), body)) + vars body + EXTEND - GLOBAL: term term0 tactic tactical tactical0 command; + GLOBAL: term term0 statement statements; int: [ [ num = NUM -> try int_of_string num - with Failure _ -> - let (x, y) = CicAst.loc_of_floc 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: [ [ s = SYMBOL "_" -> None | t = term -> Some t ] ]; - binder: [ - [ SYMBOL <:unicode> (* λ *) -> `Lambda - | SYMBOL <:unicode> (* Π *) -> `Pi + binder_low: [ + [ SYMBOL <:unicode> (* Π *) -> `Pi | SYMBOL <:unicode> (* ∃ *) -> `Exists | SYMBOL <:unicode> (* ∀ *) -> `Forall ] ]; + binder_high: [ [ SYMBOL <:unicode> (* λ *) -> `Lambda ] ]; sort: [ [ "Prop" -> `Prop | "Set" -> `Set @@ -107,22 +143,23 @@ EXTEND ]; typed_name: [ [ PAREN "("; i = IDENT; SYMBOL ":"; typ = term; PAREN ")" -> - (name_of_string i, Some typ) - | i = IDENT -> (name_of_string i, None) + (Cic.Name i, Some typ) + | i = IDENT -> (Cic.Name i, None) + ] + ]; + subst: [ + [ SYMBOL "\\subst"; (* to avoid catching frequent "a [1]" cases *) + PAREN "["; + substs = LIST1 [ + i = IDENT; SYMBOL <:unicode> (* ≔ *); t = term -> (i, t) + ] SEP SYMBOL ";"; + PAREN "]" -> + substs ] ]; substituted_name: [ (* a subs.name is an explicit substitution subject *) - [ s = IDENT; - subst = OPT [ - SYMBOL "\\subst"; (* to avoid catching frequent "a [1]" cases *) - PAREN "["; - substs = LIST1 [ - i = IDENT; SYMBOL <:unicode> (* ≔ *); t = term -> (i, t) - ] SEP SYMBOL ";"; - PAREN "]" -> - substs - ] -> - CicAst.Ident (s, subst) + [ s = IDENT; subst = OPT subst -> CicAst.Ident (s, subst) + | s = URI; subst = OPT subst -> CicAst.Uri (ind_expansion s, subst) ] ]; name: [ (* as substituted_name with no explicit substitution *) @@ -134,47 +171,93 @@ EXTEND (head, vars) ] ]; + arg: [ + [ PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ","; + SYMBOL ":"; ty = term; PAREN ")" -> names,ty + | name = IDENT -> [name],CicAst.Implicit + ] + ]; + let_defs:[ + [ defs = LIST1 [ + name = IDENT; + args = LIST1 [arg = arg -> arg]; + index_name = OPT [ "on"; idx = IDENT -> idx ]; + ty = OPT [ SYMBOL ":" ; t = term -> t ]; + SYMBOL <:unicode> (* ≝ *); + t1 = term -> + let rec list_of_binder binder ty final_term = function + | [] -> final_term + | name::tl -> + CicAst.Binder (binder, (Cic.Name name, Some ty), + list_of_binder binder ty final_term tl) + in + let rec binder_of_arg_list binder final_term = function + | [] -> final_term + | (l,ty)::tl -> + list_of_binder binder ty + (binder_of_arg_list binder final_term tl) l + in + let t1' = binder_of_arg_list `Lambda t1 args in + let ty' = + match ty with + | None -> None + | Some ty -> Some (binder_of_arg_list `Pi ty args) + in + let rec get_position_of name n = function + | [] -> (None,n) + | nam::tl -> + if nam = name then + (Some n,n) + else + (get_position_of name (n+1) tl) + in + let rec find_arg name n = function + | [] -> (fail loc (sprintf "Argument %s not found" name)) + | (l,_)::tl -> + let (got,len) = get_position_of name 0 l in + (match got with + | None -> (find_arg name (n+len) tl) + | Some where -> n + where) + in + let index = + (match index_name with + | None -> 0 + | (Some name) -> find_arg name 0 args) + in + ((Cic.Name name,ty'), t1', index) + ] SEP "and" -> defs + ]]; + constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ]; + binder_vars: [ + [ vars = [ l = LIST1 IDENT SEP SYMBOL "," -> l | SYMBOL "_" -> ["_"]]; + typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ) + | PAREN "("; + vars = [ l = LIST1 IDENT SEP SYMBOL "," -> l | SYMBOL "_" -> ["_"]]; + typ = OPT [ SYMBOL ":"; t = term -> t ]; + PAREN ")" -> (vars, typ) + ] + ]; term0: [ [ t = term; EOI -> return_term loc t ] ]; term: [ "letin" NONA [ "let"; var = typed_name; - SYMBOL "="; (* SYMBOL <:unicode> (* ≝ *); *) + SYMBOL <:unicode> (* ≝ *); t1 = term; "in"; t2 = term -> return_term loc (CicAst.LetIn (var, t1, t2)) | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; - defs = LIST1 [ - var = typed_name; - index = OPT [ PAREN "("; index = NUM; PAREN ")" -> - int_of_string index - ]; - SYMBOL "="; (* SYMBOL <:unicode> (* ≝ *); *) - t1 = term -> - (var, t1, (match index with None -> 0 | Some i -> i)) - ] SEP "and"; - "in"; body = term -> + defs = let_defs; "in"; body = term -> return_term loc (CicAst.LetRec (ind_kind, defs, body)) ] | "binder" RIGHTA [ - b = binder; - (vars, typ) = - [ vars = LIST1 IDENT; - typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ) - | PAREN "("; vars = LIST1 IDENT; - typ = OPT [ SYMBOL ":"; t = term -> t ]; PAREN ")" -> (vars, typ) - ]; - SYMBOL ","; body = term -> - let binder = - List.fold_right - (fun var body -> - let name = name_of_string var in - CicAst.Binder (b, (name, typ), body)) - vars body - in + b = binder_low; (vars, typ) = binder_vars; SYMBOL "."; body = term -> + let binder = mk_binder_ast b typ vars body in + return_term loc binder + | b = binder_high; (vars, typ) = binder_vars; SYMBOL "."; body = term -> + let binder = mk_binder_ast b typ vars body in return_term loc binder | t1 = term; SYMBOL <:unicode> (* → *); t2 = term -> - return_term loc - (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2)) + 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 *) ] @@ -200,6 +283,7 @@ EXTEND | n = substituted_name -> return_term loc n | i = NUM -> return_term loc (CicAst.Num (i, (fresh_num_instance ()))) | IMPLICIT -> return_term loc CicAst.Implicit + | PLACEHOLDER -> return_term loc CicAst.UserInput | m = META; substs = [ PAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; PAREN "]" -> @@ -214,11 +298,12 @@ EXTEND return_term loc (CicAst.Meta (index, substs)) | outtyp = OPT [ PAREN "["; typ = term; PAREN "]" -> typ ]; "match"; t = term; - indty_ident = OPT [ SYMBOL ":"; id = IDENT -> id ]; + indty_ident = OPT ["in" ; id = IDENT -> id ]; "with"; PAREN "["; patterns = LIST0 [ - lhs = pattern; SYMBOL <:unicode> (* ⇒ *); rhs = term -> + lhs = pattern; SYMBOL <:unicode> (* ⇒ *); rhs = term + -> ((lhs: CicAst.case_pattern), rhs) ] SEP SYMBOL "|"; PAREN "]" -> @@ -229,164 +314,392 @@ EXTEND | PAREN "("; t = term; PAREN ")" -> return_term loc t ] ]; - tactic_where: [ - [ where = OPT [ "in"; ident = IDENT -> ident ] -> where ] - ]; tactic_term: [ [ t = term -> t ] ]; ident_list0: [ [ PAREN "["; idents = LIST0 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ] ]; - ident_list1: [ - [ PAREN "["; idents = LIST1 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ] + tactic_term_list1: [ + [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ] ]; reduction_kind: [ - [ "reduce" -> `Reduce - | "simpl" -> `Simpl - | "whd" -> `Whd ] + [ [ IDENT "reduce" ] -> `Reduce + | [ IDENT "simplify" ] -> `Simpl + | [ IDENT "whd" ] -> `Whd + | [ IDENT "normalize" ] -> `Normalize ] + ]; + sequent_pattern_spec : [ + [ hyp_paths = + LIST0 + [ id = IDENT ; + path = OPT [SYMBOL ":" ; path = term -> path ] -> + (id,match path with Some p -> p | None -> CicAst.UserInput) ] + SEP SYMBOL ";"; + goal_path = OPT [ SYMBOL <:unicode>; term = term -> term ] -> + let goal_path = + match goal_path with + None -> CicAst.UserInput + | Some goal_path -> goal_path + in + hyp_paths,goal_path + ] + ]; + pattern_spec: [ + [ res = OPT [ + "in"; + wanted_and_sps = + [ "match" ; wanted = term ; + sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] -> + Some wanted,sps + | sps = sequent_pattern_spec -> + None,Some sps + ] -> + let wanted,hyp_paths,goal_path = + match wanted_and_sps with + wanted,None -> wanted, [], CicAst.UserInput + | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path + in + wanted, hyp_paths, goal_path ] -> + match res with + None -> None,[],CicAst.UserInput + | Some ps -> ps] + ]; + direction: [ + [ SYMBOL ">" -> `LeftToRight + | SYMBOL "<" -> `RightToLeft ] ]; tactic: [ - [ [ 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" | 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" | IDENT "Discriminate" ]; - hyp = IDENT -> - return_tactic loc (TacticAst.Discriminate hyp) - | [ IDENT "elim" | IDENT "Elim" ]; IDENT "type"; - t = tactic_term -> - return_tactic loc (TacticAst.ElimType t) - | [ IDENT "elim" | IDENT "Elim" ]; - t1 = tactic_term; - using = OPT [ "using"; using = tactic_term -> using ] -> - return_tactic loc (TacticAst.Elim (t1, using)) - | [ 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" | IDENT "Fourier" ] -> - return_tactic loc TacticAst.Fourier - | [ IDENT "injection" | IDENT "Injection" ]; ident = IDENT -> - return_tactic loc (TacticAst.Injection ident) - | [ IDENT "intros" | IDENT "Intros" ]; - num = OPT [ num = int -> num ]; - idents = OPT ident_list0 -> + [ IDENT "absurd"; t = tactic_term -> + TacticAst.Absurd (loc, t) + | IDENT "apply"; t = tactic_term -> + TacticAst.Apply (loc, t) + | IDENT "assumption" -> + TacticAst.Assumption loc + | IDENT "auto"; + depth = OPT [ IDENT "depth"; SYMBOL "="; i = NUM -> int_of_string i ]; + width = OPT [ IDENT "width"; SYMBOL "="; i = NUM -> int_of_string i ] -> + TacticAst.Auto (loc,depth,width) + | IDENT "clear"; id = IDENT -> + TacticAst.Clear (loc,id) + | IDENT "clearbody"; id = IDENT -> + TacticAst.ClearBody (loc,id) + | IDENT "change"; what = pattern_spec; "with"; t = tactic_term -> + TacticAst.Change (loc, what, t) + | IDENT "compare"; t = tactic_term -> + TacticAst.Compare (loc,t) + | IDENT "constructor"; n = NUM -> + TacticAst.Constructor (loc,int_of_string n) + | IDENT "contradiction" -> + TacticAst.Contradiction loc + | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] -> + TacticAst.Cut (loc, ident, t) + | IDENT "decide"; IDENT "equality" -> + TacticAst.DecideEquality loc + | IDENT "decompose"; where = tactic_term -> + TacticAst.Decompose (loc, where) + | IDENT "discriminate"; t = tactic_term -> + TacticAst.Discriminate (loc, t) + | IDENT "elim"; what = tactic_term; + using = OPT [ "using"; using = tactic_term -> using ]; + OPT "names"; num = OPT [num = int -> num]; idents = OPT ident_list0 -> + let idents = match idents with None -> [] | Some idents -> idents in + TacticAst.Elim (loc, what, using, num, idents) + | IDENT "elimType"; what = tactic_term; + using = OPT [ "using"; using = tactic_term -> using ]; + OPT "names"; 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 "intro" | IDENT "Intro" ] -> - return_tactic loc (TacticAst.Intros (Some 1, [])) - | [ IDENT "left" | IDENT "Left" ] -> return_tactic loc TacticAst.Left - | [ "let" | "Let" ]; - t = tactic_term; "in"; where = IDENT -> - return_tactic loc (TacticAst.LetIn (t, where)) - (* TODO Reduce *) - | [ 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" | 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) + TacticAst.ElimType (loc, what, using, num, idents) + | IDENT "exact"; t = tactic_term -> + TacticAst.Exact (loc, t) + | IDENT "exists" -> + TacticAst.Exists loc + | IDENT "fail" -> TacticAst.Fail loc + | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec -> + let (pt,_,_) = p in + if pt <> None then + raise + (Parse_error + (loc,"the pattern cannot specify the term to replace, only its paths in the hypotheses and in the conclusion")) + else + TacticAst.Fold (loc, kind, t, p) + | IDENT "fourier" -> + TacticAst.Fourier loc + | IDENT "fwd"; hyp = IDENT; idents = OPT ident_list0 -> + let idents = match idents with None -> [] | Some idents -> idents in + TacticAst.FwdSimpl (loc, hyp, idents) + | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] -> + TacticAst.Generalize (loc,p,id) + | IDENT "goal"; n = NUM -> + TacticAst.Goal (loc, int_of_string n) + | IDENT "id" -> TacticAst.IdTac loc + | IDENT "injection"; t = tactic_term -> + TacticAst.Injection (loc, t) + | IDENT "intro"; ident = OPT IDENT -> + let idents = match ident with None -> [] | Some id -> [id] in + TacticAst.Intros (loc, Some 1, idents) + | IDENT "intros"; num = OPT [num = int -> num]; idents = OPT ident_list0 -> + let idents = match idents with None -> [] | Some idents -> idents in + TacticAst.Intros (loc, num, idents) + | IDENT "lapply"; + depth = OPT [ IDENT "depth"; SYMBOL "="; i = NUM -> int_of_string i ]; + what = tactic_term; + to_what = OPT [ "to" ; t = tactic_term_list1 -> t ]; + ident = OPT [ "using" ; ident = IDENT -> ident ] -> + let to_what = match to_what with None -> [] | Some to_what -> to_what in + TacticAst.LApply (loc, depth, to_what, what, ident) + | IDENT "left" -> TacticAst.Left loc + | IDENT "letin"; where = IDENT ; SYMBOL <:unicode> ; t = tactic_term -> + TacticAst.LetIn (loc, t, where) + | kind = reduction_kind; p = pattern_spec -> + TacticAst.Reduce (loc, kind, p) + | IDENT "reflexivity" -> + TacticAst.Reflexivity loc + | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term -> + TacticAst.Replace (loc, p, t) + | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec -> + let (pt,_,_) = p in + if pt <> None then + raise + (Parse_error + (loc,"the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")) + else + TacticAst.Rewrite (loc, d, t, p) + | IDENT "right" -> + TacticAst.Right loc + | IDENT "ring" -> + TacticAst.Ring loc + | IDENT "split" -> + TacticAst.Split loc + | IDENT "symmetry" -> + TacticAst.Symmetry loc + | IDENT "transitivity"; t = tactic_term -> + TacticAst.Transitivity (loc, t) ] ]; - tactical0: [ [ t = tactical; SYMBOL "." -> t ] ]; tactical: - [ "command" NONA - [ cmd = command -> return_tactical loc (TacticAst.Command cmd) ] - | "sequence" LEFTA - [ tactics = LIST1 NEXT SEP SYMBOL ";" -> - return_tactical loc (TacticAst.Seq tactics) + [ "sequence" LEFTA + [ tacticals = LIST1 NEXT SEP SYMBOL ";" -> + match tacticals with + [] -> assert false + | [tac] -> tac + | l -> TacticAst.Seq (loc, l) ] | "then" NONA - [ tac = tactical; - PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" -> - return_tactical loc (TacticAst.Then (tac, tacs)) + [ tac = tactical; SYMBOL ";"; + PAREN "["; tacs = LIST0 tactical SEP SYMBOL "|"; PAREN "]" -> + (TacticAst.Then (loc, tac, tacs)) ] | "loops" RIGHTA - [ [ IDENT "do" | IDENT "Do" ]; count = int; tac = tactical -> - return_tactical loc (TacticAst.Do (count, tac)) - | [ IDENT "repeat" | IDENT "Repeat" ]; tac = tactical -> - return_tactical loc (TacticAst.Repeat tac) + [ IDENT "do"; count = int; tac = tactical -> + TacticAst.Do (loc, count, tac) + | IDENT "repeat"; tac = tactical -> + TacticAst.Repeat (loc, tac) ] | "simple" NONA - [ [ IDENT "tries" | IDENT "Tries" ]; - PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" -> - return_tactical loc (TacticAst.Tries tacs) - | [ 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) + [ IDENT "first"; + PAREN "["; tacs = LIST0 tactical SEP SYMBOL "|"; PAREN "]" -> + TacticAst.First (loc, tacs) + | IDENT "try"; tac = NEXT -> + TacticAst.Try (loc, tac) + | IDENT "solve"; + PAREN "["; tacs = LIST0 tactical SEP SYMBOL "|"; PAREN "]" -> + TacticAst.Solve (loc, tacs) + | PAREN "("; tac = tactical; PAREN ")" -> tac + | tac = tactic -> TacticAst.Tactic (loc, 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 + theorem_flavour: [ + [ [ IDENT "definition" ] -> `Definition + | [ IDENT "fact" ] -> `Fact + | [ IDENT "lemma" ] -> `Lemma + | [ IDENT "remark" ] -> `Remark + | [ IDENT "theorem" ] -> `Theorem ] ]; - command: [ - [ [ 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; + inductive_spec: [ [ + fst_name = IDENT; params = LIST0 [ arg=arg -> arg ]; + 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) + ] ]; + + record_spec: [ [ + name = IDENT; params = LIST0 [ arg = arg -> arg ] ; + SYMBOL ":"; typ = term; SYMBOL <:unicode>; PAREN "{" ; + fields = LIST0 [ + name = IDENT ; SYMBOL ":" ; ty = term -> (name,ty) + ] SEP SYMBOL ";"; PAREN "}" -> + let params = + List.fold_right + (fun (names, typ) acc -> + (List.map (fun name -> (name, typ)) names) @ acc) + params [] + in + (params,name,typ,fields) + ] ]; + + macro: [ + [ [ IDENT "quit" ] -> TacticAst.Quit loc +(* | [ IDENT "abort" ] -> TacticAst.Abort loc *) + | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name) +(* | [ IDENT "undo" ]; steps = OPT NUM -> + TacticAst.Undo (loc, int_opt steps) + | [ IDENT "redo" ]; steps = OPT NUM -> + TacticAst.Redo (loc, int_opt steps) *) + | [ IDENT "check" ]; t = term -> + TacticAst.Check (loc, t) + | [ IDENT "hint" ] -> TacticAst.Hint loc + | [ IDENT "whelp"; "match" ] ; t = term -> + TacticAst.WMatch (loc,t) + | [ IDENT "whelp"; IDENT "instance" ] ; t = term -> + TacticAst.WInstance (loc,t) + | [ IDENT "whelp"; IDENT "locate" ] ; id = IDENT -> + TacticAst.WLocate (loc,id) + | [ IDENT "whelp"; IDENT "elim" ] ; t = term -> + TacticAst.WElim (loc, t) + | [ IDENT "whelp"; IDENT "hint" ] ; t = term -> + TacticAst.WHint (loc,t) + | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name) + ] + ]; + + alias_spec: [ + [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING -> + let alpha = "[a-zA-Z]" in + let num = "[0-9]+" in + let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in + let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in + let rex = Str.regexp ("^"^ident^"$") in + if Str.string_match rex id 0 then + if (try ignore (UriManager.uri_of_string uri); true + with UriManager.IllFormedUri _ -> false) + then + TacticAst.Ident_alias (id, uri) + else + raise (Parse_error (loc,sprintf "Not a valid uri: %s" uri)) + else + raise (Parse_error (loc,sprintf "Not a valid identifier: %s" id)) + | IDENT "symbol"; symbol = QSTRING; + instance = OPT [ PAREN "("; IDENT "instance"; n = NUM; PAREN ")" -> n ]; + SYMBOL "="; dsc = QSTRING -> + let instance = + match instance with Some i -> int_of_string i | None -> 0 + in + TacticAst.Symbol_alias (symbol, instance, dsc) + | IDENT "num"; + instance = OPT [ PAREN "("; IDENT "instance"; n = NUM; PAREN ")" -> n ]; + SYMBOL "="; dsc = QSTRING -> + let instance = + match instance with Some i -> int_of_string i | None -> 0 + in + TacticAst.Number_alias (instance, dsc) + ] + ]; + + command: [[ + [ IDENT "set" ]; n = QSTRING; v = QSTRING -> + TacticAst.Set (loc, n, v) + | [ IDENT "drop" ] -> TacticAst.Drop loc + | [ IDENT "qed" ] -> TacticAst.Qed loc + | flavour = theorem_flavour; name = 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; + TacticAst.Obj (loc,TacticAst.Theorem (flavour, name, typ, body)) + | flavour = theorem_flavour; name = IDENT; 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)) + TacticAst.Obj (loc,TacticAst.Theorem (flavour, name, CicAst.Implicit, body)) + | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; + defs = let_defs -> + let name,ty = + match defs with + | ((Cic.Name name,Some ty),_,_) :: _ -> name,ty + | ((Cic.Name name,None),_,_) :: _ -> name,CicAst.Implicit + | _ -> assert false + in + let body = CicAst.Ident (name,None) in + TacticAst.Obj (loc,TacticAst.Theorem(`Definition, name, ty, + Some (CicAst.LetRec (ind_kind, defs, body)))) + + | [ IDENT "inductive" ]; spec = inductive_spec -> + let (params, ind_types) = spec in + TacticAst.Obj (loc,TacticAst.Inductive (params, ind_types)) + | [ 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 + TacticAst.Obj (loc,TacticAst.Inductive (params, ind_types)) + | IDENT "coercion" ; name = IDENT -> + TacticAst.Coercion (loc, CicAst.Ident (name,Some [])) + | IDENT "coercion" ; name = URI -> + TacticAst.Coercion (loc, CicAst.Uri (name,Some [])) + | IDENT "alias" ; spec = alias_spec -> + TacticAst.Alias (loc, spec) + | IDENT "record" ; (params,name,ty,fields) = record_spec -> + TacticAst.Obj (loc,TacticAst.Record (params,name,ty,fields)) + | IDENT "include" ; path = QSTRING -> + TacticAst.Include (loc,path) + | IDENT "default" ; what = QSTRING ; uris = LIST1 URI -> + let uris = List.map UriManager.uri_of_string uris in + TacticAst.Default (loc,what,uris) + ]]; + + executable: [ + [ cmd = command; SYMBOL "." -> TacticAst.Command (loc, cmd) + | tac = tactical; SYMBOL "." -> TacticAst.Tactical (loc, tac) + | mac = macro; SYMBOL "." -> TacticAst.Macro (loc, mac) ] ]; + + comment: [ + [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT -> + TacticAst.Code (loc, ex) + | str = NOTE -> + TacticAst.Note (loc, str) + ] + ]; + + statement: [ + [ ex = executable -> TacticAst.Executable (loc,ex) + | com = comment -> TacticAst.Comment (loc, com) + ] + ]; + statements: [ + [ l = LIST0 statement ; EOI -> l + ] + ]; END let exc_located_wrapper f = try - Lazy.force f - with Stdpp.Exc_located (floc, exn) -> - let (x, y) = CicAst.loc_of_floc floc in - 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)) -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)) + exc_located_wrapper (fun () -> (Grammar.Entry.parse term0 stream)) +let parse_statement stream = + exc_located_wrapper (fun () -> (Grammar.Entry.parse statement stream)) +let parse_statements stream = + exc_located_wrapper (fun () -> (Grammar.Entry.parse statements stream)) + (**/**) @@ -398,7 +711,7 @@ module EnvironmentP3 = let empty = "" - let aliases_grammar = Grammar.gcreate CicTextualLexer2.cic_lexer + let aliases_grammar = Grammar.gcreate cic_lexer let aliases = Grammar.Entry.create aliases_grammar "aliases" let to_string env = @@ -407,17 +720,19 @@ module EnvironmentP3 = (fun domain_item (dsc, _) acc -> let s = match domain_item with - | Id id -> sprintf "alias id %s = %s" id dsc - | Symbol (symb, instance) -> - sprintf "alias symbol \"%s\" (instance %d) = \"%s\"" - symb instance dsc - | Num instance -> - sprintf "alias num (instance %d) = \"%s\"" instance dsc + | Id id -> + TacticAstPp.pp_alias (TacticAst.Ident_alias (id, dsc)) ^ "." + | Symbol (symb, i) -> + TacticAstPp.pp_alias (TacticAst.Symbol_alias (symb, i, dsc)) + ^ "." + | Num i -> + TacticAstPp.pp_alias (TacticAst.Number_alias (i, dsc)) ^ "." in s :: acc) env [] in - String.concat "\n" (List.sort compare aliases) + String.concat "\n" (List.sort compare aliases) ^ + (if aliases = [] then "" else "\n") EXTEND GLOBAL: aliases; @@ -432,8 +747,8 @@ module EnvironmentP3 = alias: [ (* return a pair from an alias *) [ IDENT "alias"; choice = - [ IDENT "id"; id = IDENT; SYMBOL "="; uri = URI -> - (Id id, choice_of_uri uri) + [ IDENT "id"; id = IDENT; SYMBOL "="; suri = URI -> + (Id id, choice_of_uri suri) | IDENT "symbol"; symbol = QSTRING; PAREN "("; IDENT "instance"; instance = NUM; PAREN ")"; SYMBOL "="; dsc = QSTRING -> @@ -452,12 +767,8 @@ module EnvironmentP3 = if s = empty then Environment.empty else - try - Grammar.Entry.parse aliases (Stream.of_string s) - with Stdpp.Exc_located (floc, exn) -> - let (x, y) = CicAst.loc_of_floc floc in - 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: *)