diff options
author | 2017-02-01 15:56:45 +0100 | |
---|---|---|
committer | 2017-03-24 12:22:21 +0100 | |
commit | f9a4ca41bc1313300f5f9b9092fe24825f435706 (patch) | |
tree | f2c6f100a01e26614a5ff6e7fe7471c7356b9de4 /plugins/funind | |
parent | 71cd2838bf3eb23a8f29df973d8012ebe2ec77b0 (diff) |
Replacing "cast surgery" in LetIn by a proper field (see PR #404).
This is a patch fulfilling the relevant remark of Maxime that an
explicit information at the ML type level would be better than "cast
surgery" to carry the optional type of a let-in.
There are a very few semantic changes.
- a "(x:t:=c)" in a block of binders is now written in the more
standard way "(x:=c:t)"
- in notations, the type of a let-in is not displayed if not
explicitly asked so.
See discussion at PR #417 for more information.
Diffstat (limited to 'plugins/funind')
-rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 73 | ||||
-rw-r--r-- | plugins/funind/glob_term_to_relation.mli | 2 | ||||
-rw-r--r-- | plugins/funind/glob_termops.ml | 60 | ||||
-rw-r--r-- | plugins/funind/glob_termops.mli | 2 | ||||
-rw-r--r-- | plugins/funind/indfun.ml | 16 | ||||
-rw-r--r-- | plugins/funind/indfun_common.ml | 4 | ||||
-rw-r--r-- | plugins/funind/indfun_common.mli | 2 | ||||
-rw-r--r-- | plugins/funind/merge.ml | 16 |
8 files changed, 97 insertions, 78 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 2426dd91c..084de31c0 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -42,7 +42,7 @@ let compose_glob_context = match bt with | Lambda n -> mkGLambda(n,t,acc) | Prod n -> mkGProd(n,t,acc) - | LetIn n -> mkGLetIn(n,t,acc) + | LetIn n -> mkGLetIn(n,t,None,acc) in List.fold_right compose_binder @@ -489,7 +489,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = | u::l -> match t with | GLambda(loc,na,_,nat,b) -> - GLetIn(Loc.ghost,na,u,aux b l) + GLetIn(Loc.ghost,na,u,None,aux b l) | _ -> GApp(Loc.ghost,t,l) in @@ -535,7 +535,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = args_res.result } | GApp _ -> assert false (* we have collected all the app in [glob_decompose_app] *) - | GLetIn(_,n,t,b) -> + | GLetIn(_,n,v,t,b) -> (* if we have [(let x := v in b) t1 ... tn] , we discard our work and compute the list of constructor for [let x = v in (b t1 ... tn)] up to alpha conversion @@ -559,7 +559,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = env funnames avoid - (mkGLetIn(new_n,t,mkGApp(new_b,args))) + (mkGLetIn(new_n,v,t,mkGApp(new_b,args))) | GCases _ | GIf _ | GLetTuple _ -> (* we have [(match e1, ...., en with ..... end) t1 tn] we first compute the result from the case and @@ -603,12 +603,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 - | GLetIn(_,n,v,b) -> + | GLetIn(loc,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 -> GCast (loc,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) v_as_constr in @@ -1115,8 +1116,9 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (* We have renamed all the anonymous functions during alpha_renaming phase *) end - | GLetIn(_,n,t,b) -> + | GLetIn(loc,n,v,t,b) -> begin + let t = match t with None -> v | Some t -> GCast (loc,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 @@ -1131,7 +1133,7 @@ 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) - | _ -> GLetIn(Loc.ghost,n,t,new_b), + | _ -> GLetIn(Loc.ghost,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) -> @@ -1189,9 +1191,13 @@ let rec compute_cst_params relnames params = function compute_cst_params_from_app [] (params,rtl) | GApp(_,f,args) -> List.fold_left (compute_cst_params relnames) params (f::args) - | GLambda(_,_,_,t,b) | GProd(_,_,_,t,b) | GLetIn(_,_,t,b) | GLetTuple(_,_,_,t,b) -> + | GLambda(_,_,_,t,b) | GProd(_,_,_,t,b) | GLetTuple(_,_,_,t,b) -> let t_params = compute_cst_params relnames params t in compute_cst_params relnames t_params b + | GLetIn(_,_,v,t,b) -> + let v_params = compute_cst_params relnames params v in + let t_params = Option.fold_left (compute_cst_params relnames) v_params t in + compute_cst_params relnames t_params b | GCases _ -> params (* If there is still cases at this point they can only be discrimination ones *) @@ -1202,12 +1208,12 @@ let rec compute_cst_params relnames params = 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,_,is_defined) as param)::params',(GVar(_,id'))::rtl' - when Id.compare id id' == 0 && not is_defined -> + | ((Name id,_,None) as param)::params',(GVar(_,id'))::rtl' + when Id.compare id id' == 0 -> compute_cst_params_from_app (param::acc) (params',rtl') | _ -> List.rev acc -let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool) list array) csts = +let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * glob_constr option) list array) csts = let rels_params = Array.mapi (fun i args -> @@ -1222,11 +1228,11 @@ let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool) let _ = try List.iteri - (fun i ((n,nt,is_defined) as param) -> + (fun i ((n,nt,typ) as param) -> if Array.for_all (fun l -> - let (n',nt',is_defined') = List.nth l i in - Name.equal n n' && glob_constr_eq nt nt' && (is_defined : bool) == is_defined') + let (n',nt',typ') = List.nth l i in + Name.equal n n' && glob_constr_eq nt nt' && Option.equal glob_constr_eq typ typ') rels_params then l := param::!l @@ -1241,15 +1247,15 @@ let rec rebuild_return_type rt = match rt with | Constrexpr.CProdN(loc,n,t') -> Constrexpr.CProdN(loc,n,rebuild_return_type t') - | Constrexpr.CLetIn(loc,na,t,t') -> - Constrexpr.CLetIn(loc,na,t,rebuild_return_type t') + | Constrexpr.CLetIn(loc,na,v,t,t') -> + Constrexpr.CLetIn(loc,na,v,t,rebuild_return_type t') | _ -> Constrexpr.CProdN(Loc.ghost,[[Loc.ghost,Anonymous], Constrexpr.Default Decl_kinds.Explicit,rt], Constrexpr.CSort(Loc.ghost,GType [])) let do_build_inductive - evd (funconstants: Term.pconstant list) (funsargs: (Name.t * glob_constr * bool) list list) + evd (funconstants: Term.pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list) returned_types (rtl:glob_constr list) = let _time1 = System.get_time () in @@ -1288,16 +1294,17 @@ let do_build_inductive let resa = Array.map (build_entry_lc env funnames_as_set []) rta in let env_with_graphs = let rel_arity i funargs = (* Rebuilding arities (with parameters) *) - let rel_first_args :(Name.t * Glob_term.glob_constr * bool ) list = + let rel_first_args :(Name.t * Glob_term.glob_constr * Glob_term.glob_constr option ) list = funargs in List.fold_right - (fun (n,t,is_defined) acc -> - if is_defined - then + (fun (n,t,typ) acc -> + match typ with + | Some typ -> Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, + Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ), acc) - else + | None -> Constrexpr.CProdN (Loc.ghost, [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], @@ -1355,16 +1362,17 @@ let do_build_inductive rel_constructors in let rel_arity i funargs = (* Reduilding arities (with parameters) *) - let rel_first_args :(Name.t * Glob_term.glob_constr * bool ) list = + let rel_first_args :(Name.t * Glob_term.glob_constr * Glob_term.glob_constr option ) list = (snd (List.chop nrel_params funargs)) in List.fold_right - (fun (n,t,is_defined) acc -> - if is_defined - then + (fun (n,t,typ) acc -> + match typ with + | Some typ -> Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, + Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ), acc) - else + | None -> Constrexpr.CProdN (Loc.ghost, [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], @@ -1391,11 +1399,12 @@ let do_build_inductive in let rel_params = List.map - (fun (n,t,is_defined) -> - if is_defined - then - Constrexpr.CLocalDef((Loc.ghost,n), Constrextern.extern_glob_constr Id.Set.empty t) - else + (fun (n,t,typ) -> + match typ with + | Some typ -> + Constrexpr.CLocalDef((Loc.ghost,n), Constrextern.extern_glob_constr Id.Set.empty t, + Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ)) + | None -> Constrexpr.CLocalAssum ([(Loc.ghost,n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t) ) diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli index 5bb1376e2..0cab5a6d3 100644 --- a/plugins/funind/glob_term_to_relation.mli +++ b/plugins/funind/glob_term_to_relation.mli @@ -12,7 +12,7 @@ val build_inductive : *) Evd.evar_map -> Term.pconstant list -> - (Name.t*Glob_term.glob_constr*bool) list list -> (* The list of function args *) + (Name.t*Glob_term.glob_constr*Glob_term.glob_constr option) list list -> (* The list of function args *) Constrexpr.constr_expr list -> (* The list of function returned type *) Glob_term.glob_constr list -> (* the list of body *) unit diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 4e561fc7e..99f50437b 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -15,7 +15,7 @@ let mkGVar id = GVar(Loc.ghost,id) let mkGApp(rt,rtl) = GApp(Loc.ghost,rt,rtl) let mkGLambda(n,t,b) = GLambda(Loc.ghost,n,Explicit,t,b) let mkGProd(n,t,b) = GProd(Loc.ghost,n,Explicit,t,b) -let mkGLetIn(n,t,b) = GLetIn(Loc.ghost,n,t,b) +let mkGLetIn(n,b,t,c) = GLetIn(Loc.ghost,n,b,t,c) let mkGCases(rto,l,brl) = GCases(Loc.ghost,Term.RegularStyle,rto,l,brl) let mkGSort s = GSort(Loc.ghost,s) let mkGHole () = GHole(Loc.ghost,Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None) @@ -37,8 +37,8 @@ let glob_decompose_prod_or_letin = let rec glob_decompose_prod args = function | GProd(_,n,k,t,b) -> glob_decompose_prod ((n,None,Some t)::args) b - | GLetIn(_,n,t,b) -> - glob_decompose_prod ((n,Some t,None)::args) b + | GLetIn(_,n,b,t,c) -> + glob_decompose_prod ((n,Some b,t)::args) c | rt -> args,rt in glob_decompose_prod [] @@ -51,7 +51,7 @@ let glob_compose_prod_or_letin = fun concl decl -> match decl with | (n,None,Some t) -> mkGProd(n,t,concl) - | (n,Some bdy,None) -> mkGLetIn(n,bdy,concl) + | (n,Some bdy,t) -> mkGLetIn(n,bdy,t,concl) | _ -> assert false) let glob_decompose_prod_n n = @@ -73,8 +73,8 @@ let glob_decompose_prod_or_letin_n n = match c with | GProd(_,n,_,t,b) -> glob_decompose_prod (i-1) ((n,None,Some t)::args) b - | GLetIn(_,n,t,b) -> - glob_decompose_prod (i-1) ((n,Some t,None)::args) b + | GLetIn(_,n,b,t,c) -> + glob_decompose_prod (i-1) ((n,Some b,t)::args) c | rt -> args,rt in glob_decompose_prod n [] @@ -150,10 +150,11 @@ let change_vars = change_vars mapping t, change_vars (remove_name_from_mapping mapping name) b ) - | GLetIn(loc,name,def,b) -> + | GLetIn(loc,name,def,typ,b) -> GLetIn(loc, name, change_vars mapping def, + Option.map (change_vars mapping) typ, change_vars (remove_name_from_mapping mapping name) b ) | GLetTuple(loc,nal,(na,rto),b,e) -> @@ -272,10 +273,11 @@ let rec alpha_rt excluded rt = let new_t = alpha_rt excluded t in let new_b = alpha_rt excluded b in GProd(loc,Anonymous,k,new_t,new_b) - | GLetIn(loc,Anonymous,t,b) -> - let new_t = alpha_rt excluded t in + | GLetIn(loc,Anonymous,b,t,c) -> let new_b = alpha_rt excluded b in - GLetIn(loc,Anonymous,new_t,new_b) + let new_t = Option.map (alpha_rt excluded) t in + let new_c = alpha_rt excluded c in + GLetIn(loc,Anonymous,new_b,new_t,new_c) | GLambda(loc,Name id,k,t,b) -> let new_id = Namegen.next_ident_away id excluded in let t,b = @@ -302,19 +304,17 @@ let rec alpha_rt excluded rt = let new_t = alpha_rt new_excluded t in let new_b = alpha_rt new_excluded b in GProd(loc,Name new_id,k,new_t,new_b) - | GLetIn(loc,Name id,t,b) -> + | GLetIn(loc,Name id,b,t,c) -> let new_id = Namegen.next_ident_away id excluded in - let t,b = - if Id.equal new_id id - then t,b - else - let replace = change_vars (Id.Map.add id new_id Id.Map.empty) in - (t,replace b) + let c = + if Id.equal new_id id then c + else change_vars (Id.Map.add id new_id Id.Map.empty) c in let new_excluded = new_id::excluded in - let new_t = alpha_rt new_excluded t in let new_b = alpha_rt new_excluded b in - GLetIn(loc,Name new_id,new_t,new_b) + let new_t = Option.map (alpha_rt new_excluded) t in + let new_c = alpha_rt new_excluded c in + GLetIn(loc,Name new_id,new_b,new_t,new_c) | GLetTuple(loc,nal,(na,rto),t,b) -> @@ -388,13 +388,20 @@ let is_free_in id = | GEvar _ -> false | GPatVar _ -> false | GApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl) - | GLambda(_,n,_,t,b) | GProd(_,n,_,t,b) | GLetIn(_,n,t,b) -> + | GLambda(_,n,_,t,b) | GProd(_,n,_,t,b) -> let check_in_b = match n with | Name id' -> not (Id.equal id' id) | _ -> true in is_free_in t || (check_in_b && is_free_in b) + | GLetIn(_,n,b,t,c) -> + let check_in_c = + match n with + | Name id' -> not (Id.equal id' id) + | _ -> true + in + is_free_in b || Option.cata is_free_in true t || (check_in_c && is_free_in c) | GCases(_,_,_,el,brl) -> (List.exists (fun (e,_) -> is_free_in e) el) || List.exists is_free_in_br brl @@ -473,11 +480,12 @@ let replace_var_by_term x_id term = replace_var_by_pattern t, replace_var_by_pattern b ) - | GLetIn(_,Name id,_,_) when Id.compare id x_id == 0 -> rt - | GLetIn(loc,name,def,b) -> + | GLetIn(_,Name id,_,_,_) when Id.compare id x_id == 0 -> rt + | GLetIn(loc,name,def,typ,b) -> GLetIn(loc, name, replace_var_by_pattern def, + Option.map (replace_var_by_pattern) typ, replace_var_by_pattern b ) | GLetTuple(_,nal,_,_,_) @@ -589,7 +597,7 @@ let ids_of_glob_constr c = 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 + | GLetIn (loc,na,b,t,c) -> idof na :: ids_of_glob_constr [] b @ Option.cata (ids_of_glob_constr []) [] t @ ids_of_glob_constr [] c @ acc | GCast (loc,c,(CastConv t|CastVM t|CastNative 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 @@ -633,9 +641,9 @@ let zeta_normalize = zeta_normalize_term t, zeta_normalize_term b ) - | GLetIn(_,Name id,def,b) -> + | GLetIn(_,Name id,def,typ,b) -> zeta_normalize_term (replace_var_by_term id def b) - | GLetIn(loc,Anonymous,def,b) -> zeta_normalize_term b + | GLetIn(loc,Anonymous,def,typ,b) -> zeta_normalize_term b | GLetTuple(loc,nal,(na,rto),def,b) -> GLetTuple(loc, nal, @@ -690,7 +698,7 @@ let expand_as = | GApp(loc,f,args) -> GApp(loc,expand_as map f,List.map (expand_as map) args) | GLambda(loc,na,k,t,b) -> GLambda(loc,na,k,expand_as map t, expand_as map b) | GProd(loc,na,k,t,b) -> GProd(loc,na,k,expand_as map t, expand_as map b) - | GLetIn(loc,na,v,b) -> GLetIn(loc,na, expand_as map v,expand_as map b) + | GLetIn(loc,na,v,typ,b) -> GLetIn(loc,na, expand_as map v,Option.map (expand_as map) typ,expand_as map b) | GLetTuple(loc,nal,(na,po),v,b) -> GLetTuple(loc,nal,(na,Option.map (expand_as map) po), expand_as map v, expand_as map b) diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 179e8fe8d..84359a36b 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -19,7 +19,7 @@ val mkGVar : Id.t -> glob_constr val mkGApp : glob_constr*(glob_constr list) -> glob_constr val mkGLambda : Name.t * glob_constr * glob_constr -> glob_constr val mkGProd : Name.t * glob_constr * glob_constr -> glob_constr -val mkGLetIn : Name.t * glob_constr * glob_constr -> glob_constr +val mkGLetIn : Name.t * glob_constr * glob_constr option * glob_constr -> glob_constr val mkGCases : glob_constr option * tomatch_tuples * cases_clauses -> glob_constr val mkGSort : glob_sort -> glob_constr val mkGHole : unit -> glob_constr (* we only build Evd.BinderType Anonymous holes *) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d99c3fa04..d394fe313 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -129,7 +129,7 @@ let functional_induction with_clean c princl pat = let rec abstract_glob_constr c = function | [] -> c - | Constrexpr.CLocalDef (x,b)::bl -> Constrexpr_ops.mkLetInC(x,b,abstract_glob_constr c bl) + | Constrexpr.CLocalDef (x,b,t)::bl -> Constrexpr_ops.mkLetInC(x,b,t,abstract_glob_constr c bl) | Constrexpr.CLocalAssum (idl,k,t)::bl -> List.fold_right (fun x b -> Constrexpr_ops.mkLambdaC([x],k,t,b)) idl (abstract_glob_constr c bl) @@ -192,8 +192,10 @@ let is_rec names = | GRec _ -> error "GRec not handled" | GIf(_,b,_,lhs,rhs) -> (lookup names b) || (lookup names lhs) || (lookup names rhs) - | GLetIn(_,na,t,b) | GLambda(_,na,_,t,b) | GProd(_,na,_,t,b) -> + | GProd(_,na,_,t,b) | GLambda(_,na,_,t,b) -> lookup names t || lookup (Nameops.name_fold Id.Set.remove na names) b + | GLetIn(_,na,b,t,c) -> + lookup names b || Option.cata (lookup names) true t || lookup (Nameops.name_fold Id.Set.remove na names) c | GLetTuple(_,nal,_,t,b) -> lookup names t || lookup (List.fold_left @@ -572,8 +574,8 @@ let rec rebuild_bl (aux,assoc) bl typ = | [], _ -> (List.rev aux,replace_vars_constr_expr assoc typ,assoc) | (Constrexpr.CLocalAssum(nal,bk,_))::bl',typ -> rebuild_nal (aux,assoc) bk bl' nal (List.length nal) typ - | (Constrexpr.CLocalDef(na,_))::bl',Constrexpr.CLetIn(_,_,nat,typ') -> - rebuild_bl ((Constrexpr.CLocalDef(na,replace_vars_constr_expr assoc nat)::aux),assoc) + | (Constrexpr.CLocalDef(na,_,_))::bl',Constrexpr.CLetIn(_,_,nat,ty,typ') -> + rebuild_bl ((Constrexpr.CLocalDef(na,replace_vars_constr_expr assoc nat,Option.map (replace_vars_constr_expr assoc) ty (* ??? *))::aux),assoc) bl' typ' | _ -> assert false and rebuild_nal (aux,assoc) bk bl' nal lnal typ = @@ -726,8 +728,8 @@ let rec add_args id new_args b = CLambdaN(loc, List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, add_args id new_args b1) - | CLetIn(loc,na,b1,b2) -> - CLetIn(loc,na,add_args id new_args b1,add_args id new_args b2) + | CLetIn(loc,na,b1,t,b2) -> + CLetIn(loc,na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2) | CAppExpl(loc,(pf,r,us),exprl) -> begin match r with @@ -865,7 +867,7 @@ let make_graph (f_ref:global_reference) = List.flatten (List.map (function - | Constrexpr.CLocalDef (na,_)-> [] + | Constrexpr.CLocalDef (na,_,_)-> [] | Constrexpr.CLocalAssum (nal,_,_) -> List.map (fun (loc,n) -> diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index a45effb16..aed0fa331 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -70,8 +70,8 @@ let chop_rlambda_n = then List.rev acc,rt else match rt with - | Glob_term.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b - | Glob_term.GLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b + | 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 | _ -> raise (CErrors.UserError(Some "chop_rlambda_n", str "chop_rlambda_n: Not enough Lambdas")) diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index e5c756f56..2aabfa003 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -34,7 +34,7 @@ val list_add_set_eq : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list val chop_rlambda_n : int -> Glob_term.glob_constr -> - (Name.t*Glob_term.glob_constr*bool) list * Glob_term.glob_constr + (Name.t*Glob_term.glob_constr*Glob_term.glob_constr option) list * Glob_term.glob_constr val chop_rprod_n : int -> Glob_term.glob_constr -> (Name.t*Glob_term.glob_constr) list * Glob_term.glob_constr diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 7d7c3ad35..9c23be68a 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -510,14 +510,14 @@ let rec merge_app c1 c2 id1 id2 shift filter_shift_stable = 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,trm) , _ -> + | 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,newtrm) - | _, GLetIn(_,nme,bdy,trm) -> + GLetIn(Loc.ghost,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,newtrm) + GLetIn(Loc.ghost,nme,bdy,typ,newtrm) | _ -> let _ = prstr "\nICI4!\n" in raise NoMerge @@ -528,14 +528,14 @@ let rec merge_app_unsafe c1 c2 shift filter_shift_stable = let args = filter_shift_stable lnk (arr1 @ arr2) in GApp (Loc.ghost,GVar(Loc.ghost,shift.ident) , args) (* FIXME: what if the function appears in the body of the let? *) - | GLetIn(_,nme,bdy,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,newtrm) - | _, GLetIn(_,nme,bdy,trm) -> + GLetIn(Loc.ghost,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,newtrm) + GLetIn(Loc.ghost,nme,bdy,typ,newtrm) | _ -> let _ = prstr "\nICI4 '!\n" in raise NoMerge |