From 11a923b21b669d1a8e1c51afd42caf38d20fb79d Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 10 Jun 2003 21:20:34 +0000 Subject: Ajout notation c.(f) en v8 pour les projections de Record git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4128 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/correctness/psyntax.ml4 | 4 +- interp/constrintern.ml | 189 ++++++++++++++++++++++++++-------------- interp/topconstr.ml | 106 ++++++++++++++++++++-- interp/topconstr.mli | 14 +-- parsing/egrammar.ml | 7 +- parsing/g_constr.ml4 | 10 +-- parsing/g_constrnew.ml4 | 10 ++- parsing/g_proofs.ml4 | 6 +- parsing/g_vernac.ml4 | 2 +- parsing/ppconstr.ml | 30 +++++-- parsing/q_coqast.ml4 | 4 +- 11 files changed, 278 insertions(+), 104 deletions(-) diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4 index 888f876de..0e6b3b7d2 100644 --- a/contrib/correctness/psyntax.ml4 +++ b/contrib/correctness/psyntax.ml4 @@ -107,7 +107,7 @@ open Coqast let mk_id loc id = mkRefC (Ident (loc, id)) let mk_ref loc s = mk_id loc (id_of_string s) let mk_appl loc1 loc2 f args = - CApp (join_loc loc1 loc2, mk_ref loc1 f, List.map (fun a -> a,None) args) + CApp (join_loc loc1 loc2, (false,mk_ref loc1 f), List.map (fun a -> a,None) args) let conj_assert {a_name=n;a_value=a} {a_value=b} = let loc1 = constr_loc a in @@ -166,7 +166,7 @@ let rec coqast_of_program loc = function (function Term t -> (coqast_of_program t.loc t.desc,None) | _ -> invalid_arg "coqast_of_program") l in - CApp (dummy_loc, f, args) + CApp (dummy_loc, (false,f), args) | Expression c -> bdize c | _ -> invalid_arg "coqast_of_program" diff --git a/interp/constrintern.ml b/interp/constrintern.ml index cfb0c4fb1..17405769a 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -55,7 +55,7 @@ let explain_variable_capture id = str "The variable " ++ pr_id id ++ str " occurs in its type" let explain_wrong_explicit_implicit = - str "Found an explicitely given implicit argument but was expecting" ++ + str "Found an explicitly given implicit argument but was expecting" ++ fnl () ++ str "a regular one" let explain_negative_metavariable = @@ -122,14 +122,18 @@ let add_glob loc ref = (**********************************************************************) (* Remembering the parsing scope of variables in notations *) -let set_var_scope loc id (_,_,scopes) (_,_,varscopes) = +let make_current_scope (scopt,scopes) = option_cons scopt scopes + +let set_var_scope loc id (_,_,scopt,scopes) (_,_,varscopes) = try let idscopes = List.assoc id varscopes in - if !idscopes <> None & !idscopes <> Some scopes then + if !idscopes <> None & + make_current_scope (out_some !idscopes) + <> make_current_scope (scopt,scopes) then user_err_loc (loc,"set_var_scope", pr_id id ++ str " already occurs in a different scope") else - idscopes := Some scopes + idscopes := Some (scopt,scopes) with Not_found -> if_verbose warning ("Could not globalize " ^ (string_of_id id)) @@ -140,7 +144,7 @@ let set_var_scope loc id (_,_,scopes) (_,_,varscopes) = [vars2] is the set of global variables, env is the set of variables abstracted until this point *) -let intern_var (env,impls,scopes) ((vars1,unbndltacvars),vars2,_) loc id = +let intern_var (env,impls,_,_) ((vars1,unbndltacvars),vars2,_) loc id = (* Is [id] bound in current env or ltac vars bound to constr *) if Idset.mem id env or List.mem id vars1 then @@ -197,12 +201,22 @@ let intern_reference env lvar = function else raise e let interp_reference vars r = - let (r,_,_) = intern_reference (Idset.empty,[],[]) (vars,[],[]) r in r + let (r,_,_) = intern_reference (Idset.empty,[],None,[]) (vars,[],[]) r in r + +let apply_scope_env (ids,impls,_,scopes as env) = function + | [] -> (ids,impls,None,scopes), [] + | sc::scl -> (ids,impls,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 apply_scope_env (ids,impls,scopes as env) = function - | [] -> env, [] - | (Some sc)::scl -> (ids,impls,sc::scopes), scl - | None::scl -> env, scl +let rec simple_adjust_scopes = function + | _,[] -> [] + | [],_::args -> None :: simple_adjust_scopes ([],args) + | sc::scopes,_::args -> sc :: simple_adjust_scopes (scopes,args) (**********************************************************************) (* Cases *) @@ -298,21 +312,25 @@ let maybe_constructor ref = try ConstrPat (find_constructor ref) with InternalisationError _ -> VarPat (find_pattern_variable ref) -let rec intern_cases_pattern scopes aliases = function +let rec intern_cases_pattern scopes aliases tmp_scope = function | CPatAlias (loc, p, id) -> let aliases' = merge_aliases aliases id in - intern_cases_pattern scopes aliases' p + intern_cases_pattern scopes aliases' tmp_scope p | CPatCstr (loc, head, pl) -> let c = find_constructor head in + let argscs = + simple_adjust_scopes (find_arguments_scope (ConstructRef c), pl) in let (idsl,pl') = - List.split (List.map (intern_cases_pattern scopes ([],[])) pl) + List.split (List.map2 (intern_cases_pattern scopes ([],[])) argscs pl) in (aliases::(List.flatten idsl), PatCstr (loc,c,pl',alias_of aliases)) | CPatNumeral (loc, n) -> + let scopes = option_cons tmp_scope scopes in ([aliases], Symbols.interp_numeral_as_pattern loc n (alias_of aliases) scopes) | CPatDelimiters (loc, key, e) -> - intern_cases_pattern (find_delimiters_scope loc key::scopes) aliases e + intern_cases_pattern (find_delimiters_scope loc key::scopes) + aliases None e | CPatAtom (loc, Some head) -> (match maybe_constructor head with | ConstrPat c -> @@ -358,6 +376,18 @@ let locate_if_isevar loc na = function (**********************************************************************) (* Utilities for application *) + +let check_projection nargs = function + | RRef (loc, ref) -> + (try + let n = Recordops.find_projection_nparams ref in + if nargs <> n+1 then + user_err_loc (loc,"",str "Projection has not enough parameters"); + with Not_found -> + user_err_loc + (loc,"",pr_global_env Idset.empty ref ++ str " is not a registered projection")) + | r -> user_err_loc (loc_of_rawconstr r, "", str "Not a projection") + let set_hole_implicit i = function | RRef (loc,r) -> (loc,ImplicitArg (r,i)) | RVar (loc,id) -> (loc,ImplicitArg (VarRef id,i)) @@ -372,25 +402,43 @@ let coerce_to_id = function user_err_loc (constr_loc c, "subst_rawconstr", str"This expression should be a simple identifier") -let traverse_binder subst id (ids,impls,scopes as env) = +let traverse_binder subst id (ids,impls,tmpsc,scopes as env) = let id = try coerce_to_id (fst (List.assoc id subst)) with Not_found -> id in - id,(Idset.add id ids,impls,scopes) + id,(Idset.add id ids,impls,tmpsc,scopes) -let rec subst_rawconstr loc interp subst (ids,impls,scopes as env) = function +type ameta_scope = + | RefArg of (global_reference * int) list + | TypeArg + +let rec subst_rawconstr loc interp subst (ids,impls,_,scopes as env) = function | AVar id -> - let (a,subscopes) = + let (a,(scopt,subscopes)) = + (* subst remembers the delimiters stack in the interpretation *) + (* of the notations *) try List.assoc id subst - with Not_found -> (CRef (Ident (loc,id)),[]) in - interp (ids,impls,subscopes@scopes) a + with Not_found -> (CRef (Ident (loc,id)),(None,[])) in + let env = (ids,impls,scopt,subscopes@scopes) in + interp env a +(* + | AApp (ARef ref,args) -> + let argscopes = find_arguments_scope ref in + let argsenv = adjust_scopes env argscopes args in + RApp (loc,RRef (loc,ref), + List.map2 (subst_rawconstr loc interp subst) argsenv args) + (* TODO: adjust type_scope for lambda, annotations, etc *) +*) | t -> map_aconstr_with_binders_loc loc (traverse_binder subst) - (subst_rawconstr loc interp subst) env t + (subst_rawconstr loc interp subst) (ids,impls,None,scopes) t + +let set_type_scope (ids,impls,tmp_scope,scopes) = + (ids,impls,Some Symbols.type_scope,scopes) (**********************************************************************) (* Main loop *) -let internalise isarity sigma env allow_soapp lvar c = - let rec intern isarity (ids,impls,scopes as env) = function +let internalise sigma env allow_soapp lvar c = + let rec intern (ids,impls,tmp_scope,scopes as env) = function | CRef ref as x -> let (c,imp,subscopes) = intern_reference env lvar ref in (match intern_impargs c env imp subscopes [] with @@ -406,8 +454,8 @@ let internalise isarity sigma env allow_soapp lvar c = in let ids' = List.fold_right Idset.add lf ids in let defl = - Array.of_list (List.map (intern false (ids',impls,scopes)) lt) in - let arityl = Array.of_list (List.map (intern true env) lc) in + Array.of_list (List.map (intern (ids',impls,None,scopes)) lt) in + let arityl = Array.of_list (List.map (intern_type env) lc) in RRec (loc,RFix (Array.of_list ln,n), Array.of_list lf, arityl, defl) | CCoFix (loc, (locid,iddef), ldecl) -> let (lf,lc,lt) = intern_cofix ldecl in @@ -419,56 +467,60 @@ let internalise isarity sigma env allow_soapp lvar c = in let ids' = List.fold_right Idset.add lf ids in let defl = - Array.of_list (List.map (intern false (ids',impls,scopes)) lt) in - let arityl = Array.of_list (List.map (intern true env) lc) in + Array.of_list (List.map (intern (ids',impls,None,scopes)) lt) in + let arityl = Array.of_list (List.map (intern_type env) lc) in RRec (loc,RCoFix n, Array.of_list lf, arityl, defl) | CArrow (loc,c1,c2) -> - RProd (loc, Anonymous, intern true env c1, intern true env c2) + RProd (loc, Anonymous, intern_type env c1, intern_type env c2) | CProdN (loc,[],c2) -> - intern true env c2 + intern_type env c2 | CProdN (loc,(nal,ty)::bll,c2) -> iterate_prod loc env ty (CProdN (loc, bll, c2)) nal | CLambdaN (loc,[],c2) -> - intern isarity env c2 + intern env c2 | CLambdaN (loc,(nal,ty)::bll,c2) -> - iterate_lam loc isarity env ty (CLambdaN (loc, bll, c2)) nal + iterate_lam loc env ty (CLambdaN (loc, bll, c2)) nal | CLetIn (loc,(_,na),c1,c2) -> - RLetIn (loc, na, intern false env c1, - intern false (name_fold Idset.add na ids,impls,scopes) c2) + RLetIn (loc, na, intern env c1, + intern (name_fold Idset.add na ids,impls,tmp_scope,scopes) c2) | CNotation (loc,"- _",[CNumeral(_,Bignat.POS p)]) -> + let scopes = option_cons tmp_scope scopes in Symbols.interp_numeral loc (Bignat.NEG p) scopes | CNotation (loc,ntn,args) -> - let scopes = if isarity then Symbols.type_scope::scopes else scopes in + let scopes = option_cons tmp_scope scopes in let (ids,c) = Symbols.interp_notation ntn scopes in let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in - subst_rawconstr loc (intern false) subst env c + subst_rawconstr loc intern subst env c | CNumeral (loc, n) -> + let scopes = option_cons tmp_scope scopes in Symbols.interp_numeral loc n scopes | CDelimiters (loc, key, e) -> - intern isarity (ids,impls,find_delimiters_scope loc key::scopes) e - | CAppExpl (loc, ref, args) -> + intern (ids,impls,None,find_delimiters_scope loc key::scopes) e + | CAppExpl (loc, (isproj,ref), args) -> let (f,_,args_scopes) = intern_reference env lvar ref in + if isproj then check_projection (List.length args) f; RApp (loc, f, intern_args env args_scopes args) - | CApp (loc, f, args) -> + | CApp (loc, (isproj,f), args) -> let (c, impargs, args_scopes) = match f with | CRef ref -> intern_reference env lvar ref - | _ -> (intern false env f, [], []) + | _ -> (intern env f, [], []) in let args = intern_impargs c env impargs args_scopes args in + if isproj then check_projection (List.length args) c; (match c with | RApp (loc', f', args') -> (* May happen with the ``...`` and `...` grammars *) RApp (join_loc loc' loc, f',args'@args) | _ -> RApp (loc, c, args)) | CCases (loc, po, tms, eqns) -> - RCases (loc, option_app (intern true env) po, - List.map (intern false env) tms, + RCases (loc, option_app (intern_type env) po, + List.map (intern env) tms, List.map (intern_eqn (List.length tms) env) eqns) | COrderedCase (loc, tag, po, c, cl) -> - ROrderedCase (loc, tag, option_app (intern true env) po, - intern false env c, - Array.of_list (List.map (intern false env) cl)) + ROrderedCase (loc, tag, option_app (intern_type env) po, + intern env c, + Array.of_list (List.map (intern env) cl)) | CHole loc -> RHole (loc, QuestionMark) | CPatVar (loc, n) when allow_soapp -> @@ -488,13 +540,17 @@ let internalise isarity sigma env allow_soapp lvar c = | CSort (loc, s) -> RSort(loc,s) | CCast (loc, c1, c2) -> - RCast (loc,intern false env c1,intern true env c2) + RCast (loc,intern env c1,intern_type env c2) | CDynamic (loc,d) -> RDynamic (loc,d) - and intern_eqn n (ids,impls,scopes as env) (loc,lhs,rhs) = + and intern_type (ids,impls,tmp_scope,scopes) = + intern (ids,impls,Some Symbols.type_scope,scopes) + + and intern_eqn n (ids,impls,tmp_scope,scopes as env) (loc,lhs,rhs) = let (idsl_substl_list,pl) = - List.split (List.map (intern_cases_pattern scopes ([],[])) lhs) in + List.split + (List.map (intern_cases_pattern scopes ([],[]) None) lhs) in let idsl, substl = List.split (List.flatten idsl_substl_list) in let eqn_ids = List.flatten idsl in let subst = List.flatten substl in @@ -505,25 +561,25 @@ let internalise isarity sigma env allow_soapp lvar c = let rhs = replace_vars_constr_expr subst rhs in List.iter message_redundant_alias subst; let env_ids = List.fold_right Idset.add eqn_ids ids in - (loc, eqn_ids,pl,intern false (env_ids,impls,scopes) rhs) + (loc, eqn_ids,pl,intern (env_ids,impls,tmp_scope,scopes) rhs) - and iterate_prod loc2 (ids,impls,scopes as env) ty body = function + and iterate_prod loc2 (ids,impls,tmpsc,scopes as env) ty body = function | (loc1,na)::nal -> if nal <> [] then check_capture loc1 ty na; let ids' = name_fold Idset.add na ids in - let body = iterate_prod loc2 (ids',impls,scopes) ty body nal in - let ty = locate_if_isevar loc1 na (intern true env ty) in + let body = iterate_prod loc2 (ids',impls,tmpsc,scopes) ty body nal in + let ty = locate_if_isevar loc1 na (intern_type env ty) in RProd (join_loc loc1 loc2, na, ty, body) - | [] -> intern true env body + | [] -> intern env body - and iterate_lam loc2 isarity (ids,impls,scopes as env) ty body = function + and iterate_lam loc2 (ids,impls,tmpsc,scopes as env) ty body = function | (loc1,na)::nal -> if nal <> [] then check_capture loc1 ty na; let ids' = name_fold Idset.add na ids in - let body = iterate_lam loc2 isarity (ids',impls,scopes) ty body nal in - let ty = locate_if_isevar loc1 na (intern true env ty) in + let body = iterate_lam loc2 (ids',impls,tmpsc,scopes) 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 isarity env body + | [] -> intern env body and intern_impargs c env l subscopes args = let rec aux n l subscopes args = @@ -532,7 +588,7 @@ let internalise isarity sigma env allow_soapp lvar c = | (imp::l', (a,Some j)::args') -> if is_status_implicit imp & j>=n then if j=n then - (intern false enva a)::(aux (n+1) l' subscopes' args') + (intern enva a)::(aux (n+1) l' subscopes' args') else (RHole (set_hole_implicit n c))::(aux (n+1) l' subscopes' args) else @@ -543,7 +599,7 @@ let internalise isarity sigma env allow_soapp lvar c = if is_status_implicit imp then (RHole (set_hole_implicit n c))::(aux (n+1) l' subscopes' args) else - (intern false enva a)::(aux (n+1) l' subscopes' args') + (intern enva a)::(aux (n+1) l' subscopes' args') | ([],args) -> intern_tailargs env subscopes args | (_::l',[]) -> if List.for_all is_status_implicit l then @@ -557,18 +613,18 @@ let internalise isarity sigma env allow_soapp lvar c = raise (InternalisationError (constr_loc a, WrongExplicitImplicit)) | (a,None)::args -> let (enva,subscopes) = apply_scope_env env subscopes in - (intern false enva a) :: (intern_tailargs env subscopes args) + (intern enva a) :: (intern_tailargs env subscopes args) | [] -> [] and intern_args env subscopes = function | [] -> [] | a::args -> let (enva,subscopes) = apply_scope_env env subscopes in - (intern false enva a) :: (intern_args env subscopes args) + (intern enva a) :: (intern_args env subscopes args) in try - intern isarity env c + intern env c with InternalisationError (loc,e) -> user_err_loc (loc,"internalize",explain_internalisation_error e) @@ -583,7 +639,8 @@ let extract_ids env = Idset.empty let interp_rawconstr_gen isarity sigma env impls allow_soapp ltacvar c = - internalise isarity sigma (extract_ids env, impls, []) + let tmp_scope = if isarity then Some Symbols.type_scope else None in + internalise sigma (extract_ids env, impls, tmp_scope,[]) allow_soapp (ltacvar,Environ.named_context env, []) c let interp_rawconstr sigma env c = @@ -677,10 +734,12 @@ let interp_aconstr vars a = let env = Global.env () in (* [vl] is intended to remember the scope of the free variables of [a] *) let vl = List.map (fun id -> (id,ref None)) vars in - let c = for_grammar (internalise false Evd.empty (extract_ids env, [], []) + let c = for_grammar (internalise Evd.empty (extract_ids env, [], None, []) false (([],[]),Environ.named_context env,vl)) 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 occuring in binders have no relevant scope since bound *) - List.map (fun (id,r) -> (id,match !r with None -> [] | Some l -> l)) vl, a + (* Variables occurring in binders have no relevant scope since bound *) + List.map + (fun (id,r) -> (id,match !r with None -> None,[] | Some (a,l) -> a,l)) vl, + a diff --git a/interp/topconstr.ml b/interp/topconstr.ml index c8f79b8c5..5b1d2813b 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -176,6 +176,11 @@ allowed in abbreviatable expressions" (* Pattern-matching rawconstr and aconstr *) +let rec adjust_scopes = function + | _,[] -> [] + | [],a::args -> (None,a) :: adjust_scopes ([],args) + | sc::scopes,a::args -> (sc,a) :: adjust_scopes (scopes,args) + exception No_match let rec alpha_var id1 id2 = function @@ -186,12 +191,79 @@ let rec alpha_var id1 id2 = function let alpha_eq_val (x,y) = x = y +(* +let bind_env sc sigma var v = + try + let vvar,_ = List.assoc var sigma in + if alpha_eq_val (v,vvar) then sigma + else raise No_match + with Not_found -> + (* TODO: handle the case of multiple occs in different scopes *) + (var,(v,sc))::sigma + +let rec match_ sc alp metas sigma a1 a2 = match (a1,a2) with + | r1, AVar id2 when List.mem id2 metas -> bind_env sc sigma id2 r1 + | RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma + | RRef (_,r1), ARef r2 when r1 = r2 -> sigma + | RPatVar (_,(_,n1)), APatVar n2 when n1=n2 -> sigma + | RApp (_,f1,l1), AApp (f2,l2) when List.length l1 = List.length l2 -> + let sigma = match_ sc alp metas sigma f1 f2 in + let l1 = match f1 with + | RRef (_,ref) -> adjust_scopes (Symbols.find_arguments_scope ref,l1) + | _ -> List.map (fun a -> (None,a)) l1 in + List.fold_left2 (fun sigma (sc,a) b -> match_ sc alp metas sigma a b) sigma l1 l2 + | RLambda (_,na1,t1,b1), ALambda (na2,t2,b2) -> + match_binders sc alp metas (match_type alp metas sigma t1 t2) b1 b2 na1 na2 + | RProd (_,na1,t1,b1), AProd (na2,t2,b2) -> + match_binders (Some Symbols.type_scope) alp metas (match_type alp metas sigma t1 t2) b1 b2 na1 na2 + | RLetIn (_,na1,t1,b1), AProd (na2,t2,b2) -> + match_binders sc alp metas (match_ sc alp metas sigma t1 t2) b1 b2 na1 na2 + | RCases (_,po1,tml1,eqnl1), ACases (po2,tml2,eqnl2) -> + let sigma = option_fold_left2 (match_type alp metas) sigma po1 po2 in + let sigma = List.fold_left2 (match_ sc alp metas) sigma tml1 tml2 in + List.fold_left2 (match_equations sc alp metas) sigma eqnl1 eqnl2 + | ROrderedCase (_,st,po1,c1,bl1), AOrderedCase (st2,po2,c2,bl2) -> + let sigma = option_fold_left2 (match_type alp metas) sigma po1 po2 in + array_fold_left2 (match_ sc alp metas) + (match_ sc alp metas sigma c1 c2) bl1 bl2 + | RCast(_,c1,t1), ACast(c2,t2) -> + match_type alp metas (match_ sc alp metas sigma c1 c2) t1 t2 + | RSort (_,s1), ASort s2 when s1 = s2 -> sigma + | RPatVar _, AHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match + | a, AHole _ when not(Options.do_translate()) -> sigma + | RHole _, AHole _ -> sigma + | (RDynamic _ | RRec _ | REvar _), _ + | _,_ -> raise No_match + +and match_type x = match_ (Some Symbols.type_scope) x + +and match_binders sc alp metas sigma b1 b2 na1 na2 = match (na1,na2) with + | (na1,Name id2) when List.mem id2 metas -> + let sigma = + name_fold + (fun id sigma -> bind_env None sigma id2 (RVar (dummy_loc,id))) na1 sigma + in + match_ sc alp metas sigma b1 b2 + | (na1,na2) -> + let alp = + name_fold + (fun id1 -> name_fold (fun id2 alp -> (id1,id2)::alp) na2) na1 alp in + match_ sc alp metas sigma b1 b2 + +and match_equations sc alp metas sigma (_,idl1,pat1,rhs1) (idl2,pat2,rhs2) = + if idl1 = idl2 & pat1 = pat2 (* Useful to reason up to alpha ?? *) then + match_ sc alp metas sigma rhs1 rhs2 + else raise No_match + +*) + let bind_env sigma var v = try let vvar = List.assoc var sigma in if alpha_eq_val (v,vvar) then sigma else raise No_match - with Not_found -> + with Not_found -> + (* TODO: handle the case of multiple occs in different scopes *) (var,v)::sigma let rec match_ alp metas sigma a1 a2 = match (a1,a2) with @@ -243,7 +315,21 @@ and match_equations alp metas sigma (_,idl1,pat1,rhs1) (idl2,pat2,rhs2) = type scope_name = string -type interpretation = (identifier * scope_name list) list * aconstr +type interpretation = + (identifier * (scope_name option * scope_name list)) list * aconstr + +(* +let match_aconstr sc c (metas_scl,pat) = + let subst = match_ sc [] (List.map fst metas_scl) [] c pat in + (* Reorder canonically the substitution *) + let find x subst = + try List.assoc x subst + with Not_found -> + (* Happens for binders bound to Anonymous *) + (* Find a better way to propagate Anonymous... *) + RVar (dummy_loc,x),None in + List.map (fun (x,scl) -> let (a,sc) = find x subst in (a,sc,scl)) metas_scl +*) let match_aconstr c (metas_scl,pat) = let subst = match_ [] (List.map fst metas_scl) [] c pat in @@ -263,6 +349,8 @@ type notation = string type explicitation = int +type proj_flag = bool (* [true] = is projection *) + type cases_pattern_expr = | CPatAlias of loc * cases_pattern_expr * identifier | CPatCstr of loc * reference * cases_pattern_expr list @@ -278,8 +366,9 @@ type constr_expr = | CProdN of loc * (name located list * constr_expr) list * constr_expr | CLambdaN of loc * (name located list * constr_expr) list * constr_expr | CLetIn of loc * name located * constr_expr * constr_expr - | CAppExpl of loc * reference * constr_expr list - | CApp of loc * constr_expr * (constr_expr * explicitation option) list + | CAppExpl of loc * (proj_flag * reference) * constr_expr list + | CApp of loc * (proj_flag * constr_expr) * + (constr_expr * explicitation option) list | CCases of loc * constr_expr option * constr_expr list * (loc * cases_pattern_expr list * constr_expr) list | COrderedCase of loc * case_style * constr_expr option * constr_expr @@ -345,9 +434,9 @@ let occur_var_constr_ref id = function let rec occur_var_constr_expr id = function | CRef r -> occur_var_constr_ref id r | CArrow (loc,a,b) -> occur_var_constr_expr id a or occur_var_constr_expr id b - | CAppExpl (loc,r,l) -> + | CAppExpl (loc,(_,r),l) -> occur_var_constr_ref id r or List.exists (occur_var_constr_expr id) l - | CApp (loc,f,l) -> + | CApp (loc,(_,f),l) -> occur_var_constr_expr id f or List.exists (fun (a,_) -> occur_var_constr_expr id a) l | CProdN (_,l,b) -> occur_var_binders id b l @@ -372,7 +461,7 @@ and occur_var_binders id b = function let mkIdentC id = CRef (Ident (dummy_loc, id)) let mkRefC r = CRef r -let mkAppC (f,l) = CApp (dummy_loc, f, List.map (fun x -> (x,None)) l) +let mkAppC (f,l) = CApp (dummy_loc, (false,f), List.map (fun x -> (x,None)) l) let mkCastC (a,b) = CCast (dummy_loc,a,b) let mkLambdaC (idl,a,b) = CLambdaN (dummy_loc,[idl,a],b) let mkLetInC (id,a,b) = CLetIn (dummy_loc,id,a,b) @@ -389,7 +478,8 @@ let map_binders f g e bl = let map_constr_expr_with_binders f g 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,a,l) -> CApp (loc,f e a,List.map (fun (a,i) -> (f e a,i)) 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) | CLambdaN (loc,bl,b) -> diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 8f0f5fb75..f5f620528 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -50,10 +50,11 @@ val aconstr_of_rawconstr : identifier list -> rawconstr -> aconstr exception No_match type scope_name = string -type interpretation = (identifier * scope_name list) list * aconstr +type interpretation = + (identifier * (scope_name option * scope_name list)) list * aconstr -val match_aconstr : rawconstr -> interpretation -> - (rawconstr * scope_name list) list +val match_aconstr : (* scope_name option -> *) rawconstr -> interpretation -> + (rawconstr * (scope_name option * scope_name list)) list (*s Concrete syntax for terms *) @@ -61,6 +62,8 @@ type notation = string type explicitation = int +type proj_flag = bool (* [true] = is projection *) + type cases_pattern_expr = | CPatAlias of loc * cases_pattern_expr * identifier | CPatCstr of loc * reference * cases_pattern_expr list @@ -76,8 +79,9 @@ type constr_expr = | CProdN of loc * (name located list * constr_expr) list * constr_expr | CLambdaN of loc * (name located list * constr_expr) list * constr_expr | CLetIn of loc * name located * constr_expr * constr_expr - | CAppExpl of loc * reference * constr_expr list - | CApp of loc * constr_expr * (constr_expr * explicitation option) list + | CAppExpl of loc * (proj_flag * reference) * constr_expr list + | CApp of loc * (proj_flag * constr_expr) * + (constr_expr * explicitation option) list | CCases of loc * constr_expr option * constr_expr list * (loc * cases_pattern_expr list * constr_expr) list | COrderedCase of loc * case_style * constr_expr option * constr_expr diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index 83f4cad58..397189271 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -274,10 +274,11 @@ let subst_constr_expr a loc subs = let na = name_app (subst_id subs) na in CLetIn (loc,(loc,na),subst b,subst c) | CArrow (_,a,b) -> CArrow (loc,subst a,subst b) - | CAppExpl (_,Ident (_,id),l) -> - CAppExpl (loc,subst_ref loc subs id,List.map subst l) + | CAppExpl (_,(p,Ident (_,id)),l) -> + CAppExpl (loc,(p,subst_ref loc subs id),List.map subst l) | CAppExpl (_,r,l) -> CAppExpl (loc,r,List.map subst l) - | CApp (_,a,l) -> CApp (loc,subst a,List.map (fun (a,i) -> (subst a,i)) l) + | CApp (_,(p,a),l) -> + CApp (loc,(p,subst a),List.map (fun (a,i) -> (subst a,i)) l) | CCast (_,a,b) -> CCast (loc,subst a,subst b) | CNotation (_,n,l) -> CNotation (loc,n,List.map subst l) | CDelimiters (_,s,a) -> CDelimiters (loc,s,subst a) diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 367fd5e0e..be9e00c58 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -23,7 +23,7 @@ let constr_kw = ":"; "("; ")"; "["; "]"; "{"; "}"; ","; ";"; "->"; "="; ":="; "!"; "::"; "<:"; ":<"; "=>"; "<"; ">"; "|"; "?"; "/"; "<->"; "\\/"; "/\\"; "`"; "``"; "&"; "*"; "+"; "@"; "^"; "#"; "-"; - "~"; "'"; "<<"; ">>"; "<>"; + "~"; "'"; "<<"; ">>"; "<>"; ".(" ] let _ = List.iter (fun s -> Lexer.add_token ("",s)) constr_kw (* "let" is not a keyword because #Core#let.cci would not parse. @@ -127,12 +127,12 @@ GEXTEND Gram operconstr: [ "10" RIGHTA [ "!"; f = global; args = LIST0 (operconstr LEVEL "9") -> - CAppExpl (loc, f, args) + CAppExpl (loc, (false,f), args) (* | "!"; f = global; "with"; b = binding_list -> <:ast< (APPLISTWITH $f $b) >> *) - | f = operconstr; args = LIST1 constr91 -> CApp (loc, f, args) ] + | f = operconstr; args = LIST1 constr91 -> CApp (loc, (false,f), args) ] | "9" RIGHTA [ c1 = operconstr; "::"; c2 = operconstr LEVEL "9" -> CCast (loc, c1, c2) ] | "8" RIGHTA @@ -196,7 +196,7 @@ GEXTEND Gram | "("; lc1 = lconstr; ")"; "@"; "["; cl = ne_constr_list; "]" -> (match lc1 with | CPatVar (loc2,(false,n)) -> - CApp (loc,CPatVar (loc2, (true,n)), List.map (fun c -> c, None) cl) + CApp (loc,(false,CPatVar (loc2, (true,n))), List.map (fun c -> c, None) cl) | _ -> Util.error "Second-order pattern-matching expects a head metavariable") | IDENT "Fix"; id = identref; "{"; fbinders = fixbinders; "}" -> @@ -208,7 +208,7 @@ GEXTEND Gram | s = sort -> CSort (loc, s) | v = global -> CRef v | n = bigint -> CNumeral (loc,n) - | "!"; f = global -> CAppExpl (loc,f,[]) + | "!"; f = global -> CAppExpl (loc,(false,f),[]) | "'"; test_ident_colon; key = IDENT; ":"; c = constr; "'" -> CDelimiters (loc,key,c) ] ] ; diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4 index 88d108fdd..1876863d4 100644 --- a/parsing/g_constrnew.ml4 +++ b/parsing/g_constrnew.ml4 @@ -142,11 +142,15 @@ GEXTEND Gram | "40L" LEFTA [ "-"; c = operconstr -> CNotation(loc,"- _",[c]) ] | "10L" LEFTA - [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,f,args) - | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,f,args) ] + [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,(false,f),args) + | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(false,f),args) ] | "9" [ ] | "1L" LEFTA - [ c=operconstr; "%"; key=IDENT -> CDelimiters (loc,key,c) ] + [ c=operconstr; "%"; key=IDENT -> CDelimiters (loc,key,c) + | c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" -> + CApp(loc,(true,CRef f),args@[c,None]) + | c=operconstr; ".("; "@"; f=global; args=LIST0 NEXT -> + CAppExpl(loc,(false,f),args@[c]) ] | "0" [ c=atomic_constr -> c | c=match_constr -> c diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 7fba1f279..5acc694aa 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -117,10 +117,12 @@ GEXTEND Gram hints: [ [ IDENT "Resolve"; l = LIST1 global; dbnames = opt_hintbases -> (dbnames, - HintsResolve (List.map (fun qid -> (None, CAppExpl(loc,qid,[]))) l)) + HintsResolve + (List.map (fun qid -> (None, CAppExpl(loc,(false,qid),[]))) l)) | IDENT "Immediate"; l = LIST1 global; dbnames = opt_hintbases -> (dbnames, - HintsImmediate (List.map (fun qid-> (None, CAppExpl (loc,qid,[]))) l)) + HintsImmediate + (List.map (fun qid-> (None, CAppExpl (loc,(false,qid),[]))) l)) | IDENT "Unfold"; l = LIST1 global; dbnames = opt_hintbases -> (dbnames, HintsUnfold (List.map (fun qid -> (None,qid)) l)) ] ] ; diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 629c20177..0d431ea93 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -422,7 +422,7 @@ GEXTEND Gram let c = match n with | Some n -> let l = list_tabulate (fun _ -> (CHole (loc),None)) n in - CApp (loc,c,l) + CApp (loc,(false,c),l) | None -> c in VernacNotation (false,c,Some("'"^id^"'",[]),None,None) | IDENT "Implicits"; qid = global; "["; l = LIST0 natural; "]" -> diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 72a693012..361e24647 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -213,6 +213,19 @@ let pr_cases pr po tml eqns = prlist_with_sep (fun () -> str "| ") (pr_eqn pr) eqns ++ str "end")) +let pr_proj pr pr_app a f l = + hov 0 (pr (latom,E) a ++ cut() ++ str ".(" ++ pr_app pr f l ++ str ")") + +let pr_explapp pr f l = + hov 0 ( + str "!" ++ pr_reference f ++ + prlist (fun a -> brk (1,1) ++ pr (lapp,L) a) l) + +let pr_app pr a l = + hov 0 ( + pr (lapp,L) a ++ + prlist (fun a -> brk (1,1) ++ pr_expl_args pr a) l) + let rec pr inherited a = let (strm,prec) = match a with | CRef r -> pr_reference r, latom @@ -234,14 +247,15 @@ let rec pr inherited a = hv 1 ( hv 1 (str "[" ++ pr_let_binder pr (snd x) a ++ bll ++ str "]") ++ brk (0,1) ++ b), lletin - | CAppExpl (_,f,l) -> - hov 0 ( - str "!" ++ pr_reference f ++ - prlist (fun a -> brk (1,1) ++ pr (lapp,L) a) l), lapp - | CApp (_,a,l) -> - hov 0 ( - pr (lapp,L) a ++ - prlist (fun a -> brk (1,1) ++ pr_expl_args pr a) l), lapp + | CAppExpl (_,(true,f),l) -> + let a,l = list_sep_last l in + pr_proj pr pr_explapp a f l, lapp + | CAppExpl (_,(false,f),l) -> pr_explapp pr f l, lapp + | CApp (_,(true,a),l) -> + let c,l = list_sep_last l in + assert (snd c = None); + pr_proj pr pr_app (fst c) a l, lapp + | CApp (_,(false,a),l) -> pr_app pr a l, lapp | CCases (_,po,tml,eqns) -> pr_cases pr po tml eqns, lcases | COrderedCase (_,IfStyle,po,c,[b1;b2]) -> diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index a42465572..cf59d9a97 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -194,8 +194,8 @@ let rec mlexpr_of_constr = function | Topconstr.CProdN (loc,l,a) -> <:expr< Topconstr.CProdN $dloc$ $mlexpr_of_list (mlexpr_of_pair (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_constr) l$ $mlexpr_of_constr a$ >> | Topconstr.CLambdaN (loc,l,a) -> <:expr< Topconstr.CLambdaN $dloc$ $mlexpr_of_list (mlexpr_of_pair (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_constr) l$ $mlexpr_of_constr a$ >> | Topconstr.CLetIn (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO" - | Topconstr.CAppExpl (loc,a,l) -> <:expr< Topconstr.CAppExpl $dloc$ $mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >> - | Topconstr.CApp (loc,a,l) -> <:expr< Topconstr.CApp $dloc$ $mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option mlexpr_of_int)) l$ >> + | Topconstr.CAppExpl (loc,a,l) -> <:expr< Topconstr.CAppExpl $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >> + | Topconstr.CApp (loc,a,l) -> <:expr< Topconstr.CApp $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option mlexpr_of_int)) l$ >> | Topconstr.CCases (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO" | Topconstr.COrderedCase (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO" | Topconstr.CHole loc -> <:expr< Topconstr.CHole $dloc$ >> -- cgit v1.2.3