diff options
Diffstat (limited to 'checker/mod_checking.ml')
-rw-r--r-- | checker/mod_checking.ml | 121 |
1 files changed, 53 insertions, 68 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 95387cac..dc3ed452 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -21,8 +21,8 @@ let refresh_arity ar = Sort (Type u) when not (Univ.is_univ_variable u) -> let u' = Univ.fresh_local_univ() in mkArity (ctxt,Type u'), - Univ.enforce_geq u' u Univ.Constraint.empty - | _ -> ar, Univ.Constraint.empty + Univ.enforce_geq u' u Univ.empty_constraint + | _ -> ar, Univ.empty_constraint let check_constant_declaration env kn cb = Flags.if_verbose msgnl (str " checking cst: " ++ prcon kn); @@ -33,7 +33,7 @@ let check_constant_declaration env kn cb = let ty, cu = refresh_arity ty in let envty = add_constraints cu env' in let _ = infer_type envty ty in - (match cb.const_body with + (match body_of_constant cb with | Some bd -> let j = infer env' (force_constr bd) in conv_leq envty j ty @@ -53,17 +53,14 @@ let path_of_mexpr = function | SEBident mp -> mp | _ -> raise Not_path -let rec list_split_assoc k rev_before = function - | [] -> raise Not_found - | (k',b)::after when k=k' -> rev_before,b,after - | h::tail -> list_split_assoc k (h::rev_before) tail +let is_modular = function + | SFBmodule _ | SFBmodtype _ -> true + | SFBconst _ | SFBmind _ -> false -let rec list_fold_map2 f e = function - | [] -> (e,[],[]) - | h::t -> - let e',h1',h2' = f e h in - let e'',t1',t2' = list_fold_map2 f e' t in - e'',h1'::t1',h2'::t2' +let rec list_split_assoc ((k,m) as km) rev_before = function + | [] -> raise Not_found + | (k',b)::after when k=k' && is_modular b = m -> rev_before,b,after + | h::tail -> list_split_assoc km (h::rev_before) tail let check_definition_sub env cb1 cb2 = let check_type env t1 t2 = @@ -117,54 +114,61 @@ let check_definition_sub env cb1 cb2 = 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; - (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 -> assert false in - Reduction.conv env c1 c2 - | _ -> ()) + (* In the spirit of subtyping.check_constant, we accept + any implementations of parameters and opaques terms, + as long as they have the right type *) + (match cb2.const_body with + | Undef _ | OpaqueDef _ -> () + | Def lc2 -> + (match cb1.const_body with + | Def lc1 -> + let c1 = force_constr lc1 in + let c2 = force_constr lc2 in + Reduction.conv env c1 c2 + (* Coq only places transparent cb in With_definition_body *) + | _ -> assert false)) let lookup_modtype mp env = try Environ.lookup_modtype mp env with Not_found -> failwith ("Unknown module type: "^string_of_mp mp) +let lookup_module mp env = + try Environ.lookup_module mp env + with Not_found -> + failwith ("Unknown module: "^string_of_mp mp) + let rec check_with env mtb with_decl mp= match with_decl with - | With_definition_body _ -> - check_with_aux_def env mtb with_decl mp; + | With_definition_body (idl,c) -> + check_with_def env mtb (idl,c) mp; mtb - | With_module_body _ -> - check_with_aux_mod env mtb with_decl mp; + | With_module_body (idl,mp1) -> + check_with_mod env mtb (idl,mp1) mp; mtb -and check_with_aux_def env mtb with_decl mp = +and check_with_def env mtb (idl,c) mp = let sig_b = match mtb with | SEBstruct(sig_b) -> sig_b | _ -> error_signature_expected mtb in - let id,idl = match with_decl with - | With_definition_body (id::idl,_) | With_module_body (id::idl,_) -> - id,idl - | With_definition_body ([],_) | With_module_body ([],_) -> assert false + let id,idl = match idl with + | [] -> assert false + | id::idl -> id,idl in let l = label_of_id id in try - let rev_before,spec,after = list_split_assoc l [] sig_b in + let rev_before,spec,after = list_split_assoc (l,(idl<>[])) [] sig_b in let before = List.rev rev_before in let env' = Modops.add_signature mp before empty_delta_resolver env in - match with_decl with - | With_definition_body ([],_) -> assert false - | With_definition_body ([id],c) -> + if idl = [] then let cb = match spec with SFBconst cb -> cb | _ -> error_not_a_constant l in check_definition_sub env' c cb - | With_definition_body (_::_,_) -> + else let old = match spec with SFBmodule msb -> msb | _ -> error_not_a_module l @@ -172,49 +176,36 @@ and check_with_aux_def env mtb with_decl mp = begin match old.mod_expr with | None -> - let new_with_decl = match with_decl with - With_definition_body (_,c) -> - With_definition_body (idl,c) - | With_module_body (_,c) -> - With_module_body (idl,c) in - check_with_aux_def env' old.mod_type new_with_decl (MPdot(mp,l)) + check_with_def env' old.mod_type (idl,c) (MPdot(mp,l)) | Some msb -> error_a_generative_module_expected l end - | _ -> anomaly "Modtyping:incorrect use of with" with Not_found -> error_no_such_label l | Reduction.NotConvertible -> error_with_incorrect l -and check_with_aux_mod env mtb with_decl mp = +and check_with_mod env mtb (idl,mp1) mp = let sig_b = match mtb with | SEBstruct(sig_b) -> sig_b | _ -> error_signature_expected mtb in - let id,idl = match with_decl with - | With_definition_body (id::idl,_) | With_module_body (id::idl,_) -> - id,idl - | With_definition_body ([],_) | With_module_body ([],_) -> assert false + let id,idl = match idl with + | [] -> assert false + | id::idl -> id,idl in let l = label_of_id id in try - let rev_before,spec,after = list_split_assoc l [] sig_b in + let rev_before,spec,after = list_split_assoc (l,false) [] sig_b in let before = List.rev rev_before in - let rec mp_rec = function - | [] -> mp - | i::r -> MPdot(mp_rec r,label_of_id i) - in let env' = Modops.add_signature mp before empty_delta_resolver env in - match with_decl with - | With_module_body ([],_) -> assert false - | With_module_body ([id], mp1) -> + if idl = [] then let _ = match spec with SFBmodule msb -> msb | _ -> error_not_a_module l in - let (_:module_body) = (lookup_module mp1 env) in () - | With_module_body (_::_,mp) -> + let (_:module_body) = (Environ.lookup_module mp1 env) in () + else let old = match spec with SFBmodule msb -> msb | _ -> error_not_a_module l @@ -222,17 +213,11 @@ and check_with_aux_mod env mtb with_decl mp = begin match old.mod_expr with None -> - let new_with_decl = match with_decl with - With_definition_body (_,c) -> - With_definition_body (idl,c) - | With_module_body (_,c) -> - With_module_body (idl,c) in - check_with_aux_mod env' - old.mod_type new_with_decl (MPdot(mp,l)) + check_with_mod env' + old.mod_type (idl,mp1) (MPdot(mp,l)) | Some msb -> error_a_generative_module_expected l end - | _ -> anomaly "Modtyping:incorrect use of with" with Not_found -> error_no_such_label l | Reduction.NotConvertible -> error_with_incorrect l @@ -259,14 +244,14 @@ and check_module env mp mb = {typ_mp=mp; typ_expr=sign; typ_expr_alg=None; - typ_constraints=Univ.Constraint.empty; + typ_constraints=Univ.empty_constraint; typ_delta = mb.mod_delta;} and mtb2 = {typ_mp=mp; typ_expr=mb.mod_type; typ_expr_alg=None; - typ_constraints=Univ.Constraint.empty; - typ_delta = mb.mod_delta;}; + typ_constraints=Univ.empty_constraint; + typ_delta = mb.mod_delta;} in let env = add_module (module_body_of_type mp mtb1) env in check_subtypes env mtb1 mtb2 |