diff options
author | 2001-05-09 14:37:42 +0000 | |
---|---|---|
committer | 2001-05-09 14:37:42 +0000 | |
commit | 8b0bab9313d9b26e6c9f132e82473b4db9a4832d (patch) | |
tree | dc352810c9df3c47aa0ccb9198e3e8dfd0fd3a10 | |
parent | 0f23050eaf1271fc143c8698e830d83c2240926c (diff) |
nettoyage extraction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1737 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | contrib/extraction/extraction.ml | 124 | ||||
-rw-r--r-- | contrib/extraction/test/.depend | 36 | ||||
-rw-r--r-- | kernel/inductive.mli | 1 | ||||
-rw-r--r-- | lib/util.ml | 4 | ||||
-rw-r--r-- | lib/util.mli | 1 |
5 files changed, 83 insertions, 83 deletions
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 18d420bc0..40aa1bb60 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -187,8 +187,8 @@ type binders = (name * constr) list let rec lbinders_fold f acc env = function | [] -> acc - | (n,t) :: l -> - f n t (v_of_t env t) (lbinders_fold f acc (push_rel_assum (n,t) env) l) + | (n,t) as b :: l -> + f n t (v_of_t env t) (lbinders_fold f acc (push_rel_assum b env) l) (* [sign_of_arity] transforms an arity into a signature. It is used for example with the types of inductive definitions, which are known @@ -196,7 +196,8 @@ let rec lbinders_fold f acc env = function let sign_of_lbinders = lbinders_fold (fun _ _ v a -> v::a) [] -let sign_of_arity env c = sign_of_lbinders env (List.rev (fst (decompose_prod c))) +let sign_of_arity env c = + sign_of_lbinders env (List.rev (fst (decompose_prod c))) (* [vl_of_arity] returns the list of the lambda variables tagged [info_arity] in an arity. Renaming is done. *) @@ -327,12 +328,11 @@ let _ = declare_summary "Extraction tables" Convention: the last elements of this list correspond to external products. This is used when dealing with applications *) - let rec extract_type env c = extract_type_rec env c [] [] and extract_type_rec env c vl args = - (* We accumulate the context, the arguments and the generated variable list *) + (* We accumulate the context, arguments and generated variables list *) let t = type_of env (applist (c, args)) in (* Since [ty] is an arity, there is two non-informative case: [ty] is an arity of sort [Prop], or @@ -404,22 +404,22 @@ and extract_prod_lam env (n,t,d) vl flag = let env' = push_rel_assum (n,t) env in match tag,flag with | (Info, Arity), _ -> - (* We rename before the [push_rel], to be sure that the corresponding *) - (* [lookup_rel] will be correct. *) - let id' = next_ident_away (id_of_name n) vl in - let env' = push_rel_assum (Name id', t) env in - (match extract_type_rec_info env' d (id'::vl) [] with - | Tmltype (mld, sign, vl') -> Tmltype (mld, tag::sign, vl') - | et -> et) + (* We rename before the [push_rel], to be sure that the corresponding*) + (* [lookup_rel] will be correct. *) + let id' = next_ident_away (id_of_name n) vl in + let env' = push_rel_assum (Name id', t) env in + (match extract_type_rec_info env' d (id'::vl) [] with + | Tmltype (mld, sign, vl') -> Tmltype (mld, tag::sign, vl') + | et -> et) | (Logic, Arity), _ | _, Lam -> (match extract_type_rec_info env' d vl [] with | Tmltype (mld, sign, vl') -> Tmltype (mld, tag::sign, vl') | et -> et) | (Logic, NotArity), Prod -> - (match extract_type_rec_info env' d vl [] with - | Tmltype (mld, sign, vl') -> - Tmltype (Tarr (Miniml.Tprop, mld), tag::sign, vl') - | et -> et) + (match extract_type_rec_info env' d vl [] with + | Tmltype (mld, sign, vl') -> + Tmltype (Tarr (Miniml.Tprop, mld), tag::sign, vl') + | et -> et) | (Info, NotArity), Prod -> (* It is important to treat [d] first and [t] in second. *) (* This ensures that the end of [vl] correspond to external binders. *) @@ -555,7 +555,7 @@ and abstract_constructor cp = let rec abstract rels i = function | [] -> let rels = List.rev_map (fun x -> MLrel (i-x)) rels in - if (is_singleton_constructor cp) then + if is_singleton_constructor cp then match rels with | [var]->var | _ -> assert false @@ -598,7 +598,7 @@ and extract_case env ctx ni ip c br = (* [c] has an inductive type, not an arity type *) (match extract_term env ctx c with | Rmlterm a -> - if (is_singleton_inductive ip) then + if is_singleton_inductive ip then begin (* Informative singleton case: *) (* [match c with C i -> t] becomes [let i = c' in t'] *) @@ -625,9 +625,7 @@ and extract_case env ctx ni ip c br = and extract_fix env ctx i (fi,ti,ci as recd) = let n = Array.length ti in let ti' = Array.mapi lift ti in - (* QUESTION: ou (fun i -> type_app (lift i)) a la place de lift ?*) let lb = Array.to_list (array_map2 (fun a b -> (a,b)) fi ti') in - (* QUESTION: vaut-il mieux un combine ou un (tolist o map2) *) let env' = push_rels_assum (List.rev lb) env in let ctx' = (List.rev_map (fun (_,a) -> a = NotArity) (sign_of_lbinders env lb)) @ ctx @@ -714,7 +712,7 @@ and extract_constant sp = | None -> (match v_of_t env typ with | (Info,_) -> axiom_message sp (* We really need some code here *) - | (Logic,NotArity) -> Emlterm MLprop (* Axiom ? I don't mind! *) + | (Logic,NotArity) -> Emlterm MLprop (* Axiom? I don't mind! *) | (Logic,Arity) -> Emltype (Miniml.Tarity,[],[])) (* Idem *) | Some body -> let e = extract_constr_with_type env [] body typ in @@ -767,48 +765,43 @@ and extract_mib sp = let vl = vl_of_lbinders genv lb in (* First pass: we store inductive signatures together with an initial type var list. *) - Array.iteri - (fun i ib -> - let ip = (sp,i) in - let mis = build_mis (ip,[||]) mib in - if (mis_sort mis) = (Prop Null) then - add_inductive_extraction ip Iprop - else - add_inductive_extraction ip - (Iml (sign_of_arity genv ib.mind_nf_arity, - vl_of_arity genv ib.mind_nf_arity))) - mib.mind_packets; + for i = 0 to mib.mind_ntypes - 1 do + let ip = (sp,i) in + let mis = build_mis (ip,[||]) mib in + if (mis_sort mis) = (Prop Null) then + add_inductive_extraction ip Iprop + else + let arity = mis_nf_arity mis in + add_inductive_extraction ip + (Iml (sign_of_arity genv arity, vl_of_arity genv arity)) + done; (* Second pass: we extract constructors arities and we accumulate type variables. Thanks to on-the-fly renaming in [extract_type], the [vl] list should be correct. *) let vl = - array_fold_left_i - (fun i vl packet -> + iterate_for 0 (mib.mind_ntypes - 1) + (fun i vl -> let ip = (sp,i) in let mis = build_mis (ip,[||]) mib in - if mis_sort mis = Prop Null then - begin - for j = 0 to mis_nconstr mis do - add_constructor_extraction (ip,succ j) Cprop - done; - vl - end - else - begin - array_fold_left_i - (fun j vl _ -> - let t = mis_constructor_type (succ j) mis in - let t = snd (decompose_prod_n nb t) in - match extract_type_rec_info env t vl [] with - | Tarity | Tprop -> assert false - | Tmltype (mlt, s, v) -> - let l = list_of_ml_arrows mlt in - let cp = (ip,succ j) in - add_constructor_extraction cp (Cml (l,s,nbtokeep)); - v) - vl packet.mind_nf_lc - end) - vl mib.mind_packets + if mis_sort mis = Prop Null then begin + for j = 1 to mis_nconstr mis do + add_constructor_extraction (ip,j) Cprop + done; + vl + end else + iterate_for 1 (mis_nconstr mis) + (fun j vl -> + let t = mis_constructor_type j mis in + let t = snd (decompose_prod_n nb t) in + match extract_type_rec_info env t vl [] with + | Tarity | Tprop -> assert false + | Tmltype (mlt, s, v) -> + let l = list_of_ml_arrows mlt in + let cp = (ip,j) in + add_constructor_extraction cp (Cml (l,s,nbtokeep)); + v) + vl) + vl in (* Third pass: we update the type variables list in every tables *) for i = 0 to mib.mind_ntypes-1 do @@ -834,10 +827,10 @@ and extract_mib sp = and extract_inductive_declaration sp = extract_mib sp; let ip = (sp,0) in - if (is_singleton_inductive ip) then + if is_singleton_inductive ip then let t = match lookup_constructor_extraction (ip,1) with - | Cml ([t],_,_)-> t - | _ -> assert false + | Cml ([t],_,_)-> t + | _ -> assert false in let vl = match lookup_inductive_extraction ip with | Iml (_,vl) -> vl @@ -853,18 +846,19 @@ and extract_inductive_declaration sp = | Cml (t,_,_) -> (ConstructRef cp, t) in let l = - array_fold_left_i - (fun i acc packet -> + iterate_for 0 (mib.mind_ntypes - 1) + (fun i acc -> let ip = (sp,i) in + let mis = build_mis (ip,[||]) mib in match lookup_inductive_extraction ip with | Iprop -> acc | Iml (s,vl) -> (List.rev vl, IndRef ip, Array.to_list - (Array.mapi (one_constructor ip) packet.mind_consnames)) - :: acc ) - [] mib.mind_packets + (Array.mapi (one_constructor ip) (mis_consnames mis))) + :: acc) + [] in Dtype (List.rev l, not (mind_type_finite mib 0)) diff --git a/contrib/extraction/test/.depend b/contrib/extraction/test/.depend index 9dce03ce3..4c3bd7181 100644 --- a/contrib/extraction/test/.depend +++ b/contrib/extraction/test/.depend @@ -1,7 +1,3 @@ -theories/Init/peano.cmo: theories/Init/datatypes.cmo -theories/Init/peano.cmx: theories/Init/datatypes.cmx -theories/Init/specif.cmo: theories/Init/datatypes.cmo -theories/Init/specif.cmx: theories/Init/datatypes.cmx theories/Arith/plus.cmo: theories/Init/datatypes.cmo theories/Init/specif.cmo theories/Arith/plus.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx theories/Arith/minus.cmo: theories/Init/datatypes.cmo @@ -56,6 +52,10 @@ theories/Bool/boolEq.cmo: theories/Init/datatypes.cmo \ theories/Init/specif.cmo theories/Bool/boolEq.cmx: theories/Init/datatypes.cmx \ theories/Init/specif.cmx +theories/Init/peano.cmo: theories/Init/datatypes.cmo +theories/Init/peano.cmx: theories/Init/datatypes.cmx +theories/Init/specif.cmo: theories/Init/datatypes.cmo +theories/Init/specif.cmx: theories/Init/datatypes.cmx theories/Lists/polyList.cmo: theories/Init/datatypes.cmo \ theories/Init/specif.cmo theories/Lists/polyList.cmx: theories/Init/datatypes.cmx \ @@ -126,6 +126,14 @@ theories/IntMap/adalloc.cmx: theories/IntMap/addec.cmx \ theories/IntMap/addr.cmx theories/Init/datatypes.cmx \ theories/ZArith/fast_integer.cmx theories/IntMap/map.cmx \ theories/Init/specif.cmx theories/Bool/sumbool.cmx +theories/IntMap/mapiter.cmo: theories/IntMap/addec.cmo \ + theories/IntMap/addr.cmo theories/Init/datatypes.cmo \ + theories/IntMap/map.cmo theories/Lists/polyList.cmo \ + theories/Init/specif.cmo theories/Bool/sumbool.cmo +theories/IntMap/mapiter.cmx: theories/IntMap/addec.cmx \ + theories/IntMap/addr.cmx theories/Init/datatypes.cmx \ + theories/IntMap/map.cmx theories/Lists/polyList.cmx \ + theories/Init/specif.cmx theories/Bool/sumbool.cmx theories/IntMap/lsort.cmo: theories/IntMap/addec.cmo theories/IntMap/addr.cmo \ theories/Bool/bool.cmo theories/Init/datatypes.cmo \ theories/ZArith/fast_integer.cmo theories/IntMap/mapiter.cmo \ @@ -136,14 +144,6 @@ theories/IntMap/lsort.cmx: theories/IntMap/addec.cmx theories/IntMap/addr.cmx \ theories/ZArith/fast_integer.cmx theories/IntMap/mapiter.cmx \ theories/Lists/polyList.cmx theories/Init/specif.cmx \ theories/Bool/sumbool.cmx -theories/IntMap/mapiter.cmo: theories/IntMap/addec.cmo \ - theories/IntMap/addr.cmo theories/Init/datatypes.cmo \ - theories/IntMap/map.cmo theories/Lists/polyList.cmo \ - theories/Init/specif.cmo theories/Bool/sumbool.cmo -theories/IntMap/mapiter.cmx: theories/IntMap/addec.cmx \ - theories/IntMap/addr.cmx theories/Init/datatypes.cmx \ - theories/IntMap/map.cmx theories/Lists/polyList.cmx \ - theories/Init/specif.cmx theories/Bool/sumbool.cmx theories/IntMap/mapsubset.cmo: theories/Bool/bool.cmo \ theories/Init/datatypes.cmo theories/IntMap/fset.cmo \ theories/IntMap/map.cmo theories/IntMap/mapiter.cmo @@ -176,12 +176,6 @@ theories/IntMap/maplists.cmx: theories/IntMap/addec.cmx \ theories/Init/datatypes.cmx theories/IntMap/map.cmx \ theories/IntMap/mapiter.cmx theories/Lists/polyList.cmx \ theories/Init/specif.cmx theories/Bool/sumbool.cmx -theories/ZArith/wf_Z.cmo: theories/Init/datatypes.cmo \ - theories/ZArith/fast_integer.cmo theories/Init/peano.cmo \ - theories/Init/specif.cmo -theories/ZArith/wf_Z.cmx: theories/Init/datatypes.cmx \ - theories/ZArith/fast_integer.cmx theories/Init/peano.cmx \ - theories/Init/specif.cmx theories/ZArith/fast_integer.cmo: theories/Init/datatypes.cmo \ theories/Init/peano.cmo theories/ZArith/fast_integer.cmx: theories/Init/datatypes.cmx \ @@ -190,6 +184,12 @@ theories/ZArith/zarith_aux.cmo: theories/Init/datatypes.cmo \ theories/ZArith/fast_integer.cmo theories/ZArith/zarith_aux.cmx: theories/Init/datatypes.cmx \ theories/ZArith/fast_integer.cmx +theories/ZArith/wf_Z.cmo: theories/Init/datatypes.cmo \ + theories/ZArith/fast_integer.cmo theories/Init/peano.cmo \ + theories/Init/specif.cmo +theories/ZArith/wf_Z.cmx: theories/Init/datatypes.cmx \ + theories/ZArith/fast_integer.cmx theories/Init/peano.cmx \ + theories/Init/specif.cmx theories/ZArith/zArith_dec.cmo: theories/ZArith/fast_integer.cmo \ theories/Init/specif.cmo theories/Bool/sumbool.cmo theories/ZArith/zArith_dec.cmx: theories/ZArith/fast_integer.cmx \ diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 00c0dfbdb..cb6d7b117 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -52,6 +52,7 @@ val mis_consnames : inductive_instance -> identifier array val mis_conspaths : inductive_instance -> section_path array val mis_inductive : inductive_instance -> inductive val mis_arity : inductive_instance -> types +val mis_nf_arity : inductive_instance -> types val mis_params_ctxt : inductive_instance -> rel_context val mis_sort : inductive_instance -> sorts val mis_constructor_type : int -> inductive_instance -> types diff --git a/lib/util.ml b/lib/util.ml index cd32737d2..0c3c038dd 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -434,6 +434,10 @@ let iterate f = let repeat n f x = for i = 1 to n do f x done + +let iterate_for a b f x = + let rec iterate i v = if i > b then v else iterate (succ i) (f i v) in + iterate a x (* Misc *) diff --git a/lib/util.mli b/lib/util.mli index 5122df3e8..d5976baf1 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -130,6 +130,7 @@ val matrix_transpose : 'a list list -> 'a list list val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b val iterate : ('a -> 'a) -> int -> 'a -> 'a val repeat : int -> ('a -> unit) -> 'a -> unit +val iterate_for : int -> int -> (int -> 'a -> 'a) -> 'a -> 'a (*s Misc. *) |