diff options
Diffstat (limited to 'pretyping/termops.ml')
| -rw-r--r-- | pretyping/termops.ml | 554 |
1 files changed, 222 insertions, 332 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 02661a93..5862a852 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -1,27 +1,28 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Pp +open Errors open Util open Names open Nameops open Term -open Sign +open Vars +open Context open Environ -open Libnames -open Nametab +open Locus (* 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 ")") + | Type u -> (str "Type(" ++ Univ.Universe.pr u ++ str ")") let pr_sort_family = function | InSet -> (str "Set") @@ -34,6 +35,19 @@ let pr_name = function 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 ")" @@ -59,25 +73,19 @@ let rec pr_constr c = match kind_of_term c with (str"(" ++ pr_constr c ++ spc() ++ prlist_with_sep spc pr_constr (Array.to_list l) ++ str")") | Evar (e,l) -> hov 1 - (str"Evar#" ++ int e ++ str"{" ++ + (str"Evar#" ++ int (Evar.repr e) ++ str"{" ++ prlist_with_sep spc pr_constr (Array.to_list l) ++str"}") - | Const c -> str"Cst(" ++ pr_con c ++ str")" - | Ind (sp,i) -> str"Ind(" ++ pr_mind sp ++ str"," ++ int i ++ str")" - | Construct ((sp,i),j) -> - str"Constr(" ++ pr_mind sp ++ str"," ++ int i ++ str"," ++ int j ++ 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 ((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"}") + | 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 @@ -142,43 +150,6 @@ let print_env env = in (sign_env ++ db_env) -(*let current_module = ref empty_dirpath - -let set_module m = current_module := m*) - -let new_univ_level = - let univ_gen = ref 0 in - (fun sp -> - incr univ_gen; - Univ.make_universe_level (Lib.library_dp(),!univ_gen)) - -let new_univ () = Univ.make_universe (new_univ_level ()) -let new_Type () = mkType (new_univ ()) -let new_Type_sort () = Type (new_univ ()) - -(* This refreshes universes in types; works only for inferred types (i.e. for - types of the form (x1:A1)...(xn:An)B with B a sort or an atom in - head normal form) *) -let refresh_universes_gen strict t = - let modified = ref false in - let rec refresh t = match kind_of_term t with - | Sort (Type u) when strict or u <> Univ.type0m_univ -> - modified := true; new_Type () - | Prod (na,u,v) -> mkProd (na,u,refresh v) - | _ -> t in - let t' = refresh t in - if !modified then t' else t - -let refresh_universes = refresh_universes_gen false -let refresh_universes_strict = refresh_universes_gen true - -let new_sort_in_family = function - | InProp -> prop_sort - | InSet -> set_sort - | InType -> Type (new_univ ()) - - - (* [Rel (n+m);...;Rel(n+1)] *) let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) @@ -208,22 +179,23 @@ let push_rels_assum assums = let push_named_rec_types (lna,typarray,_) env = let ctxt = - array_map2_i + Array.map2_i (fun i na t -> match na with | Name id -> (id, None, lift i t) - | Anonymous -> anomaly "Fix declarations must be named") + | 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 rec lookup_rel_id id sign = - let rec lookrec = function - | (n, (Anonymous,_,_)::l) -> lookrec (n+1,l) - | (n, (Name id',b,t)::l) -> if id' = id then (n,b,t) else lookrec (n+1,l) - | (_, []) -> raise Not_found +let lookup_rel_id id sign = + let rec lookrec n = function + | [] -> raise Not_found + | (Anonymous, _, _) :: l -> lookrec (n + 1) l + | (Name id', b, t) :: l -> + if Names.Id.equal id' id then (n, b, t) else lookrec (n + 1) l in - lookrec (1,sign) + lookrec 1 sign (* Constructs either [forall x:t, c] or [let x:=b:t in c] *) let mkProd_or_LetIn (na,body,t) c = @@ -250,6 +222,13 @@ let it_mkNamedProd_or_LetIn init = it_named_context_quantifier mkNamedProd_or_Le 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 rec aux k decls c = match decls with + | [] -> c + | (na,Some b,t)::decls -> mkLetIn (na,b,t,aux (k-1) decls (liftn 1 k c)) + | (na,None,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 *) @@ -258,7 +237,7 @@ let rec strip_head_cast c = match kind_of_term c with 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 Array.length cl2 = 0 then f else mkApp (f,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 @@ -267,15 +246,15 @@ let rec strip_head_cast c = match kind_of_term c with 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) -> + | App (f,args) when isEvar (Array.last args) -> drop_extra_implicit_args - (mkApp (f,fst (array_chop (Array.length args - 1) 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 "last_arg" + | App (f,cl) -> Array.last cl + | _ -> anomaly (Pp.str "last_arg") (* Get the last arg of an application *) let decompose_app_vect c = @@ -285,22 +264,22 @@ let decompose_app_vect c = let adjust_app_list_size f1 l1 f2 l2 = let len1 = List.length l1 and len2 = List.length l2 in - if len1 = len2 then (f1,l1,f2,l2) + if Int.equal len1 len2 then (f1,l1,f2,l2) else if len1 < len2 then - let extras,restl2 = list_chop (len2-len1) l2 in + 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 + 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 len1 = len2 then (f1,l1,f2,l2) + if Int.equal len1 len2 then (f1,l1,f2,l2) else if len1 < len2 then - let extras,restl2 = array_chop (len2-len1) l2 in + 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 + 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 @@ -317,6 +296,7 @@ let map_constr_with_named_binders g f l c = match kind_of_term c with | 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)) -> @@ -337,45 +317,81 @@ let map_constr_with_named_binders g f l c = match kind_of_term c with (co-)fixpoint) *) let fold_rec_types g (lna,typarray,_) e = - let ctxt = array_map2_i (fun i na t -> (na, None, lift i t)) lna typarray in + let ctxt = Array.map2_i (fun i na t -> (na, None, 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 = match kind_of_term c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> c - | Cast (c,k,t) -> let c' = f l c in mkCast (c',k,f l t) - | Prod (na,t,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 - mkProd (na, t', f (g (na,None,t) l) c) - | Lambda (na,t,c) -> + let b' = f (g (na,None,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 - mkLambda (na, t', f (g (na,None,t) l) c) - | LetIn (na,b,t,c) -> - let b' = f l b in + let b' = f (g (na,None,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 c' = f (g (na,Some b,t) l) c in - mkLetIn (na, b', t', c') + let b' = f (g (na,Some 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 (c,al) -> + | App (t,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 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 c' = f l c in + let b' = f l b in let p' = f l p in - mkCase (ci, p', c', array_map_left (f l) bl) + 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') = array_map_left_pair (f l) tl (f l') bl in - mkFix (ln,(lna,tl',bl')) + 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') = array_map_left_pair (f l) tl (f l') bl in - mkCoFix (ln,(lna,tl',bl')) + 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 = match kind_of_term cstr with @@ -401,30 +417,33 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with | 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') + 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') + 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 + 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 + 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' + 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 + 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' + if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl' then cstr else mkCoFix (ln,(lna,tl',bl')) @@ -443,15 +462,16 @@ let fold_constr_with_binders g f n acc c = match kind_of_term c with | 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 + | 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' = iterate g (Array.length tl) n in - let fd = array_map2 (fun t b -> (t,b)) tl bl 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 + 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 @@ -467,14 +487,15 @@ let iter_constr_with_full_binders g f l c = match kind_of_term c with | 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 + | 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 (na,None,t) l) l lna tl in + 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 + 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 @@ -503,23 +524,16 @@ let occur_meta_or_existential c = | _ -> 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 + | 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 List.mem id vars then raise Occur + if Id.Set.mem id vars then raise Occur let occur_var env id c = let rec occur_rec c = @@ -540,10 +554,10 @@ let occur_var_in_decl env hyp (_,c,typ) = 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 + | 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 Intset.empty m + frec 1 Int.Set.empty m (* collects all metavar occurences, in left-to-right order, preserving * repetitions and all. *) @@ -551,7 +565,7 @@ let free_rels m = let collect_metas c = let rec collrec acc c = match kind_of_term c with - | Meta mv -> list_add_set mv acc + | Meta mv -> List.add_set Int.equal mv acc | _ -> fold_constr collrec acc c in List.rev (collrec [] c) @@ -560,32 +574,41 @@ let collect_metas c = 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 -> Idset.add id vars + | Var id -> Id.Set.add id vars | _ -> fold_constr aux vars c in - aux Idset.empty c + aux Id.Set.empty c (* Tests whether [m] is a subterm of [t]: [m] is appropriately lifted through abstractions of [t] *) -let dependent_main noevar m 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 eq_constr m t then + 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))); - Array.iter (deprec m) + CArray.Fun1.iter deprec m (Array.sub lt (Array.length lm) ((Array.length lt) - (Array.length lm))) - | _, Cast (c,_,_) when noevar & isMeta c -> () + | _, Cast (c,_,_) when noevar && isMeta c -> () | _, Evar _ when noevar -> () - | _ -> iter_constr_with_binders (lift 1) deprec m t + | _ -> 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 -let dependent_no_evar = dependent_main 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 (_,c,t) = + match c with + | None -> dependent a t + | Some body -> dependent a body || dependent a t let count_occurrences m t = let n = ref 0 in @@ -621,7 +644,7 @@ type meta_value_map = (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) + | 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 *) @@ -686,184 +709,42 @@ let replace_term_gen eq_fun c by_c in_t = let replace_term = replace_term_gen eq_constr -(* Substitute only at a list of locations or excluding a list of - locations; in the occurrences list (b,l), b=true means no - occurrence except the ones in l and b=false, means all occurrences - except the ones in l *) - -type hyp_location_flag = (* To distinguish body and type of local defs *) - | InHyp - | InHypTypeOnly - | InHypValueOnly - -type occurrences = bool * int list -let all_occurrences = (false,[]) -let no_occurrences_in_set = (true,[]) - -let error_invalid_occurrence l = - let l = list_uniquize (List.sort Pervasives.compare l) in - errorlabstrm "" - (str ("Invalid occurrence " ^ plural (List.length l) "number" ^": ") ++ - prlist_with_sep spc int l ++ str ".") - -let pr_position (cl,pos) = - let clpos = match cl with - | None -> str " of the goal" - | Some (id,InHyp) -> str " of hypothesis " ++ pr_id id - | Some (id,InHypTypeOnly) -> str " of the type of hypothesis " ++ pr_id id - | Some (id,InHypValueOnly) -> str " of the body of hypothesis " ++ pr_id id in - int pos ++ clpos - -let error_cannot_unify_occurrences nested (cl2,pos2,t2) (cl1,pos1,t1) (nowhere_except_in,locs) = - let s = if nested then "Found nested occurrences of the pattern" - else "Found incompatible occurrences of the pattern" in - errorlabstrm "" - (str s ++ str ":" ++ - spc () ++ str "Matched term " ++ quote (print_constr t2) ++ - strbrk " at position " ++ pr_position (cl2,pos2) ++ - strbrk " is not compatible with matched term " ++ - quote (print_constr t1) ++ strbrk " at position " ++ - pr_position (cl1,pos1) ++ str ".") - -let is_selected pos (nowhere_except_in,locs) = - nowhere_except_in && List.mem pos locs || - not nowhere_except_in && not (List.mem pos locs) - -exception NotUnifiable - -type 'a testing_function = { - match_fun : constr -> 'a; - merge_fun : 'a -> 'a -> 'a; - mutable testing_state : 'a; - mutable last_found : ((identifier * hyp_location_flag) option * int * constr) option -} - -let subst_closed_term_occ_gen_modulo (nowhere_except_in,locs as plocs) test cl occ t = - let maxocc = List.fold_right max locs 0 in - let pos = ref occ in - let nested = ref false in - let add_subst t subst = - try - test.testing_state <- test.merge_fun subst test.testing_state; - test.last_found <- Some (cl,!pos,t) - with NotUnifiable -> - let lastpos = Option.get test.last_found in - error_cannot_unify_occurrences !nested (cl,!pos,t) lastpos plocs in - let rec substrec k t = - if nowhere_except_in & !pos > maxocc then t else - try - let subst = test.match_fun t in - if is_selected !pos plocs then - (add_subst t subst; incr pos; - (* Check nested matching subterms *) - nested := true; ignore (subst_below k t); nested := false; - (* Do the effective substitution *) - mkRel k) - else - (incr pos; subst_below k t) - with NotUnifiable -> - subst_below k t - and subst_below k t = - map_constr_with_binders_left_to_right (fun d k -> k+1) substrec k t - in - let t' = substrec 1 t in - (!pos, t') - -let is_nowhere (nowhere_except_in,locs) = nowhere_except_in && locs = [] - -let check_used_occurrences nbocc (nowhere_except_in,locs) = - let rest = List.filter (fun o -> o >= nbocc) locs in - if rest <> [] then error_invalid_occurrence rest - -let proceed_with_occurrences f plocs x = - if is_nowhere plocs then (* optimization *) x else - begin - assert (List.for_all (fun x -> x >= 0) (snd plocs)); - let (nbocc,x) = f 1 x in - check_used_occurrences nbocc plocs; - x - end - -let make_eq_test c = { - match_fun = (fun c' -> if eq_constr c c' then () else raise NotUnifiable); - merge_fun = (fun () () -> ()); - testing_state = (); - last_found = None -} - -let subst_closed_term_occ_gen plocs pos c t = - subst_closed_term_occ_gen_modulo plocs (make_eq_test c) None pos t - -let subst_closed_term_occ plocs c t = - proceed_with_occurrences (fun occ -> subst_closed_term_occ_gen plocs occ c) - plocs t - -let subst_closed_term_occ_modulo plocs test cl t = - proceed_with_occurrences - (subst_closed_term_occ_gen_modulo plocs test cl) plocs t - -let map_named_declaration_with_hyploc f hyploc acc (id,bodyopt,typ) = - let f = f (Some (id,hyploc)) in - match bodyopt,hyploc with - | None, InHypValueOnly -> - errorlabstrm "" (pr_id id ++ str " has no value.") - | None, _ | Some _, InHypTypeOnly -> - let acc,typ = f acc typ in acc,(id,bodyopt,typ) - | Some body, InHypValueOnly -> - let acc,body = f acc body in acc,(id,Some body,typ) - | Some body, InHyp -> - let acc,body = f acc body in - let acc,typ = f acc typ in - acc,(id,Some body,typ) - -let subst_closed_term_occ_decl (plocs,hyploc) c d = - proceed_with_occurrences - (map_named_declaration_with_hyploc - (fun _ occ -> subst_closed_term_occ_gen plocs occ c) hyploc) plocs d - -let subst_closed_term_occ_decl_modulo (plocs,hyploc) test d = - proceed_with_occurrences - (map_named_declaration_with_hyploc - (subst_closed_term_occ_gen_modulo plocs test) - hyploc) - plocs d - 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) + Context.fold_named_context (fun (id,_,_) s -> Id.Set.add id s) + (named_context env) ~init:Id.Set.empty in + Context.fold_rel_context + (fun (na,_,_) s -> match na with Name id -> Id.Set.add id s | _ -> s) (rel_context env) ~init:s let add_vname vars = function - Name id -> Idset.add id vars + Name id -> Id.Set.add id vars | _ -> vars (*************************) (* Names environments *) (*************************) -type names_context = name list +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 rec lookup_rel_of_name id names = +let 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 + | (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 = - Sign.fold_rel_context + Context.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:[] + Context.fold_named_context (fun (id,_,_) idl -> id::idl) sign ~init:[] let ids_of_context env = (ids_of_rel_context (rel_context env)) @@ -882,15 +763,16 @@ let isGlobalRef c = | Const _ | Ind _ | Construct _ | Var _ -> true | _ -> false -let has_polymorphic_type c = - match (Global.lookup_constant c).Declarations.const_type with - | Declarations.PolymorphicArity _ -> true +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 or c2 = Pos (* Prop <= Set *) - | (Prop c1, Type u) -> pb = Reduction.CUMUL + | (Prop c1, Prop c2) -> c1 == Null || c2 == Pos (* Prop <= Set *) + | (Prop c1, Type u) -> pb == Reduction.CUMUL | (Type u1, Type u2) -> true | _ -> false @@ -899,45 +781,48 @@ 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 (f Reduction.CONV) t1 t2 + 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 = constr_cmp Reduction.CONV +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 len=0 then ([],c) else + 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 -let hdtl l = List.hd l, List.tl l - -type subst = (rel_context*constr) Intmap.t +type subst = (rel_context*constr) Evar.Map.t exception CannotFilter let filtering env cv_pb c1 c2 = - let evm = ref Intmap.empty in + let evm = ref Evar.Map.empty in let define cv_pb e1 ev c1 = - try let (e2,c2) = Intmap.find ev !evm in + 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 := Intmap.add ev (e1,c1) !evm + 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 - aux env cv_pb l1 l2; if p1=[] & p2=[] then () else - aux env cv_pb (applist (hdtl p1)) (applist (hdtl p2)) + 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 ((n,None,t1)::env) cv_pb c1 c2 @@ -963,12 +848,12 @@ let align_prod_letin c a : rel_context * 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 + let (l1,l2) = Util.List.chop lc l in l2,it_mkProd_or_LetIn a l1 -(* On reduit une serie d'eta-redex de tete ou rien du tout *) +(* 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 versions précédentes buggées *) +(* Remplace 2 earlier buggish versions *) let rec eta_reduce_head c = match kind_of_term c with @@ -976,12 +861,12 @@ let rec eta_reduce_head 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" + if lastn < 0 then anomaly (Pp.str "application without arguments") else (match kind_of_term cl.(lastn) with | Rel 1 -> let c' = - if lastn = 1 then f + if Int.equal lastn 0 then f else mkApp (f, Array.sub cl 0 lastn) in if noccurn 1 c' @@ -992,24 +877,15 @@ let rec eta_reduce_head 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_val 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 + Context.fold_rel_context f rels ~init:env0 let assums_of_rel_context sign = - Sign.fold_rel_context + Context.fold_rel_context (fun (na,c,t) l -> match c with Some _ -> l @@ -1054,37 +930,49 @@ let adjust_subst_to_rel_context sign l = | (_,Some c,_)::sign', args' -> aux (substl (List.rev subst) c :: subst) sign' args' | [], [] -> List.rev subst - | _ -> anomaly "Instance and signature do not match" + | _ -> anomaly (Pp.str "Instance and signature do not match") in aux [] (List.rev sign) l -let fold_named_context_both_sides f l ~init = list_fold_right_and_left f l init +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 + | (id',_,_) :: _ when Id.equal id id' -> true | _ :: sign -> mem_named_context id sign | [] -> false +let compact_named_context_reverse sign = + let compact l (i1,c1,t1) = + 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.fold_named_context_reverse compact ~init:[] sign + +let compact_named_context sign = List.rev (compact_named_context_reverse sign) + let clear_named_body id env = - let rec aux _ = function - | (id',Some c,t) when id = id' -> push_named (id,None,t) + let aux _ = function + | (id',Some c,t) when Id.equal id id' -> push_named (id,None,t) | d -> push_named d in fold_named_context aux env ~init:(reset_context env) -let global_vars env ids = Idset.elements (global_vars_set env ids) +let global_vars env ids = Id.Set.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) + Id.Set.union (global_vars_set env t) (global_vars_set env c) let dependency_closure env sign hyps = - if Idset.is_empty hyps then [] else + if Id.Set.is_empty hyps then [] else let (_,lh) = - Sign.fold_named_context_reverse + Context.fold_named_context_reverse (fun (hs,hl) (x,_,_ as d) -> - if Idset.mem x hs then - (Idset.union (global_vars_set_of_decl env d) (Idset.remove x hs), + 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,[]) @@ -1104,13 +992,13 @@ let context_chop k ctx = | (0, l2) -> (List.rev acc, l2) | (n, ((_,Some _,_ as h)::t)) -> chop_aux (h::acc) (n, t) | (n, (h::t)) -> chop_aux (h::acc) (pred n, t) - | (_, []) -> anomaly "context_chop" + | (_, []) -> 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 + let ctx1,ctx2 = List.chop k rels in push_rel_context ctx2 (reset_with_named_context (named_context_val env) env), ctx1 @@ -1122,13 +1010,15 @@ 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 + let na1 = Name (Id.of_string "A") in + let na2 = Name (Id.of_string "H") in fun () -> match !impossible_default_case with - | Some (id,type_of_id) -> - make_judge id type_of_id + | 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))) + (mkProd (na1,mkProp,mkArrow (mkRel 1) (mkRel 2))), + Univ.ContextSet.empty |