diff options
Diffstat (limited to 'contrib/interface/name_to_ast.ml')
| -rw-r--r-- | contrib/interface/name_to_ast.ml | 252 |
1 files changed, 252 insertions, 0 deletions
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml new file mode 100644 index 00000000..eaff0968 --- /dev/null +++ b/contrib/interface/name_to_ast.ml @@ -0,0 +1,252 @@ +open Sign;; +open Classops;; +open Names;; +open Nameops +open Coqast;; +open Ast;; +open Termast;; +open Term;; +open Impargs;; +open Reduction;; +open Libnames;; +open Libobject;; +open Environ;; +open Declarations;; +open Prettyp;; +open Inductive;; +open Util;; +open Pp;; +open Declare;; +open Nametab +open Vernacexpr;; +open Decl_kinds;; +open Constrextern;; +open Topconstr;; + +(* This function converts the parameter binders of an inductive definition, + in particular you have to be careful to handle each element in the + context containing all previously defined variables. This squeleton + 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 + | Some b -> LocalRawDef ((dummy_loc,na), extern_constr true env b) + | None -> LocalRawAssum ([dummy_loc,na], extern_constr true env c) in + let rec cvrec env = function + [] -> [] + | b::rest -> (convert_binder env b)::(cvrec (push_rel b env) rest) in + cvrec (Global.env());; + +(* 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 + Listmap.map cmap CCI;; *) + +(* This function is directly inspired by print_impl_args in pretty.ml *) + +let impl_args_to_string_by_pos = function + [] -> None + | [i] -> Some(" position " ^ (string_of_int i) ^ " is implicit.") + | l -> Some (" positions " ^ + (List.fold_right (fun i s -> (string_of_int i) ^ " " ^ s) + l + " are implicit."));; + +(* This function is directly inspired by implicit_args_id in pretty.ml *) + +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 = + (match impl_args_to_string l with + None -> ast_list + | Some(s) -> CommentString s:: + CommentString ("For " ^ (string_of_id id)):: + ast_list);; + +(* This function construct an ast to enumerate the implicit positions for an + inductive type and its constructors. It is obtained directly from + implicit_args_msg in pretty.ml. *) + +let implicit_args_to_ast_list sp mipv = + let implicit_args_descriptions = + let ast_list = ref [] in + (Array.iteri + (fun i mip -> + let imps = implicits_of_global (IndRef (sp, i)) in + (ast_list := + implicit_args_id_to_ast_list mip.mind_typename imps !ast_list; + Array.iteri + (fun j idc -> + let impls = implicits_of_global + (ConstructRef ((sp,i),j+1)) in + ast_list := + implicit_args_id_to_ast_list idc impls !ast_list) + mip.mind_consnames)) + mipv; + !ast_list) in + match implicit_args_descriptions with + [] -> [] + | _ -> [VernacComments (List.rev implicit_args_descriptions)];; + +let convert_qualid qid = + let d, id = Libnames.repr_qualid qid in + match repr_dirpath d with + [] -> nvar id + | d -> ope("QUALID", List.fold_left (fun l s -> (nvar s)::l) + [nvar id] d);; + +(* 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 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 *) + +let convert_one_inductive sp tyi = + let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp tyi in + let env = Global.env () in + let envpar = push_rel_context params env in + let sp = sp_of_global (IndRef (sp, tyi)) in + ((dummy_loc,basename sp), None, + convert_env(List.rev params), + (extern_constr true envpar arity), + convert_constructors envpar cstrnames cstrtypes);; + +(* This function converts a Mutual inductive definition to a Coqast.t. + It is obtained directly from print_mutual in pretty.ml. However, all + references to kinds have been removed and it treats only CCI stuff. *) + +let mutual_to_ast_list sp mib = + let mipv = (Global.lookup_mind sp).mind_packets in + let _, l = + Array.fold_right + (fun mi (n,l) -> (n+1, (convert_one_inductive sp n)::l)) mipv (0, []) in + VernacInductive (mib.mind_finite, l) + :: (implicit_args_to_ast_list sp mipv);; + +let constr_to_ast v = + extern_constr true (Global.env()) v;; + +let implicits_to_ast_list implicits = + match (impl_args_to_string implicits) with + | None -> [] + | Some s -> [VernacComments [CommentString s]];; + +(* +let make_variable_ast name typ implicits = + (ope("VARIABLE", + [string "VARIABLE"; + ope("BINDERLIST", + [ope("BINDER", + [(constr_to_ast (body_of_type typ)); + nvar name])])]))::(implicits_to_ast_list implicits) + ;; +*) +let make_variable_ast name typ implicits = + (VernacAssumption + ((Local,Definitional), + [false,([dummy_loc,name], constr_to_ast (body_of_type typ))])) + ::(implicits_to_ast_list implicits);; + + +let make_definition_ast name c typ implicits = + VernacDefinition ((Global,Definition), (dummy_loc,name), DefineBody ([], None, + (constr_to_ast c), Some (constr_to_ast (body_of_type typ))), + (fun _ _ -> ())) + ::(implicits_to_ast_list implicits);; + +(* This function is inspired by print_constant *) +let constant_to_ast_list kn = + let cb = Global.lookup_constant kn in + let c = cb.const_body in + let typ = cb.const_type in + let l = implicits_of_global (ConstRef kn) in + (match c with + None -> + make_variable_ast (id_of_label (label kn)) typ l + | Some c1 -> + make_definition_ast (id_of_label (label kn)) (Declarations.force c1) typ l) + +let variable_to_ast_list sp = + let (id, c, v) = get_variable sp in + let l = implicits_of_global (VarRef sp) in + (match c with + None -> + make_variable_ast id v l + | Some c1 -> + make_definition_ast id c1 v l);; + +(* this function is taken from print_inductive in file pretty.ml *) + +let inductive_to_ast_list sp = + let mib = Global.lookup_mind sp in + mutual_to_ast_list sp mib + +(* this function is inspired by print_leaf_entry from pretty.ml *) + +let leaf_entry_to_ast_list ((sp,kn),lobj) = + let tag = object_tag lobj in + match tag with + | "VARIABLE" -> variable_to_ast_list (basename sp) + | "CONSTANT" -> constant_to_ast_list kn + | "INDUCTIVE" -> inductive_to_ast_list kn + | s -> + errorlabstrm + "print" (str ("printing of unrecognized object " ^ + s ^ " has been required"));; + + + + +(* this function is inspired by print_name *) +let name_to_ast ref = + let (loc,qid) = qualid_of_reference ref in + let l = + try + let sp = Nametab.locate_obj qid in + let (sp,lobj) = + let (sp,entry) = + List.find (fun en -> (fst (fst en)) = sp) (Lib.contents_after None) + in + match entry with + | Lib.Leaf obj -> (sp,obj) + | _ -> raise Not_found + in + leaf_entry_to_ast_list (sp,lobj) + with Not_found -> + 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 -> + try (* Var locale de but, pas var de section... donc pas d'implicits *) + let dir,name = repr_qualid qid in + if (repr_dirpath dir) <> [] then raise Not_found; + 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 []) + with Not_found -> + try + let sp = Nametab.locate_syntactic_definition qid in + errorlabstrm "print" + (str "printing of syntax definitions not implemented") + with Not_found -> + errorlabstrm "print" + (pr_qualid qid ++ + spc () ++ str "not a defined object") + in + VernacList (List.map (fun x -> (dummy_loc,x)) l) + |