+let obj_of_constant status ~metasenv uri height bo ty =
+ match classify status ~metasenv [] ty with
+ | `Kind ->
+ let ty = kind_of status ~metasenv [] ty in
+ let ctx0,res = split_kind_prods [] ty in
+ let ctx,bo =
+ split_typ_lambdas status ~metasenv (List.length ctx0) [] bo in
+ (match classify status ~metasenv ctx bo with
+ | `Type
+ | `KindOrType -> (* ?? no kind formers in System F_omega *)
+ let nicectx =
+ List.map2
+ (fun p1 n ->
+ HExtlib.map_option (fun (_,k) ->
+ (*CSC: BUG here, clashes*)
+ String.uncapitalize (fst n),k) p1)
+ ctx0 ctx
+ in
+ (* BUG here: for mutual type definitions the spec is not good *)
+ let ref =
+ NReference.reference_of_spec uri (NReference.Def height) in
+ let bo = typ_of status ~metasenv ctx bo in
+ status#set_extraction_db
+ (ReferenceMap.add ref (nicectx,Some bo)
+ status#extraction_db),
+ Some (uri,TypeDefinition((nicectx,res),bo))
+ | `Kind -> status, None
+ | `PropKind
+ | `Proposition -> status, None
+ | `Term _ -> assert false (* IMPOSSIBLE *))
+ | `PropKind
+ | `Proposition -> status, None
+ | `KindOrType (* ??? *)
+ | `Type ->
+ (* CSC: TO BE FINISHED, REF NON REGISTERED *)
+ let ty = typ_of status ~metasenv [] ty in
+ status,
+ Some (uri, TermDefinition (split_typ_prods [] ty,
+ term_of status ~metasenv [] bo))
+ | `Term _ -> assert false (* IMPOSSIBLE *)
+;;
+