diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/PrintPure.ml | 58 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 35 |
2 files changed, 43 insertions, 50 deletions
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index b19e0be6..33082dc3 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -133,33 +133,39 @@ let type_id_to_string (fmt : type_formatter) (id : type_id) : string = | Option -> "Option" | Vec -> "Vec") -let rec ty_to_string (fmt : type_formatter) (ty : ty) : string = +let rec ty_to_string (fmt : type_formatter) (inside : bool) (ty : ty) : string = match ty with | Adt (id, tys) -> ( - let tys = List.map (ty_to_string fmt) tys in + let tys = List.map (ty_to_string fmt false) tys in match id with | Tuple -> "(" ^ String.concat " * " tys ^ ")" | AdtId _ | Assumed _ -> - let tys = if tys = [] then "" else " " ^ String.concat " " tys in - type_id_to_string fmt id ^ tys) + let tys_s = if tys = [] then "" else " " ^ String.concat " " tys in + let ty_s = type_id_to_string fmt id ^ tys_s in + if tys <> [] && inside then "(" ^ ty_s ^ ")" else ty_s) | TypeVar tv -> fmt.type_var_id_to_string tv | Bool -> "bool" | Char -> "char" | Integer int_ty -> integer_type_to_string int_ty | Str -> "str" - | Array aty -> "[" ^ ty_to_string fmt aty ^ "; ?]" - | Slice sty -> "[" ^ ty_to_string fmt sty ^ "]" + | Array aty -> "[" ^ ty_to_string fmt false aty ^ "; ?]" + | Slice sty -> "[" ^ ty_to_string fmt false sty ^ "]" | Arrow (arg_ty, ret_ty) -> - ty_to_string fmt arg_ty ^ " -> " ^ ty_to_string fmt ret_ty + let ty = + ty_to_string fmt true arg_ty ^ " -> " ^ ty_to_string fmt false ret_ty + in + if inside then "(" ^ ty ^ ")" else ty -let field_to_string fmt (f : field) : string = +let field_to_string fmt inside (f : field) : string = match f.field_name with - | None -> ty_to_string fmt f.field_ty - | Some field_name -> field_name ^ " : " ^ ty_to_string fmt f.field_ty + | None -> ty_to_string fmt inside f.field_ty + | Some field_name -> + let s = field_name ^ " : " ^ ty_to_string fmt false f.field_ty in + if inside then "(" ^ s ^ ")" else s let variant_to_string fmt (v : variant) : string = v.variant_name ^ "(" - ^ String.concat ", " (List.map (field_to_string fmt) v.fields) + ^ String.concat ", " (List.map (field_to_string fmt false) v.fields) ^ ")" let type_decl_to_string (fmt : type_formatter) (def : type_decl) : string = @@ -174,7 +180,7 @@ let type_decl_to_string (fmt : type_formatter) (def : type_decl) : string = if List.length fields > 0 then let fields = String.concat "," - (List.map (fun f -> "\n " ^ field_to_string fmt f) fields) + (List.map (fun f -> "\n " ^ field_to_string fmt false f) fields) in "struct " ^ name ^ params ^ "{" ^ fields ^ "}" else "struct " ^ name ^ params ^ "{}" @@ -193,7 +199,7 @@ let var_to_varname (v : var) : string = let var_to_string (fmt : type_formatter) (v : var) : string = let varname = var_to_varname v in - "(" ^ varname ^ " : " ^ ty_to_string fmt v.ty ^ ")" + "(" ^ varname ^ " : " ^ ty_to_string fmt false v.ty ^ ")" let rec mprojection_to_string (fmt : ast_formatter) (inside : string) (p : mprojection) : string = @@ -380,7 +386,7 @@ let adt_g_value_to_string (fmt : value_formatter) raise (Failure ("Inconsistently typed value: expected ADT type but found:" - ^ "\n- ty: " ^ ty_to_string fmt ty ^ "\n- variant_id: " + ^ "\n- ty: " ^ ty_to_string fmt false ty ^ "\n- variant_id: " ^ Print.option_to_string VariantId.to_string variant_id)) let rec typed_pattern_to_string (fmt : ast_formatter) (v : typed_pattern) : @@ -391,7 +397,7 @@ let rec typed_pattern_to_string (fmt : ast_formatter) (v : typed_pattern) : | PatVar (v, Some mp) -> let mp = "[@mplace=" ^ mplace_to_string fmt mp ^ "]" in "(" ^ var_to_varname v ^ " " ^ mp ^ " : " - ^ ty_to_string (ast_to_type_formatter fmt) v.ty + ^ ty_to_string (ast_to_type_formatter fmt) false v.ty ^ ")" | PatDummy -> "_" | PatAdt av -> @@ -403,15 +409,15 @@ let rec typed_pattern_to_string (fmt : ast_formatter) (v : typed_pattern) : let fun_sig_to_string (fmt : ast_formatter) (sg : fun_sig) : string = let ty_fmt = ast_to_type_formatter fmt in let type_params = List.map type_var_to_string sg.type_params in - let inputs = List.map (ty_to_string ty_fmt) sg.inputs in - let output = ty_to_string ty_fmt sg.output in + let inputs = List.map (ty_to_string ty_fmt false) sg.inputs in + let output = ty_to_string ty_fmt false sg.output in let all_types = List.concat [ type_params; inputs; [ output ] ] in String.concat " -> " all_types let inst_fun_sig_to_string (fmt : ast_formatter) (sg : inst_fun_sig) : string = let ty_fmt = ast_to_type_formatter fmt in - let inputs = List.map (ty_to_string ty_fmt) sg.inputs in - let output = ty_to_string ty_fmt sg.output in + let inputs = List.map (ty_to_string ty_fmt false) sg.inputs in + let output = ty_to_string ty_fmt false sg.output in let all_types = List.append inputs [ output ] in String.concat " -> " all_types @@ -551,7 +557,7 @@ and app_to_string (fmt : ast_formatter) (inside : bool) (indent : string) in (* Convert the type instantiation *) let ty_fmt = ast_to_type_formatter fmt in - let tys = List.map (ty_to_string ty_fmt) qualif.type_args in + let tys = List.map (ty_to_string ty_fmt true) qualif.type_args in (* *) (qualif_s, tys) | _ -> @@ -620,15 +626,21 @@ and loop_to_string (fmt : ast_formatter) (indent : string) (indent_incr : string) (loop : loop) : string = let indent1 = indent ^ indent_incr in let indent2 = indent1 ^ indent_incr in + let type_fmt = ast_to_type_formatter fmt in + let loop_inputs = + "fresh_vars: [" + ^ String.concat "; " (List.map (var_to_string type_fmt) loop.inputs) + ^ "]" + in let fun_end = texpression_to_string fmt false indent2 indent_incr loop.fun_end in let loop_body = texpression_to_string fmt false indent2 indent_incr loop.loop_body in - "loop {\n" ^ indent1 ^ "fun_end: {\n" ^ indent2 ^ fun_end ^ "\n" ^ indent1 - ^ "}\n" ^ indent1 ^ "loop_body: {\n" ^ indent2 ^ loop_body ^ "\n" ^ indent1 - ^ "}\n" ^ indent ^ "}" + "loop {\n" ^ indent1 ^ loop_inputs ^ "\n" ^ indent1 ^ "fun_end: {\n" ^ indent2 + ^ fun_end ^ "\n" ^ indent1 ^ "}\n" ^ indent1 ^ "loop_body: {\n" ^ indent2 + ^ loop_body ^ "\n" ^ indent1 ^ "}\n" ^ indent ^ "}" and meta_to_string (fmt : ast_formatter) (meta : meta) : string = let meta = diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index b5cb3a4d..a2b41165 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -248,7 +248,7 @@ let symbolic_value_to_string (ctx : bs_ctx) (sv : V.symbolic_value) : string = let ty_to_string (ctx : bs_ctx) (ty : ty) : string = let fmt = bs_ctx_to_pp_ast_formatter ctx in let fmt = PrintPure.ast_to_type_formatter fmt in - PrintPure.ty_to_string fmt ty + PrintPure.ty_to_string fmt false ty let type_decl_to_string (ctx : bs_ctx) (def : type_decl) : string = let type_params = def.type_params in @@ -808,7 +808,7 @@ let translate_fun_sig (fun_infos : FA.fun_info A.FunDeclId.Map.t) let sg = { type_params; inputs; output; doutputs; info } in { sg; output_names } -let bs_ctx_fresh_state_var (ctx : bs_ctx) : bs_ctx * var * typed_pattern = +let bs_ctx_fresh_state_var (ctx : bs_ctx) : bs_ctx * typed_pattern = (* Generate the fresh variable *) let id, var_counter = VarId.fresh ctx.var_counter in let state_var = @@ -818,7 +818,7 @@ let bs_ctx_fresh_state_var (ctx : bs_ctx) : bs_ctx * var * typed_pattern = (* Update the context *) let ctx = { ctx with var_counter; state_var = id } in (* Return *) - (ctx, state_var, state_pat) + (ctx, state_pat) let fresh_var (basename : string option) (ty : 'r T.ty) (ctx : bs_ctx) : bs_ctx * var = @@ -836,7 +836,7 @@ let fresh_named_var_for_symbolic_value (basename : string option) (* Generate the fresh variable *) let ctx, var = fresh_var basename sv.sv_ty ctx in (* Insert in the map *) - let sv_to_var = V.SymbolicValueId.Map.add sv.sv_id var ctx.sv_to_var in + let sv_to_var = V.SymbolicValueId.Map.add_strict sv.sv_id var ctx.sv_to_var in (* Update the context *) let ctx = { ctx with sv_to_var } in (* Return *) @@ -1419,7 +1419,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : let fuel = mk_fuel_input_as_list ctx effect_info in if effect_info.stateful then let state_var = mk_state_texpression ctx.state_var in - let ctx, _, nstate_var = bs_ctx_fresh_state_var ctx in + let ctx, nstate_var = bs_ctx_fresh_state_var ctx in (List.concat [ fuel; args; [ state_var ] ], ctx, Some nstate_var) else (List.concat [ fuel; args ], ctx, None) in @@ -1611,7 +1611,7 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs) let back_state, ctx, nstate = if effect_info.stateful then let back_state = mk_state_texpression ctx.state_var in - let ctx, _, nstate = bs_ctx_fresh_state_var ctx in + let ctx, nstate = bs_ctx_fresh_state_var ctx in ([ back_state ], ctx, Some nstate) else ([], ctx, None) in @@ -1805,7 +1805,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs) let back_state, ctx, nstate = if effect_info.stateful then let back_state = mk_state_texpression ctx.state_var in - let ctx, _, nstate = bs_ctx_fresh_state_var ctx in + let ctx, nstate = bs_ctx_fresh_state_var ctx in ([ back_state ], ctx, Some nstate) else ([], ctx, None) in @@ -2144,12 +2144,11 @@ and translate_forward_end (ectx : C.eval_ctx) * - add the fuel * - add the state input argument * - generate a fresh state variable for the returned state - * TODO: we do exactly the same thing in {!translate_function_call} *) let fuel = mk_fuel_input_as_list ctx effect_info in if effect_info.stateful then let state_var = mk_state_texpression ctx.state_var in - let ctx, _nstate_var, nstate_pat = bs_ctx_fresh_state_var ctx in + let ctx, nstate_pat = bs_ctx_fresh_state_var ctx in ( List.concat [ fuel; args; [ state_var ] ], ctx, [ nstate_pat; output_pat ] ) @@ -2257,24 +2256,6 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = (* Update the context for the loop body *) let ctx_loop = { ctx_end with inside_loop = true } in - (* We also need to introduce variables for the symbolic values which are - introduced in the fixed point (we have to filter the list of symbolic - values, to remove the not fresh ones - the fixed point introduces some - symbolic values and keeps some others)... *) - let ctx_loop = - let svl = - List.filter - (fun (sv : V.symbolic_value) -> - V.SymbolicValueId.Set.mem sv.sv_id loop.fresh_svalues) - loop.input_svalues - in - log#ldebug - (lazy - ("translate_loop:" ^ "\n- filtered svl: " - ^ (Print.list_to_string (symbolic_value_to_string ctx)) svl)); - let ctx_loop, _ = fresh_vars_for_symbolic_values svl ctx_loop in - ctx_loop - in (* Translate the loop body *) let loop_body = translate_expression loop.loop_expr ctx_loop in |