+open Printf
+
+let pp_indtypes indTypes =
+ List.iter
+ (fun (name, _, typ, constructors) ->
+ printf "%s: %s\n" name (CicPp.ppterm typ);
+ List.iter
+ (fun (name, term) -> printf "\t%s: %s\n" name (CicPp.ppterm term))
+ constructors)
+ indTypes;
+ flush stdout
+
+let inddef_of_ast params indTypes (disambiguator:MatitaTypes.disambiguator) =
+ let add_pi binders t =
+ List.fold_right
+ (fun (name, ast) acc ->
+ CicAst.Binder (`Forall, (Cic.Name name, Some ast), acc))
+ binders t
+ in
+ let ind_binders =
+ List.map (fun (name, _, typ, _) -> (name, add_pi params typ)) indTypes
+ in
+ let binders = ind_binders @ params in
+ let asts = ref [] in
+ let add_ast ast = asts := ast :: !asts in
+ let paramsno = List.length params in
+ let indbindersno = List.length ind_binders in
+ List.iter
+ (fun (name, _, typ, constructors) ->
+ add_ast (add_pi params typ);
+ List.iter (fun (_, ast) -> add_ast (add_pi binders ast)) constructors)
+ indTypes;
+ let (_, metasenv, terms, ugraph) =
+ disambiguator#disambiguateTermAsts ~metasenv:[] !asts
+ in
+ let terms = ref (List.rev terms) in
+ let get_term () =
+ match !terms with [] -> assert false | hd :: tl -> terms := tl; hd
+ in
+ let uri =
+ match indTypes with
+ | (name, _, _, _) :: _ -> qualify name ^ ".ind"
+ | _ -> assert false
+ in
+ let mutinds =
+ let counter = ref 0 in
+ List.map
+ (fun _ ->
+ incr counter;
+ CicUtil.term_of_uri (sprintf "%s#xpointer(1/%d)" uri !counter))
+ indTypes
+ in
+ let subst_mutinds = List.fold_right CicSubstitution.subst mutinds in
+ let cicIndTypes =
+ List.fold_left
+ (fun acc (name, inductive, typ, constructors) ->
+ let cicTyp = get_term () in
+ let cicConstructors =
+ List.fold_left
+ (fun acc (name, _) ->
+ let typ =
+ subst_mutinds (CicUtil.strip_prods indbindersno (get_term ()))
+ in
+ (name, typ) :: acc)
+ [] constructors
+ in
+ (name, inductive, cicTyp, List.rev cicConstructors) :: acc)
+ [] indTypes
+ in
+ let cicIndTypes = List.rev cicIndTypes in
+ (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno))
+
+let save_object_to_disk uri obj =
+ let ensure_path_exists path =
+ let dir = Filename.dirname path in
+ try
+ let stats = Unix.stat dir in
+ if stats.Unix.st_kind <> Unix.S_DIR then
+ raise (Failure (dir ^ " already exists and is not a directory"))
+ else
+ ()
+ with
+ Unix.Unix_error (_,_,_) ->
+ let pstatus = Unix.system ("mkdir -p " ^ dir) in
+ match pstatus with
+ | Unix.WEXITED n when n = 0 -> ()
+ | _ -> raise (Failure ("Unable to create " ^ dir))
+ in
+ (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
+ let annobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ =
+ Cic2acic.acic_object_of_cic_object ~eta_fix:false obj
+ in
+ (* prepare XML *)
+ let xml, bodyxml =
+ Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false
+ annobj
+ in
+ let xmlinnertypes =
+ Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
+ ~ask_dtd_to_the_getter:false
+ in
+ (* prepare URIs and paths *)
+ let innertypesuri = UriManager.innertypesuri_of_uri uri in
+ let bodyuri = UriManager.bodyuri_of_uri uri in
+ let innertypesfilename = Str.replace_first (Str.regexp "^cic:") ""
+ (UriManager.string_of_uri innertypesuri) ^ ".xml.gz" in
+ let innertypespath = !(Lazy.force basedir) ^ "/" ^ innertypesfilename in
+ let xmlfilename = Str.replace_first (Str.regexp "^cic:/") ""
+ (UriManager.string_of_uri uri) ^ ".xml.gz" in
+ let xmlpath = !(Lazy.force basedir) ^ "/" ^ xmlfilename in
+ let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:/") ""
+ (UriManager.string_of_uri uri) ^ ".body.xml.gz" in
+ let xmlbodypath = !(Lazy.force basedir) ^ "/" ^ xmlbodyfilename in
+ let path_scheme_of path = "file://" ^ path in
+ MatitaMisc.mkdirs (List.map Filename.dirname [innertypespath; xmlpath]);
+ (* now write to disk *)
+ ensure_path_exists innertypespath;
+ Xml.pp ~gzip:true xmlinnertypes (Some innertypespath) ;
+ ensure_path_exists xmlpath;
+ Xml.pp ~gzip:true xml (Some xmlpath) ;
+
+ (* now register to the getter *)
+ Http_getter.register' innertypesuri (path_scheme_of innertypespath);
+ Http_getter.register' uri (path_scheme_of xmlpath);
+ (* now the optional body, both write and register *)
+ (match bodyxml,bodyuri with
+ None,None -> ()
+ | Some bodyxml,Some bodyuri->
+ ensure_path_exists xmlbodypath;
+ Xml.pp ~gzip:true bodyxml (Some xmlbodypath) ;
+ Http_getter.register' bodyuri (path_scheme_of xmlbodypath)
+ | _-> assert false)
+
+ (* TODO ZACK a lot more to be done here:
+ * - save universe file *)
+let add_constant_to_world ~(console: #MatitaTypes.console)
+ ~dbd ~uri ?body ~ty ?(params = []) ?(attrs = []) ~ugraph ()