aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/topconstr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/topconstr.ml')
-rw-r--r--interp/topconstr.ml101
1 files changed, 80 insertions, 21 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 5b1d2813b..d2ef146bf 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -28,9 +28,11 @@ type aconstr =
| ALambda of name * aconstr * aconstr
| AProd of name * aconstr * aconstr
| ALetIn of name * aconstr * aconstr
- | ACases of aconstr option * aconstr list *
+ | ACases of aconstr option * aconstr option *
+ (aconstr * (name * (inductive * name list) option)) list *
(identifier list * cases_pattern list * aconstr) list
| AOrderedCase of case_style * aconstr option * aconstr * aconstr array
+ | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
| ASort of rawsort
| AHole of hole_kind
| APatVar of patvar
@@ -49,13 +51,24 @@ let map_aconstr_with_binders_loc loc g f e = function
let na,e = name_app g e na in RProd (loc,na,f e ty,f e c)
| ALetIn (na,b,c) ->
let na,e = name_app g e na in RLetIn (loc,na,f e b,f e c)
- | ACases (tyopt,tml,eqnl) ->
+ | ACases (tyopt,rtntypopt,tml,eqnl) ->
+ let cases_predicate_names tml =
+ List.flatten (List.map (function
+ | (tm,(na,None)) -> [na]
+ | (tm,(na,Some (_,nal))) -> na::nal) tml) in
+ (* TODO: apply g to na (in fact not used) *)
+ let e' = List.fold_right
+ (fun na e -> snd (name_app g e na)) (cases_predicate_names tml) e in
let fold id (idl,e) = let (id,e) = g id e in (id::idl,e) in
let eqnl = List.map (fun (idl,pat,rhs) ->
let (idl,e) = List.fold_right fold idl ([],e) in (loc,idl,pat,f e rhs)) eqnl in
- RCases (loc,option_app (f e) tyopt,List.map (f e) tml,eqnl)
+ RCases (loc,(option_app (f e) tyopt, ref (option_app (f e') rtntypopt)),
+ List.map (fun (tm,(na,x)) ->
+ (f e tm,ref (na,option_app (fun (x,y) -> (loc,x,y)) x))) tml,eqnl)
| AOrderedCase (b,tyopt,tm,bv) ->
- ROrderedCase (loc,b,option_app (f e) tyopt,f e tm,Array.map (f e) bv)
+ ROrderedCase (loc,b,option_app (f e) tyopt,f e tm,Array.map (f e) bv,ref None)
+ | ALetTuple (nal,(na,po),b,c) ->
+ RLetTuple (loc,nal,(na,option_app (f e) po),f e b,f e c)
| ACast (c,t) -> RCast (loc,f e c,f e t)
| ASort x -> RSort (loc,x)
| AHole x -> RHole (loc,x)
@@ -101,9 +114,17 @@ let rec subst_aconstr subst raw =
if r1' == r1 && r2' == r2 then raw else
ALetIn (n,r1',r2')
- | ACases (ro,rl,branches) ->
+ | ACases (ro,rtntypopt,rl,branches) ->
let ro' = option_smartmap (subst_aconstr subst) ro
- and rl' = list_smartmap (subst_aconstr subst) rl
+ and rtntypopt' = option_smartmap (subst_aconstr subst) rtntypopt
+ and rl' = list_smartmap
+ (fun (a,(n,signopt) as x) ->
+ let a' = subst_aconstr subst a in
+ let signopt' = option_app (fun ((indkn,i),nal as z) ->
+ let indkn' = subst_kn subst indkn in
+ if indkn == indkn' then z else ((indkn',i),nal)) signopt in
+ if a' == a && signopt' == signopt then x else (a',(n,signopt')))
+ rl
and branches' = list_smartmap
(fun (idl,cpl,r as branch) ->
let cpl' = list_smartmap (subst_pat subst) cpl
@@ -112,8 +133,9 @@ let rec subst_aconstr subst raw =
(idl,cpl',r'))
branches
in
- if ro' == ro && rl' == rl && branches' == branches then raw else
- ACases (ro',rl',branches')
+ if ro' == ro && rtntypopt == rtntypopt' &
+ rl' == rl && branches' == branches then raw else
+ ACases (ro',rtntypopt',rl',branches')
| AOrderedCase (b,ro,r,ra) ->
let ro' = option_smartmap (subst_aconstr subst) ro
@@ -122,6 +144,13 @@ let rec subst_aconstr subst raw =
if ro' == ro && r' == r && ra' == ra then raw else
AOrderedCase (b,ro',r',ra')
+ | ALetTuple (nal,(na,po),b,c) ->
+ let po' = option_smartmap (subst_aconstr subst) po
+ and b' = subst_aconstr subst b
+ and c' = subst_aconstr subst c in
+ if po' == po && b' == b && c' == c then raw else
+ ALetTuple (nal,(na,po'),b',c')
+
| APatVar _ | ASort _ -> raw
| AHole (ImplicitArg (ref,i)) ->
@@ -151,13 +180,22 @@ let aconstr_of_rawconstr vars a =
| RLambda (_,na,ty,c) -> add_name bound_binders na; ALambda (na,aux ty,aux c)
| RProd (_,na,ty,c) -> add_name bound_binders na; AProd (na,aux ty,aux c)
| RLetIn (_,na,b,c) -> add_name bound_binders na; ALetIn (na,aux b,aux c)
- | RCases (_,tyopt,tml,eqnl) ->
+ | RCases (_,(tyopt,rtntypopt),tml,eqnl) ->
let f (_,idl,pat,rhs) =
bound_binders := idl@(!bound_binders);
(idl,pat,aux rhs) in
- ACases (option_app aux tyopt,List.map aux tml, List.map f eqnl)
- | ROrderedCase (_,b,tyopt,tm,bv) ->
+ ACases (option_app aux tyopt,
+ option_app aux !rtntypopt,
+ List.map (fun (tm,{contents = (na,x)}) ->
+ add_name bound_binders na;
+ option_iter
+ (fun (_,_,nl) -> List.iter (add_name bound_binders) nl) x;
+ (aux tm,(na,option_app (fun (_,ind,nal) -> (ind,nal)) x))) tml,
+ List.map f eqnl)
+ | ROrderedCase (_,b,tyopt,tm,bv,_) ->
AOrderedCase (b,option_app aux tyopt,aux tm, Array.map aux bv)
+ | RLetTuple (loc,nal,(na,po),b,c) ->
+ ALetTuple (nal,(na,option_app aux po),aux b,aux c)
| RCast (_,c,t) -> ACast (aux c,aux t)
| RSort (_,s) -> ASort s
| RHole (_,w) -> AHole w
@@ -279,11 +317,13 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
match_binders alp metas (match_ alp metas sigma t1 t2) b1 b2 na1 na2
| RLetIn (_,na1,t1,b1), AProd (na2,t2,b2) ->
match_binders alp metas (match_ alp metas sigma t1 t2) b1 b2 na1 na2
- | RCases (_,po1,tml1,eqnl1), ACases (po2,tml2,eqnl2) ->
+ | RCases (_,(po1,rtno1),tml1,eqnl1), ACases (po2,rtno2,tml2,eqnl2) ->
let sigma = option_fold_left2 (match_ alp metas) sigma po1 po2 in
- let sigma = List.fold_left2 (match_ alp metas) sigma tml1 tml2 in
+ (* TODO: match rtno' with their contexts *)
+ 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
- | ROrderedCase (_,st,po1,c1,bl1), AOrderedCase (st2,po2,c2,bl2) ->
+ | ROrderedCase (_,st,po1,c1,bl1,_), AOrderedCase (st2,po2,c2,bl2) ->
let sigma = option_fold_left2 (match_ alp metas) sigma po1 po2 in
array_fold_left2 (match_ alp metas) (match_ alp metas sigma c1 c2) bl1 bl2
| RCast(_,c1,t1), ACast(c2,t2) ->
@@ -349,7 +389,7 @@ type notation = string
type explicitation = int
-type proj_flag = bool (* [true] = is projection *)
+type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
type cases_pattern_expr =
| CPatAlias of loc * cases_pattern_expr * identifier
@@ -369,10 +409,13 @@ type constr_expr =
| CAppExpl of loc * (proj_flag * reference) * constr_expr list
| CApp of loc * (proj_flag * constr_expr) *
(constr_expr * explicitation option) list
- | CCases of loc * constr_expr option * constr_expr list *
+ | CCases of loc * (constr_expr option * constr_expr option) *
+ (constr_expr * (name * (loc * reference * name list) option)) list *
(loc * cases_pattern_expr list * constr_expr) list
| COrderedCase of loc * case_style * constr_expr option * constr_expr
* constr_expr list
+ | CLetTuple of loc * name list * (name * constr_expr option) *
+ constr_expr * constr_expr
| CHole of loc
| CPatVar of loc * (bool * patvar)
| CEvar of loc * existential_key
@@ -410,6 +453,7 @@ let constr_loc = function
| CApp (loc,_,_) -> loc
| CCases (loc,_,_,_) -> loc
| COrderedCase (loc,_,_,_,_) -> loc
+ | CLetTuple (loc,_,_,_,_) -> loc
| CHole loc -> loc
| CPatVar (loc,_) -> loc
| CEvar (loc,_) -> loc
@@ -448,6 +492,7 @@ let rec occur_var_constr_expr id = function
| CHole _ | CEvar _ | CPatVar _ | CSort _ | CNumeral _ | CDynamic _ -> false
| CCases (loc,_,_,_)
| COrderedCase (loc,_,_,_,_)
+ | CLetTuple (loc,_,_,_,_)
| CFix (loc,_,_)
| CCoFix (loc,_,_) ->
Pp.warning "Capture check in multiple binders not done"; false
@@ -461,7 +506,7 @@ and occur_var_binders id b = function
let mkIdentC id = CRef (Ident (dummy_loc, id))
let mkRefC r = CRef r
-let mkAppC (f,l) = CApp (dummy_loc, (false,f), List.map (fun x -> (x,None)) l)
+let mkAppC (f,l) = CApp (dummy_loc, (None,f), List.map (fun x -> (x,None)) l)
let mkCastC (a,b) = CCast (dummy_loc,a,b)
let mkLambdaC (idl,a,b) = CLambdaN (dummy_loc,[idl,a],b)
let mkLetInC (id,a,b) = CLetIn (dummy_loc,id,a,b)
@@ -469,10 +514,11 @@ let mkProdC (idl,a,b) = CProdN (dummy_loc,[idl,a],b)
(* Used in correctness and interface *)
+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) =
- (List.fold_right (fun (_,na) -> name_fold g na) nal e,(nal,f e t)::bl) in
+ let h (nal,t) (e,bl) = (map_binder g e nal,(nal,f e t)::bl) in
List.fold_right h bl (e,[])
let map_constr_expr_with_binders f g e = function
@@ -490,12 +536,25 @@ let map_constr_expr_with_binders f g e = function
| CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a)
| CHole _ | CEvar _ | CPatVar _ | CSort _
| CNumeral _ | CDynamic _ | CRef _ as x -> x
- | CCases (loc,po,a,bl) ->
+ | CCases (loc,(po,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
- CCases (loc,option_app (f e) po,List.map (f e) a,bl)
+ let e' =
+ List.fold_right
+ (fun (tm,(na,indnal)) e ->
+ option_fold_right
+ (fun (loc,ind,nal) ->
+ List.fold_right (name_fold g) nal) indnal (name_fold g na e))
+ a e
+ in
+ CCases (loc,(option_app (f e) po, option_app (f e') rtnpo),
+ List.map (fun (tm,x) -> (f e tm,x)) a,bl)
| COrderedCase (loc,s,po,a,bl) ->
COrderedCase (loc,s,option_app (f e) po,f e a,List.map (f e) bl)
+ | CLetTuple (loc,nal,(na,po),b,c) ->
+ let e' = List.fold_right (name_fold g) nal e in
+ let e'' = name_fold g na e in
+ CLetTuple (loc,nal,(na,option_app (f e'') po),f e b,f e' c)
| CFix (loc,id,dl) ->
CFix (loc,id,List.map (fun (id,n,t,d) -> (id,n,f e t,f e d)) dl)
| CCoFix (loc,id,dl) ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 22:44:52 +0000