aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_types.ml2
-rw-r--r--plugins/funind/functional_principles_types.mli6
-rw-r--r--plugins/funind/g_indfun.ml42
-rw-r--r--plugins/funind/glob_term_to_relation.ml2
-rw-r--r--plugins/funind/glob_termops.ml24
-rw-r--r--plugins/funind/glob_termops.mli6
-rw-r--r--plugins/funind/invfun.ml2
-rw-r--r--plugins/funind/merge.ml20
8 files changed, 32 insertions, 32 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index c297f4965..0cc5af99f 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -501,7 +501,7 @@ let get_funs_constant mp dp =
exception No_graph_found
exception Found_type of int
-let make_scheme (fas : (constant*Glob_term.rawsort) list) : Entries.definition_entry list =
+let make_scheme (fas : (constant*Glob_term.glob_sort) list) : Entries.definition_entry list =
let env = Global.env ()
and sigma = Evd.empty in
let funs = List.map fst fas in
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index 24c8359dc..1c02c16ec 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -27,8 +27,8 @@ val compute_new_princ_type_from_rel : constr array -> sorts array ->
exception No_graph_found
-val make_scheme : (constant*Glob_term.rawsort) list -> Entries.definition_entry list
+val make_scheme : (constant*Glob_term.glob_sort) list -> Entries.definition_entry list
-val build_scheme : (identifier*Libnames.reference*Glob_term.rawsort) list -> unit
-val build_case_scheme : (identifier*Libnames.reference*Glob_term.rawsort) -> unit
+val build_scheme : (identifier*Libnames.reference*Glob_term.glob_sort) list -> unit
+val build_case_scheme : (identifier*Libnames.reference*Glob_term.glob_sort) -> unit
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 90f7b5970..fb053c032 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -167,7 +167,7 @@ END
let pr_fun_scheme_arg (princ_name,fun_name,s) =
Nameops.pr_id princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++
Libnames.pr_reference fun_name ++ spc() ++ str "Sort " ++
- Ppconstr.pr_rawsort s
+ Ppconstr.pr_glob_sort s
VERNAC ARGUMENT EXTEND fun_scheme_arg
PRINTED BY pr_fun_scheme_arg
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index ce224d1aa..62cf3ccba 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1200,7 +1200,7 @@ let rec rebuild_return_type rt =
Topconstr.CArrow(loc,t,rebuild_return_type t')
| Topconstr.CLetIn(loc,na,t,t') ->
Topconstr.CLetIn(loc,na,t,rebuild_return_type t')
- | _ -> Topconstr.CArrow(dummy_loc,rt,Topconstr.CSort(dummy_loc,RType None))
+ | _ -> Topconstr.CArrow(dummy_loc,rt,Topconstr.CSort(dummy_loc,GType None))
let do_build_inductive
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 0cf91f38c..3fa1f6714 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -586,28 +586,28 @@ let id_of_name = function
| Names.Name x -> x
(* TODO: finish Rec caes *)
-let ids_of_rawterm c =
- let rec ids_of_rawterm acc c =
+let ids_of_glob_constr c =
+ let rec ids_of_glob_constr acc c =
let idof = id_of_name in
match c with
| GVar (_,id) -> id::acc
| GApp (loc,g,args) ->
- ids_of_rawterm [] g @ List.flatten (List.map (ids_of_rawterm []) args) @ acc
- | GLambda (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
- | GProd (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
- | GLetIn (loc,na,b,c) -> idof na :: ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc
- | GCast (loc,c,CastConv(k,t)) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc
- | GCast (loc,c,CastCoerce) -> ids_of_rawterm [] c @ acc
- | GIf (loc,c,(na,po),b1,b2) -> ids_of_rawterm [] c @ ids_of_rawterm [] b1 @ ids_of_rawterm [] b2 @ acc
+ ids_of_glob_constr [] g @ List.flatten (List.map (ids_of_glob_constr []) args) @ acc
+ | GLambda (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc
+ | GProd (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc
+ | GLetIn (loc,na,b,c) -> idof na :: ids_of_glob_constr [] b @ ids_of_glob_constr [] c @ acc
+ | GCast (loc,c,CastConv(k,t)) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] t @ acc
+ | GCast (loc,c,CastCoerce) -> ids_of_glob_constr [] c @ acc
+ | GIf (loc,c,(na,po),b1,b2) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] b1 @ ids_of_glob_constr [] b2 @ acc
| GLetTuple (_,nal,(na,po),b,c) ->
- List.map idof nal @ ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc
+ List.map idof nal @ ids_of_glob_constr [] b @ ids_of_glob_constr [] c @ acc
| GCases (loc,sty,rtntypopt,tml,brchl) ->
- List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_rawterm [] c) brchl)
+ List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_glob_constr [] c) brchl)
| GRec _ -> failwith "Fix inside a constructor branch"
| (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GDynamic _) -> []
in
(* build the set *)
- List.fold_left (fun acc x -> Idset.add x acc) Idset.empty (ids_of_rawterm [] c)
+ List.fold_left (fun acc x -> Idset.add x acc) Idset.empty (ids_of_glob_constr [] c)
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index b6c407a24..3afb86298 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -23,7 +23,7 @@ val mkRLambda : Names.name * glob_constr * glob_constr -> glob_constr
val mkRProd : Names.name * glob_constr * glob_constr -> glob_constr
val mkRLetIn : Names.name * glob_constr * glob_constr -> glob_constr
val mkRCases : glob_constr option * tomatch_tuples * cases_clauses -> glob_constr
-val mkRSort : rawsort -> glob_constr
+val mkRSort : glob_sort -> glob_constr
val mkRHole : unit -> glob_constr (* we only build Evd.BinderType Anonymous holes *)
val mkRCast : glob_constr* glob_constr -> glob_constr
(*
@@ -115,10 +115,10 @@ val eq_cases_pattern : cases_pattern -> cases_pattern -> bool
val ids_of_pat : cases_pattern -> Names.Idset.t
(* TODO: finish this function (Fix not treated) *)
-val ids_of_rawterm: glob_constr -> Names.Idset.t
+val ids_of_glob_constr: glob_constr -> Names.Idset.t
(*
- removing let_in construction in a rawterm
+ removing let_in construction in a glob_constr
*)
val zeta_normalize : Glob_term.glob_constr -> Glob_term.glob_constr
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 4e5fb953d..426b496dd 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -774,7 +774,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
(fun entry ->
(entry.Entries.const_entry_body, Option.get entry.Entries.const_entry_type )
)
- (make_scheme (array_map_to_list (fun const -> const,Glob_term.RType None) funs))
+ (make_scheme (array_map_to_list (fun const -> const,Glob_term.GType None) funs))
)
in
let proving_tac =
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 7c32c1d20..4eedf8dc2 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -381,11 +381,11 @@ let build_raw_params prms_decl avoid =
let _ = prNamedRConstr "RAWDUMMY" dummy_glob_constr in
let res,_ = glob_decompose_prod dummy_glob_constr in
let comblist = List.combine prms_decl res in
- comblist, res , (avoid @ (Idset.elements (ids_of_rawterm dummy_glob_constr)))
+ comblist, res , (avoid @ (Idset.elements (ids_of_glob_constr dummy_glob_constr)))
*)
let ids_of_rawlist avoid rawl =
- List.fold_left Idset.union avoid (List.map ids_of_rawterm rawl)
+ List.fold_left Idset.union avoid (List.map ids_of_glob_constr rawl)
@@ -463,7 +463,7 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array
([],[],[],[]) arity_ctxt in
(* let arity_ctxt2 =
build_raw_params oib2.mind_arity_ctxt
- (Idset.elements (ids_of_rawterm oib1.mind_arity_ctxt)) in*)
+ (Idset.elements (ids_of_glob_constr oib1.mind_arity_ctxt)) in*)
let recprms1,otherprms1,args1,funresprms1 = bldprms (List.rev oib1.mind_arity_ctxt) mlnk1 in
let _ = prstr "\n\n\n" in
let recprms2,otherprms2,args2,funresprms2 = bldprms (List.rev oib2.mind_arity_ctxt) mlnk2 in
@@ -756,7 +756,7 @@ let merge_constructor_id id1 id2 shift:identifier =
(** [merge_constructors lnk shift avoid] merges the two list of
- constructor [(name*type)]. These are translated to rawterms
+ constructor [(name*type)]. These are translated to glob_constr
first, each of them having distinct var names. *)
let rec merge_constructors (shift:merge_infos) (avoid:Idset.t)
(typcstr1:(identifier * glob_constr) list)
@@ -816,7 +816,7 @@ let rec merge_mutual_inductive_body
merge_inductive_body shift Idset.empty mib1.mind_packets.(0) mib2.mind_packets.(0)
-let rawterm_to_constr_expr x = (* build a constr_expr from a glob_constr *)
+let glob_constr_to_constr_expr x = (* build a constr_expr from a glob_constr *)
Flags.with_option Flags.raw_print (Constrextern.extern_glob_type Idset.empty) x
let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
@@ -827,7 +827,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
let _ = prstr "param :" in
let _ = prNamedRConstr (string_of_name nme) tp in
let _ = prstr " ; " in
- let typ = rawterm_to_constr_expr tp in
+ let typ = glob_constr_to_constr_expr tp in
LocalRawAssum ([(dummy_loc,nme)], Topconstr.default_binder_kind, typ) :: acc)
[] params in
let concl = Constrextern.extern_constr false (Global.env()) concl in
@@ -844,18 +844,18 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
-(** [rawterm_list_to_inductive_expr ident rawlist] returns the
+(** [glob_constr_list_to_inductive_expr ident rawlist] returns the
induct_expr corresponding to the the list of constructor types
[rawlist], named ident.
FIXME: params et cstr_expr (arity) *)
-let rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
+let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
(rawlist:(identifier * glob_constr) list) =
let lident = dummy_loc, shift.ident in
let bindlist , cstr_expr = (* params , arities *)
merge_rec_params_and_arity prms1 prms2 shift mkSet in
let lcstor_expr : (bool * (lident * constr_expr)) list =
List.map (* zeta_normalize t ? *)
- (fun (id,t) -> false, ((dummy_loc,id),rawterm_to_constr_expr t))
+ (fun (id,t) -> false, ((dummy_loc,id),glob_constr_to_constr_expr t))
rawlist in
lident , bindlist , Some cstr_expr , lcstor_expr
@@ -901,7 +901,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
recprms1=prms1;
recprms1=prms1;
} in *)
- let indexpr = rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in
+ let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in
(* Declare inductive *)
let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in
let mie,impls = Command.interp_mutual_inductive indl [] true (* means: not coinductive *) in
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 03:10:48 +0000