diff options
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 198 |
1 files changed, 121 insertions, 77 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 4f7d537d3f..19444988b9 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (*i*) @@ -213,7 +215,7 @@ let is_record indsp = let encode_record r = let indsp = global_inductive r in if not (is_record indsp) then - user_err ?loc:(loc_of_reference r) ~hdr:"encode_record" + user_err ?loc:r.CAst.loc ~hdr:"encode_record" (str "This type is not a structure type."); indsp @@ -257,7 +259,7 @@ let insert_pat_delimiters ?loc p = function let insert_pat_alias ?loc p = function | Anonymous -> p - | Name id -> CAst.make ?loc @@ CPatAlias (p,id) + | Name _ as na -> CAst.make ?loc @@ CPatAlias (p,(CAst.make ?loc na)) (**********************************************************************) (* conversion of references *) @@ -269,14 +271,14 @@ let extern_evar n l = CEvar (n,l) may be inaccurate *) let default_extern_reference ?loc vars r = - Qualid (Loc.tag ?loc @@ shortest_qualid_of_global vars r) + make @@ Qualid (shortest_qualid_of_global vars r) let my_extern_reference = ref default_extern_reference let set_extern_reference f = my_extern_reference := f let get_extern_reference () = !my_extern_reference -let extern_reference ?loc vars l = !my_extern_reference ?loc vars l +let extern_reference ?loc vars l = !my_extern_reference vars l (**********************************************************************) (* mapping patterns to cases_pattern_expr *) @@ -323,34 +325,35 @@ let is_zero s = Int.equal (String.length s) i || (s.[i] == '0' && aux (i+1)) in aux 0 -let make_notation_gen loc ntn mknot mkprim destprim l = +let make_notation_gen loc ntn mknot mkprim destprim l bl = match ntn,List.map destprim l with (* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *) | "- _", [Some (Numeral (p,true))] when not (is_zero p) -> - mknot (loc,ntn,([mknot (loc,"( _ )",l)])) + assert (bl=[]); + mknot (loc,ntn,([mknot (loc,"( _ )",l,[])]),[]) | _ -> match decompose_notation_key ntn, l with | [Terminal "-"; Terminal x], [] when is_number x -> mkprim (loc, Numeral (x,false)) | [Terminal x], [] when is_number x -> mkprim (loc, Numeral (x,true)) - | _ -> mknot (loc,ntn,l) + | _ -> mknot (loc,ntn,l,bl) -let make_notation loc ntn (terms,termlists,binders as subst) = - if not (List.is_empty termlists) || not (List.is_empty binders) then +let make_notation loc ntn (terms,termlists,binders,binderlists as subst) = + if not (List.is_empty termlists) || not (List.is_empty binderlists) then CAst.make ?loc @@ CNotation (ntn,subst) else make_notation_gen loc ntn - (fun (loc,ntn,l) -> CAst.make ?loc @@ CNotation (ntn,(l,[],[]))) + (fun (loc,ntn,l,bl) -> CAst.make ?loc @@ CNotation (ntn,(l,[],bl,[]))) (fun (loc,p) -> CAst.make ?loc @@ CPrim p) - destPrim terms + destPrim terms binders let make_pat_notation ?loc ntn (terms,termlists as subst) args = if not (List.is_empty termlists) then (CAst.make ?loc @@ CPatNotation (ntn,subst,args)) else make_notation_gen loc ntn - (fun (loc,ntn,l) -> CAst.make ?loc @@ CPatNotation (ntn,(l,[]),args)) + (fun (loc,ntn,l,_) -> CAst.make ?loc @@ CPatNotation (ntn,(l,[]),args)) (fun (loc,p) -> CAst.make ?loc @@ CPatPrim p) - destPatPrim terms + destPatPrim terms [] let mkPat ?loc qid l = CAst.make ?loc @@ (* Normally irrelevant test with v8 syntax, but let's do it anyway *) @@ -383,10 +386,10 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = try if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match; extern_notation_pattern scopes vars pat - (uninterp_cases_pattern_notations scopes pat) + (uninterp_cases_pattern_notations pat) with No_match -> lift (fun ?loc -> function - | PatVar (Name id) -> CPatAtom (Some (Ident (loc,id))) + | PatVar (Name id) -> CPatAtom (Some (make ?loc @@ Ident id)) | PatVar (Anonymous) -> CPatAtom None | PatCstr(cstrsp,args,na) -> let args = List.map (extern_cases_pattern_in_scope scopes vars) args in @@ -404,7 +407,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = (* we don't want to have 'x := _' in our patterns *) acc | Some c, _ -> - ((extern_reference ?loc Id.Set.empty (ConstRef c), pat) :: acc) + ((extern_reference ?loc Id.Set.empty (ConstRef c), pat) :: acc) | _ -> raise No_match in ip q tail acc | _ -> assert false @@ -412,7 +415,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = CPatRecord(List.rev (ip projs args [])) with Not_found | No_match | Exit -> - let c = extern_reference ?loc Id.Set.empty (ConstructRef cstrsp) in + let c = extern_reference Id.Set.empty (ConstructRef cstrsp) in if !asymmetric_patterns then if pattern_printable_in_both_syntax cstrsp then CPatCstr (c, None, args) @@ -455,7 +458,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) (make_pat_notation ?loc ntn (l,ll) l2') key end | SynDefRule kn -> - let qid = Qualid (Loc.tag ?loc @@ shortest_qualid_of_syndef vars kn) in + let qid = make ?loc @@ Qualid (shortest_qualid_of_syndef vars kn) in let l1 = List.rev_map (fun (c,(scopt,scl)) -> extern_cases_pattern_in_scope (scopt,scl@scopes) vars c) @@ -481,7 +484,7 @@ and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function (match_notation_constr_cases_pattern t pat) allscopes vars keyrule in insert_pat_alias ?loc p na | PatVar Anonymous -> CAst.make ?loc @@ CPatAtom None - | PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (Ident (loc,id))) + | PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (make ?loc @@ Ident id)) with No_match -> extern_notation_pattern allscopes vars t rules @@ -514,7 +517,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = try if !Flags.raw_print || !print_no_symbol then raise No_match; extern_notation_ind_pattern scopes vars ind args - (uninterp_ind_pattern_notations scopes ind) + (uninterp_ind_pattern_notations ind) with No_match -> let c = extern_reference vars (IndRef ind) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in @@ -533,6 +536,10 @@ let occur_name na aty = | Name id -> occur_var_constr_expr id aty | Anonymous -> false +let is_gvar id c = match DAst.get c with +| GVar id' -> Id.equal id id' +| _ -> false + let is_projection nargs = function | Some r when not !Flags.in_debugger && not !Flags.raw_print && !print_projections -> (try @@ -569,7 +576,7 @@ let explicitize inctx impl (cf,f) args = is_significant_implicit (Lazy.force a)) in if visible then - (Lazy.force a,Some (Loc.tag @@ ExplByName (name_of_implicit imp))) :: tail + (Lazy.force a,Some (make @@ ExplByName (name_of_implicit imp))) :: tail else tail | a::args, _::impl -> (Lazy.force a,None) :: exprec (q+1) (args,impl) @@ -734,13 +741,13 @@ 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_notation scopes vars r'' (uninterp_notations scopes r'') + extern_notation scopes vars r'' (uninterp_notations r'') with No_match -> lift (fun ?loc -> function | GRef (ref,us) -> extern_global (select_stronger_impargs (implicits_of_global ref)) - (extern_reference ?loc vars ref) (extern_universes us) + (extern_reference vars ref) (extern_universes us) - | GVar id -> CRef (Ident (loc,id),None) + | GVar id -> CRef (make ?loc @@ Ident id,None) | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, Misctypes.IntroAnonymous, None) @@ -756,7 +763,6 @@ let rec extern inctx scopes vars r = | GApp (f,args) -> (match DAst.get f with | GRef (ref,us) -> - let rloc = f.CAst.loc in let subscopes = find_arguments_scope ref in let args = fill_arg_scopes args subscopes (snd scopes) in begin @@ -795,7 +801,7 @@ let rec extern inctx scopes vars r = (* we give up since the constructor is not complete *) | (arg, scopes) :: tail -> let head = extern true scopes vars arg in - ip q locs' tail ((extern_reference ?loc Id.Set.empty (ConstRef c), head) :: acc) + ip q locs' tail ((extern_reference ?loc Id.Set.empty (ConstRef c), head) :: acc) in CRecord (List.rev (ip projs locals args [])) with @@ -803,7 +809,7 @@ let rec extern inctx scopes vars r = let args = extern_args (extern true) vars args in extern_app inctx (select_stronger_impargs (implicits_of_global ref)) - (Some ref,extern_reference ?loc:rloc vars ref) (extern_universes us) args + (Some ref,extern_reference ?loc vars ref) (extern_universes us) args end | _ -> @@ -811,19 +817,17 @@ let rec extern inctx scopes vars r = (List.map (fun c -> lazy (sub_extern true scopes vars c)) args)) | GLetIn (na,b,t,c) -> - CLetIn ((loc,na),sub_extern false scopes vars b, + CLetIn (make ?loc na,sub_extern false scopes vars b, Option.map (extern_typ scopes vars) t, extern inctx scopes (add_vname vars na) c) | GProd (na,bk,t,c) -> let t = extern_typ scopes vars t in - let (idl,c) = factorize_prod scopes (add_vname vars na) na bk t c in - CProdN ([(Loc.tag na)::idl,Default bk,t],c) + factorize_prod scopes (add_vname vars na) na bk t c | GLambda (na,bk,t,c) -> let t = extern_typ scopes vars t in - let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) na bk t c in - CLambdaN ([(Loc.tag na)::idl,Default bk,t],c) + factorize_lambda inctx scopes (add_vname vars na) na bk t c | GCases (sty,rtntypopt,tml,eqns) -> let vars' = @@ -837,15 +841,15 @@ let rec extern inctx scopes vars r = | None -> None | Some ntn -> if occur_glob_constr id ntn then - Some (Loc.tag Anonymous) + Some (CAst.make Anonymous) else None end | Anonymous, _ -> None | Name id, GVar id' when Id.equal id id' -> None - | Name _, _ -> Some (Loc.tag na) in + | Name _, _ -> Some (CAst.make na) in (sub_extern false scopes vars tm, na', - Option.map (fun (loc,(ind,nal)) -> + 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 @@ -856,15 +860,15 @@ let rec extern inctx scopes vars r = CCases (sty,rtntypopt',tml,eqns) | GLetTuple (nal,(na,typopt),tm,b) -> - CLetTuple (List.map (fun na -> (Loc.tag na)) nal, - (Option.map (fun _ -> (Loc.tag na)) typopt, + CLetTuple (List.map CAst.make nal, + (Option.map (fun _ -> (make na)) typopt, Option.map (extern_typ scopes (add_vname vars na)) typopt), sub_extern false scopes vars tm, extern inctx scopes (List.fold_left add_vname vars nal) b) | GIf (c,(na,typopt),b1,b2) -> CIf (sub_extern false scopes vars c, - (Option.map (fun _ -> (Loc.tag na)) typopt, + (Option.map (fun _ -> (CAst.make na)) typopt, Option.map (extern_typ scopes (add_vname vars na)) typopt), sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2) @@ -882,13 +886,13 @@ let rec extern inctx scopes vars r = let n = match fst nv.(i) with | None -> None - | Some x -> Some (Loc.tag @@ Name.get_id (List.nth assums x)) + | Some x -> Some (CAst.make @@ Name.get_id (List.nth assums x)) in let ro = extern_recursion_order scopes vars (snd nv.(i)) in - ((Loc.tag fi), (n, ro), bl, extern_typ scopes vars0 ty, + ((CAst.make fi), (n, ro), bl, extern_typ scopes vars0 ty, extern false scopes vars1 def)) idv in - CFix ((loc,idv.(n)),Array.to_list listdecl) + CFix (CAst.(make ?loc idv.(n)), Array.to_list listdecl) | GCoFix n -> let listdecl = Array.mapi (fun i fi -> @@ -896,10 +900,10 @@ let rec extern inctx scopes vars r = 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 - ((Loc.tag fi),bl,extern_typ scopes vars0 tyv.(i), + ((CAst.make fi),bl,extern_typ scopes vars0 tyv.(i), sub_extern false scopes vars1 bv.(i))) idv in - CCoFix ((loc,idv.(n)),Array.to_list listdecl)) + CCoFix (CAst.(make ?loc idv.(n)),Array.to_list listdecl)) | GSort s -> CSort (extern_glob_sort s) @@ -919,24 +923,60 @@ and extern_typ (_,scopes) = and sub_extern inctx (_,scopes) = extern inctx (None,scopes) and factorize_prod scopes vars na bk aty c = - let c = extern_typ scopes vars c in - match na, c with - | Name id, { CAst.loc ; v = CProdN ([nal,Default bk',ty],c) } - when binding_kind_eq bk bk' && constr_expr_eq aty ty - && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) -> - nal,c - | _ -> - [],c + let store, get = set_temporary_memory () in + match na, DAst.get c with + | Name id, GCases (LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns)) + when is_gvar id e && List.length (store (factorize_eqns eqns)) = 1 -> + (match get () with + | [{CAst.v=(ids,disj_of_patl,b)}] -> + 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 binder = CLocalPattern (make ?loc:c.loc (p,None)) in + (match b.v with + | CProdN (bl,b) -> CProdN (binder::bl,b) + | _ -> CProdN ([binder],b)) + | _ -> assert false) + | _, _ -> + let c = extern_typ scopes vars c in + match na, c.v with + | Name id, CProdN (CLocalAssum(nal,Default bk',ty)::bl,b) + when binding_kind_eq bk bk' && constr_expr_eq aty ty + && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) -> + CProdN (CLocalAssum(make na::nal,Default bk,aty)::bl,b) + | _, CProdN (bl,b) -> + CProdN (CLocalAssum([make na],Default bk,aty)::bl,b) + | _, _ -> + CProdN ([CLocalAssum([make na],Default bk,aty)],c) and factorize_lambda inctx scopes vars na bk aty c = - let c = sub_extern inctx scopes vars c in - match c with - | { CAst.loc; v = CLambdaN ([nal,Default bk',ty],c) } - when binding_kind_eq bk bk' && constr_expr_eq aty ty - && not (occur_name na ty) (* avoid na in ty escapes scope *) -> - nal,c - | _ -> - [],c + let store, get = set_temporary_memory () in + match na, DAst.get c with + | Name id, GCases (LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns)) + when is_gvar id e && List.length (store (factorize_eqns eqns)) = 1 -> + (match get () with + | [{CAst.v=(ids,disj_of_patl,b)}] -> + 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 binder = CLocalPattern (make ?loc:c.loc (p,None)) in + (match b.v with + | CLambdaN (bl,b) -> CLambdaN (binder::bl,b) + | _ -> CLambdaN ([binder],b)) + | _ -> assert false) + | _, _ -> + let c = sub_extern inctx scopes vars c in + match c.v with + | CLambdaN (CLocalAssum(nal,Default bk',ty)::bl,b) + when binding_kind_eq bk bk' && constr_expr_eq aty ty + && not (occur_name na ty) (* avoid na in ty escapes scope *) -> + CLambdaN (CLocalAssum(make na::nal,Default bk,aty)::bl,b) + | CLambdaN (bl,b) -> + CLambdaN (CLocalAssum([make na],Default bk,aty)::bl,b) + | _ -> + CLambdaN ([CLocalAssum([make na],Default bk,aty)],c) and extern_local_binder scopes vars = function [] -> ([],[],[]) @@ -946,7 +986,7 @@ and extern_local_binder scopes vars = function let (assums,ids,l) = extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l in (assums,na::ids, - CLocalDef((Loc.tag na), extern false scopes vars bd, + CLocalDef(CAst.make na, extern false scopes vars bd, Option.map (extern false scopes vars) ty) :: l) | GLocalAssum (na,bk,ty) -> @@ -957,21 +997,21 @@ and extern_local_binder scopes vars = function match na with Name id -> not (occur_var_constr_expr id ty') | _ -> true -> (na::assums,na::ids, - CLocalAssum((Loc.tag na)::nal,k,ty')::l) + CLocalAssum(CAst.make na::nal,k,ty')::l) | (assums,ids,l) -> (na::assums,na::ids, - CLocalAssum([(Loc.tag na)],Default bk,ty) :: l)) + CLocalAssum([CAst.make na],Default bk,ty) :: l)) | GLocalPattern ((p,_),_,bk,ty) -> let ty = if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in - let p = extern_cases_pattern vars p in + let p = mkCPatOr (List.map (extern_cases_pattern vars) p) in let (assums,ids,l) = extern_local_binder scopes vars l in - (assums,ids, CLocalPattern(Loc.tag @@ (p,ty)) :: l) + (assums,ids, CLocalPattern(CAst.make @@ (p,ty)) :: l) -and extern_eqn inctx scopes vars (loc,(ids,pll,c)) = +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 - Loc.tag ?loc (pll,extern inctx scopes vars c) + make ?loc (pll,extern inctx scopes vars c) and extern_notation (tmp_scope,scopes as allscopes) vars t = function | [] -> raise No_match @@ -1014,7 +1054,7 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function | _, None -> t, [], [], [] | _ -> raise No_match in (* Try matching ... *) - let terms,termlists,binders = + let terms,termlists,binders,binderlists = match_notation_constr !print_universes t pat in (* Try availability of interpretation ... *) let e = @@ -1035,17 +1075,21 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function List.map (fun (c,(scopt,scl)) -> List.map (extern true (scopt,scl@scopes') vars) c) termlists in - let bll = - List.map (fun (bl,(scopt,scl)) -> - pi3 (extern_local_binder (scopt,scl@scopes') vars bl)) + let bl = + List.map (fun (bl,(scopt,scl)) -> + mkCPatOr (List.map (extern_cases_pattern_in_scope (scopt,scl@scopes') vars) bl)) binders in - insert_delimiters (make_notation loc ntn (l,ll,bll)) key) + let bll = + List.map (fun (bl,(scopt,scl)) -> + pi3 (extern_local_binder (scopt,scl@scopes') vars bl)) + binderlists in + insert_delimiters (make_notation loc ntn (l,ll,bl,bll)) key) | SynDefRule kn -> let l = List.map (fun (c,(scopt,scl)) -> extern true (scopt,scl@scopes) vars c, None) terms in - let a = CRef (Qualid (loc, shortest_qualid_of_syndef vars kn),None) in + let a = CRef (make ?loc @@ Qualid (shortest_qualid_of_syndef vars kn),None) in CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l) in if List.is_empty args then e else @@ -1110,7 +1154,7 @@ let extern_closed_glob ?lax goal_concl_style env sigma t = let any_any_branch = (* | _ => _ *) - Loc.tag ([],[DAst.make @@ PatVar Anonymous], DAst.make @@ GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)) + CAst.make ([],[DAst.make @@ PatVar Anonymous], DAst.make @@ GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)) let compute_displayed_name_in_pattern sigma avoid na c = let open Namegen in |