From 60aa306a3f8bd8b7b2b6a8636fe66033a0a85ec0 Mon Sep 17 00:00:00 2001 From: Nicolas Chataing Date: Tue, 4 Aug 2020 12:16:28 +0200 Subject: [PATCH] Code cleanup --- src/catala/driver.ml | 3 +- src/catala/ir/context.ml | 22 ++++++------- src/catala/ir/lambda.ml | 7 ++-- src/catala/translation/firstpass.ml | 47 ++++++++++++++------------- src/catala/translation/interpreter.ml | 6 ++-- tests/test_scope/sub_scope.catala | 5 +++ 6 files changed, 49 insertions(+), 41 deletions(-) diff --git a/src/catala/driver.ml b/src/catala/driver.ml index 6cab3324..d4e673be 100644 --- a/src/catala/driver.ml +++ b/src/catala/driver.ml @@ -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; diff --git a/src/catala/ir/context.ml b/src/catala/ir/context.ml index 62d130ac..88c94b93 100644 --- a/src/catala/ir/context.ml +++ b/src/catala/ir/context.ml @@ -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 diff --git a/src/catala/ir/lambda.ml b/src/catala/ir/lambda.ml index 27879c72..8b768623 100644 --- a/src/catala/ir/lambda.ml +++ b/src/catala/ir/lambda.ml @@ -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; diff --git a/src/catala/translation/firstpass.ml b/src/catala/translation/firstpass.ml index 5b779890..e835922d 100644 --- a/src/catala/translation/firstpass.ml +++ b/src/catala/translation/firstpass.ml @@ -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 diff --git a/src/catala/translation/interpreter.ml b/src/catala/translation/interpreter.ml index c75bdff2..067d0f37 100644 --- a/src/catala/translation/interpreter.ml +++ b/src/catala/translation/interpreter.ml @@ -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 = diff --git a/tests/test_scope/sub_scope.catala b/tests/test_scope/sub_scope.catala index 695f0444..e48e9872 100644 --- a/tests/test_scope/sub_scope.catala +++ b/tests/test_scope/sub_scope.catala @@ -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