diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/ExtrOCamlInt63.v | 56 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.mlg | 12 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 324 | ||||
| -rw-r--r-- | plugins/funind/indfun.mli | 7 | ||||
| -rw-r--r-- | plugins/ltac/extratactics.mlg | 12 | ||||
| -rw-r--r-- | plugins/ssr/ssrparser.mlg | 17 | ||||
| -rw-r--r-- | plugins/syntax/r_syntax.ml | 3 |
7 files changed, 231 insertions, 200 deletions
diff --git a/plugins/extraction/ExtrOCamlInt63.v b/plugins/extraction/ExtrOCamlInt63.v new file mode 100644 index 0000000000..a2ee602313 --- /dev/null +++ b/plugins/extraction/ExtrOCamlInt63.v @@ -0,0 +1,56 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Extraction to OCaml of native 63-bit machine integers. *) + +From Coq Require Int63 Extraction. + +(** Basic data types used by some primitive operators. *) + +Extract Inductive bool => bool [ true false ]. +Extract Inductive prod => "( * )" [ "" ]. +Extract Inductive comparison => int [ "0" "(-1)" "1" ]. +Extract Inductive DoubleType.carry => "Uint63.carry" [ "Uint63.C0" "Uint63.C1" ]. + +(** Primitive types and operators. *) +Extract Constant Int63.int => "Uint63.t". +Extraction Inline Int63.int. +(* Otherwise, the name conflicts with the primitive OCaml type [int] *) + +Extract Constant Int63.lsl => "Uint63.l_sl". +Extract Constant Int63.lsr => "Uint63.l_sr". +Extract Constant Int63.land => "Uint63.l_and". +Extract Constant Int63.lor => "Uint63.l_or". +Extract Constant Int63.lxor => "Uint63.l_xor". + +Extract Constant Int63.add => "Uint63.add". +Extract Constant Int63.sub => "Uint63.sub". +Extract Constant Int63.mul => "Uint63.mul". +Extract Constant Int63.mulc => "Uint63.mulc". +Extract Constant Int63.div => "Uint63.div". +Extract Constant Int63.mod => "Uint63.rem". + +Extract Constant Int63.eqb => "Uint63.equal". +Extract Constant Int63.ltb => "Uint63.lt". +Extract Constant Int63.leb => "Uint63.le". + +Extract Constant Int63.addc => "Uint63.addc". +Extract Constant Int63.addcarryc => "Uint63.addcarryc". +Extract Constant Int63.subc => "Uint63.subc". +Extract Constant Int63.subcarryc => "Uint63.subcarryc". + +Extract Constant Int63.diveucl => "Uint63.diveucl". +Extract Constant Int63.diveucl_21 => "Uint63.div21". +Extract Constant Int63.addmuldiv => "Uint63.addmuldiv". + +Extract Constant Int63.compare => "Uint63.compare". + +Extract Constant Int63.head0 => "Uint63.head0". +Extract Constant Int63.tail0 => "Uint63.tail0". diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index 5f859b3e4b..1b75d3d966 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -148,9 +148,7 @@ END module Vernac = Pvernac.Vernac_ module Tactic = Pltac -type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located - -let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genarg.uniform_genarg_type) = +let (wit_function_rec_definition_loc : Vernacexpr.fixpoint_expr Loc.located Genarg.uniform_genarg_type) = Genarg.create_arg "function_rec_definition_loc" let function_rec_definition_loc = @@ -175,10 +173,10 @@ let () = let is_proof_termination_interactively_checked recsl = List.exists (function - | _,((_,( Some { CAst.v = CMeasureRec _ } - | Some { CAst.v = CWfRec _}),_,_,_),_) -> true - | _,((_,Some { CAst.v = CStructRec _ },_,_,_),_) - | _,((_,None,_,_,_),_) -> false) recsl + | _,( Vernacexpr.{ rec_order = Some { CAst.v = CMeasureRec _ } } + | Vernacexpr.{ rec_order = Some { CAst.v = CWfRec _} }) -> true + | _, Vernacexpr.{ rec_order = Some { CAst.v = CStructRec _ } } + | _, Vernacexpr.{ rec_order = None } -> false) recsl let classify_as_Fixpoint recsl = Vernac_classifier.classify_vernac diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 6e19ef4804..1987677d7d 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -1,3 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + open CErrors open Sorts open Util @@ -157,17 +167,16 @@ let interp_casted_constr_with_implicits env sigma impls c = and not as a constr *) -let build_newrecursive - lnameargsardef = +let build_newrecursive lnameargsardef = let env0 = Global.env() in let sigma = Evd.from_env env0 in let (rec_sign,rec_impls) = List.fold_left - (fun (env,impls) (({CAst.v=recname},_),bl,arityc,_) -> - let arityc = Constrexpr_ops.mkCProdN bl arityc in + (fun (env,impls) { Vernacexpr.fname={CAst.v=recname}; binders; rtype } -> + let arityc = Constrexpr_ops.mkCProdN binders rtype in let arity,ctx = Constrintern.interp_type env0 sigma arityc in let evd = Evd.from_env env0 in - let evd, (_, (_, impls')) = Constrintern.interp_context_evars ~program_mode:false env evd bl in + let evd, (_, (_, impls')) = Constrintern.interp_context_evars ~program_mode:false env evd binders in let impl = Constrintern.compute_internalization_data env0 evd Constrintern.Recursive arity impls' in let open Context.Named.Declaration in let r = Sorts.Relevant in (* TODO relevance *) @@ -175,26 +184,18 @@ let build_newrecursive (env0,Constrintern.empty_internalization_env) lnameargsardef in let recdef = (* Declare local notations *) - let f (_,bl,_,def) = - let def = abstract_glob_constr def bl in - interp_casted_constr_with_implicits - rec_sign sigma rec_impls def + let f { Vernacexpr.binders; body_def } = + match body_def with + | Some body_def -> + let def = abstract_glob_constr body_def binders in + interp_casted_constr_with_implicits + rec_sign sigma rec_impls def + | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in States.with_state_protection (List.map f) lnameargsardef in recdef,rec_impls -let build_newrecursive l = - let l' = List.map - (fun ((fixna,_,bll,ar,body_opt),lnot) -> - match body_opt with - | Some body -> - (fixna,bll,ar,body) - | None -> user_err ~hdr:"Function" (str "Body of Function must be given") - ) l - in - build_newrecursive l' - let error msg = user_err Pp.(str msg) (* Checks whether or not the mutual bloc is recursive *) @@ -237,8 +238,8 @@ let rec local_binders_length = function | Constrexpr.CLocalAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl | Constrexpr.CLocalPattern _::bl -> assert false -let prepare_body ((name,_,args,types,_),_) rt = - let n = local_binders_length args in +let prepare_body { Vernacexpr.binders; rtype } rt = + let n = local_binders_length binders in (* Pp.msgnl (str "nb lambda to chop : " ++ str (string_of_int n) ++ fnl () ++Printer.pr_glob_constr rt); *) let fun_args,rt' = chop_rlambda_n n rt in (fun_args,rt') @@ -336,13 +337,13 @@ let error_error names e = | _ -> raise e let generate_principle (evd:Evd.evar_map ref) pconstants on_error - is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs interactive_proof + is_general do_built (fix_rec_l : Vernacexpr.fixpoint_expr list) recdefs interactive_proof (continue_proof : int -> Names.Constant.t array -> EConstr.constr array -> int -> Tacmach.tactic) : unit = - let names = List.map (function (({CAst.v=name},_),_,_,_,_),_ -> name) fix_rec_l in + let names = List.map (function { Vernacexpr.fname = {CAst.v=name} } -> name) fix_rec_l in let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in let funs_args = List.map fst fun_bodies in - let funs_types = List.map (function ((_,_,_,types,_),_) -> types) fix_rec_l in + let funs_types = List.map (function { Vernacexpr.rtype } -> rtype) fix_rec_l in try (* We then register the Inductive graphs of the functions *) Glob_term_to_relation.build_inductive !evd pconstants funs_args funs_types recdefs; @@ -359,7 +360,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error locate_ind f_R_mut) in - let fname_kn (((fname,_),_,_,_,_),_) = + let fname_kn { Vernacexpr.fname } = let f_ref = qualid_of_ident ?loc:fname.CAst.loc fname.CAst.v in locate_with_msg (pr_qualid f_ref++str ": Not an inductive type!") @@ -398,23 +399,25 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error with e when CErrors.noncritical e -> on_error names e -let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = +let register_struct is_rec (fixpoint_exprl: Vernacexpr.fixpoint_expr list) = match fixpoint_exprl with - | [(({CAst.v=fname},pl),_,bl,ret_type,body),_] when not is_rec -> - let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in + | [ { Vernacexpr.fname; univs; binders; rtype; body_def } ] when not is_rec -> + let body = match body_def with + | Some body -> body + | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in ComDefinition.do_definition ~program_mode:false - ~name:fname + ~name:fname.CAst.v ~poly:false ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:Decls.Definition pl - bl None body (Some ret_type); + ~kind:Decls.Definition univs + binders None body (Some rtype); let evd,rev_pconstants = List.fold_left - (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> + (fun (evd,l) { Vernacexpr.fname } -> let evd,c = Evd.fresh_global - (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in + (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname.CAst.v)) in let (cst, u) = destConst evd c in let u = EInstance.kind evd u in evd,((cst, u) :: l) @@ -427,10 +430,10 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp ComFixpoint.do_fixpoint ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly:false fixpoint_exprl; let evd,rev_pconstants = List.fold_left - (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> + (fun (evd,l) { Vernacexpr.fname } -> let evd,c = Evd.fresh_global - (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in + (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname.CAst.v)) in let (cst, u) = destConst evd c in let u = EInstance.kind evd u in evd,((cst, u) :: l) @@ -464,7 +467,7 @@ let register_wf interactive_proof ?(is_mes=false) fname rec_impls wf_rel_expr wf let unbounded_eq = let f_app_args = CAst.make @@ Constrexpr.CAppExpl( - (None,qualid_of_ident fname,None) , + (None,qualid_of_ident fname.CAst.v,None) , (List.map (function | {CAst.v=Anonymous} -> assert false @@ -485,13 +488,13 @@ let register_wf interactive_proof ?(is_mes=false) fname rec_impls wf_rel_expr wf (generate_correction_proof_wf f_ref tcc_lemma_ref is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation ); - derive_inversion [fname] + derive_inversion [fname.CAst.v] with e when CErrors.noncritical e -> (* No proof done *) () in Recdef.recursive_definition ~interactive_proof - ~is_mes fname rec_impls + ~is_mes fname.CAst.v rec_impls type_of_f wf_rel_expr rec_arg_num @@ -607,88 +610,93 @@ and rebuild_nal aux bk bl' nal typ = let rebuild_bl aux bl typ = rebuild_bl aux bl typ -let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = - let fixl,ntns = ComFixpoint.extract_fixpoint_components ~structonly:false fixpoint_exprl in - let ((_,_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in +let recompute_binder_list fixpoint_exprl = + let fixl = + List.map (fun fix -> Vernacexpr.{ + fix + with rec_order = ComFixpoint.adjust_rec_order ~structonly:false fix.binders fix.rec_order }) fixpoint_exprl in + let ((_,_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl in let constr_expr_typel = with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in let fixpoint_exprl_with_new_bl = - List.map2 (fun ((lna,rec_order_opt,bl,ret_typ,opt_body),notation_list) fix_typ -> - - let new_bl',new_ret_type = rebuild_bl [] bl fix_typ in - (((lna,rec_order_opt,new_bl',new_ret_type,opt_body),notation_list):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) - ) - fixpoint_exprl constr_expr_typel + List.map2 (fun ({ Vernacexpr.binders } as fp) fix_typ -> + let binders, rtype = rebuild_bl [] binders fix_typ in + { fp with Vernacexpr.binders; rtype } + ) fixpoint_exprl constr_expr_typel in fixpoint_exprl_with_new_bl let do_generate_principle_aux pconstants on_error register_built interactive_proof - (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Lemmas.t option = - List.iter (fun (_,l) -> if not (List.is_empty l) then error "Function does not support notations for now") fixpoint_exprl; + (fixpoint_exprl : Vernacexpr.fixpoint_expr list) : Lemmas.t option = + List.iter (fun { Vernacexpr.notations } -> + if not (List.is_empty notations) + then error "Function does not support notations for now") fixpoint_exprl; let lemma, _is_struct = match fixpoint_exprl with - | [((_,Some {CAst.v = Constrexpr.CWfRec (wf_x,wf_rel)},_,_,_),_) as fixpoint_expr] -> - let (((({CAst.v=name},pl),_,args,types,body)),_) as fixpoint_expr = - match recompute_binder_list [fixpoint_expr] with - | [e] -> e - | _ -> assert false - in - let fixpoint_exprl = [fixpoint_expr] in - let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in - let recdefs,rec_impls = build_newrecursive fixpoint_exprl in - let using_lemmas = [] in - let pre_hook pconstants = - generate_principle - (ref (Evd.from_env (Global.env ()))) - pconstants - on_error - true - register_built - fixpoint_exprl - recdefs - true - in - if register_built - then register_wf interactive_proof name rec_impls wf_rel wf_x.CAst.v using_lemmas args types body pre_hook, false - else None, false - |[((_,Some {CAst.v = Constrexpr.CMeasureRec(wf_x,wf_mes,wf_rel_opt)},_,_,_),_) as fixpoint_expr] -> - let (((({CAst.v=name},_),_,args,types,body)),_) as fixpoint_expr = - match recompute_binder_list [fixpoint_expr] with - | [e] -> e - | _ -> assert false - in - let fixpoint_exprl = [fixpoint_expr] in - let recdefs,rec_impls = build_newrecursive fixpoint_exprl in - let using_lemmas = [] in - let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in - let pre_hook pconstants = - generate_principle - (ref (Evd.from_env (Global.env ()))) - pconstants - on_error - true - register_built - fixpoint_exprl - recdefs - true - in - if register_built - then register_mes interactive_proof name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook, true - else None, true + | [{ Vernacexpr.rec_order = Some {CAst.v = Constrexpr.CWfRec (wf_x,wf_rel)} } as fixpoint_expr] -> + let { Vernacexpr.fname; univs; binders; rtype; body_def } as fixpoint_expr = + match recompute_binder_list [fixpoint_expr] with + | [e] -> e + | _ -> assert false + in + let fixpoint_exprl = [fixpoint_expr] in + let body = match body_def with + | Some body -> body + | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in + let recdefs,rec_impls = build_newrecursive fixpoint_exprl in + let using_lemmas = [] in + let pre_hook pconstants = + generate_principle + (ref (Evd.from_env (Global.env ()))) + pconstants + on_error + true + register_built + fixpoint_exprl + recdefs + true + in + if register_built + then register_wf interactive_proof fname rec_impls wf_rel wf_x.CAst.v using_lemmas binders rtype body pre_hook, false + else None, false + |[{ Vernacexpr.rec_order=Some {CAst.v = Constrexpr.CMeasureRec(wf_x,wf_mes,wf_rel_opt)} } as fixpoint_expr] -> + let { Vernacexpr.fname; univs; binders; rtype; body_def} as fixpoint_expr = + match recompute_binder_list [fixpoint_expr] with + | [e] -> e + | _ -> assert false + in + let fixpoint_exprl = [fixpoint_expr] in + let recdefs,rec_impls = build_newrecursive fixpoint_exprl in + let using_lemmas = [] in + let body = match body_def with + | Some body -> body + | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in + let pre_hook pconstants = + generate_principle + (ref (Evd.from_env (Global.env ()))) + pconstants + on_error + true + register_built + fixpoint_exprl + recdefs + true + in + if register_built + then register_mes interactive_proof fname rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas binders rtype body pre_hook, true + else None, true | _ -> - List.iter (function ((_na,ord,_args,_body,_type),_not) -> - match ord with - | Some { CAst.v = (Constrexpr.CMeasureRec _ | Constrexpr.CWfRec _) } -> - error - ("Cannot use mutual definition with well-founded recursion or measure") - | _ -> () + List.iter (function { Vernacexpr.rec_order } -> + match rec_order with + | Some { CAst.v = (Constrexpr.CMeasureRec _ | Constrexpr.CWfRec _) } -> + error + ("Cannot use mutual definition with well-founded recursion or measure") + | _ -> () ) fixpoint_exprl; let fixpoint_exprl = recompute_binder_list fixpoint_exprl in - let fix_names = - List.map (function ((({CAst.v=name},_),_,_,_,_),_) -> name) fixpoint_exprl - in + let fix_names = List.map (function { Vernacexpr.fname } -> fname.CAst.v) fixpoint_exprl in (* ok all the expressions are structural *) let recdefs,rec_impls = build_newrecursive fixpoint_exprl in let is_rec = List.exists (is_rec fix_names) recdefs in @@ -845,59 +853,59 @@ let make_graph (f_ref : GlobRef.t) = | None -> error "Cannot build a graph over an axiom!" | Some (body, _, _) -> let env = Global.env () in - let extern_body,extern_type = - with_full_print (fun () -> - (Constrextern.extern_constr false env sigma (EConstr.of_constr body), - Constrextern.extern_type false env sigma - (EConstr.of_constr (*FIXME*) c_body.const_type) - ) + let extern_body,extern_type = + with_full_print (fun () -> + (Constrextern.extern_constr false env sigma (EConstr.of_constr body), + Constrextern.extern_type false env sigma + (EConstr.of_constr (*FIXME*) c_body.const_type) ) - () - in - let (nal_tas,b,t) = get_args extern_body extern_type in - let expr_list = - match b.CAst.v with - | Constrexpr.CFix(l_id,fixexprl) -> - let l = - List.map - (fun (id,recexp,bl,t,b) -> - let { CAst.loc; v=rec_id } = match Option.get recexp with - | { CAst.v = CStructRec id } -> id - | { CAst.v = CWfRec (id,_) } -> id - | { CAst.v = CMeasureRec (oid,_,_) } -> Option.get oid - in - let new_args = - List.flatten - (List.map - (function - | Constrexpr.CLocalDef (na,_,_)-> [] - | Constrexpr.CLocalAssum (nal,_,_) -> - List.map - (fun {CAst.loc;v=n} -> CAst.make ?loc @@ - CRef(Libnames.qualid_of_ident ?loc @@ Nameops.Name.get_id n,None)) - nal - | Constrexpr.CLocalPattern _ -> assert false - ) - nal_tas - ) - in - let b' = add_args id.CAst.v new_args b in - ((((id,None), ( Some (CAst.make (CStructRec (CAst.make rec_id)))),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) - ) - fixexprl + ) () + in + let (nal_tas,b,t) = get_args extern_body extern_type in + let expr_list = + match b.CAst.v with + | Constrexpr.CFix(l_id,fixexprl) -> + let l = + List.map + (fun (id,recexp,bl,t,b) -> + let { CAst.loc; v=rec_id } = match Option.get recexp with + | { CAst.v = CStructRec id } -> id + | { CAst.v = CWfRec (id,_) } -> id + | { CAst.v = CMeasureRec (oid,_,_) } -> Option.get oid + in + let new_args = + List.flatten + (List.map + (function + | Constrexpr.CLocalDef (na,_,_)-> [] + | Constrexpr.CLocalAssum (nal,_,_) -> + List.map + (fun {CAst.loc;v=n} -> CAst.make ?loc @@ + CRef(Libnames.qualid_of_ident ?loc @@ Nameops.Name.get_id n,None)) + nal + | Constrexpr.CLocalPattern _ -> assert false + ) + nal_tas + ) in - l - | _ -> - let id = Label.to_id (Constant.label c) in - [((CAst.make id,None),None,nal_tas,t,Some b),[]] - in - let mp = Constant.modpath c in - let pstate = do_generate_principle_aux [c,Univ.Instance.empty] error_error false false expr_list in - assert (Option.is_empty pstate); - (* We register the infos *) - List.iter - (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make2 mp (Label.of_id id))) - expr_list) + let b' = add_args id.CAst.v new_args b in + { Vernacexpr.fname=id; univs=None + ; rec_order = Some (CAst.make (CStructRec (CAst.make rec_id))) + ; binders = nal_tas@bl; rtype=t; body_def=Some b'; notations = []} + ) fixexprl in + l + | _ -> + let fname = CAst.make (Label.to_id (Constant.label c)) in + [{ Vernacexpr.fname; univs=None; rec_order = None; binders=nal_tas; rtype=t; body_def=Some b; notations=[]}] + in + let mp = Constant.modpath c in + let pstate = do_generate_principle_aux [c,Univ.Instance.empty] error_error false false expr_list in + assert (Option.is_empty pstate); + (* We register the infos *) + List.iter + (fun { Vernacexpr.fname= {CAst.v=id} } -> + add_Function false (Constant.make2 mp (Label.of_id id))) + expr_list) (* *************** statically typed entrypoints ************************* *) diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index 3bc52272ac..bfc9686ae5 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -5,12 +5,9 @@ val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit -val do_generate_principle : - (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> unit +val do_generate_principle : Vernacexpr.fixpoint_expr list -> unit -val do_generate_principle_interactive : - (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> - Lemmas.t +val do_generate_principle_interactive : Vernacexpr.fixpoint_expr list -> Lemmas.t val functional_induction : bool -> diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 1e2b23bf96..21d61d1f97 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -17,7 +17,6 @@ open Genarg open Stdarg open Tacarg open Extraargs -open Pcoq.Prim open Pltac open Mod_subst open Names @@ -258,19 +257,8 @@ END open Autorewrite -let pr_orient _prc _prlc _prt = function - | true -> Pp.mt () - | false -> Pp.str " <-" - -let pr_orient_string _prc _prlc _prt (orient, s) = - pr_orient _prc _prlc _prt orient ++ Pp.spc () ++ Pp.str s - } -ARGUMENT EXTEND orient_string TYPED AS (bool * string) PRINTED BY { pr_orient_string } -| [ orient(r) preident(i) ] -> { r, i } -END - TACTIC EXTEND autorewrite | [ "autorewrite" "with" ne_preident_list(l) clause(cl) ] -> { auto_multi_rewrite l ( cl) } diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index c09250ade5..962730d8dc 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -385,7 +385,6 @@ open Pltac ARGUMENT EXTEND ssrindex PRINTED BY { pr_ssrindex } INTERPRETED BY { interp_index } -| [ int_or_var(i) ] -> { mk_index ~loc i } END @@ -523,7 +522,6 @@ ARGUMENT EXTEND ssrterm GLOBALIZED BY { glob_ssrterm } SUBSTITUTED BY { subst_ssrterm } RAW_PRINTED BY { pr_ssrterm } GLOB_PRINTED BY { pr_ssrterm } -| [ "YouShouldNotTypeThis" constr(c) ] -> { mk_lterm c } END GRAMMAR EXTEND Gram @@ -570,7 +568,6 @@ let pr_ssrbwdview _ _ _ = pr_view ARGUMENT EXTEND ssrbwdview TYPED AS ssrterm list PRINTED BY { pr_ssrbwdview } -| [ "YouShouldNotTypeThis" ] -> { [] } END (* Pcoq *) @@ -594,7 +591,6 @@ let pr_ssrfwdview _ _ _ = pr_view2 ARGUMENT EXTEND ssrfwdview TYPED AS ast_closure_term list PRINTED BY { pr_ssrfwdview } -| [ "YouShouldNotTypeThis" ] -> { [] } END (* Pcoq *) @@ -762,7 +758,6 @@ let test_ident_no_do = } ARGUMENT EXTEND ident_no_do PRINTED BY { fun _ _ _ -> Names.Id.print } -| [ "YouShouldNotTypeThis" ident(id) ] -> { id } END @@ -857,7 +852,6 @@ let _test_nobinder = Pcoq.Entry.of_parser "test_nobinder" (reject_binder false 0 } ARGUMENT EXTEND ssrcpat TYPED AS ssripatrep PRINTED BY { pr_ssripat } - | [ "YouShouldNotTypeThis" ssriorpat(x) ] -> { IPatCase(Regular x) } END (* Pcoq *) @@ -985,7 +979,6 @@ let pr_ssrintrosarg env sigma _ _ prt (tac, ipats) = ARGUMENT EXTEND ssrintrosarg TYPED AS (tactic * ssrintros) PRINTED BY { pr_ssrintrosarg env sigma } -| [ "YouShouldNotTypeThis" ssrtacarg(arg) ssrintros_ne(ipats) ] -> { arg, ipats } END { @@ -1711,14 +1704,6 @@ let _ = add_internal_name (is_tagged perm_tag) (** Tactical extensions. *) -(* The TACTIC EXTEND facility can't be used for defining new user *) -(* tacticals, because: *) -(* - the concrete syntax must start with a fixed string *) -(* We use the following workaround: *) -(* - We use the (unparsable) "YouShouldNotTypeThis" token for tacticals that *) -(* don't start with a token, then redefine the grammar and *) -(* printer using GEXTEND and set_pr_ssrtac, respectively. *) - { type ssrargfmt = ArgSsr of string | ArgSep of string @@ -2243,8 +2228,6 @@ END (** The "congr" tactic *) -(* type ssrcongrarg = open_constr * (int * constr) *) - { let pr_ssrcongrarg _ _ _ ((n, f), dgens) = diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 649b51cb0e..66db924051 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -101,10 +101,11 @@ let bigint_of_z c = match DAst.get c with let rdefinitions = ["Coq";"Reals";"Rdefinitions"] let r_modpath = MPfile (make_dir rdefinitions) +let r_base_modpath = MPdot (r_modpath, Label.make "RbaseSymbolsImpl") let r_path = make_path rdefinitions "R" let glob_IZR = GlobRef.ConstRef (Constant.make2 r_modpath @@ Label.make "IZR") -let glob_Rmult = GlobRef.ConstRef (Constant.make2 r_modpath @@ Label.make "Rmult") +let glob_Rmult = GlobRef.ConstRef (Constant.make2 r_base_modpath @@ Label.make "Rmult") let glob_Rdiv = GlobRef.ConstRef (Constant.make2 r_modpath @@ Label.make "Rdiv") let binintdef = ["Coq";"ZArith";"BinIntDef"] |