diff options
Diffstat (limited to 'interp/topconstr.ml')
| -rw-r--r-- | interp/topconstr.ml | 406 |
1 files changed, 139 insertions, 267 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 9ea6c7e4c5..ab603c37d1 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -19,56 +19,11 @@ open Term open Mod_subst open Misctypes open Decl_kinds +open Constrexpr +open Notation_term (*i*) (**********************************************************************) -(* This is the subtype of glob_constr allowed in syntactic extensions *) - -(* For AList: first constr is iterator, second is terminator; - first id is where each argument of the list has to be substituted - in iterator and snd id is alternative name just for printing; - boolean is associativity *) - -type aconstr = - (* Part common to glob_constr and cases_pattern *) - | ARef of global_reference - | AVar of identifier - | AApp of aconstr * aconstr list - | AHole of Evar_kinds.t - | AList of identifier * identifier * aconstr * aconstr * bool - (* Part only in glob_constr *) - | ALambda of name * aconstr * aconstr - | AProd of name * aconstr * aconstr - | ABinderList of identifier * identifier * aconstr * aconstr - | ALetIn of name * aconstr * aconstr - | ACases of case_style * aconstr option * - (aconstr * (name * (inductive * 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 glob_sort - | APatVar of patvar - | ACast of aconstr * aconstr cast_type - -type scope_name = string - -type tmp_scope_name = scope_name - -type subscopes = tmp_scope_name option * scope_name list - -type notation_var_instance_type = - | NtnTypeConstr | NtnTypeConstrList | NtnTypeBinderList - -type notation_var_internalization_type = - | NtnInternTypeConstr | NtnInternTypeBinder | NtnInternTypeIdent - -type interpretation = - (identifier * (subscopes * notation_var_instance_type)) list * aconstr - -(**********************************************************************) (* Re-interpret a notation as a glob_constr, taking care of binders *) let name_to_ident = function @@ -101,28 +56,28 @@ let rec subst_glob_vars l = function let ldots_var = id_of_string ".." -let glob_constr_of_aconstr_with_binders loc g f e = function - | AVar id -> GVar (loc,id) - | AApp (a,args) -> GApp (loc,f e a, List.map (f e) args) - | AList (x,y,iter,tail,swap) -> +let glob_constr_of_notation_constr_with_binders loc g f e = function + | NVar id -> GVar (loc,id) + | NApp (a,args) -> GApp (loc,f e a, List.map (f e) args) + | NList (x,y,iter,tail,swap) -> let t = f e tail in let it = f e iter in let innerl = (ldots_var,t)::(if swap then [] else [x,GVar(loc,y)]) in let inner = GApp (loc,GVar (loc,ldots_var),[subst_glob_vars innerl it]) in let outerl = (ldots_var,inner)::(if swap then [x,GVar(loc,y)] else []) in subst_glob_vars outerl it - | ABinderList (x,y,iter,tail) -> + | NBinderList (x,y,iter,tail) -> let t = f e tail in let it = f e iter in let innerl = [(ldots_var,t);(x,GVar(loc,y))] in let inner = GApp (loc,GVar (loc,ldots_var),[subst_glob_vars innerl it]) in let outerl = [(ldots_var,inner)] in subst_glob_vars outerl it - | ALambda (na,ty,c) -> + | NLambda (na,ty,c) -> let e',na = g e na in GLambda (loc,na,Explicit,f e ty,f e' c) - | AProd (na,ty,c) -> + | NProd (na,ty,c) -> let e',na = g e na in GProd (loc,na,Explicit,f e ty,f e' c) - | ALetIn (na,b,c) -> + | NLetIn (na,b,c) -> let e',na = g e na in GLetIn (loc,na,f e b,f e' c) - | ACases (sty,rtntypopt,tml,eqnl) -> + | NCases (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 @@ -138,28 +93,28 @@ let glob_constr_of_aconstr_with_binders loc g f e = function list_fold_map (cases_pattern_fold_map loc fold) ([],e) patl in (loc,idl,patl,f e rhs)) eqnl in GCases (loc,sty,Option.map (f e') rtntypopt,tml',eqnl') - | ALetTuple (nal,(na,po),b,c) -> + | NLetTuple (nal,(na,po),b,c) -> let e',nal = list_fold_map g e nal in let e'',na = g e na in GLetTuple (loc,nal,(na,Option.map (f e'') po),f e b,f e' c) - | AIf (c,(na,po),b1,b2) -> + | NIf (c,(na,po),b1,b2) -> let e',na = g e na in GIf (loc,f e c,(na,Option.map (f e') po),f e b1,f e b2) - | ARec (fk,idl,dll,tl,bl) -> + | NRec (fk,idl,dll,tl,bl) -> let e,dll = array_fold_map (list_fold_map (fun e (na,oc,b) -> let e,na = g e na in (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in let e',idl = array_fold_map (to_id g) e idl in GRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl) - | ACast (c,k) -> GCast (loc,f e c, Miscops.map_cast_type (f e) k) - | ASort x -> GSort (loc,x) - | AHole x -> GHole (loc,x) - | APatVar n -> GPatVar (loc,(false,n)) - | ARef x -> GRef (loc,x) + | NCast (c,k) -> GCast (loc,f e c, Miscops.map_cast_type (f e) k) + | NSort x -> GSort (loc,x) + | NHole x -> GHole (loc,x) + | NPatVar n -> GPatVar (loc,(false,n)) + | NRef x -> GRef (loc,x) -let rec glob_constr_of_aconstr loc x = +let rec glob_constr_of_notation_constr loc x = let rec aux () x = - glob_constr_of_aconstr_with_binders loc (fun () id -> ((),id)) aux () x + glob_constr_of_notation_constr_with_binders loc (fun () id -> ((),id)) aux () x in aux () x (****************************************************************************) @@ -260,17 +215,17 @@ let compare_recursive_parts found f (iterator,subc) = else iterator) in (* found have been collected by compare_constr *) found := newfound; - AList (x,y,iterator,f (Option.get !terminator),lassoc) + NList (x,y,iterator,f (Option.get !terminator),lassoc) | Some (x,y,None) -> let newfound = (pi1 !found, pi2 !found, (x,y) :: pi3 !found) in let iterator = f iterator in (* found have been collected by compare_constr *) found := newfound; - ABinderList (x,y,iterator,f (Option.get !terminator)) + NBinderList (x,y,iterator,f (Option.get !terminator)) else raise Not_found -let aconstr_and_vars_of_glob_constr a = +let notation_constr_and_vars_of_glob_constr a = let found = ref ([],[],[]) in let rec aux c = let keepfound = !found in @@ -287,14 +242,14 @@ let aconstr_and_vars_of_glob_constr a = | c -> aux' c and aux' = function - | GVar (_,id) -> add_id found id; AVar id - | GApp (_,g,args) -> AApp (aux g, List.map aux args) - | GLambda (_,na,bk,ty,c) -> add_name found na; ALambda (na,aux ty,aux c) - | GProd (_,na,bk,ty,c) -> add_name found na; AProd (na,aux ty,aux c) - | GLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c) + | GVar (_,id) -> add_id found id; NVar id + | GApp (_,g,args) -> NApp (aux g, List.map aux args) + | GLambda (_,na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c) + | GProd (_,na,bk,ty,c) -> add_name found na; NProd (na,aux ty,aux c) + | GLetIn (_,na,b,c) -> add_name found na; NLetIn (na,aux b,aux c) | GCases (_,sty,rtntypopt,tml,eqnl) -> let f (_,idl,pat,rhs) = List.iter (add_id found) idl; (pat,aux rhs) in - ACases (sty,Option.map aux rtntypopt, + NCases (sty,Option.map aux rtntypopt, List.map (fun (tm,(na,x)) -> add_name found na; Option.iter @@ -304,22 +259,22 @@ let aconstr_and_vars_of_glob_constr a = | GLetTuple (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) + NLetTuple (nal,(na,Option.map aux po),aux b,aux c) | GIf (loc,c,(na,po),b1,b2) -> add_name found na; - AIf (aux c,(na,Option.map aux po),aux b1,aux b2) + NIf (aux c,(na,Option.map aux po),aux b1,aux b2) | GRec (_,fk,idl,dll,tl,bl) -> Array.iter (add_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) - | GCast (_,c,k) -> ACast (aux c,Miscops.map_cast_type aux k) - | GSort (_,s) -> ASort s - | GHole (_,w) -> AHole w - | GRef (_,r) -> ARef r - | GPatVar (_,(_,n)) -> APatVar n + NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl) + | GCast (_,c,k) -> NCast (aux c,Miscops.map_cast_type aux k) + | GSort (_,s) -> NSort s + | GHole (_,w) -> NHole w + | GRef (_,r) -> NRef r + | GPatVar (_,(_,n)) -> NPatVar n | GEvar _ -> error "Existential variables not allowed in notations." @@ -369,15 +324,15 @@ let check_variables vars recvars (found,foundrec,foundrecbinding) = | NtnInternTypeIdent -> check_bound x in List.iter check_type vars -let aconstr_of_glob_constr vars recvars a = - let a,found = aconstr_and_vars_of_glob_constr a in +let notation_constr_of_glob_constr vars recvars a = + let a,found = notation_constr_and_vars_of_glob_constr a in check_variables vars recvars found; a (* Substitution of kernel names, avoiding a list of bound identifiers *) -let aconstr_of_constr avoiding t = - aconstr_of_glob_constr [] [] (Detyping.detype false avoiding [] t) +let notation_constr_of_constr avoiding t = + notation_constr_of_glob_constr [] [] (Detyping.detype false avoiding [] t) let rec subst_pat subst pat = match pat with @@ -388,56 +343,56 @@ 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 bound raw = +let rec subst_notation_constr subst bound raw = match raw with - | ARef ref -> + | NRef ref -> let ref',t = subst_global subst ref in if ref' == ref then raw else - aconstr_of_constr bound t + notation_constr_of_constr bound t - | AVar _ -> raw + | NVar _ -> raw - | AApp (r,rl) -> - let r' = subst_aconstr subst bound r - and rl' = list_smartmap (subst_aconstr subst bound) rl in + | NApp (r,rl) -> + let r' = subst_notation_constr subst bound r + and rl' = list_smartmap (subst_notation_constr subst bound) rl in if r' == r && rl' == rl then raw else - AApp(r',rl') + NApp(r',rl') - | AList (id1,id2,r1,r2,b) -> - let r1' = subst_aconstr subst bound r1 - and r2' = subst_aconstr subst bound r2 in + | NList (id1,id2,r1,r2,b) -> + let r1' = subst_notation_constr subst bound r1 + and r2' = subst_notation_constr subst bound r2 in if r1' == r1 && r2' == r2 then raw else - AList (id1,id2,r1',r2',b) + NList (id1,id2,r1',r2',b) - | ALambda (n,r1,r2) -> - let r1' = subst_aconstr subst bound r1 - and r2' = subst_aconstr subst bound r2 in + | NLambda (n,r1,r2) -> + let r1' = subst_notation_constr subst bound r1 + and r2' = subst_notation_constr subst bound r2 in if r1' == r1 && r2' == r2 then raw else - ALambda (n,r1',r2') + NLambda (n,r1',r2') - | AProd (n,r1,r2) -> - let r1' = subst_aconstr subst bound r1 - and r2' = subst_aconstr subst bound r2 in + | NProd (n,r1,r2) -> + let r1' = subst_notation_constr subst bound r1 + and r2' = subst_notation_constr subst bound r2 in if r1' == r1 && r2' == r2 then raw else - AProd (n,r1',r2') + NProd (n,r1',r2') - | ABinderList (id1,id2,r1,r2) -> - let r1' = subst_aconstr subst bound r1 - and r2' = subst_aconstr subst bound r2 in + | NBinderList (id1,id2,r1,r2) -> + let r1' = subst_notation_constr subst bound r1 + and r2' = subst_notation_constr subst bound r2 in if r1' == r1 && r2' == r2 then raw else - ABinderList (id1,id2,r1',r2') + NBinderList (id1,id2,r1',r2') - | ALetIn (n,r1,r2) -> - let r1' = subst_aconstr subst bound r1 - and r2' = subst_aconstr subst bound r2 in + | NLetIn (n,r1,r2) -> + let r1' = subst_notation_constr subst bound r1 + and r2' = subst_notation_constr subst bound r2 in if r1' == r1 && r2' == r2 then raw else - ALetIn (n,r1',r2') + NLetIn (n,r1',r2') - | ACases (sty,rtntypopt,rl,branches) -> - let rtntypopt' = Option.smartmap (subst_aconstr subst bound) rtntypopt + | NCases (sty,rtntypopt,rl,branches) -> + let rtntypopt' = Option.smartmap (subst_notation_constr subst bound) rtntypopt and rl' = list_smartmap (fun (a,(n,signopt) as x) -> - let a' = subst_aconstr subst bound a in + let a' = subst_notation_constr subst bound a in let signopt' = Option.map (fun ((indkn,i),nal as z) -> let indkn' = subst_ind subst indkn in if indkn == indkn' then z else ((indkn',i),nal)) signopt in @@ -446,62 +401,62 @@ let rec subst_aconstr subst bound raw = and branches' = list_smartmap (fun (cpl,r as branch) -> let cpl' = list_smartmap (subst_pat subst) cpl - and r' = subst_aconstr subst bound r in + and r' = subst_notation_constr subst bound r in if cpl' == cpl && r' == r then branch else (cpl',r')) branches in if rtntypopt' == rtntypopt && rtntypopt == rtntypopt' & rl' == rl && branches' == branches then raw else - ACases (sty,rtntypopt',rl',branches') + NCases (sty,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 + | NLetTuple (nal,(na,po),b,c) -> + let po' = Option.smartmap (subst_notation_constr subst bound) po + and b' = subst_notation_constr subst bound b + and c' = subst_notation_constr subst bound c in if po' == po && b' == b && c' == c then raw else - ALetTuple (nal,(na,po'),b',c') + NLetTuple (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 + | NIf (c,(na,po),b1,b2) -> + let po' = Option.smartmap (subst_notation_constr subst bound) po + and b1' = subst_notation_constr subst bound b1 + and b2' = subst_notation_constr subst bound b2 + and c' = subst_notation_constr subst bound c in if po' == po && b1' == b1 && b2' == b2 && c' == c then raw else - AIf (c',(na,po'),b1',b2') + NIf (c',(na,po'),b1',b2') - | ARec (fk,idl,dll,tl,bl) -> + | NRec (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 + let oc' = Option.smartmap (subst_notation_constr subst bound) oc in + let b' = subst_notation_constr 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 + let tl' = array_smartmap (subst_notation_constr subst bound) tl in + let bl' = array_smartmap (subst_notation_constr subst bound) bl in if dll' == dll && tl' == tl && bl' == bl then raw else - ARec (fk,idl,dll',tl',bl') + NRec (fk,idl,dll',tl',bl') - | APatVar _ | ASort _ -> raw + | NPatVar _ | NSort _ -> raw - | AHole (Evar_kinds.ImplicitArg (ref,i,b)) -> + | NHole (Evar_kinds.ImplicitArg (ref,i,b)) -> let ref',t = subst_global subst ref in if ref' == ref then raw else - AHole (Evar_kinds.InternalHole) - | AHole (Evar_kinds.BinderType _ |Evar_kinds.QuestionMark _ + NHole (Evar_kinds.InternalHole) + | NHole (Evar_kinds.BinderType _ |Evar_kinds.QuestionMark _ |Evar_kinds.CasesType |Evar_kinds.InternalHole |Evar_kinds.TomatchTypeParameter _ |Evar_kinds.GoalEvar |Evar_kinds.ImpossibleCase |Evar_kinds.MatchingVar _) -> raw - | ACast (r1,k) -> - let r1' = subst_aconstr subst bound r1 in - let k' = Miscops.smartmap_cast_type (subst_aconstr subst bound) k in - if r1' == r1 && k' == k then raw else ACast(r1',k') + | NCast (r1,k) -> + let r1' = subst_notation_constr subst bound r1 in + let k' = Miscops.smartmap_cast_type (subst_notation_constr subst bound) k in + if r1' == r1 && k' == k then raw else NCast(r1',k') let subst_interpretation subst (metas,pat) = let bound = List.map fst metas in - (metas,subst_aconstr subst bound pat) + (metas,subst_notation_constr subst bound pat) -(* Pattern-matching glob_constr and aconstr *) +(* Pattern-matching glob_constr and notation_constr *) let abstract_return_type_context pi mklam tml rtno = Option.map (fun rtn -> @@ -516,9 +471,9 @@ let abstract_return_type_context_glob_constr = (fun na c -> GLambda(dummy_loc,na,Explicit,GHole(dummy_loc,Evar_kinds.InternalHole),c)) -let abstract_return_type_context_aconstr = +let abstract_return_type_context_notation_constr = abstract_return_type_context snd - (fun na c -> ALambda(na,AHole Evar_kinds.InternalHole,c)) + (fun na c -> NLambda(na,NHole Evar_kinds.InternalHole,c)) exception No_match @@ -633,60 +588,60 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 = match (a1,a2) with (* Matching notation variable *) - | r1, AVar id2 when List.mem id2 tmetas -> bind_env alp sigma id2 r1 + | r1, NVar id2 when List.mem id2 tmetas -> bind_env alp sigma id2 r1 (* Matching recursive notations for terms *) - | r1, AList (x,_,iter,termin,lassoc) -> + | r1, NList (x,_,iter,termin,lassoc) -> match_alist (match_hd u alp) metas sigma r1 x iter termin lassoc (* Matching recursive notations for binders: ad hoc cases supporting let-in *) - | GLambda (_,na1,bk,t1,b1), ABinderList (x,_,ALambda (Name id2,_,b2),termin)-> + | GLambda (_,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name id2,_,b2),termin)-> let (decls,b) = match_iterated_binders true [(na1,bk,None,t1)] b1 in (* TODO: address the possibility that termin is a Lambda itself *) match_in u alp metas (bind_binder sigma x decls) b termin - | GProd (_,na1,bk,t1,b1), ABinderList (x,_,AProd (Name id2,_,b2),termin) + | GProd (_,na1,bk,t1,b1), NBinderList (x,_,NProd (Name id2,_,b2),termin) when na1 <> Anonymous -> let (decls,b) = match_iterated_binders false [(na1,bk,None,t1)] b1 in (* TODO: address the possibility that termin is a Prod itself *) match_in u alp metas (bind_binder sigma x decls) b termin (* Matching recursive notations for binders: general case *) - | r, ABinderList (x,_,iter,termin) -> + | r, NBinderList (x,_,iter,termin) -> match_abinderlist_with_app (match_hd u alp) metas sigma r x iter termin (* Matching individual binders as part of a recursive pattern *) - | GLambda (_,na,bk,t,b1), ALambda (Name id,_,b2) when List.mem id blmetas -> + | GLambda (_,na,bk,t,b1), NLambda (Name id,_,b2) when List.mem id blmetas -> match_in u alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2 - | GProd (_,na,bk,t,b1), AProd (Name id,_,b2) + | GProd (_,na,bk,t,b1), NProd (Name id,_,b2) when List.mem id blmetas & na <> Anonymous -> match_in u alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2 (* Matching compositionally *) - | GVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma - | GRef (_,r1), ARef r2 when (eq_gr r1 r2) -> sigma - | GPatVar (_,(_,n1)), APatVar n2 when n1=n2 -> sigma - | GApp (loc,f1,l1), AApp (f2,l2) -> + | GVar (_,id1), NVar id2 when alpha_var id1 id2 alp -> sigma + | GRef (_,r1), NRef r2 when (eq_gr r1 r2) -> sigma + | GPatVar (_,(_,n1)), NPatVar n2 when n1=n2 -> sigma + | GApp (loc,f1,l1), NApp (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 + let l21,l22 = list_chop (n2-n1) l2 in f1,l1, NApp (f2,l21), l22 else if n1 > n2 then let l11,l12 = list_chop (n1-n2) l1 in GApp (loc,f1,l11),l12, f2,l2 else f1,l1, f2, l2 in let may_use_eta = does_not_come_from_already_eta_expanded_var f1 in List.fold_left2 (match_ may_use_eta u alp metas) (match_in u alp metas sigma f1 f2) l1 l2 - | GLambda (_,na1,_,t1,b1), ALambda (na2,t2,b2) -> + | GLambda (_,na1,_,t1,b1), NLambda (na2,t2,b2) -> match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 - | GProd (_,na1,_,t1,b1), AProd (na2,t2,b2) -> + | GProd (_,na1,_,t1,b1), NProd (na2,t2,b2) -> match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 - | GLetIn (_,na1,t1,b1), ALetIn (na2,t2,b2) -> + | GLetIn (_,na1,t1,b1), NLetIn (na2,t2,b2) -> match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 - | GCases (_,sty1,rtno1,tml1,eqnl1), ACases (sty2,rtno2,tml2,eqnl2) + | GCases (_,sty1,rtno1,tml1,eqnl1), NCases (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_glob_constr tml1 rtno1 in - let rtno2' = abstract_return_type_context_aconstr tml2 rtno2 in + let rtno2' = abstract_return_type_context_notation_constr tml2 rtno2 in let sigma = try Option.fold_left2 (match_in u alp metas) sigma rtno1' rtno2' with Option.Heterogeneous -> raise No_match @@ -695,17 +650,17 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 = (fun s (tm1,_) (tm2,_) -> match_in u alp metas s tm1 tm2) sigma tml1 tml2 in List.fold_left2 (match_equations u alp metas) sigma eqnl1 eqnl2 - | GLetTuple (_,nal1,(na1,to1),b1,c1), ALetTuple (nal2,(na2,to2),b2,c2) + | GLetTuple (_,nal1,(na1,to1),b1,c1), NLetTuple (nal2,(na2,to2),b2,c2) when List.length nal1 = List.length nal2 -> let sigma = match_opt (match_binders u alp metas na1 na2) sigma to1 to2 in let sigma = match_in u alp metas sigma b1 b2 in let (alp,sigma) = List.fold_left2 (match_names metas) (alp,sigma) nal1 nal2 in match_in u alp metas sigma c1 c2 - | GIf (_,a1,(na1,to1),b1,c1), AIf (a2,(na2,to2),b2,c2) -> + | GIf (_,a1,(na1,to1),b1,c1), NIf (a2,(na2,to2),b2,c2) -> let sigma = match_opt (match_binders u alp metas na1 na2) sigma to1 to2 in List.fold_left2 (match_in u alp metas) sigma [a1;b1;c1] [a2;b2;c2] - | GRec (_,fk1,idl1,dll1,tl1,bl1), ARec (fk2,idl2,dll2,tl2,bl2) + | GRec (_,fk1,idl1,dll1,tl1,bl1), NRec (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 -> @@ -719,21 +674,21 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 = 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_in u alp metas) sigma bl1 bl2 - | GCast(_,c1,CastConv t1), ACast (c2,CastConv t2) - | GCast(_,c1,CastVM t1), ACast (c2,CastVM t2) -> + | GCast(_,c1,CastConv t1), NCast (c2,CastConv t2) + | GCast(_,c1,CastVM t1), NCast (c2,CastVM t2) -> match_in u alp metas (match_in u alp metas sigma c1 c2) t1 t2 - | GCast(_,c1, CastCoerce), ACast(c2, CastCoerce) -> + | GCast(_,c1, CastCoerce), NCast(c2, CastCoerce) -> match_in u alp metas sigma c1 c2 - | GSort (_,GType _), ASort (GType None) when not u -> sigma - | GSort (_,s1), ASort s2 when s1 = s2 -> sigma - | GPatVar _, AHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match - | a, AHole _ -> sigma + | GSort (_,GType _), NSort (GType None) when not u -> sigma + | GSort (_,s1), NSort s2 when s1 = s2 -> sigma + | GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match + | a, NHole _ -> sigma (* On the fly eta-expansion so as to use notations of the form "exists x, P x" for "ex P"; expects type not given because don't know otherwise how to ensure it corresponds to a well-typed eta-expansion; ensure at least one constructor is consumed to avoid looping *) - | b1, ALambda (Name id,AHole _,b2) when inner -> + | b1, NLambda (Name id,NHole _,b2) when inner -> let id' = Namegen.next_ident_away id (free_glob_vars b1) in match_in u alp metas (bind_binder sigma id [(Name id',Explicit,None,GHole(dummy_loc,Evar_kinds.BinderType (Name id')))]) @@ -758,7 +713,7 @@ and match_equations u alp metas sigma (_,_,patl1,rhs1) (patl2,rhs2) = (alp,sigma) patl1 patl2 in match_in u alp metas sigma rhs1 rhs2 -let match_aconstr u c (metas,pat) = +let match_notation_constr u c (metas,pat) = let vars = list_split_by (fun (_,(_,x)) -> x <> NtnTypeBinderList) metas in let vars = (List.map fst (fst vars), List.map fst (snd vars)) in let terms,termlists,binders = match_ false u [] vars ([],[],[]) c pat in @@ -795,11 +750,11 @@ let bind_env_cases_pattern (sigma,sigmalist,x as fullsigma) var v = let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with - | r1, AVar id2 when List.mem id2 metas -> (bind_env_cases_pattern sigma id2 r1),[] - | PatVar (_,Anonymous), AHole _ -> sigma,[] - | PatCstr (loc,(ind,_ as r1),largs,_), ARef (ConstructRef r2) when r1 = r2 -> + | r1, NVar id2 when List.mem id2 metas -> (bind_env_cases_pattern sigma id2 r1),[] + | PatVar (_,Anonymous), NHole _ -> sigma,[] + | PatCstr (loc,(ind,_ as r1),largs,_), NRef (ConstructRef r2) when r1 = r2 -> sigma,largs - | PatCstr (loc,(ind,_ as r1),args1,_), AApp (ARef (ConstructRef r2),l2) + | PatCstr (loc,(ind,_ as r1),args1,_), NApp (NRef (ConstructRef r2),l2) when r1 = r2 -> let l1 = add_patterns_for_params (fst r1) args1 in let le2 = List.length l2 in @@ -809,7 +764,7 @@ let rec match_cases_pattern metas sigma a1 a2 = else let l1',more_args = Util.list_chop le2 l1 in (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),more_args - | r1, AList (x,_,iter,termin,lassoc) -> + | r1, NList (x,_,iter,termin,lassoc) -> (match_alist (fun (metas,_) -> match_cases_pattern_no_more_args metas) (metas,[]) (pi1 sigma,pi2 sigma,()) r1 x iter termin lassoc),[] | _ -> raise No_match @@ -841,7 +796,7 @@ let reorder_canonically_substitution terms termlists metas = | NtnTypeBinderList -> assert false) metas ([],[]) -let match_aconstr_cases_pattern c (metas,pat) = +let match_notation_constr_cases_pattern c (metas,pat) = let vars = List.map fst metas in let (terms,termlists,()),more_args = match_cases_pattern vars ([],[],()) c pat in reorder_canonically_substitution terms termlists metas,more_args @@ -851,89 +806,6 @@ let match_aconstr_ind_pattern ind args (metas,pat) = let (terms,termlists,()),more_args = match_ind_pattern vars ([],[],()) ind args pat in reorder_canonically_substitution terms termlists metas,more_args -(**********************************************************************) -(*s Concrete syntax for terms *) - -type notation = string - -type explicitation = ExplByPos of int * identifier option | ExplByName of identifier - -type binder_kind = Default of binding_kind | Generalized of binding_kind * binding_kind * bool - -type abstraction_kind = AbsLambda | AbsPi - -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 - | CPatCstrExpl 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_notation_substitution - | CPatPrim of loc * prim_token - | CPatRecord of loc * (reference * cases_pattern_expr) list - | CPatDelimiters of loc * string * cases_pattern_expr - -and cases_pattern_notation_substitution = - cases_pattern_expr list * (** for constr subterms *) - cases_pattern_expr list list (** for recursive notations *) - -type constr_expr = - | CRef of reference - | CFix of loc * identifier located * fix_expr list - | CCoFix of loc * identifier located * cofix_expr list - | 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 - | CRecord of loc * constr_expr option * (reference * constr_expr) list - | CCases of loc * case_style * constr_expr option * - (constr_expr * (name located option * cases_pattern_expr option)) list * - (loc * cases_pattern_expr list located list * constr_expr) list - | CLetTuple of loc * name located list * (name located option * constr_expr option) * - constr_expr * constr_expr - | CIf of loc * constr_expr * (name located option * constr_expr option) - * constr_expr * constr_expr - | CHole of loc * Evar_kinds.t option - | CPatVar of loc * (bool * patvar) - | CEvar of loc * existential_key * constr_expr list option - | CSort of loc * glob_sort - | CCast of loc * constr_expr * constr_expr cast_type - | CNotation of loc * notation * constr_notation_substitution - | CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr - | CPrim of loc * prim_token - | CDelimiters of loc * string * constr_expr - -and fix_expr = - identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr - -and cofix_expr = - identifier located * local_binder list * constr_expr * constr_expr - -and recursion_order_expr = - | CStructRec - | CWfRec of constr_expr - | CMeasureRec of constr_expr * constr_expr option (* measure, relation *) - -and local_binder = - | LocalRawDef of name located * constr_expr - | LocalRawAssum of name located list * binder_kind * constr_expr - -and constr_notation_substitution = - constr_expr list * (* for constr subterms *) - constr_expr list list * (* for recursive notations *) - local_binder list list (* for binders subexpressions *) - -type typeclass_constraint = name located * binding_kind * constr_expr - -and typeclass_context = typeclass_constraint list - -type constr_pattern_expr = constr_expr let oldfashion_patterns = ref (true) let write_oldfashion_patterns = Goptions.declare_bool_option { |