summaryrefslogtreecommitdiff
path: root/plugins/funind/merge.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/merge.ml')
-rw-r--r--plugins/funind/merge.ml133
1 files changed, 63 insertions, 70 deletions
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 40ee116d..4eedf8dc 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -8,7 +8,6 @@
(* Merging of induction principles. *)
-(*i $Id: i*)
open Libnames
open Tactics
open Indfun_common
@@ -21,12 +20,12 @@ open Term
open Termops
open Declarations
open Environ
-open Rawterm
-open Rawtermops
+open Glob_term
+open Glob_termops
(** {1 Utilities} *)
-(** {2 Useful operations on constr and rawconstr} *)
+(** {2 Useful operations on constr and glob_constr} *)
let rec popn i c = if i<=0 then c else pop (popn (i-1) c)
@@ -61,7 +60,7 @@ let string_of_name nme = string_of_id (id_of_name nme)
(** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *)
let isVarf f x =
match x with
- | RVar (_,x) -> Pervasives.compare x f = 0
+ | GVar (_,x) -> Pervasives.compare x f = 0
| _ -> false
(** [ident_global_exist id] returns true if identifier [id] is linked
@@ -98,7 +97,7 @@ let prNamedConstr s c =
let prNamedRConstr s c =
begin
msg(str "");
- msg(str(s^" {§ ") ++ Printer.pr_rawconstr c ++ str " §} ");
+ msg(str(s^" {§ ") ++ Printer.pr_glob_constr c ++ str " §} ");
msg(str "");
end
let prNamedLConstr_aux lc = List.iter (prNamedConstr "\n") lc
@@ -130,7 +129,7 @@ let prNamedRLDecl s lc =
end
let showind (id:identifier) =
- let cstrid = Tacinterp.constr_of_id (Global.env()) id in
+ let cstrid = Constrintern.global_reference id in
let ind1,cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty cstrid in
let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) ind1 in
List.iter (fun (nm, optcstr, tp) ->
@@ -378,15 +377,15 @@ let verify_inds mib1 mib2 =
let build_raw_params prms_decl avoid =
let dummy_constr = compose_prod (List.map (fun (x,_,z) -> x,z) prms_decl) (mkRel 1) in
let _ = prNamedConstr "DUMMY" dummy_constr in
- let dummy_rawconstr = Detyping.detype false avoid [] dummy_constr in
- let _ = prNamedRConstr "RAWDUMMY" dummy_rawconstr in
- let res,_ = raw_decompose_prod dummy_rawconstr in
+ let dummy_glob_constr = Detyping.detype false avoid [] dummy_constr in
+ 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_rawconstr)))
+ 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)
@@ -464,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
@@ -512,37 +511,37 @@ exception NoMerge
let rec merge_app c1 c2 id1 id2 shift filter_shift_stable =
let lnk = Array.append shift.lnk1 shift.lnk2 in
match c1 , c2 with
- | RApp(_,f1, arr1), RApp(_,f2,arr2) when isVarf id1 f1 && isVarf id2 f2 ->
+ | GApp(_,f1, arr1), GApp(_,f2,arr2) when isVarf id1 f1 && isVarf id2 f2 ->
let _ = prstr "\nICI1!\n";Pp.flush_all() in
let args = filter_shift_stable lnk (arr1 @ arr2) in
- RApp (dummy_loc,RVar (dummy_loc,shift.ident) , args)
- | RApp(_,f1, arr1), RApp(_,f2,arr2) -> raise NoMerge
- | RLetIn(_,nme,bdy,trm) , _ ->
+ GApp (dummy_loc,GVar (dummy_loc,shift.ident) , args)
+ | GApp(_,f1, arr1), GApp(_,f2,arr2) -> raise NoMerge
+ | GLetIn(_,nme,bdy,trm) , _ ->
let _ = prstr "\nICI2!\n";Pp.flush_all() in
let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in
- RLetIn(dummy_loc,nme,bdy,newtrm)
- | _, RLetIn(_,nme,bdy,trm) ->
+ GLetIn(dummy_loc,nme,bdy,newtrm)
+ | _, GLetIn(_,nme,bdy,trm) ->
let _ = prstr "\nICI3!\n";Pp.flush_all() in
let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in
- RLetIn(dummy_loc,nme,bdy,newtrm)
+ GLetIn(dummy_loc,nme,bdy,newtrm)
| _ -> let _ = prstr "\nICI4!\n";Pp.flush_all() in
raise NoMerge
let rec merge_app_unsafe c1 c2 shift filter_shift_stable =
let lnk = Array.append shift.lnk1 shift.lnk2 in
match c1 , c2 with
- | RApp(_,f1, arr1), RApp(_,f2,arr2) ->
+ | GApp(_,f1, arr1), GApp(_,f2,arr2) ->
let args = filter_shift_stable lnk (arr1 @ arr2) in
- RApp (dummy_loc,RVar(dummy_loc,shift.ident) , args)
+ GApp (dummy_loc,GVar(dummy_loc,shift.ident) , args)
(* FIXME: what if the function appears in the body of the let? *)
- | RLetIn(_,nme,bdy,trm) , _ ->
+ | GLetIn(_,nme,bdy,trm) , _ ->
let _ = prstr "\nICI2 '!\n";Pp.flush_all() in
let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in
- RLetIn(dummy_loc,nme,bdy,newtrm)
- | _, RLetIn(_,nme,bdy,trm) ->
+ GLetIn(dummy_loc,nme,bdy,newtrm)
+ | _, GLetIn(_,nme,bdy,trm) ->
let _ = prstr "\nICI3 '!\n";Pp.flush_all() in
let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in
- RLetIn(dummy_loc,nme,bdy,newtrm)
+ GLetIn(dummy_loc,nme,bdy,newtrm)
| _ -> let _ = prstr "\nICI4 '!\n";Pp.flush_all() in raise NoMerge
@@ -551,24 +550,24 @@ let rec merge_app_unsafe c1 c2 shift filter_shift_stable =
calls of branch 1 with all rec calls of branch 2. *)
(* TODO: reecrire cette heuristique (jusqu'a merge_types) *)
let rec merge_rec_hyps shift accrec
- (ltyp:(Names.name * rawconstr option * rawconstr option) list)
- filter_shift_stable : (Names.name * rawconstr option * rawconstr option) list =
+ (ltyp:(Names.name * glob_constr option * glob_constr option) list)
+ filter_shift_stable : (Names.name * glob_constr option * glob_constr option) list =
let mergeonehyp t reldecl =
match reldecl with
- | (nme,x,Some (RApp(_,i,args) as ind))
+ | (nme,x,Some (GApp(_,i,args) as ind))
-> nme,x, Some (merge_app_unsafe ind t shift filter_shift_stable)
| (nme,Some _,None) -> error "letins with recursive calls not treated yet"
| (nme,None,Some _) -> assert false
| (nme,None,None) | (nme,Some _,Some _) -> assert false in
match ltyp with
| [] -> []
- | (nme,None,Some (RApp(_,f, largs) as t)) :: lt when isVarf ind2name f ->
+ | (nme,None,Some (GApp(_,f, largs) as t)) :: lt when isVarf ind2name f ->
let rechyps = List.map (mergeonehyp t) accrec in
rechyps @ merge_rec_hyps shift accrec lt filter_shift_stable
| e::lt -> e :: merge_rec_hyps shift accrec lt filter_shift_stable
-let rec build_suppl_reccall (accrec:(name * rawconstr) list) concl2 shift =
+let rec build_suppl_reccall (accrec:(name * glob_constr) list) concl2 shift =
List.map (fun (nm,tp) -> (nm,merge_app_unsafe tp concl2 shift)) accrec
@@ -578,7 +577,7 @@ let find_app (nme:identifier) ltyp =
(List.map
(fun x ->
match x with
- | _,None,Some (RApp(_,f,_)) when isVarf nme f -> raise (Found 0)
+ | _,None,Some (GApp(_,f,_)) when isVarf nme f -> raise (Found 0)
| _ -> ())
ltyp);
false
@@ -592,9 +591,9 @@ let prnt_prod_or_letin nm letbdy typ =
let rec merge_types shift accrec1
- (ltyp1:(name * rawconstr option * rawconstr option) list)
- (concl1:rawconstr) (ltyp2:(name * rawconstr option * rawconstr option) list) concl2
- : (name * rawconstr option * rawconstr option) list * rawconstr =
+ (ltyp1:(name * glob_constr option * glob_constr option) list)
+ (concl1:glob_constr) (ltyp2:(name * glob_constr option * glob_constr option) list) concl2
+ : (name * glob_constr option * glob_constr option) list * glob_constr =
let _ = prstr "MERGE_TYPES\n" in
let _ = prstr "ltyp 1 : " in
let _ = List.iter (fun (nm,lbdy,tp) -> prnt_prod_or_letin nm lbdy tp) ltyp1 in
@@ -638,7 +637,7 @@ let rec merge_types shift accrec1
rechyps , concl
| (nme,None, Some t1)as e ::lt1 ->
(match t1 with
- | RApp(_,f,carr) when isVarf ind1name f ->
+ | GApp(_,f,carr) when isVarf ind1name f ->
merge_types shift (e::accrec1) lt1 concl1 ltyp2 concl2
| _ ->
let recres, recconcl2 =
@@ -705,8 +704,8 @@ let build_link_map allargs1 allargs2 lnk =
Precond: vars sets of [typcstr1] and [typcstr2] must be disjoint.
TODO: return nothing if equalities (after linking) are contradictory. *)
-let merge_one_constructor (shift:merge_infos) (typcstr1:rawconstr)
- (typcstr2:rawconstr) : rawconstr =
+let merge_one_constructor (shift:merge_infos) (typcstr1:glob_constr)
+ (typcstr2:glob_constr) : glob_constr =
(* FIXME: les noms des parametres corerspondent en principe au
parametres du niveau mib, mais il faudrait s'en assurer *)
(* shift.nfunresprmsx last args are functional result *)
@@ -714,17 +713,17 @@ let merge_one_constructor (shift:merge_infos) (typcstr1:rawconstr)
shift.mib1.mind_nparams + shift.oib1.mind_nrealargs - shift.nfunresprms1 in
let nargs2 =
shift.mib2.mind_nparams + shift.oib2.mind_nrealargs - shift.nfunresprms2 in
- let allargs1,rest1 = raw_decompose_prod_or_letin_n nargs1 typcstr1 in
- let allargs2,rest2 = raw_decompose_prod_or_letin_n nargs2 typcstr2 in
+ let allargs1,rest1 = glob_decompose_prod_or_letin_n nargs1 typcstr1 in
+ let allargs2,rest2 = glob_decompose_prod_or_letin_n nargs2 typcstr2 in
(* Build map of linked args of [typcstr2], and apply it to [typcstr2]. *)
let linked_map = build_link_map allargs1 allargs2 shift.lnk2 in
let rest2 = change_vars linked_map rest2 in
- let hyps1,concl1 = raw_decompose_prod_or_letin rest1 in
- let hyps2,concl2' = raw_decompose_prod_or_letin rest2 in
+ let hyps1,concl1 = glob_decompose_prod_or_letin rest1 in
+ let hyps2,concl2' = glob_decompose_prod_or_letin rest2 in
let ltyp,concl2 =
merge_types shift [] (List.rev hyps1) concl1 (List.rev hyps2) concl2' in
let _ = prNamedRLDecl "ltyp result:" ltyp in
- let typ = raw_compose_prod_or_letin concl2 (List.rev ltyp) in
+ let typ = glob_compose_prod_or_letin concl2 (List.rev ltyp) in
let revargs1 =
list_filteri (fun i _ -> isArg_stable shift.lnk1.(i)) (List.rev allargs1) in
let _ = prNamedRLDecl "ltyp allargs1" allargs1 in
@@ -734,7 +733,7 @@ let merge_one_constructor (shift:merge_infos) (typcstr1:rawconstr)
let _ = prNamedRLDecl "ltyp allargs2" allargs2 in
let _ = prNamedRLDecl "ltyp revargs2" revargs2 in
let typwithprms =
- raw_compose_prod_or_letin typ (List.rev revargs2 @ List.rev revargs1) in
+ glob_compose_prod_or_letin typ (List.rev revargs2 @ List.rev revargs1) in
typwithprms
@@ -757,11 +756,11 @@ 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 * rawconstr) list)
- (typcstr2:(identifier * rawconstr) list) : (identifier * rawconstr) list =
+ (typcstr1:(identifier * glob_constr) list)
+ (typcstr2:(identifier * glob_constr) list) : (identifier * glob_constr) list =
List.flatten
(List.map
(fun (id1,rawtyp1) ->
@@ -779,12 +778,12 @@ let rec merge_constructors (shift:merge_infos) (avoid:Idset.t)
info in [shift], avoiding identifiers in [avoid]. *)
let rec merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
(oib2:one_inductive_body) =
- (* building rawconstr type of constructors *)
+ (* building glob_constr type of constructors *)
let mkrawcor nme avoid typ =
(* first replace rel 1 by a varname *)
let substindtyp = substitterm 0 (mkRel 1) (mkVar nme) typ in
Detyping.detype false (Idset.elements avoid) [] substindtyp in
- let lcstr1: rawconstr list =
+ let lcstr1: glob_constr list =
Array.to_list (Array.map (mkrawcor ind1name avoid) oib1.mind_user_lc) in
(* add to avoid all indentifiers of lcstr1 *)
let avoid2 = Idset.union avoid (ids_of_rawlist avoid lcstr1) in
@@ -793,10 +792,10 @@ let rec merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
let avoid3 = Idset.union avoid (ids_of_rawlist avoid lcstr2) in
let params1 =
- try fst (raw_decompose_prod_n shift.nrecprms1 (List.hd lcstr1))
+ try fst (glob_decompose_prod_n shift.nrecprms1 (List.hd lcstr1))
with _ -> [] in
let params2 =
- try fst (raw_decompose_prod_n shift.nrecprms2 (List.hd lcstr2))
+ try fst (glob_decompose_prod_n shift.nrecprms2 (List.hd lcstr2))
with _ -> [] in
let lcstr1 = List.combine (Array.to_list oib1.mind_consnames) lcstr1 in
@@ -817,8 +816,8 @@ 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 rawconstr *)
- Flags.with_option Flags.raw_print (Constrextern.extern_rawtype Idset.empty) x
+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) =
let params = prms2 @ prms1 in
@@ -828,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
@@ -845,38 +844,38 @@ 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
- (rawlist:(identifier * rawconstr) list) =
+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
-let mkProd_reldecl (rdecl:rel_declaration) (t2:rawconstr) =
+let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) =
match rdecl with
| (nme,None,t) ->
let traw = Detyping.detype false [] [] t in
- RProd (dummy_loc,nme,Explicit,traw,t2)
+ GProd (dummy_loc,nme,Explicit,traw,t2)
| (_,Some _,_) -> assert false
-let mkProd_reldecl (rdecl:rel_declaration) (t2:rawconstr) =
+let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) =
match rdecl with
| (nme,None,t) ->
let traw = Detyping.detype false [] [] t in
- RProd (dummy_loc,nme,Explicit,traw,t2)
+ GProd (dummy_loc,nme,Explicit,traw,t2)
| (_,Some _,_) -> assert false
@@ -902,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
@@ -1024,9 +1023,3 @@ let relprinctype_to_funprinctype relprinctype nfuns =
url = "citeseer.ist.psu.edu/bundy93rippling.html" }
*)
-(*
-*** Local Variables: ***
-*** compile-command: "make -C ../.. plugins/funind/merge.cmo" ***
-*** indent-tabs-mode: nil ***
-*** End: ***
-*)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 10:24:49 +0000