summaryrefslogtreecommitdiff
path: root/pretyping/detyping.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/detyping.ml')
-rw-r--r--pretyping/detyping.ml230
1 files changed, 115 insertions, 115 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 20cbba94..9552fc24 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: detyping.ml 12887 2010-03-27 15:57:02Z herbelin $ *)
+(* $Id$ *)
open Pp
open Util
@@ -21,6 +21,7 @@ open Sign
open Rawterm
open Nameops
open Termops
+open Namegen
open Libnames
open Nametab
open Evd
@@ -32,7 +33,7 @@ let dl = dummy_loc
(* Tools for printing of Cases *)
let encode_inductive r =
- let indsp = inductive_of_reference r in
+ let indsp = global_inductive r in
let constr_lengths = mis_constr_nargs indsp in
(indsp,constr_lengths)
@@ -60,7 +61,7 @@ let encode_tuple r =
x
module PrintingCasesMake =
- functor (Test : sig
+ functor (Test : sig
val encode : reference -> inductive * int array
val member_message : std_ppcmds -> bool -> std_ppcmds
val field : string
@@ -70,33 +71,33 @@ module PrintingCasesMake =
type t = inductive * int array
let encode = Test.encode
let subst subst ((kn,i), ints as obj) =
- let kn' = subst_kn subst kn in
+ let kn' = subst_ind subst kn in
if kn' == kn then obj else
(kn',i), ints
let printer (ind,_) = pr_global_env Idset.empty (IndRef ind)
- let key = Goptions.SecondaryTable ("Printing",Test.field)
+ let key = ["Printing";Test.field]
let title = Test.title
let member_message x = Test.member_message (printer x)
let synchronous = true
end
module PrintingCasesIf =
- PrintingCasesMake (struct
+ PrintingCasesMake (struct
let encode = encode_bool
let field = "If"
let title = "Types leading to pretty-printing of Cases using a `if' form: "
let member_message s b =
- str "Cases on elements of " ++ s ++
+ str "Cases on elements of " ++ s ++
str
(if b then " are printed using a `if' form"
else " are not printed using a `if' form")
end)
module PrintingCasesLet =
- PrintingCasesMake (struct
+ PrintingCasesMake (struct
let encode = encode_tuple
let field = "Let"
- let title =
+ let title =
"Types leading to a pretty-printing of Cases using a `let' form:"
let member_message s b =
str "Cases on elements of " ++ s ++
@@ -115,30 +116,30 @@ open Goptions
let wildcard_value = ref true
let force_wildcard () = !wildcard_value
-let _ = declare_bool_option
+let _ = declare_bool_option
{ optsync = true;
optname = "forced wildcard";
- optkey = SecondaryTable ("Printing","Wildcard");
+ optkey = ["Printing";"Wildcard"];
optread = force_wildcard;
optwrite = (:=) wildcard_value }
let synth_type_value = ref true
let synthetize_type () = !synth_type_value
-let _ = declare_bool_option
+let _ = declare_bool_option
{ optsync = true;
optname = "pattern matching return type synthesizability";
- optkey = SecondaryTable ("Printing","Synth");
+ optkey = ["Printing";"Synth"];
optread = synthetize_type;
optwrite = (:=) synth_type_value }
let reverse_matching_value = ref true
let reverse_matching () = !reverse_matching_value
-let _ = declare_bool_option
+let _ = declare_bool_option
{ optsync = true;
optname = "pattern-matching reversibility";
- optkey = SecondaryTable ("Printing","Matching");
+ optkey = ["Printing";"Matching"];
optread = reverse_matching;
optwrite = (:=) reverse_matching_value }
@@ -162,52 +163,48 @@ let computable p k =
sinon on perd la réciprocité de la synthèse (qui, lui,
engendrera un prédicat non dépendant) *)
- (nb_lam p = k+1)
+ let sign,ccl = decompose_lam_assum p in
+ (rel_context_length sign = k+1)
&&
- let _,ccl = decompose_lam p in
noccur_between 1 (k+1) ccl
let avoid_flag isgoal = if isgoal then Some true else None
-
-let lookup_name_as_renamed env t s =
- let rec lookup avoid env_names n c = match kind_of_term c with
+
+let lookup_name_as_displayed env t s =
+ let rec lookup avoid n c = match kind_of_term c with
| Prod (name,_,c') ->
- (match concrete_name (Some true) avoid env_names name c' with
- | (Name id,avoid') ->
- if id=s then (Some n)
- else lookup avoid' (add_name (Name id) env_names) (n+1) c'
- | (Anonymous,avoid') -> lookup avoid' env_names (n+1) (pop c'))
+ (match compute_displayed_name_in RenamingForGoal avoid name c' with
+ | (Name id,avoid') -> if id=s then Some n else lookup avoid' (n+1) c'
+ | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c'))
| LetIn (name,_,_,c') ->
- (match concrete_name (Some true) avoid env_names name c' with
- | (Name id,avoid') ->
- if id=s then (Some n)
- else lookup avoid' (add_name (Name id) env_names) (n+1) c'
- | (Anonymous,avoid') -> lookup avoid' env_names (n+1) (pop c'))
- | Cast (c,_,_) -> lookup avoid env_names n c
+ (match compute_displayed_name_in RenamingForGoal avoid name c' with
+ | (Name id,avoid') -> if id=s then Some n else lookup avoid' (n+1) c'
+ | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c'))
+ | Cast (c,_,_) -> lookup avoid n c
| _ -> None
- in lookup (ids_of_named_context (named_context env)) empty_names_context 1 t
+ in lookup (ids_of_named_context (named_context env)) 1 t
let lookup_index_as_renamed env t n =
let rec lookup n d c = match kind_of_term c with
| Prod (name,_,c') ->
- (match concrete_name (Some true) [] empty_names_context name c' with
+ (match compute_displayed_name_in RenamingForGoal [] name c' with
(Name _,_) -> lookup n (d+1) c'
- | (Anonymous,_) ->
+ | (Anonymous,_) ->
if n=0 then
Some (d-1)
- else if n=1 then
- Some d
- else
+ else if n=1 then
+ Some d
+ else
lookup (n-1) (d+1) c')
| LetIn (name,_,_,c') ->
- (match concrete_name (Some true) [] empty_names_context name c' with
+ (match compute_displayed_name_in RenamingForGoal [] name c' with
| (Name _,_) -> lookup n (d+1) c'
- | (Anonymous,_) ->
- if n=0 then
- Some (d-1)
- else if n=1 then
- Some d
- else
+ | (Anonymous,_) ->
+ if n=0 then
+ Some (d-1)
+ else if n=1 then
+ Some d
+ else
lookup (n-1) (d+1) c'
)
| Cast (c,_,_) -> lookup n d c
@@ -225,16 +222,17 @@ let update_name na ((_,e),c) =
na
let rec decomp_branch n nal b (avoid,env as e) c =
+ let flag = if b then RenamingForGoal else RenamingForCasesPattern in
if n=0 then (List.rev nal,(e,c))
else
let na,c,f =
match kind_of_term (strip_outer_cast c) with
- | Lambda (na,_,c) -> na,c,concrete_let_name
- | LetIn (na,_,_,c) -> na,c,concrete_name
- | _ ->
- Name (id_of_string "x"),(applist (lift 1 c, [mkRel 1])),
- concrete_name in
- let na',avoid' = f (Some b) avoid env na c in
+ | Lambda (na,_,c) -> na,c,compute_displayed_let_name_in
+ | LetIn (na,_,_,c) -> na,c,compute_displayed_name_in
+ | _ ->
+ Name (id_of_string "x"),(applist (lift 1 c, [mkRel 1])),
+ compute_displayed_name_in in
+ let na',avoid' = f flag avoid na c in
decomp_branch (n-1) (na'::nal) b (avoid',add_name na' env) c
let rec build_tree na isgoal e ci cl =
@@ -248,14 +246,14 @@ and align_tree nal isgoal (e,c as rhs) = match nal with
| [] -> [[],rhs]
| na::nal ->
match kind_of_term c with
- | Case (ci,p,c,cl) when c = mkRel (list_index na (snd e))
+ | Case (ci,p,c,cl) when c = mkRel (list_index na (snd e))
& (* don't contract if p dependent *)
computable p (ci.ci_pp_info.ind_nargs) ->
let clauses = build_tree na isgoal e ci cl in
List.flatten
(List.map (fun (pat,rhs) ->
let lines = align_tree nal isgoal rhs in
- List.map (fun (hd,rest) -> pat::hd,rest) lines)
+ List.map (fun (hd,rest) -> pat::hd,rest) lines)
clauses)
| _ ->
let pat = PatVar(dl,update_name na rhs) in
@@ -294,14 +292,14 @@ let it_destRLambda_or_LetIn_names n c =
| _ ->
(* eta-expansion *)
let rec next l =
- let x = Nameops.next_ident_away (id_of_string "x") l in
+ let x = next_ident_away (id_of_string "x") l in
(* Not efficient but unusual and no function to get free rawvars *)
(* if occur_rawconstr x c then next (x::l) else x in *)
x
in
- let x = next (free_rawvars c) in
+ let x = next (free_rawvars c) in
let a = RVar (dl,x) in
- aux (n-1) (Name x :: nal)
+ aux (n-1) (Name x :: nal)
(match c with
| RApp (loc,p,l) -> RApp (loc,c,l@[a])
| _ -> (RApp (dl,c,[a])))
@@ -311,16 +309,16 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
let (indsp,st,nparams,consnargsl,k) = data in
let synth_type = synthetize_type () in
let tomatch = detype c in
- let alias, aliastyp, pred=
- if (not !Flags.raw_print) & synth_type & computable & Array.length bl<>0
- then
+ let alias, aliastyp, pred=
+ if (not !Flags.raw_print) & synth_type & computable & Array.length bl<>0
+ then
Anonymous, None, None
else
match Option.map detype p with
| None -> Anonymous, None, None
| Some p ->
let nl,typ = it_destRLambda_or_LetIn_names k p in
- let n,typ = match typ with
+ let n,typ = match typ with
| RLambda (_,x,_,t,c) -> x, c
| _ -> Anonymous, typ in
let aliastyp =
@@ -330,21 +328,21 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
in
let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in
let tag =
- try
+ try
if !Flags.raw_print then
RegularStyle
- else if st = LetPatternStyle then
+ else if st = LetPatternStyle then
st
else if PrintingLet.active (indsp,consnargsl) then
LetStyle
- else if PrintingIf.active (indsp,consnargsl) then
+ else if PrintingIf.active (indsp,consnargsl) then
IfStyle
- else
+ else
st
with Not_found -> st
in
match tag with
- | LetStyle when aliastyp = None ->
+ | LetStyle when aliastyp = None ->
let bl' = Array.map detype bl in
let (nal,d) = it_destRLambda_or_LetIn_names consnargsl.(0) bl'.(0) in
RLetTuple (dl,nal,(alias,pred),tomatch,d)
@@ -400,7 +398,7 @@ let rec detype (isgoal:bool) avoid env t =
array_map_to_list (detype isgoal avoid env) args)
| Const sp -> RRef (dl, ConstRef sp)
| Evar (ev,cl) ->
- REvar (dl, ev,
+ REvar (dl, ev,
Some (List.map (detype isgoal avoid env) (Array.to_list cl)))
| Ind ind_sp ->
RRef (dl, IndRef ind_sp)
@@ -410,7 +408,7 @@ let rec detype (isgoal:bool) avoid env t =
let comp = computable p (ci.ci_pp_info.ind_nargs) in
detype_case comp (detype isgoal avoid env)
(detype_eqns isgoal avoid env ci comp)
- is_nondep_branch avoid
+ is_nondep_branch avoid
(ci.ci_ind,ci.ci_pp_info.style,ci.ci_npar,
ci.ci_cstr_nargs,ci.ci_pp_info.ind_nargs)
(Some p) c bl
@@ -421,7 +419,7 @@ and detype_fix isgoal avoid env (vn,_ as nvn) (names,tys,bodies) =
let def_avoid, def_env, lfi =
Array.fold_left
(fun (avoid, env, l) na ->
- let id = next_name_away na avoid in
+ let id = next_name_away na avoid in
(id::avoid, add_name (Name id) env, id::l))
(avoid, env, []) names in
let n = Array.length tys in
@@ -437,7 +435,7 @@ and detype_cofix isgoal avoid env n (names,tys,bodies) =
let def_avoid, def_env, lfi =
Array.fold_left
(fun (avoid, env, l) na ->
- let id = next_name_away na avoid in
+ let id = next_name_away na avoid in
(id::avoid, add_name (Name id) env, id::l))
(avoid, env, []) names in
let ntys = Array.length tys in
@@ -456,16 +454,16 @@ and share_names isgoal n l avoid env c t =
let na = match (na,na') with
Name _, _ -> na
| _, Name _ -> na'
- | _ -> na in
+ | _ -> na in
let t = detype isgoal avoid env t in
- let id = next_name_away na avoid in
+ let id = next_name_away na avoid in
let avoid = id::avoid and env = add_name (Name id) env in
share_names isgoal (n-1) ((Name id,Explicit,None,t)::l) avoid env c c'
(* May occur for fix built interactively *)
| LetIn (na,b,t',c), _ when n > 0 ->
let t' = detype isgoal avoid env t' in
let b = detype isgoal avoid env b in
- let id = next_name_away na avoid in
+ let id = next_name_away na avoid in
let avoid = id::avoid and env = add_name (Name id) env in
share_names isgoal n ((Name id,Explicit,Some b,t')::l) avoid env c t
(* Only if built with the f/n notation or w/o let-expansion in types *)
@@ -474,7 +472,7 @@ and share_names isgoal n l avoid env c t =
(* If it is an open proof: we cheat and eta-expand *)
| _, Prod (na',t',c') when n > 0 ->
let t' = detype isgoal avoid env t' in
- let id = next_name_away na' avoid in
+ let id = next_name_away na' avoid in
let avoid = id::avoid and env = add_name (Name id) env in
let appc = mkApp (lift 1 c,[|mkRel 1|]) in
share_names isgoal (n-1) ((Name id,Explicit,None,t')::l) avoid env appc c'
@@ -499,22 +497,22 @@ and detype_eqn isgoal avoid env constr construct_nargs branch =
let make_pat x avoid env b ids =
if force_wildcard () & noccurn 1 b then
PatVar (dl,Anonymous),avoid,(add_name Anonymous env),ids
- else
+ else
let id = next_name_away_in_cases_pattern x avoid in
PatVar (dl,Name id),id::avoid,(add_name (Name id) env),id::ids
in
let rec buildrec ids patlist avoid env n b =
if n=0 then
- (dl, ids,
+ (dl, ids,
[PatCstr(dl, constr, List.rev patlist,Anonymous)],
detype isgoal avoid env b)
else
match kind_of_term b with
- | Lambda (x,_,b) ->
+ | Lambda (x,_,b) ->
let pat,new_avoid,new_env,new_ids = make_pat x avoid env b ids in
buildrec new_ids (pat::patlist) new_avoid new_env (n-1) b
- | LetIn (x,_,_,b) ->
+ | LetIn (x,_,_,b) ->
let pat,new_avoid,new_env,new_ids = make_pat x avoid env b ids in
buildrec new_ids (pat::patlist) new_avoid new_env (n-1) b
@@ -528,21 +526,20 @@ and detype_eqn isgoal avoid env constr construct_nargs branch =
let pat,new_avoid,new_env,new_ids =
make_pat Anonymous avoid env new_b ids in
buildrec new_ids (pat::patlist) new_avoid new_env (n-1) new_b
-
- in
+
+ in
buildrec [] [] avoid env construct_nargs branch
and detype_binder isgoal bk avoid env na ty c =
+ let flag = if isgoal then RenamingForGoal else (RenamingElsewhereFor c) in
let na',avoid' =
- if bk = BLetIn then
- concrete_let_name (avoid_flag isgoal) avoid env na c
- else
- concrete_name (avoid_flag isgoal) avoid env na c in
+ if bk = BLetIn then compute_displayed_let_name_in flag avoid na c
+ else compute_displayed_name_in flag avoid na c in
let r = detype isgoal avoid' (add_name na' env) c in
match bk with
- | BProd -> RProd (dl, na',Explicit,detype isgoal avoid env ty, r)
- | BLambda -> RLambda (dl, na',Explicit,detype isgoal avoid env ty, r)
- | BLetIn -> RLetIn (dl, na',detype isgoal avoid env ty, r)
+ | BProd -> RProd (dl, na',Explicit,detype false avoid env ty, r)
+ | BLambda -> RLambda (dl, na',Explicit,detype false avoid env ty, r)
+ | BLetIn -> RLetIn (dl, na',detype false avoid env ty, r)
let rec detype_rel_context where avoid env sign =
let where = Option.map (fun c -> it_mkLambda_or_LetIn c sign) where in
@@ -553,8 +550,10 @@ let rec detype_rel_context where avoid env sign =
match where with
| None -> na,avoid
| Some c ->
- if b<>None then concrete_let_name None avoid env na c
- else concrete_name None avoid env na c in
+ if b<>None then
+ compute_displayed_let_name_in (RenamingElsewhereFor c) avoid na c
+ else
+ compute_displayed_name_in (RenamingElsewhereFor c) avoid na c in
let b = Option.map (detype false avoid env) b in
let t = detype false avoid env t in
(na',Explicit,b,t) :: aux avoid' (add_name na' env) rest
@@ -563,19 +562,19 @@ let rec detype_rel_context where avoid env sign =
(**********************************************************************)
(* Module substitution: relies on detyping *)
-let rec subst_cases_pattern subst pat =
+let rec subst_cases_pattern subst pat =
match pat with
| PatVar _ -> pat
- | PatCstr (loc,((kn,i),j),cpl,n) ->
- let kn' = subst_kn subst kn
+ | PatCstr (loc,((kn,i),j),cpl,n) ->
+ let kn' = subst_ind subst kn
and cpl' = list_smartmap (subst_cases_pattern subst) cpl in
if kn' == kn && cpl' == cpl then pat else
PatCstr (loc,((kn',i),j),cpl',n)
-let rec subst_rawconstr subst raw =
+let rec subst_rawconstr subst raw =
match raw with
- | RRef (loc,ref) ->
- let ref',t = subst_global subst ref in
+ | RRef (loc,ref) ->
+ let ref',t = subst_global subst ref in
if ref' == ref then raw else
detype false [] [] t
@@ -583,38 +582,38 @@ let rec subst_rawconstr subst raw =
| REvar _ -> raw
| RPatVar _ -> raw
- | RApp (loc,r,rl) ->
- let r' = subst_rawconstr subst r
+ | RApp (loc,r,rl) ->
+ let r' = subst_rawconstr subst r
and rl' = list_smartmap (subst_rawconstr subst) rl in
if r' == r && rl' == rl then raw else
RApp(loc,r',rl')
- | RLambda (loc,n,bk,r1,r2) ->
+ | RLambda (loc,n,bk,r1,r2) ->
let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in
if r1' == r1 && r2' == r2 then raw else
RLambda (loc,n,bk,r1',r2')
- | RProd (loc,n,bk,r1,r2) ->
+ | RProd (loc,n,bk,r1,r2) ->
let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in
if r1' == r1 && r2' == r2 then raw else
RProd (loc,n,bk,r1',r2')
- | RLetIn (loc,n,r1,r2) ->
+ | RLetIn (loc,n,r1,r2) ->
let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in
if r1' == r1 && r2' == r2 then raw else
RLetIn (loc,n,r1',r2')
- | RCases (loc,sty,rtno,rl,branches) ->
+ | RCases (loc,sty,rtno,rl,branches) ->
let rtno' = Option.smartmap (subst_rawconstr subst) rtno
and rl' = list_smartmap (fun (a,x as y) ->
let a' = subst_rawconstr subst a in
- let (n,topt) = x in
+ let (n,topt) = x in
let topt' = Option.smartmap
(fun (loc,(sp,i),x,y as t) ->
- let sp' = subst_kn subst sp in
+ let sp' = subst_ind subst sp in
if sp == sp' then t else (loc,(sp',i),x,y)) topt in
if a == a' && topt == topt' then y else (a',(n,topt'))) rl
- and branches' = list_smartmap
+ and branches' = list_smartmap
(fun (loc,idl,cpl,r as branch) ->
let cpl' =
list_smartmap (subst_cases_pattern subst) cpl
@@ -628,20 +627,20 @@ let rec subst_rawconstr subst raw =
| RLetTuple (loc,nal,(na,po),b,c) ->
let po' = Option.smartmap (subst_rawconstr subst) po
- and b' = subst_rawconstr subst b
+ and b' = subst_rawconstr subst b
and c' = subst_rawconstr subst c in
if po' == po && b' == b && c' == c then raw else
RLetTuple (loc,nal,(na,po'),b',c')
-
+
| RIf (loc,c,(na,po),b1,b2) ->
let po' = Option.smartmap (subst_rawconstr subst) po
- and b1' = subst_rawconstr subst b1
- and b2' = subst_rawconstr subst b2
+ and b1' = subst_rawconstr subst b1
+ and b2' = subst_rawconstr subst b2
and c' = subst_rawconstr subst c in
if c' == c & po' == po && b1' == b1 && b2' == b2 then raw else
RIf (loc,c',(na,po'),b1',b2')
- | RRec (loc,fix,ida,bl,ra1,ra2) ->
+ | RRec (loc,fix,ida,bl,ra1,ra2) ->
let ra1' = array_smartmap (subst_rawconstr subst) ra1
and ra2' = array_smartmap (subst_rawconstr subst) ra2 in
let bl' = array_smartmap
@@ -655,20 +654,21 @@ let rec subst_rawconstr subst raw =
| RSort _ -> raw
- | RHole (loc,ImplicitArg (ref,i)) ->
- let ref',_ = subst_global subst ref in
+ | RHole (loc,ImplicitArg (ref,i,b)) ->
+ let ref',_ = subst_global subst ref in
if ref' == ref then raw else
RHole (loc,InternalHole)
| RHole (loc, (BinderType _ | QuestionMark _ | CasesType | InternalHole |
- TomatchTypeParameter _ | GoalEvar | ImpossibleCase)) -> raw
+ TomatchTypeParameter _ | GoalEvar | ImpossibleCase | MatchingVar _)) ->
+ raw
- | RCast (loc,r1,k) ->
- (match k with
+ | RCast (loc,r1,k) ->
+ (match k with
CastConv (k,r2) ->
let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in
if r1' == r1 && r2' == r2 then raw else
RCast (loc,r1', CastConv (k,r2'))
- | CastCoerce ->
+ | CastCoerce ->
let r1' = subst_rawconstr subst r1 in
if r1' == r1 then raw else RCast (loc,r1',k))
| RDynamic _ -> raw
@@ -684,6 +684,6 @@ let simple_cases_matrix_of_branches ind brns brs =
(dummy_loc,ids,[p],c))
0 brns brs
-let return_type_of_predicate ind nparams n pred =
- let nal,p = it_destRLambda_or_LetIn_names (n+1) pred in
+let return_type_of_predicate ind nparams nrealargs_ctxt pred =
+ let nal,p = it_destRLambda_or_LetIn_names (nrealargs_ctxt+1) pred in
(List.hd nal, Some (dummy_loc, ind, nparams, List.tl nal)), Some p
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 08:33:27 +0000