Added HTML links in "fixed by" meta-assertions

Catala

Explore the docs »
View Tutorial • Report Bug • Contribute • Join Zulip Chat

Catala is a domain-specific language for deriving faithful-by-construction algorithms from legislative texts. To learn quickly about the language and its features, you can jump right to the official Catala tutorial. You can join the Catala community on Zulip!

Table of Contents

Concepts
Getting started
Building and installation
Usage
- Catala
- Clerk
Documentation
Examples
API
Contributing
Test suite
License
Limitations and disclaimer
Pierre Catala

Concepts

Catala is a programming language adapted for socio-fiscal legislative literate programming. By annotating each line of the legislative text with its meaning in terms of code, one can derive an implementation of complex socio-fiscal mechanisms that enjoys a high level of assurance regarding the code-law faithfulness.

Concretely, you have to first gather all the laws, executive orders, previous cases, etc. that contain information about the socio-fiscal mechanism that you want to implement. Then, you can proceed to annotate the text article by article, in your favorite text editor :

Once your code is complete and tested, you can use the Catala compiler to produce a lawyer-readable PDF version of your implementation. The Catala language has been specially designed in collaboration with law professionals to ensure that the code can be reviewed and certified correct by the domain experts, which are in this case lawyers and not programmers.

The Catala language is special because its logical structure mimics the logical structure of the law. Indeed, the core concept of "definition-under-conditions" that builds on default logic has been formalized by Professor Sarah Lawsky in her article A Logic for Statutes. The Catala language is the only programming language to our knowledge that embeds default logic as a first-class feature, which is why it is the only language perfectly adapted to literate legislative programming.

Getting started

To get started, the best place is the tutorial of the language. A French version is also available but might be out of sync with the latest language features.

Note: bleeding-edge version

If you are interested in the latest development version, pre-built artifacts including binaries and API documentation can be found at https://catalalang.github.io/catala

Building and installation

Catala is available as an opam package! If opam is installed on your machine, simply execute:

opam install catala

To get the cutting-edge, latest version of Catala, you can also do

opam pin add catala --dev-repo

However, if you wish to get the latest developments of the compiler, you probably want to compile it from the sources of this repository or use nix. For that, see the dedicated readme.

Usage

Catala

Use catala --help if you have installed it to get more information about the command line options available. The man page is also available online. To get the development version of the help, run make help_catala after make build. The catala binary corresponds to the Catala compiler.

The top-level Makefile contains a lot of useful targets to run. To display them, use

    make help

Plugin backends

While the compiler has some builtin backends for Catala (Python, Ocaml, etc.), it is also possible to add a custom backend to the Catala compiler without having to modify its source code. This plugin solution relies on dynamic linking: see the dedicated README.

Clerk

Use clerk --help if you have installed it to get more information about the command line options available. To get the development version of the help, run make help_clerk after make build. The clerk binary corresponds to the Catala build system, responsible for testing among other things.

To get more information about Clerk, see the dedicated readme

Catleg

Catleg is a command line utility providing useful integration with LégiFrance, the official repository of French legal documentation. See the decidated repository for more information.

Documentation

Syntax cheat sheet

A complete and handy reference of the Catala syntax can be found in the cheat sheet (for French and English versions of the syntax).

Formal semantics

To audit the formal proof of the partial certification of the Catala compiler, see the dedicated readme.

Compiler documentation

The documentation is accessible online, both for the latest release and bleeding-edge version.

It is otherwise generated from the compiler source code using dune and odoc. Run

make doc

to generate the documentation, then open the doc/odoc.html file in any browser.

Examples

To explore the different programs written in Catala, see the dedicated readme.

API

To know how to use the code generated by the Catala compiler in your favorite programming language, head to the readme of the French law library. The corresponding pre-built examples are also available.

Contributing

To know how you can contribute to the project, see the dedicated readme.

Test suite

To know how to run or improve the Catala reference test suite, see the dedicated readme.

License

The compiler and all the code contained in this repository is released under the Apache license (version 2) unless another license is explicited for a sub-directory.

Limitations and disclaimer

Catala is a research project from Inria, the French National Research Institute for Computer Science. The compiler is yet unstable and lacks some of its features.

Pierre Catala

The language is named after Pierre Catala, a professor of law who pionneered the French legaltech by creating a computer database of law cases, Juris-Data. The research group that he led in the late 1960s, the Centre d’études et de traitement de l’information juridique (CETIJ), has also influenced the creation by state conselor Lucien Mehl of the Centre de recherches et développement en informatique juridique (CENIJ), which eventually transformed into the entity managing the LegiFrance website, acting as the public service of legislative documentation.

	let rec translate_default (ctx : ctx) (exceptions : D.expr Pos.marked list)
	(just : D.expr Pos.marked) (cons : D.expr Pos.marked) (pos_default : Pos.t) :
	A.expr Pos.marked Bindlib.box =
	let exceptions =
	List.map (fun except -> thunk_expr (translate_expr ctx except) pos_default) exceptions
	in
	let exceptions =
	A.make_app (handle_default pos_default)
	[
	Bindlib.box_apply
	(fun exceptions -> (A.EArray exceptions, pos_default))
	(Bindlib.box_list exceptions);
	thunk_expr (translate_expr ctx just) pos_default;
	thunk_expr (translate_expr ctx cons) pos_default;
	]
	pos_default
	in
	exceptions

	and translate_expr (ctx : ctx) (e : D.expr Pos.marked) : A.expr Pos.marked Bindlib.box =
	match Pos.unmark e with
	\| D.EVar v -> D.VarMap.find (Pos.unmark v) ctx
	\| D.ETuple (args, s) ->
	Bindlib.box_apply
	(fun args -> Pos.same_pos_as (A.ETuple (args, s)) e)
	(Bindlib.box_list (List.map (translate_expr ctx) args))
	\| D.ETupleAccess (e1, i, s, ts) ->
	Bindlib.box_apply
	(fun e1 -> Pos.same_pos_as (A.ETupleAccess (e1, i, s, ts)) e)
	(translate_expr ctx e1)
	\| D.EInj (e1, i, en, ts) ->
	Bindlib.box_apply
	(fun e1 -> Pos.same_pos_as (A.EInj (e1, i, en, ts)) e)
	(translate_expr ctx e1)
	\| D.EMatch (e1, cases, en) ->
	Bindlib.box_apply2
	(fun e1 cases -> Pos.same_pos_as (A.EMatch (e1, cases, en)) e)
	(translate_expr ctx e1)
	(Bindlib.box_list (List.map (translate_expr ctx) cases))
	\| D.EArray es ->
	Bindlib.box_apply
	(fun es -> Pos.same_pos_as (A.EArray es) e)
	(Bindlib.box_list (List.map (translate_expr ctx) es))
	\| D.ELit l -> Bindlib.box (Pos.same_pos_as (translate_lit l) e)
	\| D.EOp op -> Bindlib.box (Pos.same_pos_as (A.EOp op) e)
	\| D.EIfThenElse (e1, e2, e3) ->
	Bindlib.box_apply3
	(fun e1 e2 e3 -> Pos.same_pos_as (A.EIfThenElse (e1, e2, e3)) e)
	(translate_expr ctx e1) (translate_expr ctx e2) (translate_expr ctx e3)
	\| D.EAssert e1 ->
	Bindlib.box_apply (fun e1 -> Pos.same_pos_as (A.EAssert e1) e) (translate_expr ctx e1)
	\| D.EApp (e1, args) ->
	Bindlib.box_apply2
	(fun e1 args -> Pos.same_pos_as (A.EApp (e1, args)) e)
	(translate_expr ctx e1)
	(Bindlib.box_list (List.map (translate_expr ctx) args))
	\| D.EAbs (pos_binder, binder, ts) ->
	let vars, body = Bindlib.unmbind binder in
	let ctx, lc_vars =
	Array.fold_right
	(fun var (ctx, lc_vars) ->
	let lc_var = A.Var.make (Bindlib.name_of var, pos_binder) in
	let lc_var_expr = A.make_var (lc_var, pos_binder) in
	(D.VarMap.add var lc_var_expr ctx, lc_var :: lc_vars))
	vars (ctx, [])
	in
	let lc_vars = Array.of_list lc_vars in
	let new_body = translate_expr ctx body in
	let new_binder = Bindlib.bind_mvar lc_vars new_body in
	Bindlib.box_apply
	(fun new_binder -> Pos.same_pos_as (A.EAbs (pos_binder, new_binder, ts)) e)
	new_binder
	\| D.EDefault (exceptions, just, cons) ->
	translate_default ctx exceptions just cons (Pos.get_position e)

	{v
	+---------------+
	\| \|
	\| Surface AST \|
	\| \|
	+---------------+
	\|
	* Separate code from legislation \|
	* Remove syntactic sugars \|
	v
	+---------------+
	\| \|
	\| Desugared AST \|
	\| \|
	+---------------+
	\|
	* Build rule trees for each definition \|
	* Order variable computations inside scope \|
	v
	+--------------------+
	\| \|
	\| Scope language AST \|
	\| \|
	+--------------------+
	\|
	* Convert scopes into functions \|
	* Thunking of subscope arguments \|
	\|
	v
	+----------------------+
	\| \|
	\| Default calculus AST \|
	\| \|
	+----------------------+ v}

	let rec def_map_to_tree (def_info : Ast.ScopeDef.t)
	(is_def_func : Scopelang.Ast.typ Pos.marked option) (def : Ast.rule Ast.RuleMap.t) :
	rule_tree list =
	(* first we look to the rules that don't have any exceptions *)
	let has_no_exception (r : Ast.RuleName.t) _ =
	not
	(Ast.RuleMap.exists
	(fun _ r' -> match r'.Ast.exception_to_rule with Some r_ex -> r_ex = r \| None -> false)
	def)
	in
	let no_exceptions = Ast.RuleMap.filter has_no_exception def in
	(* Then, for each top-level rule (that has no exceptions), we build a rule tree *)
	(* Among the top-level rules are the base rules that are exceptions to nothing *)
	let base_rules, rules_that_are_exceptions =
	Ast.RuleMap.partition (fun _ r -> Option.is_none r.Ast.exception_to_rule) no_exceptions
	in
	let base_trees : rule_tree Ast.RuleMap.t =
	Ast.RuleMap.map
	(fun r ->
	(* we look at the the eventual rule of which r is an exception *)
	match r.Ast.exception_to_rule with None -> Leaf r \| Some _ -> assert false
	(* should not happen *))
	base_rules
	in
	(* Now let's deal with the rules that are exceptions but have no exception. We have to bucket
	these, each bucket containing all the rules that are exception to the same rule *)
	let exception_targets =
	Ast.RuleMap.fold
	(fun _ r acc ->
	match r.Ast.exception_to_rule with
	\| None -> assert false (* should not happen *)
	\| Some r' -> Ast.RuleMap.add r' () acc)
	rules_that_are_exceptions Ast.RuleMap.empty
	in
	(* In each bucket corresponding to an exception target, we have all the rules that are exceptions
	to the target *)
	let exception_trees =
	Ast.RuleMap.mapi
	(fun r' _ ->
	(* we recursively call the function of a def where we have removed exception edges: this is
	why the function should terminate *)
	let def_rec =
	Ast.RuleMap.map
	(fun r ->
	{
	r with
	Ast.exception_to_rule =
	( match r.Ast.exception_to_rule with
	\| None -> None
	\| Some r'' -> if r'' = r' then None else Some r'' );
	})
	def
	in
	let def_rec =
	Ast.RuleMap.filter (fun r _ -> not (Ast.RuleMap.mem r exception_targets)) def_rec
	in
	let exceptions = def_map_to_tree def_info is_def_func def_rec in
	Node (exceptions, Ast.RuleMap.find r' def))
	exception_targets
	in
	List.map snd (Ast.RuleMap.bindings base_trees)
	@ List.map snd (Ast.RuleMap.bindings exception_trees)

	@Test@

	/*
	new scope A:
	param x content int

	scope A:
	label base_x
	def x := 0

	label exception_x
	exception base_x
	def x := 1

	exception exception_x
	def x := 2
	*/

	@@Master file@@

	@@Include: preamble.catala_en@@

	@@Include: section_121.catala_en@@

	@@Include: section_132.catala_en@@

	@@Include: section_1015.catala_en@@

	\| Ast.Aggregate (Ast.AggregateExtremum _) ->
	Errors.raise_spanned_error "Unsupported feature: minimum and maximum"
	(Pos.get_position op')

	\| Dotted of expression Pos.marked * constructor Pos.marked option * ident Pos.marked
	(** Dotted is for both struct field projection and sub-scope variables *)

	champ d'application EnfantLePlusÂgé:
	définition est_le_plus_âgé de enfant égal à
	faux # TODO: changer!

	label article_5
	definition income_tax equals two_brackets.tax_formula of individual.income

	# Then, you can declare the exception by referring back to the label
	exception article_5
	definition income_tax under condition
	individual.income <=$ $10,000
	consequence equals $0

	new enum E:
	-- Case1
	-- Case2

	new enum F:
	-- Case3
	-- Case4

	new scope A:
	param x content E
	param y content bool

	scope A:
	def x := Case1
	def y := x with Case3

	[RESULT] Computation successful! Results:
	[RESULT] x = Case1 ()
	[RESULT] y = true

	\| ETuple of (expr Pos.marked * Uid.MarkedString.info option) list
	(** The [MarkedString.info] is the former struct field name*)
	\| ETupleAccess of expr Pos.marked * int * Uid.MarkedString.info option * typ Pos.marked list
	(** The [MarkedString.info] is the former struct field name *)
	\| EInj of expr Pos.marked * int * Uid.MarkedString.info * typ Pos.marked list
	(** The [MarkedString.info] is the former enum case name *)
	\| EMatch of expr Pos.marked * (expr Pos.marked * Uid.MarkedString.info) list
	(** The [MarkedString.info] is the former enum case name *)

	\| EStruct (struct_name, e_fields) ->
	let struct_sig = Ast.StructMap.find struct_name ctx.structs in
	let d_fields, remaining_e_fields =
	List.fold_right
	(fun (field_name, _) (d_fields, e_fields) ->
	let field_e =
	try Ast.StructFieldMap.find field_name e_fields
	with Not_found ->
	Errors.raise_spanned_error
	(Format.asprintf "Missing field for structure %a: \"%a\""
	Ast.StructName.format_t struct_name Ast.StructFieldName.format_t field_name)
	(Pos.get_position e)
	in
	let field_d = translate_expr ctx field_e in
	let field_d =
	Bindlib.box_apply
	(fun field_d -> (field_d, Some (Ast.StructFieldName.get_info field_name)))
	field_d
	in
	(field_d :: d_fields, Ast.StructFieldMap.remove field_name e_fields))
	struct_sig ([], e_fields)
	in
	if Ast.StructFieldMap.cardinal remaining_e_fields > 0 then
	Errors.raise_spanned_error
	(Format.asprintf "The fields \"%a\" do not belong to the structure %a"
	Ast.StructName.format_t struct_name
	(Format.pp_print_list
	~pp_sep:(fun fmt () -> Format.fprintf fmt ", ")
	(fun fmt (field_name, _) ->
	Format.fprintf fmt "%a" Ast.StructFieldName.format_t field_name))
	(Ast.StructFieldMap.bindings remaining_e_fields))
	(Pos.get_position e)
	else
	Bindlib.box_apply (fun d_fields -> Dcalc.Ast.ETuple d_fields) (Bindlib.box_list d_fields)
	\| EStructAccess (e1, field_name, struct_name) ->
	let struct_sig = Ast.StructMap.find struct_name ctx.structs in
	let _, field_index =
	try List.assoc field_name (List.mapi (fun i (x, y) -> (x, (y, i))) struct_sig)
	with Not_found ->
	Errors.raise_spanned_error
	(Format.asprintf "The field \"%a\" does not belong to the structure %a"
	Ast.StructFieldName.format_t field_name Ast.StructName.format_t struct_name)
	(Pos.get_position e)
	in
	let e1 = translate_expr ctx e1 in
	Bindlib.box_apply
	(fun e1 ->
	Dcalc.Ast.ETupleAccess
	( e1,
	field_index,
	Some (Ast.StructFieldName.get_info field_name),
	List.map (fun (_, t) -> translate_typ ctx t) struct_sig ))
	e1
	\| EEnumInj (e1, constructor, enum_name) ->
	let enum_sig = Ast.EnumMap.find enum_name ctx.enums in
	let _, constructor_index =
	try List.assoc constructor (List.mapi (fun i (x, y) -> (x, (y, i))) enum_sig)
	with Not_found ->
	Errors.raise_spanned_error
	(Format.asprintf "The constructor \"%a\" does not belong to the enum %a"
	Ast.EnumConstructor.format_t constructor Ast.EnumName.format_t enum_name)
	(Pos.get_position e)
	in
	let e1 = translate_expr ctx e1 in
	Bindlib.box_apply
	(fun e1 ->
	Dcalc.Ast.EInj
	( e1,
	constructor_index,
	Ast.EnumConstructor.get_info constructor,
	List.map (fun (_, t) -> translate_typ ctx t) enum_sig ))
	e1
	\| EMatch (e1, enum_name, cases) ->
	let enum_sig = Ast.EnumMap.find enum_name ctx.enums in
	let d_cases, remaining_e_cases =
	List.fold_right
	(fun (constructor, _) (d_cases, e_cases) ->
	let case_e =
	try Ast.EnumConstructorMap.find constructor e_cases
	with Not_found ->
	Errors.raise_spanned_error
	(Format.asprintf
	"The constructor %a of enum %a is missing from this pattern matching"
	Ast.EnumConstructor.format_t constructor Ast.EnumName.format_t enum_name)
	(Pos.get_position e)
	in
	let case_d = translate_expr ctx case_e in
	let case_d =
	Bindlib.box_apply
	(fun case_d -> (case_d, Ast.EnumConstructor.get_info constructor))
	case_d
	in
	(case_d :: d_cases, Ast.EnumConstructorMap.remove constructor e_cases))
	enum_sig ([], cases)
	in
	if Ast.EnumConstructorMap.cardinal remaining_e_cases > 0 then
	Errors.raise_spanned_error
	(Format.asprintf "Patter matching is incomplete for enum %a: missing cases %a"
	Ast.EnumName.format_t enum_name
	(Format.pp_print_list
	~pp_sep:(fun fmt () -> Format.fprintf fmt ", ")
	(fun fmt (case_name, _) ->
	Format.fprintf fmt "%a" Ast.EnumConstructor.format_t case_name))
	(Ast.EnumConstructorMap.bindings remaining_e_cases))
	(Pos.get_position e)
	else
	let e1 = translate_expr ctx e1 in
	Bindlib.box_apply2
	(fun d_fields e1 -> Dcalc.Ast.EMatch (e1, d_fields))
	(Bindlib.box_list d_cases) e1

	scope PeriodMerge:
	# Placeholders, overwritten by caller
	definition periods1 equals []
	definition periods2 equals []

	# TODO: find a way to implement the merging of two collections of date
	# periods into a single non-overlapping collection of date periods such
	# that the output covers both input date ranges.
	definition output equals []

	\| INT_TO_DEC {
	(Builtin IntToDec, $sloc)
	}
	\| GET_DAY {
	(Builtin GetDay, $sloc)
	}
	\| GET_MONTH {
	(Builtin GetMonth, $sloc)
	}
	\| GET_YEAR {
	(Builtin GetYear, $sloc)
	}

	\| e = small_expression DOT i = ident {
	(Dotted (e, i), Pos.from_lpos $sloc)
	}

	\| Dotted (e, x) -> (
	match Pos.unmark e with
	\| Ident y when Name_resolution.is_subscope_uid scope ctxt y ->
	(* In this case, y.x is a subscope variable *)
	let subscope_uid : Scopelang.Ast.SubScopeName.t =
	Name_resolution.get_subscope_uid scope ctxt (Pos.same_pos_as y e)
	in
	let subscope_real_uid : Scopelang.Ast.ScopeName.t =
	Scopelang.Ast.SubScopeMap.find subscope_uid scope_ctxt.sub_scopes
	in
	let subscope_var_uid = Name_resolution.get_var_uid subscope_real_uid ctxt x in
	Bindlib.box
	( Scopelang.Ast.ELocation
	(SubScopeVar (subscope_real_uid, (subscope_uid, pos), (subscope_var_uid, pos))),
	pos )
	\| _ ->
	(* In this case e.x is the struct field x access of expression e *)
	let e = translate_expr scope ctxt e in
	let x_possible_structs =
	try Desugared.Ast.IdentMap.find (Pos.unmark x) ctxt.field_idmap
	with Not_found ->
	Errors.raise_spanned_error "This identifier should refer to a struct field"
	(Pos.get_position x)
	in
	if Scopelang.Ast.StructMap.cardinal x_possible_structs > 1 then
	Errors.raise_spanned_error
	(Format.asprintf
	"This struct field name is ambiguous, it can belong to %a. Desambiguate it by \
	prefixing it with the struct name."
	(Format.pp_print_list
	~pp_sep:(fun fmt () -> Format.fprintf fmt " or ")
	(fun fmt (s_name, _) ->
	Format.fprintf fmt "%a" Scopelang.Ast.StructName.format_t s_name))
	(Scopelang.Ast.StructMap.bindings x_possible_structs))
	(Pos.get_position x)
	else
	let s_uid, f_uid = Scopelang.Ast.StructMap.choose x_possible_structs in
	Bindlib.box_apply (fun e -> (Scopelang.Ast.EStructAccess (e, f_uid, s_uid), pos)) e )

	\| VERTICAL d = date_int DIV m = date_int DIV y = date_int VERTICAL {
	(LDate {
	literal_date_day = (match !Utils.Cli.locale_lang with `En -> m \| `Fr -> d);
	literal_date_month = (match !Utils.Cli.locale_lang with `En -> d \| `Fr -> m);
	literal_date_year = y;
	}, Pos.from_lpos $sloc)
	}

	\| MatchWith (e1, (cases, _cases_pos)) ->
	let e1 = translate_expr scope ctxt e1 in
	let cases_d, e_uid =
	List.fold_left
	(fun (cases_d, e_uid) (case, pos_case) ->
	match Pos.unmark case.Ast.match_case_pattern with
	\| [ constructor ], binding ->
	let possible_c_uids =
	try Desugared.Ast.IdentMap.find (Pos.unmark constructor) ctxt.constructor_idmap
	with Not_found ->
	Errors.raise_spanned_error
	"The name of this constructor has not been defined before, maybe it is a \
	typo?"
	(Pos.get_position constructor)
	in
	if e_uid = None && Scopelang.Ast.EnumMap.cardinal possible_c_uids > 1 then
	Errors.raise_spanned_error
	(Format.asprintf
	"This constuctor name is ambiguous, it can belong to %a. Desambiguate it by \
	prefixing it with the enum name."
	(Format.pp_print_list
	~pp_sep:(fun fmt () -> Format.fprintf fmt " or ")
	(fun fmt (s_name, _) ->
	Format.fprintf fmt "%a" Scopelang.Ast.EnumName.format_t s_name))
	(Scopelang.Ast.EnumMap.bindings possible_c_uids))
	(Pos.get_position constructor)
	else
	let e_uid, c_uid =
	match e_uid with
	\| Some e_uid -> (
	( e_uid,
	try Scopelang.Ast.EnumMap.find e_uid possible_c_uids
	with Not_found ->
	Errors.raise_spanned_error
	(Format.asprintf "This constructor is not part of the %a enumeration"
	Scopelang.Ast.EnumName.format_t e_uid)
	(Pos.get_position constructor) ) )
	\| None -> Scopelang.Ast.EnumMap.choose possible_c_uids
	in
	( match Scopelang.Ast.EnumConstructorMap.find_opt c_uid cases_d with

	let disambiguate_constructor (ctxt : Name_resolution.context) (constructor : string Pos.marked list)
	(pos : Pos.t) : Scopelang.Ast.EnumName.t * Scopelang.Ast.EnumConstructor.t =
	let constructor =
	match constructor with
	\| [ c ] -> c
	\| _ ->
	Errors.raise_spanned_error "The deep pattern matching syntactic sugar is not yet supported"
	pos
	in
	let possible_c_uids =
	try Desugared.Ast.IdentMap.find (Pos.unmark constructor) ctxt.constructor_idmap
	with Not_found ->
	Errors.raise_spanned_error
	"The name of this constructor has not been defined before, maybe it is a typo?"
	(Pos.get_position constructor)
	in
	if Scopelang.Ast.EnumMap.cardinal possible_c_uids > 1 then
	Errors.raise_spanned_error
	(Format.asprintf
	"This constuctor name is ambiguous, it can belong to %a. Desambiguate it by prefixing it \
	with the enum name."
	(Format.pp_print_list
	~pp_sep:(fun fmt () -> Format.fprintf fmt " or ")
	(fun fmt (s_name, _) -> Format.fprintf fmt "%a" Scopelang.Ast.EnumName.format_t s_name))
	(Scopelang.Ast.EnumMap.bindings possible_c_uids))
	(Pos.get_position constructor);
	Scopelang.Ast.EnumMap.choose possible_c_uids

	\| "@@", Star white_space, "Master file", Star white_space, "@@" -> MASTER_FILE
	\| "@@", Star white_space, "Begin metadata", Star white_space, "@@" -> BEGIN_METADATA
	\| "@@", Star white_space, "End metadata", Star white_space, "@@" -> END_METADATA
	\| ( "@@",
	Star white_space,
	"Include:",
	Star white_space,
	Plus (Compl '@'),
	Star white_space,
	Opt ('@', Star white_space, "p.", Star white_space, Plus '0' .. '9', Star white_space),
	"@@" ) ->
	let extract_components =
	R.regexp "@@\\sInclude\\:\\s([^@]+)\\s(@\\sp\\.\\s*([0-9]+)\|)@@"
	in
	let get_component = R.get_substring (R.exec ~rex:extract_components (Utf8.lexeme lexbuf)) in
	let name = get_component 1 in
	let pages = try Some (int_of_string (get_component 3)) with Not_found -> None in
	let pos = lexing_positions lexbuf in
	if Filename.extension name = ".pdf" then LAW_INCLUDE (Ast.PdfFile ((name, pos), pages))
	else LAW_INCLUDE (Ast.CatalaFile (name, pos))
	\| "@@", Plus (Compl '@'), "@@", Star '+' ->
	let extract_code_title = R.regexp "@@([^@]+)@@([\\+]*)" in
	let get_match = R.get_substring (R.exec ~rex:extract_code_title (Utf8.lexeme lexbuf)) in
	let get_new_lines = R.regexp "\n" in
	let new_lines_count =
	try Array.length (R.extract ~rex:get_new_lines (Utf8.lexeme lexbuf)) with Not_found -> 0
	in
	for _i = 1 to new_lines_count do
	new_line lexbuf
	done;
	let law_title = get_match 1 in
	let precedence = String.length (get_match 2) in

	LAW_HEADING (law_title, precedence)
	\| "@", Plus (Compl '@'), "@" ->
	let extract_article_title = R.regexp "@([^@]+)@" in
	let title = R.get_substring (R.exec ~rex:extract_article_title (Utf8.lexeme lexbuf)) 1 in
	let get_new_lines = R.regexp "\n" in
	let new_lines_count =
	try Array.length (R.extract ~rex:get_new_lines (Utf8.lexeme lexbuf)) with Not_found -> 0
	in
	(* the -1 is here to compensate for Sedlex's automatic newline detection around token *)
	for _i = 1 to new_lines_count - 1 do
	new_line lexbuf
	done;

	LAW_ARTICLE (title, None, None)

	let op_type (op : A.operator Pos.marked) : typ Pos.marked UnionFind.elem =
	let pos = Pos.get_position op in
	let bt = UnionFind.make (TLit TBool, pos) in
	let it = UnionFind.make (TLit TInt, pos) in
	let rt = UnionFind.make (TLit TRat, pos) in
	let mt = UnionFind.make (TLit TMoney, pos) in
	let dut = UnionFind.make (TLit TDuration, pos) in
	let dat = UnionFind.make (TLit TDate, pos) in
	let any = UnionFind.make (TAny (Any.fresh ()), pos) in
	let array_any = UnionFind.make (TArray any, pos) in
	let any2 = UnionFind.make (TAny (Any.fresh ()), pos) in
	let arr x y = UnionFind.make (TArrow (x, y), pos) in
	match Pos.unmark op with
	\| A.Ternop A.Fold -> arr (arr any2 (arr any any2)) (arr any2 (arr array_any any2))
	\| A.Binop (A.And \| A.Or) -> arr bt (arr bt bt)
	\| A.Binop (A.Add KInt \| A.Sub KInt \| A.Mult KInt \| A.Div KInt) -> arr it (arr it it)
	\| A.Binop (A.Add KRat \| A.Sub KRat \| A.Mult KRat \| A.Div KRat) -> arr rt (arr rt rt)
	\| A.Binop (A.Add KMoney \| A.Sub KMoney) -> arr mt (arr mt mt)
	\| A.Binop (A.Add KDuration \| A.Sub KDuration) -> arr dut (arr dut dut)
	\| A.Binop (A.Sub KDate) -> arr dat (arr dat dut)
	\| A.Binop (A.Add KDate) -> arr dat (arr dut dat)
	\| A.Binop (A.Div KMoney) -> arr mt (arr mt rt)
	\| A.Binop (A.Mult KMoney) -> arr mt (arr rt mt)
	\| A.Binop (A.Lt KInt \| A.Lte KInt \| A.Gt KInt \| A.Gte KInt) -> arr it (arr it bt)
	\| A.Binop (A.Lt KRat \| A.Lte KRat \| A.Gt KRat \| A.Gte KRat) -> arr rt (arr rt bt)
	\| A.Binop (A.Lt KMoney \| A.Lte KMoney \| A.Gt KMoney \| A.Gte KMoney) -> arr mt (arr mt bt)
	\| A.Binop (A.Lt KDate \| A.Lte KDate \| A.Gt KDate \| A.Gte KDate) -> arr dat (arr dat bt)
	\| A.Binop (A.Lt KDuration \| A.Lte KDuration \| A.Gt KDuration \| A.Gte KDuration) ->
	arr dut (arr dut bt)
	\| A.Binop (A.Eq \| A.Neq) -> arr any (arr any bt)
	\| A.Binop A.Map -> arr (arr any any2) (arr array_any any2)
	\| A.Unop (A.Minus KInt) -> arr it it
	\| A.Unop (A.Minus KRat) -> arr rt rt
	\| A.Unop (A.Minus KMoney) -> arr mt mt
	\| A.Unop (A.Minus KDuration) -> arr dut dut
	\| A.Unop A.Not -> arr bt bt
	\| A.Unop A.ErrorOnEmpty -> arr any any
	\| A.Unop (A.Log _) -> arr any any
	\| A.Unop A.Length -> arr array_any it
	\| A.Unop A.IntToRat -> arr it rt
	\| Binop (Mult (KDate \| KDuration)) \| Binop (Div (KDate \| KDuration)) \| Unop (Minus KDate) ->
	Errors.raise_spanned_error "This operator is not available!" pos

	(** Transforms a flat list of rules into a tree, taking into account the priorities declared between
	rules

	{e Invariant:} there are no exceptions cycles

	{e Invariant:} there are no dandling exception pointers in the rules *)
	let rec def_map_to_tree (def_info : Ast.ScopeDef.t)
	(is_def_func : Scopelang.Ast.typ Pos.marked option) (def : Ast.rule Ast.RuleMap.t) :
	rule_tree list =

catalalang / catala Goto Github PK

catala's Introduction

Catala

Concepts

Getting started

Building and installation

Usage

Catala

Plugin backends

Clerk

Catleg

Documentation

Syntax cheat sheet

Formal semantics

Compiler documentation

Examples

API

Contributing

Test suite

License

Limitations and disclaimer

Pierre Catala

catala's People

Contributors

Stargazers

Watchers

Forkers

catala's Issues

The problem

Objectives

New solution

The problem

Design of a simple module system

Syntax

External module lookup.

Compilation units

Literate programming

Implementation

Context

Goal

What to do ?

Why is it like this?

Replace with nominal typing

The problem

A proposal for scope functors

The problem

What do do?

The problem

How to fix it ?

The problem

How to implement the solution

Towards a markdown syntax

How to implement that

The problem

Design of an external implementations systems

Syntax

Compilation

Intererpreter

Why is it like this?

Hindley-Milner inference with constraints

A compromise

Recommend Projects

Recommend Topics

Recommend Org