summaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/cc/ccalgo.ml25
-rw-r--r--plugins/cc/cctac.ml34
-rw-r--r--plugins/extraction/common.ml76
-rw-r--r--plugins/extraction/extract_env.ml30
-rw-r--r--plugins/extraction/extraction.ml25
-rw-r--r--plugins/extraction/haskell.ml4
-rw-r--r--plugins/extraction/mlutil.ml12
-rw-r--r--plugins/extraction/mlutil.mli5
-rw-r--r--plugins/extraction/modutil.ml44
-rw-r--r--plugins/extraction/table.ml113
-rw-r--r--plugins/extraction/table.mli5
-rw-r--r--plugins/funind/g_indfun.ml46
-rw-r--r--plugins/funind/indfun.ml4
-rw-r--r--plugins/micromega/coq_micromega.ml2
-rw-r--r--plugins/subtac/subtac.ml4
-rw-r--r--plugins/subtac/subtac_classes.ml8
-rw-r--r--plugins/subtac/subtac_command.ml4
-rw-r--r--plugins/subtac/subtac_obligations.ml2
18 files changed, 238 insertions, 165 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 4171aceb..82b4143e 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ccalgo.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: ccalgo.ml 13409 2010-09-13 07:53:13Z soubiran $ *)
(* This file implements the basic congruence-closure algorithm by *)
(* Downey,Sethi and Tarjan. *)
@@ -339,6 +339,28 @@ and make_app l=function
Appli (s1,s2)->make_app ((constr_of_term s2)::l) s1
| other -> applistc (constr_of_term other) l
+let rec canonize_name c =
+ let func = canonize_name in
+ match kind_of_term c with
+ | Const kn ->
+ let canon_const = constant_of_kn (canonical_con kn) in
+ (mkConst canon_const)
+ | Ind (kn,i) ->
+ let canon_mind = mind_of_kn (canonical_mind kn) in
+ (mkInd (canon_mind,i))
+ | Construct ((kn,i),j) ->
+ let canon_mind = mind_of_kn (canonical_mind kn) in
+ mkConstruct ((canon_mind,i),j)
+ | Prod (na,t,ct) ->
+ mkProd (na,func t, func ct)
+ | Lambda (na,t,ct) ->
+ mkLambda (na, func t,func ct)
+ | LetIn (na,b,t,ct) ->
+ mkLetIn (na, func b,func t,func ct)
+ | App (ct,l) ->
+ mkApp (func ct,array_smartmap func l)
+ | _ -> c
+
(* rebuild a term from a pattern and a substitution *)
let build_subst uf subst =
@@ -366,6 +388,7 @@ let rec add_term state t=
Not_found ->
let b=next uf in
let typ = pf_type_of state.gls (constr_of_term t) in
+ let typ = canonize_name typ in
let new_node=
match t with
Symb _ | Product (_,_) ->
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index b7358121..ca1a9085 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: cctac.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: cctac.ml 13409 2010-09-13 07:53:13Z soubiran $ *)
(* This file is the interface between the c-c algorithm and Coq *)
@@ -74,11 +74,21 @@ let rec decompose_term env sigma t=
decompose_term env sigma a),
decompose_term env sigma b)
| Construct c->
- let (oib,_)=Global.lookup_inductive (fst c) in
- let nargs=mis_constructor_nargs_env env c in
- Constructor {ci_constr=c;
+ let (mind,i_ind),i_con = c in
+ let canon_mind = mind_of_kn (canonical_mind mind) in
+ let canon_ind = canon_mind,i_ind in
+ let (oib,_)=Global.lookup_inductive (canon_ind) in
+ let nargs=mis_constructor_nargs_env env (canon_ind,i_con) in
+ Constructor {ci_constr= (canon_ind,i_con);
ci_arity=nargs;
ci_nhyps=nargs-oib.mind_nparams}
+ | Ind c ->
+ let mind,i_ind = c in
+ let canon_mind = mind_of_kn (canonical_mind mind) in
+ let canon_ind = canon_mind,i_ind in (Symb (mkInd canon_ind))
+ | Const c ->
+ let canon_const = constant_of_kn (canonical_con c) in
+ (Symb (mkConst canon_const))
| _ ->if closed0 t then (Symb t) else raise Not_found
(* decompose equality in members and type *)
@@ -106,7 +116,7 @@ let rec pattern_of_constr env sigma c =
| Prod (_,a,_b) when not (dependent (mkRel 1) _b) ->
let b =pop _b in
let pa,sa = pattern_of_constr env sigma a in
- let pb,sb = pattern_of_constr env sigma (pop b) in
+ let pb,sb = pattern_of_constr env sigma b in
let sort_b = sf_of env sigma b in
let sort_a = sf_of env sigma a in
PApp(Product (sort_a,sort_b),
@@ -143,27 +153,27 @@ let patterns_of_constr env sigma nrels term=
let rec quantified_atom_of_constr env sigma nrels term =
match kind_of_term (whd_delta env term) with
- Prod (_,atom,ff) ->
+ Prod (id,atom,ff) ->
if eq_constr ff (Lazy.force _False) then
let patts=patterns_of_constr env sigma nrels atom in
`Nrule patts
- else
- quantified_atom_of_constr env sigma (succ nrels) ff
- | _ ->
+ else
+ quantified_atom_of_constr (Environ.push_rel (id,None,atom) env) sigma (succ nrels) ff
+ | _ ->
let patts=patterns_of_constr env sigma nrels term in
`Rule patts
let litteral_of_constr env sigma term=
match kind_of_term (whd_delta env term) with
- | Prod (_,atom,ff) ->
+ | Prod (id,atom,ff) ->
if eq_constr ff (Lazy.force _False) then
match (atom_of_constr env sigma atom) with
`Eq(t,a,b) -> `Neq(t,a,b)
| `Other(p) -> `Nother(p)
else
begin
- try
- quantified_atom_of_constr env sigma 1 ff
+ try
+ quantified_atom_of_constr (Environ.push_rel (id,None,atom) env) sigma 1 ff
with Not_found ->
`Other (decompose_term env sigma term)
end
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index ca72f873..8dc512fa 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: common.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: common.ml 13420 2010-09-16 15:47:08Z letouzey $ i*)
open Pp
open Util
@@ -177,6 +177,10 @@ let mktable autoclean =
let add_mpfiles_content,get_mpfiles_content,clear_mpfiles_content =
mktable false
+let get_mpfiles_content mp =
+ try get_mpfiles_content mp
+ with Not_found -> failwith "get_mpfiles_content"
+
(*s The list of external modules that will be opened initially *)
let mpfiles_add, mpfiles_mem, mpfiles_list, mpfiles_clear =
@@ -223,11 +227,13 @@ let pop_visible, push_visible, get_visible =
let vis = ref [] in
register_cleanup (fun () -> vis := []);
let pop () =
- let v = List.hd !vis in
- (* we save the 1st-level-content of MPfile for later use *)
- if get_phase () = Impl && modular () && is_modfile v.mp
- then add_mpfiles_content v.mp v.content;
- vis := List.tl !vis
+ match !vis with
+ | [] -> assert false
+ | v :: vl ->
+ vis := vl;
+ (* we save the 1st-level-content of MPfile for later use *)
+ if get_phase () = Impl && modular () && is_modfile v.mp
+ then add_mpfiles_content v.mp v.content
and push mp mps =
vis := { mp = mp; params = mps; content = Hashtbl.create 97 } :: !vis
and get () = !vis
@@ -306,8 +312,8 @@ let rec mp_renaming_fun mp = match mp with
let s = modular_rename Mod (id_of_mbid mbid) in
if not (params_ren_mem mp) then [s]
else let i,_,_ = repr_mbid mbid in [s^"__"^string_of_int i]
- | MPfile _ when not (modular ()) -> assert false (* see [at_toplevel] above *)
| MPfile _ ->
+ assert (modular ()); (* see [at_toplevel] above *)
assert (get_phase () = Pre);
let current_mpfile = (list_last (get_visible ())).mp in
if mp <> current_mpfile then mpfiles_add mp;
@@ -402,27 +408,28 @@ let visible_clash_dbg mp0 ks =
let opened_libraries () =
if not (modular ()) then []
else
- let used = mpfiles_list () in
- let rec check_elsewhere avoid = function
- | [] -> []
- | mp :: mpl ->
- let clash s = Hashtbl.mem (get_mpfiles_content mp) (Mod,s) in
- if List.exists clash avoid
- then check_elsewhere avoid mpl
- else mp :: check_elsewhere (string_of_modfile mp :: avoid) mpl
+ let used_files = mpfiles_list () in
+ let used_ks = List.map (fun mp -> Mod,string_of_modfile mp) used_files in
+ (* By default, we open all used files. Ambiguities will be resolved later
+ by using qualified names. Nonetheless, we don't open any file A that
+ contains an immediate submodule A.B hiding another file B : otherwise,
+ after such an open, there's no unambiguous way to refer to objects of B. *)
+ let to_open =
+ List.filter
+ (fun mp ->
+ not (List.exists (Hashtbl.mem (get_mpfiles_content mp)) used_ks))
+ used_files
in
- let opened = check_elsewhere [] used in
mpfiles_clear ();
- List.iter mpfiles_add opened;
- opened
+ List.iter mpfiles_add to_open;
+ mpfiles_list ()
(*s On-the-fly qualification issues for both monolithic or modular extraction. *)
-(* First, a function that factorize the printing of both [global_reference]
- and module names for ocaml. When [k=Mod] then [olab=None], otherwise it
- contains the label of the reference to print.
- [rls] is the string list giving the qualified name, short name at the end.
- Invariant: [List.length rls >= 2], simpler situations are handled elsewhere. *)
+(* [pp_ocaml_gen] below is a function that factorize the printing of both
+ [global_reference] and module names for ocaml. When [k=Mod] then [olab=None],
+ otherwise it contains the label of the reference to print.
+ [rls] is the string list giving the qualified name, short name at the end. *)
(* In Coq, we can qualify [M.t] even if we are inside [M], but in Ocaml we
cannot do that. So, if [t] gets hidden and we need a long name for it,
@@ -471,18 +478,21 @@ let pp_ocaml_bound base rls =
(* [pp_ocaml_extern] : [mp] isn't local, it is defined in another [MPfile]. *)
let pp_ocaml_extern k base rls = match rls with
- | [] | [_] -> assert false
+ | [] -> assert false
| base_s :: rls' ->
- let k's = fstlev_ks k rls' in
- if modular () && (mpfiles_mem base) &&
- (not (mpfiles_clash base k's)) &&
- (not (visible_clash base k's))
- then (* Standard situation of an object in another file: *)
- (* Thanks to the "open" of this file we remove its name *)
+ if (not (modular ())) (* Pseudo qualification with "" *)
+ || (rls' = []) (* Case of a file A.v used as a module later *)
+ || (not (mpfiles_mem base)) (* Module not opened *)
+ || (mpfiles_clash base (fstlev_ks k rls')) (* Conflict in opened files *)
+ || (visible_clash base (fstlev_ks k rls')) (* Local conflict *)
+ then
+ (* We need to fully qualify. Last clash situation is unsupported *)
+ match visible_clash_dbg base (Mod,base_s) with
+ | None -> dottify rls
+ | Some (mp,l) -> error_module_clash base (MPdot (mp,l))
+ else
+ (* Standard situation : object in an opened file *)
dottify rls'
- else match visible_clash_dbg base (Mod,base_s) with
- | None -> dottify rls
- | Some (mp,l) -> error_module_clash base (MPdot (mp,l))
(* [pp_ocaml_gen] : choosing between [pp_ocaml_extern] or [pp_ocaml_extern] *)
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 58d8fcb1..c5929392 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: extract_env.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: extract_env.ml 13420 2010-09-16 15:47:08Z letouzey $ i*)
open Term
open Declarations
@@ -69,7 +69,7 @@ module type VISIT = sig
(* Add kernel_name / constant / reference / ... in the visit lists.
These functions silently add the mp of their arg in the mp list *)
- val add_kn : mutual_inductive -> unit
+ val add_ind : mutual_inductive -> unit
val add_con : constant -> unit
val add_ref : global_reference -> unit
val add_decl_deps : ml_decl -> unit
@@ -77,31 +77,35 @@ module type VISIT = sig
(* Test functions:
is a particular object a needed dependency for the current extraction ? *)
- val needed_kn : mutual_inductive -> bool
+ val needed_ind : mutual_inductive -> bool
val needed_con : constant -> bool
val needed_mp : module_path -> bool
end
module Visit : VISIT = struct
(* What used to be in a single KNset should now be split into a KNset
- (for inductives and modules names) and a Cset for constants
+ (for inductives and modules names) and a Cset_env for constants
(and still the remaining MPset) *)
type must_visit =
- { mutable kn : Mindset.t; mutable con : Cset.t; mutable mp : MPset.t }
+ { mutable ind : KNset.t; mutable con : KNset.t; mutable mp : MPset.t }
(* the imperative internal visit lists *)
- let v = { kn = Mindset.empty ; con = Cset.empty ; mp = MPset.empty }
+ let v = { ind = KNset.empty ; con = KNset.empty ; mp = MPset.empty }
(* the accessor functions *)
- let reset () = v.kn <- Mindset.empty; v.con <- Cset.empty; v.mp <- MPset.empty
- let needed_kn kn = Mindset.mem kn v.kn
- let needed_con c = Cset.mem c v.con
+ let reset () = v.ind <- KNset.empty; v.con <- KNset.empty; v.mp <- MPset.empty
+ let needed_ind i = KNset.mem (user_mind i) v.ind
+ let needed_con c = KNset.mem (user_con c) v.con
let needed_mp mp = MPset.mem mp v.mp
let add_mp mp =
check_loaded_modfile mp; v.mp <- MPset.union (prefixes_mp mp) v.mp
- let add_kn kn = v.kn <- Mindset.add kn v.kn; add_mp (mind_modpath kn)
- let add_con c = v.con <- Cset.add c v.con; add_mp (con_modpath c)
+ let add_ind i =
+ let kn = user_mind i in
+ v.ind <- KNset.add kn v.ind; add_mp (modpath kn)
+ let add_con c =
+ let kn = user_con c in
+ v.con <- KNset.add kn v.con; add_mp (modpath kn)
let add_ref = function
| ConstRef c -> add_con c
- | IndRef (kn,_) | ConstructRef ((kn,_),_) -> add_kn kn
+ | IndRef (ind,_) | ConstructRef ((ind,_),_) -> add_ind ind
| VarRef _ -> assert false
let add_decl_deps = decl_iter_references add_ref add_ref add_ref
let add_spec_deps = spec_iter_references add_ref add_ref add_ref
@@ -280,7 +284,7 @@ let rec extract_sfb env mp all = function
let ms = extract_sfb env mp all msb in
let kn = make_kn mp empty_dirpath l in
let mind = mind_of_kn kn in
- let b = Visit.needed_kn mind in
+ let b = Visit.needed_ind mind in
if all || b then
let d = Dind (kn, extract_inductive env mind) in
if (not b) && (logical_decl d) then ms
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 057057d1..b615955f 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: extraction.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: extraction.ml 13427 2010-09-17 17:37:52Z letouzey $ i*)
(*i*)
open Util
@@ -817,6 +817,18 @@ let rec decomp_lams_eta_n n m env c t =
let eta_args = List.rev_map mkRel (interval 1 d) in
rels, applist (lift d c,eta_args)
+(* Let's try to identify some situation where extracted code
+ will allow generalisation of type variables *)
+
+let rec gentypvar_ok c = match kind_of_term c with
+ | Lambda _ | Const _ -> true
+ | App (c,v) ->
+ (* if all arguments are variables, these variables will
+ disappear after extraction (see [empty_s] below) *)
+ array_for_all isRel v && gentypvar_ok c
+ | Cast (c,_,_) -> gentypvar_ok c
+ | _ -> false
+
(*s From a constant to a ML declaration. *)
let extract_std_constant env kn body typ =
@@ -846,6 +858,17 @@ let extract_std_constant env kn body typ =
then decompose_lam_n m body
else decomp_lams_eta_n n m env body typ
in
+ (* Should we do one eta-expansion to avoid non-generalizable '_a ? *)
+ let rels, c =
+ let n = List.length rels in
+ let s,s' = list_split_at n s in
+ let k = sign_kind s in
+ let empty_s = (k = EmptySig || k = SafeLogicalSig) in
+ if lang () = Ocaml && empty_s && not (gentypvar_ok c)
+ && s' <> [] && type_maxvar t <> 0
+ then decomp_lams_eta_n (n+1) n env body typ
+ else rels,c
+ in
let n = List.length rels in
let s = list_firstn n s in
let l,l' = list_split_at n l in
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 57b7c365..29d3da4d 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: haskell.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: haskell.ml 13414 2010-09-14 13:28:15Z glondu $ i*)
(*s Production of Haskell syntax. *)
@@ -297,7 +297,7 @@ let pp_decl = function
try
let ids,s = find_type_custom r in
prlist (fun id -> str (id^" ")) ids ++ str "=" ++ spc () ++ str s
- with not_found ->
+ with Not_found ->
prlist (fun id -> pr_id id ++ str " ") l ++
if t = Taxiom then str "= () -- AXIOM TO BE REALIZED\n"
else str "=" ++ spc () ++ pp_type false l t
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 745a78fe..a079aacc 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: mlutil.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: mlutil.ml 13420 2010-09-16 15:47:08Z letouzey $ i*)
(*i*)
open Pp
@@ -656,10 +656,10 @@ let rec tmp_head_lams = function
let rec ast_glob_subst s t = match t with
| MLapp ((MLglob ((ConstRef kn) as refe)) as f, a) ->
let a = List.map (fun e -> tmp_head_lams (ast_glob_subst s e)) a in
- (try linear_beta_red a (Refmap.find refe s)
+ (try linear_beta_red a (Refmap'.find refe s)
with Not_found -> MLapp (f, a))
| MLglob ((ConstRef kn) as refe) ->
- (try Refmap.find refe s with Not_found -> t)
+ (try Refmap'.find refe s with Not_found -> t)
| _ -> ast_map (ast_glob_subst s) t
@@ -1259,7 +1259,7 @@ let con_of_string s =
| [] -> assert false
let manual_inline_set =
- List.fold_right (fun x -> Cset.add (con_of_string x))
+ List.fold_right (fun x -> Cset_env.add (con_of_string x))
[ "Coq.Init.Wf.well_founded_induction_type";
"Coq.Init.Wf.well_founded_induction";
"Coq.Init.Wf.Acc_iter";
@@ -1271,10 +1271,10 @@ let manual_inline_set =
"Coq.Init.Logic.eq_rect_r";
"Coq.Init.Specif.proj1_sig";
]
- Cset.empty
+ Cset_env.empty
let manual_inline = function
- | ConstRef c -> Cset.mem c manual_inline_set
+ | ConstRef c -> Cset_env.mem c manual_inline_set
| _ -> false
(* If the user doesn't say he wants to keep [t], we inline in two cases:
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index d6b85f12..d2ac48ea 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -6,13 +6,14 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: mlutil.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: mlutil.mli 13420 2010-09-16 15:47:08Z letouzey $ i*)
open Util
open Names
open Term
open Libnames
open Miniml
+open Table
(*s Utility functions over ML types with meta. *)
@@ -108,7 +109,7 @@ val ast_lift : int -> ml_ast -> ml_ast
val ast_pop : ml_ast -> ml_ast
val ast_subst : ml_ast -> ml_ast -> ml_ast
-val ast_glob_subst : ml_ast Refmap.t -> ml_ast -> ml_ast
+val ast_glob_subst : ml_ast Refmap'.t -> ml_ast -> ml_ast
val normalize : ml_ast -> ml_ast
val optimize_fix : ml_ast -> ml_ast
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 15145344..b4334750 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: modutil.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: modutil.ml 13420 2010-09-16 15:47:08Z letouzey $ i*)
open Names
open Declarations
@@ -217,45 +217,25 @@ let get_decl_in_structure r struc =
let dfix_to_mlfix rv av i =
let rec make_subst n s =
if n < 0 then s
- else make_subst (n-1) (Refmap.add rv.(n) (n+1) s)
+ else make_subst (n-1) (Refmap'.add rv.(n) (n+1) s)
in
- let s = make_subst (Array.length rv - 1) Refmap.empty
+ let s = make_subst (Array.length rv - 1) Refmap'.empty
in
let rec subst n t = match t with
| MLglob ((ConstRef kn) as refe) ->
- (try MLrel (n + (Refmap.find refe s)) with Not_found -> t)
+ (try MLrel (n + (Refmap'.find refe s)) with Not_found -> t)
| _ -> ast_map_lift subst n t
in
let ids = Array.map (fun r -> id_of_label (label_of_r r)) rv in
let c = Array.map (subst 0) av
in MLfix(i, ids, c)
-let rec optim to_appear s = function
- | [] -> []
- | (Dtype (r,_,Tdummy _) | Dterm(r,MLdummy,_)) as d :: l ->
- if List.mem r to_appear
- then d :: (optim to_appear s l)
- else optim to_appear s l
- | Dterm (r,t,typ) :: l ->
- let t = normalize (ast_glob_subst !s t) in
- let i = inline r t in
- if i then s := Refmap.add r t !s;
- if not i || modular () || List.mem r to_appear
- then
- let d = match optimize_fix t with
- | MLfix (0, _, [|c|]) ->
- Dfix ([|r|], [|ast_subst (MLglob r) c|], [|typ|])
- | t -> Dterm (r, t, typ)
- in d :: (optim to_appear s l)
- else optim to_appear s l
- | d :: l -> d :: (optim to_appear s l)
-
let rec optim_se top to_appear s = function
| [] -> []
| (l,SEdecl (Dterm (r,a,t))) :: lse ->
let a = normalize (ast_glob_subst !s a) in
let i = inline r a in
- if i then s := Refmap.add r a !s;
+ if i then s := Refmap'.add r a !s;
if top && i && not (modular ()) && not (List.mem r to_appear)
then optim_se top to_appear s lse
else
@@ -271,7 +251,7 @@ let rec optim_se top to_appear s = function
let fake_body = MLfix (0,[||],[||]) in
for i = 0 to Array.length rv - 1 do
if inline rv.(i) fake_body
- then s := Refmap.add rv.(i) (dfix_to_mlfix rv av i) !s
+ then s := Refmap'.add rv.(i) (dfix_to_mlfix rv av i) !s
else all := false
done;
if !all && top && not (modular ())
@@ -302,11 +282,11 @@ let base_r = function
| _ -> assert false
let reset_needed, add_needed, found_needed, is_needed =
- let needed = ref Refset.empty in
- ((fun l -> needed := Refset.empty),
- (fun r -> needed := Refset.add (base_r r) !needed),
- (fun r -> needed := Refset.remove (base_r r) !needed),
- (fun r -> Refset.mem (base_r r) !needed))
+ let needed = ref Refset'.empty in
+ ((fun l -> needed := Refset'.empty),
+ (fun r -> needed := Refset'.add (base_r r) !needed),
+ (fun r -> needed := Refset'.remove (base_r r) !needed),
+ (fun r -> Refset'.mem (base_r r) !needed))
let declared_refs = function
| Dind (kn,_) -> [|IndRef (mind_of_kn kn,0)|]
@@ -361,7 +341,7 @@ let check_implicits = function
| _ -> false
let optimize_struct to_appear struc =
- let subst = ref (Refmap.empty : ml_ast Refmap.t) in
+ let subst = ref (Refmap'.empty : ml_ast Refmap'.t) in
let opt_struc =
List.map (fun (mp,lse) -> (mp, optim_se true to_appear subst lse)) struc
in
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index fd640388..a7e636ff 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: table.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: table.ml 13420 2010-09-16 15:47:08Z letouzey $ i*)
open Names
open Term
@@ -21,6 +21,13 @@ open Util
open Pp
open Miniml
+(** Sets and maps for [global_reference] that do _not_ work modulo
+ name equivalence (otherwise use Refset / Refmap ) *)
+
+module RefOrd = struct type t = global_reference let compare = compare end
+module Refmap' = Map.Make(RefOrd)
+module Refset' = Set.Make(RefOrd)
+
(*S Utilities about [module_path] and [kernel_names] and [global_reference] *)
let occur_kn_in_ref kn = function
@@ -119,37 +126,47 @@ let rec add_labels_mp mp = function
(*s Constants tables. *)
-let terms = ref (Cmap.empty : ml_decl Cmap.t)
-let init_terms () = terms := Cmap.empty
-let add_term kn d = terms := Cmap.add kn d !terms
-let lookup_term kn = Cmap.find kn !terms
+let terms = ref (Cmap_env.empty : ml_decl Cmap_env.t)
+let init_terms () = terms := Cmap_env.empty
+let add_term kn d = terms := Cmap_env.add kn d !terms
+let lookup_term kn = Cmap_env.find kn !terms
-let types = ref (Cmap.empty : ml_schema Cmap.t)
-let init_types () = types := Cmap.empty
-let add_type kn s = types := Cmap.add kn s !types
-let lookup_type kn = Cmap.find kn !types
+let types = ref (Cmap_env.empty : ml_schema Cmap_env.t)
+let init_types () = types := Cmap_env.empty
+let add_type kn s = types := Cmap_env.add kn s !types
+let lookup_type kn = Cmap_env.find kn !types
(*s Inductives table. *)
-let inductives = ref (Mindmap.empty : (mutual_inductive_body * ml_ind) Mindmap.t)
-let init_inductives () = inductives := Mindmap.empty
-let add_ind kn mib ml_ind = inductives := Mindmap.add kn (mib,ml_ind) !inductives
-let lookup_ind kn = Mindmap.find kn !inductives
+let inductives =
+ ref (Mindmap_env.empty : (mutual_inductive_body * ml_ind) Mindmap_env.t)
+let init_inductives () = inductives := Mindmap_env.empty
+let add_ind kn mib ml_ind =
+ inductives := Mindmap_env.add kn (mib,ml_ind) !inductives
+let lookup_ind kn = Mindmap_env.find kn !inductives
(*s Recursors table. *)
+(* NB: here we can use the equivalence between canonical
+ and user constant names : Cset is fine, no need for [Cset_env] *)
+
let recursors = ref Cset.empty
let init_recursors () = recursors := Cset.empty
let add_recursors env kn =
- let make_kn id = make_con (mind_modpath kn) empty_dirpath (label_of_id id) in
+ let mk_con id =
+ make_con_equiv
+ (modpath (user_mind kn))
+ (modpath (canonical_mind kn))
+ empty_dirpath (label_of_id id)
+ in
let mib = Environ.lookup_mind kn env in
Array.iter
(fun mip ->
let id = mip.mind_typename in
- let kn_rec = make_kn (Nameops.add_suffix id "_rec")
- and kn_rect = make_kn (Nameops.add_suffix id "_rect") in
- recursors := Cset.add kn_rec (Cset.add kn_rect !recursors))
+ let c_rec = mk_con (Nameops.add_suffix id "_rec")
+ and c_rect = mk_con (Nameops.add_suffix id "_rect") in
+ recursors := Cset.add c_rec (Cset.add c_rect !recursors))
mib.mind_packets
let is_recursor = function
@@ -158,6 +175,8 @@ let is_recursor = function
(*s Record tables. *)
+(* NB: here, working modulo name equivalence is ok *)
+
let projs = ref (Refmap.empty : int Refmap.t)
let init_projs () = projs := Refmap.empty
let add_projection n kn = projs := Refmap.add (ConstRef kn) n !projs
@@ -166,12 +185,12 @@ let projection_arity r = Refmap.find r !projs
(*s Table of used axioms *)
-let info_axioms = ref Refset.empty
-let log_axioms = ref Refset.empty
-let init_axioms () = info_axioms := Refset.empty; log_axioms := Refset.empty
-let add_info_axiom r = info_axioms := Refset.add r !info_axioms
-let remove_info_axiom r = info_axioms := Refset.remove r !info_axioms
-let add_log_axiom r = log_axioms := Refset.add r !log_axioms
+let info_axioms = ref Refset'.empty
+let log_axioms = ref Refset'.empty
+let init_axioms () = info_axioms := Refset'.empty; log_axioms := Refset'.empty
+let add_info_axiom r = info_axioms := Refset'.add r !info_axioms
+let remove_info_axiom r = info_axioms := Refset'.remove r !info_axioms
+let add_log_axiom r = log_axioms := Refset'.add r !log_axioms
(*s Extraction mode: modular or monolithic *)
@@ -220,7 +239,7 @@ let pr_long_global ref = pr_path (Nametab.path_of_global ref)
let err s = errorlabstrm "Extraction" s
let warning_axioms () =
- let info_axioms = Refset.elements !info_axioms in
+ let info_axioms = Refset'.elements !info_axioms in
if info_axioms = [] then ()
else begin
let s = if List.length info_axioms = 1 then "axiom" else "axioms" in
@@ -229,7 +248,7 @@ let warning_axioms () =
++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global info_axioms)
++ str "." ++ fnl ())
end;
- let log_axioms = Refset.elements !log_axioms in
+ let log_axioms = Refset'.elements !log_axioms in
if log_axioms = [] then ()
else begin
let s = if List.length log_axioms = 1 then "axiom was" else "axioms were"
@@ -457,16 +476,16 @@ let extraction_language x = Lib.add_anonymous_leaf (extr_lang x)
(*s Extraction Inline/NoInline *)
-let empty_inline_table = (Refset.empty,Refset.empty)
+let empty_inline_table = (Refset'.empty,Refset'.empty)
let inline_table = ref empty_inline_table
-let to_inline r = Refset.mem r (fst !inline_table)
+let to_inline r = Refset'.mem r (fst !inline_table)
-let to_keep r = Refset.mem r (snd !inline_table)
+let to_keep r = Refset'.mem r (snd !inline_table)
let add_inline_entries b l =
- let f b = if b then Refset.add else Refset.remove in
+ let f b = if b then Refset'.add else Refset'.remove in
let i,k = !inline_table in
inline_table :=
(List.fold_right (f b) l i),
@@ -504,14 +523,14 @@ let extraction_inline b l =
let print_extraction_inline () =
let (i,n)= !inline_table in
- let i'= Refset.filter (function ConstRef _ -> true | _ -> false) i in
+ let i'= Refset'.filter (function ConstRef _ -> true | _ -> false) i in
msg
(str "Extraction Inline:" ++ fnl () ++
- Refset.fold
+ Refset'.fold
(fun r p ->
(p ++ str " " ++ safe_pr_long_global r ++ fnl ())) i' (mt ()) ++
str "Extraction NoInline:" ++ fnl () ++
- Refset.fold
+ Refset'.fold
(fun r p ->
(p ++ str " " ++ safe_pr_long_global r ++ fnl ())) n (mt ()))
@@ -529,10 +548,10 @@ let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
type int_or_id = ArgInt of int | ArgId of identifier
-let implicits_table = ref Refmap.empty
+let implicits_table = ref Refmap'.empty
let implicits_of_global r =
- try Refmap.find r !implicits_table with Not_found -> []
+ try Refmap'.find r !implicits_table with Not_found -> []
let add_implicits r l =
let typ = Global.type_of_global r in
@@ -552,7 +571,7 @@ let add_implicits r l =
safe_pr_global r))
in
let l' = List.map check l in
- implicits_table := Refmap.add r l' !implicits_table
+ implicits_table := Refmap'.add r l' !implicits_table
(* Registration of operations for rollback. *)
@@ -568,7 +587,7 @@ let (implicit_extraction,_) =
let _ = declare_summary "Extraction Implicit"
{ freeze_function = (fun () -> !implicits_table);
unfreeze_function = ((:=) implicits_table);
- init_function = (fun () -> implicits_table := Refmap.empty) }
+ init_function = (fun () -> implicits_table := Refmap'.empty) }
(* Grammar entries. *)
@@ -658,22 +677,22 @@ let reset_extraction_blacklist () = Lib.add_anonymous_leaf (reset_blacklist ())
let use_type_scheme_nb_args, register_type_scheme_nb_args =
let r = ref (fun _ _ -> 0) in (fun x y -> !r x y), (:=) r
-let customs = ref Refmap.empty
+let customs = ref Refmap'.empty
-let add_custom r ids s = customs := Refmap.add r (ids,s) !customs
+let add_custom r ids s = customs := Refmap'.add r (ids,s) !customs
-let is_custom r = Refmap.mem r !customs
+let is_custom r = Refmap'.mem r !customs
let is_inline_custom r = (is_custom r) && (to_inline r)
-let find_custom r = snd (Refmap.find r !customs)
+let find_custom r = snd (Refmap'.find r !customs)
-let find_type_custom r = Refmap.find r !customs
+let find_type_custom r = Refmap'.find r !customs
-let custom_matchs = ref Refmap.empty
+let custom_matchs = ref Refmap'.empty
let add_custom_match r s =
- custom_matchs := Refmap.add r s !custom_matchs
+ custom_matchs := Refmap'.add r s !custom_matchs
let indref_of_match pv =
if Array.length pv = 0 then raise Not_found;
@@ -682,11 +701,11 @@ let indref_of_match pv =
| _ -> raise Not_found
let is_custom_match pv =
- try Refmap.mem (indref_of_match pv) !custom_matchs
+ try Refmap'.mem (indref_of_match pv) !custom_matchs
with Not_found -> false
let find_custom_match pv =
- Refmap.find (indref_of_match pv) !custom_matchs
+ Refmap'.find (indref_of_match pv) !custom_matchs
(* Registration of operations for rollback. *)
@@ -703,7 +722,7 @@ let (in_customs,_) =
let _ = declare_summary "ML extractions"
{ freeze_function = (fun () -> !customs);
unfreeze_function = ((:=) customs);
- init_function = (fun () -> customs := Refmap.empty) }
+ init_function = (fun () -> customs := Refmap'.empty) }
let (in_custom_matchs,_) =
declare_object
@@ -717,7 +736,7 @@ let (in_custom_matchs,_) =
let _ = declare_summary "ML extractions custom match"
{ freeze_function = (fun () -> !custom_matchs);
unfreeze_function = ((:=) custom_matchs);
- init_function = (fun () -> custom_matchs := Refmap.empty) }
+ init_function = (fun () -> custom_matchs := Refmap'.empty) }
(* Grammar entries. *)
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index a3199b50..ff4780a1 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -6,13 +6,16 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: table.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: table.mli 13420 2010-09-16 15:47:08Z letouzey $ i*)
open Names
open Libnames
open Miniml
open Declarations
+module Refset' : Set.S with type elt = global_reference
+module Refmap' : Map.S with type key = global_reference
+
val safe_basename_of_global : global_reference -> identifier
(*s Warning and Error messages. *)
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index d287913d..e47f19bf 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -235,7 +235,7 @@ let warning_error names e =
(str "Cannot define principle(s) for "++
h 1 (prlist_with_sep (fun _ -> str","++spc ()) Libnames.pr_reference names) ++
if do_observe () then Cerrors.explain_exn e else mt ())
- | _ -> anomaly ""
+ | _ -> raise e
VERNAC COMMAND EXTEND NewFunctionalScheme
@@ -263,11 +263,11 @@ VERNAC COMMAND EXTEND NewFunctionalScheme
end
| _ -> assert false (* we can only have non empty list *)
end
- | e ->
+ | e ->
let names = List.map (fun (_,na,_) -> na) fas in
warning_error names e
-
end
+
]
END
(***** debug only ***)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index f5a5fbd4..a61671f8 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -294,7 +294,7 @@ let warning_error names e =
(str "Cannot define principle(s) for "++
h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
e_explain e)
- | _ -> anomaly ""
+ | _ -> raise e
let error_error names e =
let e_explain e =
@@ -308,7 +308,7 @@ let error_error names e =
(str "Cannot define graph(s) for " ++
h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
e_explain e)
- | _ -> anomaly ""
+ | _ -> raise e
let generate_principle on_error
is_general do_built fix_rec_l recdefs interactive_proof
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index a980d963..6376d023 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1434,7 +1434,7 @@ let micromega_gen
(" Skipping what remains of this tactic: the complexity of the goal requires "
^ "the use of a specialized external tool called csdp. \n\n"
^ "Unfortunately this instance of Coq isn't aware of the presence of any \"csdp\" executable. \n\n"
- ^ "You may need to specify the location during Coq's pre-compilation configuration step")) gl
+ ^ "This executable should be in PATH")) gl
let lift_ratproof prover l =
match prover l with
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 885f7fb6..90b409ba 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: subtac.ml 13344 2010-07-28 15:04:36Z msozeau $ *)
+(* $Id: subtac.ml 13492 2010-10-04 21:20:01Z herbelin $ *)
open Global
open Pp
@@ -80,7 +80,7 @@ let start_proof_com env isevars sopt kind (bl,t) hook =
in
let c = solve_tccs_in_type env id isevars evm c typ in
Lemmas.start_proof id kind c (fun loc gr ->
- Impargs.declare_manual_implicits (loc = Local) gr ~enriching:true imps;
+ Impargs.declare_manual_implicits (loc = Local) gr ~enriching:true [imps];
hook loc gr)
let print_subgoals () = Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index b2bf9912..4927adbe 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: subtac_classes.ml 13328 2010-07-26 11:05:30Z herbelin $ i*)
+(*i $Id: subtac_classes.ml 13516 2010-10-07 19:09:38Z msozeau $ i*)
open Pretyping
open Evd
@@ -123,7 +123,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
match props with
| Inr term ->
let c = interp_casted_constr_evars evars env' term cty in
- Inr (c, subst)
+ Inr c
| Inl props ->
let get_id =
function
@@ -162,7 +162,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
let term = Termops.it_mkLambda_or_LetIn app (ctx' @ ctx) in
term, termtype
- | Inr (def, subst) ->
+ | Inr def ->
let termtype = it_mkProd_or_LetIn cty ctx in
let term = Termops.it_mkLambda_or_LetIn def ctx in
term, termtype
@@ -174,7 +174,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
let hook vis gr =
let cst = match gr with ConstRef kn -> kn | _ -> assert false in
let inst = Typeclasses.new_instance k pri global (ConstRef cst) in
- Impargs.declare_manual_implicits false gr ~enriching:false imps;
+ Impargs.declare_manual_implicits false gr ~enriching:false [imps];
Typeclasses.add_instance inst
in
let evm = Subtac_utils.evars_of_term !evars Evd.empty term in
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index e7dd7ef1..a83611a4 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -333,7 +333,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
let gr = ConstRef c in
if Impargs.is_implicit_args () || impls <> [] then
- Impargs.declare_manual_implicits false gr impls
+ Impargs.declare_manual_implicits false gr [impls]
in
let typ = it_mkProd_or_LetIn top_arity binders in
hook, name, typ
@@ -341,7 +341,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
let typ = it_mkProd_or_LetIn top_arity binders_rel in
let hook l gr =
if Impargs.is_implicit_args () || impls <> [] then
- Impargs.declare_manual_implicits false gr impls
+ Impargs.declare_manual_implicits false gr [impls]
in hook, recname, typ
in
let fullcoqc = Evarutil.nf_evar !isevars def in
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 1424618f..b76d0cb0 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -211,7 +211,7 @@ let declare_definition prg =
in
let gr = ConstRef c in
if Impargs.is_implicit_args () || prg.prg_implicits <> [] then
- Impargs.declare_manual_implicits false gr prg.prg_implicits;
+ Impargs.declare_manual_implicits false gr [prg.prg_implicits];
print_message (Subtac_utils.definition_message prg.prg_name);
progmap_remove prg;
prg.prg_hook local gr;
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-26 20:46:04 +0000