Skip to content

Commit

Permalink
Исправление форматирования и вспомогательных алгоритмов (#322)
Browse files Browse the repository at this point in the history
  • Loading branch information
VladisP committed May 15, 2021
1 parent 586f3ac commit 519aba8
Showing 1 changed file with 52 additions and 59 deletions.
111 changes: 52 additions & 59 deletions src/compiler/GenericMatch.ref
Original file line number Diff line number Diff line change
Expand Up @@ -525,43 +525,34 @@ AddCoordinateLabels {
}

AddCoordinateLabels-Helper {
((Symbol s.SymType e.SymInfo) e.Rest) s.CoordNumber
((Symbol s.SymType e.SymInfo) e.Rest) s.CoordNumber
= (Symbol s.SymType e.SymInfo) ('{'s.CoordNumber'}')
<AddCoordinateLabels-Helper (e.Rest) <Add s.CoordNumber 1>>;

((Var s.Mode e.Index) e.Rest) s.CoordNumber
= (Var s.Mode e.Index) ('{'s.CoordNumber'}')
<AddCoordinateLabels-Helper (e.Rest) <Add s.CoordNumber 1>>;

((ClosureBrackets e.Inner) e.Rest) s.CoordNumber
= (ClosureBrackets e.Inner) ('{'s.CoordNumber'}')
<AddCoordinateLabels-Helper (e.Rest) <Add s.CoordNumber 1>>;

((Brackets e.Expr) e.Rest) s.CoordNumber
= (Brackets ('{'s.CoordNumber'}')
= (Brackets ('{'s.CoordNumber'}')
<AddCoordinateLabels-Helper (e.Expr) <Add s.CoordNumber 1>>)
: {
(Brackets e.Inner ('{'s.LastCoord'}'))
= (Brackets e.Inner ('{'s.LastCoord'}'))
('{'<Add s.LastCoord 1>'}')
<AddCoordinateLabels-Helper (e.Rest) <Add s.LastCoord 2>>
};

/* ??? */
((ClosureBrackets (TkName e.Name) e.Expr) e.Rest) s.CoordNumber
= (ClosureBrackets ('{'s.CoordNumber'}')
(TkName e.Name) ('{'<Add s.CoordNumber 1>'}')
<AddCoordinateLabels-Helper (e.Expr) <Add s.CoordNumber 2>>)
: {
(ClosureBrackets e.Inner ('{'s.LastCoord'}'))
= (ClosureBrackets e.Inner ('{'s.LastCoord'}'))
= (Brackets e.Inner ('{'s.LastCoord'}'))
('{'<Add s.LastCoord 1>'}')
<AddCoordinateLabels-Helper (e.Rest) <Add s.LastCoord 2>>
};

((ADT-Brackets (e.Name) e.Expression) e.Rest) s.CoordNumber
= (ADT-Brackets ('{'s.CoordNumber'}')
(e.Name) ('{'<Add s.CoordNumber 1>'}')
<AddCoordinateLabels-Helper (e.Expression) <Add s.CoordNumber 2>>)
= (ADT-Brackets (e.Name) ('{'s.CoordNumber'}')
<AddCoordinateLabels-Helper (e.Expression) <Add s.CoordNumber 1>>)
: {
(ADT-Brackets e.Inner ('{'s.LastCoord'}'))
= (ADT-Brackets e.Inner ('{'s.LastCoord'}'))
= (ADT-Brackets e.Inner ('{'s.LastCoord'}'))
('{'<Add s.LastCoord 1>'}')
<AddCoordinateLabels-Helper (e.Rest) <Add s.LastCoord 2>>
};
Expand All @@ -573,7 +564,7 @@ AddCoordinateLabels-Helper {
/*
Упрощение координат (редуцирование их бессмысленного скопления)

<SimplifyCoordinates (t.Contr*) t.Clash* (t.Assign*)>
<SimplifyCoordinates (t.Contr*) t.Clash* (t.Assign*)>
== (t.Contr*) t.Clash^* (t.Assign^*)
*/

Expand All @@ -598,7 +589,7 @@ SimplifyCoordinates-Expr {
/* {k} {m} E {n} ↦ {m} E {n} */
('{'s.K'}') ('{'s.M'}') e.E ('{'s.N'}')
= <SimplifyCoordinates-Expr ('{'s.M'}') e.E ('{'s.N'}')>;

/* {k} E {m} {n} ↦ {k} E {m} */
('{'s.K'}') e.E ('{'s.M'}') ('{'s.N'}')
= <SimplifyCoordinates-Expr ('{'s.K'}') e.E ('{'s.M'}')>;
Expand All @@ -609,6 +600,8 @@ SimplifyCoordinates-Expr {

('{'s.M'}') e.E ('{'s.N'}')
= ('{'s.M'}') <SimplifyCoordinates-Expr-Inner e.E> ('{'s.N'}');

/* пусто */ = /* пусто */;
}

SimplifyCoordinates-Expr-Inner {
Expand All @@ -621,11 +614,11 @@ SimplifyCoordinates-Expr-Inner {
(Brackets <SimplifyCoordinates-Expr e.E>)
<SimplifyCoordinates-Expr-Inner e.End>;

e.Begin (ADT-Brackets e.E) e.End
e.Begin (ADT-Brackets (e.Name) e.E) e.End
= <SimplifyCoordinates-Expr-Inner e.Begin>
(ADT-Brackets <SimplifyCoordinates-Expr e.E>)
(ADT-Brackets (e.Name) <SimplifyCoordinates-Expr e.E>)
<SimplifyCoordinates-Expr-Inner e.End>;

e.E = e.E;
}

Expand All @@ -640,8 +633,8 @@ SimplifyCoordinates-Expr-Inner {

Solve-Aux-Spec {
/* {m} T {n} : t.X ↦ {m} T {n} ← t.X */
(e.UsedVars) (e.Contrs) e.ClashesStart
((('{'s.M'}') t.T ('{'s.N'}')) ':' (t.X))
(e.UsedVars) (e.Contrs) e.ClashesStart
((('{'s.M'}') t.T ('{'s.N'}')) ':' (t.X))
e.ClashesEnd (e.Assigns)
, <IsTerm t.T> : True
, t.X : (Var 't' e.Tindex)
Expand All @@ -651,10 +644,10 @@ Solve-Aux-Spec {
e.ClashesStart e.ClashesEnd
(e.Assigns (('{'s.M'}') t.T ('{'s.N'}') ':' t.X))
>;

/* {m} Sym {n} : s.X ↦ {m} Sym {n} ← s.X */
(e.UsedVars) (e.Contrs) e.ClashesStart
((('{'s.M'}') t.Sym ('{'s.N'}')) ':' (t.X))
(e.UsedVars) (e.Contrs) e.ClashesStart
((('{'s.M'}') t.Sym ('{'s.N'}')) ':' (t.X))
e.ClashesEnd (e.Assigns)
, <IsSVarSubset t.Sym> : True
, t.X : (Var 's' e.Sindex)
Expand All @@ -667,24 +660,24 @@ Solve-Aux-Spec {

/* {m} (E) {n} : (P) ↦ {m} E {n} : P */
(e.UsedVars) (e.Contrs) e.ClashesStart
((('{'s.M'}') t.L ('{'s.N'}')) ':' (t.R))
((('{'s.M'}') t.L ('{'s.N'}')) ':' (t.R))
e.ClashesEnd (e.Assigns)
, t.L : (Brackets e.LBody)
, t.R : (Brackets e.RBody)
= <Solve-Aux-Spec
(e.UsedVars)
(e.Contrs) e.ClashesStart
<SimplifyCoordinates-Clash
<SimplifyCoordinates-Clash
((('{'s.M'}') e.LBody ('{'s.N'}')) ':' (e.RBody))
>
e.ClashesEnd (e.Assigns)
>;

/* {m} [E] {n} : [P] ↦ {m} E {n} : P */
(e.UsedVars) (e.Contrs) e.ClashesStart
((('{'s.M'}') t.L ('{'s.N'}')) ':' (t.R))
((('{'s.M'}') t.L ('{'s.N'}')) ':' (t.R))
e.ClashesEnd (e.Assigns)
, t.L : (ADT-Brackets ('{'s.Coord'}') (e.Name) e.LBody)
, t.L : (ADT-Brackets (e.Name) e.LBody)
, t.R : (ADT-Brackets (e.Name) e.RBody)
= <Solve-Aux-Spec
(e.UsedVars)
Expand All @@ -707,29 +700,29 @@ Solve-Aux-Spec {
(e.UsedVars) (e.Contrs) e.ClashesStart
((('{'s.M'}') t.L ('{'s.N'}')) ':' (t.Psym))
e.ClashesEnd (e.Assigns)
, t.L : (ADT-Brackets ('{'s.Coord'}') (e.LName) e.LBody)
, t.L : (ADT-Brackets (e.LName) e.LBody)
, <IsSVarSubset t.Psym> : True
= /* нет решений */;

/* {m} Sym {n} : (P) ↦ нет решений */
(e.UsedVars) (e.Contrs) e.ClashesStart
((('{'s.M'}') t.Sym ('{'s.N'}')) ':' (t.R))
((('{'s.M'}') t.Sym ('{'s.N'}')) ':' (t.R))
e.ClashesEnd (e.Assigns)
, <IsSVarSubset t.Sym> : True
, t.R : (Brackets e.RBody)
= /* нет решений */;

/* {m} Sym {n} : [P] ↦ нет решений */
(e.UsedVars) (e.Contrs) e.ClashesStart
((('{'s.M'}') t.Sym ('{'s.N'}')) ':' (t.R))
((('{'s.M'}') t.Sym ('{'s.N'}')) ':' (t.R))
e.ClashesEnd (e.Assigns)
, <IsSVarSubset t.Sym> : True
, t.R : (ADT-Brackets (e.RName) e.RBody)
= /* нет решений */;

/* {m} t.X {n} : (P) ↦ t.X → (e.NEW) */
(e.UsedVars) (e.Contrs) e.ClashesStart
((('{'s.M'}') t.X ('{'s.N'}')) ':' (t.P))
((('{'s.M'}') t.X ('{'s.N'}')) ':' (t.P))
e.ClashesEnd (e.Assigns)
, t.X : (Var 't' e.Tindex)
, t.P : (Brackets e.PBody)
Expand All @@ -743,10 +736,10 @@ Solve-Aux-Spec {
e.ClashesEnd (e.Assigns)
>
>;

/* {m} t.X {n} : [P] ↦ t.X → [e.NEW] */
(e.UsedVars) (e.Contrs) e.ClashesStart
((('{'s.M'}') t.X ('{'s.N'}')) ':' (t.P))
((('{'s.M'}') t.X ('{'s.N'}')) ':' (t.P))
e.ClashesEnd (e.Assigns)
, t.X : (Var 't' e.Tindex)
, t.P : (ADT-Brackets (e.PName) e.PBody)
Expand All @@ -762,8 +755,8 @@ Solve-Aux-Spec {
>;

/* {m} t.X {n} : Psym ↦ t.X → s.NEW */
(e.UsedVars) (e.Contrs) e,ClashesStart
((('{'s.M'}') t.X ('{'s.N'}')) ':' (t.Psym))
(e.UsedVars) (e.Contrs) e.ClashesStart
((('{'s.M'}') t.X ('{'s.N'}')) ':' (t.Psym))
e.ClashesEnd (e.Assigns)
, t.X : (Var 't' e.Tindex)
, <IsSVarSubset t.Psym> : True
Expand All @@ -780,7 +773,7 @@ Solve-Aux-Spec {

/* {m} s.X {n} : X ↦ s.X → X */
(e.UsedVars) (e.Contrs) e.ClashesStart
((('{'s.M'}') t.X ('{'s.N'}')) ':' (t.S))
((('{'s.M'}') t.X ('{'s.N'}')) ':' (t.S))
e.ClashesEnd (e.Assigns)
, t.X : (Var 's' e.Sindex)
, t.S : (Symbol e._)
Expand All @@ -796,19 +789,19 @@ Solve-Aux-Spec {

/* {m} X {n} : X ↦ стираем */
(e.UsedVars) (e.Contrs) e.ClashesStart
((('{'s.M'}') t.X ('{'s.N'}')) ':' (t.X))
((('{'s.M'}') t.X ('{'s.N'}')) ':' (t.X))
e.ClashesEnd (e.Assigns)
, t.X : (Symbol e._)
= <Solve-Aux-Spec
(e.UsedVars)
(e.Contrs)
(e.UsedVars)
(e.Contrs)
e.ClashesStart e.ClashesEnd
(e.Assigns)
>;

/* {m} X {n} : Y ↦ нет решений */
(e.UsedVars) (e.Contrs) e.ClashesStart
((('{'s.M'}') t.X ('{'s.N'}')) ':' (t.Y))
((('{'s.M'}') t.X ('{'s.N'}')) ':' (t.Y))
e.ClashesEnd (e.Assigns)
, t.X : (Symbol e._)
, t.Y : (Symbol e._)
Expand All @@ -826,7 +819,7 @@ Solve-Aux-Spec {
((('{'s.N'}') e.E) ':' (e.P))
e.ClashesEnd (e.Assigns)
>;

/* E {m} T {n} : P Pt ↦ E {m} : P && {m} T {n} : Pt */
(e.UsedVars) (e.Contrs) e.ClashesStart
((e.E ('{'s.M'}') t.T ('{'s.N'}')) ':' (e.P t.Pt))
Expand All @@ -839,7 +832,7 @@ Solve-Aux-Spec {
((('{'s.M'}') t.T ('{'s.N'}')) ':' (t.Pt))
e.ClashesEnd (e.Assigns)
>;

/* {m} T E* {n} E : Pt P ↦ {m} T {n} : Pt && {m} E* {n} E : P */
(e.UsedVars) (e.Contrs) e.ClashesStart
((('{'s.M'}') t.T e.EInner ('{'s.N'}') e.EOuter) ':' (t.Pt e.P))
Expand Down Expand Up @@ -888,7 +881,7 @@ Solve-Aux-Spec {
(e.Contrs) e.ClashesStart
((('{'s.M'}') t.X e.E ('{'s.N'}')) ':' (t.Pt e.P))
e.ClashesEnd (e.Assigns)
>
>
: e.Branch2
= <Solve-Aux-Spec t.NewVars2 e.Branch1>
<Solve-Aux-Spec (e.UsedVars) e.Branch2>;
Expand All @@ -906,14 +899,14 @@ Solve-Aux-Spec {
(e.Contrs) e.ClashesStart
((('{'s.M'}') e.E t.X ('{'s.N'}')) ':' (e.P t.Pt))
e.ClashesEnd (e.Assigns)
>
>
: e.Branch1
= <AddContraction-Spec
(t.X ':' /* пусто */)
(e.Contrs) e.ClashesStart
((('{'s.M'}') e.E t.X ('{'s.N'}')) ':' (e.P t.Pt))
e.ClashesEnd (e.Assigns)
>
>
: e.Branch2
= <Solve-Aux-Spec t.NewVars2 e.Branch1>
<Solve-Aux-Spec (e.UsedVars) e.Branch2>;
Expand All @@ -924,11 +917,11 @@ Solve-Aux-Spec {
e.ClashesEnd (e.Assigns)
, t.X : (Var 'e' e.XIndex)
= <Solve-Aux-Spec
(e.UsedVars) (e.Contrs)
(e.UsedVars) (e.Contrs)
e.ClashesStart e.ClashesEnd
(e.Assigns (('{'s.M'}') e.E ('{'s.N'}') ':' t.X))
>;

/* {m} e.X E {n} : ε ↦ e.X → ε */
(e.UsedVars) (e.Contrs) e.ClashesStart
((('{'s.M'}') t.X e.E ('{'s.N'}')) ':' (/* пусто */))
Expand All @@ -950,7 +943,7 @@ Solve-Aux-Spec {
e.ClashesEnd (e.Assigns)
, <IsTerm t.T> : True
= /* решений нет */;

/* Продолжение следует...

(e.UsedVars) (e.Contrs) (e.Assigns)
Expand Down Expand Up @@ -1095,13 +1088,13 @@ IsFreeVariableSeq {
t.Other e.Rem = False
}

/*
Проверка на то, что выражение содержит
/*
Проверка на то, что выражение содержит
метки координат на верхнем уровне
*/

HasTopLevelCoordinateLabels {
e.Begin ('{'s.M'}') e.End = True;

e.Other = False
}

0 comments on commit 519aba8

Please sign in to comment.