mirror of
https://github.com/CatalaLang/catala.git
synced 2024-09-20 00:41:05 +03:00
259 lines
9.9 KiB
OCaml
259 lines
9.9 KiB
OCaml
(* This file is part of the Catala compiler, a specification language for tax and social benefits
|
|
computation rules. Copyright (C) 2020 Inria, contributor: Nicolas Chataing
|
|
<nicolas.chataing@ens.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. *)
|
|
|
|
(** Abstract syntax tree of the desugared representation *)
|
|
|
|
open Utils
|
|
|
|
(** {1 Names, Maps and Keys} *)
|
|
|
|
module IdentMap : Map.S with type key = String.t = Map.Make (String)
|
|
|
|
module RuleName : Uid.Id with type info = Uid.MarkedString.info = Uid.Make (Uid.MarkedString) ()
|
|
|
|
module RuleMap : Map.S with type key = RuleName.t = Map.Make (RuleName)
|
|
|
|
module RuleSet : Set.S with type elt = RuleName.t = Set.Make (RuleName)
|
|
|
|
module LabelName : Uid.Id with type info = Uid.MarkedString.info = Uid.Make (Uid.MarkedString) ()
|
|
|
|
module LabelMap : Map.S with type key = LabelName.t = Map.Make (LabelName)
|
|
|
|
module LabelSet : Set.S with type elt = LabelName.t = Set.Make (LabelName)
|
|
|
|
module StateName : Uid.Id with type info = Uid.MarkedString.info = Uid.Make (Uid.MarkedString) ()
|
|
|
|
module ScopeVar : Uid.Id with type info = Uid.MarkedString.info = Uid.Make (Uid.MarkedString) ()
|
|
|
|
module ScopeVarSet : Set.S with type elt = ScopeVar.t = Set.Make (ScopeVar)
|
|
|
|
module ScopeVarMap : Map.S with type key = ScopeVar.t = Map.Make (ScopeVar)
|
|
|
|
(** Inside a scope, a definition can refer either to a scope def, or a subscope def *)
|
|
module ScopeDef = struct
|
|
type t =
|
|
| Var of ScopeVar.t * StateName.t option
|
|
| SubScopeVar of Scopelang.Ast.SubScopeName.t * ScopeVar.t
|
|
(** In this case, the [ScopeVar.t] lives inside the context of the subscope's original
|
|
declaration *)
|
|
|
|
let compare x y =
|
|
match (x, y) with
|
|
| Var (x, None), Var (y, None)
|
|
| Var (x, Some _), Var (y, None)
|
|
| Var (x, None), Var (y, Some _)
|
|
| Var (x, _), SubScopeVar (_, y)
|
|
| SubScopeVar (_, x), Var (y, _) ->
|
|
ScopeVar.compare x y
|
|
| Var (x, Some sx), Var (y, Some sy) ->
|
|
let cmp = ScopeVar.compare x y in
|
|
if cmp = 0 then StateName.compare sx sy else cmp
|
|
| SubScopeVar (x', x), SubScopeVar (y', y) ->
|
|
let cmp = Scopelang.Ast.SubScopeName.compare x' y' in
|
|
if cmp = 0 then ScopeVar.compare x y else cmp
|
|
|
|
let get_position x =
|
|
match x with
|
|
| Var (x, None) -> Pos.get_position (ScopeVar.get_info x)
|
|
| Var (_, Some sx) -> Pos.get_position (StateName.get_info sx)
|
|
| SubScopeVar (x, _) -> Pos.get_position (Scopelang.Ast.SubScopeName.get_info x)
|
|
|
|
let format_t fmt x =
|
|
match x with
|
|
| Var (v, None) -> ScopeVar.format_t fmt v
|
|
| Var (v, Some sv) -> Format.fprintf fmt "%a.%a" ScopeVar.format_t v StateName.format_t sv
|
|
| SubScopeVar (s, v) ->
|
|
Format.fprintf fmt "%a.%a" Scopelang.Ast.SubScopeName.format_t s ScopeVar.format_t v
|
|
|
|
let hash x =
|
|
match x with
|
|
| Var (v, None) -> ScopeVar.hash v
|
|
| Var (v, Some sv) -> Int.logxor (ScopeVar.hash v) (StateName.hash sv)
|
|
| SubScopeVar (w, v) -> Int.logxor (Scopelang.Ast.SubScopeName.hash w) (ScopeVar.hash v)
|
|
end
|
|
|
|
module ScopeDefMap : Map.S with type key = ScopeDef.t = Map.Make (ScopeDef)
|
|
|
|
module ScopeDefSet : Set.S with type elt = ScopeDef.t = Set.Make (ScopeDef)
|
|
|
|
(** {1 AST} *)
|
|
|
|
type location =
|
|
| ScopeVar of ScopeVar.t Pos.marked * StateName.t option
|
|
| SubScopeVar of
|
|
Scopelang.Ast.ScopeName.t * Scopelang.Ast.SubScopeName.t Pos.marked * ScopeVar.t Pos.marked
|
|
|
|
module LocationSet : Set.S with type elt = location Pos.marked = Set.Make (struct
|
|
type t = location Pos.marked
|
|
|
|
let compare x y =
|
|
match (Pos.unmark x, Pos.unmark y) with
|
|
| ScopeVar (vx, None), ScopeVar (vy, None)
|
|
| ScopeVar (vx, Some _), ScopeVar (vy, None)
|
|
| ScopeVar (vx, None), ScopeVar (vy, Some _) ->
|
|
ScopeVar.compare (Pos.unmark vx) (Pos.unmark vy)
|
|
| ScopeVar ((x, _), Some sx), ScopeVar ((y, _), Some sy) ->
|
|
let cmp = ScopeVar.compare x y in
|
|
if cmp = 0 then StateName.compare sx sy else cmp
|
|
| SubScopeVar (_, (xsubindex, _), (xsubvar, _)), SubScopeVar (_, (ysubindex, _), (ysubvar, _))
|
|
->
|
|
let c = Scopelang.Ast.SubScopeName.compare xsubindex ysubindex in
|
|
if c = 0 then ScopeVar.compare xsubvar ysubvar else c
|
|
| ScopeVar _, SubScopeVar _ -> -1
|
|
| SubScopeVar _, ScopeVar _ -> 1
|
|
end)
|
|
|
|
(** The expressions use the {{:https://lepigre.fr/ocaml-bindlib/} Bindlib} library, based on
|
|
higher-order abstract syntax*)
|
|
type expr =
|
|
| ELocation of location
|
|
| EVar of expr Bindlib.var Pos.marked
|
|
| EStruct of Scopelang.Ast.StructName.t * expr Pos.marked Scopelang.Ast.StructFieldMap.t
|
|
| EStructAccess of expr Pos.marked * Scopelang.Ast.StructFieldName.t * Scopelang.Ast.StructName.t
|
|
| EEnumInj of expr Pos.marked * Scopelang.Ast.EnumConstructor.t * Scopelang.Ast.EnumName.t
|
|
| EMatch of
|
|
expr Pos.marked
|
|
* Scopelang.Ast.EnumName.t
|
|
* expr Pos.marked Scopelang.Ast.EnumConstructorMap.t
|
|
| ELit of Dcalc.Ast.lit
|
|
| EAbs of (expr, expr Pos.marked) Bindlib.mbinder Pos.marked * Scopelang.Ast.typ Pos.marked list
|
|
| EApp of expr Pos.marked * expr Pos.marked list
|
|
| EOp of Dcalc.Ast.operator
|
|
| EDefault of expr Pos.marked list * expr Pos.marked * expr Pos.marked
|
|
| EIfThenElse of expr Pos.marked * expr Pos.marked * expr Pos.marked
|
|
| EArray of expr Pos.marked list
|
|
| ErrorOnEmpty of expr Pos.marked
|
|
|
|
type rule = {
|
|
rule_id : RuleName.t;
|
|
rule_just : expr Pos.marked Bindlib.box;
|
|
rule_cons : expr Pos.marked Bindlib.box;
|
|
rule_parameter : (Scopelang.Ast.Var.t * Scopelang.Ast.typ Pos.marked) option;
|
|
rule_exception_to_rules : RuleSet.t Pos.marked;
|
|
}
|
|
|
|
let empty_rule (pos : Pos.t) (have_parameter : Scopelang.Ast.typ Pos.marked option) : rule =
|
|
{
|
|
rule_just = Bindlib.box (ELit (Dcalc.Ast.LBool false), pos);
|
|
rule_cons = Bindlib.box (ELit Dcalc.Ast.LEmptyError, pos);
|
|
rule_parameter =
|
|
(match have_parameter with
|
|
| Some typ -> Some (Scopelang.Ast.Var.make ("dummy", pos), typ)
|
|
| None -> None);
|
|
rule_exception_to_rules = (RuleSet.empty, pos);
|
|
rule_id = RuleName.fresh ("empty", pos);
|
|
}
|
|
|
|
let always_false_rule (pos : Pos.t) (have_parameter : Scopelang.Ast.typ Pos.marked option) : rule =
|
|
{
|
|
rule_just = Bindlib.box (ELit (Dcalc.Ast.LBool true), pos);
|
|
rule_cons = Bindlib.box (ELit (Dcalc.Ast.LBool false), pos);
|
|
rule_parameter =
|
|
(match have_parameter with
|
|
| Some typ -> Some (Scopelang.Ast.Var.make ("dummy", pos), typ)
|
|
| None -> None);
|
|
rule_exception_to_rules = (RuleSet.empty, pos);
|
|
rule_id = RuleName.fresh ("always_false", pos);
|
|
}
|
|
|
|
type assertion = Scopelang.Ast.expr Pos.marked Bindlib.box
|
|
|
|
type variation_typ = Increasing | Decreasing
|
|
|
|
type reference_typ = Decree | Law
|
|
|
|
type meta_assertion =
|
|
| FixedBy of reference_typ Pos.marked
|
|
| VariesWith of unit * variation_typ Pos.marked option
|
|
|
|
type scope_def = {
|
|
scope_def_rules : rule RuleMap.t;
|
|
scope_def_typ : Scopelang.Ast.typ Pos.marked;
|
|
scope_def_is_condition : bool;
|
|
scope_def_io : Scopelang.Ast.io;
|
|
scope_def_label_groups : RuleSet.t LabelMap.t;
|
|
}
|
|
|
|
type var_or_states = WholeVar | States of StateName.t list
|
|
|
|
type scope = {
|
|
scope_vars : var_or_states ScopeVarMap.t;
|
|
scope_sub_scopes : Scopelang.Ast.ScopeName.t Scopelang.Ast.SubScopeMap.t;
|
|
scope_uid : Scopelang.Ast.ScopeName.t;
|
|
scope_defs : scope_def ScopeDefMap.t;
|
|
scope_assertions : assertion list;
|
|
scope_meta_assertions : meta_assertion list;
|
|
}
|
|
|
|
type program = {
|
|
program_scopes : scope Scopelang.Ast.ScopeMap.t;
|
|
program_enums : Scopelang.Ast.enum_ctx;
|
|
program_structs : Scopelang.Ast.struct_ctx;
|
|
}
|
|
|
|
let rec locations_used (e : expr Pos.marked) : LocationSet.t =
|
|
match Pos.unmark e with
|
|
| ELocation l -> LocationSet.singleton (l, Pos.get_position e)
|
|
| EVar _ | ELit _ | EOp _ -> LocationSet.empty
|
|
| EAbs ((binder, _), _) ->
|
|
let _, body = Bindlib.unmbind binder in
|
|
locations_used body
|
|
| EStruct (_, es) ->
|
|
Scopelang.Ast.StructFieldMap.fold
|
|
(fun _ e' acc -> LocationSet.union acc (locations_used e'))
|
|
es LocationSet.empty
|
|
| EStructAccess (e1, _, _) -> locations_used e1
|
|
| EEnumInj (e1, _, _) -> locations_used e1
|
|
| EMatch (e1, _, es) ->
|
|
Scopelang.Ast.EnumConstructorMap.fold
|
|
(fun _ e' acc -> LocationSet.union acc (locations_used e'))
|
|
es (locations_used e1)
|
|
| EApp (e1, args) ->
|
|
List.fold_left
|
|
(fun acc arg -> LocationSet.union (locations_used arg) acc)
|
|
(locations_used e1) args
|
|
| EIfThenElse (e1, e2, e3) ->
|
|
LocationSet.union (locations_used e1)
|
|
(LocationSet.union (locations_used e2) (locations_used e3))
|
|
| EDefault (excepts, just, cons) ->
|
|
List.fold_left
|
|
(fun acc except -> LocationSet.union (locations_used except) acc)
|
|
(LocationSet.union (locations_used just) (locations_used cons))
|
|
excepts
|
|
| EArray es ->
|
|
List.fold_left (fun acc e' -> LocationSet.union acc (locations_used e')) LocationSet.empty es
|
|
| ErrorOnEmpty e' -> locations_used e'
|
|
|
|
let free_variables (def : rule RuleMap.t) : Pos.t ScopeDefMap.t =
|
|
let add_locs (acc : Pos.t ScopeDefMap.t) (locs : LocationSet.t) : Pos.t ScopeDefMap.t =
|
|
LocationSet.fold
|
|
(fun (loc, loc_pos) acc ->
|
|
ScopeDefMap.add
|
|
(match loc with
|
|
| ScopeVar (v, st) -> ScopeDef.Var (Pos.unmark v, st)
|
|
| SubScopeVar (_, sub_index, sub_var) ->
|
|
ScopeDef.SubScopeVar (Pos.unmark sub_index, Pos.unmark sub_var))
|
|
loc_pos acc)
|
|
locs acc
|
|
in
|
|
RuleMap.fold
|
|
(fun _ rule acc ->
|
|
let locs =
|
|
LocationSet.union
|
|
(locations_used (Bindlib.unbox rule.rule_just))
|
|
(locations_used (Bindlib.unbox rule.rule_cons))
|
|
in
|
|
add_locs acc locs)
|
|
def ScopeDefMap.empty
|