From 2e3ee15b03cf4b7428e1a7453385d79f434ec4a7 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 8 Nov 2015 09:54:42 +0100 Subject: Moving three related small half-general half-ad-hoc utility functions next to each other, waiting for possible integration into a more uniform API. --- engine/termops.ml | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) (limited to 'engine/termops.ml') diff --git a/engine/termops.ml b/engine/termops.ml index ebd9d939aa..5716a19dd1 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -846,6 +846,34 @@ let decompose_prod_letin : constr -> int * rel_context * constr = | _ -> 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 : rel_context * constr = let (lc,_,_) = decompose_prod_letin c in let (la,l,a) = decompose_prod_letin a in -- cgit v1.2.3 From ade2363e357db3ac3f258e645fe6bba988e7e7dd Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 19 Nov 2015 22:49:25 +0100 Subject: About building of substitutions from instances. Redefining adjust_subst_to_rel_context from instantiate_context who was hidden in inductiveops.ml, renamed the latter into subst_of_rel_context_instance and moving them to Vars. The new name highlights that the input is an instance (as for applist) and the output a substitution (as for substl). This is a clearer unified interface, centralizing the difficult de-Bruijn job in one place. It saves a couple of List.rev. --- engine/termops.ml | 10 ---------- 1 file changed, 10 deletions(-) (limited to 'engine/termops.ml') diff --git a/engine/termops.ml b/engine/termops.ml index 5716a19dd1..63baec129e 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -953,16 +953,6 @@ let smash_rel_context sign = 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 subst c :: subst) sign' args' - | [], [] -> List.rev subst - | _ -> 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 rec mem_named_context id = function -- cgit v1.2.3 From 6899d3aa567436784a08af4e179c2ef1fa504a02 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 21 Nov 2015 00:17:21 +0100 Subject: Moving extended_rel_vect/extended_rel_list to the kernel. It will later be used to fix a bug and improve some code. Interestingly, there were a redundant semantic equivalent to extended_rel_list in the kernel called local_rels, and another private copy of extended_rel_list in exactly the same file. --- engine/termops.ml | 13 ------------- 1 file changed, 13 deletions(-) (limited to 'engine/termops.ml') diff --git a/engine/termops.ml b/engine/termops.ml index 63baec129e..db0f1e4db5 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -158,19 +158,6 @@ let rel_list n m = in reln [] 1 -(* Same as [rel_list] but takes a context as argument and skips let-ins *) -let extended_rel_list n hyps = - let rec reln l p = function - | (_,None,_) :: hyps -> reln (mkRel (n+p) :: l) (p+1) hyps - | (_,Some _,_) :: hyps -> reln l (p+1) hyps - | [] -> l - in - reln [] 1 hyps - -let extended_rel_vect n hyps = Array.of_list (extended_rel_list n hyps) - - - let push_rel_assum (x,t) env = push_rel (x,None,t) env let push_rels_assum assums = -- cgit v1.2.3 From a582737fc27da2c03c8c57c773fc4854c1e88d7a Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 15 Dec 2015 14:03:12 +0100 Subject: API: documenting context_chop and removing a duplicate. --- engine/termops.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'engine/termops.ml') diff --git a/engine/termops.ml b/engine/termops.ml index db0f1e4db5..c10c55220b 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -992,8 +992,8 @@ 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 - variables; skips let-in's *) +(* 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) -- cgit v1.2.3 From 9d991d36c07efbb6428e277573bd43f6d56788fc Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 8 Jan 2016 10:00:21 +0100 Subject: CLEANUP: kernel/context.ml{,i} The structure of the Context module was refined in such a way that: - Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module. - Types and functions related to rel-context were put into the Context.Rel module. - Types and functions related to named-context declarations were put into the Context.Named.Declaration module. - Types and functions related to named-context were put into the Context.Named module. - Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module. - Types and functions related to named-list-context were put into Context.NamedList module. Some missing comments were added to the *.mli file. The output of ocamldoc was checked whether it looks in a reasonable way. "TODO: cleanup" was removed The order in which are exported functions listed in the *.mli file was changed. (as in a mature modules, this order usually is not random) The order of exported functions in Context.{Rel,Named} modules is now consistent. (as there is no special reason why that order should be different) The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file. (as there is no special reason to define them in a different order) The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do. (Now they are called Context.{Rel,Named}.fold_{inside,outside}) The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated. Thrown exceptions are now documented. Naming of formal parameters was made more consistent across different functions. Comments of similar functions in different modules are now consistent. Comments from *.mli files were copied to *.ml file. (We need that information in *.mli files because that is were ocamldoc needs it. It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function, we can see the comments also there and do not need to open a different file if we want to see it.) When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1. (UTF-8 characters are used in our ocamldoc markup) "open Context" was removed from all *.mli and *.ml files. (Originally, it was OK to do that. Now it is not.) An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed. --- engine/termops.ml | 29 ++++++++++++++--------------- 1 file changed, 14 insertions(+), 15 deletions(-) (limited to 'engine/termops.ml') diff --git a/engine/termops.ml b/engine/termops.ml index c10c55220b..ce640bacf1 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -13,7 +13,6 @@ open Names open Nameops open Term open Vars -open Context open Environ (* Sorts and sort family *) @@ -700,9 +699,9 @@ let replace_term = replace_term_gen eq_constr let vars_of_env env = let s = - Context.fold_named_context (fun (id,_,_) s -> Id.Set.add id s) + Context.Named.fold_outside (fun (id,_,_) s -> Id.Set.add id s) (named_context env) ~init:Id.Set.empty in - Context.fold_rel_context + Context.Rel.fold_outside (fun (na,_,_) s -> match na with Name id -> Id.Set.add id s | _ -> s) (rel_context env) ~init:s @@ -728,12 +727,12 @@ let lookup_rel_of_name id names = let empty_names_context = [] let ids_of_rel_context sign = - Context.fold_rel_context + Context.Rel.fold_outside (fun (na,_,_) l -> match na with Name id -> id::l | Anonymous -> l) sign ~init:[] let ids_of_named_context sign = - Context.fold_named_context (fun (id,_,_) idl -> id::idl) sign ~init:[] + Context.Named.fold_outside (fun (id,_,_) idl -> id::idl) sign ~init:[] let ids_of_context env = (ids_of_rel_context (rel_context env)) @@ -788,7 +787,7 @@ let split_app c = match kind_of_term c with c::(Array.to_list prev), last | _ -> assert false -type subst = (rel_context*constr) Evar.Map.t +type subst = (Context.Rel.t * constr) Evar.Map.t exception CannotFilter @@ -825,7 +824,7 @@ let filtering env cv_pb c1 c2 = in aux env cv_pb c1 c2; !evm -let decompose_prod_letin : constr -> int * rel_context * constr = +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) ((n,None,t)::l) c | LetIn (n,d,t,c) -> prodec_rec (succ i) ((n,Some d,t)::l) c @@ -861,7 +860,7 @@ let nb_prod_modulo_zeta x = | _ -> n in count 0 x -let align_prod_letin c a : rel_context * constr = +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"; @@ -899,10 +898,10 @@ 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.fold_rel_context f rels ~init:env0 + Context.Rel.fold_outside f rels ~init:env0 let assums_of_rel_context sign = - Context.fold_rel_context + Context.Rel.fold_outside (fun (na,c,t) l -> match c with Some _ -> l @@ -912,7 +911,7 @@ let assums_of_rel_context 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 + aux (push_rel d env) (Context.Rel.Declaration.map (f env) d :: acc) sign | [] -> acc in @@ -920,10 +919,10 @@ let map_rel_context_in_env f env sign = let map_rel_context_with_binders f sign = let rec aux k = function - | d::sign -> map_rel_declaration (f k) d :: aux (k-1) sign + | d::sign -> Context.Rel.Declaration.map (f k) d :: aux (k-1) sign | [] -> [] in - aux (rel_context_length sign) sign + aux (Context.Rel.length sign) sign let substl_rel_context l = map_rel_context_with_binders (fun k -> substnl l (k-1)) @@ -955,7 +954,7 @@ let compact_named_context_reverse sign = 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 + in Context.Named.fold_inside compact ~init:[] sign let compact_named_context sign = List.rev (compact_named_context_reverse sign) @@ -976,7 +975,7 @@ let global_vars_set_of_decl env = function let dependency_closure env sign hyps = if Id.Set.is_empty hyps then [] else let (_,lh) = - Context.fold_named_context_reverse + Context.Named.fold_inside (fun (hs,hl) (x,_,_ as d) -> if Id.Set.mem x hs then (Id.Set.union (global_vars_set_of_decl env d) (Id.Set.remove x hs), -- cgit v1.2.3 From 34ef02fac1110673ae74c41c185c228ff7876de2 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 29 Jan 2016 10:13:12 +0100 Subject: CLEANUP: Context.{Rel,Named}.Declaration.t Originally, rel-context was represented as: Context.rel_context = Names.Name.t * Constr.t option * Constr.t Now it is represented as: Context.Rel.t = LocalAssum of Names.Name.t * Constr.t | LocalDef of Names.Name.t * Constr.t * Constr.t Originally, named-context was represented as: Context.named_context = Names.Id.t * Constr.t option * Constr.t Now it is represented as: Context.Named.t = LocalAssum of Names.Id.t * Constr.t | LocalDef of Names.Id.t * Constr.t * Constr.t Motivation: (1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction" function which looked like this: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published. --- engine/termops.ml | 199 +++++++++++++++++++++++++++++++----------------------- 1 file changed, 115 insertions(+), 84 deletions(-) (limited to 'engine/termops.ml') diff --git a/engine/termops.ml b/engine/termops.ml index b7d89ba7b1..f698f81513 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -15,6 +15,9 @@ open Term open Vars open Environ +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + (* Sorts and sort family *) let print_sort = function @@ -98,26 +101,28 @@ 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 (id,c,typ) = - let pbody = match c with - | None -> (mt ()) - | Some c -> +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 typ in + let pt = print_constr_env env (get_type decl) in let ptyp = (str" : " ++ pt) in - (pr_id id ++ hov 0 (pbody ++ ptyp)) + (pr_id (get_id decl) ++ hov 0 (pbody ++ ptyp)) -let pr_rel_decl env (na,c,typ) = - let pbody = match c with - | None -> mt () - | Some c -> +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 typ in - match na with + 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) @@ -157,42 +162,53 @@ let rel_list n m = in reln [] 1 -let push_rel_assum (x,t) env = push_rel (x,None,t) env +let push_rel_assum (x,t) env = + let open RelDecl in + push_rel (LocalAssum (x,t)) env let push_rels_assum assums = - push_rel_context (List.map (fun (x,t) -> (x,None,t)) 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 -> (id, None, lift i t) + | 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 - | (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 + | [] -> + 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 (na,body,t) c = - match body with - | None -> mkProd (na, t, c) - | Some b -> mkLetIn (na, b, t, 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 (na,body,t) c = - match body with - | None -> mkProd (na, t, c) - | Some b -> subst1 b c +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 @@ -208,10 +224,11 @@ let it_mkNamedProd_wo_LetIn init = it_named_context_quantifier mkNamedProd_wo_Le 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 - | (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) + | 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 (* *) @@ -302,7 +319,7 @@ 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 -> 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 = @@ -317,7 +334,9 @@ let map_left2 f a g b = r, s end -let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with +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) -> @@ -327,18 +346,18 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with else mkCast (b',k,t') | Prod (na,t,b) -> let t' = f l t in - let b' = f (g (na,None,t) l) b 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 (na,None,t) l) b 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 (na,Some bo,t) l) b 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 @@ -379,7 +398,9 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with else mkCoFix (ln,(lna,tl',bl')) (* strong *) -let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with +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) -> @@ -388,16 +409,16 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with 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 (na,None,t) l) c 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 (na,None,t) l) c 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 (na,Some b,t) l) c 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 @@ -418,7 +439,7 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with | 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 (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 @@ -426,7 +447,7 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with | 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 (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 @@ -439,23 +460,25 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with 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 = match kind_of_term c with +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 (na,None,t) n) (f n acc t) c - | Lambda (na,t,c) -> f (g (na,None,t) n) (f n acc t) c - | LetIn (na,b,t,c) -> f (g (na,Some b,t) n) (f n (f n acc b) t) c + | 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 (n,None,t) c) n lna tl in + 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 (n,None,t) c) n lna tl in + 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 @@ -467,23 +490,25 @@ let fold_constr_with_binders g f n acc c = each binder traversal; it is not recursive and the order with which subterms are processed is not specified *) -let iter_constr_with_full_binders g f l c = match kind_of_term c with +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 (na,None,t) l) c - | Lambda (na,t,c) -> f l t; f (g (na,None,t) l) c - | LetIn (na,b,t,c) -> f l b; f l t; f (g (na,Some b,t) l) c + | 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 (na,None,t) l) l lna tl in + 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 (na,None,t) l) l lna tl in + 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 @@ -531,10 +556,11 @@ let occur_var env id c = in try occur_rec c; false with Occur -> true -let occur_var_in_decl env hyp (_,c,typ) = - match c with - | None -> occur_var env hyp typ - | Some body -> +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 @@ -593,10 +619,11 @@ 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 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 @@ -699,10 +726,10 @@ let replace_term = replace_term_gen eq_constr let vars_of_env env = let s = - Context.Named.fold_outside (fun (id,_,_) s -> Id.Set.add id 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 (na,_,_) s -> match na with Name id -> Id.Set.add id s | _ -> s) + (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 @@ -728,11 +755,11 @@ let empty_names_context = [] let ids_of_rel_context sign = Context.Rel.fold_outside - (fun (na,_,_) l -> match na with Name id -> id::l | Anonymous -> l) + (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 (id,_,_) idl -> id::idl) sign ~init:[] + 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)) @@ -740,7 +767,7 @@ let ids_of_context env = let names_of_rel_context env = - List.map (fun (na,_,_) -> na) (rel_context env) + List.map RelDecl.get_name (rel_context env) let is_section_variable id = try let _ = Global.lookup_named id in true @@ -813,7 +840,7 @@ let filtering env cv_pb c1 c2 = end | Prod (n,t1,c1), Prod (_,t2,c2) -> aux env cv_pb t1 t2; - aux ((n,None,t1)::env) cv_pb c1 c2 + 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 | _ -> @@ -826,8 +853,8 @@ let filtering env cv_pb c1 c2 = 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) ((n,None,t)::l) c - | LetIn (n,d,t,c) -> prodec_rec (succ i) ((n,Some d,t)::l) c + | 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 [] @@ -902,16 +929,16 @@ let process_rel_context f env = let assums_of_rel_context sign = Context.Rel.fold_outside - (fun (na,c,t) l -> - match c with - Some _ -> l - | None -> (na, t)::l) + (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) (Context.Rel.Declaration.map (f env) d :: acc) sign + aux (push_rel d env) (RelDecl.map_constr (f env) d :: acc) sign | [] -> acc in @@ -919,7 +946,7 @@ let map_rel_context_in_env f env sign = let map_rel_context_with_binders f sign = let rec aux k = function - | d::sign -> Context.Rel.Declaration.map (f k) d :: aux (k-1) sign + | d::sign -> RelDecl.map_constr (f k) d :: aux (k-1) sign | [] -> [] in aux (Context.Rel.length sign) sign @@ -933,21 +960,23 @@ let lift_rel_context n = let smash_rel_context sign = let rec aux acc = function | [] -> acc - | (_,None,_ as d) :: l -> aux (d::acc) l - | (_,Some b,_) :: l -> + | (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 rec mem_named_context id = function - | (id',_,_) :: _ when Id.equal id id' -> true +let rec mem_named_context id ctxt = + match ctxt with + | decl :: _ when Id.equal id (NamedDecl.get_id decl) -> true | _ :: sign -> mem_named_context id sign | [] -> false let compact_named_context_reverse sign = - let compact l (i1,c1,t1) = + let compact l decl = + let (i1,c1,t1) = NamedDecl.to_tuple decl in match l with | [] -> [[i1],c1,t1] | (l2,c2,t2)::q -> @@ -959,16 +988,17 @@ let compact_named_context_reverse 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 - | (id',Some c,t) when Id.equal id id' -> push_named (id,None,t) + | 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 - | (_,None,t) -> global_vars_set env t - | (_,Some c,t) -> + | 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) @@ -976,7 +1006,8 @@ let dependency_closure env sign hyps = if Id.Set.is_empty hyps then [] else let (_,lh) = Context.Named.fold_inside - (fun (hs,hl) (x,_,_ as d) -> + (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) @@ -996,7 +1027,7 @@ let on_judgment_type f j = { j with uj_type = f j.uj_type } let context_chop k ctx = let rec chop_aux acc = function | (0, l2) -> (List.rev acc, l2) - | (n, ((_,Some _,_ as h)::t)) -> chop_aux (h::acc) (n, t) + | (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) -- cgit v1.2.3