fact: Fixpoint expressionMap (f : Expression -> Expression) (e:Expression) {struct e} : Expression := let mapF := expressionMap f in let listMapF := List.map (expressionMap f) in let optionMapF oe := match oe with | None => None | Some e => Some (expressionMap f e) end in match e with | null => f null | literal l => f (literal l) | new t => f (new t) | newarray t dims um None => f (newarray t (listMapF dims) um None) | newarray t dims um (Some inits) => f (newarray t (listMapF dims) um (Some (listMapF inits))) | method m target params => f (method m (optionMapF target) (listMapF params)) | field fi target => f (field fi (optionMapF target)) | modelField fi target => f (modelField fi (optionMapF target)) | var v => f (var v) | array target index => f (array (mapF target) (mapF index)) | arrayLength target => f (arrayLength (mapF target)) | quantifier q => f (quantifier q) | param p => f (param p) | this => f this | UnaryIntExpr op e => f (UnaryIntExpr op (mapF e)) | UnaryBoolExpr op e => f (UnaryBoolExpr op (mapF e)) | BinaryIntExpr op l r => f (BinaryIntExpr op (mapF l) (mapF r)) | RelationalExpr op l r => f (RelationalExpr op (mapF l) (mapF r)) | BinaryBoolExpr op l r => f (BinaryBoolExpr op (mapF l) (mapF r)) | BinaryCondBoolExpr op l r => f (BinaryCondBoolExpr op (mapF l) (mapF r)) | BinaryRefExpr op l r => f (BinaryRefExpr op (mapF l) (mapF r)) | JMLBinaryBoolExpr op l r => f (JMLBinaryBoolExpr op (mapF l) (mapF r)) | BoolAssignmentExpr op l r => f (BoolAssignmentExpr op (mapF l) (mapF r)) | IntAssignmentExpr op l r => f (IntAssignmentExpr op (mapF l) (mapF r)) | Assignment l r => f (Assignment (mapF l) (mapF r)) | Conditional i t e => f (Conditional (mapF i) (mapF t) (mapF e)) | Cast cl e => f (Cast cl (mapF e)) | Subtype e1 e2 => f (Subtype (mapF e1) (mapF e2)) | InstanceOf e cl => f (InstanceOf (mapF e) cl) | Result => f Result | Old e => f (Old (mapF e)) | OldL e l => f (OldL (mapF e) l) | NotAssigned refs => f (NotAssigned (listMapF refs)) | NotModified refs => f (NotModified (listMapF refs)) | OnlyAccessed refs => f (OnlyAccessed (listMapF refs)) | OnlyAssigned refs => f (OnlyAssigned (listMapF refs)) | OnlyCalled ms => f (OnlyCalled ms) | OnlyCaptured ms => f (OnlyCaptured ms) | Fresh refs => f (Fresh (listMapF refs)) | Reach ref => f (Reach (mapF ref)) | DurationExpr e => f (DurationExpr (mapF e)) | Space e => f (Space (mapF e)) | WorkingSpaceExpr e => f (WorkingSpaceExpr (mapF e)) | TypeOf e => f (TypeOf (mapF e)) | ElemType e => f (ElemType (mapF e)) | GetType t => f (GetType t) | NonNullElements e => f (NonNullElements (mapF e)) | Lockset => f Lockset | MaxObject e => f (MaxObject (mapF e)) | IsInitialized t => f (IsInitialized t) | InvariantFor e => f (InvariantFor (mapF e)) | LblNeg i e => f (LblNeg i (mapF e)) | LblPos i e => f (LblPos i (mapF e)) | Quantification q v r e => f (Quantification q v (mapF r) (mapF e)) end.
imports: JML(JMLProgramPlus) Coq(ZArith) JML(ZHelpers) JML(LogicHelpers) Coq(Bool) Coq(Sumbool) Coq(Ndec) JML(PosAux) JML(EqBoolAux) Coq(Relation_Operators) Coq(List) JML(ListFunctions) JML(ListHelpers) JML(OptionHelpers)