diff options
Diffstat (limited to 'checker/subtyping.ml')
| -rw-r--r-- | checker/subtyping.ml | 252 |
1 files changed, 119 insertions, 133 deletions
diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 7a6868fe..3a100c01 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -19,29 +19,28 @@ open Reduction open Inductive open Modops (*i*) -open Pp +open Pp (* This local type is used to subtype a constant with a constructor or an inductive type. It can also be useful to allow reorderings in inductive types *) -type namedobject = +type namedobject = | Constant of constant_body | IndType of inductive * mutual_inductive_body | IndConstr of constructor * mutual_inductive_body | Module of module_body | Modtype of module_type_body - | Alias of module_path * struct_expr_body option (* adds above information about one mutual inductive: all types and constructors *) -let add_nameobjects_of_mib ln mib map = +let add_nameobjects_of_mib ln mib map = let add_nameobjects_of_one j oib map = let ip = (ln,j) in - let map = - array_fold_right_i + let map = + array_fold_right_i (fun i id map -> Labmap.add (label_of_id id) (IndConstr((ip,i+1), mib)) map) oib.mind_consnames @@ -54,19 +53,19 @@ let add_nameobjects_of_mib ln mib map = (* creates namedobject map for the whole signature *) -let make_label_map mp list = - let add_one (l,e) map = +let make_label_map 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_kn mp empty_dirpath l) mib map + add_nameobjects_of_mib (make_mind mp empty_dirpath l) mib map | SFBmodule mb -> add_map (Module mb) | SFBmodtype mtb -> add_map (Modtype mtb) - | SFBalias (mp,t,cst) -> add_map (Alias (mp,t)) in List.fold_right add_one list Labmap.empty + let check_conv_error error f env a1 a2 = try f env a1 a2 @@ -74,20 +73,21 @@ let check_conv_error error f env a1 a2 = NotConvertible -> error () (* for now we do not allow reorderings *) -let check_inductive env msid1 l info1 mib2 spec2 = - let kn = make_kn (MPself msid1) empty_dirpath l in +let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= + let kn = make_mind mp1 empty_dirpath l in let error () = error_not_match l spec2 in let check_conv f = check_conv_error error f in - let mib1 = + let mib1 = match info1 with | IndType ((_,0), mib) -> mib | _ -> error () in + let mib2 = subst_mind subst2 mib2 in let check_inductive_type env t1 t2 = (* Due to sort-polymorphism in inductive types, the conclusions of t1 and t2, if in Type, are generated as the least upper bounds - of the types of the constructors. + of the types of the constructors. By monotonicity of the infered l.u.b. wrt subtyping (i.e. if X:U |- T(X):s and |- M:U' and U'<=U then infer_type(T(M))<=s), each @@ -114,7 +114,7 @@ let check_inductive env msid1 l info1 mib2 spec2 = | Type _, Type _ -> (* shortcut here *) Prop Null, Prop Null | (Prop _, Type _) | (Type _,Prop _) -> error () | _ -> (s1, s2) in - check_conv conv_leq env + check_conv conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2)) in @@ -145,7 +145,7 @@ let check_inductive env msid1 l info1 mib2 spec2 = check (fun mib -> mib.mind_finite); check (fun mib -> mib.mind_ntypes); assert (mib1.mind_hyps=[] && mib2.mind_hyps=[]); - assert (Array.length mib1.mind_packets >= 1 + assert (Array.length mib1.mind_packets >= 1 && Array.length mib2.mind_packets >= 1); (* Check that the expected numbers of uniform parameters are the same *) @@ -155,30 +155,30 @@ let check_inductive env msid1 l info1 mib2 spec2 = (* the inductive types and constructors types have to be convertible *) check (fun mib -> mib.mind_nparams); - begin + (*begin match mib2.mind_equiv with | None -> () - | Some kn2' -> + | Some kn2' -> let kn2 = scrape_mind env kn2' in let kn1 = match mib1.mind_equiv with None -> kn | Some kn1' -> scrape_mind env kn1' in if kn1 <> kn2 then error () - end; + end;*) (* we check that records and their field names are preserved. *) check (fun mib -> mib.mind_record); - if mib1.mind_record then begin - let rec names_prod_letin t = match t with + if mib1.mind_record then begin + let rec names_prod_letin t = match t with | Prod(n,_,t) -> n::(names_prod_letin t) | LetIn(n,_,_,t) -> n::(names_prod_letin t) | Cast(t,_,_) -> names_prod_letin t | _ -> [] - in + in assert (Array.length mib1.mind_packets = 1); assert (Array.length mib2.mind_packets = 1); - assert (Array.length mib1.mind_packets.(0).mind_user_lc = 1); - assert (Array.length mib2.mind_packets.(0).mind_user_lc = 1); + assert (Array.length mib1.mind_packets.(0).mind_user_lc = 1); + assert (Array.length mib2.mind_packets.(0).mind_user_lc = 1); check (fun mib -> names_prod_letin mib.mind_packets.(0).mind_user_lc.(0)); end; (* we first check simple things *) @@ -187,10 +187,10 @@ let check_inductive env msid1 l info1 mib2 spec2 = let _ = array_map2_i check_cons_types mib1.mind_packets mib2.mind_packets in () -let check_constant env msid1 l info1 cb2 spec2 = +let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = let error () = error_not_match l spec2 in let check_conv f = check_conv_error error f in - let check_type env t1 t2 = + let check_type env t1 t2 = (* If the type of a constant is generated, it may mention non-variable algebraic universes that the general conversion @@ -201,7 +201,7 @@ let check_constant env msid1 l info1 cb2 spec2 = Gamma |- A |> T, Gamma |- A' |> T' and Gamma |- A=A' then T <= T'). Hence they don't have to be checked again *) - let t1,t2 = + let t1,t2 = if isArity t2 then let (ctx2,s2) = destArity t2 in match s2 with @@ -236,30 +236,31 @@ let check_constant env msid1 l info1 cb2 spec2 = (t1,t2) in check_conv conv_leq env t1 t2 in - - match info1 with - | Constant cb1 -> - assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ; - (*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; - let con = make_con (MPself msid1) 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 - | _ -> ()) - | IndType ((kn,i),mind1) -> - ignore (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.")); + 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 + | _ -> ()) + | IndType ((kn,i),mind1) -> + ignore (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 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in @@ -278,111 +279,96 @@ let check_constant env msid1 l info1 cb2 spec2 = check_conv conv env ty1 ty2 | _ -> error () -let rec check_modules env msid1 l msb1 msb2 = - let mp = (MPdot(MPself msid1,l)) in - let mty1 = module_type_of_module (Some mp) msb1 in - let mty2 = module_type_of_module None msb2 in - check_modtypes env mty1 mty2 false - +let rec check_modules env msb1 msb2 subst1 subst2 = + let mty1 = module_type_of_module env None msb1 in + let mty2 = module_type_of_module env None msb2 in + check_modtypes env mty1 mty2 subst1 subst2 false; + -and check_signatures env (msid1,sig1) alias (msid2,sig2') = - let mp1 = MPself msid1 in - let env = add_signature mp1 sig1 env in - let alias = update_subst_alias alias (map_msid msid2 mp1) in - let sig2 = subst_structure alias sig2' in - let sig2 = subst_signature_msid msid2 mp1 sig2 in +and check_signatures env mp1 sig1 sig2 subst1 subst2 = let map1 = make_label_map 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 msid1 msid2 + 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 msid1 l info1 cb2 spec2 - | SFBmind mib2 -> - check_inductive env msid1 l info1 mib2 spec2 - | SFBmodule msb2 -> + check_constant env mp1 l info1 cb2 spec2 subst1 subst2 + | SFBmind mib2 -> + check_inductive env mp1 l info1 mib2 spec2 subst1 subst2 + | SFBmodule msb2 -> begin match info1 with - | Module msb -> check_modules env msid1 l msb msb2 - | Alias (mp,typ_opt) ->let msb = - {mod_expr = Some (SEBident mp); - mod_type = typ_opt; - mod_constraints = Constraint.empty; - mod_alias = (lookup_modtype mp env).typ_alias; - mod_retroknowledge = []} in - check_modules env msid1 l msb msb2 - | _ -> error_not_match l spec2 - end - | SFBalias (mp,typ_opt,_) -> - begin - match info1 with - | Alias (mp1,_) -> check_modpath_equiv env mp mp1 - | Module msb -> - let msb1 = - {mod_expr = Some (SEBident mp); - mod_type = typ_opt; - mod_constraints = Constraint.empty; - mod_alias = (lookup_modtype mp env).typ_alias; - mod_retroknowledge = []} in - check_modules env msid1 l msb msb1 + | Module msb -> check_modules env msb msb2 + subst1 subst2 | _ -> error_not_match l spec2 end | SFBmodtype mtb2 -> - let mtb1 = + let mtb1 = match info1 with | Modtype mtb -> mtb | _ -> error_not_match l spec2 in - check_modtypes env mtb1 mtb2 true + let env = add_module (module_body_of_type mtb2.typ_mp mtb2) + (add_module (module_body_of_type mtb1.typ_mp mtb1) env) in + check_modtypes env mtb1 mtb2 subst1 subst2 true in List.iter check_one_body sig2 -and check_modtypes env mtb1 mtb2 equiv = - if mtb1==mtb2 then () else (* just in case :) *) - let mtb1',mtb2'= - (match mtb1.typ_strength with - None -> eval_struct env mtb1.typ_expr, - eval_struct env mtb2.typ_expr - | Some mp -> strengthen env mtb1.typ_expr mp, - eval_struct env mtb2.typ_expr) in - let rec check_structure env str1 str2 equiv = - match str1, str2 with - | SEBstruct (msid1,list1), - SEBstruct (msid2,list2) -> - check_signatures env - (msid1,list1) mtb1.typ_alias (msid2,list2); - if equiv then - check_signatures env - (msid2,list2) mtb2.typ_alias (msid1,list1) - | SEBfunctor (arg_id1,arg_t1,body_t1), +and check_modtypes env mtb1 mtb2 subst1 subst2 equiv = + if mtb1==mtb2 then () else + let mtb1',mtb2'=mtb1.typ_expr,mtb2.typ_expr in + let rec check_structure env str1 str2 equiv subst1 subst2 = + match str1,str2 with + | SEBstruct (list1), + SEBstruct (list2) -> + check_signatures env + mtb1.typ_mp list1 list2 subst1 subst2; + if equiv then + check_signatures env + mtb2.typ_mp list2 list1 subst1 subst2 + else + () + | SEBfunctor (arg_id1,arg_t1,body_t1), SEBfunctor (arg_id2,arg_t2,body_t2) -> - check_modtypes env arg_t2 arg_t1 equiv; + check_modtypes env + arg_t2 arg_t1 + (map_mp arg_t1.typ_mp arg_t2.typ_mp) subst2 + equiv ; (* contravariant *) - let env = - add_module (MPbound arg_id2) (module_body_of_type arg_t2) env + let env = add_module + (module_body_of_type (MPbound arg_id2) arg_t2) env in - let body_t1' = - (* since we are just checking well-typedness we do not need - to expand any constant. Hence the identity resolver. *) - subst_struct_expr - (map_mbid arg_id1 (MPbound arg_id2)) - body_t1 + let env = match body_t1 with + SEBstruct str -> + add_module {mod_mp = mtb1.typ_mp; + mod_expr = None; + mod_type = body_t1; + mod_type_alg= None; + mod_constraints=mtb1.typ_constraints; + mod_retroknowledge = []; + mod_delta = mtb1.typ_delta} env + | _ -> env in - check_structure env (eval_struct env body_t1') - (eval_struct env body_t2) equiv + check_structure env body_t1 body_t2 equiv + (join (map_mbid arg_id1 (MPbound arg_id2)) subst1) + subst2 | _ , _ -> error_incompatible_modtypes mtb1 mtb2 - in + in if mtb1'== mtb2' then () - else check_structure env mtb1' mtb2' equiv + else check_structure env mtb1' mtb2' equiv subst1 subst2 -let check_subtypes env sup super = +let check_subtypes env sup super = (*if sup<>super then*) - check_modtypes env sup super false - -let check_equal env sup super = + let env = add_module + (module_body_of_type sup.typ_mp sup) env in + check_modtypes env (strengthen env 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 true + check_modtypes env sup super empty_subst + (map_mp super.typ_mp sup.typ_mp) true |