diff options
| -rw-r--r-- | plugins/extraction/extract_env.ml | 10 | ||||
| -rw-r--r-- | plugins/extraction/haskell.ml | 11 | ||||
| -rw-r--r-- | plugins/extraction/miniml.mli | 4 | ||||
| -rw-r--r-- | plugins/extraction/modutil.ml | 11 | ||||
| -rw-r--r-- | plugins/extraction/ocaml.ml | 10 |
5 files changed, 21 insertions, 25 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 202d5eadd..62473855a 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -211,9 +211,8 @@ let rec extract_sfb_spec env mp = function if logical_spec s then specs else begin Visit.add_spec_deps s; (l,Spec s) :: specs end | (l,SFBmind _) :: msig -> - let kn = make_kn mp empty_dirpath l in - let mind = mind_of_kn kn in - let s = Sind (kn, extract_inductive env mind) in + let mind = make_mind mp empty_dirpath l in + let s = Sind (mind, extract_inductive env mind) in let specs = extract_sfb_spec env mp msig in if logical_spec s then specs else begin Visit.add_spec_deps s; (l,Spec s) :: specs end @@ -294,11 +293,10 @@ let rec extract_sfb env mp all = function else ms) | (l,SFBmind mib) :: msb -> let ms = extract_sfb env mp all msb in - let kn = make_kn mp empty_dirpath l in - let mind = mind_of_kn kn in + let mind = make_mind mp empty_dirpath l in let b = Visit.needed_ind mind in if all || b then - let d = Dind (kn, extract_inductive env mind) in + let d = Dind (mind, extract_inductive env mind) in if (not b) && (logical_decl d) then ms else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index ffb3baf4a..e23e3bf79 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -74,17 +74,16 @@ let pp_global k r = let kn_sig = let specif = MPfile (dirpath_of_string "Coq.Init.Specif") in - make_kn specif empty_dirpath (mk_label "sig") + make_mind specif empty_dirpath (mk_label "sig") let rec pp_type par vl t = let rec pp_rec par = function | Tmeta _ | Tvar' _ -> assert false | Tvar i -> (try pr_id (List.nth vl (pred i)) with _ -> (str "a" ++ int i)) | Tglob (r,[]) -> pp_global Type r - | Tglob (r,l) -> - if r = IndRef (mind_of_kn kn_sig,0) then + | Tglob (IndRef(kn,0),l) when kn = mk_ind "Coq.Init.Specif" "sig" -> pp_type true vl (List.hd l) - else + | Tglob (r,l) -> pp_par par (pp_global Type r ++ spc () ++ prlist_with_sep spc (pp_type true vl) l) @@ -291,8 +290,8 @@ let rec pp_ind first kn i ind = let pp_decl = function | Dind (kn,i) when i.ind_kind = Singleton -> - pp_singleton (mind_of_kn kn) i.ind_packets.(0) ++ fnl () - | Dind (kn,i) -> hov 0 (pp_ind true (mind_of_kn kn) 0 i) + pp_singleton kn i.ind_packets.(0) ++ fnl () + | Dind (kn,i) -> hov 0 (pp_ind true kn 0 i) | Dtype (r, l, t) -> if is_inline_custom r then mt () else diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index 85cd4a42b..87ddcc7b4 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -137,13 +137,13 @@ and ml_ast = (*s ML declarations. *) type ml_decl = - | Dind of kernel_name * ml_ind + | Dind of mutual_inductive * ml_ind | Dtype of global_reference * identifier list * ml_type | Dterm of global_reference * ml_ast * ml_type | Dfix of global_reference array * ml_ast array * ml_type array type ml_spec = - | Sind of kernel_name * ml_ind + | Sind of mutual_inductive * ml_ind | Stype of global_reference * identifier list * ml_type option | Sval of global_reference * ml_type diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 027b24787..3dd51ae81 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -109,15 +109,14 @@ let decl_iter_references do_term do_cons do_type = let type_iter = type_iter_references do_type and ast_iter = ast_iter_references do_term do_cons do_type in function - | Dind (kn,ind) -> ind_iter_references do_term do_cons do_type - (mind_of_kn kn) ind + | Dind (kn,ind) -> ind_iter_references do_term do_cons do_type kn ind | Dtype (r,_,t) -> do_type r; type_iter t | Dterm (r,a,t) -> do_term r; ast_iter a; type_iter t | Dfix(rv,c,t) -> Array.iter do_term rv; Array.iter ast_iter c; Array.iter type_iter t let spec_iter_references do_term do_cons do_type = function - | Sind (kn,ind) -> ind_iter_references do_term do_cons do_type (mind_of_kn kn) ind + | Sind (kn,ind) -> ind_iter_references do_term do_cons do_type kn ind | Stype (r,_,ot) -> do_type r; Option.iter (type_iter_references do_type) ot | Sval (r,t) -> do_term r; type_iter_references do_type t @@ -295,7 +294,7 @@ let reset_needed, add_needed, add_needed_mp, found_needed, is_needed = Refset'.mem r !needed || MPset.mem (modpath_of_r r) !needed_mps)) let declared_refs = function - | Dind (kn,_) -> [IndRef (mind_of_kn kn,0)] + | Dind (kn,_) -> [IndRef (kn,0)] | Dtype (r,_,_) -> [r] | Dterm (r,_,_) -> [r] | Dfix (rv,_,_) -> Array.to_list rv @@ -306,7 +305,7 @@ let declared_refs = function let compute_deps_decl = function | Dind (kn,ind) -> (* Todo Later : avoid dependencies when Extract Inductive *) - ind_iter_references add_needed add_needed add_needed (mind_of_kn kn) ind + ind_iter_references add_needed add_needed add_needed kn ind | Dtype (r,ids,t) -> if not (is_custom r) then type_iter_references add_needed t | Dterm (r,u,t) -> @@ -319,7 +318,7 @@ let compute_deps_decl = function let compute_deps_spec = function | Sind (kn,ind) -> (* Todo Later : avoid dependencies when Extract Inductive *) - ind_iter_references add_needed add_needed add_needed (mind_of_kn kn) ind + ind_iter_references add_needed add_needed add_needed kn ind | Stype (r,ids,t) -> if not (is_custom r) then Option.iter (type_iter_references add_needed) t | Sval (r,t) -> diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 5bacddb97..902e8bbb3 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -439,7 +439,7 @@ let pp_logical_ind packet = fnl () let pp_singleton kn packet = - let name = pp_global Type (IndRef (mind_of_kn kn,0)) in + let name = pp_global Type (IndRef (kn,0)) in let l = rename_tvars keywords packet.ip_vars in hov 2 (str "type " ++ pp_parameters l ++ name ++ str " =" ++ spc () ++ pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++ @@ -447,7 +447,7 @@ let pp_singleton kn packet = pr_id packet.ip_consnames.(0))) let pp_record kn projs ip_equiv packet = - let name = pp_global Type (IndRef (mind_of_kn kn,0)) in + let name = pp_global Type (IndRef (kn,0)) in let projnames = List.map (pp_global Term) projs in let l = List.combine projnames packet.ip_types.(0) in let pl = rename_tvars keywords packet.ip_vars in @@ -469,20 +469,20 @@ let pp_ind co kn ind = let init= ref (str "type ") in let names = Array.mapi (fun i p -> if p.ip_logical then mt () else - pp_global Type (IndRef (mind_of_kn kn,i))) + pp_global Type (IndRef (kn,i))) ind.ind_packets in let cnames = Array.mapi (fun i p -> if p.ip_logical then [||] else - Array.mapi (fun j _ -> pp_global Cons (ConstructRef ((mind_of_kn kn,i),j+1))) + Array.mapi (fun j _ -> pp_global Cons (ConstructRef ((kn,i),j+1))) p.ip_types) ind.ind_packets in let rec pp i = if i >= Array.length ind.ind_packets then mt () else - let ip = (mind_of_kn kn,i) in + let ip = (kn,i) in let ip_equiv = ind.ind_equiv, i in let p = ind.ind_packets.(i) in if is_custom (IndRef ip) then pp (i+1) |