diff options
Diffstat (limited to 'pretyping/termops.ml')
| -rw-r--r-- | pretyping/termops.ml | 521 |
1 files changed, 183 insertions, 338 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 4f38fbb3..3e4c5ae5 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: termops.ml 12058 2009-04-08 10:54:59Z herbelin $ *) +(* $Id$ *) open Pp open Util @@ -34,7 +34,7 @@ let pr_name = function | Name id -> pr_id id | Anonymous -> str "_" -let pr_sp sp = str(string_of_kn sp) +let pr_path sp = str(string_of_kn sp) let pr_con sp = str(string_of_con sp) let rec pr_constr c = match kind_of_term c with @@ -42,7 +42,7 @@ let rec pr_constr c = match kind_of_term c with | Meta n -> str "Meta(" ++ int n ++ str ")" | Var id -> pr_id id | Sort s -> print_sort s - | Cast (c,_, t) -> hov 1 + | Cast (c,_, t) -> hov 1 (str"(" ++ pr_constr c ++ cut() ++ str":" ++ pr_constr t ++ str")") | Prod (Name(id),t,c) -> hov 1 @@ -65,9 +65,9 @@ let rec pr_constr c = match kind_of_term c with (str"Evar#" ++ int 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_sp sp ++ str"," ++ int i ++ str")" + | Ind (sp,i) -> str"Ind(" ++ pr_mind sp ++ str"," ++ int i ++ str")" | Construct ((sp,i),j) -> - str"Constr(" ++ pr_sp sp ++ str"," ++ int i ++ str"," ++ int j ++ str")" + str"Constr(" ++ pr_mind sp ++ str"," ++ int i ++ str"," ++ int j ++ str")" | Case (ci,p,c,bl) -> v 0 (hv 0 (str"<"++pr_constr p++str">"++ cut() ++ str"Case " ++ pr_constr c ++ str"of") ++ cut() ++ @@ -99,7 +99,7 @@ let pr_var_decl env (id,c,typ) = let pbody = match c with | None -> (mt ()) | Some c -> - (* Force evaluation *) + (* Force evaluation *) let pb = print_constr_env env c in (str" := " ++ pb ++ cut () ) in let pt = print_constr_env env typ in @@ -110,7 +110,7 @@ let pr_rel_decl env (na,c,typ) = let pbody = match c with | None -> mt () | Some c -> - (* Force evaluation *) + (* Force evaluation *) let pb = print_constr_env env c in (str":=" ++ spc () ++ pb ++ spc ()) in let ptyp = print_constr_env env typ in @@ -120,39 +120,39 @@ let pr_rel_decl env (na,c,typ) = let print_named_context env = hv 0 (fold_named_context - (fun env d pps -> + (fun env d pps -> pps ++ ws 2 ++ pr_var_decl env d) env ~init:(mt ())) -let print_rel_context env = +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 ()) + 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 + in (sign_env ++ db_env) - + (*let current_module = ref empty_dirpath let set_module m = current_module := m*) -let new_univ = +let new_univ = let univ_gen = ref 0 in (fun sp -> - incr univ_gen; + incr univ_gen; Univ.make_univ (Lib.library_dp(),!univ_gen)) let new_Type () = mkType (new_univ ()) let new_Type_sort () = Type (new_univ ()) @@ -173,26 +173,20 @@ let refresh_universes_gen strict t = let refresh_universes = refresh_universes_gen false let refresh_universes_strict = refresh_universes_gen true -let new_sort_in_family = function +let new_sort_in_family = function | InProp -> prop_sort | InSet -> set_sort | 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 = +let rel_list n m = + let rec reln l p = if p>m then l else reln (mkRel(n+p)::l) (p+1) - in + in reln [] 1 (* Same as [rel_list] but takes a context as argument and skips let-ins *) @@ -201,7 +195,7 @@ let extended_rel_list n hyps = | (_,None,_) :: hyps -> reln (mkRel (n+p) :: l) (p+1) hyps | (_,Some _,_) :: hyps -> reln l (p+1) hyps | [] -> l - in + in reln [] 1 hyps let extended_rel_vect n hyps = Array.of_list (extended_rel_list n hyps) @@ -224,53 +218,49 @@ let push_named_rec_types (lna,typarray,_) env = Array.fold_left (fun e assum -> push_named assum e) env ctxt -let rec lookup_rel_id id sign = +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) + | (n, (Name id',b,t)::l) -> if id' = id then (n,b,t) else lookrec (n+1,l) | (_, []) -> raise Not_found - in + in lookrec (1,sign) -(* Constructs either [(x:t)c] or [[x=b:t]c] *) +(* Constructs either [forall x:t, c] or [let x:=b:t in 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] *) +(* Constructs either [forall x:t, c] or [c] in which [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_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 = +let it_named_context_quantifier f ~init = List.fold_left (fun c d -> f d c) init +let it_mkProd_or_LetIn = it_named_context_quantifier mkProd_or_LetIn +let it_mkProd_wo_LetIn = it_named_context_quantifier mkProd_wo_LetIn +let it_mkLambda_or_LetIn = it_named_context_quantifier mkLambda_or_LetIn let it_mkNamedProd_or_LetIn = it_named_context_quantifier mkNamedProd_or_LetIn -let it_mkNamedLambda_or_LetIn = it_named_context_quantifier mkNamedLambda_or_LetIn - let it_mkNamedProd_wo_LetIn = it_named_context_quantifier mkNamedProd_wo_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) -> + | 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 Array.length cl2 = 0 then f else mkApp (f,cl2) - in + in collapse_rec f cl | Cast (c,_,_) -> strip_head_cast c | _ -> c @@ -358,7 +348,7 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with 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,k, t) -> + | 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') @@ -422,7 +412,7 @@ let fold_constr_with_binders g f n acc c = match kind_of_term c with | 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)) -> + | 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 @@ -446,7 +436,7 @@ let iter_constr_with_full_binders g f l c = match kind_of_term c with | 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)) -> + | 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 @@ -456,7 +446,7 @@ let iter_constr_with_full_binders g f l c = match kind_of_term c with Array.iter (f l') bl (***************************) -(* occurs check functions *) +(* occurs check functions *) (***************************) exception Occur @@ -467,42 +457,43 @@ let occur_meta c = | _ -> iter_constr occrec c in try occrec c; false with Occur -> true -let occur_existential c = +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 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_const s c = +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 + in try occur_rec c; false with Occur -> true -let occur_evar n c = +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 + 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 occur_var env id c = let rec occur_rec c = - occur_in_global env s c; - iter_constr occur_rec c - in + 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 (_,c,typ) = @@ -512,25 +503,19 @@ let occur_var_in_decl env hyp (_,c,typ) = 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 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 + in frec 1 Intset.empty m (* collects all metavar occurences, in left-to-right order, preserving * repetitions and all. *) -let collect_metas c = +let collect_metas c = let rec collrec acc c = match kind_of_term c with | Meta mv -> list_add_set mv acc @@ -538,10 +523,10 @@ let collect_metas c = in List.rev (collrec [] c) -(* (dependent M N) is true iff M is eq_term with a subterm of N - M is appropriately lifted through abstractions of N *) +(* Tests whether [m] is a subterm of [t]: + [m] is appropriately lifted through abstractions of [t] *) -let dependent m t = +let dependent_main noevar m t = let rec deprec m t = if eq_constr m t then raise Occur @@ -550,28 +535,38 @@ let dependent m t = | 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.sub lt (Array.length lm) ((Array.length lt) - (Array.length lm))) + | _, Cast (c,_,_) when noevar & isMeta c -> () + | _, Evar _ when noevar -> () | _ -> iter_constr_with_binders (lift 1) deprec m t - in + in try deprec m t; false with Occur -> true +let dependent = dependent_main false +let dependent_no_evar = dependent_main true + +(* Synonymous *) +let occur_term = dependent + let pop t = lift (-1) t (***************************) -(* bindings functions *) +(* bindings functions *) (***************************) -type metamap = (metavariable * constr) list +type meta_type_map = (metavariable * types) list + +type meta_value_map = (metavariable * constr) list -let rec subst_meta bl c = +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 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) -> @@ -580,11 +575,11 @@ let prefix_application eq_fun (k,c) (t : constr) = 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 + else None | _ -> None -let my_prefix_application eq_fun (k,c) (by_c : constr) (t : constr) = +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) -> @@ -593,7 +588,7 @@ let my_prefix_application eq_fun (k,c) (by_c : constr) (t : constr) = 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 + else None | _ -> None @@ -602,7 +597,7 @@ let my_prefix_application eq_fun (k,c) (by_c : constr) (t : constr) = 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 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 @@ -610,7 +605,7 @@ let subst_term_gen eq_fun c t = 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 + in substrec (1,c) t (* Recognizing occurrences of a given (closed) subterm in a term : @@ -618,7 +613,7 @@ let subst_term_gen eq_fun c t = 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 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 @@ -626,7 +621,7 @@ let replace_term_gen eq_fun c by_c in_t = (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 + in substrec (0,c) in_t let subst_term = subst_term_gen eq_constr @@ -645,7 +640,7 @@ 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" ^": ") ++ + (str ("Invalid occurrence " ^ plural (List.length l) "number" ^": ") ++ prlist_with_sep spc int l ++ str ".") let subst_term_occ_gen (nowhere_except_in,locs) occ c t = @@ -656,10 +651,10 @@ let subst_term_occ_gen (nowhere_except_in,locs) occ c t = if nowhere_except_in & !pos > maxocc then t else if eq_constr c t then - let r = + let r = if nowhere_except_in then if List.mem !pos locs then (mkRel k) else t - else + else if List.mem !pos locs then t else (mkRel k) in incr pos; r else @@ -670,9 +665,9 @@ let subst_term_occ_gen (nowhere_except_in,locs) occ c t = let t' = substrec (1,c) t in (!pos, t') -let subst_term_occ (nowhere_except_in,locs as plocs) c t = +let subst_term_occ (nowhere_except_in,locs as plocs) c t = if locs = [] then if nowhere_except_in then t else subst_term c t - else + else let (nbocc,t') = subst_term_occ_gen plocs 1 c t in let rest = List.filter (fun o -> o >= nbocc) locs in if rest <> [] then error_invalid_occurrence rest; @@ -693,20 +688,15 @@ let subst_term_occ_decl ((nowhere_except_in,locs as plocs),hloc) c (id,bodyopt,t if locs = [] then if nowhere_except_in then d else (id,Some (subst_term c body),subst_term c typ) - else + else let (nbocc,body') = subst_term_occ_gen plocs 1 c body in let (nbocc',t') = subst_term_occ_gen plocs nbocc c typ in let rest = List.filter (fun o -> o >= nbocc') locs in if rest <> [] then error_invalid_occurrence rest; (id,Some body',t') -(* First character of a constr *) - -let lowercase_first_char id = - lowercase_first_char_utf8 (string_of_id id) - let vars_of_env env = - let s = + let s = Sign.fold_named_context (fun (id,_,_) s -> Idset.add id s) (named_context env) ~init:Idset.empty in Sign.fold_rel_context @@ -717,85 +707,6 @@ 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 -> - lowercase_first_char (id_of_label (con_label kn)) - | 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 mkProd_name env (n,a,b) = mkProd (named_hd env a n, a, b) -let mkLambda_name env (n,a,b) = mkLambda (named_hd env a n, a, b) - -let lambda_name = mkLambda_name -let prod_name = mkProd_name - -let prod_create env (a,b) = mkProd (named_hd env a Anonymous, a, b) -let lambda_create env (a,b) = mkLambda (named_hd env a Anonymous, a, b) - -let name_assumption env (na,c,t) = - match c with - | None -> (named_hd 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 *) (*************************) @@ -804,12 +715,12 @@ 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 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 + in lookrec 1 names let empty_names_context = [] @@ -821,7 +732,7 @@ let ids_of_rel_context sign = let ids_of_named_context sign = Sign.fold_named_context (fun (id,_,_) idl -> id::idl) sign ~init:[] -let ids_of_context env = +let ids_of_context env = (ids_of_rel_context (rel_context env)) @ (ids_of_named_context (named_context env)) @@ -829,57 +740,11 @@ let ids_of_context env = let names_of_rel_context env = List.map (fun (na,_,_) -> na) (rel_context env) -(**** Globality of identifiers *) - -let rec is_imported_modpath = function - | MPfile dp -> true - | p -> false - -let is_imported_ref = function - | VarRef _ -> false - | IndRef (kn,_) - | ConstructRef ((kn,_),_) -> - let (mp,_,_) = repr_kn kn in is_imported_modpath mp - | ConstRef kn -> - let (mp,_,_) = repr_con kn in 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_constructor id = - try - match locate (make_short_qualid id) with - | ConstructRef _ as ref -> not (is_imported_ref ref) - | _ -> false - with Not_found -> - false - let is_section_variable id = try let _ = Global.lookup_named id 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 - -let isGlobalRef c = +let isGlobalRef c = match kind_of_term c with | Const _ | Ind _ | Construct _ | Var _ -> true | _ -> false @@ -889,68 +754,6 @@ let has_polymorphic_type c = | Declarations.PolymorphicArity _ -> true | _ -> false -(* 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 *) - -type avoid_flags = bool option - -let next_name_not_occuring avoid_flags name l env_names t = - let rec next id = - if List.mem id l or occur_id env_names id t or - (* Further restrictions ? *) - match avoid_flags with None -> false | Some not_only_cstr -> - (if not_only_cstr then - (* To be consistent with the intro mechanism *) - is_global id & not (is_section_variable id) - else - (* To avoid constructors in pattern-matchings *) - is_constructor 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 *) - next (id_of_string "H") - let base_sort_cmp pb s0 s1 = match (s0,s1) with | (Prop c1, Prop c2) -> c1 = Null or c2 = Pos (* Prop <= Set *) @@ -959,14 +762,77 @@ let base_sort_cmp pb s0 s1 = | _ -> false (* eq_constr extended with universe erasure *) -let rec constr_cmp cv_pb t1 t2 = - (match kind_of_term t1, kind_of_term t2 with +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 - | _ -> false) - || compare_constr (constr_cmp cv_pb) t1 t2 + | Prod (_,t1,c1), Prod (_,t2,c2) -> + f Reduction.CONV t1 t2 & f cv_pb c1 c2 + | _ -> compare_constr (f Reduction.CONV) 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 +(* 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 + 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 + +exception CannotFilter + +let filtering env cv_pb c1 c2 = + let evm = ref Intmap.empty in + let define cv_pb e1 ev c1 = + try let (e2,c2) = Intmap.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 + 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)) + | Prod (n,t1,c1), Prod (_,t2,c2) -> + aux env cv_pb t1 t2; + aux ((n,None,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 * rel_context * constr = + let rec prodec_rec i l c = match kind_of_term c with + | Prod (n,t,c) -> prodec_rec (succ i) ((n,None,t)::l) c + | LetIn (n,d,t,c) -> prodec_rec (succ i) ((n,Some d,t)::l) c + | Cast (c,_,_) -> prodec_rec i l c + | _ -> i,l,c in + prodec_rec 0 [] + +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 + l2,it_mkProd_or_LetIn a l1 + (* 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 *) @@ -976,7 +842,7 @@ let rec eta_reduce_head c = | Lambda (_,c1,c') -> (match kind_of_term (eta_reduce_head c') with | App (f,cl) -> - let lastn = (Array.length cl) - 1 in + let lastn = (Array.length cl) - 1 in if lastn < 1 then anomaly "application without arguments" else (match kind_of_term cl.(lastn) with @@ -1017,7 +883,7 @@ let assums_of_rel_context sign = | None -> (na, t)::l) sign ~init:[] -let fold_map_rel_context f env sign = +let map_rel_context_in_env f env sign = let rec aux env acc = function | d::sign -> aux (push_rel d env) (map_rel_declaration (f env) d :: acc) sign @@ -1039,6 +905,25 @@ let substl_rel_context l = let lift_rel_context n = map_rel_context_with_binders (liftn n) +let smash_rel_context sign = + let rec aux acc = function + | [] -> acc + | (_,None,_ as d) :: l -> aux (d::acc) l + | (_,Some 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 adjust_subst_to_rel_context sign l = + let rec aux subst sign l = + match sign, l with + | (_,None,_)::sign', a::args' -> aux (a::subst) sign' args' + | (_,Some c,_)::sign', args' -> + aux (substl (List.rev subst) c :: subst) sign' args' + | [], [] -> List.rev subst + | _ -> anomaly "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 rec mem_named_context id = function @@ -1046,14 +931,11 @@ let rec mem_named_context id = function | _ :: 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 clear_named_body id env = + let rec aux _ = function + | (id',Some c,t) when 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) @@ -1076,50 +958,13 @@ let dependency_closure env sign hyps = sign in List.rev lh -let default_x = id_of_string "x" - -let rec next_name_away_in_cases_pattern id avoid = - let id = match id with Name id -> id | Anonymous -> default_x in - let rec next id = - if List.mem id avoid or is_constructor id then next (lift_ident id) - else id in - next id - -(* Remark: Anonymous var may be dependent in Evar's contexts *) -let concrete_name avoid_flags l env_names n c = - if n = Anonymous & noccurn 1 c then - (Anonymous,l) - else - let fresh_id = next_name_not_occuring avoid_flags 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 avoid_flags l env_names n c = - let fresh_id = next_name_not_occuring avoid_flags n l env_names c in - (Name fresh_id, fresh_id::l) - -let rec rename_bound_var env avoid c = - let env_names = names_of_rel_context env in - let rec rename avoid c = - match kind_of_term c with - | Prod (na,c1,c2) -> - let na',avoid' = concrete_name None avoid env_names na c2 in - mkProd (na', c1, rename avoid' c2) - | LetIn (na,c1,t,c2) -> - let na',avoid' = concrete_let_name None avoid env_names na c2 in - mkLetIn (na',c1,t, rename avoid' c2) - | Cast (c,k,t) -> mkCast (rename avoid c, k,t) - | _ -> c - in - rename avoid c - (* 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 +(* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k variables *) let context_chop k ctx = let rec chop_aux acc = function |