diff options
Diffstat (limited to 'plugins/funind/glob_term_to_relation.ml')
-rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 399 |
1 files changed, 194 insertions, 205 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index b9e0e62a..a2577e2b 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -2,26 +2,30 @@ open Printer open Pp open Names open Term +open Vars open Glob_term -open Libnames +open Glob_ops +open Globnames open Indfun_common +open Errors open Util open Glob_termops +open Misctypes let observe strm = if do_observe () - then Pp.msgnl strm + then Pp.msg_debug strm else () -let observennl strm = +(*let observennl strm = if do_observe () then Pp.msg strm - else () + else ()*) type binder_type = - | Lambda of name - | Prod of name - | LetIn of name + | Lambda of Name.t + | Prod of Name.t + | LetIn of Name.t type glob_context = (binder_type*glob_constr) list @@ -54,7 +58,7 @@ type 'a build_entry_pre_return = type 'a build_entry_return = { result : 'a build_entry_pre_return list; - to_avoid : identifier list + to_avoid : Id.t list } (* @@ -86,7 +90,7 @@ let combine_results in (* and then we flatten the map *) { result = List.concat pre_result; - to_avoid = list_union res1.to_avoid res2.to_avoid + to_avoid = List.union Id.equal res1.to_avoid res2.to_avoid } @@ -111,9 +115,9 @@ let ids_of_binder = function let rec change_vars_in_binder mapping = function [] -> [] | (bt,t)::l -> - let new_mapping = List.fold_right Idmap.remove (ids_of_binder bt) mapping in + let new_mapping = List.fold_right Id.Map.remove (ids_of_binder bt) mapping in (bt,change_vars mapping t):: - (if idmap_is_empty new_mapping + (if Id.Map.is_empty new_mapping then l else change_vars_in_binder new_mapping l ) @@ -122,7 +126,7 @@ let rec replace_var_by_term_in_binder x_id term = function | [] -> [] | (bt,t)::l -> (bt,replace_var_by_term x_id term t):: - if List.mem x_id (ids_of_binder bt) + if Id.List.mem x_id (ids_of_binder bt) then l else replace_var_by_term_in_binder x_id term l @@ -130,28 +134,28 @@ let add_bt_names bt = List.append (ids_of_binder bt) let apply_args ctxt body args = let need_convert_id avoid id = - List.exists (is_free_in id) args || List.mem id avoid + List.exists (is_free_in id) args || Id.List.mem id avoid in let need_convert avoid bt = List.exists (need_convert_id avoid) (ids_of_binder bt) in - let next_name_away (na:name) (mapping: identifier Idmap.t) (avoid: identifier list) = + let next_name_away (na:Name.t) (mapping: Id.t Id.Map.t) (avoid: Id.t list) = match na with - | Name id when List.mem id avoid -> + | Name id when Id.List.mem id avoid -> let new_id = Namegen.next_ident_away id avoid in - Name new_id,Idmap.add id new_id mapping,new_id::avoid + Name new_id,Id.Map.add id new_id mapping,new_id::avoid | _ -> na,mapping,avoid in - let next_bt_away bt (avoid:identifier list) = + let next_bt_away bt (avoid:Id.t list) = match bt with | LetIn na -> - let new_na,mapping,new_avoid = next_name_away na Idmap.empty avoid in + let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid in LetIn new_na,mapping,new_avoid | Prod na -> - let new_na,mapping,new_avoid = next_name_away na Idmap.empty avoid in + let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid in Prod new_na,mapping,new_avoid | Lambda na -> - let new_na,mapping,new_avoid = next_name_away na Idmap.empty avoid in + let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid in Lambda new_na,mapping,new_avoid in let rec do_apply avoid ctxt body args = @@ -170,7 +174,7 @@ let apply_args ctxt body args = let new_avoid = id::avoid in let new_id = Namegen.next_ident_away id new_avoid in let new_avoid' = new_id :: new_avoid in - let mapping = Idmap.add id new_id Idmap.empty in + let mapping = Id.Map.add id new_id Id.Map.empty in let new_ctxt' = change_vars_in_binder mapping ctxt' in let new_body = change_vars mapping body in new_avoid',new_ctxt',new_body,new_id @@ -266,11 +270,11 @@ let make_discr_match_el = end *) let make_discr_match_brl i = - list_map_i + List.map_i (fun j (_,idl,patl,_) -> - if j=i - then (dummy_loc,idl,patl, mkGRef (Lazy.force coq_True_ref)) - else (dummy_loc,idl,patl, mkGRef (Lazy.force coq_False_ref)) + if Int.equal j i + then (Loc.ghost,idl,patl, mkGRef (Lazy.force coq_True_ref)) + else (Loc.ghost,idl,patl, mkGRef (Lazy.force coq_False_ref)) ) 0 (* @@ -285,10 +289,6 @@ let make_discr_match brl = make_discr_match_el el, make_discr_match_brl i brl) -let pr_name = function - | Name id -> Ppconstr.pr_id id - | Anonymous -> str "_" - (**********************************************************************) (* functions used to build case expression from lettuple and if ones *) (**********************************************************************) @@ -304,18 +304,17 @@ let build_constructors_of_type ind' argl = Impargs.implicits_of_global constructref in let cst_narg = - Inductiveops.mis_constructor_nargs_env + Inductiveops.constructor_nallargs_env (Global.env ()) construct in - let argl = match argl with - | None -> + let argl = + if List.is_empty argl + then Array.to_list - (Array.init cst_narg (fun _ -> mkGHole ()) + (Array.init (cst_narg - npar) (fun _ -> mkGHole ()) ) - | Some l -> - Array.to_list - (Array.init npar (fun _ -> mkGHole ()))@l + else argl in let pat_as_term = mkGApp(mkGRef (ConstructRef(ind',i+1)),argl) @@ -324,40 +323,6 @@ let build_constructors_of_type ind' argl = ) ind.Declarations.mind_consnames -(* [find_type_of] very naive attempts to discover the type of an if or a letin *) -let rec find_type_of nb b = - let f,_ = glob_decompose_app b in - match f with - | GRef(_,ref) -> - begin - let ind_type = - match ref with - | VarRef _ | ConstRef _ -> - let constr_of_ref = constr_of_global ref in - let type_of_ref = Typing.type_of (Global.env ()) Evd.empty constr_of_ref in - let (_,ret_type) = Reduction.dest_prod (Global.env ()) type_of_ref in - let ret_type,_ = decompose_app ret_type in - if not (isInd ret_type) then - begin -(* Pp.msgnl (str "not an inductive" ++ pr_lconstr ret_type); *) - raise (Invalid_argument "not an inductive") - end; - destInd ret_type - | IndRef ind -> ind - | ConstructRef c -> fst c - in - let _,ind_type_info = Inductive.lookup_mind_specif (Global.env()) ind_type in - if not (Array.length ind_type_info.Declarations.mind_consnames = nb ) - then raise (Invalid_argument "find_type_of : not a valid inductive"); - ind_type - end - | GCast(_,b,_) -> find_type_of nb b - | GApp _ -> assert false (* we have decomposed any application via glob_decompose_app *) - | _ -> raise (Invalid_argument "not a ref") - - - - (******************) (* Main functions *) (******************) @@ -368,14 +333,14 @@ let raw_push_named (na,raw_value,raw_typ) env = match na with | Anonymous -> env | Name id -> - let value = Option.map (Pretyping.Default.understand Evd.empty env) raw_value in - let typ = Pretyping.Default.understand_type Evd.empty env raw_typ in + let value = Option.map (fun x-> fst (Pretyping.understand env Evd.empty x)) raw_value in + let typ,ctx = Pretyping.understand env Evd.empty ~expected_type:Pretyping.IsType raw_typ in Environ.push_named (id,value,typ) env let add_pat_variables pat typ env : Environ.env = let rec add_pat_variables env pat typ : Environ.env = - observe (str "new rel env := " ++ Printer.pr_rel_context_of env); + observe (str "new rel env := " ++ Printer.pr_rel_context_of env Evd.empty); match pat with | PatVar(_,na) -> Environ.push_rel (na,None,typ) env @@ -385,14 +350,14 @@ let add_pat_variables pat typ env : Environ.env = with Not_found -> assert false in let constructors = Inductiveops.get_constructors env indf in - let constructor : Inductiveops.constructor_summary = List.find (fun cs -> cs.Inductiveops.cs_cstr = c) (Array.to_list constructors) in + let constructor : Inductiveops.constructor_summary = List.find (fun cs -> eq_constructor c (fst cs.Inductiveops.cs_cstr)) (Array.to_list constructors) in let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in List.fold_left2 add_pat_variables env patl (List.rev cs_args_types) in let new_env = add_pat_variables env pat typ in let res = fst ( - Sign.fold_rel_context + Context.fold_rel_context (fun (na,v,t) (env,ctxt) -> match na with | Anonymous -> assert false @@ -411,7 +376,7 @@ let add_pat_variables pat typ env : Environ.env = ~init:(env,[]) ) in - observe (str "new var env := " ++ Printer.pr_named_context_of res); + observe (str "new var env := " ++ Printer.pr_named_context_of res Evd.empty); res @@ -423,7 +388,7 @@ let rec pattern_to_term_and_type env typ = function mkGVar id | PatCstr(loc,constr,patternl,_) -> let cst_narg = - Inductiveops.mis_constructor_nargs_env + Inductiveops.constructor_nallargs_env (Global.env ()) constr in @@ -432,7 +397,7 @@ let rec pattern_to_term_and_type env typ = function with Not_found -> assert false in let constructors = Inductiveops.get_constructors env indf in - let constructor = List.find (fun cs -> cs.Inductiveops.cs_cstr = constr) (Array.to_list constructors) in + let constructor = List.find (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr) (Array.to_list constructors) in let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in let _,cstl = Inductiveops.dest_ind_family indf in let csta = Array.of_list cstl in @@ -440,7 +405,7 @@ let rec pattern_to_term_and_type env typ = function Array.to_list (Array.init (cst_narg - List.length patternl) - (fun i -> Detyping.detype false [] (Termops.names_of_rel_context env) csta.(i)) + (fun i -> Detyping.detype false [] env Evd.empty csta.(i)) ) in let patl_as_term = @@ -508,12 +473,12 @@ 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(dummy_loc,na,u,aux b l) + GLetIn(Loc.ghost,na,u,aux b l) | _ -> - GApp(dummy_loc,t,l) + GApp(Loc.ghost,t,l) in build_entry_lc env funnames avoid (aux f args) - | GVar(_,id) when Idset.mem id funnames -> + | GVar(_,id) when Id.Set.mem id funnames -> (* if we have [f t1 ... tn] with [f]$\in$[fnames] then we create a fresh variable [res], add [res] and its "value" (i.e. [res v1 ... vn]) to each @@ -521,10 +486,10 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = a pseudo value "v1 ... vn". The "value" of this branch is then simply [res] *) - let rt_as_constr = Pretyping.Default.understand Evd.empty env rt in + let rt_as_constr,ctx = Pretyping.understand env Evd.empty rt in let rt_typ = Typing.type_of env Evd.empty rt_as_constr in - let res_raw_type = Detyping.detype false [] (Termops.names_of_rel_context env) rt_typ in - let res = fresh_id args_res.to_avoid "res" in + let res_raw_type = Detyping.detype false [] env Evd.empty rt_typ in + let res = fresh_id args_res.to_avoid "_res" in let new_avoid = res::args_res.to_avoid in let res_rt = mkGVar res in let new_result = @@ -568,7 +533,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let new_b = replace_var_by_term id - (GVar(dummy_loc,id)) + (GVar(Loc.ghost,id)) b in (Name new_id,new_b,new_avoid) @@ -629,7 +594,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = and combine the two result *) let v_res = build_entry_lc env funnames avoid v in - let v_as_constr = Pretyping.Default.understand Evd.empty env v in + let v_as_constr,ctx = Pretyping.understand env Evd.empty v in let v_type = Typing.type_of env Evd.empty v_as_constr in let new_env = match n with @@ -645,7 +610,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = 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) -> - let b_as_constr = Pretyping.Default.understand Evd.empty env b in + let b_as_constr,ctx = Pretyping.understand env Evd.empty b in let b_typ = Typing.type_of env Evd.empty b_as_constr in let (ind,_) = try Inductiveops.find_inductive env Evd.empty b_typ @@ -654,11 +619,11 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = Printer.pr_glob_constr b ++ str " in " ++ Printer.pr_glob_constr rt ++ str ". try again with a cast") in - let case_pats = build_constructors_of_type ind None in - assert (Array.length case_pats = 2); + let case_pats = build_constructors_of_type (fst ind) [] in + assert (Int.equal (Array.length case_pats) 2); let brl = - list_map_i - (fun i x -> (dummy_loc,[],[case_pats.(i)],x)) + List.map_i + (fun i x -> (Loc.ghost,[],[case_pats.(i)],x)) 0 [lhs;rhs] in @@ -670,14 +635,14 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = | GLetTuple(_,nal,_,b,e) -> begin let nal_as_glob_constr = - Some (List.map + List.map (function Name id -> mkGVar id | Anonymous -> mkGHole () ) - nal) + nal in - let b_as_constr = Pretyping.Default.understand Evd.empty env b in + let b_as_constr,ctx = Pretyping.understand env Evd.empty b in let b_typ = Typing.type_of env Evd.empty b_as_constr in let (ind,_) = try Inductiveops.find_inductive env Evd.empty b_typ @@ -686,10 +651,10 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = Printer.pr_glob_constr b ++ str " in " ++ Printer.pr_glob_constr rt ++ str ". try again with a cast") in - let case_pats = build_constructors_of_type ind nal_as_glob_constr in - assert (Array.length case_pats = 1); + let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in + assert (Int.equal (Array.length case_pats) 1); let br = - (dummy_loc,[],[case_pats.(0)],e) + (Loc.ghost,[],[case_pats.(0)],e) in let match_expr = mkGCases(None,[b,(Anonymous,None)],[br]) in build_entry_lc env funnames avoid match_expr @@ -724,7 +689,7 @@ and build_entry_lc_from_case env funname make_discr in let types = List.map (fun (case_arg,_) -> - let case_arg_as_constr = Pretyping.Default.understand Evd.empty env case_arg in + let case_arg_as_constr,ctx = Pretyping.understand env Evd.empty case_arg in Typing.type_of env Evd.empty case_arg_as_constr ) el in @@ -746,7 +711,8 @@ and build_entry_lc_from_case env funname make_discr { result = List.concat (List.map (fun r -> r.result) results); to_avoid = - List.fold_left (fun acc r -> list_union acc r.to_avoid) [] results + List.fold_left (fun acc r -> List.union Id.equal acc r.to_avoid) + [] results } and build_entry_lc_from_case_term env types funname make_discr patterns_to_prevent brl avoid @@ -761,7 +727,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve (will be used in the following recursive calls) *) let new_env = List.fold_right2 add_pat_variables patl types env in - let not_those_patterns : (identifier list -> glob_constr -> glob_constr) list = + let not_those_patterns : (Id.t list -> glob_constr -> glob_constr) list = List.map2 (fun pat typ -> fun avoid pat'_as_term -> @@ -775,7 +741,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve in let raw_typ_of_id = Detyping.detype false [] - (Termops.names_of_rel_context env_with_pat_ids) typ_of_id + env_with_pat_ids Evd.empty typ_of_id in mkGProd (Name id,raw_typ_of_id,acc)) pat_ids @@ -816,18 +782,18 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve let those_pattern_preconds = (List.flatten ( - list_map3 + List.map3 (fun pat e typ_as_constr -> let this_pat_ids = ids_of_pat pat in - let typ = Detyping.detype false [] (Termops.names_of_rel_context new_env) typ_as_constr in + let typ = Detyping.detype false [] new_env Evd.empty typ_as_constr in let pat_as_term = pattern_to_term pat in List.fold_right (fun id acc -> - if Idset.mem id this_pat_ids + if Id.Set.mem id this_pat_ids then (Prod (Name id), let typ_of_id = Typing.type_of new_env Evd.empty (mkVar id) in let raw_typ_of_id = - Detyping.detype false [] (Termops.names_of_rel_context new_env) typ_of_id + Detyping.detype false [] new_env Evd.empty typ_of_id in raw_typ_of_id )::acc @@ -871,14 +837,14 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve let is_res id = try - String.sub (string_of_id id) 0 3 = "res" + String.equal (String.sub (Id.to_string id) 0 4) "_res" with Invalid_argument _ -> false let same_raw_term rt1 rt2 = match rt1,rt2 with - | GRef(_,r1), GRef (_,r2) -> r1=r2 + | GRef(_,r1,_), GRef (_,r2,_) -> Globnames.eq_gr r1 r2 | GHole _, GHole _ -> true | _ -> false let decompose_raw_eq lhs rhs = @@ -892,7 +858,7 @@ let decompose_raw_eq lhs rhs = observe (str "lrhs := " ++ int (List.length lrhs)); let sllhs = List.length llhs in let slrhs = List.length lrhs in - if same_raw_term lhd rhd && sllhs = slrhs + if same_raw_term lhd rhd && Int.equal sllhs slrhs then (* let _ = assert false in *) List.fold_right2 decompose_raw_eq llhs lrhs acc @@ -928,7 +894,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let new_t = mkGApp(mkGVar(mk_rel_id this_relname),args'@[res_rt]) in - let t' = Pretyping.Default.understand Evd.empty env new_t in + let t',ctx = Pretyping.understand env Evd.empty new_t in let new_env = Environ.push_rel (n,None,t') env in let new_b,id_to_exclude = rebuild_cons new_env @@ -937,18 +903,18 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (depth + 1) b in mkGProd(n,new_t,new_b), - Idset.filter not_free_in_t id_to_exclude + Id.Set.filter not_free_in_t id_to_exclude | _ -> (* the first args is the name of the function! *) assert false end - | GApp(loc1,GRef(loc2,eq_as_ref),[ty;GVar(loc3,id);rt]) - when eq_as_ref = Lazy.force Coqlib.coq_eq_ref && n = Anonymous + | GApp(loc1,GRef(loc2,eq_as_ref,_),[ty;GVar(loc3,id);rt]) + when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous -> begin try observe (str "computing new type for eq : " ++ pr_glob_constr rt); let t' = - try Pretyping.Default.understand Evd.empty env t + try fst (Pretyping.understand env Evd.empty t)(*FIXME*) with e when Errors.noncritical e -> raise Continue in let is_in_b = is_free_in id b in @@ -970,36 +936,36 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = in mkGProd(n,t,new_b),id_to_exclude with Continue -> - let jmeq = Libnames.IndRef (destInd (jmeq ())) in - let ty' = Pretyping.Default.understand Evd.empty env ty in + let jmeq = Globnames.IndRef (fst (destInd (jmeq ()))) in + let ty',ctx = Pretyping.understand env Evd.empty ty in let ind,args' = Inductive.find_inductive env ty' in - let mib,_ = Global.lookup_inductive ind in + let mib,_ = Global.lookup_inductive (fst ind) in let nparam = mib.Declarations.mind_nparams in let params,arg' = - ((Util.list_chop nparam args')) + ((Util.List.chop nparam args')) in let rt_typ = - GApp(Util.dummy_loc, - GRef (Util.dummy_loc,Libnames.IndRef ind), + GApp(Loc.ghost, + GRef (Loc.ghost,Globnames.IndRef (fst ind),None), (List.map (fun p -> Detyping.detype false [] - (Termops.names_of_rel_context env) + env Evd.empty p) params)@(Array.to_list (Array.make (List.length args' - nparam) (mkGHole ())))) in let eq' = - GApp(loc1,GRef(loc2,jmeq),[ty;GVar(loc3,id);rt_typ;rt]) + GApp(loc1,GRef(loc2,jmeq,None),[ty;GVar(loc3,id);rt_typ;rt]) in observe (str "computing new type for jmeq : " ++ pr_glob_constr eq'); - let eq'_as_constr = Pretyping.Default.understand Evd.empty env eq' in + let eq'_as_constr,ctx = Pretyping.understand env Evd.empty eq' in observe (str " computing new type for jmeq : done") ; let new_args = match kind_of_term eq'_as_constr with | App(_,[|_;_;ty;_|]) -> let ty = Array.to_list (snd (destApp ty)) in - let ty' = snd (Util.list_chop nparam ty) in + let ty' = snd (Util.List.chop nparam ty) in List.fold_left2 (fun acc var_as_constr arg -> if isRel var_as_constr @@ -1011,11 +977,13 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | Anonymous -> acc | Name id' -> (id',Detyping.detype false [] - (Termops.names_of_rel_context env) + env + Evd.empty arg)::acc else if isVar var_as_constr then (destVar var_as_constr,Detyping.detype false [] - (Termops.names_of_rel_context env) + env + Evd.empty arg)::acc else acc ) @@ -1041,7 +1009,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = if is_in_b then b else replace_var_by_term id rt b in let new_env = - let t' = Pretyping.Default.understand Evd.empty env eq' in + let t',ctx = Pretyping.understand env Evd.empty eq' in Environ.push_rel (n,None,t') env in let new_b,id_to_exclude = @@ -1056,10 +1024,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (* J.F:. keep this comment it explain how to remove some meaningless equalities if keep_eq then mkGProd(n,t,new_b),id_to_exclude - else new_b, Idset.add id id_to_exclude + else new_b, Id.Set.add id id_to_exclude *) - | GApp(loc1,GRef(loc2,eq_as_ref),[ty;rt1;rt2]) - when eq_as_ref = Lazy.force Coqlib.coq_eq_ref && n = Anonymous + | GApp(loc1,GRef(loc2,eq_as_ref,_),[ty;rt1;rt2]) + when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous -> begin try @@ -1079,7 +1047,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = else raise Continue with Continue -> observe (str "computing new type for prod : " ++ pr_glob_constr rt); - let t' = Pretyping.Default.understand Evd.empty env t in + let t',ctx = Pretyping.understand env Evd.empty t in let new_env = Environ.push_rel (n,None,t') env in let new_b,id_to_exclude = rebuild_cons new_env @@ -1088,14 +1056,14 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (depth + 1) b in match n with - | Name id when Idset.mem id id_to_exclude && depth >= nb_args -> - new_b,Idset.remove id - (Idset.filter not_free_in_t id_to_exclude) - | _ -> mkGProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude + | 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) + | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude end | _ -> observe (str "computing new type for prod : " ++ pr_glob_constr rt); - let t' = Pretyping.Default.understand Evd.empty env t in + let t',ctx = Pretyping.understand env Evd.empty t in let new_env = Environ.push_rel (n,None,t') env in let new_b,id_to_exclude = rebuild_cons new_env @@ -1104,17 +1072,17 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (depth + 1) b in match n with - | Name id when Idset.mem id id_to_exclude && depth >= nb_args -> - new_b,Idset.remove id - (Idset.filter not_free_in_t id_to_exclude) - | _ -> mkGProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude + | 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) + | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude end | 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 observe (str "computing new type for lambda : " ++ pr_glob_constr rt); - let t' = Pretyping.Default.understand Evd.empty env t in + let t',ctx = Pretyping.understand env Evd.empty t in match n with | Name id -> let new_env = Environ.push_rel (n,None,t') env in @@ -1124,19 +1092,19 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (args@[mkGVar id])new_crossed_types (depth + 1 ) b in - if Idset.mem id id_to_exclude && depth >= nb_args + if Id.Set.mem id id_to_exclude && depth >= nb_args then - new_b, Idset.remove id (Idset.filter not_free_in_t id_to_exclude) + new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) else - GProd(dummy_loc,n,k,t,new_b),Idset.filter not_free_in_t id_to_exclude - | _ -> anomaly "Should not have an anonymous function here" + GProd(Loc.ghost,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 | GLetIn(_,n,t,b) -> begin let not_free_in_t id = not (is_free_in id t) in - let t' = Pretyping.Default.understand Evd.empty env t in + let t',ctx = Pretyping.understand env Evd.empty t in let type_t' = Typing.type_of env Evd.empty t' in let new_env = Environ.push_rel (n,Some t',type_t') env in let new_b,id_to_exclude = @@ -1145,13 +1113,13 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = args (t::crossed_types) (depth + 1 ) b in match n with - | Name id when Idset.mem id id_to_exclude && depth >= nb_args -> - new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude) - | _ -> GLetIn(dummy_loc,n,t,new_b), - Idset.filter not_free_in_t id_to_exclude + | 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), + Id.Set.filter not_free_in_t id_to_exclude end | GLetTuple(_,nal,(na,rto),t,b) -> - assert (rto=None); + assert (Option.is_empty rto); begin let not_free_in_t id = not (is_free_in id t) in let new_t,id_to_exclude' = @@ -1161,7 +1129,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = args (crossed_types) depth t in - let t' = Pretyping.Default.understand Evd.empty env new_t in + let t',ctx = Pretyping.understand env Evd.empty new_t in let new_env = Environ.push_rel (na,None,t') env in let new_b,id_to_exclude = rebuild_cons new_env @@ -1170,15 +1138,15 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (depth + 1) b in (* match n with *) -(* | Name id when Idset.mem id id_to_exclude -> *) -(* new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude) *) +(* | 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) *) (* | _ -> *) - GLetTuple(dummy_loc,nal,(na,None),t,new_b), - Idset.filter not_free_in_t (Idset.union id_to_exclude id_to_exclude') + GLetTuple(Loc.ghost,nal,(na,None),t,new_b), + Id.Set.filter not_free_in_t (Id.Set.union id_to_exclude id_to_exclude') end - | _ -> mkGApp(mkGVar relname,args@[rt]),Idset.empty + | _ -> mkGApp(mkGVar relname,args@[rt]),Id.Set.empty (* debuging wrapper *) @@ -1201,7 +1169,7 @@ let rebuild_cons env nb_args relname args crossed_types rt = *) let rec compute_cst_params relnames params = function | GRef _ | GVar _ | GEvar _ | GPatVar _ -> params - | GApp(_,GVar(_,relname'),rtl) when Idset.mem relname' relnames -> + | GApp(_,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) @@ -1219,11 +1187,11 @@ 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_ord id id' == 0 && not is_defined -> + when Id.compare id id' == 0 && not is_defined -> compute_cst_params_from_app (param::acc) (params',rtl') | _ -> List.rev acc -let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * bool) list array) csts = +let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool) list array) csts = let rels_params = Array.mapi (fun i args -> @@ -1237,12 +1205,12 @@ let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * b let l = ref [] in let _ = try - list_iter_i + List.iteri (fun i ((n,nt,is_defined) as param) -> - if array_for_all + if Array.for_all (fun l -> let (n',nt',is_defined') = List.nth l i in - n = n' && Topconstr.eq_glob_constr nt nt' && is_defined = is_defined') + Name.equal n n' && Notation_ops.eq_glob_constr nt nt' && (is_defined : bool) == is_defined') rels_params then l := param::!l @@ -1255,22 +1223,23 @@ let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * b let rec rebuild_return_type rt = match rt with - | Topconstr.CProdN(loc,n,t') -> - Topconstr.CProdN(loc,n,rebuild_return_type t') - | Topconstr.CArrow(loc,t,t') -> - 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,GType None)) + | 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.CProdN(Loc.ghost,[[Loc.ghost,Anonymous], + Constrexpr.Default Decl_kinds.Explicit,rt], + Constrexpr.CSort(Loc.ghost,GType [])) let do_build_inductive - funnames (funsargs: (Names.name * glob_constr * bool) list list) - returned_types - (rtl:glob_constr list) = + mp_dp + funnames (funsargs: (Name.t * glob_constr * bool) list list) + returned_types + (rtl:glob_constr list) = let _time1 = System.get_time () in -(* Pp.msgnl (prlist_with_sep fnl Printer.pr_glob_constr rtl); *) - let funnames_as_set = List.fold_right Idset.add funnames Idset.empty in + (* Pp.msgnl (prlist_with_sep fnl Printer.pr_glob_constr rtl); *) + let funnames_as_set = List.fold_right Id.Set.add funnames Id.Set.empty in let funnames = Array.of_list funnames in let funsargs = Array.of_list funsargs in let returned_types = Array.of_list returned_types in @@ -1281,12 +1250,22 @@ let do_build_inductive Ensures by: obvious i*) let relnames = Array.map mk_rel_id funnames in - let relnames_as_set = Array.fold_right Idset.add relnames Idset.empty in + let relnames_as_set = Array.fold_right Id.Set.add relnames Id.Set.empty in (* Construction of the pseudo constructors *) let env = Array.fold_right (fun id env -> - Environ.push_named (id,None,Typing.type_of env Evd.empty (Constrintern.global_reference id)) env + let c = + match mp_dp with + | None -> (Constrintern.global_reference id) + | Some(mp,dp) -> mkConst (make_con mp dp (Label.of_id id)) + in + Environ.push_named (id,None, + try + Typing.type_of env Evd.empty c + with Not_found -> + raise (UserError("do_build_inductive", str "Cannot handle partial fixpoint")) + ) env ) funnames (Global.env ()) @@ -1294,19 +1273,19 @@ 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 = (* Reduilding arities (with parameters) *) - let rel_first_args :(Names.name * Glob_term.glob_constr * bool ) list = + let rel_first_args :(Name.t * Glob_term.glob_constr * bool ) list = funargs in List.fold_right (fun (n,t,is_defined) acc -> if is_defined then - Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_glob_constr Idset.empty t, + Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, acc) else - Topconstr.CProdN - (dummy_loc, - [[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t], + Constrexpr.CProdN + (Loc.ghost, + [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], acc ) ) @@ -1318,8 +1297,9 @@ let do_build_inductive Then save the graphs and reset Printing options to their primitive values *) let rel_arities = Array.mapi rel_arity funsargs in - Util.array_fold_left2 (fun env rel_name rel_ar -> - Environ.push_named (rel_name,None, Constrintern.interp_constr Evd.empty env rel_ar) env) env relnames rel_arities + Util.Array.fold_left2 (fun env rel_name rel_ar -> + Environ.push_named (rel_name,None, + fst (with_full_print (Constrintern.interp_constr env Evd.empty) rel_ar)) env) env relnames rel_arities in (* and of the real constructors*) let constr i res = @@ -1344,9 +1324,9 @@ let do_build_inductive (*i The next call to mk_rel_id is valid since we are constructing the graph Ensures by: obvious i*) - id_of_string ((string_of_id (mk_rel_id funnames.(i)))^"_"^(string_of_int !next_constructor_id)) + Id.of_string ((Id.to_string (mk_rel_id funnames.(i)))^"_"^(string_of_int !next_constructor_id)) in - let rel_constructors i rt : (identifier*glob_constr) list = + let rel_constructors i rt : (Id.t*glob_constr) list = next_constructor_id := (-1); List.map (fun constr -> (mk_constructor_id i),constr) (constr i rt) in @@ -1360,19 +1340,19 @@ let do_build_inductive rel_constructors in let rel_arity i funargs = (* Reduilding arities (with parameters) *) - let rel_first_args :(Names.name * Glob_term.glob_constr * bool ) list = - (snd (list_chop nrel_params funargs)) + let rel_first_args :(Name.t * Glob_term.glob_constr * bool ) list = + (snd (List.chop nrel_params funargs)) in List.fold_right (fun (n,t,is_defined) acc -> if is_defined then - Topconstr.CLetIn(dummy_loc,(dummy_loc, n),Constrextern.extern_glob_constr Idset.empty t, + Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, acc) else - Topconstr.CProdN - (dummy_loc, - [[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t], + Constrexpr.CProdN + (Loc.ghost, + [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], acc ) ) @@ -1384,31 +1364,40 @@ let do_build_inductive Then save the graphs and reset Printing options to their primitive values *) let rel_arities = Array.mapi rel_arity funsargs in + let rel_params_ids = + List.fold_left + (fun acc (na,_,_) -> + match na with + Anonymous -> acc + | Name id -> id::acc + ) + [] + rels_params + in let rel_params = List.map (fun (n,t,is_defined) -> if is_defined then - Topconstr.LocalRawDef((dummy_loc,n), Constrextern.extern_glob_constr Idset.empty t) + Constrexpr.LocalRawDef((Loc.ghost,n), Constrextern.extern_glob_constr Id.Set.empty t) else - Topconstr.LocalRawAssum - ([(dummy_loc,n)], Topconstr.default_binder_kind, Constrextern.extern_glob_constr Idset.empty t) + Constrexpr.LocalRawAssum + ([(Loc.ghost,n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t) ) rels_params in let ext_rels_constructors = Array.map (List.map (fun (id,t) -> - false,((dummy_loc,id), - Flags.with_option - Flags.raw_print - (Constrextern.extern_glob_type Idset.empty) ((* zeta_normalize *) t) + false,((Loc.ghost,id), + with_full_print + (Constrextern.extern_glob_type Id.Set.empty) ((* zeta_normalize *) (alpha_rt rel_params_ids t)) ) )) (rel_constructors) in let rel_ind i ext_rel_constructors = - ((dummy_loc,relnames.(i)), + ((Loc.ghost,relnames.(i)), rel_params, Some rel_arities.(i), ext_rel_constructors),[] @@ -1437,7 +1426,7 @@ let do_build_inductive (* in *) let _time2 = System.get_time () in try - with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds)) true + with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds false false)) Decl_kinds.Finite with | UserError(s,msg) as e -> let _time3 = System.get_time () in @@ -1448,7 +1437,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds)) + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds)) ++ fnl () ++ msg in @@ -1463,7 +1452,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds)) + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds)) ++ fnl () ++ Errors.print reraise in @@ -1472,9 +1461,9 @@ let do_build_inductive -let build_inductive funnames funsargs returned_types rtl = +let build_inductive mp_dp funnames funsargs returned_types rtl = try - do_build_inductive funnames funsargs returned_types rtl + do_build_inductive mp_dp funnames funsargs returned_types rtl with e when Errors.noncritical e -> raise (Building_graph e) |