Movatterモバイル変換

[0]ホーム
URL:

Skip to content

Navigation Menu

Sign in
Appearance settings

Search code, repositories, users, issues, pull requests...

Provide feedback

We read every piece of feedback, and take your input very seriously.

Saved searches

Use saved searches to filter your results more quickly

 Sign up
Appearance settings

Commitaf6fe4e

Browse files
andrewjkennedylatkin
andrewjkennedy
authored andcommitted
Support for rational exponents in units of measure
commit fd77e404911ea3948d8d6b59c9a53522eba2cef4Author: latkin <latkin@microsoft.com>Date: Wed Jan 7 17:15:14 2015 -0800 Further overflow/parsing fixes: check denominators, convert to bigint before negationcommit 09e892b3eda586775767cef1866c994ace07d217Author: andrewjkennedy <akenn@microsoft.com>Date: Wed Jan 7 11:40:53 2015 +0000 Make parsing of -2147483648 in rational exponents an errorcommit 050b8b67c30c6857353d70449955c9872939b42aAuthor: latkin <latkin@microsoft.com>Date: Tue Jan 6 14:48:11 2015 -0800 Remove unused error messagecommit 75b99d8561ff9aee087dc856cde106d6b4053622Author: latkin <latkin@microsoft.com>Date: Tue Jan 6 14:35:07 2015 -0800 Deleting obsolete testscommit ac97bcb9eb1079381c50071b5e3d95e21f21a12cMerge:f11c636 1877dffAuthor: latkin <latkin@microsoft.com>Date: Mon Jan 5 15:58:51 2015 -0800 Merge branch 'unitsexprat' ofhttps://git01.codeplex.com/forks/andrewjkennedy/fsharpcontrib into rationalexp Conflicts: src/fsharp/FSComp.txtcommit 1877dff5235e538b6b406a17478ce9b81bad735bAuthor: andrewjkennedy <akenn@microsoft.com>Date: Tue Dec 30 12:08:50 2014 +0000 Testscommit f7255be543782ae2aa5ed570c731eeb74d2205a1Author: andrewjkennedy <akenn@microsoft.com>Date: Mon Dec 29 15:37:59 2014 +0000 Added ref to System.Numericscommit 47180d60e4607233efe8a52be3f241c478793684Author: andrewjkennedy <akenn@microsoft.com>Date: Mon Dec 29 15:18:48 2014 +0000 Parsing of rational exponents is brokencommit b5ce68705045ed9944183f8238c478f7db575aa5Author: andrewjkennedy <akenn@microsoft.com>Date: Mon Dec 29 13:47:26 2014 +0000 Revert "Overflow exception catching" This reverts commit 9259f5374d0d4f20f0fb5fb4ef43e0eba71027ae.commit 11e1ed21ccf05a0552c97d635c3b91e6e6397691Author: andrewjkennedy <akenn@MSRC-3617024.europe.corp.microsoft.com>Date: Mon Dec 29 13:30:21 2014 +0000 Use BigIntegers for rationalscommit 9259f5374d0d4f20f0fb5fb4ef43e0eba71027aeAuthor: andrewjkennedy <akenn@MSRC-3617024.europe.corp.microsoft.com>Date: Mon Dec 29 13:29:23 2014 +0000 Overflow exception catchingcommit 3b835e9b20e580b01bac7e81ea53cfaa36ac06c5Author: andrewjkennedy <akenn@MSRC-3617024.europe.corp.microsoft.com>Date: Mon Nov 3 17:38:57 2014 +0000 Error message for non-parenthesized unitscommit 3160dbbac9e9e2799eb3fe13239525fa8ce8c568Author: andrewjkennedy <akenn@MSRC-3617024.europe.corp.microsoft.com>Date: Mon Nov 3 16:18:31 2014 +0000 Improved error when parentheses are omitted from exponentcommit f24e688d7794263f7dabb40f4ac9a498e82d517dAuthor: andrewjkennedy <akenn@MSRC-3617024.europe.corp.microsoft.com>Date: Mon Nov 3 13:24:59 2014 +0000 Negative test for rational exponent parsingcommit 1e55326403626df25776226501bc8fedfc089adbAuthor: andrewjkennedy <akenn@MSRC-3617024.europe.corp.microsoft.com>Date: Mon Nov 3 11:21:05 2014 +0000 Zero denominator testcommit f50f36f8603420298316ce966eb2e156e4052839Author: andrewjkennedy <akenn@MSRC-3617024.europe.corp.microsoft.com>Date: Mon Nov 3 11:07:47 2014 +0000 Small improvements as suggested by Doncommit 71fe676f97bf06dbf165defb0b1e10a250266126Author: andrewjkennedy <akenn@MSRC-3617024.europe.corp.microsoft.com>Date: Mon Nov 3 11:07:02 2014 +0000 Some positive tests for rational exponentscommit 0ac8fdc68ba807920c22b212be549751aa141548Author: andrewjkennedy <akenn@MSRC-3617024.europe.corp.microsoft.com>Date: Thu Oct 30 13:44:44 2014 +0000 Fix bug on too many measure variables e.g. let f(x:float<'a 'b>) = x;;commit 2a227d0f4463d117f3022b34a18733e3b98d8594Author: andrewjkennedy <akenn@MSRC-3617024.europe.corp.microsoft.com>Date: Thu Oct 30 10:58:49 2014 +0000 Check for 0 denominatorcommit 67acf8465ea5bfcb8766f7045ba5b47bf1a51fc5Author: andrewjkennedy <akenn@MSRC-3617024.europe.corp.microsoft.com>Date: Thu Oct 30 10:41:05 2014 +0000 Couple of non-integer exponent testscommit 89881e2a94cf0e220051d68393d5e184ddc4634eAuthor: andrewjkennedy <akenn@MSRC-3617024.europe.corp.microsoft.com>Date: Thu Oct 30 10:16:18 2014 +0000 u_rational should be outside #ifdefcommit 8461d5ee8632e15555680bc41cfea241f5ad7e5dAuthor: andrewjkennedy <akenn@MSRC-3617024.europe.corp.microsoft.com>Date: Wed Oct 29 11:05:14 2014 +0000 Updated commentscommit c9da07d8f06311e2e62958e675f8082329651bf1Author: andrewjkennedy <akenn@MSRC-3617024.europe.corp.microsoft.com>Date: Wed Oct 29 10:40:09 2014 +0000 Parentheses Revert LessGeneric testcommit b6090279f81f6583d5a2bec18eeaebb308506148Author: andrewjkennedy <akenn@MSRC-3617024.europe.corp.microsoft.com>Date: Tue Oct 28 15:42:18 2014 +0000 Negative test baseline - can now take sqrt of m!commit a69bfc41a0184784bee44c7a08f3206525b1ce81Author: andrewjkennedy <akenn@MSRC-3617024.europe.corp.microsoft.com>Date: Tue Oct 28 14:58:50 2014 +0000 Simplification to simplification: compute reduced row echelon form then normalize exponents Syntax of negative rationals: permit either u^-(2/3) or u^(-2/3)commit 4a6143daaf38909d5b75e34d5fd4b036f4b862ccAuthor: andrewjkennedy <akenn@MSRC-3617024.europe.corp.microsoft.com>Date: Tue Oct 28 11:21:17 2014 +0000 More efficient representation of measures. Separate rational implementation. Better simplified form.commit 323d627288948359795797060216d8fe7d4676cfAuthor: andrewjkennedy <akenn@MSRC-3617024.europe.corp.microsoft.com>Date: Fri Oct 17 13:46:54 2014 +0100 Normalization of unit variable exponents in type schemes Insist on parentheses around rational constants - otherwise how do we parse float<kg^2/s> Still an issue with warnings wrt "too generic"commit 547444819d02f7df2f49b69c5ef32b039d58859bAuthor: andrewjkennedy <akenn@MSRC-3617024.europe.corp.microsoft.com>Date: Thu Oct 16 14:53:43 2014 +0100 Comment out measure unification algorithm and replace with one that makes use of rational exponents. Simpolification of type schemes will currently fail if any unit variables have non-integer exponent.commit 82b5fe40c907aae75036982dc7a4b168410e66e1Author: andrewjkennedy <akenn@MSRC-3617024.europe.corp.microsoft.com>Date: Thu Oct 16 14:33:58 2014 +0100 TAST support for rational exponents; pretty-printing; pickling Solver currently projects out integers, fails on non-integerscommit d558956a1476d79b6aaa52e6ccf6d1f2f5372dacAuthor: andrewjkennedy <akenn@MSRC-3617024.europe.corp.microsoft.com>Date: Thu Oct 16 11:52:49 2014 +0100 Implement syntax for rational exponents in units-of-measure Flag syntax error in type-checker if rational exponent encountered, for now
1 parent30ed635 commitaf6fe4e

File tree

26 files changed

+397
-181
lines changed

26 files changed

+397
-181
lines changed

‎src/fsharp/FSComp.txt‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -475,6 +475,7 @@ parsMultiArgumentGenericTypeFormDeprecated,"The syntax '(typ,...,typ) ident' is
475475
622,parsMismatchedQuotationName,"Mismatched quotation operator name, beginning with '%s'"
476476
623,parsActivePatternCaseMustBeginWithUpperCase,"Active pattern case identifiers must begin with an uppercase letter"
477477
624,parsActivePatternCaseContainsPipe,"The '|' character is not permitted in active pattern case identifiers"
478+
625,parsIllegalDenominatorForMeasureExponent,"Denominator must not be 0 in unit-of-measure exponent"
478479
parsNoEqualShouldFollowNamespace,"No '=' symbol should follow a 'namespace' declaration"
479480
parsSyntaxModuleStructEndDeprecated,"The syntax 'module ... = struct .. end' is not used in F# code. Consider using 'module ... = begin .. end'"
480481
parsSyntaxModuleSigEndDeprecated,"The syntax 'module ... : sig .. end' is not used in F# code. Consider using 'module ... = begin .. end'"

‎src/fsharp/FSharp.Compiler-proto/FSharp.Compiler-proto.fsproj‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -179,6 +179,12 @@
179179
<CompileInclude="..\range.fs">
180180
<Link>range.fs</Link>
181181
</Compile>
182+
<CompileInclude="..\rational.fsi">
183+
<Link>rational.fsi</Link>
184+
</Compile>
185+
<CompileInclude="..\rational.fs">
186+
<Link>rational.fs</Link>
187+
</Compile>
182188
<CompileInclude="..\ErrorLogger.fs">
183189
<Link>ErrorLogger.fs</Link>
184190
</Compile>

‎src/fsharp/FSharp.Compiler/FSharp.Compiler.fsproj‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -135,6 +135,12 @@
135135
<CompileInclude="..\TraceCall.fs">
136136
<Link>Utilities\TraceCall.fs</Link>
137137
</Compile>
138+
<CompileInclude="..\rational.fsi">
139+
<Link>ErrorLogging\rational.fsi</Link>
140+
</Compile>
141+
<CompileInclude="..\rational.fs">
142+
<Link>ErrorLogging\rational.fs</Link>
143+
</Compile>
138144
<CompileInclude="..\range.fsi">
139145
<Link>ErrorLogging\range.fsi</Link>
140146
</Compile>
@@ -501,6 +507,7 @@
501507
<ReferenceInclude="mscorlib" />
502508
<ReferenceInclude="System" />
503509
<ReferenceInclude="System.Core" />
510+
<ReferenceInclude="System.Numerics" />
504511
<ReferenceInclude="System.Drawing" />
505512
<ReferenceInclude="System.Windows.Forms" />
506513
<ReferenceInclude="System.Runtime.Remoting" />

‎src/fsharp/FSharp.LanguageService.Compiler/FSharp.LanguageService.Compiler.fsproj‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -197,6 +197,12 @@
197197
<CompileInclude="..\range.fs">
198198
<Link>range.fs</Link>
199199
</Compile>
200+
<CompileInclude="..\rational.fsi">
201+
<Link>rational.fsi</Link>
202+
</Compile>
203+
<CompileInclude="..\rational.fs">
204+
<Link>rational.fs</Link>
205+
</Compile>
200206
<CompileInclude="..\ErrorLogger.fs">
201207
<Link>ErrorLogger.fs</Link>
202208
</Compile>
@@ -450,6 +456,7 @@
450456
<ReferenceInclude="mscorlib" />
451457
<ReferenceInclude="System" />
452458
<ReferenceInclude="System.Core" />
459+
<ReferenceInclude="System.Numerics" />
453460
<ReferenceInclude="System.Drawing" />
454461
<ReferenceInclude="System.Windows.Forms" />
455462
<ReferenceInclude="System.Runtime.Remoting" />

‎src/fsharp/NicePrint.fs‎

Lines changed: 9 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ open Microsoft.FSharp.Compiler.AbstractIL.Internal.Library
1616
openMicrosoft.FSharp.Compiler
1717
openMicrosoft.FSharp.Compiler.AbstractIL.Diagnostics
1818
openMicrosoft.FSharp.Compiler.Range
19+
openMicrosoft.FSharp.Compiler.Rational
1920
openMicrosoft.FSharp.Compiler.Ast
2021
openMicrosoft.FSharp.Compiler.ErrorLogger
2122
openMicrosoft.FSharp.Compiler.Tast
@@ -814,14 +815,16 @@ module private PrintTypes =
814815
andprivatelayoutMeasure denv unt=
815816
letsortVars vs= vs|> List.sortBy(fun(v:Typar,_)-> v.DisplayName)
816817
letsortCons cs= cs|> List.sortBy(fun(c:TyconRef,_)-> c.DisplayName)
817-
letnegvs,posvs= ListMeasureVarOccsWithNonZeroExponents unt|> sortVars|> List.partition(fun(_,e)->e<0)
818-
letnegcs,poscs= ListMeasureConOccsWithNonZeroExponents denv.gfalse unt|> sortCons|> List.partition(fun(_,e)->e<0)
818+
letnegvs,posvs= ListMeasureVarOccsWithNonZeroExponents unt|> sortVars|> List.partition(fun(_,e)->SignRational e<0)
819+
letnegcs,poscs= ListMeasureConOccsWithNonZeroExponents denv.gfalse unt|> sortCons|> List.partition(fun(_,e)->SignRational e<0)
819820
letunparL uv= layoutTyparRef denv uv
820821
letunconL tc= layoutTyconRef denv tc
821-
letprefix= spaceListL(List.map(fun(v,e)->if e=1then unparL velse unparL v-- wordL(sprintf"^%d" e)) posvs@
822-
List.map(fun(c,e)->if e=1then unconL celse unconL c-- wordL(sprintf"^%d" e)) poscs)
823-
letpostfix= spaceListL(List.map(fun(v,e)->if e=-1then unparL velse unparL v-- wordL(sprintf"^%d"(-e))) negvs@
824-
List.map(fun(c,e)->if e=-1then unconL celse unconL c-- wordL(sprintf"^%d"(-e))) negcs)
822+
letrationalL e= wordL(RationalToString e)
823+
letmeasureToPowerL x e=if e= OneRationalthen xelse x-- wordL"^"-- rationalL e
824+
letprefix= spaceListL(List.map(fun(v,e)-> measureToPowerL(unparL v) e) posvs@
825+
List.map(fun(c,e)-> measureToPowerL(unconL c) e) poscs)
826+
letpostfix= spaceListL(List.map(fun(v,e)-> measureToPowerL(unparL v)(NegRational e)) negvs@
827+
List.map(fun(c,e)-> measureToPowerL(unconL c)(NegRational e)) negcs)
825828
match(negvs,negcs)with
826829
|[],[]->(match posvs,poscswith[],[]-> wordL"1"|_-> prefix)
827830
|_-> prefix^^ sepL"/"^^(if List.length negvs+ List.length negcs>1then sepL"("^^ postfix^^ sepL")"else postfix)

‎src/fsharp/ast.fs‎

Lines changed: 12 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -255,11 +255,20 @@ and
255255
| ProductofSynMeasure*SynMeasure*range
256256
| SeqofSynMeasurelist*range
257257
| DivideofSynMeasure*SynMeasure*range
258-
| PowerofSynMeasure*int*range
258+
| PowerofSynMeasure*SynRationalConst*range
259259
| One
260260
| Anonofrange
261261
| VarofSynTypar*range
262262

263+
and
264+
[<NoEquality; NoComparison; RequireQualifiedAccess>]
265+
/// The unchecked abstract syntax tree of F# unit of measure exponents.
266+
SynRationalConst=
267+
| Integerofint32
268+
| Rationalofint32*int32*range
269+
| NegateofSynRationalConst
270+
271+
263272
//------------------------------------------------------------------------
264273
// AST: the grammar of types, expressions, declarations etc.
265274
//-----------------------------------------------------------------------
@@ -423,8 +432,8 @@ and
423432
| HashConstraintofSynType*range
424433
/// F# syntax : for units of measure e.g. m / s
425434
| MeasureDivideofSynType*SynType*range
426-
/// F# syntax : for units of measure e.g. m^3
427-
| MeasurePowerofSynType*int*range
435+
/// F# syntax : for units of measure e.g. m^3, kg^1/2
436+
| MeasurePowerofSynType*SynRationalConst*range
428437
/// F# syntax : 1, "abc" etc, used in parameters to type providers
429438
/// For the dimensionless units i.e. 1 , and static parameters to provided types
430439
| StaticConstantofSynConst*range

‎src/fsharp/csolve.fs‎

Lines changed: 80 additions & 81 deletions
Original file line numberDiff line numberDiff line change
@@ -39,6 +39,7 @@ open Microsoft.FSharp.Compiler
3939

4040
openMicrosoft.FSharp.Compiler.AbstractIL.Diagnostics
4141
openMicrosoft.FSharp.Compiler.Range
42+
openMicrosoft.FSharp.Compiler.Rational
4243
openMicrosoft.FSharp.Compiler.Ast
4344
openMicrosoft.FSharp.Compiler.ErrorLogger
4445
openMicrosoft.FSharp.Compiler.Tast
@@ -358,20 +359,20 @@ let PreferUnifyTypar (v1:Typar) (v2:Typar) =
358359

359360

360361

361-
///Ensure that vs is orderedso thatan element with minimum sized exponent
362-
/// is at the head of the list. Also, if possible, this element should have rigidity TyparRigidity.Flexible
363-
letFindMinimumMeasureExponent vs=
364-
let recfindmin vs=
362+
///Reorder a list of (variable,exponent) pairsso thata variable that is Preferred
363+
/// is at the head of the list, if possible
364+
letFindPreferredTypar vs=
365+
let recfind vs=
365366
match vswith
366367
|[]-> vs
367368
|(v:Typar,e)::vs->
368-
matchfindmin vswith
369+
matchfind vswith
369370
|[]->[(v,e)]
370-
|(v',e')::vs'->
371-
ifabs e< abs e'||(abs e= abs e'&&PreferUnifyTypar v v')
371+
|(v',e')::vs'->
372+
if PreferUnifyTypar v v'
372373
then(v, e):: vs
373374
else(v',e')::(v,e):: vs'
374-
findmin vs
375+
find vs
375376

376377
letSubstMeasure(r:Typar)ms=
377378
if r.Rigidity= TyparRigidity.Rigidthen error(InternalError("SubstMeasure: rigid",r.Range));
@@ -447,88 +448,53 @@ let SubstMeasureWarnIfRigid (csenv:ConstraintSolverEnv) trace (v:Typar) ms =
447448
WarnD(Error(FSComp.SR.csCodeLessGeneric(),v.Range))
448449
else CompleteD)
449450

450-
/// The division operator in Caml/F# rounds towards zero. For our purposes,
451-
/// we want to round towards negative infinity.
452-
letDivRoundDown x y=
453-
letsignx=if x<0then-1else1
454-
letsigny=if y<0then-1else1
455-
456-
if signx=signythen x/ y
457-
else(x-y+signy)/ y
458-
459451
/// Imperatively unify the unit-of-measure expression ms against 1.
460-
/// This is a gcd-like algorithm that proceeds as follows:
461-
/// 1. Express ms in the form 'u1^x1 * ... * 'un^xn * c1^y1 * ... * cm^ym
462-
/// where 'u1,...,'un are non-rigid measure variables, c1,...,cm are measure identifiers or rigid measure variables,
463-
/// x1,...,xn and y1,...,yn are non-zero exponents with |x1| <= |xi| for all i.
464-
/// 2. (a) If m=n=0 then we're done (we're unifying 1 against 1)
465-
/// (b) If m=0 but n<>0 then fail (we're unifying a variable-free expression against 1)
466-
/// (c) If xi is divisible by |x1| for all i, and yj is divisible by |x1| for all j, then
467-
/// immediately solve the constraint with the substitution
468-
/// 'u1 := 'u2^(-x2/x1) * ... * 'un^(-xn/x1) * c1^(-y1/x1) * ... * cm^(-ym/x1)
469-
/// (d) Otherwise, if m=1, fail (example: unifying 'u^2 * kg^3)
470-
/// (e) Otherwise, make the substitution
471-
/// 'u1 := 'u * 'u2^(-x2/x1) * ... * 'un^(-xn/x1) * c1^(-y1/x1) * ... * cm^(-ym/x1)
472-
/// where 'u is a fresh measure variable, and iterate.
473-
474-
let recUnifyMeasureWithOne(csenv:ConstraintSolverEnv)trace ms=
452+
/// There are three cases
453+
/// - ms is (equivalent to) 1
454+
/// - ms contains no non-rigid unit variables, and so cannot be unified with 1
455+
/// - ms has the form v^e * ms' for some non-rigid variable v, non-zero exponent e, and measure expression ms'
456+
/// the most general unifier is then simply v := ms' ^ -(1/e)
457+
letUnifyMeasureWithOne(csenv:ConstraintSolverEnv)trace ms=
458+
// Gather the rigid and non-rigid unit variables in this measure expression together with their exponents
475459
let(rigidVars,nonRigidVars)=(ListMeasureVarOccsWithNonZeroExponents ms)|> List.partition(fun(v,_)-> v.Rigidity= TyparRigidity.Rigid)
476-
letexpandedCons= ListMeasureConOccsWithNonZeroExponents csenv.gtrue ms
477-
letunexpandedCons= ListMeasureConOccsWithNonZeroExponents csenv.gfalse ms
478-
match FindMinimumMeasureExponent nonRigidVars, rigidVars, expandedCons, unexpandedConswith
479-
|[],[],[],_-> CompleteD
480-
|[],_,_,_-> localAbortD
481-
|(v,e)::vs, rigidVars,_,_->
482-
// don't break up abbreviations if we can help it!
483-
if unexpandedCons|> List.forall(fun(_,e')-> e'% e=0)&&(vs@rigidVars)|> List.forall(fun(_,e')-> e'% e=0)
484-
then
485-
letnewms= ProdMeasures(List.map(fun(c,e')-> MeasurePower(MeasureCon c)(-(DivRoundDown e' e))) unexpandedCons
486-
@ List.map(fun(v,e')-> MeasurePower(MeasureVar v)(-(DivRoundDown e' e)))(vs@ rigidVars))
487-
SubstMeasureWarnIfRigid csenv trace v newms
488-
else
489-
letnewms= ProdMeasures(List.map(fun(c,e')-> MeasurePower(MeasureCon c)(-(DivRoundDown e' e))) expandedCons
490-
@ List.map(fun(v,e')-> MeasurePower(MeasureVar v)(-(DivRoundDown e' e)))(vs@ rigidVars))
491-
if expandedCons|> List.forall(fun(_,e')-> e'% e=0)&&(vs@rigidVars)|> List.forall(fun(_,e')-> e'% e=0)
492-
then SubstMeasureWarnIfRigid csenv trace v newms
493-
elif isNil vs
494-
then localAbortD
495-
else
496-
// New variable v' must inherit WarnIfNotRigid from v
497-
letv'= NewAnonTypar(TyparKind.Measure,v.Range,v.Rigidity,v.StaticReq,v.DynamicReq)
498-
SubstMeasure v(MeasureProd(MeasureVar v', newms));
499-
UnifyMeasureWithOne csenv trace ms
500460

461+
// If there is at least one non-rigid variable v with exponent e, then we can unify
462+
match FindPreferredTypar nonRigidVarswith
463+
|(v,e)::vs->
464+
letunexpandedCons= ListMeasureConOccsWithNonZeroExponents csenv.gfalse ms
465+
letnewms= ProdMeasures(List.map(fun(c,e')-> MeasureRationalPower(MeasureCon c, NegRational(DivRational e' e))) unexpandedCons
466+
@ List.map(fun(v,e')-> MeasureRationalPower(MeasureVar v, NegRational(DivRational e' e)))(vs@ rigidVars))
467+
468+
SubstMeasureWarnIfRigid csenv trace v newms
469+
470+
// Otherwise we require ms to be 1
471+
|[]->
472+
if measureEquiv csenv.g ms MeasureOnethen CompleteDelse localAbortD
473+
501474
/// Imperatively unify unit-of-measure expression ms1 against ms2
502475
letUnifyMeasures(csenv:ConstraintSolverEnv)trace ms1 ms2=
503476
UnifyMeasureWithOne csenv trace(MeasureProd(ms1,MeasureInv ms2))
504477

505-
506478
/// Simplify a unit-of-measure expression ms that forms part of a type scheme.
507479
/// We make substitutions for vars, which are the (remaining) bound variables
508480
/// in the scheme that we wish to simplify.
509481
letSimplifyMeasure g vars ms=
510482
let recsimp vars=
511-
matchFindMinimumMeasureExponent(List.filter(fun(_,e)-> e<>0)(List.map(fun v->(v, MeasureVarExponent v ms)) vars))with
483+
matchFindPreferredTypar(List.filter(fun(_,e)-> SignRational e<>0)(List.map(fun v->(v, MeasureVarExponent v ms)) vars))with
512484
|[]->
513485
(vars, None)
514486

515487
|(v,e)::vs->
516-
if e<0then
517-
letv'= NewAnonTypar(TyparKind.Measure,v.Range,TyparRigidity.Flexible,v.StaticReq,v.DynamicReq)
518-
letvars'= v':: ListSet.remove typarEq v vars
519-
SubstMeasure v(MeasureInv(MeasureVar v'));
520-
simp vars'
521-
else
522-
letnewv=if v.IsCompilerGeneratedthen NewAnonTypar(TyparKind.Measure,v.Range,TyparRigidity.Flexible,v.StaticReq,v.DynamicReq)
523-
else NewNamedInferenceMeasureVar(v.Range,TyparRigidity.Flexible,v.StaticReq,v.Id)
524-
letremainingvars= ListSet.remove typarEq v vars
525-
letnewms=(ProdMeasures(List.map(fun(c,e')-> MeasurePower(MeasureCon c)(-(DivRoundDown e' e)))(ListMeasureConOccsWithNonZeroExponents gfalse ms)
526-
@ List.map(fun(v',e')->if typarEq v v'then MeasureVar newvelse MeasurePower(MeasureVar v')(-(DivRoundDown e' e)))(ListMeasureVarOccsWithNonZeroExponents ms)));
527-
SubstMeasure v newms;
528-
match vswith
529-
|[]->(remainingvars, Some newv)
530-
|_-> simp(newv::remainingvars)
531-
488+
letnewvar=if v.IsCompilerGeneratedthen NewAnonTypar(TyparKind.Measure,v.Range,TyparRigidity.Flexible,v.StaticReq,v.DynamicReq)
489+
else NewNamedInferenceMeasureVar(v.Range,TyparRigidity.Flexible,v.StaticReq,v.Id)
490+
letremainingvars= ListSet.remove typarEq v vars
491+
letnewvarExpr=if SignRational e<0then MeasureInv(MeasureVar newvar)else MeasureVar newvar
492+
letnewms=(ProdMeasures(List.map(fun(c,e')-> MeasureRationalPower(MeasureCon c, NegRational(DivRational e' e)))(ListMeasureConOccsWithNonZeroExponents gfalse ms)
493+
@ List.map(fun(v',e')->if typarEq v v'then newvarExprelse MeasureRationalPower(MeasureVar v', NegRational(DivRational e' e)))(ListMeasureVarOccsWithNonZeroExponents ms)));
494+
SubstMeasure v newms;
495+
match vswith
496+
|[]->(remainingvars, Some newvar)
497+
|_-> simp(newvar::remainingvars)
532498
simp vars
533499

534500
// Normalize a type ty that forms part of a unit-of-measure-polymorphic type scheme.
@@ -570,16 +536,46 @@ let rec SimplifyMeasuresInConstraints g param cs =
570536
letparam'= SimplifyMeasuresInConstraint g param c
571537
SimplifyMeasuresInConstraints g param' cs
572538

539+
let recGetMeasureVarGcdInType v ty=
540+
match stripTyparEqns tywith
541+
| TType_ucase(_,l)
542+
| TType_app(_,l)
543+
| TType_tuple l-> GetMeasureVarGcdInTypes v l
573544

545+
| TType_fun(d,r)-> GcdRational(GetMeasureVarGcdInType v d)(GetMeasureVarGcdInType v r)
546+
| TType_var_-> ZeroRational
547+
| TType_forall(_,tau)-> GetMeasureVarGcdInType v tau
548+
| TType_measure unt-> MeasureVarExponent v unt
549+
550+
andGetMeasureVarGcdInTypes v tys=
551+
match tyswith
552+
|[]-> ZeroRational
553+
| ty::tys-> GcdRational(GetMeasureVarGcdInType v ty)(GetMeasureVarGcdInTypes v tys)
574554

575-
// We normalize unit-of-measure-polymorphic type schemes as described in Kennedy's thesis. There
555+
// Normalize the exponents on generalizable variables in a type
556+
// by dividing them by their "rational gcd". For example, the type
557+
// float<'u^(2/3)> -> float<'u^(4/3)> would be normalized to produce
558+
// float<'u> -> float<'u^2> by dividing the exponents by 2/3.
559+
letNormalizeExponentsInTypeScheme uvars ty=
560+
uvars|> List.map(fun v->
561+
letexpGcd= AbsRational(GetMeasureVarGcdInType v ty)
562+
if expGcd= OneRational|| expGcd= ZeroRational
563+
then v
564+
else
565+
letv'= NewAnonTypar(TyparKind.Measure,v.Range,TyparRigidity.Flexible,v.StaticReq,v.DynamicReq)
566+
SubstMeasure v(MeasureRationalPower(MeasureVar v', DivRational OneRational expGcd))
567+
v')
568+
569+
570+
// We normalize unit-of-measure-polymorphic type schemes. There
576571
// are three reasons for doing this:
577572
// (1) to present concise and consistent type schemes to the programmer
578573
// (2) so that we can compute equivalence of type schemes in signature matching
579574
// (3) in order to produce a list of type parameters ordered as they appear in the (normalized) scheme.
580575
//
581-
// Representing the normal form as a matrix, with a row for each variable,
582-
// and a column for each unit-of-measure expression in the "skeleton" of the type. Entries are integer exponents.
576+
// Representing the normal form as a matrix, with a row for each variable or base unit,
577+
// and a column for each unit-of-measure expression in the "skeleton" of the type.
578+
// Entries for generalizable variables are integers; other rows may contain non-integer exponents.
583579
//
584580
// ( 0...0 a1 as1 b1 bs1 c1 cs1 ...)
585581
// ( 0...0 0 0...0 b2 bs2 c2 cs2 ...)
@@ -593,7 +589,10 @@ let rec SimplifyMeasuresInConstraints g param cs =
593589
//
594590
// The corner entries a1, b2, c3 are all positive. Entries lying above them (b1, c1, c2, etc) are
595591
// non-negative and smaller than the corresponding corner entry. Entries as1, bs1, bs2, etc are arbitrary.
596-
// This is known as a *reduced row echelon* matrix or Hermite matrix.
592+
//
593+
// Essentially this is the *reduced row echelon* matrix from linear algebra, with adjustment to ensure that
594+
// exponents are integers where possible (in the reduced row echelon form, a1, b2, etc. would be 1, possibly
595+
// forcing other entries to be non-integers).
597596
letSimplifyMeasuresInTypeScheme g resultFirst(generalizable:Typar list)ty constraints=
598597
// Only bother if we're generalizing over at least one unit-of-measure variable
599598
letuvars,vars=
@@ -602,9 +601,9 @@ let SimplifyMeasuresInTypeScheme g resultFirst (generalizable:Typar list) ty con
602601
match uvarswith
603602
|[]-> generalizable
604603
|_::_->
605-
let(untouched,generalized)= SimplifyMeasuresInType g resultFirst(SimplifyMeasuresInConstraints g(uvars,[]) constraints) ty
606-
607-
vars@ List.rev generalized@ untouched
604+
let(_,generalized)= SimplifyMeasuresInType g resultFirst(SimplifyMeasuresInConstraints g(uvars,[]) constraints) ty
605+
letgeneralized'= NormalizeExponentsInTypeScheme generalized ty
606+
vars@ List.rev generalized'
608607

609608
letfreshMeasure()= MeasureVar(NewInferenceMeasurePar())
610609

0 commit comments

Comments
 (0)
[8]ページ先頭
©2009-2025 Movatter.jp