1 files changed, 500 insertions, 0 deletions

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
new file mode 100644
index 0000000000..f9938c0356
--- /dev/null
+++ b/plugins/funind/indfun_common.ml
@@ -0,0 +1,500 @@
+open Names
+open Pp
+open Constr
+open Libnames
+open Globnames
+open Refiner
+
+let mk_prefix pre id = Id.of_string (pre^(Id.to_string 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 fresh_id avoid s = Namegen.next_ident_away_in_goal (Id.of_string s) (Id.Set.of_list 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 =
+  Array.init
+    (Array.length a - 1)
+    (fun i -> a.(i))
+
+let locate qid = 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 (CErrors.UserError(None, msg))
+
+
+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 DAst.get rt with
+	  | Glob_term.GLambda(name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b
+	  | Glob_term.GLetIn(name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b
+	  | _ ->
+	      raise (CErrors.UserError(Some "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 DAst.get rt with
+	  | Glob_term.GProd(name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b
+	  | _ -> raise (CErrors.UserError(Some "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_ident id in
+  try Constrintern.locate_reference princ_ref
+  with Not_found ->
+    CErrors.user_err ~hdr:"IndFun.const_of_id"
+      (str "cannot find " ++ Id.print id)
+
+[@@@ocaml.warning "-3"]
+let coq_constant s =
+  UnivGen.constr_of_monomorphic_global @@
+  Coqlib.gen_reference_in_modules "RecursiveDefinition"
+    Coqlib.init_modules s;;
+
+let find_reference sl s =
+  let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in
+  Nametab.locate (make_qualid dp (Id.of_string s))
+
+let eq = lazy(EConstr.of_constr (coq_constant "eq"))
+let refl_equal = lazy(EConstr.of_constr (coq_constant "eq_refl"))
+
+(*****************************************************************)
+(* Copy of the standart save mechanism but without the much too  *)
+(* slow reduction function                                       *)
+(*****************************************************************)
+open Entries
+open Decl_kinds
+open Declare
+
+let definition_message = Declare.definition_message
+
+let get_locality = function
+| Discharge -> true
+| Local -> true
+| Global -> false
+
+let save with_clean id const ?hook (locality,_,kind) =
+  let fix_exn = Future.fix_exn_of const.const_entry_body in
+  let l,r = match locality with
+    | Discharge when Lib.sections_are_opened () ->
+        let k = Kindops.logical_kind_of_goal_kind kind in
+	let c = SectionLocalDef const in
+	let _ = declare_variable id (Lib.cwd(), c, k) in
+	(Local, VarRef id)
+    | Discharge | Local | Global ->
+        let local = get_locality locality in
+        let k = Kindops.logical_kind_of_goal_kind kind in
+        let kn = declare_constant id ~local (DefinitionEntry const, k) in
+	(locality, ConstRef kn)
+  in
+  if with_clean then Proof_global.discard_current ();
+  Lemmas.call_hook ?hook ~fix_exn l r;
+  definition_message id
+
+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
+  let old_printuniverses = !Constrextern.print_universes in
+  let old_printallowmatchdefaultclause = !Detyping.print_allow_match_default_clause in
+  Constrextern.print_universes := true;
+  Detyping.print_allow_match_default_clause := false;
+  Flags.raw_print := true;
+  Impargs.make_implicit_args false;
+  Impargs.make_strict_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;
+    Constrextern.print_universes := old_printuniverses;
+    Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause;
+    Dumpglob.continue ();
+    res
+  with
+    | reraise ->
+	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;
+	Constrextern.print_universes := old_printuniverses;
+        Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause;
+	Dumpglob.continue ();
+	raise reraise
+
+
+
+
+
+
+(**********************)
+
+type function_info =
+    {
+      function_constant : Constant.t;
+      graph_ind : inductive;
+      equation_lemma : Constant.t option;
+      correctness_lemma : Constant.t option;
+      completeness_lemma : Constant.t option;
+      rect_lemma : Constant.t option;
+      rec_lemma : Constant.t option;
+      prop_lemma : Constant.t 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 = Summary.ref Cmap_env.empty ~name:"functions_db_fn"
+let from_graph = Summary.ref Indmap.empty ~name:"functions_db_gr"
+
+(*
+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_env.add finfos.function_constant finfos !from_function;
+  from_graph := Indmap.add finfos.graph_ind finfos !from_graph
+
+
+let subst_Function (subst,finfos) =
+  let do_subst_con c = Mod_subst.subst_constant subst c
+  and do_subst_ind i = Mod_subst.subst_ind subst 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.Smart.map do_subst_con finfos.equation_lemma in
+  let correctness_lemma' = Option.Smart.map do_subst_con finfos.correctness_lemma in
+  let completeness_lemma' = Option.Smart.map do_subst_con finfos.completeness_lemma in
+  let rect_lemma' = Option.Smart.map do_subst_con finfos.rect_lemma in
+  let rec_lemma' = Option.Smart.map do_subst_con finfos.rec_lemma in
+  let prop_lemma' =  Option.Smart.map 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 discharge_Function (_,finfos) = Some finfos
+
+let pr_ocst c =
+  let sigma, env = Pfedit.get_current_context () in
+  Option.fold_right (fun v acc -> Printer.pr_lconstr_env env sigma (mkConst v)) c (mt ())
+
+let pr_info f_info =
+  let sigma, env = Pfedit.get_current_context () in
+  str "function_constant := " ++
+  Printer.pr_lconstr_env env sigma (mkConst f_info.function_constant)++ fnl () ++
+  str "function_constant_type := " ++
+  (try
+     Printer.pr_lconstr_env env sigma
+       (fst (Typeops.type_of_global_in_context env (ConstRef f_info.function_constant)))
+   with e when CErrors.noncritical e -> mt ()) ++ fnl () ++
+  str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++
+  str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++
+  str "correctness_lemma := " ++ pr_ocst f_info.correctness_lemma ++ fnl () ++
+  str "rect_lemma := " ++ pr_ocst f_info.rect_lemma ++ fnl () ++
+  str "rec_lemma := " ++ pr_ocst f_info.rec_lemma ++ fnl () ++
+  str "prop_lemma := " ++ pr_ocst f_info.prop_lemma ++ fnl () ++
+  str "graph_ind := " ++ Printer.pr_lconstr_env env sigma (mkInd f_info.graph_ind) ++ fnl ()
+
+let pr_table tb =
+  let l = Cmap_env.fold (fun k v acc -> v::acc) tb [] in
+  Pp.prlist_with_sep fnl pr_info l
+
+let in_Function : function_info -> Libobject.obj =
+  let open Libobject in
+  declare_object @@ superglobal_object "FUNCTIONS_DB"
+    ~cache:cache_Function
+    ~subst:(Some subst_Function)
+    ~discharge:discharge_Function
+
+
+let find_or_none id =
+  try Some
+    (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> CErrors.anomaly (Pp.str "Not a constant.")
+    )
+  with Not_found -> None
+
+
+
+let find_Function_infos f =
+  Cmap_env.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 = Label.to_id (Constant.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 | _ -> CErrors.anomaly (Pp.str "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 = 
+  {
+    optdepr = 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 =
+  {
+    optdepr = 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 
+
+
+
+let strict_tcc = ref false
+let is_strict_tcc () = !strict_tcc
+let strict_tcc_sig =
+  {
+    optdepr = 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 jmeq () =
+  try
+    Coqlib.check_required_library Coqlib.jmeq_module_name;
+    EConstr.of_constr @@
+    UnivGen.constr_of_monomorphic_global @@
+      Coqlib.lib_ref "core.JMeq.type"
+  with e when CErrors.noncritical e -> raise (ToShow e)
+
+let jmeq_refl () =
+  try
+    Coqlib.check_required_library Coqlib.jmeq_module_name;
+    EConstr.of_constr @@
+    UnivGen.constr_of_monomorphic_global @@
+      Coqlib.lib_ref "core.JMeq.refl"
+  with e when CErrors.noncritical e -> raise (ToShow e)
+
+let h_intros l =
+  tclMAP (fun x -> Proofview.V82.of_tactic (Tactics.Simple.intro x)) l
+
+let h_id = Id.of_string "h"
+let hrec_id = Id.of_string "hrec"
+let well_founded = function () -> EConstr.of_constr (coq_constant "well_founded")
+let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc")
+let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv")
+
+[@@@ocaml.warning "-3"]
+let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@
+    Coqlib.find_reference "IndFun" ["Coq"; "Arith";"Wf_nat"] "well_founded_ltof"
+[@@@ocaml.warning "+3"]
+
+let ltof_ref = function  () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof")
+
+let evaluable_of_global_reference r = (* Tacred.evaluable_of_global_reference (Global.env ()) *)
+  match r with
+      ConstRef sp -> EvalConstRef sp
+    | VarRef id -> EvalVarRef id
+    | _ -> assert false;;
+
+let list_rewrite (rev:bool) (eqs: (EConstr.constr*bool) list) =
+  tclREPEAT
+    (List.fold_right
+       (fun (eq,b) i -> tclORELSE (Proofview.V82.of_tactic ((if b then Equality.rewriteLR else Equality.rewriteRL) eq)) i)
+       (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));;
+
+let decompose_lam_n sigma n =
+  if n < 0 then CErrors.user_err Pp.(str "decompose_lam_n: integer parameter must be positive");
+  let rec lamdec_rec l n c =
+    if Int.equal n 0 then l,c
+    else match EConstr.kind sigma c with
+      | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c
+      | Cast (c,_,_)     -> lamdec_rec l n c
+      | _ -> CErrors.user_err Pp.(str "decompose_lam_n: not enough abstractions")
+  in
+  lamdec_rec [] n
+
+let lamn n env b =
+  let open EConstr in
+  let rec lamrec = function
+    | (0, env, b)        -> b
+    | (n, ((v,t)::l), b) -> lamrec (n-1,  l, mkLambda (v,t,b))
+    | _ -> assert false
+  in
+  lamrec (n,env,b)
+
+(* compose_lam [xn:Tn;..;x1:T1] b = [x1:T1]..[xn:Tn]b *)
+let compose_lam l b = lamn (List.length l) l b
+
+(* prodn n [xn:Tn;..;x1:T1;Gamma] b = (x1:T1)..(xn:Tn)b *)
+let prodn n env b =
+  let open EConstr in
+  let rec prodrec = function
+    | (0, env, b)        -> b
+    | (n, ((v,t)::l), b) -> prodrec (n-1,  l, mkProd (v,t,b))
+    | _ -> assert false
+  in
+  prodrec (n,env,b)
+
+(* compose_prod [xn:Tn;..;x1:T1] b = (x1:T1)..(xn:Tn)b *)
+let compose_prod l b = prodn (List.length l) l b
+
+type tcc_lemma_value =
+  | Undefined
+  | Value of constr
+  | Not_needed
+
+(* We only "purify" on exceptions. XXX: What is this doing here? *)
+let funind_purify f x =
+  let st = Vernacstate.freeze_interp_state ~marshallable:false in
+  try f x
+  with e ->
+    let e = CErrors.push e in
+    Vernacstate.unfreeze_interp_state st;
+    Exninfo.iraise e