From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- interp/constrextern.ml | 383 +++++++++++++-------------- interp/constrextern.mli | 33 +-- interp/constrintern.ml | 563 ++++++++++++++++++++++------------------ interp/constrintern.mli | 107 ++++---- interp/coqlib.ml | 39 ++- interp/coqlib.mli | 74 +++--- interp/doc.tex | 2 +- interp/dumpglob.ml | 50 ++-- interp/dumpglob.mli | 9 +- interp/genarg.ml | 12 +- interp/genarg.mli | 105 ++++---- interp/implicit_quantifiers.ml | 60 ++--- interp/implicit_quantifiers.mli | 18 +- interp/interp.mllib | 2 +- interp/modintern.ml | 100 +++++-- interp/modintern.mli | 21 +- interp/notation.ml | 192 ++++++++------ interp/notation.mli | 95 ++++--- interp/ppextend.ml | 4 +- interp/ppextend.mli | 10 +- interp/reserve.ml | 95 ++++--- interp/reserve.mli | 13 +- interp/smartlocate.ml | 4 +- interp/smartlocate.mli | 16 +- interp/syntax_def.ml | 6 +- interp/syntax_def.mli | 10 +- interp/topconstr.ml | 393 ++++++++++++++-------------- interp/topconstr.mli | 108 ++++---- 28 files changed, 1298 insertions(+), 1226 deletions(-) (limited to 'interp') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index dc339622..193b38dd 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* false + +let encode_record r = + let indsp = global_inductive r in + if not (is_record indsp) then + user_err_loc (loc_of_reference r,"encode_record", + str "This type is not a structure type."); + indsp + +module PrintingRecordRecord = + PrintingInductiveMake (struct + let encode = encode_record + let field = "Record" + let title = "Types leading to pretty-printing using record notation: " + let member_message s b = + str "Terms of " ++ s ++ + str + (if b then " are printed using record notation" + else " are not printed using record notation") + end) + +module PrintingRecordConstructor = + PrintingInductiveMake (struct + let encode = encode_record + let field = "Constructor" + let title = "Types leading to pretty-printing using constructor form: " + let member_message s b = + str "Terms of " ++ s ++ + str + (if b then " are printed using constructor form" + else " are not printed using constructor form") + end) + +module PrintingRecord = Goptions.MakeRefTable(PrintingRecordRecord) +module PrintingConstructor = Goptions.MakeRefTable(PrintingRecordConstructor) + (**********************************************************************) (* Various externalisation functions *) @@ -117,6 +158,8 @@ let rec check_same_pattern p1 p2 = check_same_pattern a1 a2 | CPatCstr(_,c1,a1), CPatCstr(_,c2,a2) when c1=c2 -> List.iter2 check_same_pattern a1 a2 + | CPatCstrExpl(_,c1,a1), CPatCstrExpl(_,c2,a2) when c1=c2 -> + List.iter2 check_same_pattern a1 a2 | CPatAtom(_,r1), CPatAtom(_,r2) when r1=r2 -> () | CPatPrim(_,i1), CPatPrim(_,i2) when i1=i2 -> () | CPatDelimiters(_,s1,e1), CPatDelimiters(_,s2,e2) when s1=s2 -> @@ -204,82 +247,13 @@ and check_same_fix_binder bl1 bl2 = let same c d = try check_same_type c d; true with _ -> false -(* Idem for rawconstr *) - -let array_iter2 f v1 v2 = - List.iter2 f (Array.to_list v1) (Array.to_list v2) - -let rec same_patt p1 p2 = - match p1, p2 with - PatVar(_,na1), PatVar(_,na2) -> if na1<>na2 then failwith "PatVar" - | PatCstr(_,c1,pl1,al1), PatCstr(_,c2,pl2,al2) -> - if c1<>c2 || al1 <> al2 then failwith "PatCstr"; - List.iter2 same_patt pl1 pl2 - | _ -> failwith "same_patt" - -let rec same_raw c d = - match c,d with - | RRef(_,gr1), RRef(_,gr2) -> if gr1<>gr2 then failwith "RRef" - | RVar(_,id1), RVar(_,id2) -> if id1<>id2 then failwith "RVar" - | REvar(_,e1,a1), REvar(_,e2,a2) -> - if e1 <> e2 then failwith "REvar"; - Option.iter2(List.iter2 same_raw) a1 a2 - | RPatVar(_,pv1), RPatVar(_,pv2) -> if pv1<>pv2 then failwith "RPatVar" - | RApp(_,f1,a1), RApp(_,f2,a2) -> - List.iter2 same_raw (f1::a1) (f2::a2) - | RLambda(_,na1,bk1,t1,m1), RLambda(_,na2,bk2,t2,m2) -> - if na1 <> na2 then failwith "RLambda"; - same_raw t1 t2; same_raw m1 m2 - | RProd(_,na1,bk1,t1,m1), RProd(_,na2,bk2,t2,m2) -> - if na1 <> na2 then failwith "RProd"; - same_raw t1 t2; same_raw m1 m2 - | RLetIn(_,na1,t1,m1), RLetIn(_,na2,t2,m2) -> - if na1 <> na2 then failwith "RLetIn"; - same_raw t1 t2; same_raw m1 m2 - | RCases(_,_,_,c1,b1), RCases(_,_,_,c2,b2) -> - List.iter2 - (fun (t1,(al1,oind1)) (t2,(al2,oind2)) -> - same_raw t1 t2; - if al1 <> al2 then failwith "RCases"; - Option.iter2(fun (_,i1,_,nl1) (_,i2,_,nl2) -> - if i1<>i2 || nl1 <> nl2 then failwith "RCases") oind1 oind2) c1 c2; - List.iter2 (fun (_,_,pl1,b1) (_,_,pl2,b2) -> - List.iter2 same_patt pl1 pl2; - same_raw b1 b2) b1 b2 - | RLetTuple(_,nl1,_,b1,c1), RLetTuple(_,nl2,_,b2,c2) -> - if nl1<>nl2 then failwith "RLetTuple"; - same_raw b1 b2; - same_raw c1 c2 - | RIf(_,b1,_,t1,e1),RIf(_,b2,_,t2,e2) -> - same_raw b1 b2; same_raw t1 t2; same_raw e1 e2 - | RRec(_,fk1,na1,bl1,ty1,def1), RRec(_,fk2,na2,bl2,ty2,def2) -> - if fk1 <> fk2 || na1 <> na2 then failwith "RRec"; - array_iter2 - (List.iter2 (fun (na1,bk1,bd1,ty1) (na2,bk2,bd2,ty2) -> - if na1<>na2 then failwith "RRec"; - Option.iter2 same_raw bd1 bd2; - same_raw ty1 ty2)) bl1 bl2; - array_iter2 same_raw ty1 ty2; - array_iter2 same_raw def1 def2 - | RSort(_,s1), RSort(_,s2) -> if s1<>s2 then failwith "RSort" - | RHole _, _ -> () - | _, RHole _ -> () - | RCast(_,c1,_),r2 -> same_raw c1 r2 - | r1, RCast(_,c2,_) -> same_raw r1 c2 - | RDynamic(_,d1), RDynamic(_,d2) -> if d1<>d2 then failwith"RDynamic" - | _ -> failwith "same_raw" - -let same_rawconstr c d = - try same_raw c d; true - with Failure _ | Invalid_argument _ -> false - (**********************************************************************) (* mapping patterns to cases_pattern_expr *) let has_curly_brackets ntn = String.length ntn >= 6 & (String.sub ntn 0 6 = "{ _ } " or String.sub ntn (String.length ntn - 6) 6 = " { _ }" or - string_string_contains ntn " { _ } ") + string_string_contains ~where:ntn ~what:" { _ } ") let rec wildcards ntn n = if n = String.length ntn then [] @@ -347,7 +321,7 @@ let mkPat loc qid l = (* Normally irrelevant test with v8 syntax, but let's do it anyway *) if l = [] then CPatAtom (loc,Some qid) else CPatCstr (loc,qid,l) - (* Better to use extern_rawconstr composed with injection/retraction ?? *) + (* Better to use extern_glob_constr composed with injection/retraction ?? *) let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = try if !Flags.raw_print or !print_no_symbol then raise No_match; @@ -370,7 +344,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = let args = List.map (extern_cases_pattern_in_scope scopes vars) args in let p = try - if !Flags.raw_print then raise Exit; + if !Flags.raw_print then raise Exit; let projs = Recordops.lookup_projections (fst cstrsp) in let rec ip projs args acc = match projs with @@ -464,8 +438,11 @@ let is_projection nargs = function let is_hole = function CHole _ -> true | _ -> false -let is_significant_implicit a impl tail = - not (is_hole a) or (tail = [] & not (List.for_all is_status_implicit impl)) +let is_significant_implicit a = + not (is_hole a) + +let is_needed_for_correct_partial_application tail imp = + tail = [] & not (maximal_insertion_of imp) (* Implicit args indexes are in ascending order *) (* inctx is useful only if there is a last argument to be deduced from ctxt *) @@ -477,8 +454,9 @@ let explicitize loc inctx impl (cf,f) args = let visible = !Flags.raw_print or (!print_implicits & !print_implicits_explicit_args) or + (is_needed_for_correct_partial_application tail imp) or (!print_implicits_defensive & - is_significant_implicit a impl tail & + is_significant_implicit a & not (is_inferable_implicit inctx n imp)) in if visible then @@ -532,7 +510,7 @@ let rec extern_args extern scopes env args subscopes = extern argscopes env a :: extern_args extern scopes env args subscopes let rec remove_coercions inctx = function - | RApp (loc,RRef (_,r),args) as c + | GApp (loc,GRef (_,r),args) as c when not (!Flags.raw_print or !print_coercions) -> let nargs = List.length args in @@ -551,22 +529,17 @@ let rec remove_coercions inctx = function been confused with ordinary application or would have need a surrounding context and the coercion to funclass would have been made explicit to match *) - if l = [] then a' else RApp (loc,a',l) + if l = [] then a' else GApp (loc,a',l) | _ -> c with Not_found -> c) | c -> c let rec flatten_application = function - | RApp (loc,RApp(_,a,l'),l) -> flatten_application (RApp (loc,a,l'@l)) + | GApp (loc,GApp(_,a,l'),l) -> flatten_application (GApp (loc,a,l'@l)) | a -> a -let rec rename_rawconstr_var id0 id1 = function - RRef(loc,VarRef id) when id=id0 -> RRef(loc,VarRef id1) - | RVar(loc,id) when id=id0 -> RVar(loc,id1) - | c -> map_rawconstr (rename_rawconstr_var id0 id1) c - (**********************************************************************) -(* mapping rawterms to numerals (in presence of coercions, choose the *) +(* mapping glob_constr to numerals (in presence of coercions, choose the *) (* one with no delimiter if possible) *) let extern_possible_prim_token scopes r = @@ -574,7 +547,7 @@ let extern_possible_prim_token scopes r = let (sc,n) = uninterp_prim_token r in match availability_of_prim_token n sc scopes with | None -> None - | Some key -> Some (insert_delimiters (CPrim (loc_of_rawconstr r,n)) key) + | Some key -> Some (insert_delimiters (CPrim (loc_of_glob_constr r,n)) key) with No_match -> None @@ -586,12 +559,12 @@ let extern_optimal_prim_token scopes r r' = | _ -> raise No_match (**********************************************************************) -(* mapping rawterms to constr_expr *) +(* mapping glob_constr to constr_expr *) -let extern_rawsort = function - | RProp _ as s -> s - | RType (Some _) as s when !print_universes -> s - | RType _ -> RType None +let extern_glob_sort = function + | GProp _ as s -> s + | GType (Some _) as s when !print_universes -> s + | GType _ -> GType None let rec extern inctx scopes vars r = let r' = remove_coercions inctx r in @@ -604,31 +577,37 @@ let rec extern inctx scopes vars r = if !Flags.raw_print or !print_no_symbol then raise No_match; extern_symbol scopes vars r'' (uninterp_notations r'') with No_match -> match r' with - | RRef (loc,ref) -> + | GRef (loc,ref) -> extern_global loc (select_stronger_impargs (implicits_of_global ref)) (extern_reference loc vars ref) - | RVar (loc,id) -> CRef (Ident (loc,id)) + | GVar (loc,id) -> CRef (Ident (loc,id)) - | REvar (loc,n,None) when !print_meta_as_hole -> CHole (loc, None) + | GEvar (loc,n,None) when !print_meta_as_hole -> CHole (loc, None) - | REvar (loc,n,l) -> + | GEvar (loc,n,l) -> extern_evar loc n (Option.map (List.map (extern false scopes vars)) l) - | RPatVar (loc,n) -> + | GPatVar (loc,n) -> if !print_meta_as_hole then CHole (loc, None) else CPatVar (loc,n) - | RApp (loc,f,args) -> + | GApp (loc,f,args) -> (match f with - | RRef (rloc,ref) -> + | GRef (rloc,ref) -> let subscopes = find_arguments_scope ref in let args = extern_args (extern true) (snd scopes) vars args subscopes in begin try - if !Flags.raw_print then raise Exit; + if !Flags.raw_print then raise Exit; let cstrsp = match ref with ConstructRef c -> c | _ -> raise Not_found in let struc = Recordops.lookup_structure (fst cstrsp) in + if PrintingRecord.active (fst cstrsp) then + () + else if PrintingConstructor.active (fst cstrsp) then + raise Exit + else if not !Flags.record_print then + raise Exit; let projs = struc.Recordops.s_PROJ in let locals = struc.Recordops.s_PROJKIND in let rec cut args n = @@ -666,66 +645,66 @@ let rec extern inctx scopes vars r = explicitize loc inctx [] (None,sub_extern false scopes vars f) (List.map (sub_extern true scopes vars) args)) - | RProd (loc,Anonymous,_,t,c) -> + | GProd (loc,Anonymous,_,t,c) -> (* Anonymous product are never factorized *) CArrow (loc,extern_typ scopes vars t, extern_typ scopes vars c) - | RLetIn (loc,na,t,c) -> + | GLetIn (loc,na,t,c) -> CLetIn (loc,(loc,na),sub_extern false scopes vars t, extern inctx scopes (add_vname vars na) c) - | RProd (loc,na,bk,t,c) -> + | GProd (loc,na,bk,t,c) -> let t = extern_typ scopes vars (anonymize_if_reserved na t) in let (idl,c) = factorize_prod scopes (add_vname vars na) t c in CProdN (loc,[(dummy_loc,na)::idl,Default bk,t],c) - | RLambda (loc,na,bk,t,c) -> + | GLambda (loc,na,bk,t,c) -> let t = extern_typ scopes vars (anonymize_if_reserved na t) in let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) t c in CLambdaN (loc,[(dummy_loc,na)::idl,Default bk,t],c) - | RCases (loc,sty,rtntypopt,tml,eqns) -> + | GCases (loc,sty,rtntypopt,tml,eqns) -> let vars' = List.fold_right (name_fold Idset.add) (cases_predicate_names tml) vars in let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in let tml = List.map (fun (tm,(na,x)) -> let na' = match na,tm with - Anonymous, RVar (_,id) when - rtntypopt<>None & occur_rawconstr id (Option.get rtntypopt) + Anonymous, GVar (_,id) when + rtntypopt<>None & occur_glob_constr id (Option.get rtntypopt) -> Some (dummy_loc,Anonymous) | Anonymous, _ -> None - | Name id, RVar (_,id') when id=id' -> None + | Name id, GVar (_,id') when id=id' -> None | Name _, _ -> Some (dummy_loc,na) in (sub_extern false scopes vars tm, (na',Option.map (fun (loc,ind,n,nal) -> let params = list_tabulate - (fun _ -> RHole (dummy_loc,Evd.InternalHole)) n in + (fun _ -> GHole (dummy_loc,Evd.InternalHole)) n in let args = List.map (function - | Anonymous -> RHole (dummy_loc,Evd.InternalHole) - | Name id -> RVar (dummy_loc,id)) nal in - let t = RApp (dummy_loc,RRef (dummy_loc,IndRef ind),params@args) in + | Anonymous -> GHole (dummy_loc,Evd.InternalHole) + | Name id -> GVar (dummy_loc,id)) nal in + let t = GApp (dummy_loc,GRef (dummy_loc,IndRef ind),params@args) in (extern_typ scopes vars t)) x))) tml in let eqns = List.map (extern_eqn inctx scopes vars) eqns in CCases (loc,sty,rtntypopt',tml,eqns) - | RLetTuple (loc,nal,(na,typopt),tm,b) -> + | GLetTuple (loc,nal,(na,typopt),tm,b) -> CLetTuple (loc,List.map (fun na -> (dummy_loc,na)) nal, (Option.map (fun _ -> (dummy_loc,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) - | RIf (loc,c,(na,typopt),b1,b2) -> + | GIf (loc,c,(na,typopt),b1,b2) -> CIf (loc,sub_extern false scopes vars c, (Option.map (fun _ -> (dummy_loc,na)) typopt, Option.map (extern_typ scopes (add_vname vars na)) typopt), sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2) - | RRec (loc,fk,idv,blv,tyv,bv) -> + | GRec (loc,fk,idv,blv,tyv,bv) -> let vars' = Array.fold_right Idset.add idv vars in (match fk with - | RFix (nv,n) -> + | GFix (nv,n) -> let listdecl = Array.mapi (fun i fi -> let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in @@ -742,7 +721,7 @@ let rec extern inctx scopes vars r = extern false scopes vars1 def)) idv in CFix (loc,(loc,idv.(n)),Array.to_list listdecl) - | RCoFix n -> + | GCoFix n -> let listdecl = Array.mapi (fun i fi -> let (_,ids,bl) = extern_local_binder scopes vars blv.(i) in @@ -753,17 +732,15 @@ let rec extern inctx scopes vars r = in CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl)) - | RSort (loc,s) -> CSort (loc,extern_rawsort s) + | GSort (loc,s) -> CSort (loc,extern_glob_sort s) - | RHole (loc,e) -> CHole (loc, Some e) + | GHole (loc,e) -> CHole (loc, Some e) - | RCast (loc,c, CastConv (k,t)) -> + | GCast (loc,c, CastConv (k,t)) -> CCast (loc,sub_extern true scopes vars c, CastConv (k,extern_typ scopes vars t)) - | RCast (loc,c, CastCoerce) -> + | GCast (loc,c, CastCoerce) -> CCast (loc,sub_extern true scopes vars c, CastCoerce) - | RDynamic (loc,d) -> CDynamic (loc,d) - and extern_typ (_,scopes) = extern true (Some Notation.type_scope,scopes) @@ -774,7 +751,7 @@ and factorize_prod scopes vars aty c = if !Flags.raw_print or !print_no_symbol then raise No_match; ([],extern_symbol scopes vars c (uninterp_notations c)) with No_match -> match c with - | RProd (loc,(Name id as na),bk,ty,c) + | GProd (loc,(Name id as na),bk,ty,c) when same aty (extern_typ scopes vars (anonymize_if_reserved na ty)) & not (occur_var_constr_expr id aty) (* avoid na in ty escapes scope *) -> let (nal,c) = factorize_prod scopes (Idset.add id vars) aty c in @@ -786,7 +763,7 @@ and factorize_lambda inctx scopes vars aty c = if !Flags.raw_print or !print_no_symbol then raise No_match; ([],extern_symbol scopes vars c (uninterp_notations c)) with No_match -> match c with - | RLambda (loc,na,bk,ty,c) + | GLambda (loc,na,bk,ty,c) when same aty (extern_typ scopes vars (anonymize_if_reserved na ty)) & not (occur_name na aty) (* To avoid na in ty' escapes scope *) -> let (nal,c) = @@ -822,33 +799,40 @@ and extern_eqn inctx scopes vars (loc,ids,pl,c) = and extern_symbol (tmp_scope,scopes as allscopes) vars t = function | [] -> raise No_match | (keyrule,pat,n as _rule)::rules -> - let loc = Rawterm.loc_of_rawconstr t in + let loc = Glob_term.loc_of_glob_constr t in try (* Adjusts to the number of arguments expected by the notation *) let (t,args,argsscopes,argsimpls) = match t,n with - | RApp (_,(RRef (_,ref) as f),args), Some n + | GApp (_,f,args), Some n when List.length args >= n -> let args1, args2 = list_chop n args in - let subscopes = - try list_skipn n (find_arguments_scope ref) with _ -> [] in - let impls = - let impls = - select_impargs_size - (List.length args) (implicits_of_global ref) in - try list_skipn n impls with _ -> [] in - (if n = 0 then f else RApp (dummy_loc,f,args1)), + let subscopes, impls = + match f with + | GRef (_,ref) -> + let subscopes = + try list_skipn n (find_arguments_scope ref) with _ -> [] in + let impls = + let impls = + select_impargs_size + (List.length args) (implicits_of_global ref) in + try list_skipn n impls with _ -> [] in + subscopes,impls + | _ -> + [], [] in + (if n = 0 then f else GApp (dummy_loc,f,args1)), args2, subscopes, impls - | RApp (_,(RRef (_,ref) as f),args), None -> + | GApp (_,(GRef (_,ref) as f),args), None -> let subscopes = find_arguments_scope ref in let impls = select_impargs_size (List.length args) (implicits_of_global ref) in f, args, subscopes, impls - | RRef _, Some 0 -> RApp (dummy_loc,t,[]), [], [], [] + | GRef _, Some 0 -> GApp (dummy_loc,t,[]), [], [], [] | _, None -> t, [], [], [] | _ -> raise No_match in (* Try matching ... *) - let terms,termlists,binders = match_aconstr t pat in + let terms,termlists,binders = + match_aconstr !print_universes t pat in (* Try availability of interpretation ... *) let e = match keyrule with @@ -888,16 +872,16 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function No_match -> extern_symbol allscopes vars t rules and extern_recursion_order scopes vars = function - RStructRec -> CStructRec - | RWfRec c -> CWfRec (extern true scopes vars c) - | RMeasureRec (m,r) -> CMeasureRec (extern true scopes vars m, + GStructRec -> CStructRec + | GWfRec c -> CWfRec (extern true scopes vars c) + | GMeasureRec (m,r) -> CMeasureRec (extern true scopes vars m, Option.map (extern true scopes vars) r) -let extern_rawconstr vars c = +let extern_glob_constr vars c = extern false (None,[]) vars c -let extern_rawtype vars c = +let extern_glob_type vars c = extern_typ (None,[]) vars c (******************************************************************) @@ -920,89 +904,70 @@ let extern_constr at_top env t = let extern_type at_top env t = let avoid = if at_top then ids_of_context env else [] in let r = Detyping.detype at_top avoid (names_of_rel_context env) t in - extern_rawtype (vars_of_env env) r + extern_glob_type (vars_of_env env) r -let extern_sort s = extern_rawsort (detype_sort s) +let extern_sort s = extern_glob_sort (detype_sort s) (******************************************************************) (* Main translation function from pattern -> constr_expr *) -let rec raw_of_pat env = function - | PRef ref -> RRef (loc,ref) - | PVar id -> RVar (loc,id) - | PEvar (n,l) -> REvar (loc,n,Some (array_map_to_list (raw_of_pat env) l)) +let any_any_branch = + (* | _ => _ *) + (loc,[],[PatVar (loc,Anonymous)],GHole (loc,Evd.InternalHole)) + +let rec glob_of_pat env = function + | PRef ref -> GRef (loc,ref) + | PVar id -> GVar (loc,id) + | PEvar (n,l) -> GEvar (loc,n,Some (array_map_to_list (glob_of_pat env) l)) | PRel n -> let id = try match lookup_name_of_rel n env with | Name id -> id | Anonymous -> - anomaly "rawconstr_of_pattern: index to an anonymous variable" + anomaly "glob_constr_of_pattern: index to an anonymous variable" with Not_found -> id_of_string ("_UNBOUND_REL_"^(string_of_int n)) in - RVar (loc,id) - | PMeta None -> RHole (loc,Evd.InternalHole) - | PMeta (Some n) -> RPatVar (loc,(false,n)) + GVar (loc,id) + | PMeta None -> GHole (loc,Evd.InternalHole) + | PMeta (Some n) -> GPatVar (loc,(false,n)) | PApp (f,args) -> - RApp (loc,raw_of_pat env f,array_map_to_list (raw_of_pat env) args) + GApp (loc,glob_of_pat env f,array_map_to_list (glob_of_pat env) args) | PSoApp (n,args) -> - RApp (loc,RPatVar (loc,(true,n)), - List.map (raw_of_pat env) args) + GApp (loc,GPatVar (loc,(true,n)), + List.map (glob_of_pat env) args) | PProd (na,t,c) -> - RProd (loc,na,Explicit,raw_of_pat env t,raw_of_pat (na::env) c) + GProd (loc,na,Explicit,glob_of_pat env t,glob_of_pat (na::env) c) | PLetIn (na,t,c) -> - RLetIn (loc,na,raw_of_pat env t, raw_of_pat (na::env) c) + GLetIn (loc,na,glob_of_pat env t, glob_of_pat (na::env) c) | PLambda (na,t,c) -> - RLambda (loc,na,Explicit,raw_of_pat env t, raw_of_pat (na::env) c) + GLambda (loc,na,Explicit,glob_of_pat env t, glob_of_pat (na::env) c) | PIf (c,b1,b2) -> - RIf (loc, raw_of_pat env c, (Anonymous,None), - raw_of_pat env b1, raw_of_pat env b2) - | PCase ((LetStyle,[|n|],ind,None),PMeta None,tm,[|b|]) -> - let nal,b = it_destRLambda_or_LetIn_names n (raw_of_pat env b) in - RLetTuple (loc,nal,(Anonymous,None),raw_of_pat env tm,b) - | PCase (_,PMeta None,tm,[||]) -> - RCases (loc,RegularStyle,None,[raw_of_pat env tm,(Anonymous,None)],[]) - | PCase ((_,cstr_nargs,indo,ind_nargs),p,tm,bv) -> - let brs = Array.to_list (Array.map (raw_of_pat env) bv) in - let brns = Array.to_list cstr_nargs in - (* ind is None only if no branch and no return type *) - let ind = Option.get indo in - let mat = simple_cases_matrix_of_branches ind brns brs in - let indnames,rtn = - if p = PMeta None then (Anonymous,None),None - else - let nparams,n = Option.get ind_nargs in - return_type_of_predicate ind nparams n (raw_of_pat env p) in - RCases (loc,RegularStyle,rtn,[raw_of_pat env tm,indnames],mat) + GIf (loc, glob_of_pat env c, (Anonymous,None), + glob_of_pat env b1, glob_of_pat env b2) + | PCase ({cip_style=LetStyle; cip_ind_args=None},PMeta None,tm,[(0,n,b)]) -> + let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat env b) in + GLetTuple (loc,nal,(Anonymous,None),glob_of_pat env tm,b) + | PCase (info,p,tm,bl) -> + let mat = match bl, info.cip_ind with + | [], _ -> [] + | _, Some ind -> + let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat env c)) bl in + simple_cases_matrix_of_branches ind bl' + | _, None -> anomaly "PCase with some branches but unknown inductive" + in + let mat = if info.cip_extensible then mat @ [any_any_branch] else mat + in + let indnames,rtn = match p, info.cip_ind, info.cip_ind_args with + | PMeta None, _, _ -> (Anonymous,None),None + | _, Some ind, Some (nparams,nargs) -> + return_type_of_predicate ind nparams nargs (glob_of_pat env p) + | _ -> anomaly "PCase with non-trivial predicate but unknown inductive" + in + GCases (loc,RegularStyle,rtn,[glob_of_pat env tm,indnames],mat) | PFix f -> Detyping.detype false [] env (mkFix f) | PCoFix c -> Detyping.detype false [] env (mkCoFix c) - | PSort s -> RSort (loc,s) - -and raw_of_eqn env constr construct_nargs branch = - let make_pat x env b ids = - let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in - let id = next_name_away_with_default "x" x avoid in - PatVar (dummy_loc,Name id),(Name id)::env,id::ids - in - let rec buildrec ids patlist env n b = - if n=0 then - (dummy_loc, ids, - [PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)], - raw_of_pat env b) - else - match b with - | PLambda (x,_,b) -> - let pat,new_env,new_ids = make_pat x env b ids in - buildrec new_ids (pat::patlist) new_env (n-1) b - - | PLetIn (x,_,b) -> - let pat,new_env,new_ids = make_pat x env b ids in - buildrec new_ids (pat::patlist) new_env (n-1) b - - | _ -> - error "Unsupported branch in case-analysis while printing pattern." - in - buildrec [] [] env construct_nargs branch + | PSort s -> GSort (loc,s) let extern_constr_pattern env pat = - extern true (None,[]) Idset.empty (raw_of_pat env pat) + extern true (None,[]) Idset.empty (glob_of_pat env pat) let extern_rel_context where env sign = let a = detype_rel_context where [] (names_of_rel_context env) sign in diff --git a/interp/constrextern.mli b/interp/constrextern.mli index d0ccde2a..e1fdd068 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -1,14 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* v8 translation *) val check_same_type : constr_expr -> constr_expr -> unit -(* Translation of pattern, cases pattern, rawterm and term into syntax +(** Translation of pattern, cases pattern, glob_constr and term into syntax trees for printing *) val extern_cases_pattern : Idset.t -> cases_pattern -> cases_pattern_expr -val extern_rawconstr : Idset.t -> rawconstr -> constr_expr -val extern_rawtype : Idset.t -> rawconstr -> constr_expr +val extern_glob_constr : Idset.t -> glob_constr -> constr_expr +val extern_glob_type : Idset.t -> glob_constr -> constr_expr val extern_constr_pattern : names_context -> constr_pattern -> constr_expr -(* If [b=true] in [extern_constr b env c] then the variables in the first +(** If [b=true] in [extern_constr b env c] then the variables in the first level of quantification clashing with the variables in [env] are renamed *) val extern_constr : bool -> env -> constr -> constr_expr val extern_constr_in_scope : bool -> scope_name -> env -> constr -> constr_expr val extern_reference : loc -> Idset.t -> global_reference -> reference val extern_type : bool -> env -> types -> constr_expr -val extern_sort : sorts -> rawsort +val extern_sort : sorts -> glob_sort val extern_rel_context : constr option -> env -> rel_context -> local_binder list -(* Printing options *) +(** Printing options *) val print_implicits : bool ref val print_implicits_defensive : bool ref val print_arguments : bool ref @@ -55,25 +50,25 @@ val print_universes : bool ref val print_no_symbol : bool ref val print_projections : bool ref -(* Debug printing options *) +(** Debug printing options *) val set_debug_global_reference_printer : (loc -> global_reference -> reference) -> unit -(* This governs printing of implicit arguments. If [with_implicits] is +(** This governs printing of implicit arguments. If [with_implicits] is on and not [with_arguments] then implicit args are printed prefixed by "!"; if [with_implicits] and [with_arguments] are both on the function and not the arguments is prefixed by "!" *) val with_implicits : ('a -> 'b) -> 'a -> 'b val with_arguments : ('a -> 'b) -> 'a -> 'b -(* This forces printing of coercions *) +(** This forces printing of coercions *) val with_coercions : ('a -> 'b) -> 'a -> 'b -(* This forces printing universe names of Type{.} *) +(** This forces printing universe names of Type\{.\} *) val with_universes : ('a -> 'b) -> 'a -> 'b -(* This suppresses printing of numeral and symbols *) +(** This suppresses printing of numeral and symbols *) val without_symbols : ('a -> 'b) -> 'a -> 'b -(* This prints metas as anonymous holes *) +(** This prints metas as anonymous holes *) val with_meta_as_hole : ('a -> 'b) -> 'a -> 'b diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 4310a01e..b161d001 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* @@ -175,7 +174,7 @@ let compute_explicitable_implicit imps = function let sub_impl,_ = list_chop (List.length params) imps in let sub_impl' = List.filter is_status_implicit sub_impl in List.map name_of_implicit sub_impl' - | Recursive | Method -> + | Recursive | Method | Variable -> (* Unable to know in advance what the implicit arguments will be *) [] @@ -185,8 +184,9 @@ let compute_internalization_data env ty typ impl = (ty, expls_impl, impl, compute_arguments_scope typ) let compute_internalization_env env ty = - list_map3 - (fun id typ impl -> (id,compute_internalization_data env ty typ impl)) + list_fold_left3 + (fun map id typ impl -> Idmap.add id (compute_internalization_data env ty typ impl) map) + empty_internalization_env (**********************************************************************) (* Contracting "{ _ }" in notations *) @@ -234,6 +234,13 @@ let contract_pat_notation ntn (l,ll) = (* side effect; don't inline *) !ntn',(l,ll) +type intern_env = { + ids: Names.Idset.t; + unb: bool; + tmp_scope: Topconstr.tmp_scope_name option; + scopes: Topconstr.scope_name list; + impls: internalization_env } + (**********************************************************************) (* Remembering the parsing scope of variables in notations *) @@ -262,7 +269,7 @@ let error_expect_binder_notation_type loc id = pr_id id ++ str " is expected to occur in binding position in the right-hand side.") -let set_var_scope loc id istermvar (_,_,scopt,scopes) ntnvars = +let set_var_scope loc id istermvar env ntnvars = try let idscopes,typ = List.assoc id ntnvars in if !idscopes <> None & @@ -270,12 +277,12 @@ let set_var_scope loc id istermvar (_,_,scopt,scopes) ntnvars = we can tolerate having a variable occurring several times in different scopes: *) typ <> NtnInternTypeIdent & make_current_scope (Option.get !idscopes) - <> make_current_scope (scopt,scopes) then + <> make_current_scope (env.tmp_scope,env.scopes) then error_inconsistent_scope loc id (make_current_scope (Option.get !idscopes)) - (make_current_scope (scopt,scopes)) + (make_current_scope (env.tmp_scope,env.scopes)) else - idscopes := Some (scopt,scopes); + idscopes := Some (env.tmp_scope,env.scopes); match typ with | NtnInternTypeBinder -> if istermvar then error_expect_binder_notation_type loc id @@ -289,24 +296,43 @@ let set_var_scope loc id istermvar (_,_,scopt,scopes) ntnvars = (* Not in a notation *) () -let set_type_scope (ids,unb,tmp_scope,scopes) = - (ids,unb,Some Notation.type_scope,scopes) +let set_type_scope env = {env with tmp_scope = Some Notation.type_scope} -let reset_tmp_scope (ids,unb,tmp_scope,scopes) = - (ids,unb,None,scopes) +let reset_tmp_scope env = {env with tmp_scope = None} -let rec it_mkRProd env body = +let rec it_mkGProd env body = match env with - (na, bk, _, t) :: tl -> it_mkRProd tl (RProd (dummy_loc, na, bk, t, body)) + (na, bk, _, t) :: tl -> it_mkGProd tl (GProd (dummy_loc, na, bk, t, body)) | [] -> body -let rec it_mkRLambda env body = +let rec it_mkGLambda env body = match env with - (na, bk, _, t) :: tl -> it_mkRLambda tl (RLambda (dummy_loc, na, bk, t, body)) + (na, bk, _, t) :: tl -> it_mkGLambda tl (GLambda (dummy_loc, na, bk, t, body)) | [] -> body (**********************************************************************) (* Utilities for binders *) +let build_impls = function + |Implicit -> (function + |Name id -> Some (id, Impargs.Manual, (true,true)) + |Anonymous -> anomaly "Anonymous implicit argument") + |Explicit -> fun _ -> None + +let impls_type_list ?(args = []) = + let rec aux acc = function + |GProd (_,na,bk,_,c) -> aux ((build_impls bk na)::acc) c + |_ -> (Variable,[],List.append args (List.rev acc),[]) + in aux [] + +let impls_term_list ?(args = []) = + let rec aux acc = function + |GLambda (_,na,bk,_,c) -> aux ((build_impls bk na)::acc) c + |GRec (_, fix_kind, nas, args, tys, bds) -> + let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in + let acc' = List.fold_left (fun a (na, bk, _, _) -> (build_impls bk na)::a) acc args.(nb) in + aux acc' bds.(nb) + |_ -> (Variable,[],List.append args (List.rev acc),[]) + in aux [] let check_capture loc ty = function | Name id when occur_var_constr_expr id ty -> @@ -315,50 +341,55 @@ let check_capture loc ty = function () let locate_if_isevar loc na = function - | RHole _ -> + | GHole _ -> (try match na with - | Name id -> Reserve.find_reserved_type id + | Name id -> glob_constr_of_aconstr loc (Reserve.find_reserved_type id) | Anonymous -> raise Not_found - with Not_found -> RHole (loc, Evd.BinderType na)) + with Not_found -> GHole (loc, Evd.BinderType na)) | x -> x -let reset_hidden_inductive_implicit_test (ltacvars,namedctxvars,ntnvars,impls) = - let f = function id,(Inductive _,b,c,d) -> id,(Inductive [],b,c,d) | x -> x in - (ltacvars,namedctxvars,ntnvars,List.map f impls) +let reset_hidden_inductive_implicit_test env = + { env with impls = Idmap.fold (fun id x -> + let x = match x with + | (Inductive _,b,c,d) -> (Inductive [],b,c,d) + | x -> x + in Idmap.add id x) env.impls Idmap.empty } -let check_hidden_implicit_parameters id (_,_,_,impls) = - if List.exists (function - | (_,(Inductive indparams,_,_,_)) -> List.mem id indparams +let check_hidden_implicit_parameters id impls = + if Idmap.exists (fun _ -> function + | (Inductive indparams,_,_,_) -> List.mem id indparams | _ -> false) impls then errorlabstrm "" (strbrk "A parameter of an inductive type " ++ pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.") -let push_name_env ?(global_level=false) lvar (ids,unb,tmpsc,scopes as env) = +let push_name_env ?(global_level=false) lvar implargs env = function | loc,Anonymous -> if global_level then user_err_loc (loc,"", str "Anonymous variables not allowed"); env | loc,Name id -> - check_hidden_implicit_parameters id lvar; - set_var_scope loc id false env (let (_,_,ntnvars,_) = lvar in ntnvars); + check_hidden_implicit_parameters id env.impls ; + set_var_scope loc id false env (let (_,ntnvars) = lvar in ntnvars); if global_level then Dumpglob.dump_definition (loc,id) true "var" else Dumpglob.dump_binding loc id; - (Idset.add id ids,unb,tmpsc,scopes) + {env with ids = Idset.add id env.ids; impls = Idmap.add id implargs env.impls} let intern_generalized_binder ?(global_level=false) intern_type lvar - (ids,unb,tmpsc,sc as env) bl (loc, na) b b' t ty = - let ids = match na with Anonymous -> ids | Name na -> Idset.add na ids in + env bl (loc, na) b b' t ty = + let ids = (match na with Anonymous -> fun x -> x | Name na -> Idset.add na) env.ids in let ty, ids' = if t then ty, ids else Implicit_quantifiers.implicit_application ids Implicit_quantifiers.combine_params_freevar ty in - let ty' = intern_type (ids,true,tmpsc,sc) ty in - let fvs = Implicit_quantifiers.generalizable_vars_of_rawconstr ~bound:ids ~allowed:ids' ty' in - let env' = List.fold_left (fun env (x, l) -> push_name_env ~global_level lvar env (l, Name x)) env fvs in - let bl = List.map (fun (id, loc) -> (Name id, b, None, RHole (loc, Evd.BinderType (Name id)))) fvs in + let ty' = intern_type {env with ids = ids; unb = true} ty in + let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:ids ~allowed:ids' ty' in + let env' = List.fold_left + (fun env (x, l) -> push_name_env ~global_level lvar (Variable,[],[],[])(*?*) env (l, Name x)) + env fvs in + let bl = List.map (fun (id, loc) -> (Name id, b, None, GHole (loc, Evd.BinderType (Name id)))) fvs in let na = match na with | Anonymous -> if global_level then na @@ -371,7 +402,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar in Implicit_quantifiers.make_fresh ids' (Global.env ()) id in Name name | _ -> na - in (push_name_env ~global_level lvar env' (loc,na)), (na,b',None,ty') :: List.rev bl + in (push_name_env ~global_level lvar (impls_type_list ty')(*?*) env' (loc,na)), (na,b',None,ty') :: List.rev bl let intern_local_binder_aux ?(global_level=false) intern intern_type lvar (env,bl) = function | LocalRawAssum(nal,bk,ty) -> @@ -382,36 +413,37 @@ let intern_local_binder_aux ?(global_level=false) intern intern_type lvar (env,b let ty = locate_if_isevar loc na (intern_type env ty) in List.fold_left (fun (env,bl) na -> - (push_name_env lvar env na,(snd na,k,None,ty)::bl)) + (push_name_env lvar (impls_type_list ty) env na,(snd na,k,None,ty)::bl)) (env,bl) nal | Generalized (b,b',t) -> let env, b = intern_generalized_binder ~global_level intern_type lvar env bl (List.hd nal) b b' t ty in env, b @ bl) | LocalRawDef((loc,na as locna),def) -> - (push_name_env lvar env locna, - (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl) + let indef = intern env def in + (push_name_env lvar (impls_term_list indef) env locna, + (na,Explicit,Some(indef),GHole(loc,Evd.BinderType na))::bl) -let intern_generalization intern (ids,unb,tmp_scope,scopes as env) lvar loc bk ak c = - let c = intern (ids,true,tmp_scope,scopes) c in - let fvs = Implicit_quantifiers.generalizable_vars_of_rawconstr ~bound:ids c in +let intern_generalization intern env lvar loc bk ak c = + let c = intern {env with unb = true} c in + let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:env.ids c in let env', c' = let abs = let pi = match ak with | Some AbsPi -> true - | None when tmp_scope = Some Notation.type_scope - || List.mem Notation.type_scope scopes -> true + | None when env.tmp_scope = Some Notation.type_scope + || List.mem Notation.type_scope env.scopes -> true | _ -> false in if pi then (fun (id, loc') acc -> - RProd (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc)) + GProd (join_loc loc' loc, Name id, bk, GHole (loc', Evd.BinderType (Name id)), acc)) else (fun (id, loc') acc -> - RLambda (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc)) + GLambda (join_loc loc' loc, Name id, bk, GHole (loc', Evd.BinderType (Name id)), acc)) in List.fold_right (fun (id, loc as lid) (env, acc) -> - let env' = push_name_env lvar env (loc, Name id) in + let env' = push_name_env lvar (Variable,[],[],[]) env (loc, Name id) in (env', abs lid acc)) fvs (env,c) in c' @@ -425,14 +457,15 @@ let iterate_binder intern lvar (env,bl) = function let ty = intern_type env ty in let ty = locate_if_isevar loc na ty in List.fold_left - (fun (env,bl) na -> (push_name_env lvar env na,(snd na,k,None,ty)::bl)) + (fun (env,bl) na -> (push_name_env lvar (impls_type_list ty) env na,(snd na,k,None,ty)::bl)) (env,bl) nal | Generalized (b,b',t) -> let env, b = intern_generalized_binder intern_type lvar env bl (List.hd nal) b b' t ty in env, b @ bl) | LocalRawDef((loc,na as locna),def) -> - (push_name_env lvar env locna, - (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl) + let indef = intern env def in + (push_name_env lvar (impls_term_list indef) env locna, + (na,Explicit,Some(indef),GHole(loc,Evd.BinderType na))::bl) (**********************************************************************) (* Syntax extensions *) @@ -450,14 +483,14 @@ let find_fresh_name renaming (terms,termlists,binders) id = next_ident_away id fvs let traverse_binder (terms,_,_ as subst) - (renaming,(ids,unb,tmpsc,scopes as env))= + (renaming,env)= function | Anonymous -> (renaming,env),Anonymous | Name id -> try (* Binders bound in the notation are considered first-order objects *) let _,na = coerce_to_name (fst (List.assoc id terms)) in - (renaming,(name_fold Idset.add na ids,unb,tmpsc,scopes)), na + (renaming,{env with ids = name_fold Idset.add na env.ids}), na with Not_found -> (* Binders not bound in the notation do not capture variables *) (* outside the notation (i.e. in the substitution) *) @@ -465,7 +498,7 @@ let traverse_binder (terms,_,_ as subst) let renaming' = if id=id' then renaming else (id,id')::renaming in (renaming',env), Name id' -let make_letins loc = List.fold_right (fun (na,b,t) c -> RLetIn (loc,na,b,c)) +let make_letins loc = List.fold_right (fun (na,b,t) c -> GLetIn (loc,na,b,c)) let rec subordinate_letins letins = function (* binders come in reverse order; the non-let are returned in reverse order together *) @@ -479,13 +512,13 @@ let rec subordinate_letins letins = function letins,[] let rec subst_iterator y t = function - | RVar (_,id) as x -> if id = y then t else x - | x -> map_rawconstr (subst_iterator y t) x + | GVar (_,id) as x -> if id = y then t else x + | x -> map_glob_constr (subst_iterator y t) x -let subst_aconstr_in_rawconstr loc intern lvar subst infos c = +let subst_aconstr_in_glob_constr loc intern lvar subst infos c = let (terms,termlists,binders) = subst in - let rec aux (terms,binderopt as subst') (renaming,(ids,unb,_,scopes as env)) c = - let subinfos = renaming,(ids,unb,None,scopes) in + let rec aux (terms,binderopt as subst') (renaming,env) c = + let subinfos = renaming,{env with tmp_scope = None} in match c with | AVar id -> begin @@ -493,13 +526,14 @@ let subst_aconstr_in_rawconstr loc intern lvar subst infos c = (* of the notations *) try let (a,(scopt,subscopes)) = List.assoc id terms in - intern (ids,unb,scopt,subscopes@scopes) a + intern {env with tmp_scope = scopt; + scopes = subscopes @ env.scopes} a with Not_found -> try - RVar (loc,List.assoc id renaming) + GVar (loc,List.assoc id renaming) with Not_found -> (* Happens for local notation joint with inductive/fixpoint defs *) - RVar (loc,id) + GVar (loc,id) end | AList (x,_,iter,terminator,lassoc) -> (try @@ -516,7 +550,7 @@ let subst_aconstr_in_rawconstr loc intern lvar subst infos c = let na = try snd (coerce_to_name (fst (List.assoc id terms))) with Not_found -> na in - RHole (loc,Evd.BinderType na) + GHole (loc,Evd.BinderType na) | ABinderList (x,_,iter,terminator) -> (try (* All elements of the list are in scopes (scopt,subscopes) *) @@ -533,12 +567,12 @@ let subst_aconstr_in_rawconstr loc intern lvar subst infos c = anomaly "Inconsistent substitution of recursive notation") | AProd (Name id, AHole _, c') when option_mem_assoc id binderopt -> let (na,bk,t),letins = snd (Option.get binderopt) in - RProd (loc,na,bk,t,make_letins loc letins (aux subst' infos c')) + GProd (loc,na,bk,t,make_letins loc letins (aux subst' infos c')) | ALambda (Name id,AHole _,c') when option_mem_assoc id binderopt -> let (na,bk,t),letins = snd (Option.get binderopt) in - RLambda (loc,na,bk,t,make_letins loc letins (aux subst' infos c')) + GLambda (loc,na,bk,t,make_letins loc letins (aux subst' infos c')) | t -> - rawconstr_of_aconstr_with_binders loc (traverse_binder subst) + glob_constr_of_aconstr_with_binders loc (traverse_binder subst) (aux subst') subinfos t in aux (terms,None) infos c @@ -551,15 +585,15 @@ let split_by_type ids = let make_subst ids l = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids l -let intern_notation intern (_,_,tmp_scope,scopes as env) lvar loc ntn fullargs = +let intern_notation intern env lvar loc ntn fullargs = let ntn,(args,argslist,bll as fullargs) = contract_notation ntn fullargs in - let ((ids,c),df) = interp_notation loc ntn (tmp_scope,scopes) in + let ((ids,c),df) = interp_notation loc ntn (env.tmp_scope,env.scopes) in Dumpglob.dump_notation_location (ntn_loc loc fullargs ntn) ntn df; let ids,idsl,idsbl = split_by_type ids in let terms = make_subst ids args in let termlists = make_subst idsl argslist in let binders = make_subst idsbl bll in - subst_aconstr_in_rawconstr loc intern lvar + subst_aconstr_in_glob_constr loc intern lvar (terms,termlists,binders) ([],env) c (**********************************************************************) @@ -569,30 +603,32 @@ let string_of_ty = function | Inductive _ -> "ind" | Recursive -> "def" | Method -> "meth" + | Variable -> "var" -let intern_var (ids,_,_,_ as genv) (ltacvars,namedctxvars,ntnvars,impls) loc id = +let intern_var genv (ltacvars,ntnvars) namedctx loc id = let (ltacvars,unbndltacvars) = ltacvars in (* Is [id] an inductive type potentially with implicit *) try - let ty,expl_impls,impls,argsc = List.assoc id impls in + let ty,expl_impls,impls,argsc = Idmap.find id genv.impls in let expl_impls = List.map (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) expl_impls in let tys = string_of_ty ty in Dumpglob.dump_reference loc "<>" (string_of_id id) tys; - RVar (loc,id), make_implicits_list impls, argsc, expl_impls + GVar (loc,id), make_implicits_list impls, argsc, expl_impls with Not_found -> (* Is [id] bound in current term or is an ltac var bound to constr *) - if Idset.mem id ids or List.mem id ltacvars + if Idset.mem id genv.ids or List.mem id ltacvars then - RVar (loc,id), [], [], [] + GVar (loc,id), [], [], [] (* Is [id] a notation variable *) + else if List.mem_assoc id ntnvars then - (set_var_scope loc id true genv ntnvars; RVar (loc,id), [], [], []) + (set_var_scope loc id true genv ntnvars; GVar (loc,id), [], [], []) (* Is [id] the special variable for recursive notations *) else if ntnvars <> [] && id = ldots_var then - RVar (loc,id), [], [], [] + GVar (loc,id), [], [], [] else (* Is [id] bound to a free name in ltac (this is an ltac error message) *) try @@ -602,7 +638,7 @@ let intern_var (ids,_,_,_ as genv) (ltacvars,namedctxvars,ntnvars,impls) loc id | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0 with Not_found -> (* Is [id] a goal or section variable *) - let _ = Sign.lookup_named id namedctxvars in + let _ = Sign.lookup_named id namedctx in try (* [id] a section variable *) (* Redundant: could be done in intern_qualid *) @@ -610,14 +646,14 @@ let intern_var (ids,_,_,_ as genv) (ltacvars,namedctxvars,ntnvars,impls) loc id let impls = implicits_of_global ref in let scopes = find_arguments_scope ref in Dumpglob.dump_reference loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var"; - RRef (loc, ref), impls, scopes, [] + GRef (loc, ref), impls, scopes, [] with _ -> (* [id] a goal variable *) - RVar (loc,id), [], [], [] + GVar (loc,id), [], [], [] let find_appl_head_data = function - | RRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[] - | RApp (_,RRef (_,ref),l) as x + | GRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[] + | GApp (_,GRef (_,ref),l) as x when l <> [] & Flags.version_strictly_greater Flags.V8_2 -> let n = List.length l in x,List.map (drop_first_implicits n) (implicits_of_global ref), @@ -650,7 +686,7 @@ let intern_reference ref = let intern_qualid loc qid intern env lvar args = match intern_extended_global_of_qualid (loc,qid) with | TrueGlobal ref -> - RRef (loc, ref), args + GRef (loc, ref), args | SynDef sp -> let (ids,c) = Syntax_def.search_syntactic_definition sp in let nids = List.length ids in @@ -658,20 +694,20 @@ let intern_qualid loc qid intern env lvar args = let args1,args2 = list_chop nids args in check_no_explicitation args1; let subst = make_subst ids (List.map fst args1) in - subst_aconstr_in_rawconstr loc intern lvar (subst,[],[]) ([],env) c, args2 + subst_aconstr_in_glob_constr loc intern lvar (subst,[],[]) ([],env) c, args2 (* Rule out section vars since these should have been found by intern_var *) let intern_non_secvar_qualid loc qid intern env lvar args = match intern_qualid loc qid intern env lvar args with - | RRef (loc, VarRef id),_ -> error_global_not_found_loc loc qid + | GRef (loc, VarRef id),_ -> error_global_not_found_loc loc qid | r -> r -let intern_applied_reference intern (_, unb, _, _ as env) lvar args = function +let intern_applied_reference intern env namedctx lvar args = function | Qualid (loc, qid) -> let r,args2 = intern_qualid loc qid intern env lvar args in find_appl_head_data r, args2 | Ident (loc, id) -> - try intern_var env lvar loc id, args + try intern_var env lvar namedctx loc id, args with Not_found -> let qid = qualid_of_ident id in try @@ -679,19 +715,21 @@ let intern_applied_reference intern (_, unb, _, _ as env) lvar args = function find_appl_head_data r, args2 with e -> (* Extra allowance for non globalizing functions *) - if !interning_grammar || unb then - (RVar (loc,id), [], [], []),args + if !interning_grammar || env.unb then + (GVar (loc,id), [], [], []),args else raise e let interp_reference vars r = let (r,_,_,_),_ = intern_applied_reference (fun _ -> error_not_enough_arguments dummy_loc) - (Idset.empty,false,None,[]) (vars,[],[],[]) [] r + {ids = Idset.empty; unb = false ; + tmp_scope = None; scopes = []; impls = empty_internalization_env} [] + (vars,[]) [] r in r -let apply_scope_env (ids,unb,_,scopes) = function - | [] -> (ids,unb,None,scopes), [] - | sc::scl -> (ids,unb,sc,scopes), scl +let apply_scope_env env = function + | [] -> {env with tmp_scope = None}, [] + | sc::scl -> {env with tmp_scope = sc}, scl let rec simple_adjust_scopes n = function | [] -> if n=0 then [] else None :: simple_adjust_scopes (n-1) [] @@ -766,8 +804,8 @@ let alias_of = function | (id::_,_) -> Name id let message_redundant_alias (id1,id2) = - if_verbose warning - ("Alias variable "^(string_of_id id1)^" is merged with "^(string_of_id id2)) + if_warn msg_warning + (str "Alias variable " ++ pr_id id1 ++ str " is merged with " ++ pr_id id2) (* Expanding notations *) @@ -794,7 +832,7 @@ let rec subst_pat_iterator y t (subst,p) = match p with let pl = simple_product_of_cases_patterns l' in List.map (fun (subst',pl) -> subst'@subst,PatCstr (loc,id,pl,alias)) pl -let subst_cases_pattern loc alias intern fullsubst scopes a = +let subst_cases_pattern loc alias intern fullsubst env a = let rec aux alias (subst,substlist as fullsubst) = function | AVar id -> begin @@ -802,7 +840,8 @@ let subst_cases_pattern loc alias intern fullsubst scopes a = (* of the notations *) try let (a,(scopt,subscopes)) = List.assoc id subst in - intern (subscopes@scopes) ([],[]) scopt a + intern {env with scopes=subscopes@env.scopes; + tmp_scope = scopt} ([],[]) a with Not_found -> if id = ldots_var then [], [[], PatVar (loc,Name id)] else anomaly ("Unbound pattern notation variable: "^(string_of_id id)) @@ -847,7 +886,7 @@ type pattern_qualid_kind = ((identifier * identifier) list * cases_pattern) list) list | VarPat of identifier -let find_constructor ref f aliases pats scopes = +let find_constructor ref f aliases pats env = let (loc,qid) = qualid_of_reference ref in let gref = try locate_extended qid @@ -865,7 +904,7 @@ let find_constructor ref f aliases pats scopes = if List.length pats < nvars then error_not_enough_arguments loc; let pats1,pats2 = list_chop nvars pats in let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) vars pats1 in - let idspl1 = List.map (subst_cases_pattern loc Anonymous f (subst,[]) scopes) args in + let idspl1 = List.map (subst_cases_pattern loc Anonymous f (subst,[]) env) args in cstr, idspl1, pats2 | _ -> raise Not_found) @@ -884,9 +923,9 @@ let find_pattern_variable = function | Ident (loc,id) -> id | Qualid (loc,_) as x -> raise (InternalizationError(loc,NotAConstructor x)) -let maybe_constructor ref f aliases scopes = +let maybe_constructor ref f aliases env = try - let c,idspl1,pl2 = find_constructor ref f aliases [] scopes in + let c,idspl1,pl2 = find_constructor ref f aliases [] env in assert (pl2 = []); ConstrPat (c,idspl1) with @@ -894,12 +933,12 @@ let maybe_constructor ref f aliases scopes = | InternalizationError _ -> VarPat (find_pattern_variable ref) (* patt var also exists globally but does not satisfy preconditions *) | (Environ.NotEvaluableConst _ | Not_found) -> - if_verbose msg_warning (str "pattern " ++ pr_reference ref ++ + if_warn msg_warning (str "pattern " ++ pr_reference ref ++ str " is understood as a pattern variable"); VarPat (find_pattern_variable ref) -let mustbe_constructor loc ref f aliases patl scopes = - try find_constructor ref f aliases patl scopes +let mustbe_constructor loc ref f aliases patl env = + try find_constructor ref f aliases patl env with (Environ.NotEvaluableConst _ | Not_found) -> raise (InternalizationError (loc,NotAConstructor ref)) @@ -918,7 +957,7 @@ let sort_fields mode loc l completer = try Recordops.find_projection (global_reference_of_reference refer) with Not_found -> - user_err_loc (loc, "intern", str"Not a projection") + user_err_loc (loc_of_reference refer, "intern", pr_reference refer ++ str": Not a projection") in (* elimination of the first field from the projections *) let rec build_patt l m i acc = @@ -958,6 +997,10 @@ let sort_fields mode loc l completer = | [] -> accpatt | p::q-> let refer, patt = p in + let glob_refer = try global_reference_of_reference refer + with |Not_found -> + user_err_loc (loc_of_reference refer, "intern", + str "The field \"" ++ pr_reference refer ++ str "\" does not exist.") in let rec add_patt l acc = match l with | [] -> @@ -965,7 +1008,7 @@ let sort_fields mode loc l completer = (loc, "", str "This record contains fields of different records.") | (i, a) :: b-> - if global_reference_of_reference refer = a + if glob_refer = a then (i,List.rev_append acc l) else add_patt b ((i,a)::acc) in @@ -988,12 +1031,12 @@ let sort_fields mode loc l completer = Some (nparams, base_constructor, List.rev (clean_list sorted_indexed_pattern 0 [])) -let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat= +let rec intern_cases_pattern genv env (ids,asubst as aliases) pat = let intern_pat = intern_cases_pattern genv in match pat with | CPatAlias (loc, p, id) -> let aliases' = merge_aliases aliases id in - intern_pat scopes aliases' tmp_scope p + intern_pat env aliases' p | CPatRecord (loc, l) -> let sorted_fields = sort_fields false loc l (fun _ l -> (CPatAtom (loc, None))::l) in let self_patt = @@ -1001,41 +1044,42 @@ let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat= | None -> CPatAtom (loc, None) | Some (_, head, pl) -> CPatCstr(loc, head, pl) in - intern_pat scopes aliases tmp_scope self_patt - | CPatCstr (loc, head, pl) -> - let c,idslpl1,pl2 = mustbe_constructor loc head intern_pat aliases pl scopes in + intern_pat env aliases self_patt + | CPatCstr (loc, head, pl) | CPatCstrExpl (loc, head, pl) -> + let c,idslpl1,pl2 = mustbe_constructor loc head intern_pat aliases pl env in check_constructor_length genv loc c idslpl1 pl2; let argscs2 = find_remaining_constructor_scopes idslpl1 pl2 c in - let idslpl2 = List.map2 (intern_pat scopes ([],[])) argscs2 pl2 in + let idslpl2 = List.map2 (fun x -> intern_pat {env with tmp_scope = x} ([],[])) argscs2 pl2 in let (ids',pll) = product_of_cases_patterns ids (idslpl1@idslpl2) in let pl' = List.map (fun (asubst,pl) -> (asubst, PatCstr (loc,c,pl,alias_of aliases))) pll in ids',pl' | CPatNotation (loc,"- _",([CPatPrim(_,Numeral p)],[])) when Bigint.is_strictly_pos p -> - intern_pat scopes aliases tmp_scope (CPatPrim(loc,Numeral(Bigint.neg p))) + intern_pat env aliases (CPatPrim(loc,Numeral(Bigint.neg p))) | CPatNotation (_,"( _ )",([a],[])) -> - intern_pat scopes aliases tmp_scope a + intern_pat env aliases a | CPatNotation (loc, ntn, fullargs) -> let ntn,(args,argsl as fullargs) = contract_pat_notation ntn fullargs in - let ((ids',c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in + let ((ids',c),df) = Notation.interp_notation loc ntn (env.tmp_scope,env.scopes) in let (ids',idsl',_) = split_by_type ids' in Dumpglob.dump_notation_location (patntn_loc loc fullargs ntn) ntn df; let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in let substlist = List.map2 (fun (id,scl) a -> (id,(a,scl))) idsl' argsl in let ids'',pl = subst_cases_pattern loc (alias_of aliases) intern_pat (subst,substlist) - scopes c + env c in ids@ids'', pl | CPatPrim (loc, p) -> let a = alias_of aliases in let (c,_) = Notation.interp_prim_token_cases_pattern loc p a - (tmp_scope,scopes) in + (env.tmp_scope,env.scopes) in (ids,[asubst,c]) | CPatDelimiters (loc, key, e) -> - intern_pat (find_delimiters_scope loc key::scopes) aliases None e + intern_pat {env with scopes=find_delimiters_scope loc key::env.scopes; + tmp_scope = None} aliases e | CPatAtom (loc, Some head) -> - (match maybe_constructor head intern_pat aliases scopes with + (match maybe_constructor head intern_pat aliases env with | ConstrPat (c,idspl) -> check_constructor_length genv loc c idspl []; let (ids',pll) = product_of_cases_patterns ids idspl in @@ -1048,7 +1092,7 @@ let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat= (ids,[asubst, PatVar (loc,alias_of aliases)]) | CPatOr (loc, pl) -> assert (pl <> []); - let pl' = List.map (intern_pat scopes aliases tmp_scope) pl in + let pl' = List.map (intern_pat env aliases) pl in let (idsl,pl') = List.split pl' in let ids = List.hd idsl in check_or_pat_variables loc ids (List.tl idsl); @@ -1067,7 +1111,7 @@ let merge_impargs l args = let check_projection isproj nargs r = match (r,isproj) with - | RRef (loc, ref), Some _ -> + | GRef (loc, ref), Some _ -> (try let n = Recordops.find_projection_nparams ref + 1 in if nargs <> n then @@ -1075,15 +1119,15 @@ let check_projection isproj nargs r = with Not_found -> user_err_loc (loc,"",pr_global_env Idset.empty ref ++ str " is not a registered projection.")) - | _, Some _ -> user_err_loc (loc_of_rawconstr r, "", str "Not a projection.") + | _, Some _ -> user_err_loc (loc_of_glob_constr r, "", str "Not a projection.") | _, None -> () let get_implicit_name n imps = Some (Impargs.name_of_implicit (List.nth imps (n-1))) let set_hole_implicit i b = function - | RRef (loc,r) | RApp (_,RRef (loc,r),_) -> (loc,Evd.ImplicitArg (r,i,b)) - | RVar (loc,id) -> (loc,Evd.ImplicitArg (VarRef id,i,b)) + | GRef (loc,r) | GApp (_,GRef (loc,r),_) -> (loc,Evd.ImplicitArg (r,i,b)) + | GVar (loc,id) -> (loc,Evd.ImplicitArg (VarRef id,i,b)) | _ -> anomaly "Only refs have implicits" let exists_implicit_name id = @@ -1127,13 +1171,13 @@ let extract_explicit_arg imps args = (* Main loop *) let internalize sigma globalenv env allow_patvar lvar c = - let rec intern (ids,unb,tmp_scope,scopes as env) = function + let rec intern env = function | CRef ref as x -> let (c,imp,subscopes,l),_ = - intern_applied_reference intern env lvar [] ref in + intern_applied_reference intern env (Environ.named_context globalenv) lvar [] ref in (match intern_impargs c env imp subscopes l with - | [] -> c - | l -> RApp (constr_loc x, c, l)) + | [] -> c + | l -> GApp (constr_loc x, c, l)) | CFix (loc, (locid,iddef), dl) -> let lf = List.map (fun ((_, id),_,_,_,_) -> id) dl in let dl = Array.of_list dl in @@ -1142,30 +1186,34 @@ let internalize sigma globalenv env allow_patvar lvar c = with Not_found -> raise (InternalizationError (locid,UnboundFixName (false,iddef))) in - let idl = Array.map - (fun (id,(n,order),bl,ty,bd) -> + let idl_temp = Array.map + (fun (id,(n,order),bl,ty,_) -> let intern_ro_arg f = let before, after = split_at_annot bl n in - let ((ids',_,_,_) as env',rbefore) = + let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in - let ro = f (intern (ids', unb, tmp_scope, scopes)) in + let ro = f (intern env') in let n' = Option.map (fun _ -> List.length rbefore) n in n', ro, List.fold_left intern_local_binder (env',rbefore) after in - let n, ro, ((ids',_,_,_),rbl) = + let n, ro, (env',rbl) = match order with | CStructRec -> - intern_ro_arg (fun _ -> RStructRec) + intern_ro_arg (fun _ -> GStructRec) | CWfRec c -> - intern_ro_arg (fun f -> RWfRec (f c)) + intern_ro_arg (fun f -> GWfRec (f c)) | CMeasureRec (m,r) -> - intern_ro_arg (fun f -> RMeasureRec (f m, Option.map f r)) + intern_ro_arg (fun f -> GMeasureRec (f m, Option.map f r)) in - let ids'' = List.fold_right Idset.add lf ids' in - ((n, ro), List.rev rbl, - intern_type (ids',unb,tmp_scope,scopes) ty, - intern (ids'',unb,None,scopes) bd)) dl in - RRec (loc,RFix + ((n, ro), List.rev rbl, intern_type env' ty, env')) dl in + let idl = array_map2 (fun (_,_,_,_,bd) (a,b,c,env') -> + let env'' = list_fold_left_i (fun i en name -> + let (_,bli,tyi,_) = idl_temp.(i) in + let fix_args = (List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli) in + push_name_env lvar (impls_type_list ~args:fix_args tyi) + en (dummy_loc, Name name)) 0 env' lf in + (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in + GRec (loc,GFix (Array.map (fun (ro,_,_,_) -> ro) idl,n), Array.of_list lf, Array.map (fun (_,bl,_,_) -> bl) idl, @@ -1179,21 +1227,26 @@ let internalize sigma globalenv env allow_patvar lvar c = with Not_found -> raise (InternalizationError (locid,UnboundFixName (true,iddef))) in - let idl = Array.map - (fun (id,bl,ty,bd) -> - let ((ids',_,_,_),rbl) = + let idl_tmp = Array.map + (fun (id,bl,ty,_) -> + let (env',rbl) = List.fold_left intern_local_binder (env,[]) bl in - let ids'' = List.fold_right Idset.add lf ids' in (List.rev rbl, - intern_type (ids',unb,tmp_scope,scopes) ty, - intern (ids'',unb,None,scopes) bd)) dl in - RRec (loc,RCoFix n, + intern_type env' ty,env')) dl in + let idl = array_map2 (fun (_,_,_,bd) (b,c,env') -> + let env'' = list_fold_left_i (fun i en name -> + let (bli,tyi,_) = idl_tmp.(i) in + let cofix_args = List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli in + push_name_env lvar (impls_type_list ~args:cofix_args tyi) + en (dummy_loc, Name name)) 0 env' lf in + (b,c,intern {env'' with tmp_scope = None} bd)) dl idl_tmp in + GRec (loc,GCoFix n, Array.of_list lf, Array.map (fun (bl,_,_) -> bl) idl, Array.map (fun (_,ty,_) -> ty) idl, Array.map (fun (_,_,bd) -> bd) idl) | CArrow (loc,c1,c2) -> - RProd (loc, Anonymous, Explicit, intern_type env c1, intern_type env c2) + GProd (loc, Anonymous, Explicit, intern_type env c1, intern_type env c2) | CProdN (loc,[],c2) -> intern_type env c2 | CProdN (loc,(nal,bk,ty)::bll,c2) -> @@ -1203,8 +1256,9 @@ let internalize sigma globalenv env allow_patvar lvar c = | CLambdaN (loc,(nal,bk,ty)::bll,c2) -> iterate_lam loc (reset_tmp_scope env) bk ty (CLambdaN (loc, bll, c2)) nal | CLetIn (loc,na,c1,c2) -> - RLetIn (loc, snd na, intern (reset_tmp_scope env) c1, - intern (push_name_env lvar env na) c2) + let inc1 = intern (reset_tmp_scope env) c1 in + GLetIn (loc, snd na, inc1, + intern (push_name_env lvar (impls_term_list inc1) env na) c2) | CNotation (loc,"- _",([CPrim (_,Numeral p)],[],[])) when Bigint.is_strictly_pos p -> intern env (CPrim (loc,Numeral (Bigint.neg p))) @@ -1214,16 +1268,17 @@ let internalize sigma globalenv env allow_patvar lvar c = | CGeneralization (loc,b,a,c) -> intern_generalization intern env lvar loc b a c | CPrim (loc, p) -> - fst (Notation.interp_prim_token loc p (tmp_scope,scopes)) + fst (Notation.interp_prim_token loc p (env.tmp_scope,env.scopes)) | CDelimiters (loc, key, e) -> - intern (ids,unb,None,find_delimiters_scope loc key::scopes) e + intern {env with tmp_scope = None; + scopes = find_delimiters_scope loc key :: env.scopes} e | CAppExpl (loc, (isproj,ref), args) -> let (f,_,args_scopes,_),args = let args = List.map (fun a -> (a,None)) args in - intern_applied_reference intern env lvar args ref in + intern_applied_reference intern env (Environ.named_context globalenv) lvar args ref in check_projection isproj (List.length args) f; - (* Rem: RApp(_,f,[]) stands for @f *) - RApp (loc, f, intern_args env args_scopes (List.map fst args)) + (* Rem: GApp(_,f,[]) stands for @f *) + GApp (loc, f, intern_args env args_scopes (List.map fst args)) | CApp (loc, (isproj,f), args) -> let isproj,f,args = match f with (* Compact notations like "t.(f args') args" *) @@ -1232,7 +1287,7 @@ let internalize sigma globalenv env allow_patvar lvar c = | _ -> isproj,f,args in let (c,impargs,args_scopes,l),args = match f with - | CRef ref -> intern_applied_reference intern env lvar args ref + | CRef ref -> intern_applied_reference intern env (Environ.named_context globalenv) lvar args ref | CNotation (loc,ntn,([],[],[])) -> let c = intern_notation intern env lvar loc ntn ([],[],[]) in find_appl_head_data c, args @@ -1242,8 +1297,8 @@ let internalize sigma globalenv env allow_patvar lvar c = check_projection isproj (List.length args) c; (match c with (* Now compact "(f args') args" *) - | RApp (loc', f', args') -> RApp (join_loc loc' loc, f',args'@args) - | _ -> RApp (loc, c, args)) + | GApp (loc', f', args') -> GApp (join_loc loc' loc, f',args'@args) + | _ -> GApp (loc, c, args)) | CRecord (loc, _, fs) -> let cargs = sort_fields true loc fs @@ -1261,48 +1316,40 @@ let internalize sigma globalenv env allow_patvar lvar c = let tms,env' = List.fold_right (fun citm (inds,env) -> let (tm,ind),nal = intern_case_item env citm in - (tm,ind)::inds,List.fold_left - (push_name_env (reset_hidden_inductive_implicit_test lvar)) - env nal) + (tm,ind)::inds,List.fold_left (push_name_env lvar (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) tms ([],env) in let rtnpo = Option.map (intern_type env') rtnpo in let eqns' = List.map (intern_eqn (List.length tms) env) eqns in - RCases (loc, sty, rtnpo, tms, List.flatten eqns') + GCases (loc, sty, rtnpo, tms, List.flatten eqns') | CLetTuple (loc, nal, (na,po), b, c) -> let env' = reset_tmp_scope env in let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in let p' = Option.map (fun p -> - let env'' = List.fold_left - (push_name_env (reset_hidden_inductive_implicit_test lvar)) - env ids in + let env'' = List.fold_left (push_name_env lvar (Variable,[],[],[])) env ids in intern_type env'' p) po in - RLetTuple (loc, List.map snd nal, (na', p'), b', - intern (List.fold_left (push_name_env lvar) env nal) c) + GLetTuple (loc, List.map snd nal, (na', p'), b', + intern (List.fold_left (push_name_env lvar (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c) | CIf (loc, c, (na,po), b1, b2) -> let env' = reset_tmp_scope env in let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in let p' = Option.map (fun p -> - let env'' = List.fold_left - (push_name_env (reset_hidden_inductive_implicit_test lvar)) - env ids in + let env'' = List.fold_left (push_name_env lvar (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) ids in intern_type env'' p) po in - RIf (loc, c', (na', p'), intern env b1, intern env b2) + GIf (loc, c', (na', p'), intern env b1, intern env b2) | CHole (loc, k) -> - RHole (loc, match k with Some k -> k | None -> Evd.QuestionMark (Evd.Define true)) + GHole (loc, match k with Some k -> k | None -> Evd.QuestionMark (Evd.Define true)) | CPatVar (loc, n) when allow_patvar -> - RPatVar (loc, n) + GPatVar (loc, n) | CPatVar (loc, _) -> raise (InternalizationError (loc,IllegalMetavariable)) | CEvar (loc, n, l) -> - REvar (loc, n, Option.map (List.map (intern env)) l) + GEvar (loc, n, Option.map (List.map (intern env)) l) | CSort (loc, s) -> - RSort(loc,s) + GSort(loc,s) | CCast (loc, c1, CastConv (k, c2)) -> - RCast (loc,intern env c1, CastConv (k, intern_type env c2)) + GCast (loc,intern env c1, CastConv (k, intern_type env c2)) | CCast (loc, c1, CastCoerce) -> - RCast (loc,intern env c1, CastCoerce) - - | CDynamic (loc,d) -> RDynamic (loc,d) + GCast (loc,intern env c1, CastCoerce) and intern_type env = intern (set_type_scope env) @@ -1310,52 +1357,52 @@ let internalize sigma globalenv env allow_patvar lvar c = intern_local_binder_aux intern intern_type lvar env bind (* Expands a multiple pattern into a disjunction of multiple patterns *) - and intern_multiple_pattern scopes n (loc,pl) = + and intern_multiple_pattern env n (loc,pl) = let idsl_pll = - List.map (intern_cases_pattern globalenv scopes ([],[]) None) pl in + List.map (intern_cases_pattern globalenv {env with tmp_scope = None} ([],[])) pl in check_number_of_pattern loc n pl; product_of_cases_patterns [] idsl_pll (* Expands a disjunction of multiple pattern *) - and intern_disjunctive_multiple_pattern scopes loc n mpl = + and intern_disjunctive_multiple_pattern env loc n mpl = assert (mpl <> []); - let mpl' = List.map (intern_multiple_pattern scopes n) mpl in + let mpl' = List.map (intern_multiple_pattern env n) mpl in let (idsl,mpl') = List.split mpl' in let ids = List.hd idsl in check_or_pat_variables loc ids (List.tl idsl); (ids,List.flatten mpl') (* Expands a pattern-matching clause [lhs => rhs] *) - and intern_eqn n (ids,unb,tmp_scope,scopes) (loc,lhs,rhs) = - let eqn_ids,pll = intern_disjunctive_multiple_pattern scopes loc n lhs in + and intern_eqn n env (loc,lhs,rhs) = + let eqn_ids,pll = intern_disjunctive_multiple_pattern env loc n lhs in (* Linearity implies the order in ids is irrelevant *) check_linearity lhs eqn_ids; - let env_ids = List.fold_right Idset.add eqn_ids ids in + let env_ids = List.fold_right Idset.add eqn_ids env.ids in List.map (fun (asubst,pl) -> let rhs = replace_vars_constr_expr asubst rhs in List.iter message_redundant_alias asubst; - let rhs' = intern (env_ids,unb,tmp_scope,scopes) rhs in + let rhs' = intern {env with ids = env_ids} rhs in (loc,eqn_ids,pl,rhs')) pll - and intern_case_item (vars,unb,_,scopes as env) (tm,(na,t)) = + and intern_case_item env (tm,(na,t)) = let tm' = intern env tm in let ids,typ = match t with | Some t -> let tids = ids_of_cases_indtype t in let tids = List.fold_right Idset.add tids Idset.empty in - let t = intern_type (tids,unb,None,scopes) t in + let t = intern_type {env with ids = tids; tmp_scope = None} t in let loc,ind,l = match t with - | RRef (loc,IndRef ind) -> (loc,ind,[]) - | RApp (loc,RRef (_,IndRef ind),l) -> (loc,ind,l) - | _ -> error_bad_inductive_type (loc_of_rawconstr t) in + | GRef (loc,IndRef ind) -> (loc,ind,[]) + | GApp (loc,GRef (_,IndRef ind),l) -> (loc,ind,l) + | _ -> error_bad_inductive_type (loc_of_glob_constr t) in let nparams, nrealargs = inductive_nargs globalenv ind in let nindargs = nparams + nrealargs in if List.length l <> nindargs then error_wrong_numarg_inductive_loc loc globalenv ind nindargs; let nal = List.map (function - | RHole (loc,_) -> loc,Anonymous - | RVar (loc,id) -> loc,Name id - | c -> user_err_loc (loc_of_rawconstr c,"",str "Not a name.")) l in + | GHole (loc,_) -> loc,Anonymous + | GVar (loc,id) -> loc,Name id + | c -> user_err_loc (loc_of_glob_constr c,"",str "Not a name.")) l in let parnal,realnal = list_chop nparams nal in if List.exists (fun (_,na) -> na <> Anonymous) parnal then error_inductive_parameter_not_implicit loc; @@ -1363,8 +1410,8 @@ let internalize sigma globalenv env allow_patvar lvar c = | None -> [], None in let na = match tm', na with - | RVar (loc,id), None when Idset.mem id vars -> loc,Name id - | RRef (loc, VarRef id), None -> loc,Name id + | GVar (loc,id), None when Idset.mem id env.ids -> loc,Name id + | GRef (loc, VarRef id), None -> loc,Name id | _, None -> dummy_loc,Anonymous | _, Some (loc,na) -> loc,na in (tm',(snd na,typ)), na::ids @@ -1373,9 +1420,9 @@ let internalize sigma globalenv env allow_patvar lvar c = let rec default env bk = function | (loc1,na as locna)::nal -> if nal <> [] then check_capture loc1 ty na; - let body = default (push_name_env lvar env locna) bk nal in let ty = locate_if_isevar loc1 na (intern_type env ty) in - RProd (join_loc loc1 loc2, na, bk, ty, body) + let body = default (push_name_env lvar (impls_type_list ty) env locna) bk nal in + GProd (join_loc loc1 loc2, na, bk, ty, body) | [] -> intern_type env body in match bk with @@ -1383,22 +1430,22 @@ let internalize sigma globalenv env allow_patvar lvar c = | Generalized (b,b',t) -> let env, ibind = intern_generalized_binder intern_type lvar env [] (List.hd nal) b b' t ty in let body = intern_type env body in - it_mkRProd ibind body + it_mkGProd ibind body and iterate_lam loc2 env bk ty body nal = let rec default env bk = function | (loc1,na as locna)::nal -> if nal <> [] then check_capture loc1 ty na; - let body = default (push_name_env lvar env locna) bk nal in let ty = locate_if_isevar loc1 na (intern_type env ty) in - RLambda (join_loc loc1 loc2, na, bk, ty, body) + let body = default (push_name_env lvar (impls_type_list ty) env locna) bk nal in + GLambda (join_loc loc1 loc2, na, bk, ty, body) | [] -> intern env body in match bk with | Default b -> default env b nal | Generalized (b, b', t) -> let env, ibind = intern_generalized_binder intern_type lvar env [] (List.hd nal) b b' t ty in let body = intern env body in - it_mkRLambda ibind body + it_mkGLambda ibind body and intern_impargs c env l subscopes args = let l = select_impargs_size (List.length args) l in @@ -1418,7 +1465,7 @@ let internalize sigma globalenv env allow_patvar lvar c = (* with implicit arguments if maximal insertion is set *) [] else - RHole (set_hole_implicit (n,get_implicit_name n l) (force_inference_of imp) c) :: + GHole (set_hole_implicit (n,get_implicit_name n l) (force_inference_of imp) c) :: aux (n+1) impl' subscopes' eargs rargs end | (imp::impl', a::rargs') -> @@ -1426,7 +1473,7 @@ let internalize sigma globalenv env allow_patvar lvar c = | (imp::impl', []) -> if eargs <> [] then (let (id,(loc,_)) = List.hd eargs in - user_err_loc (loc,"",str "Not enough non implicit + user_err_loc (loc,"",str "Not enough non implicit \ arguments to accept the argument bound to " ++ pr_id id ++ str".")); [] @@ -1450,7 +1497,7 @@ let internalize sigma globalenv env allow_patvar lvar c = explain_internalization_error e) (**************************************************************************) -(* Functions to translate constr_expr into rawconstr *) +(* Functions to translate constr_expr into glob_constr *) (**************************************************************************) let extract_ids env = @@ -1459,32 +1506,34 @@ let extract_ids env = Idset.empty let intern_gen isarity sigma env - ?(impls=[]) ?(allow_patvar=false) ?(ltacvars=([],[])) + ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=([],[])) c = let tmp_scope = if isarity then Some Notation.type_scope else None in - internalize sigma env (extract_ids env, false, tmp_scope,[]) - allow_patvar (ltacvars,Environ.named_context env, [], impls) c + internalize sigma env {ids = extract_ids env; unb = false; + tmp_scope = tmp_scope; scopes = []; + impls = impls} + allow_patvar (ltacvars, []) c let intern_constr sigma env c = intern_gen false sigma env c let intern_type sigma env c = intern_gen true sigma env c -let intern_pattern env patt = +let intern_pattern globalenv patt = try - intern_cases_pattern env [] ([],[]) None patt + intern_cases_pattern globalenv {ids = extract_ids globalenv; unb = false; + tmp_scope = None; scopes = []; + impls = empty_internalization_env} ([],[]) patt with InternalizationError (loc,e) -> user_err_loc (loc,"internalize",explain_internalization_error e) -type manual_implicits = (explicitation * (bool * bool * bool)) list - (*********************************************************************) (* Functions to parse and interpret constructions *) let interp_gen kind sigma env - ?(impls=[]) ?(allow_patvar=false) ?(ltacvars=([],[])) + ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=([],[])) c = let c = intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars sigma env c in Default.understand_gen kind sigma env c @@ -1492,10 +1541,10 @@ let interp_gen kind sigma env let interp_constr sigma env c = interp_gen (OfType None) sigma env c -let interp_type sigma env ?(impls=[]) c = +let interp_type sigma env ?(impls=empty_internalization_env) c = interp_gen IsType sigma env ~impls c -let interp_casted_constr sigma env ?(impls=[]) c typ = +let interp_casted_constr sigma env ?(impls=empty_internalization_env) c typ = interp_gen (OfType (Some typ)) sigma env ~impls c let interp_open_constr sigma env c = @@ -1503,19 +1552,19 @@ let interp_open_constr sigma env c = let interp_open_constr_patvar sigma env c = let raw = intern_gen false sigma env c ~allow_patvar:true in - let sigma = ref (Evd.create_evar_defs sigma) in - let evars = ref (Gmap.empty : (identifier,rawconstr) Gmap.t) in + let sigma = ref sigma in + let evars = ref (Gmap.empty : (identifier,glob_constr) Gmap.t) in let rec patvar_to_evar r = match r with - | RPatVar (loc,(_,id)) -> + | GPatVar (loc,(_,id)) -> ( try Gmap.find id !evars with Not_found -> let ev = Evarutil.e_new_evar sigma env (Termops.new_Type()) in let ev = Evarutil.e_new_evar sigma env ev in - let rev = REvar (loc,(fst (Term.destEvar ev)),None) (*TODO*) in + let rev = GEvar (loc,(fst (Term.destEvar ev)),None) (*TODO*) in evars := Gmap.add id rev !evars; rev ) - | _ -> map_rawconstr patvar_to_evar r in + | _ -> map_glob_constr patvar_to_evar r in let raw = patvar_to_evar raw in Default.understand_tcc !sigma env raw @@ -1523,7 +1572,7 @@ let interp_constr_judgment sigma env c = Default.understand_judgment sigma env (intern_constr sigma env c) let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true) - env ?(impls=[]) kind c = + env ?(impls=empty_internalization_env) kind c = let evdref = match evdref with | None -> ref Evd.empty @@ -1531,43 +1580,44 @@ let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true) in let istype = kind = IsType in let c = intern_gen istype ~impls !evdref env c in - let imps = Implicit_quantifiers.implicits_of_rawterm ~with_products:istype c in + let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:istype c in Default.understand_tcc_evars ~fail_evar evdref env kind c, imps let interp_casted_constr_evars_impls ?evdref ?(fail_evar=true) - env ?(impls=[]) c typ = + env ?(impls=empty_internalization_env) c typ = interp_constr_evars_gen_impls ?evdref ~fail_evar env ~impls (OfType (Some typ)) c -let interp_type_evars_impls ?evdref ?(fail_evar=true) env ?(impls=[]) c = +let interp_type_evars_impls ?evdref ?(fail_evar=true) env ?(impls=empty_internalization_env) c = interp_constr_evars_gen_impls ?evdref ~fail_evar env IsType ~impls c -let interp_constr_evars_impls ?evdref ?(fail_evar=true) env ?(impls=[]) c = +let interp_constr_evars_impls ?evdref ?(fail_evar=true) env ?(impls=empty_internalization_env) c = interp_constr_evars_gen_impls ?evdref ~fail_evar env (OfType None) ~impls c -let interp_constr_evars_gen evdref env ?(impls=[]) kind c = - let c = intern_gen (kind=IsType) ~impls ( !evdref) env c in +let interp_constr_evars_gen evdref env ?(impls=empty_internalization_env) kind c = + let c = intern_gen (kind=IsType) ~impls !evdref env c in Default.understand_tcc_evars evdref env kind c -let interp_casted_constr_evars evdref env ?(impls=[]) c typ = +let interp_casted_constr_evars evdref env ?(impls=empty_internalization_env) c typ = interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c -let interp_type_evars evdref env ?(impls=[]) c = +let interp_type_evars evdref env ?(impls=empty_internalization_env) c = interp_constr_evars_gen evdref env IsType ~impls c type ltac_sign = identifier list * unbound_ltac_var_map let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=([],[])) c = let c = intern_gen as_type ~allow_patvar:true ~ltacvars sigma env c in - pattern_of_rawconstr c + pattern_of_glob_constr c -let interp_aconstr ?(impls=[]) vars recvars a = +let interp_aconstr ?(impls=empty_internalization_env) vars recvars a = let env = Global.env () in (* [vl] is intended to remember the scope of the free variables of [a] *) let vl = List.map (fun (id,typ) -> (id,(ref None,typ))) vars in - let c = internalize Evd.empty (Global.env()) (extract_ids env, false, None, []) - false (([],[]),Environ.named_context env,vl,impls) a in + let c = internalize Evd.empty (Global.env()) {ids = extract_ids env; unb = false; + tmp_scope = None; scopes = []; impls = impls} + false (([],[]),vl) a in (* Translate and check that [c] has all its free variables bound in [vars] *) - let a = aconstr_of_rawconstr vars recvars c in + let a = aconstr_of_glob_constr vars recvars c in (* Splits variables into those that are binding, bound, or both *) (* binding and bound *) let out_scope = function None -> None,[] | Some (a,l) -> a,l in @@ -1579,12 +1629,12 @@ let interp_aconstr ?(impls=[]) vars recvars a = let interp_binder sigma env na t = let t = intern_gen true sigma env t in - let t' = locate_if_isevar (loc_of_rawconstr t) na t in + let t' = locate_if_isevar (loc_of_glob_constr t) na t in Default.understand_type sigma env t' let interp_binder_evars evdref env na t = let t = intern_gen true !evdref env t in - let t' = locate_if_isevar (loc_of_rawconstr t) na t in + let t' = locate_if_isevar (loc_of_glob_constr t) na t in Default.understand_tcc_evars evdref env IsType t' open Environ @@ -1595,11 +1645,12 @@ let my_intern_constr sigma env lvar acc c = let my_intern_type sigma env lvar acc c = my_intern_constr sigma env lvar (set_type_scope acc) c -let intern_context global_level sigma env params = - let lvar = (([],[]),Environ.named_context env, [], []) in - snd (List.fold_left +let intern_context global_level sigma env impl_env params = + let lvar = (([],[]), []) in + let lenv, bl = List.fold_left (intern_local_binder_aux ~global_level (my_intern_constr sigma env lvar) (my_intern_type sigma env lvar) lvar) - ((extract_ids env,false,None,[]), []) params) + ({ids = extract_ids env; unb = false; + tmp_scope = None; scopes = []; impls = impl_env}, []) params in (lenv.impls, bl) let interp_rawcontext_gen understand_type understand_judgment env bl = let (env, par, _, impls) = @@ -1607,7 +1658,7 @@ let interp_rawcontext_gen understand_type understand_judgment env bl = (fun (env,params,n,impls) (na, k, b, t) -> match b with None -> - let t' = locate_if_isevar (loc_of_rawconstr t) na t in + let t' = locate_if_isevar (loc_of_glob_constr t) na t in let t = understand_type env t' in let d = (na,None,t) in let impls = @@ -1624,15 +1675,15 @@ let interp_rawcontext_gen understand_type understand_judgment env bl = (env,[],1,[]) (List.rev bl) in (env, par), impls -let interp_context_gen understand_type understand_judgment ?(global_level=false) sigma env params = - let bl = intern_context global_level sigma env params in - interp_rawcontext_gen understand_type understand_judgment env bl +let interp_context_gen understand_type understand_judgment ?(global_level=false) ?(impl_env=empty_internalization_env) sigma env params = + let int_env,bl = intern_context global_level sigma env impl_env params in + int_env, interp_rawcontext_gen understand_type understand_judgment env bl -let interp_context ?(global_level=false) sigma env params = - interp_context_gen (Default.understand_type sigma) - (Default.understand_judgment sigma) ~global_level sigma env params +let interp_context ?(global_level=false) ?(impl_env=empty_internalization_env) sigma env params = + interp_context_gen (Default.understand_type sigma) + (Default.understand_judgment sigma) ~global_level ~impl_env sigma env params -let interp_context_evars ?(global_level=false) evdref env params = +let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) evdref env params = interp_context_gen (fun env t -> Default.understand_tcc_evars evdref env IsType t) - (Default.understand_judgment_tcc evdref) ~global_level !evdref env params - + (Default.understand_judgment_tcc evdref) ~global_level ~impl_env !evdref env params + diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 767ec9ff..be78837f 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -1,39 +1,34 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* var_internalization_type -> @@ -70,43 +64,41 @@ val compute_internalization_env : env -> var_internalization_type -> identifier list -> types list -> Impargs.manual_explicitation list list -> internalization_env -type manual_implicits = (explicitation * (bool * bool * bool)) list - type ltac_sign = identifier list * unbound_ltac_var_map -type raw_binder = (name * binding_kind * rawconstr option * rawconstr) +type glob_binder = (name * binding_kind * glob_constr option * glob_constr) -(*s Internalisation performs interpretation of global names and notations *) +(** {6 Internalization performs interpretation of global names and notations } *) -val intern_constr : evar_map -> env -> constr_expr -> rawconstr +val intern_constr : evar_map -> env -> constr_expr -> glob_constr -val intern_type : evar_map -> env -> constr_expr -> rawconstr +val intern_type : evar_map -> env -> constr_expr -> glob_constr val intern_gen : bool -> evar_map -> env -> ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> - constr_expr -> rawconstr + constr_expr -> glob_constr val intern_pattern : env -> cases_pattern_expr -> Names.identifier list * - ((Names.identifier * Names.identifier) list * Rawterm.cases_pattern) list + ((Names.identifier * Names.identifier) list * Glob_term.cases_pattern) list -val intern_context : bool -> evar_map -> env -> local_binder list -> raw_binder list +val intern_context : bool -> evar_map -> env -> internalization_env -> local_binder list -> internalization_env * glob_binder list -(*s Composing internalization with pretyping *) +(** {6 Composing internalization with pretyping } *) -(* Main interpretation function *) +(** Main interpretation function *) val interp_gen : typing_constraint -> evar_map -> env -> ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> constr_expr -> constr -(* Particular instances *) +(** Particular instances *) val interp_constr : evar_map -> env -> constr_expr -> constr val interp_type : evar_map -> env -> ?impls:internalization_env -> - constr_expr -> types + constr_expr -> types val interp_open_constr : evar_map -> env -> constr_expr -> evar_map * constr @@ -115,18 +107,18 @@ val interp_open_constr_patvar : evar_map -> env -> constr_expr -> evar_map * c val interp_casted_constr : evar_map -> env -> ?impls:internalization_env -> constr_expr -> types -> constr -(* Accepting evars and giving back the manual implicits in addition. *) +(** Accepting evars and giving back the manual implicits in addition. *) val interp_casted_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env -> - ?impls:internalization_env -> constr_expr -> types -> constr * manual_implicits + ?impls:internalization_env -> constr_expr -> types -> constr * Impargs.manual_implicits val interp_type_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env -> ?impls:internalization_env -> - constr_expr -> types * manual_implicits + constr_expr -> types * Impargs.manual_implicits val interp_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env -> ?impls:internalization_env -> - constr_expr -> constr * manual_implicits + constr_expr -> constr * Impargs.manual_implicits val interp_casted_constr_evars : evar_map ref -> env -> ?impls:internalization_env -> constr_expr -> types -> constr @@ -134,58 +126,57 @@ val interp_casted_constr_evars : evar_map ref -> env -> val interp_type_evars : evar_map ref -> env -> ?impls:internalization_env -> constr_expr -> types -(*s Build a judgment *) +(** {6 Build a judgment } *) val interp_constr_judgment : evar_map -> env -> constr_expr -> unsafe_judgment -(* Interprets constr patterns *) +(** Interprets constr patterns *) val intern_constr_pattern : evar_map -> env -> ?as_type:bool -> ?ltacvars:ltac_sign -> constr_pattern_expr -> patvar list * constr_pattern -(* Raise Not_found if syndef not bound to a name and error if unexisting ref *) +(** Raise Not_found if syndef not bound to a name and error if unexisting ref *) val intern_reference : reference -> global_reference -(* Expands abbreviations (syndef); raise an error if not existing *) -val interp_reference : ltac_sign -> reference -> rawconstr +(** Expands abbreviations (syndef); raise an error if not existing *) +val interp_reference : ltac_sign -> reference -> glob_constr -(* Interpret binders *) +(** Interpret binders *) val interp_binder : evar_map -> env -> name -> constr_expr -> types val interp_binder_evars : evar_map ref -> env -> name -> constr_expr -> types -(* Interpret contexts: returns extended env and context *) +(** Interpret contexts: returns extended env and context *) -val interp_context_gen : (env -> rawconstr -> types) -> - (env -> rawconstr -> unsafe_judgment) -> - ?global_level:bool -> - evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits +val interp_context_gen : (env -> glob_constr -> types) -> + (env -> glob_constr -> unsafe_judgment) -> + ?global_level:bool -> ?impl_env:internalization_env -> + evar_map -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits) -val interp_context : ?global_level:bool -> - evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits +val interp_context : ?global_level:bool -> ?impl_env:internalization_env -> + evar_map -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits) -val interp_context_evars : ?global_level:bool -> - evar_map ref -> env -> local_binder list -> (env * rel_context) * manual_implicits +val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env -> + evar_map ref -> env -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits) -(* Locating references of constructions, possibly via a syntactic definition *) -(* (these functions do not modify the glob file) *) +(** Locating references of constructions, possibly via a syntactic definition + (these functions do not modify the glob file) *) val is_global : identifier -> bool val construct_reference : named_context -> identifier -> constr val global_reference : identifier -> constr val global_reference_in_absolute_module : dir_path -> identifier -> constr -(* Interprets a term as the left-hand side of a notation; the boolean - list is a set and this set is [true] for a variable occurring in - term position, [false] for a variable occurring in binding - position; [true;false] if in both kinds of position *) - +(** Interprets a term as the left-hand side of a notation; the boolean + list is a set and this set is [true] for a variable occurring in + term position, [false] for a variable occurring in binding + position; [true;false] if in both kinds of position *) val interp_aconstr : ?impls:internalization_env -> (identifier * notation_var_internalization_type) list -> (identifier * identifier) list -> constr_expr -> (identifier * (subscopes * notation_var_internalization_type)) list * aconstr -(* Globalization leak for Grammar *) +(** Globalization leak for Grammar *) val for_grammar : ('a -> 'b) -> 'a -> 'b diff --git a/interp/coqlib.ml b/interp/coqlib.ml index c5850abf..eb7828ea 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* string list -> string -> global_reference -(* [coq_reference caller_message [dir;subdir;...] s] returns a +(** [coq_reference caller_message [dir;subdir;...] s] returns a global reference to the name Coq.dir.subdir.(...).s *) val coq_reference : message -> string list -> string -> global_reference -(* idem but return a term *) +(** idem but return a term *) val coq_constant : message -> string list -> string -> constr -(* Synonyms of [coq_constant] and [coq_reference] *) +(** Synonyms of [coq_constant] and [coq_reference] *) val gen_constant : message -> string list -> string -> constr val gen_reference : message -> string list -> string -> global_reference -(* Search in several modules (not prefixed by "Coq") *) +(** Search in several modules (not prefixed by "Coq") *) val gen_constant_in_modules : string->string list list-> string -> constr val arith_modules : string list list val zarith_base_modules : string list list val init_modules : string list list -(* For tactics/commands requiring vernacular libraries *) +(** For tactics/commands requiring vernacular libraries *) val check_required_library : string list -> unit -(*s Global references *) +(** {6 Global references } *) -(* Modules *) +(** Modules *) val logic_module : dir_path val logic_type_module : dir_path val datatypes_module_name : string list val logic_module_name : string list -(* Natural numbers *) +(** Natural numbers *) val nat_path : full_path val glob_nat : global_reference val path_of_O : constructor @@ -70,7 +67,7 @@ val path_of_S : constructor val glob_O : global_reference val glob_S : global_reference -(* Booleans *) +(** Booleans *) val glob_bool : global_reference val path_of_true : constructor val path_of_false : constructor @@ -78,12 +75,13 @@ val glob_true : global_reference val glob_false : global_reference -(* Equality *) +(** Equality *) val glob_eq : global_reference val glob_identity : global_reference val glob_jmeq : global_reference -(*s Constructions and patterns related to Coq initial state are unknown +(** {6 ... } *) +(** Constructions and patterns related to Coq initial state are unknown at compile time. Therefore, we can only provide methods to build them at runtime. This is the purpose of the [constr delayed] and [constr_pattern delayed] types. Objects of this time needs to be @@ -96,7 +94,7 @@ type coq_bool_data = { andb_true_intro : constr} val build_bool_type : coq_bool_data delayed -(*s For Equality tactics *) +(** {6 For Equality tactics } *) type coq_sigma_data = { proj1 : constr; proj2 : constr; @@ -106,7 +104,9 @@ type coq_sigma_data = { val build_sigma_set : coq_sigma_data delayed val build_sigma_type : coq_sigma_data delayed -(* Non-dependent pairs in Set from Datatypes *) +val build_sigma : coq_sigma_data delayed + +(** Non-dependent pairs in Set from Datatypes *) val build_prod : coq_sigma_data delayed type coq_eq_data = { @@ -121,17 +121,19 @@ val build_coq_eq_data : coq_eq_data delayed val build_coq_identity_data : coq_eq_data delayed val build_coq_jmeq_data : coq_eq_data delayed -val build_coq_eq : constr delayed (* = [(build_coq_eq_data()).eq] *) -val build_coq_eq_refl : constr delayed (* = [(build_coq_eq_data()).refl] *) -val build_coq_eq_sym : constr delayed (* = [(build_coq_eq_data()).sym] *) +val build_coq_eq : constr delayed (** = [(build_coq_eq_data()).eq] *) +val build_coq_eq_refl : constr delayed (** = [(build_coq_eq_data()).refl] *) +val build_coq_eq_sym : constr delayed (** = [(build_coq_eq_data()).sym] *) val build_coq_f_equal2 : constr delayed -(* Data needed for discriminate and injection *) +(** Data needed for discriminate and injection *) type coq_inversion_data = { - inv_eq : constr; (* : forall params, t -> Prop *) - inv_ind : constr; (* : forall params P y, eq params y -> P y *) - inv_congr: constr (* : forall params B (f:t->B) y, eq params y -> f c=f y *) + inv_eq : constr; (** : forall params, args -> Prop *) + inv_ind : constr; (** : forall params P (H : P params) args, eq params args + -> P args *) + inv_congr: constr (** : forall params B (f:t->B) args, eq params args -> + f params = f args *) } val build_coq_inversion_eq_data : coq_inversion_data delayed @@ -139,21 +141,22 @@ val build_coq_inversion_identity_data : coq_inversion_data delayed val build_coq_inversion_jmeq_data : coq_inversion_data delayed val build_coq_inversion_eq_true_data : coq_inversion_data delayed -(* Specif *) +(** Specif *) val build_coq_sumbool : constr delayed -(*s Connectives *) -(* The False proposition *) +(** {6 ... } *) +(** Connectives + The False proposition *) val build_coq_False : constr delayed -(* The True proposition and its unique proof *) +(** The True proposition and its unique proof *) val build_coq_True : constr delayed val build_coq_I : constr delayed -(* Negation *) +(** Negation *) val build_coq_not : constr delayed -(* Conjunction *) +(** Conjunction *) val build_coq_and : constr delayed val build_coq_conj : constr delayed val build_coq_iff : constr delayed @@ -161,10 +164,10 @@ val build_coq_iff : constr delayed val build_coq_iff_left_proj : constr delayed val build_coq_iff_right_proj : constr delayed -(* Disjunction *) +(** Disjunction *) val build_coq_or : constr delayed -(* Existential quantifier *) +(** Existential quantifier *) val build_coq_ex : constr delayed val coq_eq_ref : global_reference lazy_t @@ -173,6 +176,7 @@ val coq_jmeq_ref : global_reference lazy_t val coq_eq_true_ref : global_reference lazy_t val coq_existS_ref : global_reference lazy_t val coq_existT_ref : global_reference lazy_t +val coq_exist_ref : global_reference lazy_t val coq_not_ref : global_reference lazy_t val coq_False_ref : global_reference lazy_t val coq_sumbool_ref : global_reference lazy_t diff --git a/interp/doc.tex b/interp/doc.tex index 5bd92fbd..4ce5811d 100644 --- a/interp/doc.tex +++ b/interp/doc.tex @@ -5,7 +5,7 @@ \ocwsection \label{interp} This chapter describes the translation from \Coq\ context-dependent front abstract syntax of terms (\verb=front=) to and from the -context-free, untyped, raw form of constructions (\verb=rawconstr=). +context-free, untyped, globalized form of constructions (\verb=glob_constr=). The modules translating back and forth the front abstract syntax are organized as follows. diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index c26133c6..07e813e7 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* + open_glob_file (Filename.chop_extension vfile ^ ".glob"); + output_string !glob_file "DIGEST "; + output_string !glob_file (Digest.to_hex (Digest.file vfile)); + output_char !glob_file '\n' + | File f -> + open_glob_file f; + output_string !glob_file "DIGEST NO\n" + | NoGlob | StdOut -> + () + +let end_dump_glob () = + match !glob_output with + | MultFiles | File _ -> close_glob_file () + | NoGlob | StdOut -> () let previous_state = ref MultFiles let pause () = previous_state := !glob_output; glob_output := NoGlob @@ -163,11 +176,6 @@ let dump_constraint ((loc, n), _, _) sec ty = | Names.Name id -> dump_definition (loc, id) sec ty | Names.Anonymous -> () -let dump_name (loc, n) sec ty = - match n with - | Names.Name id -> dump_definition (loc, id) sec ty - | Names.Anonymous -> () - let dump_modref loc mp ty = if dump () then let (dp, l) = Lib.split_modpath mp in @@ -192,12 +200,13 @@ let dump_libref loc dp ty = let cook_notation df sc = (* We encode notations so that they are space-free and still human-readable *) - (* - all spaces are replaced by _ *) - (* - all _ denoting a non-terminal symbol are replaced by x *) - (* - all terminal tokens are surrounded by single quotes, including '_' *) - (* which already denotes terminal _ *) - (* - all single quotes in terminal tokens are doubled *) - (* The output is decoded in function Index.prepare_entry of coqdoc *) + (* - all spaces are replaced by _ *) + (* - all _ denoting a non-terminal symbol are replaced by x *) + (* - all terminal tokens are surrounded by single quotes, including '_' *) + (* which already denotes terminal _ *) + (* - all single quotes in terminal tokens are doubled *) + (* - characters < 32 are represented by '^A, '^B, '^C, etc *) + (* The output is decoded in function Index.prepare_entry of coqdoc *) let ntn = String.make (String.length df * 3) '_' in let j = ref 0 in let l = String.length df - 1 in @@ -211,8 +220,13 @@ let cook_notation df sc = (* Next token is a terminal *) ntn.[!j] <- '\''; incr j; while !i <= l && df.[!i] <> ' ' do - if df.[!i] = '\'' then (ntn.[!j] <- '\''; incr j); - ntn.[!j] <- df.[!i]; incr j; incr i + if df.[!i] < ' ' then + let c = char_of_int (int_of_char 'A' + int_of_char df.[!i] - 1) in + (String.blit ("'^" ^ String.make 1 c) 0 ntn !j 3; j := !j+3; incr i) + else begin + if df.[!i] = '\'' then (ntn.[!j] <- '\''; incr j); + ntn.[!j] <- df.[!i]; incr j; incr i + end done; ntn.[!j] <- '\''; incr j end; diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index d3215c7d..b02cc966 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -1,19 +1,18 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit val close_glob_file : unit -> unit +val start_dump_glob : string -> unit +val end_dump_glob : unit -> unit + val dump : unit -> bool -val multi_dump : unit -> bool val noglob : unit -> unit val dump_to_stdout : unit -> unit diff --git a/interp/genarg.ml b/interp/genarg.ml index dd75bbfc..e564bd11 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -1,19 +1,17 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* f c | ByNotation (loc,s,_) -> loc -type rawconstr_and_expr = rawconstr * constr_expr option +type glob_constr_and_expr = glob_constr * constr_expr option type open_constr_expr = unit * constr_expr -type open_rawconstr = unit * rawconstr_and_expr +type open_glob_constr = unit * glob_constr_and_expr -type rawconstr_pattern_and_expr = rawconstr_and_expr * Pattern.constr_pattern +type glob_constr_pattern_and_expr = glob_constr_and_expr * Pattern.constr_pattern type 'a with_ebindings = 'a * open_constr bindings diff --git a/interp/genarg.mli b/interp/genarg.mli index 54b415d1..54aadba1 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -1,18 +1,16 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* loc) -> 'a or_by_notation -> loc -(* In globalize tactics, we need to keep the initial [constr_expr] to recompute*) -(* in the environment by the effective calls to Intro, Inversion, etc *) -(* The [constr_expr] field is [None] in TacDef though *) -type rawconstr_and_expr = rawconstr * constr_expr option +(** In globalize tactics, we need to keep the initial [constr_expr] to recompute + in the environment by the effective calls to Intro, Inversion, etc + The [constr_expr] field is [None] in TacDef though *) +type glob_constr_and_expr = glob_constr * constr_expr option type open_constr_expr = unit * constr_expr -type open_rawconstr = unit * rawconstr_and_expr +type open_glob_constr = unit * glob_constr_and_expr -type rawconstr_pattern_and_expr = rawconstr_and_expr * constr_pattern +type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern type 'a with_ebindings = 'a * open_constr bindings @@ -51,40 +49,41 @@ and or_and_intro_pattern_expr = (loc * intro_pattern_expr) list list val pr_intro_pattern : intro_pattern_expr located -> Pp.std_ppcmds val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds -(* The route of a generic argument, from parsing to evaluation - -\begin{verbatim} - parsing in_raw out_raw - char stream ----> rawtype ----> constr_expr generic_argument --------| - encapsulation decaps | - | - V - rawtype - | - globalization | - V - glob_type - | - encaps | - in_glob | - V - rawconstr generic_argument - | - out in out_glob | - type <--- constr generic_argument <---- type <------ rawtype <--------| - | decaps encaps interp decaps +(** The route of a generic argument, from parsing to evaluation. +In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc. + +{% \begin{%}verbatim{% }%} + parsing in_raw out_raw + char stream ---> raw_object ---> raw_object generic_argument -------+ + encapsulation decaps| + | + V + raw_object + | + globalization | + V + glob_object + | + encaps | + in_glob | + V + glob_object generic_argument + | + out in out_glob | + object <--- object generic_argument <--- object <--- glob_object <---+ + | decaps encaps interp decaps | V effective use -\end{verbatim} +{% \end{%}verbatim{% }%} To distinguish between the uninterpreted (raw), globalized and interpreted worlds, we annotate the type [generic_argument] by a -phantom argument which is either [constr_expr], [rawconstr] or +phantom argument which is either [constr_expr], [glob_constr] or [constr]. Transformation for each type : -\begin{verbatim} +{% \begin{%}verbatim{% }%} tag raw open type cooked closed type BoolArgType bool bool @@ -107,10 +106,10 @@ List0ArgType of argument_type List1ArgType of argument_type OptArgType of argument_type ExtraArgType of string '_a '_b -\end{verbatim} +{% \end{%}verbatim{% }%} *) -(* All of [rlevel], [glevel] and [tlevel] must be non convertible +(** All of [rlevel], [glevel] and [tlevel] must be non convertible to ensure the injectivity of the type inference from type ['co generic_argument] to [('a,'co) abstract_argument_type]; this guarantees that, for 'co fixed, the type of @@ -172,40 +171,40 @@ val rawwit_quant_hyp : (quantified_hypothesis,rlevel) abstract_argument_type val globwit_quant_hyp : (quantified_hypothesis,glevel) abstract_argument_type val wit_quant_hyp : (quantified_hypothesis,tlevel) abstract_argument_type -val rawwit_sort : (rawsort,rlevel) abstract_argument_type -val globwit_sort : (rawsort,glevel) abstract_argument_type +val rawwit_sort : (glob_sort,rlevel) abstract_argument_type +val globwit_sort : (glob_sort,glevel) abstract_argument_type val wit_sort : (sorts,tlevel) abstract_argument_type val rawwit_constr : (constr_expr,rlevel) abstract_argument_type -val globwit_constr : (rawconstr_and_expr,glevel) abstract_argument_type +val globwit_constr : (glob_constr_and_expr,glevel) abstract_argument_type val wit_constr : (constr,tlevel) abstract_argument_type val rawwit_constr_may_eval : ((constr_expr,reference or_by_notation,constr_expr) may_eval,rlevel) abstract_argument_type -val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var,rawconstr_pattern_and_expr) may_eval,glevel) abstract_argument_type +val globwit_constr_may_eval : ((glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) may_eval,glevel) abstract_argument_type val wit_constr_may_eval : (constr,tlevel) abstract_argument_type val rawwit_open_constr_gen : bool -> (open_constr_expr,rlevel) abstract_argument_type -val globwit_open_constr_gen : bool -> (open_rawconstr,glevel) abstract_argument_type +val globwit_open_constr_gen : bool -> (open_glob_constr,glevel) abstract_argument_type val wit_open_constr_gen : bool -> (open_constr,tlevel) abstract_argument_type val rawwit_open_constr : (open_constr_expr,rlevel) abstract_argument_type -val globwit_open_constr : (open_rawconstr,glevel) abstract_argument_type +val globwit_open_constr : (open_glob_constr,glevel) abstract_argument_type val wit_open_constr : (open_constr,tlevel) abstract_argument_type val rawwit_casted_open_constr : (open_constr_expr,rlevel) abstract_argument_type -val globwit_casted_open_constr : (open_rawconstr,glevel) abstract_argument_type +val globwit_casted_open_constr : (open_glob_constr,glevel) abstract_argument_type val wit_casted_open_constr : (open_constr,tlevel) abstract_argument_type val rawwit_constr_with_bindings : (constr_expr with_bindings,rlevel) abstract_argument_type -val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,glevel) abstract_argument_type +val globwit_constr_with_bindings : (glob_constr_and_expr with_bindings,glevel) abstract_argument_type val wit_constr_with_bindings : (constr with_bindings sigma,tlevel) abstract_argument_type val rawwit_bindings : (constr_expr bindings,rlevel) abstract_argument_type -val globwit_bindings : (rawconstr_and_expr bindings,glevel) abstract_argument_type +val globwit_bindings : (glob_constr_and_expr bindings,glevel) abstract_argument_type val wit_bindings : (constr bindings sigma,tlevel) abstract_argument_type val rawwit_red_expr : ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,rlevel) abstract_argument_type -val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var,rawconstr_pattern_and_expr) red_expr_gen,glevel) abstract_argument_type +val globwit_red_expr : ((glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,glevel) abstract_argument_type val wit_red_expr : ((constr,evaluable_global_reference,constr_pattern) red_expr_gen,tlevel) abstract_argument_type val wit_list0 : @@ -222,7 +221,7 @@ val wit_pair : ('b,'co) abstract_argument_type -> ('a * 'b,'co) abstract_argument_type -(* ['a generic_argument] = (Sigma t:type. t[[constr/'a]]) *) +(** ['a generic_argument] = (Sigma t:type. t[[constr/'a]]) *) type 'a generic_argument val fold_list0 : @@ -238,7 +237,7 @@ val fold_pair : ('a generic_argument -> 'a generic_argument -> 'c) -> 'a generic_argument -> 'c -(* [app_list0] fails if applied to an argument not of tag [List0 t] +(** [app_list0] fails if applied to an argument not of tag [List0 t] for some [t]; it's the responsability of the caller to ensure it *) val app_list0 : ('a generic_argument -> 'b generic_argument) -> @@ -255,7 +254,7 @@ val app_pair : ('a generic_argument -> 'b generic_argument) -> 'a generic_argument -> 'b generic_argument -(* create a new generic type of argument: force to associate +(** create a new generic type of argument: force to associate unique ML types at each of the three levels *) val create_arg : string -> ('a,tlevel) abstract_argument_type @@ -265,7 +264,7 @@ val create_arg : string -> val exists_argtype : string -> bool type argument_type = - (* Basic types *) + (** Basic types *) | BoolArgType | IntArgType | IntOrVarArgType @@ -275,7 +274,7 @@ type argument_type = | IdentArgType of bool | VarArgType | RefArgType - (* Specific types *) + (** Specific types *) | SortArgType | ConstrArgType | ConstrMayEvalArgType @@ -300,7 +299,7 @@ val out_gen : ('a,'co) abstract_argument_type -> 'co generic_argument -> 'a -(* [in_generic] is used in combination with camlp4 [Gramext.action] magic +(** [in_generic] is used in combination with camlp4 [Gramext.action] magic [in_generic: !l:type, !a:argument_type -> |a|_l -> 'l generic_argument] diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 88ed0873..f2739043 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* obj = declare_object {(default_object "GENERALIZED-IDENT") with load_function = load_generalizable_type; cache_function = cache_generalizable_type; classify_function = (fun (local, _ as obj) -> if local then Dispose else Keep obj) } - + let declare_generalizable local gen = Lib.add_anonymous_leaf (in_generalizable (local, gen)) @@ -138,33 +136,33 @@ let add_name_to_ids set na = | Anonymous -> set | Name id -> Idset.add id set -let generalizable_vars_of_rawconstr ?(bound=Idset.empty) ?(allowed=Idset.empty) = +let generalizable_vars_of_glob_constr ?(bound=Idset.empty) ?(allowed=Idset.empty) = let rec vars bound vs = function - | RVar (loc,id) -> + | GVar (loc,id) -> if is_freevar bound (Global.env ()) id then if List.mem_assoc id vs then vs else (id, loc) :: vs else vs - | RApp (loc,f,args) -> List.fold_left (vars bound) vs (f::args) - | RLambda (loc,na,_,ty,c) | RProd (loc,na,_,ty,c) | RLetIn (loc,na,ty,c) -> + | GApp (loc,f,args) -> List.fold_left (vars bound) vs (f::args) + | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) | GLetIn (loc,na,ty,c) -> let vs' = vars bound vs ty in let bound' = add_name_to_ids bound na in vars bound' vs' c - | RCases (loc,sty,rtntypopt,tml,pl) -> + | GCases (loc,sty,rtntypopt,tml,pl) -> let vs1 = vars_option bound vs rtntypopt in let vs2 = List.fold_left (fun vs (tm,_) -> vars bound vs tm) vs1 tml in List.fold_left (vars_pattern bound) vs2 pl - | RLetTuple (loc,nal,rtntyp,b,c) -> + | GLetTuple (loc,nal,rtntyp,b,c) -> let vs1 = vars_return_type bound vs rtntyp in let vs2 = vars bound vs1 b in let bound' = List.fold_left add_name_to_ids bound nal in vars bound' vs2 c - | RIf (loc,c,rtntyp,b1,b2) -> + | GIf (loc,c,rtntyp,b1,b2) -> let vs1 = vars_return_type bound vs rtntyp in let vs2 = vars bound vs1 c in let vs3 = vars bound vs2 b1 in vars bound vs3 b2 - | RRec (loc,fk,idl,bl,tyl,bv) -> + | GRec (loc,fk,idl,bl,tyl,bv) -> let bound' = Array.fold_right Idset.add idl bound in let vars_fix i vs fid = let vs1,bound1 = @@ -182,9 +180,9 @@ let generalizable_vars_of_rawconstr ?(bound=Idset.empty) ?(allowed=Idset.empty) vars bound1 vs2 bv.(i) in array_fold_left_i vars_fix vs idl - | RCast (loc,c,k) -> let v = vars bound vs c in + | GCast (loc,c,k) -> let v = vars bound vs c in (match k with CastConv (_,t) -> vars bound v t | _ -> v) - | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> vs + | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs and vars_pattern bound vs (loc,idl,p,c) = let bound' = List.fold_right Idset.add idl bound in @@ -205,8 +203,6 @@ let generalizable_vars_of_rawconstr ?(bound=Idset.empty) ?(allowed=Idset.empty) let rec make_fresh ids env x = if is_freevar ids env x then x else make_fresh ids env (Nameops.lift_subscript x) -let next_ident_away_from id avoid = make_fresh avoid (Global.env ()) id - let next_name_away_from na avoid = match na with | Anonymous -> make_fresh avoid (Global.env ()) (id_of_string "anon") @@ -297,28 +293,32 @@ let implicit_application env ?(allow_partial=true) f ty = CAppExpl (loc, (None, id), args), avoid in c, avoid -let implicits_of_rawterm ?(with_products=true) l = - let rec aux i c = - let abs loc na bk t b = - let rest = aux (succ i) b in - if bk = Implicit then +let implicits_of_glob_constr ?(with_products=true) l = + let add_impl i na bk l = + if bk = Implicit then let name = match na with | Name id -> Some id | Anonymous -> None in - (ExplByPos (i, name), (true, true, true)) :: rest - else rest + (ExplByPos (i, name), (true, true, true)) :: l + else l in + let rec aux i c = + let abs na bk b = + add_impl i na bk (aux (succ i) b) in match c with - | RProd (loc, na, bk, t, b) -> - if with_products then abs loc na bk t b + | GProd (loc, na, bk, t, b) -> + if with_products then abs na bk b else (if bk = Implicit then msg_warning (str "Ignoring implicit status of product binder " ++ pr_name na ++ str " and following binders"); []) - | RLambda (loc, na, bk, t, b) -> abs loc na bk t b - | RLetIn (loc, na, t, b) -> aux i b + | GLambda (loc, na, bk, t, b) -> abs na bk b + | GLetIn (loc, na, t, b) -> aux i b + | GRec (_, fix_kind, nas, args, tys, bds) -> + let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in + list_fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb) | _ -> [] in aux 1 l diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 4442e09d..ce518a9c 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -1,14 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* (identifier located) list option -> unit @@ -30,7 +26,7 @@ val ids_of_list : identifier list -> Idset.t val destClassApp : constr_expr -> loc * reference * constr_expr list val destClassAppExpl : constr_expr -> loc * reference * (constr_expr * explicitation located option) list -(* Fragile, should be used only for construction a set of identifiers to avoid *) +(** Fragile, should be used only for construction a set of identifiers to avoid *) val free_vars_of_constr_expr : constr_expr -> ?bound:Idset.t -> identifier list -> identifier list @@ -38,15 +34,15 @@ val free_vars_of_constr_expr : constr_expr -> ?bound:Idset.t -> val free_vars_of_binders : ?bound:Idset.t -> Names.identifier list -> local_binder list -> Idset.t * Names.identifier list -(* Returns the generalizable free ids in left-to-right +(** Returns the generalizable free ids in left-to-right order with the location of their first occurence *) -val generalizable_vars_of_rawconstr : ?bound:Idset.t -> ?allowed:Idset.t -> - rawconstr -> (Names.identifier * loc) list +val generalizable_vars_of_glob_constr : ?bound:Idset.t -> ?allowed:Idset.t -> + glob_constr -> (Names.identifier * loc) list val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier -val implicits_of_rawterm : ?with_products:bool -> Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool * bool)) list +val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits val combine_params_freevar : Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) -> diff --git a/interp/interp.mllib b/interp/interp.mllib index 3825f3d8..546f277e 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -1,3 +1,4 @@ +Tok Lexer Topconstr Ppextend @@ -15,4 +16,3 @@ Constrextern Coqlib Discharge Declare - diff --git a/interp/modintern.ml b/interp/modintern.ml index f53d1796..a13560c0 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* 'a + +val error_not_a_functor : module_struct_entry -> 'a + +val error_not_equal : module_path -> module_path -> 'a + +val error_result_must_be_signature : unit -> 'a + +oval error_not_a_modtype_loc : loc -> string -> 'a + +val error_not_a_module_loc : loc -> string -> 'a + +val error_not_a_module_or_modtype_loc : loc -> string -> 'a + +val error_with_in_module : unit -> 'a + +val error_application_to_module_type : unit -> 'a +*) + +let error_result_must_be_signature () = + error "The result module type must be a signature." + +let error_not_a_modtype_loc loc s = + Compat.Loc.raise loc (Modops.ModuleTypingError (Modops.NotAModuleType s)) + +let error_not_a_module_loc loc s = + Compat.Loc.raise loc (Modops.ModuleTypingError (Modops.NotAModule s)) + +let error_not_a_module_nor_modtype_loc loc s = + Compat.Loc.raise loc (ModuleInternalizationError (NotAModuleNorModtype s)) + +let error_incorrect_with_in_module loc = + Compat.Loc.raise loc (ModuleInternalizationError IncorrectWithInModule) + +let error_application_to_module_type loc = + Compat.Loc.raise loc (ModuleInternalizationError IncorrectModuleApplication) + + + + let rec make_mp mp = function [] -> mp | h::tl -> make_mp (MPdot(mp, label_of_id h)) tl @@ -70,7 +116,7 @@ let lookup_module (loc,qid) = let mp = Nametab.locate_module qid in Dumpglob.dump_modref loc mp "modtype"; mp with - | Not_found -> Modops.error_not_a_module_loc loc (string_of_qualid qid) + | Not_found -> error_not_a_module_loc loc (string_of_qualid qid) let lookup_modtype (loc,qid) = try @@ -78,7 +124,7 @@ let lookup_modtype (loc,qid) = Dumpglob.dump_modref loc mp "mod"; mp with | Not_found -> - Modops.error_not_a_modtype_loc loc (string_of_qualid qid) + error_not_a_modtype_loc loc (string_of_qualid qid) let lookup_module_or_modtype (loc,qid) = try @@ -88,7 +134,7 @@ let lookup_module_or_modtype (loc,qid) = let mp = Nametab.locate_modtype qid in Dumpglob.dump_modref loc mp "mod"; (mp,false) with Not_found -> - Modops.error_not_a_module_or_modtype_loc loc (string_of_qualid qid) + error_not_a_module_nor_modtype_loc loc (string_of_qualid qid) let transl_with_decl env = function | CWith_Module ((_,fqid),qid) -> @@ -96,24 +142,35 @@ let transl_with_decl env = function | CWith_Definition ((_,fqid),c) -> With_Definition (fqid,interp_constr Evd.empty env c) +let loc_of_module = function + | CMident (loc,_) | CMapply (loc,_,_) | CMwith (loc,_,_) -> loc + +let check_module_argument_is_path me' = function + | CMident _ -> () + | (CMapply (loc,_,_) | CMwith (loc,_,_)) -> + Compat.Loc.raise loc + (Modops.ModuleTypingError (Modops.ApplicationToNotPath me')) + let rec interp_modexpr env = function | CMident qid -> MSEident (lookup_module qid) - | CMapply (me1,me2) -> - let me1 = interp_modexpr env me1 in - let me2 = interp_modexpr env me2 in - MSEapply(me1,me2) - | CMwith _ -> Modops.error_with_in_module () + | CMapply (_,me1,me2) -> + let me1' = interp_modexpr env me1 in + let me2' = interp_modexpr env me2 in + check_module_argument_is_path me2' me2; + MSEapply(me1',me2') + | CMwith (loc,_,_) -> error_incorrect_with_in_module loc let rec interp_modtype env = function | CMident qid -> MSEident (lookup_modtype qid) - | CMapply (mty1,me) -> + | CMapply (_,mty1,me) -> let mty' = interp_modtype env mty1 in let me' = interp_modexpr env me in - MSEapply(mty',me') - | CMwith (mty,decl) -> + check_module_argument_is_path me' me; + MSEapply(mty',me') + | CMwith (_,mty,decl) -> let mty = interp_modtype env mty in let decl = transl_with_decl env decl in MSEwith(mty,decl) @@ -122,13 +179,14 @@ let rec interp_modexpr_or_modtype env = function | CMident qid -> let (mp,ismod) = lookup_module_or_modtype qid in (MSEident mp, ismod) - | CMapply (me1,me2) -> - let me1,ismod1 = interp_modexpr_or_modtype env me1 in - let me2,ismod2 = interp_modexpr_or_modtype env me2 in - if not ismod2 then Modops.error_application_to_module_type (); - (MSEapply (me1,me2), ismod1) - | CMwith (me,decl) -> + | CMapply (_,me1,me2) -> + let me1',ismod1 = interp_modexpr_or_modtype env me1 in + let me2',ismod2 = interp_modexpr_or_modtype env me2 in + check_module_argument_is_path me2' me2; + if not ismod2 then error_application_to_module_type (loc_of_module me2); + (MSEapply (me1',me2'), ismod1) + | CMwith (loc,me,decl) -> let me,ismod = interp_modexpr_or_modtype env me in let decl = transl_with_decl env decl in - if ismod then Modops.error_with_in_module (); + if ismod then error_incorrect_with_in_module loc; (MSEwith(me,decl), ismod) diff --git a/interp/modintern.mli b/interp/modintern.mli index e3a7cc6a..71a00c2f 100644 --- a/interp/modintern.mli +++ b/interp/modintern.mli @@ -1,14 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* module_ast -> module_struct_entry val interp_modexpr : env -> module_ast -> module_struct_entry -(* The following function tries to interprete an ast as a module, +(** The following function tries to interprete an ast as a module, and in case of failure, interpretes this ast as a module type. The boolean is true for a module, false for a module type *) diff --git a/interp/notation.ml b/interp/notation.ml index 6e02c40b..8f19ab85 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* -(* Flags.if_verbose message ("Creating scope "^scope);*) +(* Flags.if_warn message ("Creating scope "^scope);*) scope_map := Gmap.add scope empty_scope !scope_map let find_scope scope = @@ -119,7 +117,7 @@ let discharge_scope (_,(local,_,_ as o)) = let classify_scope (local,_,_ as o) = if local then Dispose else Substitute o -let (inScope,outScope) = +let inScope : bool * bool * scope_elem -> obj = declare_object {(default_object "SCOPE") with cache_function = cache_scope; open_function = open_scope; @@ -153,15 +151,15 @@ let declare_delimiters scope key = | None -> scope_map := Gmap.add scope newsc !scope_map | Some oldkey when oldkey = key -> () | Some oldkey -> - Flags.if_verbose warning - ("overwriting previous delimiting key "^oldkey^" in scope "^scope); + Flags.if_warn msg_warning + (str ("Overwriting previous delimiting key "^oldkey^" in scope "^scope)); scope_map := Gmap.add scope newsc !scope_map end; try let oldscope = Gmap.find key !delimiters_map in if oldscope = scope then () else begin - Flags.if_verbose warning ("Hiding binding of key "^key^" to "^oldscope); + Flags.if_warn msg_warning (str ("Hiding binding of key "^key^" to "^oldscope)); delimiters_map := Gmap.add key scope !delimiters_map end with Not_found -> delimiters_map := Gmap.add key scope !delimiters_map @@ -178,7 +176,7 @@ type interp_rule = | NotationRule of scope_name option * notation | SynDefRule of kernel_name -(* We define keys for rawterm and aconstr to split the syntax entries +(* We define keys for glob_constr and aconstr to split the syntax entries according to the key of the pattern (adapted from Chet Murthy by HH) *) type key = @@ -189,30 +187,25 @@ type key = let notations_key_table = ref Gmapl.empty let prim_token_key_table = Hashtbl.create 7 - -let make_gr = function - | ConstRef con -> - ConstRef(constant_of_kn(canonical_con con)) - | IndRef (kn,i) -> - IndRef(mind_of_kn(canonical_mind kn),i) - | ConstructRef ((kn,i),j )-> - ConstructRef((mind_of_kn(canonical_mind kn),i),j) - | VarRef id -> VarRef id - -let rawconstr_key = function - | RApp (_,RRef (_,ref),_) -> RefKey (make_gr ref) - | RRef (_,ref) -> RefKey (make_gr ref) +let glob_prim_constr_key = function + | GApp (_,GRef (_,ref),_) | GRef (_,ref) -> RefKey (canonical_gr ref) | _ -> Oth +let glob_constr_keys = function + | GApp (_,GRef (_,ref),_) -> [RefKey (canonical_gr ref); Oth] + | GRef (_,ref) -> [RefKey (canonical_gr ref)] + | _ -> [Oth] + let cases_pattern_key = function - | PatCstr (_,ref,_,_) -> RefKey (make_gr (ConstructRef ref)) + | PatCstr (_,ref,_,_) -> RefKey (canonical_gr (ConstructRef ref)) | _ -> Oth let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *) - | AApp (ARef ref,args) -> RefKey(make_gr ref), Some (List.length args) + | AApp (ARef ref,args) -> RefKey(canonical_gr ref), Some (List.length args) | AList (_,_,AApp (ARef ref,args),_,_) - | ABinderList (_,_,AApp (ARef ref,args),_) -> RefKey (make_gr ref), Some (List.length args) - | ARef ref -> RefKey(make_gr ref), None + | ABinderList (_,_,AApp (ARef ref,args),_) -> RefKey (canonical_gr ref), Some (List.length args) + | ARef ref -> RefKey(canonical_gr ref), None + | AApp (_,args) -> Oth, Some (List.length args) | _ -> Oth, None (**********************************************************************) @@ -221,15 +214,15 @@ let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *) type required_module = full_path * string list type 'a prim_token_interpreter = - loc -> 'a -> rawconstr + loc -> 'a -> glob_constr type cases_pattern_status = bool (* true = use prim token in patterns *) type 'a prim_token_uninterpreter = - rawconstr list * (rawconstr -> 'a option) * cases_pattern_status + glob_constr list * (glob_constr -> 'a option) * cases_pattern_status type internal_prim_token_interpreter = - loc -> prim_token -> required_module * (unit -> rawconstr) + loc -> prim_token -> required_module * (unit -> glob_constr) let prim_token_interpreter_tab = (Hashtbl.create 7 : (scope_name, internal_prim_token_interpreter) Hashtbl.t) @@ -246,7 +239,8 @@ let declare_prim_token_interpreter sc interp (patl,uninterp,b) = declare_scope sc; add_prim_token_interpreter sc interp; List.iter (fun pat -> - Hashtbl.add prim_token_key_table (rawconstr_key pat) (sc,uninterp,b)) + Hashtbl.add prim_token_key_table + (glob_prim_constr_key pat) (sc,uninterp,b)) patl let mkNumeral n = Numeral n @@ -353,7 +347,7 @@ let find_prim_token g loc p sc = (* Try for a user-defined numerical notation *) try let (_,c),df = find_notation (notation_of_prim_token p) sc in - g (rawconstr_of_aconstr loc c),df + g (glob_constr_of_aconstr loc c),df with Not_found -> (* Try for a primitive numerical notation *) let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc loc p in @@ -374,7 +368,7 @@ let interp_prim_token = interp_prim_token_gen (fun x -> x) let interp_prim_token_cases_pattern loc p name = - interp_prim_token_gen (cases_pattern_of_rawconstr name) loc p + interp_prim_token_gen (cases_pattern_of_glob_constr name) loc p let rec interp_notation loc ntn local_scopes = let scopes = make_current_scopes local_scopes in @@ -383,8 +377,11 @@ let rec interp_notation loc ntn local_scopes = user_err_loc (loc,"",str ("Unknown interpretation for notation \""^ntn^"\".")) +let isGApp = function GApp _ -> true | _ -> false + let uninterp_notations c = - Gmapl.find (rawconstr_key c) !notations_key_table + list_map_append (fun key -> Gmapl.find key !notations_key_table) + (glob_constr_keys c) let uninterp_cases_pattern_notations c = Gmapl.find (cases_pattern_key c) !notations_key_table @@ -396,7 +393,8 @@ let availability_of_notation (ntn_scope,ntn) scopes = let uninterp_prim_token c = try - let (sc,numpr,_) = Hashtbl.find prim_token_key_table (rawconstr_key c) in + let (sc,numpr,_) = + Hashtbl.find prim_token_key_table (glob_prim_constr_key c) in match numpr c with | None -> raise No_match | Some n -> (sc,n) @@ -407,7 +405,7 @@ let uninterp_prim_token_cases_pattern c = let k = cases_pattern_key c in let (sc,numpr,b) = Hashtbl.find prim_token_key_table k in if not b then raise No_match; - let na,c = rawconstr_of_closed_cases_pattern c in + let na,c = glob_constr_of_closed_cases_pattern c in match numpr c with | None -> raise No_match | Some n -> (na,sc,n) @@ -439,7 +437,8 @@ open Classops let class_scope_map = ref (Gmap.empty : (cl_typ,scope_name) Gmap.t) -let _ = Gmap.add CL_SORT "type_scope" Gmap.empty +let _ = + class_scope_map := Gmap.add CL_SORT "type_scope" Gmap.empty let declare_class_scope sc cl = class_scope_map := Gmap.add cl sc !class_scope_map @@ -447,27 +446,39 @@ let declare_class_scope sc cl = let find_class_scope cl = Gmap.find cl !class_scope_map -let find_class t = - let t, _ = decompose_app (Reductionops.whd_betaiotazeta Evd.empty t) in - match kind_of_term t with - | Var id -> CL_SECVAR id - | Const sp -> CL_CONST sp - | Ind ind_sp -> CL_IND ind_sp - | Prod (_,_,_) -> CL_FUN - | Sort _ -> CL_SORT - | _ -> raise Not_found +let find_class_scope_opt = function + | None -> None + | Some cl -> try Some (find_class_scope cl) with Not_found -> None + +let find_class t = fst (find_class_type Evd.empty t) (**********************************************************************) (* Special scopes associated to arguments of a global reference *) -let rec compute_arguments_scope t = +let rec compute_arguments_classes t = match kind_of_term (Reductionops.whd_betaiotazeta Evd.empty t) with | Prod (_,t,u) -> - let sc = - try Some (find_class_scope (find_class t)) with Not_found -> None in - sc :: compute_arguments_scope u + let cl = try Some (find_class t) with Not_found -> None in + cl :: compute_arguments_classes u | _ -> [] +let compute_arguments_scope_full t = + let cls = compute_arguments_classes t in + let scs = List.map find_class_scope_opt cls in + scs, cls + +let compute_arguments_scope t = fst (compute_arguments_scope_full t) + +(** When merging scope list, we give priority to the first one (computed + by substitution), using the second one (user given or earlier automatic) + as fallback *) + +let rec merge_scope sc1 sc2 = match sc1, sc2 with + | [], _ -> sc2 + | _, [] -> sc1 + | Some sc :: sc1, _ :: sc2 -> Some sc :: merge_scope sc1 sc2 + | None :: sc1, sco :: sc2 -> sco :: merge_scope sc1 sc2 + let arguments_scope = ref Refmap.empty type arguments_scope_discharge_request = @@ -475,36 +486,47 @@ type arguments_scope_discharge_request = | ArgsScopeManual | ArgsScopeNoDischarge -let load_arguments_scope _ (_,(_,r,scl)) = +let load_arguments_scope _ (_,(_,r,scl,cls)) = List.iter (Option.iter check_scope) scl; - arguments_scope := Refmap.add r scl !arguments_scope + arguments_scope := Refmap.add r (scl,cls) !arguments_scope let cache_arguments_scope o = load_arguments_scope 1 o -let subst_arguments_scope (subst,(req,r,scl)) = - (ArgsScopeNoDischarge,fst (subst_global subst r),scl) +let subst_arguments_scope (subst,(req,r,scl,cls)) = + let r' = fst (subst_global subst r) in + let subst_cl cl = + try Option.smartmap (subst_cl_typ subst) cl with Not_found -> None in + let cls' = list_smartmap subst_cl cls in + let scl' = merge_scope (List.map find_class_scope_opt cls') scl in + let scl'' = List.map (Option.map Declaremods.subst_scope) scl' in + (ArgsScopeNoDischarge,r',scl'',cls') -let discharge_arguments_scope (_,(req,r,l)) = +let discharge_arguments_scope (_,(req,r,l,_)) = if req = ArgsScopeNoDischarge or (isVarRef r & Lib.is_in_section r) then None - else Some (req,Lib.discharge_global r,l) + else Some (req,Lib.discharge_global r,l,[]) -let classify_arguments_scope (req,_,_ as obj) = +let classify_arguments_scope (req,_,_,_ as obj) = if req = ArgsScopeNoDischarge then Dispose else Substitute obj -let rebuild_arguments_scope (req,r,l) = +let rebuild_arguments_scope (req,r,l,_) = match req with | ArgsScopeNoDischarge -> assert false | ArgsScopeAuto -> - (req,r,compute_arguments_scope (Global.type_of_global r)) + let scs,cls = compute_arguments_scope_full (Global.type_of_global r) in + (req,r,scs,cls) | ArgsScopeManual -> (* Add to the manually given scopes the one found automatically for the extra parameters of the section *) - let l' = compute_arguments_scope (Global.type_of_global r) in + let l',cls = compute_arguments_scope_full (Global.type_of_global r) in let l1,_ = list_chop (List.length l' - List.length l) l' in - (req,r,l1@l) + (req,r,l1@l,cls) + +type arguments_scope_obj = + arguments_scope_discharge_request * global_reference * + scope_name option list * Classops.cl_typ option list -let (inArgumentsScope,outArgumentsScope) = +let inArgumentsScope : arguments_scope_obj -> obj = declare_object {(default_object "ARGUMENTS-SCOPE") with cache_function = cache_arguments_scope; load_function = load_arguments_scope; @@ -515,21 +537,22 @@ let (inArgumentsScope,outArgumentsScope) = let is_local local ref = local || isVarRef ref && Lib.is_in_section ref -let declare_arguments_scope_gen req r scl = - Lib.add_anonymous_leaf (inArgumentsScope (req,r,scl)) +let declare_arguments_scope_gen req r (scl,cls) = + Lib.add_anonymous_leaf (inArgumentsScope (req,r,scl,cls)) let declare_arguments_scope local ref scl = let req = if is_local local ref then ArgsScopeNoDischarge else ArgsScopeManual in - declare_arguments_scope_gen req ref scl + declare_arguments_scope_gen req ref (scl,[]) let find_arguments_scope r = - try Refmap.find r !arguments_scope + try fst (Refmap.find r !arguments_scope) with Not_found -> [] let declare_ref_arguments_scope ref = let t = Global.type_of_global ref in - declare_arguments_scope_gen ArgsScopeAuto ref (compute_arguments_scope t) + declare_arguments_scope_gen ArgsScopeAuto ref (compute_arguments_scope_full t) + (********************************) (* Encoding notations as string *) @@ -585,11 +608,11 @@ let pr_scope_classes sc = hov 0 (str ("Bound to class"^(if List.tl l=[] then "" else "es")) ++ spc() ++ prlist_with_sep spc pr_class l) ++ fnl() -let pr_notation_info prraw ntn c = +let pr_notation_info prglob ntn c = str "\"" ++ str ntn ++ str "\" := " ++ - prraw (rawconstr_of_aconstr dummy_loc c) + prglob (glob_constr_of_aconstr dummy_loc c) -let pr_named_scope prraw scope sc = +let pr_named_scope prglob scope sc = (if scope = default_scope then match Gmap.fold (fun _ _ x -> x+1) sc.notations 0 with | 0 -> str "No lonely notation" @@ -600,14 +623,14 @@ let pr_named_scope prraw scope sc = ++ pr_scope_classes scope ++ Gmap.fold (fun ntn ((_,r),(_,df)) strm -> - pr_notation_info prraw df r ++ fnl () ++ strm) + pr_notation_info prglob df r ++ fnl () ++ strm) sc.notations (mt ()) -let pr_scope prraw scope = pr_named_scope prraw scope (find_scope scope) +let pr_scope prglob scope = pr_named_scope prglob scope (find_scope scope) -let pr_scopes prraw = +let pr_scopes prglob = Gmap.fold - (fun scope sc strm -> pr_named_scope prraw scope sc ++ fnl () ++ strm) + (fun scope sc strm -> pr_named_scope prglob scope sc ++ fnl () ++ strm) !scope_map (mt ()) let rec find_default ntn = function @@ -627,9 +650,6 @@ let factorize_entries = function (ntn,[c],[]) l in (ntn,l_of_ntn)::rest -let is_ident s = (* Poor analysis *) - String.length s <> 0 & is_letter s.[0] - let browse_notation strict ntn map = let find = if String.contains ntn ' ' then (=) ntn @@ -677,7 +697,7 @@ let interp_notation_as_global_reference loc test ntn sc = | [] -> error_notation_not_reference loc ntn | _ -> error_ambiguous_notation loc ntn -let locate_notation prraw ntn scope = +let locate_notation prglob ntn scope = let ntns = factorize_entries (browse_notation false ntn !scope_map) in let scopes = Option.fold_right push_scope scope !scope_stack in if ntns = [] then @@ -690,7 +710,7 @@ let locate_notation prraw ntn scope = prlist (fun (sc,r,(_,df)) -> hov 0 ( - pr_notation_info prraw df r ++ tbrk (1,2) ++ + pr_notation_info prglob df r ++ tbrk (1,2) ++ (if sc = default_scope then mt () else (str ": " ++ str sc)) ++ tbrk (1,2) ++ (if Some sc = scope then str "(default interpretation)" else mt ()) @@ -726,10 +746,10 @@ let collect_notations stack = (all',ntn::knownntn)) ([],[]) stack) -let pr_visible_in_scope prraw (scope,ntns) = +let pr_visible_in_scope prglob (scope,ntns) = let strm = List.fold_right - (fun (df,r) strm -> pr_notation_info prraw df r ++ fnl () ++ strm) + (fun (df,r) strm -> pr_notation_info prglob df r ++ fnl () ++ strm) ntns (mt ()) in (if scope = default_scope then str "Lonely notation" ++ (if List.length ntns <> 1 then str "s" else mt()) @@ -737,14 +757,14 @@ let pr_visible_in_scope prraw (scope,ntns) = str "Visible in scope " ++ str scope) ++ fnl () ++ strm -let pr_scope_stack prraw stack = +let pr_scope_stack prglob stack = List.fold_left - (fun strm scntns -> strm ++ pr_visible_in_scope prraw scntns ++ fnl ()) + (fun strm scntns -> strm ++ pr_visible_in_scope prglob scntns ++ fnl ()) (mt ()) (collect_notations stack) -let pr_visibility prraw = function - | Some scope -> pr_scope_stack prraw (push_scope scope !scope_stack) - | None -> pr_scope_stack prraw !scope_stack +let pr_visibility prglob = function + | Some scope -> pr_scope_stack prglob (push_scope scope !scope_stack) + | None -> pr_scope_stack prglob !scope_stack (**********************************************************************) (* Mapping notations to concrete syntax *) diff --git a/interp/notation.mli b/interp/notation.mli index 33ffe7b4..f92ef94e 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -1,36 +1,31 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit val current_scopes : unit -> scopes -(* Check where a scope is opened or not in a scope list, or in +(** Check where a scope is opened or not in a scope list, or in * the current opened scopes *) val scope_is_open_in_scopes : scope_name -> scopes -> bool val scope_is_open : scope_name -> bool -(* Open scope *) +(** Open scope *) val open_close_scope : - (* locality *) bool * (* open *) bool * scope_name -> unit + (** locality *) bool * (* open *) bool * scope_name -> unit -(* Extend a list of scopes *) +(** Extend a list of scopes *) val empty_scope_stack : scopes val push_scope : scope_name -> scopes -> scopes -(* Declare delimiters for printing *) +val find_scope : scope_name -> scope + +(** Declare delimiters for printing *) val declare_delimiters : scope_name -> delimiters -> unit val find_delimiters_scope : loc -> delimiters -> scope_name -(*s Declare and uses back and forth an interpretation of primitive token *) +(** {6 Declare and uses back and forth an interpretation of primitive token } *) -(* A numeral interpreter is the pair of an interpreter for **integer** +(** A numeral interpreter is the pair of an interpreter for **integer** numbers in terms and an optional interpreter in pattern, if negative numbers are not supported, the interpreter must fail with an appropriate error message *) type notation_location = (dir_path * dir_path) * string type required_module = full_path * string list -type cases_pattern_status = bool (* true = use prim token in patterns *) +type cases_pattern_status = bool (** true = use prim token in patterns *) type 'a prim_token_interpreter = - loc -> 'a -> rawconstr + loc -> 'a -> glob_constr type 'a prim_token_uninterpreter = - rawconstr list * (rawconstr -> 'a option) * cases_pattern_status + glob_constr list * (glob_constr -> 'a option) * cases_pattern_status val declare_numeral_interpreter : scope_name -> required_module -> bigint prim_token_interpreter -> bigint prim_token_uninterpreter -> unit @@ -81,28 +78,28 @@ val declare_numeral_interpreter : scope_name -> required_module -> val declare_string_interpreter : scope_name -> required_module -> string prim_token_interpreter -> string prim_token_uninterpreter -> unit -(* Return the [term]/[cases_pattern] bound to a primitive token in a +(** Return the [term]/[cases_pattern] bound to a primitive token in a given scope context*) val interp_prim_token : loc -> prim_token -> local_scopes -> - rawconstr * (notation_location * scope_name option) + glob_constr * (notation_location * scope_name option) val interp_prim_token_cases_pattern : loc -> prim_token -> name -> local_scopes -> cases_pattern * (notation_location * scope_name option) -(* Return the primitive token associated to a [term]/[cases_pattern]; +(** Return the primitive token associated to a [term]/[cases_pattern]; raise [No_match] if no such token *) val uninterp_prim_token : - rawconstr -> scope_name * prim_token + glob_constr -> scope_name * prim_token val uninterp_prim_token_cases_pattern : cases_pattern -> name * scope_name * prim_token val availability_of_prim_token : prim_token -> scope_name -> local_scopes -> delimiters option option -(*s Declare and interpret back and forth a notation *) +(** {6 Declare and interpret back and forth a notation } *) -(* Binds a notation in a given scope to an interpretation *) +(** Binds a notation in a given scope to an interpretation *) type interp_rule = | NotationRule of scope_name option * notation | SynDefRule of kernel_name @@ -112,39 +109,39 @@ val declare_notation_interpretation : notation -> scope_name option -> val declare_uninterpretation : interp_rule -> interpretation -> unit -(* Return the interpretation bound to a notation *) +(** Return the interpretation bound to a notation *) val interp_notation : loc -> notation -> local_scopes -> interpretation * (notation_location * scope_name option) -(* Return the possible notations for a given term *) -val uninterp_notations : rawconstr -> +(** Return the possible notations for a given term *) +val uninterp_notations : glob_constr -> (interp_rule * interpretation * int option) list val uninterp_cases_pattern_notations : cases_pattern -> (interp_rule * interpretation * int option) list -(* Test if a notation is available in the scopes *) -(* context [scopes]; if available, the result is not None; the first *) -(* argument is itself not None if a delimiters is needed *) +(** Test if a notation is available in the scopes + context [scopes]; if available, the result is not None; the first + argument is itself not None if a delimiters is needed *) val availability_of_notation : scope_name option * notation -> local_scopes -> (scope_name option * delimiters option) option -(*s Declare and test the level of a (possibly uninterpreted) notation *) +(** {6 Declare and test the level of a (possibly uninterpreted) notation } *) val declare_notation_level : notation -> level -> unit -val level_of_notation : notation -> level (* raise [Not_found] if no level *) +val level_of_notation : notation -> level (** raise [Not_found] if no level *) -(*s** Miscellaneous *) +(** {6 Miscellaneous} *) val interp_notation_as_global_reference : loc -> (global_reference -> bool) -> notation -> delimiters option -> global_reference -(* Checks for already existing notations *) +(** Checks for already existing notations *) val exists_notation_in_scope : scope_name option -> notation -> interpretation -> bool -(* Declares and looks for scopes associated to arguments of a global ref *) +(** Declares and looks for scopes associated to arguments of a global ref *) val declare_arguments_scope : - bool (* true=local *) -> global_reference -> scope_name option list -> unit + bool (** true=local *) -> global_reference -> scope_name option list -> unit val find_arguments_scope : global_reference -> scope_name option list @@ -153,7 +150,7 @@ val declare_ref_arguments_scope : global_reference -> unit val compute_arguments_scope : Term.types -> scope_name option list -(* Building notation key *) +(** Building notation key *) type symbol = | Terminal of string @@ -164,21 +161,19 @@ type symbol = val make_notation_key : symbol list -> notation val decompose_notation_key : notation -> symbol list -(* Prints scopes (expects a pure aconstr printer) *) -val pr_scope : (rawconstr -> std_ppcmds) -> scope_name -> std_ppcmds -val pr_scopes : (rawconstr -> std_ppcmds) -> std_ppcmds -val locate_notation : (rawconstr -> std_ppcmds) -> notation -> +(** Prints scopes (expects a pure aconstr printer) *) +val pr_scope : (glob_constr -> std_ppcmds) -> scope_name -> std_ppcmds +val pr_scopes : (glob_constr -> std_ppcmds) -> std_ppcmds +val locate_notation : (glob_constr -> std_ppcmds) -> notation -> scope_name option -> std_ppcmds -val pr_visibility: (rawconstr -> std_ppcmds) -> scope_name option -> std_ppcmds +val pr_visibility: (glob_constr -> std_ppcmds) -> scope_name option -> std_ppcmds -(**********************************************************************) -(*s Printing rules for notations *) +(** {6 Printing rules for notations} *) -(* Declare and look for the printing rule for symbolic notations *) +(** Declare and look for the printing rule for symbolic notations *) type unparsing_rule = unparsing list * precedence val declare_notation_printing_rule : notation -> unparsing_rule -> unit val find_notation_printing_rule : notation -> unparsing_rule -(**********************************************************************) -(* Rem: printing rules for primitive token are canonical *) +(** Rem: printing rules for primitive token are canonical *) diff --git a/interp/ppextend.ml b/interp/ppextend.ml index 71029f3f..ebf94bd8 100644 --- a/interp/ppextend.ml +++ b/interp/ppextend.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* RefKey(canonical_gr ref), Some (List.length args) + | AList (_,_,AApp (ARef ref,args),_,_) + | ABinderList (_,_,AApp (ARef ref,args),_) -> RefKey (canonical_gr ref), Some (List.length args) + | ARef ref -> RefKey(canonical_gr ref), None + | _ -> Oth, None let cache_reserved_type (_,(id,t)) = - reserve_table := Idmap.add id t !reserve_table + let key = fst (aconstr_key t) in + reserve_table := Idmap.add id t !reserve_table; + reserve_revtable := Gmapl.add key (t,id) !reserve_revtable -let (in_reserved, _) = +let in_reserved : identifier * aconstr -> obj = declare_object {(default_object "RESERVED-TYPE") with cache_function = cache_reserved_type } +let freeze_reserved () = (!reserve_table,!reserve_revtable) +let unfreeze_reserved (r,rr) = reserve_table := r; reserve_revtable := rr +let init_reserved () = + reserve_table := Idmap.empty; reserve_revtable := Gmapl.empty + let _ = Summary.declare_summary "reserved-type" - { Summary.freeze_function = (fun () -> !reserve_table); - Summary.unfreeze_function = (fun r -> reserve_table := r); - Summary.init_function = (fun () -> reserve_table := Idmap.empty) } + { Summary.freeze_function = freeze_reserved; + Summary.unfreeze_function = unfreeze_reserved; + Summary.init_function = init_reserved } -let declare_reserved_type (loc,id) t = +let declare_reserved_type_binding (loc,id) t = if id <> root_of_id id then user_err_loc(loc,"declare_reserved_type", (pr_id id ++ str @@ -45,46 +64,36 @@ let declare_reserved_type (loc,id) t = with Not_found -> () end; add_anonymous_leaf (in_reserved (id,t)) +let declare_reserved_type idl t = + List.iter (fun id -> declare_reserved_type_binding id t) (List.rev idl) + let find_reserved_type id = Idmap.find (root_of_id id) !reserve_table -open Rawterm - -let rec unloc = function - | RVar (_,id) -> RVar (dummy_loc,id) - | RApp (_,g,args) -> RApp (dummy_loc,unloc g, List.map unloc args) - | RLambda (_,na,bk,ty,c) -> RLambda (dummy_loc,na,bk,unloc ty,unloc c) - | RProd (_,na,bk,ty,c) -> RProd (dummy_loc,na,bk,unloc ty,unloc c) - | RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c) - | RCases (_,sty,rtntypopt,tml,pl) -> - RCases (dummy_loc,sty, - (Option.map unloc rtntypopt), - List.map (fun (tm,x) -> (unloc tm,x)) tml, - List.map (fun (_,idl,p,c) -> (dummy_loc,idl,p,unloc c)) pl) - | RLetTuple (_,nal,(na,po),b,c) -> - RLetTuple (dummy_loc,nal,(na,Option.map unloc po),unloc b,unloc c) - | RIf (_,c,(na,po),b1,b2) -> - RIf (dummy_loc,unloc c,(na,Option.map unloc po),unloc b1,unloc b2) - | RRec (_,fk,idl,bl,tyl,bv) -> - RRec (dummy_loc,fk,idl, - Array.map (List.map - (fun (na,k,obd,ty) -> (na,k,Option.map unloc obd, unloc ty))) - bl, - Array.map unloc tyl, - Array.map unloc bv) - | RCast (_,c, CastConv (k,t)) -> RCast (dummy_loc,unloc c, CastConv (k,unloc t)) - | RCast (_,c, CastCoerce) -> RCast (dummy_loc,unloc c, CastCoerce) - | RSort (_,x) -> RSort (dummy_loc,x) - | RHole (_,x) -> RHole (dummy_loc,x) - | RRef (_,x) -> RRef (dummy_loc,x) - | REvar (_,x,l) -> REvar (dummy_loc,x,l) - | RPatVar (_,x) -> RPatVar (dummy_loc,x) - | RDynamic (_,x) -> RDynamic (dummy_loc,x) +let constr_key c = + try RefKey (canonical_gr (global_of_constr (fst (Term.decompose_app c)))) + with Not_found -> Oth + +let revert_reserved_type t = + try + let l = Gmapl.find (constr_key t) !reserve_revtable in + let t = Detyping.detype false [] [] t in + list_try_find + (fun (pat,id) -> + try let _ = match_aconstr false t ([],pat) in Name id + with No_match -> failwith "") l + with Not_found | Failure _ -> Anonymous + +let _ = Namegen.set_reserved_typed_name revert_reserved_type + +open Glob_term let anonymize_if_reserved na t = match na with | Name id as na -> (try - if not !Flags.raw_print & unloc t = find_reserved_type id - then RHole (dummy_loc,Evd.BinderType na) + if not !Flags.raw_print & + (try aconstr_of_glob_constr [] [] t = find_reserved_type id + with UserError _ -> false) + then GHole (dummy_loc,Evd.BinderType na) else t with Not_found -> t) | Anonymous -> t diff --git a/interp/reserve.mli b/interp/reserve.mli index fb60c038..97b22d2b 100644 --- a/interp/reserve.mli +++ b/interp/reserve.mli @@ -1,17 +1,16 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* rawconstr -> unit -val find_reserved_type : identifier -> rawconstr -val anonymize_if_reserved : name -> rawconstr -> rawconstr +val declare_reserved_type : identifier located list -> aconstr -> unit +val find_reserved_type : identifier -> aconstr +val anonymize_if_reserved : name -> glob_constr -> glob_constr diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index 3eb7c248..4e472b7a 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* global_reference -(* Extract a global_reference from a reference that can be an "alias" *) +(** Extract a global_reference from a reference that can be an "alias" *) val global_of_extended_global : extended_global_reference -> global_reference -(* Locate a reference taking into account possible "alias" notations *) +(** Locate a reference taking into account possible "alias" notations *) val global_with_alias : reference -> global_reference -(* The same for inductive types *) +(** The same for inductive types *) val global_inductive_with_alias : reference -> inductive -(* Locate a reference taking into account notations and "aliases" *) +(** Locate a reference taking into account notations and "aliases" *) val smart_global : reference or_by_notation -> global_reference -(* The same for inductive types *) +(** The same for inductive types *) val smart_global_inductive : reference or_by_notation -> inductive diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 44bb02ad..8863bbbd 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* obj = declare_object {(default_object "SYNTAXCONSTANT") with cache_function = cache_syntax_constant; load_function = load_syntax_constant; diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index a3f846bb..e4da52a3 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -1,23 +1,19 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* error "This expression should be a simple identifier." @@ -83,43 +81,43 @@ let rec cases_pattern_fold_map loc g e = function let e',patl' = list_fold_map (cases_pattern_fold_map loc g) e patl in e', PatCstr (loc,cstr,patl',na') -let rec subst_rawvars l = function - | RVar (_,id) as r -> (try List.assoc id l with Not_found -> r) - | RProd (loc,Name id,bk,t,c) -> +let rec subst_glob_vars l = function + | GVar (_,id) as r -> (try List.assoc id l with Not_found -> r) + | GProd (loc,Name id,bk,t,c) -> let id = - try match List.assoc id l with RVar(_,id') -> id' | _ -> id + try match List.assoc id l with GVar(_,id') -> id' | _ -> id with Not_found -> id in - RProd (loc,Name id,bk,subst_rawvars l t,subst_rawvars l c) - | RLambda (loc,Name id,bk,t,c) -> + GProd (loc,Name id,bk,subst_glob_vars l t,subst_glob_vars l c) + | GLambda (loc,Name id,bk,t,c) -> let id = - try match List.assoc id l with RVar(_,id') -> id' | _ -> id + try match List.assoc id l with GVar(_,id') -> id' | _ -> id with Not_found -> id in - RLambda (loc,Name id,bk,subst_rawvars l t,subst_rawvars l c) - | r -> map_rawconstr (subst_rawvars l) r (* assume: id is not binding *) + GLambda (loc,Name id,bk,subst_glob_vars l t,subst_glob_vars l c) + | r -> map_glob_constr (subst_glob_vars l) r (* assume: id is not binding *) let ldots_var = id_of_string ".." -let rawconstr_of_aconstr_with_binders loc g f e = function - | AVar id -> RVar (loc,id) - | AApp (a,args) -> RApp (loc,f e a, List.map (f e) args) +let glob_constr_of_aconstr_with_binders loc g f e = function + | AVar id -> GVar (loc,id) + | AApp (a,args) -> GApp (loc,f e a, List.map (f e) args) | AList (x,y,iter,tail,swap) -> let t = f e tail in let it = f e iter in - let innerl = (ldots_var,t)::(if swap then [] else [x,RVar(loc,y)]) in - let inner = RApp (loc,RVar (loc,ldots_var),[subst_rawvars innerl it]) in - let outerl = (ldots_var,inner)::(if swap then [x,RVar(loc,y)] else []) in - subst_rawvars outerl it + let innerl = (ldots_var,t)::(if swap then [] else [x,GVar(loc,y)]) in + let inner = GApp (loc,GVar (loc,ldots_var),[subst_glob_vars innerl it]) in + let outerl = (ldots_var,inner)::(if swap then [x,GVar(loc,y)] else []) in + subst_glob_vars outerl it | ABinderList (x,y,iter,tail) -> let t = f e tail in let it = f e iter in - let innerl = [(ldots_var,t);(x,RVar(loc,y))] in - let inner = RApp (loc,RVar (loc,ldots_var),[subst_rawvars innerl it]) in + let innerl = [(ldots_var,t);(x,GVar(loc,y))] in + let inner = GApp (loc,GVar (loc,ldots_var),[subst_glob_vars innerl it]) in let outerl = [(ldots_var,inner)] in - subst_rawvars outerl it + subst_glob_vars outerl it | ALambda (na,ty,c) -> - let e',na = g e na in RLambda (loc,na,Explicit,f e ty,f e' c) + let e',na = g e na in GLambda (loc,na,Explicit,f e ty,f e' c) | AProd (na,ty,c) -> - let e',na = g e na in RProd (loc,na,Explicit,f e ty,f e' c) + let e',na = g e na in GProd (loc,na,Explicit,f e ty,f e' c) | ALetIn (na,b,c) -> - let e',na = g e na in RLetIn (loc,na,f e b,f e' c) + let e',na = g e na in GLetIn (loc,na,f e b,f e' c) | ACases (sty,rtntypopt,tml,eqnl) -> let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') -> let e',t' = match t with @@ -135,36 +133,36 @@ let rawconstr_of_aconstr_with_binders loc g f e = function let ((idl,e),patl) = list_fold_map (cases_pattern_fold_map loc fold) ([],e) patl in (loc,idl,patl,f e rhs)) eqnl in - RCases (loc,sty,Option.map (f e') rtntypopt,tml',eqnl') + GCases (loc,sty,Option.map (f e') rtntypopt,tml',eqnl') | ALetTuple (nal,(na,po),b,c) -> let e',nal = list_fold_map g e nal in let e'',na = g e na in - RLetTuple (loc,nal,(na,Option.map (f e'') po),f e b,f e' c) + GLetTuple (loc,nal,(na,Option.map (f e'') po),f e b,f e' c) | AIf (c,(na,po),b1,b2) -> let e',na = g e na in - RIf (loc,f e c,(na,Option.map (f e') po),f e b1,f e b2) + GIf (loc,f e c,(na,Option.map (f e') po),f e b1,f e b2) | ARec (fk,idl,dll,tl,bl) -> let e,dll = array_fold_map (list_fold_map (fun e (na,oc,b) -> let e,na = g e na in (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in let e',idl = array_fold_map (to_id g) e idl in - RRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl) - | ACast (c,k) -> RCast (loc,f e c, + GRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl) + | ACast (c,k) -> GCast (loc,f e c, match k with | CastConv (k,t) -> CastConv (k,f e t) | CastCoerce -> CastCoerce) - | ASort x -> RSort (loc,x) - | AHole x -> RHole (loc,x) - | APatVar n -> RPatVar (loc,(false,n)) - | ARef x -> RRef (loc,x) + | ASort x -> GSort (loc,x) + | AHole x -> GHole (loc,x) + | APatVar n -> GPatVar (loc,(false,n)) + | ARef x -> GRef (loc,x) -let rec rawconstr_of_aconstr loc x = +let rec glob_constr_of_aconstr loc x = let rec aux () x = - rawconstr_of_aconstr_with_binders loc (fun () id -> ((),id)) aux () x + glob_constr_of_aconstr_with_binders loc (fun () id -> ((),id)) aux () x in aux () x (****************************************************************************) -(* Translating a rawconstr into a notation, interpreting recursive patterns *) +(* Translating a glob_constr into a notation, interpreting recursive patterns *) let add_id r id = r := (id :: pi1 !r, pi2 !r, pi3 !r) let add_name r = function Anonymous -> () | Name id -> add_id r id @@ -172,51 +170,51 @@ let add_name r = function Anonymous -> () | Name id -> add_id r id let split_at_recursive_part c = let sub = ref None in let rec aux = function - | RApp (loc0,RVar(loc,v),c::l) when v = ldots_var -> + | GApp (loc0,GVar(loc,v),c::l) when v = ldots_var -> if !sub <> None then (* Not narrowed enough to find only one recursive part *) raise Not_found else (sub := Some c; - if l = [] then RVar (loc,ldots_var) - else RApp (loc0,RVar (loc,ldots_var),l)) - | c -> map_rawconstr aux c in + if l = [] then GVar (loc,ldots_var) + else GApp (loc0,GVar (loc,ldots_var),l)) + | c -> map_glob_constr aux c in let outer_iterator = aux c in match !sub with | None -> (* No recursive pattern found *) raise Not_found | Some c -> match outer_iterator with - | RVar (_,v) when v = ldots_var -> (* Not enough context *) raise Not_found + | GVar (_,v) when v = ldots_var -> (* Not enough context *) raise Not_found | _ -> outer_iterator, c let on_true_do b f c = if b then (f c; b) else b -let compare_rawconstr f add t1 t2 = match t1,t2 with - | RRef (_,r1), RRef (_,r2) -> eq_gr r1 r2 - | RVar (_,v1), RVar (_,v2) -> on_true_do (v1 = v2) add (Name v1) - | RApp (_,f1,l1), RApp (_,f2,l2) -> f f1 f2 & list_for_all2eq f l1 l2 - | RLambda (_,na1,bk1,ty1,c1), RLambda (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 -> on_true_do (f ty1 ty2 & f c1 c2) add na1 - | RProd (_,na1,bk1,ty1,c1), RProd (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 -> +let compare_glob_constr f add t1 t2 = match t1,t2 with + | GRef (_,r1), GRef (_,r2) -> eq_gr r1 r2 + | GVar (_,v1), GVar (_,v2) -> on_true_do (v1 = v2) add (Name v1) + | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 & list_for_all2eq f l1 l2 + | GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 -> on_true_do (f ty1 ty2 & f c1 c2) add na1 + | GProd (_,na1,bk1,ty1,c1), GProd (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 -> on_true_do (f ty1 ty2 & f c1 c2) add na1 - | RHole _, RHole _ -> true - | RSort (_,s1), RSort (_,s2) -> s1 = s2 - | RLetIn (_,na1,b1,c1), RLetIn (_,na2,b2,c2) when na1 = na2 -> + | GHole _, GHole _ -> true + | GSort (_,s1), GSort (_,s2) -> s1 = s2 + | GLetIn (_,na1,b1,c1), GLetIn (_,na2,b2,c2) when na1 = na2 -> on_true_do (f b1 b2 & f c1 c2) add na1 - | (RCases _ | RRec _ | RDynamic _ - | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _),_ - | _,(RCases _ | RRec _ | RDynamic _ - | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _) + | (GCases _ | GRec _ + | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_ + | _,(GCases _ | GRec _ + | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _) -> error "Unsupported construction in recursive notations." - | (RRef _ | RVar _ | RApp _ | RLambda _ | RProd _ - | RHole _ | RSort _ | RLetIn _), _ + | (GRef _ | GVar _ | GApp _ | GLambda _ | GProd _ + | GHole _ | GSort _ | GLetIn _), _ -> false -let rec eq_rawconstr t1 t2 = compare_rawconstr eq_rawconstr (fun _ -> ()) t1 t2 +let rec eq_glob_constr t1 t2 = compare_glob_constr eq_glob_constr (fun _ -> ()) t1 t2 let subtract_loc loc1 loc2 = make_loc (fst (unloc loc1),fst (unloc loc2)-1) -let check_is_hole id = function RHole _ -> () | t -> - user_err_loc (loc_of_rawconstr t,"", +let check_is_hole id = function GHole _ -> () | t -> + user_err_loc (loc_of_glob_constr t,"", strbrk "In recursive notation with binders, " ++ pr_id id ++ strbrk " is expected to come without type.") @@ -224,40 +222,40 @@ let compare_recursive_parts found f (iterator,subc) = let diff = ref None in let terminator = ref None in let rec aux c1 c2 = match c1,c2 with - | RVar(_,v), term when v = ldots_var -> + | GVar(_,v), term when v = ldots_var -> (* We found the pattern *) assert (!terminator = None); terminator := Some term; true - | RApp (_,RVar(_,v),l1), RApp (_,term,l2) when v = ldots_var -> + | GApp (_,GVar(_,v),l1), GApp (_,term,l2) when v = ldots_var -> (* We found the pattern, but there are extra arguments *) (* (this allows e.g. alternative (recursive) notation of application) *) assert (!terminator = None); terminator := Some term; list_for_all2eq aux l1 l2 - | RVar (_,x), RVar (_,y) when x<>y -> + | GVar (_,x), GVar (_,y) when x<>y -> (* We found the position where it differs *) let lassoc = (!terminator <> None) in let x,y = if lassoc then y,x else x,y in !diff = None && (diff := Some (x,y,Some lassoc); true) - | RLambda (_,Name x,_,t_x,c), RLambda (_,Name y,_,t_y,term) - | RProd (_,Name x,_,t_x,c), RProd (_,Name y,_,t_y,term) -> + | GLambda (_,Name x,_,t_x,c), GLambda (_,Name y,_,t_y,term) + | GProd (_,Name x,_,t_x,c), GProd (_,Name y,_,t_y,term) -> (* We found a binding position where it differs *) check_is_hole y t_x; check_is_hole y t_y; !diff = None && (diff := Some (x,y,None); aux c term) | _ -> - compare_rawconstr aux (add_name found) c1 c2 in + compare_glob_constr aux (add_name found) c1 c2 in if aux iterator subc then match !diff with | None -> - let loc1 = loc_of_rawconstr iterator in - let loc2 = loc_of_rawconstr (Option.get !terminator) in + let loc1 = loc_of_glob_constr iterator in + let loc2 = loc_of_glob_constr (Option.get !terminator) in (* Here, we would need a loc made of several parts ... *) user_err_loc (subtract_loc loc1 loc2,"", str "Both ends of the recursive pattern are the same.") | Some (x,y,Some lassoc) -> let newfound = (pi1 !found, (x,y) :: pi2 !found, pi3 !found) in let iterator = - f (if lassoc then subst_rawvars [y,RVar(dummy_loc,x)] iterator + f (if lassoc then subst_glob_vars [y,GVar(dummy_loc,x)] iterator else iterator) in (* found have been collected by compare_constr *) found := newfound; @@ -271,7 +269,7 @@ let compare_recursive_parts found f (iterator,subc) = else raise Not_found -let aconstr_and_vars_of_rawconstr a = +let aconstr_and_vars_of_glob_constr a = let found = ref ([],[],[]) in let rec aux c = let keepfound = !found in @@ -280,7 +278,7 @@ let aconstr_and_vars_of_rawconstr a = with Not_found -> found := keepfound; match c with - | RApp (_,RVar (loc,f),[c]) when f = ldots_var -> + | GApp (_,GVar (loc,f),[c]) when f = ldots_var -> (* Fall on the second part of the recursive pattern w/o having found the first part *) user_err_loc (loc,"", @@ -288,12 +286,12 @@ let aconstr_and_vars_of_rawconstr a = | c -> aux' c and aux' = function - | RVar (_,id) -> add_id found id; AVar id - | RApp (_,g,args) -> AApp (aux g, List.map aux args) - | RLambda (_,na,bk,ty,c) -> add_name found na; ALambda (na,aux ty,aux c) - | RProd (_,na,bk,ty,c) -> add_name found na; AProd (na,aux ty,aux c) - | RLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c) - | RCases (_,sty,rtntypopt,tml,eqnl) -> + | GVar (_,id) -> add_id found id; AVar id + | GApp (_,g,args) -> AApp (aux g, List.map aux args) + | GLambda (_,na,bk,ty,c) -> add_name found na; ALambda (na,aux ty,aux c) + | GProd (_,na,bk,ty,c) -> add_name found na; AProd (na,aux ty,aux c) + | GLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c) + | GCases (_,sty,rtntypopt,tml,eqnl) -> let f (_,idl,pat,rhs) = List.iter (add_id found) idl; (pat,aux rhs) in ACases (sty,Option.map aux rtntypopt, List.map (fun (tm,(na,x)) -> @@ -302,28 +300,28 @@ let aconstr_and_vars_of_rawconstr a = (fun (_,_,_,nl) -> List.iter (add_name found) nl) x; (aux tm,(na,Option.map (fun (_,ind,n,nal) -> (ind,n,nal)) x))) tml, List.map f eqnl) - | RLetTuple (loc,nal,(na,po),b,c) -> + | GLetTuple (loc,nal,(na,po),b,c) -> add_name found na; List.iter (add_name found) nal; ALetTuple (nal,(na,Option.map aux po),aux b,aux c) - | RIf (loc,c,(na,po),b1,b2) -> + | GIf (loc,c,(na,po),b1,b2) -> add_name found na; AIf (aux c,(na,Option.map aux po),aux b1,aux b2) - | RRec (_,fk,idl,dll,tl,bl) -> + | GRec (_,fk,idl,dll,tl,bl) -> Array.iter (add_id found) idl; let dll = Array.map (List.map (fun (na,bk,oc,b) -> if bk <> Explicit then error "Binders marked as implicit not allowed in notations."; add_name found na; (na,Option.map aux oc,aux b))) dll in ARec (fk,idl,dll,Array.map aux tl,Array.map aux bl) - | RCast (_,c,k) -> ACast (aux c, + | GCast (_,c,k) -> ACast (aux c, match k with CastConv (k,t) -> CastConv (k,aux t) | CastCoerce -> CastCoerce) - | RSort (_,s) -> ASort s - | RHole (_,w) -> AHole w - | RRef (_,r) -> ARef r - | RPatVar (_,(_,n)) -> APatVar n - | RDynamic _ | REvar _ -> + | GSort (_,s) -> ASort s + | GHole (_,w) -> AHole w + | GRef (_,r) -> ARef r + | GPatVar (_,(_,n)) -> APatVar n + | GEvar _ -> error "Existential variables not allowed in notations." in @@ -372,15 +370,15 @@ let check_variables vars recvars (found,foundrec,foundrecbinding) = | NtnInternTypeIdent -> check_bound x in List.iter check_type vars -let aconstr_of_rawconstr vars recvars a = - let a,found = aconstr_and_vars_of_rawconstr a in +let aconstr_of_glob_constr vars recvars a = + let a,found = aconstr_and_vars_of_glob_constr a in check_variables vars recvars found; a (* Substitution of kernel names, avoiding a list of bound identifiers *) let aconstr_of_constr avoiding t = - aconstr_of_rawconstr [] [] (Detyping.detype false avoiding [] t) + aconstr_of_glob_constr [] [] (Detyping.detype false avoiding [] t) let rec subst_pat subst pat = match pat with @@ -510,9 +508,7 @@ let subst_interpretation subst (metas,pat) = let bound = List.map fst metas in (metas,subst_aconstr subst bound pat) -let encode_list_value l = RApp (dummy_loc,RVar (dummy_loc,ldots_var),l) - -(* Pattern-matching rawconstr and aconstr *) +(* Pattern-matching glob_constr and aconstr *) let abstract_return_type_context pi mklam tml rtno = Option.map (fun rtn -> @@ -522,19 +518,14 @@ let abstract_return_type_context pi mklam tml rtno = List.fold_right mklam nal rtn) rtno -let abstract_return_type_context_rawconstr = +let abstract_return_type_context_glob_constr = abstract_return_type_context (fun (_,_,_,nal) -> nal) - (fun na c -> RLambda(dummy_loc,na,Explicit,RHole(dummy_loc,Evd.InternalHole),c)) + (fun na c -> GLambda(dummy_loc,na,Explicit,GHole(dummy_loc,Evd.InternalHole),c)) let abstract_return_type_context_aconstr = abstract_return_type_context pi3 (fun na c -> ALambda(na,AHole Evd.InternalHole,c)) -let rec adjust_scopes = function - | _,[] -> [] - | [],a::args -> (None,a) :: adjust_scopes ([],args) - | sc::scopes,a::args -> (sc,a) :: adjust_scopes (scopes,args) - exception No_match let rec alpha_var id1 id2 = function @@ -552,7 +543,7 @@ let bind_env alp (sigma,sigmalist,sigmabinders as fullsigma) var v = else raise No_match with Not_found -> (* Check that no capture of binding variables occur *) - if List.exists (fun (id,_) ->occur_rawconstr id v) alp then raise No_match; + if List.exists (fun (id,_) ->occur_glob_constr id v) alp then raise No_match; (* TODO: handle the case of multiple occs in different scopes *) ((var,v)::sigma,sigmalist,sigmabinders) @@ -561,8 +552,8 @@ let bind_binder (sigma,sigmalist,sigmabinders) x bl = let match_fix_kind fk1 fk2 = match (fk1,fk2) with - | RCoFix n1, RCoFix n2 -> n1 = n2 - | RFix (nl1,n1), RFix (nl2,n2) -> + | GCoFix n1, GCoFix n2 -> n1 = n2 + | GFix (nl1,n1), GFix (nl2,n2) -> n1 = n2 && array_for_all2 (fun (n1,_) (n2,_) -> n2 = None || n1 = n2) nl1 nl2 | _ -> false @@ -574,7 +565,7 @@ let match_opt f sigma t1 t2 = match (t1,t2) with let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with | (Name id1,Name id2) when List.mem id2 (fst metas) -> - alp, bind_env alp sigma id2 (RVar (dummy_loc,id1)) + alp, bind_env alp sigma id2 (GVar (dummy_loc,id1)) | (Name id1,Name id2) -> (id1,id2)::alp,sigma | (Anonymous,Anonymous) -> alp,sigma | _ -> raise No_match @@ -588,20 +579,16 @@ let rec match_cases_pattern_binders metas acc pat1 pat2 = (match_names metas acc na1 na2) patl1 patl2 | _ -> raise No_match -let adjust_application_n n loc f l = - let l1,l2 = list_chop (List.length l - n) l in - if l1 = [] then f,l else RApp (loc,f,l1), l2 - let glue_letin_with_decls = true let rec match_iterated_binders islambda decls = function - | RLambda (_,na,bk,t,b) when islambda -> + | GLambda (_,na,bk,t,b) when islambda -> match_iterated_binders islambda ((na,bk,None,t)::decls) b - | RProd (_,(Name _ as na),bk,t,b) when not islambda -> + | GProd (_,(Name _ as na),bk,t,b) when not islambda -> match_iterated_binders islambda ((na,bk,None,t)::decls) b - | RLetIn (loc,na,c,b) when glue_letin_with_decls -> + | GLetIn (loc,na,c,b) when glue_letin_with_decls -> match_iterated_binders islambda - ((na,Explicit (*?*), Some c,RHole(loc,Evd.BinderType na))::decls) b + ((na,Explicit (*?*), Some c,GHole(loc,Evd.BinderType na))::decls) b | b -> (decls,b) let remove_sigma x (sigmavar,sigmalist,sigmabinders) = @@ -633,125 +620,157 @@ let match_alist match_fun metas sigma rest x iter termin lassoc = let l,sigma = aux sigma [] rest in (pi1 sigma, (x,if lassoc then l else List.rev l)::pi2 sigma, pi3 sigma) -let rec match_ alp (tmetas,blmetas as metas) sigma a1 a2 = match (a1,a2) with +let does_not_come_from_already_eta_expanded_var = + (* This is hack to avoid looping on a rule with rhs of the form *) + (* "?f (fun ?x => ?g)" since otherwise, matching "F H" expands in *) + (* "F (fun x => H x)" and "H x" is recursively matched against the same *) + (* rule, giving "H (fun x' => x x')" and so on. *) + (* Ideally, we would need the type of the expression to know which of *) + (* the arguments applied to it can be eta-expanded without looping. *) + (* The following test is then an approximation of what can be done *) + (* optimally (whether other looping situations can occur remains to be *) + (* checked). *) + function GVar _ -> false | _ -> true + +let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 = + match (a1,a2) with (* Matching notation variable *) | r1, AVar id2 when List.mem id2 tmetas -> bind_env alp sigma id2 r1 (* Matching recursive notations for terms *) | r1, AList (x,_,iter,termin,lassoc) -> - match_alist (match_ alp) metas sigma r1 x iter termin lassoc + match_alist (match_hd u alp) metas sigma r1 x iter termin lassoc (* Matching recursive notations for binders: ad hoc cases supporting let-in *) - | RLambda (_,na1,bk,t1,b1), ABinderList (x,_,ALambda (Name id2,_,b2),termin)-> + | GLambda (_,na1,bk,t1,b1), ABinderList (x,_,ALambda (Name id2,_,b2),termin)-> let (decls,b) = match_iterated_binders true [(na1,bk,None,t1)] b1 in (* TODO: address the possibility that termin is a Lambda itself *) - match_ alp metas (bind_binder sigma x decls) b termin - | RProd (_,na1,bk,t1,b1), ABinderList (x,_,AProd (Name id2,_,b2),termin) + match_in u alp metas (bind_binder sigma x decls) b termin + | GProd (_,na1,bk,t1,b1), ABinderList (x,_,AProd (Name id2,_,b2),termin) when na1 <> Anonymous -> let (decls,b) = match_iterated_binders false [(na1,bk,None,t1)] b1 in (* TODO: address the possibility that termin is a Prod itself *) - match_ alp metas (bind_binder sigma x decls) b termin + match_in u alp metas (bind_binder sigma x decls) b termin (* Matching recursive notations for binders: general case *) | r, ABinderList (x,_,iter,termin) -> - match_abinderlist_with_app (match_ alp) metas sigma r x iter termin + match_abinderlist_with_app (match_hd u alp) metas sigma r x iter termin (* Matching individual binders as part of a recursive pattern *) - | RLambda (_,na,bk,t,b1), ALambda (Name id,_,b2) when List.mem id blmetas -> - match_ alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2 - | RProd (_,na,bk,t,b1), AProd (Name id,_,b2) + | GLambda (_,na,bk,t,b1), ALambda (Name id,_,b2) when List.mem id blmetas -> + match_in u alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2 + | GProd (_,na,bk,t,b1), AProd (Name id,_,b2) when List.mem id blmetas & na <> Anonymous -> - match_ alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2 + match_in u alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2 (* Matching compositionally *) - | RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma - | RRef (_,r1), ARef r2 when (eq_gr r1 r2) -> sigma - | RPatVar (_,(_,n1)), APatVar n2 when n1=n2 -> sigma - | RApp (loc,f1,l1), AApp (f2,l2) -> + | GVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma + | GRef (_,r1), ARef r2 when (eq_gr r1 r2) -> sigma + | GPatVar (_,(_,n1)), APatVar n2 when n1=n2 -> sigma + | GApp (loc,f1,l1), AApp (f2,l2) -> let n1 = List.length l1 and n2 = List.length l2 in let f1,l1,f2,l2 = if n1 < n2 then let l21,l22 = list_chop (n2-n1) l2 in f1,l1, AApp (f2,l21), l22 else if n1 > n2 then - let l11,l12 = list_chop (n1-n2) l1 in RApp (loc,f1,l11),l12, f2,l2 + let l11,l12 = list_chop (n1-n2) l1 in GApp (loc,f1,l11),l12, f2,l2 else f1,l1, f2, l2 in - List.fold_left2 (match_ alp metas) (match_ alp metas sigma f1 f2) l1 l2 - | RLambda (_,na1,_,t1,b1), ALambda (na2,t2,b2) -> - match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2 - | RProd (_,na1,_,t1,b1), AProd (na2,t2,b2) -> - match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2 - | RLetIn (_,na1,t1,b1), ALetIn (na2,t2,b2) -> - match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2 - | RCases (_,sty1,rtno1,tml1,eqnl1), ACases (sty2,rtno2,tml2,eqnl2) + let may_use_eta = does_not_come_from_already_eta_expanded_var f1 in + List.fold_left2 (match_ may_use_eta u alp metas) + (match_in u alp metas sigma f1 f2) l1 l2 + | GLambda (_,na1,_,t1,b1), ALambda (na2,t2,b2) -> + match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 + | GProd (_,na1,_,t1,b1), AProd (na2,t2,b2) -> + match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 + | GLetIn (_,na1,t1,b1), ALetIn (na2,t2,b2) -> + match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 + | GCases (_,sty1,rtno1,tml1,eqnl1), ACases (sty2,rtno2,tml2,eqnl2) when sty1 = sty2 & List.length tml1 = List.length tml2 & List.length eqnl1 = List.length eqnl2 -> - let rtno1' = abstract_return_type_context_rawconstr tml1 rtno1 in + let rtno1' = abstract_return_type_context_glob_constr tml1 rtno1 in let rtno2' = abstract_return_type_context_aconstr tml2 rtno2 in let sigma = - try Option.fold_left2 (match_ alp metas) sigma rtno1' rtno2' + try Option.fold_left2 (match_in u alp metas) sigma rtno1' rtno2' with Option.Heterogeneous -> raise No_match in let sigma = List.fold_left2 - (fun s (tm1,_) (tm2,_) -> match_ alp metas s tm1 tm2) sigma tml1 tml2 in - List.fold_left2 (match_equations alp metas) sigma eqnl1 eqnl2 - | RLetTuple (_,nal1,(na1,to1),b1,c1), ALetTuple (nal2,(na2,to2),b2,c2) + (fun s (tm1,_) (tm2,_) -> + match_in u alp metas s tm1 tm2) sigma tml1 tml2 in + List.fold_left2 (match_equations u alp metas) sigma eqnl1 eqnl2 + | GLetTuple (_,nal1,(na1,to1),b1,c1), ALetTuple (nal2,(na2,to2),b2,c2) when List.length nal1 = List.length nal2 -> - let sigma = match_opt (match_binders alp metas na1 na2) sigma to1 to2 in - let sigma = match_ alp metas sigma b1 b2 in + let sigma = match_opt (match_binders u alp metas na1 na2) sigma to1 to2 in + let sigma = match_in u alp metas sigma b1 b2 in let (alp,sigma) = List.fold_left2 (match_names metas) (alp,sigma) nal1 nal2 in - match_ alp metas sigma c1 c2 - | RIf (_,a1,(na1,to1),b1,c1), AIf (a2,(na2,to2),b2,c2) -> - let sigma = match_opt (match_binders alp metas na1 na2) sigma to1 to2 in - List.fold_left2 (match_ alp metas) sigma [a1;b1;c1] [a2;b2;c2] - | RRec (_,fk1,idl1,dll1,tl1,bl1), ARec (fk2,idl2,dll2,tl2,bl2) + match_in u alp metas sigma c1 c2 + | GIf (_,a1,(na1,to1),b1,c1), AIf (a2,(na2,to2),b2,c2) -> + let sigma = match_opt (match_binders u alp metas na1 na2) sigma to1 to2 in + List.fold_left2 (match_in u alp metas) sigma [a1;b1;c1] [a2;b2;c2] + | GRec (_,fk1,idl1,dll1,tl1,bl1), ARec (fk2,idl2,dll2,tl2,bl2) when match_fix_kind fk1 fk2 & Array.length idl1 = Array.length idl2 & array_for_all2 (fun l1 l2 -> List.length l1 = List.length l2) dll1 dll2 -> let alp,sigma = array_fold_left2 (List.fold_left2 (fun (alp,sigma) (na1,_,oc1,b1) (na2,oc2,b2) -> let sigma = - match_ alp metas (match_opt (match_ alp metas) sigma oc1 oc2) b1 b2 + match_in u alp metas + (match_opt (match_in u alp metas) sigma oc1 oc2) b1 b2 in match_names metas (alp,sigma) na1 na2)) (alp,sigma) dll1 dll2 in - let sigma = array_fold_left2 (match_ alp metas) sigma tl1 tl2 in + let sigma = array_fold_left2 (match_in u alp metas) sigma tl1 tl2 in let alp,sigma = array_fold_right2 (fun id1 id2 alsig -> match_names metas alsig (Name id1) (Name id2)) idl1 idl2 (alp,sigma) in - array_fold_left2 (match_ alp metas) sigma bl1 bl2 - | RCast(_,c1, CastConv(_,t1)), ACast(c2, CastConv (_,t2)) -> - match_ alp metas (match_ alp metas sigma c1 c2) t1 t2 - | RCast(_,c1, CastCoerce), ACast(c2, CastCoerce) -> - match_ alp metas sigma c1 c2 - | RSort (_,RType _), ASort (RType None) -> sigma - | RSort (_,s1), ASort s2 when s1 = s2 -> sigma - | RPatVar _, AHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match + array_fold_left2 (match_in u alp metas) sigma bl1 bl2 + | GCast(_,c1, CastConv(_,t1)), ACast(c2, CastConv (_,t2)) -> + match_in u alp metas (match_in u alp metas sigma c1 c2) t1 t2 + | GCast(_,c1, CastCoerce), ACast(c2, CastCoerce) -> + match_in u alp metas sigma c1 c2 + | GSort (_,GType _), ASort (GType None) when not u -> sigma + | GSort (_,s1), ASort s2 when s1 = s2 -> sigma + | GPatVar _, AHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match | a, AHole _ -> sigma - | (RDynamic _ | RRec _ | REvar _), _ + + (* On the fly eta-expansion so as to use notations of the form + "exists x, P x" for "ex P"; expects type not given because don't know + otherwise how to ensure it corresponds to a well-typed eta-expansion; + ensure at least one constructor is consumed to avoid looping *) + | b1, ALambda (Name id,AHole _,b2) when inner -> + let id' = Namegen.next_ident_away id (free_glob_vars b1) in + match_in u alp metas (bind_binder sigma id + [(Name id',Explicit,None,GHole(dummy_loc,Evd.BinderType (Name id')))]) + (mkGApp dummy_loc b1 (GVar (dummy_loc,id'))) b2 + + | (GRec _ | GEvar _), _ | _,_ -> raise No_match -and match_binders alp metas na1 na2 sigma b1 b2 = +and match_in u = match_ true u + +and match_hd u = match_ false u + +and match_binders u alp metas na1 na2 sigma b1 b2 = let (alp,sigma) = match_names metas (alp,sigma) na1 na2 in - match_ alp metas sigma b1 b2 + match_in u alp metas sigma b1 b2 -and match_equations alp metas sigma (_,_,patl1,rhs1) (patl2,rhs2) = +and match_equations u alp metas sigma (_,_,patl1,rhs1) (patl2,rhs2) = (* patl1 and patl2 have the same length because they respectively correspond to some tml1 and tml2 that have the same length *) let (alp,sigma) = List.fold_left2 (match_cases_pattern_binders metas) (alp,sigma) patl1 patl2 in - match_ alp metas sigma rhs1 rhs2 + match_in u alp metas sigma rhs1 rhs2 -let match_aconstr c (metas,pat) = +let match_aconstr u c (metas,pat) = let vars = list_split_by (fun (_,(_,x)) -> x <> NtnTypeBinderList) metas in let vars = (List.map fst (fst vars), List.map fst (snd vars)) in - let terms,termlists,binders = match_ [] vars ([],[],[]) c pat in + let terms,termlists,binders = match_ false u [] vars ([],[],[]) c pat in (* Reorder canonically the substitution *) let find x = try List.assoc x terms with Not_found -> (* Happens for binders bound to Anonymous *) (* Find a better way to propagate Anonymous... *) - RVar (dummy_loc,x) in + GVar (dummy_loc,x) in List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders') -> match typ with | NtnTypeConstr -> @@ -824,6 +843,7 @@ type prim_token = Numeral of Bigint.bigint | String of string type cases_pattern_expr = | CPatAlias of loc * cases_pattern_expr * identifier | CPatCstr of loc * reference * cases_pattern_expr list + | CPatCstrExpl of loc * reference * cases_pattern_expr list | CPatAtom of loc * reference option | CPatOr of loc * cases_pattern_expr list | CPatNotation of loc * notation * cases_pattern_notation_substitution @@ -857,13 +877,12 @@ type constr_expr = | CHole of loc * Evd.hole_kind option | CPatVar of loc * (bool * patvar) | CEvar of loc * existential_key * constr_expr list option - | CSort of loc * rawsort + | CSort of loc * glob_sort | CCast of loc * constr_expr * constr_expr cast_type | CNotation of loc * notation * constr_notation_substitution | CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr | CPrim of loc * prim_token | CDelimiters of loc * string * constr_expr - | CDynamic of loc * Dyn.t and fix_expr = identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr @@ -929,11 +948,11 @@ let constr_loc = function | CGeneralization (loc,_,_,_) -> loc | CPrim (loc,_) -> loc | CDelimiters (loc,_,_) -> loc - | CDynamic _ -> dummy_loc let cases_pattern_expr_loc = function | CPatAlias (loc,_,_) -> loc | CPatCstr (loc,_,_) -> loc + | CPatCstrExpl (loc,_,_) -> loc | CPatAtom (loc,_) -> loc | CPatOr (loc,_) -> loc | CPatNotation (loc,_,_) -> loc @@ -950,10 +969,6 @@ let local_binders_loc bll = if bll = [] then dummy_loc else join_loc (local_binder_loc (List.hd bll)) (local_binder_loc (list_last bll)) -let occur_var_constr_ref id = function - | Ident (loc,id') -> id = id' - | Qualid _ -> false - let ids_of_cases_indtype = let add_var ids = function CRef (Ident (_,id)) -> id::ids | _ -> ids in let rec vars_of = function @@ -981,7 +996,7 @@ let rec cases_pattern_fold_names f a = function | CPatRecord (_, l) -> List.fold_left (fun acc (r, cp) -> cases_pattern_fold_names f acc cp) a l | CPatAlias (_,pat,id) -> f id a - | CPatCstr (_,_,patl) | CPatOr (_,patl) -> + | CPatCstr (_,_,patl) | CPatCstrExpl (_,_,patl) | CPatOr (_,patl) -> List.fold_left (cases_pattern_fold_names f) a patl | CPatNotation (_,_,(patl,patll)) -> List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll) @@ -1028,7 +1043,7 @@ let fold_constr_expr_with_binders g f n acc = function List.fold_left (fun acc bl -> fold_local_binders g f n acc (CHole (dummy_loc,None)) bl) acc bll | CGeneralization (_,_,_,c) -> f n acc c | CDelimiters (loc,_,a) -> f n acc a - | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _ | CRef _ -> + | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CRef _ -> acc | CRecord (loc,_,l) -> List.fold_left (fun acc (id, c) -> f n acc c) acc l | CCases (loc,sty,rtnpo,al,bl) -> @@ -1137,9 +1152,9 @@ let split_at_annot bl na = let rec aux acc = function | LocalRawAssum (bls, k, t) as x :: rest -> let l, r = list_split_when (fun (loc, na) -> na = Name id) bls in - if r = [] then aux (x :: acc) rest - else - (List.rev (if l = [] then acc else LocalRawAssum (l, k, t) :: acc), + if r = [] then aux (x :: acc) rest + else + (List.rev (if l = [] then acc else LocalRawAssum (l, k, t) :: acc), LocalRawAssum (r, k, t) :: rest) | LocalRawDef _ as x :: rest -> aux (x :: acc) rest | [] -> @@ -1186,7 +1201,7 @@ let map_constr_expr_with_binders g f e = function | CGeneralization (loc,b,a,c) -> CGeneralization (loc,b,a,f e c) | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a) | CHole _ | CEvar _ | CPatVar _ | CSort _ - | CPrim _ | CDynamic _ | CRef _ as x -> x + | CPrim _ | CRef _ as x -> x | CRecord (loc,p,l) -> CRecord (loc,p,List.map (fun (id, c) -> (id, f e c)) l) | CCases (loc,sty,rtnpo,a,bl) -> (* TODO: apply g on the binding variables in pat... *) @@ -1233,14 +1248,8 @@ type with_declaration_ast = type module_ast = | CMident of qualid located - | CMapply of module_ast * module_ast - | CMwith of module_ast * with_declaration_ast - -type module_ast_inl = module_ast * bool (* honor the inline annotations or not *) - -type 'a module_signature = - | Enforce of 'a (* ... : T *) - | Check of 'a list (* ... <: T1 <: T2, possibly empty *) + | CMapply of loc * module_ast * module_ast + | CMwith of loc * module_ast * with_declaration_ast (* Returns the ranges of locs of the notation that are not occupied by args *) (* and which are then occupied by proper symbols of the notation (or spaces) *) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index ce9de27b..4527dc48 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -1,35 +1,34 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* - (identifier * identifier) list -> rawconstr -> aconstr + (identifier * identifier) list -> glob_constr -> aconstr -(* Name of the special identifier used to encode recursive notations *) +(** Name of the special identifier used to encode recursive notations *) val ldots_var : identifier -(* Equality of rawconstr (warning: only partially implemented) *) -val eq_rawconstr : rawconstr -> rawconstr -> bool +(** Equality of glob_constr (warning: only partially implemented) *) +val eq_glob_constr : glob_constr -> glob_constr -> bool -(**********************************************************************) -(* Re-interpret a notation as a rawconstr, taking care of binders *) +(** Re-interpret a notation as a glob_constr, taking care of binders *) -val rawconstr_of_aconstr_with_binders : loc -> +val glob_constr_of_aconstr_with_binders : loc -> ('a -> name -> 'a * name) -> - ('a -> aconstr -> rawconstr) -> 'a -> aconstr -> rawconstr + ('a -> aconstr -> glob_constr) -> 'a -> aconstr -> glob_constr -val rawconstr_of_aconstr : loc -> aconstr -> rawconstr +val glob_constr_of_aconstr : loc -> aconstr -> glob_constr -(**********************************************************************) -(* [match_aconstr] matches a rawconstr against a notation *) -(* interpretation raise [No_match] if the matching fails *) +(** [match_aconstr] matches a glob_constr against a notation interpretation; + raise [No_match] if the matching fails *) exception No_match -val match_aconstr : rawconstr -> interpretation -> - (rawconstr * subscopes) list * (rawconstr list * subscopes) list * - (rawdecl list * subscopes) list +val match_aconstr : bool -> glob_constr -> interpretation -> + (glob_constr * subscopes) list * (glob_constr list * subscopes) list * + (glob_decl list * subscopes) list val match_aconstr_cases_pattern : cases_pattern -> interpretation -> (cases_pattern * subscopes) list * (cases_pattern list * subscopes) list -(**********************************************************************) -(* Substitution of kernel names in interpretation data *) +(** Substitution of kernel names in interpretation data *) val subst_interpretation : substitution -> interpretation -> interpretation -(**********************************************************************) -(*s Concrete syntax for terms *) +(** {6 Concrete syntax for terms } *) type notation = string @@ -119,18 +113,19 @@ type explicitation = ExplByPos of int * identifier option | ExplByName of identi type binder_kind = | Default of binding_kind | Generalized of binding_kind * binding_kind * bool - (* Inner binding, outer bindings, typeclass-specific flag + (** Inner binding, outer bindings, typeclass-specific flag for implicit generalization of superclasses *) type abstraction_kind = AbsLambda | AbsPi -type proj_flag = int option (* [Some n] = proj of the n-th visible argument *) +type proj_flag = int option (** [Some n] = proj of the n-th visible argument *) type prim_token = Numeral of Bigint.bigint | String of string type cases_pattern_expr = | CPatAlias of loc * cases_pattern_expr * identifier | CPatCstr of loc * reference * cases_pattern_expr list + | CPatCstrExpl of loc * reference * cases_pattern_expr list | CPatAtom of loc * reference option | CPatOr of loc * cases_pattern_expr list | CPatNotation of loc * notation * cases_pattern_notation_substitution @@ -164,13 +159,12 @@ type constr_expr = | CHole of loc * Evd.hole_kind option | CPatVar of loc * (bool * patvar) | CEvar of loc * existential_key * constr_expr list option - | CSort of loc * rawsort + | CSort of loc * glob_sort | CCast of loc * constr_expr * constr_expr cast_type | CNotation of loc * notation * constr_notation_substitution | CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr | CPrim of loc * prim_token | CDelimiters of loc * string * constr_expr - | CDynamic of loc * Dyn.t and fix_expr = identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr @@ -181,7 +175,7 @@ and cofix_expr = and recursion_order_expr = | CStructRec | CWfRec of constr_expr - | CMeasureRec of constr_expr * constr_expr option (* measure, relation *) + | CMeasureRec of constr_expr * constr_expr option (** measure, relation *) (** Anonymous defs allowed ?? *) and local_binder = @@ -199,8 +193,7 @@ and typeclass_context = typeclass_constraint list type constr_pattern_expr = constr_expr -(**********************************************************************) -(* Utilities on constr_expr *) +(** Utilities on constr_expr *) val constr_loc : constr_expr -> loc @@ -216,7 +209,7 @@ val occur_var_constr_expr : identifier -> constr_expr -> bool val default_binder_kind : binder_kind -(* Specific function for interning "in indtype" syntax of "match" *) +(** Specific function for interning "in indtype" syntax of "match" *) val ids_of_cases_indtype : constr_expr -> identifier list val mkIdentC : identifier -> constr_expr @@ -236,32 +229,31 @@ val split_at_annot : local_binder list -> identifier located option -> local_bin val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr val prod_constr_expr : constr_expr -> local_binder list -> constr_expr -(* Same as [abstract_constr_expr] and [prod_constr_expr], with location *) +(** Same as [abstract_constr_expr] and [prod_constr_expr], with location *) val mkCLambdaN : loc -> local_binder list -> constr_expr -> constr_expr val mkCProdN : loc -> local_binder list -> constr_expr -> constr_expr -(* For binders parsing *) +(** For binders parsing *) -(* With let binders *) +(** With let binders *) val names_of_local_binders : local_binder list -> name located list -(* Does not take let binders into account *) +(** Does not take let binders into account *) val names_of_local_assums : local_binder list -> name located list -(* Used in typeclasses *) +(** Used in typeclasses *) val fold_constr_expr_with_binders : (identifier -> 'a -> 'a) -> ('a -> 'b -> constr_expr -> 'b) -> 'a -> 'b -> constr_expr -> 'b -(* Used in correctness and interface; absence of var capture not guaranteed *) -(* in pattern-matching clauses and in binders of the form [x,y:T(x)] *) +(** Used in correctness and interface; absence of var capture not guaranteed + in pattern-matching clauses and in binders of the form [x,y:T(x)] *) val map_constr_expr_with_binders : (identifier -> 'a -> 'a) -> ('a -> constr_expr -> constr_expr) -> 'a -> constr_expr -> constr_expr -(**********************************************************************) -(* Concrete syntax for modules and module types *) +(** Concrete syntax for modules and module types *) type with_declaration_ast = | CWith_Module of identifier list located * qualid located @@ -269,14 +261,8 @@ type with_declaration_ast = type module_ast = | CMident of qualid located - | CMapply of module_ast * module_ast - | CMwith of module_ast * with_declaration_ast - -type module_ast_inl = module_ast * bool (* honor the inline annotations or not *) - -type 'a module_signature = - | Enforce of 'a (* ... : T *) - | Check of 'a list (* ... <: T1 <: T2, possibly empty *) + | CMapply of loc * module_ast * module_ast + | CMwith of loc * module_ast * with_declaration_ast val ntn_loc : Util.loc -> constr_notation_substitution -> string -> (int * int) list -- cgit v1.2.3