CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-11-09 01:35:56 +03:00
Code Issues Projects Releases Wiki Activity

Code cleanup

Browse Source
This commit is contained in:
Nicolas Chataing 2020-08-04 12:16:28 +02:00
parent a576682fac
commit 60aa306a3f
6 changed files with 49 additions and 41 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/catala/driver.ml
View File

@ -102,7 +102,6 @@ let driver (source_file : string) (debug : bool) (wrap_weaved_output : bool)
| Cli.Interpret -> (
try
let ctxt = Context.form_context program in
Context.print_context ctxt;
let prgm = Firstpass.translate_program_to_scope ctxt program in
Uid.UidMap.iter
(fun _uid scope ->
@ -111,7 +110,7 @@ let driver (source_file : string) (debug : bool) (wrap_weaved_output : bool)
Uid.UidMap.iter
(fun uid value ->
Printf.printf "Var %s:\t%s\n" (Uid.get_ident uid)
(Lambda.print_term ((value, Pos.no_pos), None)))
(Lambda.print_term ((value, Pos.no_pos), TDummy)))
exec_ctxt;
Printf.printf "\n")
prgm;

22
src/catala/ir/context.ml
View File

@ -47,14 +47,14 @@ type context = {
}
(** Print the context in a readable manner *)
let print_context (ctxt : context) : unit =
let print_context (ctxt : context) : string =
let rec typ_to_string = function
| Lambda.TBool -> "bool"
| Lambda.TInt -> "num"
| Lambda.TDummy -> "(.)"
| Lambda.TArrow (t1, t2) -> Printf.sprintf "%s -> (%s)" (typ_to_string t1) (typ_to_string t2)
in
let print_var (var_id : ident) (var_uid : uid) : unit =
let print_var ((var_id, var_uid) : ident * uid) : string =
let data = UidMap.find var_uid ctxt.data in
let info =
match data.uid_sort with
@ -66,17 +66,15 @@ let print_context (ctxt : context) : unit =
sub_scope_uid
| IdBinder -> Printf.sprintf "\ttyp : %s\tbinder" (typ_to_string data.uid_typ)
in
Printf.printf "%s (uid : %n)%s\n" var_id var_uid info;
()
Printf.sprintf "%s (uid : %n)%s\n" var_id var_uid info
in
IdentMap.iter
(fun scope_ident scope_uid ->
Printf.printf "Scope %s (uid : %n):\n" scope_ident scope_uid;
IdentMap.iter print_var (UidMap.find scope_uid ctxt.scopes).var_id_to_uid;
Printf.printf "\n")
ctxt.scope_id_to_uid;
()
let print_scope ((scope_ident, scope_uid) : ident * Uid.t) : string =
Printf.sprintf "Scope %s (uid : %n):\n" scope_ident scope_uid
^ ( (UidMap.find scope_uid ctxt.scopes).var_id_to_uid |> IdentMap.bindings |> List.map print_var
|> String.concat "" )
^ Printf.sprintf "\n"
in
ctxt.scope_id_to_uid |> IdentMap.bindings |> List.map print_scope |> String.concat ""
let subscope_ident (y : string) (x : string) : string = y ^ "::" ^ x

7
src/catala/ir/lambda.ml
View File

@ -17,6 +17,7 @@ type uid = Uid.t
module UidMap = Uid.UidMap
module UidSet = Uid.UidSet
(* TDummy means the term is not typed *)
type typ = TBool | TInt | TArrow of typ * typ | TDummy
type literal = Ast.literal
@ -31,7 +32,7 @@ type binding = uid * typ
(*type enum_case = uid*)
type term = untyped_term Pos.marked * typ option
type term = untyped_term Pos.marked * typ
and untyped_term =
| EVar of uid
@ -47,7 +48,7 @@ let untype (((term, _), _) : term) : untyped_term = term
let get_pos (((_, pos), _) : term) : Pos.t = pos
let get_typ ((_, typ) : term) : typ option = typ
let get_typ ((_, typ) : term) : typ = typ
let print_literal (l : literal) : string =
match l with
@ -104,6 +105,8 @@ type justification = term
type consequence = term
(* (x,y) in ordering means that default x has precedence over default y : if both are true then x
would be choser over y *)
type default_term = {
defaults : (justification * consequence) IntMap.t;
ordering : (int * int) list;

47
src/catala/translation/firstpass.ml
View File

@ -24,13 +24,13 @@ let rec expr_to_lambda ?(subdef : Uid.t option) (scope : Uid.t) (ctxt : Context.
let rec_helper = expr_to_lambda ?subdef scope ctxt in
match expr with
| IfThenElse (e_if, e_then, e_else) ->
((EIfThenElse (rec_helper e_if, rec_helper e_then, rec_helper e_else), pos), None)
((EIfThenElse (rec_helper e_if, rec_helper e_then, rec_helper e_else), pos), TDummy)
| Binop (op, e1, e2) ->
let op_term = (Pos.same_pos_as (EOp (Binop (Pos.unmark op))) op, None) in
((EApp (op_term, [ rec_helper e1; rec_helper e2 ]), pos), None)
let op_term = (Pos.same_pos_as (EOp (Binop (Pos.unmark op))) op, TDummy) in
((EApp (op_term, [ rec_helper e1; rec_helper e2 ]), pos), TDummy)
| Unop (op, e) ->
let op_term = (Pos.same_pos_as (EOp (Unop (Pos.unmark op))) op, None) in
((EApp (op_term, [ rec_helper e ]), pos), None)
let op_term = (Pos.same_pos_as (EOp (Unop (Pos.unmark op))) op, TDummy) in
((EApp (op_term, [ rec_helper e ]), pos), TDummy)
| Literal l ->
let untyped_term =
match l with
@ -39,10 +39,10 @@ let rec expr_to_lambda ?(subdef : Uid.t option) (scope : Uid.t) (ctxt : Context.
| Bool b -> EBool b
| _ -> assert false
in
((untyped_term, pos), None)
((untyped_term, pos), TDummy)
| Ident x ->
let uid = Context.get_var_uid scope ctxt (x, pos) in
((EVar uid, pos), None)
((EVar uid, pos), TDummy)
| Dotted (e, x) -> (
(* For now we only accept dotted identifiers of the type y.x where y is a sub-scope *)
match Pos.unmark e with
@ -53,16 +53,16 @@ let rec expr_to_lambda ?(subdef : Uid.t option) (scope : Uid.t) (ctxt : Context.
(* No redefinition : take the uid from the current scope *)
let ident = subscope_ident y (Pos.unmark x) in
let uid = Context.get_var_uid scope ctxt (ident, Pos.get_position e) in
((EVar uid, pos), None)
((EVar uid, pos), TDummy)
| Some uid when uid <> sub_uid ->
(* Redefinition of a var from another scope : uid from the current scope *)
let ident = subscope_ident y (Pos.unmark x) in
let uid = Context.get_var_uid scope ctxt (ident, Pos.get_position e) in
((EVar uid, pos), None)
((EVar uid, pos), TDummy)
| Some sub_uid ->
(* Redefinition of a var from the same scope, uid from the subscope *)
let uid = Context.get_var_uid sub_uid ctxt x in
((EVar uid, pos), None) )
((EVar uid, pos), TDummy) )
| _ -> assert false )
| _ -> assert false
@ -71,7 +71,7 @@ let rec typing (ctxt : Context.context) (((t, pos), _) : Lambda.term) : Lambda.t
match t with
| EVar uid ->
let typ = Context.get_uid_typ ctxt uid in
let term = ((EVar uid, pos), Some typ) in
let term = ((EVar uid, pos), typ) in
(term, typ)
| EFun (bindings, body) ->
(* Note that given the context formation process, the binder will already be present in the
@ -90,7 +90,7 @@ let rec typing (ctxt : Context.context) (((t, pos), _) : Lambda.term) : Lambda.t
| (_, arg_t) :: args -> TArrow (arg_t, build_typ args)
in
let fun_typ = build_typ bindings in
(((EFun (bindings, body), pos), Some fun_typ), fun_typ)
(((EFun (bindings, body), pos), fun_typ), fun_typ)
| EApp (f, args) ->
let f, f_typ = typing ctxt f in
let args, args_typ = args |> List.map (typing ctxt) |> List.split in
@ -102,16 +102,16 @@ let rec typing (ctxt : Context.context) (((t, pos), _) : Lambda.term) : Lambda.t
| _ -> assert false
in
let ret_typ = check_arrow_typ f_typ args_typ in
(((EApp (f, args), pos), Some ret_typ), ret_typ)
(((EApp (f, args), pos), ret_typ), ret_typ)
| EIfThenElse (t_if, t_then, t_else) ->
let t_if, typ_if = typing ctxt t_if in
let t_then, typ_then = typing ctxt t_then in
let t_else, typ_else = typing ctxt t_else in
if typ_if <> TBool then assert false
else if typ_then <> typ_else then assert false
else (((EIfThenElse (t_if, t_then, t_else), pos), Some typ_then), typ_then)
| EInt _ | EDec _ -> (((t, pos), Some TInt), TInt)
| EBool _ -> (((t, pos), Some TBool), TBool)
else (((EIfThenElse (t_if, t_then, t_else), pos), typ_then), typ_then)
| EInt _ | EDec _ -> (((t, pos), TInt), TInt)
| EBool _ -> (((t, pos), TBool), TBool)
| EOp op ->
let typ =
match op with
@ -123,24 +123,24 @@ let rec typing (ctxt : Context.context) (((t, pos), _) : Lambda.term) : Lambda.t
| Unop Minus -> TArrow (TInt, TInt)
| Unop Not -> TArrow (TBool, TBool)
in
(((t, pos), Some typ), typ)
(((t, pos), typ), typ)
(* Translation from the parsed ast to the scope language *)
let merge_conditions (precond : Lambda.term option) (cond : Lambda.term option) : Lambda.term =
match (precond, cond) with
| Some precond, Some cond ->
let op_term = ((EOp (Binop And), Pos.no_pos), None) in
((EApp (op_term, [ precond; cond ]), Pos.no_pos), None)
let op_term = ((EOp (Binop And), Pos.no_pos), TDummy) in
((EApp (op_term, [ precond; cond ]), Pos.no_pos), TDummy)
| Some cond, None | None, Some cond -> cond
| None, None -> ((EBool true, Pos.no_pos), Some TBool)
| None, None -> ((EBool true, Pos.no_pos), TBool)
(** Process a rule from the surface language *)
let process_rule (precond : Lambda.term option) (scope : uid) (ctxt : Context.context)
(prgm : Scope.program) (rule : Ast.rule) : Scope.program =
(* For now we rule out functions *)
let () = match rule.rule_parameter with Some _ -> assert false | None -> () in
let consequence_term = ((EBool rule.rule_consequence, Pos.no_pos), Some TBool) in
let consequence_term = ((EBool rule.rule_consequence, Pos.no_pos), TBool) in
let scope_prgm = UidMap.find scope prgm in
let scope_prgm =
match Pos.unmark rule.rule_name with
@ -200,6 +200,7 @@ let process_def (precond : Lambda.term option) (scope : Uid.t) (ctxt : Context.c
let () = match def.definition_parameter with Some _ -> assert false | None -> () in
(* We first check either it is a variable or a subvariable *)
let scope_prgm = UidMap.find scope prgm in
let pos = Pos.get_position def.definition_name in
let scope_prgm =
match Pos.unmark def.definition_name with
| [ x ] ->
@ -250,7 +251,9 @@ let process_def (precond : Lambda.term option) (scope : Uid.t) (ctxt : Context.c
scope_prgm with
scope_sub_defs = UidMap.add subscope_uid y_subdef scope_prgm.scope_sub_defs;
}
| _ -> assert false
| _ ->
Cli.debug_print (Printf.sprintf "Structs are not handled yet.\n%s\n" (Pos.to_string pos));
assert false
in
UidMap.add scope scope_prgm prgm

6
src/catala/translation/interpreter.ml
View File

@ -77,7 +77,7 @@ let rec eval_term (exec_ctxt : exec_context) (term : Lambda.term) : Lambda.term
| Sub -> ( - )
| Mult -> ( * )
| Div -> ( / )
| _ -> fun _ _ -> 0
| _ -> assert false
in
let op_comp =
match binop with
@ -87,7 +87,7 @@ let rec eval_term (exec_ctxt : exec_context) (term : Lambda.term) : Lambda.term
| Gte -> ( >= )
| Eq -> ( = )
| Neq -> ( <> )
| _ -> fun _ _ -> false
| _ -> assert false
in
match binop with
| Add | Sub | Mult | Div -> EInt (op_arith i1 i2)
@ -113,7 +113,7 @@ let eval_default_term (exec_ctxt : exec_context) (term : Lambda.default_term) :
match eval_term exec_ctxt cond |> Lambda.untype with EBool b -> b | _ -> assert false)
term.defaults
in
(* Now filter out the terms that have a predecessor *)
(* Now filter out the terms that have a predecessor which justification is true *)
let module ISet = Set.Make (Int) in
let key_candidates = IntMap.fold (fun x _ -> ISet.add x) candidates ISet.empty in
let chosen_one =

5
tests/test_scope/sub_scope.catala
View File

@ -1,13 +1,18 @@
/*
declaration scope O:
context o content bool
declaration scope A:
context a content int
context b content bool
context a_base content int
context scopeO scope O
declaration scope B:
context a content int
context b content bool
context scopeA scope A
context scopeAbis scope A
scope A:
def a_base = 1