diff options
Diffstat (limited to 'plugins/funind/g_indfun.ml4')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 118 |
1 files changed, 35 insertions, 83 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 41fafdf1..123399d5 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -16,19 +16,20 @@ open Indfun open Genarg open Pcoq open Tacticals +open Constr let pr_binding prc = function - | loc, Rawterm.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c) - | loc, Rawterm.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) + | loc, Glob_term.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c) + | loc, Glob_term.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) let pr_bindings prc prlc = function - | Rawterm.ImplicitBindings l -> + | Glob_term.ImplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ Util.prlist_with_sep spc prc l - | Rawterm.ExplicitBindings l -> + | Glob_term.ExplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l - | Rawterm.NoBindings -> mt () + | Glob_term.NoBindings -> mt () let pr_with_bindings prc prlc (c,bl) = prc c ++ hv 0 (pr_bindings prc prlc bl) @@ -55,7 +56,6 @@ let pr_fun_ind_using_typed prc prlc _ opt_c = ARGUMENT EXTEND fun_ind_using - TYPED AS constr_with_bindings_opt PRINTED BY pr_fun_ind_using_typed RAW_TYPED AS constr_with_bindings_opt RAW_PRINTED BY pr_fun_ind_using @@ -129,85 +129,36 @@ ARGUMENT EXTEND auto_using' | [ ] -> [ [] ] END -let pr_rec_annotation2_aux s r id l = - str ("{"^s^" ") ++ Ppconstr.pr_constr_expr r ++ - Util.pr_opt Nameops.pr_id id ++ - Pptactic.pr_auto_using Ppconstr.pr_constr_expr l ++ str "}" - -let pr_rec_annotation2 = function - | Struct id -> str "{struct" ++ Nameops.pr_id id ++ str "}" - | Wf(r,id,l) -> pr_rec_annotation2_aux "wf" r id l - | Mes(r,id,l) -> pr_rec_annotation2_aux "measure" r id l - -VERNAC ARGUMENT EXTEND rec_annotation2 -PRINTED BY pr_rec_annotation2 - [ "{" "struct" ident(id) "}"] -> [ Struct id ] -| [ "{" "wf" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Wf(r,id,l) ] -| [ "{" "measure" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Mes(r,id,l) ] -END - -let pr_binder2 (idl,c) = - str "(" ++ Util.prlist_with_sep spc Nameops.pr_id idl ++ spc () ++ - str ": " ++ Ppconstr.pr_lconstr_expr c ++ str ")" +module Gram = Pcoq.Gram +module Vernac = Pcoq.Vernac_ +module Tactic = Pcoq.Tactic -VERNAC ARGUMENT EXTEND binder2 -PRINTED BY pr_binder2 - [ "(" ne_ident_list(idl) ":" lconstr(c) ")"] -> [ (idl,c) ] -END +module FunctionGram = +struct + let gec s = Gram.entry_create ("Function."^s) + (* types *) + let function_rec_definition_loc : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) located Gram.entry = gec "function_rec_definition_loc" +end +open FunctionGram -let make_binder2 (idl,c) = - LocalRawAssum (List.map (fun id -> (Util.dummy_loc,Name id)) idl,Topconstr.default_binder_kind,c) - -let pr_rec_definition2 (id,bl,annot,type_,def) = - Nameops.pr_id id ++ spc () ++ Util.prlist_with_sep spc pr_binder2 bl ++ - Util.pr_opt pr_rec_annotation2 annot ++ spc () ++ str ":" ++ spc () ++ - Ppconstr.pr_lconstr_expr type_ ++ str " :=" ++ spc () ++ - Ppconstr.pr_lconstr_expr def - -VERNAC ARGUMENT EXTEND rec_definition2 -PRINTED BY pr_rec_definition2 - [ ident(id) binder2_list(bl) - rec_annotation2_opt(annot) ":" lconstr(type_) - ":=" lconstr(def)] -> - [ (id,bl,annot,type_,def) ] -END +GEXTEND Gram + GLOBAL: function_rec_definition_loc ; -let make_rec_definitions2 (id,bl,annot,type_,def) = - let bl = List.map make_binder2 bl in - let names = List.map snd (Topconstr.names_of_local_assums bl) in - let check_one_name () = - if List.length names > 1 then - Util.user_err_loc - (Util.dummy_loc,"Function", - Pp.str "the recursive argument needs to be specified"); - in - let check_exists_args an = - try - let id = match an with - | Struct id -> id | Wf(_,Some id,_) -> id | Mes(_,Some id,_) -> id - | Wf(_,None,_) | Mes(_,None,_) -> failwith "check_exists_args" - in - (try ignore(Util.list_index0 (Name id) names); annot - with Not_found -> Util.user_err_loc - (Util.dummy_loc,"Function", - Pp.str "No argument named " ++ Nameops.pr_id id) - ) - with Failure "check_exists_args" -> check_one_name ();annot - in - let ni = - match annot with - | None -> - annot - | Some an -> - check_exists_args an - in - ((Util.dummy_loc,id), ni, bl, type_, def) + function_rec_definition_loc: + [ [ g = Vernac.rec_definition -> loc, g ]] + ; + END +type 'a function_rec_definition_loc_argtype = ((Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) located, 'a) Genarg.abstract_argument_type +let (wit_function_rec_definition_loc : Genarg.tlevel function_rec_definition_loc_argtype), + (globwit_function_rec_definition_loc : Genarg.glevel function_rec_definition_loc_argtype), + (rawwit_function_rec_definition_loc : Genarg.rlevel function_rec_definition_loc_argtype) = + Genarg.create_arg "function_rec_definition_loc" VERNAC COMMAND EXTEND Function - ["Function" ne_rec_definition2_list_sep(recsl,"with")] -> + ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] -> [ - do_generate_principle false (List.map make_rec_definitions2 recsl); + do_generate_principle false (List.map snd recsl); ] END @@ -215,7 +166,7 @@ END let pr_fun_scheme_arg (princ_name,fun_name,s) = Nameops.pr_id princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++ Libnames.pr_reference fun_name ++ spc() ++ str "Sort " ++ - Ppconstr.pr_rawsort s + Ppconstr.pr_glob_sort s VERNAC ARGUMENT EXTEND fun_scheme_arg PRINTED BY pr_fun_scheme_arg @@ -224,17 +175,18 @@ END let warning_error names e = + let e = Cerrors.process_vernac_interp_error e in match e with | Building_graph e -> Pp.msg_warning (str "Cannot define graph(s) for " ++ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Libnames.pr_reference names) ++ - if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ()) + if do_observe () then (spc () ++ Errors.print e) else mt ()) | Defining_principle e -> Pp.msg_warning (str "Cannot define principle(s) for "++ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Libnames.pr_reference names) ++ - if do_observe () then Cerrors.explain_exn e else mt ()) + if do_observe () then Errors.print e else mt ()) | _ -> raise e @@ -480,7 +432,7 @@ TACTIC EXTEND fauto [ "fauto" tactic(tac)] -> [ let heuristic = chose_heuristic None in - finduction None heuristic (snd tac) + finduction None heuristic (Tacinterp.eval_tactic tac) ] | [ "fauto" ] -> |