summaryrefslogtreecommitdiff
path: root/plugins/funind/indfun_common.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/indfun_common.ml')
-rw-r--r--plugins/funind/indfun_common.ml558
1 files changed, 558 insertions, 0 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
new file mode 100644
index 00000000..0f048f59
--- /dev/null
+++ b/plugins/funind/indfun_common.ml
@@ -0,0 +1,558 @@
+open Names
+open Pp
+
+open Libnames
+
+let mk_prefix pre id = id_of_string (pre^(string_of_id id))
+let mk_rel_id = mk_prefix "R_"
+let mk_correct_id id = Nameops.add_suffix (mk_rel_id id) "_correct"
+let mk_complete_id id = Nameops.add_suffix (mk_rel_id id) "_complete"
+let mk_equation_id id = Nameops.add_suffix id "_equation"
+
+let msgnl m =
+ ()
+
+let invalid_argument s = raise (Invalid_argument s)
+
+
+let fresh_id avoid s = Namegen.next_ident_away_in_goal (id_of_string s) avoid
+
+let fresh_name avoid s = Name (fresh_id avoid s)
+
+let get_name avoid ?(default="H") = function
+ | Anonymous -> fresh_name avoid default
+ | Name n -> Name n
+
+let array_get_start a =
+ try
+ Array.init
+ (Array.length a - 1)
+ (fun i -> a.(i))
+ with Invalid_argument "index out of bounds" ->
+ invalid_argument "array_get_start"
+
+let id_of_name = function
+ Name id -> id
+ | _ -> raise Not_found
+
+let locate ref =
+ let (loc,qid) = qualid_of_reference ref in
+ Nametab.locate qid
+
+let locate_ind ref =
+ match locate ref with
+ | IndRef x -> x
+ | _ -> raise Not_found
+
+let locate_constant ref =
+ match locate ref with
+ | ConstRef x -> x
+ | _ -> raise Not_found
+
+
+let locate_with_msg msg f x =
+ try
+ f x
+ with
+ | Not_found -> raise (Util.UserError("", msg))
+ | e -> raise e
+
+
+let filter_map filter f =
+ let rec it = function
+ | [] -> []
+ | e::l ->
+ if filter e
+ then
+ (f e) :: it l
+ else it l
+ in
+ it
+
+
+let chop_rlambda_n =
+ let rec chop_lambda_n acc n rt =
+ if n == 0
+ then List.rev acc,rt
+ else
+ match rt with
+ | Rawterm.RLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b
+ | Rawterm.RLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b
+ | _ ->
+ raise (Util.UserError("chop_rlambda_n",
+ str "chop_rlambda_n: Not enough Lambdas"))
+ in
+ chop_lambda_n []
+
+let chop_rprod_n =
+ let rec chop_prod_n acc n rt =
+ if n == 0
+ then List.rev acc,rt
+ else
+ match rt with
+ | Rawterm.RProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b
+ | _ -> raise (Util.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products"))
+ in
+ chop_prod_n []
+
+
+
+let list_union_eq eq_fun l1 l2 =
+ let rec urec = function
+ | [] -> l2
+ | a::l -> if List.exists (eq_fun a) l2 then urec l else a::urec l
+ in
+ urec l1
+
+let list_add_set_eq eq_fun x l =
+ if List.exists (eq_fun x) l then l else x::l
+
+
+
+
+let const_of_id id =
+ let _,princ_ref =
+ qualid_of_reference (Libnames.Ident (Util.dummy_loc,id))
+ in
+ try Nametab.locate_constant princ_ref
+ with Not_found -> Util.error ("cannot find "^ string_of_id id)
+
+let def_of_const t =
+ match (Term.kind_of_term t) with
+ Term.Const sp ->
+ (try (match (Global.lookup_constant sp) with
+ {Declarations.const_body=Some c} -> Declarations.force c
+ |_ -> assert false)
+ with _ -> assert false)
+ |_ -> assert false
+
+let coq_constant s =
+ Coqlib.gen_constant_in_modules "RecursiveDefinition"
+ Coqlib.init_modules s;;
+
+let constant sl s =
+ constr_of_global
+ (Nametab.locate (make_qualid(Names.make_dirpath
+ (List.map id_of_string (List.rev sl)))
+ (id_of_string s)));;
+
+let find_reference sl s =
+ (Nametab.locate (make_qualid(Names.make_dirpath
+ (List.map id_of_string (List.rev sl)))
+ (id_of_string s)));;
+
+let eq = lazy(coq_constant "eq")
+let refl_equal = lazy(coq_constant "eq_refl")
+
+(*****************************************************************)
+(* Copy of the standart save mechanism but without the much too *)
+(* slow reduction function *)
+(*****************************************************************)
+open Declarations
+open Entries
+open Decl_kinds
+open Declare
+let definition_message id =
+ Flags.if_verbose message ((string_of_id id) ^ " is defined")
+
+
+let save with_clean id const (locality,kind) hook =
+ let {const_entry_body = pft;
+ const_entry_type = tpo;
+ const_entry_opaque = opacity } = const in
+ let l,r = match locality with
+ | Local when Lib.sections_are_opened () ->
+ let k = logical_kind_of_goal_kind kind in
+ let c = SectionLocalDef (pft, tpo, opacity) in
+ let _ = declare_variable id (Lib.cwd(), c, k) in
+ (Local, VarRef id)
+ | Local ->
+ let k = logical_kind_of_goal_kind kind in
+ let kn = declare_constant id (DefinitionEntry const, k) in
+ (Global, ConstRef kn)
+ | Global ->
+ let k = logical_kind_of_goal_kind kind in
+ let kn = declare_constant id (DefinitionEntry const, k) in
+ (Global, ConstRef kn) in
+ if with_clean then Pfedit.delete_current_proof ();
+ hook l r;
+ definition_message id
+
+
+
+
+let extract_pftreestate pts =
+ let pfterm,subgoals = Refiner.extract_open_pftreestate pts in
+ let tpfsigma = Refiner.evc_of_pftreestate pts in
+ let exl = Evarutil.non_instantiated tpfsigma in
+ if subgoals <> [] or exl <> [] then
+ Util.errorlabstrm "extract_proof"
+ (if subgoals <> [] then
+ str "Attempt to save an incomplete proof"
+ else
+ str "Attempt to save a proof with existential variables still non-instantiated");
+ let env = Global.env_of_context (Refiner.proof_of_pftreestate pts).Proof_type.goal.Evd.evar_hyps in
+ env,tpfsigma,pfterm
+
+
+let nf_betaiotazeta =
+ let clos_norm_flags flgs env sigma t =
+ Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in
+ clos_norm_flags Closure.betaiotazeta
+
+let nf_betaiota =
+ let clos_norm_flags flgs env sigma t =
+ Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in
+ clos_norm_flags Closure.betaiota
+
+let cook_proof do_reduce =
+ let pfs = Pfedit.get_pftreestate ()
+(* and ident = Pfedit.get_current_proof_name () *)
+ and (ident,strength,concl,hook) = Pfedit.current_proof_statement () in
+ let env,sigma,pfterm = extract_pftreestate pfs in
+ let pfterm =
+ if do_reduce
+ then nf_betaiota env sigma pfterm
+ else pfterm
+ in
+ (ident,
+ ({ const_entry_body = pfterm;
+ const_entry_type = Some concl;
+ const_entry_opaque = false;
+ const_entry_boxed = false},
+ strength, hook))
+
+
+let new_save_named opacity =
+ let id,(const,persistence,hook) = cook_proof true in
+ let const = { const with const_entry_opaque = opacity } in
+ save true id const persistence hook
+
+let get_proof_clean do_reduce =
+ let result = cook_proof do_reduce in
+ Pfedit.delete_current_proof ();
+ result
+
+let with_full_print f a =
+ let old_implicit_args = Impargs.is_implicit_args ()
+ and old_strict_implicit_args = Impargs.is_strict_implicit_args ()
+ and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
+ let old_rawprint = !Flags.raw_print in
+ Flags.raw_print := true;
+ Impargs.make_implicit_args false;
+ Impargs.make_strict_implicit_args false;
+ Impargs.make_contextual_implicit_args false;
+ Impargs.make_contextual_implicit_args false;
+ Dumpglob.pause ();
+ try
+ let res = f a in
+ Impargs.make_implicit_args old_implicit_args;
+ Impargs.make_strict_implicit_args old_strict_implicit_args;
+ Impargs.make_contextual_implicit_args old_contextual_implicit_args;
+ Flags.raw_print := old_rawprint;
+ Dumpglob.continue ();
+ res
+ with
+ | e ->
+ Impargs.make_implicit_args old_implicit_args;
+ Impargs.make_strict_implicit_args old_strict_implicit_args;
+ Impargs.make_contextual_implicit_args old_contextual_implicit_args;
+ Flags.raw_print := old_rawprint;
+ Dumpglob.continue ();
+ raise e
+
+
+
+
+
+
+(**********************)
+
+type function_info =
+ {
+ function_constant : constant;
+ graph_ind : inductive;
+ equation_lemma : constant option;
+ correctness_lemma : constant option;
+ completeness_lemma : constant option;
+ rect_lemma : constant option;
+ rec_lemma : constant option;
+ prop_lemma : constant option;
+ is_general : bool; (* Has this function been defined using general recursive definition *)
+ }
+
+
+(* type function_db = function_info list *)
+
+(* let function_table = ref ([] : function_db) *)
+
+
+let from_function = ref Cmap.empty
+let from_graph = ref Indmap.empty
+(*
+let rec do_cache_info finfo = function
+ | [] -> raise Not_found
+ | (finfo'::finfos as l) ->
+ if finfo' == finfo then l
+ else if finfo'.function_constant = finfo.function_constant
+ then finfo::finfos
+ else
+ let res = do_cache_info finfo finfos in
+ if res == finfos then l else finfo'::l
+
+
+let cache_Function (_,(finfos)) =
+ let new_tbl =
+ try do_cache_info finfos !function_table
+ with Not_found -> finfos::!function_table
+ in
+ if new_tbl != !function_table
+ then function_table := new_tbl
+*)
+
+let cache_Function (_,finfos) =
+ from_function := Cmap.add finfos.function_constant finfos !from_function;
+ from_graph := Indmap.add finfos.graph_ind finfos !from_graph
+
+
+let load_Function _ = cache_Function
+let open_Function _ = cache_Function
+let subst_Function (subst,finfos) =
+ let do_subst_con c = fst (Mod_subst.subst_con subst c)
+ and do_subst_ind (kn,i) = (Mod_subst.subst_ind subst kn,i)
+ in
+ let function_constant' = do_subst_con finfos.function_constant in
+ let graph_ind' = do_subst_ind finfos.graph_ind in
+ let equation_lemma' = Option.smartmap do_subst_con finfos.equation_lemma in
+ let correctness_lemma' = Option.smartmap do_subst_con finfos.correctness_lemma in
+ let completeness_lemma' = Option.smartmap do_subst_con finfos.completeness_lemma in
+ let rect_lemma' = Option.smartmap do_subst_con finfos.rect_lemma in
+ let rec_lemma' = Option.smartmap do_subst_con finfos.rec_lemma in
+ let prop_lemma' = Option.smartmap do_subst_con finfos.prop_lemma in
+ if function_constant' == finfos.function_constant &&
+ graph_ind' == finfos.graph_ind &&
+ equation_lemma' == finfos.equation_lemma &&
+ correctness_lemma' == finfos.correctness_lemma &&
+ completeness_lemma' == finfos.completeness_lemma &&
+ rect_lemma' == finfos.rect_lemma &&
+ rec_lemma' == finfos.rec_lemma &&
+ prop_lemma' == finfos.prop_lemma
+ then finfos
+ else
+ { function_constant = function_constant';
+ graph_ind = graph_ind';
+ equation_lemma = equation_lemma' ;
+ correctness_lemma = correctness_lemma' ;
+ completeness_lemma = completeness_lemma' ;
+ rect_lemma = rect_lemma' ;
+ rec_lemma = rec_lemma';
+ prop_lemma = prop_lemma';
+ is_general = finfos.is_general
+ }
+
+let classify_Function infos = Libobject.Substitute infos
+
+
+let discharge_Function (_,finfos) =
+ let function_constant' = Lib.discharge_con finfos.function_constant
+ and graph_ind' = Lib.discharge_inductive finfos.graph_ind
+ and equation_lemma' = Option.smartmap Lib.discharge_con finfos.equation_lemma
+ and correctness_lemma' = Option.smartmap Lib.discharge_con finfos.correctness_lemma
+ and completeness_lemma' = Option.smartmap Lib.discharge_con finfos.completeness_lemma
+ and rect_lemma' = Option.smartmap Lib.discharge_con finfos.rect_lemma
+ and rec_lemma' = Option.smartmap Lib.discharge_con finfos.rec_lemma
+ and prop_lemma' = Option.smartmap Lib.discharge_con finfos.prop_lemma
+ in
+ if function_constant' == finfos.function_constant &&
+ graph_ind' == finfos.graph_ind &&
+ equation_lemma' == finfos.equation_lemma &&
+ correctness_lemma' == finfos.correctness_lemma &&
+ completeness_lemma' == finfos.completeness_lemma &&
+ rect_lemma' == finfos.rect_lemma &&
+ rec_lemma' == finfos.rec_lemma &&
+ prop_lemma' == finfos.prop_lemma
+ then Some finfos
+ else
+ Some { function_constant = function_constant' ;
+ graph_ind = graph_ind' ;
+ equation_lemma = equation_lemma' ;
+ correctness_lemma = correctness_lemma' ;
+ completeness_lemma = completeness_lemma';
+ rect_lemma = rect_lemma';
+ rec_lemma = rec_lemma';
+ prop_lemma = prop_lemma' ;
+ is_general = finfos.is_general
+ }
+
+open Term
+let pr_info f_info =
+ str "function_constant := " ++ Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++
+ str "function_constant_type := " ++
+ (try Printer.pr_lconstr (Global.type_of_global (ConstRef f_info.function_constant)) with _ -> mt ()) ++ fnl () ++
+ str "equation_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.equation_lemma (mt ()) ) ++ fnl () ++
+ str "completeness_lemma :=" ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.completeness_lemma (mt ()) ) ++ fnl () ++
+ str "correctness_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.correctness_lemma (mt ()) ) ++ fnl () ++
+ str "rect_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rect_lemma (mt ()) ) ++ fnl () ++
+ str "rec_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rec_lemma (mt ()) ) ++ fnl () ++
+ str "prop_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.prop_lemma (mt ()) ) ++ fnl () ++
+ str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl ()
+
+let pr_table tb =
+ let l = Cmap.fold (fun k v acc -> v::acc) tb [] in
+ Util.prlist_with_sep fnl pr_info l
+
+let in_Function,out_Function =
+ Libobject.declare_object
+ {(Libobject.default_object "FUNCTIONS_DB") with
+ Libobject.cache_function = cache_Function;
+ Libobject.load_function = load_Function;
+ Libobject.classify_function = classify_Function;
+ Libobject.subst_function = subst_Function;
+ Libobject.discharge_function = discharge_Function
+(* Libobject.open_function = open_Function; *)
+ }
+
+
+
+(* Synchronisation with reset *)
+let freeze () =
+ !from_function,!from_graph
+let unfreeze (functions,graphs) =
+(* Pp.msgnl (str "unfreezing function_table : " ++ pr_table l); *)
+ from_function := functions;
+ from_graph := graphs
+
+let init () =
+(* Pp.msgnl (str "reseting function_table"); *)
+ from_function := Cmap.empty;
+ from_graph := Indmap.empty
+
+let _ =
+ Summary.declare_summary "functions_db_sum"
+ { Summary.freeze_function = freeze;
+ Summary.unfreeze_function = unfreeze;
+ Summary.init_function = init }
+
+let find_or_none id =
+ try Some
+ (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> Util.anomaly "Not a constant"
+ )
+ with Not_found -> None
+
+
+
+let find_Function_infos f =
+ Cmap.find f !from_function
+
+
+let find_Function_of_graph ind =
+ Indmap.find ind !from_graph
+
+let update_Function finfo =
+(* Pp.msgnl (pr_info finfo); *)
+ Lib.add_anonymous_leaf (in_Function finfo)
+
+
+let add_Function is_general f =
+ let f_id = id_of_label (con_label f) in
+ let equation_lemma = find_or_none (mk_equation_id f_id)
+ and correctness_lemma = find_or_none (mk_correct_id f_id)
+ and completeness_lemma = find_or_none (mk_complete_id f_id)
+ and rect_lemma = find_or_none (Nameops.add_suffix f_id "_rect")
+ and rec_lemma = find_or_none (Nameops.add_suffix f_id "_rec")
+ and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind")
+ and graph_ind =
+ match Nametab.locate (qualid_of_ident (mk_rel_id f_id))
+ with | IndRef ind -> ind | _ -> Util.anomaly "Not an inductive"
+ in
+ let finfos =
+ { function_constant = f;
+ equation_lemma = equation_lemma;
+ completeness_lemma = completeness_lemma;
+ correctness_lemma = correctness_lemma;
+ rect_lemma = rect_lemma;
+ rec_lemma = rec_lemma;
+ prop_lemma = prop_lemma;
+ graph_ind = graph_ind;
+ is_general = is_general
+
+ }
+ in
+ update_Function finfos
+
+let pr_table () = pr_table !from_function
+(*********************************)
+(* Debuging *)
+let functional_induction_rewrite_dependent_proofs = ref true
+let function_debug = ref false
+open Goptions
+
+let functional_induction_rewrite_dependent_proofs_sig =
+ {
+ optsync = false;
+ optname = "Functional Induction Rewrite Dependent";
+ optkey = ["Functional";"Induction";"Rewrite";"Dependent"];
+ optread = (fun () -> !functional_induction_rewrite_dependent_proofs);
+ optwrite = (fun b -> functional_induction_rewrite_dependent_proofs := b)
+ }
+let _ = declare_bool_option functional_induction_rewrite_dependent_proofs_sig
+
+let do_rewrite_dependent () = !functional_induction_rewrite_dependent_proofs = true
+
+let function_debug_sig =
+ {
+ optsync = false;
+ optname = "Function debug";
+ optkey = ["Function_debug"];
+ optread = (fun () -> !function_debug);
+ optwrite = (fun b -> function_debug := b)
+ }
+
+let _ = declare_bool_option function_debug_sig
+
+
+let do_observe () =
+ !function_debug = true
+
+
+
+let strict_tcc = ref false
+let is_strict_tcc () = !strict_tcc
+let strict_tcc_sig =
+ {
+ optsync = false;
+ optname = "Raw Function Tcc";
+ optkey = ["Function_raw_tcc"];
+ optread = (fun () -> !strict_tcc);
+ optwrite = (fun b -> strict_tcc := b)
+ }
+
+let _ = declare_bool_option strict_tcc_sig
+
+
+exception Building_graph of exn
+exception Defining_principle of exn
+exception ToShow of exn
+
+let init_constant dir s =
+ try
+ Coqlib.gen_constant "Function" dir s
+ with e -> raise (ToShow e)
+
+let jmeq () =
+ try
+ (Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
+ init_constant ["Logic";"JMeq"] "JMeq")
+ with e -> raise (ToShow e)
+
+let jmeq_rec () =
+ try
+ Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
+ init_constant ["Logic";"JMeq"] "JMeq_rec"
+ with e -> raise (ToShow e)
+
+let jmeq_refl () =
+ try
+ Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
+ init_constant ["Logic";"JMeq"] "JMeq_refl"
+ with e -> raise (ToShow e)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-13 23:29:55 +0000