From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- kernel/safe_typing.ml | 572 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 572 insertions(+) create mode 100644 kernel/safe_typing.ml (limited to 'kernel/safe_typing.ml') diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml new file mode 100644 index 00000000..4f180599 --- /dev/null +++ b/kernel/safe_typing.ml @@ -0,0 +1,572 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* () in + Environ.push_named d env + +let push_named_def (id,b,topt) senv = + let (c,typ,cst) = translate_local_def senv.env (b,topt) in + let env' = add_constraints cst senv.env in + let env'' = safe_push_named (id,Some c,typ) env' in + (cst, {senv with env=env''}) + +let push_named_assum (id,t) senv = + let (t,cst) = translate_local_assum senv.env t in + let env' = add_constraints cst senv.env in + let env'' = safe_push_named (id,None,t) env' in + (cst, {senv with env=env''}) + + +(* Insertion of constants and parameters in environment. *) + +type global_declaration = + | ConstantEntry of constant_entry + | GlobalRecipe of Cooking.recipe + +let hcons_constant_body cb = + let body = match cb.const_body with + None -> None + | Some l_constr -> let constr = Declarations.force l_constr in + Some (Declarations.from_val (hcons1_constr constr)) + in + { cb with + const_body = body; + const_type = hcons1_constr cb.const_type } + +let add_constant dir l decl senv = + check_label l senv.labset; + let cb = match decl with + ConstantEntry ce -> translate_constant senv.env ce + | GlobalRecipe r -> + let cb = translate_recipe senv.env r in + if dir = empty_dirpath then hcons_constant_body cb else cb + in +(* let cb = if dir = empty_dirpath then hcons_constant_body cb else cb in*) + let env' = Environ.add_constraints cb.const_constraints senv.env in + let kn = make_kn senv.modinfo.modpath dir l in + let env'' = Environ.add_constant kn cb env' in + kn, { old = senv.old; + env = env''; + modinfo = senv.modinfo; + labset = Labset.add l senv.labset; + revsign = (l,SPBconst cb)::senv.revsign; + revstruct = (l,SEBconst cb)::senv.revstruct; + imports = senv.imports; + loads = senv.loads } + + +(* Insertion of inductive types. *) + +let add_mind dir l mie senv = + if mie.mind_entry_inds = [] then + anomaly "empty inductive types declaration"; + (* this test is repeated by translate_mind *) + let id = (List.nth mie.mind_entry_inds 0).mind_entry_typename in + if l <> label_of_id id then + anomaly ("the label of inductive packet and its first inductive"^ + " type do not match"); + check_label l senv.labset; + (* TODO: when we will allow reorderings we will have to verify + all labels *) + let mib = translate_mind senv.env mie in + let env' = Environ.add_constraints mib.mind_constraints senv.env in + let kn = make_kn senv.modinfo.modpath dir l in + let env'' = Environ.add_mind kn mib env' in + kn, { old = senv.old; + env = env''; + modinfo = senv.modinfo; + labset = Labset.add l senv.labset; (* TODO: the same as above *) + revsign = (l,SPBmind mib)::senv.revsign; + revstruct = (l,SEBmind mib)::senv.revstruct; + imports = senv.imports; + loads = senv.loads } + + +(* Insertion of module types *) + +let add_modtype l mte senv = + check_label l senv.labset; + let mtb = translate_modtype senv.env mte in + let env' = add_modtype_constraints senv.env mtb in + let kn = make_kn senv.modinfo.modpath empty_dirpath l in + let env'' = Environ.add_modtype kn mtb env' in + kn, { old = senv.old; + env = env''; + modinfo = senv.modinfo; + labset = Labset.add l senv.labset; + revsign = (l,SPBmodtype mtb)::senv.revsign; + revstruct = (l,SEBmodtype mtb)::senv.revstruct; + imports = senv.imports; + loads = senv.loads } + + + +(* full_add_module adds module with universes and constraints *) +let full_add_module mp mb env = + let env = add_module_constraints env mb in + let env = Modops.add_module mp mb env in + env + +(* Insertion of modules *) + +let add_module l me senv = + check_label l senv.labset; + let mb = translate_module senv.env me in + let mspec = module_spec_of_body mb in + let mp = MPdot(senv.modinfo.modpath, l) in + let env' = full_add_module mp mb senv.env in + mp, { old = senv.old; + env = env'; + modinfo = senv.modinfo; + labset = Labset.add l senv.labset; + revsign = (l,SPBmodule mspec)::senv.revsign; + revstruct = (l,SEBmodule mb)::senv.revstruct; + imports = senv.imports; + loads = senv.loads } + + +(* Interactive modules *) + +let start_module l params result senv = + check_label l senv.labset; + let rec trans_params env = function + | [] -> env,[] + | (mbid,mte)::rest -> + let mtb = translate_modtype env mte in + let env = + full_add_module (MPbound mbid) (module_body_of_type mtb) env + in + let env,transrest = trans_params env rest in + env, (mbid,mtb)::transrest + in + let env,params_body = trans_params senv.env params in + let check_sig mtb = match scrape_modtype env mtb with + | MTBsig _ -> () + | MTBfunsig _ -> error_result_must_be_signature mtb + | _ -> anomaly "start_module: modtype not scraped" + in + let result_body = option_app (translate_modtype env) result in + ignore (option_app check_sig result_body); + let msid = make_msid senv.modinfo.seed (string_of_label l) in + let mp = MPself msid in + let modinfo = { msid = msid; + modpath = mp; + seed = senv.modinfo.seed; + label = l; + variant = STRUCT(params_body,result_body) } + in + mp, { old = senv; + env = env; + modinfo = modinfo; + labset = Labset.empty; + revsign = []; + revstruct = []; + imports = senv.imports; + loads = [] } + + + +let end_module l senv = + let oldsenv = senv.old in + let modinfo = senv.modinfo in + let params, restype = + match modinfo.variant with + | NONE | LIBRARY _ | SIG _ -> error_no_module_to_end () + | STRUCT(params,restype) -> (params,restype) + in + if l <> modinfo.label then error_incompatible_labels l modinfo.label; + if not (empty_context senv.env) then error_local_context None; + let functorize_type = + List.fold_right + (fun (arg_id,arg_b) mtb -> MTBfunsig (arg_id,arg_b,mtb)) + params + in + let auto_tb = MTBsig (modinfo.msid, List.rev senv.revsign) in + let mtb, mod_user_type, cst = + match restype with + | None -> functorize_type auto_tb, None, Constraint.empty + | Some res_tb -> + let cst = check_subtypes senv.env auto_tb res_tb in + let mtb = functorize_type res_tb in + mtb, Some mtb, cst + in + let mexpr = + List.fold_right + (fun (arg_id,arg_b) mtb -> MEBfunctor (arg_id,arg_b,mtb)) + params + (MEBstruct (modinfo.msid, List.rev senv.revstruct)) + in + let mb = + { mod_expr = Some mexpr; + mod_user_type = mod_user_type; + mod_type = mtb; + mod_equiv = None; + mod_constraints = cst } + in + let mspec = + { msb_modtype = mtb; + msb_equiv = None; + msb_constraints = Constraint.empty } + in + let mp = MPdot (oldsenv.modinfo.modpath, l) in + let newenv = oldsenv.env in + let newenv = + List.fold_left + (fun env (mp,mb) -> full_add_module mp mb env) + newenv + senv.loads + in + let newenv = + full_add_module mp mb newenv + in + mp, { old = oldsenv.old; + env = newenv; + modinfo = oldsenv.modinfo; + labset = Labset.add l oldsenv.labset; + revsign = (l,SPBmodule mspec)::oldsenv.revsign; + revstruct = (l,SEBmodule mb)::oldsenv.revstruct; + imports = senv.imports; + loads = senv.loads@oldsenv.loads } + + +(* Interactive module types *) + +let start_modtype l params senv = + check_label l senv.labset; + let rec trans_params env = function + | [] -> env,[] + | (mbid,mte)::rest -> + let mtb = translate_modtype env mte in + let env = + full_add_module (MPbound mbid) (module_body_of_type mtb) env + in + let env,transrest = trans_params env rest in + env, (mbid,mtb)::transrest + in + let env,params_body = trans_params senv.env params in + let msid = make_msid senv.modinfo.seed (string_of_label l) in + let mp = MPself msid in + let modinfo = { msid = msid; + modpath = mp; + seed = senv.modinfo.seed; + label = l; + variant = SIG params_body } + in + mp, { old = senv; + env = env; + modinfo = modinfo; + labset = Labset.empty; + revsign = []; + revstruct = []; + imports = senv.imports; + loads = [] } + +let end_modtype l senv = + let oldsenv = senv.old in + let modinfo = senv.modinfo in + let params = + match modinfo.variant with + | LIBRARY _ | NONE | STRUCT _ -> error_no_modtype_to_end () + | SIG params -> params + in + if l <> modinfo.label then error_incompatible_labels l modinfo.label; + if not (empty_context senv.env) then error_local_context None; + let res_tb = MTBsig (modinfo.msid, List.rev senv.revsign) in + let mtb = + List.fold_right + (fun (arg_id,arg_b) mtb -> MTBfunsig (arg_id,arg_b,mtb)) + params + res_tb + in + let kn = make_kn oldsenv.modinfo.modpath empty_dirpath l in + let newenv = oldsenv.env in + let newenv = + List.fold_left + (fun env (mp,mb) -> full_add_module mp mb env) + newenv + senv.loads + in + let newenv = + add_modtype_constraints newenv mtb + in + let newenv = + Environ.add_modtype kn mtb newenv + in + kn, { old = oldsenv.old; + env = newenv; + modinfo = oldsenv.modinfo; + labset = Labset.add l oldsenv.labset; + revsign = (l,SPBmodtype mtb)::oldsenv.revsign; + revstruct = (l,SEBmodtype mtb)::oldsenv.revstruct; + imports = senv.imports; + loads = senv.loads@oldsenv.loads } + + +let current_modpath senv = senv.modinfo.modpath +let current_msid senv = senv.modinfo.msid + + +let add_constraints cst senv = + {senv with env = Environ.add_constraints cst senv.env} + +(* Check that the engagement expected by a library matches the initial one *) +let check_engagement env c = + match Environ.engagement env, c with + | Some ImpredicativeSet, Some ImpredicativeSet -> () + | _, None -> () + | _, Some ImpredicativeSet -> + error "Needs option -impredicative-set" + +let set_engagement c senv = + {senv with env = Environ.set_engagement c senv.env} + + +(* Libraries = Compiled modules *) + +type compiled_library = + dir_path * module_body * library_info list * engagement option + + +(* We check that only initial state Require's were performed before + [start_library] was called *) + +let start_library dir senv = + if not (senv.revsign = [] && + senv.modinfo.msid = initial_msid && + senv.modinfo.variant = NONE) + then + anomaly "Safe_typing.start_library: environment should be empty"; + let dir_path,l = + match (repr_dirpath dir) with + [] -> anomaly "Empty dirpath in Safe_typing.start_library" + | hd::tl -> + make_dirpath tl, label_of_id hd + in + let msid = make_msid dir_path (string_of_label l) in + let mp = MPself msid in + let modinfo = { msid = msid; + modpath = mp; + seed = dir; + label = l; + variant = LIBRARY dir } + in + mp, { old = senv; + env = senv.env; + modinfo = modinfo; + labset = Labset.empty; + revsign = []; + revstruct = []; + imports = senv.imports; + loads = [] } + + +let export senv dir = + let modinfo = senv.modinfo in + begin + match modinfo.variant with + | LIBRARY dp -> + if dir <> dp then + anomaly "We are not exporting the right library!" + | _ -> + anomaly "We are not exporting the library" + end; + (*if senv.modinfo.params <> [] || senv.modinfo.restype <> None then + (* error_export_simple *) (); *) + let mb = + { mod_expr = Some (MEBstruct (modinfo.msid, List.rev senv.revstruct)); + mod_type = MTBsig (modinfo.msid, List.rev senv.revsign); + mod_user_type = None; + mod_equiv = None; + mod_constraints = Constraint.empty } + in + modinfo.msid, (dir,mb,senv.imports,engagement senv.env) + + +let check_imports senv needed = + let imports = senv.imports in + let check (id,stamp) = + try + let actual_stamp = List.assoc id imports in + if stamp <> actual_stamp then + error ("Inconsistent assumptions over module " ^(string_of_dirpath id)) + with Not_found -> + error ("Reference to unknown module " ^ (string_of_dirpath id)) + in + List.iter check needed + +(* we have an inefficiency: Since loaded files are added to the +environment every time a module is closed, their components are +calculated many times. Thic could be avoided in several ways: + +1 - for each file create a dummy environment containing only this +file's components, merge this environment with the global +environment, and store for the future (instead of just its type) + +2 - create "persistent modules" environment table in Environ add put +loaded by side-effect once and for all (like it is done in OCaml). +Would this be correct with respect to undo's and stuff ? +*) + +let import (dp,mb,depends,engmt) digest senv = + check_imports senv depends; + check_engagement senv.env engmt; + let mp = MPfile dp in + let env = senv.env in + mp, { senv with + env = full_add_module mp mb env; + imports = (dp,digest)::senv.imports; + loads = (mp,mb)::senv.loads } + + +(** Remove the body of opaque constants in modules *) + +let rec lighten_module mb = + { mb with + mod_expr = option_app lighten_modexpr mb.mod_expr; + mod_type = lighten_modtype mb.mod_type; + mod_user_type = option_app lighten_modtype mb.mod_user_type } + +and lighten_modtype = function + | MTBident kn as x -> x + | MTBfunsig (mbid,mtb1,mtb2) -> + MTBfunsig (mbid, lighten_modtype mtb1, lighten_modtype mtb2) + | MTBsig (msid,sign) -> MTBsig (msid, lighten_sig sign) + +and lighten_modspec ms = + { ms with msb_modtype = lighten_modtype ms.msb_modtype } + +and lighten_sig sign = + let lighten_spec (l,spec) = (l,match spec with + | SPBconst ({const_opaque=true} as x) -> SPBconst {x with const_body=None} + | (SPBconst _ | SPBmind _) as x -> x + | SPBmodule m -> SPBmodule (lighten_modspec m) + | SPBmodtype m -> SPBmodtype (lighten_modtype m)) + in + List.map lighten_spec sign + +and lighten_struct struc = + let lighten_body (l,body) = (l,match body with + | SEBconst ({const_opaque=true} as x) -> SEBconst {x with const_body=None} + | (SEBconst _ | SEBmind _) as x -> x + | SEBmodule m -> SEBmodule (lighten_module m) + | SEBmodtype m -> SEBmodtype (lighten_modtype m)) + in + List.map lighten_body struc + +and lighten_modexpr = function + | MEBfunctor (mbid,mty,mexpr) -> + MEBfunctor (mbid,lighten_modtype mty,lighten_modexpr mexpr) + | MEBident mp as x -> x + | MEBstruct (msid, struc) -> + MEBstruct (msid, lighten_struct struc) + | MEBapply (mexpr,marg,u) -> + MEBapply (lighten_modexpr mexpr,lighten_modexpr marg,u) + +let lighten_library (dp,mb,depends,s) = (dp,lighten_module mb,depends,s) + + +type judgment = unsafe_judgment + +let j_val j = j.uj_val +let j_type j = j.uj_type + +let safe_infer senv = infer (env_of_senv senv) + +let typing senv = Typeops.typing (env_of_senv senv) -- cgit v1.2.3