diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrexpr.ml | 24 | ||||
| -rw-r--r-- | interp/constrexpr_ops.ml | 55 | ||||
| -rw-r--r-- | interp/constrexpr_ops.mli | 4 | ||||
| -rw-r--r-- | interp/constrextern.ml | 140 | ||||
| -rw-r--r-- | interp/constrextern.mli | 12 | ||||
| -rw-r--r-- | interp/constrintern.ml | 784 | ||||
| -rw-r--r-- | interp/constrintern.mli | 5 | ||||
| -rw-r--r-- | interp/notation.ml | 28 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 14 | ||||
| -rw-r--r-- | interp/notation_term.ml | 5 | ||||
| -rw-r--r-- | interp/stdarg.ml | 3 | ||||
| -rw-r--r-- | interp/stdarg.mli | 2 |
12 files changed, 586 insertions, 490 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index b3f06faa1c..b14c325f69 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -13,10 +13,23 @@ open Libnames (** {6 Concrete syntax for terms } *) -(** [constr_expr] is the abstract syntax tree produced by the parser *) -type universe_decl_expr = (lident list, Glob_term.glob_constraint list) UState.gen_universe_decl +(** Universes *) +type sort_name_expr = + | CSProp | CProp | CSet + | CType of qualid + | CRawType of Univ.Level.t (** Universes like "foo.1" have no qualid form *) + +type univ_level_expr = sort_name_expr Glob_term.glob_sort_gen +type sort_expr = (sort_name_expr * int) list Glob_term.glob_sort_gen + +type instance_expr = univ_level_expr list + +(** Constraints don't have anonymous universes *) +type univ_constraint_expr = sort_name_expr * Univ.constraint_type * sort_name_expr + +type universe_decl_expr = (lident list, univ_constraint_expr list) UState.gen_universe_decl type cumul_univ_decl_expr = - ((lident * Univ.Variance.t option) list, Glob_term.glob_constraint list) UState.gen_universe_decl + ((lident * Univ.Variance.t option) list, univ_constraint_expr list) UState.gen_universe_decl type ident_decl = lident * universe_decl_expr option type cumul_ident_decl = lident * cumul_univ_decl_expr option @@ -64,8 +77,7 @@ type prim_token = | Number of NumTok.Signed.t | String of string -type instance_expr = Glob_term.glob_level list - +(** [constr_expr] is the abstract syntax tree produced by the parser *) type cases_pattern_expr_r = | CPatAlias of cases_pattern_expr * lname | CPatCstr of qualid @@ -114,7 +126,7 @@ and constr_expr_r = | CHole of Evar_kinds.t option * Namegen.intro_pattern_naming_expr * Genarg.raw_generic_argument option | CPatVar of Pattern.patvar | CEvar of Glob_term.existential_name CAst.t * (lident * constr_expr) list - | CSort of Glob_term.glob_sort + | CSort of sort_expr | CCast of constr_expr * constr_expr Glob_term.cast_type | CNotation of notation_with_optional_scope option * notation * constr_notation_substitution | CGeneralization of Glob_term.binding_kind * abstraction_kind option * constr_expr diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index a60dc11b57..f02874253e 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -18,6 +18,25 @@ open Glob_term open Notation open Constrexpr +(***********) +(* Universes *) + +let sort_name_expr_eq c1 c2 = match c1, c2 with + | CSProp, CSProp + | CProp, CProp + | CSet, CSet -> true + | CType q1, CType q2 -> Libnames.qualid_eq q1 q2 + | CRawType u1, CRawType u2 -> Univ.Level.equal u1 u2 + | (CSProp|CProp|CSet|CType _|CRawType _), _ -> false + +let univ_level_expr_eq u1 u2 = + Glob_ops.glob_sort_gen_eq sort_name_expr_eq u1 u2 + +let sort_expr_eq u1 u2 = + Glob_ops.glob_sort_gen_eq + (List.equal (fun (x,m) (y,n) -> sort_name_expr_eq x y && Int.equal m n)) + u1 u2 + (***********************) (* For binders parsing *) @@ -59,13 +78,11 @@ let explicitation_eq ex1 ex2 = match ex1, ex2 with Id.equal id1 id2 | _ -> false -let eq_ast f { CAst.v = x } { CAst.v = y } = f x y - 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) -> - eq_ast Name.equal i1 i2 && cases_pattern_expr_eq a1 a2 + CAst.eq Name.equal i1 i2 && cases_pattern_expr_eq a1 a2 | CPatCstr(c1,a1,b1), CPatCstr(c2,a2,b2) -> qualid_eq c1 c2 && Option.equal (List.equal cases_pattern_expr_eq) a1 a2 && @@ -108,10 +125,10 @@ let rec constr_expr_eq e1 e2 = else match CAst.(e1.v, e2.v) with | CRef (r1,u1), CRef (r2,u2) -> qualid_eq r1 r2 && eq_universes u1 u2 | CFix(id1,fl1), CFix(id2,fl2) -> - eq_ast Id.equal id1 id2 && + lident_eq id1 id2 && List.equal fix_expr_eq fl1 fl2 | CCoFix(id1,fl1), CCoFix(id2,fl2) -> - eq_ast Id.equal id1 id2 && + lident_eq id1 id2 && List.equal cofix_expr_eq fl1 fl2 | CProdN(bl1,a1), CProdN(bl2,a2) -> List.equal local_binder_eq bl1 bl2 && @@ -120,7 +137,7 @@ let rec constr_expr_eq e1 e2 = List.equal local_binder_eq bl1 bl2 && constr_expr_eq a1 a2 | CLetIn(na1,a1,t1,b1), CLetIn(na2,a2,t2,b2) -> - eq_ast Name.equal na1 na2 && + CAst.eq Name.equal na1 na2 && constr_expr_eq a1 a2 && Option.equal constr_expr_eq t1 t2 && constr_expr_eq b1 b2 @@ -144,14 +161,14 @@ let rec constr_expr_eq e1 e2 = List.equal case_expr_eq a1 a2 && List.equal branch_expr_eq brl1 brl2 | CLetTuple (n1, (m1, e1), t1, b1), CLetTuple (n2, (m2, e2), t2, b2) -> - List.equal (eq_ast Name.equal) n1 n2 && - Option.equal (eq_ast Name.equal) m1 m2 && + List.equal (CAst.eq Name.equal) n1 n2 && + Option.equal (CAst.eq Name.equal) m1 m2 && Option.equal constr_expr_eq e1 e2 && constr_expr_eq t1 t2 && constr_expr_eq b1 b2 | CIf (e1, (n1, r1), t1, f1), CIf (e2, (n2, r2), t2, f2) -> constr_expr_eq e1 e2 && - Option.equal (eq_ast Name.equal) n1 n2 && + Option.equal (CAst.eq Name.equal) n1 n2 && Option.equal constr_expr_eq r1 r2 && constr_expr_eq t1 t2 && constr_expr_eq f1 f2 @@ -161,7 +178,7 @@ let rec constr_expr_eq e1 e2 = | CEvar (id1, c1), CEvar (id2, c2) -> Id.equal id1.CAst.v id2.CAst.v && List.equal instance_eq c1 c2 | CSort s1, CSort s2 -> - Glob_ops.glob_sort_eq s1 s2 + sort_expr_eq s1 s2 | CCast(t1,c1), CCast(t2,c2) -> constr_expr_eq t1 t2 && cast_expr_eq c1 c2 | CNotation(inscope1, n1, s1), CNotation(inscope2, n2, s2) -> @@ -187,12 +204,12 @@ let rec constr_expr_eq e1 e2 = | CGeneralization _ | CDelimiters _ | CArray _), _ -> false and args_eq (a1,e1) (a2,e2) = - Option.equal (eq_ast explicitation_eq) e1 e2 && + Option.equal (CAst.eq explicitation_eq) e1 e2 && constr_expr_eq a1 a2 and case_expr_eq (e1, n1, p1) (e2, n2, p2) = constr_expr_eq e1 e2 && - Option.equal (eq_ast Name.equal) n1 n2 && + Option.equal (CAst.eq Name.equal) n1 n2 && Option.equal cases_pattern_expr_eq p1 p2 and branch_expr_eq {CAst.v=(p1, e1)} {CAst.v=(p2, e2)} = @@ -200,35 +217,35 @@ and branch_expr_eq {CAst.v=(p1, e1)} {CAst.v=(p2, e2)} = constr_expr_eq e1 e2 and fix_expr_eq (id1,r1,bl1,a1,b1) (id2,r2,bl2,a2,b2) = - (eq_ast Id.equal id1 id2) && + (lident_eq id1 id2) && Option.equal recursion_order_expr_eq r1 r2 && List.equal local_binder_eq bl1 bl2 && constr_expr_eq a1 a2 && constr_expr_eq b1 b2 and cofix_expr_eq (id1,bl1,a1,b1) (id2,bl2,a2,b2) = - (eq_ast Id.equal id1 id2) && + (lident_eq id1 id2) && List.equal local_binder_eq bl1 bl2 && constr_expr_eq a1 a2 && constr_expr_eq b1 b2 and recursion_order_expr_eq_r r1 r2 = match r1, r2 with - | CStructRec i1, CStructRec i2 -> eq_ast Id.equal i1 i2 + | CStructRec i1, CStructRec i2 -> lident_eq i1 i2 | CWfRec (i1,e1), CWfRec (i2,e2) -> constr_expr_eq e1 e2 | CMeasureRec (i1, e1, o1), CMeasureRec (i2, e2, o2) -> - Option.equal (eq_ast Id.equal) i1 i2 && + Option.equal lident_eq i1 i2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq o1 o2 | _ -> false -and recursion_order_expr_eq r1 r2 = eq_ast recursion_order_expr_eq_r r1 r2 +and recursion_order_expr_eq r1 r2 = CAst.eq recursion_order_expr_eq_r r1 r2 and local_binder_eq l1 l2 = match l1, l2 with | CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) -> - eq_ast Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2 + CAst.eq Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2 | CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) -> (* Don't care about the [binder_kind] *) - List.equal (eq_ast Name.equal) n1 n2 && constr_expr_eq e1 e2 + List.equal (CAst.eq Name.equal) n1 n2 && constr_expr_eq e1 e2 | _ -> false and constr_notation_substitution_eq (e1, el1, b1, bl1) (e2, el2, b2, bl2) = diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index dfa51918d1..ffa7c8ec10 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -16,6 +16,10 @@ open Constrexpr (** {6 Equalities on [constr_expr] related types} *) +val sort_name_expr_eq : sort_name_expr -> sort_name_expr -> bool +val univ_level_expr_eq : univ_level_expr -> univ_level_expr -> bool +val sort_expr_eq : sort_expr -> sort_expr -> bool + val explicitation_eq : explicitation -> explicitation -> bool (** Equality on [explicitation]. *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index cf88036f73..f3ba884856 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -800,19 +800,21 @@ let extern_args extern env args = let match_coercion_app c = match DAst.get c with | GApp (r, args) -> begin match DAst.get r with - | GRef (r,_) -> Some (c.CAst.loc, r, 0, args) + | GRef (r,_) -> Some (c.CAst.loc, r, args) | _ -> None end | _ -> None let remove_one_coercion inctx c = try match match_coercion_app c with - | Some (loc,r,pars,args) when not (!Flags.raw_print || !print_coercions) -> + | Some (loc,r,args) when not (!Flags.raw_print || !print_coercions) -> let nargs = List.length args in (match Coercionops.hide_coercion r with - | Some n when (n - pars) < nargs && (inctx || (n - pars)+1 < nargs) -> + | Some nparams when + let inctx = inctx || (* coercion to funclass implying being in context *) nparams+1 < nargs in + nparams < nargs && inctx -> (* We skip the coercion *) - let l = List.skipn (n - pars) args in + let l = List.skipn nparams args in let (a,l) = match l with a::l -> (a,l) | [] -> assert false in (* Don't flatten App's in case of funclass so that (atomic) notations on [a] work; should be compatible @@ -824,7 +826,7 @@ let remove_one_coercion inctx c = have been made explicit to match *) let a' = if List.is_empty l then a else DAst.make ?loc @@ GApp (a,l) in let inctx = inctx || not (List.is_empty l) in - Some (n-pars+1, inctx, a') + Some (nparams+1, inctx, a') | _ -> None) | _ -> None with Not_found -> @@ -867,7 +869,7 @@ let filter_enough_applied nargs l = | Some nargs -> List.filter (fun (keyrule,pat,n as _rule) -> match n with - | AppBoundedNotation n -> n > nargs + | AppBoundedNotation n -> n >= nargs | AppUnboundedNotation | NotAppNotation -> false) l (* Helper function for safe and optimal printing of primitive tokens *) @@ -884,9 +886,10 @@ let extern_prim_token_delimiter_if_required n key_n scope_n scopes = let extended_glob_local_binder_of_decl loc = function | (p,bk,None,t) -> GLocalAssum (p,bk,t) | (p,bk,Some x, t) -> + assert (bk = Explicit); match DAst.get t with - | GHole (_, IntroAnonymous, None) -> GLocalDef (p,bk,x,None) - | _ -> GLocalDef (p,bk,x,Some t) + | GHole (_, IntroAnonymous, None) -> GLocalDef (p,x,None) + | _ -> GLocalDef (p,x,Some t) let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_local_binder_of_decl loc u) @@ -921,22 +924,44 @@ let extern_float f scopes = (**********************************************************************) (* mapping glob_constr to constr_expr *) -let extern_glob_sort = function +type extern_env = Id.Set.t * UnivNames.universe_binders +let extern_env env sigma = vars_of_env env, Evd.universe_binders sigma +let empty_extern_env = Id.Set.empty, Id.Map.empty + +let extern_glob_sort_name uvars = function + | GSProp -> CSProp + | GProp -> CProp + | GSet -> CSet + | GLocalUniv u -> CType (qualid_of_lident u) + | GRawUniv u -> CRawType u + | GUniv u -> begin match UnivNames.qualid_of_level uvars u with + | Some qid -> CType qid + | None -> CRawType u + end + +let extern_glob_sort uvars = + map_glob_sort_gen (List.map (on_fst (extern_glob_sort_name uvars))) + +(** wrapper to handle print_universes: don't forget small univs *) +let extern_glob_sort uvars = function (* In case we print a glob_constr w/o having passed through detyping *) - | UNamed [(GSProp,0) | (GProp,0) | (GSet,0)] as u -> u + | UNamed [(GSProp,0) | (GProp,0) | (GSet,0)] as u -> extern_glob_sort uvars u | UNamed _ when not !print_universes -> UAnonymous {rigid=true} - | UNamed _ | UAnonymous _ as u -> u + | UNamed _ | UAnonymous _ as u -> extern_glob_sort uvars u -let extern_universes = function - | Some _ as l when !print_universes -> l +let extern_instance uvars = function + | Some l when !print_universes -> + Some (List.map (map_glob_sort_gen (extern_glob_sort_name uvars)) l) | _ -> None -let extern_ref vars ref us = +let extern_ref (vars,uvars) ref us = extern_global (select_stronger_impargs (implicits_of_global ref)) - (extern_reference vars ref) (extern_universes us) + (extern_reference vars ref) (extern_instance uvars us) let extern_var ?loc id = CRef (qualid_of_ident ?loc id,None) +let add_vname (vars,uvars) na = add_vname vars na, uvars + let rec extern inctx ?impargs scopes vars r = match remove_one_coercion inctx (flatten_application r) with | Some (nargs,inctx,r') -> @@ -993,7 +1018,7 @@ let rec extern inctx ?impargs scopes vars r = (* Otherwise... *) extern_applied_ref inctx (select_stronger_impargs (implicits_of_global ref)) - (ref,extern_reference ?loc vars ref) (extern_universes us) args) + (ref,extern_reference ?loc (fst vars) ref) (extern_instance (snd vars) us) args) | _ -> let args = List.map (fun c -> (sub_extern true scopes vars c,None)) args in let head = sub_extern false scopes vars f in @@ -1013,7 +1038,8 @@ let rec extern inctx ?impargs scopes vars r = | GCases (sty,rtntypopt,tml,eqns) -> let vars' = List.fold_right (Name.fold_right Id.Set.add) - (cases_predicate_names tml) vars in + (cases_predicate_names tml) (fst vars) in + let vars' = vars', snd vars in let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in let tml = List.map (fun (tm,(na,x)) -> let na' = match na, DAst.get tm with @@ -1033,7 +1059,7 @@ let rec extern inctx ?impargs scopes vars r = Option.map (fun {CAst.loc;v=(ind,nal)} -> let args = List.map (fun x -> DAst.make @@ PatVar x) nal in let fullargs = add_cpatt_for_params ind args in - extern_ind_pattern_in_scope scopes vars ind fullargs + extern_ind_pattern_in_scope scopes (fst vars) ind fullargs ) x)) tml in @@ -1056,7 +1082,7 @@ let rec extern inctx ?impargs scopes vars r = sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2) | GRec (fk,idv,blv,tyv,bv) -> - let vars' = Array.fold_right Id.Set.add idv vars in + let vars' = on_fst (Array.fold_right Id.Set.add idv) vars in (match fk with | GFix (nv,n) -> let listdecl = @@ -1064,8 +1090,8 @@ let rec extern inctx ?impargs scopes vars r = let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in let bl = List.map (extended_glob_local_binder_of_decl ?loc) bl in let (assums,ids,bl) = extern_local_binder scopes vars bl in - let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in - let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in + let vars0 = on_fst (List.fold_right (Name.fold_right Id.Set.add) ids) vars in + let vars1 = on_fst (List.fold_right (Name.fold_right Id.Set.add) ids) vars' in let n = match nv.(i) with | None -> None @@ -1080,14 +1106,14 @@ let rec extern inctx ?impargs scopes vars r = Array.mapi (fun i fi -> let bl = List.map (extended_glob_local_binder_of_decl ?loc) blv.(i) in let (_,ids,bl) = extern_local_binder scopes vars bl in - let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in - let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in + let vars0 = on_fst (List.fold_right (Name.fold_right Id.Set.add) ids) vars in + let vars1 = on_fst (List.fold_right (Name.fold_right Id.Set.add) ids) vars' in ((CAst.make fi),bl,extern_typ scopes vars0 tyv.(i), sub_extern true scopes vars1 bv.(i))) idv in CCoFix (CAst.(make ?loc idv.(n)),Array.to_list listdecl)) - | GSort s -> CSort (extern_glob_sort s) + | GSort s -> CSort (extern_glob_sort (snd vars) s) | GHole (e,naming,_) -> CHole (Some e, naming, None) (* TODO: extern tactics. *) @@ -1103,7 +1129,7 @@ let rec extern inctx ?impargs scopes vars r = | GFloat f -> extern_float f (snd scopes) | GArray(u,t,def,ty) -> - CArray(extern_universes u,Array.map (extern inctx scopes vars) t, extern inctx scopes vars def, extern_typ scopes vars ty) + CArray(extern_instance (snd vars) u,Array.map (extern inctx scopes vars) t, extern inctx scopes vars def, extern_typ scopes vars ty) in insert_entry_coercion coercion (CAst.make ?loc c) @@ -1125,7 +1151,7 @@ and factorize_prod ?impargs scopes vars na bk t c = let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in let disjpat = if occur_glob_constr id b then List.map (set_pat_alias id) disjpat else disjpat in let b = extern_typ scopes vars b in - let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes vars) disjpat) in + let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes (fst vars)) disjpat) in let binder = CLocalPattern p in (match b.v with | CProdN (bl,b) -> CProdN (binder::bl,b) @@ -1166,7 +1192,7 @@ and factorize_lambda inctx scopes vars na bk t c = let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in let disjpat = if occur_glob_constr id b then List.map (set_pat_alias id) disjpat else disjpat in let b = sub_extern inctx scopes vars b in - let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes vars) disjpat) in + let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes (fst vars)) disjpat) in let binder = CLocalPattern p in (match b.v with | CLambdaN (bl,b) -> CLambdaN (binder::bl,b) @@ -1192,9 +1218,9 @@ and extern_local_binder scopes vars = function [] -> ([],[],[]) | b :: l -> match DAst.get b with - | GLocalDef (na,bk,bd,ty) -> + | GLocalDef (na,bd,ty) -> let (assums,ids,l) = - extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l in + extern_local_binder scopes (on_fst (Name.fold_right Id.Set.add na) vars) l in (assums,na::ids, CLocalDef(CAst.make na, extern false scopes vars bd, Option.map (extern_typ scopes vars) ty) :: l) @@ -1202,7 +1228,7 @@ and extern_local_binder scopes vars = function | GLocalAssum (na,bk,ty) -> let implicit_type = is_reserved_type na ty in let ty = extern_typ scopes vars ty in - (match extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l with + (match extern_local_binder scopes (on_fst (Name.fold_right Id.Set.add na) vars) l with (assums,ids,CLocalAssum(nal,k,ty')::l) when (constr_expr_eq ty ty' || implicit_type && constr_expr_eq ty' hole) && match na with Name id -> not (occur_var_constr_expr id ty') @@ -1217,7 +1243,7 @@ and extern_local_binder scopes vars = function | GLocalPattern ((p,_),_,bk,ty) -> let ty = if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in - let p = mkCPatOr (List.map (extern_cases_pattern vars) p) in + let p = mkCPatOr (List.map (extern_cases_pattern (fst vars)) p) in let (assums,ids,l) = extern_local_binder scopes vars l in let p = match ty with | None -> p @@ -1225,7 +1251,7 @@ and extern_local_binder scopes vars = function (assums,ids, CLocalPattern p :: l) and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} = - let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in + let pll = List.map (List.map (extern_cases_pattern_in_scope scopes (fst vars))) pll in make ?loc (pll,extern inctx scopes vars c) and extern_notations inctx scopes vars nargs t = @@ -1275,6 +1301,7 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules = end | AppBoundedNotation _ -> raise No_match in (* Try matching ... *) + let vars, uvars = vars in let terms,termlists,binders,binderlists = match_notation_constr ~print_univ:(!print_universes) t ~vars pat in (* Try availability of interpretation ... *) @@ -1298,35 +1325,43 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules = let l = List.map (fun ((vars,c),(subentry,(scopt,scl))) -> extern (* assuming no overloading: *) true - (subentry,(scopt,scl@scopes')) vars c) - terms in + (subentry,(scopt,scl@scopes')) (vars,uvars) c) + terms + in let ll = List.map (fun ((vars,l),(subentry,(scopt,scl))) -> - List.map (extern true (subentry,(scopt,scl@scopes')) vars) l) - termlists in + List.map (extern true (subentry,(scopt,scl@scopes')) (vars,uvars)) l) + termlists + in let bl = List.map (fun ((vars,bl),(subentry,(scopt,scl))) -> - (mkCPatOr (List.map (extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars) bl)), - Explicit) - binders in + (mkCPatOr (List.map + (extern_cases_pattern_in_scope + (subentry,(scopt,scl@scopes')) vars) + bl)), + Explicit) + binders + in let bll = List.map (fun ((vars,bl),(subentry,(scopt,scl))) -> - pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) vars bl)) - binderlists in + pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) (vars,uvars) bl)) + binderlists + in let c = make_notation loc specific_ntn (l,ll,bl,bll) in let c = insert_entry_coercion coercion (insert_delimiters c key) in let args = fill_arg_scopes args argsscopes allscopes in - let args = extern_args (extern true) vars args in + let args = extern_args (extern true) (vars,uvars) args in CAst.make ?loc @@ extern_applied_notation inctx nallargs argsimpls c args) | SynDefRule kn -> let l = List.map (fun ((vars,c),(subentry,(scopt,scl))) -> - extern true (subentry,(scopt,scl@snd scopes)) vars c) - terms in + extern true (subentry,(scopt,scl@snd scopes)) (vars,uvars) c) + terms + in let cf = Nametab.shortest_qualid_of_syndef ?loc vars kn in let a = CRef (cf,None) in let args = fill_arg_scopes args argsscopes allscopes in - let args = extern_args (extern true) vars args in + let args = extern_args (extern true) (vars,uvars) args in let c = CAst.make ?loc @@ extern_applied_syntactic_definition inctx nallargs argsimpls (a,cf) l args in if isCRef_no_univ c.CAst.v && entry_has_global custom then c else match availability_of_entry_coercion custom InConstrEntrySomeLevel with @@ -1346,7 +1381,7 @@ let extern_glob_type ?impargs vars c = let extern_constr ?lax ?(inctx=false) ?scope env sigma t = let r = Detyping.detype Detyping.Later ?lax false Id.Set.empty env sigma t in - let vars = vars_of_env env in + let vars = extern_env env sigma in extern inctx (InConstrEntrySomeLevel,(scope,[])) vars r let extern_constr_in_scope ?lax ?inctx scope env sigma t = @@ -1362,16 +1397,16 @@ let extern_type ?lax ?(goal_concl_style=false) env sigma ?impargs t = (* consideration; see namegen.ml for further details *) let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in let r = Detyping.detype Detyping.Later ?lax goal_concl_style avoid env sigma t in - extern_glob_type ?impargs (vars_of_env env) r + extern_glob_type ?impargs (extern_env env sigma) r -let extern_sort sigma s = extern_glob_sort (detype_sort sigma s) +let extern_sort sigma s = extern_glob_sort (Evd.universe_binders sigma) (detype_sort sigma s) let extern_closed_glob ?lax ?(goal_concl_style=false) ?(inctx=false) ?scope env sigma t = let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in let r = Detyping.detype_closed_glob ?lax goal_concl_style avoid env sigma t in - let vars = vars_of_env env in + let vars = extern_env env sigma in extern inctx (InConstrEntrySomeLevel,(scope,[])) vars r (******************************************************************) @@ -1489,10 +1524,13 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with GArray (None, Array.map glob_of t, glob_of def, glob_of ty) let extern_constr_pattern env sigma pat = - extern true (InConstrEntrySomeLevel,(None,[])) Id.Set.empty (glob_of_pat Id.Set.empty env sigma pat) + extern true (InConstrEntrySomeLevel,(None,[])) + (* XXX no vars? *) + (Id.Set.empty, Evd.universe_binders sigma) + (glob_of_pat Id.Set.empty env sigma pat) let extern_rel_context where env sigma sign = let a = detype_rel_context Detyping.Later where Id.Set.empty (names_of_rel_context env,env) sigma sign in - let vars = vars_of_env env in + let vars = extern_env env sigma in let a = List.map (extended_glob_local_binder_of_decl) a in pi3 (extern_local_binder (InConstrEntrySomeLevel,(None,[])) vars a) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index f85e49d2df..298b52f0be 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -23,9 +23,12 @@ open Ltac_pretype (** Translation of pattern, cases pattern, glob_constr and term into syntax trees for printing *) +type extern_env = Id.Set.t * UnivNames.universe_binders +val extern_env : env -> Evd.evar_map -> extern_env + val extern_cases_pattern : Id.Set.t -> 'a cases_pattern_g -> cases_pattern_expr -val extern_glob_constr : Id.Set.t -> 'a glob_constr_g -> constr_expr -val extern_glob_type : ?impargs:Glob_term.binding_kind list -> Id.Set.t -> 'a glob_constr_g -> constr_expr +val extern_glob_constr : extern_env -> 'a glob_constr_g -> constr_expr +val extern_glob_type : ?impargs:Glob_term.binding_kind list -> extern_env -> 'a glob_constr_g -> constr_expr val extern_constr_pattern : names_context -> Evd.evar_map -> constr_pattern -> constr_expr val extern_closed_glob : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> @@ -43,7 +46,7 @@ val extern_constr_in_scope : ?lax:bool -> ?inctx:bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid val extern_type : ?lax:bool -> ?goal_concl_style:bool -> env -> Evd.evar_map -> ?impargs:Glob_term.binding_kind list -> types -> constr_expr -val extern_sort : Evd.evar_map -> Sorts.t -> glob_sort +val extern_sort : Evd.evar_map -> Sorts.t -> sort_expr val extern_rel_context : constr option -> env -> Evd.evar_map -> rel_context -> local_binder_expr list @@ -96,3 +99,6 @@ val toggle_scope_printing : val toggle_notation_printing : ?scope:Notation_term.scope_name -> notation:Constrexpr.notation -> activate:bool -> unit + +(** Probably shouldn't be used *) +val empty_extern_env : extern_env diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8bd77abc4a..70a4ea35e9 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -90,18 +90,6 @@ let for_grammar f x = a (**********************************************************************) -(* Locating reference, possibly via an abbreviation *) - -let locate_reference qid = - Smartlocate.global_of_extended_global (Nametab.locate_extended qid) - -let is_global id = - try - let _ = locate_reference (qualid_of_ident id) in true - with Not_found -> - false - -(**********************************************************************) (* Internalization errors *) type internalization_error = @@ -112,8 +100,7 @@ type internalization_error = | NonLinearPattern of Id.t | BadPatternsNumber of int * int | NotAProjection of qualid - | NotAProjectionOf of qualid * qualid - | ProjectionsOfDifferentRecords of qualid * qualid + | ProjectionsOfDifferentRecords of Recordops.struc_typ * Recordops.struc_typ exception InternalizationError of internalization_error @@ -139,13 +126,16 @@ let explain_bad_patterns_number n1 n2 = str "Expecting " ++ int n1 ++ str (String.plural n1 " pattern") ++ str " but found " ++ int n2 +let inductive_of_record record = + let inductive = GlobRef.IndRef (inductive_of_constructor record.Recordops.s_CONST) in + Nametab.shortest_qualid_of_global Id.Set.empty inductive + let explain_field_not_a_projection field_id = pr_qualid field_id ++ str ": Not a projection" -let explain_field_not_a_projection_of field_id inductive_id = - pr_qualid field_id ++ str ": Not a projection of inductive " ++ pr_qualid inductive_id - -let explain_projections_of_diff_records inductive1_id inductive2_id = +let explain_projections_of_diff_records record1 record2 = + let inductive1_id = inductive_of_record record1 in + let inductive2_id = inductive_of_record record2 in str "This record contains fields of both " ++ pr_qualid inductive1_id ++ str " and " ++ pr_qualid inductive2_id @@ -158,8 +148,6 @@ let explain_internalization_error e = | NonLinearPattern id -> explain_non_linear_pattern id | BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2 | NotAProjection field_id -> explain_field_not_a_projection field_id - | NotAProjectionOf (field_id, inductive_id) -> - explain_field_not_a_projection_of field_id inductive_id | ProjectionsOfDifferentRecords (inductive1_id, inductive2_id) -> explain_projections_of_diff_records inductive1_id inductive2_id in pp ++ str "." @@ -254,9 +242,12 @@ let contract_curly_brackets_pat ntn (l,ll) = (* side effect; don't inline *) (InConstrEntry,!ntn'),(l,ll) +type local_univs = { bound : Univ.Level.t Id.Map.t; unb_univs : bool } + type intern_env = { - ids: Names.Id.Set.t; + ids: Id.Set.t; unb: bool; + local_univs: local_univs; tmp_scope: Notation_term.tmp_scope_name option; scopes: Notation_term.scope_name list; impls: internalization_env; @@ -274,9 +265,9 @@ type pattern_intern_env = { (* Remembering the parsing scope of variables in notations *) let make_current_scope tmp scopes = match tmp, scopes with -| Some tmp_scope, (sc :: _) when String.equal sc tmp_scope -> scopes -| Some tmp_scope, scopes -> tmp_scope :: scopes -| None, scopes -> scopes + | Some tmp_scope, (sc :: _) when String.equal sc tmp_scope -> scopes + | Some tmp_scope, scopes -> tmp_scope :: scopes + | None, scopes -> scopes let pr_scope_stack = function | [] -> str "the empty scope stack" @@ -569,10 +560,10 @@ let intern_assumption intern ntnvars env nal bk ty = let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function | GLocalAssum (na,bk,t) -> (na,bk,None,t) - | GLocalDef (na,bk,c,Some t) -> (na,bk,Some c,t) - | GLocalDef (na,bk,c,None) -> + | GLocalDef (na,c,Some t) -> (na,Explicit,Some c,t) + | GLocalDef (na,c,None) -> let t = DAst.make ?loc @@ GHole(Evar_kinds.BinderType na,IntroAnonymous,None) in - (na,bk,Some c,t) + (na,Explicit,Some c,t) | GLocalPattern (_,_,_,_) -> Loc.raise ?loc (Stream.Error "pattern with quote not allowed here") ) @@ -584,7 +575,7 @@ let intern_letin_binder intern ntnvars env (({loc;v=na} as locna),def,ty) = let ty = Option.map (intern (set_type_scope (restart_prod_binders env))) ty in let impls = impls_term_list 1 term in (push_name_env ntnvars impls env locna, - (na,Explicit,term,ty)) + (na,term,ty)) let intern_cases_pattern_as_binder intern test_kind ntnvars env bk (CAst.{v=p;loc} as pv) = let p,t = match p with @@ -615,8 +606,8 @@ let intern_local_binder_aux intern ntnvars (env,bl) = function let bl' = List.map (fun {loc;v=(na,c,t)} -> DAst.make ?loc @@ GLocalAssum (na,c,t)) bl' in env, bl' @ bl | CLocalDef( {loc; v=na} as locna,def,ty) -> - let env,(na,bk,def,ty) = intern_letin_binder intern ntnvars env (locna,def,ty) in - env, (DAst.make ?loc @@ GLocalDef (na,bk,def,ty)) :: bl + let env,(na,def,ty) = intern_letin_binder intern ntnvars env (locna,def,ty) in + env, (DAst.make ?loc @@ GLocalDef (na,def,ty)) :: bl | CLocalPattern p -> let env, ((disjpat,il),id),na,bk,t = intern_cases_pattern_as_binder intern test_kind_tolerant ntnvars env Explicit p in (env, (DAst.make ?loc:p.CAst.loc @@ GLocalPattern((disjpat,List.map (fun x -> x.v) il),id,bk,t)) :: bl) @@ -659,7 +650,7 @@ let rec expand_binders ?loc mk bl c = | [] -> c | b :: bl -> match DAst.get b with - | GLocalDef (n, bk, b, oty) -> + | GLocalDef (n, b, oty) -> expand_binders ?loc mk bl (DAst.make ?loc @@ GLetIn (n, b, oty, c)) | GLocalAssum (n, bk, t) -> expand_binders ?loc mk bl (mk ?loc (n,bk,t) c) @@ -733,9 +724,9 @@ let set_type ty1 ty2 = user_err ?loc:t2.CAst.loc Pp.(str "Unexpected type constraint in notation already providing a type constraint.") let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) na ty = - match na with - | Anonymous -> (renaming,env), None, Anonymous, Explicit, set_type ty None - | Name id -> + match na with + | Anonymous -> (renaming,env), None, Anonymous, Explicit, set_type ty None + | Name id -> let store,get = set_temporary_memory () in let test_kind = test_kind_tolerant in try @@ -775,10 +766,10 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam (renaming',env), None, Name id', Explicit, set_type ty None type binder_action = -| AddLetIn of lname * constr_expr * constr_expr option -| AddTermIter of (constr_expr * subscopes) Names.Id.Map.t -| AddPreBinderIter of Id.t * local_binder_expr (* A binder to be internalized *) -| AddBinderIter of Id.t * extended_glob_local_binder (* A binder already internalized - used for generalized binders *) + | AddLetIn of lname * constr_expr * constr_expr option + | AddTermIter of (constr_expr * subscopes) Names.Id.Map.t + | AddPreBinderIter of Id.t * local_binder_expr (* A binder to be internalized *) + | AddBinderIter of Id.t * extended_glob_local_binder (* A binder already internalized - used for generalized binders *) let dmap_with_loc f n = CAst.map_with_loc (fun ?loc c -> f ?loc (DAst.get_thunk c)) n @@ -803,8 +794,8 @@ let terms_of_binders bl = let loc = bnd.loc in begin match DAst.get bnd with | GLocalAssum (Name id,_,_) -> (CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None)) :: extract_variables l - | GLocalDef (Name id,_,_,_) -> extract_variables l - | GLocalDef (Anonymous,_,_,_) + | GLocalDef (Name id,_,_) -> extract_variables l + | GLocalDef (Anonymous,_,_) | GLocalAssum (Anonymous,_,_) -> user_err Pp.(str "Cannot turn \"_\" into a term.") | GLocalPattern (([u],_),_,_,_) -> term_of_pat u :: extract_variables l | GLocalPattern ((_,_),_,_,_) -> error_cannot_coerce_disjunctive_pattern_term ?loc () @@ -856,7 +847,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = | AddTermIter nterms::rest,terminator,iter -> aux (nterms,None,Some (rest,terminator,iter)) (renaming,env) iter | AddLetIn (na,c,t)::rest,terminator,iter -> - let env,(na,_,c,t) = intern_letin_binder intern ntnvars (adjust_env env iter) (na,c,t) in + let env,(na,c,t) = intern_letin_binder intern ntnvars (adjust_env env iter) (na,c,t) in DAst.make ?loc (GLetIn (na,c,t,aux_letin env (rest,terminator,iter))) in aux_letin env (Option.get iteropt) | NVar id -> subst_var subst' (renaming, env) id @@ -976,6 +967,9 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = into a substitution for interpretation and based on binding/constr distinction *) +let cases_pattern_of_id {loc;v=id} = + CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id))) + let cases_pattern_of_name {loc;v=na} = let atom = match na with Name id -> Some (qualid_of_ident ?loc id) | Anonymous -> None in CAst.make ?loc (CPatAtom atom) @@ -991,16 +985,20 @@ let split_by_type ids subst = | NtnTypeConstr -> let terms,terms' = bind id scl terms terms' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') - | NtnTypeBinder NtnBinderParsedAsConstr (AsIdentOrPattern | AsStrictPattern) -> + | NtnTypeBinder NtnBinderParsedAsConstr (AsNameOrPattern | AsStrictPattern) -> 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,Explicit),(false,scl)) binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') | NtnTypeBinder NtnBinderParsedAsConstr AsIdent -> let a,terms = match terms with a::terms -> a,terms | _ -> assert false in + let binders' = Id.Map.add id ((cases_pattern_of_id (coerce_to_id a),Explicit),(true,scl)) binders' in + (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') + | NtnTypeBinder NtnBinderParsedAsConstr AsName -> + let a,terms = match terms with a::terms -> a,terms | _ -> assert false in let binders' = Id.Map.add id ((cases_pattern_of_name (coerce_to_name a),Explicit),(true,scl)) binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') - | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnParsedAsBinder as x) -> - let onlyident = (x = NtnParsedAsIdent) in + | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsName | NtnParsedAsPattern _ | NtnParsedAsBinder as x) -> + let onlyident = (x = NtnParsedAsIdent || x = NtnParsedAsName) in let binders,binders' = bind id (onlyident,scl) binders binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') | NtnTypeConstrList -> @@ -1053,35 +1051,35 @@ let string_of_ty = function | Variable -> "var" let gvar (loc, id) us = match us with -| None | Some [] -> DAst.make ?loc @@ GVar id -| Some _ -> - user_err ?loc (str "Variable " ++ Id.print id ++ - str " cannot have a universe instance") + | None | Some [] -> DAst.make ?loc @@ GVar id + | Some _ -> + user_err ?loc (str "Variable " ++ Id.print id ++ + str " cannot have a universe instance") let intern_var env (ltacvars,ntnvars) namedctx loc id us = (* Is [id] a notation variable *) if Id.Map.mem id ntnvars then begin if not (Id.Map.mem id env.impls) then set_var_scope ?loc id true (env.tmp_scope,env.scopes) ntnvars; - gvar (loc,id) us, [], [] + gvar (loc,id) us end else (* Is [id] registered with implicit arguments *) try - let ty,impls,argsc,uid = Id.Map.find id env.impls in + let ty,_,_,uid = Id.Map.find id env.impls in let tys = string_of_ty ty in Dumpglob.dump_reference ?loc "<>" uid tys; - gvar (loc,id) us, make_implicits_list impls, argsc + gvar (loc,id) us with Not_found -> (* Is [id] bound in current term or is an ltac var bound to constr *) if Id.Set.mem id env.ids || Id.Set.mem id ltacvars.ltac_vars then - gvar (loc,id) us, [], [] + gvar (loc,id) us else if Id.equal id ldots_var (* Is [id] the special variable for recursive notations? *) then if Id.Map.is_empty ntnvars then error_ldots_var ?loc - else gvar (loc,id) us, [], [] + else gvar (loc,id) us else if Id.Set.mem id ltacvars.ltac_bound then (* Is [id] bound to a free name in ltac (this is an ltac error message) *) user_err ?loc ~hdr:"intern_var" @@ -1093,32 +1091,73 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us = (* [id] a section variable *) (* Redundant: could be done in intern_qualid *) let ref = GlobRef.VarRef id in - let impls = implicits_of_global ref in - let scopes = find_arguments_scope ref in Dumpglob.dump_secvar ?loc id; (* this raises Not_found when not a section variable *) (* Someday we should stop relying on Dumglob raising exceptions *) - DAst.make ?loc @@ GRef (ref, us), impls, scopes + DAst.make ?loc @@ GRef (ref, us) with e when CErrors.noncritical e -> (* [id] a goal variable *) - gvar (loc,id) us, [], [] + gvar (loc,id) us + +(**********************************************************************) +(* Locating reference, possibly via an abbreviation *) + +let locate_reference qid = + Smartlocate.global_of_extended_global (Nametab.locate_extended qid) + +let is_global id = + try + let _ = locate_reference (qualid_of_ident id) in true + with Not_found -> + false -let find_appl_head_data c = +let dump_extended_global loc = function + | TrueGlobal ref -> (*feedback_global loc ref;*) Dumpglob.add_glob ?loc ref + | SynDef sp -> Dumpglob.add_glob_kn ?loc sp + +let intern_extended_global_of_qualid qid = + let r = Nametab.locate_extended qid in dump_extended_global qid.CAst.loc r; r + +let intern_reference qid = + let r = + try intern_extended_global_of_qualid qid + with Not_found as exn -> + let _, info = Exninfo.capture exn in + Nametab.error_global_not_found ~info qid + in + Smartlocate.global_of_extended_global r + +let intern_projection qid = + try + let gr = Smartlocate.global_of_extended_global (intern_extended_global_of_qualid qid) in + (gr, Recordops.find_projection gr) + with Not_found -> + Loc.raise ?loc:qid.loc (InternalizationError (NotAProjection qid)) + +(**********************************************************************) +(* Interpreting references *) + +let find_appl_head_data env (_,ntnvars) c = match DAst.get c with + | GVar id when not (Id.Map.mem id ntnvars) -> + (try + let _,impls,argsc,_ = Id.Map.find id env.impls in + make_implicits_list impls, argsc + with Not_found -> [], []) | GRef (ref,_) -> let impls = implicits_of_global ref in let scopes = find_arguments_scope ref in - c, impls, scopes + impls, scopes | GApp (r, l) -> begin match DAst.get r with | GRef (ref,_) -> let n = List.length l in let impls = implicits_of_global ref in let scopes = find_arguments_scope ref in - c, (if n = 0 then [] else List.map (drop_first_implicits n) impls), - List.skipn_at_least n scopes - | _ -> c,[],[] + (if n = 0 then [] else List.map (drop_first_implicits n) impls), + List.skipn_at_least n scopes + | _ -> [],[] end - | _ -> c,[],[] + | _ -> [],[] let error_not_enough_arguments ?loc = user_err ?loc (str "Abbreviation is not applied enough.") @@ -1132,27 +1171,37 @@ let check_no_explicitation l = | (_, Some {loc}) :: _ -> user_err ?loc (str"Unexpected explicitation of the argument of an abbreviation.") -let dump_extended_global loc = function - | TrueGlobal ref -> (*feedback_global loc ref;*) Dumpglob.add_glob ?loc ref - | SynDef sp -> Dumpglob.add_glob_kn ?loc sp - -let intern_extended_global_of_qualid qid = - let r = Nametab.locate_extended qid in dump_extended_global qid.CAst.loc r; r - -let intern_reference qid = - let r = - try intern_extended_global_of_qualid qid - with Not_found as exn -> - let _, info = Exninfo.capture exn in - Nametab.error_global_not_found ~info qid - in - Smartlocate.global_of_extended_global r - let glob_sort_of_level (level: glob_level) : glob_sort = match level with | UAnonymous {rigid} -> UAnonymous {rigid} | UNamed id -> UNamed [id,0] +let intern_sort_name ~local_univs = function + | CSProp -> GSProp + | CProp -> GProp + | CSet -> GSet + | CRawType u -> GRawUniv u + | CType qid -> + let is_id = qualid_is_ident qid in + let local = if not is_id then None + else Id.Map.find_opt (qualid_basename qid) local_univs.bound + in + match local with + | Some u -> GUniv u + | None -> + try GUniv (Univ.Level.make (Nametab.locate_universe qid)) + with Not_found -> + if is_id && local_univs.unb_univs + then GLocalUniv (CAst.make ?loc:qid.loc (qualid_basename qid)) + else + CErrors.user_err Pp.(str "Undeclared universe " ++ pr_qualid qid ++ str".") + +let intern_sort ~local_univs s = + map_glob_sort_gen (List.map (on_fst (intern_sort_name ~local_univs))) s + +let intern_instance ~local_univs us = + Option.map (List.map (map_glob_sort_gen (intern_sort_name ~local_univs))) us + (* Is it a global reference or a syntactic definition? *) let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = let loc = qid.loc in @@ -1194,6 +1243,37 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = in c, None, args2 +let intern_qualid_for_pattern test_global intern_not qid pats = + match intern_extended_global_of_qualid qid with + | TrueGlobal g -> + test_global g; + (g, false, Some [], pats) + | SynDef kn -> + let filter (vars,a) = + match a with + | NRef g -> + (* Convention: do not deactivate implicit arguments and scopes for further arguments *) + test_global g; + let () = assert (List.is_empty vars) in + Some (g, Some [], pats) + | NApp (NRef g,[]) -> (* special case: Syndef for @Cstr deactivates implicit arguments *) + test_global g; + let () = assert (List.is_empty vars) in + Some (g, None, pats) + | NApp (NRef g,args) -> + (* Convention: do not deactivate implicit arguments and scopes for further arguments *) + test_global g; + let nvars = List.length vars in + if List.length pats < nvars then error_not_enough_arguments ?loc:qid.loc; + let pats1,pats2 = List.chop nvars pats in + let subst = split_by_type_pat vars (pats1,[]) in + let args = List.map (intern_not subst) args in + Some (g, Some args, pats2) + | _ -> None in + match Syntax_def.search_filtered_syntactic_definition filter kn with + | Some (g, pats1, pats2) -> (g, true, pats1, pats2) + | None -> raise Not_found + let warn_nonprimitive_projection = CWarnings.create ~name:"nonprimitive-projection-syntax" ~category:"syntax" ~default:CWarnings.Disabled Pp.(fun f -> pr_qualid f ++ str " used as a primitive projection but is not one.") @@ -1218,38 +1298,39 @@ let check_applied_projection isproj realref qid = let intern_applied_reference ~isproj intern env namedctx (_, ntnvars as lvar) us args qid = let loc = qid.CAst.loc in + let us = intern_instance ~local_univs:env.local_univs us in if qualid_is_ident qid then - try - let res = intern_var env lvar namedctx loc (qualid_basename qid) us in - check_applied_projection isproj None qid; - res, args - with Not_found -> - try - let r, realref, args2 = intern_qualid ~no_secvar:true qid intern env ntnvars us args in - check_applied_projection isproj realref qid; - find_appl_head_data r, args2 - with Not_found as exn -> - (* Extra allowance for non globalizing functions *) - if !interning_grammar || env.unb then - (* check_applied_projection ?? *) - (gvar (loc,qualid_basename qid) us, [], []), args - else - let _, info = Exninfo.capture exn in - Nametab.error_global_not_found ~info qid + try + let res = intern_var env lvar namedctx loc (qualid_basename qid) us in + check_applied_projection isproj None qid; + res, args + with Not_found -> + try + let res, realref, args2 = intern_qualid ~no_secvar:true qid intern env ntnvars us args in + check_applied_projection isproj realref qid; + res, args2 + with Not_found as exn -> + (* Extra allowance for non globalizing functions *) + if !interning_grammar || env.unb then + (* check_applied_projection ?? *) + gvar (loc,qualid_basename qid) us, args + else + let _, info = Exninfo.capture exn in + Nametab.error_global_not_found ~info qid else - let r,realref,args2 = - try intern_qualid qid intern env ntnvars us args - with Not_found as exn -> + try + let res, realref, args2 = intern_qualid qid intern env ntnvars us args in + check_applied_projection isproj realref qid; + res, args2 + with Not_found as exn -> let _, info = Exninfo.capture exn in Nametab.error_global_not_found ~info qid - in - check_applied_projection isproj realref qid; - find_appl_head_data r, args2 let interp_reference vars r = - let (r,_,_),_ = + let r,_ = intern_applied_reference ~isproj:None (fun _ -> error_not_enough_arguments ?loc:None) - {ids = Id.Set.empty; unb = false ; + {ids = Id.Set.empty; unb = false; + local_univs = { bound=Id.Map.empty; unb_univs = false };(* <- doesn't matter here *) tmp_scope = None; scopes = []; impls = empty_internalization_env; binder_block_names = None} Environ.empty_named_context_val @@ -1259,17 +1340,18 @@ let interp_reference vars r = (**********************************************************************) (** {5 Cases } *) -(** Private internalization patterns *) +(** Intermediate type common to the patterns of the "in" and of the + "with" clause of "match" *) + type 'a raw_cases_pattern_expr_r = | RCPatAlias of 'a raw_cases_pattern_expr * lname - | RCPatCstr of GlobRef.t - * 'a raw_cases_pattern_expr list * 'a raw_cases_pattern_expr list - (** [RCPatCstr (loc, c, l1, l2)] represents [((@ c l1) l2)] *) + | RCPatCstr of GlobRef.t * 'a raw_cases_pattern_expr list | RCPatAtom of (lident * (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 (** {6 Elementary bricks } *) + let apply_scope_env env = function | [] -> {env with tmp_scope = None}, [] | sc::scl -> {env with tmp_scope = sc}, scl @@ -1282,22 +1364,19 @@ let rec simple_adjust_scopes n scopes = | [] -> None :: simple_adjust_scopes (n-1) [] | sc::scopes -> sc :: simple_adjust_scopes (n-1) scopes -let find_remaining_scopes pl1 pl2 ref = - let impls_st = implicits_of_global ref in - let len_pl1 = List.length pl1 in - let len_pl2 = List.length pl2 in - let impl_list = if Int.equal len_pl1 0 - then select_impargs_size len_pl2 impls_st - else List.skipn_at_least len_pl1 (select_stronger_impargs impls_st) in - let allscs = find_arguments_scope ref in - let scope_list = List.skipn_at_least len_pl1 allscs in - let rec aux = function - |[],l -> l - |_,[] -> [] - |h::t,_::tt when is_status_implicit h -> aux (t,tt) - |_::t,h::tt -> h :: aux (t,tt) - in ((try List.firstn len_pl1 allscs with Failure _ -> simple_adjust_scopes len_pl1 allscs), - simple_adjust_scopes len_pl2 (aux (impl_list,scope_list))) +let rec adjust_to_up l l' default = + match l, l' with + | l, [] -> [] + | [], l -> l + | true::l, l' -> default :: adjust_to_up l l' default + | false::l, y::l' -> y :: adjust_to_up l l' default + +let rec adjust_to_down l l' default = + match l, l' with + | [], l -> [] + | true::l, l' -> adjust_to_down l l' default + | false::l, [] -> default :: adjust_to_down l [] default + | false::l, y::l' -> y :: adjust_to_down l l' default (* @return the first variable that occurs twice in a pattern @@ -1340,85 +1419,16 @@ let check_or_pat_variables loc ids idsl = Id.print (List.hd ids'').v ++ strbrk " is not bound in all patterns).") | [] -> () -(** Use only when params were NOT asked to the user. - @return if letin are included *) -let check_constructor_length env loc cstr len_pl pl0 = - let n = len_pl + List.length pl0 in - if Int.equal n (Inductiveops.constructor_nallargs env cstr) then false else - (Int.equal n (Inductiveops.constructor_nalldecls env cstr) || - (error_wrong_numarg_constructor ?loc env cstr - (Inductiveops.constructor_nrealargs env cstr))) - -open Declarations - -(* Similar to Cases.adjust_local_defs but on RCPat *) -let insert_local_defs_in_pattern (ind,j) l = - let (mib,mip) = Global.lookup_inductive ind in - if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then - (* Optimisation *) l - else - let (ctx, _) = mip.mind_nf_lc.(j-1) in - let decls = List.skipn (Context.Rel.length mib.mind_params_ctxt) (List.rev ctx) in - let rec aux decls args = - match decls, args with - | Context.Rel.Declaration.LocalDef _ :: decls, args -> (DAst.make @@ RCPatAtom None) :: aux decls args - | _, [] -> [] (* In particular, if there were trailing local defs, they have been inserted *) - | Context.Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args - | _ -> assert false in - aux decls l - -let add_local_defs_and_check_length loc env g pl args = - let open GlobRef in - match g with - | ConstructRef cstr -> - (* We consider that no variables corresponding to local binders - have been given in the "explicit" arguments, which come from a - "@C args" notation or from a custom user notation *) - let pl' = insert_local_defs_in_pattern cstr pl in - let maxargs = Inductiveops.constructor_nalldecls env cstr in - if List.length pl' + List.length args > maxargs then - error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs env cstr); - (* Two possibilities: either the args are given with explicit - variables for local definitions, then we give the explicit args - extended with local defs, so that there is nothing more to be - added later on; or the args are not enough to have all arguments, - which a priori means local defs to add in the [args] part, so we - postpone the insertion of local defs in the explicit args *) - (* Note: further checks done later by check_constructor_length *) - if List.length pl' + List.length args = maxargs then pl' else pl - | _ -> pl - -let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 = - let impl_list = if Int.equal len_pl1 0 - then select_impargs_size (List.length pl2) impls_st - else List.skipn_at_least len_pl1 (select_stronger_impargs impls_st) in - let remaining_args = List.fold_left (fun i x -> if is_status_implicit x then i else succ i) in - let rec aux i = function - |[],l -> let args_len = List.length l + List.length impl_list + len_pl1 in - ((if Int.equal args_len nargs then false - else Int.equal args_len nargs_with_letin || (fst (fail (nargs - List.length impl_list + i)))) - ,l) - |imp::q as il,[] -> if is_status_implicit imp && maximal_insertion_of imp - then let (b,out) = aux i (q,[]) in (b,(DAst.make @@ RCPatAtom None)::out) - else fail (remaining_args (len_pl1+i) il) - |imp::q,(hh::tt as l) -> if is_status_implicit imp - then let (b,out) = aux i (q,l) in (b,(DAst.make @@ RCPatAtom None)::out) - else let (b,out) = aux (succ i) (q,tt) in (b,hh::out) - in aux 0 (impl_list,pl2) - -let add_implicits_check_constructor_length env loc c len_pl1 pl2 = - let nargs = Inductiveops.constructor_nallargs env c in - let nargs' = Inductiveops.constructor_nalldecls env c in - let impls_st = implicits_of_global (GlobRef.ConstructRef c) in - add_implicits_check_length (error_wrong_numarg_constructor ?loc env c) - nargs nargs' impls_st len_pl1 pl2 - -let add_implicits_check_ind_length env loc c len_pl1 pl2 = - let nallargs = inductive_nallargs env c in - let nalldecls = inductive_nalldecls env c in - let impls_st = implicits_of_global (GlobRef.IndRef c) in - add_implicits_check_length (error_wrong_numarg_inductive ?loc env c) - nallargs nalldecls impls_st len_pl1 pl2 +let check_has_letin ?loc g expanded nargs nimps tags = + let expected_ndecls = List.length tags - nimps in + let expected_nassums = List.count (fun x -> not x) tags - nimps in + if nargs = expected_nassums then false + else if nargs = expected_ndecls then true else + let env = Global.env() in + match g with + | GlobRef.ConstructRef cstr -> error_wrong_numarg_constructor ?loc env ~cstr ~expanded ~nargs ~expected_nassums ~expected_ndecls + | GlobRef.IndRef ind -> error_wrong_numarg_inductive ?loc env ~ind ~expanded ~nargs ~expected_nassums ~expected_ndecls + | _ -> assert false (** Do not raise NotEnoughArguments thanks to preconditions*) let chop_params_pattern loc ind args with_letin = @@ -1432,9 +1442,9 @@ let chop_params_pattern loc ind args with_letin = | PatVar _ | PatCstr(_,_,_) -> error_parameter_not_implicit ?loc:c.CAst.loc) params; args -let find_constructor loc add_params ref = +let find_constructor_head ?loc ref = let open GlobRef in - let (ind,_ as cstr) = match ref with + match ref with | ConstructRef cstr -> cstr | IndRef _ -> let error = str "There is an inductive name deep in a \"in\" clause." in @@ -1442,17 +1452,12 @@ let find_constructor loc add_params ref = | ConstRef _ | VarRef _ -> let error = str "This reference is not a constructor." in user_err ?loc ~hdr:"find_constructor" error - in - cstr, match add_params with - | Some nb_args -> - let env = Global.env () in - let nb = - if Int.equal nb_args (Inductiveops.constructor_nrealdecls env cstr) - then Inductiveops.inductive_nparamdecls env ind - else Inductiveops.inductive_nparams env ind - in - List.make nb ([], [(Id.Map.empty, DAst.make @@ PatVar Anonymous)]) - | None -> [] + +let find_inductive_head ?loc ref = + let open GlobRef in + match ref with + | IndRef ind -> ind + | _ -> error_bad_inductive_type ?loc () let find_pattern_variable qid = if qualid_is_ident qid then qualid_basename qid @@ -1467,10 +1472,6 @@ let check_duplicate ?loc fields = user_err ?loc (str "This record defines several times the field " ++ pr_qualid r ++ str ".") -let inductive_of_record loc record = - let inductive = GlobRef.IndRef (inductive_of_constructor record.Recordops.s_CONST) in - Nametab.shortest_qualid_of_global ?loc Id.Set.empty inductive - (** [sort_fields ~complete loc fields completer] expects a list [fields] of field assignments [f = e1; g = e2; ...], where [f, g] are fields of a record and [e1] are "values" (either terms, when @@ -1488,16 +1489,7 @@ let sort_fields ~complete loc fields completer = match fields with | [] -> None | (first_field_ref, _):: _ -> - let (first_field_glob_ref, record) = - try - let gr = locate_reference first_field_ref in - Dumpglob.add_glob ?loc:first_field_ref.CAst.loc gr; - (gr, Recordops.find_projection gr) - with Not_found as exn -> - let _, info = Exninfo.capture exn in - let info = Option.cata (Loc.add_loc info) info loc in - Exninfo.iraise (InternalizationError(NotAProjection first_field_ref), info) - in + let (first_field_glob_ref, record) = intern_projection first_field_ref in (* the number of parameters *) let nparams = record.Recordops.s_EXPECTEDPARAM in (* the reference constructor of the record *) @@ -1516,25 +1508,14 @@ let sort_fields ~complete loc fields completer = let rec index_fields fields remaining_projs acc = match fields with | (field_ref, field_value) :: fields -> - let field_glob_ref = try locate_reference field_ref - with Not_found -> - user_err ?loc:field_ref.CAst.loc ~hdr:"intern" - (str "The field \"" ++ pr_qualid field_ref ++ str "\" does not exist.") in + let field_glob_ref,this_field_record = intern_projection field_ref in let remaining_projs, (field_index, _, regular) = let the_proj = function | (idx, Some glob_id, _) -> GlobRef.equal field_glob_ref (GlobRef.ConstRef glob_id) | (idx, None, _) -> false in try CList.extract_first the_proj remaining_projs with Not_found -> - let floc = field_ref.CAst.loc in - let this_field_record = - try Recordops.find_projection field_glob_ref - with Not_found -> - let inductive_ref = inductive_of_record floc record in - Loc.raise ?loc:floc (InternalizationError(NotAProjectionOf (field_ref, inductive_ref))) in - let ind1 = inductive_of_record floc record in - let ind2 = inductive_of_record floc this_field_record in - Loc.raise ?loc (InternalizationError(ProjectionsOfDifferentRecords (ind1, ind2))) + Loc.raise ?loc (InternalizationError(ProjectionsOfDifferentRecords (record, this_field_record))) in if not regular && complete then (* "regular" is false when the field is defined @@ -1587,8 +1568,8 @@ let merge_aliases aliases {loc;v=na} = { alias_ids; alias_map; } let alias_of als = match als.alias_ids with -| [] -> Anonymous -| {v=id} :: _ -> Name id + | [] -> Anonymous + | {v=id} :: _ -> Name id (** {6 Expanding notations } @@ -1614,29 +1595,33 @@ 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 ({v=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) + | RCPatCstr (id,l) -> + RCPatCstr (id,List.map (subst_pat_iterator y t) l) | RCPatAlias (p,a) -> RCPatAlias (subst_pat_iterator y t p,a) | RCPatOr pl -> RCPatOr (List.map (subst_pat_iterator y t) pl))) let is_non_zero c = match c with -| { CAst.v = CPrim (Number p) } -> not (NumTok.Signed.is_zero p) -| _ -> false + | { CAst.v = CPrim (Number p) } -> not (NumTok.Signed.is_zero p) + | _ -> false let is_non_zero_pat c = match c with -| { CAst.v = CPatPrim (Number p) } -> not (NumTok.Signed.is_zero p) -| _ -> false + | { CAst.v = CPatPrim (Number p) } -> not (NumTok.Signed.is_zero p) + | _ -> false let get_asymmetric_patterns = Goptions.declare_bool_option_and_ref ~depr:false ~key:["Asymmetric";"Patterns"] ~value:false +type global_reference_test = { + for_ind : bool; + test_kind : ?loc:Loc.t -> GlobRef.t -> unit +} + let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat = (* At toplevel, Constructors and Inductives are accepted, in recursive calls only constructor are allowed *) - let ensure_kind test_kind ?loc g = + let ensure_kind {test_kind} ?loc g = try test_kind ?loc g with Not_found -> error_invalid_pattern_notation ?loc () @@ -1644,60 +1629,47 @@ let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat = (* [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 (CAst.make ?loc:x.loc id,scopes)) - | GHole (_,_,_) -> RCPatAtom (None) - | GRef (g,_) -> RCPatCstr (g,[],[]) + | GHole (_,_,_) -> RCPatAtom None + | GRef (g,_) -> RCPatCstr (g, []) | GApp (r, l) -> begin match DAst.get r with | GRef (g,_) -> let allscs = find_arguments_scope g in - let allscs = simple_adjust_scopes (List.length l) allscs in (* TO CHECK *) - RCPatCstr (g, List.map2 (fun sc a -> rcp_of_glob (sc,snd scopes) a) allscs l,[]) + let allscs = simple_adjust_scopes (List.length l) allscs in + RCPatCstr (g, List.map2 (fun sc a -> rcp_of_glob (sc,snd scopes) a) allscs l) | _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr.") end | _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr."))) x in - let rec drop_syndef test_kind ?loc scopes qid pats = + let make_pars ?loc g = + let env = Global.env () in + let n = match g with + | GlobRef.ConstructRef (ind,_) -> Inductiveops.inductive_nparams env ind + | _ -> 0 in + List.make n (DAst.make ?loc @@ RCPatAtom None) + in + let rec drop_syndef {test_kind} ?loc scopes qid add_par_if_no_ntn_with_par no_impl pats = try - if qualid_is_ident qid && Option.cata (Id.Set.mem (qualid_basename qid)) false env.pat_ids then + if qualid_is_ident qid && Option.cata (Id.Set.mem (qualid_basename qid)) false env.pat_ids && List.is_empty pats then raise Not_found; - match Nametab.locate_extended qid with - | SynDef sp -> - let filter (vars,a) = - try match a with - | NRef g -> - (* Convention: do not deactivate implicit arguments and scopes for further arguments *) - test_kind ?loc g; - let () = assert (List.is_empty vars) in - let (_,argscs) = find_remaining_scopes [] pats g in - Some (g, [], List.map2 (in_pat_sc scopes) argscs pats) - | NApp (NRef g,[]) -> (* special case: Syndef for @Cstr deactivates implicit arguments *) - test_kind ?loc g; - let () = assert (List.is_empty vars) in - let (_,argscs) = find_remaining_scopes [] pats g in - Some (g, List.map2 (in_pat_sc scopes) argscs pats, []) - | NApp (NRef g,args) -> - (* Convention: do not deactivate implicit arguments and scopes for further arguments *) - test_kind ?loc g; - let nvars = List.length vars in - if List.length pats < nvars then error_not_enough_arguments ?loc:qid.loc; - let pats1,pats2 = List.chop nvars pats in - let subst = split_by_type_pat vars (pats1,[]) in - let idspl1 = List.map (in_not test_kind_inner qid.loc scopes subst []) args in - let (_,argscs) = find_remaining_scopes pats1 pats2 g in - Some (g, idspl1, List.map2 (in_pat_sc scopes) argscs pats2) - | _ -> raise Not_found - with Not_found -> None in - Syntax_def.search_filtered_syntactic_definition filter sp - | TrueGlobal g -> - test_kind ?loc g; - Dumpglob.add_glob ?loc:qid.loc g; - let (_,argscs) = find_remaining_scopes [] pats g in - Some (g,[],List.map2 (in_pat_sc scopes) argscs pats) + let intern_not subst pat = in_not test_kind_inner qid.loc scopes subst [] pat in + let g, expanded, ntnpats, pats = intern_qualid_for_pattern (test_kind ?loc) intern_not qid pats in + match ntnpats with + | None -> + (* deactivate implicit *) + let ntnpats = if add_par_if_no_ntn_with_par then make_pars ?loc g else [] in + Some (g, in_patargs ?loc scopes g expanded true ntnpats pats) + | Some ntnpats -> + let ntnpats = if add_par_if_no_ntn_with_par && ntnpats = [] then make_pars ?loc g else ntnpats in + Some (g, in_patargs ?loc scopes g expanded no_impl ntnpats pats) with Not_found -> None - and in_pat test_kind scopes pt = + and in_pat ({for_ind} as test_kind) scopes pt = let open CAst in let loc = pt.loc in + (* The two policies implied by asymmetric pattern mode *) + let add_par_if_no_ntn_with_par = get_asymmetric_patterns () && not for_ind in + let no_impl = get_asymmetric_patterns () && not for_ind in match pt.v with | CPatAlias (p, id) -> DAst.make ?loc @@ RCPatAlias (in_pat test_kind scopes p, id) | CPatRecord l -> @@ -1706,36 +1678,22 @@ let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat = begin match sorted_fields with | None -> DAst.make ?loc @@ RCPatAtom None | Some (n, head, pl) -> - let pl = - let pars = List.make n (CAst.make ?loc @@ CPatAtom None) in - List.rev_append pars pl - in - let (_,argscs) = find_remaining_scopes [] pl head in - let pats = List.map2 (in_pat_sc scopes) argscs pl in - DAst.make ?loc @@ RCPatCstr(head, pats, []) + let pars = make_pars ?loc head in + let pats = in_patargs ?loc scopes head true true pars pl in + DAst.make ?loc @@ RCPatCstr(head, pats) end | CPatCstr (head, None, pl) -> begin - match drop_syndef test_kind ?loc scopes head pl with - | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c) - | None -> Loc.raise ?loc (InternalizationError (NotAConstructor head)) + match drop_syndef test_kind ?loc scopes head add_par_if_no_ntn_with_par no_impl pl with + | Some (g,pl) -> DAst.make ?loc @@ RCPatCstr(g, pl) + | None -> Loc.raise ?loc (InternalizationError (NotAConstructor head)) end | CPatCstr (qid, Some expl_pl, pl) -> - let g = - try Nametab.locate qid - with Not_found as exn -> - let _, info = Exninfo.capture exn in - let info = Option.cata (Loc.add_loc info) info loc in - Exninfo.iraise (InternalizationError (NotAConstructor qid), info) - in - if expl_pl == [] then - (* Convention: (@r) deactivates all further implicit arguments and scopes *) - DAst.make ?loc @@ RCPatCstr (g, List.map (in_pat test_kind_inner scopes) pl, []) - else - (* Convention: (@r expl_pl) deactivates implicit arguments in expl_pl and in pl *) - (* but not scopes in expl_pl *) - let (argscs1,_) = find_remaining_scopes expl_pl pl g in - DAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat test_kind_inner scopes) pl, []) + begin + match drop_syndef test_kind ?loc scopes qid false true (expl_pl@pl) with + | Some (g,pl) -> DAst.make ?loc @@ RCPatCstr (g, pl) + | None -> Loc.raise ?loc (InternalizationError (NotAConstructor qid)) + end | CPatNotation (_,(InConstrEntry,"- _"),([a],[]),[]) when is_non_zero_pat a -> let p = match a.CAst.v with CPatPrim (Number (_, p)) -> p | _ -> assert false in let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind test_kind_inner) (Number (SMinus,p)) scopes in @@ -1751,20 +1709,20 @@ let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat = | CPatDelimiters (key, e) -> in_pat test_kind (None,find_delimiters_scope ?loc key::snd scopes) e | CPatPrim p -> - let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc test_kind_inner p scopes in + let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc test_kind_inner.test_kind p scopes in rcp_of_glob scopes pat | CPatAtom (Some id) -> begin - match drop_syndef test_kind ?loc scopes id [] with - | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr (a, b, c) - | None -> DAst.make ?loc @@ RCPatAtom (Some ((make ?loc @@ find_pattern_variable id),scopes)) + match drop_syndef test_kind ?loc scopes id add_par_if_no_ntn_with_par no_impl [] with + | Some (g, pl) -> DAst.make ?loc @@ RCPatCstr (g, pl) + | None -> DAst.make ?loc @@ RCPatAtom (Some ((make ?loc @@ find_pattern_variable id),scopes)) end | CPatAtom None -> DAst.make ?loc @@ RCPatAtom None | CPatOr pl -> DAst.make ?loc @@ RCPatOr (List.map (in_pat test_kind scopes) pl) | CPatCast (_,_) -> (* We raise an error if the pattern contains a cast, due to current restrictions on casts in patterns. Cast in patterns - are supported only in local binders and only at top level. + are supported only in local binders and only at for_ind level. The only reason they are in the [cases_pattern_expr] type is that the parser needs to factor the "c : t" notation with user defined notations. In the long term, we will try to @@ -1774,7 +1732,46 @@ let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat = duplicating the levels of the [pattern] rule. *) CErrors.user_err ?loc (Pp.strbrk "Casts are not supported in this pattern.") and in_pat_sc scopes x = in_pat test_kind_inner (x,snd scopes) - and in_not (test_kind:?loc:Loc.t->'a->'b) loc scopes (subst,substlist as fullsubst) args = function + and in_patargs ?loc scopes + gr (* head of the pattern *) + expanded (* tell if comes from a notation (for error reporting) *) + no_impl (* tell if implicit are not expected (for asymmetric patterns, or @, or {| |} *) + ntnpats (* prefix of patterns obtained by expansion of notations or parameter insertion *) + pats (* user given patterns *) + = + let default = DAst.make ?loc @@ RCPatAtom None in + let npats = List.length pats in + let n = List.length ntnpats in + let ntnpats_with_letin, tags = + let tags = match gr with + | GlobRef.ConstructRef cstr -> constructor_alltags (Global.env()) cstr + | GlobRef.IndRef ind -> inductive_alltags (Global.env()) ind + | _ -> assert false in + let ntnpats_with_letin = adjust_to_up tags ntnpats default in + ntnpats_with_letin, List.skipn (List.length ntnpats_with_letin) tags in + let imps = + let imps = + if no_impl then [] else + let impls_st = implicits_of_global gr in + if Int.equal n 0 then select_impargs_size npats impls_st + else List.skipn_at_least n (select_stronger_impargs impls_st) in + adjust_to_down tags imps None in + let subscopes = adjust_to_down tags (List.skipn_at_least n (find_arguments_scope gr)) None in + let has_letin = check_has_letin ?loc gr expanded npats (List.count is_status_implicit imps) tags in + let rec aux imps subscopes tags pats = + match imps, subscopes, tags, pats with + | _, _, true::tags, p::pats when has_letin -> + in_pat_sc scopes None p :: aux imps subscopes tags pats + | _, _, true::tags, _ -> + default :: aux imps subscopes tags pats + | imp::imps, sc::subscopes, false::tags, _ when is_status_implicit imp -> + default :: aux imps subscopes tags pats + | imp::imps, sc::subscopes, false::tags, p::pats -> + in_pat_sc scopes sc p :: aux imps subscopes tags pats + | _, _, [], [] -> [] + | _ -> assert false in + ntnpats_with_letin @ aux imps subscopes tags pats + and in_not test_kind loc scopes (subst,substlist as fullsubst) args = function | NVar id -> let () = assert (List.is_empty args) in begin @@ -1789,22 +1786,15 @@ let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat = end | NRef g -> ensure_kind test_kind ?loc g; - let (_,argscs) = find_remaining_scopes [] args g in - DAst.make ?loc @@ RCPatCstr (g, [], List.map2 (in_pat_sc scopes) argscs args) - | NApp (NRef g,pl) -> + DAst.make ?loc @@ RCPatCstr (g, in_patargs ?loc scopes g true false [] args) + | NApp (NRef g,ntnpl) -> ensure_kind test_kind ?loc g; - let (argscs1,argscs2) = find_remaining_scopes pl args g in - let pl = List.map2 (fun x -> in_not test_kind_inner loc (x,snd scopes) fullsubst []) argscs1 pl in - let pl = add_local_defs_and_check_length loc genv g pl args in - let args = List.map2 (fun x -> in_pat test_kind_inner (x,snd scopes)) argscs2 args in - let pat = - if List.length pl = 0 then - (* Convention: if notation is @f, encoded as NApp(Nref g,[]), then - implicit arguments are not inherited *) - RCPatCstr (g, pl @ args, []) - else - RCPatCstr (g, pl, args) in - DAst.make ?loc @@ pat + let ntnpl = List.map (in_not test_kind_inner loc scopes fullsubst []) ntnpl in + let no_impl = + (* Convention: if notation is @f, encoded as NApp(Nref g,[]), then + implicit arguments are not inherited *) + ntnpl = [] in + DAst.make ?loc @@ RCPatCstr (g, in_patargs ?loc scopes g true no_impl ntnpl args) | NList (x,y,iter,terminator,revert) -> if not (List.is_empty args) then user_err ?loc (strbrk "Application of arguments to a recursive notation not supported in patterns."); @@ -1837,23 +1827,14 @@ let rec intern_pat genv ntnvars aliases pat = | RCPatAlias (p, id) -> let aliases' = merge_aliases aliases id in intern_pat genv ntnvars aliases' p - | RCPatCstr (head, expl_pl, pl) -> - if get_asymmetric_patterns () then - let len = if List.is_empty expl_pl then Some (List.length pl) else None in - let c,idslpl1 = find_constructor loc len head in - let with_letin = - 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@pl) - else - let c,idslpl1 = find_constructor loc None head in - 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) + | RCPatCstr (head, pl) -> + let c = find_constructor_head ?loc head in + intern_cstr_with_all_args loc c true [] pl | RCPatAtom (Some ({loc;v=id},scopes)) -> let aliases = merge_aliases aliases (make ?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) -> + | RCPatAtom None -> let { alias_ids = ids; alias_map = asubst; } = aliases in (ids, [asubst, DAst.make ?loc @@ PatVar (alias_of aliases)]) | RCPatOr pl -> @@ -1865,8 +1846,9 @@ let rec intern_pat genv ntnvars aliases pat = (ids,List.flatten pl') let intern_cases_pattern test_kind genv ntnvars env aliases pat = + let test = {for_ind=false;test_kind} in intern_pat genv ntnvars aliases - (drop_notations_pattern (test_kind,test_kind) genv env pat) + (drop_notations_pattern (test,test) genv env pat) let _ = intern_cases_pattern_fwd := @@ -1886,21 +1868,21 @@ let intern_ind_pattern genv ntnvars env pat = raise Not_found in let no_not = try - drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat + let test_top = {for_ind=true;test_kind=test_kind_top} in + let test_inner = {for_ind=false;test_kind=test_kind_inner} in + drop_notations_pattern (test_top,test_inner) genv env pat with InternalizationError (NotAConstructor _) as exn -> let _, info = Exninfo.capture exn in error_bad_inductive_type ~info () in let loc = no_not.CAst.loc in match DAst.get no_not with - | RCPatCstr (head, expl_pl, pl) -> - let c = (function GlobRef.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 idslpl = List.map (intern_pat genv ntnvars empty_alias) (expl_pl@pl2) in - (with_letin, + | RCPatCstr (head, pl) -> + let ind = find_inductive_head ?loc head in + let idslpl = List.map (intern_pat genv ntnvars empty_alias) pl in + (true, match product_of_cases_patterns empty_alias idslpl with - | ids,[asubst,pl] -> (c,ids,asubst,chop_params_pattern loc c pl with_letin) + | ids,[asubst,pl] -> (ind,ids,asubst,chop_params_pattern loc ind pl true) | _ -> error_bad_inductive_type ?loc ()) | x -> error_bad_inductive_type ?loc () @@ -1961,17 +1943,22 @@ let extract_explicit_arg imps args = (Id.Map.add id (loc, a) eargs, rargs) in aux args +let extract_regular_arguments args = + List.map_filter (function + | (a,Some pos) -> user_err ?loc:pos.loc (str "Unexpected explicit argument.") + | (a,None) -> Some a) args + (**********************************************************************) (* Main loop *) let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let rec intern env = CAst.with_loc_val (fun ?loc -> function | CRef (ref,us) -> - let (c,imp,subscopes),_ = + let c,_ = intern_applied_reference ~isproj:None intern env (Environ.named_context_val globalenv) lvar us [] ref in - apply_impargs c env imp subscopes [] loc + apply_impargs env loc c [] | CFix ({ CAst.loc = locid; v = iddef}, dl) -> let lf = List.map (fun ({CAst.v = id},_,_,_,_) -> id) dl in @@ -2070,8 +2057,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | CNotation (_,(InConstrEntry,"( _ )"),([a],[],[],[])) -> intern env a | CNotation (_,ntn,args) -> let c = intern_notation intern env ntnvars loc ntn args in - let x, impl, scopes = find_appl_head_data c in - apply_impargs x env impl scopes [] loc + apply_impargs env loc c [] | CGeneralization (b,a,c) -> intern_generalization intern env ntnvars loc b a c | CPrim p -> @@ -2080,12 +2066,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = intern {env with tmp_scope = None; scopes = find_delimiters_scope ?loc key :: env.scopes} e | CAppExpl ((isproj,ref,us), args) -> - let (f,_,args_scopes),args = + let f,args = let args = List.map (fun a -> (a,None)) args in intern_applied_reference ~isproj intern env (Environ.named_context_val globalenv) lvar us args ref in check_not_notation_variable f ntnvars; + let _,args_scopes = find_appl_head_data env lvar f in (* Rem: GApp(_,f,[]) stands for @f *) if args = [] then DAst.make ?loc @@ GApp (f,[]) else smart_gapp f loc (intern_args env args_scopes (List.map fst args)) @@ -2097,22 +2084,21 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = isproj',f,args'@args (* Don't compact "(f args') args" to resolve implicits separately *) | _ -> isproj,f,args in - let (c,impargs,args_scopes),args = - match f.CAst.v with + (match f.CAst.v with | CRef (ref,us) -> - intern_applied_reference ~isproj intern env - (Environ.named_context_val globalenv) lvar us args ref + let f, args = intern_applied_reference ~isproj intern env + (Environ.named_context_val globalenv) lvar us args ref in + apply_impargs env loc f args | CNotation (_,ntn,ntnargs) -> assert (Option.is_empty isproj); let c = intern_notation intern env ntnvars loc ntn ntnargs in - find_appl_head_data c, args + apply_impargs env loc c args | _ -> - assert (Option.is_empty isproj); - let f = intern_no_implicit env f in - let f, _, args_scopes = find_appl_head_data f in - (f,[],args_scopes), args - in - apply_impargs c env impargs args_scopes args loc + assert (Option.is_empty isproj); + let f = intern_no_implicit env f in + let _, args_scopes = find_appl_head_data env lvar f in + let args = extract_regular_arguments args in + smart_gapp f loc (intern_args env args_scopes args)) | CRecord fs -> let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in @@ -2262,12 +2248,12 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = (* end *) | CSort s -> DAst.make ?loc @@ - GSort s + GSort (intern_sort ~local_univs:env.local_univs s) | CCast (c1, c2) -> DAst.make ?loc @@ GCast (intern env c1, map_cast_type (intern_type (slide_binders env)) c2) | CArray(u,t,def,ty) -> - DAst.make ?loc @@ GArray(u, Array.map (intern env) t, intern env def, intern env ty) + DAst.make ?loc @@ GArray(intern_instance ~local_univs:env.local_univs u, Array.map (intern env) t, intern env def, intern env ty) ) and intern_type env = intern (set_type_scope env) @@ -2407,10 +2393,11 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = intern_args env subscopes rargs in aux 1 l subscopes eargs rargs - and apply_impargs c env imp subscopes l loc = - let imp = select_impargs_size (List.length (List.filter (fun (_,x) -> x == None) l)) imp in - let l = intern_impargs c env imp subscopes l in - smart_gapp c loc l + and apply_impargs env loc c args = + let impl, subscopes = find_appl_head_data env lvar c in + let imp = select_impargs_size (List.length (List.filter (fun (_,x) -> x == None) args)) impl in + let args = intern_impargs c env imp subscopes args in + smart_gapp c loc args and smart_gapp f loc = function | [] -> f @@ -2439,6 +2426,8 @@ let extract_ids env = (Termops.ids_of_rel_context (Environ.rel_context env)) Id.Set.empty +let bound_univs sigma = Evd.universe_binders sigma + let scope_of_type_kind env sigma = function | IsType -> Notation.current_type_scope_name () | OfType typ -> compute_type_scope env sigma typ @@ -2461,8 +2450,9 @@ let intern_gen kind env sigma let tmp_scope = scope_of_type_kind env sigma kind in let k = allowed_binder_kind_of_type_kind kind in internalize env {ids = extract_ids env; unb = false; - tmp_scope = tmp_scope; scopes = []; - impls; binder_block_names = Some (k,Id.Map.domain impls)} + local_univs = { bound = bound_univs sigma; unb_univs = true }; + tmp_scope = tmp_scope; scopes = []; + impls; binder_block_names = Some (k,Id.Map.domain impls)} pattern_mode (ltacvars, Id.Map.empty) c let intern_constr env sigma c = intern_gen WithoutTypeConstraint env sigma c @@ -2551,7 +2541,9 @@ let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign) let impls = empty_internalization_env in let k = allowed_binder_kind_of_type_kind kind in internalize env - {ids; unb = false; tmp_scope; scopes = []; impls; + {ids; unb = false; + local_univs = { bound = bound_univs sigma; unb_univs = true }; + tmp_scope; scopes = []; impls; binder_block_names = Some (k,Id.Set.empty)} pattern_mode (ltacvars, vl) c @@ -2561,8 +2553,11 @@ let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = let vl = Id.Map.map (fun typ -> (ref false, ref None, typ)) nenv.ninterp_var_type in let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in let c = internalize env - {ids; unb = false; tmp_scope = None; scopes = []; impls; binder_block_names = None} - false (empty_ltac_sign, vl) a in + {ids; unb = false; + local_univs = { bound = Id.Map.empty; unb_univs = false }; + tmp_scope = None; scopes = []; impls; binder_block_names = None} + false (empty_ltac_sign, vl) a + in (* Splits variables into those that are binding, bound, or both *) (* Translate and check that [c] has all its free variables bound in [vars] *) let a, reversible = notation_constr_of_glob_constr nenv c in @@ -2589,7 +2584,7 @@ let interp_binder_evars env sigma na t = let my_intern_constr env lvar acc c = internalize env acc false lvar c -let intern_context env impl_env binders = +let intern_context env ~bound_univs impl_env binders = let lvar = (empty_ltac_sign, Id.Map.empty) in let ids = (* We assume all ids around are parts of the prefix of the current @@ -2600,6 +2595,7 @@ let intern_context env impl_env binders = let (env, bl) = intern_local_binder_aux (my_intern_constr env lvar) Id.Map.empty (lenv, bl) b in (env, bl)) ({ids; unb = false; + local_univs = { bound = bound_univs; unb_univs = true }; tmp_scope = None; scopes = []; impls = impl_env; binder_block_names = Some (Some AbsPi,ids)}, []) binders in (lenv.impls, List.map glob_local_binder_of_extended bl) @@ -2636,17 +2632,21 @@ let interp_glob_context_evars ?(program_mode=false) env sigma bl = sigma, ((env, par), List.rev impls) let interp_context_evars ?program_mode ?(impl_env=empty_internalization_env) env sigma params = - let int_env,bl = intern_context env impl_env params in + let int_env,bl = intern_context env ~bound_univs:(bound_univs sigma) impl_env params in let sigma, x = interp_glob_context_evars ?program_mode env sigma bl in sigma, (int_env, x) (** Local universe and constraint declarations. *) +let interp_known_level evd u = + let u = intern_sort_name ~local_univs:{bound = bound_univs evd; unb_univs=false} u in + Pretyping.known_glob_level evd u + let interp_univ_constraints env evd cstrs = let interp (evd,cstrs) (u, d, u') = - let ul = Pretyping.interp_known_glob_level evd u in - let u'l = Pretyping.interp_known_glob_level evd u' in + let ul = interp_known_level evd u in + let u'l = interp_known_level evd u' in let cstr = (ul,d,u'l) in let cstrs' = Univ.Constraint.add cstr cstrs in try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 0de6c3e89d..f92a54e23f 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -88,7 +88,8 @@ val intern_gen : typing_constraint -> env -> evar_map -> val intern_pattern : env -> cases_pattern_expr -> lident list * (Id.t Id.Map.t * cases_pattern) list -val intern_context : env -> internalization_env -> local_binder_expr list -> internalization_env * glob_decl list +val intern_context : env -> bound_univs:UnivNames.universe_binders -> + internalization_env -> local_binder_expr list -> internalization_env * glob_decl list (** {6 Composing internalization with type inference (pretyping) } *) @@ -198,6 +199,8 @@ val check_duplicate : ?loc:Loc.t -> (qualid * constr_expr) list -> unit (** Check that a list of record field definitions doesn't contain duplicates. *) +val interp_known_level : Evd.evar_map -> sort_name_expr -> Univ.Level.t + (** Local universe and constraint declarations. *) val interp_univ_decl : Environ.env -> universe_decl_expr -> Evd.evar_map * UState.universe_decl diff --git a/interp/notation.ml b/interp/notation.ml index b5951a9c59..f2d113954b 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -62,10 +62,11 @@ let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2 let notation_binder_source_eq s1 s2 = match s1, s2 with | NtnParsedAsIdent, NtnParsedAsIdent -> true +| NtnParsedAsName, NtnParsedAsName -> true | NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2 | NtnBinderParsedAsConstr bk1, NtnBinderParsedAsConstr bk2 -> bk1 = bk2 | NtnParsedAsBinder, NtnParsedAsBinder -> true -| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _ | NtnParsedAsBinder), _ -> false +| (NtnParsedAsIdent | NtnParsedAsName | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _ | NtnParsedAsBinder), _ -> false let ntpe_eq t1 t2 = match t1, t2 with | NtnTypeConstr, NtnTypeConstr -> true @@ -639,7 +640,7 @@ let constr_of_globref allow_constant env sigma = function | GlobRef.IndRef c -> let sigma,c = Evd.fresh_inductive_instance env sigma c in sigma,mkIndU c - | GlobRef.ConstRef c when allow_constant -> + | GlobRef.ConstRef c when allow_constant || Environ.is_primitive_type env c -> let sigma,c = Evd.fresh_constant_instance env sigma c in sigma,mkConstU c | _ -> raise NotAValidPrimToken @@ -691,6 +692,13 @@ let rec constr_of_glob allow_constant to_post post env sigma g = match DAst.get sigma,mkApp (c, Array.of_list cl) end | Glob_term.GInt i -> sigma, mkInt i + | Glob_term.GFloat f -> sigma, mkFloat f + | Glob_term.GArray (_,t,def,ty) -> + let sigma, u' = Evd.fresh_array_instance env sigma in + let sigma, def' = constr_of_glob allow_constant to_post post env sigma def in + let sigma, t' = Array.fold_left_map (constr_of_glob allow_constant to_post post env) sigma t in + let sigma, ty' = constr_of_glob allow_constant to_post post env sigma ty in + sigma, mkArray (u',t',def',ty') | Glob_term.GSort gs -> let sigma,c = Evd.fresh_sort_in_family sigma (Glob_ops.glob_sort_family gs) in sigma,mkSort c @@ -711,6 +719,12 @@ let rec glob_of_constr token_kind ?loc env sigma c = match Constr.kind c with | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (GlobRef.IndRef ind, None)) | Var id -> DAst.make ?loc (Glob_term.GRef (GlobRef.VarRef id, None)) | Int i -> DAst.make ?loc (Glob_term.GInt i) + | Float f -> DAst.make ?loc (Glob_term.GFloat f) + | Array (u,t,def,ty) -> + let def' = glob_of_constr token_kind ?loc env sigma def + and t' = Array.map (glob_of_constr token_kind ?loc env sigma) t + and ty' = glob_of_constr token_kind ?loc env sigma ty in + DAst.make ?loc (Glob_term.GArray (None,t',def',ty')) | Sort Sorts.SProp -> DAst.make ?loc (Glob_term.GSort (Glob_term.UNamed [Glob_term.GSProp, 0])) | Sort Sorts.Prop -> DAst.make ?loc (Glob_term.GSort (Glob_term.UNamed [Glob_term.GProp, 0])) | Sort Sorts.Set -> DAst.make ?loc (Glob_term.GSort (Glob_term.UNamed [Glob_term.GSet, 0])) @@ -781,13 +795,7 @@ end let z_two = Z.of_int 2 (** Conversion from bigint to int63 *) -let rec int63_of_pos_bigint i = - if Z.(equal i zero) then Uint63.of_int 0 - else - let quo, remi = Z.div_rem i z_two in - if Z.(equal remi one) then Uint63.add (Uint63.of_int 1) - (Uint63.mul (Uint63.of_int 2) (int63_of_pos_bigint quo)) - else Uint63.mul (Uint63.of_int 2) (int63_of_pos_bigint quo) +let int63_of_pos_bigint i = Uint63.of_int64 (Z.to_int64 i) module Numbers = struct (** * Number notation *) @@ -1040,7 +1048,7 @@ let interp_int63 ?loc n = let bigint_of_int63 c = match Constr.kind c with - | Int i -> Z.of_string (Uint63.to_string i) + | Int i -> Z.of_int64 (Uint63.to_int64 i) | _ -> raise NotAValidPrimToken let interp o ?loc n = diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index f51d3bfdfb..0e7f085bde 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -863,7 +863,7 @@ let rec push_context_binders vars = function let vars = match DAst.get b with | GLocalAssum (na,_,_) -> Termops.add_vname vars na | GLocalPattern ((disjpat,ids),p,bk,t) -> List.fold_right Id.Set.add ids vars - | GLocalDef (na,_,_,_) -> Termops.add_vname vars na in + | GLocalDef (na,_,_) -> Termops.add_vname vars na in push_context_binders vars bl let is_term_meta id metas = @@ -881,7 +881,7 @@ let is_onlybinding_meta id metas = let is_onlybinding_pattern_like_meta isvar id metas = try match Id.List.assoc id metas with | _,NtnTypeBinder (NtnBinderParsedAsConstr - (AsIdentOrPattern | AsStrictPattern)) -> true + (AsNameOrPattern | AsStrictPattern)) -> true | _,NtnTypeBinder (NtnParsedAsPattern strict) -> not (strict && isvar) | _,NtnTypeBinder NtnParsedAsBinder -> not isvar | _ -> false @@ -1014,9 +1014,9 @@ let unify_binder_upto alp b b' = | GLocalAssum (na,bk,t), GLocalAssum (na',bk',t') -> let alp, na = unify_name_upto alp na na' in alp, DAst.make ?loc @@ GLocalAssum (na, unify_binding_kind bk bk', unify_term alp t t') - | GLocalDef (na,bk,c,t), GLocalDef (na',bk',c',t') -> + | GLocalDef (na,c,t), GLocalDef (na',c',t') -> let alp, na = unify_name_upto alp na na' in - alp, DAst.make ?loc @@ GLocalDef (na, unify_binding_kind bk bk', unify_term alp c c', unify_opt_term alp t t') + alp, DAst.make ?loc @@ GLocalDef (na, unify_term alp c c', unify_opt_term alp t t') | GLocalPattern ((disjpat,ids),id,bk,t), GLocalPattern ((disjpat',_),_,bk',t') when List.length disjpat = List.length disjpat' -> let alp, p = List.fold_left2_map unify_pat_upto alp disjpat disjpat' in alp, DAst.make ?loc @@ GLocalPattern ((p,ids), id, unify_binding_kind bk bk', unify_term alp t t') @@ -1061,7 +1061,7 @@ let rec unify_terms_binders alp cl bl' = | [], [] -> [] | c :: cl, b' :: bl' -> begin match DAst.get b' with - | GLocalDef ( _, _, _, t) -> unify_terms_binders alp cl bl' + | GLocalDef (_, _, t) -> unify_terms_binders alp cl bl' | _ -> unify_term_binder alp c b' :: unify_terms_binders alp cl bl' end | _ -> raise No_match @@ -1249,7 +1249,7 @@ let match_binderlist match_fun alp metas sigma rest x y iter termin revert = with No_match -> match DAst.get rest with | GLetIn (na,c,t,rest') when glue_inner_letin_with_decls -> - let b = DAst.make ?loc:rest.CAst.loc @@ GLocalDef (na,Explicit (*?*), c,t) in + let b = DAst.make ?loc:rest.CAst.loc @@ GLocalDef (na,c,t) in (* collect let-in *) (try aux true sigma (b::bl) rest' with OnlyTrailingLetIns @@ -1533,7 +1533,7 @@ let match_notation_constr ~print_univ c ~vars (metas,pat) = let v = glob_constr_of_cases_pattern (Global.env()) pat in (((vars,v),scl)::terms',termlists',binders',binderlists') | _ -> raise No_match) - | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnParsedAsBinder) -> + | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsName | NtnParsedAsPattern _ | NtnParsedAsBinder) -> (terms',termlists',(Id.List.assoc x binders,scl)::binders',binderlists') | NtnTypeConstrList -> (terms',(Id.List.assoc x termlists,scl)::termlists',binders',binderlists') diff --git a/interp/notation_term.ml b/interp/notation_term.ml index 29db23cc54..c541a19bfd 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -67,7 +67,8 @@ type extended_subscopes = Constrexpr.notation_entry_level * subscopes type constr_as_binder_kind = | AsIdent - | AsIdentOrPattern + | AsName + | AsNameOrPattern | AsStrictPattern type notation_binder_source = @@ -76,6 +77,8 @@ type notation_binder_source = | NtnParsedAsPattern of bool (* This accepts only ident *) | NtnParsedAsIdent + (* This accepts only name *) + | NtnParsedAsName (* This accepts ident, or pattern, or both *) | NtnBinderParsedAsConstr of constr_as_binder_kind (* This accepts ident, _, and quoted pattern *) diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 70be55f843..a953ca8898 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -37,6 +37,9 @@ let wit_pre_ident : string uniform_genarg_type = let wit_int_or_var = make0 ~dyn:(val_tag (topwit wit_int)) "int_or_var" +let wit_nat_or_var = + make0 ~dyn:(val_tag (topwit wit_nat)) "nat_or_var" + let wit_ident = make0 "ident" diff --git a/interp/stdarg.mli b/interp/stdarg.mli index bd34af5543..0a8fdf53b1 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -35,6 +35,8 @@ val wit_pre_ident : string uniform_genarg_type val wit_int_or_var : (int or_var, int or_var, int) genarg_type +val wit_nat_or_var : (int or_var, int or_var, int) genarg_type + val wit_ident : Id.t uniform_genarg_type val wit_hyp : (lident, lident, Id.t) genarg_type |