123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350(* This file is part of the Catala compiler, a specification language for tax
and social benefits computation rules. Copyright (C) 2020 Inria, contributor:
Denis Merigoux <denis.merigoux@inria.fr>
Licensed under the Apache License, Version 2.0 (the "License"); you may not
use this file except in compliance with the License. You may obtain a copy of
the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
License for the specific language governing permissions and limitations under
the License. *)(** Graph representation of the dependencies between scopes in the Catala
program. Vertices are functions, x -> y if x is used in the definition of y. *)openCatala_utilsopenShared_asttypevertex=ScopeofScopeName.t|TopdefofTopdefName.tmoduleSVertex=structtypet=vertex(* While we enforce that globals don't depend on scopes, and could therefore
compute two separate dependency graphs and traverse them one after the
other, code-wise it's simpler to have a single graph including both *)letcomparev1v2=matchv1,v2with|Scopes1,Scopes2->ScopeName.compares1s2|Topdefg1,Topdefg2->TopdefName.compareg1g2|Scope_,_->-1|_,Scope_->1|Topdef_,_|_,Topdef_->.letequalv1v2=matchv1,v2with|Scopes1,Scopes2->ScopeName.equals1s2|Topdefg1,Topdefg2->TopdefName.equalg1g2|(Scope_|Topdef_),_->falselethash=function|Scopes->ScopeName.hashs|Topdefg->TopdefName.hashgletformatppf=function|Scopes->ScopeName.formatppfs|Topdefg->TopdefName.formatppfg(* let to_string v = Format.asprintf "%a" format v
let info = function | Scope s -> ScopeName.get_info s | Topdef g ->
TopdefName.get_info g *)endmoduleVMap=Map.Make(SVertex)(** On the edges, the label is the expression responsible for the use of the
function *)moduleSEdge=structtypet=Pos.tletcompare=compareletdefault=Pos.no_posendmoduleSDependencies=Graph.Persistent.Digraph.ConcreteBidirectionalLabeled(SVertex)(SEdge)moduleSTopologicalTraversal=Graph.Topological.Make(SDependencies)moduleSSCC=Graph.Components.Make(SDependencies)(** Tarjan's stongly connected components algorithm, provided by OCamlGraph *)letrecexpr_used_defse=letrecurse_subtermse=Expr.shallow_fold(fune->VMap.union(fun_x_->Somex)(expr_used_defse))eVMap.emptyinmatchewith|ELocation(ToplevelVar{name=v,pos}),_->ifTopdefName.pathv<>[]thenVMap.emptyelseVMap.singleton(Topdefv)pos|(EScopeCall{scope;_},m)ase->ifScopeName.pathscope<>[]thenrecurse_subtermseelseVMap.add(Scopescope)(Expr.mark_posm)(recurse_subtermse)|EAbs{binder;_},_->let_,body=Bindlib.unmbindbinderinexpr_used_defsbody|e->recurse_subtermseletrule_used_defs=function|Ast.Assertione|Ast.ScopeVarDefinition{e;_}|Ast.SubScopeVarDefinition{e;_}->(* TODO: maybe this info could be passed on from previous passes without
walking through all exprs again *)expr_used_defseletbuild_program_dep_graph(prgm:'mAst.program):SDependencies.t=letg=SDependencies.emptyinletg=TopdefName.Map.fold(funv_g->SDependencies.add_vertexg(Topdefv))prgm.program_topdefsginletg=ScopeName.Map.fold(funv_g->SDependencies.add_vertexg(Scopev))prgm.program_scopesginletg=TopdefName.Map.fold(funglo_name(expr,_)g->letused_defs=expr_used_defsexprinifVMap.mem(Topdefglo_name)used_defsthenMessage.error~pos:(Mark.get(TopdefName.get_infoglo_name))"The toplevel declaration@ %a@ has@ a@ definition@ that@ refers@ \
to@ itself,@ which@ is@ not@ supported@ (Catala does not provide \
recursion)"TopdefName.formatglo_name;VMap.fold(fundefposg->letedge=SDependencies.E.createdefpos(Topdefglo_name)inSDependencies.add_edge_egedge)used_defsg)prgm.program_topdefsginScopeName.Map.fold(funscope_name(scope,_)g->List.fold_left(fungrule->letused_defs=rule_used_defsruleinifVMap.mem(Scopescope_name)used_defsthenMessage.error~pos:(Mark.get(ScopeName.get_infoscope.Ast.scope_decl_name))"The scope@ %a@ is@ calling@ into@ itself@ as@ a@ subscope,@ \
which@ is@ not@ supported@ (Catala does not provide recursion)"ScopeName.formatscope.Ast.scope_decl_name;VMap.fold(funused_defposg->letedge=SDependencies.E.createused_defpos(Scopescope_name)inSDependencies.add_edge_egedge)used_defsg)gscope.Ast.scope_decl_rules)prgm.program_scopesgletcheck_for_cycle_in_defs(g:SDependencies.t):unit=(* if there is a cycle, there will be an strongly connected component of
cardinality > 1 *)letsccs=SSCC.scc_listginmatchList.find_opt(function[]|[_]->false|_->true)sccswith|None->()|Some[]->assertfalse|Some(v0::_asscc)->letmoduleVSet=Set.Make(SVertex)inletscc=VSet.of_listsccinletrecget_cyclecyclecycle_setv=letcycle=v::cycleinletcycle_set=VSet.addvcycle_setinletsucc=SDependencies.succgvinifList.exists(funv->VSet.memvcycle_set)succthen(* a cycle may be smaller than the scc, in that case we just return the
first one found *)letreccut_afteracc=function|[]->acc|v::vs->ifList.memvsuccthenv::accelsecut_after(v::acc)vsincut_after[]cycleelseget_cyclecyclecycle_set(List.find(funsucc->VSet.memsuccscc)succ)inletcycle=get_cycle[]VSet.emptyv0inletspans=List.map2(funv1v2->letmsg=Format.asprintf"%a is used here in the definition of %a:"SVertex.formatv1SVertex.formatv2inlet_,edge_pos,_=SDependencies.find_edgegv1v2inmsg,edge_pos)cycle(List.tlcycle@[List.hdcycle])inMessage.error~extra_pos:spans"Cyclic dependency detected between the following scopes:@ @[<hv>%a@]"(Format.pp_print_list~pp_sep:(funppf()->Format.fprintfppf" →@ ")SVertex.format)(cycle@[List.hdcycle])letget_defs_ordering(g:SDependencies.t):SVertex.tlist=List.rev(STopologicalTraversal.fold(funsdacc->sd::acc)g[])moduleTVertex=structtypet=StructofStructName.t|EnumofEnumName.tlethashx=matchxwithStructx->StructName.hashx|Enumx->EnumName.hashxletcomparexy=matchx,ywith|Structx,Structy->StructName.comparexy|Enumx,Enumy->EnumName.comparexy|Struct_,Enum_->1|Enum_,Struct_->-1letequalxy=matchx,ywith|Structx,Structy->StructName.comparexy=0|Enumx,Enumy->EnumName.comparexy=0|_->falseletformat(fmt:Format.formatter)(x:t):unit=matchxwith|Structx->StructName.formatfmtx|Enumx->EnumName.formatfmtxletget_info(x:t)=matchxwith|Structx->StructName.get_infox|Enumx->EnumName.get_infoxendmoduleTVertexSet=Set.Make(TVertex)(** On the edges, the label is the expression responsible for the use of the
function *)moduleTEdge=structtypet=Pos.tletcompare=compareletdefault=Pos.no_posendmoduleTDependencies=Graph.Persistent.Digraph.ConcreteBidirectionalLabeled(TVertex)(TEdge)moduleTTopologicalTraversal=Graph.Topological.Make(TDependencies)moduleTSCC=Graph.Components.Make(TDependencies)(** Tarjan's stongly connected components algorithm, provided by OCamlGraph *)letrecget_structs_or_enums_in_type(t:typ):TVertexSet.t=matchMark.removetwith|TStructs->TVertexSet.singleton(TVertex.Structs)|TEnume->TVertexSet.singleton(TVertex.Enume)|TArrow(t1,t2)->TVertexSet.union(t1|>List.mapget_structs_or_enums_in_type|>List.fold_leftTVertexSet.unionTVertexSet.empty)(get_structs_or_enums_in_typet2)|TClosureEnv|TLit_|TAny->TVertexSet.empty|TOptiont1|TArrayt1|TDefaultt1->get_structs_or_enums_in_typet1|TTuplets->List.fold_left(funacct->TVertexSet.unionacc(get_structs_or_enums_in_typet))TVertexSet.emptytsletbuild_type_graph(structs:struct_ctx)(enums:enum_ctx):TDependencies.t=letg=TDependencies.emptyinletg=StructName.Map.fold(funsfieldsg->StructField.Map.fold(fun_typg->letdef=TVertex.Structsinletg=TDependencies.add_vertexgdefinletused=get_structs_or_enums_in_typetypinTVertexSet.fold(funusedg->ifTVertex.equaluseddefthenMessage.error~pos:(Mark.gettyp)"The type@ %a@ is@ defined@ using@ itself,@ which@ is@ \
not@ supported@ (Catala does not allow recursive types)"TVertex.formatusedelseletedge=TDependencies.E.createused(Mark.gettyp)definTDependencies.add_edge_egedge)usedg)fieldsg)structsginletg=EnumName.Map.fold(funecasesg->EnumConstructor.Map.fold(fun_typg->letdef=TVertex.Enumeinletg=TDependencies.add_vertexgdefinletused=get_structs_or_enums_in_typetypinTVertexSet.fold(funusedg->ifTVertex.equaluseddefthenMessage.error~pos:(Mark.gettyp)"The type@ %a@ is@ defined@ using@ itself,@ which@ is@ \
not@ supported@ (Catala does not allow recursive types)"TVertex.formatusedelseletedge=TDependencies.E.createused(Mark.gettyp)definTDependencies.add_edge_egedge)usedg)casesg)enumsgingletcheck_type_cycles(structs:struct_ctx)(enums:enum_ctx):TVertex.tlist=letg=build_type_graphstructsenumsin(* if there is a cycle, there will be an strongly connected component of
cardinality > 1 *)letsccs=TSCC.scc_listgin(ifList.lengthsccs<TDependencies.nb_vertexgthenletscc=List.find(funscc->List.lengthscc>1)sccsinletspans=List.flatten(List.map(funv->letvar_str,var_info=Format.asprintf"%a"TVertex.formatv,TVertex.get_infovinletsuccs=TDependencies.succ_egvinlet_,edge_pos,succ=List.find(fun(_,_,succ)->List.memsuccscc)succsinletsucc_str=Format.asprintf"%a"TVertex.formatsuccin["Cycle type "^var_str^", declared:",Mark.getvar_info;("Used here in the definition of another cycle type "^succ_str^":",edge_pos);])scc)inMessage.error~extra_pos:spans"Cyclic dependency detected between types!");List.rev(TTopologicalTraversal.fold(funvacc->v::acc)g[])