From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- interp/constrextern.ml | 238 ++++++----- interp/constrextern.mli | 9 +- interp/constrintern.ml | 905 +++++++++++++++++++++++++--------------- interp/constrintern.mli | 37 +- interp/coqlib.ml | 36 +- interp/coqlib.mli | 9 +- interp/genarg.ml | 26 +- interp/genarg.mli | 247 ++++++----- interp/implicit_quantifiers.ml | 285 +++++++++++++ interp/implicit_quantifiers.mli | 68 +++ interp/modintern.ml | 63 ++- interp/modintern.mli | 13 +- interp/notation.ml | 86 ++-- interp/notation.mli | 7 +- interp/reserve.ml | 20 +- interp/syntax_def.ml | 47 ++- interp/syntax_def.mli | 22 +- interp/topconstr.ml | 269 ++++++++---- interp/topconstr.mli | 74 +++- 19 files changed, 1660 insertions(+), 801 deletions(-) create mode 100644 interp/implicit_quantifiers.ml create mode 100644 interp/implicit_quantifiers.mli (limited to 'interp') 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,18 +316,104 @@ 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") else 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 *) @@ -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 @@ -699,121 +930,54 @@ let extract_explicit_arg imps args = ((id,(loc,a))::eargs,rargs) 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 *) +(* 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 *) +(* 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 @@ -64,11 +67,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 *) @@ -85,12 +83,19 @@ type interpretation = 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 + -- cgit v1.2.3