summaryrefslogtreecommitdiff
path: root/interp/topconstr.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /interp/topconstr.ml
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'interp/topconstr.ml')
-rw-r--r--interp/topconstr.ml269
1 files changed, 180 insertions, 89 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index af147866..b858eecb 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: topconstr.ml 9976 2007-07-12 11:58:30Z msozeau $ *)
+(* $Id: topconstr.ml 11024 2008-05-30 12:41:39Z msozeau $ *)
(*i*)
open Pp
@@ -37,11 +37,14 @@ type aconstr =
| ALambda of name * aconstr * aconstr
| AProd of name * aconstr * aconstr
| ALetIn of name * aconstr * aconstr
- | ACases of aconstr option *
+ | ACases of case_style * aconstr option *
(aconstr * (name * (inductive * int * name list) option)) list *
(cases_pattern list * aconstr) list
| ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
| AIf of aconstr * (name * aconstr option) * aconstr * aconstr
+ | ARec of fix_kind * identifier array *
+ (name * aconstr option * aconstr) list array * aconstr array *
+ aconstr array
| ASort of rawsort
| AHole of Evd.hole_kind
| APatVar of patvar
@@ -74,12 +77,12 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
let outerl = (ldots_var,inner)::(if swap then [x,RVar(loc,y)] else []) in
subst_rawvars outerl it
| ALambda (na,ty,c) ->
- let e,na = name_fold_map g e na in RLambda (loc,na,f e ty,f e c)
+ let e,na = name_fold_map g e na in RLambda (loc,na,Explicit,f e ty,f e c)
| AProd (na,ty,c) ->
- let e,na = name_fold_map g e na in RProd (loc,na,f e ty,f e c)
+ let e,na = name_fold_map g e na in RProd (loc,na,Explicit,f e ty,f e c)
| ALetIn (na,b,c) ->
let e,na = name_fold_map g e na in RLetIn (loc,na,f e b,f e c)
- | ACases (rtntypopt,tml,eqnl) ->
+ | ACases (sty,rtntypopt,tml,eqnl) ->
let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
let e',t' = match t with
| None -> e',None
@@ -94,14 +97,20 @@ 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,option_map (f e') rtntypopt,tml',eqnl')
+ RCases (loc,sty,Option.map (f e') rtntypopt,tml',eqnl')
| ALetTuple (nal,(na,po),b,c) ->
let e,nal = list_fold_map (name_fold_map g) e nal in
let e,na = name_fold_map g e na in
- RLetTuple (loc,nal,(na,option_map (f e) po),f e b,f e c)
+ RLetTuple (loc,nal,(na,Option.map (f e) po),f e b,f e c)
| AIf (c,(na,po),b1,b2) ->
let e,na = name_fold_map g e na in
- RIf (loc,f e c,(na,option_map (f e) po),f e b1,f e b2)
+ RIf (loc,f e c,(na,Option.map (f e) po),f e b1,f e b2)
+ | ARec (fk,idl,dll,tl,bl) ->
+ let e,idl = array_fold_map g e idl in
+ let e,dll = array_fold_map (list_fold_map (fun e (na,oc,b) ->
+ let e,na = name_fold_map g e na in
+ (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
+ RRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e) bl)
| ACast (c,k) -> RCast (loc,f e c,
match k with
| CastConv (k,t) -> CastConv (k,f e t)
@@ -131,9 +140,9 @@ let compare_rawconstr f t1 t2 = match t1,t2 with
| RRef (_,r1), RRef (_,r2) -> r1 = r2
| RVar (_,v1), RVar (_,v2) -> v1 = v2
| RApp (_,f1,l1), RApp (_,f2,l2) -> f f1 f2 & List.for_all2 f l1 l2
- | RLambda (_,na1,ty1,c1), RLambda (_,na2,ty2,c2) when na1 = na2 ->
+ | RLambda (_,na1,bk1,ty1,c1), RLambda (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 ->
f ty1 ty2 & f c1 c2
- | RProd (_,na1,ty1,c1), RProd (_,na2,ty2,c2) when na1 = na2 ->
+ | RProd (_,na1,bk1,ty1,c1), RProd (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 ->
f ty1 ty2 & f c1 c2
| RHole _, RHole _ -> true
| RSort (_,s1), RSort (_,s2) -> s1 = s2
@@ -180,25 +189,32 @@ let aconstr_and_vars_of_rawconstr a =
found := ldots_var :: !found; assert lassoc;
AList (x,y,AApp (AVar ldots_var,[AVar x]),aux t,lassoc)
| RApp (_,g,args) -> AApp (aux g, List.map aux args)
- | RLambda (_,na,ty,c) -> add_name found na; ALambda (na,aux ty,aux c)
- | RProd (_,na,ty,c) -> add_name found na; AProd (na,aux ty,aux c)
+ | 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 (_,rtntypopt,tml,eqnl) ->
+ | RCases (_,sty,rtntypopt,tml,eqnl) ->
let f (_,idl,pat,rhs) = found := idl@(!found); (pat,aux rhs) in
- ACases (option_map aux rtntypopt,
+ ACases (sty,Option.map aux rtntypopt,
List.map (fun (tm,(na,x)) ->
add_name found na;
- option_iter
+ Option.iter
(fun (_,_,_,nl) -> List.iter (add_name found) nl) x;
- (aux tm,(na,option_map (fun (_,ind,n,nal) -> (ind,n,nal)) x))) tml,
+ (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) ->
add_name found na;
List.iter (add_name found) nal;
- ALetTuple (nal,(na,option_map aux po),aux b,aux c)
+ ALetTuple (nal,(na,Option.map aux po),aux b,aux c)
| RIf (loc,c,(na,po),b1,b2) ->
add_name found na;
- AIf (aux c,(na,option_map aux po),aux b1,aux b2)
+ AIf (aux c,(na,Option.map aux po),aux b1,aux b2)
+ | RRec (_,fk,idl,dll,tl,bl) ->
+ Array.iter (fun id -> found := 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,
match k with CastConv (k,t) -> CastConv (k,aux t)
| CastCoerce -> CastCoerce)
@@ -206,9 +222,8 @@ let aconstr_and_vars_of_rawconstr a =
| RHole (_,w) -> AHole w
| RRef (_,r) -> ARef r
| RPatVar (_,(_,n)) -> APatVar n
- | RDynamic _ | RRec _ | REvar _ ->
- error "Fixpoints, cofixpoints, existential variables and pattern-matching not \
-allowed in abbreviatable expressions"
+ | RDynamic _ | REvar _ ->
+ error "Existential variables not allowed in notations"
(* Recognizing recursive notations *)
and terminator_of_pat f1 ll1 lr1 = function
@@ -304,12 +319,12 @@ let rec subst_aconstr subst bound raw =
if r1' == r1 && r2' == r2 then raw else
ALetIn (n,r1',r2')
- | ACases (rtntypopt,rl,branches) ->
- let rtntypopt' = option_smartmap (subst_aconstr subst bound) rtntypopt
+ | ACases (sty,rtntypopt,rl,branches) ->
+ let rtntypopt' = Option.smartmap (subst_aconstr subst bound) rtntypopt
and rl' = list_smartmap
(fun (a,(n,signopt) as x) ->
let a' = subst_aconstr subst bound a in
- let signopt' = option_map (fun ((indkn,i),n,nal as z) ->
+ let signopt' = Option.map (fun ((indkn,i),n,nal as z) ->
let indkn' = subst_kn subst indkn in
if indkn == indkn' then z else ((indkn',i),n,nal)) signopt in
if a' == a && signopt' == signopt then x else (a',(n,signopt')))
@@ -324,23 +339,34 @@ let rec subst_aconstr subst bound raw =
in
if rtntypopt' == rtntypopt && rtntypopt == rtntypopt' &
rl' == rl && branches' == branches then raw else
- ACases (rtntypopt',rl',branches')
+ ACases (sty,rtntypopt',rl',branches')
| ALetTuple (nal,(na,po),b,c) ->
- let po' = option_smartmap (subst_aconstr subst bound) po
+ let po' = Option.smartmap (subst_aconstr subst bound) po
and b' = subst_aconstr subst bound b
and c' = subst_aconstr subst bound c in
if po' == po && b' == b && c' == c then raw else
ALetTuple (nal,(na,po'),b',c')
| AIf (c,(na,po),b1,b2) ->
- let po' = option_smartmap (subst_aconstr subst bound) po
+ let po' = Option.smartmap (subst_aconstr subst bound) po
and b1' = subst_aconstr subst bound b1
and b2' = subst_aconstr subst bound b2
and c' = subst_aconstr subst bound c in
if po' == po && b1' == b1 && b2' == b2 && c' == c then raw else
AIf (c',(na,po'),b1',b2')
+ | ARec (fk,idl,dll,tl,bl) ->
+ let dll' =
+ array_smartmap (list_smartmap (fun (na,oc,b as x) ->
+ let oc' = Option.smartmap (subst_aconstr subst bound) oc in
+ let b' = subst_aconstr subst bound b in
+ if oc' == oc && b' == b then x else (na,oc',b'))) dll in
+ let tl' = array_smartmap (subst_aconstr subst bound) tl in
+ let bl' = array_smartmap (subst_aconstr subst bound) bl in
+ if dll' == dll && tl' == tl && bl' == bl then raw else
+ ARec (fk,idl,dll',tl',bl')
+
| APatVar _ | ASort _ -> raw
| AHole (Evd.ImplicitArg (ref,i)) ->
@@ -348,7 +374,8 @@ let rec subst_aconstr subst bound raw =
if ref' == ref then raw else
AHole (Evd.InternalHole)
| AHole (Evd.BinderType _ | Evd.QuestionMark _ | Evd.CasesType
- | Evd.InternalHole | Evd.TomatchTypeParameter _) -> raw
+ | Evd.InternalHole | Evd.TomatchTypeParameter _ | Evd.GoalEvar
+ | Evd.ImpossibleCase) -> raw
| ACast (r1,k) ->
match k with
@@ -362,13 +389,15 @@ let rec subst_aconstr subst bound raw =
if r1' == r1 then raw else
ACast (r1',CastCoerce)
+let subst_interpretation subst (metas,pat) =
+ (metas,subst_aconstr subst (List.map fst metas) pat)
let encode_list_value l = RApp (dummy_loc,RVar (dummy_loc,ldots_var),l)
(* Pattern-matching rawconstr and aconstr *)
let abstract_return_type_context pi mklam tml rtno =
- option_map (fun rtn ->
+ Option.map (fun rtn ->
let nal =
List.flatten (List.map (fun (_,(na,t)) ->
match t with Some x -> (pi x)@[na] | None -> [na]) tml) in
@@ -377,7 +406,7 @@ let abstract_return_type_context pi mklam tml rtno =
let abstract_return_type_context_rawconstr =
abstract_return_type_context (fun (_,_,_,nal) -> nal)
- (fun na c -> RLambda(dummy_loc,na,RHole(dummy_loc,Evd.InternalHole),c))
+ (fun na c -> RLambda(dummy_loc,na,Explicit,RHole(dummy_loc,Evd.InternalHole),c))
let abstract_return_type_context_aconstr =
abstract_return_type_context pi3
@@ -409,6 +438,14 @@ let bind_env alp sigma var v =
(* TODO: handle the case of multiple occs in different scopes *)
(var,v)::sigma
+let match_fix_kind fk1 fk2 =
+ match (fk1,fk2) with
+ | RCoFix n1, RCoFix n2 -> n1 = n2
+ | RFix (nl1,n1), RFix (nl2,n2) ->
+ n1 = n2 &&
+ array_for_all2 (fun (n1,_) (n2,_) -> n2 = None || n1 = n2) nl1 nl2
+ | _ -> false
+
let match_opt f sigma t1 t2 = match (t1,t2) with
| None, None -> sigma
| Some t1, Some t2 -> f sigma t1 t2
@@ -435,29 +472,34 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
| RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma
| RRef (_,r1), ARef r2 when r1 = r2 -> sigma
| RPatVar (_,(_,n1)), APatVar n2 when n1=n2 -> sigma
- | RApp (_,f1,l1), AApp (f2,l2) when List.length l1 = List.length l2 ->
+ | RApp (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
+ else f1,l1, f2, l2 in
List.fold_left2 (match_ alp metas) (match_ alp metas sigma f1 f2) l1 l2
| RApp (_,f1,l1), AList (x,_,(AApp (f2,l2) as iter),termin,lassoc)
when List.length l1 = List.length l2 ->
match_alist alp metas sigma (f1::l1) (f2::l2) x iter termin lassoc
- | RLambda (_,na1,t1,b1), ALambda (na2,t2,b2) ->
+ | 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) ->
+ | 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 (_,rtno1,tml1,eqnl1), ACases (rtno2,tml2,eqnl2)
- when List.length tml1 = List.length tml2
+ | RCases (_,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 rtno2' = abstract_return_type_context_aconstr tml2 rtno2 in
- let sigma = option_fold_left2 (match_ alp metas) sigma rtno1' rtno2' in
+ let sigma = Option.fold_left2 (match_ alp metas) sigma rtno1' rtno2' 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
- | 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]
| RLetTuple (_,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
@@ -465,6 +507,22 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
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)
+ 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
+ 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 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) ->
@@ -530,7 +588,9 @@ let match_aconstr c (metas_scl,pat) =
type notation = string
-type explicitation = ExplByPos of int | ExplByName of identifier
+type explicitation = ExplByPos of int * identifier option | ExplByName of identifier
+
+type binder_kind = Default of binding_kind | TypeClass of binding_kind
type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
@@ -550,22 +610,22 @@ type constr_expr =
| CFix of loc * identifier located * fixpoint_expr list
| CCoFix of loc * identifier located * cofixpoint_expr list
| CArrow of loc * constr_expr * constr_expr
- | CProdN of loc * (name located list * constr_expr) list * constr_expr
- | CLambdaN of loc * (name located list * constr_expr) list * constr_expr
+ | CProdN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
+ | CLambdaN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
| CLetIn of loc * name located * constr_expr * constr_expr
| CAppExpl of loc * (proj_flag * reference) * constr_expr list
| CApp of loc * (proj_flag * constr_expr) *
(constr_expr * explicitation located option) list
- | CCases of loc * constr_expr option *
+ | CCases of loc * case_style * constr_expr option *
(constr_expr * (name option * constr_expr option)) list *
- (loc * cases_pattern_expr list list * constr_expr) list
+ (loc * cases_pattern_expr list located list * constr_expr) list
| CLetTuple of loc * name list * (name option * constr_expr option) *
constr_expr * constr_expr
| CIf of loc * constr_expr * (name option * constr_expr option)
* constr_expr * constr_expr
- | CHole of loc
+ | CHole of loc * Evd.hole_kind option
| CPatVar of loc * (bool * patvar)
- | CEvar of loc * existential_key
+ | CEvar of loc * existential_key * constr_expr list option
| CSort of loc * rawsort
| CCast of loc * constr_expr * constr_expr cast_type
| CNotation of loc * notation * constr_expr list
@@ -573,16 +633,19 @@ type constr_expr =
| CDelimiters of loc * string * constr_expr
| CDynamic of loc * Dyn.t
-
and fixpoint_expr =
- identifier * (int option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
+ identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
and local_binder =
| LocalRawDef of name located * constr_expr
- | LocalRawAssum of name located list * constr_expr
+ | LocalRawAssum of name located list * binder_kind * constr_expr
+
+and typeclass_constraint = name located * binding_kind * constr_expr
+
+and typeclass_context = typeclass_constraint list
and cofixpoint_expr =
- identifier * local_binder list * constr_expr * constr_expr
+ identifier located * local_binder list * constr_expr * constr_expr
and recursion_order_expr =
| CStructRec
@@ -592,21 +655,23 @@ and recursion_order_expr =
(***********************)
(* For binders parsing *)
+let default_binder_kind = Default Explicit
+
let rec local_binders_length = function
| [] -> 0
| LocalRawDef _::bl -> 1 + local_binders_length bl
- | LocalRawAssum (idl,_)::bl -> List.length idl + local_binders_length bl
+ | LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl
let rec local_assums_length = function
| [] -> 0
| LocalRawDef _::bl -> local_binders_length bl
- | LocalRawAssum (idl,_)::bl -> List.length idl + 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)
+ List.flatten (List.map (function LocalRawAssum(l,_,_)->l|_->[]) bl)
let names_of_local_binders bl =
- List.flatten (List.map (function LocalRawAssum(l,_)->l|LocalRawDef(l,_)->[l]) bl)
+ List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]) bl)
(**********************************************************************)
(* Functions on constr_expr *)
@@ -622,12 +687,12 @@ let constr_loc = function
| CLetIn (loc,_,_,_) -> loc
| CAppExpl (loc,_,_) -> loc
| CApp (loc,_,_) -> loc
- | CCases (loc,_,_,_) -> loc
+ | CCases (loc,_,_,_,_) -> loc
| CLetTuple (loc,_,_,_,_) -> loc
| CIf (loc,_,_,_,_) -> loc
- | CHole loc -> loc
+ | CHole (loc, _) -> loc
| CPatVar (loc,_) -> loc
- | CEvar (loc,_) -> loc
+ | CEvar (loc,_,_) -> loc
| CSort (loc,_) -> loc
| CCast (loc,_,_) -> loc
| CNotation (loc,_,_) -> loc
@@ -663,8 +728,8 @@ let ids_of_cases_indtype =
let ids_of_cases_tomatch tms =
List.fold_right
(fun (_,(ona,indnal)) l ->
- option_fold_right (fun t -> (@) (ids_of_cases_indtype t))
- indnal (option_fold_right name_cons ona l))
+ Option.fold_right (fun t -> (@) (ids_of_cases_indtype t))
+ indnal (Option.fold_right name_cons ona l))
tms []
let is_constructor id =
@@ -680,11 +745,13 @@ let rec cases_pattern_fold_names f a = function
| CPatPrim _ | CPatAtom _ -> a
let ids_of_pattern_list =
- List.fold_left (List.fold_left (cases_pattern_fold_names Idset.add))
+ List.fold_left
+ (located_fold_left
+ (List.fold_left (cases_pattern_fold_names Idset.add)))
Idset.empty
let rec fold_constr_expr_binders g f n acc b = function
- | (nal,t)::l ->
+ | (nal,bk,t)::l ->
let nal = snd (List.split nal) in
let n' = List.fold_right (name_fold g) nal n in
f n (fold_constr_expr_binders g f n' acc b l) t
@@ -692,7 +759,7 @@ let rec fold_constr_expr_binders g f n acc b = function
f n acc b
let rec fold_local_binders g f n acc b = function
- | LocalRawAssum (nal,t)::l ->
+ | LocalRawAssum (nal,bk,t)::l ->
let nal = snd (List.split nal) in
let n' = List.fold_right (name_fold g) nal n in
f n (fold_local_binders g f n' acc b l) t
@@ -706,28 +773,28 @@ let fold_constr_expr_with_binders g f n acc = function
| CAppExpl (loc,(_,_),l) -> List.fold_left (f n) acc l
| CApp (loc,(_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l)
| CProdN (_,l,b) | CLambdaN (_,l,b) -> fold_constr_expr_binders g f n acc b l
- | CLetIn (_,na,a,b) -> fold_constr_expr_binders g f n acc b [[na],a]
+ | CLetIn (_,na,a,b) -> fold_constr_expr_binders g f n acc b [[na],default_binder_kind,a]
| CCast (loc,a,CastConv(_,b)) -> f n (f n acc a) b
| CCast (loc,a,CastCoerce) -> f n acc a
| CNotation (_,_,l) -> List.fold_left (f n) acc l
| CDelimiters (loc,_,a) -> f n acc a
| CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _ | CRef _ ->
acc
- | CCases (loc,rtnpo,al,bl) ->
+ | CCases (loc,sty,rtnpo,al,bl) ->
let ids = ids_of_cases_tomatch al in
- let acc = option_fold_left (f (List.fold_right g ids n)) acc rtnpo in
+ let acc = Option.fold_left (f (List.fold_right g ids n)) acc rtnpo in
let acc = List.fold_left (f n) acc (List.map fst al) in
List.fold_right (fun (loc,patl,rhs) acc ->
let ids = ids_of_pattern_list patl in
f (Idset.fold g ids n) acc rhs) bl acc
| CLetTuple (loc,nal,(ona,po),b,c) ->
let n' = List.fold_right (name_fold g) nal n in
- f (option_fold_right (name_fold g) ona n') (f n acc b) c
+ f (Option.fold_right (name_fold g) ona n') (f n acc b) c
| CIf (_,c,(ona,po),b1,b2) ->
let acc = f n (f n (f n acc b1) b2) c in
- option_fold_left (f (option_fold_right (name_fold g) ona n)) acc po
+ Option.fold_left (f (Option.fold_right (name_fold g) ona n)) acc po
| CFix (loc,_,l) ->
- let n' = List.fold_right (fun (id,_,_,_,_) -> g id) l n in
+ let n' = List.fold_right (fun ((_,id),_,_,_,_) -> g id) l n in
List.fold_right (fun (_,(_,o),lb,t,c) acc ->
fold_local_binders g f n'
(fold_local_binders g f n acc t lb) c lb) l acc
@@ -746,22 +813,40 @@ let mkIdentC id = CRef (Ident (dummy_loc, id))
let mkRefC r = CRef r
let mkAppC (f,l) = CApp (dummy_loc, (None,f), List.map (fun x -> (x,None)) l)
let mkCastC (a,k) = CCast (dummy_loc,a,k)
-let mkLambdaC (idl,a,b) = CLambdaN (dummy_loc,[idl,a],b)
+let mkLambdaC (idl,bk,a,b) = CLambdaN (dummy_loc,[idl,bk,a],b)
let mkLetInC (id,a,b) = CLetIn (dummy_loc,id,a,b)
-let mkProdC (idl,a,b) = CProdN (dummy_loc,[idl,a],b)
+let mkProdC (idl,bk,a,b) = CProdN (dummy_loc,[idl,bk,a],b)
+
+let rec mkCProdN loc bll c =
+ match bll with
+ | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
+ CProdN (loc,[idl,bk,t],mkCProdN (join_loc loc1 loc) bll c)
+ | LocalRawDef ((loc1,_) as id,b) :: bll ->
+ CLetIn (loc,id,b,mkCProdN (join_loc loc1 loc) bll c)
+ | [] -> c
+ | LocalRawAssum ([],_,_) :: bll -> mkCProdN loc bll c
+
+let rec mkCLambdaN loc bll c =
+ match bll with
+ | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
+ CLambdaN (loc,[idl,bk,t],mkCLambdaN (join_loc loc1 loc) bll c)
+ | LocalRawDef ((loc1,_) as id,b) :: bll ->
+ CLetIn (loc,id,b,mkCLambdaN (join_loc loc1 loc) bll c)
+ | [] -> c
+ | LocalRawAssum ([],_,_) :: bll -> mkCLambdaN loc bll c
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
+ | LocalRawAssum (idl,bk,t)::bl ->
+ List.fold_right (fun x b -> mkLambdaC([x],bk,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
+ | LocalRawAssum (idl,bk,t)::bl ->
+ List.fold_right (fun x b -> mkProdC([x],bk,t,b)) idl
(prod_constr_expr c bl)
let coerce_to_id = function
@@ -776,15 +861,15 @@ 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 (e,bl) (nal,t) = (map_binder g e nal,(nal,f e t)::bl) in
+ let h (e,bl) (nal,bk,t) = (map_binder g e nal,(nal,bk,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)
+ LocalRawAssum(nal,k,ty) ->
+ (map_binder g e nal, LocalRawAssum(nal,k,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
@@ -806,32 +891,32 @@ let map_constr_expr_with_binders g f e = function
| CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a)
| CHole _ | CEvar _ | CPatVar _ | CSort _
| CPrim _ | CDynamic _ | CRef _ as x -> x
- | CCases (loc,rtnpo,a,bl) ->
+ | CCases (loc,sty,rtnpo,a,bl) ->
(* TODO: apply g on the binding variables in pat... *)
let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in
let ids = ids_of_cases_tomatch a in
- let po = option_map (f (List.fold_right g ids e)) rtnpo in
- CCases (loc, po, List.map (fun (tm,x) -> (f e tm,x)) a,bl)
+ let po = Option.map (f (List.fold_right g ids e)) rtnpo in
+ CCases (loc, sty, po, List.map (fun (tm,x) -> (f e tm,x)) a,bl)
| CLetTuple (loc,nal,(ona,po),b,c) ->
let e' = List.fold_right (name_fold g) nal e in
- let e'' = option_fold_right (name_fold g) ona e in
- CLetTuple (loc,nal,(ona,option_map (f e'') po),f e b,f e' c)
+ let e'' = Option.fold_right (name_fold g) ona e in
+ CLetTuple (loc,nal,(ona,Option.map (f e'') po),f e b,f e' c)
| CIf (loc,c,(ona,po),b1,b2) ->
- let e' = option_fold_right (name_fold g) ona e in
- CIf (loc,f e c,(ona,option_map (f e') po),f e b1,f e b2)
+ let e' = Option.fold_right (name_fold g) ona e in
+ CIf (loc,f e c,(ona,Option.map (f e') po),f e b1,f e b2)
| CFix (loc,id,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 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,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 e'' = List.fold_left (fun e ((_,id),_,_,_) -> g id e) e' dl in
let d' = f e'' d in
(id,bl',t',d')) dl)
@@ -849,10 +934,16 @@ type with_declaration_ast =
| CWith_Module of identifier list located * qualid located
| CWith_Definition of identifier list located * constr_expr
-type module_type_ast =
- | CMTEident of qualid located
- | CMTEwith of module_type_ast * with_declaration_ast
type module_ast =
| CMEident of qualid located
| CMEapply of module_ast * module_ast
+
+type module_type_ast =
+ | CMTEident of qualid located
+ | CMTEapply of module_type_ast * module_ast
+ | CMTEwith of module_type_ast * with_declaration_ast
+
+type include_ast =
+ | CIMTE of module_type_ast
+ | CIME of module_ast