diff options
author | 2010-07-22 21:06:18 +0000 | |
---|---|---|
committer | 2010-07-22 21:06:18 +0000 | |
commit | fc06cb87286e2b114c7f92500511d5914b8f7f48 (patch) | |
tree | 71b120c836f660f7fa4a47447854b8859a2caf27 /pretyping/rawterm.ml | |
parent | 1f798216ede7e3813d75732fbebc1f8fbf6622c5 (diff) |
Extension of the recursive notations mechanism
- Added support for recursive notations with binders
- Added support for arbitrary large iterators in recursive notations
- More checks on the use of variables and improved error messages
- Do side-effects in metasyntax only when sure that everything is ok
- Documentation
Note: it seems there were a small bug in match_alist (instances obtained
from matching the first copy of iterator were not propagated).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13316 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/rawterm.ml')
-rw-r--r-- | pretyping/rawterm.ml | 32 |
1 files changed, 30 insertions, 2 deletions
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index fb6bf8545..6dbaebc46 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -32,8 +32,6 @@ type patvar = identifier type rawsort = RProp of Term.contents | RType of Univ.universe option -type binder_kind = BProd | BLambda | BLetIn - type binding_kind = Lib.binding_kind = Explicit | Implicit type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier @@ -183,6 +181,36 @@ let map_rawconstr_with_binders_loc loc g f e = function | RDynamic (_,x) -> RDynamic (loc,x) *) +let fold_rawconstr f acc = + let rec fold acc = function + | RVar _ -> acc + | RApp (_,c,args) -> List.fold_left fold (fold acc c) args + | RLambda (_,_,_,b,c) | RProd (_,_,_,b,c) | RLetIn (_,_,b,c) -> + fold (fold acc b) c + | RCases (_,_,rtntypopt,tml,pl) -> + List.fold_left fold_pattern + (List.fold_left fold (Option.fold_left fold acc rtntypopt) (List.map fst tml)) + pl + | RLetTuple (_,_,rtntyp,b,c) -> + fold (fold (fold_return_type acc rtntyp) b) c + | RIf (_,c,rtntyp,b1,b2) -> + fold (fold (fold (fold_return_type acc rtntyp) c) b1) b2 + | RRec (_,_,_,bl,tyl,bv) -> + let acc = Array.fold_left + (List.fold_left (fun acc (na,k,bbd,bty) -> + fold (Option.fold_left fold acc bbd) bty)) acc bl in + Array.fold_left fold (Array.fold_left fold acc tyl) bv + | RCast (_,c,k) -> fold (match k with CastConv (_, t) -> fold acc t | CastCoerce -> acc) c + | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> acc + + and fold_pattern acc (_,idl,p,c) = fold acc c + + and fold_return_type acc (na,tyopt) = Option.fold_left fold acc tyopt + + in fold acc + +let iter_rawconstr f = fold_rawconstr (fun () -> f) () + let occur_rawconstr id = let rec occur = function | RVar (loc,id') -> id = id' |