diff options
Diffstat (limited to 'plugins/extraction/ocaml.ml')
| -rw-r--r-- | plugins/extraction/ocaml.ml | 26 |
1 files changed, 12 insertions, 14 deletions
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 75fb35192b..e7004fe9af 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -229,12 +229,7 @@ let rec pp_expr par env args = and pp_a1 = pp_expr false env [] a1 and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in hv 0 (apply2 (pp_letin pp_id pp_a1 pp_a2)) - | MLglob r -> - (try - let args = List.skipn (projection_arity r) args in - let record = List.hd args in - pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args) - with e when CErrors.noncritical e -> apply (pp_global Term r)) + | MLglob r -> apply (pp_global Term r) | MLfix (i,ids,defs) -> let ids',env' = push_vars (List.rev (Array.to_list ids)) env in pp_fix par env' i (Array.of_list (List.rev ids'),defs) args @@ -324,10 +319,14 @@ and pp_record_proj par env typ t pv args = let n = List.length ids in let no_patvar a = not (List.exists (ast_occurs_itvl 1 n) a) in let rel_i,a = match body with - | MLrel i when i <= n -> i,[] - | MLapp(MLrel i, a) when i<=n && no_patvar a -> i,a + | MLrel i | MLmagic(MLrel i) when i <= n -> i,[] + | MLapp(MLrel i, a) | MLmagic(MLapp(MLrel i, a)) + | MLapp(MLmagic(MLrel i), a) when i<=n && no_patvar a -> i,a | _ -> raise Impossible in + let magic = + match body with MLmagic _ | MLapp(MLmagic _, _) -> true | _ -> false + in let rec lookup_rel i idx = function | Prel j :: l -> if Int.equal i j then idx else lookup_rel i (idx+1) l | Pwild :: l -> lookup_rel i (idx+1) l @@ -343,7 +342,10 @@ and pp_record_proj par env typ t pv args = let pp_args = (List.map (pp_expr true env' []) a) @ args in let pp_head = pp_expr true env [] t ++ str "." ++ pp_field r fields idx in - pp_apply pp_head par pp_args + if magic then + pp_apply (str "Obj.magic") par (pp_head :: pp_args) + else + pp_apply pp_head par pp_args and pp_record_pat (fields, args) = str "{ " ++ @@ -579,14 +581,10 @@ let pp_decl = function | Dterm (r, a, t) -> let def = if is_custom r then str (" = " ^ find_custom r) - else if is_projection r then - (prvect str (Array.make (projection_arity r) " _")) ++ - str " x = x." else pp_function (empty_env ()) a in let name = pp_global Term r in - let postdef = if is_projection r then name else mt () in - pp_val name t ++ hov 0 (str "let " ++ name ++ def ++ postdef) + pp_val name t ++ hov 0 (str "let " ++ name ++ def ++ mt ()) | Dfix (rv,defs,typs) -> pp_Dfix (rv,defs,typs) |