diff options
Diffstat (limited to 'src/Print.ml')
-rw-r--r-- | src/Print.ml | 73 |
1 files changed, 44 insertions, 29 deletions
diff --git a/src/Print.ml b/src/Print.ml index 18227c61..d2101dae 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -784,7 +784,7 @@ module LlbcAst = struct PC.type_ctx_to_adt_variant_to_string_fun type_decls in let var_id_to_string vid = - let var = V.VarId.nth fdef.locals vid in + let var = V.VarId.nth (Option.get fdef.body).locals vid in var_to_string var in let adt_field_names = PC.type_ctx_to_adt_field_names_fun type_decls in @@ -1062,41 +1062,56 @@ module LlbcAst = struct "<" ^ String.concat "," (List.append regions types) ^ ">" in - (* Arguments *) - let inputs = List.tl def.locals in - let inputs, _aux_locals = Collections.List.split_at inputs def.arg_count in - let args = List.combine inputs sg.inputs in - let args = - List.map - (fun (var, rty) -> var_to_string var ^ " : " ^ sty_to_string rty) - args - in - let args = String.concat ", " args in - (* Return type *) let ret_ty = sg.output in let ret_ty = if TU.ty_is_unit ret_ty then "" else " -> " ^ sty_to_string ret_ty in - (* All the locals (with erased regions) *) - let locals = - List.map - (fun var -> - indent ^ indent_incr ^ var_to_string var ^ " : " - ^ ety_to_string var.var_ty ^ ";") - def.locals - in - let locals = String.concat "\n" locals in + (* We print the declaration differently if it is opaque (no body) or transparent + * (we have access to a body) *) + match def.body with + | None -> + (* Arguments - we need to ignore the first input type which is actually + * the return type... TODO: fix that *) + let input_tys = List.tl sg.inputs in + let args = List.map sty_to_string input_tys in + let args = String.concat ", " args in + + (* Put everything together *) + indent ^ "opaque fn " ^ name ^ params ^ "(" ^ args ^ ")" ^ ret_ty + | Some body -> + (* Arguments *) + let inputs = List.tl body.locals in + let inputs, _aux_locals = + Collections.List.split_at inputs body.arg_count + in + let args = List.combine inputs sg.inputs in + let args = + List.map + (fun (var, rty) -> var_to_string var ^ " : " ^ sty_to_string rty) + args + in + let args = String.concat ", " args in + + (* All the locals (with erased regions) *) + let locals = + List.map + (fun var -> + indent ^ indent_incr ^ var_to_string var ^ " : " + ^ ety_to_string var.var_ty ^ ";") + body.locals + in + let locals = String.concat "\n" locals in - (* Body *) - let body = - statement_to_string fmt (indent ^ indent_incr) indent_incr def.body - in + (* Body *) + let body = + statement_to_string fmt (indent ^ indent_incr) indent_incr body.body + in - (* Put everything together *) - indent ^ "fn " ^ name ^ params ^ "(" ^ args ^ ")" ^ ret_ty ^ " {\n" ^ locals - ^ "\n\n" ^ body ^ "\n" ^ indent ^ "}" + (* Put everything together *) + indent ^ "fn " ^ name ^ params ^ "(" ^ args ^ ")" ^ ret_ty ^ " {\n" + ^ locals ^ "\n\n" ^ body ^ "\n" ^ indent ^ "}" end module PA = LlbcAst (* local module *) @@ -1139,7 +1154,7 @@ module Module = struct fun_name_to_string def.name in let var_id_to_string vid = - let var = V.VarId.nth def.locals vid in + let var = V.VarId.nth (Option.get def.body).locals vid in PA.var_to_string var in let adt_variant_to_string = |