summaryrefslogtreecommitdiff
path: root/pretyping/termops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/termops.ml')
-rw-r--r--pretyping/termops.ml938
1 files changed, 938 insertions, 0 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
new file mode 100644
index 00000000..8f12ca62
--- /dev/null
+++ b/pretyping/termops.ml
@@ -0,0 +1,938 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id: termops.ml,v 1.29.2.1 2004/07/16 19:30:46 herbelin Exp $ *)
+
+open Pp
+open Util
+open Names
+open Nameops
+open Term
+open Sign
+open Environ
+open Libnames
+open Nametab
+
+(* Sorts and sort family *)
+
+let print_sort = function
+ | Prop Pos -> (str "Set")
+ | Prop Null -> (str "Prop")
+ | Type u -> (str "Type(" ++ Univ.pr_uni u ++ str ")")
+
+let print_sort_family = function
+ | InSet -> (str "Set")
+ | InProp -> (str "Prop")
+ | InType -> (str "Type")
+
+let pr_name = function
+ | Name id -> pr_id id
+ | Anonymous -> str "_"
+
+let pr_sp sp = str(string_of_kn sp)
+
+let rec print_constr c = match kind_of_term c with
+ | Rel n -> str "#"++int n
+ | Meta n -> str "Meta(" ++ int n ++ str ")"
+ | Var id -> pr_id id
+ | Sort s -> print_sort s
+ | Cast (c,t) -> hov 1
+ (str"(" ++ print_constr c ++ cut() ++
+ str":" ++ print_constr t ++ str")")
+ | Prod (Name(id),t,c) -> hov 1
+ (str"forall " ++ pr_id id ++ str":" ++ print_constr t ++ str"," ++
+ spc() ++ print_constr c)
+ | Prod (Anonymous,t,c) -> hov 0
+ (str"(" ++ print_constr t ++ str " ->" ++ spc() ++
+ print_constr c ++ str")")
+ | Lambda (na,t,c) -> hov 1
+ (str"fun " ++ pr_name na ++ str":" ++
+ print_constr t ++ str" =>" ++ spc() ++ print_constr c)
+ | LetIn (na,b,t,c) -> hov 0
+ (str"let " ++ pr_name na ++ str":=" ++ print_constr b ++
+ str":" ++ brk(1,2) ++ print_constr t ++ cut() ++
+ print_constr c)
+ | App (c,l) -> hov 1
+ (str"(" ++ print_constr c ++ spc() ++
+ prlist_with_sep spc print_constr (Array.to_list l) ++ str")")
+ | Evar (e,l) -> hov 1
+ (str"Evar#" ++ int e ++ str"{" ++
+ prlist_with_sep spc print_constr (Array.to_list l) ++str"}")
+ | Const c -> str"Cst(" ++ pr_sp c ++ str")"
+ | Ind (sp,i) -> str"Ind(" ++ pr_sp sp ++ str"," ++ int i ++ str")"
+ | Construct ((sp,i),j) ->
+ str"Constr(" ++ pr_sp sp ++ str"," ++ int i ++ str"," ++ int j ++ str")"
+ | Case (ci,p,c,bl) -> v 0
+ (hv 0 (str"<"++print_constr p++str">"++ cut() ++ str"Case " ++
+ print_constr c ++ str"of") ++ cut() ++
+ prlist_with_sep (fun _ -> brk(1,2)) print_constr (Array.to_list bl) ++
+ cut() ++ str"end")
+ | Fix ((t,i),(lna,tl,bl)) ->
+ let fixl = Array.mapi (fun i na -> (na,t.(i),tl.(i),bl.(i))) lna in
+ hov 1
+ (str"fix " ++ int i ++ spc() ++ str"{" ++
+ v 0 (prlist_with_sep spc (fun (na,i,ty,bd) ->
+ pr_name na ++ str"/" ++ int i ++ str":" ++ print_constr ty ++
+ cut() ++ str":=" ++ print_constr bd) (Array.to_list fixl)) ++
+ str"}")
+ | CoFix(i,(lna,tl,bl)) ->
+ let fixl = Array.mapi (fun i na -> (na,tl.(i),bl.(i))) lna in
+ hov 1
+ (str"cofix " ++ int i ++ spc() ++ str"{" ++
+ v 0 (prlist_with_sep spc (fun (na,ty,bd) ->
+ pr_name na ++ str":" ++ print_constr ty ++
+ cut() ++ str":=" ++ print_constr bd) (Array.to_list fixl)) ++
+ str"}")
+
+(*let current_module = ref empty_dirpath
+
+let set_module m = current_module := m*)
+
+let new_univ =
+ let univ_gen = ref 0 in
+ (fun sp ->
+ incr univ_gen;
+ Univ.make_univ (Lib.library_dp(),!univ_gen))
+
+let new_sort_in_family = function
+ | InProp -> mk_Prop
+ | InSet -> mk_Set
+ | InType -> Type (new_univ ())
+
+
+
+(* prod_it b [xn:Tn;..;x1:T1] = (x1:T1)..(xn:Tn)b *)
+let prod_it ~init = List.fold_left (fun c (n,t) -> mkProd (n, t, c)) init
+
+(* lam_it b [xn:Tn;..;x1:T1] = [x1:T1]..[xn:Tn]b *)
+let lam_it ~init = List.fold_left (fun c (n,t) -> mkLambda (n, t, c)) init
+
+(* [Rel (n+m);...;Rel(n+1)] *)
+let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i))
+
+let rel_list n m =
+ let rec reln l p =
+ if p>m then l else reln (mkRel(n+p)::l) (p+1)
+ in
+ reln [] 1
+
+(* Same as [rel_list] but takes a context as argument and skips let-ins *)
+let extended_rel_list n hyps =
+ let rec reln l p = function
+ | (_,None,_) :: hyps -> reln (mkRel (n+p) :: l) (p+1) hyps
+ | (_,Some _,_) :: hyps -> reln l (p+1) hyps
+ | [] -> l
+ in
+ reln [] 1 hyps
+
+let extended_rel_vect n hyps = Array.of_list (extended_rel_list n hyps)
+
+
+
+let push_rel_assum (x,t) env = push_rel (x,None,t) env
+
+let push_rels_assum assums =
+ push_rel_context (List.map (fun (x,t) -> (x,None,t)) assums)
+
+let push_named_rec_types (lna,typarray,_) env =
+ let ctxt =
+ array_map2_i
+ (fun i na t ->
+ match na with
+ | Name id -> (id, None, type_app (lift i) t)
+ | Anonymous -> anomaly "Fix declarations must be named")
+ lna typarray in
+ Array.fold_left
+ (fun e assum -> push_named assum e) env ctxt
+
+let rec lookup_rel_id id sign =
+ let rec lookrec = function
+ | (n, (Anonymous,_,_)::l) -> lookrec (n+1,l)
+ | (n, (Name id',_,t)::l) -> if id' = id then (n,t) else lookrec (n+1,l)
+ | (_, []) -> raise Not_found
+ in
+ lookrec (1,sign)
+
+(* Constructs either [(x:t)c] or [[x=b:t]c] *)
+let mkProd_or_LetIn (na,body,t) c =
+ match body with
+ | None -> mkProd (na, t, c)
+ | Some b -> mkLetIn (na, b, t, c)
+
+(* Constructs either [(x:t)c] or [c] where [x] is replaced by [b] *)
+let mkProd_wo_LetIn (na,body,t) c =
+ match body with
+ | None -> mkProd (na, t, c)
+ | Some b -> subst1 b c
+
+let it_mkProd_wo_LetIn ~init =
+ List.fold_left (fun c d -> mkProd_wo_LetIn d c) init
+
+let it_mkProd_or_LetIn ~init =
+ List.fold_left (fun c d -> mkProd_or_LetIn d c) init
+
+let it_mkLambda_or_LetIn ~init =
+ List.fold_left (fun c d -> mkLambda_or_LetIn d c) init
+
+let it_named_context_quantifier f ~init =
+ List.fold_left (fun c d -> f d c) init
+
+let it_mkNamedProd_or_LetIn = it_named_context_quantifier mkNamedProd_or_LetIn
+let it_mkNamedLambda_or_LetIn = it_named_context_quantifier mkNamedLambda_or_LetIn
+
+(* *)
+
+(* strips head casts and flattens head applications *)
+let rec strip_head_cast c = match kind_of_term c with
+ | App (f,cl) ->
+ let rec collapse_rec f cl2 = match kind_of_term f with
+ | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
+ | Cast (c,_) -> collapse_rec c cl2
+ | _ -> if cl2 = [||] then f else mkApp (f,cl2)
+ in
+ collapse_rec f cl
+ | Cast (c,t) -> strip_head_cast c
+ | _ -> c
+
+(* [map_constr_with_named_binders g f l c] maps [f l] on the immediate
+ subterms of [c]; it carries an extra data [l] (typically a name
+ list) which is processed by [g na] (which typically cons [na] to
+ [l]) at each binder traversal (with name [na]); it is not recursive
+ and the order with which subterms are processed is not specified *)
+
+let map_constr_with_named_binders g f l c = match kind_of_term c with
+ | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
+ | Construct _) -> c
+ | Cast (c,t) -> mkCast (f l c, f l t)
+ | Prod (na,t,c) -> mkProd (na, f l t, f (g na l) c)
+ | Lambda (na,t,c) -> mkLambda (na, f l t, f (g na l) c)
+ | LetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g na l) c)
+ | App (c,al) -> mkApp (f l c, Array.map (f l) al)
+ | Evar (e,al) -> mkEvar (e, Array.map (f l) al)
+ | Case (ci,p,c,bl) -> mkCase (ci, f l p, f l c, Array.map (f l) bl)
+ | Fix (ln,(lna,tl,bl)) ->
+ let l' = Array.fold_left (fun l na -> g na l) l lna in
+ mkFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
+ | CoFix(ln,(lna,tl,bl)) ->
+ let l' = Array.fold_left (fun l na -> g na l) l lna in
+ mkCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
+
+(* [map_constr_with_binders_left_to_right g f n c] maps [f n] on the
+ immediate subterms of [c]; it carries an extra data [n] (typically
+ a lift index) which is processed by [g] (which typically add 1 to
+ [n]) at each binder traversal; the subterms are processed from left
+ to right according to the usual representation of the constructions
+ (this may matter if [f] does a side-effect); it is not recursive;
+ in fact, the usual representation of the constructions is at the
+ time being almost those of the ML representation (except for
+ (co-)fixpoint) *)
+
+let fold_rec_types g (lna,typarray,_) e =
+ let ctxt =
+ array_map2_i
+ (fun i na t -> (na, None, type_app (lift i) t)) lna typarray in
+ Array.fold_left
+ (fun e assum -> g assum e) e ctxt
+
+
+let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
+ | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
+ | Construct _) -> c
+ | Cast (c,t) -> let c' = f l c in mkCast (c', f l t)
+ | Prod (na,t,c) ->
+ let t' = f l t in
+ mkProd (na, t', f (g (na,None,t) l) c)
+ | Lambda (na,t,c) ->
+ let t' = f l t in
+ mkLambda (na, t', f (g (na,None,t) l) c)
+ | LetIn (na,b,t,c) ->
+ let b' = f l b in
+ let t' = f l t in
+ let c' = f (g (na,Some b,t) l) c in
+ mkLetIn (na, b', t', c')
+ | App (c,[||]) -> assert false
+ | App (c,al) ->
+ (*Special treatment to be able to recognize partially applied subterms*)
+ let a = al.(Array.length al - 1) in
+ let hd = f l (mkApp (c, Array.sub al 0 (Array.length al - 1))) in
+ mkApp (hd, [| f l a |])
+ | Evar (e,al) -> mkEvar (e, array_map_left (f l) al)
+ | Case (ci,p,c,bl) ->
+ let p' = f l p in let c' = f l c in
+ mkCase (ci, p', c', array_map_left (f l) bl)
+ | Fix (ln,(lna,tl,bl as fx)) ->
+ let l' = fold_rec_types g fx l in
+ let (tl',bl') = array_map_left_pair (f l) tl (f l') bl in
+ mkFix (ln,(lna,tl',bl'))
+ | CoFix(ln,(lna,tl,bl as fx)) ->
+ let l' = fold_rec_types g fx l in
+ let (tl',bl') = array_map_left_pair (f l) tl (f l') bl in
+ mkCoFix (ln,(lna,tl',bl'))
+
+(* strong *)
+let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with
+ | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
+ | Construct _) -> cstr
+ | Cast (c,t) ->
+ let c' = f l c in
+ let t' = f l t in
+ if c==c' && t==t' then cstr else mkCast (c', t')
+ | Prod (na,t,c) ->
+ let t' = f l t in
+ let c' = f (g (na,None,t) l) c in
+ if t==t' && c==c' then cstr else mkProd (na, t', c')
+ | Lambda (na,t,c) ->
+ let t' = f l t in
+ let c' = f (g (na,None,t) l) c in
+ if t==t' && c==c' then cstr else mkLambda (na, t', c')
+ | LetIn (na,b,t,c) ->
+ let b' = f l b in
+ let t' = f l t in
+ let c' = f (g (na,Some b,t) l) c in
+ if b==b' && t==t' && c==c' then cstr else mkLetIn (na, b', t', c')
+ | App (c,al) ->
+ let c' = f l c in
+ let al' = Array.map (f l) al in
+ if c==c' && array_for_all2 (==) al al' then cstr else mkApp (c', al')
+ | Evar (e,al) ->
+ let al' = Array.map (f l) al in
+ if array_for_all2 (==) al al' then cstr else mkEvar (e, al')
+ | Case (ci,p,c,bl) ->
+ let p' = f l p in
+ let c' = f l c in
+ let bl' = Array.map (f l) bl in
+ if p==p' && c==c' && array_for_all2 (==) bl bl' then cstr else
+ mkCase (ci, p', c', bl')
+ | Fix (ln,(lna,tl,bl)) ->
+ let tl' = Array.map (f l) tl in
+ let l' =
+ array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
+ let bl' = Array.map (f l') bl in
+ if array_for_all2 (==) tl tl' && array_for_all2 (==) bl bl'
+ then cstr
+ else mkFix (ln,(lna,tl',bl'))
+ | CoFix(ln,(lna,tl,bl)) ->
+ let tl' = Array.map (f l) tl in
+ let l' =
+ array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
+ let bl' = Array.map (f l') bl in
+ if array_for_all2 (==) tl tl' && array_for_all2 (==) bl bl'
+ then cstr
+ else mkCoFix (ln,(lna,tl',bl'))
+
+(* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
+ subterms of [c] starting from [acc] and proceeding from left to
+ right according to the usual representation of the constructions as
+ [fold_constr] but it carries an extra data [n] (typically a lift
+ index) which is processed by [g] (which typically add 1 to [n]) at
+ each binder traversal; it is not recursive *)
+
+let fold_constr_with_binders g f n acc c = match kind_of_term c with
+ | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
+ | Construct _) -> acc
+ | Cast (c,t) -> f n (f n acc c) t
+ | Prod (_,t,c) -> f (g n) (f n acc t) c
+ | Lambda (_,t,c) -> f (g n) (f n acc t) c
+ | LetIn (_,b,t,c) -> f (g n) (f n (f n acc b) t) c
+ | App (c,l) -> Array.fold_left (f n) (f n acc c) l
+ | Evar (_,l) -> Array.fold_left (f n) acc l
+ | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
+ | Fix (_,(lna,tl,bl)) ->
+ let n' = iterate g (Array.length tl) n in
+ let fd = array_map2 (fun t b -> (t,b)) tl bl in
+ Array.fold_left (fun acc (t,b) -> f n (f n' acc t) b) acc fd
+ | CoFix (_,(lna,tl,bl)) ->
+ let n' = iterate g (Array.length tl) n in
+ let fd = array_map2 (fun t b -> (t,b)) tl bl in
+ Array.fold_left (fun acc (t,b) -> f n (f n' acc t) b) acc fd
+
+(* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate
+ subterms of [c]; it carries an extra data [acc] which is processed by [g] at
+ each binder traversal; it is not recursive and the order with which
+ subterms are processed is not specified *)
+
+let iter_constr_with_full_binders g f l c = match kind_of_term c with
+ | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
+ | Construct _) -> ()
+ | Cast (c,t) -> f l c; f l t
+ | Prod (na,t,c) -> f l t; f (g (na,None,t) l) c
+ | Lambda (na,t,c) -> f l t; f (g (na,None,t) l) c
+ | LetIn (na,b,t,c) -> f l b; f l t; f (g (na,Some b,t) l) c
+ | App (c,args) -> f l c; Array.iter (f l) args
+ | Evar (_,args) -> Array.iter (f l) args
+ | Case (_,p,c,bl) -> f l p; f l c; Array.iter (f l) bl
+ | Fix (_,(lna,tl,bl)) ->
+ let l' = array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
+ Array.iter (f l) tl;
+ Array.iter (f l') bl
+ | CoFix (_,(lna,tl,bl)) ->
+ let l' = array_fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
+ Array.iter (f l) tl;
+ Array.iter (f l') bl
+
+(***************************)
+(* occurs check functions *)
+(***************************)
+
+exception Occur
+
+let occur_meta c =
+ let rec occrec c = match kind_of_term c with
+ | Meta _ -> raise Occur
+ | _ -> iter_constr occrec c
+ in try occrec c; false with Occur -> true
+
+let occur_existential c =
+ let rec occrec c = match kind_of_term c with
+ | Evar _ -> raise Occur
+ | _ -> iter_constr occrec c
+ in try occrec c; false with Occur -> true
+
+let occur_const s c =
+ let rec occur_rec c = match kind_of_term c with
+ | Const sp when sp=s -> raise Occur
+ | _ -> iter_constr occur_rec c
+ in
+ try occur_rec c; false with Occur -> true
+
+let occur_evar n c =
+ let rec occur_rec c = match kind_of_term c with
+ | Evar (sp,_) when sp=n -> raise Occur
+ | _ -> iter_constr occur_rec c
+ in
+ try occur_rec c; false with Occur -> true
+
+let occur_in_global env id constr =
+ let vars = vars_of_global env constr in
+ if List.mem id vars then raise Occur
+
+let occur_var env s c =
+ let rec occur_rec c =
+ occur_in_global env s c;
+ iter_constr occur_rec c
+ in
+ try occur_rec c; false with Occur -> true
+
+let occur_var_in_decl env hyp (_,c,typ) =
+ match c with
+ | None -> occur_var env hyp typ
+ | Some body ->
+ occur_var env hyp typ ||
+ occur_var env hyp body
+
+(* Tests that t is a subterm of c *)
+let occur_term t c =
+ let eq_constr_fail c = if eq_constr t c then raise Occur
+ in let rec occur_rec c = eq_constr_fail c; iter_constr occur_rec c
+ in try occur_rec c; false with Occur -> true
+
+(* returns the list of free debruijn indices in a term *)
+
+let free_rels m =
+ let rec frec depth acc c = match kind_of_term c with
+ | Rel n -> if n >= depth then Intset.add (n-depth+1) acc else acc
+ | _ -> fold_constr_with_binders succ frec depth acc c
+ in
+ frec 1 Intset.empty m
+
+
+(* (dependent M N) is true iff M is eq_term with a subterm of N
+ M is appropriately lifted through abstractions of N *)
+
+let dependent m t =
+ let rec deprec m t =
+ if eq_constr m t then
+ raise Occur
+ else
+ match kind_of_term m, kind_of_term t with
+ | App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt ->
+ deprec m (mkApp (ft,Array.sub lt 0 (Array.length lm)));
+ Array.iter (deprec m)
+ (Array.sub lt
+ (Array.length lm) ((Array.length lt) - (Array.length lm)))
+ | _ -> iter_constr_with_binders (lift 1) deprec m t
+ in
+ try deprec m t; false with Occur -> true
+
+let pop t = lift (-1) t
+
+(***************************)
+(* bindings functions *)
+(***************************)
+
+type metamap = (metavariable * constr) list
+
+let rec subst_meta bl c =
+ match kind_of_term c with
+ | Meta i -> (try List.assoc i bl with Not_found -> c)
+ | _ -> map_constr (subst_meta bl) c
+
+(* First utilities for avoiding telescope computation for subst_term *)
+
+let prefix_application eq_fun (k,c) (t : constr) =
+ let c' = collapse_appl c and t' = collapse_appl t in
+ match kind_of_term c', kind_of_term t' with
+ | App (f1,cl1), App (f2,cl2) ->
+ let l1 = Array.length cl1
+ and l2 = Array.length cl2 in
+ if l1 <= l2
+ && eq_fun c' (mkApp (f2, Array.sub cl2 0 l1)) then
+ Some (mkApp (mkRel k, Array.sub cl2 l1 (l2 - l1)))
+ else
+ None
+ | _ -> None
+
+let my_prefix_application eq_fun (k,c) (by_c : constr) (t : constr) =
+ let c' = collapse_appl c and t' = collapse_appl t in
+ match kind_of_term c', kind_of_term t' with
+ | App (f1,cl1), App (f2,cl2) ->
+ let l1 = Array.length cl1
+ and l2 = Array.length cl2 in
+ if l1 <= l2
+ && eq_fun c' (mkApp (f2, Array.sub cl2 0 l1)) then
+ Some (mkApp ((lift k by_c), Array.sub cl2 l1 (l2 - l1)))
+ else
+ None
+ | _ -> None
+
+(* Recognizing occurrences of a given (closed) subterm in a term for Pattern :
+ [subst_term c t] substitutes [(Rel 1)] for all occurrences of (closed)
+ term [c] in a term [t] *)
+(*i Bizarre : si on cherche un sous terme clos, pourquoi le lifter ? i*)
+
+let subst_term_gen eq_fun c t =
+ let rec substrec (k,c as kc) t =
+ match prefix_application eq_fun kc t with
+ | Some x -> x
+ | None ->
+ if eq_fun c t then mkRel k
+ else
+ map_constr_with_binders (fun (k,c) -> (k+1,lift 1 c)) substrec kc t
+ in
+ substrec (1,c) t
+
+(* Recognizing occurrences of a given (closed) subterm in a term :
+ [replace_term c1 c2 t] substitutes [c2] for all occurrences of (closed)
+ term [c1] in a term [t] *)
+(*i Meme remarque : a priori [c] n'est pas forcement clos i*)
+
+let replace_term_gen eq_fun c by_c in_t =
+ let rec substrec (k,c as kc) t =
+ match my_prefix_application eq_fun kc by_c t with
+ | Some x -> x
+ | None ->
+ (if eq_fun c t then (lift k by_c) else
+ map_constr_with_binders (fun (k,c) -> (k+1,lift 1 c))
+ substrec kc t)
+ in
+ substrec (0,c) in_t
+
+let subst_term = subst_term_gen eq_constr
+
+let replace_term = replace_term_gen eq_constr
+
+(* Substitute only a list of locations locs, the empty list is
+ interpreted as substitute all, if 0 is in the list then no
+ bindings is done. The list may contain only negative occurrences
+ that will not be substituted. *)
+
+let subst_term_occ_gen locs occ c t =
+ let maxocc = List.fold_right max locs 0 in
+ let pos = ref occ in
+ let check = ref true in
+ let except = List.exists (fun n -> n<0) locs in
+ if except & (List.exists (fun n -> n>=0) locs)
+ then error "mixing of positive and negative occurences"
+ else
+ let rec substrec (k,c as kc) t =
+ if (not except) & (!pos > maxocc) then t
+ else
+ if eq_constr c t then
+ let r =
+ if except then
+ if List.mem (- !pos) locs then t else (mkRel k)
+ else
+ if List.mem !pos locs then (mkRel k) else t
+ in incr pos; r
+ else
+ map_constr_with_binders_left_to_right
+ (fun d (k,c) -> (k+1,lift 1 c))
+ substrec kc t
+ in
+ let t' = substrec (1,c) t in
+ (!pos, t')
+
+let subst_term_occ locs c t =
+ if locs = [] then subst_term c t
+ else if List.mem 0 locs then
+ t
+ else
+ let (nbocc,t') = subst_term_occ_gen locs 1 c t in
+ if List.exists (fun o -> o >= nbocc or o <= -nbocc) locs then
+ errorlabstrm "subst_term_occ" (str "Too few occurences");
+ t'
+
+let subst_term_occ_decl locs c (id,bodyopt,typ as d) =
+ match bodyopt with
+ | None -> (id,None,subst_term_occ locs c typ)
+ | Some body ->
+ if locs = [] then
+ (id,Some (subst_term c body),type_app (subst_term c) typ)
+ else if List.mem 0 locs then
+ d
+ else
+ let (nbocc,body') = subst_term_occ_gen locs 1 c body in
+ let (nbocc',t') = subst_term_occ_gen locs nbocc c typ in
+ if List.exists (fun o -> o >= nbocc' or o <= -nbocc') locs then
+ errorlabstrm "subst_term_occ_decl" (str "Too few occurences");
+ (id,Some body',t')
+
+
+(* First character of a constr *)
+
+let first_char id =
+ let id = string_of_id id in
+ assert (id <> "");
+ String.make 1 id.[0]
+
+let lowercase_first_char id = String.lowercase (first_char id)
+
+let vars_of_env env =
+ let s =
+ Sign.fold_named_context (fun (id,_,_) s -> Idset.add id s)
+ (named_context env) ~init:Idset.empty in
+ Sign.fold_rel_context
+ (fun (na,_,_) s -> match na with Name id -> Idset.add id s | _ -> s)
+ (rel_context env) ~init:s
+
+let add_vname vars = function
+ Name id -> Idset.add id vars
+ | _ -> vars
+
+let id_of_global = Nametab.id_of_global
+
+let sort_hdchar = function
+ | Prop(_) -> "P"
+ | Type(_) -> "T"
+
+let hdchar env c =
+ let rec hdrec k c =
+ match kind_of_term c with
+ | Prod (_,_,c) -> hdrec (k+1) c
+ | Lambda (_,_,c) -> hdrec (k+1) c
+ | LetIn (_,_,_,c) -> hdrec (k+1) c
+ | Cast (c,_) -> hdrec k c
+ | App (f,l) -> hdrec k f
+ | Const kn ->
+ let c = lowercase_first_char (id_of_label (label kn)) in
+ if c = "?" then "y" else c
+ | Ind ((kn,i) as x) ->
+ if i=0 then
+ lowercase_first_char (id_of_label (label kn))
+ else
+ lowercase_first_char (id_of_global (IndRef x))
+ | Construct ((sp,i) as x) ->
+ lowercase_first_char (id_of_global (ConstructRef x))
+ | Var id -> lowercase_first_char id
+ | Sort s -> sort_hdchar s
+ | Rel n ->
+ (if n<=k then "p" (* the initial term is flexible product/function *)
+ else
+ try match Environ.lookup_rel (n-k) env with
+ | (Name id,_,_) -> lowercase_first_char id
+ | (Anonymous,_,t) -> hdrec 0 (lift (n-k) t)
+ with Not_found -> "y")
+ | Fix ((_,i),(lna,_,_)) ->
+ let id = match lna.(i) with Name id -> id | _ -> assert false in
+ lowercase_first_char id
+ | CoFix (i,(lna,_,_)) ->
+ let id = match lna.(i) with Name id -> id | _ -> assert false in
+ lowercase_first_char id
+ | Meta _|Evar _|Case (_, _, _, _) -> "y"
+ in
+ hdrec 0 c
+
+let id_of_name_using_hdchar env a = function
+ | Anonymous -> id_of_string (hdchar env a)
+ | Name id -> id
+
+let named_hd env a = function
+ | Anonymous -> Name (id_of_string (hdchar env a))
+ | x -> x
+
+let named_hd_type env a = named_hd env (body_of_type a)
+
+let prod_name env (n,a,b) = mkProd (named_hd_type env a n, a, b)
+let lambda_name env (n,a,b) = mkLambda (named_hd_type env a n, a, b)
+
+let prod_create env (a,b) = mkProd (named_hd_type env a Anonymous, a, b)
+let lambda_create env (a,b) = mkLambda (named_hd_type env a Anonymous, a, b)
+
+let name_assumption env (na,c,t) =
+ match c with
+ | None -> (named_hd_type env t na, None, t)
+ | Some body -> (named_hd env body na, c, t)
+
+let name_context env hyps =
+ snd
+ (List.fold_left
+ (fun (env,hyps) d ->
+ let d' = name_assumption env d in (push_rel d' env, d' :: hyps))
+ (env,[]) (List.rev hyps))
+
+let mkProd_or_LetIn_name env b d = mkProd_or_LetIn (name_assumption env d) b
+let mkLambda_or_LetIn_name env b d = mkLambda_or_LetIn (name_assumption env d)b
+
+let it_mkProd_or_LetIn_name env b hyps =
+ it_mkProd_or_LetIn b (name_context env hyps)
+let it_mkLambda_or_LetIn_name env b hyps =
+ it_mkLambda_or_LetIn b (name_context env hyps)
+
+(*************************)
+(* Names environments *)
+(*************************)
+type names_context = name list
+let add_name n nl = n::nl
+let lookup_name_of_rel p names =
+ try List.nth names (p-1)
+ with Invalid_argument _ | Failure _ -> raise Not_found
+let rec lookup_rel_of_name id names =
+ let rec lookrec n = function
+ | Anonymous :: l -> lookrec (n+1) l
+ | (Name id') :: l -> if id' = id then n else lookrec (n+1) l
+ | [] -> raise Not_found
+ in
+ lookrec 1 names
+let empty_names_context = []
+
+let ids_of_rel_context sign =
+ Sign.fold_rel_context
+ (fun (na,_,_) l -> match na with Name id -> id::l | Anonymous -> l)
+ sign ~init:[]
+let ids_of_named_context sign =
+ Sign.fold_named_context (fun (id,_,_) idl -> id::idl) sign ~init:[]
+
+let ids_of_context env =
+ (ids_of_rel_context (rel_context env))
+ @ (ids_of_named_context (named_context env))
+
+let names_of_rel_context env =
+ List.map (fun (na,_,_) -> na) (rel_context env)
+
+(**** Globality of identifiers *)
+
+(* TODO temporary hack!!! *)
+let rec is_imported_modpath = function
+ | MPfile dp -> dp <> (Lib.library_dp ())
+(* | MPdot (mp,_) -> is_imported_modpath mp *)
+ | _ -> false
+
+let is_imported_ref = function
+ | VarRef _ -> false
+ | ConstRef kn
+ | IndRef (kn,_)
+ | ConstructRef ((kn,_),_)
+(* | ModTypeRef ln *) ->
+ let (mp,_,_) = repr_kn kn in is_imported_modpath mp
+(* | ModRef mp ->
+ is_imported_modpath mp
+*)
+
+let is_global id =
+ try
+ let ref = locate (make_short_qualid id) in
+ not (is_imported_ref ref)
+ with Not_found ->
+ false
+
+let is_section_variable id =
+ try let _ = Sign.lookup_named id (Global.named_context()) in true
+ with Not_found -> false
+
+let next_global_ident_from allow_secvar id avoid =
+ let rec next_rec id =
+ let id = next_ident_away_from id avoid in
+ if (allow_secvar && is_section_variable id) || not (is_global id) then
+ id
+ else
+ next_rec (lift_ident id)
+ in
+ next_rec id
+
+let next_global_ident_away allow_secvar id avoid =
+ let id = next_ident_away id avoid in
+ if (allow_secvar && is_section_variable id) || not (is_global id) then
+ id
+ else
+ next_global_ident_from allow_secvar (lift_ident id) avoid
+
+(* Nouvelle version de renommage des variables (DEC 98) *)
+(* This is the algorithm to display distinct bound variables
+
+ - Règle 1 : un nom non anonyme, même non affiché, contribue à la liste
+ des noms à éviter
+ - Règle 2 : c'est la dépendance qui décide si on affiche ou pas
+
+ Exemple :
+ si bool_ind = (P:bool->Prop)(f:(P true))(f:(P false))(b:bool)(P b), alors
+ il est affiché (P:bool->Prop)(P true)->(P false)->(b:bool)(P b)
+ mais f et f0 contribue à la liste des variables à éviter (en supposant
+ que les noms f et f0 ne sont pas déjà pris)
+ Intérêt : noms homogènes dans un but avant et après Intro
+*)
+
+type used_idents = identifier list
+
+let occur_rel p env id =
+ try lookup_name_of_rel p env = Name id
+ with Not_found -> false (* Unbound indice : may happen in debug *)
+
+let occur_id nenv id0 c =
+ let rec occur n c = match kind_of_term c with
+ | Var id when id=id0 -> raise Occur
+ | Const kn when id_of_global (ConstRef kn) = id0 -> raise Occur
+ | Ind ind_sp
+ when id_of_global (IndRef ind_sp) = id0 ->
+ raise Occur
+ | Construct cstr_sp
+ when id_of_global (ConstructRef cstr_sp) = id0 ->
+ raise Occur
+ | Rel p when p>n & occur_rel (p-n) nenv id0 -> raise Occur
+ | _ -> iter_constr_with_binders succ occur n c
+ in
+ try occur 1 c; false
+ with Occur -> true
+ | Not_found -> false (* Case when a global is not in the env *)
+
+let next_name_not_occuring is_goal_ccl name l env_names t =
+ let rec next id =
+ if List.mem id l or occur_id env_names id t or
+ (* To be consistent with intro mechanism *)
+ (is_goal_ccl & is_global id & not (is_section_variable id))
+ then next (lift_ident id)
+ else id
+ in
+ match name with
+ | Name id -> next id
+ | Anonymous ->
+ (* Normally, an anonymous name is not dependent and will not be *)
+ (* taken into account by the function concrete_name; just in case *)
+ (* invent a valid name *)
+ id_of_string "H"
+
+(* On reduit une serie d'eta-redex de tete ou rien du tout *)
+(* [x1:c1;...;xn:cn]@(f;a1...an;x1;...;xn) --> @(f;a1...an) *)
+(* Remplace 2 versions précédentes buggées *)
+
+let rec eta_reduce_head c =
+ match kind_of_term c with
+ | Lambda (_,c1,c') ->
+ (match kind_of_term (eta_reduce_head c') with
+ | App (f,cl) ->
+ let lastn = (Array.length cl) - 1 in
+ if lastn < 1 then anomaly "application without arguments"
+ else
+ (match kind_of_term cl.(lastn) with
+ | Rel 1 ->
+ let c' =
+ if lastn = 1 then f
+ else mkApp (f, Array.sub cl 0 lastn)
+ in
+ if noccurn 1 c'
+ then lift (-1) c'
+ else c
+ | _ -> c)
+ | _ -> c)
+ | _ -> c
+
+(* alpha-eta conversion : ignore print names and casts *)
+let eta_eq_constr =
+ let rec aux t1 t2 =
+ let t1 = eta_reduce_head (strip_head_cast t1)
+ and t2 = eta_reduce_head (strip_head_cast t2) in
+ t1=t2 or compare_constr aux t1 t2
+ in aux
+
+
+(* iterator on rel context *)
+let process_rel_context f env =
+ let sign = named_context env in
+ let rels = rel_context env in
+ let env0 = reset_with_named_context sign env in
+ Sign.fold_rel_context f rels ~init:env0
+
+let assums_of_rel_context sign =
+ Sign.fold_rel_context
+ (fun (na,c,t) l ->
+ match c with
+ Some _ -> l
+ | None -> (na, t)::l)
+ sign ~init:[]
+
+let lift_rel_context n sign =
+ let rec liftrec k = function
+ | (na,c,t)::sign ->
+ (na,option_app (liftn n k) c,type_app (liftn n k) t)
+ ::(liftrec (k-1) sign)
+ | [] -> []
+ in
+ liftrec (rel_context_length sign) sign
+
+let fold_named_context_both_sides f l ~init = list_fold_right_and_left f l init
+
+let rec mem_named_context id = function
+ | (id',_,_) :: _ when id=id' -> true
+ | _ :: sign -> mem_named_context id sign
+ | [] -> false
+
+let make_all_name_different env =
+ let avoid = ref (ids_of_named_context (named_context env)) in
+ process_rel_context
+ (fun (na,c,t) newenv ->
+ let id = next_name_away na !avoid in
+ avoid := id::!avoid;
+ push_rel (Name id,c,t) newenv)
+ env
+
+let global_vars env ids = Idset.elements (global_vars_set env ids)
+
+let global_vars_set_of_decl env = function
+ | (_,None,t) -> global_vars_set env t
+ | (_,Some c,t) ->
+ Idset.union (global_vars_set env t)
+ (global_vars_set env c)
+
+(* Remark: Anonymous var may be dependent in Evar's contexts *)
+let concrete_name is_goal_ccl l env_names n c =
+ if n = Anonymous & noccurn 1 c then
+ (Anonymous,l)
+ else
+ let fresh_id = next_name_not_occuring is_goal_ccl n l env_names c in
+ let idopt = if noccurn 1 c then Anonymous else Name fresh_id in
+ (idopt, fresh_id::l)
+
+let concrete_let_name is_goal_ccl l env_names n c =
+ let fresh_id = next_name_not_occuring is_goal_ccl n l env_names c in
+ (Name fresh_id, fresh_id::l)
+
+let rec rename_bound_var env l c =
+ match kind_of_term c with
+ | Prod (Name s,c1,c2) ->
+ if noccurn 1 c2 then
+ let env' = push_rel (Name s,None,c1) env in
+ mkProd (Name s, c1, rename_bound_var env' l c2)
+ else
+ let s' = next_ident_away s (global_vars env c2@l) in
+ let env' = push_rel (Name s',None,c1) env in
+ mkProd (Name s', c1, rename_bound_var env' (s'::l) c2)
+ | Prod (Anonymous,c1,c2) ->
+ let env' = push_rel (Anonymous,None,c1) env in
+ mkProd (Anonymous, c1, rename_bound_var env' l c2)
+ | Cast (c,t) -> mkCast (rename_bound_var env l c, t)
+ | x -> c
+
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-16 05:02:03 +0000