Skip to content

Commit

Permalink
La notation 'with'. L'interpretation - version preliminaire
Browse files Browse the repository at this point in the history 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2975 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information
coq committed Aug 19, 2002
1 parent f0591d4 commit 04dfb01
Show file tree
Hide file tree
Showing 13 changed files with 228 additions and 69 deletions.
26 changes: 14 additions & 12 deletions .depend
View file
Expand Up @@ -448,19 +448,19 @@ kernel/inductive.cmx: kernel/declarations.cmx kernel/environ.cmx \
kernel/names.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx kernel/inductive.cmi
kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \
kernel/environ.cmi kernel/names.cmi kernel/term.cmi lib/util.cmi \
kernel/modops.cmi
kernel/environ.cmi kernel/names.cmi kernel/term.cmi kernel/univ.cmi \
lib/util.cmi kernel/modops.cmi
kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \
kernel/environ.cmx kernel/names.cmx kernel/term.cmx lib/util.cmx \
kernel/modops.cmi
kernel/environ.cmx kernel/names.cmx kernel/term.cmx kernel/univ.cmx \
lib/util.cmx kernel/modops.cmi
kernel/mod_typing.cmo: kernel/declarations.cmi kernel/entries.cmi \
kernel/environ.cmi kernel/modops.cmi kernel/names.cmi \
kernel/subtyping.cmi kernel/term_typing.cmi kernel/univ.cmi lib/util.cmi \
kernel/mod_typing.cmi
kernel/reduction.cmi kernel/subtyping.cmi kernel/term_typing.cmi \
kernel/typeops.cmi kernel/univ.cmi lib/util.cmi kernel/mod_typing.cmi
kernel/mod_typing.cmx: kernel/declarations.cmx kernel/entries.cmx \
kernel/environ.cmx kernel/modops.cmx kernel/names.cmx \
kernel/subtyping.cmx kernel/term_typing.cmx kernel/univ.cmx lib/util.cmx \
kernel/mod_typing.cmi
kernel/reduction.cmx kernel/subtyping.cmx kernel/term_typing.cmx \
kernel/typeops.cmx kernel/univ.cmx lib/util.cmx kernel/mod_typing.cmi
kernel/names.cmo: lib/hashcons.cmi lib/pp.cmi lib/predicate.cmi lib/util.cmi \
kernel/names.cmi
kernel/names.cmx: lib/hashcons.cmx lib/pp.cmx lib/predicate.cmx lib/util.cmx \
Expand Down Expand Up @@ -674,11 +674,13 @@ parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx parsing/genarg.cmx \
library/libnames.cmx kernel/names.cmx lib/pp.cmx proofs/tacexpr.cmx \
lib/util.cmx parsing/ast.cmi
parsing/astmod.cmo: parsing/astterm.cmi parsing/coqast.cmi kernel/entries.cmi \
library/lib.cmi library/libnames.cmi kernel/modops.cmi kernel/names.cmi \
library/nametab.cmi lib/pp.cmi lib/util.cmi parsing/astmod.cmi
pretyping/evd.cmi library/global.cmi library/lib.cmi library/libnames.cmi \
kernel/modops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
lib/util.cmi parsing/astmod.cmi
parsing/astmod.cmx: parsing/astterm.cmx parsing/coqast.cmx kernel/entries.cmx \
library/lib.cmx library/libnames.cmx kernel/modops.cmx kernel/names.cmx \
library/nametab.cmx lib/pp.cmx lib/util.cmx parsing/astmod.cmi
pretyping/evd.cmx library/global.cmx library/lib.cmx library/libnames.cmx \
kernel/modops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
lib/util.cmx parsing/astmod.cmi
parsing/astterm.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \
lib/dyn.cmi kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \
library/global.cmi library/impargs.cmi library/libnames.cmi \
Expand Down
8 changes: 5 additions & 3 deletions kernel/declarations.ml
View file
Expand Up @@ -148,7 +148,8 @@ and module_expr_body =
| MEBapply of module_expr_body * module_expr_body
* constraints

and module_specification_body = module_type_body * module_path option
and module_specification_body =
module_type_body * module_path option * constraints

and structure_elem_body =
| SEBconst of constant_body
Expand All @@ -160,6 +161,7 @@ and module_structure_body = (label * structure_elem_body) list

and module_body =
{ mod_expr : module_expr_body option;
mod_user_type : (module_type_body * constraints) option;
mod_user_type : module_type_body option;
mod_type : module_type_body;
mod_equiv : module_path option }
mod_equiv : module_path option;
mod_constraints : constraints }
8 changes: 5 additions & 3 deletions kernel/declarations.mli
View file
Expand Up @@ -107,7 +107,8 @@ and module_expr_body =
| MEBapply of module_expr_body * module_expr_body
* constraints

and module_specification_body = module_type_body * module_path option
and module_specification_body =
module_type_body * module_path option * constraints

and structure_elem_body =
| SEBconst of constant_body
Expand All @@ -119,9 +120,10 @@ and module_structure_body = (label * structure_elem_body) list

and module_body =
{ mod_expr : module_expr_body option;
mod_user_type : (module_type_body * constraints) option;
mod_user_type : module_type_body option;
mod_type : module_type_body;
mod_equiv : module_path option }
mod_equiv : module_path option;
mod_constraints : constraints }



Expand Down
5 changes: 4 additions & 1 deletion kernel/entries.ml
View file
Expand Up @@ -78,10 +78,13 @@ and module_type_entry =
MTEident of kernel_name
| MTEfunsig of mod_bound_id * module_type_entry * module_type_entry
| MTEsig of mod_self_id * module_signature_entry
| MTEwith of module_type_entry * with_declaration

and module_signature_entry = (label * specification_entry) list


and with_declaration =
With_Module of identifier * module_path
| With_Definition of identifier * constr

and module_expr =
MEident of module_path
Expand Down
5 changes: 4 additions & 1 deletion kernel/entries.mli
View file
Expand Up @@ -78,10 +78,13 @@ and module_type_entry =
MTEident of kernel_name
| MTEfunsig of mod_bound_id * module_type_entry * module_type_entry
| MTEsig of mod_self_id * module_signature_entry
| MTEwith of module_type_entry * with_declaration

and module_signature_entry = (label * specification_entry) list


and with_declaration =
With_Module of identifier * module_path
| With_Definition of identifier * constr

and module_expr =
MEident of module_path
Expand Down
99 changes: 85 additions & 14 deletions kernel/mod_typing.ml
View file
Expand Up @@ -24,6 +24,15 @@ let path_of_mexpr = function
| MEident mb -> mb
| _ -> raise Not_path

let rec replace_first p k = function
| [] -> []
| h::t when p h -> k::t
| h::t -> h::(replace_first p k t)

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 rec list_fold_map2 f e = function
| [] -> (e,[],[])
Expand All @@ -47,6 +56,70 @@ let rec translate_modtype env mte =
| MTEsig (msid,sig_e) ->
let str_b,sig_b = translate_entry_list env msid false sig_e in
MTBsig (msid,sig_b)
| MTEwith (mte, with_decl) ->
let mtb = translate_modtype env mte in
merge_with env mtb with_decl

and merge_with env mtb with_decl =
let msid,sig_b = match (Modops.scrape_modtype env mtb) with
| MTBsig(msid,sig_b) -> msid,sig_b
| _ -> error_signature_expected mtb
in
let id = match with_decl with
| With_Definition (id,_) | With_Module (id,_) -> id
in
let l = label_of_id id in
try
let rev_before,spec,after = list_split_assoc l [] sig_b in
let before = List.rev rev_before in
let env' = Modops.add_signature (MPself msid) before env in
let new_spec = match with_decl with
| With_Definition (id,c) ->
let cb = match spec with
SPBconst cb -> cb
| _ -> error_not_a_constant l
in
begin
match cb.const_body with
| None ->
let (j,cst1) = Typeops.infer env' c in
let cst2 =
Reduction.conv_leq env' j.uj_type cb.const_type in
let cst =
Constraint.union
(Constraint.union cb.const_constraints cst1)
cst2
in
SPBconst {cb with
const_body = Some j.uj_val;
const_constraints = cst}
| Some b ->
let cst1 = Reduction.conv env' c b in
let cst = Constraint.union cb.const_constraints cst1 in
SPBconst {cb with
const_body = Some c;
const_constraints = cst}
end
| With_Module (id, mp) ->
let (oldmtb,oldequiv,oldcst) = match spec with
SPBmodule (mtb,equiv,cst) -> (mtb,equiv,cst)
| _ -> error_not_a_module (string_of_label l)
in
let mtb = type_modpath env' mp in
let cst = check_subtypes env' mtb oldmtb in
let equiv =
match oldequiv with
| None -> Some mp
| Some mp' ->
check_modpath_equiv env' mp mp';
Some mp
in
SPBmodule (mtb, equiv, Constraint.union oldcst cst)
in
MTBsig(msid, before@(l,new_spec)::after)
with
Not_found -> error_no_such_label l
| Reduction.NotConvertible -> error_with_incorrect l

and translate_entry_list env msid is_definition sig_e =
let mp = MPself msid in
Expand All @@ -61,7 +134,7 @@ and translate_entry_list env msid is_definition sig_e =
add_mind kn mib env, (l, SEBmind mib), (l, SPBmind mib)
| SPEmodule me ->
let mb = translate_module env is_definition me in
let mspec = mb.mod_type, mb.mod_equiv in
let mspec = mb.mod_type, mb.mod_equiv, mb.mod_constraints in
let mp' = MPdot (mp,l) in
add_module mp' mb env, (l, SEBmodule mb), (l, SPBmodule mspec)
| SPEmodtype mte ->
Expand All @@ -82,9 +155,10 @@ and translate_module env is_definition me =
| None, Some mte ->
let mtb = translate_modtype env mte in
{ mod_expr = None;
mod_user_type = Some (mtb, Constraint.empty);
mod_user_type = Some mtb;
mod_type = mtb;
mod_equiv = None }
mod_equiv = None;
mod_constraints = Constraint.empty }
| Some mexpr, _ ->
let meq_o = (* do we have a transparent module ? *)
try (* TODO: transparent field in module_entry *)
Expand All @@ -104,17 +178,18 @@ and translate_module env is_definition me =
in
MEBident mp, type_modpath env mp
in
let mtb,mod_user_type =
let mtb, mod_user_type, cst =
match me.mod_entry_type with
| None -> mtb1, None
| None -> mtb1, None, Constraint.empty
| Some mte ->
let mtb2 = translate_modtype env mte in
mtb2, Some (mtb2, check_subtypes env mtb1 mtb2)
mtb2, Some mtb2, check_subtypes env mtb1 mtb2
in
{ mod_type = mtb;
mod_user_type = mod_user_type;
mod_expr = Some meb;
mod_equiv = meq_o }
mod_equiv = meq_o;
mod_constraints = cst }

(* translate_mexpr : env -> module_expr -> module_expr_body * module_type_body *)
and translate_mexpr env mexpr = match mexpr with
Expand Down Expand Up @@ -180,12 +255,7 @@ and add_module_constraints env mb =
| None -> env
| Some meb -> add_module_expr_constraints env meb
in
let env = match mb.mod_user_type with
| None -> env
| Some (mtb,cst) ->
Environ.add_constraints cst (add_modtype_constraints env mtb)
in
env
Environ.add_constraints mb.mod_constraints env

and add_modtype_constraints env = function
| MTBident _ -> env
Expand All @@ -202,7 +272,8 @@ and add_modtype_constraints env = function
and add_sig_elem_constraints env = function
| SPBconst cb -> Environ.add_constraints cb.const_constraints env
| SPBmind mib -> Environ.add_constraints mib.mind_constraints env
| SPBmodule (mtb,_) -> add_modtype_constraints env mtb
| SPBmodule (mtb,_,cst) ->
add_modtype_constraints (Environ.add_constraints cst env) mtb
| SPBmodtype mtb -> add_modtype_constraints env mtb


34 changes: 23 additions & 11 deletions kernel/modops.ml
View file
Expand Up @@ -11,6 +11,7 @@
(*i*)
open Util
open Names
open Univ
open Term
open Declarations
open Environ
Expand Down Expand Up @@ -41,6 +42,9 @@ let error_incompatible_labels l l' =
let error_result_must_be_signature mtb =
error "The result module type must be a signature"

let error_signature_expected mtb =
error "Signature expected"

let error_no_module_to_end _ =
error "No open module to end"

Expand All @@ -53,25 +57,33 @@ let error_not_a_modtype s =
let error_not_a_module s =
error ("\""^s^"\" is not a module")

let error_not_a_constant l =
error ("\""^(string_of_label l)^"\" is not a constant")

let error_with_incorrect l =
error ("Incorrect constraint for label \""^(string_of_label l)^"\"")

let rec scrape_modtype env = function
| MTBident kn -> scrape_modtype env (lookup_modtype kn env)
| mtb -> mtb


let module_body_of_spec spec =
{ mod_type = fst spec;
mod_equiv = snd spec;
mod_expr = None;
mod_user_type = None}
let module_body_of_spec (mty,mpo,cst) =
{ mod_type = mty;
mod_equiv = mpo;
mod_expr = None;
mod_user_type = None;
mod_constraints = cst}

let module_body_of_type mtb =
{ mod_type = mtb;
mod_equiv = None;
mod_expr = None;
mod_user_type = None}
mod_user_type = None;
mod_constraints = Constraint.empty}


let module_spec_of_body mb = mb.mod_type, mb.mod_equiv
let module_spec_of_body mb = mb.mod_type, mb.mod_equiv, mb.mod_constraints

let destr_functor = function
| MTBfunsig (arg_id,arg_t,body_t) -> (arg_id,arg_t,body_t)
Expand Down Expand Up @@ -114,11 +126,11 @@ and subst_signature sub sign =
in
List.map (fun (l,b) -> (l,subst_body b)) sign

and subst_module sub (mtb,mpo as mb) =
and subst_module sub (mtb,mpo,cst as mb) =
let mtb' = subst_modtype sub mtb in
let mpo' = option_smartmap (subst_mp sub) mpo in
if mtb'==mtb && mpo'==mpo then mb else
(mtb',mpo')
(mtb',mpo',cst)

let subst_signature_msid msid mp =
subst_signature (map_msid msid mp)
Expand Down Expand Up @@ -161,13 +173,13 @@ let rec strengthen_mtb env mp mtb = match scrape_modtype env mtb with
| MTBident _ -> anomaly "scrape_modtype does not work!"
| MTBfunsig _ -> mtb
| MTBsig (msid,sign) -> MTBsig (msid,strengthen_sig env msid sign mp)
and strengthen_mod env mp (mtb,mpo) =
and strengthen_mod env mp (mtb,mpo,cst) =
let mtb' = strengthen_mtb env mp mtb in
let mpo' = match mpo with
| Some _ -> mpo
| None -> Some mp
in
(mtb',mpo')
(mtb',mpo',cst)
and strengthen_sig env msid sign mp = match sign with
| [] -> []
| (l,SPBconst cb) :: rest ->
Expand Down
6 changes: 6 additions & 0 deletions kernel/modops.mli
View file
Expand Up @@ -74,10 +74,16 @@ val error_no_such_label : label -> 'a

val error_result_must_be_signature : module_type_body -> 'a

val error_signature_expected : module_type_body -> 'a

val error_no_module_to_end : unit -> 'a

val error_no_modtype_to_end : unit -> 'a

val error_not_a_modtype : string -> 'a

val error_not_a_module : string -> 'a

val error_not_a_constant : label -> 'a

val error_with_incorrect : label -> 'a

0 comments on commit 04dfb01

Please sign in to comment.