Permalink
Browse files

Moving Utils.list_* to a proper CList module, which includes stdlib

List module. That way, an "open Util" in the header permits using
any function of CList in the List namespace (and in particular, this
permits optimized reimplementations of the List functions, as, for
example, tail-rec implementations.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
1 parent 6dae53d commit f8394a52346bf1e6f98e7161e75fb65bd0631391 ppedrot committed Sep 14, 2012
Showing with 1,501 additions and 1,246 deletions.
  1. +4 −4 checker/check.ml
  2. +1 −0 checker/check.mllib
  3. +2 −2 checker/closure.ml
  4. +1 −1 checker/declarations.ml
  5. +4 −4 checker/indtypes.ml
  6. +7 −7 checker/inductive.ml
  7. +1 −1 checker/term.ml
  8. +1 −0 dev/printers.mllib
  9. +1 −0 grammar/grammar.mllib
  10. +3 −3 grammar/tacextend.ml4
  11. +1 −1 grammar/vernacextend.ml4
  12. +1 −1 ide/coqide.ml
  13. +1 −1 ide/wg_Command.ml
  14. +6 −6 ide/wg_Notebook.ml
  15. +1 −1 ide/wg_ProofView.ml
  16. +1 −1 interp/constrexpr_ops.ml
  17. +9 −9 interp/constrextern.ml
  18. +20 −20 interp/constrintern.ml
  19. +2 −2 interp/coqlib.ml
  20. +1 −1 interp/dumpglob.ml
  21. +1 −1 interp/implicit_quantifiers.ml
  22. +1 −1 interp/modintern.ml
  23. +5 −5 interp/notation.ml
  24. +18 −18 interp/notation_ops.ml
  25. +1 −1 interp/reserve.ml
  26. +1 −1 interp/topconstr.ml
  27. +2 −2 kernel/closure.ml
  28. +3 −3 kernel/declarations.ml
  29. +4 −4 kernel/indtypes.ml
  30. +7 −7 kernel/inductive.ml
  31. +2 −2 kernel/modops.ml
  32. +1 −1 kernel/names.ml
  33. +2 −2 kernel/pre_env.ml
  34. +2 −2 kernel/sign.ml
  35. +1 −1 kernel/subtyping.ml
  36. +10 −10 kernel/univ.ml
  37. +718 −0 lib/cList.ml
  38. +188 −0 lib/cList.mli
  39. +1 −0 lib/clib.mllib
  40. +2 −2 lib/gmapl.ml
  41. +3 −532 lib/util.ml
  42. +1 −127 lib/util.mli
  43. +1 −1 library/declare.ml
  44. +2 −2 library/heads.ml
  45. +4 −4 library/impargs.ml
  46. +1 −1 library/lib.ml
  47. +5 −5 library/libnames.ml
  48. +1 −1 library/library.ml
  49. +3 −3 parsing/egramcoq.ml
  50. +5 −5 parsing/g_tactic.ml4
  51. +6 −6 parsing/g_xml.ml4
  52. +1 −1 parsing/lexer.ml4
  53. +1 −1 parsing/pcoq.ml4
  54. +1 −1 plugins/cc/cctac.ml
  55. +4 −4 plugins/decl_mode/decl_interp.ml
  56. +9 −9 plugins/decl_mode/decl_proof_instr.ml
  57. +2 −2 plugins/extraction/common.ml
  58. +3 −3 plugins/extraction/extract_env.ml
  59. +13 −13 plugins/extraction/extraction.ml
  60. +9 −9 plugins/extraction/mlutil.ml
  61. +1 −1 plugins/extraction/modutil.ml
  62. +3 −3 plugins/extraction/ocaml.ml
  63. +2 −2 plugins/extraction/table.ml
  64. +3 −3 plugins/firstorder/formula.ml
  65. +1 −1 plugins/firstorder/instances.ml
  66. +1 −1 plugins/firstorder/rules.ml
  67. +2 −2 plugins/firstorder/sequent.ml
  68. +1 −1 plugins/firstorder/unify.ml
  69. +5 −5 plugins/funind/functional_principles_proofs.ml
  70. +3 −3 plugins/funind/functional_principles_types.ml
  71. +9 −9 plugins/funind/glob_term_to_relation.ml
  72. +8 −8 plugins/funind/indfun.ml
  73. +5 −5 plugins/funind/invfun.ml
  74. +2 −2 plugins/funind/merge.ml
  75. +4 −4 plugins/funind/recdef.ml
  76. +1 −1 plugins/nsatz/ideal.ml
  77. +1 −1 plugins/omega/coq_omega.ml
  78. +1 −1 plugins/omega/g_omega.ml4
  79. +9 −9 plugins/omega/omega.ml
  80. +1 −1 plugins/romega/g_romega.ml4
  81. +10 −10 plugins/romega/refl_omega.ml
  82. +4 −4 plugins/setoid_ring/newring.ml4
  83. +21 −21 pretyping/cases.ml
  84. +2 −2 pretyping/cbv.ml
  85. +1 −1 pretyping/classops.ml
  86. +1 −1 pretyping/coercion.ml
  87. +9 −9 pretyping/detyping.ml
  88. +4 −4 pretyping/evarconv.ml
  89. +13 −13 pretyping/evarutil.ml
  90. +4 −4 pretyping/evd.ml
  91. +4 −4 pretyping/glob_ops.ml
  92. +3 −3 pretyping/indrec.ml
  93. +6 −6 pretyping/inductiveops.ml
  94. +2 −2 pretyping/matching.ml
  95. +7 −7 pretyping/patternops.ml
  96. +2 −2 pretyping/pretyping.ml
  97. +2 −2 pretyping/recordops.ml
  98. +2 −2 pretyping/redops.ml
  99. +11 −11 pretyping/reductionops.ml
  100. +14 −14 pretyping/tacred.ml
  101. +7 −7 pretyping/termops.ml
  102. +8 −8 pretyping/typeclasses.ml
  103. +1 −1 pretyping/typing.ml
  104. +4 −4 printing/ppconstr.ml
  105. +1 −1 printing/pptactic.ml
  106. +2 −2 printing/prettyp.ml
  107. +2 −2 printing/printer.ml
  108. +2 −2 proofs/clenv.ml
  109. +3 −3 proofs/logic.ml
  110. +1 −1 proofs/pfedit.ml
  111. +1 −1 proofs/proofview.ml
  112. +2 −2 proofs/redexpr.ml
  113. +2 −2 proofs/refiner.ml
  114. +18 −18 tactics/auto.ml
  115. +1 −1 tactics/autorewrite.ml
  116. +5 −5 tactics/class_tactics.ml4
  117. +4 −4 tactics/eauto.ml4
  118. +2 −2 tactics/elim.ml
  119. +1 −1 tactics/eqdecide.ml4
  120. +9 −9 tactics/eqschemes.ml
  121. +6 −6 tactics/equality.ml
  122. +1 −1 tactics/hipattern.ml4
  123. +2 −2 tactics/inv.ml
  124. +1 −1 tactics/leminv.ml
  125. +2 −2 tactics/refine.ml
  126. +1 −1 tactics/rewrite.ml4
  127. +12 −12 tactics/tacinterp.ml
  128. +5 −5 tactics/tacticals.ml
  129. +14 −14 tactics/tactics.ml
  130. +1 −1 tactics/tauto.ml4
  131. +1 −1 tools/coq_makefile.ml
  132. +26 −26 toplevel/command.ml
  133. +1 −1 toplevel/discharge.ml
  134. +2 −2 toplevel/himsg.ml
  135. +5 −5 toplevel/indschemes.ml
  136. +8 −8 toplevel/lemmas.ml
  137. +8 −8 toplevel/metasyntax.ml
  138. +10 −10 toplevel/obligations.ml
  139. +7 −7 toplevel/record.ml
  140. +14 −14 toplevel/vernacentries.ml
View
@@ -149,20 +149,20 @@ let canonical_path_name p =
let find_logical_path phys_dir =
let phys_dir = canonical_path_name phys_dir in
- match list_filter2 (fun p d -> p = phys_dir) !load_paths with
+ match List.filter2 (fun p d -> p = phys_dir) !load_paths with
| _,[dir] -> dir
| _,[] -> default_root_prefix
| _,l -> anomaly ("Two logical paths are associated to "^phys_dir)
let remove_load_path dir =
- load_paths := list_filter2 (fun p d -> p <> dir) !load_paths
+ load_paths := List.filter2 (fun p d -> p <> dir) !load_paths
let add_load_path (phys_path,coq_path) =
if !Flags.debug then
ppnl (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++
str phys_path);
let phys_path = canonical_path_name phys_path in
- match list_filter2 (fun p d -> p = phys_path) !load_paths with
+ match List.filter2 (fun p d -> p = phys_path) !load_paths with
| _,[dir] ->
if coq_path <> dir
(* If this is not the default -I . to coqtop *)
@@ -185,7 +185,7 @@ let add_load_path (phys_path,coq_path) =
| _ -> anomaly ("Two logical paths are associated to "^phys_path)
let load_paths_of_dir_path dir =
- fst (list_filter2 (fun p d -> d = dir) !load_paths)
+ fst (List.filter2 (fun p d -> d = dir) !load_paths)
(************************************************************************)
(*s Locate absolute or partially qualified library names in the path *)
View
@@ -7,6 +7,7 @@ Loc
Segmenttree
Unicodetable
Errors
+CList
Util
Option
Hashcons
View
@@ -370,7 +370,7 @@ let rec compact_constr (lg, subs as s) c k =
match c with
Rel i ->
if i < k then c,s else
- (try Rel (k + lg - list_index (i-k+1) subs), (lg,subs)
+ (try Rel (k + lg - List.index (i-k+1) subs), (lg,subs)
with Not_found -> Rel (k+lg), (lg+1, (i-k+1)::subs))
| (Sort _|Var _|Meta _|Ind _|Const _|Construct _) -> c,s
| Evar(ev,v) ->
@@ -648,7 +648,7 @@ let rec get_args n tys f e stk =
let eargs = Array.sub l n (na-n) in
(Inl (subs_cons(args,e)), Zapp eargs :: s)
else (* more lambdas *)
- let etys = list_skipn na tys in
+ let etys = List.skipn na tys in
get_args (n-na) etys f (subs_cons(l,e)) s
| _ -> (Inr {norm=Cstr;term=FLambda(n,tys,f,e)}, stk)
@@ -546,7 +546,7 @@ let subst_rel_declaration sub (id,copt,t as x) =
let t' = subst_mps sub t in
if copt == copt' & t == t' then x else (id,copt',t')
-let subst_rel_context sub = list_smartmap (subst_rel_declaration sub)
+let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
type recarg =
| Norec
View
@@ -331,7 +331,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs =
recursive parameters *)
let check_rec_par (env,n,_,_) hyps nrecp largs =
- let (lpar,_) = list_chop nrecp largs in
+ let (lpar,_) = List.chop nrecp largs in
let rec find index =
function
| ([],_) -> ()
@@ -355,7 +355,7 @@ let abstract_mind_lc env ntyps npars lc =
lc
else
let make_abs =
- list_tabulate
+ List.tabulate
(function i -> lambda_implicit_lift npars (Rel (i+1))) ntyps
in
Array.map (substl make_abs) lc
@@ -432,7 +432,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc
let auxnpar = mib.mind_nparams_rec in
let nonrecpar = mib.mind_nparams - auxnpar in
let (lpar,auxlargs) =
- try list_chop auxnpar largs
+ try List.chop auxnpar largs
with Failure _ -> raise (IllFormedInd (LocalNonPos n)) in
(* If the inductive appears in the args (non params) then the
definition is not positive. *)
@@ -514,7 +514,7 @@ let check_positivity env_ar mind params nrecp inds =
let lparams = rel_context_length params in
let check_one i mip =
let ra_env =
- list_tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in
+ List.tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in
let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
check_positivity_one ienv params nrecp (mind,i) mip.mind_nf_lc
in
View
@@ -58,7 +58,7 @@ let inductive_params (mib,_) = mib.mind_nparams
let ind_subst mind mib =
let ntypes = mib.mind_ntypes in
let make_Ik k = Ind (mind,ntypes-k-1) in
- list_tabulate make_Ik ntypes
+ List.tabulate make_Ik ntypes
(* Instantiate inductives in constructor type *)
let constructor_instantiate mind mib c =
@@ -255,7 +255,7 @@ let extended_rel_list n hyps =
reln [] 1 hyps
let build_dependent_inductive ind (_,mip) params =
- let realargs,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
+ let realargs,_ = List.chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
applist
(Ind ind,
List.map (lift mip.mind_nrealargs_ctxt) params
@@ -309,7 +309,7 @@ let build_branches_type ind (_,mip as specif) params dep p =
let (args,ccl) = decompose_prod_assum typi in
let nargs = rel_context_length args in
let (_,allargs) = decompose_app ccl in
- let (lparams,vargs) = list_chop (inductive_params specif) allargs in
+ let (lparams,vargs) = List.chop (inductive_params specif) allargs in
let cargs =
if dep then
let cstr = ith_constructor_of_inductive ind (i+1) in
@@ -331,7 +331,7 @@ let build_case_type dep p c realargs =
let type_case_branches env (ind,largs) (p,pj) c =
let specif = lookup_mind_specif env ind in
let nparams = inductive_params specif in
- let (params,realargs) = list_chop nparams largs in
+ let (params,realargs) = List.chop nparams largs in
let dep = is_correct_arity env c (p,pj) ind specif params in
let lc = build_branches_type ind specif params dep p in
let ty = build_case_type dep p c realargs in
@@ -444,7 +444,7 @@ let push_var renv (x,ty,spec) =
genv = spec:: renv.genv }
let assign_var_spec renv (i,spec) =
- { renv with genv = list_assign renv.genv (i-1) spec }
+ { renv with genv = List.assign renv.genv (i-1) spec }
let push_var_renv renv (x,ty) =
push_var renv (x,ty,Lazy.lazy_from_val Not_subterm)
@@ -527,7 +527,7 @@ let branches_specif renv c_spec ci =
vra
| Dead_code -> Array.create nca Dead_code
| _ -> Array.create nca Not_subterm) in
- list_tabulate (fun j -> lazy (Lazy.force lvra).(j)) nca)
+ List.tabulate (fun j -> lazy (Lazy.force lvra).(j)) nca)
car
(* [subterm_specif renv t] computes the recursive structure of [t] and
@@ -871,7 +871,7 @@ let check_one_cofix env nbfix def deftype =
let lra = vlra.(i-1) in
let mI = inductive_of_constructor cstr_kn in
let (mib,mip) = lookup_mind_specif env mI in
- let realargs = list_skipn mib.mind_nparams args in
+ let realargs = List.skipn mib.mind_nparams args in
let rec process_args_of_constr = function
| (t::lr), (rar::lrar) ->
if rar = mk_norec then
View
@@ -346,7 +346,7 @@ let map_context f l =
if body_o' == body_o && typ' == typ then decl else
(n, body_o', typ')
in
- list_smartmap map_decl l
+ List.smartmap map_decl l
let map_rel_context = map_context
View
@@ -8,6 +8,7 @@ Loc
Segmenttree
Unicodetable
Errors
+CList
Util
Bigint
Hashcons
@@ -8,6 +8,7 @@ Loc
Segmenttree
Unicodetable
Errors
+CList
Util
Bigint
Hashcons
@@ -53,7 +53,7 @@ let rec extract_signature = function
let check_unicity s l =
let l' = List.map (fun (l,_) -> extract_signature l) l in
- if not (Util.list_distinct l') then
+ if not (Util.List.distinct l') then
Pp.msg_warning
(strbrk ("Two distinct rules of tactic entry "^s^" have the same "^
"non-terminals in the same order: put them in distinct tactic entries"))
@@ -152,10 +152,10 @@ let rec possibly_empty_subentries loc = function
else possibly_empty_subentries loc l
let possibly_atomic loc prods =
- let l = list_map_filter (function
+ let l = List.map_filter (function
| GramTerminal s :: l, _ -> Some (s,l)
| _ -> None) prods in
- possibly_empty_subentries loc (list_factorize_left l)
+ possibly_empty_subentries loc (List.factorize_left l)
let declare_tactic loc s cl =
let se = mlexpr_of_string s in
@@ -30,7 +30,7 @@ let rec make_let e = function
let check_unicity s l =
let l' = List.map (fun (_,l,_) -> extract_signature l) l in
- if not (Util.list_distinct l') then
+ if not (Util.List.distinct l') then
Pp.msg_warning
(strbrk ("Two distinct rules of entry "^s^" have the same "^
"non-terminals in the same order: put them in distinct vernac entries"))
View
@@ -1292,7 +1292,7 @@ let load_file handler f =
try
Minilib.log "Loading file starts";
let is_f = CUnix.same_file f in
- if not (Util.list_fold_left_i
+ if not (Util.List.fold_left_i
(fun i found x -> if found then found else
let {analyzed_view=av} = x in
(match av#filename with
View
@@ -55,7 +55,7 @@ class command_window coqtop =
let remove_cb () =
let index = notebook#current_page in
let () = notebook#remove_page index in
- views := Util.list_filter_i (fun i x -> i <> index) !views
+ views := Util.List.filter_i (fun i x -> i <> index) !views
in
let _ =
toolbar#insert_button
View
@@ -16,14 +16,14 @@ object(self)
(* XXX - Temporary hack to compile with archaic lablgtk *)
ignore (super#append_page ?tab_label ?menu_label page);
let real_pos = super#page_num page in
- let lower,higher = Util.list_chop real_pos term_list in
+ let lower,higher = Util.List.chop real_pos term_list in
term_list <- lower@[term]@higher;
real_pos
(* XXX - Temporary hack to compile with archaic lablgtk
method insert_term ?(build=default_build) ?pos (term:'a) =
let tab_label,menu_label,page = build term in
let real_pos = super#insert_page ?tab_label ?menu_label ?pos page in
- let lower,higher = Util.list_chop real_pos term_list in
+ let lower,higher = Util.List.chop real_pos term_list in
term_list <- lower@[term]@higher;
real_pos
*)
@@ -32,26 +32,26 @@ object(self)
(* XXX - Temporary hack to compile with archaic lablgtk *)
ignore (super#prepend_page ?tab_label ?menu_label page);
let real_pos = super#page_num page in
- let lower,higher = Util.list_chop real_pos term_list in
+ let lower,higher = Util.List.chop real_pos term_list in
term_list <- lower@[term]@higher;
real_pos
method set_term (term:'a) =
let tab_label,menu_label,page = make_page term in
let real_pos = super#current_page in
- term_list <- Util.list_map_i (fun i x -> if i = real_pos then term else x) 0 term_list;
+ term_list <- Util.List.map_i (fun i x -> if i = real_pos then term else x) 0 term_list;
super#set_page ?tab_label ?menu_label page
method get_nth_term i =
List.nth term_list i
method term_num p =
- Util.list_index0 p term_list
+ Util.List.index0 p term_list
method pages = term_list
method remove_page index =
- term_list <- Util.list_filter_i (fun i x -> if i = index then kill_page x; i <> index) term_list;
+ term_list <- Util.List.filter_i (fun i x -> if i = index then kill_page x; i <> index) term_list;
super#remove_page index
method current_term =
View
@@ -100,7 +100,7 @@ let mode_tactic sel_cb (proof:GText.view) goals hints = match goals with
proof#buffer#insert (goal_str i goals_cnt);
proof#buffer#insert (g ^ "\n")
in
- let () = Util.list_fold_left_i fold_goal 2 () rem_goals in
+ let () = Util.List.fold_left_i fold_goal 2 () rem_goals in
ignore(proof#buffer#place_cursor
~where:(proof#buffer#end_iter#backward_to_tag_toggle
@@ -75,7 +75,7 @@ let local_binder_loc = function
let local_binders_loc bll =
if bll = [] then Loc.ghost else
- Loc.merge (local_binder_loc (List.hd bll)) (local_binder_loc (list_last bll))
+ Loc.merge (local_binder_loc (List.hd bll)) (local_binder_loc (List.last bll))
(** Pseudo-constructors *)
@@ -257,7 +257,7 @@ let is_same_type c d =
(* mapping patterns to cases_pattern_expr *)
let add_patt_for_params ind l =
- Util.list_addn (fst (Inductiveops.inductive_nargs ind)) (CPatAtom (Loc.ghost,None)) l
+ Util.List.addn (fst (Inductiveops.inductive_nargs ind)) (CPatAtom (Loc.ghost,None)) l
let drop_implicits_in_patt cst nb_expl args =
let impl_st = (implicits_of_global cst) in
@@ -276,7 +276,7 @@ let drop_implicits_in_patt cst nb_expl args =
in
if nb_expl = 0 then aux impl_data
else
- let imps = list_skipn_at_least nb_expl (select_stronger_impargs impl_st) in
+ let imps = List.skipn_at_least nb_expl (select_stronger_impargs impl_st) in
impls_fit [] (imps,args)
let has_curly_brackets ntn =
@@ -355,7 +355,7 @@ let pattern_printable_in_both_syntax (ind,_ as c) =
let nb_params = Inductiveops.inductive_nparams ind in
List.exists (fun (_,impls) ->
(List.length impls >= nb_params) &&
- let params,args = Util.list_chop nb_params impls in
+ let params,args = Util.List.chop nb_params impls in
(List.for_all is_status_implicit params)&&(List.for_all (fun x -> not (is_status_implicit x)) args)
) impl_st
@@ -570,8 +570,8 @@ let explicitize loc inctx impl (cf,f) args =
let f' = match f with CRef f -> f | _ -> assert false in
CAppExpl (loc,(ip,f'),args)
else
- let (args1,args2) = list_chop i args in
- let (impl1,impl2) = if impl=[] then [],[] else list_chop i impl in
+ let (args1,args2) = List.chop i args in
+ let (impl1,impl2) = if impl=[] then [],[] else List.chop i impl in
let args1 = exprec 1 (args1,impl1) in
let args2 = exprec (i+1) (args2,impl2) in
CApp (loc,(Some (List.length args1),f),args1@args2)
@@ -617,7 +617,7 @@ let rec remove_coercions inctx = function
(try match Classops.hide_coercion r with
| Some n when n < nargs && (inctx or n+1 < nargs) ->
(* We skip a coercion *)
- let l = list_skipn n args in
+ let l = List.skipn n args in
let (a,l) = match l with a::l -> (a,l) | [] -> assert false in
(* Recursively remove the head coercions *)
let a' = remove_coercions true a in
@@ -893,17 +893,17 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
let (t,args,argsscopes,argsimpls) = match t,n with
| GApp (_,f,args), Some n
when List.length args >= n ->
- let args1, args2 = list_chop n args in
+ let args1, args2 = List.chop n args in
let subscopes, impls =
match f with
| GRef (_,ref) ->
let subscopes =
- try list_skipn n (find_arguments_scope ref) with _ -> [] in
+ try List.skipn n (find_arguments_scope ref) with _ -> [] in
let impls =
let impls =
select_impargs_size
(List.length args) (implicits_of_global ref) in
- try list_skipn n impls with _ -> [] in
+ try List.skipn n impls with _ -> [] in
subscopes,impls
| _ ->
[], [] in
Oops, something went wrong.

0 comments on commit f8394a5

Please sign in to comment.