/**
* Format check a term against an RTG
*
* This format checker supports any normalized RTG (defined by TATA),
* including non-deterministic ones. The checker also supports injections.
*
* @author Martin Bravenboer <martin.bravenboer@gmail.com>
*/
module stratego/rtg/format-check
imports
libstratego-lib
stratego/rtg/signature
stratego/rtg/util
/**
* Main invocation
*/
strategies
/**
* Checks that the current term has the format of the given RTG.
*
* Fails if the current term has an incorrect format.
* Does not report errors.
*
* @param RTG
* @type a -> a
*/
rtg-format-check(|rtg) =
rtg-format-check(false, true | rtg)
/**
* Checks that the current term has the format of one of the specified start non-terminals.
*
* Fails if the current term has an incorrect format.
* Does not report errors.
*
* @param RTG
* @type a -> a
*/
rtg-format-check(|rtg, starts) =
rtg-format-check(false, true | rtg, starts)
/**
* Checks that the current term has the format of the given RTG.
*
* @param Report errors (true/false)
* @param Fail if incorrect format (true/false)
* @param RTG
* @type a -> a
*/
rtg-format-check(report-errors, fail-on-error | rtg ) =
rtg-format-check(report-errors, fail-on-error | rtg, <?RTG(Start(<id>), _)> rtg)
/**
* Checks that the current term has the format of one of the specified start non-terminals.
*
* @param Report errors (true/false)
* @param Fail if incorrect format (true/false)
* @param RTG
* @param List(NonTerm)
* @type a -> a
*/
rtg-format-check(report-errors, fail-on-error | rtg, starts) =
where(
tbl := <new-hashtable>
; set := <new-iset>
)
; finally(
rtgfc-type(|rtg, tbl, set)
; if report-errors then
where(rtgfc-format-check-report(|rtg, tbl, set))
end
; if fail-on-error then
where(rtgfc-format-check-error(|starts, tbl, set))
end
, <hashtable-destroy> tbl
; <iset-destroy> set
)
strategies
/**
* Infers the types of all terms.
* This strategy does not fail if some of the terms has no type.
*
* @param RTG
*/
rtgfc-type(|rtg, tbl, set) =
{| rtgfc-InjUserType
, rtgfc-ListUserType
, rtgfc-OptUserType
, rtgfc-TupleUserType
, rtgfc-IntAppl
, rtgfc-StringAppl
, rtgfc-ApplUserType :
where(<rtgfc-generate-type-rules> rtg)
; rtgfc-format-check(|tbl, set)
|}
/**
* Main format check traversal.
*
* The first alternatives reuses the result of previous
* type checking. The size of the traversal is therefore the
* size of the maximal shared tree.
*
* The second alternative tries to infer as many types
* as possible, but at least one.
*
* If this fails, then the term is not in the right format.
*
* @type starts List(NonTerm)
*/
rtgfc-format-check(|tbl, set) =
where(
<repeat(rtgfc-Type(|tbl, set))> ""
; <repeat(rtgfc-Type(|tbl, set))> 0
)
; bottomup-consnil(
where(rtgfc-get-types(|tbl, set))
<+ repeat1(rtgfc-Type(|tbl, set))
; rtgfc-report-types(|tbl, set)
<+ one-consnil(not(rtgfc-is-typed(|tbl, set)))
<+ rtgfc-report-type-failure(id | tbl, set)
)
rtgfc-type-string(|tbl, set) =
is-string; rtgfc-type-special(|"", tbl, set)
rtgfc-type-int(|tbl, set) =
is-int; rtgfc-type-special(|0, tbl, set)
rtgfc-type-special(|special, tbl, set) =
?t
; where(
<rtgfc-get-types(|tbl, set)> special => types
; <hashtable-put(|t, types)> tbl
; <map({type:
?type
; <iset-add(|(t, type))> set
})> types
)
rtgfc-is-typed(|tbl, set) =
where(rtgfc-get-types(|tbl, set) => [_ | _])
/**
* Define type rules for the productions of an RTG.
*
* Type rules are defined in a dynamic rule 'UserType'.
*/
strategies
/**
* Generate format checking dynamic rules for an RTG
*
* @type RTG -> _
*/
rtgfc-generate-type-rules =
rtg-ungroup-productions
; ?RTG(Start(_), ProdRules(<id>))
; map(rtgfc-generate-type-rule <+ debug(!"internal error: cannot create type rule for "); fail)
; if oncetd(?Ref(Int())) then
rtgfc-generate-type-rule-deprecated-int
end
; if oncetd(?Ref(String())) then
rtgfc-generate-type-rule-deprecated-string
end
/**
* Int application
*/
rtgfc-generate-type-rule =
?ProdRule(a, [Appl(IntTerm(), [])])
; rules(
rtgfc-IntAppl(|tbl, set) :+ t -> t
where
<is-int> t
; rtgfc-new-type(|a, tbl, set)
)
/**
* String application
*/
rtgfc-generate-type-rule =
?ProdRule(a, [Appl(StringTerm(), [])])
; rules(
rtgfc-StringAppl(|tbl, set) :+ t -> t
where
<is-string> t
; rtgfc-new-type(|a, tbl, set)
)
/**
* Deprecated
*/
rtgfc-generate-type-rule-deprecated-int =
rules(
rtgfc-IntAppl(|tbl, set) :+ t -> t
where
<is-int> t
; rtgfc-new-type(|Int(), tbl, set)
)
/**
* Deprecated
*/
rtgfc-generate-type-rule-deprecated-string =
rules(
rtgfc-StringAppl(|tbl, set) :+ t -> t
where
<is-string> t
; rtgfc-new-type(|String(), tbl, set)
)
/**
* Injection
*/
rtgfc-generate-type-rule =
?ProdRule(b, [Ref(a)])
; rules(
rtgfc-InjUserType(|tbl, set) :+ t -> t
where
<rtgfc-has-type(|a, tbl, set)> t
; <not(rtgfc-has-type(|b, tbl, set))> t
; <rtgfc-set-type(|b, tbl, set)> t
)
/**
* Cons application
*/
rtgfc-generate-type-rule =
?ProdRule(c, [Appl(ConsTerm(), [Ref(a), Ref(b)])])
; rules(
rtgfc-ListUserType(|tbl, set) :+ t@[hd | tl] -> t
where
<rtgfc-has-type(|b, tbl, set)> tl
; <not(rtgfc-has-type(|c, tbl, set))> t
; <rtgfc-has-type(|a, tbl, set)> hd
; <rtgfc-set-type(|c, tbl, set)> t
)
/**
* Conc application
*/
rtgfc-generate-type-rule =
?ProdRule(c, [Appl(ConcTerm(), [Ref(a), Ref(b)])])
; rules(
rtgfc-ListUserType(|tbl, set) :+ t@Conc(t1, t2) -> t
where
<rtgfc-has-type(|a, tbl, set)> t1
; <rtgfc-has-type(|b, tbl, set)> t2
; <rtgfc-new-type(|c, tbl, set)> t
)
/**
* Nil application
*/
rtgfc-generate-type-rule =
?ProdRule(a, [Appl(NilTerm(), [])])
; rules(
rtgfc-ListUserType(|tbl, set) :+ [] -> []
where
<rtgfc-new-type(|a, tbl, set)> []
)
/**
* Some application
*/
rtgfc-generate-type-rule =
?ProdRule(b, [Appl(SomeTerm(), [Ref(a)])])
; rules(
rtgfc-OptUserType(|tbl, set) :+ Some(t) -> Some(t)
where
<rtgfc-has-type(|a, tbl, set)> t
; <rtgfc-new-type(|b, tbl, set)> Some(t)
)
/**
* None application
*/
rtgfc-generate-type-rule =
?ProdRule(a, [Appl(NoneTerm(), [])])
; rules(
rtgfc-OptUserType(|tbl, set) :+ None() -> None()
where
<rtgfc-new-type(|a, tbl, set)> None()
)
/**
* Tuple application
*/
rtgfc-generate-type-rule =
?ProdRule(a, [Appl(TupleTerm(_), as)])
; where(<map(?Ref(<id>))> as => arg-types)
; rules(
rtgfc-TupleUserType(|tbl, set) :+ t@""#(args) -> t
where
<not(rtgfc-has-type(|a, tbl, set))> t
; <rtgfc-list-has-type(|arg-types, tbl, set)> args
; <rtgfc-set-type(|a, tbl, set)> t
)
/**
* User-defined terminal application
*/
rtgfc-generate-type-rule =
?ProdRule(a, [Appl(Term(f), as)])
; where(<map(?Ref(<id>))> as => arg-types)
; rules(
rtgfc-ApplUserType(|tbl, set) :+ t@f#(args) -> t
where
<not(rtgfc-has-type(|a, tbl, set))> t
; <rtgfc-list-has-type(|arg-types, tbl, set)> args
; <rtgfc-set-type(|a, tbl, set)> t
)
/**
* @type List(_) -> _
* @type as List(NonTerm)
*/
rtgfc-list-has-type(|as, tbl, set) =
if ?[] then
!as => []
else
?[hd | tl]
; where(
!as => [a | bs]
; <rtgfc-has-type(|a, tbl, set)> hd
; <rtgfc-list-has-type(|bs, tbl, set)> tl
)
end
/**
* Type types a term.
*/
strategies
rtgfc-Type(|tbl, set) =
where(
rtgfc-IntAppl(|tbl, set)
+ rtgfc-StringAppl(|tbl, set)
+ rtgfc-InjUserType(|tbl, set)
+ rtgfc-ApplUserType(|tbl, set)
+ rtgfc-TupleUserType(|tbl, set)
+ rtgfc-ListUserType(|tbl, set)
+ rtgfc-OptUserType(|tbl, set)
)
strategies
/**
* Fails if t already has type nt
*
* @type t -> t
*/
rtgfc-new-type(|nt, tbl, set) =
?term
; where(
not(rtgfc-has-type(|nt, tbl, set))
; <hashtable-push(|term, nt)> tbl
; <iset-add(|(term, nt))> set
)
rtgfc-set-type(|nt, tbl, set) =
?term
; where(
<hashtable-push(|term, nt)> tbl
; <iset-add(|(term, nt))> set
)
/**
* Succeeds if t has type nt
*
* @type t -> t
*/
rtgfc-has-type(|nt, tbl, set) =
?term
; not(is-string + is-int)
; where(
<iset-contains(|(term, nt))> set
)
rtgfc-has-type(|nt, tbl, set) =
is-int
; where(<iset-contains(|(0, nt))> set)
rtgfc-has-type(|nt, tbl, set) =
is-string
; where(<iset-contains(|("", nt))> set)
rtgfc-retrieve-types(|tbl, set) =
rtgfc-get-types(|tbl, set)
<+ ?t
; where(
<hashtable-put(|t, [])> tbl
)
; ![]
rtgfc-get-types(|tbl, set) =
?t
; not(is-string + is-int)
; <hashtable-get(|t)> tbl
rtgfc-get-types(|tbl, set) =
is-int
; <hashtable-get(|0)> tbl
rtgfc-get-types(|tbl, set) =
is-string
; <hashtable-get(|"")> tbl
/**
* Reporting
*/
strategies
/**
* @param RTG or List(NonTerm)
*/
rtgfc-format-check-error(|rtg, tbl, set) =
where(starts := <?RTG(Start(<id>), _) <+ is-list> rtg)
; where(
types := <rtgfc-get-types(|tbl, set) <+ ![]>
; if <isect> (starts, types) => [] then
fail
end
)
/**
* @param RTG
*/
rtgfc-format-check-report(|rtg, tbl, set) =
where(starts := <?RTG(Start(<id>), _)> rtg)
; rtgfc-format-check-report(|starts, tbl ,set)
/**
* @param List(NonTerm)
*/
rtgfc-format-check-report(|starts, tbl, set) =
where(
<is-list> starts
; (rtgfc-get-types(|tbl, set) <+ ![]) => types
; if !types => [] then
!1 // already reported <fatal-error> ["error: term cannot be typed."]
else
<isect> (starts, <id>)
; if ?[] then
if-verbose1(
<fprintnl> (<stderr-stream>,
["error: term typed as ", <rtgfc-types-to-string> types,
" but expected ", <rtgfc-types-to-string> starts])
)
; !1
else
if-verbose2(
<rtgfc-types-to-string; debug(!"info: term typed as ")> types
)
; !0
end
end
; <set-config> ("--exit-code", <id>)
)
rtgfc-report-types(|tbl, set) = if-verbose2(
?term
; where(
rtgfc-get-types(|tbl, set)
; switch id
case ?[] :
![" Cannot type ", term]
case ?[t] :
![" Typed ", <write-to-string> term, " as ", <rtgfc-nonterm-to-string> t]
otherwise:
![" Typed ", <write-to-string> term, " as one of ", <rtgfc-types-to-string>]
end
; <fprintnl> (<stderr-stream>, <id>)
)
)
rtgfc-report-type-failure(finally | tbl, set) =
?t
; where(
<fprintnl> (<stderr-stream>, ["error: cannot type ", <write-to-string>])
)
; if <one-consnil(id)> t then
<fprintnl> (<stderr-stream>, [" inferred types of subterms: "])
; <all-consnil(
where(
<fprintnl> (<stderr-stream>, [" typed ", <write-to-string>, " as ", <rtgfc-retrieve-types(|tbl, set); rtgfc-types-to-string>])
)
)> t
else id end
; finally
rtgfc-nonterm-to-string =
?Set(<rtgfc-types-to-string>) <+ rtg-to-string
rtgfc-types-to-string =
map(rtg-to-string); separate-by(!", "); concat-strings
rtg-to-string :
Int() -> ""
rtg-to-string :
String() -> ""
strategies
/**
* @type List(a) -> List(b)
* @type s List(a) -> b
*/
map-consnil(s) =
rec x({tail:
?[_ | tail]
; s
; ![<id> | <x> tail]
<+ []
})
/**
* bttomup variant that traverses lists as cons/nil.
*/
bottomup-consnil(s) =
rec x(all-consnil(x); s)
/**
* all variant that traverses lists as cons/nil.
*/
all-consnil(s) =
is-list < ([s | s] + []) + all(s)
/**
* one variant that traverses lists as cons/nil.
*/
one-consnil(s) =
is-list < ([s | id] + [id | s]) + one(s)