diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/subtyping.ml | 105 |
1 files changed, 60 insertions, 45 deletions
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 9f03b57c5d..033eeec793 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -19,6 +19,7 @@ open Reduction open Inductive open Modops open Mod_subst +open Entries (*i*) (* This local type is used to subtype a constant with a constructor or @@ -27,7 +28,6 @@ open Mod_subst type namedobject = | Constant of constant_body - | Mind of mutual_inductive_body | IndType of inductive * mutual_inductive_body | IndConstr of constructor * mutual_inductive_body | Module of module_specification_body @@ -41,31 +41,27 @@ let add_nameobjects_of_mib ln mib map = let ip = (ln,j) in let map = array_fold_right_i - (fun i id map -> Idmap.add id (IndConstr ((ip,i), mib)) map) - oib.mind_consnames - map + (fun i id map -> + Labmap.add (label_of_id id) (IndConstr((ip,i+1), mib)) map) + oib.mind_consnames + map in - Idmap.add oib.mind_typename (IndType (ip, mib)) map + 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 + (* creates namedobject map for the whole signature *) -let make_label_map msid list = +let make_label_map mp list = let add_one (l,e) map = - let obj = - match e with - | SPBconst cb -> Constant cb - | SPBmind mib -> Mind mib - | SPBmodule mb -> Module mb - | SPBmodtype mtb -> Modtype mtb - in -(* let map = match obj with - | Mind mib -> - add_nameobjects_of_mib (make_ln (MPself msid) l) mib map - | _ -> map - in *) - Labmap.add l obj map + let add_map obj = Labmap.add l obj map in + match e with + | SPBconst cb -> add_map (Constant cb) + | SPBmind mib -> + add_nameobjects_of_mib (make_kn mp empty_dirpath l) mib map + | SPBmodule mb -> add_map (Module mb) + | SPBmodtype mtb -> add_map (Modtype mtb) in List.fold_right add_one list Labmap.empty @@ -82,8 +78,7 @@ let check_inductive cst env msid1 l info1 mib2 spec2 = let check_conv cst f = check_conv_error error cst f in let mib1 = match info1 with - | Mind mib -> mib - (* | IndType (_,mib) -> mib we will enable this later*) + | IndType ((_,0), mib) -> mib | _ -> error () in let check_packet cst p1 p2 = @@ -161,23 +156,43 @@ let check_inductive cst env msid1 l info1 mib2 spec2 = let check_constant cst env msid1 l info1 cb2 spec2 = let error () = error_not_match l spec2 in let check_conv cst f = check_conv_error error cst f in - let cb1 = - match info1 with - | Constant cb -> cb - | _ -> error () - in - assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ; - (*Start by checking types*) - let cst = check_conv cst conv_leq env cb1.const_type cb2.const_type in - match cb2.const_body with - | None -> cst - | Some lc2 -> - let c2 = Declarations.force lc2 in - let c1 = match cb1.const_body with - | Some lc1 -> Declarations.force lc1 - | None -> mkConst (make_con (MPself msid1) empty_dirpath l) - in - check_conv cst conv env c1 c2 + match info1 with + | Constant cb1 -> + assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ; + (*Start by checking types*) + let cst = check_conv cst conv_leq env cb1.const_type cb2.const_type in + let con = make_con (MPself msid1) empty_dirpath l in + let cst = + match cb2.const_body with + | None -> cst + | Some lc2 -> + let c2 = Declarations.force lc2 in + let c1 = match cb1.const_body with + | Some lc1 -> Declarations.force lc1 + | None -> mkConst con + in + check_conv cst conv env c1 c2 + in + cst + | IndType ((kn,i) as ind,mind1) -> + Util.error ("The kernel does not recognize yet that a parameter can be " ^ + "instantiated by an inductive type. Hint: you can rename the " ^ + "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 () ; + let arity1 = mind1.mind_packets.(i).mind_user_arity in + check_conv cst conv_leq env arity1 cb2.const_type + | IndConstr (((kn,i),j) as cstr,mind1) -> + Util.error ("The kernel does not recognize yet that a parameter can be " ^ + "instantiated by a constructor. Hint: you can rename the " ^ + "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 () ; + let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in + check_conv cst conv env ty1 cb2.const_type + | _ -> error () let rec check_modules cst env msid1 l msb1 msb2 = let mp = (MPdot(MPself msid1,l)) in @@ -194,11 +209,11 @@ let rec check_modules cst env msid1 l msb1 msb2 = cst -and check_signatures cst env' (msid1,sig1) (msid2,sig2') = +and check_signatures cst env (msid1,sig1) (msid2,sig2') = let mp1 = MPself msid1 in - let env = add_signature mp1 sig1 env' in + let env = add_signature mp1 sig1 env in let sig2 = subst_signature_msid msid2 mp1 sig2' in - let map1 = make_label_map msid1 sig1 in + let map1 = make_label_map mp1 sig1 in let check_one_body cst (l,spec2) = let info1 = try @@ -229,10 +244,10 @@ and check_signatures cst env' (msid1,sig1) (msid2,sig2') = List.fold_left check_one_body cst sig2 and check_modtypes cst env mtb1 mtb2 equiv = - if mtb1==mtb2 then (); (* just in case :) *) + if mtb1==mtb2 then cst else (* just in case :) *) let mtb1' = scrape_modtype env mtb1 in let mtb2' = scrape_modtype env mtb2 in - if mtb1'==mtb2' then (); + if mtb1'==mtb2' then cst else match mtb1', mtb2' with | MTBsig (msid1,list1), MTBsig (msid2,list2) -> @@ -245,7 +260,7 @@ and check_modtypes cst env mtb1 mtb2 equiv = MTBfunsig (arg_id2,arg_t2,body_t2) -> let cst = check_modtypes cst env arg_t2 arg_t1 equiv in (* contravariant *) - let env' = + let env = add_module (MPbound arg_id2) (module_body_of_type arg_t2) env in let body_t1' = @@ -255,7 +270,7 @@ and check_modtypes cst env mtb1 mtb2 equiv = (map_mbid arg_id1 (MPbound arg_id2) None) body_t1 in - check_modtypes cst env' body_t1' body_t2 equiv + check_modtypes cst env body_t1' body_t2 equiv | MTBident _ , _ -> anomaly "Subtyping: scrape failed" | _ , MTBident _ -> anomaly "Subtyping: scrape failed" | _ , _ -> error_incompatible_modtypes mtb1 mtb2 |