summaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml83
-rw-r--r--interp/constrintern.ml640
-rw-r--r--interp/constrintern.mli29
-rw-r--r--interp/dumpglob.ml228
-rw-r--r--interp/dumpglob.mli43
-rw-r--r--interp/genarg.ml22
-rw-r--r--interp/genarg.mli19
-rw-r--r--interp/implicit_quantifiers.ml214
-rw-r--r--interp/implicit_quantifiers.mli33
-rw-r--r--interp/modintern.ml34
-rw-r--r--interp/modintern.mli5
-rw-r--r--interp/notation.ml18
-rw-r--r--interp/notation.mli4
-rw-r--r--interp/syntax_def.ml13
-rw-r--r--interp/syntax_def.mli10
-rw-r--r--interp/topconstr.ml111
-rw-r--r--interp/topconstr.mli32
17 files changed, 930 insertions, 608 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index efb6c853..f99af68e 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: constrextern.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: constrextern.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
(*i*)
open Pp
@@ -190,8 +190,9 @@ let rec check_same_type ty1 ty2 =
check_same_type b1 b2
| CCast(_,a1,CastCoerce), CCast(_,a2, CastCoerce) ->
check_same_type a1 a2
- | CNotation(_,n1,e1), CNotation(_,n2,e2) when n1=n2 ->
- List.iter2 check_same_type e1 e2
+ | CNotation(_,n1,(e1,el1)), CNotation(_,n2,(e2,el2)) when n1=n2 ->
+ List.iter2 check_same_type e1 e2;
+ List.iter2 (List.iter2 check_same_type) el1 el2
| CPrim(_,i1), CPrim(_,i2) when i1=i2 -> ()
| CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) when s1=s2 ->
check_same_type e1 e2
@@ -298,7 +299,7 @@ and spaces ntn n =
if n = String.length ntn then []
else if ntn.[n] = ' ' then wildcards ntn (n+1) else spaces ntn (n+1)
-let expand_curly_brackets loc mknot ntn l =
+let expand_curly_brackets loc mknot ntn (l,ll) =
let ntn' = ref ntn in
let rec expand_ntn i =
function
@@ -311,12 +312,12 @@ let expand_curly_brackets loc mknot ntn l =
ntn' :=
String.sub !ntn' 0 p ^ "_" ^
String.sub !ntn' (p+5) (String.length !ntn' -p-5);
- mknot (loc,"{ _ }",[a]) end
+ mknot (loc,"{ _ }",([a],[])) end
else a in
a' :: expand_ntn (i+1) l in
let l = expand_ntn 0 l in
(* side effect *)
- mknot (loc,!ntn',l)
+ mknot (loc,!ntn',(l,ll))
let destPrim = function CPrim(_,t) -> Some t | _ -> None
let destPatPrim = function CPatPrim(_,t) -> Some t | _ -> None
@@ -324,18 +325,18 @@ let destPatPrim = function CPatPrim(_,t) -> Some t | _ -> None
let make_notation_gen loc ntn mknot mkprim destprim l =
if has_curly_brackets ntn
then expand_curly_brackets loc mknot ntn l
- else match ntn,List.map destprim l with
+ else match ntn,List.map destprim (fst l),(snd l) with
(* 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)])
+ | "- _", [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], [] ->
+ | [Terminal "-"; Terminal x], ([],[]) ->
(try mkprim (loc, Numeral (Bigint.neg (Bigint.of_string x)))
- with _ -> mknot (loc,ntn,[]))
- | [Terminal x], [] ->
+ with _ -> mknot (loc,ntn,([],[])))
+ | [Terminal x], ([],[]) ->
(try mkprim (loc, Numeral (Bigint.of_string x))
- with _ -> mknot (loc,ntn,[]))
+ with _ -> mknot (loc,ntn,([],[])))
| _ ->
mknot (loc,ntn,l)
@@ -351,13 +352,13 @@ let make_pat_notation loc ntn l =
(fun (loc,p) -> CPatPrim (loc,p))
destPatPrim l
-let bind_env sigma var v =
+let bind_env (sigma,sigmalist as fullsigma) var v =
try
let vvar = List.assoc var sigma in
- if v=vvar then sigma else raise No_match
+ 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
+ (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
@@ -378,15 +379,18 @@ let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with
(* 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,pat) =
- let subst = match_cases_pattern (List.map fst metas_scl) [] c pat in
+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
+ 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 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 =
@@ -424,7 +428,7 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
| PatCstr (loc,_,_,na),_ -> loc,na
| PatVar (loc,na),_ -> loc,na in
(* Try matching ... *)
- let subst = match_aconstr_cases_pattern t pat in
+ let subst,substlist = match_aconstr_cases_pattern t pat in
(* Try availability of interpretation ... *)
let p = match keyrule with
| NotationRule (sc,ntn) ->
@@ -438,7 +442,13 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
List.map (fun (c,(scopt,scl)) ->
extern_cases_pattern_in_scope (scopt,scl@scopes') vars c)
subst in
- insert_pat_delimiters loc (make_pat_notation loc ntn l) key)
+ let ll =
+ List.map (fun (c,(scopt,scl)) ->
+ let subscope = (scopt,scl@scopes') in
+ List.map (extern_cases_pattern_in_scope subscope vars) c)
+ substlist in
+ 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
@@ -544,15 +554,10 @@ let rec remove_coercions inctx = function
(* We skip a coercion *)
let l = list_skipn n args in
let (a,l) = match l with a::l -> (a,l) | [] -> assert false in
- let (a,l) =
- (* Recursively remove the head coercions *)
- match remove_coercions true a with
- | RApp (_,a,l') -> a,l'@l
- | a -> a,l in
- if l = [] then a
- else
- (* Recursively remove coercions in arguments *)
- RApp (loc,a,List.map (remove_coercions true) l)
+ (* Recursively remove the head coercions *)
+ (match remove_coercions true a with
+ | RApp (_,a,l') -> RApp (loc,a,l'@l)
+ | a -> RApp (loc,a,l))
| _ -> c
with Not_found -> c)
| c -> c
@@ -671,7 +676,7 @@ 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' =
List.fold_right (name_fold Idset.add)
@@ -694,7 +699,7 @@ let rec extern inctx scopes vars r =
| 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 (rtntypopt<>None) 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) ->
@@ -702,13 +707,13 @@ let rec extern inctx scopes vars r =
(Option.map (fun _ -> na) typopt,
Option.map (extern_typ scopes (add_vname vars na)) typopt),
sub_extern false scopes vars tm,
- extern false scopes (List.fold_left add_vname vars nal) b)
+ extern inctx scopes (List.fold_left add_vname vars nal) b)
| RIf (loc,c,(na,typopt),b1,b2) ->
CIf (loc,sub_extern false scopes vars c,
(Option.map (fun _ -> na) typopt,
Option.map (extern_typ scopes (add_vname vars na)) typopt),
- sub_extern false scopes vars b1, sub_extern false scopes vars b2)
+ sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2)
| RRec (loc,fk,idv,blv,tyv,bv) ->
let vars' = Array.fold_right Idset.add idv vars in
@@ -822,7 +827,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
| _, None -> t,[]
| _ -> raise No_match in
(* Try matching ... *)
- let subst = match_aconstr t pat in
+ let subst,substlist = match_aconstr t pat in
(* Try availability of interpretation ... *)
let e =
match keyrule with
@@ -838,7 +843,11 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
extern (* assuming no overloading: *) true
(scopt,scl@scopes') vars c)
subst in
- insert_delimiters (make_notation loc ntn l) key)
+ let ll =
+ List.map (fun (c,(scopt,scl)) ->
+ List.map (extern true (scopt,scl@scopes') vars) c)
+ substlist in
+ insert_delimiters (make_notation loc ntn (l,ll)) key)
| SynDefRule kn ->
let l =
List.map (fun (c,(scopt,scl)) ->
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 9af7e769..8d6a92a2 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: constrintern.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: constrintern.ml 11739 2009-01-02 19:33:19Z herbelin $ *)
open Pp
open Util
@@ -24,10 +24,63 @@ 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 =
- identifier list * Impargs.implicits_list * scope_name option list
+ 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
@@ -126,150 +179,6 @@ let error_inductive_parameter_not_implicit loc =
"the 'return' clauses; they must be replaced by '_' in the 'in' clauses."))
(**********************************************************************)
-(* Dump of globalization (to be used by coqdoc) *)
-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
-
-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"
-
-let remove_sections dir =
- if is_dirpath_prefix_of dir (Lib.cwd ()) then
- (* Not yet (fully) discharged *)
- extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ())
- else
- (* Theorem/Lemma outside its outer section of definition *)
- dir
-
-let dump_reference loc filepath modpath ident ty =
- dump_string (Printf.sprintf "R%d %s %s %s %s\n"
- (fst (unloc loc)) filepath modpath ident ty)
-
-let add_glob_gen loc sp lib_dp ty =
- 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_reference loc filepath modpath ident ty
-
-let add_glob loc ref =
- let sp = Nametab.sp_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 add_glob loc ref =
- if !Flags.dump && loc <> dummy_loc then add_glob loc ref
-
-let mp_of_kn kn =
- let mp,sec,l = repr_kn kn in
- MPdot (mp,l)
-
-let add_glob_kn loc kn =
- let sp = Nametab.sp_of_syntactic_definition kn in
- let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in
- add_glob_gen loc sp lib_dp "syndef"
-
-let add_glob_kn loc ref =
- if !Flags.dump && loc <> dummy_loc then add_glob_kn loc ref
-
-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 loc_of_notation f loc args ntn =
- if args=[] or ntn.[0] <> '_' then fst (unloc loc)
- else snd (unloc (f (List.hd args)))
-
-let ntn_loc = loc_of_notation constr_loc
-let patntn_loc = loc_of_notation cases_pattern_expr_loc
-
-let dump_notation_location pos ((path,df),sc) =
- let rec next growing =
- let loc = Lexer.location_function !token_number in
- let (bp,_) = 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 = string_of_dirpath path in
- let _sc = match sc with Some sc -> " "^sc | None -> "" in
- dump_string (Printf.sprintf "R%d %s \"%s\" not\n" (fst (unloc loc)) path df)
-
-(**********************************************************************)
(* Contracting "{ _ }" in notations *)
let rec wildcards ntn n =
@@ -289,38 +198,38 @@ let expand_notation_string ntn n =
(* This contracts the special case of "{ _ }" for sumbool, sumor notations *)
(* Remark: expansion of squash at definition is done in metasyntax.ml *)
-let contract_notation ntn l =
+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 ->
a::contract_squash (n+1) l in
let l = contract_squash 0 l in
(* side effect; don't inline *)
- !ntn',l
+ !ntn',(l,ll)
-let contract_pat_notation ntn l =
+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 ->
a::contract_squash (n+1) l in
let l = contract_squash 0 l in
(* side effect; don't inline *)
- !ntn',l
+ !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 set_var_scope loc id (_,scopt,scopes) varscopes =
+let set_var_scope loc id (_,_,scopt,scopes) varscopes =
let idscopes = List.assoc id varscopes in
if !idscopes <> None &
make_current_scope (Option.get !idscopes)
@@ -333,38 +242,37 @@ let set_var_scope loc id (_,scopt,scopes) varscopes =
(**********************************************************************)
(* Syntax extensions *)
-let traverse_binder subst (renaming,(ids,tmpsc,scopes as env)) id =
+let traverse_binder (subst,substlist) (renaming,(ids,unb,tmpsc,scopes as env)) 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,tmpsc,scopes)), id'
+ (renaming,(Idset.add id' ids,unb,tmpsc,scopes)), id'
with Not_found ->
(* Binders not bound in the notation do not capture variables *)
(* outside the notation (i.e. in the substitution) *)
let fvs1 = List.map (fun (_,(c,_)) -> free_vars_of_constr_expr c) subst in
- let fvs2 = List.map snd renaming in
- let fvs = List.flatten (List.map Idset.elements fvs1) @ fvs2 in
+ let fvs2 = List.flatten (List.map (fun (_,(l,_)) -> List.map free_vars_of_constr_expr l) substlist) in
+ let fvs3 = List.map snd renaming in
+ 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'
-let decode_constrlist_value = function
- | CAppExpl (_,_,l) -> l
- | _ -> anomaly "Ill-formed list argument of notation"
-
let rec subst_iterator y t = function
| RVar (_,id) as x -> if id = y then t else x
| x -> map_rawconstr (subst_iterator y t) x
-let rec subst_aconstr_in_rawconstr loc interp subst (renaming,(ids,_,scopes)) =
- function
+let rec subst_aconstr_in_rawconstr loc interp (subst,substlist as sub) infos c =
+ let (renaming,(ids,unb,_,scopes)) = infos in
+ let subinfos = renaming,(ids,unb,None,scopes) in
+ match c with
| AVar id ->
begin
(* subst remembers the delimiters stack in the interpretation *)
(* of the notations *)
try
let (a,(scopt,subscopes)) = List.assoc id subst in
- interp (ids,scopt,subscopes@scopes) a
+ interp (ids,unb,scopt,subscopes@scopes) a
with Not_found ->
try
RVar (loc,List.assoc id renaming)
@@ -375,36 +283,33 @@ let rec subst_aconstr_in_rawconstr loc interp subst (renaming,(ids,_,scopes)) =
| AList (x,_,iter,terminator,lassoc) ->
(try
(* All elements of the list are in scopes (scopt,subscopes) *)
- let (a,(scopt,subscopes)) = List.assoc x subst in
+ let (l,(scopt,subscopes)) = List.assoc x substlist in
let termin =
- subst_aconstr_in_rawconstr loc interp subst
- (renaming,(ids,None,scopes)) terminator in
- let l = decode_constrlist_value a in
+ subst_aconstr_in_rawconstr loc interp sub subinfos terminator in
List.fold_right (fun a t ->
subst_iterator ldots_var t
(subst_aconstr_in_rawconstr loc interp
- ((x,(a,(scopt,subscopes)))::subst)
- (renaming,(ids,None,scopes)) iter))
+ ((x,(a,(scopt,subscopes)))::subst,substlist) subinfos iter))
(if lassoc then List.rev l else l) termin
with Not_found ->
anomaly "Inconsistent substitution of recursive notation")
| t ->
- rawconstr_of_aconstr_with_binders loc (traverse_binder subst)
- (subst_aconstr_in_rawconstr loc interp subst)
- (renaming,(ids,None,scopes)) 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 args =
- let ntn,args = contract_notation ntn args in
- let ((ids,c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
- if !dump then dump_notation_location (ntn_loc loc args ntn) df;
- let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
- subst_aconstr_in_rawconstr loc intern subst ([],env) c
+let intern_notation intern (_,_,tmp_scope,scopes as env) loc ntn fullargs =
+ let ntn,(args,argslist) = 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
-let set_type_scope (ids,tmp_scope,scopes) =
- (ids,Some Notation.type_scope,scopes)
+let set_type_scope (ids,unb,tmp_scope,scopes) =
+ (ids,unb,Some Notation.type_scope,scopes)
-let reset_tmp_scope (ids,tmp_scope,scopes) =
- (ids,None,scopes)
+let reset_tmp_scope (ids,unb,tmp_scope,scopes) =
+ (ids,unb,None,scopes)
let rec it_mkRProd env body =
match env with
@@ -423,19 +328,26 @@ let rec it_mkRLambda env body =
[vars2] is the set of global variables, env is the set of variables
abstracted until this point *)
-let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) loc id =
+let string_of_ty = function
+ | Inductive -> "ind"
+ | Recursive -> "def"
+ | Method -> "meth"
+
+let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) loc id =
let (vars1,unbndltacvars) = ltacvars in
(* Is [id] an inductive type potentially with implicit *)
try
- let l,impl,argsc = List.assoc id impls in
+ 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
- RVar (loc,id), impl, argsc, l
+ let tys = string_of_ty ty in
+ Dumpglob.dump_reference loc "<>" (string_of_id id) tys;
+ RVar (loc,id), impl, argsc, l
with Not_found ->
(* Is [id] bound in current env or is an ltac var bound to constr *)
if Idset.mem id env or List.mem id vars1
then
- RVar (loc,id), [], [], []
+ RVar (loc,id), [], [], []
(* Is [id] a notation variable *)
else if List.mem_assoc id vars3
then
@@ -449,17 +361,17 @@ let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) loc id =
str "variable " ++ pr_id id ++ str " should be bound to a term.")
| Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
with Not_found ->
- (* Is [id] a goal or section variable *)
- let _ = Sign.lookup_named id vars2 in
- try
- (* [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, []
- with _ ->
- (* [id] a goal variable *)
- RVar (loc,id), [], [], []
-
+ (* Is [id] a goal or section variable *)
+ let _ = Sign.lookup_named id vars2 in
+ try
+ (* [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, []
+ with _ ->
+ (* [id] a goal variable *)
+ RVar (loc,id), [], [], []
+
let find_appl_head_data (_,_,_,(_,impls)) = function
| RRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[]
| x -> x,[],[],[]
@@ -478,17 +390,17 @@ let check_no_explicitation l =
let intern_qualid loc qid intern env args =
try match Nametab.extended_locate qid with
| TrueGlobal ref ->
- add_glob loc ref;
+ Dumpglob.add_glob loc ref;
RRef (loc, ref), args
| SyntacticDef sp ->
- add_glob_kn loc sp;
+ Dumpglob.add_glob_kn loc sp;
let (ids,c) = Syntax_def.search_syntactic_definition loc 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
+ subst_aconstr_in_rawconstr loc intern (subst,[]) ([],env) c, args2
with Not_found ->
error_global_not_found_loc loc qid
@@ -498,10 +410,10 @@ let intern_non_secvar_qualid loc qid intern env args =
| RRef (loc, VarRef id),_ -> error_global_not_found_loc loc qid
| r -> r
-let intern_applied_reference intern env lvar args = function
+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 lvar r, args2
| Ident (loc, id) ->
try intern_var env lvar loc id, args
with Not_found ->
@@ -511,18 +423,19 @@ let intern_applied_reference intern env lvar args = function
find_appl_head_data lvar r, args2
with e ->
(* Extra allowance for non globalizing functions *)
- if !interning_grammar then (RVar (loc,id), [], [], []),args
+ 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)
- (Idset.empty,None,[]) (vars,[],[],([],[])) [] r
+ (Idset.empty,false,None,[]) (vars,[],[],([],[])) [] r
in r
-let apply_scope_env (ids,_,scopes) = function
- | [] -> (ids,None,scopes), []
- | sc::scl -> (ids,sc,scopes), scl
+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
| [] -> []
@@ -595,8 +508,8 @@ let check_constructor_length env loc cstr pl pl0 =
(* [merge_aliases] returns the sets of all aliases encountered at this
point and a substitution mapping extra aliases to the first one *)
-let merge_aliases (ids,subst as _aliases) id =
- ids@[id], if ids=[] then subst else (id, List.hd ids)::subst
+let merge_aliases (ids,asubst as _aliases) id =
+ ids@[id], if ids=[] then asubst else (id, List.hd ids)::asubst
let alias_of = function
| ([],_) -> Anonymous
@@ -618,10 +531,6 @@ let chop_aconstr_constructor loc (ind,k) args =
| _ -> error_invalid_pattern_notation loc) params;
args
-let decode_patlist_value = function
- | CPatCstr (_,_,l) -> l
- | _ -> anomaly "Ill-formed list argument of notation"
-
let rec subst_pat_iterator y t (subst,p) = match p with
| PatVar (_,id) as x ->
if id = Name y then t else [subst,x]
@@ -630,8 +539,8 @@ let rec subst_pat_iterator y t (subst,p) = match p with
let pl = simple_product_of_cases_patterns l' in
List.map (fun (subst',pl) -> subst'@subst,PatCstr (loc,id,pl,alias)) pl
-let subst_cases_pattern loc alias intern subst scopes a =
- let rec aux alias subst = function
+let subst_cases_pattern loc alias intern fullsubst scopes a =
+ let rec aux alias (subst,substlist as fullsubst) = function
| AVar id ->
begin
(* subst remembers the delimiters stack in the interpretation *)
@@ -653,30 +562,29 @@ let subst_cases_pattern loc alias intern subst scopes a =
([],[[], PatCstr (loc,c, [], alias)])
| AApp (ARef (ConstructRef cstr),args) ->
let args = chop_aconstr_constructor loc cstr args in
- let idslpll = List.map (aux Anonymous subst) 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 (subst,pl) ->
- subst,PatCstr (loc,cstr,pl,alias)) pll in
+ let pl' = List.map (fun (asubst,pl) ->
+ asubst,PatCstr (loc,cstr,pl,alias)) pll in
ids', pl'
| AList (x,_,iter,terminator,lassoc) ->
(try
(* All elements of the list are in scopes (scopt,subscopes) *)
- let (a,(scopt,subscopes)) = List.assoc x subst in
- let termin = aux Anonymous subst terminator in
- let l = decode_patlist_value a in
+ 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) ->
- let uids,u = aux Anonymous ((x,(a,(scopt,subscopes)))::subst) iter in
+ 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 ((subst, pl) as x) ->
- match pl with PatCstr (loc, c, pl, Anonymous) -> (subst, PatCstr (loc, c, pl, alias)) | _ -> x) v
+ 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 ->
anomaly "Inconsistent substitution of recursive notation")
| t -> error_invalid_pattern_notation loc
- in aux alias subst a
-
+ in aux alias fullsubst a
+
(* Differentiating between constructors and matching variables *)
type pattern_qualid_kind =
| ConstrPat of constructor * (identifier list *
@@ -701,7 +609,7 @@ let find_constructor ref f aliases pats scopes =
if List.length pats < nvars then error_not_enough_arguments loc;
let pats1,pats2 = list_chop nvars pats in
let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) vars pats1 in
- let idspl1 = List.map (subst_cases_pattern loc (alias_of aliases) f subst scopes) args in
+ let idspl1 = List.map (subst_cases_pattern loc (alias_of aliases) f (subst,[]) scopes) args in
cstr, idspl1, pats2
| _ -> raise Not_found)
@@ -711,7 +619,7 @@ let find_constructor ref f aliases pats scopes =
let v = Environ.constant_value (Global.env()) cst in
unf (global_of_constr v)
| ConstructRef cstr ->
- add_glob loc r;
+ Dumpglob.add_glob loc r;
cstr, [], pats
| _ -> raise Not_found
in unf r
@@ -739,7 +647,7 @@ let mustbe_constructor loc ref f aliases patl scopes =
with (Environ.NotEvaluableConst _ | Not_found) ->
raise (InternalisationError (loc,NotAConstructor ref))
-let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope pat =
+let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat=
let intern_pat = intern_cases_pattern genv in
match pat with
| CPatAlias (loc, p, id) ->
@@ -751,28 +659,30 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope pat =
let argscs2 = find_remaining_constructor_scopes idslpl1 pl2 c in
let idslpl2 = List.map2 (intern_pat scopes ([],[])) argscs2 pl2 in
let (ids',pll) = product_of_cases_patterns ids (idslpl1@idslpl2) in
- let pl' = List.map (fun (subst,pl) ->
- (subst, PatCstr (loc,c,pl,alias_of aliases))) pll in
+ let pl' = List.map (fun (asubst,pl) ->
+ (asubst, PatCstr (loc,c,pl,alias_of aliases))) pll in
ids',pl'
- | CPatNotation (loc,"- _",[CPatPrim(_,Numeral p)])
+ | CPatNotation (loc,"- _",([CPatPrim(_,Numeral p)],[]))
when Bigint.is_strictly_pos p ->
intern_pat scopes aliases tmp_scope (CPatPrim(loc,Numeral(Bigint.neg p)))
- | CPatNotation (_,"( _ )",[a]) ->
+ | CPatNotation (_,"( _ )",([a],[])) ->
intern_pat scopes aliases tmp_scope a
- | CPatNotation (loc, ntn, args) ->
- let ntn,args = contract_pat_notation ntn args in
- let ((ids',c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
- if !dump then dump_notation_location (patntn_loc loc args ntn) df;
+ | CPatNotation (loc, ntn, fullargs) ->
+ let ntn,(args,argsl) = 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;
let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in
- let ids'',pl = subst_cases_pattern loc (alias_of aliases) intern_pat subst scopes
- c
+ let substlist = List.map2 (fun (id,scl) a -> (id,(a,scl))) idsl' argsl in
+ let ids'',pl =
+ subst_cases_pattern loc (alias_of aliases) intern_pat (subst,substlist)
+ scopes c
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
(tmp_scope,scopes) in
- if !dump then dump_notation_location (fst (unloc loc)) df;
- (ids,[subst,c])
+ 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
| CPatAtom (loc, Some head) ->
@@ -780,13 +690,13 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope pat =
| ConstrPat (c,idspl) ->
check_constructor_length genv loc c idspl [];
let (ids',pll) = product_of_cases_patterns ids idspl in
- (ids,List.map (fun (subst,pl) ->
- (subst, PatCstr (loc,c,pl,alias_of aliases))) pll)
+ (ids,List.map (fun (asubst,pl) ->
+ (asubst, PatCstr (loc,c,pl,alias_of aliases))) pll)
| VarPat id ->
- let ids,subst = merge_aliases aliases id in
- (ids,[subst, PatVar (loc,alias_of (ids,subst))]))
+ let ids,asubst = merge_aliases aliases id in
+ (ids,[asubst, PatVar (loc,alias_of (ids,asubst))]))
| CPatAtom (loc, None) ->
- (ids,[subst, PatVar (loc,alias_of aliases)])
+ (ids,[asubst, PatVar (loc,alias_of aliases)])
| CPatOr (loc, pl) ->
assert (pl <> []);
let pl' = List.map (intern_pat scopes aliases tmp_scope) pl in
@@ -821,48 +731,90 @@ let check_hidden_implicit_parameters id (_,_,_,(indnames,_)) =
pr_id id ++ strbrk " must not be used as a bound variable in the type \
of its constructor.")
-let push_name_env lvar (ids,tmpsc,scopes as env) = function
- | Anonymous -> env
+let push_name_env ?(fail_anonymous=false) lvar (ids,unb,tmpsc,scopes as env) = function
+ | Anonymous ->
+ if fail_anonymous then errorlabstrm "" (str "Anonymous variables not allowed");
+ env
| Name id ->
check_hidden_implicit_parameters id lvar;
- (Idset.add id ids,tmpsc,scopes)
+ (Idset.add id ids, unb,tmpsc,scopes)
-let push_loc_name_env lvar (ids,tmpsc,scopes as env) loc = function
- | Anonymous -> env
+let push_loc_name_env ?(fail_anonymous=false) lvar (ids,unb,tmpsc,scopes as env) loc = function
+ | Anonymous ->
+ if fail_anonymous then user_err_loc (loc,"", str "Anonymous variables not allowed");
+ env
| Name id ->
check_hidden_implicit_parameters id lvar;
- dump_binding loc id;
- (Idset.add id ids,tmpsc,scopes)
-
-let intern_typeclass_binders intern_type lvar env bl =
- List.fold_left
- (fun ((ids,ts,sc) as env,bl) ((loc, na), bk, ty) ->
- let env = push_loc_name_env lvar env loc na in
- let ty = locate_if_isevar loc na (intern_type env ty) in
- (env, (na,bk,None,ty)::bl))
- env bl
-
-let intern_typeclass_binder intern_type lvar (env,bl) cb =
- let (ids, fvs, bind) = Implicit_quantifiers.generalize_class_binder_raw (pi1 env) cb in
- intern_typeclass_binders intern_type lvar (env,bl) (fvs@[bind])
-
-let intern_local_binder_aux intern intern_type lvar ((ids,ts,sc as env),bl) = function
+ 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
+ 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 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
+ else
+ 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 Name name
+ | _ -> na
+ in (push_loc_name_env ~fail_anonymous lvar env' loc na), (na,b',None,ty') :: List.rev bl
+
+let intern_local_binder_aux ?(fail_anonymous=false) intern intern_type lvar ((ids,unb,ts,sc as env),bl) = function
| LocalRawAssum(nal,bk,ty) ->
(match bk with
- | Default k ->
- let (loc,na) = List.hd nal in
- (* TODO: fail if several names with different implicit types *)
- let ty = locate_if_isevar loc na (intern_type env ty) in
- List.fold_left
- (fun ((ids,ts,sc),bl) (_,na) ->
- ((name_fold Idset.add na ids,ts,sc), (na,k,None,ty)::bl))
- (env,bl) nal
- | TypeClass (b,b') ->
- intern_typeclass_binder intern_type lvar (env,bl) (List.hd nal, (b,b'), ty))
+ | Default k ->
+ let (loc,na) = List.hd nal in
+ (* TODO: fail if several names with different implicit types *)
+ let ty = locate_if_isevar loc na (intern_type env ty) in
+ List.fold_left
+ (fun ((ids,unb,ts,sc),bl) (_,na) ->
+ ((name_fold Idset.add na ids,unb,ts,sc), (na,k,None,ty)::bl))
+ (env,bl) nal
+ | Generalized (b,b',t) ->
+ let env, b = intern_generalized_binder ~fail_anonymous intern_type lvar env bl (List.hd nal) b b' t ty in
+ env, b @ bl)
| LocalRawDef((loc,na),def) ->
- ((name_fold Idset.add na ids,ts,sc),
+ ((name_fold Idset.add na ids,unb,ts,sc),
(na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
+let intern_generalization intern (ids,unb,tmp_scope,scopes as env) lvar loc bk ak c =
+ let c = intern (ids,true,tmp_scope,scopes) c in
+ let fvs = Implicit_quantifiers.free_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
+ || List.mem Notation.type_scope scopes -> true
+ | _ -> false
+ in
+ if pi then
+ (fun (id, loc') acc ->
+ RProd (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc))
+ else
+ (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) ->
+ let env' = push_loc_name_env lvar env loc (Name id) in
+ (env', abs lid acc)) fvs (env,c)
+ in c'
+
(**********************************************************************)
(* Utilities for application *)
@@ -936,7 +888,7 @@ let extract_explicit_arg imps args =
(* Main loop *)
let internalise sigma globalenv env allow_patvar lvar c =
- let rec intern (ids,tmp_scope,scopes as env) = function
+ let rec intern (ids,unb,tmp_scope,scopes as env) = function
| CRef ref as x ->
let (c,imp,subscopes,l),_ =
intern_applied_reference intern env lvar [] ref in
@@ -960,17 +912,17 @@ let internalise sigma globalenv env allow_patvar lvar c =
| None -> 0
in
let before, after = list_chop idx bl in
- let ((ids',_,_) as env',rbefore) =
+ 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', tmp_scope, scopes) c')
+ | Some c' -> f (intern (ids', unb, tmp_scope, scopes) c')
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) =
+ let n, ro, ((ids',_,_,_),rbl) =
(match order with
| CStructRec ->
intern_ro_arg None (fun _ -> RStructRec)
@@ -981,8 +933,8 @@ let internalise sigma globalenv env allow_patvar lvar c =
in
let ids'' = List.fold_right Idset.add lf ids' in
((n, ro), List.rev rbl,
- intern_type (ids',tmp_scope,scopes) ty,
- intern (ids'',None,scopes) bd)) dl in
+ intern_type (ids',unb,tmp_scope,scopes) ty,
+ intern (ids'',unb,None,scopes) bd)) dl in
RRec (loc,RFix
(Array.map (fun (ro,_,_,_) -> ro) idl,n),
Array.of_list lf,
@@ -999,12 +951,12 @@ let internalise sigma globalenv env allow_patvar lvar c =
in
let idl = Array.map
(fun (id,bl,ty,bd) ->
- let ((ids',_,_),rbl) =
+ let ((ids',_,_,_),rbl) =
List.fold_left intern_local_binder (env,[]) bl in
let ids'' = List.fold_right Idset.add lf ids' in
(List.rev rbl,
- intern_type (ids',tmp_scope,scopes) ty,
- intern (ids'',None,scopes) bd)) dl in
+ intern_type (ids',unb,tmp_scope,scopes) ty,
+ intern (ids'',unb,None,scopes) bd)) dl in
RRec (loc,RCoFix n,
Array.of_list lf,
Array.map (fun (bl,_,_) -> bl) idl,
@@ -1023,18 +975,20 @@ let internalise sigma globalenv env allow_patvar lvar c =
| CLetIn (loc,(loc1,na),c1,c2) ->
RLetIn (loc, na, intern (reset_tmp_scope env) c1,
intern (push_loc_name_env lvar env loc1 na) c2)
- | CNotation (loc,"- _",[CPrim (_,Numeral p)])
+ | CNotation (loc,"- _",([CPrim (_,Numeral p)],[]))
when Bigint.is_strictly_pos p ->
intern env (CPrim (loc,Numeral (Bigint.neg p)))
- | CNotation (_,"( _ )",[a]) -> intern env a
+ | CNotation (_,"( _ )",([a],[])) -> intern env a
| CNotation (loc,ntn,args) ->
intern_notation intern env loc ntn args
+ | 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
- if !dump then dump_notation_location (fst (unloc loc)) df;
+ Dumpglob.dump_notation_location (fst (unloc loc)) df;
c
| CDelimiters (loc, key, e) ->
- intern (ids,None,find_delimiters_scope loc key::scopes) e
+ intern (ids,unb,None,find_delimiters_scope loc key::scopes) e
| CAppExpl (loc, (isproj,ref), args) ->
let (f,_,args_scopes,_),args =
let args = List.map (fun a -> (a,None)) args in
@@ -1050,8 +1004,8 @@ let internalise sigma globalenv env allow_patvar lvar c =
let (c,impargs,args_scopes,l),args =
match f with
| CRef ref -> intern_applied_reference intern env lvar args ref
- | CNotation (loc,ntn,[]) ->
- let c = intern_notation intern env loc ntn [] in
+ | CNotation (loc,ntn,([],[])) ->
+ let c = intern_notation intern env loc ntn ([],[]) in
find_appl_head_data lvar c, args
| x -> (intern env f,[],[],[]), args in
let args =
@@ -1061,6 +1015,39 @@ let internalise sigma globalenv env allow_patvar lvar c =
(* 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
+ intern env app
+
| CCases (loc, sty, rtnpo, tms, eqns) ->
let tms,env' = List.fold_right
(fun citm (inds,env) ->
@@ -1084,7 +1071,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
let p' = Option.map (intern_type env'') po in
RIf (loc, c', (na', p'), intern env b1, intern env b2)
| CHole (loc, k) ->
- RHole (loc, match k with Some k -> k | None -> Evd.QuestionMark true)
+ RHole (loc, match k with Some k -> k | None -> Evd.QuestionMark (Evd.Define true))
| CPatVar (loc, n) when allow_patvar ->
RPatVar (loc, n)
| CPatVar (loc, _) ->
@@ -1122,24 +1109,24 @@ let internalise sigma globalenv env allow_patvar lvar c =
(ids,List.flatten mpl')
(* Expands a pattern-matching clause [lhs => rhs] *)
- and intern_eqn n (ids,tmp_scope,scopes) (loc,lhs,rhs) =
+ and intern_eqn n (ids,unb,tmp_scope,scopes) (loc,lhs,rhs) =
let eqn_ids,pll = intern_disjunctive_multiple_pattern scopes loc n lhs in
(* Linearity implies the order in ids is irrelevant *)
check_linearity lhs eqn_ids;
let env_ids = List.fold_right Idset.add eqn_ids ids in
- List.map (fun (subst,pl) ->
- let rhs = replace_vars_constr_expr subst rhs in
- List.iter message_redundant_alias subst;
- let rhs' = intern (env_ids,tmp_scope,scopes) rhs in
+ List.map (fun (asubst,pl) ->
+ let rhs = replace_vars_constr_expr asubst rhs in
+ List.iter message_redundant_alias asubst;
+ let rhs' = intern (env_ids,unb,tmp_scope,scopes) rhs in
(loc,eqn_ids,pl,rhs')) pll
- and intern_case_item (vars,_,scopes as env) (tm,(na,t)) =
+ 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 ->
let tids = ids_of_cases_indtype t in
let tids = List.fold_right Idset.add tids Idset.empty in
- let t = intern_type (tids,None,scopes) t in
+ let t = intern_type (tids,unb,None,scopes) t in
let loc,ind,l = match t with
| RRef (loc,IndRef ind) -> (loc,ind,[])
| RApp (loc,RRef (_,IndRef ind),l) -> (loc,ind,l)
@@ -1175,9 +1162,9 @@ let internalise sigma globalenv env allow_patvar lvar c =
in
match bk with
| Default b -> default env b nal
- | TypeClass (b,b') ->
- let env, ibind = intern_typeclass_binder intern_type lvar
- (env, []) (List.hd nal,(b,b'),ty) in
+ | 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
@@ -1191,9 +1178,9 @@ let internalise sigma globalenv env allow_patvar lvar c =
| [] -> intern env body
in match bk with
| Default b -> default env b nal
- | TypeClass (b, b') ->
- let env, ibind = intern_typeclass_binder intern_type lvar
- (env, []) (List.hd nal,(b,b'),ty) in
+ | 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
@@ -1258,7 +1245,7 @@ let intern_gen isarity sigma env
c =
let tmp_scope =
if isarity then Some Notation.type_scope else None in
- internalise sigma env (extract_ids env, tmp_scope,[])
+ 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
@@ -1340,22 +1327,23 @@ let interp_constr_judgment_evars evdref env c =
type ltac_sign = identifier list * unbound_ltac_var_map
-let interp_constrpattern sigma env c =
- pattern_of_rawconstr (intern_gen false sigma env ~allow_patvar:true c)
+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 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 in
- let c = internalise Evd.empty (Global.env()) (extract_ids env, None, [])
+ 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
(* 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 *)
- List.map
- (fun (id,r) -> (id,match !r with None -> None,[] | Some (a,l) -> a,l)) vl,
- a
+ 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
(* Interpret binders and contexts *)
@@ -1377,11 +1365,11 @@ let my_intern_constr sigma env lvar acc c =
let my_intern_type sigma env lvar acc c = my_intern_constr sigma env lvar (set_type_scope acc) c
-let intern_context sigma env params =
+let intern_context fail_anonymous sigma env params =
let lvar = (([],[]),Environ.named_context env, [], ([], [])) in
snd (List.fold_left
- (intern_local_binder_aux (my_intern_constr sigma env lvar) (my_intern_type sigma env lvar) lvar)
- ((extract_ids env,None,[]), []) 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 (env, par, _, impls) =
@@ -1402,17 +1390,17 @@ let interp_context_gen understand_type understand_judgment env bl =
| Some b ->
let c = understand_judgment env b in
let d = (na, Some c.uj_val, c.uj_type) in
- (push_rel d env,d::params, succ n, impls))
+ (push_rel d env, d::params, succ n, impls))
(env,[],1,[]) (List.rev bl)
in (env, par), impls
-let interp_context sigma env params =
- let bl = intern_context sigma env params in
+let interp_context ?(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 evdref env params =
- let bl = intern_context (Evd.evars_of !evdref) env params in
+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
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index ea7020be..c5371255 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 11024 2008-05-30 12:41:39Z msozeau $ i*)
+(*i $Id: constrintern.mli 11739 2009-01-02 19:33:19Z herbelin $ i*)
(*i*)
open Names
@@ -39,8 +39,10 @@ open Pretyping
argument associates a list of implicit positions and scopes to
identifiers declared in the [rel_context] of [env] *)
+type var_internalisation_type = Inductive | Recursive | Method
+
type var_internalisation_data =
- identifier list * Impargs.implicits_list * scope_name option list
+ 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
@@ -65,7 +67,7 @@ val intern_pattern : env -> cases_pattern_expr ->
Names.identifier list *
((Names.identifier * Names.identifier) list * Rawterm.cases_pattern) list
-val intern_context : evar_map -> env -> local_binder list -> raw_binder list
+val intern_context : bool -> evar_map -> env -> local_binder list -> raw_binder list
(*s Composing internalisation with pretyping *)
@@ -111,8 +113,9 @@ val interp_constr_judgment : evar_map -> env -> constr_expr -> unsafe_judgment
(* Interprets constr patterns *)
-val interp_constrpattern :
- evar_map -> env -> constr_expr -> patvar list * constr_pattern
+val intern_constr_pattern :
+ evar_map -> env -> ?as_type:bool -> ?ltacvars:ltac_sign ->
+ constr_pattern_expr -> patvar list * constr_pattern
val interp_reference : ltac_sign -> reference -> rawconstr
@@ -124,9 +127,10 @@ val interp_binder_evars : evar_defs ref -> env -> name -> constr_expr -> types
(* Interpret contexts: returns extended env and context *)
-val interp_context : 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 :
+val interp_context_evars : ?fail_anonymous:bool ->
evar_defs ref -> env -> local_binder list -> (env * rel_context) * manual_implicits
(* Locating references of constructions, possibly via a syntactic definition *)
@@ -139,15 +143,8 @@ val global_reference_in_absolute_module : dir_path -> identifier -> constr
(* Interprets into a abbreviatable constr *)
-val interp_aconstr : implicits_env -> identifier list -> constr_expr ->
- interpretation
+val interp_aconstr : implicits_env -> identifier list * identifier list
+ -> constr_expr -> interpretation
(* Globalization leak for Grammar *)
val for_grammar : ('a -> 'b) -> 'a -> 'b
-
-(* Coqdoc utility functions *)
-type coqdoc_state
-val coqdoc_freeze : unit -> coqdoc_state
-val coqdoc_unfreeze : coqdoc_state -> unit
-
-val add_glob : Util.loc -> global_reference -> unit
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
new file mode 100644
index 00000000..5ac584a7
--- /dev/null
+++ b/interp/dumpglob.ml
@@ -0,0 +1,228 @@
+(************************************************************************)
+(* 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: dumpglob.ml 11582 2008-11-12 19:49:57Z notin $ *)
+
+
+(* Dump of globalization (to be used by coqdoc) *)
+
+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 =
+ | NoGlob
+ | StdOut
+ | MultFiles
+ | File of string
+
+let glob_output = ref NoGlob
+
+let dump () = !glob_output != NoGlob
+
+let noglob () = glob_output := NoGlob
+
+let dump_to_stdout () = glob_output := StdOut; glob_file := Pervasives.stdout
+
+let multi_dump () = !glob_output = MultFiles
+
+let dump_to_dotglob f = glob_output := MultFiles
+
+let dump_into_file f = glob_output := File f; open_glob_file f
+
+let dump_string s =
+ if dump () then Pervasives.output_string !glob_file s
+
+
+let previous_state = ref MultFiles
+let pause () = previous_state := !glob_output; glob_output := NoGlob
+let continue () = glob_output := !previous_state
+
+
+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
+
+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
+ | Libnames.ConstRef cst ->
+ type_of_logical_kind (Decls.constant_kind cst)
+ | Libnames.VarRef v ->
+ "var" ^ type_of_logical_kind (Decls.variable_kind v)
+ | Libnames.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"
+ | Libnames.ConstructRef _ -> "constr"
+
+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 ())
+ 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"
+ (fst (Util.unloc loc)) filepath modpath ident ty)
+
+let add_glob_gen loc sp lib_dp ty =
+ if dump () then
+ let mod_dp,id = Libnames.repr_path sp in
+ let mod_dp = remove_sections mod_dp in
+ let mod_dp_trunc = Libnames.drop_dirpath_prefix lib_dp mod_dp in
+ let filepath = Names.string_of_dirpath lib_dp in
+ let modpath = Names.string_of_dirpath mod_dp_trunc in
+ let ident = Names.string_of_id id in
+ dump_ref loc filepath modpath ident ty
+
+let add_glob loc ref =
+ if dump () && loc <> Util.dummy_loc then
+ let sp = Nametab.sp_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 add_glob_kn loc kn =
+ if dump () && loc <> Util.dummy_loc then
+ let sp = Nametab.sp_of_syntactic_definition 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))
+ (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"
+ (fst (Util.unloc loc)) (Names.string_of_dirpath (Lib.library_dp ())) modpath ident ty)
+
+let dump_constraint ((loc, n), _, _) sec ty =
+ match n with
+ | Names.Name id -> dump_definition (loc, id) sec ty
+ | Names.Anonymous -> ()
+
+let dump_name (loc, n) sec ty =
+ match n with
+ | Names.Name id -> dump_definition (loc, id) sec ty
+ | Names.Anonymous -> ()
+
+let dump_local_binder b sec ty =
+ if dump () then
+ match b with
+ | Topconstr.LocalRawAssum (nl, _, _) ->
+ List.iter (fun x -> dump_name x sec ty) nl
+ | Topconstr.LocalRawDef _ -> ()
+
+let dump_modref loc mp ty =
+ if dump () then
+ let (dp, l) = Lib.split_modpath mp in
+ 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"
+ (fst (Util.unloc loc)) fp mp "<>" ty)
+
+let dump_moddef loc mp ty =
+ if dump () then
+ let (dp, l) = Lib.split_modpath mp in
+ let mp = Names.string_of_dirpath (Names.make_dirpath l) in
+ 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"
+ (fst (Util.unloc loc)) (Names.string_of_dirpath dp) ty)
+
+let dump_notation_location pos ((path,df),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)
+
+
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
new file mode 100644
index 00000000..a0666c81
--- /dev/null
+++ b/interp/dumpglob.mli
@@ -0,0 +1,43 @@
+(************************************************************************)
+(* 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: dumpglob.mli 11582 2008-11-12 19:49:57Z notin $ *)
+
+
+val open_glob_file : string -> unit
+val close_glob_file : unit -> unit
+
+val dump : unit -> bool
+val multi_dump : unit -> bool
+
+val noglob : unit -> unit
+val dump_to_stdout : unit -> unit
+val dump_into_file : string -> unit
+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
+
+val add_glob : Util.loc -> Libnames.global_reference -> unit
+val add_glob_kn : Util.loc -> Names.kernel_name -> unit
+
+val dump_definition : Util.loc * Names.identifier -> bool -> string -> unit
+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_binding : Util.loc -> Names.Idset.elt -> unit
+val dump_constraint : Topconstr.typeclass_constraint -> bool -> string -> unit
+val dump_local_binder : Topconstr.local_binder -> bool -> string -> unit
+
+val dump_string : string -> unit
+
diff --git a/interp/genarg.ml b/interp/genarg.ml
index c54dfe23..1da428be 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: genarg.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: genarg.ml 11481 2008-10-20 19:23:51Z herbelin $ *)
open Pp
open Util
@@ -26,7 +26,7 @@ type argument_type =
| StringArgType
| PreIdentArgType
| IntroPatternArgType
- | IdentArgType
+ | IdentArgType of bool
| VarArgType
| RefArgType
(* Specific types *)
@@ -45,7 +45,9 @@ type argument_type =
| ExtraArgType of string
type 'a and_short_name = 'a * identifier located option
-type 'a or_by_notation = AN of 'a | ByNotation of loc * string
+type 'a or_by_notation =
+ | AN of 'a
+ | ByNotation of loc * string * Notation.delimiters option
type rawconstr_and_expr = rawconstr * constr_expr option
type open_constr_expr = unit * constr_expr
@@ -124,9 +126,17 @@ let rawwit_intro_pattern = IntroPatternArgType
let globwit_intro_pattern = IntroPatternArgType
let wit_intro_pattern = IntroPatternArgType
-let rawwit_ident = IdentArgType
-let globwit_ident = IdentArgType
-let wit_ident = IdentArgType
+let rawwit_ident_gen b = IdentArgType b
+let globwit_ident_gen b = IdentArgType b
+let wit_ident_gen b = IdentArgType b
+
+let rawwit_ident = rawwit_ident_gen true
+let globwit_ident = globwit_ident_gen true
+let wit_ident = wit_ident_gen true
+
+let rawwit_pattern_ident = rawwit_ident_gen false
+let globwit_pattern_ident = globwit_ident_gen false
+let wit_pattern_ident = wit_ident_gen false
let rawwit_var = VarArgType
let globwit_var = VarArgType
diff --git a/interp/genarg.mli b/interp/genarg.mli
index da175078..86b19de7 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: genarg.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: genarg.mli 11481 2008-10-20 19:23:51Z herbelin $ i*)
open Util
open Names
@@ -19,7 +19,9 @@ open Evd
type 'a and_short_name = 'a * identifier located option
-type 'a or_by_notation = AN of 'a | ByNotation of loc * string
+type 'a or_by_notation =
+ | AN of 'a
+ | ByNotation of loc * string * Notation.delimiters option
(* In globalize tactics, we need to keep the initial [constr_expr] to recompute*)
(* in the environment by the effective calls to Intro, Inversion, etc *)
@@ -84,7 +86,8 @@ IntArgType int int
IntOrVarArgType int or_var int
StringArgType string (parsed w/ "") string
PreIdentArgType string (parsed w/o "") (vernac only)
-IdentArgType identifier identifier
+IdentArgType true identifier identifier
+IdentArgType false identifier (pattern_ident) identifier
IntroPatternArgType intro_pattern_expr intro_pattern_expr
VarArgType identifier located identifier
RefArgType reference global_reference
@@ -143,6 +146,14 @@ val rawwit_ident : (identifier,rlevel) abstract_argument_type
val globwit_ident : (identifier,glevel) abstract_argument_type
val wit_ident : (identifier,tlevel) abstract_argument_type
+val rawwit_pattern_ident : (identifier,rlevel) abstract_argument_type
+val globwit_pattern_ident : (identifier,glevel) abstract_argument_type
+val wit_pattern_ident : (identifier,tlevel) abstract_argument_type
+
+val rawwit_ident_gen : bool -> (identifier,rlevel) abstract_argument_type
+val globwit_ident_gen : bool -> (identifier,glevel) abstract_argument_type
+val wit_ident_gen : bool -> (identifier,tlevel) abstract_argument_type
+
val rawwit_var : (identifier located,rlevel) abstract_argument_type
val globwit_var : (identifier located,glevel) abstract_argument_type
val wit_var : (identifier,tlevel) abstract_argument_type
@@ -255,7 +266,7 @@ type argument_type =
| StringArgType
| PreIdentArgType
| IntroPatternArgType
- | IdentArgType
+ | IdentArgType of bool
| VarArgType
| RefArgType
(* Specific types *)
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index a83071d1..d6e207f3 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 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: implicit_quantifiers.ml 11576 2008-11-10 19:13:15Z msozeau $ i*)
(*i*)
open Names
@@ -58,7 +58,7 @@ let free_vars_of_constr_expr c ?(bound=Idset.empty) l =
in
let rec aux bdvars l c = match c with
| CRef (Ident (_,id)) -> found id bdvars l
- | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id))) :: _) when not (Idset.mem id bdvars) ->
+ | 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
@@ -81,17 +81,84 @@ let free_vars_of_binders ?(bound=Idset.empty) l (binders : local_binder list) =
| [] -> 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 rec vars bound vs = function
+ | RVar (loc,id) ->
+ if is_freevar bound (Global.env ()) id then
+ if List.mem_assoc id vs then vs
+ else (id, loc) :: vs
+ else vs
+ | RApp (loc,f,args) -> List.fold_left (vars bound) vs (f::args)
+ | RLambda (loc,na,_,ty,c) | RProd (loc,na,_,ty,c) | RLetIn (loc,na,ty,c) ->
+ 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
+ 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 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
+ 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 vs'' = vars bound vs' bty 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
+ 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
+ (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
+ 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
+ vars_option bound' vs tyopt
+ in
+ fun rt -> List.rev (vars bound [] rt)
+
let rec make_fresh ids env x =
if is_freevar ids env x then x else make_fresh ids env (Nameops.lift_ident x)
let freevars_of_ids env ids =
List.filter (is_freevar env (Global.env())) ids
-
-let binder_list_of_ids ids =
- List.map (fun id -> LocalRawAssum ([dummy_loc, Name id], Default Implicit, CHole (dummy_loc, None))) ids
let next_ident_away_from id avoid = make_fresh avoid (Global.env ()) id
-
+
+let next_name_away_from na avoid =
+ match na with
+ | Anonymous -> make_fresh avoid (Global.env ()) (id_of_string "anon")
+ | Name id -> make_fresh avoid (Global.env ()) id
+
let combine_params avoid fn applied needed =
let named, applied =
List.partition
@@ -116,7 +183,7 @@ let combine_params avoid fn applied needed =
| (x, None) :: app, (None, (Name id, _, _)) :: need ->
aux (x :: ids) avoid app need
- | _, (Some cl, (Name id, _, _) as d) :: need ->
+ | _, (Some cl, (_, _, _) as d) :: need ->
let t', avoid' = fn avoid d in
aux (t' :: ids) avoid' app need
@@ -126,26 +193,19 @@ let combine_params avoid fn applied needed =
let t', avoid' = fn avoid decl in
aux (t' :: ids) avoid' app need
- | _ :: _, [] -> failwith "combine_params: overly applied typeclass"
-
- | _, _ -> raise (Invalid_argument "combine_params")
+ | (x,_) :: _, [] ->
+ user_err_loc (constr_loc x,"",str "Typeclass does not expect more arguments")
in aux [] avoid applied needed
-let combine_params_freevar avoid applied needed =
- combine_params avoid
- (fun avoid (_, (id, _, _)) ->
- let id' = next_ident_away_from (Nameops.out_name id) avoid in
- (CRef (Ident (dummy_loc, id')), Idset.add id' avoid))
- applied needed
-
-let compute_context_vars env l =
- List.fold_left (fun avoid (iid, _, c) ->
- (match snd iid with Name i -> [i] | Anonymous -> []) @ (free_vars_of_constr_expr c ~bound:env avoid))
- [] l
-
+let combine_params_freevar =
+ 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
+ | CAppExpl (loc, (None, ref), l) -> loc, ref, l
| CRef ref -> loc_of_reference ref, ref, []
| _ -> raise Not_found
@@ -155,88 +215,34 @@ let destClassAppExpl cl =
| CRef ref -> loc_of_reference ref, ref, []
| _ -> raise Not_found
-let full_class_binders env l =
- let avoid = Idset.union env (ids_of_list (compute_context_vars env l)) in
- let l', avoid =
- List.fold_left (fun (l', avoid) (iid, bk, cl as x) ->
- match bk with
- Implicit ->
- let (loc, id, l) =
- try destClassAppExpl cl
- with Not_found ->
- user_err_loc (constr_loc cl, "class_binders", str"Not an applied type class")
- in
- let gr = Nametab.global id in
- (try
- let c = class_info gr in
- let args, avoid = combine_params_freevar avoid l (List.rev c.cl_context) in
- (iid, bk, CAppExpl (loc, (None, id), args)) :: l', avoid
- with Not_found -> not_a_class (Global.env ()) (constr_of_global gr))
- | Explicit -> (x :: l', avoid))
- ([], avoid) l
- in List.rev l'
-
-let compute_context_freevars env ctx =
- let bound, ids =
- List.fold_left
- (fun (bound, acc) (oid, id, x) ->
- let bound = match snd oid with Name n -> Idset.add n bound | Anonymous -> bound in
- bound, free_vars_of_constr_expr x ~bound acc)
- (env,[]) ctx
- in freevars_of_ids env (List.rev ids)
-
-let resolve_class_binders env l =
- let ctx = full_class_binders env l in
- let fv_ctx =
- let elts = compute_context_freevars env ctx in
- List.map (fun id -> (dummy_loc, id), CHole (dummy_loc, None)) elts
- in
- fv_ctx, ctx
-
-let full_class_binder env (iid, (bk, bk'), cl as c) =
- let avoid = Idset.union env (ids_of_list (compute_context_vars env [c])) in
- let c, avoid =
- match bk' with
- | Implicit ->
- let (loc, id, l) =
- try destClassAppExpl cl
- with Not_found ->
- user_err_loc (constr_loc cl, "class_binders", str"Not an applied type class")
- in
- let gr = Nametab.global id in
- (try
- let c = class_info gr in
- let args, avoid = combine_params_freevar avoid l (List.rev c.cl_context) in
- (iid, bk, CAppExpl (loc, (None, id), args)), avoid
- with Not_found -> not_a_class (Global.env ()) (constr_of_global gr))
- | Explicit -> ((iid,bk,cl), avoid)
- in c
-
-let compute_constraint_freevars env (oid, _, x) =
- let bound = match snd oid with Name n -> Idset.add n env | Anonymous -> env in
- let ids = free_vars_of_constr_expr x ~bound [] in
- freevars_of_ids env (List.rev ids)
-
-let resolve_class_binder env c =
- let cstr = full_class_binder env c in
- let fv_ctx =
- let elts = compute_constraint_freevars env cstr in
- List.map (fun id -> (dummy_loc, id), CHole (dummy_loc, None)) elts
- in fv_ctx, cstr
-
-let generalize_class_binder_raw env c =
- let env = Idset.union env (Termops.vars_of_env (Global.env())) in
- let fv_ctx, cstr = resolve_class_binder env c in
- let ids' = List.fold_left (fun acc ((loc, id), t) -> Idset.add id acc) env fv_ctx in
- let ctx' = List.map (fun ((loc, id), t) -> ((loc, Name id), Implicit, t)) fv_ctx in
- ids', ctx', cstr
-
-let generalize_class_binders_raw env l =
- let env = Idset.union env (Termops.vars_of_env (Global.env())) in
- let fv_ctx, cstrs = resolve_class_binders env l in
- List.map (fun ((loc, id), t) -> ((loc, Name id), Implicit, t)) fv_ctx,
- List.map (fun (iid, bk, c) -> (iid, Implicit, c)) cstrs
-
+let implicit_application env ?(allow_partial=true) f ty =
+ let is_class =
+ try
+ let (loc, r, _ as clapp) = destClassAppExpl ty in
+ let (loc, qid) = qualid_of_reference r in
+ let gr = Nametab.locate qid in
+ if Typeclasses.is_class gr then Some (clapp, gr) else None
+ with Not_found -> None
+ in
+ match is_class with
+ | None -> ty
+ | 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
+ 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
+ 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 =
match c with
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 1ee81ce9..8dd12f72 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 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: implicit_quantifiers.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
(*i*)
open Names
@@ -28,34 +28,27 @@ 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
-val free_vars_of_constr_expr : Topconstr.constr_expr ->
- ?bound:Idset.t ->
- Names.identifier list -> Names.identifier list
+(* Fragile, should be used only for construction a set of identifiers to avoid *)
-val binder_list_of_ids : identifier list -> local_binder list
-
-val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier
+val free_vars_of_constr_expr : constr_expr -> ?bound:Idset.t ->
+ identifier list -> identifier list
val free_vars_of_binders :
?bound:Idset.t -> Names.identifier list -> local_binder list -> Idset.t * Names.identifier list
-val resolve_class_binders : Idset.t -> typeclass_context ->
- (identifier located * constr_expr) list * typeclass_context
+(* Returns the free ids in left-to-right order with the location of their first occurence *)
-val full_class_binders : Idset.t -> typeclass_context -> typeclass_context
+val free_vars_of_rawconstr : ?bound:Idset.t -> rawconstr -> (Names.identifier * loc) list
-val generalize_class_binder_raw : Idset.t -> name located * (binding_kind * binding_kind) * constr_expr ->
- Idset.t * typeclass_context * typeclass_constraint
-
-val generalize_class_binders_raw : Idset.t -> typeclass_context ->
- (name located * binding_kind * constr_expr) list * (name located * binding_kind * constr_expr) list
+val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier
val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool)) list
-val combine_params : Names.Idset.t ->
+val combine_params_freevar :
+ Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
+ Topconstr.constr_expr * Names.Idset.t
+
+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) ->
- (Topconstr.constr_expr * Topconstr.explicitation located option) list ->
- ((global_reference * bool) option * Term.rel_declaration) list ->
- Topconstr.constr_expr list * Names.Idset.t
-
+ constr_expr -> constr_expr
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 4cc30b26..d40205ce 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: modintern.ml 11127 2008-06-14 15:39:46Z herbelin $ *)
+(* $Id: modintern.ml 11582 2008-11-12 19:49:57Z notin $ *)
open Pp
open Util
@@ -61,34 +61,6 @@ let lookup_qualid (modtype:bool) qid =
*)
-let split_modpath mp =
- let rec aux = function
- | MPfile dp -> dp, []
- | MPbound mbid ->
- Lib.library_dp (), [id_of_mbid mbid]
- | MPself msid -> Lib.library_dp (), [id_of_msid msid]
- | MPdot (mp,l) -> let (mp', lab) = aux mp in
- (mp', id_of_label l :: lab)
- in
- let (mp, l) = aux mp in
- mp, l
-
-let dump_moddef loc mp ty =
- if !Flags.dump then
- let (dp, l) = split_modpath mp in
- let mp = string_of_dirpath (make_dirpath l) in
- Flags.dump_string (Printf.sprintf "%s %d %s %s\n" ty (fst (unloc loc)) "<>" mp)
-
-let rec drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl -> hd :: drop_last tl
-
-let dump_modref loc mp ty =
- if !Flags.dump then
- let (dp, l) = split_modpath mp in
- let fp = string_of_dirpath dp in
- let mp = string_of_dirpath (make_dirpath (drop_last l)) in
- Flags.dump_string (Printf.sprintf "R%d %s %s %s %s\n"
- (fst (unloc loc)) fp mp "<>" ty)
-
(* 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.
@@ -96,14 +68,14 @@ let dump_modref loc mp ty =
let lookup_module (loc,qid) =
try
let mp = Nametab.locate_module qid in
- dump_modref loc mp "modtype"; mp
+ 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
- dump_modref loc mp "mod"; mp
+ Dumpglob.dump_modref loc mp "mod"; mp
with
| Not_found ->
Modops.error_not_a_modtype_loc loc (string_of_qualid qid)
diff --git a/interp/modintern.mli b/interp/modintern.mli
index c92756dc..36971599 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 11065 2008-06-06 22:39:43Z msozeau $ i*)
+(*i $Id: modintern.mli 11582 2008-11-12 19:49:57Z notin $ i*)
(*i*)
open Declarations
@@ -26,6 +26,3 @@ val interp_modtype : env -> module_type_ast -> module_struct_entry
val interp_modexpr : env -> module_ast -> module_struct_entry
val lookup_module : qualid located -> module_path
-
-val dump_moddef : loc -> module_path -> string -> unit
-val dump_modref : loc -> module_path -> string -> unit
diff --git a/interp/notation.ml b/interp/notation.ml
index 9e83b860..fcb2b6f5 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: notation.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: notation.ml 11512 2008-10-27 12:28:36Z herbelin $ *)
(*i*)
open Util
@@ -193,10 +193,6 @@ let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *)
| ARef ref -> RefKey ref, None
| _ -> Oth, None
-let pattern_key = function
- | PatCstr (_,cstr,_,_) -> RefKey (ConstructRef cstr)
- | _ -> Oth
-
(**********************************************************************)
(* Interpreting numbers (not in summary because functional objects) *)
@@ -408,7 +404,7 @@ let exists_notation_in_scope scopt ntn r =
r' = r
with Not_found -> false
-let isAVar = function AVar _ -> true | _ -> false
+let isAVar_or_AHole = function AVar _ | AHole _ -> true | _ -> false
(**********************************************************************)
(* Mapping classes to scopes *)
@@ -620,7 +616,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 l & test ref ->
+ | AApp (ARef ref, l) when List.for_all isAVar_or_AHole l & test ref ->
Some (ntn,sc,ref)
| _ -> None
@@ -632,8 +628,12 @@ let error_notation_not_reference loc ntn =
str "Unable to interpret " ++ quote (str ntn) ++
str " as a reference.")
-let interp_notation_as_global_reference loc test ntn =
- let ntns = browse_notation true ntn !scope_map in
+let interp_notation_as_global_reference loc test ntn sc =
+ let scopes = match sc with
+ | Some sc ->
+ Gmap.add sc (find_scope (find_delimiters_scope dummy_loc sc)) Gmap.empty
+ | None -> !scope_map in
+ let ntns = browse_notation true ntn scopes in
let refs = List.map (global_reference_of_notation test) ntns in
match Option.List.flatten refs with
| [_,_,ref] -> ref
diff --git a/interp/notation.mli b/interp/notation.mli
index a393aaed..4d7289c2 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 9804 2007-04-28 13:56:03Z herbelin $ i*)
+(*i $Id: notation.mli 11445 2008-10-11 16:42:46Z herbelin $ i*)
(*i*)
open Util
@@ -131,7 +131,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) ->
- notation -> global_reference
+ notation -> delimiters option -> global_reference
(* Checks for already existing notations *)
val exists_notation_in_scope : scope_name option -> notation ->
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 884dea48..fe998cba 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 10730 2008-03-30 21:42:58Z herbelin $ *)
+(* $Id: syntax_def.ml 11512 2008-10-27 12:28:36Z herbelin $ *)
open Util
open Pp
@@ -70,11 +70,18 @@ let (in_syntax_constant, out_syntax_constant) =
classify_function = classify_syntax_constant;
export_function = export_syntax_constant }
+type syndef_interpretation = (identifier * subscopes) list * aconstr
+
+(* Coercions to the general format of notation that also supports
+ variables bound to list of expressions *)
+let in_pat (ids,ac) = ((ids,[]),ac)
+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,pat,onlyparse)) in ()
+ let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in ()
let search_syntactic_definition loc kn =
- KNmap.find kn !syntax_table
+ out_pat (KNmap.find kn !syntax_table)
let locate_global_with_alias (loc,qid) =
match Nametab.extended_locate qid with
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index a063caf0..0f5e0be7 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: syntax_def.mli 10730 2008-03-30 21:42:58Z herbelin $ i*)
+(*i $Id: syntax_def.mli 11512 2008-10-27 12:28:36Z herbelin $ i*)
(*i*)
open Util
@@ -18,10 +18,12 @@ open Libnames
(* Syntactic definitions. *)
-val declare_syntactic_definition : bool -> identifier -> bool -> interpretation
- -> unit
+type syndef_interpretation = (identifier * subscopes) list * aconstr
-val search_syntactic_definition : loc -> kernel_name -> interpretation
+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
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index a51b6bb0..89ddd001 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: topconstr.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: topconstr.ml 11739 2009-01-02 19:33:19Z herbelin $ *)
(*i*)
open Pp
@@ -389,8 +389,9 @@ let rec subst_aconstr subst bound raw =
if r1' == r1 then raw else
ACast (r1',CastCoerce)
-let subst_interpretation subst (metas,pat) =
- (metas,subst_aconstr subst (List.map fst metas) pat)
+let subst_interpretation subst (metas,pat) =
+ let bound = List.map fst (fst metas @ snd metas) in
+ (metas,subst_aconstr subst bound pat)
let encode_list_value l = RApp (dummy_loc,RVar (dummy_loc,ldots_var),l)
@@ -427,16 +428,16 @@ let rec alpha_var id1 id2 = function
let alpha_eq_val (x,y) = x = y
-let bind_env alp sigma var v =
+let bind_env alp (sigma,sigmalist as fullsigma) var v =
try
let vvar = List.assoc var sigma in
- if alpha_eq_val (v,vvar) then sigma
+ if alpha_eq_val (v,vvar) then fullsigma
else raise No_match
with Not_found ->
(* Check that no capture of binding variables occur *)
if List.exists (fun (id,_) ->occur_rawconstr id v) alp then raise No_match;
(* TODO: handle the case of multiple occs in different scopes *)
- (var,v)::sigma
+ ((var,v)::sigma,sigmalist)
let match_fix_kind fk1 fk2 =
match (fk1,fk2) with
@@ -467,6 +468,10 @@ let rec match_cases_pattern metas acc pat1 pat2 =
(match_names metas acc na1 na2) patl1 patl2
| _ -> raise No_match
+let adjust_application_n n loc f l =
+ let l1,l2 = list_chop (List.length l - n) l in
+ if l1 = [] then f,l else RApp (loc,f,l1), l2
+
let 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
@@ -481,8 +486,9 @@ 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 (_,f1,l1), AList (x,_,(AApp (f2,l2) as iter),termin,lassoc)
- when List.length l1 = List.length l2 ->
+ | 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
| RLambda (_,na1,_,t1,b1), ALambda (na2,t2,b2) ->
match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2
@@ -496,9 +502,12 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
& 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 = Option.fold_left2 (match_ alp metas) sigma rtno1' rtno2' in
+ let sigma =
+ try Option.fold_left2 (match_ alp metas) sigma rtno1' rtno2'
+ with Option.Heterogeneous -> raise No_match
+ in
let sigma = List.fold_left2
- (fun s (tm1,_) (tm2,_) -> match_ alp metas s tm1 tm2) sigma tml1 tml2 in
+ (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)
when List.length nal1 = List.length nal2 ->
@@ -535,24 +544,26 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
and match_alist alp metas sigma l1 l2 x iter termin lassoc =
(* match the iterator at least once *)
- let sigma = List.fold_left2 (match_ alp (ldots_var::metas)) sigma l1 l2 in
+ 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 sigma in
+ let rest = List.assoc ldots_var sigmavar in
(* Recover the first element *)
- let t1 = List.assoc x sigma in
- let sigma = List.remove_assoc x (List.remove_assoc ldots_var sigma) in
+ 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 sigma = match_ alp (ldots_var::metas) sigma rest iter in
- let rest = List.assoc ldots_var sigma in
- let t = List.assoc x sigma in
- let sigma = List.remove_assoc x (List.remove_assoc ldots_var sigma) in
- match_alist_tail alp metas sigma (t::acc) rest
+ 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 sigma rest termin in
- let tl,sigma = match_alist_tail alp metas sigma [t1] rest in
- (x,encode_list_value (if lassoc then List.rev tl else tl))::sigma
+ 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
@@ -569,19 +580,24 @@ type scope_name = string
type tmp_scope_name = scope_name
-type interpretation =
- (identifier * (tmp_scope_name option * scope_name list)) list * aconstr
+type subscopes = tmp_scope_name option * scope_name list
-let match_aconstr c (metas_scl,pat) =
- let subst = match_ [] (List.map fst metas_scl) [] c pat in
+type interpretation =
+ (* regular vars of notation / recursive parts of notation / body *)
+ ((identifier * subscopes) list * (identifier * subscopes) list) * aconstr
+
+let match_aconstr c ((metas_scl,metaslist_scl),pat) =
+ let vars = List.map fst metas_scl @ List.map fst metaslist_scl in
+ let subst,substlist = match_ [] vars ([],[]) c pat in
(* Reorder canonically the substitution *)
- let find x subst =
+ let find x =
try List.assoc x subst
with Not_found ->
(* Happens for binders bound to Anonymous *)
(* Find a better way to propagate Anonymous... *)
RVar (dummy_loc,x) in
- List.map (fun (x,scl) -> (find x subst,scl)) metas_scl
+ List.map (fun (x,scl) -> (find x,scl)) metas_scl,
+ List.map (fun (x,scl) -> (List.assoc x substlist,scl)) metaslist_scl
(**********************************************************************)
(*s Concrete syntax for terms *)
@@ -590,18 +606,23 @@ type notation = string
type explicitation = ExplByPos of int * identifier option | ExplByName of identifier
-type binder_kind = Default of binding_kind | TypeClass of binding_kind * binding_kind
+type binder_kind = Default of binding_kind | Generalized of binding_kind * binding_kind * bool
+
+type abstraction_kind = AbsLambda | AbsPi
type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
type prim_token = Numeral of Bigint.bigint | String of string
+type 'a notation_substitution =
+ 'a list * (* for recursive notations: *) 'a list list
+
type cases_pattern_expr =
| CPatAlias of loc * cases_pattern_expr * identifier
| CPatCstr of loc * reference * cases_pattern_expr list
| CPatAtom of loc * reference option
| CPatOr of loc * cases_pattern_expr list
- | CPatNotation of loc * notation * cases_pattern_expr list
+ | CPatNotation of loc * notation * cases_pattern_expr notation_substitution
| CPatPrim of loc * prim_token
| CPatDelimiters of loc * string * cases_pattern_expr
@@ -616,6 +637,7 @@ type constr_expr =
| CAppExpl of loc * (proj_flag * reference) * constr_expr list
| CApp of loc * (proj_flag * constr_expr) *
(constr_expr * explicitation located option) list
+ | CRecord of loc * constr_expr option * (identifier located * 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
@@ -628,7 +650,8 @@ type constr_expr =
| CEvar of loc * existential_key * constr_expr list option
| CSort of loc * rawsort
| CCast of loc * constr_expr * constr_expr cast_type
- | CNotation of loc * notation * constr_expr list
+ | CNotation of loc * notation * constr_expr notation_substitution
+ | CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr
| CPrim of loc * prim_token
| CDelimiters of loc * string * constr_expr
| CDynamic of loc * Dyn.t
@@ -652,6 +675,8 @@ and recursion_order_expr =
| CWfRec of constr_expr
| CMeasureRec of constr_expr
+type constr_pattern_expr = constr_expr
+
(***********************)
(* For binders parsing *)
@@ -687,6 +712,7 @@ let constr_loc = function
| CLetIn (loc,_,_,_) -> loc
| CAppExpl (loc,_,_) -> loc
| CApp (loc,_,_) -> loc
+ | CRecord (loc,_,_) -> loc
| CCases (loc,_,_,_,_) -> loc
| CLetTuple (loc,_,_,_,_) -> loc
| CIf (loc,_,_,_,_) -> loc
@@ -696,6 +722,7 @@ let constr_loc = function
| CSort (loc,_) -> loc
| CCast (loc,_,_) -> loc
| CNotation (loc,_,_) -> loc
+ | CGeneralization (loc,_,_,_) -> loc
| CPrim (loc,_) -> loc
| CDelimiters (loc,_,_) -> loc
| CDynamic _ -> dummy_loc
@@ -718,7 +745,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
@@ -738,8 +765,10 @@ let is_constructor id =
let rec cases_pattern_fold_names f a = function
| CPatAlias (_,pat,id) -> f id a
- | CPatCstr (_,_,patl) | CPatOr (_,patl) | CPatNotation (_,_,patl) ->
+ | CPatCstr (_,_,patl) | CPatOr (_,patl) ->
List.fold_left (cases_pattern_fold_names f) a patl
+ | CPatNotation (_,_,(patl,patll)) ->
+ List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)
| CPatDelimiters (_,_,pat) -> cases_pattern_fold_names f a pat
| CPatAtom (_,Some (Ident (_,id))) when not (is_constructor id) -> f id a
| CPatPrim _ | CPatAtom _ -> a
@@ -776,10 +805,12 @@ let fold_constr_expr_with_binders g f n acc = function
| CLetIn (_,na,a,b) -> fold_constr_expr_binders g f n acc b [[na],default_binder_kind,a]
| CCast (loc,a,CastConv(_,b)) -> f n (f n acc a) b
| CCast (loc,a,CastCoerce) -> f n acc a
- | CNotation (_,_,l) -> List.fold_left (f n) acc l
+ | CNotation (_,_,(l,ll)) -> List.fold_left (f n) acc (l@List.flatten ll)
+ | CGeneralization (_,_,_,c) -> f n acc c
| CDelimiters (loc,_,a) -> f n acc a
| CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _ | CRef _ ->
acc
+ | CRecord (loc,_,l) -> List.fold_left (fun acc (id, c) -> f n acc c) acc l
| CCases (loc,sty,rtnpo,al,bl) ->
let ids = ids_of_cases_tomatch al in
let acc = Option.fold_left (f (List.fold_right g ids n)) acc rtnpo in
@@ -887,10 +918,13 @@ let map_constr_expr_with_binders g f e = function
| CLetIn (loc,na,a,b) -> CLetIn (loc,na,f e a,f (name_fold g (snd na) e) b)
| CCast (loc,a,CastConv (k,b)) -> CCast (loc,f e a,CastConv(k, f e b))
| CCast (loc,a,CastCoerce) -> CCast (loc,f e a,CastCoerce)
- | CNotation (loc,n,l) -> CNotation (loc,n,List.map (f e) l)
+ | CNotation (loc,n,(l,ll)) ->
+ 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 _
| 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) ->
(* TODO: apply g on the binding variables in pat... *)
let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in
@@ -947,3 +981,10 @@ type module_type_ast =
type include_ast =
| CIMTE of module_type_ast
| CIME of module_ast
+
+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 ntn_loc = loc_of_notation constr_loc
+let patntn_loc = loc_of_notation cases_pattern_expr_loc
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 2ac9da11..1dd5ec97 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 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: topconstr.mli 11739 2009-01-02 19:33:19Z herbelin $ i*)
(*i*)
open Pp
@@ -77,11 +77,14 @@ type scope_name = string
type tmp_scope_name = scope_name
-type interpretation =
- (identifier * (tmp_scope_name option * scope_name list)) list * aconstr
+type subscopes = tmp_scope_name option * scope_name list
+
+type interpretation =
+ (* regular vars of notation / recursive parts of notation / body *)
+ ((identifier * subscopes) list * (identifier * subscopes) list) * aconstr
val match_aconstr : rawconstr -> interpretation ->
- (rawconstr * (tmp_scope_name option * scope_name list)) list
+ (rawconstr * subscopes) list * (rawconstr list * subscopes) list
(**********************************************************************)
(* Substitution of kernel names in interpretation data *)
@@ -95,18 +98,27 @@ type notation = string
type explicitation = ExplByPos of int * identifier option | ExplByName of identifier
-type binder_kind = Default of binding_kind | TypeClass of binding_kind * 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 *)
+
+type abstraction_kind = AbsLambda | AbsPi
type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
type prim_token = Numeral of Bigint.bigint | String of string
+type 'a notation_substitution =
+ 'a list * (* for recursive notations: *) 'a list list
+
type cases_pattern_expr =
| CPatAlias of loc * cases_pattern_expr * identifier
| CPatCstr of loc * reference * cases_pattern_expr list
| CPatAtom of loc * reference option
| CPatOr of loc * cases_pattern_expr list
- | CPatNotation of loc * notation * cases_pattern_expr list
+ | CPatNotation of loc * notation * cases_pattern_expr notation_substitution
| CPatPrim of loc * prim_token
| CPatDelimiters of loc * string * cases_pattern_expr
@@ -121,6 +133,7 @@ type constr_expr =
| CAppExpl of loc * (proj_flag * reference) * constr_expr list
| CApp of loc * (proj_flag * constr_expr) *
(constr_expr * explicitation located option) list
+ | CRecord of loc * constr_expr option * (identifier located * 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
@@ -133,7 +146,8 @@ type constr_expr =
| CEvar of loc * existential_key * constr_expr list option
| CSort of loc * rawsort
| CCast of loc * constr_expr * constr_expr cast_type
- | CNotation of loc * notation * constr_expr list
+ | CNotation of loc * notation * constr_expr notation_substitution
+ | CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr
| CPrim of loc * prim_token
| CDelimiters of loc * string * constr_expr
| CDynamic of loc * Dyn.t
@@ -158,6 +172,8 @@ type typeclass_constraint = name located * binding_kind * constr_expr
and typeclass_context = typeclass_constraint list
+type constr_pattern_expr = constr_expr
+
(**********************************************************************)
(* Utilities on constr_expr *)
@@ -240,3 +256,5 @@ type include_ast =
| CIMTE of module_type_ast
| CIME of module_ast
+val ntn_loc : Util.loc -> constr_expr list -> string -> int
+val patntn_loc : Util.loc -> cases_pattern_expr list -> string -> int
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-26 07:44:55 +0000