summaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml238
-rw-r--r--interp/constrextern.mli9
-rw-r--r--interp/constrintern.ml905
-rw-r--r--interp/constrintern.mli37
-rw-r--r--interp/coqlib.ml36
-rw-r--r--interp/coqlib.mli9
-rw-r--r--interp/genarg.ml26
-rw-r--r--interp/genarg.mli247
-rw-r--r--interp/implicit_quantifiers.ml285
-rw-r--r--interp/implicit_quantifiers.mli68
-rw-r--r--interp/modintern.ml63
-rw-r--r--interp/modintern.mli13
-rw-r--r--interp/notation.ml86
-rw-r--r--interp/notation.mli7
-rw-r--r--interp/reserve.ml20
-rw-r--r--interp/syntax_def.ml47
-rw-r--r--interp/syntax_def.mli22
-rw-r--r--interp/topconstr.ml269
-rw-r--r--interp/topconstr.mli74
19 files changed, 1660 insertions, 801 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index b9d7694f..141e8f8a 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: constrextern.ml 10135 2007-09-21 14:28:12Z herbelin $ *)
+(* $Id: constrextern.ml 11024 2008-05-30 12:41:39Z msozeau $ *)
(*i*)
open Pp
@@ -44,11 +44,15 @@ let print_evar_arguments = ref false
(* This governs printing of implicit arguments. When
[print_implicits] is on then [print_implicits_explicit_args] tells
how implicit args are printed. If on, implicit args are printed
- prefixed by "!" otherwise the function and not the arguments is
- prefixed by "!" *)
+ with the form (id:=arg) otherwise arguments are printed normally and
+ the function is prefixed by "@" *)
let print_implicits = ref false
let print_implicits_explicit_args = ref false
+(* Tells if implicit arguments not known to be inferable from a rigid
+ position are systematically printed *)
+let print_implicits_defensive = ref true
+
(* This forces printing of coercions *)
let print_coercions = ref false
@@ -63,12 +67,12 @@ let print_projections = ref false
let print_meta_as_hole = ref false
-let with_arguments f = Options.with_option print_arguments f
-let with_implicits f = Options.with_option print_implicits f
-let with_coercions f = Options.with_option print_coercions f
-let with_universes f = Options.with_option print_universes f
-let without_symbols f = Options.with_option print_no_symbol f
-let with_meta_as_hole f = Options.with_option print_meta_as_hole f
+let with_arguments f = Flags.with_option print_arguments f
+let with_implicits f = Flags.with_option print_implicits f
+let with_coercions f = Flags.with_option print_coercions f
+let with_universes f = Flags.with_option print_universes f
+let without_symbols f = Flags.with_option print_no_symbol f
+let with_meta_as_hole f = Flags.with_option print_meta_as_hole f
(**********************************************************************)
(* Various externalisation functions *)
@@ -101,30 +105,20 @@ let idopt_of_name = function
| Name id -> Some id
| Anonymous -> None
-let extern_evar loc n =
-(*
- msgerrnl (str
- "Warning: existential variable turned into meta-variable during externalization");
- CPatVar (loc,(false,make_ident "META" (Some n)))
-*)
- CEvar (loc,n)
-
-let raw_string_of_ref = function
- | ConstRef kn ->
- "CONST("^(string_of_con kn)^")"
- | IndRef (kn,i) ->
- "IND("^(string_of_kn kn)^","^(string_of_int i)^")"
- | ConstructRef ((kn,i),j) ->
- "CONSTRUCT("^
- (string_of_kn kn)^","^(string_of_int i)^","^(string_of_int j)^")"
- | VarRef id ->
- "SECVAR("^(string_of_id id)^")"
+let extern_evar loc n l =
+ if !print_evar_arguments then CEvar (loc,n,l) else CEvar (loc,n,None)
+
+let debug_global_reference_printer =
+ ref (fun _ -> failwith "Cannot print a global reference")
+
+let set_debug_global_reference_printer f =
+ debug_global_reference_printer := f
let extern_reference loc vars r =
try Qualid (loc,shortest_qualid_of_global vars r)
with Not_found ->
(* happens in debugger *)
- Ident (loc,id_of_string (raw_string_of_ref r))
+ !debug_global_reference_printer loc r
(************************************************************************)
(* Equality up to location (useful for translator v8) *)
@@ -183,10 +177,10 @@ let rec check_same_type ty1 ty2 =
List.iter2 (fun (a1,e1) (a2,e2) ->
if e1<>e2 then failwith "not same expl";
check_same_type a1 a2) al1 al2
- | CCases(_,_,a1,brl1), CCases(_,_,a2,brl2) ->
+ | CCases(_,_,_,a1,brl1), CCases(_,_,_,a2,brl2) ->
List.iter2 (fun (tm1,_) (tm2,_) -> check_same_type tm1 tm2) a1 a2;
List.iter2 (fun (_,pl1,r1) (_,pl2,r2) ->
- List.iter2 (List.iter2 check_same_pattern) pl1 pl2;
+ List.iter2 (located_iter2 (List.iter2 check_same_pattern)) pl1 pl2;
check_same_type r1 r2) brl1 brl2
| CHole _, CHole _ -> ()
| CPatVar(_,i1), CPatVar(_,i2) when i1=i2 -> ()
@@ -204,7 +198,7 @@ let rec check_same_type ty1 ty2 =
| _ when ty1=ty2 -> ()
| _ -> failwith "not same type"
-and check_same_binder (nal1,e1) (nal2,e2) =
+and check_same_binder (nal1,_,e1) (nal2,_,e2) =
List.iter2 (fun (_,na1) (_,na2) ->
if na1<>na2 then failwith "not same name") nal1 nal2;
check_same_type e1 e2
@@ -212,20 +206,15 @@ and check_same_binder (nal1,e1) (nal2,e2) =
and check_same_fix_binder bl1 bl2 =
List.iter2 (fun b1 b2 ->
match b1,b2 with
- LocalRawAssum(nal1,ty1), LocalRawAssum(nal2,ty2) ->
- check_same_binder (nal1,ty1) (nal2,ty2)
+ LocalRawAssum(nal1,k,ty1), LocalRawAssum(nal2,k',ty2) ->
+ check_same_binder (nal1,k,ty1) (nal2,k',ty2)
| LocalRawDef(na1,def1), LocalRawDef(na2,def2) ->
- check_same_binder ([na1],def1) ([na2],def2)
+ check_same_binder ([na1],default_binder_kind,def1) ([na2],default_binder_kind,def2)
| _ -> failwith "not same binder") bl1 bl2
let same c d = try check_same_type c d; true with _ -> false
(* Idem for rawconstr *)
-let option_iter2 f o1 o2 =
- match o1, o2 with
- Some o1, Some o2 -> f o1 o2
- | None, None -> ()
- | _ -> failwith "option"
let array_iter2 f v1 v2 =
List.iter2 f (Array.to_list v1) (Array.to_list v2)
@@ -244,25 +233,25 @@ let rec same_raw c d =
| RVar(_,id1), RVar(_,id2) -> if id1<>id2 then failwith "RVar"
| REvar(_,e1,a1), REvar(_,e2,a2) ->
if e1 <> e2 then failwith "REvar";
- option_iter2(List.iter2 same_raw) a1 a2
+ Option.iter2(List.iter2 same_raw) a1 a2
| RPatVar(_,pv1), RPatVar(_,pv2) -> if pv1<>pv2 then failwith "RPatVar"
| RApp(_,f1,a1), RApp(_,f2,a2) ->
List.iter2 same_raw (f1::a1) (f2::a2)
- | RLambda(_,na1,t1,m1), RLambda(_,na2,t2,m2) ->
+ | RLambda(_,na1,bk1,t1,m1), RLambda(_,na2,bk2,t2,m2) ->
if na1 <> na2 then failwith "RLambda";
same_raw t1 t2; same_raw m1 m2
- | RProd(_,na1,t1,m1), RProd(_,na2,t2,m2) ->
+ | RProd(_,na1,bk1,t1,m1), RProd(_,na2,bk2,t2,m2) ->
if na1 <> na2 then failwith "RProd";
same_raw t1 t2; same_raw m1 m2
| RLetIn(_,na1,t1,m1), RLetIn(_,na2,t2,m2) ->
if na1 <> na2 then failwith "RLetIn";
same_raw t1 t2; same_raw m1 m2
- | RCases(_,_,c1,b1), RCases(_,_,c2,b2) ->
+ | RCases(_,_,_,c1,b1), RCases(_,_,_,c2,b2) ->
List.iter2
(fun (t1,(al1,oind1)) (t2,(al2,oind2)) ->
same_raw t1 t2;
if al1 <> al2 then failwith "RCases";
- option_iter2(fun (_,i1,_,nl1) (_,i2,_,nl2) ->
+ Option.iter2(fun (_,i1,_,nl1) (_,i2,_,nl2) ->
if i1<>i2 || nl1 <> nl2 then failwith "RCases") oind1 oind2) c1 c2;
List.iter2 (fun (_,_,pl1,b1) (_,_,pl2,b2) ->
List.iter2 same_patt pl1 pl2;
@@ -276,9 +265,9 @@ let rec same_raw c d =
| RRec(_,fk1,na1,bl1,ty1,def1), RRec(_,fk2,na2,bl2,ty2,def2) ->
if fk1 <> fk2 || na1 <> na2 then failwith "RRec";
array_iter2
- (List.iter2 (fun (na1,bd1,ty1) (na2,bd2,ty2) ->
+ (List.iter2 (fun (na1,bk1,bd1,ty1) (na2,bk2,bd2,ty2) ->
if na1<>na2 then failwith "RRec";
- option_iter2 same_raw bd1 bd2;
+ Option.iter2 same_raw bd1 bd2;
same_raw ty1 ty2)) bl1 bl2;
array_iter2 same_raw ty1 ty2;
array_iter2 same_raw def1 def2
@@ -374,7 +363,7 @@ let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with
| r1, AVar id2 when List.mem id2 metas -> bind_env sigma id2 r1
| PatVar (_,Anonymous), AHole _ -> sigma
| a, AHole _ -> sigma
- | PatCstr (loc,(ind,_ as r1),args1,Anonymous), _ ->
+ | PatCstr (loc,(ind,_ as r1),args1,_), _ ->
let nparams =
(fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
let l2 =
@@ -402,16 +391,16 @@ let match_aconstr_cases_pattern c (metas_scl,pat) =
(* Better to use extern_rawconstr composed with injection/retraction ?? *)
let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
try
- if !Options.raw_print or !print_no_symbol then raise No_match;
+ if !Flags.raw_print or !print_no_symbol then raise No_match;
let (na,sc,p) = uninterp_prim_token_cases_pattern pat in
- match availability_of_prim_token sc scopes p with
+ match availability_of_prim_token sc scopes with
| None -> raise No_match
| Some key ->
let loc = cases_pattern_loc pat in
insert_pat_alias loc (insert_pat_delimiters loc (CPatPrim(loc,p)) key) na
with No_match ->
try
- if !Options.raw_print or !print_no_symbol then raise No_match;
+ if !Flags.raw_print or !print_no_symbol then raise No_match;
extern_symbol_pattern scopes vars pat
(uninterp_cases_pattern_notations pat)
with No_match ->
@@ -429,22 +418,22 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
| (keyrule,pat,n as _rule)::rules ->
try
(* Check the number of arguments expected by the notation *)
- let loc = match t,n with
+ let loc,na = match t,n with
| PatCstr (_,f,l,_), Some n when List.length l > n ->
raise No_match
- | PatCstr (loc,_,_,_),_ -> loc
- | PatVar (loc,_),_ -> loc in
+ | PatCstr (loc,_,_,na),_ -> loc,na
+ | PatVar (loc,na),_ -> loc,na in
(* Try matching ... *)
let subst = match_aconstr_cases_pattern t pat in
(* Try availability of interpretation ... *)
- match keyrule with
+ let p = match keyrule with
| NotationRule (sc,ntn) ->
(match availability_of_notation (sc,ntn) allscopes with
(* Uninterpretation is not allowed in current context *)
| None -> raise No_match
(* Uninterpretation is allowed in current context *)
| Some (scopt,key) ->
- let scopes' = option_cons scopt scopes in
+ let scopes' = Option.List.cons scopt scopes in
let l =
List.map (fun (c,(scopt,scl)) ->
extern_cases_pattern_in_scope (scopt,scl@scopes') vars c)
@@ -452,7 +441,8 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
insert_pat_delimiters loc (make_pat_notation loc ntn l) key)
| SynDefRule kn ->
let qid = shortest_qualid_of_syndef vars kn in
- CPatAtom (loc,Some (Qualid (loc, qid)))
+ CPatAtom (loc,Some (Qualid (loc, qid))) in
+ insert_pat_alias loc p na
with
No_match -> extern_symbol_pattern allscopes vars t rules
@@ -468,7 +458,7 @@ let occur_name na aty =
| Anonymous -> false
let is_projection nargs = function
- | Some r when not !Options.raw_print & !print_projections ->
+ | Some r when not !Flags.raw_print & !print_projections ->
(try
let n = Recordops.find_projection_nparams r + 1 in
if n <= nargs then Some n else None
@@ -488,10 +478,11 @@ let explicitize loc inctx impl (cf,f) args =
| a::args, imp::impl when is_status_implicit imp ->
let tail = exprec (q+1) (args,impl) in
let visible =
- !Options.raw_print or
+ !Flags.raw_print or
(!print_implicits & !print_implicits_explicit_args) or
- (is_significant_implicit a impl tail &
- (not (is_inferable_implicit inctx n imp)))
+ (!print_implicits_defensive &
+ is_significant_implicit a impl tail &
+ not (is_inferable_implicit inctx n imp))
in
if visible then
(a,Some (dummy_loc, ExplByName (name_of_implicit imp))) :: tail
@@ -526,7 +517,7 @@ let extern_app loc inctx impl (cf,f) args =
extern_global loc impl f
else
if
- ((!Options.raw_print or
+ ((!Flags.raw_print or
(!print_implicits & not !print_implicits_explicit_args)) &
List.exists is_status_implicit impl)
then
@@ -545,16 +536,17 @@ let rec extern_args extern scopes env args subscopes =
let rec remove_coercions inctx = function
| RApp (loc,RRef (_,r),args) as c
- when inctx & not (!Options.raw_print or !print_coercions)
+ when not (!Flags.raw_print or !print_coercions)
->
+ let nargs = List.length args in
(try match Classops.hide_coercion r with
- | Some n when n < List.length args ->
+ | Some n when n < nargs && (inctx or n+1 < nargs) ->
(* 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) =
+ let (a,l) = match l with a::l -> (a,l) | [] -> assert false in
+ let (a,l) =
(* Recursively remove the head coercions *)
- match remove_coercions inctx a with
+ match remove_coercions true a with
| RApp (_,a,l') -> a,l'@l
| a -> a,l in
if l = [] then a
@@ -572,7 +564,7 @@ let rec rename_rawconstr_var id0 id1 = function
let rec share_fix_binders n rbl ty def =
match ty,def with
- RProd(_,na0,t0,b), RLambda(_,na1,t1,m) ->
+ RProd(_,na0,bk0,t0,b), RLambda(_,na1,bk1,t1,m) ->
if not(same_rawconstr t0 t1) then List.rev rbl, ty, def
else
let (na,b,m) =
@@ -604,7 +596,7 @@ let rec share_fix_binders n rbl ty def =
let extern_possible_prim_token scopes r =
try
let (sc,n) = uninterp_prim_token r in
- match availability_of_prim_token sc scopes n with
+ match availability_of_prim_token sc scopes with
| None -> None
| Some key -> Some (insert_delimiters (CPrim (loc_of_rawconstr r,n)) key)
with No_match ->
@@ -628,11 +620,11 @@ let extern_rawsort = function
let rec extern inctx scopes vars r =
let r' = remove_coercions inctx r in
try
- if !Options.raw_print or !print_no_symbol then raise No_match;
+ if !Flags.raw_print or !print_no_symbol then raise No_match;
extern_optimal_prim_token scopes r r'
with No_match ->
try
- if !Options.raw_print or !print_no_symbol then raise No_match;
+ if !Flags.raw_print or !print_no_symbol then raise No_match;
extern_symbol scopes vars r' (uninterp_notations r')
with No_match -> match r' with
| RRef (loc,ref) ->
@@ -641,11 +633,13 @@ let rec extern inctx scopes vars r =
| RVar (loc,id) -> CRef (Ident (loc,id))
- | REvar (loc,n,None) when !print_meta_as_hole -> CHole loc
+ | REvar (loc,n,None) when !print_meta_as_hole -> CHole (loc, None)
- | REvar (loc,n,_) -> (* we drop args *) extern_evar loc n
+ | REvar (loc,n,l) ->
+ extern_evar loc n (Option.map (List.map (extern false scopes vars)) l)
- | RPatVar (loc,n) -> if !print_meta_as_hole then CHole loc else CPatVar (loc,n)
+ | RPatVar (loc,n) ->
+ if !print_meta_as_hole then CHole (loc, None) else CPatVar (loc,n)
| RApp (loc,f,args) ->
(match f with
@@ -660,7 +654,7 @@ let rec extern inctx scopes vars r =
explicitize loc inctx [] (None,sub_extern false scopes vars f)
(List.map (sub_extern true scopes vars) args))
- | RProd (loc,Anonymous,t,c) ->
+ | RProd (loc,Anonymous,_,t,c) ->
(* Anonymous product are never factorized *)
CArrow (loc,extern_typ scopes vars t, extern_typ scopes vars c)
@@ -668,31 +662,31 @@ let rec extern inctx scopes vars r =
CLetIn (loc,(loc,na),sub_extern false scopes vars t,
extern inctx scopes (add_vname vars na) c)
- | RProd (loc,na,t,c) ->
+ | RProd (loc,na,bk,t,c) ->
let t = extern_typ scopes vars (anonymize_if_reserved na t) in
let (idl,c) = factorize_prod scopes (add_vname vars na) t c in
- CProdN (loc,[(dummy_loc,na)::idl,t],c)
+ CProdN (loc,[(dummy_loc,na)::idl,Default bk,t],c)
- | RLambda (loc,na,t,c) ->
+ | RLambda (loc,na,bk,t,c) ->
let t = extern_typ scopes vars (anonymize_if_reserved na t) in
let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) t c in
- CLambdaN (loc,[(dummy_loc,na)::idl,t],c)
+ CLambdaN (loc,[(dummy_loc,na)::idl,Default bk,t],c)
- | RCases (loc,rtntypopt,tml,eqns) ->
+ | RCases (loc,sty,rtntypopt,tml,eqns) ->
let vars' =
List.fold_right (name_fold Idset.add)
(cases_predicate_names tml) vars in
- let rtntypopt' = option_map (extern_typ scopes vars') rtntypopt in
+ let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in
let tml = List.map (fun (tm,(na,x)) ->
let na' = match na,tm with
Anonymous, RVar (_,id) when
- rtntypopt<>None & occur_rawconstr id (out_some rtntypopt)
+ rtntypopt<>None & occur_rawconstr id (Option.get rtntypopt)
-> Some Anonymous
| Anonymous, _ -> None
| Name id, RVar (_,id') when id=id' -> None
| Name _, _ -> Some na in
(sub_extern false scopes vars tm,
- (na',option_map (fun (loc,ind,n,nal) ->
+ (na',Option.map (fun (loc,ind,n,nal) ->
let params = list_tabulate
(fun _ -> RHole (dummy_loc,Evd.InternalHole)) n in
let args = List.map (function
@@ -701,19 +695,19 @@ let rec extern inctx scopes vars r =
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
- CCases (loc,rtntypopt',tml,eqns)
+ CCases (loc,sty,rtntypopt',tml,eqns)
| RLetTuple (loc,nal,(na,typopt),tm,b) ->
CLetTuple (loc,nal,
- (option_map (fun _ -> na) typopt,
- option_map (extern_typ scopes (add_vname vars na)) typopt),
+ (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)
| 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),
+ (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)
| RRec (loc,fk,idv,blv,tyv,bv) ->
@@ -726,8 +720,13 @@ let rec extern inctx scopes vars r =
let (ids,bl) = extern_local_binder scopes vars bl in
let vars0 = List.fold_right (name_fold Idset.add) ids vars in
let vars1 = List.fold_right (name_fold Idset.add) ids vars' in
- let n, ro = fst nv.(i), extern_recursion_order scopes vars (snd nv.(i)) in
- (fi, (n, ro), bl, extern_typ scopes vars0 ty,
+ let n =
+ match fst nv.(i) with
+ | None -> None
+ | Some x -> Some (dummy_loc, out_name (List.nth ids x))
+ in
+ let ro = extern_recursion_order scopes vars (snd nv.(i)) in
+ ((dummy_loc, fi), (n, ro), bl, extern_typ scopes vars0 ty,
extern false scopes vars1 def)) idv
in
CFix (loc,(loc,idv.(n)),Array.to_list listdecl)
@@ -737,14 +736,14 @@ let rec extern inctx scopes vars r =
let (ids,bl) = extern_local_binder scopes vars blv.(i) in
let vars0 = List.fold_right (name_fold Idset.add) ids vars in
let vars1 = List.fold_right (name_fold Idset.add) ids vars' in
- (fi,bl,extern_typ scopes vars0 tyv.(i),
+ ((dummy_loc, fi),bl,extern_typ scopes vars0 tyv.(i),
sub_extern false scopes vars1 bv.(i))) idv
in
CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl))
| RSort (loc,s) -> CSort (loc,extern_rawsort s)
- | RHole (loc,e) -> CHole loc
+ | RHole (loc,e) -> CHole (loc, Some e)
| RCast (loc,c, CastConv (k,t)) ->
CCast (loc,sub_extern true scopes vars c, CastConv (k,extern_typ scopes vars t))
@@ -760,10 +759,10 @@ and sub_extern inctx (_,scopes) = extern inctx (None,scopes)
and factorize_prod scopes vars aty c =
try
- if !Options.raw_print or !print_no_symbol then raise No_match;
+ if !Flags.raw_print or !print_no_symbol then raise No_match;
([],extern_symbol scopes vars c (uninterp_notations c))
with No_match -> match c with
- | RProd (loc,(Name id as na),ty,c)
+ | RProd (loc,(Name id as na),bk,ty,c)
when same aty (extern_typ scopes vars (anonymize_if_reserved na ty))
& not (occur_var_constr_expr id aty) (* avoid na in ty escapes scope *)
-> let (nal,c) = factorize_prod scopes (Idset.add id vars) aty c in
@@ -772,10 +771,10 @@ and factorize_prod scopes vars aty c =
and factorize_lambda inctx scopes vars aty c =
try
- if !Options.raw_print or !print_no_symbol then raise No_match;
+ if !Flags.raw_print or !print_no_symbol then raise No_match;
([],extern_symbol scopes vars c (uninterp_notations c))
with No_match -> match c with
- | RLambda (loc,na,ty,c)
+ | RLambda (loc,na,bk,ty,c)
when same aty (extern_typ scopes vars (anonymize_if_reserved na ty))
& not (occur_name na aty) (* To avoid na in ty' escapes scope *)
-> let (nal,c) =
@@ -785,27 +784,27 @@ and factorize_lambda inctx scopes vars aty c =
and extern_local_binder scopes vars = function
[] -> ([],[])
- | (na,Some bd,ty)::l ->
+ | (na,bk,Some bd,ty)::l ->
let (ids,l) =
extern_local_binder scopes (name_fold Idset.add na vars) l in
(na::ids,
LocalRawDef((dummy_loc,na), extern false scopes vars bd) :: l)
- | (na,None,ty)::l ->
+ | (na,bk,None,ty)::l ->
let ty = extern_typ scopes vars (anonymize_if_reserved na ty) in
(match extern_local_binder scopes (name_fold Idset.add na vars) l with
- (ids,LocalRawAssum(nal,ty')::l)
+ (ids,LocalRawAssum(nal,k,ty')::l)
when same ty ty' &
match na with Name id -> not (occur_var_constr_expr id ty')
| _ -> true ->
(na::ids,
- LocalRawAssum((dummy_loc,na)::nal,ty')::l)
+ LocalRawAssum((dummy_loc,na)::nal,k,ty')::l)
| (ids,l) ->
(na::ids,
- LocalRawAssum([(dummy_loc,na)],ty) :: l))
+ LocalRawAssum([(dummy_loc,na)],Default bk,ty) :: l))
and extern_eqn inctx scopes vars (loc,ids,pl,c) =
- (loc,[List.map (extern_cases_pattern_in_scope scopes vars) pl],
+ (loc,[loc,List.map (extern_cases_pattern_in_scope scopes vars) pl],
extern inctx scopes vars c)
and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
@@ -815,10 +814,13 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
try
(* Adjusts to the number of arguments expected by the notation *)
let (t,args) = match t,n with
- | RApp (_,f,args), Some n when List.length args > n ->
+ | RApp (_,(RRef _ as f),args), Some n when List.length args >= n ->
let args1, args2 = list_chop n args in
(if n = 0 then f else RApp (dummy_loc,f,args1)), args2
- | _ -> t,[] in
+ | RApp (_,(RRef _ as f),args), None -> f, args
+ | RRef _, Some 0 -> RApp (dummy_loc,t,[]), []
+ | _, None -> t,[]
+ | _ -> raise No_match in
(* Try matching ... *)
let subst = match_aconstr t pat in
(* Try availability of interpretation ... *)
@@ -830,7 +832,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
| None -> raise No_match
(* Uninterpretation is allowed in current context *)
| Some (scopt,key) ->
- let scopes' = option_cons scopt scopes in
+ let scopes' = Option.List.cons scopt scopes in
let l =
List.map (fun (c,(scopt,scl)) ->
extern (* assuming no overloading: *) true
@@ -838,7 +840,12 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
subst in
insert_delimiters (make_notation loc ntn l) key)
| SynDefRule kn ->
- CRef (Qualid (loc, shortest_qualid_of_syndef vars kn)) in
+ let l =
+ List.map (fun (c,(scopt,scl)) ->
+ extern true (scopt,scl@scopes) vars c, None)
+ subst in
+ let a = CRef (Qualid (loc, shortest_qualid_of_syndef vars kn)) in
+ if l = [] then a else CApp (loc,(None,a),l) in
if args = [] then e
else
(* TODO: compute scopt for the extra args, in case, head is a ref *)
@@ -868,7 +875,7 @@ let extern_constr_gen at_top scopt env t =
let avoid = if at_top then ids_of_context env else [] in
let r = Detyping.detype at_top avoid (names_of_rel_context env) t in
let vars = vars_of_env env in
- extern (not at_top) (scopt,[]) vars r
+ extern false (scopt,[]) vars r
let extern_constr_in_scope at_top scope env t =
extern_constr_gen at_top (Some scope) env t
@@ -902,7 +909,7 @@ let rec raw_of_pat env = function
| Name id -> id
| Anonymous ->
anomaly "rawconstr_of_pattern: index to an anonymous variable"
- with Not_found -> id_of_string ("[REL "^(string_of_int n)^"]") in
+ with Not_found -> id_of_string ("_UNBOUND_REL_"^(string_of_int n)) in
RVar (loc,id)
| PMeta None -> RHole (loc,Evd.InternalHole)
| PMeta (Some n) -> RPatVar (loc,(false,n))
@@ -912,11 +919,11 @@ let rec raw_of_pat env = function
RApp (loc,RPatVar (loc,(true,n)),
List.map (raw_of_pat env) args)
| PProd (na,t,c) ->
- RProd (loc,na,raw_of_pat env t,raw_of_pat (na::env) c)
+ RProd (loc,na,Explicit,raw_of_pat env t,raw_of_pat (na::env) c)
| PLetIn (na,t,c) ->
RLetIn (loc,na,raw_of_pat env t, raw_of_pat (na::env) c)
| PLambda (na,t,c) ->
- RLambda (loc,na,raw_of_pat env t, raw_of_pat (na::env) c)
+ RLambda (loc,na,Explicit,raw_of_pat env t, raw_of_pat (na::env) c)
| PIf (c,b1,b2) ->
RIf (loc, raw_of_pat env c, (Anonymous,None),
raw_of_pat env b1, raw_of_pat env b2)
@@ -924,19 +931,19 @@ let rec raw_of_pat env = function
let nal,b = it_destRLambda_or_LetIn_names n (raw_of_pat env b) in
RLetTuple (loc,nal,(Anonymous,None),raw_of_pat env tm,b)
| PCase (_,PMeta None,tm,[||]) ->
- RCases (loc,None,[raw_of_pat env tm,(Anonymous,None)],[])
+ RCases (loc,RegularStyle,None,[raw_of_pat env tm,(Anonymous,None)],[])
| PCase ((_,cstr_nargs,indo,ind_nargs),p,tm,bv) ->
let brs = Array.to_list (Array.map (raw_of_pat env) bv) in
let brns = Array.to_list cstr_nargs in
(* ind is None only if no branch and no return type *)
- let ind = out_some indo in
+ let ind = Option.get indo in
let mat = simple_cases_matrix_of_branches ind brns brs in
let indnames,rtn =
if p = PMeta None then (Anonymous,None),None
else
- let nparams,n = out_some ind_nargs in
+ let nparams,n = Option.get ind_nargs in
return_type_of_predicate ind nparams n (raw_of_pat env p) in
- RCases (loc,rtn,[raw_of_pat env tm,indnames],mat)
+ RCases (loc,RegularStyle,rtn,[raw_of_pat env tm,indnames],mat)
| PFix f -> Detyping.detype false [] env (mkFix f)
| PCoFix c -> Detyping.detype false [] env (mkCoFix c)
| PSort s -> RSort (loc,s)
@@ -972,3 +979,8 @@ and raw_of_eqn env constr construct_nargs branch =
let extern_constr_pattern env pat =
extern true (None,[]) Idset.empty (raw_of_pat env pat)
+
+let extern_rel_context where env sign =
+ let a = detype_rel_context where [] (names_of_rel_context env) sign in
+ let vars = vars_of_env env in
+ snd (extern_local_binder (None,[]) vars a)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index ca145dd9..ec0a262b 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: constrextern.mli 8831 2006-05-19 09:29:54Z herbelin $ i*)
+(*i $Id: constrextern.mli 10790 2008-04-14 22:34:19Z herbelin $ i*)
(*i*)
open Util
@@ -42,9 +42,12 @@ val extern_constr_in_scope : bool -> scope_name -> env -> constr -> constr_expr
val extern_reference : loc -> Idset.t -> global_reference -> reference
val extern_type : bool -> env -> types -> constr_expr
val extern_sort : sorts -> rawsort
+val extern_rel_context : constr option -> env ->
+ rel_context -> local_binder list
(* Printing options *)
val print_implicits : bool ref
+val print_implicits_defensive : bool ref
val print_arguments : bool ref
val print_evar_arguments : bool ref
val print_coercions : bool ref
@@ -52,6 +55,10 @@ val print_universes : bool ref
val print_no_symbol : bool ref
val print_projections : bool ref
+(* Debug printing options *)
+val set_debug_global_reference_printer :
+ (loc -> global_reference -> reference) -> unit
+
(* This governs printing of implicit arguments. If [with_implicits] is
on and not [with_arguments] then implicit args are printed prefixed
by "!"; if [with_implicits] and [with_arguments] are both on the
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index e1ee5486..9abee4d4 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -6,11 +6,11 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: constrintern.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
+(* $Id: constrintern.ml 11065 2008-06-06 22:39:43Z msozeau $ *)
open Pp
open Util
-open Options
+open Flags
open Names
open Nameops
open Libnames
@@ -32,6 +32,8 @@ type var_internalisation_data =
type implicits_env = (identifier * var_internalisation_data) list
type full_implicits_env = identifier list * implicits_env
+type raw_binder = (name * binding_kind * rawconstr option * rawconstr)
+
let interning_grammar = ref false
(* Historically for parsing grammar rules, but in fact used only for
@@ -42,8 +44,6 @@ let for_grammar f x =
interning_grammar := false;
a
-let variables_bind = ref false
-
(**********************************************************************)
(* Internalisation errors *)
@@ -86,7 +86,7 @@ let explain_bad_patterns_number n1 n2 =
let explain_bad_explicitation_number n po =
match n with
- | ExplByPos n ->
+ | ExplByPos (n,_id) ->
let s = match po with
| None -> str "a regular argument"
| Some p -> int p in
@@ -142,15 +142,110 @@ let coqdoc_unfreeze (lt,tn,lp) =
token_number := tn;
last_pos := lp
-let add_glob loc ref =
- let sp = Nametab.sp_of_global ref in
- let lib_dp = Lib.library_part ref in
+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_trunc = drop_dirpath_prefix lib_dp mod_dp 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 fullname = string_of_qualid (make_qualid mod_dp_trunc id) in
- dump_string (Printf.sprintf "R%d %s %s\n" (fst (unloc loc)) filepath fullname)
+ 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)))
@@ -169,8 +264,8 @@ let dump_notation_location pos ((path,df),sc) =
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\"%s\n" (fst (unloc loc)) path df sc)
+ 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 *)
@@ -221,12 +316,12 @@ let contract_pat_notation ntn l =
(**********************************************************************)
(* Remembering the parsing scope of variables in notations *)
-let make_current_scope (tmp_scope,scopes) = option_cons tmp_scope scopes
+let make_current_scope (tmp_scope,scopes) = Option.List.cons tmp_scope scopes
let set_var_scope loc id (_,scopt,scopes) varscopes =
let idscopes = List.assoc id varscopes in
if !idscopes <> None &
- make_current_scope (out_some !idscopes)
+ make_current_scope (Option.get !idscopes)
<> make_current_scope (scopt,scopes) then
user_err_loc (loc,"set_var_scope",
pr_id id ++ str " already occurs in a different scope")
@@ -234,6 +329,92 @@ let set_var_scope loc id (_,scopt,scopes) varscopes =
idscopes := Some (scopt,scopes)
(**********************************************************************)
+(* Syntax extensions *)
+
+let traverse_binder subst (renaming,(ids,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'
+ 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 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
+ | 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
+ with Not_found ->
+ try
+ RVar (loc,List.assoc id renaming)
+ with Not_found ->
+ (* Happens for local notation joint with inductive/fixpoint defs *)
+ RVar (loc,id)
+ end
+ | 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 =
+ subst_aconstr_in_rawconstr loc interp subst
+ (renaming,(ids,None,scopes)) terminator in
+ let l = decode_constrlist_value a 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))
+ (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
+
+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 set_type_scope (ids,tmp_scope,scopes) =
+ (ids,Some Notation.type_scope,scopes)
+
+let reset_tmp_scope (ids,tmp_scope,scopes) =
+ (ids,None,scopes)
+
+let rec it_mkRProd env body =
+ match env with
+ (na, bk, _, t) :: tl -> it_mkRProd tl (RProd (dummy_loc, na, bk, t, body))
+ | [] -> body
+
+let rec it_mkRLambda env body =
+ match env with
+ (na, bk, _, t) :: tl -> it_mkRLambda tl (RLambda (dummy_loc, na, bk, t, body))
+ | [] -> body
+
+(**********************************************************************)
(* Discriminating between bound variables and global references *)
(* [vars1] is a set of name to avoid (used for the tactic language);
@@ -281,52 +462,60 @@ let find_appl_head_data (_,_,_,(_,impls)) = function
| RRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[]
| x -> x,[],[],[]
+let error_not_enough_arguments loc =
+ user_err_loc (loc,"",str "Abbreviation is not applied enough")
+
+let check_no_explicitation l =
+ let l = List.filter (fun (a,b) -> b <> None) l in
+ if l <> [] then
+ let loc = fst (Option.get (snd (List.hd l))) in
+ user_err_loc
+ (loc,"",str"Unexpected explicitation of the argument of an abbreviation")
+
(* Is it a global reference or a syntactic definition? *)
-let intern_qualid loc qid =
+let intern_qualid loc qid intern env args =
try match Nametab.extended_locate qid with
| TrueGlobal ref ->
- if !dump then add_glob loc ref;
- RRef (loc, ref)
+ add_glob loc ref;
+ RRef (loc, ref), args
| SyntacticDef sp ->
- Syntax_def.search_syntactic_definition loc sp
+ 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
with Not_found ->
error_global_not_found_loc loc qid
(* Rule out section vars since these should have been found by intern_var *)
-let intern_non_secvar_qualid loc qid =
- match intern_qualid loc qid with
- | RRef (loc, VarRef id) -> error_global_not_found_loc loc qid
+let intern_non_secvar_qualid loc qid intern env args =
+ match intern_qualid loc qid intern env args with
+ | RRef (loc, VarRef id),_ -> error_global_not_found_loc loc qid
| r -> r
-let intern_inductive r =
- let loc,qid = qualid_of_reference r in
- try match Nametab.extended_locate qid with
- | TrueGlobal (IndRef ind) -> ind, []
- | TrueGlobal _ -> raise Not_found
- | SyntacticDef sp ->
- (match Syntax_def.search_syntactic_definition loc sp with
- | RApp (_,RRef(_,IndRef ind),l)
- when List.for_all (function RHole _ -> true | _ -> false) l ->
- (ind, List.map (fun _ -> Anonymous) l)
- | _ -> raise Not_found)
- with Not_found ->
- error_global_not_found_loc loc qid
-
-let intern_reference env lvar = function
+let intern_applied_reference intern env lvar args = function
| Qualid (loc, qid) ->
- find_appl_head_data lvar (intern_qualid loc qid)
+ let r,args2 = intern_qualid loc qid intern env args in
+ find_appl_head_data lvar r, args2
| Ident (loc, id) ->
- try intern_var env lvar loc id
+ try intern_var env lvar loc id, args
with Not_found ->
let qid = make_short_qualid id in
- try find_appl_head_data lvar (intern_non_secvar_qualid loc qid)
+ try
+ let r,args2 = intern_non_secvar_qualid loc qid intern env args in
+ find_appl_head_data lvar r, args2
with e ->
(* Extra allowance for non globalizing functions *)
- if !interning_grammar then RVar (loc,id), [], [], []
+ if !interning_grammar then (RVar (loc,id), [], [], []),args
else raise e
let interp_reference vars r =
- let r,_,_,_ = intern_reference (Idset.empty,None,[]) (vars,[],[],([],[])) r
+ let (r,_,_,_),_ =
+ intern_applied_reference (fun _ -> error_not_enough_arguments dummy_loc)
+ (Idset.empty,None,[]) (vars,[],[],([],[])) [] r
in r
let apply_scope_env (ids,_,scopes) = function
@@ -339,10 +528,16 @@ let rec adjust_scopes env scopes = function
let (enva,scopes) = apply_scope_env env scopes in
enva :: adjust_scopes env scopes args
-let rec simple_adjust_scopes = function
- | _,[] -> []
- | [],_::args -> None :: simple_adjust_scopes ([],args)
- | sc::scopes,_::args -> sc :: simple_adjust_scopes (scopes,args)
+let rec simple_adjust_scopes n = function
+ | [] -> if n=0 then [] else None :: simple_adjust_scopes (n-1) []
+ | sc::scopes -> sc :: simple_adjust_scopes (n-1) scopes
+
+let find_remaining_constructor_scopes pl1 pl2 (ind,j as cstr) =
+ let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
+ let npar = mib.Declarations.mind_nparams in
+ snd (list_chop (List.length pl1 + npar)
+ (simple_adjust_scopes (npar + List.length pl2)
+ (find_arguments_scope (ConstructRef cstr))))
(**********************************************************************)
(* Cases *)
@@ -368,8 +563,7 @@ let rec has_duplicate = function
| x::l -> if List.mem x l then (Some x) else has_duplicate l
let loc_of_lhs lhs =
- join_loc (cases_pattern_expr_loc (List.hd (List.hd lhs)))
- (cases_pattern_expr_loc (list_last (list_last lhs)))
+ join_loc (fst (List.hd lhs)) (fst (list_last lhs))
let check_linearity lhs ids =
match has_duplicate ids with
@@ -412,6 +606,16 @@ let message_redundant_alias (id1,id2) =
(* Expanding notations *)
+let error_invalid_pattern_notation loc =
+ user_err_loc (loc,"",str "Invalid notation for pattern")
+
+let chop_aconstr_constructor loc (ind,k) args =
+ let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
+ let params,args = list_chop nparams args in
+ List.iter (function AHole _ -> ()
+ | _ -> error_invalid_pattern_notation loc) params;
+ args
+
let decode_patlist_value = function
| CPatCstr (_,_,l) -> l
| _ -> anomaly "Ill-formed list argument of notation"
@@ -445,13 +649,12 @@ let subst_cases_pattern loc alias intern subst scopes a =
end
| ARef (ConstructRef c) ->
([],[[], PatCstr (loc,c, [], alias)])
- | AApp (ARef (ConstructRef (ind,_ as c)),args) ->
- let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
- let _,args = list_chop nparams args in
+ | AApp (ARef (ConstructRef cstr),args) ->
+ let args = chop_aconstr_constructor loc cstr args in
let idslpll = List.map (aux Anonymous subst) args in
let ids',pll = product_of_cases_patterns [] idslpll in
let pl' = List.map (fun (subst,pl) ->
- subst,PatCstr (loc,c,pl,alias)) pll in
+ subst,PatCstr (loc,cstr,pl,alias)) pll in
ids', pl'
| AList (x,_,iter,terminator,lassoc) ->
(try
@@ -469,65 +672,57 @@ let subst_cases_pattern loc alias intern subst scopes a =
match pl with PatCstr (loc, c, pl, Anonymous) -> (subst, PatCstr (loc, c, pl, alias)) | _ -> x) v
with Not_found ->
anomaly "Inconsistent substitution of recursive notation")
- | t -> user_err_loc (loc,"",str "Invalid notation for pattern")
+ | t -> error_invalid_pattern_notation loc
in aux alias subst a
(* Differentiating between constructors and matching variables *)
type pattern_qualid_kind =
- | ConstrPat of (constructor * cases_pattern list)
+ | ConstrPat of constructor * (identifier list *
+ ((identifier * identifier) list * cases_pattern) list) list
| VarPat of identifier
-let rec patt_of_rawterm loc cstr =
- match cstr with
- | RRef (_,(ConstructRef c as x)) ->
- if !dump then add_glob loc x;
- (c,[])
- | RApp (_,RApp(_,h,l1),l2) -> patt_of_rawterm loc (RApp(loc,h,l1@l2))
- | RApp (_,RRef(_,(ConstructRef c as x)),pl) ->
- if !dump then add_glob loc x;
- let (mib,_) = Inductive.lookup_mind_specif (Global.env()) (fst c) in
- let npar = mib.Declarations.mind_nparams in
- let (params,args) =
- if List.length pl <= npar then (pl,[]) else
- list_chop npar pl in
- (* All parameters must be _ *)
- List.iter
- (function RHole _ -> ()
- | _ -> raise Not_found) params;
- let pl' = List.map
- (fun c ->
- let (c,pl) = patt_of_rawterm loc c in
- PatCstr(loc,c,pl,Anonymous)) args in
- (c,pl')
- | _ -> raise Not_found
-
-let find_constructor ref =
+let find_constructor ref f aliases pats scopes =
let (loc,qid) = qualid_of_reference ref in
let gref =
try extended_locate qid
- with Not_found ->
- raise (InternalisationError (loc,NotAConstructor ref)) in
- match gref with
- | SyntacticDef sp ->
- let sdef = Syntax_def.search_syntactic_definition loc sp in
- patt_of_rawterm loc sdef
- | TrueGlobal r ->
- let rec unf = function
- | ConstRef cst ->
- let v = Environ.constant_value (Global.env()) cst in
- unf (global_of_constr v)
- | ConstructRef c ->
- if !dump then add_glob loc r;
- c, []
- | _ -> raise Not_found
- in unf r
+ with Not_found -> raise (InternalisationError (loc,NotAConstructor ref)) in
+ match gref with
+ | SyntacticDef sp ->
+ let (vars,a) = Syntax_def.search_syntactic_definition loc sp in
+ (match a with
+ | ARef (ConstructRef cstr) ->
+ assert (vars=[]);
+ cstr, [], pats
+ | AApp (ARef (ConstructRef cstr),args) ->
+ let args = chop_aconstr_constructor loc cstr args in
+ let nvars = List.length vars in
+ 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
+ cstr, idspl1, pats2
+ | _ -> raise Not_found)
+
+ | TrueGlobal r ->
+ let rec unf = function
+ | ConstRef cst ->
+ let v = Environ.constant_value (Global.env()) cst in
+ unf (global_of_constr v)
+ | ConstructRef cstr ->
+ add_glob loc r;
+ cstr, [], pats
+ | _ -> raise Not_found
+ in unf r
let find_pattern_variable = function
| Ident (loc,id) -> id
| Qualid (loc,_) as x -> raise (InternalisationError(loc,NotAConstructor x))
-let maybe_constructor ref =
- try ConstrPat (find_constructor ref)
+let maybe_constructor ref f aliases scopes =
+ try
+ let c,idspl1,pl2 = find_constructor ref f aliases [] scopes in
+ assert (pl2 = []);
+ ConstrPat (c,idspl1)
with
(* patt var does not exists globally *)
| InternalisationError _ -> VarPat (find_pattern_variable ref)
@@ -537,39 +732,37 @@ let maybe_constructor ref =
str " is understood as a pattern variable");
VarPat (find_pattern_variable ref)
-let mustbe_constructor loc ref =
- try find_constructor ref
+let mustbe_constructor loc ref f aliases patl scopes =
+ try find_constructor ref f aliases patl scopes
with (Environ.NotEvaluableConst _ | Not_found) ->
raise (InternalisationError (loc,NotAConstructor ref))
-let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope =
- function
+let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope pat =
+ let intern_pat = intern_cases_pattern genv in
+ match pat with
| CPatAlias (loc, p, id) ->
let aliases' = merge_aliases aliases id in
- intern_cases_pattern genv scopes aliases' tmp_scope p
+ intern_pat scopes aliases' tmp_scope p
| CPatCstr (loc, head, pl) ->
- let c,pl0 = mustbe_constructor loc head in
- let argscs =
- simple_adjust_scopes (find_arguments_scope (ConstructRef c), pl) in
- check_constructor_length genv loc c pl0 pl;
- let idslpl =
- List.map2 (intern_cases_pattern genv scopes ([],[])) argscs pl in
- let (ids',pll) = product_of_cases_patterns ids idslpl in
+ let c,idslpl1,pl2 = mustbe_constructor loc head intern_pat aliases pl scopes in
+ check_constructor_length genv loc c idslpl1 pl2;
+ let argscs2 = find_remaining_constructor_scopes idslpl1 pl2 c in
+ let idslpl2 = List.map2 (intern_pat scopes ([],[])) argscs2 pl2 in
+ let (ids',pll) = product_of_cases_patterns ids (idslpl1@idslpl2) in
let pl' = List.map (fun (subst,pl) ->
- (subst, PatCstr (loc,c,pl0@pl,alias_of aliases))) pll in
+ (subst, PatCstr (loc,c,pl,alias_of aliases))) pll in
ids',pl'
| CPatNotation (loc,"- _",[CPatPrim(_,Numeral p)])
when Bigint.is_strictly_pos p ->
- let np = Numeral (Bigint.neg p) in
- intern_cases_pattern genv scopes aliases tmp_scope (CPatPrim(loc,np))
+ intern_pat scopes aliases tmp_scope (CPatPrim(loc,Numeral(Bigint.neg p)))
| CPatNotation (_,"( _ )",[a]) ->
- intern_cases_pattern genv scopes aliases tmp_scope 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;
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_cases_pattern genv) subst scopes
+ let ids'',pl = subst_cases_pattern loc (alias_of aliases) intern_pat subst scopes
c
in ids@ids'', pl
| CPatPrim (loc, p) ->
@@ -579,13 +772,14 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope =
if !dump then dump_notation_location (fst (unloc loc)) df;
(ids,[subst,c])
| CPatDelimiters (loc, key, e) ->
- intern_cases_pattern genv (find_delimiters_scope loc key::scopes)
- aliases None e
+ intern_pat (find_delimiters_scope loc key::scopes) aliases None e
| CPatAtom (loc, Some head) ->
- (match maybe_constructor head with
- | ConstrPat (c,args) ->
- check_constructor_length genv loc c [] [];
- (ids,[subst, PatCstr (loc,c,args,alias_of aliases)])
+ (match maybe_constructor head intern_pat aliases scopes with
+ | 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)
| VarPat id ->
let ids,subst = merge_aliases aliases id in
(ids,[subst, PatVar (loc,alias_of (ids,subst))]))
@@ -593,8 +787,7 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope =
(ids,[subst, PatVar (loc,alias_of aliases)])
| CPatOr (loc, pl) ->
assert (pl <> []);
- let pl' =
- List.map (intern_cases_pattern genv scopes aliases tmp_scope) pl in
+ let pl' = List.map (intern_pat scopes aliases tmp_scope) pl in
let (idsl,pl') = List.split pl' in
let ids = List.hd idsl in
check_or_pat_variables loc ids (List.tl idsl);
@@ -632,6 +825,44 @@ let push_name_env lvar (ids,tmpsc,scopes as env) = function
check_hidden_implicit_parameters id lvar;
(Idset.add id ids,tmpsc,scopes)
+let push_loc_name_env lvar (ids,tmpsc,scopes as env) loc = function
+ | Anonymous -> 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) na b ty =
+ let ctx = (na, b, ty) in
+ let (fvs, bind) = Implicit_quantifiers.generalize_class_binders_raw (pi1 env) [ctx] in
+ let env, ifvs = intern_typeclass_binders intern_type lvar (env,bl) fvs in
+ intern_typeclass_binders intern_type lvar (env,ifvs) bind
+
+let intern_local_binder_aux intern intern_type lvar ((ids,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 ->
+ intern_typeclass_binder intern_type lvar (env,bl) (List.hd nal) b ty)
+ | LocalRawDef((loc,na),def) ->
+ ((name_fold Idset.add na ids,ts,sc),
+ (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
+
(**********************************************************************)
(* Utilities for application *)
@@ -683,7 +914,7 @@ let extract_explicit_arg imps args =
user_err_loc (loc,"",str "Argument name " ++ pr_id id
++ str " occurs more than once");
id
- | ExplByPos p ->
+ | ExplByPos (p,_id) ->
let id =
try
let imp = List.nth imps (p-1) in
@@ -700,120 +931,53 @@ let extract_explicit_arg imps args =
in aux args
(**********************************************************************)
-(* Syntax extensions *)
-
-let traverse_binder subst (renaming,(ids,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'
- 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 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
- | 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
- with Not_found ->
- try
- RVar (loc,List.assoc id renaming)
- with Not_found ->
- (* Happens for local notation joint with inductive/fixpoint defs *)
- RVar (loc,id)
- end
- | 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 =
- subst_aconstr_in_rawconstr loc interp subst
- (renaming,(ids,None,scopes)) terminator in
- let l = decode_constrlist_value a 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))
- (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
-
-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 set_type_scope (ids,tmp_scope,scopes) =
- (ids,Some Notation.type_scope,scopes)
-
-let reset_tmp_scope (ids,tmp_scope,scopes) =
- (ids,None,scopes)
-
-(**********************************************************************)
(* Main loop *)
-let internalise sigma globalenv env allow_soapp lvar c =
+let internalise sigma globalenv env allow_patvar lvar c =
let rec intern (ids,tmp_scope,scopes as env) = function
| CRef ref as x ->
- let (c,imp,subscopes,l) = intern_reference env lvar ref in
+ let (c,imp,subscopes,l),_ =
+ intern_applied_reference intern env lvar [] ref in
(match intern_impargs c env imp subscopes l with
| [] -> c
| l -> RApp (constr_loc x, c, l))
| CFix (loc, (locid,iddef), dl) ->
- let lf = List.map (fun (id,_,_,_,_) -> id) dl in
+ let lf = List.map (fun ((_, id),_,_,_,_) -> id) dl in
let dl = Array.of_list dl in
let n =
- try
- (list_index iddef lf) -1
+ try list_index0 iddef lf
with Not_found ->
raise (InternalisationError (locid,UnboundFixName (false,iddef)))
in
let idl = Array.map
(fun (id,(n,order),bl,ty,bd) ->
let intern_ro_arg c f =
- let before, after = list_chop (succ (out_some n)) bl in
- let ((ids',_,_),rafter) =
- List.fold_left intern_local_binder (env,[]) after in
- let ro = (intern (ids', tmp_scope, scopes) c) in
- f ro, List.fold_left intern_local_binder (env,rafter) before
+ let idx =
+ match n with
+ Some (loc, n) -> list_index0 (Name n) (List.map snd (names_of_local_assums bl))
+ | None -> 0
+ in
+ let before, after = list_chop idx bl in
+ let ((ids',_,_) as env',rbefore) =
+ List.fold_left intern_local_binder (env,[]) before in
+ let ro =
+ match c with
+ | None -> RStructRec
+ | Some c' -> f (intern (ids', 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 ro, ((ids',_,_),rbl) =
+ let n, ro, ((ids',_,_),rbl) =
(match order with
- CStructRec ->
- RStructRec,
- List.fold_left intern_local_binder (env,[]) bl
- | CWfRec c ->
- intern_ro_arg c (fun r -> RWfRec r)
- | CMeasureRec c ->
- intern_ro_arg c (fun r -> RMeasureRec r))
- in
- let ids'' = List.fold_right Idset.add lf ids' in
+ | CStructRec ->
+ intern_ro_arg None (fun _ -> RStructRec)
+ | CWfRec c ->
+ intern_ro_arg (Some c) (fun r -> RWfRec r)
+ | CMeasureRec c ->
+ intern_ro_arg (Some c) (fun r -> RMeasureRec r))
+ 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
@@ -824,11 +988,10 @@ let internalise sigma globalenv env allow_soapp lvar c =
Array.map (fun (_,_,ty,_) -> ty) idl,
Array.map (fun (_,_,_,bd) -> bd) idl)
| CCoFix (loc, (locid,iddef), dl) ->
- let lf = List.map (fun (id,_,_,_) -> id) dl in
+ let lf = List.map (fun ((_, id),_,_,_) -> id) dl in
let dl = Array.of_list dl in
let n =
- try
- (list_index iddef lf) -1
+ try list_index0 iddef lf
with Not_found ->
raise (InternalisationError (locid,UnboundFixName (true,iddef)))
in
@@ -846,18 +1009,18 @@ let internalise sigma globalenv env allow_soapp lvar c =
Array.map (fun (_,ty,_) -> ty) idl,
Array.map (fun (_,_,bd) -> bd) idl)
| CArrow (loc,c1,c2) ->
- RProd (loc, Anonymous, intern_type env c1, intern_type env c2)
+ RProd (loc, Anonymous, Explicit, intern_type env c1, intern_type env c2)
| CProdN (loc,[],c2) ->
intern_type env c2
- | CProdN (loc,(nal,ty)::bll,c2) ->
- iterate_prod loc env ty (CProdN (loc, bll, c2)) nal
+ | CProdN (loc,(nal,bk,ty)::bll,c2) ->
+ iterate_prod loc env bk ty (CProdN (loc, bll, c2)) nal
| CLambdaN (loc,[],c2) ->
intern env c2
- | CLambdaN (loc,(nal,ty)::bll,c2) ->
- iterate_lam loc (reset_tmp_scope env) ty (CLambdaN (loc, bll, c2)) nal
- | CLetIn (loc,(_,na),c1,c2) ->
+ | CLambdaN (loc,(nal,bk,ty)::bll,c2) ->
+ iterate_lam loc (reset_tmp_scope env) bk ty (CLambdaN (loc, bll, c2)) nal
+ | CLetIn (loc,(loc1,na),c1,c2) ->
RLetIn (loc, na, intern (reset_tmp_scope env) c1,
- intern (push_name_env lvar env na) c2)
+ intern (push_loc_name_env lvar env loc1 na) c2)
| CNotation (loc,"- _",[CPrim (_,Numeral p)])
when Bigint.is_strictly_pos p ->
intern env (CPrim (loc,Numeral (Bigint.neg p)))
@@ -871,22 +1034,24 @@ let internalise sigma globalenv env allow_soapp lvar c =
| CDelimiters (loc, key, e) ->
intern (ids,None,find_delimiters_scope loc key::scopes) e
| CAppExpl (loc, (isproj,ref), args) ->
- let (f,_,args_scopes,_) = intern_reference env lvar ref in
+ let (f,_,args_scopes,_),args =
+ let args = List.map (fun a -> (a,None)) args in
+ intern_applied_reference intern env lvar args ref in
check_projection isproj (List.length args) f;
- RApp (loc, f, intern_args env args_scopes args)
+ RApp (loc, f, intern_args env args_scopes (List.map fst args))
| CApp (loc, (isproj,f), args) ->
let isproj,f,args = match f with
(* Compact notations like "t.(f args') args" *)
| CApp (_,(Some _,f), args') when isproj=None -> isproj,f,args'@args
(* Don't compact "(f args') args" to resolve implicits separately *)
| _ -> isproj,f,args in
- let (c,impargs,args_scopes,l) =
+ let (c,impargs,args_scopes,l),args =
match f with
- | CRef ref -> intern_reference env lvar ref
+ | CRef ref -> intern_applied_reference intern env lvar args ref
| CNotation (loc,ntn,[]) ->
let c = intern_notation intern env loc ntn [] in
- find_appl_head_data lvar c
- | x -> (intern env f,[],[],[]) in
+ find_appl_head_data lvar c, args
+ | x -> (intern env f,[],[],[]), args in
let args =
intern_impargs c env impargs args_scopes (merge_impargs l args) in
check_projection isproj (List.length args) c;
@@ -894,38 +1059,36 @@ let internalise sigma globalenv env allow_soapp lvar c =
(* Now compact "(f args') args" *)
| RApp (loc', f', args') -> RApp (join_loc loc' loc, f',args'@args)
| _ -> RApp (loc, c, args))
- | CCases (loc, rtnpo, tms, eqns) ->
+ | CCases (loc, sty, rtnpo, tms, eqns) ->
let tms,env' = List.fold_right
(fun citm (inds,env) ->
let (tm,ind),nal = intern_case_item env citm in
(tm,ind)::inds,List.fold_left (push_name_env lvar) env nal)
tms ([],env) in
- let rtnpo = option_map (intern_type env') rtnpo in
+ let rtnpo = Option.map (intern_type env') rtnpo in
let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
- RCases (loc, rtnpo, tms, List.flatten eqns')
+ RCases (loc, sty, rtnpo, tms, List.flatten eqns')
| CLetTuple (loc, nal, (na,po), b, c) ->
let env' = reset_tmp_scope env in
let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in
let env'' = List.fold_left (push_name_env lvar) env ids in
- let p' = option_map (intern_type env'') po in
+ let p' = Option.map (intern_type env'') po in
RLetTuple (loc, nal, (na', p'), b',
intern (List.fold_left (push_name_env lvar) env nal) c)
| CIf (loc, c, (na,po), b1, b2) ->
let env' = reset_tmp_scope env in
let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in
let env'' = List.fold_left (push_name_env lvar) env ids in
- let p' = option_map (intern_type env'') po in
+ let p' = Option.map (intern_type env'') po in
RIf (loc, c', (na', p'), intern env b1, intern env b2)
- | CHole loc ->
- RHole (loc, Evd.QuestionMark true)
- | CPatVar (loc, n) when allow_soapp ->
+ | CHole (loc, k) ->
+ RHole (loc, match k with Some k -> k | None -> Evd.QuestionMark true)
+ | CPatVar (loc, n) when allow_patvar ->
RPatVar (loc, n)
- | CPatVar (loc, (false,n)) ->
- error_unbound_patvar loc n
| CPatVar (loc, _) ->
raise (InternalisationError (loc,NegativeMetavariable))
- | CEvar (loc, n) ->
- REvar (loc, n, None)
+ | CEvar (loc, n, l) ->
+ REvar (loc, n, Option.map (List.map (intern env)) l)
| CSort (loc, s) ->
RSort(loc,s)
| CCast (loc, c1, CastConv (k, c2)) ->
@@ -937,29 +1100,20 @@ let internalise sigma globalenv env allow_soapp lvar c =
and intern_type env = intern (set_type_scope env)
- and intern_local_binder ((ids,ts,sc as env),bl) = function
- | LocalRawAssum(nal,ty) ->
- 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,None,ty)::bl))
- (env,bl) nal
- | LocalRawDef((loc,na),def) ->
- ((name_fold Idset.add na ids,ts,sc),
- (na,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
+ and intern_local_binder env bind =
+ intern_local_binder_aux intern intern_type lvar env bind
(* Expands a multiple pattern into a disjunction of multiple patterns *)
- and intern_multiple_pattern scopes pl =
+ and intern_multiple_pattern scopes n (loc,pl) =
let idsl_pll =
List.map (intern_cases_pattern globalenv scopes ([],[]) None) pl in
+ check_number_of_pattern loc n pl;
product_of_cases_patterns [] idsl_pll
(* Expands a disjunction of multiple pattern *)
- and intern_disjunctive_multiple_pattern scopes loc mpl =
+ and intern_disjunctive_multiple_pattern scopes loc n mpl =
assert (mpl <> []);
- let mpl' = List.map (intern_multiple_pattern scopes) mpl in
+ let mpl' = List.map (intern_multiple_pattern scopes n) mpl in
let (idsl,mpl') = List.split mpl' in
let ids = List.hd idsl in
check_or_pat_variables loc ids (List.tl idsl);
@@ -967,10 +1121,9 @@ let internalise sigma globalenv env allow_soapp lvar c =
(* Expands a pattern-matching clause [lhs => rhs] *)
and intern_eqn n (ids,tmp_scope,scopes) (loc,lhs,rhs) =
- let eqn_ids,pll = intern_disjunctive_multiple_pattern scopes loc lhs in
+ 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;
- check_number_of_pattern loc n (snd (List.hd pll));
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
@@ -1008,23 +1161,40 @@ let internalise sigma globalenv env allow_soapp lvar c =
| _, None -> Anonymous
| _, Some na -> na in
(tm',(na,typ)), na::ids
-
- and iterate_prod loc2 env ty body = function
+
+ and iterate_prod loc2 env bk ty body nal =
+ let rec default env bk = function
| (loc1,na)::nal ->
if nal <> [] then check_capture loc1 ty na;
- let body = iterate_prod loc2 (push_name_env lvar env na) ty body nal in
+ let body = default (push_loc_name_env lvar env loc1 na) bk nal in
let ty = locate_if_isevar loc1 na (intern_type env ty) in
- RProd (join_loc loc1 loc2, na, ty, body)
+ RProd (join_loc loc1 loc2, na, bk, ty, body)
| [] -> intern_type env body
-
- and iterate_lam loc2 env ty body = function
- | (loc1,na)::nal ->
- if nal <> [] then check_capture loc1 ty na;
- let body = iterate_lam loc2 (push_name_env lvar env na) ty body nal in
- let ty = locate_if_isevar loc1 na (intern_type env ty) in
- RLambda (join_loc loc1 loc2, na, ty, body)
- | [] -> intern env body
-
+ in
+ match bk with
+ | Default b -> default env b nal
+ | TypeClass b ->
+ let env, ibind = intern_typeclass_binder intern_type lvar
+ (env, []) (List.hd nal) b ty in
+ let body = intern_type env body in
+ it_mkRProd ibind body
+
+ and iterate_lam loc2 env bk ty body nal =
+ let rec default env bk = function
+ | (loc1,na)::nal ->
+ if nal <> [] then check_capture loc1 ty na;
+ let body = default (push_loc_name_env lvar env loc1 na) bk nal in
+ let ty = locate_if_isevar loc1 na (intern_type env ty) in
+ RLambda (join_loc loc1 loc2, na, bk, ty, body)
+ | [] -> intern env body
+ in match bk with
+ | Default b -> default env b nal
+ | TypeClass b ->
+ let env, ibind = intern_typeclass_binder intern_type lvar
+ (env, []) (List.hd nal) b ty in
+ let body = intern env body in
+ it_mkRLambda ibind body
+
and intern_impargs c env l subscopes args =
let eargs, rargs = extract_explicit_arg l args in
let rec aux n impl subscopes eargs rargs =
@@ -1037,10 +1207,9 @@ let internalise sigma globalenv env allow_soapp lvar c =
let eargs' = List.remove_assoc id eargs in
intern enva a :: aux (n+1) impl' subscopes' eargs' rargs
with Not_found ->
- if rargs=[] & eargs=[] &
- not (List.for_all is_status_implicit impl') then
- (* Less regular arguments than expected: don't complete *)
- (* with implicit arguments *)
+ if rargs=[] & eargs=[] & not (maximal_insertion_of imp) then
+ (* Less regular arguments than expected: complete *)
+ (* with implicit arguments if maximal insertion is set *)
[]
else
RHole (set_hole_implicit (n,get_implicit_name n l) c) ::
@@ -1051,7 +1220,7 @@ let internalise sigma globalenv env allow_soapp lvar c =
| (imp::impl', []) ->
if eargs <> [] then
(let (id,(loc,_)) = List.hd eargs in
- user_err_loc (loc,"",str "Not enough non implicit
+ user_err_loc (loc,"",str "Not enough non implicit
arguments to accept the argument bound to " ++ pr_id id));
[]
| ([], rargs) ->
@@ -1082,13 +1251,13 @@ let extract_ids env =
Idset.empty
let intern_gen isarity sigma env
- ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[]))
+ ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
c =
let tmp_scope =
if isarity then Some Notation.type_scope else None in
- internalise sigma env (extract_ids env, tmp_scope,[])
- allow_soapp (ltacvars,Environ.named_context env, [], impls) c
-
+ internalise sigma env (extract_ids env, tmp_scope,[])
+ allow_patvar (ltacvars,Environ.named_context env, [], impls) c
+
let intern_constr sigma env c = intern_gen false sigma env c
let intern_type sigma env c = intern_gen true sigma env c
@@ -1104,17 +1273,36 @@ let intern_pattern env patt =
let intern_ltac isarity ltacvars sigma env c =
intern_gen isarity sigma env ~ltacvars:ltacvars c
+type manual_implicits = (explicitation * (bool * bool)) list
+
+let implicits_of_rawterm l =
+ let rec aux i c =
+ match c with
+ RProd (loc, na, bk, t, b) | RLambda (loc, na, bk, t, b) ->
+ let rest = aux (succ i) b in
+ if bk = Implicit then
+ let name =
+ match na with
+ Name id -> Some id
+ | Anonymous -> None
+ in
+ (ExplByPos (i, name), (true, true)) :: rest
+ else rest
+ | RLetIn (loc, na, t, b) -> aux i b
+ | _ -> []
+ in aux 1 l
+
(*********************************************************************)
(* Functions to parse and interpret constructions *)
let interp_gen kind sigma env
- ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[]))
+ ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
c =
- Default.understand_gen kind sigma env
- (intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars sigma env c)
+ let c = intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars sigma env c in
+ Default.understand_gen kind sigma env c
let interp_constr sigma env c =
- interp_gen (OfType None) sigma env c
+ interp_gen (OfType None) sigma env c
let interp_type sigma env ?(impls=([],[])) c =
interp_gen IsType sigma env ~impls c
@@ -1128,25 +1316,46 @@ let interp_open_constr sigma env c =
let interp_constr_judgment sigma env c =
Default.understand_judgment sigma env (intern_constr sigma env c)
-
-let interp_constr_evars_gen isevars env ?(impls=([],[])) kind c =
- Default.understand_tcc_evars isevars env kind
- (intern_gen (kind=IsType) ~impls (Evd.evars_of !isevars) env c)
-
-let interp_casted_constr_evars isevars env ?(impls=([],[])) c typ =
- interp_constr_evars_gen isevars env ~impls (OfType (Some typ)) c
-
-let interp_type_evars isevars env ?(impls=([],[])) c =
- interp_constr_evars_gen isevars env IsType ~impls c
-
-let interp_constr_judgment_evars isevars env c =
- Default.understand_judgment_tcc isevars env
- (intern_constr (Evd.evars_of !isevars) env c)
+let interp_constr_evars_gen_impls ?evdref
+ env ?(impls=([],[])) kind c =
+ match evdref with
+ | None ->
+ let c = intern_gen (kind=IsType) ~impls Evd.empty env c in
+ let imps = implicits_of_rawterm c in
+ Default.understand_gen kind Evd.empty env c, imps
+ | Some evdref ->
+ let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in
+ let imps = implicits_of_rawterm c in
+ Default.understand_tcc_evars evdref env kind c, imps
+
+let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c =
+ let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in
+ Default.understand_tcc_evars evdref env kind c
+
+let interp_casted_constr_evars_impls ?evdref
+ env ?(impls=([],[])) c typ =
+ interp_constr_evars_gen_impls ?evdref env ~impls (OfType (Some typ)) c
+
+let interp_type_evars_impls ?evdref env ?(impls=([],[])) c =
+ interp_constr_evars_gen_impls ?evdref env IsType ~impls c
+
+let interp_constr_evars_impls ?evdref env ?(impls=([],[])) c =
+ interp_constr_evars_gen_impls ?evdref env (OfType None) ~impls c
+
+let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ =
+ interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c
+
+let interp_type_evars evdref env ?(impls=([],[])) c =
+ interp_constr_evars_gen evdref env IsType ~impls c
+
+let interp_constr_judgment_evars evdref env c =
+ Default.understand_judgment_tcc evdref env
+ (intern_constr (Evd.evars_of !evdref) env c)
type ltac_sign = identifier list * unbound_ltac_var_map
let interp_constrpattern sigma env c =
- pattern_of_rawconstr (intern_gen false sigma env ~allow_soapp:true c)
+ pattern_of_rawconstr (intern_gen false sigma env ~allow_patvar:true c)
let interp_aconstr impls vars a =
let env = Global.env () in
@@ -1169,50 +1378,58 @@ let interp_binder sigma env na t =
let t' = locate_if_isevar (loc_of_rawconstr t) na t in
Default.understand_type sigma env t'
-let interp_binder_evars isevars env na t =
- let t = intern_gen true (Evd.evars_of !isevars) env t in
+let interp_binder_evars evdref env na t =
+ let t = intern_gen true (Evd.evars_of !evdref) env t in
let t' = locate_if_isevar (loc_of_rawconstr t) na t in
- Default.understand_tcc_evars isevars env IsType t'
+ Default.understand_tcc_evars evdref env IsType t'
open Environ
open Term
-let interp_context sigma env params =
- List.fold_left
- (fun (env,params) d -> match d with
- | LocalRawAssum ([_,na],(CHole _ as t)) ->
- let t = interp_binder sigma env na t in
- let d = (na,None,t) in
- (push_rel d env, d::params)
- | LocalRawAssum (nal,t) ->
- let t = interp_type sigma env t in
- let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in
- let ctx = List.rev ctx in
- (push_rel_context ctx env, ctx@params)
- | LocalRawDef ((_,na),c) ->
- let c = interp_constr_judgment sigma env c in
- let d = (na, Some c.uj_val, c.uj_type) in
- (push_rel d env,d::params))
- (env,[]) params
-
-let interp_context_evars isevars env params =
- List.fold_left
- (fun (env,params) d -> match d with
- | LocalRawAssum ([_,na],(CHole _ as t)) ->
- let t = interp_binder_evars isevars env na t in
- let d = (na,None,t) in
- (push_rel d env, d::params)
- | LocalRawAssum (nal,t) ->
- let t = interp_type_evars isevars env t in
- let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in
- let ctx = List.rev ctx in
- (push_rel_context ctx env, ctx@params)
- | LocalRawDef ((_,na),c) ->
- let c = interp_constr_judgment_evars isevars env c in
- let d = (na, Some c.uj_val, c.uj_type) in
- (push_rel d env,d::params))
- (env,[]) params
+let my_intern_constr sigma env lvar acc c =
+ internalise sigma env acc false lvar 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 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)
+
+let interp_context_gen understand_type understand_judgment env bl =
+ let (env, par, _, impls) =
+ List.fold_left
+ (fun (env,params,n,impls) (na, k, b, t) ->
+ match b with
+ None ->
+ let t' = locate_if_isevar (loc_of_rawconstr t) na t in
+ let t = understand_type env t' in
+ let d = (na,None,t) in
+ let impls =
+ if k = Implicit then
+ let na = match na with Name n -> Some n | Anonymous -> None in
+ (ExplByPos (n, na), (true, true)) :: impls
+ else impls
+ in
+ (push_rel d env, d::params, succ n, impls)
+ | 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))
+ (env,[],1,[]) (List.rev bl)
+ in (env, par), impls
+let interp_context sigma env params =
+ let bl = intern_context 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
+ interp_context_gen (fun env t -> Default.understand_tcc_evars evdref env IsType t)
+ (Default.understand_judgment_tcc evdref) env bl
+
(**********************************************************************)
(* Locating reference, possibly via an abbreviation *)
@@ -1221,7 +1438,7 @@ let locate_reference qid =
| TrueGlobal ref -> ref
| SyntacticDef kn ->
match Syntax_def.search_syntactic_definition dummy_loc kn with
- | Rawterm.RRef (_,ref) -> ref
+ | [],ARef ref -> ref
| _ -> raise Not_found
let is_global id =
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 4479fcd4..ea7020be 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 9976 2007-07-12 11:58:30Z msozeau $ i*)
+(*i $Id: constrintern.mli 11024 2008-05-30 12:41:39Z msozeau $ i*)
(*i*)
open Names
@@ -45,8 +45,12 @@ type var_internalisation_data =
type implicits_env = (identifier * var_internalisation_data) list
type full_implicits_env = identifier list * implicits_env
+type manual_implicits = (explicitation * (bool * bool)) list
+
type ltac_sign = identifier list * unbound_ltac_var_map
+type raw_binder = (name * binding_kind * rawconstr option * rawconstr)
+
(*s Internalisation performs interpretation of global names and notations *)
val intern_constr : evar_map -> env -> constr_expr -> rawconstr
@@ -54,19 +58,21 @@ val intern_constr : evar_map -> env -> constr_expr -> rawconstr
val intern_type : evar_map -> env -> constr_expr -> rawconstr
val intern_gen : bool -> evar_map -> env ->
- ?impls:full_implicits_env -> ?allow_soapp:bool -> ?ltacvars:ltac_sign ->
+ ?impls:full_implicits_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
constr_expr -> rawconstr
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
+
(*s Composing internalisation with pretyping *)
(* Main interpretation function *)
val interp_gen : typing_constraint -> evar_map -> env ->
- ?impls:full_implicits_env -> ?allow_soapp:bool -> ?ltacvars:ltac_sign ->
+ ?impls:full_implicits_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
constr_expr -> constr
(* Particular instances *)
@@ -74,14 +80,25 @@ val interp_gen : typing_constraint -> evar_map -> env ->
val interp_constr : evar_map -> env ->
constr_expr -> constr
-val interp_casted_constr : evar_map -> env -> ?impls:full_implicits_env ->
- constr_expr -> types -> constr
-
val interp_type : evar_map -> env -> ?impls:full_implicits_env ->
constr_expr -> types
val interp_open_constr : evar_map -> env -> constr_expr -> evar_map * constr
+val interp_casted_constr : evar_map -> env -> ?impls:full_implicits_env ->
+ constr_expr -> types -> constr
+
+(* Accepting evars and giving back the manual implicits in addition. *)
+
+val interp_casted_constr_evars_impls : ?evdref:(evar_defs ref) -> env ->
+ ?impls:full_implicits_env -> constr_expr -> types -> constr * manual_implicits
+
+val interp_type_evars_impls : ?evdref:(evar_defs ref) -> env -> ?impls:full_implicits_env ->
+ constr_expr -> types * manual_implicits
+
+val interp_constr_evars_impls : ?evdref:(evar_defs ref) -> env -> ?impls:full_implicits_env ->
+ constr_expr -> constr * manual_implicits
+
val interp_casted_constr_evars : evar_defs ref -> env ->
?impls:full_implicits_env -> constr_expr -> types -> constr
@@ -103,12 +120,14 @@ val interp_reference : ltac_sign -> reference -> rawconstr
val interp_binder : evar_map -> env -> name -> constr_expr -> types
+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
+val interp_context : evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits
val interp_context_evars :
- evar_defs ref -> env -> local_binder list -> env * rel_context
+ evar_defs ref -> env -> local_binder list -> (env * rel_context) * manual_implicits
(* Locating references of constructions, possibly via a syntactic definition *)
@@ -130,3 +149,5 @@ val for_grammar : ('a -> 'b) -> 'a -> 'b
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/coqlib.ml b/interp/coqlib.ml
index 0c3ffd0c..65e4dcd5 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqlib.ml 10067 2007-08-09 17:13:16Z msozeau $ *)
+(* $Id: coqlib.ml 11072 2008-06-08 16:13:37Z herbelin $ *)
open Util
open Pp
@@ -36,13 +36,6 @@ let coq_constant locstr dir s = constr_of_global (coq_reference locstr dir s)
let gen_reference = coq_reference
let gen_constant = coq_constant
-let list_try_find f =
- let rec try_find_f = function
- | [] -> raise Not_found
- | h::t -> try f h with Not_found -> try_find_f t
- in
- try_find_f
-
let has_suffix_in_dirs dirs ref =
let dir = dirpath (sp_of_global ref) in
List.exists (fun d -> is_dirpath_prefix_of d dir) dirs
@@ -77,7 +70,7 @@ let check_required_library d =
(dummy_loc,make_qualid (make_dirpath (List.rev prefix)) m)
*)
(* or failing ...*)
- error ("Library "^(list_last d)^" has to be required first")
+ error ("Library "^(string_of_dirpath dir)^" has to be required first")
(************************************************************************)
(* Specific Coq objects *)
@@ -109,13 +102,22 @@ let init_id = id_of_string "Init"
let arith_id = id_of_string "Arith"
let datatypes_id = id_of_string "Datatypes"
-let logic_module = make_dir ["Coq";"Init";"Logic"]
+let logic_module_name = ["Coq";"Init";"Logic"]
+let logic_module = make_dir logic_module_name
let logic_type_module = make_dir ["Coq";"Init";"Logic_Type"]
let datatypes_module = make_dir ["Coq";"Init";"Datatypes"]
let arith_module = make_dir ["Coq";"Arith";"Arith"]
(* TODO: temporary hack *)
let make_kn dir id = Libnames.encode_kn dir id
+let make_con dir id = Libnames.encode_con dir id
+
+(** Identity *)
+
+let id = make_con datatypes_module (id_of_string "id")
+let type_of_id = make_con datatypes_module (id_of_string "ID")
+
+let _ = Cases.set_impossible_default_clause (mkConst id,mkConst type_of_id)
(** Natural numbers *)
let nat_kn = make_kn datatypes_module (id_of_string "nat")
@@ -150,8 +152,19 @@ type coq_sigma_data = {
intro : constr;
typ : constr }
+type coq_bool_data = {
+ andb : constr;
+ andb_prop : constr;
+ andb_true_intro : constr}
+
type 'a delayed = unit -> 'a
+let build_bool_type () =
+ { andb = init_constant ["Datatypes"] "andb";
+ andb_prop = init_constant ["Datatypes"] "andb_prop";
+ andb_true_intro = init_constant ["Datatypes"] "andb_true_intro" }
+
+
let build_sigma_set () = anomaly "Use build_sigma_type"
let build_sigma_type () =
@@ -190,7 +203,8 @@ let coq_eq_congr = lazy_init_constant ["Logic"] "f_equal"
let coq_eq_sym = lazy_init_constant ["Logic"] "sym_eq"
let coq_f_equal2 = lazy_init_constant ["Logic"] "f_equal2"
-let build_coq_eq_data () = {
+let build_coq_eq_data () =
+ let _ = check_required_library logic_module_name in {
eq = Lazy.force coq_eq_eq;
refl = Lazy.force coq_eq_refl;
ind = Lazy.force coq_eq_ind;
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 7254800c..a85b6a8e 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: coqlib.mli 10067 2007-08-09 17:13:16Z msozeau $ i*)
+(*i $Id: coqlib.mli 10180 2007-10-05 13:02:23Z vsiles $ i*)
(*i*)
open Names
@@ -73,6 +73,7 @@ val path_of_false : constructor
val glob_true : global_reference
val glob_false : global_reference
+
(* Equality *)
val glob_eq : global_reference
@@ -84,6 +85,12 @@ val glob_eq : global_reference
type 'a delayed = unit -> 'a
+type coq_bool_data = {
+ andb : constr;
+ andb_prop : constr;
+ andb_true_intro : constr}
+val build_bool_type : coq_bool_data delayed
+
(*s For Equality tactics *)
type coq_sigma_data = {
proj1 : constr;
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 77ed1fe6..49c157f2 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: genarg.ml 8926 2006-06-08 20:23:17Z herbelin $ *)
+(* $Id: genarg.ml 10753 2008-04-04 14:55:47Z herbelin $ *)
open Pp
open Util
@@ -16,6 +16,7 @@ open Nametab
open Rawterm
open Topconstr
open Term
+open Evd
type argument_type =
(* Basic types *)
@@ -44,19 +45,25 @@ 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 rawconstr_and_expr = rawconstr * constr_expr option
+type open_constr_expr = unit * constr_expr
+type open_rawconstr = unit * rawconstr_and_expr
+
+type 'a with_ebindings = 'a * open_constr bindings
(* Dynamics but tagged by a type expression *)
-type ('a,'b) generic_argument = argument_type * Obj.t
+type 'a generic_argument = argument_type * Obj.t
let dyntab = ref ([] : string list)
type rlevel = constr_expr
type glevel = rawconstr_and_expr
-type tlevel = constr
+type tlevel = open_constr
-type ('a,'b,'c) abstract_argument_type = argument_type
+type ('a,'b) abstract_argument_type = argument_type
let create_arg s =
if List.mem s !dyntab then
@@ -72,6 +79,8 @@ type intro_pattern_expr =
| IntroWildcard
| IntroIdentifier of identifier
| IntroAnonymous
+ | IntroRewrite of bool
+ | IntroFresh of identifier
and case_intro_pattern_expr = intro_pattern_expr list list
let rec pr_intro_pattern = function
@@ -79,6 +88,9 @@ let rec pr_intro_pattern = function
| IntroWildcard -> str "_"
| IntroIdentifier id -> pr_id id
| IntroAnonymous -> str "?"
+ | IntroRewrite true -> str "->"
+ | IntroRewrite false -> str "<-"
+ | IntroFresh id -> str "?" ++ pr_id id
and pr_case_intro_pattern = function
| [pl] ->
@@ -88,10 +100,6 @@ and pr_case_intro_pattern = function
hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll)
++ str "]"
-type open_constr = Evd.evar_map * Term.constr
-type open_constr_expr = unit * constr_expr
-type open_rawconstr = unit * rawconstr_and_expr
-
let rawwit_bool = BoolArgType
let globwit_bool = BoolArgType
let wit_bool = BoolArgType
@@ -218,7 +226,7 @@ let app_list1 f = function
let app_opt f = function
| (OptArgType t as u, l) ->
let o = Obj.magic l in
- (u, Obj.repr (option_map (fun x -> out_gen t (f (in_gen t x))) o))
+ (u, Obj.repr (Option.map (fun x -> out_gen t (f (in_gen t x))) o))
| _ -> failwith "Genarg: not an opt"
let app_pair f1 f2 = function
diff --git a/interp/genarg.mli b/interp/genarg.mli
index c4275589..3548585b 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 8983 2006-06-23 13:21:49Z herbelin $ i*)
+(*i $Id: genarg.mli 10753 2008-04-04 14:55:47Z herbelin $ i*)
open Util
open Names
@@ -15,23 +15,29 @@ open Libnames
open Rawterm
open Topconstr
open Term
+open Evd
type 'a and_short_name = 'a * identifier located option
+type 'a or_by_notation = AN of 'a | ByNotation of loc * string
+
(* In globalize tactics, we need to keep the initial [constr_expr] to recompute*)
(* in the environment by the effective calls to Intro, Inversion, etc *)
(* The [constr_expr] field is [None] in TacDef though *)
type rawconstr_and_expr = rawconstr * constr_expr option
-type open_constr = Evd.evar_map * Term.constr
type open_constr_expr = unit * constr_expr
type open_rawconstr = unit * rawconstr_and_expr
+type 'a with_ebindings = 'a * open_constr bindings
+
type intro_pattern_expr =
| IntroOrAndPattern of case_intro_pattern_expr
| IntroWildcard
| IntroIdentifier of identifier
| IntroAnonymous
+ | IntroRewrite of bool
+ | IntroFresh of identifier
and case_intro_pattern_expr = intro_pattern_expr list list
val pr_intro_pattern : intro_pattern_expr -> Pp.std_ppcmds
@@ -40,21 +46,34 @@ val pr_case_intro_pattern : case_intro_pattern_expr -> Pp.std_ppcmds
(* The route of a generic argument, from parsing to evaluation
\begin{verbatim}
- parsing in_raw out_raw
- char stream ----> rawtype ----> rawconstr generic_argument ---->
- |
- | interp
- V
- type <---- constr generic_argument <----
- out in
+ parsing in_raw out_raw
+ char stream ----> rawtype ----> constr_expr generic_argument --------|
+ encapsulation decaps |
+ |
+ V
+ rawtype
+ |
+ globalization |
+ V
+ glob_type
+ |
+ encaps |
+ in_glob |
+ V
+ rawconstr generic_argument
+ |
+ out in out_glob |
+ type <--- constr generic_argument <---- type <------ rawtype <--------|
+ | decaps encaps interp decaps
+ |
+ V
+effective use
\end{verbatim}
-To distinguish between the uninterpreted (raw) and the interpreted
-worlds, we annotate the type [generic_argument] by a phantom argument
-which is either [constr_expr] or [constr] (actually we add also a second
-argument [raw_tactic_expr] and [tactic], but this is only for technical
-reasons, because these types are undefined at the type of compilation
-of [Genarg]).
+To distinguish between the uninterpreted (raw), globalized and
+interpreted worlds, we annotate the type [generic_argument] by a
+phantom argument which is either [constr_expr], [rawconstr] or
+[constr].
Transformation for each type :
\begin{verbatim}
@@ -84,147 +103,146 @@ ExtraArgType of string '_a '_b
(* All of [rlevel], [glevel] and [tlevel] must be non convertible
to ensure the injectivity of the type inference from type
- [('co,'ta) generic_argument] to [('a,'co,'ta) abstract_argument_type]
- is injective; this guarantees that, for 'b fixed, the type of
+ ['co generic_argument] to [('a,'co) abstract_argument_type];
+ this guarantees that, for 'co fixed, the type of
out_gen is monomorphic over 'a, hence type-safe
*)
type rlevel = constr_expr
type glevel = rawconstr_and_expr
-type tlevel = constr
+type tlevel = open_constr
-type ('a,'co,'ta) abstract_argument_type
+type ('a,'co) abstract_argument_type
-val rawwit_bool : (bool,rlevel,'ta) abstract_argument_type
-val globwit_bool : (bool,glevel,'ta) abstract_argument_type
-val wit_bool : (bool,tlevel,'ta) abstract_argument_type
+val rawwit_bool : (bool,rlevel) abstract_argument_type
+val globwit_bool : (bool,glevel) abstract_argument_type
+val wit_bool : (bool,tlevel) abstract_argument_type
-val rawwit_int : (int,rlevel,'ta) abstract_argument_type
-val globwit_int : (int,glevel,'ta) abstract_argument_type
-val wit_int : (int,tlevel,'ta) abstract_argument_type
+val rawwit_int : (int,rlevel) abstract_argument_type
+val globwit_int : (int,glevel) abstract_argument_type
+val wit_int : (int,tlevel) abstract_argument_type
-val rawwit_int_or_var : (int or_var,rlevel,'ta) abstract_argument_type
-val globwit_int_or_var : (int or_var,glevel,'ta) abstract_argument_type
-val wit_int_or_var : (int or_var,tlevel,'ta) abstract_argument_type
+val rawwit_int_or_var : (int or_var,rlevel) abstract_argument_type
+val globwit_int_or_var : (int or_var,glevel) abstract_argument_type
+val wit_int_or_var : (int or_var,tlevel) abstract_argument_type
-val rawwit_string : (string,rlevel,'ta) abstract_argument_type
-val globwit_string : (string,glevel,'ta) abstract_argument_type
-val wit_string : (string,tlevel,'ta) abstract_argument_type
+val rawwit_string : (string,rlevel) abstract_argument_type
+val globwit_string : (string,glevel) abstract_argument_type
+val wit_string : (string,tlevel) abstract_argument_type
-val rawwit_pre_ident : (string,rlevel,'ta) abstract_argument_type
-val globwit_pre_ident : (string,glevel,'ta) abstract_argument_type
-val wit_pre_ident : (string,tlevel,'ta) abstract_argument_type
+val rawwit_pre_ident : (string,rlevel) abstract_argument_type
+val globwit_pre_ident : (string,glevel) abstract_argument_type
+val wit_pre_ident : (string,tlevel) abstract_argument_type
-val rawwit_intro_pattern : (intro_pattern_expr,rlevel,'ta) abstract_argument_type
-val globwit_intro_pattern : (intro_pattern_expr,glevel,'ta) abstract_argument_type
-val wit_intro_pattern : (intro_pattern_expr,tlevel,'ta) abstract_argument_type
+val rawwit_intro_pattern : (intro_pattern_expr,rlevel) abstract_argument_type
+val globwit_intro_pattern : (intro_pattern_expr,glevel) abstract_argument_type
+val wit_intro_pattern : (intro_pattern_expr,tlevel) abstract_argument_type
-val rawwit_ident : (identifier,rlevel,'ta) abstract_argument_type
-val globwit_ident : (identifier,glevel,'ta) abstract_argument_type
-val wit_ident : (identifier,tlevel,'ta) abstract_argument_type
+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_var : (identifier located,rlevel,'ta) abstract_argument_type
-val globwit_var : (identifier located,glevel,'ta) abstract_argument_type
-val wit_var : (identifier,tlevel,'ta) 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
-val rawwit_ref : (reference,rlevel,'ta) abstract_argument_type
-val globwit_ref : (global_reference located or_var,glevel,'ta) abstract_argument_type
-val wit_ref : (global_reference,tlevel,'ta) abstract_argument_type
+val rawwit_ref : (reference,rlevel) abstract_argument_type
+val globwit_ref : (global_reference located or_var,glevel) abstract_argument_type
+val wit_ref : (global_reference,tlevel) abstract_argument_type
-val rawwit_quant_hyp : (quantified_hypothesis,rlevel,'ta) abstract_argument_type
-val globwit_quant_hyp : (quantified_hypothesis,glevel,'ta) abstract_argument_type
-val wit_quant_hyp : (quantified_hypothesis,tlevel,'ta) abstract_argument_type
+val rawwit_quant_hyp : (quantified_hypothesis,rlevel) abstract_argument_type
+val globwit_quant_hyp : (quantified_hypothesis,glevel) abstract_argument_type
+val wit_quant_hyp : (quantified_hypothesis,tlevel) abstract_argument_type
-val rawwit_sort : (rawsort,rlevel,'ta) abstract_argument_type
-val globwit_sort : (rawsort,glevel,'ta) abstract_argument_type
-val wit_sort : (sorts,tlevel,'ta) abstract_argument_type
+val rawwit_sort : (rawsort,rlevel) abstract_argument_type
+val globwit_sort : (rawsort,glevel) abstract_argument_type
+val wit_sort : (sorts,tlevel) abstract_argument_type
-val rawwit_constr : (constr_expr,rlevel,'ta) abstract_argument_type
-val globwit_constr : (rawconstr_and_expr,glevel,'ta) abstract_argument_type
-val wit_constr : (constr,tlevel,'ta) abstract_argument_type
+val rawwit_constr : (constr_expr,rlevel) abstract_argument_type
+val globwit_constr : (rawconstr_and_expr,glevel) abstract_argument_type
+val wit_constr : (constr,tlevel) abstract_argument_type
-val rawwit_constr_may_eval : ((constr_expr,reference) may_eval,rlevel,'ta) abstract_argument_type
-val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) may_eval,glevel,'ta) abstract_argument_type
-val wit_constr_may_eval : (constr,tlevel,'ta) abstract_argument_type
+val rawwit_constr_may_eval : ((constr_expr,reference or_by_notation) may_eval,rlevel) abstract_argument_type
+val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) may_eval,glevel) abstract_argument_type
+val wit_constr_may_eval : (constr,tlevel) abstract_argument_type
-val rawwit_open_constr_gen : bool -> (open_constr_expr,rlevel,'ta) abstract_argument_type
-val globwit_open_constr_gen : bool -> (open_rawconstr,glevel,'ta) abstract_argument_type
-val wit_open_constr_gen : bool -> (open_constr,tlevel,'ta) abstract_argument_type
+val rawwit_open_constr_gen : bool -> (open_constr_expr,rlevel) abstract_argument_type
+val globwit_open_constr_gen : bool -> (open_rawconstr,glevel) abstract_argument_type
+val wit_open_constr_gen : bool -> (open_constr,tlevel) abstract_argument_type
-val rawwit_open_constr : (open_constr_expr,rlevel,'ta) abstract_argument_type
-val globwit_open_constr : (open_rawconstr,glevel,'ta) abstract_argument_type
-val wit_open_constr : (open_constr,tlevel,'ta) abstract_argument_type
+val rawwit_open_constr : (open_constr_expr,rlevel) abstract_argument_type
+val globwit_open_constr : (open_rawconstr,glevel) abstract_argument_type
+val wit_open_constr : (open_constr,tlevel) abstract_argument_type
-val rawwit_casted_open_constr : (open_constr_expr,rlevel,'ta) abstract_argument_type
-val globwit_casted_open_constr : (open_rawconstr,glevel,'ta) abstract_argument_type
-val wit_casted_open_constr : (open_constr,tlevel,'ta) abstract_argument_type
+val rawwit_casted_open_constr : (open_constr_expr,rlevel) abstract_argument_type
+val globwit_casted_open_constr : (open_rawconstr,glevel) abstract_argument_type
+val wit_casted_open_constr : (open_constr,tlevel) abstract_argument_type
-val rawwit_constr_with_bindings : (constr_expr with_bindings,rlevel,'ta) abstract_argument_type
-val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,glevel,'ta) abstract_argument_type
-val wit_constr_with_bindings : (constr with_bindings,tlevel,'ta) abstract_argument_type
+val rawwit_constr_with_bindings : (constr_expr with_bindings,rlevel) abstract_argument_type
+val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,glevel) abstract_argument_type
+val wit_constr_with_bindings : (constr with_ebindings,tlevel) abstract_argument_type
-val rawwit_bindings : (constr_expr bindings,rlevel,'ta) abstract_argument_type
-val globwit_bindings : (rawconstr_and_expr bindings,glevel,'ta) abstract_argument_type
-val wit_bindings : (constr bindings,tlevel,'ta) abstract_argument_type
+val rawwit_bindings : (constr_expr bindings,rlevel) abstract_argument_type
+val globwit_bindings : (rawconstr_and_expr bindings,glevel) abstract_argument_type
+val wit_bindings : (open_constr bindings,tlevel) abstract_argument_type
-val rawwit_red_expr : ((constr_expr,reference) red_expr_gen,rlevel,'ta) abstract_argument_type
-val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) red_expr_gen,glevel,'ta) abstract_argument_type
-val wit_red_expr : ((constr,evaluable_global_reference) red_expr_gen,tlevel,'ta) abstract_argument_type
+val rawwit_red_expr : ((constr_expr,reference or_by_notation) red_expr_gen,rlevel) abstract_argument_type
+val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) red_expr_gen,glevel) abstract_argument_type
+val wit_red_expr : ((constr,evaluable_global_reference) red_expr_gen,tlevel) abstract_argument_type
val wit_list0 :
- ('a,'co,'ta) abstract_argument_type -> ('a list,'co,'ta) abstract_argument_type
+ ('a,'co) abstract_argument_type -> ('a list,'co) abstract_argument_type
val wit_list1 :
- ('a,'co,'ta) abstract_argument_type -> ('a list,'co,'ta) abstract_argument_type
+ ('a,'co) abstract_argument_type -> ('a list,'co) abstract_argument_type
val wit_opt :
- ('a,'co,'ta) abstract_argument_type -> ('a option,'co,'ta) abstract_argument_type
+ ('a,'co) abstract_argument_type -> ('a option,'co) abstract_argument_type
val wit_pair :
- ('a,'co,'ta) abstract_argument_type ->
- ('b,'co,'ta) abstract_argument_type ->
- ('a * 'b,'co,'ta) abstract_argument_type
+ ('a,'co) abstract_argument_type ->
+ ('b,'co) abstract_argument_type ->
+ ('a * 'b,'co) abstract_argument_type
(* ['a generic_argument] = (Sigma t:type. t[[constr/'a]]) *)
-type ('a,'b) generic_argument
+type 'a generic_argument
val fold_list0 :
- (('a,'b) generic_argument -> 'c -> 'c) -> ('a,'b) generic_argument -> 'c -> 'c
+ ('a generic_argument -> 'c -> 'c) -> 'a generic_argument -> 'c -> 'c
val fold_list1 :
- (('a,'b) generic_argument -> 'c -> 'c) -> ('a,'b) generic_argument -> 'c -> 'c
+ ('a generic_argument -> 'c -> 'c) -> 'a generic_argument -> 'c -> 'c
val fold_opt :
- (('a,'b) generic_argument -> 'c) -> 'c -> ('a,'b) generic_argument -> 'c
+ ('a generic_argument -> 'c) -> 'c -> 'a generic_argument -> 'c
val fold_pair :
- (('a,'b) generic_argument -> ('a,'b) generic_argument -> 'c) ->
- ('a,'b) generic_argument -> 'c
+ ('a generic_argument -> 'a generic_argument -> 'c) ->
+ 'a generic_argument -> 'c
(* [app_list0] fails if applied to an argument not of tag [List0 t]
for some [t]; it's the responsability of the caller to ensure it *)
-val app_list0 : (('a,'b) generic_argument -> ('c,'d) generic_argument) ->
-('a,'b) generic_argument -> ('c,'d) generic_argument
+val app_list0 : ('a generic_argument -> 'b generic_argument) ->
+'a generic_argument -> 'b generic_argument
-val app_list1 : (('a,'b) generic_argument -> ('c,'d) generic_argument) ->
-('a,'b) generic_argument -> ('c,'d) generic_argument
+val app_list1 : ('a generic_argument -> 'b generic_argument) ->
+'a generic_argument -> 'b generic_argument
-val app_opt : (('a,'b) generic_argument -> ('c,'d) generic_argument) ->
-('a,'b) generic_argument -> ('c,'d) generic_argument
+val app_opt : ('a generic_argument -> 'b generic_argument) ->
+'a generic_argument -> 'b generic_argument
val app_pair :
- (('a,'b) generic_argument -> ('c,'d) generic_argument) ->
- (('a,'b) generic_argument -> ('c,'d) generic_argument)
- -> ('a,'b) generic_argument -> ('c,'d) generic_argument
+ ('a generic_argument -> 'b generic_argument) ->
+ ('a generic_argument -> 'b generic_argument)
+ -> 'a generic_argument -> 'b generic_argument
-(* Manque l'ordre supérieur, on aimerait ('co,'ta) 'a; manque aussi le
- polymorphism, on aimerait que 'b et 'c restent polymorphes à l'appel
- de create *)
+(* create a new generic type of argument: force to associate
+ unique ML types at each of the three levels *)
val create_arg : string ->
- ('a,tlevel,'ta) abstract_argument_type
- * ('globa,glevel,'globta) abstract_argument_type
- * ('rawa,rlevel,'rawta) abstract_argument_type
+ ('a,tlevel) abstract_argument_type
+ * ('globa,glevel) abstract_argument_type
+ * ('rawa,rlevel) abstract_argument_type
val exists_argtype : string -> bool
@@ -254,15 +272,21 @@ type argument_type =
| PairArgType of argument_type * argument_type
| ExtraArgType of string
-val genarg_tag : ('a,'b) generic_argument -> argument_type
+val genarg_tag : 'a generic_argument -> argument_type
+
+val unquote : ('a,'co) abstract_argument_type -> argument_type
-val unquote : ('a,'co,'ta) abstract_argument_type -> argument_type
+val in_gen :
+ ('a,'co) abstract_argument_type -> 'a -> 'co generic_argument
+val out_gen :
+ ('a,'co) abstract_argument_type -> 'co generic_argument -> 'a
-(* We'd like
- [in_generic: !b:type, !a:argument_type -> (f a) -> b generic_argument]
+(* [in_generic] is used in combination with camlp4 [Gramext.action] magic
- with f a = b if a is Constr, f a = c if a is Tactic, otherwise f a = |a|
+ [in_generic: !l:type, !a:argument_type -> |a|_l -> 'l generic_argument]
+
+ where |a|_l is the interpretation of a at level l
[in_generic] is not typable; we replace the second argument by an absurd
type (with no introduction rule)
@@ -270,9 +294,4 @@ val unquote : ('a,'co,'ta) abstract_argument_type -> argument_type
type an_arg_of_this_type
val in_generic :
- argument_type -> an_arg_of_this_type -> ('a,'b) generic_argument
-
-val in_gen :
- ('a,'co,'ta) abstract_argument_type -> 'a -> ('co,'ta) generic_argument
-val out_gen :
- ('a,'co,'ta) abstract_argument_type -> ('co,'ta) generic_argument -> 'a
+ argument_type -> an_arg_of_this_type -> 'co generic_argument
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
new file mode 100644
index 00000000..d480ad39
--- /dev/null
+++ b/interp/implicit_quantifiers.ml
@@ -0,0 +1,285 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+
+(*i $Id: implicit_quantifiers.ml 10922 2008-05-12 12:47:17Z msozeau $ i*)
+
+(*i*)
+open Names
+open Decl_kinds
+open Term
+open Sign
+open Evd
+open Environ
+open Nametab
+open Mod_subst
+open Util
+open Rawterm
+open Topconstr
+open Libnames
+open Typeclasses
+open Typeclasses_errors
+open Pp
+(*i*)
+
+let ids_of_list l =
+ List.fold_right Idset.add l Idset.empty
+
+
+let locate_reference qid =
+ match Nametab.extended_locate qid with
+ | TrueGlobal ref -> true
+ | SyntacticDef kn -> true
+
+let is_global id =
+ try
+ locate_reference (make_short_qualid id)
+ with Not_found ->
+ false
+
+let is_freevar ids env x =
+ try
+ if Idset.mem x ids then false
+ else
+ try ignore(Environ.lookup_named x env) ; false
+ with _ -> not (is_global x)
+ with _ -> true
+
+(* Auxilliary functions for the inference of implicitly quantified variables. *)
+
+let free_vars_of_constr_expr c ?(bound=Idset.empty) l =
+ let found id bdvars l =
+ if List.mem id l then l
+ else if not (is_freevar bdvars (Global.env ()) id)
+ then l else id :: l
+ 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) ->
+ fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c
+ | c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c
+ in aux bound l c
+
+let ids_of_names l =
+ List.fold_left (fun acc x -> match snd x with Name na -> na :: acc | Anonymous -> acc) [] l
+
+let free_vars_of_binders ?(bound=Idset.empty) l (binders : local_binder list) =
+ let rec aux bdvars l c = match c with
+ ((LocalRawAssum (n, _, c)) :: tl) ->
+ let bound = ids_of_names n in
+ let l' = free_vars_of_constr_expr c ~bound:bdvars l in
+ aux (Idset.union (ids_of_list bound) bdvars) l' tl
+
+ | ((LocalRawDef (n, c)) :: tl) ->
+ let bound = match snd n with Anonymous -> [] | Name n -> [n] in
+ let l' = free_vars_of_constr_expr c ~bound:bdvars l in
+ aux (Idset.union (ids_of_list bound) bdvars) l' tl
+
+ | [] -> bdvars, l
+ in aux bound l binders
+
+let 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 compute_constrs_freevars env constrs =
+ let ids =
+ List.rev (List.fold_left
+ (fun acc x -> free_vars_of_constr_expr x acc)
+ [] constrs)
+ in freevars_of_ids env ids
+
+(* let compute_context_freevars env ctx = *)
+(* let ids = *)
+(* List.rev *)
+(* (List.fold_left *)
+(* (fun acc (_,i,x) -> free_vars_of_constr_expr x acc) *)
+(* [] constrs) *)
+(* in freevars_of_ids ids *)
+
+let compute_constrs_freevars_binders env constrs =
+ let elts = compute_constrs_freevars env constrs in
+ List.map (fun id -> (dummy_loc, id), CHole (dummy_loc, None)) elts
+
+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 rec name_rec id = *)
+(* if Idset.mem id avoid then name_rec (Nameops.lift_ident id) else id in *)
+(* name_rec id *)
+
+let ids_of_named_context_avoiding avoid l =
+ List.fold_left (fun (ids, avoid) id ->
+ let id' = next_ident_away_from id avoid in id' :: ids, Idset.add id' avoid)
+ ([], avoid) (Termops.ids_of_named_context l)
+
+let combine_params avoid fn applied needed =
+ let named, applied =
+ List.partition
+ (function
+ (t, Some (loc, ExplByName id)) ->
+ if not (List.exists (fun (_, (id', _, _)) -> id = id') needed) then
+ user_err_loc (loc,"",str "Wrong argument name: " ++ Nameops.pr_id id);
+ true
+ | _ -> false) applied
+ in
+ let named = List.map
+ (fun x -> match x with (t, Some (loc, ExplByName id)) -> id, t | _ -> assert false)
+ named
+ in
+ let rec aux ids avoid app need =
+ match app, need with
+ [], [] -> List.rev ids, avoid
+
+ | app, (_, (id, _, _)) :: need when List.mem_assoc id named ->
+ aux (List.assoc id named :: ids) avoid app need
+
+ | (x, None) :: app, (None, (id, _, _)) :: need ->
+ aux (x :: ids) avoid app need
+
+ | _, (Some cl, (id, _, _) as d) :: need ->
+ let t', avoid' = fn avoid d in
+ aux (t' :: ids) avoid' app need
+
+ | x :: app, (None, _) :: need -> aux (fst x :: ids) avoid app need
+
+ | [], (None, _ as decl) :: need ->
+ let t', avoid' = fn avoid decl in
+ aux (t' :: ids) avoid' app need
+
+ | _ :: _, [] -> failwith "combine_params: overly applied typeclass"
+ in aux [] avoid applied needed
+
+let combine_params_freevar avoid applied needed =
+ combine_params avoid
+ (fun avoid (_, (id, _, _)) ->
+ let id' = next_ident_away_from 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 destClassApp cl =
+ match cl with
+ | CApp (loc, (None,CRef ref), l) -> loc, ref, List.map fst l
+ | CRef ref -> loc_of_reference ref, ref, []
+ | _ -> raise Not_found
+
+let destClassAppExpl cl =
+ match cl with
+ | CApp (loc, (None,CRef ref), l) -> loc, ref, l
+ | 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 constr_expr_of_constraint (kind, id) l =
+ match kind with
+ | Implicit -> CAppExpl (fst id, (None, Ident id), l)
+ | Explicit -> CApp (fst id, (None, CRef (Ident id)),
+ List.map (fun x -> x, None) l)
+
+(* | CApp of loc * (proj_flag * constr_expr) * *)
+(* (constr_expr * explicitation located option) list *)
+
+
+let constrs_of_context l =
+ List.map (fun (_, id, l) -> constr_expr_of_constraint id l) 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 generalize_class_binders env l =
+ let fv_ctx, cstrs = resolve_class_binders env l in
+ List.map (fun ((loc, id), t) -> LocalRawAssum ([loc, Name id], Default Implicit, t)) fv_ctx,
+ List.map (fun (iid, bk, c) -> LocalRawAssum ([iid], Default Implicit, c))
+ cstrs
+
+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 ctx_of_class_binders env l =
+ let (x, y) = generalize_class_binders env l in x @ y
+
+let implicits_of_binders l =
+ let rec aux i l =
+ match l with
+ [] -> []
+ | hd :: tl ->
+ let res, reslen =
+ match hd with
+ LocalRawAssum (nal, Default Implicit, t) ->
+ list_map_i (fun i (_,id) ->
+ let name =
+ match id with
+ Name id -> Some id
+ | Anonymous -> None
+ in ExplByPos (i, name), (true, true))
+ i nal, List.length nal
+ | LocalRawAssum (nal, _, _) -> [], List.length nal
+ | LocalRawDef _ -> [], 1
+ in res @ (aux (i + reslen) tl)
+ in aux 1 l
+
+let implicits_of_rawterm l =
+ let rec aux i c =
+ match c with
+ RProd (loc, na, bk, t, b) | RLambda (loc, na, bk, t, b) ->
+ let rest = aux (succ i) b in
+ if bk = Implicit then
+ let name =
+ match na with
+ Name id -> Some id
+ | Anonymous -> None
+ in
+ (ExplByPos (i, name), (true, true)) :: rest
+ else rest
+ | RLetIn (loc, na, t, b) -> aux i b
+ | _ -> []
+ in aux 1 l
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
new file mode 100644
index 00000000..ff81dc10
--- /dev/null
+++ b/interp/implicit_quantifiers.mli
@@ -0,0 +1,68 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+
+(*i $Id: implicit_quantifiers.mli 10739 2008-04-01 14:45:20Z herbelin $ i*)
+
+(*i*)
+open Names
+open Decl_kinds
+open Term
+open Sign
+open Evd
+open Environ
+open Nametab
+open Mod_subst
+open Rawterm
+open Topconstr
+open Util
+open Libnames
+open Typeclasses
+(*i*)
+
+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
+
+val binder_list_of_ids : identifier list -> local_binder list
+
+val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier
+
+val free_vars_of_binders :
+ ?bound:Idset.t -> Names.identifier list -> local_binder list -> Idset.t * Names.identifier list
+
+val compute_constrs_freevars : Idset.t -> constr_expr list -> identifier list
+val compute_constrs_freevars_binders : Idset.t -> constr_expr list -> (identifier located * constr_expr) list
+val resolve_class_binders : Idset.t -> typeclass_context ->
+ (identifier located * constr_expr) list * typeclass_context
+
+val full_class_binders : Idset.t -> typeclass_context -> typeclass_context
+
+val generalize_class_binders_raw : Idset.t -> typeclass_context ->
+ (name located * binding_kind * constr_expr) list * (name located * binding_kind * constr_expr) list
+
+val ctx_of_class_binders : Idset.t -> typeclass_context -> local_binder list
+
+val implicits_of_binders : local_binder list -> (Topconstr.explicitation * (bool * bool)) list
+
+val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool)) list
+
+val combine_params : Names.Idset.t ->
+ (Names.Idset.t -> (global_reference * bool) option * (Names.identifier * Term.constr option * Term.types) ->
+ Topconstr.constr_expr * Names.Idset.t) ->
+ (Topconstr.constr_expr * Topconstr.explicitation located option) list ->
+ ((global_reference * bool) option * Term.named_declaration) list ->
+ Topconstr.constr_expr list * Names.Idset.t
+
+
+val ids_of_named_context_avoiding : Names.Idset.t ->
+ Sign.named_context -> Names.Idset.elt list * Names.Idset.t
+
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 71bd431d..4cc30b26 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: modintern.ml 6582 2005-01-13 14:28:56Z sacerdot $ *)
+(* $Id: modintern.ml 11127 2008-06-14 15:39:46Z herbelin $ *)
open Pp
open Util
@@ -60,20 +60,50 @@ 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.
*)
-
let lookup_module (loc,qid) =
try
- Nametab.locate_module qid
+ let mp = Nametab.locate_module qid in
+ 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
- Nametab.locate_modtype qid
+ let mp = Nametab.locate_modtype qid in
+ dump_modref loc mp "mod"; mp
with
| Not_found ->
Modops.error_not_a_modtype_loc loc (string_of_qualid qid)
@@ -84,20 +114,23 @@ let transl_with_decl env = function
| CWith_Definition ((_,fqid),c) ->
With_Definition (fqid,interp_constr Evd.empty env c)
-let rec interp_modtype env = function
- | CMTEident qid ->
- MTEident (lookup_modtype qid)
- | CMTEwith (mty,decl) ->
- let mty = interp_modtype env mty in
- let decl = transl_with_decl env decl in
- MTEwith(mty,decl)
-
-
let rec interp_modexpr env = function
| CMEident qid ->
- MEident (lookup_module qid)
+ MSEident (lookup_module qid)
| CMEapply (me1,me2) ->
let me1 = interp_modexpr env me1 in
let me2 = interp_modexpr env me2 in
- MEapply(me1,me2)
+ MSEapply(me1,me2)
+
+let rec interp_modtype env = function
+ | CMTEident qid ->
+ MSEident (lookup_modtype qid)
+ | CMTEapply (mty1,me) ->
+ let mty' = interp_modtype env mty1 in
+ let me' = interp_modexpr env me in
+ MSEapply(mty',me')
+ | CMTEwith (mty,decl) ->
+ let mty = interp_modtype env mty in
+ let decl = transl_with_decl env decl in
+ MSEwith(mty,decl)
diff --git a/interp/modintern.mli b/interp/modintern.mli
index 844450ac..c92756dc 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -6,19 +6,26 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: modintern.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: modintern.mli 11065 2008-06-06 22:39:43Z msozeau $ i*)
(*i*)
open Declarations
open Environ
open Entries
+open Util
+open Libnames
+open Names
open Topconstr
(*i*)
(* Module expressions and module types are interpreted relatively to
eventual functor or funsig arguments. *)
-val interp_modtype : env -> module_type_ast -> module_type_entry
+val interp_modtype : env -> module_type_ast -> module_struct_entry
-val interp_modexpr : env -> module_ast -> module_expr
+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 08c6f31f..98a199ad 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: notation.ml 9694 2007-03-09 18:09:53Z herbelin $ *)
+(* $Id: notation.ml 10893 2008-05-07 09:20:43Z herbelin $ *)
(*i*)
open Util
@@ -73,7 +73,7 @@ let init_scope_map () =
let declare_scope scope =
try let _ = Gmap.find scope !scope_map in ()
with Not_found ->
-(* Options.if_verbose message ("Creating scope "^scope);*)
+(* Flags.if_verbose message ("Creating scope "^scope);*)
scope_map := Gmap.add scope empty_scope !scope_map
let find_scope scope =
@@ -133,7 +133,7 @@ let push_scopes = List.fold_right push_scope
type local_scopes = tmp_scope_name option * scope_name list
let make_current_scopes (tmp_scope,scopes) =
- option_fold_right push_scope tmp_scope (push_scopes scopes !scope_stack)
+ Option.fold_right push_scope tmp_scope (push_scopes scopes !scope_stack)
(**********************************************************************)
(* Delimiters *)
@@ -142,16 +142,16 @@ let delimiters_map = ref Gmap.empty
let declare_delimiters scope key =
let sc = find_scope scope in
- if sc.delimiters <> None && Options.is_verbose () then begin
- let old = out_some sc.delimiters in
- Options.if_verbose
+ if sc.delimiters <> None && Flags.is_verbose () then begin
+ let old = Option.get sc.delimiters in
+ Flags.if_verbose
warning ("Overwritting previous delimiting key "^old^" in scope "^scope)
end;
let sc = { sc with delimiters = Some key } in
scope_map := Gmap.add scope sc !scope_map;
if Gmap.mem key !delimiters_map then begin
let oldsc = Gmap.find key !delimiters_map in
- Options.if_verbose warning ("Hiding binding of key "^key^" to "^oldsc)
+ Flags.if_verbose warning ("Hiding binding of key "^key^" to "^oldsc)
end;
delimiters_map := Gmap.add key scope !delimiters_map
@@ -187,10 +187,10 @@ let cases_pattern_key = function
| PatCstr (_,ref,_,_) -> RefKey (ConstructRef ref)
| _ -> Oth
-let aconstr_key = function
+let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *)
| AApp (ARef ref,args) -> RefKey ref, Some (List.length args)
| AList (_,_,AApp (ARef ref,args),_,_) -> RefKey ref, Some (List.length args)
- | ARef ref -> RefKey ref, Some 0
+ | ARef ref -> RefKey ref, None
| _ -> Oth, None
let pattern_key = function
@@ -239,12 +239,12 @@ let delay dir int loc x = (dir, (fun () -> int loc x))
let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) =
declare_prim_token_interpreter sc
(fun cont loc -> function Numeral n-> delay dir interp loc n | p -> cont loc p)
- (patl, (fun r -> option_map mkNumeral (uninterp r)), inpat)
+ (patl, (fun r -> Option.map mkNumeral (uninterp r)), inpat)
let declare_string_interpreter sc dir interp (patl,uninterp,inpat) =
declare_prim_token_interpreter sc
(fun cont loc -> function String s -> delay dir interp loc s | p -> cont loc p)
- (patl, (fun r -> option_map mkString (uninterp r)), inpat)
+ (patl, (fun r -> Option.map mkString (uninterp r)), inpat)
let check_required_module loc sc (sp,d) =
try let _ = Nametab.absolute_reference sp in ()
@@ -288,7 +288,7 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
let declare_notation_level ntn level =
if Gmap.mem ntn !notation_level_map then
- error ("Notation "^ntn^" is already assigned a level");
+ anomaly ("Notation "^ntn^" is already assigned a level");
notation_level_map := Gmap.add ntn level !notation_level_map
let level_of_notation ntn =
@@ -299,8 +299,8 @@ let level_of_notation ntn =
let declare_notation_interpretation ntn scopt pat df =
let scope = match scopt with Some s -> s | None -> default_scope in
let sc = find_scope scope in
- if Gmap.mem ntn sc.notations && Options.is_verbose () then
- msg_warning (str ("Notation "^ntn^" was already used"^
+ if Gmap.mem ntn sc.notations then
+ Flags.if_warn msg_warning (str ("Notation "^ntn^" was already used"^
(if scopt = None then "" else " in scope "^scope)));
let sc = { sc with notations = Gmap.add ntn (pat,df) sc.notations } in
scope_map := Gmap.add scope sc !scope_map;
@@ -393,16 +393,10 @@ let uninterp_prim_token_cases_pattern c =
| Some n -> (na,sc,n)
with Not_found -> raise No_match
-let availability_of_prim_token printer_scope local_scopes t =
- let f scope =
- try
- (* raise Not_found if no primitive interpreter for scope *)
- let interp = Hashtbl.find prim_token_interpreter_tab scope in
- (* raise Not_found if no primitive interpreter for this token in scope *)
- let _ = interp dummy_loc t in true
- with Not_found -> false in
+let availability_of_prim_token printer_scope local_scopes =
+ let f scope = Hashtbl.mem prim_token_interpreter_tab scope in
let scopes = make_current_scopes local_scopes in
- option_map snd (find_without_delimiters f (Some printer_scope,None) scopes)
+ Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes)
(* Miscellaneous *)
@@ -414,6 +408,8 @@ let exists_notation_in_scope scopt ntn r =
r' = r
with Not_found -> false
+let isAVar = function AVar _ -> true | _ -> false
+
(**********************************************************************)
(* Mapping classes to scopes *)
@@ -458,7 +454,7 @@ type arguments_scope_discharge_request =
| ArgsScopeNoDischarge
let load_arguments_scope _ (_,(_,r,scl)) =
- List.iter (option_iter check_scope) scl;
+ List.iter (Option.iter check_scope) scl;
arguments_scope := Refmap.add r scl !arguments_scope
let cache_arguments_scope o =
@@ -471,7 +467,7 @@ let discharge_arguments_scope (_,(req,r,l)) =
if req = ArgsScopeNoDischarge then None
else Some (req,pop_global_reference r,l)
-let rebuild_arguments_scope (req,r,l) =
+let rebuild_arguments_scope (_,(req,r,l)) =
match req with
| ArgsScopeNoDischarge -> assert false
| ArgsScopeAuto ->
@@ -608,21 +604,51 @@ let factorize_entries = function
let is_ident s = (* Poor analysis *)
String.length s <> 0 & is_letter s.[0]
-let browse_notation ntn map =
+let browse_notation strict ntn map =
let find =
if String.contains ntn ' ' then (=) ntn
- else fun ntn' -> List.mem (Terminal ntn) (decompose_notation_key ntn') in
+ else fun ntn' ->
+ let toks = decompose_notation_key ntn' in
+ let trms = List.filter (function Terminal _ -> true | _ -> false) toks in
+ if strict then [Terminal ntn] = trms else List.mem (Terminal ntn) trms in
let l =
Gmap.fold
(fun scope_name sc ->
Gmap.fold (fun ntn ((_,r),df) l ->
if find ntn then (ntn,(scope_name,r,df))::l else l) sc.notations)
map [] in
- let l = List.sort (fun x y -> Pervasives.compare (fst x) (fst y)) l in
- factorize_entries l
+ List.sort (fun x y -> Pervasives.compare (fst x) (fst y)) l
+
+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 ->
+ Some (ntn,sc,ref)
+ | _ -> None
+
+let error_ambiguous_notation loc _ntn =
+ user_err_loc (loc,"",str "Ambiguous notation")
+
+let error_notation_not_reference loc ntn =
+ user_err_loc (loc,"",
+ 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 refs = List.map (global_reference_of_notation test) ntns in
+ match Option.List.flatten refs with
+ | [_,_,ref] -> ref
+ | [] -> error_notation_not_reference loc ntn
+ | refs ->
+ let f (ntn,sc,ref) = find_default ntn !scope_stack = Some sc in
+ match List.filter f refs with
+ | [_,_,ref] -> ref
+ | [] -> error_notation_not_reference loc ntn
+ | _ -> error_ambiguous_notation loc ntn
let locate_notation prraw ntn =
- let ntns = browse_notation ntn !scope_map in
+ let ntns = factorize_entries (browse_notation false ntn !scope_map) in
if ntns = [] then
str "Unknown notation"
else
diff --git a/interp/notation.mli b/interp/notation.mli
index f5c8bdac..a393aaed 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 9694 2007-03-09 18:09:53Z herbelin $ i*)
+(*i $Id: notation.mli 9804 2007-04-28 13:56:03Z herbelin $ i*)
(*i*)
open Util
@@ -93,7 +93,7 @@ val uninterp_prim_token_cases_pattern :
cases_pattern -> name * scope_name * prim_token
val availability_of_prim_token :
- scope_name -> local_scopes -> prim_token -> delimiters option option
+ scope_name -> local_scopes -> delimiters option option
(*s Declare and interpret back and forth a notation *)
@@ -130,6 +130,9 @@ 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
+
(* Checks for already existing notations *)
val exists_notation_in_scope : scope_name option -> notation ->
interpretation -> bool
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 3ec0182b..f7496832 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: reserve.ml 9976 2007-07-12 11:58:30Z msozeau $ i*)
+(*i $Id: reserve.ml 10727 2008-03-28 20:22:43Z msozeau $ i*)
(* Reserved names *)
@@ -54,22 +54,22 @@ open Rawterm
let rec unloc = function
| RVar (_,id) -> RVar (dummy_loc,id)
| RApp (_,g,args) -> RApp (dummy_loc,unloc g, List.map unloc args)
- | RLambda (_,na,ty,c) -> RLambda (dummy_loc,na,unloc ty,unloc c)
- | RProd (_,na,ty,c) -> RProd (dummy_loc,na,unloc ty,unloc c)
+ | RLambda (_,na,bk,ty,c) -> RLambda (dummy_loc,na,bk,unloc ty,unloc c)
+ | RProd (_,na,bk,ty,c) -> RProd (dummy_loc,na,bk,unloc ty,unloc c)
| RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c)
- | RCases (_,rtntypopt,tml,pl) ->
- RCases (dummy_loc,
- (option_map unloc rtntypopt),
+ | RCases (_,sty,rtntypopt,tml,pl) ->
+ RCases (dummy_loc,sty,
+ (Option.map unloc rtntypopt),
List.map (fun (tm,x) -> (unloc tm,x)) tml,
List.map (fun (_,idl,p,c) -> (dummy_loc,idl,p,unloc c)) pl)
| RLetTuple (_,nal,(na,po),b,c) ->
- RLetTuple (dummy_loc,nal,(na,option_map unloc po),unloc b,unloc c)
+ RLetTuple (dummy_loc,nal,(na,Option.map unloc po),unloc b,unloc c)
| RIf (_,c,(na,po),b1,b2) ->
- RIf (dummy_loc,unloc c,(na,option_map unloc po),unloc b1,unloc b2)
+ RIf (dummy_loc,unloc c,(na,Option.map unloc po),unloc b1,unloc b2)
| RRec (_,fk,idl,bl,tyl,bv) ->
RRec (dummy_loc,fk,idl,
Array.map (List.map
- (fun (na,obd,ty) -> (na,option_map unloc obd, unloc ty)))
+ (fun (na,k,obd,ty) -> (na,k,Option.map unloc obd, unloc ty)))
bl,
Array.map unloc tyl,
Array.map unloc bv)
@@ -85,7 +85,7 @@ let rec unloc = function
let anonymize_if_reserved na t = match na with
| Name id as na ->
(try
- if unloc t = find_reserved_type id
+ if not !Flags.raw_print & unloc t = find_reserved_type id
then RHole (dummy_loc,Evd.BinderType na)
else t
with Not_found -> t)
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 3389cd8a..884dea48 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 7779 2006-01-03 20:33:47Z herbelin $ *)
+(* $Id: syntax_def.ml 10730 2008-03-30 21:42:58Z herbelin $ *)
open Util
open Pp
@@ -19,7 +19,7 @@ open Nameops
(* Syntactic definitions. *)
-let syntax_table = ref (KNmap.empty : aconstr KNmap.t)
+let syntax_table = ref (KNmap.empty : interpretation KNmap.t)
let _ = Summary.declare_summary
"SYNTAXCONSTANT"
@@ -32,28 +32,28 @@ let _ = Summary.declare_summary
let add_syntax_constant kn c =
syntax_table := KNmap.add kn c !syntax_table
-let load_syntax_constant i ((sp,kn),(local,c,onlyparse)) =
+let load_syntax_constant i ((sp,kn),(local,pat,onlyparse)) =
if Nametab.exists_cci sp then
errorlabstrm "cache_syntax_constant"
(pr_id (basename sp) ++ str " already exists");
- add_syntax_constant kn c;
+ add_syntax_constant kn pat;
Nametab.push_syntactic_definition (Nametab.Until i) sp kn;
if not onlyparse then
(* Declare it to be used as long name *)
- Notation.declare_uninterpretation (Notation.SynDefRule kn) ([],c)
+ Notation.declare_uninterpretation (Notation.SynDefRule kn) pat
-let open_syntax_constant i ((sp,kn),(_,c,onlyparse)) =
+let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
Nametab.push_syntactic_definition (Nametab.Exactly i) sp kn;
if not onlyparse then
(* Redeclare it to be used as (short) name in case an other (distfix)
notation was declared inbetween *)
- Notation.declare_uninterpretation (Notation.SynDefRule kn) ([],c)
+ Notation.declare_uninterpretation (Notation.SynDefRule kn) pat
let cache_syntax_constant d =
load_syntax_constant 1 d
-let subst_syntax_constant ((sp,kn),subst,(local,c,onlyparse)) =
- (local,subst_aconstr subst [] c,onlyparse)
+let subst_syntax_constant ((sp,kn),subst,(local,pat,onlyparse)) =
+ (local,subst_interpretation subst pat,onlyparse)
let classify_syntax_constant (_,(local,_,_ as o)) =
if local then Dispose else Substitute o
@@ -70,23 +70,30 @@ let (in_syntax_constant, out_syntax_constant) =
classify_function = classify_syntax_constant;
export_function = export_syntax_constant }
-let declare_syntactic_definition local id onlyparse c =
- let _ = add_leaf id (in_syntax_constant (local,c,onlyparse)) in ()
-
-let rec set_loc loc _ a =
- rawconstr_of_aconstr_with_binders loc (fun id e -> (id,e)) (set_loc loc) () a
+let declare_syntactic_definition local id onlyparse pat =
+ let _ = add_leaf id (in_syntax_constant (local,pat,onlyparse)) in ()
let search_syntactic_definition loc kn =
- set_loc loc () (KNmap.find kn !syntax_table)
-
-exception BoundToASyntacticDefThatIsNotARef
+ KNmap.find kn !syntax_table
-let locate_global qid =
+let locate_global_with_alias (loc,qid) =
match Nametab.extended_locate qid with
| TrueGlobal ref -> ref
| SyntacticDef kn ->
match search_syntactic_definition dummy_loc kn with
- | Rawterm.RRef (_,ref) -> ref
+ | [],ARef ref -> ref
| _ ->
- errorlabstrm "" (pr_qualid qid ++
+ user_err_loc (loc,"",pr_qualid qid ++
str " is bound to a notation that does not denote a reference")
+
+let inductive_of_reference_with_alias r =
+ match locate_global_with_alias (qualid_of_reference r) with
+ | IndRef ind -> ind
+ | ref ->
+ user_err_loc (loc_of_reference r,"global_inductive",
+ pr_reference r ++ spc () ++ str "is not an inductive type")
+
+let global_with_alias r =
+ let (loc,qid as lqid) = qualid_of_reference r in
+ try locate_global_with_alias lqid
+ with Not_found -> Nametab.error_global_not_found_loc loc qid
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index ac7318b5..a063caf0 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -6,27 +6,33 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: syntax_def.mli 7051 2005-05-20 15:45:51Z herbelin $ i*)
+(*i $Id: syntax_def.mli 10730 2008-03-30 21:42:58Z herbelin $ i*)
(*i*)
open Util
open Names
open Topconstr
open Rawterm
+open Libnames
(*i*)
(* Syntactic definitions. *)
-val declare_syntactic_definition : bool -> identifier -> bool -> aconstr
+val declare_syntactic_definition : bool -> identifier -> bool -> interpretation
-> unit
-val search_syntactic_definition : loc -> kernel_name -> rawconstr
+val search_syntactic_definition : loc -> kernel_name -> interpretation
+(* [locate_global_with_alias] locates global reference possibly following
+ a notation if this notation has a role of aliasing; raise Not_found
+ if not bound in the global env; raise an error if bound to a
+ syntactic def that does not denote a reference *)
-(* [locate_global] locates global reference possibly following a chain of
- syntactic aliases; raise Not_found if not bound in the global env;
- raise an error if bound to a syntactic def that does not denote a
- reference *)
+val locate_global_with_alias : qualid located -> global_reference
-val locate_global : Libnames.qualid -> Libnames.global_reference
+(* Locate a reference taking into account possible "alias" notations *)
+val global_with_alias : reference -> global_reference
+
+(* The same for inductive types *)
+val inductive_of_reference_with_alias : reference -> inductive
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index af147866..b858eecb 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: topconstr.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
+(* $Id: topconstr.ml 11024 2008-05-30 12:41:39Z msozeau $ *)
(*i*)
open Pp
@@ -37,11 +37,14 @@ type aconstr =
| ALambda of name * aconstr * aconstr
| AProd of name * aconstr * aconstr
| ALetIn of name * aconstr * aconstr
- | ACases of aconstr option *
+ | ACases of case_style * aconstr option *
(aconstr * (name * (inductive * int * name list) option)) list *
(cases_pattern list * aconstr) list
| ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
| AIf of aconstr * (name * aconstr option) * aconstr * aconstr
+ | ARec of fix_kind * identifier array *
+ (name * aconstr option * aconstr) list array * aconstr array *
+ aconstr array
| ASort of rawsort
| AHole of Evd.hole_kind
| APatVar of patvar
@@ -74,12 +77,12 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
let outerl = (ldots_var,inner)::(if swap then [x,RVar(loc,y)] else []) in
subst_rawvars outerl it
| ALambda (na,ty,c) ->
- let e,na = name_fold_map g e na in RLambda (loc,na,f e ty,f e c)
+ let e,na = name_fold_map g e na in RLambda (loc,na,Explicit,f e ty,f e c)
| AProd (na,ty,c) ->
- let e,na = name_fold_map g e na in RProd (loc,na,f e ty,f e c)
+ let e,na = name_fold_map g e na in RProd (loc,na,Explicit,f e ty,f e c)
| ALetIn (na,b,c) ->
let e,na = name_fold_map g e na in RLetIn (loc,na,f e b,f e c)
- | ACases (rtntypopt,tml,eqnl) ->
+ | ACases (sty,rtntypopt,tml,eqnl) ->
let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
let e',t' = match t with
| None -> e',None
@@ -94,14 +97,20 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
let ((idl,e),patl) =
list_fold_map (cases_pattern_fold_map loc fold) ([],e) patl in
(loc,idl,patl,f e rhs)) eqnl in
- RCases (loc,option_map (f e') rtntypopt,tml',eqnl')
+ RCases (loc,sty,Option.map (f e') rtntypopt,tml',eqnl')
| ALetTuple (nal,(na,po),b,c) ->
let e,nal = list_fold_map (name_fold_map g) e nal in
let e,na = name_fold_map g e na in
- RLetTuple (loc,nal,(na,option_map (f e) po),f e b,f e c)
+ RLetTuple (loc,nal,(na,Option.map (f e) po),f e b,f e c)
| AIf (c,(na,po),b1,b2) ->
let e,na = name_fold_map g e na in
- RIf (loc,f e c,(na,option_map (f e) po),f e b1,f e b2)
+ RIf (loc,f e c,(na,Option.map (f e) po),f e b1,f e b2)
+ | ARec (fk,idl,dll,tl,bl) ->
+ let e,idl = array_fold_map g e idl in
+ let e,dll = array_fold_map (list_fold_map (fun e (na,oc,b) ->
+ let e,na = name_fold_map g e na in
+ (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
+ RRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e) bl)
| ACast (c,k) -> RCast (loc,f e c,
match k with
| CastConv (k,t) -> CastConv (k,f e t)
@@ -131,9 +140,9 @@ let compare_rawconstr f t1 t2 = match t1,t2 with
| RRef (_,r1), RRef (_,r2) -> r1 = r2
| RVar (_,v1), RVar (_,v2) -> v1 = v2
| RApp (_,f1,l1), RApp (_,f2,l2) -> f f1 f2 & List.for_all2 f l1 l2
- | RLambda (_,na1,ty1,c1), RLambda (_,na2,ty2,c2) when na1 = na2 ->
+ | RLambda (_,na1,bk1,ty1,c1), RLambda (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 ->
f ty1 ty2 & f c1 c2
- | RProd (_,na1,ty1,c1), RProd (_,na2,ty2,c2) when na1 = na2 ->
+ | RProd (_,na1,bk1,ty1,c1), RProd (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 ->
f ty1 ty2 & f c1 c2
| RHole _, RHole _ -> true
| RSort (_,s1), RSort (_,s2) -> s1 = s2
@@ -180,25 +189,32 @@ let aconstr_and_vars_of_rawconstr a =
found := ldots_var :: !found; assert lassoc;
AList (x,y,AApp (AVar ldots_var,[AVar x]),aux t,lassoc)
| RApp (_,g,args) -> AApp (aux g, List.map aux args)
- | RLambda (_,na,ty,c) -> add_name found na; ALambda (na,aux ty,aux c)
- | RProd (_,na,ty,c) -> add_name found na; AProd (na,aux ty,aux c)
+ | RLambda (_,na,bk,ty,c) -> add_name found na; ALambda (na,aux ty,aux c)
+ | RProd (_,na,bk,ty,c) -> add_name found na; AProd (na,aux ty,aux c)
| RLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c)
- | RCases (_,rtntypopt,tml,eqnl) ->
+ | RCases (_,sty,rtntypopt,tml,eqnl) ->
let f (_,idl,pat,rhs) = found := idl@(!found); (pat,aux rhs) in
- ACases (option_map aux rtntypopt,
+ ACases (sty,Option.map aux rtntypopt,
List.map (fun (tm,(na,x)) ->
add_name found na;
- option_iter
+ Option.iter
(fun (_,_,_,nl) -> List.iter (add_name found) nl) x;
- (aux tm,(na,option_map (fun (_,ind,n,nal) -> (ind,n,nal)) x))) tml,
+ (aux tm,(na,Option.map (fun (_,ind,n,nal) -> (ind,n,nal)) x))) tml,
List.map f eqnl)
| RLetTuple (loc,nal,(na,po),b,c) ->
add_name found na;
List.iter (add_name found) nal;
- ALetTuple (nal,(na,option_map aux po),aux b,aux c)
+ ALetTuple (nal,(na,Option.map aux po),aux b,aux c)
| RIf (loc,c,(na,po),b1,b2) ->
add_name found na;
- AIf (aux c,(na,option_map aux po),aux b1,aux b2)
+ AIf (aux c,(na,Option.map aux po),aux b1,aux b2)
+ | RRec (_,fk,idl,dll,tl,bl) ->
+ Array.iter (fun id -> found := id::!found) idl;
+ let dll = Array.map (List.map (fun (na,bk,oc,b) ->
+ if bk <> Explicit then
+ error "Binders marked as implicit not allowed in notations";
+ add_name found na; (na,Option.map aux oc,aux b))) dll in
+ ARec (fk,idl,dll,Array.map aux tl,Array.map aux bl)
| RCast (_,c,k) -> ACast (aux c,
match k with CastConv (k,t) -> CastConv (k,aux t)
| CastCoerce -> CastCoerce)
@@ -206,9 +222,8 @@ let aconstr_and_vars_of_rawconstr a =
| RHole (_,w) -> AHole w
| RRef (_,r) -> ARef r
| RPatVar (_,(_,n)) -> APatVar n
- | RDynamic _ | RRec _ | REvar _ ->
- error "Fixpoints, cofixpoints, existential variables and pattern-matching not \
-allowed in abbreviatable expressions"
+ | RDynamic _ | REvar _ ->
+ error "Existential variables not allowed in notations"
(* Recognizing recursive notations *)
and terminator_of_pat f1 ll1 lr1 = function
@@ -304,12 +319,12 @@ let rec subst_aconstr subst bound raw =
if r1' == r1 && r2' == r2 then raw else
ALetIn (n,r1',r2')
- | ACases (rtntypopt,rl,branches) ->
- let rtntypopt' = option_smartmap (subst_aconstr subst bound) rtntypopt
+ | ACases (sty,rtntypopt,rl,branches) ->
+ let rtntypopt' = Option.smartmap (subst_aconstr subst bound) rtntypopt
and rl' = list_smartmap
(fun (a,(n,signopt) as x) ->
let a' = subst_aconstr subst bound a in
- let signopt' = option_map (fun ((indkn,i),n,nal as z) ->
+ let signopt' = Option.map (fun ((indkn,i),n,nal as z) ->
let indkn' = subst_kn subst indkn in
if indkn == indkn' then z else ((indkn',i),n,nal)) signopt in
if a' == a && signopt' == signopt then x else (a',(n,signopt')))
@@ -324,23 +339,34 @@ let rec subst_aconstr subst bound raw =
in
if rtntypopt' == rtntypopt && rtntypopt == rtntypopt' &
rl' == rl && branches' == branches then raw else
- ACases (rtntypopt',rl',branches')
+ ACases (sty,rtntypopt',rl',branches')
| ALetTuple (nal,(na,po),b,c) ->
- let po' = option_smartmap (subst_aconstr subst bound) po
+ let po' = Option.smartmap (subst_aconstr subst bound) po
and b' = subst_aconstr subst bound b
and c' = subst_aconstr subst bound c in
if po' == po && b' == b && c' == c then raw else
ALetTuple (nal,(na,po'),b',c')
| AIf (c,(na,po),b1,b2) ->
- let po' = option_smartmap (subst_aconstr subst bound) po
+ let po' = Option.smartmap (subst_aconstr subst bound) po
and b1' = subst_aconstr subst bound b1
and b2' = subst_aconstr subst bound b2
and c' = subst_aconstr subst bound c in
if po' == po && b1' == b1 && b2' == b2 && c' == c then raw else
AIf (c',(na,po'),b1',b2')
+ | ARec (fk,idl,dll,tl,bl) ->
+ let dll' =
+ array_smartmap (list_smartmap (fun (na,oc,b as x) ->
+ let oc' = Option.smartmap (subst_aconstr subst bound) oc in
+ let b' = subst_aconstr subst bound b in
+ if oc' == oc && b' == b then x else (na,oc',b'))) dll in
+ let tl' = array_smartmap (subst_aconstr subst bound) tl in
+ let bl' = array_smartmap (subst_aconstr subst bound) bl in
+ if dll' == dll && tl' == tl && bl' == bl then raw else
+ ARec (fk,idl,dll',tl',bl')
+
| APatVar _ | ASort _ -> raw
| AHole (Evd.ImplicitArg (ref,i)) ->
@@ -348,7 +374,8 @@ let rec subst_aconstr subst bound raw =
if ref' == ref then raw else
AHole (Evd.InternalHole)
| AHole (Evd.BinderType _ | Evd.QuestionMark _ | Evd.CasesType
- | Evd.InternalHole | Evd.TomatchTypeParameter _) -> raw
+ | Evd.InternalHole | Evd.TomatchTypeParameter _ | Evd.GoalEvar
+ | Evd.ImpossibleCase) -> raw
| ACast (r1,k) ->
match k with
@@ -362,13 +389,15 @@ 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 encode_list_value l = RApp (dummy_loc,RVar (dummy_loc,ldots_var),l)
(* Pattern-matching rawconstr and aconstr *)
let abstract_return_type_context pi mklam tml rtno =
- option_map (fun rtn ->
+ Option.map (fun rtn ->
let nal =
List.flatten (List.map (fun (_,(na,t)) ->
match t with Some x -> (pi x)@[na] | None -> [na]) tml) in
@@ -377,7 +406,7 @@ let abstract_return_type_context pi mklam tml rtno =
let abstract_return_type_context_rawconstr =
abstract_return_type_context (fun (_,_,_,nal) -> nal)
- (fun na c -> RLambda(dummy_loc,na,RHole(dummy_loc,Evd.InternalHole),c))
+ (fun na c -> RLambda(dummy_loc,na,Explicit,RHole(dummy_loc,Evd.InternalHole),c))
let abstract_return_type_context_aconstr =
abstract_return_type_context pi3
@@ -409,6 +438,14 @@ let bind_env alp sigma var v =
(* TODO: handle the case of multiple occs in different scopes *)
(var,v)::sigma
+let match_fix_kind fk1 fk2 =
+ match (fk1,fk2) with
+ | RCoFix n1, RCoFix n2 -> n1 = n2
+ | RFix (nl1,n1), RFix (nl2,n2) ->
+ n1 = n2 &&
+ array_for_all2 (fun (n1,_) (n2,_) -> n2 = None || n1 = n2) nl1 nl2
+ | _ -> false
+
let match_opt f sigma t1 t2 = match (t1,t2) with
| None, None -> sigma
| Some t1, Some t2 -> f sigma t1 t2
@@ -435,29 +472,34 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
| RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma
| RRef (_,r1), ARef r2 when r1 = r2 -> sigma
| RPatVar (_,(_,n1)), APatVar n2 when n1=n2 -> sigma
- | RApp (_,f1,l1), AApp (f2,l2) when List.length l1 = List.length l2 ->
+ | RApp (loc,f1,l1), AApp (f2,l2) ->
+ let n1 = List.length l1 and n2 = List.length l2 in
+ let f1,l1,f2,l2 =
+ if n1 < n2 then
+ let l21,l22 = list_chop (n2-n1) l2 in f1,l1, AApp (f2,l21), l22
+ else if n1 > n2 then
+ let l11,l12 = list_chop (n1-n2) l1 in RApp (loc,f1,l11),l12, f2,l2
+ 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 ->
match_alist alp metas sigma (f1::l1) (f2::l2) x iter termin lassoc
- | RLambda (_,na1,t1,b1), ALambda (na2,t2,b2) ->
+ | RLambda (_,na1,_,t1,b1), ALambda (na2,t2,b2) ->
match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2
- | RProd (_,na1,t1,b1), AProd (na2,t2,b2) ->
+ | RProd (_,na1,_,t1,b1), AProd (na2,t2,b2) ->
match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2
| RLetIn (_,na1,t1,b1), ALetIn (na2,t2,b2) ->
match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2
- | RCases (_,rtno1,tml1,eqnl1), ACases (rtno2,tml2,eqnl2)
- when List.length tml1 = List.length tml2
+ | RCases (_,sty1,rtno1,tml1,eqnl1), ACases (sty2,rtno2,tml2,eqnl2)
+ when sty1 = sty2
+ & List.length tml1 = List.length tml2
& List.length eqnl1 = List.length eqnl2 ->
let rtno1' = abstract_return_type_context_rawconstr tml1 rtno1 in
let rtno2' = abstract_return_type_context_aconstr tml2 rtno2 in
- let sigma = option_fold_left2 (match_ alp metas) sigma rtno1' rtno2' in
+ let sigma = Option.fold_left2 (match_ alp metas) sigma rtno1' rtno2' in
let sigma = List.fold_left2
(fun s (tm1,_) (tm2,_) -> match_ alp metas s tm1 tm2) sigma tml1 tml2 in
List.fold_left2 (match_equations alp metas) sigma eqnl1 eqnl2
- | RIf (_,a1,(na1,to1),b1,c1), AIf (a2,(na2,to2),b2,c2) ->
- let sigma = match_opt (match_binders alp metas na1 na2) sigma to1 to2 in
- List.fold_left2 (match_ alp metas) sigma [a1;b1;c1] [a2;b2;c2]
| RLetTuple (_,nal1,(na1,to1),b1,c1), ALetTuple (nal2,(na2,to2),b2,c2)
when List.length nal1 = List.length nal2 ->
let sigma = match_opt (match_binders alp metas na1 na2) sigma to1 to2 in
@@ -465,6 +507,22 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
let (alp,sigma) =
List.fold_left2 (match_names metas) (alp,sigma) nal1 nal2 in
match_ alp metas sigma c1 c2
+ | RIf (_,a1,(na1,to1),b1,c1), AIf (a2,(na2,to2),b2,c2) ->
+ let sigma = match_opt (match_binders alp metas na1 na2) sigma to1 to2 in
+ List.fold_left2 (match_ alp metas) sigma [a1;b1;c1] [a2;b2;c2]
+ | RRec (_,fk1,idl1,dll1,tl1,bl1), ARec (fk2,idl2,dll2,tl2,bl2)
+ when match_fix_kind fk1 fk2 & Array.length idl1 = Array.length idl2 &
+ array_for_all2 (fun l1 l2 -> List.length l1 = List.length l2) dll1 dll2
+ ->
+ let alp,sigma = array_fold_left2
+ (List.fold_left2 (fun (alp,sigma) (na1,_,oc1,b1) (na2,oc2,b2) ->
+ let sigma =
+ match_ alp metas (match_opt (match_ alp metas) sigma oc1 oc2) b1 b2
+ in match_names metas (alp,sigma) na1 na2)) (alp,sigma) dll1 dll2 in
+ let sigma = array_fold_left2 (match_ alp metas) sigma tl1 tl2 in
+ let alp,sigma = array_fold_right2 (fun id1 id2 alsig ->
+ match_names metas alsig (Name id1) (Name id2)) idl1 idl2 (alp,sigma) in
+ array_fold_left2 (match_ alp metas) sigma bl1 bl2
| RCast(_,c1, CastConv(_,t1)), ACast(c2, CastConv (_,t2)) ->
match_ alp metas (match_ alp metas sigma c1 c2) t1 t2
| RCast(_,c1, CastCoerce), ACast(c2, CastCoerce) ->
@@ -530,7 +588,9 @@ let match_aconstr c (metas_scl,pat) =
type notation = string
-type explicitation = ExplByPos of int | ExplByName of identifier
+type explicitation = ExplByPos of int * identifier option | ExplByName of identifier
+
+type binder_kind = Default of binding_kind | TypeClass of binding_kind
type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
@@ -550,22 +610,22 @@ type constr_expr =
| CFix of loc * identifier located * fixpoint_expr list
| CCoFix of loc * identifier located * cofixpoint_expr list
| CArrow of loc * constr_expr * constr_expr
- | CProdN of loc * (name located list * constr_expr) list * constr_expr
- | CLambdaN of loc * (name located list * constr_expr) list * constr_expr
+ | CProdN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
+ | CLambdaN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
| CLetIn of loc * name located * constr_expr * constr_expr
| CAppExpl of loc * (proj_flag * reference) * constr_expr list
| CApp of loc * (proj_flag * constr_expr) *
(constr_expr * explicitation located option) list
- | CCases of loc * constr_expr option *
+ | CCases of loc * case_style * constr_expr option *
(constr_expr * (name option * constr_expr option)) list *
- (loc * cases_pattern_expr list list * constr_expr) list
+ (loc * cases_pattern_expr list located list * constr_expr) list
| CLetTuple of loc * name list * (name option * constr_expr option) *
constr_expr * constr_expr
| CIf of loc * constr_expr * (name option * constr_expr option)
* constr_expr * constr_expr
- | CHole of loc
+ | CHole of loc * Evd.hole_kind option
| CPatVar of loc * (bool * patvar)
- | CEvar of loc * existential_key
+ | 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
@@ -573,16 +633,19 @@ type constr_expr =
| CDelimiters of loc * string * constr_expr
| CDynamic of loc * Dyn.t
-
and fixpoint_expr =
- identifier * (int option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
+ identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
and local_binder =
| LocalRawDef of name located * constr_expr
- | LocalRawAssum of name located list * constr_expr
+ | LocalRawAssum of name located list * binder_kind * constr_expr
+
+and typeclass_constraint = name located * binding_kind * constr_expr
+
+and typeclass_context = typeclass_constraint list
and cofixpoint_expr =
- identifier * local_binder list * constr_expr * constr_expr
+ identifier located * local_binder list * constr_expr * constr_expr
and recursion_order_expr =
| CStructRec
@@ -592,21 +655,23 @@ and recursion_order_expr =
(***********************)
(* For binders parsing *)
+let default_binder_kind = Default Explicit
+
let rec local_binders_length = function
| [] -> 0
| LocalRawDef _::bl -> 1 + local_binders_length bl
- | LocalRawAssum (idl,_)::bl -> List.length idl + local_binders_length bl
+ | LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl
let rec local_assums_length = function
| [] -> 0
| LocalRawDef _::bl -> local_binders_length bl
- | LocalRawAssum (idl,_)::bl -> List.length idl + local_binders_length bl
+ | LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl
let names_of_local_assums bl =
- List.flatten (List.map (function LocalRawAssum(l,_)->l|_->[]) bl)
+ List.flatten (List.map (function LocalRawAssum(l,_,_)->l|_->[]) bl)
let names_of_local_binders bl =
- List.flatten (List.map (function LocalRawAssum(l,_)->l|LocalRawDef(l,_)->[l]) bl)
+ List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]) bl)
(**********************************************************************)
(* Functions on constr_expr *)
@@ -622,12 +687,12 @@ let constr_loc = function
| CLetIn (loc,_,_,_) -> loc
| CAppExpl (loc,_,_) -> loc
| CApp (loc,_,_) -> loc
- | CCases (loc,_,_,_) -> loc
+ | CCases (loc,_,_,_,_) -> loc
| CLetTuple (loc,_,_,_,_) -> loc
| CIf (loc,_,_,_,_) -> loc
- | CHole loc -> loc
+ | CHole (loc, _) -> loc
| CPatVar (loc,_) -> loc
- | CEvar (loc,_) -> loc
+ | CEvar (loc,_,_) -> loc
| CSort (loc,_) -> loc
| CCast (loc,_,_) -> loc
| CNotation (loc,_,_) -> loc
@@ -663,8 +728,8 @@ let ids_of_cases_indtype =
let ids_of_cases_tomatch tms =
List.fold_right
(fun (_,(ona,indnal)) l ->
- option_fold_right (fun t -> (@) (ids_of_cases_indtype t))
- indnal (option_fold_right name_cons ona l))
+ Option.fold_right (fun t -> (@) (ids_of_cases_indtype t))
+ indnal (Option.fold_right name_cons ona l))
tms []
let is_constructor id =
@@ -680,11 +745,13 @@ let rec cases_pattern_fold_names f a = function
| CPatPrim _ | CPatAtom _ -> a
let ids_of_pattern_list =
- List.fold_left (List.fold_left (cases_pattern_fold_names Idset.add))
+ List.fold_left
+ (located_fold_left
+ (List.fold_left (cases_pattern_fold_names Idset.add)))
Idset.empty
let rec fold_constr_expr_binders g f n acc b = function
- | (nal,t)::l ->
+ | (nal,bk,t)::l ->
let nal = snd (List.split nal) in
let n' = List.fold_right (name_fold g) nal n in
f n (fold_constr_expr_binders g f n' acc b l) t
@@ -692,7 +759,7 @@ let rec fold_constr_expr_binders g f n acc b = function
f n acc b
let rec fold_local_binders g f n acc b = function
- | LocalRawAssum (nal,t)::l ->
+ | LocalRawAssum (nal,bk,t)::l ->
let nal = snd (List.split nal) in
let n' = List.fold_right (name_fold g) nal n in
f n (fold_local_binders g f n' acc b l) t
@@ -706,28 +773,28 @@ let fold_constr_expr_with_binders g f n acc = function
| CAppExpl (loc,(_,_),l) -> List.fold_left (f n) acc l
| CApp (loc,(_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l)
| CProdN (_,l,b) | CLambdaN (_,l,b) -> fold_constr_expr_binders g f n acc b l
- | CLetIn (_,na,a,b) -> fold_constr_expr_binders g f n acc b [[na],a]
+ | 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
| CDelimiters (loc,_,a) -> f n acc a
| CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _ | CRef _ ->
acc
- | CCases (loc,rtnpo,al,bl) ->
+ | 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
+ let acc = Option.fold_left (f (List.fold_right g ids n)) acc rtnpo in
let acc = List.fold_left (f n) acc (List.map fst al) in
List.fold_right (fun (loc,patl,rhs) acc ->
let ids = ids_of_pattern_list patl in
f (Idset.fold g ids n) acc rhs) bl acc
| CLetTuple (loc,nal,(ona,po),b,c) ->
let n' = List.fold_right (name_fold g) nal n in
- f (option_fold_right (name_fold g) ona n') (f n acc b) c
+ f (Option.fold_right (name_fold g) ona n') (f n acc b) c
| CIf (_,c,(ona,po),b1,b2) ->
let acc = f n (f n (f n acc b1) b2) c in
- option_fold_left (f (option_fold_right (name_fold g) ona n)) acc po
+ Option.fold_left (f (Option.fold_right (name_fold g) ona n)) acc po
| CFix (loc,_,l) ->
- let n' = List.fold_right (fun (id,_,_,_,_) -> g id) l n in
+ let n' = List.fold_right (fun ((_,id),_,_,_,_) -> g id) l n in
List.fold_right (fun (_,(_,o),lb,t,c) acc ->
fold_local_binders g f n'
(fold_local_binders g f n acc t lb) c lb) l acc
@@ -746,22 +813,40 @@ let mkIdentC id = CRef (Ident (dummy_loc, id))
let mkRefC r = CRef r
let mkAppC (f,l) = CApp (dummy_loc, (None,f), List.map (fun x -> (x,None)) l)
let mkCastC (a,k) = CCast (dummy_loc,a,k)
-let mkLambdaC (idl,a,b) = CLambdaN (dummy_loc,[idl,a],b)
+let mkLambdaC (idl,bk,a,b) = CLambdaN (dummy_loc,[idl,bk,a],b)
let mkLetInC (id,a,b) = CLetIn (dummy_loc,id,a,b)
-let mkProdC (idl,a,b) = CProdN (dummy_loc,[idl,a],b)
+let mkProdC (idl,bk,a,b) = CProdN (dummy_loc,[idl,bk,a],b)
+
+let rec mkCProdN loc bll c =
+ match bll with
+ | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
+ CProdN (loc,[idl,bk,t],mkCProdN (join_loc loc1 loc) bll c)
+ | LocalRawDef ((loc1,_) as id,b) :: bll ->
+ CLetIn (loc,id,b,mkCProdN (join_loc loc1 loc) bll c)
+ | [] -> c
+ | LocalRawAssum ([],_,_) :: bll -> mkCProdN loc bll c
+
+let rec mkCLambdaN loc bll c =
+ match bll with
+ | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
+ CLambdaN (loc,[idl,bk,t],mkCLambdaN (join_loc loc1 loc) bll c)
+ | LocalRawDef ((loc1,_) as id,b) :: bll ->
+ CLetIn (loc,id,b,mkCLambdaN (join_loc loc1 loc) bll c)
+ | [] -> c
+ | LocalRawAssum ([],_,_) :: bll -> mkCLambdaN loc bll c
let rec abstract_constr_expr c = function
| [] -> c
| LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl)
- | LocalRawAssum (idl,t)::bl ->
- List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl
+ | LocalRawAssum (idl,bk,t)::bl ->
+ List.fold_right (fun x b -> mkLambdaC([x],bk,t,b)) idl
(abstract_constr_expr c bl)
let rec prod_constr_expr c = function
| [] -> c
| LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl)
- | LocalRawAssum (idl,t)::bl ->
- List.fold_right (fun x b -> mkProdC([x],t,b)) idl
+ | LocalRawAssum (idl,bk,t)::bl ->
+ List.fold_right (fun x b -> mkProdC([x],bk,t,b)) idl
(prod_constr_expr c bl)
let coerce_to_id = function
@@ -776,15 +861,15 @@ let map_binder g e nal = List.fold_right (fun (_,na) -> name_fold g na) nal e
let map_binders f g e bl =
(* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
- let h (e,bl) (nal,t) = (map_binder g e nal,(nal,f e t)::bl) in
+ let h (e,bl) (nal,bk,t) = (map_binder g e nal,(nal,bk,f e t)::bl) in
let (e,rbl) = List.fold_left h (e,[]) bl in
(e, List.rev rbl)
let map_local_binders f g e bl =
(* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
let h (e,bl) = function
- LocalRawAssum(nal,ty) ->
- (map_binder g e nal, LocalRawAssum(nal,f e ty)::bl)
+ LocalRawAssum(nal,k,ty) ->
+ (map_binder g e nal, LocalRawAssum(nal,k,f e ty)::bl)
| LocalRawDef((loc,na),ty) ->
(name_fold g na e, LocalRawDef((loc,na),f e ty)::bl) in
let (e,rbl) = List.fold_left h (e,[]) bl in
@@ -806,32 +891,32 @@ let map_constr_expr_with_binders g f e = function
| CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a)
| CHole _ | CEvar _ | CPatVar _ | CSort _
| CPrim _ | CDynamic _ | CRef _ as x -> x
- | CCases (loc,rtnpo,a,bl) ->
+ | 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
let ids = ids_of_cases_tomatch a in
- let po = option_map (f (List.fold_right g ids e)) rtnpo in
- CCases (loc, po, List.map (fun (tm,x) -> (f e tm,x)) a,bl)
+ let po = Option.map (f (List.fold_right g ids e)) rtnpo in
+ CCases (loc, sty, po, List.map (fun (tm,x) -> (f e tm,x)) a,bl)
| CLetTuple (loc,nal,(ona,po),b,c) ->
let e' = List.fold_right (name_fold g) nal e in
- let e'' = option_fold_right (name_fold g) ona e in
- CLetTuple (loc,nal,(ona,option_map (f e'') po),f e b,f e' c)
+ let e'' = Option.fold_right (name_fold g) ona e in
+ CLetTuple (loc,nal,(ona,Option.map (f e'') po),f e b,f e' c)
| CIf (loc,c,(ona,po),b1,b2) ->
- let e' = option_fold_right (name_fold g) ona e in
- CIf (loc,f e c,(ona,option_map (f e') po),f e b1,f e b2)
+ let e' = Option.fold_right (name_fold g) ona e in
+ CIf (loc,f e c,(ona,Option.map (f e') po),f e b1,f e b2)
| CFix (loc,id,dl) ->
CFix (loc,id,List.map (fun (id,n,bl,t,d) ->
let (e',bl') = map_local_binders f g e bl in
let t' = f e' t in
(* Note: fix names should be inserted before the arguments... *)
- let e'' = List.fold_left (fun e (id,_,_,_,_) -> g id e) e' dl in
+ let e'' = List.fold_left (fun e ((_,id),_,_,_,_) -> g id e) e' dl in
let d' = f e'' d in
(id,n,bl',t',d')) dl)
| CCoFix (loc,id,dl) ->
CCoFix (loc,id,List.map (fun (id,bl,t,d) ->
let (e',bl') = map_local_binders f g e bl in
let t' = f e' t in
- let e'' = List.fold_left (fun e (id,_,_,_) -> g id e) e' dl in
+ let e'' = List.fold_left (fun e ((_,id),_,_,_) -> g id e) e' dl in
let d' = f e'' d in
(id,bl',t',d')) dl)
@@ -849,10 +934,16 @@ type with_declaration_ast =
| CWith_Module of identifier list located * qualid located
| CWith_Definition of identifier list located * constr_expr
-type module_type_ast =
- | CMTEident of qualid located
- | CMTEwith of module_type_ast * with_declaration_ast
type module_ast =
| CMEident of qualid located
| CMEapply of module_ast * module_ast
+
+type module_type_ast =
+ | CMTEident of qualid located
+ | CMTEapply of module_type_ast * module_ast
+ | CMTEwith of module_type_ast * with_declaration_ast
+
+type include_ast =
+ | CIMTE of module_type_ast
+ | CIME of module_ast
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 3c359bd5..d4fef0dc 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 9976 2007-07-12 11:58:30Z msozeau $ i*)
+(*i $Id: topconstr.mli 11024 2008-05-30 12:41:39Z msozeau $ i*)
(*i*)
open Pp
@@ -33,11 +33,14 @@ type aconstr =
| ALambda of name * aconstr * aconstr
| AProd of name * aconstr * aconstr
| ALetIn of name * aconstr * aconstr
- | ACases of aconstr option *
+ | ACases of case_style * aconstr option *
(aconstr * (name * (inductive * int * name list) option)) list *
(cases_pattern list * aconstr) list
| ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
| AIf of aconstr * (name * aconstr option) * aconstr * aconstr
+ | ARec of fix_kind * identifier array *
+ (name * aconstr option * aconstr) list array * aconstr array *
+ aconstr array
| ASort of rawsort
| AHole of Evd.hole_kind
| APatVar of patvar
@@ -65,11 +68,6 @@ val rawconstr_of_aconstr_with_binders : loc ->
val rawconstr_of_aconstr : loc -> aconstr -> rawconstr
(**********************************************************************)
-(* Substitution of kernel names, avoiding a list of bound identifiers *)
-
-val subst_aconstr : substitution -> identifier list -> aconstr -> aconstr
-
-(**********************************************************************)
(* [match_aconstr metas] matches a rawconstr against an aconstr with *)
(* metavariables in [metas]; raise [No_match] if the matching fails *)
@@ -86,11 +84,18 @@ val match_aconstr : rawconstr -> interpretation ->
(rawconstr * (tmp_scope_name option * scope_name list)) list
(**********************************************************************)
+(* Substitution of kernel names in interpretation data *)
+
+val subst_interpretation : substitution -> interpretation -> interpretation
+
+(**********************************************************************)
(*s Concrete syntax for terms *)
type notation = string
-type explicitation = ExplByPos of int | ExplByName of identifier
+type explicitation = ExplByPos of int * identifier option | ExplByName of identifier
+
+type binder_kind = Default of binding_kind | TypeClass of binding_kind
type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
@@ -110,22 +115,22 @@ type constr_expr =
| CFix of loc * identifier located * fixpoint_expr list
| CCoFix of loc * identifier located * cofixpoint_expr list
| CArrow of loc * constr_expr * constr_expr
- | CProdN of loc * (name located list * constr_expr) list * constr_expr
- | CLambdaN of loc * (name located list * constr_expr) list * constr_expr
+ | CProdN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
+ | CLambdaN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
| CLetIn of loc * name located * constr_expr * constr_expr
| CAppExpl of loc * (proj_flag * reference) * constr_expr list
| CApp of loc * (proj_flag * constr_expr) *
- (constr_expr * explicitation located option) list
- | CCases of loc * constr_expr option *
+ (constr_expr * explicitation located option) list
+ | CCases of loc * case_style * constr_expr option *
(constr_expr * (name option * constr_expr option)) list *
- (loc * cases_pattern_expr list list * constr_expr) list
+ (loc * cases_pattern_expr list located list * constr_expr) list
| CLetTuple of loc * name list * (name option * constr_expr option) *
constr_expr * constr_expr
| CIf of loc * constr_expr * (name option * constr_expr option)
* constr_expr * constr_expr
- | CHole of loc
+ | CHole of loc * Evd.hole_kind option
| CPatVar of loc * (bool * patvar)
- | CEvar of loc * existential_key
+ | 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
@@ -134,19 +139,24 @@ type constr_expr =
| CDynamic of loc * Dyn.t
and fixpoint_expr =
- identifier * (int option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
+ identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
and cofixpoint_expr =
- identifier * local_binder list * constr_expr * constr_expr
+ identifier located * local_binder list * constr_expr * constr_expr
and recursion_order_expr =
| CStructRec
| CWfRec of constr_expr
| CMeasureRec of constr_expr
+(** Anonymous defs allowed ?? *)
and local_binder =
| LocalRawDef of name located * constr_expr
- | LocalRawAssum of name located list * constr_expr
+ | LocalRawAssum of name located list * binder_kind * constr_expr
+
+type typeclass_constraint = name located * binding_kind * constr_expr
+
+and typeclass_context = typeclass_constraint list
(**********************************************************************)
(* Utilities on constr_expr *)
@@ -161,6 +171,8 @@ val replace_vars_constr_expr :
val free_vars_of_constr_expr : constr_expr -> Idset.t
val occur_var_constr_expr : identifier -> constr_expr -> bool
+val default_binder_kind : binder_kind
+
(* Specific function for interning "in indtype" syntax of "match" *)
val ids_of_cases_indtype : constr_expr -> identifier list
@@ -168,15 +180,19 @@ val mkIdentC : identifier -> constr_expr
val mkRefC : reference -> constr_expr
val mkAppC : constr_expr * constr_expr list -> constr_expr
val mkCastC : constr_expr * constr_expr cast_type -> constr_expr
-val mkLambdaC : name located list * constr_expr * constr_expr -> constr_expr
+val mkLambdaC : name located list * binder_kind * constr_expr * constr_expr -> constr_expr
val mkLetInC : name located * constr_expr * constr_expr -> constr_expr
-val mkProdC : name located list * constr_expr * constr_expr -> constr_expr
+val mkProdC : name located list * binder_kind * constr_expr * constr_expr -> constr_expr
val coerce_to_id : constr_expr -> identifier located
val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
+(* Same as [abstract_constr_expr] and [prod_constr_expr], with location *)
+val mkCLambdaN : loc -> local_binder list -> constr_expr -> constr_expr
+val mkCProdN : loc -> local_binder list -> constr_expr -> constr_expr
+
(* For binders parsing *)
(* Includes let binders *)
@@ -191,6 +207,11 @@ val names_of_local_assums : local_binder list -> name located list
(* With let binders *)
val names_of_local_binders : local_binder list -> name located list
+(* Used in typeclasses *)
+
+val fold_constr_expr_with_binders : (identifier -> 'a -> 'a) ->
+ ('a -> 'b -> constr_expr -> 'b) -> 'a -> 'b -> constr_expr -> 'b
+
(* Used in correctness and interface; absence of var capture not guaranteed *)
(* in pattern-matching clauses and in binders of the form [x,y:T(x)] *)
@@ -205,10 +226,17 @@ type with_declaration_ast =
| CWith_Module of identifier list located * qualid located
| CWith_Definition of identifier list located * constr_expr
-type module_type_ast =
- | CMTEident of qualid located
- | CMTEwith of module_type_ast * with_declaration_ast
type module_ast =
| CMEident of qualid located
| CMEapply of module_ast * module_ast
+
+type module_type_ast =
+ | CMTEident of qualid located
+ | CMTEapply of module_type_ast * module_ast
+ | CMTEwith of module_type_ast * with_declaration_ast
+
+type include_ast =
+ | CIMTE of module_type_ast
+ | CIME of module_ast
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-15 23:13:34 +0000