diff options
Diffstat (limited to 'plugins/funind/functional_principles_types.ml')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 30 |
1 files changed, 14 insertions, 16 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 18d63dd94..70245a8b1 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -1,3 +1,4 @@ +open API open Printer open CErrors open Util @@ -12,7 +13,6 @@ open Context.Rel.Declaration open Indfun_common open Functional_principles_proofs open Misctypes -open Sigma.Notations module RelDecl = Context.Rel.Declaration @@ -44,7 +44,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let id = Namegen.next_ident_away x avoid in Hashtbl.add tbl id x; RelDecl.set_name (Name id) decl :: change_predicates_names (id::avoid) predicates - | Anonymous -> anomaly (Pp.str "Anonymous property binder ")) + | Anonymous -> anomaly (Pp.str "Anonymous property binder.")) in let avoid = (Termops.ids_of_context env_with_params ) in let princ_type_info = @@ -62,7 +62,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = then List.tl args else args in - Context.Named.Declaration.LocalAssum (Nameops.out_name (Context.Rel.Declaration.get_name decl), + Context.Named.Declaration.LocalAssum (Nameops.Name.get_id (Context.Rel.Declaration.get_name decl), Term.compose_prod real_args (mkSort new_sort)) in let new_predicates = @@ -150,7 +150,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = ([],[]) in let new_f,binders_to_remove_from_f = compute_new_princ_type remove env f in - applist(new_f, new_args), + applistc 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 @@ -185,11 +185,11 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = with | Toberemoved -> -(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) +(* observe (str "Decl of "++Ppconstr.Name.print 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 "); *) +(* observe (str "Decl of "++Ppconstr.Name.print 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 @@ -214,11 +214,11 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = with | Toberemoved -> -(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) +(* observe (str "Decl of "++Ppconstr.Name.print 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 "); *) +(* observe (str "Decl of "++Ppconstr.Name.print 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 @@ -330,7 +330,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) match new_princ_name with | Some (id) -> id,id | None -> - let id_of_f = Label.to_id (con_label (fst f)) in + let id_of_f = Label.to_id (Constant.label (fst 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 @@ -389,17 +389,17 @@ let generate_functional_principle (evd: Evd.evar_map ref) exception Not_Rec let get_funs_constant mp dp = - let get_funs_constant const e : (Names.constant*int) array = + let get_funs_constant const e : (Names.Constant.t*int) array = match kind_of_term ((strip_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 + let const = Constant.make3 mp dp (Label.of_id id) in const,i | Anonymous -> - anomaly (Pp.str "Anonymous fix") + anomaly (Pp.str "Anonymous fix.") ) na | _ -> [|const,0|] @@ -656,7 +656,7 @@ let build_case_scheme fa = user_err ~hdr:"FunInd.build_case_scheme" (str "Cannot find " ++ Libnames.pr_reference f) in let first_fun,u = destConst funs in - let funs_mp,funs_dp,_ = Names.repr_con first_fun in + let funs_mp,funs_dp,_ = Constant.repr3 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 (fun (c,_) -> (c,u)) this_block_funs_indexes in @@ -669,11 +669,9 @@ let build_case_scheme fa = let ind = first_fun_kn,funs_indexes in (ind,Univ.Instance.empty)(*FIXME*),prop_sort in - let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma (scheme, sigma, _) = + let (sigma, scheme) = Indrec.build_case_analysis_scheme_default env sigma ind sf in - let sigma = Sigma.to_evar_map sigma in let scheme_type = EConstr.Unsafe.to_constr ((Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme)) in let sorts = (fun (_,_,x) -> |