| | | 1 | | using NanoCLang.Environemnts; |
| | | 2 | | using System; |
| | | 3 | | using System.Collections.Generic; |
| | | 4 | | |
| | | 5 | | namespace NanoCLang.Entities { |
| | | 6 | | /// <summary> |
| | | 7 | | /// Provides a class for refined types. |
| | | 8 | | /// </summary> |
| | | 9 | | public class RefinedType : Type, IEquatable<RefinedType?> { |
| | | 10 | | /// <summary> |
| | | 11 | | /// Gets the default value that the refinement parameter uses. |
| | | 12 | | /// </summary> |
| | | 13 | | private const string DEFAULT_NAME = "v"; |
| | | 14 | | /// <summary> |
| | | 15 | | /// Creates a new instance of a refined type that refines the <paramref name="baseType"/> with the <paramref nam |
| | | 16 | | /// </summary> |
| | | 17 | | /// <param name="name">Name of the free variable that is used in the refinement.</param> |
| | | 18 | | /// <param name="baseType">Base type that is refined.</param> |
| | | 19 | | /// <param name="refinement">Refinement expression.</param> |
| | 2746 | 20 | | public RefinedType(string name, BasicType baseType, PureExpression refinement) { |
| | 1373 | 21 | | RefinementParameter = name; |
| | 1373 | 22 | | BaseType = baseType; |
| | 1373 | 23 | | Refinement = refinement; |
| | 1373 | 24 | | } |
| | | 25 | | /// <summary> |
| | | 26 | | /// Creates a new refined type from the <paramref name="refinement"/> function that gives the refinement with re |
| | | 27 | | /// </summary> |
| | | 28 | | /// <param name="baseType">Base type that is refined.</param> |
| | | 29 | | /// <param name="refinement">Refinement function.</param> |
| | | 30 | | /// <param name="refineVar">Name of the free variable that is used in the refinement.</param> |
| | | 31 | | public RefinedType(BasicType baseType, Func<VariableExpression, PureExpression> refinement, string refineVar = D |
| | 1413 | 32 | | : this(refineVar, baseType, refinement(new VariableExpression(refineVar))) { } |
| | | 33 | | /// <summary> |
| | | 34 | | /// Creates a new refined type, that further refines the initial <paramref name="type"/>, from the <paramref nam |
| | | 35 | | /// </summary> |
| | | 36 | | /// <param name="type">Refined type that is further refined.</param> |
| | | 37 | | /// <param name="refinement">Refinement function.</param> |
| | | 38 | | /// <param name="refineVar">Name of the free variable that is used in the refinement.</param> |
| | | 39 | | public RefinedType(Type type, Func<VariableExpression, PureExpression> refinement, string refineVar = DEFAULT_NA |
| | 624 | 40 | | : this(refineVar, type.BaseType, type is RefinedType |
| | 624 | 41 | | ? refinement(new VariableExpression(refineVar)) & type.Refinement |
| | 1872 | 42 | | : refinement(new VariableExpression(refineVar))) { } |
| | | 43 | | /// <summary> |
| | | 44 | | /// Name of the free variable that is used in the refinement. |
| | | 45 | | /// </summary> |
| | 1279 | 46 | | public string RefinementParameter { get; } // Constant v |
| | | 47 | | /// <summary> |
| | | 48 | | /// Base type that is refined. |
| | | 49 | | /// </summary> |
| | 3038 | 50 | | public override BasicType BaseType { get; } |
| | | 51 | | /// <summary> |
| | | 52 | | /// Refinement expression of the <see cref="RefinementParameter"/>. |
| | | 53 | | /// </summary> |
| | 2134 | 54 | | public override PureExpression Refinement { get; } |
| | | 55 | | /// <inheritdoc/> |
| | 135 | 56 | | public override int Size => BaseType.Size; |
| | | 57 | | /// <inheritdoc/> |
| | 119 | 58 | | public override void WellFormed(LocalEnvironment gamma, Heap heap) { |
| | 119 | 59 | | VerbConsole.WriteLine(VerbosityLevel.Default, $"WF-Type: {this}"); |
| | 119 | 60 | | BaseType.WellFormed(gamma, heap); |
| | 238 | 61 | | gamma.With(RefinementParameter, BaseType, gamma => Refinement.WellFormed(gamma)); |
| | 119 | 62 | | } |
| | | 63 | | /// <inheritdoc/> |
| | 265 | 64 | | public override IEnumerable<StringFormatterToken> Tokens(NanoCSourceFormat args) { |
| | 265 | 65 | | yield return "{"; |
| | 265 | 66 | | yield return RefinementParameter; |
| | 530 | 67 | | if (args.SpaceBeforeTypeOperator) yield return " "; |
| | 265 | 68 | | yield return ":"; |
| | 530 | 69 | | if (args.SpaceAfterTypeOperator) yield return " "; |
| | 4239 | 70 | | foreach (var tk in BaseType.Tokens(args)) yield return tk; |
| | 530 | 71 | | if (args.SpaceBeforeRefineOperator) yield return " "; |
| | 265 | 72 | | yield return "|"; |
| | 530 | 73 | | if (args.SpaceAfterRefineOperator) yield return " "; |
| | 10695 | 74 | | foreach (var tk in Refinement.Tokens(args)) yield return tk; |
| | 265 | 75 | | yield return "}"; |
| | 265 | 76 | | } |
| | | 77 | | /// <inheritdoc/> |
| | 149 | 78 | | public override bool ProperSubType(LocalEnvironment gamma, Type other) => BaseType.SubType(gamma, other.BaseType |
| | 148 | 79 | | private bool CheckRefinement(LocalEnvironment gamma, Type other) { |
| | 148 | 80 | | return other switch { |
| | 29 | 81 | | BasicType _ => true, |
| | 119 | 82 | | RefinedType refined => CheckRefinement(gamma, refined), |
| | 0 | 83 | | _ => throw new InvalidProgramException("Expected basic type or refined type here!") |
| | 148 | 84 | | }; |
| | 148 | 85 | | } |
| | 119 | 86 | | private bool CheckRefinement(LocalEnvironment gamma, RefinedType refined) => Refinement == refined.Refinement || |
| | 236 | 87 | | gamma => NanoCSMT.Default.ValidImplication(gamma, Refinement, refined.Refinement)); |
| | | 88 | | /// <inheritdoc/> |
| | | 89 | | public override Type Replace(Substitutor sub) |
| | 147 | 90 | | => new RefinedType(RefinementParameter, (BasicType)BaseType.Replace(sub), Refinement.Replace(sub)); |
| | | 91 | | /// <inheritdoc/> |
| | 85 | 92 | | public override IEnumerable<StringFormatterToken> Tokens(CSourceFormat args) => BaseType.Tokens(args); |
| | | 93 | | #region Equality checks |
| | | 94 | | /// <inheritdoc/> |
| | 237 | 95 | | public override bool Equals(object? obj) => Equals(obj as RefinedType); |
| | | 96 | | /// <inheritdoc/> |
| | 237 | 97 | | public bool Equals(RefinedType? other) => !(other is null) && RefinementParameter == other.RefinementParameter & |
| | | 98 | | /// <inheritdoc/> |
| | 0 | 99 | | public override int GetHashCode() => System.HashCode.Combine(RefinementParameter, BaseType, Refinement); |
| | | 100 | | /// <inheritdoc/> |
| | 0 | 101 | | public static bool operator ==(RefinedType? left, RefinedType? right) => EqualityComparer<RefinedType?>.Default. |
| | | 102 | | /// <inheritdoc/> |
| | 0 | 103 | | public static bool operator !=(RefinedType? left, RefinedType? right) => !(left == right); |
| | | 104 | | #endregion |
| | | 105 | | } |
| | | 106 | | } |