summaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2007-10-15 19:55:12 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2007-10-15 19:55:12 +0000
commit4767d724d489a7ad67f696e9401e70b9f9ae2143 (patch)
tree142a99bc1cd3beef403f1942908de090f70c5e07 /contrib
parent72b9a7df489ea47b3e5470741fd39f6100d31676 (diff)
Imported Upstream version 8.1.pl2+dfsgupstream/8.1.pl2+dfsg
Diffstat (limited to 'contrib')
-rw-r--r--contrib/cc/cctac.ml6
-rw-r--r--contrib/cc/cctac.mli4
-rw-r--r--contrib/extraction/extract_env.ml5
-rw-r--r--contrib/extraction/extraction.ml25
-rw-r--r--contrib/extraction/table.ml87
-rw-r--r--contrib/extraction/table.mli9
-rw-r--r--contrib/setoid_ring/Ring_tac.v9
-rw-r--r--contrib/setoid_ring/newring.ml47
8 files changed, 85 insertions, 67 deletions
diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml
index 86251254..dc0dec0e 100644
--- a/contrib/cc/cctac.ml
+++ b/contrib/cc/cctac.ml
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: cctac.ml 9856 2007-05-24 14:05:40Z corbinea $ *)
+(* $Id: cctac.ml 10121 2007-09-14 09:45:40Z corbinea $ *)
(* This file is the interface between the c-c algorithm and Coq *)
@@ -199,7 +199,7 @@ let build_projection intype outtype (cstr:constructor) special default gls=
let ind=destInd h in
let types=Inductiveops.arities_of_constructors env ind in
let lp=Array.length types in
- let ci=(snd cstr)-1 in
+ let ci=pred (snd cstr) in
let branch i=
let ti=Term.prod_appvect types.(i) argv in
let rc=fst (Sign.decompose_prod_assum ti) in
@@ -247,7 +247,7 @@ let rec proof_tac p gls =
and tx2=constr_of_term p2.p_rhs in
let typf = pf_type_of gls tf1 in
let typx = pf_type_of gls tx1 in
- let typfx = prod_applist typf [tx1] in
+ let typfx = pf_type_of gls (mkApp (tf1,[|tx1|])) in
let id = pf_get_new_id (id_of_string "f") gls in
let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
let lemma1 =
diff --git a/contrib/cc/cctac.mli b/contrib/cc/cctac.mli
index 97fa4d77..ffc4b9c4 100644
--- a/contrib/cc/cctac.mli
+++ b/contrib/cc/cctac.mli
@@ -6,11 +6,13 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: cctac.mli 9151 2006-09-19 13:32:22Z corbinea $ *)
+(* $Id: cctac.mli 10121 2007-09-14 09:45:40Z corbinea $ *)
open Term
open Proof_type
+val proof_tac: Ccproof.proof -> Proof_type.tactic
+
val cc_tactic : int -> constr list -> tactic
val cc_fail : tactic
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index e31b701c..825b3554 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: extract_env.ml 9486 2007-01-15 19:11:28Z letouzey $ i*)
+(*i $Id: extract_env.ml 10209 2007-10-09 21:49:37Z letouzey $ i*)
open Term
open Declarations
@@ -92,7 +92,8 @@ module Visit : VISIT = struct
let needed_kn kn = KNset.mem kn v.kn
let needed_con c = Cset.mem c v.con
let needed_mp mp = MPset.mem mp v.mp
- let add_mp mp = v.mp <- MPset.union (prefixes_mp 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 <- KNset.add kn v.kn; add_mp (modpath kn)
let add_con c = v.con <- Cset.add c v.con; add_mp (con_modpath c)
let add_ref = function
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 6fd4a3cc..6982ffc6 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: extraction.ml 9456 2006-12-17 20:08:38Z letouzey $ i*)
+(*i $Id: extraction.ml 10195 2007-10-08 01:47:55Z letouzey $ i*)
(*i*)
open Util
@@ -31,10 +31,6 @@ open Mlutil
exception I of inductive_info
-(* A set of all inductive currently being computed,
- to avoid loops in [extract_inductive] *)
-let internal_call = ref KNset.empty
-
(* A set of all fixpoint functions currently being extracted *)
let current_fixpoints = ref ([] : constant list)
@@ -303,13 +299,15 @@ and extract_type_scheme env db c p =
(*S Extraction of an inductive type. *)
and extract_ind env kn = (* kn is supposed to be in long form *)
- try
- if KNset.mem kn !internal_call then lookup_ind kn (* Already started. *)
- else if visible_kn kn then lookup_ind kn (* Standard situation. *)
- else raise Not_found (* Never trust the table for a internal kn. *)
+ let mib = Environ.lookup_mind kn env in
+ try
+ (* For a same kn, we can get various bodies due to module substitutions.
+ We hence check that the mib has not changed from recording
+ time to retrieving time. Ideally we should also check the env. *)
+ let (mib0,ml_ind) = lookup_ind kn in
+ if not (mib = mib0) then raise Not_found;
+ ml_ind
with Not_found ->
- internal_call := KNset.add kn !internal_call;
- let mib = Environ.lookup_mind kn env in
(* First, if this inductive is aliased via a Module, *)
(* we process the original inductive. *)
option_iter (fun kn -> ignore (extract_ind env kn)) mib.mind_equiv;
@@ -335,7 +333,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
ip_types = t })
mib.mind_packets
in
- add_ind kn
+ add_ind kn mib
{ind_info = Standard;
ind_nparams = npar;
ind_packets = packets;
@@ -425,8 +423,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
ind_packets = packets;
ind_equiv = mib.mind_equiv}
in
- add_ind kn i;
- internal_call := KNset.remove kn !internal_call;
+ add_ind kn mib i;
i
(*s [extract_type_cons] extracts the type of an inductive
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index b1a3cb31..6d39faee 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: table.ml 9310 2006-10-28 19:35:09Z herbelin $ i*)
+(*i $Id: table.ml 10209 2007-10-09 21:49:37Z letouzey $ i*)
open Names
open Term
@@ -60,7 +60,6 @@ let at_toplevel mp =
let visible_kn kn = at_toplevel (base_mp (modpath kn))
let visible_con kn = at_toplevel (base_mp (con_modpath kn))
-
(*S The main tables: constants, inductives, records, ... *)
(*s Constants tables. *)
@@ -77,9 +76,9 @@ let lookup_type kn = Cmap.find kn !types
(*s Inductives table. *)
-let inductives = ref (KNmap.empty : ml_ind KNmap.t)
+let inductives = ref (KNmap.empty : (mutual_inductive_body * ml_ind) KNmap.t)
let init_inductives () = inductives := KNmap.empty
-let add_ind kn m = inductives := KNmap.add kn m !inductives
+let add_ind kn mib ml_ind = inductives := KNmap.add kn (mib,ml_ind) !inductives
let lookup_ind kn = KNmap.find kn !inductives
(*s Recursors table. *)
@@ -124,11 +123,24 @@ let reset_tables () =
let id_of_global = function
| ConstRef kn -> let _,_,l = repr_con kn in id_of_label l
- | IndRef (kn,i) -> (lookup_ind kn).ind_packets.(i).ip_typename
- | ConstructRef ((kn,i),j) -> (lookup_ind kn).ind_packets.(i).ip_consnames.(j-1)
+ | IndRef (kn,i) -> (snd (lookup_ind kn)).ind_packets.(i).ip_typename
+ | ConstructRef ((kn,i),j) ->
+ (snd (lookup_ind kn)).ind_packets.(i).ip_consnames.(j-1)
| _ -> assert false
-let pr_global r = pr_id (id_of_global r)
+let pr_global r =
+ try Printer.pr_global r
+ with _ -> pr_id (id_of_global r)
+
+(* idem, but with qualification, and only for constants. *)
+
+let pr_long_global r =
+ try Printer.pr_global r
+ with _ -> match r with
+ | ConstRef kn ->
+ let mp,_,l = repr_con kn in
+ str ((string_of_mp mp)^"."^(string_of_label l))
+ | _ -> assert false
(*S Warning and Error messages. *)
@@ -150,13 +162,13 @@ let warning_log_ax r =
spc () ++ str "may lead to incorrect or non-terminating ML terms.")
let check_inside_module () =
- try
- ignore (Lib.what_is_opened ());
- Options.if_verbose warning
- ("Extraction inside an opened module is experimental.\n"^
- "In case of problem, close it first.\n");
- Pp.flush_all ()
- with Not_found -> ()
+ if Lib.is_modtype () then
+ err (str "You can't do that within a Module Type." ++ fnl () ++
+ str "Close it and try again.")
+ else if Lib.is_module () then
+ msg_warning
+ (str "Extraction inside an opened module is experimental.\n" ++
+ str "In case of problem, close it first.\n")
let check_inside_section () =
if Lib.sections_are_opened () then
@@ -164,10 +176,10 @@ let check_inside_section () =
str "Close it and try again.")
let error_constant r =
- err (Printer.pr_global r ++ str " is not a constant.")
+ err (pr_global r ++ str " is not a constant.")
let error_inductive r =
- err (Printer.pr_global r ++ spc () ++ str "is not an inductive type.")
+ err (pr_global r ++ spc () ++ str "is not an inductive type.")
let error_nb_cons () =
err (str "Not the right number of constructors.")
@@ -187,23 +199,23 @@ let error_scheme () =
err (str "No Scheme modular extraction available yet.")
let error_not_visible r =
- err (Printer.pr_global r ++ str " is not directly visible.\n" ++
+ err (pr_global r ++ str " is not directly visible.\n" ++
str "For example, it may be inside an applied functor." ++
str "Use Recursive Extraction to get the whole environment.")
-let error_unqualified_name s1 s2 =
- err (str (s1 ^ " is used in " ^ s2 ^ " where it cannot be disambiguated\n" ^
- "in ML from another name sharing the same basename.\n" ^
- "Please do some renaming.\n"))
-
let error_MPfile_as_mod d =
err (str ("The whole file "^(string_of_dirpath d)^".v is used somewhere as a module.\n"^
"Extraction cannot currently deal with this situation.\n"))
let error_record r =
- err (str "Record " ++ Printer.pr_global r ++ str " has an anonymous field." ++ fnl () ++
+ err (str "Record " ++ pr_global r ++ str " has an anonymous field." ++ fnl () ++
str "To help extraction, please use an explicit name.")
+let check_loaded_modfile mp = match base_mp mp with
+ | MPfile dp -> if not (Library.library_is_loaded dp) then
+ err (str ("Please load library "^(string_of_dirpath dp^" first.")))
+ | _ -> ()
+
(*S The Extraction auxiliary commands *)
(*s Extraction AutoInline *)
@@ -310,7 +322,7 @@ let _ = declare_summary "Extraction Lang"
{ freeze_function = (fun () -> !lang_ref);
unfreeze_function = ((:=) lang_ref);
init_function = (fun () -> lang_ref := Ocaml);
- survive_module = false;
+ survive_module = true;
survive_section = true }
let extraction_language x = Lib.add_anonymous_leaf (extr_lang x)
@@ -342,28 +354,21 @@ let (inline_extraction,_) =
load_function = (fun _ (_,(b,l)) -> add_inline_entries b l);
export_function = (fun x -> Some x);
classify_function = (fun (_,o) -> Substitute o);
- (*CSC: The following substitution may istantiate a realized parameter.
- The right solution would be to make the substitution erase the
- realizer from the table. However, this is not allowed by Coq.
- In this particular case, though, keeping the realizer is place seems
- to be harmless since the current code looks for a realizer only
- when the constant is a parameter. However, if this behaviour changes
- subtle bugs can happear in the future. *)
subst_function =
- (fun (_,s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))}
+ (fun (_,s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))
+ }
let _ = declare_summary "Extraction Inline"
{ freeze_function = (fun () -> !inline_table);
unfreeze_function = ((:=) inline_table);
init_function = (fun () -> inline_table := empty_inline_table);
- survive_module = false;
+ survive_module = true;
survive_section = true }
(* Grammar entries. *)
let extraction_inline b l =
check_inside_section ();
- check_inside_module ();
let refs = List.map Nametab.global l in
List.iter
(fun r -> match r with
@@ -380,11 +385,11 @@ let print_extraction_inline () =
(str "Extraction Inline:" ++ fnl () ++
Refset.fold
(fun r p ->
- (p ++ str " " ++ Printer.pr_global r ++ fnl ())) i' (mt ()) ++
+ (p ++ str " " ++ pr_long_global r ++ fnl ())) i' (mt ()) ++
str "Extraction NoInline:" ++ fnl () ++
Refset.fold
(fun r p ->
- (p ++ str " " ++ Printer.pr_global r ++ fnl ())) n (mt ()))
+ (p ++ str " " ++ pr_long_global r ++ fnl ())) n (mt ()))
(* Reset part *)
@@ -423,20 +428,23 @@ let (in_customs,_) =
{(default_object "ML extractions") with
cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s);
load_function = (fun _ (_,(r,ids,s)) -> add_custom r ids s);
- export_function = (fun x -> Some x)}
+ export_function = (fun x -> Some x);
+ classify_function = (fun (_,o) -> Substitute o);
+ subst_function =
+ (fun (_,s,(r,ids,str)) -> (fst (subst_global s r), ids, str))
+ }
let _ = declare_summary "ML extractions"
{ freeze_function = (fun () -> !customs);
unfreeze_function = ((:=) customs);
init_function = (fun () -> customs := Refmap.empty);
- survive_module = false;
+ survive_module = true;
survive_section = true }
(* Grammar entries. *)
let extract_constant_inline inline r ids s =
check_inside_section ();
- check_inside_module ();
let g = Nametab.global r in
match g with
| ConstRef kn ->
@@ -455,7 +463,6 @@ let extract_constant_inline inline r ids s =
let extract_inductive r (s,l) =
check_inside_section ();
- check_inside_module ();
let g = Nametab.global r in
match g with
| IndRef ((kn,i) as ip) ->
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 66662138..c9a4e8da 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -6,11 +6,12 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: table.mli 6441 2004-12-09 02:27:09Z letouzey $ i*)
+(*i $Id: table.mli 10209 2007-10-09 21:49:37Z letouzey $ i*)
open Names
open Libnames
open Miniml
+open Declarations
val id_of_global : global_reference -> identifier
@@ -27,11 +28,11 @@ val error_unknown_module : qualid -> 'a
val error_toplevel : unit -> 'a
val error_scheme : unit -> 'a
val error_not_visible : global_reference -> 'a
-val error_unqualified_name : string -> string -> 'a
val error_MPfile_as_mod : dir_path -> 'a
val error_record : global_reference -> 'a
val check_inside_module : unit -> unit
val check_inside_section : unit -> unit
+val check_loaded_modfile : module_path -> unit
(*s utilities concerning [module_path]. *)
@@ -55,8 +56,8 @@ val lookup_term : constant -> ml_decl
val add_type : constant -> ml_schema -> unit
val lookup_type : constant -> ml_schema
-val add_ind : kernel_name -> ml_ind -> unit
-val lookup_ind : kernel_name -> ml_ind
+val add_ind : kernel_name -> mutual_inductive_body -> ml_ind -> unit
+val lookup_ind : kernel_name -> mutual_inductive_body * ml_ind
val add_recursors : Environ.env -> kernel_name -> unit
val is_recursor : global_reference -> bool
diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v
index b55c5443..d8bb9eae 100644
--- a/contrib/setoid_ring/Ring_tac.v
+++ b/contrib/setoid_ring/Ring_tac.v
@@ -152,8 +152,15 @@ Ltac ParseRingComponents lemma :=
(* ring tactics *)
+Ltac relation_carrier req :=
+ let ty := type of req in
+ match eval hnf in ty with
+ ?R -> _ => R
+ | _ => fail 1000 "Equality has no relation type"
+ end.
+
Ltac FV_hypo_tac mkFV req lH :=
- let R := match type of req with ?R -> _ => R end in
+ let R := relation_carrier req in
let FV_hypo_l_tac h :=
match h with @mkhypo (req ?pe _) _ => mkFV pe end in
let FV_hypo_r_tac h :=
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index f963fc9c..134ba1a8 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(*i $Id: newring.ml4 9968 2007-07-11 15:49:07Z barras $ i*)
+(*i $Id: newring.ml4 10047 2007-07-24 17:55:18Z barras $ i*)
open Pp
open Util
@@ -465,7 +465,8 @@ let op_smorph r add mul req m1 m2 =
let default_ring_equality (r,add,mul,opp,req) =
let is_setoid = function
- {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _} -> true
+ {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _;rel_aeq=rel} ->
+ eq_constr req rel (* Qu: use conversion ? *)
| _ -> false in
match default_relation_for_carrier ~filter:is_setoid r with
Leibniz _ ->
@@ -625,6 +626,7 @@ let interp_sign env sign =
(* Same remark on ill-typed terms ... *)
let add_theory name rth eqth morphth cst_tac (pre,post) power sign =
+ check_required_library (cdir@["Ring_base"]);
let env = Global.env() in
let sigma = Evd.empty in
let (kind,r,zero,one,add,mul,sub,opp,req) = dest_ring env sigma rth in
@@ -986,6 +988,7 @@ let default_field_equality r inv req =
inv_m.lem
let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign =
+ check_required_library (cdir@["Field_tac"]);
let env = Global.env() in
let sigma = Evd.empty in
let (kind,r,zero,one,add,mul,sub,opp,div,inv,req,rth) =