From 001ff72b2c17fb7b2fcaefa2555c115f0d909a03 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 28 Oct 2013 14:08:46 +0100 Subject: Initial work on reintroducing old-style polymorphism for compatibility (the stdlib does not compile entirely). --- plugins/Derive/g_derive.ml4 | 2 +- plugins/extraction/extract_env.ml | 2 +- plugins/extraction/extraction.ml | 29 +++++++++++++------------- plugins/extraction/table.ml | 2 +- plugins/funind/functional_principles_proofs.ml | 2 +- plugins/funind/indfun.ml | 2 +- plugins/funind/merge.ml | 2 +- plugins/xml/xmlcommand.ml | 2 +- 8 files changed, 21 insertions(+), 22 deletions(-) (limited to 'plugins') diff --git a/plugins/Derive/g_derive.ml4 b/plugins/Derive/g_derive.ml4 index 9137c3d28..c7db26fb8 100644 --- a/plugins/Derive/g_derive.ml4 +++ b/plugins/Derive/g_derive.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater) +let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[], false),VtLater) VERNAC COMMAND EXTEND Derive CLASSIFIED BY classify_derive_command | [ "Derive" ident(f) "From" constr(init) "Upto" constr(r) "As" ident(lemma) ] -> diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 74de31368..791294902 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -131,7 +131,7 @@ end exception Impossible let check_arity env cb = - let t = cb.const_type in + let t = Typeops.type_of_constant_type env cb.const_type in if Reduction.is_arity env t then raise Impossible let check_fix env cb i = diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 5b79f6d78..f7b677a1e 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -202,17 +202,15 @@ let parse_ind_args si args relmax = let oib_equal o1 o2 = Id.equal o1.mind_typename o2.mind_typename && List.equal eq_rel_declaration o1.mind_arity_ctxt o2.mind_arity_ctxt && - begin match o1.mind_arity, o2.mind_arity with - (* | Monomorphic {mind_user_arity=c1; mind_sort=s1}, *) - (* Monomorphic {mind_user_arity=c2; mind_sort=s2} -> *) - (* eq_constr c1 c2 && Sorts.equal s1 s2 *) - (* | ma1, ma2 -> Pervasives.(=) ma1 ma2 (\** FIXME: this one is surely wrong *\) end && *) - (* Array.equal Id.equal o1.mind_consnames o2.mind_consnames *) - | {mind_user_arity=c1; mind_sort=s1}, - {mind_user_arity=c2; mind_sort=s2} -> - eq_constr c1 c2 && Sorts.equal s1 s2 - end && - Array.equal Id.equal o1.mind_consnames o2.mind_consnames + begin + match o1.mind_arity, o2.mind_arity with + | RegularArity {mind_user_arity=c1; mind_sort=s1}, RegularArity {mind_user_arity=c2; mind_sort=s2} -> + eq_constr c1 c2 && Sorts.equal s1 s2 + | {mind_user_arity=c1; mind_sort=s1}, + {mind_user_arity=c2; mind_sort=s2} -> + eq_constr c1 c2 && Sorts.equal s1 s2 + end && + Array.equal Id.equal o1.mind_consnames o2.mind_consnames let mib_equal m1 m2 = Array.equal oib_equal m1.mind_packets m1.mind_packets && @@ -525,7 +523,8 @@ and mlt_env env r = match r with | _ -> None with Not_found -> let cb = Environ.lookup_constant kn env in - let typ = cb.const_type (* FIXME not sure if we should instantiate univs here *) in + let typ = Typeops.type_of_constant_type env cb.const_type + (* FIXME not sure if we should instantiate univs here *) in match cb.const_body with | Undef _ | OpaqueDef _ -> None | Def l_body -> @@ -553,7 +552,7 @@ let record_constant_type env kn opt_typ = lookup_type kn with Not_found -> let typ = match opt_typ with - | None -> (lookup_constant kn env).const_type + | None -> Typeops.type_of_constant_type env (lookup_constant kn env).const_type | Some typ -> typ in let mlt = extract_type env [] 1 typ [] in let schema = (type_maxvar mlt, mlt) @@ -976,7 +975,7 @@ let extract_fixpoint env vkn (fi,ti,ci) = let extract_constant env kn cb = let r = ConstRef kn in - let typ = cb.const_type in + let typ = Global.type_of_global_unsafe r in let warn_info () = if not (is_custom r) then add_info_axiom r in let warn_log () = if not (constant_has_body cb) then add_log_axiom r in @@ -1023,7 +1022,7 @@ let extract_constant env kn cb = let extract_constant_spec env kn cb = let r = ConstRef kn in - let typ = cb.const_type in + let typ = Global.type_of_global_unsafe r in match flag_of_type env typ with | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype)) | (Logic, Default) -> Sval (r, Tdummy Kother) diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 133f4ada9..c48873c80 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -816,7 +816,7 @@ let extract_constant_inline inline r ids s = match g with | ConstRef kn -> let env = Global.env () in - let typ = (Environ.lookup_constant kn env).const_type in + let typ = Global.type_of_global_unsafe (ConstRef kn) in let typ = Reduction.whd_betadeltaiota env typ in if Reduction.is_arity env typ then begin diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index a3af23dcd..f0c7b5a7f 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -964,7 +964,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in (* observe (str "eq_rhs " ++ pr_lconstr eq_rhs); *) let type_ctxt,type_of_f = decompose_prod_n_assum (nb_params + nb_args) - ((*FIXME*)f_def.const_type) in + (Typeops.type_of_constant_type (Global.env ()) (*FIXME*)f_def.const_type) in let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in let lemma_type = it_mkProd_or_LetIn eqn type_ctxt in let f_id = Label.to_id (con_label (fst (destConst f))) in diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d6ad5575b..49f833590 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -771,7 +771,7 @@ let make_graph (f_ref:global_reference) = with_full_print (fun () -> (Constrextern.extern_constr false env body, Constrextern.extern_type false env - ((*FIXNE*) c_body.const_type) + ((*FIXNE*) Typeops.type_of_constant_type env c_body.const_type) ) ) () diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index d0497f6f6..2e524a35f 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -139,7 +139,7 @@ let showind (id:Id.t) = print_string (string_of_name nm^":"); prconstr tp; print_string "\n") ib1.mind_arity_ctxt; - Printf.printf "arity :"; prconstr ib1.mind_arity.mind_user_arity; + Printf.printf "arity :"; prconstr (Inductiveops.type_of_inductive (Global.env ()) ind1); Array.iteri (fun i x -> Printf.printf"type constr %d :" i ; prconstr x) ib1.mind_user_lc diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 3d655920b..8f47859da 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -380,7 +380,7 @@ let print internal glob_ref kind xml_library_root = let val0 = Declareops.body_of_constant cb in let typ = cb.Declarations.const_type in let hyps = cb.Declarations.const_hyps in - let typ = (* Typeops.type_of_constant_type (Global.env()) *) typ in + let typ = Typeops.type_of_constant_type (Global.env()) typ in Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps | Globnames.IndRef (kn,_) -> let mib = Global.lookup_mind kn in -- cgit v1.2.3