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

Added tuples to default calculus

Browse Source
This commit is contained in:
Denis Merigoux 2020-11-23 16:12:45 +01:00
parent e5078b1c98
commit 35dcd57b2b
8 changed files with 217 additions and 79 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/catala/default_calculus/ast.ml
View File

@ -14,12 +14,18 @@
module Pos = Utils.Pos
type typ = TBool | TUnit | TArrow of typ Pos.marked * typ Pos.marked
type typ =
| TBool
| TUnit
| TTuple of typ Pos.marked list
| TArrow of typ Pos.marked * typ Pos.marked
type lit = LTrue | LFalse | LEmptyError
type expr =
| EVar of expr Pos.marked Bindlib.var
| ETuple of expr Pos.marked list
| ETupleAccess of expr Pos.marked * int
| ELit of lit
| EAbs of Pos.t * (expr Pos.marked, expr Pos.marked) Bindlib.binder * typ
| EApp of expr Pos.marked * expr Pos.marked

117
src/catala/default_calculus/interpreter.ml
View File

@ -16,58 +16,73 @@ module Pos = Utils.Pos
module Errors = Utils.Errors
module A = Ast
let is_value (e : A.expr Pos.marked) : bool =
match Pos.unmark e with A.EAbs _ | ELit _ -> true | _ -> false
let is_empty_error (e : A.expr Pos.marked) : bool =
match Pos.unmark e with ELit LEmptyError -> true | _ -> false
let rec evaluate_expr (e : A.expr Pos.marked) : A.expr Pos.marked =
if is_value e then e
else
match Pos.unmark e with
| EVar _ ->
Errors.raise_spanned_error
"Free variable found at evaluation (should not happen if term was well-typed"
(Pos.get_position e)
| EApp (e1, e2) -> (
let e1 = evaluate_expr e1 in
let e2 = evaluate_expr e2 in
match Pos.unmark e1 with
| EAbs (_, binder, _) -> evaluate_expr (Bindlib.subst binder e2)
| ELit LEmptyError -> Pos.same_pos_as (A.ELit LEmptyError) e
| _ ->
Errors.raise_spanned_error
"Function has not been reduced to a lambda at evaluation (should not happen if the \
term was well-typed"
(Pos.get_position e) )
| EAbs _ | ELit _ -> assert false (* should not happen because the remaining cases are values *)
| EDefault (just, cons, subs) -> (
let just = evaluate_expr just in
match Pos.unmark just with
| ELit LEmptyError -> Pos.same_pos_as (A.ELit LEmptyError) e
| ELit LTrue -> evaluate_expr cons
| ELit LFalse -> (
let subs = List.map evaluate_expr subs in
let empty_count = List.length (List.filter is_empty_error subs) in
match List.length subs - empty_count with
| 0 -> Pos.same_pos_as (A.ELit LEmptyError) e
| 1 -> List.find (fun sub -> not (is_empty_error sub)) subs
| _ ->
Errors.raise_multispanned_error
"There is a conflict between multiple rules for assigning a single value."
( [
( Some "This rule is not triggered, so we consider rules of lower priority:",
Pos.get_position e );
]
@ List.map
(fun sub ->
( Some
"This value is available because the justification of its rule is true:",
Pos.get_position sub ))
(List.filter (fun sub -> not (is_empty_error sub)) subs) ) )
| _ ->
Errors.raise_spanned_error
"Default justification has not been reduced to a boolean at evaluation (should not \
happen if the term was well-typed"
(Pos.get_position e) )
match Pos.unmark e with
| EVar _ ->
Errors.raise_spanned_error
"free variable found at evaluation (should not happen if term was well-typed"
(Pos.get_position e)
| EApp (e1, e2) -> (
let e1 = evaluate_expr e1 in
let e2 = evaluate_expr e2 in
match Pos.unmark e1 with
| EAbs (_, binder, _) -> evaluate_expr (Bindlib.subst binder e2)
| ELit LEmptyError -> Pos.same_pos_as (A.ELit LEmptyError) e
| _ ->
Errors.raise_spanned_error
"function has not been reduced to a lambda at evaluation (should not happen if the \
term was well-typed"
(Pos.get_position e) )
| EAbs _ | ELit _ -> e (* thse are values *)
| ETuple es -> Pos.same_pos_as (A.ETuple (List.map evaluate_expr es)) e
| ETupleAccess (e1, n) -> (
let e1 = evaluate_expr e1 in
match Pos.unmark e1 with
| ETuple es -> (
match List.nth_opt es n with
| Some e' -> e'
| None ->
Errors.raise_spanned_error
(Format.asprintf
"the tuple has %d components but the %i-th element was requested (should not \
happen if the term was well-type)"
(List.length es) n)
(Pos.get_position e1) )
| _ ->
Errors.raise_spanned_error
(Format.asprintf
"the expression should be a tuple with %d components but is not (should not happen \
if the term was well-typed)"
n)
(Pos.get_position e1) )
| EDefault (just, cons, subs) -> (
let just = evaluate_expr just in
match Pos.unmark just with
| ELit LEmptyError -> Pos.same_pos_as (A.ELit LEmptyError) e
| ELit LTrue -> evaluate_expr cons
| ELit LFalse -> (
let subs = List.map evaluate_expr subs in
let empty_count = List.length (List.filter is_empty_error subs) in
match List.length subs - empty_count with
| 0 -> Pos.same_pos_as (A.ELit LEmptyError) e
| 1 -> List.find (fun sub -> not (is_empty_error sub)) subs
| _ ->
Errors.raise_multispanned_error
"there is a conflict between multiple rules for assigning a single value."
( [
( Some "This rule is not triggered, so we consider rules of lower priority:",
Pos.get_position e );
]
@ List.map
(fun sub ->
( Some "This value is available because the justification of its rule is true:",
Pos.get_position sub ))
(List.filter (fun sub -> not (is_empty_error sub)) subs) ) )
| _ ->
Errors.raise_spanned_error
"Default justification has not been reduced to a boolean at evaluation (should not \
happen if the term was well-typed"
(Pos.get_position e) )

51
src/catala/default_calculus/typing.ml
View File

@ -23,6 +23,7 @@ type typ =
| TUnit
| TBool
| TArrow of typ Pos.marked UnionFind.elem * typ Pos.marked UnionFind.elem
| TTuple of typ Pos.marked UnionFind.elem list
| TAny
let rec format_typ (fmt : Format.formatter) (ty : typ Pos.marked UnionFind.elem) : unit =
@ -31,6 +32,10 @@ let rec format_typ (fmt : Format.formatter) (ty : typ Pos.marked UnionFind.elem)
| TUnit -> Format.fprintf fmt "unit"
| TBool -> Format.fprintf fmt "bool"
| TAny -> Format.fprintf fmt "any"
| TTuple ts ->
Format.fprintf fmt "(%a)"
(Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt ", ") format_typ)
ts
| TArrow (t1, t2) -> Format.fprintf fmt "%a -> %a" format_typ t1 format_typ t2
let rec unify (t1 : typ Pos.marked UnionFind.elem) (t2 : typ Pos.marked UnionFind.elem) : unit =
@ -41,6 +46,7 @@ let rec unify (t1 : typ Pos.marked UnionFind.elem) (t2 : typ Pos.marked UnionFin
| (TArrow (t11, t12), _), (TArrow (t21, t22), _) ->
unify t11 t21;
unify t12 t22
| (TTuple ts1, _), (TTuple ts2, _) -> List.iter2 unify ts1 ts2
| (TAny, _), (TAny, _) -> ignore (UnionFind.union t1 t2)
| (TAny, _), t_repr | t_repr, (TAny, _) ->
let t_union = UnionFind.union t1 t2 in
@ -62,6 +68,7 @@ let rec ast_to_typ (ty : A.typ) : typ =
TArrow
( UnionFind.make (Pos.map_under_mark ast_to_typ t1),
UnionFind.make (Pos.map_under_mark ast_to_typ t2) )
| A.TTuple ts -> TTuple (List.map (fun t -> UnionFind.make (Pos.map_under_mark ast_to_typ t)) ts)
let rec typ_to_ast (ty : typ Pos.marked UnionFind.elem) : A.typ Pos.marked =
Pos.map_under_mark
@ -69,6 +76,7 @@ let rec typ_to_ast (ty : typ Pos.marked UnionFind.elem) : A.typ Pos.marked =
match ty with
| TUnit -> A.TUnit
| TBool -> A.TBool
| TTuple ts -> A.TTuple (List.map typ_to_ast ts)
| TArrow (t1, t2) -> A.TArrow (typ_to_ast t1, typ_to_ast t2)
| TAny -> A.TUnit)
(UnionFind.get (UnionFind.find ty))
@ -86,6 +94,25 @@ let rec typecheck_expr_bottom_up (env : env) (e : A.expr Pos.marked) : typ Pos.m
(Pos.get_position e) )
| ELit (LTrue | LFalse) -> UnionFind.make (Pos.same_pos_as TBool e)
| ELit LEmptyError -> UnionFind.make (Pos.same_pos_as TAny e)
| ETuple es ->
let ts = List.map (typecheck_expr_bottom_up env) es in
UnionFind.make (Pos.same_pos_as (TTuple ts) e)
| ETupleAccess (e1, n) -> (
let t1 = typecheck_expr_bottom_up env e1 in
match Pos.unmark (UnionFind.get (UnionFind.find t1)) with
| TTuple ts -> (
match List.nth_opt ts n with
| Some t' -> t'
| None ->
Errors.raise_spanned_error
(Format.asprintf
"expression should have a tuple type with at least %d elements but only has %d" n
(List.length ts))
(Pos.get_position e1) )
| _ ->
Errors.raise_spanned_error
(Format.asprintf "exprected a tuple, got a %a" format_typ t1)
(Pos.get_position e1) )
| EAbs (pos_binder, binder, tau) ->
let x, body = Bindlib.unbind binder in
let env = A.VarMap.add x (ast_to_typ tau, pos_binder) env in
@ -113,6 +140,30 @@ and typecheck_expr_top_down (env : env) (e : A.expr Pos.marked)
(Pos.get_position e) )
| ELit (LTrue | LFalse) -> unify tau (UnionFind.make (Pos.same_pos_as TBool e))
| ELit LEmptyError -> unify tau (UnionFind.make (Pos.same_pos_as TAny e))
| ETuple es -> (
let tau' = UnionFind.get (UnionFind.find tau) in
match Pos.unmark tau' with
| TTuple ts -> List.iter2 (typecheck_expr_top_down env) es ts
| _ ->
Errors.raise_spanned_error
(Format.asprintf "exprected %a, got a tuple" format_typ tau)
(Pos.get_position e) )
| ETupleAccess (e1, n) -> (
let t1 = typecheck_expr_bottom_up env e1 in
match Pos.unmark (UnionFind.get (UnionFind.find t1)) with
| TTuple t1s -> (
match List.nth_opt t1s n with
| Some t1n -> unify t1n tau
| None ->
Errors.raise_spanned_error
(Format.asprintf
"expression should have a tuple type with at least %d elements but only has %d" n
(List.length t1s))
(Pos.get_position e1) )
| _ ->
Errors.raise_spanned_error
(Format.asprintf "exprected a tuple , got %a" format_typ tau)
(Pos.get_position e) )
| EAbs (pos_binder, binder, t_arg) ->
let x, body = Bindlib.unbind binder in
let env = A.VarMap.add x (ast_to_typ t_arg, pos_binder) env in

21
src/catala/desugared/ast.ml
View File

@ -15,9 +15,6 @@
module Pos = Utils.Pos
module Uid = Utils.Uid
module IdentMap = Map.Make (String)
module Var = Uid.Make (Uid.MarkedString)
module VarSet = Set.Make (Var)
module VarMap = Map.Make (Var)
module LocalVar = Uid.Make (Uid.MarkedString)
module LocalVarSet = Set.Make (LocalVar)
module LocalVarMap = Map.Make (LocalVar)
@ -25,23 +22,29 @@ module LocalVarMap = Map.Make (LocalVar)
(** Inside a scope, a definition can refer either to a scope def, or a subscope def *)
module ScopeDef = struct
type t =
| Var of Var.t
| SubScopeVar of Scopelang.Ast.SubScopeName.t * Var.t
| Var of Scopelang.Ast.ScopeVar.t
| SubScopeVar of Scopelang.Ast.SubScopeName.t * Scopelang.Ast.ScopeVar.t
(** In this case, the [Uid.Var.t] lives inside the context of the subscope's original
declaration *)
let compare x y =
match (x, y) with
| Var x, Var y | Var x, SubScopeVar (_, y) | SubScopeVar (_, x), Var y -> Var.compare x y
| Var x, Var y | Var x, SubScopeVar (_, y) | SubScopeVar (_, x), Var y ->
Scopelang.Ast.ScopeVar.compare x y
| SubScopeVar (_, x), SubScopeVar (_, y) -> Scopelang.Ast.SubScopeName.compare x y
let format_t x =
match x with
| Var v -> Var.format_t v
| Var v -> Scopelang.Ast.ScopeVar.format_t v
| SubScopeVar (s, v) ->
Printf.sprintf "%s.%s" (Scopelang.Ast.SubScopeName.format_t s) (Var.format_t v)
Printf.sprintf "%s.%s"
(Scopelang.Ast.SubScopeName.format_t s)
(Scopelang.Ast.ScopeVar.format_t v)
let hash x = match x with Var v -> Var.hash v | SubScopeVar (_, v) -> Var.hash v
let hash x =
match x with
| Var v -> Scopelang.Ast.ScopeVar.hash v
| SubScopeVar (_, v) -> Scopelang.Ast.ScopeVar.hash v
end
module ScopeDefMap = Map.Make (ScopeDef)

19
src/catala/desugared/interpreter.ml
View File

@ -25,21 +25,25 @@ module Errors = Utils.Errors
In the graph, x -> y if x is used in the definition of y. *)
module Vertex = struct
type t = Var of Ast.Var.t | SubScope of Scopelang.Ast.SubScopeName.t
type t = Var of Scopelang.Ast.ScopeVar.t | SubScope of Scopelang.Ast.SubScopeName.t
let hash x =
match x with Var x -> Ast.Var.hash x | SubScope x -> Scopelang.Ast.SubScopeName.hash x
match x with
| Var x -> Scopelang.Ast.ScopeVar.hash x
| SubScope x -> Scopelang.Ast.SubScopeName.hash x
let compare = compare
let equal x y =
match (x, y) with
| Var x, Var y -> Ast.Var.compare x y = 0
| Var x, Var y -> Scopelang.Ast.ScopeVar.compare x y = 0
| SubScope x, SubScope y -> Scopelang.Ast.SubScopeName.compare x y = 0
| _ -> false
let format_t (x : t) : string =
match x with Var v -> Ast.Var.format_t v | SubScope v -> Scopelang.Ast.SubScopeName.format_t v
match x with
| Var v -> Scopelang.Ast.ScopeVar.format_t v
| SubScope v -> Scopelang.Ast.SubScopeName.format_t v
end
(** On the edges, the label is the expression responsible for the use of the variable *)
@ -69,7 +73,8 @@ let check_for_cycle (g : ScopeDependencies.t) : unit =
(fun v ->
let var_str, var_info =
match v with
| Vertex.Var v -> (Ast.Var.format_t v, Ast.Var.get_info v)
| Vertex.Var v ->
(Scopelang.Ast.ScopeVar.format_t v, Scopelang.Ast.ScopeVar.get_info v)
| Vertex.SubScope v ->
(Scopelang.Ast.SubScopeName.format_t v, Scopelang.Ast.SubScopeName.get_info v)
in
@ -77,7 +82,7 @@ let check_for_cycle (g : ScopeDependencies.t) : unit =
let _, edge_pos, succ = List.find (fun (_, _, succ) -> List.mem succ scc) succs in
let succ_str =
match succ with
| Vertex.Var v -> Ast.Var.format_t v
| Vertex.Var v -> Scopelang.Ast.ScopeVar.format_t v
| Vertex.SubScope v -> Scopelang.Ast.SubScopeName.format_t v
in
[
@ -95,7 +100,7 @@ let build_scope_dependencies (scope : Ast.scope) (ctxt : Name_resolution.context
let scope_ctxt = Scopelang.Ast.ScopeMap.find scope_uid ctxt.scopes in
let g =
Ast.IdentMap.fold
(fun _ (v : Ast.Var.t) g -> ScopeDependencies.add_vertex g (Vertex.Var v))
(fun _ (v : Scopelang.Ast.ScopeVar.t) g -> ScopeDependencies.add_vertex g (Vertex.Var v))
scope_ctxt.var_idmap g
in
let g =

29
src/catala/desugared/name_resolution.ml
View File

@ -27,7 +27,7 @@ type def_context = { var_idmap : Ast.LocalVar.t Ast.IdentMap.t }
matching *)
type scope_context = {
var_idmap : Ast.Var.t Ast.IdentMap.t;
var_idmap : Scopelang.Ast.ScopeVar.t Ast.IdentMap.t;
sub_scopes_idmap : Scopelang.Ast.SubScopeName.t Ast.IdentMap.t;
sub_scopes : Scopelang.Ast.ScopeName.t Scopelang.Ast.SubScopeMap.t;
definitions : def_context Ast.ScopeDefMap.t;
@ -38,7 +38,7 @@ type scope_context = {
type context = {
scope_idmap : Scopelang.Ast.ScopeName.t Ast.IdentMap.t;
scopes : scope_context Scopelang.Ast.ScopeMap.t;
var_typs : typ Ast.VarMap.t;
var_typs : typ Scopelang.Ast.ScopeVarMap.t;
}
let raise_unsupported_feature (msg : string) (pos : Pos.t) =
@ -50,7 +50,8 @@ let raise_unknown_identifier (msg : string) (ident : ident Pos.marked) =
(Pos.get_position ident)
(** Get the type associated to an uid *)
let get_var_typ (ctxt : context) (uid : Ast.Var.t) : typ = Ast.VarMap.find uid ctxt.var_typs
let get_var_typ (ctxt : context) (uid : Scopelang.Ast.ScopeVar.t) : typ =
Scopelang.Ast.ScopeVarMap.find uid ctxt.var_typs
(** Process a subscope declaration *)
let process_subscope_decl (scope : Scopelang.Ast.ScopeName.t) (ctxt : context)
@ -112,16 +113,19 @@ let process_data_decl (scope : Scopelang.Ast.ScopeName.t) (ctxt : context)
match Ast.IdentMap.find_opt name scope_ctxt.var_idmap with
| Some use ->
Errors.raise_multispanned_error "var name already used"
[ (Some "first use", Pos.get_position (Ast.Var.get_info use)); (Some "second use", pos) ]
[
(Some "first use", Pos.get_position (Scopelang.Ast.ScopeVar.get_info use));
(Some "second use", pos);
]
| None ->
let uid = Ast.Var.fresh (name, pos) in
let uid = Scopelang.Ast.ScopeVar.fresh (name, pos) in
let scope_ctxt =
{ scope_ctxt with var_idmap = Ast.IdentMap.add name uid scope_ctxt.var_idmap }
in
{
ctxt with
scopes = Scopelang.Ast.ScopeMap.add scope scope_ctxt ctxt.scopes;
var_typs = assert false (* Ast.VarMap.add uid data_typ ctxt.var_typs *);
var_typs = assert false (* Scopelang.Ast.ScopeVarMap.add uid data_typ ctxt.var_typs *);
}
(** Process an item declaration *)
@ -275,7 +279,7 @@ let form_context (prgm : Surface.Ast.program) : context =
{
scope_idmap = Ast.IdentMap.empty;
scopes = Scopelang.Ast.ScopeMap.empty;
var_typs = Ast.VarMap.empty;
var_typs = Scopelang.Ast.ScopeVarMap.empty;
}
in
let ctxt =
@ -289,7 +293,7 @@ let form_context (prgm : Surface.Ast.program) : context =
(** Get the variable uid inside the scope given in argument *)
let get_var_uid (scope_uid : Scopelang.Ast.ScopeName.t) (ctxt : context)
((x, pos) : ident Pos.marked) : Ast.Var.t =
((x, pos) : ident Pos.marked) : Scopelang.Ast.ScopeVar.t =
let scope = Scopelang.Ast.ScopeMap.find scope_uid ctxt.scopes in
match Ast.IdentMap.find_opt x scope.var_idmap with
| None -> raise_unknown_identifier "for a var of this scope" (x, pos)
@ -304,9 +308,12 @@ let get_subscope_uid (scope_uid : Scopelang.Ast.ScopeName.t) (ctxt : context)
| Some sub_uid -> sub_uid
(** Checks if the var_uid belongs to the scope scope_uid *)
let belongs_to (ctxt : context) (uid : Ast.Var.t) (scope_uid : Scopelang.Ast.ScopeName.t) : bool =
let belongs_to (ctxt : context) (uid : Scopelang.Ast.ScopeVar.t)
(scope_uid : Scopelang.Ast.ScopeName.t) : bool =
let scope = Scopelang.Ast.ScopeMap.find scope_uid ctxt.scopes in
Ast.IdentMap.exists (fun _ var_uid -> Ast.Var.compare uid var_uid = 0) scope.var_idmap
Ast.IdentMap.exists
(fun _ var_uid -> Scopelang.Ast.ScopeVar.compare uid var_uid = 0)
scope.var_idmap
let get_def_typ (ctxt : context) (def : Ast.ScopeDef.t) : typ =
match def with
@ -314,4 +321,4 @@ let get_def_typ (ctxt : context) (def : Ast.ScopeDef.t) : typ =
(* we don't need to look at the subscope prefix because [x] is already the uid referring back to
the original subscope *)
| Ast.ScopeDef.Var x ->
Ast.VarMap.find x ctxt.var_typs
Scopelang.Ast.ScopeVarMap.find x ctxt.var_typs

19
src/catala/scope_language/ast.ml
View File

@ -20,3 +20,22 @@ module ScopeMap = Map.Make (ScopeName)
module SubScopeName = Uid.Make (Uid.MarkedString)
module SubScopeNameSet = Set.Make (SubScopeName)
module SubScopeMap = Map.Make (SubScopeName)
module ScopeVar = Uid.Make (Uid.MarkedString)
module ScopeVarSet = Set.Make (ScopeVar)
module ScopeVarMap = Map.Make (ScopeVar)
type location = ScopeVar of ScopeVar.t | SubScopeVar of ScopeName.t * SubScopeName.t * ScopeVar.t
type expr =
| ELocation of location
| EVar of expr Pos.marked Bindlib.var
| ELit of Dcalc.Ast.lit
| EAbs of Pos.t * (expr Pos.marked, expr Pos.marked) Bindlib.binder * Dcalc.Ast.typ
| EApp of expr Pos.marked * expr Pos.marked
| EDefault of expr Pos.marked * expr Pos.marked * expr Pos.marked list
type rule = Definition of location * Dcalc.Ast.typ * expr | Call of ScopeName.t * SubScopeName.t
type scope_decl = { scope_decl_name : ScopeName.t; scope_decl_rules : rule list }
type program = scope_decl ScopeMap.t

32
src/catala/scope_language/scope_to_dcalc.ml Normal file
View File

@ -0,0 +1,32 @@
(* 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. *)
module Pos = Utils.Pos
type ctx = Ast.location list
type scope_ctx = Dcalc.Ast.Var.t Ast.ScopeMap.t
let hole_var : Dcalc.Ast.Var.t = Bindlib.new_var (fun x -> (Dcalc.Ast.EVar x, Pos.no_pos)) "hole"
let translate_rules (_p : scope_ctx) (_ctx : ctx) (_rules : Ast.rule list) : Dcalc.Ast.expr * ctx =
assert false
let translate_scope_decl (p : scope_ctx) (sigma : Ast.scope_decl) : Dcalc.Ast.expr =
let ctx = [] in
let _defs, ctx = translate_rules p ctx sigma.scope_decl_rules in
let _scope_variables =
List.filter_map (fun l -> match l with Ast.ScopeVar v -> Some v | _ -> None) ctx
in
assert false