diff options
Diffstat (limited to 'interp/topconstr.ml')
| -rw-r--r-- | interp/topconstr.ml | 482 |
1 files changed, 269 insertions, 213 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml index a2b6e8b7..82f74f40 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: topconstr.ml,v 1.35.2.3 2004/11/17 09:51:41 herbelin Exp $ *) +(* $Id: topconstr.ml 8624 2006-03-13 17:38:17Z msozeau $ *) (*i*) open Pp @@ -16,6 +16,7 @@ open Nameops open Libnames open Rawterm open Term +open Mod_subst (*i*) (**********************************************************************) @@ -36,20 +37,19 @@ type aconstr = | ALambda of name * aconstr * aconstr | AProd of name * aconstr * aconstr | ALetIn of name * aconstr * aconstr - | ACases of aconstr option * aconstr option * + | ACases of 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 | AIf of aconstr * (name * aconstr option) * aconstr * aconstr | ASort of rawsort - | AHole of hole_kind + | AHole of Evd.hole_kind | APatVar of patvar - | ACast of aconstr * aconstr + | ACast of aconstr * cast_kind * aconstr let name_app f e = function - | Name id -> let (id, e) = f id e in (Name id, e) - | Anonymous -> Anonymous, e + | Name id -> let (id, e) = f id e in (e, Name id) + | Anonymous -> e,Anonymous let rec subst_rawvars l = function | RVar (_,id) as r -> (try List.assoc id l with Not_found -> r) @@ -67,40 +67,44 @@ 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 na,e = name_app g e na in RLambda (loc,na,f e ty,f e c) + let e,na = name_app g e na in RLambda (loc,na,f e ty,f e c) | AProd (na,ty,c) -> - let na,e = name_app g e na in RProd (loc,na,f e ty,f e c) + let e,na = 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,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 e,na = name_app g e na in RLetIn (loc,na,f e b,f e c) + | ACases (rtntypopt,tml,eqnl) -> + let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') -> + let e',t' = match t with + | None -> e',None + | Some (ind,nal) -> + let e',nal' = List.fold_right (fun na (e',nal) -> + let e',na' = name_app g e' na in e',na'::nal) nal (e',[]) in + e',Some (loc,ind,nal') in + let e',na' = name_app g e' na in + (e',(f e tm,(na',t'))::tml')) 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, 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,ref None) + 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') rtntypopt,tml',eqnl') | ALetTuple (nal,(na,po),b,c) -> - let e,nal = list_fold_map (fun e na -> let (na,e) = name_app g e na in e,na) e nal in - let na,e = name_app g e na in + let e,nal = list_fold_map (name_app g) e nal in + let e,na = name_app g e na in RLetTuple (loc,nal,(na,option_app (f e) po),f e b,f e c) | AIf (c,(na,po),b1,b2) -> - let na,e = name_app g e na in + let e,na = name_app g e na in RIf (loc,f e c,(na,option_app (f e) po),f e b1,f e b2) - | ACast (c,t) -> RCast (loc,f e c,f e t) + | ACast (c,k,t) -> RCast (loc,f e c,k,f e t) | ASort x -> RSort (loc,x) | AHole x -> RHole (loc,x) | APatVar n -> RPatVar (loc,(false,n)) | ARef x -> RRef (loc,x) +let rec rawconstr_of_aconstr loc x = + let rec aux () x = + rawconstr_of_aconstr_with_binders loc (fun id () -> (id,())) aux () x + in aux () x + let rec subst_pat subst pat = match pat with | PatVar _ -> pat @@ -110,100 +114,6 @@ let rec subst_pat subst pat = if kn' == kn && cpl' == cpl then pat else PatCstr (loc,((kn',i),j),cpl',n) -let rec subst_aconstr subst raw = - match raw with - | ARef ref -> - let ref' = subst_global subst ref in - if ref' == ref then raw else - ARef ref' - - | AVar _ -> raw - - | AApp (r,rl) -> - let r' = subst_aconstr subst r - and rl' = list_smartmap (subst_aconstr subst) rl in - if r' == r && rl' == rl then raw else - AApp(r',rl') - - | AList (id1,id2,r1,r2,b) -> - let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in - if r1' == r1 && r2' == r2 then raw else - AList (id1,id2,r1',r2',b) - - | ALambda (n,r1,r2) -> - let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in - if r1' == r1 && r2' == r2 then raw else - ALambda (n,r1',r2') - - | AProd (n,r1,r2) -> - let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in - if r1' == r1 && r2' == r2 then raw else - AProd (n,r1',r2') - - | ALetIn (n,r1,r2) -> - let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in - if r1' == r1 && r2' == r2 then raw else - ALetIn (n,r1',r2') - - | ACases (ro,rtntypopt,rl,branches) -> - let ro' = option_smartmap (subst_aconstr subst) ro - 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 - and r' = subst_aconstr subst r in - if cpl' == cpl && r' == r then branch else - (idl,cpl',r')) - branches - in - 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 - and r' = subst_aconstr subst r - and ra' = array_smartmap (subst_aconstr subst) ra in - 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') - - | AIf (c,(na,po),b1,b2) -> - let po' = option_smartmap (subst_aconstr subst) po - and b1' = subst_aconstr subst b1 - and b2' = subst_aconstr subst b2 - and c' = subst_aconstr subst c in - if po' == po && b1' == b1 && b2' == b2 && c' == c then raw else - AIf (c',(na,po'),b1',b2') - - | APatVar _ | ASort _ -> raw - - | AHole (ImplicitArg (ref,i)) -> - let ref' = subst_global subst ref in - if ref' == ref then raw else - AHole (ImplicitArg (ref',i)) - | AHole (BinderType _ | QuestionMark | CasesType | - InternalHole | TomatchTypeParameter _) -> raw - - | ACast (r1,r2) -> - let r1' = subst_aconstr subst r1 and r2' = subst_aconstr subst r2 in - if r1' == r1 && r2' == r2 then raw else - ACast (r1',r2') - let add_name r = function | Anonymous -> () | Name id -> r := id :: !r @@ -222,9 +132,9 @@ let compare_rawconstr f t1 t2 = match t1,t2 with f ty1 ty2 & f c1 c2 | RHole _, RHole _ -> true | RSort (_,s1), RSort (_,s2) -> s1 = s2 - | (RLetIn _ | RCases _ | ROrderedCase _ | RRec _ | RDynamic _ + | (RLetIn _ | RCases _ | RRec _ | RDynamic _ | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _),_ - | _,(RLetIn _ | RCases _ | ROrderedCase _ | RRec _ | RDynamic _ + | _,(RLetIn _ | RCases _ | RRec _ | RDynamic _ | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _) -> error "Unsupported construction in recursive notations" | (RRef _ | RVar _ | RApp _ | RLambda _ | RProd _ | RHole _ | RSort _), _ @@ -232,7 +142,7 @@ let compare_rawconstr f t1 t2 = match t1,t2 with let rec eq_rawconstr t1 t2 = compare_rawconstr eq_rawconstr t1 t2 -let discriminate_patterns nl l1 l2 = +let discriminate_patterns foundvars nl l1 l2 = let diff = ref None in let rec aux n c1 c2 = match c1,c2 with | RVar (_,v1), RVar (_,v2) when v1<>v2 -> @@ -245,42 +155,48 @@ let discriminate_patterns nl l1 l2 = let l = list_map2_i aux 0 l1 l2 in if not (List.for_all ((=) true) l) then error "Both ends of the recursive pattern differ"; - !diff + match !diff with + | None -> error "Both ends of the recursive pattern are the same" + | Some (x,y,_ as discr) -> + List.iter (fun id -> + if List.mem id !foundvars + then error "Variables used in the recursive part of a pattern are not allowed to occur outside of the recursive part"; + foundvars := id::!foundvars) [x;y]; + discr let aconstr_and_vars_of_rawconstr a = let found = ref [] in - let bound_binders = ref [] in let rec aux = function - | RVar (_,id) -> - if not (List.mem id !bound_binders) then found := id::!found; - AVar id + | RVar (_,id) -> found := id::!found; AVar id | RApp (_,f,args) when has_ldots args -> make_aconstr_list f args + | RApp (_,RVar (_,f),[RApp (_,t,[c]);d]) when f = ldots_var -> + (* Special case for alternative (recursive) notation of application *) + let x,y,lassoc = discriminate_patterns found 0 [c] [d] in + 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 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,rtntypopt),tml,eqnl) -> + | 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) + | RLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c) + | RCases (_,rtntypopt,tml,eqnl) -> let f (_,idl,pat,rhs) = - bound_binders := idl@(!bound_binders); + found := idl@(!found); (idl,pat,aux rhs) in - ACases (option_app aux tyopt, - option_app aux !rtntypopt, - List.map (fun (tm,{contents = (na,x)}) -> - add_name bound_binders na; + ACases (option_app aux rtntypopt, + List.map (fun (tm,(na,x)) -> + add_name found na; option_iter - (fun (_,_,nl) -> List.iter (add_name bound_binders) nl) x; + (fun (_,_,nl) -> List.iter (add_name found) 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) -> - add_name bound_binders na; - List.iter (add_name bound_binders) nal; + add_name found na; + List.iter (add_name found) nal; ALetTuple (nal,(na,option_app aux po),aux b,aux c) | RIf (loc,c,(na,po),b1,b2) -> - add_name bound_binders na; + add_name found na; AIf (aux c,(na,option_app aux po),aux b1,aux b2) - | RCast (_,c,t) -> ACast (aux c,aux t) + | RCast (_,c,k,t) -> ACast (aux c,k,aux t) | RSort (_,s) -> ASort s | RHole (_,w) -> AHole w | RRef (_,r) -> ARef r @@ -300,13 +216,7 @@ allowed in abbreviatable expressions" error "Both ends of the recursive pattern have different lengths"; let ll2,l2' = list_chop nl l2 in let t = List.hd l2' and lr2 = List.tl l2' in - let discr = discriminate_patterns nl (ll1@lr1) (ll2@lr2) in - let x,y,order = match discr with Some z -> z | None -> - error "Both ends of the recursive pattern are the same" in - List.iter (fun id -> - if List.mem id !bound_binders or List.mem id !found - then error "Variables used in the recursive part of a pattern are not allowed to occur outside of the recursive part"; - found := id::!found) [x;y]; + let x,y,order = discriminate_patterns found nl (ll1@lr1) (ll2@lr2) in let iter = if order then RApp (loc,f2,ll2@RVar (loc,ldots_var)::lr2) else RApp (loc,f1,ll1@RVar (loc,ldots_var)::lr1) in @@ -326,20 +236,126 @@ allowed in abbreviatable expressions" in let t = aux a in (* Side effect *) - t, !found, !bound_binders + t, !found let aconstr_of_rawconstr vars a = - let a,notbindingvars,binders = aconstr_and_vars_of_rawconstr a in + let a,foundvars = aconstr_and_vars_of_rawconstr a in let check_type x = - if not (List.mem x notbindingvars or List.mem x binders) then + if not (List.mem x foundvars) then error ((string_of_id x)^" is unbound in the right-hand-side") in List.iter check_type vars; a +let aconstr_of_constr avoiding t = + aconstr_of_rawconstr [] (Detyping.detype false avoiding [] t) + +let rec subst_aconstr subst bound raw = + match raw with + | ARef ref -> + let ref',t = subst_global subst ref in + if ref' == ref then raw else + aconstr_of_constr bound t + + | AVar _ -> raw + + | AApp (r,rl) -> + let r' = subst_aconstr subst bound r + and rl' = list_smartmap (subst_aconstr subst bound) rl in + if r' == r && rl' == rl then raw else + AApp(r',rl') + + | AList (id1,id2,r1,r2,b) -> + let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in + if r1' == r1 && r2' == r2 then raw else + AList (id1,id2,r1',r2',b) + + | ALambda (n,r1,r2) -> + let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in + if r1' == r1 && r2' == r2 then raw else + ALambda (n,r1',r2') + + | AProd (n,r1,r2) -> + let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in + if r1' == r1 && r2' == r2 then raw else + AProd (n,r1',r2') + + | ALetIn (n,r1,r2) -> + let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in + 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 + and rl' = list_smartmap + (fun (a,(n,signopt) as x) -> + let a' = subst_aconstr subst bound 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 + and r' = subst_aconstr subst bound r in + if cpl' == cpl && r' == r then branch else + (idl,cpl',r')) + branches + in + if rtntypopt' == rtntypopt && rtntypopt == rtntypopt' & + rl' == rl && branches' == branches then raw else + ACases (rtntypopt',rl',branches') + + | ALetTuple (nal,(na,po),b,c) -> + 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 + 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') + + | APatVar _ | ASort _ -> raw + + | AHole (Evd.ImplicitArg (ref,i)) -> + let ref',t = subst_global subst ref in + if ref' == ref then raw else + AHole (Evd.InternalHole) + | AHole (Evd.BinderType _ | Evd.QuestionMark | Evd.CasesType | + Evd.InternalHole | Evd.TomatchTypeParameter _) -> raw + + | ACast (r1,k,r2) -> + let r1' = subst_aconstr subst bound r1 and r2' = subst_aconstr subst bound r2 in + if r1' == r1 && r2' == r2 then raw else + ACast (r1',k,r2') + + 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_app (fun rtn -> + let nal = + List.flatten (List.map (fun (_,(na,t)) -> + match t with Some x -> (pi x)@[na] | None -> [na]) tml) in + List.fold_right mklam nal rtn) + rtno + +let abstract_return_type_context_rawconstr = + abstract_return_type_context pi3 + (fun na c -> RLambda(dummy_loc,na,RHole(dummy_loc,Evd.InternalHole),c)) + +let abstract_return_type_context_aconstr = + abstract_return_type_context snd + (fun na c -> ALambda(na,AHole Evd.InternalHole,c)) + let rec adjust_scopes = function | _,[] -> [] | [],a::args -> (None,a) :: adjust_scopes ([],args) @@ -366,6 +382,18 @@ let bind_env alp sigma var v = (* TODO: handle the case of multiple occs in different scopes *) (var,v)::sigma +let match_opt f sigma t1 t2 = match (t1,t2) with + | None, None -> sigma + | Some t1, Some t2 -> f sigma t1 t2 + | _ -> raise No_match + +let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with + | (Name id1,Name id2) when List.mem id2 metas -> + alp, bind_env alp sigma id2 (RVar (dummy_loc,id1)) + | (Name id1,Name id2) -> (id1,id2)::alp,sigma + | (Anonymous,Anonymous) -> alp,sigma + | _ -> raise No_match + let rec match_ alp metas sigma a1 a2 = match (a1,a2) with | r1, AVar id2 when List.mem id2 metas -> bind_env alp sigma id2 r1 | RVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma @@ -377,28 +405,34 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with 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) -> - match_binders alp metas (match_ alp metas sigma t1 t2) b1 b2 na1 na2 + match_binders alp metas na1 na2 (match_ alp metas sigma t1 t2) b1 b2 | RProd (_,na1,t1,b1), AProd (na2,t2,b2) -> - match_binders alp metas (match_ alp metas sigma t1 t2) b1 b2 na1 na2 + 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 (match_ alp metas sigma t1 t2) b1 b2 na1 na2 - | RCases (_,(po1,rtno1),tml1,eqnl1), ACases (po2,rtno2,tml2,eqnl2) + 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 -> - let sigma = option_fold_left2 (match_ alp metas) sigma po1 po2 in - (* TODO: match rtno' with their contexts *) - let sigma = List.fold_left2 + 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 = 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) - when Array.length bl1 = Array.length 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) -> + 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 + let sigma = match_ alp metas sigma b1 b2 in + let (alp,sigma) = + List.fold_left2 (match_names metas) (alp,sigma) nal1 nal2 in + match_ alp metas sigma c1 c2 + | RCast(_,c1,_,t1), ACast(c2,_,t2) -> match_ alp metas (match_ alp metas sigma c1 c2) t1 t2 | RSort (_,s1), ASort s2 when s1 = s2 -> sigma | RPatVar _, AHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match - | a, AHole _ when not(Options.do_translate()) -> sigma - | RHole _, AHole _ -> sigma + | a, AHole _ -> sigma | (RDynamic _ | RRec _ | REvar _), _ | _,_ -> raise No_match @@ -423,13 +457,9 @@ and match_alist alp metas sigma l1 l2 x iter termin lassoc = let tl,sigma = match_alist_tail alp metas sigma [t1] rest in (x,encode_list_value (if lassoc then List.rev tl else tl))::sigma -and match_binders alp metas sigma b1 b2 na1 na2 = match (na1,na2) with - | (Name id1,Name id2) when List.mem id2 metas -> - let sigma = bind_env alp sigma id2 (RVar (dummy_loc,id1)) in - match_ alp metas sigma b1 b2 - | (Name id1,Name id2) -> match_ ((id1,id2)::alp) metas sigma b1 b2 - | (Anonymous,Anonymous) -> match_ alp metas sigma b1 b2 - | _ -> raise No_match +and match_binders alp metas na1 na2 sigma b1 b2 = + let (alp,sigma) = match_names metas (alp,sigma) na1 na2 in + match_ alp metas sigma b1 b2 and match_equations alp metas sigma (_,idl1,pat1,rhs1) (idl2,pat2,rhs2) = if idl1 = idl2 & pat1 = pat2 (* Useful to reason up to alpha ?? *) then @@ -461,12 +491,15 @@ type explicitation = ExplByPos of int | ExplByName of identifier type proj_flag = int option (* [Some n] = proj of the n-th visible argument *) +type prim_token = Numeral of Bigint.bigint | String of string + type cases_pattern_expr = | CPatAlias of loc * cases_pattern_expr * identifier | CPatCstr of loc * reference * cases_pattern_expr list | CPatAtom of loc * reference option + | CPatOr of loc * cases_pattern_expr list | CPatNotation of loc * notation * cases_pattern_expr list - | CPatNumeral of loc * Bignat.bigint + | CPatPrim of loc * prim_token | CPatDelimiters of loc * string * cases_pattern_expr type constr_expr = @@ -480,11 +513,9 @@ type 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 * constr_expr option) * + | CCases of loc * constr_expr option * (constr_expr * (name option * constr_expr 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 option * constr_expr option) * constr_expr * constr_expr | CIf of loc * constr_expr * (name option * constr_expr option) @@ -493,14 +524,15 @@ type constr_expr = | CPatVar of loc * (bool * patvar) | CEvar of loc * existential_key | CSort of loc * rawsort - | CCast of loc * constr_expr * constr_expr + | CCast of loc * constr_expr * cast_kind * constr_expr | CNotation of loc * notation * constr_expr list - | CNumeral of loc * Bignat.bigint + | CPrim of loc * prim_token | CDelimiters of loc * string * constr_expr | CDynamic of loc * Dyn.t + and fixpoint_expr = - identifier * int * local_binder list * constr_expr * constr_expr + identifier * (int * recursion_order_expr) * local_binder list * constr_expr * constr_expr and local_binder = | LocalRawDef of name located * constr_expr @@ -509,6 +541,10 @@ and local_binder = and cofixpoint_expr = identifier * local_binder list * constr_expr * constr_expr +and recursion_order_expr = + | CStructRec + | CWfRec of constr_expr + (***********************) (* For binders parsing *) @@ -520,6 +556,9 @@ let rec local_binders_length = function let names_of_local_assums 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) + (**********************************************************************) (* Functions on constr_expr *) @@ -535,16 +574,15 @@ let constr_loc = function | CAppExpl (loc,_,_) -> loc | CApp (loc,_,_) -> loc | CCases (loc,_,_,_) -> loc - | COrderedCase (loc,_,_,_,_) -> loc | CLetTuple (loc,_,_,_,_) -> loc | CIf (loc,_,_,_,_) -> loc | CHole loc -> loc | CPatVar (loc,_) -> loc | CEvar (loc,_) -> loc | CSort (loc,_) -> loc - | CCast (loc,_,_) -> loc + | CCast (loc,_,_,_) -> loc | CNotation (loc,_,_) -> loc - | CNumeral (loc,_) -> loc + | CPrim (loc,_) -> loc | CDelimiters (loc,_,_) -> loc | CDynamic _ -> dummy_loc @@ -552,8 +590,9 @@ let cases_pattern_loc = function | CPatAlias (loc,_,_) -> loc | CPatCstr (loc,_,_) -> loc | CPatAtom (loc,_) -> loc + | CPatOr (loc,_) -> loc | CPatNotation (loc,_,_) -> loc - | CPatNumeral (loc,_) -> loc + | CPatPrim (loc,_) -> loc | CPatDelimiters (loc,_,_) -> loc let occur_var_constr_ref id = function @@ -571,12 +610,12 @@ let rec occur_var_constr_expr id = function | CProdN (_,l,b) -> occur_var_binders id b l | CLambdaN (_,l,b) -> occur_var_binders id b l | CLetIn (_,na,a,b) -> occur_var_binders id b [[na],a] - | CCast (loc,a,b) -> occur_var_constr_expr id a or occur_var_constr_expr id b + | CCast (loc,a,_,b) -> + occur_var_constr_expr id a or occur_var_constr_expr id b | CNotation (_,_,l) -> List.exists (occur_var_constr_expr id) l | CDelimiters (loc,_,a) -> occur_var_constr_expr id a - | CHole _ | CEvar _ | CPatVar _ | CSort _ | CNumeral _ | CDynamic _ -> false + | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _ -> false | CCases (loc,_,_,_) - | COrderedCase (loc,_,_,_,_) | CLetTuple (loc,_,_,_,_) | CIf (loc,_,_,_,_) | CFix (loc,_,_) @@ -593,26 +632,45 @@ 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, (None,f), List.map (fun x -> (x,None)) l) -let mkCastC (a,b) = CCast (dummy_loc,a,b) +let mkCastC (a,k,b) = CCast (dummy_loc,a,k,b) let mkLambdaC (idl,a,b) = CLambdaN (dummy_loc,[idl,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 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 coerce_to_id = function + | CRef (Ident (loc,id)) -> (loc,id) + | a -> user_err_loc + (constr_loc a,"coerce_to_id", + str "This expression should be a simple identifier") + (* Used in correctness and interface *) let names_of_cases_indtype = - let rec vars_of ids t = - match t with - (* We deal only with the regular cases *) - | CApp (_,_,l) -> List.fold_left (fun ids (a,_) -> vars_of ids a) [] l - | CRef (Ident (_,id)) -> id::ids - | CNotation (_,_,l) - (* assume the ntn is applicative and does not instantiate the head !! *) - | CAppExpl (_,_,l) -> List.fold_left vars_of [] l - | CDelimiters(_,_,c) -> vars_of ids c - | _ -> ids in - vars_of [] + let add_var ids = function CRef (Ident (_,id)) -> id::ids | _ -> ids in + let rec vars_of = function + (* We deal only with the regular cases *) + | CApp (_,_,l) -> List.fold_left add_var [] (List.map fst l) + | CNotation (_,_,l) + (* assume the ntn is applicative and does not instantiate the head !! *) + | CAppExpl (_,_,l) -> List.fold_left add_var [] l + | CDelimiters(_,_,c) -> vars_of c + | _ -> [] in + vars_of let map_binder g e nal = List.fold_right (fun (_,na) -> name_fold g na) nal e @@ -642,12 +700,12 @@ let map_constr_expr_with_binders f g e = function | CLambdaN (loc,bl,b) -> let (e,bl) = map_binders f g e bl in CLambdaN (loc,bl,f e b) | CLetIn (loc,na,a,b) -> CLetIn (loc,na,f e a,f (name_fold g (snd na) e) b) - | CCast (loc,a,b) -> CCast (loc,f e a,f e b) + | CCast (loc,a,k,b) -> CCast (loc,f e a,k,f e b) | CNotation (loc,n,l) -> CNotation (loc,n,List.map (f e) l) | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a) | CHole _ | CEvar _ | CPatVar _ | CSort _ - | CNumeral _ | CDynamic _ | CRef _ as x -> x - | CCases (loc,(po,rtnpo),a,bl) -> + | CPrim _ | CDynamic _ | CRef _ as x -> x + | CCases (loc,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 e' = @@ -660,10 +718,8 @@ let map_constr_expr_with_binders f g e = function indnal (option_fold_right (name_fold g) na e)) a e in - CCases (loc,(option_app (f e) po, option_app (f e') rtnpo), + CCases (loc,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,(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 @@ -698,8 +754,8 @@ let rec replace_vars_constr_expr l = function (* Concrete syntax for modules and modules types *) type with_declaration_ast = - | CWith_Module of identifier located * qualid located - | CWith_Definition of identifier located * constr_expr + | CWith_Module of identifier list located * qualid located + | CWith_Definition of identifier list located * constr_expr type module_type_ast = | CMTEident of qualid located |