fact: Definition desugarMultiple (specs:list FULL_SPEC_CASE.t) : list FULL_SPEC_CASE.t := let desugar1Clauses (l:list MethodSpecClause) : list MethodSpecClause := let ens := mergeEnsures (extractClauses ensuresT false l) in let sig := mergeSignals (extractClauses signalsT false l) in let sgo := mergeSignalsOnly (extractClauses signalsOnlyT false l) in let div := mergeDiverges (extractClauses divergesT false l) in let whe := mergeWhen (extractClauses whenT false l) in let ass := mergeAssignable (extractClauses assignableT false l) in let acc := mergeAccessible (extractClauses accessibleT false l) in let cal := mergeCallable (extractClauses callableT false l) in let mea := mergeMeasuredBy (extractClauses measuredByT false l) in let cap := mergeCaptures (extractClauses capturesT false l) in let wor := mergeWorkingSpace (extractClauses workingSpaceT false l) in let dur := mergeDuration (extractClauses durationT false l) in let rens := mergeEnsures (extractClauses ensuresT true l) in let rsig := mergeSignals (extractClauses signalsT true l) in let rsgo := mergeSignalsOnly (extractClauses signalsOnlyT true l) in let rdiv := mergeDiverges (extractClauses divergesT true l) in let rwhe := mergeWhen (extractClauses whenT true l) in let rass := mergeAssignable (extractClauses assignableT true l) in let racc := mergeAccessible (extractClauses accessibleT true l) in let rcal := mergeCallable (extractClauses callableT true l) in let rmea := mergeMeasuredBy (extractClauses measuredByT true l) in let rcap := mergeCaptures (extractClauses capturesT true l) in let rwor := mergeWorkingSpace (extractClauses workingSpaceT true l) in let rdur := mergeDuration (extractClauses durationT true l) in let optionClauses := optionMap (ensuresC false) ens :: optionMap (signalsC false) sig :: optionMap (signalsOnlyC false) sgo :: optionMap (divergesC false) div :: optionMap (whenC false) whe :: optionMap (assignableC false) ass :: optionMap (accessibleC false) acc :: optionMap (callableC false) cal :: optionMap (measuredByC false) mea :: optionMap (capturesC false) cap :: optionMap (workingSpaceC false) wor :: optionMap (durationC false) dur :: optionMap (ensuresC true) rens :: optionMap (signalsC true) rsig :: optionMap (signalsOnlyC true) rsgo :: optionMap (divergesC true) rdiv :: optionMap (whenC true) rwhe :: optionMap (assignableC true) rass :: optionMap (accessibleC true) racc :: optionMap (callableC true) rcal :: optionMap (measuredByC true) rmea :: optionMap (capturesC true) rcap :: optionMap (workingSpaceC true) rwor :: optionMap (durationC true) rdur :: nil in optionList2list optionClauses in let fix desugar1Case (case:GENERIC_SPEC_CASE.t) : GENERIC_SPEC_CASE.t := let (fvd0,ovd0,sh0,body0) := case in let fvd1 := option2list (mergeForallVarDecl fvd0) in let ovd1 := option2list (mergeOldVarDecl ovd0) in let sh0r := extractRequires true sh0 in let sh0nr := extractRequires false sh0 in let sh1r := optionMap (requiresSH true) (mergeRequires sh0r) in let sh1nr := optionMap (requiresSH false) (mergeRequires sh0nr) in let sh1 := optionList2list (sh1nr :: sh1r :: nil) in let body1 := match body0 with | inl cl => inl _ (desugar1Clauses cl) | inr nested => inr _ (map desugar1Case nested) end in GENERIC_SPEC_CASE.Build_t fvd1 ovd1 sh1 body1 in let desugar1 (spec:FULL_SPEC_CASE.t) : FULL_SPEC_CASE.t := let (sct,v,r,cc,case) := spec in FULL_SPEC_CASE.Build_t sct v r cc (desugar1Case case) in map desugar1 specs.
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)