CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-11-08 07:51:43 +03:00
Code Issues Projects Releases Wiki Activity

Preventing recursive type definitions

Browse Source
This commit is contained in:
Denis Merigoux 2020-12-06 12:32:36 +01:00
parent 8abe20849d
commit ee0cb1eefc
11 changed files with 206 additions and 33 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

165
src/catala/scope_language/dependency.ml
View File

@ -18,12 +18,12 @@
module Pos = Utils.Pos
module Errors = Utils.Errors
module Vertex = struct
module SVertex = struct
type t = Ast.ScopeName.t
let hash x = Ast.ScopeName.hash x
let compare = compare
let compare = Ast.ScopeName.compare
let equal x y = Ast.ScopeName.compare x y = 0
@ -31,7 +31,7 @@ module Vertex = struct
end
(** On the edges, the label is the expression responsible for the use of the function *)
module Edge = struct
module SEdge = struct
type t = Pos.t
let compare = compare
@ -39,15 +39,15 @@ module Edge = struct
let default = Pos.no_pos
end
module Dependencies = Graph.Persistent.Digraph.ConcreteBidirectionalLabeled (Vertex) (Edge)
module TopologicalTraversal = Graph.Topological.Make (Dependencies)
module SDependencies = Graph.Persistent.Digraph.ConcreteBidirectionalLabeled (SVertex) (SEdge)
module STopologicalTraversal = Graph.Topological.Make (SDependencies)
module SCC = Graph.Components.Make (Dependencies)
module SSCC = Graph.Components.Make (SDependencies)
(** Tarjan's stongly connected components algorithm, provided by OCamlGraph *)
let build_program_dep_graph (prgm : Ast.program) : Dependencies.t =
let g = Dependencies.empty in
let g = Ast.ScopeMap.fold (fun v _ g -> Dependencies.add_vertex g v) prgm.program_scopes g in
let build_program_dep_graph (prgm : Ast.program) : SDependencies.t =
let g = SDependencies.empty in
let g = Ast.ScopeMap.fold (fun v _ g -> SDependencies.add_vertex g v) prgm.program_scopes g in
Ast.ScopeMap.fold
(fun scope_name scope g ->
let subscopes =
@ -58,8 +58,10 @@ let build_program_dep_graph (prgm : Ast.program) : Dependencies.t =
| Ast.Call (subscope, subindex) ->
if subscope = scope_name then
Errors.raise_spanned_error
"The scope %a is calling into itself as a subscope, which is forbidden since \
Catala does not provide recursion"
(Format.asprintf
"The scope %a is calling into itself as a subscope, which is forbidden \
since Catala does not provide recursion"
Ast.ScopeName.format_t scope.Ast.scope_decl_name)
(Pos.get_position (Ast.ScopeName.get_info scope.Ast.scope_decl_name))
else
Ast.ScopeMap.add subscope
@ -69,15 +71,15 @@ let build_program_dep_graph (prgm : Ast.program) : Dependencies.t =
in
Ast.ScopeMap.fold
(fun subscope pos g ->
let edge = Dependencies.E.create subscope pos scope_name in
Dependencies.add_edge_e g edge)
let edge = SDependencies.E.create subscope pos scope_name in
SDependencies.add_edge_e g edge)
subscopes g)
prgm.program_scopes g
let check_for_cycle (g : Dependencies.t) : unit =
let check_for_cycle_in_scope (g : SDependencies.t) : unit =
(* if there is a cycle, there will be an strongly connected component of cardinality > 1 *)
let sccs = SCC.scc_list g in
if List.length sccs < Dependencies.nb_vertex g then
let sccs = SSCC.scc_list g in
if List.length sccs < SDependencies.nb_vertex g then
let scc = List.find (fun scc -> List.length scc > 1) sccs in
Errors.raise_multispanned_error "Cyclic dependency detected between scopes!"
(List.flatten
@ -86,7 +88,7 @@ let check_for_cycle (g : Dependencies.t) : unit =
let var_str, var_info =
(Format.asprintf "%a" Ast.ScopeName.format_t v, Ast.ScopeName.get_info v)
in
let succs = Dependencies.succ_e g v in
let succs = SDependencies.succ_e g v in
let _, edge_pos, succ = List.find (fun (_, _, succ) -> List.mem succ scc) succs in
let succ_str = Format.asprintf "%a" Ast.ScopeName.format_t succ in
[
@ -96,5 +98,130 @@ let check_for_cycle (g : Dependencies.t) : unit =
])
scc))
let get_scope_ordering (g : Dependencies.t) : Ast.ScopeName.t list =
List.rev (TopologicalTraversal.fold (fun sd acc -> sd :: acc) g [])
let get_scope_ordering (g : SDependencies.t) : Ast.ScopeName.t list =
List.rev (STopologicalTraversal.fold (fun sd acc -> sd :: acc) g [])
module TVertex = struct
type t = Struct of Ast.StructName.t | Enum of Ast.EnumName.t
let hash x = match x with Struct x -> Ast.StructName.hash x | Enum x -> Ast.EnumName.hash x
let compare x y =
match (x, y) with
| Struct x, Struct y -> Ast.StructName.compare x y
| Enum x, Enum y -> Ast.EnumName.compare x y
| Struct _, Enum _ -> 1
| Enum _, Struct _ -> -1
let equal x y =
match (x, y) with
| Struct x, Struct y -> Ast.StructName.compare x y = 0
| Enum x, Enum y -> Ast.EnumName.compare x y = 0
| _ -> false
let format_t (fmt : Format.formatter) (x : t) : unit =
match x with Struct x -> Ast.StructName.format_t fmt x | Enum x -> Ast.EnumName.format_t fmt x
let get_info (x : t) =
match x with Struct x -> Ast.StructName.get_info x | Enum x -> Ast.EnumName.get_info x
end
module TVertexSet = Set.Make (TVertex)
(** On the edges, the label is the expression responsible for the use of the function *)
module TEdge = struct
type t = Pos.t
let compare = compare
let default = Pos.no_pos
end
module TDependencies = Graph.Persistent.Digraph.ConcreteBidirectionalLabeled (TVertex) (TEdge)
module TTopologicalTraversal = Graph.Topological.Make (TDependencies)
module TSCC = Graph.Components.Make (TDependencies)
(** Tarjan's stongly connected components algorithm, provided by OCamlGraph *)
let rec get_structs_or_enums_in_type (t : Ast.typ Pos.marked) : TVertexSet.t =
match Pos.unmark t with
| Ast.TStruct s -> TVertexSet.singleton (TVertex.Struct s)
| Ast.TEnum e -> TVertexSet.singleton (TVertex.Enum e)
| Ast.TArrow (t1, t2) ->
TVertexSet.union (get_structs_or_enums_in_type t1) (get_structs_or_enums_in_type t2)
| Ast.TBool | Ast.TUnit | Ast.TInt -> TVertexSet.empty
let build_type_graph (structs : Ast.struct_ctx) (enums : Ast.enum_ctx) : TDependencies.t =
let g = TDependencies.empty in
let g =
Ast.StructMap.fold
(fun s fields g ->
List.fold_left
(fun g (_, typ) ->
let def = TVertex.Struct s in
let g = TDependencies.add_vertex g def in
let used = get_structs_or_enums_in_type typ in
TVertexSet.fold
(fun used g ->
if TVertex.equal used def then
Errors.raise_spanned_error
(Format.asprintf
"The type %a is defined using itself, which is forbidden since Catala does \
not provide recursive types"
TVertex.format_t used)
(Pos.get_position typ)
else
let edge = TDependencies.E.create used (Pos.get_position typ) def in
TDependencies.add_edge_e g edge)
used g)
g fields)
structs g
in
let g =
Ast.EnumMap.fold
(fun e cases g ->
List.fold_left
(fun g (_, typ) ->
let def = TVertex.Enum e in
let g = TDependencies.add_vertex g def in
let used = get_structs_or_enums_in_type typ in
TVertexSet.fold
(fun used g ->
if TVertex.equal used def then
Errors.raise_spanned_error
(Format.asprintf
"The type %a is defined using itself, which is forbidden since Catala does \
not provide recursive types"
TVertex.format_t used)
(Pos.get_position typ)
else
let edge = TDependencies.E.create used (Pos.get_position typ) def in
TDependencies.add_edge_e g edge)
used g)
g cases)
enums g
in
g
let check_type_cycles (structs : Ast.struct_ctx) (enums : Ast.enum_ctx) : unit =
let g = build_type_graph structs enums in
(* if there is a cycle, there will be an strongly connected component of cardinality > 1 *)
let sccs = TSCC.scc_list g in
if List.length sccs < TDependencies.nb_vertex g then
let scc = List.find (fun scc -> List.length scc > 1) sccs in
Errors.raise_multispanned_error "Cyclic dependency detected between types!"
(List.flatten
(List.map
(fun v ->
let var_str, var_info =
(Format.asprintf "%a" TVertex.format_t v, TVertex.get_info v)
in
let succs = TDependencies.succ_e g v in
let _, edge_pos, succ = List.find (fun (_, _, succ) -> List.mem succ scc) succs in
let succ_str = Format.asprintf "%a" TVertex.format_t succ in
[
(Some ("Cycle type " ^ var_str ^ ", declared:"), Pos.get_position var_info);
( Some ("Used here in the definition of another cycle type " ^ succ_str ^ ":"),
edge_pos );
])
scc))

3
src/catala/scope_language/scope_to_dcalc.ml
View File

@ -420,7 +420,8 @@ let build_scope_typ_from_sig (scope_sig : (Ast.ScopeVar.t * Dcalc.Ast.typ) list)
let translate_program (prgm : Ast.program) (top_level_scope_name : Ast.ScopeName.t) :
Dcalc.Ast.expr Pos.marked =
let scope_dependencies = Dependency.build_program_dep_graph prgm in
Dependency.check_for_cycle scope_dependencies;
Dependency.check_for_cycle_in_scope scope_dependencies;
Dependency.check_type_cycles prgm.program_structs prgm.program_enums;
let scope_ordering = Dependency.get_scope_ordering scope_dependencies in
let struct_ctx = prgm.program_structs in
let enum_ctx = prgm.program_enums in

2
syntax_highlighting/nv/atom/grammars/catala_nv.cson
View File

@ -100,7 +100,7 @@
'name' : 'keyword.control.catala_nv'
}
{
'match' : '\\b(scope|fun\\s+of|new|includes|set|type|option|struct|enume|param|rule|condition|data|ok|assert|def)\\b'
'match' : '\\b(scope|fun\\s+of|new|includes|set|type|option|struct|enum|param|rule|condition|data|ok|assert|def)\\b'
'name' : 'keyword.other.catala_nv'
}
{

2
syntax_highlighting/nv/catala_nv.iro
View File

@ -213,7 +213,7 @@ code : context {
}
: pattern {
regex \= \b(scope|fun\s+of|new|includes|set|type|option|struct|enume|param|rule|condition|data|ok|assert|def)\b
regex \= \b(scope|fun\s+of|new|includes|set|type|option|struct|enum|param|rule|condition|data|ok|assert|def)\b
styles [] = .keyword_rule ;
}

26
syntax_highlighting/nv/pygments/catala_nv.py
View File

@ -3,7 +3,8 @@ from pygments.token import *
import re
__all__=['CatalaNvLexer']
__all__ = ['CatalaNvLexer']
class CatalaNvLexer(RegexLexer):
name = 'CatalaNv'
@ -12,7 +13,7 @@ class CatalaNvLexer(RegexLexer):
flags = re.MULTILINE | re.UNICODE
tokens = {
'root' : [
'root': [
(u'(@@)', bygroups(Generic.Heading), 'main__1'),
(u'(@)', bygroups(Generic.Heading), 'main__2'),
(u'([^\\/\\n\\r])', bygroups(Text)),
@ -20,17 +21,22 @@ class CatalaNvLexer(RegexLexer):
('(\n|\r|\r\n)', Text),
('.', Text),
],
'code' : [
'code': [
(u'(\\s*\\#.*$)', bygroups(Comment.Single)),
(u'(param)(\\s+)([a-z\xe9\xe8\xe0\xe2\xf9\xee\xea\u0153\xe7][a-z\xe9\xe8\xe0\xe2\xf9\xee\xea\u0153\xe7A-Z\xc9\xc8\xc0\xc2\xd9\xce\xca\u0152\xc70-9_\\\']*)', bygroups(Keyword.Declaration, Text, Name.Variable)),
(u'(param)(\\s+)([a-z\xe9\xe8\xe0\xe2\xf9\xee\xea\u0153\xe7][a-z\xe9\xe8\xe0\xe2\xf9\xee\xea\u0153\xe7A-Z\xc9\xc8\xc0\xc2\xd9\xce\xca\u0152\xc70-9_\\\']*)',
bygroups(Keyword.Declaration, Text, Name.Variable)),
(u'\\b(match|with|fixed|by|decreasing|increasing|varies|with\\s+param|we\\s+have|in|such\\s+that|exists|for|all|of|if|then|else)\\b', bygroups(Keyword.Reserved)),
(u'\\b(scope|fun\\s+of|new|includes|set|type|option|struct|enume|param|rule|condition|data|ok|assert|def)\\b', bygroups(Keyword.Declaration)),
(u'\\b(scope|fun\\s+of|new|includes|set|type|option|struct|enum|param|rule|condition|data|ok|assert|def)\\b',
bygroups(Keyword.Declaration)),
(u'(\\|[0-9]+/[0-9]+/[0-9]+\\|)', bygroups(Number.Integer)),
(u'\\b(true|false)\\b', bygroups(Keyword.Constant)),
(u'\\b([0-9]+(,[0.9]*|))\\b', bygroups(Number.Integer)),
(u'(\\-\\-|\\;|\\.|\\,|\\:=|\\:|\\(|\\)|\\[|\\])', bygroups(Operator)),
(u'(\\-\\>|\\+|\\-|\\*|/|\\!|not|or|and|=|>|<|\\\\$|%|year|month|day)', bygroups(Operator)),
(u'\\b(int|bool|date|amount|text|decimal|number|sum|now)\\b', bygroups(Keyword.Type)),
(u'(\\-\\-|\\;|\\.|\\,|\\:=|\\:|\\(|\\)|\\[|\\])',
bygroups(Operator)),
(u'(\\-\\>|\\+|\\-|\\*|/|\\!|not|or|and|=|>|<|\\\\$|%|year|month|day)',
bygroups(Operator)),
(u'\\b(int|bool|date|amount|text|decimal|number|sum|now)\\b',
bygroups(Keyword.Type)),
(u'\\b([A-Z\xc9\xc8\xc0\xc2\xd9\xce\xca\u0152\xc7][a-z\xe9\xe8\xe0\xe2\xf9\xee\xea\u0153\xe7A-Z\xc9\xc8\xc0\xc2\xd9\xce\xca\u0152\xc70-9_\\\']*)(\\.)([a-z\xe9\xe8\xe0\xe2\xf9\xee\xea\u0153\xe7][a-z\xe9\xe8\xe0\xe2\xf9\xee\xea\u0153\xe7A-Z\xc9\xc8\xc0\xc2\xd9\xce\xca\u0152\xc70-9_\\\']*)\\b', bygroups(Name.Class, Operator, Name.Variable)),
(u'\\b([a-z\xe9\xe8\xe0\xe2\xf9\xee\xea\u0153\xe7][a-z\xe9\xe8\xe0\xe2\xf9\xee\xea\u0153\xe7A-Z\xc9\xc8\xc0\xc2\xd9\xce\xca\u0152\xc70-9_\\\']*)(\\.)([a-z\xe9\xe8\xe0\xe2\xf9\xee\xea\u0153\xe7][a-z\xe9\xe8\xe0\xe2\xf9\xee\xea\u0153\xe7A-Z\xc9\xc8\xc0\xc2\xd9\xce\xca\u0152\xc70-9_\\\'\\.]*)\\b', bygroups(Name.Variable, Operator, Text)),
(u'\\b([a-z\xe9\xe8\xe0\xe2\xf9\xee\xea\u0153\xe7][a-z\xe9\xe8\xe0\xe2\xf9\xee\xea\u0153\xe7A-Z\xc9\xc8\xc0\xc2\xd9\xce\xca\u0152\xc70-9_\\\']*)\\b', bygroups(Name.Variable)),
@ -38,12 +44,12 @@ class CatalaNvLexer(RegexLexer):
('(\n|\r|\r\n)', Text),
('.', Text),
],
'main__1' : [
'main__1': [
(u'(.)', bygroups(Generic.Heading)),
('(\n|\r|\r\n)', Text),
('.', Text),
],
'main__2' : [
'main__2': [
(u'(.)', bygroups(Generic.Heading)),
('(\n|\r|\r\n)', Text),
('.', Text),

2
syntax_highlighting/nv/vscode/syntaxes/catalavs.xml
View File

@ -161,7 +161,7 @@
</dict>
<dict>
<key>match</key>
<string>\b(scope|fun\s+of|new|includes|set|type|option|struct|enume|param|rule|condition|data|ok|assert|def)\b</string>
<string>\b(scope|fun\s+of|new|includes|set|type|option|struct|enum|param|rule|condition|data|ok|assert|def)\b</string>
<key>name</key>
<string>keyword.other.catala_nv</string>
</dict>

4
tests/Makefile
View File

@ -53,4 +53,8 @@ test_scope/sub_vars_in_sub_var.catala:
$(call interpret_with_scope_and_compare,nv,A)
test_struct/simple.catala:
$(call interpret_with_scope_and_compare,nv,A)
test_struct/nested.catala:
$(call interpret_with_scope_and_compare,nv,A)
test_struct/nested2.catala:
$(call interpret_with_scope_and_compare,nv,A)

12
tests/test_struct/nested.catala Normal file
View File

@ -0,0 +1,12 @@
@Article@
/*
new struct S:
data x type S
new scope A:
param y type S
scope A:
def y := S { -- x: 1 }
*/

6
tests/test_struct/nested.catala.A.out Normal file
View File

@ -0,0 +1,6 @@
[ERROR] The type S is defined using itself, which is forbidden since Catala does not provide recursive types
[ERROR]
[ERROR] --> test_struct/nested.catala
[ERROR] |
[ERROR] 5 | data x type S
[ERROR] | ^

11
tests/test_struct/nested2.catala Normal file
View File

@ -0,0 +1,11 @@
@Article@
/*
new struct S:
data x type E
data y type int
new enum E:
-- Case1 type bool
-- Case2 type S
*/

6
tests/test_struct/nested2.catala.A.out Normal file
View File

@ -0,0 +1,6 @@
[ERROR] Unknown type, not a struct or enum previously declared
[ERROR]
[ERROR] --> test_struct/nested2.catala
[ERROR] |
[ERROR] 5 | data x type E
[ERROR] | ^