summaryrefslogtreecommitdiff
path: root/engine/termops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/termops.ml')
-rw-r--r--engine/termops.ml1069
1 files changed, 1069 insertions, 0 deletions
diff --git a/engine/termops.ml b/engine/termops.ml
new file mode 100644
index 00000000..697b9a5f
--- /dev/null
+++ b/engine/termops.ml
@@ -0,0 +1,1069 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Pp
+open CErrors
+open Util
+open Names
+open Nameops
+open Term
+open Vars
+open Environ
+
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
+(* Sorts and sort family *)
+
+let print_sort = function
+ | Prop Pos -> (str "Set")
+ | Prop Null -> (str "Prop")
+ | Type u -> (str "Type(" ++ Univ.Universe.pr u ++ str ")")
+
+let pr_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_con sp = str(string_of_con sp)
+
+let pr_fix pr_constr ((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":" ++ pr_constr ty ++
+ cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
+ str"}")
+
+let pr_puniverses p u =
+ if Univ.Instance.is_empty u then p
+ else p ++ str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)"
+
+let rec pr_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"(" ++ pr_constr c ++ cut() ++
+ str":" ++ pr_constr t ++ str")")
+ | Prod (Name(id),t,c) -> hov 1
+ (str"forall " ++ pr_id id ++ str":" ++ pr_constr t ++ str"," ++
+ spc() ++ pr_constr c)
+ | Prod (Anonymous,t,c) -> hov 0
+ (str"(" ++ pr_constr t ++ str " ->" ++ spc() ++
+ pr_constr c ++ str")")
+ | Lambda (na,t,c) -> hov 1
+ (str"fun " ++ pr_name na ++ str":" ++
+ pr_constr t ++ str" =>" ++ spc() ++ pr_constr c)
+ | LetIn (na,b,t,c) -> hov 0
+ (str"let " ++ pr_name na ++ str":=" ++ pr_constr b ++
+ str":" ++ brk(1,2) ++ pr_constr t ++ cut() ++
+ pr_constr c)
+ | App (c,l) -> hov 1
+ (str"(" ++ pr_constr c ++ spc() ++
+ prlist_with_sep spc pr_constr (Array.to_list l) ++ str")")
+ | Evar (e,l) -> hov 1
+ (str"Evar#" ++ int (Evar.repr e) ++ str"{" ++
+ prlist_with_sep spc pr_constr (Array.to_list l) ++str"}")
+ | Const (c,u) -> str"Cst(" ++ pr_puniverses (pr_con c) u ++ str")"
+ | Ind ((sp,i),u) -> str"Ind(" ++ pr_puniverses (pr_mind sp ++ str"," ++ int i) u ++ str")"
+ | Construct (((sp,i),j),u) ->
+ str"Constr(" ++ pr_puniverses (pr_mind sp ++ str"," ++ int i ++ str"," ++ int j) u ++ str")"
+ | Proj (p,c) -> str"Proj(" ++ pr_con (Projection.constant p) ++ str"," ++ bool (Projection.unfolded p) ++ pr_constr c ++ str")"
+ | Case (ci,p,c,bl) -> v 0
+ (hv 0 (str"<"++pr_constr p++str">"++ cut() ++ str"Case " ++
+ pr_constr c ++ str"of") ++ cut() ++
+ prlist_with_sep (fun _ -> brk(1,2)) pr_constr (Array.to_list bl) ++
+ cut() ++ str"end")
+ | Fix f -> pr_fix pr_constr f
+ | 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":" ++ pr_constr ty ++
+ cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
+ str"}")
+
+let term_printer = ref (fun _ -> pr_constr)
+let print_constr_env t = !term_printer t
+let print_constr t = !term_printer (Global.env()) t
+let set_print_constr f = term_printer := f
+
+let pr_var_decl env decl =
+ let open NamedDecl in
+ let pbody = match decl with
+ | LocalAssum _ -> mt ()
+ | LocalDef (_,c,_) ->
+ (* Force evaluation *)
+ let pb = print_constr_env env c in
+ (str" := " ++ pb ++ cut () ) in
+ let pt = print_constr_env env (get_type decl) in
+ let ptyp = (str" : " ++ pt) in
+ (pr_id (get_id decl) ++ hov 0 (pbody ++ ptyp))
+
+let pr_rel_decl env decl =
+ let open RelDecl in
+ let pbody = match decl with
+ | LocalAssum _ -> mt ()
+ | LocalDef (_,c,_) ->
+ (* Force evaluation *)
+ let pb = print_constr_env env c in
+ (str":=" ++ spc () ++ pb ++ spc ()) in
+ let ptyp = print_constr_env env (get_type decl) in
+ match get_name decl with
+ | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
+ | Name id -> hov 0 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
+
+let print_named_context env =
+ hv 0 (fold_named_context
+ (fun env d pps ->
+ pps ++ ws 2 ++ pr_var_decl env d)
+ env ~init:(mt ()))
+
+let print_rel_context env =
+ hv 0 (fold_rel_context
+ (fun env d pps -> pps ++ ws 2 ++ pr_rel_decl env d)
+ env ~init:(mt ()))
+
+let print_env env =
+ let sign_env =
+ fold_named_context
+ (fun env d pps ->
+ let pidt = pr_var_decl env d in
+ (pps ++ fnl () ++ pidt))
+ env ~init:(mt ())
+ in
+ let db_env =
+ fold_rel_context
+ (fun env d pps ->
+ let pnat = pr_rel_decl env d in (pps ++ fnl () ++ pnat))
+ env ~init:(mt ())
+ in
+ (sign_env ++ db_env)
+
+(* [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
+
+let push_rel_assum (x,t) env =
+ let open RelDecl in
+ push_rel (LocalAssum (x,t)) env
+
+let push_rels_assum assums =
+ let open RelDecl in
+ push_rel_context (List.map (fun (x,t) -> LocalAssum (x,t)) assums)
+
+let push_named_rec_types (lna,typarray,_) env =
+ let open NamedDecl in
+ let ctxt =
+ Array.map2_i
+ (fun i na t ->
+ match na with
+ | Name id -> LocalAssum (id, lift i t)
+ | Anonymous -> anomaly (Pp.str "Fix declarations must be named"))
+ lna typarray in
+ Array.fold_left
+ (fun e assum -> push_named assum e) env ctxt
+
+let lookup_rel_id id sign =
+ let open RelDecl in
+ let rec lookrec n = function
+ | [] ->
+ raise Not_found
+ | (LocalAssum (Anonymous, _) | LocalDef (Anonymous,_,_)) :: l ->
+ lookrec (n + 1) l
+ | LocalAssum (Name id', t) :: l ->
+ if Names.Id.equal id' id then (n,None,t) else lookrec (n + 1) l
+ | LocalDef (Name id', b, t) :: l ->
+ if Names.Id.equal id' id then (n,Some b,t) else lookrec (n + 1) l
+ in
+ lookrec 1 sign
+
+(* Constructs either [forall x:t, c] or [let x:=b:t in c] *)
+let mkProd_or_LetIn decl c =
+ let open RelDecl in
+ match decl with
+ | LocalAssum (na,t) -> mkProd (na, t, c)
+ | LocalDef (na,b,t) -> mkLetIn (na, b, t, c)
+
+(* Constructs either [forall x:t, c] or [c] in which [x] is replaced by [b] *)
+let mkProd_wo_LetIn decl c =
+ let open RelDecl in
+ match decl with
+ | LocalAssum (na,t) -> mkProd (na, t, c)
+ | LocalDef (_,b,_) -> subst1 b c
+
+let it_mkProd init = List.fold_left (fun c (n,t) -> mkProd (n, t, c)) init
+let it_mkLambda init = List.fold_left (fun c (n,t) -> mkLambda (n, t, c)) init
+
+let it_named_context_quantifier f ~init =
+ List.fold_left (fun c d -> f d c) init
+
+let it_mkProd_or_LetIn init = it_named_context_quantifier mkProd_or_LetIn ~init
+let it_mkProd_wo_LetIn init = it_named_context_quantifier mkProd_wo_LetIn ~init
+let it_mkLambda_or_LetIn init = it_named_context_quantifier mkLambda_or_LetIn ~init
+let it_mkNamedProd_or_LetIn init = it_named_context_quantifier mkNamedProd_or_LetIn ~init
+let it_mkNamedProd_wo_LetIn init = it_named_context_quantifier mkNamedProd_wo_LetIn ~init
+let it_mkNamedLambda_or_LetIn init = it_named_context_quantifier mkNamedLambda_or_LetIn ~init
+
+let it_mkLambda_or_LetIn_from_no_LetIn c decls =
+ let open RelDecl in
+ let rec aux k decls c = match decls with
+ | [] -> c
+ | LocalDef (na,b,t) :: decls -> mkLetIn (na,b,t,aux (k-1) decls (liftn 1 k c))
+ | LocalAssum (na,t) :: decls -> mkLambda (na,t,aux (k-1) decls c)
+ in aux (List.length decls) (List.rev decls) c
+
+(* *)
+
+(* 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 Int.equal (Array.length cl2) 0 then f else mkApp (f,cl2)
+ in
+ collapse_rec f cl
+ | Cast (c,_,_) -> strip_head_cast c
+ | _ -> c
+
+let rec drop_extra_implicit_args c = match kind_of_term c with
+ (* Removed trailing extra implicit arguments, what improves compatibility
+ for constants with recently added maximal implicit arguments *)
+ | App (f,args) when isEvar (Array.last args) ->
+ drop_extra_implicit_args
+ (mkApp (f,fst (Array.chop (Array.length args - 1) args)))
+ | _ -> c
+
+(* Get the last arg of an application *)
+let last_arg c = match kind_of_term c with
+ | App (f,cl) -> Array.last cl
+ | _ -> anomaly (Pp.str "last_arg")
+
+(* Get the last arg of an application *)
+let decompose_app_vect c =
+ match kind_of_term c with
+ | App (f,cl) -> (f, cl)
+ | _ -> (c,[||])
+
+let adjust_app_list_size f1 l1 f2 l2 =
+ let len1 = List.length l1 and len2 = List.length l2 in
+ if Int.equal len1 len2 then (f1,l1,f2,l2)
+ else if len1 < len2 then
+ let extras,restl2 = List.chop (len2-len1) l2 in
+ (f1, l1, applist (f2,extras), restl2)
+ else
+ let extras,restl1 = List.chop (len1-len2) l1 in
+ (applist (f1,extras), restl1, f2, l2)
+
+let adjust_app_array_size f1 l1 f2 l2 =
+ let len1 = Array.length l1 and len2 = Array.length l2 in
+ if Int.equal len1 len2 then (f1,l1,f2,l2)
+ else if len1 < len2 then
+ let extras,restl2 = Array.chop (len2-len1) l2 in
+ (f1, l1, appvect (f2,extras), restl2)
+ else
+ let extras,restl1 = Array.chop (len1-len2) l1 in
+ (appvect (f1,extras), restl1, f2, l2)
+
+(* [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,k,t) -> mkCast (f l c, k, 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)
+ | Proj (p,c) -> mkProj (p, f l c)
+ | 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 -> RelDecl.LocalAssum (na, lift i t)) lna typarray in
+ Array.fold_left (fun e assum -> g assum e) e ctxt
+
+let map_left2 f a g b =
+ let l = Array.length a in
+ if Int.equal l 0 then [||], [||] else begin
+ let r = Array.make l (f a.(0)) in
+ let s = Array.make l (g b.(0)) in
+ for i = 1 to l - 1 do
+ r.(i) <- f a.(i);
+ s.(i) <- g b.(i)
+ done;
+ r, s
+ end
+
+let map_constr_with_binders_left_to_right g f l c =
+ let open RelDecl in
+ match kind_of_term c with
+ | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
+ | Construct _) -> c
+ | Cast (b,k,t) ->
+ let b' = f l b in
+ let t' = f l t in
+ if b' == b && t' == t then c
+ else mkCast (b',k,t')
+ | Prod (na,t,b) ->
+ let t' = f l t in
+ let b' = f (g (LocalAssum (na,t)) l) b in
+ if t' == t && b' == b then c
+ else mkProd (na, t', b')
+ | Lambda (na,t,b) ->
+ let t' = f l t in
+ let b' = f (g (LocalAssum (na,t)) l) b in
+ if t' == t && b' == b then c
+ else mkLambda (na, t', b')
+ | LetIn (na,bo,t,b) ->
+ let bo' = f l bo in
+ let t' = f l t in
+ let b' = f (g (LocalDef (na,bo,t)) l) b in
+ if bo' == bo && t' == t && b' == b then c
+ else mkLetIn (na, bo', t', b')
+ | App (c,[||]) -> assert false
+ | App (t,al) ->
+ (*Special treatment to be able to recognize partially applied subterms*)
+ let a = al.(Array.length al - 1) in
+ let app = (mkApp (t, Array.sub al 0 (Array.length al - 1))) in
+ let app' = f l app in
+ let a' = f l a in
+ if app' == app && a' == a then c
+ else mkApp (app', [| a' |])
+ | Proj (p,b) ->
+ let b' = f l b in
+ if b' == b then c
+ else mkProj (p, b')
+ | Evar (e,al) ->
+ let al' = Array.map_left (f l) al in
+ if Array.for_all2 (==) al' al then c
+ else mkEvar (e, al')
+ | Case (ci,p,b,bl) ->
+ (* In v8 concrete syntax, predicate is after the term to match! *)
+ let b' = f l b in
+ let p' = f l p in
+ let bl' = Array.map_left (f l) bl in
+ if b' == b && p' == p && bl' == bl then c
+ else mkCase (ci, p', b', bl')
+ | Fix (ln,(lna,tl,bl as fx)) ->
+ let l' = fold_rec_types g fx l in
+ let (tl', bl') = map_left2 (f l) tl (f l') bl in
+ if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
+ then c
+ else mkFix (ln,(lna,tl',bl'))
+ | CoFix(ln,(lna,tl,bl as fx)) ->
+ let l' = fold_rec_types g fx l in
+ let (tl', bl') = map_left2 (f l) tl (f l') bl in
+ if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
+ then c
+ else mkCoFix (ln,(lna,tl',bl'))
+
+(* strong *)
+let map_constr_with_full_binders g f l cstr =
+ let open RelDecl in
+ match kind_of_term cstr with
+ | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
+ | Construct _) -> cstr
+ | Cast (c,k, t) ->
+ let c' = f l c in
+ let t' = f l t in
+ if c==c' && t==t' then cstr else mkCast (c', k, t')
+ | Prod (na,t,c) ->
+ let t' = f l t in
+ let c' = f (g (LocalAssum (na,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 (LocalAssum (na,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 (LocalDef (na,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')
+ | Proj (p,c) ->
+ let c' = f l c in
+ if c' == c then cstr else mkProj (p, c')
+ | 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 (LocalAssum (na,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 (LocalAssum (na,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_full_binders g f n acc c =
+ let open RelDecl in
+ 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 (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
+ | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
+ | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c
+ | App (c,l) -> Array.fold_left (f n) (f n acc c) l
+ | Proj (p,c) -> f n acc c
+ | 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' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl 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' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl 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
+
+let fold_constr_with_binders g f n acc c =
+ fold_constr_with_full_binders (fun _ x -> g x) f n acc c
+
+(* [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 =
+ let open RelDecl in
+ 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 (LocalAssum (na,t)) l) c
+ | Lambda (na,t,c) -> f l t; f (g (LocalAssum (na,t)) l) c
+ | LetIn (na,b,t,c) -> f l b; f l t; f (g (LocalDef (na,b,t)) l) c
+ | App (c,args) -> f l c; Array.iter (f l) args
+ | Proj (p,c) -> f l c
+ | 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 (LocalAssum (na,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 (LocalAssum (na,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_meta_or_existential c =
+ let rec occrec c = match kind_of_term c with
+ | Evar _ -> raise Occur
+ | Meta _ -> raise Occur
+ | _ -> iter_constr occrec c
+ in try occrec c; false with Occur -> true
+
+let occur_evar n c =
+ let rec occur_rec c = match kind_of_term c with
+ | Evar (sp,_) when Evar.equal 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 Id.Set.mem id vars then raise Occur
+
+let occur_var env id c =
+ let rec occur_rec c =
+ match kind_of_term c with
+ | Var _ | Const _ | Ind _ | Construct _ -> occur_in_global env id c
+ | _ -> iter_constr occur_rec c
+ in
+ try occur_rec c; false with Occur -> true
+
+let occur_var_in_decl env hyp decl =
+ let open NamedDecl in
+ match decl with
+ | LocalAssum (_,typ) -> occur_var env hyp typ
+ | LocalDef (_, body, typ) ->
+ occur_var env hyp typ ||
+ occur_var env hyp body
+
+let local_occur_var id c =
+ let rec occur c = match kind_of_term c with
+ | Var id' -> if Id.equal id id' then raise Occur
+ | _ -> Constr.iter occur c
+ in
+ try occur 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 Int.Set.add (n-depth+1) acc else acc
+ | _ -> fold_constr_with_binders succ frec depth acc c
+ in
+ frec 1 Int.Set.empty m
+
+(* collects all metavar occurrences, in left-to-right order, preserving
+ * repetitions and all. *)
+
+let collect_metas c =
+ let rec collrec acc c =
+ match kind_of_term c with
+ | Meta mv -> List.add_set Int.equal mv acc
+ | _ -> fold_constr collrec acc c
+ in
+ List.rev (collrec [] c)
+
+(* collects all vars; warning: this is only visible vars, not dependencies in
+ all section variables; for the latter, use global_vars_set *)
+let collect_vars c =
+ let rec aux vars c = match kind_of_term c with
+ | Var id -> Id.Set.add id vars
+ | _ -> fold_constr aux vars c in
+ aux Id.Set.empty c
+
+let vars_of_global_reference env gr =
+ let c, _ = Universes.unsafe_constr_of_global gr in
+ vars_of_global (Global.env ()) c
+
+(* Tests whether [m] is a subterm of [t]:
+ [m] is appropriately lifted through abstractions of [t] *)
+
+let dependent_main noevar univs m t =
+ let eqc x y = if univs then fst (Universes.eq_constr_universes x y) else eq_constr_nounivs x y in
+ let rec deprec m t =
+ if eqc 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)));
+ CArray.Fun1.iter deprec m
+ (Array.sub lt
+ (Array.length lm) ((Array.length lt) - (Array.length lm)))
+ | _, Cast (c,_,_) when noevar && isMeta c -> ()
+ | _, Evar _ when noevar -> ()
+ | _ -> iter_constr_with_binders (fun c -> lift 1 c) deprec m t
+ in
+ try deprec m t; false with Occur -> true
+
+let dependent = dependent_main false false
+let dependent_no_evar = dependent_main true false
+
+let dependent_univs = dependent_main false true
+let dependent_univs_no_evar = dependent_main true true
+
+let dependent_in_decl a decl =
+ let open NamedDecl in
+ match decl with
+ | LocalAssum (_,t) -> dependent a t
+ | LocalDef (_, body, t) -> dependent a body || dependent a t
+
+let count_occurrences m t =
+ let n = ref 0 in
+ let rec countrec m t =
+ if eq_constr m t then
+ incr n
+ else
+ match kind_of_term m, kind_of_term t with
+ | App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt ->
+ countrec m (mkApp (ft,Array.sub lt 0 (Array.length lm)));
+ Array.iter (countrec m)
+ (Array.sub lt
+ (Array.length lm) ((Array.length lt) - (Array.length lm)))
+ | _, Cast (c,_,_) when isMeta c -> ()
+ | _, Evar _ -> ()
+ | _ -> iter_constr_with_binders (lift 1) countrec m t
+ in
+ countrec m t;
+ !n
+
+(* Synonymous *)
+let occur_term = dependent
+
+let pop t = lift (-1) t
+
+(***************************)
+(* bindings functions *)
+(***************************)
+
+type meta_type_map = (metavariable * types) list
+
+type meta_value_map = (metavariable * constr) list
+
+let rec subst_meta bl c =
+ match kind_of_term c with
+ | Meta i -> (try Int.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 subterm in a term: [subst_term c t]
+ substitutes [(Rel 1)] for all occurrences of term [c] in a term [t];
+ works if [c] has rels *)
+
+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
+
+let subst_term = subst_term_gen eq_constr
+
+(* Recognizing occurrences of a given subterm in a term :
+ [replace_term c1 c2 t] substitutes [c2] for all occurrences of
+ term [c1] in a term [t]; works if [c1] and [c2] have rels *)
+
+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 replace_term = replace_term_gen eq_constr
+
+let vars_of_env env =
+ let s =
+ Context.Named.fold_outside (fun decl s -> Id.Set.add (NamedDecl.get_id decl) s)
+ (named_context env) ~init:Id.Set.empty in
+ Context.Rel.fold_outside
+ (fun decl s -> match RelDecl.get_name decl with Name id -> Id.Set.add id s | _ -> s)
+ (rel_context env) ~init:s
+
+let add_vname vars = function
+ Name id -> Id.Set.add id vars
+ | _ -> vars
+
+(*************************)
+(* Names environments *)
+(*************************)
+type names_context = Name.t 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 lookup_rel_of_name id names =
+ let rec lookrec n = function
+ | Anonymous :: l -> lookrec (n+1) l
+ | (Name id') :: l -> if Id.equal 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 =
+ Context.Rel.fold_outside
+ (fun decl l -> match RelDecl.get_name decl with Name id -> id::l | Anonymous -> l)
+ sign ~init:[]
+
+let ids_of_named_context sign =
+ Context.Named.fold_outside (fun decl idl -> NamedDecl.get_id decl :: 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 RelDecl.get_name (rel_context env)
+
+let is_section_variable id =
+ try let _ = Global.lookup_named id in true
+ with Not_found -> false
+
+let isGlobalRef c =
+ match kind_of_term c with
+ | Const _ | Ind _ | Construct _ | Var _ -> true
+ | _ -> false
+
+let is_template_polymorphic env f =
+ match kind_of_term f with
+ | Ind ind -> Environ.template_polymorphic_pind ind env
+ | Const c -> Environ.template_polymorphic_pconstant c env
+ | _ -> false
+
+let base_sort_cmp pb s0 s1 =
+ match (s0,s1) with
+ | (Prop c1, Prop c2) -> c1 == Null || c2 == Pos (* Prop <= Set *)
+ | (Prop c1, Type u) -> pb == Reduction.CUMUL
+ | (Type u1, Type u2) -> true
+ | _ -> false
+
+(* eq_constr extended with universe erasure *)
+let compare_constr_univ f cv_pb t1 t2 =
+ match kind_of_term t1, kind_of_term t2 with
+ Sort s1, Sort s2 -> base_sort_cmp cv_pb s1 s2
+ | Prod (_,t1,c1), Prod (_,t2,c2) ->
+ f Reduction.CONV t1 t2 && f cv_pb c1 c2
+ | _ -> compare_constr (fun t1 t2 -> f Reduction.CONV t1 t2) t1 t2
+
+let rec constr_cmp cv_pb t1 t2 = compare_constr_univ constr_cmp cv_pb t1 t2
+
+let eq_constr t1 t2 = constr_cmp Reduction.CONV t1 t2
+
+(* App(c,[t1,...tn]) -> ([c,t1,...,tn-1],tn)
+ App(c,[||]) -> ([],c) *)
+let split_app c = match kind_of_term c with
+ App(c,l) ->
+ let len = Array.length l in
+ if Int.equal len 0 then ([],c) else
+ let last = Array.get l (len-1) in
+ let prev = Array.sub l 0 (len-1) in
+ c::(Array.to_list prev), last
+ | _ -> assert false
+
+type subst = (Context.Rel.t * constr) Evar.Map.t
+
+exception CannotFilter
+
+let filtering env cv_pb c1 c2 =
+ let evm = ref Evar.Map.empty in
+ let define cv_pb e1 ev c1 =
+ try let (e2,c2) = Evar.Map.find ev !evm in
+ let shift = List.length e1 - List.length e2 in
+ if constr_cmp cv_pb c1 (lift shift c2) then () else raise CannotFilter
+ with Not_found ->
+ evm := Evar.Map.add ev (e1,c1) !evm
+ in
+ let rec aux env cv_pb c1 c2 =
+ match kind_of_term c1, kind_of_term c2 with
+ | App _, App _ ->
+ let ((p1,l1),(p2,l2)) = (split_app c1),(split_app c2) in
+ let () = aux env cv_pb l1 l2 in
+ begin match p1, p2 with
+ | [], [] -> ()
+ | (h1 :: p1), (h2 :: p2) ->
+ aux env cv_pb (applistc h1 p1) (applistc h2 p2)
+ | _ -> assert false
+ end
+ | Prod (n,t1,c1), Prod (_,t2,c2) ->
+ aux env cv_pb t1 t2;
+ aux (RelDecl.LocalAssum (n,t1) :: env) cv_pb c1 c2
+ | _, Evar (ev,_) -> define cv_pb env ev c1
+ | Evar (ev,_), _ -> define cv_pb env ev c2
+ | _ ->
+ if compare_constr_univ
+ (fun pb c1 c2 -> aux env pb c1 c2; true) cv_pb c1 c2 then ()
+ else raise CannotFilter
+ (* TODO: le reste des binders *)
+ in
+ aux env cv_pb c1 c2; !evm
+
+let decompose_prod_letin : constr -> int * Context.Rel.t * constr =
+ let rec prodec_rec i l c = match kind_of_term c with
+ | Prod (n,t,c) -> prodec_rec (succ i) (RelDecl.LocalAssum (n,t)::l) c
+ | LetIn (n,d,t,c) -> prodec_rec (succ i) (RelDecl.LocalDef (n,d,t)::l) c
+ | Cast (c,_,_) -> prodec_rec i l c
+ | _ -> i,l,c in
+ prodec_rec 0 []
+
+(* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction
+ * gives n (casts are ignored) *)
+let nb_lam =
+ let rec nbrec n c = match kind_of_term c with
+ | Lambda (_,_,c) -> nbrec (n+1) c
+ | Cast (c,_,_) -> nbrec n c
+ | _ -> n
+ in
+ nbrec 0
+
+(* similar to nb_lam, but gives the number of products instead *)
+let nb_prod =
+ let rec nbrec n c = match kind_of_term c with
+ | Prod (_,_,c) -> nbrec (n+1) c
+ | Cast (c,_,_) -> nbrec n c
+ | _ -> n
+ in
+ nbrec 0
+
+let nb_prod_modulo_zeta x =
+ let rec count n c =
+ match kind_of_term c with
+ Prod(_,_,t) -> count (n+1) t
+ | LetIn(_,a,_,t) -> count n (subst1 a t)
+ | Cast(c,_,_) -> count n c
+ | _ -> n
+ in count 0 x
+
+let align_prod_letin c a : Context.Rel.t * constr =
+ let (lc,_,_) = decompose_prod_letin c in
+ let (la,l,a) = decompose_prod_letin a in
+ if not (la >= lc) then invalid_arg "align_prod_letin";
+ let (l1,l2) = Util.List.chop lc l in
+ l2,it_mkProd_or_LetIn a l1
+
+(* We reduce a series of head eta-redex or nothing at all *)
+(* [x1:c1;...;xn:cn]@(f;a1...an;x1;...;xn) --> @(f;a1...an) *)
+(* Remplace 2 earlier buggish versions *)
+
+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 < 0 then anomaly (Pp.str "application without arguments")
+ else
+ (match kind_of_term cl.(lastn) with
+ | Rel 1 ->
+ let c' =
+ if Int.equal lastn 0 then f
+ else mkApp (f, Array.sub cl 0 lastn)
+ in
+ if noccurn 1 c'
+ then lift (-1) c'
+ else c
+ | _ -> c)
+ | _ -> c)
+ | _ -> c
+
+
+(* iterator on rel context *)
+let process_rel_context f env =
+ let sign = named_context_val env in
+ let rels = rel_context env in
+ let env0 = reset_with_named_context sign env in
+ Context.Rel.fold_outside f rels ~init:env0
+
+let assums_of_rel_context sign =
+ Context.Rel.fold_outside
+ (fun decl l ->
+ match decl with
+ | RelDecl.LocalDef _ -> l
+ | RelDecl.LocalAssum (na,t) -> (na, t)::l)
+ sign ~init:[]
+
+let map_rel_context_in_env f env sign =
+ let rec aux env acc = function
+ | d::sign ->
+ aux (push_rel d env) (RelDecl.map_constr (f env) d :: acc) sign
+ | [] ->
+ acc
+ in
+ aux env [] (List.rev sign)
+
+let map_rel_context_with_binders f sign =
+ let rec aux k = function
+ | d::sign -> RelDecl.map_constr (f k) d :: aux (k-1) sign
+ | [] -> []
+ in
+ aux (Context.Rel.length sign) sign
+
+let substl_rel_context l =
+ map_rel_context_with_binders (fun k -> substnl l (k-1))
+
+let lift_rel_context n =
+ map_rel_context_with_binders (liftn n)
+
+let smash_rel_context sign =
+ let rec aux acc = function
+ | [] -> acc
+ | (RelDecl.LocalAssum _ as d) :: l -> aux (d::acc) l
+ | RelDecl.LocalDef (_,b,_) :: l ->
+ (* Quadratic in the number of let but there are probably a few of them *)
+ aux (List.rev (substl_rel_context [b] (List.rev acc))) l
+ in List.rev (aux [] sign)
+
+let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init
+
+let mem_named_context_val id ctxt =
+ try ignore(Environ.lookup_named_val id ctxt); true with Not_found -> false
+
+let compact_named_context_reverse sign =
+ let compact l decl =
+ let (i1,c1,t1) = NamedDecl.to_tuple decl in
+ match l with
+ | [] -> [[i1],c1,t1]
+ | (l2,c2,t2)::q ->
+ if Option.equal Constr.equal c1 c2 && Constr.equal t1 t2
+ then (i1::l2,c2,t2)::q
+ else ([i1],c1,t1)::l
+ in Context.Named.fold_inside compact ~init:[] sign
+
+let compact_named_context sign = List.rev (compact_named_context_reverse sign)
+
+let clear_named_body id env =
+ let open NamedDecl in
+ let aux _ = function
+ | LocalDef (id',c,t) when Id.equal id id' -> push_named (LocalAssum (id,t))
+ | d -> push_named d in
+ fold_named_context aux env ~init:(reset_context env)
+
+let global_vars env ids = Id.Set.elements (global_vars_set env ids)
+
+let global_vars_set_of_decl env = function
+ | NamedDecl.LocalAssum (_,t) -> global_vars_set env t
+ | NamedDecl.LocalDef (_,c,t) ->
+ Id.Set.union (global_vars_set env t)
+ (global_vars_set env c)
+
+let dependency_closure env sign hyps =
+ if Id.Set.is_empty hyps then [] else
+ let (_,lh) =
+ Context.Named.fold_inside
+ (fun (hs,hl) d ->
+ let x = NamedDecl.get_id d in
+ if Id.Set.mem x hs then
+ (Id.Set.union (global_vars_set_of_decl env d) (Id.Set.remove x hs),
+ x::hl)
+ else (hs,hl))
+ ~init:(hyps,[])
+ sign in
+ List.rev lh
+
+(* Combinators on judgments *)
+
+let on_judgment f j = { uj_val = f j.uj_val; uj_type = f j.uj_type }
+let on_judgment_value f j = { j with uj_val = f j.uj_val }
+let on_judgment_type f j = { j with uj_type = f j.uj_type }
+
+(* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k non let-in
+ variables skips let-in's; let-in's in the middle are put in ctx2 *)
+let context_chop k ctx =
+ let rec chop_aux acc = function
+ | (0, l2) -> (List.rev acc, l2)
+ | (n, (RelDecl.LocalDef _ as h)::t) -> chop_aux (h::acc) (n, t)
+ | (n, (h::t)) -> chop_aux (h::acc) (pred n, t)
+ | (_, []) -> anomaly (Pp.str "context_chop")
+ in chop_aux [] (k,ctx)
+
+(* Do not skip let-in's *)
+let env_rel_context_chop k env =
+ let rels = rel_context env in
+ let ctx1,ctx2 = List.chop k rels in
+ push_rel_context ctx2 (reset_with_named_context (named_context_val env) env),
+ ctx1
+
+(*******************************************)
+(* Functions to deal with impossible cases *)
+(*******************************************)
+let impossible_default_case = ref None
+
+let set_impossible_default_clause c = impossible_default_case := Some c
+
+let coq_unit_judge =
+ let na1 = Name (Id.of_string "A") in
+ let na2 = Name (Id.of_string "H") in
+ fun () ->
+ match !impossible_default_case with
+ | Some fn ->
+ let (id,type_of_id), ctx = fn () in
+ make_judge id type_of_id, ctx
+ | None ->
+ (* In case the constants id/ID are not defined *)
+ make_judge (mkLambda (na1,mkProp,mkLambda(na2,mkRel 1,mkRel 1)))
+ (mkProd (na1,mkProp,mkArrow (mkRel 1) (mkRel 2))),
+ Univ.ContextSet.empty
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 04:10:59 +0000