diff options
Diffstat (limited to 'plugins')
27 files changed, 291 insertions, 242 deletions
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 7bddbc994f..d38c3c869b 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -39,7 +39,7 @@ let build_newrecursive lnameargsardef = List.fold_left (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 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 binders in let impl = Constrintern.compute_internalization_data env0 evd Constrintern.Recursive arity impls' in @@ -164,7 +164,7 @@ let prepare_body { Vernacexpr.binders } rt = let fun_args,rt' = chop_rlambda_n n rt in (fun_args,rt') -let build_functional_principle ?(opaque=Proof_global.Transparent) (evd:Evd.evar_map ref) interactive_proof old_princ_type sorts funs i proof_tac hook = +let build_functional_principle ?(opaque=Proof_global.Transparent) (evd:Evd.evar_map ref) old_princ_type sorts funs _i proof_tac hook = (* First we get the type of the old graph principle *) let mutr_nparams = (Tactics.compute_elim_sig !evd (EConstr.of_constr old_princ_type)).Tactics.nparams in (* let time1 = System.get_time () in *) @@ -199,7 +199,7 @@ let build_functional_principle ?(opaque=Proof_global.Transparent) (evd:Evd.evar_ (* end; *) let open Proof_global in - let { name; entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x)) lemma in + let { entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false) lemma in match entries with | [entry] -> entry, hook @@ -235,7 +235,6 @@ let change_property_sort evd toSort princ princName = (List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) princ_info.Tactics.params) let generate_functional_principle (evd: Evd.evar_map ref) - interactive_proof old_princ_type sorts new_princ_name funs i proof_tac = try @@ -283,26 +282,25 @@ let generate_functional_principle (evd: Evd.evar_map ref) register_with_sort Sorts.InSet in let entry, hook = - build_functional_principle evd interactive_proof old_princ_type new_sorts funs i + build_functional_principle evd old_princ_type new_sorts funs i proof_tac hook in (* Pr 1278 : Don't forget to close the goal if an error is raised !!!! *) let uctx = Evd.evar_universe_context sigma in - let hook_data = hook, uctx, [] in - let _ : Names.GlobRef.t = DeclareDef.declare_definition - ~name:new_princ_name ~hook_data + let _ : Names.GlobRef.t = DeclareDef.declare_entry + ~name:new_princ_name ~hook ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:Decls.(IsProof Theorem) - UnivNames.empty_binders - entry [] in + ~impargs:[] + ~uctx entry in () with e when CErrors.noncritical e -> raise (Defining_principle e) let generate_principle (evd:Evd.evar_map ref) pconstants on_error - is_general do_built fix_rec_l recdefs interactive_proof + is_general do_built fix_rec_l recdefs (continue_proof : int -> Names.Constant.t array -> EConstr.constr array -> int -> Tacmach.tactic) : unit = let names = List.map (function { Vernacexpr.fname = {CAst.v=name} } -> name) fix_rec_l in @@ -335,7 +333,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error let funs_kn = Array.of_list (List.map fname_kn fix_rec_l) in let _ = List.map_i - (fun i x -> + (fun i _x -> let env = Global.env () in let princ = Indrec.lookup_eliminator env (ind_kn,i) (Sorts.InProp) in let evd = ref (Evd.from_env env) in @@ -346,7 +344,6 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error let princ_type = EConstr.Unsafe.to_constr princ_type in generate_functional_principle evd - interactive_proof princ_type None None @@ -374,7 +371,6 @@ let register_struct is_rec fixpoint_exprl = | None -> CErrors.user_err ~hdr:"Function" Pp.(str "Body of Function must be given") in ComDefinition.do_definition - ~program_mode:false ~name:fname.CAst.v ~poly:false ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) @@ -412,7 +408,7 @@ let register_struct is_rec fixpoint_exprl = None,evd,List.rev rev_pconstants let generate_correction_proof_wf f_ref tcc_lemma_ref - is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation + is_mes functional_ref eq_ref rec_arg_num rec_arg_type relation (_: int) (_:Names.Constant.t array) (_:EConstr.constr array) (_:int) : Tacmach.tactic = Functional_principles_proofs.prove_principle_for_gen (f_ref,functional_ref,eq_ref) @@ -430,7 +426,7 @@ let generate_correction_proof_wf f_ref tcc_lemma_ref res = fv \rightarrow graph\ x_1\ldots x_n\ res\] decomposed as the context and the conclusion *) -let generate_type evd g_to_f f graph i = +let generate_type evd g_to_f f graph = let open Context.Rel.Declaration in let open EConstr in let open EConstr.Vars in @@ -498,7 +494,7 @@ let generate_type evd g_to_f f graph i = WARNING: while convertible, [type_of body] and [type] can be non equal *) let find_induction_principle evd f = - let f_as_constant,u = match EConstr.kind !evd f with + let f_as_constant, _u = match EConstr.kind !evd f with | Constr.Const c' -> c' | _ -> CErrors.user_err Pp.(str "Must be used with a function") in @@ -545,7 +541,7 @@ let rec generate_fresh_id x avoid i = let id = Namegen.next_ident_away_in_goal x (Id.Set.of_list avoid) in id::(generate_fresh_id x (id::avoid) (pred i)) -let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i : Tacmach.tactic = +let prove_fun_correct evd graphs_constr schemes lemmas_types_infos i : Tacmach.tactic = let open Constr in let open EConstr in let open Context.Rel.Declaration in @@ -1140,7 +1136,7 @@ let get_funs_constant mp = to prevent Reset strange thing *) let l_bodies = List.map find_constant_body (Array.to_list (Array.map fst l_const)) in - let l_params,l_fixes = List.split (List.map Term.decompose_lam l_bodies) in + let l_params, _l_fixes = List.split (List.map Term.decompose_lam l_bodies) in (* all the parameters must be equal*) let _check_params = let first_params = List.hd l_params in @@ -1240,7 +1236,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef in let entry, _hook = try - build_functional_principle ~opaque evd false + build_functional_principle ~opaque evd first_type (Array.of_list sorts) this_block_funs @@ -1261,7 +1257,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef let sorts = Array.of_list sorts in List.map (Functional_principles_types.compute_new_princ_type_from_rel funs sorts) other_princ_types in - let first_princ_body,first_princ_type = Declare.(entry.proof_entry_body, entry.proof_entry_type) in + let first_princ_body = entry.Declare.proof_entry_body in let ctxt,fix = Term.decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*) let (idxs,_),(_,ta,_ as decl) = Constr.destFix fix in let other_result = @@ -1291,7 +1287,6 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef let entry, _hook = build_functional_principle evd - false (List.nth other_princ_types (!i - 1)) (Array.of_list sorts) this_block_funs @@ -1330,9 +1325,8 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) = let lemmas_types_infos = Util.Array.map2_i (fun i f_constr graph -> - (* let const_of_f,u = destConst f_constr in *) let (type_of_lemma_ctxt,type_of_lemma_concl,graph) = - generate_type evd false f_constr graph i + generate_type evd false f_constr graph in let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in graphs_constr.(i) <- graph; @@ -1367,7 +1361,7 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) = ) in let proving_tac = - prove_fun_correct !evd funs_constr graphs_constr schemes lemmas_types_infos + prove_fun_correct !evd graphs_constr schemes lemmas_types_infos in Array.iteri (fun i f_as_constant -> @@ -1397,8 +1391,8 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) = let lemmas_types_infos = Util.Array.map2_i (fun i f_constr graph -> - let (type_of_lemma_ctxt,type_of_lemma_concl,graph) = - generate_type evd true f_constr graph i + let (type_of_lemma_ctxt,type_of_lemma_concl,graph) = + generate_type evd true f_constr graph in let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in graphs_constr.(i) <- graph; @@ -1414,7 +1408,7 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) = in let (kn,_) as graph_ind,u = (destInd !evd graphs_constr.(0)) in - let mib,mip = Global.lookup_inductive graph_ind in + let mib, _mip = Global.lookup_inductive graph_ind in let sigma, scheme = (Indrec.build_mutual_induction_scheme (Global.env ()) !evd (Array.to_list @@ -1484,7 +1478,7 @@ let derive_inversion fix_names = *) List.iter (fun c -> ignore (find_Function_infos (fst c))) fix_names_as_constant ; try - let evd', lind = + let _evd', lind = List.fold_right (fun id (evd,l) -> let evd,id = @@ -1535,11 +1529,11 @@ let register_wf interactive_proof ?(is_mes=false) fname rec_impls wf_rel_expr wf in let eq = Constrexpr_ops.mkCProdN args unbounded_eq in let hook ((f_ref,_) as fconst) tcc_lemma_ref (functional_ref,_) (eq_ref,_) rec_arg_num rec_arg_type - nb_args relation = + _nb_args relation = try pre_hook [fconst] (generate_correction_proof_wf f_ref tcc_lemma_ref is_mes - functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation + functional_ref eq_ref rec_arg_num rec_arg_type relation ); derive_inversion [fname] with e when CErrors.noncritical e -> @@ -1561,7 +1555,7 @@ let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt w | None -> begin match args with - | [Constrexpr.CLocalAssum ([{CAst.v=Name x}],k,t)] -> t,x + | [Constrexpr.CLocalAssum ([{CAst.v=Name x}],_k,t)] -> t,x | _ -> CErrors.user_err (Pp.str "Recursive argument must be specified") end | Some wf_args -> @@ -1569,7 +1563,7 @@ let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt w match List.find (function - | Constrexpr.CLocalAssum(l,k,t) -> + | Constrexpr.CLocalAssum(l,_k,t) -> List.exists (function {CAst.v=Name id} -> Id.equal id wf_args | _ -> false) l @@ -1577,7 +1571,7 @@ let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt w ) args with - | Constrexpr.CLocalAssum(_,k,t) -> t,wf_args + | Constrexpr.CLocalAssum(_,_k,t) -> t,wf_args | _ -> assert false with Not_found -> assert false in @@ -1625,7 +1619,7 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro let lemma, _is_struct = match fixpoint_exprl with | [{ 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 = + let { Vernacexpr.fname; univs = _; binders; rtype; body_def } as fixpoint_expr = match recompute_binder_list [fixpoint_expr] with | [e] -> e | _ -> assert false @@ -1644,13 +1638,12 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro register_built fixpoint_exprl recdefs - true in if register_built then register_wf interactive_proof fname.CAst.v 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 = + let { Vernacexpr.fname; univs = _; binders; rtype; body_def} as fixpoint_expr = match recompute_binder_list [fixpoint_expr] with | [e] -> e | _ -> assert false @@ -1671,7 +1664,6 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro register_built fixpoint_exprl recdefs - true in if register_built then register_mes interactive_proof fname.CAst.v rec_impls wf_mes wf_rel_opt @@ -1689,7 +1681,7 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro let fixpoint_exprl = recompute_binder_list 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 recdefs, _rec_impls = build_newrecursive fixpoint_exprl in let is_rec = List.exists (is_rec fix_names) recdefs in let lemma,evd,pconstants = if register_built @@ -1705,7 +1697,6 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro register_built fixpoint_exprl recdefs - interactive_proof (Functional_principles_proofs.prove_princ_for_struct evd interactive_proof); if register_built then begin derive_inversion fix_names; end; @@ -2066,7 +2057,6 @@ let build_case_scheme fa = *) generate_functional_principle (ref (Evd.from_env (Global.env ()))) - false scheme_type (Some ([|sorts|])) (Some princ_name) diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 9b80cbd803..7b1aa7a07a 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -47,7 +47,7 @@ DECLARE PLUGIN "ltac_plugin" let with_delayed_uconstr ist c tac = let flags = { - Pretyping.use_typeclasses = false; + Pretyping.use_typeclasses = Pretyping.NoUseTC; solve_unification_constraints = true; fail_evar = false; expand_evars = true; @@ -345,7 +345,7 @@ open EConstr open Vars let constr_flags () = { - Pretyping.use_typeclasses = true; + Pretyping.use_typeclasses = Pretyping.UseTC; Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics (); Pretyping.fail_evar = false; Pretyping.expand_evars = true; @@ -375,22 +375,22 @@ let refine_tac ist simple with_classes c = TACTIC EXTEND refine | [ "refine" uconstr(c) ] -> - { refine_tac ist false true c } + { refine_tac ist false Pretyping.UseTC c } END TACTIC EXTEND simple_refine | [ "simple" "refine" uconstr(c) ] -> - { refine_tac ist true true c } + { refine_tac ist true Pretyping.UseTC c } END TACTIC EXTEND notcs_refine | [ "notypeclasses" "refine" uconstr(c) ] -> - { refine_tac ist false false c } + { refine_tac ist false Pretyping.NoUseTC c } END TACTIC EXTEND notcs_simple_refine | [ "simple" "notypeclasses" "refine" uconstr(c) ] -> - { refine_tac ist true false c } + { refine_tac ist true Pretyping.NoUseTC c } END (* Solve unification constraints using heuristics or fail if any remain *) diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index 3c30c881fb..b4527694ae 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -53,7 +53,7 @@ END let eval_uconstrs ist cs = let flags = { - Pretyping.use_typeclasses = false; + Pretyping.use_typeclasses = Pretyping.NoUseTC; solve_unification_constraints = true; fail_evar = false; expand_evars = true; diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 5bfbe7a49a..6a158bde17 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -125,7 +125,7 @@ let destruction_arg_of_constr (c,lbind as clbind) = match lbind with | _ -> ElimOnConstr clbind let mkNumeral n = - Numeral ((if 0<=n then SPlus else SMinus),NumTok.int (string_of_int (abs n))) + Numeral (NumTok.Signed.of_int_string (string_of_int n)) let mkTacCase with_evar = function | [(clear,ElimOnConstr cl),(None,None),None],None -> @@ -185,10 +185,6 @@ let merge_occurrences loc cl = function in (Some p, ans) -let warn_deprecated_eqn_syntax = - CWarnings.create ~name:"deprecated-eqn-syntax" ~category:"deprecated" - (fun arg -> strbrk (Printf.sprintf "Syntax \"_eqn:%s\" is deprecated. Please use \"eqn:%s\" instead." arg arg)) - (* Auxiliary grammar rules *) open Pvernac.Vernac_ @@ -461,10 +457,6 @@ GRAMMAR EXTEND Gram ; eqn_ipat: [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> { Some (CAst.make ~loc pat) } - | IDENT "_eqn"; ":"; pat = naming_intropattern -> - { warn_deprecated_eqn_syntax ~loc "H"; Some (CAst.make ~loc pat) } - | IDENT "_eqn" -> - { warn_deprecated_eqn_syntax ~loc "?"; Some (CAst.make ~loc IntroAnonymous) } | -> { None } ] ] ; as_name: diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 4af5699317..4127d28bae 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -44,11 +44,11 @@ let coincide s pat off = !break let atactic n = - if n = 5 then Aentry Pltac.binder_tactic - else Aentryl (Pltac.tactic_expr, string_of_int n) + if n = 5 then Pcoq.Symbol.nterm Pltac.binder_tactic + else Pcoq.Symbol.nterml Pltac.tactic_expr (string_of_int n) type entry_name = EntryName : - 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Extend.symbol -> entry_name + 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Pcoq.Symbol.t -> entry_name (** Quite ad-hoc *) let get_tacentry n m = @@ -57,8 +57,8 @@ let get_tacentry n m = && not (Int.equal m 5) (* Because tactic5 is at binder_tactic *) && not (Int.equal m 0) (* Because tactic0 is at simple_tactic *) in - if check_lvl n then EntryName (rawwit Tacarg.wit_tactic, Aself) - else if check_lvl (n + 1) then EntryName (rawwit Tacarg.wit_tactic, Anext) + if check_lvl n then EntryName (rawwit Tacarg.wit_tactic, Pcoq.Symbol.self) + else if check_lvl (n + 1) then EntryName (rawwit Tacarg.wit_tactic, Pcoq.Symbol.next) else EntryName (rawwit Tacarg.wit_tactic, atactic n) let get_separator = function @@ -140,23 +140,23 @@ let head_is_ident tg = match tg.tacgram_prods with let rec prod_item_of_symbol lev = function | Extend.Ulist1 s -> let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in - EntryName (Rawwit (ListArg typ), Alist1 e) + EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list1 e) | Extend.Ulist0 s -> let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in - EntryName (Rawwit (ListArg typ), Alist0 e) + EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list0 e) | Extend.Ulist1sep (s, sep) -> let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in - EntryName (Rawwit (ListArg typ), Alist1sep (e, Atoken (CLexer.terminal sep))) + EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list1sep e (Pcoq.Symbol.token (CLexer.terminal sep)) false) | Extend.Ulist0sep (s, sep) -> let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in - EntryName (Rawwit (ListArg typ), Alist0sep (e, Atoken (CLexer.terminal sep))) + EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list0sep e (Pcoq.Symbol.token (CLexer.terminal sep)) false) | Extend.Uopt s -> let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in - EntryName (Rawwit (OptArg typ), Aopt e) + EntryName (Rawwit (OptArg typ), Pcoq.Symbol.opt e) | Extend.Uentry arg -> let ArgT.Any tag = arg in let wit = ExtraArg tag in - EntryName (Rawwit wit, Extend.Aentry (genarg_grammar wit)) + EntryName (Rawwit wit, Pcoq.Symbol.nterm (genarg_grammar wit)) | Extend.Uentryl (s, n) -> let ArgT.Any tag = s in assert (coincide (ArgT.repr tag) "tactic" 0); @@ -191,7 +191,7 @@ let add_tactic_entry (kn, ml, tg) state = in let prods = List.map map tg.tacgram_prods in let rules = make_rule mkact prods in - let r = ExtendRule (entry, (pos, [(None, None, [rules])])) in + let r = ExtendRule (entry, { pos; data=[(None, None, [rules])]}) in ([r], state) let tactic_grammar = @@ -399,23 +399,29 @@ let create_ltac_quotation name cast (e, l) = in let () = ltac_quotations := String.Set.add name !ltac_quotations in let entry = match l with - | None -> Aentry e - | Some l -> Aentryl (e, string_of_int l) + | None -> Pcoq.Symbol.nterm e + | Some l -> Pcoq.Symbol.nterml e (string_of_int l) in (* let level = Some "1" in *) let level = None in let assoc = None in let rule = - Next (Next (Next (Next (Next (Stop, - Atoken (CLexer.terminal name)), - Atoken (CLexer.terminal ":")), - Atoken (CLexer.terminal "(")), - entry), - Atoken (CLexer.terminal ")")) + Pcoq.( + Rule.next + (Rule.next + (Rule.next + (Rule.next + (Rule.next + Rule.stop + (Symbol.token (CLexer.terminal name))) + (Symbol.token (CLexer.terminal ":"))) + (Symbol.token (CLexer.terminal "("))) + entry) + (Symbol.token (CLexer.terminal ")"))) in let action _ v _ _ _ loc = cast (Some loc, v) in - let gram = (level, assoc, [Rule (rule, action)]) in - Pcoq.grammar_extend Pltac.tactic_arg (None, [gram]) + let gram = (level, assoc, [Pcoq.Production.make rule action]) in + Pcoq.grammar_extend Pltac.tactic_arg {pos=None; data=[gram]} (** Command *) @@ -759,7 +765,7 @@ let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) = e | Vernacextend.Arg_rules rules -> let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in - let () = Pcoq.grammar_extend e (None, [(None, None, rules)]) in + let () = Pcoq.grammar_extend e {pos=None; data=[(None, None, rules)]} in e in let (rpr, gpr, tpr) = arg.arg_printer in diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 9e0b9d3254..b0e26e1def 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -546,7 +546,7 @@ let interp_gen kind ist pattern_mode flags env sigma c = (evd,c) let constr_flags () = { - use_typeclasses = true; + use_typeclasses = UseTC; solve_unification_constraints = true; fail_evar = true; expand_evars = true; @@ -564,7 +564,7 @@ let interp_constr = interp_constr_gen WithoutTypeConstraint let interp_type = interp_constr_gen IsType let open_constr_use_classes_flags () = { - use_typeclasses = true; + use_typeclasses = UseTC; solve_unification_constraints = true; fail_evar = false; expand_evars = true; @@ -573,7 +573,7 @@ let open_constr_use_classes_flags () = { } let open_constr_no_classes_flags () = { - use_typeclasses = false; + use_typeclasses = NoUseTC; solve_unification_constraints = true; fail_evar = false; expand_evars = true; @@ -582,7 +582,7 @@ let open_constr_no_classes_flags () = { } let pure_open_constr_flags = { - use_typeclasses = false; + use_typeclasses = NoUseTC; solve_unification_constraints = true; fail_evar = false; expand_evars = false; diff --git a/plugins/ltac/tactic_option.ml b/plugins/ltac/tactic_option.ml index c72a527537..4f00f17892 100644 --- a/plugins/ltac/tactic_option.ml +++ b/plugins/ltac/tactic_option.ml @@ -13,15 +13,11 @@ open Pp let declare_tactic_option ?(default=Tacexpr.TacId []) name = let locality = Summary.ref false ~name:(name^"-locality") in - let default_tactic_expr : Tacexpr.glob_tactic_expr ref = - Summary.ref default ~name:(name^"-default-tacexpr") - in let default_tactic : Tacexpr.glob_tactic_expr ref = - Summary.ref !default_tactic_expr ~name:(name^"-default-tactic") + Summary.ref default ~name:(name^"-default-tactic") in let set_default_tactic local t = locality := local; - default_tactic_expr := t; default_tactic := t in let cache (_, (local, tac)) = set_default_tactic local tac in @@ -42,12 +38,11 @@ let declare_tactic_option ?(default=Tacexpr.TacId []) name = subst_function = subst} in let put local tac = - set_default_tactic local tac; Lib.add_anonymous_leaf (input (local, tac)) in let get () = !locality, Tacinterp.eval_tactic !default_tactic in let print () = - Pptactic.pr_glob_tactic (Global.env ()) !default_tactic_expr ++ + Pptactic.pr_glob_tactic (Global.env ()) !default_tactic ++ (if !locality then str" (locally defined)" else str" (globally defined)") in put, get, print diff --git a/plugins/micromega/.ocamlformat b/plugins/micromega/.ocamlformat new file mode 100644 index 0000000000..a22a2ff88c --- /dev/null +++ b/plugins/micromega/.ocamlformat @@ -0,0 +1 @@ +disable=false diff --git a/plugins/micromega/.ocamlformat-ignore b/plugins/micromega/.ocamlformat-ignore new file mode 100644 index 0000000000..157a987754 --- /dev/null +++ b/plugins/micromega/.ocamlformat-ignore @@ -0,0 +1 @@ +micromega.ml diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 824abdaf89..1958fff4cc 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -651,10 +651,10 @@ let z_cert_of_pos pos = in simplify_cone z_spec (_cert_of_pos pos) -open Mutils (** All constraints (initial or derived) have an index and have a justification i.e., proof. Given a constraint, all the coefficients are always integers. *) +open Mutils open Polynomial diff --git a/plugins/micromega/certificate.mli b/plugins/micromega/certificate.mli index d8c9ade04d..cabd36ebb7 100644 --- a/plugins/micromega/certificate.mli +++ b/plugins/micromega/certificate.mli @@ -10,36 +10,36 @@ module Mc = Micromega -val use_simplex : bool ref (** [use_simplex] is bound to the Coq option Simplex. If set, use the Simplex method, otherwise use Fourier *) +val use_simplex : bool ref type ('prf, 'model) res = Prf of 'prf | Model of 'model | Unknown type zres = (Mc.zArithProof, int * Mc.z list) res type qres = (Mc.q Mc.psatz, int * Mc.q list) res -val dump_file : string option ref (** [dump_file] is bound to the Coq option Dump Arith. If set to some [file], arithmetic goals are dumped in filexxx.v *) +val dump_file : string option ref -val q_cert_of_pos : Sos_types.positivstellensatz -> Mc.q Mc.psatz (** [q_cert_of_pos prf] converts a Sos proof into a rational Coq proof *) +val q_cert_of_pos : Sos_types.positivstellensatz -> Mc.q Mc.psatz -val z_cert_of_pos : Sos_types.positivstellensatz -> Mc.z Mc.psatz (** [z_cert_of_pos prf] converts a Sos proof into an integer Coq proof *) +val z_cert_of_pos : Sos_types.positivstellensatz -> Mc.z Mc.psatz -val lia : bool -> int -> (Mc.z Mc.pExpr * Mc.op1) list -> zres (** [lia enum depth sys] generates an unsat proof for the linear constraints in [sys]. If the Simplex option is set, any failure to find a proof should be considered as a bug. *) +val lia : bool -> int -> (Mc.z Mc.pExpr * Mc.op1) list -> zres -val nlia : bool -> int -> (Mc.z Mc.pExpr * Mc.op1) list -> zres (** [nlia enum depth sys] generates an unsat proof for the non-linear constraints in [sys]. The solver is incomplete -- the problem is undecidable *) +val nlia : bool -> int -> (Mc.z Mc.pExpr * Mc.op1) list -> zres -val linear_prover_with_cert : int -> (Mc.q Mc.pExpr * Mc.op1) list -> qres (** [linear_prover_with_cert depth sys] generates an unsat proof for the linear constraints in [sys]. Over the rationals, the solver is complete. *) +val linear_prover_with_cert : int -> (Mc.q Mc.pExpr * Mc.op1) list -> qres -val nlinear_prover : int -> (Mc.q Mc.pExpr * Mc.op1) list -> qres (** [nlinear depth sys] generates an unsat proof for the non-linear constraints in [sys]. The solver is incompete -- the problem is decidable. *) +val nlinear_prover : int -> (Mc.q Mc.pExpr * Mc.op1) list -> qres diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 82f8b5b3e2..43f6f5a35e 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1476,6 +1476,9 @@ let parse_goal gl parse_arith (env : Env.t) hyps term = let lhyps, env, tg = parse_hyps gl parse_arith env tg hyps in (lhyps, f, env) +(** + * The datastructures that aggregate theory-dependent proof values. + *) type ('synt_c, 'prf) domain_spec = { typ : EConstr.constr ; (* is the type of the interpretation domain - Z, Q, R*) @@ -1485,9 +1488,6 @@ type ('synt_c, 'prf) domain_spec = ; proof_typ : EConstr.constr ; dump_proof : 'prf -> EConstr.constr ; coeff_eq : 'synt_c -> 'synt_c -> bool } -(** - * The datastructures that aggregate theory-dependent proof values. - *) let zz_domain_spec = lazy diff --git a/plugins/micromega/coq_micromega.mli b/plugins/micromega/coq_micromega.mli index f2f7fd424f..679290891d 100644 --- a/plugins/micromega/coq_micromega.mli +++ b/plugins/micromega/coq_micromega.mli @@ -24,5 +24,5 @@ val print_lia_profile : unit -> unit (** {5 Use Micromega independently from tactics. } *) -val dump_proof_term : Micromega.zArithProof -> EConstr.t (** [dump_proof_term] generates the Coq representation of a Micromega proof witness *) +val dump_proof_term : Micromega.zArithProof -> EConstr.t diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml index 5ed7d9865e..3d1770a541 100644 --- a/plugins/micromega/mfourier.ml +++ b/plugins/micromega/mfourier.ml @@ -17,8 +17,8 @@ open Vect let debug = false let compare_float (p : float) q = pervasives_compare p q -open Itv (** Implementation of intervals *) +open Itv type vector = Vect.t @@ -47,8 +47,8 @@ and cstr_info = {bound : interval; prf : proof; pos : int; neg : int} [v] is an upper-bound of the set of variables which appear in [s]. *) -exception SystemContradiction of proof (** To be thrown when a system has no solution *) +exception SystemContradiction of proof (** Pretty printing *) let rec pp_proof o prf = diff --git a/plugins/micromega/mutils.mli b/plugins/micromega/mutils.mli index 146860ca00..09d55cf073 100644 --- a/plugins/micromega/mutils.mli +++ b/plugins/micromega/mutils.mli @@ -26,8 +26,8 @@ end module IMap : sig include Map.S with type key = int - val from : key -> 'elt t -> 'elt t (** [from k m] returns the submap of [m] with keys greater or equal k *) + val from : key -> 'elt t -> 'elt t end module Cmp : sig diff --git a/plugins/micromega/persistent_cache.mli b/plugins/micromega/persistent_cache.mli index 16d3f0a517..08e8c53757 100644 --- a/plugins/micromega/persistent_cache.mli +++ b/plugins/micromega/persistent_cache.mli @@ -14,25 +14,25 @@ module type PHashtable = sig type 'a t type key - val open_in : string -> 'a t (** [open_in f] rebuilds a table from the records stored in file [f]. As marshaling is not type-safe, it might segfault. *) + val open_in : string -> 'a t - val find : 'a t -> key -> 'a (** find has the specification of Hashtable.find *) + val find : 'a t -> key -> 'a - val add : 'a t -> key -> 'a -> unit (** [add tbl key elem] adds the binding [key] [elem] to the table [tbl]. (and writes the binding to the file associated with [tbl].) If [key] is already bound, raises KeyAlreadyBound *) + val add : 'a t -> key -> 'a -> unit - val memo : string -> (key -> 'a) -> key -> 'a (** [memo cache f] returns a memo function for [f] using file [cache] as persistent table. Note that the cache will only be loaded when the function is used for the first time *) + val memo : string -> (key -> 'a) -> key -> 'a - val memo_cond : string -> (key -> bool) -> (key -> 'a) -> key -> 'a (** [memo cache cond f] only use the cache if [cond k] holds for the key [k]. *) + val memo_cond : string -> (key -> bool) -> (key -> 'a) -> key -> 'a end module PHashtable (Key : HashedType) : PHashtable with type key = Key.t diff --git a/plugins/micromega/polynomial.mli b/plugins/micromega/polynomial.mli index bdd77440bb..9c09f76691 100644 --- a/plugins/micromega/polynomial.mli +++ b/plugins/micromega/polynomial.mli @@ -17,52 +17,52 @@ val max_nb_cstr : int ref type var = int module Monomial : sig - type t (** A monomial is represented by a multiset of variables *) + type t - val fold : (var -> int -> 'a -> 'a) -> t -> 'a -> 'a (** [fold f m acc] folds over the variables with multiplicities *) + val fold : (var -> int -> 'a -> 'a) -> t -> 'a -> 'a - val degree : t -> int (** [degree m] is the sum of the degrees of each variable *) + val degree : t -> int - val const : t (** [const] @return the empty monomial i.e. without any variable *) + val const : t val is_const : t -> bool - val var : var -> t (** [var x] @return the monomial x^1 *) + val var : var -> t - val prod : t -> t -> t (** [prod n m] @return the monomial n*m *) + val prod : t -> t -> t - val sqrt : t -> t option (** [sqrt m] @return [Some r] iff r^2 = m *) + val sqrt : t -> t option - val is_var : t -> bool (** [is_var m] @return [true] iff m = x^1 for some variable x *) + val is_var : t -> bool - val get_var : t -> var option (** [get_var m] @return [x] iff m = x^1 for variable x *) + val get_var : t -> var option - val div : t -> t -> t * int (** [div m1 m2] @return a pair [mr,n] such that mr * (m2)^n = m1 where n is maximum *) + val div : t -> t -> t * int - val compare : t -> t -> int (** [compare m1 m2] provides a total order over monomials*) + val compare : t -> t -> int - val variables : t -> ISet.t (** [variables m] @return the set of variables with (strictly) positive multiplicities *) + val variables : t -> ISet.t end module MonMap : sig @@ -82,36 +82,36 @@ module Poly : sig type t - val constant : Q.t -> t (** [constant c] @return the constant polynomial c *) + val constant : Q.t -> t - val variable : var -> t (** [variable x] @return the polynomial 1.x^1 *) + val variable : var -> t - val addition : t -> t -> t (** [addition p1 p2] @return the polynomial p1+p2 *) + val addition : t -> t -> t - val product : t -> t -> t (** [product p1 p2] @return the polynomial p1*p2 *) + val product : t -> t -> t - val uminus : t -> t (** [uminus p] @return the polynomial -p i.e product by -1 *) + val uminus : t -> t - val get : Monomial.t -> t -> Q.t (** [get mi p] @return the coefficient ai of the monomial mi. *) + val get : Monomial.t -> t -> Q.t - val fold : (Monomial.t -> Q.t -> 'a -> 'a) -> t -> 'a -> 'a (** [fold f p a] folds f over the monomials of p with non-zero coefficient *) + val fold : (Monomial.t -> Q.t -> 'a -> 'a) -> t -> 'a -> 'a - val add : Monomial.t -> Q.t -> t -> t (** [add m n p] @return the polynomial n*m + p *) + val add : Monomial.t -> Q.t -> t -> t end type cstr = {coeffs : Vect.t; op : op; cst : Q.t} @@ -125,9 +125,9 @@ val eval_op : op -> Q.t -> Q.t -> bool val opAdd : op -> op -> op -val is_strict : cstr -> bool (** [is_strict c] @return whether the constraint is strict i.e. c.op = Gt *) +val is_strict : cstr -> bool exception Strict @@ -147,70 +147,70 @@ module LinPoly : sig This is done using the monomial tables of the module MonT. *) module MonT : sig - val clear : unit -> unit (** [clear ()] clears the mapping. *) + val clear : unit -> unit - val reserve : int -> unit (** [reserve i] reserves the integer i *) + val reserve : int -> unit - val get_fresh : unit -> int (** [get_fresh ()] return the first fresh variable *) + val get_fresh : unit -> int - val retrieve : int -> Monomial.t (** [retrieve x] @return the monomial corresponding to the variable [x] *) + val retrieve : int -> Monomial.t - val register : Monomial.t -> int (** [register m] @return the variable index for the monomial m *) + val register : Monomial.t -> int end - val linpol_of_pol : Poly.t -> t (** [linpol_of_pol p] linearise the polynomial p *) + val linpol_of_pol : Poly.t -> t - val var : var -> t (** [var x] @return 1.y where y is the variable index of the monomial x^1. *) + val var : var -> t - val coq_poly_of_linpol : (Q.t -> 'a) -> t -> 'a Mc.pExpr (** [coq_poly_of_linpol c p] @param p is a multi-variate polynomial. @param c maps a rational to a Coq polynomial coefficient. @return the coq expression corresponding to polynomial [p].*) + val coq_poly_of_linpol : (Q.t -> 'a) -> t -> 'a Mc.pExpr - val of_monomial : Monomial.t -> t (** [of_monomial m] @returns 1.x where x is the variable (index) for monomial m *) + val of_monomial : Monomial.t -> t - val of_vect : Vect.t -> t (** [of_vect v] @returns a1.x1 + ... + an.xn This is not the identity because xi is the variable index of xi^1 *) + val of_vect : Vect.t -> t - val variables : t -> ISet.t (** [variables p] @return the set of variables of the polynomial p interpreted as a multi-variate polynomial *) + val variables : t -> ISet.t - val is_variable : t -> var option (** [is_variable p] @return Some x if p = a.x for a >= 0 *) + val is_variable : t -> var option - val is_linear : t -> bool (** [is_linear p] @return whether the multi-variate polynomial is linear. *) + val is_linear : t -> bool - val is_linear_for : var -> t -> bool (** [is_linear_for x p] @return true if the polynomial is linear in x i.e can be written c*x+r where c is a constant and r is independent from x *) + val is_linear_for : var -> t -> bool - val constant : Q.t -> t (** [constant c] @return the constant polynomial c *) + val constant : Q.t -> t (** [search_linear pred p] @return a variable x such p = a.x + b such that @@ -219,44 +219,44 @@ module LinPoly : sig val search_linear : (Q.t -> bool) -> t -> var option - val search_all_linear : (Q.t -> bool) -> t -> var list (** [search_all_linear pred p] @return all the variables x such p = a.x + b such that p is linear in x i.e x does not occur in b and a is a constant such that [pred a] *) + val search_all_linear : (Q.t -> bool) -> t -> var list val get_bound : t -> Vect.Bound.t option - val product : t -> t -> t (** [product p q] @return the product of the polynomial [p*q] *) + val product : t -> t -> t - val factorise : var -> t -> t * t (** [factorise x p] @return [a,b] such that [p = a.x + b] and [x] does not occur in [b] *) + val factorise : var -> t -> t * t - val collect_square : t -> Monomial.t MonMap.t (** [collect_square p] @return a mapping m such that m[s] = s^2 for every s^2 that is a monomial of [p] *) + val collect_square : t -> Monomial.t MonMap.t - val monomials : t -> ISet.t (** [monomials p] @return the set of monomials. *) + val monomials : t -> ISet.t - val degree : t -> int (** [degree p] @return return the maximum degree *) + val degree : t -> int - val pp_var : out_channel -> var -> unit (** [pp_var o v] pretty-prints a monomial indexed by v. *) + val pp_var : out_channel -> var -> unit - val pp : out_channel -> t -> unit (** [pp o p] pretty-prints a polynomial. *) + val pp : out_channel -> t -> unit - val pp_goal : string -> out_channel -> (t * op) list -> unit (** [pp_goal typ o l] pretty-prints the list of constraints as a Coq goal. *) + val pp_goal : string -> out_channel -> (t * op) list -> unit end module ProofFormat : sig @@ -318,47 +318,47 @@ val opMult : op -> op -> op module WithProof : sig type t = (LinPoly.t * op) * ProofFormat.prf_rule - exception InvalidProof (** [InvalidProof] is raised if the operation is invalid. *) + exception InvalidProof val compare : t -> t -> int val annot : string -> t -> t val of_cstr : cstr * ProofFormat.prf_rule -> t - val output : out_channel -> t -> unit (** [out_channel chan c] pretty-prints the constraint [c] over the channel [chan] *) + val output : out_channel -> t -> unit val output_sys : out_channel -> t list -> unit - val zero : t (** [zero] represents the tautology (0=0) *) + val zero : t - val const : Q.t -> t (** [const n] represents the tautology (n>=0) *) + val const : Q.t -> t - val product : t -> t -> t (** [product p q] @return the polynomial p*q with its sign and proof *) + val product : t -> t -> t - val addition : t -> t -> t (** [addition p q] @return the polynomial p+q with its sign and proof *) + val addition : t -> t -> t - val mult : LinPoly.t -> t -> t (** [mult p q] @return the polynomial p*q with its sign and proof. @raise InvalidProof if p is not a constant and p is not an equality *) + val mult : LinPoly.t -> t -> t - val cutting_plane : t -> t option (** [cutting_plane p] does integer reasoning and adjust the constant to be integral *) + val cutting_plane : t -> t option - val linear_pivot : t list -> t -> Vect.var -> t -> t option (** [linear_pivot sys p x q] @return the polynomial [q] where [x] is eliminated using the polynomial [p] The pivoting operation is only defined if - p is linear in x i.e p = a.x+b and x neither occurs in a and b - The pivoting also requires some sign conditions for [a] *) + val linear_pivot : t list -> t -> Vect.var -> t -> t option (** [subst sys] performs the equivalent of the 'subst' tactic of Coq. For every p=0 \in sys such that p is linear in x with coefficient +/- 1 @@ -371,8 +371,8 @@ module WithProof : sig val subst : t list -> t list - val subst1 : t list -> t list (** [subst1 sys] performs a single substitution *) + val subst1 : t list -> t list val saturate_subst : bool -> t list -> t list val is_substitution : bool -> t -> var option diff --git a/plugins/micromega/simplex.ml b/plugins/micromega/simplex.ml index 702099a95d..eaa26ded62 100644 --- a/plugins/micromega/simplex.ml +++ b/plugins/micromega/simplex.ml @@ -62,9 +62,9 @@ let get_profile_info () = type iset = unit IMap.t -type tableau = Vect.t IMap.t (** Mapping basic variables to their equation. All variables >= than a threshold rst are restricted.*) +type tableau = Vect.t IMap.t module Restricted = struct type t = @@ -366,9 +366,9 @@ let push_real (opt : bool) (nw : var) (v : Vect.t) (rst : Restricted.t) let v' = safe_find "push_real" nw t' in Unsat (Vect.set nw Q.one (Vect.set 0 Q.zero (Vect.mul Q.neg_one v'))) ) -open Mutils (** One complication is that equalities needs some pre-processing. *) +open Mutils open Polynomial diff --git a/plugins/micromega/vect.ml b/plugins/micromega/vect.ml index 15f37868f7..3e0b1f2cd9 100644 --- a/plugins/micromega/vect.ml +++ b/plugins/micromega/vect.ml @@ -12,12 +12,12 @@ open NumCompat open Q.Notations open Mutils -type var = int (** [t] is the type of vectors. A vector [(x1,v1) ; ... ; (xn,vn)] is such that: - variables indexes are ordered (x1 < ... < xn - values are all non-zero *) +type var = int type mono = {var : var; coe : Q.t} type t = mono list diff --git a/plugins/micromega/vect.mli b/plugins/micromega/vect.mli index 8a26337602..9db6c075f8 100644 --- a/plugins/micromega/vect.mli +++ b/plugins/micromega/vect.mli @@ -11,10 +11,9 @@ open NumCompat open Mutils -type var = int (** Variables are simply (positive) integers. *) +type var = int -type t (** The type of vectors or equivalently linear expressions. The current implementation is using association lists. A list [(0,c),(x1,ai),...,(xn,an)] represents the linear expression @@ -24,6 +23,7 @@ type t Moreover, the representation is spare and variables with a zero coefficient are not represented. *) +type t type vector = t @@ -38,147 +38,147 @@ val compare : t -> t -> int (** {1 Basic accessors and utility functions} *) -val pp_gen : (out_channel -> var -> unit) -> out_channel -> t -> unit (** [pp_gen pp_var o v] prints the representation of the vector [v] over the channel [o] *) +val pp_gen : (out_channel -> var -> unit) -> out_channel -> t -> unit -val pp : out_channel -> t -> unit (** [pp o v] prints the representation of the vector [v] over the channel [o] *) +val pp : out_channel -> t -> unit -val pp_smt : out_channel -> t -> unit (** [pp_smt o v] prints the representation of the vector [v] over the channel [o] using SMTLIB conventions *) +val pp_smt : out_channel -> t -> unit -val variables : t -> ISet.t (** [variables v] returns the set of variables with non-zero coefficients *) +val variables : t -> ISet.t -val get_cst : t -> Q.t (** [get_cst v] returns c i.e. the coefficient of the variable zero *) +val get_cst : t -> Q.t -val decomp_cst : t -> Q.t * t (** [decomp_cst v] returns the pair (c,a1.x1+...+an.xn) *) +val decomp_cst : t -> Q.t * t -val decomp_at : int -> t -> Q.t * t (** [decomp_cst v] returns the pair (ai, ai+1.xi+...+an.xn) *) +val decomp_at : int -> t -> Q.t * t val decomp_fst : t -> (var * Q.t) * t -val cst : Q.t -> t (** [cst c] returns the vector v=c+0.x1+...+0.xn *) +val cst : Q.t -> t -val is_constant : t -> bool (** [is_constant v] holds if [v] is a constant vector i.e. v=c+0.x1+...+0.xn *) +val is_constant : t -> bool -val null : t (** [null] is the empty vector i.e. 0+0.x1+...+0.xn *) +val null : t -val is_null : t -> bool (** [is_null v] returns whether [v] is the [null] vector i.e [equal v null] *) +val is_null : t -> bool -val get : var -> t -> Q.t (** [get xi v] returns the coefficient ai of the variable [xi]. [get] is also defined for the variable 0 *) +val get : var -> t -> Q.t -val set : var -> Q.t -> t -> t (** [set xi ai' v] returns the vector c+a1.x1+...ai'.xi+...+an.xn i.e. the coefficient of the variable xi is set to ai' *) +val set : var -> Q.t -> t -> t -val mkvar : var -> t (** [mkvar xi] returns 1.xi *) +val mkvar : var -> t -val update : var -> (Q.t -> Q.t) -> t -> t (** [update xi f v] returns c+a1.x1+...+f(ai).xi+...+an.xn *) +val update : var -> (Q.t -> Q.t) -> t -> t -val fresh : t -> int (** [fresh v] return the fresh variable with index 1+ max (variables v) *) +val fresh : t -> int -val choose : t -> (var * Q.t * t) option (** [choose v] decomposes a vector [v] depending on whether it is [null] or not. @return None if v is [null] @return Some(x,n,r) where v = r + n.x x is the smallest variable with non-zero coefficient n <> 0. *) +val choose : t -> (var * Q.t * t) option -val from_list : Q.t list -> t (** [from_list l] returns the vector c+a1.x1...an.xn from the list of coefficient [l=c;a1;...;an] *) +val from_list : Q.t list -> t -val to_list : t -> Q.t list (** [to_list v] returns the list of all coefficient of the vector v i.e. [c;a1;...;an] The list representation is (obviously) not sparsed and therefore certain ai may be 0 *) +val to_list : t -> Q.t list -val decr_var : int -> t -> t (** [decr_var i v] decrements the variables of the vector [v] by the amount [i]. Beware, it is only defined if all the variables of v are greater than i *) +val decr_var : int -> t -> t -val incr_var : int -> t -> t (** [incr_var i v] increments the variables of the vector [v] by the amount [i]. *) +val incr_var : int -> t -> t -val gcd : t -> Z.t (** [gcd v] returns gcd(num(c),num(a1),...,num(an)) where num extracts the numerator of a rational value. *) +val gcd : t -> Z.t -val normalise : t -> t (** [normalise v] returns a vector with only integer coefficients *) +val normalise : t -> t (** {1 Linear arithmetics} *) -val add : t -> t -> t (** [add v1 v2] is vector addition. @param v1 is of the form c +a1.x1 +...+an.xn @param v2 is of the form c'+a1'.x1 +...+an'.xn @return c1+c1'+ (a1+a1').x1 + ... + (an+an').xn *) +val add : t -> t -> t -val mul : Q.t -> t -> t (** [mul a v] is vector multiplication of vector [v] by a scalar [a]. @return a.v = a.c+a.a1.x1+...+a.an.xn *) +val mul : Q.t -> t -> t -val mul_add : Q.t -> t -> Q.t -> t -> t (** [mul_add c1 v1 c2 v2] returns the linear combination c1.v1+c2.v2 *) +val mul_add : Q.t -> t -> Q.t -> t -> t -val subst : int -> t -> t -> t (** [subst x v v'] replaces x by v in vector v' *) +val subst : int -> t -> t -> t -val div : Q.t -> t -> t (** [div c1 v1] returns the mutiplication by the inverse of c1 i.e (1/c1).v1 *) +val div : Q.t -> t -> t -val uminus : t -> t (** [uminus v] @return -v the opposite vector of v i.e. (-1).v *) +val uminus : t -> t (** {1 Iterators} *) -val fold : ('acc -> var -> Q.t -> 'acc) -> 'acc -> t -> 'acc (** [fold f acc v] returns f (f (f acc 0 c ) x1 a1 ) ... xn an *) +val fold : ('acc -> var -> Q.t -> 'acc) -> 'acc -> t -> 'acc -val fold_error : ('acc -> var -> Q.t -> 'acc option) -> 'acc -> t -> 'acc option (** [fold_error f acc v] is the same as [fold (fun acc x i -> match acc with None -> None | Some acc' -> f acc' x i) (Some acc) v] but with early exit... *) +val fold_error : ('acc -> var -> Q.t -> 'acc option) -> 'acc -> t -> 'acc option -val find : (var -> Q.t -> 'c option) -> t -> 'c option (** [find f v] returns the first [f xi ai] such that [f xi ai <> None]. If no such xi ai exists, it returns None *) +val find : (var -> Q.t -> 'c option) -> t -> 'c option -val for_all : (var -> Q.t -> bool) -> t -> bool (** [for_all p v] returns /\_{i>=0} (f xi ai) *) +val for_all : (var -> Q.t -> bool) -> t -> bool -val exists2 : (Q.t -> Q.t -> bool) -> t -> t -> (var * Q.t * Q.t) option (** [exists2 p v v'] returns Some(xi,ai,ai') if p(xi,ai,ai') holds and ai,ai' <> 0. It returns None if no such pair of coefficient exists. *) +val exists2 : (Q.t -> Q.t -> bool) -> t -> t -> (var * Q.t * Q.t) option -val dotproduct : t -> t -> Q.t (** [dotproduct v1 v2] is the dot product of v1 and v2. *) +val dotproduct : t -> t -> Q.t val map : (var -> Q.t -> 'a) -> t -> 'a list val abs_min_elt : t -> (var * Q.t) option val partition : (var -> Q.t -> bool) -> t -> t * t module Bound : sig - type t = {cst : Q.t; var : var; coeff : Q.t} (** represents a0 + ai.xi *) + type t = {cst : Q.t; var : var; coeff : Q.t} val of_vect : vector -> t option end diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index 53a58342d2..41579d5792 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -326,20 +326,20 @@ type term_kind = Application of EConstr.constr | OtherTerm of EConstr.constr module type Elt = sig type elt - val name : string (** name *) + val name : string val table : (term_kind * decl_kind) HConstr.t ref val cast : elt decl -> decl_kind val dest : decl_kind -> elt decl option - val get_key : int (** [get_key] is the type-index used as key for the instance *) + val get_key : int - val mk_elt : Evd.evar_map -> EConstr.t -> EConstr.t array -> elt (** [mk_elt evd i [a0,..,an] returns the element of the table built from the type-instance i and the arguments (type indexes and projections) of the type-class constructor. *) + val mk_elt : Evd.evar_map -> EConstr.t -> EConstr.t array -> elt (* val arity : int*) end diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 01b12474dd..e0b083a70a 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -239,7 +239,7 @@ let interp_refine ist gl rc = } in let kind = Pretyping.OfType (pf_concl gl) in let flags = { - Pretyping.use_typeclasses = true; + Pretyping.use_typeclasses = Pretyping.UseTC; solve_unification_constraints = true; fail_evar = false; expand_evars = true; diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 1dca8fd57b..442b40221b 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -350,8 +350,8 @@ let interp_index ist gl idx = | Some c -> let rc = Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) c in begin match Notation.uninterp_prim_token rc with - | _, Constrexpr.Numeral (b,{NumTok.int = s; frac = ""; exp = ""}) -> - let n = int_of_string s in (match b with SPlus -> n | SMinus -> -n) + | _, Constrexpr.Numeral n when NumTok.Signed.is_int n -> + int_of_string (NumTok.Signed.to_string n) | _ -> raise Not_found end | None -> raise Not_found diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index df6189f212..4b78e64d98 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -402,7 +402,7 @@ let rec interp_search_about args accu = match args with | [] -> accu | (flag, arg) :: rem -> fun gr env typ -> - let ans = Search.search_about_filter arg gr env typ in + let ans = Search.search_filter arg gr env typ in (if flag then ans else not ans) && interp_search_about rem accu gr env typ let interp_search_arg arg = diff --git a/plugins/syntax/float_syntax.ml b/plugins/syntax/float_syntax.ml index 23d4d63228..e0a9906689 100644 --- a/plugins/syntax/float_syntax.ml +++ b/plugins/syntax/float_syntax.ml @@ -22,9 +22,56 @@ let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) (*** Parsing for float in digital notation ***) -let interp_float ?loc (sign,n) = - let sign = Constrexpr.(match sign with SPlus -> "" | SMinus -> "-") in - DAst.make ?loc (GFloat (Float64.of_string (sign ^ NumTok.to_string n))) +let warn_inexact_float = + CWarnings.create ~name:"inexact-float" ~category:"parsing" + (fun (sn, f) -> + Pp.strbrk + (Printf.sprintf + "The constant %s is not a binary64 floating-point value. \ + A closest value will be used and unambiguously printed %s." + sn (Float64.to_string f))) + +let interp_float ?loc n = + let sn = NumTok.Signed.to_string n in + let f = Float64.of_string sn in + (* return true when f is not exactly equal to n, + this is only used to decide whether or not to display a warning + and does not play any actual role in the parsing *) + let inexact () = match Float64.classify f with + | Float64.(PInf | NInf | NaN) -> true + | Float64.(PZero | NZero) -> not (NumTok.Signed.is_zero n) + | Float64.(PNormal | NNormal | PSubn | NSubn) -> + let m, e = + let (_, i), f, e = NumTok.Signed.to_decimal_and_exponent n in + let i = NumTok.UnsignedNat.to_string i in + let f = match f with + | None -> "" | Some f -> NumTok.UnsignedNat.to_string f in + let e = match e with + | None -> "0" | Some e -> NumTok.SignedNat.to_string e in + Bigint.of_string (i ^ f), + (try int_of_string e with Failure _ -> 0) - String.length f in + let m', e' = + let m', e' = Float64.frshiftexp f in + let m' = Float64.normfr_mantissa m' in + let e' = Uint63.to_int_min e' 4096 - Float64.eshift - 53 in + Bigint.of_string (Uint63.to_string m'), + e' in + let c2, c5 = Bigint.(of_int 2, of_int 5) in + (* check m*5^e <> m'*2^e' *) + let check m e m' e' = + not (Bigint.(equal (mult m (pow c5 e)) (mult m' (pow c2 e')))) in + (* check m*5^e*2^e' <> m' *) + let check' m e e' m' = + not (Bigint.(equal (mult (mult m (pow c5 e)) (pow c2 e')) m')) in + (* we now have to check m*10^e <> m'*2^e' *) + if e >= 0 then + if e <= e' then check m e m' (e' - e) + else check' m e (e - e') m' + else (* e < 0 *) + if e' <= e then check m' (-e) m (e - e') + else check' m' (-e) (e' - e) m in + if inexact () then warn_inexact_float ?loc (sn, f); + DAst.make ?loc (GFloat f) (* Pretty printing is already handled in constrextern.ml *) diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg index 49d29e7b63..e66dbe17b2 100644 --- a/plugins/syntax/g_numeral.mlg +++ b/plugins/syntax/g_numeral.mlg @@ -21,16 +21,16 @@ open Pcoq.Prim let pr_numnot_option = function | Nop -> mt () - | Warning n -> str "(warning after " ++ str n ++ str ")" - | Abstract n -> str "(abstract after " ++ str n ++ str ")" + | Warning n -> str "(warning after " ++ NumTok.UnsignedNat.print n ++ str ")" + | Abstract n -> str "(abstract after " ++ NumTok.UnsignedNat.print n ++ str ")" } VERNAC ARGUMENT EXTEND numnotoption PRINTED BY { pr_numnot_option } | [ ] -> { Nop } -| [ "(" "warning" "after" bigint(waft) ")" ] -> { Warning waft } -| [ "(" "abstract" "after" bigint(n) ")" ] -> { Abstract n } +| [ "(" "warning" "after" bignat(waft) ")" ] -> { Warning (NumTok.UnsignedNat.of_string waft) } +| [ "(" "abstract" "after" bignat(n) ")" ] -> { Abstract (NumTok.UnsignedNat.of_string n) } END VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 7043653f7b..c4e9c8b73d 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -12,7 +12,6 @@ open Util open Names open Glob_term open Bigint -open Constrexpr (* Poor's man DECLARE PLUGIN *) let __coq_plugin_name = "r_syntax_plugin" @@ -113,8 +112,8 @@ let z_modpath = MPdot (MPfile (make_dir binintdef), Label.make "Z") let glob_pow_pos = GlobRef.ConstRef (Constant.make2 z_modpath @@ Label.make "pow_pos") -let r_of_rawnum ?loc (sign,n) = - let n, f, e = NumTok.(n.int, n.frac, n.exp) in +let r_of_rawnum ?loc n = + let n,e = NumTok.Signed.to_bigint_and_exponent n in let izr z = DAst.make @@ GApp (DAst.make @@ GRef(glob_IZR,None), [z]) in let rmult r r' = @@ -126,15 +125,7 @@ let r_of_rawnum ?loc (sign,n) = let e = pos_of_bignat e in DAst.make @@ GApp (DAst.make @@ GRef(glob_pow_pos,None), [ten; e]) in let n = - let n = Bigint.of_string (n ^ f) in - let n = match sign with SPlus -> n | SMinus -> Bigint.(neg n) in izr (z_of_int ?loc n) in - let e = - let e = if e = "" then Bigint.zero else match e.[1] with - | '+' -> Bigint.of_string (String.sub e 2 (String.length e - 2)) - | '-' -> Bigint.(neg (of_string (String.sub e 2 (String.length e - 2)))) - | _ -> Bigint.of_string (String.sub e 1 (String.length e - 1)) in - Bigint.(sub e (of_int (String.length (String.concat "" (String.split_on_char '_' f))))) in if Bigint.is_strictly_pos e then rmult n (izr (pow10 e)) else if Bigint.is_strictly_neg e then rdiv n (izr (pow10 (neg e))) else n (* e = 0 *) @@ -143,12 +134,41 @@ let r_of_rawnum ?loc (sign,n) = (* Printing R via scopes *) (**********************************************************************) -let rawnum_of_r c = match DAst.get c with +let rawnum_of_r c = + (* print i * 10^e, precondition: e <> 0 *) + let numTok_of_int_exp i e = + (* choose between 123e-2 and 1.23, this is purely heuristic + and doesn't play any soundness role *) + let choose_exponent = + if Bigint.is_strictly_pos e then + true (* don't print 12 * 10^2 as 1200 to distinguish them *) + else + let i = Bigint.to_string i in + let li = if i.[0] = '-' then String.length i - 1 else String.length i in + let e = Bigint.neg e in + let le = String.length (Bigint.to_string e) in + Bigint.(less_than (add (of_int li) (of_int le)) e) in + (* print 123 * 10^-2 as 123e-2 *) + let numTok_exponent () = NumTok.Signed.of_bigint_and_exponent i e in + (* print 123 * 10^-2 as 1.23, precondition e < 0 *) + let numTok_dot () = + let s, i = + if Bigint.is_pos_or_zero i then NumTok.SPlus, Bigint.to_string i + else NumTok.SMinus, Bigint.(to_string (neg i)) in + let ni = String.length i in + let e = - (Bigint.to_int e) in + assert (e > 0); + let i, f = + if e < ni then String.sub i 0 (ni - e), String.sub i (ni - e) e + else "0", String.make (e - ni) '0' ^ i in + let i = s, NumTok.UnsignedNat.of_string i in + let f = NumTok.UnsignedNat.of_string f in + NumTok.Signed.of_decimal_and_exponent i (Some f) None in + if choose_exponent then numTok_exponent () else numTok_dot () in + match DAst.get c with | GApp (r, [a]) when is_gr r glob_IZR -> let n = bigint_of_z a in - let s, n = - if is_strictly_neg n then SMinus, neg n else SPlus, n in - s, NumTok.int (to_string n) + NumTok.Signed.of_bigint n | GApp (md, [l; r]) when is_gr md glob_Rmult || is_gr md glob_Rdiv -> begin match DAst.get l, DAst.get r with | GApp (i, [l]), GApp (i', [r]) @@ -161,11 +181,8 @@ let rawnum_of_r c = match DAst.get c with else let i = bigint_of_z l in let e = bignat_of_pos e in - let s, i = if is_pos_or_zero i then SPlus, i else SMinus, neg i in - let i = Bigint.to_string i in - let se = if is_gr md glob_Rdiv then "-" else "" in - let e = "e" ^ se ^ Bigint.to_string e in - s, { NumTok.int = i; frac = ""; exp = e } + let e = if is_gr md glob_Rdiv then neg e else e in + numTok_of_int_exp i e | _ -> raise Non_closed_number end | _ -> raise Non_closed_number |