- (insert_owner, insert_sort, insert_rel, insert_obj)
-
-let execute_insert dbh (insert_owner, insert_sort, insert_rel, insert_obj)
- uri owner (sort_cols, rel_cols, obj_cols)
-=
- insert_owner#execute [`String uri; `String owner];
- List.iter insert_sort#execute sort_cols;
- List.iter insert_rel#execute rel_cols;
- List.iter insert_obj#execute obj_cols
-
-let insert_const_no dbh uri =
+ if sort_tuples <> [] then
+ begin
+ let query_sort =
+ sprintf "INSERT %s VALUES %s;" (sort_tbl ()) (String.concat "," sort_tuples)
+ in
+ ignore (Mysql.exec dbd query_sort)
+ end;
+ if rel_tuples <> [] then
+ begin
+ let query_rel =
+ sprintf "INSERT %s VALUES %s;" (rel_tbl ()) (String.concat "," rel_tuples)
+ in
+ ignore (Mysql.exec dbd query_rel)
+ end;
+ if obj_tuples <> [] then
+ begin
+ let query_obj =
+ sprintf "INSERT %s VALUES %s;" (obj_tbl ()) (String.concat "," obj_tuples)
+ in
+ ignore (Mysql.exec dbd query_obj)
+ end
+
+
+let count_distinct position l =
+ MetadataConstraints.StringSet.cardinal
+ (List.fold_left (fun acc d ->
+ match position with
+ | `Conclusion ->
+ (match d with
+ | `Obj (name,`InConclusion)
+ | `Obj (name,`MainConclusion _ ) ->
+ MetadataConstraints.StringSet.add name acc
+ | _ -> acc)
+ | `Hypothesis ->
+ (match d with
+ | `Obj (name,`InHypothesis)
+ | `Obj (name,`MainHypothesis _) ->
+ MetadataConstraints.StringSet.add name acc
+ | _ -> acc)
+ | `Statement ->
+ (match d with
+ | `Obj (name,`InBody) -> acc
+ | `Obj (name,_) -> MetadataConstraints.StringSet.add name acc
+ | _ -> acc)
+ ) MetadataConstraints.StringSet.empty l)
+(*
+let insert_const_no dbd uri =
+ let term = CicUtil.term_of_uri uri in
+ let ty = CicTypeChecker.type_of_aux'