let (name, body, typ) = Environ.lookup_rel i env in

match name with

Name id -> build_var id

let s_ast =

match s with

Prop _ -> if s = prop_sort then "Prop" else "Set"

| Type _ -> "Type" (* skip universe *)

match k with

VMcast -> "VMcast"

| DEFAULTcast -> "DEFAULTcast"

| REVERTcast -> "REVERTcast"

let num_args = Leaf (string_of_int info.ci_npar) in

let match_typ = Node ("CaseMatch", [match_ast]) in

let branches = Node ("CaseBranches", branch_asts) in

match cb.const_body with

| Undef _ ->

None

| Def cs ->

Some (Mod_subst.force_constr cs)

| OpaqueDef o ->

Array.to_list

(CArray.map2_i

(fun i name typ -> (name, None, Vars.lift i typ))

List.map

(fun ind_body ->

let univ_context = mutind_body.mind_universes in

let univ_instance = UContext.instance univ_context in

let name_id = ind_body.mind_typename in

let mutind_spec = (mutind_body, ind_body) in

let typ = Inductive.type_of_inductive env (mutind_spec, univ_instance) in

(Names.Name name_id, None, typ))

let constr_names = Array.to_list ind_body.mind_consnames in

let indexes = List.map string_of_int (range 1 ((List.length constr_names) + 1)) in

let constrs = Array.to_list ind_body.mind_user_lc in

match kind_of_term trm with

| Rel i ->

build_rel env i

| Var v ->

build_var v

| Meta mv ->

build_meta mv

| Evar (k, cs) ->

let cs' = List.map (build_ast env depth) (Array.to_list cs) in

build_evar k cs'

| Sort s ->

build_sort s

| Cast (c, k, t) ->

let c' = build_ast env depth c in

let t' = build_ast env depth t in

build_cast c' k t'

| Prod (n, t, b) ->

let t' = build_ast env depth t in

let b' = build_ast (Environ.push_rel (n, None, t) env) depth b in

build_product n t' b'

| Lambda (n, t, b) ->

let t' = build_ast env depth t in

let b' = build_ast (Environ.push_rel (n, None, t) env) depth b in

build_lambda n t' b'

| LetIn (n, t, e, b) ->

let t' = build_ast env depth t in

let e' = build_ast env depth e in

let b' = build_ast (Environ.push_rel (n, Some e, t) env) depth b in

build_let_in n t' e' b'

| App (f, xs) ->

let f' = build_ast env depth f in

let xs' = List.map (build_ast env depth) (Array.to_list xs) in

build_app f' xs'

| Case (ci, ct, m, bs) ->

let typ = build_ast env depth ct in

let match_typ = build_ast env depth m in

let branches = List.map (build_ast env depth) (Array.to_list bs) in

build_case ci typ match_typ branches

| Proj (p, c) ->

let p' = build_ast env depth (Term.mkConst (Projection.constant p)) in

let c' = build_ast env depth c in

build_proj p' c'

| Construct ((i, c_index), _) ->

build_construct i c_index

| Const c ->

build_const env depth c

| Fix ((is, i), (ns, ts, ds)) ->

build_fix i (build_fixpoint_functions env depth ns ts ds)

| CoFix (i, (ns, ts, ds)) ->

build_cofix i (build_fixpoint_functions env depth ns ts ds)

| Ind i ->

let kn = Constant.canonical c in

if depth <= 0 then (* don't expand *)

Node ("Const", [Leaf (string_of_kn kn)])

else (* expand *)

let cb = Environ.lookup_constant c env in

match get_definition cb with

| None ->

begin

match cb.const_type with

| RegularArity _ -> (* axiom *)

Node ("Const", [Leaf (string_of_kn kn)])

| TemplateArity _ -> assert false

end

| Some t ->

let env_fix = Environ.push_rel_context (bindings_for_fix names typs) env in

List.map

(fun i ->

let def = build_ast env_fix depth (Array.get defs i) in

build_fix_fun i def)

if depth <= 0 then (* don't expand *)

let kn = Names.canonical_mind i in

Node ("MInd", [Leaf (string_of_kn kn); Leaf (string_of_int i_index)])

else (* expand *)

let mutind_body = Environ.lookup_mind i env in

let ind_bodies = mutind_body.mind_packets in

let ind_bodies_list = Array.to_list ind_bodies in

let env_ind = Environ.push_rel_context (bindings_for_inductive env mutind_body ind_bodies_list) env in

let cs = List.map (build_oinductive env_ind depth) ind_bodies_list in

let constrs =

List.map (fun (i, (n, typ)) -> Node ("Cons", [Leaf i; Leaf (Names.string_of_id n); build_ast env (depth - 1) typ])) (named_constructors ind_body)

in

match a with

| Leaf s -> s

| Node (h, l) ->

let sl = List.map string_of_ast l in

let s = String.concat " " sl in

match a with

| Leaf v -> hash v

| Node (v, l) ->

let ls = v :: List.map (digest_of_ast hash) l in

match gref with

| Globnames.VarRef _ -> ""

| Globnames.ConstRef cst ->

Names.string_of_kn (Names.canonical_con cst)

| Globnames.IndRef (kn,_) ->

Names.string_of_kn (Names.canonical_mind kn)

let (loc,qid) = Libnames.qualid_of_reference ref in

try Nametab.dirpath_of_module (Nametab.locate_module qid)

with Not_found ->

let selected_gref = ref [] in

let select gref env constr =

if Search.module_filter (dirlist, false) gref env constr

then selected_gref := gref :: !selected_gref

in

Search.generic_search None select;

try

let glob = Glob_term.GRef(Loc.ghost, gref, None) in

let env = Global.env() in

let sigma = Evd.from_env env in

let sigma', c = Pretyping.understand_tcc env sigma glob in

let sigma2 = Evarconv.consider_remaining_unif_problems env sigma' in

let sigma3, nf = Evarutil.nf_evars_and_universes sigma2 in

let pl, uctx = Evd.universe_context sigma3 in

let env2 = Environ.push_context uctx (Evarutil.nf_env_evar sigma3 env) in

let c2 = nf c in

let t = Environ.j_type (Typeops.infer env2 c2) in

let t2 = Environ.j_type (Typeops.infer env2 t) in

Term.is_Prop t2

with _ ->

begin

Pp.msg_error (str "unable to determine the type of the type for ref");

false

match gref with

| Globnames.VarRef _ -> false

| Globnames.ConstRef cst ->

let cb = Environ.lookup_constant cst (Global.env ()) in

(match cb.Declarations.const_body with

| Declarations.OpaqueDef _ -> true

| _ -> false)

let fmt =

match out with

| Some oc -> Pp_control.with_output_to oc

| None -> Buffer.clear buf; Format.formatter_of_buffer buf

in

Format.pp_set_max_boxes fmt max_int;

let type_ast = build_ast (Global.env ()) 0 t_type in

let type_digest = digest_of_ast hash type_ast in

let s = Printf.sprintf

"%s { \"name\": \"%s\", \"isProp\": %B, \"isOpaque\": %B, \"typeDigest\": \"%s\" }"

!delim (string_of_gref gref) (is_prop gref) (is_opaque gref) type_digest

in

pp_with fmt (str s);

let body_ast = build_ast (Global.env ()) 1 t_body in

let body_digest = digest_of_ast hash body_ast in

let s = Printf.sprintf

"%s { \"name\": \"%s\", \"isProp\": %B, \"isOpaque\": %B, \"bodyDigest\": \"%s\" }"

!delim (string_of_gref gref) (is_prop gref) (is_opaque gref) body_digest

in

pp_with fmt (str s);

let type_ast = build_ast (Global.env ()) 0 t_type in

let body_ast = build_ast (Global.env ()) 1 t_body in

let type_digest = digest_of_ast hash type_ast in

let body_digest = digest_of_ast hash body_ast in

let s = Printf.sprintf

"%s { \"name\": \"%s\", \"isProp\": %B, \"isOpaque\": %B, \"typeDigest\": \"%s\", \"bodyDigest\": \"%s\" }"

!delim (string_of_gref gref) (is_prop gref) (is_opaque gref) type_digest body_digest

in

pp_with fmt (str s);

match gref with

| Globnames.VarRef _ -> ()

| Globnames.ConstRef cst ->

let t = mkConst cst in

print_ast fmt gref t

| Globnames.IndRef i ->

let t = mkInd i in

print_ast fmt gref t

match gref with

| Globnames.ConstRef cst ->

let cb = Environ.lookup_constant cst (Global.env()) in

begin match cb.Declarations.const_type with

| Declarations.RegularArity t ->

let ast = build_ast (Global.env ()) 0 t in

let s = Printf.sprintf "%s: %s\n" (string_of_gref gref) (string_of_ast ast) in

pp_with fmt (str s)

| Declarations.TemplateArity _ -> ()

end

match gref with

| Globnames.VarRef _ -> ()

| Globnames.ConstRef cst ->

let t_body = mkConst cst in

let cb = Environ.lookup_constant cst (Global.env()) in

begin match cb.Declarations.const_type with

| Declarations.RegularArity t_type ->

print_ast_all_digest hash fmt gref t_type t_body delim

| Declarations.TemplateArity _ ->

print_ast_body_digest hash fmt gref t_body delim

end

| Globnames.IndRef i ->

let t_body = mkInd i in

print_ast_body_digest hash fmt gref t_body delim