From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- pretyping/detyping.ml | 234 ++++++++++++++++++++++++++++---------------------- 1 file changed, 130 insertions(+), 104 deletions(-) (limited to 'pretyping/detyping.ml') diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 9ba5949a..0dc5a9ba 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -14,6 +14,7 @@ open Pp open CErrors open Util open Names +open Constr open Term open EConstr open Vars @@ -26,7 +27,6 @@ open Libnames open Globnames open Nametab open Mod_subst -open Misctypes open Decl_kinds open Context.Named.Declaration open Ltac_pretype @@ -36,7 +36,7 @@ type _ delay = | Later : [ `thunk ] delay (** Should we keep details of universes during detyping ? *) -let print_universes = Flags.univ_print +let print_universes = ref false (** If true, prints local context of evars, whatever print_arguments *) let print_evar_arguments = ref false @@ -87,7 +87,7 @@ let encode_tuple ({CAst.loc} as r) = module PrintingInductiveMake = functor (Test : sig - val encode : reference -> inductive + val encode : qualid -> inductive val member_message : Pp.t -> bool -> Pp.t val field : string val title : string @@ -501,13 +501,104 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = let eqnl = detype_eqns constructs constagsl bl in GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl) +let rec share_names detype n l avoid env sigma c t = + match EConstr.kind sigma c, EConstr.kind sigma t with + (* factorize even when not necessary to have better presentation *) + | Lambda (na,t,c), Prod (na',t',c') -> + let na = match (na,na') with + Name _, _ -> na + | _, Name _ -> na' + | _ -> na in + let t' = detype avoid env sigma t in + let id = next_name_away na avoid in + let avoid = Id.Set.add id avoid and env = add_name (Name id) None t env in + share_names detype (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c' + (* May occur for fix built interactively *) + | LetIn (na,b,t',c), _ when n > 0 -> + let t'' = detype avoid env sigma t' in + let b' = detype avoid env sigma b in + let id = next_name_away na avoid in + let avoid = Id.Set. add id avoid and env = add_name (Name id) (Some b) t' env in + share_names detype n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t) + (* Only if built with the f/n notation or w/o let-expansion in types *) + | _, LetIn (_,b,_,t) when n > 0 -> + share_names detype n l avoid env sigma c (subst1 b t) + (* If it is an open proof: we cheat and eta-expand *) + | _, Prod (na',t',c') when n > 0 -> + let t'' = detype avoid env sigma t' in + let id = next_name_away na' avoid in + let avoid = Id.Set.add id avoid and env = add_name (Name id) None t' env in + let appc = mkApp (lift 1 c,[|mkRel 1|]) in + share_names detype (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c' + (* If built with the f/n notation: we renounce to share names *) + | _ -> + if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough"); + let c = detype avoid env sigma c in + let t = detype avoid env sigma t in + (List.rev l,c,t) + +let rec share_pattern_names detype n l avoid env sigma c t = + let open Pattern in + if n = 0 then + let c = detype avoid env sigma c in + let t = detype avoid env sigma t in + (List.rev l,c,t) + else match c, t with + | PLambda (na,t,c), PProd (na',t',c') -> + let na = match (na,na') with + Name _, _ -> na + | _, Name _ -> na' + | _ -> na in + let t' = detype avoid env sigma t in + let id = next_name_away na avoid in + let avoid = Id.Set.add id avoid in + let env = Name id :: env in + share_pattern_names detype (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c' + | _ -> + if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough"); + let c = detype avoid env sigma c in + let t = detype avoid env sigma t in + (List.rev l,c,t) + +let detype_fix detype avoid env sigma (vn,_ as nvn) (names,tys,bodies) = + let def_avoid, def_env, lfi = + Array.fold_left2 + (fun (avoid, env, l) na ty -> + let id = next_name_away na avoid in + (Id.Set.add id avoid, add_name (Name id) None ty env, id::l)) + (avoid, env, []) names tys in + let n = Array.length tys in + let v = Array.map3 + (fun c t i -> share_names detype (i+1) [] def_avoid def_env sigma c (lift n t)) + bodies tys vn in + GRec(GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi), + Array.map (fun (bl,_,_) -> bl) v, + Array.map (fun (_,_,ty) -> ty) v, + Array.map (fun (_,bd,_) -> bd) v) + +let detype_cofix detype avoid env sigma n (names,tys,bodies) = + let def_avoid, def_env, lfi = + Array.fold_left2 + (fun (avoid, env, l) na ty -> + let id = next_name_away na avoid in + (Id.Set.add id avoid, add_name (Name id) None ty env, id::l)) + (avoid, env, []) names tys in + let ntys = Array.length tys in + let v = Array.map2 + (fun c t -> share_names detype 0 [] def_avoid def_env sigma c (lift ntys t)) + bodies tys in + GRec(GCoFix n,Array.of_list (List.rev lfi), + Array.map (fun (bl,_,_) -> bl) v, + Array.map (fun (_,_,ty) -> ty) v, + Array.map (fun (_,bd,_) -> bd) v) + let detype_universe sigma u = let fn (l, n) = Some (Termops.reference_of_level sigma l, n) in Univ.Universe.map fn u let detype_sort sigma = function - | Prop Null -> GProp - | Prop Pos -> GSet + | Prop -> GProp + | Set -> GSet | Type u -> GType (if !print_universes @@ -584,13 +675,12 @@ and detype_r d flags avoid env sigma t = (Array.map_to_list (detype d flags avoid env sigma) args) | Const (sp,u) -> GRef (ConstRef sp, detype_instance sigma u) | Proj (p,c) -> - let noparams () = - let pb = Environ.lookup_projection p (snd env) in - let pars = pb.Declarations.proj_npars in - let hole = DAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in - let args = List.make pars hole in - GApp (DAst.make @@ GRef (ConstRef (Projection.constant p), None), - (args @ [detype d flags avoid env sigma c])) + let noparams () = + let pars = Projection.npars p in + let hole = DAst.make @@ GHole(Evar_kinds.InternalHole,Namegen.IntroAnonymous,None) in + let args = List.make pars hole in + GApp (DAst.make @@ GRef (ConstRef (Projection.constant p), None), + (args @ [detype d flags avoid env sigma c])) in if fst flags || !Flags.in_debugger || !Flags.in_toplevel then try noparams () @@ -603,8 +693,9 @@ and detype_r d flags avoid env sigma t = (** Print the compatibility match version *) let c' = try - let pb = Environ.lookup_projection p (snd env) in - let body = pb.Declarations.proj_body in + let ind = Projection.inductive p in + let bodies = Inductiveops.legacy_match_projection (snd env) ind in + let body = bodies.(Projection.arg p) in let ty = Retyping.get_type_of (snd env) sigma c in let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma ty in let body' = strip_lam_assum body in @@ -660,76 +751,8 @@ and detype_r d flags avoid env sigma t = (ci.ci_ind,ci.ci_pp_info.style, ci.ci_pp_info.cstr_tags,ci.ci_pp_info.ind_tags) p c bl - | Fix (nvn,recdef) -> detype_fix d flags avoid env sigma nvn recdef - | CoFix (n,recdef) -> detype_cofix d flags avoid env sigma n recdef - -and detype_fix d flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) = - let def_avoid, def_env, lfi = - Array.fold_left2 - (fun (avoid, env, l) na ty -> - let id = next_name_away na avoid in - (Id.Set.add id avoid, add_name (Name id) None ty env, id::l)) - (avoid, env, []) names tys in - let n = Array.length tys in - let v = Array.map3 - (fun c t i -> share_names d flags (i+1) [] def_avoid def_env sigma c (lift n t)) - bodies tys vn in - GRec(GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi), - Array.map (fun (bl,_,_) -> bl) v, - Array.map (fun (_,_,ty) -> ty) v, - Array.map (fun (_,bd,_) -> bd) v) - -and detype_cofix d flags avoid env sigma n (names,tys,bodies) = - let def_avoid, def_env, lfi = - Array.fold_left2 - (fun (avoid, env, l) na ty -> - let id = next_name_away na avoid in - (Id.Set.add id avoid, add_name (Name id) None ty env, id::l)) - (avoid, env, []) names tys in - let ntys = Array.length tys in - let v = Array.map2 - (fun c t -> share_names d flags 0 [] def_avoid def_env sigma c (lift ntys t)) - bodies tys in - GRec(GCoFix n,Array.of_list (List.rev lfi), - Array.map (fun (bl,_,_) -> bl) v, - Array.map (fun (_,_,ty) -> ty) v, - Array.map (fun (_,bd,_) -> bd) v) - -and share_names d flags n l avoid env sigma c t = - match EConstr.kind sigma c, EConstr.kind sigma t with - (* factorize even when not necessary to have better presentation *) - | Lambda (na,t,c), Prod (na',t',c') -> - let na = match (na,na') with - Name _, _ -> na - | _, Name _ -> na' - | _ -> na in - let t' = detype d flags avoid env sigma t in - let id = next_name_away na avoid in - let avoid = Id.Set.add id avoid and env = add_name (Name id) None t env in - share_names d flags (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c' - (* May occur for fix built interactively *) - | LetIn (na,b,t',c), _ when n > 0 -> - let t'' = detype d flags avoid env sigma t' in - let b' = detype d flags avoid env sigma b in - let id = next_name_away na avoid in - let avoid = Id.Set. add id avoid and env = add_name (Name id) (Some b) t' env in - share_names d flags n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t) - (* Only if built with the f/n notation or w/o let-expansion in types *) - | _, LetIn (_,b,_,t) when n > 0 -> - share_names d flags n l avoid env sigma c (subst1 b t) - (* If it is an open proof: we cheat and eta-expand *) - | _, Prod (na',t',c') when n > 0 -> - let t'' = detype d flags avoid env sigma t' in - let id = next_name_away na' avoid in - let avoid = Id.Set.add id avoid and env = add_name (Name id) None t' env in - let appc = mkApp (lift 1 c,[|mkRel 1|]) in - share_names d flags (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c' - (* If built with the f/n notation: we renounce to share names *) - | _ -> - if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough"); - let c = detype d flags avoid env sigma c in - let t = detype d flags avoid env sigma t in - (List.rev l,c,t) + | Fix (nvn,recdef) -> detype_fix (detype d flags) avoid env sigma nvn recdef + | CoFix (n,recdef) -> detype_cofix (detype d flags) avoid env sigma n recdef and detype_eqns d flags avoid env sigma ci computable constructs consnargsl bl = try @@ -902,7 +925,7 @@ let rec subst_cases_pattern subst = DAst.map (function | PatVar _ as pat -> pat | PatCstr (((kn,i),j),cpl,n) as pat -> let kn' = subst_mind subst kn - and cpl' = List.smartmap (subst_cases_pattern subst) cpl in + and cpl' = List.Smart.map (subst_cases_pattern subst) cpl in if kn' == kn && cpl' == cpl then pat else PatCstr (((kn',i),j),cpl',n) ) @@ -911,9 +934,11 @@ let (f_subst_genarg, subst_genarg_hook) = Hook.make () let rec subst_glob_constr subst = DAst.map (function | GRef (ref,u) as raw -> - let ref',t = subst_global subst ref in - if ref' == ref then raw else - DAst.get (detype Now false Id.Set.empty (Global.env()) Evd.empty (EConstr.of_constr t)) + let ref',t = subst_global subst ref in + if ref' == ref then raw else + let env = Global.env () in + let evd = Evd.from_env env in + DAst.get (detype Now false Id.Set.empty env evd (EConstr.of_constr t)) | GSort _ | GVar _ @@ -922,7 +947,7 @@ let rec subst_glob_constr subst = DAst.map (function | GApp (r,rl) as raw -> let r' = subst_glob_constr subst r - and rl' = List.smartmap (subst_glob_constr subst) rl in + and rl' = List.Smart.map (subst_glob_constr subst) rl in if r' == r && rl' == rl then raw else GApp(r',rl') @@ -939,25 +964,25 @@ let rec subst_glob_constr subst = DAst.map (function | GLetIn (n,r1,t,r2) as raw -> let r1' = subst_glob_constr subst r1 in let r2' = subst_glob_constr subst r2 in - let t' = Option.smartmap (subst_glob_constr subst) t in + let t' = Option.Smart.map (subst_glob_constr subst) t in if r1' == r1 && t == t' && r2' == r2 then raw else GLetIn (n,r1',t',r2') | GCases (sty,rtno,rl,branches) as raw -> let open CAst in - let rtno' = Option.smartmap (subst_glob_constr subst) rtno - and rl' = List.smartmap (fun (a,x as y) -> + let rtno' = Option.Smart.map (subst_glob_constr subst) rtno + and rl' = List.Smart.map (fun (a,x as y) -> let a' = subst_glob_constr subst a in let (n,topt) = x in - let topt' = Option.smartmap + let topt' = Option.Smart.map (fun ({loc;v=((sp,i),y)} as t) -> let sp' = subst_mind subst sp in if sp == sp' then t else CAst.(make ?loc ((sp',i),y))) topt in if a == a' && topt == topt' then y else (a',(n,topt'))) rl - and branches' = List.smartmap + and branches' = List.Smart.map (fun ({loc;v=(idl,cpl,r)} as branch) -> let cpl' = - List.smartmap (subst_cases_pattern subst) cpl + List.Smart.map (subst_cases_pattern subst) cpl and r' = subst_glob_constr subst r in if cpl' == cpl && r' == r then branch else CAst.(make ?loc (idl,cpl',r'))) @@ -967,14 +992,14 @@ let rec subst_glob_constr subst = DAst.map (function GCases (sty,rtno',rl',branches') | GLetTuple (nal,(na,po),b,c) as raw -> - let po' = Option.smartmap (subst_glob_constr subst) po + let po' = Option.Smart.map (subst_glob_constr subst) po and b' = subst_glob_constr subst b and c' = subst_glob_constr subst c in if po' == po && b' == b && c' == c then raw else GLetTuple (nal,(na,po'),b',c') | GIf (c,(na,po),b1,b2) as raw -> - let po' = Option.smartmap (subst_glob_constr subst) po + let po' = Option.Smart.map (subst_glob_constr subst) po and b1' = subst_glob_constr subst b1 and b2' = subst_glob_constr subst b2 and c' = subst_glob_constr subst c in @@ -982,12 +1007,12 @@ let rec subst_glob_constr subst = DAst.map (function GIf (c',(na,po'),b1',b2') | GRec (fix,ida,bl,ra1,ra2) as raw -> - let ra1' = Array.smartmap (subst_glob_constr subst) ra1 - and ra2' = Array.smartmap (subst_glob_constr subst) ra2 in - let bl' = Array.smartmap - (List.smartmap (fun (na,k,obd,ty as dcl) -> + let ra1' = Array.Smart.map (subst_glob_constr subst) ra1 + and ra2' = Array.Smart.map (subst_glob_constr subst) ra2 in + let bl' = Array.Smart.map + (List.Smart.map (fun (na,k,obd,ty as dcl) -> let ty' = subst_glob_constr subst ty in - let obd' = Option.smartmap (subst_glob_constr subst) obd in + let obd' = Option.Smart.map (subst_glob_constr subst) obd in if ty'==ty && obd'==obd then dcl else (na,k,obd',ty'))) bl in if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else @@ -1000,14 +1025,15 @@ let rec subst_glob_constr subst = DAst.map (function if nref == ref then knd else Evar_kinds.ImplicitArg (nref, i, b) | _ -> knd in - let nsolve = Option.smartmap (Hook.get f_subst_genarg subst) solve in + let nsolve = Option.Smart.map (Hook.get f_subst_genarg subst) solve in if nsolve == solve && nknd == knd then raw else GHole (nknd, naming, nsolve) | GCast (r1,k) as raw -> let r1' = subst_glob_constr subst r1 in - let k' = Miscops.smartmap_cast_type (subst_glob_constr subst) k in + let k' = smartmap_cast_type (subst_glob_constr subst) k in if r1' == r1 && k' == k then raw else GCast (r1',k') + ) (* Utilities to transform kernel cases to simple pattern-matching problem *) -- cgit v1.2.3