fact: Definition rewriteFullSpecification (specs0:list FULL_SPEC_CASE.t) (m:METHOD.t) (enc:TYPEDEF.t) : list SpecificationCase := let specs1 := desugarAll specs0 m enc in let specs2 := map (fun spec => addDefaults spec m (heavyweightDefaults spec m)) specs1 in let rewrite1 (spec:FULL_SPEC_CASE.t) : SpecificationCase := let (sct,v,r,cc,case) := spec in let (fvd,ovd,sh,body) := case in let vis := match v with None => Public | Some v' => v' end in let clauses := match body with | inl cl => cl | inr _ => nil end in CASE.Build_t vis (hd (FORALL_VAR_DECL.Build_t nil) fvd) (hd (OLD_VAR_DECL.Build_t nil) ovd) (optionalSame2Requires (hd errorRequires (extractRequires false sh))) (TAG.mkBasicClause ensuresT (hd errorEnsures (extractClauses ensuresT false clauses))) (TAG.mkBasicClause signalsT (hd errorSignals (extractClauses signalsT false clauses))) (TAG.mkBasicClause signalsOnlyT (hd errorSignalsOnly (extractClauses signalsOnlyT false clauses))) (TAG.mkBasicClause divergesT (hd errorDiverges (extractClauses divergesT false clauses))) (TAG.mkBasicClause whenT (hd errorWhen (extractClauses whenT false clauses))) (TAG.mkBasicClause assignableT (hd errorAssignable (extractClauses assignableT false clauses))) (TAG.mkBasicClause accessibleT (hd errorAccessible (extractClauses accessibleT false clauses))) (TAG.mkBasicClause callableT (hd errorCallable (extractClauses callableT false clauses))) (TAG.mkBasicClause measuredByT (hd errorMeasuredBy (extractClauses measuredByT false clauses))) (TAG.mkBasicClause capturesT (hd errorCaptures (extractClauses capturesT false clauses))) (TAG.mkBasicClause workingSpaceT (hd errorWorkingSpace (extractClauses workingSpaceT false clauses))) (TAG.mkBasicClause durationT (hd errorDuration (extractClauses durationT false clauses))) (optionalSame2Requires (hd (NotSpecified:optionalSame Expression) (extractRequires true sh))) (TAG.mkBasicClause ensuresT (hd NotSpecified (extractClauses ensuresT true clauses))) (TAG.mkBasicClause signalsT (hd (Exception_e, NotSpecified) (extractClauses signalsT true clauses))) (TAG.mkBasicClause signalsOnlyT (hd nil (extractClauses signalsOnlyT true clauses))) (TAG.mkBasicClause divergesT (hd NotSpecified (extractClauses divergesT true clauses))) (TAG.mkBasicClause whenT (hd NotSpecified (extractClauses whenT true clauses))) (TAG.mkBasicClause assignableT (hd NotSpecified (extractClauses assignableT true clauses))) (TAG.mkBasicClause accessibleT (hd NotSpecified (extractClauses accessibleT true clauses))) (TAG.mkBasicClause callableT (hd NotSpecified (extractClauses callableT true clauses))) (TAG.mkBasicClause measuredByT (hd (NotSpecified, None) (extractClauses measuredByT true clauses))) (TAG.mkBasicClause capturesT (hd NotSpecified (extractClauses capturesT true clauses))) (TAG.mkBasicClause workingSpaceT (hd (NotSpecified, None) (extractClauses workingSpaceT true clauses))) (TAG.mkBasicClause durationT (hd (NotSpecified, None) (extractClauses durationT true clauses))) r cc in map rewrite1 specs2.
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)