diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 4 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 2 | ||||
| -rw-r--r-- | pretyping/rawterm.ml | 32 | ||||
| -rw-r--r-- | pretyping/rawterm.mli | 4 |
4 files changed, 36 insertions, 6 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index da417f44d..1ae4d96fa 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1032,7 +1032,7 @@ let rec generalize_problem names pb = function tomatch = Abstract d :: tomatch; pred = generalize_predicate names i d pb.tomatch pb'.pred } -(* No more patterns: typing the right-hand-side of equations *) +(* No more patterns: typing the right-hand side of equations *) let build_leaf pb = let rhs = extract_rhs pb in let j = pb.typing_function (mk_tycon pb.pred) rhs.rhs_env pb.evdref rhs.it in @@ -1669,7 +1669,7 @@ let prepare_predicate loc typing_fun evdref env tomatchs sign tycon pred = let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, eqns) = - (* We build the matrix of patterns and right-hand-side *) + (* We build the matrix of patterns and right-hand side *) let matx = matx_of_eqns env tomatchl eqns in (* We build the vector of terms to match consistently with the *) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 9113efd55..01d1b8b00 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -362,6 +362,8 @@ let detype_sort = function | Prop c -> RProp c | Type u -> RType (Some u) +type binder_kind = BProd | BLambda | BLetIn + (**********************************************************************) (* Main detyping function *) 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' diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 2498af7b5..242244bd6 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -33,8 +33,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 @@ -105,6 +103,8 @@ val map_rawconstr_with_binders_loc : loc -> ('a -> rawconstr -> rawconstr) -> 'a -> rawconstr -> rawconstr *) +val fold_rawconstr : ('a -> rawconstr -> 'a) -> 'a -> rawconstr -> 'a +val iter_rawconstr : (rawconstr -> unit) -> rawconstr -> unit val occur_rawconstr : identifier -> rawconstr -> bool val free_rawvars : rawconstr -> identifier list val loc_of_rawconstr : rawconstr -> loc |