From 2a20061cc2790eedee7fab6230fe1dd2b4d58c24 Mon Sep 17 00:00:00 2001 From: xclerc Date: Mon, 14 Oct 2013 08:32:27 +0000 Subject: Remove some uses of local modules (some were unused, some were costly). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16883 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/xml/cic2acic.ml | 231 +++++++++++++++++-------------------- plugins/xml/doubleTypeInference.ml | 15 +-- plugins/xml/xmlcommand.ml | 79 ++++++------- 3 files changed, 148 insertions(+), 177 deletions(-) (limited to 'plugins/xml') diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index a7a181aa6..f98625b64 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -36,8 +36,7 @@ let get_module_path_of_full_path path = (*CSC: Problem: here we are using the wrong (???) hypothesis that there do *) (*CSC: not exist two modules whose dir_paths are one a prefix of the other *) let remove_module_dirpath_from_dirpath ~basedir dir = - let module Ln = Libnames in - if Ln.is_dirpath_prefix_of basedir dir then + if Libnames.is_dirpath_prefix_of basedir dir then let ids = Names.DirPath.repr dir in let rec remove_firsts n l = match n,l with @@ -57,14 +56,12 @@ let remove_module_dirpath_from_dirpath ~basedir dir = let get_uri_of_var v pvars = - let module D = Decls in - let module N = Names in let rec search_in_open_sections = function [] -> Errors.error ("Variable "^v^" not found") | he::tl as modules -> - let dirpath = N.DirPath.make modules in - if List.mem (N.Id.of_string v) (D.last_section_hyps dirpath) then + let dirpath = Names.DirPath.make modules in + if List.mem (Names.Id.of_string v) (Decls.last_section_hyps dirpath) then modules else search_in_open_sections tl @@ -73,11 +70,11 @@ let get_uri_of_var v pvars = if List.mem v pvars then [] else - search_in_open_sections (N.DirPath.repr (Lib.cwd ())) + search_in_open_sections (Names.DirPath.repr (Lib.cwd ())) in "cic:" ^ List.fold_left - (fun i x -> "/" ^ N.Id.to_string x ^ i) "" path + (fun i x -> "/" ^ Names.Id.to_string x ^ i) "" path ;; type tag = @@ -120,23 +117,20 @@ let subtract l1 l2 = ;; let token_list_of_path dir id tag = - let module N = Names in let token_list_of_dirpath dirpath = - List.rev_map N.Id.to_string (N.DirPath.repr dirpath) in - token_list_of_dirpath dir @ [N.Id.to_string id ^ "." ^ (ext_of_tag tag)] + List.rev_map Names.Id.to_string (Names.DirPath.repr dirpath) in + token_list_of_dirpath dir @ [Names.Id.to_string id ^ "." ^ (ext_of_tag tag)] let token_list_of_kernel_name tag = - let module N = Names in - let module GN = Globnames in let id,dir = match tag with | Variable kn -> - N.Label.to_id (N.label kn), Lib.cwd () + Names.Label.to_id (Names.label kn), Lib.cwd () | Constant con -> - N.Label.to_id (N.con_label con), - Lib.remove_section_part (GN.ConstRef con) + Names.Label.to_id (Names.con_label con), + Lib.remove_section_part (Globnames.ConstRef con) | Inductive kn -> - N.Label.to_id (N.mind_label kn), - Lib.remove_section_part (GN.IndRef (kn,0)) + Names.Label.to_id (Names.mind_label kn), + Lib.remove_section_part (Globnames.IndRef (kn,0)) in token_list_of_path dir id (etag_of_tag tag) ;; @@ -146,8 +140,7 @@ let uri_of_kernel_name tag = "cic:/" ^ String.concat "/" tokens let uri_of_declaration id tag = - let module LN = Libnames in - let dir = LN.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ()) in + let dir = Libnames.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ()) in let tokens = token_list_of_path dir id tag in "cic:/" ^ String.concat "/" tokens @@ -322,16 +315,10 @@ let acic_of_cic_context' computeinnertypes seed ids_to_terms constr_to_ids ids_to_father_ids ids_to_inner_sorts ids_to_inner_types ?(fake_dependent_products=false) env idrefs evar_map t expectedty = - let module D = DoubleTypeInference in - let module E = Environ in - let module N = Names in - let module A = Acic in - let module T = Term in - let module V = Vars in let fresh_id' = fresh_id seed ids_to_terms constr_to_ids ids_to_father_ids in (* CSC: do you have any reasonable substitute for 503? *) let terms_to_types = Acic.CicHash.create 503 in - D.double_type_of env evar_map t expectedty terms_to_types ; + DoubleTypeInference.double_type_of env evar_map t expectedty terms_to_types ; let rec aux computeinnertypes father passed_lambdas_or_prods_or_letins env idrefs ?(subst=None,[]) tt = @@ -339,9 +326,9 @@ let acic_of_cic_context' computeinnertypes seed ids_to_terms constr_to_ids let aux' = aux computeinnertypes (Some fresh_id'') [] in let string_of_sort_family = function - Coq_sort T.InProp -> "Prop" - | Coq_sort T.InSet -> "Set" - | Coq_sort T.InType -> "Type" + Coq_sort Term.InProp -> "Prop" + | Coq_sort Term.InSet -> "Set" + | Coq_sort Term.InType -> "Type" | CProp -> "CProp" in let string_of_sort t = @@ -349,7 +336,8 @@ let acic_of_cic_context' computeinnertypes seed ids_to_terms constr_to_ids (type_as_sort env evar_map t) in let ainnertypes,innertype,innersort,expected_available = - let {D.synthesized = synthesized; D.expected = expected} = + let {DoubleTypeInference.synthesized = synthesized; + DoubleTypeInference.expected = expected} = if computeinnertypes then try Acic.CicHash.find terms_to_types tt @@ -361,11 +349,11 @@ Pp.msg_debug (Pp.(++) (Pp.str "BUG: this subterm was not visited during the doub (* type inference algorithm has not been applied. *) (* We need to refresh the universes because we are doing *) (* type inference on an already inferred type. *) - {D.synthesized = + {DoubleTypeInference.synthesized = Reductionops.nf_beta evar_map (CPropRetyping.get_type_of env evar_map (Termops.refresh_universes tt)) ; - D.expected = None} + DoubleTypeInference.expected = None} in let innersort = let synthesized_innersort = @@ -470,19 +458,19 @@ print_endline "PASSATO" ; flush stdout ; if uninst_vars_length > 0 then (* Not enough arguments provided. We must eta-expand! *) let un_args,_ = - T.decompose_prod_n uninst_vars_length + Term.decompose_prod_n uninst_vars_length (CPropRetyping.get_type_of env evar_map tt) in let eta_expanded = let arguments = - List.map (V.lift uninst_vars_length) t @ + List.map (Vars.lift uninst_vars_length) t @ Termops.rel_list 0 uninst_vars_length in Unshare.unshare - (T.lamn uninst_vars_length un_args - (T.applistc h arguments)) + (Term.lamn uninst_vars_length un_args + (Term.applistc h arguments)) in - D.double_type_of env evar_map eta_expanded + DoubleTypeInference.double_type_of env evar_map eta_expanded None terms_to_types ; Hashtbl.remove ids_to_inner_types fresh_id'' ; aux' env idrefs eta_expanded @@ -492,48 +480,48 @@ print_endline "PASSATO" ; flush stdout ; (* Now that we have all the auxiliary functions we *) (* can finally proceed with the main case analysis. *) - match T.kind_of_term tt with - T.Rel n -> + match Term.kind_of_term tt with + Term.Rel n -> let id = - match List.nth (E.rel_context env) (n - 1) with - (N.Name id,_,_) -> id - | (N.Anonymous,_,_) -> Nameops.make_ident "_" None + match List.nth (Environ.rel_context env) (n - 1) with + (Names.Name id,_,_) -> id + | (Names.Anonymous,_,_) -> Nameops.make_ident "_" None in Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; if is_a_Prop innersort && expected_available then add_inner_type fresh_id'' ; - A.ARel (fresh_id'', n, List.nth idrefs (n-1), id) - | T.Var id -> - let pvars = Termops.ids_of_named_context (E.named_context env) in - let pvars = List.map N.Id.to_string pvars in - let path = get_uri_of_var (N.Id.to_string id) pvars in + Acic.ARel (fresh_id'', n, List.nth idrefs (n-1), id) + | Term.Var id -> + let pvars = Termops.ids_of_named_context (Environ.named_context env) in + let pvars = List.map Names.Id.to_string pvars in + let path = get_uri_of_var (Names.Id.to_string id) pvars in Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; if is_a_Prop innersort && expected_available then add_inner_type fresh_id'' ; - A.AVar - (fresh_id'', path ^ "/" ^ (N.Id.to_string id) ^ ".var") - | T.Evar (n,l) -> + Acic.AVar + (fresh_id'', path ^ "/" ^ (Names.Id.to_string id) ^ ".var") + | Term.Evar (n,l) -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; if is_a_Prop innersort && expected_available then add_inner_type fresh_id'' ; - A.AEvar + Acic.AEvar (fresh_id'', n, Array.to_list (Array.map (aux' env idrefs) l)) - | T.Meta _ -> Errors.anomaly (Pp.str "Meta met during exporting to XML") - | T.Sort s -> A.ASort (fresh_id'', s) - | T.Cast (v,_, t) -> + | Term.Meta _ -> Errors.anomaly (Pp.str "Meta met during exporting to XML") + | Term.Sort s -> Acic.ASort (fresh_id'', s) + | Term.Cast (v,_, t) -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; if is_a_Prop innersort then add_inner_type fresh_id'' ; - A.ACast (fresh_id'', aux' env idrefs v, aux' env idrefs t) - | T.Prod (n,s,t) -> + Acic.ACast (fresh_id'', aux' env idrefs v, aux' env idrefs t) + | Term.Prod (n,s,t) -> let n' = match n with - N.Anonymous -> N.Anonymous + Names.Anonymous -> Names.Anonymous | _ -> - if not fake_dependent_products && V.noccurn 1 t then - N.Anonymous + if not fake_dependent_products && Vars.noccurn 1 t then + Names.Anonymous else - N.Name + Names.Name (Namegen.next_name_away n (Termops.ids_of_context env)) in Hashtbl.add ids_to_inner_sorts fresh_id'' @@ -549,7 +537,7 @@ print_endline "PASSATO" ; flush stdout ; match Term.kind_of_term (Hashtbl.find ids_to_terms father') with - T.Prod _ -> true + Term.Prod _ -> true | _ -> false in (fresh_id'', n', aux' env idrefs s):: @@ -557,20 +545,20 @@ print_endline "PASSATO" ; flush stdout ; passed_lambdas_or_prods_or_letins else []) in - let new_env = E.push_rel (n', None, s) env in + let new_env = Environ.push_rel (n', None, s) env in let new_idrefs = fresh_id''::idrefs in (match Term.kind_of_term t with - T.Prod _ -> + Term.Prod _ -> aux computeinnertypes (Some fresh_id'') new_passed_prods new_env new_idrefs t | _ -> - A.AProds (new_passed_prods, aux' new_env new_idrefs t)) - | T.Lambda (n,s,t) -> + Acic.AProds (new_passed_prods, aux' new_env new_idrefs t)) + | Term.Lambda (n,s,t) -> let n' = match n with - N.Anonymous -> N.Anonymous + Names.Anonymous -> Names.Anonymous | _ -> - N.Name (Namegen.next_name_away n (Termops.ids_of_context env)) + Names.Name (Namegen.next_name_away n (Termops.ids_of_context env)) in Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; let sourcetype = CPropRetyping.get_type_of env evar_map s in @@ -583,7 +571,7 @@ print_endline "PASSATO" ; flush stdout ; match Term.kind_of_term (Hashtbl.find ids_to_terms father') with - T.Lambda _ -> true + Term.Lambda _ -> true | _ -> false in if is_a_Prop innersort && @@ -594,10 +582,10 @@ print_endline "PASSATO" ; flush stdout ; (if father_is_lambda then passed_lambdas_or_prods_or_letins else []) in - let new_env = E.push_rel (n', None, s) env in + let new_env = Environ.push_rel (n', None, s) env in let new_idrefs = fresh_id''::idrefs in (match Term.kind_of_term t with - T.Lambda _ -> + Term.Lambda _ -> aux computeinnertypes (Some fresh_id'') new_passed_lambdas new_env new_idrefs t | _ -> @@ -606,19 +594,19 @@ print_endline "PASSATO" ; flush stdout ; (* can create nested Lambdas. Here we perform the *) (* flattening. *) match t' with - A.ALambdas (lambdas, t'') -> - A.ALambdas (lambdas@new_passed_lambdas, t'') + Acic.ALambdas (lambdas, t'') -> + Acic.ALambdas (lambdas@new_passed_lambdas, t'') | _ -> - A.ALambdas (new_passed_lambdas, t') + Acic.ALambdas (new_passed_lambdas, t') ) - | T.LetIn (n,s,t,d) -> + | Term.LetIn (n,s,t,d) -> let id = match n with - N.Anonymous -> N.Id.of_string "_X" - | N.Name id -> id + Names.Anonymous -> Names.Id.of_string "_X" + | Names.Name id -> id in let n' = - N.Name (Namegen.next_ident_away id (Termops.ids_of_context env)) + Names.Name (Namegen.next_ident_away id (Termops.ids_of_context env)) in Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; let sourcesort = @@ -634,7 +622,7 @@ print_endline "PASSATO" ; flush stdout ; match Term.kind_of_term (Hashtbl.find ids_to_terms father') with - T.LetIn _ -> true + Term.LetIn _ -> true | _ -> false in if is_a_Prop innersort then @@ -644,15 +632,15 @@ print_endline "PASSATO" ; flush stdout ; (if father_is_letin then passed_lambdas_or_prods_or_letins else []) in - let new_env = E.push_rel (n', Some s, t) env in + let new_env = Environ.push_rel (n', Some s, t) env in let new_idrefs = fresh_id''::idrefs in (match Term.kind_of_term d with - T.LetIn _ -> + Term.LetIn _ -> aux computeinnertypes (Some fresh_id'') new_passed_letins new_env new_idrefs d - | _ -> A.ALetIns + | _ -> Acic.ALetIns (new_passed_letins, aux' new_env new_idrefs d)) - | T.App (h,t) -> + | Term.App (h,t) -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; if is_a_Prop innersort then add_inner_type fresh_id'' ; @@ -669,7 +657,7 @@ print_endline "PASSATO" ; flush stdout ; (* maybe all the arguments were used for the explicit *) (* named substitution *) if residual_args_not_empty then - A.AApp (fresh_id'', h'::residual_args) + Acic.AApp (fresh_id'', h'::residual_args) else h' in @@ -679,48 +667,48 @@ print_endline "PASSATO" ; flush stdout ; explicit_substitute_and_eta_expand_if_required h (Array.to_list t) t' compute_result_if_eta_expansion_not_required - | T.Const kn -> + | Term.Const kn -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; if is_a_Prop innersort && expected_available then add_inner_type fresh_id'' ; let compute_result_if_eta_expansion_not_required _ _ = - A.AConst (fresh_id'', subst, (uri_of_kernel_name (Constant kn))) + Acic.AConst (fresh_id'', subst, (uri_of_kernel_name (Constant kn))) in let (_,subst') = subst in explicit_substitute_and_eta_expand_if_required tt [] (List.map snd subst') compute_result_if_eta_expansion_not_required - | T.Ind (kn,i) -> + | Term.Ind (kn,i) -> let compute_result_if_eta_expansion_not_required _ _ = - A.AInd (fresh_id'', subst, (uri_of_kernel_name (Inductive kn)), i) + Acic.AInd (fresh_id'', subst, (uri_of_kernel_name (Inductive kn)), i) in let (_,subst') = subst in explicit_substitute_and_eta_expand_if_required tt [] (List.map snd subst') compute_result_if_eta_expansion_not_required - | T.Construct ((kn,i),j) -> + | Term.Construct ((kn,i),j) -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; if is_a_Prop innersort && expected_available then add_inner_type fresh_id'' ; let compute_result_if_eta_expansion_not_required _ _ = - A.AConstruct + Acic.AConstruct (fresh_id'', subst, (uri_of_kernel_name (Inductive kn)), i, j) in let (_,subst') = subst in explicit_substitute_and_eta_expand_if_required tt [] (List.map snd subst') compute_result_if_eta_expansion_not_required - | T.Case ({T.ci_ind=(kn,i)},ty,term,a) -> + | Term.Case ({Term.ci_ind=(kn,i)},ty,term,a) -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; if is_a_Prop innersort then add_inner_type fresh_id'' ; let a' = Array.fold_right (fun x i -> (aux' env idrefs x)::i) a [] in - A.ACase + Acic.ACase (fresh_id'', (uri_of_kernel_name (Inductive kn)), i, aux' env idrefs ty, aux' env idrefs term, a') - | T.Fix ((ai,i),(f,t,b)) -> + | Term.Fix ((ai,i),(f,t,b)) -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; if is_a_Prop innersort then add_inner_type fresh_id'' ; let fresh_idrefs = @@ -732,29 +720,29 @@ print_endline "PASSATO" ; flush stdout ; let ids = ref (Termops.ids_of_context env) in Array.map (function - N.Anonymous -> Errors.error "Anonymous fix function met" - | N.Name id as n -> - let res = N.Name (Namegen.next_name_away n !ids) in + Names.Anonymous -> Errors.error "Anonymous fix function met" + | Names.Name id as n -> + let res = Names.Name (Namegen.next_name_away n !ids) in ids := id::!ids ; res ) f in - A.AFix (fresh_id'', i, + Acic.AFix (fresh_id'', i, Array.fold_right (fun (id,fi,ti,bi,ai) i -> let fi' = match fi with - N.Name fi -> fi - | N.Anonymous -> Errors.error "Anonymous fix function met" + Names.Name fi -> fi + | Names.Anonymous -> Errors.error "Anonymous fix function met" in (id, fi', ai, aux' env idrefs ti, - aux' (E.push_rec_types (f',t,b) env) new_idrefs bi)::i) + aux' (Environ.push_rec_types (f',t,b) env) new_idrefs bi)::i) (Array.mapi (fun j x -> (fresh_idrefs.(j),x,t.(j),b.(j),ai.(j))) f' ) [] ) - | T.CoFix (i,(f,t,b)) -> + | Term.CoFix (i,(f,t,b)) -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; if is_a_Prop innersort then add_inner_type fresh_id'' ; let fresh_idrefs = @@ -766,24 +754,24 @@ print_endline "PASSATO" ; flush stdout ; let ids = ref (Termops.ids_of_context env) in Array.map (function - N.Anonymous -> Errors.error "Anonymous fix function met" - | N.Name id as n -> - let res = N.Name (Namegen.next_name_away n !ids) in + Names.Anonymous -> Errors.error "Anonymous fix function met" + | Names.Name id as n -> + let res = Names.Name (Namegen.next_name_away n !ids) in ids := id::!ids ; res ) f in - A.ACoFix (fresh_id'', i, + Acic.ACoFix (fresh_id'', i, Array.fold_right (fun (id,fi,ti,bi) i -> let fi' = match fi with - N.Name fi -> fi - | N.Anonymous -> Errors.error "Anonymous fix function met" + Names.Name fi -> fi + | Names.Anonymous -> Errors.error "Anonymous fix function met" in (id, fi', aux' env idrefs ti, - aux' (E.push_rec_types (f',t,b) env) new_idrefs bi)::i) + aux' (Environ.push_rec_types (f',t,b) env) new_idrefs bi)::i) (Array.mapi (fun j x -> (fresh_idrefs.(j),x,t.(j),b.(j)) ) f' ) [] @@ -807,7 +795,6 @@ let acic_of_cic_context metasenv context t = *) let acic_object_of_cic_object sigma obj = - let module A = Acic in let ids_to_terms = Hashtbl.create 503 in let constr_to_ids = Acic.CicHash.create 503 in let ids_to_father_ids = Hashtbl.create 503 in @@ -837,23 +824,23 @@ let acic_object_of_cic_object sigma obj = in let aobj = match obj with - A.Constant (id,bo,ty,params) -> + Acic.Constant (id,bo,ty,params) -> let abo = match bo with None -> None | Some bo' -> Some (acic_term_of_cic_term' bo' (Some ty)) in let aty = acic_term_of_cic_term' ty None in - A.AConstant (fresh_id (),id,abo,aty,params) - | A.Variable (id,bo,ty,params) -> + Acic.AConstant (fresh_id (),id,abo,aty,params) + | Acic.Variable (id,bo,ty,params) -> let abo = match bo with Some bo -> Some (acic_term_of_cic_term' bo (Some ty)) | None -> None in let aty = acic_term_of_cic_term' ty None in - A.AVariable (fresh_id (),id,abo,aty,params) - | A.CurrentProof (id,conjectures,bo,ty) -> + Acic.AVariable (fresh_id (),id,abo,aty,params) + | Acic.CurrentProof (id,conjectures,bo,ty) -> let aconjectures = List.map (function (i,canonical_context,term) as conjecture -> @@ -870,7 +857,7 @@ let acic_object_of_cic_object sigma obj = Hashtbl.add ids_to_hypotheses hid hyp ; incr hypotheses_seed ; match decl_or_def with - A.Decl t -> + Acic.Decl t -> let final_env,final_idrefs,atl = aux (Environ.push_rel (Names.Name n,None,t) env) new_idrefs tl @@ -878,8 +865,8 @@ let acic_object_of_cic_object sigma obj = let at = acic_term_of_cic_term_context' env idrefs sigma t None in - final_env,final_idrefs,(hid,(n,A.Decl at))::atl - | A.Def (t,ty) -> + final_env,final_idrefs,(hid,(n,Acic.Decl at))::atl + | Acic.Def (t,ty) -> let final_env,final_idrefs,atl = aux (Environ.push_rel (Names.Name n,Some t,ty) env) @@ -890,10 +877,10 @@ let acic_object_of_cic_object sigma obj = in let dummy_never_used = let s = "dummy_never_used" in - A.ARel (s,99,s,Names.Id.of_string s) + Acic.ARel (s,99,s,Names.Id.of_string s) in final_env,final_idrefs, - (hid,(n,A.Def (at,dummy_never_used)))::atl + (hid,(n,Acic.Def (at,dummy_never_used)))::atl in aux env [] canonical_context in @@ -905,8 +892,8 @@ let acic_object_of_cic_object sigma obj = ) conjectures in let abo = acic_term_of_cic_term_context' env [] sigma bo (Some ty) in let aty = acic_term_of_cic_term_context' env [] sigma ty None in - A.ACurrentProof (fresh_id (),id,aconjectures,abo,aty) - | A.InductiveDefinition (tys,params,paramsno) -> + Acic.ACurrentProof (fresh_id (),id,aconjectures,abo,aty) + | Acic.InductiveDefinition (tys,params,paramsno) -> let env' = List.fold_right (fun (name,_,arity,_) env -> @@ -930,7 +917,7 @@ let acic_object_of_cic_object sigma obj = (id,name,inductive,aty,acons) ) (List.rev idrefs) tys in - A.AInductiveDefinition (fresh_id (),atys,params,paramsno) + Acic.AInductiveDefinition (fresh_id (),atys,params,paramsno) in aobj,ids_to_terms,constr_to_ids,ids_to_father_ids,ids_to_inner_sorts, ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml index 5a3880b01..d54308165 100644 --- a/plugins/xml/doubleTypeInference.ml +++ b/plugins/xml/doubleTypeInference.ml @@ -16,20 +16,17 @@ type types = {synthesized : Term.types ; expected : Term.types option};; let cprop = - let module N = Names in - N.make_con - (N.MPfile + Names.make_con + (Names.MPfile (Libnames.dirpath_of_string "CoRN.algebra.CLogic")) - (N.DirPath.empty) - (N.Label.make "CProp") + (Names.DirPath.empty) + (Names.Label.make "CProp") ;; let whd_betadeltaiotacprop env _evar_map ty = - let module C = Closure in - let module CR = C.RedFlags in (*** CProp is made Opaque ***) - let flags = CR.red_sub C.betadeltaiota (CR.fCONST cprop) in - C.whd_val (C.create_clos_infos flags env) (C.inject ty) + let flags = Closure.RedFlags.red_sub Closure.betadeltaiota (Closure.RedFlags.fCONST cprop) in + Closure.whd_val (Closure.create_clos_infos flags env) (Closure.inject ty) ;; diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index d065ba61a..abd6b3b73 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -53,7 +53,6 @@ let filter_params pvars hyps = (* better unless this function is reimplemented in the Declare *) (* module. *) let search_variables () = - let module N = Names in let cwd = Lib.cwd () in let cwdsp = Libnames.make_path cwd (Names.Id.of_string "dummy") in let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in @@ -62,8 +61,8 @@ let search_variables () = [] -> [] | he::tl as modules -> let one_section_variables = - let dirpath = N.DirPath.make (modules @ N.DirPath.repr modulepath) in - let t = List.map N.Id.to_string (Decls.last_section_hyps dirpath) in + let dirpath = Names.DirPath.make (modules @ Names.DirPath.repr modulepath) in + let t = List.map Names.Id.to_string (Decls.last_section_hyps dirpath) in [he,t] in one_section_variables @ aux tl @@ -88,7 +87,6 @@ let rec join_dirs cwd = ;; let filename_of_path xml_library_root tag = - let module N = Names in match xml_library_root with None -> None (* stdout *) | Some xml_library_root' -> @@ -109,11 +107,10 @@ let types_filename_of_filename = ;; let theory_filename xml_library_root = - let module N = Names in match xml_library_root with None -> None (* stdout *) | Some xml_library_root' -> - let toks = List.map N.Id.to_string (N.DirPath.repr (Lib.library_dp ())) in + let toks = List.map Names.Id.to_string (Names.DirPath.repr (Lib.library_dp ())) in (* theory from A/B/C/F.v goes into A/B/C/F.theory *) let alltoks = List.rev toks in Some (join_dirs xml_library_root' alltoks ^ ".theory") @@ -160,10 +157,9 @@ let string_list_of_named_context_list = (* Used only for variables (since for constants and mutual *) (* inductive types this information is already available. *) let find_hyps t = - let module T = Term in let rec aux l t = - match T.kind_of_term t with - T.Var id when not (List.mem id l) -> + match Term.kind_of_term t with + Term.Var id when not (List.mem id l) -> let (_,bo,ty) = Global.lookup_named id in let boids = match bo with @@ -171,27 +167,27 @@ let find_hyps t = | None -> l in id::(aux boids ty) - | T.Var _ - | T.Rel _ - | T.Meta _ - | T.Evar _ - | T.Sort _ -> l - | T.Cast (te,_, ty) -> aux (aux l te) ty - | T.Prod (_,s,t) -> aux (aux l s) t - | T.Lambda (_,s,t) -> aux (aux l s) t - | T.LetIn (_,s,_,t) -> aux (aux l s) t - | T.App (he,tl) -> Array.fold_left (fun i x -> aux i x) (aux l he) tl - | T.Const con -> + | Term.Var _ + | Term.Rel _ + | Term.Meta _ + | Term.Evar _ + | Term.Sort _ -> l + | Term.Cast (te,_, ty) -> aux (aux l te) ty + | Term.Prod (_,s,t) -> aux (aux l s) t + | Term.Lambda (_,s,t) -> aux (aux l s) t + | Term.LetIn (_,s,_,t) -> aux (aux l s) t + | Term.App (he,tl) -> Array.fold_left (fun i x -> aux i x) (aux l he) tl + | Term.Const con -> let hyps = (Global.lookup_constant con).Declarations.const_hyps in map_and_filter l hyps @ l - | T.Ind ind - | T.Construct (ind,_) -> + | Term.Ind ind + | Term.Construct (ind,_) -> let hyps = (fst (Global.lookup_inductive ind)).Declarations.mind_hyps in map_and_filter l hyps @ l - | T.Case (_,t1,t2,b) -> + | Term.Case (_,t1,t2,b) -> Array.fold_left (fun i x -> aux i x) (aux (aux l t1) t2) b - | T.Fix (_,(_,tys,bodies)) - | T.CoFix (_,(_,tys,bodies)) -> + | Term.Fix (_,(_,tys,bodies)) + | Term.CoFix (_,(_,tys,bodies)) -> let r = Array.fold_left (fun i x -> aux i x) l tys in Array.fold_left (fun i x -> aux i x) r bodies and map_and_filter l = @@ -339,15 +335,14 @@ let kind_of_constant kn = ;; let kind_of_global r = - let module Gn = Globnames in match r with - | Gn.IndRef kn | Gn.ConstructRef (kn,_) -> + | Globnames.IndRef kn | Globnames.ConstructRef (kn,_) -> let isrecord = try let _ = Recordops.lookup_projections kn in Declare.KernelSilent with Not_found -> Declare.KernelVerbose in kind_of_inductive isrecord (fst kn) - | Gn.VarRef id -> kind_of_variable id - | Gn.ConstRef kn -> kind_of_constant kn + | Globnames.VarRef id -> kind_of_variable id + | Globnames.ConstRef kn -> kind_of_constant kn ;; let print_object_kind uri (xmltag,variation) = @@ -366,39 +361,31 @@ let print_object_kind uri (xmltag,variation) = (* form of the definition (all the parameters are *) (* lambda-abstracted, but the object can still refer to variables) *) let print internal glob_ref kind xml_library_root = - let module D = Declareops in - let module De = Declare in - let module G = Global in - let module N = Names in - let module Nt = Nametab in - let module T = Term in - let module X = Xml in - let module Gn = Globnames in (* Variables are the identifiers of the variables in scope *) let variables = search_variables () in let tag,obj = match glob_ref with - Gn.VarRef id -> + Globnames.VarRef id -> (* this kn is fake since it is not provided by Coq *) let kn = Lib.make_kn id in - let (_,body,typ) = G.lookup_named id in + let (_,body,typ) = Global.lookup_named id in Cic2acic.Variable kn,mk_variable_obj id body typ - | Gn.ConstRef kn -> - let id = N.Label.to_id (N.con_label kn) in - let cb = G.lookup_constant kn in - let val0 = D.body_of_constant cb in + | Globnames.ConstRef kn -> + let id = Names.Label.to_id (Names.con_label kn) in + let cb = Global.lookup_constant kn in + 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 Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps - | Gn.IndRef (kn,_) -> - let mib = G.lookup_mind kn in + | Globnames.IndRef (kn,_) -> + let mib = Global.lookup_mind kn in let {Declarations.mind_nparams=nparams; Declarations.mind_packets=packs ; Declarations.mind_hyps=hyps; Declarations.mind_finite=finite} = mib in Cic2acic.Inductive kn,mk_inductive_obj kn mib packs variables nparams hyps finite - | Gn.ConstructRef _ -> + | Globnames.ConstructRef _ -> Errors.error ("a single constructor cannot be printed in XML") in let fn = filename_of_path xml_library_root tag in -- cgit v1.2.3