summaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
commit97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch)
tree97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /interp
parent300293c119981054c95182a90c829058530a6b6f (diff)
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml383
-rw-r--r--interp/constrextern.mli33
-rw-r--r--interp/constrintern.ml563
-rw-r--r--interp/constrintern.mli107
-rw-r--r--interp/coqlib.ml39
-rw-r--r--interp/coqlib.mli74
-rw-r--r--interp/doc.tex2
-rw-r--r--interp/dumpglob.ml50
-rw-r--r--interp/dumpglob.mli9
-rw-r--r--interp/genarg.ml12
-rw-r--r--interp/genarg.mli105
-rw-r--r--interp/implicit_quantifiers.ml60
-rw-r--r--interp/implicit_quantifiers.mli18
-rw-r--r--interp/interp.mllib2
-rw-r--r--interp/modintern.ml100
-rw-r--r--interp/modintern.mli21
-rw-r--r--interp/notation.ml192
-rw-r--r--interp/notation.mli95
-rw-r--r--interp/ppextend.ml4
-rw-r--r--interp/ppextend.mli10
-rw-r--r--interp/reserve.ml95
-rw-r--r--interp/reserve.mli13
-rw-r--r--interp/smartlocate.ml4
-rw-r--r--interp/smartlocate.mli16
-rw-r--r--interp/syntax_def.ml6
-rw-r--r--interp/syntax_def.mli10
-rw-r--r--interp/topconstr.ml393
-rw-r--r--interp/topconstr.mli108
28 files changed, 1298 insertions, 1226 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index dc339622..193b38dd 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: constrextern.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
(*i*)
open Pp
open Util
@@ -23,7 +21,7 @@ open Environ
open Libnames
open Impargs
open Topconstr
-open Rawterm
+open Glob_term
open Pattern
open Nametab
open Notation
@@ -31,7 +29,7 @@ open Reserve
open Detyping
(*i*)
-(* Translation from rawconstr to front constr *)
+(* Translation from glob_constr to front constr *)
(**********************************************************************)
(* Parametrization *)
@@ -76,6 +74,49 @@ let without_symbols f = Flags.with_option print_no_symbol f
let with_meta_as_hole f = Flags.with_option print_meta_as_hole f
(**********************************************************************)
+(* Control printing of records *)
+
+let is_record indsp =
+ try
+ let _ = Recordops.lookup_structure indsp in
+ true
+ with Not_found -> false
+
+let encode_record r =
+ let indsp = global_inductive r in
+ if not (is_record indsp) then
+ user_err_loc (loc_of_reference r,"encode_record",
+ str "This type is not a structure type.");
+ indsp
+
+module PrintingRecordRecord =
+ PrintingInductiveMake (struct
+ let encode = encode_record
+ let field = "Record"
+ let title = "Types leading to pretty-printing using record notation: "
+ let member_message s b =
+ str "Terms of " ++ s ++
+ str
+ (if b then " are printed using record notation"
+ else " are not printed using record notation")
+ end)
+
+module PrintingRecordConstructor =
+ PrintingInductiveMake (struct
+ let encode = encode_record
+ let field = "Constructor"
+ let title = "Types leading to pretty-printing using constructor form: "
+ let member_message s b =
+ str "Terms of " ++ s ++
+ str
+ (if b then " are printed using constructor form"
+ else " are not printed using constructor form")
+ end)
+
+module PrintingRecord = Goptions.MakeRefTable(PrintingRecordRecord)
+module PrintingConstructor = Goptions.MakeRefTable(PrintingRecordConstructor)
+
+(**********************************************************************)
(* Various externalisation functions *)
let insert_delimiters e = function
@@ -117,6 +158,8 @@ let rec check_same_pattern p1 p2 =
check_same_pattern a1 a2
| CPatCstr(_,c1,a1), CPatCstr(_,c2,a2) when c1=c2 ->
List.iter2 check_same_pattern a1 a2
+ | CPatCstrExpl(_,c1,a1), CPatCstrExpl(_,c2,a2) when c1=c2 ->
+ List.iter2 check_same_pattern a1 a2
| CPatAtom(_,r1), CPatAtom(_,r2) when r1=r2 -> ()
| CPatPrim(_,i1), CPatPrim(_,i2) when i1=i2 -> ()
| CPatDelimiters(_,s1,e1), CPatDelimiters(_,s2,e2) when s1=s2 ->
@@ -204,82 +247,13 @@ and check_same_fix_binder bl1 bl2 =
let same c d = try check_same_type c d; true with _ -> false
-(* Idem for rawconstr *)
-
-let array_iter2 f v1 v2 =
- List.iter2 f (Array.to_list v1) (Array.to_list v2)
-
-let rec same_patt p1 p2 =
- match p1, p2 with
- PatVar(_,na1), PatVar(_,na2) -> if na1<>na2 then failwith "PatVar"
- | PatCstr(_,c1,pl1,al1), PatCstr(_,c2,pl2,al2) ->
- if c1<>c2 || al1 <> al2 then failwith "PatCstr";
- List.iter2 same_patt pl1 pl2
- | _ -> failwith "same_patt"
-
-let rec same_raw c d =
- match c,d with
- | RRef(_,gr1), RRef(_,gr2) -> if gr1<>gr2 then failwith "RRef"
- | RVar(_,id1), RVar(_,id2) -> if id1<>id2 then failwith "RVar"
- | REvar(_,e1,a1), REvar(_,e2,a2) ->
- if e1 <> e2 then failwith "REvar";
- Option.iter2(List.iter2 same_raw) a1 a2
- | RPatVar(_,pv1), RPatVar(_,pv2) -> if pv1<>pv2 then failwith "RPatVar"
- | RApp(_,f1,a1), RApp(_,f2,a2) ->
- List.iter2 same_raw (f1::a1) (f2::a2)
- | RLambda(_,na1,bk1,t1,m1), RLambda(_,na2,bk2,t2,m2) ->
- if na1 <> na2 then failwith "RLambda";
- same_raw t1 t2; same_raw m1 m2
- | RProd(_,na1,bk1,t1,m1), RProd(_,na2,bk2,t2,m2) ->
- if na1 <> na2 then failwith "RProd";
- same_raw t1 t2; same_raw m1 m2
- | RLetIn(_,na1,t1,m1), RLetIn(_,na2,t2,m2) ->
- if na1 <> na2 then failwith "RLetIn";
- same_raw t1 t2; same_raw m1 m2
- | RCases(_,_,_,c1,b1), RCases(_,_,_,c2,b2) ->
- List.iter2
- (fun (t1,(al1,oind1)) (t2,(al2,oind2)) ->
- same_raw t1 t2;
- if al1 <> al2 then failwith "RCases";
- Option.iter2(fun (_,i1,_,nl1) (_,i2,_,nl2) ->
- if i1<>i2 || nl1 <> nl2 then failwith "RCases") oind1 oind2) c1 c2;
- List.iter2 (fun (_,_,pl1,b1) (_,_,pl2,b2) ->
- List.iter2 same_patt pl1 pl2;
- same_raw b1 b2) b1 b2
- | RLetTuple(_,nl1,_,b1,c1), RLetTuple(_,nl2,_,b2,c2) ->
- if nl1<>nl2 then failwith "RLetTuple";
- same_raw b1 b2;
- same_raw c1 c2
- | RIf(_,b1,_,t1,e1),RIf(_,b2,_,t2,e2) ->
- same_raw b1 b2; same_raw t1 t2; same_raw e1 e2
- | RRec(_,fk1,na1,bl1,ty1,def1), RRec(_,fk2,na2,bl2,ty2,def2) ->
- if fk1 <> fk2 || na1 <> na2 then failwith "RRec";
- array_iter2
- (List.iter2 (fun (na1,bk1,bd1,ty1) (na2,bk2,bd2,ty2) ->
- if na1<>na2 then failwith "RRec";
- Option.iter2 same_raw bd1 bd2;
- same_raw ty1 ty2)) bl1 bl2;
- array_iter2 same_raw ty1 ty2;
- array_iter2 same_raw def1 def2
- | RSort(_,s1), RSort(_,s2) -> if s1<>s2 then failwith "RSort"
- | RHole _, _ -> ()
- | _, RHole _ -> ()
- | RCast(_,c1,_),r2 -> same_raw c1 r2
- | r1, RCast(_,c2,_) -> same_raw r1 c2
- | RDynamic(_,d1), RDynamic(_,d2) -> if d1<>d2 then failwith"RDynamic"
- | _ -> failwith "same_raw"
-
-let same_rawconstr c d =
- try same_raw c d; true
- with Failure _ | Invalid_argument _ -> false
-
(**********************************************************************)
(* mapping patterns to cases_pattern_expr *)
let has_curly_brackets ntn =
String.length ntn >= 6 & (String.sub ntn 0 6 = "{ _ } " or
String.sub ntn (String.length ntn - 6) 6 = " { _ }" or
- string_string_contains ntn " { _ } ")
+ string_string_contains ~where:ntn ~what:" { _ } ")
let rec wildcards ntn n =
if n = String.length ntn then []
@@ -347,7 +321,7 @@ let mkPat loc qid l =
(* Normally irrelevant test with v8 syntax, but let's do it anyway *)
if l = [] then CPatAtom (loc,Some qid) else CPatCstr (loc,qid,l)
- (* Better to use extern_rawconstr composed with injection/retraction ?? *)
+ (* Better to use extern_glob_constr composed with injection/retraction ?? *)
let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
try
if !Flags.raw_print or !print_no_symbol then raise No_match;
@@ -370,7 +344,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
let p =
try
- if !Flags.raw_print then raise Exit;
+ if !Flags.raw_print then raise Exit;
let projs = Recordops.lookup_projections (fst cstrsp) in
let rec ip projs args acc =
match projs with
@@ -464,8 +438,11 @@ let is_projection nargs = function
let is_hole = function CHole _ -> true | _ -> false
-let is_significant_implicit a impl tail =
- not (is_hole a) or (tail = [] & not (List.for_all is_status_implicit impl))
+let is_significant_implicit a =
+ not (is_hole a)
+
+let is_needed_for_correct_partial_application tail imp =
+ tail = [] & not (maximal_insertion_of imp)
(* Implicit args indexes are in ascending order *)
(* inctx is useful only if there is a last argument to be deduced from ctxt *)
@@ -477,8 +454,9 @@ let explicitize loc inctx impl (cf,f) args =
let visible =
!Flags.raw_print or
(!print_implicits & !print_implicits_explicit_args) or
+ (is_needed_for_correct_partial_application tail imp) or
(!print_implicits_defensive &
- is_significant_implicit a impl tail &
+ is_significant_implicit a &
not (is_inferable_implicit inctx n imp))
in
if visible then
@@ -532,7 +510,7 @@ let rec extern_args extern scopes env args subscopes =
extern argscopes env a :: extern_args extern scopes env args subscopes
let rec remove_coercions inctx = function
- | RApp (loc,RRef (_,r),args) as c
+ | GApp (loc,GRef (_,r),args) as c
when not (!Flags.raw_print or !print_coercions)
->
let nargs = List.length args in
@@ -551,22 +529,17 @@ let rec remove_coercions inctx = function
been confused with ordinary application or would have need
a surrounding context and the coercion to funclass would
have been made explicit to match *)
- if l = [] then a' else RApp (loc,a',l)
+ if l = [] then a' else GApp (loc,a',l)
| _ -> c
with Not_found -> c)
| c -> c
let rec flatten_application = function
- | RApp (loc,RApp(_,a,l'),l) -> flatten_application (RApp (loc,a,l'@l))
+ | GApp (loc,GApp(_,a,l'),l) -> flatten_application (GApp (loc,a,l'@l))
| a -> a
-let rec rename_rawconstr_var id0 id1 = function
- RRef(loc,VarRef id) when id=id0 -> RRef(loc,VarRef id1)
- | RVar(loc,id) when id=id0 -> RVar(loc,id1)
- | c -> map_rawconstr (rename_rawconstr_var id0 id1) c
-
(**********************************************************************)
-(* mapping rawterms to numerals (in presence of coercions, choose the *)
+(* mapping glob_constr to numerals (in presence of coercions, choose the *)
(* one with no delimiter if possible) *)
let extern_possible_prim_token scopes r =
@@ -574,7 +547,7 @@ let extern_possible_prim_token scopes r =
let (sc,n) = uninterp_prim_token r in
match availability_of_prim_token n sc scopes with
| None -> None
- | Some key -> Some (insert_delimiters (CPrim (loc_of_rawconstr r,n)) key)
+ | Some key -> Some (insert_delimiters (CPrim (loc_of_glob_constr r,n)) key)
with No_match ->
None
@@ -586,12 +559,12 @@ let extern_optimal_prim_token scopes r r' =
| _ -> raise No_match
(**********************************************************************)
-(* mapping rawterms to constr_expr *)
+(* mapping glob_constr to constr_expr *)
-let extern_rawsort = function
- | RProp _ as s -> s
- | RType (Some _) as s when !print_universes -> s
- | RType _ -> RType None
+let extern_glob_sort = function
+ | GProp _ as s -> s
+ | GType (Some _) as s when !print_universes -> s
+ | GType _ -> GType None
let rec extern inctx scopes vars r =
let r' = remove_coercions inctx r in
@@ -604,31 +577,37 @@ let rec extern inctx scopes vars r =
if !Flags.raw_print or !print_no_symbol then raise No_match;
extern_symbol scopes vars r'' (uninterp_notations r'')
with No_match -> match r' with
- | RRef (loc,ref) ->
+ | GRef (loc,ref) ->
extern_global loc (select_stronger_impargs (implicits_of_global ref))
(extern_reference loc vars ref)
- | RVar (loc,id) -> CRef (Ident (loc,id))
+ | GVar (loc,id) -> CRef (Ident (loc,id))
- | REvar (loc,n,None) when !print_meta_as_hole -> CHole (loc, None)
+ | GEvar (loc,n,None) when !print_meta_as_hole -> CHole (loc, None)
- | REvar (loc,n,l) ->
+ | GEvar (loc,n,l) ->
extern_evar loc n (Option.map (List.map (extern false scopes vars)) l)
- | RPatVar (loc,n) ->
+ | GPatVar (loc,n) ->
if !print_meta_as_hole then CHole (loc, None) else CPatVar (loc,n)
- | RApp (loc,f,args) ->
+ | GApp (loc,f,args) ->
(match f with
- | RRef (rloc,ref) ->
+ | GRef (rloc,ref) ->
let subscopes = find_arguments_scope ref in
let args =
extern_args (extern true) (snd scopes) vars args subscopes in
begin
try
- if !Flags.raw_print then raise Exit;
+ if !Flags.raw_print then raise Exit;
let cstrsp = match ref with ConstructRef c -> c | _ -> raise Not_found in
let struc = Recordops.lookup_structure (fst cstrsp) in
+ if PrintingRecord.active (fst cstrsp) then
+ ()
+ else if PrintingConstructor.active (fst cstrsp) then
+ raise Exit
+ else if not !Flags.record_print then
+ raise Exit;
let projs = struc.Recordops.s_PROJ in
let locals = struc.Recordops.s_PROJKIND in
let rec cut args n =
@@ -666,66 +645,66 @@ let rec extern inctx scopes vars r =
explicitize loc inctx [] (None,sub_extern false scopes vars f)
(List.map (sub_extern true scopes vars) args))
- | RProd (loc,Anonymous,_,t,c) ->
+ | GProd (loc,Anonymous,_,t,c) ->
(* Anonymous product are never factorized *)
CArrow (loc,extern_typ scopes vars t, extern_typ scopes vars c)
- | RLetIn (loc,na,t,c) ->
+ | GLetIn (loc,na,t,c) ->
CLetIn (loc,(loc,na),sub_extern false scopes vars t,
extern inctx scopes (add_vname vars na) c)
- | RProd (loc,na,bk,t,c) ->
+ | GProd (loc,na,bk,t,c) ->
let t = extern_typ scopes vars (anonymize_if_reserved na t) in
let (idl,c) = factorize_prod scopes (add_vname vars na) t c in
CProdN (loc,[(dummy_loc,na)::idl,Default bk,t],c)
- | RLambda (loc,na,bk,t,c) ->
+ | GLambda (loc,na,bk,t,c) ->
let t = extern_typ scopes vars (anonymize_if_reserved na t) in
let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) t c in
CLambdaN (loc,[(dummy_loc,na)::idl,Default bk,t],c)
- | RCases (loc,sty,rtntypopt,tml,eqns) ->
+ | GCases (loc,sty,rtntypopt,tml,eqns) ->
let vars' =
List.fold_right (name_fold Idset.add)
(cases_predicate_names tml) vars in
let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in
let tml = List.map (fun (tm,(na,x)) ->
let na' = match na,tm with
- Anonymous, RVar (_,id) when
- rtntypopt<>None & occur_rawconstr id (Option.get rtntypopt)
+ Anonymous, GVar (_,id) when
+ rtntypopt<>None & occur_glob_constr id (Option.get rtntypopt)
-> Some (dummy_loc,Anonymous)
| Anonymous, _ -> None
- | Name id, RVar (_,id') when id=id' -> None
+ | Name id, GVar (_,id') when id=id' -> None
| Name _, _ -> Some (dummy_loc,na) in
(sub_extern false scopes vars tm,
(na',Option.map (fun (loc,ind,n,nal) ->
let params = list_tabulate
- (fun _ -> RHole (dummy_loc,Evd.InternalHole)) n in
+ (fun _ -> GHole (dummy_loc,Evd.InternalHole)) n in
let args = List.map (function
- | Anonymous -> RHole (dummy_loc,Evd.InternalHole)
- | Name id -> RVar (dummy_loc,id)) nal in
- let t = RApp (dummy_loc,RRef (dummy_loc,IndRef ind),params@args) in
+ | Anonymous -> GHole (dummy_loc,Evd.InternalHole)
+ | Name id -> GVar (dummy_loc,id)) nal in
+ let t = GApp (dummy_loc,GRef (dummy_loc,IndRef ind),params@args) in
(extern_typ scopes vars t)) x))) tml in
let eqns = List.map (extern_eqn inctx scopes vars) eqns in
CCases (loc,sty,rtntypopt',tml,eqns)
- | RLetTuple (loc,nal,(na,typopt),tm,b) ->
+ | GLetTuple (loc,nal,(na,typopt),tm,b) ->
CLetTuple (loc,List.map (fun na -> (dummy_loc,na)) nal,
(Option.map (fun _ -> (dummy_loc,na)) typopt,
Option.map (extern_typ scopes (add_vname vars na)) typopt),
sub_extern false scopes vars tm,
extern inctx scopes (List.fold_left add_vname vars nal) b)
- | RIf (loc,c,(na,typopt),b1,b2) ->
+ | GIf (loc,c,(na,typopt),b1,b2) ->
CIf (loc,sub_extern false scopes vars c,
(Option.map (fun _ -> (dummy_loc,na)) typopt,
Option.map (extern_typ scopes (add_vname vars na)) typopt),
sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2)
- | RRec (loc,fk,idv,blv,tyv,bv) ->
+ | GRec (loc,fk,idv,blv,tyv,bv) ->
let vars' = Array.fold_right Idset.add idv vars in
(match fk with
- | RFix (nv,n) ->
+ | GFix (nv,n) ->
let listdecl =
Array.mapi (fun i fi ->
let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in
@@ -742,7 +721,7 @@ let rec extern inctx scopes vars r =
extern false scopes vars1 def)) idv
in
CFix (loc,(loc,idv.(n)),Array.to_list listdecl)
- | RCoFix n ->
+ | GCoFix n ->
let listdecl =
Array.mapi (fun i fi ->
let (_,ids,bl) = extern_local_binder scopes vars blv.(i) in
@@ -753,17 +732,15 @@ let rec extern inctx scopes vars r =
in
CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl))
- | RSort (loc,s) -> CSort (loc,extern_rawsort s)
+ | GSort (loc,s) -> CSort (loc,extern_glob_sort s)
- | RHole (loc,e) -> CHole (loc, Some e)
+ | GHole (loc,e) -> CHole (loc, Some e)
- | RCast (loc,c, CastConv (k,t)) ->
+ | GCast (loc,c, CastConv (k,t)) ->
CCast (loc,sub_extern true scopes vars c, CastConv (k,extern_typ scopes vars t))
- | RCast (loc,c, CastCoerce) ->
+ | GCast (loc,c, CastCoerce) ->
CCast (loc,sub_extern true scopes vars c, CastCoerce)
- | RDynamic (loc,d) -> CDynamic (loc,d)
-
and extern_typ (_,scopes) =
extern true (Some Notation.type_scope,scopes)
@@ -774,7 +751,7 @@ and factorize_prod scopes vars aty c =
if !Flags.raw_print or !print_no_symbol then raise No_match;
([],extern_symbol scopes vars c (uninterp_notations c))
with No_match -> match c with
- | RProd (loc,(Name id as na),bk,ty,c)
+ | GProd (loc,(Name id as na),bk,ty,c)
when same aty (extern_typ scopes vars (anonymize_if_reserved na ty))
& not (occur_var_constr_expr id aty) (* avoid na in ty escapes scope *)
-> let (nal,c) = factorize_prod scopes (Idset.add id vars) aty c in
@@ -786,7 +763,7 @@ and factorize_lambda inctx scopes vars aty c =
if !Flags.raw_print or !print_no_symbol then raise No_match;
([],extern_symbol scopes vars c (uninterp_notations c))
with No_match -> match c with
- | RLambda (loc,na,bk,ty,c)
+ | GLambda (loc,na,bk,ty,c)
when same aty (extern_typ scopes vars (anonymize_if_reserved na ty))
& not (occur_name na aty) (* To avoid na in ty' escapes scope *)
-> let (nal,c) =
@@ -822,33 +799,40 @@ and extern_eqn inctx scopes vars (loc,ids,pl,c) =
and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
| [] -> raise No_match
| (keyrule,pat,n as _rule)::rules ->
- let loc = Rawterm.loc_of_rawconstr t in
+ let loc = Glob_term.loc_of_glob_constr t in
try
(* Adjusts to the number of arguments expected by the notation *)
let (t,args,argsscopes,argsimpls) = match t,n with
- | RApp (_,(RRef (_,ref) as f),args), Some n
+ | GApp (_,f,args), Some n
when List.length args >= n ->
let args1, args2 = list_chop n args in
- let subscopes =
- try list_skipn n (find_arguments_scope ref) with _ -> [] in
- let impls =
- let impls =
- select_impargs_size
- (List.length args) (implicits_of_global ref) in
- try list_skipn n impls with _ -> [] in
- (if n = 0 then f else RApp (dummy_loc,f,args1)),
+ let subscopes, impls =
+ match f with
+ | GRef (_,ref) ->
+ let subscopes =
+ try list_skipn n (find_arguments_scope ref) with _ -> [] in
+ let impls =
+ let impls =
+ select_impargs_size
+ (List.length args) (implicits_of_global ref) in
+ try list_skipn n impls with _ -> [] in
+ subscopes,impls
+ | _ ->
+ [], [] in
+ (if n = 0 then f else GApp (dummy_loc,f,args1)),
args2, subscopes, impls
- | RApp (_,(RRef (_,ref) as f),args), None ->
+ | GApp (_,(GRef (_,ref) as f),args), None ->
let subscopes = find_arguments_scope ref in
let impls =
select_impargs_size
(List.length args) (implicits_of_global ref) in
f, args, subscopes, impls
- | RRef _, Some 0 -> RApp (dummy_loc,t,[]), [], [], []
+ | GRef _, Some 0 -> GApp (dummy_loc,t,[]), [], [], []
| _, None -> t, [], [], []
| _ -> raise No_match in
(* Try matching ... *)
- let terms,termlists,binders = match_aconstr t pat in
+ let terms,termlists,binders =
+ match_aconstr !print_universes t pat in
(* Try availability of interpretation ... *)
let e =
match keyrule with
@@ -888,16 +872,16 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
No_match -> extern_symbol allscopes vars t rules
and extern_recursion_order scopes vars = function
- RStructRec -> CStructRec
- | RWfRec c -> CWfRec (extern true scopes vars c)
- | RMeasureRec (m,r) -> CMeasureRec (extern true scopes vars m,
+ GStructRec -> CStructRec
+ | GWfRec c -> CWfRec (extern true scopes vars c)
+ | GMeasureRec (m,r) -> CMeasureRec (extern true scopes vars m,
Option.map (extern true scopes vars) r)
-let extern_rawconstr vars c =
+let extern_glob_constr vars c =
extern false (None,[]) vars c
-let extern_rawtype vars c =
+let extern_glob_type vars c =
extern_typ (None,[]) vars c
(******************************************************************)
@@ -920,89 +904,70 @@ let extern_constr at_top env t =
let extern_type at_top env t =
let avoid = if at_top then ids_of_context env else [] in
let r = Detyping.detype at_top avoid (names_of_rel_context env) t in
- extern_rawtype (vars_of_env env) r
+ extern_glob_type (vars_of_env env) r
-let extern_sort s = extern_rawsort (detype_sort s)
+let extern_sort s = extern_glob_sort (detype_sort s)
(******************************************************************)
(* Main translation function from pattern -> constr_expr *)
-let rec raw_of_pat env = function
- | PRef ref -> RRef (loc,ref)
- | PVar id -> RVar (loc,id)
- | PEvar (n,l) -> REvar (loc,n,Some (array_map_to_list (raw_of_pat env) l))
+let any_any_branch =
+ (* | _ => _ *)
+ (loc,[],[PatVar (loc,Anonymous)],GHole (loc,Evd.InternalHole))
+
+let rec glob_of_pat env = function
+ | PRef ref -> GRef (loc,ref)
+ | PVar id -> GVar (loc,id)
+ | PEvar (n,l) -> GEvar (loc,n,Some (array_map_to_list (glob_of_pat env) l))
| PRel n ->
let id = try match lookup_name_of_rel n env with
| Name id -> id
| Anonymous ->
- anomaly "rawconstr_of_pattern: index to an anonymous variable"
+ anomaly "glob_constr_of_pattern: index to an anonymous variable"
with Not_found -> id_of_string ("_UNBOUND_REL_"^(string_of_int n)) in
- RVar (loc,id)
- | PMeta None -> RHole (loc,Evd.InternalHole)
- | PMeta (Some n) -> RPatVar (loc,(false,n))
+ GVar (loc,id)
+ | PMeta None -> GHole (loc,Evd.InternalHole)
+ | PMeta (Some n) -> GPatVar (loc,(false,n))
| PApp (f,args) ->
- RApp (loc,raw_of_pat env f,array_map_to_list (raw_of_pat env) args)
+ GApp (loc,glob_of_pat env f,array_map_to_list (glob_of_pat env) args)
| PSoApp (n,args) ->
- RApp (loc,RPatVar (loc,(true,n)),
- List.map (raw_of_pat env) args)
+ GApp (loc,GPatVar (loc,(true,n)),
+ List.map (glob_of_pat env) args)
| PProd (na,t,c) ->
- RProd (loc,na,Explicit,raw_of_pat env t,raw_of_pat (na::env) c)
+ GProd (loc,na,Explicit,glob_of_pat env t,glob_of_pat (na::env) c)
| PLetIn (na,t,c) ->
- RLetIn (loc,na,raw_of_pat env t, raw_of_pat (na::env) c)
+ GLetIn (loc,na,glob_of_pat env t, glob_of_pat (na::env) c)
| PLambda (na,t,c) ->
- RLambda (loc,na,Explicit,raw_of_pat env t, raw_of_pat (na::env) c)
+ GLambda (loc,na,Explicit,glob_of_pat env t, glob_of_pat (na::env) c)
| PIf (c,b1,b2) ->
- RIf (loc, raw_of_pat env c, (Anonymous,None),
- raw_of_pat env b1, raw_of_pat env b2)
- | PCase ((LetStyle,[|n|],ind,None),PMeta None,tm,[|b|]) ->
- let nal,b = it_destRLambda_or_LetIn_names n (raw_of_pat env b) in
- RLetTuple (loc,nal,(Anonymous,None),raw_of_pat env tm,b)
- | PCase (_,PMeta None,tm,[||]) ->
- RCases (loc,RegularStyle,None,[raw_of_pat env tm,(Anonymous,None)],[])
- | PCase ((_,cstr_nargs,indo,ind_nargs),p,tm,bv) ->
- let brs = Array.to_list (Array.map (raw_of_pat env) bv) in
- let brns = Array.to_list cstr_nargs in
- (* ind is None only if no branch and no return type *)
- let ind = Option.get indo in
- let mat = simple_cases_matrix_of_branches ind brns brs in
- let indnames,rtn =
- if p = PMeta None then (Anonymous,None),None
- else
- let nparams,n = Option.get ind_nargs in
- return_type_of_predicate ind nparams n (raw_of_pat env p) in
- RCases (loc,RegularStyle,rtn,[raw_of_pat env tm,indnames],mat)
+ GIf (loc, glob_of_pat env c, (Anonymous,None),
+ glob_of_pat env b1, glob_of_pat env b2)
+ | PCase ({cip_style=LetStyle; cip_ind_args=None},PMeta None,tm,[(0,n,b)]) ->
+ let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat env b) in
+ GLetTuple (loc,nal,(Anonymous,None),glob_of_pat env tm,b)
+ | PCase (info,p,tm,bl) ->
+ let mat = match bl, info.cip_ind with
+ | [], _ -> []
+ | _, Some ind ->
+ let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat env c)) bl in
+ simple_cases_matrix_of_branches ind bl'
+ | _, None -> anomaly "PCase with some branches but unknown inductive"
+ in
+ let mat = if info.cip_extensible then mat @ [any_any_branch] else mat
+ in
+ let indnames,rtn = match p, info.cip_ind, info.cip_ind_args with
+ | PMeta None, _, _ -> (Anonymous,None),None
+ | _, Some ind, Some (nparams,nargs) ->
+ return_type_of_predicate ind nparams nargs (glob_of_pat env p)
+ | _ -> anomaly "PCase with non-trivial predicate but unknown inductive"
+ in
+ GCases (loc,RegularStyle,rtn,[glob_of_pat env tm,indnames],mat)
| PFix f -> Detyping.detype false [] env (mkFix f)
| PCoFix c -> Detyping.detype false [] env (mkCoFix c)
- | PSort s -> RSort (loc,s)
-
-and raw_of_eqn env constr construct_nargs branch =
- let make_pat x env b ids =
- let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in
- let id = next_name_away_with_default "x" x avoid in
- PatVar (dummy_loc,Name id),(Name id)::env,id::ids
- in
- let rec buildrec ids patlist env n b =
- if n=0 then
- (dummy_loc, ids,
- [PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)],
- raw_of_pat env b)
- else
- match b with
- | PLambda (x,_,b) ->
- let pat,new_env,new_ids = make_pat x env b ids in
- buildrec new_ids (pat::patlist) new_env (n-1) b
-
- | PLetIn (x,_,b) ->
- let pat,new_env,new_ids = make_pat x env b ids in
- buildrec new_ids (pat::patlist) new_env (n-1) b
-
- | _ ->
- error "Unsupported branch in case-analysis while printing pattern."
- in
- buildrec [] [] env construct_nargs branch
+ | PSort s -> GSort (loc,s)
let extern_constr_pattern env pat =
- extern true (None,[]) Idset.empty (raw_of_pat env pat)
+ extern true (None,[]) Idset.empty (glob_of_pat env pat)
let extern_rel_context where env sign =
let a = detype_rel_context where [] (names_of_rel_context env) sign in
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index d0ccde2a..e1fdd068 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -1,14 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: constrextern.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
open Util
open Names
open Term
@@ -17,35 +14,33 @@ open Sign
open Environ
open Libnames
open Nametab
-open Rawterm
+open Glob_term
open Pattern
open Topconstr
open Notation
-(*i*)
-(* v7->v8 translation *)
val check_same_type : constr_expr -> constr_expr -> unit
-(* Translation of pattern, cases pattern, rawterm and term into syntax
+(** Translation of pattern, cases pattern, glob_constr and term into syntax
trees for printing *)
val extern_cases_pattern : Idset.t -> cases_pattern -> cases_pattern_expr
-val extern_rawconstr : Idset.t -> rawconstr -> constr_expr
-val extern_rawtype : Idset.t -> rawconstr -> constr_expr
+val extern_glob_constr : Idset.t -> glob_constr -> constr_expr
+val extern_glob_type : Idset.t -> glob_constr -> constr_expr
val extern_constr_pattern : names_context -> constr_pattern -> constr_expr
-(* If [b=true] in [extern_constr b env c] then the variables in the first
+(** If [b=true] in [extern_constr b env c] then the variables in the first
level of quantification clashing with the variables in [env] are renamed *)
val extern_constr : bool -> env -> constr -> constr_expr
val extern_constr_in_scope : bool -> scope_name -> env -> constr -> constr_expr
val extern_reference : loc -> Idset.t -> global_reference -> reference
val extern_type : bool -> env -> types -> constr_expr
-val extern_sort : sorts -> rawsort
+val extern_sort : sorts -> glob_sort
val extern_rel_context : constr option -> env ->
rel_context -> local_binder list
-(* Printing options *)
+(** Printing options *)
val print_implicits : bool ref
val print_implicits_defensive : bool ref
val print_arguments : bool ref
@@ -55,25 +50,25 @@ val print_universes : bool ref
val print_no_symbol : bool ref
val print_projections : bool ref
-(* Debug printing options *)
+(** Debug printing options *)
val set_debug_global_reference_printer :
(loc -> global_reference -> reference) -> unit
-(* This governs printing of implicit arguments. If [with_implicits] is
+(** This governs printing of implicit arguments. If [with_implicits] is
on and not [with_arguments] then implicit args are printed prefixed
by "!"; if [with_implicits] and [with_arguments] are both on the
function and not the arguments is prefixed by "!" *)
val with_implicits : ('a -> 'b) -> 'a -> 'b
val with_arguments : ('a -> 'b) -> 'a -> 'b
-(* This forces printing of coercions *)
+(** This forces printing of coercions *)
val with_coercions : ('a -> 'b) -> 'a -> 'b
-(* This forces printing universe names of Type{.} *)
+(** This forces printing universe names of Type\{.\} *)
val with_universes : ('a -> 'b) -> 'a -> 'b
-(* This suppresses printing of numeral and symbols *)
+(** This suppresses printing of numeral and symbols *)
val without_symbols : ('a -> 'b) -> 'a -> 'b
-(* This prints metas as anonymous holes *)
+(** This prints metas as anonymous holes *)
val with_meta_as_hole : ('a -> 'b) -> 'a -> 'b
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4310a01e..b161d001 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: constrintern.ml 14656 2011-11-16 08:46:31Z herbelin $ *)
-
open Pp
open Util
open Flags
@@ -16,7 +14,7 @@ open Nameops
open Namegen
open Libnames
open Impargs
-open Rawterm
+open Glob_term
open Pattern
open Pretyping
open Cases
@@ -32,6 +30,7 @@ type var_internalization_type =
| Inductive of identifier list (* list of params *)
| Recursive
| Method
+ | Variable
type var_internalization_data =
(* type of the "free" variable, for coqdoc, e.g. while typing the
@@ -46,9 +45,9 @@ type var_internalization_data =
scope_name option list
type internalization_env =
- (identifier * var_internalization_data) list
+ (var_internalization_data) Idmap.t
-type raw_binder = (name * binding_kind * rawconstr option * rawconstr)
+type glob_binder = (name * binding_kind * glob_constr option * glob_constr)
let interning_grammar = ref false
@@ -167,7 +166,7 @@ let error_inductive_parameter_not_implicit loc =
(* Pre-computing the implicit arguments and arguments scopes needed *)
(* for interpretation *)
-let empty_internalization_env = []
+let empty_internalization_env = Idmap.empty
let compute_explicitable_implicit imps = function
| Inductive params ->
@@ -175,7 +174,7 @@ let compute_explicitable_implicit imps = function
let sub_impl,_ = list_chop (List.length params) imps in
let sub_impl' = List.filter is_status_implicit sub_impl in
List.map name_of_implicit sub_impl'
- | Recursive | Method ->
+ | Recursive | Method | Variable ->
(* Unable to know in advance what the implicit arguments will be *)
[]
@@ -185,8 +184,9 @@ let compute_internalization_data env ty typ impl =
(ty, expls_impl, impl, compute_arguments_scope typ)
let compute_internalization_env env ty =
- list_map3
- (fun id typ impl -> (id,compute_internalization_data env ty typ impl))
+ list_fold_left3
+ (fun map id typ impl -> Idmap.add id (compute_internalization_data env ty typ impl) map)
+ empty_internalization_env
(**********************************************************************)
(* Contracting "{ _ }" in notations *)
@@ -234,6 +234,13 @@ let contract_pat_notation ntn (l,ll) =
(* side effect; don't inline *)
!ntn',(l,ll)
+type intern_env = {
+ ids: Names.Idset.t;
+ unb: bool;
+ tmp_scope: Topconstr.tmp_scope_name option;
+ scopes: Topconstr.scope_name list;
+ impls: internalization_env }
+
(**********************************************************************)
(* Remembering the parsing scope of variables in notations *)
@@ -262,7 +269,7 @@ let error_expect_binder_notation_type loc id =
pr_id id ++
str " is expected to occur in binding position in the right-hand side.")
-let set_var_scope loc id istermvar (_,_,scopt,scopes) ntnvars =
+let set_var_scope loc id istermvar env ntnvars =
try
let idscopes,typ = List.assoc id ntnvars in
if !idscopes <> None &
@@ -270,12 +277,12 @@ let set_var_scope loc id istermvar (_,_,scopt,scopes) ntnvars =
we can tolerate having a variable occurring several times in
different scopes: *) typ <> NtnInternTypeIdent &
make_current_scope (Option.get !idscopes)
- <> make_current_scope (scopt,scopes) then
+ <> make_current_scope (env.tmp_scope,env.scopes) then
error_inconsistent_scope loc id
(make_current_scope (Option.get !idscopes))
- (make_current_scope (scopt,scopes))
+ (make_current_scope (env.tmp_scope,env.scopes))
else
- idscopes := Some (scopt,scopes);
+ idscopes := Some (env.tmp_scope,env.scopes);
match typ with
| NtnInternTypeBinder ->
if istermvar then error_expect_binder_notation_type loc id
@@ -289,24 +296,43 @@ let set_var_scope loc id istermvar (_,_,scopt,scopes) ntnvars =
(* Not in a notation *)
()
-let set_type_scope (ids,unb,tmp_scope,scopes) =
- (ids,unb,Some Notation.type_scope,scopes)
+let set_type_scope env = {env with tmp_scope = Some Notation.type_scope}
-let reset_tmp_scope (ids,unb,tmp_scope,scopes) =
- (ids,unb,None,scopes)
+let reset_tmp_scope env = {env with tmp_scope = None}
-let rec it_mkRProd env body =
+let rec it_mkGProd env body =
match env with
- (na, bk, _, t) :: tl -> it_mkRProd tl (RProd (dummy_loc, na, bk, t, body))
+ (na, bk, _, t) :: tl -> it_mkGProd tl (GProd (dummy_loc, na, bk, t, body))
| [] -> body
-let rec it_mkRLambda env body =
+let rec it_mkGLambda env body =
match env with
- (na, bk, _, t) :: tl -> it_mkRLambda tl (RLambda (dummy_loc, na, bk, t, body))
+ (na, bk, _, t) :: tl -> it_mkGLambda tl (GLambda (dummy_loc, na, bk, t, body))
| [] -> body
(**********************************************************************)
(* Utilities for binders *)
+let build_impls = function
+ |Implicit -> (function
+ |Name id -> Some (id, Impargs.Manual, (true,true))
+ |Anonymous -> anomaly "Anonymous implicit argument")
+ |Explicit -> fun _ -> None
+
+let impls_type_list ?(args = []) =
+ let rec aux acc = function
+ |GProd (_,na,bk,_,c) -> aux ((build_impls bk na)::acc) c
+ |_ -> (Variable,[],List.append args (List.rev acc),[])
+ in aux []
+
+let impls_term_list ?(args = []) =
+ let rec aux acc = function
+ |GLambda (_,na,bk,_,c) -> aux ((build_impls bk na)::acc) c
+ |GRec (_, fix_kind, nas, args, tys, bds) ->
+ let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in
+ let acc' = List.fold_left (fun a (na, bk, _, _) -> (build_impls bk na)::a) acc args.(nb) in
+ aux acc' bds.(nb)
+ |_ -> (Variable,[],List.append args (List.rev acc),[])
+ in aux []
let check_capture loc ty = function
| Name id when occur_var_constr_expr id ty ->
@@ -315,50 +341,55 @@ let check_capture loc ty = function
()
let locate_if_isevar loc na = function
- | RHole _ ->
+ | GHole _ ->
(try match na with
- | Name id -> Reserve.find_reserved_type id
+ | Name id -> glob_constr_of_aconstr loc (Reserve.find_reserved_type id)
| Anonymous -> raise Not_found
- with Not_found -> RHole (loc, Evd.BinderType na))
+ with Not_found -> GHole (loc, Evd.BinderType na))
| x -> x
-let reset_hidden_inductive_implicit_test (ltacvars,namedctxvars,ntnvars,impls) =
- let f = function id,(Inductive _,b,c,d) -> id,(Inductive [],b,c,d) | x -> x in
- (ltacvars,namedctxvars,ntnvars,List.map f impls)
+let reset_hidden_inductive_implicit_test env =
+ { env with impls = Idmap.fold (fun id x ->
+ let x = match x with
+ | (Inductive _,b,c,d) -> (Inductive [],b,c,d)
+ | x -> x
+ in Idmap.add id x) env.impls Idmap.empty }
-let check_hidden_implicit_parameters id (_,_,_,impls) =
- if List.exists (function
- | (_,(Inductive indparams,_,_,_)) -> List.mem id indparams
+let check_hidden_implicit_parameters id impls =
+ if Idmap.exists (fun _ -> function
+ | (Inductive indparams,_,_,_) -> List.mem id indparams
| _ -> false) impls
then
errorlabstrm "" (strbrk "A parameter of an inductive type " ++
pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.")
-let push_name_env ?(global_level=false) lvar (ids,unb,tmpsc,scopes as env) =
+let push_name_env ?(global_level=false) lvar implargs env =
function
| loc,Anonymous ->
if global_level then
user_err_loc (loc,"", str "Anonymous variables not allowed");
env
| loc,Name id ->
- check_hidden_implicit_parameters id lvar;
- set_var_scope loc id false env (let (_,_,ntnvars,_) = lvar in ntnvars);
+ check_hidden_implicit_parameters id env.impls ;
+ set_var_scope loc id false env (let (_,ntnvars) = lvar in ntnvars);
if global_level then Dumpglob.dump_definition (loc,id) true "var"
else Dumpglob.dump_binding loc id;
- (Idset.add id ids,unb,tmpsc,scopes)
+ {env with ids = Idset.add id env.ids; impls = Idmap.add id implargs env.impls}
let intern_generalized_binder ?(global_level=false) intern_type lvar
- (ids,unb,tmpsc,sc as env) bl (loc, na) b b' t ty =
- let ids = match na with Anonymous -> ids | Name na -> Idset.add na ids in
+ env bl (loc, na) b b' t ty =
+ let ids = (match na with Anonymous -> fun x -> x | Name na -> Idset.add na) env.ids in
let ty, ids' =
if t then ty, ids else
Implicit_quantifiers.implicit_application ids
Implicit_quantifiers.combine_params_freevar ty
in
- let ty' = intern_type (ids,true,tmpsc,sc) ty in
- let fvs = Implicit_quantifiers.generalizable_vars_of_rawconstr ~bound:ids ~allowed:ids' ty' in
- let env' = List.fold_left (fun env (x, l) -> push_name_env ~global_level lvar env (l, Name x)) env fvs in
- let bl = List.map (fun (id, loc) -> (Name id, b, None, RHole (loc, Evd.BinderType (Name id)))) fvs in
+ let ty' = intern_type {env with ids = ids; unb = true} ty in
+ let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:ids ~allowed:ids' ty' in
+ let env' = List.fold_left
+ (fun env (x, l) -> push_name_env ~global_level lvar (Variable,[],[],[])(*?*) env (l, Name x))
+ env fvs in
+ let bl = List.map (fun (id, loc) -> (Name id, b, None, GHole (loc, Evd.BinderType (Name id)))) fvs in
let na = match na with
| Anonymous ->
if global_level then na
@@ -371,7 +402,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar
in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
in Name name
| _ -> na
- in (push_name_env ~global_level lvar env' (loc,na)), (na,b',None,ty') :: List.rev bl
+ in (push_name_env ~global_level lvar (impls_type_list ty')(*?*) env' (loc,na)), (na,b',None,ty') :: List.rev bl
let intern_local_binder_aux ?(global_level=false) intern intern_type lvar (env,bl) = function
| LocalRawAssum(nal,bk,ty) ->
@@ -382,36 +413,37 @@ let intern_local_binder_aux ?(global_level=false) intern intern_type lvar (env,b
let ty = locate_if_isevar loc na (intern_type env ty) in
List.fold_left
(fun (env,bl) na ->
- (push_name_env lvar env na,(snd na,k,None,ty)::bl))
+ (push_name_env lvar (impls_type_list ty) env na,(snd na,k,None,ty)::bl))
(env,bl) nal
| Generalized (b,b',t) ->
let env, b = intern_generalized_binder ~global_level intern_type lvar env bl (List.hd nal) b b' t ty in
env, b @ bl)
| LocalRawDef((loc,na as locna),def) ->
- (push_name_env lvar env locna,
- (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
+ let indef = intern env def in
+ (push_name_env lvar (impls_term_list indef) env locna,
+ (na,Explicit,Some(indef),GHole(loc,Evd.BinderType na))::bl)
-let intern_generalization intern (ids,unb,tmp_scope,scopes as env) lvar loc bk ak c =
- let c = intern (ids,true,tmp_scope,scopes) c in
- let fvs = Implicit_quantifiers.generalizable_vars_of_rawconstr ~bound:ids c in
+let intern_generalization intern env lvar loc bk ak c =
+ let c = intern {env with unb = true} c in
+ let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:env.ids c in
let env', c' =
let abs =
let pi =
match ak with
| Some AbsPi -> true
- | None when tmp_scope = Some Notation.type_scope
- || List.mem Notation.type_scope scopes -> true
+ | None when env.tmp_scope = Some Notation.type_scope
+ || List.mem Notation.type_scope env.scopes -> true
| _ -> false
in
if pi then
(fun (id, loc') acc ->
- RProd (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc))
+ GProd (join_loc loc' loc, Name id, bk, GHole (loc', Evd.BinderType (Name id)), acc))
else
(fun (id, loc') acc ->
- RLambda (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc))
+ GLambda (join_loc loc' loc, Name id, bk, GHole (loc', Evd.BinderType (Name id)), acc))
in
List.fold_right (fun (id, loc as lid) (env, acc) ->
- let env' = push_name_env lvar env (loc, Name id) in
+ let env' = push_name_env lvar (Variable,[],[],[]) env (loc, Name id) in
(env', abs lid acc)) fvs (env,c)
in c'
@@ -425,14 +457,15 @@ let iterate_binder intern lvar (env,bl) = function
let ty = intern_type env ty in
let ty = locate_if_isevar loc na ty in
List.fold_left
- (fun (env,bl) na -> (push_name_env lvar env na,(snd na,k,None,ty)::bl))
+ (fun (env,bl) na -> (push_name_env lvar (impls_type_list ty) env na,(snd na,k,None,ty)::bl))
(env,bl) nal
| Generalized (b,b',t) ->
let env, b = intern_generalized_binder intern_type lvar env bl (List.hd nal) b b' t ty in
env, b @ bl)
| LocalRawDef((loc,na as locna),def) ->
- (push_name_env lvar env locna,
- (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
+ let indef = intern env def in
+ (push_name_env lvar (impls_term_list indef) env locna,
+ (na,Explicit,Some(indef),GHole(loc,Evd.BinderType na))::bl)
(**********************************************************************)
(* Syntax extensions *)
@@ -450,14 +483,14 @@ let find_fresh_name renaming (terms,termlists,binders) id =
next_ident_away id fvs
let traverse_binder (terms,_,_ as subst)
- (renaming,(ids,unb,tmpsc,scopes as env))=
+ (renaming,env)=
function
| Anonymous -> (renaming,env),Anonymous
| Name id ->
try
(* Binders bound in the notation are considered first-order objects *)
let _,na = coerce_to_name (fst (List.assoc id terms)) in
- (renaming,(name_fold Idset.add na ids,unb,tmpsc,scopes)), na
+ (renaming,{env with ids = name_fold Idset.add na env.ids}), na
with Not_found ->
(* Binders not bound in the notation do not capture variables *)
(* outside the notation (i.e. in the substitution) *)
@@ -465,7 +498,7 @@ let traverse_binder (terms,_,_ as subst)
let renaming' = if id=id' then renaming else (id,id')::renaming in
(renaming',env), Name id'
-let make_letins loc = List.fold_right (fun (na,b,t) c -> RLetIn (loc,na,b,c))
+let make_letins loc = List.fold_right (fun (na,b,t) c -> GLetIn (loc,na,b,c))
let rec subordinate_letins letins = function
(* binders come in reverse order; the non-let are returned in reverse order together *)
@@ -479,13 +512,13 @@ let rec subordinate_letins letins = function
letins,[]
let rec subst_iterator y t = function
- | RVar (_,id) as x -> if id = y then t else x
- | x -> map_rawconstr (subst_iterator y t) x
+ | GVar (_,id) as x -> if id = y then t else x
+ | x -> map_glob_constr (subst_iterator y t) x
-let subst_aconstr_in_rawconstr loc intern lvar subst infos c =
+let subst_aconstr_in_glob_constr loc intern lvar subst infos c =
let (terms,termlists,binders) = subst in
- let rec aux (terms,binderopt as subst') (renaming,(ids,unb,_,scopes as env)) c =
- let subinfos = renaming,(ids,unb,None,scopes) in
+ let rec aux (terms,binderopt as subst') (renaming,env) c =
+ let subinfos = renaming,{env with tmp_scope = None} in
match c with
| AVar id ->
begin
@@ -493,13 +526,14 @@ let subst_aconstr_in_rawconstr loc intern lvar subst infos c =
(* of the notations *)
try
let (a,(scopt,subscopes)) = List.assoc id terms in
- intern (ids,unb,scopt,subscopes@scopes) a
+ intern {env with tmp_scope = scopt;
+ scopes = subscopes @ env.scopes} a
with Not_found ->
try
- RVar (loc,List.assoc id renaming)
+ GVar (loc,List.assoc id renaming)
with Not_found ->
(* Happens for local notation joint with inductive/fixpoint defs *)
- RVar (loc,id)
+ GVar (loc,id)
end
| AList (x,_,iter,terminator,lassoc) ->
(try
@@ -516,7 +550,7 @@ let subst_aconstr_in_rawconstr loc intern lvar subst infos c =
let na =
try snd (coerce_to_name (fst (List.assoc id terms)))
with Not_found -> na in
- RHole (loc,Evd.BinderType na)
+ GHole (loc,Evd.BinderType na)
| ABinderList (x,_,iter,terminator) ->
(try
(* All elements of the list are in scopes (scopt,subscopes) *)
@@ -533,12 +567,12 @@ let subst_aconstr_in_rawconstr loc intern lvar subst infos c =
anomaly "Inconsistent substitution of recursive notation")
| AProd (Name id, AHole _, c') when option_mem_assoc id binderopt ->
let (na,bk,t),letins = snd (Option.get binderopt) in
- RProd (loc,na,bk,t,make_letins loc letins (aux subst' infos c'))
+ GProd (loc,na,bk,t,make_letins loc letins (aux subst' infos c'))
| ALambda (Name id,AHole _,c') when option_mem_assoc id binderopt ->
let (na,bk,t),letins = snd (Option.get binderopt) in
- RLambda (loc,na,bk,t,make_letins loc letins (aux subst' infos c'))
+ GLambda (loc,na,bk,t,make_letins loc letins (aux subst' infos c'))
| t ->
- rawconstr_of_aconstr_with_binders loc (traverse_binder subst)
+ glob_constr_of_aconstr_with_binders loc (traverse_binder subst)
(aux subst') subinfos t
in aux (terms,None) infos c
@@ -551,15 +585,15 @@ let split_by_type ids =
let make_subst ids l = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids l
-let intern_notation intern (_,_,tmp_scope,scopes as env) lvar loc ntn fullargs =
+let intern_notation intern env lvar loc ntn fullargs =
let ntn,(args,argslist,bll as fullargs) = contract_notation ntn fullargs in
- let ((ids,c),df) = interp_notation loc ntn (tmp_scope,scopes) in
+ let ((ids,c),df) = interp_notation loc ntn (env.tmp_scope,env.scopes) in
Dumpglob.dump_notation_location (ntn_loc loc fullargs ntn) ntn df;
let ids,idsl,idsbl = split_by_type ids in
let terms = make_subst ids args in
let termlists = make_subst idsl argslist in
let binders = make_subst idsbl bll in
- subst_aconstr_in_rawconstr loc intern lvar
+ subst_aconstr_in_glob_constr loc intern lvar
(terms,termlists,binders) ([],env) c
(**********************************************************************)
@@ -569,30 +603,32 @@ let string_of_ty = function
| Inductive _ -> "ind"
| Recursive -> "def"
| Method -> "meth"
+ | Variable -> "var"
-let intern_var (ids,_,_,_ as genv) (ltacvars,namedctxvars,ntnvars,impls) loc id =
+let intern_var genv (ltacvars,ntnvars) namedctx loc id =
let (ltacvars,unbndltacvars) = ltacvars in
(* Is [id] an inductive type potentially with implicit *)
try
- let ty,expl_impls,impls,argsc = List.assoc id impls in
+ let ty,expl_impls,impls,argsc = Idmap.find id genv.impls in
let expl_impls = List.map
(fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) expl_impls in
let tys = string_of_ty ty in
Dumpglob.dump_reference loc "<>" (string_of_id id) tys;
- RVar (loc,id), make_implicits_list impls, argsc, expl_impls
+ GVar (loc,id), make_implicits_list impls, argsc, expl_impls
with Not_found ->
(* Is [id] bound in current term or is an ltac var bound to constr *)
- if Idset.mem id ids or List.mem id ltacvars
+ if Idset.mem id genv.ids or List.mem id ltacvars
then
- RVar (loc,id), [], [], []
+ GVar (loc,id), [], [], []
(* Is [id] a notation variable *)
+
else if List.mem_assoc id ntnvars
then
- (set_var_scope loc id true genv ntnvars; RVar (loc,id), [], [], [])
+ (set_var_scope loc id true genv ntnvars; GVar (loc,id), [], [], [])
(* Is [id] the special variable for recursive notations *)
else if ntnvars <> [] && id = ldots_var
then
- RVar (loc,id), [], [], []
+ GVar (loc,id), [], [], []
else
(* Is [id] bound to a free name in ltac (this is an ltac error message) *)
try
@@ -602,7 +638,7 @@ let intern_var (ids,_,_,_ as genv) (ltacvars,namedctxvars,ntnvars,impls) loc id
| Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
with Not_found ->
(* Is [id] a goal or section variable *)
- let _ = Sign.lookup_named id namedctxvars in
+ let _ = Sign.lookup_named id namedctx in
try
(* [id] a section variable *)
(* Redundant: could be done in intern_qualid *)
@@ -610,14 +646,14 @@ let intern_var (ids,_,_,_ as genv) (ltacvars,namedctxvars,ntnvars,impls) loc id
let impls = implicits_of_global ref in
let scopes = find_arguments_scope ref in
Dumpglob.dump_reference loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var";
- RRef (loc, ref), impls, scopes, []
+ GRef (loc, ref), impls, scopes, []
with _ ->
(* [id] a goal variable *)
- RVar (loc,id), [], [], []
+ GVar (loc,id), [], [], []
let find_appl_head_data = function
- | RRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[]
- | RApp (_,RRef (_,ref),l) as x
+ | GRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[]
+ | GApp (_,GRef (_,ref),l) as x
when l <> [] & Flags.version_strictly_greater Flags.V8_2 ->
let n = List.length l in
x,List.map (drop_first_implicits n) (implicits_of_global ref),
@@ -650,7 +686,7 @@ let intern_reference ref =
let intern_qualid loc qid intern env lvar args =
match intern_extended_global_of_qualid (loc,qid) with
| TrueGlobal ref ->
- RRef (loc, ref), args
+ GRef (loc, ref), args
| SynDef sp ->
let (ids,c) = Syntax_def.search_syntactic_definition sp in
let nids = List.length ids in
@@ -658,20 +694,20 @@ let intern_qualid loc qid intern env lvar args =
let args1,args2 = list_chop nids args in
check_no_explicitation args1;
let subst = make_subst ids (List.map fst args1) in
- subst_aconstr_in_rawconstr loc intern lvar (subst,[],[]) ([],env) c, args2
+ subst_aconstr_in_glob_constr loc intern lvar (subst,[],[]) ([],env) c, args2
(* Rule out section vars since these should have been found by intern_var *)
let intern_non_secvar_qualid loc qid intern env lvar args =
match intern_qualid loc qid intern env lvar args with
- | RRef (loc, VarRef id),_ -> error_global_not_found_loc loc qid
+ | GRef (loc, VarRef id),_ -> error_global_not_found_loc loc qid
| r -> r
-let intern_applied_reference intern (_, unb, _, _ as env) lvar args = function
+let intern_applied_reference intern env namedctx lvar args = function
| Qualid (loc, qid) ->
let r,args2 = intern_qualid loc qid intern env lvar args in
find_appl_head_data r, args2
| Ident (loc, id) ->
- try intern_var env lvar loc id, args
+ try intern_var env lvar namedctx loc id, args
with Not_found ->
let qid = qualid_of_ident id in
try
@@ -679,19 +715,21 @@ let intern_applied_reference intern (_, unb, _, _ as env) lvar args = function
find_appl_head_data r, args2
with e ->
(* Extra allowance for non globalizing functions *)
- if !interning_grammar || unb then
- (RVar (loc,id), [], [], []),args
+ if !interning_grammar || env.unb then
+ (GVar (loc,id), [], [], []),args
else raise e
let interp_reference vars r =
let (r,_,_,_),_ =
intern_applied_reference (fun _ -> error_not_enough_arguments dummy_loc)
- (Idset.empty,false,None,[]) (vars,[],[],[]) [] r
+ {ids = Idset.empty; unb = false ;
+ tmp_scope = None; scopes = []; impls = empty_internalization_env} []
+ (vars,[]) [] r
in r
-let apply_scope_env (ids,unb,_,scopes) = function
- | [] -> (ids,unb,None,scopes), []
- | sc::scl -> (ids,unb,sc,scopes), scl
+let apply_scope_env env = function
+ | [] -> {env with tmp_scope = None}, []
+ | sc::scl -> {env with tmp_scope = sc}, scl
let rec simple_adjust_scopes n = function
| [] -> if n=0 then [] else None :: simple_adjust_scopes (n-1) []
@@ -766,8 +804,8 @@ let alias_of = function
| (id::_,_) -> Name id
let message_redundant_alias (id1,id2) =
- if_verbose warning
- ("Alias variable "^(string_of_id id1)^" is merged with "^(string_of_id id2))
+ if_warn msg_warning
+ (str "Alias variable " ++ pr_id id1 ++ str " is merged with " ++ pr_id id2)
(* Expanding notations *)
@@ -794,7 +832,7 @@ let rec subst_pat_iterator y t (subst,p) = match p with
let pl = simple_product_of_cases_patterns l' in
List.map (fun (subst',pl) -> subst'@subst,PatCstr (loc,id,pl,alias)) pl
-let subst_cases_pattern loc alias intern fullsubst scopes a =
+let subst_cases_pattern loc alias intern fullsubst env a =
let rec aux alias (subst,substlist as fullsubst) = function
| AVar id ->
begin
@@ -802,7 +840,8 @@ let subst_cases_pattern loc alias intern fullsubst scopes a =
(* of the notations *)
try
let (a,(scopt,subscopes)) = List.assoc id subst in
- intern (subscopes@scopes) ([],[]) scopt a
+ intern {env with scopes=subscopes@env.scopes;
+ tmp_scope = scopt} ([],[]) a
with Not_found ->
if id = ldots_var then [], [[], PatVar (loc,Name id)] else
anomaly ("Unbound pattern notation variable: "^(string_of_id id))
@@ -847,7 +886,7 @@ type pattern_qualid_kind =
((identifier * identifier) list * cases_pattern) list) list
| VarPat of identifier
-let find_constructor ref f aliases pats scopes =
+let find_constructor ref f aliases pats env =
let (loc,qid) = qualid_of_reference ref in
let gref =
try locate_extended qid
@@ -865,7 +904,7 @@ let find_constructor ref f aliases pats scopes =
if List.length pats < nvars then error_not_enough_arguments loc;
let pats1,pats2 = list_chop nvars pats in
let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) vars pats1 in
- let idspl1 = List.map (subst_cases_pattern loc Anonymous f (subst,[]) scopes) args in
+ let idspl1 = List.map (subst_cases_pattern loc Anonymous f (subst,[]) env) args in
cstr, idspl1, pats2
| _ -> raise Not_found)
@@ -884,9 +923,9 @@ let find_pattern_variable = function
| Ident (loc,id) -> id
| Qualid (loc,_) as x -> raise (InternalizationError(loc,NotAConstructor x))
-let maybe_constructor ref f aliases scopes =
+let maybe_constructor ref f aliases env =
try
- let c,idspl1,pl2 = find_constructor ref f aliases [] scopes in
+ let c,idspl1,pl2 = find_constructor ref f aliases [] env in
assert (pl2 = []);
ConstrPat (c,idspl1)
with
@@ -894,12 +933,12 @@ let maybe_constructor ref f aliases scopes =
| InternalizationError _ -> VarPat (find_pattern_variable ref)
(* patt var also exists globally but does not satisfy preconditions *)
| (Environ.NotEvaluableConst _ | Not_found) ->
- if_verbose msg_warning (str "pattern " ++ pr_reference ref ++
+ if_warn msg_warning (str "pattern " ++ pr_reference ref ++
str " is understood as a pattern variable");
VarPat (find_pattern_variable ref)
-let mustbe_constructor loc ref f aliases patl scopes =
- try find_constructor ref f aliases patl scopes
+let mustbe_constructor loc ref f aliases patl env =
+ try find_constructor ref f aliases patl env
with (Environ.NotEvaluableConst _ | Not_found) ->
raise (InternalizationError (loc,NotAConstructor ref))
@@ -918,7 +957,7 @@ let sort_fields mode loc l completer =
try Recordops.find_projection
(global_reference_of_reference refer)
with Not_found ->
- user_err_loc (loc, "intern", str"Not a projection")
+ user_err_loc (loc_of_reference refer, "intern", pr_reference refer ++ str": Not a projection")
in
(* elimination of the first field from the projections *)
let rec build_patt l m i acc =
@@ -958,6 +997,10 @@ let sort_fields mode loc l completer =
| [] -> accpatt
| p::q->
let refer, patt = p in
+ let glob_refer = try global_reference_of_reference refer
+ with |Not_found ->
+ user_err_loc (loc_of_reference refer, "intern",
+ str "The field \"" ++ pr_reference refer ++ str "\" does not exist.") in
let rec add_patt l acc =
match l with
| [] ->
@@ -965,7 +1008,7 @@ let sort_fields mode loc l completer =
(loc, "",
str "This record contains fields of different records.")
| (i, a) :: b->
- if global_reference_of_reference refer = a
+ if glob_refer = a
then (i,List.rev_append acc l)
else add_patt b ((i,a)::acc)
in
@@ -988,12 +1031,12 @@ let sort_fields mode loc l completer =
Some (nparams, base_constructor,
List.rev (clean_list sorted_indexed_pattern 0 []))
-let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat=
+let rec intern_cases_pattern genv env (ids,asubst as aliases) pat =
let intern_pat = intern_cases_pattern genv in
match pat with
| CPatAlias (loc, p, id) ->
let aliases' = merge_aliases aliases id in
- intern_pat scopes aliases' tmp_scope p
+ intern_pat env aliases' p
| CPatRecord (loc, l) ->
let sorted_fields = sort_fields false loc l (fun _ l -> (CPatAtom (loc, None))::l) in
let self_patt =
@@ -1001,41 +1044,42 @@ let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat=
| None -> CPatAtom (loc, None)
| Some (_, head, pl) -> CPatCstr(loc, head, pl)
in
- intern_pat scopes aliases tmp_scope self_patt
- | CPatCstr (loc, head, pl) ->
- let c,idslpl1,pl2 = mustbe_constructor loc head intern_pat aliases pl scopes in
+ intern_pat env aliases self_patt
+ | CPatCstr (loc, head, pl) | CPatCstrExpl (loc, head, pl) ->
+ let c,idslpl1,pl2 = mustbe_constructor loc head intern_pat aliases pl env in
check_constructor_length genv loc c idslpl1 pl2;
let argscs2 = find_remaining_constructor_scopes idslpl1 pl2 c in
- let idslpl2 = List.map2 (intern_pat scopes ([],[])) argscs2 pl2 in
+ let idslpl2 = List.map2 (fun x -> intern_pat {env with tmp_scope = x} ([],[])) argscs2 pl2 in
let (ids',pll) = product_of_cases_patterns ids (idslpl1@idslpl2) in
let pl' = List.map (fun (asubst,pl) ->
(asubst, PatCstr (loc,c,pl,alias_of aliases))) pll in
ids',pl'
| CPatNotation (loc,"- _",([CPatPrim(_,Numeral p)],[]))
when Bigint.is_strictly_pos p ->
- intern_pat scopes aliases tmp_scope (CPatPrim(loc,Numeral(Bigint.neg p)))
+ intern_pat env aliases (CPatPrim(loc,Numeral(Bigint.neg p)))
| CPatNotation (_,"( _ )",([a],[])) ->
- intern_pat scopes aliases tmp_scope a
+ intern_pat env aliases a
| CPatNotation (loc, ntn, fullargs) ->
let ntn,(args,argsl as fullargs) = contract_pat_notation ntn fullargs in
- let ((ids',c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
+ let ((ids',c),df) = Notation.interp_notation loc ntn (env.tmp_scope,env.scopes) in
let (ids',idsl',_) = split_by_type ids' in
Dumpglob.dump_notation_location (patntn_loc loc fullargs ntn) ntn df;
let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in
let substlist = List.map2 (fun (id,scl) a -> (id,(a,scl))) idsl' argsl in
let ids'',pl =
subst_cases_pattern loc (alias_of aliases) intern_pat (subst,substlist)
- scopes c
+ env c
in ids@ids'', pl
| CPatPrim (loc, p) ->
let a = alias_of aliases in
let (c,_) = Notation.interp_prim_token_cases_pattern loc p a
- (tmp_scope,scopes) in
+ (env.tmp_scope,env.scopes) in
(ids,[asubst,c])
| CPatDelimiters (loc, key, e) ->
- intern_pat (find_delimiters_scope loc key::scopes) aliases None e
+ intern_pat {env with scopes=find_delimiters_scope loc key::env.scopes;
+ tmp_scope = None} aliases e
| CPatAtom (loc, Some head) ->
- (match maybe_constructor head intern_pat aliases scopes with
+ (match maybe_constructor head intern_pat aliases env with
| ConstrPat (c,idspl) ->
check_constructor_length genv loc c idspl [];
let (ids',pll) = product_of_cases_patterns ids idspl in
@@ -1048,7 +1092,7 @@ let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat=
(ids,[asubst, PatVar (loc,alias_of aliases)])
| CPatOr (loc, pl) ->
assert (pl <> []);
- let pl' = List.map (intern_pat scopes aliases tmp_scope) pl in
+ let pl' = List.map (intern_pat env aliases) pl in
let (idsl,pl') = List.split pl' in
let ids = List.hd idsl in
check_or_pat_variables loc ids (List.tl idsl);
@@ -1067,7 +1111,7 @@ let merge_impargs l args =
let check_projection isproj nargs r =
match (r,isproj) with
- | RRef (loc, ref), Some _ ->
+ | GRef (loc, ref), Some _ ->
(try
let n = Recordops.find_projection_nparams ref + 1 in
if nargs <> n then
@@ -1075,15 +1119,15 @@ let check_projection isproj nargs r =
with Not_found ->
user_err_loc
(loc,"",pr_global_env Idset.empty ref ++ str " is not a registered projection."))
- | _, Some _ -> user_err_loc (loc_of_rawconstr r, "", str "Not a projection.")
+ | _, Some _ -> user_err_loc (loc_of_glob_constr r, "", str "Not a projection.")
| _, None -> ()
let get_implicit_name n imps =
Some (Impargs.name_of_implicit (List.nth imps (n-1)))
let set_hole_implicit i b = function
- | RRef (loc,r) | RApp (_,RRef (loc,r),_) -> (loc,Evd.ImplicitArg (r,i,b))
- | RVar (loc,id) -> (loc,Evd.ImplicitArg (VarRef id,i,b))
+ | GRef (loc,r) | GApp (_,GRef (loc,r),_) -> (loc,Evd.ImplicitArg (r,i,b))
+ | GVar (loc,id) -> (loc,Evd.ImplicitArg (VarRef id,i,b))
| _ -> anomaly "Only refs have implicits"
let exists_implicit_name id =
@@ -1127,13 +1171,13 @@ let extract_explicit_arg imps args =
(* Main loop *)
let internalize sigma globalenv env allow_patvar lvar c =
- let rec intern (ids,unb,tmp_scope,scopes as env) = function
+ let rec intern env = function
| CRef ref as x ->
let (c,imp,subscopes,l),_ =
- intern_applied_reference intern env lvar [] ref in
+ intern_applied_reference intern env (Environ.named_context globalenv) lvar [] ref in
(match intern_impargs c env imp subscopes l with
- | [] -> c
- | l -> RApp (constr_loc x, c, l))
+ | [] -> c
+ | l -> GApp (constr_loc x, c, l))
| CFix (loc, (locid,iddef), dl) ->
let lf = List.map (fun ((_, id),_,_,_,_) -> id) dl in
let dl = Array.of_list dl in
@@ -1142,30 +1186,34 @@ let internalize sigma globalenv env allow_patvar lvar c =
with Not_found ->
raise (InternalizationError (locid,UnboundFixName (false,iddef)))
in
- let idl = Array.map
- (fun (id,(n,order),bl,ty,bd) ->
+ let idl_temp = Array.map
+ (fun (id,(n,order),bl,ty,_) ->
let intern_ro_arg f =
let before, after = split_at_annot bl n in
- let ((ids',_,_,_) as env',rbefore) =
+ let (env',rbefore) =
List.fold_left intern_local_binder (env,[]) before in
- let ro = f (intern (ids', unb, tmp_scope, scopes)) in
+ let ro = f (intern env') in
let n' = Option.map (fun _ -> List.length rbefore) n in
n', ro, List.fold_left intern_local_binder (env',rbefore) after
in
- let n, ro, ((ids',_,_,_),rbl) =
+ let n, ro, (env',rbl) =
match order with
| CStructRec ->
- intern_ro_arg (fun _ -> RStructRec)
+ intern_ro_arg (fun _ -> GStructRec)
| CWfRec c ->
- intern_ro_arg (fun f -> RWfRec (f c))
+ intern_ro_arg (fun f -> GWfRec (f c))
| CMeasureRec (m,r) ->
- intern_ro_arg (fun f -> RMeasureRec (f m, Option.map f r))
+ intern_ro_arg (fun f -> GMeasureRec (f m, Option.map f r))
in
- let ids'' = List.fold_right Idset.add lf ids' in
- ((n, ro), List.rev rbl,
- intern_type (ids',unb,tmp_scope,scopes) ty,
- intern (ids'',unb,None,scopes) bd)) dl in
- RRec (loc,RFix
+ ((n, ro), List.rev rbl, intern_type env' ty, env')) dl in
+ let idl = array_map2 (fun (_,_,_,_,bd) (a,b,c,env') ->
+ let env'' = list_fold_left_i (fun i en name ->
+ let (_,bli,tyi,_) = idl_temp.(i) in
+ let fix_args = (List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli) in
+ push_name_env lvar (impls_type_list ~args:fix_args tyi)
+ en (dummy_loc, Name name)) 0 env' lf in
+ (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in
+ GRec (loc,GFix
(Array.map (fun (ro,_,_,_) -> ro) idl,n),
Array.of_list lf,
Array.map (fun (_,bl,_,_) -> bl) idl,
@@ -1179,21 +1227,26 @@ let internalize sigma globalenv env allow_patvar lvar c =
with Not_found ->
raise (InternalizationError (locid,UnboundFixName (true,iddef)))
in
- let idl = Array.map
- (fun (id,bl,ty,bd) ->
- let ((ids',_,_,_),rbl) =
+ let idl_tmp = Array.map
+ (fun (id,bl,ty,_) ->
+ let (env',rbl) =
List.fold_left intern_local_binder (env,[]) bl in
- let ids'' = List.fold_right Idset.add lf ids' in
(List.rev rbl,
- intern_type (ids',unb,tmp_scope,scopes) ty,
- intern (ids'',unb,None,scopes) bd)) dl in
- RRec (loc,RCoFix n,
+ intern_type env' ty,env')) dl in
+ let idl = array_map2 (fun (_,_,_,bd) (b,c,env') ->
+ let env'' = list_fold_left_i (fun i en name ->
+ let (bli,tyi,_) = idl_tmp.(i) in
+ let cofix_args = List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli in
+ push_name_env lvar (impls_type_list ~args:cofix_args tyi)
+ en (dummy_loc, Name name)) 0 env' lf in
+ (b,c,intern {env'' with tmp_scope = None} bd)) dl idl_tmp in
+ GRec (loc,GCoFix n,
Array.of_list lf,
Array.map (fun (bl,_,_) -> bl) idl,
Array.map (fun (_,ty,_) -> ty) idl,
Array.map (fun (_,_,bd) -> bd) idl)
| CArrow (loc,c1,c2) ->
- RProd (loc, Anonymous, Explicit, intern_type env c1, intern_type env c2)
+ GProd (loc, Anonymous, Explicit, intern_type env c1, intern_type env c2)
| CProdN (loc,[],c2) ->
intern_type env c2
| CProdN (loc,(nal,bk,ty)::bll,c2) ->
@@ -1203,8 +1256,9 @@ let internalize sigma globalenv env allow_patvar lvar c =
| CLambdaN (loc,(nal,bk,ty)::bll,c2) ->
iterate_lam loc (reset_tmp_scope env) bk ty (CLambdaN (loc, bll, c2)) nal
| CLetIn (loc,na,c1,c2) ->
- RLetIn (loc, snd na, intern (reset_tmp_scope env) c1,
- intern (push_name_env lvar env na) c2)
+ let inc1 = intern (reset_tmp_scope env) c1 in
+ GLetIn (loc, snd na, inc1,
+ intern (push_name_env lvar (impls_term_list inc1) env na) c2)
| CNotation (loc,"- _",([CPrim (_,Numeral p)],[],[]))
when Bigint.is_strictly_pos p ->
intern env (CPrim (loc,Numeral (Bigint.neg p)))
@@ -1214,16 +1268,17 @@ let internalize sigma globalenv env allow_patvar lvar c =
| CGeneralization (loc,b,a,c) ->
intern_generalization intern env lvar loc b a c
| CPrim (loc, p) ->
- fst (Notation.interp_prim_token loc p (tmp_scope,scopes))
+ fst (Notation.interp_prim_token loc p (env.tmp_scope,env.scopes))
| CDelimiters (loc, key, e) ->
- intern (ids,unb,None,find_delimiters_scope loc key::scopes) e
+ intern {env with tmp_scope = None;
+ scopes = find_delimiters_scope loc key :: env.scopes} e
| CAppExpl (loc, (isproj,ref), args) ->
let (f,_,args_scopes,_),args =
let args = List.map (fun a -> (a,None)) args in
- intern_applied_reference intern env lvar args ref in
+ intern_applied_reference intern env (Environ.named_context globalenv) lvar args ref in
check_projection isproj (List.length args) f;
- (* Rem: RApp(_,f,[]) stands for @f *)
- RApp (loc, f, intern_args env args_scopes (List.map fst args))
+ (* Rem: GApp(_,f,[]) stands for @f *)
+ GApp (loc, f, intern_args env args_scopes (List.map fst args))
| CApp (loc, (isproj,f), args) ->
let isproj,f,args = match f with
(* Compact notations like "t.(f args') args" *)
@@ -1232,7 +1287,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
| _ -> isproj,f,args in
let (c,impargs,args_scopes,l),args =
match f with
- | CRef ref -> intern_applied_reference intern env lvar args ref
+ | CRef ref -> intern_applied_reference intern env (Environ.named_context globalenv) lvar args ref
| CNotation (loc,ntn,([],[],[])) ->
let c = intern_notation intern env lvar loc ntn ([],[],[]) in
find_appl_head_data c, args
@@ -1242,8 +1297,8 @@ let internalize sigma globalenv env allow_patvar lvar c =
check_projection isproj (List.length args) c;
(match c with
(* Now compact "(f args') args" *)
- | RApp (loc', f', args') -> RApp (join_loc loc' loc, f',args'@args)
- | _ -> RApp (loc, c, args))
+ | GApp (loc', f', args') -> GApp (join_loc loc' loc, f',args'@args)
+ | _ -> GApp (loc, c, args))
| CRecord (loc, _, fs) ->
let cargs =
sort_fields true loc fs
@@ -1261,48 +1316,40 @@ let internalize sigma globalenv env allow_patvar lvar c =
let tms,env' = List.fold_right
(fun citm (inds,env) ->
let (tm,ind),nal = intern_case_item env citm in
- (tm,ind)::inds,List.fold_left
- (push_name_env (reset_hidden_inductive_implicit_test lvar))
- env nal)
+ (tm,ind)::inds,List.fold_left (push_name_env lvar (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal)
tms ([],env) in
let rtnpo = Option.map (intern_type env') rtnpo in
let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
- RCases (loc, sty, rtnpo, tms, List.flatten eqns')
+ GCases (loc, sty, rtnpo, tms, List.flatten eqns')
| CLetTuple (loc, nal, (na,po), b, c) ->
let env' = reset_tmp_scope env in
let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in
let p' = Option.map (fun p ->
- let env'' = List.fold_left
- (push_name_env (reset_hidden_inductive_implicit_test lvar))
- env ids in
+ let env'' = List.fold_left (push_name_env lvar (Variable,[],[],[])) env ids in
intern_type env'' p) po in
- RLetTuple (loc, List.map snd nal, (na', p'), b',
- intern (List.fold_left (push_name_env lvar) env nal) c)
+ GLetTuple (loc, List.map snd nal, (na', p'), b',
+ intern (List.fold_left (push_name_env lvar (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c)
| CIf (loc, c, (na,po), b1, b2) ->
let env' = reset_tmp_scope env in
let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in
let p' = Option.map (fun p ->
- let env'' = List.fold_left
- (push_name_env (reset_hidden_inductive_implicit_test lvar))
- env ids in
+ let env'' = List.fold_left (push_name_env lvar (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) ids in
intern_type env'' p) po in
- RIf (loc, c', (na', p'), intern env b1, intern env b2)
+ GIf (loc, c', (na', p'), intern env b1, intern env b2)
| CHole (loc, k) ->
- RHole (loc, match k with Some k -> k | None -> Evd.QuestionMark (Evd.Define true))
+ GHole (loc, match k with Some k -> k | None -> Evd.QuestionMark (Evd.Define true))
| CPatVar (loc, n) when allow_patvar ->
- RPatVar (loc, n)
+ GPatVar (loc, n)
| CPatVar (loc, _) ->
raise (InternalizationError (loc,IllegalMetavariable))
| CEvar (loc, n, l) ->
- REvar (loc, n, Option.map (List.map (intern env)) l)
+ GEvar (loc, n, Option.map (List.map (intern env)) l)
| CSort (loc, s) ->
- RSort(loc,s)
+ GSort(loc,s)
| CCast (loc, c1, CastConv (k, c2)) ->
- RCast (loc,intern env c1, CastConv (k, intern_type env c2))
+ GCast (loc,intern env c1, CastConv (k, intern_type env c2))
| CCast (loc, c1, CastCoerce) ->
- RCast (loc,intern env c1, CastCoerce)
-
- | CDynamic (loc,d) -> RDynamic (loc,d)
+ GCast (loc,intern env c1, CastCoerce)
and intern_type env = intern (set_type_scope env)
@@ -1310,52 +1357,52 @@ let internalize sigma globalenv env allow_patvar lvar c =
intern_local_binder_aux intern intern_type lvar env bind
(* Expands a multiple pattern into a disjunction of multiple patterns *)
- and intern_multiple_pattern scopes n (loc,pl) =
+ and intern_multiple_pattern env n (loc,pl) =
let idsl_pll =
- List.map (intern_cases_pattern globalenv scopes ([],[]) None) pl in
+ List.map (intern_cases_pattern globalenv {env with tmp_scope = None} ([],[])) pl in
check_number_of_pattern loc n pl;
product_of_cases_patterns [] idsl_pll
(* Expands a disjunction of multiple pattern *)
- and intern_disjunctive_multiple_pattern scopes loc n mpl =
+ and intern_disjunctive_multiple_pattern env loc n mpl =
assert (mpl <> []);
- let mpl' = List.map (intern_multiple_pattern scopes n) mpl in
+ let mpl' = List.map (intern_multiple_pattern env n) mpl in
let (idsl,mpl') = List.split mpl' in
let ids = List.hd idsl in
check_or_pat_variables loc ids (List.tl idsl);
(ids,List.flatten mpl')
(* Expands a pattern-matching clause [lhs => rhs] *)
- and intern_eqn n (ids,unb,tmp_scope,scopes) (loc,lhs,rhs) =
- let eqn_ids,pll = intern_disjunctive_multiple_pattern scopes loc n lhs in
+ and intern_eqn n env (loc,lhs,rhs) =
+ let eqn_ids,pll = intern_disjunctive_multiple_pattern env loc n lhs in
(* Linearity implies the order in ids is irrelevant *)
check_linearity lhs eqn_ids;
- let env_ids = List.fold_right Idset.add eqn_ids ids in
+ let env_ids = List.fold_right Idset.add eqn_ids env.ids in
List.map (fun (asubst,pl) ->
let rhs = replace_vars_constr_expr asubst rhs in
List.iter message_redundant_alias asubst;
- let rhs' = intern (env_ids,unb,tmp_scope,scopes) rhs in
+ let rhs' = intern {env with ids = env_ids} rhs in
(loc,eqn_ids,pl,rhs')) pll
- and intern_case_item (vars,unb,_,scopes as env) (tm,(na,t)) =
+ and intern_case_item env (tm,(na,t)) =
let tm' = intern env tm in
let ids,typ = match t with
| Some t ->
let tids = ids_of_cases_indtype t in
let tids = List.fold_right Idset.add tids Idset.empty in
- let t = intern_type (tids,unb,None,scopes) t in
+ let t = intern_type {env with ids = tids; tmp_scope = None} t in
let loc,ind,l = match t with
- | RRef (loc,IndRef ind) -> (loc,ind,[])
- | RApp (loc,RRef (_,IndRef ind),l) -> (loc,ind,l)
- | _ -> error_bad_inductive_type (loc_of_rawconstr t) in
+ | GRef (loc,IndRef ind) -> (loc,ind,[])
+ | GApp (loc,GRef (_,IndRef ind),l) -> (loc,ind,l)
+ | _ -> error_bad_inductive_type (loc_of_glob_constr t) in
let nparams, nrealargs = inductive_nargs globalenv ind in
let nindargs = nparams + nrealargs in
if List.length l <> nindargs then
error_wrong_numarg_inductive_loc loc globalenv ind nindargs;
let nal = List.map (function
- | RHole (loc,_) -> loc,Anonymous
- | RVar (loc,id) -> loc,Name id
- | c -> user_err_loc (loc_of_rawconstr c,"",str "Not a name.")) l in
+ | GHole (loc,_) -> loc,Anonymous
+ | GVar (loc,id) -> loc,Name id
+ | c -> user_err_loc (loc_of_glob_constr c,"",str "Not a name.")) l in
let parnal,realnal = list_chop nparams nal in
if List.exists (fun (_,na) -> na <> Anonymous) parnal then
error_inductive_parameter_not_implicit loc;
@@ -1363,8 +1410,8 @@ let internalize sigma globalenv env allow_patvar lvar c =
| None ->
[], None in
let na = match tm', na with
- | RVar (loc,id), None when Idset.mem id vars -> loc,Name id
- | RRef (loc, VarRef id), None -> loc,Name id
+ | GVar (loc,id), None when Idset.mem id env.ids -> loc,Name id
+ | GRef (loc, VarRef id), None -> loc,Name id
| _, None -> dummy_loc,Anonymous
| _, Some (loc,na) -> loc,na in
(tm',(snd na,typ)), na::ids
@@ -1373,9 +1420,9 @@ let internalize sigma globalenv env allow_patvar lvar c =
let rec default env bk = function
| (loc1,na as locna)::nal ->
if nal <> [] then check_capture loc1 ty na;
- let body = default (push_name_env lvar env locna) bk nal in
let ty = locate_if_isevar loc1 na (intern_type env ty) in
- RProd (join_loc loc1 loc2, na, bk, ty, body)
+ let body = default (push_name_env lvar (impls_type_list ty) env locna) bk nal in
+ GProd (join_loc loc1 loc2, na, bk, ty, body)
| [] -> intern_type env body
in
match bk with
@@ -1383,22 +1430,22 @@ let internalize sigma globalenv env allow_patvar lvar c =
| Generalized (b,b',t) ->
let env, ibind = intern_generalized_binder intern_type lvar env [] (List.hd nal) b b' t ty in
let body = intern_type env body in
- it_mkRProd ibind body
+ it_mkGProd ibind body
and iterate_lam loc2 env bk ty body nal =
let rec default env bk = function
| (loc1,na as locna)::nal ->
if nal <> [] then check_capture loc1 ty na;
- let body = default (push_name_env lvar env locna) bk nal in
let ty = locate_if_isevar loc1 na (intern_type env ty) in
- RLambda (join_loc loc1 loc2, na, bk, ty, body)
+ let body = default (push_name_env lvar (impls_type_list ty) env locna) bk nal in
+ GLambda (join_loc loc1 loc2, na, bk, ty, body)
| [] -> intern env body
in match bk with
| Default b -> default env b nal
| Generalized (b, b', t) ->
let env, ibind = intern_generalized_binder intern_type lvar env [] (List.hd nal) b b' t ty in
let body = intern env body in
- it_mkRLambda ibind body
+ it_mkGLambda ibind body
and intern_impargs c env l subscopes args =
let l = select_impargs_size (List.length args) l in
@@ -1418,7 +1465,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
(* with implicit arguments if maximal insertion is set *)
[]
else
- RHole (set_hole_implicit (n,get_implicit_name n l) (force_inference_of imp) c) ::
+ GHole (set_hole_implicit (n,get_implicit_name n l) (force_inference_of imp) c) ::
aux (n+1) impl' subscopes' eargs rargs
end
| (imp::impl', a::rargs') ->
@@ -1426,7 +1473,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
| (imp::impl', []) ->
if eargs <> [] then
(let (id,(loc,_)) = List.hd eargs in
- user_err_loc (loc,"",str "Not enough non implicit
+ user_err_loc (loc,"",str "Not enough non implicit \
arguments to accept the argument bound to " ++
pr_id id ++ str"."));
[]
@@ -1450,7 +1497,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
explain_internalization_error e)
(**************************************************************************)
-(* Functions to translate constr_expr into rawconstr *)
+(* Functions to translate constr_expr into glob_constr *)
(**************************************************************************)
let extract_ids env =
@@ -1459,32 +1506,34 @@ let extract_ids env =
Idset.empty
let intern_gen isarity sigma env
- ?(impls=[]) ?(allow_patvar=false) ?(ltacvars=([],[]))
+ ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=([],[]))
c =
let tmp_scope =
if isarity then Some Notation.type_scope else None in
- internalize sigma env (extract_ids env, false, tmp_scope,[])
- allow_patvar (ltacvars,Environ.named_context env, [], impls) c
+ internalize sigma env {ids = extract_ids env; unb = false;
+ tmp_scope = tmp_scope; scopes = [];
+ impls = impls}
+ allow_patvar (ltacvars, []) c
let intern_constr sigma env c = intern_gen false sigma env c
let intern_type sigma env c = intern_gen true sigma env c
-let intern_pattern env patt =
+let intern_pattern globalenv patt =
try
- intern_cases_pattern env [] ([],[]) None patt
+ intern_cases_pattern globalenv {ids = extract_ids globalenv; unb = false;
+ tmp_scope = None; scopes = [];
+ impls = empty_internalization_env} ([],[]) patt
with
InternalizationError (loc,e) ->
user_err_loc (loc,"internalize",explain_internalization_error e)
-type manual_implicits = (explicitation * (bool * bool * bool)) list
-
(*********************************************************************)
(* Functions to parse and interpret constructions *)
let interp_gen kind sigma env
- ?(impls=[]) ?(allow_patvar=false) ?(ltacvars=([],[]))
+ ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=([],[]))
c =
let c = intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars sigma env c in
Default.understand_gen kind sigma env c
@@ -1492,10 +1541,10 @@ let interp_gen kind sigma env
let interp_constr sigma env c =
interp_gen (OfType None) sigma env c
-let interp_type sigma env ?(impls=[]) c =
+let interp_type sigma env ?(impls=empty_internalization_env) c =
interp_gen IsType sigma env ~impls c
-let interp_casted_constr sigma env ?(impls=[]) c typ =
+let interp_casted_constr sigma env ?(impls=empty_internalization_env) c typ =
interp_gen (OfType (Some typ)) sigma env ~impls c
let interp_open_constr sigma env c =
@@ -1503,19 +1552,19 @@ let interp_open_constr sigma env c =
let interp_open_constr_patvar sigma env c =
let raw = intern_gen false sigma env c ~allow_patvar:true in
- let sigma = ref (Evd.create_evar_defs sigma) in
- let evars = ref (Gmap.empty : (identifier,rawconstr) Gmap.t) in
+ let sigma = ref sigma in
+ let evars = ref (Gmap.empty : (identifier,glob_constr) Gmap.t) in
let rec patvar_to_evar r = match r with
- | RPatVar (loc,(_,id)) ->
+ | GPatVar (loc,(_,id)) ->
( try Gmap.find id !evars
with Not_found ->
let ev = Evarutil.e_new_evar sigma env (Termops.new_Type()) in
let ev = Evarutil.e_new_evar sigma env ev in
- let rev = REvar (loc,(fst (Term.destEvar ev)),None) (*TODO*) in
+ let rev = GEvar (loc,(fst (Term.destEvar ev)),None) (*TODO*) in
evars := Gmap.add id rev !evars;
rev
)
- | _ -> map_rawconstr patvar_to_evar r in
+ | _ -> map_glob_constr patvar_to_evar r in
let raw = patvar_to_evar raw in
Default.understand_tcc !sigma env raw
@@ -1523,7 +1572,7 @@ let interp_constr_judgment sigma env c =
Default.understand_judgment sigma env (intern_constr sigma env c)
let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true)
- env ?(impls=[]) kind c =
+ env ?(impls=empty_internalization_env) kind c =
let evdref =
match evdref with
| None -> ref Evd.empty
@@ -1531,43 +1580,44 @@ let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true)
in
let istype = kind = IsType in
let c = intern_gen istype ~impls !evdref env c in
- let imps = Implicit_quantifiers.implicits_of_rawterm ~with_products:istype c in
+ let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:istype c in
Default.understand_tcc_evars ~fail_evar evdref env kind c, imps
let interp_casted_constr_evars_impls ?evdref ?(fail_evar=true)
- env ?(impls=[]) c typ =
+ env ?(impls=empty_internalization_env) c typ =
interp_constr_evars_gen_impls ?evdref ~fail_evar env ~impls (OfType (Some typ)) c
-let interp_type_evars_impls ?evdref ?(fail_evar=true) env ?(impls=[]) c =
+let interp_type_evars_impls ?evdref ?(fail_evar=true) env ?(impls=empty_internalization_env) c =
interp_constr_evars_gen_impls ?evdref ~fail_evar env IsType ~impls c
-let interp_constr_evars_impls ?evdref ?(fail_evar=true) env ?(impls=[]) c =
+let interp_constr_evars_impls ?evdref ?(fail_evar=true) env ?(impls=empty_internalization_env) c =
interp_constr_evars_gen_impls ?evdref ~fail_evar env (OfType None) ~impls c
-let interp_constr_evars_gen evdref env ?(impls=[]) kind c =
- let c = intern_gen (kind=IsType) ~impls ( !evdref) env c in
+let interp_constr_evars_gen evdref env ?(impls=empty_internalization_env) kind c =
+ let c = intern_gen (kind=IsType) ~impls !evdref env c in
Default.understand_tcc_evars evdref env kind c
-let interp_casted_constr_evars evdref env ?(impls=[]) c typ =
+let interp_casted_constr_evars evdref env ?(impls=empty_internalization_env) c typ =
interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c
-let interp_type_evars evdref env ?(impls=[]) c =
+let interp_type_evars evdref env ?(impls=empty_internalization_env) c =
interp_constr_evars_gen evdref env IsType ~impls c
type ltac_sign = identifier list * unbound_ltac_var_map
let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=([],[])) c =
let c = intern_gen as_type ~allow_patvar:true ~ltacvars sigma env c in
- pattern_of_rawconstr c
+ pattern_of_glob_constr c
-let interp_aconstr ?(impls=[]) vars recvars a =
+let interp_aconstr ?(impls=empty_internalization_env) vars recvars a =
let env = Global.env () in
(* [vl] is intended to remember the scope of the free variables of [a] *)
let vl = List.map (fun (id,typ) -> (id,(ref None,typ))) vars in
- let c = internalize Evd.empty (Global.env()) (extract_ids env, false, None, [])
- false (([],[]),Environ.named_context env,vl,impls) a in
+ let c = internalize Evd.empty (Global.env()) {ids = extract_ids env; unb = false;
+ tmp_scope = None; scopes = []; impls = impls}
+ false (([],[]),vl) a in
(* Translate and check that [c] has all its free variables bound in [vars] *)
- let a = aconstr_of_rawconstr vars recvars c in
+ let a = aconstr_of_glob_constr vars recvars c in
(* Splits variables into those that are binding, bound, or both *)
(* binding and bound *)
let out_scope = function None -> None,[] | Some (a,l) -> a,l in
@@ -1579,12 +1629,12 @@ let interp_aconstr ?(impls=[]) vars recvars a =
let interp_binder sigma env na t =
let t = intern_gen true sigma env t in
- let t' = locate_if_isevar (loc_of_rawconstr t) na t in
+ let t' = locate_if_isevar (loc_of_glob_constr t) na t in
Default.understand_type sigma env t'
let interp_binder_evars evdref env na t =
let t = intern_gen true !evdref env t in
- let t' = locate_if_isevar (loc_of_rawconstr t) na t in
+ let t' = locate_if_isevar (loc_of_glob_constr t) na t in
Default.understand_tcc_evars evdref env IsType t'
open Environ
@@ -1595,11 +1645,12 @@ let my_intern_constr sigma env lvar acc c =
let my_intern_type sigma env lvar acc c = my_intern_constr sigma env lvar (set_type_scope acc) c
-let intern_context global_level sigma env params =
- let lvar = (([],[]),Environ.named_context env, [], []) in
- snd (List.fold_left
+let intern_context global_level sigma env impl_env params =
+ let lvar = (([],[]), []) in
+ let lenv, bl = List.fold_left
(intern_local_binder_aux ~global_level (my_intern_constr sigma env lvar) (my_intern_type sigma env lvar) lvar)
- ((extract_ids env,false,None,[]), []) params)
+ ({ids = extract_ids env; unb = false;
+ tmp_scope = None; scopes = []; impls = impl_env}, []) params in (lenv.impls, bl)
let interp_rawcontext_gen understand_type understand_judgment env bl =
let (env, par, _, impls) =
@@ -1607,7 +1658,7 @@ let interp_rawcontext_gen understand_type understand_judgment env bl =
(fun (env,params,n,impls) (na, k, b, t) ->
match b with
None ->
- let t' = locate_if_isevar (loc_of_rawconstr t) na t in
+ let t' = locate_if_isevar (loc_of_glob_constr t) na t in
let t = understand_type env t' in
let d = (na,None,t) in
let impls =
@@ -1624,15 +1675,15 @@ let interp_rawcontext_gen understand_type understand_judgment env bl =
(env,[],1,[]) (List.rev bl)
in (env, par), impls
-let interp_context_gen understand_type understand_judgment ?(global_level=false) sigma env params =
- let bl = intern_context global_level sigma env params in
- interp_rawcontext_gen understand_type understand_judgment env bl
+let interp_context_gen understand_type understand_judgment ?(global_level=false) ?(impl_env=empty_internalization_env) sigma env params =
+ let int_env,bl = intern_context global_level sigma env impl_env params in
+ int_env, interp_rawcontext_gen understand_type understand_judgment env bl
-let interp_context ?(global_level=false) sigma env params =
- interp_context_gen (Default.understand_type sigma)
- (Default.understand_judgment sigma) ~global_level sigma env params
+let interp_context ?(global_level=false) ?(impl_env=empty_internalization_env) sigma env params =
+ interp_context_gen (Default.understand_type sigma)
+ (Default.understand_judgment sigma) ~global_level ~impl_env sigma env params
-let interp_context_evars ?(global_level=false) evdref env params =
+let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) evdref env params =
interp_context_gen (fun env t -> Default.understand_tcc_evars evdref env IsType t)
- (Default.understand_judgment_tcc evdref) ~global_level !evdref env params
-
+ (Default.understand_judgment_tcc evdref) ~global_level ~impl_env !evdref env params
+
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 767ec9ff..be78837f 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -1,39 +1,34 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: constrintern.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
open Names
open Term
open Sign
open Evd
open Environ
open Libnames
-open Rawterm
+open Glob_term
open Pattern
open Topconstr
open Termops
open Pretyping
-(*i*)
-(*s Translation from front abstract syntax of term to untyped terms (rawconstr)
+(** Translation from front abstract syntax of term to untyped terms (glob_constr) *)
- The translation performs:
+(** The translation performs:
- resolution of names :
- check all variables are bound
- make absolute the references to global objets
- resolution of symbolic notations using scopes
- insertion of implicit arguments
-*)
-(* To interpret implicit arguments and arg scopes of recursive variables
+ To interpret implicit arguments and arg scopes of recursive variables
while internalizing inductive types and recursive definitions, and also
projection while typing records.
@@ -45,22 +40,21 @@ type var_internalization_type =
| Inductive of identifier list (* list of params *)
| Recursive
| Method
+ | Variable
type var_internalization_data =
var_internalization_type *
- (* type of the "free" variable, for coqdoc, e.g. while typing the
- constructor of JMeq, "JMeq" behaves as a variable of type Inductive *)
+ (** type of the "free" variable, for coqdoc, e.g. while typing the
+ constructor of JMeq, "JMeq" behaves as a variable of type Inductive *)
identifier list *
- (* impargs to automatically add to the variable, e.g. for "JMeq A a B b"
+ (** impargs to automatically add to the variable, e.g. for "JMeq A a B b"
in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *)
Impargs.implicit_status list * (** signature of impargs of the variable *)
- scope_name option list (* subscopes of the args of the variable *)
+ scope_name option list (** subscopes of the args of the variable *)
-(* A map of free variables to their implicit arguments and scopes *)
-type internalization_env =
- (identifier * var_internalization_data) list
+(** A map of free variables to their implicit arguments and scopes *)
+type internalization_env = var_internalization_data Idmap.t
-(* Contains also a list of identifiers to automatically apply to the variables*)
val empty_internalization_env : internalization_env
val compute_internalization_data : env -> var_internalization_type ->
@@ -70,43 +64,41 @@ val compute_internalization_env : env -> var_internalization_type ->
identifier list -> types list -> Impargs.manual_explicitation list list ->
internalization_env
-type manual_implicits = (explicitation * (bool * bool * bool)) list
-
type ltac_sign = identifier list * unbound_ltac_var_map
-type raw_binder = (name * binding_kind * rawconstr option * rawconstr)
+type glob_binder = (name * binding_kind * glob_constr option * glob_constr)
-(*s Internalisation performs interpretation of global names and notations *)
+(** {6 Internalization performs interpretation of global names and notations } *)
-val intern_constr : evar_map -> env -> constr_expr -> rawconstr
+val intern_constr : evar_map -> env -> constr_expr -> glob_constr
-val intern_type : evar_map -> env -> constr_expr -> rawconstr
+val intern_type : evar_map -> env -> constr_expr -> glob_constr
val intern_gen : bool -> evar_map -> env ->
?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
- constr_expr -> rawconstr
+ constr_expr -> glob_constr
val intern_pattern : env -> cases_pattern_expr ->
Names.identifier list *
- ((Names.identifier * Names.identifier) list * Rawterm.cases_pattern) list
+ ((Names.identifier * Names.identifier) list * Glob_term.cases_pattern) list
-val intern_context : bool -> evar_map -> env -> local_binder list -> raw_binder list
+val intern_context : bool -> evar_map -> env -> internalization_env -> local_binder list -> internalization_env * glob_binder list
-(*s Composing internalization with pretyping *)
+(** {6 Composing internalization with pretyping } *)
-(* Main interpretation function *)
+(** Main interpretation function *)
val interp_gen : typing_constraint -> evar_map -> env ->
?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
constr_expr -> constr
-(* Particular instances *)
+(** Particular instances *)
val interp_constr : evar_map -> env ->
constr_expr -> constr
val interp_type : evar_map -> env -> ?impls:internalization_env ->
- constr_expr -> types
+ constr_expr -> types
val interp_open_constr : evar_map -> env -> constr_expr -> evar_map * constr
@@ -115,18 +107,18 @@ val interp_open_constr_patvar : evar_map -> env -> constr_expr -> evar_map * c
val interp_casted_constr : evar_map -> env -> ?impls:internalization_env ->
constr_expr -> types -> constr
-(* Accepting evars and giving back the manual implicits in addition. *)
+(** Accepting evars and giving back the manual implicits in addition. *)
val interp_casted_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env ->
- ?impls:internalization_env -> constr_expr -> types -> constr * manual_implicits
+ ?impls:internalization_env -> constr_expr -> types -> constr * Impargs.manual_implicits
val interp_type_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool ->
env -> ?impls:internalization_env ->
- constr_expr -> types * manual_implicits
+ constr_expr -> types * Impargs.manual_implicits
val interp_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool ->
env -> ?impls:internalization_env ->
- constr_expr -> constr * manual_implicits
+ constr_expr -> constr * Impargs.manual_implicits
val interp_casted_constr_evars : evar_map ref -> env ->
?impls:internalization_env -> constr_expr -> types -> constr
@@ -134,58 +126,57 @@ val interp_casted_constr_evars : evar_map ref -> env ->
val interp_type_evars : evar_map ref -> env -> ?impls:internalization_env ->
constr_expr -> types
-(*s Build a judgment *)
+(** {6 Build a judgment } *)
val interp_constr_judgment : evar_map -> env -> constr_expr -> unsafe_judgment
-(* Interprets constr patterns *)
+(** Interprets constr patterns *)
val intern_constr_pattern :
evar_map -> env -> ?as_type:bool -> ?ltacvars:ltac_sign ->
constr_pattern_expr -> patvar list * constr_pattern
-(* Raise Not_found if syndef not bound to a name and error if unexisting ref *)
+(** Raise Not_found if syndef not bound to a name and error if unexisting ref *)
val intern_reference : reference -> global_reference
-(* Expands abbreviations (syndef); raise an error if not existing *)
-val interp_reference : ltac_sign -> reference -> rawconstr
+(** Expands abbreviations (syndef); raise an error if not existing *)
+val interp_reference : ltac_sign -> reference -> glob_constr
-(* Interpret binders *)
+(** Interpret binders *)
val interp_binder : evar_map -> env -> name -> constr_expr -> types
val interp_binder_evars : evar_map ref -> env -> name -> constr_expr -> types
-(* Interpret contexts: returns extended env and context *)
+(** Interpret contexts: returns extended env and context *)
-val interp_context_gen : (env -> rawconstr -> types) ->
- (env -> rawconstr -> unsafe_judgment) ->
- ?global_level:bool ->
- evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits
+val interp_context_gen : (env -> glob_constr -> types) ->
+ (env -> glob_constr -> unsafe_judgment) ->
+ ?global_level:bool -> ?impl_env:internalization_env ->
+ evar_map -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits)
-val interp_context : ?global_level:bool ->
- evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits
+val interp_context : ?global_level:bool -> ?impl_env:internalization_env ->
+ evar_map -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits)
-val interp_context_evars : ?global_level:bool ->
- evar_map ref -> env -> local_binder list -> (env * rel_context) * manual_implicits
+val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env ->
+ evar_map ref -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits)
-(* Locating references of constructions, possibly via a syntactic definition *)
-(* (these functions do not modify the glob file) *)
+(** Locating references of constructions, possibly via a syntactic definition
+ (these functions do not modify the glob file) *)
val is_global : identifier -> bool
val construct_reference : named_context -> identifier -> constr
val global_reference : identifier -> constr
val global_reference_in_absolute_module : dir_path -> identifier -> constr
-(* Interprets a term as the left-hand side of a notation; the boolean
- list is a set and this set is [true] for a variable occurring in
- term position, [false] for a variable occurring in binding
- position; [true;false] if in both kinds of position *)
-
+(** Interprets a term as the left-hand side of a notation; the boolean
+ list is a set and this set is [true] for a variable occurring in
+ term position, [false] for a variable occurring in binding
+ position; [true;false] if in both kinds of position *)
val interp_aconstr : ?impls:internalization_env ->
(identifier * notation_var_internalization_type) list ->
(identifier * identifier) list -> constr_expr ->
(identifier * (subscopes * notation_var_internalization_type)) list * aconstr
-(* Globalization leak for Grammar *)
+(** Globalization leak for Grammar *)
val for_grammar : ('a -> 'b) -> 'a -> 'b
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index c5850abf..eb7828ea 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqlib.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Util
open Pp
open Names
@@ -44,8 +42,8 @@ let global_of_extended q =
let gen_constant_in_modules locstr dirs s =
let dirs = List.map make_dir dirs in
- let id = id_of_string s in
- let all = Nametab.locate_extended_all (qualid_of_ident id) in
+ let qualid = qualid_of_string s in
+ let all = Nametab.locate_extended_all qualid in
let all = list_uniquize (list_map_filter global_of_extended all) in
let these = List.filter (has_suffix_in_dirs dirs) all in
match these with
@@ -93,10 +91,12 @@ let logic_constant dir s = gen_constant "Coqlib" ("Logic"::dir) s
let arith_dir = ["Coq";"Arith"]
let arith_modules = [arith_dir]
+let numbers_dir = [ "Coq";"Numbers"]
+let parith_dir = ["Coq";"PArith"]
let narith_dir = ["Coq";"NArith"]
-
let zarith_dir = ["Coq";"ZArith"]
-let zarith_base_modules = [narith_dir;zarith_dir]
+
+let zarith_base_modules = [numbers_dir;parith_dir;narith_dir;zarith_dir]
let init_dir = ["Coq";"Init"]
let init_modules = [
@@ -108,11 +108,6 @@ let init_modules = [
init_dir@["Wf"]
]
-let coq_id = id_of_string "Coq"
-let init_id = id_of_string "Init"
-let arith_id = id_of_string "Arith"
-let datatypes_id = id_of_string "Datatypes"
-
let logic_module_name = ["Coq";"Init";"Logic"]
let logic_module = make_dir logic_module_name
@@ -137,7 +132,7 @@ let make_con dir id = Libnames.encode_con dir id
let id = make_con datatypes_module (id_of_string "id")
let type_of_id = make_con datatypes_module (id_of_string "ID")
-let _ = Cases.set_impossible_default_clause (mkConst id,mkConst type_of_id)
+let _ = Termops.set_impossible_default_clause (mkConst id,mkConst type_of_id)
(** Natural numbers *)
let nat_kn = make_kn datatypes_module (id_of_string "nat")
@@ -192,10 +187,17 @@ let build_sigma_set () = anomaly "Use build_sigma_type"
let build_sigma_type () =
{ proj1 = init_constant ["Specif"] "projT1";
proj2 = init_constant ["Specif"] "projT2";
- elim = init_constant ["Specif"] "sigT_rec";
+ elim = init_constant ["Specif"] "sigT_rect";
intro = init_constant ["Specif"] "existT";
typ = init_constant ["Specif"] "sigT" }
+let build_sigma () =
+ { proj1 = init_constant ["Specif"] "proj1_sig";
+ proj2 = init_constant ["Specif"] "proj2_sig";
+ elim = init_constant ["Specif"] "sig_rect";
+ intro = init_constant ["Specif"] "exist";
+ typ = init_constant ["Specif"] "sig" }
+
let build_prod () =
{ proj1 = init_constant ["Datatypes"] "fst";
proj2 = init_constant ["Datatypes"] "snd";
@@ -227,8 +229,6 @@ let lazy_logic_constant dir id = lazy (logic_constant dir id)
let coq_eq_eq = lazy_init_constant ["Logic"] "eq"
let coq_eq_refl = lazy_init_constant ["Logic"] "eq_refl"
let coq_eq_ind = lazy_init_constant ["Logic"] "eq_ind"
-let coq_eq_rec = lazy_init_constant ["Logic"] "eq_rec"
-let coq_eq_rect = lazy_init_constant ["Logic"] "eq_rect"
let coq_eq_congr = lazy_init_constant ["Logic"] "f_equal"
let coq_eq_sym = lazy_init_constant ["Logic"] "eq_sym"
let coq_eq_trans = lazy_init_constant ["Logic"] "eq_trans"
@@ -250,8 +250,6 @@ let build_coq_eq_refl () = Lazy.force coq_eq_refl
let build_coq_eq_sym () = Lazy.force coq_eq_sym
let build_coq_f_equal2 () = Lazy.force coq_f_equal2
-let build_coq_sym_eq = build_coq_eq_sym (* compatibility *)
-
let build_coq_inversion_eq_data () =
let _ = check_required_library logic_module_name in {
inv_eq = Lazy.force coq_eq_eq;
@@ -263,8 +261,6 @@ let build_coq_inversion_eq_data () =
let coq_jmeq_eq = lazy_logic_constant ["JMeq"] "JMeq"
let coq_jmeq_refl = lazy_logic_constant ["JMeq"] "JMeq_refl"
let coq_jmeq_ind = lazy_logic_constant ["JMeq"] "JMeq_ind"
-let coq_jmeq_rec = lazy_logic_constant ["JMeq"] "JMeq_rec"
-let coq_jmeq_rect = lazy_logic_constant ["JMeq"] "JMeq_rect"
let coq_jmeq_sym = lazy_logic_constant ["JMeq"] "JMeq_sym"
let coq_jmeq_congr = lazy_logic_constant ["JMeq"] "JMeq_congr"
let coq_jmeq_trans = lazy_logic_constant ["JMeq"] "JMeq_trans"
@@ -300,8 +296,6 @@ let build_coq_sumbool () = Lazy.force coq_sumbool
let coq_identity_eq = lazy_init_constant ["Datatypes"] "identity"
let coq_identity_refl = lazy_init_constant ["Datatypes"] "identity_refl"
let coq_identity_ind = lazy_init_constant ["Datatypes"] "identity_ind"
-let coq_identity_rec = lazy_init_constant ["Datatypes"] "identity_rec"
-let coq_identity_rect = lazy_init_constant ["Datatypes"] "identity_rect"
let coq_identity_congr = lazy_init_constant ["Logic_Type"] "identity_congr"
let coq_identity_sym = lazy_init_constant ["Logic_Type"] "identity_sym"
let coq_identity_trans = lazy_init_constant ["Logic_Type"] "identity_trans"
@@ -376,6 +370,7 @@ let coq_jmeq_ref = lazy (gen_reference "Coqlib" ["Logic";"JMeq"] "JMeq")
let coq_eq_true_ref = lazy (gen_reference "Coqlib" ["Init";"Datatypes"] "eq_true")
let coq_existS_ref = lazy (anomaly "use coq_existT_ref")
let coq_existT_ref = lazy (init_reference ["Specif"] "existT")
+let coq_exist_ref = lazy (init_reference ["Specif"] "exist")
let coq_not_ref = lazy (init_reference ["Logic"] "not")
let coq_False_ref = lazy (init_reference ["Logic"] "False")
let coq_sumbool_ref = lazy (init_reference ["Specif"] "sumbool")
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 64a9df6d..5d3580f2 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -1,26 +1,23 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: coqlib.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
open Names
open Libnames
open Nametab
open Term
open Pattern
open Util
-(*i*)
-(*s This module collects the global references, constructions and
+(** This module collects the global references, constructions and
patterns of the standard library used in ocaml files *)
-(*s [find_reference caller_message [dir;subdir;...] s] returns a global
+(** {6 ... } *)
+(** [find_reference caller_message [dir;subdir;...] s] returns a global
reference to the name dir.subdir.(...).s; the corresponding module
must have been required or in the process of being compiled so that
it must be used lazyly; it raises an anomaly with the given message
@@ -30,39 +27,39 @@ type message = string
val find_reference : message -> string list -> string -> global_reference
-(* [coq_reference caller_message [dir;subdir;...] s] returns a
+(** [coq_reference caller_message [dir;subdir;...] s] returns a
global reference to the name Coq.dir.subdir.(...).s *)
val coq_reference : message -> string list -> string -> global_reference
-(* idem but return a term *)
+(** idem but return a term *)
val coq_constant : message -> string list -> string -> constr
-(* Synonyms of [coq_constant] and [coq_reference] *)
+(** Synonyms of [coq_constant] and [coq_reference] *)
val gen_constant : message -> string list -> string -> constr
val gen_reference : message -> string list -> string -> global_reference
-(* Search in several modules (not prefixed by "Coq") *)
+(** Search in several modules (not prefixed by "Coq") *)
val gen_constant_in_modules : string->string list list-> string -> constr
val arith_modules : string list list
val zarith_base_modules : string list list
val init_modules : string list list
-(* For tactics/commands requiring vernacular libraries *)
+(** For tactics/commands requiring vernacular libraries *)
val check_required_library : string list -> unit
-(*s Global references *)
+(** {6 Global references } *)
-(* Modules *)
+(** Modules *)
val logic_module : dir_path
val logic_type_module : dir_path
val datatypes_module_name : string list
val logic_module_name : string list
-(* Natural numbers *)
+(** Natural numbers *)
val nat_path : full_path
val glob_nat : global_reference
val path_of_O : constructor
@@ -70,7 +67,7 @@ val path_of_S : constructor
val glob_O : global_reference
val glob_S : global_reference
-(* Booleans *)
+(** Booleans *)
val glob_bool : global_reference
val path_of_true : constructor
val path_of_false : constructor
@@ -78,12 +75,13 @@ val glob_true : global_reference
val glob_false : global_reference
-(* Equality *)
+(** Equality *)
val glob_eq : global_reference
val glob_identity : global_reference
val glob_jmeq : global_reference
-(*s Constructions and patterns related to Coq initial state are unknown
+(** {6 ... } *)
+(** Constructions and patterns related to Coq initial state are unknown
at compile time. Therefore, we can only provide methods to build
them at runtime. This is the purpose of the [constr delayed] and
[constr_pattern delayed] types. Objects of this time needs to be
@@ -96,7 +94,7 @@ type coq_bool_data = {
andb_true_intro : constr}
val build_bool_type : coq_bool_data delayed
-(*s For Equality tactics *)
+(** {6 For Equality tactics } *)
type coq_sigma_data = {
proj1 : constr;
proj2 : constr;
@@ -106,7 +104,9 @@ type coq_sigma_data = {
val build_sigma_set : coq_sigma_data delayed
val build_sigma_type : coq_sigma_data delayed
-(* Non-dependent pairs in Set from Datatypes *)
+val build_sigma : coq_sigma_data delayed
+
+(** Non-dependent pairs in Set from Datatypes *)
val build_prod : coq_sigma_data delayed
type coq_eq_data = {
@@ -121,17 +121,19 @@ val build_coq_eq_data : coq_eq_data delayed
val build_coq_identity_data : coq_eq_data delayed
val build_coq_jmeq_data : coq_eq_data delayed
-val build_coq_eq : constr delayed (* = [(build_coq_eq_data()).eq] *)
-val build_coq_eq_refl : constr delayed (* = [(build_coq_eq_data()).refl] *)
-val build_coq_eq_sym : constr delayed (* = [(build_coq_eq_data()).sym] *)
+val build_coq_eq : constr delayed (** = [(build_coq_eq_data()).eq] *)
+val build_coq_eq_refl : constr delayed (** = [(build_coq_eq_data()).refl] *)
+val build_coq_eq_sym : constr delayed (** = [(build_coq_eq_data()).sym] *)
val build_coq_f_equal2 : constr delayed
-(* Data needed for discriminate and injection *)
+(** Data needed for discriminate and injection *)
type coq_inversion_data = {
- inv_eq : constr; (* : forall params, t -> Prop *)
- inv_ind : constr; (* : forall params P y, eq params y -> P y *)
- inv_congr: constr (* : forall params B (f:t->B) y, eq params y -> f c=f y *)
+ inv_eq : constr; (** : forall params, args -> Prop *)
+ inv_ind : constr; (** : forall params P (H : P params) args, eq params args
+ -> P args *)
+ inv_congr: constr (** : forall params B (f:t->B) args, eq params args ->
+ f params = f args *)
}
val build_coq_inversion_eq_data : coq_inversion_data delayed
@@ -139,21 +141,22 @@ val build_coq_inversion_identity_data : coq_inversion_data delayed
val build_coq_inversion_jmeq_data : coq_inversion_data delayed
val build_coq_inversion_eq_true_data : coq_inversion_data delayed
-(* Specif *)
+(** Specif *)
val build_coq_sumbool : constr delayed
-(*s Connectives *)
-(* The False proposition *)
+(** {6 ... } *)
+(** Connectives
+ The False proposition *)
val build_coq_False : constr delayed
-(* The True proposition and its unique proof *)
+(** The True proposition and its unique proof *)
val build_coq_True : constr delayed
val build_coq_I : constr delayed
-(* Negation *)
+(** Negation *)
val build_coq_not : constr delayed
-(* Conjunction *)
+(** Conjunction *)
val build_coq_and : constr delayed
val build_coq_conj : constr delayed
val build_coq_iff : constr delayed
@@ -161,10 +164,10 @@ val build_coq_iff : constr delayed
val build_coq_iff_left_proj : constr delayed
val build_coq_iff_right_proj : constr delayed
-(* Disjunction *)
+(** Disjunction *)
val build_coq_or : constr delayed
-(* Existential quantifier *)
+(** Existential quantifier *)
val build_coq_ex : constr delayed
val coq_eq_ref : global_reference lazy_t
@@ -173,6 +176,7 @@ val coq_jmeq_ref : global_reference lazy_t
val coq_eq_true_ref : global_reference lazy_t
val coq_existS_ref : global_reference lazy_t
val coq_existT_ref : global_reference lazy_t
+val coq_exist_ref : global_reference lazy_t
val coq_not_ref : global_reference lazy_t
val coq_False_ref : global_reference lazy_t
val coq_sumbool_ref : global_reference lazy_t
diff --git a/interp/doc.tex b/interp/doc.tex
index 5bd92fbd..4ce5811d 100644
--- a/interp/doc.tex
+++ b/interp/doc.tex
@@ -5,7 +5,7 @@
\ocwsection \label{interp}
This chapter describes the translation from \Coq\ context-dependent
front abstract syntax of terms (\verb=front=) to and from the
-context-free, untyped, raw form of constructions (\verb=rawconstr=).
+context-free, untyped, globalized form of constructions (\verb=glob_constr=).
The modules translating back and forth the front abstract syntax are
organized as follows.
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index c26133c6..07e813e7 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: dumpglob.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
(* Dump of globalization (to be used by coqdoc) *)
@@ -33,8 +31,6 @@ let noglob () = glob_output := NoGlob
let dump_to_stdout () = glob_output := StdOut; glob_file := Pervasives.stdout
-let multi_dump () = !glob_output = MultFiles
-
let dump_to_dotglob f = glob_output := MultFiles
let dump_into_file f = glob_output := File f; open_glob_file f
@@ -42,6 +38,23 @@ let dump_into_file f = glob_output := File f; open_glob_file f
let dump_string s =
if dump () then Pervasives.output_string !glob_file s
+let start_dump_glob vfile =
+ match !glob_output with
+ | MultFiles ->
+ open_glob_file (Filename.chop_extension vfile ^ ".glob");
+ output_string !glob_file "DIGEST ";
+ output_string !glob_file (Digest.to_hex (Digest.file vfile));
+ output_char !glob_file '\n'
+ | File f ->
+ open_glob_file f;
+ output_string !glob_file "DIGEST NO\n"
+ | NoGlob | StdOut ->
+ ()
+
+let end_dump_glob () =
+ match !glob_output with
+ | MultFiles | File _ -> close_glob_file ()
+ | NoGlob | StdOut -> ()
let previous_state = ref MultFiles
let pause () = previous_state := !glob_output; glob_output := NoGlob
@@ -163,11 +176,6 @@ let dump_constraint ((loc, n), _, _) sec ty =
| Names.Name id -> dump_definition (loc, id) sec ty
| Names.Anonymous -> ()
-let dump_name (loc, n) sec ty =
- match n with
- | Names.Name id -> dump_definition (loc, id) sec ty
- | Names.Anonymous -> ()
-
let dump_modref loc mp ty =
if dump () then
let (dp, l) = Lib.split_modpath mp in
@@ -192,12 +200,13 @@ let dump_libref loc dp ty =
let cook_notation df sc =
(* We encode notations so that they are space-free and still human-readable *)
- (* - all spaces are replaced by _ *)
- (* - all _ denoting a non-terminal symbol are replaced by x *)
- (* - all terminal tokens are surrounded by single quotes, including '_' *)
- (* which already denotes terminal _ *)
- (* - all single quotes in terminal tokens are doubled *)
- (* The output is decoded in function Index.prepare_entry of coqdoc *)
+ (* - all spaces are replaced by _ *)
+ (* - all _ denoting a non-terminal symbol are replaced by x *)
+ (* - all terminal tokens are surrounded by single quotes, including '_' *)
+ (* which already denotes terminal _ *)
+ (* - all single quotes in terminal tokens are doubled *)
+ (* - characters < 32 are represented by '^A, '^B, '^C, etc *)
+ (* The output is decoded in function Index.prepare_entry of coqdoc *)
let ntn = String.make (String.length df * 3) '_' in
let j = ref 0 in
let l = String.length df - 1 in
@@ -211,8 +220,13 @@ let cook_notation df sc =
(* Next token is a terminal *)
ntn.[!j] <- '\''; incr j;
while !i <= l && df.[!i] <> ' ' do
- if df.[!i] = '\'' then (ntn.[!j] <- '\''; incr j);
- ntn.[!j] <- df.[!i]; incr j; incr i
+ if df.[!i] < ' ' then
+ let c = char_of_int (int_of_char 'A' + int_of_char df.[!i] - 1) in
+ (String.blit ("'^" ^ String.make 1 c) 0 ntn !j 3; j := !j+3; incr i)
+ else begin
+ if df.[!i] = '\'' then (ntn.[!j] <- '\''; incr j);
+ ntn.[!j] <- df.[!i]; incr j; incr i
+ end
done;
ntn.[!j] <- '\''; incr j
end;
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index d3215c7d..b02cc966 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -1,19 +1,18 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: dumpglob.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
-
-
val open_glob_file : string -> unit
val close_glob_file : unit -> unit
+val start_dump_glob : string -> unit
+val end_dump_glob : unit -> unit
+
val dump : unit -> bool
-val multi_dump : unit -> bool
val noglob : unit -> unit
val dump_to_stdout : unit -> unit
diff --git a/interp/genarg.ml b/interp/genarg.ml
index dd75bbfc..e564bd11 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -1,19 +1,17 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: genarg.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Pp
open Util
open Names
open Nameops
open Nametab
-open Rawterm
+open Glob_term
open Topconstr
open Term
open Evd
@@ -53,11 +51,11 @@ let loc_of_or_by_notation f = function
| AN c -> f c
| ByNotation (loc,s,_) -> loc
-type rawconstr_and_expr = rawconstr * constr_expr option
+type glob_constr_and_expr = glob_constr * constr_expr option
type open_constr_expr = unit * constr_expr
-type open_rawconstr = unit * rawconstr_and_expr
+type open_glob_constr = unit * glob_constr_and_expr
-type rawconstr_pattern_and_expr = rawconstr_and_expr * Pattern.constr_pattern
+type glob_constr_pattern_and_expr = glob_constr_and_expr * Pattern.constr_pattern
type 'a with_ebindings = 'a * open_constr bindings
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 54b415d1..54aadba1 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -1,18 +1,16 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: genarg.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
open Util
open Names
open Term
open Libnames
-open Rawterm
+open Glob_term
open Pattern
open Topconstr
open Term
@@ -26,15 +24,15 @@ type 'a or_by_notation =
val loc_of_or_by_notation : ('a -> loc) -> 'a or_by_notation -> loc
-(* In globalize tactics, we need to keep the initial [constr_expr] to recompute*)
-(* in the environment by the effective calls to Intro, Inversion, etc *)
-(* The [constr_expr] field is [None] in TacDef though *)
-type rawconstr_and_expr = rawconstr * constr_expr option
+(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
+ in the environment by the effective calls to Intro, Inversion, etc
+ The [constr_expr] field is [None] in TacDef though *)
+type glob_constr_and_expr = glob_constr * constr_expr option
type open_constr_expr = unit * constr_expr
-type open_rawconstr = unit * rawconstr_and_expr
+type open_glob_constr = unit * glob_constr_and_expr
-type rawconstr_pattern_and_expr = rawconstr_and_expr * constr_pattern
+type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern
type 'a with_ebindings = 'a * open_constr bindings
@@ -51,40 +49,41 @@ and or_and_intro_pattern_expr = (loc * intro_pattern_expr) list list
val pr_intro_pattern : intro_pattern_expr located -> Pp.std_ppcmds
val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds
-(* The route of a generic argument, from parsing to evaluation
-
-\begin{verbatim}
- parsing in_raw out_raw
- char stream ----> rawtype ----> constr_expr generic_argument --------|
- encapsulation decaps |
- |
- V
- rawtype
- |
- globalization |
- V
- glob_type
- |
- encaps |
- in_glob |
- V
- rawconstr generic_argument
- |
- out in out_glob |
- type <--- constr generic_argument <---- type <------ rawtype <--------|
- | decaps encaps interp decaps
+(** The route of a generic argument, from parsing to evaluation.
+In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc.
+
+{% \begin{%}verbatim{% }%}
+ parsing in_raw out_raw
+ char stream ---> raw_object ---> raw_object generic_argument -------+
+ encapsulation decaps|
+ |
+ V
+ raw_object
+ |
+ globalization |
+ V
+ glob_object
+ |
+ encaps |
+ in_glob |
+ V
+ glob_object generic_argument
+ |
+ out in out_glob |
+ object <--- object generic_argument <--- object <--- glob_object <---+
+ | decaps encaps interp decaps
|
V
effective use
-\end{verbatim}
+{% \end{%}verbatim{% }%}
To distinguish between the uninterpreted (raw), globalized and
interpreted worlds, we annotate the type [generic_argument] by a
-phantom argument which is either [constr_expr], [rawconstr] or
+phantom argument which is either [constr_expr], [glob_constr] or
[constr].
Transformation for each type :
-\begin{verbatim}
+{% \begin{%}verbatim{% }%}
tag raw open type cooked closed type
BoolArgType bool bool
@@ -107,10 +106,10 @@ List0ArgType of argument_type
List1ArgType of argument_type
OptArgType of argument_type
ExtraArgType of string '_a '_b
-\end{verbatim}
+{% \end{%}verbatim{% }%}
*)
-(* All of [rlevel], [glevel] and [tlevel] must be non convertible
+(** All of [rlevel], [glevel] and [tlevel] must be non convertible
to ensure the injectivity of the type inference from type
['co generic_argument] to [('a,'co) abstract_argument_type];
this guarantees that, for 'co fixed, the type of
@@ -172,40 +171,40 @@ val rawwit_quant_hyp : (quantified_hypothesis,rlevel) abstract_argument_type
val globwit_quant_hyp : (quantified_hypothesis,glevel) abstract_argument_type
val wit_quant_hyp : (quantified_hypothesis,tlevel) abstract_argument_type
-val rawwit_sort : (rawsort,rlevel) abstract_argument_type
-val globwit_sort : (rawsort,glevel) abstract_argument_type
+val rawwit_sort : (glob_sort,rlevel) abstract_argument_type
+val globwit_sort : (glob_sort,glevel) abstract_argument_type
val wit_sort : (sorts,tlevel) abstract_argument_type
val rawwit_constr : (constr_expr,rlevel) abstract_argument_type
-val globwit_constr : (rawconstr_and_expr,glevel) abstract_argument_type
+val globwit_constr : (glob_constr_and_expr,glevel) abstract_argument_type
val wit_constr : (constr,tlevel) abstract_argument_type
val rawwit_constr_may_eval : ((constr_expr,reference or_by_notation,constr_expr) may_eval,rlevel) abstract_argument_type
-val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var,rawconstr_pattern_and_expr) may_eval,glevel) abstract_argument_type
+val globwit_constr_may_eval : ((glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) may_eval,glevel) abstract_argument_type
val wit_constr_may_eval : (constr,tlevel) abstract_argument_type
val rawwit_open_constr_gen : bool -> (open_constr_expr,rlevel) abstract_argument_type
-val globwit_open_constr_gen : bool -> (open_rawconstr,glevel) abstract_argument_type
+val globwit_open_constr_gen : bool -> (open_glob_constr,glevel) abstract_argument_type
val wit_open_constr_gen : bool -> (open_constr,tlevel) abstract_argument_type
val rawwit_open_constr : (open_constr_expr,rlevel) abstract_argument_type
-val globwit_open_constr : (open_rawconstr,glevel) abstract_argument_type
+val globwit_open_constr : (open_glob_constr,glevel) abstract_argument_type
val wit_open_constr : (open_constr,tlevel) abstract_argument_type
val rawwit_casted_open_constr : (open_constr_expr,rlevel) abstract_argument_type
-val globwit_casted_open_constr : (open_rawconstr,glevel) abstract_argument_type
+val globwit_casted_open_constr : (open_glob_constr,glevel) abstract_argument_type
val wit_casted_open_constr : (open_constr,tlevel) abstract_argument_type
val rawwit_constr_with_bindings : (constr_expr with_bindings,rlevel) abstract_argument_type
-val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,glevel) abstract_argument_type
+val globwit_constr_with_bindings : (glob_constr_and_expr with_bindings,glevel) abstract_argument_type
val wit_constr_with_bindings : (constr with_bindings sigma,tlevel) abstract_argument_type
val rawwit_bindings : (constr_expr bindings,rlevel) abstract_argument_type
-val globwit_bindings : (rawconstr_and_expr bindings,glevel) abstract_argument_type
+val globwit_bindings : (glob_constr_and_expr bindings,glevel) abstract_argument_type
val wit_bindings : (constr bindings sigma,tlevel) abstract_argument_type
val rawwit_red_expr : ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,rlevel) abstract_argument_type
-val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var,rawconstr_pattern_and_expr) red_expr_gen,glevel) abstract_argument_type
+val globwit_red_expr : ((glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,glevel) abstract_argument_type
val wit_red_expr : ((constr,evaluable_global_reference,constr_pattern) red_expr_gen,tlevel) abstract_argument_type
val wit_list0 :
@@ -222,7 +221,7 @@ val wit_pair :
('b,'co) abstract_argument_type ->
('a * 'b,'co) abstract_argument_type
-(* ['a generic_argument] = (Sigma t:type. t[[constr/'a]]) *)
+(** ['a generic_argument] = (Sigma t:type. t[[constr/'a]]) *)
type 'a generic_argument
val fold_list0 :
@@ -238,7 +237,7 @@ val fold_pair :
('a generic_argument -> 'a generic_argument -> 'c) ->
'a generic_argument -> 'c
-(* [app_list0] fails if applied to an argument not of tag [List0 t]
+(** [app_list0] fails if applied to an argument not of tag [List0 t]
for some [t]; it's the responsability of the caller to ensure it *)
val app_list0 : ('a generic_argument -> 'b generic_argument) ->
@@ -255,7 +254,7 @@ val app_pair :
('a generic_argument -> 'b generic_argument)
-> 'a generic_argument -> 'b generic_argument
-(* create a new generic type of argument: force to associate
+(** create a new generic type of argument: force to associate
unique ML types at each of the three levels *)
val create_arg : string ->
('a,tlevel) abstract_argument_type
@@ -265,7 +264,7 @@ val create_arg : string ->
val exists_argtype : string -> bool
type argument_type =
- (* Basic types *)
+ (** Basic types *)
| BoolArgType
| IntArgType
| IntOrVarArgType
@@ -275,7 +274,7 @@ type argument_type =
| IdentArgType of bool
| VarArgType
| RefArgType
- (* Specific types *)
+ (** Specific types *)
| SortArgType
| ConstrArgType
| ConstrMayEvalArgType
@@ -300,7 +299,7 @@ val out_gen :
('a,'co) abstract_argument_type -> 'co generic_argument -> 'a
-(* [in_generic] is used in combination with camlp4 [Gramext.action] magic
+(** [in_generic] is used in combination with camlp4 [Gramext.action] magic
[in_generic: !l:type, !a:argument_type -> |a|_l -> 'l generic_argument]
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 88ed0873..f2739043 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: implicit_quantifiers.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(*i*)
open Names
open Decl_kinds
@@ -18,7 +16,7 @@ open Environ
open Nametab
open Mod_subst
open Util
-open Rawterm
+open Glob_term
open Topconstr
open Libnames
open Typeclasses
@@ -58,14 +56,14 @@ let cache_generalizable_type (_,(local,cmd)) =
let load_generalizable_type _ (_,(local,cmd)) =
generalizable_table := add_generalizable cmd !generalizable_table
-
-let (in_generalizable, _) =
+
+let in_generalizable : bool * identifier located list option -> obj =
declare_object {(default_object "GENERALIZED-IDENT") with
load_function = load_generalizable_type;
cache_function = cache_generalizable_type;
classify_function = (fun (local, _ as obj) -> if local then Dispose else Keep obj)
}
-
+
let declare_generalizable local gen =
Lib.add_anonymous_leaf (in_generalizable (local, gen))
@@ -138,33 +136,33 @@ let add_name_to_ids set na =
| Anonymous -> set
| Name id -> Idset.add id set
-let generalizable_vars_of_rawconstr ?(bound=Idset.empty) ?(allowed=Idset.empty) =
+let generalizable_vars_of_glob_constr ?(bound=Idset.empty) ?(allowed=Idset.empty) =
let rec vars bound vs = function
- | RVar (loc,id) ->
+ | GVar (loc,id) ->
if is_freevar bound (Global.env ()) id then
if List.mem_assoc id vs then vs
else (id, loc) :: vs
else vs
- | RApp (loc,f,args) -> List.fold_left (vars bound) vs (f::args)
- | RLambda (loc,na,_,ty,c) | RProd (loc,na,_,ty,c) | RLetIn (loc,na,ty,c) ->
+ | GApp (loc,f,args) -> List.fold_left (vars bound) vs (f::args)
+ | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) | GLetIn (loc,na,ty,c) ->
let vs' = vars bound vs ty in
let bound' = add_name_to_ids bound na in
vars bound' vs' c
- | RCases (loc,sty,rtntypopt,tml,pl) ->
+ | GCases (loc,sty,rtntypopt,tml,pl) ->
let vs1 = vars_option bound vs rtntypopt in
let vs2 = List.fold_left (fun vs (tm,_) -> vars bound vs tm) vs1 tml in
List.fold_left (vars_pattern bound) vs2 pl
- | RLetTuple (loc,nal,rtntyp,b,c) ->
+ | GLetTuple (loc,nal,rtntyp,b,c) ->
let vs1 = vars_return_type bound vs rtntyp in
let vs2 = vars bound vs1 b in
let bound' = List.fold_left add_name_to_ids bound nal in
vars bound' vs2 c
- | RIf (loc,c,rtntyp,b1,b2) ->
+ | GIf (loc,c,rtntyp,b1,b2) ->
let vs1 = vars_return_type bound vs rtntyp in
let vs2 = vars bound vs1 c in
let vs3 = vars bound vs2 b1 in
vars bound vs3 b2
- | RRec (loc,fk,idl,bl,tyl,bv) ->
+ | GRec (loc,fk,idl,bl,tyl,bv) ->
let bound' = Array.fold_right Idset.add idl bound in
let vars_fix i vs fid =
let vs1,bound1 =
@@ -182,9 +180,9 @@ let generalizable_vars_of_rawconstr ?(bound=Idset.empty) ?(allowed=Idset.empty)
vars bound1 vs2 bv.(i)
in
array_fold_left_i vars_fix vs idl
- | RCast (loc,c,k) -> let v = vars bound vs c in
+ | GCast (loc,c,k) -> let v = vars bound vs c in
(match k with CastConv (_,t) -> vars bound v t | _ -> v)
- | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> vs
+ | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs
and vars_pattern bound vs (loc,idl,p,c) =
let bound' = List.fold_right Idset.add idl bound in
@@ -205,8 +203,6 @@ let generalizable_vars_of_rawconstr ?(bound=Idset.empty) ?(allowed=Idset.empty)
let rec make_fresh ids env x =
if is_freevar ids env x then x else make_fresh ids env (Nameops.lift_subscript x)
-let next_ident_away_from id avoid = make_fresh avoid (Global.env ()) id
-
let next_name_away_from na avoid =
match na with
| Anonymous -> make_fresh avoid (Global.env ()) (id_of_string "anon")
@@ -297,28 +293,32 @@ let implicit_application env ?(allow_partial=true) f ty =
CAppExpl (loc, (None, id), args), avoid
in c, avoid
-let implicits_of_rawterm ?(with_products=true) l =
- let rec aux i c =
- let abs loc na bk t b =
- let rest = aux (succ i) b in
- if bk = Implicit then
+let implicits_of_glob_constr ?(with_products=true) l =
+ let add_impl i na bk l =
+ if bk = Implicit then
let name =
match na with
| Name id -> Some id
| Anonymous -> None
in
- (ExplByPos (i, name), (true, true, true)) :: rest
- else rest
+ (ExplByPos (i, name), (true, true, true)) :: l
+ else l in
+ let rec aux i c =
+ let abs na bk b =
+ add_impl i na bk (aux (succ i) b)
in
match c with
- | RProd (loc, na, bk, t, b) ->
- if with_products then abs loc na bk t b
+ | GProd (loc, na, bk, t, b) ->
+ if with_products then abs na bk b
else
(if bk = Implicit then
msg_warning (str "Ignoring implicit status of product binder " ++
pr_name na ++ str " and following binders");
[])
- | RLambda (loc, na, bk, t, b) -> abs loc na bk t b
- | RLetIn (loc, na, t, b) -> aux i b
+ | GLambda (loc, na, bk, t, b) -> abs na bk b
+ | GLetIn (loc, na, t, b) -> aux i b
+ | GRec (_, fix_kind, nas, args, tys, bds) ->
+ let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in
+ list_fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb)
| _ -> []
in aux 1 l
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 4442e09d..ce518a9c 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -1,14 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: implicit_quantifiers.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
open Names
open Decl_kinds
open Term
@@ -17,12 +14,11 @@ open Evd
open Environ
open Nametab
open Mod_subst
-open Rawterm
+open Glob_term
open Topconstr
open Util
open Libnames
open Typeclasses
-(*i*)
val declare_generalizable : Vernacexpr.locality_flag -> (identifier located) list option -> unit
@@ -30,7 +26,7 @@ val ids_of_list : identifier list -> Idset.t
val destClassApp : constr_expr -> loc * reference * constr_expr list
val destClassAppExpl : constr_expr -> loc * reference * (constr_expr * explicitation located option) list
-(* Fragile, should be used only for construction a set of identifiers to avoid *)
+(** Fragile, should be used only for construction a set of identifiers to avoid *)
val free_vars_of_constr_expr : constr_expr -> ?bound:Idset.t ->
identifier list -> identifier list
@@ -38,15 +34,15 @@ val free_vars_of_constr_expr : constr_expr -> ?bound:Idset.t ->
val free_vars_of_binders :
?bound:Idset.t -> Names.identifier list -> local_binder list -> Idset.t * Names.identifier list
-(* Returns the generalizable free ids in left-to-right
+(** Returns the generalizable free ids in left-to-right
order with the location of their first occurence *)
-val generalizable_vars_of_rawconstr : ?bound:Idset.t -> ?allowed:Idset.t ->
- rawconstr -> (Names.identifier * loc) list
+val generalizable_vars_of_glob_constr : ?bound:Idset.t -> ?allowed:Idset.t ->
+ glob_constr -> (Names.identifier * loc) list
val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier
-val implicits_of_rawterm : ?with_products:bool -> Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool * bool)) list
+val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits
val combine_params_freevar :
Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
diff --git a/interp/interp.mllib b/interp/interp.mllib
index 3825f3d8..546f277e 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -1,3 +1,4 @@
+Tok
Lexer
Topconstr
Ppextend
@@ -15,4 +16,3 @@ Constrextern
Coqlib
Discharge
Declare
-
diff --git a/interp/modintern.ml b/interp/modintern.ml
index f53d1796..a13560c0 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: modintern.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Pp
open Util
open Names
@@ -16,6 +14,54 @@ open Libnames
open Topconstr
open Constrintern
+type module_internalization_error =
+ | NotAModuleNorModtype of string
+ | IncorrectWithInModule
+ | IncorrectModuleApplication
+
+exception ModuleInternalizationError of module_internalization_error
+
+(*
+val error_declaration_not_path : module_struct_entry -> 'a
+
+val error_not_a_functor : module_struct_entry -> 'a
+
+val error_not_equal : module_path -> module_path -> 'a
+
+val error_result_must_be_signature : unit -> 'a
+
+oval error_not_a_modtype_loc : loc -> string -> 'a
+
+val error_not_a_module_loc : loc -> string -> 'a
+
+val error_not_a_module_or_modtype_loc : loc -> string -> 'a
+
+val error_with_in_module : unit -> 'a
+
+val error_application_to_module_type : unit -> 'a
+*)
+
+let error_result_must_be_signature () =
+ error "The result module type must be a signature."
+
+let error_not_a_modtype_loc loc s =
+ Compat.Loc.raise loc (Modops.ModuleTypingError (Modops.NotAModuleType s))
+
+let error_not_a_module_loc loc s =
+ Compat.Loc.raise loc (Modops.ModuleTypingError (Modops.NotAModule s))
+
+let error_not_a_module_nor_modtype_loc loc s =
+ Compat.Loc.raise loc (ModuleInternalizationError (NotAModuleNorModtype s))
+
+let error_incorrect_with_in_module loc =
+ Compat.Loc.raise loc (ModuleInternalizationError IncorrectWithInModule)
+
+let error_application_to_module_type loc =
+ Compat.Loc.raise loc (ModuleInternalizationError IncorrectModuleApplication)
+
+
+
+
let rec make_mp mp = function
[] -> mp
| h::tl -> make_mp (MPdot(mp, label_of_id h)) tl
@@ -70,7 +116,7 @@ let lookup_module (loc,qid) =
let mp = Nametab.locate_module qid in
Dumpglob.dump_modref loc mp "modtype"; mp
with
- | Not_found -> Modops.error_not_a_module_loc loc (string_of_qualid qid)
+ | Not_found -> error_not_a_module_loc loc (string_of_qualid qid)
let lookup_modtype (loc,qid) =
try
@@ -78,7 +124,7 @@ let lookup_modtype (loc,qid) =
Dumpglob.dump_modref loc mp "mod"; mp
with
| Not_found ->
- Modops.error_not_a_modtype_loc loc (string_of_qualid qid)
+ error_not_a_modtype_loc loc (string_of_qualid qid)
let lookup_module_or_modtype (loc,qid) =
try
@@ -88,7 +134,7 @@ let lookup_module_or_modtype (loc,qid) =
let mp = Nametab.locate_modtype qid in
Dumpglob.dump_modref loc mp "mod"; (mp,false)
with Not_found ->
- Modops.error_not_a_module_or_modtype_loc loc (string_of_qualid qid)
+ error_not_a_module_nor_modtype_loc loc (string_of_qualid qid)
let transl_with_decl env = function
| CWith_Module ((_,fqid),qid) ->
@@ -96,24 +142,35 @@ let transl_with_decl env = function
| CWith_Definition ((_,fqid),c) ->
With_Definition (fqid,interp_constr Evd.empty env c)
+let loc_of_module = function
+ | CMident (loc,_) | CMapply (loc,_,_) | CMwith (loc,_,_) -> loc
+
+let check_module_argument_is_path me' = function
+ | CMident _ -> ()
+ | (CMapply (loc,_,_) | CMwith (loc,_,_)) ->
+ Compat.Loc.raise loc
+ (Modops.ModuleTypingError (Modops.ApplicationToNotPath me'))
+
let rec interp_modexpr env = function
| CMident qid ->
MSEident (lookup_module qid)
- | CMapply (me1,me2) ->
- let me1 = interp_modexpr env me1 in
- let me2 = interp_modexpr env me2 in
- MSEapply(me1,me2)
- | CMwith _ -> Modops.error_with_in_module ()
+ | CMapply (_,me1,me2) ->
+ let me1' = interp_modexpr env me1 in
+ let me2' = interp_modexpr env me2 in
+ check_module_argument_is_path me2' me2;
+ MSEapply(me1',me2')
+ | CMwith (loc,_,_) -> error_incorrect_with_in_module loc
let rec interp_modtype env = function
| CMident qid ->
MSEident (lookup_modtype qid)
- | CMapply (mty1,me) ->
+ | CMapply (_,mty1,me) ->
let mty' = interp_modtype env mty1 in
let me' = interp_modexpr env me in
- MSEapply(mty',me')
- | CMwith (mty,decl) ->
+ check_module_argument_is_path me' me;
+ MSEapply(mty',me')
+ | CMwith (_,mty,decl) ->
let mty = interp_modtype env mty in
let decl = transl_with_decl env decl in
MSEwith(mty,decl)
@@ -122,13 +179,14 @@ let rec interp_modexpr_or_modtype env = function
| CMident qid ->
let (mp,ismod) = lookup_module_or_modtype qid in
(MSEident mp, ismod)
- | CMapply (me1,me2) ->
- let me1,ismod1 = interp_modexpr_or_modtype env me1 in
- let me2,ismod2 = interp_modexpr_or_modtype env me2 in
- if not ismod2 then Modops.error_application_to_module_type ();
- (MSEapply (me1,me2), ismod1)
- | CMwith (me,decl) ->
+ | CMapply (_,me1,me2) ->
+ let me1',ismod1 = interp_modexpr_or_modtype env me1 in
+ let me2',ismod2 = interp_modexpr_or_modtype env me2 in
+ check_module_argument_is_path me2' me2;
+ if not ismod2 then error_application_to_module_type (loc_of_module me2);
+ (MSEapply (me1',me2'), ismod1)
+ | CMwith (loc,me,decl) ->
let me,ismod = interp_modexpr_or_modtype env me in
let decl = transl_with_decl env decl in
- if ismod then Modops.error_with_in_module ();
+ if ismod then error_incorrect_with_in_module loc;
(MSEwith(me,decl), ismod)
diff --git a/interp/modintern.mli b/interp/modintern.mli
index e3a7cc6a..71a00c2f 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -1,14 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: modintern.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
open Declarations
open Environ
open Entries
@@ -16,16 +13,24 @@ open Util
open Libnames
open Names
open Topconstr
-(*i*)
-(* Module expressions and module types are interpreted relatively to
- eventual functor or funsig arguments. *)
+(** Module internalization errors *)
+
+type module_internalization_error =
+ | NotAModuleNorModtype of string
+ | IncorrectWithInModule
+ | IncorrectModuleApplication
+
+exception ModuleInternalizationError of module_internalization_error
+
+(** Module expressions and module types are interpreted relatively to
+ possible functor or functor signature arguments. *)
val interp_modtype : env -> module_ast -> module_struct_entry
val interp_modexpr : env -> module_ast -> module_struct_entry
-(* The following function tries to interprete an ast as a module,
+(** The following function tries to interprete an ast as a module,
and in case of failure, interpretes this ast as a module type.
The boolean is true for a module, false for a module type *)
diff --git a/interp/notation.ml b/interp/notation.ml
index 6e02c40b..8f19ab85 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: notation.ml 14820 2011-12-18 22:11:32Z herbelin $ *)
-
(*i*)
open Util
open Pp
@@ -17,7 +15,7 @@ open Term
open Nametab
open Libnames
open Summary
-open Rawterm
+open Glob_term
open Topconstr
open Ppextend
(*i*)
@@ -73,7 +71,7 @@ let init_scope_map () =
let declare_scope scope =
try let _ = Gmap.find scope !scope_map in ()
with Not_found ->
-(* Flags.if_verbose message ("Creating scope "^scope);*)
+(* Flags.if_warn message ("Creating scope "^scope);*)
scope_map := Gmap.add scope empty_scope !scope_map
let find_scope scope =
@@ -119,7 +117,7 @@ let discharge_scope (_,(local,_,_ as o)) =
let classify_scope (local,_,_ as o) =
if local then Dispose else Substitute o
-let (inScope,outScope) =
+let inScope : bool * bool * scope_elem -> obj =
declare_object {(default_object "SCOPE") with
cache_function = cache_scope;
open_function = open_scope;
@@ -153,15 +151,15 @@ let declare_delimiters scope key =
| None -> scope_map := Gmap.add scope newsc !scope_map
| Some oldkey when oldkey = key -> ()
| Some oldkey ->
- Flags.if_verbose warning
- ("overwriting previous delimiting key "^oldkey^" in scope "^scope);
+ Flags.if_warn msg_warning
+ (str ("Overwriting previous delimiting key "^oldkey^" in scope "^scope));
scope_map := Gmap.add scope newsc !scope_map
end;
try
let oldscope = Gmap.find key !delimiters_map in
if oldscope = scope then ()
else begin
- Flags.if_verbose warning ("Hiding binding of key "^key^" to "^oldscope);
+ Flags.if_warn msg_warning (str ("Hiding binding of key "^key^" to "^oldscope));
delimiters_map := Gmap.add key scope !delimiters_map
end
with Not_found -> delimiters_map := Gmap.add key scope !delimiters_map
@@ -178,7 +176,7 @@ type interp_rule =
| NotationRule of scope_name option * notation
| SynDefRule of kernel_name
-(* We define keys for rawterm and aconstr to split the syntax entries
+(* We define keys for glob_constr and aconstr to split the syntax entries
according to the key of the pattern (adapted from Chet Murthy by HH) *)
type key =
@@ -189,30 +187,25 @@ type key =
let notations_key_table = ref Gmapl.empty
let prim_token_key_table = Hashtbl.create 7
-
-let make_gr = function
- | ConstRef con ->
- ConstRef(constant_of_kn(canonical_con con))
- | IndRef (kn,i) ->
- IndRef(mind_of_kn(canonical_mind kn),i)
- | ConstructRef ((kn,i),j )->
- ConstructRef((mind_of_kn(canonical_mind kn),i),j)
- | VarRef id -> VarRef id
-
-let rawconstr_key = function
- | RApp (_,RRef (_,ref),_) -> RefKey (make_gr ref)
- | RRef (_,ref) -> RefKey (make_gr ref)
+let glob_prim_constr_key = function
+ | GApp (_,GRef (_,ref),_) | GRef (_,ref) -> RefKey (canonical_gr ref)
| _ -> Oth
+let glob_constr_keys = function
+ | GApp (_,GRef (_,ref),_) -> [RefKey (canonical_gr ref); Oth]
+ | GRef (_,ref) -> [RefKey (canonical_gr ref)]
+ | _ -> [Oth]
+
let cases_pattern_key = function
- | PatCstr (_,ref,_,_) -> RefKey (make_gr (ConstructRef ref))
+ | PatCstr (_,ref,_,_) -> RefKey (canonical_gr (ConstructRef ref))
| _ -> Oth
let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *)
- | AApp (ARef ref,args) -> RefKey(make_gr ref), Some (List.length args)
+ | AApp (ARef ref,args) -> RefKey(canonical_gr ref), Some (List.length args)
| AList (_,_,AApp (ARef ref,args),_,_)
- | ABinderList (_,_,AApp (ARef ref,args),_) -> RefKey (make_gr ref), Some (List.length args)
- | ARef ref -> RefKey(make_gr ref), None
+ | ABinderList (_,_,AApp (ARef ref,args),_) -> RefKey (canonical_gr ref), Some (List.length args)
+ | ARef ref -> RefKey(canonical_gr ref), None
+ | AApp (_,args) -> Oth, Some (List.length args)
| _ -> Oth, None
(**********************************************************************)
@@ -221,15 +214,15 @@ let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *)
type required_module = full_path * string list
type 'a prim_token_interpreter =
- loc -> 'a -> rawconstr
+ loc -> 'a -> glob_constr
type cases_pattern_status = bool (* true = use prim token in patterns *)
type 'a prim_token_uninterpreter =
- rawconstr list * (rawconstr -> 'a option) * cases_pattern_status
+ glob_constr list * (glob_constr -> 'a option) * cases_pattern_status
type internal_prim_token_interpreter =
- loc -> prim_token -> required_module * (unit -> rawconstr)
+ loc -> prim_token -> required_module * (unit -> glob_constr)
let prim_token_interpreter_tab =
(Hashtbl.create 7 : (scope_name, internal_prim_token_interpreter) Hashtbl.t)
@@ -246,7 +239,8 @@ let declare_prim_token_interpreter sc interp (patl,uninterp,b) =
declare_scope sc;
add_prim_token_interpreter sc interp;
List.iter (fun pat ->
- Hashtbl.add prim_token_key_table (rawconstr_key pat) (sc,uninterp,b))
+ Hashtbl.add prim_token_key_table
+ (glob_prim_constr_key pat) (sc,uninterp,b))
patl
let mkNumeral n = Numeral n
@@ -353,7 +347,7 @@ let find_prim_token g loc p sc =
(* Try for a user-defined numerical notation *)
try
let (_,c),df = find_notation (notation_of_prim_token p) sc in
- g (rawconstr_of_aconstr loc c),df
+ g (glob_constr_of_aconstr loc c),df
with Not_found ->
(* Try for a primitive numerical notation *)
let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc loc p in
@@ -374,7 +368,7 @@ let interp_prim_token =
interp_prim_token_gen (fun x -> x)
let interp_prim_token_cases_pattern loc p name =
- interp_prim_token_gen (cases_pattern_of_rawconstr name) loc p
+ interp_prim_token_gen (cases_pattern_of_glob_constr name) loc p
let rec interp_notation loc ntn local_scopes =
let scopes = make_current_scopes local_scopes in
@@ -383,8 +377,11 @@ let rec interp_notation loc ntn local_scopes =
user_err_loc
(loc,"",str ("Unknown interpretation for notation \""^ntn^"\"."))
+let isGApp = function GApp _ -> true | _ -> false
+
let uninterp_notations c =
- Gmapl.find (rawconstr_key c) !notations_key_table
+ list_map_append (fun key -> Gmapl.find key !notations_key_table)
+ (glob_constr_keys c)
let uninterp_cases_pattern_notations c =
Gmapl.find (cases_pattern_key c) !notations_key_table
@@ -396,7 +393,8 @@ let availability_of_notation (ntn_scope,ntn) scopes =
let uninterp_prim_token c =
try
- let (sc,numpr,_) = Hashtbl.find prim_token_key_table (rawconstr_key c) in
+ let (sc,numpr,_) =
+ Hashtbl.find prim_token_key_table (glob_prim_constr_key c) in
match numpr c with
| None -> raise No_match
| Some n -> (sc,n)
@@ -407,7 +405,7 @@ let uninterp_prim_token_cases_pattern c =
let k = cases_pattern_key c in
let (sc,numpr,b) = Hashtbl.find prim_token_key_table k in
if not b then raise No_match;
- let na,c = rawconstr_of_closed_cases_pattern c in
+ let na,c = glob_constr_of_closed_cases_pattern c in
match numpr c with
| None -> raise No_match
| Some n -> (na,sc,n)
@@ -439,7 +437,8 @@ open Classops
let class_scope_map = ref (Gmap.empty : (cl_typ,scope_name) Gmap.t)
-let _ = Gmap.add CL_SORT "type_scope" Gmap.empty
+let _ =
+ class_scope_map := Gmap.add CL_SORT "type_scope" Gmap.empty
let declare_class_scope sc cl =
class_scope_map := Gmap.add cl sc !class_scope_map
@@ -447,27 +446,39 @@ let declare_class_scope sc cl =
let find_class_scope cl =
Gmap.find cl !class_scope_map
-let find_class t =
- let t, _ = decompose_app (Reductionops.whd_betaiotazeta Evd.empty t) in
- match kind_of_term t with
- | Var id -> CL_SECVAR id
- | Const sp -> CL_CONST sp
- | Ind ind_sp -> CL_IND ind_sp
- | Prod (_,_,_) -> CL_FUN
- | Sort _ -> CL_SORT
- | _ -> raise Not_found
+let find_class_scope_opt = function
+ | None -> None
+ | Some cl -> try Some (find_class_scope cl) with Not_found -> None
+
+let find_class t = fst (find_class_type Evd.empty t)
(**********************************************************************)
(* Special scopes associated to arguments of a global reference *)
-let rec compute_arguments_scope t =
+let rec compute_arguments_classes t =
match kind_of_term (Reductionops.whd_betaiotazeta Evd.empty t) with
| Prod (_,t,u) ->
- let sc =
- try Some (find_class_scope (find_class t)) with Not_found -> None in
- sc :: compute_arguments_scope u
+ let cl = try Some (find_class t) with Not_found -> None in
+ cl :: compute_arguments_classes u
| _ -> []
+let compute_arguments_scope_full t =
+ let cls = compute_arguments_classes t in
+ let scs = List.map find_class_scope_opt cls in
+ scs, cls
+
+let compute_arguments_scope t = fst (compute_arguments_scope_full t)
+
+(** When merging scope list, we give priority to the first one (computed
+ by substitution), using the second one (user given or earlier automatic)
+ as fallback *)
+
+let rec merge_scope sc1 sc2 = match sc1, sc2 with
+ | [], _ -> sc2
+ | _, [] -> sc1
+ | Some sc :: sc1, _ :: sc2 -> Some sc :: merge_scope sc1 sc2
+ | None :: sc1, sco :: sc2 -> sco :: merge_scope sc1 sc2
+
let arguments_scope = ref Refmap.empty
type arguments_scope_discharge_request =
@@ -475,36 +486,47 @@ type arguments_scope_discharge_request =
| ArgsScopeManual
| ArgsScopeNoDischarge
-let load_arguments_scope _ (_,(_,r,scl)) =
+let load_arguments_scope _ (_,(_,r,scl,cls)) =
List.iter (Option.iter check_scope) scl;
- arguments_scope := Refmap.add r scl !arguments_scope
+ arguments_scope := Refmap.add r (scl,cls) !arguments_scope
let cache_arguments_scope o =
load_arguments_scope 1 o
-let subst_arguments_scope (subst,(req,r,scl)) =
- (ArgsScopeNoDischarge,fst (subst_global subst r),scl)
+let subst_arguments_scope (subst,(req,r,scl,cls)) =
+ let r' = fst (subst_global subst r) in
+ let subst_cl cl =
+ try Option.smartmap (subst_cl_typ subst) cl with Not_found -> None in
+ let cls' = list_smartmap subst_cl cls in
+ let scl' = merge_scope (List.map find_class_scope_opt cls') scl in
+ let scl'' = List.map (Option.map Declaremods.subst_scope) scl' in
+ (ArgsScopeNoDischarge,r',scl'',cls')
-let discharge_arguments_scope (_,(req,r,l)) =
+let discharge_arguments_scope (_,(req,r,l,_)) =
if req = ArgsScopeNoDischarge or (isVarRef r & Lib.is_in_section r) then None
- else Some (req,Lib.discharge_global r,l)
+ else Some (req,Lib.discharge_global r,l,[])
-let classify_arguments_scope (req,_,_ as obj) =
+let classify_arguments_scope (req,_,_,_ as obj) =
if req = ArgsScopeNoDischarge then Dispose else Substitute obj
-let rebuild_arguments_scope (req,r,l) =
+let rebuild_arguments_scope (req,r,l,_) =
match req with
| ArgsScopeNoDischarge -> assert false
| ArgsScopeAuto ->
- (req,r,compute_arguments_scope (Global.type_of_global r))
+ let scs,cls = compute_arguments_scope_full (Global.type_of_global r) in
+ (req,r,scs,cls)
| ArgsScopeManual ->
(* Add to the manually given scopes the one found automatically
for the extra parameters of the section *)
- let l' = compute_arguments_scope (Global.type_of_global r) in
+ let l',cls = compute_arguments_scope_full (Global.type_of_global r) in
let l1,_ = list_chop (List.length l' - List.length l) l' in
- (req,r,l1@l)
+ (req,r,l1@l,cls)
+
+type arguments_scope_obj =
+ arguments_scope_discharge_request * global_reference *
+ scope_name option list * Classops.cl_typ option list
-let (inArgumentsScope,outArgumentsScope) =
+let inArgumentsScope : arguments_scope_obj -> obj =
declare_object {(default_object "ARGUMENTS-SCOPE") with
cache_function = cache_arguments_scope;
load_function = load_arguments_scope;
@@ -515,21 +537,22 @@ let (inArgumentsScope,outArgumentsScope) =
let is_local local ref = local || isVarRef ref && Lib.is_in_section ref
-let declare_arguments_scope_gen req r scl =
- Lib.add_anonymous_leaf (inArgumentsScope (req,r,scl))
+let declare_arguments_scope_gen req r (scl,cls) =
+ Lib.add_anonymous_leaf (inArgumentsScope (req,r,scl,cls))
let declare_arguments_scope local ref scl =
let req =
if is_local local ref then ArgsScopeNoDischarge else ArgsScopeManual in
- declare_arguments_scope_gen req ref scl
+ declare_arguments_scope_gen req ref (scl,[])
let find_arguments_scope r =
- try Refmap.find r !arguments_scope
+ try fst (Refmap.find r !arguments_scope)
with Not_found -> []
let declare_ref_arguments_scope ref =
let t = Global.type_of_global ref in
- declare_arguments_scope_gen ArgsScopeAuto ref (compute_arguments_scope t)
+ declare_arguments_scope_gen ArgsScopeAuto ref (compute_arguments_scope_full t)
+
(********************************)
(* Encoding notations as string *)
@@ -585,11 +608,11 @@ let pr_scope_classes sc =
hov 0 (str ("Bound to class"^(if List.tl l=[] then "" else "es")) ++
spc() ++ prlist_with_sep spc pr_class l) ++ fnl()
-let pr_notation_info prraw ntn c =
+let pr_notation_info prglob ntn c =
str "\"" ++ str ntn ++ str "\" := " ++
- prraw (rawconstr_of_aconstr dummy_loc c)
+ prglob (glob_constr_of_aconstr dummy_loc c)
-let pr_named_scope prraw scope sc =
+let pr_named_scope prglob scope sc =
(if scope = default_scope then
match Gmap.fold (fun _ _ x -> x+1) sc.notations 0 with
| 0 -> str "No lonely notation"
@@ -600,14 +623,14 @@ let pr_named_scope prraw scope sc =
++ pr_scope_classes scope
++ Gmap.fold
(fun ntn ((_,r),(_,df)) strm ->
- pr_notation_info prraw df r ++ fnl () ++ strm)
+ pr_notation_info prglob df r ++ fnl () ++ strm)
sc.notations (mt ())
-let pr_scope prraw scope = pr_named_scope prraw scope (find_scope scope)
+let pr_scope prglob scope = pr_named_scope prglob scope (find_scope scope)
-let pr_scopes prraw =
+let pr_scopes prglob =
Gmap.fold
- (fun scope sc strm -> pr_named_scope prraw scope sc ++ fnl () ++ strm)
+ (fun scope sc strm -> pr_named_scope prglob scope sc ++ fnl () ++ strm)
!scope_map (mt ())
let rec find_default ntn = function
@@ -627,9 +650,6 @@ let factorize_entries = function
(ntn,[c],[]) l in
(ntn,l_of_ntn)::rest
-let is_ident s = (* Poor analysis *)
- String.length s <> 0 & is_letter s.[0]
-
let browse_notation strict ntn map =
let find =
if String.contains ntn ' ' then (=) ntn
@@ -677,7 +697,7 @@ let interp_notation_as_global_reference loc test ntn sc =
| [] -> error_notation_not_reference loc ntn
| _ -> error_ambiguous_notation loc ntn
-let locate_notation prraw ntn scope =
+let locate_notation prglob ntn scope =
let ntns = factorize_entries (browse_notation false ntn !scope_map) in
let scopes = Option.fold_right push_scope scope !scope_stack in
if ntns = [] then
@@ -690,7 +710,7 @@ let locate_notation prraw ntn scope =
prlist
(fun (sc,r,(_,df)) ->
hov 0 (
- pr_notation_info prraw df r ++ tbrk (1,2) ++
+ pr_notation_info prglob df r ++ tbrk (1,2) ++
(if sc = default_scope then mt () else (str ": " ++ str sc)) ++
tbrk (1,2) ++
(if Some sc = scope then str "(default interpretation)" else mt ())
@@ -726,10 +746,10 @@ let collect_notations stack =
(all',ntn::knownntn))
([],[]) stack)
-let pr_visible_in_scope prraw (scope,ntns) =
+let pr_visible_in_scope prglob (scope,ntns) =
let strm =
List.fold_right
- (fun (df,r) strm -> pr_notation_info prraw df r ++ fnl () ++ strm)
+ (fun (df,r) strm -> pr_notation_info prglob df r ++ fnl () ++ strm)
ntns (mt ()) in
(if scope = default_scope then
str "Lonely notation" ++ (if List.length ntns <> 1 then str "s" else mt())
@@ -737,14 +757,14 @@ let pr_visible_in_scope prraw (scope,ntns) =
str "Visible in scope " ++ str scope)
++ fnl () ++ strm
-let pr_scope_stack prraw stack =
+let pr_scope_stack prglob stack =
List.fold_left
- (fun strm scntns -> strm ++ pr_visible_in_scope prraw scntns ++ fnl ())
+ (fun strm scntns -> strm ++ pr_visible_in_scope prglob scntns ++ fnl ())
(mt ()) (collect_notations stack)
-let pr_visibility prraw = function
- | Some scope -> pr_scope_stack prraw (push_scope scope !scope_stack)
- | None -> pr_scope_stack prraw !scope_stack
+let pr_visibility prglob = function
+ | Some scope -> pr_scope_stack prglob (push_scope scope !scope_stack)
+ | None -> pr_scope_stack prglob !scope_stack
(**********************************************************************)
(* Mapping notations to concrete syntax *)
diff --git a/interp/notation.mli b/interp/notation.mli
index 33ffe7b4..f92ef94e 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -1,36 +1,31 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: notation.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
open Util
open Pp
open Bigint
open Names
open Nametab
open Libnames
-open Rawterm
+open Glob_term
open Topconstr
open Ppextend
-(*i*)
-
-(**********************************************************************)
-(* Scopes *)
+(** Notations *)
-(*s A scope is a set of interpreters for symbols + optional
+(** {6 Scopes } *)
+(** A scope is a set of interpreters for symbols + optional
interpreter and printers for integers + optional delimiters *)
type level = precedence * tolerability list
type delimiters = string
type scope
-type scopes (* = [scope_name list] *)
+type scopes (** = [scope_name list] *)
type local_scopes = tmp_scope_name option * scope_name list
@@ -39,41 +34,43 @@ val declare_scope : scope_name -> unit
val current_scopes : unit -> scopes
-(* Check where a scope is opened or not in a scope list, or in
+(** Check where a scope is opened or not in a scope list, or in
* the current opened scopes *)
val scope_is_open_in_scopes : scope_name -> scopes -> bool
val scope_is_open : scope_name -> bool
-(* Open scope *)
+(** Open scope *)
val open_close_scope :
- (* locality *) bool * (* open *) bool * scope_name -> unit
+ (** locality *) bool * (* open *) bool * scope_name -> unit
-(* Extend a list of scopes *)
+(** Extend a list of scopes *)
val empty_scope_stack : scopes
val push_scope : scope_name -> scopes -> scopes
-(* Declare delimiters for printing *)
+val find_scope : scope_name -> scope
+
+(** Declare delimiters for printing *)
val declare_delimiters : scope_name -> delimiters -> unit
val find_delimiters_scope : loc -> delimiters -> scope_name
-(*s Declare and uses back and forth an interpretation of primitive token *)
+(** {6 Declare and uses back and forth an interpretation of primitive token } *)
-(* A numeral interpreter is the pair of an interpreter for **integer**
+(** A numeral interpreter is the pair of an interpreter for **integer**
numbers in terms and an optional interpreter in pattern, if
negative numbers are not supported, the interpreter must fail with
an appropriate error message *)
type notation_location = (dir_path * dir_path) * string
type required_module = full_path * string list
-type cases_pattern_status = bool (* true = use prim token in patterns *)
+type cases_pattern_status = bool (** true = use prim token in patterns *)
type 'a prim_token_interpreter =
- loc -> 'a -> rawconstr
+ loc -> 'a -> glob_constr
type 'a prim_token_uninterpreter =
- rawconstr list * (rawconstr -> 'a option) * cases_pattern_status
+ glob_constr list * (glob_constr -> 'a option) * cases_pattern_status
val declare_numeral_interpreter : scope_name -> required_module ->
bigint prim_token_interpreter -> bigint prim_token_uninterpreter -> unit
@@ -81,28 +78,28 @@ val declare_numeral_interpreter : scope_name -> required_module ->
val declare_string_interpreter : scope_name -> required_module ->
string prim_token_interpreter -> string prim_token_uninterpreter -> unit
-(* Return the [term]/[cases_pattern] bound to a primitive token in a
+(** Return the [term]/[cases_pattern] bound to a primitive token in a
given scope context*)
val interp_prim_token : loc -> prim_token -> local_scopes ->
- rawconstr * (notation_location * scope_name option)
+ glob_constr * (notation_location * scope_name option)
val interp_prim_token_cases_pattern : loc -> prim_token -> name ->
local_scopes -> cases_pattern * (notation_location * scope_name option)
-(* Return the primitive token associated to a [term]/[cases_pattern];
+(** Return the primitive token associated to a [term]/[cases_pattern];
raise [No_match] if no such token *)
val uninterp_prim_token :
- rawconstr -> scope_name * prim_token
+ glob_constr -> scope_name * prim_token
val uninterp_prim_token_cases_pattern :
cases_pattern -> name * scope_name * prim_token
val availability_of_prim_token :
prim_token -> scope_name -> local_scopes -> delimiters option option
-(*s Declare and interpret back and forth a notation *)
+(** {6 Declare and interpret back and forth a notation } *)
-(* Binds a notation in a given scope to an interpretation *)
+(** Binds a notation in a given scope to an interpretation *)
type interp_rule =
| NotationRule of scope_name option * notation
| SynDefRule of kernel_name
@@ -112,39 +109,39 @@ val declare_notation_interpretation : notation -> scope_name option ->
val declare_uninterpretation : interp_rule -> interpretation -> unit
-(* Return the interpretation bound to a notation *)
+(** Return the interpretation bound to a notation *)
val interp_notation : loc -> notation -> local_scopes ->
interpretation * (notation_location * scope_name option)
-(* Return the possible notations for a given term *)
-val uninterp_notations : rawconstr ->
+(** Return the possible notations for a given term *)
+val uninterp_notations : glob_constr ->
(interp_rule * interpretation * int option) list
val uninterp_cases_pattern_notations : cases_pattern ->
(interp_rule * interpretation * int option) list
-(* Test if a notation is available in the scopes *)
-(* context [scopes]; if available, the result is not None; the first *)
-(* argument is itself not None if a delimiters is needed *)
+(** Test if a notation is available in the scopes
+ context [scopes]; if available, the result is not None; the first
+ argument is itself not None if a delimiters is needed *)
val availability_of_notation : scope_name option * notation -> local_scopes ->
(scope_name option * delimiters option) option
-(*s Declare and test the level of a (possibly uninterpreted) notation *)
+(** {6 Declare and test the level of a (possibly uninterpreted) notation } *)
val declare_notation_level : notation -> level -> unit
-val level_of_notation : notation -> level (* raise [Not_found] if no level *)
+val level_of_notation : notation -> level (** raise [Not_found] if no level *)
-(*s** Miscellaneous *)
+(** {6 Miscellaneous} *)
val interp_notation_as_global_reference : loc -> (global_reference -> bool) ->
notation -> delimiters option -> global_reference
-(* Checks for already existing notations *)
+(** Checks for already existing notations *)
val exists_notation_in_scope : scope_name option -> notation ->
interpretation -> bool
-(* Declares and looks for scopes associated to arguments of a global ref *)
+(** Declares and looks for scopes associated to arguments of a global ref *)
val declare_arguments_scope :
- bool (* true=local *) -> global_reference -> scope_name option list -> unit
+ bool (** true=local *) -> global_reference -> scope_name option list -> unit
val find_arguments_scope : global_reference -> scope_name option list
@@ -153,7 +150,7 @@ val declare_ref_arguments_scope : global_reference -> unit
val compute_arguments_scope : Term.types -> scope_name option list
-(* Building notation key *)
+(** Building notation key *)
type symbol =
| Terminal of string
@@ -164,21 +161,19 @@ type symbol =
val make_notation_key : symbol list -> notation
val decompose_notation_key : notation -> symbol list
-(* Prints scopes (expects a pure aconstr printer) *)
-val pr_scope : (rawconstr -> std_ppcmds) -> scope_name -> std_ppcmds
-val pr_scopes : (rawconstr -> std_ppcmds) -> std_ppcmds
-val locate_notation : (rawconstr -> std_ppcmds) -> notation ->
+(** Prints scopes (expects a pure aconstr printer) *)
+val pr_scope : (glob_constr -> std_ppcmds) -> scope_name -> std_ppcmds
+val pr_scopes : (glob_constr -> std_ppcmds) -> std_ppcmds
+val locate_notation : (glob_constr -> std_ppcmds) -> notation ->
scope_name option -> std_ppcmds
-val pr_visibility: (rawconstr -> std_ppcmds) -> scope_name option -> std_ppcmds
+val pr_visibility: (glob_constr -> std_ppcmds) -> scope_name option -> std_ppcmds
-(**********************************************************************)
-(*s Printing rules for notations *)
+(** {6 Printing rules for notations} *)
-(* Declare and look for the printing rule for symbolic notations *)
+(** Declare and look for the printing rule for symbolic notations *)
type unparsing_rule = unparsing list * precedence
val declare_notation_printing_rule : notation -> unparsing_rule -> unit
val find_notation_printing_rule : notation -> unparsing_rule
-(**********************************************************************)
-(* Rem: printing rules for primitive token are canonical *)
+(** Rem: printing rules for primitive token are canonical *)
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index 71029f3f..ebf94bd8 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: ppextend.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
(*i*)
open Pp
open Util
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index e2c4ca98..d3be8c49 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -1,21 +1,17 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: ppextend.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
open Pp
open Names
-(*i*)
-(*s Pretty-print. *)
+(** {6 Pretty-print. } *)
-(* Dealing with precedences *)
+(** Dealing with precedences *)
type precedence = int
diff --git a/interp/reserve.ml b/interp/reserve.ml
index b0303a30..a07f5c84 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: reserve.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(* Reserved names *)
open Util
@@ -17,23 +15,44 @@ open Nameops
open Summary
open Libobject
open Lib
+open Topconstr
+open Libnames
+
+type key =
+ | RefKey of global_reference
+ | Oth
let reserve_table = ref Idmap.empty
+let reserve_revtable = ref Gmapl.empty
+
+let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *)
+ | AApp (ARef ref,args) -> RefKey(canonical_gr ref), Some (List.length args)
+ | AList (_,_,AApp (ARef ref,args),_,_)
+ | ABinderList (_,_,AApp (ARef ref,args),_) -> RefKey (canonical_gr ref), Some (List.length args)
+ | ARef ref -> RefKey(canonical_gr ref), None
+ | _ -> Oth, None
let cache_reserved_type (_,(id,t)) =
- reserve_table := Idmap.add id t !reserve_table
+ let key = fst (aconstr_key t) in
+ reserve_table := Idmap.add id t !reserve_table;
+ reserve_revtable := Gmapl.add key (t,id) !reserve_revtable
-let (in_reserved, _) =
+let in_reserved : identifier * aconstr -> obj =
declare_object {(default_object "RESERVED-TYPE") with
cache_function = cache_reserved_type }
+let freeze_reserved () = (!reserve_table,!reserve_revtable)
+let unfreeze_reserved (r,rr) = reserve_table := r; reserve_revtable := rr
+let init_reserved () =
+ reserve_table := Idmap.empty; reserve_revtable := Gmapl.empty
+
let _ =
Summary.declare_summary "reserved-type"
- { Summary.freeze_function = (fun () -> !reserve_table);
- Summary.unfreeze_function = (fun r -> reserve_table := r);
- Summary.init_function = (fun () -> reserve_table := Idmap.empty) }
+ { Summary.freeze_function = freeze_reserved;
+ Summary.unfreeze_function = unfreeze_reserved;
+ Summary.init_function = init_reserved }
-let declare_reserved_type (loc,id) t =
+let declare_reserved_type_binding (loc,id) t =
if id <> root_of_id id then
user_err_loc(loc,"declare_reserved_type",
(pr_id id ++ str
@@ -45,46 +64,36 @@ let declare_reserved_type (loc,id) t =
with Not_found -> () end;
add_anonymous_leaf (in_reserved (id,t))
+let declare_reserved_type idl t =
+ List.iter (fun id -> declare_reserved_type_binding id t) (List.rev idl)
+
let find_reserved_type id = Idmap.find (root_of_id id) !reserve_table
-open Rawterm
-
-let rec unloc = function
- | RVar (_,id) -> RVar (dummy_loc,id)
- | RApp (_,g,args) -> RApp (dummy_loc,unloc g, List.map unloc args)
- | RLambda (_,na,bk,ty,c) -> RLambda (dummy_loc,na,bk,unloc ty,unloc c)
- | RProd (_,na,bk,ty,c) -> RProd (dummy_loc,na,bk,unloc ty,unloc c)
- | RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c)
- | RCases (_,sty,rtntypopt,tml,pl) ->
- RCases (dummy_loc,sty,
- (Option.map unloc rtntypopt),
- List.map (fun (tm,x) -> (unloc tm,x)) tml,
- List.map (fun (_,idl,p,c) -> (dummy_loc,idl,p,unloc c)) pl)
- | RLetTuple (_,nal,(na,po),b,c) ->
- RLetTuple (dummy_loc,nal,(na,Option.map unloc po),unloc b,unloc c)
- | RIf (_,c,(na,po),b1,b2) ->
- RIf (dummy_loc,unloc c,(na,Option.map unloc po),unloc b1,unloc b2)
- | RRec (_,fk,idl,bl,tyl,bv) ->
- RRec (dummy_loc,fk,idl,
- Array.map (List.map
- (fun (na,k,obd,ty) -> (na,k,Option.map unloc obd, unloc ty)))
- bl,
- Array.map unloc tyl,
- Array.map unloc bv)
- | RCast (_,c, CastConv (k,t)) -> RCast (dummy_loc,unloc c, CastConv (k,unloc t))
- | RCast (_,c, CastCoerce) -> RCast (dummy_loc,unloc c, CastCoerce)
- | RSort (_,x) -> RSort (dummy_loc,x)
- | RHole (_,x) -> RHole (dummy_loc,x)
- | RRef (_,x) -> RRef (dummy_loc,x)
- | REvar (_,x,l) -> REvar (dummy_loc,x,l)
- | RPatVar (_,x) -> RPatVar (dummy_loc,x)
- | RDynamic (_,x) -> RDynamic (dummy_loc,x)
+let constr_key c =
+ try RefKey (canonical_gr (global_of_constr (fst (Term.decompose_app c))))
+ with Not_found -> Oth
+
+let revert_reserved_type t =
+ try
+ let l = Gmapl.find (constr_key t) !reserve_revtable in
+ let t = Detyping.detype false [] [] t in
+ list_try_find
+ (fun (pat,id) ->
+ try let _ = match_aconstr false t ([],pat) in Name id
+ with No_match -> failwith "") l
+ with Not_found | Failure _ -> Anonymous
+
+let _ = Namegen.set_reserved_typed_name revert_reserved_type
+
+open Glob_term
let anonymize_if_reserved na t = match na with
| Name id as na ->
(try
- if not !Flags.raw_print & unloc t = find_reserved_type id
- then RHole (dummy_loc,Evd.BinderType na)
+ if not !Flags.raw_print &
+ (try aconstr_of_glob_constr [] [] t = find_reserved_type id
+ with UserError _ -> false)
+ then GHole (dummy_loc,Evd.BinderType na)
else t
with Not_found -> t)
| Anonymous -> t
diff --git a/interp/reserve.mli b/interp/reserve.mli
index fb60c038..97b22d2b 100644
--- a/interp/reserve.mli
+++ b/interp/reserve.mli
@@ -1,17 +1,16 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: reserve.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
open Util
open Names
-open Rawterm
+open Glob_term
+open Topconstr
-val declare_reserved_type : identifier located -> rawconstr -> unit
-val find_reserved_type : identifier -> rawconstr
-val anonymize_if_reserved : name -> rawconstr -> rawconstr
+val declare_reserved_type : identifier located list -> aconstr -> unit
+val find_reserved_type : identifier -> aconstr
+val anonymize_if_reserved : name -> glob_constr -> glob_constr
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 3eb7c248..4e472b7a 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -11,8 +11,6 @@
(* This file provides high-level name globalization functions *)
-(* $Id:$ *)
-
(* *)
open Pp
open Util
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index 720c88bb..474058cc 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -1,37 +1,35 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id:$ *)
-
open Util
open Names
open Libnames
open Genarg
-(* [locate_global_with_alias] locates global reference possibly following
+(** [locate_global_with_alias] locates global reference possibly following
a notation if this notation has a role of aliasing; raise Not_found
if not bound in the global env; raise an error if bound to a
syntactic def that does not denote a reference *)
val locate_global_with_alias : qualid located -> global_reference
-(* Extract a global_reference from a reference that can be an "alias" *)
+(** Extract a global_reference from a reference that can be an "alias" *)
val global_of_extended_global : extended_global_reference -> global_reference
-(* Locate a reference taking into account possible "alias" notations *)
+(** Locate a reference taking into account possible "alias" notations *)
val global_with_alias : reference -> global_reference
-(* The same for inductive types *)
+(** The same for inductive types *)
val global_inductive_with_alias : reference -> inductive
-(* Locate a reference taking into account notations and "aliases" *)
+(** Locate a reference taking into account notations and "aliases" *)
val smart_global : reference or_by_notation -> global_reference
-(* The same for inductive types *)
+(** The same for inductive types *)
val smart_global_inductive : reference or_by_notation -> inductive
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 44bb02ad..8863bbbd 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: syntax_def.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
open Util
open Pp
open Names
@@ -64,7 +62,7 @@ let subst_syntax_constant (subst,(local,pat,onlyparse)) =
let classify_syntax_constant (local,_,_ as o) =
if local then Dispose else Substitute o
-let (in_syntax_constant, out_syntax_constant) =
+let in_syntax_constant : bool * interpretation * bool -> obj =
declare_object {(default_object "SYNTAXCONSTANT") with
cache_function = cache_syntax_constant;
load_function = load_syntax_constant;
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index a3f846bb..e4da52a3 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -1,23 +1,19 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: syntax_def.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
open Util
open Names
open Topconstr
-open Rawterm
+open Glob_term
open Nametab
open Libnames
-(*i*)
-(* Syntactic definitions. *)
+(** Syntactic definitions. *)
type syndef_interpretation = (identifier * subscopes) list * aconstr
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 2d4e41ec..b484d175 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -1,26 +1,24 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: topconstr.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
(*i*)
open Pp
open Util
open Names
open Nameops
open Libnames
-open Rawterm
+open Glob_term
open Term
open Mod_subst
(*i*)
(**********************************************************************)
-(* This is the subtype of rawconstr allowed in syntactic extensions *)
+(* This is the subtype of glob_constr allowed in syntactic extensions *)
(* For AList: first constr is iterator, second is terminator;
first id is where each argument of the list has to be substituted
@@ -28,12 +26,12 @@ open Mod_subst
boolean is associativity *)
type aconstr =
- (* Part common to rawconstr and cases_pattern *)
+ (* Part common to glob_constr and cases_pattern *)
| ARef of global_reference
| AVar of identifier
| AApp of aconstr * aconstr list
| AList of identifier * identifier * aconstr * aconstr * bool
- (* Part only in rawconstr *)
+ (* Part only in glob_constr *)
| ALambda of name * aconstr * aconstr
| AProd of name * aconstr * aconstr
| ABinderList of identifier * identifier * aconstr * aconstr
@@ -46,7 +44,7 @@ type aconstr =
| ARec of fix_kind * identifier array *
(name * aconstr option * aconstr) list array * aconstr array *
aconstr array
- | ASort of rawsort
+ | ASort of glob_sort
| AHole of Evd.hole_kind
| APatVar of patvar
| ACast of aconstr * aconstr cast_type
@@ -67,7 +65,7 @@ type interpretation =
(identifier * (subscopes * notation_var_instance_type)) list * aconstr
(**********************************************************************)
-(* Re-interpret a notation as a rawconstr, taking care of binders *)
+(* Re-interpret a notation as a glob_constr, taking care of binders *)
let name_to_ident = function
| Anonymous -> error "This expression should be a simple identifier."
@@ -83,43 +81,43 @@ let rec cases_pattern_fold_map loc g e = function
let e',patl' = list_fold_map (cases_pattern_fold_map loc g) e patl in
e', PatCstr (loc,cstr,patl',na')
-let rec subst_rawvars l = function
- | RVar (_,id) as r -> (try List.assoc id l with Not_found -> r)
- | RProd (loc,Name id,bk,t,c) ->
+let rec subst_glob_vars l = function
+ | GVar (_,id) as r -> (try List.assoc id l with Not_found -> r)
+ | GProd (loc,Name id,bk,t,c) ->
let id =
- try match List.assoc id l with RVar(_,id') -> id' | _ -> id
+ try match List.assoc id l with GVar(_,id') -> id' | _ -> id
with Not_found -> id in
- RProd (loc,Name id,bk,subst_rawvars l t,subst_rawvars l c)
- | RLambda (loc,Name id,bk,t,c) ->
+ GProd (loc,Name id,bk,subst_glob_vars l t,subst_glob_vars l c)
+ | GLambda (loc,Name id,bk,t,c) ->
let id =
- try match List.assoc id l with RVar(_,id') -> id' | _ -> id
+ try match List.assoc id l with GVar(_,id') -> id' | _ -> id
with Not_found -> id in
- RLambda (loc,Name id,bk,subst_rawvars l t,subst_rawvars l c)
- | r -> map_rawconstr (subst_rawvars l) r (* assume: id is not binding *)
+ GLambda (loc,Name id,bk,subst_glob_vars l t,subst_glob_vars l c)
+ | r -> map_glob_constr (subst_glob_vars l) r (* assume: id is not binding *)
let ldots_var = id_of_string ".."
-let rawconstr_of_aconstr_with_binders loc g f e = function
- | AVar id -> RVar (loc,id)
- | AApp (a,args) -> RApp (loc,f e a, List.map (f e) args)
+let glob_constr_of_aconstr_with_binders loc g f e = function
+ | AVar id -> GVar (loc,id)
+ | AApp (a,args) -> GApp (loc,f e a, List.map (f e) args)
| AList (x,y,iter,tail,swap) ->
let t = f e tail in let it = f e iter in
- let innerl = (ldots_var,t)::(if swap then [] else [x,RVar(loc,y)]) in
- let inner = RApp (loc,RVar (loc,ldots_var),[subst_rawvars innerl it]) in
- let outerl = (ldots_var,inner)::(if swap then [x,RVar(loc,y)] else []) in
- subst_rawvars outerl it
+ let innerl = (ldots_var,t)::(if swap then [] else [x,GVar(loc,y)]) in
+ let inner = GApp (loc,GVar (loc,ldots_var),[subst_glob_vars innerl it]) in
+ let outerl = (ldots_var,inner)::(if swap then [x,GVar(loc,y)] else []) in
+ subst_glob_vars outerl it
| ABinderList (x,y,iter,tail) ->
let t = f e tail in let it = f e iter in
- let innerl = [(ldots_var,t);(x,RVar(loc,y))] in
- let inner = RApp (loc,RVar (loc,ldots_var),[subst_rawvars innerl it]) in
+ let innerl = [(ldots_var,t);(x,GVar(loc,y))] in
+ let inner = GApp (loc,GVar (loc,ldots_var),[subst_glob_vars innerl it]) in
let outerl = [(ldots_var,inner)] in
- subst_rawvars outerl it
+ subst_glob_vars outerl it
| ALambda (na,ty,c) ->
- let e',na = g e na in RLambda (loc,na,Explicit,f e ty,f e' c)
+ let e',na = g e na in GLambda (loc,na,Explicit,f e ty,f e' c)
| AProd (na,ty,c) ->
- let e',na = g e na in RProd (loc,na,Explicit,f e ty,f e' c)
+ let e',na = g e na in GProd (loc,na,Explicit,f e ty,f e' c)
| ALetIn (na,b,c) ->
- let e',na = g e na in RLetIn (loc,na,f e b,f e' c)
+ let e',na = g e na in GLetIn (loc,na,f e b,f e' c)
| ACases (sty,rtntypopt,tml,eqnl) ->
let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
let e',t' = match t with
@@ -135,36 +133,36 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
let ((idl,e),patl) =
list_fold_map (cases_pattern_fold_map loc fold) ([],e) patl in
(loc,idl,patl,f e rhs)) eqnl in
- RCases (loc,sty,Option.map (f e') rtntypopt,tml',eqnl')
+ GCases (loc,sty,Option.map (f e') rtntypopt,tml',eqnl')
| ALetTuple (nal,(na,po),b,c) ->
let e',nal = list_fold_map g e nal in
let e'',na = g e na in
- RLetTuple (loc,nal,(na,Option.map (f e'') po),f e b,f e' c)
+ GLetTuple (loc,nal,(na,Option.map (f e'') po),f e b,f e' c)
| AIf (c,(na,po),b1,b2) ->
let e',na = g e na in
- RIf (loc,f e c,(na,Option.map (f e') po),f e b1,f e b2)
+ GIf (loc,f e c,(na,Option.map (f e') po),f e b1,f e b2)
| ARec (fk,idl,dll,tl,bl) ->
let e,dll = array_fold_map (list_fold_map (fun e (na,oc,b) ->
let e,na = g e na in
(e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
let e',idl = array_fold_map (to_id g) e idl in
- RRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl)
- | ACast (c,k) -> RCast (loc,f e c,
+ GRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl)
+ | ACast (c,k) -> GCast (loc,f e c,
match k with
| CastConv (k,t) -> CastConv (k,f e t)
| CastCoerce -> CastCoerce)
- | ASort x -> RSort (loc,x)
- | AHole x -> RHole (loc,x)
- | APatVar n -> RPatVar (loc,(false,n))
- | ARef x -> RRef (loc,x)
+ | ASort x -> GSort (loc,x)
+ | AHole x -> GHole (loc,x)
+ | APatVar n -> GPatVar (loc,(false,n))
+ | ARef x -> GRef (loc,x)
-let rec rawconstr_of_aconstr loc x =
+let rec glob_constr_of_aconstr loc x =
let rec aux () x =
- rawconstr_of_aconstr_with_binders loc (fun () id -> ((),id)) aux () x
+ glob_constr_of_aconstr_with_binders loc (fun () id -> ((),id)) aux () x
in aux () x
(****************************************************************************)
-(* Translating a rawconstr into a notation, interpreting recursive patterns *)
+(* Translating a glob_constr into a notation, interpreting recursive patterns *)
let add_id r id = r := (id :: pi1 !r, pi2 !r, pi3 !r)
let add_name r = function Anonymous -> () | Name id -> add_id r id
@@ -172,51 +170,51 @@ let add_name r = function Anonymous -> () | Name id -> add_id r id
let split_at_recursive_part c =
let sub = ref None in
let rec aux = function
- | RApp (loc0,RVar(loc,v),c::l) when v = ldots_var ->
+ | GApp (loc0,GVar(loc,v),c::l) when v = ldots_var ->
if !sub <> None then
(* Not narrowed enough to find only one recursive part *)
raise Not_found
else
(sub := Some c;
- if l = [] then RVar (loc,ldots_var)
- else RApp (loc0,RVar (loc,ldots_var),l))
- | c -> map_rawconstr aux c in
+ if l = [] then GVar (loc,ldots_var)
+ else GApp (loc0,GVar (loc,ldots_var),l))
+ | c -> map_glob_constr aux c in
let outer_iterator = aux c in
match !sub with
| None -> (* No recursive pattern found *) raise Not_found
| Some c ->
match outer_iterator with
- | RVar (_,v) when v = ldots_var -> (* Not enough context *) raise Not_found
+ | GVar (_,v) when v = ldots_var -> (* Not enough context *) raise Not_found
| _ -> outer_iterator, c
let on_true_do b f c = if b then (f c; b) else b
-let compare_rawconstr f add t1 t2 = match t1,t2 with
- | RRef (_,r1), RRef (_,r2) -> eq_gr r1 r2
- | RVar (_,v1), RVar (_,v2) -> on_true_do (v1 = v2) add (Name v1)
- | RApp (_,f1,l1), RApp (_,f2,l2) -> f f1 f2 & list_for_all2eq f l1 l2
- | RLambda (_,na1,bk1,ty1,c1), RLambda (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 -> on_true_do (f ty1 ty2 & f c1 c2) add na1
- | RProd (_,na1,bk1,ty1,c1), RProd (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 ->
+let compare_glob_constr f add t1 t2 = match t1,t2 with
+ | GRef (_,r1), GRef (_,r2) -> eq_gr r1 r2
+ | GVar (_,v1), GVar (_,v2) -> on_true_do (v1 = v2) add (Name v1)
+ | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 & list_for_all2eq f l1 l2
+ | GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 -> on_true_do (f ty1 ty2 & f c1 c2) add na1
+ | GProd (_,na1,bk1,ty1,c1), GProd (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 ->
on_true_do (f ty1 ty2 & f c1 c2) add na1
- | RHole _, RHole _ -> true
- | RSort (_,s1), RSort (_,s2) -> s1 = s2
- | RLetIn (_,na1,b1,c1), RLetIn (_,na2,b2,c2) when na1 = na2 ->
+ | GHole _, GHole _ -> true
+ | GSort (_,s1), GSort (_,s2) -> s1 = s2
+ | GLetIn (_,na1,b1,c1), GLetIn (_,na2,b2,c2) when na1 = na2 ->
on_true_do (f b1 b2 & f c1 c2) add na1
- | (RCases _ | RRec _ | RDynamic _
- | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _),_
- | _,(RCases _ | RRec _ | RDynamic _
- | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _)
+ | (GCases _ | GRec _
+ | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_
+ | _,(GCases _ | GRec _
+ | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _)
-> error "Unsupported construction in recursive notations."
- | (RRef _ | RVar _ | RApp _ | RLambda _ | RProd _
- | RHole _ | RSort _ | RLetIn _), _
+ | (GRef _ | GVar _ | GApp _ | GLambda _ | GProd _
+ | GHole _ | GSort _ | GLetIn _), _
-> false
-let rec eq_rawconstr t1 t2 = compare_rawconstr eq_rawconstr (fun _ -> ()) t1 t2
+let rec eq_glob_constr t1 t2 = compare_glob_constr eq_glob_constr (fun _ -> ()) t1 t2
let subtract_loc loc1 loc2 = make_loc (fst (unloc loc1),fst (unloc loc2)-1)
-let check_is_hole id = function RHole _ -> () | t ->
- user_err_loc (loc_of_rawconstr t,"",
+let check_is_hole id = function GHole _ -> () | t ->
+ user_err_loc (loc_of_glob_constr t,"",
strbrk "In recursive notation with binders, " ++ pr_id id ++
strbrk " is expected to come without type.")
@@ -224,40 +222,40 @@ let compare_recursive_parts found f (iterator,subc) =
let diff = ref None in
let terminator = ref None in
let rec aux c1 c2 = match c1,c2 with
- | RVar(_,v), term when v = ldots_var ->
+ | GVar(_,v), term when v = ldots_var ->
(* We found the pattern *)
assert (!terminator = None); terminator := Some term;
true
- | RApp (_,RVar(_,v),l1), RApp (_,term,l2) when v = ldots_var ->
+ | GApp (_,GVar(_,v),l1), GApp (_,term,l2) when v = ldots_var ->
(* We found the pattern, but there are extra arguments *)
(* (this allows e.g. alternative (recursive) notation of application) *)
assert (!terminator = None); terminator := Some term;
list_for_all2eq aux l1 l2
- | RVar (_,x), RVar (_,y) when x<>y ->
+ | GVar (_,x), GVar (_,y) when x<>y ->
(* We found the position where it differs *)
let lassoc = (!terminator <> None) in
let x,y = if lassoc then y,x else x,y in
!diff = None && (diff := Some (x,y,Some lassoc); true)
- | RLambda (_,Name x,_,t_x,c), RLambda (_,Name y,_,t_y,term)
- | RProd (_,Name x,_,t_x,c), RProd (_,Name y,_,t_y,term) ->
+ | GLambda (_,Name x,_,t_x,c), GLambda (_,Name y,_,t_y,term)
+ | GProd (_,Name x,_,t_x,c), GProd (_,Name y,_,t_y,term) ->
(* We found a binding position where it differs *)
check_is_hole y t_x;
check_is_hole y t_y;
!diff = None && (diff := Some (x,y,None); aux c term)
| _ ->
- compare_rawconstr aux (add_name found) c1 c2 in
+ compare_glob_constr aux (add_name found) c1 c2 in
if aux iterator subc then
match !diff with
| None ->
- let loc1 = loc_of_rawconstr iterator in
- let loc2 = loc_of_rawconstr (Option.get !terminator) in
+ let loc1 = loc_of_glob_constr iterator in
+ let loc2 = loc_of_glob_constr (Option.get !terminator) in
(* Here, we would need a loc made of several parts ... *)
user_err_loc (subtract_loc loc1 loc2,"",
str "Both ends of the recursive pattern are the same.")
| Some (x,y,Some lassoc) ->
let newfound = (pi1 !found, (x,y) :: pi2 !found, pi3 !found) in
let iterator =
- f (if lassoc then subst_rawvars [y,RVar(dummy_loc,x)] iterator
+ f (if lassoc then subst_glob_vars [y,GVar(dummy_loc,x)] iterator
else iterator) in
(* found have been collected by compare_constr *)
found := newfound;
@@ -271,7 +269,7 @@ let compare_recursive_parts found f (iterator,subc) =
else
raise Not_found
-let aconstr_and_vars_of_rawconstr a =
+let aconstr_and_vars_of_glob_constr a =
let found = ref ([],[],[]) in
let rec aux c =
let keepfound = !found in
@@ -280,7 +278,7 @@ let aconstr_and_vars_of_rawconstr a =
with Not_found ->
found := keepfound;
match c with
- | RApp (_,RVar (loc,f),[c]) when f = ldots_var ->
+ | GApp (_,GVar (loc,f),[c]) when f = ldots_var ->
(* Fall on the second part of the recursive pattern w/o having
found the first part *)
user_err_loc (loc,"",
@@ -288,12 +286,12 @@ let aconstr_and_vars_of_rawconstr a =
| c ->
aux' c
and aux' = function
- | RVar (_,id) -> add_id found id; AVar id
- | RApp (_,g,args) -> AApp (aux g, List.map aux args)
- | RLambda (_,na,bk,ty,c) -> add_name found na; ALambda (na,aux ty,aux c)
- | RProd (_,na,bk,ty,c) -> add_name found na; AProd (na,aux ty,aux c)
- | RLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c)
- | RCases (_,sty,rtntypopt,tml,eqnl) ->
+ | GVar (_,id) -> add_id found id; AVar id
+ | GApp (_,g,args) -> AApp (aux g, List.map aux args)
+ | GLambda (_,na,bk,ty,c) -> add_name found na; ALambda (na,aux ty,aux c)
+ | GProd (_,na,bk,ty,c) -> add_name found na; AProd (na,aux ty,aux c)
+ | GLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c)
+ | GCases (_,sty,rtntypopt,tml,eqnl) ->
let f (_,idl,pat,rhs) = List.iter (add_id found) idl; (pat,aux rhs) in
ACases (sty,Option.map aux rtntypopt,
List.map (fun (tm,(na,x)) ->
@@ -302,28 +300,28 @@ let aconstr_and_vars_of_rawconstr a =
(fun (_,_,_,nl) -> List.iter (add_name found) nl) x;
(aux tm,(na,Option.map (fun (_,ind,n,nal) -> (ind,n,nal)) x))) tml,
List.map f eqnl)
- | RLetTuple (loc,nal,(na,po),b,c) ->
+ | GLetTuple (loc,nal,(na,po),b,c) ->
add_name found na;
List.iter (add_name found) nal;
ALetTuple (nal,(na,Option.map aux po),aux b,aux c)
- | RIf (loc,c,(na,po),b1,b2) ->
+ | GIf (loc,c,(na,po),b1,b2) ->
add_name found na;
AIf (aux c,(na,Option.map aux po),aux b1,aux b2)
- | RRec (_,fk,idl,dll,tl,bl) ->
+ | GRec (_,fk,idl,dll,tl,bl) ->
Array.iter (add_id found) idl;
let dll = Array.map (List.map (fun (na,bk,oc,b) ->
if bk <> Explicit then
error "Binders marked as implicit not allowed in notations.";
add_name found na; (na,Option.map aux oc,aux b))) dll in
ARec (fk,idl,dll,Array.map aux tl,Array.map aux bl)
- | RCast (_,c,k) -> ACast (aux c,
+ | GCast (_,c,k) -> ACast (aux c,
match k with CastConv (k,t) -> CastConv (k,aux t)
| CastCoerce -> CastCoerce)
- | RSort (_,s) -> ASort s
- | RHole (_,w) -> AHole w
- | RRef (_,r) -> ARef r
- | RPatVar (_,(_,n)) -> APatVar n
- | RDynamic _ | REvar _ ->
+ | GSort (_,s) -> ASort s
+ | GHole (_,w) -> AHole w
+ | GRef (_,r) -> ARef r
+ | GPatVar (_,(_,n)) -> APatVar n
+ | GEvar _ ->
error "Existential variables not allowed in notations."
in
@@ -372,15 +370,15 @@ let check_variables vars recvars (found,foundrec,foundrecbinding) =
| NtnInternTypeIdent -> check_bound x in
List.iter check_type vars
-let aconstr_of_rawconstr vars recvars a =
- let a,found = aconstr_and_vars_of_rawconstr a in
+let aconstr_of_glob_constr vars recvars a =
+ let a,found = aconstr_and_vars_of_glob_constr a in
check_variables vars recvars found;
a
(* Substitution of kernel names, avoiding a list of bound identifiers *)
let aconstr_of_constr avoiding t =
- aconstr_of_rawconstr [] [] (Detyping.detype false avoiding [] t)
+ aconstr_of_glob_constr [] [] (Detyping.detype false avoiding [] t)
let rec subst_pat subst pat =
match pat with
@@ -510,9 +508,7 @@ let subst_interpretation subst (metas,pat) =
let bound = List.map fst metas in
(metas,subst_aconstr subst bound pat)
-let encode_list_value l = RApp (dummy_loc,RVar (dummy_loc,ldots_var),l)
-
-(* Pattern-matching rawconstr and aconstr *)
+(* Pattern-matching glob_constr and aconstr *)
let abstract_return_type_context pi mklam tml rtno =
Option.map (fun rtn ->
@@ -522,19 +518,14 @@ let abstract_return_type_context pi mklam tml rtno =
List.fold_right mklam nal rtn)
rtno
-let abstract_return_type_context_rawconstr =
+let abstract_return_type_context_glob_constr =
abstract_return_type_context (fun (_,_,_,nal) -> nal)
- (fun na c -> RLambda(dummy_loc,na,Explicit,RHole(dummy_loc,Evd.InternalHole),c))
+ (fun na c -> GLambda(dummy_loc,na,Explicit,GHole(dummy_loc,Evd.InternalHole),c))
let abstract_return_type_context_aconstr =
abstract_return_type_context pi3
(fun na c -> ALambda(na,AHole Evd.InternalHole,c))
-let rec adjust_scopes = function
- | _,[] -> []
- | [],a::args -> (None,a) :: adjust_scopes ([],args)
- | sc::scopes,a::args -> (sc,a) :: adjust_scopes (scopes,args)
-
exception No_match
let rec alpha_var id1 id2 = function
@@ -552,7 +543,7 @@ let bind_env alp (sigma,sigmalist,sigmabinders as fullsigma) var v =
else raise No_match
with Not_found ->
(* Check that no capture of binding variables occur *)
- if List.exists (fun (id,_) ->occur_rawconstr id v) alp then raise No_match;
+ if List.exists (fun (id,_) ->occur_glob_constr id v) alp then raise No_match;
(* TODO: handle the case of multiple occs in different scopes *)
((var,v)::sigma,sigmalist,sigmabinders)
@@ -561,8 +552,8 @@ let bind_binder (sigma,sigmalist,sigmabinders) x bl =
let match_fix_kind fk1 fk2 =
match (fk1,fk2) with
- | RCoFix n1, RCoFix n2 -> n1 = n2
- | RFix (nl1,n1), RFix (nl2,n2) ->
+ | GCoFix n1, GCoFix n2 -> n1 = n2
+ | GFix (nl1,n1), GFix (nl2,n2) ->
n1 = n2 &&
array_for_all2 (fun (n1,_) (n2,_) -> n2 = None || n1 = n2) nl1 nl2
| _ -> false
@@ -574,7 +565,7 @@ let match_opt f sigma t1 t2 = match (t1,t2) with
let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
| (Name id1,Name id2) when List.mem id2 (fst metas) ->
- alp, bind_env alp sigma id2 (RVar (dummy_loc,id1))
+ alp, bind_env alp sigma id2 (GVar (dummy_loc,id1))
| (Name id1,Name id2) -> (id1,id2)::alp,sigma
| (Anonymous,Anonymous) -> alp,sigma
| _ -> raise No_match
@@ -588,20 +579,16 @@ let rec match_cases_pattern_binders metas acc pat1 pat2 =
(match_names metas acc na1 na2) patl1 patl2
| _ -> raise No_match
-let adjust_application_n n loc f l =
- let l1,l2 = list_chop (List.length l - n) l in
- if l1 = [] then f,l else RApp (loc,f,l1), l2
-
let glue_letin_with_decls = true
let rec match_iterated_binders islambda decls = function
- | RLambda (_,na,bk,t,b) when islambda ->
+ | GLambda (_,na,bk,t,b) when islambda ->
match_iterated_binders islambda ((na,bk,None,t)::decls) b
- | RProd (_,(Name _ as na),bk,t,b) when not islambda ->
+ | GProd (_,(Name _ as na),bk,t,b) when not islambda ->
match_iterated_binders islambda ((na,bk,None,t)::decls) b
- | RLetIn (loc,na,c,b) when glue_letin_with_decls ->
+ | GLetIn (loc,na,c,b) when glue_letin_with_decls ->
match_iterated_binders islambda
- ((na,Explicit (*?*), Some c,RHole(loc,Evd.BinderType na))::decls) b
+ ((na,Explicit (*?*), Some c,GHole(loc,Evd.BinderType na))::decls) b
| b -> (decls,b)
let remove_sigma x (sigmavar,sigmalist,sigmabinders) =
@@ -633,125 +620,157 @@ let match_alist match_fun metas sigma rest x iter termin lassoc =
let l,sigma = aux sigma [] rest in
(pi1 sigma, (x,if lassoc then l else List.rev l)::pi2 sigma, pi3 sigma)
-let rec match_ alp (tmetas,blmetas as metas) sigma a1 a2 = match (a1,a2) with
+let does_not_come_from_already_eta_expanded_var =
+ (* This is hack to avoid looping on a rule with rhs of the form *)
+ (* "?f (fun ?x => ?g)" since otherwise, matching "F H" expands in *)
+ (* "F (fun x => H x)" and "H x" is recursively matched against the same *)
+ (* rule, giving "H (fun x' => x x')" and so on. *)
+ (* Ideally, we would need the type of the expression to know which of *)
+ (* the arguments applied to it can be eta-expanded without looping. *)
+ (* The following test is then an approximation of what can be done *)
+ (* optimally (whether other looping situations can occur remains to be *)
+ (* checked). *)
+ function GVar _ -> false | _ -> true
+
+let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
+ match (a1,a2) with
(* Matching notation variable *)
| r1, AVar id2 when List.mem id2 tmetas -> bind_env alp sigma id2 r1
(* Matching recursive notations for terms *)
| r1, AList (x,_,iter,termin,lassoc) ->
- match_alist (match_ alp) metas sigma r1 x iter termin lassoc
+ match_alist (match_hd u alp) metas sigma r1 x iter termin lassoc
(* Matching recursive notations for binders: ad hoc cases supporting let-in *)
- | RLambda (_,na1,bk,t1,b1), ABinderList (x,_,ALambda (Name id2,_,b2),termin)->
+ | GLambda (_,na1,bk,t1,b1), ABinderList (x,_,ALambda (Name id2,_,b2),termin)->
let (decls,b) = match_iterated_binders true [(na1,bk,None,t1)] b1 in
(* TODO: address the possibility that termin is a Lambda itself *)
- match_ alp metas (bind_binder sigma x decls) b termin
- | RProd (_,na1,bk,t1,b1), ABinderList (x,_,AProd (Name id2,_,b2),termin)
+ match_in u alp metas (bind_binder sigma x decls) b termin
+ | GProd (_,na1,bk,t1,b1), ABinderList (x,_,AProd (Name id2,_,b2),termin)
when na1 <> Anonymous ->
let (decls,b) = match_iterated_binders false [(na1,bk,None,t1)] b1 in
(* TODO: address the possibility that termin is a Prod itself *)
- match_ alp metas (bind_binder sigma x decls) b termin
+ match_in u alp metas (bind_binder sigma x decls) b termin
(* Matching recursive notations for binders: general case *)
| r, ABinderList (x,_,iter,termin) ->
- match_abinderlist_with_app (match_ alp) metas sigma r x iter termin
+ match_abinderlist_with_app (match_hd u alp) metas sigma r x iter termin
(* Matching individual binders as part of a recursive pattern *)
- | RLambda (_,na,bk,t,b1), ALambda (Name id,_,b2) when List.mem id blmetas ->
- match_ alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2
- | RProd (_,na,bk,t,b1), AProd (Name id,_,b2)
+ | GLambda (_,na,bk,t,b1), ALambda (Name id,_,b2) when List.mem id blmetas ->
+ match_in u alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2
+ | GProd (_,na,bk,t,b1), AProd (Name id,_,b2)
when List.mem id blmetas & na <> Anonymous ->
- match_ alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2
+ match_in u alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2
(* Matching compositionally *)
- | RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma
- | RRef (_,r1), ARef r2 when (eq_gr r1 r2) -> sigma
- | RPatVar (_,(_,n1)), APatVar n2 when n1=n2 -> sigma
- | RApp (loc,f1,l1), AApp (f2,l2) ->
+ | GVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma
+ | GRef (_,r1), ARef r2 when (eq_gr r1 r2) -> sigma
+ | GPatVar (_,(_,n1)), APatVar n2 when n1=n2 -> sigma
+ | GApp (loc,f1,l1), AApp (f2,l2) ->
let n1 = List.length l1 and n2 = List.length l2 in
let f1,l1,f2,l2 =
if n1 < n2 then
let l21,l22 = list_chop (n2-n1) l2 in f1,l1, AApp (f2,l21), l22
else if n1 > n2 then
- let l11,l12 = list_chop (n1-n2) l1 in RApp (loc,f1,l11),l12, f2,l2
+ let l11,l12 = list_chop (n1-n2) l1 in GApp (loc,f1,l11),l12, f2,l2
else f1,l1, f2, l2 in
- List.fold_left2 (match_ alp metas) (match_ alp metas sigma f1 f2) l1 l2
- | RLambda (_,na1,_,t1,b1), ALambda (na2,t2,b2) ->
- match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2
- | RProd (_,na1,_,t1,b1), AProd (na2,t2,b2) ->
- match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2
- | RLetIn (_,na1,t1,b1), ALetIn (na2,t2,b2) ->
- match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2
- | RCases (_,sty1,rtno1,tml1,eqnl1), ACases (sty2,rtno2,tml2,eqnl2)
+ let may_use_eta = does_not_come_from_already_eta_expanded_var f1 in
+ List.fold_left2 (match_ may_use_eta u alp metas)
+ (match_in u alp metas sigma f1 f2) l1 l2
+ | GLambda (_,na1,_,t1,b1), ALambda (na2,t2,b2) ->
+ match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2
+ | GProd (_,na1,_,t1,b1), AProd (na2,t2,b2) ->
+ match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2
+ | GLetIn (_,na1,t1,b1), ALetIn (na2,t2,b2) ->
+ match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2
+ | GCases (_,sty1,rtno1,tml1,eqnl1), ACases (sty2,rtno2,tml2,eqnl2)
when sty1 = sty2
& List.length tml1 = List.length tml2
& List.length eqnl1 = List.length eqnl2 ->
- let rtno1' = abstract_return_type_context_rawconstr tml1 rtno1 in
+ let rtno1' = abstract_return_type_context_glob_constr tml1 rtno1 in
let rtno2' = abstract_return_type_context_aconstr tml2 rtno2 in
let sigma =
- try Option.fold_left2 (match_ alp metas) sigma rtno1' rtno2'
+ try Option.fold_left2 (match_in u alp metas) sigma rtno1' rtno2'
with Option.Heterogeneous -> raise No_match
in
let sigma = List.fold_left2
- (fun s (tm1,_) (tm2,_) -> match_ alp metas s tm1 tm2) sigma tml1 tml2 in
- List.fold_left2 (match_equations alp metas) sigma eqnl1 eqnl2
- | RLetTuple (_,nal1,(na1,to1),b1,c1), ALetTuple (nal2,(na2,to2),b2,c2)
+ (fun s (tm1,_) (tm2,_) ->
+ match_in u alp metas s tm1 tm2) sigma tml1 tml2 in
+ List.fold_left2 (match_equations u alp metas) sigma eqnl1 eqnl2
+ | GLetTuple (_,nal1,(na1,to1),b1,c1), ALetTuple (nal2,(na2,to2),b2,c2)
when List.length nal1 = List.length nal2 ->
- let sigma = match_opt (match_binders alp metas na1 na2) sigma to1 to2 in
- let sigma = match_ alp metas sigma b1 b2 in
+ let sigma = match_opt (match_binders u alp metas na1 na2) sigma to1 to2 in
+ let sigma = match_in u alp metas sigma b1 b2 in
let (alp,sigma) =
List.fold_left2 (match_names metas) (alp,sigma) nal1 nal2 in
- match_ alp metas sigma c1 c2
- | RIf (_,a1,(na1,to1),b1,c1), AIf (a2,(na2,to2),b2,c2) ->
- let sigma = match_opt (match_binders alp metas na1 na2) sigma to1 to2 in
- List.fold_left2 (match_ alp metas) sigma [a1;b1;c1] [a2;b2;c2]
- | RRec (_,fk1,idl1,dll1,tl1,bl1), ARec (fk2,idl2,dll2,tl2,bl2)
+ match_in u alp metas sigma c1 c2
+ | GIf (_,a1,(na1,to1),b1,c1), AIf (a2,(na2,to2),b2,c2) ->
+ let sigma = match_opt (match_binders u alp metas na1 na2) sigma to1 to2 in
+ List.fold_left2 (match_in u alp metas) sigma [a1;b1;c1] [a2;b2;c2]
+ | GRec (_,fk1,idl1,dll1,tl1,bl1), ARec (fk2,idl2,dll2,tl2,bl2)
when match_fix_kind fk1 fk2 & Array.length idl1 = Array.length idl2 &
array_for_all2 (fun l1 l2 -> List.length l1 = List.length l2) dll1 dll2
->
let alp,sigma = array_fold_left2
(List.fold_left2 (fun (alp,sigma) (na1,_,oc1,b1) (na2,oc2,b2) ->
let sigma =
- match_ alp metas (match_opt (match_ alp metas) sigma oc1 oc2) b1 b2
+ match_in u alp metas
+ (match_opt (match_in u alp metas) sigma oc1 oc2) b1 b2
in match_names metas (alp,sigma) na1 na2)) (alp,sigma) dll1 dll2 in
- let sigma = array_fold_left2 (match_ alp metas) sigma tl1 tl2 in
+ let sigma = array_fold_left2 (match_in u alp metas) sigma tl1 tl2 in
let alp,sigma = array_fold_right2 (fun id1 id2 alsig ->
match_names metas alsig (Name id1) (Name id2)) idl1 idl2 (alp,sigma) in
- array_fold_left2 (match_ alp metas) sigma bl1 bl2
- | RCast(_,c1, CastConv(_,t1)), ACast(c2, CastConv (_,t2)) ->
- match_ alp metas (match_ alp metas sigma c1 c2) t1 t2
- | RCast(_,c1, CastCoerce), ACast(c2, CastCoerce) ->
- match_ alp metas sigma c1 c2
- | RSort (_,RType _), ASort (RType None) -> sigma
- | RSort (_,s1), ASort s2 when s1 = s2 -> sigma
- | RPatVar _, AHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
+ array_fold_left2 (match_in u alp metas) sigma bl1 bl2
+ | GCast(_,c1, CastConv(_,t1)), ACast(c2, CastConv (_,t2)) ->
+ match_in u alp metas (match_in u alp metas sigma c1 c2) t1 t2
+ | GCast(_,c1, CastCoerce), ACast(c2, CastCoerce) ->
+ match_in u alp metas sigma c1 c2
+ | GSort (_,GType _), ASort (GType None) when not u -> sigma
+ | GSort (_,s1), ASort s2 when s1 = s2 -> sigma
+ | GPatVar _, AHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
| a, AHole _ -> sigma
- | (RDynamic _ | RRec _ | REvar _), _
+
+ (* On the fly eta-expansion so as to use notations of the form
+ "exists x, P x" for "ex P"; expects type not given because don't know
+ otherwise how to ensure it corresponds to a well-typed eta-expansion;
+ ensure at least one constructor is consumed to avoid looping *)
+ | b1, ALambda (Name id,AHole _,b2) when inner ->
+ let id' = Namegen.next_ident_away id (free_glob_vars b1) in
+ match_in u alp metas (bind_binder sigma id
+ [(Name id',Explicit,None,GHole(dummy_loc,Evd.BinderType (Name id')))])
+ (mkGApp dummy_loc b1 (GVar (dummy_loc,id'))) b2
+
+ | (GRec _ | GEvar _), _
| _,_ -> raise No_match
-and match_binders alp metas na1 na2 sigma b1 b2 =
+and match_in u = match_ true u
+
+and match_hd u = match_ false u
+
+and match_binders u alp metas na1 na2 sigma b1 b2 =
let (alp,sigma) = match_names metas (alp,sigma) na1 na2 in
- match_ alp metas sigma b1 b2
+ match_in u alp metas sigma b1 b2
-and match_equations alp metas sigma (_,_,patl1,rhs1) (patl2,rhs2) =
+and match_equations u alp metas sigma (_,_,patl1,rhs1) (patl2,rhs2) =
(* patl1 and patl2 have the same length because they respectively
correspond to some tml1 and tml2 that have the same length *)
let (alp,sigma) =
List.fold_left2 (match_cases_pattern_binders metas)
(alp,sigma) patl1 patl2 in
- match_ alp metas sigma rhs1 rhs2
+ match_in u alp metas sigma rhs1 rhs2
-let match_aconstr c (metas,pat) =
+let match_aconstr u c (metas,pat) =
let vars = list_split_by (fun (_,(_,x)) -> x <> NtnTypeBinderList) metas in
let vars = (List.map fst (fst vars), List.map fst (snd vars)) in
- let terms,termlists,binders = match_ [] vars ([],[],[]) c pat in
+ let terms,termlists,binders = match_ false u [] vars ([],[],[]) c pat in
(* Reorder canonically the substitution *)
let find x =
try List.assoc x terms
with Not_found ->
(* Happens for binders bound to Anonymous *)
(* Find a better way to propagate Anonymous... *)
- RVar (dummy_loc,x) in
+ GVar (dummy_loc,x) in
List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders') ->
match typ with
| NtnTypeConstr ->
@@ -824,6 +843,7 @@ type prim_token = Numeral of Bigint.bigint | String of string
type cases_pattern_expr =
| CPatAlias of loc * cases_pattern_expr * identifier
| CPatCstr of loc * reference * cases_pattern_expr list
+ | CPatCstrExpl of loc * reference * cases_pattern_expr list
| CPatAtom of loc * reference option
| CPatOr of loc * cases_pattern_expr list
| CPatNotation of loc * notation * cases_pattern_notation_substitution
@@ -857,13 +877,12 @@ type constr_expr =
| CHole of loc * Evd.hole_kind option
| CPatVar of loc * (bool * patvar)
| CEvar of loc * existential_key * constr_expr list option
- | CSort of loc * rawsort
+ | CSort of loc * glob_sort
| CCast of loc * constr_expr * constr_expr cast_type
| CNotation of loc * notation * constr_notation_substitution
| CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr
| CPrim of loc * prim_token
| CDelimiters of loc * string * constr_expr
- | CDynamic of loc * Dyn.t
and fix_expr =
identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
@@ -929,11 +948,11 @@ let constr_loc = function
| CGeneralization (loc,_,_,_) -> loc
| CPrim (loc,_) -> loc
| CDelimiters (loc,_,_) -> loc
- | CDynamic _ -> dummy_loc
let cases_pattern_expr_loc = function
| CPatAlias (loc,_,_) -> loc
| CPatCstr (loc,_,_) -> loc
+ | CPatCstrExpl (loc,_,_) -> loc
| CPatAtom (loc,_) -> loc
| CPatOr (loc,_) -> loc
| CPatNotation (loc,_,_) -> loc
@@ -950,10 +969,6 @@ let local_binders_loc bll =
if bll = [] then dummy_loc else
join_loc (local_binder_loc (List.hd bll)) (local_binder_loc (list_last bll))
-let occur_var_constr_ref id = function
- | Ident (loc,id') -> id = id'
- | Qualid _ -> false
-
let ids_of_cases_indtype =
let add_var ids = function CRef (Ident (_,id)) -> id::ids | _ -> ids in
let rec vars_of = function
@@ -981,7 +996,7 @@ let rec cases_pattern_fold_names f a = function
| CPatRecord (_, l) ->
List.fold_left (fun acc (r, cp) -> cases_pattern_fold_names f acc cp) a l
| CPatAlias (_,pat,id) -> f id a
- | CPatCstr (_,_,patl) | CPatOr (_,patl) ->
+ | CPatCstr (_,_,patl) | CPatCstrExpl (_,_,patl) | CPatOr (_,patl) ->
List.fold_left (cases_pattern_fold_names f) a patl
| CPatNotation (_,_,(patl,patll)) ->
List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)
@@ -1028,7 +1043,7 @@ let fold_constr_expr_with_binders g f n acc = function
List.fold_left (fun acc bl -> fold_local_binders g f n acc (CHole (dummy_loc,None)) bl) acc bll
| CGeneralization (_,_,_,c) -> f n acc c
| CDelimiters (loc,_,a) -> f n acc a
- | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _ | CRef _ ->
+ | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CRef _ ->
acc
| CRecord (loc,_,l) -> List.fold_left (fun acc (id, c) -> f n acc c) acc l
| CCases (loc,sty,rtnpo,al,bl) ->
@@ -1137,9 +1152,9 @@ let split_at_annot bl na =
let rec aux acc = function
| LocalRawAssum (bls, k, t) as x :: rest ->
let l, r = list_split_when (fun (loc, na) -> na = Name id) bls in
- if r = [] then aux (x :: acc) rest
- else
- (List.rev (if l = [] then acc else LocalRawAssum (l, k, t) :: acc),
+ if r = [] then aux (x :: acc) rest
+ else
+ (List.rev (if l = [] then acc else LocalRawAssum (l, k, t) :: acc),
LocalRawAssum (r, k, t) :: rest)
| LocalRawDef _ as x :: rest -> aux (x :: acc) rest
| [] ->
@@ -1186,7 +1201,7 @@ let map_constr_expr_with_binders g f e = function
| CGeneralization (loc,b,a,c) -> CGeneralization (loc,b,a,f e c)
| CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a)
| CHole _ | CEvar _ | CPatVar _ | CSort _
- | CPrim _ | CDynamic _ | CRef _ as x -> x
+ | CPrim _ | CRef _ as x -> x
| CRecord (loc,p,l) -> CRecord (loc,p,List.map (fun (id, c) -> (id, f e c)) l)
| CCases (loc,sty,rtnpo,a,bl) ->
(* TODO: apply g on the binding variables in pat... *)
@@ -1233,14 +1248,8 @@ type with_declaration_ast =
type module_ast =
| CMident of qualid located
- | CMapply of module_ast * module_ast
- | CMwith of module_ast * with_declaration_ast
-
-type module_ast_inl = module_ast * bool (* honor the inline annotations or not *)
-
-type 'a module_signature =
- | Enforce of 'a (* ... : T *)
- | Check of 'a list (* ... <: T1 <: T2, possibly empty *)
+ | CMapply of loc * module_ast * module_ast
+ | CMwith of loc * module_ast * with_declaration_ast
(* Returns the ranges of locs of the notation that are not occupied by args *)
(* and which are then occupied by proper symbols of the notation (or spaces) *)
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index ce9de27b..4527dc48 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -1,35 +1,34 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: topconstr.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
open Pp
open Util
open Names
open Libnames
-open Rawterm
+open Glob_term
open Term
open Mod_subst
-(*i*)
-(*s This is the subtype of rawconstr allowed in syntactic extensions *)
-(* No location since intended to be substituted at any place of a text *)
-(* Complex expressions such as fixpoints and cofixpoints are excluded, *)
-(* non global expressions such as existential variables also *)
+(** Topconstr: definitions of [aconstr] et [constr_expr] *)
+
+(** {6 aconstr } *)
+(** This is the subtype of glob_constr allowed in syntactic extensions
+ No location since intended to be substituted at any place of a text
+ Complex expressions such as fixpoints and cofixpoints are excluded,
+ non global expressions such as existential variables also *)
type aconstr =
- (* Part common to [rawconstr] and [cases_pattern] *)
+ (** Part common to [glob_constr] and [cases_pattern] *)
| ARef of global_reference
| AVar of identifier
| AApp of aconstr * aconstr list
| AList of identifier * identifier * aconstr * aconstr * bool
- (* Part only in [rawconstr] *)
+ (** Part only in [glob_constr] *)
| ALambda of name * aconstr * aconstr
| AProd of name * aconstr * aconstr
| ABinderList of identifier * identifier * aconstr * aconstr
@@ -42,7 +41,7 @@ type aconstr =
| ARec of fix_kind * identifier array *
(name * aconstr option * aconstr) list array * aconstr array *
aconstr array
- | ASort of rawsort
+ | ASort of glob_sort
| AHole of Evd.hole_kind
| APatVar of patvar
| ACast of aconstr * aconstr cast_type
@@ -68,49 +67,44 @@ type notation_var_internalization_type =
type interpretation =
(identifier * (subscopes * notation_var_instance_type)) list * aconstr
-(**********************************************************************)
-(* Translate a rawconstr into a notation given the list of variables *)
-(* bound by the notation; also interpret recursive patterns *)
+(** Translate a glob_constr into a notation given the list of variables
+ bound by the notation; also interpret recursive patterns *)
-val aconstr_of_rawconstr :
+val aconstr_of_glob_constr :
(identifier * notation_var_internalization_type) list ->
- (identifier * identifier) list -> rawconstr -> aconstr
+ (identifier * identifier) list -> glob_constr -> aconstr
-(* Name of the special identifier used to encode recursive notations *)
+(** Name of the special identifier used to encode recursive notations *)
val ldots_var : identifier
-(* Equality of rawconstr (warning: only partially implemented) *)
-val eq_rawconstr : rawconstr -> rawconstr -> bool
+(** Equality of glob_constr (warning: only partially implemented) *)
+val eq_glob_constr : glob_constr -> glob_constr -> bool
-(**********************************************************************)
-(* Re-interpret a notation as a rawconstr, taking care of binders *)
+(** Re-interpret a notation as a glob_constr, taking care of binders *)
-val rawconstr_of_aconstr_with_binders : loc ->
+val glob_constr_of_aconstr_with_binders : loc ->
('a -> name -> 'a * name) ->
- ('a -> aconstr -> rawconstr) -> 'a -> aconstr -> rawconstr
+ ('a -> aconstr -> glob_constr) -> 'a -> aconstr -> glob_constr
-val rawconstr_of_aconstr : loc -> aconstr -> rawconstr
+val glob_constr_of_aconstr : loc -> aconstr -> glob_constr
-(**********************************************************************)
-(* [match_aconstr] matches a rawconstr against a notation *)
-(* interpretation raise [No_match] if the matching fails *)
+(** [match_aconstr] matches a glob_constr against a notation interpretation;
+ raise [No_match] if the matching fails *)
exception No_match
-val match_aconstr : rawconstr -> interpretation ->
- (rawconstr * subscopes) list * (rawconstr list * subscopes) list *
- (rawdecl list * subscopes) list
+val match_aconstr : bool -> glob_constr -> interpretation ->
+ (glob_constr * subscopes) list * (glob_constr list * subscopes) list *
+ (glob_decl list * subscopes) list
val match_aconstr_cases_pattern : cases_pattern -> interpretation ->
(cases_pattern * subscopes) list * (cases_pattern list * subscopes) list
-(**********************************************************************)
-(* Substitution of kernel names in interpretation data *)
+(** Substitution of kernel names in interpretation data *)
val subst_interpretation : substitution -> interpretation -> interpretation
-(**********************************************************************)
-(*s Concrete syntax for terms *)
+(** {6 Concrete syntax for terms } *)
type notation = string
@@ -119,18 +113,19 @@ type explicitation = ExplByPos of int * identifier option | ExplByName of identi
type binder_kind =
| Default of binding_kind
| Generalized of binding_kind * binding_kind * bool
- (* Inner binding, outer bindings, typeclass-specific flag
+ (** Inner binding, outer bindings, typeclass-specific flag
for implicit generalization of superclasses *)
type abstraction_kind = AbsLambda | AbsPi
-type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
+type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
type prim_token = Numeral of Bigint.bigint | String of string
type cases_pattern_expr =
| CPatAlias of loc * cases_pattern_expr * identifier
| CPatCstr of loc * reference * cases_pattern_expr list
+ | CPatCstrExpl of loc * reference * cases_pattern_expr list
| CPatAtom of loc * reference option
| CPatOr of loc * cases_pattern_expr list
| CPatNotation of loc * notation * cases_pattern_notation_substitution
@@ -164,13 +159,12 @@ type constr_expr =
| CHole of loc * Evd.hole_kind option
| CPatVar of loc * (bool * patvar)
| CEvar of loc * existential_key * constr_expr list option
- | CSort of loc * rawsort
+ | CSort of loc * glob_sort
| CCast of loc * constr_expr * constr_expr cast_type
| CNotation of loc * notation * constr_notation_substitution
| CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr
| CPrim of loc * prim_token
| CDelimiters of loc * string * constr_expr
- | CDynamic of loc * Dyn.t
and fix_expr =
identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
@@ -181,7 +175,7 @@ and cofix_expr =
and recursion_order_expr =
| CStructRec
| CWfRec of constr_expr
- | CMeasureRec of constr_expr * constr_expr option (* measure, relation *)
+ | CMeasureRec of constr_expr * constr_expr option (** measure, relation *)
(** Anonymous defs allowed ?? *)
and local_binder =
@@ -199,8 +193,7 @@ and typeclass_context = typeclass_constraint list
type constr_pattern_expr = constr_expr
-(**********************************************************************)
-(* Utilities on constr_expr *)
+(** Utilities on constr_expr *)
val constr_loc : constr_expr -> loc
@@ -216,7 +209,7 @@ val occur_var_constr_expr : identifier -> constr_expr -> bool
val default_binder_kind : binder_kind
-(* Specific function for interning "in indtype" syntax of "match" *)
+(** Specific function for interning "in indtype" syntax of "match" *)
val ids_of_cases_indtype : constr_expr -> identifier list
val mkIdentC : identifier -> constr_expr
@@ -236,32 +229,31 @@ val split_at_annot : local_binder list -> identifier located option -> local_bin
val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
-(* Same as [abstract_constr_expr] and [prod_constr_expr], with location *)
+(** Same as [abstract_constr_expr] and [prod_constr_expr], with location *)
val mkCLambdaN : loc -> local_binder list -> constr_expr -> constr_expr
val mkCProdN : loc -> local_binder list -> constr_expr -> constr_expr
-(* For binders parsing *)
+(** For binders parsing *)
-(* With let binders *)
+(** With let binders *)
val names_of_local_binders : local_binder list -> name located list
-(* Does not take let binders into account *)
+(** Does not take let binders into account *)
val names_of_local_assums : local_binder list -> name located list
-(* Used in typeclasses *)
+(** Used in typeclasses *)
val fold_constr_expr_with_binders : (identifier -> 'a -> 'a) ->
('a -> 'b -> constr_expr -> 'b) -> 'a -> 'b -> constr_expr -> 'b
-(* Used in correctness and interface; absence of var capture not guaranteed *)
-(* in pattern-matching clauses and in binders of the form [x,y:T(x)] *)
+(** Used in correctness and interface; absence of var capture not guaranteed
+ in pattern-matching clauses and in binders of the form [x,y:T(x)] *)
val map_constr_expr_with_binders :
(identifier -> 'a -> 'a) -> ('a -> constr_expr -> constr_expr) ->
'a -> constr_expr -> constr_expr
-(**********************************************************************)
-(* Concrete syntax for modules and module types *)
+(** Concrete syntax for modules and module types *)
type with_declaration_ast =
| CWith_Module of identifier list located * qualid located
@@ -269,14 +261,8 @@ type with_declaration_ast =
type module_ast =
| CMident of qualid located
- | CMapply of module_ast * module_ast
- | CMwith of module_ast * with_declaration_ast
-
-type module_ast_inl = module_ast * bool (* honor the inline annotations or not *)
-
-type 'a module_signature =
- | Enforce of 'a (* ... : T *)
- | Check of 'a list (* ... <: T1 <: T2, possibly empty *)
+ | CMapply of loc * module_ast * module_ast
+ | CMwith of loc * module_ast * with_declaration_ast
val ntn_loc :
Util.loc -> constr_notation_substitution -> string -> (int * int) list
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-01 13:45:01 +0000