diff options
Diffstat (limited to 'checker/modops.ml')
| -rw-r--r-- | checker/modops.ml | 58 |
1 files changed, 31 insertions, 27 deletions
diff --git a/checker/modops.ml b/checker/modops.ml index b720fb62..c7ad0977 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (*i*) @@ -16,29 +18,29 @@ open Declarations (*i*) let error_not_a_constant l = - error ("\""^(Label.to_string l)^"\" is not a constant") + user_err Pp.(str ("\""^(Label.to_string l)^"\" is not a constant")) -let error_not_a_functor () = error "Application of not a functor" +let error_not_a_functor () = user_err Pp.(str "Application of not a functor") -let error_incompatible_modtypes _ _ = error "Incompatible module types" +let error_incompatible_modtypes _ _ = user_err Pp.(str "Incompatible module types") let error_not_match l _ = - error ("Signature components for label "^Label.to_string l^" do not match") + user_err Pp.(str ("Signature components for label "^Label.to_string l^" do not match")) -let error_no_such_label l = error ("No such label "^Label.to_string l) +let error_no_such_label l = user_err Pp.(str ("No such label "^Label.to_string l)) let error_no_such_label_sub l l1 = let l1 = ModPath.to_string l1 in - error ("The field "^ - Label.to_string l^" is missing in "^l1^".") + user_err Pp.(str ("The field "^ + Label.to_string l^" is missing in "^l1^".")) -let error_not_a_module_loc loc s = - user_err_loc (loc,"",str ("\""^Label.to_string s^"\" is not a module")) +let error_not_a_module_loc ?loc s = + user_err ?loc (str ("\""^Label.to_string s^"\" is not a module")) -let error_not_a_module s = error_not_a_module_loc Loc.ghost s +let error_not_a_module s = error_not_a_module_loc s let error_with_module () = - error "Unsupported 'with' constraint in module implementation" + user_err Pp.(str "Unsupported 'with' constraint in module implementation") let is_functor = function | MoreFunctor _ -> true @@ -49,7 +51,7 @@ let destr_functor = function | NoFunctor _ -> error_not_a_functor () let module_body_of_type mp mtb = - { mtb with mod_mp = mp; mod_expr = Abstract } + { mtb with mod_mp = mp; mod_expr = Abstract; mod_retroknowledge = ModBodyRK [] } let rec add_structure mp sign resolver env = let add_one env (l,elem) = @@ -83,27 +85,29 @@ let strengthen_const mp_from l cb resolver = | Def _ -> cb | _ -> let con = Constant.make2 mp_from l in - let u = - if cb.const_polymorphic then - Univ.make_abstract_instance cb.const_universes - else Univ.Instance.empty + let u = + match cb.const_universes with + | Monomorphic_const _ -> Univ.Instance.empty + | Polymorphic_const auctx -> Univ.make_abstract_instance auctx in { cb with const_body = Def (Declarations.from_val (Const (con,u))) } let rec strengthen_mod mp_from mp_to mb = if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then mb - else strengthen_body true mp_from mp_to mb + else + let mk_expr mp_to = Algebraic (NoFunctor (MEident mp_to)) in + strengthen_body mk_expr mp_from mp_to mb -and strengthen_body is_mod mp_from mp_to mb = +and strengthen_body : 'a. (_ -> 'a) -> _ -> _ -> 'a generic_module_body -> 'a generic_module_body = + fun mk_expr mp_from mp_to mb -> match mb.mod_type with | MoreFunctor _ -> mb | NoFunctor sign -> let resolve_out,sign_out = strengthen_sig mp_from sign mp_to mb.mod_delta in { mb with - mod_expr = - (if is_mod then Algebraic (NoFunctor (MEident mp_to)) else Abstract); + mod_expr = mk_expr mp_to; mod_type = NoFunctor sign_out; mod_delta = resolve_out } @@ -130,7 +134,7 @@ and strengthen_sig mp_from sign mp_to resolver = resolve_out,item::rest' let strengthen mtb mp = - strengthen_body false mtb.mod_mp mp mtb + strengthen_body ignore mtb.mod_mp mp mtb let subst_and_strengthen mb mp = strengthen_mod mb.mod_mp mp (subst_module (map_mp mb.mod_mp mp) mb) @@ -138,9 +142,9 @@ let subst_and_strengthen mb mp = let module_type_of_module mp mb = let mtb = { mb with - mod_expr = Abstract; + mod_expr = (); mod_type_alg = None; - mod_retroknowledge = [] } + mod_retroknowledge = ModTypeRK } in match mp with | Some mp -> strengthen {mtb with mod_mp = mp} mp |