diff options
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/extraction.ml | 12 | ||||
| -rw-r--r-- | plugins/extraction/mlutil.ml | 5 | ||||
| -rw-r--r-- | plugins/extraction/ocaml.ml | 26 |
3 files changed, 15 insertions, 28 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 78c6255c1e..cca212f332 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -754,18 +754,6 @@ and extract_cst_app env sg mle mlt kn args = let la = List.length args in (* The ml arguments, already expunged from known logical ones *) let mla = make_mlargs env sg mle s args metas in - let mla = - if magic1 || lang () != Ocaml then mla - else - try - (* for better optimisations later, we discard dependent args - of projections and replace them by fake args that will be - removed during final pretty-print. *) - let l,l' = List.chop (projection_arity (GlobRef.ConstRef kn)) mla in - if not (List.is_empty l') then (List.map (fun _ -> MLexn "Proj Args") l) @ l' - else mla - with e when CErrors.noncritical e -> mla - in (* For strict languages, purely logical signatures lead to a dummy lam (except when [Kill Ktype] everywhere). So a [MLdummy] is left accordingly. *) diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 2d5872718f..baa1881297 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -1547,6 +1547,7 @@ let inline r t = not (to_keep r) (* The user DOES want to keep it *) && not (is_inline_custom r) && (to_inline r (* The user DOES want to inline it *) - || (lang () != Haskell && not (is_projection r) && - (is_recursor r || manual_inline r || inline_test r t))) + || (lang () != Haskell && + (is_projection r || is_recursor r || + manual_inline r || inline_test r t))) 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) |