diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 44 | ||||
| -rw-r--r-- | interp/constrintern.ml | 106 | ||||
| -rw-r--r-- | interp/constrintern.mli | 2 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.ml | 215 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.mli | 51 | ||||
| -rw-r--r-- | interp/reserve.ml | 6 | ||||
| -rw-r--r-- | interp/topconstr.ml | 78 | ||||
| -rw-r--r-- | interp/topconstr.mli | 25 |
8 files changed, 428 insertions, 99 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 1117d25079..7e288f3117 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -216,7 +216,7 @@ let rec check_same_type ty1 ty2 = | _ when ty1=ty2 -> () | _ -> failwith "not same type" -and check_same_binder (nal1,e1) (nal2,e2) = +and check_same_binder (nal1,_,e1) (nal2,_,e2) = List.iter2 (fun (_,na1) (_,na2) -> if na1<>na2 then failwith "not same name") nal1 nal2; check_same_type e1 e2 @@ -224,10 +224,10 @@ and check_same_binder (nal1,e1) (nal2,e2) = and check_same_fix_binder bl1 bl2 = List.iter2 (fun b1 b2 -> match b1,b2 with - LocalRawAssum(nal1,ty1), LocalRawAssum(nal2,ty2) -> - check_same_binder (nal1,ty1) (nal2,ty2) + LocalRawAssum(nal1,k,ty1), LocalRawAssum(nal2,k',ty2) -> + check_same_binder (nal1,k,ty1) (nal2,k',ty2) | LocalRawDef(na1,def1), LocalRawDef(na2,def2) -> - check_same_binder ([na1],def1) ([na2],def2) + check_same_binder ([na1],default_binder_kind,def1) ([na2],default_binder_kind,def2) | _ -> failwith "not same binder") bl1 bl2 let same c d = try check_same_type c d; true with _ -> false @@ -255,10 +255,10 @@ let rec same_raw c d = | RPatVar(_,pv1), RPatVar(_,pv2) -> if pv1<>pv2 then failwith "RPatVar" | RApp(_,f1,a1), RApp(_,f2,a2) -> List.iter2 same_raw (f1::a1) (f2::a2) - | RLambda(_,na1,t1,m1), RLambda(_,na2,t2,m2) -> + | RLambda(_,na1,bk1,t1,m1), RLambda(_,na2,bk2,t2,m2) -> if na1 <> na2 then failwith "RLambda"; same_raw t1 t2; same_raw m1 m2 - | RProd(_,na1,t1,m1), RProd(_,na2,t2,m2) -> + | RProd(_,na1,bk1,t1,m1), RProd(_,na2,bk2,t2,m2) -> if na1 <> na2 then failwith "RProd"; same_raw t1 t2; same_raw m1 m2 | RLetIn(_,na1,t1,m1), RLetIn(_,na2,t2,m2) -> @@ -283,7 +283,7 @@ let rec same_raw c d = | RRec(_,fk1,na1,bl1,ty1,def1), RRec(_,fk2,na2,bl2,ty2,def2) -> if fk1 <> fk2 || na1 <> na2 then failwith "RRec"; array_iter2 - (List.iter2 (fun (na1,bd1,ty1) (na2,bd2,ty2) -> + (List.iter2 (fun (na1,bk1,bd1,ty1) (na2,bk2,bd2,ty2) -> if na1<>na2 then failwith "RRec"; Option.iter2 same_raw bd1 bd2; same_raw ty1 ty2)) bl1 bl2; @@ -582,7 +582,7 @@ let rec rename_rawconstr_var id0 id1 = function let rec share_fix_binders n rbl ty def = match ty,def with - RProd(_,na0,t0,b), RLambda(_,na1,t1,m) -> + RProd(_,na0,bk0,t0,b), RLambda(_,na1,bk1,t1,m) -> if not(same_rawconstr t0 t1) then List.rev rbl, ty, def else let (na,b,m) = @@ -672,7 +672,7 @@ let rec extern inctx scopes vars r = explicitize loc inctx [] (None,sub_extern false scopes vars f) (List.map (sub_extern true scopes vars) args)) - | RProd (loc,Anonymous,t,c) -> + | RProd (loc,Anonymous,_,t,c) -> (* Anonymous product are never factorized *) CArrow (loc,extern_typ scopes vars t, extern_typ scopes vars c) @@ -680,15 +680,15 @@ let rec extern inctx scopes vars r = CLetIn (loc,(loc,na),sub_extern false scopes vars t, extern inctx scopes (add_vname vars na) c) - | RProd (loc,na,t,c) -> + | RProd (loc,na,bk,t,c) -> let t = extern_typ scopes vars (anonymize_if_reserved na t) in let (idl,c) = factorize_prod scopes (add_vname vars na) t c in - CProdN (loc,[(dummy_loc,na)::idl,t],c) + CProdN (loc,[(dummy_loc,na)::idl,Default bk,t],c) - | RLambda (loc,na,t,c) -> + | RLambda (loc,na,bk,t,c) -> let t = extern_typ scopes vars (anonymize_if_reserved na t) in let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) t c in - CLambdaN (loc,[(dummy_loc,na)::idl,t],c) + CLambdaN (loc,[(dummy_loc,na)::idl,Default bk,t],c) | RCases (loc,rtntypopt,tml,eqns) -> let vars' = @@ -775,7 +775,7 @@ and factorize_prod scopes vars aty c = if !Flags.raw_print or !print_no_symbol then raise No_match; ([],extern_symbol scopes vars c (uninterp_notations c)) with No_match -> match c with - | RProd (loc,(Name id as na),ty,c) + | RProd (loc,(Name id as na),bk,ty,c) when same aty (extern_typ scopes vars (anonymize_if_reserved na ty)) & not (occur_var_constr_expr id aty) (* avoid na in ty escapes scope *) -> let (nal,c) = factorize_prod scopes (Idset.add id vars) aty c in @@ -787,7 +787,7 @@ and factorize_lambda inctx scopes vars aty c = if !Flags.raw_print or !print_no_symbol then raise No_match; ([],extern_symbol scopes vars c (uninterp_notations c)) with No_match -> match c with - | RLambda (loc,na,ty,c) + | RLambda (loc,na,bk,ty,c) when same aty (extern_typ scopes vars (anonymize_if_reserved na ty)) & not (occur_name na aty) (* To avoid na in ty' escapes scope *) -> let (nal,c) = @@ -797,24 +797,24 @@ and factorize_lambda inctx scopes vars aty c = and extern_local_binder scopes vars = function [] -> ([],[]) - | (na,Some bd,ty)::l -> + | (na,bk,Some bd,ty)::l -> let (ids,l) = extern_local_binder scopes (name_fold Idset.add na vars) l in (na::ids, LocalRawDef((dummy_loc,na), extern false scopes vars bd) :: l) - | (na,None,ty)::l -> + | (na,bk,None,ty)::l -> let ty = extern_typ scopes vars (anonymize_if_reserved na ty) in (match extern_local_binder scopes (name_fold Idset.add na vars) l with - (ids,LocalRawAssum(nal,ty')::l) + (ids,LocalRawAssum(nal,k,ty')::l) when same ty ty' & match na with Name id -> not (occur_var_constr_expr id ty') | _ -> true -> (na::ids, - LocalRawAssum((dummy_loc,na)::nal,ty')::l) + LocalRawAssum((dummy_loc,na)::nal,k,ty')::l) | (ids,l) -> (na::ids, - LocalRawAssum([(dummy_loc,na)],ty) :: l)) + LocalRawAssum([(dummy_loc,na)],Default bk,ty) :: l)) and extern_eqn inctx scopes vars (loc,ids,pl,c) = (loc,[List.map (extern_cases_pattern_in_scope scopes vars) pl], @@ -927,11 +927,11 @@ let rec raw_of_pat env = function RApp (loc,RPatVar (loc,(true,n)), List.map (raw_of_pat env) args) | PProd (na,t,c) -> - RProd (loc,na,raw_of_pat env t,raw_of_pat (na::env) c) + RProd (loc,na,Explicit,raw_of_pat env t,raw_of_pat (na::env) c) | PLetIn (na,t,c) -> RLetIn (loc,na,raw_of_pat env t, raw_of_pat (na::env) c) | PLambda (na,t,c) -> - RLambda (loc,na,raw_of_pat env t, raw_of_pat (na::env) c) + RLambda (loc,na,Explicit,raw_of_pat env t, raw_of_pat (na::env) c) | PIf (c,b1,b2) -> RIf (loc, raw_of_pat env c, (Anonymous,None), raw_of_pat env b1, raw_of_pat env b2) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index a418253462..3214ca6c45 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -86,7 +86,7 @@ let explain_bad_patterns_number n1 n2 = let explain_bad_explicitation_number n po = match n with - | ExplByPos n -> + | ExplByPos (n,_id) -> let s = match po with | None -> str "a regular argument" | Some p -> int p in @@ -683,7 +683,7 @@ let extract_explicit_arg imps args = user_err_loc (loc,"",str "Argument name " ++ pr_id id ++ str " occurs more than once"); id - | ExplByPos p -> + | ExplByPos (p,_id) -> let id = try let imp = List.nth imps (p-1) in @@ -775,6 +775,16 @@ let set_type_scope (ids,tmp_scope,scopes) = let reset_tmp_scope (ids,tmp_scope,scopes) = (ids,None,scopes) +let rec it_mkRProd env body = + match env with + (na, bk, _, t) :: tl -> it_mkRProd tl (RProd (dummy_loc, na, bk, t, body)) + | [] -> body + +let rec it_mkRLambda env body = + match env with + (na, bk, _, t) :: tl -> it_mkRLambda tl (RLambda (dummy_loc, na, bk, t, body)) + | [] -> body + (**********************************************************************) (* Main loop *) @@ -844,15 +854,15 @@ let internalise sigma globalenv env allow_patvar lvar c = Array.map (fun (_,ty,_) -> ty) idl, Array.map (fun (_,_,bd) -> bd) idl) | CArrow (loc,c1,c2) -> - RProd (loc, Anonymous, intern_type env c1, intern_type env c2) + RProd (loc, Anonymous, Explicit, intern_type env c1, intern_type env c2) | CProdN (loc,[],c2) -> intern_type env c2 - | CProdN (loc,(nal,ty)::bll,c2) -> - iterate_prod loc env ty (CProdN (loc, bll, c2)) nal + | CProdN (loc,(nal,bk,ty)::bll,c2) -> + iterate_prod loc env bk ty (CProdN (loc, bll, c2)) nal | CLambdaN (loc,[],c2) -> intern env c2 - | CLambdaN (loc,(nal,ty)::bll,c2) -> - iterate_lam loc (reset_tmp_scope env) ty (CLambdaN (loc, bll, c2)) nal + | CLambdaN (loc,(nal,bk,ty)::bll,c2) -> + iterate_lam loc (reset_tmp_scope env) bk ty (CLambdaN (loc, bll, c2)) nal | CLetIn (loc,(_,na),c1,c2) -> RLetIn (loc, na, intern (reset_tmp_scope env) c1, intern (push_name_env lvar env na) c2) @@ -934,17 +944,20 @@ let internalise sigma globalenv env allow_patvar lvar c = and intern_type env = intern (set_type_scope env) and intern_local_binder ((ids,ts,sc as env),bl) = function - | LocalRawAssum(nal,ty) -> - let (loc,na) = List.hd nal in - (* TODO: fail if several names with different implicit types *) - let ty = locate_if_isevar loc na (intern_type env ty) in - List.fold_left - (fun ((ids,ts,sc),bl) (_,na) -> - ((name_fold Idset.add na ids,ts,sc), (na,None,ty)::bl)) - (env,bl) nal + | LocalRawAssum(nal,bk,ty) -> + (match bk with + | Default k -> + let (loc,na) = List.hd nal in + (* TODO: fail if several names with different implicit types *) + let ty = locate_if_isevar loc na (intern_type env ty) in + List.fold_left + (fun ((ids,ts,sc),bl) (_,na) -> + ((name_fold Idset.add na ids,ts,sc), (na,k,None,ty)::bl)) + (env,bl) nal + | TypeClass b -> anomaly ("TODO: intern_local_binder TypeClass")) | LocalRawDef((loc,na),def) -> ((name_fold Idset.add na ids,ts,sc), - (na,Some(intern env def),RHole(loc,Evd.BinderType na))::bl) + (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl) (* Expands a multiple pattern into a disjunction of multiple patterns *) and intern_multiple_pattern scopes pl = @@ -1004,22 +1017,50 @@ let internalise sigma globalenv env allow_patvar lvar c = | _, None -> Anonymous | _, Some na -> na in (tm',(na,typ)), na::ids + + and intern_typeclass_binders env bl = + List.fold_left + (fun ((ids,ts,sc) as env,bl) ((loc, na), bk, ty) -> + let ty = locate_if_isevar loc na (intern_type env ty) in + ((name_fold Idset.add na ids,ts,sc), (na,bk,None,ty)::bl)) + env bl - and iterate_prod loc2 env ty body = function + and iterate_prod loc2 env bk ty body nal = + let rec default env bk = function | (loc1,na)::nal -> if nal <> [] then check_capture loc1 ty na; - let body = iterate_prod loc2 (push_name_env lvar env na) ty body nal in + let body = default (push_name_env lvar env na) bk nal in let ty = locate_if_isevar loc1 na (intern_type env ty) in - RProd (join_loc loc1 loc2, na, ty, body) + RProd (join_loc loc1 loc2, na, bk, ty, body) | [] -> intern_type env body - - and iterate_lam loc2 env ty body = function - | (loc1,na)::nal -> - if nal <> [] then check_capture loc1 ty na; - let body = iterate_lam loc2 (push_name_env lvar env na) ty body nal in - let ty = locate_if_isevar loc1 na (intern_type env ty) in - RLambda (join_loc loc1 loc2, na, ty, body) - | [] -> intern env body + in + match bk with + | Default b -> default env b nal + | TypeClass b -> + let ctx = (List.hd nal, b, ty) in + let (fvs, bind) = Implicit_quantifiers.generalize_class_binders_raw (pi1 env) [ctx] in + let env, ifvs = intern_typeclass_binders (env,[]) fvs in + let env, ibind = intern_typeclass_binders (env,ifvs) bind in + let body = intern_type env body in + it_mkRProd ibind body + + and iterate_lam loc2 env bk ty body nal = + let rec default env bk = function + | (loc1,na)::nal -> + if nal <> [] then check_capture loc1 ty na; + let body = default (push_name_env lvar env na) bk nal in + let ty = locate_if_isevar loc1 na (intern_type env ty) in + RLambda (join_loc loc1 loc2, na, bk, ty, body) + | [] -> intern env body + in match bk with + | Default b -> default env b nal + | TypeClass b -> + let ctx = (List.hd nal, b, ty) in + let (fvs, bind) = Implicit_quantifiers.generalize_class_binders_raw (pi1 env) [ctx] in + let env, ifvs = intern_typeclass_binders (env,[]) fvs in + let env, ibind = intern_typeclass_binders (env,ifvs) bind 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 @@ -1046,7 +1087,7 @@ let internalise sigma globalenv env allow_patvar lvar c = | (imp::impl', []) -> if eargs <> [] then (let (id,(loc,_)) = List.hd eargs in - user_err_loc (loc,"",str "Not enough non implicit + user_err_loc (loc,"",str "Not enough non implicit arguments to accept the argument bound to " ++ pr_id id)); [] | ([], rargs) -> @@ -1123,7 +1164,6 @@ let interp_open_constr sigma env c = let interp_constr_judgment sigma env c = Default.understand_judgment sigma env (intern_constr sigma env c) - let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c = Default.understand_tcc_evars evdref env kind (intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c) @@ -1175,11 +1215,11 @@ open Term let interp_context sigma env params = List.fold_left (fun (env,params) d -> match d with - | LocalRawAssum ([_,na],(CHole _ as t)) -> + | LocalRawAssum ([_,na],k,(CHole _ as t)) -> let t = interp_binder sigma env na t in let d = (na,None,t) in (push_rel d env, d::params) - | LocalRawAssum (nal,t) -> + | LocalRawAssum (nal,k,t) -> let t = interp_type sigma env t in let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in let ctx = List.rev ctx in @@ -1193,11 +1233,11 @@ let interp_context sigma env params = let interp_context_evars evdref env params = List.fold_left (fun (env,params) d -> match d with - | LocalRawAssum ([_,na],(CHole _ as t)) -> + | LocalRawAssum ([_,na],k,(CHole _ as t)) -> let t = interp_binder_evars evdref env na t in let d = (na,None,t) in (push_rel d env, d::params) - | LocalRawAssum (nal,t) -> + | LocalRawAssum (nal,k,t) -> let t = interp_type_evars evdref env t in let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in let ctx = List.rev ctx in diff --git a/interp/constrintern.mli b/interp/constrintern.mli index eac01a92ae..f4272a2b19 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -103,6 +103,8 @@ val interp_reference : ltac_sign -> reference -> rawconstr val interp_binder : evar_map -> env -> name -> constr_expr -> types +val interp_binder_evars : evar_defs ref -> env -> name -> constr_expr -> types + (* Interpret contexts: returns extended env and context *) val interp_context : evar_map -> env -> local_binder list -> env * rel_context diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml new file mode 100644 index 0000000000..d9113644cb --- /dev/null +++ b/interp/implicit_quantifiers.ml @@ -0,0 +1,215 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: classes.ml 6748 2005-02-18 22:17:50Z herbelin $ i*) + +(*i*) +open Names +open Decl_kinds +open Term +open Sign +open Evd +open Environ +open Nametab +open Mod_subst +open Util +open Rawterm +open Topconstr +open Libnames +open Typeclasses +open Typeclasses_errors +(*i*) + +(* 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 Idset.mem id bdvars then l else if List.mem id l then l else id :: l in + let rec aux bdvars l c = match c with + | CRef (Ident (_,id)) -> found id bdvars l + | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id))) :: _) when not (Idset.mem id bdvars) -> + fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c + | c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c + in aux bound l c + + +let locate_reference qid = + match Nametab.extended_locate qid with + | TrueGlobal ref -> ref + | SyntacticDef kn -> + match Syntax_def.search_syntactic_definition dummy_loc kn with + | Rawterm.RRef (_,ref) -> ref + | _ -> raise Not_found + +let is_global id = + try + let _ = locate_reference (make_short_qualid id) in true + with Not_found -> + false + +let is_freevar ids env x = + try + if Idset.mem x ids then false + else + try ignore(Environ.lookup_named x env) ; false + with _ -> not (is_global x) + with _ -> true + +let freevars_of_ids env ids = + List.filter (is_freevar env (Global.env())) ids + +let compute_constrs_freevars env constrs = + let ids = + List.rev (List.fold_left + (fun acc x -> free_vars_of_constr_expr x acc) + [] constrs) + in freevars_of_ids env ids + +(* let compute_context_freevars env ctx = *) +(* let ids = *) +(* List.rev *) +(* (List.fold_left *) +(* (fun acc (_,i,x) -> free_vars_of_constr_expr x acc) *) +(* [] constrs) *) +(* in freevars_of_ids ids *) + +let compute_constrs_freevars_binders env constrs = + let elts = compute_constrs_freevars env constrs in + List.map (fun id -> (dummy_loc, id), CHole dummy_loc) elts + +let ids_of_named_context_avoiding avoid l = + List.fold_left (fun (ids, avoid) id -> + let id' = Nameops.next_ident_away_from id avoid in id' :: ids, id' :: avoid) + ([], avoid) (Termops.ids_of_named_context l) + +let combine_params avoid applied needed = + let rec aux ids app need = + match app, need with + [], need -> + let need', avoid = ids_of_named_context_avoiding avoid need in + List.rev ids @ (List.map mkIdentC need'), avoid + | x :: app, _ :: need -> aux (x :: ids) app need + | _ :: _, [] -> failwith "combine_params: overly applied typeclass" + in aux [] applied needed + +let compute_context_vars env l = + List.fold_left (fun l (iid, _, c) -> + (match snd iid with Name i -> [i] | Anonymous -> []) @ free_vars_of_constr_expr c ~bound:env l) + [] l + +let destClassApp cl = + match cl with + | CApp (loc, (None,CRef (Ident f)), l) -> f, List.map fst l + | _ -> raise Not_found + +let full_class_binders env l = + let avoid = compute_context_vars env l in + let l', avoid = + List.fold_left (fun (l', avoid) (iid, bk, cl as x) -> + match bk with + Explicit -> + let (id, l) = destClassApp cl in + (try + let c = class_info (snd id) in + let args, avoid = combine_params avoid l (List.rev c.cl_context @ List.rev c.cl_super @ List.rev c.cl_params) in + (iid, bk, CAppExpl (fst id, (None, Ident id), args)) :: l', avoid + with Not_found -> unbound_class (Global.env ()) id) + | Implicit -> (x :: l', avoid)) + ([], avoid) l + in List.rev l' + +let constr_expr_of_constraint (kind, id) l = + match kind with + | Explicit -> CAppExpl (fst id, (None, Ident id), l) + | Implicit -> CApp (fst id, (None, CRef (Ident id)), + List.map (fun x -> x, None) l) + +(* | CApp of loc * (proj_flag * constr_expr) * *) +(* (constr_expr * explicitation located option) list *) + + +let constrs_of_context l = + List.map (fun (_, id, l) -> constr_expr_of_constraint id l) l + +let compute_context_freevars env ctx = + let bound, ids = + List.fold_left + (fun (bound, acc) (oid, id, x) -> + let bound = match snd oid with Name n -> Idset.add n bound | Anonymous -> bound in + bound, free_vars_of_constr_expr x ~bound acc) + (env,[]) ctx + in freevars_of_ids env (List.rev ids) + +let resolve_class_binders env l = + let ctx = full_class_binders env l in + let fv_ctx = + let elts = compute_context_freevars env ctx in + List.map (fun id -> (dummy_loc, id), CHole dummy_loc) elts + in + fv_ctx, ctx + +let generalize_class_binders env l = + let fv_ctx, cstrs = resolve_class_binders env l in + List.map (fun ((loc, id), t) -> LocalRawAssum ([loc, Name id], Default Implicit, t)) fv_ctx, + List.map (fun (iid, bk, c) -> LocalRawAssum ([iid], Default Implicit, c)) + cstrs + +let generalize_class_binders_raw env l = + let fv_ctx, cstrs = resolve_class_binders env l in + List.map (fun ((loc, id), t) -> ((loc, Name id), Implicit, t)) fv_ctx, + List.map (fun (iid, bk, c) -> (iid, Implicit, c)) cstrs + +let ctx_of_class_binders env l = + let (x, y) = generalize_class_binders env l in x @ y + +let implicits_of_binders l = + let rec aux i l = + match l with + [] -> [] + | hd :: tl -> + let res, reslen = + match hd with + LocalRawAssum (nal, Default Implicit, t) -> + list_map_i (fun i (_,id) -> + let name = + match id with + Name id -> Some id + | Anonymous -> None + in ExplByPos (i, name), (true, true)) + i nal, List.length nal + | LocalRawAssum (nal, _, _) -> [], List.length nal + | LocalRawDef _ -> [], 1 + in res @ (aux (i + reslen) tl) + in aux 1 l + +let implicits_of_rawterm l = + let rec aux i c = + match c with + RProd (loc, na, bk, t, b) | RLambda (loc, na, bk, t, b) -> + let rest = aux (succ i) b in + if bk = Implicit then + let name = + match na with + Name id -> Some id + | Anonymous -> None + in + (ExplByPos (i, name), (true, true)) :: rest + else rest + | RLetIn (loc, na, t, b) -> aux i b + | _ -> [] + in aux 1 l + +let nf_named_context sigma ctx = + Sign.map_named_context (Reductionops.nf_evar sigma) ctx + +let nf_rel_context sigma ctx = + Sign.map_rel_context (Reductionops.nf_evar sigma) ctx + +let nf_env sigma env = + let nc' = nf_named_context sigma (Environ.named_context env) in + let rel' = nf_rel_context sigma (Environ.rel_context env) in + push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env) diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli new file mode 100644 index 0000000000..a61dbcadf5 --- /dev/null +++ b/interp/implicit_quantifiers.mli @@ -0,0 +1,51 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: classes.ml 6748 2005-02-18 22:17:50Z herbelin $ i*) + +(*i*) +open Names +open Decl_kinds +open Term +open Sign +open Evd +open Environ +open Nametab +open Mod_subst +open Rawterm +open Topconstr +open Util +open Typeclasses +(*i*) + +val destClassApp : constr_expr -> identifier located * constr_expr list + +val free_vars_of_constr_expr : Topconstr.constr_expr -> + ?bound:Idset.t -> + Names.identifier list -> Names.identifier list + +val compute_constrs_freevars : Idset.t -> constr_expr list -> identifier list +val compute_constrs_freevars_binders : Idset.t -> constr_expr list -> (identifier located * constr_expr) list +val resolve_class_binders : Idset.t -> typeclass_context -> + (identifier located * constr_expr) list * typeclass_context + +val full_class_binders : Idset.t -> typeclass_context -> typeclass_context + +val generalize_class_binders_raw : Idset.t -> typeclass_context -> + (name located * binding_kind * constr_expr) list * (name located * binding_kind * constr_expr) list + +val ctx_of_class_binders : Idset.t -> typeclass_context -> local_binder list + +val implicits_of_binders : local_binder list -> (Topconstr.explicitation * (bool * bool)) list + +val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool)) list + +val nf_named_context : evar_map -> named_context -> named_context +val nf_rel_context : evar_map -> rel_context -> rel_context +val nf_env : evar_map -> env -> env + diff --git a/interp/reserve.ml b/interp/reserve.ml index 02e15f0690..f3c3506b5c 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -54,8 +54,8 @@ open Rawterm let rec unloc = function | RVar (_,id) -> RVar (dummy_loc,id) | RApp (_,g,args) -> RApp (dummy_loc,unloc g, List.map unloc args) - | RLambda (_,na,ty,c) -> RLambda (dummy_loc,na,unloc ty,unloc c) - | RProd (_,na,ty,c) -> RProd (dummy_loc,na,unloc ty,unloc c) + | RLambda (_,na,bk,ty,c) -> RLambda (dummy_loc,na,bk,unloc ty,unloc c) + | RProd (_,na,bk,ty,c) -> RProd (dummy_loc,na,bk,unloc ty,unloc c) | RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c) | RCases (_,rtntypopt,tml,pl) -> RCases (dummy_loc, @@ -69,7 +69,7 @@ let rec unloc = function | RRec (_,fk,idl,bl,tyl,bv) -> RRec (dummy_loc,fk,idl, Array.map (List.map - (fun (na,obd,ty) -> (na,Option.map unloc obd, unloc ty))) + (fun (na,k,obd,ty) -> (na,k,Option.map unloc obd, unloc ty))) bl, Array.map unloc tyl, Array.map unloc bv) diff --git a/interp/topconstr.ml b/interp/topconstr.ml index e29f172109..2994bc3aea 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -74,9 +74,9 @@ let rawconstr_of_aconstr_with_binders loc g f e = function let outerl = (ldots_var,inner)::(if swap then [x,RVar(loc,y)] else []) in subst_rawvars outerl it | ALambda (na,ty,c) -> - let e,na = name_fold_map g e na in RLambda (loc,na,f e ty,f e c) + let e,na = name_fold_map g e na in RLambda (loc,na,Explicit,f e ty,f e c) | AProd (na,ty,c) -> - let e,na = name_fold_map g e na in RProd (loc,na,f e ty,f e c) + let e,na = name_fold_map g e na in RProd (loc,na,Explicit,f e ty,f e c) | ALetIn (na,b,c) -> let e,na = name_fold_map g e na in RLetIn (loc,na,f e b,f e c) | ACases (rtntypopt,tml,eqnl) -> @@ -131,9 +131,9 @@ let compare_rawconstr f t1 t2 = match t1,t2 with | RRef (_,r1), RRef (_,r2) -> r1 = r2 | RVar (_,v1), RVar (_,v2) -> v1 = v2 | RApp (_,f1,l1), RApp (_,f2,l2) -> f f1 f2 & List.for_all2 f l1 l2 - | RLambda (_,na1,ty1,c1), RLambda (_,na2,ty2,c2) when na1 = na2 -> + | RLambda (_,na1,bk1,ty1,c1), RLambda (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 -> f ty1 ty2 & f c1 c2 - | RProd (_,na1,ty1,c1), RProd (_,na2,ty2,c2) when na1 = na2 -> + | RProd (_,na1,bk1,ty1,c1), RProd (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 -> f ty1 ty2 & f c1 c2 | RHole _, RHole _ -> true | RSort (_,s1), RSort (_,s2) -> s1 = s2 @@ -180,8 +180,8 @@ let aconstr_and_vars_of_rawconstr a = found := ldots_var :: !found; assert lassoc; AList (x,y,AApp (AVar ldots_var,[AVar x]),aux t,lassoc) | RApp (_,g,args) -> AApp (aux g, List.map aux args) - | RLambda (_,na,ty,c) -> add_name found na; ALambda (na,aux ty,aux c) - | RProd (_,na,ty,c) -> add_name found na; AProd (na,aux ty,aux c) + | RLambda (_,na,bk,ty,c) -> add_name found na; ALambda (na,aux ty,aux c) + | RProd (_,na,bk,ty,c) -> add_name found na; AProd (na,aux ty,aux c) | RLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c) | RCases (_,rtntypopt,tml,eqnl) -> let f (_,idl,pat,rhs) = found := idl@(!found); (pat,aux rhs) in @@ -377,7 +377,7 @@ let abstract_return_type_context pi mklam tml rtno = let abstract_return_type_context_rawconstr = abstract_return_type_context (fun (_,_,_,nal) -> nal) - (fun na c -> RLambda(dummy_loc,na,RHole(dummy_loc,Evd.InternalHole),c)) + (fun na c -> RLambda(dummy_loc,na,Explicit,RHole(dummy_loc,Evd.InternalHole),c)) let abstract_return_type_context_aconstr = abstract_return_type_context pi3 @@ -440,9 +440,9 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with | RApp (_,f1,l1), AList (x,_,(AApp (f2,l2) as iter),termin,lassoc) when List.length l1 = List.length l2 -> match_alist alp metas sigma (f1::l1) (f2::l2) x iter termin lassoc - | RLambda (_,na1,t1,b1), ALambda (na2,t2,b2) -> + | RLambda (_,na1,_,t1,b1), ALambda (na2,t2,b2) -> match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2 - | RProd (_,na1,t1,b1), AProd (na2,t2,b2) -> + | RProd (_,na1,_,t1,b1), AProd (na2,t2,b2) -> match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2 | RLetIn (_,na1,t1,b1), ALetIn (na2,t2,b2) -> match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2 @@ -530,7 +530,9 @@ let match_aconstr c (metas_scl,pat) = type notation = string -type explicitation = ExplByPos of int | ExplByName of identifier +type explicitation = ExplByPos of int * identifier option | ExplByName of identifier + +type binder_kind = Default of binding_kind | TypeClass of binding_kind type proj_flag = int option (* [Some n] = proj of the n-th visible argument *) @@ -550,8 +552,8 @@ type constr_expr = | CFix of loc * identifier located * fixpoint_expr list | CCoFix of loc * identifier located * cofixpoint_expr list | CArrow of loc * constr_expr * constr_expr - | CProdN of loc * (name located list * constr_expr) list * constr_expr - | CLambdaN of loc * (name located list * constr_expr) list * constr_expr + | CProdN of loc * (name located list * binder_kind * constr_expr) list * constr_expr + | CLambdaN of loc * (name located list * binder_kind * constr_expr) list * constr_expr | CLetIn of loc * name located * constr_expr * constr_expr | CAppExpl of loc * (proj_flag * reference) * constr_expr list | CApp of loc * (proj_flag * constr_expr) * @@ -579,7 +581,11 @@ and fixpoint_expr = and local_binder = | LocalRawDef of name located * constr_expr - | LocalRawAssum of name located list * constr_expr + | LocalRawAssum of name located list * binder_kind * constr_expr + +and typeclass_constraint = name located * binding_kind * constr_expr + +and typeclass_context = typeclass_constraint list and cofixpoint_expr = identifier * local_binder list * constr_expr * constr_expr @@ -592,21 +598,23 @@ and recursion_order_expr = (***********************) (* For binders parsing *) +let default_binder_kind = Default Explicit + let rec local_binders_length = function | [] -> 0 | LocalRawDef _::bl -> 1 + local_binders_length bl - | LocalRawAssum (idl,_)::bl -> List.length idl + local_binders_length bl + | LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl let rec local_assums_length = function | [] -> 0 | LocalRawDef _::bl -> local_binders_length bl - | LocalRawAssum (idl,_)::bl -> List.length idl + local_binders_length bl + | LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl let names_of_local_assums bl = - List.flatten (List.map (function LocalRawAssum(l,_)->l|_->[]) bl) + List.flatten (List.map (function LocalRawAssum(l,_,_)->l|_->[]) bl) let names_of_local_binders bl = - List.flatten (List.map (function LocalRawAssum(l,_)->l|LocalRawDef(l,_)->[l]) bl) + List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]) bl) (**********************************************************************) (* Functions on constr_expr *) @@ -684,7 +692,7 @@ let ids_of_pattern_list = Idset.empty let rec fold_constr_expr_binders g f n acc b = function - | (nal,t)::l -> + | (nal,bk,t)::l -> let nal = snd (List.split nal) in let n' = List.fold_right (name_fold g) nal n in f n (fold_constr_expr_binders g f n' acc b l) t @@ -692,7 +700,7 @@ let rec fold_constr_expr_binders g f n acc b = function f n acc b let rec fold_local_binders g f n acc b = function - | LocalRawAssum (nal,t)::l -> + | LocalRawAssum (nal,bk,t)::l -> let nal = snd (List.split nal) in let n' = List.fold_right (name_fold g) nal n in f n (fold_local_binders g f n' acc b l) t @@ -706,7 +714,7 @@ let fold_constr_expr_with_binders g f n acc = function | CAppExpl (loc,(_,_),l) -> List.fold_left (f n) acc l | CApp (loc,(_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l) | CProdN (_,l,b) | CLambdaN (_,l,b) -> fold_constr_expr_binders g f n acc b l - | CLetIn (_,na,a,b) -> fold_constr_expr_binders g f n acc b [[na],a] + | CLetIn (_,na,a,b) -> fold_constr_expr_binders g f n acc b [[na],default_binder_kind,a] | CCast (loc,a,CastConv(_,b)) -> f n (f n acc a) b | CCast (loc,a,CastCoerce) -> f n acc a | CNotation (_,_,l) -> List.fold_left (f n) acc l @@ -746,40 +754,40 @@ let mkIdentC id = CRef (Ident (dummy_loc, id)) let mkRefC r = CRef r let mkAppC (f,l) = CApp (dummy_loc, (None,f), List.map (fun x -> (x,None)) l) let mkCastC (a,k) = CCast (dummy_loc,a,k) -let mkLambdaC (idl,a,b) = CLambdaN (dummy_loc,[idl,a],b) +let mkLambdaC (idl,bk,a,b) = CLambdaN (dummy_loc,[idl,bk,a],b) let mkLetInC (id,a,b) = CLetIn (dummy_loc,id,a,b) -let mkProdC (idl,a,b) = CProdN (dummy_loc,[idl,a],b) +let mkProdC (idl,bk,a,b) = CProdN (dummy_loc,[idl,bk,a],b) let rec mkCProdN loc bll c = match bll with - | LocalRawAssum ((loc1,_)::_ as idl,t) :: bll -> - CProdN (loc,[idl,t],mkCProdN (join_loc loc1 loc) bll c) + | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll -> + CProdN (loc,[idl,bk,t],mkCProdN (join_loc loc1 loc) bll c) | LocalRawDef ((loc1,_) as id,b) :: bll -> CLetIn (loc,id,b,mkCProdN (join_loc loc1 loc) bll c) | [] -> c - | LocalRawAssum ([],_) :: bll -> mkCProdN loc bll c + | LocalRawAssum ([],_,_) :: bll -> mkCProdN loc bll c let rec mkCLambdaN loc bll c = match bll with - | LocalRawAssum ((loc1,_)::_ as idl,t) :: bll -> - CLambdaN (loc,[idl,t],mkCLambdaN (join_loc loc1 loc) bll c) + | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll -> + CLambdaN (loc,[idl,bk,t],mkCLambdaN (join_loc loc1 loc) bll c) | LocalRawDef ((loc1,_) as id,b) :: bll -> CLetIn (loc,id,b,mkCLambdaN (join_loc loc1 loc) bll c) | [] -> c - | LocalRawAssum ([],_) :: bll -> mkCLambdaN loc bll c + | LocalRawAssum ([],_,_) :: bll -> mkCLambdaN loc bll c let rec abstract_constr_expr c = function | [] -> c | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl) - | LocalRawAssum (idl,t)::bl -> - List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl + | LocalRawAssum (idl,bk,t)::bl -> + List.fold_right (fun x b -> mkLambdaC([x],bk,t,b)) idl (abstract_constr_expr c bl) let rec prod_constr_expr c = function | [] -> c | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl) - | LocalRawAssum (idl,t)::bl -> - List.fold_right (fun x b -> mkProdC([x],t,b)) idl + | LocalRawAssum (idl,bk,t)::bl -> + List.fold_right (fun x b -> mkProdC([x],bk,t,b)) idl (prod_constr_expr c bl) let coerce_to_id = function @@ -794,15 +802,15 @@ let map_binder g e nal = List.fold_right (fun (_,na) -> name_fold g na) nal e let map_binders f g e bl = (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *) - let h (e,bl) (nal,t) = (map_binder g e nal,(nal,f e t)::bl) in + let h (e,bl) (nal,bk,t) = (map_binder g e nal,(nal,bk,f e t)::bl) in let (e,rbl) = List.fold_left h (e,[]) bl in (e, List.rev rbl) let map_local_binders f g e bl = (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *) let h (e,bl) = function - LocalRawAssum(nal,ty) -> - (map_binder g e nal, LocalRawAssum(nal,f e ty)::bl) + LocalRawAssum(nal,k,ty) -> + (map_binder g e nal, LocalRawAssum(nal,k,f e ty)::bl) | LocalRawDef((loc,na),ty) -> (name_fold g na e, LocalRawDef((loc,na),f e ty)::bl) in let (e,rbl) = List.fold_left h (e,[]) bl in diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 3d928bbb4a..608cedb3c1 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -90,7 +90,9 @@ val match_aconstr : rawconstr -> interpretation -> type notation = string -type explicitation = ExplByPos of int | ExplByName of identifier +type explicitation = ExplByPos of int * identifier option | ExplByName of identifier + +type binder_kind = Default of binding_kind | TypeClass of binding_kind type proj_flag = int option (* [Some n] = proj of the n-th visible argument *) @@ -110,8 +112,8 @@ type constr_expr = | CFix of loc * identifier located * fixpoint_expr list | CCoFix of loc * identifier located * cofixpoint_expr list | CArrow of loc * constr_expr * constr_expr - | CProdN of loc * (name located list * constr_expr) list * constr_expr - | CLambdaN of loc * (name located list * constr_expr) list * constr_expr + | CProdN of loc * (name located list * binder_kind * constr_expr) list * constr_expr + | CLambdaN of loc * (name located list * binder_kind * constr_expr) list * constr_expr | CLetIn of loc * name located * constr_expr * constr_expr | CAppExpl of loc * (proj_flag * reference) * constr_expr list | CApp of loc * (proj_flag * constr_expr) * @@ -146,7 +148,11 @@ and recursion_order_expr = and local_binder = | LocalRawDef of name located * constr_expr - | LocalRawAssum of name located list * constr_expr + | LocalRawAssum of name located list * binder_kind * constr_expr + +type typeclass_constraint = name located * binding_kind * constr_expr + +and typeclass_context = typeclass_constraint list (**********************************************************************) (* Utilities on constr_expr *) @@ -161,6 +167,8 @@ val replace_vars_constr_expr : val free_vars_of_constr_expr : constr_expr -> Idset.t val occur_var_constr_expr : identifier -> constr_expr -> bool +val default_binder_kind : binder_kind + (* Specific function for interning "in indtype" syntax of "match" *) val ids_of_cases_indtype : constr_expr -> identifier list @@ -168,9 +176,9 @@ val mkIdentC : identifier -> constr_expr val mkRefC : reference -> constr_expr val mkAppC : constr_expr * constr_expr list -> constr_expr val mkCastC : constr_expr * constr_expr cast_type -> constr_expr -val mkLambdaC : name located list * constr_expr * constr_expr -> constr_expr +val mkLambdaC : name located list * binder_kind * constr_expr * constr_expr -> constr_expr val mkLetInC : name located * constr_expr * constr_expr -> constr_expr -val mkProdC : name located list * constr_expr * constr_expr -> constr_expr +val mkProdC : name located list * binder_kind * constr_expr * constr_expr -> constr_expr val coerce_to_id : constr_expr -> identifier located @@ -195,6 +203,11 @@ val names_of_local_assums : local_binder list -> name located list (* With let binders *) val names_of_local_binders : local_binder list -> name located list +(* Used in typeclasses *) + +val fold_constr_expr_with_binders : (identifier -> 'a -> 'a) -> + ('a -> 'b -> constr_expr -> 'b) -> 'a -> 'b -> constr_expr -> 'b + (* Used in correctness and interface; absence of var capture not guaranteed *) (* in pattern-matching clauses and in binders of the form [x,y:T(x)] *) |