diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-02 15:12:05 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-02 15:25:14 +0200 |
commit | b6b98a67c65d7aeeeeca12d1ccb9d55b654c554d (patch) | |
tree | 2a90fbdf676aea46265fc5dd45ed220a47d9ff82 /interp | |
parent | 4648732544f43ad87266f33967995b29d2b8338b (diff) |
A slight phase of documentation and uniformization of names of
functions about interpretation, internalization, externalization of
notations.
Main syntactic changes:
- subst_aconstr_in_glob_constr -> instantiate_notation_constr
(because aconstr has been renamed to notation_constr long time ago)
- extern_symbol -> extern_notation
(because symbol.ml has been renamed to notation.ml long time ago)
- documentation of notations_ops.mli
Main semantic changes:
- Notation_ops.eq_glob_constr which was partial eq disappears: use
glob_constr_eq instead
- In particular, this impacts a change on funind which now use the
(fully implemented) glob_constr_eq
Somehow, instantiate_notation_constr should be in notation_ops.ml for
symmetry with match_notation_constr but it is bit painful to do.
Diffstat (limited to 'interp')
-rw-r--r-- | interp/constrextern.ml | 26 | ||||
-rw-r--r-- | interp/constrintern.ml | 6 | ||||
-rw-r--r-- | interp/notation_ops.ml | 186 | ||||
-rw-r--r-- | interp/notation_ops.mli | 32 |
4 files changed, 128 insertions, 122 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 592f59333..e5ccb76b4 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -175,6 +175,10 @@ let add_patt_for_params ind l = if !Flags.in_debugger then l else Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CPatAtom (Loc.ghost,None)) l +let add_cpatt_for_params ind l = + if !Flags.in_debugger then l else + Util.List.addn (Inductiveops.inductive_nparamdecls ind) (PatVar (Loc.ghost,Anonymous)) l + let drop_implicits_in_patt cst nb_expl args = let impl_st = (implicits_of_global cst) in let impl_data = extract_impargs_data impl_st in @@ -299,7 +303,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = with No_match -> try if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_symbol_pattern scopes vars pat + extern_notation_pattern scopes vars pat (uninterp_cases_pattern_notations pat) with No_match -> match pat with @@ -382,7 +386,7 @@ and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args)) in assert (List.is_empty substlist); mkPat loc qid (List.rev_append l1 l2') -and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function +and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function | [] -> raise No_match | (keyrule,pat,n as _rule)::rules -> try @@ -395,9 +399,9 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function | PatVar (loc,Anonymous) -> CPatAtom (loc, None) | PatVar (loc,Name id) -> CPatAtom (loc, Some (Ident (loc,id))) with - No_match -> extern_symbol_pattern allscopes vars t rules + No_match -> extern_notation_pattern allscopes vars t rules -let rec extern_symbol_ind_pattern allscopes vars ind args = function +let rec extern_notation_ind_pattern allscopes vars ind args = function | [] -> raise No_match | (keyrule,pat,n as _rule)::rules -> try @@ -405,7 +409,7 @@ let rec extern_symbol_ind_pattern allscopes vars ind args = function apply_notation_to_pattern Loc.ghost (IndRef ind) (match_notation_constr_ind_pattern ind args pat) allscopes vars keyrule with - No_match -> extern_symbol_ind_pattern allscopes vars ind args rules + No_match -> extern_notation_ind_pattern allscopes vars ind args rules let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = (* pboutill: There are letins in pat which is incompatible with notations and @@ -425,7 +429,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = with No_match -> try if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_symbol_ind_pattern scopes vars ind args + extern_notation_ind_pattern scopes vars ind args (uninterp_ind_pattern_notations ind) with No_match -> let c = extern_reference Loc.ghost vars (IndRef ind) in @@ -622,7 +626,7 @@ let rec extern inctx scopes vars r = try let r'' = flatten_application r' in if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_symbol scopes vars r'' (uninterp_notations r'') + extern_notation scopes vars r'' (uninterp_notations r'') with No_match -> match r' with | GRef (loc,ref,us) -> extern_global loc (select_stronger_impargs (implicits_of_global ref)) @@ -730,9 +734,7 @@ let rec extern inctx scopes vars r = na', Option.map (fun (loc,ind,nal) -> let args = List.map (fun x -> PatVar (Loc.ghost, x)) nal in - let fullargs = - if !Flags.in_debugger then args else - Notation_ops.add_patterns_for_params ind args in + let fullargs = add_cpatt_for_params ind args in extern_ind_pattern_in_scope scopes vars ind fullargs ) x)) tml @@ -842,7 +844,7 @@ and extern_eqn inctx scopes vars (loc,ids,pl,c) = (loc,[loc,List.map (extern_cases_pattern_in_scope scopes vars) pl], extern inctx scopes vars c) -and extern_symbol (tmp_scope,scopes as allscopes) vars t = function +and extern_notation (tmp_scope,scopes as allscopes) vars t = function | [] -> raise No_match | (keyrule,pat,n as _rule)::rules -> let loc = Glob_ops.loc_of_glob_constr t in @@ -917,7 +919,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function let args = extern_args (extern true) scopes vars args argsscopes in explicitize loc false argsimpls (None,e) args with - No_match -> extern_symbol allscopes vars t rules + No_match -> extern_notation allscopes vars t rules and extern_recursion_order scopes vars = function GStructRec -> CStructRec diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 4a451634d..50252a368 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -526,7 +526,7 @@ let rec subst_iterator y t = function | GVar (_,id) as x -> if Id.equal id y then t else x | x -> map_glob_constr (subst_iterator y t) x -let subst_aconstr_in_glob_constr loc intern (_,ntnvars as lvar) subst infos c = +let instantiate_notation_constr loc intern (_,ntnvars as lvar) subst infos c = let (terms,termlists,binders) = subst in (* when called while defining a notation, avoid capturing the private binders of the expression by variables bound by the notation (see #3892) *) @@ -649,7 +649,7 @@ let intern_notation intern env lvar loc ntn fullargs = let terms = make_subst ids args in let termlists = make_subst idsl argslist in let binders = make_subst idsbl bll in - subst_aconstr_in_glob_constr loc intern lvar + instantiate_notation_constr loc intern lvar (terms, termlists, binders) (Id.Map.empty, env) c (**********************************************************************) @@ -759,7 +759,7 @@ let intern_qualid loc qid intern env lvar us args = let subst = (terms, 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 = subst_aconstr_in_glob_constr loc intern lvar subst infos c in + let c = instantiate_notation_constr loc intern lvar subst infos c in let c = match us, c with | None, _ -> c | Some _, GRef (loc, ref, None) -> GRef (loc, ref, us) diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 5b49ebcbd..b4cf6e943 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -12,15 +12,103 @@ open Util open Names open Nameops open Globnames +open Decl_kinds open Misctypes open Glob_term open Glob_ops open Mod_subst open Notation_term -open Decl_kinds (**********************************************************************) -(* Re-interpret a notation as a glob_constr, taking care of binders *) +(* Utilities *) + +let on_true_do b f c = if b then (f c; b) else b + +let compare_glob_constr f add t1 t2 = match t1,t2 with + | GRef (_,r1,_), GRef (_,r2,_) -> eq_gr r1 r2 + | GVar (_,v1), GVar (_,v2) -> on_true_do (Id.equal v1 v2) add (Name v1) + | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2 + | GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2) + when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 -> + on_true_do (f ty1 ty2 && f c1 c2) add na1 + | GProd (_,na1,bk1,ty1,c1), GProd (_,na2,bk2,ty2,c2) + when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 -> + on_true_do (f ty1 ty2 && f c1 c2) add na1 + | GHole _, GHole _ -> true + | GSort (_,s1), GSort (_,s2) -> Miscops.glob_sort_eq s1 s2 + | GLetIn (_,na1,b1,c1), GLetIn (_,na2,b2,c2) when Name.equal na1 na2 -> + on_true_do (f b1 b2 && f c1 c2) add na1 + | (GCases _ | GRec _ + | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_ + | _,(GCases _ | GRec _ + | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _) + -> error "Unsupported construction in recursive notations." + | (GRef _ | GVar _ | GApp _ | GLambda _ | GProd _ + | GHole _ | GSort _ | GLetIn _), _ + -> false + +let rec eq_notation_constr t1 t2 = match t1, t2 with +| NRef gr1, NRef gr2 -> eq_gr gr1 gr2 +| NVar id1, NVar id2 -> Id.equal id1 id2 +| NApp (t1, a1), NApp (t2, a2) -> + eq_notation_constr t1 t2 && List.equal eq_notation_constr a1 a2 +| NHole (_, _, _), NHole (_, _, _) -> true (** FIXME? *) +| NList (i1, j1, t1, u1, b1), NList (i2, j2, t2, u2, b2) -> + Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 && + eq_notation_constr u1 u2 && b1 == b2 +| NLambda (na1, t1, u1), NLambda (na2, t2, u2) -> + Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2 +| NProd (na1, t1, u1), NProd (na2, t2, u2) -> + Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2 +| NBinderList (i1, j1, t1, u1), NBinderList (i2, j2, t2, u2) -> + Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 && + eq_notation_constr u1 u2 +| NLetIn (na1, t1, u1), NLetIn (na2, t2, u2) -> + Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2 +| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (** FIXME? *) + let eqpat (p1, t1) (p2, t2) = + List.equal cases_pattern_eq p1 p2 && + eq_notation_constr t1 t2 + in + let eqf (t1, (na1, o1)) (t2, (na2, o2)) = + let eq (i1, n1) (i2, n2) = eq_ind i1 i2 && List.equal Name.equal n1 n2 in + eq_notation_constr t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2 + in + Option.equal eq_notation_constr o1 o2 && + List.equal eqf r1 r2 && + List.equal eqpat p1 p2 +| NLetTuple (nas1, (na1, o1), t1, u1), NLetTuple (nas2, (na2, o2), t2, u2) -> + List.equal Name.equal nas1 nas2 && + Name.equal na1 na2 && + Option.equal eq_notation_constr o1 o2 && + eq_notation_constr t1 t2 && + eq_notation_constr u1 u2 +| NIf (t1, (na1, o1), u1, r1), NIf (t2, (na2, o2), u2, r2) -> + eq_notation_constr t1 t2 && + Name.equal na1 na2 && + Option.equal eq_notation_constr o1 o2 && + eq_notation_constr u1 u2 && + eq_notation_constr r1 r2 +| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (** FIXME? *) + let eq (na1, o1, t1) (na2, o2, t2) = + Name.equal na1 na2 && + Option.equal eq_notation_constr o1 o2 && + eq_notation_constr t1 t2 + in + Array.equal Id.equal ids1 ids2 && + Array.equal (List.equal eq) ts1 ts2 && + Array.equal eq_notation_constr us1 us2 && + Array.equal eq_notation_constr rs1 rs2 +| NSort s1, NSort s2 -> + Miscops.glob_sort_eq s1 s2 +| NCast (t1, c1), NCast (t2, c2) -> + eq_notation_constr t1 t2 && cast_type_eq eq_notation_constr c1 c2 +| (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _ + | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _ + | NRec _ | NSort _ | NCast _), _ -> false + +(**********************************************************************) +(* Re-interpret a notation as a glob_constr, taking care of binders *) let name_to_ident = function | Anonymous -> Errors.error "This expression should be a simple identifier." @@ -112,7 +200,7 @@ let glob_constr_of_notation_constr loc x = glob_constr_of_notation_constr_with_binders loc (fun () id -> ((),id)) aux () x in aux () x -(****************************************************************************) +(******************************************************************************) (* Translating a glob_constr into a notation, interpreting recursive patterns *) let add_id r id = r := (id :: pi1 !r, pi2 !r, pi3 !r) @@ -142,94 +230,6 @@ let split_at_recursive_part c = | GVar (_,v) when Id.equal v ldots_var -> (* Not enough context *) raise Not_found | _ -> outer_iterator, c -let on_true_do b f c = if b then (f c; b) else b - -let compare_glob_constr f add t1 t2 = match t1,t2 with - | GRef (_,r1,_), GRef (_,r2,_) -> eq_gr r1 r2 - | GVar (_,v1), GVar (_,v2) -> on_true_do (Id.equal v1 v2) add (Name v1) - | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2 - | GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2) - when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 -> - on_true_do (f ty1 ty2 && f c1 c2) add na1 - | GProd (_,na1,bk1,ty1,c1), GProd (_,na2,bk2,ty2,c2) - when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 -> - on_true_do (f ty1 ty2 && f c1 c2) add na1 - | GHole _, GHole _ -> true - | GSort (_,s1), GSort (_,s2) -> Miscops.glob_sort_eq s1 s2 - | GLetIn (_,na1,b1,c1), GLetIn (_,na2,b2,c2) when Name.equal na1 na2 -> - on_true_do (f b1 b2 && f c1 c2) add na1 - | (GCases _ | GRec _ - | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_ - | _,(GCases _ | GRec _ - | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _) - -> error "Unsupported construction in recursive notations." - | (GRef _ | GVar _ | GApp _ | GLambda _ | GProd _ - | GHole _ | GSort _ | GLetIn _), _ - -> false - -let rec eq_glob_constr t1 t2 = compare_glob_constr eq_glob_constr (fun _ -> ()) t1 t2 - -let rec eq_notation_constr t1 t2 = match t1, t2 with -| NRef gr1, NRef gr2 -> eq_gr gr1 gr2 -| NVar id1, NVar id2 -> Id.equal id1 id2 -| NApp (t1, a1), NApp (t2, a2) -> - eq_notation_constr t1 t2 && List.equal eq_notation_constr a1 a2 -| NHole (_, _, _), NHole (_, _, _) -> true (** FIXME? *) -| NList (i1, j1, t1, u1, b1), NList (i2, j2, t2, u2, b2) -> - Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 && - eq_notation_constr u1 u2 && b1 == b2 -| NLambda (na1, t1, u1), NLambda (na2, t2, u2) -> - Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2 -| NProd (na1, t1, u1), NProd (na2, t2, u2) -> - Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2 -| NBinderList (i1, j1, t1, u1), NBinderList (i2, j2, t2, u2) -> - Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 && - eq_notation_constr u1 u2 -| NLetIn (na1, t1, u1), NLetIn (na2, t2, u2) -> - Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2 -| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (** FIXME? *) - let eqpat (p1, t1) (p2, t2) = - List.equal cases_pattern_eq p1 p2 && - eq_notation_constr t1 t2 - in - let eqf (t1, (na1, o1)) (t2, (na2, o2)) = - let eq (i1, n1) (i2, n2) = eq_ind i1 i2 && List.equal Name.equal n1 n2 in - eq_notation_constr t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2 - in - Option.equal eq_notation_constr o1 o2 && - List.equal eqf r1 r2 && - List.equal eqpat p1 p2 -| NLetTuple (nas1, (na1, o1), t1, u1), NLetTuple (nas2, (na2, o2), t2, u2) -> - List.equal Name.equal nas1 nas2 && - Name.equal na1 na2 && - Option.equal eq_notation_constr o1 o2 && - eq_notation_constr t1 t2 && - eq_notation_constr u1 u2 -| NIf (t1, (na1, o1), u1, r1), NIf (t2, (na2, o2), u2, r2) -> - eq_notation_constr t1 t2 && - Name.equal na1 na2 && - Option.equal eq_notation_constr o1 o2 && - eq_notation_constr u1 u2 && - eq_notation_constr r1 r2 -| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (** FIXME? *) - let eq (na1, o1, t1) (na2, o2, t2) = - Name.equal na1 na2 && - Option.equal eq_notation_constr o1 o2 && - eq_notation_constr t1 t2 - in - Array.equal Id.equal ids1 ids2 && - Array.equal (List.equal eq) ts1 ts2 && - Array.equal eq_notation_constr us1 us2 && - Array.equal eq_notation_constr rs1 rs2 -| NSort s1, NSort s2 -> - Miscops.glob_sort_eq s1 s2 -| NCast (t1, c1), NCast (t2, c2) -> - eq_notation_constr t1 t2 && cast_type_eq eq_notation_constr c1 c2 -| (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _ - | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _ - | NRec _ | NSort _ | NCast _), _ -> false - - let subtract_loc loc1 loc2 = Loc.make_loc (fst (Loc.unloc loc1),fst (Loc.unloc loc2)-1) let check_is_hole id = function GHole _ -> () | t -> @@ -409,6 +409,7 @@ let notation_constr_of_glob_constr nenv a = let () = check_variables nenv found in a +(**********************************************************************) (* Substitution of kernel names, avoiding a list of bound identifiers *) let notation_constr_of_constr avoiding t = @@ -544,7 +545,8 @@ let subst_interpretation subst (metas,pat) = let bound = List.map fst metas in (metas,subst_notation_constr subst bound pat) -(* Pattern-matching glob_constr and notation_constr *) +(**********************************************************************) +(* Pattern-matching a [glob_constr] against a [notation_constr] *) let abstract_return_type_context pi mklam tml rtno = Option.map (fun rtn -> diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 280ccfd21..576c5b943 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -10,24 +10,28 @@ open Names open Notation_term open Glob_term -(** Utilities about [notation_constr] *) +(** {5 Utilities about [notation_constr]} *) -(** Translate a [glob_constr] into a notation given the list of variables - bound by the notation; also interpret recursive patterns *) +val eq_notation_constr : notation_constr -> notation_constr -> bool -val notation_constr_of_glob_constr : notation_interp_env -> - glob_constr -> notation_constr +(** Substitution of kernel names in interpretation data *) +val subst_interpretation : + Mod_subst.substitution -> interpretation -> interpretation + (** Name of the special identifier used to encode recursive notations *) + val ldots_var : Id.t -(** Equality of [glob_constr] (warning: only partially implemented) *) -(** FIXME: nothing to do here *) -val eq_glob_constr : glob_constr -> glob_constr -> bool +(** {5 Translation back and forth between [glob_constr] and [notation_constr] *) -val eq_notation_constr : notation_constr -> notation_constr -> bool +(** Translate a [glob_constr] into a notation given the list of variables + bound by the notation; also interpret recursive patterns *) + +val notation_constr_of_glob_constr : notation_interp_env -> + glob_constr -> notation_constr -(** Re-interpret a notation as a [glob_constr], taking care of binders *) +(** Re-interpret a notation as a [glob_constr], taking care of binders *) val glob_constr_of_notation_constr_with_binders : Loc.t -> ('a -> Name.t -> 'a * Name.t) -> @@ -36,6 +40,8 @@ val glob_constr_of_notation_constr_with_binders : Loc.t -> val glob_constr_of_notation_constr : Loc.t -> notation_constr -> glob_constr +(** {5 Matching a notation pattern against a [glob_constr] *) + (** [match_notation_constr] matches a [glob_constr] against a notation interpretation; raise [No_match] if the matching fails *) @@ -55,9 +61,5 @@ val match_notation_constr_ind_pattern : ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) * (int * cases_pattern list) -(** Substitution of kernel names in interpretation data *) - -val subst_interpretation : - Mod_subst.substitution -> interpretation -> interpretation +(** {5 Matching a notation pattern against a [glob_constr] *) -val add_patterns_for_params : inductive -> cases_pattern list -> cases_pattern list |