summaryrefslogtreecommitdiff
path: root/checker/subtyping.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/subtyping.ml')
-rw-r--r--checker/subtyping.ml115
1 files changed, 61 insertions, 54 deletions
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 4f113cf9..6953df7d 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: subtyping.ml 10664 2008-03-14 11:27:37Z soubiran $ i*)
-
(*i*)
open Util
open Names
@@ -30,15 +28,18 @@ type namedobject =
| Constant of constant_body
| IndType of inductive * mutual_inductive_body
| IndConstr of constructor * mutual_inductive_body
+
+type namedmodule =
| Module of module_body
| Modtype of module_type_body
(* adds above information about one mutual inductive: all types and
constructors *)
-let add_nameobjects_of_mib ln mib map =
- let add_nameobjects_of_one j oib map =
- let ip = (ln,j) in
+let add_mib_nameobjects mp l mib map =
+ let ind = make_mind mp empty_dirpath l in
+ let add_mip_nameobjects j oib map =
+ let ip = (ind,j) in
let map =
array_fold_right_i
(fun i id map ->
@@ -48,22 +49,32 @@ let add_nameobjects_of_mib ln mib map =
in
Labmap.add (label_of_id oib.mind_typename) (IndType (ip, mib)) map
in
- array_fold_right_i add_nameobjects_of_one mib.mind_packets map
+ array_fold_right_i add_mip_nameobjects mib.mind_packets map
+
+
+(* creates (namedobject/namedmodule) map for the whole signature *)
+type labmap = { objs : namedobject Labmap.t; mods : namedmodule Labmap.t }
-(* creates namedobject map for the whole signature *)
+let empty_labmap = { objs = Labmap.empty; mods = Labmap.empty }
-let make_label_map mp list =
+let get_obj mp map l =
+ try Labmap.find l map.objs
+ with Not_found -> error_no_such_label_sub l mp
+
+let get_mod mp map l =
+ try Labmap.find l map.mods
+ with Not_found -> error_no_such_label_sub l mp
+
+let make_labmap mp list =
let add_one (l,e) map =
- let add_map obj = Labmap.add l obj map in
match e with
- | SFBconst cb -> add_map (Constant cb)
- | SFBmind mib ->
- add_nameobjects_of_mib (make_mind mp empty_dirpath l) mib map
- | SFBmodule mb -> add_map (Module mb)
- | SFBmodtype mtb -> add_map (Modtype mtb)
+ | SFBconst cb -> { map with objs = Labmap.add l (Constant cb) map.objs }
+ | SFBmind mib -> { map with objs = add_mib_nameobjects mp l mib map.objs }
+ | SFBmodule mb -> { map with mods = Labmap.add l (Module mb) map.mods }
+ | SFBmodtype mtb -> { map with mods = Labmap.add l (Modtype mtb) map.mods }
in
- List.fold_right add_one list Labmap.empty
+ List.fold_right add_one list empty_labmap
let check_conv_error error f env a1 a2 =
@@ -239,22 +250,29 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
match info1 with
| Constant cb1 ->
assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ;
- (*Start by checking types*)
- let cb1 = subst_const_body subst1 cb1 in
- let cb2 = subst_const_body subst2 cb2 in
- let typ1 = Typeops.type_of_constant_type env cb1.const_type in
- let typ2 = Typeops.type_of_constant_type env cb2.const_type in
- check_type env typ1 typ2;
- let con = make_con mp1 empty_dirpath l in
- (match cb2 with
- | {const_body=Some lc2;const_opaque=false} ->
- let c2 = force_constr lc2 in
- let c1 = match cb1.const_body with
- | Some lc1 -> force_constr lc1
- | None -> Const con
- in
- check_conv conv env c1 c2
- | _ -> ())
+ let cb1 = subst_const_body subst1 cb1 in
+ let cb2 = subst_const_body subst2 cb2 in
+ (*Start by checking types*)
+ let typ1 = Typeops.type_of_constant_type env cb1.const_type in
+ let typ2 = Typeops.type_of_constant_type env cb2.const_type in
+ check_type env typ1 typ2;
+ (* Now we check the bodies:
+ - A transparent constant can only be implemented by a compatible
+ transparent constant.
+ - In the signature, an opaque is handled just as a parameter:
+ anything of the right type can implement it, even if bodies differ.
+ *)
+ (match cb2.const_body with
+ | Undef _ | OpaqueDef _ -> ()
+ | Def lc2 ->
+ (match cb1.const_body with
+ | Undef _ | OpaqueDef _ -> error ()
+ | Def lc1 ->
+ (* NB: cb1 might have been strengthened and appear as transparent.
+ Anyway [check_conv] will handle that afterwards. *)
+ let c1 = force_constr lc1 in
+ let c2 = force_constr lc2 in
+ check_conv conv env c1 c2))
| IndType ((kn,i),mind1) ->
ignore (Util.error (
"The kernel does not recognize yet that a parameter can be " ^
@@ -262,7 +280,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
"inductive type and give a definition to map the old name to the new " ^
"name."));
assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ;
- if cb2.const_body <> None then error () ;
+ if constant_has_body cb2 then error () ;
let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in
let typ2 = Typeops.type_of_constant_type env cb2.const_type in
check_conv conv_leq env arity1 typ2
@@ -273,42 +291,37 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
"constructor and give a definition to map the old name to the new " ^
"name."));
assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ;
- if cb2.const_body <> None then error () ;
+ if constant_has_body cb2 then error () ;
let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in
let ty2 = Typeops.type_of_constant_type env cb2.const_type in
check_conv conv env ty1 ty2
- | _ -> error ()
let rec check_modules env msb1 msb2 subst1 subst2 =
let mty1 = module_type_of_module None msb1 in
- let mty2 = module_type_of_module None msb2 in
+ let mty2 = module_type_of_module None msb2 in
check_modtypes env mty1 mty2 subst1 subst2 false;
and check_signatures env mp1 sig1 sig2 subst1 subst2 =
- let map1 = make_label_map mp1 sig1 in
+ let map1 = make_labmap mp1 sig1 in
let check_one_body (l,spec2) =
- let info1 =
- try
- Labmap.find l map1
- with
- Not_found -> error_no_such_label_sub l mp1
- in
match spec2 with
| SFBconst cb2 ->
- check_constant env mp1 l info1 cb2 spec2 subst1 subst2
+ check_constant env mp1 l (get_obj mp1 map1 l)
+ cb2 spec2 subst1 subst2
| SFBmind mib2 ->
- check_inductive env mp1 l info1 mib2 spec2 subst1 subst2
+ check_inductive env mp1 l (get_obj mp1 map1 l)
+ mib2 spec2 subst1 subst2
| SFBmodule msb2 ->
begin
- match info1 with
+ match get_mod mp1 map1 l with
| Module msb -> check_modules env msb msb2
subst1 subst2
| _ -> error_not_match l spec2
end
| SFBmodtype mtb2 ->
let mtb1 =
- match info1 with
+ match get_mod mp1 map1 l with
| Modtype mtb -> mtb
| _ -> error_not_match l spec2
in
@@ -363,11 +376,5 @@ and check_modtypes env mtb1 mtb2 subst1 subst2 equiv =
else check_structure env mtb1' mtb2' equiv subst1 subst2
let check_subtypes env sup super =
- (*if sup<>super then*)
check_modtypes env (strengthen sup sup.typ_mp) super empty_subst
- (map_mp super.typ_mp sup.typ_mp) false
-
-let check_equal env sup super =
- (*if sup<>super then*)
- check_modtypes env sup super empty_subst
- (map_mp super.typ_mp sup.typ_mp) true
+ (map_mp super.typ_mp sup.typ_mp) false
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 17:40:49 +0000