aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/interface/ascent.mli5
-rw-r--r--contrib/interface/vtp.ml7
-rw-r--r--contrib/interface/xlate.ml64
-rw-r--r--interp/constrextern.ml54
-rw-r--r--interp/constrintern.ml67
-rw-r--r--interp/reserve.ml9
-rw-r--r--interp/topconstr.ml47
-rw-r--r--interp/topconstr.mli27
-rw-r--r--lib/util.ml19
-rw-r--r--lib/util.mli4
-rw-r--r--parsing/egrammar.ml14
-rw-r--r--parsing/g_constr.ml410
-rw-r--r--parsing/g_constrnew.ml438
-rw-r--r--parsing/g_vernac.ml48
-rw-r--r--parsing/g_vernacnew.ml412
-rw-r--r--parsing/ppconstr.ml19
-rw-r--r--parsing/termast.ml69
-rw-r--r--pretyping/detyping.ml87
-rw-r--r--pretyping/pretyping.ml51
-rw-r--r--pretyping/rawterm.ml40
-rw-r--r--pretyping/rawterm.mli4
-rw-r--r--tactics/tacinterp.ml17
-rw-r--r--test-suite/output/Fixpoint.v7
-rw-r--r--toplevel/command.ml17
-rw-r--r--toplevel/vernac.ml2
-rw-r--r--translate/ppconstrnew.ml54
-rw-r--r--translate/ppconstrnew.mli7
-rw-r--r--translate/ppvernacnew.ml76
28 files changed, 541 insertions, 294 deletions
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 41ce1c4c1c..61d0d5a3af 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -34,7 +34,7 @@ and ct_COERCION_OPT =
and ct_COFIXTAC =
CT_cofixtac of ct_ID * ct_FORMULA
and ct_COFIX_REC =
- CT_cofix_rec of ct_ID * ct_FORMULA * ct_FORMULA
+ CT_cofix_rec of ct_ID * ct_BINDER_LIST * ct_FORMULA * ct_FORMULA
and ct_COFIX_REC_LIST =
CT_cofix_rec_list of ct_COFIX_REC * ct_COFIX_REC list
and ct_COFIX_TAC_LIST =
@@ -276,7 +276,8 @@ and ct_FIX_BINDER =
and ct_FIX_BINDER_LIST =
CT_fix_binder_list of ct_FIX_BINDER * ct_FIX_BINDER list
and ct_FIX_REC =
- CT_fix_rec of ct_ID * ct_BINDER_NE_LIST * ct_ID_OPT * ct_FORMULA * ct_FORMULA
+ CT_fix_rec of ct_ID * ct_BINDER_NE_LIST * ct_ID_OPT *
+ ct_FORMULA * ct_FORMULA
and ct_FIX_REC_LIST =
CT_fix_rec_list of ct_FIX_REC * ct_FIX_REC list
and ct_FIX_TAC_LIST =
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 8ff97b0c75..ff41852380 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -84,11 +84,12 @@ and fCOFIXTAC = function
fFORMULA x2;
fNODE "cofixtac" 2
and fCOFIX_REC = function
-| CT_cofix_rec(x1, x2, x3) ->
+| CT_cofix_rec(x1, x2, x3, x4) ->
fID x1;
- fFORMULA x2;
+ fBINDER_LIST x2;
fFORMULA x3;
- fNODE "cofix_rec" 3
+ fFORMULA x4;
+ fNODE "cofix_rec" 4
and fCOFIX_REC_LIST = function
| CT_cofix_rec_list(x,l) ->
fCOFIX_REC x;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 33b3488dbf..fad049a06b 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -293,22 +293,12 @@ let rec decompose_last = function
| [a] -> [], a
| a::tl -> let rl, b = decompose_last tl in (a::rl), b;;
-(* The boolean argument should be false if a name is not really necessary,
- for instance if there is only one argument. On the other hand, all
- recursive calls in this function should have the boolean argument to true,
- because recursive calls mean that there is more than one argument. *)
-
-let rec make_fix_struct b = function
- 0, CProdN(_, [(na::tl,_)], CProdN(_, _,_)) -> xlate_id_opt na
- | 0, CProdN(_, [([na],_)], _) ->
- if b then xlate_id_opt na else ctv_ID_OPT_NONE
- | n, CProdN(_, [(l,_)],body) ->
- let len = List.length l in
- if len <= n then
- make_fix_struct true (n-len, body)
- else
- xlate_id_opt(List.nth l n)
- | _, _ -> xlate_error "unexpected result of parsing for Fixpoint";;
+let make_fix_struct (n,bl) =
+ let names = names_of_local_assums bl in
+ let nn = List.length names in
+ if nn = 1 then ctv_ID_OPT_NONE
+ else if n < nn then xlate_id_opt(List.nth names n)
+ else xlate_error "unexpected result of parsing for Fixpoint";;
let rec xlate_binder = function
@@ -344,8 +334,6 @@ and
and
xlate_binder_list = function
l -> CT_binder_list( List.map xlate_binder_l l)
-and cvt_fixpoint_binders bl =
- CT_binder_list(List.map xlate_binder bl)
and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
CRef r -> varc (xlate_reference r)
@@ -432,20 +420,22 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
xlate_error "Second order variable not supported"
| CEvar (_, _) -> xlate_error "CEvar not supported"
| CCoFix (_, (_, id), lm::lmi) ->
- let strip_mutcorec (fid, arf, ardef) =
- CT_cofix_rec (xlate_ident fid, xlate_formula arf, xlate_formula ardef) in
+ let strip_mutcorec (fid, bl,arf, ardef) =
+ CT_cofix_rec (xlate_ident fid, xlate_binder_list bl,
+ xlate_formula arf, xlate_formula ardef) in
CT_cofixc(xlate_ident id,
(CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi)))
| CFix (_, (_, id), lm::lmi) ->
- let strip_mutrec (fid, n, optional_nargs, arf, ardef) =
- let struct_arg = make_fix_struct false (n, arf) in
- let split_rank = match optional_nargs with
- Some v -> v
- | None -> n+1 in
- let (bl,arf,ardef) = Ppconstr.split_fix split_rank arf ardef in
+ let strip_mutrec (fid, n, bl, arf, ardef) =
+ let (struct_arg,bl,arf,ardef) =
+ if bl = [] then
+ let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
+ let bl = List.map (fun(nal,ty)->LocalRawAssum(nal,ty)) bl in
+ (xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef)
+ else (make_fix_struct (n, bl),bl,arf,ardef) in
let arf = xlate_formula arf in
let ardef = xlate_formula ardef in
- match cvt_fixpoint_binders bl with
+ match xlate_binder_list bl with
| CT_binder_list (b :: bl) ->
CT_fix_rec (xlate_ident fid, CT_binder_ne_list (b, bl),
struct_arg, arf, ardef)
@@ -1868,15 +1858,16 @@ let rec xlate_vernac =
(CT_co_ind co_or_ind, CT_ind_spec_list (List.map strip_mutind lmi))
| VernacFixpoint [] -> xlate_error "mutual recursive"
| VernacFixpoint (lm :: lmi) ->
- let strip_mutrec ((fid, n, optional_nargs, arf, ardef), ntn) =
- let struct_arg = make_fix_struct false (n, arf) in
- let split_rank = match optional_nargs with
- Some v -> v
- | None -> n+1 in
- let (bl,arf,ardef) = Ppconstr.split_fix split_rank arf ardef in
+ let strip_mutrec ((fid, n, bl, arf, ardef), ntn) =
+ let (struct_arg,bl,arf,ardef) =
+ if bl = [] then
+ let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
+ let bl = List.map (fun(nal,ty)->LocalRawAssum(nal,ty)) bl in
+ (xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef)
+ else (make_fix_struct (n, bl),bl,arf,ardef) in
let arf = xlate_formula arf in
let ardef = xlate_formula ardef in
- match cvt_fixpoint_binders bl with
+ match xlate_binder_list bl with
| CT_binder_list (b :: bl) ->
CT_fix_rec (xlate_ident fid, CT_binder_ne_list (b, bl),
struct_arg, arf, ardef)
@@ -1885,8 +1876,9 @@ let rec xlate_vernac =
(CT_fix_rec_list (strip_mutrec lm, List.map strip_mutrec lmi))
| VernacCoFixpoint [] -> xlate_error "mutual corecursive"
| VernacCoFixpoint (lm :: lmi) ->
- let strip_mutcorec (fid, arf, ardef) =
- CT_cofix_rec (xlate_ident fid, xlate_formula arf, xlate_formula ardef) in
+ let strip_mutcorec (fid, bl, arf, ardef) =
+ CT_cofix_rec (xlate_ident fid, xlate_binder_list bl,
+ xlate_formula arf, xlate_formula ardef) in
CT_cofix_decl
(CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi))
| VernacScheme [] -> xlate_error "induction scheme"
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index fa1faf9cf3..0f0968aad7 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1009,14 +1009,16 @@ let rec check_same_type ty1 ty2 =
match ty1, ty2 with
| CRef r1, CRef r2 -> check_same_ref r1 r2
| CFix(_,(_,id1),fl1), CFix(_,(_,id2),fl2) when id1=id2 ->
- List.iter2 (fun (id1,i1,_,a1,b1) (id2,i2,_,a2,b2) ->
+ List.iter2 (fun (id1,i1,bl1,a1,b1) (id2,i2,bl2,a2,b2) ->
if id1<>id2 || i1<>i2 then failwith "not same fix";
+ check_same_fix_binder bl1 bl2;
check_same_type a1 a2;
check_same_type b1 b2)
fl1 fl2
| CCoFix(_,(_,id1),fl1), CCoFix(_,(_,id2),fl2) when id1=id2 ->
- List.iter2 (fun (id1,a1,b1) (id2,a2,b2) ->
+ List.iter2 (fun (id1,bl1,a1,b1) (id2,bl2,a2,b2) ->
if id1<>id2 then failwith "not same fix";
+ check_same_fix_binder bl1 bl2;
check_same_type a1 a2;
check_same_type b1 b2)
fl1 fl2
@@ -1066,6 +1068,15 @@ and check_same_binder (nal1,e1) (nal2,e2) =
if na1<>na2 then failwith "not same name") nal1 nal2;
check_same_type e1 e2
+and check_same_fix_binder bl1 bl2 =
+ List.iter2 (fun b1 b2 ->
+ match b1,b2 with
+ LocalRawAssum(nal1,ty1), LocalRawAssum(nal2,ty2) ->
+ check_same_binder (nal1,ty1) (nal2,ty2)
+ | LocalRawDef(na1,def1), LocalRawDef(na2,def2) ->
+ check_same_binder ([na1],def1) ([na2],def2)
+ | _ -> failwith "not same binder") bl1 bl2
+
let same c d = try check_same_type c d; true with _ -> false
(**********************************************************************)
@@ -1502,21 +1513,27 @@ let rec extern inctx scopes vars r =
(Some na,option_app (extern_type scopes (add_vname vars na)) typopt),
sub_extern false scopes vars b1, sub_extern false scopes vars b2)
- | RRec (loc,fk,idv,tyv,bv) ->
+ | RRec (loc,fk,idv,blv,tyv,bv) ->
let vars' = Array.fold_right Idset.add idv vars in
(match fk with
| RFix (nv,n) ->
let listdecl =
Array.mapi (fun i fi ->
- (fi,nv.(i), None, extern_type scopes vars tyv.(i),
- extern false scopes vars' bv.(i))) idv
+ let (ids,bl) = extern_local_binder scopes vars blv.(i) in
+ let vars0 = List.fold_right (name_fold Idset.add) ids vars in
+ let vars1 = List.fold_right (name_fold Idset.add) ids vars' in
+ (fi,nv.(i), bl, extern_type scopes vars1 tyv.(i),
+ extern false scopes vars0 bv.(i))) idv
in
CFix (loc,(loc,idv.(n)),Array.to_list listdecl)
| RCoFix n ->
let listdecl =
Array.mapi (fun i fi ->
- (fi,extern_type scopes vars tyv.(i),
- sub_extern false scopes vars' bv.(i))) idv
+ let (ids,bl) = extern_local_binder scopes vars blv.(i) in
+ let vars0 = List.fold_right (name_fold Idset.add) ids vars in
+ let vars1 = List.fold_right (name_fold Idset.add) ids vars' in
+ (fi,bl,extern_type scopes vars1 tyv.(i),
+ sub_extern false scopes vars0 bv.(i))) idv
in
CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl))
@@ -1557,6 +1574,29 @@ and factorize_lambda inctx scopes vars aty = function
((loc,na)::nal,c)
| c -> ([],sub_extern inctx scopes vars c)
+and extern_local_binder scopes vars = function
+ [] -> ([],[])
+ | (na,Some bd,ty)::l ->
+ let na = name_app translate_ident na in
+ let (ids,l) =
+ extern_local_binder scopes (name_fold Idset.add na vars) l in
+ (na::ids,
+ LocalRawDef((dummy_loc,na), extern false scopes vars bd) :: l)
+
+ | (na,None,ty)::l ->
+ let na = name_app translate_ident na in
+ let ty = extern_type scopes vars (anonymize_if_reserved na ty) in
+ (match extern_local_binder scopes (name_fold Idset.add na vars) l with
+ (ids,LocalRawAssum(nal,ty')::l)
+ when same ty ty' &
+ match na with Name id -> not (occur_var_constr_expr id ty')
+ | _ -> true ->
+ (na::ids,
+ LocalRawAssum((dummy_loc,na)::nal,ty')::l)
+ | (ids,l) ->
+ (na::ids,
+ LocalRawAssum([(dummy_loc,na)],ty) :: l))
+
and extern_eqn inctx scopes vars (loc,ids,pl,c) =
(loc,List.map (extern_cases_pattern_in_scope scopes vars) pl,
extern inctx scopes vars c)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index a12df82f5b..0812baaac5 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -530,18 +530,6 @@ let rec intern_cases_pattern scopes aliases tmp_scope = function
(**********************************************************************)
(* Fix and CoFix *)
-let rec intern_fix = function
- | [] -> ([],[],[],[])
- | (fi, n, on, c, t)::rest->
- let (lf,ln,lc,lt) = intern_fix rest in
- (fi::lf, n::ln, c::lc, t::lt)
-
-let rec intern_cofix = function
- | [] -> ([],[],[])
- | (fi, c, t)::rest ->
- let (lf,lc,lt) = intern_cofix rest in
- (fi::lf, c::lc, t::lt)
-
(**********************************************************************)
(* Utilities for binders *)
@@ -688,8 +676,9 @@ let internalise sigma env allow_soapp lvar c =
(match intern_impargs c env imp subscopes l with
| [] -> c
| l -> RApp (constr_loc x, c, l))
- | CFix (loc, (locid,iddef), ldecl) ->
- let (lf,ln,lc,lt) = intern_fix ldecl in
+ | CFix (loc, (locid,iddef), dl) ->
+ let lf = List.map (fun (id,_,_,_,_) -> id) dl in
+ let dl = Array.of_list dl in
let n =
try
(list_index iddef lf) -1
@@ -697,12 +686,22 @@ let internalise sigma env allow_soapp lvar c =
raise (InternalisationError (locid,UnboundFixName (false,iddef)))
in
let ids' = List.fold_right Idset.add lf ids in
- let defl =
- Array.of_list (List.map (intern (ids',None,scopes)) lt) in
- let arityl = Array.of_list (List.map (intern_type env) lc) in
- RRec (loc,RFix (Array.of_list ln,n), Array.of_list lf, arityl, defl)
- | CCoFix (loc, (locid,iddef), ldecl) ->
- let (lf,lc,lt) = intern_cofix ldecl in
+ let idl = Array.map
+ (fun (id,n,bl,ty,bd) ->
+ let ((ids'',_,_),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'',tmp_scope,scopes) ty,
+ intern (ids''',None,scopes) bd)) dl in
+ RRec (loc,RFix (Array.map (fun (_,n,_,_,_) -> n) dl,n),
+ Array.of_list lf,
+ Array.map (fun (bl,_,_) -> bl) idl,
+ Array.map (fun (_,ty,_) -> ty) idl,
+ Array.map (fun (_,_,bd) -> bd) idl)
+ | CCoFix (loc, (locid,iddef), dl) ->
+ let lf = List.map (fun (id,_,_,_) -> id) dl in
+ let dl = Array.of_list dl in
let n =
try
(list_index iddef lf) -1
@@ -710,10 +709,19 @@ let internalise sigma env allow_soapp lvar c =
raise (InternalisationError (locid,UnboundFixName (true,iddef)))
in
let ids' = List.fold_right Idset.add lf ids in
- let defl =
- Array.of_list (List.map (intern (ids',None,scopes)) lt) in
- let arityl = Array.of_list (List.map (intern_type env) lc) in
- RRec (loc,RCoFix n, Array.of_list lf, arityl, defl)
+ let idl = Array.map
+ (fun (id,bl,ty,bd) ->
+ let ((ids'',_,_),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'',tmp_scope,scopes) ty,
+ intern (ids''',None,scopes) bd)) dl in
+ RRec (loc,RCoFix 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, intern_type env c1, intern_type env c2)
| CProdN (loc,[],c2) ->
@@ -813,6 +821,17 @@ let internalise sigma env allow_soapp lvar c =
and intern_type (ids,_,scopes) =
intern (ids,Some Symbols.type_scope,scopes)
+ and intern_local_binder ((ids,ts,sc as env),bl) = function
+ LocalRawAssum(nal,ty) ->
+ let ids' = List.fold_left
+ (fun ids (_,na) -> name_fold Idset.add na ids) ids nal in
+ ((ids',ts,sc),
+ List.map (fun (_,na) ->
+ (na,None,intern_type env ty)) nal @bl)
+ | LocalRawDef((loc,na),def) ->
+ ((name_fold Idset.add na ids,ts,sc),
+ (na,Some(intern env def),RHole(loc,BinderType na))::bl)
+
and intern_eqn n (ids,tmp_scope,scopes as env) (loc,lhs,rhs) =
let (idsl_substl_list,pl) =
List.split
diff --git a/interp/reserve.ml b/interp/reserve.ml
index ed4cdba39f..8334922741 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -69,8 +69,13 @@ let rec unloc = function
RLetTuple (dummy_loc,nal,(na,option_app unloc po),unloc b,unloc c)
| RIf (_,c,(na,po),b1,b2) ->
RIf (dummy_loc,unloc c,(na,option_app unloc po),unloc b1,unloc b2)
- | RRec (_,fk,idl,tyl,bv) ->
- RRec (dummy_loc,fk,idl,Array.map unloc tyl,Array.map unloc bv)
+ | RRec (_,fk,idl,bl,tyl,bv) ->
+ RRec (dummy_loc,fk,idl,
+ Array.map (List.map
+ (fun (na,obd,ty) -> (na,option_app unloc obd, unloc ty)))
+ bl,
+ Array.map unloc tyl,
+ Array.map unloc bv)
| RCast (_,c,t) -> RCast (dummy_loc,unloc c,unloc t)
| RSort (_,x) -> RSort (dummy_loc,x)
| RHole (_,x) -> RHole (dummy_loc,x)
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 3d26e9d7f8..1fe8edaca3 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -361,22 +361,27 @@ type constr_expr =
| CDelimiters of loc * string * constr_expr
| CDynamic of loc * Dyn.t
-and fixpoint_expr = identifier * int * int option * constr_expr * constr_expr
+and fixpoint_expr =
+ identifier * int * local_binder list * constr_expr * constr_expr
-and cofixpoint_expr = identifier * constr_expr * constr_expr
+and local_binder =
+ | LocalRawDef of name located * constr_expr
+ | LocalRawAssum of name located list * constr_expr
+
+and cofixpoint_expr =
+ identifier * local_binder list * constr_expr * constr_expr
(***********************)
(* For binders parsing *)
-type local_binder =
- | LocalRawDef of name located * constr_expr
- | LocalRawAssum of name located list * constr_expr
-
let rec local_binders_length = function
| [] -> 0
| LocalRawDef _::bl -> 1 + local_binders_length bl
| LocalRawAssum (idl,_)::bl -> List.length idl + local_binders_length bl
+let names_of_local_assums bl =
+ List.flatten (List.map (function LocalRawAssum(l,_)->l|_->[]) bl)
+
(**********************************************************************)
(* Functions on constr_expr *)
@@ -475,8 +480,19 @@ let map_binder g e nal = List.fold_right (fun (_,na) -> name_fold g na) nal e
let map_binders f g e bl =
(* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
- let h (nal,t) (e,bl) = (map_binder g e nal,(nal,f e t)::bl) in
- List.fold_right h bl (e,[])
+ let h (e,bl) (nal,t) = (map_binder g e nal,(nal,f e t)::bl) in
+ let (e,rbl) = List.fold_left h (e,[]) bl in
+ (e, List.rev rbl)
+
+let map_local_binders f g e bl =
+ (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
+ let h (e,bl) = function
+ LocalRawAssum(nal,ty) ->
+ (map_binder g e nal, LocalRawAssum(nal,f e ty)::bl)
+ | LocalRawDef((loc,na),ty) ->
+ (name_fold g na e, LocalRawDef((loc,na),f e ty)::bl) in
+ let (e,rbl) = List.fold_left h (e,[]) bl in
+ (e, List.rev rbl)
let map_constr_expr_with_binders f g e = function
| CArrow (loc,a,b) -> CArrow (loc,f e a,f e b)
@@ -518,9 +534,20 @@ let map_constr_expr_with_binders f g e = function
let e' = option_fold_right (name_fold g) ona e in
CIf (loc,f e c,(ona,option_app (f e') po),f e b1,f e b2)
| CFix (loc,id,dl) ->
- CFix (loc,id,List.map (fun (id,n,on,t,d) -> (id,n,on,f e t,f e d)) dl)
+ CFix (loc,id,List.map (fun (id,n,bl,t,d) ->
+ let (e',bl') = map_local_binders f g e bl in
+ let t' = f e' t in
+ (* Note: fix names should be inserted before the arguments... *)
+ let e'' = List.fold_left (fun e (id,_,_,_,_) -> g id e) e' dl in
+ let d' = f e'' d in
+ (id,n,bl',t',d')) dl)
| CCoFix (loc,id,dl) ->
- CCoFix (loc,id,List.map (fun (id,t,d) -> (id,f e t,f e d)) dl)
+ CCoFix (loc,id,List.map (fun (id,bl,t,d) ->
+ let (e',bl') = map_local_binders f g e bl in
+ let t' = f e' t in
+ let e'' = List.fold_left (fun e (id,_,_,_) -> g id e) e' dl in
+ let d' = f e'' d in
+ (id,bl',t',d')) dl)
(* Used in constrintern *)
let rec replace_vars_constr_expr l = function
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index d35418b515..a56a96dea6 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -107,9 +107,16 @@ type constr_expr =
| CDelimiters of loc * string * constr_expr
| CDynamic of loc * Dyn.t
-and fixpoint_expr = identifier * int * int option * constr_expr * constr_expr
+and fixpoint_expr =
+ identifier * int * local_binder list * constr_expr * constr_expr
+
+and cofixpoint_expr =
+ identifier * local_binder list * constr_expr * constr_expr
+
+and local_binder =
+ | LocalRawDef of name located * constr_expr
+ | LocalRawAssum of name located list * constr_expr
-and cofixpoint_expr = identifier * constr_expr * constr_expr
val constr_loc : constr_expr -> loc
@@ -131,6 +138,14 @@ val mkLambdaC : name located list * constr_expr * constr_expr -> constr_expr
val mkLetInC : name located * constr_expr * constr_expr -> constr_expr
val mkProdC : name located list * constr_expr * constr_expr -> constr_expr
+(* For binders parsing *)
+
+(* Includes let binders *)
+val local_binders_length : local_binder list -> int
+
+(* Does not take let binders into account *)
+val names_of_local_assums : local_binder list -> name located list
+
(* 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)] *)
@@ -138,14 +153,6 @@ val map_constr_expr_with_binders :
('a -> constr_expr -> constr_expr) ->
(identifier -> 'a -> 'a) -> 'a -> constr_expr -> constr_expr
-(* For binders parsing *)
-
-type local_binder =
- | LocalRawDef of name located * constr_expr
- | LocalRawAssum of name located list * constr_expr
-
-val local_binders_length : local_binder list -> int
-
(* Concrete syntax for modules and modules types *)
type with_declaration_ast =
diff --git a/lib/util.ml b/lib/util.ml
index f57b9a6dbc..f2af9f6d43 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -401,6 +401,25 @@ let array_for_all2 f v1 v2 =
let lv1 = Array.length v1 in
lv1 = Array.length v2 && allrec (pred lv1)
+let array_for_all3 f v1 v2 v3 =
+ let rec allrec = function
+ | -1 -> true
+ | n -> (f v1.(n) v2.(n) v3.(n)) && (allrec (n-1))
+ in
+ let lv1 = Array.length v1 in
+ lv1 = Array.length v2 && lv1 = Array.length v3 && allrec (pred lv1)
+
+let array_for_all4 f v1 v2 v3 v4 =
+ let rec allrec = function
+ | -1 -> true
+ | n -> (f v1.(n) v2.(n) v3.(n) v4.(n)) && (allrec (n-1))
+ in
+ let lv1 = Array.length v1 in
+ lv1 = Array.length v2 &&
+ lv1 = Array.length v3 &&
+ lv1 = Array.length v4 &&
+ allrec (pred lv1)
+
let array_hd v =
match Array.length v with
| 0 -> failwith "array_hd"
diff --git a/lib/util.mli b/lib/util.mli
index e2e46f5286..121b114a7d 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -136,6 +136,10 @@ val list_map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
val array_exists : ('a -> bool) -> 'a array -> bool
val array_for_all : ('a -> bool) -> 'a array -> bool
val array_for_all2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool
+val array_for_all3 : ('a -> 'b -> 'c -> bool) ->
+ 'a array -> 'b array -> 'c array -> bool
+val array_for_all4 : ('a -> 'b -> 'c -> 'd -> bool) ->
+ 'a array -> 'b array -> 'c array -> 'd array -> bool
val array_hd : 'a array -> 'a
val array_tl : 'a array -> 'a array
val array_last : 'a array -> 'a
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 27f52e73a1..c8f167eb3b 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -237,9 +237,19 @@ let subst_constr_expr a loc subs =
let na = option_app (name_app (subst_id subs)) na in
CIf (loc,subst c,(na,option_app subst po),subst b1,subst b2)
| CFix (_,id,dl) ->
- CFix (loc,id,List.map (fun (id,n,on, t,d) -> (id,n, on,subst t,subst d)) dl)
+ CFix (loc,id,List.map (fun (id,n,bl, t,d) ->
+ (id,n,
+ List.map(function
+ LocalRawAssum(nal,ty) -> LocalRawAssum(nal,subst ty)
+ | LocalRawDef(na,def) -> LocalRawDef(na,subst def)) bl,
+ subst t,subst d)) dl)
| CCoFix (_,id,dl) ->
- CCoFix (loc,id,List.map (fun (id,t,d) -> (id,subst t,subst d)) dl)
+ CCoFix (loc,id,List.map (fun (id,bl,t,d) ->
+ (id,
+ List.map(function
+ LocalRawAssum(nal,ty) -> LocalRawAssum(nal,subst ty)
+ | LocalRawDef(na,def) -> LocalRawDef(na,subst def)) bl,
+ subst t,subst d)) dl)
in subst a
let make_rule univ assoc etyp rule =
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 3e513f0719..2f606ffd30 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -339,21 +339,19 @@ GEXTEND Gram
fixbinder:
[ [ id = base_ident; "/"; recarg = natural; ":"; type_ = constr;
":="; def = constr ->
- (id, recarg-1, None, type_, def)
+ (id, recarg-1, [], type_, def)
| id = base_ident; bl = ne_simple_binders_list; ":"; type_ = constr;
":="; def = constr ->
let ni = List.length (List.flatten (List.map fst bl)) -1 in
- let loc0 = fst (List.hd (fst (List.hd bl))) in
- let loc1 = join_loc loc0 (constr_loc type_) in
- let loc2 = join_loc loc0 (constr_loc def) in
- (id, ni, None, CProdN (loc1,bl,type_), CLambdaN (loc2,bl,def)) ] ]
+ let bl = List.map (fun(nal,ty)->LocalRawAssum(nal,ty)) bl in
+ (id, ni, bl, type_, def) ] ]
;
fixbinders:
[ [ fbs = LIST1 fixbinder SEP "with" -> fbs ] ]
;
cofixbinder:
[ [ id = base_ident; ":"; type_ = constr; ":="; def = constr ->
- (id, type_, def) ] ]
+ (id, [],type_, def) ] ]
;
cofixbinders:
[ [ fbs = LIST1 cofixbinder SEP "with" -> fbs ] ]
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index fb770768a9..606949e5f9 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -68,37 +68,33 @@ let rec mkCLambdaN loc bll c =
| [] -> c
| LocalRawAssum ([],_) :: bll -> mkCLambdaN loc bll c
-let rec decls_of_binders = function
- | [] -> []
- | LocalRawDef _::bl -> decls_of_binders bl
- | LocalRawAssum (idl,_)::bl -> idl @ decls_of_binders bl
-
-let rec index_of_annot bl ann =
- match decls_of_binders bl,ann with
+let rec index_of_annot loc bl ann =
+ match names_of_local_assums bl,ann with
| [_], None -> 0
| lids, Some x ->
let ids = List.map snd lids in
(try list_index (snd x) ids - 1
- with Not_found -> error "no such fix variable")
- | _ -> error "cannot guess decreasing argument of fix"
+ with Not_found ->
+ user_err_loc(fst x,"index_of_annot", Pp.str"no such fix variable"))
+ | _ -> user_err_loc(loc,"index_of_annot",
+ Pp.str "cannot guess decreasing argument of fix")
-let mk_fixb (loc,id,bl,ann,body,(tloc,tyc)) =
- let n = index_of_annot bl ann in
- let nargs = List.length (decls_of_binders bl) in
+let mk_fixb (id,bl,ann,body,(loc,tyc)) =
+ let n = index_of_annot (fst id) bl ann in
let ty = match tyc with
- None -> CHole tloc
- | Some t -> mkCProdN loc bl t in
- (snd id,n,Some nargs,ty,mkCLambdaN loc bl body)
+ Some ty -> ty
+ | None -> CHole loc in
+ (snd id,n,bl,ty,body)
-let mk_cofixb (loc,id,bl,ann,body,(tloc,tyc)) =
+let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
let _ = option_app (fun (aloc,_) ->
Util.user_err_loc
(aloc,"Constr:mk_cofixb",
Pp.str"Annotation forbidden in cofix expression")) ann in
let ty = match tyc with
- None -> CHole tloc
- | Some t -> mkCProdN loc bl t in
- (snd id,ty,mkCLambdaN loc bl body)
+ Some ty -> ty
+ | None -> CHole loc in
+ (snd id,bl,ty,body)
let mk_fix(loc,kw,id,dcls) =
if kw then
@@ -109,7 +105,7 @@ let mk_fix(loc,kw,id,dcls) =
CCoFix(loc,id,fb)
let mk_single_fix (loc,kw,dcl) =
- let (_,id,_,_,_,_) = dcl in mk_fix(loc,kw,id,[dcl])
+ let (id,_,_,_,_) = dcl in mk_fix(loc,kw,id,[dcl])
let binder_constr =
create_constr_entry (get_univ "constr") "binder_constr"
@@ -255,7 +251,7 @@ GEXTEND Gram
;
fix_decl:
[ [ id=identref; bl=LIST0 binder_let; ann=fixannot; ty=type_cstr; ":=";
- c=operconstr LEVEL "200" -> (loc,id,bl,ann,c,ty) ] ]
+ c=operconstr LEVEL "200" -> (id,bl,ann,c,ty) ] ]
;
fixannot:
[ [ "{"; IDENT "struct"; id=name; "}" -> Some id
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index def4b9fbf9..cde9061b3d 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -252,17 +252,15 @@ GEXTEND Gram
[ [ id = base_ident; bl = ne_fix_binders; ":"; type_ = constr;
":="; def = constr; ntn = OPT decl_notation ->
let ni = List.length (List.flatten (List.map fst bl)) - 1 in
- let loc0 = fst (List.hd (fst (List.hd bl))) in
- let loc1 = join_loc loc0 (constr_loc type_) in
- let loc2 = join_loc loc0 (constr_loc def) in
- ((id, ni, None, CProdN (loc1,bl,type_), CLambdaN (loc2,bl,def)), ntn) ] ]
+ let bl = List.map (fun(nal,ty)->LocalRawAssum(nal,ty)) bl in
+ ((id, ni, bl, type_, def), ntn) ] ]
;
specifrec:
[ [ l = LIST1 onerec SEP "with" -> l ] ]
;
onecorec:
[ [ id = base_ident; ":"; c = constr; ":="; def = constr ->
- (id,c,def) ] ]
+ (id,[],c,def) ] ]
;
specifcorec:
[ [ l = LIST1 onecorec SEP "with" -> l ] ]
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 70235d9ecf..75222eaa43 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -204,8 +204,7 @@ GEXTEND Gram
[ [ id = base_ident; bl = LIST1 binder_let;
annot = OPT rec_annotation; type_ = type_cstr;
":="; def = lconstr; ntn = decl_notation ->
- let names = List.map snd (G_constrnew.decls_of_binders bl) in
- let nargs = List.length names in
+ let names = List.map snd (names_of_local_assums bl) in
let ni =
match annot with
Some id ->
@@ -219,17 +218,12 @@ GEXTEND Gram
(loc,"Fixpoint",
Pp.str "the recursive argument needs to be specified");
0 in
- let loc0 = G_constrnew.loc_of_binder_let bl in
- let loc1 = join_loc loc0 (constr_loc type_) in
- let loc2 = join_loc loc0 (constr_loc def) in
- ((id, ni, Some nargs, G_constrnew.mkCProdN loc1 bl type_,
- G_constrnew.mkCLambdaN loc2 bl def),ntn) ] ]
+ ((id, ni, bl, type_, def),ntn) ] ]
;
corec_definition:
[ [ id = base_ident; bl = LIST0 binder_let; c = type_cstr; ":=";
def = lconstr ->
- (id,G_constrnew.mkCProdN loc bl c ,
- G_constrnew.mkCLambdaN loc bl def) ] ]
+ (id,bl,c ,def) ] ]
;
rec_annotation:
[ [ "{"; IDENT "struct"; id=IDENT; "}" -> id_of_string id ] ]
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 77853c5e1a..335d3b7964 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -110,6 +110,13 @@ let pr_binder pr (nal,t) =
let pr_binders pr bl =
hv 0 (prlist_with_sep pr_semicolon (pr_binder pr) bl)
+let pr_local_binder pr = function
+ LocalRawAssum(nal,t) -> pr_binder pr (nal,t)
+ | LocalRawDef((_,na),t) -> pr_let_binder pr na t
+
+let pr_local_binders pr bl =
+ hv 0 (prlist_with_sep pr_semicolon (pr_local_binder pr) bl)
+
let pr_global vars ref = pr_global_env vars ref
let rec pr_lambda_tail pr bll = function
@@ -155,13 +162,15 @@ let rec split_fix n typ def =
let (bl,typ,def) = split_fix (n-1) typ def in
(concat_binder na t bl,typ,def)
-let pr_fixdecl pr (id,n,_,t,c) =
- let (bl,t,c) = split_fix (n+1) t c in
+let pr_fixdecl pr (id,n,bl,t,c) =
pr_recursive_decl pr id
- (brk (1,2) ++ str "[" ++ pr_binders pr bl ++ str "]") t c
+ (brk (1,2) ++ str "[" ++ pr_local_binders pr bl ++ str "]") t c
-let pr_cofixdecl pr (id,t,c) =
- pr_recursive_decl pr id (mt ()) t c
+let pr_cofixdecl pr (id,bl,t,c) =
+ let b =
+ if bl=[] then mt() else
+ brk(1,2) ++ str"[" ++ pr_local_binders pr bl ++ str "]" in
+ pr_recursive_decl pr id b t c
let pr_recursive fix pr_decl id = function
| [] -> anomaly "(co)fixpoint with no definition"
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 0e8b84f741..8f00678f1e 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -95,6 +95,29 @@ let idopt_of_name = function
| Name id -> Some id
| Anonymous -> None
+let ast_of_binders bl =
+ List.map (fun (nal,isdef,ty) ->
+ if isdef then ope("LETBINDER",ty::List.map ast_of_name nal)
+ else ope("BINDER",ty::List.map ast_of_name nal)) bl
+
+let ast_type_of_binder bl t =
+ List.fold_right (fun (nal,isdef,ty) ast ->
+ if isdef then
+ ope("LETIN",[ty;slam(idopt_of_name (List.hd nal),ast)])
+ else
+ ope("PROD",[ty;List.fold_right
+ (fun na ast -> slam(idopt_of_name na,ast)) nal ast]))
+ bl t
+
+let ast_body_of_binder bl t =
+ List.fold_right (fun (nal,isdef,ty) ast ->
+ if isdef then
+ ope("LETIN",[ty;slam(idopt_of_name (List.hd nal),ast)])
+ else
+ ope("LAMBDA",[ty;List.fold_right
+ (fun na ast -> slam(idopt_of_name na,ast)) nal ast]))
+ bl t
+
let ast_of_constant_ref sp =
ope("CONST", [path_section dummy_loc sp])
@@ -259,12 +282,12 @@ let rec ast_of_raw = function
| RLetTuple _ | RIf _ ->
error "Let tuple not supported in v7"
- | RRec (_,fk,idv,tyv,bv) ->
+ | RRec (_,fk,idv,blv,tyv,bv) ->
let alfi = Array.map ast_of_ident idv in
(match fk with
| RFix (nv,n) ->
let rec split_lambda binds = function
- | (0, t) -> (binds,ast_of_raw t)
+ | (0, t) -> (List.rev binds,ast_of_raw t)
| (n, RLetIn (_,na,b,c)) ->
let bind = ope("LETBINDER",[ast_of_raw b;ast_of_name na]) in
split_lambda (bind::binds) (n,c)
@@ -280,11 +303,26 @@ let rec ast_of_raw = function
let listdecl =
Array.mapi
(fun i fi ->
- let (lparams,astdef) = split_lambda [] (nv.(i)+1,bv.(i)) in
- let asttyp = split_product (nv.(i)+1,tyv.(i)) in
- ope("FDECL",
- [fi; ope ("BINDERS",List.rev lparams);
- asttyp; astdef]))
+ if List.length blv.(i) >= nv.(i)+1 then
+ let (oldfixp,factb) = list_chop (nv.(i)+1) blv.(i) in
+ let bl = factorize_local_binder oldfixp in
+ let factb = factorize_local_binder factb in
+ let asttyp = ast_type_of_binder factb
+ (ast_of_raw tyv.(i)) in
+ let astdef = ast_body_of_binder factb
+ (ast_of_raw bv.(i)) in
+ ope("FDECL",[fi;ope("BINDERS",ast_of_binders bl);
+ asttyp; astdef])
+ else
+ let n = nv.(i)+1 - List.length blv.(i) in
+ let (lparams,astdef) =
+ split_lambda [] (n,bv.(i)) in
+ let bl = factorize_local_binder blv.(i) in
+ let lparams = ast_of_binders bl @ lparams in
+ let asttyp = split_product (n,tyv.(i)) in
+ ope("FDECL",
+ [fi; ope ("BINDERS",lparams);
+ asttyp; astdef]))
alfi
in
ope("FIX", alfi.(n)::(Array.to_list listdecl))
@@ -292,7 +330,10 @@ let rec ast_of_raw = function
let listdecl =
Array.mapi
(fun i fi ->
- ope("CFDECL",[fi; ast_of_raw tyv.(i); ast_of_raw bv.(i)]))
+ let bl = factorize_local_binder blv.(i) in
+ let asttyp = ast_type_of_binder bl (ast_of_raw tyv.(i)) in
+ let astdef = ast_body_of_binder bl (ast_of_raw bv.(i)) in
+ ope("CFDECL",[fi; asttyp; astdef]))
alfi
in
ope("COFIX", alfi.(n)::(Array.to_list listdecl)))
@@ -325,6 +366,18 @@ and factorize_binder n oper na aty c =
in
(p,slam(idopt_of_name na, body))
+and factorize_local_binder = function
+ [] -> []
+ | (na,Some bd,ty)::l ->
+ ([na],true,ast_of_raw bd) :: factorize_local_binder l
+ | (na,None,ty)::l ->
+ let ty = ast_of_raw ty in
+ (match factorize_local_binder l with
+ (lna,false,ty') :: l when ty=ty' ->
+ (na::lna,false,ty') :: l
+ | l -> ([na],false,ty) :: l)
+
+
let ast_of_rawconstr = ast_of_raw
(******************************************************************)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index ffd2fad54a..e1f0da13b5 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -358,45 +358,14 @@ and detype_fix tenv avoid env (vn,_ as nvn) (names,tys,bodies) =
let id = next_name_away na avoid in
(id::avoid, add_name (Name id) env, id::l))
(avoid, env, []) names in
- (* Be sure that bodies and types share the same names *)
- let rec share_names n l avoid env c t =
- if n = 0 then
- let c = detype tenv avoid env c in
- let t = detype tenv avoid env t in
- List.fold_left (fun (c,typ) (na,body,t) -> match body with
- | None -> (RLambda (dummy_loc,na,t,c),RProd (dummy_loc,na,t,typ))
- | Some b -> (RLetIn (dummy_loc,na,b,c),RLetIn (dummy_loc,na,b,typ)))
- (c,t) l
- else match kind_of_term c, kind_of_term t with
- | Lambda (na,t,c), Prod (_,t',c') ->
- let t = detype tenv avoid env t in
- let id = next_name_away na avoid in
- let avoid = id::avoid and env = add_name (Name id) env in
- share_names (n-1) ((Name id,None,t)::l) avoid env c c'
- (* May occur for fix built interactively *)
- | LetIn (na,b,t',c), _ ->
- let t' = detype tenv avoid env t' in
- let b = detype tenv avoid env b in
- let id = next_name_away na avoid in
- let avoid = id::avoid and env = add_name (Name id) env in
- share_names n ((Name id,Some b,t')::l) avoid env c t
- (* Only if built with the f/n notation or w/o let-expansion in types *)
- | _, LetIn (_,b,_,t) ->
- share_names n l avoid env c (subst1 b t)
- (* If it is an open proof: we cheat and eta-expand *)
- | _, Prod (na',t',c') ->
- let t' = detype tenv avoid env t' in
- let avoid = name_cons na' avoid and env = add_name na' env in
- let appc = mkApp (lift 1 c,[|mkRel 1|]) in
- share_names (n-1) ((na',None,t')::l) avoid env appc c'
- (* If built with the f/n notation: we renounce to share names *)
- | _ -> share_names 0 l avoid env c t in
let n = Array.length tys in
let v = array_map3
- (fun c t i -> share_names (i+1) [] def_avoid def_env c (lift n t))
+ (fun c t i -> share_names tenv (i+1) [] def_avoid def_env c (lift n t))
bodies tys vn in
RRec(dummy_loc,RFix nvn,Array.of_list (List.rev lfi),
- Array.map snd v, Array.map fst v)
+ Array.map (fun (bl,_,_) -> bl) v,
+ Array.map (fun (_,_,ty) -> ty) v,
+ Array.map (fun (_,bd,_) -> bd) v)
and detype_cofix tenv avoid env n (names,tys,bodies) =
let def_avoid, def_env, lfi =
@@ -405,9 +374,53 @@ and detype_cofix tenv avoid env n (names,tys,bodies) =
let id = next_name_away na avoid in
(id::avoid, add_name (Name id) env, id::l))
(avoid, env, []) names in
+ let n = Array.length tys in
+ let v = array_map2
+ (fun c t -> share_names tenv 0 [] def_avoid def_env c (lift n t))
+ bodies tys in
RRec(dummy_loc,RCoFix n,Array.of_list (List.rev lfi),
- Array.map (detype tenv avoid env) tys,
- Array.map (detype tenv def_avoid def_env) bodies)
+ Array.map (fun (bl,_,_) -> bl) v,
+ Array.map (fun (_,_,ty) -> ty) v,
+ Array.map (fun (_,bd,_) -> bd) v)
+
+and share_names tenv n l avoid env c t =
+ if !Options.v7 && n=0 then
+ let c = detype tenv avoid env c in
+ let t = detype tenv avoid env t in
+ (l,c,t)
+ else
+ match kind_of_term c, kind_of_term t with
+ | Lambda (na,t,c), Prod (na',t',c') ->
+ let na = match (na,na') with
+ Name _, _ -> na
+ | _, Name _ -> na'
+ | _ -> na in
+ let t = detype tenv avoid env t in
+ let id = next_name_away na avoid in
+ let avoid = id::avoid and env = add_name (Name id) env in
+ share_names tenv (n-1) ((Name id,None,t)::l) avoid env c c'
+ (* May occur for fix built interactively *)
+ | LetIn (na,b,t',c), _ ->
+ let t' = detype tenv avoid env t' in
+ let b = detype tenv avoid env b in
+ let id = next_name_away na avoid in
+ let avoid = id::avoid and env = add_name (Name id) env in
+ share_names tenv n ((Name id,Some b,t')::l) avoid env c t
+ (* Only if built with the f/n notation or w/o let-expansion in types *)
+ | _, LetIn (_,b,_,t) ->
+ share_names tenv n l avoid env c (subst1 b t)
+ (* If it is an open proof: we cheat and eta-expand *)
+ | _, Prod (na',t',c') ->
+ let t' = detype tenv avoid env t' in
+ let avoid = name_cons na' avoid and env = add_name na' env in
+ let appc = mkApp (lift 1 c,[|mkRel 1|]) in
+ share_names tenv (n-1) ((na',None,t')::l) avoid env appc c'
+ (* If built with the f/n notation: we renounce to share names *)
+ | _ ->
+ if n>0 then warning "Detyping.detype: cannot factorize fix enough";
+ let c = detype tenv avoid env c in
+ let t = detype tenv avoid env t in
+ (l,c,t)
and detype_eqn tenv avoid env constr construct_nargs branch =
let make_pat x avoid env b ids =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 5f2d8d97dd..a2ea06e4ef 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -244,31 +244,54 @@ let rec pretype tycon env isevars lvar = function
{ uj_val = new_isevar isevars env (loc,k) ty; uj_type = ty }
| None -> error_unsolvable_implicit loc env (evars_of isevars) k)
- | RRec (loc,fixkind,names,lar,vdef) ->
+ | RRec (loc,fixkind,names,bl,lar,vdef) ->
+ let rec type_bl env ctxt = function
+ [] -> ctxt
+ | (na,None,ty)::bl ->
+ let ty' = pretype_type empty_valcon env isevars lvar ty in
+ let dcl = (na,None,ty'.utj_val) in
+ type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl
+ | (na,Some bd,ty)::bl ->
+ let ty' = pretype_type empty_valcon env isevars lvar ty in
+ let bd' = pretype (mk_tycon ty'.utj_val) env isevars lvar ty in
+ let dcl = (na,Some bd'.uj_val,ty'.utj_val) in
+ type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl in
+ let ctxtv = Array.map (type_bl env empty_rel_context) bl in
let larj =
- Array.map (pretype_type empty_valcon env isevars lvar) lar in
+ array_map2
+ (fun e ar ->
+ pretype_type empty_valcon (push_rel_context e env) isevars lvar ar)
+ ctxtv lar in
let lara = Array.map (fun a -> a.utj_val) larj in
+ let ftys = array_map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in
let nbfix = Array.length lar in
let names = Array.map (fun id -> Name id) names in
- let newenv = push_rec_types (names,lara,[||]) env in
+ (* Note: bodies are not used by push_rec_types, so [||] is safe *)
+ let newenv = push_rec_types (names,ftys,[||]) env in
let vdefj =
- Array.mapi
- (fun i def -> (* we lift nbfix times the type in tycon, because of
- * the nbfix variables pushed to newenv *)
- pretype (mk_tycon (lift nbfix (larj.(i).utj_val)))
- newenv isevars lvar def)
- vdef in
- evar_type_fixpoint loc env isevars names lara vdefj;
+ array_map2_i
+ (fun i ctxt def ->
+ (* we lift nbfix times the type in tycon, because of
+ * the nbfix variables pushed to newenv *)
+ let (ctxt,ty) =
+ decompose_prod_n_assum (rel_context_length ctxt)
+ (lift nbfix ftys.(i)) in
+ let nenv = push_rel_context ctxt newenv in
+ let j = pretype (mk_tycon ty) nenv isevars lvar def in
+ { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
+ uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
+ ctxtv vdef in
+ evar_type_fixpoint loc env isevars names ftys vdefj;
let fixj =
match fixkind with
| RFix (vn,i as vni) ->
- let fix = (vni,(names,lara,Array.map j_val vdefj)) in
+ let fix = (vni,(names,ftys,Array.map j_val vdefj)) in
(try check_fix env fix with e -> Stdpp.raise_with_loc loc e);
- make_judge (mkFix fix) lara.(i)
+ make_judge (mkFix fix) ftys.(i)
| RCoFix i ->
- let cofix = (i,(names,lara,Array.map j_val vdefj)) in
+ let cofix = (i,(names,ftys,Array.map j_val vdefj)) in
(try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e);
- make_judge (mkCoFix cofix) lara.(i) in
+ make_judge (mkCoFix cofix) ftys.(i) in
inh_conv_coerce_to_tycon loc env isevars fixj tycon
| RSort (loc,s) ->
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 6442ca9693..6e7f8f70fc 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -70,19 +70,20 @@ type rawconstr =
| RCases of loc * (rawconstr option * rawconstr option ref) *
(rawconstr * (name * (loc * inductive * name list) option) ref) list *
(loc * identifier list * cases_pattern list * rawconstr) list
- (* Rem: "ref" used for the v7->v8 translation only *)
| ROrderedCase of loc * case_style * rawconstr option * rawconstr *
rawconstr array * rawconstr option ref
| RLetTuple of loc * name list * (name * rawconstr option) *
rawconstr * rawconstr
| RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
- | RRec of loc * fix_kind * identifier array *
+ | RRec of loc * fix_kind * identifier array * rawdecl list array *
rawconstr array * rawconstr array
| RSort of loc * rawsort
| RHole of (loc * hole_kind)
| RCast of loc * rawconstr * rawconstr
| RDynamic of loc * Dyn.t
+and rawdecl = name * rawconstr option * rawconstr
+
let cases_predicate_names tml =
List.flatten (List.map (function
| (tm,{contents=(na,None)}) -> [na]
@@ -97,6 +98,7 @@ let cases_predicate_names tml =
- boolean in POldCase means it is recursive
i*)
+let map_rawdecl f (na,obd,ty) = (na,option_app f obd,f ty)
let map_rawconstr f = function
| RVar (loc,id) -> RVar (loc,id)
@@ -114,9 +116,12 @@ let map_rawconstr f = function
RLetTuple (loc,nal,(na,option_app f po),f b,f c)
| RIf (loc,c,(na,po),b1,b2) ->
RIf (loc,f c,(na,option_app f po),f b1,f b2)
- | RRec (loc,fk,idl,tyl,bv) -> RRec (loc,fk,idl,Array.map f tyl,Array.map f bv)
+ | RRec (loc,fk,idl,bl,tyl,bv) ->
+ RRec (loc,fk,idl,Array.map (List.map (map_rawdecl f)) bl,
+ Array.map f tyl,Array.map f bv)
| RCast (loc,c,t) -> RCast (loc,f c,f t)
| (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) as x -> x
+
(*
let name_app f e = function
@@ -176,9 +181,18 @@ let occur_rawconstr id =
or (occur b) or (not (List.mem (Name id) nal) & (occur c))
| RIf (loc,c,rtntyp,b1,b2) ->
occur_return_type rtntyp id or (occur c) or (occur b1) or (occur b2)
- | RRec (loc,fk,idl,tyl,bv) ->
- (array_exists occur tyl) or
- (not (array_exists (fun id2 -> id=id2) idl) & array_exists occur bv)
+ | RRec (loc,fk,idl,bl,tyl,bv) ->
+ not (array_for_all4 (fun fid bl ty bd ->
+ let rec occur_fix = function
+ [] -> not (occur ty) && (fid=id or not(occur bd))
+ | (na,bbd,bty)::bl ->
+ not (occur bty) &&
+ (match bbd with
+ Some bd -> not (occur bd)
+ | _ -> true) &&
+ (na=Name id or not(occur_fix bl)) in
+ occur_fix bl)
+ idl bl tyl bv)
| RCast (loc,c,t) -> (occur c) or (occur t)
| (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> false
@@ -275,11 +289,17 @@ let rec subst_raw subst raw =
if c' == c & po' == po && b1' == b1 && b2' == b2 then raw else
RIf (loc,c',(na,po'),b1',b2')
- | RRec (loc,fix,ida,ra1,ra2) ->
+ | RRec (loc,fix,ida,bl,ra1,ra2) ->
let ra1' = array_smartmap (subst_raw subst) ra1
and ra2' = array_smartmap (subst_raw subst) ra2 in
- if ra1' == ra1 && ra2' == ra2 then raw else
- RRec (loc,fix,ida,ra1',ra2')
+ let bl' = array_smartmap
+ (list_smartmap (fun (na,obd,ty as dcl) ->
+ let ty' = subst_raw subst ty in
+ let obd' = option_smartmap (subst_raw subst) obd in
+ if ty'==ty & obd'==obd then dcl else (na,obd',ty')))
+ bl in
+ if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else
+ RRec (loc,fix,ida,bl',ra1',ra2')
| RSort _ -> raw
@@ -310,7 +330,7 @@ let loc_of_rawconstr = function
| ROrderedCase (loc,_,_,_,_,_) -> loc
| RLetTuple (loc,_,_,_,_) -> loc
| RIf (loc,_,_,_,_) -> loc
- | RRec (loc,_,_,_,_) -> loc
+ | RRec (loc,_,_,_,_,_) -> loc
| RSort (loc,_) -> loc
| RHole (loc,_) -> loc
| RCast (loc,_,_) -> loc
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 869861ccd7..e5b2a23fe8 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -73,13 +73,15 @@ type rawconstr =
| RLetTuple of loc * name list * (name * rawconstr option) *
rawconstr * rawconstr
| RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
- | RRec of loc * fix_kind * identifier array *
+ | RRec of loc * fix_kind * identifier array * rawdecl list array *
rawconstr array * rawconstr array
| RSort of loc * rawsort
| RHole of (loc * hole_kind)
| RCast of loc * rawconstr * rawconstr
| RDynamic of loc * Dyn.t
+and rawdecl = name * rawconstr option * rawconstr
+
val cases_predicate_names :
(rawconstr * (name * (loc * inductive * name list) option) ref) list ->
name list
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 14482cb7a1..5c792a463b 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -242,12 +242,13 @@ let coerce_to_inductive = function
(* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
let atomic_mactab = ref Idmap.empty
let add_primitive_tactic s tac =
- let id = id_of_string s in
- atomic_mactab := Idmap.add id tac !atomic_mactab
+ (if not !Options.v7 then
+ let id = id_of_string s in
+ atomic_mactab := Idmap.add id tac !atomic_mactab)
let _ =
if not !Options.v7 then
- let nocl = {onhyps=Some[];onconcl=true; concl_occs=[]} in
+ (let nocl = {onhyps=Some[];onconcl=true; concl_occs=[]} in
List.iter
(fun (s,t) -> add_primitive_tactic s (TacAtom((0,0),t)))
[ "red", TacReduce(Red false,nocl);
@@ -266,8 +267,14 @@ let _ =
"constructor", TacAnyConstructor None;
"reflexivity", TacReflexivity;
"symmetry", TacSymmetry nocl
- ]
-
+ ];
+ List.iter
+ (fun (s,t) -> add_primitive_tactic s t)
+ [ "idtac",TacId "";
+ "fail", TacFail(ArgArg 0,"");
+ "fresh", TacArg(TacFreshId None)
+ ])
+
let lookup_atomic id = Idmap.find id !atomic_mactab
let is_atomic id = Idmap.mem id !atomic_mactab
let is_atomic_kn kn =
diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v
new file mode 100644
index 0000000000..270fff4ef2
--- /dev/null
+++ b/test-suite/output/Fixpoint.v
@@ -0,0 +1,7 @@
+Require PolyList.
+
+Check Fix F { F/4 : (A,B:Set)(A->B)->(list A)->(list B) :=
+ [_,_,f,l]Cases l of
+ nil => (nil ?)
+ | (cons a l) => (cons (f a) (F ? ? f l))
+ end}.
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 46de560b46..30548d74d2 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -456,7 +456,8 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list) =
(* Declare the notations for the recursive types pushed in local context*)
let (rec_sign,arityl) =
List.fold_left
- (fun (env,arl) ((recname,_,_,arityc,_),_) ->
+ (fun (env,arl) ((recname,_,bl,arityc,_),_) ->
+ let arityc = prod_rawconstr arityc bl in
let arity = interp_type sigma env0 arityc in
(Environ.push_named (recname,None,arity) env, (arity::arl)))
(env0,[]) lnameargsardef in
@@ -479,7 +480,8 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list) =
(Lib.cwd(),SectionLocalAssum arity, IsAssumption Definitional) in
()) lrecnames arityl;
List.map2
- (fun ((_,_,_,_,def),_) arity ->
+ (fun ((_,_,bl,_,def),_) arity ->
+ let def = abstract_rawconstr def bl in
interp_casted_constr sigma rec_sign def arity)
lnameargsardef arityl
with e ->
@@ -521,14 +523,15 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list) =
Metasyntax.add_notation_interpretation df [] c scope) notations
let build_corecursive lnameardef =
- let lrecnames = List.map (fun (f,_,_) -> f) lnameardef
+ let lrecnames = List.map (fun (f,_,_,_) -> f) lnameardef
and sigma = Evd.empty
and env0 = Global.env() in
let fs = States.freeze() in
let (rec_sign,arityl) =
try
List.fold_left
- (fun (env,arl) (recname,arityc,_) ->
+ (fun (env,arl) (recname,bl,arityc,_) ->
+ let arityc = prod_rawconstr arityc bl in
let arj = type_judgment_of_rawconstr Evd.empty env0 arityc in
let arity = arj.utj_val in
let _ = declare_variable recname
@@ -540,8 +543,10 @@ let build_corecursive lnameardef =
let arityl = List.rev arityl in
let recdef =
try
- List.map (fun (_,arityc,def) ->
- let arity = interp_constr sigma rec_sign arityc in
+ List.map (fun (_,bl,arityc,def) ->
+ let arityc = prod_rawconstr arityc bl in
+ let def = abstract_rawconstr def bl in
+ let arity = interp_constr sigma rec_sign arityc in
interp_casted_constr sigma rec_sign def arity)
lnameardef
with e ->
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 8438e9b02b..f72c533e1e 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -154,7 +154,7 @@ let pr_new_syntax loc ocom =
if !translate_file then
msg (hov 0 (comment (fst loc) ++ com ++ comment (snd loc)))
else
- msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ com));
+ msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
States.unfreeze fs;
Constrintern.set_temporary_implicits_in [];
Constrextern.set_temporary_implicits_out [];
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index b98be6c6c7..2825344e45 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -76,7 +76,7 @@ let pr_notation pr s env =
let pr_delimiters key strm =
strm ++ str ("%"^key)
-let surround p = str"(" ++ p ++ str")"
+let surround p = hov 1 (str"(" ++ p ++ str")")
let pr_located pr ((b,e),x) =
if Options.do_translate() && (b,e)<>dummy_loc then
@@ -350,24 +350,15 @@ let pr_recursive_decl pr id bl annot t c =
pr_opt_type_spc pr t ++ str " :=" ++
pr_sep_com (fun () -> brk(1,2)) (pr ltop) c
-let name_of_binder = function
- | LocalRawAssum (nal,_) -> nal
- | LocalRawDef (_,_) -> []
-
-let pr_fixdecl pr (id,n,_,t0,c0) =
- let (bl,c,t) = extract_def_binders c0 t0 in
- let (bl,t,c) =
- let ids = List.flatten (List.map name_of_binder bl) in
- if List.length ids <= n then split_fix (n+1) t0 c0 else (bl,t,c) in
+let pr_fixdecl pr (id,n,bl,t,c) =
let annot =
- let ids = List.flatten (List.map name_of_binder bl) in
+ let ids = names_of_local_assums bl in
if List.length ids > 1 then
spc() ++ str "{struct " ++ pr_name (snd (List.nth ids n)) ++ str"}"
else mt() in
pr_recursive_decl pr id bl annot t c
-let pr_cofixdecl pr (id,t,c) =
- let (bl,c,t) = extract_def_binders c t in
+let pr_cofixdecl pr (id,bl,t,c) =
pr_recursive_decl pr id bl (mt()) t c
let pr_recursive pr_decl id = function
@@ -588,6 +579,20 @@ let rec pr sep inherited a =
let pr = pr mt
+let rec abstract_constr_expr c = function
+ | [] -> c
+ | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl)
+ | LocalRawAssum (idl,t)::bl ->
+ List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl
+ (abstract_constr_expr c bl)
+
+let rec prod_constr_expr c = function
+ | [] -> c
+ | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl)
+ | LocalRawAssum (idl,t)::bl ->
+ List.fold_right (fun x b -> mkProdC([x],t,b)) idl
+ (prod_constr_expr c bl)
+
let rec strip_context n iscast t =
if n = 0 then
[], if iscast then match t with CCast (_,c,_) -> c | _ -> t else t
@@ -619,12 +624,15 @@ let rec strip_context n iscast t =
LocalRawDef (na,b) :: bl', c
| _ -> anomaly "ppconstrnew: strip_context"
-let transf istype env n iscast c =
+let transf istype env iscast bl c =
+ let c' =
+ if istype then abstract_constr_expr c bl
+ else prod_constr_expr c bl in
if Options.do_translate() then
let r =
Constrintern.for_grammar
(Constrintern.interp_rawconstr_gen istype Evd.empty env false ([],[]))
- c in
+ c' in
begin try
(* Try to infer old case and type annotations *)
let _ = Pretyping.understand_gen_tcc Evd.empty env [] None r in
@@ -634,11 +642,12 @@ let transf istype env n iscast c =
(if istype then Constrextern.extern_rawtype
else Constrextern.extern_rawconstr)
(Termops.vars_of_env env) r in
+ let n = local_binders_length bl in
strip_context n iscast c
- else [], c
+ else bl, c
-let pr_constr_env env c = pr lsimple (snd (transf false env 0 false c))
-let pr_lconstr_env env c = pr ltop (snd (transf false env 0 false c))
+let pr_constr_env env c = pr lsimple (snd (transf false env false [] c))
+let pr_lconstr_env env c = pr ltop (snd (transf false env false [] c))
let pr_constr c = pr_constr_env (Global.env()) c
let pr_lconstr c = pr_lconstr_env (Global.env()) c
@@ -658,10 +667,11 @@ let is_Eval_key c =
let pr_protect_eval c =
if is_Eval_key c then h 0 (str "(" ++ pr ltop c ++ str ")") else pr ltop c
-let pr_lconstr_env_n env n b c =
- let bl, c = transf false env n b c in bl, pr_protect_eval c
-let pr_type_env_n env n c = pr ltop (snd (transf true env n false c))
-let pr_type c = pr ltop (snd (transf true (Global.env()) 0 false c))
+let pr_lconstr_env_n env iscast bl c =
+ let bl, c = transf false env iscast bl c in
+ bl, pr_protect_eval c
+let pr_type_env_n env bl c = pr ltop (snd (transf true env false bl c))
+let pr_type c = pr ltop (snd (transf true (Global.env()) false [] c))
let transf_pattern env c =
if Options.do_translate() then
diff --git a/translate/ppconstrnew.mli b/translate/ppconstrnew.mli
index 542549f74e..2b79c6b71b 100644
--- a/translate/ppconstrnew.mli
+++ b/translate/ppconstrnew.mli
@@ -65,14 +65,17 @@ val pr_constr : constr_expr -> std_ppcmds
val pr_lconstr : constr_expr -> std_ppcmds
val pr_constr_env : env -> constr_expr -> std_ppcmds
val pr_lconstr_env : env -> constr_expr -> std_ppcmds
-val pr_lconstr_env_n : env -> int -> bool -> constr_expr ->
+val pr_lconstr_env_n : env -> bool -> local_binder list -> constr_expr ->
local_binder list * std_ppcmds
-val pr_type_env_n : env -> int -> constr_expr -> std_ppcmds
+val pr_type_env_n : env -> local_binder list -> constr_expr -> std_ppcmds
val pr_type : constr_expr -> std_ppcmds
val pr_cases_pattern : cases_pattern_expr -> std_ppcmds
val pr_may_eval :
('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> ('a,'b) may_eval
-> std_ppcmds
+val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
+val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
+
val pr_rawconstr_env : env -> rawconstr -> std_ppcmds
val pr_lrawconstr_env : env -> rawconstr -> std_ppcmds
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index cfeb12f06c..2fd54a006a 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -259,7 +259,8 @@ let pr_module_vardecls pr_c (idl,mty) =
[make_mbid lib_dir (string_of_id id),
Modintern.interp_modtype (Global.env()) mty]) idl;
(* Builds the stream *)
- spc() ++ str"(" ++ prlist_with_sep spc pr_lident idl ++ str":" ++ m ++ str")"
+ spc() ++
+ hov 1 (str"(" ++ prlist_with_sep spc pr_lident idl ++ str":" ++ m ++ str")")
let pr_module_binders l pr_c =
(* Effet de bord complexe pour garantir la declaration des noms des
@@ -275,7 +276,8 @@ let rec pr_module_expr = function
| CMEapply (me1,(CMEident _ as me2)) ->
pr_module_expr me1 ++ spc() ++ pr_module_expr me2
| CMEapply (me1,me2) ->
- pr_module_expr me1 ++ spc() ++ str"(" ++ pr_module_expr me2 ++ str")"
+ pr_module_expr me1 ++ spc() ++
+ hov 1 (str"(" ++ pr_module_expr me2 ++ str")")
(*
let pr_opt_casted_constr pr_c = function
@@ -285,7 +287,7 @@ let pr_opt_casted_constr pr_c = function
let pr_type_option pr_c = function
| CHole loc -> mt()
- | _ as c -> str":" ++ pr_c c
+ | _ as c -> brk(0,2) ++ str":" ++ pr_c c
let without_translation f x =
let old = Options.do_translate () in
@@ -299,20 +301,6 @@ let pr_decl_notation prc =
str "where " ++ qsnew ntn ++ str " := " ++ without_translation prc c ++
pr_opt (fun sc -> str ": " ++ str sc) scopt)
-let rec abstract_rawconstr c = function
- | [] -> c
- | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_rawconstr c bl)
- | LocalRawAssum (idl,t)::bl ->
- List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl
- (abstract_rawconstr c bl)
-
-let rec prod_rawconstr c = function
- | [] -> c
- | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_rawconstr c bl)
- | LocalRawAssum (idl,t)::bl ->
- List.fold_right (fun x b -> mkProdC([x],t,b)) idl
- (prod_rawconstr c bl)
-
let pr_vbinders l =
hv 0 (pr_binders l)
@@ -320,9 +308,7 @@ let pr_binders_arg =
pr_ne_sep spc pr_binders
let pr_and_type_binders_arg bl =
- let n = local_binders_length bl in
- let c = abstract_rawconstr (CHole dummy_loc) bl in
- let bl, _ = pr_lconstr_env_n (Global.env()) n false c in
+ let bl, _ = pr_lconstr_env_n (Global.env()) false bl (CHole dummy_loc) in
pr_binders_arg bl
let pr_onescheme (id,dep,ind,s) =
@@ -369,7 +355,8 @@ let pr_ne_params_list pr_c l =
match factorize l with
| [p] -> pr_params pr_c p
| l ->
- prlist_with_sep spc (fun p -> str "(" ++ pr_params pr_c p ++ str ")") l
+ prlist_with_sep spc
+ (fun p -> hov 1 (str "(" ++ pr_params pr_c p ++ str ")")) l
(*
prlist_with_sep pr_semicolon (pr_params pr_c)
*)
@@ -403,7 +390,7 @@ let pr_syntax_modifier = function
let pr_syntax_modifiers = function
| [] -> mt()
| l -> spc() ++
- hov 0 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
+ hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
let pr_grammar_tactic_rule (name,(s,pil),t) =
(*
@@ -619,14 +606,10 @@ let rec pr_vernac = function
(bl2,CCast (dummy_loc,body,ty'),
spc() ++ str":" ++
pr_sep_com spc
- (pr_type_env_n (Global.env())
- (local_binders_length bl + local_binders_length bl2))
- (prod_rawconstr ty bl)) in
- let n = local_binders_length bl + local_binders_length bl2 in
+ (pr_type_env_n (Global.env()) (bl@bl2)) ty') in
let iscast = d <> None in
let bindings,ppred =
- pr_lconstr_env_n (Global.env()) n iscast
- (abstract_rawconstr (abstract_rawconstr body bl2) bl) in
+ pr_lconstr_env_n (Global.env()) iscast (bl@bl2) body in
(pr_binders_arg bindings,ty,Some (pr_reduce red ++ ppred))
| ProveBody (bl,t) ->
(pr_and_type_binders_arg bl, str" :" ++ pr_spc_type t, None)
@@ -720,7 +703,7 @@ let rec pr_vernac = function
let pr_constructor (coe,(id,c)) =
hov 2 (pr_lident id ++ str" " ++
(if coe then str":>" else str":") ++
- pr_sep_com spc (pr_type_env_n ind_env_params 0) c) in
+ pr_sep_com spc (pr_type_env_n ind_env_params []) c) in
let pr_constructor_list l = match l with
| [] -> mt()
| _ ->
@@ -754,8 +737,10 @@ let rec pr_vernac = function
let notations =
List.fold_right (fun (_,ntnopt) l -> option_cons ntnopt l) recs [] in
let impl = List.map
- (fun ((recname,_, _, arityc,_),_) ->
- let arity = Constrintern.interp_type sigma env0 arityc in
+ (fun ((recname,_, bl, arityc,_),_) ->
+ let arity =
+ Constrintern.interp_type sigma env0
+ (prod_constr_expr arityc bl) in
let impl_in =
if Impargs.is_implicit_args()
then Impargs.compute_implicits false env0 arity
@@ -776,8 +761,10 @@ let rec pr_vernac = function
let rec_sign =
List.fold_left
- (fun env ((recname,_,_,arityc,_),_) ->
- let arity = Constrintern.interp_type sigma env0 arityc in
+ (fun env ((recname,_,bl,arityc,_),_) ->
+ let arity =
+ Constrintern.interp_type sigma env0
+ (prod_constr_expr arityc bl) in
Environ.push_named (recname,None,arity) env)
(Global.env()) recs in
@@ -785,21 +772,19 @@ let rec pr_vernac = function
| LocalRawAssum (nal,_) -> nal
| LocalRawDef (_,_) -> [] in
let pr_onerec = function
- | (id,n,_,type_0,def0),ntn ->
- let (bl,def,type_) = extract_def_binders def0 type_0 in
- let ids = List.flatten (List.map name_of_binder bl) in
- let (bl,def,type_) =
- if List.length ids <= n then split_fix (n+1) def0 type_0
- else (bl,def,type_) in
+ | (id,n,bl,type_,def),ntn ->
let ids = List.flatten (List.map name_of_binder bl) in
+ let name =
+ try snd (List.nth ids n)
+ with Failure _ ->
+ warn (str "non-printable fixpoint \""++pr_id id++str"\"");
+ Anonymous in
let annot =
if List.length ids > 1 then
- spc() ++ str "{struct " ++
- pr_name (snd (List.nth ids n)) ++ str"}"
+ spc() ++ str "{struct " ++ pr_name name ++ str"}"
else mt() in
- let bl, ppc =
- pr_lconstr_env_n rec_sign (local_binders_length bl)
- true (abstract_rawconstr (CCast (dummy_loc,def,type_)) bl) in
+ let bl,ppc =
+ pr_lconstr_env_n rec_sign true bl (CCast(dummy_loc,def,type_)) in
pr_id id ++ pr_binders_arg bl ++ annot ++ spc()
++ pr_type_option (fun c -> spc() ++ pr_type c) type_
++ str" :=" ++ brk(1,1) ++ ppc ++
@@ -809,8 +794,7 @@ let rec pr_vernac = function
prlist_with_sep (fun _ -> fnl() ++ fnl() ++ str"with ") pr_onerec recs)
| VernacCoFixpoint corecs ->
- let pr_onecorec (id,c,def) =
- let (bl,def,c) = extract_def_binders def c in
+ let pr_onecorec (id,bl,c,def) =
pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
spc() ++ pr_type c ++
str" :=" ++ brk(1,1) ++ pr_lconstr def in
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 08:30:58 +0000