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

Preliminary support for modules/externals + CLI subcommands (#478)

Browse Source
This commit is contained in:
Louis Gesbert 2023-06-20 09:31:45 +02:00 committed by GitHub
commit f31a78593e
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
50 changed files with 1220 additions and 689 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

41
Dockerfile
View File

@ -1,15 +1,9 @@
# Stage 1: setup an opam switch with all dependencies installed
#
# STAGE 1: setup an opam switch with all dependencies installed
#
# (only depends on the opam files)
FROM ocamlpro/ocaml:4.14-2023-04-02 AS dev-build-context
# pandoc and ninja are not in alpine stable yet, install it manually with an explicit repository
RUN sudo apk add pandoc --repository=http://dl-cdn.alpinelinux.org/alpine/edge/community/
# In order to compiler rescript for `npm install` in french_law/js we need
# the following dependencies (according to https://github.com/GlancingMind/rescript-alpine-docker)
RUN sudo apk add python3
RUN sudo ln -s /usr/bin/python3 /usr/bin/python
RUN sudo apk add g++
RUN sudo apk add make
FROM ocamlpro/ocaml:4.14-2023-06-18 AS dev-build-context
# Image from https://hub.docker.com/r/ocamlpro/ocaml
RUN mkdir catala
WORKDIR catala
@ -22,16 +16,31 @@ ENV OPAMVAR_cataladevmode=1
ENV OPAMVAR_catalaz3mode=1
# Get a switch with all the dependencies installed
RUN opam --cli=2.1 update && \
opam --cli=2.1 switch create catala ocaml-system && \
opam --cli=2.1 pin . --no-action && \
# DON'T run 'opam update' here. Instead use a newer parent Docker image
# (update the 'FROM' line above)
RUN opam --cli=2.1 switch create catala ocaml-system && \
opam --cli=2.1 install . --with-test --with-doc --depext-only && \
opam --cli=2.1 install . --with-test --with-doc --deps-only && \
opam clean
# Note: just one `opam switch create .` command should be enough once opam 2.1.3 is released (opam#5047 ; opam#5185)
# Note: just `opam switch create . --deps-only --with-test --with-doc && opam clean`
# should be enough once opam 2.2 is released (see opam#5185)
# Install extra dependencies not handled yet by the opam depexts
#
# python3, ninja (samurai in this case), etc. already got installed through opam's
# depext mechanism at this point -- see clerk.opam and catala.opam
#
# pandoc is not in alpine stable yet though, so install it manually with an explicit repository
RUN sudo apk add pandoc --repository=http://dl-cdn.alpinelinux.org/alpine/edge/community/
# Workaround broken rescript build that recompiles its own version of
# ninja with a badly written script :[]
RUN sudo apk add pythonispython3
# Stage 2: get the whole repo, run checks and builds
#
# STAGE 2: get the whole repo, run checks and builds
#
FROM dev-build-context
# Get the full repo

1
catala.opam
View File

@ -53,6 +53,7 @@ depends: [
depopts: ["z3"]
conflicts: [
"z3" {< "4.8.11"}
"base" {>= "v0.16.0"}
]
build: [
["dune" "subst"] {dev}

239
compiler/catala_utils/cli.ml
View File

@ -17,7 +17,7 @@
type backend_lang = En | Fr | Pl
type backend_option_builtin =
type backend_option =
[ `Latex
| `Makefile
| `Html
@ -33,8 +33,6 @@ type backend_option_builtin =
| `Exceptions
| `Proof ]
type 'a backend_option = [ backend_option_builtin | `Plugin of 'a ]
(** Associates a {!type: Cli.backend_lang} with its string represtation. *)
let languages = ["en", En; "fr", Fr; "pl", Pl]
@ -42,41 +40,6 @@ let language_code =
let rl = List.map (fun (a, b) -> b, a) languages in
fun l -> List.assoc l rl
let backend_option_to_string = function
| `Interpret -> "Interpret"
| `Interpret_Lcalc -> "Interpret_Lcalc"
| `Makefile -> "Makefile"
| `OCaml -> "Ocaml"
| `Scopelang -> "Scopelang"
| `Dcalc -> "Dcalc"
| `Latex -> "Latex"
| `Proof -> "Proof"
| `Html -> "Html"
| `Python -> "Python"
| `Typecheck -> "Typecheck"
| `Scalc -> "Scalc"
| `Lcalc -> "Lcalc"
| `Exceptions -> "Exceptions"
| `Plugin s -> s
let backend_option_of_string backend =
match String.lowercase_ascii backend with
| "interpret" -> `Interpret
| "interpret_lcalc" -> `Interpret_Lcalc
| "makefile" -> `Makefile
| "ocaml" -> `OCaml
| "scopelang" -> `Scopelang
| "dcalc" -> `Dcalc
| "latex" -> `Latex
| "proof" -> `Proof
| "html" -> `Html
| "python" -> `Python
| "typecheck" -> `Typecheck
| "scalc" -> `Scalc
| "lcalc" -> `Lcalc
| "exceptions" -> `Exceptions
| s -> `Plugin s
(** Source files to be compiled *)
let source_files : string list ref = ref []
@ -109,7 +72,7 @@ open Cmdliner
let file =
Arg.(
required
& pos 1 (some file) None
& pos 0 (some file) None
& info [] ~docv:"FILE" ~doc:"Catala master file to be compiled.")
let debug =
@ -143,7 +106,7 @@ let unstyled =
Arg.(
value
& flag
& info ["unstyled"; "u"]
& info ["unstyled"]
~doc:
"Removes styling (colors, etc.) from terminal output. Equivalent to \
$(b,--color=never)")
@ -203,14 +166,6 @@ let print_only_law =
"In literate programming output, skip all code and metadata sections \
and print only the text of the law.")
let backend =
Arg.(
required
& pos 0 (some string) None
& info [] ~docv:"COMMAND"
~doc:
"Backend selection (see the list of commands for available options).")
let plugins_dirs =
let doc = "Set the given directory to be searched for backend plugins." in
let env = Cmd.Env.info "CATALA_PLUGINS" ~doc in
@ -277,13 +232,24 @@ let output =
compiler. Defaults to $(i,FILE).$(i,EXT) where $(i,EXT) depends on \
the chosen backend. Use $(b,-o -) for stdout.")
type options = {
let link_modules =
Arg.(
value
& opt_all file []
& info ["use"; "u"] ~docv:"FILE"
~doc:
"Specifies an additional module to be linked to the Catala program. \
$(i,FILE) must be a catala file with a metadata section expressing \
what is exported ; for interpretation, a compiled OCaml shared \
module by the same basename (either .cmo or .cmxs) will be \
expected.")
type global_options = {
debug : bool;
color : when_enum;
message_format : message_format_enum;
wrap_weaved_output : bool;
avoid_exceptions : bool;
backend : string;
plugins_dirs : string list;
language : string option;
max_prec_digits : int option;
@ -297,9 +263,10 @@ type options = {
output_file : string option;
closure_conversion : bool;
print_only_law : bool;
link_modules : string list;
}
let options =
let global_options =
let make
debug
color
@ -308,7 +275,6 @@ let options =
wrap_weaved_output
avoid_exceptions
closure_conversion
backend
plugins_dirs
language
max_prec_digits
@ -320,14 +286,14 @@ let options =
ex_scope
ex_variable
output_file
print_only_law : options =
print_only_law
link_modules : global_options =
{
debug;
color = (if unstyled then Never else color);
message_format;
wrap_weaved_output;
avoid_exceptions;
backend;
plugins_dirs;
language;
max_prec_digits;
@ -341,6 +307,7 @@ let options =
output_file;
closure_conversion;
print_only_law;
link_modules;
}
in
Term.(
@ -352,7 +319,6 @@ let options =
$ wrap_weaved_output
$ avoid_exceptions
$ closure_conversion
$ backend
$ plugins_dirs
$ language
$ max_prec_digits_opt
@ -364,9 +330,8 @@ let options =
$ ex_scope
$ ex_variable
$ output
$ print_only_law)
let catala_t f = Term.(const f $ file $ options)
$ print_only_law
$ link_modules)
let set_option_globals options : unit =
debug_flag := options.debug;
@ -382,6 +347,101 @@ let set_option_globals options : unit =
avoid_exceptions_flag := options.avoid_exceptions;
message_format_flag := options.message_format
let subcommands handler =
[
Cmd.v
(Cmd.info "interpret"
~doc:
"Runs the interpreter on the Catala program, executing the scope \
specified by the $(b,-s) option assuming no additional external \
inputs.")
Term.(const (handler `Interpret) $ file $ global_options);
Cmd.v
(Cmd.info "interpret_lcalc"
~doc:
"Runs the interpreter on the lcalc pass on the Catala program, \
executing the scope specified by the $(b,-s) option assuming no \
additional external inputs.")
Term.(const (handler `Interpret_Lcalc) $ file $ global_options);
Cmd.v
(Cmd.info "typecheck"
~doc:"Parses and typechecks a Catala program, without interpreting it.")
Term.(const (handler `Typecheck) $ file $ global_options);
Cmd.v
(Cmd.info "proof"
~doc:
"Generates and proves verification conditions about the \
well-behaved execution of the Catala program.")
Term.(const (handler `Proof) $ file $ global_options);
Cmd.v
(Cmd.info "ocaml"
~doc:"Generates an OCaml translation of the Catala program.")
Term.(const (handler `OCaml) $ file $ global_options);
Cmd.v
(Cmd.info "python"
~doc:"Generates a Python translation of the Catala program.")
Term.(const (handler `Python) $ file $ global_options);
Cmd.v
(Cmd.info "latex"
~doc:
"Weaves a LaTeX literate programming output of the Catala program.")
Term.(const (handler `Latex) $ file $ global_options);
Cmd.v
(Cmd.info "html"
~doc:
"Weaves an HTML literate programming output of the Catala program.")
Term.(const (handler `Html) $ file $ global_options);
Cmd.v
(Cmd.info "makefile"
~doc:
"Generates a Makefile-compatible list of the file dependencies of a \
Catala program.")
Term.(const (handler `Makefile) $ file $ global_options);
Cmd.v
(Cmd.info "scopelang"
~doc:
"Prints a debugging verbatim of the scope language intermediate \
representation of the Catala program. Use the $(b,-s) option to \
restrict the output to a particular scope.")
Term.(const (handler `Scopelang) $ file $ global_options);
Cmd.v
(Cmd.info "dcalc"
~doc:
"Prints a debugging verbatim of the default calculus intermediate \
representation of the Catala program. Use the $(b,-s) option to \
restrict the output to a particular scope.")
Term.(const (handler `Dcalc) $ file $ global_options);
Cmd.v
(Cmd.info "lcalc"
~doc:
"Prints a debugging verbatim of the lambda calculus intermediate \
representation of the Catala program. Use the $(b,-s) option to \
restrict the output to a particular scope.")
Term.(const (handler `Lcalc) $ file $ global_options);
Cmd.v
(Cmd.info "scalc"
~doc:
"Prints a debugging verbatim of the statement calculus intermediate \
representation of the Catala program. Use the $(b,-s) option to \
restrict the output to a particular scope.")
Term.(const (handler `Scalc) $ file $ global_options);
Cmd.v
(Cmd.info "exceptions"
~doc:
"Prints the exception tree for the definitions of a particular \
variable, for debugging purposes. Use the $(b,-s) option to select \
the scope and the $(b,-v) option to select the variable. Use \
foo.bar to access state bar of variable foo or variable bar of \
subscope foo.")
Term.(const (handler `Exceptions) $ file $ global_options);
Cmd.v
(Cmd.info "pygmentize"
~doc:
"This special command is a wrapper around the $(b,pygmentize) \
command that enables support for colorising Catala code.")
Term.(const (fun _ -> assert false) $ file);
]
let version = "0.8.0"
let info =
@ -395,67 +455,6 @@ let info =
`P
"Catala is a domain-specific language for deriving \
faithful-by-construction algorithms from legislative texts.";
`S Manpage.s_commands;
`I
( "$(b,Intepret)",
"Runs the interpreter on the Catala program, executing the scope \
specified by the $(b,-s) option assuming no additional external \
inputs." );
`I
( "$(b,Intepret_Lcalc)",
"Runs the interpreter on the lcalc pass on the Catala program, \
executing the scope specified by the $(b,-s) option assuming no \
additional external inputs." );
`I
( "$(b,Typecheck)",
"Parses and typechecks a Catala program, without interpreting it." );
`I
( "$(b,Proof)",
"Generates and proves verification conditions about the well-behaved \
execution of the Catala program." );
`I ("$(b,OCaml)", "Generates an OCaml translation of the Catala program.");
`I ("$(b,Python)", "Generates a Python translation of the Catala program.");
`I
( "$(b,LaTeX)",
"Weaves a LaTeX literate programming output of the Catala program." );
`I
( "$(b,HTML)",
"Weaves an HTML literate programming output of the Catala program." );
`I
( "$(b,Makefile)",
"Generates a Makefile-compatible list of the file dependencies of a \
Catala program." );
`I
( "$(b,Scopelang)",
"Prints a debugging verbatim of the scope language intermediate \
representation of the Catala program. Use the $(b,-s) option to \
restrict the output to a particular scope." );
`I
( "$(b,Dcalc)",
"Prints a debugging verbatim of the default calculus intermediate \
representation of the Catala program. Use the $(b,-s) option to \
restrict the output to a particular scope." );
`I
( "$(b,Lcalc)",
"Prints a debugging verbatim of the lambda calculus intermediate \
representation of the Catala program. Use the $(b,-s) option to \
restrict the output to a particular scope." );
`I
( "$(b,Scalc)",
"Prints a debugging verbatim of the statement calculus intermediate \
representation of the Catala program. Use the $(b,-s) option to \
restrict the output to a particular scope." );
`I
( "$(b,Exceptions)",
"Prints the exception tree for the definitions of a particular \
variable, for debugging purposes. Use the $(b,-s) option to select \
the scope and the $(b,-v) option to select the variable. Use \
foo.bar to access state bar of variable foo or variable bar of \
subscope foo." );
`I
( "$(b,pygmentize)",
"This special command is a wrapper around the $(b,pygmentize) \
command that enables support for colorising Catala code." );
`S Manpage.s_authors;
`P "The authors are listed by alphabetical order.";
`P "Nicolas Chataing <nicolas.chataing@ens.fr>";
@ -474,3 +473,5 @@ let info =
in
let exits = Cmd.Exit.defaults @ [Cmd.Exit.info ~doc:"on error." 1] in
Cmd.info "catala" ~version ~doc ~exits ~man
let catala_t ?(extra = []) handler = Cmd.group info (subcommands handler @ extra)

26
compiler/catala_utils/cli.mli
View File

@ -17,7 +17,7 @@
type backend_lang = En | Fr | Pl
type backend_option_builtin =
type backend_option =
[ `Latex
| `Makefile
| `Html
@ -33,8 +33,6 @@ type backend_option_builtin =
| `Exceptions
| `Proof ]
type 'a backend_option = [ backend_option_builtin | `Plugin of 'a ]
(** The usual auto/always/never option argument *)
type when_enum = Auto | Always | Never
@ -43,14 +41,6 @@ val languages : (string * backend_lang) list
val language_code : backend_lang -> string
(** Returns the lowercase two-letter language code *)
val backend_option_to_string : string backend_option -> string
(** [backend_option_to_string backend] returns the string representation of the
given [backend].*)
val backend_option_of_string : string -> string backend_option
(** [backend_option_of_string backend] returns the {!type:backend_option}
corresponding to the [backend] string. *)
(** {2 Configuration globals} *)
val source_files : string list ref
@ -95,20 +85,18 @@ val trace_opt : bool Cmdliner.Term.t
val check_invariants_opt : bool Cmdliner.Term.t
val wrap_weaved_output : bool Cmdliner.Term.t
val print_only_law : bool Cmdliner.Term.t
val backend : string Cmdliner.Term.t
val plugins_dirs : string list Cmdliner.Term.t
val language : string option Cmdliner.Term.t
val max_prec_digits_opt : int option Cmdliner.Term.t
val ex_scope : string option Cmdliner.Term.t
val output : string option Cmdliner.Term.t
type options = {
type global_options = {
debug : bool;
color : when_enum;
message_format : message_format_enum;
wrap_weaved_output : bool;
avoid_exceptions : bool;
backend : string;
plugins_dirs : string list;
language : string option;
max_prec_digits : int option;
@ -122,14 +110,18 @@ type options = {
output_file : string option;
closure_conversion : bool;
print_only_law : bool;
link_modules : string list;
}
(** {2 Command-line application} *)
val options : options Cmdliner.Term.t
val global_options : global_options Cmdliner.Term.t
val catala_t : (string -> options -> 'a) -> 'a Cmdliner.Term.t
val catala_t :
?extra:int Cmdliner.Cmd.t list ->
(backend_option -> string -> global_options -> int) ->
int Cmdliner.Cmd.t
(** Main entry point: [catala_t file options] *)
val set_option_globals : options -> unit
val set_option_globals : global_options -> unit
val version : string
val info : Cmdliner.Cmd.info

4
compiler/catala_web_interpreter.ml
View File

@ -10,14 +10,13 @@ let _ =
(scope : Js.js_string Js.t)
(language : Js.js_string Js.t)
(trace : bool) =
driver
driver `Interpret
(Contents (Js.to_string contents))
{
Cli.debug = false;
color = Never;
wrap_weaved_output = false;
avoid_exceptions = false;
backend = "Interpret";
plugins_dirs = [];
language = Some (Js.to_string language);
max_prec_digits = None;
@ -32,5 +31,6 @@ let _ =
ex_variable = None;
output_file = None;
print_only_law = false;
link_modules = [];
}
end)

46
compiler/dcalc/from_scopelang.ml
View File

@ -57,7 +57,6 @@ type 'm ctx = {
subscope_vars :
('m Ast.expr Var.t * naked_typ * Desugared.Ast.io) ScopeVar.Map.t
SubScopeName.Map.t;
local_vars : ('m Scopelang.Ast.expr, 'm Ast.expr Var.t) Var.Map.t;
date_rounding : date_rounding;
}
@ -202,22 +201,6 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Scopelang.Ast.expr) :
'm Ast.expr boxed =
let m = Mark.get e in
match Mark.remove e with
| EVar v -> Expr.evar (Var.Map.find v ctx.local_vars) m
| ELit
((LBool _ | LInt _ | LRat _ | LMoney _ | LUnit | LDate _ | LDuration _) as
l) ->
Expr.elit l m
| EStruct { name; fields } ->
let fields = StructField.Map.map (translate_expr ctx) fields in
Expr.estruct name fields m
| EStructAccess { e; field; name } ->
Expr.estructaccess (translate_expr ctx e) field name m
| ETuple es -> Expr.etuple (List.map (translate_expr ctx) es) m
| ETupleAccess { e; index; size } ->
Expr.etupleaccess (translate_expr ctx e) index size m
| EInj { e; cons; name } ->
let e' = translate_expr ctx e in
Expr.einj e' cons name m
| EMatch { e = e1; name; cases = e_cases } ->
let enum_sig = EnumName.Map.find name ctx.enums in
let d_cases, remaining_e_cases =
@ -534,23 +517,6 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Scopelang.Ast.expr) :
EndCall m
in
new_e
| EAbs { binder; tys } ->
let xs, body = Bindlib.unmbind binder in
let new_xs = Array.map (fun x -> Var.make (Bindlib.name_of x)) xs in
let both_xs = Array.map2 (fun x new_x -> x, new_x) xs new_xs in
let body =
translate_expr
{
ctx with
local_vars =
Array.fold_left
(fun local_vars (x, new_x) -> Var.Map.add x new_x local_vars)
ctx.local_vars both_xs;
}
body
in
let binder = Expr.bind new_xs body in
Expr.eabs binder tys m
| EDefault { excepts; just; cons } ->
let excepts = collapse_similar_outcomes excepts in
Expr.edefault
@ -582,16 +548,13 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Scopelang.Ast.expr) :
| ELocation (ToplevelVar v) ->
let v, _ = TopdefName.Map.find (Mark.remove v) ctx.toplevel_vars in
Expr.evar v m
| EIfThenElse { cond; etrue; efalse } ->
Expr.eifthenelse (translate_expr ctx cond) (translate_expr ctx etrue)
(translate_expr ctx efalse)
m
| EOp { op = Add_dat_dur _; tys } ->
Expr.eop (Add_dat_dur ctx.date_rounding) tys m
| EOp { op; tys } -> Expr.eop (Operator.translate op) tys m
| EEmptyError -> Expr.eemptyerror m
| EErrorOnEmpty e' -> Expr.eerroronempty (translate_expr ctx e') m
| EArray es -> Expr.earray (List.map (translate_expr ctx) es) m
| ( EVar _ | EAbs _ | ELit _ | EExternal _ | EStruct _ | EStructAccess _
| ETuple _ | ETupleAccess _ | EInj _ | EEmptyError | EErrorOnEmpty _
| EArray _ | EIfThenElse _ ) as e ->
Expr.map ~f:(translate_expr ctx) (e, m)
(** The result of a rule translation is a list of assignment, with variables and
expressions. We also return the new translation context available after the
@ -1123,7 +1086,6 @@ let translate_program (prgm : 'm Scopelang.Ast.program) : 'm Ast.program =
scopes_parameters = sctx;
scope_vars = ScopeVar.Map.empty;
subscope_vars = SubScopeName.Map.empty;
local_vars = Var.Map.empty;
toplevel_vars;
date_rounding = AbortOnRound;
}

6
compiler/desugared/ast.ml
View File

@ -224,7 +224,7 @@ type scope = {
type program = {
program_scopes : scope ScopeName.Map.t;
program_topdefs : (expr * typ) TopdefName.Map.t;
program_topdefs : (expr option * typ) TopdefName.Map.t;
program_ctx : decl_ctx;
}
@ -291,4 +291,6 @@ let fold_exprs ~(f : 'a -> expr -> 'a) ~(init : 'a) (p : program) : 'a =
acc)
p.program_scopes init
in
TopdefName.Map.fold (fun _ (e, _) acc -> f acc e) p.program_topdefs acc
TopdefName.Map.fold
(fun _ (e, _) acc -> Option.fold ~none:acc ~some:(f acc) e)
p.program_topdefs acc

2
compiler/desugared/ast.mli
View File

@ -114,7 +114,7 @@ type scope = {
type program = {
program_scopes : scope ScopeName.Map.t;
program_topdefs : (expr * typ) TopdefName.Map.t;
program_topdefs : (expr option * typ) TopdefName.Map.t;
program_ctx : decl_ctx;
}

5
compiler/desugared/disambiguate.ml
View File

@ -70,7 +70,10 @@ let program prg =
in
let program_topdefs =
TopdefName.Map.map
(fun (e, ty) -> Expr.unbox (expr prg.program_ctx env (Expr.box e)), ty)
(function
| Some e, ty ->
Some (Expr.unbox (expr prg.program_ctx env (Expr.box e))), ty
| None, ty -> None, ty)
prg.program_topdefs
in
let env =

110
compiler/desugared/from_surface.ml
View File

@ -132,7 +132,7 @@ let disambiguate_constructor
"The deep pattern matching syntactic sugar is not yet supported"
in
let possible_c_uids =
try IdentName.Map.find (Mark.remove constructor) ctxt.constructor_idmap
try Ident.Map.find (Mark.remove constructor) ctxt.constructor_idmap
with Not_found ->
Message.raise_spanned_error (Mark.get constructor)
"The name of this constructor has not been defined before, maybe it is \
@ -198,7 +198,7 @@ let rec translate_expr
(expr : Surface.Ast.expression) : Ast.expr boxed =
let scope_vars =
match scope with
| None -> IdentName.Map.empty
| None -> Ident.Map.empty
| Some s -> (ScopeName.Map.find s ctxt.scopes).var_idmap
in
let rec_helper = translate_expr scope inside_definition_of ctxt in
@ -302,12 +302,12 @@ let rec translate_expr
| Ident ([], (x, pos)) -> (
(* first we check whether this is a local var, then we resort to scope-wide
variables, then global variables *)
match IdentName.Map.find_opt x ctxt.local_var_idmap with
match Ident.Map.find_opt x ctxt.local_var_idmap with
| Some uid ->
Expr.make_var uid emark
(* the whole box thing is to accomodate for this case *)
| None -> (
match IdentName.Map.find_opt x scope_vars with
match Ident.Map.find_opt x scope_vars with
| Some (ScopeVar uid) ->
(* If the referenced variable has states, then here are the rules to
desambiguate. In general, only the last state can be referenced.
@ -352,7 +352,7 @@ let rec translate_expr
(* Note: allowing access to a global variable with the same name as a
subscope is disputable, but I see no good reason to forbid it either *)
| None -> (
match IdentName.Map.find_opt x ctxt.topdefs with
match Ident.Map.find_opt x ctxt.topdefs with
| Some v ->
Expr.elocation
(ToplevelVar (v, Mark.get (TopdefName.get_info v)))
@ -360,8 +360,9 @@ let rec translate_expr
| None ->
Name_resolution.raise_unknown_identifier
"for a local, scope-wide or global variable" (x, pos))))
| Ident (_path, _x) ->
Message.raise_spanned_error pos "Qualified paths are not supported yet"
| Surface.Ast.Ident (path, x) ->
let path = List.map Mark.remove path in
Expr.eexternal (path, Mark.remove x) emark
| Dotted (e, ((path, x), _ppos)) -> (
match path, Mark.remove e with
| [], Ident ([], (y, _))
@ -369,7 +370,7 @@ let rec translate_expr
Name_resolution.is_subscope_uid s ctxt y) ->
(* In this case, y.x is a subscope variable *)
let subscope_uid, subscope_real_uid =
match IdentName.Map.find y scope_vars with
match Ident.Map.find y scope_vars with
| SubScope (sub, sc) -> sub, sc
| ScopeVar _ -> assert false
in
@ -409,7 +410,7 @@ let rec translate_expr
(fun acc (fld_id, e) ->
let var =
match
IdentName.Map.find_opt (Mark.remove fld_id) scope_def.var_idmap
Ident.Map.find_opt (Mark.remove fld_id) scope_def.var_idmap
with
| Some (ScopeVar v) -> v
| Some (SubScope _) | None ->
@ -449,7 +450,7 @@ let rec translate_expr
Expr.eapp fn [rec_helper e1] emark
| StructLit ((([], s_name), _), fields) ->
let s_uid =
match IdentName.Map.find_opt (Mark.remove s_name) ctxt.typedefs with
match Ident.Map.find_opt (Mark.remove s_name) ctxt.typedefs with
| Some (Name_resolution.TStruct s_uid) -> s_uid
| _ ->
Message.raise_spanned_error (Mark.get s_name)
@ -462,7 +463,7 @@ let rec translate_expr
let f_uid =
try
StructName.Map.find s_uid
(IdentName.Map.find (Mark.remove f_name) ctxt.field_idmap)
(Ident.Map.find (Mark.remove f_name) ctxt.field_idmap)
with Not_found ->
Message.raise_spanned_error (Mark.get f_name)
"This identifier should refer to a field of struct %s"
@ -492,7 +493,7 @@ let rec translate_expr
Message.raise_spanned_error pos "Qualified paths are not supported yet"
| EnumInject (((path, (constructor, pos_constructor)), _), payload) -> (
let possible_c_uids =
try IdentName.Map.find constructor ctxt.constructor_idmap
try Ident.Map.find constructor ctxt.constructor_idmap
with Not_found ->
Message.raise_spanned_error pos_constructor
"The name of this constructor has not been defined before, maybe it \
@ -1028,7 +1029,7 @@ let process_def
match def.definition_label with
| Some (label_str, label_pos) ->
Ast.ExplicitlyLabeled
(IdentName.Map.find label_str scope_def_ctxt.label_idmap, label_pos)
(Ident.Map.find label_str scope_def_ctxt.label_idmap, label_pos)
| None -> Ast.Unlabeled
in
let exception_situation =
@ -1045,8 +1046,7 @@ let process_def
| ExceptionToLabel label_str -> (
try
let label_id =
IdentName.Map.find (Mark.remove label_str)
scope_def_ctxt.label_idmap
Ident.Map.find (Mark.remove label_str) scope_def_ctxt.label_idmap
in
ExceptionToLabel (label_id, Mark.get label_str)
with Not_found ->
@ -1248,17 +1248,16 @@ let process_topdef
(prgm : Ast.program)
(def : S.top_def) : Ast.program =
let id =
IdentName.Map.find
(Mark.remove def.S.topdef_name)
ctxt.Name_resolution.topdefs
Ident.Map.find (Mark.remove def.S.topdef_name) ctxt.Name_resolution.topdefs
in
let translate_typ t = Name_resolution.process_type ctxt t in
let translate_tbase (tbase, m) = translate_typ (Base tbase, m) in
let typ = translate_typ def.S.topdef_type in
let expr =
match def.S.topdef_args with
| None -> translate_expr None None ctxt def.S.topdef_expr
| Some (args, _) ->
let expr_opt =
match def.S.topdef_expr, def.S.topdef_args with
| None, _ -> None
| Some e, None -> Some (Expr.unbox_closed (translate_expr None None ctxt e))
| Some e, Some (args, _) ->
let ctxt, args_tys =
List.fold_left_map
(fun ctxt ((lbl, pos), ty) ->
@ -1266,19 +1265,38 @@ let process_topdef
ctxt, ((v, pos), ty))
ctxt args
in
let body = translate_expr None None ctxt def.S.topdef_expr in
let body = translate_expr None None ctxt e in
let args, tys = List.split args_tys in
Expr.make_abs
(Array.of_list (List.map Mark.remove args))
body
(List.map translate_tbase tys)
(Mark.get def.S.topdef_name)
let e =
Expr.make_abs
(Array.of_list (List.map Mark.remove args))
body
(List.map translate_tbase tys)
(Mark.get def.S.topdef_name)
in
Some (Expr.unbox_closed e)
in
{
prgm with
Ast.program_topdefs =
TopdefName.Map.add id (Expr.unbox expr, typ) prgm.Ast.program_topdefs;
}
let program_topdefs =
TopdefName.Map.update id
(fun def0 ->
match def0, expr_opt with
| None, eopt -> Some (eopt, typ)
| Some (eopt0, ty0), eopt -> (
let err msg =
Message.raise_multispanned_error
[None, Mark.get ty0; None, Mark.get typ]
(msg ^^ " for %a") TopdefName.format_t id
in
if not (Type.equal ty0 typ) then err "Conflicting type definitions"
else
match eopt0, eopt with
| None, None -> err "Multiple declarations"
| Some _, Some _ -> err "Multiple definitions"
| Some e, None -> Some (Some e, typ)
| None, Some e -> Some (Some e, ty0)))
prgm.Ast.program_topdefs
in
{ prgm with Ast.program_topdefs }
let attribute_to_io (attr : Surface.Ast.scope_decl_context_io) : Ast.io =
{
@ -1295,7 +1313,7 @@ let attribute_to_io (attr : Surface.Ast.scope_decl_context_io) : Ast.io =
let init_scope_defs
(ctxt : Name_resolution.context)
(scope_idmap : Name_resolution.scope_var_or_subscope IdentName.Map.t) :
(scope_idmap : Name_resolution.scope_var_or_subscope Ident.Map.t) :
Ast.scope_def Ast.ScopeDef.Map.t =
(* Initializing the definitions of all scopes and subscope vars, with no rules
yet inside *)
@ -1351,7 +1369,7 @@ let init_scope_defs
let sub_scope_def =
ScopeName.Map.find subscope_uid ctxt.Name_resolution.scopes
in
IdentName.Map.fold
Ident.Map.fold
(fun _ v scope_def_map ->
match v with
| Name_resolution.SubScope _ -> scope_def_map
@ -1373,7 +1391,7 @@ let init_scope_defs
scope_def_map)
sub_scope_def.Name_resolution.var_idmap scope_def_map
in
IdentName.Map.fold add_def scope_idmap Ast.ScopeDef.Map.empty
Ident.Map.fold add_def scope_idmap Ast.ScopeDef.Map.empty
(** Main function of this module *)
let translate_program
@ -1384,7 +1402,7 @@ let translate_program
ScopeName.Map.mapi
(fun s_uid s_context ->
let scope_vars =
IdentName.Map.fold
Ident.Map.fold
(fun _ v acc ->
match v with
| Name_resolution.SubScope _ -> acc
@ -1396,7 +1414,7 @@ let translate_program
s_context.Name_resolution.var_idmap ScopeVar.Map.empty
in
let scope_sub_scopes =
IdentName.Map.fold
Ident.Map.fold
(fun _ v acc ->
match v with
| Name_resolution.ScopeVar _ -> acc
@ -1415,13 +1433,14 @@ let translate_program
})
ctxt.Name_resolution.scopes
in
let translate_type t = Name_resolution.process_type ctxt t in
{
Ast.program_ctx =
{
ctx_structs = ctxt.Name_resolution.structs;
ctx_enums = ctxt.Name_resolution.enums;
ctx_scopes =
IdentName.Map.fold
Ident.Map.fold
(fun _ def acc ->
match def with
| Name_resolution.TScope (scope, scope_out_struct) ->
@ -1429,6 +1448,19 @@ let translate_program
| _ -> acc)
ctxt.Name_resolution.typedefs ScopeName.Map.empty;
ctx_struct_fields = ctxt.Name_resolution.field_idmap;
ctx_modules =
List.fold_left
(fun map (path, def) ->
match def with
| Surface.Ast.Topdef { topdef_name; topdef_type; _ }, _pos ->
Qident.Map.add
(path, Mark.remove topdef_name)
(translate_type topdef_type)
map
| (ScopeDecl _ | StructDecl _ | EnumDecl _), _ (* as e *) ->
map (* assert false (\* TODO *\) *)
| ScopeUse _, _ -> assert false)
Qident.Map.empty prgm.Surface.Ast.program_interfaces;
};
Ast.program_topdefs = TopdefName.Map.empty;
Ast.program_scopes;

2
compiler/desugared/linting.ml
View File

@ -109,7 +109,7 @@ let detect_unused_struct_fields (p : program) : unit =
| EDStructAccess { name_opt = Some name; e = e_struct; field } ->
let field =
StructName.Map.find name
(IdentName.Map.find field p.program_ctx.ctx_struct_fields)
(Ident.Map.find field p.program_ctx.ctx_struct_fields)
in
StructField.Set.add field
(structs_fields_used_expr e_struct struct_fields_used)

117
compiler/desugared/name_resolution.ml
View File

@ -27,7 +27,7 @@ type unique_rulename = Ambiguous of Pos.t list | Unique of RuleName.t Mark.pos
type scope_def_context = {
default_exception_rulename : unique_rulename option;
label_idmap : LabelName.t IdentName.Map.t;
label_idmap : LabelName.t Ident.Map.t;
}
type scope_var_or_subscope =
@ -35,7 +35,7 @@ type scope_var_or_subscope =
| SubScope of SubScopeName.t * ScopeName.t
type scope_context = {
var_idmap : scope_var_or_subscope IdentName.Map.t;
var_idmap : scope_var_or_subscope Ident.Map.t;
(** All variables, including scope variables and subscopes *)
scope_defs_contexts : scope_def_context Ast.ScopeDef.Map.t;
(** What is the default rule to refer to for unnamed exceptions, if any *)
@ -56,7 +56,7 @@ type var_sig = {
var_sig_parameters :
(Uid.MarkedString.info * Shared_ast.typ) list Mark.pos option;
var_sig_io : Surface.Ast.scope_decl_context_io;
var_sig_states_idmap : StateName.t IdentName.Map.t;
var_sig_states_idmap : StateName.t Ident.Map.t;
var_sig_states_list : StateName.t list;
}
@ -69,19 +69,19 @@ type typedef =
(** Implicitly defined output struct *)
type context = {
local_var_idmap : Ast.expr Var.t IdentName.Map.t;
local_var_idmap : Ast.expr Var.t Ident.Map.t;
(** Inside a definition, local variables can be introduced by functions
arguments or pattern matching *)
typedefs : typedef IdentName.Map.t;
typedefs : typedef Ident.Map.t;
(** Gathers the names of the scopes, structs and enums *)
field_idmap : StructField.t StructName.Map.t IdentName.Map.t;
field_idmap : StructField.t StructName.Map.t Ident.Map.t;
(** The names of the struct fields. Names of fields can be shared between
different structs *)
constructor_idmap : EnumConstructor.t EnumName.Map.t IdentName.Map.t;
constructor_idmap : EnumConstructor.t EnumName.Map.t Ident.Map.t;
(** The names of the enum constructors. Constructor names can be shared
between different enums *)
scopes : scope_context ScopeName.Map.t; (** For each scope, its context *)
topdefs : TopdefName.t IdentName.Map.t; (** Global definitions *)
topdefs : TopdefName.t Ident.Map.t; (** Global definitions *)
structs : struct_context StructName.Map.t;
(** For each struct, its context *)
enums : enum_context EnumName.Map.t; (** For each enum, its context *)
@ -99,7 +99,7 @@ let raise_unsupported_feature (msg : string) (pos : Pos.t) =
(** Function to call whenever an identifier used somewhere has not been declared
in the program previously *)
let raise_unknown_identifier (msg : string) (ident : IdentName.t Mark.pos) =
let raise_unknown_identifier (msg : string) (ident : Ident.t Mark.pos) =
Message.raise_spanned_error (Mark.get ident)
"@{<yellow>\"%s\"@}: unknown identifier %s" (Mark.remove ident) msg
@ -118,9 +118,9 @@ let get_var_io (ctxt : context) (uid : ScopeVar.t) :
let get_var_uid
(scope_uid : ScopeName.t)
(ctxt : context)
((x, pos) : IdentName.t Mark.pos) : ScopeVar.t =
((x, pos) : Ident.t Mark.pos) : ScopeVar.t =
let scope = ScopeName.Map.find scope_uid ctxt.scopes in
match IdentName.Map.find_opt x scope.var_idmap with
match Ident.Map.find_opt x scope.var_idmap with
| Some (ScopeVar uid) -> uid
| _ ->
raise_unknown_identifier
@ -131,18 +131,18 @@ let get_var_uid
let get_subscope_uid
(scope_uid : ScopeName.t)
(ctxt : context)
((y, pos) : IdentName.t Mark.pos) : SubScopeName.t =
((y, pos) : Ident.t Mark.pos) : SubScopeName.t =
let scope = ScopeName.Map.find scope_uid ctxt.scopes in
match IdentName.Map.find_opt y scope.var_idmap with
match Ident.Map.find_opt y scope.var_idmap with
| Some (SubScope (sub_uid, _sub_id)) -> sub_uid
| _ -> raise_unknown_identifier "for a subscope of this scope" (y, pos)
(** [is_subscope_uid scope_uid ctxt y] returns true if [y] belongs to the
subscopes of [scope_uid]. *)
let is_subscope_uid (scope_uid : ScopeName.t) (ctxt : context) (y : IdentName.t)
: bool =
let is_subscope_uid (scope_uid : ScopeName.t) (ctxt : context) (y : Ident.t) :
bool =
let scope = ScopeName.Map.find scope_uid ctxt.scopes in
match IdentName.Map.find_opt y scope.var_idmap with
match Ident.Map.find_opt y scope.var_idmap with
| Some (SubScope _) -> true
| _ -> false
@ -150,7 +150,7 @@ let is_subscope_uid (scope_uid : ScopeName.t) (ctxt : context) (y : IdentName.t)
let belongs_to (ctxt : context) (uid : ScopeVar.t) (scope_uid : ScopeName.t) :
bool =
let scope = ScopeName.Map.find scope_uid ctxt.scopes in
IdentName.Map.exists
Ident.Map.exists
(fun _ -> function
| ScopeVar var_uid -> ScopeVar.equal uid var_uid
| _ -> false)
@ -184,7 +184,7 @@ let is_def_cond (ctxt : context) (def : Ast.ScopeDef.t) : bool =
is_var_cond ctxt x
let get_enum ctxt id =
match IdentName.Map.find (Mark.remove id) ctxt.typedefs with
match Ident.Map.find (Mark.remove id) ctxt.typedefs with
| TEnum id -> id
| TStruct sid ->
Message.raise_multispanned_error
@ -205,7 +205,7 @@ let get_enum ctxt id =
(Mark.remove id)
let get_struct ctxt id =
match IdentName.Map.find (Mark.remove id) ctxt.typedefs with
match Ident.Map.find (Mark.remove id) ctxt.typedefs with
| TStruct id | TScope (_, { out_struct_name = id; _ }) -> id
| TEnum eid ->
Message.raise_multispanned_error
@ -219,7 +219,7 @@ let get_struct ctxt id =
(Mark.remove id)
let get_scope ctxt id =
match IdentName.Map.find (Mark.remove id) ctxt.typedefs with
match Ident.Map.find (Mark.remove id) ctxt.typedefs with
| TScope (id, _) -> id
| TEnum eid ->
Message.raise_multispanned_error
@ -249,7 +249,7 @@ let process_subscope_decl
let name, name_pos = decl.scope_decl_context_scope_name in
let subscope, s_pos = decl.scope_decl_context_scope_sub_scope in
let scope_ctxt = ScopeName.Map.find scope ctxt.scopes in
match IdentName.Map.find_opt subscope scope_ctxt.var_idmap with
match Ident.Map.find_opt subscope scope_ctxt.var_idmap with
| Some use ->
let info =
match use with
@ -268,7 +268,7 @@ let process_subscope_decl
{
scope_ctxt with
var_idmap =
IdentName.Map.add name
Ident.Map.add name
(SubScope (sub_scope_uid, original_subscope_uid))
scope_ctxt.var_idmap;
sub_scopes =
@ -304,7 +304,7 @@ let rec process_base_typ
| Surface.Ast.Boolean -> TLit TBool, typ_pos
| Surface.Ast.Text -> raise_unsupported_feature "text type" typ_pos
| Surface.Ast.Named ([], (ident, _pos)) -> (
match IdentName.Map.find_opt ident ctxt.typedefs with
match Ident.Map.find_opt ident ctxt.typedefs with
| Some (TStruct s_uid) -> TStruct s_uid, typ_pos
| Some (TEnum e_uid) -> TEnum e_uid, typ_pos
| Some (TScope (_, scope_str)) ->
@ -337,7 +337,7 @@ let process_data_decl
let is_cond = is_type_cond decl.scope_decl_context_item_typ in
let name, pos = decl.scope_decl_context_item_name in
let scope_ctxt = ScopeName.Map.find scope ctxt.scopes in
match IdentName.Map.find_opt name scope_ctxt.var_idmap with
match Ident.Map.find_opt name scope_ctxt.var_idmap with
| Some use ->
let info =
match use with
@ -352,15 +352,14 @@ let process_data_decl
let scope_ctxt =
{
scope_ctxt with
var_idmap = IdentName.Map.add name (ScopeVar uid) scope_ctxt.var_idmap;
var_idmap = Ident.Map.add name (ScopeVar uid) scope_ctxt.var_idmap;
}
in
let states_idmap, states_list =
List.fold_right
(fun state_id
((states_idmap : StateName.t IdentName.Map.t), states_list) ->
(fun state_id ((states_idmap : StateName.t Ident.Map.t), states_list) ->
let state_id_name = Mark.remove state_id in
if IdentName.Map.mem state_id_name states_idmap then
if Ident.Map.mem state_id_name states_idmap then
Message.raise_multispanned_error_full
[
( Some
@ -375,15 +374,15 @@ let process_data_decl
"Second instance of state @{<yellow>\"%s\"@}:"
state_id_name),
Mark.get
(IdentName.Map.find state_id_name states_idmap
(Ident.Map.find state_id_name states_idmap
|> StateName.get_info) );
]
"There are two states with the same name for the same variable: \
this is ambiguous. Please change the name of either states.";
let state_uid = StateName.fresh state_id in
( IdentName.Map.add state_id_name state_uid states_idmap,
( Ident.Map.add state_id_name state_uid states_idmap,
state_uid :: states_list ))
decl.scope_decl_context_item_states (IdentName.Map.empty, [])
decl.scope_decl_context_item_states (Ident.Map.empty, [])
in
let var_sig_parameters =
Option.map
@ -407,14 +406,13 @@ let process_data_decl
}
(** Adds a binding to the context *)
let add_def_local_var (ctxt : context) (name : IdentName.t) :
let add_def_local_var (ctxt : context) (name : Ident.t) :
context * Ast.expr Var.t =
let local_var_uid = Var.make name in
let ctxt =
{
ctxt with
local_var_idmap =
IdentName.Map.add name local_var_uid ctxt.local_var_idmap;
local_var_idmap = Ident.Map.add name local_var_uid ctxt.local_var_idmap;
}
in
ctxt, local_var_uid
@ -436,7 +434,7 @@ let process_struct_decl (ctxt : context) (sdecl : Surface.Ast.struct_decl) :
{
ctxt with
field_idmap =
IdentName.Map.update
Ident.Map.update
(Mark.remove fdecl.Surface.Ast.struct_decl_field_name)
(fun uids ->
match uids with
@ -481,7 +479,7 @@ let process_enum_decl (ctxt : context) (edecl : Surface.Ast.enum_decl) : context
{
ctxt with
constructor_idmap =
IdentName.Map.update
Ident.Map.update
(Mark.remove cdecl.Surface.Ast.enum_decl_case_name)
(fun uids ->
match uids with
@ -569,21 +567,21 @@ let process_scope_decl (ctxt : context) (decl : Surface.Ast.scope_decl) :
let out_struct_fields =
let sco = ScopeName.Map.find scope_uid ctxt.scopes in
let str = get_struct ctxt decl.scope_decl_name in
IdentName.Map.fold
Ident.Map.fold
(fun id var svmap ->
match var with
| SubScope _ -> svmap
| ScopeVar v -> (
try
let field =
StructName.Map.find str (IdentName.Map.find id ctxt.field_idmap)
StructName.Map.find str (Ident.Map.find id ctxt.field_idmap)
in
ScopeVar.Map.add v field svmap
with Not_found -> svmap))
sco.var_idmap ScopeVar.Map.empty
in
let typedefs =
IdentName.Map.update
Ident.Map.update
(Mark.remove decl.scope_decl_name)
(function
| Some (TScope (scope, { out_struct_name; _ })) ->
@ -617,13 +615,13 @@ let process_name_item (ctxt : context) (item : Surface.Ast.code_item Mark.pos) :
Option.iter
(fun use ->
raise_already_defined_error (typedef_info use) name pos "scope")
(IdentName.Map.find_opt name ctxt.typedefs);
(Ident.Map.find_opt name ctxt.typedefs);
let scope_uid = ScopeName.fresh (name, pos) in
let out_struct_uid = StructName.fresh (name, pos) in
{
ctxt with
typedefs =
IdentName.Map.add name
Ident.Map.add name
(TScope
( scope_uid,
{
@ -634,7 +632,7 @@ let process_name_item (ctxt : context) (item : Surface.Ast.code_item Mark.pos) :
scopes =
ScopeName.Map.add scope_uid
{
var_idmap = IdentName.Map.empty;
var_idmap = Ident.Map.empty;
scope_defs_contexts = Ast.ScopeDef.Map.empty;
sub_scopes = ScopeName.Set.empty;
}
@ -645,12 +643,12 @@ let process_name_item (ctxt : context) (item : Surface.Ast.code_item Mark.pos) :
Option.iter
(fun use ->
raise_already_defined_error (typedef_info use) name pos "struct")
(IdentName.Map.find_opt name ctxt.typedefs);
(Ident.Map.find_opt name ctxt.typedefs);
let s_uid = StructName.fresh sdecl.struct_decl_name in
{
ctxt with
typedefs =
IdentName.Map.add
Ident.Map.add
(Mark.remove sdecl.struct_decl_name)
(TStruct s_uid) ctxt.typedefs;
}
@ -659,12 +657,12 @@ let process_name_item (ctxt : context) (item : Surface.Ast.code_item Mark.pos) :
Option.iter
(fun use ->
raise_already_defined_error (typedef_info use) name pos "enum")
(IdentName.Map.find_opt name ctxt.typedefs);
(Ident.Map.find_opt name ctxt.typedefs);
let e_uid = EnumName.fresh edecl.enum_decl_name in
{
ctxt with
typedefs =
IdentName.Map.add
Ident.Map.add
(Mark.remove edecl.enum_decl_name)
(TEnum e_uid) ctxt.typedefs;
}
@ -675,9 +673,9 @@ let process_name_item (ctxt : context) (item : Surface.Ast.code_item Mark.pos) :
(fun use ->
raise_already_defined_error (TopdefName.get_info use) name pos
"toplevel definition")
(IdentName.Map.find_opt name ctxt.topdefs);
(Ident.Map.find_opt name ctxt.topdefs);
let uid = TopdefName.fresh def.topdef_name in
{ ctxt with topdefs = IdentName.Map.add name uid ctxt.topdefs }
{ ctxt with topdefs = Ident.Map.add name uid ctxt.topdefs }
(** Process a code item that is a declaration *)
let process_decl_item (ctxt : context) (item : Surface.Ast.code_item Mark.pos) :
@ -731,8 +729,7 @@ let get_def_key
| Some state -> (
try
Some
(IdentName.Map.find (Mark.remove state)
var_sig.var_sig_states_idmap)
(Ident.Map.find (Mark.remove state) var_sig.var_sig_states_idmap)
with Not_found ->
Message.raise_multispanned_error
[
@ -742,7 +739,7 @@ let get_def_key
"This identifier is not a state declared for variable %a."
ScopeVar.format_t x_uid)
| None ->
if not (IdentName.Map.is_empty var_sig.var_sig_states_idmap) then
if not (Ident.Map.is_empty var_sig.var_sig_states_idmap) then
Message.raise_multispanned_error
[
None, Mark.get x;
@ -754,7 +751,7 @@ let get_def_key
else None )
| [y; x] ->
let (subscope_uid, subscope_real_uid) : SubScopeName.t * ScopeName.t =
match IdentName.Map.find_opt (Mark.remove y) scope_ctxt.var_idmap with
match Ident.Map.find_opt (Mark.remove y) scope_ctxt.var_idmap with
| Some (SubScope (v, u)) -> v, u
| Some _ ->
Message.raise_spanned_error pos
@ -782,7 +779,7 @@ let update_def_key_ctx
| None -> def_key_ctx
| Some label ->
let new_label_idmap =
IdentName.Map.update (Mark.remove label)
Ident.Map.update (Mark.remove label)
(fun existing_label ->
match existing_label with
| Some existing_label -> Some existing_label
@ -836,7 +833,7 @@ let empty_def_key_ctx =
(* Here, this is the first time we encounter a definition for this
definition key *)
default_exception_rulename = None;
label_idmap = IdentName.Map.empty;
label_idmap = Ident.Map.empty;
}
let process_definition
@ -885,7 +882,7 @@ let process_scope_use (ctxt : context) (suse : Surface.Ast.scope_use) : context
=
let s_name =
match
IdentName.Map.find_opt
Ident.Map.find_opt
(Mark.remove suse.Surface.Ast.scope_use_name)
ctxt.typedefs
with
@ -913,15 +910,15 @@ let process_use_item (ctxt : context) (item : Surface.Ast.code_item Mark.pos) :
let form_context (prgm : Surface.Ast.program) : context =
let empty_ctxt =
{
local_var_idmap = IdentName.Map.empty;
typedefs = IdentName.Map.empty;
local_var_idmap = Ident.Map.empty;
typedefs = Ident.Map.empty;
scopes = ScopeName.Map.empty;
topdefs = IdentName.Map.empty;
topdefs = Ident.Map.empty;
var_typs = ScopeVar.Map.empty;
structs = StructName.Map.empty;
field_idmap = IdentName.Map.empty;
field_idmap = Ident.Map.empty;
enums = EnumName.Map.empty;
constructor_idmap = IdentName.Map.empty;
constructor_idmap = Ident.Map.empty;
}
in
let ctxt =

33
compiler/desugared/name_resolution.mli
View File

@ -27,7 +27,7 @@ type unique_rulename = Ambiguous of Pos.t list | Unique of RuleName.t Mark.pos
type scope_def_context = {
default_exception_rulename : unique_rulename option;
label_idmap : LabelName.t IdentName.Map.t;
label_idmap : LabelName.t Ident.Map.t;
}
type scope_var_or_subscope =
@ -35,7 +35,7 @@ type scope_var_or_subscope =
| SubScope of SubScopeName.t * ScopeName.t
type scope_context = {
var_idmap : scope_var_or_subscope IdentName.Map.t;
var_idmap : scope_var_or_subscope Ident.Map.t;
(** All variables, including scope variables and subscopes *)
scope_defs_contexts : scope_def_context Ast.ScopeDef.Map.t;
(** What is the default rule to refer to for unnamed exceptions, if any *)
@ -56,7 +56,7 @@ type var_sig = {
var_sig_parameters :
(Uid.MarkedString.info * Shared_ast.typ) list Mark.pos option;
var_sig_io : Surface.Ast.scope_decl_context_io;
var_sig_states_idmap : StateName.t IdentName.Map.t;
var_sig_states_idmap : StateName.t Ident.Map.t;
var_sig_states_list : StateName.t list;
}
@ -69,19 +69,19 @@ type typedef =
(** Implicitly defined output struct *)
type context = {
local_var_idmap : Ast.expr Var.t IdentName.Map.t;
local_var_idmap : Ast.expr Var.t Ident.Map.t;
(** Inside a definition, local variables can be introduced by functions
arguments or pattern matching *)
typedefs : typedef IdentName.Map.t;
typedefs : typedef Ident.Map.t;
(** Gathers the names of the scopes, structs and enums *)
field_idmap : StructField.t StructName.Map.t IdentName.Map.t;
field_idmap : StructField.t StructName.Map.t Ident.Map.t;
(** The names of the struct fields. Names of fields can be shared between
different structs *)
constructor_idmap : EnumConstructor.t EnumName.Map.t IdentName.Map.t;
constructor_idmap : EnumConstructor.t EnumName.Map.t Ident.Map.t;
(** The names of the enum constructors. Constructor names can be shared
between different enums *)
scopes : scope_context ScopeName.Map.t; (** For each scope, its context *)
topdefs : TopdefName.t IdentName.Map.t; (** Global definitions *)
topdefs : TopdefName.t Ident.Map.t; (** Global definitions *)
structs : struct_context StructName.Map.t;
(** For each struct, its context *)
enums : enum_context EnumName.Map.t; (** For each enum, its context *)
@ -96,7 +96,7 @@ val raise_unsupported_feature : string -> Pos.t -> 'a
(** Temporary function raising an error message saying that a feature is not
supported yet *)
val raise_unknown_identifier : string -> IdentName.t Mark.pos -> 'a
val raise_unknown_identifier : string -> Ident.t Mark.pos -> 'a
(** Function to call whenever an identifier used somewhere has not been declared
in the program previously *)
@ -106,14 +106,14 @@ val get_var_typ : context -> ScopeVar.t -> typ
val is_var_cond : context -> ScopeVar.t -> bool
val get_var_io : context -> ScopeVar.t -> Surface.Ast.scope_decl_context_io
val get_var_uid : ScopeName.t -> context -> IdentName.t Mark.pos -> ScopeVar.t
val get_var_uid : ScopeName.t -> context -> Ident.t Mark.pos -> ScopeVar.t
(** Get the variable uid inside the scope given in argument *)
val get_subscope_uid :
ScopeName.t -> context -> IdentName.t Mark.pos -> SubScopeName.t
ScopeName.t -> context -> Ident.t Mark.pos -> SubScopeName.t
(** Get the subscope uid inside the scope given in argument *)
val is_subscope_uid : ScopeName.t -> context -> IdentName.t -> bool
val is_subscope_uid : ScopeName.t -> context -> Ident.t -> bool
(** [is_subscope_uid scope_uid ctxt y] returns true if [y] belongs to the
subscopes of [scope_uid]. *)
@ -131,7 +131,7 @@ val get_params :
val is_def_cond : context -> Ast.ScopeDef.t -> bool
val is_type_cond : Surface.Ast.typ -> bool
val add_def_local_var : context -> IdentName.t -> context * Ast.expr Var.t
val add_def_local_var : context -> Ident.t -> context * Ast.expr Var.t
(** Adds a binding to the context *)
val get_def_key :
@ -143,21 +143,20 @@ val get_def_key :
Ast.ScopeDef.t
(** Usage: [get_def_key var_name var_state scope_uid ctxt pos]*)
val get_enum : context -> IdentName.t Mark.pos -> EnumName.t
val get_enum : context -> Ident.t Mark.pos -> EnumName.t
(** Find an enum definition from the typedefs, failing if there is none or it
has a different kind *)
val get_struct : context -> IdentName.t Mark.pos -> StructName.t
val get_struct : context -> Ident.t Mark.pos -> StructName.t
(** Find a struct definition from the typedefs (possibly an implicit output
struct from a scope), failing if there is none or it has a different kind *)
val get_scope : context -> IdentName.t Mark.pos -> ScopeName.t
val get_scope : context -> Ident.t Mark.pos -> ScopeName.t
(** Find a scope definition from the typedefs, failing if there is none or it
has a different kind *)
val process_type : context -> Surface.Ast.typ -> typ
(** Convert a surface base type to an AST type *)
(* Note: should probably be moved to a different module *)
(** {1 API} *)

146
compiler/driver.ml
View File

@ -21,9 +21,11 @@ open Catala_utils
string representation. *)
let extensions = [".catala_fr", "fr"; ".catala_en", "en"; ".catala_pl", "pl"]
type backend = [ Cli.backend_option | `Plugin of Plugin.handler ]
let get_scope_uid
(options : Cli.options)
(backend : Plugin.t Cli.backend_option)
(options : Cli.global_options)
(backend : backend)
(ctxt : Desugared.Name_resolution.context) =
match options.ex_scope, backend with
| None, `Interpret ->
@ -31,26 +33,26 @@ let get_scope_uid
| None, _ ->
let _, scope =
try
Shared_ast.IdentName.Map.filter_map
Shared_ast.Ident.Map.filter_map
(fun _ -> function
| Desugared.Name_resolution.TScope (uid, _) -> Some uid
| _ -> None)
ctxt.typedefs
|> Shared_ast.IdentName.Map.choose
|> Shared_ast.Ident.Map.choose
with Not_found ->
Message.raise_error "There isn't any scope inside the program."
in
scope
| Some name, _ -> (
match Shared_ast.IdentName.Map.find_opt name ctxt.typedefs with
match Shared_ast.Ident.Map.find_opt name ctxt.typedefs with
| Some (Desugared.Name_resolution.TScope (uid, _)) -> uid
| _ ->
Message.raise_error
"There is no scope @{<yellow>\"%s\"@} inside the program." name)
let get_variable_uid
(options : Cli.options)
(backend : Plugin.t Cli.backend_option)
(options : Cli.global_options)
(backend : backend)
(ctxt : Desugared.Name_resolution.context)
(scope_uid : Shared_ast.ScopeName.t) =
match options.ex_variable, backend with
@ -75,7 +77,7 @@ let get_variable_uid
| Some groups -> Re.Group.get groups 1, Some (Re.Group.get groups 2)
in
match
Shared_ast.IdentName.Map.find_opt first_part
Shared_ast.Ident.Map.find_opt first_part
(Shared_ast.ScopeName.Map.find scope_uid ctxt.scopes).var_idmap
with
| None ->
@ -95,7 +97,7 @@ let get_variable_uid
Shared_ast.ScopeName.format_t scope_uid
| Some second_part -> (
match
Shared_ast.IdentName.Map.find_opt second_part
Shared_ast.Ident.Map.find_opt second_part
(Shared_ast.ScopeName.Map.find subscope_name ctxt.scopes).var_idmap
with
| Some (Desugared.Name_resolution.ScopeVar v) ->
@ -117,7 +119,7 @@ let get_variable_uid
(fun second_part ->
let var_sig = Shared_ast.ScopeVar.Map.find v ctxt.var_typs in
match
Shared_ast.IdentName.Map.find_opt second_part
Shared_ast.Ident.Map.find_opt second_part
var_sig.var_sig_states_idmap
with
| Some state -> state
@ -129,17 +131,14 @@ let get_variable_uid
scope_uid)
second_part )))
let modname_of_file f =
(* Fixme: make this more robust *)
String.capitalize_ascii Filename.(basename (remove_extension f))
(** Entry function for the executable. Returns a negative number in case of
error. Usage: [driver source_file options]*)
let driver source_file (options : Cli.options) : int =
let driver backend source_file (options : Cli.global_options) : int =
try
List.iter
(fun d ->
match Sys.is_directory d with
| true -> Plugin.load_dir d
| false -> ()
| exception Sys_error _ -> ())
options.plugins_dirs;
Cli.set_option_globals options;
if options.debug then Printexc.record_backtrace true;
Message.emit_debug "Reading files...";
@ -167,28 +166,23 @@ let driver source_file (options : Cli.options) : int =
"The selected language (%s) is not supported by Catala" l
in
Cli.locale_lang := language;
let backend = options.backend in
let backend =
match Cli.backend_option_of_string backend with
| #Cli.backend_option_builtin as backend -> backend
| `Plugin s -> (
try `Plugin (Plugin.find s)
with Not_found ->
Message.raise_error
"The selected backend (%s) is not supported by Catala, nor was a \
plugin by this name found under %a"
backend
(Format.pp_print_list
~pp_sep:(fun ppf () -> Format.fprintf ppf "@ or @ ")
(fun ppf dir ->
Format.pp_print_string ppf
(try Unix.readlink dir with _ -> dir)))
options.plugins_dirs)
in
let prgm =
Surface.Parser_driver.parse_top_level_file source_file language
in
let prgm = Surface.Fill_positions.fill_pos_with_legislative_info prgm in
let prgm =
List.fold_left
(fun prgm f ->
let lang =
Option.value ~default:language
@@ Option.bind
(List.assoc_opt (Filename.extension f) extensions)
(fun l -> List.assoc_opt l Cli.languages)
in
let modname = modname_of_file f in
Surface.Parser_driver.add_interface (FileName f) lang [modname] prgm)
prgm options.link_modules
in
let get_output ?ext =
File.get_out_channel ~source_file ~output_file:options.output_file ?ext
in
@ -373,6 +367,14 @@ let driver source_file (options : Cli.options) : int =
Verification.Solver.solve_vc prgm.decl_ctx vcs
| `Interpret ->
if options.link_modules <> [] then (
Message.emit_debug "Loading shared modules...";
List.iter
Dynlink.(
fun m ->
loadfile
(adapt_filename (Filename.remove_extension m ^ ".cmo")))
options.link_modules);
Message.emit_debug "Starting interpretation (dcalc)...";
let results =
Shared_ast.Interpreter.interpret_program_dcalc prgm scope_uid
@ -490,7 +492,13 @@ let driver source_file (options : Cli.options) : int =
Message.emit_debug "Compiling program into OCaml...";
Message.emit_debug "Writing to %s..."
(Option.value ~default:"stdout" output_file);
Lcalc.To_ocaml.format_program fmt prgm type_ordering
let modname =
match source_file with
(* FIXME: WIP placeholder *)
| FileName n -> Some (modname_of_file n)
| _ -> None
in
Lcalc.To_ocaml.format_program fmt ?modname prgm type_ordering
| `Plugin (Plugin.Dcalc _) -> assert false
| `Plugin (Plugin.Lcalc p) ->
let output_file, _ =
@ -561,15 +569,65 @@ let driver source_file (options : Cli.options) : int =
-1
let main () =
if
Array.length Sys.argv >= 2
&& String.lowercase_ascii Sys.argv.(1) = "pygmentize"
then Literate.Pygmentize.exec ();
let argv = Array.copy Sys.argv in
(* Our command names (first argument) are case-insensitive *)
if Array.length argv >= 2 then argv.(1) <- String.lowercase_ascii argv.(1);
(* Pygmentize is a specific exec subcommand that doesn't go through
cmdliner *)
if Array.length Sys.argv >= 2 && argv.(1) = "pygmentize" then
Literate.Pygmentize.exec ();
(* Peek to load plugins before the command-line is parsed proper *)
let plugins =
let plugins_dirs =
match
Cmdliner.Cmd.eval_peek_opts ~argv Cli.global_options ~version_opt:true
with
| Some opts, _ ->
Cli.set_option_globals opts;
(* Do this asap, for debug options, etc. *)
opts.Cli.plugins_dirs
| None, _ -> []
in
List.iter
(fun d ->
match Sys.is_directory d with
| true -> Plugin.load_dir d
| false -> ()
| exception Sys_error _ -> ())
plugins_dirs;
Plugin.list ()
in
let return_code =
Cmdliner.Cmd.eval'
(Cmdliner.Cmd.v Cli.info (Cli.catala_t (fun f -> driver (FileName f))))
Cmdliner.Cmd.eval' ~argv
(Cli.catala_t
(fun backend f -> driver backend (FileName f))
~extra:plugins)
in
exit return_code
(* Export module PluginAPI, hide parent module Plugin *)
module Plugin = Plugin.PluginAPI
module Plugin = struct
open Plugin
include PluginAPI
open Cmdliner
let register_cmd info plugin =
let term =
Term.(
const (fun file opts -> driver (`Plugin plugin) (FileName file) opts)
$ Cli.file
$ Cli.global_options)
in
register_generic info term
let info_name info = Cmd.name (Cmd.v info (Term.const ()))
let register_dcalc info ~extension apply =
register_cmd info (Dcalc { name = info_name info; extension; apply })
let register_lcalc info ~extension apply =
register_cmd info (Lcalc { name = info_name info; extension; apply })
let register_scalc info ~extension apply =
register_cmd info (Scalc { name = info_name info; extension; apply })
end

32
compiler/driver.mli
View File

@ -16,11 +16,39 @@
the License. *)
open Catala_utils
module Plugin = Plugin.PluginAPI
val driver : Pos.input_file -> Cli.options -> int
val driver :
[< Cli.backend_option | `Plugin of Plugin.handler ] ->
Pos.input_file ->
Cli.global_options ->
int
(** Entry function for the executable. Returns a negative number in case of
error. *)
val main : unit -> unit
(** Main program entry point, including command-line parsing and return code *)
module Plugin : sig
include module type of Plugin.PluginAPI
open Cmdliner
val register_generic : Cmd.info -> Cmd.Exit.code Term.t -> unit
val register_dcalc :
Cmd.info ->
extension:string ->
Shared_ast.untyped Dcalc.Ast.program plugin_apply_fun_typ ->
unit
val register_lcalc :
Cmd.info ->
extension:string ->
Shared_ast.untyped Lcalc.Ast.program plugin_apply_fun_typ ->
unit
val register_scalc :
Cmd.info ->
extension:string ->
Scalc.Ast.program plugin_apply_fun_typ ->
unit
end

6
compiler/lcalc/closure_conversion.ml
View File

@ -38,7 +38,8 @@ let rec hoist_context_free_closures :
let m = Mark.get e in
match Mark.remove e with
| EStruct _ | EStructAccess _ | ETuple _ | ETupleAccess _ | EInj _ | EArray _
| ELit _ | EAssert _ | EOp _ | EIfThenElse _ | ERaise _ | ECatch _ | EVar _ ->
| ELit _ | EAssert _ | EOp _ | EIfThenElse _ | ERaise _ | ECatch _ | EVar _
| EExternal _ ->
Expr.map_gather ~acc:[] ~join:( @ ) ~f:(hoist_context_free_closures ctx) e
| EMatch { e; cases; name } ->
let collected_closures, new_e = (hoist_context_free_closures ctx) e in
@ -98,7 +99,8 @@ let rec transform_closures_expr :
let m = Mark.get e in
match Mark.remove e with
| EStruct _ | EStructAccess _ | ETuple _ | ETupleAccess _ | EInj _ | EArray _
| ELit _ | EAssert _ | EOp _ | EIfThenElse _ | ERaise _ | ECatch _ ->
| ELit _ | EExternal _ | EAssert _ | EOp _ | EIfThenElse _ | ERaise _
| ECatch _ ->
Expr.map_gather ~acc:Var.Set.empty ~join:Var.Set.union
~f:(transform_closures_expr ctx)
e

6
compiler/lcalc/compile_with_exceptions.ml
View File

@ -74,9 +74,9 @@ and translate_expr (ctx : 'm ctx) (e : 'm D.expr) : 'm A.expr boxed =
| EDefault { excepts; just; cons } ->
translate_default ctx excepts just cons (Mark.get e)
| EOp { op; tys } -> Expr.eop (Operator.translate op) tys m
| ( ELit _ | EApp _ | EArray _ | EVar _ | EAbs _ | EIfThenElse _ | ETuple _
| ETupleAccess _ | EInj _ | EAssert _ | EStruct _ | EStructAccess _
| EMatch _ ) as e ->
| ( ELit _ | EApp _ | EArray _ | EVar _ | EExternal _ | EAbs _ | EIfThenElse _
| ETuple _ | ETupleAccess _ | EInj _ | EAssert _ | EStruct _
| EStructAccess _ | EMatch _ ) as e ->
Expr.map ~f:(translate_expr ctx) (Mark.add m e)
| _ -> .

1
compiler/lcalc/compile_without_exceptions.ml
View File

@ -107,6 +107,7 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) : (lcalc, typed) boxed_gexpr
if (Var.Map.find x ctx.ctx_vars).info_pure then
Ast.OptionMonad.return (Expr.evar (trans_var ctx x) m) ~mark
else Expr.evar (trans_var ctx x) m
| EExternal eref -> Expr.eexternal eref mark
| EApp { f = EVar v, _; args = [(ELit LUnit, _)] } ->
(* Invariant: as users cannot write thunks, it can only come from prior
compilation passes. Hence we can safely remove those. *)

74
compiler/lcalc/to_ocaml.ml
View File

@ -87,6 +87,8 @@ let avoid_keywords (s : string) : string =
| "while" | "with" | "Stdlib" | "Runtime" | "Oper" ->
s ^ "_user"
| _ -> s
(* Fixme: this could cause clashes if the user program contains both e.g. [new]
and [new_user] *)
let format_struct_name (fmt : Format.formatter) (v : StructName.t) : unit =
Format.asprintf "%a" StructName.format_t v
@ -230,6 +232,7 @@ let rec format_expr (ctx : decl_ctx) (fmt : Format.formatter) (e : 'm expr) :
in
match Mark.remove e with
| EVar v -> Format.fprintf fmt "%a" format_var v
| EExternal qid -> Qident.format fmt qid
| ETuple es ->
Format.fprintf fmt "@[<hov 2>(%a)@]"
(Format.pp_print_list
@ -520,14 +523,15 @@ let rec format_scope_body_expr
let format_code_items
(ctx : decl_ctx)
(fmt : Format.formatter)
(code_items : 'm Ast.expr code_item_list) : unit =
(code_items : 'm Ast.expr code_item_list) : 'm Ast.expr Var.t String.Map.t =
Scope.fold_left
~f:(fun () item var ->
~f:(fun bnd item var ->
match item with
| Topdef (_, typ, e) ->
| Topdef (name, typ, e) ->
Format.fprintf fmt "@\n@\n@[<hov 2>let %a : %a =@\n%a@]" format_var var
format_typ typ (format_expr ctx) e
| ScopeDef (_, body) ->
format_typ typ (format_expr ctx) e;
String.Map.add (Mark.remove (TopdefName.get_info name)) var bnd
| ScopeDef (name, body) ->
let scope_input_var, scope_body_expr =
Bindlib.unbind body.scope_body_expr
in
@ -536,22 +540,54 @@ let format_code_items
(`Sname body.scope_body_input_struct) format_to_module_name
(`Sname body.scope_body_output_struct)
(format_scope_body_expr ctx)
scope_body_expr)
~init:() code_items
scope_body_expr;
String.Map.add (Mark.remove (ScopeName.get_info name)) var bnd)
~init:String.Map.empty code_items
let format_module_registration
fmt
(bnd : 'm Ast.expr Var.t String.Map.t)
modname =
Format.pp_open_vbox fmt 2;
Format.pp_print_string fmt "let () =";
Format.pp_print_space fmt ();
Format.pp_open_hvbox fmt 2;
Format.fprintf fmt "Runtime_ocaml.Runtime.register_module %S" modname;
Format.pp_print_space fmt ();
Format.pp_open_vbox fmt 2;
Format.pp_print_string fmt "[ ";
Format.pp_print_seq
~pp_sep:(fun fmt () ->
Format.pp_print_char fmt ';';
Format.pp_print_cut fmt ())
(fun fmt (id, var) ->
Format.fprintf fmt "@[<hov 2>%S,@ Obj.repr %a@]" id format_var var)
fmt (String.Map.to_seq bnd);
Format.pp_close_box fmt ();
Format.pp_print_char fmt ' ';
Format.pp_print_string fmt "]";
Format.pp_print_space fmt ();
Format.pp_print_string fmt "\"todo-module-hash\"";
Format.pp_close_box fmt ();
Format.pp_close_box fmt ()
let header =
{ocaml|
(** This file has been generated by the Catala compiler, do not edit! *)
open Runtime_ocaml.Runtime
[@@@ocaml.warning "-4-26-27-32-41-42"]
|ocaml}
let format_program
(fmt : Format.formatter)
?modname
(p : 'm Ast.program)
(type_ordering : Scopelang.Dependency.TVertex.t list) : unit =
Format.fprintf fmt
"(** This file has been generated by the Catala compiler, do not edit! *)@\n\
@\n\
open Runtime_ocaml.Runtime@\n\
@\n\
[@@@@@@ocaml.warning \"-4-26-27-32-41-42\"]@\n\
@\n\
%a%a@\n\
@?"
(format_ctx type_ordering) p.decl_ctx
(format_code_items p.decl_ctx)
p.code_items
Format.pp_print_string fmt header;
format_ctx type_ordering fmt p.decl_ctx;
let bnd = format_code_items p.decl_ctx fmt p.code_items in
Format.pp_print_newline fmt ();
Option.iter (format_module_registration fmt bnd) modname

4
compiler/lcalc/to_ocaml.mli
View File

@ -40,7 +40,9 @@ val format_var : Format.formatter -> 'm Var.t -> unit
val format_program :
Format.formatter ->
?modname:string ->
'm Ast.program ->
Scopelang.Dependency.TVertex.t list ->
unit
(** Usage [format_program fmt p type_dependencies_ordering] *)
(** Usage [format_program fmt p type_dependencies_ordering]. If [modname] is
set, registers the module for dynamic loading *)

56
compiler/plugin.ml
View File

@ -16,45 +16,43 @@
open Catala_utils
type 'ast plugin_apply_fun_typ =
source_file:Pos.input_file ->
output_file:string option ->
scope:Shared_ast.ScopeName.t option ->
'ast ->
Scopelang.Dependency.TVertex.t list ->
unit
type 'ast gen = {
name : string;
extension : string;
apply : 'ast plugin_apply_fun_typ;
}
type t =
| Dcalc of Shared_ast.untyped Dcalc.Ast.program gen
| Lcalc of Shared_ast.untyped Lcalc.Ast.program gen
| Scalc of Scalc.Ast.program gen
let name = function
| Dcalc { name; _ } | Lcalc { name; _ } | Scalc { name; _ } -> name
type t = Cmdliner.Cmd.Exit.code Cmdliner.Cmd.t
let backend_plugins : (string, t) Hashtbl.t = Hashtbl.create 17
let register t =
Hashtbl.replace backend_plugins (String.lowercase_ascii (name t)) t
Hashtbl.replace backend_plugins
(String.lowercase_ascii (Cmdliner.Cmd.name t))
t
let list () = Hashtbl.to_seq_values backend_plugins |> List.of_seq
module PluginAPI = struct
let register_dcalc ~name ~extension apply =
register (Dcalc { name; extension; apply })
open Cmdliner
let register_lcalc ~name ~extension apply =
register (Lcalc { name; extension; apply })
let register_generic info term = register (Cmd.v info term)
let register_scalc ~name ~extension apply =
register (Scalc { name; extension; apply })
(* For plugins relying on the standard [Driver] *)
type 'ast plugin_apply_fun_typ =
source_file:Pos.input_file ->
output_file:string option ->
scope:Shared_ast.ScopeName.t option ->
'ast ->
Scopelang.Dependency.TVertex.t list ->
unit
end
let find name = Hashtbl.find backend_plugins (String.lowercase_ascii name)
type 'ast gen = {
name : string;
extension : string;
apply : 'ast PluginAPI.plugin_apply_fun_typ;
}
type handler =
| Dcalc of Shared_ast.untyped Dcalc.Ast.program gen
| Lcalc of Shared_ast.untyped Lcalc.Ast.program gen
| Scalc of Scalc.Ast.program gen
let load_file f =
try

77
compiler/plugin.mli
View File

@ -14,31 +14,37 @@
License for the specific language governing permissions and limitations under
the License. *)
(** {2 catala-facing API} *)
open Catala_utils
type 'ast plugin_apply_fun_typ =
source_file:Pos.input_file ->
output_file:string option ->
scope:Shared_ast.ScopeName.t option ->
'ast ->
Scopelang.Dependency.TVertex.t list ->
unit
type t = Cmdliner.Cmd.Exit.code Cmdliner.Cmd.t
(** Plugins just provide an additional top-level command *)
type 'ast gen = {
name : string;
extension : string;
apply : 'ast plugin_apply_fun_typ;
}
(** {2 plugin-facing API} *)
type t =
| Dcalc of Shared_ast.untyped Dcalc.Ast.program gen
| Lcalc of Shared_ast.untyped Lcalc.Ast.program gen
| Scalc of Scalc.Ast.program gen
module PluginAPI : sig
open Cmdliner
val find : string -> t
(** Find a registered plugin *)
val register_generic : Cmd.info -> Cmd.Exit.code Term.t -> unit
(** Entry point for the registration of a generic catala subcommand *)
(** The following are used by [Driver.Plugin] to provide a higher-level
interface, registering plugins that rely on the [Driver.driver] function. *)
type 'ast plugin_apply_fun_typ =
source_file:Pos.input_file ->
output_file:string option ->
scope:Shared_ast.ScopeName.t option ->
'ast ->
Scopelang.Dependency.TVertex.t list ->
unit
end
val register : t -> unit
(** {2 catala-facing API} *)
val list : unit -> t list
(** List registered plugins *)
val load_file : string -> unit
(** Load the given plugin (cmo/cma or cmxs file) *)
@ -46,26 +52,15 @@ val load_file : string -> unit
val load_dir : string -> unit
(** Load all plugins found in the given directory *)
(** {2 plugin-facing API} *)
(** {3 Facilities for plugins using the standard driver} *)
module PluginAPI : sig
val register_dcalc :
name:string ->
extension:string ->
Shared_ast.untyped Dcalc.Ast.program plugin_apply_fun_typ ->
unit
type 'ast gen = {
name : string;
extension : string;
apply : 'ast PluginAPI.plugin_apply_fun_typ;
}
val register_lcalc :
name:string ->
extension:string ->
Shared_ast.untyped Lcalc.Ast.program plugin_apply_fun_typ ->
unit
val register_scalc :
name:string ->
extension:string ->
Scalc.Ast.program plugin_apply_fun_typ ->
unit
end
val register : t -> unit
type handler =
| Dcalc of Shared_ast.untyped Dcalc.Ast.program gen
| Lcalc of Shared_ast.untyped Lcalc.Ast.program gen
| Scalc of Scalc.Ast.program gen

11
compiler/plugins/api_web.ml
View File

@ -15,9 +15,6 @@
License for the specific language governing permissions and limitations under
the License. *)
(** Catala plugin for generating web APIs. It generates OCaml code before the
the associated [js_of_ocaml] wrapper. *)
open Catala_utils
open Shared_ast
open Lcalc
@ -28,6 +25,12 @@ module D = Dcalc.Ast
let name = "api_web"
let extension = ".ml"
let info =
Cmdliner.Cmd.info name
~doc:
"Catala plugin for generating web APIs. It generates OCaml code before \
the associated [js_of_ocaml] wrapper."
(** Contains all format functions used to generating the [js_of_ocaml] wrapper
of the corresponding Catala program. *)
module To_jsoo = struct
@ -468,4 +471,4 @@ let apply
(Option.value ~default:"stdout" jsoo_output_file);
To_jsoo.format_program fmt module_name prgm type_ordering)
let () = Driver.Plugin.register_lcalc ~name ~extension apply
let () = Driver.Plugin.register_lcalc info ~extension apply

11
compiler/plugins/json_schema.ml
View File

@ -14,12 +14,15 @@
License for the specific language governing permissions and limitations under
the License. *)
(** Catala plugin for generating {{:https://json-schema.org} JSON schemas} used
to build forms for the Catala website. *)
let name = "json_schema"
let extension = "_schema.json"
let info =
Cmdliner.Cmd.info name
~doc:
"Catala plugin for generating {{:https://json-schema.org} JSON schemas} \
used to build forms for the Catala website."
open Catala_utils
open Shared_ast
open Lcalc.To_ocaml
@ -232,4 +235,4 @@ let apply
| None ->
Message.raise_error "A scope must be specified for the plugin: %s" name
let () = Driver.Plugin.register_lcalc ~name ~extension apply
let () = Driver.Plugin.register_lcalc info ~extension apply

10
compiler/plugins/lazy_interp.ml
View File

@ -17,6 +17,10 @@
open Catala_utils
open Shared_ast
let name = "lazy"
let extension = ".out" (* unused *)
let info = Cmdliner.Cmd.info name ~doc:"Experimental lazy evaluation (plugin)"
(* -- Definition of the lazy interpreter -- *)
let log fmt = Format.ifprintf Format.err_formatter (fmt ^^ "@\n")
@ -209,6 +213,7 @@ let rec lazy_eval :
| (ELit (LBool false), _), _ ->
error e "Assert failure (%a)" Expr.format e
| _ -> error e "Invalid assertion condition %a" Expr.format e)
| EExternal _, _ -> assert false (* todo *)
| _ -> .
let interpret_program (prg : ('dcalc, 'm) gexpr program) (scope : ScopeName.t) :
@ -251,9 +256,6 @@ let interpret_program (prg : ('dcalc, 'm) gexpr program) (scope : ScopeName.t) :
(* -- Plugin registration -- *)
let name = "lazy"
let extension = ".out" (* unused *)
let apply ~source_file ~output_file ~scope prg _type_ordering =
let scope =
match scope with
@ -268,4 +270,4 @@ let apply ~source_file ~output_file ~scope prg _type_ordering =
let result_expr, _env = interpret_program prg scope in
Expr.format fmt result_expr
let () = Driver.Plugin.register_dcalc ~name ~extension apply
let () = Driver.Plugin.register_dcalc info ~extension apply

8
compiler/plugins/python.ml
View File

@ -25,10 +25,16 @@ open Catala_utils
let name = "python-plugin"
let extension = ".py"
let info =
Cmdliner.Cmd.info name
~doc:
"This plugin is for demonstration purposes and should be equivalent to \
using the built-in Python backend"
let apply ~source_file ~output_file ~scope prgm type_ordering =
ignore source_file;
ignore scope;
File.with_formatter_of_opt_file output_file
@@ fun fmt -> Scalc.To_python.format_program fmt prgm type_ordering
let () = Driver.Plugin.register_scalc ~name ~extension apply
let () = Driver.Plugin.register_scalc info ~extension apply

73
compiler/scopelang/from_desugared.ml
View File

@ -46,6 +46,17 @@ let rec translate_expr (ctx : ctx) (e : Desugared.Ast.expr) :
untyped Ast.expr boxed =
let m = Mark.get e in
match Mark.remove e with
| EVar v -> Expr.evar (Var.Map.find v ctx.var_mapping) m
| EAbs { binder; tys } ->
let vars, body = Bindlib.unmbind binder in
let new_vars = Array.map (fun var -> Var.make (Bindlib.name_of var)) vars in
let ctx =
List.fold_left2
(fun ctx var new_var ->
{ ctx with var_mapping = Var.Map.add var new_var ctx.var_mapping })
ctx (Array.to_list vars) (Array.to_list new_vars)
in
Expr.eabs (Expr.bind new_vars (translate_expr ctx body)) tys m
| ELocation (SubScopeVar (s_name, ss_name, s_var)) ->
(* When referring to a subscope variable in an expression, we are referring
to the output, hence we take the last state. *)
@ -70,9 +81,6 @@ let rec translate_expr (ctx : ctx) (e : Desugared.Ast.expr) :
| States states -> Mark.copy s_var (List.assoc state states)))
m
| ELocation (ToplevelVar v) -> Expr.elocation (ToplevelVar v) m
| EVar v -> Expr.evar (Var.Map.find v ctx.var_mapping) m
| EStruct { name; fields } ->
Expr.estruct name (StructField.Map.map (translate_expr ctx) fields) m
| EDStructAccess { name_opt = None; _ } ->
(* Note: this could only happen if disambiguation was disabled. If we want
to support it, we should still allow this case when the field has only
@ -84,7 +92,7 @@ let rec translate_expr (ctx : ctx) (e : Desugared.Ast.expr) :
let field =
try
StructName.Map.find name
(IdentName.Map.find field ctx.decl_ctx.ctx_struct_fields)
(Ident.Map.find field ctx.decl_ctx.ctx_struct_fields)
with Not_found ->
(* Should not happen after disambiguation *)
Message.raise_spanned_error (Expr.mark_pos m)
@ -93,14 +101,6 @@ let rec translate_expr (ctx : ctx) (e : Desugared.Ast.expr) :
field StructName.format_t name
in
Expr.estructaccess e' field name m
| ETuple es -> Expr.etuple (List.map (translate_expr ctx) es) m
| ETupleAccess { e; index; size } ->
Expr.etupleaccess (translate_expr ctx e) index size m
| EInj { e; cons; name } -> Expr.einj (translate_expr ctx e) cons name m
| EMatch { e; name; cases } ->
Expr.ematch (translate_expr ctx e) name
(EnumConstructor.Map.map (translate_expr ctx) cases)
m
| EScopeCall { scope; args } ->
Expr.escopecall scope
(ScopeVar.Map.fold
@ -117,20 +117,6 @@ let rec translate_expr (ctx : ctx) (e : Desugared.Ast.expr) :
ScopeVar.Map.add v' (translate_expr ctx e) args')
args ScopeVar.Map.empty)
m
| ELit
((LBool _ | LInt _ | LRat _ | LMoney _ | LUnit | LDate _ | LDuration _) as
l) ->
Expr.elit l m
| EAbs { binder; tys } ->
let vars, body = Bindlib.unmbind binder in
let new_vars = Array.map (fun var -> Var.make (Bindlib.name_of var)) vars in
let ctx =
List.fold_left2
(fun ctx var new_var ->
{ ctx with var_mapping = Var.Map.add var new_var ctx.var_mapping })
ctx (Array.to_list vars) (Array.to_list new_vars)
in
Expr.eabs (Expr.bind new_vars (translate_expr ctx body)) tys m
| EApp { f = EOp { op; tys }, m1; args } ->
let args = List.map (translate_expr ctx) args in
Operator.kind_dispatch op
@ -144,19 +130,10 @@ let rec translate_expr (ctx : ctx) (e : Desugared.Ast.expr) :
| op, `Reversed ->
Expr.eapp (Expr.eop op (List.rev tys) m1) (List.rev args) m)
| EOp _ -> assert false (* Only allowed within [EApp] *)
| EApp { f; args } ->
Expr.eapp (translate_expr ctx f) (List.map (translate_expr ctx) args) m
| EDefault { excepts; just; cons } ->
Expr.edefault
(List.map (translate_expr ctx) excepts)
(translate_expr ctx just) (translate_expr ctx cons) m
| EIfThenElse { cond; etrue; efalse } ->
Expr.eifthenelse (translate_expr ctx cond) (translate_expr ctx etrue)
(translate_expr ctx efalse)
m
| EArray args -> Expr.earray (List.map (translate_expr ctx) args) m
| EEmptyError -> Expr.eemptyerror m
| EErrorOnEmpty e1 -> Expr.eerroronempty (translate_expr ctx e1) m
| ( EStruct _ | ETuple _ | ETupleAccess _ | EInj _ | EMatch _ | ELit _
| EApp _ | EDefault _ | EIfThenElse _ | EArray _ | EEmptyError
| EErrorOnEmpty _ | EExternal _ ) as e ->
Expr.map ~f:(translate_expr ctx) (e, m)
(** {1 Rule tree construction} *)
@ -825,18 +802,24 @@ let translate_program
{ out_str with out_struct_fields })
pgrm.Desugared.Ast.program_ctx.ctx_scopes
in
let new_program_scopes =
let program_scopes =
ScopeName.Map.fold
(fun scope_name scope new_program_scopes ->
let new_program_scope = translate_scope ctx scope exc_graphs in
ScopeName.Map.add scope_name new_program_scope new_program_scopes)
pgrm.program_scopes ScopeName.Map.empty
in
let program_topdefs =
TopdefName.Map.mapi
(fun id -> function
| Some e, ty -> Expr.unbox (translate_expr ctx e), ty
| None, (_, pos) ->
Message.raise_spanned_error pos "No definition found for %a"
TopdefName.format_t id)
pgrm.program_topdefs
in
{
Ast.program_topdefs =
TopdefName.Map.map
(fun (e, ty) -> Expr.unbox (translate_expr ctx e), ty)
pgrm.program_topdefs;
Ast.program_scopes = new_program_scopes;
Ast.program_topdefs;
program_scopes;
program_ctx = { pgrm.program_ctx with ctx_scopes };
}

42
compiler/shared_ast/definitions.ml
View File

@ -36,7 +36,7 @@ module LabelName = Uid.Gen ()
(** Used for unresolved structs/maps in desugared *)
module IdentName = String
module Ident = String
(** Only used by desugared/scopelang *)
@ -56,8 +56,13 @@ module StateName = Uid.Gen ()
(** These types allow to select the features present in any given expression
type *)
type yes = private Yes
type no = |
type yes = Yes
type no =
| No
(** Phantom types used in the definitions below. We don't make them
abstract, because the typer needs to know that their intersection is
empty. *)
type desugared =
< monomorphic : yes
@ -71,7 +76,8 @@ type desugared =
; explicitScopes : yes
; assertions : no
; defaultTerms : yes
; exceptions : no >
; exceptions : no
; custom : no >
type scopelang =
< monomorphic : yes
@ -85,7 +91,8 @@ type scopelang =
; explicitScopes : yes
; assertions : no
; defaultTerms : yes
; exceptions : no >
; exceptions : no
; custom : no >
type dcalc =
< monomorphic : yes
@ -99,7 +106,8 @@ type dcalc =
; explicitScopes : no
; assertions : yes
; defaultTerms : yes
; exceptions : no >
; exceptions : no
; custom : no >
type lcalc =
< monomorphic : yes
@ -113,7 +121,8 @@ type lcalc =
; explicitScopes : no
; assertions : yes
; defaultTerms : no
; exceptions : yes >
; exceptions : yes
; custom : no >
type 'a any = < .. > as 'a
(** ['a any] is 'a, but adds the constraint that it should be restricted to
@ -131,7 +140,8 @@ type ('a, 'b) dcalc_lcalc =
; explicitScopes : no
; assertions : yes
; defaultTerms : 'a
; exceptions : 'b >
; exceptions : 'b
; custom : no >
(** This type regroups Dcalc and Lcalc ASTs. *)
(** {2 Types} *)
@ -379,6 +389,7 @@ and ('a, 'b, 'm) base_gexpr =
-> ('a, (< .. > as 'b), 'm) base_gexpr
| EArray : ('a, 'm) gexpr list -> ('a, < .. >, 'm) base_gexpr
| EVar : ('a, 'm) naked_gexpr Bindlib.var -> ('a, _, 'm) base_gexpr
| EExternal : Qident.t -> ('a, < .. >, 't) base_gexpr
| EAbs : {
binder : (('a, 'a, 'm) base_gexpr, ('a, 'm) gexpr) Bindlib.mbinder;
tys : typ list;
@ -424,7 +435,7 @@ and ('a, 'b, 'm) base_gexpr =
| EDStructAccess : {
name_opt : StructName.t option;
e : ('a, 'm) gexpr;
field : IdentName.t;
field : Ident.t;
}
-> ('a, < syntacticNames : yes ; .. >, 'm) base_gexpr
(** [desugared] has ambiguous struct fields *)
@ -456,6 +467,16 @@ and ('a, 'b, 'm) base_gexpr =
handler : ('a, 'm) gexpr;
}
-> ('a, < exceptions : yes ; .. >, 'm) base_gexpr
(* Only used during evaluation *)
| ECustom : {
obj : Obj.t;
targs : typ list;
tret : typ;
}
-> ('a, < custom : yes ; .. >, 't) base_gexpr
(** A function of the given type, as a runtime OCaml object. The specified
types for arguments and result must be the Catala types corresponding
to the runtime types of the function. *)
(** Useful for errors and printing, for example *)
type any_expr = AnyExpr : ('a, _) gexpr -> any_expr
@ -549,9 +570,10 @@ type scope_out_struct = {
type decl_ctx = {
ctx_enums : enum_ctx;
ctx_structs : struct_ctx;
ctx_struct_fields : StructField.t StructName.Map.t IdentName.Map.t;
ctx_struct_fields : StructField.t StructName.Map.t Ident.Map.t;
(** needed for disambiguation (desugared -> scope) *)
ctx_scopes : scope_out_struct ScopeName.Map.t;
ctx_modules : typ Qident.Map.t;
}
type 'e program = { decl_ctx : decl_ctx; code_items : 'e code_item_list }

43
compiler/shared_ast/expr.ml
View File

@ -109,6 +109,7 @@ let subst binder vars =
Bindlib.msubst binder (Array.of_list (List.map Mark.remove vars))
let evar v mark = Mark.add mark (Bindlib.box_var v)
let eexternal eref mark = Mark.add mark (Bindlib.box (EExternal eref))
let etuple args = Box.appn args @@ fun args -> ETuple args
let etupleaccess e index size =
@ -140,6 +141,9 @@ let eraise e1 = Box.app0 @@ ERaise e1
let ecatch body exn handler =
Box.app2 body handler @@ fun body handler -> ECatch { body; exn; handler }
let ecustom obj targs tret mark =
Mark.add mark (Bindlib.box (ECustom { obj; targs; tret }))
let elocation loc = Box.app0 @@ ELocation loc
let estruct name (fields : ('a, 't) boxed_gexpr StructField.Map.t) mark =
@ -268,6 +272,7 @@ let map
| EOp { op; tys } -> eop op tys m
| EArray args -> earray (List.map f args) m
| EVar v -> evar (Var.translate v) m
| EExternal eref -> eexternal eref m
| EAbs { binder; tys } ->
let vars, body = Bindlib.unmbind binder in
let body = f body in
@ -298,6 +303,7 @@ let map
| EScopeCall { scope; args } ->
let fields = ScopeVar.Map.map f args in
escopecall scope fields m
| ECustom { obj; targs; tret } -> ecustom obj targs tret m
let rec map_top_down ~f e = map ~f:(map_top_down ~f) (f e)
let map_marks ~f e = map_top_down ~f:(Mark.map_mark f) e
@ -310,7 +316,9 @@ let shallow_fold
(acc : 'acc) : 'acc =
let lfold x acc = List.fold_left (fun acc x -> f x acc) acc x in
match Mark.remove e with
| ELit _ | EOp _ | EVar _ | ERaise _ | ELocation _ | EEmptyError -> acc
| ELit _ | EOp _ | EVar _ | EExternal _ | ERaise _ | ELocation _ | EEmptyError
->
acc
| EApp { f = e; args } -> acc |> f e |> lfold args
| EArray args -> acc |> lfold args
| EAbs { binder; tys = _ } ->
@ -330,6 +338,7 @@ let shallow_fold
| EMatch { e; cases; _ } ->
acc |> f e |> EnumConstructor.Map.fold (fun _ -> f) cases
| EScopeCall { args; _ } -> acc |> ScopeVar.Map.fold (fun _ -> f) args
| ECustom _ -> acc
(* Like [map], but also allows to gather a result bottom-up. *)
let map_gather
@ -360,6 +369,7 @@ let map_gather
let acc, args = lfoldmap args in
acc, earray args m
| EVar v -> acc, evar (Var.translate v) m
| EExternal eref -> acc, eexternal eref m
| EAbs { binder; tys } ->
let vars, body = Bindlib.unmbind binder in
let acc, body = f body in
@ -433,6 +443,7 @@ let map_gather
args (acc, ScopeVar.Map.empty)
in
acc, escopecall scope args m
| ECustom { obj; targs; tret } -> acc, ecustom obj targs tret m
(* - *)
@ -441,6 +452,11 @@ let rec rebox (e : ('a any, 't) gexpr) = map ~f:rebox e
let box e = Mark.map Bindlib.box e
let unbox (e, m) = Bindlib.unbox e, m
let unbox_closed e =
Box.assert_closed (fst e);
unbox e
let untype e = map_marks ~f:(fun m -> Untyped { pos = mark_pos m }) e
(* Tests *)
@ -541,6 +557,7 @@ and equal : type a. (a, 't) gexpr -> (a, 't) gexpr -> bool =
fun e1 e2 ->
match Mark.remove e1, Mark.remove e2 with
| EVar v1, EVar v2 -> Bindlib.eq_vars v1 v2
| EExternal eref1, EExternal eref2 -> Qident.equal eref1 eref2
| ETuple es1, ETuple es2 -> equal_list es1 es2
| ( ETupleAccess { e = e1; index = id1; size = s1 },
ETupleAccess { e = e2; index = id2; size = s2 } ) ->
@ -573,7 +590,7 @@ and equal : type a. (a, 't) gexpr -> (a, 't) gexpr -> bool =
StructName.equal s1 s2 && StructField.Map.equal equal fields1 fields2
| ( EDStructAccess { e = e1; field = f1; name_opt = s1 },
EDStructAccess { e = e2; field = f2; name_opt = s2 } ) ->
Option.equal StructName.equal s1 s2 && IdentName.equal f1 f2 && equal e1 e2
Option.equal StructName.equal s1 s2 && Ident.equal f1 f2 && equal e1 e2
| ( EStructAccess { e = e1; field = f1; name = s1 },
EStructAccess { e = e2; field = f2; name = s2 } ) ->
StructName.equal s1 s2 && StructField.equal f1 f2 && equal e1 e2
@ -588,10 +605,14 @@ and equal : type a. (a, 't) gexpr -> (a, 't) gexpr -> bool =
| ( EScopeCall { scope = s1; args = fields1 },
EScopeCall { scope = s2; args = fields2 } ) ->
ScopeName.equal s1 s2 && ScopeVar.Map.equal equal fields1 fields2
| ( ( EVar _ | ETuple _ | ETupleAccess _ | EArray _ | ELit _ | EAbs _ | EApp _
| EAssert _ | EOp _ | EDefault _ | EIfThenElse _ | EEmptyError
| EErrorOnEmpty _ | ERaise _ | ECatch _ | ELocation _ | EStruct _
| EDStructAccess _ | EStructAccess _ | EInj _ | EMatch _ | EScopeCall _ ),
| ( ECustom { obj = obj1; targs = targs1; tret = tret1 },
ECustom { obj = obj2; targs = targs2; tret = tret2 } ) ->
Type.equal_list targs1 targs2 && Type.equal tret1 tret2 && obj1 == obj2
| ( ( EVar _ | EExternal _ | ETuple _ | ETupleAccess _ | EArray _ | ELit _
| EAbs _ | EApp _ | EAssert _ | EOp _ | EDefault _ | EIfThenElse _
| EEmptyError | EErrorOnEmpty _ | ERaise _ | ECatch _ | ELocation _
| EStruct _ | EDStructAccess _ | EStructAccess _ | EInj _ | EMatch _
| EScopeCall _ | ECustom _ ),
_ ) ->
false
@ -614,6 +635,8 @@ let rec compare : type a. (a, _) gexpr -> (a, _) gexpr -> int =
List.compare compare a1 a2
| EVar v1, EVar v2 ->
Bindlib.compare_vars v1 v2
| EExternal eref1, EExternal eref2 ->
Qident.compare eref1 eref2
| EAbs {binder=binder1; tys=typs1},
EAbs {binder=binder2; tys=typs2} ->
List.compare Type.compare typs1 typs2 @@< fun () ->
@ -633,7 +656,7 @@ let rec compare : type a. (a, _) gexpr -> (a, _) gexpr -> int =
| EDStructAccess {e=e1; field=field_name1; name_opt=struct_name1},
EDStructAccess {e=e2; field=field_name2; name_opt=struct_name2} ->
compare e1 e2 @@< fun () ->
IdentName.compare field_name1 field_name2 @@< fun () ->
Ident.compare field_name1 field_name2 @@< fun () ->
Option.compare StructName.compare struct_name1 struct_name2
| EStructAccess {e=e1; field=field_name1; name=struct_name1},
EStructAccess {e=e2; field=field_name2; name=struct_name2} ->
@ -678,11 +701,15 @@ let rec compare : type a. (a, _) gexpr -> (a, _) gexpr -> int =
compare_except ex1 ex2 @@< fun () ->
compare etry1 etry2 @@< fun () ->
compare ewith1 ewith2
| ECustom _, _ | _, ECustom _ ->
(* fixme: ideally this would be forbidden by typing *)
invalid_arg "Custom block comparison"
| ELit _, _ -> -1 | _, ELit _ -> 1
| EApp _, _ -> -1 | _, EApp _ -> 1
| EOp _, _ -> -1 | _, EOp _ -> 1
| EArray _, _ -> -1 | _, EArray _ -> 1
| EVar _, _ -> -1 | _, EVar _ -> 1
| EExternal _, _ -> -1 | _, EExternal _ -> 1
| EAbs _, _ -> -1 | _, EAbs _ -> 1
| EIfThenElse _, _ -> -1 | _, EIfThenElse _ -> 1
| ELocation _, _ -> -1 | _, ELocation _ -> 1
@ -735,7 +762,7 @@ let format ppf e = Print.expr ~debug:false () ppf e
let rec size : type a. (a, 't) gexpr -> int =
fun e ->
match Mark.remove e with
| EVar _ | ELit _ | EOp _ | EEmptyError -> 1
| EVar _ | EExternal _ | ELit _ | EOp _ | EEmptyError | ECustom _ -> 1
| ETuple args -> List.fold_left (fun acc arg -> acc + size arg) 1 args
| EArray args -> List.fold_left (fun acc arg -> acc + size arg) 1 args
| ETupleAccess { e; _ } -> size e + 1

14
compiler/shared_ast/expr.mli
View File

@ -28,10 +28,15 @@ val box : ('a, 'm) gexpr -> ('a, 'm) boxed_gexpr
val unbox : ('a, 'm) boxed_gexpr -> ('a, 'm) gexpr
(** For closed expressions, similar to [Bindlib.unbox] *)
val unbox_closed : ('a, 'm) boxed_gexpr -> ('a, 'm) gexpr
(** Similar to [unbox], but with an added assertion check on the expression
being closed *)
val rebox : ('a any, 'm) gexpr -> ('a, 'm) boxed_gexpr
(** Rebuild the whole term, re-binding all variables and exposing free variables *)
val evar : ('a, 'm) gexpr Var.t -> 'm mark -> ('a, 'm) boxed_gexpr
val eexternal : Qident.t -> 'm mark -> ('a any, 'm) boxed_gexpr
val bind :
('a, 'm) gexpr Var.t array ->
@ -110,7 +115,7 @@ val estruct :
val edstructaccess :
('a, 'm) boxed_gexpr ->
IdentName.t ->
Ident.t ->
StructName.t option ->
'm mark ->
((< syntacticNames : yes ; .. > as 'a), 'm) boxed_gexpr
@ -142,6 +147,13 @@ val escopecall :
'm mark ->
((< explicitScopes : yes ; .. > as 'a), 'm) boxed_gexpr
val ecustom :
Obj.t ->
Type.t list ->
Type.t ->
'm mark ->
(< custom : Definitions.yes ; .. >, 'm) boxed_gexpr
val fun_id : 'm mark -> ('a any, 'm) boxed_gexpr
(** {2 Manipulation of marks} *)

206
compiler/shared_ast/interpreter.ml
View File

@ -23,6 +23,21 @@ open Definitions
open Op
module Runtime = Runtime_ocaml.Runtime
type features =
< monomorphic : yes
; polymorphic : yes
; overloaded : no
; resolved : yes
; syntacticNames : no
; resolvedNames : yes
; scopeVarStates : no
; scopeVarSimpl : no
; explicitScopes : no
; assertions : yes >
type ('d, 'e, 'c) astk =
< features ; defaultTerms : 'd ; exceptions : 'e ; custom : 'c >
(** {1 Helpers} *)
let is_empty_error : type a. (a, 'm) gexpr -> bool =
@ -375,10 +390,123 @@ let rec evaluate_operator
_ ) ->
err ()
(* /S\ dark magic here. This relies both on internals of [Lcalc.to_ocaml] *and*
of the OCaml runtime *)
let rec runtime_to_val :
(decl_ctx -> ('a, 'm) gexpr -> ('a, 'm) gexpr) ->
decl_ctx ->
'm mark ->
typ ->
Obj.t ->
(((_, _, yes) astk as 'a), 'm) gexpr =
fun eval_expr ctx m ty o ->
let m = Expr.map_ty (fun _ -> ty) m in
match Mark.remove ty with
| TLit TBool -> ELit (LBool (Obj.obj o)), m
| TLit TUnit -> ELit LUnit, m
| TLit TInt -> ELit (LInt (Obj.obj o)), m
| TLit TRat -> ELit (LRat (Obj.obj o)), m
| TLit TMoney -> ELit (LMoney (Obj.obj o)), m
| TLit TDate -> ELit (LDate (Obj.obj o)), m
| TLit TDuration -> ELit (LDuration (Obj.obj o)), m
| TTuple ts ->
( ETuple
(List.map2
(runtime_to_val eval_expr ctx m)
ts
(Array.to_list (Obj.obj o))),
m )
| TStruct name ->
StructName.Map.find name ctx.ctx_structs
|> StructField.Map.to_seq
|> Seq.map2
(fun o (fld, ty) -> fld, runtime_to_val eval_expr ctx m ty o)
(Array.to_seq (Obj.obj o))
|> StructField.Map.of_seq
|> fun fields -> EStruct { name; fields }, m
| TEnum name ->
(* we only use non-constant constructors of arity 1, which allows us to
always use the tag directly (ordered as declared in the constr map), and
the field 0 *)
let cons, ty =
List.nth
(EnumConstructor.Map.bindings (EnumName.Map.find name ctx.ctx_enums))
(Obj.tag o - Obj.first_non_constant_constructor_tag)
in
let e = runtime_to_val eval_expr ctx m ty (Obj.field o 0) in
EInj { name; cons; e }, m
| TOption _ty -> assert false
| TArray ty ->
( EArray
(List.map
(runtime_to_val eval_expr ctx m ty)
(Array.to_list (Obj.obj o))),
m )
| TArrow (targs, tret) -> ECustom { obj = o; targs; tret }, m
| TAny -> assert false
and val_to_runtime :
(decl_ctx -> ('a, 'm) gexpr -> ('a, 'm) gexpr) ->
decl_ctx ->
typ ->
('b, 'm) gexpr ->
Obj.t =
fun eval_expr ctx ty v ->
match Mark.remove ty, Mark.remove v with
| TLit TBool, ELit (LBool b) -> Obj.repr b
| TLit TUnit, ELit LUnit -> Obj.repr ()
| TLit TInt, ELit (LInt i) -> Obj.repr i
| TLit TRat, ELit (LRat r) -> Obj.repr r
| TLit TMoney, ELit (LMoney m) -> Obj.repr m
| TLit TDate, ELit (LDate t) -> Obj.repr t
| TLit TDuration, ELit (LDuration d) -> Obj.repr d
| TTuple ts, ETuple es ->
List.map2 (val_to_runtime eval_expr ctx) ts es |> Array.of_list |> Obj.repr
| TStruct name1, EStruct { name; fields } ->
assert (StructName.equal name name1);
let fld_tys = StructName.Map.find name ctx.ctx_structs in
Seq.map2
(fun (_, ty) (_, v) -> val_to_runtime eval_expr ctx ty v)
(StructField.Map.to_seq fld_tys)
(StructField.Map.to_seq fields)
|> Array.of_seq
|> Obj.repr
| TEnum name1, EInj { name; cons; e } ->
assert (EnumName.equal name name1);
let rec find_tag n = function
| [] -> assert false
| (c, ty) :: _ when EnumConstructor.equal c cons -> n, ty
| _ :: r -> find_tag (n + 1) r
in
let tag, ty =
find_tag Obj.first_non_constant_constructor_tag
(EnumConstructor.Map.bindings (EnumName.Map.find name ctx.ctx_enums))
in
let o = Obj.with_tag tag (Obj.repr (Some ())) in
Obj.set_field o 0 (val_to_runtime eval_expr ctx ty e);
o
| TOption _ty, _ -> assert false
| TArray ty, EArray es ->
Array.of_list (List.map (val_to_runtime eval_expr ctx ty) es) |> Obj.repr
| TArrow (targs, tret), _ ->
let m = Mark.get v in
(* we want stg like [fun args -> val_to_runtime (eval_expr ctx (EApp (v,
args)))] but in curried form *)
let rec curry acc = function
| [] ->
let args = List.rev acc in
val_to_runtime eval_expr ctx tret
(eval_expr ctx (EApp { f = v; args }, m))
| targ :: targs ->
Obj.repr (fun x ->
curry (runtime_to_val eval_expr ctx m targ x :: acc) targs)
in
curry [] targs
| _ -> assert false
let rec evaluate_expr :
type a b.
decl_ctx -> ((a, b) dcalc_lcalc, 'm) gexpr -> ((a, b) dcalc_lcalc, 'm) gexpr
=
type d e.
decl_ctx -> ((d, e, yes) astk, 't) gexpr -> ((d, e, yes) astk, 't) gexpr =
fun ctx e ->
let m = Mark.get e in
let pos = Expr.mark_pos m in
@ -387,6 +515,14 @@ let rec evaluate_expr :
Message.raise_spanned_error pos
"free variable found at evaluation (should not happen if term was \
well-typed)"
| EExternal qid -> (
match Qident.Map.find_opt qid ctx.ctx_modules with
| None ->
Message.raise_spanned_error pos "Reference to %a could not be resolved"
Qident.format qid
| Some ty ->
let o = Runtime.lookup_value qid in
runtime_to_val evaluate_expr ctx m ty o)
| EApp { f = e1; args } -> (
let e1 = evaluate_expr ctx e1 in
let args = List.map (evaluate_expr ctx) args in
@ -403,11 +539,23 @@ let rec evaluate_expr :
(Bindlib.mbinder_arity binder)
(List.length args)
| EOp { op; _ } -> evaluate_operator (evaluate_expr ctx) op m args
| ECustom { obj; targs; tret } ->
(* Applies the arguments one by one to the curried form *)
List.fold_left2
(fun fobj targ arg ->
(Obj.obj fobj : Obj.t -> Obj.t)
(val_to_runtime evaluate_expr ctx targ arg))
obj targs args
|> Obj.obj
|> fun o -> runtime_to_val evaluate_expr ctx m tret o
| _ ->
Message.raise_spanned_error pos
"function has not been reduced to a lambda at evaluation (should not \
happen if the term was well-typed")
| (EAbs _ | ELit _ | EOp _) as e -> Mark.add m e (* these are values *)
| EAbs { binder; tys } -> Expr.unbox (Expr.eabs (Bindlib.box binder) tys m)
| ELit _ as e -> Mark.add m e
| EOp { op; tys } -> Expr.unbox (Expr.eop (Operator.translate op) tys m)
(* | EAbs _ as e -> Marked.mark m e (* these are values *) *)
| EStruct { fields = es; name } ->
let fields, es = List.split (StructField.Map.bindings es) in
let es = List.map (evaluate_expr ctx) es in
@ -514,6 +662,7 @@ let rec evaluate_expr :
Message.raise_spanned_error (Expr.pos e')
"Expected a boolean literal for the result of this assertion \
(should not happen if the term was well-typed)")
| ECustom _ -> e
| EEmptyError -> Mark.copy e EEmptyError
| EErrorOnEmpty e' -> (
match evaluate_expr ctx e' with
@ -552,6 +701,55 @@ let rec evaluate_expr :
evaluate_expr ctx handler)
| _ -> .
(* Typing shenanigan to add custom terms to the AST type. This is an identity
and could be optimised into [Obj.magic]. *)
let addcustom e =
let rec f :
type c d e.
((d, e, c) astk, 't) gexpr -> ((d, e, yes) astk, 't) gexpr boxed =
function
| (ECustom _, _) as e -> Expr.map ~f e
| EOp { op; tys }, m -> Expr.eop (Operator.translate op) tys m
| (EDefault _, _) as e -> Expr.map ~f e
| (EEmptyError, _) as e -> Expr.map ~f e
| (EErrorOnEmpty _, _) as e -> Expr.map ~f e
| (ECatch _, _) as e -> Expr.map ~f e
| (ERaise _, _) as e -> Expr.map ~f e
| ( ( EAssert _ | ELit _ | EApp _ | EArray _ | EVar _ | EExternal _ | EAbs _
| EIfThenElse _ | ETuple _ | ETupleAccess _ | EInj _ | EStruct _
| EStructAccess _ | EMatch _ ),
_ ) as e ->
Expr.map ~f e
| _ -> .
in
Expr.unbox (f e)
let delcustom e =
let rec f :
type c d e.
((d, e, c) astk, 't) gexpr -> ((d, e, no) astk, 't) gexpr boxed = function
| ECustom _, _ -> invalid_arg "Custom term remaining in evaluated term"
| EOp { op; tys }, m -> Expr.eop (Operator.translate op) tys m
| (EDefault _, _) as e -> Expr.map ~f e
| (EEmptyError, _) as e -> Expr.map ~f e
| (EErrorOnEmpty _, _) as e -> Expr.map ~f e
| (ECatch _, _) as e -> Expr.map ~f e
| (ERaise _, _) as e -> Expr.map ~f e
| ( ( EAssert _ | ELit _ | EApp _ | EArray _ | EVar _ | EExternal _ | EAbs _
| EIfThenElse _ | ETuple _ | ETupleAccess _ | EInj _ | EStruct _
| EStructAccess _ | EMatch _ ),
_ ) as e ->
Expr.map ~f e
| _ -> .
in
Expr.unbox (f e)
(* Evaluation may introduce intermediate custom terms ([ECustom], pointers to
external functions), straying away from the DCalc and LCalc ASTS. [addcustom]
and [delcustom] are needed to expand and shrink the type of the terms to
reflect that. *)
let evaluate_expr ctx e = delcustom (evaluate_expr ctx (addcustom e))
let interpret_program_lcalc p s : (Uid.MarkedString.info * ('a, 'm) gexpr) list
=
let e = Expr.unbox @@ Program.to_expr p s in

19
compiler/shared_ast/interpreter.mli
View File

@ -20,8 +20,21 @@
open Catala_utils
open Definitions
type features =
< monomorphic : yes
; polymorphic : yes
; overloaded : no
; resolved : yes
; syntacticNames : no
; resolvedNames : yes
; scopeVarStates : no
; scopeVarSimpl : no
; explicitScopes : no
; assertions : yes >
(** The interpreter only works on dcalc and lcalc, which share these features *)
val evaluate_operator :
((((_, _) dcalc_lcalc as 'a), 'm) gexpr -> ('a, 'm) gexpr) ->
(((< features ; .. > as 'a), 'm) gexpr -> ('a, 'm) gexpr) ->
'a operator ->
'm mark ->
('a, 'm) gexpr list ->
@ -32,9 +45,7 @@ val evaluate_operator :
operator. *)
val evaluate_expr :
decl_ctx ->
(('a, 'b) dcalc_lcalc, 'm) gexpr ->
(('a, 'b) dcalc_lcalc, 'm) gexpr
decl_ctx -> (((_, _) dcalc_lcalc as 'a), 'm) gexpr -> ('a, 'm) gexpr
(** Evaluates an expression according to the semantics of the default calculus. *)
val interpret_program_dcalc :

32
compiler/shared_ast/optimizations.ml
View File

@ -184,7 +184,7 @@ let rec optimize_expr :
when name = name1 ->
Mark.remove (StructField.Map.find field fields)
| EDefault { excepts; just; cons } -> (
(* TODO: mechanically prove each of these optimizations correct :) *)
(* TODO: mechanically prove each of these optimizations correct *)
let excepts =
List.filter (fun except -> Mark.remove except <> EEmptyError) excepts
(* we can discard the exceptions that are always empty error *)
@ -198,7 +198,8 @@ let rec optimize_expr :
(* at this point we know a conflict error will be triggered so we just
feed the expression to the interpreter that will print the beautiful
right error message *)
Mark.remove (Interpreter.evaluate_expr ctx.decl_ctx e)
let _ = Interpreter.evaluate_expr ctx.decl_ctx e in
assert false
else
match excepts, just with
| [except], _ when Expr.is_value except ->
@ -302,7 +303,12 @@ let rec optimize_expr :
in
Expr.Box.app1 e reduce mark
let optimize_expr (decl_ctx : decl_ctx) (e : (('a, 'b) dcalc_lcalc, 'm) gexpr) =
let optimize_expr :
'm.
decl_ctx ->
(('a, 'b) dcalc_lcalc, 'm) gexpr ->
(('a, 'b) dcalc_lcalc, 'm) boxed_gexpr =
fun (decl_ctx : decl_ctx) (e : (('a, 'b) dcalc_lcalc, 'm) gexpr) ->
optimize_expr { var_values = Var.Map.empty; decl_ctx } e
let optimize_program (p : 'm program) : 'm program =
@ -339,15 +345,7 @@ let test_iota_reduction_1 () =
x"
(Format.asprintf "before=%a\nafter=%a" Expr.format (Expr.unbox matchA)
Expr.format
(Expr.unbox
(optimize_expr
{
ctx_enums = EnumName.Map.empty;
ctx_structs = StructName.Map.empty;
ctx_struct_fields = IdentName.Map.empty;
ctx_scopes = ScopeName.Map.empty;
}
(Expr.unbox matchA))))
(Expr.unbox (optimize_expr Program.empty_ctx (Expr.unbox matchA))))
let cases_of_list l : ('a, 't) boxed_gexpr EnumConstructor.Map.t =
EnumConstructor.Map.of_seq
@ -409,12 +407,4 @@ let test_iota_reduction_2 () =
\ | B → (λ (x: any) → D B x)\n"
(Format.asprintf "before=@[%a@]@.after=%a@." Expr.format (Expr.unbox matchA)
Expr.format
(Expr.unbox
(optimize_expr
{
ctx_enums = EnumName.Map.empty;
ctx_structs = StructName.Map.empty;
ctx_struct_fields = IdentName.Map.empty;
ctx_scopes = ScopeName.Map.empty;
}
(Expr.unbox matchA))))
(Expr.unbox (optimize_expr Program.empty_ctx (Expr.unbox matchA))))

6
compiler/shared_ast/print.ml
View File

@ -379,6 +379,7 @@ module Precedence = struct
| EOp _ -> Contained
| EArray _ -> Contained
| EVar _ -> Contained
| EExternal _ -> Contained
| EAbs _ -> Abs
| EIfThenElse _ -> Contained
| EStruct _ -> Contained
@ -395,6 +396,7 @@ module Precedence = struct
| EErrorOnEmpty _ -> App
| ERaise _ -> App
| ECatch _ -> App
| ECustom _ -> Contained
let needs_parens ~context ?(rhs = false) e =
match expr context, expr e with
@ -461,6 +463,7 @@ let rec expr_aux :
let rhs ex = paren ~rhs:true ex in
match Mark.remove e with
| EVar v -> var fmt v
| EExternal eref -> Qident.format fmt eref
| ETuple es ->
Format.fprintf fmt "@[<hov 2>%a%a%a@]" punctuation "("
(Format.pp_print_list
@ -608,7 +611,7 @@ let rec expr_aux :
| ELocation loc -> location fmt loc
| EDStructAccess { e; field; _ } ->
Format.fprintf fmt "@[<hv 2>%a%a@,%a%a%a@]" (lhs exprc) e punctuation "."
punctuation "\"" IdentName.format_t field punctuation "\""
punctuation "\"" Ident.format_t field punctuation "\""
| EStruct { name; fields } ->
if StructField.Map.is_empty fields then (
punctuation fmt "{";
@ -665,6 +668,7 @@ let rec expr_aux :
Format.pp_close_box fmt ();
punctuation fmt "}";
Format.pp_close_box fmt ()
| ECustom _ -> Format.pp_print_string fmt "<obj>"
let rec colors =
let open Ocolor_types in

9
compiler/shared_ast/program.ml
View File

@ -28,6 +28,15 @@ let fold_left_exprs ~f ~init { code_items; decl_ctx = _ } =
let fold_right_exprs ~f ~init { code_items; decl_ctx = _ } =
Scope.fold_right ~f:(fun e _ acc -> f e acc) ~init code_items
let empty_ctx =
{
ctx_enums = EnumName.Map.empty;
ctx_structs = StructName.Map.empty;
ctx_struct_fields = Ident.Map.empty;
ctx_scopes = ScopeName.Map.empty;
ctx_modules = Qident.Map.empty;
}
let get_scope_body { code_items; _ } scope =
match
Scope.fold_left ~init:None

4
compiler/shared_ast/program.mli
View File

@ -17,6 +17,10 @@
open Definitions
(** {2 Program declaration context helpers} *)
val empty_ctx : decl_ctx
(** {2 Transformations} *)
val map_exprs :

53
compiler/shared_ast/qident.ml Normal file
View File

@ -0,0 +1,53 @@
(* This file is part of the Catala compiler, a specification language for tax
and social benefits computation rules. Copyright (C) 2023 Inria, contributor:
Louis Gesbert <louis.gesbert@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. *)
(** This module defines module names and path accesses, used to refer to
separate compilation units *)
open Catala_utils
type modname = string
type ident = string
type path = modname list
type t = path * ident
let compare_path = List.compare String.compare
let equal_path = List.equal String.equal
let compare (p1, i1) (p2, i2) =
match compare_path p1 p2 with 0 -> String.compare i1 i2 | n -> n
let equal (p1, i1) (p2, i2) = equal_path p1 p2 && String.equal i1 i2
module Ord = struct
type nonrec t = t
let compare = compare
end
module Set = Set.Make (Ord)
module Map = Map.Make (Ord)
let format_modname ppf m = Format.fprintf ppf "@{<blue>%s@}" m
let format_path ppf p =
let pp_sep ppf () = Format.fprintf ppf "@{<cyan>.@}" in
Format.pp_print_list ~pp_sep format_modname ppf p;
pp_sep ppf ()
let format ppf (p, i) =
format_path ppf p;
Format.pp_print_string ppf i

36
compiler/shared_ast/qident.mli Normal file
View File

@ -0,0 +1,36 @@
(* This file is part of the Catala compiler, a specification language for tax
and social benefits computation rules. Copyright (C) 2023 Inria, contributor:
Louis Gesbert <louis.gesbert@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. *)
(** This module defines module names and path accesses, used to refer to
separate compilation units. *)
type modname = string
(** Expected to be a uident (i.e. start with an uppercase letter) *)
type ident = string
(** Expected to be a lident (i.e. start with a lowercase letter) *)
type path = modname list
type t = path * ident
val compare_path : path -> path -> int
val equal_path : path -> path -> bool
val compare : t -> t -> int
val equal : t -> t -> bool
val format : Format.formatter -> t -> unit
module Set : Set.S with type elt = t
module Map : Map.S with type key = t

1
compiler/shared_ast/shared_ast.ml
View File

@ -16,6 +16,7 @@
include Definitions
module Var = Var
module Qident = Qident
module Type = Type
module Operator = Operator
module Expr = Expr

17
compiler/shared_ast/typing.ml
View File

@ -458,7 +458,7 @@ and typecheck_expr_top_down :
in
let field =
let candidate_structs =
try A.IdentName.Map.find field ctx.ctx_struct_fields
try A.Ident.Map.find field ctx.ctx_struct_fields
with Not_found ->
Message.raise_spanned_error
(Expr.mark_pos context_mark)
@ -610,6 +610,16 @@ and typecheck_expr_top_down :
"Variable %s not found in the current context" (Bindlib.name_of v)
in
Expr.evar (Var.translate v) (mark_with_tau_and_unify tau')
| A.EExternal eref ->
let ty =
try Qident.Map.find eref ctx.ctx_modules
with Not_found ->
Message.raise_spanned_error pos_e
"Could not resolve the reference to %a.@ Make sure the corresponding \
module was properly loaded?"
Qident.format eref
in
Expr.eexternal eref (mark_with_tau_and_unify (ast_to_typ ty))
| A.ELit lit -> Expr.elit lit (ty_mark (lit_type lit))
| A.ETuple es ->
let tys = List.map (fun _ -> unionfind (TAny (Any.fresh ()))) es in
@ -787,6 +797,11 @@ and typecheck_expr_top_down :
List.map (typecheck_expr_top_down ~leave_unresolved ctx env cell_type) es
in
Expr.earray es' mark
| A.ECustom { obj; targs; tret } ->
let mark =
mark_with_tau_and_unify (ast_to_typ (A.TArrow (targs, tret), Expr.pos e))
in
Expr.ecustom obj targs tret mark
let wrap ctx f e =
try f e

4
compiler/surface/ast.ml
View File

@ -735,7 +735,7 @@ type top_def = {
topdef_args : (lident Mark.pos * base_typ Mark.pos) list Mark.pos option;
(** Empty list if this is not a function *)
topdef_type : typ;
topdef_expr : expression;
topdef_expr : expression option;
}
[@@deriving
visitors
@ -869,6 +869,8 @@ type law_structure =
}]
type program = {
program_interfaces :
((Shared_ast.Qident.path[@opaque]) * code_item Mark.pos) list;
program_items : law_structure list;
program_source_files : (string[@opaque]) list;
}

127
compiler/surface/parser.messages
View File

@ -238,9 +238,9 @@ source_file: BEGIN_CODE DECLARATION YEAR
## code_item -> DECLARATION . STRUCT UIDENT COLON list(addpos(struct_scope)) [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION . SCOPE UIDENT COLON nonempty_list(addpos(scope_decl_item)) [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION . ENUM UIDENT COLON list(addpos(enum_decl_line)) [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION . lident CONTENT typ_data DEPENDS separated_nonempty_list(COMMA,var_content) DEFINED_AS expression [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION . lident CONTENT typ_data DEPENDS LPAREN separated_nonempty_list(COMMA,var_content) RPAREN DEFINED_AS expression [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION . lident CONTENT typ_data DEFINED_AS expression [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION . lident CONTENT typ_data DEPENDS separated_nonempty_list(COMMA,var_content) option(opt_def) [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION . lident CONTENT typ_data DEPENDS LPAREN separated_nonempty_list(COMMA,var_content) RPAREN option(opt_def) [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION . lident CONTENT typ_data option(opt_def) [ SCOPE END_CODE DECLARATION ]
##
## The known suffix of the stack is as follows:
## DECLARATION
@ -944,7 +944,7 @@ expected the name of the scope being used
source_file: BEGIN_CODE YEAR
##
## Ends in an error in state: 394.
## Ends in an error in state: 393.
##
## source_file_item -> BEGIN_CODE . code END_CODE [ LAW_TEXT LAW_HEADING EOF BEGIN_METADATA BEGIN_DIRECTIVE BEGIN_CODE ]
##
@ -1005,8 +1005,8 @@ source_file: BEGIN_METADATA LAW_TEXT LAW_HEADING
## accurate view of the past (what has been recognized so far), they
## may provide an INCOMPLETE view of the future (what was expected next).
## In state 1, spurious reduction of production nonempty_list(LAW_TEXT) -> LAW_TEXT
## In state 383, spurious reduction of production law_text -> nonempty_list(LAW_TEXT)
## In state 384, spurious reduction of production option(law_text) -> law_text
## In state 382, spurious reduction of production law_text -> nonempty_list(LAW_TEXT)
## In state 383, spurious reduction of production option(law_text) -> law_text
##
expected some law text or code block
@ -4019,9 +4019,9 @@ source_file: BEGIN_CODE DECLARATION LIDENT YEAR
##
## Ends in an error in state: 364.
##
## code_item -> DECLARATION lident . CONTENT typ_data DEPENDS separated_nonempty_list(COMMA,var_content) DEFINED_AS expression [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION lident . CONTENT typ_data DEPENDS LPAREN separated_nonempty_list(COMMA,var_content) RPAREN DEFINED_AS expression [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION lident . CONTENT typ_data DEFINED_AS expression [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION lident . CONTENT typ_data DEPENDS separated_nonempty_list(COMMA,var_content) option(opt_def) [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION lident . CONTENT typ_data DEPENDS LPAREN separated_nonempty_list(COMMA,var_content) RPAREN option(opt_def) [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION lident . CONTENT typ_data option(opt_def) [ SCOPE END_CODE DECLARATION ]
##
## The known suffix of the stack is as follows:
## DECLARATION lident
@ -4033,9 +4033,9 @@ source_file: BEGIN_CODE DECLARATION LIDENT CONTENT YEAR
##
## Ends in an error in state: 365.
##
## code_item -> DECLARATION lident CONTENT . typ_data DEPENDS separated_nonempty_list(COMMA,var_content) DEFINED_AS expression [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION lident CONTENT . typ_data DEPENDS LPAREN separated_nonempty_list(COMMA,var_content) RPAREN DEFINED_AS expression [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION lident CONTENT . typ_data DEFINED_AS expression [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION lident CONTENT . typ_data DEPENDS separated_nonempty_list(COMMA,var_content) option(opt_def) [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION lident CONTENT . typ_data DEPENDS LPAREN separated_nonempty_list(COMMA,var_content) RPAREN option(opt_def) [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION lident CONTENT . typ_data option(opt_def) [ SCOPE END_CODE DECLARATION ]
##
## The known suffix of the stack is as follows:
## DECLARATION lident CONTENT
@ -4047,9 +4047,9 @@ source_file: BEGIN_CODE DECLARATION LIDENT CONTENT BOOLEAN YEAR
##
## Ends in an error in state: 366.
##
## code_item -> DECLARATION lident CONTENT typ_data . DEPENDS separated_nonempty_list(COMMA,var_content) DEFINED_AS expression [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION lident CONTENT typ_data . DEPENDS LPAREN separated_nonempty_list(COMMA,var_content) RPAREN DEFINED_AS expression [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION lident CONTENT typ_data . DEFINED_AS expression [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION lident CONTENT typ_data . DEPENDS separated_nonempty_list(COMMA,var_content) option(opt_def) [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION lident CONTENT typ_data . DEPENDS LPAREN separated_nonempty_list(COMMA,var_content) RPAREN option(opt_def) [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION lident CONTENT typ_data . option(opt_def) [ SCOPE END_CODE DECLARATION ]
##
## The known suffix of the stack is as follows:
## DECLARATION lident CONTENT typ_data
@ -4062,8 +4062,8 @@ source_file: BEGIN_CODE DECLARATION LIDENT CONTENT UIDENT DEPENDS YEAR
##
## Ends in an error in state: 367.
##
## code_item -> DECLARATION lident CONTENT typ_data DEPENDS . separated_nonempty_list(COMMA,var_content) DEFINED_AS expression [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION lident CONTENT typ_data DEPENDS . LPAREN separated_nonempty_list(COMMA,var_content) RPAREN DEFINED_AS expression [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION lident CONTENT typ_data DEPENDS . separated_nonempty_list(COMMA,var_content) option(opt_def) [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION lident CONTENT typ_data DEPENDS . LPAREN separated_nonempty_list(COMMA,var_content) RPAREN option(opt_def) [ SCOPE END_CODE DECLARATION ]
##
## The known suffix of the stack is as follows:
## DECLARATION lident CONTENT typ_data DEPENDS
@ -4075,7 +4075,7 @@ source_file: BEGIN_CODE DECLARATION LIDENT CONTENT UIDENT DEPENDS LPAREN YEAR
##
## Ends in an error in state: 368.
##
## code_item -> DECLARATION lident CONTENT typ_data DEPENDS LPAREN . separated_nonempty_list(COMMA,var_content) RPAREN DEFINED_AS expression [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION lident CONTENT typ_data DEPENDS LPAREN . separated_nonempty_list(COMMA,var_content) RPAREN option(opt_def) [ SCOPE END_CODE DECLARATION ]
##
## The known suffix of the stack is as follows:
## DECLARATION lident CONTENT typ_data DEPENDS LPAREN
@ -4087,7 +4087,7 @@ source_file: BEGIN_CODE DECLARATION LIDENT CONTENT UIDENT DEPENDS LPAREN LIDENT
##
## Ends in an error in state: 369.
##
## code_item -> DECLARATION lident CONTENT typ_data DEPENDS LPAREN separated_nonempty_list(COMMA,var_content) . RPAREN DEFINED_AS expression [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION lident CONTENT typ_data DEPENDS LPAREN separated_nonempty_list(COMMA,var_content) . RPAREN option(opt_def) [ SCOPE END_CODE DECLARATION ]
##
## The known suffix of the stack is as follows:
## DECLARATION lident CONTENT typ_data DEPENDS LPAREN separated_nonempty_list(COMMA,var_content)
@ -4109,7 +4109,7 @@ source_file: BEGIN_CODE DECLARATION LIDENT CONTENT UIDENT DEPENDS LPAREN LIDENT
##
## Ends in an error in state: 370.
##
## code_item -> DECLARATION lident CONTENT typ_data DEPENDS LPAREN separated_nonempty_list(COMMA,var_content) RPAREN . DEFINED_AS expression [ SCOPE END_CODE DECLARATION ]
## code_item -> DECLARATION lident CONTENT typ_data DEPENDS LPAREN separated_nonempty_list(COMMA,var_content) RPAREN . option(opt_def) [ SCOPE END_CODE DECLARATION ]
##
## The known suffix of the stack is as follows:
## DECLARATION lident CONTENT typ_data DEPENDS LPAREN separated_nonempty_list(COMMA,var_content) RPAREN
@ -4121,46 +4121,14 @@ source_file: BEGIN_CODE DECLARATION LIDENT CONTENT UIDENT DEPENDS LPAREN LIDENT
##
## Ends in an error in state: 371.
##
## code_item -> DECLARATION lident CONTENT typ_data DEPENDS LPAREN separated_nonempty_list(COMMA,var_content) RPAREN DEFINED_AS . expression [ SCOPE END_CODE DECLARATION ]
## option(opt_def) -> DEFINED_AS . expression [ SCOPE END_CODE DECLARATION ]
##
## The known suffix of the stack is as follows:
## DECLARATION lident CONTENT typ_data DEPENDS LPAREN separated_nonempty_list(COMMA,var_content) RPAREN DEFINED_AS
## DEFINED_AS
##
expected an expression
source_file: BEGIN_CODE DECLARATION LIDENT CONTENT UIDENT DEPENDS LPAREN LIDENT CONTENT UIDENT RPAREN DEFINED_AS FALSE YEAR
##
## Ends in an error in state: 372.
##
## code_item -> DECLARATION lident CONTENT typ_data DEPENDS LPAREN separated_nonempty_list(COMMA,var_content) RPAREN DEFINED_AS expression . [ SCOPE END_CODE DECLARATION ]
## expression -> expression . DOT qlident [ XOR WITH SCOPE PLUSPLUS PLUS OR OF NOT_EQUAL MULT MINUS LESSER_EQUAL LESSER GREATER_EQUAL GREATER FOR EQUAL END_CODE DOT DIV DECLARATION CONTAINS AND ]
## expression -> expression . OF funcall_args [ XOR WITH SCOPE PLUSPLUS PLUS OR OF NOT_EQUAL MULT MINUS LESSER_EQUAL LESSER GREATER_EQUAL GREATER FOR EQUAL END_CODE DOT DIV DECLARATION CONTAINS AND ]
## expression -> expression . WITH constructor_binding [ XOR WITH SCOPE PLUSPLUS PLUS OR OF NOT_EQUAL MULT MINUS LESSER_EQUAL LESSER GREATER_EQUAL GREATER FOR EQUAL END_CODE DOT DIV DECLARATION CONTAINS AND ]
## expression -> expression . CONTAINS expression [ XOR WITH SCOPE PLUSPLUS PLUS OR OF NOT_EQUAL MULT MINUS LESSER_EQUAL LESSER GREATER_EQUAL GREATER FOR EQUAL END_CODE DOT DIV DECLARATION CONTAINS AND ]
## expression -> expression . FOR lident AMONG expression [ XOR WITH SCOPE PLUSPLUS PLUS OR OF NOT_EQUAL MULT MINUS LESSER_EQUAL LESSER GREATER_EQUAL GREATER FOR EQUAL END_CODE DOT DIV DECLARATION CONTAINS AND ]
## expression -> expression . MULT expression [ XOR WITH SCOPE PLUSPLUS PLUS OR OF NOT_EQUAL MULT MINUS LESSER_EQUAL LESSER GREATER_EQUAL GREATER FOR EQUAL END_CODE DOT DIV DECLARATION CONTAINS AND ]
## expression -> expression . DIV expression [ XOR WITH SCOPE PLUSPLUS PLUS OR OF NOT_EQUAL MULT MINUS LESSER_EQUAL LESSER GREATER_EQUAL GREATER FOR EQUAL END_CODE DOT DIV DECLARATION CONTAINS AND ]
## expression -> expression . PLUS expression [ XOR WITH SCOPE PLUSPLUS PLUS OR OF NOT_EQUAL MULT MINUS LESSER_EQUAL LESSER GREATER_EQUAL GREATER FOR EQUAL END_CODE DOT DIV DECLARATION CONTAINS AND ]
## expression -> expression . MINUS expression [ XOR WITH SCOPE PLUSPLUS PLUS OR OF NOT_EQUAL MULT MINUS LESSER_EQUAL LESSER GREATER_EQUAL GREATER FOR EQUAL END_CODE DOT DIV DECLARATION CONTAINS AND ]
## expression -> expression . PLUSPLUS expression [ XOR WITH SCOPE PLUSPLUS PLUS OR OF NOT_EQUAL MULT MINUS LESSER_EQUAL LESSER GREATER_EQUAL GREATER FOR EQUAL END_CODE DOT DIV DECLARATION CONTAINS AND ]
## expression -> expression . LESSER expression [ XOR WITH SCOPE PLUSPLUS PLUS OR OF NOT_EQUAL MULT MINUS LESSER_EQUAL LESSER GREATER_EQUAL GREATER FOR EQUAL END_CODE DOT DIV DECLARATION CONTAINS AND ]
## expression -> expression . LESSER_EQUAL expression [ XOR WITH SCOPE PLUSPLUS PLUS OR OF NOT_EQUAL MULT MINUS LESSER_EQUAL LESSER GREATER_EQUAL GREATER FOR EQUAL END_CODE DOT DIV DECLARATION CONTAINS AND ]
## expression -> expression . GREATER expression [ XOR WITH SCOPE PLUSPLUS PLUS OR OF NOT_EQUAL MULT MINUS LESSER_EQUAL LESSER GREATER_EQUAL GREATER FOR EQUAL END_CODE DOT DIV DECLARATION CONTAINS AND ]
## expression -> expression . GREATER_EQUAL expression [ XOR WITH SCOPE PLUSPLUS PLUS OR OF NOT_EQUAL MULT MINUS LESSER_EQUAL LESSER GREATER_EQUAL GREATER FOR EQUAL END_CODE DOT DIV DECLARATION CONTAINS AND ]
## expression -> expression . EQUAL expression [ XOR WITH SCOPE PLUSPLUS PLUS OR OF NOT_EQUAL MULT MINUS LESSER_EQUAL LESSER GREATER_EQUAL GREATER FOR EQUAL END_CODE DOT DIV DECLARATION CONTAINS AND ]
## expression -> expression . NOT_EQUAL expression [ XOR WITH SCOPE PLUSPLUS PLUS OR OF NOT_EQUAL MULT MINUS LESSER_EQUAL LESSER GREATER_EQUAL GREATER FOR EQUAL END_CODE DOT DIV DECLARATION CONTAINS AND ]
## expression -> expression . AND expression [ XOR WITH SCOPE PLUSPLUS PLUS OR OF NOT_EQUAL MULT MINUS LESSER_EQUAL LESSER GREATER_EQUAL GREATER FOR EQUAL END_CODE DOT DIV DECLARATION CONTAINS AND ]
## expression -> expression . OR expression [ XOR WITH SCOPE PLUSPLUS PLUS OR OF NOT_EQUAL MULT MINUS LESSER_EQUAL LESSER GREATER_EQUAL GREATER FOR EQUAL END_CODE DOT DIV DECLARATION CONTAINS AND ]
## expression -> expression . XOR expression [ XOR WITH SCOPE PLUSPLUS PLUS OR OF NOT_EQUAL MULT MINUS LESSER_EQUAL LESSER GREATER_EQUAL GREATER FOR EQUAL END_CODE DOT DIV DECLARATION CONTAINS AND ]
## expression -> expression . FOR lident AMONG expression SUCH THAT expression [ XOR WITH SCOPE PLUSPLUS PLUS OR OF NOT_EQUAL MULT MINUS LESSER_EQUAL LESSER GREATER_EQUAL GREATER FOR EQUAL END_CODE DOT DIV DECLARATION CONTAINS AND ]
##
## The known suffix of the stack is as follows:
## DECLARATION lident CONTENT typ_data DEPENDS LPAREN separated_nonempty_list(COMMA,var_content) RPAREN DEFINED_AS expression
##
expected a binary operator continuing the expression, or a keyword ending the expression and starting the next item
source_file: BEGIN_CODE DECLARATION LIDENT CONTENT UIDENT DEPENDS LIDENT YEAR
##
## Ends in an error in state: 305.
@ -4212,44 +4180,10 @@ source_file: BEGIN_CODE DECLARATION LIDENT CONTENT UIDENT DEPENDS LIDENT CONTENT
expected the definition of another argument in the form '<var> content <type>'
source_file: BEGIN_CODE DECLARATION LIDENT CONTENT UIDENT DEPENDS LIDENT CONTENT UIDENT RPAREN
##
## Ends in an error in state: 373.
##
## code_item -> DECLARATION lident CONTENT typ_data DEPENDS separated_nonempty_list(COMMA,var_content) . DEFINED_AS expression [ SCOPE END_CODE DECLARATION ]
##
## The known suffix of the stack is as follows:
## DECLARATION lident CONTENT typ_data DEPENDS separated_nonempty_list(COMMA,var_content)
##
## WARNING: This example involves spurious reductions.
## This implies that, although the LR(1) items shown above provide an
## accurate view of the past (what has been recognized so far), they
## may provide an INCOMPLETE view of the future (what was expected next).
## In state 21, spurious reduction of production quident -> UIDENT
## In state 30, spurious reduction of production primitive_typ -> quident
## In state 296, spurious reduction of production typ_data -> primitive_typ
## In state 307, spurious reduction of production separated_nonempty_list(COMMA,var_content) -> lident CONTENT typ_data
##
expected 'equals <expression>'
source_file: BEGIN_CODE DECLARATION LIDENT CONTENT UIDENT DEPENDS LIDENT CONTENT UIDENT DEFINED_AS YEAR
##
## Ends in an error in state: 374.
##
## code_item -> DECLARATION lident CONTENT typ_data DEPENDS separated_nonempty_list(COMMA,var_content) DEFINED_AS . expression [ SCOPE END_CODE DECLARATION ]
##
## The known suffix of the stack is as follows:
## DECLARATION lident CONTENT typ_data DEPENDS separated_nonempty_list(COMMA,var_content) DEFINED_AS
##
expected an expression
source_file: BEGIN_CODE DECLARATION LIDENT CONTENT UIDENT DEPENDS LIDENT CONTENT UIDENT DEFINED_AS FALSE YEAR
##
## Ends in an error in state: 375.
## Ends in an error in state: 372.
##
## code_item -> DECLARATION lident CONTENT typ_data DEPENDS separated_nonempty_list(COMMA,var_content) DEFINED_AS expression . [ SCOPE END_CODE DECLARATION ]
## expression -> expression . DOT qlident [ XOR WITH SCOPE PLUSPLUS PLUS OR OF NOT_EQUAL MULT MINUS LESSER_EQUAL LESSER GREATER_EQUAL GREATER FOR EQUAL END_CODE DOT DIV DECLARATION CONTAINS AND ]
## expression -> expression . OF funcall_args [ XOR WITH SCOPE PLUSPLUS PLUS OR OF NOT_EQUAL MULT MINUS LESSER_EQUAL LESSER GREATER_EQUAL GREATER FOR EQUAL END_CODE DOT DIV DECLARATION CONTAINS AND ]
## expression -> expression . WITH constructor_binding [ XOR WITH SCOPE PLUSPLUS PLUS OR OF NOT_EQUAL MULT MINUS LESSER_EQUAL LESSER GREATER_EQUAL GREATER FOR EQUAL END_CODE DOT DIV DECLARATION CONTAINS AND ]
@ -4270,16 +4204,17 @@ source_file: BEGIN_CODE DECLARATION LIDENT CONTENT UIDENT DEPENDS LIDENT CONTENT
## expression -> expression . OR expression [ XOR WITH SCOPE PLUSPLUS PLUS OR OF NOT_EQUAL MULT MINUS LESSER_EQUAL LESSER GREATER_EQUAL GREATER FOR EQUAL END_CODE DOT DIV DECLARATION CONTAINS AND ]
## expression -> expression . XOR expression [ XOR WITH SCOPE PLUSPLUS PLUS OR OF NOT_EQUAL MULT MINUS LESSER_EQUAL LESSER GREATER_EQUAL GREATER FOR EQUAL END_CODE DOT DIV DECLARATION CONTAINS AND ]
## expression -> expression . FOR lident AMONG expression SUCH THAT expression [ XOR WITH SCOPE PLUSPLUS PLUS OR OF NOT_EQUAL MULT MINUS LESSER_EQUAL LESSER GREATER_EQUAL GREATER FOR EQUAL END_CODE DOT DIV DECLARATION CONTAINS AND ]
## option(opt_def) -> DEFINED_AS expression . [ SCOPE END_CODE DECLARATION ]
##
## The known suffix of the stack is as follows:
## DECLARATION lident CONTENT typ_data DEPENDS separated_nonempty_list(COMMA,var_content) DEFINED_AS expression
## DEFINED_AS expression
##
expected a binary operator continuing the expression, or a keyword ending the expression and starting the next item
source_file: BEGIN_DIRECTIVE YEAR
##
## Ends in an error in state: 385.
## Ends in an error in state: 384.
##
## source_file_item -> BEGIN_DIRECTIVE . LAW_INCLUDE COLON nonempty_list(DIRECTIVE_ARG) option(AT_PAGE) END_DIRECTIVE [ LAW_TEXT LAW_HEADING EOF BEGIN_METADATA BEGIN_DIRECTIVE BEGIN_CODE ]
##
@ -4291,7 +4226,7 @@ expected a directive, e.g. 'Include: <filename>'
source_file: BEGIN_DIRECTIVE LAW_INCLUDE YEAR
##
## Ends in an error in state: 386.
## Ends in an error in state: 385.
##
## source_file_item -> BEGIN_DIRECTIVE LAW_INCLUDE . COLON nonempty_list(DIRECTIVE_ARG) option(AT_PAGE) END_DIRECTIVE [ LAW_TEXT LAW_HEADING EOF BEGIN_METADATA BEGIN_DIRECTIVE BEGIN_CODE ]
##
@ -4303,7 +4238,7 @@ expected ':', then a file name or 'JORFTEXTNNNNNNNNNNNN'
source_file: BEGIN_DIRECTIVE LAW_INCLUDE COLON YEAR
##
## Ends in an error in state: 387.
## Ends in an error in state: 386.
##
## source_file_item -> BEGIN_DIRECTIVE LAW_INCLUDE COLON . nonempty_list(DIRECTIVE_ARG) option(AT_PAGE) END_DIRECTIVE [ LAW_TEXT LAW_HEADING EOF BEGIN_METADATA BEGIN_DIRECTIVE BEGIN_CODE ]
##
@ -4315,7 +4250,7 @@ expected a file name or 'JORFTEXTNNNNNNNNNNNN'
source_file: BEGIN_DIRECTIVE LAW_INCLUDE COLON DIRECTIVE_ARG YEAR
##
## Ends in an error in state: 388.
## Ends in an error in state: 387.
##
## nonempty_list(DIRECTIVE_ARG) -> DIRECTIVE_ARG . [ END_DIRECTIVE AT_PAGE ]
## nonempty_list(DIRECTIVE_ARG) -> DIRECTIVE_ARG . nonempty_list(DIRECTIVE_ARG) [ END_DIRECTIVE AT_PAGE ]
@ -4328,7 +4263,7 @@ expected a page specification in the form '@p.<number>', or a newline
source_file: BEGIN_DIRECTIVE LAW_INCLUDE COLON DIRECTIVE_ARG AT_PAGE YEAR
##
## Ends in an error in state: 392.
## Ends in an error in state: 391.
##
## source_file_item -> BEGIN_DIRECTIVE LAW_INCLUDE COLON nonempty_list(DIRECTIVE_ARG) option(AT_PAGE) . END_DIRECTIVE [ LAW_TEXT LAW_HEADING EOF BEGIN_METADATA BEGIN_DIRECTIVE BEGIN_CODE ]
##
@ -4340,7 +4275,7 @@ expected a newline
source_file: LAW_HEADING YEAR
##
## Ends in an error in state: 397.
## Ends in an error in state: 396.
##
## source_file -> source_file_item . source_file [ # ]
##

7
compiler/surface/parser.mly
View File

@ -658,15 +658,18 @@ let code_item :=
| DECLARATION ; name = lident ;
CONTENT ; ty = addpos(typ) ;
args = depends_stance ;
DEFINED_AS ; e = expression ; {
topdef_expr = option(opt_def) ; {
Topdef {
topdef_name = name;
topdef_args = args;
topdef_type = type_from_args args ty;
topdef_expr = e;
topdef_expr;
}
}
let opt_def ==
| DEFINED_AS; e = expression; <>
let code :=
| code = list(addpos(code_item)) ; <>

48
compiler/surface/parser_driver.ml
View File

@ -291,6 +291,7 @@ let rec parse_source_file
(match input with Some input -> close_in input | None -> ());
let program = expand_includes source_file_name commands language in
{
program_interfaces = [];
program_items = program.Ast.program_items;
program_source_files = source_file_name :: program.Ast.program_source_files;
}
@ -309,6 +310,7 @@ and expand_includes
let sub_source = Filename.concat source_dir (Mark.remove sub_source) in
let includ_program = parse_source_file (FileName sub_source) language in
{
program_interfaces = [];
Ast.program_source_files =
acc.Ast.program_source_files @ includ_program.program_source_files;
Ast.program_items =
@ -316,27 +318,71 @@ and expand_includes
}
| Ast.LawHeading (heading, commands') ->
let {
Ast.program_interfaces = _;
Ast.program_items = commands';
Ast.program_source_files = new_sources;
} =
expand_includes source_file commands' language
in
{
Ast.program_interfaces = [];
Ast.program_source_files = acc.Ast.program_source_files @ new_sources;
Ast.program_items =
acc.Ast.program_items @ [Ast.LawHeading (heading, commands')];
}
| i -> { acc with Ast.program_items = acc.Ast.program_items @ [i] })
{ Ast.program_source_files = []; Ast.program_items = [] }
{
Ast.program_interfaces = [];
Ast.program_source_files = [];
Ast.program_items = [];
}
commands
(** {2 Handling interfaces} *)
let get_interface program =
let rec filter acc = function
| Ast.LawInclude _ -> acc
| Ast.LawHeading (_, str) -> List.fold_left filter acc str
| Ast.LawText _ -> acc
| Ast.CodeBlock (code, _, true) ->
List.fold_left
(fun acc -> function
| Ast.ScopeUse _, _ -> acc
| ((Ast.ScopeDecl _ | StructDecl _ | EnumDecl _), _) as e -> e :: acc
| Ast.Topdef def, m ->
(Ast.Topdef { def with topdef_expr = None }, m) :: acc)
acc code
| Ast.CodeBlock (_, _, false) ->
(* Non-metadata blocks are ignored *)
acc
in
List.fold_left filter [] program.Ast.program_items
let qualify_interface path code_items =
List.map (fun item -> path, item) code_items
(** {1 API} *)
let add_interface source_file language path program =
let interface =
parse_source_file source_file language
|> get_interface
|> qualify_interface path
in
{
program with
Ast.program_interfaces =
List.append interface program.Ast.program_interfaces;
}
let parse_top_level_file
(source_file : Pos.input_file)
(language : Cli.backend_lang) : Ast.program =
let program = parse_source_file source_file language in
let interface = get_interface program in
{
program with
Ast.program_items = law_struct_list_to_tree program.Ast.program_items;
Ast.program_interfaces = qualify_interface [] interface;
}

9
compiler/surface/parser_driver.mli
View File

@ -19,4 +19,13 @@
open Catala_utils
val add_interface :
Pos.input_file ->
Cli.backend_lang ->
Shared_ast.Qident.path ->
Ast.program ->
Ast.program
(** Reads only declarations in metadata in the supplied input file, and add them
to the given program *)
val parse_top_level_file : Pos.input_file -> Cli.backend_lang -> Ast.program

1
compiler/verification/z3backend.real.ml
View File

@ -656,6 +656,7 @@ and translate_expr (ctx : context) (vc : typed expr) : context * Expr.expr =
of a match. It actually corresponds to applying an accessor to an enum,
the corresponding Z3 expression was previously stored in the context *)
ctx, e)
| EExternal _ -> failwith "[Z3 encoding] EExternal unsupported"
| EStruct _ -> failwith "[Z3 encoding] EStruct unsupported"
| EStructAccess { e; field; name } ->
let ctx, z3_struct = find_or_create_struct ctx name in

39
examples/Makefile.common.mk
View File

@ -6,8 +6,8 @@ LATEXMK?=latexmk
CURR_DIR=examples/$(shell basename $(shell pwd))/
CATALA=cd ../../; _build/default/compiler/catala.exe \
$(CATALA_OPTS) --language=$(CATALA_LANG)
CATALA=cd ../../; _build/default/compiler/catala.exe
CATALA_OPTS := $(CATALA_OPTS) --language=$(CATALA_LANG)
PLUGIN_DIR=_build/default/compiler/plugins
@ -20,49 +20,43 @@ help : ../Makefile.common.mk
#> SCOPE=<ScopeName> <target_file>.run : Runs the interpeter for the scope of the file
%.run: %.catala_$(CATALA_LANG)
@$(CATALA) Makefile $(CURR_DIR)$<
$(CATALA) \
Interpret \
@$(CATALA) Makefile $(CATALA_OPTS) $(CURR_DIR)$<
$(CATALA) Interpret $(CATALA_OPTS) \
-s $(SCOPE) \
$(CURR_DIR)$<
#> <target_file>.ml : Compiles the file to OCaml
%.ml: %.catala_$(CATALA_LANG)
@$(CATALA) Makefile $(CURR_DIR)$<
$(CATALA) \
OCaml \
@$(CATALA) Makefile $(CATALA_OPTS) $(CURR_DIR)$<
$(CATALA) OCaml $(CATALA_OPTS) \
$(CURR_DIR)$<
#> <target_file>_api_web.ml : Compiles the file to OCaml + generates the API web
%_api_web.ml: %.catala_$(CATALA_LANG)
@$(CATALA) Makefile $(CURR_DIR)$<
$(CATALA) \
api_web \
@$(CATALA) Makefile $(CATALA_OPTS) $(CURR_DIR)$<
$(CATALA) api_web $(CATALA_OPTS) \
--plugin-dir=$(PLUGIN_DIR) \
$(CURR_DIR)$<
#> SCOPE=<ScopeName> <target_file>_api_web.ml : Generates the JSON schema
%_schema.json: %.catala_$(CATALA_LANG)
@$(CATALA) Makefile $(CURR_DIR)$<
$(CATALA) \
json_schema \
@$(CATALA) Makefile $(CATALA_OPTS) $(CURR_DIR)$<
$(CATALA) json_schema $(CATALA_OPTS) \
--plugin-dir=$(PLUGIN_DIR) \
-s $(SCOPE) \
$(CURR_DIR)$<
#> <target_file>.py : Compiles the file to Python
%.py: %.catala_$(CATALA_LANG)
@$(CATALA) Makefile $(CURR_DIR)$<
$(CATALA) \
Python \
@$(CATALA) Makefile $(CATALA_OPTS) $(CURR_DIR)$<
$(CATALA) Python $(CATALA_OPTS) \
$(CURR_DIR)$<
#> <target_file>.tex : Weaves the file to LaTeX
%.tex: %.catala_$(CATALA_LANG)
@$(CATALA) Makefile $(CURR_DIR)$<
$(CATALA) \
@$(CATALA) Makefile $(CATALA_OPTS) $(CURR_DIR)$<
$(CATALA) LaTeX $(CATALA_OPTS) \
--wrap \
LaTeX \
$(CURR_DIR)$<
#> <target_file>.pdf : Weaves the file to PDF (via XeLaTeX)
@ -71,10 +65,9 @@ help : ../Makefile.common.mk
#> <target_file>.html : Weaves the file to HTML
%.html: %.catala_$(CATALA_LANG)
@$(CATALA) Makefile $(CURR_DIR)$<
$(CATALA) \
@$(CATALA) Makefile $(CATALA_OPTS) $(CURR_DIR)$<
$(CATALA) HTML $(CATALA_OPTS) \
--wrap \
HTML \
$(CURR_DIR)$<
%.spellok: %.catala_$(CATALA_LANG) ../whitelist.$(CATALA_LANG)

20
runtimes/ocaml/runtime.ml
View File

@ -737,3 +737,23 @@ module Oper = struct
end
include Oper
type hash = string
let modules_table : (string, hash) Hashtbl.t = Hashtbl.create 13
let values_table : (string list * string, Obj.t) Hashtbl.t = Hashtbl.create 13
let register_module modname values hash =
Hashtbl.add modules_table modname hash;
List.iter (fun (id, v) -> Hashtbl.add values_table ([modname], id) v) values
let check_module m h = String.equal (Hashtbl.find modules_table m) h
let lookup_value qid =
try Hashtbl.find values_table qid
with Not_found ->
failwith
("Could not resolve reference to "
^ String.concat "." (fst qid)
^ "."
^ snd qid)

18
runtimes/ocaml/runtime.mli
View File

@ -385,3 +385,21 @@ module Oper : sig
end
include module type of Oper
(** Modules API *)
type hash = string
val register_module : string -> (string * Obj.t) list -> hash -> unit
(** Registers a module by the given name defining the given bindings. Required
for evaluation to be able to access the given values. The last argument is
expected to be a hash of the source file and the Catala version, and will in
time be used to ensure that the module and the interface are in sync *)
val check_module : string -> hash -> bool
(** Returns [true] if it has been registered with the correct hash, [false] if
there is a hash mismatch.
@raise Not_found if the module does not exist at all *)
val lookup_value : string list * string -> Obj.t

7
tests/test_scope/good/191_fix_record_name_confusion.catala_en
View File

@ -17,12 +17,14 @@ scope ScopeB:
```catala-test-inline
$ catala OCaml -O
(** This file has been generated by the Catala compiler, do not edit! *)
open Runtime_ocaml.Runtime
[@@@ocaml.warning "-4-26-27-32-41-42"]
module ScopeA = struct
type t = {a: bool}
end
@ -58,4 +60,9 @@ let scope_b (scope_b_in: ScopeBIn.t) : ScopeB.t =
start_line=8; start_column=10; end_line=8; end_column=11;
law_headings=["Article"]})) in
{ScopeB.a = a_}
let () =
Runtime_ocaml.Runtime.register_module "191_fix_record_name_confusion"
[ "ScopeA", Obj.repr scope_a;
"ScopeB", Obj.repr scope_b ]
"todo-module-hash"
```