diff options
Diffstat (limited to 'plugins/xml/cic2acic.ml')
| -rw-r--r-- | plugins/xml/cic2acic.ml | 942 |
1 files changed, 0 insertions, 942 deletions
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml deleted file mode 100644 index 165bf83d..00000000 --- a/plugins/xml/cic2acic.ml +++ /dev/null @@ -1,942 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) -(* \VV/ **************************************************************) -(* // * The HELM Project / The EU MoWGLI Project *) -(* * University of Bologna *) -(************************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(* *) -(* Copyright (C) 2000-2004, HELM Team. *) -(* http://helm.cs.unibo.it *) -(************************************************************************) - -(* Utility Functions *) - -exception TwoModulesWhoseDirPathIsOneAPrefixOfTheOther;; -let get_module_path_of_full_path path = - let dirpath = fst (Libnames.repr_path path) in - let modules = Lib.library_dp () :: (Library.loaded_libraries ()) in - match - List.filter - (function modul -> Libnames.is_dirpath_prefix_of modul dirpath) modules - with - [] -> - Pp.msg_warn ("Modules not supported: reference to "^ - Libnames.string_of_path path^" will be wrong"); - dirpath - | [modul] -> modul - | _ -> - raise TwoModulesWhoseDirPathIsOneAPrefixOfTheOther -;; - -(*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 - let ids = Names.repr_dirpath dir in - let rec remove_firsts n l = - match n,l with - (0,l) -> l - | (n,he::tl) -> remove_firsts (n-1) tl - | _ -> assert false - in - let ids' = - List.rev - (remove_firsts - (List.length (Names.repr_dirpath basedir)) - (List.rev ids)) - in - ids' - else Names.repr_dirpath 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 - [] -> Util.error ("Variable "^v^" not found") - | he::tl as modules -> - let dirpath = N.make_dirpath modules in - if List.mem (N.id_of_string v) (D.last_section_hyps dirpath) then - modules - else - search_in_open_sections tl - in - let path = - if List.mem v pvars then - [] - else - search_in_open_sections (N.repr_dirpath (Lib.cwd ())) - in - "cic:" ^ - List.fold_left - (fun i x -> "/" ^ N.string_of_id x ^ i) "" path -;; - -type tag = - Constant of Names.constant - | Inductive of Names.mutual_inductive - | Variable of Names.kernel_name -;; - -type etag = - TConstant - | TInductive - | TVariable -;; - -let etag_of_tag = - function - Constant _ -> TConstant - | Inductive _ -> TInductive - | Variable _ -> TVariable - -let ext_of_tag = - function - TConstant -> "con" - | TInductive -> "ind" - | TVariable -> "var" -;; - -exception FunctorsXMLExportationNotImplementedYet;; - -let subtract l1 l2 = - let l1' = List.rev (Names.repr_dirpath l1) in - let l2' = List.rev (Names.repr_dirpath l2) in - let rec aux = - function - he::tl when tl = l2' -> [he] - | he::tl -> he::(aux tl) - | [] -> assert (l2' = []) ; [] - in - Names.make_dirpath (List.rev (aux l1')) -;; - -let token_list_of_path dir id tag = - let module N = Names in - let token_list_of_dirpath dirpath = - List.rev_map N.string_of_id (N.repr_dirpath dirpath) in - token_list_of_dirpath dir @ [N.string_of_id id ^ "." ^ (ext_of_tag tag)] - -let token_list_of_kernel_name tag = - let module N = Names in - let module LN = Libnames in - let id,dir = match tag with - | Variable kn -> - N.id_of_label (N.label kn), Lib.cwd () - | Constant con -> - N.id_of_label (N.con_label con), - Lib.remove_section_part (LN.ConstRef con) - | Inductive kn -> - N.id_of_label (N.mind_label kn), - Lib.remove_section_part (LN.IndRef (kn,0)) - in - token_list_of_path dir id (etag_of_tag tag) -;; - -let uri_of_kernel_name tag = - let tokens = token_list_of_kernel_name tag in - "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 tokens = token_list_of_path dir id tag in - "cic:/" ^ String.concat "/" tokens - -(* Special functions for handling of CCorn's CProp "sort" *) - -type sort = - Coq_sort of Term.sorts_family - | CProp -;; - -let prerr_endline _ = ();; - -let family_of_term ty = - match Term.kind_of_term ty with - Term.Sort s -> Coq_sort (Term.family_of_sort s) - | Term.Const _ -> CProp (* I could check that the constant is CProp *) - | _ -> Util.anomaly "family_of_term" -;; - -module CPropRetyping = - struct - module T = Term - - let outsort env sigma t = - family_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma t) - - let rec subst_type env sigma typ = function - | [] -> typ - | h::rest -> - match T.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma typ) with - | T.Prod (na,c1,c2) -> subst_type env sigma (T.subst1 h c2) rest - | _ -> Util.anomaly "Non-functional construction" - - - let sort_of_atomic_type env sigma ft args = - let rec concl_of_arity env ar = - match T.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma ar) with - | T.Prod (na, t, b) -> concl_of_arity (Environ.push_rel (na,None,t) env) b - | T.Sort s -> Coq_sort (T.family_of_sort s) - | _ -> outsort env sigma (subst_type env sigma ft (Array.to_list args)) - in concl_of_arity env ft - -let typeur sigma metamap = - let rec type_of env cstr= - match Term.kind_of_term cstr with - | T.Meta n -> - (try T.strip_outer_cast (List.assoc n metamap) - with Not_found -> Util.anomaly "type_of: this is not a well-typed term") - | T.Rel n -> - let (_,_,ty) = Environ.lookup_rel n env in - T.lift n ty - | T.Var id -> - (try - let (_,_,ty) = Environ.lookup_named id env in - ty - with Not_found -> - Util.anomaly ("type_of: variable "^(Names.string_of_id id)^" unbound")) - | T.Const c -> - let cb = Environ.lookup_constant c env in - Typeops.type_of_constant_type env (cb.Declarations.const_type) - | T.Evar ev -> Evd.existential_type sigma ev - | T.Ind ind -> Inductiveops.type_of_inductive env ind - | T.Construct cstr -> Inductiveops.type_of_constructor env cstr - | T.Case (_,p,c,lf) -> - let Inductiveops.IndType(_,realargs) = - try Inductiveops.find_rectype env sigma (type_of env c) - with Not_found -> Util.anomaly "type_of: Bad recursive type" in - let t = Reductionops.whd_beta sigma (T.applist (p, realargs)) in - (match Term.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma (type_of env t)) with - | T.Prod _ -> Reductionops.whd_beta sigma (T.applist (t, [c])) - | _ -> t) - | T.Lambda (name,c1,c2) -> - T.mkProd (name, c1, type_of (Environ.push_rel (name,None,c1) env) c2) - | T.LetIn (name,b,c1,c2) -> - T.subst1 b (type_of (Environ.push_rel (name,Some b,c1) env) c2) - | T.Fix ((_,i),(_,tys,_)) -> tys.(i) - | T.CoFix (i,(_,tys,_)) -> tys.(i) - | T.App(f,args)-> - T.strip_outer_cast - (subst_type env sigma (type_of env f) (Array.to_list args)) - | T.Cast (c,_, t) -> t - | T.Sort _ | T.Prod _ -> - match sort_of env cstr with - Coq_sort T.InProp -> T.mkProp - | Coq_sort T.InSet -> T.mkSet - | Coq_sort T.InType -> T.mkType Univ.type1_univ (* ERROR HERE *) - | CProp -> T.mkConst DoubleTypeInference.cprop - - and sort_of env t = - match Term.kind_of_term t with - | T.Cast (c,_, s) when T.isSort s -> family_of_term s - | T.Sort (T.Prop c) -> Coq_sort T.InType - | T.Sort (T.Type u) -> Coq_sort T.InType - | T.Prod (name,t,c2) -> - (match sort_of env t,sort_of (Environ.push_rel (name,None,t) env) c2 with - | _, (Coq_sort T.InProp as s) -> s - | Coq_sort T.InProp, (Coq_sort T.InSet as s) - | Coq_sort T.InSet, (Coq_sort T.InSet as s) -> s - | Coq_sort T.InType, (Coq_sort T.InSet as s) - | CProp, (Coq_sort T.InSet as s) when - Environ.engagement env = Some Declarations.ImpredicativeSet -> s - | Coq_sort T.InType, Coq_sort T.InSet - | CProp, Coq_sort T.InSet -> Coq_sort T.InType - | _, (Coq_sort T.InType as s) -> s (*Type Univ.dummy_univ*) - | _, (CProp as s) -> s) - | T.App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args - | T.Lambda _ | T.Fix _ | T.Construct _ -> - Util.anomaly "sort_of: Not a type (1)" - | _ -> outsort env sigma (type_of env t) - - and sort_family_of env t = - match T.kind_of_term t with - | T.Cast (c,_, s) when T.isSort s -> family_of_term s - | T.Sort (T.Prop c) -> Coq_sort T.InType - | T.Sort (T.Type u) -> Coq_sort T.InType - | T.Prod (name,t,c2) -> sort_family_of (Environ.push_rel (name,None,t) env) c2 - | T.App(f,args) -> - sort_of_atomic_type env sigma (type_of env f) args - | T.Lambda _ | T.Fix _ | T.Construct _ -> - Util.anomaly "sort_of: Not a type (1)" - | _ -> outsort env sigma (type_of env t) - - in type_of, sort_of, sort_family_of - - let get_type_of env sigma c = let f,_,_ = typeur sigma [] in f env c - let get_sort_family_of env sigma c = let _,_,f = typeur sigma [] in f env c - - end -;; - -let get_sort_family_of env evar_map ty = - CPropRetyping.get_sort_family_of env evar_map ty -;; - -let type_as_sort env evar_map ty = -(* CCorn code *) - family_of_term (DoubleTypeInference.whd_betadeltaiotacprop env evar_map ty) -;; - -let is_a_Prop = - function - "Prop" - | "CProp" -> true - | _ -> false -;; - -(* Main Functions *) - -type anntypes = - {annsynthesized : Acic.aconstr ; annexpected : Acic.aconstr option} -;; - -let gen_id seed = - let res = "i" ^ string_of_int !seed in - incr seed ; - res -;; - -let fresh_id seed ids_to_terms constr_to_ids ids_to_father_ids = - fun father t -> - let res = gen_id seed in - Hashtbl.add ids_to_father_ids res father ; - Hashtbl.add ids_to_terms res t ; - Acic.CicHash.add constr_to_ids t res ; - res -;; - -let source_id_of_id id = "#source#" ^ id;; - -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 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 ; - let rec aux computeinnertypes father passed_lambdas_or_prods_or_letins env - idrefs ?(subst=None,[]) tt - = - let fresh_id'' = fresh_id' father tt in - 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" - | CProp -> "CProp" - in - let string_of_sort t = - string_of_sort_family - (type_as_sort env evar_map t) - in - let ainnertypes,innertype,innersort,expected_available = - let {D.synthesized = synthesized; D.expected = expected} = - if computeinnertypes then -try - Acic.CicHash.find terms_to_types tt -with e when e <> Sys.Break -> -(*CSC: Warning: it really happens, for example in Ring_theory!!! *) -Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-type-inference: ") (Printer.pr_lconstr tt)) ; assert false - else - (* We are already in an inner-type and Coscoy's double *) - (* 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 = - Reductionops.nf_beta evar_map - (CPropRetyping.get_type_of env evar_map - (Termops.refresh_universes tt)) ; - D.expected = None} - in -(* Debugging only: -print_endline "TERMINE:" ; flush stdout ; -Pp.ppnl (Printer.pr_lconstr tt) ; flush stdout ; -print_endline "TIPO:" ; flush stdout ; -Pp.ppnl (Printer.pr_lconstr synthesized) ; flush stdout ; -print_endline "ENVIRONMENT:" ; flush stdout ; -Pp.ppnl (Printer.pr_context_of env) ; flush stdout ; -print_endline "FINE_ENVIRONMENT" ; flush stdout ; -*) - let innersort = - let synthesized_innersort = - get_sort_family_of env evar_map synthesized - in - match expected with - None -> synthesized_innersort - | Some ty -> - let expected_innersort = - get_sort_family_of env evar_map ty - in - match expected_innersort, synthesized_innersort with - CProp, _ - | _, CProp -> CProp - | _, _ -> expected_innersort - in -(* Debugging only: -print_endline "PASSATO" ; flush stdout ; -*) - let ainnertypes,expected_available = - if computeinnertypes then - let annexpected,expected_available = - match expected with - None -> None,false - | Some expectedty' -> - Some (aux false (Some fresh_id'') [] env idrefs expectedty'), - true - in - Some - {annsynthesized = - aux false (Some fresh_id'') [] env idrefs synthesized ; - annexpected = annexpected - }, expected_available - else - None,false - in - ainnertypes,synthesized, string_of_sort_family innersort, - expected_available - in - let add_inner_type id = - match ainnertypes with - None -> () - | Some ainnertypes -> Hashtbl.add ids_to_inner_types id ainnertypes - in - - (* explicit_substitute_and_eta_expand_if_required h t t' *) - (* where [t] = [] and [tt] = [h]{[t']} ("{.}" denotes explicit *) - (* named substitution) or [tt] = (App [h]::[t]) (and [t'] = []) *) - (* check if [h] is a term that requires an explicit named *) - (* substitution and, in that case, uses the first arguments of *) - (* [t] as the actual arguments of the substitution. If there *) - (* are not enough parameters in the list [t], then eta-expansion *) - (* is performed. *) - let - explicit_substitute_and_eta_expand_if_required h t t' - compute_result_if_eta_expansion_not_required - = - let subst,residual_args,uninst_vars = - let variables,basedir = - try - let g = Libnames.global_of_constr h in - let sp = - match g with - Libnames.ConstructRef ((induri,_),_) - | Libnames.IndRef (induri,_) -> - Nametab.path_of_global (Libnames.IndRef (induri,0)) - | Libnames.VarRef id -> - (* Invariant: variables are never cooked in Coq *) - raise Not_found - | _ -> Nametab.path_of_global g - in - Dischargedhypsmap.get_discharged_hyps sp, - get_module_path_of_full_path sp - with Not_found -> - (* no explicit substitution *) - [], Libnames.dirpath_of_string "dummy" - in - (* returns a triple whose first element is *) - (* an explicit named substitution of "type" *) - (* (variable * argument) list, whose *) - (* second element is the list of residual *) - (* arguments and whose third argument is *) - (* the list of uninstantiated variables *) - let rec get_explicit_subst variables arguments = - match variables,arguments with - [],_ -> [],arguments,[] - | _,[] -> [],[],variables - | he1::tl1,he2::tl2 -> - let subst,extra_args,uninst = get_explicit_subst tl1 tl2 in - let (he1_sp, he1_id) = Libnames.repr_path he1 in - let he1' = remove_module_dirpath_from_dirpath ~basedir he1_sp in - let he1'' = - String.concat "/" - (List.map Names.string_of_id (List.rev he1')) ^ "/" - ^ (Names.string_of_id he1_id) ^ ".var" - in - (he1'',he2)::subst, extra_args, uninst - in - get_explicit_subst variables t' - in - let uninst_vars_length = List.length uninst_vars in - if uninst_vars_length > 0 then - (* Not enough arguments provided. We must eta-expand! *) - let un_args,_ = - T.decompose_prod_n uninst_vars_length - (CPropRetyping.get_type_of env evar_map tt) - in - let eta_expanded = - let arguments = - List.map (T.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)) - in - D.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 - else - compute_result_if_eta_expansion_not_required subst residual_args - in - - (* 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 -> - let id = - match List.nth (E.rel_context env) (n - 1) with - (N.Name id,_,_) -> id - | (N.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.string_of_id pvars in - let path = get_uri_of_var (N.string_of_id 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.string_of_id id) ^ ".var") - | T.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 - (fresh_id'', n, Array.to_list (Array.map (aux' env idrefs) l)) - | T.Meta _ -> Util.anomaly "Meta met during exporting to XML" - | T.Sort s -> A.ASort (fresh_id'', s) - | T.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) -> - let n' = - match n with - N.Anonymous -> N.Anonymous - | _ -> - if not fake_dependent_products && T.noccurn 1 t then - N.Anonymous - else - N.Name - (Namegen.next_name_away n (Termops.ids_of_context env)) - in - Hashtbl.add ids_to_inner_sorts fresh_id'' - (string_of_sort innertype) ; - let sourcetype = CPropRetyping.get_type_of env evar_map s in - Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'') - (string_of_sort sourcetype) ; - let new_passed_prods = - let father_is_prod = - match father with - None -> false - | Some father' -> - match - Term.kind_of_term (Hashtbl.find ids_to_terms father') - with - T.Prod _ -> true - | _ -> false - in - (fresh_id'', n', aux' env idrefs s):: - (if father_is_prod then - passed_lambdas_or_prods_or_letins - else []) - in - let new_env = E.push_rel (n', None, s) env in - let new_idrefs = fresh_id''::idrefs in - (match Term.kind_of_term t with - T.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) -> - let n' = - match n with - N.Anonymous -> N.Anonymous - | _ -> - N.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 - Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'') - (string_of_sort sourcetype) ; - let father_is_lambda = - match father with - None -> false - | Some father' -> - match - Term.kind_of_term (Hashtbl.find ids_to_terms father') - with - T.Lambda _ -> true - | _ -> false - in - if is_a_Prop innersort && - ((not father_is_lambda) || expected_available) - then add_inner_type fresh_id'' ; - let new_passed_lambdas = - (fresh_id'',n', aux' env idrefs s):: - (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_idrefs = fresh_id''::idrefs in - (match Term.kind_of_term t with - T.Lambda _ -> - aux computeinnertypes (Some fresh_id'') new_passed_lambdas - new_env new_idrefs t - | _ -> - let t' = aux' new_env new_idrefs t in - (* eta-expansion for explicit named substitutions *) - (* can create nested Lambdas. Here we perform the *) - (* flattening. *) - match t' with - A.ALambdas (lambdas, t'') -> - A.ALambdas (lambdas@new_passed_lambdas, t'') - | _ -> - A.ALambdas (new_passed_lambdas, t') - ) - | T.LetIn (n,s,t,d) -> - let id = - match n with - N.Anonymous -> N.id_of_string "_X" - | N.Name id -> id - in - let n' = - N.Name (Namegen.next_ident_away id (Termops.ids_of_context env)) - in - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - let sourcesort = - get_sort_family_of env evar_map - (CPropRetyping.get_type_of env evar_map s) - in - Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'') - (string_of_sort_family sourcesort) ; - let father_is_letin = - match father with - None -> false - | Some father' -> - match - Term.kind_of_term (Hashtbl.find ids_to_terms father') - with - T.LetIn _ -> true - | _ -> false - in - if is_a_Prop innersort then - add_inner_type fresh_id'' ; - let new_passed_letins = - (fresh_id'',n', aux' env idrefs s):: - (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_idrefs = fresh_id''::idrefs in - (match Term.kind_of_term d with - T.LetIn _ -> - aux computeinnertypes (Some fresh_id'') new_passed_letins - new_env new_idrefs d - | _ -> A.ALetIns - (new_passed_letins, aux' new_env new_idrefs d)) - | T.App (h,t) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if is_a_Prop innersort then - add_inner_type fresh_id'' ; - let - compute_result_if_eta_expansion_not_required subst residual_args - = - let residual_args_not_empty = residual_args <> [] in - let h' = - if residual_args_not_empty then - aux' env idrefs ~subst:(None,subst) h - else - aux' env idrefs ~subst:(Some fresh_id'',subst) h - in - (* maybe all the arguments were used for the explicit *) - (* named substitution *) - if residual_args_not_empty then - A.AApp (fresh_id'', h'::residual_args) - else - h' - in - let t' = - Array.fold_right (fun x i -> (aux' env idrefs x)::i) t [] - in - explicit_substitute_and_eta_expand_if_required h - (Array.to_list t) t' - compute_result_if_eta_expansion_not_required - | T.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))) - 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) -> - let compute_result_if_eta_expansion_not_required _ _ = - A.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) -> - 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 - (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) -> - 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 - (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)) -> - Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; - if is_a_Prop innersort then add_inner_type fresh_id'' ; - let fresh_idrefs = - Array.init (Array.length t) (function _ -> gen_id seed) in - let new_idrefs = - (List.rev (Array.to_list fresh_idrefs)) @ idrefs - in - let f' = - let ids = ref (Termops.ids_of_context env) in - Array.map - (function - N.Anonymous -> Util.error "Anonymous fix function met" - | N.Name id as n -> - let res = N.Name (Namegen.next_name_away n !ids) in - ids := id::!ids ; - res - ) f - in - A.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 -> Util.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) - (Array.mapi - (fun j x -> (fresh_idrefs.(j),x,t.(j),b.(j),ai.(j))) f' - ) [] - ) - | T.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 = - Array.init (Array.length t) (function _ -> gen_id seed) in - let new_idrefs = - (List.rev (Array.to_list fresh_idrefs)) @ idrefs - in - let f' = - let ids = ref (Termops.ids_of_context env) in - Array.map - (function - N.Anonymous -> Util.error "Anonymous fix function met" - | N.Name id as n -> - let res = N.Name (Namegen.next_name_away n !ids) in - ids := id::!ids ; - res - ) f - in - A.ACoFix (fresh_id'', i, - Array.fold_right - (fun (id,fi,ti,bi) i -> - let fi' = - match fi with - N.Name fi -> fi - | N.Anonymous -> Util.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) - (Array.mapi - (fun j x -> (fresh_idrefs.(j),x,t.(j),b.(j)) ) f' - ) [] - ) - in - aux computeinnertypes None [] env idrefs t -;; - -(* Obsolete [HH 1/2009] -let acic_of_cic_context metasenv context t = - 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 - let ids_to_inner_sorts = Hashtbl.create 503 in - let ids_to_inner_types = Hashtbl.create 503 in - let seed = ref 0 in - acic_of_cic_context' true seed ids_to_terms constr_to_ids ids_to_father_ids - ids_to_inner_sorts ids_to_inner_types metasenv context t, - ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types -;; -*) - -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 - let ids_to_inner_sorts = Hashtbl.create 503 in - let ids_to_inner_types = Hashtbl.create 503 in - let ids_to_conjectures = Hashtbl.create 11 in - let ids_to_hypotheses = Hashtbl.create 127 in - let hypotheses_seed = ref 0 in - let conjectures_seed = ref 0 in - let seed = ref 0 in - let acic_term_of_cic_term_context' = - acic_of_cic_context' true seed ids_to_terms constr_to_ids ids_to_father_ids - ids_to_inner_sorts ids_to_inner_types in -(*CSC: is this the right env to use? Hhmmm. There is a problem: in *) -(*CSC: Global.env () the object we are exporting is already defined, *) -(*CSC: either in the environment or in the named context (in the case *) -(*CSC: of variables. Is this a problem? *) - let env = Global.env () in - let acic_term_of_cic_term' ?fake_dependent_products = - acic_term_of_cic_term_context' ?fake_dependent_products env [] sigma in -(*CSC: the fresh_id is not stored anywhere. This _MUST_ be fixed using *) -(*CSC: a modified version of the already existent fresh_id function *) - let fresh_id () = - let res = "i" ^ string_of_int !seed in - incr seed ; - res - in - let aobj = - match obj with - A.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) -> - 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) -> - let aconjectures = - List.map - (function (i,canonical_context,term) as conjecture -> - let cid = "c" ^ string_of_int !conjectures_seed in - Hashtbl.add ids_to_conjectures cid conjecture ; - incr conjectures_seed ; - let canonical_env,idrefs',acanonical_context = - let rec aux env idrefs = - function - [] -> env,idrefs,[] - | ((n,decl_or_def) as hyp)::tl -> - let hid = "h" ^ string_of_int !hypotheses_seed in - let new_idrefs = hid::idrefs in - Hashtbl.add ids_to_hypotheses hid hyp ; - incr hypotheses_seed ; - match decl_or_def with - A.Decl t -> - let final_env,final_idrefs,atl = - aux (Environ.push_rel (Names.Name n,None,t) env) - new_idrefs tl - in - 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) -> - let final_env,final_idrefs,atl = - aux - (Environ.push_rel (Names.Name n,Some t,ty) env) - new_idrefs tl - in - let at = - acic_term_of_cic_term_context' env idrefs sigma t None - in - let dummy_never_used = - let s = "dummy_never_used" in - A.ARel (s,99,s,Names.id_of_string s) - in - final_env,final_idrefs, - (hid,(n,A.Def (at,dummy_never_used)))::atl - in - aux env [] canonical_context - in - let aterm = - acic_term_of_cic_term_context' canonical_env idrefs' sigma term - None - in - (cid,i,List.rev acanonical_context,aterm) - ) 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) -> - let env' = - List.fold_right - (fun (name,_,arity,_) env -> - Environ.push_rel (Names.Name name, None, arity) env - ) (List.rev tys) env in - let idrefs = List.map (function _ -> gen_id seed) tys in - let atys = - List.map2 - (fun id (name,inductive,ty,cons) -> - let acons = - List.map - (function (name,ty) -> - (name, - acic_term_of_cic_term_context' ~fake_dependent_products:true - env' idrefs Evd.empty ty None) - ) cons - in - let aty = - acic_term_of_cic_term' ~fake_dependent_products:true ty None - in - (id,name,inductive,aty,acons) - ) (List.rev idrefs) tys - in - A.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 -;; |