summaryrefslogtreecommitdiff
path: root/interp/constrextern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrextern.ml')
-rw-r--r--interp/constrextern.ml383
1 files changed, 174 insertions, 209 deletions
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 *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: constrextern.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
(*i*)
open Pp
open Util
@@ -23,7 +21,7 @@ open Environ
open Libnames
open Impargs
open Topconstr
-open Rawterm
+open Glob_term
open Pattern
open Nametab
open Notation
@@ -31,7 +29,7 @@ open Reserve
open Detyping
(*i*)
-(* Translation from rawconstr to front constr *)
+(* Translation from glob_constr to front constr *)
(**********************************************************************)
(* Parametrization *)
@@ -76,6 +74,49 @@ let without_symbols f = Flags.with_option print_no_symbol f
let with_meta_as_hole f = Flags.with_option print_meta_as_hole f
(**********************************************************************)
+(* Control printing of records *)
+
+let is_record indsp =
+ try
+ let _ = Recordops.lookup_structure indsp in
+ true
+ with Not_found -> 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 *)
let insert_delimiters e = function
@@ -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