diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrexpr_ops.ml | 20 | ||||
| -rw-r--r-- | interp/constrextern.ml | 31 | ||||
| -rw-r--r-- | interp/constrintern.ml | 208 | ||||
| -rw-r--r-- | interp/constrintern.mli | 5 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.ml | 4 | ||||
| -rw-r--r-- | interp/notation.ml | 29 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 46 | ||||
| -rw-r--r-- | interp/notation_ops.mli | 1 | ||||
| -rw-r--r-- | interp/ppextend.ml | 1 | ||||
| -rw-r--r-- | interp/ppextend.mli | 1 |
10 files changed, 219 insertions, 127 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 83add7a7c..4877bf271 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -67,7 +67,7 @@ let rec cases_pattern_expr_eq p1 p2 = if CAst.(p1.v == p2.v) then true else match CAst.(p1.v, p2.v) with | CPatAlias(a1,i1), CPatAlias(a2,i2) -> - Id.equal i1 i2 && cases_pattern_expr_eq a1 a2 + Name.equal (snd i1) (snd i2) && cases_pattern_expr_eq a1 a2 | CPatCstr(c1,a1,b1), CPatCstr(c2,a2,b2) -> eq_reference c1 c2 && Option.equal (List.equal cases_pattern_expr_eq) a1 a2 && @@ -222,9 +222,10 @@ and local_binder_eq l1 l2 = match l1, l2 with List.equal (eq_located Name.equal) n1 n2 && constr_expr_eq e1 e2 | _ -> false -and constr_notation_substitution_eq (e1, el1, bl1) (e2, el2, bl2) = +and constr_notation_substitution_eq (e1, el1, b1, bl1) (e2, el2, b2, bl2) = List.equal constr_expr_eq e1 e2 && List.equal (List.equal constr_expr_eq) el1 el2 && + List.equal cases_pattern_expr_eq b1 b2 && List.equal (List.equal local_binder_eq) bl1 bl2 and instance_eq (x1,c1) (x2,c2) = @@ -268,7 +269,7 @@ let is_constructor id = let rec cases_pattern_fold_names f a pt = match CAst.(pt.v) with | CPatRecord l -> List.fold_left (fun acc (r, cp) -> cases_pattern_fold_names f acc cp) a l - | CPatAlias (pat,id) -> f id a + | CPatAlias (pat,(loc,na)) -> Name.fold_right f na (cases_pattern_fold_names f a pat) | CPatOr (patl) -> List.fold_left (cases_pattern_fold_names f) a patl | CPatCstr (_,patl1,patl2) -> @@ -324,7 +325,7 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function f (Name.fold_right g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b | CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b | CCast (a,CastCoerce) -> f n acc a - | CNotation (_,(l,ll,bll)) -> + | CNotation (_,(l,ll,bl,bll)) -> (* The following is an approximation: we don't know exactly if an ident is binding nor to which subterms bindings apply *) let acc = List.fold_left (f n) acc (l@List.flatten ll) in @@ -394,9 +395,9 @@ let map_constr_expr_with_binders g f e = CAst.map (function | CLetIn (na,a,t,b) -> CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (snd na) e) b) | CCast (a,c) -> CCast (f e a, Miscops.map_cast_type (f e) c) - | CNotation (n,(l,ll,bll)) -> + | CNotation (n,(l,ll,bl,bll)) -> (* This is an approximation because we don't know what binds what *) - CNotation (n,(List.map (f e) l,List.map (List.map (f e)) ll, + CNotation (n,(List.map (f e) l,List.map (List.map (f e)) ll, bl, List.map (fun bl -> snd (map_local_binders f g e bl)) bll)) | CGeneralization (b,a,c) -> CGeneralization (b,a,f e c) | CDelimiters (s,a) -> CDelimiters (s,f e a) @@ -455,9 +456,10 @@ let locs_of_notation ?loc locs ntn = | (ba,ea)::l -> if Int.equal pos ba then aux ea l else (pos,ba)::aux ea l in aux bl (List.sort (fun l1 l2 -> fst l1 - fst l2) locs) -let ntn_loc ?loc (args,argslist,binderslist) = +let ntn_loc ?loc (args,argslist,binders,binderslist) = locs_of_notation ?loc (List.map constr_loc (args@List.flatten argslist)@ + List.map cases_pattern_expr_loc binders@ List.map local_binders_loc binderslist) let patntn_loc ?loc (args,argslist) = @@ -564,12 +566,12 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function | CHole (None,Misctypes.IntroAnonymous,None) -> CPatAtom None | CLetIn ((loc,Name id),b,None,{ CAst.v = CRef (Ident (_,id'),None) }) when Id.equal id id' -> - CPatAlias (coerce_to_cases_pattern_expr b, id) + CPatAlias (coerce_to_cases_pattern_expr b, (loc,Name id)) | CApp ((None,p),args) when List.for_all (fun (_,e) -> e=None) args -> (mkAppPattern (coerce_to_cases_pattern_expr p) (List.map (fun (a,_) -> coerce_to_cases_pattern_expr a) args)).CAst.v | CAppExpl ((None,r,i),args) -> CPatCstr (r,Some (List.map coerce_to_cases_pattern_expr args),[]) - | CNotation (ntn,(c,cl,[])) -> + | CNotation (ntn,(c,cl,[],[])) -> CPatNotation (ntn,(List.map coerce_to_cases_pattern_expr c, List.map (List.map coerce_to_cases_pattern_expr) cl),[]) | CPrim p -> diff --git a/interp/constrextern.ml b/interp/constrextern.ml index ef20086e6..013f5713e 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -257,7 +257,7 @@ let insert_pat_delimiters ?loc p = function let insert_pat_alias ?loc p = function | Anonymous -> p - | Name id -> CAst.make ?loc @@ CPatAlias (p,id) + | Name _ as na -> CAst.make ?loc @@ CPatAlias (p,(loc,na)) (**********************************************************************) (* conversion of references *) @@ -323,34 +323,35 @@ let is_zero s = Int.equal (String.length s) i || (s.[i] == '0' && aux (i+1)) in aux 0 -let make_notation_gen loc ntn mknot mkprim destprim l = +let make_notation_gen loc ntn mknot mkprim destprim l bl = match ntn,List.map destprim l with (* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *) | "- _", [Some (Numeral (p,true))] when not (is_zero p) -> - mknot (loc,ntn,([mknot (loc,"( _ )",l)])) + assert (bl=[]); + mknot (loc,ntn,([mknot (loc,"( _ )",l,[])]),[]) | _ -> match decompose_notation_key ntn, l with | [Terminal "-"; Terminal x], [] when is_number x -> mkprim (loc, Numeral (x,false)) | [Terminal x], [] when is_number x -> mkprim (loc, Numeral (x,true)) - | _ -> mknot (loc,ntn,l) + | _ -> mknot (loc,ntn,l,bl) -let make_notation loc ntn (terms,termlists,binders as subst) = - if not (List.is_empty termlists) || not (List.is_empty binders) then +let make_notation loc ntn (terms,termlists,binders,binderlists as subst) = + if not (List.is_empty termlists) || not (List.is_empty binderlists) then CAst.make ?loc @@ CNotation (ntn,subst) else make_notation_gen loc ntn - (fun (loc,ntn,l) -> CAst.make ?loc @@ CNotation (ntn,(l,[],[]))) + (fun (loc,ntn,l,bl) -> CAst.make ?loc @@ CNotation (ntn,(l,[],bl,[]))) (fun (loc,p) -> CAst.make ?loc @@ CPrim p) - destPrim terms + destPrim terms binders let make_pat_notation ?loc ntn (terms,termlists as subst) args = if not (List.is_empty termlists) then (CAst.make ?loc @@ CPatNotation (ntn,subst,args)) else make_notation_gen loc ntn - (fun (loc,ntn,l) -> CAst.make ?loc @@ CPatNotation (ntn,(l,[]),args)) + (fun (loc,ntn,l,_) -> CAst.make ?loc @@ CPatNotation (ntn,(l,[]),args)) (fun (loc,p) -> CAst.make ?loc @@ CPatPrim p) - destPatPrim terms + destPatPrim terms [] let mkPat ?loc qid l = CAst.make ?loc @@ (* Normally irrelevant test with v8 syntax, but let's do it anyway *) @@ -1040,7 +1041,7 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function | _, None -> t, [], [], [] | _ -> raise No_match in (* Try matching ... *) - let terms,termlists,binders = + let terms,termlists,binders,binderlists = match_notation_constr !print_universes t pat in (* Try availability of interpretation ... *) let e = @@ -1061,11 +1062,15 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function List.map (fun (c,(scopt,scl)) -> List.map (extern true (scopt,scl@scopes') vars) c) termlists in + let bl = + List.map (fun (bl,(scopt,scl)) -> + extern_cases_pattern_in_scope (scopt,scl@scopes') vars bl) + binders in let bll = List.map (fun (bl,(scopt,scl)) -> pi3 (extern_local_binder (scopt,scl@scopes') vars bl)) - binders in - insert_delimiters (make_notation loc ntn (l,ll,bll)) key) + binderlists in + insert_delimiters (make_notation loc ntn (l,ll,bl,bll)) key) | SynDefRule kn -> let l = List.map (fun (c,(scopt,scl)) -> diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 000c7dab3..6a415a8e5 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -213,20 +213,20 @@ let expand_notation_string ntn n = (* This contracts the special case of "{ _ }" for sumbool, sumor notations *) (* Remark: expansion of squash at definition is done in metasyntax.ml *) -let contract_notation ntn (l,ll,bll) = +let contract_curly_brackets ntn (l,ll,bl,bll) = let ntn' = ref ntn in let rec contract_squash n = function | [] -> [] - | { CAst.v = CNotation ("{ _ }",([a],[],[])) } :: l -> + | { CAst.v = CNotation ("{ _ }",([a],[],[],[])) } :: l -> ntn' := expand_notation_string !ntn' n; contract_squash n (a::l) | a :: l -> a::contract_squash (n+1) l in let l = contract_squash 0 l in (* side effect; don't inline *) - !ntn',(l,ll,bll) + !ntn',(l,ll,bl,bll) -let contract_pat_notation ntn (l,ll) = +let contract_curly_brackets_pat ntn (l,ll) = let ntn' = ref ntn in let rec contract_squash n = function | [] -> [] @@ -286,14 +286,9 @@ let set_var_scope ?loc id istermvar (tmp_scope,subscopes as scopes) ntnvars = end in match typ with - | NtnInternTypeBinder -> + | Notation_term.NtnInternTypeOnlyBinder -> if istermvar then error_expect_binder_notation_type ?loc id - | NtnInternTypeConstr -> - (* We need sometimes to parse idents at a constr level for - factorization and we cannot enforce this constraint: - if not istermvar then error_expect_constr_notation_type loc id *) - () - | NtnInternTypeIdent -> () + | Notation_term.NtnInternTypeAny -> () with Not_found -> (* Not in a notation *) () @@ -302,6 +297,9 @@ let set_type_scope env = {env with tmp_scope = Notation.current_type_scope_name let reset_tmp_scope env = {env with tmp_scope = None} +let set_env_scopes env (scopt,subscopes) = + {env with tmp_scope = scopt; scopes = subscopes @ env.scopes} + let mkGProd ?loc (na,bk,t) body = DAst.make ?loc @@ GProd (na, bk, t, body) let mkGLambda ?loc (na,bk,t) body = DAst.make ?loc @@ GLambda (na, bk, t, body) @@ -451,7 +449,7 @@ let intern_cases_pattern_as_binder ?loc ntnvars env p = il,cp | _ -> assert false in - let env = List.fold_right (fun id env -> push_name_env Id.Map.empty (Variable,[],[],[]) env (None,Name id)) il env in + let env = List.fold_right (fun (loc,id) env -> push_name_env ntnvars (Variable,[],[],[]) env (loc,Name id)) il env in let na = alias_of_pat cp in let ienv = Name.fold_right Id.Set.remove na env.ids in let id = Namegen.next_name_away_with_default "pat" (alias_of_pat cp) ienv in @@ -476,7 +474,7 @@ let intern_local_binder_aux ?(global_level=false) intern ntnvars (env,bl) = func let bk = Default Explicit in let _, bl' = intern_assumption intern ntnvars env [na] bk tyc in let _,(_,bk,t) = List.hd bl' in - (env, (DAst.make ?loc @@ GLocalPattern((cp,il),id,bk,t)) :: bl) + (env, (DAst.make ?loc @@ GLocalPattern((cp,List.map snd il),id,bk,t)) :: bl) let intern_generalization intern env ntnvars loc bk ak c = let c = intern {env with unb = true} c in @@ -532,7 +530,7 @@ let option_mem_assoc id = function | Some (id',c) -> Id.equal id id' | None -> false -let find_fresh_name renaming (terms,termlists,binders) avoid id = +let find_fresh_name renaming (terms,termlists,binders,binderlists) avoid id = let fold1 _ (c, _) accu = Id.Set.union (free_vars_of_constr_expr c) accu in let fold2 _ (l, _) accu = let fold accu c = Id.Set.union (free_vars_of_constr_expr c) accu in @@ -545,22 +543,27 @@ let find_fresh_name renaming (terms,termlists,binders) avoid id = (* TODO binders *) next_ident_away_from id (fun id -> Id.Set.mem id fvs3) -let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function +let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) = function | Anonymous -> (renaming,env), None, Anonymous | Name id -> try (* We instantiate binder name with patterns which may be parsed as terms *) let pat = coerce_to_cases_pattern_expr (fst (Id.Map.find id terms)) in - let env,((pat,ids),id),na = intern_cases_pattern_as_binder ?loc:pat.CAst.loc Id.Map.empty env pat in + let env,((pat,ids),id),na = intern_pat ntnvars env pat in let pat, na = match DAst.get pat with | PatVar na -> None, na - | _ -> - Some ((ids,pat),id), snd na in + | _ -> Some ((List.map snd ids,pat),id), snd na in (renaming,env), pat, na with Not_found -> try (* Trying to associate a pattern *) - raise Not_found + let pat,scopes = Id.Map.find id binders in + let env = set_env_scopes env scopes in + let env,((pat,ids),id),na = intern_pat ntnvars env pat in + let pat, na = match DAst.get pat with + | PatVar na -> None, na + | _ -> Some ((List.map snd ids,pat),id), snd na in + (renaming,env), pat, na with Not_found -> (* Binders not bound in the notation do not capture variables *) (* outside the notation (i.e. in the substitution) *) @@ -612,8 +615,8 @@ let flatten_binders bl = | a -> [a] in List.flatten (List.map dispatch bl) -let instantiate_notation_constr loc intern ntnvars subst infos c = - let (terms,termlists,binders) = subst in +let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = + let (terms,termlists,binders,binderlists) = subst in (* when called while defining a notation, avoid capturing the private binders of the expression by variables bound by the notation (see #3892) *) let avoid = Id.Map.domain ntnvars in @@ -644,7 +647,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = (if revert then List.rev l else l),scopes with Not_found -> try - let (bl,(scopt,subscopes)) = Id.Map.find x binders in + let (bl,(scopt,subscopes)) = Id.Map.find x binderlists in let env,bl' = List.fold_left (intern_local_binder_aux intern ntnvars) (env,[]) bl in terms_of_binders (if revert then bl' else List.rev bl'),(None,[]) with Not_found -> @@ -671,14 +674,21 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = let gc = intern nenv c in (gc, Some c) in - let bindings = Id.Map.map mk_env terms in + let mk_env' (c, (tmp_scope, subscopes)) = + let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in + let _,((pat,_),_),_ = intern_pat ntnvars nenv c in + (glob_constr_of_cases_pattern pat, None) + in + let terms = Id.Map.map mk_env terms in + let binders = Id.Map.map mk_env' binders in + let bindings = Id.Map.fold Id.Map.add terms binders in Some (Genintern.generic_substitute_notation bindings arg) in DAst.make ?loc @@ GHole (knd, naming, arg) | NBinderList (x,y,iter,terminator,revert) -> (try (* All elements of the list are in scopes (scopt,subscopes) *) - let (bl,(scopt,subscopes)) = Id.Map.find x binders in + let (bl,(scopt,subscopes)) = Id.Map.find x binderlists in (* We flatten binders so that we can interpret them at substitution time *) let bl = flatten_binders bl in let bl = if revert then List.rev bl else bl in @@ -698,17 +708,17 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = (* Two special cases to keep binder name synchronous with BinderType *) | NProd (na,NHole(Evar_kinds.BinderType na',naming,arg),c') when Name.equal na na' -> - let subinfos,pat,na = traverse_binder subst avoid subinfos na in + let subinfos,pat,na = traverse_binder intern_pat ntnvars subst avoid subinfos na in let ty = DAst.make ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in DAst.make ?loc @@ GProd (na,Explicit,ty,Option.fold_right apply_cases_pattern pat (aux subst' subinfos c')) | NLambda (na,NHole(Evar_kinds.BinderType na',naming,arg),c') when Name.equal na na' -> - let subinfos,pat,na = traverse_binder subst avoid subinfos na in + let subinfos,pat,na = traverse_binder intern_pat ntnvars subst avoid subinfos na in let ty = DAst.make ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in DAst.make ?loc @@ GLambda (na,Explicit,ty,Option.fold_right apply_cases_pattern pat (aux subst' subinfos c')) | t -> glob_constr_of_notation_constr_with_binders ?loc - (traverse_binder subst avoid) (aux subst') subinfos t + (traverse_binder intern_pat ntnvars subst avoid) (aux subst') subinfos t and subst_var (terms, binderopt, _terminopt) (renaming, env) id = (* subst remembers the delimiters stack in the interpretation *) (* of the notations *) @@ -718,6 +728,15 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = scopes = subscopes @ env.scopes} a with Not_found -> try + let pat,scopes = Id.Map.find id binders in + let env = set_env_scopes env scopes in + (* We deactivate the check on hidden parameters *) + (* since we are only interested in the pattern as a term *) + let env = reset_hidden_inductive_implicit_test env in + let env,((pat,ids),id),na = intern_pat ntnvars env pat in + glob_constr_of_cases_pattern pat + with Not_found -> + try match binderopt with | Some (x,binder) when Id.equal x id -> let terms = terms_of_binders [binder] in @@ -733,27 +752,71 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = GVar id) in aux (terms,None,None) infos c -let split_by_type ids = - List.fold_right (fun (x,(scl,typ)) (l1,l2,l3) -> +(* Turning substitution coming from parsing and based on production + into a substitution for interpretation and based on binding/constr + distinction *) + +let split_by_type ids subst = + let bind id scl l s = + match l with + | [] -> assert false + | a::l -> l, Id.Map.add id (a,scl) s in + let (terms,termlists,binders,binderlists),subst = + List.fold_left (fun ((terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')) (id,(scl,typ)) -> + match typ with + | NtnTypeConstr -> + let terms,terms' = bind id scl terms terms' in + (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') + | NtnTypeBinder true -> + let a,terms = match terms with a::terms -> a,terms | _ -> assert false in + let binders' = Id.Map.add id (coerce_to_cases_pattern_expr a,scl) binders' in + (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') + | NtnTypeBinder false -> + let binders,binders' = bind id scl binders binders' in + (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') + | NtnTypeConstrList -> + let termlists,termlists' = bind id scl termlists termlists' in + (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') + | NtnTypeBinderList -> + let binderlists,binderlists' = bind id scl binderlists binderlists' in + (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')) + (subst,(Id.Map.empty,Id.Map.empty,Id.Map.empty,Id.Map.empty)) ids in + assert (terms = [] && termlists = [] && binders = [] && binderlists = []); + subst + +let split_by_type_pat ?loc ids subst = + let bind id scl l s = + match l with + | [] -> assert false + | a::l -> l, Id.Map.add id (a,scl) s in + let (terms,termlists),subst = + List.fold_left (fun ((terms,termlists),(terms',termlists')) (id,(scl,typ)) -> match typ with - | NtnTypeConstr | NtnTypeOnlyBinder -> ((x,scl)::l1,l2,l3) - | NtnTypeConstrList -> (l1,(x,scl)::l2,l3) - | NtnTypeBinderList -> (l1,l2,(x,scl)::l3)) ids ([],[],[]) + | NtnTypeConstr | NtnTypeBinder _ -> + let terms,terms' = bind id scl terms terms' in + (terms,termlists),(terms',termlists') + | NtnTypeConstrList -> + let termlists,termlists' = bind id scl termlists termlists' in + (terms,termlists),(terms',termlists') + | NtnTypeBinderList -> error_invalid_pattern_notation ?loc ()) + (subst,(Id.Map.empty,Id.Map.empty)) ids in + assert (terms = [] && termlists = []); + subst let make_subst ids l = let fold accu (id, scl) a = Id.Map.add id (a, scl) accu in List.fold_left2 fold Id.Map.empty ids l let intern_notation intern env ntnvars loc ntn fullargs = - let ntn,(args,argslist,bll as fullargs) = contract_notation ntn fullargs in + (* Adjust to parsing of { } *) + let ntn,fullargs = contract_curly_brackets ntn fullargs in + (* Recover interpretation { } *) let ((ids,c),df) = interp_notation ?loc ntn (env.tmp_scope,env.scopes) in Dumpglob.dump_notation_location (ntn_loc ?loc fullargs ntn) ntn df; - let ids,idsl,idsbl = split_by_type ids in - let terms = make_subst ids args in - let termlists = make_subst idsl argslist in - let binders = make_subst idsbl bll in - instantiate_notation_constr loc intern ntnvars - (terms, termlists, binders) (Id.Map.empty, env) c + (* Dispatch parsing substitution to an interpretation substitution *) + let subst = split_by_type ids fullargs in + (* Instantiate the notation *) + instantiate_notation_constr loc intern intern_cases_pattern_as_binder ntnvars subst (Id.Map.empty, env) c (**********************************************************************) (* Discriminating between bound variables and global references *) @@ -883,10 +946,10 @@ let intern_qualid loc qid intern env ntnvars us args = let args1,args2 = List.chop nids args in check_no_explicitation args1; let terms = make_subst ids (List.map fst args1) in - let subst = (terms, Id.Map.empty, Id.Map.empty) in + let subst = (terms, Id.Map.empty, Id.Map.empty, Id.Map.empty) in let infos = (Id.Map.empty, env) in let projapp = match c with NRef _ -> true | _ -> false in - let c = instantiate_notation_constr loc intern ntnvars subst infos c in + let c = instantiate_notation_constr loc intern intern_cases_pattern_as_binder ntnvars subst infos c in let loc = c.CAst.loc in let err () = user_err ?loc (str "Notation " ++ pr_qualid qid @@ -953,11 +1016,11 @@ let interp_reference vars r = (** Private internalization patterns *) type 'a raw_cases_pattern_expr_r = - | RCPatAlias of 'a raw_cases_pattern_expr * Id.t + | RCPatAlias of 'a raw_cases_pattern_expr * Name.t Loc.located | RCPatCstr of Globnames.global_reference * 'a raw_cases_pattern_expr list * 'a raw_cases_pattern_expr list (** [RCPatCstr (loc, c, l1, l2)] represents ((@c l1) l2) *) - | RCPatAtom of (Id.t * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option + | RCPatAtom of (Id.t Loc.located * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option | RCPatOr of 'a raw_cases_pattern_expr list and 'a raw_cases_pattern_expr = ('a raw_cases_pattern_expr_r, 'a) DAst.t @@ -1017,7 +1080,7 @@ let check_number_of_pattern loc n l = if not (Int.equal n p) then raise (InternalizationError (loc,BadPatternsNumber (n,p))) let check_or_pat_variables loc ids idsl = - if List.exists (fun ids' -> not (List.eq_set Id.equal ids ids')) idsl then + if List.exists (fun ids' -> not (List.eq_set (fun (loc,id) (_,id') -> Id.equal id id') ids ids')) idsl then user_err ?loc (str "The components of this disjunctive pattern must bind the same variables.") @@ -1256,7 +1319,7 @@ let sort_fields ~complete loc fields completer = (** {6 Manage multiple aliases} *) type alias = { - alias_ids : Id.t list; + alias_ids : Id.t Loc.located list; alias_map : Id.t Id.Map.t; } @@ -1267,17 +1330,20 @@ let empty_alias = { (* [merge_aliases] returns the sets of all aliases encountered at this point and a substitution mapping extra aliases to the first one *) -let merge_aliases aliases id = - let alias_ids = aliases.alias_ids @ [id] in +let merge_aliases aliases (loc,na) = + match na with + | Anonymous -> aliases + | Name id -> + let alias_ids = aliases.alias_ids @ [loc,id] in let alias_map = match aliases.alias_ids with | [] -> aliases.alias_map - | id' :: _ -> Id.Map.add id id' aliases.alias_map + | (_,id') :: _ -> Id.Map.add id id' aliases.alias_map in { alias_ids; alias_map; } let alias_of als = match als.alias_ids with | [] -> Anonymous -| id :: _ -> Name id +| (_,id) :: _ -> Name id (** {6 Expanding notations } @@ -1295,6 +1361,8 @@ let is_zero s = let merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2 let product_of_cases_patterns aliases idspl = + (* each [pl] is a disjunction of patterns over common identifiers [ids] *) + (* We stepwise build a disjunction of patterns [ptaill] over common [ids'] *) List.fold_right (fun (ids,pl) (ids',ptaill) -> (ids @ ids', (* Cartesian prod of the or-pats for the nth arg and the tail args *) @@ -1305,7 +1373,7 @@ let product_of_cases_patterns aliases idspl = let rec subst_pat_iterator y t = DAst.(map (function | RCPatAtom id as p -> - begin match id with Some (x,_) when Id.equal x y -> DAst.get t | _ -> p end + begin match id with Some ((_,x),_) when Id.equal x y -> DAst.get t | _ -> p end | RCPatCstr (id,l1,l2) -> RCPatCstr (id,List.map (subst_pat_iterator y t) l1, List.map (subst_pat_iterator y t) l2) @@ -1335,7 +1403,7 @@ let drop_notations_pattern looked_for genv = in (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *) let rec rcp_of_glob scopes x = DAst.(map (function - | GVar id -> RCPatAtom (Some (id,scopes)) + | GVar id -> RCPatAtom (Some ((x.CAst.loc,id),scopes)) | GHole (_,_,_) -> RCPatAtom (None) | GRef (g,_) -> RCPatCstr (g,[],[]) | GApp (r, l) -> @@ -1426,24 +1494,22 @@ let drop_notations_pattern looked_for genv = rcp_of_glob scopes pat | CPatNotation ("( _ )",([a],[]),[]) -> in_pat top scopes a - | CPatNotation (ntn, fullargs,extrargs) -> - let ntn,(args,argsl as fullargs) = contract_pat_notation ntn fullargs in + | CPatNotation (ntn,fullargs,extrargs) -> + let ntn,(terms,termlists) = contract_curly_brackets_pat ntn fullargs in let ((ids',c),df) = Notation.interp_notation ?loc ntn scopes in - let (ids',idsl',_) = split_by_type ids' in + let (terms,termlists) = split_by_type_pat ?loc ids' (terms,termlists) in Dumpglob.dump_notation_location (patntn_loc ?loc fullargs ntn) ntn df; - let substlist = make_subst idsl' argsl in - let subst = make_subst ids' args in - in_not top loc scopes (subst,substlist) extrargs c + in_not top loc scopes (terms,termlists) extrargs c | CPatDelimiters (key, e) -> in_pat top (None,find_delimiters_scope ?loc key::snd scopes) e | CPatPrim p -> let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (test_kind false) p scopes in rcp_of_glob scopes pat - | CPatAtom Some id -> + | CPatAtom (Some id) -> begin match drop_syndef top scopes id [] with | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr (a, b, c) - | None -> DAst.make ?loc @@ RCPatAtom (Some (find_pattern_variable id,scopes)) + | None -> DAst.make ?loc @@ RCPatAtom (Some ((loc,find_pattern_variable id),scopes)) end | CPatAtom None -> DAst.make ?loc @@ RCPatAtom None | CPatOr pl -> DAst.make ?loc @@ RCPatOr (List.map (in_pat top scopes) pl) @@ -1473,7 +1539,7 @@ let drop_notations_pattern looked_for genv = let (a,(scopt,subscopes)) = Id.Map.find id subst in in_pat top (scopt,subscopes@snd scopes) a with Not_found -> - if Id.equal id ldots_var then DAst.make ?loc @@ RCPatAtom (Some (id,scopes)) else + if Id.equal id ldots_var then DAst.make ?loc @@ RCPatAtom (Some ((loc,id),scopes)) else anomaly (str "Unbound pattern notation variable: " ++ Id.print id ++ str ".") end | NRef g -> @@ -1530,8 +1596,8 @@ let rec intern_pat genv ntnvars aliases pat = let with_letin, pl2 = add_implicits_check_constructor_length genv loc c (List.length idslpl1 + List.length expl_pl) pl in intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl2) - | RCPatAtom (Some (id,scopes)) -> - let aliases = merge_aliases aliases id in + | RCPatAtom (Some ((loc,id),scopes)) -> + let aliases = merge_aliases aliases (loc,Name id) in set_var_scope ?loc id false scopes ntnvars; (aliases.alias_ids,[aliases.alias_map, DAst.make ?loc @@ PatVar (alias_of aliases)]) (* TO CHECK: aura-t-on id? *) | RCPatAtom (None) -> @@ -1565,10 +1631,9 @@ let intern_ind_pattern genv ntnvars scopes pat = let c = (function IndRef ind -> ind | _ -> error_bad_inductive_type ?loc) head in let with_letin, pl2 = add_implicits_check_ind_length genv loc c (List.length expl_pl) pl in - let idslpl1 = List.rev_map (intern_pat genv ntnvars empty_alias) expl_pl in - let idslpl2 = List.map (intern_pat genv ntnvars empty_alias) pl2 in + let idslpl = List.map (intern_pat genv ntnvars empty_alias) (expl_pl@pl2) in (with_letin, - match product_of_cases_patterns empty_alias (List.rev_append idslpl1 idslpl2) with + match product_of_cases_patterns empty_alias idslpl with | _,[_,pl] -> (c,chop_params_pattern loc c pl with_letin) | _ -> error_bad_inductive_type ?loc) | x -> error_bad_inductive_type ?loc @@ -1740,10 +1805,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = DAst.make ?loc @@ GLetIn (snd na, inc1, int, intern (push_name_env ntnvars (impls_term_list inc1) env na) c2) - | CNotation ("- _", ([a],[],[])) when is_non_zero a -> + | CNotation ("- _", ([a],[],[],[])) when is_non_zero a -> let p = match a.CAst.v with CPrim (Numeral (p, _)) -> p | _ -> assert false in intern env (CAst.make ?loc @@ CPrim (Numeral (p,false))) - | CNotation ("( _ )",([a],[],[])) -> intern env a + | CNotation ("( _ )",([a],[],[],[])) -> intern env a | CNotation (ntn,args) -> intern_notation intern env ntnvars loc ntn args | CGeneralization (b,a,c) -> @@ -1775,8 +1840,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | CRef (ref,us) -> intern_applied_reference intern env (Environ.named_context globalenv) lvar us args ref - | CNotation (ntn,([],[],[])) -> - let c = intern_notation intern env ntnvars loc ntn ([],[],[]) in + | CNotation (ntn,([],[],[],[])) -> + let c = intern_notation intern env ntnvars loc ntn ([],[],[],[]) in let x, impl, scopes, l = find_appl_head_data c in (x,impl,scopes,l), args | _ -> (intern env f,[],[],[]), args in @@ -1878,6 +1943,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | None -> None | Some gen -> let (ltacvars, ntnvars) = lvar in + (* Preventively declare notation variables in ltac as non-bindings *) + Id.Map.iter (fun x (isonlybinding,_,_) -> isonlybinding := false) ntnvars; let ntnvars = Id.Map.domain ntnvars in let extra = ltacvars.ltac_extra in let lvars = Id.Set.union ltacvars.ltac_bound ltacvars.ltac_vars in @@ -1946,6 +2013,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = and intern_eqn n env (loc,(lhs,rhs)) = let eqn_ids,pll = intern_disjunctive_multiple_pattern env loc n lhs in (* Linearity implies the order in ids is irrelevant *) + let eqn_ids = List.map snd eqn_ids in check_linearity lhs eqn_ids; let env_ids = List.fold_right Id.Set.add eqn_ids env.ids in List.map (fun (asubst,pl) -> @@ -2193,7 +2261,7 @@ let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = let out_scope = function None -> None,[] | Some (a,l) -> a,l in let unused = match reversible with NonInjective ids -> ids | _ -> [] in let vars = Id.Map.mapi (fun id (isonlybinding, sc, typ) -> - (!isonlybinding && not (List.mem_f Id.equal id unused), out_scope !sc, typ)) vl in + (!isonlybinding && not (List.mem_f Id.equal id unused), out_scope !sc)) vl in (* Returns [a] and the ordered list of variables with their scopes *) vars, a, reversible diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 87b587b71..f09b17a49 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -87,7 +87,7 @@ val intern_gen : typing_constraint -> env -> constr_expr -> glob_constr val intern_pattern : env -> cases_pattern_expr -> - Id.t list * (Id.t Id.Map.t * cases_pattern) list + Id.t Loc.located list * (Id.t Id.Map.t * cases_pattern) list val intern_context : bool -> env -> internalization_env -> local_binder_expr list -> internalization_env * glob_decl list @@ -184,8 +184,7 @@ val global_reference_in_absolute_module : DirPath.t -> Id.t -> Globnames.global_ guaranteed to have the same domain as the input one. *) val interp_notation_constr : env -> ?impls:internalization_env -> notation_interp_env -> constr_expr -> - (bool * subscopes * notation_var_internalization_type) Id.Map.t * - notation_constr * reversibility_status + (bool * subscopes) Id.Map.t * notation_constr * reversibility_status (** Globalization options *) val parsing_explicit : bool ref diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 519f2480b..a838d7106 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -93,8 +93,8 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = in let rec aux bdvars l c = match CAst.(c.v) with | CRef (Ident (loc,id),_) -> found loc id bdvars l - | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef (Ident (_, id),_) } :: _, [], [])) when not (Id.Set.mem id bdvars) -> - Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c + | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef (Ident (_, id),_) } :: _, [], [], [])) when not (Id.Set.mem id bdvars) -> + Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c in aux bound l c diff --git a/interp/notation.ml b/interp/notation.ml index 31f16e1a9..e6186e08c 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -82,18 +82,31 @@ let parenRelation_eq t1 t2 = match t1, t2 with | Prec l1, Prec l2 -> Int.equal l1 l2 | _ -> false -let notation_var_internalization_type_eq v1 v2 = match v1, v2 with -| NtnInternTypeConstr, NtnInternTypeConstr -> true -| NtnInternTypeBinder, NtnInternTypeBinder -> true -| NtnInternTypeIdent, NtnInternTypeIdent -> true -| (NtnInternTypeConstr | NtnInternTypeBinder | NtnInternTypeIdent), _ -> false +open Extend + +let production_level_eq l1 l2 = true (* (l1 = l2) *) + +let production_position_eq pp1 pp2 = true (* pp1 = pp2 *) (* match pp1, pp2 with +| NextLevel, NextLevel -> true +| NumLevel n1, NumLevel n2 -> Int.equal n1 n2 +| (NextLevel | NumLevel _), _ -> false *) + +let constr_entry_key_eq v1 v2 = match v1, v2 with +| ETName, ETName -> true +| ETReference, ETReference -> true +| ETBigint, ETBigint -> true +| ETBinder b1, ETBinder b2 -> b1 == b2 +| ETConstr (n1,pp1), ETConstr (n2,pp2) -> production_level_eq n1 n2 && production_position_eq pp1 pp2 +| ETPattern n1, ETPattern n2 -> Int.equal n1 n2 +| ETOther (s1,s1'), ETOther (s2,s2') -> String.equal s1 s2 && String.equal s1' s2' +| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _), _ -> false let level_eq (l1, t1, u1) (l2, t2, u2) = let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in Int.equal l1 l2 && List.equal tolerability_eq t1 t2 - && List.equal notation_var_internalization_type_eq u1 u2 + && List.equal constr_entry_key_eq u1 u2 let declare_scope scope = try let _ = String.Map.find scope !scope_map in () @@ -611,10 +624,10 @@ let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2 let ntpe_eq t1 t2 = match t1, t2 with | NtnTypeConstr, NtnTypeConstr -> true -| NtnTypeOnlyBinder, NtnTypeOnlyBinder -> true +| NtnTypeBinder b1, NtnTypeBinder b2 -> b1 = (b2:bool) | NtnTypeConstrList, NtnTypeConstrList -> true | NtnTypeBinderList, NtnTypeBinderList -> true -| (NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList), _ -> false +| (NtnTypeConstr | NtnTypeBinder _ | NtnTypeConstrList | NtnTypeBinderList), _ -> false let var_attributes_eq (_, (sc1, tp1)) (_, (sc2, tp2)) = pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 && diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 3a3d4ffa8..ec568823e 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -472,17 +472,16 @@ let check_variables_and_reversibility nenv str " position as part of a recursive pattern.") in let check_type x typ = match typ with - | NtnInternTypeConstr -> + | NtnInternTypeAny -> begin try check_pair "term" x (Id.Map.find x recvars) foundrec with Not_found -> check_bound x end - | NtnInternTypeBinder -> + | NtnInternTypeOnlyBinder -> begin try check_pair "binding" x (Id.Map.find x recvars) foundrecbinding with Not_found -> check_bound x - end - | NtnInternTypeIdent -> check_bound x in + end in Id.Map.iter check_type vars; List.rev !injective @@ -665,7 +664,7 @@ let is_term_meta id metas = with Not_found -> false let is_onlybinding_meta id metas = - try match Id.List.assoc id metas with _,NtnTypeOnlyBinder -> true | _ -> false + try match Id.List.assoc id metas with _,NtnTypeBinder _ -> true | _ -> false with Not_found -> false let is_bindinglist_meta id metas = @@ -885,8 +884,11 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma) (* TODO: look at the consequences for alp *) alp, add_env alp sigma var (DAst.make @@ GVar id) +let force_cases_pattern c = + DAst.make ?loc:c.CAst.loc (DAst.get c) + let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) var c = - let pat = try cases_pattern_of_glob_constr Anonymous c with Not_found -> raise No_match in + let pat = try force_cases_pattern (cases_pattern_of_glob_constr Anonymous c) with Not_found -> raise No_match in try (* If already bound to a binder, unify the term and the binder *) let pat' = Id.List.assoc var binders in @@ -961,8 +963,10 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with | (Anonymous,Anonymous) -> alp,sigma | _ -> raise No_match -let rec match_cases_pattern_binders metas acc pat1 pat2 = +let rec match_cases_pattern_binders metas (alp,sigma as acc) pat1 pat2 = match DAst.get pat1, DAst.get pat2 with + | _, PatVar (Name id2) when is_onlybinding_meta id2 metas -> + bind_binding_env alp sigma id2 pat1 | PatVar na1, PatVar na2 -> match_names metas acc na1 na2 | PatCstr (c1,patl1,na1), PatCstr (c2,patl2,na2) when eq_constructor c1 c2 && Int.equal (List.length patl1) (List.length patl2) -> @@ -1265,26 +1269,24 @@ and match_equations u alp metas sigma (_,(_,patl1,rhs1)) (patl2,rhs2) = let match_notation_constr u c (metas,pat) = let terms,termlists,binders,binderlists = match_ false u ([],[]) metas ([],[],[],[]) c pat in - (* Reorder canonically the substitution *) - let find_binder x = - try glob_constr_of_cases_pattern (Id.List.assoc x binders) - with Not_found -> - (* Happens for binders bound to Anonymous *) - (* Find a better way to propagate Anonymous... *) - DAst.make @@GVar x in - List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders') -> + (* Turning substitution based on binding/constr distinction into a + substitution based on entry productions *) + List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders',binderlists') -> match typ with | NtnTypeConstr -> let term = try Id.List.assoc x terms with Not_found -> raise No_match in - ((term, scl)::terms',termlists',binders') - | NtnTypeOnlyBinder -> - ((find_binder x, scl)::terms',termlists',binders') + ((term, scl)::terms',termlists',binders',binderlists') + | NtnTypeBinder true -> + let v = glob_constr_of_cases_pattern (Id.List.assoc x binders) in + ((v,scl)::terms',termlists',binders',binderlists') + | NtnTypeBinder false -> + (terms',termlists',(Id.List.assoc x binders,scl)::binders',binderlists') | NtnTypeConstrList -> - (terms',(Id.List.assoc x termlists,scl)::termlists',binders') + (terms',(Id.List.assoc x termlists,scl)::termlists',binders',binderlists') | NtnTypeBinderList -> let bl = try Id.List.assoc x binderlists with Not_found -> raise No_match in - (terms',termlists',(bl, scl)::binders')) - metas ([],[],[]) + (terms',termlists',binders',(bl, scl)::binderlists')) + metas ([],[],[],[]) (* Matching cases pattern *) @@ -1356,7 +1358,7 @@ let reorder_canonically_substitution terms termlists metas = List.fold_right (fun (x,(scl,typ)) (terms',termlists') -> match typ with | NtnTypeConstr -> ((Id.List.assoc x terms, scl)::terms',termlists') - | NtnTypeOnlyBinder -> assert false + | NtnTypeBinder _ -> assert false | NtnTypeConstrList -> (terms',(Id.List.assoc x termlists,scl)::termlists') | NtnTypeBinderList -> assert false) metas ([],[]) diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 74be6f512..1a2dfc9ca 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -52,6 +52,7 @@ exception No_match val match_notation_constr : bool -> 'a glob_constr_g -> interpretation -> ('a glob_constr_g * subscopes) list * ('a glob_constr_g list * subscopes) list * + ('a cases_pattern_g * subscopes) list * ('a extended_glob_local_binder_g list * subscopes) list val match_notation_constr_cases_pattern : diff --git a/interp/ppextend.ml b/interp/ppextend.ml index ce19dd8a9..606196fcd 100644 --- a/interp/ppextend.ml +++ b/interp/ppextend.ml @@ -33,6 +33,7 @@ let ppcmd_of_cut = function type unparsing = | UnpMetaVar of int * parenRelation + | UnpBinderMetaVar of int * parenRelation | UnpListMetaVar of int * parenRelation * unparsing list | UnpBinderListMetaVar of int * bool * unparsing list | UnpTerminal of string diff --git a/interp/ppextend.mli b/interp/ppextend.mli index 7b62a2074..77823e32a 100644 --- a/interp/ppextend.mli +++ b/interp/ppextend.mli @@ -26,6 +26,7 @@ val ppcmd_of_cut : ppcut -> Pp.t type unparsing = | UnpMetaVar of int * parenRelation + | UnpBinderMetaVar of int * parenRelation | UnpListMetaVar of int * parenRelation * unparsing list | UnpBinderListMetaVar of int * bool * unparsing list | UnpTerminal of string |