aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/glob_term_to_relation.ml84
-rw-r--r--plugins/funind/glob_termops.ml146
-rw-r--r--plugins/funind/indfun.ml2
-rw-r--r--plugins/funind/indfun_common.ml4
-rw-r--r--plugins/funind/merge.ml42
-rw-r--r--plugins/funind/recdef.ml10
6 files changed, 147 insertions, 141 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 938fe52373..7f2b21e79d 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -345,10 +345,10 @@ let raw_push_named (na,raw_value,raw_typ) env =
let add_pat_variables pat typ env : Environ.env =
- let rec add_pat_variables env (loc, pat) typ : Environ.env =
+ let rec add_pat_variables env pat typ : Environ.env =
observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env));
- match pat with
+ match pat.CAst.v with
| PatVar na -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env
| PatCstr(c,patl,na) ->
let Inductiveops.IndType(indf,indargs) =
@@ -398,7 +398,7 @@ let add_pat_variables pat typ env : Environ.env =
-let rec pattern_to_term_and_type env typ = Loc.with_unloc (function
+let rec pattern_to_term_and_type env typ = CAst.with_val (function
| PatVar Anonymous -> assert false
| PatVar (Name id) ->
mkGVar id
@@ -466,11 +466,12 @@ let rec pattern_to_term_and_type env typ = Loc.with_unloc (function
let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
observe (str " Entering : " ++ Printer.pr_glob_constr rt);
- match rt with
- | _, GRef _ | _, GVar _ | _, GEvar _ | _, GPatVar _ | _, GSort _ | _, GHole _ ->
+ let open CAst in
+ match rt.v with
+ | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ ->
(* do nothing (except changing type of course) *)
mk_result [] rt avoid
- | _, GApp(_,_) ->
+ | GApp(_,_) ->
let f,args = glob_decompose_app rt in
let args_res : (glob_constr list) build_entry_return =
List.fold_right (* create the arguments lists of constructors and combine them *)
@@ -482,14 +483,14 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
(mk_result [] [] avoid)
in
begin
- match Loc.obj f with
+ match f.v with
| GLambda _ ->
let rec aux t l =
match l with
| [] -> t
- | u::l -> Loc.tag @@
- match t with
- | loc, GLambda(na,_,nat,b) ->
+ | u::l -> CAst.make @@
+ match t.v with
+ | GLambda(na,_,nat,b) ->
GLetIn(na,u,None,aux b l)
| _ ->
GApp(t,l)
@@ -550,7 +551,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
let new_b =
replace_var_by_term
id
- (Loc.tag @@ GVar id)
+ (CAst.make @@ GVar id)
b
in
(Name new_id,new_b,new_avoid)
@@ -579,7 +580,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
| GProd _ -> error "Cannot apply a type"
end (* end of the application treatement *)
- | _, GLambda(n,_,t,b) ->
+ | GLambda(n,_,t,b) ->
(* we first compute the list of constructor
corresponding to the body of the function,
then the one corresponding to the type
@@ -594,7 +595,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
let new_env = raw_push_named (new_n,None,t) env in
let b_res = build_entry_lc new_env funnames avoid b in
combine_results (combine_lam new_n) t_res b_res
- | _, GProd(n,_,t,b) ->
+ | GProd(n,_,t,b) ->
(* we first compute the list of constructor
corresponding to the body of the function,
then the one corresponding to the type
@@ -604,13 +605,13 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
let new_env = raw_push_named (n,None,t) env in
let b_res = build_entry_lc new_env funnames avoid b in
combine_results (combine_prod n) t_res b_res
- | loc, GLetIn(n,v,typ,b) ->
+ | GLetIn(n,v,typ,b) ->
(* we first compute the list of constructor
corresponding to the body of the function,
then the one corresponding to the value [t]
and combine the two result
*)
- let v = match typ with None -> v | Some t -> Loc.tag ?loc @@ GCast (v,CastConv t) in
+ let v = match typ with None -> v | Some t -> CAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in
let v_res = build_entry_lc env funnames avoid v in
let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in
let v_type = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr v_as_constr) in
@@ -622,13 +623,13 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
in
let b_res = build_entry_lc new_env funnames avoid b in
combine_results (combine_letin n) v_res b_res
- | _, GCases(_,_,el,brl) ->
+ | GCases(_,_,el,brl) ->
(* we create the discrimination function
and treat the case itself
*)
let make_discr = make_discr_match brl in
build_entry_lc_from_case env funnames make_discr el brl avoid
- | _, GIf(b,(na,e_option),lhs,rhs) ->
+ | GIf(b,(na,e_option),lhs,rhs) ->
let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
let b_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr b_as_constr) in
let (ind,_) =
@@ -651,7 +652,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
in
(* Pp.msgnl (str "new case := " ++ Printer.pr_glob_constr match_expr); *)
build_entry_lc env funnames avoid match_expr
- | _, GLetTuple(nal,_,b,e) ->
+ | GLetTuple(nal,_,b,e) ->
begin
let nal_as_glob_constr =
List.map
@@ -677,8 +678,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
build_entry_lc env funnames avoid match_expr
end
- | _, GRec _ -> error "Not handled GRec"
- | _, GCast(b,_) ->
+ | GRec _ -> error "Not handled GRec"
+ | GCast(b,_) ->
build_entry_lc env funnames avoid b
and build_entry_lc_from_case env funname make_discr
(el:tomatch_tuples)
@@ -860,8 +861,8 @@ let is_res id =
-let same_raw_term (_,rt1) (_,rt2) =
- match rt1,rt2 with
+let same_raw_term rt1 rt2 =
+ match CAst.(rt1.v, rt2.v) with
| GRef(r1,_), GRef (r2,_) -> Globnames.eq_gr r1 r2
| GHole _, GHole _ -> true
| _ -> false
@@ -894,16 +895,17 @@ exception Continue
let rec rebuild_cons env nb_args relname args crossed_types depth rt =
observe (str "rebuilding : " ++ pr_glob_constr rt);
let open Context.Rel.Declaration in
- match rt with
- | _, GProd(n,k,t,b) ->
+ let open CAst in
+ match rt.v with
+ | GProd(n,k,t,b) ->
let not_free_in_t id = not (is_free_in id t) in
let new_crossed_types = t::crossed_types in
begin
match t with
- | _, GApp(((_, GVar(res_id)) as res_rt),args') when is_res res_id ->
+ | { v = GApp(({ v = GVar res_id } as res_rt),args') } when is_res res_id ->
begin
match args' with
- | (_, (GVar this_relname))::args' ->
+ | { v = GVar this_relname }::args' ->
(*i The next call to mk_rel_id is
valid since we are constructing the graph
Ensures by: obvious
@@ -925,7 +927,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
| _ -> (* the first args is the name of the function! *)
assert false
end
- | loc1, GApp((loc2, GRef(eq_as_ref,_)),[ty;(loc3, GVar id);rt])
+ | { loc = loc1; v = GApp({ loc = loc2; v = GRef(eq_as_ref,_) },[ty; { loc = loc3; v = GVar id};rt]) }
when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous
->
begin
@@ -962,8 +964,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
let params,arg' =
((Util.List.chop nparam args'))
in
- let rt_typ = Loc.tag @@
- GApp(Loc.tag @@ GRef (Globnames.IndRef (fst ind),None),
+ let rt_typ = CAst.make @@
+ GApp(CAst.make @@ GRef (Globnames.IndRef (fst ind),None),
(List.map
(fun p -> Detyping.detype false []
env (Evd.from_env env)
@@ -973,7 +975,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
(mkGHole ()))))
in
let eq' =
- Loc.tag ?loc:loc1 @@ GApp(Loc.tag ?loc:loc2 @@GRef(jmeq,None),[ty;Loc.tag ?loc:loc3 @@ GVar id;rt_typ;rt])
+ CAst.make ?loc:loc1 @@ GApp(CAst.make ?loc:loc2 @@GRef(jmeq,None),[ty;CAst.make ?loc:loc3 @@ GVar id;rt_typ;rt])
in
observe (str "computing new type for jmeq : " ++ pr_glob_constr eq');
let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in
@@ -1042,7 +1044,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
mkGProd(n,t,new_b),id_to_exclude
else new_b, Id.Set.add id id_to_exclude
*)
- | loc1, GApp((loc2, GRef(eq_as_ref,_)),[ty;rt1;rt2])
+ | { loc = loc1; v = GApp({ loc = loc2; v = GRef(eq_as_ref,_) },[ty;rt1;rt2]) }
when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous
->
begin
@@ -1093,7 +1095,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
(Id.Set.filter not_free_in_t id_to_exclude)
| _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
end
- | _, GLambda(n,k,t,b) ->
+ | GLambda(n,k,t,b) ->
begin
let not_free_in_t id = not (is_free_in id t) in
let new_crossed_types = t :: crossed_types in
@@ -1112,14 +1114,14 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
then
new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
else
- Loc.tag @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
+ CAst.make @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
| _ -> anomaly (Pp.str "Should not have an anonymous function here")
(* We have renamed all the anonymous functions during alpha_renaming phase *)
end
- | loc, GLetIn(n,v,t,b) ->
+ | GLetIn(n,v,t,b) ->
begin
- let t = match t with None -> v | Some t -> Loc.tag ?loc @@ GCast (v,CastConv t) in
+ let t = match t with None -> v | Some t -> CAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in
let not_free_in_t id = not (is_free_in id t) in
let evd = (Evd.from_env env) in
let t',ctx = Pretyping.understand env evd t in
@@ -1135,10 +1137,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
match n with
| Name id when Id.Set.mem id id_to_exclude && depth >= nb_args ->
new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
- | _ -> Loc.tag @@ GLetIn(n,t,None,new_b), (* HOPING IT WOULD WORK *)
+ | _ -> CAst.make @@ GLetIn(n,t,None,new_b), (* HOPING IT WOULD WORK *)
Id.Set.filter not_free_in_t id_to_exclude
end
- | _, GLetTuple(nal,(na,rto),t,b) ->
+ | GLetTuple(nal,(na,rto),t,b) ->
assert (Option.is_empty rto);
begin
let not_free_in_t id = not (is_free_in id t) in
@@ -1161,7 +1163,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
(* | Name id when Id.Set.mem id id_to_exclude -> *)
(* new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) *)
(* | _ -> *)
- Loc.tag @@ GLetTuple(nal,(na,None),t,new_b),
+ CAst.make @@ GLetTuple(nal,(na,None),t,new_b),
Id.Set.filter not_free_in_t (Id.Set.union id_to_exclude id_to_exclude')
end
@@ -1187,9 +1189,9 @@ let rebuild_cons env nb_args relname args crossed_types rt =
TODO: Find a valid way to deal with implicit arguments here!
*)
-let rec compute_cst_params relnames params gt = Loc.with_unloc (function
+let rec compute_cst_params relnames params gt = CAst.with_val (function
| GRef _ | GVar _ | GEvar _ | GPatVar _ -> params
- | GApp((_, GVar relname'),rtl) when Id.Set.mem relname' relnames ->
+ | GApp({ CAst.v = GVar relname' },rtl) when Id.Set.mem relname' relnames ->
compute_cst_params_from_app [] (params,rtl)
| GApp(f,args) ->
List.fold_left (compute_cst_params relnames) params (f::args)
@@ -1211,7 +1213,7 @@ let rec compute_cst_params relnames params gt = Loc.with_unloc (function
and compute_cst_params_from_app acc (params,rtl) =
match params,rtl with
| _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *)
- | ((Name id,_,None) as param)::params',(_, GVar id')::rtl'
+ | ((Name id,_,None) as param)::params', { CAst.v = GVar id' }::rtl'
when Id.compare id id' == 0 ->
compute_cst_params_from_app (param::acc) (params',rtl')
| _ -> List.rev acc
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 66b9897d04..5abcb100f7 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -10,16 +10,16 @@ open Misctypes
Some basic functions to rebuild glob_constr
In each of them the location is Loc.ghost
*)
-let mkGRef ref = Loc.tag @@ GRef(ref,None)
-let mkGVar id = Loc.tag @@ GVar(id)
-let mkGApp(rt,rtl) = Loc.tag @@ GApp(rt,rtl)
-let mkGLambda(n,t,b) = Loc.tag @@ GLambda(n,Explicit,t,b)
-let mkGProd(n,t,b) = Loc.tag @@ GProd(n,Explicit,t,b)
-let mkGLetIn(n,b,t,c) = Loc.tag @@ GLetIn(n,b,t,c)
-let mkGCases(rto,l,brl) = Loc.tag @@ GCases(Term.RegularStyle,rto,l,brl)
-let mkGSort s = Loc.tag @@ GSort(s)
-let mkGHole () = Loc.tag @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None)
-let mkGCast(b,t) = Loc.tag @@ GCast(b,CastConv t)
+let mkGRef ref = CAst.make @@ GRef(ref,None)
+let mkGVar id = CAst.make @@ GVar(id)
+let mkGApp(rt,rtl) = CAst.make @@ GApp(rt,rtl)
+let mkGLambda(n,t,b) = CAst.make @@ GLambda(n,Explicit,t,b)
+let mkGProd(n,t,b) = CAst.make @@ GProd(n,Explicit,t,b)
+let mkGLetIn(n,b,t,c) = CAst.make @@ GLetIn(n,b,t,c)
+let mkGCases(rto,l,brl) = CAst.make @@ GCases(Term.RegularStyle,rto,l,brl)
+let mkGSort s = CAst.make @@ GSort(s)
+let mkGHole () = CAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None)
+let mkGCast(b,t) = CAst.make @@ GCast(b,CastConv t)
(*
Some basic functions to decompose glob_constrs
@@ -27,7 +27,7 @@ let mkGCast(b,t) = Loc.tag @@ GCast(b,CastConv t)
*)
let glob_decompose_prod =
let rec glob_decompose_prod args = function
- | _, GProd(n,k,t,b) ->
+ | { CAst.v = GProd(n,k,t,b) } ->
glob_decompose_prod ((n,t)::args) b
| rt -> args,rt
in
@@ -35,9 +35,9 @@ let glob_decompose_prod =
let glob_decompose_prod_or_letin =
let rec glob_decompose_prod args = function
- | _, GProd(n,k,t,b) ->
+ | { CAst.v = GProd(n,k,t,b) } ->
glob_decompose_prod ((n,None,Some t)::args) b
- | _, GLetIn(n,b,t,c) ->
+ | { CAst.v = GLetIn(n,b,t,c) } ->
glob_decompose_prod ((n,Some b,t)::args) c
| rt -> args,rt
in
@@ -59,7 +59,7 @@ let glob_decompose_prod_n n =
if i<=0 then args,c
else
match c with
- | _, GProd(n,_,t,b) ->
+ | { CAst.v = GProd(n,_,t,b) } ->
glob_decompose_prod (i-1) ((n,t)::args) b
| rt -> args,rt
in
@@ -71,9 +71,9 @@ let glob_decompose_prod_or_letin_n n =
if i<=0 then args,c
else
match c with
- | _, GProd(n,_,t,b) ->
+ | { CAst.v = GProd(n,_,t,b) } ->
glob_decompose_prod (i-1) ((n,None,Some t)::args) b
- | _, GLetIn(n,b,t,c) ->
+ | { CAst.v = GLetIn(n,b,t,c) } ->
glob_decompose_prod (i-1) ((n,Some b,t)::args) c
| rt -> args,rt
in
@@ -84,7 +84,7 @@ let glob_decompose_app =
let rec decompose_rapp acc rt =
(* msgnl (str "glob_decompose_app on : "++ Printer.pr_glob_constr rt); *)
match rt with
- | _, GApp(rt,rtl) ->
+ | { CAst.v = GApp(rt,rtl) } ->
decompose_rapp (List.fold_left (fun y x -> x::y) acc rtl) rt
| rt -> rt,List.rev acc
in
@@ -120,7 +120,7 @@ let remove_name_from_mapping mapping na =
let change_vars =
let rec change_vars mapping rt =
- Loc.map (function
+ CAst.map (function
| GRef _ as x -> x
| GVar id ->
let new_id =
@@ -189,18 +189,19 @@ let change_vars =
-let rec alpha_pat excluded (loc, pat) =
- match pat with
+let rec alpha_pat excluded pat =
+ let loc = pat.CAst.loc in
+ match pat.CAst.v with
| PatVar Anonymous ->
let new_id = Indfun_common.fresh_id excluded "_x" in
- (Loc.tag ?loc @@ PatVar(Name new_id)),(new_id::excluded),Id.Map.empty
+ (CAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded),Id.Map.empty
| PatVar(Name id) ->
if Id.List.mem id excluded
then
let new_id = Namegen.next_ident_away id excluded in
- (Loc.tag ?loc @@ PatVar(Name new_id)),(new_id::excluded),
+ (CAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded),
(Id.Map.add id new_id Id.Map.empty)
- else (Loc.tag ?loc pat),excluded,Id.Map.empty
+ else pat, excluded,Id.Map.empty
| PatCstr(constr,patl,na) ->
let new_na,new_excluded,map =
match na with
@@ -218,7 +219,7 @@ let rec alpha_pat excluded (loc, pat) =
([],new_excluded,map)
patl
in
- (Loc.tag ?loc @@ PatCstr(constr,List.rev new_patl,new_na)),new_excluded,new_map
+ (CAst.make ?loc @@ PatCstr(constr,List.rev new_patl,new_na)),new_excluded,new_map
let alpha_patl excluded patl =
let patl,new_excluded,map =
@@ -236,8 +237,8 @@ let alpha_patl excluded patl =
let raw_get_pattern_id pat acc =
- let rec get_pattern_id (loc, pat) =
- match pat with
+ let rec get_pattern_id pat =
+ match pat.CAst.v with
| PatVar(Anonymous) -> assert false
| PatVar(Name id) ->
[id]
@@ -254,10 +255,11 @@ let raw_get_pattern_id pat acc =
let get_pattern_id pat = raw_get_pattern_id pat []
-let rec alpha_rt excluded (loc, rt) =
- let new_rt = Loc.tag ?loc @@
- match rt with
- | GRef _ | GVar _ | GEvar _ | GPatVar _ -> rt
+let rec alpha_rt excluded rt =
+ let loc = rt.CAst.loc in
+ let new_rt = CAst.make ?loc @@
+ match rt.CAst.v with
+ | GRef _ | GVar _ | GEvar _ | GPatVar _ as rt -> rt
| GLambda(Anonymous,k,t,b) ->
let new_id = Namegen.next_ident_away (Id.of_string "_x") excluded in
let new_excluded = new_id :: excluded in
@@ -351,8 +353,8 @@ let rec alpha_rt excluded (loc, rt) =
alpha_rt excluded rhs
)
| GRec _ -> error "Not handled GRec"
- | GSort _ -> rt
- | GHole _ -> rt
+ | GSort _
+ | GHole _ as rt -> rt
| GCast (b,c) ->
GCast(alpha_rt excluded b,
Miscops.map_cast_type (alpha_rt excluded) c)
@@ -375,7 +377,7 @@ and alpha_br excluded (loc,(ids,patl,res)) =
[is_free_in id rt] checks if [id] is a free variable in [rt]
*)
let is_free_in id =
- let rec is_free_in (loc, gt) = match gt with
+ let rec is_free_in x = CAst.with_loc_val (fun ?loc -> function
| GRef _ -> false
| GVar id' -> Id.compare id' id == 0
| GEvar _ -> false
@@ -411,6 +413,7 @@ let is_free_in id =
| GHole _ -> false
| GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t
| GCast (b,CastCoerce) -> is_free_in b
+ ) x
and is_free_in_br (_,(ids,_,rt)) =
(not (Id.List.mem id ids)) && is_free_in rt
in
@@ -418,7 +421,7 @@ let is_free_in id =
-let rec pattern_to_term pt = Loc.with_unloc (function
+let rec pattern_to_term pt = CAst.with_val (function
| PatVar Anonymous -> assert false
| PatVar(Name id) ->
mkGVar id
@@ -445,39 +448,38 @@ let rec pattern_to_term pt = Loc.with_unloc (function
let replace_var_by_term x_id term =
- let rec replace_var_by_pattern (loc, rt) = Loc.tag ?loc @@
- match rt with
- | GRef _ -> rt
- | GVar id when Id.compare id x_id == 0 -> Loc.obj term
- | GVar _ -> rt
- | GEvar _ -> rt
- | GPatVar _ -> rt
+ let rec replace_var_by_pattern x = CAst.map (function
+ | GVar id when Id.compare id x_id == 0 -> term.CAst.v
+ | GRef _
+ | GVar _
+ | GEvar _
+ | GPatVar _ as rt -> rt
| GApp(rt',rtl) ->
GApp(replace_var_by_pattern rt',
List.map replace_var_by_pattern rtl
)
- | GLambda(Name id,_,_,_) when Id.compare id x_id == 0 -> rt
+ | GLambda(Name id,_,_,_) as rt when Id.compare id x_id == 0 -> rt
| GLambda(name,k,t,b) ->
GLambda(name,
k,
replace_var_by_pattern t,
replace_var_by_pattern b
)
- | GProd(Name id,_,_,_) when Id.compare id x_id == 0 -> rt
+ | GProd(Name id,_,_,_) as rt when Id.compare id x_id == 0 -> rt
| GProd(name,k,t,b) ->
GProd( name,
k,
replace_var_by_pattern t,
replace_var_by_pattern b
)
- | GLetIn(Name id,_,_,_) when Id.compare id x_id == 0 -> rt
+ | GLetIn(Name id,_,_,_) as rt when Id.compare id x_id == 0 -> rt
| GLetIn(name,def,typ,b) ->
GLetIn(name,
replace_var_by_pattern def,
Option.map (replace_var_by_pattern) typ,
replace_var_by_pattern b
)
- | GLetTuple(nal,_,_,_)
+ | GLetTuple(nal,_,_,_) as rt
when List.exists (function Name id -> Id.equal id x_id | _ -> false) nal ->
rt
| GLetTuple(nal,(na,rto),def,b) ->
@@ -499,11 +501,12 @@ let replace_var_by_term x_id term =
replace_var_by_pattern rhs
)
| GRec _ -> raise (UserError(None,str "Not handled GRec"))
- | GSort _ -> rt
- | GHole _ -> rt
+ | GSort _
+ | GHole _ as rt -> rt
| GCast(b,c) ->
GCast(replace_var_by_pattern b,
Miscops.map_cast_type replace_var_by_pattern c)
+ ) x
and replace_var_by_pattern_br ((loc,(idl,patl,res)) as br) =
if List.exists (fun id -> Id.compare id x_id == 0) idl
then br
@@ -520,9 +523,10 @@ exception NotUnifiable
let rec are_unifiable_aux = function
| [] -> ()
| eq::eqs ->
+ let open CAst in
match eq with
- | (_,PatVar _),_ | _,(_,PatVar _) -> are_unifiable_aux eqs
- | (_,PatCstr(constructor1,cpl1,_)),(_,PatCstr(constructor2,cpl2,_)) ->
+ | { v = PatVar _ },_ | _, { v = PatVar _ } -> are_unifiable_aux eqs
+ | { v = PatCstr(constructor1,cpl1,_) }, { v = PatCstr(constructor2,cpl2,_) } ->
if not (eq_constructor constructor2 constructor1)
then raise NotUnifiable
else
@@ -542,9 +546,10 @@ let are_unifiable pat1 pat2 =
let rec eq_cases_pattern_aux = function
| [] -> ()
| eq::eqs ->
+ let open CAst in
match eq with
- | (_,PatVar _),(_,PatVar _) -> eq_cases_pattern_aux eqs
- | (_,PatCstr(constructor1,cpl1,_)),(_,PatCstr(constructor2,cpl2,_)) ->
+ | { v = PatVar _ }, { v = PatVar _ } -> eq_cases_pattern_aux eqs
+ | { v = PatCstr(constructor1,cpl1,_) }, { v = PatCstr(constructor2,cpl2,_) } ->
if not (eq_constructor constructor2 constructor1)
then raise NotUnifiable
else
@@ -564,7 +569,7 @@ let eq_cases_pattern pat1 pat2 =
let ids_of_pat =
- let rec ids_of_pat ids = Loc.with_unloc (function
+ let rec ids_of_pat ids = CAst.with_val (function
| PatVar Anonymous -> ids
| PatVar(Name id) -> Id.Set.add id ids
| PatCstr(_,patl,_) -> List.fold_left ids_of_pat ids patl
@@ -578,7 +583,7 @@ let id_of_name = function
(* TODO: finish Rec caes *)
let ids_of_glob_constr c =
- let rec ids_of_glob_constr acc (loc, c) =
+ let rec ids_of_glob_constr acc {loc; CAst.v = c} =
let idof = id_of_name in
match c with
| GVar id -> id::acc
@@ -605,12 +610,11 @@ let ids_of_glob_constr c =
let zeta_normalize =
- let rec zeta_normalize_term (loc, rt) = Loc.tag ?loc @@
- match rt with
- | GRef _ -> rt
- | GVar _ -> rt
- | GEvar _ -> rt
- | GPatVar _ -> rt
+ let rec zeta_normalize_term x = CAst.map (function
+ | GRef _
+ | GVar _
+ | GEvar _
+ | GPatVar _ as rt -> rt
| GApp(rt',rtl) ->
GApp(zeta_normalize_term rt',
List.map zeta_normalize_term rtl
@@ -628,9 +632,9 @@ let zeta_normalize =
zeta_normalize_term b
)
| GLetIn(Name id,def,typ,b) ->
- Loc.obj @@ zeta_normalize_term (replace_var_by_term id def b)
+ (zeta_normalize_term (replace_var_by_term id def b)).CAst.v
| GLetIn(Anonymous,def,typ,b) ->
- Loc.obj @@ zeta_normalize_term b
+ (zeta_normalize_term b).CAst.v
| GLetTuple(nal,(na,rto),def,b) ->
GLetTuple(nal,
(na,Option.map zeta_normalize_term rto),
@@ -650,11 +654,12 @@ let zeta_normalize =
zeta_normalize_term rhs
)
| GRec _ -> raise (UserError(None,str "Not handled GRec"))
- | GSort _ -> rt
- | GHole _ -> rt
+ | GSort _
+ | GHole _ as rt -> rt
| GCast(b,c) ->
GCast(zeta_normalize_term b,
Miscops.map_cast_type zeta_normalize_term c)
+ ) x
and zeta_normalize_br (loc,(idl,patl,res)) =
(loc,(idl,patl,zeta_normalize_term res))
in
@@ -665,21 +670,19 @@ let zeta_normalize =
let expand_as =
- let rec add_as map (loc, pat) =
+ let rec add_as map ({loc; CAst.v = pat } as rt) =
match pat with
| PatVar _ -> map
| PatCstr(_,patl,Name id) ->
- Id.Map.add id (pattern_to_term (loc, pat)) (List.fold_left add_as map patl)
+ Id.Map.add id (pattern_to_term rt) (List.fold_left add_as map patl)
| PatCstr(_,patl,_) -> List.fold_left add_as map patl
in
- let rec expand_as map (loc, rt) =
- Loc.tag ?loc @@
- match rt with
- | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> rt
- | GVar id ->
+ let rec expand_as map = CAst.map (function
+ | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ as rt -> rt
+ | GVar id as rt ->
begin
try
- Loc.obj @@ Id.Map.find id map
+ (Id.Map.find id map).CAst.v
with Not_found -> rt
end
| GApp(f,args) -> GApp(expand_as map f,List.map (expand_as map) args)
@@ -699,6 +702,7 @@ let expand_as =
| GCases(sty,po,el,brl) ->
GCases(sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
List.map (expand_as_br map) brl)
+ )
and expand_as_br map (loc,(idl,cpl,rt)) =
(loc,(idl,cpl, expand_as (List.fold_left add_as map cpl) rt))
in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index f4e9aa3720..ab83cb15a6 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -190,7 +190,7 @@ let build_newrecursive l =
let is_rec names =
let names = List.fold_right Id.Set.add names Id.Set.empty in
let check_id id names = Id.Set.mem id names in
- let rec lookup names (loc, gt) = match gt with
+ let rec lookup names gt = match gt.CAst.v with
| GVar(id) -> check_id id names
| GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> false
| GCast(b,_) -> lookup names b
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index de8dc53f11..394b252aac 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -69,7 +69,7 @@ let chop_rlambda_n =
if n == 0
then List.rev acc,rt
else
- match Loc.obj rt with
+ match rt.CAst.v with
| Glob_term.GLambda(name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b
| Glob_term.GLetIn(name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b
| _ ->
@@ -83,7 +83,7 @@ let chop_rprod_n =
if n == 0
then List.rev acc,rt
else
- match Loc.obj rt with
+ match rt.CAst.v with
| Glob_term.GProd(name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b
| _ -> raise (CErrors.UserError(Some "chop_rprod_n",str "chop_rprod_n: Not enough products"))
in
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 5b51a213a1..d4865bf5ea 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -66,7 +66,7 @@ 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
@@ -504,40 +504,40 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array
exception NoMerge
-let rec merge_app (loc1, c1) (loc2, c2) id1 id2 shift filter_shift_stable =
+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
+ 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
- Loc.tag @@ GApp ((Loc.tag @@ GVar shift.ident) , args)
+ 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 (loc2, c2) id1 id2 shift filter_shift_stable in
- Loc.tag @@ GLetIn(nme,bdy,typ,newtrm)
+ let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in
+ CAst.make @@ GLetIn(nme,bdy,typ,newtrm)
| _, GLetIn(nme,bdy,typ,trm) ->
let _ = prstr "\nICI3!\n" in
- let newtrm = merge_app (loc1, c1) trm id1 id2 shift filter_shift_stable in
- Loc.tag @@ GLetIn(nme,bdy,typ,newtrm)
+ let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in
+ CAst.make @@ GLetIn(nme,bdy,typ,newtrm)
| _ -> let _ = prstr "\nICI4!\n" in
raise NoMerge
-let rec merge_app_unsafe (l1, c1) (l2, c2) shift filter_shift_stable =
+let rec merge_app_unsafe c1 c2 shift filter_shift_stable =
let lnk = Array.append shift.lnk1 shift.lnk2 in
- match c1 , c2 with
+ match CAst.(c1.v, c2.v) with
| GApp(f1, arr1), GApp(f2,arr2) ->
let args = filter_shift_stable lnk (arr1 @ arr2) in
- Loc.tag @@ GApp (Loc.tag @@ GVar 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) , _ ->
let _ = prstr "\nICI2 '!\n" in
- let newtrm = merge_app_unsafe trm (l2, c2) shift filter_shift_stable in
- Loc.tag @@ GLetIn(nme,bdy,typ,newtrm)
+ let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in
+ CAst.make @@ GLetIn(nme,bdy,typ,newtrm)
| _, GLetIn(nme,bdy,typ,trm) ->
let _ = prstr "\nICI3 '!\n" in
- let newtrm = merge_app_unsafe (l1, c1) trm shift filter_shift_stable in
- Loc.tag @@ GLetIn(nme,bdy,typ,newtrm)
+ let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in
+ CAst.make @@ GLetIn(nme,bdy,typ,newtrm)
| _ -> let _ = prstr "\nICI4 '!\n" in raise NoMerge
@@ -550,14 +550,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
@@ -573,7 +573,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
@@ -632,8 +632,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 =
@@ -864,7 +864,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
- Loc.tag @@ GProd (nme,Explicit,traw,t2)
+ CAst.make @@ GProd (nme,Explicit,traw,t2)
| LocalDef _ -> assert false
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 9e469c7564..8c88399448 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -188,15 +188,15 @@ let (value_f:Constr.constr list -> global_reference -> Constr.constr) =
in
let env = Environ.push_rel_context context (Global.env ()) in
let glob_body =
- Loc.tag @@
+ CAst.make @@
GCases
(RegularStyle,None,
- [Loc.tag @@ GApp(Loc.tag @@ GRef(fterm,None), List.rev_map (fun x_id -> Loc.tag @@ GVar x_id) rev_x_id_l),
+ [CAst.make @@ GApp(CAst.make @@ GRef(fterm,None), List.rev_map (fun x_id -> CAst.make @@ GVar x_id) rev_x_id_l),
(Anonymous,None)],
- [Loc.tag ([v_id], [Loc.tag @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1),
- [Loc.tag @@ PatVar(Name v_id); Loc.tag @@ PatVar Anonymous],
+ [Loc.tag ([v_id], [CAst.make @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1),
+ [CAst.make @@ PatVar(Name v_id); CAst.make @@ PatVar Anonymous],
Anonymous)],
- Loc.tag @@ GVar v_id)])
+ CAst.make @@ GVar v_id)])
in
let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in
it_mkLambda_or_LetIn body context
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 01:11:14 +0000