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