@@ -422,3 +422,100 @@ module HashStamps =
422422 | TType_ var( r, Nullness.Known n) -> hashStamp r.Stamp |> pipeToHash ( hash n)
423423 | TType_ var( r, Nullness.Variable _) -> hashStamp r.Stamp
424424 | TType_ measure _ -> 0
425+
426+ /// Lossless accumulation of TType structure (parallel to HashStamps.hashTType but retaining full shape tokens)
427+ module AccumulateTypes =
428+ type NullnessToken =
429+ | Known of NullnessInfo
430+ | Variable
431+ | Absent
432+
433+ /// Convert compiler Nullness info to token form
434+ let inline toNullnessToken ( n : Nullness ) =
435+ match n with
436+ | Nullness.Known k -> NullnessToken.Known k
437+ | Nullness.Variable _ -> NullnessToken.Variable
438+
439+ /// Tokens capturing a lossless, structural representation of TType needed for deterministic keys.
440+ type TypeToken =
441+ | UCase of string * TypeToken list
442+ | App of Stamp * NullnessToken * TypeToken list
443+ | Anon of Stamp * TypeToken list
444+ | Tuple of bool * TypeToken list
445+ | Forall of Stamp list * TypeToken
446+ | Fun of TypeToken * TypeToken * NullnessToken
447+ | Var of Stamp * NullnessToken
448+ | Measure of MeasureToken
449+ and MeasureToken =
450+ | MVar of Stamp
451+ | MConst of Stamp
452+ | MProd of MeasureToken * MeasureToken
453+ | MInv of MeasureToken
454+ | MOne
455+ | MRationalPower of MeasureToken * Rational
456+
457+ /// Accumulate Measure to MeasureToken
458+ let rec private accumulateMeasure m =
459+ match m with
460+ | Measure.Var mv -> MVar mv.Stamp
461+ | Measure.Const( tcref, _) -> MConst tcref.Stamp
462+ | Measure.Prod( m1, m2, _) -> MProd( accumulateMeasure m1, accumulateMeasure m2)
463+ | Measure.Inv m1 -> MInv ( accumulateMeasure m1)
464+ | Measure.One _ -> MOne
465+ | Measure.RationalPower( m1, r) -> MRationalPower( accumulateMeasure m1, r)
466+
467+ /// Accumulate a TType into a lossless token tree. Uses stamps for identity where appropriate (matching hashTType logic).
468+ let rec accumulateTType ( ty : TType ) : TypeToken =
469+ match ty with
470+ | TType_ ucase( u, tinst) ->
471+ let args = tinst |> List.map accumulateTType
472+ UCase( u.CaseName, args)
473+ | TType_ app( tcref, tinst, n) ->
474+ let args = tinst |> List.map accumulateTType
475+ App( tcref.Stamp, toNullnessToken n, args)
476+ | TType_ anon( info, tys) ->
477+ let args = tys |> List.map accumulateTType
478+ Anon( info.Stamp, args)
479+ | TType_ tuple( tupInfo, tys) ->
480+ let elems = tys |> List.map accumulateTType
481+ let isStruct = evalTupInfoIsStruct tupInfo
482+ Tuple( isStruct, elems)
483+ | TType_ forall( tps, tau) ->
484+ let stamps = tps |> List.map ( fun tp -> tp.Stamp)
485+ let body = accumulateTType tau
486+ Forall( stamps, body)
487+ | TType_ fun( d, r, n) ->
488+ Fun( accumulateTType d, accumulateTType r, toNullnessToken n)
489+ | TType_ var( r, n) ->
490+ Var( r.Stamp, toNullnessToken n)
491+ | TType_ measure m -> Measure ( accumulateMeasure m)
492+
493+ // /// Flatten accumulated token tree to a sequence of simple discriminators and payload (useful for generic hashing/serialization)
494+ //let flatten (root: TypeToken) : obj list =
495+ // let res = System.Collections.Generic.List<obj>()
496+ // let rec loop tt =
497+ // match tt with
498+ // | UCase(name, args) ->
499+ // res.Add "UCASE"; res.Add name; res.Add args.Length; args |> List.iter loop
500+ // | App(stamp, nTok, args) ->
501+ // res.Add "APP"; res.Add stamp; res.Add (match nTok with | Known k -> box k | Variable -> box "VAR" | Absent -> box null);
502+ // res.Add args.Length; args |> List.iter loop
503+ // | Anon(stamp, args) -> res.Add "ANON"; res.Add stamp; res.Add args.Length; args |> List.iter loop
504+ // | Tuple(isStruct, elems) -> res.Add "TUP"; res.Add isStruct; res.Add elems.Length; elems |> List.iter loop
505+ // | Forall(stamps, body) -> res.Add "FORALL"; res.Add stamps.Length; stamps |> List.iter (fun s -> res.Add s); loop body
506+ // | Fun(d, r, nTok) ->
507+ // res.Add "FUN"; res.Add (match nTok with | Known k -> box k | Variable -> box "VAR" | Absent -> box null); loop d; loop r
508+ // | Var(stamp, nTok) -> res.Add "VAR"; res.Add stamp; res.Add (match nTok with | Known k -> box k | Variable -> box "VAR" | Absent -> box null)
509+ // | Measure m ->
510+ // res.Add "MEASURE"
511+ // let rec loopM mt =
512+ // match mt with
513+ // | MVar s -> res.Add "MVAR"; res.Add s
514+ // | MConst s -> res.Add "MCONST"; res.Add s
515+ // | MProd(a, b) -> res.Add "MPROD"; loopM a; loopM b
516+ // | MInv x -> res.Add "MINV"; loopM x
517+ // | MOne -> res.Add "MONE"
518+ // | MRationalPower(x, r) -> res.Add "MRAT"; res.Add (box r); loopM x
519+ // loopM m
520+ // loop root
521+ // res |> Seq.toList
0 commit comments