зеркало из https://github.com/microsoft/formula.git
Added regression tests
This commit is contained in:
ejackson
Родитель
13cd7fb168
Коммит
f0be0c73f6
|
|
@ -178,6 +178,10 @@ App_Data/*.ldf
|
|||
# Microsoft Fakes
|
||||
FakesAssemblies/
|
||||
|
||||
# =========================
|
||||
# Exclude generated cs files
|
||||
# =========================
|
||||
*.g.cs
|
||||
|
||||
# =========================
|
||||
# Windows detritus
|
||||
|
|
|
|||
|
|
@ -0,0 +1,6 @@
|
|||
<?xml version="1.0" encoding="utf-8" ?>
|
||||
<configuration>
|
||||
<startup>
|
||||
<supportedRuntime version="v4.0" sku=".NETFramework,Version=v4.5" />
|
||||
</startup>
|
||||
</configuration>
|
||||
|
|
@ -0,0 +1,125 @@
|
|||
domain LittleFuncLang
|
||||
{
|
||||
Var ::= new (name: String).
|
||||
Val ::= new (val: Real).
|
||||
Add ::= new (arg1: any Expr, arg2: any Expr).
|
||||
Let ::= new (var: any Var, init: any Expr, in: any Expr).
|
||||
Expr ::= Var + Val + Add + Let.
|
||||
|
||||
//// Records the occurrences of subexpressions under let experessions.
|
||||
//// For example SubExpr(e, p, LEFT, l) means e is the left subexpression of p.
|
||||
//// And l is the deepest let Subexpr in which e occurs.
|
||||
|
||||
Subexpr ::= (expr: Expr,
|
||||
parent: Subexpr + { NIL },
|
||||
loc: { LEFT, RIGHT, NIL },
|
||||
let: Subexpr + { NIL }).
|
||||
|
||||
Subexpr(e, p, l, t) :-
|
||||
e is Expr, p = NIL, l = NIL, t = NIL;
|
||||
p is Subexpr, e = p.expr.arg1, l = LEFT, t = p.let;
|
||||
p is Subexpr, e = p.expr.arg2, l = RIGHT, t = p.let;
|
||||
p is Subexpr, e = p.expr.init, l = LEFT, t = p.let;
|
||||
p is Subexpr, e = p.expr.in, l = RIGHT, t = p.
|
||||
|
||||
//// Bindings map variables to values in the scope of a let expression.
|
||||
//// Initially every variable is mapped to ERROR.
|
||||
|
||||
Binding ::= (var: Var, scope: Subexpr + { NIL }, val: Real + { ERROR }).
|
||||
|
||||
Binding(v, NIL, ERROR) :-
|
||||
s is Subexpr, v = s.expr, v : Var.
|
||||
|
||||
Binding(var, s, v) :-
|
||||
s is Subexpr,
|
||||
s.expr = Let(var, init, _),
|
||||
Eval(init, s.let, v);
|
||||
|
||||
s is Subexpr,
|
||||
s.expr = Let(intro, _, _),
|
||||
Binding(var, s.let, v),
|
||||
var != intro.
|
||||
|
||||
//// Evaluate an expression in a scope.
|
||||
|
||||
Eval ::= (expr: Expr, scope: Subexpr + { NIL }, val: Real + { ERROR }).
|
||||
|
||||
Eval(s.expr, s.let, v) :-
|
||||
s is Subexpr(Val(v), _, _, _).
|
||||
|
||||
Eval(s.expr, s.let, v) :-
|
||||
s is Subexpr, Binding(s.expr, s.let, v).
|
||||
|
||||
Eval(s.expr, s.let, v) :-
|
||||
s is Subexpr, s.expr = Let(_, _, in), Eval(in, s, v).
|
||||
|
||||
Eval(s.expr, s.let, v) :-
|
||||
s is Subexpr,
|
||||
s.expr = Add(e1, _),
|
||||
Eval(e1, s.let, ERROR),
|
||||
v = ERROR;
|
||||
|
||||
s is Subexpr,
|
||||
s.expr = Add(_, e2),
|
||||
Eval(e2, s.let, ERROR),
|
||||
v = ERROR;
|
||||
|
||||
s is Subexpr,
|
||||
s.expr = Add(e1, e2),
|
||||
Eval(e1, s.let, v1),
|
||||
Eval(e2, s.let, v2),
|
||||
v = v1 + v2.
|
||||
}
|
||||
|
||||
//// Evaluates to ERROR because var y is not defined
|
||||
model Prog1 of LittleFuncLang
|
||||
{
|
||||
Let(
|
||||
Var("x"),
|
||||
Val(3),
|
||||
Add(Var("x"), Var("y"))).
|
||||
}
|
||||
|
||||
//// Evaluates to 9
|
||||
model Prog2 of LittleFuncLang
|
||||
{
|
||||
Let(Var("x"),
|
||||
Val(3),
|
||||
Let(
|
||||
Var("y"),
|
||||
Add(Var("x"), Var("x")),
|
||||
Add(Var("x"), Var("y")))).
|
||||
}
|
||||
|
||||
//// Evaluates to 10
|
||||
model Prog3 of LittleFuncLang
|
||||
{
|
||||
Let(
|
||||
Var("x"),
|
||||
Let(Var("x"),
|
||||
Val(3),
|
||||
Add(Val(2), Var("x"))),
|
||||
Add(Var("x"), Var("x"))).
|
||||
}
|
||||
|
||||
//// Evaluates to 10
|
||||
model Prog4 of LittleFuncLang
|
||||
{
|
||||
Let(
|
||||
Var("x"),
|
||||
Let(Var("y"),
|
||||
Val(3),
|
||||
Add(Val(2), Var("y"))),
|
||||
Add(Var("x"), Var("x"))).
|
||||
}
|
||||
|
||||
//// Evaluates to ERROR because var y is used outside of its scope.
|
||||
model Prog5 of LittleFuncLang
|
||||
{
|
||||
Let(
|
||||
Var("x"),
|
||||
Let(Var("y"),
|
||||
Val(3),
|
||||
Add(Val(2), Var("y"))),
|
||||
Add(Var("x"), Var("y"))).
|
||||
}
|
||||
|
|
@ -0,0 +1,78 @@
|
|||
<?xml version="1.0" encoding="utf-8"?>
|
||||
<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
|
||||
<Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />
|
||||
<PropertyGroup>
|
||||
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
|
||||
<Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
|
||||
<ProjectGuid>{89DEB961-3DF1-4826-852A-69EDFF62632D}</ProjectGuid>
|
||||
<OutputType>Exe</OutputType>
|
||||
<AppDesignerFolder>Properties</AppDesignerFolder>
|
||||
<RootNamespace>LittleFuncLang</RootNamespace>
|
||||
<AssemblyName>LittleFuncLang</AssemblyName>
|
||||
<TargetFrameworkVersion>v4.5</TargetFrameworkVersion>
|
||||
<FileAlignment>512</FileAlignment>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
|
||||
<PlatformTarget>x86</PlatformTarget>
|
||||
<DebugSymbols>true</DebugSymbols>
|
||||
<DebugType>full</DebugType>
|
||||
<Optimize>false</Optimize>
|
||||
<OutputPath>bin\Debug\</OutputPath>
|
||||
<DefineConstants>DEBUG;TRACE</DefineConstants>
|
||||
<ErrorReport>prompt</ErrorReport>
|
||||
<WarningLevel>4</WarningLevel>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
|
||||
<PlatformTarget>AnyCPU</PlatformTarget>
|
||||
<DebugType>pdbonly</DebugType>
|
||||
<Optimize>true</Optimize>
|
||||
<OutputPath>bin\Release\</OutputPath>
|
||||
<DefineConstants>TRACE</DefineConstants>
|
||||
<ErrorReport>prompt</ErrorReport>
|
||||
<WarningLevel>4</WarningLevel>
|
||||
</PropertyGroup>
|
||||
<ItemGroup>
|
||||
<Reference Include="Core">
|
||||
<HintPath>..\..\..\..\Bld\Drops\Formula_Debug_x86\Core.dll</HintPath>
|
||||
</Reference>
|
||||
<Reference Include="System" />
|
||||
<Reference Include="System.Core" />
|
||||
<Reference Include="System.Numerics" />
|
||||
<Reference Include="System.Xml.Linq" />
|
||||
<Reference Include="System.Data.DataSetExtensions" />
|
||||
<Reference Include="Microsoft.CSharp" />
|
||||
<Reference Include="System.Data" />
|
||||
<Reference Include="System.Xml" />
|
||||
</ItemGroup>
|
||||
<ItemGroup>
|
||||
<Compile Include="LittleFuncLang.4ml.g.cs">
|
||||
<AutoGen>True</AutoGen>
|
||||
<DesignTime>True</DesignTime>
|
||||
<DependentUpon>LittleFuncLang.4ml</DependentUpon>
|
||||
</Compile>
|
||||
<Compile Include="Program.cs" />
|
||||
<Compile Include="Properties\AssemblyInfo.cs" />
|
||||
</ItemGroup>
|
||||
<ItemGroup>
|
||||
<None Include="App.config" />
|
||||
<None Include="LittleFuncLang.4ml">
|
||||
<Generator>FormulaCodeGenerator</Generator>
|
||||
<LastGenOutput>LittleFuncLang.4ml.g.cs</LastGenOutput>
|
||||
</None>
|
||||
</ItemGroup>
|
||||
<Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
|
||||
<!-- To modify your build process, add your task inside one of the targets below and uncomment it.
|
||||
Other similar extension points exist, see Microsoft.Common.targets.
|
||||
<Target Name="BeforeBuild">
|
||||
</Target>
|
||||
<Target Name="AfterBuild">
|
||||
</Target>
|
||||
-->
|
||||
<UsingTask TaskName="FormulaCodeGeneratorTask.FormulaCodeGeneratorTask" AssemblyFile="..\..\..\..\Src\Extensions\FormulaCodeGeneratorTask\bin\x86\FormulaCodeGeneratorTask.dll" />
|
||||
<Target Name="BeforeBuild" Condition="'$(BuildingInsideVisualStudio)' != 'true'">
|
||||
<ItemGroup>
|
||||
<FormulaGenFiles Include="@(None->'%(FullPath)')" Condition="%(None.Generator) == 'FormulaCodeGenerator'" />
|
||||
</ItemGroup>
|
||||
<FormulaCodeGeneratorTask GeneratorInputs="@(FormulaGenFiles->'%(FullPath),%(CustomToolNamespace),%(IsThreadSafe),%(IsObjectGraph),%(IsNewOnly)')" DefaultNamespace="$(RootNamespace)" />
|
||||
</Target>
|
||||
</Project>
|
||||
|
|
@ -0,0 +1,20 @@
|
|||
|
||||
Microsoft Visual Studio Solution File, Format Version 12.00
|
||||
# Visual Studio 2012
|
||||
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "LittleFuncLang", "LittleFuncLang.csproj", "{89DEB961-3DF1-4826-852A-69EDFF62632D}"
|
||||
EndProject
|
||||
Global
|
||||
GlobalSection(SolutionConfigurationPlatforms) = preSolution
|
||||
Debug|Any CPU = Debug|Any CPU
|
||||
Release|Any CPU = Release|Any CPU
|
||||
EndGlobalSection
|
||||
GlobalSection(ProjectConfigurationPlatforms) = postSolution
|
||||
{89DEB961-3DF1-4826-852A-69EDFF62632D}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
|
||||
{89DEB961-3DF1-4826-852A-69EDFF62632D}.Debug|Any CPU.Build.0 = Debug|Any CPU
|
||||
{89DEB961-3DF1-4826-852A-69EDFF62632D}.Release|Any CPU.ActiveCfg = Release|Any CPU
|
||||
{89DEB961-3DF1-4826-852A-69EDFF62632D}.Release|Any CPU.Build.0 = Release|Any CPU
|
||||
EndGlobalSection
|
||||
GlobalSection(SolutionProperties) = preSolution
|
||||
HideSolutionNode = FALSE
|
||||
EndGlobalSection
|
||||
EndGlobal
|
||||
|
|
@ -0,0 +1,130 @@
|
|||
namespace LittleFuncLang
|
||||
{
|
||||
using System;
|
||||
using System.Collections.Generic;
|
||||
using System.IO;
|
||||
using System.Linq;
|
||||
using System.Text;
|
||||
using System.Threading.Tasks;
|
||||
|
||||
using Microsoft.Formula.API;
|
||||
using Microsoft.Formula.API.Generators;
|
||||
using Microsoft.Formula.API.Nodes;
|
||||
|
||||
class Program
|
||||
{
|
||||
private static string formulaFile;
|
||||
|
||||
static void Main(string[] args)
|
||||
{
|
||||
var asDir = new DirectoryInfo(System.Reflection.Assembly.GetExecutingAssembly().Location);
|
||||
formulaFile = asDir.Parent.Parent.Parent.FullName + "\\LittleFuncLang.4ml";
|
||||
|
||||
List<ICSharpTerm> objects;
|
||||
AST<Model> model;
|
||||
|
||||
if (LoadModelFromFile("Prog4", out objects))
|
||||
{
|
||||
ToAST("Prog4", objects, out model);
|
||||
|
||||
LittleFuncLang_Root.Let letExpr = null;
|
||||
foreach (var o in objects)
|
||||
{
|
||||
if (o is LittleFuncLang_Root.Let)
|
||||
{
|
||||
letExpr = (LittleFuncLang_Root.Let)o;
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
if (letExpr == null)
|
||||
{
|
||||
Console.WriteLine("Could not find a let expression");
|
||||
}
|
||||
else
|
||||
{
|
||||
letExpr.@in = (LittleFuncLang_Root.IArgType_Let__2)letExpr.init;
|
||||
}
|
||||
|
||||
ToAST("Prog4'", objects, out model);
|
||||
}
|
||||
}
|
||||
|
||||
private static bool ToAST(string modelName, List<ICSharpTerm> objects, out AST<Model> model)
|
||||
{
|
||||
var result = Factory.Instance.MkModel(
|
||||
modelName,
|
||||
"LittleFuncLang",
|
||||
objects,
|
||||
out model,
|
||||
null,
|
||||
"LittleFuncLang.4ml");
|
||||
|
||||
if (result)
|
||||
{
|
||||
model.Print(Console.Out);
|
||||
return true;
|
||||
}
|
||||
else
|
||||
{
|
||||
Console.WriteLine("Could not build model from object graph");
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
private static bool LoadModelFromFile(string model, out List<ICSharpTerm> objects)
|
||||
{
|
||||
objects = null;
|
||||
|
||||
InstallResult res;
|
||||
var env = new Env();
|
||||
if (!env.Install(formulaFile, out res) && res == null)
|
||||
{
|
||||
throw new Exception("Could not start installation");
|
||||
}
|
||||
|
||||
foreach (var f in res.Flags)
|
||||
{
|
||||
Console.WriteLine("{0} ({1}, {2}) : {3} {4} : {5}",
|
||||
f.Item1.Node.Name,
|
||||
f.Item2.Span.StartLine,
|
||||
f.Item2.Span.StartCol,
|
||||
f.Item2.Severity,
|
||||
f.Item2.Code,
|
||||
f.Item2.Message);
|
||||
}
|
||||
|
||||
if (!res.Succeeded)
|
||||
{
|
||||
Console.WriteLine("Could not install file; exiting");
|
||||
return false;
|
||||
}
|
||||
|
||||
Task<ObjectGraphResult> createTask;
|
||||
if (!LittleFuncLang_Root.CreateObjectGraph(env, new ProgramName(formulaFile), "Prog4", out createTask))
|
||||
{
|
||||
throw new Exception("Could not start object graph creation");
|
||||
}
|
||||
|
||||
createTask.Wait();
|
||||
foreach (var f in createTask.Result.Flags)
|
||||
{
|
||||
Console.WriteLine("({0}, {1}) : {2} {3} : {4}",
|
||||
f.Span.StartLine,
|
||||
f.Span.StartCol,
|
||||
f.Severity,
|
||||
f.Code,
|
||||
f.Message);
|
||||
}
|
||||
|
||||
if (!createTask.Result.Succeeded)
|
||||
{
|
||||
Console.WriteLine("Could not create object graph {0}; exiting", model);
|
||||
return false;
|
||||
}
|
||||
|
||||
objects = createTask.Result.Objects;
|
||||
return true;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -0,0 +1,36 @@
|
|||
using System.Reflection;
|
||||
using System.Runtime.CompilerServices;
|
||||
using System.Runtime.InteropServices;
|
||||
|
||||
// General Information about an assembly is controlled through the following
|
||||
// set of attributes. Change these attribute values to modify the information
|
||||
// associated with an assembly.
|
||||
[assembly: AssemblyTitle("LittleFuncLang")]
|
||||
[assembly: AssemblyDescription("")]
|
||||
[assembly: AssemblyConfiguration("")]
|
||||
[assembly: AssemblyCompany("")]
|
||||
[assembly: AssemblyProduct("LittleFuncLang")]
|
||||
[assembly: AssemblyCopyright("Copyright © 2013")]
|
||||
[assembly: AssemblyTrademark("")]
|
||||
[assembly: AssemblyCulture("")]
|
||||
|
||||
// Setting ComVisible to false makes the types in this assembly not visible
|
||||
// to COM components. If you need to access a type in this assembly from
|
||||
// COM, set the ComVisible attribute to true on that type.
|
||||
[assembly: ComVisible(false)]
|
||||
|
||||
// The following GUID is for the ID of the typelib if this project is exposed to COM
|
||||
[assembly: Guid("430fd9e7-b0dc-44d6-bf4f-d3d4f7ef2083")]
|
||||
|
||||
// Version information for an assembly consists of the following four values:
|
||||
//
|
||||
// Major Version
|
||||
// Minor Version
|
||||
// Build Number
|
||||
// Revision
|
||||
//
|
||||
// You can specify all the values or you can default the Build and Revision Numbers
|
||||
// by using the '*' as shown below:
|
||||
// [assembly: AssemblyVersion("1.0.*")]
|
||||
[assembly: AssemblyVersion("1.0.0.0")]
|
||||
[assembly: AssemblyFileVersion("1.0.0.0")]
|
||||
|
|
@ -0,0 +1,15 @@
|
|||
=================================
|
||||
Console output
|
||||
=================================
|
||||
OUT: model Prog4 of LittleFuncLang at "LittleFuncLang.4ml"
|
||||
OUT: {
|
||||
OUT: Let(Var("x"), Let(Var("y"), Val(3), Add(Val(2), Var("y"))), Add(Var("x"), Var("x"))).
|
||||
OUT: }
|
||||
OUT:
|
||||
OUT: model Prog4' of LittleFuncLang at "LittleFuncLang.4ml"
|
||||
OUT: {
|
||||
OUT: Let(Var("x"), Let(Var("y"), Val(3), Add(Val(2), Var("y"))), Let(Var("y"), Val(3), Add(Val(2), Var("y")))).
|
||||
OUT: }
|
||||
OUT:
|
||||
OUT:
|
||||
EXIT: 0
|
||||
|
|
@ -0,0 +1,3 @@
|
|||
run: bin\Debug\LittleFuncLang.exe
|
||||
dsc: Test code generator and loading / converting object graphs
|
||||
acc: .\
|
||||
|
|
@ -0,0 +1,37 @@
|
|||
=================================
|
||||
Console output
|
||||
=================================
|
||||
OUT:
|
||||
OUT: []> v off
|
||||
OUT: verbose off
|
||||
OUT:
|
||||
OUT: []> l tests.4ml
|
||||
OUT: (Failed) tests.4ml
|
||||
OUT: tests.4ml (3, 14): The type id _ is undefined.
|
||||
OUT: tests.4ml (8, 4): _ is not a legal symbol identifier
|
||||
OUT: tests.4ml (13, 17): _ is not a legal label identifier
|
||||
OUT: tests.4ml (18, 17): _ is not a legal label identifier
|
||||
OUT: tests.4ml (18, 20): The type id _ is undefined.
|
||||
OUT: tests.4ml (23, 20): The type id _ is undefined.
|
||||
OUT: tests.4ml (29, 25): The label a has multiple definitions. See index 1 and index 0
|
||||
OUT: tests.4ml (30, 17): The type id H is undefined.
|
||||
OUT: tests.4ml (32, 12): The type id A is undefined.
|
||||
OUT: tests.4ml (32, 16): The type id B is undefined.
|
||||
OUT: tests.4ml (33, 12): The type id _ is undefined.
|
||||
OUT: tests.4ml (34, 12): The type id BadTypeNames._ is undefined.
|
||||
OUT: tests.4ml (35, 12): The type id _ is undefined.
|
||||
OUT: tests.4ml (35, 16): The type id BadTypeNames._ is undefined.
|
||||
OUT: tests.4ml (45, 18): The type id Any is ambiguous. See (43, 19): A1.Any and (43, 1): B1.Any
|
||||
OUT: tests.4ml (45, 24): The type id Data is ambiguous. See (43, 19): A1.Data and (43, 1): B1.Data
|
||||
OUT: tests.4ml (56, 15): The type F has multiple definitions. See (56, 15) and (54, 19)
|
||||
OUT: tests.4ml (66, 4): The symbol F has multiple definitions. See (66, 4) and (64, 19)
|
||||
OUT: tests.4ml (76, 4): The symbol F has multiple definitions. See (76, 4) and (74, 19)
|
||||
OUT: tests.4ml (86, 4): The symbol F has multiple definitions. See (86, 4) and (84, 19)
|
||||
OUT: tests.4ml (96, 4): The symbol F has multiple definitions. See (96, 4) and (94, 19)
|
||||
OUT: tests.4ml (106, 4): The symbol F has multiple definitions. See (106, 4) and (104, 19)
|
||||
OUT: tests.4ml (116, 10): The type id F is ambiguous. See (114, 19): X.F and (114, 26): Y.F
|
||||
OUT: tests.4ml (0, 0): The install operation failed
|
||||
OUT:
|
||||
OUT: []> x
|
||||
OUT:
|
||||
EXIT: 1
|
||||
|
|
@ -0,0 +1,4 @@
|
|||
run: ..\..\..\..\Bld\Drops\Formula_Debug_x86\Formula.exe
|
||||
arg: -v: off -l: "tests.4ml" -x
|
||||
acc: .\
|
||||
dsc: Type declarations that are wrong
|
||||
|
|
@ -0,0 +1,120 @@
|
|||
domain BadRuleForms
|
||||
{
|
||||
q4 :- _ is _.
|
||||
}
|
||||
|
||||
domain BadData1
|
||||
{
|
||||
_ ::= new (i: Integer).
|
||||
}
|
||||
|
||||
domain BadData2
|
||||
{
|
||||
F ::= new (_: Integer).
|
||||
}
|
||||
|
||||
domain BadData3
|
||||
{
|
||||
G ::= new (_: _).
|
||||
}
|
||||
|
||||
domain BadData4
|
||||
{
|
||||
H ::= new (a: _).
|
||||
}
|
||||
|
||||
domain BadData5
|
||||
{
|
||||
G ::= new (Integer).
|
||||
I ::= fun (a: G -> a: G).
|
||||
J ::= new (H).
|
||||
|
||||
U1 ::= A + B + Integer.
|
||||
U2 ::= _ + Integer.
|
||||
U3 ::= BadTypeNames._ + Integer.
|
||||
U4 ::= _ + BadTypeNames._.
|
||||
}
|
||||
|
||||
domain A1
|
||||
{
|
||||
|
||||
}
|
||||
|
||||
domain B1 extends A1
|
||||
{
|
||||
Ambiguity ::= Any + Data.
|
||||
}
|
||||
|
||||
|
||||
domain A2
|
||||
{
|
||||
F ::= new (PosInteger + { TRUE }).
|
||||
}
|
||||
|
||||
domain B2 extends A2
|
||||
{
|
||||
F ::= new (PosInteger + { FALSE }).
|
||||
}
|
||||
|
||||
domain A3
|
||||
{
|
||||
F ::= new (a: String, Integer).
|
||||
}
|
||||
|
||||
domain B3 extends A3
|
||||
{
|
||||
F ::= new (String, a: Integer).
|
||||
}
|
||||
|
||||
domain A4
|
||||
{
|
||||
F ::= fun (a: String -> Integer).
|
||||
}
|
||||
|
||||
domain B4 extends A4
|
||||
{
|
||||
F ::= inj (a: String -> Integer).
|
||||
}
|
||||
|
||||
domain A5
|
||||
{
|
||||
F ::= fun (a: String -> Integer).
|
||||
}
|
||||
|
||||
domain B5 extends A5
|
||||
{
|
||||
F ::= new (a: String, Integer).
|
||||
}
|
||||
|
||||
domain A6
|
||||
{
|
||||
F ::= (a: String, Integer).
|
||||
}
|
||||
|
||||
domain B6 extends A6
|
||||
{
|
||||
F ::= new (a: String, Integer).
|
||||
}
|
||||
|
||||
domain A7
|
||||
{
|
||||
F ::= (String).
|
||||
}
|
||||
|
||||
domain B7 extends A7
|
||||
{
|
||||
F ::= (String, Integer).
|
||||
}
|
||||
|
||||
domain A8
|
||||
{
|
||||
F ::= (String).
|
||||
}
|
||||
|
||||
domain B8 extends X::A8, Y::A8
|
||||
{
|
||||
U ::= F.
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
|
@ -0,0 +1,238 @@
|
|||
namespace ListParser
|
||||
{
|
||||
using System;
|
||||
using System.Collections.Generic;
|
||||
using System.Diagnostics.Contracts;
|
||||
using System.IO;
|
||||
using System.Linq;
|
||||
using System.Text;
|
||||
using System.Threading.Tasks;
|
||||
|
||||
using Microsoft.Formula.API;
|
||||
using Microsoft.Formula.API.ASTQueries;
|
||||
using Microsoft.Formula.API.Nodes;
|
||||
using Microsoft.Formula.API.Plugins;
|
||||
using Microsoft.Formula.Compiler;
|
||||
using Microsoft.Formula.Common;
|
||||
|
||||
public class ListParser : IQuoteParser
|
||||
{
|
||||
private enum ParserState { None, Nat, Id };
|
||||
|
||||
private static readonly Tuple<string, CnstKind>[] noSettings = new Tuple<string, CnstKind>[0];
|
||||
private static readonly AST<Domain> listDomain;
|
||||
private const string consName = "Cons";
|
||||
private const string nilName = "NIL";
|
||||
private const char idPrefix = '$';
|
||||
private const string idPrefixStr = "$";
|
||||
private const string listDomainStr =
|
||||
@"
|
||||
domain Lists
|
||||
{{
|
||||
{0} ::= new (left: any {0} + Natural + {{ {1} }}, right: any {0} + Natural + {{ {1} }}).
|
||||
}}
|
||||
";
|
||||
|
||||
static ListParser()
|
||||
{
|
||||
var progName = new ProgramName("env:///temp.4ml");
|
||||
var progText = string.Format(listDomainStr, consName, nilName);
|
||||
var task = Factory.Instance.ParseText(progName, progText);
|
||||
task.Wait();
|
||||
if (!task.Result.Succeeded)
|
||||
{
|
||||
throw new Exception("Could not parse domain definition");
|
||||
}
|
||||
|
||||
var query = new NodePred[] {
|
||||
NodePredFactory.Instance.Star,
|
||||
NodePredFactory.Instance.MkPredicate(NodeKind.Domain) };
|
||||
listDomain = (AST<Domain>)task.Result.Program.FindAny(query);
|
||||
}
|
||||
|
||||
public string UnquotePrefix
|
||||
{
|
||||
get { return idPrefixStr; }
|
||||
}
|
||||
|
||||
public AST<Domain> SuggestedDataModel
|
||||
{
|
||||
get { return listDomain; }
|
||||
}
|
||||
|
||||
public IEnumerable<Tuple<string, CnstKind>> SuggestedSettings
|
||||
{
|
||||
get { return noSettings; }
|
||||
}
|
||||
|
||||
public ListParser()
|
||||
{
|
||||
}
|
||||
|
||||
public IQuoteParser CreateInstance(
|
||||
AST<Node> module,
|
||||
string collectionName,
|
||||
string instanceName)
|
||||
{
|
||||
return new ListParser();
|
||||
}
|
||||
|
||||
public bool Parse(
|
||||
Configuration config,
|
||||
Stream quoteStream,
|
||||
SourcePositioner positioner,
|
||||
out AST<Node> results,
|
||||
out List<Flag> flags)
|
||||
{
|
||||
results = null;
|
||||
flags = new List<Flag>();
|
||||
var lines = new LinkedList<string>();
|
||||
var revList = new LinkedList<AST<Node>>();
|
||||
using (var sr = new StreamReader(quoteStream))
|
||||
{
|
||||
while (!sr.EndOfStream)
|
||||
{
|
||||
lines.AddLast(sr.ReadLine());
|
||||
}
|
||||
}
|
||||
|
||||
char c;
|
||||
string token = string.Empty;
|
||||
var state = ParserState.None;
|
||||
int lineNum = 0, colNum = 0;
|
||||
int sL = 0, sC = 0;
|
||||
foreach (var line in lines)
|
||||
{
|
||||
for (colNum = 0; colNum < line.Length; ++colNum)
|
||||
{
|
||||
c = line[colNum];
|
||||
if (char.IsDigit(c))
|
||||
{
|
||||
token += c;
|
||||
if (state == ParserState.None)
|
||||
{
|
||||
state = ParserState.Nat;
|
||||
sL = lineNum;
|
||||
sC = colNum;
|
||||
}
|
||||
}
|
||||
else if (c == idPrefix)
|
||||
{
|
||||
if (state == ParserState.None)
|
||||
{
|
||||
token = idPrefixStr;
|
||||
state = ParserState.Id;
|
||||
sL = lineNum;
|
||||
sC = colNum;
|
||||
}
|
||||
else
|
||||
{
|
||||
flags.Add(new Flag(
|
||||
SeverityKind.Error,
|
||||
positioner.GetSourcePosition(lineNum, colNum, lineNum, colNum),
|
||||
Constants.QuotationError.ToString("Unexpected character " + c),
|
||||
Constants.QuotationError.Code));
|
||||
return false;
|
||||
}
|
||||
}
|
||||
else if (c == ' ' || c == '\t')
|
||||
{
|
||||
if (state == ParserState.Nat)
|
||||
{
|
||||
Contract.Assert(token.Length > 0);
|
||||
Rational r;
|
||||
Rational.TryParseFraction(token, out r);
|
||||
revList.AddFirst(Factory.Instance.MkCnst(r, positioner.GetSourcePosition(sL, sC, lineNum, colNum - 1)));
|
||||
token = string.Empty;
|
||||
}
|
||||
else if (state == ParserState.Id)
|
||||
{
|
||||
if (token.Length < 2)
|
||||
{
|
||||
flags.Add(new Flag(
|
||||
SeverityKind.Error,
|
||||
positioner.GetSourcePosition(lineNum, colNum, lineNum, colNum),
|
||||
Constants.QuotationError.ToString("Bad id"),
|
||||
Constants.QuotationError.Code));
|
||||
return false;
|
||||
}
|
||||
|
||||
revList.AddFirst(Factory.Instance.MkId(token, positioner.GetSourcePosition(sL, sC, lineNum, colNum - 1)));
|
||||
token = string.Empty;
|
||||
}
|
||||
|
||||
state = ParserState.None;
|
||||
}
|
||||
else
|
||||
{
|
||||
flags.Add(new Flag(
|
||||
SeverityKind.Error,
|
||||
positioner.GetSourcePosition(lineNum, colNum, lineNum, colNum),
|
||||
Constants.QuotationError.ToString("Unexpected character " + c),
|
||||
Constants.QuotationError.Code));
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
if (state == ParserState.Nat)
|
||||
{
|
||||
Contract.Assert(token.Length > 0);
|
||||
Rational r;
|
||||
Rational.TryParseFraction(token, out r);
|
||||
revList.AddFirst(Factory.Instance.MkCnst(r, positioner.GetSourcePosition(sL, sC, lineNum, colNum)));
|
||||
}
|
||||
else if (state == ParserState.Id)
|
||||
{
|
||||
if (token.Length < 2)
|
||||
{
|
||||
flags.Add(new Flag(
|
||||
SeverityKind.Error,
|
||||
positioner.GetSourcePosition(lineNum, colNum, lineNum, colNum),
|
||||
Constants.QuotationError.ToString("Bad id"),
|
||||
Constants.QuotationError.Code));
|
||||
return false;
|
||||
}
|
||||
|
||||
revList.AddFirst(Factory.Instance.MkId(token, positioner.GetSourcePosition(sL, sC, lineNum, colNum)));
|
||||
}
|
||||
|
||||
token = string.Empty;
|
||||
state = ParserState.None;
|
||||
++lineNum;
|
||||
}
|
||||
|
||||
if (revList.Count == 0)
|
||||
{
|
||||
results = Factory.Instance.MkId(nilName, positioner.GetSourcePosition(0, 0, 0, 0));
|
||||
}
|
||||
else
|
||||
{
|
||||
foreach (var item in revList)
|
||||
{
|
||||
if (results == null)
|
||||
{
|
||||
results = item;
|
||||
}
|
||||
else
|
||||
{
|
||||
results = Factory.Instance.AddArg(
|
||||
Factory.Instance.MkFuncTerm(Factory.Instance.MkId(consName, item.Node.Span), item.Node.Span),
|
||||
results);
|
||||
results = Factory.Instance.AddArg((AST<FuncTerm>)results, item, false);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
public bool Render(
|
||||
Configuration config,
|
||||
TextWriter writer,
|
||||
AST<Node> ast,
|
||||
out List<Flag> flags)
|
||||
{
|
||||
throw new NotImplementedException();
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -0,0 +1,57 @@
|
|||
<?xml version="1.0" encoding="utf-8"?>
|
||||
<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
|
||||
<Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />
|
||||
<PropertyGroup>
|
||||
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
|
||||
<Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
|
||||
<ProjectGuid>{ED7B13FC-FDCD-4230-A404-8EF9CFF7E321}</ProjectGuid>
|
||||
<OutputType>Library</OutputType>
|
||||
<AppDesignerFolder>Properties</AppDesignerFolder>
|
||||
<RootNamespace>ListParser</RootNamespace>
|
||||
<AssemblyName>ListParser</AssemblyName>
|
||||
<TargetFrameworkVersion>v4.5</TargetFrameworkVersion>
|
||||
<FileAlignment>512</FileAlignment>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
|
||||
<DebugSymbols>true</DebugSymbols>
|
||||
<DebugType>full</DebugType>
|
||||
<Optimize>false</Optimize>
|
||||
<OutputPath>bin\Debug\</OutputPath>
|
||||
<DefineConstants>DEBUG;TRACE</DefineConstants>
|
||||
<ErrorReport>prompt</ErrorReport>
|
||||
<WarningLevel>4</WarningLevel>
|
||||
<PlatformTarget>x86</PlatformTarget>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
|
||||
<DebugType>pdbonly</DebugType>
|
||||
<Optimize>true</Optimize>
|
||||
<OutputPath>bin\Release\</OutputPath>
|
||||
<DefineConstants>TRACE</DefineConstants>
|
||||
<ErrorReport>prompt</ErrorReport>
|
||||
<WarningLevel>4</WarningLevel>
|
||||
</PropertyGroup>
|
||||
<ItemGroup>
|
||||
<Reference Include="Core">
|
||||
<HintPath>..\..\..\..\Bld\Drops\Formula_Debug_x86\Core.dll</HintPath>
|
||||
</Reference>
|
||||
<Reference Include="System" />
|
||||
<Reference Include="System.Core" />
|
||||
<Reference Include="System.Xml.Linq" />
|
||||
<Reference Include="System.Data.DataSetExtensions" />
|
||||
<Reference Include="Microsoft.CSharp" />
|
||||
<Reference Include="System.Data" />
|
||||
<Reference Include="System.Xml" />
|
||||
</ItemGroup>
|
||||
<ItemGroup>
|
||||
<Compile Include="ListParser.cs" />
|
||||
<Compile Include="Properties\AssemblyInfo.cs" />
|
||||
</ItemGroup>
|
||||
<Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
|
||||
<!-- To modify your build process, add your task inside one of the targets below and uncomment it.
|
||||
Other similar extension points exist, see Microsoft.Common.targets.
|
||||
<Target Name="BeforeBuild">
|
||||
</Target>
|
||||
<Target Name="AfterBuild">
|
||||
</Target>
|
||||
-->
|
||||
</Project>
|
||||
|
|
@ -0,0 +1,20 @@
|
|||
|
||||
Microsoft Visual Studio Solution File, Format Version 12.00
|
||||
# Visual Studio 2012
|
||||
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ListParser", "ListParser.csproj", "{ED7B13FC-FDCD-4230-A404-8EF9CFF7E321}"
|
||||
EndProject
|
||||
Global
|
||||
GlobalSection(SolutionConfigurationPlatforms) = preSolution
|
||||
Debug|Any CPU = Debug|Any CPU
|
||||
Release|Any CPU = Release|Any CPU
|
||||
EndGlobalSection
|
||||
GlobalSection(ProjectConfigurationPlatforms) = postSolution
|
||||
{ED7B13FC-FDCD-4230-A404-8EF9CFF7E321}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
|
||||
{ED7B13FC-FDCD-4230-A404-8EF9CFF7E321}.Debug|Any CPU.Build.0 = Debug|Any CPU
|
||||
{ED7B13FC-FDCD-4230-A404-8EF9CFF7E321}.Release|Any CPU.ActiveCfg = Release|Any CPU
|
||||
{ED7B13FC-FDCD-4230-A404-8EF9CFF7E321}.Release|Any CPU.Build.0 = Release|Any CPU
|
||||
EndGlobalSection
|
||||
GlobalSection(SolutionProperties) = preSolution
|
||||
HideSolutionNode = FALSE
|
||||
EndGlobalSection
|
||||
EndGlobal
|
||||
|
|
@ -0,0 +1,36 @@
|
|||
using System.Reflection;
|
||||
using System.Runtime.CompilerServices;
|
||||
using System.Runtime.InteropServices;
|
||||
|
||||
// General Information about an assembly is controlled through the following
|
||||
// set of attributes. Change these attribute values to modify the information
|
||||
// associated with an assembly.
|
||||
[assembly: AssemblyTitle("ListParser")]
|
||||
[assembly: AssemblyDescription("")]
|
||||
[assembly: AssemblyConfiguration("")]
|
||||
[assembly: AssemblyCompany("")]
|
||||
[assembly: AssemblyProduct("ListParser")]
|
||||
[assembly: AssemblyCopyright("Copyright © 2013")]
|
||||
[assembly: AssemblyTrademark("")]
|
||||
[assembly: AssemblyCulture("")]
|
||||
|
||||
// Setting ComVisible to false makes the types in this assembly not visible
|
||||
// to COM components. If you need to access a type in this assembly from
|
||||
// COM, set the ComVisible attribute to true on that type.
|
||||
[assembly: ComVisible(false)]
|
||||
|
||||
// The following GUID is for the ID of the typelib if this project is exposed to COM
|
||||
[assembly: Guid("cddc639d-3af8-460c-8e4c-c39fca365b62")]
|
||||
|
||||
// Version information for an assembly consists of the following four values:
|
||||
//
|
||||
// Major Version
|
||||
// Minor Version
|
||||
// Build Number
|
||||
// Revision
|
||||
//
|
||||
// You can specify all the values or you can default the Build and Revision Numbers
|
||||
// by using the '*' as shown below:
|
||||
// [assembly: AssemblyVersion("1.0.*")]
|
||||
[assembly: AssemblyVersion("1.0.0.0")]
|
||||
[assembly: AssemblyFileVersion("1.0.0.0")]
|
||||
|
|
@ -0,0 +1,17 @@
|
|||
=================================
|
||||
Console output
|
||||
=================================
|
||||
OUT:
|
||||
OUT: []> v off
|
||||
OUT: verbose off
|
||||
OUT:
|
||||
OUT: []> l tests.4ml
|
||||
OUT: (Failed) tests.4ml
|
||||
OUT: tests.4ml (14, 16): Syntax error - Only data constructors can appear here.
|
||||
OUT: tests.4ml (20, 5): Argument 1 of function R is badly typed.
|
||||
OUT: tests.4ml (25, 12): Argument 2 of function Cons is badly typed.
|
||||
OUT: tests.4ml (0, 0): The install operation failed
|
||||
OUT:
|
||||
OUT: []> x
|
||||
OUT:
|
||||
EXIT: 1
|
||||
|
|
@ -0,0 +1,4 @@
|
|||
run: ..\..\..\..\Bld\Drops\Formula_Debug_x86\Formula.exe
|
||||
arg: -v: off -l: "tests.4ml" -x
|
||||
acc: .\
|
||||
dsc: Test various terms that render correctly, but are later incorrect.
|
||||
|
|
@ -0,0 +1,27 @@
|
|||
[
|
||||
parsers.ListParser = '"ListParser at ..\ListParser\bin\Debug\ListParser.dll"',
|
||||
parse_ActiveParser = "ListParser"
|
||||
]
|
||||
|
||||
domain Lists
|
||||
{
|
||||
Cons ::= new (right: any Cons + Natural + { NIL }, left: any Cons + Natural + { NIL } ).
|
||||
R ::= new (Integer).
|
||||
}
|
||||
|
||||
model M1 of Lists
|
||||
{
|
||||
`1 $`2 $ 3 + 4 $`$`.
|
||||
}
|
||||
|
||||
|
||||
model M2 of Lists
|
||||
{
|
||||
R(`1 $`2 $ 3 $`$`).
|
||||
}
|
||||
|
||||
model M3 of Lists
|
||||
{
|
||||
R(`1 $`2 $ "3" $`$`).
|
||||
}
|
||||
|
||||
|
|
@ -0,0 +1,24 @@
|
|||
=================================
|
||||
Console output
|
||||
=================================
|
||||
OUT:
|
||||
OUT: []> v off
|
||||
OUT: verbose off
|
||||
OUT:
|
||||
OUT: []> l tests.4ml
|
||||
OUT: (Failed) tests.4ml
|
||||
OUT: tests.4ml (14, 4): Could not parse or render.
|
||||
OUT: tests.4ml (14, 31): Could not parse or render. Unexpected character $
|
||||
OUT: tests.4ml (21, 4): Could not parse or render.
|
||||
OUT: tests.4ml (25, 5): Could not parse or render. Unexpected character a
|
||||
OUT: tests.4ml (33, 24): Could not parse or render.
|
||||
OUT: tests.4ml (33, 26): Could not parse or render. Unexpected character `
|
||||
OUT: tests.4ml (40, 13): Could not parse or render.
|
||||
OUT: tests.4ml (41, 24): Could not parse or render. Unexpected character b
|
||||
OUT: tests.4ml (47, 5): Could not parse or render.
|
||||
OUT: tests.4ml (52, 15): Could not parse or render. Unexpected character a
|
||||
OUT: tests.4ml (0, 0): The install operation failed
|
||||
OUT:
|
||||
OUT: []> x
|
||||
OUT:
|
||||
EXIT: 1
|
||||
|
|
@ -0,0 +1,4 @@
|
|||
run: ..\..\..\..\Bld\Drops\Formula_Debug_x86\Formula.exe
|
||||
arg: -v: off -l: "tests.4ml" -x
|
||||
acc: .\
|
||||
dsc: Test various unrenderable terms.
|
||||
|
|
@ -0,0 +1,61 @@
|
|||
[
|
||||
parsers.ListParser = '"ListParser at ..\ListParser\bin\Debug\ListParser.dll"',
|
||||
parse_ActiveParser = "ListParser"
|
||||
]
|
||||
|
||||
domain Lists
|
||||
{
|
||||
Cons ::= new (right: any Cons + Natural + { NIL }, left: any Cons + Natural + { NIL } ).
|
||||
}
|
||||
|
||||
model M1 of Lists
|
||||
{
|
||||
|
||||
`1 2 $ Cons(5, NIL) $ 3 4 5$$`.
|
||||
|
||||
}
|
||||
|
||||
model M2 of Lists
|
||||
{
|
||||
|
||||
`$NIL$1
|
||||
2 $ Cons(5,
|
||||
NIL) $ 3
|
||||
|
||||
a4
|
||||
|
||||
|
||||
5`.
|
||||
}
|
||||
|
||||
model M3 of Lists
|
||||
{
|
||||
`1 $`2 $ Cons(NIL, ` `` `) $`$`.
|
||||
}
|
||||
|
||||
model M4 of Lists
|
||||
{
|
||||
`1
|
||||
$
|
||||
`2 $
|
||||
NIL $b`$`.
|
||||
}
|
||||
|
||||
model M5 of Lists
|
||||
{
|
||||
|
||||
`1 $`2 $ 3 $`$
|
||||
$NIL$1
|
||||
2 $ Cons(5,
|
||||
NIL) $ 3
|
||||
|
||||
a4
|
||||
|
||||
|
||||
5
|
||||
|
||||
`.
|
||||
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -0,0 +1,774 @@
|
|||
=================================
|
||||
Console output
|
||||
=================================
|
||||
OUT:
|
||||
OUT: []> v off
|
||||
OUT: verbose off
|
||||
OUT:
|
||||
OUT: []> l tests.4ml
|
||||
OUT: (Compiled) tests.4ml
|
||||
OUT:
|
||||
OUT: []> dt A1
|
||||
OUT: Reduced form
|
||||
OUT: domain A1
|
||||
OUT: {
|
||||
OUT: Cons ::= new (val: Integer, tail: any Cons + { NIL }).
|
||||
OUT: Things ::= Cons.
|
||||
OUT: }
|
||||
OUT:
|
||||
OUT: Symbol table
|
||||
OUT: Space | Name | Arity | Kind
|
||||
OUT: -------|---------------|-------|-------
|
||||
OUT: | Boolean | 0 | unn
|
||||
OUT: | Cons | 2 | con
|
||||
OUT: | FALSE | 0 | ncnst
|
||||
OUT: | Integer | 0 | unn
|
||||
OUT: | NIL | 0 | ncnst
|
||||
OUT: | Natural | 0 | unn
|
||||
OUT: | NegInteger | 0 | unn
|
||||
OUT: | PosInteger | 0 | unn
|
||||
OUT: | Real | 0 | unn
|
||||
OUT: | String | 0 | unn
|
||||
OUT: | TRUE | 0 | ncnst
|
||||
OUT: | Things | 0 | unn
|
||||
OUT: A1 | Any | 0 | unn
|
||||
OUT: A1 | Constant | 0 | unn
|
||||
OUT: A1 | Data | 0 | unn
|
||||
OUT: A1 | conforms | 0 | dcnst
|
||||
OUT: A1 | notFunctional | 0 | dcnst
|
||||
OUT: A1 | notInjective | 0 | dcnst
|
||||
OUT: A1 | notInvTotal | 0 | dcnst
|
||||
OUT: A1 | notRelational | 0 | dcnst
|
||||
OUT: A1 | notTotal | 0 | dcnst
|
||||
OUT:
|
||||
OUT: Type constants: #Boolean #Cons #Cons[0] #Cons[1] #Integer #Natural #NegInteger #PosInteger #Real #String #Things A1.#Any A1.#Constant A1.#Data
|
||||
OUT: Symbolic constants:
|
||||
OUT: Rationals:
|
||||
OUT: Strings:
|
||||
OUT: Variables:
|
||||
OUT:
|
||||
OUT: []> typ A1
|
||||
OUT:
|
||||
OUT: []> dt A1'
|
||||
OUT: Reduced form
|
||||
OUT: domain A1'
|
||||
OUT: {
|
||||
OUT: List ::= Cons + { NIL }.
|
||||
OUT: Cons ::= new (val: Real, tail: any List).
|
||||
OUT: Things ::= Cons + List.
|
||||
OUT: }
|
||||
OUT:
|
||||
OUT: Symbol table
|
||||
OUT: Space | Name | Arity | Kind
|
||||
OUT: -------|---------------|-------|-------
|
||||
OUT: | Boolean | 0 | unn
|
||||
OUT: | Cons | 2 | con
|
||||
OUT: | FALSE | 0 | ncnst
|
||||
OUT: | Integer | 0 | unn
|
||||
OUT: | List | 0 | unn
|
||||
OUT: | NIL | 0 | ncnst
|
||||
OUT: | Natural | 0 | unn
|
||||
OUT: | NegInteger | 0 | unn
|
||||
OUT: | PosInteger | 0 | unn
|
||||
OUT: | Real | 0 | unn
|
||||
OUT: | String | 0 | unn
|
||||
OUT: | TRUE | 0 | ncnst
|
||||
OUT: | Things | 0 | unn
|
||||
OUT: A1' | Any | 0 | unn
|
||||
OUT: A1' | Constant | 0 | unn
|
||||
OUT: A1' | Data | 0 | unn
|
||||
OUT: A1' | conforms | 0 | dcnst
|
||||
OUT: A1' | notFunctional | 0 | dcnst
|
||||
OUT: A1' | notInjective | 0 | dcnst
|
||||
OUT: A1' | notInvTotal | 0 | dcnst
|
||||
OUT: A1' | notRelational | 0 | dcnst
|
||||
OUT: A1' | notTotal | 0 | dcnst
|
||||
OUT:
|
||||
OUT: Type constants: #Boolean #Cons #Cons[0] #Cons[1] #Integer #List #Natural #NegInteger #PosInteger #Real #String #Things A1'.#Any A1'.#Constant A1'.#Data
|
||||
OUT: Symbolic constants:
|
||||
OUT: Rationals:
|
||||
OUT: Strings:
|
||||
OUT: Variables:
|
||||
OUT:
|
||||
OUT: []> typ A1'
|
||||
OUT:
|
||||
OUT: []> dt T1
|
||||
OUT: Reduced form
|
||||
OUT: transform T1 (in1:: A1, in2:: A1)
|
||||
OUT: returns (out:: A1')
|
||||
OUT: {
|
||||
OUT: Triple ::= (in1.Cons + { NIL }, in2.Cons + { NIL }, out.Cons + { NIL }).
|
||||
OUT: Things ::= Triple + in1.Things + in2.Things + out.Things.
|
||||
OUT:
|
||||
OUT: out.Cons(x, y)
|
||||
OUT: :-
|
||||
OUT: in1.Cons(x, y).
|
||||
OUT:
|
||||
OUT: Triple(c, c, c)
|
||||
OUT: :-
|
||||
OUT: c is in1.Cons.
|
||||
OUT:
|
||||
OUT: _(x)
|
||||
OUT: :-
|
||||
OUT: x is Things.
|
||||
OUT:
|
||||
OUT: out._(x)
|
||||
OUT: :-
|
||||
OUT: x is in1.Cons.
|
||||
OUT:
|
||||
OUT: out.Cons(1, in1.Cons(1, NIL)).
|
||||
OUT:
|
||||
OUT: out.Cons(1, out.Cons(1, NIL)).
|
||||
OUT: }
|
||||
OUT:
|
||||
OUT: Symbol table
|
||||
OUT: Space | Name | Arity | Kind
|
||||
OUT: ---------|---------------|-------|-------
|
||||
OUT: | Boolean | 0 | unn
|
||||
OUT: | FALSE | 0 | ncnst
|
||||
OUT: | Integer | 0 | unn
|
||||
OUT: | NIL | 0 | ncnst
|
||||
OUT: | Natural | 0 | unn
|
||||
OUT: | NegInteger | 0 | unn
|
||||
OUT: | PosInteger | 0 | unn
|
||||
OUT: | Real | 0 | unn
|
||||
OUT: | String | 0 | unn
|
||||
OUT: | TRUE | 0 | ncnst
|
||||
OUT: | Things | 0 | unn
|
||||
OUT: | Triple | 3 | con
|
||||
OUT: | ~scValue | 2 | con
|
||||
OUT: T1 | Any | 0 | unn
|
||||
OUT: T1 | Constant | 0 | unn
|
||||
OUT: T1 | Data | 0 | unn
|
||||
OUT: T1 | ensures | 0 | dcnst
|
||||
OUT: T1 | requires | 0 | dcnst
|
||||
OUT: in1 | Any | 0 | unn
|
||||
OUT: in1 | Boolean | 0 | unn
|
||||
OUT: in1 | Cons | 2 | con
|
||||
OUT: in1 | Constant | 0 | unn
|
||||
OUT: in1 | Data | 0 | unn
|
||||
OUT: in1 | Integer | 0 | unn
|
||||
OUT: in1 | Natural | 0 | unn
|
||||
OUT: in1 | NegInteger | 0 | unn
|
||||
OUT: in1 | PosInteger | 0 | unn
|
||||
OUT: in1 | Real | 0 | unn
|
||||
OUT: in1 | String | 0 | unn
|
||||
OUT: in1 | Things | 0 | unn
|
||||
OUT: in1.A1 | Any | 0 | unn
|
||||
OUT: in1.A1 | Constant | 0 | unn
|
||||
OUT: in1.A1 | Data | 0 | unn
|
||||
OUT: in1.A1 | conforms | 0 | dcnst
|
||||
OUT: in1.A1 | notFunctional | 0 | dcnst
|
||||
OUT: in1.A1 | notInjective | 0 | dcnst
|
||||
OUT: in1.A1 | notInvTotal | 0 | dcnst
|
||||
OUT: in1.A1 | notRelational | 0 | dcnst
|
||||
OUT: in1.A1 | notTotal | 0 | dcnst
|
||||
OUT: in2 | Any | 0 | unn
|
||||
OUT: in2 | Boolean | 0 | unn
|
||||
OUT: in2 | Cons | 2 | con
|
||||
OUT: in2 | Constant | 0 | unn
|
||||
OUT: in2 | Data | 0 | unn
|
||||
OUT: in2 | Integer | 0 | unn
|
||||
OUT: in2 | Natural | 0 | unn
|
||||
OUT: in2 | NegInteger | 0 | unn
|
||||
OUT: in2 | PosInteger | 0 | unn
|
||||
OUT: in2 | Real | 0 | unn
|
||||
OUT: in2 | String | 0 | unn
|
||||
OUT: in2 | Things | 0 | unn
|
||||
OUT: in2.A1 | Any | 0 | unn
|
||||
OUT: in2.A1 | Constant | 0 | unn
|
||||
OUT: in2.A1 | Data | 0 | unn
|
||||
OUT: in2.A1 | conforms | 0 | dcnst
|
||||
OUT: in2.A1 | notFunctional | 0 | dcnst
|
||||
OUT: in2.A1 | notInjective | 0 | dcnst
|
||||
OUT: in2.A1 | notInvTotal | 0 | dcnst
|
||||
OUT: in2.A1 | notRelational | 0 | dcnst
|
||||
OUT: in2.A1 | notTotal | 0 | dcnst
|
||||
OUT: out | Any | 0 | unn
|
||||
OUT: out | Boolean | 0 | unn
|
||||
OUT: out | Cons | 2 | con
|
||||
OUT: out | Constant | 0 | unn
|
||||
OUT: out | Data | 0 | unn
|
||||
OUT: out | Integer | 0 | unn
|
||||
OUT: out | List | 0 | unn
|
||||
OUT: out | Natural | 0 | unn
|
||||
OUT: out | NegInteger | 0 | unn
|
||||
OUT: out | PosInteger | 0 | unn
|
||||
OUT: out | Real | 0 | unn
|
||||
OUT: out | String | 0 | unn
|
||||
OUT: out | Things | 0 | unn
|
||||
OUT: out.A1' | Any | 0 | unn
|
||||
OUT: out.A1' | Constant | 0 | unn
|
||||
OUT: out.A1' | Data | 0 | unn
|
||||
OUT: out.A1' | conforms | 0 | dcnst
|
||||
OUT: out.A1' | notFunctional | 0 | dcnst
|
||||
OUT: out.A1' | notInjective | 0 | dcnst
|
||||
OUT: out.A1' | notInvTotal | 0 | dcnst
|
||||
OUT: out.A1' | notRelational | 0 | dcnst
|
||||
OUT: out.A1' | notTotal | 0 | dcnst
|
||||
OUT:
|
||||
OUT: Type constants: #Boolean #Integer #Natural #NegInteger #PosInteger #Real #String #Things #Triple #Triple[0] #Triple[1] #Triple[2] T1.#Any T1.#Constant T1.#Data in1.#Any in1.#Boolean in1.#Cons in1.#Cons[0] in1.#Cons[1] in1.#Constant in1.#Data in1.#Integer in1.#Natural in1.#NegInteger in1.#PosInteger in1.#Real in1.#String in1.#Things in1.A1.#Any in1.A1.#Constant in1.A1.#Data in2.#Any in2.#Boolean in2.#Cons in2.#Cons[0] in2.#Cons[1] in2.#Constant in2.#Data in2.#Integer in2.#Natural in2.#NegInteger in2.#PosInteger in2.#Real in2.#String in2.#Things in2.A1.#Any in2.A1.#Constant in2.A1.#Data out.#Any out.#Boolean out.#Cons out.#Cons[0] out.#Cons[1] out.#Constant out.#Data out.#Integer out.#List out.#Natural out.#NegInteger out.#PosInteger out.#Real out.#String out.#Things out.A1'.#Any out.A1'.#Constant out.A1'.#Data
|
||||
OUT: Symbolic constants:
|
||||
OUT: Rationals: 1
|
||||
OUT: Strings:
|
||||
OUT: Variables: c x y
|
||||
OUT:
|
||||
OUT: []> typ T1
|
||||
OUT: + Type environment at (23, 4)
|
||||
OUT: x: Integer
|
||||
OUT: y: {NIL} + in1.Cons
|
||||
OUT: ~dc0: in1.Cons
|
||||
OUT: Coerced arg 2 of (23, 4): in1 --> out
|
||||
OUT: + Type environment at (23, 22)
|
||||
OUT: x: Integer
|
||||
OUT: y: {NIL} + in1.Cons
|
||||
OUT: ~dc0: in1.Cons
|
||||
OUT: + Type environment at (26, 4)
|
||||
OUT: c: in1.Cons
|
||||
OUT: Coerced arg 2 of (26, 4): in1 --> in2
|
||||
OUT: Coerced arg 3 of (26, 4): in1 --> out
|
||||
OUT: + Type environment at (26, 23)
|
||||
OUT: c: in1.Cons
|
||||
OUT: + Type environment at (29, 4)
|
||||
OUT: x: Triple + out.Cons + in2.Cons + in1.Cons
|
||||
OUT: + Type environment at (29, 12)
|
||||
OUT: x: Triple + out.Cons + in2.Cons + in1.Cons
|
||||
OUT: + Type environment at (32, 4)
|
||||
OUT: x: in1.Cons
|
||||
OUT: Coerced arg 1 of (32, 4): in1 --> out
|
||||
OUT: + Type environment at (32, 16)
|
||||
OUT: x: in1.Cons
|
||||
OUT: + Type environment at (35, 4)
|
||||
OUT: Coerced arg 2 of (35, 4): in1 --> out
|
||||
OUT: + Type environment at (35, 4)
|
||||
OUT: + Type environment at (38, 4)
|
||||
OUT: + Type environment at (38, 4)
|
||||
OUT:
|
||||
OUT: []> dt B
|
||||
OUT: Reduced form
|
||||
OUT: domain B includes X:: A1', A1'
|
||||
OUT: {
|
||||
OUT:
|
||||
OUT: Cons(1, x)
|
||||
OUT: :-
|
||||
OUT: x is X.Cons.
|
||||
OUT:
|
||||
OUT: X.Cons(1, x)
|
||||
OUT: :-
|
||||
OUT: x is Cons.
|
||||
OUT: }
|
||||
OUT:
|
||||
OUT: Symbol table
|
||||
OUT: Space | Name | Arity | Kind
|
||||
OUT: -------|---------------|-------|-------
|
||||
OUT: | Boolean | 0 | unn
|
||||
OUT: | Cons | 2 | con
|
||||
OUT: | FALSE | 0 | ncnst
|
||||
OUT: | Integer | 0 | unn
|
||||
OUT: | List | 0 | unn
|
||||
OUT: | NIL | 0 | ncnst
|
||||
OUT: | Natural | 0 | unn
|
||||
OUT: | NegInteger | 0 | unn
|
||||
OUT: | PosInteger | 0 | unn
|
||||
OUT: | Real | 0 | unn
|
||||
OUT: | String | 0 | unn
|
||||
OUT: | TRUE | 0 | ncnst
|
||||
OUT: | Things | 0 | unn
|
||||
OUT: A1' | Any | 0 | unn
|
||||
OUT: A1' | Constant | 0 | unn
|
||||
OUT: A1' | Data | 0 | unn
|
||||
OUT: A1' | conforms | 0 | dcnst
|
||||
OUT: A1' | notFunctional | 0 | dcnst
|
||||
OUT: A1' | notInjective | 0 | dcnst
|
||||
OUT: A1' | notInvTotal | 0 | dcnst
|
||||
OUT: A1' | notRelational | 0 | dcnst
|
||||
OUT: A1' | notTotal | 0 | dcnst
|
||||
OUT: B | Any | 0 | unn
|
||||
OUT: B | Constant | 0 | unn
|
||||
OUT: B | Data | 0 | unn
|
||||
OUT: B | conforms | 0 | dcnst
|
||||
OUT: B | notFunctional | 0 | dcnst
|
||||
OUT: B | notInjective | 0 | dcnst
|
||||
OUT: B | notInvTotal | 0 | dcnst
|
||||
OUT: B | notRelational | 0 | dcnst
|
||||
OUT: B | notTotal | 0 | dcnst
|
||||
OUT: X | Any | 0 | unn
|
||||
OUT: X | Boolean | 0 | unn
|
||||
OUT: X | Cons | 2 | con
|
||||
OUT: X | Constant | 0 | unn
|
||||
OUT: X | Data | 0 | unn
|
||||
OUT: X | Integer | 0 | unn
|
||||
OUT: X | List | 0 | unn
|
||||
OUT: X | Natural | 0 | unn
|
||||
OUT: X | NegInteger | 0 | unn
|
||||
OUT: X | PosInteger | 0 | unn
|
||||
OUT: X | Real | 0 | unn
|
||||
OUT: X | String | 0 | unn
|
||||
OUT: X | Things | 0 | unn
|
||||
OUT: X.A1' | Any | 0 | unn
|
||||
OUT: X.A1' | Constant | 0 | unn
|
||||
OUT: X.A1' | Data | 0 | unn
|
||||
OUT: X.A1' | conforms | 0 | dcnst
|
||||
OUT: X.A1' | notFunctional | 0 | dcnst
|
||||
OUT: X.A1' | notInjective | 0 | dcnst
|
||||
OUT: X.A1' | notInvTotal | 0 | dcnst
|
||||
OUT: X.A1' | notRelational | 0 | dcnst
|
||||
OUT: X.A1' | notTotal | 0 | dcnst
|
||||
OUT:
|
||||
OUT: Type constants: #Boolean #Cons #Cons[0] #Cons[1] #Integer #List #Natural #NegInteger #PosInteger #Real #String #Things A1'.#Any A1'.#Constant A1'.#Data B.#Any B.#Constant B.#Data X.#Any X.#Boolean X.#Cons X.#Cons[0] X.#Cons[1] X.#Constant X.#Data X.#Integer X.#List X.#Natural X.#NegInteger X.#PosInteger X.#Real X.#String X.#Things X.A1'.#Any X.A1'.#Constant X.A1'.#Data
|
||||
OUT: Symbolic constants:
|
||||
OUT: Rationals: 1
|
||||
OUT: Strings:
|
||||
OUT: Variables: x
|
||||
OUT:
|
||||
OUT: []> typ B
|
||||
OUT: + Type environment at (54, 4)
|
||||
OUT: x: X.Cons
|
||||
OUT: Coerced arg 2 of (54, 4): X -->
|
||||
OUT: + Type environment at (54, 18)
|
||||
OUT: x: X.Cons
|
||||
OUT: + Type environment at (57, 4)
|
||||
OUT: x: Cons
|
||||
OUT: Coerced arg 2 of (57, 4): --> X
|
||||
OUT: + Type environment at (57, 20)
|
||||
OUT: x: Cons
|
||||
OUT:
|
||||
OUT: []> dt C
|
||||
OUT: Reduced form
|
||||
OUT: domain C includes Y:: B, A1'
|
||||
OUT: {
|
||||
OUT:
|
||||
OUT: Cons(1, x)
|
||||
OUT: :-
|
||||
OUT: x is X.Cons.
|
||||
OUT:
|
||||
OUT: X.Cons(1, x)
|
||||
OUT: :-
|
||||
OUT: x is Cons.
|
||||
OUT:
|
||||
OUT: Y.Cons(1, x)
|
||||
OUT: :-
|
||||
OUT: x is X.Cons.
|
||||
OUT:
|
||||
OUT: X.Cons(1, x)
|
||||
OUT: :-
|
||||
OUT: x is Y.Cons.
|
||||
OUT: }
|
||||
OUT:
|
||||
OUT: Symbol table
|
||||
OUT: Space | Name | Arity | Kind
|
||||
OUT: ---------|---------------|-------|-------
|
||||
OUT: | Boolean | 0 | unn
|
||||
OUT: | Cons | 2 | con
|
||||
OUT: | FALSE | 0 | ncnst
|
||||
OUT: | Integer | 0 | unn
|
||||
OUT: | List | 0 | unn
|
||||
OUT: | NIL | 0 | ncnst
|
||||
OUT: | Natural | 0 | unn
|
||||
OUT: | NegInteger | 0 | unn
|
||||
OUT: | PosInteger | 0 | unn
|
||||
OUT: | Real | 0 | unn
|
||||
OUT: | String | 0 | unn
|
||||
OUT: | TRUE | 0 | ncnst
|
||||
OUT: | Things | 0 | unn
|
||||
OUT: A1' | Any | 0 | unn
|
||||
OUT: A1' | Constant | 0 | unn
|
||||
OUT: A1' | Data | 0 | unn
|
||||
OUT: A1' | conforms | 0 | dcnst
|
||||
OUT: A1' | notFunctional | 0 | dcnst
|
||||
OUT: A1' | notInjective | 0 | dcnst
|
||||
OUT: A1' | notInvTotal | 0 | dcnst
|
||||
OUT: A1' | notRelational | 0 | dcnst
|
||||
OUT: A1' | notTotal | 0 | dcnst
|
||||
OUT: C | Any | 0 | unn
|
||||
OUT: C | Constant | 0 | unn
|
||||
OUT: C | Data | 0 | unn
|
||||
OUT: C | conforms | 0 | dcnst
|
||||
OUT: C | notFunctional | 0 | dcnst
|
||||
OUT: C | notInjective | 0 | dcnst
|
||||
OUT: C | notInvTotal | 0 | dcnst
|
||||
OUT: C | notRelational | 0 | dcnst
|
||||
OUT: C | notTotal | 0 | dcnst
|
||||
OUT: Y | Any | 0 | unn
|
||||
OUT: Y | Boolean | 0 | unn
|
||||
OUT: Y | Cons | 2 | con
|
||||
OUT: Y | Constant | 0 | unn
|
||||
OUT: Y | Data | 0 | unn
|
||||
OUT: Y | Integer | 0 | unn
|
||||
OUT: Y | List | 0 | unn
|
||||
OUT: Y | Natural | 0 | unn
|
||||
OUT: Y | NegInteger | 0 | unn
|
||||
OUT: Y | PosInteger | 0 | unn
|
||||
OUT: Y | Real | 0 | unn
|
||||
OUT: Y | String | 0 | unn
|
||||
OUT: Y | Things | 0 | unn
|
||||
OUT: Y.A1' | Any | 0 | unn
|
||||
OUT: Y.A1' | Constant | 0 | unn
|
||||
OUT: Y.A1' | Data | 0 | unn
|
||||
OUT: Y.A1' | conforms | 0 | dcnst
|
||||
OUT: Y.A1' | notFunctional | 0 | dcnst
|
||||
OUT: Y.A1' | notInjective | 0 | dcnst
|
||||
OUT: Y.A1' | notInvTotal | 0 | dcnst
|
||||
OUT: Y.A1' | notRelational | 0 | dcnst
|
||||
OUT: Y.A1' | notTotal | 0 | dcnst
|
||||
OUT: Y.B | Any | 0 | unn
|
||||
OUT: Y.B | Constant | 0 | unn
|
||||
OUT: Y.B | Data | 0 | unn
|
||||
OUT: Y.B | conforms | 0 | dcnst
|
||||
OUT: Y.B | notFunctional | 0 | dcnst
|
||||
OUT: Y.B | notInjective | 0 | dcnst
|
||||
OUT: Y.B | notInvTotal | 0 | dcnst
|
||||
OUT: Y.B | notRelational | 0 | dcnst
|
||||
OUT: Y.B | notTotal | 0 | dcnst
|
||||
OUT: Y.X | Any | 0 | unn
|
||||
OUT: Y.X | Boolean | 0 | unn
|
||||
OUT: Y.X | Cons | 2 | con
|
||||
OUT: Y.X | Constant | 0 | unn
|
||||
OUT: Y.X | Data | 0 | unn
|
||||
OUT: Y.X | Integer | 0 | unn
|
||||
OUT: Y.X | List | 0 | unn
|
||||
OUT: Y.X | Natural | 0 | unn
|
||||
OUT: Y.X | NegInteger | 0 | unn
|
||||
OUT: Y.X | PosInteger | 0 | unn
|
||||
OUT: Y.X | Real | 0 | unn
|
||||
OUT: Y.X | String | 0 | unn
|
||||
OUT: Y.X | Things | 0 | unn
|
||||
OUT: Y.X.A1' | Any | 0 | unn
|
||||
OUT: Y.X.A1' | Constant | 0 | unn
|
||||
OUT: Y.X.A1' | Data | 0 | unn
|
||||
OUT: Y.X.A1' | conforms | 0 | dcnst
|
||||
OUT: Y.X.A1' | notFunctional | 0 | dcnst
|
||||
OUT: Y.X.A1' | notInjective | 0 | dcnst
|
||||
OUT: Y.X.A1' | notInvTotal | 0 | dcnst
|
||||
OUT: Y.X.A1' | notRelational | 0 | dcnst
|
||||
OUT: Y.X.A1' | notTotal | 0 | dcnst
|
||||
OUT:
|
||||
OUT: Type constants: #Boolean #Cons #Cons[0] #Cons[1] #Integer #List #Natural #NegInteger #PosInteger #Real #String #Things A1'.#Any A1'.#Constant A1'.#Data C.#Any C.#Constant C.#Data Y.#Any Y.#Boolean Y.#Cons Y.#Cons[0] Y.#Cons[1] Y.#Constant Y.#Data Y.#Integer Y.#List Y.#Natural Y.#NegInteger Y.#PosInteger Y.#Real Y.#String Y.#Things Y.A1'.#Any Y.A1'.#Constant Y.A1'.#Data Y.B.#Any Y.B.#Constant Y.B.#Data Y.X.#Any Y.X.#Boolean Y.X.#Cons Y.X.#Cons[0] Y.X.#Cons[1] Y.X.#Constant Y.X.#Data Y.X.#Integer Y.X.#List Y.X.#Natural Y.X.#NegInteger Y.X.#PosInteger Y.X.#Real Y.X.#String Y.X.#Things Y.X.A1'.#Any Y.X.A1'.#Constant Y.X.A1'.#Data
|
||||
OUT: Symbolic constants:
|
||||
OUT: Rationals: 1
|
||||
OUT: Strings:
|
||||
OUT: Variables: x
|
||||
OUT:
|
||||
OUT: []> typ C
|
||||
OUT: + Type environment at (63, 4)
|
||||
OUT: x: Y.X.Cons
|
||||
OUT: Coerced arg 2 of (63, 4): Y.X -->
|
||||
OUT: + Type environment at (63, 18)
|
||||
OUT: x: Y.X.Cons
|
||||
OUT: + Type environment at (66, 4)
|
||||
OUT: x: Cons
|
||||
OUT: Coerced arg 2 of (66, 4): --> Y.X
|
||||
OUT: + Type environment at (66, 20)
|
||||
OUT: x: Cons
|
||||
OUT: + Type environment at (69, 4)
|
||||
OUT: x: Y.X.Cons
|
||||
OUT: Coerced arg 2 of (69, 4): Y.X --> Y
|
||||
OUT: + Type environment at (69, 20)
|
||||
OUT: x: Y.X.Cons
|
||||
OUT: + Type environment at (72, 4)
|
||||
OUT: x: Y.Cons
|
||||
OUT: Coerced arg 2 of (72, 4): Y --> Y.X
|
||||
OUT: + Type environment at (72, 20)
|
||||
OUT: x: Y.Cons
|
||||
OUT:
|
||||
OUT: []> dt T2
|
||||
OUT: Reduced form
|
||||
OUT: transform T2 (in1:: A1, in2:: A1)
|
||||
OUT: returns (out:: B)
|
||||
OUT: {
|
||||
OUT:
|
||||
OUT: out.X._(x)
|
||||
OUT: :-
|
||||
OUT: x is in1.Cons.
|
||||
OUT:
|
||||
OUT: out.Cons(1, x)
|
||||
OUT: :-
|
||||
OUT: x is in1.Cons.
|
||||
OUT: }
|
||||
OUT:
|
||||
OUT: Symbol table
|
||||
OUT: Space | Name | Arity | Kind
|
||||
OUT: -----------|---------------|-------|-------
|
||||
OUT: | Boolean | 0 | unn
|
||||
OUT: | FALSE | 0 | ncnst
|
||||
OUT: | Integer | 0 | unn
|
||||
OUT: | NIL | 0 | ncnst
|
||||
OUT: | Natural | 0 | unn
|
||||
OUT: | NegInteger | 0 | unn
|
||||
OUT: | PosInteger | 0 | unn
|
||||
OUT: | Real | 0 | unn
|
||||
OUT: | String | 0 | unn
|
||||
OUT: | TRUE | 0 | ncnst
|
||||
OUT: | ~scValue | 2 | con
|
||||
OUT: T2 | Any | 0 | unn
|
||||
OUT: T2 | Constant | 0 | unn
|
||||
OUT: T2 | Data | 0 | unn
|
||||
OUT: T2 | ensures | 0 | dcnst
|
||||
OUT: T2 | requires | 0 | dcnst
|
||||
OUT: in1 | Any | 0 | unn
|
||||
OUT: in1 | Boolean | 0 | unn
|
||||
OUT: in1 | Cons | 2 | con
|
||||
OUT: in1 | Constant | 0 | unn
|
||||
OUT: in1 | Data | 0 | unn
|
||||
OUT: in1 | Integer | 0 | unn
|
||||
OUT: in1 | Natural | 0 | unn
|
||||
OUT: in1 | NegInteger | 0 | unn
|
||||
OUT: in1 | PosInteger | 0 | unn
|
||||
OUT: in1 | Real | 0 | unn
|
||||
OUT: in1 | String | 0 | unn
|
||||
OUT: in1 | Things | 0 | unn
|
||||
OUT: in1.A1 | Any | 0 | unn
|
||||
OUT: in1.A1 | Constant | 0 | unn
|
||||
OUT: in1.A1 | Data | 0 | unn
|
||||
OUT: in1.A1 | conforms | 0 | dcnst
|
||||
OUT: in1.A1 | notFunctional | 0 | dcnst
|
||||
OUT: in1.A1 | notInjective | 0 | dcnst
|
||||
OUT: in1.A1 | notInvTotal | 0 | dcnst
|
||||
OUT: in1.A1 | notRelational | 0 | dcnst
|
||||
OUT: in1.A1 | notTotal | 0 | dcnst
|
||||
OUT: in2 | Any | 0 | unn
|
||||
OUT: in2 | Boolean | 0 | unn
|
||||
OUT: in2 | Cons | 2 | con
|
||||
OUT: in2 | Constant | 0 | unn
|
||||
OUT: in2 | Data | 0 | unn
|
||||
OUT: in2 | Integer | 0 | unn
|
||||
OUT: in2 | Natural | 0 | unn
|
||||
OUT: in2 | NegInteger | 0 | unn
|
||||
OUT: in2 | PosInteger | 0 | unn
|
||||
OUT: in2 | Real | 0 | unn
|
||||
OUT: in2 | String | 0 | unn
|
||||
OUT: in2 | Things | 0 | unn
|
||||
OUT: in2.A1 | Any | 0 | unn
|
||||
OUT: in2.A1 | Constant | 0 | unn
|
||||
OUT: in2.A1 | Data | 0 | unn
|
||||
OUT: in2.A1 | conforms | 0 | dcnst
|
||||
OUT: in2.A1 | notFunctional | 0 | dcnst
|
||||
OUT: in2.A1 | notInjective | 0 | dcnst
|
||||
OUT: in2.A1 | notInvTotal | 0 | dcnst
|
||||
OUT: in2.A1 | notRelational | 0 | dcnst
|
||||
OUT: in2.A1 | notTotal | 0 | dcnst
|
||||
OUT: out | Any | 0 | unn
|
||||
OUT: out | Boolean | 0 | unn
|
||||
OUT: out | Cons | 2 | con
|
||||
OUT: out | Constant | 0 | unn
|
||||
OUT: out | Data | 0 | unn
|
||||
OUT: out | Integer | 0 | unn
|
||||
OUT: out | List | 0 | unn
|
||||
OUT: out | Natural | 0 | unn
|
||||
OUT: out | NegInteger | 0 | unn
|
||||
OUT: out | PosInteger | 0 | unn
|
||||
OUT: out | Real | 0 | unn
|
||||
OUT: out | String | 0 | unn
|
||||
OUT: out | Things | 0 | unn
|
||||
OUT: out.A1' | Any | 0 | unn
|
||||
OUT: out.A1' | Constant | 0 | unn
|
||||
OUT: out.A1' | Data | 0 | unn
|
||||
OUT: out.A1' | conforms | 0 | dcnst
|
||||
OUT: out.A1' | notFunctional | 0 | dcnst
|
||||
OUT: out.A1' | notInjective | 0 | dcnst
|
||||
OUT: out.A1' | notInvTotal | 0 | dcnst
|
||||
OUT: out.A1' | notRelational | 0 | dcnst
|
||||
OUT: out.A1' | notTotal | 0 | dcnst
|
||||
OUT: out.B | Any | 0 | unn
|
||||
OUT: out.B | Constant | 0 | unn
|
||||
OUT: out.B | Data | 0 | unn
|
||||
OUT: out.B | conforms | 0 | dcnst
|
||||
OUT: out.B | notFunctional | 0 | dcnst
|
||||
OUT: out.B | notInjective | 0 | dcnst
|
||||
OUT: out.B | notInvTotal | 0 | dcnst
|
||||
OUT: out.B | notRelational | 0 | dcnst
|
||||
OUT: out.B | notTotal | 0 | dcnst
|
||||
OUT: out.X | Any | 0 | unn
|
||||
OUT: out.X | Boolean | 0 | unn
|
||||
OUT: out.X | Cons | 2 | con
|
||||
OUT: out.X | Constant | 0 | unn
|
||||
OUT: out.X | Data | 0 | unn
|
||||
OUT: out.X | Integer | 0 | unn
|
||||
OUT: out.X | List | 0 | unn
|
||||
OUT: out.X | Natural | 0 | unn
|
||||
OUT: out.X | NegInteger | 0 | unn
|
||||
OUT: out.X | PosInteger | 0 | unn
|
||||
OUT: out.X | Real | 0 | unn
|
||||
OUT: out.X | String | 0 | unn
|
||||
OUT: out.X | Things | 0 | unn
|
||||
OUT: out.X.A1' | Any | 0 | unn
|
||||
OUT: out.X.A1' | Constant | 0 | unn
|
||||
OUT: out.X.A1' | Data | 0 | unn
|
||||
OUT: out.X.A1' | conforms | 0 | dcnst
|
||||
OUT: out.X.A1' | notFunctional | 0 | dcnst
|
||||
OUT: out.X.A1' | notInjective | 0 | dcnst
|
||||
OUT: out.X.A1' | notInvTotal | 0 | dcnst
|
||||
OUT: out.X.A1' | notRelational | 0 | dcnst
|
||||
OUT: out.X.A1' | notTotal | 0 | dcnst
|
||||
OUT:
|
||||
OUT: Type constants: #Boolean #Integer #Natural #NegInteger #PosInteger #Real #String T2.#Any T2.#Constant T2.#Data in1.#Any in1.#Boolean in1.#Cons in1.#Cons[0] in1.#Cons[1] in1.#Constant in1.#Data in1.#Integer in1.#Natural in1.#NegInteger in1.#PosInteger in1.#Real in1.#String in1.#Things in1.A1.#Any in1.A1.#Constant in1.A1.#Data in2.#Any in2.#Boolean in2.#Cons in2.#Cons[0] in2.#Cons[1] in2.#Constant in2.#Data in2.#Integer in2.#Natural in2.#NegInteger in2.#PosInteger in2.#Real in2.#String in2.#Things in2.A1.#Any in2.A1.#Constant in2.A1.#Data out.#Any out.#Boolean out.#Cons out.#Cons[0] out.#Cons[1] out.#Constant out.#Data out.#Integer out.#List out.#Natural out.#NegInteger out.#PosInteger out.#Real out.#String out.#Things out.A1'.#Any out.A1'.#Constant out.A1'.#Data out.B.#Any out.B.#Constant out.B.#Data out.X.#Any out.X.#Boolean out.X.#Cons out.X.#Cons[0] out.X.#Cons[1] out.X.#Constant out.X.#Data out.X.#Integer out.X.#List out.X.#Natural out.X.#NegInteger out.X.#PosInteger out.X.#Real out.X.#String out.X.#Things out.X.A1'.#Any out.X.A1'.#Constant out.X.A1'.#Data
|
||||
OUT: Symbolic constants:
|
||||
OUT: Rationals: 1
|
||||
OUT: Strings:
|
||||
OUT: Variables: x
|
||||
OUT:
|
||||
OUT: []> typ T2
|
||||
OUT: + Type environment at (78, 4)
|
||||
OUT: x: in1.Cons
|
||||
OUT: Coerced arg 1 of (78, 4): in1 --> out.X
|
||||
OUT: + Type environment at (78, 18)
|
||||
OUT: x: in1.Cons
|
||||
OUT: + Type environment at (81, 4)
|
||||
OUT: x: in1.Cons
|
||||
OUT: Coerced arg 2 of (81, 4): in1 --> out
|
||||
OUT: + Type environment at (81, 22)
|
||||
OUT: x: in1.Cons
|
||||
OUT:
|
||||
OUT: []> dt D
|
||||
OUT: Reduced form
|
||||
OUT: domain D includes Y:: B, X:: A1', A1'
|
||||
OUT: {
|
||||
OUT: Type1 ::= Y.X.Cons + Y.Cons.
|
||||
OUT: Type2 ::= Cons + X.Cons.
|
||||
OUT: F ::= (Type2).
|
||||
OUT: F' ::= (Type1).
|
||||
OUT:
|
||||
OUT: F(x)
|
||||
OUT: :-
|
||||
OUT: x is Type1.
|
||||
OUT:
|
||||
OUT: F'(x)
|
||||
OUT: :-
|
||||
OUT: x is Type2.
|
||||
OUT: }
|
||||
OUT:
|
||||
OUT: Symbol table
|
||||
OUT: Space | Name | Arity | Kind
|
||||
OUT: ---------|---------------|-------|-------
|
||||
OUT: | Boolean | 0 | unn
|
||||
OUT: | Cons | 2 | con
|
||||
OUT: | F | 1 | con
|
||||
OUT: | F' | 1 | con
|
||||
OUT: | FALSE | 0 | ncnst
|
||||
OUT: | Integer | 0 | unn
|
||||
OUT: | List | 0 | unn
|
||||
OUT: | NIL | 0 | ncnst
|
||||
OUT: | Natural | 0 | unn
|
||||
OUT: | NegInteger | 0 | unn
|
||||
OUT: | PosInteger | 0 | unn
|
||||
OUT: | Real | 0 | unn
|
||||
OUT: | String | 0 | unn
|
||||
OUT: | TRUE | 0 | ncnst
|
||||
OUT: | Things | 0 | unn
|
||||
OUT: | Type1 | 0 | unn
|
||||
OUT: | Type2 | 0 | unn
|
||||
OUT: A1' | Any | 0 | unn
|
||||
OUT: A1' | Constant | 0 | unn
|
||||
OUT: A1' | Data | 0 | unn
|
||||
OUT: A1' | conforms | 0 | dcnst
|
||||
OUT: A1' | notFunctional | 0 | dcnst
|
||||
OUT: A1' | notInjective | 0 | dcnst
|
||||
OUT: A1' | notInvTotal | 0 | dcnst
|
||||
OUT: A1' | notRelational | 0 | dcnst
|
||||
OUT: A1' | notTotal | 0 | dcnst
|
||||
OUT: D | Any | 0 | unn
|
||||
OUT: D | Constant | 0 | unn
|
||||
OUT: D | Data | 0 | unn
|
||||
OUT: D | conforms | 0 | dcnst
|
||||
OUT: D | notFunctional | 0 | dcnst
|
||||
OUT: D | notInjective | 0 | dcnst
|
||||
OUT: D | notInvTotal | 0 | dcnst
|
||||
OUT: D | notRelational | 0 | dcnst
|
||||
OUT: D | notTotal | 0 | dcnst
|
||||
OUT: X | Any | 0 | unn
|
||||
OUT: X | Boolean | 0 | unn
|
||||
OUT: X | Cons | 2 | con
|
||||
OUT: X | Constant | 0 | unn
|
||||
OUT: X | Data | 0 | unn
|
||||
OUT: X | Integer | 0 | unn
|
||||
OUT: X | List | 0 | unn
|
||||
OUT: X | Natural | 0 | unn
|
||||
OUT: X | NegInteger | 0 | unn
|
||||
OUT: X | PosInteger | 0 | unn
|
||||
OUT: X | Real | 0 | unn
|
||||
OUT: X | String | 0 | unn
|
||||
OUT: X | Things | 0 | unn
|
||||
OUT: X.A1' | Any | 0 | unn
|
||||
OUT: X.A1' | Constant | 0 | unn
|
||||
OUT: X.A1' | Data | 0 | unn
|
||||
OUT: X.A1' | conforms | 0 | dcnst
|
||||
OUT: X.A1' | notFunctional | 0 | dcnst
|
||||
OUT: X.A1' | notInjective | 0 | dcnst
|
||||
OUT: X.A1' | notInvTotal | 0 | dcnst
|
||||
OUT: X.A1' | notRelational | 0 | dcnst
|
||||
OUT: X.A1' | notTotal | 0 | dcnst
|
||||
OUT: Y | Any | 0 | unn
|
||||
OUT: Y | Boolean | 0 | unn
|
||||
OUT: Y | Cons | 2 | con
|
||||
OUT: Y | Constant | 0 | unn
|
||||
OUT: Y | Data | 0 | unn
|
||||
OUT: Y | Integer | 0 | unn
|
||||
OUT: Y | List | 0 | unn
|
||||
OUT: Y | Natural | 0 | unn
|
||||
OUT: Y | NegInteger | 0 | unn
|
||||
OUT: Y | PosInteger | 0 | unn
|
||||
OUT: Y | Real | 0 | unn
|
||||
OUT: Y | String | 0 | unn
|
||||
OUT: Y | Things | 0 | unn
|
||||
OUT: Y.A1' | Any | 0 | unn
|
||||
OUT: Y.A1' | Constant | 0 | unn
|
||||
OUT: Y.A1' | Data | 0 | unn
|
||||
OUT: Y.A1' | conforms | 0 | dcnst
|
||||
OUT: Y.A1' | notFunctional | 0 | dcnst
|
||||
OUT: Y.A1' | notInjective | 0 | dcnst
|
||||
OUT: Y.A1' | notInvTotal | 0 | dcnst
|
||||
OUT: Y.A1' | notRelational | 0 | dcnst
|
||||
OUT: Y.A1' | notTotal | 0 | dcnst
|
||||
OUT: Y.B | Any | 0 | unn
|
||||
OUT: Y.B | Constant | 0 | unn
|
||||
OUT: Y.B | Data | 0 | unn
|
||||
OUT: Y.B | conforms | 0 | dcnst
|
||||
OUT: Y.B | notFunctional | 0 | dcnst
|
||||
OUT: Y.B | notInjective | 0 | dcnst
|
||||
OUT: Y.B | notInvTotal | 0 | dcnst
|
||||
OUT: Y.B | notRelational | 0 | dcnst
|
||||
OUT: Y.B | notTotal | 0 | dcnst
|
||||
OUT: Y.X | Any | 0 | unn
|
||||
OUT: Y.X | Boolean | 0 | unn
|
||||
OUT: Y.X | Cons | 2 | con
|
||||
OUT: Y.X | Constant | 0 | unn
|
||||
OUT: Y.X | Data | 0 | unn
|
||||
OUT: Y.X | Integer | 0 | unn
|
||||
OUT: Y.X | List | 0 | unn
|
||||
OUT: Y.X | Natural | 0 | unn
|
||||
OUT: Y.X | NegInteger | 0 | unn
|
||||
OUT: Y.X | PosInteger | 0 | unn
|
||||
OUT: Y.X | Real | 0 | unn
|
||||
OUT: Y.X | String | 0 | unn
|
||||
OUT: Y.X | Things | 0 | unn
|
||||
OUT: Y.X.A1' | Any | 0 | unn
|
||||
OUT: Y.X.A1' | Constant | 0 | unn
|
||||
OUT: Y.X.A1' | Data | 0 | unn
|
||||
OUT: Y.X.A1' | conforms | 0 | dcnst
|
||||
OUT: Y.X.A1' | notFunctional | 0 | dcnst
|
||||
OUT: Y.X.A1' | notInjective | 0 | dcnst
|
||||
OUT: Y.X.A1' | notInvTotal | 0 | dcnst
|
||||
OUT: Y.X.A1' | notRelational | 0 | dcnst
|
||||
OUT: Y.X.A1' | notTotal | 0 | dcnst
|
||||
OUT:
|
||||
OUT: Type constants: #Boolean #Cons #Cons[0] #Cons[1] #F #F' #F'[0] #F[0] #Integer #List #Natural #NegInteger #PosInteger #Real #String #Things #Type1 #Type2 A1'.#Any A1'.#Constant A1'.#Data D.#Any D.#Constant D.#Data X.#Any X.#Boolean X.#Cons X.#Cons[0] X.#Cons[1] X.#Constant X.#Data X.#Integer X.#List X.#Natural X.#NegInteger X.#PosInteger X.#Real X.#String X.#Things X.A1'.#Any X.A1'.#Constant X.A1'.#Data Y.#Any Y.#Boolean Y.#Cons Y.#Cons[0] Y.#Cons[1] Y.#Constant Y.#Data Y.#Integer Y.#List Y.#Natural Y.#NegInteger Y.#PosInteger Y.#Real Y.#String Y.#Things Y.A1'.#Any Y.A1'.#Constant Y.A1'.#Data Y.B.#Any Y.B.#Constant Y.B.#Data Y.X.#Any Y.X.#Boolean Y.X.#Cons Y.X.#Cons[0] Y.X.#Cons[1] Y.X.#Constant Y.X.#Data Y.X.#Integer Y.X.#List Y.X.#Natural Y.X.#NegInteger Y.X.#PosInteger Y.X.#Real Y.X.#String Y.X.#Things Y.X.A1'.#Any Y.X.A1'.#Constant Y.X.A1'.#Data
|
||||
OUT: Symbolic constants:
|
||||
OUT: Rationals: 1
|
||||
OUT: Strings:
|
||||
OUT: Variables: x
|
||||
OUT:
|
||||
OUT: []> typ D
|
||||
OUT: + Type environment at (93, 4)
|
||||
OUT: x: Y.X.Cons + Y.Cons
|
||||
OUT: Coerced arg 1 of (93, 4): Y -->
|
||||
OUT: + Type environment at (93, 12)
|
||||
OUT: x: Y.X.Cons + Y.Cons
|
||||
OUT: + Type environment at (96, 4)
|
||||
OUT: x: Cons + X.Cons
|
||||
OUT: Coerced arg 1 of (96, 4): --> Y
|
||||
OUT: + Type environment at (96, 13)
|
||||
OUT: x: Cons + X.Cons
|
||||
OUT:
|
||||
OUT: []> x
|
||||
OUT:
|
||||
EXIT: 0
|
||||
|
|
@ -0,0 +1,12 @@
|
|||
run: ..\..\..\..\Bld\Drops\Formula_Debug_x86\Formula.exe
|
||||
arg: -v: off -l: "tests.4ml"
|
||||
arg: -dt: "A1" -typ: "A1"
|
||||
arg: -dt: "A1'" -typ: "A1'"
|
||||
arg: -dt: "T1" -typ: "T1"
|
||||
arg: -dt: "B" -typ: "B"
|
||||
arg: -dt: "C" -typ: "C"
|
||||
arg: -dt: "T2" -typ: "T2"
|
||||
arg: -dt: "D" -typ: "D"
|
||||
arg: -x
|
||||
acc: .\
|
||||
dsc: Rules testing various coercions
|
||||
|
|
@ -0,0 +1,100 @@
|
|||
domain A1
|
||||
{
|
||||
Cons ::= new (val: Integer, tail: any Cons + {NIL}).
|
||||
Things ::= Cons.
|
||||
}
|
||||
|
||||
domain A1'
|
||||
{
|
||||
List ::= Cons + {NIL}.
|
||||
Cons ::= new (val: Real, tail: any List).
|
||||
Things ::= Cons + List.
|
||||
}
|
||||
|
||||
transform T1 (in1:: A1, in2:: A1) returns (out:: A1')
|
||||
{
|
||||
Triple ::= (in1.Cons + {NIL},
|
||||
in2.Cons + {NIL},
|
||||
out.Cons + {NIL}).
|
||||
|
||||
Things ::= Triple + in1.Things + in2.Things + out.Things.
|
||||
|
||||
//// Coercion through constants
|
||||
out.Cons(x, y) :- in1.Cons(x, y).
|
||||
|
||||
//// Multiple distinct coercions for same head term.
|
||||
Triple(c, c, c) :- c is in1.Cons.
|
||||
|
||||
//// Coercion not introduced when type already subtype of expected type
|
||||
_(x) :- x is Things.
|
||||
|
||||
//// Forced coercion through identity function.
|
||||
out._(x) :- x is in1.Cons.
|
||||
|
||||
//// Coercions on constructor applications
|
||||
out.Cons(1, in1.Cons(1, NIL)).
|
||||
|
||||
//// Robustness against explicit qualification
|
||||
out.Cons(1, out.Cons(1, NIL)).
|
||||
}
|
||||
|
||||
transform T1' (in1:: A1, in2:: A1) returns (out:: A1')
|
||||
{
|
||||
Triple ::= (in1.Cons + {NIL},
|
||||
in2.Cons + {NIL},
|
||||
out.Cons + {NIL}).
|
||||
|
||||
//// Coercion inside of comprehension
|
||||
q :- x is in1.Cons, count({ out.Cons(1, x) }) > 0.
|
||||
}
|
||||
|
||||
domain B includes X::A1', A1'
|
||||
{
|
||||
//// Coercion deletes the renaming prefix X.
|
||||
Cons(1, x) :- x is X.Cons.
|
||||
|
||||
//// Coercion extends the empty renaming prefix
|
||||
X.Cons(1, x) :- x is Cons.
|
||||
}
|
||||
|
||||
domain C includes Y::B, A1'
|
||||
{
|
||||
//// Coercion deletes the renaming prefix Y.X.
|
||||
Cons(1, x) :- x is X.Cons.
|
||||
|
||||
//// Coercion extends the empty renaming prefix to Y.X.
|
||||
X.Cons(1, x) :- x is Cons.
|
||||
|
||||
//// Coercion deletes the renaming prefix X.
|
||||
Y.Cons(1, x) :- x is X.Cons.
|
||||
|
||||
//// Coercion extends the empty renaming prefix
|
||||
X.Cons(1, x) :- x is Y.Cons.
|
||||
}
|
||||
|
||||
transform T2 (in1:: A1, in2:: A1) returns (out:: B)
|
||||
{
|
||||
//// Deeper qualification disambiguates coercion
|
||||
out.X._(x) :- x is in1.Cons.
|
||||
|
||||
//// Explicit qualification of Cons disambiguates coercion
|
||||
out.Cons(1, x) :- x is in1.Cons.
|
||||
}
|
||||
|
||||
domain D includes Y::B, X::A1', A1'
|
||||
{
|
||||
Type1 ::= Y.X.Cons + Y.Cons.
|
||||
Type2 ::= Cons + X.Cons.
|
||||
|
||||
F ::= (Type2).
|
||||
F' ::= (Type1).
|
||||
|
||||
//// Coercion deletes the renaming prefix Y.
|
||||
F(x) :- x is Type1.
|
||||
|
||||
//// Coercion adds the renaming prefix Y.
|
||||
F'(x) :- x is Type2.
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
|
@ -0,0 +1,78 @@
|
|||
=================================
|
||||
Console output
|
||||
=================================
|
||||
OUT:
|
||||
OUT: []> v off
|
||||
OUT: verbose off
|
||||
OUT:
|
||||
OUT: []> l tests.4ml
|
||||
OUT: (Failed) tests.4ml
|
||||
OUT: tests.4ml (20, 4): Argument 1 of function in1.Cons is unsafe. Some values of type Real are not allowed here.
|
||||
OUT: tests.4ml (20, 4): Argument 2 of function in1.Cons is badly typed. Cannot coerce values of type out.Cons.
|
||||
OUT: tests.4ml (25, 4): Argument 2 of function in1.Cons is badly typed. Cannot coerce values of type out.Cons.
|
||||
OUT: tests.4ml (29, 4): Argument 1 of function Triple is badly typed. Cannot coerce values of type in2.Cons.
|
||||
OUT: tests.4ml (29, 4): Argument 2 of function Triple is badly typed. Cannot coerce values of type in1.Cons.
|
||||
OUT: tests.4ml (29, 4): Argument 3 of function Triple is badly typed. Cannot coerce values of type in1.Cons.
|
||||
OUT: tests.4ml (32, 4): Argument 1 of function in2._ is unsafe. Some values of type T1.q are not allowed here.
|
||||
OUT: tests.4ml (32, 4): Argument 1 of function in2._ is unsafe. Some values of type Triple are not allowed here.
|
||||
OUT: tests.4ml (35, 4): Argument 1 of function in2._ is badly typed. Cannot coerce values of type out.Cons.
|
||||
OUT: tests.4ml (38, 4): Argument 2 of function in1.Cons is badly typed. Cannot coerce values of type out.Cons.
|
||||
OUT: tests.4ml (41, 32): Argument 2 of function in1.Cons is badly typed. Cannot coerce values of type out.Cons.
|
||||
OUT: tests.4ml (55, 4): Argument 1 of function G has an ambiguous coercion; possibly "Y.X" -> "".
|
||||
OUT: tests.4ml (55, 4): Argument 1 of function G has an ambiguous coercion; possibly "Y.X" -> "Y".
|
||||
OUT: tests.4ml (58, 4): Argument 1 of function G' has an ambiguous coercion; possibly "" -> "Y".
|
||||
OUT: tests.4ml (58, 4): Argument 1 of function G' has an ambiguous coercion; possibly "" -> "Y.X".
|
||||
OUT: tests.4ml (61, 4): Argument 1 of function G'' has an ambiguous coercion; possibly "Y" -> "".
|
||||
OUT: tests.4ml (61, 4): Argument 1 of function G'' has an ambiguous coercion; possibly "Y" -> "Y.X".
|
||||
OUT: tests.4ml (67, 4): Argument 1 of function out._ has an ambiguous coercion; possibly "in1" -> "out".
|
||||
OUT: tests.4ml (67, 4): Argument 1 of function out._ has an ambiguous coercion; possibly "in1" -> "out.X".
|
||||
OUT: tests.4ml (70, 4): Argument 1 of function in1._ is badly typed. Cannot coerce values of type out.Cons.
|
||||
OUT: tests.4ml (82, 4): Argument 1 of function F is badly typed. Cannot coerce values of type Y.X.Cons.
|
||||
OUT: tests.4ml (85, 4): Argument 1 of function F' is badly typed. Cannot coerce values of type Y.Cons.
|
||||
OUT: tests.4ml (0, 0): The install operation failed
|
||||
OUT:
|
||||
OUT: []> dt A1
|
||||
OUT: No module with that name
|
||||
OUT:
|
||||
OUT: []> typ A1
|
||||
OUT: No module with that name
|
||||
OUT:
|
||||
OUT: []> dt A1'
|
||||
OUT: No module with that name
|
||||
OUT:
|
||||
OUT: []> typ A1'
|
||||
OUT: No module with that name
|
||||
OUT:
|
||||
OUT: []> dt T1
|
||||
OUT: No module with that name
|
||||
OUT:
|
||||
OUT: []> typ T1
|
||||
OUT: No module with that name
|
||||
OUT:
|
||||
OUT: []> dt B
|
||||
OUT: No module with that name
|
||||
OUT:
|
||||
OUT: []> typ B
|
||||
OUT: No module with that name
|
||||
OUT:
|
||||
OUT: []> dt C
|
||||
OUT: No module with that name
|
||||
OUT:
|
||||
OUT: []> typ C
|
||||
OUT: No module with that name
|
||||
OUT:
|
||||
OUT: []> dt T2
|
||||
OUT: No module with that name
|
||||
OUT:
|
||||
OUT: []> typ T2
|
||||
OUT: No module with that name
|
||||
OUT:
|
||||
OUT: []> dt D
|
||||
OUT: No module with that name
|
||||
OUT:
|
||||
OUT: []> typ D
|
||||
OUT: No module with that name
|
||||
OUT:
|
||||
OUT: []> x
|
||||
OUT:
|
||||
EXIT: 1
|
||||
|
|
@ -0,0 +1,12 @@
|
|||
run: ..\..\..\..\Bld\Drops\Formula_Debug_x86\Formula.exe
|
||||
arg: -v: off -l: "tests.4ml"
|
||||
arg: -dt: "A1" -typ: "A1"
|
||||
arg: -dt: "A1'" -typ: "A1'"
|
||||
arg: -dt: "T1" -typ: "T1"
|
||||
arg: -dt: "B" -typ: "B"
|
||||
arg: -dt: "C" -typ: "C"
|
||||
arg: -dt: "T2" -typ: "T2"
|
||||
arg: -dt: "D" -typ: "D"
|
||||
arg: -x
|
||||
acc: .\
|
||||
dsc: Rules testing various uncoercible heads
|
||||
|
|
@ -0,0 +1,86 @@
|
|||
domain A1
|
||||
{
|
||||
Cons ::= new (val: Integer, tail: any Cons + {NIL}).
|
||||
}
|
||||
|
||||
domain A1'
|
||||
{
|
||||
List ::= Cons + {NIL}.
|
||||
Cons ::= new (val: Real, tail: any List).
|
||||
}
|
||||
|
||||
transform T1 (in1:: A1, in2:: A1) returns (out:: A1')
|
||||
{
|
||||
InCons ::= in1.Cons + in2.Cons.
|
||||
Triple ::= (in1.Cons + {NIL},
|
||||
in2.Cons + {NIL},
|
||||
out.Cons + {NIL}).
|
||||
|
||||
//// Cannot Coercion because out lists are bigger than in lists
|
||||
in1.Cons(x, y) :- out.Cons(x, y).
|
||||
|
||||
//// Cannot coerce, because coercion must be possible for all
|
||||
//// members of type, even though type inference shows coercion is possible.
|
||||
//// Could relax this constraint in the future.
|
||||
in1.Cons(1, y) :- out.Cons(1, y), y = out.Cons(z, NIL), z: Integer.
|
||||
|
||||
|
||||
//// No common prefix that can coerce both kinds of lists.
|
||||
Triple(c, c, c) :- c is InCons.
|
||||
|
||||
//// Unsafe coercions
|
||||
in2._(x) :- x is T1.Any.
|
||||
|
||||
//// Unsafe coercions.
|
||||
in2._(x) :- x is out.Cons.
|
||||
|
||||
//// Cannot coerce in this direction, because of widening
|
||||
in1.Cons(1, out.Cons(1, NIL)).
|
||||
|
||||
//// Coercion inside of comprehension
|
||||
q :- x is out.Cons, count({ in1.Cons(1, x) }) > 0.
|
||||
}
|
||||
|
||||
domain B includes X::A1', A1'
|
||||
{
|
||||
}
|
||||
|
||||
domain C includes Y::B, A1'
|
||||
{
|
||||
G ::= (Cons + Y.Cons).
|
||||
G' ::= (Y.X.Cons + Y.Cons).
|
||||
G'' ::= (Cons + X.Cons).
|
||||
|
||||
//// Ambiguous coercion.
|
||||
G(x) :- x is X.Cons.
|
||||
|
||||
//// Ambiguous coercion.
|
||||
G'(x) :- x is Cons.
|
||||
|
||||
//// Ambiguous coercion.
|
||||
G''(x) :- x is Y.Cons.
|
||||
}
|
||||
|
||||
transform T2 (in1:: A1, in2:: A1) returns (out:: B)
|
||||
{
|
||||
//// Ambiguous coercion
|
||||
out._(x) :- x is in1.Cons.
|
||||
|
||||
//// Unsafe coercion
|
||||
in1._(y) :- out.Cons(x, y).
|
||||
}
|
||||
|
||||
domain D includes Y::B, X::A1', A1'
|
||||
{
|
||||
Type1 ::= Y.X.Cons + X.Cons.
|
||||
Type2 ::= Cons + Y.Cons.
|
||||
|
||||
F ::= (Type2).
|
||||
F' ::= (Type1).
|
||||
|
||||
//// No coercion satisfying constraints.
|
||||
F(x) :- x is Type1.
|
||||
|
||||
//// No coercion satisfying constraints.
|
||||
F'(x) :- x is Type2.
|
||||
}
|
||||
|
|
@ -0,0 +1,317 @@
|
|||
=================================
|
||||
Console output
|
||||
=================================
|
||||
OUT:
|
||||
OUT: []> v off
|
||||
OUT: verbose off
|
||||
OUT:
|
||||
OUT: []> l tests.4ml
|
||||
OUT: (Compiled) tests.4ml
|
||||
OUT:
|
||||
OUT: []> dt CanForms
|
||||
OUT: Reduced form
|
||||
OUT: domain CanForms
|
||||
OUT: {
|
||||
OUT: F ::= new (Integer).
|
||||
OUT: Zero ::= { 0 }.
|
||||
OUT: G ::= new (nxt: any G + { NIL }).
|
||||
OUT: Nil ::= { NIL }.
|
||||
OUT: H ::= new (H').
|
||||
OUT: H' ::= new ({ 0 }).
|
||||
OUT: I ::= new (I').
|
||||
OUT: I' ::= new ({ RED }).
|
||||
OUT: R ::= new ({ 0, 1 }, { 0, 1 }).
|
||||
OUT: R' ::= new (Boolean, Boolean).
|
||||
OUT: Thing ::= F + G + Nil + H + H' + I + I' + R + R' + Real + String + Boolean.
|
||||
OUT:
|
||||
OUT: F(x)
|
||||
OUT: :-
|
||||
OUT: F(x), x : PosInteger;
|
||||
OUT: F(x), x : NegInteger;
|
||||
OUT: F(x), x : Zero.
|
||||
OUT:
|
||||
OUT: _(y)
|
||||
OUT: :-
|
||||
OUT: y is G(x), x : G;
|
||||
OUT: y is G(x), x : Nil.
|
||||
OUT:
|
||||
OUT: _(x)
|
||||
OUT: :-
|
||||
OUT: x = H(H'(0)).
|
||||
OUT:
|
||||
OUT: _(x)
|
||||
OUT: :-
|
||||
OUT: x = I(I'(RED)).
|
||||
OUT:
|
||||
OUT: _(x)
|
||||
OUT: :-
|
||||
OUT: x is Thing.
|
||||
OUT:
|
||||
OUT: G(x.nxt.nxt.nxt.nxt.nxt.nxt.nxt)
|
||||
OUT: :-
|
||||
OUT: x is Thing.
|
||||
OUT:
|
||||
OUT: G(x.nxt.nxt.nxt.nxt.nxt.nxt.nxt)
|
||||
OUT: :-
|
||||
OUT: x is Thing;
|
||||
OUT: x is Thing, x = G(G(G(_))).
|
||||
OUT:
|
||||
OUT: G(x)
|
||||
OUT: :-
|
||||
OUT: x is Thing, x.nxt.nxt.nxt = G(_);
|
||||
OUT: x is Thing, x.nxt.nxt.nxt.nxt.nxt.nxt.nxt = G(_).
|
||||
OUT:
|
||||
OUT: _(x)
|
||||
OUT: :-
|
||||
OUT: x is R(0, 0).
|
||||
OUT:
|
||||
OUT: _(x)
|
||||
OUT: :-
|
||||
OUT: x is R(0, 1);
|
||||
OUT: x is R(1, 0);
|
||||
OUT: x is R(1, 1).
|
||||
OUT:
|
||||
OUT: _(x)
|
||||
OUT: :-
|
||||
OUT: x is R(0, 1);
|
||||
OUT: x is R(1, 0);
|
||||
OUT: x is R(1, 1);
|
||||
OUT: x is R(0, 0).
|
||||
OUT:
|
||||
OUT: _(x)
|
||||
OUT: :-
|
||||
OUT: x is R'(TRUE, FALSE);
|
||||
OUT: x is R'(FALSE, TRUE);
|
||||
OUT: x is R'(TRUE, TRUE).
|
||||
OUT:
|
||||
OUT: _(x)
|
||||
OUT: :-
|
||||
OUT: x is R'(TRUE, FALSE);
|
||||
OUT: x is R'(FALSE, TRUE);
|
||||
OUT: x is R'(TRUE, TRUE);
|
||||
OUT: x is R'(FALSE, FALSE).
|
||||
OUT:
|
||||
OUT: _(x)
|
||||
OUT: :-
|
||||
OUT: x is R'(TRUE, y), y : Boolean;
|
||||
OUT: x is R'(y, TRUE), y : Boolean.
|
||||
OUT:
|
||||
OUT: _(x)
|
||||
OUT: :-
|
||||
OUT: x is R'(TRUE, y), y : Boolean;
|
||||
OUT: x is R'(y, TRUE), y : Boolean;
|
||||
OUT: x is R'(FALSE, FALSE).
|
||||
OUT: }
|
||||
OUT:
|
||||
OUT: Symbol table
|
||||
OUT: Space | Name | Arity | Kind
|
||||
OUT: ----------|---------------|-------|-------
|
||||
OUT: | Boolean | 0 | unn
|
||||
OUT: | F | 1 | con
|
||||
OUT: | FALSE | 0 | ncnst
|
||||
OUT: | G | 1 | con
|
||||
OUT: | H | 1 | con
|
||||
OUT: | H' | 1 | con
|
||||
OUT: | I | 1 | con
|
||||
OUT: | I' | 1 | con
|
||||
OUT: | Integer | 0 | unn
|
||||
OUT: | NIL | 0 | ncnst
|
||||
OUT: | Natural | 0 | unn
|
||||
OUT: | NegInteger | 0 | unn
|
||||
OUT: | Nil | 0 | unn
|
||||
OUT: | PosInteger | 0 | unn
|
||||
OUT: | R | 2 | con
|
||||
OUT: | R' | 2 | con
|
||||
OUT: | RED | 0 | ncnst
|
||||
OUT: | Real | 0 | unn
|
||||
OUT: | String | 0 | unn
|
||||
OUT: | TRUE | 0 | ncnst
|
||||
OUT: | Thing | 0 | unn
|
||||
OUT: | Zero | 0 | unn
|
||||
OUT: CanForms | Any | 0 | unn
|
||||
OUT: CanForms | Constant | 0 | unn
|
||||
OUT: CanForms | Data | 0 | unn
|
||||
OUT: CanForms | conforms | 0 | dcnst
|
||||
OUT: CanForms | notFunctional | 0 | dcnst
|
||||
OUT: CanForms | notInjective | 0 | dcnst
|
||||
OUT: CanForms | notInvTotal | 0 | dcnst
|
||||
OUT: CanForms | notRelational | 0 | dcnst
|
||||
OUT: CanForms | notTotal | 0 | dcnst
|
||||
OUT:
|
||||
OUT: Type constants: #Boolean #F #F[0] #G #G[0] #H #H' #H'[0] #H[0] #I #I' #I'[0] #I[0] #Integer #Natural #NegInteger #Nil #PosInteger #R #R' #R'[0] #R'[1] #R[0] #R[1] #Real #String #Thing #Zero CanForms.#Any CanForms.#Constant CanForms.#Data
|
||||
OUT: Symbolic constants:
|
||||
OUT: Rationals: 0 1
|
||||
OUT: Strings:
|
||||
OUT: Variables: x y
|
||||
OUT:
|
||||
OUT: []> typ CanForms
|
||||
OUT: + Type environment at (21, 4)
|
||||
OUT: x: Integer
|
||||
OUT: ~dc0: F
|
||||
OUT: + Type environment at (21, 12)
|
||||
OUT: x: PosInteger
|
||||
OUT: ~dc0: F(PosInteger)
|
||||
OUT: + Type environment at (22, 12)
|
||||
OUT: x: NegInteger
|
||||
OUT: ~dc0: F(NegInteger)
|
||||
OUT: + Type environment at (23, 12)
|
||||
OUT: x: {0..0}
|
||||
OUT: ~dc0: F({0..0})
|
||||
OUT: + Type environment at (25, 4)
|
||||
OUT: x: G + {NIL}
|
||||
OUT: y: G
|
||||
OUT: + Type environment at (25, 12)
|
||||
OUT: x: G
|
||||
OUT: y: G(G)
|
||||
OUT: + Type environment at (26, 12)
|
||||
OUT: x: {NIL}
|
||||
OUT: y: G({NIL})
|
||||
OUT: + Type environment at (28, 4)
|
||||
OUT: x: H
|
||||
OUT: + Type environment at (28, 14)
|
||||
OUT: x: H
|
||||
OUT: + Type environment at (30, 4)
|
||||
OUT: x: I
|
||||
OUT: + Type environment at (30, 14)
|
||||
OUT: x: I
|
||||
OUT: + Type environment at (32, 4)
|
||||
OUT: x: R' + R + I' + I + H' + H + G + F
|
||||
OUT: + Type environment at (32, 12)
|
||||
OUT: x: R' + R + I' + I + H' + H + G + F
|
||||
OUT: + Type environment at (34, 4)
|
||||
OUT: x: G(G(G(G(G(G(G))))))
|
||||
OUT: ~sv0: G(G(G(G(G(G)))))
|
||||
OUT: ~sv1: G(G(G(G(G))))
|
||||
OUT: ~sv2: G(G(G(G)))
|
||||
OUT: ~sv3: G(G(G))
|
||||
OUT: ~sv4: G(G)
|
||||
OUT: ~sv5: G
|
||||
OUT: ~sv6: G + {NIL}
|
||||
OUT: + Type environment at (34, 40)
|
||||
OUT: x: G(G(G(G(G(G(G))))))
|
||||
OUT: ~sv0: G(G(G(G(G(G)))))
|
||||
OUT: ~sv1: G(G(G(G(G))))
|
||||
OUT: ~sv2: G(G(G(G)))
|
||||
OUT: ~sv3: G(G(G))
|
||||
OUT: ~sv4: G(G)
|
||||
OUT: ~sv5: G
|
||||
OUT: ~sv6: G + {NIL}
|
||||
OUT: + Type environment at (36, 4)
|
||||
OUT: x: G(G(G(G(G(G(G))))))
|
||||
OUT: ~dc0: G(G(G(G)))
|
||||
OUT: ~sv0: G(G(G(G(G(G)))))
|
||||
OUT: ~sv1: G(G(G(G(G))))
|
||||
OUT: ~sv2: G(G(G(G)))
|
||||
OUT: ~sv3: G(G(G))
|
||||
OUT: ~sv4: G(G)
|
||||
OUT: ~sv5: G
|
||||
OUT: ~sv6: G + {NIL}
|
||||
OUT: + Type environment at (36, 40)
|
||||
OUT: x: G(G(G(G(G(G(G))))))
|
||||
OUT: ~sv0: G(G(G(G(G(G)))))
|
||||
OUT: ~sv1: G(G(G(G(G))))
|
||||
OUT: ~sv2: G(G(G(G)))
|
||||
OUT: ~sv3: G(G(G))
|
||||
OUT: ~sv4: G(G)
|
||||
OUT: ~sv5: G
|
||||
OUT: ~sv6: G + {NIL}
|
||||
OUT: + Type environment at (37, 40)
|
||||
OUT: x: G(G(G(G(G(G(G))))))
|
||||
OUT: ~dc0: G(G(G(G)))
|
||||
OUT: ~sv0: G(G(G(G(G(G)))))
|
||||
OUT: ~sv1: G(G(G(G(G))))
|
||||
OUT: ~sv2: G(G(G(G)))
|
||||
OUT: ~sv3: G(G(G))
|
||||
OUT: ~sv4: G(G)
|
||||
OUT: ~sv5: G
|
||||
OUT: ~sv6: G + {NIL}
|
||||
OUT: + Type environment at (39, 4)
|
||||
OUT: x: G(G(G(G(G(G(G(G)))) + G)))
|
||||
OUT: ~dc0: G + {NIL}
|
||||
OUT: ~sv0: G(G(G(G(G(G(G)))) + G))
|
||||
OUT: ~sv1: G(G(G(G(G(G)))) + G)
|
||||
OUT: ~sv2: G(G(G(G(G)))) + G
|
||||
OUT: ~sv3: G(G(G(G)))
|
||||
OUT: ~sv4: G(G(G))
|
||||
OUT: ~sv5: G(G)
|
||||
OUT: ~sv6: G
|
||||
OUT: + Type environment at (39, 12)
|
||||
OUT: x: G(G(G(G)))
|
||||
OUT: ~dc0: G + {NIL}
|
||||
OUT: ~sv0: G(G(G))
|
||||
OUT: ~sv1: G(G)
|
||||
OUT: ~sv2: G
|
||||
OUT: + Type environment at (40, 12)
|
||||
OUT: x: G(G(G(G(G(G(G(G)))))))
|
||||
OUT: ~dc0: G + {NIL}
|
||||
OUT: ~sv0: G(G(G(G(G(G(G))))))
|
||||
OUT: ~sv1: G(G(G(G(G(G)))))
|
||||
OUT: ~sv2: G(G(G(G(G))))
|
||||
OUT: ~sv3: G(G(G(G)))
|
||||
OUT: ~sv4: G(G(G))
|
||||
OUT: ~sv5: G(G)
|
||||
OUT: ~sv6: G
|
||||
OUT: + Type environment at (42, 4)
|
||||
OUT: x: R({0..0}, {0..0})
|
||||
OUT: + Type environment at (42, 12)
|
||||
OUT: x: R({0..0}, {0..0})
|
||||
OUT: + Type environment at (44, 4)
|
||||
OUT: x: R({1..1}, {0..1}) + R({0..1}, {1..1})
|
||||
OUT: + Type environment at (44, 12)
|
||||
OUT: x: R({0..0}, {1..1})
|
||||
OUT: + Type environment at (44, 26)
|
||||
OUT: x: R({1..1}, {0..0})
|
||||
OUT: + Type environment at (44, 40)
|
||||
OUT: x: R({1..1}, {1..1})
|
||||
OUT: + Type environment at (46, 4)
|
||||
OUT: x: R
|
||||
OUT: + Type environment at (46, 12)
|
||||
OUT: x: R({0..0}, {1..1})
|
||||
OUT: + Type environment at (46, 26)
|
||||
OUT: x: R({1..1}, {0..0})
|
||||
OUT: + Type environment at (46, 40)
|
||||
OUT: x: R({1..1}, {1..1})
|
||||
OUT: + Type environment at (46, 54)
|
||||
OUT: x: R({0..0}, {0..0})
|
||||
OUT: + Type environment at (48, 4)
|
||||
OUT: x: R'({TRUE}, {FALSE} + {TRUE}) + R'({FALSE} + {TRUE}, {TRUE})
|
||||
OUT: + Type environment at (48, 12)
|
||||
OUT: x: R'({TRUE}, {FALSE})
|
||||
OUT: + Type environment at (48, 34)
|
||||
OUT: x: R'({FALSE}, {TRUE})
|
||||
OUT: + Type environment at (48, 56)
|
||||
OUT: x: R'({TRUE}, {TRUE})
|
||||
OUT: + Type environment at (50, 4)
|
||||
OUT: x: R'
|
||||
OUT: + Type environment at (50, 12)
|
||||
OUT: x: R'({TRUE}, {FALSE})
|
||||
OUT: + Type environment at (50, 34)
|
||||
OUT: x: R'({FALSE}, {TRUE})
|
||||
OUT: + Type environment at (51, 12)
|
||||
OUT: x: R'({TRUE}, {TRUE})
|
||||
OUT: + Type environment at (51, 34)
|
||||
OUT: x: R'({FALSE}, {FALSE})
|
||||
OUT: + Type environment at (53, 4)
|
||||
OUT: x: R'({TRUE}, {FALSE} + {TRUE}) + R'({FALSE} + {TRUE}, {TRUE})
|
||||
OUT: y: {FALSE} + {TRUE}
|
||||
OUT: + Type environment at (53, 12)
|
||||
OUT: x: R'({TRUE}, {FALSE} + {TRUE})
|
||||
OUT: y: {FALSE} + {TRUE}
|
||||
OUT: + Type environment at (54, 12)
|
||||
OUT: x: R'({FALSE} + {TRUE}, {TRUE})
|
||||
OUT: y: {FALSE} + {TRUE}
|
||||
OUT: + Type environment at (56, 4)
|
||||
OUT: x: R'
|
||||
OUT: y: {FALSE} + {TRUE}
|
||||
OUT: + Type environment at (56, 12)
|
||||
OUT: x: R'({TRUE}, {FALSE} + {TRUE})
|
||||
OUT: y: {FALSE} + {TRUE}
|
||||
OUT: + Type environment at (57, 12)
|
||||
OUT: x: R'({FALSE} + {TRUE}, {TRUE})
|
||||
OUT: y: {FALSE} + {TRUE}
|
||||
OUT: + Type environment at (58, 12)
|
||||
OUT: x: R'({FALSE}, {FALSE})
|
||||
OUT:
|
||||
OUT: []> x
|
||||
OUT:
|
||||
EXIT: 0
|
||||
|
|
@ -0,0 +1,4 @@
|
|||
run: ..\..\..\..\Bld\Drops\Formula_Debug_x86\Formula.exe
|
||||
arg: -v: off -l: "tests.4ml" -dt: "CanForms" -typ: "CanForms" -x
|
||||
acc: .\
|
||||
dsc: Rules generating various canonical forms
|
||||
|
|
@ -0,0 +1,59 @@
|
|||
domain CanForms
|
||||
{
|
||||
F ::= new (Integer).
|
||||
Zero ::= { 0 }.
|
||||
|
||||
G ::= new (nxt: any G + {NIL}).
|
||||
Nil ::= {NIL}.
|
||||
|
||||
H ::= new (H').
|
||||
H' ::= new ({0}).
|
||||
|
||||
I ::= new (I').
|
||||
I' ::= new ({RED}).
|
||||
|
||||
R ::= new ({0, 1}, {0, 1}).
|
||||
|
||||
R' ::= new (Boolean , Boolean).
|
||||
|
||||
Thing ::= F + G + Nil + H + H' + I + I' + R + R' + Real + String + Boolean.
|
||||
|
||||
F(x) :- F(x), x : PosInteger;
|
||||
F(x), x : NegInteger;
|
||||
F(x), x : Zero.
|
||||
|
||||
_(y) :- y is G(x), x : G;
|
||||
y is G(x), x : Nil.
|
||||
|
||||
_(x) :- x = H(H'(0)).
|
||||
|
||||
_(x) :- x = I(I'(RED)).
|
||||
|
||||
_(x) :- x is Thing.
|
||||
|
||||
G(x.nxt.nxt.nxt.nxt.nxt.nxt.nxt) :- x is Thing.
|
||||
|
||||
G(x.nxt.nxt.nxt.nxt.nxt.nxt.nxt) :- x is Thing;
|
||||
x is Thing, x = G(G(G(_))).
|
||||
|
||||
G(x) :- x is Thing, x.nxt.nxt.nxt = G(_);
|
||||
x is Thing, x.nxt.nxt.nxt.nxt.nxt.nxt.nxt = G(_).
|
||||
|
||||
_(x) :- x is R(0, 0).
|
||||
|
||||
_(x) :- x is R(0, 1); x is R(1, 0); x is R(1, 1).
|
||||
|
||||
_(x) :- x is R(0, 1); x is R(1, 0); x is R(1, 1); x is R(0, 0).
|
||||
|
||||
_(x) :- x is R'(TRUE, FALSE); x is R'(FALSE, TRUE); x is R'(TRUE, TRUE).
|
||||
|
||||
_(x) :- x is R'(TRUE, FALSE); x is R'(FALSE, TRUE);
|
||||
x is R'(TRUE, TRUE); x is R'(FALSE, FALSE).
|
||||
|
||||
_(x) :- x is R'(TRUE, y), y : Boolean;
|
||||
x is R'(y, TRUE), y : Boolean.
|
||||
|
||||
_(x) :- x is R'(TRUE, y), y : Boolean;
|
||||
x is R'(y, TRUE), y : Boolean;
|
||||
x is R'(FALSE, FALSE).
|
||||
}
|
||||
|
|
@ -0,0 +1,407 @@
|
|||
=================================
|
||||
Console output
|
||||
=================================
|
||||
OUT:
|
||||
OUT: []> v off
|
||||
OUT: verbose off
|
||||
OUT:
|
||||
OUT: []> l tests.4ml
|
||||
OUT: (Compiled) tests.4ml
|
||||
OUT:
|
||||
OUT: []> dt Good
|
||||
OUT: Reduced form
|
||||
OUT: domain Good extends Base
|
||||
OUT: {
|
||||
OUT: P ::= ({ 1..1000000 }, { 1000001..1000001, TRUE }).
|
||||
OUT: P' ::= ({ 1..1000000, FALSE }, { 1000001..1000001, TRUE }).
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: TRUE >= FALSE.
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: TRUE >= 1.
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: TRUE >= "TRUE".
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: TRUE >= TRUE.
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: 1 >= 0.
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: "TRUE" >= "FALSE".
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: x is Tree(2, _), y is Tree(1, Tree(_, _)), x >= y.
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: Cons(1, Cons(2, Cons(3, Cons(4, NIL)))) >= Cons(1, Cons(2, Cons(3, NIL))).
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: x is Tree(Tree(_, _), _), y is Tree(2, _), x >= y.
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: x is Tree, x.lft.lft.lft = Tree(_, _), y is Tree, y.lft.lft = NIL, x >= y.
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: x is B, y is A, x >= y.
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: A(_) >= 0.
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: A(_) >= "0".
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: A(_) >= NIL.
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: "abcdefg" >= "abc".
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: FALSE < TRUE.
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: 1 < TRUE.
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: "TRUE" < TRUE.
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: TRUE <= TRUE.
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: 0 < 1.
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: "FALSE" < "TRUE".
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: x is Tree(1, Tree(_, _)), y is Tree(2, _), x < y.
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: Cons(1, Cons(2, Cons(3, NIL))) < Cons(1, Cons(2, Cons(3, Cons(4, NIL)))).
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: x is Tree(Tree(_, _), _), y is Tree(2, _), y < x.
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: x is Tree, x.lft.lft.lft = Tree(_, _), y is Tree, y.lft.lft = NIL, y < x.
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: x is B, y is A, y < x.
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: 0 < A(_).
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: "0" < A(_).
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: NIL < A(_).
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: "abc" < "abcdefg".
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: P(x, y), x <= y.
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: P'(x, y), or(x, x) < and(y, y).
|
||||
OUT:
|
||||
OUT: q
|
||||
OUT: :-
|
||||
OUT: R(x), y = -1 * x, x >= y.
|
||||
OUT: }
|
||||
OUT:
|
||||
OUT: Symbol table
|
||||
OUT: Space | Name | Arity | Kind
|
||||
OUT: -------|---------------|-------|-------
|
||||
OUT: | A | 1 | con
|
||||
OUT: | A' | 1 | con
|
||||
OUT: | B | 1 | con
|
||||
OUT: | Boolean | 0 | unn
|
||||
OUT: | Cons | 2 | con
|
||||
OUT: | F | 1 | con
|
||||
OUT: | FALSE | 0 | ncnst
|
||||
OUT: | Integer | 0 | unn
|
||||
OUT: | NIL | 0 | ncnst
|
||||
OUT: | Natural | 0 | unn
|
||||
OUT: | NegInteger | 0 | unn
|
||||
OUT: | P | 2 | con
|
||||
OUT: | P' | 2 | con
|
||||
OUT: | PosInteger | 0 | unn
|
||||
OUT: | R | 1 | con
|
||||
OUT: | Real | 0 | unn
|
||||
OUT: | String | 0 | unn
|
||||
OUT: | TRUE | 0 | ncnst
|
||||
OUT: | Tree | 2 | con
|
||||
OUT: Base | Any | 0 | unn
|
||||
OUT: Base | Constant | 0 | unn
|
||||
OUT: Base | Data | 0 | unn
|
||||
OUT: Base | conforms | 0 | dcnst
|
||||
OUT: Base | notFunctional | 0 | dcnst
|
||||
OUT: Base | notInjective | 0 | dcnst
|
||||
OUT: Base | notInvTotal | 0 | dcnst
|
||||
OUT: Base | notRelational | 0 | dcnst
|
||||
OUT: Base | notTotal | 0 | dcnst
|
||||
OUT: Good | Any | 0 | unn
|
||||
OUT: Good | Constant | 0 | unn
|
||||
OUT: Good | Data | 0 | unn
|
||||
OUT: Good | conforms | 0 | dcnst
|
||||
OUT: Good | notFunctional | 0 | dcnst
|
||||
OUT: Good | notInjective | 0 | dcnst
|
||||
OUT: Good | notInvTotal | 0 | dcnst
|
||||
OUT: Good | notRelational | 0 | dcnst
|
||||
OUT: Good | notTotal | 0 | dcnst
|
||||
OUT: Good | q | 0 | dcnst
|
||||
OUT:
|
||||
OUT: Type constants: #A #A' #A'[0] #A[0] #B #B[0] #Boolean #Cons #Cons[0] #Cons[1] #F #F[0] #Integer #Natural #NegInteger #P #P' #P'[0] #P'[1] #P[0] #P[1] #PosInteger #R #R[0] #Real #String #Tree #Tree[0] #Tree[1] Base.#Any Base.#Constant Base.#Data Good.#Any Good.#Constant Good.#Data
|
||||
OUT: Symbolic constants:
|
||||
OUT: Rationals: -1 0 1 2 3 4 1000000 1000001
|
||||
OUT: Strings: "0" "FALSE" "TRUE" "abc" "abcdefg"
|
||||
OUT: Variables: x y
|
||||
OUT:
|
||||
OUT: []> typ Good
|
||||
OUT: + Type environment at (16, 4)
|
||||
OUT: + Type environment at (16, 14)
|
||||
OUT: + Type environment at (17, 4)
|
||||
OUT: + Type environment at (17, 14)
|
||||
OUT: + Type environment at (18, 4)
|
||||
OUT: + Type environment at (18, 14)
|
||||
OUT: + Type environment at (19, 4)
|
||||
OUT: + Type environment at (19, 14)
|
||||
OUT: + Type environment at (20, 4)
|
||||
OUT: + Type environment at (20, 11)
|
||||
OUT: + Type environment at (21, 4)
|
||||
OUT: + Type environment at (21, 16)
|
||||
OUT: + Type environment at (23, 4)
|
||||
OUT: x: Tree({2..2}, Tree + {NIL} + Natural)
|
||||
OUT: ~dc0: Tree + {NIL} + Natural
|
||||
OUT: y: Tree({1..1}, Tree)
|
||||
OUT: ~dc1: Tree + {NIL} + Natural
|
||||
OUT: ~dc2: Tree + {NIL} + Natural
|
||||
OUT: + Type environment at (23, 9)
|
||||
OUT: x: Tree({2..2}, Tree + {NIL} + Natural)
|
||||
OUT: ~dc0: Tree + {NIL} + Natural
|
||||
OUT: y: Tree({1..1}, Tree)
|
||||
OUT: ~dc1: Tree + {NIL} + Natural
|
||||
OUT: ~dc2: Tree + {NIL} + Natural
|
||||
OUT: + Type environment at (24, 4)
|
||||
OUT: + Type environment at (24, 49)
|
||||
OUT: + Type environment at (25, 4)
|
||||
OUT: x: Tree(Tree, Tree + {NIL} + Natural)
|
||||
OUT: ~dc0: Tree + {NIL} + Natural
|
||||
OUT: y: Tree({2..2}, Tree + {NIL} + Natural)
|
||||
OUT: ~dc1: Tree + {NIL} + Natural
|
||||
OUT: ~dc2: Tree + {NIL} + Natural
|
||||
OUT: ~dc3: Tree + {NIL} + Natural
|
||||
OUT: + Type environment at (25, 9)
|
||||
OUT: x: Tree(Tree, Tree + {NIL} + Natural)
|
||||
OUT: ~dc0: Tree + {NIL} + Natural
|
||||
OUT: y: Tree({2..2}, Tree + {NIL} + Natural)
|
||||
OUT: ~dc1: Tree + {NIL} + Natural
|
||||
OUT: ~dc2: Tree + {NIL} + Natural
|
||||
OUT: ~dc3: Tree + {NIL} + Natural
|
||||
OUT: + Type environment at (26, 4)
|
||||
OUT: x: Tree(Tree(Tree(Tree, Tree + {NIL} + Natural), Tree + {NIL} + Natural), Tree + {NIL} + Natural)
|
||||
OUT: ~dc0: Tree + {NIL} + Natural
|
||||
OUT: y: Tree(Tree({NIL}, Tree + {NIL} + Natural), Tree + {NIL} + Natural)
|
||||
OUT: ~dc1: Tree + {NIL} + Natural
|
||||
OUT: ~sv0: Tree(Tree(Tree, Tree + {NIL} + Natural), Tree + {NIL} + Natural)
|
||||
OUT: ~sv1: Tree + {NIL} + Natural
|
||||
OUT: ~sv2: Tree({NIL}, Tree + {NIL} + Natural)
|
||||
OUT: ~sv3: Tree + {NIL} + Natural
|
||||
OUT: ~sv4: Tree(Tree, Tree + {NIL} + Natural)
|
||||
OUT: ~sv5: Tree + {NIL} + Natural
|
||||
OUT: ~sv6: Tree
|
||||
OUT: ~sv7: Tree + {NIL} + Natural
|
||||
OUT: ~sv8: {NIL}
|
||||
OUT: ~sv9: Tree + {NIL} + Natural
|
||||
OUT: + Type environment at (26, 9)
|
||||
OUT: x: Tree(Tree(Tree(Tree, Tree + {NIL} + Natural), Tree + {NIL} + Natural), Tree + {NIL} + Natural)
|
||||
OUT: ~dc0: Tree + {NIL} + Natural
|
||||
OUT: y: Tree(Tree({NIL}, Tree + {NIL} + Natural), Tree + {NIL} + Natural)
|
||||
OUT: ~dc1: Tree + {NIL} + Natural
|
||||
OUT: ~sv0: Tree(Tree(Tree, Tree + {NIL} + Natural), Tree + {NIL} + Natural)
|
||||
OUT: ~sv1: Tree + {NIL} + Natural
|
||||
OUT: ~sv2: Tree({NIL}, Tree + {NIL} + Natural)
|
||||
OUT: ~sv3: Tree + {NIL} + Natural
|
||||
OUT: ~sv4: Tree(Tree, Tree + {NIL} + Natural)
|
||||
OUT: ~sv5: Tree + {NIL} + Natural
|
||||
OUT: ~sv6: Tree
|
||||
OUT: ~sv7: Tree + {NIL} + Natural
|
||||
OUT: ~sv8: {NIL}
|
||||
OUT: ~sv9: Tree + {NIL} + Natural
|
||||
OUT: + Type environment at (29, 4)
|
||||
OUT: x: B
|
||||
OUT: y: A
|
||||
OUT: + Type environment at (29, 9)
|
||||
OUT: x: B
|
||||
OUT: y: A
|
||||
OUT: + Type environment at (30, 4)
|
||||
OUT: ~dc0: {FALSE}
|
||||
OUT: + Type environment at (30, 14)
|
||||
OUT: ~dc0: {FALSE}
|
||||
OUT: + Type environment at (31, 4)
|
||||
OUT: ~dc0: {FALSE}
|
||||
OUT: + Type environment at (31, 14)
|
||||
OUT: ~dc0: {FALSE}
|
||||
OUT: + Type environment at (32, 4)
|
||||
OUT: ~dc0: {FALSE}
|
||||
OUT: + Type environment at (32, 14)
|
||||
OUT: ~dc0: {FALSE}
|
||||
OUT: + Type environment at (33, 4)
|
||||
OUT: + Type environment at (33, 19)
|
||||
OUT: + Type environment at (35, 4)
|
||||
OUT: + Type environment at (35, 15)
|
||||
OUT: + Type environment at (36, 4)
|
||||
OUT: + Type environment at (36, 11)
|
||||
OUT: + Type environment at (37, 4)
|
||||
OUT: + Type environment at (37, 16)
|
||||
OUT: + Type environment at (38, 4)
|
||||
OUT: + Type environment at (38, 14)
|
||||
OUT: + Type environment at (39, 4)
|
||||
OUT: + Type environment at (39, 11)
|
||||
OUT: + Type environment at (40, 4)
|
||||
OUT: + Type environment at (40, 17)
|
||||
OUT: + Type environment at (42, 4)
|
||||
OUT: x: Tree({1..1}, Tree)
|
||||
OUT: ~dc0: Tree + {NIL} + Natural
|
||||
OUT: y: Tree({2..2}, Tree + {NIL} + Natural)
|
||||
OUT: ~dc1: Tree + {NIL} + Natural
|
||||
OUT: ~dc2: Tree + {NIL} + Natural
|
||||
OUT: + Type environment at (42, 9)
|
||||
OUT: x: Tree({1..1}, Tree)
|
||||
OUT: ~dc0: Tree + {NIL} + Natural
|
||||
OUT: y: Tree({2..2}, Tree + {NIL} + Natural)
|
||||
OUT: ~dc1: Tree + {NIL} + Natural
|
||||
OUT: ~dc2: Tree + {NIL} + Natural
|
||||
OUT: + Type environment at (43, 4)
|
||||
OUT: + Type environment at (43, 40)
|
||||
OUT: + Type environment at (44, 4)
|
||||
OUT: x: Tree(Tree, Tree + {NIL} + Natural)
|
||||
OUT: ~dc0: Tree + {NIL} + Natural
|
||||
OUT: y: Tree({2..2}, Tree + {NIL} + Natural)
|
||||
OUT: ~dc1: Tree + {NIL} + Natural
|
||||
OUT: ~dc2: Tree + {NIL} + Natural
|
||||
OUT: ~dc3: Tree + {NIL} + Natural
|
||||
OUT: + Type environment at (44, 9)
|
||||
OUT: x: Tree(Tree, Tree + {NIL} + Natural)
|
||||
OUT: ~dc0: Tree + {NIL} + Natural
|
||||
OUT: y: Tree({2..2}, Tree + {NIL} + Natural)
|
||||
OUT: ~dc1: Tree + {NIL} + Natural
|
||||
OUT: ~dc2: Tree + {NIL} + Natural
|
||||
OUT: ~dc3: Tree + {NIL} + Natural
|
||||
OUT: + Type environment at (45, 4)
|
||||
OUT: x: Tree(Tree(Tree(Tree, Tree + {NIL} + Natural), Tree + {NIL} + Natural), Tree + {NIL} + Natural)
|
||||
OUT: ~dc0: Tree + {NIL} + Natural
|
||||
OUT: y: Tree(Tree({NIL}, Tree + {NIL} + Natural), Tree + {NIL} + Natural)
|
||||
OUT: ~dc1: Tree + {NIL} + Natural
|
||||
OUT: ~sv0: Tree(Tree(Tree, Tree + {NIL} + Natural), Tree + {NIL} + Natural)
|
||||
OUT: ~sv1: Tree + {NIL} + Natural
|
||||
OUT: ~sv2: Tree({NIL}, Tree + {NIL} + Natural)
|
||||
OUT: ~sv3: Tree + {NIL} + Natural
|
||||
OUT: ~sv4: Tree(Tree, Tree + {NIL} + Natural)
|
||||
OUT: ~sv5: Tree + {NIL} + Natural
|
||||
OUT: ~sv6: Tree
|
||||
OUT: ~sv7: Tree + {NIL} + Natural
|
||||
OUT: ~sv8: {NIL}
|
||||
OUT: ~sv9: Tree + {NIL} + Natural
|
||||
OUT: + Type environment at (45, 9)
|
||||
OUT: x: Tree(Tree(Tree(Tree, Tree + {NIL} + Natural), Tree + {NIL} + Natural), Tree + {NIL} + Natural)
|
||||
OUT: ~dc0: Tree + {NIL} + Natural
|
||||
OUT: y: Tree(Tree({NIL}, Tree + {NIL} + Natural), Tree + {NIL} + Natural)
|
||||
OUT: ~dc1: Tree + {NIL} + Natural
|
||||
OUT: ~sv0: Tree(Tree(Tree, Tree + {NIL} + Natural), Tree + {NIL} + Natural)
|
||||
OUT: ~sv1: Tree + {NIL} + Natural
|
||||
OUT: ~sv2: Tree({NIL}, Tree + {NIL} + Natural)
|
||||
OUT: ~sv3: Tree + {NIL} + Natural
|
||||
OUT: ~sv4: Tree(Tree, Tree + {NIL} + Natural)
|
||||
OUT: ~sv5: Tree + {NIL} + Natural
|
||||
OUT: ~sv6: Tree
|
||||
OUT: ~sv7: Tree + {NIL} + Natural
|
||||
OUT: ~sv8: {NIL}
|
||||
OUT: ~sv9: Tree + {NIL} + Natural
|
||||
OUT: + Type environment at (48, 4)
|
||||
OUT: x: B
|
||||
OUT: y: A
|
||||
OUT: + Type environment at (48, 9)
|
||||
OUT: x: B
|
||||
OUT: y: A
|
||||
OUT: + Type environment at (49, 4)
|
||||
OUT: ~dc0: {FALSE}
|
||||
OUT: + Type environment at (49, 11)
|
||||
OUT: ~dc0: {FALSE}
|
||||
OUT: + Type environment at (50, 4)
|
||||
OUT: ~dc0: {FALSE}
|
||||
OUT: + Type environment at (50, 13)
|
||||
OUT: ~dc0: {FALSE}
|
||||
OUT: + Type environment at (51, 4)
|
||||
OUT: ~dc0: {FALSE}
|
||||
OUT: + Type environment at (51, 13)
|
||||
OUT: ~dc0: {FALSE}
|
||||
OUT: + Type environment at (52, 4)
|
||||
OUT: + Type environment at (52, 15)
|
||||
OUT: + Type environment at (57, 4)
|
||||
OUT: x: {1..1000000}
|
||||
OUT: ~dc0: P
|
||||
OUT: y: {1000001..1000001} + {TRUE}
|
||||
OUT: + Type environment at (57, 9)
|
||||
OUT: x: {1..1000000}
|
||||
OUT: ~dc0: P
|
||||
OUT: y: {1000001..1000001} + {TRUE}
|
||||
OUT: + Type environment at (58, 4)
|
||||
OUT: x: {FALSE}
|
||||
OUT: ~dc0: P'({FALSE}, {TRUE})
|
||||
OUT: y: {TRUE}
|
||||
OUT: + Type environment at (58, 9)
|
||||
OUT: x: {FALSE}
|
||||
OUT: ~dc0: P'({FALSE}, {TRUE})
|
||||
OUT: y: {TRUE}
|
||||
OUT: + Type environment at (59, 4)
|
||||
OUT: x: {0..0} + NegInteger
|
||||
OUT: ~dc0: R
|
||||
OUT: y: Natural
|
||||
OUT: + Type environment at (59, 9)
|
||||
OUT: x: {0..0} + NegInteger
|
||||
OUT: ~dc0: R
|
||||
OUT: y: Natural
|
||||
OUT:
|
||||
OUT: []> x
|
||||
OUT:
|
||||
EXIT: 0
|
||||
|
|
@ -0,0 +1,5 @@
|
|||
run: ..\..\..\..\Bld\Drops\Formula_Debug_x86\Formula.exe
|
||||
arg: -v: off -l: "tests.4ml" -dt: "Good" -typ: "Good" -x
|
||||
acc: .\
|
||||
dsc: Rules with inequalities that are SAT.
|
||||
|
||||
|
|
@ -0,0 +1,61 @@
|
|||
domain Base
|
||||
{
|
||||
Cons ::= new (val: Natural, tail: any Cons + { NIL } ).
|
||||
R ::= new (val: NegInteger + { 0 }).
|
||||
B ::= new (val: Boolean).
|
||||
A ::= new (val: { FALSE } ).
|
||||
A' ::= new (val: { TRUE } ).
|
||||
Tree ::= new (lft: any Natural + Tree + { NIL },
|
||||
rt: any Natural + Tree + { NIL } ).
|
||||
F ::= new (any Integer + F).
|
||||
}
|
||||
|
||||
domain Good extends Base
|
||||
{
|
||||
|
||||
q :- TRUE >= FALSE.
|
||||
q :- TRUE >= 1.
|
||||
q :- TRUE >= "TRUE".
|
||||
q :- TRUE >= TRUE.
|
||||
q :- 1 >= 0.
|
||||
q :- "TRUE" >= "FALSE".
|
||||
|
||||
q :- x is Tree(2, _), y is Tree(1, Tree(_, _)), x >= y.
|
||||
q :- Cons(1, Cons(2, Cons(3, Cons(4, NIL)))) >= Cons(1, Cons(2, Cons(3, NIL))).
|
||||
q :- x is Tree(Tree(_, _), _), y is Tree(2, _), x >= y.
|
||||
q :- x is Tree, x.lft.lft.lft = Tree(_,_),
|
||||
y is Tree, y.lft.lft = NIL,
|
||||
x >= y.
|
||||
q :- x is B, y is A, x >= y.
|
||||
q :- A(_) >= 0.
|
||||
q :- A(_) >= "0".
|
||||
q :- A(_) >= NIL.
|
||||
q :- "abcdefg" >= "abc".
|
||||
|
||||
q :- FALSE < TRUE.
|
||||
q :- 1 < TRUE.
|
||||
q :- "TRUE" < TRUE.
|
||||
q :- TRUE <= TRUE.
|
||||
q :- 0 < 1.
|
||||
q :- "FALSE" < "TRUE" .
|
||||
|
||||
q :- x is Tree(1, Tree(_, _)), y is Tree(2, _), x < y.
|
||||
q :- Cons(1, Cons(2, Cons(3, NIL))) < Cons(1, Cons(2, Cons(3, Cons(4, NIL)))).
|
||||
q :- x is Tree(Tree(_, _), _), y is Tree(2, _), y < x.
|
||||
q :- x is Tree, x.lft.lft.lft = Tree(_,_),
|
||||
y is Tree, y.lft.lft = NIL,
|
||||
y < x.
|
||||
q :- x is B, y is A, y < x.
|
||||
q :- 0 < A(_).
|
||||
q :- "0" < A(_).
|
||||
q :- NIL < A(_).
|
||||
q :- "abc" < "abcdefg".
|
||||
|
||||
P ::= ( { 1..1000000 } , { 1000001..1000001, TRUE } ).
|
||||
P' ::= ( { 1..1000000, FALSE } , { 1000001..1000001, TRUE } ).
|
||||
|
||||
q :- P(x, y), x <= y.
|
||||
q :- P'(x, y), or(x,x) < and(y, y).
|
||||
q :- R(x), y = -1*x, x >= y.
|
||||
}
|
||||
|
||||
|
|
@ -0,0 +1,53 @@
|
|||
=================================
|
||||
Console output
|
||||
=================================
|
||||
OUT:
|
||||
OUT: []> v off
|
||||
OUT: verbose off
|
||||
OUT:
|
||||
OUT: []> l tests.4ml
|
||||
OUT: (Failed) tests.4ml
|
||||
OUT: tests.4ml (15, 14): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (16, 14): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (17, 14): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (18, 14): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (19, 11): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (20, 16): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (22, 20): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (23, 49): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (24, 54): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (27, 11): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (28, 27): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (29, 14): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (30, 14): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (31, 14): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (32, 19): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (34, 15): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (35, 11): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (36, 16): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (37, 14): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (38, 11): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (39, 17): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (41, 29): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (42, 40): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (43, 54): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (46, 11): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (47, 27): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (48, 11): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (49, 13): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (50, 13): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (51, 15): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (56, 20): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (57, 27): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (58, 17): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (0, 0): The install operation failed
|
||||
OUT:
|
||||
OUT: []> dt Bad
|
||||
OUT: No module with that name
|
||||
OUT:
|
||||
OUT: []> typ Bad
|
||||
OUT: No module with that name
|
||||
OUT:
|
||||
OUT: []> x
|
||||
OUT:
|
||||
EXIT: 1
|
||||
|
|
@ -0,0 +1,5 @@
|
|||
run: ..\..\..\..\Bld\Drops\Formula_Debug_x86\Formula.exe
|
||||
arg: -v: off -l: "tests.4ml" -dt: "Bad" -typ: "Bad" -x
|
||||
acc: .\
|
||||
dsc: Rules with inequalities that are UNSAT.
|
||||
|
||||
|
|
@ -0,0 +1,60 @@
|
|||
domain Base
|
||||
{
|
||||
Cons ::= new (val: Natural, tail: any Cons + { NIL } ).
|
||||
R ::= new (val: NegInteger + { 0 }).
|
||||
B ::= new (val: Boolean).
|
||||
A ::= new (val: { FALSE } ).
|
||||
A' ::= new (val: { TRUE } ).
|
||||
Tree ::= new (lft: any Natural + Tree + { NIL },
|
||||
rt: any Natural + Tree + { NIL } ).
|
||||
F ::= new (any Integer + F).
|
||||
}
|
||||
|
||||
domain Bad extends Base
|
||||
{
|
||||
q :- TRUE < FALSE.
|
||||
q :- TRUE < 1.
|
||||
q :- TRUE < "TRUE".
|
||||
q :- TRUE < TRUE.
|
||||
q :- 1 < 0.
|
||||
q :- "TRUE" < "FALSE".
|
||||
|
||||
q :- Tree(2, _) < Tree(1, Tree(_, _)).
|
||||
q :- Cons(1, Cons(2, Cons(3, Cons(4, NIL)))) < Cons(1, Cons(2, Cons(3, NIL))).
|
||||
q :- x is Tree(Tree(_, _), _), y is Tree(2, _), x < y.
|
||||
q :- x is Tree, x.lft.lft.lft = Tree(_,_),
|
||||
y is Tree, y.lft.lft = NIL,
|
||||
x < y.
|
||||
q :- x is B, y is A, x < y.
|
||||
q :- A(_) < 0.
|
||||
q :- A(_) < "0".
|
||||
q :- A(_) < NIL.
|
||||
q :- "abcdefg" < "abc".
|
||||
|
||||
q :- FALSE >= TRUE.
|
||||
q :- 1 >= TRUE.
|
||||
q :- "TRUE" >= TRUE.
|
||||
q :- TRUE > TRUE.
|
||||
q :- 0 >= 1.
|
||||
q :- "FALSE" >= "TRUE" .
|
||||
|
||||
q :- Tree(1, Tree(_, _)) >= Tree(2, _).
|
||||
q :- Cons(1, Cons(2, Cons(3, NIL))) >= Cons(1, Cons(2, Cons(3, Cons(4, NIL)))).
|
||||
q :- x is Tree(Tree(_, _), _), y is Tree(2, _), y >= x.
|
||||
q :- x is Tree, x.lft.lft.lft = Tree(_,_),
|
||||
y is Tree, y.lft.lft = NIL,
|
||||
y >= x.
|
||||
q :- x is B, y is A, y >= x.
|
||||
q :- 0 >= A(_).
|
||||
q :- "0" >= A(_).
|
||||
q :- NIL >= A(_).
|
||||
q :- "abc" >= "abcdefg".
|
||||
|
||||
P ::= ( { 1..1000000 } , { 1000001..1000001, TRUE } ).
|
||||
P' ::= ( { 1..1000000, FALSE } , { 1000001..1000001, TRUE } ).
|
||||
|
||||
q :- P(x, y), x > y.
|
||||
q :- P'(x, y), or(x,x) > and(y, y).
|
||||
q :- R(x), x > -1*x.
|
||||
}
|
||||
|
||||
|
|
@ -0,0 +1,191 @@
|
|||
=================================
|
||||
Console output
|
||||
=================================
|
||||
OUT:
|
||||
OUT: []> v off
|
||||
OUT: verbose off
|
||||
OUT:
|
||||
OUT: []> l tests.4ml
|
||||
OUT: (Compiled) tests.4ml
|
||||
OUT:
|
||||
OUT: []> dt Good
|
||||
OUT: Reduced form
|
||||
OUT: domain Good
|
||||
OUT: {
|
||||
OUT: A ::= new (arg1: B).
|
||||
OUT: B ::= new (arg1: C).
|
||||
OUT: C ::= new (arg1: { 1 }).
|
||||
OUT: G ::= (Any).
|
||||
OUT: F1 ::= new (arg1: { 1..50 }, arg2: { 1..50 }).
|
||||
OUT: F2 ::= new (arg1: { 0..50 }, arg2: { 0..50 }).
|
||||
OUT: F3 ::= new (arg1: { -348978933..0, "hello" }, arg2: { 500000..3245345435, blue }, arg3: PosInteger).
|
||||
OUT:
|
||||
OUT: q0
|
||||
OUT: :-
|
||||
OUT: F1(x, y), x = y + 2.
|
||||
OUT:
|
||||
OUT: q1
|
||||
OUT: :-
|
||||
OUT: F2(x, y), 1 - x = x + 1.
|
||||
OUT:
|
||||
OUT: q2
|
||||
OUT: :-
|
||||
OUT: F3(x, y, z), x <= y, x : Real, y : Real.
|
||||
OUT:
|
||||
OUT: q3
|
||||
OUT: :-
|
||||
OUT: F3(x, y, z), x <= z, x : Real.
|
||||
OUT:
|
||||
OUT: q4
|
||||
OUT: :-
|
||||
OUT: x1 = 5 % 3, x2 = 5 % -3, x3 = -5 % 3, x4 = -5 % -3, x5 = 1/2 % 2.
|
||||
OUT:
|
||||
OUT: q5
|
||||
OUT: :-
|
||||
OUT: F3(x, y, z), x : NegInteger.
|
||||
OUT:
|
||||
OUT: q6
|
||||
OUT: :-
|
||||
OUT: x : A.
|
||||
OUT:
|
||||
OUT: q7
|
||||
OUT: :-
|
||||
OUT: G(x), G(y), x = or(x, y), or(or(x, y), y) = or(or(x, y), y).
|
||||
OUT:
|
||||
OUT: q8
|
||||
OUT: :-
|
||||
OUT: G(x), G(y), y / x > 0, x = 1 * x.
|
||||
OUT: }
|
||||
OUT:
|
||||
OUT: Symbol table
|
||||
OUT: Space | Name | Arity | Kind
|
||||
OUT: -------|---------------|-------|-------
|
||||
OUT: | A | 1 | con
|
||||
OUT: | B | 1 | con
|
||||
OUT: | Boolean | 0 | unn
|
||||
OUT: | C | 1 | con
|
||||
OUT: | F1 | 2 | con
|
||||
OUT: | F2 | 2 | con
|
||||
OUT: | F3 | 3 | con
|
||||
OUT: | FALSE | 0 | ncnst
|
||||
OUT: | G | 1 | con
|
||||
OUT: | Integer | 0 | unn
|
||||
OUT: | Natural | 0 | unn
|
||||
OUT: | NegInteger | 0 | unn
|
||||
OUT: | PosInteger | 0 | unn
|
||||
OUT: | Real | 0 | unn
|
||||
OUT: | String | 0 | unn
|
||||
OUT: | TRUE | 0 | ncnst
|
||||
OUT: | blue | 0 | ncnst
|
||||
OUT: Good | Any | 0 | unn
|
||||
OUT: Good | Constant | 0 | unn
|
||||
OUT: Good | Data | 0 | unn
|
||||
OUT: Good | conforms | 0 | dcnst
|
||||
OUT: Good | notFunctional | 0 | dcnst
|
||||
OUT: Good | notInjective | 0 | dcnst
|
||||
OUT: Good | notInvTotal | 0 | dcnst
|
||||
OUT: Good | notRelational | 0 | dcnst
|
||||
OUT: Good | notTotal | 0 | dcnst
|
||||
OUT: Good | q0 | 0 | dcnst
|
||||
OUT: Good | q1 | 0 | dcnst
|
||||
OUT: Good | q2 | 0 | dcnst
|
||||
OUT: Good | q3 | 0 | dcnst
|
||||
OUT: Good | q4 | 0 | dcnst
|
||||
OUT: Good | q5 | 0 | dcnst
|
||||
OUT: Good | q6 | 0 | dcnst
|
||||
OUT: Good | q7 | 0 | dcnst
|
||||
OUT: Good | q8 | 0 | dcnst
|
||||
OUT:
|
||||
OUT: Type constants: #A #A[0] #B #B[0] #Boolean #C #C[0] #F1 #F1[0] #F1[1] #F2 #F2[0] #F2[1] #F3 #F3[0] #F3[1] #F3[2] #G #G[0] #Integer #Natural #NegInteger #PosInteger #Real #String Good.#Any Good.#Constant Good.#Data
|
||||
OUT: Symbolic constants:
|
||||
OUT: Rationals: -348978933 -5 -3 0 1/2 1 2 3 5 50 500000 3245345435
|
||||
OUT: Strings: "hello"
|
||||
OUT: Variables: x x1 x2 x3 x4 x5 y z
|
||||
OUT:
|
||||
OUT: []> typ Good
|
||||
OUT: + Type environment at (10, 5)
|
||||
OUT: ~dc0: F1({3..50}, {1..50})
|
||||
OUT: x: {3..50}
|
||||
OUT: y: {1..50}
|
||||
OUT: + Type environment at (10, 11)
|
||||
OUT: ~dc0: F1({3..50}, {1..50})
|
||||
OUT: x: {3..50}
|
||||
OUT: y: {1..50}
|
||||
OUT: + Type environment at (14, 5)
|
||||
OUT: ~dc0: F2
|
||||
OUT: x: {0..50}
|
||||
OUT: y: {0..50}
|
||||
OUT: + Type environment at (14, 11)
|
||||
OUT: ~dc0: F2
|
||||
OUT: x: {0..50}
|
||||
OUT: y: {0..50}
|
||||
OUT: + Type environment at (18, 5)
|
||||
OUT: ~dc0: F3({-348978933..0}, {500000..3245345435}, PosInteger)
|
||||
OUT: x: {-348978933..0}
|
||||
OUT: y: {500000..3245345435}
|
||||
OUT: z: PosInteger
|
||||
OUT: + Type environment at (18, 11)
|
||||
OUT: ~dc0: F3({-348978933..0}, {500000..3245345435}, PosInteger)
|
||||
OUT: x: {-348978933..0}
|
||||
OUT: y: {500000..3245345435}
|
||||
OUT: z: PosInteger
|
||||
OUT: + Type environment at (20, 5)
|
||||
OUT: ~dc0: F3({-348978933..0}, {500000..3245345435} + {blue}, PosInteger)
|
||||
OUT: x: {-348978933..0}
|
||||
OUT: y: {500000..3245345435} + {blue}
|
||||
OUT: z: PosInteger
|
||||
OUT: + Type environment at (20, 11)
|
||||
OUT: ~dc0: F3({-348978933..0}, {500000..3245345435} + {blue}, PosInteger)
|
||||
OUT: x: {-348978933..0}
|
||||
OUT: y: {500000..3245345435} + {blue}
|
||||
OUT: z: PosInteger
|
||||
OUT: + Type environment at (22, 5)
|
||||
OUT: x1: {2..2}
|
||||
OUT: x2: {2..2}
|
||||
OUT: x3: {1..1}
|
||||
OUT: x4: {1..1}
|
||||
OUT: x5: {1/2}
|
||||
OUT: + Type environment at (22, 14)
|
||||
OUT: x1: {2..2}
|
||||
OUT: x2: {2..2}
|
||||
OUT: x3: {1..1}
|
||||
OUT: x4: {1..1}
|
||||
OUT: x5: {1/2}
|
||||
OUT: + Type environment at (28, 4)
|
||||
OUT: ~dc0: F3({-348978933..-1}, {500000..3245345435} + {blue}, PosInteger)
|
||||
OUT: x: {-348978933..-1}
|
||||
OUT: y: {500000..3245345435} + {blue}
|
||||
OUT: z: PosInteger
|
||||
OUT: + Type environment at (28, 10)
|
||||
OUT: ~dc0: F3({-348978933..-1}, {500000..3245345435} + {blue}, PosInteger)
|
||||
OUT: x: {-348978933..-1}
|
||||
OUT: y: {500000..3245345435} + {blue}
|
||||
OUT: z: PosInteger
|
||||
OUT: + Type environment at (30, 4)
|
||||
OUT: x: A
|
||||
OUT: + Type environment at (30, 12)
|
||||
OUT: x: A
|
||||
OUT: + Type environment at (32, 4)
|
||||
OUT: ~dc0: G({FALSE} + {TRUE})
|
||||
OUT: x: {FALSE} + {TRUE}
|
||||
OUT: y: {FALSE} + {TRUE}
|
||||
OUT: ~dc1: G({FALSE} + {TRUE})
|
||||
OUT: + Type environment at (32, 10)
|
||||
OUT: ~dc0: G({FALSE} + {TRUE})
|
||||
OUT: x: {FALSE} + {TRUE}
|
||||
OUT: y: {FALSE} + {TRUE}
|
||||
OUT: ~dc1: G({FALSE} + {TRUE})
|
||||
OUT: + Type environment at (34, 4)
|
||||
OUT: ~dc0: G(Real)
|
||||
OUT: x: Real
|
||||
OUT: y: Real
|
||||
OUT: ~dc1: G(Real)
|
||||
OUT: + Type environment at (34, 10)
|
||||
OUT: ~dc0: G(Real)
|
||||
OUT: x: Real
|
||||
OUT: y: Real
|
||||
OUT: ~dc1: G(Real)
|
||||
OUT:
|
||||
OUT: []> x
|
||||
OUT:
|
||||
EXIT: 0
|
||||
|
|
@ -0,0 +1,4 @@
|
|||
run: ..\..\..\..\Bld\Drops\Formula_Debug_x86\Formula.exe
|
||||
arg: -v: off -l: "tests.4ml" -dt: "Good" -typ: "Good" -x
|
||||
acc: .\
|
||||
dsc: Rules for which constraints on interpreted functions are SAT
|
||||
|
|
@ -0,0 +1,35 @@
|
|||
domain Good
|
||||
{
|
||||
A ::= new (arg1: B).
|
||||
B ::= new (arg1: C).
|
||||
C ::= new (arg1: { 1 }).
|
||||
G ::= (Any).
|
||||
|
||||
F1 ::= new (arg1: { 1..50 }, arg2: { 1..50 } ).
|
||||
|
||||
q0 :- F1(x, y), x = y + 2.
|
||||
|
||||
F2 ::= new (arg1: { 0..50 }, arg2: { 0..50 } ).
|
||||
|
||||
q1 :- F2(x, y), 1 - x = x + 1.
|
||||
|
||||
F3 ::= new (arg1: { -348978933..0, "hello" }, arg2: { 500000..3245345435, blue }, arg3: PosInteger).
|
||||
|
||||
q2 :- F3(x, y, z), x <= y, x : Real, y : Real.
|
||||
|
||||
q3 :- F3(x, y, z), x <= z, x : Real.
|
||||
|
||||
q4 :- x1 = 5 % 3,
|
||||
x2 = 5 % -3,
|
||||
x3 = -5 % 3,
|
||||
x4 = -5 % -3,
|
||||
x5 = (1/2) % 2.
|
||||
|
||||
q5 :- F3(x, y, z), x : NegInteger.
|
||||
|
||||
q6 :- x : A.
|
||||
|
||||
q7 :- G(x), G(y), x = or(x, y), or(or(x, y), y) = or(or(x, y), y).
|
||||
|
||||
q8 :- G(x), G(y), y / x > 0, x = 1*x.
|
||||
}
|
||||
|
|
@ -0,0 +1,24 @@
|
|||
=================================
|
||||
Console output
|
||||
=================================
|
||||
OUT:
|
||||
OUT: []> v off
|
||||
OUT: verbose off
|
||||
OUT:
|
||||
OUT: []> l tests.4ml
|
||||
OUT: (Failed) tests.4ml
|
||||
OUT: tests.4ml (17, 23): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (19, 27): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (23, 26): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (25, 26): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (27, 26): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (29, 18): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (31, 41): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (33, 17): Argument 2 of function + is badly typed.
|
||||
OUT: tests.4ml (35, 15): Syntax error - or got 3 arguments but needs 2
|
||||
OUT: tests.4ml (37, 13): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (0, 0): The install operation failed
|
||||
OUT:
|
||||
OUT: []> x
|
||||
OUT:
|
||||
EXIT: 1
|
||||
|
|
@ -0,0 +1,4 @@
|
|||
run: ..\..\..\..\Bld\Drops\Formula_Debug_x86\Formula.exe
|
||||
arg: -v: off -l: "tests.4ml" -x
|
||||
acc: .\
|
||||
dsc: Rules for which constraints on interpreted functions are UNSAT
|
||||
|
|
@ -0,0 +1,38 @@
|
|||
domain Base
|
||||
{
|
||||
Cons ::= new (val: Natural, tail: any Cons + { NIL } ).
|
||||
R ::= new (val: NegInteger + { 0 }).
|
||||
B ::= new (val: Boolean).
|
||||
A ::= new (val: { FALSE } ).
|
||||
A' ::= new (val: { TRUE } ).
|
||||
Tree ::= new (lft: any Natural + Tree + { NIL },
|
||||
rt: any Natural + Tree + { NIL } ).
|
||||
F ::= new (any Integer + F).
|
||||
}
|
||||
|
||||
domain Bad extends Base
|
||||
{
|
||||
F2 ::= new (arg1: { 1..50 }, arg2: { 1..50 } ).
|
||||
|
||||
q0 :- F2(x, y), x = x + 2.
|
||||
|
||||
q1 :- F2(x, y), 1 - x = x + 1.
|
||||
|
||||
F3 ::= new (arg1: { -348978933..0 }, arg2: { 500000..3245345435 }, arg3: PosInteger).
|
||||
|
||||
q2 :- F3(x, y, z), x >= y.
|
||||
|
||||
q3 :- F3(x, y, z), x >= z.
|
||||
|
||||
q4 :- F3(x, y, z), x : PosInteger.
|
||||
|
||||
q5 :- x.arg1 = x.arg2 + 1, x : F3.
|
||||
|
||||
q6 :- x = or(x, y), or(or(x, y), y) != x.
|
||||
|
||||
q7 :- x = y + "hello".
|
||||
|
||||
q8 :- x = or(a,b,c).
|
||||
|
||||
q9 :- y / x > 0, x = 0*x.
|
||||
}
|
||||
|
|
@ -0,0 +1,64 @@
|
|||
=================================
|
||||
Console output
|
||||
=================================
|
||||
OUT:
|
||||
OUT: []> v off
|
||||
OUT: verbose off
|
||||
OUT:
|
||||
OUT: []> l tests.4ml
|
||||
OUT: (Compiled) tests.4ml
|
||||
OUT:
|
||||
OUT: []> dt Widened
|
||||
OUT: Reduced form
|
||||
OUT: domain Widened
|
||||
OUT: {
|
||||
OUT: F1 ::= new (arg1: { 1..500000 }, arg2: { 1..50 }).
|
||||
OUT:
|
||||
OUT: q0
|
||||
OUT: :-
|
||||
OUT: F1(x, y), x = x + 2.
|
||||
OUT: }
|
||||
OUT:
|
||||
OUT: Symbol table
|
||||
OUT: Space | Name | Arity | Kind
|
||||
OUT: ---------|---------------|-------|-------
|
||||
OUT: | Boolean | 0 | unn
|
||||
OUT: | F1 | 2 | con
|
||||
OUT: | FALSE | 0 | ncnst
|
||||
OUT: | Integer | 0 | unn
|
||||
OUT: | Natural | 0 | unn
|
||||
OUT: | NegInteger | 0 | unn
|
||||
OUT: | PosInteger | 0 | unn
|
||||
OUT: | Real | 0 | unn
|
||||
OUT: | String | 0 | unn
|
||||
OUT: | TRUE | 0 | ncnst
|
||||
OUT: Widened | Any | 0 | unn
|
||||
OUT: Widened | Constant | 0 | unn
|
||||
OUT: Widened | Data | 0 | unn
|
||||
OUT: Widened | conforms | 0 | dcnst
|
||||
OUT: Widened | notFunctional | 0 | dcnst
|
||||
OUT: Widened | notInjective | 0 | dcnst
|
||||
OUT: Widened | notInvTotal | 0 | dcnst
|
||||
OUT: Widened | notRelational | 0 | dcnst
|
||||
OUT: Widened | notTotal | 0 | dcnst
|
||||
OUT: Widened | q0 | 0 | dcnst
|
||||
OUT:
|
||||
OUT: Type constants: #Boolean #F1 #F1[0] #F1[1] #Integer #Natural #NegInteger #PosInteger #Real #String Widened.#Any Widened.#Constant Widened.#Data
|
||||
OUT: Symbolic constants:
|
||||
OUT: Rationals: 1 2 50 500000
|
||||
OUT: Strings:
|
||||
OUT: Variables: x y
|
||||
OUT:
|
||||
OUT: []> typ Widened
|
||||
OUT: + Type environment at (5, 5)
|
||||
OUT: ~dc0: F1
|
||||
OUT: x: {1..500000}
|
||||
OUT: y: {1..50}
|
||||
OUT: + Type environment at (5, 11)
|
||||
OUT: ~dc0: F1
|
||||
OUT: x: {1..500000}
|
||||
OUT: y: {1..50}
|
||||
OUT:
|
||||
OUT: []> x
|
||||
OUT:
|
||||
EXIT: 0
|
||||
|
|
@ -0,0 +1,4 @@
|
|||
run: ..\..\..\..\Bld\Drops\Formula_Debug_x86\Formula.exe
|
||||
arg: -v: off -l: "tests.4ml" -dt: "Widened" -typ: "Widened" -x
|
||||
acc: .\
|
||||
dsc: Rules for which constraints unsat this is undetectable (WIDENED)
|
||||
|
|
@ -0,0 +1,6 @@
|
|||
domain Widened
|
||||
{
|
||||
F1 ::= new (arg1: { 1..500000 }, arg2: { 1..50 } ).
|
||||
|
||||
q0 :- F1(x, y), x = x + 2. //// Misses the error because of widening.
|
||||
}
|
||||
|
|
@ -0,0 +1,234 @@
|
|||
=================================
|
||||
Console output
|
||||
=================================
|
||||
OUT:
|
||||
OUT: []> v off
|
||||
OUT: verbose off
|
||||
OUT:
|
||||
OUT: []> l tests.4ml
|
||||
OUT: (Compiled) tests.4ml
|
||||
OUT:
|
||||
OUT: []> dt ConvTypes
|
||||
OUT: Reduced form
|
||||
OUT: domain ConvTypes
|
||||
OUT: {
|
||||
OUT: F ::= new (Integer).
|
||||
OUT: G ::= (Integer).
|
||||
OUT:
|
||||
OUT: q0
|
||||
OUT: :-
|
||||
OUT: x is Any.
|
||||
OUT:
|
||||
OUT: q1
|
||||
OUT: :-
|
||||
OUT: x is Data.
|
||||
OUT:
|
||||
OUT: q3
|
||||
OUT: :-
|
||||
OUT: _ is Any;
|
||||
OUT: _ is Data.
|
||||
OUT:
|
||||
OUT: q4
|
||||
OUT: :-
|
||||
OUT: x is Any;
|
||||
OUT: x is Data.
|
||||
OUT: }
|
||||
OUT:
|
||||
OUT: Symbol table
|
||||
OUT: Space | Name | Arity | Kind
|
||||
OUT: -----------|---------------|-------|-------
|
||||
OUT: | Boolean | 0 | unn
|
||||
OUT: | F | 1 | con
|
||||
OUT: | FALSE | 0 | ncnst
|
||||
OUT: | G | 1 | con
|
||||
OUT: | Integer | 0 | unn
|
||||
OUT: | Natural | 0 | unn
|
||||
OUT: | NegInteger | 0 | unn
|
||||
OUT: | PosInteger | 0 | unn
|
||||
OUT: | Real | 0 | unn
|
||||
OUT: | String | 0 | unn
|
||||
OUT: | TRUE | 0 | ncnst
|
||||
OUT: ConvTypes | Any | 0 | unn
|
||||
OUT: ConvTypes | Constant | 0 | unn
|
||||
OUT: ConvTypes | Data | 0 | unn
|
||||
OUT: ConvTypes | conforms | 0 | dcnst
|
||||
OUT: ConvTypes | notFunctional | 0 | dcnst
|
||||
OUT: ConvTypes | notInjective | 0 | dcnst
|
||||
OUT: ConvTypes | notInvTotal | 0 | dcnst
|
||||
OUT: ConvTypes | notRelational | 0 | dcnst
|
||||
OUT: ConvTypes | notTotal | 0 | dcnst
|
||||
OUT: ConvTypes | q0 | 0 | dcnst
|
||||
OUT: ConvTypes | q1 | 0 | dcnst
|
||||
OUT: ConvTypes | q3 | 0 | dcnst
|
||||
OUT: ConvTypes | q4 | 0 | dcnst
|
||||
OUT:
|
||||
OUT: Type constants: #Boolean #F #F[0] #G #G[0] #Integer #Natural #NegInteger #PosInteger #Real #String ConvTypes.#Any ConvTypes.#Constant ConvTypes.#Data
|
||||
OUT: Symbolic constants:
|
||||
OUT: Rationals:
|
||||
OUT: Strings:
|
||||
OUT: Variables: x
|
||||
OUT:
|
||||
OUT: []> typ ConvTypes
|
||||
OUT: + Type environment at (6, 3)
|
||||
OUT: x: {ConvTypes.notInvTotal} + {ConvTypes.notTotal} + {ConvTypes.notInjective} + {ConvTypes.notFunctional} + {ConvTypes.notRelational} + {ConvTypes.conforms} + {ConvTypes.q4} + {ConvTypes.q3} + {ConvTypes.q1} + {ConvTypes.q0} + G + F
|
||||
OUT: + Type environment at (6, 9)
|
||||
OUT: x: {ConvTypes.notInvTotal} + {ConvTypes.notTotal} + {ConvTypes.notInjective} + {ConvTypes.notFunctional} + {ConvTypes.notRelational} + {ConvTypes.conforms} + {ConvTypes.q4} + {ConvTypes.q3} + {ConvTypes.q1} + {ConvTypes.q0} + G + F
|
||||
OUT: + Type environment at (7, 3)
|
||||
OUT: x: F
|
||||
OUT: + Type environment at (7, 9)
|
||||
OUT: x: F
|
||||
OUT: + Type environment at (9, 3)
|
||||
OUT: ~dc2: {ConvTypes.notInvTotal} + {ConvTypes.notTotal} + {ConvTypes.notInjective} + {ConvTypes.notFunctional} + {ConvTypes.notRelational} + {ConvTypes.conforms} + {ConvTypes.q4} + {ConvTypes.q3} + {ConvTypes.q1} + {ConvTypes.q0} + G + F
|
||||
OUT: + Type environment at (9, 9)
|
||||
OUT: ~dc2: {ConvTypes.notInvTotal} + {ConvTypes.notTotal} + {ConvTypes.notInjective} + {ConvTypes.notFunctional} + {ConvTypes.notRelational} + {ConvTypes.conforms} + {ConvTypes.q4} + {ConvTypes.q3} + {ConvTypes.q1} + {ConvTypes.q0} + G + F
|
||||
OUT: + Type environment at (10, 9)
|
||||
OUT: ~dc2: F
|
||||
OUT: + Type environment at (12, 3)
|
||||
OUT: x: {ConvTypes.notInvTotal} + {ConvTypes.notTotal} + {ConvTypes.notInjective} + {ConvTypes.notFunctional} + {ConvTypes.notRelational} + {ConvTypes.conforms} + {ConvTypes.q4} + {ConvTypes.q3} + {ConvTypes.q1} + {ConvTypes.q0} + G + F
|
||||
OUT: + Type environment at (12, 9)
|
||||
OUT: x: {ConvTypes.notInvTotal} + {ConvTypes.notTotal} + {ConvTypes.notInjective} + {ConvTypes.notFunctional} + {ConvTypes.notRelational} + {ConvTypes.conforms} + {ConvTypes.q4} + {ConvTypes.q3} + {ConvTypes.q1} + {ConvTypes.q0} + G + F
|
||||
OUT: + Type environment at (13, 9)
|
||||
OUT: x: F
|
||||
OUT:
|
||||
OUT: []> dt Good
|
||||
OUT: Reduced form
|
||||
OUT: domain Good
|
||||
OUT: {
|
||||
OUT: F0 ::= new (x: NegInteger, y: Real).
|
||||
OUT: F1 ::= new (x: NegInteger + { "hello" }, y: String).
|
||||
OUT: F2 ::= new (x: Boolean, y: String + { TRUE }).
|
||||
OUT: F3 ::= new (x: { 1..1000 }, y: { "hello", RED, 1 }).
|
||||
OUT:
|
||||
OUT: q0
|
||||
OUT: :-
|
||||
OUT: F0(x, x).
|
||||
OUT:
|
||||
OUT: q1
|
||||
OUT: :-
|
||||
OUT: F1(x, x).
|
||||
OUT:
|
||||
OUT: q2
|
||||
OUT: :-
|
||||
OUT: F2(x, x).
|
||||
OUT:
|
||||
OUT: q3
|
||||
OUT: :-
|
||||
OUT: F3(x, x).
|
||||
OUT: }
|
||||
OUT:
|
||||
OUT: Symbol table
|
||||
OUT: Space | Name | Arity | Kind
|
||||
OUT: -------|---------------|-------|-------
|
||||
OUT: | Boolean | 0 | unn
|
||||
OUT: | F0 | 2 | con
|
||||
OUT: | F1 | 2 | con
|
||||
OUT: | F2 | 2 | con
|
||||
OUT: | F3 | 2 | con
|
||||
OUT: | FALSE | 0 | ncnst
|
||||
OUT: | Integer | 0 | unn
|
||||
OUT: | Natural | 0 | unn
|
||||
OUT: | NegInteger | 0 | unn
|
||||
OUT: | PosInteger | 0 | unn
|
||||
OUT: | RED | 0 | ncnst
|
||||
OUT: | Real | 0 | unn
|
||||
OUT: | String | 0 | unn
|
||||
OUT: | TRUE | 0 | ncnst
|
||||
OUT: Good | Any | 0 | unn
|
||||
OUT: Good | Constant | 0 | unn
|
||||
OUT: Good | Data | 0 | unn
|
||||
OUT: Good | conforms | 0 | dcnst
|
||||
OUT: Good | notFunctional | 0 | dcnst
|
||||
OUT: Good | notInjective | 0 | dcnst
|
||||
OUT: Good | notInvTotal | 0 | dcnst
|
||||
OUT: Good | notRelational | 0 | dcnst
|
||||
OUT: Good | notTotal | 0 | dcnst
|
||||
OUT: Good | q0 | 0 | dcnst
|
||||
OUT: Good | q1 | 0 | dcnst
|
||||
OUT: Good | q2 | 0 | dcnst
|
||||
OUT: Good | q3 | 0 | dcnst
|
||||
OUT:
|
||||
OUT: Type constants: #Boolean #F0 #F0[0] #F0[1] #F1 #F1[0] #F1[1] #F2 #F2[0] #F2[1] #F3 #F3[0] #F3[1] #Integer #Natural #NegInteger #PosInteger #Real #String Good.#Any Good.#Constant Good.#Data
|
||||
OUT: Symbolic constants:
|
||||
OUT: Rationals: 1 1000
|
||||
OUT: Strings: "hello"
|
||||
OUT: Variables: x
|
||||
OUT:
|
||||
OUT: []> typ Good
|
||||
OUT: + Type environment at (19, 4)
|
||||
OUT: ~dc0: F0(NegInteger, NegInteger)
|
||||
OUT: x: NegInteger
|
||||
OUT: + Type environment at (19, 10)
|
||||
OUT: ~dc0: F0(NegInteger, NegInteger)
|
||||
OUT: x: NegInteger
|
||||
OUT: + Type environment at (22, 4)
|
||||
OUT: ~dc0: F1({"hello"} + NegInteger, {"hello"})
|
||||
OUT: x: {"hello"}
|
||||
OUT: + Type environment at (22, 10)
|
||||
OUT: ~dc0: F1({"hello"} + NegInteger, {"hello"})
|
||||
OUT: x: {"hello"}
|
||||
OUT: + Type environment at (25, 4)
|
||||
OUT: ~dc0: F2({FALSE} + {TRUE}, {TRUE})
|
||||
OUT: x: {TRUE}
|
||||
OUT: + Type environment at (25, 10)
|
||||
OUT: ~dc0: F2({FALSE} + {TRUE}, {TRUE})
|
||||
OUT: x: {TRUE}
|
||||
OUT: + Type environment at (28, 4)
|
||||
OUT: ~dc0: F3({1..1}, {1..1})
|
||||
OUT: x: {1..1}
|
||||
OUT: + Type environment at (28, 10)
|
||||
OUT: ~dc0: F3({1..1}, {1..1})
|
||||
OUT: x: {1..1}
|
||||
OUT:
|
||||
OUT: []> dt Facts
|
||||
OUT: Reduced form
|
||||
OUT: domain Facts
|
||||
OUT: {
|
||||
OUT: T ::= new (left: any T + Natural, right: any T + Natural).
|
||||
OUT:
|
||||
OUT: T(1, 2).
|
||||
OUT:
|
||||
OUT: T(T(1, 2), T(3, 4)).
|
||||
OUT:
|
||||
OUT: T(T(0, T(0, 0)), 0).
|
||||
OUT: }
|
||||
OUT:
|
||||
OUT: Symbol table
|
||||
OUT: Space | Name | Arity | Kind
|
||||
OUT: -------|---------------|-------|-------
|
||||
OUT: | Boolean | 0 | unn
|
||||
OUT: | FALSE | 0 | ncnst
|
||||
OUT: | Integer | 0 | unn
|
||||
OUT: | Natural | 0 | unn
|
||||
OUT: | NegInteger | 0 | unn
|
||||
OUT: | PosInteger | 0 | unn
|
||||
OUT: | Real | 0 | unn
|
||||
OUT: | String | 0 | unn
|
||||
OUT: | T | 2 | con
|
||||
OUT: | TRUE | 0 | ncnst
|
||||
OUT: Facts | Any | 0 | unn
|
||||
OUT: Facts | Constant | 0 | unn
|
||||
OUT: Facts | Data | 0 | unn
|
||||
OUT: Facts | conforms | 0 | dcnst
|
||||
OUT: Facts | notFunctional | 0 | dcnst
|
||||
OUT: Facts | notInjective | 0 | dcnst
|
||||
OUT: Facts | notInvTotal | 0 | dcnst
|
||||
OUT: Facts | notRelational | 0 | dcnst
|
||||
OUT: Facts | notTotal | 0 | dcnst
|
||||
OUT:
|
||||
OUT: Type constants: #Boolean #Integer #Natural #NegInteger #PosInteger #Real #String #T #T[0] #T[1] Facts.#Any Facts.#Constant Facts.#Data
|
||||
OUT: Symbolic constants:
|
||||
OUT: Rationals: 0 1 2 3 4
|
||||
OUT: Strings:
|
||||
OUT: Variables:
|
||||
OUT:
|
||||
OUT: []> typ Facts
|
||||
OUT: + Type environment at (35, 4)
|
||||
OUT: + Type environment at (35, 4)
|
||||
OUT: + Type environment at (36, 4)
|
||||
OUT: + Type environment at (36, 4)
|
||||
OUT: + Type environment at (37, 4)
|
||||
OUT: + Type environment at (37, 4)
|
||||
OUT:
|
||||
OUT: []> x
|
||||
OUT:
|
||||
EXIT: 0
|
||||
|
|
@ -0,0 +1,8 @@
|
|||
run: ..\..\..\..\Bld\Drops\Formula_Debug_x86\Formula.exe
|
||||
arg: -v: off -l: "tests.4ml"
|
||||
arg: -dt: "ConvTypes" -typ: "ConvTypes"
|
||||
arg: -dt: "Good" -typ: "Good"
|
||||
arg: -dt: "Facts" -typ: "Facts"
|
||||
arg: -x
|
||||
acc: .\
|
||||
dsc: Rules for which various type constraints are SAT
|
||||
|
|
@ -0,0 +1,38 @@
|
|||
domain ConvTypes
|
||||
{
|
||||
F ::= new (Integer).
|
||||
G ::= (Integer).
|
||||
|
||||
q0 :- x is Any.
|
||||
q1 :- x is Data.
|
||||
|
||||
q3 :- _ is Any;
|
||||
_ is Data.
|
||||
|
||||
q4 :- x is Any;
|
||||
x is Data.
|
||||
}
|
||||
|
||||
domain Good
|
||||
{
|
||||
F0 ::= new (x: NegInteger, y: Real).
|
||||
q0 :- F0(x, x).
|
||||
|
||||
F1 ::= new (x: NegInteger + { "hello" }, y: String).
|
||||
q1 :- F1(x, x).
|
||||
|
||||
F2 ::= new (x: Boolean, y: String + { TRUE }).
|
||||
q2 :- F2(x, x).
|
||||
|
||||
F3 ::= new (x: { 1..1000 }, y: { "hello", RED, 1 }).
|
||||
q3 :- F3(x, x).
|
||||
}
|
||||
|
||||
domain Facts
|
||||
{
|
||||
T ::= new (left: any T + Natural, right: any T + Natural).
|
||||
|
||||
T(1, 2).
|
||||
T(T(1, 2), T(3, 4)).
|
||||
T(T(0, T(0, 0)), 0).
|
||||
}
|
||||
|
|
@ -0,0 +1,23 @@
|
|||
=================================
|
||||
Console output
|
||||
=================================
|
||||
OUT:
|
||||
OUT: []> v off
|
||||
OUT: verbose off
|
||||
OUT:
|
||||
OUT: []> l tests.4ml
|
||||
OUT: (Failed) tests.4ml
|
||||
OUT: tests.4ml (4, 21): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (5, 9): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (6, 9): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (9, 9): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (10, 9): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (16, 10): Argument 2 of function F0 is badly typed.
|
||||
OUT: tests.4ml (19, 10): Argument 2 of function F1 is badly typed.
|
||||
OUT: tests.4ml (22, 10): Argument 2 of function F2 is badly typed.
|
||||
OUT: tests.4ml (25, 10): Argument 2 of function F3 is badly typed.
|
||||
OUT: tests.4ml (0, 0): The install operation failed
|
||||
OUT:
|
||||
OUT: []> x
|
||||
OUT:
|
||||
EXIT: 1
|
||||
|
|
@ -0,0 +1,4 @@
|
|||
run: ..\..\..\..\Bld\Drops\Formula_Debug_x86\Formula.exe
|
||||
arg: -v: off -l: "tests.4ml" -x
|
||||
acc: .\
|
||||
dsc: Rules for which various type constraints are UNSAT
|
||||
|
|
@ -0,0 +1,26 @@
|
|||
//// Unsatisfiable because finds only accept constructors.
|
||||
domain EmptyConvenienceTypes
|
||||
{
|
||||
q0 :- x is Any, x = 0.
|
||||
q1 :- x is Data.
|
||||
q2 :- x is Constant.
|
||||
|
||||
q3 :- _ is Any;
|
||||
_ is Data;
|
||||
_ is Constant.
|
||||
}
|
||||
|
||||
domain TypeErrors
|
||||
{
|
||||
F0 ::= new (x: NegInteger, y: PosInteger).
|
||||
q0 :- F0(x, x).
|
||||
|
||||
F1 ::= new (x: NegInteger, y: String).
|
||||
q1 :- F1(x, x).
|
||||
|
||||
F2 ::= new (x: Boolean, y: String).
|
||||
q2 :- F2(x, x).
|
||||
|
||||
F3 ::= new (x: { 1..1000 }, y: { "hello", red, 0 }).
|
||||
q3 :- F3(x, x).
|
||||
}
|
||||
|
|
@ -0,0 +1,424 @@
|
|||
=================================
|
||||
Console output
|
||||
=================================
|
||||
OUT:
|
||||
OUT: []> v off
|
||||
OUT: verbose off
|
||||
OUT:
|
||||
OUT: []> l tests.4ml
|
||||
OUT: (Compiled) tests.4ml
|
||||
OUT:
|
||||
OUT: []> dt Good
|
||||
OUT: Reduced form
|
||||
OUT: domain Good extends Base
|
||||
OUT: {
|
||||
OUT: G ::= (Good.Any).
|
||||
OUT:
|
||||
OUT: q0
|
||||
OUT: :-
|
||||
OUT: G(z), Tree(x, y) = z.
|
||||
OUT:
|
||||
OUT: q1
|
||||
OUT: :-
|
||||
OUT: G(x), x = Cons(a, y), y = Cons(b, z).
|
||||
OUT:
|
||||
OUT: q2
|
||||
OUT: :-
|
||||
OUT: G(x), Tree(x, x) = Tree(y, Tree(z, z)).
|
||||
OUT:
|
||||
OUT: q3
|
||||
OUT: :-
|
||||
OUT: Tree(x, Tree(y, y)), z = Cons(y, x).
|
||||
OUT:
|
||||
OUT: q4
|
||||
OUT: :-
|
||||
OUT: G(x), Tree(x, y) = Tree(y, x), x = Tree(z, z).
|
||||
OUT:
|
||||
OUT: q5
|
||||
OUT: :-
|
||||
OUT: G(x0), x0 = Cons(0, x1), x1 = Cons(1, x2), x2 = Cons(2, x3), x3 = Cons(3, x4), x4 = Cons(4, x5), x5 = Cons(5, x6), x6 = Cons(6, x7), x7 = Cons(7, x8), x8 = Cons(8, x9), x9 = Cons(9, x10), x10 = Cons(10, x11), x11 = Cons(11, x12), x12 = Cons(12, x13), x13 = Cons(13, x14), x14 = Cons(14, x15), x15 = Cons(15, x16), x16 = Cons(16, x17), x17 = Cons(17, x18), x18 = Cons(18, x19), x19 = Cons(19, x20), x20 = Cons(20, x21), x21 = Cons(21, x22).
|
||||
OUT:
|
||||
OUT: q6
|
||||
OUT: :-
|
||||
OUT: G(z), Tree(1, Tree(2, NIL)) = x, Tree(2, Tree(z, NIL)) = y.
|
||||
OUT:
|
||||
OUT: q7
|
||||
OUT: :-
|
||||
OUT: x = Cons(0, Cons(1, Cons(2, Cons(3, Cons(4, Cons(5, Cons(6, Cons(7, Cons(8, Cons(9, Cons(10, Cons(11, Cons(12, Cons(13, Cons(14, Cons(15, Cons(16, Cons(17, Cons(18, Cons(19, Cons(20, Cons(21, NIL)))))))))))))))))))))).
|
||||
OUT:
|
||||
OUT: q8
|
||||
OUT: :-
|
||||
OUT: Tree(x, y), x = Tree(z, z), y = Tree(x, x), z = 3.
|
||||
OUT:
|
||||
OUT: q9
|
||||
OUT: :-
|
||||
OUT: A(FALSE) = A(FALSE).
|
||||
OUT:
|
||||
OUT: q10
|
||||
OUT: :-
|
||||
OUT: x = 1, x = y, y = 1.
|
||||
OUT:
|
||||
OUT: q11
|
||||
OUT: :-
|
||||
OUT: x = F(y), x = F(z), y = F(y'), y = F(z'), z' = y', G(y').
|
||||
OUT:
|
||||
OUT: q12
|
||||
OUT: :-
|
||||
OUT: G(x), x.lft.rt.lft.rt = y.
|
||||
OUT:
|
||||
OUT: q13
|
||||
OUT: :-
|
||||
OUT: G(x), G(y), x.lft.rt = y.rt, y.rt = x.lft.rt.
|
||||
OUT:
|
||||
OUT: q14
|
||||
OUT: :-
|
||||
OUT: x.lft = Tree(z, Tree(z', z')), y.lft = Tree(w, w), x = y, G(x).
|
||||
OUT:
|
||||
OUT: q15
|
||||
OUT: :-
|
||||
OUT: G(x), G(y), x.val = y.val, x != y.
|
||||
OUT:
|
||||
OUT: q16
|
||||
OUT: :-
|
||||
OUT: A(_), A'(_).
|
||||
OUT:
|
||||
OUT: q17
|
||||
OUT: :-
|
||||
OUT: x is R(y).
|
||||
OUT:
|
||||
OUT: q18
|
||||
OUT: :-
|
||||
OUT: Tree(_, _).
|
||||
OUT:
|
||||
OUT: q19
|
||||
OUT: :-
|
||||
OUT: x is Good.Data.
|
||||
OUT: }
|
||||
OUT:
|
||||
OUT: Symbol table
|
||||
OUT: Space | Name | Arity | Kind
|
||||
OUT: -------|---------------|-------|-------
|
||||
OUT: | A | 1 | con
|
||||
OUT: | A' | 1 | con
|
||||
OUT: | B | 1 | con
|
||||
OUT: | Boolean | 0 | unn
|
||||
OUT: | Cons | 2 | con
|
||||
OUT: | F | 1 | con
|
||||
OUT: | FALSE | 0 | ncnst
|
||||
OUT: | G | 1 | con
|
||||
OUT: | Integer | 0 | unn
|
||||
OUT: | NIL | 0 | ncnst
|
||||
OUT: | Natural | 0 | unn
|
||||
OUT: | NegInteger | 0 | unn
|
||||
OUT: | PosInteger | 0 | unn
|
||||
OUT: | R | 1 | con
|
||||
OUT: | Real | 0 | unn
|
||||
OUT: | String | 0 | unn
|
||||
OUT: | TRUE | 0 | ncnst
|
||||
OUT: | Tree | 2 | con
|
||||
OUT: Base | Any | 0 | unn
|
||||
OUT: Base | Constant | 0 | unn
|
||||
OUT: Base | Data | 0 | unn
|
||||
OUT: Base | conforms | 0 | dcnst
|
||||
OUT: Base | notFunctional | 0 | dcnst
|
||||
OUT: Base | notInjective | 0 | dcnst
|
||||
OUT: Base | notInvTotal | 0 | dcnst
|
||||
OUT: Base | notRelational | 0 | dcnst
|
||||
OUT: Base | notTotal | 0 | dcnst
|
||||
OUT: Good | Any | 0 | unn
|
||||
OUT: Good | Constant | 0 | unn
|
||||
OUT: Good | Data | 0 | unn
|
||||
OUT: Good | conforms | 0 | dcnst
|
||||
OUT: Good | notFunctional | 0 | dcnst
|
||||
OUT: Good | notInjective | 0 | dcnst
|
||||
OUT: Good | notInvTotal | 0 | dcnst
|
||||
OUT: Good | notRelational | 0 | dcnst
|
||||
OUT: Good | notTotal | 0 | dcnst
|
||||
OUT: Good | q0 | 0 | dcnst
|
||||
OUT: Good | q1 | 0 | dcnst
|
||||
OUT: Good | q10 | 0 | dcnst
|
||||
OUT: Good | q11 | 0 | dcnst
|
||||
OUT: Good | q12 | 0 | dcnst
|
||||
OUT: Good | q13 | 0 | dcnst
|
||||
OUT: Good | q14 | 0 | dcnst
|
||||
OUT: Good | q15 | 0 | dcnst
|
||||
OUT: Good | q16 | 0 | dcnst
|
||||
OUT: Good | q17 | 0 | dcnst
|
||||
OUT: Good | q18 | 0 | dcnst
|
||||
OUT: Good | q19 | 0 | dcnst
|
||||
OUT: Good | q2 | 0 | dcnst
|
||||
OUT: Good | q3 | 0 | dcnst
|
||||
OUT: Good | q4 | 0 | dcnst
|
||||
OUT: Good | q5 | 0 | dcnst
|
||||
OUT: Good | q6 | 0 | dcnst
|
||||
OUT: Good | q7 | 0 | dcnst
|
||||
OUT: Good | q8 | 0 | dcnst
|
||||
OUT: Good | q9 | 0 | dcnst
|
||||
OUT:
|
||||
OUT: Type constants: #A #A' #A'[0] #A[0] #B #B[0] #Boolean #Cons #Cons[0] #Cons[1] #F #F[0] #G #G[0] #Integer #Natural #NegInteger #PosInteger #R #R[0] #Real #String #Tree #Tree[0] #Tree[1] Base.#Any Base.#Constant Base.#Data Good.#Any Good.#Constant Good.#Data
|
||||
OUT: Symbolic constants:
|
||||
OUT: Rationals: 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21
|
||||
OUT: Strings:
|
||||
OUT: Variables: a b w x x0 x1 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x2 x20 x21 x22 x3 x4 x5 x6 x7 x8 x9 y y' z z'
|
||||
OUT:
|
||||
OUT: []> typ Good
|
||||
OUT: + Type environment at (17, 4)
|
||||
OUT: ~dc0: G(Tree)
|
||||
OUT: z: Tree
|
||||
OUT: x: Tree + {NIL} + Natural
|
||||
OUT: y: Tree + {NIL} + Natural
|
||||
OUT: + Type environment at (17, 10)
|
||||
OUT: ~dc0: G(Tree)
|
||||
OUT: z: Tree
|
||||
OUT: x: Tree + {NIL} + Natural
|
||||
OUT: y: Tree + {NIL} + Natural
|
||||
OUT: + Type environment at (19, 4)
|
||||
OUT: ~dc0: G(Cons(Natural, Cons))
|
||||
OUT: z: {NIL} + Cons
|
||||
OUT: x: Cons(Natural, Cons)
|
||||
OUT: y: Cons
|
||||
OUT: a: Natural
|
||||
OUT: b: Natural
|
||||
OUT: + Type environment at (19, 10)
|
||||
OUT: ~dc0: G(Cons(Natural, Cons))
|
||||
OUT: z: {NIL} + Cons
|
||||
OUT: x: Cons(Natural, Cons)
|
||||
OUT: y: Cons
|
||||
OUT: a: Natural
|
||||
OUT: b: Natural
|
||||
OUT: + Type environment at (21, 4)
|
||||
OUT: ~dc0: G(Tree)
|
||||
OUT: z: Tree + {NIL} + Natural
|
||||
OUT: x: Tree
|
||||
OUT: y: Tree
|
||||
OUT: + Type environment at (21, 10)
|
||||
OUT: ~dc0: G(Tree)
|
||||
OUT: z: Tree + {NIL} + Natural
|
||||
OUT: x: Tree
|
||||
OUT: y: Tree
|
||||
OUT: + Type environment at (23, 4)
|
||||
OUT: ~dc0: Tree({NIL}, Tree(Natural, Natural))
|
||||
OUT: z: Cons(Natural, {NIL})
|
||||
OUT: x: {NIL}
|
||||
OUT: y: Natural
|
||||
OUT: + Type environment at (23, 10)
|
||||
OUT: ~dc0: Tree({NIL}, Tree(Natural, Natural))
|
||||
OUT: z: Cons(Natural, {NIL})
|
||||
OUT: x: {NIL}
|
||||
OUT: y: Natural
|
||||
OUT: + Type environment at (25, 4)
|
||||
OUT: ~dc0: G(Tree)
|
||||
OUT: z: Tree + {NIL} + Natural
|
||||
OUT: x: Tree
|
||||
OUT: y: Tree
|
||||
OUT: + Type environment at (25, 10)
|
||||
OUT: ~dc0: G(Tree)
|
||||
OUT: z: Tree + {NIL} + Natural
|
||||
OUT: x: Tree
|
||||
OUT: y: Tree
|
||||
OUT: + Type environment at (27, 4)
|
||||
OUT: ~dc0: G(Cons({0..0}, Cons({1..1}, Cons({2..2}, Cons({3..3}, Cons({4..4}, Cons({5..5}, Cons({6..6}, Cons({7..7}, Cons({8..8}, Cons({9..9}, Cons({10..10}, Cons({11..11}, Cons({12..12}, Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons)))))))))))))))))))))))
|
||||
OUT: x0: Cons({0..0}, Cons({1..1}, Cons({2..2}, Cons({3..3}, Cons({4..4}, Cons({5..5}, Cons({6..6}, Cons({7..7}, Cons({8..8}, Cons({9..9}, Cons({10..10}, Cons({11..11}, Cons({12..12}, Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons))))))))))))))))))))))
|
||||
OUT: x1: Cons({1..1}, Cons({2..2}, Cons({3..3}, Cons({4..4}, Cons({5..5}, Cons({6..6}, Cons({7..7}, Cons({8..8}, Cons({9..9}, Cons({10..10}, Cons({11..11}, Cons({12..12}, Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons)))))))))))))))))))))
|
||||
OUT: x2: Cons({2..2}, Cons({3..3}, Cons({4..4}, Cons({5..5}, Cons({6..6}, Cons({7..7}, Cons({8..8}, Cons({9..9}, Cons({10..10}, Cons({11..11}, Cons({12..12}, Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons))))))))))))))))))))
|
||||
OUT: x3: Cons({3..3}, Cons({4..4}, Cons({5..5}, Cons({6..6}, Cons({7..7}, Cons({8..8}, Cons({9..9}, Cons({10..10}, Cons({11..11}, Cons({12..12}, Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons)))))))))))))))))))
|
||||
OUT: x4: Cons({4..4}, Cons({5..5}, Cons({6..6}, Cons({7..7}, Cons({8..8}, Cons({9..9}, Cons({10..10}, Cons({11..11}, Cons({12..12}, Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons))))))))))))))))))
|
||||
OUT: x5: Cons({5..5}, Cons({6..6}, Cons({7..7}, Cons({8..8}, Cons({9..9}, Cons({10..10}, Cons({11..11}, Cons({12..12}, Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons)))))))))))))))))
|
||||
OUT: x6: Cons({6..6}, Cons({7..7}, Cons({8..8}, Cons({9..9}, Cons({10..10}, Cons({11..11}, Cons({12..12}, Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons))))))))))))))))
|
||||
OUT: x7: Cons({7..7}, Cons({8..8}, Cons({9..9}, Cons({10..10}, Cons({11..11}, Cons({12..12}, Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons)))))))))))))))
|
||||
OUT: x8: Cons({8..8}, Cons({9..9}, Cons({10..10}, Cons({11..11}, Cons({12..12}, Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons))))))))))))))
|
||||
OUT: x9: Cons({9..9}, Cons({10..10}, Cons({11..11}, Cons({12..12}, Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons)))))))))))))
|
||||
OUT: x10: Cons({10..10}, Cons({11..11}, Cons({12..12}, Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons))))))))))))
|
||||
OUT: x11: Cons({11..11}, Cons({12..12}, Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons)))))))))))
|
||||
OUT: x12: Cons({12..12}, Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons))))))))))
|
||||
OUT: x13: Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons)))))))))
|
||||
OUT: x14: Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons))))))))
|
||||
OUT: x15: Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons)))))))
|
||||
OUT: x16: Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons))))))
|
||||
OUT: x17: Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons)))))
|
||||
OUT: x18: Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons))))
|
||||
OUT: x19: Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons)))
|
||||
OUT: x20: Cons({20..20}, Cons({21..21}, {NIL} + Cons))
|
||||
OUT: x21: Cons({21..21}, {NIL} + Cons)
|
||||
OUT: x22: {NIL} + Cons
|
||||
OUT: + Type environment at (27, 10)
|
||||
OUT: ~dc0: G(Cons({0..0}, Cons({1..1}, Cons({2..2}, Cons({3..3}, Cons({4..4}, Cons({5..5}, Cons({6..6}, Cons({7..7}, Cons({8..8}, Cons({9..9}, Cons({10..10}, Cons({11..11}, Cons({12..12}, Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons)))))))))))))))))))))))
|
||||
OUT: x0: Cons({0..0}, Cons({1..1}, Cons({2..2}, Cons({3..3}, Cons({4..4}, Cons({5..5}, Cons({6..6}, Cons({7..7}, Cons({8..8}, Cons({9..9}, Cons({10..10}, Cons({11..11}, Cons({12..12}, Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons))))))))))))))))))))))
|
||||
OUT: x1: Cons({1..1}, Cons({2..2}, Cons({3..3}, Cons({4..4}, Cons({5..5}, Cons({6..6}, Cons({7..7}, Cons({8..8}, Cons({9..9}, Cons({10..10}, Cons({11..11}, Cons({12..12}, Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons)))))))))))))))))))))
|
||||
OUT: x2: Cons({2..2}, Cons({3..3}, Cons({4..4}, Cons({5..5}, Cons({6..6}, Cons({7..7}, Cons({8..8}, Cons({9..9}, Cons({10..10}, Cons({11..11}, Cons({12..12}, Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons))))))))))))))))))))
|
||||
OUT: x3: Cons({3..3}, Cons({4..4}, Cons({5..5}, Cons({6..6}, Cons({7..7}, Cons({8..8}, Cons({9..9}, Cons({10..10}, Cons({11..11}, Cons({12..12}, Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons)))))))))))))))))))
|
||||
OUT: x4: Cons({4..4}, Cons({5..5}, Cons({6..6}, Cons({7..7}, Cons({8..8}, Cons({9..9}, Cons({10..10}, Cons({11..11}, Cons({12..12}, Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons))))))))))))))))))
|
||||
OUT: x5: Cons({5..5}, Cons({6..6}, Cons({7..7}, Cons({8..8}, Cons({9..9}, Cons({10..10}, Cons({11..11}, Cons({12..12}, Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons)))))))))))))))))
|
||||
OUT: x6: Cons({6..6}, Cons({7..7}, Cons({8..8}, Cons({9..9}, Cons({10..10}, Cons({11..11}, Cons({12..12}, Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons))))))))))))))))
|
||||
OUT: x7: Cons({7..7}, Cons({8..8}, Cons({9..9}, Cons({10..10}, Cons({11..11}, Cons({12..12}, Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons)))))))))))))))
|
||||
OUT: x8: Cons({8..8}, Cons({9..9}, Cons({10..10}, Cons({11..11}, Cons({12..12}, Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons))))))))))))))
|
||||
OUT: x9: Cons({9..9}, Cons({10..10}, Cons({11..11}, Cons({12..12}, Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons)))))))))))))
|
||||
OUT: x10: Cons({10..10}, Cons({11..11}, Cons({12..12}, Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons))))))))))))
|
||||
OUT: x11: Cons({11..11}, Cons({12..12}, Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons)))))))))))
|
||||
OUT: x12: Cons({12..12}, Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons))))))))))
|
||||
OUT: x13: Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons)))))))))
|
||||
OUT: x14: Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons))))))))
|
||||
OUT: x15: Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons)))))))
|
||||
OUT: x16: Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons))))))
|
||||
OUT: x17: Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons)))))
|
||||
OUT: x18: Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons))))
|
||||
OUT: x19: Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL} + Cons)))
|
||||
OUT: x20: Cons({20..20}, Cons({21..21}, {NIL} + Cons))
|
||||
OUT: x21: Cons({21..21}, {NIL} + Cons)
|
||||
OUT: x22: {NIL} + Cons
|
||||
OUT: + Type environment at (51, 4)
|
||||
OUT: ~dc0: G(Tree + {NIL} + Natural)
|
||||
OUT: z: Tree + {NIL} + Natural
|
||||
OUT: x: Tree({1..1}, Tree({2..2}, {NIL}))
|
||||
OUT: y: Tree({2..2}, Tree(Tree + {NIL} + Natural, {NIL}))
|
||||
OUT: + Type environment at (51, 10)
|
||||
OUT: ~dc0: G(Tree + {NIL} + Natural)
|
||||
OUT: z: Tree + {NIL} + Natural
|
||||
OUT: x: Tree({1..1}, Tree({2..2}, {NIL}))
|
||||
OUT: y: Tree({2..2}, Tree(Tree + {NIL} + Natural, {NIL}))
|
||||
OUT: + Type environment at (55, 4)
|
||||
OUT: x: Cons({0..0}, Cons({1..1}, Cons({2..2}, Cons({3..3}, Cons({4..4}, Cons({5..5}, Cons({6..6}, Cons({7..7}, Cons({8..8}, Cons({9..9}, Cons({10..10}, Cons({11..11}, Cons({12..12}, Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL}))))))))))))))))))))))
|
||||
OUT: + Type environment at (55, 12)
|
||||
OUT: x: Cons({0..0}, Cons({1..1}, Cons({2..2}, Cons({3..3}, Cons({4..4}, Cons({5..5}, Cons({6..6}, Cons({7..7}, Cons({8..8}, Cons({9..9}, Cons({10..10}, Cons({11..11}, Cons({12..12}, Cons({13..13}, Cons({14..14}, Cons({15..15}, Cons({16..16}, Cons({17..17}, Cons({18..18}, Cons({19..19}, Cons({20..20}, Cons({21..21}, {NIL}))))))))))))))))))))))
|
||||
OUT: + Type environment at (79, 4)
|
||||
OUT: ~dc0: Tree(Tree({3..3}, {3..3}), Tree(Tree({3..3}, {3..3}), Tree({3..3}, {3..3})))
|
||||
OUT: z: {3..3}
|
||||
OUT: x: Tree({3..3}, {3..3})
|
||||
OUT: y: Tree(Tree({3..3}, {3..3}), Tree({3..3}, {3..3}))
|
||||
OUT: + Type environment at (79, 10)
|
||||
OUT: ~dc0: Tree(Tree({3..3}, {3..3}), Tree(Tree({3..3}, {3..3}), Tree({3..3}, {3..3})))
|
||||
OUT: z: {3..3}
|
||||
OUT: x: Tree({3..3}, {3..3})
|
||||
OUT: y: Tree(Tree({3..3}, {3..3}), Tree({3..3}, {3..3}))
|
||||
OUT: + Type environment at (83, 4)
|
||||
OUT: + Type environment at (83, 19)
|
||||
OUT: + Type environment at (85, 4)
|
||||
OUT: x: {1..1}
|
||||
OUT: y: {1..1}
|
||||
OUT: + Type environment at (85, 13)
|
||||
OUT: x: {1..1}
|
||||
OUT: y: {1..1}
|
||||
OUT: + Type environment at (87, 4)
|
||||
OUT: ~dc0: G(F + Integer)
|
||||
OUT: z: F
|
||||
OUT: x: F(F)
|
||||
OUT: y: F
|
||||
OUT: y': F + Integer
|
||||
OUT: z': F + Integer
|
||||
OUT: + Type environment at (87, 13)
|
||||
OUT: ~dc0: G(F + Integer)
|
||||
OUT: z: F
|
||||
OUT: x: F(F)
|
||||
OUT: y: F
|
||||
OUT: y': F + Integer
|
||||
OUT: z': F + Integer
|
||||
OUT: + Type environment at (92, 4)
|
||||
OUT: ~dc0: G(Tree(Tree(Tree + {NIL} + Natural, Tree(Tree, Tree + {NIL} + Natural)), Tree + {NIL} + Natural))
|
||||
OUT: x: Tree(Tree(Tree + {NIL} + Natural, Tree(Tree, Tree + {NIL} + Natural)), Tree + {NIL} + Natural)
|
||||
OUT: y: Tree + {NIL} + Natural
|
||||
OUT: ~sv0: Tree(Tree + {NIL} + Natural, Tree(Tree, Tree + {NIL} + Natural))
|
||||
OUT: ~sv1: Tree + {NIL} + Natural
|
||||
OUT: ~sv2: Tree + {NIL} + Natural
|
||||
OUT: ~sv3: Tree(Tree, Tree + {NIL} + Natural)
|
||||
OUT: ~sv4: Tree
|
||||
OUT: ~sv5: Tree + {NIL} + Natural
|
||||
OUT: ~sv6: Tree + {NIL} + Natural
|
||||
OUT: ~sv7: Tree + {NIL} + Natural
|
||||
OUT: + Type environment at (92, 11)
|
||||
OUT: ~dc0: G(Tree(Tree(Tree + {NIL} + Natural, Tree(Tree, Tree + {NIL} + Natural)), Tree + {NIL} + Natural))
|
||||
OUT: x: Tree(Tree(Tree + {NIL} + Natural, Tree(Tree, Tree + {NIL} + Natural)), Tree + {NIL} + Natural)
|
||||
OUT: y: Tree + {NIL} + Natural
|
||||
OUT: ~sv0: Tree(Tree + {NIL} + Natural, Tree(Tree, Tree + {NIL} + Natural))
|
||||
OUT: ~sv1: Tree + {NIL} + Natural
|
||||
OUT: ~sv2: Tree + {NIL} + Natural
|
||||
OUT: ~sv3: Tree(Tree, Tree + {NIL} + Natural)
|
||||
OUT: ~sv4: Tree
|
||||
OUT: ~sv5: Tree + {NIL} + Natural
|
||||
OUT: ~sv6: Tree + {NIL} + Natural
|
||||
OUT: ~sv7: Tree + {NIL} + Natural
|
||||
OUT: + Type environment at (94, 4)
|
||||
OUT: ~dc0: G(Tree(Tree, Tree + {NIL} + Natural))
|
||||
OUT: x: Tree(Tree, Tree + {NIL} + Natural)
|
||||
OUT: y: Tree
|
||||
OUT: ~dc1: G(Tree)
|
||||
OUT: ~sv0: Tree
|
||||
OUT: ~sv1: Tree + {NIL} + Natural
|
||||
OUT: ~sv2: Tree + {NIL} + Natural
|
||||
OUT: ~sv3: Tree + {NIL} + Natural
|
||||
OUT: ~sv4: Tree + {NIL} + Natural
|
||||
OUT: ~sv5: Tree + {NIL} + Natural
|
||||
OUT: + Type environment at (94, 11)
|
||||
OUT: ~dc0: G(Tree(Tree, Tree + {NIL} + Natural))
|
||||
OUT: x: Tree(Tree, Tree + {NIL} + Natural)
|
||||
OUT: y: Tree
|
||||
OUT: ~dc1: G(Tree)
|
||||
OUT: ~sv0: Tree
|
||||
OUT: ~sv1: Tree + {NIL} + Natural
|
||||
OUT: ~sv2: Tree + {NIL} + Natural
|
||||
OUT: ~sv3: Tree + {NIL} + Natural
|
||||
OUT: ~sv4: Tree + {NIL} + Natural
|
||||
OUT: ~sv5: Tree + {NIL} + Natural
|
||||
OUT: + Type environment at (96, 4)
|
||||
OUT: ~dc0: G(Tree(Tree(Tree, Tree), Tree + {NIL} + Natural))
|
||||
OUT: z: Tree
|
||||
OUT: x: Tree(Tree(Tree, Tree), Tree + {NIL} + Natural)
|
||||
OUT: y: Tree(Tree(Tree, Tree), Tree + {NIL} + Natural)
|
||||
OUT: z': Tree + {NIL} + Natural
|
||||
OUT: ~sv0: Tree(Tree, Tree)
|
||||
OUT: ~sv1: Tree + {NIL} + Natural
|
||||
OUT: ~sv2: Tree(Tree, Tree)
|
||||
OUT: ~sv3: Tree + {NIL} + Natural
|
||||
OUT: w: Tree
|
||||
OUT: + Type environment at (96, 17)
|
||||
OUT: ~dc0: G(Tree(Tree(Tree, Tree), Tree + {NIL} + Natural))
|
||||
OUT: z: Tree
|
||||
OUT: x: Tree(Tree(Tree, Tree), Tree + {NIL} + Natural)
|
||||
OUT: y: Tree(Tree(Tree, Tree), Tree + {NIL} + Natural)
|
||||
OUT: z': Tree + {NIL} + Natural
|
||||
OUT: ~sv0: Tree(Tree, Tree)
|
||||
OUT: ~sv1: Tree + {NIL} + Natural
|
||||
OUT: ~sv2: Tree(Tree, Tree)
|
||||
OUT: ~sv3: Tree + {NIL} + Natural
|
||||
OUT: w: Tree
|
||||
OUT: + Type environment at (101, 4)
|
||||
OUT: ~dc0: G(R + Cons + B + A' + A)
|
||||
OUT: x: R + Cons + B + A' + A
|
||||
OUT: y: R + Cons + B + A' + A
|
||||
OUT: ~dc1: G(R + Cons + B + A' + A)
|
||||
OUT: + Type environment at (101, 11)
|
||||
OUT: ~dc0: G(R + Cons + B + A' + A)
|
||||
OUT: x: R + Cons + B + A' + A
|
||||
OUT: y: R + Cons + B + A' + A
|
||||
OUT: ~dc1: G(R + Cons + B + A' + A)
|
||||
OUT: + Type environment at (103, 4)
|
||||
OUT: ~dc0: A
|
||||
OUT: ~dc1: {FALSE}
|
||||
OUT: ~dc2: A'
|
||||
OUT: ~dc3: {TRUE}
|
||||
OUT: + Type environment at (103, 11)
|
||||
OUT: ~dc0: A
|
||||
OUT: ~dc1: {FALSE}
|
||||
OUT: ~dc2: A'
|
||||
OUT: ~dc3: {TRUE}
|
||||
OUT: + Type environment at (105, 4)
|
||||
OUT: x: R
|
||||
OUT: y: {0..0} + NegInteger
|
||||
OUT: + Type environment at (105, 11)
|
||||
OUT: x: R
|
||||
OUT: y: {0..0} + NegInteger
|
||||
OUT: + Type environment at (107, 4)
|
||||
OUT: ~dc0: Tree
|
||||
OUT: ~dc1: Tree + {NIL} + Natural
|
||||
OUT: ~dc2: Tree + {NIL} + Natural
|
||||
OUT: + Type environment at (107, 11)
|
||||
OUT: ~dc0: Tree
|
||||
OUT: ~dc1: Tree + {NIL} + Natural
|
||||
OUT: ~dc2: Tree + {NIL} + Natural
|
||||
OUT: + Type environment at (109, 4)
|
||||
OUT: x: Tree + R + F + Cons + B + A' + A
|
||||
OUT: + Type environment at (109, 11)
|
||||
OUT: x: Tree + R + F + Cons + B + A' + A
|
||||
OUT:
|
||||
OUT: []> x
|
||||
OUT:
|
||||
EXIT: 0
|
||||
|
|
@ -0,0 +1,4 @@
|
|||
run: ..\..\..\..\Bld\Drops\Formula_Debug_x86\Formula.exe
|
||||
arg: -v: off -l: "tests.4ml" -dt: "Good" -typ: "Good" -x
|
||||
acc: .\
|
||||
dsc: Rules for which unification constraints are SAT
|
||||
|
|
@ -0,0 +1,110 @@
|
|||
domain Base
|
||||
{
|
||||
Cons ::= new (val: Natural, tail: any Cons + { NIL } ).
|
||||
R ::= new (val: NegInteger + { 0 }).
|
||||
B ::= new (val: Boolean).
|
||||
A ::= new (val: { FALSE } ).
|
||||
A' ::= new (val: { TRUE } ).
|
||||
Tree ::= new (lft: any Natural + Tree + { NIL },
|
||||
rt: any Natural + Tree + { NIL } ).
|
||||
F ::= new (any Integer + F).
|
||||
}
|
||||
|
||||
domain Good extends Base
|
||||
{
|
||||
G ::= (Good.Any).
|
||||
|
||||
q0 :- G(z), Tree(x, y) = z.
|
||||
|
||||
q1 :- G(x), x = Cons(a, y), y = Cons(b, z).
|
||||
|
||||
q2 :- G(x), Tree(x, x) = Tree(y, Tree(z, z)).
|
||||
|
||||
q3 :- Tree(x, Tree(y, y)), z = Cons(y, x).
|
||||
|
||||
q4 :- G(x), Tree(x, y) = Tree(y, x), x = Tree(z, z).
|
||||
|
||||
q5 :- G(x0),
|
||||
x0 = Cons(0, x1),
|
||||
x1 = Cons(1, x2),
|
||||
x2 = Cons(2, x3),
|
||||
x3 = Cons(3, x4),
|
||||
x4 = Cons(4, x5),
|
||||
x5 = Cons(5, x6),
|
||||
x6 = Cons(6, x7),
|
||||
x7 = Cons(7, x8),
|
||||
x8 = Cons(8, x9),
|
||||
x9 = Cons(9, x10),
|
||||
x10 = Cons(10, x11),
|
||||
x11 = Cons(11, x12),
|
||||
x12 = Cons(12, x13),
|
||||
x13 = Cons(13, x14),
|
||||
x14 = Cons(14, x15),
|
||||
x15 = Cons(15, x16),
|
||||
x16 = Cons(16, x17),
|
||||
x17 = Cons(17, x18),
|
||||
x18 = Cons(18, x19),
|
||||
x19 = Cons(19, x20),
|
||||
x20 = Cons(20, x21),
|
||||
x21 = Cons(21, x22).
|
||||
|
||||
q6 :- G(z),
|
||||
Tree(1, Tree(2, NIL)) = x,
|
||||
Tree(2, Tree(z, NIL)) = y.
|
||||
|
||||
q7 :- x =
|
||||
Cons(0,
|
||||
Cons(1,
|
||||
Cons(2,
|
||||
Cons(3,
|
||||
Cons(4,
|
||||
Cons(5,
|
||||
Cons(6,
|
||||
Cons(7,
|
||||
Cons(8,
|
||||
Cons(9,
|
||||
Cons(10,
|
||||
Cons(11,
|
||||
Cons(12,
|
||||
Cons(13,
|
||||
Cons(14,
|
||||
Cons(15,
|
||||
Cons(16,
|
||||
Cons(17,
|
||||
Cons(18,
|
||||
Cons(19,
|
||||
Cons(20,
|
||||
Cons(21, NIL)))))))))))))))))))))).
|
||||
|
||||
q8 :- Tree(x, y),
|
||||
x = Tree(z, z), y = Tree(x, x),
|
||||
z = 3.
|
||||
|
||||
q9 :- A(FALSE) = A(FALSE).
|
||||
|
||||
q10 :- x = 1, x = y, y = 1.
|
||||
|
||||
q11 :- x = F(y), x = F(z),
|
||||
y = F(y'), y = F(z'),
|
||||
z' = y',
|
||||
G(y').
|
||||
|
||||
q12 :- G(x), x.lft.rt.lft.rt = y.
|
||||
|
||||
q13 :- G(x), G(y), x.lft.rt = y.rt, y.rt = x.lft.rt.
|
||||
|
||||
q14 :- x.lft = Tree( z, Tree(z', z')),
|
||||
y.lft = Tree( w, w ),
|
||||
x = y,
|
||||
G(x).
|
||||
|
||||
q15 :- G(x), G(y), x.val = y.val, x != y.
|
||||
|
||||
q16 :- A(_), A'(_).
|
||||
|
||||
q17 :- x is R(y).
|
||||
|
||||
q18 :- Tree(_, _).
|
||||
|
||||
q19 :- x is Good.Data.
|
||||
}
|
||||
|
|
@ -0,0 +1,32 @@
|
|||
=================================
|
||||
Console output
|
||||
=================================
|
||||
OUT:
|
||||
OUT: []> v off
|
||||
OUT: verbose off
|
||||
OUT:
|
||||
OUT: []> l tests.4ml
|
||||
OUT: (Failed) tests.4ml
|
||||
OUT: tests.4ml (15, 21): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (17, 28): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (19, 21): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (21, 30): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (23, 37): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (46, 14): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (50, 12): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (52, 12): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (78, 12): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (80, 19): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (82, 27): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (86, 13): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (88, 11): Argument 1 of function .tail is badly typed.
|
||||
OUT: tests.4ml (90, 28): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (92, 33): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (96, 13): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (100, 13): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (102, 41): This constraint is unsatisfiable.
|
||||
OUT: tests.4ml (0, 0): The install operation failed
|
||||
OUT:
|
||||
OUT: []> x
|
||||
OUT:
|
||||
EXIT: 1
|
||||
|
|
@ -0,0 +1,4 @@
|
|||
run: ..\..\..\..\Bld\Drops\Formula_Debug_x86\Formula.exe
|
||||
arg: -v: off -l: "tests.4ml" -x
|
||||
acc: .\
|
||||
dsc: Rules for which unification constraints are UNSAT
|
||||
|
|
@ -0,0 +1,103 @@
|
|||
domain Base
|
||||
{
|
||||
Cons ::= new (val: Natural, tail: any Cons + { NIL } ).
|
||||
R ::= new (val: NegInteger + { 0 }).
|
||||
B ::= new (val: Boolean).
|
||||
A ::= new (val: { FALSE } ).
|
||||
A' ::= new (val: { TRUE } ).
|
||||
Tree ::= new (lft: any Natural + Tree + { NIL },
|
||||
rt: any Natural + Tree + { NIL } ).
|
||||
F ::= new (any Integer + F).
|
||||
}
|
||||
|
||||
domain Bad extends Base
|
||||
{
|
||||
q0 :- Tree(x, y) = y.
|
||||
|
||||
q1 :- x = Cons(a, y), y = Cons(b, x).
|
||||
|
||||
q2 :- Tree(x, x) = Tree(y, Tree(y, z)).
|
||||
|
||||
q3 :- Tree(x, Tree(y, y)) = Cons(y, x).
|
||||
|
||||
q4 :- Tree(x, y) = Tree(y, x), x = Tree(y, y).
|
||||
|
||||
q5 :- x0 = Cons(0, x1),
|
||||
x1 = Cons(1, x2),
|
||||
x2 = Cons(2, x3),
|
||||
x3 = Cons(3, x4),
|
||||
x4 = Cons(4, x5),
|
||||
x5 = Cons(5, x6),
|
||||
x6 = Cons(6, x7),
|
||||
x7 = Cons(7, x8),
|
||||
x8 = Cons(8, x9),
|
||||
x9 = Cons(9, x10),
|
||||
x10 = Cons(10, x11),
|
||||
x11 = Cons(11, x12),
|
||||
x12 = Cons(12, x13),
|
||||
x13 = Cons(13, x14),
|
||||
x14 = Cons(14, x15),
|
||||
x15 = Cons(15, x16),
|
||||
x16 = Cons(16, x17),
|
||||
x17 = Cons(17, x18),
|
||||
x18 = Cons(18, x19),
|
||||
x19 = Cons(19, x20),
|
||||
x20 = Cons(20, x21),
|
||||
x21 = Cons(21, x0).
|
||||
|
||||
q6 :- Tree(1, Tree(2, NIL)) = x,
|
||||
Tree(2, Tree(z, NIL)) = y,
|
||||
x = y.
|
||||
|
||||
q7 :- x =
|
||||
Cons(0,
|
||||
Cons(1,
|
||||
Cons(2,
|
||||
Cons(3,
|
||||
Cons(4,
|
||||
Cons(5,
|
||||
Cons(6,
|
||||
Cons(7,
|
||||
Cons(8,
|
||||
Cons(9,
|
||||
Cons(10,
|
||||
Cons(11,
|
||||
Cons(12,
|
||||
Cons(13,
|
||||
Cons(14,
|
||||
Cons(15,
|
||||
Cons(16,
|
||||
Cons(17,
|
||||
Cons(18,
|
||||
Cons(19,
|
||||
Cons(20,
|
||||
Cons(21, x)))))))))))))))))))))).
|
||||
|
||||
q8 :- Tree(x, y),
|
||||
x = Tree(z, z), y = Tree(x, x),
|
||||
y = z.
|
||||
|
||||
q9 :- B(FALSE) = A(FALSE).
|
||||
|
||||
q10 :- x = y, x = 1, y = 2.
|
||||
|
||||
q11 :- x = F(y), x = F(z),
|
||||
y = F(y'), y = F(z'),
|
||||
z = y'.
|
||||
|
||||
q12 :- x.lft.rt.lft.rt.tail = y.
|
||||
|
||||
q13 :- x.lft = y, y.lft = x.
|
||||
|
||||
q14 :- x.lft.rt = y.rt, y.rt = x.lft.
|
||||
|
||||
q15 :- y = Tree(y', z),
|
||||
x.lft = y,
|
||||
x = y'.
|
||||
|
||||
q16 :- x.lft = Tree( z, Tree(z, z')),
|
||||
y.lft = Tree( w, w ),
|
||||
x = y.
|
||||
|
||||
q17 :- x.lft = y.lft, x.rt = y.rt, x != y.
|
||||
}
|
||||
|
|
@ -0,0 +1,6 @@
|
|||
<?xml version="1.0" encoding="utf-8" ?>
|
||||
<configuration>
|
||||
<startup>
|
||||
<supportedRuntime version="v4.0" sku=".NETFramework,Version=v4.5" />
|
||||
</startup>
|
||||
</configuration>
|
||||
|
|
@ -0,0 +1,61 @@
|
|||
<?xml version="1.0" encoding="utf-8"?>
|
||||
<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
|
||||
<Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />
|
||||
<PropertyGroup>
|
||||
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
|
||||
<Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
|
||||
<ProjectGuid>{E9014C29-75C5-4484-A4D3-63CA735FD3FF}</ProjectGuid>
|
||||
<OutputType>Exe</OutputType>
|
||||
<AppDesignerFolder>Properties</AppDesignerFolder>
|
||||
<RootNamespace>Check</RootNamespace>
|
||||
<AssemblyName>Check</AssemblyName>
|
||||
<TargetFrameworkVersion>v4.5</TargetFrameworkVersion>
|
||||
<FileAlignment>512</FileAlignment>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
|
||||
<PlatformTarget>AnyCPU</PlatformTarget>
|
||||
<DebugSymbols>true</DebugSymbols>
|
||||
<DebugType>full</DebugType>
|
||||
<Optimize>false</Optimize>
|
||||
<OutputPath>bin\Debug\</OutputPath>
|
||||
<DefineConstants>DEBUG;TRACE</DefineConstants>
|
||||
<ErrorReport>prompt</ErrorReport>
|
||||
<WarningLevel>4</WarningLevel>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
|
||||
<PlatformTarget>AnyCPU</PlatformTarget>
|
||||
<DebugType>pdbonly</DebugType>
|
||||
<Optimize>true</Optimize>
|
||||
<OutputPath>bin\Release\</OutputPath>
|
||||
<DefineConstants>TRACE</DefineConstants>
|
||||
<ErrorReport>prompt</ErrorReport>
|
||||
<WarningLevel>4</WarningLevel>
|
||||
</PropertyGroup>
|
||||
<ItemGroup>
|
||||
<Reference Include="System" />
|
||||
<Reference Include="System.Core" />
|
||||
<Reference Include="System.Xml.Linq" />
|
||||
<Reference Include="System.Data.DataSetExtensions" />
|
||||
<Reference Include="Microsoft.CSharp" />
|
||||
<Reference Include="System.Data" />
|
||||
<Reference Include="System.Xml" />
|
||||
</ItemGroup>
|
||||
<ItemGroup>
|
||||
<Compile Include="Checker.cs" />
|
||||
<Compile Include="OptionParser.cs" />
|
||||
<Compile Include="Options.cs" />
|
||||
<Compile Include="Program.cs" />
|
||||
<Compile Include="Properties\AssemblyInfo.cs" />
|
||||
</ItemGroup>
|
||||
<ItemGroup>
|
||||
<None Include="App.config" />
|
||||
</ItemGroup>
|
||||
<Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
|
||||
<!-- To modify your build process, add your task inside one of the targets below and uncomment it.
|
||||
Other similar extension points exist, see Microsoft.Common.targets.
|
||||
<Target Name="BeforeBuild">
|
||||
</Target>
|
||||
<Target Name="AfterBuild">
|
||||
</Target>
|
||||
-->
|
||||
</Project>
|
||||
|
|
@ -0,0 +1,20 @@
|
|||
|
||||
Microsoft Visual Studio Solution File, Format Version 12.00
|
||||
# Visual Studio 2012
|
||||
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Check", "Check.csproj", "{E9014C29-75C5-4484-A4D3-63CA735FD3FF}"
|
||||
EndProject
|
||||
Global
|
||||
GlobalSection(SolutionConfigurationPlatforms) = preSolution
|
||||
Debug|Any CPU = Debug|Any CPU
|
||||
Release|Any CPU = Release|Any CPU
|
||||
EndGlobalSection
|
||||
GlobalSection(ProjectConfigurationPlatforms) = postSolution
|
||||
{E9014C29-75C5-4484-A4D3-63CA735FD3FF}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
|
||||
{E9014C29-75C5-4484-A4D3-63CA735FD3FF}.Debug|Any CPU.Build.0 = Debug|Any CPU
|
||||
{E9014C29-75C5-4484-A4D3-63CA735FD3FF}.Release|Any CPU.ActiveCfg = Release|Any CPU
|
||||
{E9014C29-75C5-4484-A4D3-63CA735FD3FF}.Release|Any CPU.Build.0 = Release|Any CPU
|
||||
EndGlobalSection
|
||||
GlobalSection(SolutionProperties) = preSolution
|
||||
HideSolutionNode = FALSE
|
||||
EndGlobalSection
|
||||
EndGlobal
|
||||
|
|
@ -0,0 +1,533 @@
|
|||
namespace Check
|
||||
{
|
||||
using System;
|
||||
using System.Collections.Generic;
|
||||
using System.Diagnostics;
|
||||
using System.IO;
|
||||
using System.Linq;
|
||||
using System.Text;
|
||||
using System.Threading.Tasks;
|
||||
|
||||
public class Checker
|
||||
{
|
||||
private const int BufferSize = 1024;
|
||||
|
||||
private const string RunOption = "run";
|
||||
private const string AcceptOption = "acc";
|
||||
private const string IncludeOption = "inc";
|
||||
private const string AddOption = "add";
|
||||
private const string IgnorePromptOption = "igp";
|
||||
private const string DescrOption = "dsc";
|
||||
private const string ArgsOption = "arg";
|
||||
private const string TestOption = "cfg";
|
||||
private const string DelOption = "del";
|
||||
|
||||
private const string TmpStreamFile = "check-tmp.txt";
|
||||
private const string AccFiles = "acc*.txt";
|
||||
private const string AccPrefix = "acc";
|
||||
private const string AccExt = ".txt";
|
||||
private const string LogFile = "check-output.log";
|
||||
|
||||
private static readonly string[] AllOptions = new string[]
|
||||
{
|
||||
RunOption,
|
||||
AcceptOption,
|
||||
IncludeOption,
|
||||
AddOption,
|
||||
IgnorePromptOption,
|
||||
DescrOption,
|
||||
ArgsOption,
|
||||
TestOption,
|
||||
DelOption
|
||||
};
|
||||
|
||||
private string activeDirectory;
|
||||
|
||||
public string Description
|
||||
{
|
||||
get;
|
||||
private set;
|
||||
}
|
||||
|
||||
public Checker(string activeDirectory)
|
||||
{
|
||||
this.activeDirectory = activeDirectory;
|
||||
}
|
||||
|
||||
public static void PrintUsage()
|
||||
{
|
||||
Console.WriteLine(
|
||||
"USAGE: Check -{0}: exe -{1}: dir [-{6}: args] [-{2}: files] [-{8}: files] [-{7}: file] [-{3}] [-{4}] [-{5}: descriptors]",
|
||||
RunOption,
|
||||
AcceptOption,
|
||||
IncludeOption,
|
||||
AddOption,
|
||||
IgnorePromptOption,
|
||||
DescrOption,
|
||||
ArgsOption,
|
||||
TestOption,
|
||||
DelOption
|
||||
);
|
||||
|
||||
Console.WriteLine();
|
||||
Console.WriteLine("-{0}\tAn exe to run", RunOption);
|
||||
Console.WriteLine("-{0}\tA directory containing acceptable outputs", AcceptOption);
|
||||
Console.WriteLine("-{0}\tA list of arguments to the exe", ArgsOption);
|
||||
Console.WriteLine("-{0}\tA list of files that should be included as output", IncludeOption);
|
||||
Console.WriteLine("-{0}\tA list of files that should be deleted before running", DelOption);
|
||||
Console.WriteLine("-{0}\tA test file with additional configuration", TestOption);
|
||||
Console.WriteLine("-{0}\tAdds the output of this run to set of acceptable outputs", AddOption);
|
||||
Console.WriteLine("-{0}\tIgnore output sent to the prompt by commands", IgnorePromptOption);
|
||||
Console.WriteLine("-{0}\tDescriptions of this test", DescrOption);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Runs check using command line arguments
|
||||
/// </summary>
|
||||
/// <returns></returns>
|
||||
public bool Check()
|
||||
{
|
||||
Options opts;
|
||||
int errPos;
|
||||
string cmdStr;
|
||||
if (!OptionParser.Parse(out opts, out errPos, out cmdStr))
|
||||
{
|
||||
Console.WriteLine("ERROR: Could not parse command line");
|
||||
Console.WriteLine("INPUT: {0}", cmdStr);
|
||||
Console.WriteLine("POS : {0}^", errPos == 0 ? string.Empty : new string(' ', errPos));
|
||||
Console.WriteLine();
|
||||
PrintUsage();
|
||||
return false;
|
||||
}
|
||||
|
||||
bool isTestSet, result = true;
|
||||
Tuple<OptValueKind, object>[] testFile;
|
||||
result = ValidateOption(opts, TestOption, true, 1, 1, out isTestSet, out testFile) && result;
|
||||
if (isTestSet)
|
||||
{
|
||||
result = opts.LoadMore(activeDirectory, (string)testFile[0].Item2) && result;
|
||||
if (result)
|
||||
{
|
||||
activeDirectory = new FileInfo(Path.Combine(activeDirectory, (string)testFile[0].Item2)).DirectoryName;
|
||||
}
|
||||
}
|
||||
|
||||
return result && Check(opts);
|
||||
}
|
||||
|
||||
public bool Check(string testfile)
|
||||
{
|
||||
var opts = new Options();
|
||||
if (!opts.LoadMore(activeDirectory, testfile))
|
||||
{
|
||||
return false;
|
||||
}
|
||||
|
||||
return Check(opts);
|
||||
}
|
||||
|
||||
private bool Check(Options opts)
|
||||
{
|
||||
bool isSet, result = true;
|
||||
Tuple<OptValueKind, object>[] exe;
|
||||
result = ValidateOption(opts, RunOption, false, 1, 1, out isSet, out exe) && result;
|
||||
|
||||
Tuple<OptValueKind, object>[] accDir;
|
||||
result = ValidateOption(opts, AcceptOption, false, 1, 1, out isSet, out accDir) && result;
|
||||
|
||||
bool isIncl;
|
||||
Tuple<OptValueKind, object>[] includes;
|
||||
result = ValidateOption(opts, IncludeOption, true, 1, int.MaxValue, out isIncl, out includes) && result;
|
||||
|
||||
bool isArgs;
|
||||
Tuple<OptValueKind, object>[] exeArgs;
|
||||
result = ValidateOption(opts, ArgsOption, true, 1, int.MaxValue, out isArgs, out exeArgs) && result;
|
||||
|
||||
bool isAdd;
|
||||
Tuple<OptValueKind, object>[] values;
|
||||
result = ValidateOption(opts, AddOption, true, 0, 0, out isAdd, out values) && result;
|
||||
|
||||
bool isIgnPrmpt;
|
||||
result = ValidateOption(opts, IgnorePromptOption, true, 0, 0, out isIgnPrmpt, out values) && result;
|
||||
|
||||
bool isDel;
|
||||
Tuple<OptValueKind, object>[] delFiles;
|
||||
result = ValidateOption(opts, DelOption, true, 1, int.MaxValue, out isDel, out delFiles) && result;
|
||||
|
||||
bool isDescr;
|
||||
Tuple<OptValueKind, object>[] descrs;
|
||||
result = ValidateOption(opts, DescrOption, true, 1, int.MaxValue, out isDescr, out descrs) && result;
|
||||
|
||||
string[] unknownOpts;
|
||||
if (opts.TryGetOptionsBesides(AllOptions, out unknownOpts))
|
||||
{
|
||||
foreach (var uo in unknownOpts)
|
||||
{
|
||||
Console.WriteLine("ERROR: -{0} is not a legal option", uo);
|
||||
}
|
||||
|
||||
result = false;
|
||||
}
|
||||
|
||||
if (!result)
|
||||
{
|
||||
Console.WriteLine();
|
||||
PrintUsage();
|
||||
return false;
|
||||
}
|
||||
|
||||
if (isDescr)
|
||||
{
|
||||
var fullDescr = "";
|
||||
foreach (var v in descrs)
|
||||
{
|
||||
fullDescr += v.Item2.ToString() + " ";
|
||||
}
|
||||
|
||||
Description = fullDescr;
|
||||
Console.WriteLine("*********** Checking {0}***********", fullDescr);
|
||||
}
|
||||
|
||||
if (isDel)
|
||||
{
|
||||
foreach (var df in delFiles)
|
||||
{
|
||||
try
|
||||
{
|
||||
var dfi = new FileInfo(Path.Combine(activeDirectory, df.Item2.ToString()));
|
||||
if (dfi.Exists)
|
||||
{
|
||||
Console.WriteLine("DEL: Deleted file {0}", dfi.FullName);
|
||||
dfi.Attributes = FileAttributes.Normal;
|
||||
dfi.Delete();
|
||||
}
|
||||
}
|
||||
catch (Exception e)
|
||||
{
|
||||
Console.WriteLine(
|
||||
"Error deleting file {0} - {1}",
|
||||
df.Item2,
|
||||
e.Message);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
StreamWriter tmpWriter;
|
||||
if (!OpenTmpStream(out tmpWriter))
|
||||
{
|
||||
return false;
|
||||
}
|
||||
|
||||
if (!Run(tmpWriter, isIgnPrmpt, exe[0].Item2.ToString(), exeArgs))
|
||||
{
|
||||
result = false;
|
||||
}
|
||||
else if (isIncl && !AppendIncludes(tmpWriter, includes))
|
||||
{
|
||||
result = false;
|
||||
}
|
||||
|
||||
if (!CloseTmpStream(tmpWriter))
|
||||
{
|
||||
result = false;
|
||||
}
|
||||
|
||||
if (result && !CompareAcceptors(accDir[0].Item2.ToString(), isAdd))
|
||||
{
|
||||
File.Delete(Path.Combine(activeDirectory, LogFile));
|
||||
File.Copy(
|
||||
Path.Combine(activeDirectory, TmpStreamFile),
|
||||
Path.Combine(activeDirectory, LogFile));
|
||||
Console.WriteLine("LOGGED: Saved bad output to {0}",
|
||||
Path.Combine(activeDirectory, LogFile));
|
||||
|
||||
result = false;
|
||||
}
|
||||
|
||||
if (!DeleteTmpFile())
|
||||
{
|
||||
result = false;
|
||||
}
|
||||
|
||||
if (result)
|
||||
{
|
||||
Console.WriteLine("SUCCESS: Output matched");
|
||||
}
|
||||
|
||||
return result;
|
||||
}
|
||||
|
||||
private static bool ValidateOption(
|
||||
Options opts,
|
||||
string opt,
|
||||
bool isOptional,
|
||||
int nArgsMin,
|
||||
int nArgsMax,
|
||||
out bool isSet,
|
||||
out Tuple<OptValueKind, object>[] values)
|
||||
{
|
||||
isSet = opts.TryGetOption(opt, out values);
|
||||
if (!isSet && !isOptional)
|
||||
{
|
||||
Console.WriteLine("ERROR: -{0} option not provided", opt);
|
||||
return false;
|
||||
}
|
||||
else if (isSet && (values.Length < nArgsMin || values.Length > nArgsMax))
|
||||
{
|
||||
Console.WriteLine("ERROR: -{0} option has wrong number of arguments", opt);
|
||||
return false;
|
||||
}
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
private bool OpenTmpStream(out StreamWriter wr)
|
||||
{
|
||||
wr = null;
|
||||
try
|
||||
{
|
||||
wr = new StreamWriter(Path.Combine(activeDirectory, TmpStreamFile));
|
||||
}
|
||||
catch (Exception e)
|
||||
{
|
||||
Console.WriteLine(
|
||||
"ERROR: Could not open temporary file {0} - {1}",
|
||||
TmpStreamFile,
|
||||
e.Message);
|
||||
return false;
|
||||
}
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
private static bool CloseTmpStream(StreamWriter wr)
|
||||
{
|
||||
try
|
||||
{
|
||||
wr.Close();
|
||||
}
|
||||
catch (Exception e)
|
||||
{
|
||||
Console.WriteLine(
|
||||
"ERROR: Could not close temporary file {0} - {1}",
|
||||
TmpStreamFile,
|
||||
e.Message);
|
||||
return false;
|
||||
}
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
private bool DeleteTmpFile()
|
||||
{
|
||||
try
|
||||
{
|
||||
var fi = new FileInfo(Path.Combine(activeDirectory, TmpStreamFile));
|
||||
if (fi.Exists)
|
||||
{
|
||||
fi.Delete();
|
||||
}
|
||||
}
|
||||
catch (Exception e)
|
||||
{
|
||||
Console.WriteLine(
|
||||
"ERROR: Could not delete temporary file {0} - {1}",
|
||||
TmpStreamFile,
|
||||
e.Message);
|
||||
return false;
|
||||
}
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
private bool AppendIncludes(StreamWriter outStream,
|
||||
Tuple<OptValueKind, object>[] includes)
|
||||
{
|
||||
foreach (var inc in includes)
|
||||
{
|
||||
outStream.WriteLine();
|
||||
outStream.WriteLine("=================================");
|
||||
outStream.WriteLine("{0}", inc.Item2.ToString());
|
||||
outStream.WriteLine("=================================");
|
||||
|
||||
try
|
||||
{
|
||||
using (var sr = new StreamReader(Path.Combine(activeDirectory, inc.Item2.ToString())))
|
||||
{
|
||||
while (!sr.EndOfStream)
|
||||
{
|
||||
outStream.WriteLine(sr.ReadLine());
|
||||
}
|
||||
}
|
||||
}
|
||||
catch (Exception e)
|
||||
{
|
||||
Console.WriteLine("ERROR: Could not include {0} - {1}", inc.Item2.ToString(), e.Message);
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
private bool CompareAcceptors(string accDir, bool add)
|
||||
{
|
||||
var tmpFile = Path.Combine(activeDirectory, TmpStreamFile);
|
||||
try
|
||||
{
|
||||
var di = new DirectoryInfo(Path.Combine(activeDirectory, accDir));
|
||||
if (!di.Exists)
|
||||
{
|
||||
Console.WriteLine("ERROR: Acceptor directory {0} does not exist", accDir);
|
||||
return false;
|
||||
}
|
||||
|
||||
var hashSet = new HashSet<string>();
|
||||
foreach (var fi in di.EnumerateFiles(AccFiles))
|
||||
{
|
||||
hashSet.Add(fi.Name);
|
||||
if (!IsDifferent(fi.FullName, tmpFile))
|
||||
{
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
||||
if (add)
|
||||
{
|
||||
var nextId = 0;
|
||||
string name = "";
|
||||
while (hashSet.Contains(name = string.Format("{0}_{1}{2}", AccPrefix, nextId, AccExt)))
|
||||
{
|
||||
++nextId;
|
||||
}
|
||||
|
||||
File.Copy(
|
||||
Path.Combine(activeDirectory, TmpStreamFile),
|
||||
Path.Combine(Path.Combine(activeDirectory, accDir), name));
|
||||
return true;
|
||||
}
|
||||
else
|
||||
{
|
||||
Console.WriteLine("ERROR: Output is not accepted");
|
||||
return false;
|
||||
}
|
||||
}
|
||||
catch (Exception e)
|
||||
{
|
||||
Console.WriteLine("ERROR: Could not compare acceptors - {0}", e.Message);
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
private bool Run(
|
||||
StreamWriter outStream,
|
||||
bool ignorePrompt,
|
||||
string exe,
|
||||
Tuple<OptValueKind, object>[] values)
|
||||
{
|
||||
var args = "";
|
||||
if (values != null)
|
||||
{
|
||||
foreach (var v in values)
|
||||
{
|
||||
args += v.Item2.ToString() + " ";
|
||||
}
|
||||
}
|
||||
|
||||
if (!ignorePrompt)
|
||||
{
|
||||
outStream.WriteLine("=================================");
|
||||
outStream.WriteLine(" Console output ");
|
||||
outStream.WriteLine("=================================");
|
||||
}
|
||||
|
||||
try
|
||||
{
|
||||
var psi = new ProcessStartInfo();
|
||||
psi.UseShellExecute = false;
|
||||
psi.RedirectStandardError = true;
|
||||
psi.RedirectStandardOutput = true;
|
||||
psi.WorkingDirectory = activeDirectory;
|
||||
psi.FileName = Path.Combine(activeDirectory, exe);
|
||||
psi.Arguments = args.Trim();
|
||||
psi.CreateNoWindow = true;
|
||||
|
||||
var process = new Process();
|
||||
process.StartInfo = psi;
|
||||
process.OutputDataReceived += (s, e) => OutputReceived(outStream, ignorePrompt, s, e);
|
||||
process.Start();
|
||||
process.BeginErrorReadLine();
|
||||
process.BeginOutputReadLine();
|
||||
process.WaitForExit();
|
||||
|
||||
Console.WriteLine("EXIT: {0}", process.ExitCode);
|
||||
outStream.WriteLine("EXIT: {0}", process.ExitCode);
|
||||
}
|
||||
catch (Exception e)
|
||||
{
|
||||
Console.WriteLine("ERROR: Failed to run command: {0}", e.Message);
|
||||
return false;
|
||||
}
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
private static void OutputReceived(
|
||||
StreamWriter outStream,
|
||||
bool ignorePrompt,
|
||||
object sender,
|
||||
DataReceivedEventArgs e)
|
||||
{
|
||||
if (ignorePrompt)
|
||||
{
|
||||
Console.WriteLine("OUT: {0}", e.Data);
|
||||
}
|
||||
else
|
||||
{
|
||||
outStream.WriteLine("OUT: {0}", e.Data);
|
||||
}
|
||||
}
|
||||
|
||||
private static bool IsDifferent(string file1, string file2)
|
||||
{
|
||||
int read1, read2;
|
||||
var buf1 = new char[BufferSize];
|
||||
var buf2 = new char[BufferSize];
|
||||
try
|
||||
{
|
||||
using (var sr1 = new StreamReader(file1))
|
||||
{
|
||||
using (var sr2 = new StreamReader(file2))
|
||||
{
|
||||
while (true)
|
||||
{
|
||||
read1 = sr1.ReadBlock(buf1, 0, BufferSize);
|
||||
read2 = sr2.ReadBlock(buf2, 0, BufferSize);
|
||||
if (read1 != read2)
|
||||
{
|
||||
return true;
|
||||
}
|
||||
|
||||
for (int i = 0; i < read1; ++i)
|
||||
{
|
||||
if (buf1[i] != buf2[i])
|
||||
{
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
||||
if (read1 == 0)
|
||||
{
|
||||
return false;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
catch
|
||||
{
|
||||
return true;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -0,0 +1,344 @@
|
|||
namespace Check
|
||||
{
|
||||
using System;
|
||||
using System.Collections.Generic;
|
||||
using System.Diagnostics.Contracts;
|
||||
using System.Linq;
|
||||
using System.Threading;
|
||||
|
||||
internal class OptionParser
|
||||
{
|
||||
private enum ParseState
|
||||
{
|
||||
SwStart = 0,
|
||||
SwStartCnt,
|
||||
SwName,
|
||||
SwNameOrEnd,
|
||||
SwEndOrVal,
|
||||
FirstVal,
|
||||
Next,
|
||||
IdVal,
|
||||
IntVal,
|
||||
StrValStart,
|
||||
StrValEnd,
|
||||
StrVal, //// A string without escapes '"..."'
|
||||
EStrVal, //// A string with escapes "..."
|
||||
EStrValEsc,
|
||||
Unhandled,
|
||||
NParseStates
|
||||
}
|
||||
|
||||
private static Func<char, char, Options, ParseState>[][] ParseTable =
|
||||
new Func<char, char, Options, ParseState>[(int)ParseState.NParseStates][];
|
||||
|
||||
static OptionParser()
|
||||
{
|
||||
ParseTable[(int)ParseState.SwStart] = new Func<char, char, Options, ParseState>[]
|
||||
{
|
||||
(c, la, opt) => c != '-'
|
||||
? ParseState.Unhandled
|
||||
: (la == '-'
|
||||
? ParseState.SwStartCnt
|
||||
: (IsIdStart(la) ? ParseState.SwName : ParseState.Unhandled)),
|
||||
(c, la, opt) => c == '/' && IsIdStart(la) ? ParseState.SwName : ParseState.Unhandled,
|
||||
(c, la, opt) => IsWhitespace(c) ? ParseState.SwStart : ParseState.Unhandled
|
||||
};
|
||||
|
||||
ParseTable[(int)ParseState.SwStartCnt] = new Func<char, char, Options, ParseState>[]
|
||||
{
|
||||
(c, la, opt) => Start(opt, null, ParseState.SwName)
|
||||
};
|
||||
|
||||
ParseTable[(int)ParseState.SwName] = new Func<char, char, Options, ParseState>[]
|
||||
{
|
||||
(c, la, opt) => !IsIdStart(c)
|
||||
? ParseState.Unhandled
|
||||
: (IsIdMiddle(la) ? Start(opt, null, ParseState.SwNameOrEnd, c)
|
||||
: SE(opt, null, ParseState.SwEndOrVal, c))
|
||||
};
|
||||
|
||||
ParseTable[(int)ParseState.SwNameOrEnd] = new Func<char, char, Options, ParseState>[]
|
||||
{
|
||||
(c, la, opt) => IsIdMiddle(la)
|
||||
? App(opt, ParseState.SwNameOrEnd, c)
|
||||
: AE(opt, ParseState.SwEndOrVal, c)
|
||||
};
|
||||
|
||||
ParseTable[(int)ParseState.SwEndOrVal] = new Func<char, char, Options, ParseState>[]
|
||||
{
|
||||
(c, la, opt) => c != '-'
|
||||
? ParseState.Unhandled
|
||||
: (la == '-'
|
||||
? ParseState.SwStartCnt
|
||||
: (IsIdStart(la) ? ParseState.SwName : ParseState.Unhandled)),
|
||||
(c, la, opt) => c == '/' && IsIdStart(la) ? ParseState.SwName : ParseState.Unhandled,
|
||||
(c, la, opt) => c == ':' ? ParseState.FirstVal : ParseState.Unhandled,
|
||||
(c, la, opt) => IsWhitespace(c) ? ParseState.SwEndOrVal : ParseState.Unhandled
|
||||
};
|
||||
|
||||
ParseTable[(int)ParseState.FirstVal] = new Func<char, char, Options, ParseState>[]
|
||||
{
|
||||
(c, la, opt) => !IsIdStart(c)
|
||||
? ParseState.Unhandled
|
||||
: (IsIdMiddle(la)
|
||||
? Start(opt, OptValueKind.Id, ParseState.IdVal, c)
|
||||
: SE(opt, OptValueKind.Id, ParseState.Next, c)),
|
||||
(c, la, opt) => !char.IsDigit(c)
|
||||
? ParseState.Unhandled
|
||||
: (char.IsDigit(la)
|
||||
? Start(opt, OptValueKind.Integer, ParseState.IntVal, c)
|
||||
: SE(opt, OptValueKind.Integer, ParseState.Next, c)),
|
||||
(c, la, opt) => c == '\"'
|
||||
? Start(opt, OptValueKind.String, ParseState.EStrVal)
|
||||
: ParseState.Unhandled,
|
||||
(c, la, opt) => c == '\'' && la == '\"'
|
||||
? Start(opt, OptValueKind.String, ParseState.StrValStart)
|
||||
: ParseState.Unhandled,
|
||||
(c, la, opt) => IsWhitespace(c) ? ParseState.FirstVal : ParseState.Unhandled
|
||||
};
|
||||
|
||||
ParseTable[(int)ParseState.IdVal] = new Func<char, char, Options, ParseState>[]
|
||||
{
|
||||
(c, la, opt) => IsIdMiddle(la)
|
||||
? App(opt, ParseState.IdVal, c)
|
||||
: AE(opt, ParseState.Next, c)
|
||||
};
|
||||
|
||||
ParseTable[(int)ParseState.IntVal] = new Func<char, char, Options, ParseState>[]
|
||||
{
|
||||
(c, la, opt) => char.IsDigit(la)
|
||||
? App(opt, ParseState.IntVal, c)
|
||||
: AE(opt, ParseState.Next, c)
|
||||
};
|
||||
|
||||
ParseTable[(int)ParseState.StrValStart] = new Func<char, char, Options, ParseState>[]
|
||||
{
|
||||
(c, la, opt) => ParseState.StrVal
|
||||
};
|
||||
|
||||
ParseTable[(int)ParseState.StrVal] = new Func<char, char, Options, ParseState>[]
|
||||
{
|
||||
(c, la, opt) => c == '\"' && la == '\''
|
||||
? ParseState.StrValEnd
|
||||
: App(opt, ParseState.StrVal, c)
|
||||
};
|
||||
|
||||
ParseTable[(int)ParseState.StrValEnd] = new Func<char, char, Options, ParseState>[]
|
||||
{
|
||||
(c, la, opt) => End(opt, ParseState.Next)
|
||||
};
|
||||
|
||||
ParseTable[(int)ParseState.EStrVal] = new Func<char, char, Options, ParseState>[]
|
||||
{
|
||||
(c, la, opt) => c == '\\' ? ParseState.EStrValEsc : ParseState.Unhandled,
|
||||
(c, la, opt) => c == '\"' ? End(opt, ParseState.Next) : App(opt, ParseState.EStrVal, c)
|
||||
};
|
||||
|
||||
ParseTable[(int)ParseState.EStrValEsc] = new Func<char, char, Options, ParseState>[]
|
||||
{
|
||||
(c, la, opt) => AppEsc(opt, ParseState.EStrVal, c)
|
||||
};
|
||||
|
||||
ParseTable[(int)ParseState.Next] = new Func<char, char, Options, ParseState>[]
|
||||
{
|
||||
(c, la, opt) => c != '-'
|
||||
? ParseState.Unhandled
|
||||
: (la == '-'
|
||||
? ParseState.SwStartCnt
|
||||
: (IsIdStart(la) ? ParseState.SwName : ParseState.Unhandled)),
|
||||
(c, la, opt) => c == '/' && IsIdStart(la) ? ParseState.SwName : ParseState.Unhandled,
|
||||
(c, la, opt) => c == ',' ? ParseState.FirstVal : ParseState.Unhandled,
|
||||
(c, la, opt) => IsWhitespace(c) ? ParseState.Next : ParseState.Unhandled
|
||||
};
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Attempts to parse the command line arguments contained in the environment.
|
||||
/// </summary>
|
||||
/// <returns></returns>
|
||||
public static bool Parse(
|
||||
out Options options,
|
||||
out int errPos,
|
||||
out string cmdStr)
|
||||
{
|
||||
var cmdLine = Environment.CommandLine.Trim();
|
||||
var exeName = Environment.GetCommandLineArgs()[0].Trim();
|
||||
|
||||
//// Need to find where the name of the exeName ends in
|
||||
//// the command line. The exeName is provided after
|
||||
//// command line escaping rules have been applied, so we cannot
|
||||
//// directly compare exeName with the unescaped cmdLine.
|
||||
//// This code uses an approximate logic that quotes are ignored
|
||||
//// in the transform from cmdLine -> exeName.
|
||||
|
||||
int i = 0, j = 0;
|
||||
char cExe, cCmd;
|
||||
while (i < cmdLine.Length)
|
||||
{
|
||||
cCmd = cmdLine[i];
|
||||
cExe = j < exeName.Length ? exeName[j] : '\0';
|
||||
|
||||
if (cCmd == '\"')
|
||||
{
|
||||
++i;
|
||||
}
|
||||
else if (j == 0 && cCmd == ' ')
|
||||
{
|
||||
//// Leading spaces in cmdLine can be ignored
|
||||
++i;
|
||||
}
|
||||
else if (cCmd == cExe)
|
||||
{
|
||||
++i;
|
||||
++j;
|
||||
}
|
||||
else if (j == exeName.Length)
|
||||
{
|
||||
|
||||
break;
|
||||
}
|
||||
else
|
||||
{
|
||||
cmdStr = cmdLine;
|
||||
errPos = i;
|
||||
options = new Options();
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
if (i == cmdLine.Length)
|
||||
{
|
||||
cmdStr = string.Empty;
|
||||
errPos = 0;
|
||||
options = new Options();
|
||||
return true;
|
||||
}
|
||||
|
||||
cmdStr = cmdLine.Substring(i);
|
||||
return Parse(cmdStr, out options, out errPos);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// A switch string can contain switches and flags.
|
||||
/// Flags have the form:
|
||||
/// -f or --flag
|
||||
/// Switches have the form:
|
||||
/// -s: val_1,...,val_n
|
||||
/// --switch: val_1,...,val_n
|
||||
/// where val_i is either an integer, quoted string, or bareword.
|
||||
/// </summary>
|
||||
public static bool Parse(string switchString,
|
||||
out Options options,
|
||||
out int errPos)
|
||||
{
|
||||
//// Contract.Requires(flags != null && switches != null && msgs != null);
|
||||
options = new Options();
|
||||
var state = ParseState.SwStart;
|
||||
char c, la = switchString[0];
|
||||
int last = switchString.Length - 1;
|
||||
Func<char, char, Options, ParseState>[] actions;
|
||||
for (int i = 0; i < switchString.Length; ++i)
|
||||
{
|
||||
c = la;
|
||||
la = i < last ? switchString[i + 1] : '\0';
|
||||
actions = ParseTable[(int)state];
|
||||
foreach (var a in actions)
|
||||
{
|
||||
if ((state = a(c, la, options)) != ParseState.Unhandled)
|
||||
{
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
if (state == ParseState.Unhandled)
|
||||
{
|
||||
errPos = i;
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
if (state == ParseState.FirstVal ||
|
||||
state == ParseState.StrValStart ||
|
||||
state == ParseState.StrVal ||
|
||||
state == ParseState.EStrVal ||
|
||||
state == ParseState.EStrValEsc ||
|
||||
!options.EndToken())
|
||||
{
|
||||
errPos = switchString.Length;
|
||||
return false;
|
||||
}
|
||||
|
||||
errPos = 0;
|
||||
return true;
|
||||
}
|
||||
|
||||
private static bool IsWhitespace(char c)
|
||||
{
|
||||
return char.IsWhiteSpace(c) || c == '\0';
|
||||
}
|
||||
|
||||
private static bool IsIdStart(char c)
|
||||
{
|
||||
return char.IsLetter(c) || c == '_';
|
||||
}
|
||||
|
||||
private static bool IsIdMiddle(char c)
|
||||
{
|
||||
return char.IsLetterOrDigit(c) || c == '_';
|
||||
}
|
||||
|
||||
private static ParseState Start(Options opt, OptValueKind? kind, ParseState next, char c = '\0')
|
||||
{
|
||||
opt.StartToken(kind, c);
|
||||
return next;
|
||||
}
|
||||
|
||||
private static ParseState App(Options opt, ParseState next, char c)
|
||||
{
|
||||
opt.AppendToken(c);
|
||||
return next;
|
||||
}
|
||||
|
||||
private static ParseState End(Options opt, ParseState next)
|
||||
{
|
||||
return opt.EndToken() ? next : ParseState.Unhandled;
|
||||
}
|
||||
|
||||
private static ParseState SE(Options opt, OptValueKind? kind, ParseState next, char c = '\0')
|
||||
{
|
||||
opt.StartToken(kind, c);
|
||||
return opt.EndToken() ? next : ParseState.Unhandled;
|
||||
}
|
||||
|
||||
private static ParseState AE(Options opt, ParseState next, char c)
|
||||
{
|
||||
opt.AppendToken(c);
|
||||
return opt.EndToken() ? next : ParseState.Unhandled;
|
||||
}
|
||||
|
||||
private static ParseState AppEsc(Options opt, ParseState next, char c)
|
||||
{
|
||||
switch (c)
|
||||
{
|
||||
case 'n':
|
||||
case 'N':
|
||||
opt.AppendToken('\n');
|
||||
break;
|
||||
case 'r':
|
||||
case 'R':
|
||||
opt.AppendToken('\r');
|
||||
break;
|
||||
case 't':
|
||||
case 'T':
|
||||
opt.AppendToken('\t');
|
||||
break;
|
||||
default:
|
||||
opt.AppendToken(c);
|
||||
break;
|
||||
}
|
||||
|
||||
return next;
|
||||
}
|
||||
|
||||
}
|
||||
}
|
||||
|
|
@ -0,0 +1,201 @@
|
|||
namespace Check
|
||||
{
|
||||
using System;
|
||||
using System.Collections.Generic;
|
||||
using System.Diagnostics.Contracts;
|
||||
using System.IO;
|
||||
using System.Linq;
|
||||
using System.Threading;
|
||||
|
||||
internal enum OptValueKind { Id, Integer, String }
|
||||
|
||||
internal class Options
|
||||
{
|
||||
private static readonly char[] OptDelims = new char[] { ':' };
|
||||
|
||||
private OptValueKind? kind = null;
|
||||
private string token = "";
|
||||
|
||||
private LinkedList<Tuple<string, LinkedList<Tuple<OptValueKind, object>>>> options =
|
||||
new LinkedList<Tuple<string, LinkedList<Tuple<OptValueKind, object>>>>();
|
||||
|
||||
public IEnumerable<Tuple<string, LinkedList<Tuple<OptValueKind, object>>>> OptionLists
|
||||
{
|
||||
get
|
||||
{
|
||||
return options;
|
||||
}
|
||||
}
|
||||
|
||||
public void StartToken(OptValueKind? kind, char c = '\0')
|
||||
{
|
||||
this.kind = kind;
|
||||
token = "";
|
||||
if (c != '\0')
|
||||
{
|
||||
token += c;
|
||||
}
|
||||
}
|
||||
|
||||
public void AppendToken(char c)
|
||||
{
|
||||
token += c;
|
||||
}
|
||||
|
||||
public bool EndToken()
|
||||
{
|
||||
if (token == "" && kind == null)
|
||||
{
|
||||
return true;
|
||||
}
|
||||
else if (kind == null)
|
||||
{
|
||||
options.AddLast(
|
||||
new Tuple<string, LinkedList<Tuple<OptValueKind, object>>>(
|
||||
token,
|
||||
new LinkedList<Tuple<OptValueKind, object>>()));
|
||||
}
|
||||
else if (kind == OptValueKind.Integer)
|
||||
{
|
||||
Contract.Assert(options.Count > 0);
|
||||
var opt = options.Last.Value.Item2;
|
||||
int i;
|
||||
if (!int.TryParse(token, out i))
|
||||
{
|
||||
return false;
|
||||
}
|
||||
|
||||
opt.AddLast(new Tuple<OptValueKind, object>((OptValueKind)kind, i));
|
||||
}
|
||||
else if (kind == OptValueKind.Id)
|
||||
{
|
||||
Contract.Assert(options.Count > 0);
|
||||
Contract.Assert(!string.IsNullOrEmpty(token));
|
||||
var opt = options.Last.Value.Item2;
|
||||
opt.AddLast(new Tuple<OptValueKind, object>((OptValueKind)kind, token));
|
||||
}
|
||||
else if (kind == OptValueKind.String)
|
||||
{
|
||||
Contract.Assert(options.Count > 0);
|
||||
var opt = options.Last.Value.Item2;
|
||||
opt.AddLast(new Tuple<OptValueKind, object>((OptValueKind)kind, token));
|
||||
}
|
||||
else
|
||||
{
|
||||
throw new NotImplementedException();
|
||||
}
|
||||
|
||||
token = "";
|
||||
kind = null;
|
||||
return true;
|
||||
}
|
||||
|
||||
public bool TryGetOptionsBesides(string[] options, out string[] besides)
|
||||
{
|
||||
var besidesList = new List<string>();
|
||||
foreach (var opt in this.options)
|
||||
{
|
||||
if (!options.Contains<string>(opt.Item1))
|
||||
{
|
||||
besidesList.Add(opt.Item1);
|
||||
}
|
||||
}
|
||||
|
||||
besides = besidesList.ToArray();
|
||||
return besides.Length > 0;
|
||||
}
|
||||
|
||||
public bool TryGetOption(string option, out Tuple<OptValueKind, object>[] values)
|
||||
{
|
||||
var valList = new List<Tuple<OptValueKind, object>>();
|
||||
bool isSet = false;
|
||||
|
||||
foreach (var opt in options)
|
||||
{
|
||||
if (opt.Item1 != option)
|
||||
{
|
||||
continue;
|
||||
}
|
||||
|
||||
isSet = true;
|
||||
if (opt.Item2 == null || opt.Item2.Count == 0)
|
||||
{
|
||||
continue;
|
||||
}
|
||||
|
||||
valList.AddRange(opt.Item2);
|
||||
}
|
||||
|
||||
if (isSet)
|
||||
{
|
||||
values = valList.ToArray();
|
||||
return true;
|
||||
}
|
||||
else
|
||||
{
|
||||
values = null;
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
public bool LoadMore(string activeDirectory, string optFile)
|
||||
{
|
||||
try
|
||||
{
|
||||
using (var sr = new StreamReader(Path.Combine(activeDirectory, optFile)))
|
||||
{
|
||||
string line;
|
||||
int lineNum = 0;
|
||||
while (!sr.EndOfStream)
|
||||
{
|
||||
++lineNum;
|
||||
line = sr.ReadLine().Trim();
|
||||
if (string.IsNullOrEmpty(line) || line[0] == ';')
|
||||
{
|
||||
continue;
|
||||
}
|
||||
|
||||
var splits = line.Split(OptDelims, 2);
|
||||
if (splits.Length != 2)
|
||||
{
|
||||
Console.WriteLine(
|
||||
"ERROR: Could not parse options file {0} at line {1}",
|
||||
optFile,
|
||||
lineNum);
|
||||
return false;
|
||||
}
|
||||
|
||||
splits[0] = splits[0].Trim();
|
||||
if (string.IsNullOrEmpty(splits[0]))
|
||||
{
|
||||
Console.WriteLine(
|
||||
"ERROR: Could not parse options file {0} at line {1}",
|
||||
optFile,
|
||||
lineNum);
|
||||
return false;
|
||||
}
|
||||
|
||||
var optVals = new LinkedList<Tuple<OptValueKind, object>>();
|
||||
options.AddLast(
|
||||
new Tuple<string, LinkedList<Tuple<OptValueKind, object>>>(
|
||||
splits[0],
|
||||
optVals));
|
||||
|
||||
splits[1] = splits[1].Trim();
|
||||
if (!string.IsNullOrEmpty(splits[1]))
|
||||
{
|
||||
optVals.AddLast(new Tuple<OptValueKind, object>(OptValueKind.String, splits[1]));
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
catch (Exception e)
|
||||
{
|
||||
Console.WriteLine("ERROR: Could not load options file {0} - {1}", optFile, e.Message);
|
||||
return false;
|
||||
}
|
||||
|
||||
return true;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -0,0 +1,23 @@
|
|||
namespace Check
|
||||
{
|
||||
using System;
|
||||
using System.Collections.Generic;
|
||||
using System.Diagnostics;
|
||||
using System.IO;
|
||||
using System.Linq;
|
||||
using System.Text;
|
||||
using System.Threading.Tasks;
|
||||
|
||||
internal class Program
|
||||
{
|
||||
private const int FailCode = 1;
|
||||
public static void Main(string[] args)
|
||||
{
|
||||
var checker = new Checker(Environment.CurrentDirectory);
|
||||
if (!checker.Check())
|
||||
{
|
||||
Environment.ExitCode = FailCode;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -0,0 +1,36 @@
|
|||
using System.Reflection;
|
||||
using System.Runtime.CompilerServices;
|
||||
using System.Runtime.InteropServices;
|
||||
|
||||
// General Information about an assembly is controlled through the following
|
||||
// set of attributes. Change these attribute values to modify the information
|
||||
// associated with an assembly.
|
||||
[assembly: AssemblyTitle("Check")]
|
||||
[assembly: AssemblyDescription("")]
|
||||
[assembly: AssemblyConfiguration("")]
|
||||
[assembly: AssemblyCompany("")]
|
||||
[assembly: AssemblyProduct("Check")]
|
||||
[assembly: AssemblyCopyright("Copyright © 2013")]
|
||||
[assembly: AssemblyTrademark("")]
|
||||
[assembly: AssemblyCulture("")]
|
||||
|
||||
// Setting ComVisible to false makes the types in this assembly not visible
|
||||
// to COM components. If you need to access a type in this assembly from
|
||||
// COM, set the ComVisible attribute to true on that type.
|
||||
[assembly: ComVisible(false)]
|
||||
|
||||
// The following GUID is for the ID of the typelib if this project is exposed to COM
|
||||
[assembly: Guid("d7982aa6-55b5-444c-8714-b682be4d6365")]
|
||||
|
||||
// Version information for an assembly consists of the following four values:
|
||||
//
|
||||
// Major Version
|
||||
// Minor Version
|
||||
// Build Number
|
||||
// Revision
|
||||
//
|
||||
// You can specify all the values or you can default the Build and Revision Numbers
|
||||
// by using the '*' as shown below:
|
||||
// [assembly: AssemblyVersion("1.0.*")]
|
||||
[assembly: AssemblyVersion("1.0.0.0")]
|
||||
[assembly: AssemblyFileVersion("1.0.0.0")]
|
||||
|
|
@ -0,0 +1,6 @@
|
|||
<?xml version="1.0" encoding="utf-8" ?>
|
||||
<configuration>
|
||||
<startup>
|
||||
<supportedRuntime version="v4.0" sku=".NETFramework,Version=v4.5" />
|
||||
</startup>
|
||||
</configuration>
|
||||
|
|
@ -0,0 +1,71 @@
|
|||
namespace Test
|
||||
{
|
||||
using System;
|
||||
using System.Collections.Generic;
|
||||
using System.IO;
|
||||
using System.Linq;
|
||||
using System.Text;
|
||||
using System.Threading.Tasks;
|
||||
|
||||
class Program
|
||||
{
|
||||
private const int FailCode = 1;
|
||||
private const string TestFilePattern = "testconfig*.txt";
|
||||
|
||||
static void Main(string[] args)
|
||||
{
|
||||
try
|
||||
{
|
||||
if (args.Length > 1)
|
||||
{
|
||||
Console.WriteLine("USAGE: Test.exe [root dir]");
|
||||
}
|
||||
|
||||
DirectoryInfo di = args.Length == 0
|
||||
? new DirectoryInfo(Environment.CurrentDirectory)
|
||||
: new DirectoryInfo(Path.Combine(Environment.CurrentDirectory, args[0]));
|
||||
|
||||
if (!di.Exists)
|
||||
{
|
||||
Console.WriteLine("Failed to run tests; directory {0} does not exist", di.FullName);
|
||||
Environment.ExitCode = FailCode;
|
||||
return;
|
||||
}
|
||||
|
||||
Console.WriteLine("Running tests under {0}...", di.FullName);
|
||||
int testCount = 0, failCount = 0;
|
||||
Test(di, ref testCount, ref failCount);
|
||||
|
||||
Console.WriteLine();
|
||||
Console.WriteLine("Total tests: {0}, Passed tests: {1}. Failed tests: {2}", testCount, testCount - failCount, failCount);
|
||||
if (failCount > 0)
|
||||
{
|
||||
Environment.ExitCode = FailCode;
|
||||
}
|
||||
}
|
||||
catch (Exception e)
|
||||
{
|
||||
Console.WriteLine("Failed to run tests - {0}", e.Message);
|
||||
Environment.ExitCode = FailCode;
|
||||
}
|
||||
}
|
||||
|
||||
private static void Test(DirectoryInfo di, ref int testCount, ref int failCount)
|
||||
{
|
||||
foreach (var fi in di.EnumerateFiles(TestFilePattern))
|
||||
{
|
||||
++testCount;
|
||||
var checker = new Check.Checker(di.FullName);
|
||||
if (!checker.Check(fi.Name))
|
||||
{
|
||||
++failCount;
|
||||
}
|
||||
}
|
||||
|
||||
foreach (var dp in di.EnumerateDirectories())
|
||||
{
|
||||
Test(dp, ref testCount, ref failCount);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -0,0 +1,36 @@
|
|||
using System.Reflection;
|
||||
using System.Runtime.CompilerServices;
|
||||
using System.Runtime.InteropServices;
|
||||
|
||||
// General Information about an assembly is controlled through the following
|
||||
// set of attributes. Change these attribute values to modify the information
|
||||
// associated with an assembly.
|
||||
[assembly: AssemblyTitle("Test")]
|
||||
[assembly: AssemblyDescription("")]
|
||||
[assembly: AssemblyConfiguration("")]
|
||||
[assembly: AssemblyCompany("")]
|
||||
[assembly: AssemblyProduct("Test")]
|
||||
[assembly: AssemblyCopyright("Copyright © 2013")]
|
||||
[assembly: AssemblyTrademark("")]
|
||||
[assembly: AssemblyCulture("")]
|
||||
|
||||
// Setting ComVisible to false makes the types in this assembly not visible
|
||||
// to COM components. If you need to access a type in this assembly from
|
||||
// COM, set the ComVisible attribute to true on that type.
|
||||
[assembly: ComVisible(false)]
|
||||
|
||||
// The following GUID is for the ID of the typelib if this project is exposed to COM
|
||||
[assembly: Guid("7308b59d-a187-44b3-8512-d4dba11652e7")]
|
||||
|
||||
// Version information for an assembly consists of the following four values:
|
||||
//
|
||||
// Major Version
|
||||
// Minor Version
|
||||
// Build Number
|
||||
// Revision
|
||||
//
|
||||
// You can specify all the values or you can default the Build and Revision Numbers
|
||||
// by using the '*' as shown below:
|
||||
// [assembly: AssemblyVersion("1.0.*")]
|
||||
[assembly: AssemblyVersion("1.0.0.0")]
|
||||
[assembly: AssemblyFileVersion("1.0.0.0")]
|
||||
|
|
@ -0,0 +1,64 @@
|
|||
<?xml version="1.0" encoding="utf-8"?>
|
||||
<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
|
||||
<Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />
|
||||
<PropertyGroup>
|
||||
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
|
||||
<Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
|
||||
<ProjectGuid>{9C59ADEB-531C-46F3-AF36-4F39C84488D7}</ProjectGuid>
|
||||
<OutputType>Exe</OutputType>
|
||||
<AppDesignerFolder>Properties</AppDesignerFolder>
|
||||
<RootNamespace>Test</RootNamespace>
|
||||
<AssemblyName>Test</AssemblyName>
|
||||
<TargetFrameworkVersion>v4.5</TargetFrameworkVersion>
|
||||
<FileAlignment>512</FileAlignment>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
|
||||
<PlatformTarget>AnyCPU</PlatformTarget>
|
||||
<DebugSymbols>true</DebugSymbols>
|
||||
<DebugType>full</DebugType>
|
||||
<Optimize>false</Optimize>
|
||||
<OutputPath>bin\Debug\</OutputPath>
|
||||
<DefineConstants>DEBUG;TRACE</DefineConstants>
|
||||
<ErrorReport>prompt</ErrorReport>
|
||||
<WarningLevel>4</WarningLevel>
|
||||
</PropertyGroup>
|
||||
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
|
||||
<PlatformTarget>AnyCPU</PlatformTarget>
|
||||
<DebugType>pdbonly</DebugType>
|
||||
<Optimize>true</Optimize>
|
||||
<OutputPath>bin\Release\</OutputPath>
|
||||
<DefineConstants>TRACE</DefineConstants>
|
||||
<ErrorReport>prompt</ErrorReport>
|
||||
<WarningLevel>4</WarningLevel>
|
||||
</PropertyGroup>
|
||||
<ItemGroup>
|
||||
<Reference Include="System" />
|
||||
<Reference Include="System.Core" />
|
||||
<Reference Include="System.Xml.Linq" />
|
||||
<Reference Include="System.Data.DataSetExtensions" />
|
||||
<Reference Include="Microsoft.CSharp" />
|
||||
<Reference Include="System.Data" />
|
||||
<Reference Include="System.Xml" />
|
||||
</ItemGroup>
|
||||
<ItemGroup>
|
||||
<Compile Include="Program.cs" />
|
||||
<Compile Include="Properties\AssemblyInfo.cs" />
|
||||
</ItemGroup>
|
||||
<ItemGroup>
|
||||
<None Include="App.config" />
|
||||
</ItemGroup>
|
||||
<ItemGroup>
|
||||
<ProjectReference Include="..\Check\Check.csproj">
|
||||
<Project>{e9014c29-75c5-4484-a4d3-63ca735fd3ff}</Project>
|
||||
<Name>Check</Name>
|
||||
</ProjectReference>
|
||||
</ItemGroup>
|
||||
<Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
|
||||
<!-- To modify your build process, add your task inside one of the targets below and uncomment it.
|
||||
Other similar extension points exist, see Microsoft.Common.targets.
|
||||
<Target Name="BeforeBuild">
|
||||
</Target>
|
||||
<Target Name="AfterBuild">
|
||||
</Target>
|
||||
-->
|
||||
</Project>
|
||||
|
|
@ -0,0 +1,38 @@
|
|||
|
||||
Microsoft Visual Studio Solution File, Format Version 12.00
|
||||
# Visual Studio 2012
|
||||
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Test", "Test.csproj", "{9C59ADEB-531C-46F3-AF36-4F39C84488D7}"
|
||||
EndProject
|
||||
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Check", "..\Check\Check.csproj", "{E9014C29-75C5-4484-A4D3-63CA735FD3FF}"
|
||||
EndProject
|
||||
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "LittleFuncLang", "..\..\Tests\API\LittleFuncLang\LittleFuncLang.csproj", "{89DEB961-3DF1-4826-852A-69EDFF62632D}"
|
||||
EndProject
|
||||
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ListParser", "..\..\Tests\Parsers\ListParser\ListParser.csproj", "{ED7B13FC-FDCD-4230-A404-8EF9CFF7E321}"
|
||||
EndProject
|
||||
Global
|
||||
GlobalSection(SolutionConfigurationPlatforms) = preSolution
|
||||
Debug|Any CPU = Debug|Any CPU
|
||||
Release|Any CPU = Release|Any CPU
|
||||
EndGlobalSection
|
||||
GlobalSection(ProjectConfigurationPlatforms) = postSolution
|
||||
{9C59ADEB-531C-46F3-AF36-4F39C84488D7}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
|
||||
{9C59ADEB-531C-46F3-AF36-4F39C84488D7}.Debug|Any CPU.Build.0 = Debug|Any CPU
|
||||
{9C59ADEB-531C-46F3-AF36-4F39C84488D7}.Release|Any CPU.ActiveCfg = Release|Any CPU
|
||||
{9C59ADEB-531C-46F3-AF36-4F39C84488D7}.Release|Any CPU.Build.0 = Release|Any CPU
|
||||
{E9014C29-75C5-4484-A4D3-63CA735FD3FF}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
|
||||
{E9014C29-75C5-4484-A4D3-63CA735FD3FF}.Debug|Any CPU.Build.0 = Debug|Any CPU
|
||||
{E9014C29-75C5-4484-A4D3-63CA735FD3FF}.Release|Any CPU.ActiveCfg = Release|Any CPU
|
||||
{E9014C29-75C5-4484-A4D3-63CA735FD3FF}.Release|Any CPU.Build.0 = Release|Any CPU
|
||||
{89DEB961-3DF1-4826-852A-69EDFF62632D}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
|
||||
{89DEB961-3DF1-4826-852A-69EDFF62632D}.Debug|Any CPU.Build.0 = Debug|Any CPU
|
||||
{89DEB961-3DF1-4826-852A-69EDFF62632D}.Release|Any CPU.ActiveCfg = Release|Any CPU
|
||||
{89DEB961-3DF1-4826-852A-69EDFF62632D}.Release|Any CPU.Build.0 = Release|Any CPU
|
||||
{ED7B13FC-FDCD-4230-A404-8EF9CFF7E321}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
|
||||
{ED7B13FC-FDCD-4230-A404-8EF9CFF7E321}.Debug|Any CPU.Build.0 = Debug|Any CPU
|
||||
{ED7B13FC-FDCD-4230-A404-8EF9CFF7E321}.Release|Any CPU.ActiveCfg = Release|Any CPU
|
||||
{ED7B13FC-FDCD-4230-A404-8EF9CFF7E321}.Release|Any CPU.Build.0 = Release|Any CPU
|
||||
EndGlobalSection
|
||||
GlobalSection(SolutionProperties) = preSolution
|
||||
HideSolutionNode = FALSE
|
||||
EndGlobalSection
|
||||
EndGlobal
|
||||
Загрузка…
Ссылка в новой задаче