summaryrefslogtreecommitdiff
path: root/toplevel/class.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /toplevel/class.ml
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'toplevel/class.ml')
-rw-r--r--toplevel/class.ml57
1 files changed, 22 insertions, 35 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 6ebc663b..3526bd8c 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: class.ml 11343 2008-09-01 20:55:13Z herbelin $ *)
+(* $Id$ *)
open Util
open Pp
@@ -29,10 +29,6 @@ open Safe_typing
let strength_min l = if List.mem Local l then Local else Global
-let id_of_varid c = match kind_of_term c with
- | Var id -> id
- | _ -> anomaly "class__id_of_varid"
-
(* Errors *)
type coercion_error_kind =
@@ -54,7 +50,7 @@ let explain_coercion_error g = function
| NotAFunction ->
(Printer.pr_global g ++ str" is not a function")
| NoSource (Some cl) ->
- (str "Cannot recognize " ++ pr_class cl ++ str " as a source class of "
+ (str "Cannot recognize " ++ pr_class cl ++ str " as a source class of "
++ Printer.pr_global g)
| NoSource None ->
(str ": cannot find the source class of " ++ Printer.pr_global g)
@@ -62,7 +58,7 @@ let explain_coercion_error g = function
pr_class cl ++ str " cannot be a source class"
| NotUniform ->
(Printer.pr_global g ++
- str" does not respect the inheritance uniform condition");
+ str" does not respect the uniform inheritance condition");
| NoTarget ->
(str"Cannot find the target class")
| WrongTarget (clt,cl) ->
@@ -95,33 +91,24 @@ let check_target clt = function
(* condition d'heritage uniforme *)
-let uniform_cond nargs lt =
+let uniform_cond nargs lt =
let rec aux = function
| (0,[]) -> true
| (n,t::l) -> (strip_outer_cast t = mkRel n) & (aux ((n-1),l))
| _ -> false
- in
+ in
aux (nargs,lt)
-let id_of_cl = function
- | CL_FUN -> id_of_string "FUNCLASS"
- | CL_SORT -> id_of_string "SORTCLASS"
- | CL_CONST kn -> id_of_label (con_label kn)
- | CL_IND ind ->
- let (_,mip) = Global.lookup_inductive ind in
- mip.mind_typename
- | CL_SECVAR id -> id
-
let class_of_global = function
| ConstRef sp -> CL_CONST sp
| IndRef sp -> CL_IND sp
| VarRef id -> CL_SECVAR id
- | ConstructRef _ as c ->
+ | ConstructRef _ as c ->
errorlabstrm "class_of_global"
- (str "Constructors, such as " ++ Printer.pr_global c ++
+ (str "Constructors, such as " ++ Printer.pr_global c ++
str ", cannot be used as a class.")
-(*
+(*
lp est la liste (inverse'e) des arguments de la coercion
ids est le nom de la classe source
sps_opt est le sp de la classe source dans le cas des structures
@@ -140,13 +127,13 @@ let get_source lp source =
match lp with
| [] -> raise Not_found
| t1::_ -> find_class_type (Global.env()) Evd.empty t1
- in
+ in
(cl1,lv1,1)
| Some cl ->
let rec aux = function
| [] -> raise Not_found
| t1::lt ->
- try
+ try
let cl1,lv1 = find_class_type (Global.env()) Evd.empty t1 in
if cl = cl1 then cl1,lv1,(List.length lt+1)
else raise Not_found
@@ -154,20 +141,20 @@ let get_source lp source =
in aux (List.rev lp)
let get_target t ind =
- if (ind > 1) then
+ if (ind > 1) then
CL_FUN
- else
+ else
fst (find_class_type (Global.env()) Evd.empty t)
-let prods_of t =
+let prods_of t =
let rec aux acc d = match kind_of_term d with
| Prod (_,c1,c2) -> aux (c1::acc) c2
| Cast (c,_,_) -> aux acc c
| _ -> (d,acc)
- in
+ in
aux [] t
-let strength_of_cl = function
+let strength_of_cl = function
| CL_CONST kn -> Global
| CL_SECVAR id -> Local
| _ -> Global
@@ -182,7 +169,7 @@ let ident_key_of_class = function
| CL_FUN -> "Funclass"
| CL_SORT -> "Sortclass"
| CL_CONST sp -> string_of_label (con_label sp)
- | CL_IND (sp,_) -> string_of_label (label sp)
+ | CL_IND (sp,_) -> string_of_label (mind_label sp)
| CL_SECVAR id -> string_of_id id
(* coercion identité *)
@@ -199,7 +186,7 @@ let build_id_coercion idf_opt source =
let c = match constant_opt_value env (destConst vs) with
| Some c -> c
| None -> error_not_transparent source in
- let lams,t = Sign.decompose_lam_assum c in
+ let lams,t = decompose_lam_assum c in
let val_f =
it_mkLambda_or_LetIn
(mkLambda (Name (id_of_string "x"),
@@ -213,7 +200,7 @@ let build_id_coercion idf_opt source =
lams
in
(* juste pour verification *)
- let _ =
+ let _ =
if not
(Reductionops.is_conv_leq env Evd.empty
(Typing.type_of env Evd.empty val_f) typ_f)
@@ -242,7 +229,7 @@ let check_source = function
| Some (CL_FUN|CL_SORT as s) -> raise (CoercionError (ForbiddenSourceClass s))
| _ -> ()
-(*
+(*
nom de la fonction coercion
strength de f
nom de la classe source (optionnel)
@@ -261,7 +248,7 @@ let add_new_coercion_core coef stre source target isid =
let llp = List.length lp in
if llp = 0 then raise (CoercionError NotAFunction);
let (cls,lvs,ind) =
- try
+ try
get_source lp source
with Not_found ->
raise (CoercionError (NoSource source))
@@ -271,7 +258,7 @@ let add_new_coercion_core coef stre source target isid =
raise (CoercionError NotUniform);
let clt =
try
- get_target tg ind
+ get_target tg ind
with Not_found ->
raise (CoercionError NoTarget)
in
@@ -304,7 +291,7 @@ let try_add_new_identity_coercion id stre ~source ~target =
let try_add_new_coercion_with_source ref stre ~source =
try_add_new_coercion_core ref stre (Some source) None false
-let add_coercion_hook stre ref =
+let add_coercion_hook stre ref =
try_add_new_coercion ref stre;
Flags.if_verbose message
(string_of_qualid (shortest_qualid_of_global Idset.empty ref)