diff options
Diffstat (limited to 'plugins/xml/cic2acic.ml')
| -rw-r--r-- | plugins/xml/cic2acic.ml | 231 |
1 files changed, 109 insertions, 122 deletions
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 |