-
Notifications
You must be signed in to change notification settings - Fork 2
/
ctor-var-unif.maude
59 lines (53 loc) · 2.71 KB
/
ctor-var-unif.maude
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
--- name: ctor-var-unif.maude
--- reqs: prelude, full-maude, decl.maude, sortify.maude, ctor-refine.maude
--- desc: This module has methods such that, given a term
--- and a Module that is FVP, sensible, and B-preregular,
--- and where its constructor subsignature is preregular
--- below the whole signature, then it has facilities
--- to compute sets of constructor variants, by computing
--- sets of most general constructor instances modulo B.
---
--- This constructor variant functionality is then
--- lifted to compute constructor unifiers through
--- an easy signature transformation.
--- This module computes most general constructor variants/unifiers;
--- Since this module relies on ctor-refine, the target module should
--- not rely on kinds anywhere in its defintion
fmod CTOR-VARIANT is
pr META-LEVEL .
pr MGCI .
pr TERMSET-FM .
pr EQ-VARIANT .
pr UNIFICATION-PROBLEM-AUX . --- UnifProbLHSToTL
pr HETEROGENEOUS-LIST-FUNCTOR . --- toHL, hl-func
op ctor-variants : Module Term -> VariantTripleSet .
op $ctor-variants : Module VariantTripleSet VariantTripleSet -> VariantTripleSet .
op ctor-unifiers : Module UnificationProblem ~> SubstitutionSet .
op $ctor-unifiers : Module Term SubstSetNatPair ~> SubstitutionSet .
var M : Module .
var T : Term .
var I : Nat .
var S S' : Substitution .
var SS : SubstitutionSet .
var VS VS' : VariantTripleSet .
var P : Parent .
var B : Bool .
var UP : UnificationProblem .
--- OUT: a set of constructor variants computed by computing all regular variants
--- and then copmuting their most general constructor instances of those terms
eq ctor-variants(M,T) = $ctor-variants(M,variants(M,T),empty) .
eq $ctor-variants(M,{T,S,I,P,B} | VS,VS') = $ctor-variants(M,VS,VS' | applySubs({T,S,I,P,B},mgci(M,T,s(I)))) .
eq $ctor-variants(M,empty,VS') = VS' .
--- OUT: a set of constructor variant unifiers computed by first computing all of the regular
--- variant unifiers and then:
--- [1] lifting the LHS of each unificand in the problem to a heterogeneous list in HL[M] module
--- [2] applying the regular unifiers to the lifted list
--- [3] computing the most general substitutions mapping the lifted list into constructors
--- [4] composing the constructor substitutions with their original unifiers
eq ctor-unifiers(M,UP) = $ctor-unifiers(hl-func(M),toHL(M,UnifProbLHSToTL(UP)),#var-unifiers(M,UP)) .
--- Apply steps [2-4] above where the SubstSetNatPair is all the standard variant unifiers
eq $ctor-unifiers(M,T,ssnp(S | SS,I)) =
(S << mgci(M,getTerm(metaReduce(M,T << S)),I)) |
$ctor-unifiers(M,T,ssnp(SS,I)) .
eq $ctor-unifiers(M,T,ssnp(empty,I)) = empty .
endfm