Skip to content

Commit

Permalink
Support for rational exponents in units of measure
Browse files Browse the repository at this point in the history 
commit fd77e404911ea3948d8d6b59c9a53522eba2cef4
Author: latkin <[email protected]>
Date:   Wed Jan 7 17:15:14 2015 -0800

    Further overflow/parsing fixes: check denominators, convert to bigint before negation

commit 09e892b3eda586775767cef1866c994ace07d217
Author: andrewjkennedy <[email protected]>
Date:   Wed Jan 7 11:40:53 2015 +0000

    Make parsing of -2147483648 in rational exponents an error

commit 050b8b67c30c6857353d70449955c9872939b42a
Author: latkin <[email protected]>
Date:   Tue Jan 6 14:48:11 2015 -0800

    Remove unused error message

commit 75b99d8561ff9aee087dc856cde106d6b4053622
Author: latkin <[email protected]>
Date:   Tue Jan 6 14:35:07 2015 -0800

    Deleting obsolete tests

commit ac97bcb9eb1079381c50071b5e3d95e21f21a12c
Merge: f11c636 1877dff
Author: latkin <[email protected]>
Date:   Mon Jan 5 15:58:51 2015 -0800

    Merge branch 'unitsexprat' of https://git01.codeplex.com/forks/andrewjkennedy/fsharpcontrib into rationalexp

    Conflicts:
    	src/fsharp/FSComp.txt

commit 1877dff5235e538b6b406a17478ce9b81bad735b
Author: andrewjkennedy <[email protected]>
Date:   Tue Dec 30 12:08:50 2014 +0000

    Tests

commit f7255be543782ae2aa5ed570c731eeb74d2205a1
Author: andrewjkennedy <[email protected]>
Date:   Mon Dec 29 15:37:59 2014 +0000

    Added ref to System.Numerics

commit 47180d60e4607233efe8a52be3f241c478793684
Author: andrewjkennedy <[email protected]>
Date:   Mon Dec 29 15:18:48 2014 +0000

    Parsing of rational exponents is broken

commit b5ce68705045ed9944183f8238c478f7db575aa5
Author: andrewjkennedy <[email protected]>
Date:   Mon Dec 29 13:47:26 2014 +0000

    Revert "Overflow exception catching"

    This reverts commit 9259f5374d0d4f20f0fb5fb4ef43e0eba71027ae.

commit 11e1ed21ccf05a0552c97d635c3b91e6e6397691
Author: andrewjkennedy <[email protected]>
Date:   Mon Dec 29 13:30:21 2014 +0000

    Use BigIntegers for rationals

commit 9259f5374d0d4f20f0fb5fb4ef43e0eba71027ae
Author: andrewjkennedy <[email protected]>
Date:   Mon Dec 29 13:29:23 2014 +0000

    Overflow exception catching

commit 3b835e9b20e580b01bac7e81ea53cfaa36ac06c5
Author: andrewjkennedy <[email protected]>
Date:   Mon Nov 3 17:38:57 2014 +0000

    Error message for non-parenthesized units

commit 3160dbbac9e9e2799eb3fe13239525fa8ce8c568
Author: andrewjkennedy <[email protected]>
Date:   Mon Nov 3 16:18:31 2014 +0000

    Improved error when parentheses are omitted from exponent

commit f24e688d7794263f7dabb40f4ac9a498e82d517d
Author: andrewjkennedy <[email protected]>
Date:   Mon Nov 3 13:24:59 2014 +0000

    Negative test for rational exponent parsing

commit 1e55326403626df25776226501bc8fedfc089adb
Author: andrewjkennedy <[email protected]>
Date:   Mon Nov 3 11:21:05 2014 +0000

    Zero denominator test

commit f50f36f8603420298316ce966eb2e156e4052839
Author: andrewjkennedy <[email protected]>
Date:   Mon Nov 3 11:07:47 2014 +0000

    Small improvements as suggested by Don

commit 71fe676f97bf06dbf165defb0b1e10a250266126
Author: andrewjkennedy <[email protected]>
Date:   Mon Nov 3 11:07:02 2014 +0000

    Some positive tests for rational exponents

commit 0ac8fdc68ba807920c22b212be549751aa141548
Author: andrewjkennedy <[email protected]>
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 2a227d0f4463d117f3022b34a18733e3b98d8594
Author: andrewjkennedy <[email protected]>
Date:   Thu Oct 30 10:58:49 2014 +0000

    Check for 0 denominator

commit 67acf8465ea5bfcb8766f7045ba5b47bf1a51fc5
Author: andrewjkennedy <[email protected]>
Date:   Thu Oct 30 10:41:05 2014 +0000

    Couple of non-integer exponent tests

commit 89881e2a94cf0e220051d68393d5e184ddc4634e
Author: andrewjkennedy <[email protected]>
Date:   Thu Oct 30 10:16:18 2014 +0000

    u_rational should be outside #ifdef

commit 8461d5ee8632e15555680bc41cfea241f5ad7e5d
Author: andrewjkennedy <[email protected]>
Date:   Wed Oct 29 11:05:14 2014 +0000

    Updated comments

commit c9da07d8f06311e2e62958e675f8082329651bf1
Author: andrewjkennedy <[email protected]>
Date:   Wed Oct 29 10:40:09 2014 +0000

    Parentheses
    Revert LessGeneric test

commit b6090279f81f6583d5a2bec18eeaebb308506148
Author: andrewjkennedy <[email protected]>
Date:   Tue Oct 28 15:42:18 2014 +0000

    Negative test baseline - can now take sqrt of m!

commit a69bfc41a0184784bee44c7a08f3206525b1ce81
Author: andrewjkennedy <[email protected]>
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 4a6143daaf38909d5b75e34d5fd4b036f4b862cc
Author: andrewjkennedy <[email protected]>
Date:   Tue Oct 28 11:21:17 2014 +0000

    More efficient representation of measures.
    Separate rational implementation.
    Better simplified form.

commit 323d627288948359795797060216d8fe7d4676cf
Author: andrewjkennedy <[email protected]>
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 547444819d02f7df2f49b69c5ef32b039d58859b
Author: andrewjkennedy <[email protected]>
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 82b5fe40c907aae75036982dc7a4b168410e66e1
Author: andrewjkennedy <[email protected]>
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-integers

commit d558956a1476d79b6aaa52e6ccf6d1f2f5372dac
Author: andrewjkennedy <[email protected]>
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
  • Loading branch information
@latkin
andrewjkennedy authored and latkin committed Jan 6, 2015
1 parent 30ed635 commit af6fe4e
Show file tree
Hide file tree
Showing 26 changed files with 397 additions and 181 deletions.
1 change: 1 addition & 0 deletions src/fsharp/FSComp.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -475,6 +475,7 @@ parsMultiArgumentGenericTypeFormDeprecated,"The syntax '(typ,...,typ) ident' is
622,parsMismatchedQuotationName,"Mismatched quotation operator name, beginning with '%s'"
623,parsActivePatternCaseMustBeginWithUpperCase,"Active pattern case identifiers must begin with an uppercase letter"
624,parsActivePatternCaseContainsPipe,"The '|' character is not permitted in active pattern case identifiers"
625,parsIllegalDenominatorForMeasureExponent,"Denominator must not be 0 in unit-of-measure exponent"
parsNoEqualShouldFollowNamespace,"No '=' symbol should follow a 'namespace' declaration"
parsSyntaxModuleStructEndDeprecated,"The syntax 'module ... = struct .. end' is not used in F# code. Consider using 'module ... = begin .. end'"
parsSyntaxModuleSigEndDeprecated,"The syntax 'module ... : sig .. end' is not used in F# code. Consider using 'module ... = begin .. end'"
Expand Down
6 changes: 6 additions & 0 deletions src/fsharp/FSharp.Compiler-proto/FSharp.Compiler-proto.fsproj
View file
Original file line number Diff line number Diff line change
Expand Up @@ -179,6 +179,12 @@
<Compile Include="..\range.fs">
<Link>range.fs</Link>
</Compile>
<Compile Include="..\rational.fsi">
<Link>rational.fsi</Link>
</Compile>
<Compile Include="..\rational.fs">
<Link>rational.fs</Link>
</Compile>
<Compile Include="..\ErrorLogger.fs">
<Link>ErrorLogger.fs</Link>
</Compile>
Expand Down
7 changes: 7 additions & 0 deletions src/fsharp/FSharp.Compiler/FSharp.Compiler.fsproj
View file
Original file line number Diff line number Diff line change
Expand Up @@ -135,6 +135,12 @@
<Compile Include="..\TraceCall.fs">
<Link>Utilities\TraceCall.fs</Link>
</Compile>
<Compile Include="..\rational.fsi">
<Link>ErrorLogging\rational.fsi</Link>
</Compile>
<Compile Include="..\rational.fs">
<Link>ErrorLogging\rational.fs</Link>
</Compile>
<Compile Include="..\range.fsi">
<Link>ErrorLogging\range.fsi</Link>
</Compile>
Expand Down Expand Up @@ -501,6 +507,7 @@
<Reference Include="mscorlib" />
<Reference Include="System" />
<Reference Include="System.Core" />
<Reference Include="System.Numerics" />
<Reference Include="System.Drawing" />
<Reference Include="System.Windows.Forms" />
<Reference Include="System.Runtime.Remoting" />
Expand Down
7 changes: 7 additions & 0 deletions src/fsharp/FSharp.LanguageService.Compiler/FSharp.LanguageService.Compiler.fsproj
View file
Original file line number Diff line number Diff line change
Expand Up @@ -197,6 +197,12 @@
<Compile Include="..\range.fs">
<Link>range.fs</Link>
</Compile>
<Compile Include="..\rational.fsi">
<Link>rational.fsi</Link>
</Compile>
<Compile Include="..\rational.fs">
<Link>rational.fs</Link>
</Compile>
<Compile Include="..\ErrorLogger.fs">
<Link>ErrorLogger.fs</Link>
</Compile>
Expand Down Expand Up @@ -450,6 +456,7 @@
<Reference Include="mscorlib" />
<Reference Include="System" />
<Reference Include="System.Core" />
<Reference Include="System.Numerics" />
<Reference Include="System.Drawing" />
<Reference Include="System.Windows.Forms" />
<Reference Include="System.Runtime.Remoting" />
Expand Down
15 changes: 9 additions & 6 deletions src/fsharp/NicePrint.fs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ open Microsoft.FSharp.Compiler.AbstractIL.Internal.Library
open Microsoft.FSharp.Compiler
open Microsoft.FSharp.Compiler.AbstractIL.Diagnostics
open Microsoft.FSharp.Compiler.Range
open Microsoft.FSharp.Compiler.Rational
open Microsoft.FSharp.Compiler.Ast
open Microsoft.FSharp.Compiler.ErrorLogger
open Microsoft.FSharp.Compiler.Tast
Expand Down Expand Up @@ -814,14 +815,16 @@ module private PrintTypes =
and private layoutMeasure denv unt =
let sortVars vs = vs |> List.sortBy (fun (v:Typar,_) -> v.DisplayName)
let sortCons cs = cs |> List.sortBy (fun (c:TyconRef,_) -> c.DisplayName)
let negvs,posvs = ListMeasureVarOccsWithNonZeroExponents unt |> sortVars |> List.partition (fun (_,e) -> e<0)
let negcs,poscs = ListMeasureConOccsWithNonZeroExponents denv.g false unt |> sortCons |> List.partition (fun (_,e) -> e<0)
let negvs,posvs = ListMeasureVarOccsWithNonZeroExponents unt |> sortVars |> List.partition (fun (_,e) -> SignRational e < 0)
let negcs,poscs = ListMeasureConOccsWithNonZeroExponents denv.g false unt |> sortCons |> List.partition (fun (_,e) -> SignRational e < 0)
let unparL uv = layoutTyparRef denv uv
let unconL tc = layoutTyconRef denv tc
let prefix = spaceListL (List.map (fun (v,e) -> if e=1 then unparL v else unparL v -- wordL (sprintf "^ %d" e)) posvs @
List.map (fun (c,e) -> if e=1 then unconL c else unconL c -- wordL (sprintf "^ %d" e)) poscs)
let postfix = spaceListL (List.map (fun (v,e) -> if e= -1 then unparL v else unparL v -- wordL (sprintf "^ %d" (-e))) negvs @
List.map (fun (c,e) -> if e= -1 then unconL c else unconL c -- wordL (sprintf "^ %d" (-e))) negcs)
let rationalL e = wordL (RationalToString e)
let measureToPowerL x e = if e = OneRational then x else x -- wordL "^" -- rationalL e
let prefix = spaceListL (List.map (fun (v,e) -> measureToPowerL (unparL v) e) posvs @
List.map (fun (c,e) -> measureToPowerL (unconL c) e) poscs)
let postfix = spaceListL (List.map (fun (v,e) -> measureToPowerL (unparL v) (NegRational e)) negvs @
List.map (fun (c,e) -> measureToPowerL (unconL c) (NegRational e)) negcs)
match (negvs,negcs) with
| [],[] -> (match posvs,poscs with [],[] -> wordL "1" | _ -> prefix)
| _ -> prefix ^^ sepL "/" ^^ (if List.length negvs + List.length negcs > 1 then sepL "(" ^^ postfix ^^ sepL ")" else postfix)
Expand Down
15 changes: 12 additions & 3 deletions src/fsharp/ast.fs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -255,11 +255,20 @@ and
| Product of SynMeasure * SynMeasure * range
| Seq of SynMeasure list * range
| Divide of SynMeasure * SynMeasure * range
| Power of SynMeasure * int * range
| Power of SynMeasure * SynRationalConst * range
| One
| Anon of range
| Var of SynTypar * range

and
[<NoEquality; NoComparison; RequireQualifiedAccess>]
/// The unchecked abstract syntax tree of F# unit of measure exponents.
SynRationalConst =
| Integer of int32
| Rational of int32 * int32 * range
| Negate of SynRationalConst


//------------------------------------------------------------------------
// AST: the grammar of types, expressions, declarations etc.
//-----------------------------------------------------------------------
Expand Down Expand Up @@ -423,8 +432,8 @@ and
| HashConstraint of SynType * range
/// F# syntax : for units of measure e.g. m / s
| MeasureDivide of SynType * SynType * range
/// F# syntax : for units of measure e.g. m^3
| MeasurePower of SynType * int * range
/// F# syntax : for units of measure e.g. m^3, kg^1/2
| MeasurePower of SynType * SynRationalConst * range
/// F# syntax : 1, "abc" etc, used in parameters to type providers
/// For the dimensionless units i.e. 1 , and static parameters to provided types
| StaticConstant of SynConst * range
Expand Down
161 changes: 80 additions & 81 deletions src/fsharp/csolve.fs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,7 @@ open Microsoft.FSharp.Compiler

open Microsoft.FSharp.Compiler.AbstractIL.Diagnostics
open Microsoft.FSharp.Compiler.Range
open Microsoft.FSharp.Compiler.Rational
open Microsoft.FSharp.Compiler.Ast
open Microsoft.FSharp.Compiler.ErrorLogger
open Microsoft.FSharp.Compiler.Tast
Expand Down Expand Up @@ -358,20 +359,20 @@ let PreferUnifyTypar (v1:Typar) (v2:Typar) =



/// Ensure that vs is ordered so that an element with minimum sized exponent
/// is at the head of the list. Also, if possible, this element should have rigidity TyparRigidity.Flexible
let FindMinimumMeasureExponent vs =
let rec findmin vs =
/// Reorder a list of (variable,exponent) pairs so that a variable that is Preferred
/// is at the head of the list, if possible
let FindPreferredTypar vs =
let rec find vs =
match vs with
| [] -> vs
| (v:Typar,e)::vs ->
match findmin vs with
match find vs with
| [] -> [(v,e)]
| (v',e')::vs' ->
if abs e < abs e' || (abs e = abs e' && PreferUnifyTypar v v')
| (v',e')::vs' ->
if PreferUnifyTypar v v'
then (v, e) :: vs
else (v',e') :: (v,e) :: vs'
findmin vs
find vs

let SubstMeasure (r:Typar) ms =
if r.Rigidity = TyparRigidity.Rigid then error(InternalError("SubstMeasure: rigid",r.Range));
Expand Down Expand Up @@ -447,88 +448,53 @@ let SubstMeasureWarnIfRigid (csenv:ConstraintSolverEnv) trace (v:Typar) ms =
WarnD(Error(FSComp.SR.csCodeLessGeneric(),v.Range))
else CompleteD)

/// The division operator in Caml/F# rounds towards zero. For our purposes,
/// we want to round towards negative infinity.
let DivRoundDown x y =
let signx=if x<0 then -1 else 1
let signy=if y<0 then -1 else 1

if signx=signy then x / y
else (x-y+signy) / y

/// Imperatively unify the unit-of-measure expression ms against 1.
/// This is a gcd-like algorithm that proceeds as follows:
/// 1. Express ms in the form 'u1^x1 * ... * 'un^xn * c1^y1 * ... * cm^ym
/// where 'u1,...,'un are non-rigid measure variables, c1,...,cm are measure identifiers or rigid measure variables,
/// x1,...,xn and y1,...,yn are non-zero exponents with |x1| <= |xi| for all i.
/// 2. (a) If m=n=0 then we're done (we're unifying 1 against 1)
/// (b) If m=0 but n<>0 then fail (we're unifying a variable-free expression against 1)
/// (c) If xi is divisible by |x1| for all i, and yj is divisible by |x1| for all j, then
/// immediately solve the constraint with the substitution
/// 'u1 := 'u2^(-x2/x1) * ... * 'un^(-xn/x1) * c1^(-y1/x1) * ... * cm^(-ym/x1)
/// (d) Otherwise, if m=1, fail (example: unifying 'u^2 * kg^3)
/// (e) Otherwise, make the substitution
/// 'u1 := 'u * 'u2^(-x2/x1) * ... * 'un^(-xn/x1) * c1^(-y1/x1) * ... * cm^(-ym/x1)
/// where 'u is a fresh measure variable, and iterate.
let rec UnifyMeasureWithOne (csenv:ConstraintSolverEnv) trace ms =
/// There are three cases
/// - ms is (equivalent to) 1
/// - ms contains no non-rigid unit variables, and so cannot be unified with 1
/// - ms has the form v^e * ms' for some non-rigid variable v, non-zero exponent e, and measure expression ms'
/// the most general unifier is then simply v := ms' ^ -(1/e)
let UnifyMeasureWithOne (csenv:ConstraintSolverEnv) trace ms =
// Gather the rigid and non-rigid unit variables in this measure expression together with their exponents
let (rigidVars,nonRigidVars) = (ListMeasureVarOccsWithNonZeroExponents ms) |> List.partition (fun (v,_) -> v.Rigidity = TyparRigidity.Rigid)
let expandedCons = ListMeasureConOccsWithNonZeroExponents csenv.g true ms
let unexpandedCons = ListMeasureConOccsWithNonZeroExponents csenv.g false ms
match FindMinimumMeasureExponent nonRigidVars, rigidVars, expandedCons, unexpandedCons with
| [], [], [], _ -> CompleteD
| [], _, _, _ -> localAbortD
| (v,e)::vs, rigidVars, _, _ ->
// don't break up abbreviations if we can help it!
if unexpandedCons |> List.forall (fun (_,e') -> e' % e = 0) && (vs@rigidVars) |> List.forall (fun (_,e') -> e' % e = 0)
then
let newms = ProdMeasures (List.map (fun (c,e') -> MeasurePower (MeasureCon c) (- (DivRoundDown e' e))) unexpandedCons
@ List.map (fun (v,e') -> MeasurePower (MeasureVar v) (- (DivRoundDown e' e))) (vs @ rigidVars))
SubstMeasureWarnIfRigid csenv trace v newms
else
let newms = ProdMeasures (List.map (fun (c,e') -> MeasurePower (MeasureCon c) (- (DivRoundDown e' e))) expandedCons
@ List.map (fun (v,e') -> MeasurePower (MeasureVar v) (- (DivRoundDown e' e))) (vs @ rigidVars))
if expandedCons |> List.forall (fun (_,e') -> e' % e = 0) && (vs@rigidVars) |> List.forall (fun (_,e') -> e' % e = 0)
then SubstMeasureWarnIfRigid csenv trace v newms
elif isNil vs
then localAbortD
else
// New variable v' must inherit WarnIfNotRigid from v
let v' = NewAnonTypar (TyparKind.Measure,v.Range,v.Rigidity,v.StaticReq,v.DynamicReq)
SubstMeasure v (MeasureProd(MeasureVar v', newms));
UnifyMeasureWithOne csenv trace ms

// If there is at least one non-rigid variable v with exponent e, then we can unify
match FindPreferredTypar nonRigidVars with
| (v,e)::vs ->
let unexpandedCons = ListMeasureConOccsWithNonZeroExponents csenv.g false ms
let newms = ProdMeasures (List.map (fun (c,e') -> MeasureRationalPower (MeasureCon c, NegRational (DivRational e' e))) unexpandedCons
@ List.map (fun (v,e') -> MeasureRationalPower (MeasureVar v, NegRational (DivRational e' e))) (vs @ rigidVars))

SubstMeasureWarnIfRigid csenv trace v newms

// Otherwise we require ms to be 1
| [] ->
if measureEquiv csenv.g ms MeasureOne then CompleteD else localAbortD

/// Imperatively unify unit-of-measure expression ms1 against ms2
let UnifyMeasures (csenv:ConstraintSolverEnv) trace ms1 ms2 =
UnifyMeasureWithOne csenv trace (MeasureProd(ms1,MeasureInv ms2))


/// Simplify a unit-of-measure expression ms that forms part of a type scheme.
/// We make substitutions for vars, which are the (remaining) bound variables
/// in the scheme that we wish to simplify.
let SimplifyMeasure g vars ms =
let rec simp vars =
match FindMinimumMeasureExponent (List.filter (fun (_,e) -> e<>0) (List.map (fun v -> (v, MeasureVarExponent v ms)) vars)) with
match FindPreferredTypar (List.filter (fun (_,e) -> SignRational e<>0) (List.map (fun v -> (v, MeasureVarExponent v ms)) vars)) with
| [] ->
(vars, None)

| (v,e)::vs ->
if e < 0 then
let v' = NewAnonTypar (TyparKind.Measure,v.Range,TyparRigidity.Flexible,v.StaticReq,v.DynamicReq)
let vars' = v' :: ListSet.remove typarEq v vars
SubstMeasure v (MeasureInv (MeasureVar v'));
simp vars'
else
let newv = if v.IsCompilerGenerated then NewAnonTypar (TyparKind.Measure,v.Range,TyparRigidity.Flexible,v.StaticReq,v.DynamicReq)
else NewNamedInferenceMeasureVar (v.Range,TyparRigidity.Flexible,v.StaticReq,v.Id)
let remainingvars = ListSet.remove typarEq v vars
let newms = (ProdMeasures (List.map (fun (c,e') -> MeasurePower (MeasureCon c) (- (DivRoundDown e' e))) (ListMeasureConOccsWithNonZeroExponents g false ms)
@ List.map (fun (v',e') -> if typarEq v v' then MeasureVar newv else MeasurePower (MeasureVar v') (- (DivRoundDown e' e))) (ListMeasureVarOccsWithNonZeroExponents ms)));
SubstMeasure v newms;
match vs with
| [] -> (remainingvars, Some newv)
| _ -> simp (newv::remainingvars)

let newvar = if v.IsCompilerGenerated then NewAnonTypar (TyparKind.Measure,v.Range,TyparRigidity.Flexible,v.StaticReq,v.DynamicReq)
else NewNamedInferenceMeasureVar (v.Range,TyparRigidity.Flexible,v.StaticReq,v.Id)
let remainingvars = ListSet.remove typarEq v vars
let newvarExpr = if SignRational e < 0 then MeasureInv (MeasureVar newvar) else MeasureVar newvar
let newms = (ProdMeasures (List.map (fun (c,e') -> MeasureRationalPower (MeasureCon c, NegRational (DivRational e' e))) (ListMeasureConOccsWithNonZeroExponents g false ms)
@ List.map (fun (v',e') -> if typarEq v v' then newvarExpr else MeasureRationalPower (MeasureVar v', NegRational (DivRational e' e))) (ListMeasureVarOccsWithNonZeroExponents ms)));
SubstMeasure v newms;
match vs with
| [] -> (remainingvars, Some newvar)
| _ -> simp (newvar::remainingvars)
simp vars

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

let rec GetMeasureVarGcdInType v ty =
match stripTyparEqns ty with
| TType_ucase(_,l)
| TType_app (_,l)
| TType_tuple l -> GetMeasureVarGcdInTypes v l

| TType_fun (d,r) -> GcdRational (GetMeasureVarGcdInType v d) (GetMeasureVarGcdInType v r)
| TType_var _ -> ZeroRational
| TType_forall (_,tau) -> GetMeasureVarGcdInType v tau
| TType_measure unt -> MeasureVarExponent v unt

and GetMeasureVarGcdInTypes v tys =
match tys with
| [] -> ZeroRational
| ty::tys -> GcdRational (GetMeasureVarGcdInType v ty) (GetMeasureVarGcdInTypes v tys)

// We normalize unit-of-measure-polymorphic type schemes as described in Kennedy's thesis. There
// Normalize the exponents on generalizable variables in a type
// by dividing them by their "rational gcd". For example, the type
// float<'u^(2/3)> -> float<'u^(4/3)> would be normalized to produce
// float<'u> -> float<'u^2> by dividing the exponents by 2/3.
let NormalizeExponentsInTypeScheme uvars ty =
uvars |> List.map (fun v ->
let expGcd = AbsRational (GetMeasureVarGcdInType v ty)
if expGcd = OneRational || expGcd = ZeroRational
then v
else
let v' = NewAnonTypar (TyparKind.Measure,v.Range,TyparRigidity.Flexible,v.StaticReq,v.DynamicReq)
SubstMeasure v (MeasureRationalPower (MeasureVar v', DivRational OneRational expGcd))
v')


// We normalize unit-of-measure-polymorphic type schemes. There
// are three reasons for doing this:
// (1) to present concise and consistent type schemes to the programmer
// (2) so that we can compute equivalence of type schemes in signature matching
// (3) in order to produce a list of type parameters ordered as they appear in the (normalized) scheme.
//
// Representing the normal form as a matrix, with a row for each variable,
// and a column for each unit-of-measure expression in the "skeleton" of the type. Entries are integer exponents.
// Representing the normal form as a matrix, with a row for each variable or base unit,
// and a column for each unit-of-measure expression in the "skeleton" of the type.
// Entries for generalizable variables are integers; other rows may contain non-integer exponents.
//
// ( 0...0 a1 as1 b1 bs1 c1 cs1 ...)
// ( 0...0 0 0...0 b2 bs2 c2 cs2 ...)
Expand All @@ -593,7 +589,10 @@ let rec SimplifyMeasuresInConstraints g param cs =
//
// The corner entries a1, b2, c3 are all positive. Entries lying above them (b1, c1, c2, etc) are
// non-negative and smaller than the corresponding corner entry. Entries as1, bs1, bs2, etc are arbitrary.
// This is known as a *reduced row echelon* matrix or Hermite matrix.
//
// Essentially this is the *reduced row echelon* matrix from linear algebra, with adjustment to ensure that
// exponents are integers where possible (in the reduced row echelon form, a1, b2, etc. would be 1, possibly
// forcing other entries to be non-integers).
let SimplifyMeasuresInTypeScheme g resultFirst (generalizable:Typar list) ty constraints =
// Only bother if we're generalizing over at least one unit-of-measure variable
let uvars, vars =
Expand All @@ -602,9 +601,9 @@ let SimplifyMeasuresInTypeScheme g resultFirst (generalizable:Typar list) ty con
match uvars with
| [] -> generalizable
| _::_ ->
let (untouched, generalized) = SimplifyMeasuresInType g resultFirst (SimplifyMeasuresInConstraints g (uvars, []) constraints) ty

vars @ List.rev generalized @ untouched
let (_, generalized) = SimplifyMeasuresInType g resultFirst (SimplifyMeasuresInConstraints g (uvars, []) constraints) ty
let generalized' = NormalizeExponentsInTypeScheme generalized ty
vars @ List.rev generalized'

let freshMeasure () = MeasureVar (NewInferenceMeasurePar ())

Expand Down
Loading

0 comments on commit af6fe4e

Please sign in to comment.