aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/merge.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/merge.ml')
-rw-r--r--plugins/funind/merge.ml56
1 files changed, 28 insertions, 28 deletions
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 0af0898a0..b99a05dfb 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -65,14 +65,14 @@ let string_of_name = id_of_name %> Id.to_string
(** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *)
let isVarf f x =
match x with
- | GVar (_,x) -> Id.equal x f
+ | { CAst.v = GVar x } -> Id.equal x f
| _ -> false
(** [ident_global_exist id] returns true if identifier [id] is linked
in global environment. *)
let ident_global_exist id =
try
- let ans = CRef (Libnames.Ident (Loc.ghost,id), None) in
+ let ans = CAst.make @@ CRef (Libnames.Ident (Loc.tag id), None) in
let _ = ignore (Constrintern.intern_constr (Global.env()) ans) in
true
with e when CErrors.noncritical e -> false
@@ -505,38 +505,38 @@ 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
- | GApp(_,f1, arr1), GApp(_,f2,arr2) when isVarf id1 f1 && isVarf id2 f2 ->
+ match CAst.(c1.v, c2.v) with
+ | GApp(f1, arr1), GApp(f2,arr2) when isVarf id1 f1 && isVarf id2 f2 ->
let _ = prstr "\nICI1!\n" in
let args = filter_shift_stable lnk (arr1 @ arr2) in
- GApp (Loc.ghost,GVar (Loc.ghost,shift.ident) , args)
- | GApp(_,f1, arr1), GApp(_,f2,arr2) -> raise NoMerge
- | GLetIn(_,nme,bdy,typ,trm) , _ ->
+ CAst.make @@ GApp ((CAst.make @@ GVar shift.ident) , args)
+ | GApp(f1, arr1), GApp(f2,arr2) -> raise NoMerge
+ | GLetIn(nme,bdy,typ,trm) , _ ->
let _ = prstr "\nICI2!\n" in
let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in
- GLetIn(Loc.ghost,nme,bdy,typ,newtrm)
- | _, GLetIn(_,nme,bdy,typ,trm) ->
+ CAst.make @@ GLetIn(nme,bdy,typ,newtrm)
+ | _, GLetIn(nme,bdy,typ,trm) ->
let _ = prstr "\nICI3!\n" in
let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in
- GLetIn(Loc.ghost,nme,bdy,typ,newtrm)
+ CAst.make @@ GLetIn(nme,bdy,typ,newtrm)
| _ -> let _ = prstr "\nICI4!\n" 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
- | GApp(_,f1, arr1), GApp(_,f2,arr2) ->
+ match CAst.(c1.v, c2.v) with
+ | GApp(f1, arr1), GApp(f2,arr2) ->
let args = filter_shift_stable lnk (arr1 @ arr2) in
- GApp (Loc.ghost,GVar(Loc.ghost,shift.ident) , args)
+ CAst.make @@ GApp (CAst.make @@ GVar shift.ident, args)
(* FIXME: what if the function appears in the body of the let? *)
- | GLetIn(_,nme,bdy,typ,trm) , _ ->
+ | GLetIn(nme,bdy,typ,trm) , _ ->
let _ = prstr "\nICI2 '!\n" in
let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in
- GLetIn(Loc.ghost,nme,bdy,typ,newtrm)
- | _, GLetIn(_,nme,bdy,typ,trm) ->
+ CAst.make @@ GLetIn(nme,bdy,typ,newtrm)
+ | _, GLetIn(nme,bdy,typ,trm) ->
let _ = prstr "\nICI3 '!\n" in
let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in
- GLetIn(Loc.ghost,nme,bdy,typ,newtrm)
+ CAst.make @@ GLetIn(nme,bdy,typ,newtrm)
| _ -> let _ = prstr "\nICI4 '!\n" in raise NoMerge
@@ -549,14 +549,14 @@ let rec merge_rec_hyps shift accrec
filter_shift_stable : (Name.t * glob_constr option * glob_constr option) list =
let mergeonehyp t reldecl =
match reldecl with
- | (nme,x,Some (GApp(_,i,args) as ind))
+ | (nme,x,Some ({ CAst.v = 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 (GApp(_,f, largs) as t)) :: lt when isVarf ind2name f ->
+ | (nme,None,Some ({ CAst. v = 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
@@ -572,7 +572,7 @@ let find_app (nme:Id.t) ltyp =
(List.map
(fun x ->
match x with
- | _,None,Some (GApp(_,f,_)) when isVarf nme f -> raise (Found 0)
+ | _,None,Some { CAst.v = GApp(f,_)} when isVarf nme f -> raise (Found 0)
| _ -> ())
ltyp);
false
@@ -631,8 +631,8 @@ let rec merge_types shift accrec1
rechyps , concl
| (nme,None, Some t1)as e ::lt1 ->
- (match t1 with
- | GApp(_,f,carr) when isVarf ind1name f ->
+ (match t1.CAst.v with
+ | GApp(f,carr) when isVarf ind1name f ->
merge_types shift (e::accrec1) lt1 concl1 ltyp2 concl2
| _ ->
let recres, recconcl2 =
@@ -824,7 +824,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
let _ = prNamedRConstr (string_of_name nme) tp in
let _ = prstr " ; " in
let typ = glob_constr_to_constr_expr tp in
- CLocalAssum ([(Loc.ghost,nme)], Constrexpr_ops.default_binder_kind, typ) :: acc)
+ CLocalAssum ([(Loc.tag nme)], Constrexpr_ops.default_binder_kind, typ) :: acc)
[] params in
let concl = Constrextern.extern_constr false (Global.env()) Evd.empty concl in
let arity,_ =
@@ -834,7 +834,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
let c = RelDecl.get_type decl in
let typ = Constrextern.extern_constr false env Evd.empty c in
let newenv = Environ.push_rel (LocalAssum (nm,c)) env in
- CProdN (Loc.ghost, [[(Loc.ghost,nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv)
+ CAst.make @@ CProdN ([[(Loc.tag nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv)
(concl,Global.env())
(shift.funresprms2 @ shift.funresprms1
@ shift.args2 @ shift.args1 @ shift.otherprms2 @ shift.otherprms1) in
@@ -848,12 +848,12 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
FIXME: params et cstr_expr (arity) *)
let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
(rawlist:(Id.t * glob_constr) list) =
- let lident = (Loc.ghost, shift.ident), None in
+ let lident = (Loc.tag shift.ident), None 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, ((Loc.ghost,id),glob_constr_to_constr_expr t))
+ (fun (id,t) -> false, ((Loc.tag id),glob_constr_to_constr_expr t))
rawlist in
lident , bindlist , Some cstr_expr , lcstor_expr
@@ -863,7 +863,7 @@ let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) =
| LocalAssum (nme,t) ->
let t = EConstr.of_constr t in
let traw = Detyping.detype false [] (Global.env()) Evd.empty t in
- GProd (Loc.ghost,nme,Explicit,traw,t2)
+ CAst.make @@ GProd (nme,Explicit,traw,t2)
| LocalDef _ -> assert false
@@ -901,7 +901,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
(* Find infos on identifier id. *)
let find_Function_infos_safe (id:Id.t): Indfun_common.function_info =
let kn_of_id x =
- let f_ref = Libnames.Ident (Loc.ghost,x) in
+ let f_ref = Libnames.Ident (Loc.tag x) in
locate_with_msg (str "Don't know what to do with " ++ Libnames.pr_reference f_ref)
locate_constant f_ref in
try find_Function_infos (kn_of_id id)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 14:22:15 +0000