diff options
Diffstat (limited to 'contrib/funind/functional_principles_types.ml')
-rw-r--r-- | contrib/funind/functional_principles_types.ml | 531 |
1 files changed, 324 insertions, 207 deletions
diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml index 8ef13264..f83eae8d 100644 --- a/contrib/funind/functional_principles_types.ml +++ b/contrib/funind/functional_principles_types.ml @@ -19,9 +19,41 @@ exception Toberemoved_with_rel of int*constr exception Toberemoved +let pr_elim_scheme el = + let env = Global.env () in + let msg = str "params := " ++ Printer.pr_rel_context env el.params in + let env = Environ.push_rel_context el.params env in + let msg = msg ++ fnl () ++ str "predicates := "++ Printer.pr_rel_context env el.predicates in + let env = Environ.push_rel_context el.predicates env in + let msg = msg ++ fnl () ++ str "branches := " ++ Printer.pr_rel_context env el.branches in + let env = Environ.push_rel_context el.branches env in + let msg = msg ++ fnl () ++ str "args := " ++ Printer.pr_rel_context env el.args in + let env = Environ.push_rel_context el.args env in + msg ++ fnl () ++ str "concl := " ++ pr_lconstr_env env el.concl + +let observe s = + if do_observe () + then Pp.msgnl s +let pr_elim_scheme el = + let env = Global.env () in + let msg = str "params := " ++ Printer.pr_rel_context env el.params in + let env = Environ.push_rel_context el.params env in + let msg = msg ++ fnl () ++ str "predicates := "++ Printer.pr_rel_context env el.predicates in + let env = Environ.push_rel_context el.predicates env in + let msg = msg ++ fnl () ++ str "branches := " ++ Printer.pr_rel_context env el.branches in + let env = Environ.push_rel_context el.branches env in + let msg = msg ++ fnl () ++ str "args := " ++ Printer.pr_rel_context env el.args in + let env = Environ.push_rel_context el.args env in + msg ++ fnl () ++ str "concl := " ++ pr_lconstr_env env el.concl + + +let observe s = + if do_observe () + then Pp.msgnl s + (* Transform an inductive induction principle into a functional one @@ -29,6 +61,25 @@ exception Toberemoved let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let princ_type_info = compute_elim_sig princ_type in let env = Global.env () in + let env_with_params = Environ.push_rel_context princ_type_info.params env in + let tbl = Hashtbl.create 792 in + let rec change_predicates_names (avoid:identifier list) (predicates:Sign.rel_context) : Sign.rel_context = + match predicates with + | [] -> [] + |(Name x,v,t)::predicates -> + let id = Nameops.next_ident_away x avoid in + Hashtbl.add tbl id x; + (Name id,v,t)::(change_predicates_names (id::avoid) predicates) + | (Anonymous,_,_)::_ -> anomaly "Anonymous property binder " + in + let avoid = (Termops.ids_of_context env_with_params ) in + let princ_type_info = + { princ_type_info with + predicates = change_predicates_names avoid princ_type_info.predicates + } + in +(* observe (str "starting princ_type := " ++ pr_lconstr_env env princ_type); *) +(* observe (str "princ_infos : " ++ pr_elim_scheme princ_type_info); *) let change_predicate_sort i (x,_,t) = let new_sort = sorts.(i) in let args,_ = decompose_prod t in @@ -37,7 +88,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = then List.tl args else args in - x,None,compose_prod real_args (mkSort new_sort) + Nameops.out_name x,None,compose_prod real_args (mkSort new_sort) in let new_predicates = list_map_i @@ -45,20 +96,21 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = 0 princ_type_info.predicates in - let env_with_params_and_predicates = - Environ.push_rel_context - new_predicates - (Environ.push_rel_context - princ_type_info.params - env - ) - in + let env_with_params_and_predicates = List.fold_right Environ.push_named new_predicates env_with_params in let rel_as_kn = fst (match princ_type_info.indref with | Some (Libnames.IndRef ind) -> ind - | _ -> failwith "Not a valid predicate" + | _ -> error "Not a valid predicate" ) in + let ptes_vars = List.map (fun (id,_,_) -> id) new_predicates in + let is_pte = + let set = List.fold_right Idset.add ptes_vars Idset.empty in + fun t -> + match kind_of_term t with + | Var id -> Idset.mem id set + | _ -> false + in let pre_princ = it_mkProd_or_LetIn ~init: @@ -72,6 +124,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = ) princ_type_info.branches in + let pre_princ = substl (List.map mkVar ptes_vars) pre_princ in let is_dom c = match kind_of_term c with | Ind((u,_)) -> u = rel_as_kn @@ -108,21 +161,15 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = | Prod(x,t,b) -> compute_new_princ_type_for_binder remove mkProd env x t b | Lambda(x,t,b) -> - compute_new_princ_type_for_binder remove mkLambda env x t b + compute_new_princ_type_for_binder remove mkLambda env x t b | Ind _ | Construct _ when is_dom pre_princ -> raise Toberemoved | App(f,args) when is_dom f -> let var_to_be_removed = destRel (array_last args) in let num = get_fun_num f in raise (Toberemoved_with_rel (var_to_be_removed,mk_replacement pre_princ num args)) | App(f,args) -> - let is_pte = - match kind_of_term f with - | Rel n -> - is_pte (Environ.lookup_rel n env) - | _ -> false - in let args = - if is_pte && remove + if is_pte f && remove then array_get_start args else args in @@ -138,15 +185,13 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = compute_new_princ_type_for_letin remove env x v t b | _ -> pre_princ,[] in -(* observennl ( *) -(* match kind_of_term pre_princ with *) -(* | Prod _ -> *) -(* str "compute_new_princ_type for "++ *) +(* let _ = match kind_of_term pre_princ with *) +(* | Prod _ -> *) +(* observe(str "compute_new_princ_type for "++ *) (* pr_lconstr_env env pre_princ ++ *) (* str" is "++ *) -(* pr_lconstr_env env new_princ_type ++ fnl () *) -(* | _ -> str "" *) -(* ); *) +(* pr_lconstr_env env new_princ_type ++ fnl ()) *) +(* | _ -> () in *) res and compute_new_princ_type_for_binder remove bind_fun env x t b = @@ -156,25 +201,25 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let new_x : name = get_name (ids_of_context env) x in let new_env = Environ.push_rel (x,None,t) env in let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in - if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b - then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b - else - ( - bind_fun(new_x,new_t,new_b), - list_union_eq - eq_constr - binders_to_remove_from_t - (List.map pop binders_to_remove_from_b) - ) - - with - | Toberemoved -> -(* msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) - let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in + if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b + then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b + else + ( + bind_fun(new_x,new_t,new_b), + list_union_eq + eq_constr + binders_to_remove_from_t + (List.map pop binders_to_remove_from_b) + ) + + with + | Toberemoved -> +(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) + let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in new_b, List.map pop binders_to_remove_from_b | Toberemoved_with_rel (n,c) -> -(* msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) - let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in +(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) + let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b) end and compute_new_princ_type_for_letin remove env x v t b = @@ -184,7 +229,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let new_v,binders_to_remove_from_v = compute_new_princ_type remove env v in let new_x : name = get_name (ids_of_context env) x in let new_env = Environ.push_rel (x,Some v,t) env in - let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in + let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b else @@ -198,24 +243,33 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = with | Toberemoved -> -(* msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) +(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in new_b, List.map pop binders_to_remove_from_b | Toberemoved_with_rel (n,c) -> -(* msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) +(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b) end and compute_new_princ_type_with_acc remove env e (c_acc,to_remove_acc) = - let new_e,to_remove_from_e = compute_new_princ_type remove env e - in - new_e::c_acc,list_union_eq eq_constr to_remove_from_e to_remove_acc + let new_e,to_remove_from_e = compute_new_princ_type remove env e + in + new_e::c_acc,list_union_eq eq_constr to_remove_from_e to_remove_acc in (* observe (str "Computing new principe from " ++ pr_lconstr_env env_with_params_and_predicates pre_princ); *) let pre_res,_ = - compute_new_princ_type princ_type_info.indarg_in_concl env_with_params_and_predicates pre_princ in + compute_new_princ_type princ_type_info.indarg_in_concl env_with_params_and_predicates pre_princ + in + let pre_res = + replace_vars + (list_map_i (fun i id -> (id, mkRel i)) 1 ptes_vars) + (lift (List.length ptes_vars) pre_res) + in it_mkProd_or_LetIn - ~init:(it_mkProd_or_LetIn ~init:pre_res new_predicates) + ~init:(it_mkProd_or_LetIn + ~init:pre_res (List.map (fun (id,t,b) -> Name(Hashtbl.find tbl id), t,b) + new_predicates) + ) princ_type_info.params @@ -246,128 +300,101 @@ let change_property_sort toSort princ princName = let pp_dur time time' = str (string_of_float (System.time_difference time time')) -(* End of things to be removed latter : just here to compare - saving proof with and without normalizing the proof -*) - -let qed () = Command.save_named true +(* let qed () = save_named true *) let defined () = Command.save_named false -let generate_functional_principle - interactive_proof - old_princ_type sorts new_princ_name funs i proof_tac - = - let f = funs.(i) in - let type_sort = Termops.new_sort_in_family InType in - let new_sorts = - match sorts with - | None -> Array.make (Array.length funs) (type_sort) - | Some a -> a - in + + + + + +let build_functional_principle interactive_proof old_princ_type sorts funs i proof_tac hook = (* First we get the type of the old graph principle *) let mutr_nparams = (compute_elim_sig old_princ_type).nparams in - (* First we get the type of the old graph principle *) - let new_principle_type = + (* let time1 = System.get_time () in *) + let new_principle_type = compute_new_princ_type_from_rel (Array.map mkConst funs) - new_sorts + sorts old_princ_type - in -(* observe (str "new_principle_type : " ++ pr_lconstr new_principle_type); *) - let base_new_princ_name,new_princ_name = - match new_princ_name with - | Some (id) -> id,id - | None -> - let id_of_f = id_of_label (con_label f) in - id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort) in - let names = ref [new_princ_name] in - let hook _ _ = - if sorts = None - then -(* let id_of_f = id_of_label (con_label f) in *) - let register_with_sort fam_sort = - let s = Termops.new_sort_in_family fam_sort in - let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in - let value = - change_property_sort s new_principle_type new_princ_name - in -(* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let ce = - { const_entry_body = value; - const_entry_type = None; - const_entry_opaque = false; - const_entry_boxed = Options.boxed_definitions() - } - in - ignore( - Declare.declare_constant - name - (Entries.DefinitionEntry ce, - Decl_kinds.IsDefinition (Decl_kinds.Scheme) - ) - ); - names := name :: !names - in - register_with_sort InProp; - register_with_sort InSet + (* let time2 = System.get_time () in *) + (* Pp.msgnl (str "computing principle type := " ++ System.fmt_time_difference time1 time2); *) + (* observe (str "new_principle_type : " ++ pr_lconstr new_principle_type); *) + let new_princ_name = + next_global_ident_away true (id_of_string "___________princ_________") [] in begin Command.start_proof new_princ_name (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem)) new_principle_type - hook + (hook new_principle_type) ; - try - let _tim1 = System.get_time () in - Pfedit.by (proof_tac (Array.map mkConst funs) mutr_nparams); - let _tim2 = System.get_time () in -(* begin *) -(* let dur1 = System.time_difference tim1 tim2 in *) -(* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *) -(* end; *) - let do_save = not (do_observe ()) && not interactive_proof in - let _ = - try -(* Vernacentries.show_script (); *) - Options.silently defined (); - let _dur2 = System.time_difference _tim2 (System.get_time ()) in -(* Pp.msgnl (str ("Time to check proof: ") ++ str (string_of_float dur2)); *) - Options.if_verbose - (fun () -> - Pp.msgnl ( - prlist_with_sep - (fun () -> str" is defined " ++ fnl ()) - Ppconstr.pr_id - (List.rev !names) ++ str" is defined " - ) - ) - () - with e when do_save -> - msg_warning - ( - Cerrors.explain_exn e - ); - if not (do_observe ()) - then begin Vernacentries.interp (Vernacexpr.VernacAbort None);raise e end - in - () - -(* let tim3 = Sys.time () in *) -(* Pp.msgnl (str ("Time to save proof: ") ++ str (string_of_float (tim3 -. tim2))); *) - - with - | e -> - msg_warning - ( - Cerrors.explain_exn e - ); - if not ( do_observe ()) - then begin Vernacentries.interp (Vernacexpr.VernacAbort None);raise e end + (* let _tim1 = System.get_time () in *) + Pfedit.by (proof_tac (Array.map mkConst funs) mutr_nparams); + (* let _tim2 = System.get_time () in *) + (* begin *) + (* let dur1 = System.time_difference tim1 tim2 in *) + (* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *) + (* end; *) + get_proof_clean true end +let generate_functional_principle + interactive_proof + old_princ_type sorts new_princ_name funs i proof_tac + = + let f = funs.(i) in + let type_sort = Termops.new_sort_in_family InType in + let new_sorts = + match sorts with + | None -> Array.make (Array.length funs) (type_sort) + | Some a -> a + in + let base_new_princ_name,new_princ_name = + match new_princ_name with + | Some (id) -> id,id + | None -> + let id_of_f = id_of_label (con_label f) in + id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort) + in + let names = ref [new_princ_name] in + let hook new_principle_type _ _ = + if sorts = None + then + (* let id_of_f = id_of_label (con_label f) in *) + let register_with_sort fam_sort = + let s = Termops.new_sort_in_family fam_sort in + let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in + let value = change_property_sort s new_principle_type new_princ_name in + (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) + let ce = + { const_entry_body = value; + const_entry_type = None; + const_entry_opaque = false; + const_entry_boxed = Options.boxed_definitions() + } + in + ignore( + Declare.declare_constant + name + (Entries.DefinitionEntry ce, + Decl_kinds.IsDefinition (Decl_kinds.Scheme) + ) + ); + names := name :: !names + in + register_with_sort InProp; + register_with_sort InSet + in + let (id,(entry,g_kind,hook)) = + build_functional_principle interactive_proof old_princ_type new_sorts funs i proof_tac hook + in + save false new_princ_name entry g_kind hook +(* defined () *) + exception Not_Rec @@ -441,30 +468,20 @@ let get_funs_constant mp dp = l_const exception No_graph_found - -let make_scheme fas = +exception Found_type of int + +let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_entry list = let env = Global.env () and sigma = Evd.empty in - let id_to_constr id = - Tacinterp.constr_of_id env id - in - let funs = - List.map - (fun (_,f,_) -> - try id_to_constr f - with Not_found -> - Util.error ("Cannot find "^ string_of_id f) - ) - fas - in - let first_fun = destConst (List.hd funs) in - let funs_mp,funs_dp,first_fun_id = Names.repr_con first_fun in - let first_fun_rel_id = mk_rel_id (id_of_label first_fun_id) in + let funs = List.map fst fas in + let first_fun = List.hd funs in + + + let funs_mp,funs_dp,_ = Names.repr_con first_fun in let first_fun_kn = try - (* Fixme: take into account funs_mp and funs_dp *) - fst (destInd (id_to_constr first_fun_rel_id)) - with Not_found -> raise No_graph_found + fst (find_Function_infos first_fun).graph_ind + with Not_found -> raise No_graph_found in let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in let this_block_funs = Array.map fst this_block_funs_indexes in @@ -472,7 +489,7 @@ let make_scheme fas = let funs_indexes = let this_block_funs_indexes = Array.to_list this_block_funs_indexes in List.map - (function const -> List.assoc (destConst const) this_block_funs_indexes) + (function const -> List.assoc const this_block_funs_indexes) funs in let ind_list = @@ -484,49 +501,149 @@ let make_scheme fas = ) funs_indexes in - let l_schemes = List.map (Typing.type_of env sigma ) (Indrec.build_mutual_indrec env sigma ind_list) in + let l_schemes = + List.map + (Typing.type_of env sigma) + (Indrec.build_mutual_indrec env sigma ind_list) + in let i = ref (-1) in let sorts = - List.rev_map (fun (_,_,x) -> + List.rev_map (fun (_,x) -> Termops.new_sort_in_family (Pretyping.interp_elimination_sort x) ) fas in - let princ_names = List.map (fun (x,_,_) -> x) fas in - let _ = List.map2 - (fun princ_name scheme_type -> - incr i; -(* observe (str "Generating " ++ Ppconstr.pr_id princ_name ++str " with " ++ *) -(* pr_lconstr scheme_type ++ str " and " ++ (fun a -> prlist_with_sep spc (fun c -> pr_lconstr (mkConst c)) (Array.to_list a)) this_block_funs *) -(* ); *) - generate_functional_principle - false - scheme_type - (Some (Array.of_list sorts)) - (Some princ_name) - this_block_funs - !i - (prove_princ_for_struct false !i (Array.of_list (List.map destConst funs))) - ) - princ_names - l_schemes + (* We create the first priciple by tactic *) + let first_type,other_princ_types = + match l_schemes with + s::l_schemes -> s,l_schemes + | _ -> anomaly "" in - () + let (_,(const,_,_)) = + build_functional_principle false + first_type + (Array.of_list sorts) + this_block_funs + 0 + (prove_princ_for_struct false 0 (Array.of_list funs)) + (fun _ _ _ -> ()) + in + incr i; + (* The others are just deduced *) + if other_princ_types = [] + then + [const] + else + let other_fun_princ_types = + let funs = Array.map mkConst this_block_funs in + let sorts = Array.of_list sorts in + List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types + in + let first_princ_body,first_princ_type = const.Entries.const_entry_body, const.Entries.const_entry_type in + let ctxt,fix = Sign.decompose_lam_assum first_princ_body in (* the principle has for forall ...., fix .*) + let (idxs,_),(_,ta,_ as decl) = destFix fix in + let other_result = + List.map (* we can now compute the other principles *) + (fun scheme_type -> + incr i; + observe (Printer.pr_lconstr scheme_type); + let type_concl = snd (Sign.decompose_prod_assum scheme_type) in + let applied_f = List.hd (List.rev (snd (decompose_app type_concl))) in + let f = fst (decompose_app applied_f) in + try (* we search the number of the function in the fix block (name of the function) *) + Array.iteri + (fun j t -> + let t = snd (Sign.decompose_prod_assum t) in + let applied_g = List.hd (List.rev (snd (decompose_app t))) in + let g = fst (decompose_app applied_g) in + if eq_constr f g + then raise (Found_type j); + observe (Printer.pr_lconstr f ++ str " <> " ++ + Printer.pr_lconstr g) + + ) + ta; + (* If we reach this point, the two principle are not mutually recursive + We fall back to the previous method + *) + let (_,(const,_,_)) = + build_functional_principle + false + (List.nth other_princ_types (!i - 1)) + (Array.of_list sorts) + this_block_funs + !i + (prove_princ_for_struct false !i (Array.of_list funs)) + (fun _ _ _ -> ()) + in + const + with Found_type i -> + let princ_body = + Termops.it_mkLambda_or_LetIn ~init:(mkFix((idxs,i),decl)) ctxt + in + {const with + Entries.const_entry_body = princ_body; + Entries.const_entry_type = Some scheme_type + } + ) + other_fun_princ_types + in + const::other_result + +let build_scheme fas = +(* (fun (f,_) -> *) +(* try Libnames.constr_of_global (Nametab.global f) *) +(* with Not_found -> *) +(* Util.error ("Cannot find "^ Libnames.string_of_reference f) *) +(* ) *) +(* fas *) -let make_case_scheme fa = + let bodies_types = + make_scheme + (List.map + (fun (_,f,sort) -> + let f_as_constant = + try + match Nametab.global f with + | Libnames.ConstRef c -> c + | _ -> Util.error "Functional Scheme can only be used with functions" + with Not_found -> + Util.error ("Cannot find "^ Libnames.string_of_reference f) + in + (f_as_constant,sort) + ) + fas + ) + in + List.iter2 + (fun (princ_id,_,_) def_entry -> + ignore (Declare.declare_constant + princ_id + (Entries.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem)); + Options.if_verbose (fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined")) princ_id + ) + fas + bodies_types + + + +let build_case_scheme fa = let env = Global.env () and sigma = Evd.empty in - let id_to_constr id = - Tacinterp.constr_of_id env id - in - let funs = (fun (_,f,_) -> id_to_constr f) fa in +(* let id_to_constr id = *) +(* Tacinterp.constr_of_id env id *) +(* in *) + let funs = (fun (_,f,_) -> + try Libnames.constr_of_global (Nametab.global f) + with Not_found -> + Util.error ("Cannot find "^ Libnames.string_of_reference f)) fa in let first_fun = destConst funs in - let funs_mp,funs_dp,first_fun_id = Names.repr_con first_fun in - let first_fun_rel_id = mk_rel_id (id_of_label first_fun_id) in - let first_fun_kn = - (* Fixme: take into accour funs_mp and funs_dp *) - fst (destInd (id_to_constr first_fun_rel_id)) - in + + let funs_mp,funs_dp,_ = Names.repr_con first_fun in + let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind with Not_found -> raise No_graph_found in + + + let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in let this_block_funs = Array.map fst this_block_funs_indexes in let prop_sort = InProp in |