summaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /interp
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml328
-rw-r--r--interp/constrextern.mli6
-rw-r--r--interp/constrintern.ml776
-rw-r--r--interp/constrintern.mli106
-rw-r--r--interp/coqlib.ml202
-rw-r--r--interp/coqlib.mli48
-rw-r--r--interp/dumpglob.ml114
-rw-r--r--interp/dumpglob.mli10
-rw-r--r--interp/genarg.ml23
-rw-r--r--interp/genarg.mli52
-rw-r--r--interp/implicit_quantifiers.ml220
-rw-r--r--interp/implicit_quantifiers.mli14
-rw-r--r--interp/interp.mllib18
-rw-r--r--interp/modintern.ml68
-rw-r--r--interp/modintern.mli13
-rw-r--r--interp/notation.ml171
-rw-r--r--interp/notation.mli34
-rw-r--r--interp/ppextend.ml4
-rw-r--r--interp/ppextend.mli4
-rw-r--r--interp/reserve.ml18
-rw-r--r--interp/reserve.mli2
-rw-r--r--interp/smartlocate.ml64
-rw-r--r--interp/smartlocate.mli37
-rw-r--r--interp/syntax_def.ml68
-rw-r--r--interp/syntax_def.mli21
-rw-r--r--interp/topconstr.ml388
-rw-r--r--interp/topconstr.mli80
27 files changed, 1733 insertions, 1156 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 99bcf159..e61dffeb 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: constrextern.ml 12495 2009-11-11 12:10:44Z herbelin $ *)
+(* $Id$ *)
(*i*)
open Pp
@@ -16,6 +16,7 @@ open Names
open Nameops
open Term
open Termops
+open Namegen
open Inductive
open Sign
open Environ
@@ -92,19 +93,6 @@ let insert_pat_alias loc p = function
(**********************************************************************)
(* conversion of references *)
-let ids_of_ctxt ctxt =
- Array.to_list
- (Array.map
- (function c -> match kind_of_term c with
- | Var id -> id
- | _ ->
- error "Arbitrary substitution of references not implemented.")
- ctxt)
-
-let idopt_of_name = function
- | Name id -> Some id
- | Anonymous -> None
-
let extern_evar loc n l =
if !print_evar_arguments then CEvar (loc,n,l) else CEvar (loc,n,None)
@@ -279,8 +267,8 @@ let rec same_raw c d =
| 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 =
+
+let same_rawconstr c d =
try same_raw c d; true
with Failure _ | Invalid_argument _ -> false
@@ -305,12 +293,12 @@ let expand_curly_brackets loc mknot ntn (l,ll) =
function
| [] -> []
| a::l ->
- let a' =
+ let a' =
let p = List.nth (wildcards !ntn' 0) i - 2 in
if p>=0 & p+5 <= String.length !ntn' & String.sub !ntn' p 5 = "{ _ }"
then begin
- ntn' :=
- String.sub !ntn' 0 p ^ "_" ^
+ ntn' :=
+ String.sub !ntn' 0 p ^ "_" ^
String.sub !ntn' (p+5) (String.length !ntn' -p-5);
mknot (loc,"{ _ }",([a],[])) end
else a in
@@ -329,7 +317,7 @@ let make_notation_gen loc ntn mknot mkprim destprim l =
(* Special case to avoid writing "- 3" for e.g. (Zopp 3) *)
| "- _", [Some (Numeral p)],[] when Bigint.is_strictly_pos p ->
mknot (loc,ntn,([mknot (loc,"( _ )",l)],[]))
- | _ ->
+ | _ ->
match decompose_notation_key ntn, l with
| [Terminal "-"; Terminal x], ([],[]) ->
(try mkprim (loc, Numeral (Bigint.neg (Bigint.of_string x)))
@@ -352,80 +340,72 @@ let make_pat_notation loc ntn l =
(fun (loc,p) -> CPatPrim (loc,p))
destPatPrim l
-let bind_env (sigma,sigmalist as fullsigma) var v =
- try
- let vvar = List.assoc var sigma in
- if v=vvar then fullsigma else raise No_match
- with Not_found ->
- (* TODO: handle the case of multiple occs in different scopes *)
- (var,v)::sigma,sigmalist
-
-let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with
- | r1, AVar id2 when List.mem id2 metas -> bind_env sigma id2 r1
- | PatVar (_,Anonymous), AHole _ -> sigma
- | PatCstr (loc,(ind,_ as r1),args1,_), _ ->
- let nparams =
- (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
- let l2 =
- match a2 with
- | ARef (ConstructRef r2) when r1 = r2 -> []
- | AApp (ARef (ConstructRef r2),l2) when r1 = r2 -> l2
- | _ -> raise No_match in
- if List.length l2 <> nparams + List.length args1
- then raise No_match
- else
- let (p2,args2) = list_chop nparams l2 in
- (* All parameters must be _ *)
- List.iter (function AHole _ -> () | _ -> raise No_match) p2;
- List.fold_left2 (match_cases_pattern metas) sigma args1 args2
- (* TODO: use recursive notations *)
- | _ -> raise No_match
-
-let match_aconstr_cases_pattern c ((metas_scl,metaslist_scl),pat) =
- let vars = List.map fst metas_scl @ List.map fst metaslist_scl in
- let subst,substlist = match_cases_pattern vars ([],[]) c pat in
- (* Reorder canonically the substitution *)
- let find x subst =
- try List.assoc x subst
- with Not_found -> anomaly "match_aconstr_cases_pattern" in
- List.map (fun (x,scl) -> (find x subst,scl)) metas_scl,
- List.map (fun (x,scl) -> (find x substlist,scl)) metaslist_scl
-
(* Better to use extern_rawconstr composed with injection/retraction ?? *)
let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
- try
+ try
if !Flags.raw_print or !print_no_symbol then raise No_match;
let (na,sc,p) = uninterp_prim_token_cases_pattern pat in
- match availability_of_prim_token sc scopes with
+ match availability_of_prim_token p sc scopes with
| None -> raise No_match
| Some key ->
let loc = cases_pattern_loc pat in
insert_pat_alias loc (insert_pat_delimiters loc (CPatPrim(loc,p)) key) na
with No_match ->
- try
+ try
if !Flags.raw_print or !print_no_symbol then raise No_match;
extern_symbol_pattern scopes vars pat
(uninterp_cases_pattern_notations pat)
with No_match ->
match pat with
| PatVar (loc,Name id) -> CPatAtom (loc,Some (Ident (loc,id)))
- | PatVar (loc,Anonymous) -> CPatAtom (loc, None)
+ | PatVar (loc,Anonymous) -> CPatAtom (loc, None)
| PatCstr(loc,cstrsp,args,na) ->
let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
- let p = CPatCstr
- (loc,extern_reference loc vars (ConstructRef cstrsp),args) in
+ let p =
+ try
+ if !Flags.raw_print then raise Exit;
+ let projs = Recordops.lookup_projections (fst cstrsp) in
+ let rec ip projs args acc =
+ match projs with
+ | [] -> acc
+ | None :: q -> ip q args acc
+ | Some c :: q ->
+ match args with
+ | [] -> raise No_match
+ | CPatAtom(_, None) :: tail -> ip q tail acc
+ (* we don't want to have 'x = _' in our patterns *)
+ | head :: tail -> ip q tail
+ ((extern_reference loc Idset.empty (ConstRef c), head) :: acc)
+ in
+ CPatRecord(loc, List.rev (ip projs args []))
+ with
+ Not_found | No_match | Exit ->
+ CPatCstr (loc, extern_reference loc vars (ConstructRef cstrsp), args) in
insert_pat_alias loc p na
-
+
and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
| [] -> raise No_match
| (keyrule,pat,n as _rule)::rules ->
- try
- (* Check the number of arguments expected by the notation *)
- let loc,na = match t,n with
- | PatCstr (_,f,l,_), Some n when List.length l > n ->
- raise No_match
- | PatCstr (loc,_,_,na),_ -> loc,na
- | PatVar (loc,na),_ -> loc,na in
+ try
+ match t,n with
+ | PatCstr (loc,(ind,_),l,na), n when n = Some 0 or n = None or
+ n = Some(fst(Global.lookup_inductive ind)).Declarations.mind_nparams ->
+ (* Abbreviation for the constructor name only *)
+ (match keyrule with
+ | NotationRule (sc,ntn) -> raise No_match
+ | SynDefRule kn ->
+ let p =
+ let qid = Qualid (loc, shortest_qualid_of_syndef vars kn) in
+ if l = [] then
+ CPatAtom (loc,Some qid)
+ else
+ let l =
+ List.map (extern_cases_pattern_in_scope allscopes vars) l in
+ CPatCstr (loc,qid,l) in
+ insert_pat_alias loc p na)
+ | PatCstr (_,f,l,_), Some n when List.length l > n ->
+ raise No_match
+ | PatCstr (loc,_,_,na),_ ->
(* Try matching ... *)
let subst,substlist = match_aconstr_cases_pattern t pat in
(* Try availability of interpretation ... *)
@@ -446,16 +426,18 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
let subscope = (scopt,scl@scopes') in
List.map (extern_cases_pattern_in_scope subscope vars) c)
substlist in
- insert_pat_delimiters loc
+ insert_pat_delimiters loc
(make_pat_notation loc ntn (l,ll)) key)
| SynDefRule kn ->
let qid = shortest_qualid_of_syndef vars kn in
CPatAtom (loc,Some (Qualid (loc, qid))) in
insert_pat_alias loc p na
- with
- No_match -> extern_symbol_pattern allscopes vars t rules
+ | PatVar (loc,Anonymous),_ -> CPatAtom (loc, None)
+ | PatVar (loc,Name id),_ -> CPatAtom (loc, Some (Ident (loc,id)))
+ with
+ No_match -> extern_symbol_pattern allscopes vars t rules
-let extern_cases_pattern vars p =
+let extern_cases_pattern vars p =
extern_cases_pattern_in_scope (None,[]) vars p
(**********************************************************************)
@@ -468,7 +450,7 @@ let occur_name na aty =
let is_projection nargs = function
| Some r when not !Flags.raw_print & !print_projections ->
- (try
+ (try
let n = Recordops.find_projection_nparams r + 1 in
if n <= nargs then Some n else None
with Not_found -> None)
@@ -488,13 +470,13 @@ let explicitize loc inctx impl (cf,f) args =
let tail = exprec (q+1) (args,impl) in
let visible =
!Flags.raw_print or
- (!print_implicits & !print_implicits_explicit_args) or
+ (!print_implicits & !print_implicits_explicit_args) or
(!print_implicits_defensive &
is_significant_implicit a impl tail &
not (is_inferable_implicit inctx n imp))
in
- if visible then
- (a,Some (dummy_loc, ExplByName (name_of_implicit imp))) :: tail
+ if visible then
+ (a,Some (dummy_loc, ExplByName (name_of_implicit imp))) :: tail
else
tail
| a::args, _::impl -> (a,None) :: exprec (q+1) (args,impl)
@@ -511,7 +493,7 @@ let explicitize loc inctx impl (cf,f) args =
let args1 = exprec 1 (args1,impl1) in
let args2 = exprec (i+1) (args2,impl2) in
CApp (loc,(Some (List.length args1),f),args1@args2)
- | None ->
+ | None ->
let args = exprec 1 (args,impl) in
if args = [] then f else CApp (loc, (None, f), args)
@@ -525,11 +507,11 @@ let extern_app loc inctx impl (cf,f) args =
if args = [] (* maybe caused by a hidden coercion *) then
extern_global loc impl f
else
- if
+ if
((!Flags.raw_print or
(!print_implicits & not !print_implicits_explicit_args)) &
List.exists is_status_implicit impl)
- then
+ then
CAppExpl (loc, (is_projection (List.length args) cf, f), args)
else
explicitize loc inctx impl (cf,CRef f) args
@@ -550,49 +532,33 @@ let rec remove_coercions inctx = function
let nargs = List.length args in
(try match Classops.hide_coercion r with
| Some n when n < nargs && (inctx or n+1 < nargs) ->
- (* We skip a coercion *)
+ (* We skip a coercion *)
let l = list_skipn n args in
let (a,l) = match l with a::l -> (a,l) | [] -> assert false in
(* Recursively remove the head coercions *)
- (match remove_coercions true a with
- | RApp (_,a,l') -> RApp (loc,a,l'@l)
- | a -> RApp (loc,a,l))
+ let a' = remove_coercions true a in
+ (* Don't flatten App's in case of funclass so that
+ (atomic) notations on [a] work; should be compatible
+ since printer does not care whether App's are
+ collapsed or not and notations with an implicit
+ coercion using funclass either would have already
+ 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)
| _ -> 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))
+ | 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
-let rec share_fix_binders n rbl ty def =
- match ty,def with
- RProd(_,na0,bk0,t0,b), RLambda(_,na1,bk1,t1,m) ->
- if not(same_rawconstr t0 t1) then List.rev rbl, ty, def
- else
- let (na,b,m) =
- match na0, na1 with
- Name id0, Name id1 ->
- if id0=id1 then (na0,b,m)
- else if not (occur_rawconstr id1 b) then
- (na1,rename_rawconstr_var id0 id1 b,m)
- else if not (occur_rawconstr id0 m) then
- (na1,b,rename_rawconstr_var id1 id0 m)
- else (* vraiment pas de chance! *)
- failwith "share_fix_binders: capture"
- | Name id, Anonymous ->
- if not (occur_rawconstr id m) then (na0,b,m)
- else
- failwith "share_fix_binders: capture"
- | Anonymous, Name id ->
- if not (occur_rawconstr id b) then (na1,b,m)
- else
- failwith "share_fix_binders: capture"
- | _ -> (na1,b,m) in
- share_fix_binders (n-1) ((na,None,t0)::rbl) b m
- | _ -> List.rev rbl, ty, def
-
(**********************************************************************)
(* mapping rawterms to numerals (in presence of coercions, choose the *)
(* one with no delimiter if possible) *)
@@ -600,7 +566,7 @@ let rec share_fix_binders n rbl ty def =
let extern_possible_prim_token scopes r =
try
let (sc,n) = uninterp_prim_token r in
- match availability_of_prim_token sc scopes with
+ match availability_of_prim_token n sc scopes with
| None -> None
| Some key -> Some (insert_delimiters (CPrim (loc_of_rawconstr r,n)) key)
with No_match ->
@@ -623,13 +589,14 @@ let extern_rawsort = function
let rec extern inctx scopes vars r =
let r' = remove_coercions inctx r in
- try
+ try
if !Flags.raw_print or !print_no_symbol then raise No_match;
extern_optimal_prim_token scopes r r'
with No_match ->
- try
+ try
+ let r'' = flatten_application r' in
if !Flags.raw_print or !print_no_symbol then raise No_match;
- extern_symbol scopes vars r' (uninterp_notations r')
+ extern_symbol scopes vars r'' (uninterp_notations r'')
with No_match -> match r' with
| RRef (loc,ref) ->
extern_global loc (implicits_of_global ref)
@@ -651,10 +618,44 @@ let rec extern inctx scopes vars r =
let subscopes = find_arguments_scope ref in
let args =
extern_args (extern true) (snd scopes) vars args subscopes in
- extern_app loc inctx (implicits_of_global ref)
- (Some ref,extern_reference rloc vars ref)
- args
- | _ ->
+ begin
+ try
+ 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
+ let projs = struc.Recordops.s_PROJ in
+ let locals = struc.Recordops.s_PROJKIND in
+ let rec cut args n =
+ if n = 0 then args
+ else
+ match args with
+ | [] -> raise No_match
+ | _ :: t -> cut t (n - 1) in
+ let args = cut args struc.Recordops.s_EXPECTEDPARAM in
+ let rec ip projs locs args acc =
+ match projs with
+ | [] -> acc
+ | None :: q -> raise No_match
+ | Some c :: q ->
+ match locs with
+ | [] -> anomaly "projections corruption [Constrextern.extern]"
+ | (_, false) :: locs' ->
+ (* we don't want to print locals *)
+ ip q locs' args acc
+ | (_, true) :: locs' ->
+ match args with
+ | [] -> raise No_match
+ (* we give up since the constructor is not complete *)
+ | head :: tail -> ip q locs' tail
+ ((extern_reference loc Idset.empty (ConstRef c), head) :: acc)
+ in
+ CRecord (loc, None, List.rev (ip projs locals args []))
+ with
+ | Not_found | No_match | Exit ->
+ extern_app loc inctx (implicits_of_global ref)
+ (Some ref,extern_reference rloc vars ref) args
+ end
+ | _ ->
explicitize loc inctx [] (None,sub_extern false scopes vars f)
(List.map (sub_extern true scopes vars) args))
@@ -675,15 +676,15 @@ let rec extern inctx scopes vars r =
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) ->
- let vars' =
+ 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
+ Anonymous, RVar (_,id) when
rtntypopt<>None & occur_rawconstr id (Option.get rtntypopt)
-> Some Anonymous
| Anonymous, _ -> None
@@ -694,11 +695,11 @@ let rec extern inctx scopes vars r =
let params = list_tabulate
(fun _ -> RHole (dummy_loc,Evd.InternalHole)) n in
let args = List.map (function
- | Anonymous -> RHole (dummy_loc,Evd.InternalHole)
+ | 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
(extern_typ scopes vars t)) x))) tml in
- let eqns = List.map (extern_eqn inctx scopes vars) eqns 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) ->
@@ -718,23 +719,23 @@ let rec extern inctx scopes vars r =
let vars' = Array.fold_right Idset.add idv vars in
(match fk with
| RFix (nv,n) ->
- let listdecl =
+ let listdecl =
Array.mapi (fun i fi ->
let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in
let (ids,bl) = extern_local_binder scopes vars bl in
let vars0 = List.fold_right (name_fold Idset.add) ids vars in
let vars1 = List.fold_right (name_fold Idset.add) ids vars' in
- let n =
+ let n =
match fst nv.(i) with
| None -> None
| Some x -> Some (dummy_loc, out_name (List.nth ids x))
- in
+ in
let ro = extern_recursion_order scopes vars (snd nv.(i)) in
((dummy_loc, fi), (n, ro), bl, extern_typ scopes vars0 ty,
extern false scopes vars1 def)) idv
- in
+ in
CFix (loc,(loc,idv.(n)),Array.to_list listdecl)
- | RCoFix n ->
+ | RCoFix n ->
let listdecl =
Array.mapi (fun i fi ->
let (ids,bl) = extern_local_binder scopes vars blv.(i) in
@@ -756,13 +757,13 @@ let rec extern inctx scopes vars r =
| RDynamic (loc,d) -> CDynamic (loc,d)
-and extern_typ (_,scopes) =
+and extern_typ (_,scopes) =
extern true (Some Notation.type_scope,scopes)
and sub_extern inctx (_,scopes) = extern inctx (None,scopes)
and factorize_prod scopes vars aty c =
- try
+ try
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
@@ -774,7 +775,7 @@ and factorize_prod scopes vars aty c =
| c -> ([],extern_typ scopes vars c)
and factorize_lambda inctx scopes vars aty c =
- try
+ try
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
@@ -793,7 +794,7 @@ and extern_local_binder scopes vars = function
extern_local_binder scopes (name_fold Idset.add na vars) l in
(na::ids,
LocalRawDef((dummy_loc,na), extern false scopes vars bd) :: l)
-
+
| (na,bk,None,ty)::l ->
let ty = extern_typ scopes vars (anonymize_if_reserved na ty) in
(match extern_local_binder scopes (name_fold Idset.add na vars) l with
@@ -817,13 +818,22 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
let loc = Rawterm.loc_of_rawconstr t in
try
(* Adjusts to the number of arguments expected by the notation *)
- let (t,args) = match t,n with
- | RApp (_,(RRef _ as f),args), Some n when List.length args >= n ->
+ let (t,args,argsscopes,argsimpls) = match t,n with
+ | RApp (_,(RRef (_,ref) as f),args), Some n
+ when List.length args >= n ->
let args1, args2 = list_chop n args in
- (if n = 0 then f else RApp (dummy_loc,f,args1)), args2
- | RApp (_,(RRef _ as f),args), None -> f, args
- | RRef _, Some 0 -> RApp (dummy_loc,t,[]), []
- | _, None -> t,[]
+ let subscopes =
+ try list_skipn n (find_arguments_scope ref) with _ -> [] in
+ let impls =
+ try list_skipn n (implicits_of_global ref) with _ -> [] in
+ (if n = 0 then f else RApp (dummy_loc,f,args1)),
+ args2, subscopes, impls
+ | RApp (_,(RRef (_,ref) as f),args), None ->
+ let subscopes = find_arguments_scope ref in
+ let impls = implicits_of_global ref in
+ f, args, subscopes, impls
+ | RRef _, Some 0 -> RApp (dummy_loc,t,[]), [], [], []
+ | _, None -> t, [], [], []
| _ -> raise No_match in
(* Try matching ... *)
let subst,substlist = match_aconstr t pat in
@@ -854,18 +864,18 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
subst in
let a = CRef (Qualid (loc, shortest_qualid_of_syndef vars kn)) in
if l = [] then a else CApp (loc,(None,a),l) in
- if args = [] then e
+ if args = [] then e
else
- (* TODO: compute scopt for the extra args, in case, head is a ref *)
- explicitize loc false [] (None,e)
- (List.map (extern true allscopes vars) args)
+ let args = extern_args (extern true) scopes vars args argsscopes in
+ explicitize loc false argsimpls (None,e) args
with
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 c -> CMeasureRec (extern true scopes vars c)
+ | RMeasureRec (m,r) -> CMeasureRec (extern true scopes vars m,
+ Option.map (extern true scopes vars) r)
let extern_rawconstr vars c =
@@ -901,13 +911,6 @@ let extern_sort s = extern_rawsort (detype_sort s)
(******************************************************************)
(* Main translation function from pattern -> constr_expr *)
-let it_destPLambda n c =
- let rec aux n nal c =
- if n=0 then (nal,c) else match c with
- | PLambda (na,_,c) -> aux (n-1) (na::nal) c
- | _ -> anomaly "it_destPLambda" in
- aux n [] c
-
let rec raw_of_pat env = function
| PRef ref -> RRef (loc,ref)
| PVar id -> RVar (loc,id)
@@ -933,7 +936,7 @@ let rec raw_of_pat env = function
| PLambda (na,t,c) ->
RLambda (loc,na,Explicit,raw_of_pat env t, raw_of_pat (na::env) c)
| PIf (c,b1,b2) ->
- RIf (loc, raw_of_pat env c, (Anonymous,None),
+ 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
@@ -948,7 +951,7 @@ let rec raw_of_pat env = function
let mat = simple_cases_matrix_of_branches ind brns brs in
let indnames,rtn =
if p = PMeta None then (Anonymous,None),None
- else
+ 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)
@@ -956,9 +959,6 @@ let rec raw_of_pat env = function
| PCoFix c -> Detyping.detype false [] env (mkCoFix c)
| PSort s -> RSort (loc,s)
-and raw_of_eqns env constructs consnargsl bl =
- Array.to_list (array_map3 (raw_of_eqn env) constructs consnargsl bl)
-
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
@@ -967,22 +967,22 @@ and raw_of_eqn env constr construct_nargs branch =
in
let rec buildrec ids patlist env n b =
if n=0 then
- (dummy_loc, ids,
+ (dummy_loc, ids,
[PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)],
raw_of_pat env b)
else
match b with
- | PLambda (x,_,b) ->
+ | 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) ->
+ | 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
+ in
buildrec [] [] env construct_nargs branch
let extern_constr_pattern env pat =
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index ec0a262b..08a74e61 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: constrextern.mli 10790 2008-04-14 22:34:19Z herbelin $ i*)
+(*i $Id$ i*)
(*i*)
open Util
@@ -34,7 +34,7 @@ val extern_rawconstr : Idset.t -> rawconstr -> constr_expr
val extern_rawtype : Idset.t -> rawconstr -> 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
@@ -42,7 +42,7 @@ 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_rel_context : constr option -> env ->
+val extern_rel_context : constr option -> env ->
rel_context -> local_binder list
(* Printing options *)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c8faf911..b5604cf7 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -6,13 +6,14 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: constrintern.ml 13131 2010-06-13 18:45:17Z herbelin $ *)
+(* $Id$ *)
open Pp
open Util
open Flags
open Names
open Nameops
+open Namegen
open Libnames
open Impargs
open Rawterm
@@ -24,66 +25,32 @@ open Nametab
open Notation
open Inductiveops
-open Decl_kinds
-
-let type_of_logical_kind =
- function
- | IsDefinition def ->
- (match def with
- | Definition -> "def"
- | Coercion -> "coe"
- | SubClass -> "subclass"
- | CanonicalStructure -> "canonstruc"
- | Example -> "ex"
- | Fixpoint -> "def"
- | CoFixpoint -> "def"
- | Scheme -> "scheme"
- | StructureComponent -> "proj"
- | IdentityCoercion -> "coe"
- | Instance -> "inst"
- | Method -> "meth")
- | IsAssumption a ->
- (match a with
- | Definitional -> "defax"
- | Logical -> "prfax"
- | Conjectural -> "prfax")
- | IsProof th ->
- (match th with
- | Theorem
- | Lemma
- | Fact
- | Remark
- | Property
- | Proposition
- | Corollary -> "thm")
-
-let type_of_global_ref gr =
- if Typeclasses.is_class gr then
- "class"
- else
- match gr with
- | ConstRef cst ->
- type_of_logical_kind (Decls.constant_kind cst)
- | VarRef v ->
- "var" ^ type_of_logical_kind (Decls.variable_kind v)
- | IndRef ind ->
- let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in
- if mib.Declarations.mind_record then
- if mib.Declarations.mind_finite then "rec"
- else "corec"
- else if mib.Declarations.mind_finite then "ind"
- else "coind"
- | ConstructRef _ -> "constr"
-
-(* To interpret implicits and arg scopes of recursive variables in
- inductive types and recursive definitions *)
-type var_internalisation_type = Inductive | Recursive | Method
-
-type var_internalisation_data =
- var_internalisation_type * identifier list * Impargs.implicits_list * scope_name option list
-
-type implicits_env = (identifier * var_internalisation_data) list
-type full_implicits_env = identifier list * implicits_env
+(* To interpret implicits and arg scopes of variables in inductive
+ types and recursive definitions and of projection names in records *)
+
+type var_internalization_type = Inductive | Recursive | Method
+
+type var_internalization_data =
+ (* type of the "free" variable, for coqdoc, e.g. while typing the
+ constructor of JMeq, "JMeq" behaves as a variable of type Inductive *)
+ var_internalization_type *
+ (* 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) *)
+ identifier list *
+ (* signature of impargs of the variable *)
+ Impargs.implicits_list *
+ (* subscopes of the args of the variable *)
+ scope_name option list
+
+type internalization_env =
+ (identifier * var_internalization_data) list
+
+type full_internalization_env =
+ (* a superset of the list of variables that may be automatically
+ inserted and that must not occur as binders *)
+ identifier list *
+ (* mapping of the variables to their internalization data *)
+ internalization_env
type raw_binder = (name * binding_kind * rawconstr option * rawconstr)
@@ -98,6 +65,33 @@ let for_grammar f x =
a
(**********************************************************************)
+(* Locating reference, possibly via an abbreviation *)
+
+let locate_reference qid =
+ Smartlocate.global_of_extended_global (Nametab.locate_extended qid)
+
+let is_global id =
+ try
+ let _ = locate_reference (qualid_of_ident id) in true
+ with Not_found ->
+ false
+
+let global_reference_of_reference ref =
+ locate_reference (snd (qualid_of_reference ref))
+
+let global_reference id =
+ constr_of_global (locate_reference (qualid_of_ident id))
+
+let construct_reference ctx id =
+ try
+ Term.mkVar (let _ = Sign.lookup_named id ctx in id)
+ with Not_found ->
+ global_reference id
+
+let global_reference_in_absolute_module dir id =
+ constr_of_global (Nametab.global_of_path (Libnames.make_path dir id))
+
+(**********************************************************************)
(* Internalisation errors *)
type internalisation_error =
@@ -126,7 +120,7 @@ let explain_not_a_constructor ref =
str "Unknown constructor: " ++ pr_reference ref
let explain_unbound_fix_name is_cofix id =
- str "The name" ++ spc () ++ pr_id id ++
+ str "The name" ++ spc () ++ pr_id id ++
spc () ++ str "is not bound in the corresponding" ++ spc () ++
str (if is_cofix then "co" else "") ++ str "fixpoint definition"
@@ -143,13 +137,13 @@ let explain_bad_explicitation_number n po =
let s = match po with
| None -> str "a regular argument"
| Some p -> int p in
- str "Bad explicitation number: found " ++ int n ++
+ str "Bad explicitation number: found " ++ int n ++
str" but was expecting " ++ s
| ExplByName id ->
let s = match po with
| None -> str "a regular argument"
| Some p -> (*pr_id (name_of_position p) in*) failwith "" in
- str "Bad explicitation name: found " ++ pr_id id ++
+ str "Bad explicitation name: found " ++ pr_id id ++
str" but was expecting " ++ s
let explain_internalisation_error e =
@@ -164,13 +158,8 @@ let explain_internalisation_error e =
| BadExplicitationNumber (n,po) -> explain_bad_explicitation_number n po in
pp ++ str "."
-let error_unbound_patvar loc n =
- user_err_loc
- (loc,"glob_qualid_or_patvar", str "?" ++ pr_patvar n ++
- str " is unbound.")
-
let error_bad_inductive_type loc =
- user_err_loc (loc,"",str
+ user_err_loc (loc,"",str
"This should be an inductive type applied to names or \"_\".")
let error_inductive_parameter_not_implicit loc =
@@ -179,6 +168,35 @@ let error_inductive_parameter_not_implicit loc =
"the 'return' clauses; they must be replaced by '_' in the 'in' clauses."))
(**********************************************************************)
+(* Pre-computing the implicit arguments and arguments scopes needed *)
+(* for interpretation *)
+
+let empty_internalization_env = ([],[])
+
+let set_internalization_env_params ienv params =
+ let nparams = List.length params in
+ if nparams = 0 then
+ ([],ienv)
+ else
+ let ienv_with_implicit_params =
+ List.map (fun (id,(ty,_,impl,scopes)) ->
+ let sub_impl,_ = list_chop nparams impl in
+ let sub_impl' = List.filter is_status_implicit sub_impl in
+ (id,(ty,List.map name_of_implicit sub_impl',impl,scopes))) ienv in
+ (params, ienv_with_implicit_params)
+
+let compute_internalization_data env ty typ impls =
+ let impl = compute_implicits_with_manual env typ (is_implicit_args()) impls in
+ (ty, [], impl, compute_arguments_scope typ)
+
+let compute_full_internalization_env env ty params idl typl impll =
+ set_internalization_env_params
+ (list_map3
+ (fun id typ impl -> (id,compute_internalization_data env ty typ impl))
+ idl typl impll)
+ params
+
+(**********************************************************************)
(* Contracting "{ _ }" in notations *)
let rec wildcards ntn n =
@@ -191,8 +209,8 @@ and spaces ntn n =
let expand_notation_string ntn n =
let pos = List.nth (wildcards ntn 0) n in
let hd = if pos = 0 then "" else String.sub ntn 0 pos in
- let tl =
- if pos = String.length ntn then ""
+ let tl =
+ if pos = String.length ntn then ""
else String.sub ntn (pos+1) (String.length ntn - pos -1) in
hd ^ "{ _ }" ^ tl
@@ -202,7 +220,7 @@ let contract_notation ntn (l,ll) =
let ntn' = ref ntn in
let rec contract_squash n = function
| [] -> []
- | CNotation (_,"{ _ }",([a],[])) :: l ->
+ | CNotation (_,"{ _ }",([a],[])) :: l ->
ntn' := expand_notation_string !ntn' n;
contract_squash n (a::l)
| a :: l ->
@@ -215,7 +233,7 @@ let contract_pat_notation ntn (l,ll) =
let ntn' = ref ntn in
let rec contract_squash n = function
| [] -> []
- | CPatNotation (_,"{ _ }",([a],[])) :: l ->
+ | CPatNotation (_,"{ _ }",([a],[])) :: l ->
ntn' := expand_notation_string !ntn' n;
contract_squash n (a::l)
| a :: l ->
@@ -227,26 +245,40 @@ let contract_pat_notation ntn (l,ll) =
(**********************************************************************)
(* Remembering the parsing scope of variables in notations *)
-let make_current_scope (tmp_scope,scopes) = Option.List.cons tmp_scope scopes
+let make_current_scope = function
+ | (Some tmp_scope,(sc::_ as scopes)) when sc = tmp_scope -> scopes
+ | (Some tmp_scope,scopes) -> tmp_scope::scopes
+ | None,scopes -> scopes
let set_var_scope loc id (_,_,scopt,scopes) varscopes =
let idscopes = List.assoc id varscopes in
- if !idscopes <> None &
+ if !idscopes <> None &
make_current_scope (Option.get !idscopes)
<> make_current_scope (scopt,scopes) then
+ let pr_scope_stack = function
+ | [] -> str "the empty scope stack"
+ | [a] -> str "scope " ++ str a
+ | l -> str "scope stack " ++
+ str "[" ++ prlist_with_sep pr_comma str l ++ str "]" in
user_err_loc (loc,"set_var_scope",
- pr_id id ++ str " already occurs in a different scope.")
+ pr_id id ++ str " is used both in " ++
+ pr_scope_stack (make_current_scope (Option.get !idscopes)) ++
+ strbrk " and in " ++
+ pr_scope_stack (make_current_scope (scopt,scopes)))
else
idscopes := Some (scopt,scopes)
(**********************************************************************)
(* Syntax extensions *)
-let traverse_binder (subst,substlist) (renaming,(ids,unb,tmpsc,scopes as env)) id =
+let traverse_binder (subst,substlist) (renaming,(ids,unb,tmpsc,scopes as env))=
+ function
+ | Anonymous -> (renaming,env),Anonymous
+ | Name id ->
try
(* Binders bound in the notation are considered first-order objects *)
- let _,id' = coerce_to_id (fst (List.assoc id subst)) in
- (renaming,(Idset.add id' ids,unb,tmpsc,scopes)), id'
+ let _,na = coerce_to_name (fst (List.assoc id subst)) in
+ (renaming,(name_fold Idset.add na ids,unb,tmpsc,scopes)), na
with Not_found ->
(* Binders not bound in the notation do not capture variables *)
(* outside the notation (i.e. in the substitution) *)
@@ -256,7 +288,7 @@ let traverse_binder (subst,substlist) (renaming,(ids,unb,tmpsc,scopes as env)) i
let fvs = List.flatten (List.map Idset.elements (fvs1@fvs2)) @ fvs3 in
let id' = next_ident_away id fvs in
let renaming' = if id=id' then renaming else (id,id')::renaming in
- (renaming',env), id'
+ (renaming',env), Name id'
let rec subst_iterator y t = function
| RVar (_,id) as x -> if id = y then t else x
@@ -270,40 +302,45 @@ let rec subst_aconstr_in_rawconstr loc interp (subst,substlist as sub) infos c =
begin
(* subst remembers the delimiters stack in the interpretation *)
(* of the notations *)
- try
+ try
let (a,(scopt,subscopes)) = List.assoc id subst in
interp (ids,unb,scopt,subscopes@scopes) a
- with Not_found ->
- try
+ with Not_found ->
+ try
RVar (loc,List.assoc id renaming)
- with Not_found ->
+ with Not_found ->
(* Happens for local notation joint with inductive/fixpoint defs *)
RVar (loc,id)
end
| AList (x,_,iter,terminator,lassoc) ->
- (try
+ (try
(* All elements of the list are in scopes (scopt,subscopes) *)
let (l,(scopt,subscopes)) = List.assoc x substlist in
- let termin =
+ let termin =
subst_aconstr_in_rawconstr loc interp sub subinfos terminator in
- List.fold_right (fun a t ->
+ List.fold_right (fun a t ->
subst_iterator ldots_var t
- (subst_aconstr_in_rawconstr loc interp
+ (subst_aconstr_in_rawconstr loc interp
((x,(a,(scopt,subscopes)))::subst,substlist) subinfos iter))
(if lassoc then List.rev l else l) termin
- with Not_found ->
+ with Not_found ->
anomaly "Inconsistent substitution of recursive notation")
+ | AHole (Evd.BinderType (Name id as na)) ->
+ let na =
+ try snd (coerce_to_name (fst (List.assoc id subst)))
+ with Not_found -> na in
+ RHole (loc,Evd.BinderType na)
| t ->
rawconstr_of_aconstr_with_binders loc (traverse_binder sub)
(subst_aconstr_in_rawconstr loc interp sub) subinfos t
let intern_notation intern (_,_,tmp_scope,scopes as env) loc ntn fullargs =
- let ntn,(args,argslist) = contract_notation ntn fullargs in
+ let ntn,(args,argslist as fullargs) = contract_notation ntn fullargs in
let (((ids,idsl),c),df) = interp_notation loc ntn (tmp_scope,scopes) in
- Dumpglob.dump_notation_location (Topconstr.ntn_loc loc args 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 argslist in
- subst_aconstr_in_rawconstr loc intern (subst,substlist) ([],env) c
+ Dumpglob.dump_notation_location (ntn_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 argslist in
+ subst_aconstr_in_rawconstr loc intern (subst,substlist) ([],env) c
let set_type_scope (ids,unb,tmp_scope,scopes) =
(ids,unb,Some Notation.type_scope,scopes)
@@ -337,8 +374,8 @@ let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) l
let (vars1,unbndltacvars) = ltacvars in
(* Is [id] an inductive type potentially with implicit *)
try
- let ty, l,impl,argsc = List.assoc id impls in
- let l = List.map
+ let ty,l,impl,argsc = List.assoc id impls in
+ let l = List.map
(fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) l in
let tys = string_of_ty ty in
Dumpglob.dump_reference loc "<>" (string_of_id id) tys;
@@ -353,7 +390,6 @@ let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) l
then
(set_var_scope loc id genv vars3; RVar (loc,id), [], [], [])
else
-
(* Is [id] bound to a free name in ltac (this is an ltac error message) *)
try
match List.assoc id unbndltacvars with
@@ -367,13 +403,21 @@ let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) l
(* [id] a section variable *)
(* Redundant: could be done in intern_qualid *)
let ref = VarRef id in
- RRef (loc, ref), implicits_of_global ref, find_arguments_scope ref, []
+ 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, []
with _ ->
(* [id] a goal variable *)
RVar (loc,id), [], [], []
-
-let find_appl_head_data (_,_,_,(_,impls)) = function
+
+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
+ when l <> [] & Flags.version_strictly_greater Flags.V8_2 ->
+ let n = List.length l in
+ x,list_skipn_at_least n (implicits_of_global ref),
+ list_skipn_at_least n (find_arguments_scope ref),[]
| x -> x,[],[],[]
let error_not_enough_arguments loc =
@@ -386,23 +430,31 @@ let check_no_explicitation l =
user_err_loc
(loc,"",str"Unexpected explicitation of the argument of an abbreviation.")
+let dump_extended_global loc = function
+ | TrueGlobal ref -> Dumpglob.add_glob loc ref
+ | SynDef sp -> Dumpglob.add_glob_kn loc sp
+
+let intern_extended_global_of_qualid (loc,qid) =
+ try let r = Nametab.locate_extended qid in dump_extended_global loc r; r
+ with Not_found -> error_global_not_found_loc loc qid
+
+let intern_reference ref =
+ Smartlocate.global_of_extended_global
+ (intern_extended_global_of_qualid (qualid_of_reference ref))
+
(* Is it a global reference or a syntactic definition? *)
let intern_qualid loc qid intern env args =
- try match Nametab.extended_locate qid with
+ match intern_extended_global_of_qualid (loc,qid) with
| TrueGlobal ref ->
- Dumpglob.add_glob loc ref;
RRef (loc, ref), args
- | SyntacticDef sp ->
- Dumpglob.add_glob_kn loc sp;
- let (ids,c) = Syntax_def.search_syntactic_definition loc sp in
+ | SynDef sp ->
+ let (ids,c) = Syntax_def.search_syntactic_definition sp in
let nids = List.length ids in
if List.length args < nids then error_not_enough_arguments loc;
let args1,args2 = list_chop nids args in
check_no_explicitation args1;
let subst = List.map2 (fun (id,scl) a -> (id,(fst a,scl))) ids args1 in
subst_aconstr_in_rawconstr loc intern (subst,[]) ([],env) c, args2
- with Not_found ->
- error_global_not_found_loc loc qid
(* Rule out section vars since these should have been found by intern_var *)
let intern_non_secvar_qualid loc qid intern env args =
@@ -413,20 +465,20 @@ let intern_non_secvar_qualid loc qid intern env args =
let intern_applied_reference intern (_, unb, _, _ as env) lvar args = function
| Qualid (loc, qid) ->
let r,args2 = intern_qualid loc qid intern env args in
- find_appl_head_data lvar r, args2
+ find_appl_head_data r, args2
| Ident (loc, id) ->
try intern_var env lvar loc id, args
- with Not_found ->
- let qid = make_short_qualid id in
+ with Not_found ->
+ let qid = qualid_of_ident id in
try
let r,args2 = intern_non_secvar_qualid loc qid intern env args in
- find_appl_head_data lvar r, args2
+ find_appl_head_data r, args2
with e ->
(* Extra allowance for non globalizing functions *)
if !interning_grammar || unb then
(RVar (loc,id), [], [], []),args
else raise e
-
+
let interp_reference vars r =
let (r,_,_,_),_ =
intern_applied_reference (fun _ -> error_not_enough_arguments dummy_loc)
@@ -437,12 +489,6 @@ let apply_scope_env (ids,unb,_,scopes) = function
| [] -> (ids,unb,None,scopes), []
| sc::scl -> (ids,unb,sc,scopes), scl
-let rec adjust_scopes env scopes = function
- | [] -> []
- | a::args ->
- let (enva,scopes) = apply_scope_env env scopes in
- enva :: adjust_scopes env scopes args
-
let rec simple_adjust_scopes n = function
| [] -> if n=0 then [] else None :: simple_adjust_scopes (n-1) []
| sc::scopes -> sc :: simple_adjust_scopes (n-1) scopes
@@ -473,11 +519,11 @@ let simple_product_of_cases_patterns pl =
pl [[],[]]
(* Check linearity of pattern-matching *)
-let rec has_duplicate = function
+let rec has_duplicate = function
| [] -> None
| x::l -> if List.mem x l then (Some x) else has_duplicate l
-let loc_of_lhs lhs =
+let loc_of_lhs lhs =
join_loc (fst (List.hd lhs)) (fst (list_last lhs))
let check_linearity lhs ids =
@@ -494,7 +540,7 @@ let check_number_of_pattern loc n l =
let check_or_pat_variables loc ids idsl =
if List.exists (fun ids' -> not (list_eq_set ids ids')) idsl then
- user_err_loc (loc, "", str
+ user_err_loc (loc, "", str
"The components of this disjunctive pattern must bind the same variables.")
let check_constructor_length env loc cstr pl pl0 =
@@ -516,7 +562,7 @@ let alias_of = function
| (id::_,_) -> Name id
let message_redundant_alias (id1,id2) =
- if_verbose warning
+ if_verbose warning
("Alias variable "^(string_of_id id1)^" is merged with "^(string_of_id id2))
(* Expanding notations *)
@@ -525,12 +571,16 @@ let error_invalid_pattern_notation loc =
user_err_loc (loc,"",str "Invalid notation for pattern.")
let chop_aconstr_constructor loc (ind,k) args =
- let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
- if nparams > List.length args then error_invalid_pattern_notation loc;
- let params,args = list_chop nparams args in
- List.iter (function AHole _ -> ()
- | _ -> error_invalid_pattern_notation loc) params;
- args
+ if List.length args = 0 then (* Tolerance for a @id notation *) args else
+ begin
+ let mib,_ = Global.lookup_inductive ind in
+ let nparams = mib.Declarations.mind_nparams in
+ if nparams > List.length args then error_invalid_pattern_notation loc;
+ let params,args = list_chop nparams args in
+ List.iter (function AHole _ -> ()
+ | _ -> error_invalid_pattern_notation loc) params;
+ args
+ end
let rec subst_pat_iterator y t (subst,p) = match p with
| PatVar (_,id) as x ->
@@ -546,10 +596,10 @@ let subst_cases_pattern loc alias intern fullsubst scopes a =
begin
(* subst remembers the delimiters stack in the interpretation *)
(* of the notations *)
- try
+ try
let (a,(scopt,subscopes)) = List.assoc id subst in
intern (subscopes@scopes) ([],[]) scopt a
- with Not_found ->
+ with Not_found ->
if id = ldots_var then [], [[], PatVar (loc,Name id)] else
anomaly ("Unbound pattern notation variable: "^(string_of_id id))
(*
@@ -565,41 +615,41 @@ let subst_cases_pattern loc alias intern fullsubst scopes a =
let args = chop_aconstr_constructor loc cstr args in
let idslpll = List.map (aux Anonymous fullsubst) args in
let ids',pll = product_of_cases_patterns [] idslpll in
- let pl' = List.map (fun (asubst,pl) ->
+ let pl' = List.map (fun (asubst,pl) ->
asubst,PatCstr (loc,cstr,pl,alias)) pll in
ids', pl'
| AList (x,_,iter,terminator,lassoc) ->
- (try
+ (try
(* All elements of the list are in scopes (scopt,subscopes) *)
let (l,(scopt,subscopes)) = List.assoc x substlist in
let termin = aux Anonymous fullsubst terminator in
let idsl,v =
- List.fold_right (fun a (tids,t) ->
+ List.fold_right (fun a (tids,t) ->
let uids,u = aux Anonymous ((x,(a,(scopt,subscopes)))::subst,substlist) iter in
let pll = List.map (subst_pat_iterator ldots_var t) u in
tids@uids, List.flatten pll)
(if lassoc then List.rev l else l) termin in
idsl, List.map (fun ((asubst, pl) as x) ->
match pl with PatCstr (loc, c, pl, Anonymous) -> (asubst, PatCstr (loc, c, pl, alias)) | _ -> x) v
- with Not_found ->
+ with Not_found ->
anomaly "Inconsistent substitution of recursive notation")
| t -> error_invalid_pattern_notation loc
in aux alias fullsubst a
(* Differentiating between constructors and matching variables *)
type pattern_qualid_kind =
- | ConstrPat of constructor * (identifier list *
+ | ConstrPat of constructor * (identifier list *
((identifier * identifier) list * cases_pattern) list) list
| VarPat of identifier
let find_constructor ref f aliases pats scopes =
let (loc,qid) = qualid_of_reference ref in
let gref =
- try extended_locate qid
+ try locate_extended qid
with Not_found -> raise (InternalisationError (loc,NotAConstructor ref)) in
match gref with
- | SyntacticDef sp ->
- let (vars,a) = Syntax_def.search_syntactic_definition loc sp in
+ | SynDef sp ->
+ let (vars,a) = Syntax_def.search_syntactic_definition sp in
(match a with
| ARef (ConstructRef cstr) ->
assert (vars=[]);
@@ -613,14 +663,14 @@ let find_constructor ref f aliases pats scopes =
let idspl1 = List.map (subst_cases_pattern loc (alias_of aliases) f (subst,[]) scopes) args in
cstr, idspl1, pats2
| _ -> raise Not_found)
-
+
| TrueGlobal r ->
let rec unf = function
| ConstRef cst ->
let v = Environ.constant_value (Global.env()) cst in
unf (global_of_constr v)
- | ConstructRef cstr ->
- Dumpglob.add_glob loc r;
+ | ConstructRef cstr ->
+ Dumpglob.add_glob loc r;
cstr, [], pats
| _ -> raise Not_found
in unf r
@@ -643,17 +693,110 @@ let maybe_constructor ref f aliases scopes =
str " is understood as a pattern variable");
VarPat (find_pattern_variable ref)
-let mustbe_constructor loc ref f aliases patl scopes =
+let mustbe_constructor loc ref f aliases patl scopes =
try find_constructor ref f aliases patl scopes
with (Environ.NotEvaluableConst _ | Not_found) ->
raise (InternalisationError (loc,NotAConstructor ref))
+let sort_fields mode loc l completer =
+(*mode=false if pattern and true if constructor*)
+ match l with
+ | [] -> None
+ | (refer, value)::rem ->
+ let (nparams, (* the number of parameters *)
+ base_constructor, (* the reference constructor of the record *)
+ (max, (* number of params *)
+ (first_index, (* index of the first field of the record *)
+ list_proj))) (* list of projections *)
+ =
+ let record =
+ try Recordops.find_projection
+ (global_reference_of_reference refer)
+ with Not_found ->
+ user_err_loc (loc, "intern", str"Not a projection")
+ in
+ (* elimination of the first field from the projections *)
+ let rec build_patt l m i acc =
+ match l with
+ | [] -> (i, acc)
+ | (Some name) :: b->
+ (match m with
+ | [] -> anomaly "Number of projections mismatch"
+ | (_, regular)::tm ->
+ let boolean = not regular in
+ if ConstRef name = global_reference_of_reference refer
+ then
+ if boolean && mode then
+ user_err_loc (loc, "", str"No local fields allowed in a record construction.")
+ else build_patt b tm (i + 1) (i, snd acc) (* we found it *)
+ else
+ build_patt b tm (if boolean&&mode then i else i + 1)
+ (if boolean && mode then acc
+ else fst acc, (i, ConstRef name) :: snd acc))
+ | None :: b-> (* we don't want anonymous fields *)
+ if mode then
+ user_err_loc (loc, "", str "This record contains anonymous fields.")
+ else build_patt b m (i+1) acc
+ (* anonymous arguments don't appear in m *)
+ in
+ let ind = record.Recordops.s_CONST in
+ try (* insertion of Constextern.reference_global *)
+ (record.Recordops.s_EXPECTEDPARAM,
+ Qualid (loc, shortest_qualid_of_global Idset.empty (ConstructRef ind)),
+ build_patt record.Recordops.s_PROJ record.Recordops.s_PROJKIND 1 (0,[]))
+ with Not_found -> anomaly "Environment corruption for records."
+ in
+ (* now we want to have all fields of the pattern indexed by their place in
+ the constructor *)
+ let rec sf patts accpatt =
+ match patts with
+ | [] -> accpatt
+ | p::q->
+ let refer, patt = p in
+ let rec add_patt l acc =
+ match l with
+ | [] ->
+ user_err_loc
+ (loc, "",
+ str "This record contains fields of different records.")
+ | (i, a) :: b->
+ if global_reference_of_reference refer = a
+ then (i,List.rev_append acc l)
+ else add_patt b ((i,a)::acc)
+ in
+ let (index, projs) = add_patt (snd accpatt) [] in
+ sf q ((index, patt)::fst accpatt, projs) in
+ let (unsorted_indexed_pattern, remainings) =
+ sf rem ([first_index, value], list_proj) in
+ (* we sort them *)
+ let sorted_indexed_pattern =
+ List.sort (fun (i, _) (j, _) -> compare i j) unsorted_indexed_pattern in
+ (* a function to complete with wildcards *)
+ let rec complete_list n l =
+ if n <= 1 then l else complete_list (n-1) (completer n l) in
+ (* a function to remove indice *)
+ let rec clean_list l i acc =
+ match l with
+ | [] -> complete_list (max - i) acc
+ | (k, p)::q-> clean_list q k (p::(complete_list (k - i) acc))
+ in
+ 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 intern_pat = intern_cases_pattern genv in
+ 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
+ | CPatRecord (loc, l) ->
+ let sorted_fields = sort_fields false loc l (fun _ l -> (CPatAtom (loc, None))::l) in
+ let self_patt =
+ match sorted_fields with
+ | 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
check_constructor_length genv loc c idslpl1 pl2;
@@ -669,9 +812,9 @@ let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat=
| CPatNotation (_,"( _ )",([a],[])) ->
intern_pat scopes aliases tmp_scope a
| CPatNotation (loc, ntn, fullargs) ->
- let ntn,(args,argsl) = contract_pat_notation ntn fullargs in
+ let ntn,(args,argsl as fullargs) = contract_pat_notation ntn fullargs in
let (((ids',idsl'),c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
- Dumpglob.dump_notation_location (Topconstr.patntn_loc loc args ntn) df;
+ 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 =
@@ -680,9 +823,8 @@ let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat=
in ids@ids'', pl
| CPatPrim (loc, p) ->
let a = alias_of aliases in
- let (c,df) = Notation.interp_prim_token_cases_pattern loc p a
+ let (c,_) = Notation.interp_prim_token_cases_pattern loc p a
(tmp_scope,scopes) in
- Dumpglob.dump_notation_location (fst (unloc loc)) df;
(ids,[asubst,c])
| CPatDelimiters (loc, key, e) ->
intern_pat (find_delimiters_scope loc key::scopes) aliases None e
@@ -719,10 +861,10 @@ let check_capture loc ty = function
()
let locate_if_isevar loc na = function
- | RHole _ ->
+ | RHole _ ->
(try match na with
| Name id -> Reserve.find_reserved_type id
- | Anonymous -> raise Not_found
+ | Anonymous -> raise Not_found
with Not_found -> RHole (loc, Evd.BinderType na))
| x -> x
@@ -732,43 +874,44 @@ let check_hidden_implicit_parameters id (_,_,_,(indnames,_)) =
pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.")
let push_name_env ?(fail_anonymous=false) lvar (ids,unb,tmpsc,scopes as env) = function
- | Anonymous ->
+ | Anonymous ->
if fail_anonymous then errorlabstrm "" (str "Anonymous variables not allowed");
env
- | Name id ->
+ | Name id ->
check_hidden_implicit_parameters id lvar;
(Idset.add id ids, unb,tmpsc,scopes)
let push_loc_name_env ?(fail_anonymous=false) lvar (ids,unb,tmpsc,scopes as env) loc = function
- | Anonymous ->
+ | Anonymous ->
if fail_anonymous then user_err_loc (loc,"", str "Anonymous variables not allowed");
env
- | Name id ->
+ | Name id ->
check_hidden_implicit_parameters id lvar;
Dumpglob.dump_binding loc id;
(Idset.add id ids,unb,tmpsc,scopes)
let intern_generalized_binder ?(fail_anonymous=false) intern_type lvar
(ids,unb,tmpsc,sc as env) bl (loc, na) b b' t ty =
- let ty =
- if t then ty else
+ let ids = match na with Anonymous -> ids | Name na -> Idset.add na 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.free_vars_of_rawconstr ~bound:ids 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_loc_name_env ~fail_anonymous 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 na = match na with
- | Anonymous ->
- if fail_anonymous then na
+ | Anonymous ->
+ if fail_anonymous then na
else
- let name =
- let id =
+ let name =
+ let id =
match ty with
| CApp (_, (_, CRef (Ident (loc,id))), _) -> id
| _ -> id_of_string "H"
- in Implicit_quantifiers.make_fresh ids (Global.env ()) id
+ in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
in Name name
| _ -> na
in (push_loc_name_env ~fail_anonymous lvar env' loc na), (na,b',None,ty') :: List.rev bl
@@ -793,26 +936,26 @@ let intern_local_binder_aux ?(fail_anonymous=false) intern intern_type lvar ((id
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.free_vars_of_rawconstr ~bound:ids c in
- let env', c' =
- let abs =
- let pi =
+ let fvs = Implicit_quantifiers.generalizable_vars_of_rawconstr ~bound:ids c in
+ let env', c' =
+ let abs =
+ let pi =
match ak with
| Some AbsPi -> true
- | None when tmp_scope = Some Notation.type_scope
+ | None when tmp_scope = Some Notation.type_scope
|| List.mem Notation.type_scope scopes -> true
| _ -> false
- in
+ in
if pi then
(fun (id, loc') acc ->
RProd (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc))
else
- (fun (id, loc') acc ->
+ (fun (id, loc') acc ->
RLambda (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc))
in
- List.fold_right (fun (id, loc as lid) (env, acc) ->
+ List.fold_right (fun (id, loc as lid) (env, acc) ->
let env' = push_loc_name_env lvar env loc (Name id) in
- (env', abs lid acc)) fvs (env,c)
+ (env', abs lid acc)) fvs (env,c)
in c'
(**********************************************************************)
@@ -820,20 +963,20 @@ let intern_generalization intern (ids,unb,tmp_scope,scopes as env) lvar loc bk a
let merge_impargs l args =
List.fold_right (fun a l ->
- match a with
- | (_,Some (_,(ExplByName id as x))) when
+ match a with
+ | (_,Some (_,(ExplByName id as x))) when
List.exists (function (_,Some (_,y)) -> x=y | _ -> false) args -> l
| _ -> a::l)
- l args
+ l args
-let check_projection isproj nargs r =
+let check_projection isproj nargs r =
match (r,isproj) with
| RRef (loc, ref), Some _ ->
(try
let n = Recordops.find_projection_nparams ref + 1 in
if nargs <> n then
user_err_loc (loc,"",str "Projection has not the right number of explicit parameters.");
- with Not_found ->
+ 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.")
@@ -842,9 +985,9 @@ let check_projection isproj nargs r =
let get_implicit_name n imps =
Some (Impargs.name_of_implicit (List.nth imps (n-1)))
-let set_hole_implicit i = function
- | RRef (loc,r) -> (loc,Evd.ImplicitArg (r,i))
- | RVar (loc,id) -> (loc,Evd.ImplicitArg (VarRef id,i))
+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))
| _ -> anomaly "Only refs have implicits"
let exists_implicit_name id =
@@ -869,7 +1012,7 @@ let extract_explicit_arg imps args =
id
| ExplByPos (p,_id) ->
let id =
- try
+ try
let imp = List.nth imps (p-1) in
if not (is_status_implicit imp) then failwith "imp";
name_of_implicit imp
@@ -905,37 +1048,29 @@ let internalise sigma globalenv env allow_patvar lvar c =
in
let idl = Array.map
(fun (id,(n,order),bl,ty,bd) ->
- let intern_ro_arg c f =
- let idx =
- match n with
- Some (loc, n) -> list_index0 (Name n) (List.map snd (names_of_local_assums bl))
- | None -> 0
- in
+ let intern_ro_arg f =
+ let idx = Option.default 0 (index_of_annot bl n) in
let before, after = list_chop idx bl in
let ((ids',_,_,_) as env',rbefore) =
List.fold_left intern_local_binder (env,[]) before in
- let ro =
- match c with
- | None -> RStructRec
- | Some c' -> f (intern (ids', unb, tmp_scope, scopes) c')
- in
+ let ro = f (intern (ids', unb, tmp_scope, scopes)) in
let n' = Option.map (fun _ -> List.length before) n in
n', ro, List.fold_left intern_local_binder (env',rbefore) after
in
let n, ro, ((ids',_,_,_),rbl) =
- (match order with
- | CStructRec ->
- intern_ro_arg None (fun _ -> RStructRec)
- | CWfRec c ->
- intern_ro_arg (Some c) (fun r -> RWfRec r)
- | CMeasureRec c ->
- intern_ro_arg (Some c) (fun r -> RMeasureRec r))
+ match order with
+ | CStructRec ->
+ intern_ro_arg (fun _ -> RStructRec)
+ | CWfRec c ->
+ intern_ro_arg (fun f -> RWfRec (f c))
+ | CMeasureRec (m,r) ->
+ intern_ro_arg (fun f -> RMeasureRec (f m, Option.map f r))
in
let ids'' = List.fold_right Idset.add lf ids' in
- ((n, ro), List.rev rbl,
+ ((n, ro), List.rev rbl,
intern_type (ids',unb,tmp_scope,scopes) ty,
intern (ids'',unb,None,scopes) bd)) dl in
- RRec (loc,RFix
+ RRec (loc,RFix
(Array.map (fun (ro,_,_,_) -> ro) idl,n),
Array.of_list lf,
Array.map (fun (_,bl,_,_) -> bl) idl,
@@ -976,7 +1111,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
RLetIn (loc, na, intern (reset_tmp_scope env) c1,
intern (push_loc_name_env lvar env loc1 na) c2)
| CNotation (loc,"- _",([CPrim (_,Numeral p)],[]))
- when Bigint.is_strictly_pos p ->
+ when Bigint.is_strictly_pos p ->
intern env (CPrim (loc,Numeral (Bigint.neg p)))
| CNotation (_,"( _ )",([a],[])) -> intern env a
| CNotation (loc,ntn,args) ->
@@ -984,9 +1119,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
| CGeneralization (loc,b,a,c) ->
intern_generalization intern env lvar loc b a c
| CPrim (loc, p) ->
- let c,df = Notation.interp_prim_token loc p (tmp_scope,scopes) in
- Dumpglob.dump_notation_location (fst (unloc loc)) df;
- c
+ fst (Notation.interp_prim_token loc p (tmp_scope,scopes))
| CDelimiters (loc, key, e) ->
intern (ids,unb,None,find_delimiters_scope loc key::scopes) e
| CAppExpl (loc, (isproj,ref), args) ->
@@ -994,6 +1127,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
let args = List.map (fun a -> (a,None)) args in
intern_applied_reference intern env 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))
| CApp (loc, (isproj,f), args) ->
let isproj,f,args = match f with
@@ -1006,48 +1140,28 @@ let internalise sigma globalenv env allow_patvar lvar c =
| CRef ref -> intern_applied_reference intern env lvar args ref
| CNotation (loc,ntn,([],[])) ->
let c = intern_notation intern env loc ntn ([],[]) in
- find_appl_head_data lvar c, args
+ find_appl_head_data c, args
| x -> (intern env f,[],[],[]), args in
- let args =
+ let args =
intern_impargs c env impargs args_scopes (merge_impargs l args) in
check_projection isproj (List.length args) c;
- (match c with
+ (match c with
(* Now compact "(f args') args" *)
| RApp (loc', f', args') -> RApp (join_loc loc' loc, f',args'@args)
| _ -> RApp (loc, c, args))
- | CRecord (loc, w, fs) ->
- let id, _ = List.hd fs in
- let record =
- let (id,_,_,_),_ = intern_applied_reference intern env lvar [] (Ident id) in
- match id with
- | RRef (loc, ref) ->
- (try Recordops.find_projection ref
- with Not_found -> user_err_loc (loc, "intern", str"Not a projection"))
- | c -> user_err_loc (loc_of_rawconstr id, "intern", str"Not a projection")
- in
- let args =
- let pars = list_make record.Recordops.s_EXPECTEDPARAM (CHole (loc, None)) in
- let fields, rest =
- List.fold_left (fun (args, rest as acc) (na, b) ->
- if b then
- try
- let id = out_name na in
- let _, t = List.assoc id rest in
- t :: args, List.remove_assoc id rest
- with _ -> CHole (loc, Some (Evd.QuestionMark (Evd.Define true))) :: args, rest
- else acc) ([], List.map (fun ((loc, id), t) -> id, (loc, t)) fs) record.Recordops.s_PROJKIND
- in
- if rest <> [] then
- let id, (loc, t) = List.hd rest in
- user_err_loc (loc,"intern",(str "Unknown field name " ++ pr_id id))
- else pars @ List.rev fields
- in
- let constrname =
- Qualid (loc, shortest_qualid_of_global Idset.empty (ConstructRef record.Recordops.s_CONST))
- in
- let app = CAppExpl (loc, (None, constrname), args) in
+ | CRecord (loc, _, fs) ->
+ let cargs =
+ sort_fields true loc fs
+ (fun k l -> CHole (loc, Some (Evd.QuestionMark (Evd.Define true))) :: l)
+ in
+ begin
+ match cargs with
+ | None -> user_err_loc (loc, "intern", str"No constructor inference.")
+ | Some (n, constrname, args) ->
+ let pars = list_make n (CHole (loc, None)) in
+ let app = CAppExpl (loc, (None, constrname), List.rev_append pars args) in
intern env app
-
+ end
| CCases (loc, sty, rtnpo, tms, eqns) ->
let tms,env' = List.fold_right
(fun citm (inds,env) ->
@@ -1072,7 +1186,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
let env'' = List.fold_left (push_name_env lvar) env ids in
intern_type env'' p) po in
RIf (loc, c', (na', p'), intern env b1, intern env b2)
- | CHole (loc, k) ->
+ | CHole (loc, k) ->
RHole (loc, match k with Some k -> k | None -> Evd.QuestionMark (Evd.Define true))
| CPatVar (loc, n) when allow_patvar ->
RPatVar (loc, n)
@@ -1091,12 +1205,12 @@ let internalise sigma globalenv env allow_patvar lvar c =
and intern_type env = intern (set_type_scope env)
- and intern_local_binder env bind =
+ and intern_local_binder env bind =
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) =
- let idsl_pll =
+ let idsl_pll =
List.map (intern_cases_pattern globalenv scopes ([],[]) None) pl in
check_number_of_pattern loc n pl;
product_of_cases_patterns [] idsl_pll
@@ -1125,7 +1239,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
and intern_case_item (vars,unb,_,scopes as env) (tm,(na,t)) =
let tm' = intern env tm in
let ids,typ = match t with
- | Some t ->
+ | 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
@@ -1145,7 +1259,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
if List.exists ((<>) Anonymous) parnal then
error_inductive_parameter_not_implicit loc;
realnal, Some (loc,ind,nparams,realnal)
- | None ->
+ | None ->
[], None in
let na = match tm', na with
| RVar (_,id), None when Idset.mem id vars -> Name id
@@ -1153,7 +1267,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
| _, None -> Anonymous
| _, Some na -> na in
(tm',(na,typ)), na::ids
-
+
and iterate_prod loc2 env bk ty body nal =
let rec default env bk = function
| (loc1,na)::nal ->
@@ -1165,14 +1279,14 @@ let internalise sigma globalenv env allow_patvar lvar c =
in
match bk with
| Default b -> default env b nal
- | Generalized (b,b',t) ->
+ | 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
-
- and iterate_lam loc2 env bk ty body nal =
- let rec default env bk = function
+
+ and iterate_lam loc2 env bk ty body nal =
+ let rec default env bk = function
| (loc1,na)::nal ->
if nal <> [] then check_capture loc1 ty na;
let body = default (push_loc_name_env lvar env loc1 na) bk nal in
@@ -1181,19 +1295,19 @@ let internalise sigma globalenv env allow_patvar lvar c =
| [] -> intern env body
in match bk with
| Default b -> default env b nal
- | Generalized (b, b', t) ->
+ | 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
-
+
and intern_impargs c env l subscopes args =
let eargs, rargs = extract_explicit_arg l args in
let rec aux n impl subscopes eargs rargs =
let (enva,subscopes') = apply_scope_env env subscopes in
match (impl,rargs) with
| (imp::impl', rargs) when is_status_implicit imp ->
- begin try
+ begin try
let id = name_of_implicit imp in
let (_,a) = List.assoc id eargs in
let eargs' = List.remove_assoc id eargs in
@@ -1204,16 +1318,16 @@ let internalise 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) c) ::
+ RHole (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') ->
intern enva a :: aux (n+1) impl' subscopes' eargs rargs'
- | (imp::impl', []) ->
- if eargs <> [] then
+ | (imp::impl', []) ->
+ if eargs <> [] then
(let (id,(loc,_)) = List.hd eargs in
user_err_loc (loc,"",str "Not enough non implicit
- arguments to accept the argument bound to " ++
+ arguments to accept the argument bound to " ++
pr_id id ++ str"."));
[]
| ([], rargs) ->
@@ -1227,51 +1341,49 @@ let internalise sigma globalenv env allow_patvar lvar c =
let (enva,subscopes) = apply_scope_env env subscopes in
(intern enva a) :: (intern_args env subscopes args)
- in
- try
+ in
+ try
intern env c
with
InternalisationError (loc,e) ->
- user_err_loc (loc,"internalize",explain_internalisation_error e)
+ user_err_loc (loc,"internalize",
+ explain_internalisation_error e)
(**************************************************************************)
(* Functions to translate constr_expr into rawconstr *)
(**************************************************************************)
let extract_ids env =
- List.fold_right Idset.add
+ List.fold_right Idset.add
(Termops.ids_of_rel_context (Environ.rel_context env))
Idset.empty
let intern_gen isarity sigma env
?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
c =
- let tmp_scope =
+ let tmp_scope =
if isarity then Some Notation.type_scope else None in
internalise sigma env (extract_ids env, false, tmp_scope,[])
allow_patvar (ltacvars,Environ.named_context env, [], impls) 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_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 =
try
- intern_cases_pattern env [] ([],[]) None patt
- with
+ intern_cases_pattern env [] ([],[]) None patt
+ with
InternalisationError (loc,e) ->
user_err_loc (loc,"internalize",explain_internalisation_error e)
-let intern_ltac isarity ltacvars sigma env c =
- intern_gen isarity sigma env ~ltacvars:ltacvars c
-
-type manual_implicits = (explicitation * (bool * bool)) list
+type manual_implicits = (explicitation * (bool * bool * bool)) list
(*********************************************************************)
(* Functions to parse and interpret constructions *)
-let interp_gen kind sigma env
+let interp_gen kind sigma env
?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
c =
let c = intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars sigma env c in
@@ -1284,39 +1396,56 @@ let interp_type sigma env ?(impls=([],[])) c =
interp_gen IsType sigma env ~impls c
let interp_casted_constr sigma env ?(impls=([],[])) c typ =
- interp_gen (OfType (Some typ)) sigma env ~impls c
+ interp_gen (OfType (Some typ)) sigma env ~impls c
let interp_open_constr sigma env c =
Default.understand_tcc sigma env (intern_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 rec patvar_to_evar r = match r with
+ | RPatVar (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
+ evars := Gmap.add id rev !evars;
+ rev
+ )
+ | _ -> map_rawconstr patvar_to_evar r in
+ let raw = patvar_to_evar raw in
+ Default.understand_tcc !sigma env raw
+
let interp_constr_judgment sigma env c =
Default.understand_judgment sigma env (intern_constr sigma env c)
-let interp_constr_evars_gen_impls ?evdref
+let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true)
env ?(impls=([],[])) kind c =
- match evdref with
- | None ->
- let c = intern_gen (kind=IsType) ~impls Evd.empty env c in
- let imps = Implicit_quantifiers.implicits_of_rawterm c in
- Default.understand_gen kind Evd.empty env c, imps
- | Some evdref ->
- let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in
- let imps = Implicit_quantifiers.implicits_of_rawterm c in
- Default.understand_tcc_evars evdref env kind c, imps
+ let evdref =
+ match evdref with
+ | None -> ref Evd.empty
+ | Some evdref -> evdref
+ in
+ let c = intern_gen (kind=IsType) ~impls !evdref env c in
+ let imps = Implicit_quantifiers.implicits_of_rawterm c in
+ Default.understand_tcc_evars ~fail_evar evdref env kind c, imps
-let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c =
- let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in
- Default.understand_tcc_evars evdref env kind c
-
-let interp_casted_constr_evars_impls ?evdref
+let interp_casted_constr_evars_impls ?evdref ?(fail_evar=true)
env ?(impls=([],[])) c typ =
- interp_constr_evars_gen_impls ?evdref env ~impls (OfType (Some typ)) c
+ interp_constr_evars_gen_impls ?evdref ~fail_evar env ~impls (OfType (Some typ)) c
-let interp_type_evars_impls ?evdref env ?(impls=([],[])) c =
- interp_constr_evars_gen_impls ?evdref env IsType ~impls c
+let interp_type_evars_impls ?evdref ?(fail_evar=true) env ?(impls=([],[])) c =
+ interp_constr_evars_gen_impls ?evdref ~fail_evar env IsType ~impls c
-let interp_constr_evars_impls ?evdref env ?(impls=([],[])) c =
- interp_constr_evars_gen_impls ?evdref env (OfType None) ~impls c
+let interp_constr_evars_impls ?evdref ?(fail_evar=true) env ?(impls=([],[])) 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
+ Default.understand_tcc_evars evdref env kind c
let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ =
interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c
@@ -1324,27 +1453,23 @@ let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ =
let interp_type_evars evdref env ?(impls=([],[])) c =
interp_constr_evars_gen evdref env IsType ~impls c
-let interp_constr_judgment_evars evdref env c =
- Default.understand_judgment_tcc evdref env
- (intern_constr (Evd.evars_of !evdref) env 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
-let interp_aconstr impls (vars,varslist) a =
+let interp_aconstr ?(impls=([],[])) (vars,varslist) 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 -> (id,ref None)) (vars@varslist) in
let c = internalise Evd.empty (Global.env()) (extract_ids env, false, None, [])
- false (([],[]),Environ.named_context env,vl,([],impls)) a in
+ false (([],[]),Environ.named_context env,vl,impls) a in
(* Translate and check that [c] has all its free variables bound in [vars] *)
let a = aconstr_of_rawconstr vars c in
(* Returns [a] and the ordered list of variables with their scopes *)
(* Variables occurring in binders have no relevant scope since bound *)
- let vl = List.map (fun (id,r) ->
+ let vl = List.map (fun (id,r) ->
(id,match !r with None -> None,[] | Some (a,l) -> a,l)) vl in
list_chop (List.length vars) vl, a
@@ -1356,7 +1481,7 @@ let interp_binder sigma env na t =
Default.understand_type sigma env t'
let interp_binder_evars evdref env na t =
- let t = intern_gen true (Evd.evars_of !evdref) env t in
+ let t = intern_gen true !evdref env t in
let t' = locate_if_isevar (loc_of_rawconstr t) na t in
Default.understand_tcc_evars evdref env IsType t'
@@ -1374,7 +1499,7 @@ let intern_context fail_anonymous sigma env params =
(intern_local_binder_aux ~fail_anonymous (my_intern_constr sigma env lvar) (my_intern_type sigma env lvar) lvar)
((extract_ids env,false,None,[]), []) params)
-let interp_context_gen understand_type understand_judgment env bl =
+let interp_rawcontext_gen understand_type understand_judgment env bl =
let (env, par, _, impls) =
List.fold_left
(fun (env,params,n,impls) (na, k, b, t) ->
@@ -1383,10 +1508,10 @@ let interp_context_gen understand_type understand_judgment env bl =
let t' = locate_if_isevar (loc_of_rawconstr t) na t in
let t = understand_type env t' in
let d = (na,None,t) in
- let impls =
+ let impls =
if k = Implicit then
let na = match na with Name n -> Some n | Anonymous -> None in
- (ExplByPos (n, na), (true, true)) :: impls
+ (ExplByPos (n, na), (true, true, true)) :: impls
else impls
in
(push_rel d env, d::params, succ n, impls)
@@ -1397,42 +1522,15 @@ let interp_context_gen understand_type understand_judgment env bl =
(env,[],1,[]) (List.rev bl)
in (env, par), impls
-let interp_context ?(fail_anonymous=false) sigma env params =
+let interp_context_gen understand_type understand_judgment ?(fail_anonymous=false) sigma env params =
let bl = intern_context fail_anonymous sigma env params in
- interp_context_gen (Default.understand_type sigma)
- (Default.understand_judgment sigma) env bl
-
-let interp_context_evars ?(fail_anonymous=false) evdref env params =
- let bl = intern_context fail_anonymous (Evd.evars_of !evdref) env params in
- interp_context_gen (fun env t -> Default.understand_tcc_evars evdref env IsType t)
- (Default.understand_judgment_tcc evdref) env bl
-
-(**********************************************************************)
-(* Locating reference, possibly via an abbreviation *)
-
-let locate_reference qid =
- match Nametab.extended_locate qid with
- | TrueGlobal ref -> ref
- | SyntacticDef kn ->
- match Syntax_def.search_syntactic_definition dummy_loc kn with
- | [],ARef ref -> ref
- | _ -> raise Not_found
+ interp_rawcontext_gen understand_type understand_judgment env bl
-let is_global id =
- try
- let _ = locate_reference (make_short_qualid id) in true
- with Not_found ->
- false
-
-let global_reference id =
- constr_of_global (locate_reference (make_short_qualid id))
-
-let construct_reference ctx id =
- try
- Term.mkVar (let _ = Sign.lookup_named id ctx in id)
- with Not_found ->
- global_reference id
-
-let global_reference_in_absolute_module dir id =
- constr_of_global (Nametab.absolute_reference (Libnames.make_path dir id))
+let interp_context ?(fail_anonymous=false) sigma env params =
+ interp_context_gen (Default.understand_type sigma)
+ (Default.understand_judgment sigma) ~fail_anonymous sigma env params
+let interp_context_evars ?(fail_anonymous=false) evdref env params =
+ interp_context_gen (fun env t -> Default.understand_tcc_evars evdref env IsType t)
+ (Default.understand_judgment_tcc evdref) ~fail_anonymous !evdref env params
+
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index c5371255..5a62541d 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: constrintern.mli 11739 2009-01-02 19:33:19Z herbelin $ i*)
+(*i $Id$ i*)
(*i*)
open Names
@@ -33,21 +33,44 @@ open Pretyping
- insert existential variables for implicit arguments
*)
-(* To interpret implicits and arg scopes of recursive variables in
- inductive types and recursive definitions; mention of a list of
- implicits arguments in the ``rel'' part of [env]; the second
- argument associates a list of implicit positions and scopes to
- identifiers declared in the [rel_context] of [env] *)
+(* To interpret implicits and arg scopes of recursive variables while
+ internalizing inductive types and recursive definitions, and also
+ projection while typing records.
-type var_internalisation_type = Inductive | Recursive | Method
-
-type var_internalisation_data =
- var_internalisation_type * identifier list * Impargs.implicits_list * scope_name option list
+ the third and fourth arguments associate a list of implicit
+ positions and scopes to identifiers declared in the [rel_context]
+ of [env] *)
-type implicits_env = (identifier * var_internalisation_data) list
-type full_implicits_env = identifier list * implicits_env
+type var_internalization_type = Inductive | Recursive | Method
-type manual_implicits = (explicitation * (bool * bool)) list
+type var_internalization_data =
+ var_internalization_type *
+ identifier list *
+ Impargs.implicits_list *
+ scope_name option list
+
+(* A map of free variables to their implicit arguments and scopes *)
+type internalization_env =
+ (identifier * var_internalization_data) list
+
+(* Contains also a list of identifiers to automatically apply to the variables*)
+type full_internalization_env =
+ identifier list * internalization_env
+
+val empty_internalization_env : full_internalization_env
+
+val compute_internalization_data : env -> var_internalization_type ->
+ types -> Impargs.manual_explicitation list -> var_internalization_data
+
+val set_internalization_env_params :
+ internalization_env -> identifier list -> full_internalization_env
+
+val compute_full_internalization_env : env ->
+ var_internalization_type ->
+ identifier list -> identifier list -> types list ->
+ Impargs.manual_explicitation list list -> full_internalization_env
+
+type manual_implicits = (explicitation * (bool * bool * bool)) list
type ltac_sign = identifier list * unbound_ltac_var_map
@@ -60,7 +83,7 @@ val intern_constr : evar_map -> env -> constr_expr -> rawconstr
val intern_type : evar_map -> env -> constr_expr -> rawconstr
val intern_gen : bool -> evar_map -> env ->
- ?impls:full_implicits_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
+ ?impls:full_internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
constr_expr -> rawconstr
val intern_pattern : env -> cases_pattern_expr ->
@@ -69,42 +92,46 @@ val intern_pattern : env -> cases_pattern_expr ->
val intern_context : bool -> evar_map -> env -> local_binder list -> raw_binder list
-(*s Composing internalisation with pretyping *)
+(*s Composing internalization with pretyping *)
(* Main interpretation function *)
val interp_gen : typing_constraint -> evar_map -> env ->
- ?impls:full_implicits_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
+ ?impls:full_internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
constr_expr -> constr
(* Particular instances *)
-val interp_constr : evar_map -> env ->
+val interp_constr : evar_map -> env ->
constr_expr -> constr
-val interp_type : evar_map -> env -> ?impls:full_implicits_env ->
+val interp_type : evar_map -> env -> ?impls:full_internalization_env ->
constr_expr -> types
val interp_open_constr : evar_map -> env -> constr_expr -> evar_map * constr
-val interp_casted_constr : evar_map -> env -> ?impls:full_implicits_env ->
+val interp_open_constr_patvar : evar_map -> env -> constr_expr -> evar_map * constr
+
+val interp_casted_constr : evar_map -> env -> ?impls:full_internalization_env ->
constr_expr -> types -> constr
(* Accepting evars and giving back the manual implicits in addition. *)
-val interp_casted_constr_evars_impls : ?evdref:(evar_defs ref) -> env ->
- ?impls:full_implicits_env -> constr_expr -> types -> constr * manual_implicits
+val interp_casted_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env ->
+ ?impls:full_internalization_env -> constr_expr -> types -> constr * manual_implicits
-val interp_type_evars_impls : ?evdref:(evar_defs ref) -> env -> ?impls:full_implicits_env ->
+val interp_type_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool ->
+ env -> ?impls:full_internalization_env ->
constr_expr -> types * manual_implicits
-val interp_constr_evars_impls : ?evdref:(evar_defs ref) -> env -> ?impls:full_implicits_env ->
+val interp_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool ->
+ env -> ?impls:full_internalization_env ->
constr_expr -> constr * manual_implicits
-val interp_casted_constr_evars : evar_defs ref -> env ->
- ?impls:full_implicits_env -> constr_expr -> types -> constr
+val interp_casted_constr_evars : evar_map ref -> env ->
+ ?impls:full_internalization_env -> constr_expr -> types -> constr
-val interp_type_evars : evar_defs ref -> env -> ?impls:full_implicits_env ->
+val interp_type_evars : evar_map ref -> env -> ?impls:full_internalization_env ->
constr_expr -> types
(*s Build a judgment *)
@@ -113,29 +140,38 @@ val interp_constr_judgment : evar_map -> env -> constr_expr -> unsafe_judgment
(* Interprets constr patterns *)
-val intern_constr_pattern :
- evar_map -> env -> ?as_type:bool -> ?ltacvars:ltac_sign ->
+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 *)
+val intern_reference : reference -> global_reference
+
+(* Expands abbreviations (syndef); raise an error if not existing *)
val interp_reference : ltac_sign -> reference -> rawconstr
(* Interpret binders *)
val interp_binder : evar_map -> env -> name -> constr_expr -> types
-val interp_binder_evars : evar_defs ref -> env -> name -> constr_expr -> types
+val interp_binder_evars : evar_map ref -> env -> name -> constr_expr -> types
(* Interpret contexts: returns extended env and context *)
-val interp_context : ?fail_anonymous:bool ->
+val interp_context_gen : (env -> rawconstr -> types) ->
+ (env -> rawconstr -> unsafe_judgment) ->
+ ?fail_anonymous:bool ->
+ evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits
+
+val interp_context : ?fail_anonymous:bool ->
evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits
-val interp_context_evars : ?fail_anonymous:bool ->
- evar_defs ref -> env -> local_binder list -> (env * rel_context) * manual_implicits
+val interp_context_evars : ?fail_anonymous:bool ->
+ evar_map ref -> env -> local_binder list -> (env * rel_context) * manual_implicits
(* Locating references of constructions, possibly via a syntactic definition *)
+(* (these functions do not modify the glob file) *)
-val locate_reference : qualid -> global_reference
val is_global : identifier -> bool
val construct_reference : named_context -> identifier -> constr
val global_reference : identifier -> constr
@@ -143,8 +179,8 @@ val global_reference_in_absolute_module : dir_path -> identifier -> constr
(* Interprets into a abbreviatable constr *)
-val interp_aconstr : implicits_env -> identifier list * identifier list
- -> constr_expr -> interpretation
+val interp_aconstr : ?impls:full_internalization_env ->
+ identifier list * identifier list -> constr_expr -> interpretation
(* Globalization leak for Grammar *)
val for_grammar : ('a -> 'b) -> 'a -> 'b
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index ca758458..898369be 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqlib.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id$ *)
open Util
open Pp
@@ -15,6 +15,7 @@ open Term
open Libnames
open Pattern
open Nametab
+open Smartlocate
(************************************************************************)
(* Generic functions to find Coq objects *)
@@ -25,10 +26,8 @@ let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
let find_reference locstr dir s =
let sp = Libnames.make_path (make_dir dir) (id_of_string s) in
- try
- Nametab.absolute_reference sp
- with Not_found ->
- anomaly (locstr^": cannot find "^(string_of_path sp))
+ try global_of_extended_global (Nametab.extended_global_of_path sp)
+ with Not_found -> anomaly (locstr^": cannot find "^(string_of_path sp))
let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s
let coq_constant locstr dir s = constr_of_global (coq_reference locstr dir s)
@@ -37,25 +36,29 @@ let gen_reference = coq_reference
let gen_constant = coq_constant
let has_suffix_in_dirs dirs ref =
- let dir = dirpath (sp_of_global ref) in
+ let dir = dirpath (path_of_global ref) in
List.exists (fun d -> is_dirpath_prefix_of d dir) dirs
+let global_of_extended q =
+ try Some (global_of_extended_global q) with Not_found -> None
+
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_all (make_short_qualid id) in
+ let all = Nametab.locate_extended_all (qualid_of_ident id) 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
| [x] -> constr_of_global x
| [] ->
anomalylabstrm "" (str (locstr^": cannot find "^s^
" in module"^(if List.length dirs > 1 then "s " else " ")) ++
- prlist_with_sep pr_coma pr_dirpath dirs)
+ prlist_with_sep pr_comma pr_dirpath dirs)
| l ->
- anomalylabstrm ""
+ anomalylabstrm ""
(str (locstr^": found more than once object of name "^s^
" in module"^(if List.length dirs > 1 then "s " else " ")) ++
- prlist_with_sep pr_coma pr_dirpath dirs)
+ prlist_with_sep pr_comma pr_dirpath dirs)
(* For tactics/commands requiring vernacular libraries *)
@@ -63,21 +66,29 @@ let gen_constant_in_modules locstr dirs s =
let check_required_library d =
let d' = List.map id_of_string d in
let dir = make_dirpath (List.rev d') in
+ let mp = (fst(Lib.current_prefix())) in
+ let current_dir = match mp with
+ | MPfile dp -> (dir=dp)
+ | _ -> false
+ in
if not (Library.library_is_loaded dir) then
+ if not current_dir then
(* Loading silently ...
let m, prefix = list_sep_last d' in
- read_library
+ read_library
(dummy_loc,make_qualid (make_dirpath (List.rev prefix)) m)
*)
(* or failing ...*)
- error ("Library "^(string_of_dirpath dir)^" has to be required first.")
+ error ("Library "^(string_of_dirpath dir)^" has to be required first.")
(************************************************************************)
(* Specific Coq objects *)
let init_reference dir s = gen_reference "Coqlib" ("Init"::dir) s
-let init_constant dir s = gen_constant "Coqlib" ("Init"::dir) s
+let init_constant dir s = gen_constant "Coqlib" ("Init"::dir) s
+
+let logic_constant dir s = gen_constant "Coqlib" ("Logic"::dir) s
let arith_dir = ["Coq";"Arith"]
let arith_modules = [arith_dir]
@@ -96,7 +107,7 @@ let init_modules = [
init_dir@["Peano"];
init_dir@["Wf"]
]
-
+
let coq_id = id_of_string "Coq"
let init_id = id_of_string "Init"
let arith_id = id_of_string "Arith"
@@ -104,12 +115,21 @@ let datatypes_id = id_of_string "Datatypes"
let logic_module_name = ["Coq";"Init";"Logic"]
let logic_module = make_dir logic_module_name
-let logic_type_module = make_dir ["Coq";"Init";"Logic_Type"]
-let datatypes_module = make_dir ["Coq";"Init";"Datatypes"]
-let arith_module = make_dir ["Coq";"Arith";"Arith"]
+
+let logic_type_module_name = ["Coq";"Init";"Logic_Type"]
+let logic_type_module = make_dir logic_type_module_name
+
+let datatypes_module_name = ["Coq";"Init";"Datatypes"]
+let datatypes_module = make_dir datatypes_module_name
+
+let arith_module_name = ["Coq";"Arith";"Arith"]
+let arith_module = make_dir arith_module_name
+
+let jmeq_module_name = ["Coq";"Logic";"JMeq"]
+let jmeq_module = make_dir jmeq_module_name
(* TODO: temporary hack *)
-let make_kn dir id = Libnames.encode_kn dir id
+let make_kn dir id = Libnames.encode_mind dir id
let make_con dir id = Libnames.encode_con dir id
(** Identity *)
@@ -142,9 +162,14 @@ let glob_false = ConstructRef path_of_false
(** Equality *)
let eq_kn = make_kn logic_module (id_of_string "eq")
-
let glob_eq = IndRef (eq_kn,0)
+let identity_kn = make_kn datatypes_module (id_of_string "identity")
+let glob_identity = IndRef (identity_kn,0)
+
+let jmeq_kn = make_kn jmeq_module (id_of_string "JMeq")
+let glob_jmeq = IndRef (jmeq_kn,0)
+
type coq_sigma_data = {
proj1 : constr;
proj2 : constr;
@@ -159,7 +184,7 @@ type coq_bool_data = {
type 'a delayed = unit -> 'a
-let build_bool_type () =
+let build_bool_type () =
{ andb = init_constant ["Datatypes"] "andb";
andb_prop = init_constant ["Datatypes"] "andb_prop";
andb_true_intro = init_constant ["Datatypes"] "andb_true_intro" }
@@ -182,41 +207,93 @@ let build_prod () =
typ = init_constant ["Datatypes"] "prod" }
(* Equalities *)
-type coq_leibniz_eq_data = {
+type coq_eq_data = {
eq : constr;
- refl : constr;
ind : constr;
- rrec : constr option;
- rect : constr option;
- congr: constr;
- sym : constr }
+ refl : constr;
+ sym : constr;
+ trans: constr;
+ congr: constr }
+
+(* 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 *)
+}
let lazy_init_constant dir id = lazy (init_constant dir id)
+let lazy_logic_constant dir id = lazy (logic_constant dir id)
+
+(* Leibniz equality on Type *)
-(* Equality on Set *)
let coq_eq_eq = lazy_init_constant ["Logic"] "eq"
-let coq_eq_refl = lazy_init_constant ["Logic"] "refl_equal"
+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"] "sym_eq"
+let coq_eq_sym = lazy_init_constant ["Logic"] "eq_sym"
+let coq_eq_trans = lazy_init_constant ["Logic"] "eq_trans"
let coq_f_equal2 = lazy_init_constant ["Logic"] "f_equal2"
+let coq_eq_congr_canonical =
+ lazy_init_constant ["Logic"] "f_equal_canonical_form"
let build_coq_eq_data () =
let _ = check_required_library logic_module_name in {
eq = Lazy.force coq_eq_eq;
- refl = Lazy.force coq_eq_refl;
ind = Lazy.force coq_eq_ind;
- rrec = Some (Lazy.force coq_eq_rec);
- rect = Some (Lazy.force coq_eq_rect);
- congr = Lazy.force coq_eq_congr;
- sym = Lazy.force coq_eq_sym }
+ refl = Lazy.force coq_eq_refl;
+ sym = Lazy.force coq_eq_sym;
+ trans = Lazy.force coq_eq_trans;
+ congr = Lazy.force coq_eq_congr }
let build_coq_eq () = Lazy.force coq_eq_eq
-let build_coq_sym_eq () = Lazy.force coq_eq_sym
+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;
+ inv_ind = Lazy.force coq_eq_ind;
+ inv_congr = Lazy.force coq_eq_congr_canonical }
+
+(* Heterogenous equality on Type *)
+
+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"
+let coq_jmeq_congr_canonical =
+ lazy_logic_constant ["JMeq"] "JMeq_congr_canonical_form"
+
+let build_coq_jmeq_data () =
+ let _ = check_required_library jmeq_module_name in {
+ eq = Lazy.force coq_jmeq_eq;
+ ind = Lazy.force coq_jmeq_ind;
+ refl = Lazy.force coq_jmeq_refl;
+ sym = Lazy.force coq_jmeq_sym;
+ trans = Lazy.force coq_jmeq_trans;
+ congr = Lazy.force coq_jmeq_congr }
+
+let join_jmeq_types eq =
+ mkLambda(Name (id_of_string "A"),Termops.new_Type(),
+ mkLambda(Name (id_of_string "x"),mkRel 1,
+ mkApp (eq,[|mkRel 2;mkRel 1;mkRel 2|])))
+
+let build_coq_inversion_jmeq_data () =
+ let _ = check_required_library logic_module_name in {
+ inv_eq = join_jmeq_types (Lazy.force coq_jmeq_eq);
+ inv_ind = Lazy.force coq_jmeq_ind;
+ inv_congr = Lazy.force coq_jmeq_congr_canonical }
+
(* Specif *)
let coq_sumbool = lazy_init_constant ["Specif"] "sumbool"
@@ -228,17 +305,38 @@ let coq_identity_refl = lazy_init_constant ["Datatypes"] "refl_identity"
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"] "congr_id"
-let coq_identity_sym = lazy_init_constant ["Logic_Type"] "sym_id"
+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"
+let coq_identity_congr_canonical = lazy_init_constant ["Logic_Type"] "identity_congr_canonical_form"
-let build_coq_identity_data () = {
+let build_coq_identity_data () =
+ let _ = check_required_library datatypes_module_name in {
eq = Lazy.force coq_identity_eq;
- refl = Lazy.force coq_identity_refl;
ind = Lazy.force coq_identity_ind;
- rrec = Some (Lazy.force coq_identity_rec);
- rect = Some (Lazy.force coq_identity_rect);
- congr = Lazy.force coq_identity_congr;
- sym = Lazy.force coq_identity_sym }
+ refl = Lazy.force coq_identity_refl;
+ sym = Lazy.force coq_identity_sym;
+ trans = Lazy.force coq_identity_trans;
+ congr = Lazy.force coq_identity_congr }
+
+let build_coq_inversion_identity_data () =
+ let _ = check_required_library datatypes_module_name in
+ let _ = check_required_library logic_type_module_name in {
+ inv_eq = Lazy.force coq_identity_eq;
+ inv_ind = Lazy.force coq_identity_ind;
+ inv_congr = Lazy.force coq_identity_congr_canonical }
+
+(* Equality to true *)
+let coq_eq_true_eq = lazy_init_constant ["Datatypes"] "eq_true"
+let coq_eq_true_ind = lazy_init_constant ["Datatypes"] "eq_true_ind"
+let coq_eq_true_congr = lazy_init_constant ["Logic"] "eq_true_congr"
+
+let build_coq_inversion_eq_true_data () =
+ let _ = check_required_library datatypes_module_name in
+ let _ = check_required_library logic_module_name in {
+ inv_eq = Lazy.force coq_eq_true_eq;
+ inv_ind = Lazy.force coq_eq_true_ind;
+ inv_congr = Lazy.force coq_eq_true_congr }
(* The False proposition *)
let coq_False = lazy_init_constant ["Logic"] "False"
@@ -253,6 +351,10 @@ let coq_and = lazy_init_constant ["Logic"] "and"
let coq_conj = lazy_init_constant ["Logic"] "conj"
let coq_or = lazy_init_constant ["Logic"] "or"
let coq_ex = lazy_init_constant ["Logic"] "ex"
+let coq_iff = lazy_init_constant ["Logic"] "iff"
+
+let coq_iff_left_proj = lazy_init_constant ["Logic"] "proj1"
+let coq_iff_right_proj = lazy_init_constant ["Logic"] "proj2"
(* Runtime part *)
let build_coq_True () = Lazy.force coq_True
@@ -262,12 +364,19 @@ let build_coq_False () = Lazy.force coq_False
let build_coq_not () = Lazy.force coq_not
let build_coq_and () = Lazy.force coq_and
let build_coq_conj () = Lazy.force coq_conj
-let build_coq_or () = Lazy.force coq_or
-let build_coq_ex () = Lazy.force coq_ex
+let build_coq_or () = Lazy.force coq_or
+let build_coq_ex () = Lazy.force coq_ex
+let build_coq_iff () = Lazy.force coq_iff
+
+let build_coq_iff_left_proj () = Lazy.force coq_iff_left_proj
+let build_coq_iff_right_proj () = Lazy.force coq_iff_right_proj
+
(* The following is less readable but does not depend on parsing *)
let coq_eq_ref = lazy (init_reference ["Logic"] "eq")
-let coq_identity_ref = lazy (init_reference ["Datatypes"] "identity")
+let coq_identity_ref = lazy (init_reference ["Datatypes"] "identity")
+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_not_ref = lazy (init_reference ["Logic"] "not")
@@ -275,4 +384,5 @@ let coq_False_ref = lazy (init_reference ["Logic"] "False")
let coq_sumbool_ref = lazy (init_reference ["Specif"] "sumbool")
let coq_sig_ref = lazy (init_reference ["Specif"] "sig")
let coq_or_ref = lazy (init_reference ["Logic"] "or")
+let coq_iff_ref = lazy (init_reference ["Logic"] "iff")
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index a85b6a8e..6bb79c8b 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: coqlib.mli 10180 2007-10-05 13:02:23Z vsiles $ i*)
+(*i $Id$ i*)
(*i*)
open Names
@@ -58,8 +58,11 @@ val check_required_library : string list -> unit
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 *)
-val nat_path : section_path
+val nat_path : full_path
val glob_nat : global_reference
val path_of_O : constructor
val path_of_S : constructor
@@ -76,6 +79,8 @@ val glob_false : global_reference
(* 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
at compile time. Therefore, we can only provide methods to build
@@ -104,22 +109,36 @@ val build_sigma_type : coq_sigma_data delayed
(* Non-dependent pairs in Set from Datatypes *)
val build_prod : coq_sigma_data delayed
-type coq_leibniz_eq_data = {
+type coq_eq_data = {
eq : constr;
- refl : constr;
ind : constr;
- rrec : constr option;
- rect : constr option;
- congr: constr;
- sym : constr }
+ refl : constr;
+ sym : constr;
+ trans: constr;
+ congr: constr }
-val build_coq_eq_data : coq_leibniz_eq_data delayed
-val build_coq_identity_data : coq_leibniz_eq_data delayed
+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_sym_eq : constr delayed (* = [(build_coq_eq_data()).sym] *)
+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 *)
+
+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 *)
+}
+
+val build_coq_inversion_eq_data : coq_inversion_data delayed
+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 *)
val build_coq_sumbool : constr delayed
@@ -137,6 +156,10 @@ val build_coq_not : constr delayed
(* Conjunction *)
val build_coq_and : constr delayed
val build_coq_conj : constr delayed
+val build_coq_iff : constr delayed
+
+val build_coq_iff_left_proj : constr delayed
+val build_coq_iff_right_proj : constr delayed
(* Disjunction *)
val build_coq_or : constr delayed
@@ -146,6 +169,8 @@ val build_coq_ex : constr delayed
val coq_eq_ref : global_reference lazy_t
val coq_identity_ref : global_reference lazy_t
+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_not_ref : global_reference lazy_t
@@ -154,3 +179,4 @@ val coq_sumbool_ref : global_reference lazy_t
val coq_sig_ref : global_reference lazy_t
val coq_or_ref : global_reference lazy_t
+val coq_iff_ref : global_reference lazy_t
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 5ac584a7..702c509d 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: dumpglob.ml 11582 2008-11-12 19:49:57Z notin $ *)
+(* $Id$ *)
(* Dump of globalization (to be used by coqdoc) *)
@@ -15,11 +15,11 @@ let glob_file = ref Pervasives.stdout
let open_glob_file f =
glob_file := Pervasives.open_out f
-
+
let close_glob_file () =
Pervasives.close_out !glob_file
-type glob_output_t =
+type glob_output_t =
| NoGlob
| StdOut
| MultFiles
@@ -39,7 +39,7 @@ let dump_to_dotglob f = glob_output := MultFiles
let dump_into_file f = glob_output := File f; open_glob_file f
-let dump_string s =
+let dump_string s =
if dump () then Pervasives.output_string !glob_file s
@@ -47,28 +47,15 @@ let previous_state = ref MultFiles
let pause () = previous_state := !glob_output; glob_output := NoGlob
let continue () = glob_output := !previous_state
+type coqdoc_state = Lexer.location_table
-let token_number = ref 0
-let last_pos = ref 0
-
-type coqdoc_state = Lexer.location_table * int * int
-
-let coqdoc_freeze () =
- let lt = Lexer.location_table() in
- let state = (lt,!token_number,!last_pos) in
- token_number := 0;
- last_pos := 0;
- state
-
-let coqdoc_unfreeze (lt,tn,lp) =
- Lexer.restore_location_table lt;
- token_number := tn;
- last_pos := lp
+let coqdoc_freeze = Lexer.location_table
+let coqdoc_unfreeze = Lexer.restore_location_table
open Decl_kinds
let type_of_logical_kind = function
- | IsDefinition def ->
+ | IsDefinition def ->
(match def with
| Definition -> "def"
| Coercion -> "coe"
@@ -102,7 +89,7 @@ let type_of_global_ref gr =
"class"
else
match gr with
- | Libnames.ConstRef cst ->
+ | Libnames.ConstRef cst ->
type_of_logical_kind (Decls.constant_kind cst)
| Libnames.VarRef v ->
"var" ^ type_of_logical_kind (Decls.variable_kind v)
@@ -118,13 +105,13 @@ let type_of_global_ref gr =
let remove_sections dir =
if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then
(* Not yet (fully) discharged *)
- Libnames.extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ())
+ Libnames.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ())
else
(* Theorem/Lemma outside its outer section of definition *)
dir
let dump_ref loc filepath modpath ident ty =
- dump_string (Printf.sprintf "R%d %s %s %s %s\n"
+ dump_string (Printf.sprintf "R%d %s %s %s %s\n"
(fst (Util.unloc loc)) filepath modpath ident ty)
let add_glob_gen loc sp lib_dp ty =
@@ -137,41 +124,31 @@ let add_glob_gen loc sp lib_dp ty =
let ident = Names.string_of_id id in
dump_ref loc filepath modpath ident ty
-let add_glob loc ref =
+let add_glob loc ref =
if dump () && loc <> Util.dummy_loc then
- let sp = Nametab.sp_of_global ref in
+ let sp = Nametab.path_of_global ref in
let lib_dp = Lib.library_part ref in
let ty = type_of_global_ref ref in
add_glob_gen loc sp lib_dp ty
-
-let mp_of_kn kn =
- let mp,sec,l = Names.repr_kn kn in
- Names.MPdot (mp,l)
+
+let mp_of_kn kn =
+ let mp,sec,l = Names.repr_kn kn in
+ Names.MPdot (mp,l)
let add_glob_kn loc kn =
if dump () && loc <> Util.dummy_loc then
- let sp = Nametab.sp_of_syntactic_definition kn in
+ let sp = Nametab.path_of_syndef kn in
let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in
add_glob_gen loc sp lib_dp "syndef"
-let add_local loc id = ()
-(* let mod_dp,id = repr_path sp in *)
-(* let mod_dp = remove_sections mod_dp in *)
-(* let mod_dp_trunc = drop_dirpath_prefix lib_dp mod_dp in *)
-(* let filepath = string_of_dirpath lib_dp in *)
-(* let modpath = string_of_dirpath mod_dp_trunc in *)
-(* let ident = string_of_id id in *)
-(* dump_string (Printf.sprintf "R%d %s %s %s %s\n" *)
-(* (fst (unloc loc)) filepath modpath ident ty) *)
-
let dump_binding loc id = ()
-
+
let dump_definition (loc, id) sec s =
- dump_string (Printf.sprintf "%s %d %s %s\n" s (fst (Util.unloc loc))
+ dump_string (Printf.sprintf "%s %d %s %s\n" s (fst (Util.unloc loc))
(Names.string_of_dirpath (Lib.current_dirpath sec)) (Names.string_of_id id))
-
+
let dump_reference loc modpath ident ty =
- dump_string (Printf.sprintf "R%d %s %s %s %s\n"
+ dump_string (Printf.sprintf "R%d %s %s %s %s\n"
(fst (Util.unloc loc)) (Names.string_of_dirpath (Lib.library_dp ())) modpath ident ty)
let dump_constraint ((loc, n), _, _) sec ty =
@@ -187,7 +164,7 @@ let dump_name (loc, n) sec ty =
let dump_local_binder b sec ty =
if dump () then
match b with
- | Topconstr.LocalRawAssum (nl, _, _) ->
+ | Topconstr.LocalRawAssum (nl, _, _) ->
List.iter (fun x -> dump_name x sec ty) nl
| Topconstr.LocalRawDef _ -> ()
@@ -197,7 +174,7 @@ let dump_modref loc mp ty =
let l = if l = [] then l else Util.list_drop_last l in
let fp = Names.string_of_dirpath dp in
let mp = Names.string_of_dirpath (Names.make_dirpath l) in
- dump_string (Printf.sprintf "R%d %s %s %s %s\n"
+ dump_string (Printf.sprintf "R%d %s %s %s %s\n"
(fst (Util.unloc loc)) fp mp "<>" ty)
let dump_moddef loc mp ty =
@@ -207,22 +184,33 @@ let dump_moddef loc mp ty =
dump_string (Printf.sprintf "%s %d %s %s\n" ty (fst (Util.unloc loc)) "<>" mp)
let dump_libref loc dp ty =
- dump_string (Printf.sprintf "R%d %s <> <> %s\n"
+ dump_string (Printf.sprintf "R%d %s <> <> %s\n"
(fst (Util.unloc loc)) (Names.string_of_dirpath dp) ty)
-let dump_notation_location pos ((path,df),sc) =
+let cook_notation df sc =
+ let ntn = String.make (String.length df * 3) '_' in
+ let j = ref 0 in
+ let quoted = ref false in
+ for i = 0 to String.length df - 1 do
+ if df.[i] = '\'' then quoted := not !quoted;
+ if df.[i] = ' ' then (ntn.[!j] <- '_'; incr j) else
+ if df.[i] = '_' && not !quoted then (ntn.[!j] <- 'x'; incr j) else
+ if df.[i] = 'x' && not !quoted then (String.blit "'x'" 0 ntn !j 3; j := !j + 3) else
+ (ntn.[!j] <- df.[i]; incr j)
+ done;
+ let df = String.sub ntn 0 !j in
+ match sc with Some sc -> ":" ^ sc ^ ":" ^ df | _ -> "::" ^ df
+
+let dump_notation (loc,(df,_)) sc sec =
+ (* We dump the location of the opening '"' *)
+ dump_string (Printf.sprintf "not %d %s %s\n" (fst (Util.unloc loc))
+ (Names.string_of_dirpath (Lib.current_dirpath sec)) (cook_notation df sc))
+
+let dump_notation_location posl df (((path,secpath),_),sc) =
if dump () then
- let rec next growing =
- let loc = Lexer.location_function !token_number in
- let (bp,_) = Util.unloc loc in
- if growing then if bp >= pos then loc else (incr token_number; next true)
- else if bp = pos then loc
- else if bp > pos then (decr token_number;next false)
- else (incr token_number;next true) in
- let loc = next (pos >= !last_pos) in
- last_pos := pos;
- let path = Names.string_of_dirpath path in
- let _sc = match sc with Some sc -> " "^sc | _ -> "" in
- dump_string (Printf.sprintf "R%d %s \"%s\" not\n" (fst (Util.unloc loc)) path df)
-
-
+ let path = Names.string_of_dirpath path in
+ let secpath = Names.string_of_dirpath secpath in
+ let df = cook_notation df sc in
+ List.iter (fun (bl,el) ->
+ dump_string(Printf.sprintf "R%d:%d %s %s %s not\n" bl el path secpath df))
+ posl
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index a0666c81..f6d7baef 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: dumpglob.mli 11582 2008-11-12 19:49:57Z notin $ *)
+(* $Id$ *)
val open_glob_file : string -> unit
@@ -23,8 +23,9 @@ val dump_to_dotglob : unit -> unit
val pause : unit -> unit
val continue : unit -> unit
-val coqdoc_freeze : unit -> Lexer.location_table * int * int
-val coqdoc_unfreeze : Lexer.location_table * int * int -> unit
+type coqdoc_state = Lexer.location_table
+val coqdoc_freeze : unit -> coqdoc_state
+val coqdoc_unfreeze : coqdoc_state -> unit
val add_glob : Util.loc -> Libnames.global_reference -> unit
val add_glob_kn : Util.loc -> Names.kernel_name -> unit
@@ -34,8 +35,9 @@ val dump_moddef : Util.loc -> Names.module_path -> string -> unit
val dump_modref : Util.loc -> Names.module_path -> string -> unit
val dump_reference : Util.loc -> string -> string -> string -> unit
val dump_libref : Util.loc -> Names.dir_path -> string -> unit
-val dump_notation_location : int -> (Notation.notation_location * Topconstr.scope_name option) -> unit
+val dump_notation_location : (int * int) list -> Topconstr.notation -> (Notation.notation_location * Topconstr.scope_name option) -> unit
val dump_binding : Util.loc -> Names.Idset.elt -> unit
+val dump_notation : Util.loc * (Topconstr.notation * Notation.notation_location) -> Topconstr.scope_name option -> bool -> unit
val dump_constraint : Topconstr.typeclass_constraint -> bool -> string -> unit
val dump_local_binder : Topconstr.local_binder -> bool -> string -> unit
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 1da428be..c9ba20e6 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: genarg.ml 11481 2008-10-20 19:23:51Z herbelin $ *)
+(* $Id$ *)
open Pp
open Util
@@ -47,12 +47,18 @@ type argument_type =
type 'a and_short_name = 'a * identifier located option
type 'a or_by_notation =
| AN of 'a
- | ByNotation of loc * string * Notation.delimiters option
+ | ByNotation of (loc * string * Notation.delimiters option)
+
+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 open_constr_expr = unit * constr_expr
type open_rawconstr = unit * rawconstr_and_expr
+type rawconstr_pattern_and_expr = rawconstr_and_expr * Pattern.constr_pattern
+
type 'a with_ebindings = 'a * open_constr bindings
(* Dynamics but tagged by a type expression *)
@@ -61,9 +67,9 @@ type 'a generic_argument = argument_type * Obj.t
let dyntab = ref ([] : string list)
-type rlevel = constr_expr
-type glevel = rawconstr_and_expr
-type tlevel = open_constr
+type rlevel
+type glevel
+type tlevel
type ('a,'b) abstract_argument_type = argument_type
@@ -82,6 +88,7 @@ type intro_pattern_expr =
| IntroRewrite of bool
| IntroIdentifier of identifier
| IntroFresh of identifier
+ | IntroForthcoming of bool
| IntroAnonymous
and or_and_intro_pattern_expr = (loc * intro_pattern_expr) list list
@@ -92,11 +99,13 @@ let rec pr_intro_pattern (_,pat) = match pat with
| IntroRewrite false -> str "<-"
| IntroIdentifier id -> pr_id id
| IntroFresh id -> str "?" ++ pr_id id
+ | IntroForthcoming true -> str "*"
+ | IntroForthcoming false -> str "**"
| IntroAnonymous -> str "?"
and pr_or_and_intro_pattern = function
| [pl] ->
- str "(" ++ hv 0 (prlist_with_sep pr_coma pr_intro_pattern pl) ++ str ")"
+ str "(" ++ hv 0 (prlist_with_sep pr_comma pr_intro_pattern pl) ++ str ")"
| pll ->
str "[" ++
hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll)
@@ -163,7 +172,7 @@ let globwit_constr_may_eval = ConstrMayEvalArgType
let wit_constr_may_eval = ConstrMayEvalArgType
let rawwit_open_constr_gen b = OpenConstrArgType b
-let globwit_open_constr_gen b = OpenConstrArgType b
+let globwit_open_constr_gen b = OpenConstrArgType b
let wit_open_constr_gen b = OpenConstrArgType b
let rawwit_open_constr = rawwit_open_constr_gen false
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 86b19de7..fab5ff33 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -6,13 +6,14 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: genarg.mli 11481 2008-10-20 19:23:51Z herbelin $ i*)
+(*i $Id$ i*)
open Util
open Names
open Term
open Libnames
open Rawterm
+open Pattern
open Topconstr
open Term
open Evd
@@ -21,7 +22,9 @@ type 'a and_short_name = 'a * identifier located option
type 'a or_by_notation =
| AN of 'a
- | ByNotation of loc * string * Notation.delimiters option
+ | ByNotation of (loc * string * Notation.delimiters option)
+
+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 *)
@@ -31,6 +34,8 @@ type rawconstr_and_expr = rawconstr * constr_expr option
type open_constr_expr = unit * constr_expr
type open_rawconstr = unit * rawconstr_and_expr
+type rawconstr_pattern_and_expr = rawconstr_and_expr * constr_pattern
+
type 'a with_ebindings = 'a * open_constr bindings
type intro_pattern_expr =
@@ -39,6 +44,7 @@ type intro_pattern_expr =
| IntroRewrite of bool
| IntroIdentifier of identifier
| IntroFresh of identifier
+ | IntroForthcoming of bool
| IntroAnonymous
and or_and_intro_pattern_expr = (loc * intro_pattern_expr) list list
@@ -72,7 +78,7 @@ val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds
effective use
\end{verbatim}
-To distinguish between the uninterpreted (raw), globalized and
+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
[constr].
@@ -104,16 +110,16 @@ ExtraArgType of string '_a '_b
\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
- out_gen is monomorphic over 'a, hence type-safe
+ out_gen is monomorphic over 'a, hence type-safe
*)
-type rlevel = constr_expr
-type glevel = rawconstr_and_expr
-type tlevel = open_constr
+type rlevel
+type glevel
+type tlevel
type ('a,'co) abstract_argument_type
@@ -174,8 +180,8 @@ val rawwit_constr : (constr_expr,rlevel) abstract_argument_type
val globwit_constr : (rawconstr_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) may_eval,rlevel) abstract_argument_type
-val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) may_eval,glevel) 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 wit_constr_may_eval : (constr,tlevel) abstract_argument_type
val rawwit_open_constr_gen : bool -> (open_constr_expr,rlevel) abstract_argument_type
@@ -192,15 +198,15 @@ 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 wit_constr_with_bindings : (constr with_ebindings,tlevel) 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 wit_bindings : (open_constr bindings,tlevel) abstract_argument_type
+val wit_bindings : (constr bindings sigma,tlevel) abstract_argument_type
-val rawwit_red_expr : ((constr_expr,reference or_by_notation) red_expr_gen,rlevel) abstract_argument_type
-val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) red_expr_gen,glevel) abstract_argument_type
-val wit_red_expr : ((constr,evaluable_global_reference) red_expr_gen,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 wit_red_expr : ((constr,evaluable_global_reference,constr_pattern) red_expr_gen,tlevel) abstract_argument_type
val wit_list0 :
('a,'co) abstract_argument_type -> ('a list,'co) abstract_argument_type
@@ -219,29 +225,29 @@ val wit_pair :
(* ['a generic_argument] = (Sigma t:type. t[[constr/'a]]) *)
type 'a generic_argument
-val fold_list0 :
+val fold_list0 :
('a generic_argument -> 'c -> 'c) -> 'a generic_argument -> 'c -> 'c
-val fold_list1 :
+val fold_list1 :
('a generic_argument -> 'c -> 'c) -> 'a generic_argument -> 'c -> 'c
val fold_opt :
('a generic_argument -> 'c) -> 'c -> 'a generic_argument -> 'c
val fold_pair :
- ('a generic_argument -> 'a generic_argument -> 'c) ->
+ ('a generic_argument -> 'a generic_argument -> 'c) ->
'a generic_argument -> 'c
(* [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) ->
+val app_list0 : ('a generic_argument -> 'b generic_argument) ->
'a generic_argument -> 'b generic_argument
-val app_list1 : ('a generic_argument -> 'b generic_argument) ->
+val app_list1 : ('a generic_argument -> 'b generic_argument) ->
'a generic_argument -> 'b generic_argument
-val app_opt : ('a generic_argument -> 'b generic_argument) ->
+val app_opt : ('a generic_argument -> 'b generic_argument) ->
'a generic_argument -> 'b generic_argument
val app_pair :
@@ -291,7 +297,7 @@ val unquote : ('a,'co) abstract_argument_type -> argument_type
val in_gen :
('a,'co) abstract_argument_type -> 'a -> 'co generic_argument
val out_gen :
- ('a,'co) abstract_argument_type -> 'co generic_argument -> 'a
+ ('a,'co) abstract_argument_type -> 'co generic_argument -> 'a
(* [in_generic] is used in combination with camlp4 [Gramext.action] magic
@@ -305,5 +311,5 @@ val out_gen :
*)
type an_arg_of_this_type
-val in_generic :
+val in_generic :
argument_type -> an_arg_of_this_type -> 'co generic_argument
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index d6e207f3..d5894b20 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: implicit_quantifiers.ml 11576 2008-11-10 19:13:15Z msozeau $ i*)
+(*i $Id$ i*)
(*i*)
open Names
@@ -24,20 +24,65 @@ open Libnames
open Typeclasses
open Typeclasses_errors
open Pp
+open Libobject
+open Nameops
(*i*)
-let ids_of_list l =
+let generalizable_table = ref Idpred.empty
+
+let _ =
+ Summary.declare_summary "generalizable-ident"
+ { Summary.freeze_function = (fun () -> !generalizable_table);
+ Summary.unfreeze_function = (fun r -> generalizable_table := r);
+ Summary.init_function = (fun () -> generalizable_table := Idpred.empty) }
+
+let declare_generalizable_ident table (loc,id) =
+ if id <> root_of_id id then
+ user_err_loc(loc,"declare_generalizable_ident",
+ (pr_id id ++ str
+ " is not declarable as generalizable identifier: it must have no trailing digits, quote, or _"));
+ if Idpred.mem id table then
+ user_err_loc(loc,"declare_generalizable_ident",
+ (pr_id id++str" is already declared as a generalizable identifier"))
+ else Idpred.add id table
+
+let add_generalizable gen table =
+ match gen with
+ | None -> Idpred.empty
+ | Some [] -> Idpred.full
+ | Some l -> List.fold_left (fun table lid -> declare_generalizable_ident table lid)
+ table l
+
+let cache_generalizable_type (_,(local,cmd)) =
+ generalizable_table := add_generalizable cmd !generalizable_table
+
+let load_generalizable_type _ (_,(local,cmd)) =
+ generalizable_table := add_generalizable cmd !generalizable_table
+
+let (in_generalizable, _) =
+ 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))
+
+let find_generalizable_ident id = Idpred.mem (root_of_id id) !generalizable_table
+
+let ids_of_list l =
List.fold_right Idset.add l Idset.empty
let locate_reference qid =
- match Nametab.extended_locate qid with
+ match Nametab.locate_extended qid with
| TrueGlobal ref -> true
- | SyntacticDef kn -> true
+ | SynDef kn -> true
let is_global id =
- try
- locate_reference (make_short_qualid id)
- with Not_found ->
+ try
+ locate_reference (qualid_of_ident id)
+ with Not_found ->
false
let is_freevar ids env x =
@@ -48,122 +93,130 @@ let is_freevar ids env x =
with _ -> not (is_global x)
with _ -> true
-(* Auxilliary functions for the inference of implicitly quantified variables. *)
+(* Auxilliary functions for the inference of implicitly quantified variables. *)
-let free_vars_of_constr_expr c ?(bound=Idset.empty) l =
- let found id bdvars l =
- if List.mem id l then l
- else if not (is_freevar bdvars (Global.env ()) id)
- then l else id :: l
+let ungeneralizable loc id =
+ user_err_loc (loc, "Generalization",
+ str "Unbound and ungeneralizable variable " ++ pr_id id)
+
+let free_vars_of_constr_expr c ?(bound=Idset.empty) l =
+ let found loc id bdvars l =
+ if List.mem id l then l
+ else if is_freevar bdvars (Global.env ()) id
+ then
+ if find_generalizable_ident id then id :: l
+ else ungeneralizable loc id
+ else l
in
let rec aux bdvars l c = match c with
- | CRef (Ident (_,id)) -> found id bdvars l
+ | CRef (Ident (loc,id)) -> found loc id bdvars l
| CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id)) :: _, [])) when not (Idset.mem id bdvars) ->
fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c
| c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c
in aux bound l c
-let ids_of_names l =
+let ids_of_names l =
List.fold_left (fun acc x -> match snd x with Name na -> na :: acc | Anonymous -> acc) [] l
-let free_vars_of_binders ?(bound=Idset.empty) l (binders : local_binder list) =
+let free_vars_of_binders ?(bound=Idset.empty) l (binders : local_binder list) =
let rec aux bdvars l c = match c with
((LocalRawAssum (n, _, c)) :: tl) ->
let bound = ids_of_names n in
let l' = free_vars_of_constr_expr c ~bound:bdvars l in
aux (Idset.union (ids_of_list bound) bdvars) l' tl
- | ((LocalRawDef (n, c)) :: tl) ->
+ | ((LocalRawDef (n, c)) :: tl) ->
let bound = match snd n with Anonymous -> [] | Name n -> [n] in
let l' = free_vars_of_constr_expr c ~bound:bdvars l in
aux (Idset.union (ids_of_list bound) bdvars) l' tl
-
+
| [] -> bdvars, l
in aux bound l binders
-let add_name_to_ids set na =
- match na with
- | Anonymous -> set
- | Name id -> Idset.add id set
-
-let free_vars_of_rawconstr ?(bound=Idset.empty) =
+let add_name_to_ids set na =
+ match na with
+ | Anonymous -> set
+ | Name id -> Idset.add id set
+
+let generalizable_vars_of_rawconstr ?(bound=Idset.empty) ?(allowed=Idset.empty) =
let rec vars bound vs = function
- | RVar (loc,id) ->
+ | RVar (loc,id) ->
if is_freevar bound (Global.env ()) id then
- if List.mem_assoc id vs then vs
+ 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) ->
- let vs' = vars bound vs ty in
- let bound' = add_name_to_ids bound na in
+ | RLambda (loc,na,_,ty,c) | RProd (loc,na,_,ty,c) | RLetIn (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) ->
- let vs1 = vars_option bound vs rtntypopt in
- let vs2 = List.fold_left (fun vs (tm,_) -> vars bound vs tm) vs1 tml in
+ 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) ->
- let vs1 = vars_return_type bound vs rtntyp in
- let vs2 = vars bound vs1 b in
+ 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) ->
- let vs1 = vars_return_type bound vs rtntyp in
- let vs2 = vars bound vs1 c in
- let vs3 = vars bound vs2 b1 in
+ | RIf (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) ->
- let bound' = Array.fold_right Idset.add idl bound in
- let vars_fix i vs fid =
- let vs1,bound1 =
- List.fold_left
- (fun (vs,bound) (na,k,bbd,bty) ->
- let vs' = vars_option bound vs bbd in
+ let bound' = Array.fold_right Idset.add idl bound in
+ let vars_fix i vs fid =
+ let vs1,bound1 =
+ List.fold_left
+ (fun (vs,bound) (na,k,bbd,bty) ->
+ let vs' = vars_option bound vs bbd in
let vs'' = vars bound vs' bty in
- let bound' = add_name_to_ids bound na in
+ let bound' = add_name_to_ids bound na in
(vs'',bound')
)
(vs,bound')
bl.(i)
in
- let vs2 = vars bound1 vs1 tyl.(i) in
+ let vs2 = vars bound1 vs1 tyl.(i) in
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
+ | RCast (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
- and vars_pattern bound vs (loc,idl,p,c) =
- let bound' = List.fold_right Idset.add idl bound in
+ and vars_pattern bound vs (loc,idl,p,c) =
+ let bound' = List.fold_right Idset.add idl bound in
vars bound' vs c
and vars_option bound vs = function None -> vs | Some p -> vars bound vs p
- and vars_return_type bound vs (na,tyopt) =
- let bound' = add_name_to_ids bound na in
+ and vars_return_type bound vs (na,tyopt) =
+ let bound' = add_name_to_ids bound na in
vars_option bound' vs tyopt
- in
- fun rt -> List.rev (vars bound [] rt)
-
+ in fun rt ->
+ let vars = List.rev (vars bound [] rt) in
+ List.iter (fun (id, loc) ->
+ if not (Idset.mem id allowed || find_generalizable_ident id) then
+ ungeneralizable loc id) vars;
+ vars
+
let rec make_fresh ids env x =
- if is_freevar ids env x then x else make_fresh ids env (Nameops.lift_ident x)
+ if is_freevar ids env x then x else make_fresh ids env (Nameops.lift_subscript x)
-let freevars_of_ids env ids =
- List.filter (is_freevar env (Global.env())) ids
-
let next_ident_away_from id avoid = make_fresh avoid (Global.env ()) id
-let next_name_away_from na avoid =
+let next_name_away_from na avoid =
match na with
| Anonymous -> make_fresh avoid (Global.env ()) (id_of_string "anon")
| Name id -> make_fresh avoid (Global.env ()) id
let combine_params avoid fn applied needed =
- let named, applied =
- List.partition
+ let named, applied =
+ List.partition
(function
- (t, Some (loc, ExplByName id)) ->
+ (t, Some (loc, ExplByName id)) ->
if not (List.exists (fun (_, (id', _, _)) -> Name id = id') needed) then
user_err_loc (loc,"",str "Wrong argument name: " ++ Nameops.pr_id id);
true
@@ -173,49 +226,50 @@ let combine_params avoid fn applied needed =
(fun x -> match x with (t, Some (loc, ExplByName id)) -> id, t | _ -> assert false)
named
in
+ let needed = List.filter (fun (_, (_, b, _)) -> b = None) needed in
let rec aux ids avoid app need =
match app, need with
[], [] -> List.rev ids, avoid
| app, (_, (Name id, _, _)) :: need when List.mem_assoc id named ->
aux (List.assoc id named :: ids) avoid app need
-
+
| (x, None) :: app, (None, (Name id, _, _)) :: need ->
aux (x :: ids) avoid app need
-
- | _, (Some cl, (_, _, _) as d) :: need ->
+
+ | _, (Some cl, (_, _, _) as d) :: need ->
let t', avoid' = fn avoid d in
aux (t' :: ids) avoid' app need
| x :: app, (None, _) :: need -> aux (fst x :: ids) avoid app need
- | [], (None, _ as decl) :: need ->
+ | [], (None, _ as decl) :: need ->
let t', avoid' = fn avoid decl in
aux (t' :: ids) avoid' app need
- | (x,_) :: _, [] ->
+ | (x,_) :: _, [] ->
user_err_loc (constr_loc x,"",str "Typeclass does not expect more arguments")
in aux [] avoid applied needed
let combine_params_freevar =
- fun avoid (_, (na, _, _)) ->
+ fun avoid (_, (na, _, _)) ->
let id' = next_name_away_from na avoid in
(CRef (Ident (dummy_loc, id')), Idset.add id' avoid)
-
+
let destClassApp cl =
match cl with
- | CApp (loc, (None,CRef ref), l) -> loc, ref, List.map fst l
+ | CApp (loc, (None, CRef ref), l) -> loc, ref, List.map fst l
| CAppExpl (loc, (None, ref), l) -> loc, ref, l
| CRef ref -> loc_of_reference ref, ref, []
| _ -> raise Not_found
-
+
let destClassAppExpl cl =
match cl with
- | CApp (loc, (None,CRef ref), l) -> loc, ref, l
+ | CApp (loc, (None, CRef ref), l) -> loc, ref, l
| CRef ref -> loc_of_reference ref, ref, []
| _ -> raise Not_found
-let implicit_application env ?(allow_partial=true) f ty =
+let implicit_application env ?(allow_partial=true) f ty =
let is_class =
try
let (loc, r, _ as clapp) = destClassAppExpl ty in
@@ -223,30 +277,30 @@ let implicit_application env ?(allow_partial=true) f ty =
let gr = Nametab.locate qid in
if Typeclasses.is_class gr then Some (clapp, gr) else None
with Not_found -> None
- in
+ in
match is_class with
- | None -> ty
- | Some ((loc, id, par), gr) ->
+ | None -> ty, env
+ | Some ((loc, id, par), gr) ->
let avoid = Idset.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in
let c, avoid =
let c = class_info gr in
let (ci, rd) = c.cl_context in
if not allow_partial then
- begin
+ begin
let applen = List.fold_left (fun acc (x, y) -> if y = None then succ acc else acc) 0 par in
let needlen = List.fold_left (fun acc x -> if x = None then succ acc else acc) 0 ci in
- if needlen <> applen then
+ if needlen <> applen then
Typeclasses_errors.mismatched_ctx_inst (Global.env ()) Parameters (List.map fst par) rd
end;
let pars = List.rev (List.combine ci rd) in
let args, avoid = combine_params avoid f par pars in
CAppExpl (loc, (None, id), args), avoid
- in c
-
-let implicits_of_rawterm l =
- let rec aux i c =
+ in c, avoid
+
+let implicits_of_rawterm l =
+ let rec aux i c =
match c with
- RProd (loc, na, bk, t, b) | RLambda (loc, na, bk, t, b) ->
+ RProd (loc, na, bk, t, b) | RLambda (loc, na, bk, t, b) ->
let rest = aux (succ i) b in
if bk = Implicit then
let name =
@@ -254,7 +308,7 @@ let implicits_of_rawterm l =
Name id -> Some id
| Anonymous -> None
in
- (ExplByPos (i, name), (true, true)) :: rest
+ (ExplByPos (i, name), (true, true, true)) :: rest
else rest
| RLetIn (loc, na, t, b) -> aux i b
| _ -> []
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 8dd12f72..1feae81f 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: implicit_quantifiers.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
+(*i $Id$ i*)
(*i*)
open Names
@@ -24,6 +24,8 @@ open Libnames
open Typeclasses
(*i*)
+val declare_generalizable : Vernacexpr.locality_flag -> (identifier located) list option -> unit
+
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
@@ -36,13 +38,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 free ids in left-to-right order with the location of their first occurence *)
+(* Returns the generalizable free ids in left-to-right
+ order with the location of their first occurence *)
-val free_vars_of_rawconstr : ?bound:Idset.t -> rawconstr -> (Names.identifier * loc) list
+val generalizable_vars_of_rawconstr : ?bound:Idset.t -> ?allowed:Idset.t ->
+ rawconstr -> (Names.identifier * loc) list
val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier
-val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool)) list
+val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool * bool)) list
val combine_params_freevar :
Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
@@ -51,4 +55,4 @@ val combine_params_freevar :
val implicit_application : Idset.t -> ?allow_partial:bool ->
(Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
Topconstr.constr_expr * Names.Idset.t) ->
- constr_expr -> constr_expr
+ constr_expr -> constr_expr * Idset.t
diff --git a/interp/interp.mllib b/interp/interp.mllib
new file mode 100644
index 00000000..3825f3d8
--- /dev/null
+++ b/interp/interp.mllib
@@ -0,0 +1,18 @@
+Lexer
+Topconstr
+Ppextend
+Notation
+Dumpglob
+Genarg
+Syntax_def
+Smartlocate
+Reserve
+Impargs
+Implicit_quantifiers
+Constrintern
+Modintern
+Constrextern
+Coqlib
+Discharge
+Declare
+
diff --git a/interp/modintern.ml b/interp/modintern.ml
index d40205ce..049745ca 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: modintern.ml 11582 2008-11-12 19:49:57Z notin $ *)
+(* $Id$ *)
open Pp
open Util
@@ -15,7 +15,7 @@ open Entries
open Libnames
open Topconstr
open Constrintern
-
+
let rec make_mp mp = function
[] -> mp
| h::tl -> make_mp (MPdot(mp, label_of_id h)) tl
@@ -25,7 +25,7 @@ let rec make_mp mp = function
the module prefix *)
exception BadRef
-let lookup_qualid (modtype:bool) qid =
+let lookup_qualid (modtype:bool) qid =
let rec make_mp mp = function
[] -> mp
| h::tl -> make_mp (MPdot(mp, label_of_id h)) tl
@@ -33,13 +33,13 @@ let lookup_qualid (modtype:bool) qid =
let rec find_module_prefix dir n =
if n<0 then raise Not_found;
let dir',dir'' = list_chop n dir in
- let id',dir''' =
- match dir'' with
- | hd::tl -> hd,tl
+ let id',dir''' =
+ match dir'' with
+ | hd::tl -> hd,tl
| _ -> anomaly "This list should not be empty!"
in
let qid' = make_qualid dir' id' in
- try
+ try
match Nametab.locate qid' with
| ModRef mp -> mp,dir'''
| _ -> raise BadRef
@@ -47,11 +47,11 @@ let lookup_qualid (modtype:bool) qid =
Not_found -> find_module_prefix dir (pred n)
in
try Nametab.locate qid
- with Not_found ->
+ with Not_found ->
let (dir,id) = repr_qualid qid in
let pref_mp,dir' = find_module_prefix dir (List.length dir - 1) in
- let mp =
- List.fold_left (fun mp id -> MPdot (mp, label_of_id id)) pref_mp dir'
+ let mp =
+ List.fold_left (fun mp id -> MPdot (mp, label_of_id id)) pref_mp dir'
in
if modtype then
ModTypeRef (make_ln mp (label_of_id id))
@@ -61,7 +61,7 @@ let lookup_qualid (modtype:bool) qid =
*)
-(* Search for the head of [qid] in [binders].
+(* Search for the head of [qid] in [binders].
If found, returns the module_path/kernel_name created from the dirpath
and the basename. Searches Nametab otherwise.
*)
@@ -71,38 +71,64 @@ let lookup_module (loc,qid) =
Dumpglob.dump_modref loc mp "modtype"; mp
with
| Not_found -> Modops.error_not_a_module_loc loc (string_of_qualid qid)
-
+
let lookup_modtype (loc,qid) =
try
let mp = Nametab.locate_modtype qid in
Dumpglob.dump_modref loc mp "mod"; mp
with
- | Not_found ->
+ | Not_found ->
Modops.error_not_a_modtype_loc loc (string_of_qualid qid)
-let transl_with_decl env = function
+let lookup_module_or_modtype (loc,qid) =
+ try
+ let mp = Nametab.locate_module qid in
+ Dumpglob.dump_modref loc mp "modtype"; (mp,true)
+ with Not_found -> try
+ 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)
+
+let transl_with_decl env = function
| CWith_Module ((_,fqid),qid) ->
With_Module (fqid,lookup_module qid)
| CWith_Definition ((_,fqid),c) ->
With_Definition (fqid,interp_constr Evd.empty env c)
-let rec interp_modexpr env = function
- | CMEident qid ->
+let rec interp_modexpr env = function
+ | CMident qid ->
MSEident (lookup_module qid)
- | CMEapply (me1,me2) ->
+ | 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 ()
-let rec interp_modtype env = function
- | CMTEident qid ->
+
+let rec interp_modtype env = function
+ | CMident qid ->
MSEident (lookup_modtype qid)
- | CMTEapply (mty1,me) ->
+ | CMapply (mty1,me) ->
let mty' = interp_modtype env mty1 in
let me' = interp_modexpr env me in
MSEapply(mty',me')
- | CMTEwith (mty,decl) ->
+ | CMwith (mty,decl) ->
let mty = interp_modtype env mty in
let decl = transl_with_decl env decl in
MSEwith(mty,decl)
+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) ->
+ 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 ();
+ (MSEwith(me,decl), ismod)
diff --git a/interp/modintern.mli b/interp/modintern.mli
index 36971599..e528b7af 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: modintern.mli 11582 2008-11-12 19:49:57Z notin $ i*)
+(*i $Id$ i*)
(*i*)
open Declarations
@@ -18,11 +18,18 @@ open Names
open Topconstr
(*i*)
-(* Module expressions and module types are interpreted relatively to
+(* Module expressions and module types are interpreted relatively to
eventual functor or funsig arguments. *)
-val interp_modtype : env -> module_type_ast -> module_struct_entry
+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,
+ and in case of failure, interpretes this ast as a module type.
+ The boolean is true for a module, false for a module type *)
+
+val interp_modexpr_or_modtype : env -> module_ast ->
+ module_struct_entry * bool
+
val lookup_module : qualid located -> module_path
diff --git a/interp/notation.ml b/interp/notation.ml
index 776fff79..a72a6b6f 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: notation.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id$ *)
(*i*)
open Util
@@ -30,7 +30,7 @@ open Ppextend
no interpretation for negative numbers in [nat]); interpreters both for
terms and patterns can be set; these interpreters are in permanent table
[numeral_interpreter_tab]
- - a set of ML printers for expressions denoting numbers parsable in
+ - a set of ML printers for expressions denoting numbers parsable in
this scope
- a set of interpretations for infix (more generally distfix) notations
- an optional pair of delimiters which, when occurring in a syntactic
@@ -42,7 +42,7 @@ open Ppextend
type level = precedence * tolerability list
type delimiters = string
-type notation_location = dir_path * string
+type notation_location = (dir_path * dir_path) * string
type scope = {
notations: (string, interpretation * notation_location) Gmap.t;
@@ -92,6 +92,11 @@ let scope_stack = ref []
let current_scopes () = !scope_stack
+let scope_is_open_in_scopes sc l =
+ List.mem (Scope sc) l
+
+let scope_is_open sc = scope_is_open_in_scopes sc (!scope_stack)
+
(* TODO: push nat_scope, z_scope, ... in scopes summary *)
(* Exportation of scopes *)
@@ -104,22 +109,22 @@ let open_scope i (_,(local,op,sc)) =
let cache_scope o =
open_scope 1 o
-let subst_scope (_,subst,sc) = sc
+let subst_scope (subst,sc) = sc
open Libobject
-let classify_scope (_,(local,_,_ as o)) =
- if local then Dispose else Substitute o
+let discharge_scope (local,_,_ as o) =
+ if local then None else Some o
-let export_scope (local,_,_ as x) = if local then None else Some x
+let classify_scope (local,_,_ as o) =
+ if local then Dispose else Substitute o
-let (inScope,outScope) =
+let (inScope,outScope) =
declare_object {(default_object "SCOPE") with
cache_function = cache_scope;
open_function = open_scope;
subst_function = subst_scope;
- classify_function = classify_scope;
- export_function = export_scope }
+ classify_function = classify_scope }
let open_close_scope (local,opening,sc) =
Lib.add_anonymous_leaf (inScope (local,opening,Scope sc))
@@ -142,23 +147,28 @@ let delimiters_map = ref Gmap.empty
let declare_delimiters scope key =
let sc = find_scope scope in
- if sc.delimiters <> None && Flags.is_verbose () then begin
- let old = Option.get sc.delimiters in
- Flags.if_verbose
- warning ("Overwritting previous delimiting key "^old^" in scope "^scope)
- end;
- let sc = { sc with delimiters = Some key } in
- scope_map := Gmap.add scope sc !scope_map;
- if Gmap.mem key !delimiters_map then begin
- let oldsc = Gmap.find key !delimiters_map in
- Flags.if_verbose warning ("Hiding binding of key "^key^" to "^oldsc)
+ let newsc = { sc with delimiters = Some key } in
+ begin match sc.delimiters with
+ | 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);
+ scope_map := Gmap.add scope newsc !scope_map
end;
- delimiters_map := Gmap.add key scope !delimiters_map
-
-let find_delimiters_scope loc key =
+ 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);
+ delimiters_map := Gmap.add key scope !delimiters_map
+ end
+ with Not_found -> delimiters_map := Gmap.add key scope !delimiters_map
+
+let find_delimiters_scope loc key =
try Gmap.find key !delimiters_map
- with Not_found ->
- user_err_loc
+ with Not_found ->
+ user_err_loc
(loc, "find_delimiters", str ("Unknown scope delimiting key "^key^"."))
(* Uninterpretation tables *)
@@ -178,25 +188,35 @@ 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 ref
- | RRef (_,ref) -> RefKey ref
+ | RApp (_,RRef (_,ref),_) -> RefKey (make_gr ref)
+ | RRef (_,ref) -> RefKey (make_gr ref)
| _ -> Oth
let cases_pattern_key = function
- | PatCstr (_,ref,_,_) -> RefKey (ConstructRef ref)
+ | PatCstr (_,ref,_,_) -> RefKey (make_gr (ConstructRef ref))
| _ -> Oth
let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *)
- | AApp (ARef ref,args) -> RefKey ref, Some (List.length args)
- | AList (_,_,AApp (ARef ref,args),_,_) -> RefKey ref, Some (List.length args)
- | ARef ref -> RefKey ref, None
+ | AApp (ARef ref,args) -> RefKey(make_gr ref), Some (List.length args)
+ | AList (_,_,AApp (ARef ref,args),_,_) -> RefKey (make_gr ref), Some (List.length args)
+ | ARef ref -> RefKey(make_gr ref), None
| _ -> Oth, None
(**********************************************************************)
(* Interpreting numbers (not in summary because functional objects) *)
-type required_module = section_path * string list
+type required_module = full_path * string list
type 'a prim_token_interpreter =
loc -> 'a -> rawconstr
@@ -213,7 +233,7 @@ let prim_token_interpreter_tab =
(Hashtbl.create 7 : (scope_name, internal_prim_token_interpreter) Hashtbl.t)
let add_prim_token_interpreter sc interp =
- try
+ try
let cont = Hashtbl.find prim_token_interpreter_tab sc in
Hashtbl.replace prim_token_interpreter_tab sc (interp cont)
with Not_found ->
@@ -223,7 +243,7 @@ let add_prim_token_interpreter sc interp =
let declare_prim_token_interpreter sc interp (patl,uninterp,b) =
declare_scope sc;
add_prim_token_interpreter sc interp;
- List.iter (fun pat ->
+ List.iter (fun pat ->
Hashtbl.add prim_token_key_table (rawconstr_key pat) (sc,uninterp,b))
patl
@@ -243,7 +263,7 @@ let declare_string_interpreter sc dir interp (patl,uninterp,inpat) =
(patl, (fun r -> Option.map mkString (uninterp r)), inpat)
let check_required_module loc sc (sp,d) =
- try let _ = Nametab.absolute_reference sp in ()
+ try let _ = Nametab.global_of_path sp in ()
with Not_found ->
user_err_loc (loc,"prim_token_interpreter",
str ("Cannot interpret in "^sc^" without requiring first module "
@@ -260,7 +280,7 @@ let find_with_delimiters = function
| None -> None
let rec find_without_delimiters find (ntn_scope,ntn) = function
- | Scope scope :: scopes ->
+ | Scope scope :: scopes ->
(* Is the expected ntn/numpr attached to the most recently open scope? *)
if Some scope = ntn_scope then
Some (None,None)
@@ -272,7 +292,7 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
else
find_without_delimiters find (ntn_scope,ntn) scopes
| SingleNotation ntn' :: scopes ->
- if ntn_scope = None & ntn = Some ntn' then
+ if ntn_scope = None & ntn = Some ntn' then
Some (None,None)
else
find_without_delimiters find (ntn_scope,ntn) scopes
@@ -335,7 +355,7 @@ let find_prim_token g loc p sc =
(* Try for a primitive numerical notation *)
let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc loc p in
check_required_module loc sc spdir;
- g (interp ()), (dirpath (fst spdir),"")
+ g (interp ()), ((dirpath (fst spdir),empty_dirpath),"")
let interp_prim_token_gen g loc p local_scopes =
let scopes = make_current_scopes local_scopes in
@@ -371,7 +391,7 @@ let availability_of_notation (ntn_scope,ntn) scopes =
find_without_delimiters f (ntn_scope,Some ntn) (make_current_scopes scopes)
let uninterp_prim_token c =
- try
+ try
let (sc,numpr,_) = Hashtbl.find prim_token_key_table (rawconstr_key c) in
match numpr c with
| None -> raise No_match
@@ -379,7 +399,7 @@ let uninterp_prim_token c =
with Not_found -> raise No_match
let uninterp_prim_token_cases_pattern c =
- try
+ try
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;
@@ -389,8 +409,10 @@ let uninterp_prim_token_cases_pattern c =
| Some n -> (na,sc,n)
with Not_found -> raise No_match
-let availability_of_prim_token printer_scope local_scopes =
- let f scope = Hashtbl.mem prim_token_interpreter_tab scope in
+let availability_of_prim_token n printer_scope local_scopes =
+ let f scope =
+ try ignore (Hashtbl.find prim_token_interpreter_tab scope dummy_loc n); true
+ with Not_found -> false in
let scopes = make_current_scopes local_scopes in
Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes)
@@ -456,13 +478,16 @@ let load_arguments_scope _ (_,(_,r,scl)) =
let cache_arguments_scope o =
load_arguments_scope 1 o
-let subst_arguments_scope (_,subst,(req,r,scl)) =
+let subst_arguments_scope (subst,(req,r,scl)) =
(ArgsScopeNoDischarge,fst (subst_global subst r),scl)
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)
+let classify_arguments_scope (req,_,_ as obj) =
+ if req = ArgsScopeNoDischarge then Dispose else Substitute obj
+
let rebuild_arguments_scope (req,r,l) =
match req with
| ArgsScopeNoDischarge -> assert false
@@ -475,21 +500,23 @@ let rebuild_arguments_scope (req,r,l) =
let l1,_ = list_chop (List.length l' - List.length l) l' in
(req,r,l1@l)
-let (inArgumentsScope,outArgumentsScope) =
+let (inArgumentsScope,outArgumentsScope) =
declare_object {(default_object "ARGUMENTS-SCOPE") with
cache_function = cache_arguments_scope;
load_function = load_arguments_scope;
subst_function = subst_arguments_scope;
- classify_function = (fun (_,o) -> Substitute o);
+ classify_function = classify_arguments_scope;
discharge_function = discharge_arguments_scope;
- rebuild_function = rebuild_arguments_scope;
- export_function = (fun x -> Some x) }
+ rebuild_function = rebuild_arguments_scope }
+
+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 local ref scl =
- let req = if local then ArgsScopeNoDischarge else ArgsScopeManual in
+ let req =
+ if is_local local ref then ArgsScopeNoDischarge else ArgsScopeManual in
declare_arguments_scope_gen req ref scl
let find_arguments_scope r =
@@ -511,8 +538,9 @@ type symbol =
let rec string_of_symbol = function
| NonTerminal _ -> ["_"]
+ | Terminal "_" -> ["'_'"]
| Terminal s -> [s]
- | SProdList (_,l) ->
+ | SProdList (_,l) ->
let l = List.flatten (List.map string_of_symbol l) in "_"::l@".."::l@["_"]
| Break _ -> []
@@ -525,14 +553,14 @@ let decompose_notation_key s =
if n>=len then List.rev dirs else
let pos =
try
- String.index_from s n ' '
+ String.index_from s n ' '
with Not_found -> len
in
let tok =
match String.sub s n (pos-n) with
| "_" -> NonTerminal (id_of_string "_")
- | s -> Terminal s in
- decomp_ntn (tok::dirs) (pos+1)
+ | s -> Terminal (drop_simple_quotes s) in
+ decomp_ntn (tok::dirs) (pos+1)
in
decomp_ntn [] 0
@@ -549,12 +577,12 @@ let classes_of_scope sc =
let pr_scope_classes sc =
let l = classes_of_scope sc in
if l = [] then mt()
- else
+ else
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 =
- str "\"" ++ str ntn ++ str "\" := " ++
+ str "\"" ++ str ntn ++ str "\" := " ++
prraw (rawconstr_of_aconstr dummy_loc c)
let pr_named_scope prraw scope sc =
@@ -562,7 +590,7 @@ let pr_named_scope prraw scope sc =
match Gmap.fold (fun _ _ x -> x+1) sc.notations 0 with
| 0 -> str "No lonely notation"
| n -> str "Lonely notation" ++ (if n=1 then mt() else str"s")
- else
+ else
str "Scope " ++ str scope ++ fnl () ++ pr_delimiters_info sc.delimiters)
++ fnl ()
++ pr_scope_classes scope
@@ -574,7 +602,7 @@ let pr_named_scope prraw scope sc =
let pr_scope prraw scope = pr_named_scope prraw scope (find_scope scope)
let pr_scopes prraw =
- Gmap.fold
+ Gmap.fold
(fun scope sc strm -> pr_named_scope prraw scope sc ++ fnl () ++ strm)
!scope_map (mt ())
@@ -606,7 +634,7 @@ let browse_notation strict ntn map =
let trms = List.filter (function Terminal _ -> true | _ -> false) toks in
if strict then [Terminal ntn] = trms else List.mem (Terminal ntn) trms in
let l =
- Gmap.fold
+ Gmap.fold
(fun scope_name sc ->
Gmap.fold (fun ntn ((_,r),df) l ->
if find ntn then (ntn,(scope_name,r,df))::l else l) sc.notations)
@@ -616,7 +644,7 @@ let browse_notation strict ntn map =
let global_reference_of_notation test (ntn,(sc,c,_)) =
match c with
| ARef ref when test ref -> Some (ntn,sc,ref)
- | AApp (ARef ref, l) when List.for_all isAVar_or_AHole l & test ref ->
+ | AApp (ARef ref, l) when List.for_all isAVar_or_AHole l & test ref ->
Some (ntn,sc,ref)
| _ -> None
@@ -638,27 +666,28 @@ let interp_notation_as_global_reference loc test ntn sc =
match Option.List.flatten refs with
| [_,_,ref] -> ref
| [] -> error_notation_not_reference loc ntn
- | refs ->
+ | refs ->
let f (ntn,sc,ref) = find_default ntn !scope_stack = Some sc in
match List.filter f refs with
| [_,_,ref] -> ref
| [] -> error_notation_not_reference loc ntn
| _ -> error_ambiguous_notation loc ntn
-let locate_notation prraw ntn =
+let locate_notation prraw 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
str "Unknown notation"
else
t (str "Notation " ++
- tab () ++ str "Scope " ++ tab () ++ fnl () ++
+ tab () ++ str "Scope " ++ tab () ++ fnl () ++
prlist (fun (ntn,l) ->
- let scope = find_default ntn !scope_stack in
- prlist
+ let scope = find_default ntn scopes in
+ prlist
(fun (sc,r,(_,df)) ->
hov 0 (
pr_notation_info prraw df r ++ tbrk (1,2) ++
- (if sc = default_scope then mt () else (str ": " ++ str sc)) ++
+ (if sc = default_scope then mt () else (str ": " ++ str sc)) ++
tbrk (1,2) ++
(if Some sc = scope then str "(default interpretation)" else mt ())
++ fnl ()))
@@ -688,7 +717,7 @@ let collect_notations stack =
let all' = match all with
| (s,lonelyntn)::rest when s = default_scope ->
(s,(df,r)::lonelyntn)::rest
- | _ ->
+ | _ ->
(default_scope,[df,r])::all in
(all',ntn::knownntn))
([],[]) stack)
@@ -700,11 +729,11 @@ let pr_visible_in_scope prraw (scope,ntns) =
ntns (mt ()) in
(if scope = default_scope then
str "Lonely notation" ++ (if List.length ntns <> 1 then str "s" else mt())
- else
+ else
str "Visible in scope " ++ str scope)
++ fnl () ++ strm
-let pr_scope_stack prraw stack =
+let pr_scope_stack prraw stack =
List.fold_left
(fun strm scntns -> strm ++ pr_visible_in_scope prraw scntns ++ fnl ())
(mt ()) (collect_notations stack)
@@ -719,7 +748,7 @@ let pr_visibility prraw = function
type unparsing_rule = unparsing list * precedence
(* Concrete syntax for symbolic-extension table *)
-let printing_rules =
+let printing_rules =
ref (Gmap.empty : (string,unparsing_rule) Gmap.t)
let declare_notation_printing_rule ntn unpl =
@@ -759,10 +788,8 @@ let init () =
printing_rules := Gmap.empty;
class_scope_map := Gmap.add CL_SORT "type_scope" Gmap.empty
-let _ =
+let _ =
declare_summary "symbols"
{ freeze_function = freeze;
unfreeze_function = unfreeze;
- init_function = init;
- survive_module = false;
- survive_section = false }
+ init_function = init }
diff --git a/interp/notation.mli b/interp/notation.mli
index 4d7289c2..f52e17cc 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: notation.mli 11445 2008-10-11 16:42:46Z herbelin $ i*)
+(*i $Id$ i*)
(*i*)
open Util
@@ -39,9 +39,14 @@ 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
+ * the current opened scopes *)
+val scope_is_open_in_scopes : scope_name -> scopes -> bool
+val scope_is_open : scope_name -> bool
+
(* Open scope *)
-val open_close_scope :
+val open_close_scope :
(* locality *) bool * (* open *) bool * scope_name -> unit
(* Extend a list of scopes *)
@@ -60,8 +65,8 @@ val find_delimiters_scope : loc -> delimiters -> scope_name
negative numbers are not supported, the interpreter must fail with
an appropriate error message *)
-type notation_location = dir_path * string
-type required_module = section_path * string list
+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 'a prim_token_interpreter =
@@ -81,19 +86,19 @@ val declare_string_interpreter : scope_name -> required_module ->
val interp_prim_token : loc -> prim_token -> local_scopes ->
rawconstr * (notation_location * scope_name option)
-val interp_prim_token_cases_pattern : loc -> prim_token -> name ->
+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];
raise [No_match] if no such token *)
-val uninterp_prim_token :
+val uninterp_prim_token :
rawconstr -> scope_name * prim_token
-val uninterp_prim_token_cases_pattern :
+val uninterp_prim_token_cases_pattern :
cases_pattern -> name * scope_name * prim_token
-val availability_of_prim_token :
- scope_name -> local_scopes -> delimiters option option
+val availability_of_prim_token :
+ prim_token -> scope_name -> local_scopes -> delimiters option option
(*s Declare and interpret back and forth a notation *)
@@ -120,7 +125,7 @@ val uninterp_cases_pattern_notations : cases_pattern ->
(* 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 ->
+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 *)
@@ -130,7 +135,7 @@ val level_of_notation : notation -> level (* raise [Not_found] if no level *)
(*s** Miscellaneous *)
-val interp_notation_as_global_reference : loc -> (global_reference -> bool) ->
+val interp_notation_as_global_reference : loc -> (global_reference -> bool) ->
notation -> delimiters option -> global_reference
(* Checks for already existing notations *)
@@ -138,7 +143,7 @@ val exists_notation_in_scope : scope_name option -> notation ->
interpretation -> bool
(* Declares and looks for scopes associated to arguments of a global ref *)
-val declare_arguments_scope :
+val declare_arguments_scope :
bool (* true=local *) -> global_reference -> scope_name option list -> unit
val find_arguments_scope : global_reference -> scope_name option list
@@ -159,10 +164,11 @@ type symbol =
val make_notation_key : symbol list -> notation
val decompose_notation_key : notation -> symbol list
-(* Prints scopes (expect a pure aconstr printer *)
+(* 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 -> std_ppcmds
+val locate_notation : (rawconstr -> std_ppcmds) -> notation ->
+ scope_name option -> std_ppcmds
val pr_visibility: (rawconstr -> std_ppcmds) -> scope_name option -> std_ppcmds
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index 34e93624..a4142d69 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: ppextend.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
+(*i $Id$ *)
(*i*)
open Pp
@@ -50,7 +50,7 @@ let ppcmd_of_cut = function
| PpBrk(n1,n2) -> brk(n1,n2)
| PpTbrk(n1,n2) -> tbrk(n1,n2)
-type unparsing =
+type unparsing =
| UnpMetaVar of int * parenRelation
| UnpListMetaVar of int * parenRelation * unparsing list
| UnpTerminal of string
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index 3d49c210..3d09587d 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: ppextend.mli 6616 2005-01-21 17:18:23Z herbelin $ i*)
+(*i $Id$ i*)
(*i*)
open Pp
@@ -40,7 +40,7 @@ val ppcmd_of_box : ppbox -> std_ppcmds -> std_ppcmds
val ppcmd_of_cut : ppcut -> std_ppcmds
-type unparsing =
+type unparsing =
| UnpMetaVar of int * parenRelation
| UnpListMetaVar of int * parenRelation * unparsing list
| UnpTerminal of string
diff --git a/interp/reserve.ml b/interp/reserve.ml
index f7496832..9d841282 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: reserve.ml 10727 2008-03-28 20:22:43Z msozeau $ i*)
+(*i $Id$ i*)
(* Reserved names *)
@@ -24,24 +24,22 @@ let cache_reserved_type (_,(id,t)) =
reserve_table := Idmap.add id t !reserve_table
let (in_reserved, _) =
- declare_object {(default_object "RESERVED-TYPE") with
+ declare_object {(default_object "RESERVED-TYPE") with
cache_function = cache_reserved_type }
-let _ =
+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.survive_module = false;
- Summary.survive_section = false }
+ Summary.init_function = (fun () -> reserve_table := Idmap.empty) }
-let declare_reserved_type (loc,id) t =
+let declare_reserved_type (loc,id) t =
if id <> root_of_id id then
user_err_loc(loc,"declare_reserved_type",
(pr_id id ++ str
" is not reservable: it must have no trailing digits, quote, or _"));
begin try
- let _ = Idmap.find id !reserve_table in
+ let _ = Idmap.find id !reserve_table in
user_err_loc(loc,"declare_reserved_type",
(pr_id id++str" is already bound to a type"))
with Not_found -> () end;
@@ -68,7 +66,7 @@ let rec unloc = function
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
+ Array.map (List.map
(fun (na,k,obd,ty) -> (na,k,Option.map unloc obd, unloc ty)))
bl,
Array.map unloc tyl,
@@ -84,7 +82,7 @@ let rec unloc = function
let anonymize_if_reserved na t = match na with
| Name id as na ->
- (try
+ (try
if not !Flags.raw_print & unloc t = find_reserved_type id
then RHole (dummy_loc,Evd.BinderType na)
else t
diff --git a/interp/reserve.mli b/interp/reserve.mli
index 13349ee9..a83e66c4 100644
--- a/interp/reserve.mli
+++ b/interp/reserve.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: reserve.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id$ i*)
open Util
open Names
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
new file mode 100644
index 00000000..faad3c50
--- /dev/null
+++ b/interp/smartlocate.ml
@@ -0,0 +1,64 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* Created by Hugo Herbelin from code formerly dispatched in
+ syntax_def.ml or tacinterp.ml, Sep 2009 *)
+
+(* This file provides high-level name globalization functions *)
+
+(* $Id:$ *)
+
+(* *)
+open Pp
+open Util
+open Names
+open Libnames
+open Genarg
+open Syntax_def
+open Topconstr
+
+let global_of_extended_global = function
+ | TrueGlobal ref -> ref
+ | SynDef kn ->
+ match search_syntactic_definition kn with
+ | [],ARef ref -> ref
+ | _ -> raise Not_found
+
+let locate_global_with_alias (loc,qid) =
+ let ref = Nametab.locate_extended qid in
+ try global_of_extended_global ref
+ with Not_found ->
+ user_err_loc (loc,"",pr_qualid qid ++
+ str " is bound to a notation that does not denote a reference.")
+
+let global_inductive_with_alias r =
+ let (loc,qid as lqid) = qualid_of_reference r in
+ try match locate_global_with_alias lqid with
+ | IndRef ind -> ind
+ | ref ->
+ user_err_loc (loc_of_reference r,"global_inductive",
+ pr_reference r ++ spc () ++ str "is not an inductive type.")
+ with Not_found -> Nametab.error_global_not_found_loc loc qid
+
+let global_with_alias r =
+ let (loc,qid as lqid) = qualid_of_reference r in
+ try locate_global_with_alias lqid
+ with Not_found -> Nametab.error_global_not_found_loc loc qid
+
+let smart_global = function
+ | AN r ->
+ global_with_alias r
+ | ByNotation (loc,ntn,sc) ->
+ Notation.interp_notation_as_global_reference loc (fun _ -> true) ntn sc
+
+let smart_global_inductive = function
+ | AN r ->
+ global_inductive_with_alias r
+ | ByNotation (loc,ntn,sc) ->
+ destIndRef
+ (Notation.interp_notation_as_global_reference loc isIndRef ntn sc)
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
new file mode 100644
index 00000000..682484f5
--- /dev/null
+++ b/interp/smartlocate.mli
@@ -0,0 +1,37 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \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
+ 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" *)
+val global_of_extended_global : extended_global_reference -> global_reference
+
+(* Locate a reference taking into account possible "alias" notations *)
+val global_with_alias : reference -> global_reference
+
+(* The same for inductive types *)
+val global_inductive_with_alias : reference -> inductive
+
+(* Locate a reference taking into account notations and "aliases" *)
+val smart_global : reference or_by_notation -> global_reference
+
+(* 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 fe998cba..245ed0f5 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: syntax_def.ml 11512 2008-10-27 12:28:36Z herbelin $ *)
+(* $Id$ *)
open Util
open Pp
@@ -16,6 +16,7 @@ open Topconstr
open Libobject
open Lib
open Nameops
+open Nametab
(* Syntactic definitions. *)
@@ -25,9 +26,7 @@ let _ = Summary.declare_summary
"SYNTAXCONSTANT"
{ Summary.freeze_function = (fun () -> !syntax_table);
Summary.unfreeze_function = (fun ft -> syntax_table := ft);
- Summary.init_function = (fun () -> syntax_table := KNmap.empty);
- Summary.survive_module = false;
- Summary.survive_section = false }
+ Summary.init_function = (fun () -> syntax_table := KNmap.empty) }
let add_syntax_constant kn c =
syntax_table := KNmap.add kn c !syntax_table
@@ -37,38 +36,41 @@ let load_syntax_constant i ((sp,kn),(local,pat,onlyparse)) =
errorlabstrm "cache_syntax_constant"
(pr_id (basename sp) ++ str " already exists");
add_syntax_constant kn pat;
- Nametab.push_syntactic_definition (Nametab.Until i) sp kn;
- if not onlyparse then
- (* Declare it to be used as long name *)
- Notation.declare_uninterpretation (Notation.SynDefRule kn) pat
+ Nametab.push_syndef (Nametab.Until i) sp kn
+
+let is_alias_of_already_visible_name sp = function
+ | _,ARef ref ->
+ let (dir,id) = repr_qualid (shortest_qualid_of_global Idset.empty ref) in
+ dir = empty_dirpath && id = basename sp
+ | _ ->
+ false
let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
- Nametab.push_syntactic_definition (Nametab.Exactly i) sp kn;
- if not onlyparse then
- (* Redeclare it to be used as (short) name in case an other (distfix)
- notation was declared inbetween *)
- Notation.declare_uninterpretation (Notation.SynDefRule kn) pat
+ if not (is_alias_of_already_visible_name sp pat) then begin
+ Nametab.push_syndef (Nametab.Exactly i) sp kn;
+ if not onlyparse then
+ (* Redeclare it to be used as (short) name in case an other (distfix)
+ notation was declared inbetween *)
+ Notation.declare_uninterpretation (Notation.SynDefRule kn) pat
+ end
let cache_syntax_constant d =
- load_syntax_constant 1 d
+ load_syntax_constant 1 d;
+ open_syntax_constant 1 d
-let subst_syntax_constant ((sp,kn),subst,(local,pat,onlyparse)) =
+let subst_syntax_constant (subst,(local,pat,onlyparse)) =
(local,subst_interpretation subst pat,onlyparse)
-let classify_syntax_constant (_,(local,_,_ as o)) =
+let classify_syntax_constant (local,_,_ as o) =
if local then Dispose else Substitute o
-let export_syntax_constant (local,_,_ as o) =
- if local then None else Some o
-
let (in_syntax_constant, out_syntax_constant) =
declare_object {(default_object "SYNTAXCONSTANT") with
cache_function = cache_syntax_constant;
load_function = load_syntax_constant;
open_function = open_syntax_constant;
subst_function = subst_syntax_constant;
- classify_function = classify_syntax_constant;
- export_function = export_syntax_constant }
+ classify_function = classify_syntax_constant }
type syndef_interpretation = (identifier * subscopes) list * aconstr
@@ -80,27 +82,5 @@ let out_pat ((ids,idsl),ac) = assert (idsl=[]); (ids,ac)
let declare_syntactic_definition local id onlyparse pat =
let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in ()
-let search_syntactic_definition loc kn =
+let search_syntactic_definition kn =
out_pat (KNmap.find kn !syntax_table)
-
-let locate_global_with_alias (loc,qid) =
- match Nametab.extended_locate qid with
- | TrueGlobal ref -> ref
- | SyntacticDef kn ->
- match search_syntactic_definition dummy_loc kn with
- | [],ARef ref -> ref
- | _ ->
- user_err_loc (loc,"",pr_qualid qid ++
- str " is bound to a notation that does not denote a reference")
-
-let inductive_of_reference_with_alias r =
- match locate_global_with_alias (qualid_of_reference r) with
- | IndRef ind -> ind
- | ref ->
- user_err_loc (loc_of_reference r,"global_inductive",
- pr_reference r ++ spc () ++ str "is not an inductive type")
-
-let global_with_alias r =
- let (loc,qid as lqid) = qualid_of_reference r in
- try locate_global_with_alias lqid
- with Not_found -> Nametab.error_global_not_found_loc loc qid
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 0f5e0be7..b4da6dd7 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -6,13 +6,14 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: syntax_def.mli 11512 2008-10-27 12:28:36Z herbelin $ i*)
+(*i $Id$ i*)
(*i*)
open Util
open Names
open Topconstr
open Rawterm
+open Nametab
open Libnames
(*i*)
@@ -20,21 +21,7 @@ open Libnames
type syndef_interpretation = (identifier * subscopes) list * aconstr
-val declare_syntactic_definition : bool -> identifier -> bool ->
+val declare_syntactic_definition : bool -> identifier -> bool ->
syndef_interpretation -> unit
-val search_syntactic_definition : loc -> kernel_name -> syndef_interpretation
-
-(* [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
-
-(* Locate a reference taking into account possible "alias" notations *)
-val global_with_alias : reference -> global_reference
-
-(* The same for inductive types *)
-val inductive_of_reference_with_alias : reference -> inductive
-
+val search_syntactic_definition : kernel_name -> syndef_interpretation
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 89ddd001..d7528fad 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: topconstr.ml 11739 2009-01-02 19:33:19Z herbelin $ *)
+(* $Id$ *)
(*i*)
open Pp
@@ -23,7 +23,7 @@ open Mod_subst
(* This is the subtype of rawconstr 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
+ first id is where each argument of the list has to be substituted
in iterator and snd id is alternative name just for printing;
boolean is associativity *)
@@ -43,7 +43,7 @@ type aconstr =
| ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
| AIf of aconstr * (name * aconstr option) * aconstr * aconstr
| ARec of fix_kind * identifier array *
- (name * aconstr option * aconstr) list array * aconstr array *
+ (name * aconstr option * aconstr) list array * aconstr array *
aconstr array
| ASort of rawsort
| AHole of Evd.hole_kind
@@ -53,11 +53,17 @@ type aconstr =
(**********************************************************************)
(* Re-interpret a notation as a rawconstr, taking care of binders *)
+let name_to_ident = function
+ | Anonymous -> error "This expression should be a simple identifier."
+ | Name id -> id
+
+let to_id g e id = let e,na = g e (Name id) in e,name_to_ident na
+
let rec cases_pattern_fold_map loc g e = function
| PatVar (_,na) ->
- let e',na' = name_fold_map g e na in e', PatVar (loc,na')
+ let e',na' = g e na in e', PatVar (loc,na')
| PatCstr (_,cstr,patl,na) ->
- let e',na' = name_fold_map g e na in
+ let e',na' = g e na in
let e',patl' = list_fold_map (cases_pattern_fold_map loc g) e patl in
e', PatCstr (loc,cstr,patl',na')
@@ -77,42 +83,42 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
let outerl = (ldots_var,inner)::(if swap then [x,RVar(loc,y)] else []) in
subst_rawvars outerl it
| ALambda (na,ty,c) ->
- let e,na = name_fold_map g e na in RLambda (loc,na,Explicit,f e ty,f e c)
+ let e,na = g e na in RLambda (loc,na,Explicit,f e ty,f e c)
| AProd (na,ty,c) ->
- let e,na = name_fold_map g e na in RProd (loc,na,Explicit,f e ty,f e c)
+ let e,na = g e na in RProd (loc,na,Explicit,f e ty,f e c)
| ALetIn (na,b,c) ->
- let e,na = name_fold_map g e na in RLetIn (loc,na,f e b,f e c)
+ let e,na = g e na in RLetIn (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
| None -> e',None
- | Some (ind,npar,nal) ->
- let e',nal' = List.fold_right (fun na (e',nal) ->
- let e',na' = name_fold_map g e' na in e',na'::nal) nal (e',[]) in
+ | Some (ind,npar,nal) ->
+ let e',nal' = List.fold_right (fun na (e',nal) ->
+ let e',na' = g e' na in e',na'::nal) nal (e',[]) in
e',Some (loc,ind,npar,nal') in
- let e',na' = name_fold_map g e' na in
+ let e',na' = g e' na in
(e',(f e tm,(na',t'))::tml')) tml (e,[]) in
- let fold (idl,e) id = let (e,id) = g e id in ((id::idl,e),id) in
+ let fold (idl,e) na = let (e,na) = g e na in ((name_cons na idl,e),na) in
let eqnl' = List.map (fun (patl,rhs) ->
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')
| ALetTuple (nal,(na,po),b,c) ->
- let e,nal = list_fold_map (name_fold_map g) e nal in
- let e,na = name_fold_map g e na in
+ 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)
| AIf (c,(na,po),b1,b2) ->
- let e,na = name_fold_map g e na in
+ let e,na = g e na in
RIf (loc,f e c,(na,Option.map (f e) po),f e b1,f e b2)
| ARec (fk,idl,dll,tl,bl) ->
- let e,idl = array_fold_map g e idl in
+ let e,idl = array_fold_map (to_id g) e idl in
let e,dll = array_fold_map (list_fold_map (fun e (na,oc,b) ->
- let e,na = name_fold_map g e na in
+ let e,na = g e na in
(e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
RRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e) bl)
- | ACast (c,k) -> RCast (loc,f e c,
- match k with
+ | ACast (c,k) -> RCast (loc,f e c,
+ match k with
| CastConv (k,t) -> CastConv (k,f e t)
| CastCoerce -> CastCoerce)
| ASort x -> RSort (loc,x)
@@ -121,7 +127,7 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
| ARef x -> RRef (loc,x)
let rec rawconstr_of_aconstr loc x =
- let rec aux () x =
+ let rec aux () x =
rawconstr_of_aconstr_with_binders loc (fun () id -> ((),id)) aux () x
in aux () x
@@ -137,7 +143,7 @@ let has_ldots =
(function RApp (_,RVar(_,v),_) when v = ldots_var -> true | _ -> false)
let compare_rawconstr f t1 t2 = match t1,t2 with
- | RRef (_,r1), RRef (_,r2) -> r1 = r2
+ | RRef (_,r1), RRef (_,r2) -> eq_gr r1 r2
| RVar (_,v1), RVar (_,v2) -> v1 = v2
| RApp (_,f1,l1), RApp (_,f2,l2) -> f f1 f2 & List.for_all2 f l1 l2
| RLambda (_,na1,bk1,ty1,c1), RLambda (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 ->
@@ -161,7 +167,7 @@ let discriminate_patterns foundvars nl l1 l2 =
let rec aux n c1 c2 = match c1,c2 with
| RVar (_,v1), RVar (_,v2) when v1<>v2 ->
if !diff = None then (diff := Some (v1,v2,(n>=nl)); true)
- else
+ else
!diff = Some (v1,v2,(n>=nl)) or !diff = Some (v2,v1,(n<nl))
or (error
"Both ends of the recursive pattern differ in more than one place")
@@ -182,7 +188,7 @@ let aconstr_and_vars_of_rawconstr a =
let found = ref [] in
let rec aux = function
| RVar (_,id) -> found := id::!found; AVar id
- | RApp (_,f,args) when has_ldots args -> make_aconstr_list f args
+ | RApp (_,f,args) when has_ldots args -> make_aconstr_list f args
| RApp (_,RVar (_,f),[RApp (_,t,[c]);d]) when f = ldots_var ->
(* Special case for alternative (recursive) notation of application *)
let x,y,lassoc = discriminate_patterns found 0 [c] [d] in
@@ -210,13 +216,13 @@ let aconstr_and_vars_of_rawconstr a =
AIf (aux c,(na,Option.map aux po),aux b1,aux b2)
| RRec (_,fk,idl,dll,tl,bl) ->
Array.iter (fun id -> found := id::!found) idl;
- let dll = Array.map (List.map (fun (na,bk,oc,b) ->
- if bk <> Explicit then
+ 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,
- match k with CastConv (k,t) -> CastConv (k,aux t)
+ | RCast (_,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
@@ -271,65 +277,65 @@ let aconstr_of_rawconstr vars a =
let aconstr_of_constr avoiding t =
aconstr_of_rawconstr [] (Detyping.detype false avoiding [] t)
-let rec subst_pat subst pat =
+let rec subst_pat subst pat =
match pat with
| PatVar _ -> pat
- | PatCstr (loc,((kn,i),j),cpl,n) ->
- let kn' = subst_kn subst kn
+ | PatCstr (loc,((kn,i),j),cpl,n) ->
+ let kn' = subst_ind subst kn
and cpl' = list_smartmap (subst_pat subst) cpl in
if kn' == kn && cpl' == cpl then pat else
PatCstr (loc,((kn',i),j),cpl',n)
let rec subst_aconstr subst bound raw =
match raw with
- | ARef ref ->
- let ref',t = subst_global subst ref in
+ | ARef ref ->
+ let ref',t = subst_global subst ref in
if ref' == ref then raw else
aconstr_of_constr bound t
| AVar _ -> raw
- | AApp (r,rl) ->
- let r' = subst_aconstr subst bound r
+ | AApp (r,rl) ->
+ let r' = subst_aconstr subst bound r
and rl' = list_smartmap (subst_aconstr subst bound) rl in
if r' == r && rl' == rl then raw else
AApp(r',rl')
- | AList (id1,id2,r1,r2,b) ->
+ | AList (id1,id2,r1,r2,b) ->
let r1' = subst_aconstr subst bound r1
and r2' = subst_aconstr subst bound r2 in
if r1' == r1 && r2' == r2 then raw else
AList (id1,id2,r1',r2',b)
- | ALambda (n,r1,r2) ->
+ | ALambda (n,r1,r2) ->
let r1' = subst_aconstr subst bound r1
and r2' = subst_aconstr subst bound r2 in
if r1' == r1 && r2' == r2 then raw else
ALambda (n,r1',r2')
- | AProd (n,r1,r2) ->
+ | AProd (n,r1,r2) ->
let r1' = subst_aconstr subst bound r1
and r2' = subst_aconstr subst bound r2 in
if r1' == r1 && r2' == r2 then raw else
AProd (n,r1',r2')
- | ALetIn (n,r1,r2) ->
- let r1' = subst_aconstr subst bound r1
+ | ALetIn (n,r1,r2) ->
+ let r1' = subst_aconstr subst bound r1
and r2' = subst_aconstr subst bound r2 in
if r1' == r1 && r2' == r2 then raw else
ALetIn (n,r1',r2')
- | ACases (sty,rtntypopt,rl,branches) ->
+ | ACases (sty,rtntypopt,rl,branches) ->
let rtntypopt' = Option.smartmap (subst_aconstr subst bound) rtntypopt
and rl' = list_smartmap
- (fun (a,(n,signopt) as x) ->
+ (fun (a,(n,signopt) as x) ->
let a' = subst_aconstr subst bound a in
let signopt' = Option.map (fun ((indkn,i),n,nal as z) ->
- let indkn' = subst_kn subst indkn in
+ let indkn' = subst_ind subst indkn in
if indkn == indkn' then z else ((indkn',i),n,nal)) signopt in
if a' == a && signopt' == signopt then x else (a',(n,signopt')))
rl
- and branches' = list_smartmap
+ and branches' = list_smartmap
(fun (cpl,r as branch) ->
let cpl' = list_smartmap (subst_pat subst) cpl
and r' = subst_aconstr subst bound r in
@@ -343,7 +349,7 @@ let rec subst_aconstr subst bound raw =
| ALetTuple (nal,(na,po),b,c) ->
let po' = Option.smartmap (subst_aconstr subst bound) po
- and b' = subst_aconstr subst bound b
+ and b' = subst_aconstr subst bound b
and c' = subst_aconstr subst bound c in
if po' == po && b' == b && c' == c then raw else
ALetTuple (nal,(na,po'),b',c')
@@ -351,13 +357,13 @@ let rec subst_aconstr subst bound raw =
| AIf (c,(na,po),b1,b2) ->
let po' = Option.smartmap (subst_aconstr subst bound) po
and b1' = subst_aconstr subst bound b1
- and b2' = subst_aconstr subst bound b2
+ and b2' = subst_aconstr subst bound b2
and c' = subst_aconstr subst bound c in
if po' == po && b1' == b1 && b2' == b2 && c' == c then raw else
AIf (c',(na,po'),b1',b2')
| ARec (fk,idl,dll,tl,bl) ->
- let dll' =
+ let dll' =
array_smartmap (list_smartmap (fun (na,oc,b as x) ->
let oc' = Option.smartmap (subst_aconstr subst bound) oc in
let b' = subst_aconstr subst bound b in
@@ -369,18 +375,18 @@ let rec subst_aconstr subst bound raw =
| APatVar _ | ASort _ -> raw
- | AHole (Evd.ImplicitArg (ref,i)) ->
- let ref',t = subst_global subst ref in
+ | AHole (Evd.ImplicitArg (ref,i,b)) ->
+ let ref',t = subst_global subst ref in
if ref' == ref then raw else
AHole (Evd.InternalHole)
- | AHole (Evd.BinderType _ | Evd.QuestionMark _ | Evd.CasesType
+ | AHole (Evd.BinderType _ | Evd.QuestionMark _ | Evd.CasesType
| Evd.InternalHole | Evd.TomatchTypeParameter _ | Evd.GoalEvar
- | Evd.ImpossibleCase) -> raw
+ | Evd.ImpossibleCase | Evd.MatchingVar _) -> raw
- | ACast (r1,k) ->
+ | ACast (r1,k) ->
match k with
CastConv (k, r2) ->
- let r1' = subst_aconstr subst bound r1
+ let r1' = subst_aconstr subst bound r1
and r2' = subst_aconstr subst bound r2 in
if r1' == r1 && r2' == r2 then raw else
ACast (r1',CastConv (k,r2'))
@@ -388,7 +394,7 @@ let rec subst_aconstr subst bound raw =
let r1' = subst_aconstr subst bound r1 in
if r1' == r1 then raw else
ACast (r1',CastCoerce)
-
+
let subst_interpretation subst (metas,pat) =
let bound = List.map fst (fst metas @ snd metas) in
(metas,subst_aconstr subst bound pat)
@@ -443,7 +449,7 @@ let match_fix_kind fk1 fk2 =
match (fk1,fk2) with
| RCoFix n1, RCoFix n2 -> n1 = n2
| RFix (nl1,n1), RFix (nl2,n2) ->
- n1 = n2 &&
+ n1 = n2 &&
array_for_all2 (fun (n1,_) (n2,_) -> n2 = None || n1 = n2) nl1 nl2
| _ -> false
@@ -452,19 +458,23 @@ let match_opt f sigma t1 t2 = match (t1,t2) with
| Some t1, Some t2 -> f sigma t1 t2
| _ -> raise No_match
+let rawconstr_of_name = function
+ | Anonymous -> RHole (dummy_loc,Evd.InternalHole)
+ | Name id -> RVar (dummy_loc,id)
+
let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
- | (Name id1,Name id2) when List.mem id2 metas ->
- alp, bind_env alp sigma id2 (RVar (dummy_loc,id1))
+ | (na,Name id2) when List.mem id2 metas ->
+ alp, bind_env alp sigma id2 (rawconstr_of_name na)
| (Name id1,Name id2) -> (id1,id2)::alp,sigma
| (Anonymous,Anonymous) -> alp,sigma
| _ -> raise No_match
-let rec match_cases_pattern metas acc pat1 pat2 =
+let rec match_cases_pattern_binders metas acc pat1 pat2 =
match (pat1,pat2) with
| PatVar (_,na1), PatVar (_,na2) -> match_names metas acc na1 na2
| PatCstr (_,c1,patl1,na1), PatCstr (_,c2,patl2,na2)
when c1 = c2 & List.length patl1 = List.length patl2 ->
- List.fold_left2 (match_cases_pattern metas)
+ List.fold_left2 (match_cases_pattern_binders metas)
(match_names metas acc na1 na2) patl1 patl2
| _ -> raise No_match
@@ -472,10 +482,33 @@ 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 match_alist match_fun metas sigma l1 l2 x iter termin lassoc =
+ (* match the iterator at least once *)
+ let sigmavar,sigmalist =
+ List.fold_left2 (match_fun (ldots_var::metas)) sigma l1 l2 in
+ (* Recover the recursive position *)
+ let rest = List.assoc ldots_var sigmavar in
+ (* Recover the first element *)
+ let t1 = List.assoc x sigmavar in
+ let sigmavar = List.remove_assoc x (List.remove_assoc ldots_var sigmavar) in
+ (* try to find the remaining elements or the terminator *)
+ let rec match_alist_tail metas sigma acc rest =
+ try
+ let sigmavar,sigmalist = match_fun (ldots_var::metas) sigma rest iter in
+ let rest = List.assoc ldots_var sigmavar in
+ let t = List.assoc x sigmavar in
+ let sigmavar =
+ List.remove_assoc x (List.remove_assoc ldots_var sigmavar) in
+ match_alist_tail metas (sigmavar,sigmalist) (t::acc) rest
+ with No_match ->
+ List.rev acc, match_fun metas (sigmavar,sigmalist) rest termin in
+ let tl,(sigmavar,sigmalist) = match_alist_tail metas sigma [t1] rest in
+ (sigmavar, (x,if lassoc then List.rev tl else tl)::sigmalist)
+
let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
| r1, AVar id2 when List.mem id2 metas -> bind_env alp sigma id2 r1
| RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma
- | RRef (_,r1), ARef r2 when r1 = r2 -> 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) ->
let n1 = List.length l1 and n2 = List.length l2 in
@@ -486,30 +519,31 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
let l11,l12 = list_chop (n1-n2) l1 in RApp (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
- | RApp (loc,f1,l1), AList (x,_,(AApp (f2,l2) as iter),termin,lassoc)
+ | RApp (loc,f1,l1), AList (x,_,(AApp (f2,l2) as iter),termin,lassoc)
when List.length l1 >= List.length l2 ->
let f1,l1 = adjust_application_n (List.length l2) loc f1 l1 in
- match_alist alp metas sigma (f1::l1) (f2::l2) x iter termin lassoc
+ match_alist (match_ alp)
+ metas sigma (f1::l1) (f2::l2) x iter termin lassoc
| 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)
+ | RCases (_,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 rtno2' = abstract_return_type_context_aconstr tml2 rtno2 in
- let sigma =
- try Option.fold_left2 (match_ alp metas) sigma rtno1' rtno2'
+ let sigma =
+ try Option.fold_left2 (match_ alp metas) sigma rtno1' rtno2'
with Option.Heterogeneous -> raise No_match
in
- let sigma = List.fold_left2
+ 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)
+ | RLetTuple (_,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
@@ -519,7 +553,7 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
| 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)
+ | RRec (_,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
->
@@ -529,7 +563,7 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
match_ alp metas (match_opt (match_ 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 alp,sigma = array_fold_right2 (fun id1 id2 alsig ->
+ 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)) ->
@@ -539,32 +573,9 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
| RSort (_,s1), ASort s2 when s1 = s2 -> sigma
| RPatVar _, AHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
| a, AHole _ -> sigma
- | (RDynamic _ | RRec _ | REvar _), _
+ | (RDynamic _ | RRec _ | REvar _), _
| _,_ -> raise No_match
-and match_alist alp metas sigma l1 l2 x iter termin lassoc =
- (* match the iterator at least once *)
- let sigmavar,sigmalist =
- List.fold_left2 (match_ alp (ldots_var::metas)) sigma l1 l2 in
- (* Recover the recursive position *)
- let rest = List.assoc ldots_var sigmavar in
- (* Recover the first element *)
- let t1 = List.assoc x sigmavar in
- let sigmavar = List.remove_assoc x (List.remove_assoc ldots_var sigmavar) in
- (* try to find the remaining elements or the terminator *)
- let rec match_alist_tail alp metas sigma acc rest =
- try
- let sigmavar,sigmalist = match_ alp (ldots_var::metas) sigma rest iter in
- let rest = List.assoc ldots_var sigmavar in
- let t = List.assoc x sigmavar in
- let sigmavar =
- List.remove_assoc x (List.remove_assoc ldots_var sigmavar) in
- match_alist_tail alp metas (sigmavar,sigmalist) (t::acc) rest
- with No_match ->
- List.rev acc, match_ alp metas (sigmavar,sigmalist) rest termin in
- let tl,(sigmavar,sigmalist) = match_alist_tail alp metas sigma [t1] rest in
- (sigmavar, (x,if lassoc then List.rev tl else tl)::sigmalist)
-
and match_binders alp metas na1 na2 sigma b1 b2 =
let (alp,sigma) = match_names metas (alp,sigma) na1 na2 in
match_ alp metas sigma b1 b2
@@ -572,8 +583,9 @@ and match_binders alp metas na1 na2 sigma b1 b2 =
and match_equations 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 metas) (alp,sigma) patl1 patl2 in
+ let (alp,sigma) =
+ List.fold_left2 (match_cases_pattern_binders metas)
+ (alp,sigma) patl1 patl2 in
match_ alp metas sigma rhs1 rhs2
type scope_name = string
@@ -599,6 +611,55 @@ let match_aconstr c ((metas_scl,metaslist_scl),pat) =
List.map (fun (x,scl) -> (find x,scl)) metas_scl,
List.map (fun (x,scl) -> (List.assoc x substlist,scl)) metaslist_scl
+(* Matching cases pattern *)
+
+let bind_env_cases_pattern (sigma,sigmalist as fullsigma) var v =
+ try
+ let vvar = List.assoc var sigma in
+ if v=vvar then fullsigma else raise No_match
+ with Not_found ->
+ (* TODO: handle the case of multiple occs in different scopes *)
+ (var,v)::sigma,sigmalist
+
+let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with
+ | r1, AVar id2 when List.mem id2 metas -> bind_env_cases_pattern sigma id2 r1
+ | PatVar (_,Anonymous), AHole _ -> sigma
+ | PatCstr (loc,(ind,_ as r1),[],_), ARef (ConstructRef r2) when r1 = r2 ->
+ sigma
+ | PatCstr (loc,(ind,_ as r1),args1,_), AApp (ARef (ConstructRef r2),l2)
+ when r1 = r2 ->
+ let nparams = Inductive.inductive_params (Global.lookup_inductive ind) in
+ if List.length l2 <> nparams + List.length args1
+ then
+ (* TODO: revert partially applied notations of the form
+ "Notation P := (@pair)." *)
+ raise No_match
+ else
+ let (p2,args2) = list_chop nparams l2 in
+ (* All parameters must be _ *)
+ List.iter (function AHole _ -> () | _ -> raise No_match) p2;
+ List.fold_left2 (match_cases_pattern metas) sigma args1 args2
+ | PatCstr (loc,(ind,_ as r1),args1,_),
+ AList (x,_,(AApp (ARef (ConstructRef r2),l2) as iter),termin,lassoc)
+ when r1 = r2 ->
+ let nparams = Inductive.inductive_params (Global.lookup_inductive ind) in
+ assert (List.length args1 + nparams = List.length l2);
+ let (p2,args2) = list_chop nparams l2 in
+ List.iter (function AHole _ -> () | _ -> raise No_match) p2;
+ match_alist match_cases_pattern
+ metas sigma args1 args2 x iter termin lassoc
+ | _ -> raise No_match
+
+let match_aconstr_cases_pattern c ((metas_scl,metaslist_scl),pat) =
+ let vars = List.map fst metas_scl @ List.map fst metaslist_scl in
+ let subst,substlist = match_cases_pattern vars ([],[]) c pat in
+ (* Reorder canonically the substitution *)
+ let find x subst =
+ try List.assoc x subst
+ with Not_found -> anomaly "match_aconstr_cases_pattern" in
+ List.map (fun (x,scl) -> (find x subst,scl)) metas_scl,
+ List.map (fun (x,scl) -> (find x substlist,scl)) metaslist_scl
+
(**********************************************************************)
(*s Concrete syntax for terms *)
@@ -624,20 +685,21 @@ type cases_pattern_expr =
| CPatOr of loc * cases_pattern_expr list
| CPatNotation of loc * notation * cases_pattern_expr notation_substitution
| CPatPrim of loc * prim_token
+ | CPatRecord of loc * (reference * cases_pattern_expr) list
| CPatDelimiters of loc * string * cases_pattern_expr
type constr_expr =
| CRef of reference
- | CFix of loc * identifier located * fixpoint_expr list
- | CCoFix of loc * identifier located * cofixpoint_expr list
+ | CFix of loc * identifier located * fix_expr list
+ | CCoFix of loc * identifier located * cofix_expr list
| CArrow of loc * constr_expr * constr_expr
| CProdN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
| CLambdaN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
| CLetIn of loc * name located * constr_expr * constr_expr
| CAppExpl of loc * (proj_flag * reference) * constr_expr list
- | CApp of loc * (proj_flag * constr_expr) *
+ | CApp of loc * (proj_flag * constr_expr) *
(constr_expr * explicitation located option) list
- | CRecord of loc * constr_expr option * (identifier located * constr_expr) list
+ | CRecord of loc * constr_expr option * (reference * constr_expr) list
| CCases of loc * case_style * constr_expr option *
(constr_expr * (name option * constr_expr option)) list *
(loc * cases_pattern_expr list located list * constr_expr) list
@@ -656,24 +718,24 @@ type constr_expr =
| CDelimiters of loc * string * constr_expr
| CDynamic of loc * Dyn.t
-and fixpoint_expr =
+and fix_expr =
identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
and local_binder =
| LocalRawDef of name located * constr_expr
| LocalRawAssum of name located list * binder_kind * constr_expr
-
+
and typeclass_constraint = name located * binding_kind * constr_expr
and typeclass_context = typeclass_constraint list
-and cofixpoint_expr =
+and cofix_expr =
identifier located * local_binder list * constr_expr * constr_expr
-and recursion_order_expr =
+and recursion_order_expr =
| CStructRec
| CWfRec of constr_expr
- | CMeasureRec of constr_expr
+ | CMeasureRec of constr_expr * constr_expr option (* measure, relation *)
type constr_pattern_expr = constr_expr
@@ -682,16 +744,6 @@ type constr_pattern_expr = constr_expr
let default_binder_kind = Default Explicit
-let rec local_binders_length = function
- | [] -> 0
- | LocalRawDef _::bl -> 1 + local_binders_length bl
- | LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl
-
-let rec local_assums_length = function
- | [] -> 0
- | LocalRawDef _::bl -> local_binders_length bl
- | LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl
-
let names_of_local_assums bl =
List.flatten (List.map (function LocalRawAssum(l,_,_)->l|_->[]) bl)
@@ -733,6 +785,7 @@ let cases_pattern_expr_loc = function
| CPatAtom (loc,_) -> loc
| CPatOr (loc,_) -> loc
| CPatNotation (loc,_,_) -> loc
+ | CPatRecord (loc, _) -> loc
| CPatPrim (loc,_) -> loc
| CPatDelimiters (loc,_,_) -> loc
@@ -745,7 +798,7 @@ let ids_of_cases_indtype =
let rec vars_of = function
(* We deal only with the regular cases *)
| CApp (_,_,l) -> List.fold_left add_var [] (List.map fst l)
- | CNotation (_,_,(l,[]))
+ | CNotation (_,_,(l,[]))
(* assume the ntn is applicative and does not instantiate the head !! *)
| CAppExpl (_,_,l) -> List.fold_left add_var [] l
| CDelimiters(_,_,c) -> vars_of c
@@ -760,10 +813,12 @@ let ids_of_cases_tomatch tms =
tms []
let is_constructor id =
- try ignore (Nametab.extended_locate (make_short_qualid id)); true
+ try ignore (Nametab.locate_extended (qualid_of_ident id)); true
with Not_found -> true
-
+
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) ->
List.fold_left (cases_pattern_fold_names f) a patl
@@ -775,7 +830,7 @@ let rec cases_pattern_fold_names f a = function
let ids_of_pattern_list =
List.fold_left
- (located_fold_left
+ (located_fold_left
(List.fold_left (cases_pattern_fold_names Idset.add)))
Idset.empty
@@ -827,12 +882,12 @@ let fold_constr_expr_with_binders g f n acc = function
| CFix (loc,_,l) ->
let n' = List.fold_right (fun ((_,id),_,_,_,_) -> g id) l n in
List.fold_right (fun (_,(_,o),lb,t,c) acc ->
- fold_local_binders g f n'
+ fold_local_binders g f n'
(fold_local_binders g f n acc t lb) c lb) l acc
- | CCoFix (loc,_,_) ->
+ | CCoFix (loc,_,_) ->
Pp.warning "Capture check in multiple binders not done"; acc
-let free_vars_of_constr_expr c =
+let free_vars_of_constr_expr c =
let rec aux bdvars l = function
| CRef (Ident (_,id)) -> if List.mem id bdvars then l else Idset.add id l
| c -> fold_constr_expr_with_binders (fun a l -> a::l) aux bdvars l c
@@ -842,26 +897,31 @@ let occur_var_constr_expr id c = Idset.mem id (free_vars_of_constr_expr c)
let mkIdentC id = CRef (Ident (dummy_loc, id))
let mkRefC r = CRef r
-let mkAppC (f,l) = CApp (dummy_loc, (None,f), List.map (fun x -> (x,None)) l)
let mkCastC (a,k) = CCast (dummy_loc,a,k)
let mkLambdaC (idl,bk,a,b) = CLambdaN (dummy_loc,[idl,bk,a],b)
let mkLetInC (id,a,b) = CLetIn (dummy_loc,id,a,b)
let mkProdC (idl,bk,a,b) = CProdN (dummy_loc,[idl,bk,a],b)
+let mkAppC (f,l) =
+ let l = List.map (fun x -> (x,None)) l in
+ match f with
+ | CApp (_,g,l') -> CApp (dummy_loc, g, l' @ l)
+ | _ -> CApp (dummy_loc, (None, f), l)
+
let rec mkCProdN loc bll c =
match bll with
- | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
+ | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
CProdN (loc,[idl,bk,t],mkCProdN (join_loc loc1 loc) bll c)
- | LocalRawDef ((loc1,_) as id,b) :: bll ->
+ | LocalRawDef ((loc1,_) as id,b) :: bll ->
CLetIn (loc,id,b,mkCProdN (join_loc loc1 loc) bll c)
| [] -> c
| LocalRawAssum ([],_,_) :: bll -> mkCProdN loc bll c
let rec mkCLambdaN loc bll c =
match bll with
- | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
+ | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
CLambdaN (loc,[idl,bk,t],mkCLambdaN (join_loc loc1 loc) bll c)
- | LocalRawDef ((loc1,_) as id,b) :: bll ->
+ | LocalRawDef ((loc1,_) as id,b) :: bll ->
CLetIn (loc,id,b,mkCLambdaN (join_loc loc1 loc) bll c)
| [] -> c
| LocalRawAssum ([],_,_) :: bll -> mkCLambdaN loc bll c
@@ -872,7 +932,7 @@ let rec abstract_constr_expr c = function
| LocalRawAssum (idl,bk,t)::bl ->
List.fold_right (fun x b -> mkLambdaC([x],bk,t,b)) idl
(abstract_constr_expr c bl)
-
+
let rec prod_constr_expr c = function
| [] -> c
| LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl)
@@ -880,12 +940,39 @@ let rec prod_constr_expr c = function
List.fold_right (fun x b -> mkProdC([x],bk,t,b)) idl
(prod_constr_expr c bl)
+let coerce_reference_to_id = function
+ | Ident (_,id) -> id
+ | Qualid (loc,_) ->
+ user_err_loc (loc, "coerce_reference_to_id",
+ str "This expression should be a simple identifier.")
+
let coerce_to_id = function
| CRef (Ident (loc,id)) -> (loc,id)
| a -> user_err_loc
(constr_loc a,"coerce_to_id",
str "This expression should be a simple identifier.")
+let coerce_to_name = function
+ | CRef (Ident (loc,id)) -> (loc,Name id)
+ | CHole (loc,_) -> (loc,Anonymous)
+ | a -> user_err_loc
+ (constr_loc a,"coerce_to_name",
+ str "This expression should be a name.")
+
+(* Interpret the index of a recursion order annotation *)
+
+let index_of_annot bl na =
+ let names = List.map snd (names_of_local_assums bl) in
+ match na with
+ | None ->
+ if names = [] then error "A fixpoint needs at least one parameter."
+ else None
+ | Some (loc, id) ->
+ try Some (list_index0 (Name id) names)
+ with Not_found ->
+ user_err_loc(loc,"",
+ str "No parameter named " ++ Nameops.pr_id id ++ str".")
+
(* Used in correctness and interface *)
let map_binder g e nal = List.fold_right (fun (_,na) -> name_fold g na) nal e
@@ -908,8 +995,8 @@ let map_local_binders f g e bl =
let map_constr_expr_with_binders g f e = function
| CArrow (loc,a,b) -> CArrow (loc,f e a,f e b)
- | CAppExpl (loc,r,l) -> CAppExpl (loc,r,List.map (f e) l)
- | CApp (loc,(p,a),l) ->
+ | CAppExpl (loc,r,l) -> CAppExpl (loc,r,List.map (f e) l)
+ | CApp (loc,(p,a),l) ->
CApp (loc,(p,f e a),List.map (fun (a,i) -> (f e a,i)) l)
| CProdN (loc,bl,b) ->
let (e,bl) = map_binders f g e bl in CProdN (loc,bl,f e b)
@@ -922,7 +1009,7 @@ let map_constr_expr_with_binders g f e = function
CNotation (loc,n,(List.map (f e) l,List.map (List.map (f e)) ll))
| 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 _
+ | CHole _ | CEvar _ | CPatVar _ | CSort _
| CPrim _ | CDynamic _ | 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) ->
@@ -939,7 +1026,7 @@ let map_constr_expr_with_binders g f e = function
let e' = Option.fold_right (name_fold g) ona e in
CIf (loc,f e c,(ona,Option.map (f e') po),f e b1,f e b2)
| CFix (loc,id,dl) ->
- CFix (loc,id,List.map (fun (id,n,bl,t,d) ->
+ CFix (loc,id,List.map (fun (id,n,bl,t,d) ->
let (e',bl') = map_local_binders f g e bl in
let t' = f e' t in
(* Note: fix names should be inserted before the arguments... *)
@@ -958,33 +1045,38 @@ let map_constr_expr_with_binders g f e = function
let rec replace_vars_constr_expr l = function
| CRef (Ident (loc,id)) as x ->
(try CRef (Ident (loc,List.assoc id l)) with Not_found -> x)
- | c -> map_constr_expr_with_binders List.remove_assoc
+ | c -> map_constr_expr_with_binders List.remove_assoc
replace_vars_constr_expr l c
(**********************************************************************)
(* Concrete syntax for modules and modules types *)
-type with_declaration_ast =
+type with_declaration_ast =
| CWith_Module of identifier list located * qualid located
| CWith_Definition of identifier list located * constr_expr
+type module_ast =
+ | CMident of qualid located
+ | CMapply of module_ast * module_ast
+ | CMwith of module_ast * with_declaration_ast
-type module_ast =
- | CMEident of qualid located
- | CMEapply of module_ast * module_ast
+type module_ast_inl = module_ast * bool (* honor the inline annotations or not *)
-type module_type_ast =
- | CMTEident of qualid located
- | CMTEapply of module_type_ast * module_ast
- | CMTEwith of module_type_ast * with_declaration_ast
+type 'a module_signature =
+ | Enforce of 'a (* ... : T *)
+ | Check of 'a list (* ... <: T1 <: T2, possibly empty *)
-type include_ast =
- | CIMTE of module_type_ast
- | CIME of module_ast
+(* Returns the ranges of locs of the notation that are not occupied by args *)
+(* and which are them occupied by proper symbols of the notation (or spaces) *)
-let loc_of_notation f loc args ntn =
- if args=[] or ntn.[0] <> '_' then fst (Util.unloc loc)
- else snd (Util.unloc (f (List.hd args)))
+let locs_of_notation f loc (args,argslist) ntn =
+ let (bl,el) = Util.unloc loc in
+ let rec aux pos = function
+ | [] -> if pos = el then [] else [(pos,el-1)]
+ | a::l ->
+ let ba,ea = Util.unloc (f a) in
+ if pos = ba then aux ea l else (pos,ba-1)::aux ea l
+ in aux bl (args@List.flatten argslist)
-let ntn_loc = loc_of_notation constr_loc
-let patntn_loc = loc_of_notation cases_pattern_expr_loc
+let ntn_loc = locs_of_notation constr_loc
+let patntn_loc = locs_of_notation cases_pattern_expr_loc
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 1dd5ec97..f67edfb9 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: topconstr.mli 11739 2009-01-02 19:33:19Z herbelin $ i*)
+(*i $Id$ i*)
(*i*)
open Pp
@@ -39,7 +39,7 @@ type aconstr =
| ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
| AIf of aconstr * (name * aconstr option) * aconstr * aconstr
| ARec of fix_kind * identifier array *
- (name * aconstr option * aconstr) list array * aconstr array *
+ (name * aconstr option * aconstr) list array * aconstr array *
aconstr array
| ASort of rawsort
| AHole of Evd.hole_kind
@@ -48,7 +48,7 @@ type aconstr =
(**********************************************************************)
(* Translate a rawconstr into a notation given the list of variables *)
-(* bound by the notation; also interpret recursive patterns *)
+(* bound by the notation; also interpret recursive patterns *)
val aconstr_of_rawconstr : identifier list -> rawconstr -> aconstr
@@ -61,8 +61,8 @@ val eq_rawconstr : rawconstr -> rawconstr -> bool
(**********************************************************************)
(* Re-interpret a notation as a rawconstr, taking care of binders *)
-val rawconstr_of_aconstr_with_binders : loc ->
- ('a -> identifier -> 'a * identifier) ->
+val rawconstr_of_aconstr_with_binders : loc ->
+ ('a -> name -> 'a * name) ->
('a -> aconstr -> rawconstr) -> 'a -> aconstr -> rawconstr
val rawconstr_of_aconstr : loc -> aconstr -> rawconstr
@@ -86,6 +86,9 @@ type interpretation =
val match_aconstr : rawconstr -> interpretation ->
(rawconstr * subscopes) list * (rawconstr 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 *)
@@ -97,9 +100,9 @@ val subst_interpretation : substitution -> interpretation -> interpretation
type notation = string
type explicitation = ExplByPos of int * identifier option | ExplByName of identifier
-
-type binder_kind =
- | Default of binding_kind
+
+type binder_kind =
+ | Default of binding_kind
| Generalized of binding_kind * binding_kind * bool
(* Inner binding, outer bindings, typeclass-specific flag
for implicit generalization of superclasses *)
@@ -120,20 +123,21 @@ type cases_pattern_expr =
| CPatOr of loc * cases_pattern_expr list
| CPatNotation of loc * notation * cases_pattern_expr notation_substitution
| CPatPrim of loc * prim_token
+ | CPatRecord of Util.loc * (reference * cases_pattern_expr) list
| CPatDelimiters of loc * string * cases_pattern_expr
type constr_expr =
| CRef of reference
- | CFix of loc * identifier located * fixpoint_expr list
- | CCoFix of loc * identifier located * cofixpoint_expr list
+ | CFix of loc * identifier located * fix_expr list
+ | CCoFix of loc * identifier located * cofix_expr list
| CArrow of loc * constr_expr * constr_expr
| CProdN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
| CLambdaN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
| CLetIn of loc * name located * constr_expr * constr_expr
| CAppExpl of loc * (proj_flag * reference) * constr_expr list
- | CApp of loc * (proj_flag * constr_expr) *
+ | CApp of loc * (proj_flag * constr_expr) *
(constr_expr * explicitation located option) list
- | CRecord of loc * constr_expr option * (identifier located * constr_expr) list
+ | CRecord of loc * constr_expr option * (reference * constr_expr) list
| CCases of loc * case_style * constr_expr option *
(constr_expr * (name option * constr_expr option)) list *
(loc * cases_pattern_expr list located list * constr_expr) list
@@ -152,22 +156,22 @@ type constr_expr =
| CDelimiters of loc * string * constr_expr
| CDynamic of loc * Dyn.t
-and fixpoint_expr =
+and fix_expr =
identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
-and cofixpoint_expr =
+and cofix_expr =
identifier located * local_binder list * constr_expr * constr_expr
-and recursion_order_expr =
+and recursion_order_expr =
| CStructRec
| CWfRec of constr_expr
- | CMeasureRec of constr_expr
+ | CMeasureRec of constr_expr * constr_expr option (* measure, relation *)
(** Anonymous defs allowed ?? *)
and local_binder =
| LocalRawDef of name located * constr_expr
| LocalRawAssum of name located list * binder_kind * constr_expr
-
+
type typeclass_constraint = name located * binding_kind * constr_expr
and typeclass_context = typeclass_constraint list
@@ -200,7 +204,11 @@ val mkLambdaC : name located list * binder_kind * constr_expr * constr_expr -> c
val mkLetInC : name located * constr_expr * constr_expr -> constr_expr
val mkProdC : name located list * binder_kind * constr_expr * constr_expr -> constr_expr
+val coerce_reference_to_id : reference -> identifier
val coerce_to_id : constr_expr -> identifier located
+val coerce_to_name : constr_expr -> name located
+
+val index_of_annot : local_binder list -> identifier located option -> int option
val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
@@ -211,18 +219,12 @@ val mkCProdN : loc -> local_binder list -> constr_expr -> constr_expr
(* For binders parsing *)
-(* Includes let binders *)
-val local_binders_length : local_binder list -> int
-
-(* Excludes let binders *)
-val local_assums_length : local_binder list -> int
+(* With let binders *)
+val names_of_local_binders : local_binder list -> name located list
(* Does not take let binders into account *)
val names_of_local_assums : local_binder list -> name located list
-(* With let binders *)
-val names_of_local_binders : local_binder list -> name located list
-
(* Used in typeclasses *)
val fold_constr_expr_with_binders : (identifier -> 'a -> 'a) ->
@@ -238,23 +240,23 @@ val map_constr_expr_with_binders :
(**********************************************************************)
(* Concrete syntax for modules and module types *)
-type with_declaration_ast =
+type with_declaration_ast =
| CWith_Module of identifier list located * qualid located
| CWith_Definition of identifier list located * constr_expr
+type module_ast =
+ | CMident of qualid located
+ | CMapply of module_ast * module_ast
+ | CMwith of module_ast * with_declaration_ast
-type module_ast =
- | CMEident of qualid located
- | CMEapply of module_ast * module_ast
-
-type module_type_ast =
- | CMTEident of qualid located
- | CMTEapply of module_type_ast * module_ast
- | CMTEwith of module_type_ast * with_declaration_ast
+type module_ast_inl = module_ast * bool (* honor the inline annotations or not *)
-type include_ast =
- | CIMTE of module_type_ast
- | CIME of module_ast
+type 'a module_signature =
+ | Enforce of 'a (* ... : T *)
+ | Check of 'a list (* ... <: T1 <: T2, possibly empty *)
-val ntn_loc : Util.loc -> constr_expr list -> string -> int
-val patntn_loc : Util.loc -> cases_pattern_expr list -> string -> int
+val ntn_loc :
+ Util.loc -> constr_expr notation_substitution -> string -> (int * int) list
+val patntn_loc :
+ Util.loc -> cases_pattern_expr notation_substitution -> string ->
+ (int * int) list
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-01 15:33:33 +0000