diff options
| -rw-r--r-- | dev/top_printers.ml | 3 | ||||
| -rw-r--r-- | kernel/subtyping.ml | 12 | ||||
| -rw-r--r-- | library/declaremods.ml | 26 | ||||
| -rwxr-xr-x | library/nametab.ml | 16 | ||||
| -rwxr-xr-x | library/nametab.mli | 2 | ||||
| -rw-r--r-- | test-suite/modules/Nametab.v | 110 | ||||
| -rw-r--r-- | test-suite/modules/Przyklad.v | 32 | ||||
| -rw-r--r-- | test-suite/modules/fun_objects.v | 20 | ||||
| -rw-r--r-- | test-suite/modules/grammar.v | 10 | ||||
| -rw-r--r-- | test-suite/modules/modul.v | 8 | ||||
| -rw-r--r-- | test-suite/modules/modulik.v | 5 | ||||
| -rw-r--r-- | test-suite/modules/obj.v | 14 | ||||
| -rw-r--r-- | test-suite/modules/objects.v | 20 | ||||
| -rw-r--r-- | test-suite/modules/sub_objects.v | 16 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 16 |
15 files changed, 188 insertions, 122 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 0339a8fdd..62fc841e6 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -34,7 +34,8 @@ let prast c = pp(print_ast c) let prastpat c = pp(print_astpat c) let prastpatl c = pp(print_astlpat c) -let ppterm = (fun x -> pp(prterm x)) +let ppterm x = pp(prterm x) +let ppterm_univ x = Termast.with_universes ppterm x let pprawterm = (fun x -> pp(pr_rawterm x)) let pppattern = (fun x -> pp(pr_pattern x)) let pptype = (fun x -> pp(prtype x)) diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 5a7ce3cb3..4b4ae17cf 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -145,6 +145,17 @@ let check_constant cst env msid1 l info1 cb2 spec2 = | _ -> error () in assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ; + (*Start by checking bodies*) + match cb2.const_body with + | None -> check_conv cst conv_leq env cb1.const_type cb2.const_type + | Some c2 -> (* no checking types ! *) + let c1 = match cb1.const_body with + | None -> mkConst (make_kn (MPself msid1) empty_dirpath l) + | Some c1 -> c1 + in + check_conv cst conv env c1 c2 + +(* (*Start by checking types*) let cst = check_conv cst conv_leq env cb1.const_type cb2.const_type in match cb1.const_body, cb2.const_body with | None, None -> cst @@ -158,6 +169,7 @@ let check_constant cst env msid1 l info1 cb2 spec2 = env (mkConst (make_kn (MPself msid1) empty_dirpath l)) c2 +*) let rec check_modules cst env msid1 l msb1 msb2 = let cst = check_modtypes cst env (fst msb1) (fst msb2) false in diff --git a/library/declaremods.ml b/library/declaremods.ml index 76ed46619..7b5adfdc9 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -549,28 +549,38 @@ let declare_modtype id mte = -let rec get_module_substobjs = function - MEident mp -> MPmap.find mp !modtab_substobjs - | MEfunctor (mbid,_,mexpr) -> - let (subst, mbids, msid, objs) = get_module_substobjs mexpr in +let rec get_module_substobjs locals = function + MEident (MPbound mbid as mp) -> + begin + try + let mty = List.assoc mbid locals in + get_modtype_substobjs mty + with + Not_found -> MPmap.find mp !modtab_substobjs + end + | MEident mp -> MPmap.find mp !modtab_substobjs + | MEfunctor (mbid,mty,mexpr) -> + let (subst, mbids, msid, objs) = + get_module_substobjs ((mbid,mty)::locals) mexpr + in (subst, mbid::mbids, msid, objs) | MEstruct (msid,_) -> (empty_subst, [], msid, []) | MEapply (mexpr, MEident mp) -> - let (subst, mbids, msid, objs) = get_module_substobjs mexpr in + let (subst, mbids, msid, objs) = get_module_substobjs locals mexpr in (match mbids with | mbid::mbids -> (add_mbid mbid mp subst, mbids, msid, objs) | [] -> anomaly "Too few arguments in functor") - | MEapply (_,_) -> - anomaly "The argument of a module application must be a path!" + | MEapply (_,mexpr) -> + Modops.error_application_to_not_path mexpr let declare_module id me = let substobjs = match me with | {mod_entry_type = Some mte} -> get_modtype_substobjs mte - | {mod_entry_expr = Some mexpr} -> get_module_substobjs mexpr + | {mod_entry_expr = Some mexpr} -> get_module_substobjs [] mexpr | _ -> anomaly "declare_module: No type, no body ..." in let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in diff --git a/library/nametab.ml b/library/nametab.ml index c80675aec..bc419a237 100755 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -32,14 +32,14 @@ type 'a path_status = Nothing | Relative of 'a | Absolute of 'a (* Dictionaries of short names *) type 'a nametree = ('a path_status * 'a nametree ModIdmap.t) type ccitab = extended_global_reference nametree Idmap.t -type kntab = kernel_name nametree Idmap.t +type knsptab = (kernel_name * section_path) nametree Idmap.t type objtab = section_path nametree Idmap.t type dirtab = global_dir_reference nametree ModIdmap.t let the_ccitab = ref (Idmap.empty : ccitab) let the_dirtab = ref (ModIdmap.empty : dirtab) let the_objtab = ref (Idmap.empty : objtab) -let the_modtypetab = ref (Idmap.empty : kntab) +let the_modtypetab = ref (Idmap.empty : knsptab) (* This table translates extended_global_references back to section paths *) module Globtab = Map.Make(struct type t=extended_global_reference @@ -194,7 +194,7 @@ let push_syntactic_definition visibility sp kn = let push = push_cci -let push_modtype = push_idtree the_modtypetab +let push_modtype vis sp kn = push_idtree the_modtypetab vis sp (kn,sp) (* This is for dischargeable non-cci objects (removed at the end of the @@ -257,7 +257,8 @@ let locate_syntactic_definition qid = match extended_locate qid with | TrueGlobal _ -> raise Not_found | SyntacticDef kn -> kn -let locate_modtype qid = get (find_modtype qid) +let full_name_modtype qid = get (find_modtype qid) +let locate_modtype qid = fst (get (find_modtype qid)) let locate_obj qid = get (find_in_idtree the_objtab qid) @@ -376,24 +377,27 @@ let global_inductive (loc,qid as locqid) = (********************************************************************) (* Registration of tables as a global table and rollback *) -type frozen = ccitab * dirtab * objtab * globtab +type frozen = ccitab * dirtab * objtab * knsptab * globtab let init () = the_ccitab := Idmap.empty; the_dirtab := ModIdmap.empty; the_objtab := Idmap.empty; + the_modtypetab := Idmap.empty; the_globtab := Globtab.empty let freeze () = !the_ccitab, !the_dirtab, !the_objtab, + !the_modtypetab, !the_globtab -let unfreeze (mc,md,mo,gt) = +let unfreeze (mc,md,mo,mt,gt) = the_ccitab := mc; the_dirtab := md; the_objtab := mo; + the_modtypetab := mt; the_globtab := gt let _ = diff --git a/library/nametab.mli b/library/nametab.mli index b64fe0d9d..626a529e6 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -120,6 +120,8 @@ val exists_dir : dir_path -> bool val exists_section : dir_path -> bool (* deprecated *) val exists_module : dir_path -> bool (* deprecated *) +val full_name_modtype : qualid -> kernel_name * section_path + (*s Roots of the space of absolute names *) (* This turns a "user" absolute name into a global reference; diff --git a/test-suite/modules/Nametab.v b/test-suite/modules/Nametab.v index 9d8c49ef7..9773bc6f4 100644 --- a/test-suite/modules/Nametab.v +++ b/test-suite/modules/Nametab.v @@ -1,35 +1,35 @@ -Module M. - Definition id:=[x:Set]x. - Module M. - Definition zero:(id nat):= O. - Definition id:=Set. - Definition nacik:id:=nat. - End M. -End M. - -Module M. +Module Q. Module N. Module K. Definition id:=Set. End K. End N. -End M. - +End Q. Locate id. Locate K.id. Locate N.K.id. -Locate M.N.K.id. -Locate Top.M.N.K.id. +Locate Q.N.K.id. +Locate Top.Q.N.K.id. Locate K. Locate N.K. -Locate M.N.K. -Locate Scratch.M.N.K. +Locate Q.N.K. +Locate Top.Q.N.K. Locate N. -Locate M.N. -Locate Scratch.M.N. -Locate M. -Locate Scratch.M. +Locate Q.N. +Locate Top.Q.N. +Locate Q. +Locate Top.Q. + + +Module Type SIG. +End SIG. + +Module Type FSIG[X:SIG]. +End FSIG. + +Module F[X:SIG]. +End F. (* #trace Nametab.push;; @@ -40,46 +40,74 @@ Locate Scratch.M. *) Module M. +Reset M. Module M[X:SIG]. +Reset M. Module M[X,Y:SIG]. +Reset M. Module M[X:SIG;Y:SIG]. -Module M[X,Y:SIG;X,Z:SIG]. +Reset M. +Module M[X,Y:SIG;Z1,Z:SIG]. +Reset M. Module M[X:SIG][Y:SIG]. -Module M[X,Y:SIG][X,Z:SIG]. +Reset M. +Module M[X,Y:SIG][Z1,Z:SIG]. +Reset M. Module M:SIG. +Reset M. Module M[X:SIG]:SIG. +Reset M. Module M[X,Y:SIG]:SIG. +Reset M. Module M[X:SIG;Y:SIG]:SIG. -Module M[X,Y:SIG;X,Z:SIG]:SIG. +Reset M. +Module M[X,Y:SIG;Z1,Z:SIG]:SIG. +Reset M. Module M[X:SIG][Y:SIG]:SIG. -Module M[X,Y:SIG][X,Z:SIG]:SIG. -Module M:=(M N). -Module M[X:SIG]:=(M N). -Module M[X,Y:SIG]:=(M N). -Module M[X:SIG;Y:SIG]:=(M N). -Module M[X,Y:SIG;X,Z:SIG]:=(M N). -Module M[X:SIG][Y:SIG]:=(M N). -Module M[X,Y:SIG][X,Z:SIG]:=(M N). -Module M:SIG:=(M N). -Module M[X:SIG]:SIG:=(M N). -Module M[X,Y:SIG]:SIG:=(M N). -Module M[X:SIG;Y:SIG]:SIG:=(M N). -Module M[X,Y:SIG;X,Z:SIG]:SIG:=(M N). -Module M[X:SIG][Y:SIG]:SIG:=(M N). -Module M[X,Y:SIG][X,Z:SIG]:SIG:=(M N). +Reset M. +Module M[X,Y:SIG][Z1,Z:SIG]:SIG. +Reset M. +Module M:=(F Q). +Reset M. +Module M[X:FSIG]:=(X Q). +Reset M. +Module M[X,Y:FSIG]:=(X Q). +Reset M. +Module M[X:FSIG;Y:SIG]:=(X Y). +Reset M. +Module M[X,Y:FSIG;Z1,Z:SIG]:=(X Z). +Reset M. +Module M[X:FSIG][Y:SIG]:=(X Y). +Reset M. +Module M[X,Y:FSIG][Z1,Z:SIG]:=(X Z). +Reset M. +Module M:SIG:=(F Q). +Reset M. +Module M[X:FSIG]:SIG:=(X Q). +Reset M. +Module M[X,Y:FSIG]:SIG:=(X Q). +Reset M. +Module M[X:FSIG;Y:SIG]:SIG:=(X Y). +Reset M. +Module M[X,Y:FSIG;Z1,Z:SIG]:SIG:=(X Z). +Reset M. +Module M[X:FSIG][Y:SIG]:SIG:=(X Y). +Reset M. +Module M[X,Y:FSIG][Z1,Z:SIG]:SIG:=(X Z). +Reset M. -Moduletype SIG. +Module Type ELEM. Parameter A:Set. Parameter x:A. -EndT SIG. +End ELEM. Module Nat. Definition A:=nat. Definition x:=O. End Nat. -Module List[X:SIG]. +Module List[X:ELEM]. Inductive list : Set := nil : list | cons : X.A -> list -> list. diff --git a/test-suite/modules/Przyklad.v b/test-suite/modules/Przyklad.v index ecf9a8c25..4f4c2066d 100644 --- a/test-suite/modules/Przyklad.v +++ b/test-suite/modules/Przyklad.v @@ -27,12 +27,12 @@ Split with b0; Reflexivity. Save. -Modtype ELEM. +Module Type ELEM. Parameter T : Set. Parameter eq_dec : (a,a':T){a=a'}+{~ a=a'}. -EndT ELEM. +End ELEM. -Modtype SET[Elt : ELEM]. +Module Type SET[Elt : ELEM]. Parameter T : Set. Parameter empty : T. Parameter add : Elt.T -> T -> T. @@ -50,9 +50,9 @@ Modtype SET[Elt : ELEM]. (s:T) (e:Elt.T) (e':Elt.T) ~(e=e') -> (find e (add e' s))=(find e s). -EndT SET. +End SET. -Mod FuncDict[E : ELEM]. +Module FuncDict[E : ELEM]. Definition T := E.T -> bool. Definition empty := [e':E.T] false. Definition find := [e':E.T] [s:T] (s e'). @@ -93,20 +93,20 @@ Mod FuncDict[E : ELEM]. Qed. -EndM FuncDict. +End FuncDict. -Mod F : SET := FuncDict. +Module F : SET := FuncDict. -Mod Nat. +Module Nat. Definition T:=nat. Lemma eq_dec : (a,a':T){a=a'}+{~ a=a'}. Decide Equality. Qed. -EndM Nat. +End Nat. -Mod SetNat:=F Nat. +Module SetNat:=F Nat. Lemma no_zero_in_empty:(SetNat.find O SetNat.empty)=false. @@ -114,9 +114,9 @@ Apply SetNat.find_empty_false. Save. (***************************************************************************) -Mod Lemmas[G:SET][E:ELEM]. +Module Lemmas[G:SET][E:ELEM]. - Mod ESet:=G E. + Module ESet:=G E. Lemma commute : (S:ESet.T)(a1,a2:E.T) let S1 = (ESet.add a1 (ESet.add a2 S)) in @@ -132,13 +132,13 @@ Mod Lemmas[G:SET][E:ELEM]. Try (Rewrite ESet.find_add_false; Auto); Auto). Save. -EndM Lemmas. +End Lemmas. Inductive list [A:Set] : Set := nil : (list A) | cons : A -> (list A) -> (list A). -Mod ListDict[E : ELEM]. +Module ListDict[E : ELEM]. Definition T := (list E.T). Definition elt := E.T. @@ -179,10 +179,10 @@ Mod ListDict[E : ELEM]. Save. -EndM ListDict. +End ListDict. -Mod L : SET := ListDict. +Module L : SET := ListDict. diff --git a/test-suite/modules/fun_objects.v b/test-suite/modules/fun_objects.v index b14c3f793..0f8eef847 100644 --- a/test-suite/modules/fun_objects.v +++ b/test-suite/modules/fun_objects.v @@ -1,29 +1,29 @@ Implicit Arguments On. -Modtype SIG. +Module Type SIG. Parameter id:(A:Set)A->A. -EndT SIG. +End SIG. -Mod M[X:SIG]. +Module M[X:SIG]. Definition idid := (X.id X.id). Definition id := (idid X.id). -EndM M. +End M. -Mod N:=M. +Module N:=M. -Mod Nat. +Module Nat. Definition T := nat. Definition x := O. Definition id := [A:Set][x:A]x. -EndM Nat. +End Nat. -Mod Z:=(N Nat). +Module Z:=(N Nat). Check (Z.idid O). -Mod P[Y:SIG] := N. +Module P[Y:SIG] := N. -Mod Y:=P Nat Z. +Module Y:=P Nat Z. Check (Y.id O). diff --git a/test-suite/modules/grammar.v b/test-suite/modules/grammar.v index 7751e9f38..fb734b5d5 100644 --- a/test-suite/modules/grammar.v +++ b/test-suite/modules/grammar.v @@ -1,15 +1,15 @@ -Mod N. +Module N. Definition f:=plus. Syntax constr level 7: plus [ (f $n $m)] -> [ $n:L "+" $m:E]. Check (f O O). -EndM N. +End N. Check (N.f O O). -Imp N. +Import N. Check (N.f O O). Check (f O O). -Mod M:=N. +Module M:=N. Check (f O O). Check (N.f O O). -Imp M. +Import M. Check (f O O). Check (N.f O O). diff --git a/test-suite/modules/modul.v b/test-suite/modules/modul.v index ba333c525..5612ea755 100644 --- a/test-suite/modules/modul.v +++ b/test-suite/modules/modul.v @@ -1,4 +1,4 @@ -Mod M. +Module M. Parameter rel:nat -> nat -> Prop. Axiom w : (n:nat)(rel O (S n)). @@ -14,13 +14,13 @@ Mod M. Auto. Save. -EndM M. +End M. (*Lemma w1 : (M.rel O (S O)). Auto. *) -Imp M. +Import M. Print Hint *. Lemma w1 : (O#(S O)). @@ -35,5 +35,5 @@ Locate rel. Locate M. -Mod N:=Scratch.M. +Module N:=Top.M. diff --git a/test-suite/modules/modulik.v b/test-suite/modules/modulik.v deleted file mode 100644 index 50d985e52..000000000 --- a/test-suite/modules/modulik.v +++ /dev/null @@ -1,5 +0,0 @@ -Definition toto := Set. - -Mod M. - Definition id:=[X:Set]X. -EndM M. diff --git a/test-suite/modules/obj.v b/test-suite/modules/obj.v index b02bdf189..2231e0849 100644 --- a/test-suite/modules/obj.v +++ b/test-suite/modules/obj.v @@ -1,26 +1,26 @@ Implicit Arguments On. -Mod M. +Module M. Definition a:=[s:Set]s. Print a. -EndM M. +End M. Print M.a. -Mod K. +Module K. Definition app:=[A,B:Set; f:(A->B); x:A](f x). - Mod N. + Module N. Definition apap:=[A,B:Set](app (app 1!A 2!B)). Print app. Print apap. - EndM N. + End N. Print N.apap. -EndM K. +End K. Print K.app. Print K.N.apap. -Mod W:=K.N. +Module W:=K.N. Print W.apap. diff --git a/test-suite/modules/objects.v b/test-suite/modules/objects.v index 8183c67c6..c2d1c52dd 100644 --- a/test-suite/modules/objects.v +++ b/test-suite/modules/objects.v @@ -1,32 +1,32 @@ Reset Initial. -Modtype SET. +Module Type SET. Axiom T:Set. Axiom x:T. -EndT SET. +End SET. Implicit Arguments On. -Mod M[X:SET]. +Module M[X:SET]. Definition T := nat. Definition x := O. Definition f := [A:Set][x:A]X.x. -EndM M. +End M. -Mod N:=M. +Module N:=M. -Mod Nat. +Module Nat. Definition T := nat. Definition x := O. -EndM Nat. +End Nat. -Mod Z:=(N Nat). +Module Z:=(N Nat). Check (Z.f O). -Mod P[Y:SET] := N. +Module P[Y:SET] := N. -Mod Y:=P Z Nat. +Module Y:=P Z Nat. Check (Y.f O). diff --git a/test-suite/modules/sub_objects.v b/test-suite/modules/sub_objects.v index f800dec52..73fd6f322 100644 --- a/test-suite/modules/sub_objects.v +++ b/test-suite/modules/sub_objects.v @@ -3,33 +3,33 @@ Reset Initial. Set Implicit Arguments. -Mod M. +Module M. Definition id:=[A:Set][x:A]x. - Modtype SIG. + Module Type SIG. Parameter idid:(A:Set)A->A. - EndT SIG. + End SIG. - Mod N. + Module N. Definition idid:=[A:Set][x:A](id x). Grammar constr constr8 := not_eq [ "#" constr7($b) ] -> [ (idid $b) ]. Syntactic Definition inc := (plus (S O)). - EndM N. + End N. Definition zero:=(N.idid O). -EndM M. +End M. Definition zero := (M.N.idid O). Definition jeden := (M.N.inc O). -Mod Goly:=M.N. +Module Goly:=M.N. Definition Gole_zero := (Goly.idid O). Definition Goly_jeden := (Goly.inc O). -Mod Ubrany : M.SIG := M.N. +Module Ubrany : M.SIG := M.N. Definition Ubrane_zero := (Ubrany.idid O). diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 6e0ba7087..f3e2ac0f1 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -205,6 +205,20 @@ let print_located_qualid (_,qid) = let sp = Nametab.sp_of_syntactic_definition kn in msgnl (pr_sp sp) with Not_found -> + try + let dir = match Nametab.locate_dir qid with + | DirOpenModule (dir,_) + | DirOpenModtype (dir,_) + | DirOpenSection (dir,_) + | DirModule (dir,_) + | DirClosedSection dir -> dir + in + msgnl (pr_dirpath dir) + with Not_found -> + try + let (_,sp) = Nametab.full_name_modtype qid in + msgnl (pr_sp sp) + with Not_found -> msgnl (pr_qualid qid ++ str " is not a defined object") (*let print_path_entry (s,l) = @@ -426,7 +440,7 @@ let vernac_declare_module_type id bl mty_ast_o = | _, None -> Declaremods.start_modtype id argids args; if_verbose message - ("Interactive Module "^ string_of_id id ^" started") + ("Interactive Module Type "^ string_of_id id ^" started") | _, Some base_mty -> let mty = |