diff options
Diffstat (limited to 'plugins/interface/name_to_ast.ml')
| -rw-r--r-- | plugins/interface/name_to_ast.ml | 46 |
1 files changed, 23 insertions, 23 deletions
diff --git a/plugins/interface/name_to_ast.ml b/plugins/interface/name_to_ast.ml index f5e8be31e..ef61a8202 100644 --- a/plugins/interface/name_to_ast.ml +++ b/plugins/interface/name_to_ast.ml @@ -26,7 +26,7 @@ open Topconstr;; of this procedure is taken from the function print_env in pretty.ml *) let convert_env = let convert_binder env (na, b, c) = - match b with + match b with | Some b -> LocalRawDef ((dummy_loc,na), extern_constr true env b) | None -> LocalRawAssum ([dummy_loc,na], default_binder_kind, extern_constr true env c) in let rec cvrec env = function @@ -34,7 +34,7 @@ let convert_env = | b::rest -> (convert_binder env b)::(cvrec (push_rel b env) rest) in cvrec (Global.env());; -(* let mib string = +(* let mib string = let sp = Nametab.sp_of_id CCI (id_of_string string) in let lobj = Lib.map_leaf (objsp_of sp) in let (cmap, _) = outMutualInductive lobj in @@ -52,10 +52,10 @@ let impl_args_to_string_by_pos = function (* This function is directly inspired by implicit_args_id in pretty.ml *) -let impl_args_to_string l = +let impl_args_to_string l = impl_args_to_string_by_pos (positions_of_implicits l) -let implicit_args_id_to_ast_list id l ast_list = +let implicit_args_id_to_ast_list id l ast_list = (match impl_args_to_string l with None -> ast_list | Some(s) -> CommentString s:: @@ -67,7 +67,7 @@ let implicit_args_id_to_ast_list id l ast_list = implicit_args_msg in pretty.ml. *) let implicit_args_to_ast_list sp mipv = - let implicit_args_descriptions = + let implicit_args_descriptions = let ast_list = ref [] in (Array.iteri (fun i mip -> @@ -78,7 +78,7 @@ let implicit_args_to_ast_list sp mipv = (fun j idc -> let impls = implicits_of_global (ConstructRef ((sp,i),j+1)) in - ast_list := + ast_list := implicit_args_id_to_ast_list idc impls !ast_list) mip.mind_consnames)) mipv; @@ -86,19 +86,19 @@ let implicit_args_to_ast_list sp mipv = match implicit_args_descriptions with [] -> [] | _ -> [VernacComments (List.rev implicit_args_descriptions)];; - + (* This function converts constructors for an inductive definition to a Coqast.t. It is obtained directly from print_constructors in pretty.ml *) let convert_constructors envpar names types = - let array_idC = - array_map2 - (fun n t -> + let array_idC = + array_map2 + (fun n t -> let coercion_flag = false (* arbitrary *) in (coercion_flag, ((dummy_loc,n), extern_constr true envpar t))) names types in Array.to_list array_idC;; - + (* this function converts one inductive type in a possibly multiple inductive definition *) @@ -124,7 +124,7 @@ let mutual_to_ast_list sp mib = VernacInductive ((if mib.mind_finite then Decl_kinds.Finite else Decl_kinds.CoFinite), false, l) :: (implicit_args_to_ast_list sp mipv);; -let constr_to_ast v = +let constr_to_ast v = extern_constr true (Global.env()) v;; let implicits_to_ast_list implicits = @@ -137,10 +137,10 @@ let make_variable_ast name typ implicits = ((Local,Definitional),false,(*inline flag*) [false,([dummy_loc,name], constr_to_ast typ)])) ::(implicits_to_ast_list implicits);; - + let make_definition_ast name c typ implicits = - VernacDefinition ((Global,false,Definition), (dummy_loc,name), + VernacDefinition ((Global,false,Definition), (dummy_loc,name), DefineBody ([], None, constr_to_ast c, Some (constr_to_ast typ)), (fun _ _ -> ())) ::(implicits_to_ast_list implicits);; @@ -152,7 +152,7 @@ let constant_to_ast_list kn = let typ = Typeops.type_of_constant_type (Global.env()) cb.const_type in let l = implicits_of_global (ConstRef kn) in (match c with - None -> + None -> make_variable_ast (id_of_label (con_label kn)) typ l | Some c1 -> make_definition_ast (id_of_label (con_label kn)) (Declarations.force c1) typ l) @@ -161,7 +161,7 @@ let variable_to_ast_list sp = let (id, c, v) = Global.lookup_named sp in let l = implicits_of_global (VarRef sp) in (match c with - None -> + None -> make_variable_ast id v l | Some c1 -> make_definition_ast id c1 v l);; @@ -180,8 +180,8 @@ let leaf_entry_to_ast_list ((sp,kn),lobj) = | "VARIABLE" -> variable_to_ast_list (basename sp) | "CONSTANT" -> constant_to_ast_list (constant_of_kn kn) | "INDUCTIVE" -> inductive_to_ast_list kn - | s -> - errorlabstrm + | s -> + errorlabstrm "print" (str ("printing of unrecognized object " ^ s ^ " has been required"));; @@ -191,18 +191,18 @@ let leaf_entry_to_ast_list ((sp,kn),lobj) = (* this function is inspired by print_name *) let name_to_ast ref = let (loc,qid) = qualid_of_reference ref in - let l = - try + let l = + try match Nametab.locate qid with | ConstRef sp -> constant_to_ast_list sp | IndRef (sp,_) -> inductive_to_ast_list sp | ConstructRef ((sp,_),_) -> inductive_to_ast_list sp | VarRef sp -> variable_to_ast_list sp - with Not_found -> + with Not_found -> try (* Var locale de but, pas var de section... donc pas d'implicits *) - let dir,name = repr_qualid qid in + let dir,name = repr_qualid qid in if (repr_dirpath dir) <> [] then raise Not_found; - let (_,c,typ) = Global.lookup_named name in + let (_,c,typ) = Global.lookup_named name in (match c with None -> make_variable_ast name typ [] | Some c1 -> make_definition_ast name c1 typ []) |