diff options
Diffstat (limited to 'contrib/funind/functional_principles_types.ml')
| -rw-r--r-- | contrib/funind/functional_principles_types.ml | 733 |
1 files changed, 0 insertions, 733 deletions
diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml deleted file mode 100644 index b03bdf31..00000000 --- a/contrib/funind/functional_principles_types.ml +++ /dev/null @@ -1,733 +0,0 @@ -open Printer -open Util -open Term -open Termops -open Names -open Declarations -open Pp -open Entries -open Hiddentac -open Evd -open Tacmach -open Proof_type -open Tacticals -open Tactics -open Indfun_common -open Functional_principles_proofs - -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 -*) -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 - let real_args = - if princ_type_info.indarg_in_concl - then List.tl args - else args - in - Nameops.out_name x,None,compose_prod real_args (mkSort new_sort) - in - let new_predicates = - list_map_i - change_predicate_sort - 0 - princ_type_info.predicates - 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 - | _ -> 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: - (it_mkProd_or_LetIn - ~init:(Option.fold_right - mkProd_or_LetIn - princ_type_info.indarg - princ_type_info.concl - ) - princ_type_info.args - ) - 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 - | Construct((u,_),_) -> u = rel_as_kn - | _ -> false - in - let get_fun_num c = - match kind_of_term c with - | Ind(_,num) -> num - | Construct((_,num),_) -> num - | _ -> assert false - in - let dummy_var = mkVar (id_of_string "________") in - let mk_replacement c i args = - let res = mkApp(rel_to_fun.(i),Array.map pop (array_get_start args)) in -(* observe (str "replacing " ++ pr_lconstr c ++ str " by " ++ pr_lconstr res); *) - res - in - let rec has_dummy_var t = - fold_constr - (fun b t -> b || (eq_constr t dummy_var) || (has_dummy_var t)) - false - t - in - let rec compute_new_princ_type remove env pre_princ : types*(constr list) = - let (new_princ_type,_) as res = - match kind_of_term pre_princ with - | Rel n -> - begin - try match Environ.lookup_rel n env with - | _,_,t when is_dom t -> raise Toberemoved - | _ -> pre_princ,[] with Not_found -> assert false - end - | 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 - | 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 args = - if is_pte f && remove - then array_get_start args - else args - in - let new_args,binders_to_remove = - Array.fold_right (compute_new_princ_type_with_acc remove env) - args - ([],[]) - in - let new_f,binders_to_remove_from_f = compute_new_princ_type remove env f in - applist(new_f, new_args), - list_union_eq eq_constr binders_to_remove_from_f binders_to_remove - | LetIn(x,v,t,b) -> - compute_new_princ_type_for_letin remove env x v t b - | _ -> pre_princ,[] - in -(* 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 ()) *) -(* | _ -> () in *) - res - - and compute_new_princ_type_for_binder remove bind_fun env x t b = - begin - try - let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in - 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 -> -(* 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) -> -(* 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 = - begin - try - let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in - 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 - 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 - ( - mkLetIn(new_x,new_v,new_t,new_b), - list_union_eq - eq_constr - (list_union_eq eq_constr binders_to_remove_from_t binders_to_remove_from_v) - (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) -> -(* 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 - 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 - 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 (List.map (fun (id,t,b) -> Name(Hashtbl.find tbl id), t,b) - new_predicates) - ) - princ_type_info.params - - - -let change_property_sort toSort princ princName = - let princ_info = compute_elim_sig princ in - let change_sort_in_predicate (x,v,t) = - (x,None, - let args,_ = decompose_prod t in - compose_prod args (mkSort toSort) - ) - in - let princName_as_constr = Tacinterp.constr_of_id (Global.env ()) princName in - let init = - let nargs = (princ_info.nparams + (List.length princ_info.predicates)) in - mkApp(princName_as_constr, - Array.init nargs - (fun i -> mkRel (nargs - i ))) - in - it_mkLambda_or_LetIn - ~init: - (it_mkLambda_or_LetIn ~init - (List.map change_sort_in_predicate princ_info.predicates) - ) - princ_info.params - - -let pp_dur time time' = - str (string_of_float (System.time_difference time time')) - -(* let qed () = save_named true *) -let defined () = - try - Command.save_named false - with - | UserError("extract_proof",msg) -> - Util.errorlabstrm - "defined" - ((try - str "On goal : " ++ fnl () ++ pr_open_subgoals () ++ fnl () - with _ -> mt () - ) ++msg) - | e -> raise e - - - -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 - (* let time1 = System.get_time () in *) - let new_principle_type = - compute_new_princ_type_from_rel - (Array.map mkConst funs) - sorts - old_princ_type - in - (* 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 new_principle_type) - ; - (* 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 - = - try - 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 = Flags.boxed_definitions() - } - in - ignore( - Declare.declare_constant - name - (Entries.DefinitionEntry ce, - Decl_kinds.IsDefinition (Decl_kinds.Scheme) - ) - ); - Flags.if_verbose - (fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined")) - name; - 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 - (* Pr 1278 : - Don't forget to close the goal if an error is raised !!!! - *) - save false new_princ_name entry g_kind hook - with e -> - begin - begin - try - let id = Pfedit.get_current_proof_name () in - let s = string_of_id id in - let n = String.length "___________princ_________" in - if String.length s >= n - then if String.sub s 0 n = "___________princ_________" - then Pfedit.delete_current_proof () - else () - else () - with _ -> () - end; - raise (Defining_principle e) - end -(* defined () *) - - -exception Not_Rec - -let get_funs_constant mp dp = - let rec get_funs_constant const e : (Names.constant*int) array = - match kind_of_term (snd (decompose_lam e)) with - | Fix((_,(na,_,_))) -> - Array.mapi - (fun i na -> - match na with - | Name id -> - let const = make_con mp dp (label_of_id id) in - const,i - | Anonymous -> - anomaly "Anonymous fix" - ) - na - | _ -> [|const,0|] - in - function const -> - let find_constant_body const = - match (Global.lookup_constant const ).const_body with - | Some b -> - let body = force b in - let body = Tacred.cbv_norm_flags - (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) - (Global.env ()) - (Evd.empty) - body - in - body - | None -> error ( "Cannot define a principle over an axiom ") - in - let f = find_constant_body const in - let l_const = get_funs_constant const f in - (* - We need to check that all the functions found are in the same block - to prevent Reset stange 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 decompose_lam l_bodies) in - (* all the paremeter must be equal*) - let _check_params = - let first_params = List.hd l_params in - List.iter - (fun params -> - if not ((=) first_params params) - then error "Not a mutal recursive block" - ) - l_params - in - (* The bodies has to be very similar *) - let _check_bodies = - try - let extract_info is_first body = - match kind_of_term body with - | Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca) - | _ -> - if is_first && (List.length l_bodies = 1) - then raise Not_Rec - else error "Not a mutal recursive block" - in - let first_infos = extract_info true (List.hd l_bodies) in - let check body = (* Hope this is correct *) - if not (first_infos = (extract_info false body)) - then error "Not a mutal recursive block" - in - List.iter check l_bodies - with Not_Rec -> () - in - l_const - -exception No_graph_found -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 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 - 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 - let funs_indexes = - let this_block_funs_indexes = Array.to_list this_block_funs_indexes in - List.map - (function const -> List.assoc const this_block_funs_indexes) - funs - in - let ind_list = - List.map - (fun (idx) -> - let ind = first_fun_kn,idx in - let (mib,mip) = Global.lookup_inductive ind in - ind,mib,mip,true,prop_sort - ) - funs_indexes - 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) -> - Termops.new_sort_in_family (Pretyping.interp_elimination_sort x) - ) - fas - in - (* 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,_,_)) = - try - 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 _ _ _ -> ()) - with e -> - begin - begin - try - let id = Pfedit.get_current_proof_name () in - let s = string_of_id id in - let n = String.length "___________princ_________" in - if String.length s >= n - then if String.sub s 0 n = "___________princ_________" - then Pfedit.delete_current_proof () - else () - else () - with _ -> () - end; - raise (Defining_principle e) - end - - in - incr i; - let opacity = - let finfos = find_Function_infos this_block_funs.(0) in - try - let equation = Option.get finfos.equation_lemma in - (Global.lookup_constant equation).Declarations.const_opaque - with Option.IsNone -> (* non recursive definition *) - false - in - let const = {const with const_entry_opaque = opacity } in - (* 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 = - 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)); - Flags.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,_) -> - 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,_ = 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 - let funs_indexes = - let this_block_funs_indexes = Array.to_list this_block_funs_indexes in - List.assoc (destConst funs) this_block_funs_indexes - in - let ind_fun = - let ind = first_fun_kn,funs_indexes in - ind,prop_sort - in - let scheme_type = (Typing.type_of env sigma ) ((fun (ind,sf) -> Indrec.make_case_gen env sigma ind sf) ind_fun) in - let sorts = - (fun (_,_,x) -> - Termops.new_sort_in_family (Pretyping.interp_elimination_sort x) - ) - fa - in - let princ_name = (fun (x,_,_) -> x) fa in - let _ = -(* 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 ([|sorts|])) - (Some princ_name) - this_block_funs - 0 - (prove_princ_for_struct false 0 [|destConst funs|]) - in - () |