diff options
Diffstat (limited to 'contrib/extraction/ocaml.ml')
| -rw-r--r-- | contrib/extraction/ocaml.ml | 118 |
1 files changed, 61 insertions, 57 deletions
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index 707ef94f..ff9cfd21 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ocaml.ml,v 1.100.2.1 2004/07/16 19:30:08 herbelin Exp $ i*) +(*i $Id: ocaml.ml,v 1.100.2.6 2005/12/01 17:01:22 letouzey Exp $ i*) (*s Production of Ocaml syntax. *) @@ -20,8 +20,6 @@ open Miniml open Mlutil open Modutil -let cons_cofix = ref Refset.empty - (*s Some utility functions. *) let pp_par par st = if par then str "(" ++ st ++ str ")" else st @@ -68,6 +66,12 @@ let sec_space_if = function true -> spc () | false -> mt () let fnl2 () = fnl () ++ fnl () +let pp_parameters l = + (pp_boxed_tuple pp_tvar l ++ space_if (l<>[])) + +let pp_string_parameters l = + (pp_boxed_tuple str l ++ space_if (l<>[])) + (*s Generic renaming issues. *) let rec rename_id id avoid = @@ -126,7 +130,7 @@ let keywords = "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ] Idset.empty -let preamble _ used_modules (mldummy,tdummy,tunknown) = +let preamble _ used_modules (mldummy,tdummy,tunknown) _ = let pp_mp = function | MPfile d -> pr_upper_id (List.hd (repr_dirpath d)) | _ -> assert false @@ -167,22 +171,33 @@ let pp_global r = let empty_env () = [], P.globals () +exception NoRecord + +let find_projections = function Record l -> l | _ -> raise NoRecord + (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses are needed or not. *) +let kn_sig = + let specif = MPfile (dirpath_of_string "Coq.Init.Specif") in + make_kn specif empty_dirpath (mk_label "sig") + let rec pp_type par vl t = let rec pp_rec par = function | Tmeta _ | Tvar' _ | Taxiom -> assert false | Tvar i -> (try pp_tvar (List.nth vl (pred i)) with _ -> (str "'a" ++ int i)) | Tglob (r,[]) -> pp_global r - | Tglob (r,l) -> pp_tuple_light pp_rec l ++ spc () ++ pp_global r + | Tglob (r,l) -> + if r = IndRef (kn_sig,0) then + pp_tuple_light pp_rec l + else + pp_tuple_light pp_rec l ++ spc () ++ pp_global r | Tarr (t1,t2) -> pp_par par (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2) | Tdummy -> str "__" | Tunknown -> str "__" - | Tcustom s -> str s in hov 0 (pp_rec par t) @@ -193,7 +208,7 @@ let rec pp_type par vl t = let expr_needs_par = function | MLlam _ -> true - | MLcase (_,[|_|]) -> false + | MLcase (_,_,[|_|]) -> false | MLcase _ -> true | _ -> false @@ -231,30 +246,32 @@ let rec pp_expr par env args = let record = List.hd args in pp_apply (record ++ str "." ++ pp_global r) par (List.tl args) with _ -> apply (pp_global r)) - | MLcons (r,[]) -> + | MLcons (Coinductive,r,[]) -> assert (args=[]); - if Refset.mem r !cons_cofix then - pp_par par (str "lazy " ++ pp_global r) - else pp_global r - | MLcons (r,args') -> - (try - let projs = find_projections (kn_of_r r) in - pp_record_pat (projs, List.map (pp_expr true env []) args') - with Not_found -> - assert (args=[]); - let tuple = pp_tuple (pp_expr true env []) args' in - if Refset.mem r !cons_cofix then - pp_par par (str "lazy (" ++ pp_global r ++ spc() ++ tuple ++str ")") - else pp_par par (pp_global r ++ spc () ++ tuple)) - | MLcase (t, pv) -> + pp_par par (str "lazy " ++ pp_global r) + | MLcons (Coinductive,r,args') -> + assert (args=[]); + let tuple = pp_tuple (pp_expr true env []) args' in + pp_par par (str "lazy (" ++ pp_global r ++ spc() ++ tuple ++str ")") + | MLcons (_,r,[]) -> + assert (args=[]); + pp_global r + | MLcons (Record projs, r, args') -> + assert (args=[]); + pp_record_pat (projs, List.map (pp_expr true env []) args') + | MLcons (_,r,args') -> + assert (args=[]); + let tuple = pp_tuple (pp_expr true env []) args' in + pp_par par (pp_global r ++ spc () ++ tuple) + | MLcase (i, t, pv) -> let r,_,_ = pv.(0) in - let expr = if Refset.mem r !cons_cofix then + let expr = if i = Coinductive then (str "Lazy.force" ++ spc () ++ pp_expr true env [] t) else (pp_expr false env [] t) in (try - let projs = find_projections (kn_of_r r) in + let projs = find_projections i in let (_, ids, c) = pv.(0) in let n = List.length ids in match c with @@ -263,17 +280,17 @@ let rec pp_expr par env args = pp_global (List.nth projs (n-i)))) | MLapp (MLrel i, a) when i <= n -> if List.exists (ast_occurs_itvl 1 n) a - then raise Not_found + then raise NoRecord else let ids,env' = push_vars (List.rev ids) env in (pp_apply (pp_expr true env [] t ++ str "." ++ pp_global (List.nth projs (n-i))) par ((List.map (pp_expr true env' []) a) @ args)) - | _ -> raise Not_found - with Not_found -> + | _ -> raise NoRecord + with NoRecord -> if Array.length pv = 1 then - let s1,s2 = pp_one_pat env pv.(0) in + let s1,s2 = pp_one_pat env i pv.(0) in apply (hv 0 (pp_par par' @@ -285,7 +302,7 @@ let rec pp_expr par env args = apply (pp_par par' (v 0 (str "match " ++ expr ++ str " with" ++ - fnl () ++ str " | " ++ pp_pat env pv)))) + fnl () ++ str " | " ++ pp_pat env i pv)))) | 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 @@ -307,21 +324,21 @@ and pp_record_pat (projs, args) = (List.combine projs args) ++ str " }" -and pp_one_pat env (r,ids,t) = +and pp_one_pat env i (r,ids,t) = let ids,env' = push_vars (List.rev ids) env in let expr = pp_expr (expr_needs_par t) env' [] t in try - let projs = find_projections (kn_of_r r) in + let projs = find_projections i in pp_record_pat (projs, List.rev_map pr_id ids), expr - with Not_found -> + with NoRecord -> let args = if ids = [] then (mt ()) else str " " ++ pp_boxed_tuple pr_id (List.rev ids) in pp_global r ++ args, expr -and pp_pat env pv = +and pp_pat env i pv = prvect_with_sep (fun () -> (fnl () ++ str " | ")) - (fun x -> let s1,s2 = pp_one_pat env x in + (fun x -> let s1,s2 = pp_one_pat env i x in hov 2 (s1 ++ str " ->" ++ spc () ++ s2)) pv and pp_function env f t = @@ -331,20 +348,17 @@ and pp_function env f t = let ktl = array_map_to_list (fun (_,l,t0) -> (List.length l,t0)) pv in not (List.exists (fun (k,t0) -> ast_occurs (k+1) t0) ktl) in - let is_not_cofix pv = - let (r,_,_) = pv.(0) in not (Refset.mem r !cons_cofix) - in match t' with - | MLcase(MLrel 1,pv) when is_not_cofix pv -> + | MLcase(i,MLrel 1,pv) when i=Standard -> if is_function pv then (f ++ pr_binding (List.rev (List.tl bl)) ++ str " = function" ++ fnl () ++ - v 0 (str " | " ++ pp_pat env' pv)) + v 0 (str " | " ++ pp_pat env' i pv)) else (f ++ pr_binding (List.rev bl) ++ str " = match " ++ pr_id (List.hd bl) ++ str " with" ++ fnl () ++ - v 0 (str " | " ++ pp_pat env' pv)) + v 0 (str " | " ++ pp_pat env' i pv)) | _ -> (f ++ pr_binding (List.rev bl) ++ str " =" ++ fnl () ++ str " " ++ @@ -384,12 +398,6 @@ let rec pp_Dfix init i ((rv,c,t) as fix) = (*s Pretty-printing of inductive types declaration. *) -let pp_parameters l = - (pp_boxed_tuple pp_tvar l ++ space_if (l<>[])) - -let pp_string_parameters l = - (pp_boxed_tuple str l ++ space_if (l<>[])) - let pp_one_ind prefix ip pl cv = let pl = rename_tvars keywords pl in let pp_constructor (r,l) = @@ -420,9 +428,8 @@ let pp_singleton kn packet = pp_comment (str "singleton inductive, whose constructor was " ++ pr_id packet.ip_consnames.(0))) -let pp_record kn packet = - let l = List.combine (find_projections kn) packet.ip_types.(0) in - let projs = find_projections kn in +let pp_record kn projs packet = + let l = List.combine projs packet.ip_types.(0) in let pl = rename_tvars keywords packet.ip_vars in str "type " ++ pp_parameters pl ++ pp_global (IndRef (kn,0)) ++ str " = { "++ hov 0 (prlist_with_sep (fun () -> str ";" ++ spc ()) @@ -466,13 +473,9 @@ let pp_ind co kn ind = let pp_mind kn i = match i.ind_info with | Singleton -> pp_singleton kn i.ind_packets.(0) - | Coinductive -> - let nop _ = () - and add r = cons_cofix := Refset.add r !cons_cofix in - decl_iter_references nop add nop (Dind (kn,i)); - pp_ind true kn i - | Record -> pp_record kn i.ind_packets.(0) - | _ -> pp_ind false kn i + | Coinductive -> pp_ind true kn i + | Record projs -> pp_record kn projs i.ind_packets.(0) + | Standard -> pp_ind false kn i let pp_decl mpl = local_mpl := mpl; @@ -481,6 +484,7 @@ let pp_decl mpl = | Dtype (r, l, t) -> if is_inline_custom r then failwith "empty phrase" else + let pp_r = pp_global r in let l = rename_tvars keywords l in let ids, def = try let ids,s = find_type_custom r in @@ -490,7 +494,7 @@ let pp_decl mpl = if t = Taxiom then str "(* AXIOM TO BE REALIZED *)" else str "=" ++ spc () ++ pp_type false l t in - hov 2 (str "type" ++ spc () ++ ids ++ pp_global r ++ + hov 2 (str "type" ++ spc () ++ ids ++ pp_r ++ spc () ++ def) | Dterm (r, a, t) -> if is_inline_custom r then failwith "empty phrase" |